summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/SymbolicToPure.ml')
-rw-r--r--src/SymbolicToPure.ml260
1 files changed, 225 insertions, 35 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 19fa85b3..69c22b09 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -6,8 +6,10 @@ module E = Expressions
module A = CfimAst
module M = Modules
module S = SymbolicAst
+module TA = TypesAnalysis
open Pure
+(** TODO: move this, it is not useful for symbolic -> pure *)
type name =
| FunName of A.FunDefId.id * V.BackwardFunctionId.id option
| TypeName of T.TypeDefId.id
@@ -38,8 +40,8 @@ module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType)
generation with collision in mind, it is always good to have such checks.
*)
-let fun_to_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) :
- Id.name =
+let translate_fun_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option)
+ : Id.name =
let sg = fdef.signature in
(* General function to generate a suffix for a region group
* (i.e., an abstraction)*)
@@ -93,22 +95,26 @@ let fun_to_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) :
add_to_last fdef.name
(** Generates a name for a type (simply reuses the name in the definition) *)
-let type_to_name (def : T.type_def) : Id.name = def.T.name
+let translate_type_name (def : T.type_def) : Id.name = def.T.name
type type_context = { type_defs : type_def TypeDefId.Map.t }
-type fun_context = unit
-(** TODO *)
+type fun_context = { fun_defs : fun_def FunDefId.Map.t }
+(* TODO: do we really need that actually? *)
type synth_ctx = {
names : NameMap.t;
+ (* TODO: remove? *)
type_context : type_context;
fun_context : fun_context;
declarations : M.declaration_group list;
}
-let rec translate_sty (ctx : synth_ctx) (ty : T.sty) : ty =
- let translate = translate_sty ctx in
+type bs_ctx = { types_infos : TA.type_infos }
+(** Body synthesis context *)
+
+let rec translate_sty (ty : T.sty) : ty =
+ let translate = translate_sty in
match ty with
| T.Adt (type_id, regions, tys) ->
(* Can't translate types with regions for now *)
@@ -125,52 +131,236 @@ let rec translate_sty (ctx : synth_ctx) (ty : T.sty) : ty =
| Slice ty -> Slice (translate ty)
| Ref (_, rty, _) -> translate rty
-let translate_field (ctx : synth_ctx) (f : T.field) : field =
+let translate_field (f : T.field) : field =
let field_name = f.field_name in
- let field_ty = translate_sty ctx f.field_ty in
+ let field_ty = translate_sty f.field_ty in
{ field_name; field_ty }
-let translate_fields (ctx : synth_ctx) (fl : T.field list) : field list =
- List.map (translate_field ctx) fl
+let translate_fields (fl : T.field list) : field list =
+ List.map translate_field fl
-let translate_variant (ctx : synth_ctx) (v : T.variant) : variant =
+let translate_variant (v : T.variant) : variant =
let variant_name = v.variant_name in
- let fields = translate_fields ctx v.fields in
+ let fields = translate_fields v.fields in
{ variant_name; fields }
-let translate_variants (ctx : synth_ctx) (vl : T.variant list) : variant list =
- List.map (translate_variant ctx) vl
+let translate_variants (vl : T.variant list) : variant list =
+ List.map translate_variant vl
(** Translate a type def kind to IM *)
-let translate_type_def_kind (ctx : synth_ctx) (kind : T.type_def_kind) :
- type_def_kind =
+let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind =
match kind with
- | T.Struct fields -> Struct (translate_fields ctx fields)
- | T.Enum variants -> Enum (translate_variants ctx variants)
+ | T.Struct fields -> Struct (translate_fields fields)
+ | T.Enum variants -> Enum (translate_variants variants)
(** Translate a type definition from IM
TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
point of moving this definition for now.
*)
-let translate_type_def (ctx : synth_ctx) (def : T.type_def) :
- synth_ctx * type_def =
+let translate_type_def (def : T.type_def) : type_def =
(* Translate *)
let def_id = def.T.def_id in
- let name = type_to_name def in
+ let name = translate_type_name def in
(* Can't translate types with regions for now *)
assert (def.region_params = []);
let type_params = def.type_params in
- let kind = translate_type_def_kind ctx def.T.kind in
- let def = { def_id; name; type_params; kind } in
- (* Insert in the context *)
- (* type context *)
- let type_context = ctx.type_context in
- let type_defs = type_context.type_defs in
- let type_defs = TypeDefId.Map.add def_id def type_defs in
- let type_context = { type_defs } in
- (* names map *)
- let names = NameMap.add (TypeName def_id) name ctx.names in
- (* update the fields *)
- let ctx = { ctx with type_context; names } in
- (ctx, def)
+ let kind = translate_type_def_kind def.T.kind in
+ { def_id; name; type_params; kind }
+
+(** Translate a type, seen as an input/output of a forward function
+ (preserve all borrows, etc.)
+*)
+
+let rec translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty =
+ let translate = translate_fwd_ty ctx in
+ match ty with
+ | T.Adt (type_id, regions, tys) ->
+ (* Can't translate types with regions for now *)
+ assert (regions = []);
+ (* No general parametricity for now *)
+ assert (not (List.exists (TypesUtils.ty_has_borrows ctx.types_infos) tys));
+ (* Translate the type parameters *)
+ let tys = List.map translate tys in
+ Adt (type_id, tys)
+ | TypeVar vid -> TypeVar vid
+ | Bool -> Bool
+ | Char -> Char
+ | Never -> failwith "Unreachable"
+ | Integer int_ty -> Integer int_ty
+ | Str -> Str
+ | Array ty ->
+ assert (not (TypesUtils.ty_has_borrows ctx.types_infos ty));
+ Array (translate ty)
+ | Slice ty ->
+ assert (not (TypesUtils.ty_has_borrows ctx.types_infos ty));
+ Slice (translate ty)
+ | Ref (_, rty, _) -> translate rty
+
+(** Translate a type, when some regions may have ended.
+
+ We return an option, because the translated type may be empty.
+
+ [inside_mut]: are we inside a mutable borrow?
+ *)
+let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
+ (inside_mut : bool) (ty : 'r T.ty) : ty option =
+ let translate = translate_back_ty ctx keep_region inside_mut in
+ (* A small helper for "leave" types *)
+ let wrap ty = if inside_mut then Some ty else None in
+ match ty with
+ | T.Adt (type_id, regions, tys) -> (
+ match type_id with
+ | T.AdtId _ | Assumed _ ->
+ (* Don't accept ADTs (which are not tuples) with borrows for now *)
+ assert (not (TypesUtils.ty_has_borrows ctx.types_infos ty));
+ None
+ | T.Tuple -> (
+ (* Tuples can contain borrows (which we eliminated) *)
+ let tys_t = List.filter_map translate tys in
+ match tys_t with [] -> None | _ -> Some (Adt (T.Tuple, tys_t))))
+ | TypeVar vid -> wrap (TypeVar vid)
+ | Bool -> wrap Bool
+ | Char -> wrap Char
+ | Never -> failwith "Unreachable"
+ | Integer int_ty -> wrap (Integer int_ty)
+ | Str -> wrap Str
+ | Array ty -> (
+ assert (not (TypesUtils.ty_has_borrows ctx.types_infos ty));
+ match translate ty with None -> None | Some ty -> Some (Array ty))
+ | Slice ty -> (
+ assert (not (TypesUtils.ty_has_borrows ctx.types_infos ty));
+ match translate ty with None -> None | Some ty -> Some (Slice ty))
+ | Ref (r, rty, rkind) -> (
+ match rkind with
+ | T.Shared ->
+ (* Ignore shared references, unless we are below a mutable borrow *)
+ if inside_mut then translate rty else None
+ | T.Mut ->
+ (* Dive in, remembering the fact that we are inside a mutable borrow *)
+ let inside_mut = true in
+ if keep_region r then translate_back_ty ctx keep_region inside_mut rty
+ else None)
+
+(** Small utility: list the transitive parents of a region var group.
+ We don't do that in an efficient manner, but it doesn't matter.
+ *)
+let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) :
+ T.RegionGroupId.Set.t =
+ let rg = T.RegionGroupId.nth def.signature.regions_hierarchy gid in
+ let parents =
+ List.fold_left
+ (fun s gid ->
+ (* Compute the parents *)
+ let parents = list_parent_region_groups def gid in
+ (* Parents U current region *)
+ let parents = T.RegionGroupId.Set.add gid parents in
+ (* Make the union with the accumulator *)
+ T.RegionGroupId.Set.union s parents)
+ T.RegionGroupId.Set.empty rg.parents
+ in
+ parents
+
+let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def)
+ (bid : V.BackwardFunctionId.id option) : fun_sig =
+ let sg = def.signature in
+ (* Retrieve the list of parent backward functions *)
+ let gid, parents =
+ match bid with
+ | None -> (None, T.RegionGroupId.Set.empty)
+ | Some bid ->
+ let gid = T.RegionGroupId.of_int (V.BackwardFunctionId.to_int bid) in
+ let parents = list_parent_region_groups def gid in
+ (Some gid, parents)
+ in
+ (* List the inputs for:
+ * - the forward function
+ * - the parent backward functions, in proper order
+ * - the current backward function (if it is a backward function)
+ *)
+ let fwd_inputs = List.map (translate_fwd_ty ctx) sg.inputs in
+ (* For the backward functions: for now we don't supported nested borrows,
+ * so just check that there aren't parent regions *)
+ assert (T.RegionGroupId.Set.is_empty parents);
+ (* Small helper to translate types for backward functions *)
+ let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.sty -> ty option
+ =
+ let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
+ let regions = T.RegionVarId.Set.of_list rg.regions in
+ let keep_region r =
+ match r with
+ | T.Static -> raise Unimplemented
+ | T.Var r -> T.RegionVarId.Set.mem r regions
+ in
+ let inside_mut = false in
+ translate_back_ty ctx keep_region inside_mut
+ in
+ (* Compute the additinal inputs for the current function, if it is a backward
+ * function *)
+ let back_inputs =
+ match gid with
+ | None -> []
+ | Some gid ->
+ (* For now, we don't allow nested borrows, so the additional inputs to the
+ * backward function can only come from borrows that were returned like
+ * in (for the backward function we introduce for 'a):
+ * ```
+ * fn f<'a>(...) -> &'a mut u32;
+ * ```
+ * Upon ending the abstraction for 'a, we need to get back the borrow
+ * the function returned.
+ *)
+ List.filter_map (translate_back_ty_for_gid gid) [ sg.output ]
+ in
+ let inputs = List.append fwd_inputs back_inputs in
+ (* Outputs *)
+ let outputs : ty list =
+ match gid with
+ | None ->
+ (* This is a forward function: there is one output *)
+ [ translate_fwd_ty ctx sg.output ]
+ | Some gid ->
+ (* This is a backward function: there might be several outputs.
+ * The outputs are the borrows inside the regions of the abstractions
+ * and which are present in the input values. For instance, see:
+ * ```
+ * fn f<'a>(x : 'a mut u32) -> ...;
+ * ```
+ * Upon ending the abstraction for 'a, we give back the borrow which
+ * was consumed through the `x` parameter.
+ *)
+ List.filter_map (translate_back_ty_for_gid gid) sg.inputs
+ in
+ (* Type parameters *)
+ let type_params = sg.type_params in
+ (* Return *)
+ { type_params; inputs; outputs }
+
+let translate_typed_value (v : V.typed_value) (ctx : bs_ctx) :
+ bs_ctx * typed_value =
+ raise Unimplemented
+
+let rec translate_expression (def : A.fun_def)
+ (bid : V.BackwardFunctionId.id option) (body : S.expression) (ctx : bs_ctx)
+ : expression =
+ match body with
+ | S.Return v ->
+ let _, v = translate_typed_value v ctx in
+ Return (Value v)
+ | Panic -> Panic
+ | FunCall (call, e) -> raise Unimplemented
+ | EndAbstraction (abs, e) -> raise Unimplemented
+ | Expansion (sv, exp) -> raise Unimplemented
+ | Meta (_, e) ->
+ (* We ignore the meta information *)
+ translate_expression def bid e ctx
+
+let translate_fun_def (types_infos : TA.type_infos) (def : A.fun_def)
+ (bid : V.BackwardFunctionId.id option) (body : S.expression) : fun_def =
+ let bs_ctx = { types_infos } in
+ (* Translate the function *)
+ let def_id = def.A.def_id in
+ let name = translate_fun_name def bid in
+ let signature = translate_fun_sig bs_ctx def bid in
+ let body = translate_expression def bid body bs_ctx in
+ { def_id; name; signature; body }
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 07:39:19 +0000