Add support for structures containing borrows

Makefile

@@ -156,6 +156,8 @@ INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*)
 INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST))
 # Remove some temporary files which are inserted by, for instance, Emacs
 INPUTS_LIST := $(filter-out %~,$(INPUTS_LIST))
+INPUTS_LIST := $(filter-out .%,$(INPUTS_LIST))
+INPUTS_LIST := $(filter-out #%,$(INPUTS_LIST))
 # Remove the directory prefix, replace with `test-`
 INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST))
 

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.
-f54e30a484a373514df354cfe3fd1ba238bdee6b
+3402870cbf5b49d92fd18c312831ef30a14e6a5b

src/Config.ml

@@ -335,6 +335,9 @@ let type_check_pure_code = ref false
     as far as possible while leaving "holes" in the generated code? *)
 let fail_hard = ref false
 
+(** Shall we emit errors instead of warnings? *)
+let warnings_as_errors = ref true
+
 (** If true, add the type name as a prefix
     to the variant names.
     Ex.:

src/Errors.ml

@@ -49,7 +49,7 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option)
   if !Config.fail_hard then (
     let msg = format_error_message_with_file_line file line span msg in
     log#serror (msg ^ "\n");
-    raise (Failure (format_error_message_with_file_line file line span msg)))
+    raise (Failure msg))
   else
     let () = push_error span msg in
     raise (CFailure (span, msg))
@@ -74,5 +74,22 @@ let sanity_check_opt_span (file : string) (line : int) b span =
 let internal_error (file : string) (line : int) span =
   craise file line span "Internal error, please file an issue"
 
+let warn_opt_span (file : string) (line : int) (span : Meta.span option)
+    (msg : string) =
+  if !Config.warnings_as_errors then
+    craise_opt_span file line span
+      (msg ^ "\nYou can deactivate this error with the option -soft-warnings")
+  else
+    let msg = format_error_message_with_file_line file line span msg in
+    log#swarning (msg ^ "\n")
+
+let cassert_warn_opt_span (file : string) (line : int) (b : bool)
+    (span : Meta.span option) (msg : string) =
+  if not b then warn_opt_span file line span msg
+
+let cassert_warn (file : string) (line : int) (b : bool) (span : Meta.span)
+    (msg : string) =
+  if not b then warn_opt_span file line (Some span) msg
+
 let exec_raise = craise
 let exec_assert = cassert

src/Main.ml

@@ -122,6 +122,9 @@ let () =
       ( "-abort-on-error",
         Arg.Set fail_hard,
         " Abort on the first encountered error" );
+      ( "-soft-warnings",
+        Arg.Clear warnings_as_errors,
+        " Do not treat warnings as errors" );
       ( "-tuple-nested-proj",
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \

src/extract/Extract.ml

@@ -646,6 +646,11 @@ and extract_adt_cons (span : Meta.span) (ctx : extraction_ctx)
     (generics : generic_args) (args : texpression list) : unit =
   let e_ty = TAdt (adt_cons.adt_id, generics) in
   let is_single_pat = false in
+  (* Sanity check: make sure the expression is not a tuple constructor
+     with no arguments (the properly extracted expression would be a function) *)
+  cassert __FILE__ __LINE__
+    (not (adt_cons.adt_id = TTuple && generics.types != [] && args = []))
+    span "Unreachable";
   let _ =
     extract_adt_g_value span
       (fun ctx inside e ->

src/interp/Interpreter.ml

@@ -49,9 +49,13 @@ let compute_contexts (m : crate) : decls_ctx =
  *)
 let normalize_inst_fun_sig (span : Meta.span) (ctx : eval_ctx)
     (sg : inst_fun_sig) : inst_fun_sig =
-  let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
-    sg
-  in
+  let { regions_hierarchy = _; trait_type_constraints; inputs; output } = sg in
+  cassert_warn __FILE__ __LINE__
+    (trait_type_constraints = [])
+    span
+    "Detected type constraints over associated traits (of the shape: `where \
+     Foo::T = U`). We do not handle this properly yet: the translation may be \
+     incorrect, and the generated output will likely not typecheck.";
   let norm = AssociatedTypes.ctx_normalize_ty (Some span) ctx in
   let inputs = List.map norm inputs in
   let output = norm output in
@@ -199,17 +203,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
    * do it, and because it gives a bit of sanity.
    * *)
   let sg = fdef.signature in
