diff options
| -rw-r--r-- | src/Assumed.ml | 13 | ||||
| -rw-r--r-- | src/Interpreter.ml | 162 | ||||
| -rw-r--r-- | src/Logging.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 109 | ||||
| -rw-r--r-- | src/Translate.ml | 46 |
5 files changed, 224 insertions, 112 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index 2fc8dd61..c40387ea 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -1,4 +1,3 @@ -module T = Types (** This module contains various utilities for the assumed functions. Note that `Box::free` is peculiar: we don't really handle it as a function, @@ -8,6 +7,7 @@ module T = Types not as a function call, and thus never need its signature. *) +module T = Types module A = CfimAst open TypesUtils @@ -56,3 +56,14 @@ let box_deref_shared_sig = box_deref_sig false (** `&'a mut Box<T> -> &'a mut T` *) let box_deref_mut_sig = box_deref_sig true + +(** The list of assumed functions, and their signatures. + + Rk.: following what is written above, we don't include `Box::free`. + *) +let assumed_functions : (A.assumed_fun_id * A.fun_sig) list = + [ + (BoxNew, box_new_sig); + (BoxDeref, box_deref_shared_sig); + (BoxDerefMut, box_deref_mut_sig); + ] diff --git a/src/Interpreter.ml b/src/Interpreter.ml index cd7952e0..74e4e815 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,100 +10,94 @@ open InterpreterStatements (** The local logger *) let log = L.interpreter_log -module Test = struct - let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : - C.eval_ctx = - let type_decls, _ = M.split_declarations m.declarations in - let type_defs, fun_defs = M.compute_defs_maps m in - let type_defs_groups, _funs_defs_groups = - M.split_declarations_to_group_maps m.declarations - in - let type_infos = - TypesAnalysis.analyze_type_declarations type_defs type_decls - in - let type_context = { C.type_defs_groups; type_defs; type_infos } in - C.reset_global_counters (); - { - C.type_context; - C.fun_context = fun_defs; - C.type_vars; - C.env = []; - C.ended_regions = T.RegionId.Set.empty; - } - - (** Initialize an evaluation context to execute a function. +let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : + C.eval_ctx = + let type_decls, _ = M.split_declarations m.declarations in + let type_defs, fun_defs = M.compute_defs_maps m in + let type_defs_groups, _funs_defs_groups = + M.split_declarations_to_group_maps m.declarations + in + let type_infos = + TypesAnalysis.analyze_type_declarations type_defs type_decls + in + let type_context = { C.type_defs_groups; type_defs; type_infos } in + C.reset_global_counters (); + { + C.type_context; + C.fun_context = fun_defs; + C.type_vars; + C.env = []; + C.ended_regions = T.RegionId.Set.empty; + } + +(** Initialize an evaluation context to execute a function. Introduces local variables initialized in the following manner: - input arguments are initialized as symbolic values - the remaining locals are initialized as ⊥ Abstractions are introduced for the regions present in the function signature. - *) - let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) - : C.eval_ctx = - (* The abstractions are not initialized the same way as for function - * calls: they contain *loan* projectors, because they "provide" us - * with the input values (which behave as if they had been returned - * by some function calls...). - * Also, note that we properly set the set of parents of every abstraction: - * this should not be necessary, as those abstractions should never be - * *automatically* ended (because ending some borrows requires to end - * one of them), but rather selectively ended when generating code - * for each of the backward functions. We do it only because we can - * do it, and because it gives a bit of sanity. - * *) - let sg = fdef.signature in - (* Create the context *) - let ctx = initialize_context m sg.type_params in - (* Instantiate the signature *) - let type_params = - List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params - in - let inst_sg = instantiate_fun_sig type_params sg in - (* Create fresh symbolic values for the inputs *) - let input_svs = - List.map - (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) - inst_sg.inputs + *) +let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : + C.eval_ctx = + (* The abstractions are not initialized the same way as for function + * calls: they contain *loan* projectors, because they "provide" us + * with the input values (which behave as if they had been returned + * by some function calls...). + * Also, note that we properly set the set of parents of every abstraction: + * this should not be necessary, as those abstractions should never be + * *automatically* ended (because ending some borrows requires to end + * one of them), but rather selectively ended when generating code + * for each of the backward functions. We do it only because we can + * do it, and because it gives a bit of sanity. + * *) + let sg = fdef.signature in + (* Create the context *) + let ctx = initialize_context m sg.type_params in + (* Instantiate the signature *) + let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in + let inst_sg = instantiate_fun_sig type_params sg in + (* Create fresh symbolic values for the inputs *) + let input_svs = + List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs + in + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let call_id = C.fresh_fun_call_id () in + assert (call_id = V.FunCallId.zero); + let empty_absl = + create_empty_abstractions_from_abs_region_groups call_id V.SynthInput + inst_sg.A.regions_hierarchy + in + (* Add the avalues to the abstractions and insert them in the context *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Project over the values - we use *loan* projectors, as explained above *) + let avalues = + List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs in - (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) - let call_id = C.fresh_fun_call_id () in - assert (call_id = V.FunCallId.zero); - let empty_absl = - create_empty_abstractions_from_abs_region_groups call_id V.SynthInput - inst_sg.A.regions_hierarchy - in - (* Add the avalues to the abstractions and insert them in the context *) - let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = - (* Project over the values - we use *loan* projectors, as explained above *) - let avalues = - List.map - (mk_aproj_loans_value_from_symbolic_value abs.regions) - input_svs - in - (* Insert the avalues in the abstraction *) - let abs = { abs with avalues } in - (* Insert the abstraction in the context *) - let ctx = { ctx with env = Abs abs :: ctx.env } in - (* Return *) - ctx - in - let ctx = List.fold_left insert_abs ctx empty_absl in - (* Split the variables between return var, inputs and remaining locals *) - let ret_var = List.hd fdef.locals in - let input_vars, local_vars = - Collections.List.split_at (List.tl fdef.locals) fdef.arg_count - in - (* Push the return variable (initialized with ⊥) *) - let ctx = C.ctx_push_uninitialized_var ctx ret_var in - (* Push the input variables (initialized with symbolic values) *) - let input_values = List.map mk_typed_value_from_symbolic_value input_svs in - let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in - (* Push the remaining local variables (initialized with ⊥) *) - let ctx = C.ctx_push_uninitialized_vars ctx local_vars in + (* Insert the avalues in the abstraction *) + let abs = { abs with avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) ctx + in + let ctx = List.fold_left insert_abs ctx empty_absl in + (* Split the variables between return var, inputs and remaining locals *) + let ret_var = List.hd fdef.locals in + let input_vars, local_vars = + Collections.List.split_at (List.tl fdef.locals) fdef.arg_count + in + (* Push the return variable (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_var ctx ret_var in + (* Push the input variables (initialized with symbolic values) *) + let input_values = List.map mk_typed_value_from_symbolic_value input_svs in + let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in + (* Push the remaining local variables (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_vars ctx local_vars in + (* Return *) + ctx +module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. *) diff --git a/src/Logging.ml b/src/Logging.ml index 36ede236..23bf672d 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -9,6 +9,12 @@ let main_log = L.get_logger "MainLogger" (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) +(** Logger for Translate *) +let translate_log = L.get_logger "MainLogger.Translate" + +(** Logger for SymbolicToPure *) +let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure" + (** Logger for Interpreter *) let interpreter_log = L.get_logger "MainLogger.Interpreter" diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a3aad6df..46beb5c8 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -7,8 +7,12 @@ module A = CfimAst module M = Modules module S = SymbolicAst module TA = TypesAnalysis +module L = Logging open Pure +(** The local logger *) +let log = L.symbolic_to_pure_log + (** TODO: move this, it is not useful for symbolic -> pure *) type name = | FunName of A.FunDefId.id * T.RegionVarId.id option @@ -353,9 +357,8 @@ let translate_type_def (def : T.type_def) : type_def = (preserve all borrows, etc.) *) -let rec translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty = - let translate = translate_fwd_ty ctx in - let types_infos = ctx.type_context.types_infos in +let rec translate_fwd_ty (types_infos : TA.type_infos) (ty : 'r T.ty) : ty = + let translate = translate_fwd_ty types_infos in match ty with | T.Adt (type_id, regions, tys) -> (* Can't translate types with regions for now *) @@ -379,16 +382,20 @@ let rec translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty = Slice (translate ty) | Ref (_, rty, _) -> translate rty +(** Simply calls [translate_fwd_ty] *) +let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty = + let types_infos = ctx.type_context.types_infos in + translate_fwd_ty types_infos ty + (** 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 - let types_infos = ctx.type_context.types_infos in +let rec translate_back_ty (types_infos : TA.type_infos) + (keep_region : 'r -> bool) (inside_mut : bool) (ty : 'r T.ty) : ty option = + let translate = translate_back_ty types_infos 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 @@ -422,20 +429,27 @@ let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) | 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 + if keep_region r then + translate_back_ty types_infos keep_region inside_mut rty else None) +(** Simply calls [translate_back_ty] *) +let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) + (inside_mut : bool) (ty : 'r T.ty) : ty option = + 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 (def : A.fun_def) (gid : T.RegionGroupId.id) : +let rec list_parent_region_groups (sg : A.fun_sig) (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t = - let rg = T.RegionGroupId.nth def.signature.regions_hierarchy gid in + 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 def gid in + 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 *) @@ -445,13 +459,13 @@ let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : parents (** Small utility: same as [list_parent_region_groups], but returns an ordered list. *) -let list_ordered_parent_region_groups (def : A.fun_def) +let list_ordered_parent_region_groups (sg : A.fun_sig) (gid : T.RegionGroupId.id) : T.RegionGroupId.id list = - let pset = list_parent_region_groups def gid in + 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) - def.signature.regions_hierarchy + sg.regions_hierarchy in let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in parents @@ -480,15 +494,14 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : V.abs list = let abs_ids = list_ancestor_abstractions_ids ctx abs in List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids -let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) +let translate_fun_sig (types_infos : TA.type_infos) (sg : A.fun_sig) (bid : T.RegionGroupId.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 parents = list_parent_region_groups def bid in + let parents = list_parent_region_groups sg bid in (Some bid, parents) in (* List the inputs for: @@ -496,7 +509,7 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) * - 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 + let fwd_inputs = List.map (translate_fwd_ty types_infos) 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); @@ -511,7 +524,7 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) | T.Var r -> T.RegionVarId.Set.mem r regions in let inside_mut = false in - translate_back_ty ctx keep_region inside_mut + translate_back_ty types_infos keep_region inside_mut in (* Compute the additinal inputs for the current function, if it is a backward * function *) @@ -536,7 +549,7 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) match gid with | None -> (* This is a forward function: there is one output *) - [ translate_fwd_ty ctx sg.output ] + [ translate_fwd_ty types_infos 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 @@ -558,7 +571,7 @@ let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh ctx.var_counter in - let ty = translate_fwd_ty ctx sv.sv_ty in + let ty = ctx_translate_fwd_ty ctx sv.sv_ty in let var = { id; ty } in (* Insert in the map *) let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in @@ -619,7 +632,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue let var = lookup_var_for_symbolic_value sv ctx in (mk_typed_rvalue_from_var var).value in - let ty = translate_fwd_ty ctx v.ty in + let ty = ctx_translate_fwd_ty ctx v.ty in { value; ty } (** Explore an abstraction value and convert it to a consumed value @@ -657,7 +670,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) : if field_values = [] then None else let value = RvAdt { variant_id; field_values } in - let ty = translate_fwd_ty ctx av.ty in + let ty = ctx_translate_fwd_ty ctx av.ty in let rv = { value; ty } in Some rv) | ABottom -> failwith "Unreachable" @@ -766,7 +779,7 @@ let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) : if field_values = [] then (ctx, None) else let value = LvTuple field_values in - let ty = translate_fwd_ty ctx av.ty in + let ty = ctx_translate_fwd_ty ctx av.ty in let lv : typed_lvalue = { value; ty } in (ctx, Some lv)) | ABottom -> failwith "Unreachable" @@ -867,7 +880,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : expression = (* Translate the function call *) - let type_params = List.map (translate_fwd_ty ctx) call.type_params in + let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in let args = List.map (typed_value_to_rvalue ctx) call.args in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in (* Retrieve the function id, and register the function call in the context @@ -909,7 +922,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : | V.FunCall -> let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in let call = call_info.forward in - let type_params = List.map (translate_fwd_ty ctx) call.type_params in + let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in (* Retrive the orignal call and the parent abstractions *) let forward, backwards = get_abs_ancestors ctx abs in (* Retrieve the values consumed when we called the forward function and @@ -1122,6 +1135,48 @@ let translate_fun_def (fs_ctx : fs_ctx) (body : S.expression) : fun_def = (* 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 + (* 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 body = translate_expression body bs_ctx in { def_id; name; signature; body } + +let translate_type_defs (type_defs : T.type_def list) : type_def TypeDefId.Map.t + = + List.fold_left + (fun tdefs def -> + let tdef = translate_type_def def in + TypeDefId.Map.add def.def_id tdef tdefs) + TypeDefId.Map.empty type_defs + +let translate_fun_signatures (types_infos : TA.type_infos) + (functions : (A.fun_id * A.fun_sig) list) : fun_sig RegularFunIdMap.t = + (* For every function, translate the signatures of: + - the forward function + - the backward functions + *) + let translate_one (fun_id : A.fun_id) (sg : A.fun_sig) : + (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 + (* 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 + (id, tsg)) + sg.regions_hierarchy + in + (* Return *) + (fwd_id, fwd_sg) :: back_sgs + in + let translated = + List.concat (List.map (fun (id, sg) -> translate_one id sg) functions) + in + List.fold_left + (fun m (id, sg) -> RegularFunIdMap.add id sg m) + RegularFunIdMap.empty translated diff --git a/src/Translate.ml b/src/Translate.ml new file mode 100644 index 00000000..8c6a6def --- /dev/null +++ b/src/Translate.ml @@ -0,0 +1,46 @@ +module L = Logging +module T = Types +module A = CfimAst +module M = Modules +module SA = SymbolicAst +open Cps +open InterpreterUtils +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 = + (* 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)); + + (* 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 + () |