1//===- FormulaSerialization.cpp ---------------------------------*- C++ -*-===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8
9#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"
10#include "clang/Analysis/FlowSensitive/Arena.h"
11#include "clang/Analysis/FlowSensitive/Formula.h"
12#include "clang/Basic/LLVM.h"
13#include "llvm/ADT/DenseMap.h"
14#include "llvm/ADT/StringRef.h"
15#include "llvm/Support/Error.h"
16#include "llvm/Support/ErrorHandling.h"
17#include <cassert>
18#include <cstddef>
19#include <stack>
20#include <vector>
21
22namespace clang::dataflow {
23
24// Returns the leading indicator of operation formulas. `AtomRef` and `Literal`
25// are handled differently.
26static char compactSigil(Formula::Kind K) {
27 switch (K) {
28 case Formula::AtomRef:
29 case Formula::Literal:
30 // No sigil.
31 return '\0';
32 case Formula::Not:
33 return '!';
34 case Formula::And:
35 return '&';
36 case Formula::Or:
37 return '|';
38 case Formula::Implies:
39 return '>';
40 case Formula::Equal:
41 return '=';
42 }
43 llvm_unreachable("unhandled formula kind");
44}
45
46// Avoids recursion to avoid stack overflows from very large formulas.
47void serializeFormula(const Formula &F, llvm::raw_ostream &OS) {
48 std::stack<const Formula *> WorkList;
49 WorkList.push(x: &F);
50 while (!WorkList.empty()) {
51 const Formula *Current = WorkList.top();
52 WorkList.pop();
53 switch (Formula::numOperands(K: Current->kind())) {
54 case 0:
55 switch (Current->kind()) {
56 case Formula::AtomRef:
57 OS << Current->getAtom();
58 break;
59 case Formula::Literal:
60 OS << (Current->literal() ? 'T' : 'F');
61 break;
62 default:
63 llvm_unreachable("unhandled formula kind");
64 }
65 break;
66 case 1:
67 OS << compactSigil(K: Current->kind());
68 WorkList.push(x: Current->operands()[0]);
69 break;
70 case 2:
71 OS << compactSigil(K: Current->kind());
72 WorkList.push(x: Current->operands()[1]);
73 WorkList.push(x: Current->operands()[0]);
74 break;
75 default:
76 llvm_unreachable("unhandled formula arity");
77 }
78 }
79}
80
81struct Operation {
82 Operation(Formula::Kind Kind) : Kind(Kind) {}
83 const Formula::Kind Kind;
84 const unsigned ExpectedNumOperands = Formula::numOperands(K: Kind);
85 std::vector<const Formula *> Operands;
86};
87
88// Avoids recursion to avoid stack overflows from very large formulas.
89static llvm::Expected<const Formula *>
90parseFormulaInternal(llvm::StringRef &Str, Arena &A,
91 llvm::DenseMap<unsigned, Atom> &AtomMap) {
92 std::stack<Operation> ActiveOperations;
93
94 while (true) {
95 if (ActiveOperations.empty() ||
96 ActiveOperations.top().ExpectedNumOperands >
97 ActiveOperations.top().Operands.size()) {
98 if (Str.empty()) {
99 return llvm::createStringError(EC: llvm::inconvertibleErrorCode(),
100 S: "unexpected end of input");
101 }
102 char Prefix = Str[0];
103 Str = Str.drop_front();
104
105 switch (Prefix) {
106 // Terminals
107 case 'T':
108 case 'F':
109 case 'V': {
110 const Formula *TerminalFormula;
111 switch (Prefix) {
112 case 'T':
113 TerminalFormula = &A.makeLiteral(Value: true);
114 break;
115 case 'F':
116 TerminalFormula = &A.makeLiteral(Value: false);
117 break;
118 case 'V': {
119 unsigned AtomID;
120 if (Str.consumeInteger(Radix: 10, Result&: AtomID))
121 return llvm::createStringError(EC: llvm::inconvertibleErrorCode(),
122 S: "expected atom id");
123 auto [It, Inserted] = AtomMap.try_emplace(Key: AtomID, Args: Atom());
124 if (Inserted)
125 It->second = A.makeAtom();
126 TerminalFormula = &A.makeAtomRef(A: It->second);
127 break;
128 }
129 default:
130 llvm_unreachable("unexpected terminal character");
131 }
132 if (ActiveOperations.empty()) {
133 return TerminalFormula;
134 }
135 Operation *Op = &ActiveOperations.top();
136 Op->Operands.push_back(x: TerminalFormula);
137 } break;
138 case '!':
139 ActiveOperations.emplace(args: Formula::Kind::Not);
140 break;
141 case '&':
142 ActiveOperations.emplace(args: Formula::Kind::And);
143 break;
144 case '|':
145 ActiveOperations.emplace(args: Formula::Kind::Or);
146 break;
147 case '>':
148 ActiveOperations.emplace(args: Formula::Kind::Implies);
149 break;
150 case '=':
151 ActiveOperations.emplace(args: Formula::Kind::Equal);
152 break;
153 default:
154 return llvm::createStringError(EC: llvm::inconvertibleErrorCode(),
155 Fmt: "unexpected prefix character: %c",
156 Vals: Prefix);
157 }
158 } else if (!ActiveOperations.empty() &&
159 ActiveOperations.top().ExpectedNumOperands ==
160 ActiveOperations.top().Operands.size()) {
161 Operation *Op = &ActiveOperations.top();
162 const Formula *OpFormula = nullptr;
163 switch (Op->Kind) {
164 case Formula::Kind::Not:
165 OpFormula = &A.makeNot(Val: *Op->Operands[0]);
166 break;
167 case Formula::Kind::And:
168 OpFormula = &A.makeAnd(LHS: *Op->Operands[0], RHS: *Op->Operands[1]);
169 break;
170 case Formula::Kind::Or:
171 OpFormula = &A.makeOr(LHS: *Op->Operands[0], RHS: *Op->Operands[1]);
172 break;
173 case Formula::Kind::Implies:
174 OpFormula = &A.makeImplies(LHS: *Op->Operands[0], RHS: *Op->Operands[1]);
175 break;
176 case Formula::Kind::Equal:
177 OpFormula = &A.makeEquals(LHS: *Op->Operands[0], RHS: *Op->Operands[1]);
178 break;
179 default:
180 return llvm::createStringError(EC: llvm::inconvertibleErrorCode(),
181 Fmt: "only unary and binary operations are "
182 "expected, but got Formula::Kind %u",
183 Vals: Op->Kind);
184 }
185 ActiveOperations.pop();
186 if (ActiveOperations.empty())
187 return OpFormula;
188 Op = &ActiveOperations.top();
189 Op->Operands.push_back(x: OpFormula);
190 } else {
191 llvm_unreachable(
192 "we should never have added more operands than expected");
193 }
194 }
195}
196
197llvm::Expected<const Formula *>
198parseFormula(llvm::StringRef Str, Arena &A,
199 llvm::DenseMap<unsigned, Atom> &AtomMap) {
200 size_t OriginalSize = Str.size();
201 llvm::Expected<const Formula *> F = parseFormulaInternal(Str, A, AtomMap);
202 if (!F)
203 return F.takeError();
204 if (!Str.empty())
205 return llvm::createStringError(EC: llvm::inconvertibleErrorCode(),
206 S: ("unexpected suffix of length: " +
207 llvm::Twine(Str.size() - OriginalSize))
208 .str());
209 return F;
210}
211
212} // namespace clang::dataflow
213