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/InterpreterExpressions.ml | 94 +++++++++++++++++++-------------------
 1 file changed, 47 insertions(+), 47 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index afbf4605..51be904f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -23,7 +23,7 @@ let log = Logging.expressions_log
     Note that the place should have been prepared so that there are no remaining
     loans.
 *)
-let expand_primitively_copyable_at_place (config : config)
+let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Small helper *)
@@ -36,7 +36,7 @@ let expand_primitively_copyable_at_place (config : config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx))
+          expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -59,7 +59,7 @@ let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
   (* Call the continuation *)
   cf v ctx
 
-let access_rplace_reorganize_and_read (config : config)
+let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
@@ -71,7 +71,7 @@ let access_rplace_reorganize_and_read (config : config)
    * borrows) *)
   let cc =
     if expand_prim_copy then
-      comp cc (expand_primitively_copyable_at_place config access p)
+      comp cc (expand_primitively_copyable_at_place meta config access p)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -79,10 +79,10 @@ let access_rplace_reorganize_and_read (config : config)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
-  access_rplace_reorganize_and_read config expand_prim_copy access p
+  access_rplace_reorganize_and_read meta config expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
@@ -224,7 +224,7 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
@@ -237,12 +237,12 @@ let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
-        access_rplace_reorganize config expand_prim_copy access p cf ctx
+        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
     | Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
-        access_rplace_reorganize config expand_prim_copy access p cf ctx
+        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
   in
   (* Apply *)
   prepare cf ctx
@@ -358,7 +358,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   (* Debug *)
@@ -368,7 +368,7 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
      ^ eval_ctx_to_string ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
-    (prepare_eval_operand_reorganize config op)
+    (prepare_eval_operand_reorganize meta config op)
     (eval_operand_no_reorganize config op)
     cf ctx
 
@@ -376,16 +376,16 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
     cm_fun =
-  fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
+  fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
 
 (** Evaluate several operands. *)
-let eval_operands (config : config) (ops : operand list)
+let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
     (cf : typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
-  let prepare = prepare_eval_operands_reorganize config ops in
+  let prepare = prepare_eval_operands_reorganize meta config ops in
   (* Evaluate the operands *)
   let eval =
     fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
@@ -393,9 +393,9 @@ let eval_operands (config : config) (ops : operand list)
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
     (cf : typed_value * typed_value -> m_fun) : m_fun =
-  let eval_op = eval_operands config [ op1; op2 ] in
+  let eval_op = eval_operands meta config [ op1; op2 ] in
   let use_res cf res =
     match res with
     | [ v1; v2 ] -> cf (v1, v2)
@@ -403,10 +403,10 @@ let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let eval_op = eval_operand config op in
+  let eval_op = eval_operand meta config op in
   (* Apply the unop *)
   let apply cf (v : typed_value) : m_fun =
     match (unop, v.value) with
@@ -451,11 +451,11 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand config op in
+  let eval_op = eval_operand meta config op in
   (* Generate a fresh symbolic value to store the result *)
   let apply cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -472,17 +472,17 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
     let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
     (* Synthesize the symbolic AST *)
     synthesize_unary_op ctx unop v
-      (mk_opt_place_from_op op ctx)
+      (mk_opt_place_from_op meta op ctx)
       res_sv None expr
   in
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (config : config) (unop : unop) (op : operand)
+let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_unary_op_concrete config unop op cf
-  | SymbolicMode -> eval_unary_op_symbolic config unop op cf
+  | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
+  | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
@@ -557,10 +557,10 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
         | Ne | Eq -> raise (Failure "Unreachable"))
     | _ -> raise (Failure "Invalid inputs for binop")
 
-let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config op1 op2 in
+  let eval_ops = eval_two_operands meta config op1 op2 in
   (* Compute the result of the binop *)
   let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
@@ -569,11 +569,11 @@ let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config op1 op2 in
+  let eval_ops = eval_two_operands meta config op1 op2 in
   (* Compute the result of applying the binop *)
   let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
    fun ctx ->
@@ -609,20 +609,20 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
     let v = mk_typed_value_from_symbolic_value res_sv in
     let expr = cf (Ok v) ctx in
     (* Synthesize the symbolic AST *)
-    let p1 = mk_opt_place_from_op op1 ctx in
-    let p2 = mk_opt_place_from_op op2 ctx in
+    let p1 = mk_opt_place_from_op meta op1 ctx in
+    let p2 = mk_opt_place_from_op meta op2 ctx in
     synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
   in
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
-  | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
+  | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
 
-let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
@@ -643,7 +643,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
 
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read config expand_prim_copy access p
+        access_rplace_reorganize_and_read meta config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -693,7 +693,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
       let access = Write in
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read config expand_prim_copy access p
+        access_rplace_reorganize_and_read meta config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -714,10 +714,10 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
     (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_operands config ops in
+  let eval_ops = eval_operands meta config ops in
   (* Compute the value *)
   let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
    fun ctx ->
@@ -781,7 +781,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
@@ -793,12 +793,12 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
   let comp_wrap f = comp f wrap_in_result cf in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> comp_wrap (eval_operand config op) ctx
-  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
-  | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
-  | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
+  | Use op -> comp_wrap (eval_operand meta config op) ctx
+  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
+  | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
   | Aggregate (aggregate_kind, ops) ->
-      comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
+      comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
   | Discriminant _ ->
       raise
         (Failure
@@ -806,11 +806,11 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
             the AST")
   | Global _ -> raise (Failure "Unreachable")
 
-let eval_fake_read (config : config) (p : place) : cm_fun =
+let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   let expand_prim_copy = false in
   let cf_prepare cf =
-    access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+    access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-- 
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/InterpreterExpressions.ml | 185 +++++++++++++++++++------------------
 1 file changed, 93 insertions(+), 92 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 51be904f..f82c7130 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -11,6 +11,7 @@ open Cps
 open InterpreterUtils
 open InterpreterExpansion
 open InterpreterPaths
+open Errors
 
 (** The local logger *)
 let log = Logging.expressions_log
@@ -29,14 +30,14 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
   (* Small helper *)
   let rec expand : cm_fun =
    fun cf ctx ->
-    let v = read_place access p ctx in
+    let v = read_place meta access p ctx in
     match
       find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v
     with
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx))
+          expand_symbolic_value_no_branching meta config sv (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -48,14 +49,14 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
     We also check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
-let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
+let read_place (meta : Meta.meta) (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
-  let v = read_place access p ctx in
+  let v = read_place meta access p ctx in
   (* Check that there are no bottoms in the value *)
-  assert (not (bottom_in_value ctx.ended_regions v));
+  cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value";
   (* Check that there are no reserved borrows in the value *)
-  assert (not (reserved_in_value v));
+  cassert (not (reserved_in_value v)) meta "There should be no reserved borrows in the value";
   (* Call the continuation *)
   cf v ctx
 
@@ -64,9 +65,9 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Make sure we can evaluate the path *)
-  let cc = update_ctx_along_read_place config access p in
+  let cc = update_ctx_along_read_place meta config access p in
   (* End the proper loans at the place itself *)
-  let cc = comp cc (end_loans_at_place config access p) in
+  let cc = comp cc (end_loans_at_place meta config access p) in
   (* Expand the copyable values which contain borrows (which are necessarily shared
    * borrows) *)
   let cc =
@@ -75,7 +76,7 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
-  let read_place = read_place access p in
+  let read_place = read_place meta access p in
   (* Compose *)
   comp cc read_place cf ctx
 
@@ -87,7 +88,7 @@ let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_c
     ctx
 
 (** Convert an operand constant operand value to a typed value *)
-let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value =
+let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal) : typed_value =
   (* Check the type while converting - we actually need some information
      * contained in the type *)
   log#ldebug
@@ -100,11 +101,11 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value =
   | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty }
   | TInteger int_ty, VScalar v ->
       (* Check the type and the ranges *)
-      assert (int_ty = v.int_ty);
-      assert (check_scalar_value_in_range v);
+      cassert (int_ty = v.int_ty) meta "Wrong type TODO: error message";
+      cassert (check_scalar_value_in_range v) meta "Wrong range TODO: error message";
       { value = VLiteral (VScalar v); ty = TLiteral ty }
   (* Remaining cases (invalid) *)
-  | _, _ -> raise (Failure "Improperly typed constant value")
+  | _, _ -> craise meta "Improperly typed constant value"
 
 (** Copy a value, and return the resulting value.
 
@@ -117,13 +118,13 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value =
     parameter to control this copy ([allow_adt_copy]). Note that here by ADT we
     mean the user-defined ADTs (not tuples or assumed types).
  *)
