Merge pull request #325 from Nadrieril/update-charon

AeneasVerif · Aug 29, 2024 · e39c93d · e39c93d
2 parents 80dbc55 + 50fa02b
commit e39c93d
Show file tree

Hide file tree

Showing 14 changed files with 97 additions and 87 deletions.
diff --git a/charon-pin b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-79355ca1a90eccd7e3c3ded0fe3d1473a91f20ac
+f1dc801340e4105927fe8f7be17b16ecaef78699
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
@@ -200,8 +200,7 @@ module Sig = struct
     mk_sig generics inputs output
 end
 
-type raw_assumed_fun_info =
-  assumed_fun_id * fun_sig * bool * string * bool list option
+type raw_assumed_fun_info = assumed_fun_id * fun_sig * bool * bool list option
 
 type assumed_fun_info = {
   fun_id : assumed_fun_id;
@@ -217,7 +216,8 @@ type assumed_fun_info = {
 }
 
 let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
-  let fun_id, fun_sig, can_fail, name, keep_types = raw in
+  let fun_id, fun_sig, can_fail, keep_types = raw in
+  let name = Charon.PrintExpressions.assumed_fun_id_to_string fun_id in
   { fun_id; fun_sig; can_fail; name; keep_types }
 
 (** The list of assumed functions and all their information:
@@ -235,38 +235,29 @@ let raw_assumed_fun_infos : raw_assumed_fun_info list =
   [
     (* TODO: the names are not correct ("Box" should be an impl elem for instance)
        but it's not important) *)
-    ( BoxNew,
-      Sig.box_new_sig,
-      false,
-      "alloc::boxed::Box::new",
-      Some [ true; false ] );
-    (* Array Index *)
-    ( ArrayIndexShared,
+    (BoxNew, Sig.box_new_sig, false, Some [ true; false ]);
+    (* Array to slice*)
+    (ArrayToSliceShared, Sig.array_to_slice_sig false, true, None);
+    (ArrayToSliceMut, Sig.array_to_slice_sig true, true, None);
+    (* Array Repeat *)
+    (ArrayRepeat, Sig.array_repeat_sig, false, None);
+    (* Indexing *)
+    ( Index { is_array = true; mutability = RShared; is_range = false },
       Sig.array_index_sig false,
       true,
-      "@ArrayIndexShared",
       None );
-    (ArrayIndexMut, Sig.array_index_sig true, true, "@ArrayIndexMut", None);
-    (* Array to slice*)
-    ( ArrayToSliceShared,
-      Sig.array_to_slice_sig false,
+    ( Index { is_array = true; mutability = RMut; is_range = false },
+      Sig.array_index_sig true,
       true,
-      "@ArrayToSliceShared",
       None );
-    ( ArrayToSliceMut,
-      Sig.array_to_slice_sig true,
+    ( Index { is_array = false; mutability = RShared; is_range = false },
+      Sig.slice_index_sig false,
       true,
-      "@ArrayToSliceMut",
       None );
-    (* Array Repeat *)
-    (ArrayRepeat, Sig.array_repeat_sig, false, "@ArrayRepeat", None);
-    (* Slice Index *)
-    ( SliceIndexShared,
-      Sig.slice_index_sig false,
+    ( Index { is_array = false; mutability = RMut; is_range = false },
+      Sig.slice_index_sig true,
       true,
-      "@SliceIndexShared",
       None );
-    (SliceIndexMut, Sig.slice_index_sig true, true, "@SliceIndexMut", None);
   ]
 
 let assumed_fun_infos : assumed_fun_info list =

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
@@ -1152,23 +1152,31 @@ let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
   match backend () with
   | FStar | Coq | HOL4 ->
       [
-        (ArrayIndexShared, "array_index_usize");
-        (ArrayIndexMut, "array_index_mut_usize");
         (ArrayToSliceShared, "array_to_slice");
         (ArrayToSliceMut, "array_to_slice_mut");
         (ArrayRepeat, "array_repeat");
-        (SliceIndexShared, "slice_index_usize");
-        (SliceIndexMut, "slice_index_mut_usize");
+        ( Index { is_array = true; mutability = RShared; is_range = false },
+          "array_index_usize" );
+        ( Index { is_array = true; mutability = RMut; is_range = false },
+          "array_index_mut_usize" );
+        ( Index { is_array = false; mutability = RShared; is_range = false },
+          "slice_index_usize" );
+        ( Index { is_array = false; mutability = RMut; is_range = false },
+          "slice_index_mut_usize" );
       ]
   | Lean ->
       [
-        (ArrayIndexShared, "Array.index_usize");
-        (ArrayIndexMut, "Array.index_mut_usize");
         (ArrayToSliceShared, "Array.to_slice");
         (ArrayToSliceMut, "Array.to_slice_mut");
         (ArrayRepeat, "Array.repeat");
-        (SliceIndexShared, "Slice.index_usize");
-        (SliceIndexMut, "Slice.index_mut_usize");
+        ( Index { is_array = true; mutability = RShared; is_range = false },
+          "Array.index_usize" );
+        ( Index { is_array = true; mutability = RMut; is_range = false },
+          "Array.index_mut_usize" );
+        ( Index { is_array = false; mutability = RShared; is_range = false },
+          "Slice.index_usize" );
+        ( Index { is_array = false; mutability = RMut; is_range = false },
+          "Slice.index_mut_usize" );
       ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =

diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
@@ -111,8 +111,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
             | Aggregate _
             | Len _
             | NullaryOp _
-            | RawPtr _
-            | ShallowInitBox _ -> ()
+            | RawPtr _ -> ()
             | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
                 can_fail := binop_can_fail bop || !can_fail

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
@@ -640,17 +640,21 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
              * but we prefer to also check it here - this leads to cleaner messages
              * and debugging *)
             let def = ctx_lookup_type_decl ctx def_id in
-            (match def.kind with
-            | Struct _ | Enum ([] | [ _ ]) -> ()
-            | Enum (_ :: _) ->
-                craise __FILE__ __LINE__ span
-                  ("Attempted to greedily expand a symbolic enumeration with > \
-                    1 variants (option [greedy_expand_symbolics_with_borrows] \
-                    of [config]): "
-                  ^ name_to_string ctx def.item_meta.name)
-            | Alias _ | Opaque | Error _ ->
-                craise __FILE__ __LINE__ span
-                  "Attempted to greedily expand an alias or opaque type");
+            begin
+              match def.kind with
+              | Struct _ | Enum ([] | [ _ ]) -> ()
+              | Enum (_ :: _) ->
+                  craise __FILE__ __LINE__ span
+                    ("Attempted to greedily expand a symbolic enumeration with \
+                      > 1 variants (option \
+                      [greedy_expand_symbolics_with_borrows] of [config]): "
+                    ^ name_to_string ctx def.item_meta.name)
+              | Alias _ | Opaque | Error _ ->
+                  craise __FILE__ __LINE__ span
+                    "Attempted to greedily expand an alias or opaque type"
+              | Union _ ->
+                  craise __FILE__ __LINE__ span "Unions are not supported"
+            end;
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
               craise __FILE__ __LINE__ span

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
@@ -688,6 +688,9 @@ let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
     typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
     =
   match bkind with
+  | BUniqueImmutable ->
+      craise __FILE__ __LINE__ span
+        "Unique immutable closure captures are not supported"
   | BShared | BTwoPhaseMut | BShallow ->
       (* **REMARK**: we initially treated shallow borrows like shared borrows.
          In practice this restricted the behaviour too much, so for now we

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
@@ -477,13 +477,8 @@ let eval_assumed_function_call_concrete (config : config) (span : Meta.span)
       let ctx, cf_eval_body =
         match fid with
         | BoxNew -> eval_box_new_concrete config span generics ctx
-        | ArrayIndexShared
-        | ArrayIndexMut
-        | ArrayToSliceShared
-        | ArrayToSliceMut
-        | ArrayRepeat
-        | SliceIndexShared
-        | SliceIndexMut -> craise __FILE__ __LINE__ span "Unimplemented"
+        | Index _ | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat ->
+            craise __FILE__ __LINE__ span "Unimplemented"
       in
       let cc = cc_comp cc cf_eval_body in
 
@@ -892,10 +887,14 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                   | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable"
                   | Len _ ->
                       craise __FILE__ __LINE__ st.span "Len is not handled yet"
-                  | ShallowInitBox _ ->
-                      craise __FILE__ __LINE__ st.span "ShallowInitBox"
                   | Use _
-                  | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
+                  | RvRef
+                      ( _,
+                        ( BShared
+                        | BMut
+                        | BTwoPhaseMut
+                        | BShallow
+                        | BUniqueImmutable ) )
                   | NullaryOp _
                   | UnaryOp _
                   | BinaryOp _

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
@@ -300,7 +300,6 @@ let rvalue_get_place (rv : rvalue) : place option =
   | Global _
   | Discriminant _
   | Aggregate _ -> None
-  | ShallowInitBox _ -> failwith "ShallowInitBox"
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
 let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool =

diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
@@ -489,15 +489,7 @@ let fun_suffix (lp_id : LoopId.id option) : string =
   lp_suff
 
 let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
-  match fid with
-  | BoxNew -> "alloc::boxed::Box::new"
-  | ArrayIndexShared -> "@ArrayIndexShared"
-  | ArrayIndexMut -> "@ArrayIndexMut"
-  | ArrayToSliceShared -> "@ArrayToSliceShared"
-  | ArrayToSliceMut -> "@ArrayToSliceMut"
-  | ArrayRepeat -> "@ArrayRepeat"
-  | SliceIndexShared -> "@SliceIndexShared"
-  | SliceIndexMut -> "@SliceIndexMut"
+  Charon.PrintExpressions.assumed_fun_id_to_string fid
 
 let llbc_fun_id_to_string (env : fmt_env) (fid : A.fun_id) : string =
   match fid with

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
@@ -1207,6 +1207,9 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   match adt_decl.kind with
                   | Enum _ | Alias _ | Opaque | Error _ ->
                       craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
+                  | Union _ ->
+                      craise __FILE__ __LINE__ def.item_meta.span
+                        "Unions are not supported"
                   | Struct fields -> fields
                 in
                 let num_fields = List.length fields in
@@ -1587,13 +1590,8 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 | BoxNew ->
                     let arg, args = Collections.List.pop args in
                     mk_apps def.item_meta.span arg args
-                | SliceIndexShared
-                | SliceIndexMut
-                | ArrayIndexShared
-                | ArrayIndexMut
-                | ArrayToSliceShared
-                | ArrayToSliceMut
-                | ArrayRepeat -> super#visit_texpression env e)
+                | Index _ | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
+                  -> super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
@@ -578,7 +578,7 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   | Alias _ ->
       craise __FILE__ __LINE__ span
         "type aliases should have been removed earlier"
-  | T.Opaque | T.Error _ -> Opaque
+  | T.Union _ | T.Opaque | T.Error _ -> Opaque
 
 (** Translate a type definition from LLBC
 
@@ -2192,16 +2192,23 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           let back_fun_name =
             let name =
               match fid with
-              | FunId (FAssumed fid) -> (
+              | FunId (FAssumed fid) -> begin
                   match fid with
                   | BoxNew -> "box_new"
                   | ArrayRepeat -> "array_repeat"
-                  | ArrayIndexShared -> "index_shared"
-                  | ArrayIndexMut -> "index_mut"
                   | ArrayToSliceShared -> "to_slice_shared"
                   | ArrayToSliceMut -> "to_slice_mut"
-                  | SliceIndexShared -> "index_shared"
-                  | SliceIndexMut -> "index_mut")
+                  | Index { is_array = _; mutability = RMut; is_range = false }
+                    -> "index_mut"
+                  | Index
+                      { is_array = _; mutability = RShared; is_range = false }
+                    -> "index_shared"
+                  | Index { is_array = _; mutability = RMut; is_range = true }
+                    -> "subslice_mut"
+                  | Index
+                      { is_array = _; mutability = RShared; is_range = true } ->
+                      "subslice_shared"
+                end
               | FunId (FRegular fid) | TraitMethod (_, _, fid) -> (
                   let decl =
                     FunDeclId.Map.find fid ctx.fun_ctx.llbc_fun_decls

diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
@@ -294,6 +294,8 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
       | Alias _ ->
           craise __FILE__ __LINE__ def.item_meta.span
             "type aliases should have been removed earlier"
+      | Union _ ->
+          craise __FILE__ __LINE__ def.item_meta.span "unions are not supported"
       | Opaque | Error _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in

diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
@@ -12,6 +12,14 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
   let info = TypesAnalysis.analyze_ty infos ty in
   info.TypesAnalysis.contains_borrow
 
+(** Checks that a type is copyable.
+  *
+  * This used to recursively traverse the type to ensure all its fields were
+  * `Copy`. Instead we trust rustc's typechecking like we do for other marker
+  * traits.
+  *)
+let ty_is_copyable (_ty : ty) : bool = true
+
 let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool
     =
   let visitor =

diff --git a/flake.lock b/flake.lock