diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimAstUtils.ml | 32 | ||||
| -rw-r--r-- | src/Interpreter.ml | 83 | ||||
| -rw-r--r-- | src/Pure.ml | 21 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 60 | ||||
| -rw-r--r-- | src/Translate.ml | 26 |
5 files changed, 147 insertions, 75 deletions
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml index 96410dde..430678f1 100644 --- a/src/CfimAstUtils.ml +++ b/src/CfimAstUtils.ml @@ -1,5 +1,6 @@ open CfimAst open Utils +module T = Types (** Check if a [statement] contains loops *) let statement_has_loops (st : statement) : bool = @@ -17,3 +18,34 @@ let statement_has_loops (st : statement) : bool = (** Check if a [fun_def] contains loops *) let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body + +(** 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 (sg : fun_sig) (gid : T.RegionGroupId.id) : + T.RegionGroupId.Set.t = + let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in + let parents = + List.fold_left + (fun s gid -> + (* Compute the parents *) + let parents = list_parent_region_groups sg 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 + +(** Small utility: same as [list_parent_region_groups], but returns an ordered list. *) +let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) + : T.RegionGroupId.id list = + let pset = list_parent_region_groups sg gid in + let parents = + List.filter + (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset) + sg.regions_hierarchy + in + let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in + parents diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 74e4e815..617f6211 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -5,6 +5,7 @@ module M = Modules module SA = SymbolicAst open Cps open InterpreterUtils +open InterpreterExpressions open InterpreterStatements (** The local logger *) @@ -97,6 +98,66 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : (* Return *) ctx +(** Evaluate a function with the symbolic interpreter *) +let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) + (m : M.cfim_module) (fid : A.FunDefId.id) + (back_id : T.RegionGroupId.id option) : unit = + (* Retrieve the function declaration *) + let fdef = A.FunDefId.nth m.functions fid in + + (* Debug *) + let name_to_string () = + Print.name_to_string fdef.A.name + ^ " (" + ^ Print.option_to_string T.RegionGroupId.to_string back_id + ^ ")" + in + log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ())); + + (* Create the evaluation context *) + let ctx = initialize_symbolic_context_for_fun m fdef in + + (* Create the continuation to finish the evaluation *) + let config = C.config_of_partial C.SymbolicMode config in + let cf_finish res ctx = + match res with + | Return -> + if synthesize then + (* There are two cases: + * - if this is a forward translation, we retrieve the returned value. + * - if this is a backward translation, we introduce "return" + * abstractions to consume the return value, then end all the + * abstractions up to the one in which we are interested. + *) + match back_id with + | None -> + (* Forward translation *) + (* Move the return value *) + let ret_vid = V.VarId.zero in + let cf_move = + eval_operand config (E.Move (mk_place_from_var_id ret_vid)) + in + (* Generate the Return node *) + let cf_return ret_value : m_fun = + fun _ -> Some (SA.Return ret_value) + in + (* Apply *) + cf_move cf_return ctx + | Some back_id -> + (* Backward translation *) raise Errors.Unimplemented + else None + | Panic -> + (* Note that as we explore all the execution branches, one of + * the executions can lead to a panic *) + if synthesize then Some SA.Panic else None + | _ -> + failwith ("evaluate_function_symbolic failed on: " ^ name_to_string ()) + in + + (* Evaluate the function *) + let _ = eval_function_body config fdef.A.body cf_finish ctx in + () + module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. @@ -163,26 +224,8 @@ module Test = struct log#ldebug (lazy ("test_function_symbolic: " ^ Print.name_to_string fdef.A.name)); - (* Create the evaluation context *) - let ctx = initialize_symbolic_context_for_fun m fdef in - - (* Create the continuation to check the function's result *) - let cf_check res _ = - match res with - | Return -> if synthesize then raise Errors.Unimplemented else None - | Panic -> - (* Note that as we explore all the execution branches, one of - * the executions can lead to a panic *) - if synthesize then Some SA.Panic else None - | _ -> - failwith - ("Unit test failed (symbolic execution) on: " - ^ Print.name_to_string fdef.A.name) - in - - (* Evaluate the function *) - let config = C.config_of_partial C.SymbolicMode config in - let _ = eval_function_body config fdef.A.body cf_check ctx in + (* Execute *) + let _ = evaluate_function_symbolic config synthesize m fid None in () (** Execute the symbolic interpreter on a list of functions. diff --git a/src/Pure.ml b/src/Pure.ml index 9a16264d..068a2127 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -134,7 +134,19 @@ type fun_id = | Unop of unop | Binop of E.binop * T.integer_type -type call = { func : fun_id; type_params : ty list; args : typed_rvalue list } +type call = { + func : fun_id; + type_params : ty list; + args : typed_rvalue list; + (** Note that at this point, some functions have no arguments. For instance: + ``` + fn f(); + ``` + + In the extracted code, we add a unit argument. This is unit argument is + added later, when going from the "pure" AST to the "extracted" AST. + *) +} type let_bindings = | Call of typed_lvalue list * call @@ -216,7 +228,12 @@ type inst_fun_sig = { inputs : ty list; outputs : ty list } type fun_def = { def_id : FunDefId.id; - name : name; + basename : name; + (** The "base" name of the function. + + The base name is the original name of the Rust function. We add suffixes + (to identify the forward/backward functions) later. + *) signature : fun_sig; body : expression; } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 46beb5c8..51d3c170 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1,4 +1,6 @@ open Errors +open Pure +open CfimAstUtils module Id = Identifiers module T = Types module V = Values @@ -8,7 +10,6 @@ module M = Modules module S = SymbolicAst module TA = TypesAnalysis module L = Logging -open Pure (** The local logger *) let log = L.symbolic_to_pure_log @@ -148,7 +149,7 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) : let outputs = List.map subst sg.outputs in { inputs; outputs } -type regular_fun_id = { fun_id : A.fun_id; back_id : T.RegionGroupId.id option } +type regular_fun_id = A.fun_id * T.RegionGroupId.id option [@@deriving show, ord] (** We use this type as a key for lookups *) @@ -189,7 +190,6 @@ type call_info = { type bs_ctx = { type_context : type_context; fun_context : fun_context; - fun_def : A.fun_def; bid : T.RegionGroupId.id option; sv_to_var : var V.SymbolicValueId.Map.t; (** Whenever we encounter a new symbolic value (introduced because of @@ -239,7 +239,6 @@ let fs_ctx_to_bs_ctx (fs_ctx : fs_ctx) : bs_ctx = let calls = V.FunCallId.Map.empty in let abstractions = V.AbstractionId.Map.empty in { - fun_def; bid; sv_to_var; var_counter; @@ -255,7 +254,7 @@ let get_instantiated_fun_sig (fun_id : A.fun_id) (back_id : T.RegionGroupId.id option) (tys : ty list) (ctx : bs_ctx) : inst_fun_sig = (* Lookup the non-instantiated function signature *) - let sg = RegularFunIdMap.find { fun_id; back_id } ctx.fun_context.fun_sigs in + let sg = RegularFunIdMap.find (fun_id, back_id) ctx.fun_context.fun_sigs in (* Create the substitution *) let tsubst = make_type_subst sg.type_params tys in (* Apply *) @@ -439,37 +438,6 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) let types_infos = ctx.type_context.types_infos in translate_back_ty types_infos keep_region inside_mut ty -(** 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 (sg : A.fun_sig) (gid : T.RegionGroupId.id) : - T.RegionGroupId.Set.t = - let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in - let parents = - List.fold_left - (fun s gid -> - (* Compute the parents *) - let parents = list_parent_region_groups sg 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 - -(** Small utility: same as [list_parent_region_groups], but returns an ordered list. *) -let list_ordered_parent_region_groups (sg : A.fun_sig) - (gid : T.RegionGroupId.id) : T.RegionGroupId.id list = - let pset = list_parent_region_groups sg gid in - let parents = - List.filter - (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset) - sg.regions_hierarchy - in - let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in - parents - let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) : V.AbstractionId.id list = (* We could do something more "elegant" without references, but it is @@ -1128,20 +1096,22 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) let otherwise = translate_expression otherwise ctx in Switch (scrutinee, SwitchInt (int_ty, branches, otherwise)) +(* TODO: move *) +let bs_ctx_lookup_local_function_sig (def_id : FunDefId.id) + (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig = + let id = (A.Local def_id, back_id) in + RegularFunIdMap.find id ctx.fun_context.fun_sigs + let translate_fun_def (fs_ctx : fs_ctx) (body : S.expression) : fun_def = let def = fs_ctx.fun_def in let bid = fs_ctx.bid in let bs_ctx = fs_ctx_to_bs_ctx fs_ctx in (* Translate the function *) let def_id = def.A.def_id in - let name = translate_fun_name def bid in - (* TODO: the signature should already have been translated. - * Do we need it actually? *) - let signature = - translate_fun_sig bs_ctx.type_context.types_infos def.signature bid - in + let basename = def.name in + let signature = bs_ctx_lookup_local_function_sig def_id bid bs_ctx in let body = translate_expression body bs_ctx in - { def_id; name; signature; body } + { def_id; basename; signature; body } let translate_type_defs (type_defs : T.type_def list) : type_def TypeDefId.Map.t = @@ -1161,13 +1131,13 @@ let translate_fun_signatures (types_infos : TA.type_infos) (regular_fun_id * fun_sig) list = (* The forward function *) let fwd_sg = translate_fun_sig types_infos sg None in - let fwd_id = { fun_id; back_id = None } in + let fwd_id = (fun_id, None) in (* The backward functions *) let back_sgs = List.map (fun (rg : T.region_var_group) -> let tsg = translate_fun_sig types_infos sg (Some rg.id) in - let id = { fun_id; back_id = Some rg.id } in + let id = (fun_id, Some rg.id) in (id, tsg)) sg.regions_hierarchy in diff --git a/src/Translate.ml b/src/Translate.ml index 8c6a6def..efdad619 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -3,6 +3,7 @@ module T = Types module A = CfimAst module M = Modules module SA = SymbolicAst +open Errors open Cps open InterpreterUtils open InterpreterStatements @@ -10,18 +11,21 @@ open InterpreterStatements (** The local logger *) let log = L.translate_log -(** Execute the symbolic interpreter on a function to generate a pure AST. - - We don't apply any micro pass. - *) -let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module) - (fid : A.FunDefId.id) : unit = +(** Execute the symbolic interpreter on a function to generate a symbolic AST. *) +let translate_function_to_symbolic (config : C.partial_config) + (m : M.cfim_module) (fid : A.FunDefId.id) + (back_id : T.RegionGroupId.id option) : unit = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in (* Debug *) log#ldebug - (lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name)); + (lazy + ("translate_function_to_pure: " + ^ Print.name_to_string fdef.A.name + ^ " (" + ^ Print.option_to_string T.RegionGroupId.to_string back_id + ^ ")")); (* Create the evaluation context *) let ctx = initialize_symbolic_context_for_fun m fdef in @@ -29,7 +33,7 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module) (* Create the continuation to check the function's result *) let cf_check res _ = match res with - | Return -> if synthesize then raise Errors.Unimplemented else None + | Return -> raise Errors.Unimplemented | Panic -> (* Note that as we explore all the execution branches, one of * the executions can lead to a panic *) @@ -44,3 +48,9 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module) let config = C.config_of_partial C.SymbolicMode config in let _ = eval_function_body config fdef.A.body cf_check ctx in () + +let translate (config : C.partial_config) (m : M.cfim_module) : unit = + (* Translate all the type definitions *) + + (* Translate all the function signatures *) + raise Unimplemented |