-let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
+let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
     (v : typed_value) : eval_ctx * typed_value =
   log#ldebug
     (lazy
       ("copy_value: "
-      ^ typed_value_to_string ctx v
-      ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
+      ^ typed_value_to_string meta ctx v
+      ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx));
   (* Remark: at some point we rewrote this function to use iterators, but then
    * we reverted the changes: the result was less clear actually. In particular,
    * the fact that we have exhaustive matches below makes very obvious the cases
@@ -134,9 +135,9 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
       (* Sanity check *)
       (match v.ty with
       | TAdt (TAssumed TBox, _) ->
-          raise (Failure "Can't copy an assumed value other than Option")
+          craise meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-          assert (allow_adt_copy || ty_is_primitively_copyable ty)
+          cassert (allow_adt_copy || ty_is_primitively_copyable ty) meta "TODO: error message"
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -146,15 +147,15 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          assert (ty_is_primitively_copyable ty)
-      | _ -> raise (Failure "Unreachable"));
+          cassert (ty_is_primitively_copyable ty) meta "TODO: error message"
+      | _ -> craise meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
-          (copy_value allow_adt_copy config)
+          (copy_value meta allow_adt_copy config)
           ctx av.field_values
       in
       (ctx, { v with value = VAdt { av with field_values = fields } })
-  | VBottom -> raise (Failure "Can't copy ⊥")
+  | VBottom -> craise meta "Can't copy ⊥"
   | VBorrow bc -> (
       (* We can only copy shared borrows *)
       match bc with
@@ -162,24 +163,24 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
           (* We need to create a new borrow id for the copied borrow, and
            * update the context accordingly *)
           let bid' = fresh_borrow_id () in
-          let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
+          let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in
           (ctx, { v with value = VBorrow (VSharedBorrow bid') })
-      | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
+      | VMutBorrow (_, _) -> craise meta "Can't copy a mutable borrow"
       | VReservedMutBorrow _ ->
-          raise (Failure "Can't copy a reserved mut borrow"))
+          craise meta "Can't copy a reserved mut borrow")
   | VLoan lc -> (
       (* We can only copy shared loans *)
       match lc with
-      | VMutLoan _ -> raise (Failure "Can't copy a mutable loan")
+      | VMutLoan _ -> craise meta "Can't copy a mutable loan"
       | VSharedLoan (_, sv) ->
           (* We don't copy the shared loan: only the shared value inside *)
-          copy_value allow_adt_copy config ctx sv)
+          copy_value meta allow_adt_copy config ctx sv)
   | VSymbolic sp ->
       (* We can copy only if the type is "primitively" copyable.
        * Note that in the general case, copy is a trait: copying values
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
-      assert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty));
+      cassert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)) meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
        * is symbolic expansion. The important subcase is the expansion of shared
@@ -248,25 +249,25 @@ let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : o
   prepare cf ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
-let eval_operand_no_reorganize (config : config) (op : operand)
+let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operand)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
     (lazy
       ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op
-     ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+     ^ "\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* Evaluate *)
   match op with
   | Constant cv -> (
       match cv.value with
       | CLiteral lit ->
-          cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx
+          cf (literal_to_typed_value meta (ty_as_literal cv.ty) lit) ctx
       | CTraitConst (trait_ref, const_name) -> (
           let ctx0 = ctx in
           (* Simply introduce a fresh symbolic value *)
           let ty = cv.ty in
-          let v = mk_fresh_symbolic_typed_value ty in
+          let v = mk_fresh_symbolic_typed_value meta ty in
           (* Continue the evaluation *)
           let e = cf v ctx in
           (* Wrap the generated expression *)
@@ -277,7 +278,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                 (SymbolicAst.IntroSymbolic
                    ( ctx0,
                      None,
-                     value_as_symbolic v.value,
+                     value_as_symbolic meta v.value,
                      SymbolicAst.VaTraitConstValue (trait_ref, const_name),
                      e )))
       | CVar vid -> (
@@ -294,49 +295,49 @@ let eval_operand_no_reorganize (config : config) (op : operand)
             | ConcreteMode ->
                 (* Copy the value - this is more of a sanity check *)
                 let allow_adt_copy = false in
-                copy_value allow_adt_copy config ctx cv
+                copy_value meta allow_adt_copy config ctx cv
             | SymbolicMode ->
                 (* We use the looked up value only for its type *)
-                let v = mk_fresh_symbolic_typed_value cv.ty in
+                let v = mk_fresh_symbolic_typed_value meta cv.ty in
                 (ctx, v)
           in
           (* Continue *)
           let e = cf cv ctx in
           (* If we are synthesizing a symbolic AST, it means that we are in symbolic
              mode: the value of the const generic is necessarily symbolic. *)
-          assert (e = None || is_symbolic cv.value);
+          cassert (e = None || is_symbolic cv.value) meta "The value of the const generic should be symbolic";
           (* We have to wrap the generated expression *)
           match e with
           | None -> None
           | Some e ->
               (* If we are synthesizing a symbolic AST, it means that we are in symbolic
                  mode: the value of the const generic is necessarily symbolic. *)
-              assert (is_symbolic cv.value);
+              cassert (is_symbolic cv.value) meta "The value of the const generic should be symbolic";
               (* *)
               Some
                 (SymbolicAst.IntroSymbolic
                    ( ctx0,
                      None,
-                     value_as_symbolic cv.value,
+                     value_as_symbolic meta cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
-      | CFnPtr _ -> raise (Failure "TODO"))
+      | CFnPtr _ -> craise meta "TODO")
   | Copy p ->
       (* Access the value *)
       let access = Read in
-      let cc = read_place access p in
+      let cc = read_place meta access p in
       (* Copy the value *)
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        assert (not (bottom_in_value ctx.ended_regions v));
-        assert (
+        cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
+        cassert (
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
-               ctx.type_ctx.type_infos v));
+               ctx.type_ctx.type_infos v)) meta "TODO: error message";
         (* Actually perform the copy *)
         let allow_adt_copy = false in
-        let ctx, v = copy_value allow_adt_copy config ctx v in
+        let ctx, v = copy_value meta allow_adt_copy config ctx v in
         (* Continue *)
         cf v ctx
       in
@@ -345,14 +346,14 @@ let eval_operand_no_reorganize (config : config) (op : operand)
   | Move p ->
       (* Access the value *)
       let access = Move in
-      let cc = read_place access p in
+      let cc = read_place meta access p in
       (* Move the value *)
       let move cf v : m_fun =
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
-        assert (not (bottom_in_value ctx.ended_regions v));
+        cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
         let bottom : typed_value = { value = VBottom; ty = v.ty } in
-        let ctx = write_place access p bottom ctx in
+        let ctx = write_place meta access p bottom ctx in
         cf v ctx
       in
       (* Compose and apply *)
@@ -365,11 +366,11 @@ let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : type
   log#ldebug
     (lazy
       ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
-     ^ eval_ctx_to_string ctx ^ "\n"));
+     ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
     (prepare_eval_operand_reorganize meta config op)
-    (eval_operand_no_reorganize config op)
+    (eval_operand_no_reorganize meta config op)
     cf ctx
 
 (** Small utility.
@@ -388,7 +389,7 @@ let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
   let prepare = prepare_eval_operands_reorganize meta config ops in
   (* Evaluate the operands *)
   let eval =
-    fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
+    fold_left_list_apply_continuation (eval_operand_no_reorganize meta config) ops
   in
   (* Compose and apply *)
   comp prepare eval cf ctx
@@ -399,7 +400,7 @@ let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2
   let use_res cf res =
     match res with
     | [ v1; v2 ] -> cf (v1, v2)
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
   in
   comp eval_op use_res cf
 
@@ -420,7 +421,7 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o
     | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)),
         VLiteral (VScalar sv) ) -> (
         (* Cast between integers *)
-        assert (src_ty = sv.int_ty);
+        cassert (src_ty = sv.int_ty) meta "TODO: error message";
         let i = sv.value in
         match mk_scalar tgt_ty i with
         | Error _ -> cf (Error EPanic)
@@ -442,12 +443,12 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o
         let b =
           if Z.of_int 0 = sv.value then false
           else if Z.of_int 1 = sv.value then true
-          else raise (Failure "Conversion from int to bool: out of range")
+          else craise meta "Conversion from int to bool: out of range"
         in
         let value = VLiteral (VBool b) in
         let ty = TLiteral TBool in
         cf (Ok { ty; value })
-    | _ -> raise (Failure "Invalid input for unop")
+    | _ -> craise meta "Invalid input for unop"
   in
   comp eval_op apply cf
 
@@ -465,7 +466,7 @@ let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (o
       | Not, (TLiteral TBool as lty) -> lty
       | Neg, (TLiteral (TInteger _) as lty) -> lty
       | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
-      | _ -> raise (Failure "Invalid input for unop")
+      | _ -> craise meta "Invalid input for unop"
     in
     let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuation *)
@@ -487,15 +488,15 @@ let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : opera
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
  *)
