diff options
| -rw-r--r-- | src/Interpreter.ml | 133 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 8 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 45 |
3 files changed, 134 insertions, 52 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f753206c..0adff0dc 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -12,6 +12,7 @@ open ValuesUtils module Inv = Invariants open InterpreterUtils module S = Synthesis +open Utils (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -74,33 +75,6 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = None with FoundLoanContent lc -> Some lc -(** Check if a region is in a set of regions *) -let region_in_set (r : T.RegionId.id T.region) (rset : T.RegionId.set_t) : bool - = - match r with T.Static -> false | T.Var id -> T.RegionId.Set.mem id rset - -(** Return the set of regions in an rty *) -let rty_regions (ty : T.rty) : T.RegionId.set_t = - let s = ref T.RegionId.Set.empty in - let add_region (r : T.RegionId.id T.region) = - match r with T.Static -> () | T.Var rid -> s := T.RegionId.Set.add rid !s - in - let obj = - object - inherit [_] T.iter_ty - - method! visit_'r _env r = add_region r - end - in - (* Explore the type *) - obj#visit_ty () ty; - (* Return the set of accumulated regions *) - !s - -let rty_regions_intersect (ty : T.rty) (regions : T.RegionId.set_t) : bool = - let ty_regions = rty_regions ty in - not (T.RegionId.Set.disjoint ty_regions regions) - (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that the regions which are already ended inside the abstraction don't @@ -3667,8 +3641,9 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) ctx (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_new (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = +let eval_box_new_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx eval_result = (* Check and retrieve the arguments *) match (region_params, type_params, ctx.env) with | ( [], @@ -3700,7 +3675,7 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list) (** Auxiliary function which factorizes code to evaluate `std::Deref::deref` and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) -let eval_box_deref_mut_or_shared (config : C.config) +let eval_box_deref_mut_or_shared_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx eval_result = (* Check the arguments *) @@ -3735,17 +3710,20 @@ let eval_box_deref_mut_or_shared (config : C.config) | _ -> failwith "Inconsistent state" (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = +let eval_box_deref_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx eval_result = let is_mut = false in - eval_box_deref_mut_or_shared config region_params type_params is_mut ctx + eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut + ctx (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref_mut (config : C.config) +let eval_box_deref_mut_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = let is_mut = true in - eval_box_deref_mut_or_shared config region_params type_params is_mut ctx + eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut + ctx (** Auxiliary function - see [eval_non_local_function_call]. @@ -3768,7 +3746,7 @@ let eval_box_deref_mut (config : C.config) *) let eval_box_free (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) - (ctx : C.eval_ctx) : C.eval_ctx eval_result = + (ctx : C.eval_ctx) : C.eval_ctx = match (region_params, type_params, args) with | [], [ boxed_ty ], [ E.Move input_box_place ] -> (* Required type checking *) @@ -3783,9 +3761,38 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) let ctx = assign_to_place config ctx mk_unit_value dest in (* Return *) - Ok ctx + ctx | _ -> failwith "Inconsistent state" +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_new_symbolic (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + raise Unimplemented + +(** Auxiliary function which factorizes code to evaluate `std::Deref::deref` + and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) +let eval_box_deref_mut_or_shared_symbolic (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + raise Unimplemented + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref_symbolic (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + let is_mut = false in + eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut + ctx + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref_mut_symbolic (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + let is_mut = true in + eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut + ctx + (** Evaluate a non-local function call in concrete mode *) let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) (fid : A.assumed_fun_id) (region_params : T.erased_region list) @@ -3799,7 +3806,7 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) match fid with | A.BoxFree -> (* Degenerate case: box_free *) - eval_box_free config region_params type_params args dest ctx + Ok (eval_box_free config region_params type_params args dest ctx) | _ -> ( (* "Normal" case: not box_free *) (* Evaluate the operands *) @@ -3830,10 +3837,11 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) access to a body. *) let res = match fid with - | A.BoxNew -> eval_box_new config region_params type_params ctx - | A.BoxDeref -> eval_box_deref config region_params type_params ctx + | A.BoxNew -> eval_box_new_concrete config region_params type_params ctx + | A.BoxDeref -> + eval_box_deref_concrete config region_params type_params ctx | A.BoxDerefMut -> - eval_box_deref_mut config region_params type_params ctx + eval_box_deref_mut_concrete config region_params type_params ctx | A.BoxFree -> failwith "Unreachable" (* should have been treated above *) in @@ -3855,11 +3863,45 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) let eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) (fid : A.assumed_fun_id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : - C.eval_ctx eval_result = + C.eval_ctx = (* Synthesis *) S.synthesize_non_local_function_call fid region_params type_params args dest; - raise Unimplemented + (* Sanity check: make sure the type parameters don't contain regions - + * this is a current limitation of our synthesis *) + assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params); + + (* There are two cases (and this is extremely annoying): + - the function is not box_free + - the function is box_free + See [eval_box_free] + *) + match fid with + | A.BoxFree -> + (* Degenerate case: box_free *) + eval_box_free config region_params type_params args dest ctx + | _ -> + (* "Normal" case: not box_free *) + (* Evaluate the operands *) + let ctx, args_vl = eval_operands config ctx args in + + (* Evaluate the function call *) + let ctx, ret_value = + match fid with + | A.BoxNew -> eval_box_new_symbolic config region_params type_params ctx + | A.BoxDeref -> + eval_box_deref_symbolic config region_params type_params ctx + | A.BoxDerefMut -> + eval_box_deref_mut_symbolic config region_params type_params ctx + | A.BoxFree -> failwith "Unreachable" + (* should have been treated above *) + in + + (* Move the return value to its destination *) + let ctx = assign_to_place config ctx ret_value dest in + + (* Return *) + ctx (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` (auxiliary helper for [eval_statement]) *) @@ -3888,8 +3930,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) eval_non_local_function_call_concrete config ctx fid region_params type_params args dest | C.SymbolicMode -> - eval_non_local_function_call_symbolic config ctx fid region_params - type_params args dest + Ok + (eval_non_local_function_call_symbolic config ctx fid region_params + type_params args dest) (** Evaluate a statement *) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 20d4c3af..66ca8998 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -9,6 +9,7 @@ module A = CfimAst module L = Logging open TypesUtils open ValuesUtils +open Utils (** Some utilities *) @@ -147,13 +148,6 @@ type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id -exception Found -(** Utility exception - - When looking for something while exploring a term, it can be easier to - just throw an exception to signal we found what we were looking for. - *) - exception FoundBorrowContent of V.borrow_content (** Utility exception *) diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index 4b3d8b0f..faf77eac 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -1,4 +1,5 @@ open Types +open Utils (** Retrieve the list of fields for the given variant of a [type_def]. @@ -22,6 +23,32 @@ let ty_is_unit (ty : 'r ty) : bool = (** The unit type *) let mk_unit_ty : ety = Adt (Tuple, [], []) +(** Check if a region is in a set of regions *) +let region_in_set (r : RegionId.id region) (rset : RegionId.set_t) : bool = + match r with Static -> false | Var id -> RegionId.Set.mem id rset + +(** Return the set of regions in an rty *) +let rty_regions (ty : rty) : RegionId.set_t = + let s = ref RegionId.Set.empty in + let add_region (r : RegionId.id region) = + match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s + in + let obj = + object + inherit [_] iter_ty + + method! visit_'r _env r = add_region r + end + in + (* Explore the type *) + obj#visit_ty () ty; + (* Return the set of accumulated regions *) + !s + +let rty_regions_intersect (ty : rty) (regions : RegionId.set_t) : bool = + let ty_regions = rty_regions ty in + not (RegionId.Set.disjoint ty_regions regions) + (** Convert an [ety], containing no region variables, to an [rty]. In practice, it is the identity. @@ -43,3 +70,21 @@ let rec ety_no_regions_to_rty (ty : ety) : rty = failwith "Can't convert a ref with erased regions to a ref with non-erased \ regions" + +(** Check if a [ty] contains regions *) +let rec ty_has_regions (ty : ety) : bool = + let obj = + object + inherit [_] iter_ty as super + + method! visit_Adt env type_id regions tys = + if regions = [] then super#visit_Adt env type_id regions tys + else raise Found + + method! visit_Ref _ _ _ _ = raise Found + end + in + try + obj#visit_ty () ty; + false + with Found -> true |