Skip to content

Commit 486686c

Browse files
ymandymand
committed
[clang][dataflow] Abstract the logical operations (assume, allows, proves) and drop distinction between boolean operations.
This commit drastically simplifies the original refactoring. We keep the boolean model separately, but we only maintain one version, since there turned out to be no meaningful difference between them. Instead, the difference lies in the logical operations, so we've abstacted those. We're down to 35 failing tests, all with clear explanations based on the limitations of this approach; primarily, the inability to encode custom API/operator meanings using logical formulae.
1 parent ed9bb21 commit 486686c

File tree

6 files changed

+189
-218
lines changed

6 files changed

+189
-218
lines changed

‎clang/include/clang/Analysis/FlowSensitive/Transfer.h

Lines changed: 2 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -48,57 +48,11 @@ class StmtToEnvMap {
4848
const TypeErasedDataflowAnalysisState &CurState;
4949
};
5050

51-
namespace sat_bool_model {
51+
namespace bool_model {
5252

5353
BoolValue &freshBoolValue(Environment &Env);
5454

55-
BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
56-
57-
BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
58-
59-
BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
60-
61-
BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
62-
63-
BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
64-
65-
BoolValue &notOp(BoolValue &Sub, Environment &Env);
66-
67-
// Models the transition along a branch edge in the CFG.
68-
// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
69-
// for `else`.
70-
// CondVal -- the abstract value representing the condition.
71-
void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
72-
73-
} // namespace sat_bool_model
74-
75-
namespace simple_bool_model {
76-
77-
std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env);
78-
79-
BoolValue &freshBoolValue(Environment &Env);
80-
81-
BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
82-
83-
BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
84-
85-
BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
86-
87-
BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
88-
89-
BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
90-
91-
BoolValue &notOp(BoolValue &Sub, Environment &Env);
92-
93-
// Models the transition along a branch edge in the CFG.
94-
// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
95-
// for `else`.
96-
// CondVal -- the abstract value representing the condition.
97-
void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
98-
99-
} // namespace simple_bool_model
100-
101-
namespace bool_model = simple_bool_model;
55+
} // namespace bool_model
10256

10357
/// Evaluates `S` and updates `Env` accordingly.
10458
///

‎clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

