From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 17:19:14 +0100
Subject: WIP: does not compile yet because we need to propagate the meta
 variable.

---
 compiler/Interpreter.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ccae4588..961a64a4 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -173,7 +173,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
     - the list of symbolic values introduced for the input values
     - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
+let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fdef : fun_decl) :
     eval_ctx * symbolic_value list * inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
@@ -232,12 +232,12 @@ 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 ctx ret_var in
+  let ctx = ctx_push_uninitialized_var 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 ctx (List.combine input_vars input_values) in
+  let ctx = ctx_push_vars meta ctx (List.combine input_vars input_values) in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars meta ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : decls_ctx)
     (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
@@ -479,7 +479,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
   log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
 
   (* Create the evaluation context *)
-  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
+  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun meta ctx fdef in
 
   let regions_hierarchy =
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -612,7 +612,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (crate : crate) (decls_ctx : decls_ctx)
+  let test_unit_function (meta : Meta.meta)  (crate : crate) (decls_ctx : decls_ctx)
       (fid : FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = FunDeclId.Map.find fid crate.fun_decls in
@@ -634,7 +634,7 @@ module Test = struct
     let ctx = initialize_eval_ctx decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars ctx body.locals in
+    let ctx = ctx_push_uninitialized_vars meta ctx body.locals in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -665,7 +665,7 @@ module Test = struct
     && def.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (crate : crate) : unit =
+  let test_unit_functions (meta : Meta.meta)  (crate : crate) : unit =
     let unit_funs =
       FunDeclId.Map.filter
         (fun _ -> fun_decl_is_transparent_unit)
@@ -673,7 +673,7 @@ module Test = struct
     in
     let decls_ctx = compute_contexts crate in
     let test_unit_fun _ (def : fun_decl) : unit =
-      test_unit_function crate decls_ctx def.def_id
+      test_unit_function meta crate decls_ctx def.def_id
     in
     FunDeclId.Map.iter test_unit_fun unit_funs
 end
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/Interpreter.ml | 87 +++++++++++++++++++++++++------------------------
 1 file changed, 44 insertions(+), 43 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 961a64a4..a9ca415e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -10,6 +10,7 @@ open Values
 open LlbcAst
 open Contexts
 open SynthesizeSymbolic
+open Errors
 module SA = SymbolicAst
 
 (** The local logger *)
@@ -67,7 +68,7 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
     clauses (we are not considering a function call, so we don't need to
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
-let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
+let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) (kind : item_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
@@ -83,7 +84,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
       List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics
     in
     (* Annoying that we have to generate this substitution here *)
-    let r_subst _ = raise (Failure "Unexpected region") in
+    let r_subst _ = craise meta "Unexpected region" in
     let ty_subst =
       Substitute.make_type_subst_from_vars sg.generics.types types
     in
@@ -121,7 +122,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
         trait_instance_id =
       match TraitClauseId.Map.find_opt clause_id tr_map with
       | Some tr -> tr
-      | None -> raise (Failure "Local trait clause not found")
+      | None -> craise meta "Local trait clause not found"
     in
     let mk_subst tr_map =
       let tr_subst = mk_tr_subst tr_map in
@@ -149,10 +150,10 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
     in
     { regions; types; const_generics; trait_refs }
   in
-  let inst_sg = instantiate_fun_sig ctx generics tr_self sg regions_hierarchy in
+  let inst_sg = instantiate_fun_sig meta ctx generics tr_self sg regions_hierarchy in
   (* Compute the normalization maps *)
   let ctx =
-    AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
+    AssociatedTypes.ctx_add_norm_trait_types_from_preds meta ctx
       inst_sg.trait_type_constraints
   in
   (* Normalize the signature *)
@@ -173,7 +174,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
     - the list of symbolic values introduced for the input values
     - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fdef : fun_decl) :
+let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     eval_ctx * symbolic_value list * inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
@@ -195,22 +196,22 @@ let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fd
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx ctx region_groups sg.generics.types
+    initialize_eval_ctx fdef.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 ctx fdef.signature regions_hierarchy fdef.kind
+    symbolic_instantiate_fun_sig fdef.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 ty) inst_sg.inputs
+    List.map (fun ty -> mk_fresh_symbolic_value fdef.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
-  assert (call_id = FunCallId.zero);
+  cassert (call_id = FunCallId.zero) fdef.meta "The abstractions should be empty (i.e., with no avalues) abstractions";
   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 *)
@@ -232,12 +233,12 @@ let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fd
     Collections.List.split_at (List.tl body.locals) body.arg_count
   in
   (* Push the return variable (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_var meta ctx ret_var in
+  let ctx = ctx_push_uninitialized_var fdef.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 meta ctx (List.combine input_vars input_values) in
+  let ctx = ctx_push_vars fdef.meta ctx (List.combine input_vars input_values) in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars meta ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars fdef.meta ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -271,7 +272,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 ctx));
+      ^ Print.Contexts.eval_ctx_to_string fdef.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
@@ -280,12 +281,12 @@ 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 ctx fdef.signature regions_hierarchy fdef.kind
+    symbolic_instantiate_fun_sig fdef.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 pop_return_value in
+  let cf_pop_frame = pop_frame fdef.meta config 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
@@ -313,7 +314,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 ctx abs.regions
+            apply_proj_borrows_on_input_value fdef.meta config ctx abs.regions
               abs.ancestors_regions ret_value ret_rty
           in
           (ctx, [ avalue ])
@@ -329,7 +330,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
-        assert (region_can_end back_id);
+        cassert (region_can_end back_id) fdef.meta "The region should be able to end";
         let ctx =
           create_push_abstractions_from_abs_region_groups
             (fun rg_id -> SynthRet rg_id)
@@ -416,9 +417,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', rg_id', LoopSynthInput) ->
                 (* We only allow to end the loop synth input abs for the region
                    group [rg_id] *)
