Bump 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.
-fbd54169205bf97e3c42cbfef95ca5807d697bfb
+aabfaf42d9c3c3e2ef773f70ff98b14af5b56f26

src/BorrowCheck.ml

@@ -19,12 +19,12 @@ let borrow_check_crate (crate : crate) (marked_ids : Contexts.marked_ids) : unit
   (* Borrow-check *)
   let borrow_check_fun (fdef : fun_decl) : unit =
     match fdef.body with
-    | None -> ()
-    | Some _ ->
+    | Body _ ->
         let synthesize = false in
         let _ =
           evaluate_function_symbolic synthesize trans_ctx marked_ids fdef
         in
         ()
+    | _ -> ()
   in
   List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls)

src/PrePasses.ml

@@ -62,7 +62,7 @@ let erase_body_regions (crate : crate) (f : fun_decl) : fun_decl =
   (* Map  *)
   let body =
     match f.body with
-    | Some body ->
+    | Body body ->
         let body =
           {
             body with
@@ -74,8 +74,8 @@ let erase_body_regions (crate : crate) (f : fun_decl) : fun_decl =
               };
           }
         in
-        Some { body with body = erase_visitor#visit_block 0 body.body }
-    | None -> None
+        Body { body with body = erase_visitor#visit_block 0 body.body }
+    | other -> other
   in
 
   let f : fun_decl = { f with body } in
@@ -135,10 +135,10 @@ let remove_unreachable (crate : crate) (f : fun_decl) : fun_decl =
     end
   in
   match f.body with
-  | None -> f
-  | Some body ->
+  | Body body ->
       let body = { body with body = visitor#visit_block () body.body } in
-      { f with body = Some body }
+      { f with body = Body body }
+  | _ -> f
 
 (** The Rust compiler generates a unique implementation of [Default] for arrays
     for every choice of length. For instance, if we write:
@@ -642,8 +642,8 @@ let update_loops (crate : crate) (f : fun_decl) : fun_decl =
   (* Map  *)
   let body =
     match f.body with
-    | Some body -> Some { body with body = visitor#visit_block 0 body.body }
-    | None -> None
+    | Body body -> Body { body with body = visitor#visit_block 0 body.body }
+    | other -> other
   in
 
   let f : fun_decl = { f with body } in
@@ -726,8 +726,8 @@ let remove_useless_joins (crate : crate) (f : fun_decl) : fun_decl =
 
   let body =
     match f.body with
-    | Some body -> Some { body with body = snd (update_block [] body.body) }
-    | None -> None
+    | Body body -> Body { body with body = snd (update_block [] body.body) }
+    | other -> other
   in
 
   let f : fun_decl = { f with body } in
@@ -818,8 +818,8 @@ let remove_shallow_borrows_storage_live_dead (crate : crate) (f : fun_decl) :
 
   let body =
     match f.body with
-    | None -> None
-    | Some body -> Some { body with body = filter_in_body body.body }
+    | Body body -> Body { body with body = filter_in_body body.body }
+    | other -> other
   in
   let f = { f with body } in
   [%ldebug
@@ -878,7 +878,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
   (* Map  *)
   let body =
     match f.body with
-    | Some body ->
+    | Body body ->
         let new_locals = ref [] in
         let _, gen =
           LocalId.mk_stateful_generator_starting_at_id
@@ -1006,7 +1006,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
           | _ -> [ st ]
         in
         let body_body = map_statement decompose_in_statement body.body in
-        Some
+        Body
           {
             body with
             body = body_body;
@@ -1016,7 +1016,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
                 locals = body.locals.locals @ List.rev !new_locals;
               };
           }
-    | None -> None
+    | other -> other
   in
   { f with body }
 
@@ -1025,7 +1025,7 @@ let refresh_statement_ids (_ : crate) (f : fun_decl) : fun_decl =
   (* Map  *)
   let body =
     match f.body with
-    | Some body ->
+    | Body body ->
         let _, gen_id = StatementId.fresh_stateful_generator () in
 
         (* Visit the rvalue *)
@@ -1036,8 +1036,8 @@ let refresh_statement_ids (_ : crate) (f : fun_decl) : fun_decl =
           end
         in
 
-        Some { body with body = visitor#visit_block () body.body }
-    | None -> None
+        Body { body with body = visitor#visit_block () body.body }
+    | other -> other
   in
   { f with body }
 
@@ -1099,8 +1099,8 @@ let simplify_panics (crate : crate) (f : fun_decl) : fun_decl =
 
   let body =
     match f.body with
-    | None -> None
-    | Some body -> Some { body with body = visitor#visit_block () body.body }
+    | Body body -> Body { body with body = visitor#visit_block () body.body }
+    | other -> other
   in
   { f with body }
 
@@ -1126,8 +1126,7 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl =
   (* Map  *)
   let body =
     match f.body with
-    | None -> None
-    | Some body -> (
+    | Body body -> (
         let new_locals = ref [] in
         let _, gen =
           LocalId.mk_stateful_generator_starting_at_id
@@ -1230,7 +1229,7 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl =
         (* Visit all the statements and decompose the operands *)
         try
           let body_body = map_statement decompose_in_statement body.body in
-          Some
+          Body
             {
               body with
               body = body_body;
@@ -1263,7 +1262,8 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl =
           [%save_error_opt_span] error.span
             ("Failure when pre- processing: " ^ name
            ^ "; ignoring its body.\nName pattern: '" ^ name_pattern ^ "'");
-          None)
+          Opaque)
+    | other -> other
   in
   { f with body }
 
@@ -1339,8 +1339,7 @@ let replace_static (crate : crate) : crate =
     (* Update the uses of this definition *)
     let update (f : fun_decl) : fun_decl =
       match f.body with
-      | None -> f
-      | Some body ->
+      | Body body ->
           let visitor =
             object
               inherit [_] map_statement
@@ -1366,7 +1365,8 @@ let replace_static (crate : crate) : crate =
           in
 
           let body = { body with body = visitor#visit_block () body.body } in
-          { f with body = Some body }
+          { f with body = Body body }
+      | _ -> f
     in
     let fun_decls = FunDeclId.Map.map update crate.fun_decls in
     { crate with fun_decls }
@@ -1745,8 +1745,8 @@ let simplify_trait_calls (crate : crate) : crate =
     (fun _ (f : fun_decl) ->
       if f.item_meta.is_local then visitor#visit_fun_decl_id () f.def_id;
       match f.body with
-      | None -> ()
-      | Some body -> visitor#visit_block () body.body)
+      | Body body -> visitor#visit_block () body.body
+      | _ -> ())
     crate.fun_decls;
 
   GlobalDeclId.Map.iter
@@ -1889,15 +1889,18 @@ let apply_passes (crate : crate) : crate =
         "After applying [" ^ pass_name ^ "]:\n"
         ^ Print.Crate.crate_fun_decl_to_string crate f];
       f
-    with CFailure _ ->
+    with CFailure e ->
       (* The error was already registered, we don't need to register it twice.
          However, we replace the body of the function, and save an error to
          report to the user the fact that we will ignore the function body *)
       let fmt = Print.Crate.crate_to_fmt_env crate in
       let name = Print.name_to_string fmt f.item_meta.name in
       [%save_error] f.item_meta.span
         ("Ignoring the body of '" ^ name ^ "' because of previous error");
-      { f with body = None }
+      let msg =
+        Errors.format_error_message_with_file_line e.file e.line e.span e.msg
+      in
+      { f with body = Error { span = f.item_meta.span; msg } }
   in
   let fun_decls : fun_decl FunDeclId.Map.t =
     let num_decls = FunDeclId.Map.cardinal crate.fun_decls in

src/Translate.ml

@@ -27,15 +27,15 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx)
   [%ltrace name_to_string trans_ctx fdef.item_meta.name];
 
   match fdef.body with
-  | None -> None
-  | Some _ ->
+  | Body _ ->
       (* Evaluate - note that [evaluate_function_symbolic synthesize] catches
          exceptions to at least generate a dummy body if we do not abort on failure. *)
       let synthesize = true in
       let inputs, symb =
         evaluate_function_symbolic synthesize trans_ctx marked_ids fdef
       in
       Some (inputs, Option.get symb)
+  | _ -> None
 
 (** Sanity check helper.
 
@@ -211,7 +211,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
      function)
   *)
   let ctx =
-    match (fdef.body, symbolic_trans) with
+    match (LlbcAstUtils.body_as_body fdef.body, symbolic_trans) with
     | None, None -> ctx
     | Some body, Some (input_svs, _) ->
         let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in
@@ -394,7 +394,9 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
     let funs = FunDeclId.Map.values trans_ctx.fun_ctx.to_extract in
     (* Split between opaque and transparent *)
     let opaque, transparent =
-      List.partition (fun (d : fun_decl) -> Option.is_none d.body) funs
+      List.partition
+        (fun (d : fun_decl) -> not (LlbcAstUtils.body_is_known d.body))
+        funs
     in
 
     (* Reorder the transparent functions to have the biggest first:
@@ -1655,7 +1657,7 @@ let extract_translated_crate (filename : string) (dest_dir : string)
            If the backend is Lean the module names depends on the path,
            so we generate names of the shape [Types.lean], [Funs.lean], etc.
            because those files should be placed in the proper sub-folder.
-           
+
            Otherwise, we prepend the crate name to generate, e.g.,
            [Foo_Types.fst], [Foo_Funs.fst], etc.
          *)

src/interp/Interp.ml

@@ -292,7 +292,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx)
       inst_sg.abs_regions_hierarchy region_can_end compute_abs_avalues ctx
   in
   (* Split the variables between return var, inputs and remaining locals *)
-  let body = Option.get fdef.body in
+  let body = [%add_loc] body_as_body_exn fdef.body in
   let ret_var = List.hd body.locals.locals in
   let input_vars, local_vars =
     Collections.List.split_at (List.tl body.locals.locals) body.locals.arg_count
@@ -536,9 +536,8 @@ let evaluate_function_symbolic (synthesize : bool) (decls_ctx : decls_ctx)
   (* Evaluate the function *)
   let symbolic =
     try
-      let ctx_resl, cc =
-        eval_function_body config (Option.get fdef.body).body ctx
-      in
+      let body = [%add_loc] body_as_body_exn fdef.body in
+      let ctx_resl, cc = eval_function_body config body.body ctx in
       let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
       (* Finish synthesizing *)
       if synthesize then Some (cc el) else None
@@ -570,7 +569,7 @@ module Test = struct
       (fid : FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = FunDeclId.Map.find fid crate.fun_decls in
-    let body = Option.get fdef.body in
+    let body = [%add_loc] body_as_body_exn fdef.body in
     let span = fdef.item_meta.span in
 
     (* Debug *)
@@ -613,7 +612,7 @@ module Test = struct
   (** Small helper: return true if the function is a *transparent* unit function
       (no parameters, no arguments) - TODO: move *)
   let fun_decl_is_transparent_unit (def : fun_decl) : bool =
-    Option.is_some def.body
+    body_is_known def.body
     && def.generics = empty_generic_params
     && def.signature.inputs = []
 

src/interp/InterpStatements.ml

@@ -1386,11 +1386,13 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
       (* We can evaluate the function call only if it is not opaque *)
       let body =
         match def.body with
-        | None ->
+        | Body body -> body
+        | other ->
             [%craise] span
-              ("Can't evaluate a call to an opaque function: "
-              ^ name_to_string ctx def.item_meta.name)
-        | Some body -> body
+              ("Can't evaluate a call to function: "
+              ^ name_to_string ctx def.item_meta.name
+              ^ ", it is "
+              ^ Charon.GAst.show_body Fmt.nop other)
       in
       (* TODO: we need to normalize the types if we want to correctly support traits *)
       [%cassert] body.span (generics.trait_refs = [])
@@ -1399,7 +1401,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
         [%add_loc] Subst.make_subst_from_generics (Some span) def.generics
           generics Self
       in
-      let locals, body_st = Subst.fun_body_substitute_in_body subst body in
+      let locals, body_st = Subst.expr_body_substitute subst body in
 
       (* Evaluate the input operands *)
       [%sanity_check] body.span (List.length args = body.locals.arg_count);

src/llbc/FunsAnalysis.ml

@@ -176,14 +176,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) :
       let has_builtin_info = builtin_info <> None in
       group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
       match f.body with
-      | None ->
+      | Body body -> obj#visit_block body.body.span body.body
+      | _ ->
           let info_can_fail =
             match builtin_info with
             | None -> true
             | Some { can_fail } -> can_fail
           in
           obj#may_fail info_can_fail
-      | Some body -> obj#visit_block body.body.span body.body
     in
     List.iter visit_fun d;
     (* We need to know if the declaration group contains a global - note that