Skip to content

Commit ff9537d

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 ff9537d

File tree

6 files changed

+184
-220
lines changed

6 files changed

+184
-220
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: 169 additions & 30 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,169 @@
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); Right == false)
55+
return Right;
56+
return std::nullopt;
57+
}
58+
case Formula::Or: {
59+
ArrayRef<const Formula *> Operands = F.operands();
60+
assert(Operands.size() == 2);
61+
auto &LHS = *Operands[0];
62+
auto &RHS = *Operands[1];
63+
if (std::optional<bool> Left = getLiteralValue(LHS, Env))
64+
return *Left ? Left : getLiteralValue(RHS, Env);
65+
if (std::optional<bool> Right = getLiteralValue(RHS, Env); Right == true)
66+
return Right;
67+
return std::nullopt;
68+
}
69+
case Formula::Equal: {
70+
ArrayRef<const Formula *> Operands = F.operands();
71+
assert(Operands.size() == 2);
72+
auto &LHS = *Operands[0];
73+
auto &RHS = *Operands[1];
74+
if (&LHS == &RHS)
75+
return true;
76+
auto V_L = getLiteralValue(LHS, Env);
77+
return V_L.has_value() && V_L == getLiteralValue(RHS, Env);
78+
}
79+
default:
80+
return std::nullopt;
81+
}
82+
}
83+
84+
// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
85+
// value to use for atoms encountered in the formula.
86+
static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
87+
switch (F.kind()) {
88+
case Formula::AtomRef:
89+
// FIXME: if the atom is set to a different value, mark the block as
90+
// unreachable.
91+
Env.setAtomValue(F.getAtom(), AtomVal);
92+
break;
93+
case Formula::Literal:
94+
// FIXME: if the literal is `false`, mark the block as unreachable.
95+
break;
96+
case Formula::Not: {
97+
ArrayRef<const Formula *> Operands = F.operands();
98+
assert(Operands.size() == 1);
99+
assumeFormula(!AtomVal, *Operands[0], Env);
100+
break;
101+
}
102+
case Formula::And: {
103+
if (AtomVal == true) {
104+
ArrayRef<const Formula *> Operands = F.operands();
105+
assert(Operands.size() == 2);
106+
assumeFormula(true, *Operands[0], Env);
107+
assumeFormula(true, *Operands[1], Env);
108+
}
109+
break;
110+
}
111+
case Formula::Or: {
112+
if (AtomVal == false) {
113+
// Interpret the negated "or" as "and" of negated operands.
114+
ArrayRef<const Formula *> Operands = F.operands();
115+
assert(Operands.size() == 2);
116+
assumeFormula(false, *Operands[0], Env);
117+
assumeFormula(false, *Operands[1], Env);
118+
}
119+
break;
120+
}
121+
case Formula::Equal: {
122+
ArrayRef<const Formula *> Operands = F.operands();
123+
assert(Operands.size() == 2);
124+
auto &LHS = *Operands[0];
125+
auto &RHS = *Operands[1];
126+
if (auto V = getLiteralValue(LHS, Env)) {
127+
assumeFormula(AtomVal == *V, RHS, Env);
128+
} else if (auto V = getLiteralValue(RHS, Env)) {
129+
assumeFormula(AtomVal == *V, LHS, Env);
130+
}
131+
break;
132+
}
133+
default:
134+
break;
135+
}
136+
}
137+
138+
BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
139+
const Environment &Env2, Environment &JoinedEnv) {
140+
if (auto V1 = getLiteralValue(Val1.formula(), Env1);
141+
V1.has_value() && V1 == getLiteralValue(Val2.formula(), Env2))
142+
return JoinedEnv.getBoolLiteralValue(*V1);
143+
return JoinedEnv.makeAtomicBoolValue();
144+
}
145+
146+
void assume(Environment &Env, const Formula &F) {
147+
assumeFormula(/*AtomVal*/ true, F, Env);
148+
}
149+
150+
bool allows(const Environment &Env, const Formula &F) {
151+
auto V = getLiteralValue(F, Env);
152+
// We are conservative in the negative direction: if we can't determine the
153+
// value, assume it is allowed.
154+
return V.value_or(true);
155+
}
156+
157+
bool proves(const Environment &Env, const Formula &F) {
158+
auto V = getLiteralValue(F, Env);
159+
return V.value_or(false);
160+
}
161+
} // namespace simple_bool_model
162+
163+
namespace sat_bool_model {
164+
BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
165+
const Environment &Env2, Environment &JoinedEnv) {
166+
auto &A = JoinedEnv.arena();
167+
auto &JoinedVal = JoinedEnv.makeAtomicBoolValue();
168+
auto &JoinedFormula = JoinedVal.formula();
169+
JoinedEnv.assume(
170+
A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
171+
A.makeEquals(JoinedFormula, Val1.formula())),
172+
A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
173+
A.makeEquals(JoinedFormula, Val2.formula()))));
174+
return JoinedVal;
175+
}
176+
177+
void assume(Environment &Env, const Formula &F) {
178+
Env.getDataflowAnalysisContext().addFlowConditionConstraint(
179+
Env.getFlowConditionToken(), F);
180+
}
181+
182+
bool allows(const Environment &Env, const Formula &F) {
183+
return Env.getDataflowAnalysisContext().flowConditionAllows(
184+
Env.getFlowConditionToken(), F);
185+
}
186+
187+
bool proves(const Environment &Env, const Formula &F) {
188+
return Env.getDataflowAnalysisContext().flowConditionImplies(
189+
Env.getFlowConditionToken(), F);
190+
}
191+
} // namespace sat_bool_model
192+
193+
namespace bool_model = simple_bool_model;
194+
33195
// FIXME: convert these to parameters of the analysis or environment. Current
34196
// settings have been experimentaly validated, but only for a particular
35197
// analysis.
@@ -130,23 +292,9 @@ static Value *joinDistinctValues(QualType Type, Value &Val1,
130292
// if (o.has_value())
131293
// x = o.value();
132294
// ```
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);
295+
auto &B1 = cast<BoolValue>(Val1);
296+
auto &B2 = cast<BoolValue>(Val2);
297+
return &bool_model::join(B1, Env1, B2, Env2, JoinedEnv);
150298
}
151299

152300
Value *JoinedVal = nullptr;
@@ -1070,23 +1218,14 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
10701218
return Loc;
10711219
}
10721220

1073-
void Environment::assume(const Formula &F) {
1074-
DACtx->addFlowConditionConstraint(FlowConditionToken, F);
1075-
}
1221+
void Environment::assume(const Formula &F) { bool_model::assume(*this, F); }
10761222

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

10881227
bool Environment::allows(const Formula &F) const {
1089-
return DACtx->flowConditionAllows(FlowConditionToken, F);
1228+
return bool_model::allows(*this, F);
10901229
}
10911230

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

0 commit comments

Comments
 (0)