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