-                assert (
+                cassert (
                   if Option.is_some loop_id then loop_id = Some loop_id'
-                  else true);
+                  else true) fdef.meta "Only the loop synth input abs for the region group [rg_id] are allowed to end";
                 (* Loop abstractions *)
                 let rg_id' = Option.get rg_id' in
                 if rg_id' = back_id && inside_loop then
@@ -426,7 +427,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                 else abs
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
-                assert (loop_id = Some loop_id');
+                cassert (loop_id = Some loop_id') fdef.meta "TODO: error message";
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -446,7 +447,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 id cf)
+        (fun cf id -> end_abstraction fdef.meta config id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -468,7 +469,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : decls_ctx)
+let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
     (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
@@ -479,7 +480,7 @@ let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : dec
   log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
 
   (* Create the evaluation context *)
-  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun meta ctx fdef in
+  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
 
   let regions_hierarchy =
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -512,7 +513,7 @@ let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : dec
           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 pop_return_value in
+            let cf_pop = pop_frame fdef.meta config pop_return_value in
             (* Generate the Return node *)
             let cf_return ret_value : m_fun =
              fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -529,7 +530,7 @@ let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : dec
             match res with
             | Return -> None
             | LoopReturn loop_id -> Some loop_id
-            | _ -> raise (Failure "Unreachable")
+            | _ -> craise fdef.meta "Unreachable"
           in
           let is_regular_return = true in
           let inside_loop = Option.is_some loop_id in
@@ -555,14 +556,14 @@ let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : dec
             match res with
             | EndEnterLoop _ -> false
             | EndContinue _ -> true
-            | _ -> raise (Failure "Unreachable")
+            | _ -> craise fdef.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 pop_return_value in
+            let cf_pop = pop_frame fdef.meta config pop_return_value in
             (* Generate the Return node *)
             let cf_return _ret_value : m_fun =
              fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -596,13 +597,13 @@ let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : dec
          * the executions can lead to a panic *)
         if synthesize then Some SA.Panic else None
     | Unit | Break _ | Continue _ ->
-        raise
-          (Failure ("evaluate_function_symbolic failed on: " ^ name_to_string ()))
+        craise
+        fdef.meta ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    eval_function_body fdef.meta config (Option.get fdef.body).body cf_finish ctx
   in
 
   (* Return *)
@@ -612,7 +613,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (meta : Meta.meta)  (crate : crate) (decls_ctx : decls_ctx)
+  let test_unit_function (crate : crate) (decls_ctx : decls_ctx)
       (fid : FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = FunDeclId.Map.find fid crate.fun_decls in
@@ -627,14 +628,14 @@ module Test = struct
             fdef.name));
 
     (* Sanity check - *)
