-
Notifications
You must be signed in to change notification settings - Fork 10.8k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[dataflow] Add dedicated representation of boolean formulas
This is the first step in untangling the two current jobs of BoolValue. === Desired end-state: === - BoolValue will model C++ booleans e.g. held in StorageLocations. this includes describing uncertainty (e.g. "top" is a Value concern) - Formula describes analysis-level assertions in terms of SAT atoms. These can still be linked together: a BoolValue may have a corresponding SAT atom which is constrained by formulas. === Done in this patch: === BoolValue is left intact, Formula is just the input type to the SAT solver, and we build formulas as needed to invoke the solver. === Incidental changes to debug string printing: === - variables renamed from B0 etc to V0 etc B0 collides with the names of basic blocks, which is confusing when debugging flow conditions. - debug printing of formulas (Formula and Atom) uses operator<< rather than debugString(), so works with gtest. Therefore moved out of DebugSupport.h - Did the same to Solver::Result, and some helper changes to SolverTest, so that we get useful messages on unit test failures - formulas are now printed as infix expressions on one line, rather than wrapped/indented S-exprs. My experience is that this is easier to scan FCs for small examples, and large ones are unreadable either way. - most of the several debugString() functions for constraints/results are unused, so removed them rather than updating tests. Inlined the one that was actually used into its callsite. Differential Revision: https://reviews.llvm.org/D153366
- Loading branch information
1 parent
61bcaae
commit 2fd614e
Showing
15 changed files
with
587 additions
and
918 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,137 @@ | ||
//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===// | ||
// | ||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. | ||
// See https://llvm.org/LICENSE.txt for license information. | ||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | ||
// | ||
//===----------------------------------------------------------------------===// | ||
|
||
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H | ||
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H | ||
|
||
#include "clang/Basic/LLVM.h" | ||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/DenseMap.h" | ||
#include "llvm/ADT/DenseMapInfo.h" | ||
#include "llvm/ADT/STLFunctionalExtras.h" | ||
#include "llvm/Support/Allocator.h" | ||
#include "llvm/Support/raw_ostream.h" | ||
#include <cassert> | ||
#include <string> | ||
#include <type_traits> | ||
|
||
namespace clang::dataflow { | ||
|
||
/// Identifies an atomic boolean variable such as "V1". | ||
/// | ||
/// This often represents an assertion that is interesting to the analysis but | ||
/// cannot immediately be proven true or false. For example: | ||
/// - V1 may mean "the program reaches this point", | ||
/// - V2 may mean "the parameter was null" | ||
/// | ||
/// We can use these variables in formulas to describe relationships we know | ||
/// to be true: "if the parameter was null, the program reaches this point". | ||
/// We also express hypotheses as formulas, and use a SAT solver to check | ||
/// whether they are consistent with the known facts. | ||
enum class Atom : unsigned {}; | ||
|
||
/// A boolean expression such as "true" or "V1 & !V2". | ||
/// Expressions may refer to boolean atomic variables. These should take a | ||
/// consistent true/false value across the set of formulas being considered. | ||
/// | ||
/// (Formulas are always expressions in terms of boolean variables rather than | ||
/// e.g. integers because our underlying model is SAT rather than e.g. SMT). | ||
/// | ||
/// Simple formulas such as "true" and "V1" are self-contained. | ||
/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or' | ||
/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as | ||
/// trailing objects. | ||
/// For this reason, Formulas are Arena-allocated and over-aligned. | ||
class Formula; | ||
class alignas(const Formula *) Formula { | ||
public: | ||
enum Kind : unsigned { | ||
/// A reference to an atomic boolean variable. | ||
/// We name these e.g. "V3", where 3 == atom identity == Value. | ||
AtomRef, | ||
// FIXME: add const true/false rather than modeling them as variables | ||
|
||
Not, /// True if its only operand is false | ||
|
||
// These kinds connect two operands LHS and RHS | ||
And, /// True if LHS and RHS are both true | ||
Or, /// True if either LHS or RHS is true | ||
Implies, /// True if LHS is false or RHS is true | ||
Equal, /// True if LHS and RHS have the same truth value | ||
}; | ||
Kind kind() const { return FormulaKind; } | ||
|
||
Atom getAtom() const { | ||
assert(kind() == AtomRef); | ||
return static_cast<Atom>(Value); | ||
} | ||
|
||
ArrayRef<const Formula *> operands() const { | ||
return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), | ||
numOperands(kind())); | ||
} | ||
|
||
using AtomNames = llvm::DenseMap<Atom, std::string>; | ||
// Produce a stable human-readable representation of this formula. | ||
// For example: (V3 | !(V1 & V2)) | ||
// If AtomNames is provided, these override the default V0, V1... names. | ||
void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const; | ||
|
||
// Allocate Formulas using Arena rather than calling this function directly. | ||
static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, | ||
ArrayRef<const Formula *> Operands, | ||
unsigned Value = 0); | ||
|
||
private: | ||
Formula() = default; | ||
Formula(const Formula &) = delete; | ||
Formula &operator=(const Formula &) = delete; | ||
|
||
static unsigned numOperands(Kind K) { | ||
switch (K) { | ||
case AtomRef: | ||
return 0; | ||
case Not: | ||
return 1; | ||
case And: | ||
case Or: | ||
case Implies: | ||
case Equal: | ||
return 2; | ||
} | ||
} | ||
|
||
Kind FormulaKind; | ||
// Some kinds of formula have scalar values, e.g. AtomRef's atom number. | ||
unsigned Value; | ||
}; | ||
|
||
// The default names of atoms are V0, V1 etc in order of creation. | ||
inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) { | ||
return OS << 'V' << static_cast<unsigned>(A); | ||
} | ||
inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) { | ||
F.print(OS); | ||
return OS; | ||
} | ||
|
||
} // namespace clang::dataflow | ||
namespace llvm { | ||
template <> struct DenseMapInfo<clang::dataflow::Atom> { | ||
using Atom = clang::dataflow::Atom; | ||
using Underlying = std::underlying_type_t<Atom>; | ||
|
||
static inline Atom getEmptyKey() { return Atom(Underlying(-1)); } | ||
static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); } | ||
static unsigned getHashValue(const Atom &Val) { | ||
return DenseMapInfo<Underlying>::getHashValue(Underlying(Val)); | ||
} | ||
static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; } | ||
}; | ||
} // namespace llvm | ||
#endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.