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

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
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 :confused:

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

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];