Start working on the generation of the symbolic AST

10 files changed, 240 insertions, 52 deletions

diff --git a/src/Collections.ml b/src/Collections.ml
index b73bc3b6..54d0acac 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -9,6 +9,8 @@ module List = struct
   
       `split_at ls i` splits `ls` into two lists where the first list has
       length `i`.
+      
+      Raise `Failure` if the list is too short.
   *)
   let rec split_at (ls : 'a list) (i : int) =
     if i < 0 then raise (Invalid_argument "split_at take positive integers")
@@ -21,6 +23,18 @@ module List = struct
       | x :: ls' ->
           let ls1, ls2 = split_at ls' (i - 1) in
           (x :: ls1, ls2)
+
+  (** Pop the last element of a list
+     
+      Raise `Failure` if the list is empty.
+   *)
+  let rec pop_last (ls : 'a list) : 'a list * 'a =
+    match ls with
+    | [] -> raise (Failure "The list is empty")
+    | [ x ] -> ([], x)
+    | x :: ls ->
+        let ls, last = pop_last ls in
+        (x :: ls, last)
 end
 
 module type OrderedType = sig
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 39c6ab91..6f0c02c4 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -68,6 +68,9 @@ let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
 let abstraction_id_counter, fresh_abstraction_id =
   AbstractionId.fresh_stateful_generator ()
 
+let fun_call_id_counter, fresh_fun_call_id =
+  FunCallId.fresh_stateful_generator ()
+
 (** We shouldn't need to reset the global counters, but it might be good to
     do it from time to time, for instance every time we start evaluating/
     synthesizing a function.
@@ -83,7 +86,8 @@ let reset_global_counters () =
   symbolic_value_id_counter := SymbolicValueId.generator_zero;
   borrow_id_counter := BorrowId.generator_zero;
   region_id_counter := RegionId.generator_zero;
-  abstraction_id_counter := AbstractionId.generator_zero
+  abstraction_id_counter := AbstractionId.generator_zero;
+  fun_call_id_counter := FunCallId.generator_zero
 
 type binder = {
   index : VarId.id;  (** Unique variable identifier *)
diff --git a/src/Cps.ml b/src/Cps.ml
index 2c515ed0..d7c50f26 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -4,6 +4,7 @@
 module T = Types
 module V = Values
 module C = Contexts
+module SA = SymbolicAst
 
 (** TODO: change the name *)
 type eval_error = EPanic
@@ -19,7 +20,7 @@ type statement_eval_res =
 (** Synthesized expresssion - dummy for now *)
 type sexpr = SOne | SList of sexpr list
 
-type eval_result = sexpr option
+type eval_result = SA.expression option
 
 type m_fun = C.eval_ctx -> eval_result
 (** Continuation function *)
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index b2d952b1..69e12545 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -11,7 +11,7 @@ module Subst = Substitute
 module L = Logging
 open TypesUtils
 module Inv = Invariants
-module S = Synthesis
+module S = SynthesizeSymbolic
 open Cps
 open ValuesUtils
 open InterpreterUtils
@@ -52,7 +52,7 @@ type proj_kind = LoanProj | BorrowProj
 *)
 let apply_symbolic_expansion_to_target_avalues (config : C.config)
     (allow_reborrows : bool) (proj_kind : proj_kind)
-    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+    (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Symbolic values contained in the expansion might contain already ended regions *)
   let check_symbolic_no_ended = false in
@@ -150,7 +150,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
 *)
 let apply_symbolic_expansion_to_avalues (config : C.config)
     (allow_reborrows : bool) (original_sv : V.symbolic_value)
-    (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
+    (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
   let apply_expansion proj_kind ctx =
     apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
       original_sv expansion ctx
@@ -199,7 +199,7 @@ let replace_symbolic_values (at_most_once : bool)
     This function does update the synthesis.
 *)
 let apply_symbolic_expansion_non_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+    (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
@@ -221,7 +221,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
     (kind : V.sv_kind) (def_id : T.TypeDefId.id)
     (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (ctx : C.eval_ctx) : symbolic_expansion list =
+    (ctx : C.eval_ctx) : V.symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = C.ctx_lookup_type_def ctx def_id in
@@ -236,31 +236,31 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   (* Initialize the expanded value for a given variant *)
   let initialize
       ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
-      symbolic_expansion =
+      V.symbolic_expansion =
     let field_values =
       List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types
     in
-    let see = SeAdt (variant_id, field_values) in
+    let see = V.SeAdt (variant_id, field_values) in
     see
   in
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
 let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
-    (field_types : T.rty list) : symbolic_expansion =
+    (field_types : T.rty list) : V.symbolic_expansion =
   (* Generate the field values *)
   let field_values =
     List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
   in
   let variant_id = None in
-  let see = SeAdt (variant_id, field_values) in
+  let see = V.SeAdt (variant_id, field_values) in
   see
 
 let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
-    symbolic_expansion =
+    V.symbolic_expansion =
   (* Introduce a fresh symbolic value *)
   let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
-  let see = SeAdt (None, [ boxed_value ]) in
+  let see = V.SeAdt (None, [ boxed_value ]) in
   see
 
 let expand_symbolic_value_shared_borrow (config : C.config)
@@ -363,16 +363,16 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   let bids = !borrows in
   assert (not (V.BorrowId.Set.is_empty bids));
   let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
-  let see = SeSharedRef (bids, shared_sv) in
+  let see = V.SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
     apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
       ctx
   in
+  (* Call the continuation *)
+  let expr = cf ctx in
   (* Update the synthesized program *)
-  S.synthesize_symbolic_expansion_no_branching original_sv see;
-  (* Continue *)
-  cf ctx
+  S.synthesize_symbolic_expansion_no_branching original_sv see expr
 
 (** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : C.config)
@@ -388,7 +388,7 @@ let expand_symbolic_value_borrow (config : C.config)
        * borrow id *)
       let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
       let bid = C.fresh_borrow_id () in
-      let see = SeMutRef (bid, sv) in
+      let see = V.SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
        * check that we perform exactly one substitution) *)
       let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
@@ -402,10 +402,10 @@ let expand_symbolic_value_borrow (config : C.config)
         apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
           see ctx
       in
+      (* Apply the continuation *)
+      let expr = cf ctx in
       (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_no_branching original_sv see;
-      (* Continue *)
-      cf ctx
+      S.synthesize_symbolic_expansion_no_branching original_sv see expr
   | T.Shared ->
       expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx
 
@@ -419,7 +419,7 @@ let expand_symbolic_value_borrow (config : C.config)
 *)
 let apply_branching_symbolic_expansions_non_borrow (config : C.config)
     (sv : V.symbolic_value)
-    (see_cf_l : (symbolic_expansion option * m_fun) list) : m_fun =
+    (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun =
  fun ctx ->
   assert (see_cf_l <> []);
   (* Apply the symbolic expansion in in the context and call the continuation *)
@@ -447,7 +447,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
     | _ -> failwith "Unreachable"
   in
   (* Synthesize and return *)
-  S.synthesize_symbolic_expansion sv subterms
+  let seel = List.map fst see_cf_l in
+  S.synthesize_symbolic_expansion sv seel subterms
 
 (** Expand a symbolic value which is not an enumeration with several variants
     (i.e., in a situation where it doesn't lead to branching).
@@ -492,10 +493,10 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
         in
+        (* Call the continuation *)
+        let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv see;
-        (* Continue *)
-        cf ctx
+        S.synthesize_symbolic_expansion_no_branching original_sv see expr
     (* Boxes *)
     | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
         let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
@@ -503,10 +504,10 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
         in
+        (* Call the continuation *)
+        let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv see;
-        (* Continue *)
-        cf ctx
+        S.synthesize_symbolic_expansion_no_branching original_sv see expr
     (* Borrows *)
     | T.Ref (region, ref_ty, rkind) ->
         expand_symbolic_value_borrow config original_sv region ref_ty rkind cf
@@ -514,13 +515,12 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     (* Booleans *)
     | T.Bool ->
         assert allow_branching;
-        (* Synthesis *)
-        S.synthesize_symbolic_expansion_if_branching original_sv;
         (* Expand the symbolic value to true or false and continue execution *)
-        let see_true = SeConcrete (V.Bool true) in
-        let see_false = SeConcrete (V.Bool false) in
+        let see_true = V.SeConcrete (V.Bool true) in
+        let see_false = V.SeConcrete (V.Bool false) in
         let seel = [ see_true; see_false ] in
         let seel = List.map (fun see -> (Some see, cf)) seel in
+        (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
         apply_branching_symbolic_expansions_non_borrow config original_sv seel
           ctx
     | _ -> failwith ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)
@@ -569,8 +569,6 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
 let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
     (int_type : T.integer_type) (tgts : (V.scalar_value * m_fun) list)
     (otherwise : m_fun) : m_fun =
-  (* Synthesis *)
-  S.synthesize_symbolic_expansion_switch_int_branching sv;
   (* Sanity check *)
   assert (sv.V.sv_ty = T.Integer int_type);
   (* For all the branches of the switch, we expand the symbolic value
@@ -583,10 +581,10 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
    * (optional expansion, statement to execute)
    *)
   let tgts =
-    List.map (fun (v, cf) -> (Some (SeConcrete (V.Scalar v)), cf)) tgts
+    List.map (fun (v, cf) -> (Some (V.SeConcrete (V.Scalar v)), cf)) tgts
   in
   let tgts = List.append tgts [ (None, otherwise) ] in
-  (* Then expand and evaluate *)
+  (* Then expand and evaluate - this generates the proper symbolic AST *)
   apply_branching_symbolic_expansions_non_borrow config sv tgts
 
 (** See [expand_symbolic_value] *)
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 982d9460..946bacea 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -8,13 +8,6 @@ open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
-(** A symbolic expansion *)
-type symbolic_expansion =
-  | SeConcrete of V.constant_value
-  | SeAdt of (T.VariantId.id option * V.symbolic_value list)
-  | SeMutRef of V.BorrowId.id * V.symbolic_value
-  | SeSharedRef of V.BorrowId.Set.t * V.symbolic_value
-
 (** Auxiliary function.
 
     Apply a proj_borrows on a shared borrow.
@@ -255,7 +248,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
 
 (** Convert a symbolic expansion *which is not a borrow* to a value *)
 let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
-    (see : symbolic_expansion) : V.typed_value =
+    (see : V.symbolic_expansion) : V.typed_value =
   let ty = Subst.erase_regions sv.V.sv_ty in
   let value =
     match see with
@@ -277,7 +270,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
     during a symbolic expansion.
   *)
 let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
-    (see : symbolic_expansion) : V.typed_value =
+    (see : V.symbolic_expansion) : V.typed_value =
   match see with
   | SeMutRef (bid, bv) ->
       let ty = Subst.erase_regions sv.V.sv_ty in
@@ -293,7 +286,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
     TODO: detailed comments. See [apply_proj_borrows]
 *)
 let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
-    (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
+    (see : V.symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
   assert (ty_has_regions_in_set regions original_sv_ty);
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index d76def43..17fe700f 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -668,9 +668,14 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind)
   let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref =
     ref V.AbstractionId.Map.empty
   in
+  (* We generate *one* fresh call identifier for all the introduced abstractions
+   * (it links them together) *)
+  let call_id = C.fresh_fun_call_id () in
   (* Auxiliary function to create one abstraction *)
-  let create_abs (rg : A.abs_region_group) : V.abs =
+  let create_abs (back_id : V.BackwardFunctionId.id) (rg : A.abs_region_group) :
+      V.abs =
     let abs_id = rg.T.id in
+    let back_id = Some back_id in
     let parents =
       List.fold_left
         (fun s pid -> V.AbstractionId.Set.add pid s)
@@ -695,10 +700,19 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind)
       V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
         !abs_to_ancestors_regions;
     (* Create the abstraction *)
-    { V.abs_id; kind; parents; regions; ancestors_regions; avalues = [] }
+    {
+      V.abs_id;
+      call_id;
+      back_id;
+      kind;
+      parents;
+      regions;
+      ancestors_regions;
+      avalues = [];
+    }
   in
   (* Apply *)
-  List.map create_abs rgl
+  V.BackwardFunctionId.mapi create_abs rgl
 
 (** Evaluate a statement *)
 let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
new file mode 100644
index 00000000..6b66ada7
--- /dev/null
+++ b/src/SymbolicAst.ml
@@ -0,0 +1,47 @@
+(** The "symbolic" AST is the AST directly generated by the symbolic execution.
+    It is very rough and meant to be extremely straightforward to build during
+    the symbolic execution: we later apply transformations to generate the
+    pure AST that we export. *)
+
+open Identifiers
+module T = Types
+module V = Values
+module E = Expressions
+module A = CfimAst
+
+type fun_id =
+  | Fun of A.fun_id
+      (** A "regular" function (i.e., a function which is not a primitive operation) *)
+  | Unop of E.unop
+  | Binop of E.binop
+
+type call = {
+  call_id : V.FunCallId.id;
+  func : A.fun_id;
+  type_params : T.ety list;
+  args : V.typed_value list;
+  dest : V.symbolic_value;
+}
+
+type expression =
+  | Return
+  | Panic
+  | FunCall of call * expression
+  | EndAbstraction of V.abs * expression
+  | Expansion of V.symbolic_value * expansion
+
+and expansion =
+  | ExpandNoBranch of V.symbolic_expansion * expression
+      (** A symbolic expansion which doesn't generate a branching.
+          Includes: expansion of borrows, structures, enumerations with one
+          variants... *)
+  | ExpandEnum of
+      (T.VariantId.id option * V.symbolic_value list * expression) list
+      (** A symbolic expansion of an ADT value which leads to branching (i.e.,
+          a match over an enumeration with strictly more than one variant *)
+  | ExpandBool of expression * expression
+      (** A boolean expansion (i.e, an `if ... then ... else ...`) *)
+  | ExpandInt of
+      T.integer_type * (V.scalar_value * expression) list * expression
+      (** An integer expansion (i.e, a switch over an integer). The last
+          expression is for the "otherwise" branch. *)
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 8a0dce93..acecd517 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -42,13 +42,13 @@ let synthesize_symbolic_expansion (_sv : V.symbolic_value)
     (i.e., applied on a value which is not an enumeration with several variants).
  *)
 let synthesize_symbolic_expansion_no_branching (_sv : V.symbolic_value)
-    (_see : symbolic_expansion) : unit =
+    (_see : V.symbolic_expansion) : unit =
   ()
 
 (** Synthesize code for a symbolic enum expansion (which leads to branching)
  *)
 let synthesize_symbolic_expansion_enum_branching (_sv : V.symbolic_value)
-    (_seel : symbolic_expansion list) : unit =
+    (_seel : V.symbolic_expansion list) : unit =
   ()
 
 let synthesize_symbolic_expansion_if_branching (_sv : V.symbolic_value) : unit =
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
new file mode 100644
index 00000000..b9bad7c9
--- /dev/null
+++ b/src/SynthesizeSymbolic.ml
@@ -0,0 +1,89 @@
+open Errors
+open Identifiers
+module C = Collections
+module T = Types
+module V = Values
+module E = Expressions
+module A = CfimAst
+open SymbolicAst
+
+let synthesize_symbolic_expansion (sv : V.symbolic_value)
+    (seel : V.symbolic_expansion option list) (exprl : expression list option) :
+    expression option =
+  match exprl with
+  | None -> None
+  | Some exprl ->
+      let ls = List.combine seel exprl in
+      (* Match on the symbolic value type to know which can of expansion happened *)
+      let expansion =
+        match sv.V.sv_ty with
+        | T.Bool -> (
+            (* Boolean expansion: there should be two branches *)
+            match ls with
+            | [
+             (Some (V.SeConcrete (V.Bool true)), true_exp);
+             (Some (V.SeConcrete (V.Bool false)), false_exp);
+            ] ->
+                ExpandBool (true_exp, false_exp)
+            | _ -> failwith "Ill-formed boolean expansion")
+        | T.Integer int_ty ->
+            (* Switch over an integer: split between the "regular" branches
+               and the "otherwise" branch (which should be the last branch) *)
+            let branches, otherwise = C.List.pop_last ls in
+            (* For all the regular branches, the symbolic value should have
+             * been expanded to a constant *)
+            let get_scalar (see : V.symbolic_expansion option) : V.scalar_value
+                =
+              match see with
+              | Some (V.SeConcrete (V.Scalar cv)) ->
+                  assert (cv.V.int_ty = int_ty);
+                  cv
+              | _ -> failwith "Unreachable"
+            in
+            let branches =
+              List.map (fun (see, exp) -> (get_scalar see, exp)) branches
+            in
+            (* For the otherwise branch, the symbolic value should have been left
+             * unchanged *)
+            let otherwise_see, otherwise = otherwise in
+            assert (otherwise_see = None);
+            (* Return *)
+            ExpandInt (int_ty, branches, otherwise)
+        | T.Adt (adt_id, regions, types) -> (
+            (* An ADT expansion can lead to branching: check if this is the case *)
+            match ls with
+            | [] -> failwith "Ill-formed ADT expansion"
+            | [ (see, exp) ] ->
+                (* No branching *)
+                ExpandNoBranch (Option.get see, exp)
+            | ls ->
+                (* Branching: it is necessarily an enumeration expansion *)
+                let get_variant (see : V.symbolic_expansion option) :
+                    T.VariantId.id option * V.symbolic_value list =
+                  match see with
+                  | Some (V.SeAdt (vid, fields)) -> (vid, fields)
+                  | _ -> failwith "Ill-formed branching ADT expansion"
+                in
+                let exp =
+                  List.map
+                    (fun (see, exp) ->
+                      let vid, fields = get_variant see in
+                      (vid, fields, exp))
+                    ls
+                in
+                ExpandEnum exp)
+        | T.Ref (r, ty, rkind) -> (
+            (* Reference expansion: there should be one branch *)
+            match ls with
+            | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
+            | _ -> failwith "Ill-formed borrow expansion")
+        | T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
+            failwith "Ill-formed symbolic expansion"
+      in
+      Some (Expansion (sv, expansion))
+
+let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
+    (see : V.symbolic_expansion) (expr : expression option) : expression option
+    =
+  let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
+  synthesize_symbolic_expansion sv [ Some see ] exprl
diff --git a/src/Values.ml b/src/Values.ml
index 4946b811..1812cd18 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -13,6 +13,10 @@ module SymbolicValueId = IdGen ()
 
 module AbstractionId = IdGen ()
 
+module FunCallId = IdGen ()
+
+module BackwardFunctionId = IdGen ()
+
 (** A variable *)
 
 type big_int = Z.t
@@ -712,6 +716,17 @@ type abs_kind =
 
 type abs = {
   abs_id : (AbstractionId.id[@opaque]);
+  call_id : (FunCallId.id[@opaque]);
+      (** The identifier of the function call which introduced this
+          abstraction. This is not used by the symbolic execution:
+          this is only used for pretty-printing and debugging, in the
+          symbolic AST, generated by the symbolic execution.
+       *)
+  back_id : (BackwardFunctionId.id option[@opaque]);
+      (** The id of the backward function to which this abstraction is linked.
+          This is not used by the symbolic execution: it is a utility for
+          the symbolic AST, generated by the symbolic execution.
+       *)
   kind : (abs_kind[@opaque]);
   parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
   regions : (RegionId.Set.t[@opaque]);  (** Regions owned by this abstraction *)
@@ -744,3 +759,16 @@ type abs = {
     In order to model the relations between the borrows, we use "abstraction values",
     which are a special kind of value.
 *)
+
+(** A symbolic expansion
+    
+    A symbolic expansion doesn't represent a value, but rather an operation
+    that we apply to values.
+    
+    TODO: this should rather be name "expanded_symbolic"
+ *)
+type symbolic_expansion =
+  | SeConcrete of constant_value
+  | SeAdt of (VariantId.id option * symbolic_value list)
+  | SeMutRef of BorrowId.id * symbolic_value
+  | SeSharedRef of BorrowId.Set.t * symbolic_value