-let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
+let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typed_value)
     (v2 : typed_value) : (typed_value, eval_error) result =
   (* Equality check binops (Eq, Ne) accept values from a wide variety of types.
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
-    assert (v1.ty = v2.ty);
+    cassert (v1.ty = v2.ty) meta "TODO: error message";
     (* Equality/inequality check is primitive only for a subset of types *)
-    assert (ty_is_primitively_copyable v1.ty);
+    cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
@@ -510,7 +511,7 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
         match binop with
         | Lt | Le | Ge | Gt ->
             (* The two operands must have the same type and the result is a boolean *)
-            assert (sv1.int_ty = sv2.int_ty);
+            cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is a boolean";
             let b =
               match binop with
               | Lt -> Z.lt sv1.value sv2.value
@@ -519,14 +520,14 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
               | Gt -> Z.gt sv1.value sv2.value
               | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
               | Shr | Ne | Eq ->
-                  raise (Failure "Unreachable")
+                  craise meta "Unreachable"
             in
             Ok
               ({ value = VLiteral (VBool b); ty = TLiteral TBool }
                 : typed_value)
         | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
             (* The two operands must have the same type and the result is an integer *)
-            assert (sv1.int_ty = sv2.int_ty);
+            cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is an integer";
             let res =
               match binop with
               | Div ->
@@ -543,7 +544,7 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
               | BitAnd -> raise Unimplemented
               | BitOr -> raise Unimplemented
               | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
-                  raise (Failure "Unreachable")
+                  craise meta "Unreachable"
             in
             match res with
             | Error _ -> Error EPanic
@@ -554,8 +555,8 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
                     ty = TLiteral (TInteger sv1.int_ty);
                   })
         | Shl | Shr -> raise Unimplemented
-        | Ne | Eq -> raise (Failure "Unreachable"))
-    | _ -> raise (Failure "Invalid inputs for binop")
+        | Ne | Eq -> craise meta "Unreachable")
+    | _ -> craise meta "Invalid inputs for binop"
 
 let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
@@ -564,7 +565,7 @@ let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop)
   (* Compute the result of the binop *)
   let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
-    cf (eval_binary_op_concrete_compute binop v1 v2)
+    cf (eval_binary_op_concrete_compute meta binop v1 v2)
   in
   (* Compose and apply *)
   comp eval_ops compute cf
@@ -582,9 +583,9 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop)
     let res_sv_ty =
       if binop = Eq || binop = Ne then (
         (* Equality operations *)
-        assert (v1.ty = v2.ty);
+        cassert (v1.ty = v2.ty) meta "TODO: error message";
         (* Equality/inequality check is primitive only for a subset of types *)
-        assert (ty_is_primitively_copyable v1.ty);
+        cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
         TLiteral TBool)
       else
         (* Other operations: input types are integers *)
@@ -592,17 +593,17 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop)
         | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
             match binop with
             | Lt | Le | Ge | Gt ->
-                assert (int_ty1 = int_ty2);
+                cassert (int_ty1 = int_ty2) meta "TODO: error message";
                 TLiteral TBool
             | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
-                assert (int_ty1 = int_ty2);
+                cassert (int_ty1 = int_ty2) meta "TODO: error message";
                 TLiteral (TInteger int_ty1)
             | Shl | Shr ->
                 (* The number of bits can be of a different integer type
                    than the operand *)
                 TLiteral (TInteger int_ty1)
-            | Ne | Eq -> raise (Failure "Unreachable"))
-        | _ -> raise (Failure "Invalid inputs for binop")
+            | Ne | Eq -> craise meta "Unreachable")
+        | _ -> craise meta "Invalid inputs for binop"
     in
     let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuattion *)
@@ -631,14 +632,14 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
          In practice this restricted the behaviour too much, so for now we
          forbid them.
       *)
-      assert (bkind <> BShallow);
+      cassert (bkind <> BShallow) meta "Shallow borrow are currently forbidden";
 
       (* Access the value *)
       let access =
         match bkind with
         | BShared | BShallow -> Read
         | BTwoPhaseMut -> Write
-        | _ -> raise (Failure "Unreachable")
+        | _ -> craise meta "Unreachable"
       in
 
       let expand_prim_copy = false in
@@ -663,14 +664,14 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
               { v with value = v' }
         in
         (* Update the borrowed value in the context *)
-        let ctx = write_place access p nv ctx in
+        let ctx = write_place meta access p nv ctx in
         (* Compute the rvalue - simply a shared borrow with a the fresh id.
          * Note that the reference is *mutable* if we do a two-phase borrow *)
         let ref_kind =
           match bkind with
           | BShared | BShallow -> RShared
           | BTwoPhaseMut -> RMut
-          | _ -> raise (Failure "Unreachable")
+          | _ -> craise meta "Unreachable"
         in
         let rv_ty = TRef (RErased, v.ty, ref_kind) in
         let bc =
@@ -680,7 +681,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
                  handle shallow borrows like shared borrows *)
               VSharedBorrow bid
           | BTwoPhaseMut -> VReservedMutBorrow bid
-          | _ -> raise (Failure "Unreachable")
+          | _ -> craise meta "Unreachable"
         in
         let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in
         (* Continue *)
@@ -707,7 +708,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
         (* Compute the value with which to replace the value at place p *)
         let nv = { v with value = VLoan (VMutLoan bid) } in
         (* Update the value in the context *)
-        let ctx = write_place access p nv ctx in
+        let ctx = write_place meta access p nv ctx in
         (* Continue *)
         cf rv ctx
       in
@@ -736,16 +737,16 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind :
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
-            assert (
+            cassert (
               List.length type_decl.generics.regions
-              = List.length generics.regions);
+              = List.length generics.regions) meta "TODO: error message";
             let expected_field_types =
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id
                 opt_variant_id generics
             in
-            assert (
+            cassert (
               expected_field_types
-              = List.map (fun (v : typed_value) -> v.ty) values);
+              = List.map (fun (v : typed_value) -> v.ty) values) meta "TODO: error message";
             (* Construct the value *)
             let av : adt_value =
               { variant_id = opt_variant_id; field_values = values }
@@ -754,13 +755,13 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind :
             let aggregated : typed_value = { value = VAdt av; ty = aty } in
             (* Call the continuation *)
             cf aggregated ctx
-        | TAssumed _ -> raise (Failure "Unreachable"))
+        | TAssumed _ -> craise meta "Unreachable")
     | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        assert (List.for_all (fun (v : typed_value) -> v.ty = ety) values);
+        cassert (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta "All the values do not have the proper type";
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        assert (len = Z.of_int (List.length values));
+        cassert (len = Z.of_int (List.length values)) meta "The number of values is not consistent with the length";
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
         let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
@@ -768,15 +769,15 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind :
            array we introduce here might be duplicated in the generated
            code: by introducing a symbolic value we introduce a let-binding
            in the generated code. *)
-        let saggregated = mk_fresh_symbolic_typed_value ty in
+        let saggregated = mk_fresh_symbolic_typed_value meta ty in
         (* Call the continuation *)
         match cf saggregated ctx with
         | None -> None
         | Some e ->
             (* Introduce the symbolic value in the AST *)
-            let sv = ValuesUtils.value_as_symbolic saggregated.value in
+            let sv = ValuesUtils.value_as_symbolic meta saggregated.value in
             Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
-    | AggregatedClosure _ -> raise (Failure "Closures are not supported yet")
+    | AggregatedClosure _ -> craise meta "Closures are not supported yet"
   in
   (* Compose and apply *)
   comp eval_ops compute cf
@@ -800,11 +801,11 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue
   | Aggregate (aggregate_kind, ops) ->
       comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
   | Discriminant _ ->
-      raise
-        (Failure
+      craise
+        meta
            "Unreachable: discriminant reads should have been eliminated from \
-            the AST")
-  | Global _ -> raise (Failure "Unreachable")
+            the AST"
+  | Global _ -> craise meta "Unreachable"
 
 let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
  fun cf ctx ->
@@ -814,7 +815,7 @@ let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-    assert (not (bottom_in_value ctx.ended_regions v));
+    cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
     cf ctx
   in
   comp cf_prepare cf_continue cf ctx
-- 
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/InterpreterExpressions.ml | 98 +++++++++++++++++++-------------------
 1 file changed, 49 insertions(+), 49 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index f82c7130..d74e0751 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -24,7 +24,7 @@ let log = Logging.expressions_log
     Note that the place should have been prepared so that there are no remaining
     loans.
 *)
