Merge pull request #331 from Nadrieril/update-charon

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.
-cdc1dcde447a50cbc20336c79b21b42ac977b7fd
+96448ed72c9e8838ca2ed6b8477b5f2fb9cc8058

compiler/FunsAnalysis.ml

@@ -107,6 +107,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
             | Use _
             | RvRef _
             | Global _
+            | GlobalRef _
             | Discriminant _
             | Aggregate _
             | Len _

compiler/InterpreterExpressions.ml

@@ -780,7 +780,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
   let v, cf_compute =
     (* Match on the aggregate kind *)
     match aggregate_kind with
-    | AggregatedAdt (type_id, opt_variant_id, generics) -> (
+    | AggregatedAdt (type_id, opt_variant_id, opt_field_id, generics) -> (
+        (* The opt_field_id is Some only for unions, that we don't support *)
+        sanity_check __FILE__ __LINE__ (opt_field_id = None) span;
         match type_id with
         | TTuple ->
             let tys = List.map (fun (v : typed_value) -> v.ty) values in

compiler/InterpreterStatements.ml

@@ -828,6 +828,26 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                 regions_hierarchy,
                 inst_sg )))
 
+(** Helper: introduce a fresh symbolic value for a global *)
+let eval_global_as_fresh_symbolic_value (span : Meta.span)
+    (gref : global_decl_ref) (ctx : eval_ctx) : symbolic_value =
+  let generics = gref.global_generics in
+  let global = ctx_lookup_global_decl ctx gref.global_id in
+  cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
+    "Const globals should not contain regions";
+  (* Instantiate the type  *)
+  (* There shouldn't be any reference to Self *)
+  let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
+  let generics = Subst.generic_args_erase_regions generics in
+  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+    Subst.make_subst_from_generics global.generics generics tr_self
+  in
+  let ty =
+    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+      global.ty
+  in
+  mk_fresh_symbolic_value span ty
+
 (** Evaluate a statement *)
 let rec eval_statement (config : config) (st : statement) : stl_cm_fun =
  fun ctx ->
@@ -865,6 +885,9 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
       | Global gref ->
           (* Evaluate the global *)
           eval_global config st.span p gref ctx
+      | GlobalRef (gref, rkind) ->
+          (* Evaluate the reference to the global *)
+          eval_global_ref config st.span p gref rkind ctx
       | _ ->
           (* Evaluate the rvalue *)
           let res, ctx, cc = eval_rvalue_not_global config st.span rvalue ctx in
@@ -884,7 +907,8 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                  * reserved borrow, we later can't translate it to pure values...) *)
                 let cc =
                   match rvalue with
-                  | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable"
+                  | Global _ | GlobalRef _ ->
+                      craise __FILE__ __LINE__ st.span "Unreachable"
                   | Len _ ->
                       craise __FILE__ __LINE__ st.span "Len is not handled yet"
                   | Use _
@@ -973,31 +997,18 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
 and eval_global (config : config) (span : Meta.span) (dest : place)
     (gref : global_decl_ref) : stl_cm_fun =
  fun ctx ->
-  let generics = gref.global_generics in
-  let global = ctx_lookup_global_decl ctx gref.global_id in
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body *)
+      let generics = gref.global_generics in
+      let global = ctx_lookup_global_decl ctx gref.global_id in
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
       eval_transparent_function_call_concrete config span global.body call ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
-      cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
-        "Const globals should not contain regions";
-      (* Instantiate the type  *)
-      (* There shouldn't be any reference to Self *)
-      let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
-      let generics = Subst.generic_args_erase_regions generics in
-      let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-        Subst.make_subst_from_generics global.generics generics tr_self
-      in
-      let ty =
-        Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-          global.ty
-      in
-      let sval = mk_fresh_symbolic_value span ty in
+      let sval = eval_global_as_fresh_symbolic_value span gref ctx in
       let ctx, cc =
         assign_to_place config span
           (mk_typed_value_from_symbolic_value sval)
@@ -1007,6 +1018,47 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
         cc_singleton __FILE__ __LINE__ span
           (cc_comp (S.synthesize_global_eval gref sval) cc) )
 
+and eval_global_ref (config : config) (span : Meta.span) (dest : place)
+    (gref : global_decl_ref) (rk : ref_kind) : stl_cm_fun =
+ fun ctx ->
+  (* We only support shared references to globals *)
+  cassert __FILE__ __LINE__ (rk = RShared) span
+    "Can only create shared references to global values";
+  match config.mode with
+  | ConcreteMode ->
+      (* We should treat the evaluation of the global as a call to the global body,
+         then create a reference *)
+      craise __FILE__ __LINE__ span "Unimplemented"
+  | SymbolicMode ->
+      (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
+       * defined as equal to the value of the global (see {!S.synthesize_global_eval}).
+       * We then create a reference to the global.
+       *)
+      let sval = eval_global_as_fresh_symbolic_value span gref ctx in
+      let typed_sval = mk_typed_value_from_symbolic_value sval in
+      (* Create a shared loan containing the global, as well as a shared borrow *)
+      let bid = fresh_borrow_id () in
+      let loan : typed_value =
+        {
+          value = VLoan (VSharedLoan (BorrowId.Set.singleton bid, typed_sval));
+          ty = sval.sv_ty;
+        }
+      in
+      let borrow : typed_value =
+        {
+          value = VBorrow (VSharedBorrow bid);
+          ty = TRef (RErased, sval.sv_ty, RShared);
+        }
+      in
+      (* We need to push the shared loan in a dummy variable *)
+      let dummy_id = fresh_dummy_var_id () in
+      let ctx = ctx_push_dummy_var ctx dummy_id loan in
+      (* Assign the borrow to its destination *)
+      let ctx, cc = assign_to_place config span borrow dest ctx in
+      ( [ (ctx, Unit) ],
+        cc_singleton __FILE__ __LINE__ span
+          (cc_comp (S.synthesize_global_eval gref sval) cc) )
+
 (** Evaluate a switch *)
 and eval_switch (config : config) (span : Meta.span) (switch : switch) :
     stl_cm_fun =

compiler/InterpreterUtils.ml

@@ -298,6 +298,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   | UnaryOp _
   | BinaryOp _
   | Global _
+  | GlobalRef _
   | Discriminant _
   | Aggregate _ -> None
 

compiler/PrePasses.ml

@@ -110,7 +110,8 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl =
     | Assign (_, rv) -> (
         match rv with
         | Use _ | RvRef _ -> not must_end_with_exit
-        | Aggregate (AggregatedAdt (TTuple, _, _), []) -> not must_end_with_exit
+        | Aggregate (AggregatedAdt (TTuple, _, _, _), []) ->
+            not must_end_with_exit
         | _ -> false)
     | FakeRead _ | Drop _ | Nop -> not must_end_with_exit
     | Panic | Return -> true