From 81e50a64bd6fbbce7560ee810d5dc06212b77691 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 20 Sep 2024 10:32:12 +0200
Subject: [PATCH 1/3] Disallow const_item_mutation

---
 lib/OutputRust.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lib/OutputRust.ml b/lib/OutputRust.ml
index 6323c6a6..3149c651 100644
--- a/lib/OutputRust.ml
+++ b/lib/OutputRust.ml
@@ -9,7 +9,6 @@ let directives = String.trim {|
 #![allow(non_camel_case_types)]
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
-#![allow(const_item_mutation)]
 |}
 
 let rust_name f = f ^ ".rs"

From 9542aa91f0b5d599d2e40d5b1283e245c29017a1 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 20 Sep 2024 10:32:25 +0200
Subject: [PATCH 2/3] Simplify deref of addrof

---
 lib/OptimizeMiniRust.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 7b56a62b..51f13683 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -886,6 +886,15 @@ let rewrite_nonminimal_bool = object
     | _ -> Call (e, tys, args)
 end
 
+let remove_deref_addrof = object
+  inherit [_] map_expr as super
+  method! visit_Deref _ e =
+    let e = super#visit_expr () e in
+    match e with
+    | Borrow (_, e) -> e
+    | _ -> Deref e
+end
+
 let map_funs f_map files =
   let files =
     List.fold_left (fun files (filename, decls) ->
@@ -907,6 +916,7 @@ let simplify_minirust files =
   let files = map_funs remove_auto_deref#visit_expr files in
   let files = map_funs rewrite_assign_op#visit_expr files in
   let files = map_funs rewrite_nonminimal_bool#visit_expr files in
+  let files = map_funs remove_deref_addrof#visit_expr files in
   (* We do this simplification last, as the previous passes might
      have introduced unit statements *)
   let files = map_funs remove_trailing_unit#visit_expr files in

From e9dbb05c3309a5594f039b21b06bb06fd11a7789 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Tue, 24 Sep 2024 17:16:36 +0200
Subject: [PATCH 3/3] Fix Makefile sed for Rust tests

---
 test/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Makefile b/test/Makefile
index b45218c9..86fbb4fa 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -305,7 +305,7 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rs: $(ALL_KRML_FILES) $(KRML_BIN)
 	$(KRML) -minimal -bundle $(notdir $(subst rust,Rust,$*))=\* \
 	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
-	$(SED) -i 's/\(mutation..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	$(SED) -i 's/\(patterns..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
 	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
 
 %.rust-test: $(OUTPUT_DIR)/%.rs