-let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
+let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Small helper *)
@@ -37,7 +37,7 @@ let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching meta config sv (Some (mk_mplace meta p ctx))
+          expand_symbolic_value_no_branching config meta sv (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -60,19 +60,19 @@ let read_place (meta : Meta.meta) (access : access_kind) (p : place) (cf : typed
   (* Call the continuation *)
   cf v ctx
 
-let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
+let access_rplace_reorganize_and_read (config : config) (meta : Meta.meta)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Make sure we can evaluate the path *)
-  let cc = update_ctx_along_read_place meta config access p in
+  let cc = update_ctx_along_read_place config meta access p in
   (* End the proper loans at the place itself *)
-  let cc = comp cc (end_loans_at_place meta config access p) in
+  let cc = comp cc (end_loans_at_place config meta access p) in
   (* Expand the copyable values which contain borrows (which are necessarily shared
    * borrows) *)
   let cc =
     if expand_prim_copy then
-      comp cc (expand_primitively_copyable_at_place meta config access p)
+      comp cc (expand_primitively_copyable_at_place config meta access p)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -80,10 +80,10 @@ let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (config : config) (meta : Meta.meta) (expand_prim_copy : bool)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
-  access_rplace_reorganize_and_read meta config expand_prim_copy access p
+  access_rplace_reorganize_and_read config meta expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
@@ -225,7 +225,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta) (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
@@ -238,18 +238,18 @@ let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : o
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
-        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
     | Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
-        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
   in
   (* Apply *)
   prepare cf ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
-let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operand)
+let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operand)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
@@ -359,7 +359,7 @@ let eval_operand_no_reorganize (meta : Meta.meta) (config : config) (op : operan
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   (* Debug *)
@@ -369,34 +369,34 @@ let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : type
      ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
-    (prepare_eval_operand_reorganize meta config op)
-    (eval_operand_no_reorganize meta config op)
+    (prepare_eval_operand_reorganize config meta op)
+    (eval_operand_no_reorganize config meta op)
     cf ctx
 
 (** Small utility.
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta) (ops : operand list) :
     cm_fun =
-  fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
+  fold_left_apply_continuation (prepare_eval_operand_reorganize config meta) ops
 
 (** Evaluate several operands. *)
-let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
+let eval_operands (config : config) (meta : Meta.meta) (ops : operand list)
     (cf : typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
-  let prepare = prepare_eval_operands_reorganize meta config ops in
+  let prepare = prepare_eval_operands_reorganize config meta ops in
   (* Evaluate the operands *)
   let eval =
-    fold_left_list_apply_continuation (eval_operand_no_reorganize meta config) ops
+    fold_left_list_apply_continuation (eval_operand_no_reorganize config meta) ops
   in
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand) (op2 : operand)
     (cf : typed_value * typed_value -> m_fun) : m_fun =
-  let eval_op = eval_operands meta config [ op1; op2 ] in
+  let eval_op = eval_operands config meta [ op1; op2 ] in
   let use_res cf res =
     match res with
     | [ v1; v2 ] -> cf (v1, v2)
@@ -404,10 +404,10 @@ let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let eval_op = eval_operand meta config op in
+  let eval_op = eval_operand config meta op in
   (* Apply the unop *)
   let apply cf (v : typed_value) : m_fun =
     match (unop, v.value) with
@@ -452,11 +452,11 @@ let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (o
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand meta config op in
+  let eval_op = eval_operand config meta op in
   (* Generate a fresh symbolic value to store the result *)
   let apply cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -479,11 +479,11 @@ let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (o
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
+let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
-  | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
+  | ConcreteMode -> eval_unary_op_concrete config meta unop op cf
+  | SymbolicMode -> eval_unary_op_symbolic config meta unop op cf
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
@@ -558,10 +558,10 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
         | Ne | Eq -> craise meta "Unreachable")
     | _ -> craise meta "Invalid inputs for binop"
 
-let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands meta config op1 op2 in
+  let eval_ops = eval_two_operands config meta op1 op2 in
   (* Compute the result of the binop *)
   let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
@@ -570,11 +570,11 @@ let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands meta config op1 op2 in
+  let eval_ops = eval_two_operands config meta op1 op2 in
   (* Compute the result of applying the binop *)
   let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
    fun ctx ->
@@ -617,13 +617,13 @@ let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
-  | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 cf
+  | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 cf
 
-let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : borrow_kind)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
@@ -644,7 +644,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
 
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read meta config expand_prim_copy access p
+        access_rplace_reorganize_and_read config meta expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -694,7 +694,7 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
       let access = Write in
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read meta config expand_prim_copy access p
+        access_rplace_reorganize_and_read config meta expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -715,10 +715,10 @@ let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : bo
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind : aggregate_kind)
     (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_operands meta config ops in
+  let eval_ops = eval_operands config meta ops in
   (* Compute the value *)
   let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
    fun ctx ->
@@ -782,7 +782,7 @@ let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind :
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (config : config) (meta : Meta.meta) (rvalue : rvalue)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
@@ -794,12 +794,12 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue
   let comp_wrap f = comp f wrap_in_result cf in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> comp_wrap (eval_operand meta config op) ctx
-  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
-  | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
-  | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
+  | Use op -> comp_wrap (eval_operand config meta op) ctx
+  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config meta p bkind) ctx
+  | UnaryOp (unop, op) -> eval_unary_op config meta unop op cf ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op config meta binop op1 op2 cf ctx
   | Aggregate (aggregate_kind, ops) ->
-      comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
+      comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx
   | Discriminant _ ->
       craise
         meta
@@ -807,11 +807,11 @@ let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue
             the AST"
   | Global _ -> craise meta "Unreachable"
 
-let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
+let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
   let expand_prim_copy = false in
   let cf_prepare cf =
-    access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
+    access_rplace_reorganize_and_read config meta expand_prim_copy Read p cf
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-- 
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/InterpreterExpressions.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index d74e0751..6c4f8af5 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -741,7 +741,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
               List.length type_decl.generics.regions
               = List.length generics.regions) meta "TODO: error message";
             let expected_field_types =
-              AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id
+              AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
             in
             cassert (
-- 
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/InterpreterExpressions.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 6c4f8af5..3922a3ab 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -137,7 +137,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       | TAdt (TAssumed TBox, _) ->
           craise meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-          cassert (allow_adt_copy || ty_is_primitively_copyable ty) meta "TODO: error message"
+        sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -147,7 +147,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          cassert (ty_is_primitively_copyable ty) meta "TODO: error message"
+            sanity_check (ty_is_primitively_copyable ty) meta
       | _ -> craise meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
@@ -330,11 +330,11 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
-        cassert (
+        sanity_check (not (bottom_in_value ctx.ended_regions v)) meta;
+        sanity_check (
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
-               ctx.type_ctx.type_infos v)) meta "TODO: error message";
+               ctx.type_ctx.type_infos v)) meta;
         (* Actually perform the copy *)
         let allow_adt_copy = false in
         let ctx, v = copy_value meta allow_adt_copy config ctx v in
