diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 1 | ||||
| -rw-r--r-- | src/Interpreter.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 80 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 77 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 6 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 5 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 33 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 29 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 78 | ||||
| -rw-r--r-- | src/Invariants.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 12 | ||||
| -rw-r--r-- | src/Values.ml | 45 |
12 files changed, 116 insertions, 255 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 89056680..5225645c 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -67,6 +67,7 @@ type eval_ctx = { fun_context : fun_def list; type_vars : type_var list; env : env; + ended_regions : RegionId.set_t; symbolic_counter : SymbolicValueId.generator; (* TODO: make this global? *) borrow_counter : BorrowId.generator; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 384e0a11..54911d85 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -30,6 +30,7 @@ module Test = struct C.fun_context = fun_defs; C.type_vars; C.env = []; + C.ended_regions = T.RegionId.Set.empty; C.symbolic_counter = V.SymbolicValueId.generator_zero; C.borrow_counter = V.BorrowId.generator_zero; C.region_counter = T.RegionId.generator_zero; diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index fbd958ef..3cfa78e0 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -626,13 +626,7 @@ let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) : (* Generate the fresh a symbolic value *) let ctx, sv_id = C.fresh_symbolic_value_id ctx in let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in - let value : V.symbolic_proj_comp = - (* Note that the set of ended regions is empty: we shouldn't have to take - * into account any ended regions at this point, otherwise we would be in - * the first case where we should return ⊥ *) - { V.svalue; V.rset_ended = T.RegionId.Set.empty } - in - let value = V.Symbolic value in + let value = V.Symbolic svalue in (ctx, { V.value; V.ty }) (** End a borrow identified by its borrow id in a context @@ -759,8 +753,15 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) let ctx = end_abstraction_loans config abs_id ctx in (* End the abstraction itself by redistributing the borrows it contains *) let ctx = end_abstraction_borrows config abs_id ctx in - (* End the regions owned by the abstraction *) - let ctx = end_abstraction_regions config abs_id ctx in + (* End the regions owned by the abstraction - note that we don't need to + * relookup the abstraction: the set of regions in an abstraction never + * changes... *) + let ctx = + { + ctx with + ended_regions = T.RegionId.Set.union ctx.ended_regions abs.V.regions; + } + in (* Remove all the references to the id of the current abstraction, and remove * the abstraction itself *) end_abstraction_remove_from_context config abs_id ctx @@ -911,63 +912,6 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) (* Reexplore *) end_abstraction_borrows config abs_id ctx -(** Update the symbolic values in a context to register the regions in the - abstraction we are ending as already ended. - Note that this function also checks that no symbolic value in an abstraction - contains regions which we are ending. - Of course, we ignore the abstraction we are currently ending... - *) -and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the abstraction to retrieve the set of owned regions *) - let abs = C.ctx_lookup_abs ctx abs_id in - let ended_regions = abs.V.regions in - (* Update all the symbolic values in the context *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic _ sproj = - let sproj = - { - sproj with - V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions; - } - in - V.Symbolic sproj - - method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj = - (* Sanity check *) - (match aproj with - | V.AProjLoans _ -> () - | V.AProjBorrows (sv, ty) -> ( - match abs_regions with - | None -> failwith "Unexpected" - | Some abs_regions -> - assert ( - not - (projections_intersect sv.V.sv_ty ended_regions ty - abs_regions)))); - (* Return - nothing to update *) - aproj - - method! visit_abs (regions : T.RegionId.set_t option) abs = - if abs.V.abs_id = abs_id then abs - else ( - assert (Option.is_none regions); - (* Check that we don't project over already ended regions *) - assert (T.RegionId.Set.disjoint ended_regions abs.V.regions); - (* Remember the set of regions owned by the abstraction *) - let regions = Some abs.V.regions in - super#visit_abs regions abs) - (** Whenever we dive in an abstraction, we need to keep track of the - set of regions owned by the abstraction. - Also: we don't dive in the abstraction we are currently ending... *) - end - in - (* Update the context *) - obj#visit_eval_ctx None ctx - (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : C.config) (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = @@ -1022,7 +966,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : to do a sanity check. *) assert (not (loans_in_value sv)); (* Check there isn't [Bottom] (this is actually an invariant *) - assert (not (bottom_in_value sv)); + assert (not (bottom_in_value ctx.ended_regions sv)); (* Check there aren't inactivated borrows *) assert (not (inactivated_in_value sv)); (* Update the loan content *) @@ -1094,7 +1038,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) ("activate_inactivated_mut_borrow: resulting value:\n" ^ V.show_typed_value sv)); assert (not (loans_in_value sv)); - assert (not (bottom_in_value sv)); + assert (not (bottom_in_value ctx.ended_regions sv)); assert (not (inactivated_in_value sv)); (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 7366a819..24ec018e 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -152,7 +152,7 @@ let replace_symbolic_values (at_most_once : bool) inherit [_] C.map_eval_ctx as super method! visit_Symbolic env spc = - if same_symbolic_id spc.V.svalue original_sv then replace () + if same_symbolic_id spc original_sv then replace () else super#visit_Symbolic env spc end in @@ -190,9 +190,9 @@ let apply_symbolic_expansion_non_borrow (config : C.config) doesn't allow the expansion of enumerations *containing several variants*. *) let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list = + (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list) + (types : T.rty list) (ctx : C.eval_ctx) : + (C.eval_ctx * symbolic_expansion) list = (* Lookup the definition and check if it is an enumeration with several * variants *) let def = C.ctx_lookup_type_def ctx def_id in @@ -210,8 +210,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) C.eval_ctx * symbolic_expansion = let ctx, field_values = List.fold_left_map - (fun ctx (ty : T.rty) -> - mk_fresh_symbolic_proj_comp ended_regions ty ctx) + (fun ctx (ty : T.rty) -> mk_fresh_symbolic_value ty ctx) ctx field_types in let see = SeAdt (variant_id, field_values) in @@ -220,32 +219,29 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (* Initialize all the expanded values of all the variants *) List.map (initialize ctx) variants_fields_types -let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) - (field_types : T.rty list) (ctx : C.eval_ctx) : - C.eval_ctx * symbolic_expansion = +let compute_expanded_symbolic_tuple_value (field_types : T.rty list) + (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion = (* Generate the field values *) let ctx, field_values = List.fold_left_map - (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx) + (fun ctx sv_ty -> mk_fresh_symbolic_value sv_ty ctx) ctx field_types in let variant_id = None in let see = SeAdt (variant_id, field_values) in (ctx, see) -let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) - (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion = +let compute_expanded_symbolic_box_value (boxed_ty : T.rty) (ctx : C.eval_ctx) : + C.eval_ctx * symbolic_expansion = (* Introduce a fresh symbolic value *) - let ctx, boxed_value = - mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx - in + let ctx, boxed_value = mk_fresh_symbolic_value boxed_ty ctx in let see = SeAdt (None, [ boxed_value ]) in (ctx, see) let expand_symbolic_value_shared_borrow (config : C.config) - (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) - (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx = - (* First, replace the projectors on borrows (AProjBorrow and proj_comp) + (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) : + C.eval_ctx = + (* First, replace the projectors on borrows. * The important point is that the symbolic value to expand may appear * several times, if it has been copied. In this case, we need to introduce * one fresh borrow id per instance. @@ -285,7 +281,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) inherit [_] C.map_eval_ctx as super method! visit_Symbolic env sv = - if same_symbolic_id sv.V.svalue original_sv then + if same_symbolic_id sv original_sv then let bid = fresh_borrow () in V.Borrow (V.SharedBorrow bid) else super#visit_Symbolic env sv @@ -326,7 +322,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) (* Finally, replace the projectors on loans *) let bids = !borrows in assert (not (V.BorrowId.Set.is_empty bids)); - let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in + let ctx, shared_sv = mk_fresh_symbolic_value ref_ty ctx in let see = SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = @@ -339,17 +335,16 @@ let expand_symbolic_value_shared_borrow (config : C.config) ctx let expand_symbolic_value_borrow (config : C.config) - (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) - (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) - (ctx : C.eval_ctx) : C.eval_ctx = + (original_sv : V.symbolic_value) (region : T.RegionId.id T.region) + (ref_ty : T.rty) (rkind : T.ref_kind) (ctx : C.eval_ctx) : C.eval_ctx = (* Check that we are allowed to expand the reference *) - assert (not (region_in_set region ended_regions)); + assert (not (region_in_set region ctx.ended_regions)); (* Match on the reference kind *) match rkind with | T.Mut -> (* Simple case: simply create a fresh symbolic value and a fresh * borrow id *) - let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in + let ctx, sv = mk_fresh_symbolic_value ref_ty ctx in let ctx, bid = C.fresh_borrow_id ctx in let see = SeMutRef (bid, sv) in (* Expand the symbolic values - we simply perform a substitution (and @@ -370,8 +365,7 @@ let expand_symbolic_value_borrow (config : C.config) (* Return *) ctx | T.Shared -> - expand_symbolic_value_shared_borrow config original_sv ended_regions - ref_ty ctx + expand_symbolic_value_shared_borrow config original_sv ref_ty ctx (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). @@ -379,13 +373,12 @@ let expand_symbolic_value_borrow (config : C.config) This function is used when exploring paths. *) let expand_symbolic_value_no_branching (config : C.config) - (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : + (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) - let original_sv = sp.V.svalue in + let original_sv = sp in let rty = original_sv.V.sv_ty in - let ended_regions = sp.V.rset_ended in let ctx = match (pe, rty) with (* "Regular" ADTs *) @@ -396,8 +389,8 @@ let expand_symbolic_value_no_branching (config : C.config) * don't allow to expand enumerations with strictly more than one variant *) let expand_enumerations = false in match - compute_expanded_symbolic_adt_value expand_enumerations ended_regions - def_id regions types ctx + compute_expanded_symbolic_adt_value expand_enumerations def_id regions + types ctx with | [ (ctx, see) ] -> (* Apply in the context *) @@ -413,9 +406,7 @@ let expand_symbolic_value_no_branching (config : C.config) | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> assert (arity = List.length tys); (* Generate the field values *) - let ctx, see = - compute_expanded_symbolic_tuple_value ended_regions tys ctx - in + let ctx, see = compute_expanded_symbolic_tuple_value tys ctx in (* Apply in the context *) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx @@ -426,9 +417,7 @@ let expand_symbolic_value_no_branching (config : C.config) ctx (* Boxes *) | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - let ctx, see = - compute_expanded_symbolic_box_value ended_regions boxed_ty ctx - in + let ctx, see = compute_expanded_symbolic_box_value boxed_ty ctx in (* Apply in the context *) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx @@ -439,8 +428,7 @@ let expand_symbolic_value_no_branching (config : C.config) ctx (* Borrows *) | Deref, T.Ref (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config original_sv ended_regions region - ref_ty rkind ctx + expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx | _ -> failwith ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) @@ -454,13 +442,12 @@ let expand_symbolic_value_no_branching (config : C.config) This might lead to branching. *) -let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp) +let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx list = (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) - let original_sv = sp.V.svalue in + let original_sv = sp in let rty = original_sv.V.sv_ty in - let ended_regions = sp.V.rset_ended in match rty with (* The value should be a "regular" ADTs *) | T.Adt (T.AdtId def_id, regions, types) -> @@ -468,8 +455,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp) * don't allow to expand enumerations with strictly more than one variant *) let expand_enumerations = true in let res = - compute_expanded_symbolic_adt_value expand_enumerations ended_regions - def_id regions types ctx + compute_expanded_symbolic_adt_value expand_enumerations def_id regions + types ctx in (* Update the synthesized program *) let seel = List.map (fun (_, x) -> x) res in diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index e379eacd..f9b1ab3c 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -87,7 +87,7 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) let access = Move in prepare_rplace config access p ctx in - assert (not (bottom_in_value v)); + assert (not (bottom_in_value ctx.ended_regions v)); (ctx, v) (** Evaluate an operand. *) @@ -109,7 +109,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let ctx, v = prepare_rplace config access p ctx in (* Copy the value *) L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value v)); + assert (not (bottom_in_value ctx.ended_regions v)); let allow_adt_copy = false in copy_value allow_adt_copy config ctx v | Expressions.Move p -> ( @@ -118,7 +118,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let ctx, v = prepare_rplace config access p ctx in (* Move the value *) L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value v)); + assert (not (bottom_in_value ctx.ended_regions v)); let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with | Error _ -> failwith "Unreachable" diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 80725bab..bfe877ab 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -28,7 +28,7 @@ type path_fail_kind = | FailInactivatedMutBorrow of V.BorrowId.id (** Failure because we couldn't go inside an inactivated mutable borrow (which should get activated) *) - | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp) + | FailSymbolic of (E.projection_elem * V.symbolic_value) (** 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) @@ -774,8 +774,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * Note that in the general case, copy is a trait: copying values * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) - assert ( - type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.V.sv_ty)); + assert (type_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty)); (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values * is symbolic expansion. The important subcase is the expansion of shared diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index ada1a89a..21c9e034 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -13,9 +13,9 @@ open InterpreterBorrowsCore (** A symbolic expansion *) type symbolic_expansion = | SeConcrete of V.constant_value - | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list) - | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp - | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp + | SeAdt of (T.VariantId.id option * V.symbolic_value list) + | SeMutRef of V.BorrowId.id * V.symbolic_value + | SeSharedRef of V.BorrowId.set_t * V.symbolic_value (** Auxiliary function. @@ -92,8 +92,9 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) asb | V.Loan _, _ -> failwith "Unreachable" | V.Symbolic s, _ -> - assert (not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions)); - [ V.AsbProjReborrows (s.V.svalue, ty) ] + (* Check that the projection doesn't contain ended regions *) + assert (not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); + [ V.AsbProjReborrows (s, ty) ] | _ -> failwith "Unreachable" (** Apply (and reduce) a projector over borrows to a value. @@ -212,12 +213,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) V.ABorrow bc | V.Loan _, _ -> failwith "Unreachable" | V.Symbolic s, _ -> - (* Check that the symbolic value doesn't contain already ended regions, + (* Check that the projection doesn't contain already ended regions, * if necessary *) if check_symbolic_no_ended then assert ( - not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions)); - V.ASymbolic (V.AProjBorrows (s.V.svalue, ty)) + not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); + V.ASymbolic (V.AProjBorrows (s, ty)) | _ -> failwith "Unreachable" in { V.value; V.ty } @@ -231,7 +232,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) | SeConcrete cv -> V.Concrete cv | SeAdt (variant_id, field_values) -> let field_values = - List.map mk_typed_value_from_proj_comp field_values + List.map mk_typed_value_from_symbolic_value field_values in V.Adt { V.variant_id; V.field_values } | SeMutRef (_, _) | SeSharedRef (_, _) -> @@ -250,7 +251,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) match see with | SeMutRef (bid, bv) -> let ty = Subst.erase_regions sv.V.sv_ty in - let bv = mk_typed_value_from_proj_comp bv in + let bv = mk_typed_value_from_symbolic_value bv in let value = V.Borrow (V.MutBorrow (bid, bv)) in { V.value; ty } | SeSharedRef (_, _) -> @@ -271,14 +272,14 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) -> (* Project over the field values *) let field_values = - List.map mk_aproj_loans_from_proj_comp field_values + List.map mk_aproj_loans_from_symbolic_value field_values in (V.AAdt { V.variant_id; field_values }, original_sv_ty) | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> (* Sanity check *) - assert (spc.V.svalue.V.sv_ty = ref_ty); + assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_proj_comp spc in + let child_av = mk_aproj_loans_from_symbolic_value spc in (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) if region_in_set r regions then @@ -289,14 +290,14 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty) | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) -> (* Sanity check *) - assert (spc.V.svalue.V.sv_ty = ref_ty); + assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_proj_comp spc in + let child_av = mk_aproj_loans_from_symbolic_value spc in (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) if region_in_set r regions then (* In the set: keep *) - let shared_value = mk_typed_value_from_proj_comp spc in + let shared_value = mk_typed_value_from_symbolic_value spc in (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty) else (* Not in the set: ignore *) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 5eee5296..c4bbdf23 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -74,10 +74,8 @@ let eval_assertion (config : C.config) (ctx : C.eval_ctx) * `true` *) S.synthesize_assert v; let see = SeConcrete (V.Bool true) in - let ctx = - apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx - in - S.synthesize_symbolic_expansion_no_branching sv.V.svalue see; + let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in + S.synthesize_symbolic_expansion_no_branching sv see; (* We can finally fully evaluate the operand *) let ctx, _ = eval_operand config ctx assertion.cond in Ok ctx @@ -641,15 +639,13 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) else eval_statement config ctx st2 | V.Symbolic sv -> (* Synthesis *) - S.synthesize_symbolic_expansion_if_branching sv.V.svalue; + S.synthesize_symbolic_expansion_if_branching sv; (* Expand the symbolic value to true or false *) let see_true = SeConcrete (V.Bool true) in let see_false = SeConcrete (V.Bool false) in let expand_and_execute see st = (* Apply the symbolic expansion *) - let ctx = - apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx - in + let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in (* Evaluate the operand *) let ctx, _ = eval_operand config ctx op in (* Evaluate the branch *) @@ -674,7 +670,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) | Some (_, tgt) -> eval_statement config ctx tgt) | V.Symbolic sv -> (* Synthesis *) - S.synthesize_symbolic_expansion_switch_int_branching sv.V.svalue; + S.synthesize_symbolic_expansion_switch_int_branching sv; (* For all the branches of the switch, we expand the symbolic value * to the value given by the branch and execute the branch statement. * For the otherwise branch, we leave the symbolic value as it is @@ -685,9 +681,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) let exec_branch (switch_value, branch_st) = let see = SeConcrete (V.Scalar switch_value) in (* Apply the symbolic expansion *) - let ctx = - apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx - in + let ctx = apply_symbolic_expansion_non_borrow config sv see ctx in (* Evaluate the operand *) let ctx, _ = eval_operand config ctx op in (* Evaluate the branch *) @@ -810,11 +804,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (args : E.operand list) (dest : E.place) : C.eval_ctx = (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in - let ctx, ret_spc = - mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx - in - let ret_value = mk_typed_value_from_proj_comp ret_spc in - let ret_av = mk_aproj_loans_from_symbolic_value ret_spc.V.svalue in + let ctx, ret_spc = mk_fresh_symbolic_value ret_sv_ty ctx in + let ret_value = mk_typed_value_from_symbolic_value ret_spc in + let ret_av = mk_aproj_loans_from_symbolic_value ret_spc in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in let args_with_rtypes = List.combine args inst_sg.A.inputs in @@ -857,8 +849,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (* Move the return value to its destination *) let ctx = assign_to_place config ctx ret_value dest in (* Synthesis *) - S.synthesize_function_call fid region_params type_params args dest - ret_spc.V.svalue; + S.synthesize_function_call fid region_params type_params args dest ret_spc; (* Return *) ctx diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 458c11b4..fcc6050f 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -51,51 +51,19 @@ let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) : let svalue = { V.sv_id; V.sv_ty = ty } in (ctx, svalue) -(** Create a fresh symbolic proj comp *) -let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty) - (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp = - let ctx, svalue = mk_fresh_symbolic_value ty ctx in - let sv = { V.svalue; rset_ended = ended_regions } in - (ctx, sv) - -(** Create a fresh symbolic value (as a complementary projector) *) -let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t) - (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in - let value : V.value = V.Symbolic sv in - let ty : T.ety = Subst.erase_regions ty in - let sv : V.typed_value = { V.value; ty } in - (ctx, sv) - -let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value = - let ty = Subst.erase_regions sv.V.svalue.V.sv_ty in - let value = V.Symbolic sv in - { V.value; ty } - -(** Create a typed value from a symbolic value. - - Initializes the set of ended regions with `empty`. - *) +(** Create a typed value from a symbolic value. *) let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : V.typed_value = - let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in - mk_typed_value_from_proj_comp spc - -let mk_aproj_loans_from_proj_comp (spc : V.symbolic_proj_comp) : V.typed_avalue - = - let ty = spc.V.svalue.V.sv_ty in - let proj = V.AProjLoans spc.V.svalue in - let value = V.ASymbolic proj in - { V.value; ty } - -(** Create a Loans projector from a symbolic value. + let av = V.Symbolic svalue in + let av : V.typed_value = + { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty } + in + av - Initializes the set of ended regions with `empty`. - *) +(** Create a loans projector from a symbolic value. *) let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) : V.typed_avalue = - let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in - let av = V.ASymbolic (V.AProjLoans spc.V.svalue) in + let av = V.ASymbolic (V.AProjLoans svalue) in let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in av @@ -162,7 +130,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : inherit [_] C.iter_eval_ctx method! visit_Symbolic _ sv = - if sv.V.svalue.V.sv_id = sv_id then raise Found else () + if sv.V.sv_id = sv_id then raise Found else () method! visit_ASymbolic _ aproj = match aproj with @@ -228,36 +196,33 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) || projections_intersect ty1 rset1 ty2 rset2 | _ -> failwith "Unreachable" -(** Check if the ended regions of a comp projector over a symbolic value - intersect the regions listed in another projection *) -let symbolic_proj_comp_ended_regions_intersect_proj (s : V.symbolic_proj_comp) - (ty : T.rty) (regions : T.RegionId.set_t) : bool = - projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions - (** Check that a symbolic value doesn't contain ended regions. Note that we don't check that the set of ended regions is empty: we check that the set of ended regions doesn't intersect the set of regions used in the type (this is more general). *) -let symbolic_proj_comp_ended_regions (s : V.symbolic_proj_comp) : bool = - let regions = rty_regions s.V.svalue.V.sv_ty in - not (T.RegionId.Set.disjoint regions s.rset_ended) +let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t) + (s : V.symbolic_value) : bool = + let regions = rty_regions s.V.sv_ty in + not (T.RegionId.Set.disjoint regions ended_regions) (** Check if a [value] contains ⊥. Note that this function is very general: it also checks wether symbolic values contain already ended regions. *) -let bottom_in_value (v : V.typed_value) : bool = +let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) : + bool = let obj = object inherit [_] V.iter_typed_value method! visit_Bottom _ = raise Found - method! visit_symbolic_proj_comp _ s = - if symbolic_proj_comp_ended_regions s then raise Found else () + method! visit_symbolic_value _ s = + if symbolic_value_has_ended_regions ended_regions s then raise Found + else () end in (* We use exceptions *) @@ -273,7 +238,7 @@ let bottom_in_value (v : V.typed_value) : bool = TODO: remove? *) -let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) : +let bottom_in_avalue (ended_regions : T.RegionId.set_t) (v : V.typed_avalue) : bool = let obj = object @@ -281,8 +246,9 @@ let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) : method! visit_Bottom _ = raise Found - method! visit_symbolic_proj_comp _ sv = - if symbolic_proj_comp_ended_regions sv then raise Found else () + method! visit_symbolic_value _ sv = + if symbolic_value_has_ended_regions ended_regions sv then raise Found + else () method! visit_aproj _ ap = (* Nothing to do actually *) diff --git a/src/Invariants.ml b/src/Invariants.ml index 11b00381..86fa3d46 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -433,8 +433,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | Abstract (V.AMutBorrow (_, sv)) -> assert (Subst.erase_regions sv.V.ty = ty) | _ -> failwith "Inconsistent context")) - | V.Symbolic spc, ty -> - let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in + | V.Symbolic sv, ty -> + let ty' = Subst.erase_regions sv.V.sv_ty in assert (ty' = ty) | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) diff --git a/src/Print.ml b/src/Print.ml index 0b436f1a..f714e847 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -214,11 +214,6 @@ module Values = struct (sv : V.symbolic_value) : string = symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty - let symbolic_proj_comp_to_string (fmt : PT.rtype_formatter) - (sp : V.symbolic_proj_comp) : string = - let regions = T.RegionId.set_to_string sp.rset_ended in - "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")" - let symbolic_value_proj_to_string (fmt : value_formatter) (sv : V.symbolic_value) (rty : T.rty) : string = symbolic_value_id_to_string sv.sv_id @@ -275,8 +270,7 @@ module Values = struct | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty | Borrow bc -> borrow_content_to_string fmt bc | Loan lc -> loan_content_to_string fmt lc - | Symbolic s -> - symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) s + | Symbolic s -> symbolic_value_to_string (value_to_rtype_formatter fmt) s and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) : string = @@ -539,6 +533,7 @@ module Contexts = struct let eval_ctx_to_string (ctx : C.eval_ctx) : string = let fmt = eval_ctx_to_ctx_formatter ctx in + let ended_regions = T.RegionId.set_to_string ctx.ended_regions in let frames = split_env_according_to_frames ctx.env in let num_frames = List.length frames in let frames = @@ -547,7 +542,8 @@ module Contexts = struct "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n") frames in - "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames + "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames + ^ " frame(s)\n" ^ String.concat "" frames end module PC = Contexts (* local module *) diff --git a/src/Values.ml b/src/Values.ml index 47bdda23..b6bb414b 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -47,35 +47,7 @@ type constant_value = type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } [@@deriving show] -(** Symbolic value. - - TODO: a symbolic value may not always have the same type!! - For references: - - a projector on loans may see a symbolic value of id `sid` as having type `T` - - a projector on borrows may see it as having type `&mut T` - We need to make this clear and more consistant. - So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj]. - The kind of projector will then depend on the context. - Actually, maybe we shouldn't use this type. Or for abstractions we should - use different types. Something like: - - [proj_borrows] for values - - [aproj_loans], [aproj_borrows] for avalues - *) - -(** TODO: make it clear that complementary projectors are projectors on borrows. - ** TODO: actually this is useless: the set of ended regions should be global! - ** (and thus stored in the context) *) -type symbolic_proj_comp = { - svalue : symbolic_value; (** The symbolic value itself *) - rset_ended : RegionId.set_t; - (** The regions used in the symbolic value which have already ended *) -} -[@@deriving show] -(** A complementary projector over a symbolic value. - - "Complementary" stands for the fact that it is a projector over all the - regions *but* the ones which are listed in the projector. -*) +(** A symbolic value *) (** Ancestor for [typed_value] iter visitor *) class ['self] iter_typed_value_base = @@ -86,8 +58,7 @@ class ['self] iter_typed_value_base = method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> () - method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit = - fun _ _ -> () + method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> () method visit_ety : 'env -> ety -> unit = fun _ _ -> () end @@ -103,8 +74,7 @@ class ['self] map_typed_value_base = method visit_erased_region : 'env -> erased_region -> erased_region = fun _ r -> r - method visit_symbolic_proj_comp - : 'env -> symbolic_proj_comp -> symbolic_proj_comp = + method visit_symbolic_value : 'env -> symbolic_value -> symbolic_value = fun _ sv -> sv method visit_ety : 'env -> ety -> ety = fun _ ty -> ty @@ -117,8 +87,13 @@ type value = | Bottom (** No value (uninitialized or moved value) *) | Borrow of borrow_content (** A borrowed value *) | Loan of loan_content (** A loaned value *) - | Symbolic of symbolic_proj_comp - (** Unknown (symbolic) value. This is a projector on borrows (TODO: make this clearer). *) + | Symbolic of symbolic_value + (** Borrow projector over a symbolic value. + + Note that contrary to the abstraction-values case, symbolic values + appearing in regular values are interpreted as *borrow* projectors, + they can never be *loan* projectors. + *) and adt_value = { variant_id : (VariantId.id option[@opaque]); |