[PATCH] D45517: [analyzer] False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+  return Solver.check() != Z3_L_FALSE;
+}
----------------
george.karpenkov wrote:
> solver can also return "unknown", what happens then?
If it returns `Z3_L_UNDEF`, e.g. in case of a timeout, this assumes that the state was feasible because we couldn't prove the opposite. In that case the report won't be invalidated.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+    return;
+  ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
----------------
george.karpenkov wrote:
> TBH I'm really confused here. Why does the method take two constraint ranges? What's `OnlyPurged`? From reading the code it seems it's set by seeing whether the program point only purges dead symbols, but at least a comment should be added as to why this affects behavior.
The logic was:
  - add every constraint from the last node (first visited),
  - for other nodes on the path, only add those that disappear in the next step.

So `OnlyPurged` is meant to signal that we only want to add those symbols to the solver that are getting purged from the program state.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1278
+      // a valid APSIntType.
+      if (RangeTy.isNull())
+        continue;
----------------
george.karpenkov wrote:
> I'm really curious where does it happen and why.
I encountered some 1-bit `APSInt`s that wouldn't work together with any other integer-handling logic. As @ddcc mentioned, he has a fix for that in D35450 (`Z3ConstraintManager::fixAPSInt()`).


https://reviews.llvm.org/D45517