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.
-5332b4eec44dbdb0e9be8b1a359257f71c905e55
+eaa116ab1782ff49cc9c7c1f4d0ae61c357b280b

src/PrePasses.ml

@@ -577,7 +577,7 @@ let remove_shallow_borrows_storage_live_dead (crate : crate) (f : fun_decl) :
 
         method! visit_Assign env p rv =
           match (p.kind, rv) with
-          | PlaceLocal var_id, RvRef (_, BShallow) ->
+          | PlaceLocal var_id, RvRef (_, BShallow, _) ->
               (* Filter *)
               filtered := LocalId.Set.add var_id !filtered;
               Nop
@@ -773,6 +773,17 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
                       new_statements := st :: !new_statements;
                       local_id
                     in
+                    let str_len =
+                      Constant
+                        {
+                          kind =
+                            CLiteral
+                              (VScalar
+                                 (UnsignedScalar
+                                    (Usize, Z.of_int (String.length str))));
+                          ty = TLiteral (TUInt Usize);
+                        }
+                    in
                     (* Then the borrow *)
                     let local_id =
                       let nlocal_id = fresh_local cv.ty in
@@ -783,7 +794,9 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
                       in
                       let rv =
                         RvRef
-                          ({ kind = PlaceLocal local_id; ty = str_ty }, bkind)
+                          ( { kind = PlaceLocal local_id; ty = str_ty },
+                            bkind,
+                            str_len )
                       in
                       let lv = { kind = PlaceLocal nlocal_id; ty = cv.ty } in
                       let st =
@@ -914,14 +927,24 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl =
                 (* Introduce the intermediate reference *)
                 let local_id =
                   let local_id = fresh_local ref_ty in
+                  let metadata =
+                    Copy
+                      {
+                        kind = PlaceGlobal crate.unit_metadata;
+                        ty = mk_unit_ty;
+                      }
+                  in
                   let st =
                     {
                       span;
                       statement_id = StatementId.zero;
                       kind =
                         Assign
                           ( { kind = PlaceLocal local_id; ty = ref_ty },
-                            RvRef ({ kind = PlaceGlobal gref; ty }, BShared) );
+                            RvRef
+                              ( { kind = PlaceGlobal gref; ty },
+                                BShared,
+                                metadata ) );
                       comments_before = [];
                     }
                   in

src/extract/ExtractBuiltin.ml

@@ -60,7 +60,16 @@ let builtin_globals () : (string * string) list =
   let mk_ints_globals name =
     List.map (fun ty -> mk_int_global ty name) all_int_names
   in
-  List.concat [ mk_ints_globals "MIN"; mk_ints_globals "MAX" ]
+  List.concat
+    [
+      mk_ints_globals "MIN";
+      mk_ints_globals "MAX";
+      [
+        (* UNIT_METADATA should be eliminated through a micro-pass and should
+           never appear in the code.. *)
+        ("UNIT_METADATA", "UNIT_METADATA");
+      ];
+    ]
 
 let mk_builtin_globals_map () : Pure.builtin_global_info NameMatcherMap.t =
   NameMatcherMap.of_list

src/interp/InterpreterExpressions.ml

@@ -677,7 +677,10 @@ let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
            (otherwise it throws an exception) *)
         let _ = cast_unsize_to_modified_fields span ctx ty0 ty1 in
         ty1
-    | _ -> [%craise] span ("Invalid input for unop: " ^ unop_to_string ctx unop)
+    | _ ->
+        [%craise] span
+          ("Invalid input for unop: " ^ unop_to_string ctx unop ^ " on "
+         ^ ty_to_string ctx v.ty)
   in
   let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
   (* Compute the result *)
@@ -1039,7 +1042,8 @@ let eval_rvalue_not_global (config : config) (span : Meta.span)
   (* Delegate to the proper auxiliary function *)
   match rvalue with
   | Use op -> wrap_in_result (eval_operand config span op ctx)
-  | RvRef (p, bkind) -> wrap_in_result (eval_rvalue_ref config span p bkind ctx)
+  | RvRef (p, bkind, _) ->
+      wrap_in_result (eval_rvalue_ref config span p bkind ctx)
   | UnaryOp (unop, op) -> eval_unary_op config span unop op ctx
   | BinaryOp (binop, op1, op2) -> eval_binary_op config span binop op1 op2 ctx
   | Aggregate (aggregate_kind, ops) ->

src/interp/InterpreterStatements.ml

@@ -839,7 +839,8 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                       | BMut
                       | BTwoPhaseMut
                       | BShallow