@@ -737,9 +737,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
-            cassert (
+            sanity_check (
               List.length type_decl.generics.regions
-              = List.length generics.regions) meta "TODO: error message";
+              = List.length generics.regions) meta;
             let expected_field_types =
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
@@ -758,10 +758,10 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAssumed _ -> craise meta "Unreachable")
     | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        cassert (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta "All the values do not have the proper type";
+        sanity_check (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta;
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        cassert (len = Z.of_int (List.length values)) meta "The number of values is not consistent with the length";
+        sanity_check (len = Z.of_int (List.length values)) meta;
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
         let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
-- 
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/InterpreterExpressions.ml | 68 +++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 3922a3ab..7045d886 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -101,8 +101,8 @@ let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
   | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty }
   | TInteger int_ty, VScalar v ->
       (* Check the type and the ranges *)
-      cassert (int_ty = v.int_ty) meta "Wrong type TODO: error message";
-      cassert (check_scalar_value_in_range v) meta "Wrong range TODO: error message";
+      sanity_check (int_ty = v.int_ty) meta;
+      sanity_check (check_scalar_value_in_range v) meta;
       { value = VLiteral (VScalar v); ty = TLiteral ty }
   (* Remaining cases (invalid) *)
   | _, _ -> craise meta "Improperly typed constant value"
@@ -123,8 +123,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
   log#ldebug
     (lazy
       ("copy_value: "
-      ^ typed_value_to_string meta ctx v
-      ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx));
+      ^ typed_value_to_string ~meta:(Some meta) ctx v
+      ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Remark: at some point we rewrote this function to use iterators, but then
    * we reverted the changes: the result was less clear actually. In particular,
    * the fact that we have exhaustive matches below makes very obvious the cases
@@ -135,7 +135,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       (* Sanity check *)
       (match v.ty with
       | TAdt (TAssumed TBox, _) ->
-          craise meta "Can't copy an assumed value other than Option"
+          exec_raise meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
         sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
       | TAdt (TTuple, _) -> () (* Ok *)
@@ -147,15 +147,15 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-            sanity_check (ty_is_primitively_copyable ty) meta
-      | _ -> craise meta "Unreachable");
+            exec_assert (ty_is_primitively_copyable ty) meta "The type is not primitively copyable"
+      | _ -> exec_raise meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
           (copy_value meta allow_adt_copy config)
           ctx av.field_values
       in
       (ctx, { v with value = VAdt { av with field_values = fields } })
-  | VBottom -> craise meta "Can't copy ⊥"
+  | VBottom -> exec_raise meta "Can't copy ⊥"
   | VBorrow bc -> (
       (* We can only copy shared borrows *)
       match bc with
@@ -165,13 +165,13 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
           let bid' = fresh_borrow_id () in
           let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in
           (ctx, { v with value = VBorrow (VSharedBorrow bid') })
-      | VMutBorrow (_, _) -> craise meta "Can't copy a mutable borrow"
+      | VMutBorrow (_, _) -> exec_raise meta "Can't copy a mutable borrow"
       | VReservedMutBorrow _ ->
-          craise meta "Can't copy a reserved mut borrow")
+          exec_raise meta "Can't copy a reserved mut borrow")
   | VLoan lc -> (
       (* We can only copy shared loans *)
       match lc with
-      | VMutLoan _ -> craise meta "Can't copy a mutable loan"
+      | VMutLoan _ -> exec_raise meta "Can't copy a mutable loan"
       | VSharedLoan (_, sv) ->
           (* We don't copy the shared loan: only the shared value inside *)
           copy_value meta allow_adt_copy config ctx sv)
@@ -256,7 +256,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
   log#ldebug
     (lazy
       ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op
-     ^ "\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+     ^ "\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
   (* Evaluate *)
   match op with
   | Constant cv -> (
@@ -305,14 +305,14 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
           let e = cf cv ctx in
           (* If we are synthesizing a symbolic AST, it means that we are in symbolic
              mode: the value of the const generic is necessarily symbolic. *)
-          cassert (e = None || is_symbolic cv.value) meta "The value of the const generic should be symbolic";
+          sanity_check (e = None || is_symbolic cv.value) meta;
           (* We have to wrap the generated expression *)
           match e with
           | None -> None
           | Some e ->
               (* If we are synthesizing a symbolic AST, it means that we are in symbolic
                  mode: the value of the const generic is necessarily symbolic. *)
-              cassert (is_symbolic cv.value) meta "The value of the const generic should be symbolic";
+              sanity_check (is_symbolic cv.value) meta;
               (* *)
               Some
                 (SymbolicAst.IntroSymbolic
@@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
                      value_as_symbolic meta cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
-      | CFnPtr _ -> craise meta "TODO")
+      | CFnPtr _ -> craise meta "TODO: error message")
   | Copy p ->
       (* Access the value *)
       let access = Read in
@@ -330,7 +330,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        sanity_check (not (bottom_in_value ctx.ended_regions v)) meta;
+        exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "Can not copy a value containing bottom";
         sanity_check (
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
@@ -351,7 +351,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let move cf v : m_fun =
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
-        cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
+        exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
         let bottom : typed_value = { value = VBottom; ty = v.ty } in
         let ctx = write_place meta access p bottom ctx in
         cf v ctx
@@ -366,7 +366,7 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed
   log#ldebug
     (lazy
       ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
-     ^ eval_ctx_to_string meta ctx ^ "\n"));
+     ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
     (prepare_eval_operand_reorganize config meta op)
@@ -421,7 +421,7 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o
     | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)),
         VLiteral (VScalar sv) ) -> (
         (* Cast between integers *)
-        cassert (src_ty = sv.int_ty) meta "TODO: error message";
+        sanity_check (src_ty = sv.int_ty) meta;
         let i = sv.value in
         match mk_scalar tgt_ty i with
         | Error _ -> cf (Error EPanic)
@@ -443,12 +443,12 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o
         let b =
           if Z.of_int 0 = sv.value then false
           else if Z.of_int 1 = sv.value then true
-          else craise meta "Conversion from int to bool: out of range"
+          else exec_raise meta "Conversion from int to bool: out of range"
         in
         let value = VLiteral (VBool b) in
         let ty = TLiteral TBool in
         cf (Ok { ty; value })
-    | _ -> craise meta "Invalid input for unop"
+    | _ -> exec_raise meta "Invalid input for unop"
   in
   comp eval_op apply cf
 
@@ -466,7 +466,7 @@ let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (o
       | Not, (TLiteral TBool as lty) -> lty
       | Neg, (TLiteral (TInteger _) as lty) -> lty
       | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
-      | _ -> craise meta "Invalid input for unop"
+      | _ -> exec_raise meta "Invalid input for unop"
     in
     let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuation *)
@@ -494,9 +494,9 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
-    cassert (v1.ty = v2.ty) meta "TODO: error message";
+    exec_assert (v1.ty = v2.ty) meta "TODO: error message";
     (* Equality/inequality check is primitive only for a subset of types *)
-    cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
+    exec_assert (ty_is_primitively_copyable v1.ty) meta "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
@@ -511,7 +511,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
         match binop with
         | Lt | Le | Ge | Gt ->
             (* The two operands must have the same type and the result is a boolean *)
-            cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is a boolean";
+            sanity_check (sv1.int_ty = sv2.int_ty) meta;
             let b =
               match binop with
               | Lt -> Z.lt sv1.value sv2.value
@@ -527,7 +527,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
                 : typed_value)
         | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
             (* The two operands must have the same type and the result is an integer *)
-            cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is an integer";
+            sanity_check (sv1.int_ty = sv2.int_ty) meta;
             let res =
               match binop with
               | Div ->
@@ -583,9 +583,9 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
     let res_sv_ty =
       if binop = Eq || binop = Ne then (
         (* Equality operations *)
-        cassert (v1.ty = v2.ty) meta "TODO: error message";
+        sanity_check (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
-        cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
+        exec_assert (ty_is_primitively_copyable v1.ty) meta "The type is not primitively copyable";
         TLiteral TBool)
       else
         (* Other operations: input types are integers *)
@@ -593,10 +593,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
             match binop with
             | Lt | Le | Ge | Gt ->
-                cassert (int_ty1 = int_ty2) meta "TODO: error message";
+                sanity_check (int_ty1 = int_ty2) meta;
                 TLiteral TBool
             | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
-                cassert (int_ty1 = int_ty2) meta "TODO: error message";
+                sanity_check (int_ty1 = int_ty2) meta;
                 TLiteral (TInteger int_ty1)
             | Shl | Shr ->
                 (* The number of bits can be of a different integer type
@@ -632,7 +632,7 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : bo
          In practice this restricted the behaviour too much, so for now we
          forbid them.
       *)
-      cassert (bkind <> BShallow) meta "Shallow borrow are currently forbidden";
+      sanity_check (bkind <> BShallow) meta;
 
       (* Access the value *)
       let access =
@@ -744,9 +744,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
             in
-            cassert (
+            sanity_check (
               expected_field_types
-              = List.map (fun (v : typed_value) -> v.ty) values) meta "TODO: error message";
+              = List.map (fun (v : typed_value) -> v.ty) values) meta;
             (* Construct the value *)
             let av : adt_value =
               { variant_id = opt_variant_id; field_values = values }
@@ -815,7 +815,7 @@ let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-    cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
+    cassert (not (bottom_in_value ctx.ended_regions v)) meta "Fake read: the value contains bottom";
     cf ctx
   in
   comp cf_prepare cf_continue cf ctx
-- 
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/InterpreterExpressions.ml | 174 ++++++++++++++++++++++---------------
 1 file changed, 104 insertions(+), 70 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 7045d886..3d01024b 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -37,7 +37,8 @@ let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config meta sv (Some (mk_mplace meta p ctx))
+          expand_symbolic_value_no_branching config meta sv
+            (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -49,14 +50,18 @@ let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta)
     We also check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
-let read_place (meta : Meta.meta) (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
-    m_fun =
+let read_place (meta : Meta.meta) (access : access_kind) (p : place)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   let v = read_place meta access p ctx in
   (* Check that there are no bottoms in the value *)
-  cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value";
+  cassert
+    (not (bottom_in_value ctx.ended_regions v))
+    meta "There should be no bottoms in the value";
   (* Check that there are no reserved borrows in the value *)
-  cassert (not (reserved_in_value v)) meta "There should be no reserved borrows in the value";
+  cassert
+    (not (reserved_in_value v))
+    meta "There should be no reserved borrows in the value";
   (* Call the continuation *)
   cf v ctx
 
@@ -80,15 +85,16 @@ let access_rplace_reorganize_and_read (config : config) (meta : Meta.meta)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (config : config) (meta : Meta.meta) (expand_prim_copy : bool)
-    (access : access_kind) (p : place) : cm_fun =
+let access_rplace_reorganize (config : config) (meta : Meta.meta)
+    (expand_prim_copy : bool) (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   access_rplace_reorganize_and_read config meta expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
 (** Convert an operand constant operand value to a typed value *)
-let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal) : typed_value =
+let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
+    : typed_value =
   (* Check the type while converting - we actually need some information
      * contained in the type *)
   log#ldebug
@@ -118,13 +124,14 @@ let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
     parameter to control this copy ([allow_adt_copy]). Note that here by ADT we
     mean the user-defined ADTs (not tuples or assumed types).
  *)
-let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
-    (v : typed_value) : eval_ctx * typed_value =
+let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
+    (ctx : eval_ctx) (v : typed_value) : eval_ctx * typed_value =
   log#ldebug
     (lazy
       ("copy_value: "
       ^ typed_value_to_string ~meta:(Some meta) ctx v
-      ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+      ^ "\n- context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Remark: at some point we rewrote this function to use iterators, but then
    * we reverted the changes: the result was less clear actually. In particular,
    * the fact that we have exhaustive matches below makes very obvious the cases
@@ -137,7 +144,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       | TAdt (TAssumed TBox, _) ->
           exec_raise meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-        sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
+          sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -147,7 +154,9 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-            exec_assert (ty_is_primitively_copyable ty) meta "The type is not primitively copyable"
+          exec_assert
+            (ty_is_primitively_copyable ty)
+            meta "The type is not primitively copyable"
       | _ -> exec_raise meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
@@ -180,7 +189,9 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
        * Note that in the general case, copy is a trait: copying values
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
-      cassert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)) meta "Not primitively copyable";
+      cassert
+        (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+        meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
        * is symbolic expansion. The important subcase is the expansion of shared
@@ -225,7 +236,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta)
+    (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
@@ -249,14 +261,16 @@ let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta) (op : o
   prepare cf ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
-let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operand)
-    (cf : typed_value -> m_fun) : m_fun =
+let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
+    (op : operand) (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
     (lazy
       ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op
-     ^ "\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+     ^ "\n- ctx:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n"));
   (* Evaluate *)
   match op with
   | Constant cv -> (
@@ -330,11 +344,14 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "Can not copy a value containing bottom";
-        sanity_check (
-          Option.is_none
-            (find_first_primitively_copyable_sv_with_borrows
-               ctx.type_ctx.type_infos v)) meta;
+        exec_assert
+          (not (bottom_in_value ctx.ended_regions v))
+          meta "Can not copy a value containing bottom";
+        sanity_check
+          (Option.is_none
+             (find_first_primitively_copyable_sv_with_borrows
+                ctx.type_ctx.type_infos v))
+          meta;
         (* Actually perform the copy *)
         let allow_adt_copy = false in
         let ctx, v = copy_value meta allow_adt_copy config ctx v in
@@ -351,7 +368,9 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let move cf v : m_fun =
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
-        exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
+        exec_assert
+          (not (bottom_in_value ctx.ended_regions v))
+          meta "There should be no bottoms in the value we are about to move";
         let bottom : typed_value = { value = VBottom; ty = v.ty } in
         let ctx = write_place meta access p bottom ctx in
         cf v ctx
@@ -359,14 +378,15 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed_value -> m_fun) :
-    m_fun =
+let eval_operand (config : config) (meta : Meta.meta) (op : operand)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
     (lazy
       ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
-     ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
     (prepare_eval_operand_reorganize config meta op)
@@ -377,8 +397,8 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta) (ops : operand list) :
-    cm_fun =
+let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta)
+    (ops : operand list) : cm_fun =
   fold_left_apply_continuation (prepare_eval_operand_reorganize config meta) ops
 
 (** Evaluate several operands. *)
@@ -389,23 +409,23 @@ let eval_operands (config : config) (meta : Meta.meta) (ops : operand list)
   let prepare = prepare_eval_operands_reorganize config meta ops in
   (* Evaluate the operands *)
   let eval =
-    fold_left_list_apply_continuation (eval_operand_no_reorganize config meta) ops
+    fold_left_list_apply_continuation
+      (eval_operand_no_reorganize config meta)
+      ops
   in
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand) (op2 : operand)
-    (cf : typed_value * typed_value -> m_fun) : m_fun =
+let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand)
+    (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun =
   let eval_op = eval_operands config meta [ op1; op2 ] in
   let use_res cf res =
-    match res with
-    | [ v1; v2 ] -> cf (v1, v2)
-    | _ -> craise meta "Unreachable"
+    match res with [ v1; v2 ] -> cf (v1, v2) | _ -> craise meta "Unreachable"
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
+    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
   let eval_op = eval_operand config meta op in
   (* Apply the unop *)
@@ -452,8 +472,8 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop)
+    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
   let eval_op = eval_operand config meta op in
@@ -479,8 +499,8 @@ let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (o
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop) (op : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop)
+    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
   | ConcreteMode -> eval_unary_op_concrete config meta unop op cf
   | SymbolicMode -> eval_unary_op_symbolic config meta unop op cf
@@ -488,15 +508,17 @@ let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop) (op : opera
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
  *)
-let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typed_value)
-    (v2 : typed_value) : (typed_value, eval_error) result =
+let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
+    (v1 : typed_value) (v2 : typed_value) : (typed_value, eval_error) result =
   (* Equality check binops (Eq, Ne) accept values from a wide variety of types.
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
     exec_assert (v1.ty = v2.ty) meta "TODO: error message";
     (* Equality/inequality check is primitive only for a subset of types *)
-    exec_assert (ty_is_primitively_copyable v1.ty) meta "Type is not primitively copyable";
+    exec_assert
+      (ty_is_primitively_copyable v1.ty)
+      meta "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
@@ -558,8 +580,9 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
         | Ne | Eq -> craise meta "Unreachable")
     | _ -> craise meta "Invalid inputs for binop"
 
