Skip to content

Commit

Permalink
Ignore injection symbols when tracking locations in the proof trace (#…
Browse files Browse the repository at this point in the history
…964)

fixes: #963

---------

Co-authored-by: rv-jenkins <[email protected]>
  • Loading branch information
gtrepta and rv-jenkins authored Jan 31, 2024
1 parent 8c77e21 commit 78a8fa2
Show file tree
Hide file tree
Showing 5 changed files with 121 additions and 107 deletions.
2 changes: 1 addition & 1 deletion include/kllvm/binary/ProofTraceParser.h
Original file line number Diff line number Diff line change
Expand Up @@ -210,7 +210,7 @@ class LLVMRewriteTrace {

class ProofTraceParser {
public:
static constexpr uint32_t expectedVersion = 3u;
static constexpr uint32_t expectedVersion = 4u;

private:
bool verbose;
Expand Down
1 change: 1 addition & 0 deletions include/kllvm/codegen/CreateTerm.h
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,7 @@ llvm::Type *getValueType(ValueType sort, llvm::Module *Module);
llvm::Type *getParamType(ValueType sort, llvm::Module *Module);

bool isCollectionSort(ValueType cat);
bool isInjectionSymbol(KOREPattern *p, KORESymbol *sym);

void addAbort(llvm::BasicBlock *block, llvm::Module *Module);

Expand Down
29 changes: 21 additions & 8 deletions lib/codegen/CreateTerm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -294,8 +294,11 @@ sptr<KORESort> termSort(KOREPattern *pattern) {
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;
std::string newLocation = fmt::format("{}:{}", locationStack, idx);
if (isInjectionSymbol(p, Definition->getInjSymbol())) {
newLocation = locationStack;
}
llvm::Value *ret = createAllocation(p, newLocation).first;
auto *sort = dynamic_cast<KORECompositeSort *>(p->getSort().get());
ProofEvent e(Definition, Module);
CurrentBlock = e.hookArg(ret, sort, CurrentBlock);
Expand Down Expand Up @@ -770,10 +773,11 @@ llvm::Value *CreateTerm::notInjectionCase(
if (idx == 2 && val != nullptr) {
ChildValue = val;
} else {
ChildValue
= createAllocation(
child.get(), fmt::format("{}:{}", locationStack, idx - 2))
.first;
std::string newLocation = fmt::format("{}:{}", locationStack, idx - 2);
if (isInjectionSymbol(child.get(), Definition->getInjSymbol())) {
newLocation = locationStack;
}
ChildValue = createAllocation(child.get(), newLocation).first;
}

auto *sort = dynamic_cast<KORECompositeSort *>(child->getSort().get());
Expand Down Expand Up @@ -907,8 +911,7 @@ CreateTerm::createAllocation(KOREPattern *pattern, std::string locationStack) {
symbolDecl->getAttributes().count("sortInjection")
&& (cat == SortCategory::Symbol)) {
std::pair<llvm::Value *, bool> val = createAllocation(
constructor->getArguments()[0].get(),
fmt::format("{}:0", locationStack));
constructor->getArguments()[0].get(), locationStack);
if (val.second) {
llvm::Instruction *Tag = llvm::CallInst::Create(
getOrInsertFunction(
Expand Down Expand Up @@ -1254,4 +1257,14 @@ bool isCollectionSort(ValueType cat) {
}
}

bool isInjectionSymbol(KOREPattern *p, KORESymbol *inj) {
if (auto *constructor = dynamic_cast<KORECompositePattern *>(p)) {
KORESymbol const *symbol = constructor->getConstructor();
if (symbol->getName() == inj->getName()) {
return true;
}
}
return false;
}

} // namespace kllvm
2 changes: 1 addition & 1 deletion runtime/util/util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ block *constructRawTerm(void *subject, char const *sort, bool raw_value) {
}

void printProofHintHeader(char *output_file) {
uint32_t version = 3;
uint32_t version = 4;
FILE *file = fopen(output_file, "a");
fprintf(file, "HINT");
fwrite(&version, sizeof(version), 1, file);
Expand Down
Loading

0 comments on commit 78a8fa2

Please sign in to comment.