12#include "llvm/Support/Error.h"
17static std::pair<const Formula *, const Formula *>
19 auto Res = std::make_pair(&LHS, &RHS);
21 std::swap(Res.first, Res.second);
25template <
class Key,
class ComputeFunc>
28 auto [It, Inserted] =
Cache.try_emplace(std::forward<Key>(K));
35 return cached(AtomRefs, A, [&] {
37 static_cast<unsigned>(A));
46 return LHS.
literal() ? &RHS : &LHS;
48 return RHS.
literal() ? &LHS : &RHS;
59 return LHS.
literal() ? &LHS : &RHS;
61 return RHS.
literal() ? &RHS : &LHS;
68 return cached(Nots, &Val, [&] {
79 return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
105 auto [It, Inserted] = IntegerLiterals.try_emplace(
Value,
nullptr);
108 It->second = &create<IntegerValue>();
113 auto [It, Inserted] = FormulaValues.try_emplace(&F);
116 ? (
BoolValue *)&create<AtomicBoolValue>(F)
117 : &create<FormulaBoolValue>(F);
123 auto EatSpaces = [&] { In = In.ltrim(
' '); };
126 if (In.consume_front(
"!")) {
127 if (
auto *Arg = parse(A, In))
132 if (In.consume_front(
"(")) {
133 auto *Arg1 = parse(A, In);
139 if (In.consume_front(
"|"))
141 else if (In.consume_front(
"&"))
143 else if (In.consume_front(
"=>"))
145 else if (In.consume_front(
"="))
150 auto *Arg2 = parse(A, In);
155 if (!In.consume_front(
")"))
158 return &(A.*Op)(*Arg1, *Arg2);
163 if (
In.consume_front(
"V")) {
164 std::underlying_type_t<Atom> At;
165 if (
In.consumeInteger(10, At))
170 if (
In.consume_front(
"true"))
172 if (
In.consume_front(
"false"))
178class FormulaParseError :
public llvm::ErrorInfo<FormulaParseError> {
184 FormulaParseError(llvm::StringRef Formula,
unsigned Offset)
185 : Formula(Formula), Offset(Offset) {}
187 void log(raw_ostream &OS)
const override {
188 OS <<
"bad formula at offset " << Offset <<
"\n";
189 OS << Formula <<
"\n";
190 OS.indent(Offset) <<
"^";
193 std::error_code convertToErrorCode()
const override {
194 return std::make_error_code(std::errc::invalid_argument);
198char FormulaParseError::ID = 0;
203 llvm::StringRef Rest = In;
204 auto *
Result = parse(*
this, Rest);
206 return llvm::make_error<FormulaParseError>(In, In.size() - Rest.size());
209 return llvm::make_error<FormulaParseError>(In, In.size() - Rest.size());
TypePropertyCache< Private > Cache
The Arena owns the objects that model data within an analysis.
const Formula & makeEquals(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS <=> RHS.
const Formula & makeAtomRef(Atom A)
Returns a formula for the variable A.
IntegerValue & makeIntLiteral(llvm::APInt Value)
Returns a symbolic integer value that models an integer literal equal to Value.
const Formula & makeNot(const Formula &Val)
Returns a formula for the negation of Val.
const Formula & makeOr(const Formula &LHS, const Formula &RHS)
Returns a formula for the disjunction of LHS and RHS.
BoolValue & makeBoolValue(const Formula &)
Creates a BoolValue wrapping a particular formula.
const Formula & makeAnd(const Formula &LHS, const Formula &RHS)
Returns a formula for the conjunction of LHS and RHS.
const Formula & makeImplies(const Formula &LHS, const Formula &RHS)
Returns a formula for LHS => RHS.
const Formula & makeLiteral(bool Value)
Returns a formula for a literal true/false.
llvm::Expected< const Formula & > parseFormula(llvm::StringRef)
Base class for all values computed by abstract interpretation.
Dataflow Directional Tag Classes.
const Formula & cached(llvm::DenseMap< Key, const Formula * > &Cache, Key K, ComputeFunc &&Compute)
Atom
Identifies an atomic boolean variable such as "V1".
static std::pair< const Formula *, const Formula * > canonicalFormulaPair(const Formula &LHS, const Formula &RHS)
if(T->getSizeExpr()) TRY_TO(TraverseStmt(const_cast< Expr * >(T -> getSizeExpr())))
@ Result
The result type of a method or function.