1//===- Formula.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/Formula.h"
10#include "clang/Basic/LLVM.h"
11#include "llvm/ADT/STLExtras.h"
12#include "llvm/ADT/StringRef.h"
13#include "llvm/Support/Allocator.h"
14#include "llvm/Support/ErrorHandling.h"
15#include <cassert>
16
17namespace clang::dataflow {
18
19const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
20 ArrayRef<const Formula *> Operands,
21 unsigned Value) {
22 assert(Operands.size() == numOperands(K));
23 if (Value != 0) // Currently, formulas have values or operands, not both.
24 assert(numOperands(K) == 0);
25 void *Mem = Alloc.Allocate(Size: sizeof(Formula) +
26 Operands.size() * sizeof(Operands.front()),
27 Alignment: alignof(Formula));
28 Formula *Result = new (Mem) Formula();
29 Result->FormulaKind = K;
30 Result->Value = Value;
31 // Operands are stored as `const Formula *`s after the formula itself.
32 // We don't need to construct an object as pointers are trivial types.
33 // Formula is alignas(const Formula *), so alignment is satisfied.
34 llvm::copy(Range&: Operands, Out: reinterpret_cast<const Formula **>(Result + 1));
35 return *Result;
36}
37
38static llvm::StringLiteral sigil(Formula::Kind K) {
39 switch (K) {
40 case Formula::AtomRef:
41 case Formula::Literal:
42 return "";
43 case Formula::Not:
44 return "!";
45 case Formula::And:
46 return " & ";
47 case Formula::Or:
48 return " | ";
49 case Formula::Implies:
50 return " => ";
51 case Formula::Equal:
52 return " = ";
53 }
54 llvm_unreachable("unhandled formula kind");
55}
56
57void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
58 if (Names && kind() == AtomRef)
59 if (auto It = Names->find(Val: getAtom()); It != Names->end()) {
60 OS << It->second;
61 return;
62 }
63
64 switch (numOperands(K: kind())) {
65 case 0:
66 switch (kind()) {
67 case AtomRef:
68 OS << getAtom();
69 break;
70 case Literal:
71 OS << (literal() ? "true" : "false");
72 break;
73 default:
74 llvm_unreachable("unhandled formula kind");
75 }
76 break;
77 case 1:
78 OS << sigil(K: kind());
79 operands()[0]->print(OS, Names);
80 break;
81 case 2:
82 OS << '(';
83 operands()[0]->print(OS, Names);
84 OS << sigil(K: kind());
85 operands()[1]->print(OS, Names);
86 OS << ')';
87 break;
88 default:
89 llvm_unreachable("unhandled formula arity");
90 }
91}
92
93} // namespace clang::dataflow
94