[clang] [StaticAnalyzer] early return if sym is concrete on assuming (PR #115579)

Ding Fei via cfe-commits cfe-commits at lists.llvm.org
Mon Nov 11 08:34:55 PST 2024


================
@@ -23,7 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
 ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
                                                    SymbolRef Sym,
                                                    bool Assumption) {
-  Sym = simplify(State, Sym);
+  SVal SimplifiedVal = simplifyToSVal(State, Sym);
+  if (SimplifiedVal.isConstant()) {
+    bool Feasible = SimplifiedVal.isZeroConstant() ? !Assumption : Assumption;
----------------
danix800 wrote:

Maybe `Assumption ? !SimplifiedVal.isZeroConstant() : SimplifiedVal.isZeroConstant()` is more clear, which reads more naturally like:

```c
if (SimplifiedVal) {
  // ...
}
```

being translated into

```c
if (Assumption) // you want SimplifiedVal to be true?
   Feasible = !SimplifiedVal.isZeroConstant(); // ok, then it SHOULD NOT be zero
else
   Feasible = SimplifiedVal.isZeroConstant(); // no, then it SHOULD be zero
```

Honestly I made a truth table to aid in understanding the equivalence of all these forms:

|Assume|isZero|isZero != Assume|Assume ? !isZero : isZero | isZero ? !Assume : Assume |
|---|---|---|---|---|
|T|T|F|F|F|
|T|F|T|T|T|
|F|T|T|T|T|
|F|F|F|F|F|

And YES! they are equivalent!

But I'll choose the shortest one as you suggested! Thanks!

https://github.com/llvm/llvm-project/pull/115579


More information about the cfe-commits mailing list