llvmorg-github-actions[bot] wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang Author: Jan Voung (jvoung) <details> <summary>Changes</summary> For https://github.com/llvm/llvm-project/issues/224638. Based on an earlier attempt https://github.com/llvm/llvm-project/pull/82950 but with cleanups and fixes. This allows the dataflow analyses to run without a SAT solver (and much faster) with a tradeoff that correlated branches and some disjunctions are not handled (more false positives). None of the models needed to change -- this is swapped in transparently during `assume`, `proves`, `allows`, etc. - fix the FIXMEs regarding unreachable blocks - fill out more forced assignment cases during assumeFormula (e.g., for Equal and Implies, more Or cases) - track assumed formulas which aren't resolved initially, and try later to a fixed point. A later assume() call can make an earlier assumed formula have literals (this can happen when we branch to the then vs else). For example, helps when the model uses makeImplies e.g., for InequalityCheckRightNullopt. - expose joinBoolValues to reuse in Crubit's `mergeFormulas` instead of exposing the `FlowConditionToken` and always doing a join with a `makeOr`: https://github.com/google/crubit/blob/2e91a0a3d93ae631d2e04333fd7fa34c6d5e7f8a/nullability/pointer_nullability_analysis.cc#L140 - fill out popCall, equivalentTo, etc. Currently only hooks up to some parameterized tests. The next patch will hook it into some checker options (for std::optional, then absl::StatusOr) Leave to future work whether to do a hybrid of the models. === Example benchmarks with optional checker (checker time only). (1) llvm/tools/obj2yaml/elf2yaml.cpp - Watched Literals Solver: 42 s - Z3: 2.4 s - Simple: 0.2 s (2) llvm/lib/Target/AArch64/AArch64ISelLowering.cpp - WLS: 23 s - Z3: 0.9 s - Simple: 0.2 s (3) llvm/tools/llvm-readobj/ELFDumper.cpp - WLS: 83 s - Z3: 4.9 s - Simple: 0.3 s --- Patch is 116.52 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/231061.diff 5 Files Affected: - (modified) clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h (+21-2) - (modified) clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h (+88-13) - (modified) clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp (+524-24) - (modified) clang/unittests/Analysis/FlowSensitive/TransferTest.cpp (+427-293) - (modified) clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp (+37-11) ``````````diff diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 36d735db46b19..2320d071b3e2f 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -55,6 +55,20 @@ struct SimpleLogicalContext { llvm::DenseMap<Atom, llvm::DenseSet<Atom>> TokenDeps; }; +/// Selects the boolean model used to represent and reason about path +/// conditions and boolean values in `Environment`. +enum class BoolModelKind { + /// Full boolean formula tracking backed by a SAT solver. + SAT, + /// Lightweight model that tracks known truth assignments for atoms (e.g., + /// for each `assume()`) and unresolved assumed formulas, propagating forced + /// assignments and evaluating queries directly without invoking a SAT + /// solver. + /// Join operations are more conservative than in the SAT model (intersecting + /// known facts instead of encoding a disjunctive case split). + Simple, +}; + /// Owns objects that encompass the state of a program and stores context that /// is used during dataflow analysis. class DataflowAnalysisContext { @@ -70,6 +84,9 @@ class DataflowAnalysisContext { /// (This is always non-null within an AnalysisContext, the framework /// provides a fallback no-op logger). Logger *Log = nullptr; + + /// Which boolean model to use in `Environment`. + BoolModelKind BoolModel = BoolModelKind::SAT; }; /// Constructs a dataflow analysis context. @@ -80,7 +97,8 @@ class DataflowAnalysisContext { DataflowAnalysisContext(std::unique_ptr<Solver> S, Options Opts = Options{ /*ContextSensitiveOpts=*/std::nullopt, - /*Logger=*/nullptr}) + /*Logger=*/nullptr, + /*BoolModel=*/BoolModelKind::SAT}) : DataflowAnalysisContext(*S, std::move(S), Opts) {} /// Constructs a dataflow analysis context. @@ -90,7 +108,8 @@ class DataflowAnalysisContext { /// `S` must outlive the `DataflowAnalysisContext`. DataflowAnalysisContext(Solver &S, Options Opts = Options{ /*ContextSensitiveOpts=*/std::nullopt, - /*Logger=*/nullptr}) + /*Logger=*/nullptr, + /*BoolModel=*/BoolModelKind::SAT}) : DataflowAnalysisContext(S, nullptr, Opts) {} ~DataflowAnalysisContext(); diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index 47ac06137bb5f..d55e50002ff3f 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -34,6 +34,7 @@ #include "llvm/Support/ErrorHandling.h" #include <cassert> #include <memory> +#include <optional> #include <type_traits> #include <utility> #include <vector> @@ -157,19 +158,82 @@ class Environment { } }; + /// Abstract interface for modeling boolean formulas and path conditions in + /// an `Environment`. + class BoolModel { + public: + explicit BoolModel(BoolModelKind K) : K(K) {} + virtual ~BoolModel() = default; + + BoolModelKind getKind() const { return K; } + + /// Returns an exact copy of this model state. + virtual std::unique_ptr<BoolModel> clone() const = 0; + + /// If this model state was cloned, updates this model state to be a fork + /// so that mutations to either model state will not affect the other. + virtual void onFork() = 0; + + /// Records a fact that must be true if this point in the program is + /// reached. + virtual void assume(const Formula &F) = 0; + + /// Returns true if `F` is always true when this point is reached. + /// Returns false if the formula may be false (or the flow condition isn't + /// sufficiently precise to prove that it is true). + /// See `Environment::proves` for more details. + virtual bool proves(const Formula &F) const = 0; + + /// Returns true if `F` may be true when this point is reached. + /// Returns false if the formula is always false when this point is reached + /// (or the flow condition is overly constraining). + /// See `Environment::allows` for more details. + virtual bool allows(const Formula &F) const = 0; + + /// Joins two distinct boolean values `Val1` (from `Model1`) and `Val2` + /// (from `Model2`) into `JoinedEnv`. + /// Requires `Model1` and `Model2` to have the same kind as `this`. + virtual BoolValue &joinBoolValues(BoolValue &Val1, const BoolModel &Model1, + BoolValue &Val2, const BoolModel &Model2, + Environment &JoinedEnv) = 0; + + /// Populates `this` with the join of `ModelA` and `ModelB`. + /// + /// Requirements: `ModelA` and `ModelB` must have the same kind as `this`. + virtual void join(const BoolModel &ModelA, const BoolModel &ModelB) = 0; + + /// Widens `this` with respect to `PrevModel` and returns whether the state + /// changed relative to `PrevModel`. + /// + /// Requirements: `PrevModel` must have the same kind as `this`. + virtual LatticeEffect widen(const BoolModel &PrevModel) = 0; + + /// Returns whether this boolean model state is equivalent to `Other` for + /// convergence purposes. + /// Requirements: `Other` must have the same kind as `this`. + virtual bool isEquivalentTo(const BoolModel &Other) const = 0; + + /// Returns the flow condition token (only meaningful for SAT-based models). + virtual Atom getFlowConditionToken() const = 0; + + virtual void dump(raw_ostream &OS) const = 0; + + private: + BoolModelKind K; + }; + /// Creates an environment that uses `DACtx` to store objects that encompass /// the state of a program. `FlowConditionToken` sets the flow condition - /// associated with the environment. Generally, new environments should be - /// initialized with a fresh token, by using one of the other - /// constructors. This constructor is for specialized use, including - /// deserialization and delegation from other constructors. - Environment(DataflowAnalysisContext &DACtx, Atom FlowConditionToken) - : DACtx(&DACtx), FlowConditionToken(FlowConditionToken) {} + /// associated with the environment (requires `DACtx.getOptions().BoolModel == + /// BoolModelKind::SAT`). Generally, new environments should be initialized + /// using one of the other constructors. This constructor is for specialized + /// use, such as deserialization. + Environment(DataflowAnalysisContext &DACtx, Atom FlowConditionToken); /// Creates an environment that uses `DACtx` to store objects that encompass - /// the state of a program. Populates a fresh atom as flow condition token. - explicit Environment(DataflowAnalysisContext &DACtx) - : Environment(DACtx, DACtx.arena().makeFlowConditionToken()) {} + /// the state of a program. Initializes the boolean model configured in + /// `DACtx.getOptions().BoolModel`. + explicit Environment(DataflowAnalysisContext &DACtx); /// Creates an environment that uses `DACtx` to store objects that encompass /// the state of a program, with `S` as the statement to analyze. @@ -279,6 +343,14 @@ class Environment { Environment &JoinedEnv, Environment::ValueModel &Model); + /// Joins two distinct boolean values `Val1` (from `Env1`) and `Val2` (from + /// `Env2`) into this environment. + BoolValue &joinBoolValues(BoolValue &Val1, const Environment &Env1, + BoolValue &Val2, const Environment &Env2) { + return BoolState->joinBoolValues(Val1, *Env1.BoolState, Val2, + *Env2.BoolState, *this); + } + /// Widens the environment point-wise, using `PrevEnv` as needed to inform the /// approximation. /// @@ -669,7 +741,9 @@ class Environment { /// In particular, where the FC token appears in flow conditions of successor /// environments, it means "point X may have been reached", not /// "point X was reached". - Atom getFlowConditionToken() const { return FlowConditionToken; } + Atom getFlowConditionToken() const { + return BoolState->getFlowConditionToken(); + } /// Record a fact that must be true if this point in the program is reached. void assume(const Formula &); @@ -720,8 +794,8 @@ class Environment { using ThisExprOverridesMap = llvm::DenseMap<const CXXThisExpr *, RecordStorageLocation *>; - // The copy-constructor is for use in fork() only. - Environment(const Environment &) = default; + // The copy-constructor is for use in fork() and pushCall() only. + Environment(const Environment &); /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise /// return null. @@ -855,7 +929,8 @@ class Environment { llvm::MapVector<const Expr *, Value *> ExprToVal; llvm::MapVector<const StorageLocation *, Value *> LocToVal; - Atom FlowConditionToken; + // The flow condition abstracted in a boolean model. + std::unique_ptr<BoolModel> BoolState; }; /// Returns the storage location for the implicit object of a diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp index ab0b76037837f..268ee8af63796 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -22,16 +22,20 @@ #include "clang/Analysis/FlowSensitive/ASTOps.h" #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h" #include "clang/Analysis/FlowSensitive/DataflowLattice.h" +#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "clang/Basic/LLVM.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/MapVector.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/ScopeExit.h" +#include "llvm/ADT/SetVector.h" #include "llvm/Support/ErrorHandling.h" #include <cassert> #include <memory> +#include <optional> #include <stack> #include <utility> @@ -40,6 +44,481 @@ namespace clang { namespace dataflow { +namespace { + +class SimpleBoolModel : public Environment::BoolModel { +public: + SimpleBoolModel() : BoolModel(BoolModelKind::Simple) {} + + static bool classof(const BoolModel *M) { + return M->getKind() == BoolModelKind::Simple; + } + + std::unique_ptr<BoolModel> clone() const override { + return std::make_unique<SimpleBoolModel>(*this); + } + + void onFork() override {} + + void assume(const Formula &F) override { + if (HasContradiction) + return; + unsigned PrevSize = AtomToVal.size(); + // Given that F is assumed true, see if we can force the assignment + // of any atoms and ultimately reduce F to a literal (if possible). + // For example, if F is `A && B`, we will force `A` and `B` to be true. + // If F is `A || B`, we will only force an assignment if one of A or B is + // already known to be false. + assumeFormula(/*AssumedVal=*/true, F); + if (HasContradiction) + return; + + // Retain `F` in `AssumedFormulas` only if it has not yet been reduced to a + // known truth value in `AtomToVal` (e.g., `A || B` or `A == B` where + // neither side is known yet). + // + // - Why save unresolved formulas: a compound formula (like + // `EqVal => (LHS == RHS)` from a comparison expression) is often assumed + // while its atoms are still unknown; when we later follow a branch that + // fixes one of those atoms, the propagation loop below can reduce the + // saved formula to concrete `AtomToVal` entries. + // + // - Skipping formulas that already evaluate to `true` avoids bloating + // `AssumedFormulas` with single-atom and conjunctive assumptions that are + // already fully represented by `AtomToVal` (though it also drops + // disjunctive formulas that were reduced using a branch-local atom, such + // as on the RHS of a short-circuit `&&` or `||`). + // TODO(jvoung): We may want to retain some disjunctive formulas, but + // would need to profile and see how much it helps vs how much it costs. + if (std::optional<bool> Val = getLiteralValue(F)) { + if (!*Val) { + HasContradiction = true; + return; + } + } else { + AssumedFormulas.insert(&F); + } + + if (AtomToVal.size() == PrevSize) + return; + + // Propagate newly learned atom values through any pending assumed formulas. + // Note: Do not remove formulas from `AssumedFormulas` when they evaluate to + // `true` in a branch, because the atoms that satisfied them may be + // branch-local and discarded at a subsequent `join`, where the formula + // itself still holds on both branches. + bool Changed = true; + while (Changed && !HasContradiction) { + Changed = false; + for (const Formula *Pending : AssumedFormulas) { + unsigned Before = AtomToVal.size(); + assumeFormula(/*AssumedVal=*/true, *Pending); + if (HasContradiction) + return; + if (getLiteralValue(*Pending) == false) { + HasContradiction = true; + return; + } + if (AtomToVal.size() > Before) + Changed = true; + } + } + } + + bool proves(const Formula &F) const override { + if (HasContradiction) + return true; + auto V = getLiteralValue(F); + return V.value_or(false); + } + + bool allows(const Formula &F) const override { + if (HasContradiction) + return false; + auto V = getLiteralValue(F); + // We are conservative in the negative direction: if we can't determine the + // value, assume it is allowed. + return V.value_or(true); + } + + BoolValue &joinBoolValues(BoolValue &Val1, const BoolModel &Model1, + BoolValue &Val2, const BoolModel &Model2, + Environment &JoinedEnv) override { + const auto &S1 = cast<SimpleBoolModel>(Model1); + const auto &S2 = cast<SimpleBoolModel>(Model2); + if (S1.HasContradiction && !S2.HasContradiction) + return Val2; + if (S2.HasContradiction && !S1.HasContradiction) + return Val1; + if (auto V1 = S1.getLiteralValue(Val1.formula()); + V1.has_value() && V1 == S2.getLiteralValue(Val2.formula())) + return JoinedEnv.getBoolLiteralValue(*V1); + return JoinedEnv.makeAtomicBoolValue(); + } + + void join(const BoolModel &ModelA, const BoolModel &ModelB) override { + const auto &SA = cast<SimpleBoolModel>(ModelA); + const auto &SB = cast<SimpleBoolModel>(ModelB); + AtomToVal.clear(); + AssumedFormulas.clear(); + HasContradiction = false; + + if (SA.HasContradiction && SB.HasContradiction) { + HasContradiction = true; + } else if (SA.HasContradiction) { + AtomToVal = SB.AtomToVal; + AssumedFormulas = SB.AssumedFormulas; + } else if (SB.HasContradiction) { + AtomToVal = SA.AtomToVal; + AssumedFormulas = SA.AssumedFormulas; + } else { + // Intersect the AtomToVal maps. + for (const auto &Entry : SA.AtomToVal) { + auto It = SB.AtomToVal.find(Entry.first); + if (It != SB.AtomToVal.end() && Entry.second == It->second) + AtomToVal.insert({Entry.first, Entry.second}); + } + + // Keep assumed formulas that hold on both branches: either because both + // environments still carry `F` as an unresolved formula, or because one + // branch carries `F` and the other branch's `AtomToVal` assignments + // already prove `F`. Any branch-local formulas not proved by the other + // branch are dropped here, which shrinks `AssumedFormulas` at joins. + for (const Formula *F : SA.AssumedFormulas) { + if (SB.AssumedFormulas.contains(F) || SB.proves(*F)) + AssumedFormulas.insert(F); + } + for (const Formula *F : SB.AssumedFormulas) { + if (SA.proves(*F)) + AssumedFormulas.insert(F); + } + } + } + + LatticeEffect widen(const BoolModel &PrevModel) override { + const auto &PrevSimple = cast<SimpleBoolModel>(PrevModel); + SimpleBoolModel Widened; + Widened.join(*this, PrevSimple); + LatticeEffect Effect = Widened.isEquivalentTo(PrevSimple) + ? LatticeEffect::Unchanged + : LatticeEffect::Changed; + *this = std::move(Widened); + return Effect; + } + + bool isEquivalentTo(const BoolModel &Other) const override { + const auto &OtherSimple = cast<SimpleBoolModel>(Other); + if (HasContradiction != OtherSimple.HasContradiction) + return false; + if (HasContradiction) + return true; + if (AtomToVal.size() != OtherSimple.AtomToVal.size() || + AssumedFormulas != OtherSimple.AssumedFormulas) + return false; + return llvm::all_of(AtomToVal, [&](const auto &Entry) { + return OtherSimple.getAtomValue(Entry.first) == Entry.second; + }); + } + + Atom getFlowConditionToken() const override { + llvm_unreachable( + "getFlowConditionToken() is only supported in SatBoolModel"); + } + + void dump(raw_ostream &OS) const override { + OS << "SimpleBoolModel:\n"; + OS << " HasContradiction: " << HasContradiction << "\n"; + OS << " AtomToVal:\n"; + for (auto [A, V] : AtomToVal) + OS << " " << A << " = " << (V ? "true" : "false") << "\n"; + OS << " AssumedFormulas:\n"; + for (const Formula *F : AssumedFormulas) + OS << " " << *F << "\n"; + } + +private: + std::optional<bool> getAtomValue(Atom A) const { + auto It = AtomToVal.find(A); + if (It == AtomToVal.end()) + return std::nullopt; + return It->second; + } + + void setAtomValue(Atom A, bool B) { AtomToVal[A] = B; } + + std::optional<bool> getLiteralValue(const Formula &F) const { + switch (F.kind()) { + case Formula::AtomRef: + return 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])) + 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)) + return !*Left ? Left : getLiteralValue(RHS); + if (std::optional<bool> Right = getLiteralValue(RHS); 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)) + return *Left ? Left : getLiteralValue(RHS); + if (std::optional<bool> Right = getLiteralValue(RHS); Right == true) + return Right; + return std::nullopt; + } + case Formula::Implies: { + 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)) + return !*Left ? true : getLiteralValue(RHS); + if (std::optional<bool> Right = getLiteralValue(RHS); Right == true) + return true; + 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; + if ((LHS.kind() == Formula::Not && LHS.operands()[0] == &RHS) || + (RHS.kind() == Formula::Not && RHS.operands()[0] == &LHS)) + return false; + auto V_L = getLiteralValue(LHS); + if (!V_L.has_value()) + return std::nullopt; + aut... [truncated] `````````` </details> https://github.com/llvm/llvm-project/pull/231061 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
