Arena.cpp Source File (original) (raw)

12#include "llvm/Support/Error.h"

13#include

17static std::pair<const Formula *, const Formula *>

19 auto Res = std::make_pair(&LHS, &RHS);

20 if (&RHS < &LHS)

21 std::swap(Res.first, Res.second);

22 return Res;

23}

25template <class Key, class ComputeFunc>

26static const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,

28 auto [It, Inserted] = Cache.try_emplace(std::forward(K));

29 if (Inserted)

31 return *It->second;

32}

35 return cached(AtomRefs, A, [&] {

37 static_cast<unsigned>(A));

38 });

39}

43 if (&LHS == &RHS)

44 return &LHS;

46 return LHS.literal() ? &RHS : &LHS;

48 return RHS.literal() ? &LHS : &RHS;

51 });

52}

56 if (&LHS == &RHS)

57 return &LHS;

59 return LHS.literal() ? &LHS : &RHS;

61 return RHS.literal() ? &RHS : &LHS;

64 });

65}

68 return cached(Nots, &Val, [&] {

75 });

76}

79 return cached(Implies, std::make_pair(&LHS, &RHS), [&] {

80 if (&LHS == &RHS)

88 });

89}

93 if (&LHS == &RHS)

101 });

102}

103

105 auto [It, Inserted] = IntegerLiterals.try_emplace(Value, nullptr);

106

107 if (Inserted)

108 It->second = &create();

109 return *It->second;

110}

111

113 auto [It, Inserted] = FormulaValues.try_emplace(&F);

114 if (Inserted)

116 ? (BoolValue *)&create(F)

117 : &create(F);

118 return *It->second;

119}

120

121namespace {

122const Formula *parse(Arena &A, llvm::StringRef &In) {

123 auto EatSpaces = [&] { In = In.ltrim(' '); };

124 EatSpaces();

125

126 if (In.consume_front("!")) {

127 if (auto *Arg = parse(A, In))

129 return nullptr;

130 }

131

132 if (In.consume_front("(")) {

133 auto *Arg1 = parse(A, In);

134 if (!Arg1)

135 return nullptr;

136

137 EatSpaces();

139 if (In.consume_front("|"))

141 else if (In.consume_front("&"))

143 else if (In.consume_front("=>"))

145 else if (In.consume_front("="))

147 else

148 return nullptr;

149

150 auto *Arg2 = parse(A, In);

151 if (!Arg2)

152 return nullptr;

153

154 EatSpaces();

155 if (!In.consume_front(")"))

156 return nullptr;

157

158 return &(A.*Op)(*Arg1, *Arg2);

159 }

160

161

162

163 if (In.consume_front("V")) {

164 std::underlying_type_t At;

165 if (In.consumeInteger(10, At))

166 return nullptr;

168 }

169

170 if (In.consume_front("true"))

172 if (In.consume_front("false"))

174

175 return nullptr;

176}

177

178class FormulaParseError : public llvm::ErrorInfo {

179 std::string Formula;

180 unsigned Offset;

181

182public:

183 static char ID;

184 FormulaParseError(llvm::StringRef Formula, unsigned Offset)

185 : Formula(Formula), Offset(Offset) {}

186

187 void log(raw_ostream &OS) const override {

188 OS << "bad formula at offset " << Offset << "\n";

189 OS << Formula << "\n";

190 OS.indent(Offset) << "^";

191 }

192

193 std::error_code convertToErrorCode() const override {

194 return std::make_error_code(std::errc::invalid_argument);

195 }

196};

197

198char FormulaParseError::ID = 0;

199

200}

201

203 llvm::StringRef Rest = In;

204 auto *Result = parse(*this, Rest);

205 if ( Result )

206 return llvm::make_error(In, In.size() - Rest.size());

207 Rest = Rest.ltrim();

208 if (!Rest.empty())

209 return llvm::make_error(In, In.size() - Rest.size());

211}

212

213}

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)

ArrayRef< const Formula * > operands() const

@ Equal

True if LHS is false or RHS is true.

@ Implies

True if either LHS or RHS is true.

@ AtomRef

A reference to an atomic boolean variable.

@ Literal

Constant true or false.

@ Or

True if LHS and RHS are both true.

@ And

True if its only operand is false.

static const Formula & create(llvm::BumpPtrAllocator &Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value=0)

Base class for all values computed by abstract interpretation.

Dataflow Directional Tag Classes.

static 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.