[PATCH] D122838: [clang][dataflow] Add support for correlation of boolean (tracked) values

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

xazax.hun added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp:79
+    for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
+      Expr1 = &Env1.makeAnd(*Expr1, *Constraint);
+    }
----------------
Hmm, interesting.
I think we view every boolean formula at a certain program point implicitly as `FlowConditionAtThatPoint && Formula`. And the flow condition at a program point should already be a disjunction of its predecessors.

So it would be interpreted as: `(FlowConditionPred1 || FlowConditionPred2) && (FormulaAtPred1 || FormulaAtPred2)`.
While this is great, this is not the strongest condition we could derive. 
`(FlowConditionPred1 && FormulaAtPred1)  || (FormulaAtPred2 && FlowConditionPred2)` created by this code snippet is stronger which is great.

My main concern is whether we would end up seeing an exponential explosion in the size of these formulas in the number of branches following each other in a sequence.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D122838