summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 18:29:01 +0100
committerSon Ho2022-01-04 18:29:01 +0100
commitb05a03dda5d5100f4f714bd120ba1aed4c0130df (patch)
tree78d95c38f9ab92404c038bf436fd003686e5c48a /src
parentfb482999dd7b26a3910ae9ee2dfe650c99cc140f (diff)
Start working on invariant checking
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml5
-rw-r--r--src/Invariants.ml31
-rw-r--r--src/Values.ml8
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