154 lines · cpp
1//===- FormulaSerialization.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-exception6//7//===----------------------------------------------------------------------===//8 9#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"10#include "clang/Analysis/FlowSensitive/Arena.h"11#include "clang/Analysis/FlowSensitive/Formula.h"12#include "clang/Basic/LLVM.h"13#include "llvm/ADT/DenseMap.h"14#include "llvm/ADT/STLExtras.h"15#include "llvm/ADT/StringRef.h"16#include "llvm/Support/Allocator.h"17#include "llvm/Support/Error.h"18#include "llvm/Support/ErrorHandling.h"19#include <cassert>20 21namespace clang::dataflow {22 23// Returns the leading indicator of operation formulas. `AtomRef` and `Literal`24// are handled differently.25static char compactSigil(Formula::Kind K) {26 switch (K) {27 case Formula::AtomRef:28 case Formula::Literal:29 // No sigil.30 return '\0';31 case Formula::Not:32 return '!';33 case Formula::And:34 return '&';35 case Formula::Or:36 return '|';37 case Formula::Implies:38 return '>';39 case Formula::Equal:40 return '=';41 }42 llvm_unreachable("unhandled formula kind");43}44 45void serializeFormula(const Formula &F, llvm::raw_ostream &OS) {46 switch (Formula::numOperands(F.kind())) {47 case 0:48 switch (F.kind()) {49 case Formula::AtomRef:50 OS << F.getAtom();51 break;52 case Formula::Literal:53 OS << (F.literal() ? 'T' : 'F');54 break;55 default:56 llvm_unreachable("unhandled formula kind");57 }58 break;59 case 1:60 OS << compactSigil(F.kind());61 serializeFormula(*F.operands()[0], OS);62 break;63 case 2:64 OS << compactSigil(F.kind());65 serializeFormula(*F.operands()[0], OS);66 serializeFormula(*F.operands()[1], OS);67 break;68 default:69 llvm_unreachable("unhandled formula arity");70 }71}72 73static llvm::Expected<const Formula *>74parsePrefix(llvm::StringRef &Str, Arena &A,75 llvm::DenseMap<unsigned, Atom> &AtomMap) {76 if (Str.empty())77 return llvm::createStringError(llvm::inconvertibleErrorCode(),78 "unexpected end of input");79 80 char Prefix = Str[0];81 Str = Str.drop_front();82 83 switch (Prefix) {84 case 'T':85 return &A.makeLiteral(true);86 case 'F':87 return &A.makeLiteral(false);88 case 'V': {89 unsigned AtomID;90 if (Str.consumeInteger(10, AtomID))91 return llvm::createStringError(llvm::inconvertibleErrorCode(),92 "expected atom id");93 auto [It, Inserted] = AtomMap.try_emplace(AtomID, Atom());94 if (Inserted)95 It->second = A.makeAtom();96 return &A.makeAtomRef(It->second);97 }98 case '!': {99 auto OperandOrErr = parsePrefix(Str, A, AtomMap);100 if (!OperandOrErr)101 return OperandOrErr.takeError();102 return &A.makeNot(**OperandOrErr);103 }104 case '&':105 case '|':106 case '>':107 case '=': {108 auto LeftOrErr = parsePrefix(Str, A, AtomMap);109 if (!LeftOrErr)110 return LeftOrErr.takeError();111 112 auto RightOrErr = parsePrefix(Str, A, AtomMap);113 if (!RightOrErr)114 return RightOrErr.takeError();115 116 const Formula &LHS = **LeftOrErr;117 const Formula &RHS = **RightOrErr;118 119 switch (Prefix) {120 case '&':121 return &A.makeAnd(LHS, RHS);122 case '|':123 return &A.makeOr(LHS, RHS);124 case '>':125 return &A.makeImplies(LHS, RHS);126 case '=':127 return &A.makeEquals(LHS, RHS);128 default:129 llvm_unreachable("unexpected binary op");130 }131 }132 default:133 return llvm::createStringError(llvm::inconvertibleErrorCode(),134 "unexpected prefix character: %c", Prefix);135 }136}137 138llvm::Expected<const Formula *>139parseFormula(llvm::StringRef Str, Arena &A,140 llvm::DenseMap<unsigned, Atom> &AtomMap) {141 size_t OriginalSize = Str.size();142 llvm::Expected<const Formula *> F = parsePrefix(Str, A, AtomMap);143 if (!F)144 return F.takeError();145 if (!Str.empty())146 return llvm::createStringError(llvm::inconvertibleErrorCode(),147 ("unexpected suffix of length: " +148 llvm::Twine(Str.size() - OriginalSize))149 .str());150 return F;151}152 153} // namespace clang::dataflow154