summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 16:17:53 +0100
committerSon Ho2022-01-04 16:17:53 +0100
commit0b02fbacbd2c619835c10436e0b3ea3b919bac67 (patch)
treee4ccf4efac2cdcf849d0a5307f099595b22f9a67 /src
parent401c2234078f2ad9f00eb748aaae14404e8c8b72 (diff)
Make more progress on symbolic expansion
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml316
1 files changed, 160 insertions, 156 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9c806e8f..c871d530 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -69,12 +69,18 @@ let mk_box_value (v : V.typed_value) : V.typed_value =
let box_v = V.Adt { variant_id = None; field_values = [ v ] } in
mk_typed_value box_ty box_v
-(** Create a fresh symbolic value (as a complementary projector) *)
+(** 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.typed_value =
+ (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
let ctx, sv_id = C.fresh_symbolic_value_id ctx in
let svalue = { V.sv_id; V.sv_ty = ty } 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
@@ -2681,6 +2687,139 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
| Error _ -> failwith "Unreachable"
| Ok ctx -> ctx
+(** Projector kind *)
+type proj_kind = LoanProj | BorrowProj
+
+(** Auxiliary function.
+ Apply a symbolic expansion to avalues in a context, targetting a specific
+ kind of projectors.
+
+ [proj_kind] controls whether we apply the expansion to projectors
+ on loans or projectors on borrows.
+
+ When dealing with reference expansion, it is necessary to first apply the
+ expansion on loan projectors, then on borrow projectors. The reason is
+ that reducing the borrow projectors might require to perform some reborrows,
+ in which case we need to lookup the corresponding loans in the context.
+
+ [allow_reborrows] controls whether we allow reborrows or not. It is useful
+ only if we target borrow projectors.
+*)
+let apply_symbolic_expansion_to_target_avalues (config : C.config)
+ (allow_reborrows : bool) (proj_kind : proj_kind)
+ (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+ (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Symbolic values contained in the expansion might contain already ended regions *)
+ let check_symbolic_no_ended = false in
+ (* Prepare reborrows registration *)
+ let fresh_reborrow, apply_registered_reborrows =
+ prepare_reborrows config allow_reborrows ctx
+ in
+ (* Visitor to apply the expansion *)
+ let obj =
+ object
+ inherit [_] C.map_eval_ctx as super
+
+ method! visit_abs proj_regions abs =
+ assert (Option.is_none proj_regions);
+ let proj_regions = Some abs.V.regions in
+ super#visit_abs proj_regions abs
+ (** When visiting an abstraction, we remember the regions it owns to be
+ able to properly reduce projectors when expanding symbolic values *)
+
+ method! visit_ASymbolic proj_regions aproj =
+ let proj_regions = Option.get proj_regions in
+ match (aproj, proj_kind) with
+ | V.AProjLoans sv, LoanProj ->
+ (* Check if this is the symbolic value we are looking for *)
+ if sv = original_sv then
+ (* Apply the projector *)
+ let projected_value =
+ apply_proj_loans_on_symbolic_expansion ctx proj_regions
+ expansion sv.V.sv_ty
+ in
+ (* Replace *)
+ projected_value.V.value
+ else
+ (* Not the searched symbolic value: nothing to do *)
+ super#visit_ASymbolic (Some proj_regions) aproj
+ | V.AProjBorrows (sv, proj_ty), BorrowProj ->
+ (* Check if this is the symbolic value we are looking for *)
+ if sv = original_sv then
+ (* Convert the symbolic expansion to a value on which we can
+ * apply a projector (if the expansion is a reference expansion,
+ * convert it to a borrow) *)
+ let expansion =
+ symbolic_expansion_to_value_with_borrows original_sv expansion
+ in
+ (* Apply the projector *)
+ let projected_value =
+ apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+ proj_regions expansion proj_ty
+ in
+ (* Replace *)
+ projected_value.V.value
+ else
+ (* Not the searched symbolic value: nothing to do *)
+ super#visit_ASymbolic (Some proj_regions) aproj
+ | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
+ (* Nothing to do *)
+ super#visit_ASymbolic (Some proj_regions) aproj
+ end
+ in
+ (* Apply the expansion *)
+ let ctx = obj#visit_eval_ctx None ctx in
+ (* Apply the reborrows *)
+ apply_registered_reborrows ctx
+
+(** Auxiliary function.
+ Apply a symbolic expansion to avalues in a context.
+*)
+let apply_symbolic_expansion_to_avalues (config : C.config)
+ (allow_reborrows : bool) (original_sv : V.symbolic_value)
+ (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
+ let apply_expansion proj_kind ctx =
+ apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+ original_sv expansion ctx
+ in
+ (* First target the loan projectors, then the borrow projectors *)
+ let ctx = apply_expansion LoanProj ctx in
+ let ctx = apply_expansion BorrowProj ctx in
+ ctx
+
+(** Apply a symbolic expansion to a context, by replacing the original
+ symbolic value with its expanded value. Is valid only if the expansion
+ is not a borrow (i.e., an adt...).
+*)
+let apply_symbolic_expansion_non_borrow (config : C.config)
+ (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+ (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Convert the expansion to a value *)
+ let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+ (* Visitor to apply the expansion to *non-abstraction* values *)
+ let obj =
+ object
+ inherit [_] C.map_eval_ctx as super
+
+ method! visit_Symbolic env spc =
+ if spc.V.svalue = original_sv then nv.V.value
+ else super#visit_Symbolic env spc
+ (** Replace a symbolic value with its expansion.
+ Note that there may be several references to the same symbolic value
+ in the context, if the value has been copied. Expansion is then a bit
+ subtle in the case we expand shared borrows, in which case we need to
+ introduce a unique borrow identifier for every borrow (this is not
+ the case here: this function should NOT be used to expand borrows).
+ *)
+ end
+ in
+ (* Apply the expansion to non-abstraction values *)
+ let ctx = obj#visit_eval_ctx None ctx in
+ (* Apply the expansion to abstraction values *)
+ let allow_reborrows = false in
+ apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+ expansion ctx
+
(** Compute an expanded ADT bottom value *)
let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
(def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
@@ -2795,7 +2934,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
(ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id)
(opt_variant_id : T.VariantId.id option)
(regions : T.RegionId.id T.region list) (types : T.rty list)
- (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) 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 = T.TypeDefId.nth ctx.type_context def_id in
@@ -2810,42 +2949,40 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
(* Initialize the expanded value for a given variant *)
let initialize (ctx : C.eval_ctx)
((variant_id, field_types) : T.VariantId.id option * T.rty list) :
- C.eval_ctx * V.typed_value =
+ 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)
ctx field_types
in
- let av = V.Adt { variant_id; field_values } in
- let ty = T.Adt (T.AdtId def_id, regions, types) in
- let ty = Subst.erase_regions ty in
- (ctx, { V.value = av; V.ty })
+ let see = SeAdt (variant_id, field_values) in
+ (ctx, see)
in
(* 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 * V.typed_value =
+ (field_types : T.rty list) (ctx : C.eval_ctx) :
+ C.eval_ctx * symbolic_expansion =
(* Generate the field values *)
- let ctx, fields =
+ let ctx, field_values =
List.fold_left_map
(fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx)
ctx field_types
in
- let v = V.Adt { variant_id = None; field_values = fields } in
- let field_types = List.map Subst.erase_regions field_types in
- let ty = T.Adt (T.Tuple, [], field_types) in
- (ctx, { V.value = v; V.ty })
+ 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 * V.typed_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 box_value = mk_box_value boxed_value in
- (ctx, box_value)
+ let see = SeAdt (None, [ boxed_value ]) in
+ (ctx, see)
let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
(region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
@@ -2862,139 +2999,6 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
raise Unimplemented
| T.Shared -> raise Unimplemented
-(** Projector kind *)
-type proj_kind = LoanProj | BorrowProj
-
-(** Auxiliary function.
- Apply a symbolic expansion to avalues in a context, targetting a specific
- kind of projectors.
-
- [proj_kind] controls whether we apply the expansion to projectors
- on loans or projectors on borrows.
-
- When dealing with reference expansion, it is necessary to first apply the
- expansion on loan projectors, then on borrow projectors. The reason is
- that reducing the borrow projectors might require to perform some reborrows,
- in which case we need to lookup the corresponding loans in the context.
-
- [allow_reborrows] controls whether we allow reborrows or not. It is useful
- only if we target borrow projectors.
-*)
-let apply_symbolic_expansion_to_target_avalues (config : C.config)
- (allow_reborrows : bool) (proj_kind : proj_kind)
- (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
- (ctx : C.eval_ctx) : C.eval_ctx =
- (* Symbolic values contained in the expansion might contain already ended regions *)
- let check_symbolic_no_ended = false in
- (* Prepare reborrows registration *)
- let fresh_reborrow, apply_registered_reborrows =
- prepare_reborrows config allow_reborrows ctx
- in
- (* Visitor to apply the expansion *)
- let obj =
- object
- inherit [_] C.map_eval_ctx as super
-
- method! visit_abs proj_regions abs =
- assert (Option.is_none proj_regions);
- let proj_regions = Some abs.V.regions in
- super#visit_abs proj_regions abs
- (** When visiting an abstraction, we remember the regions it owns to be
- able to properly reduce projectors when expanding symbolic values *)
-
- method! visit_ASymbolic proj_regions aproj =
- let proj_regions = Option.get proj_regions in
- match (aproj, proj_kind) with
- | V.AProjLoans sv, LoanProj ->
- (* Check if this is the symbolic value we are looking for *)
- if sv = original_sv then
- (* Apply the projector *)
- let projected_value =
- apply_proj_loans_on_symbolic_expansion ctx proj_regions
- expansion sv.V.sv_ty
- in
- (* Replace *)
- projected_value.V.value
- else
- (* Not the searched symbolic value: nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
- | V.AProjBorrows (sv, proj_ty), BorrowProj ->
- (* Check if this is the symbolic value we are looking for *)
- if sv = original_sv then
- (* Convert the symbolic expansion to a value on which we can
- * apply a projector (if the expansion is a reference expansion,
- * convert it to a borrow) *)
- let expansion =
- symbolic_expansion_to_value_with_borrows original_sv expansion
- in
- (* Apply the projector *)
- let projected_value =
- apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- proj_regions expansion proj_ty
- in
- (* Replace *)
- projected_value.V.value
- else
- (* Not the searched symbolic value: nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
- | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
- (* Nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
- end
- in
- (* Apply the expansion *)
- let ctx = obj#visit_eval_ctx None ctx in
- (* Apply the reborrows *)
- apply_registered_reborrows ctx
-
-(** Auxiliary function.
- Apply a symbolic expansion to avalues in a context.
-*)
-let apply_symbolic_expansion_to_avalues (config : C.config)
- (allow_reborrows : bool) (original_sv : V.symbolic_value)
- (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
- let apply_expansion proj_kind ctx =
- apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
- original_sv expansion ctx
- in
- (* First target the loan projectors, then the borrow projectors *)
- let ctx = apply_expansion LoanProj ctx in
- let ctx = apply_expansion BorrowProj ctx in
- ctx
-
-(** Apply a symbolic expansion to a context, by replacing the original
- symbolic value with its expanded value. Is valid only if the expansion
- is not a borrow (i.e., an adt...).
-*)
-let apply_symbolic_expansion_non_borrow (config : C.config)
- (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
- (ctx : C.eval_ctx) : C.eval_ctx =
- (* Convert the expansion to a value *)
- let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
- (* Visitor to apply the expansion to *non-abstraction* values *)
- let obj =
- object
- inherit [_] C.map_eval_ctx as super
-
- method! visit_Symbolic env spc =
- if spc.V.svalue = original_sv then nv.V.value
- else super#visit_Symbolic env spc
- (** Replace a symbolic value with its expansion.
- Note that there may be several references to the same symbolic value
- in the context, if the value has been copied. Expansion is then a bit
- subtle in the case we expand shared borrows, in which case we need to
- introduce a unique borrow identifier for every borrow (this is not
- the case here: this function should NOT be used to expand borrows).
- *)
- end
- in
- (* Apply the expansion to non-abstraction values *)
- let ctx = obj#visit_eval_ctx None ctx in
- (* Apply the expansion to abstraction values *)
- let allow_reborrows = false in
- apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
- expansion ctx
-
(** Expand a symbolic value which is not an enumeration with several variants.
This function is used when exploring a path.
@@ -3030,12 +3034,6 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
in
(* Apply in the context *)
apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
- (* Borrows *)
- | Deref, T.Ref (region, ref_ty, rkind) ->
- let _ =
- expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
- in
- raise Unimplemented
(* Boxes *)
| DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
let ctx, nv =
@@ -3043,6 +3041,12 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
in
(* Apply in the context *)
apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
+ (* Borrows *)
+ | Deref, T.Ref (region, ref_ty, rkind) ->
+ let _ =
+ expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
+ in
+ raise Unimplemented
| _ ->
failwith
("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)