[prev in list] [next in list] [prev in thread] [next in thread] 

List:       cfe-commits
Subject:    [PATCH] D122838: [clang][dataflow] Add support for correlation of boolean (tracked) values
From:       Gábor_Horváth_via_Phabricator via cfe-commits <cfe-commits
Date:       2022-03-31 20:26:03
Message-ID: sU7bo7RORIaK3LjjwqY-kA () geopod-ismtpd-3-1
[Download RAW message or body]

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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[prev in list] [next in list] [prev in thread] [next in thread]