-let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
-    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop)
+    (op1 : operand) (op2 : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
   let eval_ops = eval_two_operands config meta op1 op2 in
   (* Compute the result of the binop *)
@@ -570,8 +593,9 @@ let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
-    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
+    (op1 : operand) (op2 : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
   let eval_ops = eval_two_operands config meta op1 op2 in
@@ -585,7 +609,9 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         (* Equality operations *)
         sanity_check (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
-        exec_assert (ty_is_primitively_copyable v1.ty) meta "The type is not primitively copyable";
+        exec_assert
+          (ty_is_primitively_copyable v1.ty)
+          meta "The type is not primitively copyable";
         TLiteral TBool)
       else
         (* Other operations: input types are integers *)
@@ -617,14 +643,15 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop) (op1 : operand)
-    (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop)
+    (op1 : operand) (op2 : operand)
+    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
   | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 cf
   | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 cf
 
-let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : borrow_kind)
-    (cf : typed_value -> m_fun) : m_fun =
+let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
+    (bkind : borrow_kind) (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
   | BShared | BTwoPhaseMut | BShallow ->
@@ -715,8 +742,9 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : bo
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind : aggregate_kind)
-    (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
+let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
+    (aggregate_kind : aggregate_kind) (ops : operand list)
+    (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
   let eval_ops = eval_operands config meta ops in
   (* Compute the value *)
@@ -737,16 +765,18 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
-            sanity_check (
-              List.length type_decl.generics.regions
-              = List.length generics.regions) meta;
+            sanity_check
+              (List.length type_decl.generics.regions
+              = List.length generics.regions)
+              meta;
             let expected_field_types =
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
             in
-            sanity_check (
-              expected_field_types
-              = List.map (fun (v : typed_value) -> v.ty) values) meta;
+            sanity_check
+              (expected_field_types
+              = List.map (fun (v : typed_value) -> v.ty) values)
+              meta;
             (* Construct the value *)
             let av : adt_value =
               { variant_id = opt_variant_id; field_values = values }
@@ -758,7 +788,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAssumed _ -> craise meta "Unreachable")
     | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        sanity_check (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta;
+        sanity_check
+          (List.for_all (fun (v : typed_value) -> v.ty = ety) values)
+          meta;
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
         sanity_check (len = Z.of_int (List.length values)) meta;
@@ -782,8 +814,8 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (config : config) (meta : Meta.meta) (rvalue : rvalue)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+let eval_rvalue_not_global (config : config) (meta : Meta.meta)
+    (rvalue : rvalue) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
   (* Small helpers *)
@@ -797,14 +829,14 @@ let eval_rvalue_not_global (config : config) (meta : Meta.meta) (rvalue : rvalue
   | Use op -> comp_wrap (eval_operand config meta op) ctx
   | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config meta p bkind) ctx
   | UnaryOp (unop, op) -> eval_unary_op config meta unop op cf ctx
-  | BinaryOp (binop, op1, op2) -> eval_binary_op config meta binop op1 op2 cf ctx
+  | BinaryOp (binop, op1, op2) ->
+      eval_binary_op config meta binop op1 op2 cf ctx
   | Aggregate (aggregate_kind, ops) ->
       comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx
   | Discriminant _ ->
-      craise
-        meta
-           "Unreachable: discriminant reads should have been eliminated from \
-            the AST"
+      craise meta
+        "Unreachable: discriminant reads should have been eliminated from the \
+         AST"
   | Global _ -> craise meta "Unreachable"
 
 let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
@@ -815,7 +847,9 @@ let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-    cassert (not (bottom_in_value ctx.ended_regions v)) meta "Fake read: the value contains bottom";
+    cassert
+      (not (bottom_in_value ctx.ended_regions v))
+      meta "Fake read: the value contains bottom";
     cf ctx
   in
   comp cf_prepare cf_continue cf ctx
-- 
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/InterpreterExpressions.ml | 104 ++++++++++++++++++-------------------
 1 file changed, 52 insertions(+), 52 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 3d01024b..59f74ad8 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -55,11 +55,11 @@ let read_place (meta : Meta.meta) (access : access_kind) (p : place)
  fun ctx ->
   let v = read_place meta access p ctx in
   (* Check that there are no bottoms in the value *)
-  cassert
+  cassert __FILE__ __LINE__
     (not (bottom_in_value ctx.ended_regions v))
     meta "There should be no bottoms in the value";
   (* Check that there are no reserved borrows in the value *)
-  cassert
+  cassert __FILE__ __LINE__
     (not (reserved_in_value v))
     meta "There should be no reserved borrows in the value";
   (* Call the continuation *)
@@ -107,11 +107,11 @@ let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
   | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty }
   | TInteger int_ty, VScalar v ->
       (* Check the type and the ranges *)
-      sanity_check (int_ty = v.int_ty) meta;
-      sanity_check (check_scalar_value_in_range v) meta;
+      sanity_check __FILE__ __LINE__ (int_ty = v.int_ty) meta;
+      sanity_check __FILE__ __LINE__ (check_scalar_value_in_range v) meta;
       { value = VLiteral (VScalar v); ty = TLiteral ty }
   (* Remaining cases (invalid) *)
-  | _, _ -> craise meta "Improperly typed constant value"
+  | _, _ -> craise __FILE__ __LINE__ meta "Improperly typed constant value"
 
 (** Copy a value, and return the resulting value.
 
@@ -142,9 +142,9 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       (* Sanity check *)
       (match v.ty with
       | TAdt (TAssumed TBox, _) ->
-          exec_raise meta "Can't copy an assumed value other than Option"
+          exec_raise __FILE__ __LINE__ meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-          sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
+          sanity_check __FILE__ __LINE__ (allow_adt_copy || ty_is_primitively_copyable ty) meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -154,17 +154,17 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          exec_assert
+          exec_assert __FILE__ __LINE__
             (ty_is_primitively_copyable ty)
             meta "The type is not primitively copyable"
-      | _ -> exec_raise meta "Unreachable");
+      | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
           (copy_value meta allow_adt_copy config)
           ctx av.field_values
       in
       (ctx, { v with value = VAdt { av with field_values = fields } })
-  | VBottom -> exec_raise meta "Can't copy ⊥"
+  | VBottom -> exec_raise __FILE__ __LINE__ meta "Can't copy ⊥"
   | VBorrow bc -> (
       (* We can only copy shared borrows *)
       match bc with
@@ -174,13 +174,13 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
           let bid' = fresh_borrow_id () in
           let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in
           (ctx, { v with value = VBorrow (VSharedBorrow bid') })
-      | VMutBorrow (_, _) -> exec_raise meta "Can't copy a mutable borrow"
+      | VMutBorrow (_, _) -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable borrow"
       | VReservedMutBorrow _ ->
-          exec_raise meta "Can't copy a reserved mut borrow")
+          exec_raise __FILE__ __LINE__ meta "Can't copy a reserved mut borrow")
   | VLoan lc -> (
       (* We can only copy shared loans *)
       match lc with
-      | VMutLoan _ -> exec_raise meta "Can't copy a mutable loan"
+      | VMutLoan _ -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable loan"
       | VSharedLoan (_, sv) ->
           (* We don't copy the shared loan: only the shared value inside *)
           copy_value meta allow_adt_copy config ctx sv)
@@ -189,7 +189,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
        * Note that in the general case, copy is a trait: copying values
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
-      cassert
+      cassert __FILE__ __LINE__
         (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
         meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
@@ -319,14 +319,14 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
           let e = cf cv ctx in
           (* If we are synthesizing a symbolic AST, it means that we are in symbolic
              mode: the value of the const generic is necessarily symbolic. *)
-          sanity_check (e = None || is_symbolic cv.value) meta;
+          sanity_check __FILE__ __LINE__ (e = None || is_symbolic cv.value) meta;
           (* We have to wrap the generated expression *)
           match e with
           | None -> None
           | Some e ->
               (* If we are synthesizing a symbolic AST, it means that we are in symbolic
                  mode: the value of the const generic is necessarily symbolic. *)
-              sanity_check (is_symbolic cv.value) meta;
+              sanity_check __FILE__ __LINE__ (is_symbolic cv.value) meta;
               (* *)
               Some
                 (SymbolicAst.IntroSymbolic
@@ -335,7 +335,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
                      value_as_symbolic meta cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
-      | CFnPtr _ -> craise meta "TODO: error message")
+      | CFnPtr _ -> craise __FILE__ __LINE__ meta "TODO: error message")
   | Copy p ->
       (* Access the value *)
       let access = Read in
@@ -344,10 +344,10 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        exec_assert
+        exec_assert __FILE__ __LINE__
           (not (bottom_in_value ctx.ended_regions v))
           meta "Can not copy a value containing bottom";
-        sanity_check
+        sanity_check __FILE__ __LINE__
           (Option.is_none
              (find_first_primitively_copyable_sv_with_borrows
                 ctx.type_ctx.type_infos v))
@@ -368,7 +368,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
       let move cf v : m_fun =
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
-        exec_assert
+        exec_assert __FILE__ __LINE__
           (not (bottom_in_value ctx.ended_regions v))
           meta "There should be no bottoms in the value we are about to move";
         let bottom : typed_value = { value = VBottom; ty = v.ty } in
@@ -420,7 +420,7 @@ let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand)
     (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun =
   let eval_op = eval_operands config meta [ op1; op2 ] in
   let use_res cf res =
-    match res with [ v1; v2 ] -> cf (v1, v2) | _ -> craise meta "Unreachable"
+    match res with [ v1; v2 ] -> cf (v1, v2) | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
   comp eval_op use_res cf
 
@@ -441,7 +441,7 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
     | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)),
         VLiteral (VScalar sv) ) -> (
         (* Cast between integers *)
-        sanity_check (src_ty = sv.int_ty) meta;
+        sanity_check __FILE__ __LINE__ (src_ty = sv.int_ty) meta;
         let i = sv.value in
         match mk_scalar tgt_ty i with
         | Error _ -> cf (Error EPanic)
@@ -463,12 +463,12 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
         let b =
           if Z.of_int 0 = sv.value then false
           else if Z.of_int 1 = sv.value then true
-          else exec_raise meta "Conversion from int to bool: out of range"
+          else exec_raise __FILE__ __LINE__ meta "Conversion from int to bool: out of range"
         in
         let value = VLiteral (VBool b) in
         let ty = TLiteral TBool in
         cf (Ok { ty; value })
-    | _ -> exec_raise meta "Invalid input for unop"
+    | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop"
   in
   comp eval_op apply cf
 
@@ -486,7 +486,7 @@ let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop)
       | Not, (TLiteral TBool as lty) -> lty
       | Neg, (TLiteral (TInteger _) as lty) -> lty
       | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
-      | _ -> exec_raise meta "Invalid input for unop"
+      | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop"
     in
     let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuation *)
@@ -514,9 +514,9 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
-    exec_assert (v1.ty = v2.ty) meta "TODO: error message";
+    exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "TODO: error message";
     (* Equality/inequality check is primitive only for a subset of types *)
-    exec_assert
+    exec_assert __FILE__ __LINE__
       (ty_is_primitively_copyable v1.ty)
       meta "Type is not primitively copyable";
     let b = v1 = v2 in
@@ -533,7 +533,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
         match binop with
         | Lt | Le | Ge | Gt ->
             (* The two operands must have the same type and the result is a boolean *)
-            sanity_check (sv1.int_ty = sv2.int_ty) meta;
+            sanity_check __FILE__ __LINE__ (sv1.int_ty = sv2.int_ty) meta;
             let b =
               match binop with
               | Lt -> Z.lt sv1.value sv2.value
@@ -542,14 +542,14 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
               | Gt -> Z.gt sv1.value sv2.value
               | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
               | Shr | Ne | Eq ->
-                  craise meta "Unreachable"
+                  craise __FILE__ __LINE__ meta "Unreachable"
             in
             Ok
               ({ value = VLiteral (VBool b); ty = TLiteral TBool }
                 : typed_value)
         | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
             (* The two operands must have the same type and the result is an integer *)
-            sanity_check (sv1.int_ty = sv2.int_ty) meta;
+            sanity_check __FILE__ __LINE__ (sv1.int_ty = sv2.int_ty) meta;
             let res =
               match binop with
               | Div ->
@@ -566,7 +566,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
               | BitAnd -> raise Unimplemented
               | BitOr -> raise Unimplemented
               | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
-                  craise meta "Unreachable"
+                  craise __FILE__ __LINE__ meta "Unreachable"
             in
             match res with
             | Error _ -> Error EPanic
@@ -577,8 +577,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
                     ty = TLiteral (TInteger sv1.int_ty);
                   })
         | Shl | Shr -> raise Unimplemented
