Skip to content

Commit 526c9b7

Browse files
martinboehmemartinboehme
authored
[clang][nullability] Use proves() and assume() instead of deprecated synonyms. (#70297)
1 parent da28c33 commit 526c9b7

File tree

8 files changed

+149
-161
lines changed

8 files changed

+149
-161
lines changed

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -114,11 +114,10 @@ class ModelDumper {
114114
// guaranteed true/false here is valuable and hard to determine by hand.
115115
if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
116116
JOS.attribute("formula", llvm::to_string(B->formula()));
117-
JOS.attribute(
118-
"truth", Env.flowConditionImplies(B->formula()) ? "true"
119-
: Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
120-
? "false"
121-
: "unknown");
117+
JOS.attribute("truth", Env.proves(B->formula()) ? "true"
118+
: Env.proves(Env.arena().makeNot(B->formula()))
119+
? "false"
120+
: "unknown");
122121
}
123122
}
124123
void dump(const StorageLocation &L) {

‎clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ bool ChromiumCheckModel::transfer(const CFGElement &Element, Environment &Env) {
5959
if (const auto *M = dyn_cast<CXXMethodDecl>(Call->getDirectCallee())) {
6060
if (isCheckLikeMethod(CheckDecls, *M)) {
6161
// Mark this branch as unreachable.
62-
Env.addToFlowCondition(Env.arena().makeLiteral(false));
62+
Env.assume(Env.arena().makeLiteral(false));
6363
return true;
6464
}
6565
}

‎clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -413,16 +413,15 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
413413
auto *HasValueVal =
414414
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
415415
return HasValueVal != nullptr &&
416-
Env.flowConditionImplies(Env.arena().makeNot(HasValueVal->formula()));
416+
Env.proves(Env.arena().makeNot(HasValueVal->formula()));
417417
}
418418

419419
/// Returns true if and only if `OptionalVal` is initialized and known to be
420420
/// non-empty in `Env`.
421421
bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
422422
auto *HasValueVal =
423423
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
424-
return HasValueVal != nullptr &&
425-
Env.flowConditionImplies(HasValueVal->formula());
424+
return HasValueVal != nullptr && Env.proves(HasValueVal->formula());
426425
}
427426

428427
Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
@@ -490,8 +489,8 @@ void transferValueOrImpl(
490489
if (HasValueVal == nullptr)
491490
return;
492491

493-
Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
494-
HasValueVal->formula()));
492+
Env.assume(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
493+
HasValueVal->formula()));
495494
}
496495

497496
void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr,
@@ -717,8 +716,8 @@ void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
717716
if (auto *RHasVal = getHasValue(Env, Env.getValue(*CmpExpr->getArg(1)))) {
718717
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
719718
CmpValue = &A.makeNot(*CmpValue);
720-
Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(),
721-
RHasVal->formula()));
719+
Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(),
720+
RHasVal->formula()));
722721
}
723722
}
724723

@@ -729,7 +728,7 @@ void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
729728
if (auto *HasVal = getHasValue(Env, Env.getValue(*E))) {
730729
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
731730
CmpValue = &A.makeNot(*CmpValue);
732-
Env.addToFlowCondition(
731+
Env.assume(
733732
evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
734733
}
735734
}
@@ -917,7 +916,7 @@ llvm::SmallVector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
917916
if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
918917
auto *Prop = OptionalVal->getProperty("has_value");
919918
if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
920-
if (Env.flowConditionImplies(HasValueVal->formula()))
919+
if (Env.proves(HasValueVal->formula()))
921920
return {};
922921
}
923922
}
@@ -1004,14 +1003,13 @@ bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
10041003
bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
10051004
bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
10061005
if (MustNonEmpty1 && MustNonEmpty2)
1007-
MergedEnv.addToFlowCondition(HasValueVal.formula());
1006+
MergedEnv.assume(HasValueVal.formula());
10081007
else if (
10091008
// Only make the costly calls to `isEmptyOptional` if we got "unknown"
10101009
// (false) for both calls to `isNonEmptyOptional`.
10111010
!MustNonEmpty1 && !MustNonEmpty2 && isEmptyOptional(Val1, Env1) &&
10121011
isEmptyOptional(Val2, Env2))
1013-
MergedEnv.addToFlowCondition(
1014-
MergedEnv.arena().makeNot(HasValueVal.formula()));
1012+
MergedEnv.assume(MergedEnv.arena().makeNot(HasValueVal.formula()));
10151013
setHasValue(MergedVal, HasValueVal);
10161014
return true;
10171015
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ class TerminatorVisitor
148148
ConditionValue = false;
149149
}
150150

151-
Env.addToFlowCondition(Val->formula());
151+
Env.assume(Val->formula());
152152
return {&Cond, ConditionValue};
153153
}
154154

‎clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ TEST(ChromiumCheckModelTest, CheckSuccessImpliesConditionHolds) {
159159

160160
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
161161

162-
EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula()));
162+
EXPECT_TRUE(Env.proves(FooVal->formula()));
163163
};
164164

165165
std::string Code = R"(
@@ -190,7 +190,7 @@ TEST(ChromiumCheckModelTest, UnrelatedCheckIgnored) {
190190

191191
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
192192

193-
EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula()));
193+
EXPECT_FALSE(Env.proves(FooVal->formula()));
194194
};
195195

