diff options
| -rw-r--r-- | src/Interpreter.ml | 5 | ||||
| -rw-r--r-- | src/Invariants.ml | 31 | ||||
| -rw-r--r-- | src/Values.ml | 8 |
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 |