[analyzer] Undefined or garbage value for slightly complex loop variables

classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

[analyzer] Undefined or garbage value for slightly complex loop variables

suyash singh via cfe-dev
I hit a problem where it seems the analyzer is not tracking loop control as expected. In the following code, I see a[0] is detected to be a garbage value when symbolically executed. 

clang -cc1 -analyze  -analyzer-checker=core  test.c 
test.c:19:3: warning: Undefined or garbage value returned to caller
  return a[0];
  ^~~~~~~~~~~
1 warning generated.

Dumping the egraph, I see that the analyzer eagerly assumes the expression "x < (offs+users)" is false along one of the paths, which is what leads to the failure. 

1) clang -cc1 -analyze  -analyzer-checker=core  -analyzer-config  eagerly-assume=true  -analyzer-dump-egraph=graph.dot  -trim-egraph   test.c
2) exploded-graph-rewriter.py --single-path --diff --diff graph.dot

Program points: 61. test.c: 14 : 18 : BinaryOperator S867 PostStmt x < (offs + users) Tag: ExprEngine : Eagerly Assume False 62. BlockEdge [B4] -> [B1] 63. BlockEntrance [B1] Store: (0x814b8a8) No changes! Expressions: #0 Call foo - S867 x < (offs + users) (conj_$5{unsigned int, LC1, S815, #1}) < ((conj_$5{unsigned int, LC1, S815, #1}) + (conj_$2{unsigned int, LC1, S796, #1})) + S867 x < (offs + users) 0 S32b Ranges: (conj_$5{unsigned int, LC1, S815, #1}) < ((conj_$5{unsigned int, LC1, S815, #1}) + (conj_$2{unsigned int, LC1, S796, #1})) { [0, 0] }

disabling eagerly-assume shows the same problem. 
clang -cc1 -analyze  -analyzer-checker=core  -analyzer-config  eagerly-assume=false test.c

adding a "__builtin_assume(offs==0);" shows the same problem, and 
adding a "__builtin_assume(offs=0);" avoids the problem but shows a new warning ...
test.c:14:20: warning: the argument to '__builtin_assume' has side effects that will be discarded
  __builtin_assume(offs=0);
                   ^~~~~~
warning: Trimmed ExplodedGraph is empty.
Warning: dumping graph requires assertions
1 warning generated.

So for the case of "__builtin_assume(offs=0);", one of two things may be occurring:
1) There really may be a side effect even though the warning says something different.
2) There really is no side effect, but the SA is picking up on the constraint. 

These are contradictory, and I'm not sure which is correct :/

Does any one have knowledge of this particular issue and where to dig further into this? Or maybe I'm just missing something obvious :/ 

Thanks - Vince 

The reproducer … 

unsigned getusers(void);
unsigned getoffs(void);
unsigned foo(void);
unsigned foo(void) {
  unsigned users;
  unsigned offs;
  unsigned x;
  unsigned a[1];
  users = getusers();
  offs = getoffs();
  for (x = offs; x < (offs+users); x++) {
    a[(x + offs)] = 0;
  }
  // SA warns 'warning: Undefined or garbage value returned to caller'
  return a[0];
}


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev