diff options
Diffstat (limited to '')
| -rw-r--r-- | src/PureMicroPasses.ml | 13 | ||||
| -rw-r--r-- | src/PureUtils.ml | 90 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 109 | ||||
| -rw-r--r-- | src/Translate.ml | 3 |
4 files changed, 104 insertions, 111 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index efe26bc4..b3e65055 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -2,6 +2,7 @@ open Errors open Pure +open PureUtils open TranslateCore (** The local logger *) @@ -299,7 +300,7 @@ let to_monadic (def : fun_def) : fun_def = method! visit_call env call = (* If no arguments, introduce unit *) if call.args = [] then - let args = [ Value (SymbolicToPure.unit_rvalue, None) ] in + let args = [ Value (unit_rvalue, None) ] in { call with args } (* Otherwise: nothing to do *) else super#visit_call env call end @@ -311,12 +312,10 @@ let to_monadic (def : fun_def) : fun_def = let def = if def.inputs = [] then ( assert (def.signature.inputs = []); - let signature = - { def.signature with inputs = [ SymbolicToPure.unit_ty ] } - in + let signature = { def.signature with inputs = [ unit_ty ] } in let var_cnt = get_expression_min_var_counter def.body in let id, _ = VarId.fresh var_cnt in - let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in + let var = { id; basename = None; ty = unit_ty } in let inputs = [ var ] in { def with signature; inputs }) else def @@ -326,10 +325,10 @@ let to_monadic (def : fun_def) : fun_def = match (def.back_id, def.signature.outputs) with | None, [ out_ty ] -> (* Forward function: there is always exactly one output *) - SymbolicToPure.mk_result_ty out_ty + mk_result_ty out_ty | Some _, outputs -> (* Backward function: we have to group them *) - SymbolicToPure.mk_result_ty (SymbolicToPure.mk_tuple_ty outputs) + mk_result_ty (mk_tuple_ty outputs) | _ -> failwith "Unreachable" in let outputs = [ output_ty ] in diff --git a/src/PureUtils.ml b/src/PureUtils.ml new file mode 100644 index 00000000..e5ce94a0 --- /dev/null +++ b/src/PureUtils.ml @@ -0,0 +1,90 @@ +open Identifiers +open Pure + +(* TODO : move *) +let binop_can_fail (binop : E.binop) : bool = + match binop with + | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false + | Div | Rem | Add | Sub | Mul -> true + | Shl | Shr -> raise Errors.Unimplemented + +let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } + +let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys) + +let unit_ty : ty = Adt (Tuple, []) + +let unit_rvalue : typed_rvalue = + let value = RvAdt { variant_id = None; field_values = [] } in + let ty = unit_ty in + { value; ty } + +let mk_typed_rvalue_from_var (v : var) : typed_rvalue = + let value = RvPlace (mk_place_from_var v) in + let ty = v.ty in + { value; ty } + +let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = + let value = LvVar (Var (v, mp)) in + let ty = v.ty in + { value; ty } + +let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue = + let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in + let ty = Adt (Tuple, tys) in + let value = LvAdt { variant_id = None; field_values = vl } in + { value; ty } + +let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id) + (vl : typed_lvalue list) : typed_lvalue = + let value = LvAdt { variant_id = Some variant_id; field_values = vl } in + { value; ty = adt_ty } + +let ty_as_integer (t : ty) : T.integer_type = + match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable" + +(* TODO: move *) +let type_def_is_enum (def : T.type_def) : bool = + match def.kind with T.Struct _ -> false | Enum _ -> true + +let mk_result_fail_rvalue (ty : ty) : typed_rvalue = + let ty = Adt (Assumed Result, [ ty ]) in + let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in + { value; ty } + +let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue = + let ty = Adt (Assumed Result, [ v.ty ]) in + let value = + RvAdt { variant_id = Some result_return_id; field_values = [ v ] } + in + { value; ty } + +let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) + +(** Type substitution *) +let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty = + let obj = + object + inherit [_] map_ty + + method! visit_TypeVar _ var_id = tsubst var_id + end + in + obj#visit_ty () ty + +let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty + = + let ls = List.combine vars tys in + let mp = + List.fold_left + (fun mp (k, v) -> TypeVarId.Map.add (k : type_var).index v mp) + TypeVarId.Map.empty ls + in + fun id -> TypeVarId.Map.find id mp + +let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) : + inst_fun_sig = + let subst = ty_substitute tsubst in + let inputs = List.map subst sg.inputs in + let outputs = List.map subst sg.outputs in + { inputs; outputs } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 345555e7..d7bcadb4 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1,11 +1,8 @@ open Errors -open Pure open CfimAstUtils +open Pure +open PureUtils module Id = Identifiers -module T = Types -module V = Values -module E = Expressions -module A = CfimAst module M = Modules module S = SymbolicAst module TA = TypesAnalysis @@ -15,96 +12,6 @@ module PP = PrintPure (** The local logger *) let log = L.symbolic_to_pure_log -(* TODO : move *) -let binop_can_fail (binop : E.binop) : bool = - match binop with - | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false - | Div | Rem | Add | Sub | Mul -> true - | Shl | Shr -> raise Unimplemented - -(* TODO: move *) -let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } - -let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys) - -let unit_ty : ty = Adt (Tuple, []) - -let unit_rvalue : typed_rvalue = - let value = RvAdt { variant_id = None; field_values = [] } in - let ty = unit_ty in - { value; ty } - -let mk_typed_rvalue_from_var (v : var) : typed_rvalue = - let value = RvPlace (mk_place_from_var v) in - let ty = v.ty in - { value; ty } - -(* TODO: move *) -let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = - let value = LvVar (Var (v, mp)) in - let ty = v.ty in - { value; ty } - -let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue = - let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in - let ty = Adt (Tuple, tys) in - let value = LvAdt { variant_id = None; field_values = vl } in - { value; ty } - -let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id) - (vl : typed_lvalue list) : typed_lvalue = - let value = LvAdt { variant_id = Some variant_id; field_values = vl } in - { value; ty = adt_ty } - -let ty_as_integer (t : ty) : T.integer_type = - match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable" - -(* TODO: move *) -let type_def_is_enum (def : T.type_def) : bool = - match def.kind with T.Struct _ -> false | Enum _ -> true - -let mk_result_fail_rvalue (ty : ty) : typed_rvalue = - let ty = Adt (Assumed Result, [ ty ]) in - let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in - { value; ty } - -let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue = - let ty = Adt (Assumed Result, [ v.ty ]) in - let value = - RvAdt { variant_id = Some result_return_id; field_values = [ v ] } - in - { value; ty } - -let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) - -(** Type substitution *) -let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty = - let obj = - object - inherit [_] map_ty - - method! visit_TypeVar _ var_id = tsubst var_id - end - in - obj#visit_ty () ty - -let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty - = - let ls = List.combine vars tys in - let mp = - List.fold_left - (fun mp (k, v) -> TypeVarId.Map.add (k : type_var).index v mp) - TypeVarId.Map.empty ls - in - fun id -> TypeVarId.Map.find id mp - -let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) : - inst_fun_sig = - let subst = ty_substitute tsubst in - let inputs = List.map subst sg.inputs in - let outputs = List.map subst sg.outputs in - { inputs; outputs } - type regular_fun_id = A.fun_id * T.RegionGroupId.id option [@@deriving show, ord] (** We use this type as a key for lookups *) @@ -183,13 +90,16 @@ type bs_ctx = { (** Body synthesis context *) (* TODO: move *) +let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter = + Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs + ctx.fun_context.cfim_fun_defs ctx.fun_def + let type_def_to_string (ctx : bs_ctx) (def : type_def) : string = let type_params = def.type_params in let type_defs = ctx.type_context.cfim_type_defs in let fmt = PrintPure.mk_type_formatter type_defs type_params in PrintPure.type_def_to_string fmt def -(* TODO: move *) let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string = let type_params = ctx.fun_def.signature.type_params in let type_defs = ctx.type_context.cfim_type_defs in @@ -197,7 +107,6 @@ let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string = let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in PrintPure.typed_rvalue_to_string fmt v -(* TODO: move *) let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_params = sg.type_params in let type_defs = ctx.type_context.cfim_type_defs in @@ -205,7 +114,6 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in PrintPure.fun_sig_to_string fmt sg -(* TODO: move *) let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string = let type_params = def.signature.type_params in let type_defs = ctx.type_context.cfim_type_defs in @@ -214,11 +122,6 @@ let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string = PrintPure.fun_def_to_string fmt def (* TODO: move *) -let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter = - Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs - ctx.fun_context.cfim_fun_defs ctx.fun_def - -(* TODO: move *) let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let fmt = bs_ctx_to_value_formatter ctx in let fmt = Print.CfimAst.ast_to_value_formatter fmt in diff --git a/src/Translate.ml b/src/Translate.ml index 63b6027e..005ace94 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -6,6 +6,7 @@ module A = CfimAst module M = Modules module SA = SymbolicAst module Micro = PureMicroPasses +open PureUtils open TranslateCore (** The local logger *) @@ -175,7 +176,7 @@ let translate_function_to_pure (config : C.partial_config) let backward_output_tys = List.map (fun (v : Pure.var) -> v.ty) backward_outputs in - let backward_ret_ty = SymbolicToPure.mk_tuple_ty backward_output_tys in + let backward_ret_ty = mk_tuple_ty backward_output_tys in let backward_inputs = T.RegionGroupId.Map.singleton back_id backward_inputs in |