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 | |
17 | namespace clang::dataflow { |
18 | |
19 | const 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 | |
38 | static 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 | |
57 | void 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 | |