Move some functions from Interpreter to InterpreterExpressions

2 files changed, 477 insertions, 437 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 4ca7d58f..73967f61 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -17,6 +17,7 @@ open InterpreterProjectors
 open InterpreterBorrows
 open InterpreterExpansion
 open InterpreterPaths
+open InterpreterExpressions
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -33,443 +34,6 @@ open InterpreterPaths
 
 (* TODO: remove the config parameters when they are useless *)
 
-(** TODO: change the name *)
-type eval_error = Panic
-
-type 'a eval_result = ('a, eval_error) result
-
-(** Convert a constant operand value to a typed value *)
-let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
-    (cv : E.operand_constant_value) : V.typed_value =
-  (* Check the type while converting *)
-  match (ty, cv) with
-  (* Unit *)
-  | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value
-  (* Adt with one variant and no fields *)
-  | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' ->
-      assert (def_id = def_id');
-      (* Check that the adt definition only has one variant with no fields,
-         compute the variant id at the same time. *)
-      let def = C.ctx_lookup_type_def ctx def_id in
-      assert (List.length def.region_params = 0);
-      assert (List.length def.type_params = 0);
-      let variant_id =
-        match def.kind with
-        | Struct fields ->
-            assert (List.length fields = 0);
-            None
-        | Enum variants ->
-            assert (List.length variants = 1);
-            let variant_id = T.VariantId.zero in
-            let variant = T.VariantId.nth variants variant_id in
-            assert (List.length variant.fields = 0);
-            Some variant_id
-      in
-      let value = V.Adt { variant_id; field_values = [] } in
-      { value; ty }
-  (* Scalar, boolean... *)
-  | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
-  | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty }
-  | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty }
-  | T.Integer int_ty, ConstantValue (V.Scalar v) ->
-      (* Check the type and the ranges *)
-      assert (int_ty == v.int_ty);
-      assert (check_scalar_value_in_range v);
-      { V.value = V.Concrete (V.Scalar v); ty }
-  (* Remaining cases (invalid) - listing as much as we can on purpose
-     (allows to catch errors at compilation if the definitions change) *)
-  | _, Unit | _, ConstantAdt _ | _, ConstantValue _ ->
-      failwith "Improperly typed constant value"
-
-(** Small utility *)
-let prepare_rplace (config : C.config) (access : access_kind) (p : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
-  let ctx = update_ctx_along_read_place config access p ctx in
-  let ctx = end_loans_at_place config access p ctx in
-  let v = read_place_unwrap config access p ctx in
-  (ctx, v)
-
-(** Prepare the evaluation of an operand. *)
-let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
-    : C.eval_ctx * V.typed_value =
-  let ctx, v =
-    match op with
-    | Expressions.Constant (ty, cv) ->
-        let v = constant_value_to_typed_value ctx ty cv in
-        (ctx, v)
-    | Expressions.Copy p ->
-        (* Access the value *)
-        let access = Read in
-        prepare_rplace config access p ctx
-    | Expressions.Move p ->
-        (* Access the value *)
-        let access = Move in
-        prepare_rplace config access p ctx
-  in
-  assert (not (bottom_in_value v));
-  (ctx, v)
-
-(** Evaluate an operand. *)
-let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
-    C.eval_ctx * V.typed_value =
-  (* Debug *)
-  L.log#ldebug
-    (lazy
-      ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n"
-     ^ operand_to_string ctx op ^ "\n"));
-  (* Evaluate *)
-  match op with
-  | Expressions.Constant (ty, cv) ->
-      let v = constant_value_to_typed_value ctx ty cv in
-      (ctx, v)
-  | Expressions.Copy p ->
-      (* Access the value *)
-      let access = Read in
-      let ctx, v = prepare_rplace config access p ctx in
-      (* Copy the value *)
-      L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v));
-      assert (not (bottom_in_value v));
-      let allow_adt_copy = false in
-      copy_value allow_adt_copy config ctx v
-  | Expressions.Move p -> (
-      (* Access the value *)
-      let access = Move in
-      let ctx, v = prepare_rplace config access p ctx in
-      (* Move the value *)
-      L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v));
-      assert (not (bottom_in_value v));
-      let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
-      match write_place config access p bottom ctx with
-      | Error _ -> failwith "Unreachable"
-      | Ok ctx -> (ctx, v))
-
-(** Evaluate several operands. *)
-let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list)
-    : C.eval_ctx * V.typed_value list =
-  List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops
-
-let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand)
-    (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value =
-  match eval_operands config ctx [ op1; op2 ] with
-  | ctx, [ v1; v2 ] -> (ctx, v1, v2)
-  | _ -> failwith "Unreachable"
-
-let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx)
-    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
-    =
-  (* Evaluate the operand *)
-  let ctx, v = eval_operand config ctx op in
-  (* Apply the unop *)
-  match (unop, v.V.value) with
-  | E.Not, V.Concrete (Bool b) ->
-      Ok (ctx, { v with V.value = V.Concrete (Bool (not b)) })
-  | E.Neg, V.Concrete (V.Scalar sv) -> (
-      let i = Z.neg sv.V.value in
-      match mk_scalar sv.int_ty i with
-      | Error _ -> Error Panic
-      | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) }))
-  | _ -> failwith "Invalid input for unop"
-
-let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
-    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
-    =
-  (* Evaluate the operand *)
-  let ctx, v = eval_operand config ctx op in
-  (* Generate a fresh symbolic value to store the result *)
-  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
-  let res_sv_ty =
-    match (unop, v.V.ty) with
-    | E.Not, T.Bool -> T.Bool
-    | E.Neg, T.Integer int_ty -> T.Integer int_ty
-    | _ -> failwith "Invalid input for unop"
-  in
-  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
-  (* Synthesize *)
-  S.synthesize_unary_op unop v res_sv;
-  (* Return *)
-  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
-
-let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop)
-    (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
-  match config.mode with
-  | C.ConcreteMode -> eval_unary_op_concrete config ctx unop op
-  | C.SymbolicMode -> eval_unary_op_symbolic config ctx unop op
-
-let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx)
-    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
-    (C.eval_ctx * V.typed_value) eval_result =
-  (* Evaluate the operands *)
-  let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
-  (* 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);
-    (* Equality/inequality check is primitive only for a subset of types *)
-    assert (type_is_primitively_copyable v1.ty);
-    let b = v1 = v2 in
-    Ok (ctx, { V.value = V.Concrete (Bool b); ty = T.Bool }))
-  else
-    (* For the non-equality operations, the input values are necessarily scalars *)
-    match (v1.V.value, v2.V.value) with
-    | V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> (
-        let res =
-          (* There are binops which require the two operands to have the same
-             type, and binops for which it is not the case.
-             There are also binops which return booleans, and binops which
-             return integers.
-          *)
-          match binop with
-          | E.Lt | E.Le | E.Ge | E.Gt ->
-              (* The two operands must have the same type and the result is a boolean *)
-              assert (sv1.int_ty = sv2.int_ty);
-              let b =
-                match binop with
-                | E.Lt -> Z.lt sv1.V.value sv2.V.value
-                | E.Le -> Z.leq sv1.V.value sv2.V.value
-                | E.Ge -> Z.geq sv1.V.value sv2.V.value
-                | E.Gt -> Z.gt sv1.V.value sv2.V.value
-                | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
-                | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
-                    failwith "Unreachable"
-              in
-              Ok
-                ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
-          | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
-          | E.BitOr -> (
-              (* The two operands must have the same type and the result is an integer *)
-              assert (sv1.int_ty = sv2.int_ty);
-              let res =
-                match binop with
-                | E.Div ->
-                    if sv2.V.value = Z.zero then Error ()
-                    else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value)
-                | E.Rem ->
-                    (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
-                    if sv2.V.value = Z.zero then Error ()
-                    else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value)
-                | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value)
-                | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value)
-                | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value)
-                | E.BitXor -> raise Unimplemented
-                | E.BitAnd -> raise Unimplemented
-                | E.BitOr -> raise Unimplemented
-                | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq ->
-                    failwith "Unreachable"
-              in
-              match res with
-              | Error err -> Error err
-              | Ok sv ->
-                  Ok
-                    {
-                      V.value = V.Concrete (V.Scalar sv);
-                      ty = Integer sv1.int_ty;
-                    })
-          | E.Shl | E.Shr -> raise Unimplemented
-          | E.Ne | E.Eq -> failwith "Unreachable"
-        in
-        match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v))
-    | _ -> failwith "Invalid inputs for binop"
-
-let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
-    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
-    (C.eval_ctx * V.typed_value) eval_result =
-  (* Evaluate the operands *)
-  let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
-  (* Generate a fresh symbolic value to store the result *)
-  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
-  let res_sv_ty =
-    if binop = Eq || binop = Ne then (
-      (* Equality operations *)
-      assert (v1.ty = v2.ty);
-      (* Equality/inequality check is primitive only for a subset of types *)
-      assert (type_is_primitively_copyable v1.ty);
-      T.Bool)
-    else
-      (* Other operations: input types are integers *)
-      match (v1.V.ty, v2.V.ty) with
-      | T.Integer int_ty1, T.Integer int_ty2 -> (
-          match binop with
-          | E.Lt | E.Le | E.Ge | E.Gt ->
-              assert (int_ty1 = int_ty2);
-              T.Bool
-          | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
-          | E.BitOr ->
-              assert (int_ty1 = int_ty2);
-              T.Integer int_ty1
-          | E.Shl | E.Shr -> raise Unimplemented
-          | E.Ne | E.Eq -> failwith "Unreachable")
-      | _ -> failwith "Invalid inputs for binop"
-  in
-  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
-  (* Synthesize *)
-  S.synthesize_binary_op binop v1 v2 res_sv;
-  (* Return *)
-  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
-
-let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
-    (op1 : E.operand) (op2 : E.operand) :
-    (C.eval_ctx * V.typed_value) eval_result =
-  match config.mode with
-  | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
-  | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
-
-(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *)
-let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
-  (* Note that discriminant values have type `isize` *)
-  (* Access the value *)
-  let access = Read in
-  let ctx, v = prepare_rplace config access p ctx in
-  match v.V.value with
-  | Adt av -> (
-      match av.variant_id with
-      | None ->
-          failwith "Invalid input for `discriminant`: structure instead of enum"
-      | Some variant_id -> (
-          let id = Z.of_int (T.VariantId.to_int variant_id) in
-          match mk_scalar Isize id with
-          | Error _ ->
-              failwith "Disciminant id out of range"
-              (* Should really never happen *)
-          | Ok sv ->
-              (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
-      )
-  | _ -> failwith "Invalid input for `discriminant`"
-
-let eval_rvalue_discriminant (config : C.config) (p : E.place)
-    (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list =
-  S.synthesize_eval_rvalue_discriminant p;
-  (* Note that discriminant values have type `isize` *)
-  (* Access the value *)
-  let access = Read in
-  let ctx, v = prepare_rplace config access p ctx in
-  match v.V.value with
-  | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ]
-  | Symbolic sv ->
-      (* Expand the symbolic value - may lead to branching *)
-      let ctxl = expand_symbolic_enum_value config sv ctx in
-      (* This time the value is concrete: reevaluate *)
-      List.map (eval_rvalue_discriminant_concrete config p) ctxl
-  | _ -> failwith "Invalid input for `discriminant`"
-
-let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
-    (bkind : E.borrow_kind) : C.eval_ctx * V.typed_value =
-  S.synthesize_eval_rvalue_ref p bkind;
-  match bkind with
-  | E.Shared | E.TwoPhaseMut ->
-      (* Access the value *)
-      let access = if bkind = E.Shared then Read else Write in
-      let ctx, v = prepare_rplace config access p ctx in
-      (* Compute the rvalue - simply a shared borrow with a fresh id *)
-      let ctx, bid = C.fresh_borrow_id ctx in
-      (* Note that the reference is *mutable* if we do a two-phase borrow *)
-      let rv_ty =
-        T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
-      in
-      let bc =
-        if bkind = E.Shared then V.SharedBorrow bid
-        else V.InactivatedMutBorrow bid
-      in
-      let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
-      (* Compute the value with which to replace the value at place p *)
-      let nv =
-        match v.V.value with
-        | V.Loan (V.SharedLoan (bids, sv)) ->
-            (* Shared loan: insert the new borrow id *)
-            let bids1 = V.BorrowId.Set.add bid bids in
-            { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
-        | _ ->
-            (* Not a shared loan: add a wrapper *)
-            let v' = V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) in
-            { v with V.value = v' }
-      in
-      (* Update the value in the context *)
-      let ctx = write_place_unwrap config access p nv ctx in
-      (* Return *)
-      (ctx, rv)
-  | E.Mut ->
-      (* Access the value *)
-      let access = Write in
-      let ctx, v = prepare_rplace config access p ctx in
-      (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
-      let ctx, bid = C.fresh_borrow_id ctx in
-      let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
-      let rv : V.typed_value =
-        { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
-      in
-      (* Compute the value with which to replace the value at place p *)
-      let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
-      (* Update the value in the context *)
-      let ctx = write_place_unwrap config access p nv ctx in
-      (* Return *)
-      (ctx, rv)
-
-let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
-    (aggregate_kind : E.aggregate_kind) (ops : E.operand list) :
-    C.eval_ctx * V.typed_value =
-  S.synthesize_eval_rvalue_aggregate aggregate_kind ops;
-  (* Evaluate the operands *)
-  let ctx, values = eval_operands config ctx ops in
-  (* Match on the aggregate kind *)
-  match aggregate_kind with
-  | E.AggregatedTuple ->
-      let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
-      let v = V.Adt { variant_id = None; field_values = values } in
-      let ty = T.Adt (T.Tuple, [], tys) in
-      (ctx, { V.value = v; ty })
-  | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
-      (* Sanity checks *)
-      let type_def = C.ctx_lookup_type_def ctx def_id in
-      assert (List.length type_def.region_params = List.length regions);
-      let expected_field_types =
-        Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
-          types
-      in
-      assert (
-        expected_field_types
-        = List.map (fun (v : V.typed_value) -> v.V.ty) values);
-      (* Construct the value *)
-      let av : V.adt_value =
-        { V.variant_id = opt_variant_id; V.field_values = values }
-      in
-      let aty = T.Adt (T.AdtId def_id, regions, types) in
-      (ctx, { V.value = Adt av; ty = aty })
-
-(** Evaluate an rvalue which is not a discriminant.
-
-    We define a function for this specific case, because evaluating
-    a discriminant might lead to branching (if we evaluate the discriminant
-    of a symbolic enumeration value), while it is not the case for the
-    other rvalues.
- *)
-let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
-    (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result =
-  match rvalue with
-  | E.Use op -> Ok (eval_operand config ctx op)
-  | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind)
-  | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op
-  | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
-  | E.Aggregate (aggregate_kind, ops) ->
-      Ok (eval_rvalue_aggregate config ctx aggregate_kind ops)
-  | E.Discriminant _ -> failwith "Unreachable"
-
-(** Evaluate an rvalue in a given context: return the updated context and
-    the computed value.
-
-    Returns a list of pairs (new context, computed rvalue) because
-    `discriminant` might lead to a branching in case it is applied
-    on a symbolic enumeration value.
-*)
-let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
-    (C.eval_ctx * V.typed_value) list eval_result =
-  match rvalue with
-  | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx)
-  | _ -> (
-      match eval_rvalue_non_discriminant config ctx rvalue with
-      | Error e -> Error e
-      | Ok res -> Ok [ res ])
-
 (** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return
 
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
new file mode 100644
index 00000000..41eda802
--- /dev/null
+++ b/src/InterpreterExpressions.ml
@@ -0,0 +1,476 @@
+module T = Types
+module V = Values
+open Scalars
+module E = Expressions
+open Errors
+module C = Contexts
+module Subst = Substitute
+module A = CfimAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = Synthesis
+open Utils
+open InterpreterUtils
+open InterpreterProjectors
+open InterpreterBorrows
+open InterpreterExpansion
+open InterpreterPaths
+
+(** TODO: change the name *)
+type eval_error = Panic
+
+type 'a eval_result = ('a, eval_error) result
+
+(** Convert a constant operand value to a typed value *)
+let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
+    (cv : E.operand_constant_value) : V.typed_value =
+  (* Check the type while converting *)
+  match (ty, cv) with
+  (* Unit *)
+  | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value
+  (* Adt with one variant and no fields *)
+  | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' ->
+      assert (def_id = def_id');
+      (* Check that the adt definition only has one variant with no fields,
+         compute the variant id at the same time. *)
+      let def = C.ctx_lookup_type_def ctx def_id in
+      assert (List.length def.region_params = 0);
+      assert (List.length def.type_params = 0);
+      let variant_id =
+        match def.kind with
+        | Struct fields ->
+            assert (List.length fields = 0);
+            None
+        | Enum variants ->
+            assert (List.length variants = 1);
+            let variant_id = T.VariantId.zero in
+            let variant = T.VariantId.nth variants variant_id in
+            assert (List.length variant.fields = 0);
+            Some variant_id
+      in
+      let value = V.Adt { variant_id; field_values = [] } in
+      { value; ty }
+  (* Scalar, boolean... *)
+  | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
+  | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty }
+  | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty }
+  | T.Integer int_ty, ConstantValue (V.Scalar v) ->
+      (* Check the type and the ranges *)
+      assert (int_ty == v.int_ty);
+      assert (check_scalar_value_in_range v);
+      { V.value = V.Concrete (V.Scalar v); ty }
+  (* Remaining cases (invalid) - listing as much as we can on purpose
+     (allows to catch errors at compilation if the definitions change) *)
+  | _, Unit | _, ConstantAdt _ | _, ConstantValue _ ->
+      failwith "Improperly typed constant value"
+
+(** Small utility *)
+let prepare_rplace (config : C.config) (access : access_kind) (p : E.place)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  let ctx = update_ctx_along_read_place config access p ctx in
+  let ctx = end_loans_at_place config access p ctx in
+  let v = read_place_unwrap config access p ctx in
+  (ctx, v)
+
+(** Prepare the evaluation of an operand. *)
+let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
+    : C.eval_ctx * V.typed_value =
+  let ctx, v =
+    match op with
+    | Expressions.Constant (ty, cv) ->
+        let v = constant_value_to_typed_value ctx ty cv in
+        (ctx, v)
+    | Expressions.Copy p ->
+        (* Access the value *)
+        let access = Read in
+        prepare_rplace config access p ctx
+    | Expressions.Move p ->
+        (* Access the value *)
+        let access = Move in
+        prepare_rplace config access p ctx
+  in
+  assert (not (bottom_in_value v));
+  (ctx, v)
+
+(** Evaluate an operand. *)
+let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
+    C.eval_ctx * V.typed_value =
+  (* Debug *)
+  L.log#ldebug
+    (lazy
+      ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n"
+     ^ operand_to_string ctx op ^ "\n"));
+  (* Evaluate *)
+  match op with
+  | Expressions.Constant (ty, cv) ->
+      let v = constant_value_to_typed_value ctx ty cv in
+      (ctx, v)
+  | Expressions.Copy p ->
+      (* Access the value *)
+      let access = Read in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Copy the value *)
+      L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v));
+      assert (not (bottom_in_value v));
+      let allow_adt_copy = false in
+      copy_value allow_adt_copy config ctx v
+  | Expressions.Move p -> (
+      (* Access the value *)
+      let access = Move in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Move the value *)
+      L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v));
+      assert (not (bottom_in_value v));
+      let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
+      match write_place config access p bottom ctx with
+      | Error _ -> failwith "Unreachable"
+      | Ok ctx -> (ctx, v))
+
+(** Evaluate several operands. *)
+let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list)
+    : C.eval_ctx * V.typed_value list =
+  List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops
+
+let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand)
+    (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value =
+  match eval_operands config ctx [ op1; op2 ] with
+  | ctx, [ v1; v2 ] -> (ctx, v1, v2)
+  | _ -> failwith "Unreachable"
+
+let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx)
+    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
+    =
+  (* Evaluate the operand *)
+  let ctx, v = eval_operand config ctx op in
+  (* Apply the unop *)
+  match (unop, v.V.value) with
+  | E.Not, V.Concrete (Bool b) ->
+      Ok (ctx, { v with V.value = V.Concrete (Bool (not b)) })
+  | E.Neg, V.Concrete (V.Scalar sv) -> (
+      let i = Z.neg sv.V.value in
+      match mk_scalar sv.int_ty i with
+      | Error _ -> Error Panic
+      | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) }))
+  | _ -> failwith "Invalid input for unop"
+
+let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
+    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
+    =
+  (* Evaluate the operand *)
+  let ctx, v = eval_operand config ctx op in
+  (* Generate a fresh symbolic value to store the result *)
+  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
+  let res_sv_ty =
+    match (unop, v.V.ty) with
+    | E.Not, T.Bool -> T.Bool
+    | E.Neg, T.Integer int_ty -> T.Integer int_ty
+    | _ -> failwith "Invalid input for unop"
+  in
+  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  (* Synthesize *)
+  S.synthesize_unary_op unop v res_sv;
+  (* Return *)
+  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
+
+let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop)
+    (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
+  match config.mode with
+  | C.ConcreteMode -> eval_unary_op_concrete config ctx unop op
+  | C.SymbolicMode -> eval_unary_op_symbolic config ctx unop op
+
+let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx)
+    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
+    (C.eval_ctx * V.typed_value) eval_result =
+  (* Evaluate the operands *)
+  let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
+  (* 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);
+    (* Equality/inequality check is primitive only for a subset of types *)
+    assert (type_is_primitively_copyable v1.ty);
+    let b = v1 = v2 in
+    Ok (ctx, { V.value = V.Concrete (Bool b); ty = T.Bool }))
+  else
+    (* For the non-equality operations, the input values are necessarily scalars *)
+    match (v1.V.value, v2.V.value) with
+    | V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> (
+        let res =
+          (* There are binops which require the two operands to have the same
+             type, and binops for which it is not the case.
+             There are also binops which return booleans, and binops which
+             return integers.
+          *)
+          match binop with
+          | E.Lt | E.Le | E.Ge | E.Gt ->
+              (* The two operands must have the same type and the result is a boolean *)
+              assert (sv1.int_ty = sv2.int_ty);
+              let b =
+                match binop with
+                | E.Lt -> Z.lt sv1.V.value sv2.V.value
+                | E.Le -> Z.leq sv1.V.value sv2.V.value
+                | E.Ge -> Z.geq sv1.V.value sv2.V.value
+                | E.Gt -> Z.gt sv1.V.value sv2.V.value
+                | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
+                | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
+                    failwith "Unreachable"
+              in
+              Ok
+                ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
+          | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
+          | E.BitOr -> (
+              (* The two operands must have the same type and the result is an integer *)
+              assert (sv1.int_ty = sv2.int_ty);
+              let res =
+                match binop with
+                | E.Div ->
+                    if sv2.V.value = Z.zero then Error ()
+                    else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value)
+                | E.Rem ->
+                    (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
+                    if sv2.V.value = Z.zero then Error ()
+                    else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value)
+                | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value)
+                | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value)
+                | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value)
+                | E.BitXor -> raise Unimplemented
+                | E.BitAnd -> raise Unimplemented
+                | E.BitOr -> raise Unimplemented
+                | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq ->
+                    failwith "Unreachable"
+              in
+              match res with
+              | Error err -> Error err
+              | Ok sv ->
+                  Ok
+                    {
+                      V.value = V.Concrete (V.Scalar sv);
+                      ty = Integer sv1.int_ty;
+                    })
+          | E.Shl | E.Shr -> raise Unimplemented
+          | E.Ne | E.Eq -> failwith "Unreachable"
+        in
+        match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v))
+    | _ -> failwith "Invalid inputs for binop"
+
+let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
+    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
+    (C.eval_ctx * V.typed_value) eval_result =
+  (* Evaluate the operands *)
+  let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
+  (* Generate a fresh symbolic value to store the result *)
+  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
+  let res_sv_ty =
+    if binop = Eq || binop = Ne then (
+      (* Equality operations *)
+      assert (v1.ty = v2.ty);
+      (* Equality/inequality check is primitive only for a subset of types *)
+      assert (type_is_primitively_copyable v1.ty);
+      T.Bool)
+    else
+      (* Other operations: input types are integers *)
+      match (v1.V.ty, v2.V.ty) with
+      | T.Integer int_ty1, T.Integer int_ty2 -> (
+          match binop with
+          | E.Lt | E.Le | E.Ge | E.Gt ->
+              assert (int_ty1 = int_ty2);
+              T.Bool
+          | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
+          | E.BitOr ->
+              assert (int_ty1 = int_ty2);
+              T.Integer int_ty1
+          | E.Shl | E.Shr -> raise Unimplemented
+          | E.Ne | E.Eq -> failwith "Unreachable")
+      | _ -> failwith "Invalid inputs for binop"
+  in
+  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  (* Synthesize *)
+  S.synthesize_binary_op binop v1 v2 res_sv;
+  (* Return *)
+  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
+
+let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
+    (op1 : E.operand) (op2 : E.operand) :
+    (C.eval_ctx * V.typed_value) eval_result =
+  match config.mode with
+  | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
+  | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
+
+(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *)
+let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  (* Note that discriminant values have type `isize` *)
+  (* Access the value *)
+  let access = Read in
+  let ctx, v = prepare_rplace config access p ctx in
+  match v.V.value with
+  | Adt av -> (
+      match av.variant_id with
+      | None ->
+          failwith "Invalid input for `discriminant`: structure instead of enum"
+      | Some variant_id -> (
+          let id = Z.of_int (T.VariantId.to_int variant_id) in
+          match mk_scalar Isize id with
+          | Error _ ->
+              failwith "Disciminant id out of range"
+              (* Should really never happen *)
+          | Ok sv ->
+              (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
+      )
+  | _ -> failwith "Invalid input for `discriminant`"
+
+let eval_rvalue_discriminant (config : C.config) (p : E.place)
+    (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list =
+  S.synthesize_eval_rvalue_discriminant p;
+  (* Note that discriminant values have type `isize` *)
+  (* Access the value *)
+  let access = Read in
+  let ctx, v = prepare_rplace config access p ctx in
+  match v.V.value with
+  | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ]
+  | Symbolic sv ->
+      (* Expand the symbolic value - may lead to branching *)
+      let ctxl = expand_symbolic_enum_value config sv ctx in
+      (* This time the value is concrete: reevaluate *)
+      List.map (eval_rvalue_discriminant_concrete config p) ctxl
+  | _ -> failwith "Invalid input for `discriminant`"
+
+let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
+    (bkind : E.borrow_kind) : C.eval_ctx * V.typed_value =
+  S.synthesize_eval_rvalue_ref p bkind;
+  match bkind with
+  | E.Shared | E.TwoPhaseMut ->
+      (* Access the value *)
+      let access = if bkind = E.Shared then Read else Write in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Compute the rvalue - simply a shared borrow with a fresh id *)
+      let ctx, bid = C.fresh_borrow_id ctx in
+      (* Note that the reference is *mutable* if we do a two-phase borrow *)
+      let rv_ty =
+        T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+      in
+      let bc =
+        if bkind = E.Shared then V.SharedBorrow bid
+        else V.InactivatedMutBorrow bid
+      in
+      let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
+      (* Compute the value with which to replace the value at place p *)
+      let nv =
+        match v.V.value with
+        | V.Loan (V.SharedLoan (bids, sv)) ->
+            (* Shared loan: insert the new borrow id *)
+            let bids1 = V.BorrowId.Set.add bid bids in
+            { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
+        | _ ->
+            (* Not a shared loan: add a wrapper *)
+            let v' = V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) in
+            { v with V.value = v' }
+      in
+      (* Update the value in the context *)
+      let ctx = write_place_unwrap config access p nv ctx in
+      (* Return *)
+      (ctx, rv)
+  | E.Mut ->
+      (* Access the value *)
+      let access = Write in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
+      let ctx, bid = C.fresh_borrow_id ctx in
+      let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
+      let rv : V.typed_value =
+        { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
+      in
+      (* Compute the value with which to replace the value at place p *)
+      let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
+      (* Update the value in the context *)
+      let ctx = write_place_unwrap config access p nv ctx in
+      (* Return *)
+      (ctx, rv)
+
+let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
+    (aggregate_kind : E.aggregate_kind) (ops : E.operand list) :
+    C.eval_ctx * V.typed_value =
+  S.synthesize_eval_rvalue_aggregate aggregate_kind ops;
+  (* Evaluate the operands *)
+  let ctx, values = eval_operands config ctx ops in
+  (* Match on the aggregate kind *)
+  match aggregate_kind with
+  | E.AggregatedTuple ->
+      let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+      let v = V.Adt { variant_id = None; field_values = values } in
+      let ty = T.Adt (T.Tuple, [], tys) in
+      (ctx, { V.value = v; ty })
+  | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
+      (* Sanity checks *)
+      let type_def = C.ctx_lookup_type_def ctx def_id in
+      assert (List.length type_def.region_params = List.length regions);
+      let expected_field_types =
+        Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
+          types
+      in
+      assert (
+        expected_field_types
+        = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+      (* Construct the value *)
+      let av : V.adt_value =
+        { V.variant_id = opt_variant_id; V.field_values = values }
+      in
+      let aty = T.Adt (T.AdtId def_id, regions, types) in
+      (ctx, { V.value = Adt av; ty = aty })
+
+(** Evaluate an rvalue which is not a discriminant.
+
+    We define a function for this specific case, because evaluating
+    a discriminant might lead to branching (if we evaluate the discriminant
+    of a symbolic enumeration value), while it is not the case for the
+    other rvalues.
+ *)
+let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
+    (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result =
+  match rvalue with
+  | E.Use op -> Ok (eval_operand config ctx op)
+  | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind)
+  | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op
+  | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
+  | E.Aggregate (aggregate_kind, ops) ->
+      Ok (eval_rvalue_aggregate config ctx aggregate_kind ops)
+  | E.Discriminant _ -> failwith "Unreachable"
+
+(** Evaluate an rvalue in a given context: return the updated context and
+    the computed value.
+
+    Returns a list of pairs (new context, computed rvalue) because
+    `discriminant` might lead to a branching in case it is applied
+    on a symbolic enumeration value.
+*)
+let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
+    (C.eval_ctx * V.typed_value) list eval_result =
+  match rvalue with
+  | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx)
+  | _ -> (
+      match eval_rvalue_non_discriminant config ctx rvalue with
+      | Error e -> Error e
+      | Ok res -> Ok [ res ])
+
+(** Drop a value at a given place *)
+let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
+    =
+  L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
+  (* Prepare the place (by ending the loans, then the borrows) *)
+  let ctx, v = prepare_lplace config p ctx in
+  (* Replace the value with [Bottom] *)
+  let nv = { v with value = V.Bottom } in
+  let ctx = write_place_unwrap config Write p nv ctx in
+  ctx
+
+(** Assign a value to a given place *)
+let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
+    (p : E.place) : C.eval_ctx =
+  (* Prepare the destination *)
+  let ctx, _ = prepare_lplace config p ctx in
+  (* Update the destination *)
+  let ctx = write_place_unwrap config Write p v ctx in
+  ctx