-    assert (fdef.signature.generics = empty_generic_params);
-    assert (body.arg_count = 0);
+    cassert (fdef.signature.generics = empty_generic_params) fdef.meta "TODO: Error message";
+    cassert (body.arg_count = 0) fdef.meta "TODO: Error message";
 
     (* Create the evaluation context *)
-    let ctx = initialize_eval_ctx decls_ctx [] [] [] in
+    let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars meta ctx body.locals in
+    let ctx = ctx_push_uninitialized_vars fdef.meta ctx body.locals in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -643,18 +644,18 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame config pop_return_value (fun _ _ -> None) ctx
+          pop_frame fdef.meta config pop_return_value (fun _ _ -> None) ctx
       | _ ->
-          raise
-            (Failure
+          craise
+            fdef.meta
                ("Unit test failed (concrete execution) on: "
                ^ Print.Types.name_to_string
                    (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-                   fdef.name))
+                   fdef.name)
     in
 
     (* Evaluate the function *)
-    let _ = eval_function_body config body.body cf_check ctx in
+    let _ = eval_function_body body.meta config body.body cf_check ctx in
     ()
 
   (** Small helper: return true if the function is a *transparent* unit function
@@ -665,7 +666,7 @@ module Test = struct
     && def.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (meta : Meta.meta)  (crate : crate) : unit =
+  let test_unit_functions (crate : crate) : unit =
     let unit_funs =
       FunDeclId.Map.filter
         (fun _ -> fun_decl_is_transparent_unit)
@@ -673,7 +674,7 @@ module Test = struct
     in
     let decls_ctx = compute_contexts crate in
     let test_unit_fun _ (def : fun_decl) : unit =
-      test_unit_function meta crate decls_ctx def.def_id
+      test_unit_function crate decls_ctx def.def_id
     in
     FunDeclId.Map.iter test_unit_fun unit_funs
 end
-- 
cgit v1.2.3


From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 12:06:05 +0100
Subject: Inverted meta and config argument orders (from meta -> config to
 config -> meta)

---
 compiler/Interpreter.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a9ca415e..6e2c15d7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -286,7 +286,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   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 fdef.meta config pop_return_value in
+  let cf_pop_frame = pop_frame config fdef.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
@@ -314,7 +314,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 fdef.meta config ctx abs.regions
+            apply_proj_borrows_on_input_value config fdef.meta ctx abs.regions
               abs.ancestors_regions ret_value ret_rty
           in
           (ctx, [ avalue ])
@@ -447,7 +447,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 fdef.meta config id cf)
+        (fun cf id -> end_abstraction config fdef.meta id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -513,7 +513,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 fdef.meta config pop_return_value in
+            let cf_pop = pop_frame config fdef.meta pop_return_value in
             (* Generate the Return node *)
             let cf_return ret_value : m_fun =
              fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -563,7 +563,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             (* 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 fdef.meta config pop_return_value in
+            let cf_pop = pop_frame config fdef.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))
@@ -603,7 +603,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body fdef.meta config (Option.get fdef.body).body cf_finish ctx
+    eval_function_body config fdef.meta (Option.get fdef.body).body cf_finish ctx
   in
 
   (* Return *)
