[clang] [clang][dataflow] Factor out built-in boolean model into an explicit module. (PR #82950)
Yitzhak Mandelbaum via cfe-commits
cfe-commits at lists.llvm.org
Thu Mar 21 11:00:30 PDT 2024
https://github.com/ymand updated https://github.com/llvm/llvm-project/pull/82950
>From 33f753d99bbb477ad37614d29658e964aa590a80 Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzhakm at google.com>
Date: Fri, 23 Feb 2024 20:15:36 +0000
Subject: [PATCH 1/3] [clang][dataflow] Factor out built-in boolean model into
an explicit module.
In the process, drastically simplify the handling of terminators.
---
.../clang/Analysis/FlowSensitive/Transfer.h | 24 +++
clang/lib/Analysis/FlowSensitive/Transfer.cpp | 144 ++++++++++++------
2 files changed, 124 insertions(+), 44 deletions(-)
diff --git a/clang/include/clang/Analysis/FlowSensitive/Transfer.h b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
index ed148250d8eb29..bc8e9cdb03d703 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Transfer.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
@@ -48,6 +48,30 @@ class StmtToEnvMap {
const TypeErasedDataflowAnalysisState &CurState;
};
+namespace bool_model {
+
+BoolValue &freshBoolValue(Environment &Env);
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue ¬Op(BoolValue &Sub, Environment &Env);
+
+// Models the transition along a branch edge in the CFG.
+// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
+// for `else`.
+// CondVal -- the abstract value representing the condition.
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
+
+} // namespace bool_model
+
/// Evaluates `S` and updates `Env` accordingly.
///
/// Requirements:
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index 960e9688ffb725..6e215daaf3fa19 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -50,21 +50,6 @@ const Environment *StmtToEnvMap::getEnvironment(const Stmt &S) const {
return &State->Env;
}
-static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
- Environment &Env) {
- Value *LHSValue = Env.getValue(LHS);
- Value *RHSValue = Env.getValue(RHS);
-
- if (LHSValue == RHSValue)
- return Env.getBoolLiteralValue(true);
-
- if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
- if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
- return Env.makeIff(*LHSBool, *RHSBool);
-
- return Env.makeAtomicBoolValue();
-}
-
static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
auto &A = Env.getDataflowAnalysisContext().arena();
@@ -73,6 +58,68 @@ static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
return V;
}
+static void propagateValue(const Expr &From, const Expr &To, Environment &Env) {
+ if (auto *Val = Env.getValue(From))
+ Env.setValue(To, *Val);
+}
+
+static void propagateStorageLocation(const Expr &From, const Expr &To,
+ Environment &Env) {
+ if (auto *Loc = Env.getStorageLocation(From))
+ Env.setStorageLocation(To, *Loc);
+}
+
+// Propagates the value or storage location of `From` to `To` in cases where
+// `From` may be either a glvalue or a prvalue. `To` must be a glvalue iff
+// `From` is a glvalue.
+static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
+ Environment &Env) {
+ assert(From.isGLValue() == To.isGLValue());
+ if (From.isGLValue())
+ propagateStorageLocation(From, To, Env);
+ else
+ propagateValue(From, To, Env);
+}
+
+namespace bool_model {
+
+BoolValue &freshBoolValue(Environment &Env) {
+ return Env.makeAtomicBoolValue();
+}
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
+ return unpackValue(V, Env);
+}
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ return Env.makeOr(LHS, RHS);
+}
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ return Env.makeAnd(LHS, RHS);
+}
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ return Env.makeIff(LHS, RHS);
+}
+
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ return Env.makeNot(Env.makeIff(LHS, RHS));
+}
+
+BoolValue ¬Op(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
+
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
+ if (BranchVal)
+ Env.assume(CondVal.formula());
+ else
+ // The condition must be inverted for the successor that encompasses the
+ // "else" branch, if such exists.
+ Env.assume(Env.makeNot(CondVal).formula());
+}
+
+} // namespace bool_model
+
// Unpacks the value (if any) associated with `E` and updates `E` to the new
// value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,
// by skipping past the reference.
@@ -86,34 +133,45 @@ static Value *maybeUnpackLValueExpr(const Expr &E, Environment &Env) {
if (B == nullptr)
return Val;
- auto &UnpackedVal = unpackValue(*B, Env);
+ auto &UnpackedVal = bool_model::rValueFromLValue(*B, Env);
if (&UnpackedVal == Val)
return Val;
Env.setValue(*Loc, UnpackedVal);
return &UnpackedVal;
}
-static void propagateValue(const Expr &From, const Expr &To, Environment &Env) {
- if (auto *Val = Env.getValue(From))
- Env.setValue(To, *Val);
+static BoolValue &evaluateEquality(const Expr &LHS, const Expr &RHS,
+ Environment &Env) {
+ Value *LHSValue = Env.getValue(LHS);
+ Value *RHSValue = Env.getValue(RHS);
+
+ // Bug!
+ if (LHSValue == RHSValue)
+ return Env.getBoolLiteralValue(true);
+
+ if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
+ if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
+ return bool_model::eqOp(*LHSBool, *RHSBool, Env);
+
+ // TODO Why this eager construcoitn of an atomic?
+ return Env.makeAtomicBoolValue();
}
-static void propagateStorageLocation(const Expr &From, const Expr &To,
+static BoolValue &evaluateInequality(const Expr &LHS, const Expr &RHS,
Environment &Env) {
- if (auto *Loc = Env.getStorageLocation(From))
- Env.setStorageLocation(To, *Loc);
-}
+ Value *LHSValue = Env.getValue(LHS);
+ Value *RHSValue = Env.getValue(RHS);
-// Propagates the value or storage location of `From` to `To` in cases where
-// `From` may be either a glvalue or a prvalue. `To` must be a glvalue iff
-// `From` is a glvalue.
-static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
- Environment &Env) {
- assert(From.isGLValue() == To.isGLValue());
- if (From.isGLValue())
- propagateStorageLocation(From, To, Env);
- else
- propagateValue(From, To, Env);
+ // Bug!
+ if (LHSValue == RHSValue)
+ return Env.getBoolLiteralValue(false);
+
+ if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
+ if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
+ return bool_model::neOp(*LHSBool, *RHSBool, Env);
+
+ // TODO Why this eager construcoitn of an atomic?
+ return Env.makeAtomicBoolValue();
}
namespace {
@@ -153,22 +211,20 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
BoolValue &RHSVal = getLogicOperatorSubExprValue(*RHS);
if (S->getOpcode() == BO_LAnd)
- Env.setValue(*S, Env.makeAnd(LHSVal, RHSVal));
+ Env.setValue(*S, bool_model::logicalAndOp(LHSVal, RHSVal, Env));
else
- Env.setValue(*S, Env.makeOr(LHSVal, RHSVal));
+ Env.setValue(*S, bool_model::logicalOrOp(LHSVal, RHSVal, Env));
break;
}
case BO_NE:
- case BO_EQ: {
- auto &LHSEqRHSValue = evaluateBooleanEquality(*LHS, *RHS, Env);
- Env.setValue(*S, S->getOpcode() == BO_EQ ? LHSEqRHSValue
- : Env.makeNot(LHSEqRHSValue));
+ Env.setValue(*S, evaluateInequality(*LHS, *RHS, Env));
break;
- }
- case BO_Comma: {
+ case BO_EQ:
+ Env.setValue(*S, evaluateEquality(*LHS, *RHS, Env));
+ break;
+ case BO_Comma:
propagateValueOrStorageLocation(*RHS, *S, Env);
break;
- }
default:
break;
}
@@ -273,7 +329,7 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
else
// FIXME: If integer modeling is added, then update this code to create
// the boolean based on the integer model.
- Env.setValue(*S, Env.makeAtomicBoolValue());
+ Env.setValue(*S, bool_model::freshBoolValue(Env));
break;
}
@@ -362,7 +418,7 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
if (SubExprVal == nullptr)
break;
- Env.setValue(*S, Env.makeNot(*SubExprVal));
+ Env.setValue(*S, bool_model::notOp(*SubExprVal, Env));
break;
}
default:
>From ed9bb21a095f3cce6d89865ff316162078bd5122 Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzhakm at google.com>
Date: Mon, 11 Mar 2024 16:57:14 +0000
Subject: [PATCH 2/3] [clang][dataflow] Add implementation of a simple boolean
model
The new model still uses atomic variables in boolean formulas, but it limits the
environment to accumulating truth values for atomic variables, rather than
the arbitrary formula allowed by the flow condition.
---
.../FlowSensitive/DataflowEnvironment.h | 4 +
.../clang/Analysis/FlowSensitive/Transfer.h | 32 +++-
.../FlowSensitive/DataflowEnvironment.cpp | 30 ++++
.../Models/UncheckedOptionalAccessModel.cpp | 3 +-
clang/lib/Analysis/FlowSensitive/Transfer.cpp | 146 +++++++++++++++++-
.../TypeErasedDataflowAnalysis.cpp | 4 +-
.../Analysis/FlowSensitive/TransferTest.cpp | 8 +-
.../TypeErasedDataflowAnalysisTest.cpp | 4 +
.../UncheckedOptionalAccessModelTest.cpp | 17 +-
9 files changed, 228 insertions(+), 20 deletions(-)
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index 2330697299fdd7..15ce37c13a6c77 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -500,6 +500,9 @@ class Environment {
return cast_or_null<T>(getValue(E));
}
+ std::optional<bool> getAtomValue(Atom A) const;
+ void setAtomValue(Atom A, bool);
+
// FIXME: should we deprecate the following & call arena().create() directly?
/// Creates a `T` (some subclass of `Value`), forwarding `args` to the
@@ -720,6 +723,7 @@ class Environment {
// deterministic sequence. This in turn produces deterministic SAT formulas.
llvm::MapVector<const Expr *, Value *> ExprToVal;
llvm::MapVector<const StorageLocation *, Value *> LocToVal;
+ llvm::MapVector<Atom, bool> AtomToVal;
Atom FlowConditionToken;
};
diff --git a/clang/include/clang/Analysis/FlowSensitive/Transfer.h b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
index bc8e9cdb03d703..6fe8ded1974c07 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Transfer.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
@@ -48,7 +48,7 @@ class StmtToEnvMap {
const TypeErasedDataflowAnalysisState &CurState;
};
-namespace bool_model {
+namespace sat_bool_model {
BoolValue &freshBoolValue(Environment &Env);
@@ -70,7 +70,35 @@ BoolValue ¬Op(BoolValue &Sub, Environment &Env);
// CondVal -- the abstract value representing the condition.
void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
-} // namespace bool_model
+} // namespace sat_bool_model
+
+namespace simple_bool_model {
+
+std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env);
+
+BoolValue &freshBoolValue(Environment &Env);
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue ¬Op(BoolValue &Sub, Environment &Env);
+
+// Models the transition along a branch edge in the CFG.
+// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
+// for `else`.
+// CondVal -- the abstract value representing the condition.
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
+
+} // namespace simple_bool_model
+
+namespace bool_model = simple_bool_model;
/// Evaluates `S` and updates `Env` accordingly.
///
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index cc1ebd511191a9..b573403dfd000f 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -17,6 +17,7 @@
#include "clang/AST/DeclCXX.h"
#include "clang/AST/Type.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Transfer.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
@@ -132,6 +133,13 @@ static Value *joinDistinctValues(QualType Type, Value &Val1,
auto &Expr1 = cast<BoolValue>(Val1).formula();
auto &Expr2 = cast<BoolValue>(Val2).formula();
auto &A = JoinedEnv.arena();
+
+#if 1
+ if (auto V1 = simple_bool_model::getLiteralValue(Expr1, Env1);
+ V1.has_value() && V1 == simple_bool_model::getLiteralValue(Expr2, Env2))
+ return &JoinedEnv.getBoolLiteralValue(*V1);
+#endif
+
auto &JoinedVal = A.makeAtomRef(A.makeAtom());
JoinedEnv.assume(
A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
@@ -706,6 +714,12 @@ Environment Environment::join(const Environment &EnvA, const Environment &EnvB,
JoinedEnv.ExprToLoc = joinExprMaps(EnvA.ExprToLoc, EnvB.ExprToLoc);
}
+ for (auto &Entry : EnvA.AtomToVal) {
+ auto It = EnvB.AtomToVal.find(Entry.first);
+ if (It != EnvB.AtomToVal.end() && Entry.second == It->second)
+ JoinedEnv.AtomToVal.insert({Entry.first, Entry.second});
+ }
+
return JoinedEnv;
}
@@ -1060,9 +1074,16 @@ void Environment::assume(const Formula &F) {
DACtx->addFlowConditionConstraint(FlowConditionToken, F);
}
+#if 0
bool Environment::proves(const Formula &F) const {
return DACtx->flowConditionImplies(FlowConditionToken, F);
}
+#else
+bool Environment::proves(const Formula &F) const {
+ auto V = simple_bool_model::getLiteralValue(F, *this);
+ return V.has_value() && *V;
+}
+#endif
bool Environment::allows(const Formula &F) const {
return DACtx->flowConditionAllows(FlowConditionToken, F);
@@ -1120,6 +1141,15 @@ void Environment::dump() const {
dump(llvm::dbgs());
}
+std::optional<bool> Environment::getAtomValue(Atom A) const {
+ auto It = AtomToVal.find(A);
+ if (It == AtomToVal.end())
+ return std::nullopt;
+ return It->second;
+}
+
+void Environment::setAtomValue(Atom A, bool b) { AtomToVal[A] = b; }
+
RecordStorageLocation *getImplicitObjectLocation(const CXXMemberCallExpr &MCE,
const Environment &Env) {
Expr *ImplicitObject = MCE.getImplicitObjectArgument();
diff --git a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
index dbf4878622eba9..f840ccd3828153 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -653,8 +653,7 @@ const Formula &evaluateEquality(Arena &A, const Formula &EqVal,
// If neither is set, then they are equal.
// We rewrite b) as !EqVal => (LHS v RHS), for a more compact formula.
return A.makeAnd(
- A.makeImplies(EqVal, A.makeOr(A.makeAnd(LHS, RHS),
- A.makeAnd(A.makeNot(LHS), A.makeNot(RHS)))),
+ A.makeImplies(EqVal, A.makeEquals(LHS, RHS)),
A.makeImplies(A.makeNot(EqVal), A.makeOr(LHS, RHS)));
}
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index 6e215daaf3fa19..dbe4d625652b69 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -81,7 +81,7 @@ static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
propagateValue(From, To, Env);
}
-namespace bool_model {
+namespace sat_bool_model {
BoolValue &freshBoolValue(Environment &Env) {
return Env.makeAtomicBoolValue();
@@ -110,15 +110,145 @@ BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
BoolValue ¬Op(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
- if (BranchVal)
- Env.assume(CondVal.formula());
- else
- // The condition must be inverted for the successor that encompasses the
- // "else" branch, if such exists.
- Env.assume(Env.makeNot(CondVal).formula());
+ // The condition must be inverted for the successor that encompasses the
+ // "else" branch, if such exists.
+ BoolValue &AssertedVal = BranchVal ? CondVal : Env.makeNot(CondVal);
+ Env.assume(AssertedVal.formula());
+}
+
+} // namespace sat_bool_model
+
+namespace simple_bool_model {
+
+std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env) {
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ return Env.getAtomValue(F.getAtom());
+ case Formula::Literal:
+ return F.literal();
+ case Formula::Not: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 1);
+ if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
+ return !*Maybe;
+ return std::nullopt;
+ }
+ default:
+ return std::nullopt;
+ }
+}
+
+BoolValue &freshBoolValue(Environment &Env) {
+ return Env.makeAtomicBoolValue();
+}
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
+ return unpackValue(V, Env);
+}
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ // FIXME: check if these optimizations are already built in to the formula
+ // generation.
+ if (auto V = getLiteralValue(LHS.formula(), Env))
+ return *V ? Env.getBoolLiteralValue(true) : RHS;
+ if (auto V = getLiteralValue(RHS.formula(), Env))
+ return *V ? Env.getBoolLiteralValue(true) : LHS;
+ return Env.makeOr(LHS, RHS);
+}
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ if (auto V = getLiteralValue(LHS.formula(), Env))
+ return *V ? RHS : Env.getBoolLiteralValue(false);
+ if (auto V = getLiteralValue(RHS.formula(), Env))
+ return *V ? LHS : Env.getBoolLiteralValue(false);
+ return Env.makeAnd(LHS, RHS);
+}
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ if (&LHS.formula() == &RHS.formula())
+ return Env.getBoolLiteralValue(true);
+ if (auto V = getLiteralValue(LHS.formula(), Env))
+ return *V ? RHS : Env.makeNot(RHS);
+ if (auto V = getLiteralValue(RHS.formula(), Env))
+ return *V ? LHS : Env.makeNot(LHS);
+ return Env.makeIff(LHS, RHS);
+}
+
+// FIXME: i think this could be implemented in terms of eqOp.
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+ if (&LHS.formula() == &RHS.formula())
+ return Env.getBoolLiteralValue(false);
+ if (auto V = getLiteralValue(LHS.formula(), Env))
+ return *V ? Env.makeNot(RHS) : RHS;
+ if (auto V = getLiteralValue(RHS.formula(), Env))
+ return *V ? Env.makeNot(LHS) : LHS;
+ return Env.makeNot(Env.makeIff(LHS, RHS));
+}
+
+BoolValue ¬Op(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
+
+// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
+// value to use for atoms encountered in the formula.
+static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
+ // TODO: handle literals directly rather than calling getLiteralValue.
+ std::optional<bool> Lit = getLiteralValue(F, Env);
+ if (Lit.has_value())
+ // FIXME: Nothing to do. Could verify no contradiction, but not sure what
+ // we'd do with that here. Need to poison the Env.
+ return;
+
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ // FIXME: check for contradictions
+ Env.setAtomValue(F.getAtom(), AtomVal);
+ break;
+ case Formula::Not: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 1);
+ assumeFormula(!AtomVal, *Operands[0], Env);
+ break;
+ }
+ case Formula::And: {
+ if (AtomVal == true) {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ assumeFormula(true, *Operands[0], Env);
+ assumeFormula(true, *Operands[1], Env);
+ }
+ break;
+ }
+ case Formula::Or: {
+ if (AtomVal == false) {
+ // Interpret the negated "or" as "and" of negated operands.
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ assumeFormula(false, *Operands[0], Env);
+ assumeFormula(false, *Operands[1], Env);
+ }
+ break;
+ }
+ case Formula::Equal: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ auto &LHS = *Operands[0];
+ auto &RHS = *Operands[1];
+ if (auto V = getLiteralValue(LHS, Env)) {
+ assumeFormula(AtomVal == *V, RHS, Env);
+ } else if (auto V = getLiteralValue(RHS, Env)) {
+ assumeFormula(AtomVal == *V, LHS, Env);
+ }
+ break;
+ }
+ default:
+ break;
+ }
+}
+
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
+ assumeFormula(BranchVal, CondVal.formula(), Env);
}
-} // namespace bool_model
+} // namespace simple_bool_model
// Unpacks the value (if any) associated with `E` and updates `E` to the new
// value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,
diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
index 595f70f819ddb5..df0427fa2cce32 100644
--- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -284,7 +284,6 @@ computeBlockInputState(const CFGBlock &Block, AnalysisContext &AC) {
Builder.addUnowned(PredState);
continue;
}
-
bool BranchVal = blockIndexInPredecessor(*Pred, Block) == 0;
// `transferBranch` may need to mutate the environment to describe the
@@ -465,7 +464,8 @@ transferCFGBlock(const CFGBlock &Block, AnalysisContext &AC,
// we have *some* value for the condition expression. This ensures that
// when we extend the flow condition, it actually changes.
if (State.Env.getValue(*TerminatorCond) == nullptr)
- State.Env.setValue(*TerminatorCond, State.Env.makeAtomicBoolValue());
+ State.Env.setValue(*TerminatorCond,
+ bool_model::freshBoolValue(State.Env));
AC.Log.recordState(State);
}
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 1d3b268976a767..4a0b148c1ee0da 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -6,6 +6,7 @@
//
//===----------------------------------------------------------------------===//
+#include "clang/Analysis/FlowSensitive/Transfer.h"
#include "TestingSupport.h"
#include "clang/AST/ASTContext.h"
#include "clang/AST/Decl.h"
@@ -35,6 +36,7 @@ using ::testing::Eq;
using ::testing::IsNull;
using ::testing::Ne;
using ::testing::NotNull;
+using ::testing::Optional;
using ::testing::UnorderedElementsAre;
// Declares a minimal coroutine library.
@@ -4412,12 +4414,12 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
bool foo();
void target() {
- do {
+ do {
bool Bar = foo();
if (Bar) break;
(void)Bar;
/*[[p]]*/
- } while (true);
+ } while (true);
}
)";
// The key property that we are verifying is implicit in `runDataflow` --
@@ -4434,6 +4436,8 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
ASSERT_THAT(BarDecl, NotNull());
auto &BarVal = getFormula(*BarDecl, Env);
+ ASSERT_EQ(BarVal.kind(), Formula::AtomRef);
+ ASSERT_THAT(Env.getAtomValue(BarVal.getAtom()), Optional(false));
EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
});
}
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
index bea00ab1a1f062..3724e877d60f57 100644
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -286,6 +286,10 @@ TEST_F(DiscardExprStateTest, BooleanOperator) {
const auto &AndOpState = blockStateForStmt(BlockStates, AndOp);
EXPECT_EQ(AndOpState.Env.getValue(*AndOp.getLHS()), LHSValue);
EXPECT_EQ(AndOpState.Env.getValue(*AndOp.getRHS()), RHSValue);
+ // FIXME: this test is too strict. We want to check equivalence not equality;
+ // as is, its a change detector test. Notice that we only evaluate `b1 && b2`
+ // in a context where we know that `b1 is true, so there's a potential
+ // optimization to store only `RHSValue` as the operation's value.
EXPECT_EQ(AndOpState.Env.getValue(AndOp),
&AndOpState.Env.makeAnd(*LHSValue, *RHSValue));
diff --git a/clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp
index 9430730004dbd2..7011345053e9a0 100644
--- a/clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp
@@ -1382,9 +1382,10 @@ class UncheckedOptionalAccessTest
INSTANTIATE_TEST_SUITE_P(
UncheckedOptionalUseTestInst, UncheckedOptionalAccessTest,
- ::testing::Values(OptionalTypeIdentifier{"std", "optional"},
- OptionalTypeIdentifier{"absl", "optional"},
- OptionalTypeIdentifier{"base", "Optional"}),
+ ::testing::Values(OptionalTypeIdentifier{"std", "optional"}// ,
+ // OptionalTypeIdentifier{"absl", "optional"},
+ // OptionalTypeIdentifier{"base", "Optional"}
+ ),
[](const ::testing::TestParamInfo<OptionalTypeIdentifier> &Info) {
return Info.param.NamespaceName;
});
@@ -2954,7 +2955,7 @@ TEST_P(UncheckedOptionalAccessTest, CorrelatedBranches) {
)");
}
-TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValuesThenCheck) {
ExpectDiagnosticsFor(
R"code(
#include "unchecked_optional_access_test.h"
@@ -2973,7 +2974,9 @@ TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
}
}
)code");
+}
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValuesCheckInBranches) {
ExpectDiagnosticsFor(R"code(
#include "unchecked_optional_access_test.h"
@@ -2989,7 +2992,9 @@ TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
opt.value();
}
)code");
+}
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValuesCheckInOneBranch) {
ExpectDiagnosticsFor(
R"code(
#include "unchecked_optional_access_test.h"
@@ -3005,7 +3010,9 @@ TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
opt.value(); // [[unsafe]]
}
)code");
+}
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValuesSetInBothBranches) {
ExpectDiagnosticsFor(
R"code(
#include "unchecked_optional_access_test.h"
@@ -3020,7 +3027,9 @@ TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
opt.value();
}
)code");
+}
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValuesSetInOneBranch) {
ExpectDiagnosticsFor(
R"code(
#include "unchecked_optional_access_test.h"
>From ff9537d374ba3062874d7b64aaa6947c860e0c79 Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzhakm at google.com>
Date: Thu, 21 Mar 2024 17:23:34 +0000
Subject: [PATCH 3/3] [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.
---
.../clang/Analysis/FlowSensitive/Transfer.h | 50 +----
.../FlowSensitive/DataflowEnvironment.cpp | 199 +++++++++++++++---
clang/lib/Analysis/FlowSensitive/Transfer.cpp | 143 +------------
.../TypeErasedDataflowAnalysis.cpp | 1 +
.../Analysis/FlowSensitive/TransferTest.cpp | 9 +
.../TypeErasedDataflowAnalysisTest.cpp | 2 +-
6 files changed, 184 insertions(+), 220 deletions(-)
diff --git a/clang/include/clang/Analysis/FlowSensitive/Transfer.h b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
index 6fe8ded1974c07..938ac5f3439ca8 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Transfer.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Transfer.h
@@ -48,57 +48,11 @@ class StmtToEnvMap {
const TypeErasedDataflowAnalysisState &CurState;
};
-namespace sat_bool_model {
+namespace bool_model {
BoolValue &freshBoolValue(Environment &Env);
-BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
-
-BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue ¬Op(BoolValue &Sub, Environment &Env);
-
-// Models the transition along a branch edge in the CFG.
-// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
-// for `else`.
-// CondVal -- the abstract value representing the condition.
-void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
-
-} // namespace sat_bool_model
-
-namespace simple_bool_model {
-
-std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env);
-
-BoolValue &freshBoolValue(Environment &Env);
-
-BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
-
-BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
-
-BoolValue ¬Op(BoolValue &Sub, Environment &Env);
-
-// Models the transition along a branch edge in the CFG.
-// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
-// for `else`.
-// CondVal -- the abstract value representing the condition.
-void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
-
-} // namespace simple_bool_model
-
-namespace bool_model = simple_bool_model;
+} // namespace bool_model
/// Evaluates `S` and updates `Env` accordingly.
///
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index b573403dfd000f..8a41c9b948d44b 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -17,7 +17,6 @@
#include "clang/AST/DeclCXX.h"
#include "clang/AST/Type.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
-#include "clang/Analysis/FlowSensitive/Transfer.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
@@ -30,6 +29,169 @@
namespace clang {
namespace dataflow {
+namespace simple_bool_model {
+static std::optional<bool> getLiteralValue(const Formula &F,
+ const Environment &Env) {
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ return Env.getAtomValue(F.getAtom());
+ case Formula::Literal:
+ return F.literal();
+ case Formula::Not: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 1);
+ if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
+ return !*Maybe;
+ return std::nullopt;
+ }
+ case Formula::And: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ auto &LHS = *Operands[0];
+ auto &RHS = *Operands[1];
+ if (std::optional<bool> Left = getLiteralValue(LHS, Env))
+ return !*Left ? Left : getLiteralValue(RHS, Env);
+ if (std::optional<bool> Right = getLiteralValue(RHS, Env); Right == false)
+ return Right;
+ return std::nullopt;
+ }
+ case Formula::Or: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ auto &LHS = *Operands[0];
+ auto &RHS = *Operands[1];
+ if (std::optional<bool> Left = getLiteralValue(LHS, Env))
+ return *Left ? Left : getLiteralValue(RHS, Env);
+ if (std::optional<bool> Right = getLiteralValue(RHS, Env); Right == true)
+ return Right;
+ return std::nullopt;
+ }
+ case Formula::Equal: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ auto &LHS = *Operands[0];
+ auto &RHS = *Operands[1];
+ if (&LHS == &RHS)
+ return true;
+ auto V_L = getLiteralValue(LHS, Env);
+ return V_L.has_value() && V_L == getLiteralValue(RHS, Env);
+ }
+ default:
+ return std::nullopt;
+ }
+}
+
+// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
+// value to use for atoms encountered in the formula.
+static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ // FIXME: if the atom is set to a different value, mark the block as
+ // unreachable.
+ Env.setAtomValue(F.getAtom(), AtomVal);
+ break;
+ case Formula::Literal:
+ // FIXME: if the literal is `false`, mark the block as unreachable.
+ break;
+ case Formula::Not: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 1);
+ assumeFormula(!AtomVal, *Operands[0], Env);
+ break;
+ }
+ case Formula::And: {
+ if (AtomVal == true) {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ assumeFormula(true, *Operands[0], Env);
+ assumeFormula(true, *Operands[1], Env);
+ }
+ break;
+ }
+ case Formula::Or: {
+ if (AtomVal == false) {
+ // Interpret the negated "or" as "and" of negated operands.
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ assumeFormula(false, *Operands[0], Env);
+ assumeFormula(false, *Operands[1], Env);
+ }
+ break;
+ }
+ case Formula::Equal: {
+ ArrayRef<const Formula *> Operands = F.operands();
+ assert(Operands.size() == 2);
+ auto &LHS = *Operands[0];
+ auto &RHS = *Operands[1];
+ if (auto V = getLiteralValue(LHS, Env)) {
+ assumeFormula(AtomVal == *V, RHS, Env);
+ } else if (auto V = getLiteralValue(RHS, Env)) {
+ assumeFormula(AtomVal == *V, LHS, Env);
+ }
+ break;
+ }
+ default:
+ break;
+ }
+}
+
+BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
+ const Environment &Env2, Environment &JoinedEnv) {
+ if (auto V1 = getLiteralValue(Val1.formula(), Env1);
+ V1.has_value() && V1 == getLiteralValue(Val2.formula(), Env2))
+ return JoinedEnv.getBoolLiteralValue(*V1);
+ return JoinedEnv.makeAtomicBoolValue();
+}
+
+void assume(Environment &Env, const Formula &F) {
+ assumeFormula(/*AtomVal*/ true, F, Env);
+}
+
+bool allows(const Environment &Env, const Formula &F) {
+ auto V = getLiteralValue(F, Env);
+ // We are conservative in the negative direction: if we can't determine the
+ // value, assume it is allowed.
+ return V.value_or(true);
+}
+
+bool proves(const Environment &Env, const Formula &F) {
+ auto V = getLiteralValue(F, Env);
+ return V.value_or(false);
+}
+} // namespace simple_bool_model
+
+namespace sat_bool_model {
+BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
+ const Environment &Env2, Environment &JoinedEnv) {
+ auto &A = JoinedEnv.arena();
+ auto &JoinedVal = JoinedEnv.makeAtomicBoolValue();
+ auto &JoinedFormula = JoinedVal.formula();
+ JoinedEnv.assume(
+ A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
+ A.makeEquals(JoinedFormula, Val1.formula())),
+ A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
+ A.makeEquals(JoinedFormula, Val2.formula()))));
+ return JoinedVal;
+}
+
+void assume(Environment &Env, const Formula &F) {
+ Env.getDataflowAnalysisContext().addFlowConditionConstraint(
+ Env.getFlowConditionToken(), F);
+}
+
+bool allows(const Environment &Env, const Formula &F) {
+ return Env.getDataflowAnalysisContext().flowConditionAllows(
+ Env.getFlowConditionToken(), F);
+}
+
+bool proves(const Environment &Env, const Formula &F) {
+ return Env.getDataflowAnalysisContext().flowConditionImplies(
+ Env.getFlowConditionToken(), F);
+}
+} // namespace sat_bool_model
+
+namespace bool_model = simple_bool_model;
+
// FIXME: convert these to parameters of the analysis or environment. Current
// settings have been experimentaly validated, but only for a particular
// analysis.
@@ -130,23 +292,9 @@ static Value *joinDistinctValues(QualType Type, Value &Val1,
// if (o.has_value())
// x = o.value();
// ```
- auto &Expr1 = cast<BoolValue>(Val1).formula();
- auto &Expr2 = cast<BoolValue>(Val2).formula();
- auto &A = JoinedEnv.arena();
-
-#if 1
- if (auto V1 = simple_bool_model::getLiteralValue(Expr1, Env1);
- V1.has_value() && V1 == simple_bool_model::getLiteralValue(Expr2, Env2))
- return &JoinedEnv.getBoolLiteralValue(*V1);
-#endif
-
- auto &JoinedVal = A.makeAtomRef(A.makeAtom());
- JoinedEnv.assume(
- A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
- A.makeEquals(JoinedVal, Expr1)),
- A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
- A.makeEquals(JoinedVal, Expr2))));
- return &A.makeBoolValue(JoinedVal);
+ auto &B1 = cast<BoolValue>(Val1);
+ auto &B2 = cast<BoolValue>(Val2);
+ return &bool_model::join(B1, Env1, B2, Env2, JoinedEnv);
}
Value *JoinedVal = nullptr;
@@ -1070,23 +1218,14 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
return Loc;
}
-void Environment::assume(const Formula &F) {
- DACtx->addFlowConditionConstraint(FlowConditionToken, F);
-}
+void Environment::assume(const Formula &F) { bool_model::assume(*this, F); }
-#if 0
-bool Environment::proves(const Formula &F) const {
- return DACtx->flowConditionImplies(FlowConditionToken, F);
-}
-#else
bool Environment::proves(const Formula &F) const {
- auto V = simple_bool_model::getLiteralValue(F, *this);
- return V.has_value() && *V;
+ return bool_model::proves(*this, F);
}
-#endif
bool Environment::allows(const Formula &F) const {
- return DACtx->flowConditionAllows(FlowConditionToken, F);
+ return bool_model::allows(*this, F);
}
void Environment::dump(raw_ostream &OS) const {
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index dbe4d625652b69..4ad58f82353fe0 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -81,7 +81,7 @@ static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
propagateValue(From, To, Env);
}
-namespace sat_bool_model {
+namespace bool_model {
BoolValue &freshBoolValue(Environment &Env) {
return Env.makeAtomicBoolValue();
@@ -109,146 +109,7 @@ BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
BoolValue ¬Op(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
-void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
- // The condition must be inverted for the successor that encompasses the
- // "else" branch, if such exists.
- BoolValue &AssertedVal = BranchVal ? CondVal : Env.makeNot(CondVal);
- Env.assume(AssertedVal.formula());
-}
-
-} // namespace sat_bool_model
-
-namespace simple_bool_model {
-
-std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env) {
- switch (F.kind()) {
- case Formula::AtomRef:
- return Env.getAtomValue(F.getAtom());
- case Formula::Literal:
- return F.literal();
- case Formula::Not: {
- ArrayRef<const Formula *> Operands = F.operands();
- assert(Operands.size() == 1);
- if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
- return !*Maybe;
- return std::nullopt;
- }
- default:
- return std::nullopt;
- }
-}
-
-BoolValue &freshBoolValue(Environment &Env) {
- return Env.makeAtomicBoolValue();
-}
-
-BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
- return unpackValue(V, Env);
-}
-
-BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
- // FIXME: check if these optimizations are already built in to the formula
- // generation.
- if (auto V = getLiteralValue(LHS.formula(), Env))
- return *V ? Env.getBoolLiteralValue(true) : RHS;
- if (auto V = getLiteralValue(RHS.formula(), Env))
- return *V ? Env.getBoolLiteralValue(true) : LHS;
- return Env.makeOr(LHS, RHS);
-}
-
-BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
- if (auto V = getLiteralValue(LHS.formula(), Env))
- return *V ? RHS : Env.getBoolLiteralValue(false);
- if (auto V = getLiteralValue(RHS.formula(), Env))
- return *V ? LHS : Env.getBoolLiteralValue(false);
- return Env.makeAnd(LHS, RHS);
-}
-
-BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
- if (&LHS.formula() == &RHS.formula())
- return Env.getBoolLiteralValue(true);
- if (auto V = getLiteralValue(LHS.formula(), Env))
- return *V ? RHS : Env.makeNot(RHS);
- if (auto V = getLiteralValue(RHS.formula(), Env))
- return *V ? LHS : Env.makeNot(LHS);
- return Env.makeIff(LHS, RHS);
-}
-
-// FIXME: i think this could be implemented in terms of eqOp.
-BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
- if (&LHS.formula() == &RHS.formula())
- return Env.getBoolLiteralValue(false);
- if (auto V = getLiteralValue(LHS.formula(), Env))
- return *V ? Env.makeNot(RHS) : RHS;
- if (auto V = getLiteralValue(RHS.formula(), Env))
- return *V ? Env.makeNot(LHS) : LHS;
- return Env.makeNot(Env.makeIff(LHS, RHS));
-}
-
-BoolValue ¬Op(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
-
-// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
-// value to use for atoms encountered in the formula.
-static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
- // TODO: handle literals directly rather than calling getLiteralValue.
- std::optional<bool> Lit = getLiteralValue(F, Env);
- if (Lit.has_value())
- // FIXME: Nothing to do. Could verify no contradiction, but not sure what
- // we'd do with that here. Need to poison the Env.
- return;
-
- switch (F.kind()) {
- case Formula::AtomRef:
- // FIXME: check for contradictions
- Env.setAtomValue(F.getAtom(), AtomVal);
- break;
- case Formula::Not: {
- ArrayRef<const Formula *> Operands = F.operands();
- assert(Operands.size() == 1);
- assumeFormula(!AtomVal, *Operands[0], Env);
- break;
- }
- case Formula::And: {
- if (AtomVal == true) {
- ArrayRef<const Formula *> Operands = F.operands();
- assert(Operands.size() == 2);
- assumeFormula(true, *Operands[0], Env);
- assumeFormula(true, *Operands[1], Env);
- }
- break;
- }
- case Formula::Or: {
- if (AtomVal == false) {
- // Interpret the negated "or" as "and" of negated operands.
- ArrayRef<const Formula *> Operands = F.operands();
- assert(Operands.size() == 2);
- assumeFormula(false, *Operands[0], Env);
- assumeFormula(false, *Operands[1], Env);
- }
- break;
- }
- case Formula::Equal: {
- ArrayRef<const Formula *> Operands = F.operands();
- assert(Operands.size() == 2);
- auto &LHS = *Operands[0];
- auto &RHS = *Operands[1];
- if (auto V = getLiteralValue(LHS, Env)) {
- assumeFormula(AtomVal == *V, RHS, Env);
- } else if (auto V = getLiteralValue(RHS, Env)) {
- assumeFormula(AtomVal == *V, LHS, Env);
- }
- break;
- }
- default:
- break;
- }
-}
-
-void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
- assumeFormula(BranchVal, CondVal.formula(), Env);
-}
-
-} // namespace simple_bool_model
+} // namespace bool_model
// Unpacks the value (if any) associated with `E` and updates `E` to the new
// value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,
diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
index df0427fa2cce32..bea19776daba18 100644
--- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -296,6 +296,7 @@ computeBlockInputState(const CFGBlock &Block, AnalysisContext &AC) {
// assert ourselves instead of asserting via `cast()` so that we get
// a more meaningful line number if the assertion fails.
assert(CondVal != nullptr);
+ // Invert the condition if this is the successor for the "else" branch.
BoolValue *AssertedVal =
BranchVal ? CondVal : &Copy.Env.makeNot(*CondVal);
Copy.Env.assume(AssertedVal->formula());
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 4a0b148c1ee0da..3765bdcfb23d00 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -3749,6 +3749,11 @@ TEST(TransferTest, AssignFromBoolLiteral) {
});
}
+// TODO: this looks like a change-detector test. And, I don't see the value of
+// the three different cases. Why not 12? It's really not clear what we're
+// getting at here. Is this a test for correct formula construction? If so, we
+// should name it (and comment) rather than tieing it to assignment.
+// Also, this should be "InitializeFrom...".
TEST(TransferTest, AssignFromCompositeBoolExpression) {
{
std::string Code = R"(
@@ -5119,6 +5124,10 @@ TEST(TransferTest, WhileStmtBranchExtendsFlowCondition) {
});
}
+// TODO: this test is overly complicated for what its name implies it's
+// testing. It involves a complex condition of (A or B), where neither holds
+// separately. But, that involves join machinery and SAT solving, which is well
+// more than the simple test for DoWhile support in flow-condition extenionsion.
TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) {
std::string Code = R"(
void target(bool Foo) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
index 3724e877d60f57..d12e79c7848ddf 100644
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -288,7 +288,7 @@ TEST_F(DiscardExprStateTest, BooleanOperator) {
EXPECT_EQ(AndOpState.Env.getValue(*AndOp.getRHS()), RHSValue);
// FIXME: this test is too strict. We want to check equivalence not equality;
// as is, its a change detector test. Notice that we only evaluate `b1 && b2`
- // in a context where we know that `b1 is true, so there's a potential
+ // in a context where we know that `b1` is true, so there's a potential
// optimization to store only `RHSValue` as the operation's value.
EXPECT_EQ(AndOpState.Env.getValue(AndOp),
&AndOpState.Env.makeAnd(*LHSValue, *RHSValue));
More information about the cfe-commits
mailing list