196196
std::string Code = R"(

‎clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp

Lines changed: 22 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -157,44 +157,44 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
157157
switch (BO->getOpcode()) {
158158
case BO_GT:
159159
// pos > pos
160-
State.Env.addToFlowCondition(
160+
State.Env.assume(
161161
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
162162
LHSProps.Pos->formula())));
163163
// pos > zero
164-
State.Env.addToFlowCondition(
164+
State.Env.assume(
165165
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
166166
LHSProps.Pos->formula())));
167167
break;
168168
case BO_LT:
169169
// neg < neg
170-
State.Env.addToFlowCondition(
170+
State.Env.assume(
171171
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
172172
LHSProps.Neg->formula())));
173173
// neg < zero
174-
State.Env.addToFlowCondition(
174+
State.Env.assume(
175175
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
176176
LHSProps.Neg->formula())));
177177
break;
178178
case BO_GE:
179179
// pos >= pos
180-
State.Env.addToFlowCondition(
180+
State.Env.assume(
181181
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
182182
LHSProps.Pos->formula())));
183183
break;
184184
case BO_LE:
185185
// neg <= neg
186-
State.Env.addToFlowCondition(
186+
State.Env.assume(
187187
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
188188
LHSProps.Neg->formula())));
189189
break;
190190
case BO_EQ:
191-
State.Env.addToFlowCondition(
191+
State.Env.assume(
192192
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
193193
LHSProps.Neg->formula())));
194-
State.Env.addToFlowCondition(
194+
State.Env.assume(
195195
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
196196
LHSProps.Zero->formula())));
197-
State.Env.addToFlowCondition(
197+
State.Env.assume(
198198
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
199199
LHSProps.Pos->formula())));
200200
break;
@@ -215,14 +215,14 @@ void transferUnaryMinus(const UnaryOperator *UO,
215215
return;
216216

217217
// a is pos ==> -a is neg
218-
State.Env.addToFlowCondition(
218+
State.Env.assume(
219219
A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula()));
220220
// a is neg ==> -a is pos
221-
State.Env.addToFlowCondition(
221+
State.Env.assume(
222222
A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula()));
223223
// a is zero ==> -a is zero
224-
State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(),
225-
UnaryOpProps.Zero->formula()));
224+
State.Env.assume(A.makeImplies(OperandProps.Zero->formula(),
225+
UnaryOpProps.Zero->formula()));
226226
}
227227

228228
void transferUnaryNot(const UnaryOperator *UO,
@@ -235,19 +235,19 @@ void transferUnaryNot(const UnaryOperator *UO,
235235
return;
236236

237237
// a is neg or pos ==> !a is zero
238-
State.Env.addToFlowCondition(A.makeImplies(
238+
State.Env.assume(A.makeImplies(
239239
A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()),
240240
UnaryOpProps.Zero->formula()));
241241

242242
// FIXME Handle this logic universally, not just for unary not. But Where to
243243
// put the generic handler, transferExpr maybe?
244244
if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) {
245245
// !a <==> a is zero
246-
State.Env.addToFlowCondition(
246+
State.Env.assume(
247247
A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula()));
248248
// !a <==> !a is not zero
249-
State.Env.addToFlowCondition(A.makeEquals(
250-
UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula())));
249+
State.Env.assume(A.makeEquals(UOBoolVal->formula(),
250+
A.makeNot(UnaryOpProps.Zero->formula())));
251251
}
252252
}
253253

@@ -391,11 +391,10 @@ BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
391391
// path taken - this simplifies the flow condition tracked in `MergedEnv`.
392392
// Otherwise, information about which path was taken is used to associate
393393
// `MergedBool` with `Bool1` and `Bool2`.
394-
if (Env1.flowConditionImplies(B1) && Env2.flowConditionImplies(B2)) {
395-
MergedEnv.addToFlowCondition(MergedBool.formula());
396-
} else if (Env1.flowConditionImplies(A.makeNot(B1)) &&
397-
Env2.flowConditionImplies(A.makeNot(B2))) {
398-
MergedEnv.addToFlowCondition(A.makeNot(MergedBool.formula()));
394+
if (Env1.proves(B1) && Env2.proves(B2)) {
395+
MergedEnv.assume(MergedBool.formula());
396+
} else if (Env1.proves(A.makeNot(B1)) && Env2.proves(A.makeNot(B2))) {
397+
MergedEnv.assume(A.makeNot(MergedBool.formula()));
399398
}
400399
return MergedBool;
401400
}
@@ -484,7 +483,7 @@ testing::AssertionResult isPropertyImplied(const Environment &Env,
484483
if (!Prop)
485484
return Result;
486485
auto *BVProp = cast<BoolValue>(Prop);
487-
if (Env.flowConditionImplies(BVProp->formula()) != Implies)
486+
if (Env.proves(BVProp->formula()) != Implies)
488487
return testing::AssertionFailure()
489488
<< Property << " is " << (Implies ? "not" : "") << " implied"
490489
<< ", but should " << (Implies ? "" : "not ") << "be";

0 commit comments

Comments
 (0)