From cb8fe609ba0a9894b207c14da9e88bf311978d4c Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 6 Nov 2023 20:28:43 -0600 Subject: [PATCH] Hook event for proof hints (#873) --- docs/proof-trace.md | 13 +- include/kllvm/codegen/CreateTerm.h | 2 + include/kllvm/codegen/ProofEvent.h | 42 ++++++ lib/codegen/CMakeLists.txt | 1 + lib/codegen/CreateTerm.cpp | 102 ++++++++------- lib/codegen/ProofEvent.cpp | 198 +++++++++++++++++++++++++++++ 6 files changed, 309 insertions(+), 49 deletions(-) create mode 100644 include/kllvm/codegen/ProofEvent.h create mode 100644 lib/codegen/ProofEvent.cpp diff --git a/docs/proof-trace.md b/docs/proof-trace.md index 28f182364..511369380 100644 --- a/docs/proof-trace.md +++ b/docs/proof-trace.md @@ -25,6 +25,15 @@ Here is a BNF styled description of the format delimited_serial_kore := 0xffffffffffffffff serialized_term 0xcccccccccccccccc null_terminated_name := +relative_position := [0-9]+(:[0-9]+)* 0x00 + +function_event := 0xdddddddddddddddd null_terminated_name relative_position + +hook_event := 0xaaaaaaaaaaaaaaaa null_terminated_name hook_arg* 0xbbbbbbbbbbbbbbbb serialized_term + +hook_arg := serialized_term + | function_event + | hook_event variable := null_terminated_name serialized_term 0xcccccccccccccccc @@ -35,7 +44,7 @@ rewrite_trace := rule_ordinal rule_arity variable* delimited_serial_kore initial_config := delimited_serial_kore -proof_trace := initial_config rewrite_trace* +proof_trace := (function_event|hook_event)* initial_config (function_event|hook_event|rewrite_trace)* ``` ## Notes @@ -43,3 +52,5 @@ proof_trace := initial_config rewrite_trace* - The `rule_arity` should be used to determine how many variable substitutions to read - The serialized term for a variable substitution does not begin with the sentinel delimiter. This is because the null terminated variable name can act as the sentinel. +- The `function_event|hook_event`s at the beginning of the proof_trace are related to configuration initialization. +- The `relative_position` is a null terminated string of positive integers separated by `:` (ie. `0:1:1`) diff --git a/include/kllvm/codegen/CreateTerm.h b/include/kllvm/codegen/CreateTerm.h index 38bd73bc5..4ce1a0048 100644 --- a/include/kllvm/codegen/CreateTerm.h +++ b/include/kllvm/codegen/CreateTerm.h @@ -20,6 +20,8 @@ class CreateTerm { bool isAnywhereOwise; std::set staticTerms; + llvm::Value * + alloc_arg(KORECompositePattern *pattern, int idx, std::string locationStack); llvm::Value *createHook( KORECompositePattern *hookAtt, KORECompositePattern *pattern, std::string locationStack = "0"); diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h new file mode 100644 index 000000000..a3238d58d --- /dev/null +++ b/include/kllvm/codegen/ProofEvent.h @@ -0,0 +1,42 @@ +#ifndef PROOF_EVENT_H +#define PROOF_EVENT_H + +#include "kllvm/ast/AST.h" +#include "kllvm/codegen/DecisionParser.h" +#include "kllvm/codegen/Util.h" + +#include "llvm/IR/Instructions.h" + +namespace kllvm { + +void writeUInt64( + llvm::Value *outputFile, llvm::Module *Module, uint64_t value, + llvm::BasicBlock *Block); + +class ProofEvent { +private: + KOREDefinition *Definition; + llvm::BasicBlock *CurrentBlock; + llvm::Module *Module; + llvm::LLVMContext &Ctx; + std::pair + proofBranch(std::string label); + +public: + llvm::BasicBlock *hookEvent_pre(std::string name); + llvm::BasicBlock *hookEvent_post(llvm::Value *val, KORECompositeSort *sort); + llvm::BasicBlock *hookArg(llvm::Value *val, KORECompositeSort *sort); + +public: + ProofEvent( + KOREDefinition *Definition, llvm::BasicBlock *EntryBlock, + llvm::Module *Module) + : Definition(Definition) + , CurrentBlock(EntryBlock) + , Module(Module) + , Ctx(Module->getContext()) { } +}; + +} // namespace kllvm + +#endif // PROOF_EVENT_H diff --git a/lib/codegen/CMakeLists.txt b/lib/codegen/CMakeLists.txt index b43036ae4..9b268348e 100644 --- a/lib/codegen/CMakeLists.txt +++ b/lib/codegen/CMakeLists.txt @@ -6,6 +6,7 @@ add_library(Codegen Decision.cpp DecisionParser.cpp EmitConfigParser.cpp + ProofEvent.cpp Util.cpp ) diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp index 3b205fa6b..3be5dd918 100644 --- a/lib/codegen/CreateTerm.cpp +++ b/lib/codegen/CreateTerm.cpp @@ -1,6 +1,7 @@ #include "kllvm/codegen/CreateTerm.h" #include "kllvm/codegen/CreateStaticTerm.h" #include "kllvm/codegen/Debug.h" +#include "kllvm/codegen/ProofEvent.h" #include "kllvm/codegen/Util.h" #include @@ -311,11 +312,16 @@ sptr termSort(KOREPattern *pattern) { } } -#define ALLOC_ARG(x) \ - createAllocation( \ - pattern->getArguments()[x].get(), \ - fmt::format("{}:{}", locationStack, x)) \ - .first +llvm::Value *CreateTerm::alloc_arg( + KORECompositePattern *pattern, int idx, std::string locationStack) { + KOREPattern *p = pattern->getArguments()[idx].get(); + llvm::Value *ret + = createAllocation(p, fmt::format("{}:{}", locationStack, idx)).first; + auto sort = dynamic_cast(p->getSort().get()); + ProofEvent e(Definition, CurrentBlock, Module); + CurrentBlock = e.hookArg(ret, sort); + return ret; +} std::string escape(std::string str) { std::stringstream os; @@ -336,7 +342,7 @@ llvm::Value *CreateTerm::createHook( std::string name = strPattern->getContents(); if (name == "BOOL.and" || name == "BOOL.andThen") { assert(pattern->getArguments().size() == 2); - llvm::Value *firstArg = ALLOC_ARG(0); + llvm::Value *firstArg = alloc_arg(pattern, 0, locationStack); llvm::BasicBlock *CondBlock = CurrentBlock; llvm::BasicBlock *TrueBlock = llvm::BasicBlock::Create(Ctx, "then", CurrentBlock->getParent()); @@ -344,7 +350,7 @@ llvm::Value *CreateTerm::createHook( Ctx, "hook_BOOL_and", CurrentBlock->getParent()); llvm::BranchInst::Create(TrueBlock, MergeBlock, firstArg, CurrentBlock); CurrentBlock = TrueBlock; - llvm::Value *secondArg = ALLOC_ARG(1); + llvm::Value *secondArg = alloc_arg(pattern, 1, locationStack); llvm::BranchInst::Create(MergeBlock, CurrentBlock); llvm::PHINode *Phi = llvm::PHINode::Create( llvm::Type::getInt1Ty(Ctx), 2, "phi", MergeBlock); @@ -354,7 +360,7 @@ llvm::Value *CreateTerm::createHook( return Phi; } else if (name == "BOOL.or" || name == "BOOL.orElse") { assert(pattern->getArguments().size() == 2); - llvm::Value *firstArg = ALLOC_ARG(0); + llvm::Value *firstArg = alloc_arg(pattern, 0, locationStack); llvm::BasicBlock *CondBlock = CurrentBlock; llvm::BasicBlock *FalseBlock = llvm::BasicBlock::Create(Ctx, "else", CurrentBlock->getParent()); @@ -362,7 +368,7 @@ llvm::Value *CreateTerm::createHook( Ctx, "hook_BOOL_or", CurrentBlock->getParent()); llvm::BranchInst::Create(MergeBlock, FalseBlock, firstArg, CurrentBlock); CurrentBlock = FalseBlock; - llvm::Value *secondArg = ALLOC_ARG(1); + llvm::Value *secondArg = alloc_arg(pattern, 1, locationStack); llvm::BranchInst::Create(MergeBlock, CurrentBlock); llvm::PHINode *Phi = llvm::PHINode::Create( llvm::Type::getInt1Ty(Ctx), 2, "phi", MergeBlock); @@ -372,7 +378,7 @@ llvm::Value *CreateTerm::createHook( return Phi; } else if (name == "BOOL.not") { assert(pattern->getArguments().size() == 1); - llvm::Value *arg = ALLOC_ARG(0); + llvm::Value *arg = alloc_arg(pattern, 0, locationStack); llvm::BinaryOperator *Not = llvm::BinaryOperator::Create( llvm::Instruction::Xor, arg, llvm::ConstantInt::get(llvm::Type::getInt1Ty(Ctx), 1), "hook_BOOL_not", @@ -380,7 +386,7 @@ llvm::Value *CreateTerm::createHook( return Not; } else if (name == "BOOL.implies") { assert(pattern->getArguments().size() == 2); - llvm::Value *firstArg = ALLOC_ARG(0); + llvm::Value *firstArg = alloc_arg(pattern, 0, locationStack); llvm::BasicBlock *CondBlock = CurrentBlock; llvm::BasicBlock *TrueBlock = llvm::BasicBlock::Create(Ctx, "then", CurrentBlock->getParent()); @@ -388,7 +394,7 @@ llvm::Value *CreateTerm::createHook( Ctx, "hook_BOOL_implies", CurrentBlock->getParent()); llvm::BranchInst::Create(TrueBlock, MergeBlock, firstArg, CurrentBlock); CurrentBlock = TrueBlock; - llvm::Value *secondArg = ALLOC_ARG(1); + llvm::Value *secondArg = alloc_arg(pattern, 1, locationStack); llvm::BranchInst::Create(MergeBlock, CurrentBlock); llvm::PHINode *Phi = llvm::PHINode::Create( llvm::Type::getInt1Ty(Ctx), 2, "phi", MergeBlock); @@ -399,23 +405,23 @@ llvm::Value *CreateTerm::createHook( return Phi; } else if (name == "BOOL.ne" || name == "BOOL.xor") { assert(pattern->getArguments().size() == 2); - llvm::Value *firstArg = ALLOC_ARG(0); - llvm::Value *secondArg = ALLOC_ARG(1); + llvm::Value *firstArg = alloc_arg(pattern, 0, locationStack); + llvm::Value *secondArg = alloc_arg(pattern, 1, locationStack); llvm::BinaryOperator *Xor = llvm::BinaryOperator::Create( llvm::Instruction::Xor, firstArg, secondArg, "hook_BOOL_ne", CurrentBlock); return Xor; } else if (name == "BOOL.eq") { assert(pattern->getArguments().size() == 2); - llvm::Value *firstArg = ALLOC_ARG(0); - llvm::Value *secondArg = ALLOC_ARG(1); + llvm::Value *firstArg = alloc_arg(pattern, 0, locationStack); + llvm::Value *secondArg = alloc_arg(pattern, 1, locationStack); llvm::ICmpInst *Eq = new llvm::ICmpInst( *CurrentBlock, llvm::CmpInst::ICMP_EQ, firstArg, secondArg, "hook_BOOL_eq"); return Eq; } else if (name == "KEQUAL.ite") { assert(pattern->getArguments().size() == 3); - llvm::Value *cond = ALLOC_ARG(0); + llvm::Value *cond = alloc_arg(pattern, 0, locationStack); llvm::BasicBlock *TrueBlock = llvm::BasicBlock::Create(Ctx, "then", CurrentBlock->getParent()); llvm::BasicBlock *FalseBlock @@ -424,10 +430,10 @@ llvm::Value *CreateTerm::createHook( Ctx, "hook_KEQUAL_ite", CurrentBlock->getParent()); llvm::BranchInst::Create(TrueBlock, FalseBlock, cond, CurrentBlock); CurrentBlock = TrueBlock; - llvm::Value *trueArg = ALLOC_ARG(1); + llvm::Value *trueArg = alloc_arg(pattern, 1, locationStack); llvm::BasicBlock *NewTrueBlock = CurrentBlock; CurrentBlock = FalseBlock; - llvm::Value *falseArg = ALLOC_ARG(2); + llvm::Value *falseArg = alloc_arg(pattern, 2, locationStack); if (trueArg->getType()->isPointerTy() && !falseArg->getType()->isPointerTy()) { llvm::AllocaInst *AllocCollection @@ -451,7 +457,7 @@ llvm::Value *CreateTerm::createHook( CurrentBlock = MergeBlock; return Phi; } else if (name == "MINT.uvalue") { - llvm::Value *mint = ALLOC_ARG(0); + llvm::Value *mint = alloc_arg(pattern, 0, locationStack); ValueType cat = dynamic_cast( pattern->getConstructor()->getArguments()[0].get()) ->getCategory(Definition); @@ -502,7 +508,7 @@ llvm::Value *CreateTerm::createHook( setDebugLoc(result); return result; } else if (name == "MINT.svalue") { - llvm::Value *mint = ALLOC_ARG(0); + llvm::Value *mint = alloc_arg(pattern, 0, locationStack); ValueType cat = dynamic_cast( pattern->getConstructor()->getArguments()[0].get()) ->getCategory(Definition); @@ -553,7 +559,7 @@ llvm::Value *CreateTerm::createHook( setDebugLoc(result); return result; } else if (name == "MINT.integer") { - llvm::Value *mpz = ALLOC_ARG(0); + llvm::Value *mpz = alloc_arg(pattern, 0, locationStack); ValueType cat = dynamic_cast( pattern->getConstructor()->getSort().get()) ->getCategory(Definition); @@ -597,16 +603,16 @@ llvm::Value *CreateTerm::createHook( return result; } } else if (name == "MINT.neg") { - llvm::Value *in = ALLOC_ARG(0); + llvm::Value *in = alloc_arg(pattern, 0, locationStack); return llvm::BinaryOperator::CreateNeg(in, "hook_MINT_neg", CurrentBlock); } else if (name == "MINT.not") { - llvm::Value *in = ALLOC_ARG(0); + llvm::Value *in = alloc_arg(pattern, 0, locationStack); return llvm::BinaryOperator::CreateNot(in, "hook_MINT_not", CurrentBlock); #define MINT_CMP(hookname, inst) \ } \ else if (name == "MINT." #hookname) { \ - llvm::Value *first = ALLOC_ARG(0); \ - llvm::Value *second = ALLOC_ARG(1); \ + llvm::Value *first = alloc_arg(pattern, 0, locationStack); \ + llvm::Value *second = alloc_arg(pattern, 1, locationStack); \ return new llvm::ICmpInst( \ *CurrentBlock, llvm::CmpInst::inst, first, second, \ "hook_MINT_" #hookname) @@ -623,8 +629,8 @@ llvm::Value *CreateTerm::createHook( #define MINT_BINOP(hookname, inst) \ } \ else if (name == "MINT." #hookname) { \ - llvm::Value *first = ALLOC_ARG(0); \ - llvm::Value *second = ALLOC_ARG(1); \ + llvm::Value *first = alloc_arg(pattern, 0, locationStack); \ + llvm::Value *second = alloc_arg(pattern, 1, locationStack); \ return llvm::BinaryOperator::Create( \ llvm::Instruction::inst, first, second, "hook_MINT_" #hookname, \ CurrentBlock) @@ -673,7 +679,7 @@ llvm::Value *CreateTerm::createFunctionCall( int i = 0; for (auto sort : pattern->getConstructor()->getArguments()) { auto concreteSort = dynamic_cast(sort.get()); - llvm::Value *arg = ALLOC_ARG(i); + llvm::Value *arg = alloc_arg(pattern, i, locationStack); i++; switch (concreteSort->getCategory(Definition).cat) { case SortCategory::Map: @@ -916,11 +922,25 @@ CreateTerm::createAllocation(KOREPattern *pattern, std::string locationStack) { || (symbolDecl->getAttributes().count("anywhere") && !isAnywhereOwise)) { if (symbolDecl->getAttributes().count("hook")) { - return std::make_pair( - createHook( - symbolDecl->getAttributes().at("hook").get(), constructor, - locationStack), - true); + auto sort + = dynamic_cast(constructor->getSort().get()); + auto strPattern + = dynamic_cast(symbolDecl->getAttributes() + .at("hook") + .get() + ->getArguments()[0] + .get()); + std::string name = strPattern->getContents(); + + ProofEvent p1(Definition, CurrentBlock, Module); + CurrentBlock = p1.hookEvent_pre(name); + llvm::Value *val = createHook( + symbolDecl->getAttributes().at("hook").get(), constructor, + locationStack); + ProofEvent p2(Definition, CurrentBlock, Module); + CurrentBlock = p2.hookEvent_post(val, sort); + + return std::make_pair(val, true); } else { std::ostringstream Out; symbol->print(Out, 0, false); @@ -1006,20 +1026,6 @@ void addAbort(llvm::BasicBlock *block, llvm::Module *Module) { new llvm::UnreachableInst(Module->getContext(), block); } -void writeUInt64( - llvm::Value *outputFile, llvm::Module *Module, uint64_t value, - llvm::BasicBlock *Block) { - llvm::CallInst::Create( - getOrInsertFunction( - Module, "writeUInt64ToFile", - llvm::Type::getVoidTy(Module->getContext()), - llvm::Type::getInt8PtrTy(Module->getContext()), - llvm::Type::getInt64Ty(Module->getContext())), - {outputFile, llvm::ConstantInt::get( - llvm::Type::getInt64Ty(Module->getContext()), value)}, - "", Block); -} - bool makeFunction( std::string name, KOREPattern *pattern, KOREDefinition *definition, llvm::Module *Module, bool tailcc, bool bigStep, bool apply, diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp new file mode 100644 index 000000000..e375bf220 --- /dev/null +++ b/lib/codegen/ProofEvent.cpp @@ -0,0 +1,198 @@ +#include "kllvm/codegen/ProofEvent.h" +#include "kllvm/codegen/CreateTerm.h" + +#include "llvm/IR/IRBuilder.h" + +namespace kllvm { + +void writeUInt64( + llvm::Value *outputFile, llvm::Module *Module, uint64_t value, + llvm::BasicBlock *Block) { + llvm::CallInst::Create( + getOrInsertFunction( + Module, "writeUInt64ToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt64Ty(Module->getContext())), + {outputFile, llvm::ConstantInt::get( + llvm::Type::getInt64Ty(Module->getContext()), value)}, + "", Block); +} + +std::pair +ProofEvent::proofBranch(std::string label) { + llvm::Function *f = CurrentBlock->getParent(); + auto ProofOutputFlag = Module->getOrInsertGlobal( + "proof_output", llvm::Type::getInt1Ty(Module->getContext())); + auto proofOutput = new llvm::LoadInst( + llvm::Type::getInt1Ty(Module->getContext()), ProofOutputFlag, + "proof_output", CurrentBlock); + llvm::BasicBlock *TrueBlock + = llvm::BasicBlock::Create(Module->getContext(), "if_" + label, f); + llvm::BasicBlock *MergeBlock + = llvm::BasicBlock::Create(Module->getContext(), "tail_" + label, f); + llvm::BranchInst::Create(TrueBlock, MergeBlock, proofOutput, CurrentBlock); + return std::pair(TrueBlock, MergeBlock); +} + +llvm::BasicBlock *ProofEvent::hookEvent_pre(std::string name) { + auto b = proofBranch("hookpre"); + auto TrueBlock = b.first; + auto MergeBlock = b.second; + auto OutputFileName = Module->getOrInsertGlobal( + "output_file", llvm::Type::getInt8PtrTy(Module->getContext())); + auto ir = new llvm::IRBuilder(TrueBlock); + auto outputFile = new llvm::LoadInst( + llvm::Type::getInt8PtrTy(Module->getContext()), OutputFileName, "output", + TrueBlock); + + auto nameptr = ir->CreateGlobalStringPtr(name, "", 0, Module); + + writeUInt64(outputFile, Module, 0xaaaaaaaaaaaaaaaa, TrueBlock); + ir->CreateCall( + getOrInsertFunction( + Module, "printVariableToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, nameptr}); + + llvm::BranchInst::Create(MergeBlock, TrueBlock); + + // Some places will try to use llvm::Instruction::insertAfter on the back of + // the MergeBlock. + // If the MergeBlock has no instructions, this has resulted in a segfault when + // printing the IR. Adding an effective nop prevents this. + llvm::BinaryOperator::Create( + llvm::Instruction::Add, + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + "nop", MergeBlock); + + return CurrentBlock = MergeBlock; +} + +llvm::BasicBlock * +ProofEvent::hookEvent_post(llvm::Value *val, KORECompositeSort *sort) { + auto b = proofBranch("hookpost"); + auto TrueBlock = b.first; + auto MergeBlock = b.second; + auto OutputFileName = Module->getOrInsertGlobal( + "output_file", llvm::Type::getInt8PtrTy(Module->getContext())); + auto ir = new llvm::IRBuilder(TrueBlock); + auto outputFile = new llvm::LoadInst( + llvm::Type::getInt8PtrTy(Module->getContext()), OutputFileName, "output", + TrueBlock); + + auto cat = sort->getCategory(Definition); + std::ostringstream Out; + sort->print(Out); + auto sortptr = ir->CreateGlobalStringPtr(Out.str(), "", 0, Module); + + writeUInt64(outputFile, Module, 0xbbbbbbbbbbbbbbbb, TrueBlock); + if (cat.cat == SortCategory::Symbol || cat.cat == SortCategory::Variable) { + ir->CreateCall( + getOrInsertFunction( + Module, "serializeTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + getValueType({SortCategory::Symbol, 0}, Module), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } else if (val->getType()->isIntegerTy()) { + val = ir->CreateIntToPtr( + val, llvm::Type::getInt8PtrTy(Module->getContext())); + ir->CreateCall( + getOrInsertFunction( + Module, "serializeRawTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } else { + val = ir->CreatePointerCast( + val, llvm::Type::getInt8PtrTy(Module->getContext())); + ir->CreateCall( + getOrInsertFunction( + Module, "serializeRawTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } + + llvm::BranchInst::Create(MergeBlock, TrueBlock); + + llvm::BinaryOperator::Create( + llvm::Instruction::Add, + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + "nop", MergeBlock); + + return CurrentBlock = MergeBlock; +} + +llvm::BasicBlock * +ProofEvent::hookArg(llvm::Value *val, KORECompositeSort *sort) { + auto b = proofBranch("hookarg"); + auto TrueBlock = b.first; + auto MergeBlock = b.second; + auto OutputFileName = Module->getOrInsertGlobal( + "output_file", llvm::Type::getInt8PtrTy(Module->getContext())); + auto ir = new llvm::IRBuilder(TrueBlock); + auto outputFile = new llvm::LoadInst( + llvm::Type::getInt8PtrTy(Module->getContext()), OutputFileName, "output", + TrueBlock); + + auto cat = sort->getCategory(Definition); + std::ostringstream Out; + sort->print(Out); + auto sortptr = ir->CreateGlobalStringPtr(Out.str(), "", 0, Module); + + if (cat.cat == SortCategory::Symbol || cat.cat == SortCategory::Variable) { + ir->CreateCall( + getOrInsertFunction( + Module, "serializeTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + getValueType({SortCategory::Symbol, 0}, Module), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } else if (val->getType()->isIntegerTy()) { + val = ir->CreateIntToPtr( + val, llvm::Type::getInt8PtrTy(Module->getContext())); + ir->CreateCall( + getOrInsertFunction( + Module, "serializeRawTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } else { + val = ir->CreatePointerCast( + val, llvm::Type::getInt8PtrTy(Module->getContext())); + ir->CreateCall( + getOrInsertFunction( + Module, "serializeRawTermToFile", + llvm::Type::getVoidTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext()), + llvm::Type::getInt8PtrTy(Module->getContext())), + {outputFile, val, sortptr}); + } + + llvm::BranchInst::Create(MergeBlock, TrueBlock); + + llvm::BinaryOperator::Create( + llvm::Instruction::Add, + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + llvm::ConstantInt::get(llvm::Type::getInt8Ty(Module->getContext()), 0), + "nop", MergeBlock); + + return CurrentBlock = MergeBlock; +} + +} // namespace kllvm