diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimAst.ml | 1 | ||||
| -rw-r--r-- | src/Interpreter.ml | 55 | ||||
| -rw-r--r-- | src/Types.ml | 1 | ||||
| -rw-r--r-- | src/Values.ml | 12 |
4 files changed, 54 insertions, 15 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 36977aad..d2bf9181 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -58,6 +58,7 @@ type expression = | Switch of operand * switch_targets | Loop of expression [@@deriving show] +(* TODO: merge with statement *) and switch_targets = | If of expression * expression (** Gives the "if" and "else" blocks *) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d737f79d..57a4e08b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -21,6 +21,8 @@ module L = Logging where invariants might be broken, etc. *) +(* TODO: test with PLT-redex *) + (** Some utilities *) let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string @@ -901,7 +903,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) (** When we fail reading from or writing to a path, it might be because we need to update the environment by ending borrows, expanding symbolic - values, etc. The following type is used to convey this information. *) + values, etc. The following type is used to convey this information. + + TODO: compare with borrow_lres? +*) type path_fail_kind = | FailSharedLoan of V.BorrowId.Set.t (** Failure because we couldn't go inside a shared loan *) @@ -912,6 +917,7 @@ type path_fail_kind = (which should get activated) *) | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp) (** Failure because we need to enter a symbolic value (and thus need to expand it) *) + (* TODO: Remove the parentheses *) | FailBottom of (int * E.projection_elem * T.ety) (** Failure because we need to enter an any value - we can expand Bottom values if they are left values. We return the number of elements which @@ -1348,7 +1354,9 @@ exception UpdateCtx of C.eval_ctx This is used when reading, borrowing, writing to a value. We typically first call [update_ctx_along_read_place] or [update_ctx_along_write_place] - to get access to the value, then call this function to "prepare" the value. + to get access to the value, then call this function to "prepare" the value: + when moving values, we can't move a value which contains loans and thus need + to end them, etc. *) let rec end_loans_at_place (config : C.config) (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = @@ -1360,7 +1368,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) In particular, we need to end the proper loans in the value. Also, we fail if the value contains any [Bottom]. - We use exceptions to make it handy. + We use exceptions to make it handy: whenever we update the + context, we raise an exception wrapping the updated context. *) let rec inspect_update v : unit = match v.V.value with @@ -1400,15 +1409,17 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) in (* Inspect the value and update the context while doing so. If the context gets updated: perform a recursive call (many things - may have been updated in the context: first we need to retrieve the - proper updated value - and this value may actually not be accessible - anymore + may have been updated in the context: we need to re-read the value + at place [p] - and this value may actually not be accessible + anymore...) *) try inspect_update v; (* No context update required: return the current context *) ctx - with UpdateCtx ctx -> end_loans_at_place config access p ctx) + with UpdateCtx ctx -> + (* The context was updated: do a recursive call to reinspect the value *) + end_loans_at_place config access p ctx) (** Drop (end) all the loans and borrows at a given place, which should be seen as an l-value (we will write to it later, but need to drop the borrows @@ -1878,12 +1889,12 @@ type statement_eval_res = Unit | Break of int | Continue of int | Return (** Small utility. Prepare a place which is to be used as the destination of an assignment: - update the environment along the paths, collect the borrows (to end the - loans) at the place, then drop the borrows. + update the environment along the paths, end the borrows and loans at + this place, etc. - Return the updated value at the end of the place. This value is likely - to contain [Bottom] values (as we drop borrows) but should not contain - any loan or borrow. + Return the updated context and the (updated) value at the end of the + place. This value should not contain any loan or borrow (and we check + it is the case). Note that it is very likely to contain [Bottom] values. *) let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = @@ -1901,7 +1912,12 @@ let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : (ctx, v) (** Read the value at a given place. - As long as it is a loan, end the loan *) + As long as it is a loan, end the loan. + This function doesn't perform a recursive exploration: + it won't dive into the value to end all the inner + loans (contrary to [drop_borrows_loans_at_lplace] for + instance). + *) let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = let v = read_place_unwrap config access p ctx in @@ -1914,6 +1930,17 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) end_loan_exactly_at_place config access p ctx | _ -> ctx +(** Updates the discriminant of a value at a given place. + + There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one (because the variant is not the proper + one, or the value is actually [Bottom] - this happens when + initializing ADT values), in which case we replace the value with + a variant with all its fields set to [Bottom]. + For instance, something like: `Cons Bottom Bottom`. + *) let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) (variant_id : T.VariantId.id) : (C.eval_ctx * statement_eval_res) eval_result = @@ -2466,6 +2493,8 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : (** Test a unit function (taking no arguments) by evaluating it in an empty environment + + TODO: put in a sub-module *) let test_unit_function (type_defs : T.type_def list) (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result = diff --git a/src/Types.ml b/src/Types.ml index 2b57e3f7..fce5c827 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -75,6 +75,7 @@ type 'r ty = | Ref of 'r * 'r ty * ref_kind | Assumed of assumed_ty * 'r list * 'r ty list [@@deriving show] +(* TODO: group Bool, Char, etc. in Constant *) type rty = RegionVarId.id region ty [@@deriving show] (** Type with *R*egions. diff --git a/src/Values.ml b/src/Values.ml index 3e6bc838..57a0aeb0 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -82,9 +82,12 @@ type value = | Concrete of constant_value (** Concrete (non-symbolic) value *) | Adt of adt_value (** Enumerations and structures *) | Tuple of typed_value list - (** Tuple - note that units are encoded as 0-tuples *) + (** Tuple - note that units are encoded as 0-tuples + TODO: merge with Adt? + *) | Bottom (** No value (uninitialized or moved value) *) - | Assumed of assumed_value (** Assumed types (Box, Vec, Cell...) *) + | Assumed of assumed_value + (** Value of an abstract type (Box, Vec, Cell...) *) | Borrow of borrow_content (** A borrowed value *) | Loan of loan_content (** A loaned value *) | Symbolic of symbolic_proj_comp (** Unknown value *) @@ -92,9 +95,12 @@ type value = and adt_value = { def_id : TypeDefId.id; + (* TODO: remove *) variant_id : VariantId.id option; regions : erased_region list; + (* TODO: remove *) types : ety list; + (* TODO: remove *) field_values : typed_value list; } [@@deriving show] @@ -147,6 +153,7 @@ type avalue = | AAssumed of aassumed_value | AProj of aproj [@@deriving show] +(* TODO: merge with value *) and aadt_value = { adef_id : TypeDefId.id; @@ -156,6 +163,7 @@ and aadt_value = { afield_values : typed_avalue list; } [@@deriving show] +(* TODO: merge with adt_value *) and aloan_content = | AMutLoan of BorrowId.id * typed_avalue |