@@ -644,7 +644,7 @@ module Test = struct
       | Return ->
           (* Ok: drop the local variables and finish *)
           let pop_return_value = true in
-          pop_frame fdef.meta config pop_return_value (fun _ _ -> None) ctx
+          pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
           craise
             fdef.meta
@@ -655,7 +655,7 @@ module Test = struct
     in
 
     (* Evaluate the function *)
-    let _ = eval_function_body body.meta config body.body cf_check ctx in
+    let _ = eval_function_body config body.meta body.body cf_check ctx in
     ()
 
   (** Small helper: return true if the function is a *transparent* unit function
-- 
cgit v1.2.3


From 7a304e990d80dc052f63f66401544040fa0f2728 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 26 Mar 2024 12:14:32 +0100
Subject: added a meta option field to norm_ctx and changed the meta used by
 some assert to the norm_ctx one

---
 compiler/Interpreter.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 6e2c15d7..2ac772ae 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -49,11 +49,11 @@ let compute_contexts (m : crate) : decls_ctx =
     to compute a normalization map (for the associated types) and that we added
     it in the context.
  *)
-let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
+let normalize_inst_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
   let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
     sg
   in
-  let norm = AssociatedTypes.ctx_normalize_ty ctx in
+  let norm = AssociatedTypes.ctx_normalize_ty meta ctx in
   let inputs = List.map norm inputs in
   let output = norm output in
   { sg with inputs; output }
@@ -157,7 +157,7 @@ let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : fun_s
       inst_sg.trait_type_constraints
   in
   (* Normalize the signature *)
-  let inst_sg = normalize_inst_fun_sig ctx inst_sg in
+  let inst_sg = normalize_inst_fun_sig meta ctx inst_sg in
   (* Return *)
   (ctx, inst_sg)
 
-- 
cgit v1.2.3


From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 27 Mar 2024 10:22:06 +0100
Subject: Added sanity_check and sanity_check_opt_meta helpers and changed
 sanity checks related cassert to these helpers to have a proper error message

---
 compiler/Interpreter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 2ac772ae..0bbde79c 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -628,8 +628,8 @@ module Test = struct
             fdef.name));
 
     (* Sanity check - *)
-    cassert (fdef.signature.generics = empty_generic_params) fdef.meta "TODO: Error message";
-    cassert (body.arg_count = 0) fdef.meta "TODO: Error message";
+    sanity_check (fdef.signature.generics = empty_generic_params) fdef.meta;
+    sanity_check (body.arg_count = 0) fdef.meta;
 
     (* Create the evaluation context *)
     let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/Interpreter.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 0bbde79c..034304c7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -211,7 +211,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
-  cassert (call_id = FunCallId.zero) fdef.meta "The abstractions should be empty (i.e., with no avalues) abstractions";
+  sanity_check (call_id = FunCallId.zero) fdef.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 *)
@@ -272,7 +272,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 fdef.meta ctx));
+      ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.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
@@ -330,7 +330,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
-        cassert (region_can_end back_id) fdef.meta "The region should be able to end";
+        sanity_check (region_can_end back_id) fdef.meta;
         let ctx =
           create_push_abstractions_from_abs_region_groups
             (fun rg_id -> SynthRet rg_id)
@@ -417,9 +417,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', rg_id', LoopSynthInput) ->
                 (* We only allow to end the loop synth input abs for the region
                    group [rg_id] *)
-                cassert (
+                sanity_check (
                   if Option.is_some loop_id then loop_id = Some loop_id'
-                  else true) fdef.meta "Only the loop synth input abs for the region group [rg_id] are allowed to end";
+                  else true) fdef.meta;
                 (* Loop abstractions *)
                 let rg_id' = Option.get rg_id' in
                 if rg_id' = back_id && inside_loop then
