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

Fix some bugs relating to machine integer literals #1172

Merged
merged 3 commits into from
Dec 5, 2024
Merged

Fix some bugs relating to machine integer literals #1172

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
401ce06
try and fix mint literal construction and pattern matching
dwightguth Dec 3, 2024
93f37f8
add test
dwightguth Dec 3, 2024
c7a582e
use sort.bits if lit string doesn't contain precision
dwightguth Dec 3, 2024
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
11 changes: 8 additions & 3 deletions lib/codegen/CreateStaticTerm.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,10 +306,15 @@ create_static_term::create_token(value_type sort, std::string contents) {
assert(false && "not implemented yet: tokens");
case sort_category::MInt: {
size_t idx = contents.find_first_of("pP");
assert(idx != std::string::npos);
uint64_t bits = std::stoi(contents.substr(idx + 1));
uint64_t bits{};
if (idx == std::string::npos) {
bits = sort.bits;
} else {
bits = std::stoi(contents.substr(idx + 1));
contents = contents.substr(0, idx);
}
return llvm::ConstantInt::get(
llvm::IntegerType::get(ctx_, bits), contents.substr(0, idx), 10);
llvm::IntegerType::get(ctx_, bits), contents, 10);
}
case sort_category::Bool:
return llvm::ConstantInt::get(
Expand Down
33 changes: 24 additions & 9 deletions lib/codegen/EmitConfigParser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -491,15 +491,18 @@ static void emit_get_token(kore_definition *definition, llvm::Module *module) {
= llvm::ConstantInt::get(llvm::Type::getInt32Ty(ctx), 0);
for (auto const &entry : sorts) {
std::string name = entry.first;
if (!entry.second->get_object_sort_variables().empty()) {
// TODO: MINT in initial configuration
continue;
}
auto sort = kore_composite_sort::create(name);
value_type cat = sort->get_category(definition);
if (cat.cat == sort_category::Symbol
|| cat.cat == sort_category::Variable) {
continue;
value_type cat{};
if (entry.second->attributes().contains(attribute_set::key::Hook)
&& entry.second->attributes().get_string(attribute_set::key::Hook)
== "MINT.MInt") {
cat.cat = sort_category::MInt;
} else {
cat = sort->get_category(definition);
if (cat.cat == sort_category::Symbol
|| cat.cat == sort_category::Variable) {
continue;
}
}
current_block->insertInto(func);
current_block->setName("is_" + name);
Expand Down Expand Up @@ -527,10 +530,22 @@ static void emit_get_token(kore_definition *definition, llvm::Module *module) {
case sort_category::List:
case sort_category::Set:
case sort_category::StringBuffer:
case sort_category::MInt:
// TODO: tokens
add_abort(case_block, module);
break;
case sort_category::MInt: {
auto const &len = func->arg_begin() + 1;
auto const &contents = func->arg_begin() + 2;
auto *get_mint_token = get_or_insert_function(
module, "get_mint_token",
llvm::FunctionType::get(
ptr_ty, {llvm::Type::getInt64Ty(ctx), ptr_ty}, false));
auto *mint_token = llvm::CallInst::Create(
get_mint_token, {len, contents}, "", case_block);
phi->addIncoming(mint_token, case_block);
llvm::BranchInst::Create(merge_block, case_block);
break;
}
case sort_category::Bool: {
auto *str = llvm::ConstantDataArray::getString(ctx, "true", false);
auto *global = module->getOrInsertGlobal("bool_true", str->getType());
Expand Down
2 changes: 2 additions & 0 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,8 @@ object Generator {
case "false" => "0"
case _ => str
}
} else if (hookAtt.contains("MINT.MInt")) {
str.substring(0, str.indexOf('p'))
} else str,
SortCategory(hookAtt.orElse(Some("STRING.String")), sort, symlib)
)
Expand Down
18 changes: 18 additions & 0 deletions runtime/util/ConfigurationParser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,24 @@ static thread_local Cache cache;

extern "C" {

size_t *hook_MINT_export(mpz_t in, uint64_t bits);

void *get_mint_token(size_t size, char const *c_str) {
std::string str = std::string(c_str, size);
size_t idx = str.find('p');
assert(idx != std::string::npos);
std::string precision_str = str.substr(idx + 1);
long long precision = std::stoll(precision_str);
long long precision_in_bytes = (precision + 7) / 8;
char *token = (char *)malloc(precision_in_bytes);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can you remind me where we handle the deallocation of this?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It looks like this memory might be leaking currently; it's supposed to be freed by the configuration parser once it's no longer needed, but I don't see that happening currently. This is not a regression though; the same thing is already happening with other terms in the configuration parser.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Got it. Should we add an issue in this repo so we don't lose track of this?

std::string val_str = str.substr(0, idx);
mpz_t z;
mpz_init_set_str(z, val_str.c_str(), 10);
size_t *mint = hook_MINT_export(z, precision);
memcpy(token, mint, precision_in_bytes);
return token;
}

uint32_t get_tag_for_symbol_name_internal(char const *);

void init_float(floating *result, char const *c_str) {
Expand Down
Loading
Loading