From 05db1377f1b987050e58643b9bf001f62a77e303 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 08:43:24 +0100
Subject: Introduce the type_context definition

---
 src/Contexts.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 5e8ae3d0..521ea0ed 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -60,8 +60,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
 type config = { mode : interpreter_mode; check_invariants : bool }
 [@@deriving show]
 
+type type_context = { type_defs : type_def list } [@@deriving show]
+
 type eval_ctx = {
-  type_context : type_def list;
+  type_context : type_context;
   fun_context : fun_def list;
   type_vars : type_var list;
   env : env;
@@ -94,7 +96,7 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   lookup ctx.env
 
 let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def =
-  TypeDefId.nth ctx.type_context tid
+  TypeDefId.nth ctx.type_context.type_defs tid
 
 let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def =
   FunDefId.nth ctx.fun_context fid
-- 
cgit v1.2.3


From f25a5619a3fde75140c20595c5b39282bbbb40e2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 13:24:15 +0100
Subject: Implement the symbolic case of eval_rvalue_discriminant

---
 src/Contexts.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 521ea0ed..4d924a9d 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -68,7 +68,8 @@ type eval_ctx = {
   type_vars : type_var list;
   env : env;
   symbolic_counter : SymbolicValueId.generator;
-  borrow_counter : BorrowId.generator;
+  (* TODO: make this global? *)
+  borrow_counter : BorrowId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
 (** Evaluation context *)
-- 
cgit v1.2.3


From 8904a6daf444082a26172ad3187f9d61420ab8ec Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 16:42:24 +0100
Subject: Prepare the terrain for evaluation of function calls in symbolic mode

---
 src/Contexts.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 4d924a9d..fec1e11b 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -69,7 +69,9 @@ type eval_ctx = {
   env : env;
   symbolic_counter : SymbolicValueId.generator;
   (* TODO: make this global? *)
-  borrow_counter : BorrowId.generator; (* TODO: make this global? *)
+  borrow_counter : BorrowId.generator;
+  (* TODO: make this global? *)
+  abstraction_counter : AbstractionId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
 (** Evaluation context *)
-- 
cgit v1.2.3


From b191de7f680e4ae43178fc42ccabc91808e189f8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 18:13:06 +0100
Subject: Make good progress on eval_local_function_call_symbolic

---
 src/Contexts.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index fec1e11b..89056680 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -71,6 +71,8 @@ type eval_ctx = {
   (* TODO: make this global? *)
   borrow_counter : BorrowId.generator;
   (* TODO: make this global? *)
+  region_counter : RegionId.generator;
+  (* TODO: make this global? *)
   abstraction_counter : AbstractionId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
@@ -84,6 +86,14 @@ let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id =
   let id, counter' = BorrowId.fresh ctx.borrow_counter in
   ({ ctx with borrow_counter = counter' }, id)
 
+let fresh_region_id (ctx : eval_ctx) : eval_ctx * RegionId.id =
+  let id, counter' = RegionId.fresh ctx.region_counter in
+  ({ ctx with region_counter = counter' }, id)
+
+let fresh_abstraction_id (ctx : eval_ctx) : eval_ctx * AbstractionId.id =
+  let id, counter' = AbstractionId.fresh ctx.abstraction_counter in
+  ({ ctx with abstraction_counter = counter' }, id)
+
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
-- 
cgit v1.2.3


From 7137e0733650e0ce37eff4ff805c95543f2c1161 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 17:44:17 +0100
Subject: Remove the symbolic_proj_comp def and make the set of ended regions a
 field in the eval_ctx struct

---
 src/Contexts.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 89056680..5225645c 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -67,6 +67,7 @@ type eval_ctx = {
   fun_context : fun_def list;
   type_vars : type_var list;
   env : env;
+  ended_regions : RegionId.set_t;
   symbolic_counter : SymbolicValueId.generator;
   (* TODO: make this global? *)
   borrow_counter : BorrowId.generator;
-- 
cgit v1.2.3


From f3982cbe9782405b50b04c948ba7cb0bd89ef85f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 18:20:24 +0100
Subject: Make the symbolic, borrow, region and abstration counters global and
 stateful

---
 src/Contexts.ml | 63 ++++++++++++++++++++++++++++++++++++---------------------
 1 file changed, 40 insertions(+), 23 deletions(-)

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 5225645c..f8a7b56b 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -3,6 +3,46 @@ open Values
 open CfimAst
 module V = Values
 
+(** Some global counters.
+ *
+ * Note that those counters were initially stored in [eval_ctx] values,
+ * but it proved better to make them global and stateful:
+ * - when branching (and thus executing on several paths with different
+ *   contexts) it is better to really have unique ids everywhere (and
+ *   not have fresh ids shared by several contexts even though introduced
+ *   after the branching) because at some point we might need to merge the
+ *   different contexts
+ * - also, it is a lot more convenient to not store those counters in contexts
+ *   objects
+ *)
+
+let symbolic_value_id_counter, fresh_symbolic_value_id =
+  SymbolicValueId.fresh_stateful_generator ()
+
+let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
+
+let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
+
+let abstraction_id_counter, fresh_abstraction_id =
+  AbstractionId.fresh_stateful_generator ()
+
+(** We shouldn't need to reset the global counters, but it might be good to
+    to it from time to time, every time we evaluate/synthesize a function for
+    instance.
+    
+    The reasons are manifold:
+    - it might prevent the counters from overflowing (although this seems
+      extremely unlikely - as a side node: we have overflow checks to make
+      sure the synthesis doesn't get impacted by potential overflows)
+    - most importantly, it allows to always manipulate low values, which
+      is always a lot more readable when debugging
+ *)
+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
+
 type binder = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
@@ -68,33 +108,10 @@ type eval_ctx = {
   type_vars : type_var list;
   env : env;
   ended_regions : RegionId.set_t;
-  symbolic_counter : SymbolicValueId.generator;
-  (* TODO: make this global? *)
-  borrow_counter : BorrowId.generator;
-  (* TODO: make this global? *)
-  region_counter : RegionId.generator;
-  (* TODO: make this global? *)
-  abstraction_counter : AbstractionId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
 (** Evaluation context *)
 
-let fresh_symbolic_value_id (ctx : eval_ctx) : eval_ctx * SymbolicValueId.id =
-  let id, counter' = SymbolicValueId.fresh ctx.symbolic_counter in
-  ({ ctx with symbolic_counter = counter' }, id)
-
-let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id =
-  let id, counter' = BorrowId.fresh ctx.borrow_counter in
-  ({ ctx with borrow_counter = counter' }, id)
-
-let fresh_region_id (ctx : eval_ctx) : eval_ctx * RegionId.id =
-  let id, counter' = RegionId.fresh ctx.region_counter in
-  ({ ctx with region_counter = counter' }, id)
-
-let fresh_abstraction_id (ctx : eval_ctx) : eval_ctx * AbstractionId.id =
-  let id, counter' = AbstractionId.fresh ctx.abstraction_counter in
-  ({ ctx with abstraction_counter = counter' }, id)
-
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
-- 
cgit v1.2.3


From 1d0254f555e26968badf05d605cd630c018dcaa8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 18:25:09 +0100
Subject: Cleanup

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

(limited to 'src/Contexts.ml')

diff --git a/src/Contexts.ml b/src/Contexts.ml
index f8a7b56b..0fe3a09a 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -27,8 +27,8 @@ let abstraction_id_counter, fresh_abstraction_id =
   AbstractionId.fresh_stateful_generator ()
 
 (** We shouldn't need to reset the global counters, but it might be good to
-    to it from time to time, every time we evaluate/synthesize a function for
-    instance.
+    do it from time to time, for instance every time we start evaluating/
+    synthesizing a function.
     
     The reasons are manifold:
     - it might prevent the counters from overflowing (although this seems
-- 
cgit v1.2.3