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 18 namespace clang::dataflow { 19 20 const 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(sizeof(Formula) + 27 Operands.size() * sizeof(Operands.front()), 28 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(Operands, reinterpret_cast<const Formula **>(Result + 1)); 36 return *Result; 37 } 38 39 static 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 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()) { 61 OS << It->second; 62 return; 63 } 64 65 switch (numOperands(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(kind()); 80 operands()[0]->print(OS, Names); 81 break; 82 case 2: 83 OS << '('; 84 operands()[0]->print(OS, Names); 85 OS << sigil(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