[PATCH] D125931: [clang][dataflow] Add support for correlated branches to optional model

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp:596-598
+      MergedEnv.makeOr(
+          MergedEnv.makeAnd(Env1.getFlowConditionToken(), *HasValueVal1),
+          MergedEnv.makeAnd(Env2.getFlowConditionToken(), *HasValueVal2)));
----------------
ymandel wrote:
> What's the plan for loops? This will increase the size of the constraint on every iteration, preventing termination.
I have nothing to add, just a brain dump. In this particular case, the analysis domain has infinite chains, the size of the Boolean formulas can increase indefinitely (at least syntactically). The canonical solution to deal with infinite chains is to do a widening operation such that the widened state over approximates both the state of the old and the new iteration. A very simple way of doing this would be to simply erase all knowledge we accumulated about the Boolean value. On the other hand, I wonder if it is often possible to do something smarter. There might be cases when the value is syntactically larger in the new iteration but actually it has the exact same truth table. The solver might be able to show this. On the other hand, if the loop generates new Boolean symbols in each iteration, we have little hope fore that.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125931/new/

https://reviews.llvm.org/D125931