From 3716938f59c434f4904540afd52c6ac922f91d67 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 30 Jan 2024 20:22:19 +0100 Subject: [PATCH] Add no-op flag to enable mutable byte arrays (#3934) This PR adds a flag that we will propagate to downstream semantics to explicitly opt them in to the _current_ behaviour of K w.r.t. the `Bytes` sort. It is currently a no-op, but will eventually provide a potential performance increase by introducing potentially unsound behaviour. --- .../org/kframework/backend/llvm/LLVMKompileOptions.java | 6 ++++++ 1 file changed, 6 insertions(+) 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 9a7732d2572..9893c18768d 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 @@ -106,4 +106,10 @@ public List convert(String str) { description = "Emit proof hint instrumentation code into the generated interpreter", hidden = true) public boolean enableProofHints; + + @Parameter( + names = "--llvm-mutable-bytes", + description = "Use a faster, unsound representation for byte arrays on the LLVM backend", + hidden = true) + public boolean llvmMutableBytes; }