diff options
| -rw-r--r-- | src/CfimAst.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 64 | ||||
| -rw-r--r-- | src/Values.ml | 23 |
3 files changed, 16 insertions, 75 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 0e36f6df..64151a48 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -10,8 +10,8 @@ type var = { name : string option; var_ty : ety; (** The variable type - erased type, because variables are not used - ** in function signatures - TODO: useless? TODO: binder type for - function definitions *) + ** in function signatures: they are only used to declare the list of + ** variables manipulated by a function body *) } [@@deriving show] (** A variable, as used in a function definition *) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 5ffc0908..d34c20dc 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -90,23 +90,6 @@ let borrows_in_value (v : V.typed_value) : bool = false with Found -> true -(** Check a predicate on all the loans in a value - TODO: remove? *) -let forall_borrows_in_value (pred : V.borrow_content -> bool) - (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content env lc = - if not (pred lc) then raise Found else super#visit_borrow_content env lc - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - true - with Found -> false - (** Check if a value contains inactivated mutable borrows *) let inactivated_in_value (v : V.typed_value) : bool = let obj = @@ -137,43 +120,6 @@ let loans_in_value (v : V.typed_value) : bool = false with Found -> true -(** Check a predicate on all the loans in a value - TODO: remove?*) -let forall_loans_in_value (pred : V.loan_content -> bool) (v : V.typed_value) : - bool = - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_loan_content env lc = - if not (pred lc) then raise Found else super#visit_loan_content env lc - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - true - with Found -> false - -(** Return true if there are mutable borrows/loans or inactivated mut borrows - in the value - TODO: remove? *) -let mut_inactivated_borrows_loans_in_value (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value - - method! visit_MutLoan _ _ = raise Found - - method! visit_MutBorrow _ _ = raise Found - - method! visit_InactivatedMutBorrow _ _ = raise Found - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - false - with Found -> true - (** Lookup a loan content. The loan is referred to by a borrow id. @@ -821,11 +767,13 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : (* Check that there is only one borrow id (l) and update the loan *) assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); (* We need to check that there aren't any loans in the value: - we should have gotten rid of those already, but it is better - to do a sanity check. *) + we should have gotten rid of those already, but it is better + to do a sanity check. *) assert (not (loans_in_value sv)); - (* Also need to check there isn't [Bottom] (this is actually an invariant *) + (* Check there isn't [Bottom] (this is actually an invariant *) assert (not (bottom_in_value sv)); + (* Check there aren't inactivated borrows *) + assert (not (inactivated_in_value sv)); (* Update the loan content *) let env = update_loan ek l (V.MutLoan l) ctx.env in let ctx = { ctx with env } in @@ -1878,7 +1826,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : let aty = T.Adt (T.AdtId def_id, regions, types) in Ok (ctx, { V.value = Adt av; ty = aty })) -(** Result of evaluating a statement - TODO: add prefix *) +(** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return (** Small utility. diff --git a/src/Values.ml b/src/Values.ml index aabd41c2..78923e5e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -1,12 +1,6 @@ open Identifiers open Types -(** TODO: do we put the type variable/variable/region names everywhere - (to not have to perform lookups by using the ids?) - No: it is good not to duplicate and to use ids. This allows to split/ - make very explicit the role of variables/identifiers/binders/etc. - *) - module VarId = IdGen () module BorrowId = IdGen () @@ -199,22 +193,21 @@ class ['self] map_typed_avalue_base = method visit_rty : 'env -> rty -> rty = fun _ ty -> ty end +(** Abstraction values are used inside of abstractions to properly model + borrowing relations introduced by function calls. + + When calling a function, we lose information about the borrow graph: + part of it is thus "abstracted" away. +*) type avalue = | AConcrete of constant_value - | AAdt of aadt_value + | AAdt of adt_avalue | ABottom | ALoan of aloan_content | ABorrow of aborrow_content | ASymbolic of aproj - (** Abstraction values are used inside of abstractions to properly model - borrowing relations introduced by function calls. - - When calling a function, we lose information about the borrow graph: - part of it is thus "abstracted" away. -*) -(* TODO: rename to adt_avalue? *) -and aadt_value = { +and adt_avalue = { variant_id : (VariantId.id option[@opaque]); field_values : typed_avalue list; } |