Start working on greedy symbolic value expansion and expansion before

assignment

12 files changed, 318 insertions, 67 deletions

diff --git a/TODO.md b/TODO.md
index fdebe51f..c56c91a9 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,13 +1,13 @@
 # TODO
 
-1. add a switch to allow general symbolic values (containing references, etc.)
-  or not.
-
-2. expand symbolic values which are primitively copyable upon using them as
+1. expand symbolic values which are primitively copyable upon using them as
   function arguments or putting them in the return value, in order to deduplicate
   those values.
 
-4. add a check in function inputs: ok to take as parameters symbolic values with
+2. add a switch to allow general symbolic values (containing references, etc.)
+  or not.
+
+3. add a check in function inputs: ok to take as parameters symbolic values with
   borrow parameters *if* they come from the "input abstractions".
   In order to do this, add a symbolic value kind (would make things easier than
   adding ad-hoc lookups...): `FunRet`, `FunGivenBack`, `SynthInput`, `SynthGivenBack`
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 6eafd9ef..8a9c4857 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -3,6 +3,7 @@ open Values
 open CfimAst
 module V = Values
 open ValuesUtils
+module M = Modules
 
 (** Some global counters.
  *
@@ -104,10 +105,42 @@ type env = env_elem list
 
 type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
 
-type config = { mode : interpreter_mode; check_invariants : bool }
+type config = {
+  mode : interpreter_mode;
+      (** Concrete mode (interpreter) or symbolic mode (for synthesis) **)
+  check_invariants : bool;
+      (** Check that invariants are maintained whenever we execute a statement *)
+  greedy_expand_symbolics_with_borrows : bool;
+      (** Expand all symbolic values containing borrows upon introduction - allows
+          to use restrict ourselves to a simpler model for the projectors over
+          symbolic values.
+          The interpreter fails if doing this requires to do a branching (because
+          we need to expand an enumeration with strictly more than one variant)
+          or if we need to expand a recursive type (because this leads to looping).
+       *)
+}
 [@@deriving show]
 
-type type_context = { type_defs : type_def list } [@@deriving show]
+type partial_config = {
+  check_invariants : bool;
+  greedy_expand_symbolics_with_borrows : bool;
+}
+(** See [config] *)
+
+let config_of_partial (mode : interpreter_mode) (config : partial_config) :
+    config =
+  {
+    mode;
+    check_invariants = config.check_invariants;
+    greedy_expand_symbolics_with_borrows =
+      config.greedy_expand_symbolics_with_borrows;
+  }
+
+type type_context = {
+  type_defs_groups : M.types_decl_group TypeDefId.map_t;
+  type_defs : type_def list;
+}
+[@@deriving show]
 
 type eval_ctx = {
   type_context : type_context;
@@ -137,9 +170,11 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   in
   lookup ctx.env
 
+(** TODO: make this more efficient with maps *)
 let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def =
   TypeDefId.nth ctx.type_context.type_defs tid
 
+(** TODO: make this more efficient with maps *)
 let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def =
   FunDefId.nth ctx.fun_context fid
 
@@ -269,6 +304,10 @@ let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
 let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
   env_lookup_abs ctx.env abs_id
 
+let ctx_type_def_is_rec (ctx : eval_ctx) (id : TypeDefId.id) : bool =
+  let decl_group = TypeDefId.Map.find id ctx.type_context.type_defs_groups in
+  match decl_group with M.Rec _ -> true | M.NonRec _ -> false
+
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
   object (self : 'self)
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 18b8edee..c6d7ea10 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -12,6 +12,8 @@ module type Id = sig
 
   type set_t
 
+  type +!'a map_t
+
   val zero : id
 
   val generator_zero : generator
@@ -55,13 +57,18 @@ module type Id = sig
 
   val show_set_t : set_t -> string
 
+  val pp_map_t :
+    (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a map_t -> unit
+
+  val show_map_t : ('a -> string) -> 'a map_t -> string
+
   module Ord : Map.OrderedType with type t = id
 
   module Set : Set.S with type elt = id with type t = set_t
 
   val set_to_string : Set.t -> string
 
-  module Map : Map.S with type key = id
+  module Map : Map.S with type key = id with type 'a t = 'a map_t
 
   (* TODO: map_to_string *)
 
@@ -134,12 +141,37 @@ module IdGen () : Id = struct
 
   type set_t = Set.t
 
+  type +!'a map_t = 'a Map.t
+
   let show_set_t s =
     let ids = Set.fold (fun id s -> to_string id :: s) s [] in
     let ids = List.rev ids in
     "{" ^ String.concat "," ids ^ "}"
 
-  let pp_set_t fmt s = Format.pp_print_string fmt (show_set_t s)
+  let pp_set_t fmt s =
+    let pp_string = Format.pp_print_string fmt in
+    pp_string "{";
+    Set.iter (fun id -> pp_string (to_string id ^ ",")) s;
+    pp_string "}"
+
+  let show_map_t show_a s =
+    let ids =
+      Map.fold (fun id x s -> (to_string id ^ " -> " ^ show_a x) :: s) s []
+    in
+    let ids = List.rev ids in
+    "{" ^ String.concat "," ids ^ "}"
+
+  let pp_map_t (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter)
+      (m : 'a map_t) : unit =
+    let pp_string = Format.pp_print_string fmt in
+    pp_string "{";
+    Map.iter
+      (fun id x ->
+        pp_string (to_string id ^ " -> ");
+        pp_a fmt x;
+        pp_string ",")
+      m;
+    pp_string "}"
 
   let set_to_string ids =
     let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ae5376f9..c998214b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,6 +1,7 @@
 module L = Logging
 module T = Types
 module A = CfimAst
+module M = Modules
 open Utils
 open InterpreterUtils
 open InterpreterExpressions
@@ -25,12 +26,16 @@ open InterpreterStatements
 let log = L.interpreter_log
 
 module Test = struct
-  let initialize_context (type_context : C.type_context)
-      (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx =
+  let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) :
+      C.eval_ctx =
+    let type_defs_groups, _funs_defs_groups =
+      M.split_declarations_to_group_maps m.declarations
+    in
+    let type_context = { C.type_defs_groups; type_defs = m.types } in
     C.reset_global_counters ();
     {
       C.type_context;
-      C.fun_context = fun_defs;
+      C.fun_context = m.functions;
       C.type_vars;
       C.env = [];
       C.ended_regions = T.RegionId.Set.empty;
@@ -44,8 +49,8 @@ module Test = struct
       "Dummy" abstractions are introduced for the regions present in the
       function signature.
    *)
-  let initialize_symbolic_context_for_fun (type_context : C.type_context)
-      (fun_defs : A.fun_def list) (fdef : A.fun_def) : C.eval_ctx =
+  let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def)
+      : C.eval_ctx =
     (* The abstractions are not initialized the same way as for function
      * calls: they contain *loan* projectors, because they "provide" us
      * with the input values (which behave as if they had been returned
@@ -59,7 +64,7 @@ module Test = struct
      * *)
     let sg = fdef.signature in
     (* Create the context *)
-    let ctx = initialize_context type_context fun_defs sg.type_params in
+    let ctx = initialize_context m sg.type_params in
     (* Instantiate the signature *)
     let type_params =
       List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params
@@ -108,14 +113,14 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (type_context : C.type_context)
-      (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result =
+  let test_unit_function (config : C.partial_config) (m : M.cfim_module)
+      (fid : A.FunDefId.id) : unit eval_result =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDefId.nth fun_defs fid in
+    let fdef = A.FunDefId.nth m.functions fid in
 
     (* Debug *)
     log#ldebug
-      (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name));
+      (lazy ("test_unit_function: " ^ Print.name_to_string fdef.A.name));
 
     (* Sanity check - *)
     assert (List.length fdef.A.signature.region_params = 0);
@@ -123,13 +128,13 @@ module Test = struct
     assert (fdef.A.arg_count = 0);
 
     (* Create the evaluation context *)
-    let ctx = initialize_context type_context fun_defs [] in
+    let ctx = initialize_context m [] in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
 
     (* Evaluate the function *)
-    let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in
+    let config = C.config_of_partial C.ConcreteMode config in
     match eval_function_body config ctx fdef.A.body with
     | [ Ok _ ] -> Ok ()
     | [ Error err ] -> Error err
@@ -146,34 +151,31 @@ module Test = struct
     && List.length def.A.signature.inputs = 0
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (type_defs : T.type_def list)
-      (fun_defs : A.fun_def list) : unit =
-    let unit_funs = List.filter fun_def_is_unit fun_defs in
+  let test_unit_functions (config : C.partial_config) (m : M.cfim_module) : unit
+      =
+    let unit_funs = List.filter fun_def_is_unit m.functions in
     let test_unit_fun (def : A.fun_def) : unit =
-      let type_ctx = { C.type_defs } in
-      match test_unit_function type_ctx fun_defs def.A.def_id with
+      match test_unit_function config m def.A.def_id with
       | Error _ -> failwith "Unit test failed (concrete execution)"
       | Ok _ -> ()
     in
     List.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
-  let test_function_symbolic (type_context : C.type_context)
-      (fun_defs : A.fun_def list) (fid : A.FunDefId.id) :
-      C.eval_ctx eval_result list =
+  let test_function_symbolic (config : C.partial_config) (m : M.cfim_module)
+      (fid : A.FunDefId.id) : C.eval_ctx eval_result list =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDefId.nth fun_defs fid in
+    let fdef = A.FunDefId.nth m.functions fid in
 
     (* Debug *)
     log#ldebug
-      (lazy
-        ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name));
+      (lazy ("test_function_symbolic: " ^ Print.name_to_string fdef.A.name));
 
     (* Create the evaluation context *)
-    let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in
+    let ctx = initialize_symbolic_context_for_fun m fdef in
 
     (* Evaluate the function *)
-    let config = { C.mode = C.SymbolicMode; C.check_invariants = true } in
+    let config = C.config_of_partial C.SymbolicMode config in
     eval_function_body config ctx fdef.A.body
 
   (** Execute the symbolic interpreter on a list of functions.
@@ -181,17 +183,16 @@ module Test = struct
       TODO: for now we ignore the functions which contain loops, because
       they are not supported by the symbolic interpreter.
    *)
-  let test_functions_symbolic (type_defs : T.type_def list)
-      (fun_defs : A.fun_def list) : unit =
+  let test_functions_symbolic (config : C.partial_config) (m : M.cfim_module) :
+      unit =
     let no_loop_funs =
-      List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) fun_defs
+      List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions
     in
     let test_fun (def : A.fun_def) : unit =
-      let type_ctx = { C.type_defs } in
       (* Execute the function - note that as the symbolic interpreter explores
        * all the path, some executions are expected to "panic": we thus don't
        * check the return value *)
-      let _ = test_function_symbolic type_ctx fun_defs def.A.def_id in
+      let _ = test_function_symbolic config m def.A.def_id in
       ()
     in
     List.iter test_fun no_loop_funs
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 3903ca14..4f0ac11c 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -406,12 +406,9 @@ let expand_symbolic_value_borrow (config : C.config)
 
 (** Expand a symbolic value which is not an enumeration with several variants
     (i.e., in a situation where it doesn't lead to branching).
-
-    This function is used when exploring paths.
  *)
 let expand_symbolic_value_no_branching (config : C.config)
-    (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
-    C.eval_ctx =
+    (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Remember the initial context for printing purposes *)
   let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
@@ -419,11 +416,9 @@ let expand_symbolic_value_no_branching (config : C.config)
   let original_sv = sp in
   let rty = original_sv.V.sv_ty in
   let ctx =
-    match (pe, rty) with
+    match rty with
     (* "Regular" ADTs *)
-    | ( Field (ProjAdt (def_id, _opt_variant_id), _),
-        T.Adt (T.AdtId def_id', regions, types) ) -> (
-        assert (def_id = def_id');
+    | T.Adt (T.AdtId def_id, regions, types) -> (
         (* Compute the expanded value - there should be exactly one because we
          * don't allow to expand enumerations with strictly more than one variant *)
         let expand_enumerations = false in
@@ -440,10 +435,12 @@ let expand_symbolic_value_no_branching (config : C.config)
             S.synthesize_symbolic_expansion_no_branching original_sv see;
             (* Return *)
             ctx
-        | _ -> failwith "Unexpected")
+        | _ ->
+            failwith
+              "expand_symbolic_value_no_branching: the expansion lead to \
+               branching")
     (* Tuples *)
-    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
-        assert (arity = List.length tys);
+    | T.Adt (T.Tuple, [], tys) ->
         (* Generate the field values *)
         let see = compute_expanded_symbolic_tuple_value tys in
         (* Apply in the context *)
@@ -455,7 +452,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         (* Return *)
         ctx
     (* Boxes *)
-    | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
+    | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
         let see = compute_expanded_symbolic_box_value boxed_ty in
         (* Apply in the context *)
         let ctx =
@@ -466,11 +463,11 @@ let expand_symbolic_value_no_branching (config : C.config)
         (* Return *)
         ctx
     (* Borrows *)
-    | Deref, T.Ref (region, ref_ty, rkind) ->
+    | T.Ref (region, ref_ty, rkind) ->
         expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx
     | _ ->
         failwith
-          ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
+          ("expand_symbolic_value_no_branching: unreachable: " ^ T.show_rty rty)
   in
   (* Debugging *)
   (* Debug *)
@@ -485,6 +482,36 @@ let expand_symbolic_value_no_branching (config : C.config)
   (* Return *)
   ctx
 
+(** Expand a symbolic value which is not an enumeration with several variants
+    (i.e., in a situation where it doesn't lead to branching).
+
+    This function is used when exploring paths. It simply performs a few
+    sanity checks before calling [expand_symbolic_value_no_branching].
+ *)
+let expand_symbolic_value_no_branching_from_projection_elem (config : C.config)
+    (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* Sanity checks *)
+  let rty = sp.V.sv_ty in
+  let _ =
+    match (pe, rty) with
+    (* "Regular" ADTs *)
+    | Field (ProjAdt (def_id, _), _), T.Adt (T.AdtId def_id', _, _) ->
+        assert (def_id = def_id')
+    (* Tuples *)
+    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
+        assert (arity = List.length tys)
+    (* Boxes *)
+    | DerefBox, T.Adt (T.Assumed T.Box, [], [ _ ]) -> ()
+    (* Borrows *)
+    | Deref, T.Ref (_, _, _) -> ()
+    | _ ->
+        failwith
+          ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
+  in
+  (* Perform the expansion *)
+  expand_symbolic_value_no_branching config sp ctx
+
 (** Expand a symbolic enumeration value.
 
     This might lead to branching.
@@ -519,3 +546,80 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
       in
       List.map apply seel
   | _ -> failwith "Unexpected"
+
+(** Expand all the symbolic values which contain borrows.
+    Allows us to restrict ourselves to a simpler model for the projectors over
+    symbolic values.
+    
+    Fails if doing this requires to do a branching (because we need to expand
+    an enumeration with strictly more than one variant, a slice, etc.) or if
+    we need to expand a recursive type (because this leads to looping).
+ *)
+let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
+    : C.eval_ctx =
+  (* The visitor object, to look for symbolic values in the concrete environment *)
+  let obj =
+    object
+      inherit [_] C.iter_eval_ctx
+
+      method! visit_Symbolic _ sv =
+        if ty_has_regions (Subst.erase_regions sv.V.sv_ty) then
+          raise (FoundSymbolicValue sv)
+        else ()
+
+      method! visit_abs _ _ = ()
+      (** Don't enter abstractions *)
+    end
+  in
+
+  let rec expand (ctx : C.eval_ctx) : C.eval_ctx =
+    try
+      obj#visit_eval_ctx () ctx;
+      ctx
+    with FoundSymbolicValue sv ->
+      (* Expand and recheck the environment *)
+      let ctx =
+        match sv.V.sv_ty with
+        | T.Adt (AdtId def_id, _, _) ->
+            (* [expand_symbolic_value_no_branching] checks if there are branchings,
+             * but we prefer to also check it here - this leads to cleaner messages
+             * and debugging *)
+            let def = C.ctx_lookup_type_def ctx def_id in
+            (match def.kind with
+            | T.Struct _ | T.Enum ([] | [ _ ]) -> ()
+            | T.Enum (_ :: _) ->
+                failwith
+                  ("Attempted to greedily expand a symbolic enumeration with > \
+                    1 variants (option [greedy_expand_symbolics_with_borrows] \
+                    of [config]): "
+                  ^ Print.name_to_string def.name));
+            (* Also, we need to check if the definition is recursive *)
+            if C.ctx_type_def_is_rec ctx def_id then
+              failwith
+                ("Attempted to greedily expand a recursive definition (option \
+                  [greedy_expand_symbolics_with_borrows] of [config]): "
+                ^ Print.name_to_string def.name)
+            else expand_symbolic_value_no_branching config sv ctx
+        | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) ->
+            (* Ok *)
+            expand_symbolic_value_no_branching config sv ctx
+        | T.Array _ -> raise Errors.Unimplemented
+        | T.Slice _ -> failwith "Can't expand symbolic slices"
+        | T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
+            failwith "Unreachable"
+      in
+      expand ctx
+  in
+  expand ctx
+
+(** If this mode is activated through the [config], greedily expand the symbolic
+    values which need to be expanded. See [config] for more information.
+ *)
+let greedy_expand_symbolic_values (config : C.config) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  let ctx =
+    if config.greedy_expand_symbolics_with_borrows then
+      greedy_expand_symbolics_with_borrows config ctx
+    else ctx
+  in
+  ctx
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f3b07cc2..93ec8640 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -114,6 +114,8 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
     | Expressions.Copy p ->
         (* Access the value *)
         let access = Read in
+        (* TODO: expand the value if it is a symbolic value *)
+        raise Unimplemented;
         prepare_rplace config access p ctx
     | Expressions.Move p ->
         (* Access the value *)
@@ -139,6 +141,8 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
+      (* TODO: expand the value if it is a symbolic value *)
+      raise Unimplemented;
       let ctx, v = prepare_rplace config access p ctx in
       (* Copy the value *)
       assert (not (bottom_in_value ctx.ended_regions v));
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index e1c80d89..6bc22af4 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -469,7 +469,8 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
             activate_inactivated_mut_borrow config bid ctx
         | FailSymbolic (pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config pe sp ctx
+            expand_symbolic_value_no_branching_from_projection_elem config pe sp
+              ctx
         | FailBottom (_, _, _) ->
             (* We can't expand [Bottom] values while reading them *)
             failwith "Found [Bottom] while reading a place"
@@ -496,7 +497,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
             activate_inactivated_mut_borrow config bid ctx
         | FailSymbolic (pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config pe sp ctx
+            expand_symbolic_value_no_branching_from_projection_elem config pe sp
+              ctx
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the [Bottom] value *)
             expand_bottom_value_from_projection config access p remaining_pes pe
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index d13dc515..e6fadbdd 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -598,6 +598,9 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
       ("\n**About to evaluate statement**: [\n"
       ^ statement_to_string_with_tab ctx st
       ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
+  (* Expand the symbolic values if necessary - we need to do that before
+   * checking the invariants *)
+  let ctx = greedy_expand_symbolic_values config ctx in
   (* Sanity check *)
   if config.C.check_invariants then Inv.check_invariants ctx;
   (* Evaluate *)
@@ -888,6 +891,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   in
   (* Evaluate the input operands *)
   let ctx, args = eval_operands config ctx args in
+  (* TODO: expand the primitively copyable symbolic values *)
+  raise Errors.Unimplemented;
   let args_with_rtypes = List.combine args inst_sg.A.inputs in
   (* Check the type of the input arguments *)
   assert (
@@ -1021,6 +1026,9 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx)
     match res with
     | Error err -> Error err
     | Ok (ctx, res) -> (
+        (* Expand the symbolic values if necessary - we need to do that before
+         * checking the invariants *)
+        let ctx = greedy_expand_symbolic_values config ctx in
         (* Sanity check *)
         if config.C.check_invariants then Inv.check_invariants ctx;
         match res with
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 7664f70e..5009410e 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -621,7 +621,16 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
   in
   visitor#visit_eval_ctx (None : V.abs option) ctx
 
+(** TODO:
+    
+    - a symbolic value can't be both in proj_borrows and in the concrete env
+      (this is why we preemptively expand copyable symbolic values)
+
+ *)
+let check_symbolic_values (ctx : C.eval_ctx) : unit = raise Errors.Unimplemented
+
 let check_invariants (ctx : C.eval_ctx) : unit =
   check_loans_borrows_relation_invariant ctx;
   check_borrowed_values_invariant ctx;
-  check_typing_invariant ctx
+  check_typing_invariant ctx;
+  check_symbolic_values ctx
diff --git a/src/Modules.ml b/src/Modules.ml
index bf5e9835..e4cb06c1 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -14,3 +14,47 @@ type cfim_module = {
   functions : fun_def list;
 }
 (** CFIM module *)
+
+type 'id decl_group = NonRec of 'id | Rec of 'id list [@@deriving show]
+
+type types_decl_group = TypeDefId.id decl_group [@@deriving show]
+
+type funs_decl_group = FunDefId.id decl_group [@@deriving show]
+
+(** Split a module's declarations between types and functions *)
+let split_declarations (decls : declaration list) :
+    types_decl_group list * funs_decl_group list =
+  let rec split decls =
+    match decls with
+    | [] -> ([], [])
+    | d :: decls' -> (
+        let types, funs = split decls' in
+        match d with
+        | Type id -> (NonRec id :: types, funs)
+        | Fun id -> (types, NonRec id :: funs)
+        | RecTypes ids -> (Rec ids :: types, funs)
+        | RecFuns ids -> (types, Rec ids :: funs))
+  in
+  split decls
+
+(** Split a module's declarations into two maps from type/fun ids to
+    declaration groups.
+ *)
+let split_declarations_to_group_maps (decls : declaration list) :
+    types_decl_group TypeDefId.Map.t * funs_decl_group FunDefId.Map.t =
+  let module G (M : Map.S) = struct
+    let add_group (map : M.key decl_group M.t) (group : M.key decl_group) :
+        M.key decl_group M.t =
+      match group with
+      | NonRec id -> M.add id group map
+      | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
+
+    let create_map (groups : M.key decl_group list) : M.key decl_group M.t =
+      List.fold_left add_group M.empty groups
+  end in
+  let types, funs = split_declarations decls in
+  let module TG = G (TypeDefId.Map) in
+  let types = TG.create_map types in
+  let module FG = G (FunDefId.Map) in
+  let funs = FG.create_map funs in
+  (types, funs)
diff --git a/src/Print.ml b/src/Print.ml
index d4f051f9..1eab6714 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -10,6 +10,8 @@ module M = Modules
 let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
   match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
 
+let name_to_string (name : name) : string = String.concat "::" name
+
 (** Pretty-printing for types *)
 module Types = struct
   let type_var_to_string (tv : T.type_var) : string = tv.name
@@ -115,8 +117,6 @@ module Types = struct
     ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
     ^ ")"
 
-  let name_to_string (name : name) : string = String.concat "::" name
-
   let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string)
       (def : T.type_def) : string =
     let regions = def.region_params in
@@ -492,7 +492,7 @@ module Contexts = struct
     | Struct _ -> failwith "Unreachable"
     | Enum variants ->
         let variant = T.VariantId.nth variants variant_id in
-        PT.name_to_string def.name ^ "::" ^ variant.variant_name
+        name_to_string def.name ^ "::" ^ variant.variant_name
 
   let type_ctx_to_adt_field_names_fun (ctx : T.type_def list) :
       T.TypeDefId.id -> T.VariantId.id option -> string list option =
@@ -514,7 +514,7 @@ module Contexts = struct
     in
     let type_def_id_to_string def_id =
       let def = T.TypeDefId.nth ctx.type_context.type_defs def_id in
-      PT.name_to_string def.name
+      name_to_string def.name
     in
     let adt_variant_to_string =
       type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs
@@ -633,7 +633,7 @@ module CfimAst = struct
     in
     let fun_def_id_to_string def_id =
       let def = A.FunDefId.nth ctx.fun_context def_id in
-      PT.name_to_string def.name
+      name_to_string def.name
     in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
@@ -851,7 +851,7 @@ module CfimAst = struct
     let sg = def.signature in
 
     (* Function name *)
-    let name = PT.name_to_string def.A.name in
+    let name = name_to_string def.A.name in
 
     (* Region/type parameters *)
     let regions = sg.region_params in
@@ -911,7 +911,7 @@ module Module = struct
       string =
     let type_def_id_to_string (id : T.TypeDefId.id) : string =
       let def = T.TypeDefId.nth type_context id in
-      PT.name_to_string def.name
+      name_to_string def.name
     in
     PT.type_def_to_string type_def_id_to_string def
 
@@ -933,11 +933,11 @@ module Module = struct
     in
     let type_def_id_to_string def_id =
       let def = T.TypeDefId.nth type_context def_id in
-      PT.name_to_string def.name
+      name_to_string def.name
     in
     let fun_def_id_to_string def_id =
       let def = A.FunDefId.nth fun_context def_id in
-      PT.name_to_string def.name
+      name_to_string def.name
     in
     let var_id_to_string vid =
       let var = V.VarId.nth def.locals vid in
diff --git a/src/main.ml b/src/main.ml
index c6545fcb..e8f46b99 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -59,8 +59,16 @@ let () =
       (* Print the module *)
       main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
+      (* Some options for the execution *)
+      let config =
+        {
+          C.check_invariants = true;
+          greedy_expand_symbolics_with_borrows = false;
+        }
+      in
+
       (* Test the unit functions with the concrete interpreter *)
-      I.Test.test_unit_functions m.types m.functions;
+      I.Test.test_unit_functions config m;
 
       (* Evaluate the symbolic interpreter on the functions *)
-      I.Test.test_functions_symbolic m.types m.functions
+      I.Test.test_functions_symbolic config m