Merge pull request #487 from FStarLang/afromher_rs

Rust backend: allow const_item_mutation warning, simplify deref_addrof pattern

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

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"

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