From 2d26b93482c5b967c84e65e2c55ffc1cb2967dbb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Thu, 17 Oct 2024 17:02:43 +0100 Subject: [PATCH 1/2] Marking simplifications that preserve definedness (#4662) For the booster-with-remainders to be fully operational and therefore the dependency on Kore be reduced, the simplifications that contain partial functions but which we know preserve definedness must be marked as such. --- k-distribution/include/kframework/builtin/domains.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index b04af99c8e..bd6ea7716e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1366,10 +1366,10 @@ module INT-SYMBOLIC [symbolic] rule X %Int N => X requires 0 <=Int X andBool X X [simplification] - rule 0 < 0 [simplification] - rule X >>Int 0 => X [simplification] - rule 0 >>Int _ => 0 [simplification] + rule X < X [simplification, preserves-definedness] + rule 0 < 0 requires 0 <=Int Y [simplification, preserves-definedness] + rule X >>Int 0 => X [simplification, preserves-definedness] + rule 0 >>Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness] endmodule module INT-SYMBOLIC-KORE [symbolic, haskell] From 82039eea869a48d37f5a610be1a71249334a8316 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 17 Oct 2024 11:59:33 -0500 Subject: [PATCH 2/2] add hidden visibility flag (#4666) This PR adds a flag to kompile which passes through to the llvm backend. Fairly straightforward. --- .../main/java/org/kframework/backend/llvm/LLVMBackend.java | 3 +++ .../org/kframework/backend/llvm/LLVMKompileOptions.java | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index 420f6c1676..e154e7b653 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -146,6 +146,9 @@ private void llvmKompile(String type, String executable) { if (options.llvmMutableBytes) { args.add("--mutable-bytes"); } + if (options.llvmHiddenVisibility) { + args.add("--hidden-visibility"); + } if (options.debug) { args.add("-g"); diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java index 282b58c2f0..b330a5268a 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java @@ -119,4 +119,10 @@ public List convert(String str) { description = "Use a faster, unsound representation for byte arrays on the LLVM backend", hidden = true) public boolean llvmMutableBytes; + + @Parameter( + names = "--llvm-hidden-visibility", + description = "Build the llvm backend with -fvisibility=hidden", + hidden = true) + public boolean llvmHiddenVisibility; }