Merge pull request #116 from AeneasVerif/item_meta

1 files changed, 28 insertions, 28 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 769e3144..d9af063e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -196,12 +196,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     (List.for_all
        (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
        (sg.output :: sg.inputs))
-    fdef.meta "Nested borrows are not supported yet";
+    fdef.item_meta.meta "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.meta "ADTs containing borrows are not supported yet";
+    fdef.item_meta.meta "ADTs containing borrows are not supported yet";
 
   (* Create the context *)
   let regions_hierarchy =
@@ -211,23 +211,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 fdef.meta ctx region_groups sg.generics.types
+    initialize_eval_ctx fdef.item_meta.meta 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.meta ctx fdef.signature regions_hierarchy
+    symbolic_instantiate_fun_sig fdef.item_meta.meta 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.meta ty) inst_sg.inputs
+    List.map (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta 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.meta;
+  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.meta;
   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 *)
@@ -249,14 +249,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     Collections.List.split_at (List.tl body.locals) body.arg_count
   in
   (* Push the return variable (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_var fdef.meta ctx ret_var in
+  let ctx = ctx_push_uninitialized_var fdef.item_meta.meta 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.meta ctx (List.combine input_vars input_values)
+    ctx_push_vars fdef.item_meta.meta ctx (List.combine input_vars input_values)
   in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars fdef.meta ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -290,7 +290,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 ~meta:(Some fdef.meta) ctx));
+      ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.item_meta.meta) 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
@@ -299,13 +299,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.meta ctx fdef.signature regions_hierarchy
+    symbolic_instantiate_fun_sig fdef.item_meta.meta 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 cf_pop_frame = pop_frame config fdef.meta pop_return_value in
+  let cf_pop_frame = pop_frame config fdef.item_meta.meta pop_return_value 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
@@ -333,7 +333,7 @@ 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.meta ctx abs.regions
+            apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx abs.regions
               abs.ancestors_regions ret_value ret_rty
           in
           (ctx, [ avalue ])
@@ -349,7 +349,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.meta;
+        sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.item_meta.meta;
         let ctx =
           create_push_abstractions_from_abs_region_groups
             (fun rg_id -> SynthRet rg_id)
@@ -439,7 +439,7 @@ 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.meta;
+                  fdef.item_meta.meta;
                 (* Loop abstractions *)
                 let rg_id' = Option.get rg_id' in
                 if rg_id' = back_id && inside_loop then
@@ -448,7 +448,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
                 sanity_check __FILE__ __LINE__ (loop_id = Some loop_id')
-                  fdef.meta;
+                  fdef.item_meta.meta;
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
     let cf_end_target_abs cf =
       List.fold_left
-        (fun cf id -> end_abstraction config fdef.meta id cf)
+        (fun cf id -> end_abstraction config fdef.item_meta.meta id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -534,7 +534,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
           let fwd_e =
             (* Pop the frame and retrieve the returned value at the same time*)
             let pop_return_value = true in
-            let cf_pop = pop_frame config fdef.meta pop_return_value in
+            let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return ret_value : m_fun =
              fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -551,7 +551,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.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
           in
           let is_regular_return = true in
           let inside_loop = Option.is_some loop_id in
@@ -577,14 +577,14 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             match res with
             | EndEnterLoop _ -> false
             | EndContinue _ -> true
-            | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "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 cf_pop = pop_frame config fdef.meta pop_return_value in
+            let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return _ret_value : m_fun =
              fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -618,7 +618,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
          * the executions can lead to a panic *)
         if synthesize then Some SA.Panic else None
     | Unit | Break _ | Continue _ ->
-        craise __FILE__ __LINE__ fdef.meta
+        craise __FILE__ __LINE__ fdef.item_meta.meta
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
@@ -652,14 +652,14 @@ module Test = struct
     (* Sanity check - *)
     sanity_check __FILE__ __LINE__
       (fdef.signature.generics = empty_generic_params)
-      fdef.meta;
-    sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta;
+      fdef.item_meta.meta;
+    sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.item_meta.meta;
 
     (* Create the evaluation context *)
-    let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
+    let ctx = initialize_eval_ctx fdef.item_meta.meta decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars fdef.meta ctx body.locals in
+    let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx body.locals in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -668,9 +668,9 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
+          pop_frame config fdef.item_meta.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
-          craise __FILE__ __LINE__ fdef.meta
+          craise __FILE__ __LINE__ fdef.item_meta.meta
             ("Unit test failed (concrete execution) on: "
             ^ Print.Types.name_to_string
                 (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)