Skip to content

Commit 33f753d

Browse files
ymandymand
committed
[clang][dataflow] Factor out built-in boolean model into an explicit module.
In the process, drastically simplify the handling of terminators.
1 parent 7340263 commit 33f753d

File tree

2 files changed

+124
-44
lines changed

2 files changed

+124
-44
lines changed

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,30 @@ class StmtToEnvMap {
4848
const TypeErasedDataflowAnalysisState &CurState;
4949
};
5050

51+
namespace bool_model {
52+
53+
BoolValue &freshBoolValue(Environment &Env);
54+
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 bool_model
74+
5175
/// Evaluates `S` and updates `Env` accordingly.
5276
///
5377
/// Requirements:

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

Lines changed: 100 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -50,21 +50,6 @@ const Environment *StmtToEnvMap::getEnvironment(const Stmt &S) const {
5050
return &State->Env;
5151
}
5252

53-
static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
54-
Environment &Env) {
55-
Value *LHSValue = Env.getValue(LHS);
56-
Value *RHSValue = Env.getValue(RHS);
57-
58-
if (LHSValue == RHSValue)
59-
return Env.getBoolLiteralValue(true);
60-
61-
if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
62-
if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
63-
return Env.makeIff(*LHSBool, *RHSBool);
64-
65-
return Env.makeAtomicBoolValue();
66-
}
67-
6853
static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
6954
if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
7055
auto &A = Env.getDataflowAnalysisContext().arena();
@@ -73,6 +58,68 @@ static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
7358
return V;
7459
}
7560

61+
static void propagateValue(const Expr &From, const Expr &To, Environment &Env) {
62+
if (auto *Val = Env.getValue(From))
63+
Env.setValue(To, *Val);
64+
}
65+
66+
static void propagateStorageLocation(const Expr &From, const Expr &To,
67+
Environment &Env) {
68+
if (auto *Loc = Env.getStorageLocation(From))
69+
Env.setStorageLocation(To, *Loc);
70+
}
71+
72+
// Propagates the value or storage location of `From` to `To` in cases where
73+
// `From` may be either a glvalue or a prvalue. `To` must be a glvalue iff
74+
// `From` is a glvalue.
75+
static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
76+
Environment &Env) {
77+
assert(From.isGLValue() == To.isGLValue());
78+
if (From.isGLValue())
79+
propagateStorageLocation(From, To, Env);
80+
else
81+
propagateValue(From, To, Env);
82+
}
83+
84+
namespace bool_model {
85+
86+
BoolValue &freshBoolValue(Environment &Env) {
87+
return Env.makeAtomicBoolValue();
88+
}
89+
90+
BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
91+
return unpackValue(V, Env);
92+
}
93+
94+
BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
95+
return Env.makeOr(LHS, RHS);
96+
}
97+
98+
BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
99+
return Env.makeAnd(LHS, RHS);
100+
}
101+
102+
BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
103+
return Env.makeIff(LHS, RHS);
104+
}
105+
106+
BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
107+
return Env.makeNot(Env.makeIff(LHS, RHS));
108+
}
109+
110+
BoolValue &notOp(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
111+
112+
void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
113+
if (BranchVal)
114+
Env.assume(CondVal.formula());
115+
else
116+
// The condition must be inverted for the successor that encompasses the
117+
// "else" branch, if such exists.
118+
Env.assume(Env.makeNot(CondVal).formula());
119+
}
120+
121+
} // namespace bool_model
122+
76123
// Unpacks the value (if any) associated with `E` and updates `E` to the new
77124
// value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,
78125
// by skipping past the reference.
@@ -86,34 +133,45 @@ static Value *maybeUnpackLValueExpr(const Expr &E, Environment &Env) {
86133
if (B == nullptr)
87134
return Val;
88135

89-
auto &UnpackedVal = unpackValue(*B, Env);
136+
auto &UnpackedVal = bool_model::rValueFromLValue(*B, Env);
90137
if (&UnpackedVal == Val)
91138
return Val;
92139
Env.setValue(*Loc, UnpackedVal);
93140
return &UnpackedVal;
94141
}
95142

