SimplifyConstraints.cpp Source File (original) (raw)

10#include "llvm/ADT/EquivalenceClasses.h"

13namespace dataflow {

17static const Formula &

19 const llvm::DenseMap<Atom, const Formula *> &Substitutions,

21 switch (F.kind()) {

23 if (auto iter = Substitutions.find(F.getAtom());

24 iter != Substitutions.end())

25 return *iter->second;

26 return F;

28 return F;

44 }

45 llvm_unreachable("Unknown formula kind");

46}

52static llvm::DenseSet

54 llvm::EquivalenceClasses &EquivalentAtoms) {

55 llvm::DenseSet Result;

58 Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));

61}

67 llvm::EquivalenceClasses::iterator LeaderIt) {

69 for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);

70 MemberIt != EquivalentAtoms.member_end(); ++MemberIt)

71 Result.push_back(*MemberIt);

73}

77 auto contradiction = [&]() {

78 Constraints.clear();

79 Constraints.insert(&arena.makeLiteral(false));

80 };

82 llvm::EquivalenceClasses EquivalentAtoms;

83 llvm::DenseSet TrueAtoms;

84 llvm::DenseSet FalseAtoms;

86 while (true) {

87 for (const auto *Constraint : Constraints) {

88 switch (Constraint->kind()) {

90 TrueAtoms.insert(Constraint->getAtom());

91 break;

94 FalseAtoms.insert(Constraint->operands()[0]->getAtom());

95 break;

100 EquivalentAtoms.unionSets(operands[0]->getAtom(),

101 operands[1]->getAtom());

102 }

103 break;

104 }

105 default:

106 break;

107 }

108 }

109

112

113 llvm::DenseMap<Atom, const Formula *> Substitutions;

114 for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {

115 Atom TheAtom = It->getData();

116 Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);

117 if (TrueAtoms.contains(Leader)) {

118 if (FalseAtoms.contains(Leader)) {

119 contradiction();

120 return;

121 }

122 Substitutions.insert({TheAtom, &arena.makeLiteral(true)});

123 } else if (FalseAtoms.contains(Leader)) {

124 Substitutions.insert({TheAtom, &arena.makeLiteral(false)});

125 } else if (TheAtom != Leader) {

126 Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});

127 }

128 }

129

130 llvm::SetVector<const Formula *> NewConstraints;

131 for (const auto *Constraint : Constraints) {

132 const Formula &NewConstraint =

133 substitute(*Constraint, Substitutions, arena);

134 if (NewConstraint.isLiteral(true))

135 continue;

136 if (NewConstraint.isLiteral(false)) {

137 contradiction();

138 return;

139 }

141 NewConstraints.insert(NewConstraint.operands()[0]);

142 NewConstraints.insert(NewConstraint.operands()[1]);

143 continue;

144 }

145 NewConstraints.insert(&NewConstraint);

146 }

147

148 if (NewConstraints == Constraints)

149 break;

150 Constraints = std::move(NewConstraints);

151 }

152

153 if (Info) {

154 for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();

155 It != End; ++It) {

156 if (!It->isLeader())

157 continue;

158 Atom At = *EquivalentAtoms.findLeader(It);

159 if (TrueAtoms.contains(At) || FalseAtoms.contains(At))

160 continue;

163 if (Atoms.size() == 1)

164 continue;

165 std::sort(Atoms.begin(), Atoms.end());

167 }

168 for (Atom At : TrueAtoms)

170 EquivalentAtoms, EquivalentAtoms.findValue(At)));

172 for (Atom At : FalseAtoms)

174 EquivalentAtoms, EquivalentAtoms.findValue(At)));

176 }

177}

178

179}

180}

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.

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

bool isLiteral(bool b) 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 llvm::SmallVector< Atom > atomsInEquivalenceClass(const llvm::EquivalenceClasses< Atom > &EquivalentAtoms, llvm::EquivalenceClasses< Atom >::iterator LeaderIt)

Atom

Identifies an atomic boolean variable such as "V1".

void simplifyConstraints(llvm::SetVector< const Formula * > &Constraints, Arena &arena, SimplifyConstraintsInfo *Info=nullptr)

Simplifies a set of constraints (implicitly connected by "and") in a way that does not change satisfi...

static llvm::DenseSet< Atom > projectToLeaders(const llvm::DenseSet< Atom > &Atoms, llvm::EquivalenceClasses< Atom > &EquivalentAtoms)

static const Formula & substitute(const Formula &F, const llvm::DenseMap< Atom, const Formula * > &Substitutions, Arena &arena)

The JSON file list parser is used to communicate input to InstallAPI.

@ Result

The result type of a method or function.

Information on the way a set of constraints was simplified.

llvm::SmallVector< Atom > TrueAtoms

Atoms that the original constraints imply must be true.

llvm::SmallVector< llvm::SmallVector< Atom > > EquivalentAtoms

List of equivalence classes of atoms.

llvm::SmallVector< Atom > FalseAtoms

Atoms that the original constraints imply must be false.