martong added inline comments.
================
Comment at:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:390-396
/// Try to simplify a given symbolic expression's associated value based on the
/// constraints in State. This is needed because the Environment bindings are
/// not getting updated when a new constraint is added to the State.
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+/// If the symbol is simplified to a constant then it returns the original
+/// symbol.
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
----------------
steakhal wrote:
> I'm confused about which comment corresponds to which function.
> You should also signify the difference between the two APIs.
>
> Shouldn't be one of them an implementation detail? If so, why do we have the
> same visibility?
> Shouldn't be one of them an implementation detail? If so, why do we have the
> same visibility?
No, we use both of them. `simplify` that always returns a symbol is used e.g.
in `RangedConstraintManager::assumeSym`.
And we use `simplifyToSVal` directly in `EquivalenceClass::simplify`.
================
Comment at: clang/test/Analysis/solver-sym-simplification-concreteint.c:22
+ // c == 0 --> 0 + 1 == 0 contradiction
+ clang_analyzer_eval(c == 0); // expected-warning{{FALSE}}
+
----------------
steakhal wrote:
> Could we have an `eval(c == -1) // TRUE`?
> Also, please disable eager bifurcation to prevent state-splits in the eval
> arguments.
Actually, it is `eval(c == -1) // FALSE` that holds.
This is because after the simplification with `b==1` we have a constraint
`c+1==0` but we do not reorder this equality to `c==-1`. Besides we have
another constraint that we inherited from a previous State, this is `c: [0,
1]`. Now, when you query `c==-1` then the latter constraint is found, thus
resulting in an infeasible state, so you'll receive `FALSE` in the warning.
Actually, these are the constraints after line 19:
```
"constraints": [
{ "symbol": "(reg_$1<int c>) + (reg_$0<int b>)", "range": "{ [0, 0] }" },
{ "symbol": "(reg_$1<int c>) + 1", "range": "{ [0, 0] }" },
{ "symbol": "reg_$0<int b>", "range": "{ [1, 1] }" },
{ "symbol": "reg_$1<int c>", "range": "{ [0, 1] }" }
],
```
I am considering to create a follow-up patch, where the reordering of `c+1==0`
to `c==-1` is done (perhaps by reusing `RangedConstraintManager::assumeSymRel`).
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D110913/new/
https://reviews.llvm.org/D110913
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
