Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor generation of proof hint "rule applied" event #862

Closed
wants to merge 6 commits into from
Closed

Refactor generation of proof hint "rule applied" event #862

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bfac04e
WIP
gtrepta Oct 11, 2023
669a3b1
WIP
gtrepta Oct 11, 2023
540b453
Merge branch 'master' into hint_emitPlace
Baltoli Oct 17, 2023
abaf477
Merge branch 'master' into hint_emitPlace
Baltoli Oct 27, 2023
c200aca
Merge branch 'master' into hint_emitPlace
Baltoli Nov 1, 2023
3ae3fe9
Merge branch 'master' into hint_emitPlace
Baltoli Nov 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 0 additions & 56 deletions lib/codegen/CreateTerm.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1130,62 +1130,6 @@ bool makeFunction(
auto outputFile = new llvm::LoadInst(
llvm::Type::getInt8PtrTy(Module->getContext()), OutputFileName,
"output", TrueBlock);
writeUInt64(outputFile, Module, axiom->getOrdinal(), TrueBlock);
writeUInt64(
outputFile, Module, applyRule->arg_end() - applyRule->arg_begin(),
TrueBlock);
for (auto entry = subst.begin(); entry != subst.end(); ++entry) {
auto key = entry->getKey();
auto val = entry->getValue();
auto var = vars[key.str()];
auto sort = dynamic_cast<KORECompositeSort *>(var->getSort().get());
auto cat = sort->getCategory(definition);
std::ostringstream Out;
sort->print(Out);
auto sortptr = ir->CreateGlobalStringPtr(Out.str(), "", 0, Module);
auto varname = ir->CreateGlobalStringPtr(key, "", 0, Module);
ir->CreateCall(
getOrInsertFunction(
Module, "printVariableToFile",
llvm::Type::getVoidTy(Module->getContext()),
llvm::Type::getInt8PtrTy(Module->getContext()),
llvm::Type::getInt8PtrTy(Module->getContext())),
{outputFile, varname});
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});
}
writeUInt64(outputFile, Module, 0xcccccccccccccccc, TrueBlock);
}

writeUInt64(outputFile, Module, 0xffffffffffffffff, TrueBlock);
ir->CreateCall(
Expand Down
116 changes: 112 additions & 4 deletions lib/codegen/Decision.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
#include <llvm/IR/DerivedTypes.h>
#include <llvm/IR/Function.h>
#include <llvm/IR/GlobalVariable.h>
#include <llvm/IR/IRBuilder.h>
#include <llvm/IR/InstrTypes.h>
#include <llvm/IR/Instruction.h>
#include <llvm/IR/Instructions.h>
Expand Down Expand Up @@ -557,10 +558,117 @@ void LeafNode::codegen(Decision *d) {
types.push_back(val->getType());
}
auto type = getParamType(d->Cat, d->Module);
auto Call = llvm::CallInst::Create(
getOrInsertFunction(
d->Module, name, llvm::FunctionType::get(type, types, false)),
args, "", d->CurrentBlock);

llvm::Module *Module = d->Module;
llvm::BasicBlock *CurrentBlock = d->CurrentBlock;
llvm::Function *applyRule = getOrInsertFunction(
d->Module, name, llvm::FunctionType::get(type, types, false));

auto ProofOutputFlag = Module->getOrInsertGlobal(
"proof_output", llvm::Type::getInt1Ty(Module->getContext()));
auto OutputFileName = Module->getOrInsertGlobal(
"output_file", llvm::Type::getInt8PtrTy(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", CurrentBlock->getParent());
llvm::BasicBlock *MergeBlock = llvm::BasicBlock::Create(
Module->getContext(), "tail", CurrentBlock->getParent());
llvm::BranchInst::Create(TrueBlock, MergeBlock, proofOutput, CurrentBlock);
auto ir = new llvm::IRBuilder(TrueBlock);

auto outputFile = new llvm::LoadInst(
llvm::Type::getInt8PtrTy(Module->getContext()), OutputFileName, "output",
TrueBlock);

size_t ordinal = std::stoll(name.substr(11));
KOREDefinition *definition = d->Definition;
KOREAxiomDeclaration *axiom = definition->getAxiomByOrdinal(ordinal);
std::map<std::string, KOREVariablePattern *> vars;
for (KOREPattern *lhs : axiom->getLeftHandSide()) {
lhs->markVariables(vars);
}
axiom->getRightHandSide()->markVariables(vars);
std::vector<std::string> paramNames;
for (auto iter = vars.begin(); iter != vars.end(); ++iter) {
auto &entry = *iter;
paramNames.push_back(entry.first);
}

#define WriteUInt64(val) \
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()), (val))}, \
"", TrueBlock);

WriteUInt64(ordinal);
WriteUInt64(applyRule->arg_end() - applyRule->arg_begin());

int i = 0;
for (auto arg = args.begin(); arg != args.end(); arg++, i++) {
std::string name = paramNames[i];
auto sort = dynamic_cast<KORECompositeSort *>(vars[name]->getSort().get());
std::ostringstream Out;
sort->print(Out);
auto sortptr = ir->CreateGlobalStringPtr(Out.str(), "", 0, Module);
auto cat = sort->getCategory(definition);
auto s = ir->CreateGlobalStringPtr(name, "", 0, Module);
auto val = *arg;
ir->CreateCall(
getOrInsertFunction(
Module, "printVariableToFile",
llvm::Type::getVoidTy(Module->getContext()),
llvm::Type::getInt8PtrTy(Module->getContext()),
llvm::Type::getInt8PtrTy(Module->getContext())),
{outputFile, s});
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, *arg, 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});
}
WriteUInt64(0xcccccccccccccccc);
}

llvm::BranchInst::Create(MergeBlock, TrueBlock);
d->CurrentBlock = MergeBlock;
auto Call = llvm::CallInst::Create(applyRule, args, "", d->CurrentBlock);

// How do you emit the resulting config from here?

setDebugLoc(Call);
Call->setCallingConv(llvm::CallingConv::Tail);
Comment on lines +668 to 673
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This still needs to be implemented. The call instruction is meant to be tail recursive, I tried changing that but from what I remember it wasn't that simple.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Once this is implemented, the call that's left in CreateTerm to emit the config on rewrites can be removed, right? i.e. that it's there and not here is why we have configs and not function returns in the trace.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe so, yes.

if (child == nullptr) {
Expand Down