Skip to content

Commit

Permalink
Revert "Reland "[dataflow] Add dedicated representation of boolean fo…
Browse files Browse the repository at this point in the history 
…rmulas" and followups

These changes are OK, but they break downstream stuff that needs more time to adapt :-(

This reverts commit 7157956.
This reverts commit 5e4ad81.
This reverts commit 1c3ac8d.
  • Loading branch information
@sam-mccall
sam-mccall committed Jul 5, 2023
1 parent e52a6d7 commit 2d8cd19
Show file tree
Hide file tree
Showing 24 changed files with 1,458 additions and 976 deletions.
116 changes: 50 additions & 66 deletions clang/include/clang/Analysis/FlowSensitive/Arena.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,20 +8,19 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H

#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include <vector>

namespace clang::dataflow {

/// The Arena owns the objects that model data within an analysis.
/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
/// For example, `Value` and `StorageLocation`.
class Arena {
public:
Arena()
: True(Formula::create(Alloc, Formula::Literal, {}, 1)),
False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
: TrueVal(create<AtomicBoolValue>()),
FalseVal(create<AtomicBoolValue>()) {}
Arena(const Arena &) = delete;
Arena &operator=(const Arena &) = delete;

Expand Down Expand Up @@ -57,89 +56,74 @@ class Arena {
.get());
}

/// Creates a BoolValue wrapping a particular formula.
///
/// Passing in the same formula will result in the same BoolValue.
/// FIXME: Interning BoolValues but not other Values is inconsistent.
/// Decide whether we want Value interning or not.
BoolValue &makeBoolValue(const Formula &);

/// Creates a fresh atom and wraps in in an AtomicBoolValue.
/// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
/// Stop relying on pointer identity and remove this guarantee.
AtomicBoolValue &makeAtomValue() {
return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
}

/// Creates a fresh Top boolean value.
TopBoolValue &makeTopValue() {
// No need for deduplicating: there's no way to create aliasing Tops.
return create<TopBoolValue>(makeAtomRef(makeAtom()));
}
/// Returns a boolean value that represents the conjunction of `LHS` and
/// `RHS`. Subsequent calls with the same arguments, regardless of their
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS);

/// Returns a boolean value that represents the disjunction of `LHS` and
/// `RHS`. Subsequent calls with the same arguments, regardless of their
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS);

/// Returns a boolean value that represents the negation of `Val`. Subsequent
/// calls with the same argument will return the same result.
BoolValue &makeNot(BoolValue &Val);

/// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
/// with the same arguments, will return the same result. If the given boolean
/// values represent the same value, the result will be a value that
/// represents the true boolean literal.
BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS);

/// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls
/// with the same arguments, regardless of their order, will return the same
/// result. If the given boolean values represent the same value, the result
/// will be a value that represents the true boolean literal.
BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS);

/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`. These literals are the same every time.
/// Integer literals are not typed; the type is determined by the `Expr` that
/// an integer literal is associated with.
IntegerValue &makeIntLiteral(llvm::APInt Value);

// Factories for boolean formulas.
// Formulas are interned: passing the same arguments return the same result.
// For commutative operations like And/Or, interning ignores order.
// Simplifications are applied: makeOr(X, X) => X, etc.

/// Returns a formula for the conjunction of `LHS` and `RHS`.
const Formula &makeAnd(const Formula &LHS, const Formula &RHS);

/// Returns a formula for the disjunction of `LHS` and `RHS`.
const Formula &makeOr(const Formula &LHS, const Formula &RHS);

/// Returns a formula for the negation of `Val`.
const Formula &makeNot(const Formula &Val);

/// Returns a formula for `LHS => RHS`.
const Formula &makeImplies(const Formula &LHS, const Formula &RHS);

/// Returns a formula for `LHS <=> RHS`.
const Formula &makeEquals(const Formula &LHS, const Formula &RHS);

/// Returns a formula for the variable A.
const Formula &makeAtomRef(Atom A);

/// Returns a formula for a literal true/false.
const Formula &makeLiteral(bool Value) { return Value ? True : False; }

/// Returns a new atomic boolean variable, distinct from any other.
Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`. These literals are the same every time.
AtomicBoolValue &makeLiteral(bool Value) const {
return Value ? TrueVal : FalseVal;
}

/// Creates a fresh flow condition and returns a token that identifies it. The
/// token can be used to perform various operations on the flow condition such
/// as adding constraints to it, forking it, joining it with another flow
/// condition, or checking implications.
Atom makeFlowConditionToken() { return makeAtom(); }
AtomicBoolValue &makeFlowConditionToken() {
return create<AtomicBoolValue>();
}

private:
llvm::BumpPtrAllocator Alloc;

// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;

// Indices that are used to avoid recreating the same integer literals and
// composite boolean values.
llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
using FormulaPair = std::pair<const Formula *, const Formula *>;
llvm::DenseMap<FormulaPair, const Formula *> Ands;
llvm::DenseMap<FormulaPair, const Formula *> Ors;
llvm::DenseMap<const Formula *, const Formula *> Nots;
llvm::DenseMap<FormulaPair, const Formula *> Implies;
llvm::DenseMap<FormulaPair, const Formula *> Equals;
llvm::DenseMap<Atom, const Formula *> AtomRefs;

llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
unsigned NextAtom = 0;

const Formula &True, &False;
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
ConjunctionVals;
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
DisjunctionVals;
llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
ImplicationVals;
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
BiconditionalVals;

AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
};

} // namespace clang::dataflow
Expand Down
29 changes: 16 additions & 13 deletions clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,31 +138,33 @@ class DataflowAnalysisContext {
PointerValue &getOrCreateNullPointerValue(QualType PointeeType);

/// Adds `Constraint` to the flow condition identified by `Token`.
void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
void addFlowConditionConstraint(AtomicBoolValue &Token,
BoolValue &Constraint);

/// Creates a new flow condition with the same constraints as the flow
/// condition identified by `Token` and returns its token.
Atom forkFlowCondition(Atom Token);
AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);

