Merge pull request #5 from AeneasVerif/protz_initializers

Rely on upstream fixes to disable systematic desugaring of array assi…

Makefile

@@ -3,7 +3,7 @@ KRML_HOME 		?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
 EURYDICE	?= ./eurydice $(EURYDICE_FLAGS)
 CHARON		?= $(CHARON_HOME)/bin/charon
 
-CHARON_TEST_FILES	= array
+CHARON_TEST_FILES	= arrays
 TEST_DIRS		= array const_generics traits array2d int_switch nested_arrays # step_by
 
 .PHONY: all
@@ -30,6 +30,7 @@ charon-test-%: $(CHARON_HOME)/tests/llbc/%.llbc | out/test-% all
 
 # Tests checked into the current repository
 .PHONY: phony
+.PRECIOUS: test/%/out.llbc
 test/%/out.llbc: phony
 	cd test/$* && $(CHARON) --errors-as-warnings && mv $*.llbc out.llbc
 

bin/main.ml

@@ -118,7 +118,7 @@ Supported options:|}
   let files = Krml.Structs.pass_by_ref files in
   let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
   let files = Krml.Simplify.optimize_lets files in
-  let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in
+  (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   let files = Krml.Simplify.sequence_to_let#visit_files () files in
   let files = Krml.Simplify.hoist#visit_files [] files in

lib/AstOfLlbc.ml

@@ -821,24 +821,28 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta
 
   | Call { func = FnOpRegular ({
         func;
-        generics = { types = type_args; const_generics = const_generic_args; _ };
+        generics = { types = type_args; const_generics = const_generic_args; trait_refs; _ };
         trait_and_method_generic_args
       } as fn_ptr); args; dest; _ }
   ->
       (* General case for function calls and trait method calls. *)
       L.log "Calls" "Visiting call: %s" (Charon.PrintExpressions.fn_ptr_to_string env.format_env fn_ptr);
       L.log "Calls" "is_array_map: %b" (RustNames.is_array_map env fn_ptr);
-      L.log "Calls" "--> %d type_args, %d const_generics" (List.length type_args) (List.length const_generic_args);
+      L.log "Calls" "--> %d type_args, %d const_generics, %d trait_refs"
+        (List.length type_args) (List.length const_generic_args) (List.length trait_refs);
 
       (* For now, we take trait type arguments to be part of the code-gen *)
-      let type_args, const_generic_args =
+      let type_args, const_generic_args, trait_refs =
         match trait_and_method_generic_args with
         | None ->
-            type_args, const_generic_args
-        | Some { types; const_generics; _ } ->
-            types @ type_args, const_generics @ const_generic_args
+            type_args, const_generic_args, trait_refs
+        | Some { types; const_generics; trait_refs; _ } ->
+            types @ type_args, const_generics @ const_generic_args, trait_refs @ trait_refs
       in
-      L.log "Calls" "--> %d type_args, %d const_generics" (List.length type_args) (List.length const_generic_args);
+      L.log "Calls" "--> %d type_args, %d const_generics, %d trait_refs"
+        (List.length type_args) (List.length const_generic_args) (List.length trait_refs);
+      L.log "Calls" "--> trait_refs: %s\n"
+        (String.concat " ++ " (List.map (Charon.PrintTypes.trait_ref_to_string env.format_env) trait_refs));
       L.log "Calls" "--> pattern: %s" (string_of_fn_ptr env fn_ptr);
 
       let dest, _ = expression_of_place env dest in

lib/Cleanup2.ml

@@ -90,32 +90,48 @@ let remove_array_repeats = object(self)
     match e.node, es with
     | ETApp ({ node = EQualified lid; _ }, [ len ], [ _ ]), [ init ] when lid = Builtin.array_repeat.name ->
         let l = match len.node with EConstant (_, s) -> int_of_string s | _ -> failwith "impossible" in
+        let init = self#visit_expr env init in
         EBufCreateL (Stack, List.init l (fun _ -> init))
     | _ ->
         super#visit_EApp env e es
 
   method! visit_ELet (((), _) as env) b e1 e2 =
+    let rec all_repeats e =
+      match e.node with
+      | EConstant _ ->
+          true
+      | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ _ ], [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name ->
+          all_repeats init
+      | _ ->
+          false
+    in
     match e1.node with
     | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ len ], [ _ ]); _ }, [ init ]) when lid = Builtin.array_repeat.name ->
-        (* let b = [ init; len ] *)
-        let module H = Krml.Helpers in
-        let len = self#visit_expr env len in
-        let init = self#visit_expr env init in
-        (* let b; *)
-        ELet (b, H.any,
-        (* let _ = *)
-        with_type e2.typ (ELet (H.sequence_binding (),
-          (* for *)
-          H.with_unit (EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *),
-            H.mk_lt_usize (Krml.DeBruijn.lift 2 len) (* i < len *),
-            H.mk_incr_usize (* i++ *),
-            let i = with_type H.usize (EBound 0) in
-            let b = with_type b.typ (EBound 1) in
-            let b_i = with_type (H.assert_tbuf_or_tarray b.typ) (EBufRead (b, i)) in
-            (* b[i] := init *)
-            H.with_unit (EAssign (b_i, Krml.DeBruijn.lift 2 init)))),
-        (* e2 *)
-        Krml.DeBruijn.lift 1 (self#visit_expr env e2))))
+        if all_repeats e1 then
+          (* Further code-gen can handle nested ebufcreatel's by using nested
+             static initializer lists, possiblye shortening to { 0 } if
+             applicable. *)
+          super#visit_ELet env b e1 e2
+        else
+          (* let b = [ init; len ] *)
+          let module H = Krml.Helpers in
+          let len = self#visit_expr env len in
+          let init = self#visit_expr env init in
+          (* let b; *)
+          ELet (b, H.any,
+          (* let _ = *)
+          with_type e2.typ (ELet (H.sequence_binding (),
+            (* for *)
+            H.with_unit (EFor (Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *),
+              H.mk_lt_usize (Krml.DeBruijn.lift 2 len) (* i < len *),
+              H.mk_incr_usize (* i++ *),
+              let i = with_type H.usize (EBound 0) in
+              let b = with_type b.typ (EBound 1) in
+              let b_i = with_type (H.assert_tbuf_or_tarray b.typ) (EBufRead (b, i)) in
+              (* b[i] := init *)
+              H.with_unit (EAssign (b_i, Krml.DeBruijn.lift 2 init)))),
+          (* e2 *)
+          Krml.DeBruijn.lift 1 (self#visit_expr env e2))))
 
     | _ ->
         super#visit_ELet env b e1 e2