-  (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+  let span = fdef.item_meta.span in
+  (* Sanity check: no nested borrows *)
   cassert __FILE__ __LINE__
     (List.for_all
-       (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+       (fun ty ->
+         not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
        (sg.output :: sg.inputs))
-    fdef.item_meta.span "Nested borrows are not supported yet";
-  cassert __FILE__ __LINE__
-    (List.for_all
-       (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
-       (sg.output :: sg.inputs))
-    fdef.item_meta.span "ADTs containing borrows are not supported yet";
+    span "Nested borrows are not supported yet";
 
   (* Create the context *)
   let regions_hierarchy =
@@ -219,25 +220,23 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx (Some fdef.item_meta.span) ctx region_groups
-      sg.generics.types sg.generics.const_generics
+    initialize_eval_ctx (Some span) ctx region_groups sg.generics.types
+      sg.generics.const_generics
   in
   (* Instantiate the signature. This updates the context because we compute
      at the same time the normalization map for the associated types.
   *)
   let ctx, inst_sg =
-    symbolic_instantiate_fun_sig fdef.item_meta.span ctx fdef.signature
-      regions_hierarchy fdef.kind
+    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
+      fdef.kind
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
-    List.map
-      (fun ty -> mk_fresh_symbolic_value fdef.item_meta.span ty)
-      inst_sg.inputs
+    List.map (fun ty -> mk_fresh_symbolic_value span ty) inst_sg.inputs
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
-  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.span;
+  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) span;
   let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
       eval_ctx * typed_avalue list =
     (* Project over the values - we use *loan* projectors, as explained above *)
@@ -259,14 +258,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     Collections.List.split_at (List.tl body.locals.vars) body.locals.arg_count
   in
   (* Push the return variable (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_var fdef.item_meta.span ctx ret_var in
+  let ctx = ctx_push_uninitialized_var span ctx ret_var in
   (* Push the input variables (initialized with symbolic values) *)
   let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
-  let ctx =
-    ctx_push_vars fdef.item_meta.span ctx (List.combine input_vars input_values)
-  in
+  let ctx = ctx_push_vars span ctx (List.combine input_vars input_values) in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars fdef.item_meta.span ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars span ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -286,6 +283,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     (fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id)
     (loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool)
     (ctx : eval_ctx) : SA.expression =
+  let span = fdef.item_meta.span in
   log#ldebug
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return:"
@@ -300,7 +298,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       ^ "\n- inside_loop: "
       ^ Print.bool_to_string inside_loop
       ^ "\n- ctx:\n"
-      ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx));
+      ^ Print.Contexts.eval_ctx_to_string ~span:(Some span) ctx));
   (* We need to instantiate the function signature - to retrieve
    * the return type. Note that it is important to re-generate
    * an instantiation of the signature, so that we use fresh
@@ -309,15 +307,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let _, ret_inst_sg =
-    symbolic_instantiate_fun_sig fdef.item_meta.span ctx fdef.signature
-      regions_hierarchy fdef.kind
+    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
+      fdef.kind
   in
   let ret_rty = ret_inst_sg.output in
   (* Move the return value out of the return variable *)
   let pop_return_value = is_regular_return in
-  let ret_value, ctx, cc =
-    pop_frame config fdef.item_meta.span pop_return_value ctx
-  in
+  let ret_value, ctx, cc = pop_frame config span pop_return_value ctx in
 
   (* We need to find the parents regions/abstractions of the region we
    * will end - this will allow us to, first, mark the other return
@@ -344,8 +340,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
           eval_ctx * typed_avalue list =
         let ctx, avalue =
-          apply_proj_borrows_on_input_value config fdef.item_meta.span ctx
-            abs.regions abs.ancestors_regions ret_value ret_rty
+          apply_proj_borrows_on_input_value config span ctx abs.regions
+            abs.ancestors_regions ret_value ret_rty
         in
         (ctx, [ avalue ])
       in
@@ -360,8 +356,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       let region_can_end rid =
         RegionGroupId.Set.mem rid parent_and_current_rgs
       in
-      sanity_check __FILE__ __LINE__ (region_can_end back_id)
-        fdef.item_meta.span;
+      sanity_check __FILE__ __LINE__ (region_can_end back_id) span;
       let ctx =
         create_push_abstractions_from_abs_region_groups
           (fun rg_id -> SynthRet rg_id)
@@ -374,7 +369,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return: (after \
         putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n"
-      ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx));
+      ^ Print.Contexts.eval_ctx_to_string ~span:(Some span) ctx));
 
   (* We now need to end the proper *input* abstractions - pay attention
    * to the fact that we end the *input* abstractions, not the *return*
@@ -477,16 +472,15 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
               sanity_check __FILE__ __LINE__
                 (if Option.is_some loop_id then loop_id = Some loop_id'
                  else true)
-                fdef.item_meta.span;
+                span;
               (* Loop abstractions *)
               let rg_id' = Option.get rg_id' in
               if rg_id' = back_id && inside_loop then
                 { abs with can_end = true }
               else abs
           | Loop (loop_id', _, LoopCall) ->
               (* We can end all the loop call abstractions *)
-              sanity_check __FILE__ __LINE__ (loop_id = Some loop_id')
-                fdef.item_meta.span;
+              sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') span;
               { abs with can_end = true }
           | SynthInput rg_id' ->
               if rg_id' = back_id && end_fun_synth_input then
@@ -509,7 +503,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   let ctx, cc =
     comp cc
       (fold_left_apply_continuation
-         (fun id ctx -> end_abstraction config fdef.item_meta.span id ctx)
+         (fun id ctx -> end_abstraction config span id ctx)
          target_abs_ids ctx)
   in
   (* Generate the Return node *)
@@ -535,6 +529,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
 let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
     (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
+  let span = fdef.item_meta.span in
   let name_to_string () =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
@@ -576,7 +571,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
           (* Pop the frame and retrieve the returned value at the same time *)
           let pop_return_value = true in
           let ret_value, ctx, cc_pop =
-            pop_frame config fdef.item_meta.span pop_return_value ctx
+            pop_frame config span pop_return_value ctx
           in
           (* Generate the Return node *)
           cc_pop (SA.Return (ctx, ret_value))
@@ -589,7 +584,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
           match res with
           | Return -> None
           | LoopReturn loop_id -> Some loop_id
-          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+          | _ -> craise __FILE__ __LINE__ span "Unreachable"
         in
         let is_regular_return = true in
         let inside_loop = Option.is_some loop_id in
@@ -612,15 +607,15 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
           match res with
           | EndEnterLoop _ -> false
           | EndContinue _ -> true
-          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+          | _ -> craise __FILE__ __LINE__ span "Unreachable"
         in
         (* Forward translation *)
         let fwd_e =
           (* Pop the frame - there is no returned value to pop: in the
              translation we will simply call the loop function *)
           let pop_return_value = false in
           let _ret_value, _ctx, cc_pop =
-            pop_frame config fdef.item_meta.span pop_return_value ctx
+            pop_frame config span pop_return_value ctx
           in
           (* Generate the Return node *)
           cc_pop (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -647,7 +642,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
          * the executions can lead to a panic *)
         SA.Panic
     | Unit | Break _ | Continue _ ->
-        craise __FILE__ __LINE__ fdef.item_meta.span
+        craise __FILE__ __LINE__ span
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
@@ -675,6 +670,7 @@ module Test = struct
     (* Retrieve the function declaration *)
     let fdef = FunDeclId.Map.find fid crate.fun_decls in
     let body = Option.get fdef.body in
+    let span = fdef.item_meta.span in
 
     (* Debug *)
     log#ldebug
@@ -687,20 +683,14 @@ module Test = struct
     (* Sanity check - *)
     sanity_check __FILE__ __LINE__
       (fdef.signature.generics = empty_generic_params)
-      fdef.item_meta.span;
-    sanity_check __FILE__ __LINE__
-      (body.locals.arg_count = 0)
-      fdef.item_meta.span;
+      span;
+    sanity_check __FILE__ __LINE__ (body.locals.arg_count = 0) span;
 
     (* Create the evaluation context *)
-    let ctx =
-      initialize_eval_ctx (Some fdef.item_meta.span) decls_ctx [] [] []
-    in
+    let ctx = initialize_eval_ctx (Some span) decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx =
-      ctx_push_uninitialized_vars fdef.item_meta.span ctx body.locals.vars
-    in
+    let ctx = ctx_push_uninitialized_vars span ctx body.locals.vars in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -709,9 +699,9 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame config fdef.item_meta.span pop_return_value ctx
+          pop_frame config span pop_return_value ctx
       | _ ->
-          craise __FILE__ __LINE__ fdef.item_meta.span
+          craise __FILE__ __LINE__ span
             ("Unit test failed (concrete execution) on: "
             ^ Print.Types.name_to_string
                 (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)