summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-08 15:52:39 +0100
committerSon Ho2021-12-08 15:52:39 +0100
commit0f504d23898edea2158a08d1f367f5a120131ca0 (patch)
tree4cd05b1d0a89e401f0768b4e5fea2c62f935baf4
parentfecddc900d35ae9cbf13213824b3e7e079f3a681 (diff)
Make minor modifications
-rw-r--r--src/CfimAst.ml4
-rw-r--r--src/Interpreter.ml64
-rw-r--r--src/Values.ml23
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;
}