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

[Vince Bridgers 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];
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200215/4f80f380/attachment.html>