/// Creates a new flow condition that represents the disjunction of the flow
/// conditions identified by `FirstToken` and `SecondToken`, and returns its
/// token.
Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
AtomicBoolValue &SecondToken);

/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` imply that `Val` is true.
bool flowConditionImplies(Atom Token, const Formula &);
bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);

/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` are always true.
bool flowConditionIsTautology(Atom Token);
bool flowConditionIsTautology(AtomicBoolValue &Token);

/// Returns true if `Val1` is equivalent to `Val2`.
/// Note: This function doesn't take into account constraints on `Val1` and
/// `Val2` imposed by the flow condition.
bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);

LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS = llvm::dbgs());

/// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
Expand All @@ -179,7 +181,7 @@ class DataflowAnalysisContext {
/// included in `Constraints` to provide contextually-accurate results, e.g.
/// if any definitions or relationships of the values in `Constraints` have
/// been stored in flow conditions.
Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);

private:
friend class Environment;
Expand Down Expand Up @@ -207,12 +209,12 @@ class DataflowAnalysisContext {
/// to track tokens of flow conditions that were already visited by recursive
/// calls.
void addTransitiveFlowConditionConstraints(
Atom Token, llvm::SetVector<const Formula *> &Constraints,
llvm::DenseSet<Atom> &VisitedTokens);
AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);

/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
return querySolver(std::move(Constraints)).getStatus() ==
Solver::Result::Status::Unsatisfiable;
}
Expand Down Expand Up @@ -251,8 +253,9 @@ class DataflowAnalysisContext {
// Flow conditions depend on other flow conditions if they are created using
// `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
// dependencies is stored in the `FlowConditionDeps` map.
llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
FlowConditionDeps;
llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;

llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;

Expand Down
36 changes: 13 additions & 23 deletions clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -456,85 +456,77 @@ class Environment {
template <typename T, typename... Args>
std::enable_if_t<std::is_base_of<Value, T>::value, T &>
create(Args &&...args) {
return arena().create<T>(std::forward<Args>(args)...);
return DACtx->arena().create<T>(std::forward<Args>(args)...);
}

/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`
IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
return arena().makeIntLiteral(Value);
return DACtx->arena().makeIntLiteral(Value);
}

/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`
BoolValue &getBoolLiteralValue(bool Value) const {
return arena().makeBoolValue(arena().makeLiteral(Value));
AtomicBoolValue &getBoolLiteralValue(bool Value) const {
return DACtx->arena().makeLiteral(Value);
}

/// Returns an atomic boolean value.
BoolValue &makeAtomicBoolValue() const {
return arena().makeAtomValue();
return DACtx->arena().create<AtomicBoolValue>();
}

/// Returns a unique instance of boolean Top.
BoolValue &makeTopBoolValue() const {
return arena().makeTopValue();
return DACtx->arena().create<TopBoolValue>();
}

/// Returns a boolean value that represents the conjunction of `LHS` and
/// `RHS`. Subsequent calls with the same arguments, regardless of their
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
return arena().makeBoolValue(
arena().makeAnd(LHS.formula(), RHS.formula()));
return DACtx->arena().makeAnd(LHS, RHS);
}

/// Returns a boolean value that represents the disjunction of `LHS` and
/// `RHS`. Subsequent calls with the same arguments, regardless of their
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
return arena().makeBoolValue(
arena().makeOr(LHS.formula(), RHS.formula()));
return DACtx->arena().makeOr(LHS, RHS);
}

/// Returns a boolean value that represents the negation of `Val`. Subsequent
/// calls with the same argument will return the same result.
BoolValue &makeNot(BoolValue &Val) const {
return arena().makeBoolValue(arena().makeNot(Val.formula()));
return DACtx->arena().makeNot(Val);
}

/// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
/// the same arguments, will return the same result. If the given boolean
/// values represent the same value, the result will be a value that
/// represents the true boolean literal.
BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
return arena().makeBoolValue(
arena().makeImplies(LHS.formula(), RHS.formula()));
return DACtx->arena().makeImplies(LHS, RHS);
}

/// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
/// the same arguments, regardless of their order, will return the same
/// result. If the given boolean values represent the same value, the result
/// will be a value that represents the true boolean literal.
BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
return arena().makeBoolValue(
arena().makeEquals(LHS.formula(), RHS.formula()));
return DACtx->arena().makeEquals(LHS, RHS);
}

/// Returns the token that identifies the flow condition of the environment.
Atom getFlowConditionToken() const { return FlowConditionToken; }
AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }

/// Adds `Val` to the set of clauses that constitute the flow condition.
void addToFlowCondition(const Formula &);
LLVM_DEPRECATED("Use Formula version instead", "")
void addToFlowCondition(BoolValue &Val);

/// Returns true if and only if the clauses that constitute the flow condition
/// imply that `Val` is true.
bool flowConditionImplies(const Formula &) const;
LLVM_DEPRECATED("Use Formula version instead", "")
bool flowConditionImplies(BoolValue &Val) const;

/// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
Expand All @@ -555,8 +547,6 @@ class Environment {
/// Returns the `DataflowAnalysisContext` used by the environment.
DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }

Arena &arena() const { return DACtx->arena(); }

LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;

Expand Down Expand Up @@ -627,7 +617,7 @@ class Environment {
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;

Atom FlowConditionToken;
AtomicBoolValue *FlowConditionToken;
};

/// Returns the storage location for the implicit object of a
Expand Down

0 comments on commit 2d8cd19

Please sign in to comment.