summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CfimAst.ml4
-rw-r--r--src/CfimOfJson.ml10
-rw-r--r--src/Interpreter.ml15
-rw-r--r--src/Print.ml72
-rw-r--r--src/Substitute.ml4
-rw-r--r--src/Types.ml16
-rw-r--r--src/Values.ml2
7 files changed, 86 insertions, 37 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 64151a48..192638cf 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -28,8 +28,8 @@ type fun_sig = {
region_params : region_var list;
num_early_bound_regions : int;
type_params : type_var list;
- inputs : rty list;
- output : rty;
+ inputs : sty list;
+ output : sty;
}
[@@deriving show]
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 0a7eeb78..3494f004 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -124,8 +124,8 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
Ok (T.Ref (region, ty, ref_kind))
| _ -> Error "")
-let rty_of_json (js : json) : (T.rty, string) result =
- combine_error_msgs js "rty_of_json" (ty_of_json region_of_json js)
+let sty_of_json (js : json) : (T.sty, string) result =
+ combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js)
let ety_of_json (js : json) : (T.ety, string) result =
combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js)
@@ -135,7 +135,7 @@ let field_of_json (js : json) : (T.field, string) result =
(match js with
| `Assoc [ ("name", name); ("ty", ty) ] ->
let* name = string_of_json name in
- let* ty = rty_of_json ty in
+ let* ty = sty_of_json ty in
Ok { T.field_name = name; field_ty = ty }
| _ -> Error "")
@@ -450,8 +450,8 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
let* region_params = list_of_json region_var_of_json region_params in
let* num_early_bound_regions = int_of_json num_early_bound_regions in
let* type_params = list_of_json type_var_of_json type_params in
- let* inputs = list_of_json rty_of_json inputs in
- let* output = rty_of_json output in
+ let* inputs = list_of_json sty_of_json inputs in
+ let* output = sty_of_json output in
Ok
{
A.region_params;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 8b929b0f..9555b0ca 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -584,8 +584,12 @@ exception FoundOuter of outer_borrows_or_abs
Note that the two abstractions have different views (in terms of regions)
of the symbolic value (hence the two region types).
*)
-let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
- (rset2 : V.RegionId.set_t) : bool =
+let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
+ (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool =
+ 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
+ in
match (ty1, ty2) with
| T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
| T.Integer int_ty1, T.Integer int_ty2 ->
@@ -603,8 +607,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
let regions = List.combine regions1 regions2 in
let tys = List.combine tys1 tys2 in
List.exists
- (fun (r1, r2) ->
- V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2)
+ (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2)
regions
|| List.exists
(fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2)
@@ -616,7 +619,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
assert (kind1 = kind2);
(* The projections intersect if the borrows intersect or their contents
* intersect *)
- (V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2)
+ (region_in_set r1 rset1 && region_in_set r2 rset2)
|| projections_intersect ty1 rset1 ty2 rset2
| _ -> failwith "Unreachable"
@@ -628,7 +631,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
map borrows to regions - or to interpret the borrows as belonging
to some regions...)
*)
-let apply_proj_borrows (regions : V.RegionId.set_t) (v : V.typed_value)
+let apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
(ty : T.rty) : V.typed_avalue =
(* Sanity check - TODO: move this elsewhere (here we perform the check at every
* recursive call which is a bit overkill...) *)
diff --git a/src/Print.ml b/src/Print.ml
index e9ba4730..bf07e57e 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -16,6 +16,12 @@ module Types = struct
| Some name -> name
| None -> T.RegionVarId.to_string rv.index
+ let region_var_id_to_string (rid : T.RegionVarId.id) : string =
+ "rv@" ^ T.RegionVarId.to_string rid
+
+ let region_id_to_string (rid : T.RegionId.id) : string =
+ "r@" ^ T.RegionId.to_string rid
+
let region_to_string (rid_to_string : 'rid -> string) (r : 'rid T.region) :
string =
match r with Static -> "'static" | Var rid -> rid_to_string rid
@@ -33,9 +39,11 @@ module Types = struct
type_def_id_to_string : T.TypeDefId.id -> string;
}
- type etype_formatter = T.erased_region type_formatter
+ type stype_formatter = T.RegionVarId.id T.region type_formatter
- type rtype_formatter = T.RegionVarId.id T.region type_formatter
+ type rtype_formatter = T.RegionId.id T.region type_formatter
+
+ type etype_formatter = T.erased_region type_formatter
let integer_type_to_string = function
| T.Isize -> "isize"
@@ -87,9 +95,14 @@ module Types = struct
else if List.length regions + List.length types > 0 then "<" ^ params ^ ">"
else ""
- let rty_to_string fmt (ty : T.rty) : string = ty_to_string fmt ty
+ let sty_to_string (fmt : stype_formatter) (ty : T.sty) : string =
+ ty_to_string fmt ty
+
+ let rty_to_string (fmt : rtype_formatter) (ty : T.rty) : string =
+ ty_to_string fmt ty
- let ety_to_string fmt (ty : T.ety) : string = ty_to_string fmt ty
+ let ety_to_string (fmt : etype_formatter) (ty : T.ety) : string =
+ ty_to_string fmt ty
let field_to_string fmt (f : T.field) : string =
f.field_name ^ " : " ^ ty_to_string fmt f.field_ty
@@ -148,7 +161,8 @@ module PT = Types (* local module *)
(** Pretty-printing for values *)
module Values = struct
type value_formatter = {
- r_to_string : T.RegionVarId.id -> string;
+ rvar_to_string : T.RegionVarId.id -> string;
+ r_to_string : T.RegionId.id -> string;
type_var_id_to_string : T.TypeVarId.id -> string;
type_def_id_to_string : T.TypeDefId.id -> string;
adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
@@ -171,6 +185,13 @@ module Values = struct
PT.type_def_id_to_string = fmt.type_def_id_to_string;
}
+ let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
+ {
+ PT.r_to_string = PT.region_to_string fmt.rvar_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;
+ }
+
let var_id_to_string (id : V.VarId.id) : string =
"var@" ^ V.VarId.to_string id
@@ -191,14 +212,11 @@ module Values = struct
let symbolic_value_to_string (fmt : PT.rtype_formatter)
(sv : V.symbolic_value) : string =
- symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.ty_to_string fmt sv.sv_ty
-
- let region_id_to_string (rid : V.RegionId.id) : string =
- "r@" ^ V.RegionId.to_string rid
+ 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 = V.RegionId.set_to_string sp.rset_ended in
+ 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)
@@ -411,7 +429,7 @@ module Values = struct
^ "{parents="
^ V.AbstractionId.set_to_string abs.parents
^ "}" ^ "{regions="
- ^ V.RegionId.set_to_string abs.regions
+ ^ T.RegionId.set_to_string abs.regions
^ "}" ^ " {\n" ^ avs ^ "\n}"
end
@@ -465,8 +483,10 @@ module Contexts = struct
Some fields
let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
- (* We shouldn't use r_to_string *)
- let r_to_string _ = failwith "Unexpected use of r_to_string" in
+ (* We shouldn't use rvar_to_string *)
+ let rvar_to_string r = failwith "Unexpected use of rvar_to_string" in
+ let r_to_string r = PT.region_id_to_string r in
+
let type_var_id_to_string vid =
let v = C.lookup_type_var ctx vid in
v.name
@@ -484,6 +504,7 @@ module Contexts = struct
in
let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in
{
+ rvar_to_string;
r_to_string;
type_var_id_to_string;
type_def_id_to_string;
@@ -527,7 +548,8 @@ module PC = Contexts (* local module *)
(** Pretty-printing for contexts (generic functions) *)
module CfimAst = struct
type ast_formatter = {
- r_to_string : T.RegionVarId.id -> string;
+ rvar_to_string : T.RegionVarId.id -> string;
+ r_to_string : T.RegionId.id -> string;
type_var_id_to_string : T.TypeVarId.id -> string;
type_def_id_to_string : T.TypeDefId.id -> string;
adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
@@ -541,6 +563,7 @@ module CfimAst = struct
let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
{
+ PV.rvar_to_string = fmt.rvar_to_string;
PV.r_to_string = fmt.r_to_string;
PV.type_var_id_to_string = fmt.type_var_id_to_string;
PV.type_def_id_to_string = fmt.type_def_id_to_string;
@@ -563,6 +586,13 @@ module CfimAst = struct
PT.type_def_id_to_string = fmt.type_def_id_to_string;
}
+ let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter =
+ {
+ PT.r_to_string = PT.region_to_string fmt.rvar_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;
+ }
+
let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) :
T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
fun def_id opt_variant_id field_id ->
@@ -581,6 +611,7 @@ module CfimAst = struct
PT.name_to_string def.name
in
{
+ rvar_to_string = ctx_fmt.PV.rvar_to_string;
r_to_string = ctx_fmt.PV.r_to_string;
type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
type_def_id_to_string = ctx_fmt.PV.type_def_id_to_string;
@@ -790,6 +821,8 @@ module CfimAst = struct
(indent_incr : string) (def : A.fun_def) : string =
let rty_fmt = ast_to_rtype_formatter fmt in
let rty_to_string = PT.rty_to_string rty_fmt in
+ let sty_fmt = ast_to_stype_formatter fmt in
+ let sty_to_string = PT.sty_to_string sty_fmt in
let ety_fmt = ast_to_etype_formatter fmt in
let ety_to_string = PT.ety_to_string ety_fmt in
let sg = def.signature in
@@ -814,7 +847,7 @@ module CfimAst = struct
let args = List.combine inputs sg.inputs in
let args =
List.map
- (fun (var, rty) -> var_to_string var ^ " : " ^ rty_to_string rty)
+ (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty)
args
in
let args = String.concat ", " args in
@@ -822,7 +855,7 @@ module CfimAst = struct
(* Return type *)
let ret_ty = sg.output in
let ret_ty =
- if TU.ty_is_unit ret_ty then "" else " -> " ^ rty_to_string ret_ty
+ if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty
in
(* All the locals (with erased regions) *)
@@ -863,10 +896,14 @@ module Module = struct
with the variables local to a function's definition *)
let def_ctx_to_ast_formatter (type_context : T.type_def list)
(fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter =
- let r_to_string vid =
+ let rvar_to_string vid =
let var = T.RegionVarId.nth def.signature.region_params vid in
PT.region_var_to_string var
in
+ let r_to_string vid =
+ (* TODO: we might want something more informative *)
+ PT.region_id_to_string vid
+ in
let type_var_id_to_string vid =
let var = T.TypeVarId.nth def.signature.type_params vid in
PT.type_var_to_string var
@@ -891,6 +928,7 @@ module Module = struct
in
let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_context in
{
+ rvar_to_string;
r_to_string;
type_var_id_to_string;
type_def_id_to_string;
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 78109913..9adbf4a6 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -37,8 +37,8 @@ let erase_regions (ty : T.rty) : T.ety =
(** Erase the regions in a type and substitute the type variables *)
let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
- (ty : T.rty) : T.ety =
- let rsubst (_ : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
+ (ty : 'r T.region T.ty) : T.ety =
+ let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
ty_substitute rsubst tsubst ty
(** Create a type substitution from a list of type variable ids and a list of
diff --git a/src/Types.ml b/src/Types.ml
index 59a512eb..c9eeff7e 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -9,6 +9,10 @@ module VariantId = IdGen ()
module FieldId = IdGen ()
module RegionVarId = IdGen ()
+(** Region variable ids. Used in function signatures. *)
+
+module RegionId = IdGen ()
+(** Region ids. Used for symbolic executions. *)
type ('id, 'name) indexed_var = {
index : 'id; (** Unique index identifying the variable *)
@@ -79,19 +83,25 @@ type 'r ty =
[@@deriving show]
(* TODO: group Bool, Char, etc. in Constant *)
-type rty = RegionVarId.id region ty [@@deriving show]
-(** Type with *R*egions.
+type sty = RegionVarId.id region ty [@@deriving show]
+(** *S*ignature types.
Used in function signatures and type definitions.
*)
+type rty = RegionId.id region ty [@@deriving show]
+(** Type with *R*egions.
+
+ Used during symbolic execution.
+ *)
+
type ety = erased_region ty [@@deriving show]
(** Type with *E*rased regions.
Used in function bodies, "general" value types, etc.
*)
-type field = { field_name : string; field_ty : rty } [@@deriving show]
+type field = { field_name : string; field_ty : sty } [@@deriving show]
type variant = { variant_name : string; fields : field list } [@@deriving show]
diff --git a/src/Values.ml b/src/Values.ml
index 4b5b9b4e..96feb814 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -13,8 +13,6 @@ module SymbolicValueId = IdGen ()
module AbstractionId = IdGen ()
-module RegionId = IdGen ()
-
(** A variable *)
type big_int = Z.t
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 12:42:26 +0000