@@ -427,7 +427,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                 else abs
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
-                cassert (loop_id = Some loop_id') fdef.meta "TODO: error message";
+                sanity_check (loop_id = Some loop_id') fdef.meta;
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -603,7 +603,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body config fdef.meta (Option.get fdef.body).body cf_finish ctx
+    eval_function_body config (Option.get fdef.body).body cf_finish ctx
   in
 
   (* Return *)
@@ -655,7 +655,7 @@ module Test = struct
     in
 
     (* Evaluate the function *)
-    let _ = eval_function_body config body.meta body.body cf_check ctx in
+    let _ = eval_function_body config body.body cf_check ctx in
     ()
 
   (** Small helper: return true if the function is a *transparent* unit function
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/Interpreter.ml | 43 +++++++++++++++++++++++++------------------
 1 file changed, 25 insertions(+), 18 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 034304c7..453ad088 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -49,7 +49,8 @@ let compute_contexts (m : crate) : decls_ctx =
     to compute a normalization map (for the associated types) and that we added
     it in the context.
  *)
-let normalize_inst_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
+let normalize_inst_fun_sig (meta : Meta.meta) (ctx : eval_ctx)
+    (sg : inst_fun_sig) : inst_fun_sig =
   let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
     sg
   in
@@ -68,8 +69,8 @@ let normalize_inst_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : inst_fun_si
     clauses (we are not considering a function call, so we don't need to
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
-let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : fun_sig)
-    (regions_hierarchy : region_var_groups) (kind : item_kind) :
+let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx)
+    (sg : fun_sig) (regions_hierarchy : region_var_groups) (kind : item_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
@@ -150,7 +151,9 @@ let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : fun_s
     in
     { regions; types; const_generics; trait_refs }
   in
-  let inst_sg = instantiate_fun_sig meta ctx generics tr_self sg regions_hierarchy in
+  let inst_sg =
+    instantiate_fun_sig meta ctx generics tr_self sg regions_hierarchy
+  in
   (* Compute the normalization maps *)
   let ctx =
     AssociatedTypes.ctx_add_norm_trait_types_from_preds meta ctx
@@ -203,7 +206,8 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
      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 fdef.kind
+    symbolic_instantiate_fun_sig fdef.meta ctx fdef.signature regions_hierarchy
+      fdef.kind
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
@@ -236,7 +240,9 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
   let ctx = ctx_push_uninitialized_var fdef.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) in
+  let ctx =
+    ctx_push_vars fdef.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
   (* Return *)
@@ -281,7 +287,8 @@ 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 fdef.kind
+    symbolic_instantiate_fun_sig fdef.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 *)
@@ -417,9 +424,10 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', rg_id', LoopSynthInput) ->
                 (* We only allow to end the loop synth input abs for the region
                    group [rg_id] *)
-                sanity_check (
-                  if Option.is_some loop_id then loop_id = Some loop_id'
-                  else true) fdef.meta;
+                sanity_check
+                  (if Option.is_some loop_id then loop_id = Some loop_id'
+                   else true)
+                  fdef.meta;
                 (* Loop abstractions *)
                 let rg_id' = Option.get rg_id' in
                 if rg_id' = back_id && inside_loop then
@@ -597,8 +605,8 @@ 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
-        fdef.meta ("evaluate_function_symbolic failed on: " ^ name_to_string ())
+        craise fdef.meta
+          ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
   (* Evaluate the function *)
@@ -646,12 +654,11 @@ module Test = struct
           let pop_return_value = true in
           pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
-          craise
-            fdef.meta
-               ("Unit test failed (concrete execution) on: "
-               ^ Print.Types.name_to_string
-                   (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-                   fdef.name)
+          craise fdef.meta
+            ("Unit test failed (concrete execution) on: "
+            ^ Print.Types.name_to_string
+                (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
+                fdef.name)
     in
 
     (* Evaluate the function *)
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/Interpreter.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 453ad088..ea1d5633 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -85,7 +85,7 @@ let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx)
       List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics
     in
     (* Annoying that we have to generate this substitution here *)
-    let r_subst _ = craise meta "Unexpected region" in
+    let r_subst _ = craise __FILE__ __LINE__ meta "Unexpected region" in
     let ty_subst =
       Substitute.make_type_subst_from_vars sg.generics.types types
     in
@@ -123,7 +123,7 @@ let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx)
         trait_instance_id =
       match TraitClauseId.Map.find_opt clause_id tr_map with
       | Some tr -> tr
