Skip to content

Commit

Permalink
Hook event for proof hints (#873)
Browse files Browse the repository at this point in the history
  • Loading branch information
@gtrepta
gtrepta authored Nov 7, 2023
1 parent a0588de commit cb8fe60
Show file tree
Hide file tree
Showing 6 changed files with 309 additions and 49 deletions.
13 changes: 12 additions & 1 deletion docs/proof-trace.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,15 @@ Here is a BNF styled description of the format
delimited_serial_kore := 0xffffffffffffffff serialized_term 0xcccccccccccccccc
null_terminated_name := <c-style null terminated string>
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
Expand All @@ -35,11 +44,13 @@ 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

- 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`)
2 changes: 2 additions & 0 deletions include/kllvm/codegen/CreateTerm.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ class CreateTerm {
bool isAnywhereOwise;
std::set<KOREPattern *> staticTerms;

llvm::Value *
alloc_arg(KORECompositePattern *pattern, int idx, std::string locationStack);
llvm::Value *createHook(
KORECompositePattern *hookAtt, KORECompositePattern *pattern,
std::string locationStack = "0");
Expand Down
42 changes: 42 additions & 0 deletions include/kllvm/codegen/ProofEvent.h
View file
Original file line number Diff line number Diff line change
@@ -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<llvm::BasicBlock *, llvm::BasicBlock *>
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
1 change: 1 addition & 0 deletions lib/codegen/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ add_library(Codegen
Decision.cpp
DecisionParser.cpp
EmitConfigParser.cpp
ProofEvent.cpp
Util.cpp
)

Expand Down
102 changes: 54 additions & 48 deletions lib/codegen/CreateTerm.cpp
View file
Original file line number Diff line number Diff line change
@@ -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 <fmt/format.h>
Expand Down Expand Up @@ -311,11 +312,16 @@ sptr<KORESort> 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<KORECompositeSort *>(p->getSort().get());
ProofEvent e(Definition, CurrentBlock, Module);
CurrentBlock = e.hookArg(ret, sort);
return ret;
}

std::string escape(std::string str) {
std::stringstream os;
Expand All @@ -336,15 +342,15 @@ 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());
llvm::BasicBlock *MergeBlock = llvm::BasicBlock::Create(
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);
Expand All @@ -354,15 +360,15 @@ 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());
llvm::BasicBlock *MergeBlock = llvm::BasicBlock::Create(
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);
Expand All @@ -372,23 +378,23 @@ 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",
CurrentBlock);
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());
llvm::BasicBlock *MergeBlock = llvm::BasicBlock::Create(
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);
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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<KORECompositeSort *>(
pattern->getConstructor()->getArguments()[0].get())
->getCategory(Definition);
Expand Down Expand Up @@ -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<KORECompositeSort *>(
pattern->getConstructor()->getArguments()[0].get())
->getCategory(Definition);
Expand Down Expand Up @@ -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<KORECompositeSort *>(
pattern->getConstructor()->getSort().get())
->getCategory(Definition);
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -673,7 +679,7 @@ llvm::Value *CreateTerm::createFunctionCall(
int i = 0;
for (auto sort : pattern->getConstructor()->getArguments()) {
auto concreteSort = dynamic_cast<KORECompositeSort *>(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:
Expand Down Expand Up @@ -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<KORECompositeSort *>(constructor->getSort().get());
auto strPattern
= dynamic_cast<KOREStringPattern *>(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);
Expand Down Expand Up @@ -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,
Expand Down
Loading

0 comments on commit cb8fe60

Please sign in to comment.