1 //===- Formula.cpp ----------------------------------------------*- C++ -*-===//
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
7 //===----------------------------------------------------------------------===//
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"
16 #include <type_traits>
18 namespace clang::dataflow
{
20 const Formula
&Formula::create(llvm::BumpPtrAllocator
&Alloc
, Kind K
,
21 ArrayRef
<const Formula
*> Operands
,
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(sizeof(Formula
) +
27 Operands
.size() * sizeof(Operands
.front()),
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(Operands
, reinterpret_cast<const Formula
**>(Result
+ 1));
39 static llvm::StringLiteral
sigil(Formula::Kind K
) {
41 case Formula::AtomRef
:
42 case Formula::Literal
:
50 case Formula::Implies
:
55 llvm_unreachable("unhandled formula kind");
58 void Formula::print(llvm::raw_ostream
&OS
, const AtomNames
*Names
) const {
59 if (Names
&& kind() == AtomRef
)
60 if (auto It
= Names
->find(getAtom()); It
!= Names
->end()) {
65 switch (numOperands(kind())) {
72 OS
<< (literal() ? "true" : "false");
75 llvm_unreachable("unhandled formula kind");
80 operands()[0]->print(OS
, Names
);
84 operands()[0]->print(OS
, Names
);
86 operands()[1]->print(OS
, Names
);
90 llvm_unreachable("unhandled formula arity");
94 } // namespace clang::dataflow