-        | Ne | Eq -> craise meta "Unreachable")
-    | _ -> craise meta "Invalid inputs for binop"
+        | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
+    | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
 
 let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop)
     (op1 : operand) (op2 : operand)
@@ -607,9 +607,9 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
     let res_sv_ty =
       if binop = Eq || binop = Ne then (
         (* Equality operations *)
-        sanity_check (v1.ty = v2.ty) meta;
+        sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
-        exec_assert
+        exec_assert __FILE__ __LINE__
           (ty_is_primitively_copyable v1.ty)
           meta "The type is not primitively copyable";
         TLiteral TBool)
@@ -619,17 +619,17 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
             match binop with
             | Lt | Le | Ge | Gt ->
-                sanity_check (int_ty1 = int_ty2) meta;
+                sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
                 TLiteral TBool
             | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
-                sanity_check (int_ty1 = int_ty2) meta;
+                sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
                 TLiteral (TInteger int_ty1)
             | Shl | Shr ->
                 (* The number of bits can be of a different integer type
                    than the operand *)
                 TLiteral (TInteger int_ty1)
-            | Ne | Eq -> craise meta "Unreachable")
-        | _ -> craise meta "Invalid inputs for binop"
+            | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
+        | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
     in
     let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuattion *)
@@ -659,14 +659,14 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
          In practice this restricted the behaviour too much, so for now we
          forbid them.
       *)
