diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Contexts.ml | 5 | ||||
| -rw-r--r-- | src/Interpreter.ml | 47 | ||||
| -rw-r--r-- | src/Print.ml | 111 | ||||
| -rw-r--r-- | src/Values.ml | 165 |
4 files changed, 184 insertions, 144 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 1fbe2c09..62e4d7b9 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -130,7 +130,10 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx = *) let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx = - assert (List.for_all (fun (var, value) -> var.var_ty = value.ty) vars); + assert ( + List.for_all + (fun (var, (value : typed_value)) -> var.var_ty = value.ty) + vars); let vars = List.map (fun (var, value) -> Var (var_to_binder var, value)) vars in diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d6367702..ad7bdba1 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -251,11 +251,11 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) else () (** Check the borrow id and control the diving *) - method! visit_SharedBorrow env bid = + method! visit_SharedBorrow _env bid = if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid)) else () (** Check the borrow id *) - method! visit_InactivatedMutBorrow env bid = + method! visit_InactivatedMutBorrow _env bid = if bid = l then raise (FoundBorrowContent (V.InactivatedMutBorrow bid)) else () (** Check the borrow id *) @@ -372,7 +372,7 @@ let unwrap_res_to_outer_or opt default = match opt with Some x -> Outer x | None -> default (** Return the first loan we find in a value *) -let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = +let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = let obj = object inherit [_] V.iter_typed_value @@ -387,7 +387,7 @@ let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = with FoundLoanContent lc -> Some lc (** Check if a value contains ⊥ *) -let rec bottom_in_value (v : V.typed_value) : bool = +let bottom_in_value (v : V.typed_value) : bool = let obj = object inherit [_] V.iter_typed_value @@ -1202,7 +1202,11 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list) Subst.type_def_get_instantiated_field_type def opt_variant_id types in (* Initialize the expanded value *) - let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in + let fields = + List.map + (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value)) + field_types + in let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in let ty = T.Adt (T.AdtId def_id, regions, types) in { V.value = av; V.ty } @@ -1211,7 +1215,9 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list) let compute_expanded_bottom_tuple_value (field_types : T.ety list) : V.typed_value = (* Generate the field values *) - let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in + let fields = + List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types + in let v = V.Adt { variant_id = None; field_values = fields } in let ty = T.Adt (T.Tuple, [], field_types) in { V.value = v; V.ty } @@ -1366,7 +1372,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) 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 = + let rec inspect_update (v : V.typed_value) : unit = match v.V.value with | V.Concrete _ -> () | V.Bottom -> () @@ -1463,7 +1469,7 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) We use exceptions to make it handy. *) - let rec inspect_update (end_loans : bool) v : unit = + let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit = match v.V.value with | V.Concrete _ -> () | V.Bottom -> @@ -1654,7 +1660,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : (* Move the value *) L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); assert (not (bottom_in_value v)); - let bottom = { V.value = Bottom; ty = v.ty } in + let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with | Error _ -> failwith "Unreachable" | Ok ctx -> (ctx, v)) @@ -1723,7 +1729,8 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop) | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq -> failwith "Unreachable" in - Ok { V.value = V.Concrete (Bool b); ty = T.Bool } + Ok + ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value) | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr -> ( (* The two operands must have the same type and the result is an integer *) @@ -1783,7 +1790,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : if bkind = E.Shared then V.SharedBorrow bid else V.InactivatedMutBorrow bid in - let rv = { V.value = V.Borrow bc; ty = rv_ty } in + let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Compute the value with which to replace the value at place p *) let nv = match v.V.value with @@ -1809,7 +1816,9 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let ctx, bid = C.fresh_borrow_id ctx in let rv_ty = T.Ref (T.Erased, v.ty, Mut) in - let rv = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in + let rv : V.typed_value = + { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } + in (* Compute the value with which to replace the value at place p *) let nv = { v with V.value = V.Loan (V.MutLoan bid) } in (* Update the value in the context *) @@ -1847,7 +1856,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : (* Match on the aggregate kind *) match aggregate_kind with | E.AggregatedTuple -> - let tys = List.map (fun v -> v.V.ty) values in + let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in let v = V.Adt { variant_id = None; field_values = values } in let ty = T.Adt (T.Tuple, [], tys) in Ok (ctx, { V.value = v; ty }) @@ -1859,9 +1868,13 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id types in - assert (expected_field_types = List.map (fun v -> v.V.ty) values); + assert ( + expected_field_types + = List.map (fun (v : V.typed_value) -> v.V.ty) values); (* Construct the value *) - let av = { V.variant_id = opt_variant_id; V.field_values = values } in + let av : V.adt_value = + { V.variant_id = opt_variant_id; V.field_values = values } + in let aty = T.Adt (T.AdtId def_id, regions, types) in Ok (ctx, { V.value = Adt av; ty = aty })) @@ -2242,7 +2255,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) (* Create and push the input variables *) let input_vars = - V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl + V.VarId.mapi_from1 + (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v)) + args_vl in let ctx = C.ctx_push_vars ctx input_vars in diff --git a/src/Print.ml b/src/Print.ml index f92102fe..359416c8 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -201,29 +201,22 @@ module Values = struct let regions = V.RegionId.set_to_string sp.rset_ended in "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")" - type ('r, 'sv, 'bc, 'lc) gen_value_formatter = { - r_to_string : 'r -> string; - sv_to_string : 'sv -> string; - bc_to_string : 'bc -> string; - lc_to_string : 'lc -> string; - } - (** Auxiliary record: we use it to factorize value formatting *) - - let rec g_typed_value_to_string (fmt : value_formatter) - (gfmt : ('r, 'sv, 'bc, 'lc) gen_value_formatter) - (v : ('r, 'sv, 'bc, 'lc) V.g_typed_value) : string = - let ty_fmt : 'r PT.type_formatter = - { - PT.r_to_string = gfmt.r_to_string; - PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; - } - in + 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 + ^ " : " + ^ PT.ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty + ^ " <: " + ^ PT.ty_to_string (value_to_rtype_formatter fmt) rty + + let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) : + string = + let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in match v.value with | Concrete cv -> constant_value_to_string cv | Adt av -> ( let field_values = - List.map (g_typed_value_to_string fmt gfmt) av.field_values + List.map (typed_value_to_string fmt) av.field_values in match v.ty with | T.Adt (T.Tuple, _, _) -> @@ -258,22 +251,10 @@ module Values = struct | _ -> failwith "Inconsistent value") | _ -> failwith "Inconsistent typed value") | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty - | Borrow bc -> gfmt.bc_to_string bc - | Loan lc -> gfmt.lc_to_string lc - | Symbolic s -> gfmt.sv_to_string s - - let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) : - string = - let gfmt = - { - r_to_string = PT.erased_region_to_string; - sv_to_string = - symbolic_proj_comp_to_string (value_to_rtype_formatter fmt); - bc_to_string = borrow_content_to_string fmt; - lc_to_string = loan_content_to_string fmt; - } - in - g_typed_value_to_string fmt gfmt v + | 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 and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) : string = @@ -294,14 +275,6 @@ module Values = struct "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")" | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋" - 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 - ^ " : " - ^ PT.ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty - ^ " <: " - ^ PT.ty_to_string (value_to_rtype_formatter fmt) rty - let rec abstract_shared_borrows_to_string (fmt : value_formatter) (abs : V.abstract_shared_borrows) : string = match abs with @@ -324,15 +297,49 @@ module Values = struct let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) : string = - let gfmt = - { - r_to_string = PT.region_to_string fmt.r_to_string; - sv_to_string = aproj_to_string fmt; - bc_to_string = aborrow_content_to_string fmt; - lc_to_string = aloan_content_to_string fmt; - } - in - g_typed_value_to_string fmt gfmt v + let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in + match v.value with + | AConcrete cv -> constant_value_to_string cv + | AAdt av -> ( + let field_values = + List.map (typed_avalue_to_string fmt) av.field_values + in + match v.ty with + | T.Adt (T.Tuple, _, _) -> + (* Tuple *) + "(" ^ String.concat ", " field_values ^ ")" + | T.Adt (T.AdtId def_id, _, _) -> + (* "Regular" ADT *) + let adt_ident = + match av.variant_id with + | Some vid -> fmt.adt_variant_to_string def_id vid + | None -> fmt.type_def_id_to_string def_id + in + if List.length field_values > 0 then + match fmt.adt_field_names def_id av.V.variant_id with + | None -> + let field_values = String.concat ", " field_values in + adt_ident ^ " (" ^ field_values ^ ")" + | Some field_names -> + let field_values = List.combine field_names field_values in + let field_values = + List.map + (fun (field, value) -> field ^ " = " ^ value ^ ";") + field_values + in + let field_values = String.concat " " field_values in + adt_ident ^ " { " ^ field_values ^ " }" + else adt_ident + | T.Adt (T.Assumed aty, _, _) -> ( + (* Assumed type *) + match (aty, field_values) with + | Box, [ bv ] -> "@Box(" ^ bv ^ ")" + | _ -> failwith "Inconsistent value") + | _ -> failwith "Inconsistent typed value") + | ABottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty + | ABorrow bc -> aborrow_content_to_string fmt bc + | ALoan lc -> aloan_content_to_string fmt lc + | ASymbolic s -> aproj_to_string fmt s and aloan_content_to_string (fmt : value_formatter) (lc : V.aloan_content) : string = diff --git a/src/Values.ml b/src/Values.ml index 633b2157..764612af 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -63,79 +63,54 @@ type symbolic_proj_comp = { "Complementary" stands for the fact that it is a projector over all the regions *but* the ones which are listed in the projector. - *) +*) -(** Polymorphic iter visitor *) -class ['self] iter_'r_ty_base = +(** Ancestor for iter visitor for [typed_value] *) +class ['self] iter_typed_value_base = object (self : 'self) - method visit_ty : 'env 'r. ('env -> 'r -> unit) -> 'env -> 'r ty -> unit = - fun _visit_'r _env _ty -> () - end + inherit [_] VisitorsRuntime.iter -(** A generic, untyped value, used in the environments. + method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> () - Parameterized by: - - 'ty: type - - 'sv: symbolic value - - 'bc: borrow content - - 'lc: loan content + method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> () - Can be specialized for "regular" values or values in abstractions. + method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit = + fun _ _ -> () - TODO: unfactorize value and avalue. Making them instanciations of `g_value` - creates more problems than solutions, in particular when dealing with - visitors (which we can't automatically generate). -*) -type ('r, 'sv, 'bc, 'lc) g_value = - | Concrete of (constant_value[@opaque]) (** Concrete (non-symbolic) value *) - | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value - (** Enumerations, structures, tuples, assumed types. Note that units - are encoded as 0-tuples *) - | Bottom (** No value (uninitialized or moved value) *) - | Borrow of 'bc (** A borrowed value *) - | Loan of 'lc (** A loaned value *) - | Symbolic of 'sv (** Unknown value *) - -and ('r, 'sv, 'bc, 'lc) g_adt_value = { - variant_id : VariantId.id option; [@opaque] - field_values : ('r, 'sv, 'bc, 'lc) g_typed_value list; -} + method visit_ety : 'env -> ety -> unit = fun _ _ -> () + end -(** "Generic" ADT value (not "GADT" value) *) +(** Ancestor for map visitor for [typed_value] *) +class ['self] map_typed_value_base = + object (self : 'self) + inherit [_] VisitorsRuntime.map -and ('r, 'sv, 'bc, 'lc) g_typed_value = { - value : ('r, 'sv, 'bc, 'lc) g_value; - ty : 'r ty; -} -[@@deriving - show, - visitors - { - name = "iter_g_typed_value"; - variety = "iter"; - ancestors = [ "iter_'r_ty_base" ]; - polymorphic = true; - (* Heirs expect a polymorphic class *) - concrete = true; - }] + method visit_constant_value : 'env -> constant_value -> constant_value = + fun _ cv -> cv -class ['self] iter_typed_value_base = - object (self : 'self) - inherit [_] iter_g_typed_value + method visit_erased_region : 'env -> erased_region -> erased_region = + fun _ r -> r - method visit_erased_region : 'env. 'env -> erased_region -> unit = - fun _env _ -> () + method visit_symbolic_proj_comp + : 'env -> symbolic_proj_comp -> symbolic_proj_comp = + fun _ sv -> sv - method visit_symbolic_proj_comp : 'env. 'env -> symbolic_proj_comp -> unit = - fun _env _ -> () + method visit_ety : 'env -> ety -> ety = fun _ ty -> ty end +(** An untyped value, used in the environments *) type value = - (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value -(** "Regular" value *) + | Concrete of constant_value (** Concrete (non-symbolic) value *) + | Adt of adt_value (** Enumerations and structures *) + | 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 *) -and adt_value = - (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value +and adt_value = { + variant_id : (VariantId.id option[@opaque]); + field_values : typed_value list; +} and borrow_content = | SharedBorrow of (BorrowId.id[@opaque]) (** A shared value *) @@ -157,12 +132,7 @@ and loan_content = | SharedLoan of (BorrowId.set_t[@opaque]) * typed_value | MutLoan of (BorrowId.id[@opaque]) -and typed_value = - ( erased_region, - symbolic_proj_comp, - borrow_content, - loan_content ) - g_typed_value +and typed_value = { value : value; ty : ety } [@@deriving show, visitors @@ -172,6 +142,14 @@ and typed_value = ancestors = [ "iter_typed_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; + }, + visitors + { + name = "map_typed_value"; + variety = "map"; + ancestors = [ "map_typed_value_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; }] (** "Regular" typed value (we map variables to typed values) *) @@ -189,24 +167,46 @@ type aproj = type region = RegionVarId.id Types.region [@@deriving show] +(** Ancestor for iter visitor for [typed_avalue] *) class ['self] iter_typed_avalue_base = object (self : 'self) - inherit [_] iter_g_typed_value + inherit [_] iter_typed_value + + method visit_region : 'env -> region -> unit = fun _ _ -> () + + method visit_aproj : 'env -> aproj -> unit = fun _ _ -> () + + method visit_abstract_shared_borrows + : 'env -> abstract_shared_borrows -> unit = + fun _ _ -> () - method visit_region : 'env. 'env -> region -> unit = fun _env _r -> () + method visit_rty : 'env -> rty -> unit = fun _ _ -> () + end + +(** Ancestor for MAP visitor for [typed_avalue] *) +class ['self] map_typed_avalue_base = + object (self : 'self) + inherit [_] map_typed_value - method visit_aproj : 'env. 'env -> aproj -> unit = fun env _ -> () + method visit_region : 'env -> region -> region = fun _ r -> r - method visit_typed_value : 'env. 'env -> typed_value -> unit = - fun _env _v -> () + method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p method visit_abstract_shared_borrows - : 'env. 'env -> abstract_shared_borrows -> unit = - fun _env _asb -> () + : 'env -> abstract_shared_borrows -> abstract_shared_borrows = + fun _ asb -> asb + + method visit_rty : 'env -> rty -> rty = fun _ ty -> ty end -type avalue = (region, aproj, aborrow_content, aloan_content) g_value -(** Abstraction values are used inside of abstractions to properly model +type avalue = + | AConcrete of constant_value + | AAdt of aadt_value + | 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: @@ -214,7 +214,10 @@ type avalue = (region, aproj, aborrow_content, aloan_content) g_value *) (* TODO: rename to adt_avalue? *) -and aadt_value = (region, aproj, aborrow_content, aloan_content) g_adt_value +and aadt_value = { + variant_id : (VariantId.id option[@opaque]); + field_values : typed_avalue list; +} and aloan_content = | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue @@ -234,7 +237,9 @@ and aborrow_content = | AIgnoredMutBorrow of typed_avalue | AIgnoredSharedBorrow of abstract_shared_borrows -and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value +(* TODO: we may want to merge this with typed_value - would prevent some issues + when accessing fields... *) +and typed_avalue = { value : avalue; ty : rty } [@@deriving show, visitors @@ -244,6 +249,14 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value ancestors = [ "iter_typed_avalue_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; + }, + visitors + { + name = "map_typed_avalue"; + variety = "map"; + ancestors = [ "map_typed_avalue_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; }] type abs = { @@ -263,6 +276,7 @@ type abs = { which are a special kind of value. *) +(* (** Polymorphic version of the map visitor for [g_typed_value]. The polymorphic visitor generated by the visitors macro caused some @@ -575,3 +589,4 @@ class ['self] map_typed_avalue = : 'env -> abstract_shared_borrows -> aloan_content = fun _env asb -> AIgnoredSharedLoan asb end + *) |