Lines changed: 174 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@
1717
#include "clang/AST/DeclCXX.h"
1818
#include "clang/AST/Type.h"
1919
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
20-
#include "clang/Analysis/FlowSensitive/Transfer.h"
2120
#include "clang/Analysis/FlowSensitive/Value.h"
2221
#include "llvm/ADT/DenseMap.h"
2322
#include "llvm/ADT/DenseSet.h"
@@ -30,6 +29,174 @@
3029
namespace clang {
3130
namespace dataflow {
3231

32+
namespace simple_bool_model {
33+
static std::optional<bool> getLiteralValue(const Formula &F,
34+
const Environment &Env) {
35+
switch (F.kind()) {
36+
case Formula::AtomRef:
37+
return Env.getAtomValue(F.getAtom());
38+
case Formula::Literal:
39+
return F.literal();
40+
case Formula::Not: {
41+
ArrayRef<const Formula *> Operands = F.operands();
42+
assert(Operands.size() == 1);
43+
if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
44+
return !*Maybe;
45+
return std::nullopt;
46+
}
47+
case Formula::And: {
48+
ArrayRef<const Formula *> Operands = F.operands();
49+
assert(Operands.size() == 2);
50+
auto &LHS = *Operands[0];
51+
auto &RHS = *Operands[1];
52+
if (std::optional<bool> Left = getLiteralValue(LHS, Env))
53+
return !*Left ? Left : getLiteralValue(RHS, Env);
54+
if (std::optional<bool> Right = getLiteralValue(RHS, Env);
55+
Right.has_value() && !*Right)
56+
return Right;
57+
return std::nullopt;
58+
}
59+
case Formula::Or: {
60+
ArrayRef<const Formula *> Operands = F.operands();
61+
assert(Operands.size() == 2);
62+
auto &LHS = *Operands[0];
63+
auto &RHS = *Operands[1];
64+
if (std::optional<bool> Left = getLiteralValue(LHS, Env))
65+
return *Left ? Left : getLiteralValue(RHS, Env);
66+
if (std::optional<bool> Right = getLiteralValue(RHS, Env);
67+
Right.has_value() && *Right)
68+
return Right;
69+
return std::nullopt;
70+
}
71+
case Formula::Equal: {
72+
ArrayRef<const Formula *> Operands = F.operands();
73+
assert(Operands.size() == 2);
74+
auto &LHS = *Operands[0];
75+
auto &RHS = *Operands[1];
76+
if (&LHS == &RHS) return true;
77+
auto V_L = getLiteralValue(LHS, Env);
78+
auto V_R = getLiteralValue(RHS, Env);
79+
return V_L.has_value() && V_R.has_value() && (*V_L == *V_R);
80+
}
81+
default:
82+
return std::nullopt;
83+
}
84+
}
85+
86+
// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
87+
// value to use for atoms encountered in the formula.
88+
static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
89+
// TODO: handle literals directly rather than calling getLiteralValue.
90+
std::optional<bool> Lit = getLiteralValue(F, Env);
91+
if (Lit.has_value())
92+
// FIXME: Nothing to do. Could verify no contradiction, but not sure what
93+
// we'd do with that here. Need to poison the Env.
94+
return;
95+
96+
switch (F.kind()) {
97+
case Formula::AtomRef:
98+
// FIXME: check for contradictions
99+
Env.setAtomValue(F.getAtom(), AtomVal);
100+
break;
101+
case Formula::Not: {
102+
ArrayRef<const Formula *> Operands = F.operands();
103+
assert(Operands.size() == 1);
104+
assumeFormula(!AtomVal, *Operands[0], Env);
105+
break;
106+
}
107+
case Formula::And: {
108+
if (AtomVal == true) {
109+
ArrayRef<const Formula *> Operands = F.operands();
110+
assert(Operands.size() == 2);
111+
assumeFormula(true, *Operands[0], Env);
112+
assumeFormula(true, *Operands[1], Env);
113+
}
114+
break;
115+
}
116+
case Formula::Or: {
117+
if (AtomVal == false) {
118+
// Interpret the negated "or" as "and" of negated operands.
119+
ArrayRef<const Formula *> Operands = F.operands();
120+
assert(Operands.size() == 2);
121+
assumeFormula(false, *Operands[0], Env);
122+
assumeFormula(false, *Operands[1], Env);
123+
}
124+
break;
125+
}
126+
case Formula::Equal: {
127+
ArrayRef<const Formula *> Operands = F.operands();
128+
assert(Operands.size() == 2);
129+
auto &LHS = *Operands[0];
130+
auto &RHS = *Operands[1];
131+
if (auto V = getLiteralValue(LHS, Env)) {
132+
assumeFormula(AtomVal == *V, RHS, Env);
133+
} else if (auto V = getLiteralValue(RHS, Env)) {
134+
assumeFormula(AtomVal == *V, LHS, Env);
135+
}
136+
break;
137+
}
138+
default:
139+
break;
140+
}
141+
}
142+
143+
BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
144+
const Environment &Env2, Environment &JoinedEnv) {
145+
if (auto V1 = getLiteralValue(Val1.formula(), Env1);
146+
V1.has_value() && V1 == getLiteralValue(Val2.formula(), Env2))
147+
return JoinedEnv.getBoolLiteralValue(*V1);
148+
return JoinedEnv.makeAtomicBoolValue();
149+
}
150+
151+
void assume(Environment &Env, const Formula &F) {
152+
assumeFormula(/*AtomVal*/true, F, Env);
153+
}
154+
155+
bool allows(const Environment &Env, const Formula &F) {
156+
auto V = getLiteralValue(F, Env);
157+
// We are conservative in the negative direction: if we can't determine the
158+
// value, assume its allowed.
159+
return !V.has_value() || *V;
160+
}
161+
162+
bool proves(const Environment &Env, const Formula &F) {
163+
auto V = getLiteralValue(F, Env);
164+
return V.has_value() && *V;
165+
}
166+
} // namespace simple_bool_model
167+
168+
namespace sat_bool_model {
169+
BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
170+
const Environment &Env2, Environment &JoinedEnv) {
171+
auto &A = JoinedEnv.arena();
172+
auto &JoinedVal = JoinedEnv.makeAtomicBoolValue();
173+
auto &JoinedFormula = JoinedVal.formula();
174+
JoinedEnv.assume(
175+
A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
176+
A.makeEquals(JoinedFormula, Val1.formula())),
177+
A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
178+
A.makeEquals(JoinedFormula, Val2.formula()))));
179+
return JoinedVal;
180+
}
181+
182+
void assume(Environment &Env, const Formula &F) {
183+
Env.getDataflowAnalysisContext().addFlowConditionConstraint(
184+
Env.getFlowConditionToken(), F);
185+
}
186+
187+
bool allows(const Environment &Env, const Formula &F) {
188+
return Env.getDataflowAnalysisContext().flowConditionAllows(
189+
Env.getFlowConditionToken(), F);
190+
}
191+
192+
bool proves(const Environment &Env, const Formula &F) {
193+
return Env.getDataflowAnalysisContext().flowConditionImplies(
194+
Env.getFlowConditionToken(), F);
195+
}
196+
} // namespace sat_bool_model
197+
198+
namespace bool_model = simple_bool_model;
199+
33200
// FIXME: convert these to parameters of the analysis or environment. Current
34201
// settings have been experimentaly validated, but only for a particular
35202
// analysis.
@@ -130,23 +297,9 @@ static Value *joinDistinctValues(QualType Type, Value &Val1,
130297
// if (o.has_value())
131298
// x = o.value();
132299
// ```
133-
auto &Expr1 = cast<BoolValue>(Val1).formula();
134-
auto &Expr2 = cast<BoolValue>(Val2).formula();
135-
auto &A = JoinedEnv.arena();
136-
137-
#if 1
138-
if (auto V1 = simple_bool_model::getLiteralValue(Expr1, Env1);
139-
V1.has_value() && V1 == simple_bool_model::getLiteralValue(Expr2, Env2))
140-
return &JoinedEnv.getBoolLiteralValue(*V1);
141-
#endif
142-
143-
auto &JoinedVal = A.makeAtomRef(A.makeAtom());
144-
JoinedEnv.assume(
145-
A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
146-
A.makeEquals(JoinedVal, Expr1)),
147-
A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
148-
A.makeEquals(JoinedVal, Expr2))));
149-
return &A.makeBoolValue(JoinedVal);
300+
auto &B1 = cast<BoolValue>(Val1);
301+
auto &B2 = cast<BoolValue>(Val2);
302+
return &bool_model::join(B1, Env1, B2, Env2, JoinedEnv);
150303
}
151304

152305
Value *JoinedVal = nullptr;
@@ -1071,22 +1224,15 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
10711224
}
10721225

10731226
void Environment::assume(const Formula &F) {
1074-
DACtx->addFlowConditionConstraint(FlowConditionToken, F);
1227+
bool_model::assume(*this, F);
10751228
}
10761229

1077-
#if 0
10781230
bool Environment::proves(const Formula &F) const {
1079-
return DACtx->flowConditionImplies(FlowConditionToken, F);
1080-
}
1081-
#else
1082-
bool Environment::proves(const Formula &F) const {
1083-
auto V = simple_bool_model::getLiteralValue(F, *this);
1084-
return V.has_value() && *V;
1231+
return bool_model::proves(*this, F);
10851232
}
1086-
#endif
10871233

10881234
bool Environment::allows(const Formula &F) const {
1089-
return DACtx->flowConditionAllows(FlowConditionToken, F);
1235+
return bool_model::allows(*this, F);
10901236
}
10911237

10921238
void Environment::dump(raw_ostream &OS) const {

0 commit comments

Comments
 (0)