-                      | BUniqueImmutable ) )
+                      | BUniqueImmutable ),
+                      _ )
                 | NullaryOp _
                 | UnaryOp _
                 | BinaryOp _
@@ -890,7 +891,7 @@ and eval_rvalue_global (config : config) (span : Meta.span) (dest : place)
  fun ctx ->
   (* One of the micro-passes makes sures there is only one case to handle *)
   match rv with
-  | RvRef ({ kind = PlaceGlobal gref; ty = _ }, BShared) ->
+  | RvRef ({ kind = PlaceGlobal gref; ty = _ }, BShared, _) ->
       eval_global_ref config span dest gref RShared ctx
   | _ ->
       [%craise] span

src/interp/InterpreterUtils.ml

@@ -325,7 +325,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | Len (p, _, _) | RvRef (p, _) | RawPtr (p, _) -> Some p
+  | Len (p, _, _) | RvRef (p, _, _) | RawPtr (p, _, _) -> Some p
   | NullaryOp _
   | UnaryOp _
   | BinaryOp _

src/llbc/RegionsHierarchy.ml

@@ -166,6 +166,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
     | TFnDef _ -> [%craise_opt_span] span "unsupported: FnDef"
     | TDynTrait _ ->
         [%craise_opt_span] span "Dynamic trait types are not supported yet"
+    | TPtrMetadata _ -> [%craise_opt_span] span "unsupported: PtrMetadata"
     | TError _ ->
         [%craise_opt_span] span "Found type error in the output of charon"
   and explore_generics (outer : region list) (generics : generic_args) =

src/llbc/TypesAnalysis.ml

@@ -364,6 +364,7 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
         in
         analyze span expl_info ty_info output
     | TFnDef _ -> [%craise_opt_span] span "unsupported: FnDef"
+    | TPtrMetadata _ -> [%craise_opt_span] span "unsupported: PtrMetadata"
     | TError _ ->
         [%craise_opt_span] span "Found type error in the output of charon"
   in
@@ -649,7 +650,12 @@ let compute_outlive_proj_ty (span : Meta.span option)
                back values computed for the generated backward functions may \
                be incorrect.";
             ()
-        | TRawPtr _ | TDynTrait _ | TFnPtr _ | TFnDef _ | TError _ ->
+        | TRawPtr _
+        | TDynTrait _
+        | TFnPtr _
+        | TFnDef _
+        | TPtrMetadata _
+        | TError _ ->
             (* Don't know what to do *)
             [%craise_opt_span] span "Not handled yet"
     end

src/pure/PureMicroPasses.ml

@@ -3188,33 +3188,40 @@ let filter_loop_inputs_explore_one_visitor (ctx : ctx)
   reset_fvar_id_counter ();
   let body = open_all_fun_body span body in
   [%ldebug "After opening binders:\n" ^ fun_body_to_string ctx body];
+  (* Note that not all binders bind free variables: some of them might be `_` because
+     filtered the useless binders. *)
   let used =
-    ref (List.map (fun v -> ((fst (as_pat_open span v)).id, false)) body.inputs)
+    ref
+      (List.map
+         (fun (v : tpattern) ->
+           let id =
+             match v.pat with
+             | POpen (fv, _) -> Some fv.id
+             | _ -> None
+           in
+           (id, false))
+         body.inputs)
   in
   let inputs =
     List.map
-      (fun v ->
-        let v, _ = as_pat_open span v in
-        (v.id, mk_texpr_from_fvar v))
+      (fun (v : tpattern) ->
+        match v.pat with
+        | POpen (fv, _) -> Some (fv.id, mk_texpr_from_fvar fv)
+        | _ -> None)
       body.inputs
   in
   [%ltrace
     "inputs:\n"
     ^ String.concat ", " (List.map (tpattern_to_string ctx) body.inputs)];
   let inputs_set =
-    FVarId.Set.of_list
-      (List.map
-         (fun x ->
-           let x, _ = as_pat_open span x in
-           x.id)
-         body.inputs)
+    FVarId.Set.of_list (List.map fst (List.filter_map (fun x -> x) inputs))
   in
   [%sanity_check] decl.item_meta.span (Option.is_some decl.loop_id);
 
   let fun_id = (T.FRegular decl.def_id, decl.loop_id) in
 
   let set_used (vid : fvar_id) =
-    used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used
+    used := List.map (fun (vid', b) -> (vid', b || Some vid = vid')) !used
   in
 
   let visitor =
@@ -3245,10 +3252,13 @@ let filter_loop_inputs_explore_one_visitor (ctx : ctx)
                             (List.map (texpr_to_string ctx) args)];
                       let used_args = List.combine inputs args in
                       List.iter
-                        (fun ((vid, var), arg) ->
-                          if var <> arg then (
-                            self#visit_texpr env arg;
-                            set_used vid))
+                        (fun (input, arg) ->
+                          match input with
+                          | Some (vid, var) ->
+                              if var <> arg then (
+                                self#visit_texpr env arg;
+                                set_used vid)
+                          | None -> ())
                         used_args)
                     else super#visit_texpr env e
                 | _ -> super#visit_texpr env e)
@@ -3269,7 +3279,11 @@ let filter_loop_inputs_explore_one_visitor (ctx : ctx)
   [%ltrace
     "- used variables: "
     ^ String.concat ", "
-        (List.map (Print.pair_to_string FVarId.to_string string_of_bool) !used)];
+        (List.map
+           (Print.pair_to_string
+              (Print.option_to_string FVarId.to_string)
+              string_of_bool)
+           !used)];
 
   (* Save the filtering information, if there is anything to filter *)
   if List.exists (fun (_, b) -> not b) !used then