96-
static void propagateValue(const Expr &From, const Expr &To, Environment &Env) {
97-
if (auto *Val = Env.getValue(From))
98-
Env.setValue(To, *Val);
143+
static BoolValue &evaluateEquality(const Expr &LHS, const Expr &RHS,
144+
Environment &Env) {
145+
Value *LHSValue = Env.getValue(LHS);
146+
Value *RHSValue = Env.getValue(RHS);
147+
148+
// Bug!
149+
if (LHSValue == RHSValue)
150+
return Env.getBoolLiteralValue(true);
151+
152+
if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
153+
if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
154+
return bool_model::eqOp(*LHSBool, *RHSBool, Env);
155+
156+
// TODO Why this eager construcoitn of an atomic?
157+
return Env.makeAtomicBoolValue();
99158
}
100159

101-
static void propagateStorageLocation(const Expr &From, const Expr &To,
160+
static BoolValue &evaluateInequality(const Expr &LHS, const Expr &RHS,
102161
Environment &Env) {
103-
if (auto *Loc = Env.getStorageLocation(From))
104-
Env.setStorageLocation(To, *Loc);
105-
}
162+
Value *LHSValue = Env.getValue(LHS);
163+
Value *RHSValue = Env.getValue(RHS);
106164

107-
// Propagates the value or storage location of `From` to `To` in cases where
108-
// `From` may be either a glvalue or a prvalue. `To` must be a glvalue iff
109-
// `From` is a glvalue.
110-
static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
111-
Environment &Env) {
112-
assert(From.isGLValue() == To.isGLValue());
113-
if (From.isGLValue())
114-
propagateStorageLocation(From, To, Env);
115-
else
116-
propagateValue(From, To, Env);
165+
// Bug!
166+
if (LHSValue == RHSValue)
167+
return Env.getBoolLiteralValue(false);
168+
169+
if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
170+
if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
171+
return bool_model::neOp(*LHSBool, *RHSBool, Env);
172+
173+
// TODO Why this eager construcoitn of an atomic?
174+
return Env.makeAtomicBoolValue();
117175
}
118176

119177
namespace {
@@ -153,22 +211,20 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
153211
BoolValue &RHSVal = getLogicOperatorSubExprValue(*RHS);
154212

155213
if (S->getOpcode() == BO_LAnd)
156-
Env.setValue(*S, Env.makeAnd(LHSVal, RHSVal));
214+
Env.setValue(*S, bool_model::logicalAndOp(LHSVal, RHSVal, Env));
157215
else
158-
Env.setValue(*S, Env.makeOr(LHSVal, RHSVal));
216+
Env.setValue(*S, bool_model::logicalOrOp(LHSVal, RHSVal, Env));
159217
break;
160218
}
161219
case BO_NE:
162-
case BO_EQ: {
163-
auto &LHSEqRHSValue = evaluateBooleanEquality(*LHS, *RHS, Env);
164-
Env.setValue(*S, S->getOpcode() == BO_EQ ? LHSEqRHSValue
165-
: Env.makeNot(LHSEqRHSValue));
220+
Env.setValue(*S, evaluateInequality(*LHS, *RHS, Env));
166221
break;
167-
}
168-
case BO_Comma: {
222+
case BO_EQ:
223+
Env.setValue(*S, evaluateEquality(*LHS, *RHS, Env));
224+
break;
225+
case BO_Comma:
169226
propagateValueOrStorageLocation(*RHS, *S, Env);
170227
break;
171-
}
172228
default:
173229
break;
174230
}
@@ -273,7 +329,7 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
273329
else
274330
// FIXME: If integer modeling is added, then update this code to create
275331
// the boolean based on the integer model.
276-
Env.setValue(*S, Env.makeAtomicBoolValue());
332+
Env.setValue(*S, bool_model::freshBoolValue(Env));
277333
break;
278334
}
279335

@@ -362,7 +418,7 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
362418
if (SubExprVal == nullptr)
363419
break;
364420

365-
Env.setValue(*S, Env.makeNot(*SubExprVal));
421+
Env.setValue(*S, bool_model::notOp(*SubExprVal, Env));
366422
break;
367423
}
368424
default:

0 commit comments

Comments
 (0)