FormulaSerialization.cpp Source File (original) (raw)

13#include "llvm/ADT/DenseMap.h"

14#include "llvm/ADT/STLExtras.h"

15#include "llvm/ADT/StringRef.h"

16#include "llvm/Support/Allocator.h"

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

18#include "llvm/Support/ErrorHandling.h"

19#include

26 switch (K) {

30 return '\0';

32 return '!';

34 return '&';

36 return '|';

38 return '>';

40 return '=';

41 }

42 llvm_unreachable("unhandled formula kind");

43}

47 case 0:

48 switch (F.kind()) {

51 break;

53 OS << (F.literal() ? 'T' : 'F');

54 break;

55 default:

56 llvm_unreachable("unhandled formula kind");

57 }

58 break;

59 case 1:

62 break;

63 case 2:

67 break;

68 default:

69 llvm_unreachable("unhandled formula arity");

70 }

71}

75 llvm::DenseMap<unsigned, Atom> &AtomMap) {

76 if (Str.empty())

77 return llvm::createStringError(llvm::inconvertibleErrorCode(),

78 "unexpected end of input");

80 char Prefix = Str[0];

81 Str = Str.drop_front();

83 switch (Prefix) {

84 case 'T':

86 case 'F':

88 case 'V': {

89 unsigned AtomID;

90 if (Str.consumeInteger(10, AtomID))

91 return llvm::createStringError(llvm::inconvertibleErrorCode(),

92 "expected atom id");

93 auto [It, Inserted] = AtomMap.try_emplace(AtomID, Atom());

94 if (Inserted)

97 }

98 case '!': {

99 auto OperandOrErr = parsePrefix(Str, A, AtomMap);

100 if (!OperandOrErr)

101 return OperandOrErr.takeError();

102 return &A.makeNot(**OperandOrErr);

103 }

104 case '&':

105 case '|':

106 case '>':

107 case '=': {

108 auto LeftOrErr = parsePrefix(Str, A, AtomMap);

109 if (!LeftOrErr)

110 return LeftOrErr.takeError();

111

112 auto RightOrErr = parsePrefix(Str, A, AtomMap);

113 if (!RightOrErr)

114 return RightOrErr.takeError();

115

116 const Formula &LHS = **LeftOrErr;

117 const Formula &RHS = **RightOrErr;

118

119 switch (Prefix) {

120 case '&':

121 return &A.makeAnd(LHS, RHS);

122 case '|':

123 return &A.makeOr(LHS, RHS);

124 case '>':

126 case '=':

128 default:

129 llvm_unreachable("unexpected binary op");

130 }

131 }

132 default:

133 return llvm::createStringError(llvm::inconvertibleErrorCode(),

134 "unexpected prefix character: %c", Prefix);

135 }

136}

137

140 llvm::DenseMap<unsigned, Atom> &AtomMap) {

141 size_t OriginalSize = Str.size();

143 if (!F)

144 return F.takeError();

145 if (!Str.empty())

146 return llvm::createStringError(llvm::inconvertibleErrorCode(),

147 ("unexpected suffix of length: " +

148 llvm::Twine(Str.size() - OriginalSize))

149 .str());

150 return F;

151}

152

153}

Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.

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.

Atom makeAtom()

Returns a new atomic boolean variable, distinct from any other.

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.

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.

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 unsigned numOperands(Kind K)

Count of operands (sub-formulas) associated with Formulas of kind K.

Dataflow Directional Tag Classes.

static llvm::Expected< const Formula * > parsePrefix(llvm::StringRef &Str, Arena &A, llvm::DenseMap< unsigned, Atom > &AtomMap)

Definition FormulaSerialization.cpp:74

Atom

Identifies an atomic boolean variable such as "V1".

void serializeFormula(const Formula &F, llvm::raw_ostream &OS)

Prints F to OS in a compact format, optimized for easy parsing (deserialization) rather than human us...

Definition FormulaSerialization.cpp:45

llvm::Expected< const Formula * > parseFormula(llvm::StringRef Str, Arena &A, llvm::DenseMap< unsigned, Atom > &AtomMap)

Parses Str to build a serialized Formula.

Definition FormulaSerialization.cpp:139

static char compactSigil(Formula::Kind K)

Definition FormulaSerialization.cpp:25