src/symbolic/SymbolicToPureExpressions.ml

@@ -631,7 +631,6 @@ and translate_function_call_aux (call : S.call) (e : S.expr) (ctx : bs_ctx) :
         | CastRawPtr _ -> [%craise] ctx.span "Unsupported: raw ptr casts"
         | CastTransmute _ -> [%craise] ctx.span "Unsupported: transmute"
       end
-    | S.Unop E.PtrMetadata -> [%craise] ctx.span "Unsupported unop: PtrMetadata"
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->

src/symbolic/SymbolicToPureTypes.ml

@@ -127,6 +127,7 @@ let rec translate_sty (span : Meta.span option) (ty : T.ty) : ty =
       [%craise_opt_span] span "Arrow types are not supported yet"
   | TDynTrait _ ->
       [%craise_opt_span] span "Dynamic trait types are not supported yet"
+  | TPtrMetadata _ -> [%craise_opt_span] span "unsupported: PtrMetadata"
   | TError _ ->
       [%craise_opt_span] span "Found type error in the output of charon"
 
@@ -313,6 +314,7 @@ let rec translate_fwd_ty (span : Meta.span option) (type_infos : type_infos)
       [%craise_opt_span] span "Arrow types are not supported yet"
   | TDynTrait _ ->
       [%craise_opt_span] span "Dynamic trait types are not supported yet"
+  | TPtrMetadata _ -> [%craise_opt_span] span "unsupported: PtrMetadata"
   | TError _ ->
       [%craise_opt_span] span "Found type error in the output of charon"
 
@@ -431,6 +433,7 @@ let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos)
       [%craise_opt_span] span "Arrow types are not supported yet"
   | TDynTrait _ ->
       [%craise_opt_span] span "Dynamic trait types are not supported yet"
+  | TPtrMetadata _ -> [%craise_opt_span] span "unsupported: PtrMetadata"
   | TError _ ->
       [%craise_opt_span] span "Found type error in the output of charon"
 

src/symbolic/SymbolicToPureValues.ml

@@ -510,12 +510,14 @@ let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) :
     ^ Print.list_to_string (texpr_to_string ctx) values];
   values
 
-let translate_mprojection_elem (pe : E.projection_elem) :
+let translate_mprojection_elem span (pe : E.projection_elem) :
     mprojection_elem option =
   match pe with
   | Deref -> None
   | Field (pkind, field_id) -> Some { pkind; field_id }
   | ProjIndex _ | Subslice _ -> None
+  | PtrMetadata ->
+      [%craise_opt_span] span "supported place projection: pointer metadata"
 
 (** Translate a "meta"-place *)
 let rec translate_mplace span type_infos (p : S.mplace) : mplace =
@@ -528,7 +530,7 @@ let rec translate_mplace span type_infos (p : S.mplace) : mplace =
       PlaceGlobal { global_id = id; global_generics }
   | PlaceProjection (p, pe) -> (
       let p = translate_mplace span type_infos p in
-      let pe = translate_mprojection_elem pe in
+      let pe = translate_mprojection_elem span pe in
       match pe with
       | None -> p
       | Some pe -> PlaceProjection (p, pe))

src/symbolic/SynthesizeSymbolic.ml

@@ -98,6 +98,7 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
     | TFnPtr _
     | TRawPtr _
     | TDynTrait _
+    | TPtrMetadata _
     | TError _ -> [%craise] span "Ill-formed symbolic expansion"
   in
   Expansion (place, sv, expansion)