Skip to content

Commit

Permalink
Remove array namespace check (#988)
Browse files Browse the repository at this point in the history
For runtimeverification/k#3976

There's a special case for a hook namespace in `ARRAY` which falls back
to K semantics for those symbols. The frontend wont emit any hook
attributes in that namespace for the ARRAY module anyway so it can
safely be removed.
  • Loading branch information
gtrepta authored Feb 19, 2024
1 parent 95ab61e commit 38a50d2
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 12 deletions.
3 changes: 0 additions & 3 deletions lib/ast/AST.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -218,9 +218,6 @@ ValueType KORECompositeSort::getCategory(std::string const &hookName) {
category = SortCategory::MInt;
bits = std::stoi(hookName.substr(10));
} else {
// ARRAY.Array is implemented in K and therefore should fall through to the
// default category. Should it one day be implemented as a fully hooked
// sort, a check needs to be added to the list above.
category = SortCategory::Symbol;
}
return {category, bits};
Expand Down
11 changes: 2 additions & 9 deletions lib/codegen/CreateTerm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -648,15 +648,8 @@ llvm::Value *CreateTerm::createHook(
assert(false && "not implemented yet: MInt");
abort();
}
std::string domain = name.substr(0, name.find('.'));
if (domain == "ARRAY") {
// array is not really hooked in llvm, it's implemented in K
auto fn_name = fmt::format(
"eval_{}", ast_to_string(*pattern->getConstructor(), 0, false));
return createFunctionCall(fn_name, pattern, false, true, locationStack);
}
std::string hookName
= "hook_" + domain + "_" + name.substr(name.find('.') + 1);
std::string hookName = "hook_" + name.substr(0, name.find('.')) + "_"
+ name.substr(name.find('.') + 1);
return createFunctionCall(hookName, pattern, true, false, locationStack);
}

Expand Down

0 comments on commit 38a50d2

Please sign in to comment.