-      sanity_check (bkind <> BShallow) meta;
+      sanity_check __FILE__ __LINE__ (bkind <> BShallow) meta;
 
       (* Access the value *)
       let access =
         match bkind with
         | BShared | BShallow -> Read
         | BTwoPhaseMut -> Write
-        | _ -> craise meta "Unreachable"
+        | _ -> craise __FILE__ __LINE__ meta "Unreachable"
       in
 
       let expand_prim_copy = false in
@@ -698,7 +698,7 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
           match bkind with
           | BShared | BShallow -> RShared
           | BTwoPhaseMut -> RMut
-          | _ -> craise meta "Unreachable"
+          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         let rv_ty = TRef (RErased, v.ty, ref_kind) in
         let bc =
@@ -708,7 +708,7 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
                  handle shallow borrows like shared borrows *)
               VSharedBorrow bid
           | BTwoPhaseMut -> VReservedMutBorrow bid
-          | _ -> craise meta "Unreachable"
+          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in
         (* Continue *)
@@ -765,7 +765,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
-            sanity_check
+            sanity_check __FILE__ __LINE__
               (List.length type_decl.generics.regions
               = List.length generics.regions)
               meta;
@@ -773,7 +773,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
             in
-            sanity_check
+            sanity_check __FILE__ __LINE__
               (expected_field_types
               = List.map (fun (v : typed_value) -> v.ty) values)
               meta;
@@ -785,15 +785,15 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
             let aggregated : typed_value = { value = VAdt av; ty = aty } in
             (* Call the continuation *)
             cf aggregated ctx
-        | TAssumed _ -> craise meta "Unreachable")
+        | TAssumed _ -> craise __FILE__ __LINE__ meta "Unreachable")
     | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        sanity_check
+        sanity_check __FILE__ __LINE__
           (List.for_all (fun (v : typed_value) -> v.ty = ety) values)
           meta;
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        sanity_check (len = Z.of_int (List.length values)) meta;
+        sanity_check __FILE__ __LINE__ (len = Z.of_int (List.length values)) meta;
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
         let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
@@ -809,7 +809,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
             (* Introduce the symbolic value in the AST *)
             let sv = ValuesUtils.value_as_symbolic meta saggregated.value in
             Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
-    | AggregatedClosure _ -> craise meta "Closures are not supported yet"
+    | AggregatedClosure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet"
   in
   (* Compose and apply *)
   comp eval_ops compute cf
@@ -834,10 +834,10 @@ let eval_rvalue_not_global (config : config) (meta : Meta.meta)
   | Aggregate (aggregate_kind, ops) ->
       comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx
   | Discriminant _ ->
-      craise meta
+      craise __FILE__ __LINE__ meta
         "Unreachable: discriminant reads should have been eliminated from the \
          AST"
-  | Global _ -> craise meta "Unreachable"
+  | Global _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
 let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
@@ -847,7 +847,7 @@ let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
-    cassert
+    cassert __FILE__ __LINE__
       (not (bottom_in_value ctx.ended_regions v))
       meta "Fake read: the value contains bottom";
     cf 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/InterpreterExpressions.ml | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 59f74ad8..d61ba410 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -142,9 +142,12 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       (* Sanity check *)
       (match v.ty with
       | TAdt (TAssumed TBox, _) ->
-          exec_raise __FILE__ __LINE__ meta "Can't copy an assumed value other than Option"
+          exec_raise __FILE__ __LINE__ meta
+            "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-          sanity_check __FILE__ __LINE__ (allow_adt_copy || ty_is_primitively_copyable ty) meta
+          sanity_check __FILE__ __LINE__
+            (allow_adt_copy || ty_is_primitively_copyable ty)
+            meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -174,13 +177,15 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
           let bid' = fresh_borrow_id () in
           let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in
           (ctx, { v with value = VBorrow (VSharedBorrow bid') })
-      | VMutBorrow (_, _) -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable borrow"
+      | VMutBorrow (_, _) ->
+          exec_raise __FILE__ __LINE__ meta "Can't copy a mutable borrow"
       | VReservedMutBorrow _ ->
           exec_raise __FILE__ __LINE__ meta "Can't copy a reserved mut borrow")
   | VLoan lc -> (
       (* We can only copy shared loans *)
       match lc with
-      | VMutLoan _ -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable loan"
+      | VMutLoan _ ->
+          exec_raise __FILE__ __LINE__ meta "Can't copy a mutable loan"
       | VSharedLoan (_, sv) ->
           (* We don't copy the shared loan: only the shared value inside *)
           copy_value meta allow_adt_copy config ctx sv)
@@ -420,7 +425,9 @@ let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand)
     (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun =
   let eval_op = eval_operands config meta [ op1; op2 ] in
   let use_res cf res =
-    match res with [ v1; v2 ] -> cf (v1, v2) | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+    match res with
+    | [ v1; v2 ] -> cf (v1, v2)
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
   comp eval_op use_res cf
 
@@ -463,7 +470,9 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
         let b =
           if Z.of_int 0 = sv.value then false
           else if Z.of_int 1 = sv.value then true
-          else exec_raise __FILE__ __LINE__ meta "Conversion from int to bool: out of range"
+          else
+            exec_raise __FILE__ __LINE__ meta
+              "Conversion from int to bool: out of range"
         in
         let value = VLiteral (VBool b) in
         let ty = TLiteral TBool in
@@ -793,7 +802,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
           meta;
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        sanity_check __FILE__ __LINE__ (len = Z.of_int (List.length values)) meta;
+        sanity_check __FILE__ __LINE__
+          (len = Z.of_int (List.length values))
+          meta;
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
         let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
@@ -809,7 +820,8 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
             (* Introduce the symbolic value in the AST *)
             let sv = ValuesUtils.value_as_symbolic meta saggregated.value in
             Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
-    | AggregatedClosure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet"
+    | AggregatedClosure _ ->
+        craise __FILE__ __LINE__ meta "Closures are not supported yet"
   in
   (* Compose and apply *)
   comp eval_ops compute cf
-- 
cgit v1.2.3


From 5809c45fbbfcbb78b15a97be619dcde4ab4868b8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 16:21:15 +0100
Subject: Add some error messages

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

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index d61ba410..48a1cce6 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -340,7 +340,9 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
                      value_as_symbolic meta cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
-      | CFnPtr _ -> craise __FILE__ __LINE__ meta "TODO: error message")
+      | CFnPtr _ ->
+          craise __FILE__ __LINE__ meta
+            "Function pointers are not supported yet")
   | Copy p ->
       (* Access the value *)
       let access = Read in
@@ -523,7 +525,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
    * The remaining binops only operate on scalars. *)
   if binop = Eq || binop = Ne then (
     (* Equality operations *)
-    exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "TODO: error message";
+    exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
+      "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
     exec_assert __FILE__ __LINE__
       (ty_is_primitively_copyable v1.ty)
-- 
cgit v1.2.3