Start working on invariant checking

3 files changed, 40 insertions, 4 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 1c54d9a4..e11adcbf 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -9,6 +9,7 @@ module A = CfimAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
+module Inv = Invariants
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -4247,6 +4248,8 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
     (lazy
       ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate statement: "
      ^ statement_to_string ctx st ^ "\n"));
+  (* Sanity check *)
+  if config.C.check_invariants then Inv.check_invariants ctx;
   (* Evaluate *)
   match st with
   | A.Assign (p, rvalue) -> (
@@ -4423,6 +4426,8 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx)
   match eval_statement config ctx body with
   | Error err -> Error err
   | Ok (ctx, res) -> (
+      (* Sanity check *)
+      if config.C.check_invariants then Inv.check_invariants ctx;
       match res with
       | Unit | Break _ | Continue _ -> failwith "Inconsistent state"
       | Return -> Ok ctx)
diff --git a/src/Invariants.ml b/src/Invariants.ml
new file mode 100644
index 00000000..f6a5b6b0
--- /dev/null
+++ b/src/Invariants.ml
@@ -0,0 +1,31 @@
+(* The following module defines functions to check that some invariants
+ * are always maintained by evaluation contexts *)
+
+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
+
+(** Check that:
+    - loans and borrows are correctly related
+    - borrows/loans can't contain ⊥ or inactivated mut borrows
+    - shared loans can't contain mutable loans
+    - TODO: a two-phase borrow can't point to a value inside an abstraction
+ *)
+let check_borrows_invariant (ctx : C.eval_ctx) : unit = ()
+
+let check_no_bottom_below_ref_invariant (ctx : C.eval_ctx) : unit = ()
+
+let check_typing_invariant (ctx : C.eval_ctx) : unit = ()
+
+let check_invariants (ctx : C.eval_ctx) : unit =
+  check_borrows_invariant ctx;
+  check_no_bottom_below_ref_invariant ctx;
+  check_typing_invariant ctx
diff --git a/src/Values.ml b/src/Values.ml
index 3af287c7..8ecf8849 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -72,7 +72,7 @@ type symbolic_proj_comp = {
 
 (** Ancestor for iter visitor for [typed_value] *)
 class ['self] iter_typed_value_base =
-  object (self : 'self)
+  object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
     method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
@@ -87,7 +87,7 @@ class ['self] iter_typed_value_base =
 
 (** Ancestor for map visitor for [typed_value] *)
 class ['self] map_typed_value_base =
-  object (self : 'self)
+  object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
     method visit_constant_value : 'env -> constant_value -> constant_value =
@@ -210,7 +210,7 @@ type region = RegionVarId.id Types.region [@@deriving show]
 
 (** Ancestor for iter visitor for [typed_avalue] *)
 class ['self] iter_typed_avalue_base =
-  object (self : 'self)
+  object (_self : 'self)
     inherit [_] iter_typed_value
 
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
@@ -226,7 +226,7 @@ class ['self] iter_typed_avalue_base =
 
 (** Ancestor for MAP visitor for [typed_avalue] *)
 class ['self] map_typed_avalue_base =
-  object (self : 'self)
+  object (_self : 'self)
     inherit [_] map_typed_value
 
     method visit_region : 'env -> region -> region = fun _ r -> r