-      | None -> craise meta "Local trait clause not found"
+      | None -> craise __FILE__ __LINE__ meta "Local trait clause not found"
     in
     let mk_subst tr_map =
       let tr_subst = mk_tr_subst tr_map in
@@ -215,7 +215,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
-  sanity_check (call_id = FunCallId.zero) fdef.meta;
+  sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.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 *)
@@ -337,7 +337,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 (region_can_end back_id) fdef.meta;
+        sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.meta;
         let ctx =
           create_push_abstractions_from_abs_region_groups
             (fun rg_id -> SynthRet rg_id)
@@ -424,7 +424,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
             | Loop (loop_id', rg_id', LoopSynthInput) ->
                 (* We only allow to end the loop synth input abs for the region
                    group [rg_id] *)
-                sanity_check
+                sanity_check __FILE__ __LINE__
                   (if Option.is_some loop_id then loop_id = Some loop_id'
                    else true)
                   fdef.meta;
@@ -435,7 +435,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                 else abs
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
-                sanity_check (loop_id = Some loop_id') fdef.meta;
+                sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') fdef.meta;
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -538,7 +538,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             match res with
             | Return -> None
             | LoopReturn loop_id -> Some loop_id
-            | _ -> craise fdef.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
           in
           let is_regular_return = true in
           let inside_loop = Option.is_some loop_id in
@@ -564,7 +564,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
             match res with
             | EndEnterLoop _ -> false
             | EndContinue _ -> true
-            | _ -> craise fdef.meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
           in
           (* Forward translation *)
           let fwd_e =
@@ -605,7 +605,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 fdef.meta
+        craise __FILE__ __LINE__ fdef.meta
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
   in
 
@@ -636,8 +636,8 @@ module Test = struct
             fdef.name));
 
     (* Sanity check - *)
-    sanity_check (fdef.signature.generics = empty_generic_params) fdef.meta;
-    sanity_check (body.arg_count = 0) fdef.meta;
+    sanity_check __FILE__ __LINE__ (fdef.signature.generics = empty_generic_params) fdef.meta;
+    sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta;
 
     (* Create the evaluation context *)
     let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
@@ -654,7 +654,7 @@ module Test = struct
           let pop_return_value = true in
           pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
       | _ ->
-          craise fdef.meta
+          craise __FILE__ __LINE__ fdef.meta
             ("Unit test failed (concrete execution) on: "
             ^ Print.Types.name_to_string
                 (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-- 
cgit v1.2.3


From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 14:07:36 +0100
Subject: formatting and changed save_error condition for failing from b to not
 b

---
 compiler/Interpreter.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ea1d5633..a65e1663 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -435,7 +435,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                 else abs
             | Loop (loop_id', _, LoopCall) ->
                 (* We can end all the loop call abstractions *)
-                sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') fdef.meta;
+                sanity_check __FILE__ __LINE__ (loop_id = Some loop_id')
+                  fdef.meta;
                 { abs with can_end = true }
             | SynthInput rg_id' ->
                 if rg_id' = back_id && end_fun_synth_input then
@@ -636,7 +637,9 @@ module Test = struct
             fdef.name));
 
     (* Sanity check - *)
-    sanity_check __FILE__ __LINE__ (fdef.signature.generics = empty_generic_params) fdef.meta;
+    sanity_check __FILE__ __LINE__
+      (fdef.signature.generics = empty_generic_params)
+      fdef.meta;
     sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta;
 
     (* Create the evaluation context *)
-- 
cgit v1.2.3