diff options
| -rw-r--r-- | src/CfimAst.ml | 17 | ||||
| -rw-r--r-- | src/CfimAstUtils.ml | 5 | ||||
| -rw-r--r-- | src/Interpreter.ml | 173 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 101 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 28 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | src/Utilities.ml | 16 | ||||
| -rw-r--r-- | src/Utils.ml | 17 | ||||
| -rw-r--r-- | src/main.ml | 2 |
10 files changed, 269 insertions, 94 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index a4a128c3..ac66d1a4 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -95,13 +95,19 @@ class ['self] iter_statement_base = method visit_assertion : 'env -> assertion -> unit = fun _ _ -> () + method visit_operand : 'env -> operand -> unit = fun _ _ -> () + method visit_call : 'env -> call -> unit = fun _ _ -> () + + method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () + + method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () end (** Ancestor for [typed_value] map visitor *) class ['self] map_statement_base = object (_self : 'self) - inherit [_] VisitorsRuntime.iter + inherit [_] VisitorsRuntime.map method visit_place : 'env -> place -> place = fun _ x -> x @@ -111,7 +117,15 @@ class ['self] map_statement_base = method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x + method visit_operand : 'env -> operand -> operand = fun _ x -> x + method visit_call : 'env -> call -> call = fun _ x -> x + + method visit_integer_type : 'env -> integer_type -> integer_type = + fun _ x -> x + + method visit_scalar_value : 'env -> scalar_value -> scalar_value = + fun _ x -> x end type statement = @@ -136,7 +150,6 @@ type statement = | Sequence of statement * statement | Switch of operand * switch_targets | Loop of statement -[@@deriving show] and switch_targets = | If of statement * statement (** Gives the "if" and "else" blocks *) diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml index f811475c..96410dde 100644 --- a/src/CfimAstUtils.ml +++ b/src/CfimAstUtils.ml @@ -2,7 +2,7 @@ open CfimAst open Utils (** Check if a [statement] contains loops *) -let rec statement_has_loops (st : statement) : bool = +let statement_has_loops (st : statement) : bool = let obj = object inherit [_] iter_statement @@ -14,3 +14,6 @@ let rec statement_has_loops (st : statement) : bool = obj#visit_statement () st; false with Found -> true + +(** Check if a [fun_def] contains loops *) +let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body diff --git a/src/Interpreter.ml b/src/Interpreter.ml index e74aa1e7..cb42abf2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,4 +1,9 @@ +open Errors module L = Logging +module T = Types +module A = CfimAst +open Utils +open InterpreterUtils open InterpreterExpressions open InterpreterStatements @@ -18,9 +23,94 @@ open InterpreterStatements (* TODO: remove the config parameters when they are useless *) module Test = struct + let initialize_context (type_context : C.type_context) + (fun_defs : A.fun_def list) : C.eval_ctx = + { + C.type_context; + C.fun_context = fun_defs; + C.type_vars = []; + C.env = []; + C.symbolic_counter = V.SymbolicValueId.generator_zero; + C.borrow_counter = V.BorrowId.generator_zero; + C.region_counter = T.RegionId.generator_zero; + C.abstraction_counter = V.AbstractionId.generator_zero; + } + + (** 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 ⊥ + "Dummy" abstractions are introduced for the regions present in the + function signature. + *) + let initialize_symbolic_context_for_fun (type_context : C.type_context) + (fun_defs : A.fun_def list) (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. + * *) + (* Create the context *) + let ctx = initialize_context type_context fun_defs in + (* Instantiate the signature *) + let sg = fdef.signature in + let type_params = + List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params + in + let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in + (* Create fresh symbolic values for the inputs *) + let ctx, input_svs = + List.fold_left_map + (fun ctx ty -> mk_fresh_symbolic_value ty ctx) + ctx inst_sg.inputs + in + (* Create the abstractions and insert them in the context *) + let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = + let abs_id = rg.A.id in + let parents = + List.fold_left + (fun s pid -> V.AbstractionId.Set.add pid s) + V.AbstractionId.Set.empty rg.A.parents + in + let regions = + List.fold_left + (fun s rid -> T.RegionId.Set.add rid s) + T.RegionId.Set.empty rg.A.regions + in + (* Project over the values - we use *loan* projectors, as explained above *) + let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in + (* Create the abstraction *) + let abs = { V.abs_id; parents; regions; avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in + (* Return *) + ctx + in + (* Split the variables between return var, inputs and remaining locals *) + let ret_var = List.hd fdef.locals in + let input_vars, local_vars = + 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 + (** Test a unit function (taking no arguments) by evaluating it in an empty - environment - *) + environment. + *) let test_unit_function (type_context : C.type_context) (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) @@ -36,20 +126,9 @@ module Test = struct assert (fdef.A.arg_count = 0); (* Create the evaluation context *) - let ctx = - { - C.type_context; - C.fun_context = fun_defs; - C.type_vars = []; - C.env = []; - C.symbolic_counter = V.SymbolicValueId.generator_zero; - C.borrow_counter = V.BorrowId.generator_zero; - C.region_counter = T.RegionId.generator_zero; - C.abstraction_counter = V.AbstractionId.generator_zero; - } - in + let ctx = initialize_context type_context fun_defs in - (* Put the (uninitialized) local variables *) + (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in (* Evaluate the function *) @@ -70,15 +149,65 @@ module Test = struct && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) - let test_all_unit_functions (type_defs : T.type_def list) + let test_unit_functions (type_defs : T.type_def list) + (fun_defs : A.fun_def list) : unit = + let unit_funs = List.filter fun_def_is_unit fun_defs in + let test_unit_fun (def : A.fun_def) : unit = + let type_ctx = { C.type_defs } in + match test_unit_function type_ctx fun_defs def.A.def_id with + | Error _ -> failwith "Unit test failed (concrete execution)" + | Ok _ -> () + in + List.iter test_unit_fun unit_funs + + (** Execute the symbolic interpreter on a function. *) + let test_symbolic_function (type_context : C.type_context) + (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result list + = + (* Retrieve the function declaration *) + let fdef = A.FunDefId.nth fun_defs fid in + + (* Debug *) + L.log#ldebug + (lazy + ("test_symbolic_function: " ^ Print.Types.name_to_string fdef.A.name)); + + (* Sanity check - *) + assert (List.length fdef.A.signature.region_params = 0); + assert (List.length fdef.A.signature.type_params = 0); + assert (fdef.A.arg_count = 0); + + (* Create the evaluation context *) + let ctx = initialize_context type_context fun_defs in + + (* Initialize the inputs as symbolic values *) + raise Unimplemented + + (* (* Initialize the remaining local variables as Bottom *) + let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in + + (* Evaluate the function *) + let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in + match eval_function_body config ctx fdef.A.body with + | [ Ok _ ] -> Ok () + | [ Error err ] -> Error err + | _ -> + (* We execute the concrete interpreter: there shouldn't be any branching *) + failwith "Unreachable"*) + + (** Execute the symbolic interpreter on a list of functions. + + TODO: for now we ignore the functions which contain loops, because + they are not supported by the symbolic interpreter. + *) + let test_symbolic_functions (type_defs : T.type_def list) (fun_defs : A.fun_def list) : unit = + let no_loop_funs = List.filter CfimAstUtils.fun_def_has_loops fun_defs in let test_fun (def : A.fun_def) : unit = - if fun_def_is_unit def then - let type_ctx = { C.type_defs } in - match test_unit_function type_ctx fun_defs def.A.def_id with - | Error _ -> failwith "Unit test failed" - | Ok _ -> () - else () + let type_ctx = { C.type_defs } in + let res = test_symbolic_function type_ctx fun_defs def.A.def_id in + if List.for_all Result.is_ok res then () + else failwith "Unit test failed (symbolic execution)" in List.iter test_fun fun_defs end diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index d4de318b..80725bab 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -410,7 +410,7 @@ let expand_bottom_value_from_projection (config : C.config) during whose evaluation we got stuck *) let projection' = fst - (Utilities.list_split_at p.projection + (Utils.list_split_at p.projection (List.length p.projection - remaining_pes)) in let p' = { p with projection = projection' } in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 91035574..6b06a27f 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -421,6 +421,54 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) (* Return *) Ok ctx) +(** Instantiate a function signature, introducing fresh abstraction ids and + region ids. This is mostly used in preparation of function calls, when + evaluating in symbolic mode of course. + + Note: there are no region parameters, because they should be erased. + *) +let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) + (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig = + (* Generate fresh abstraction ids and create a substitution from region + * group ids to abstraction ids *) + let ctx, rg_abs_ids_bindings = + List.fold_left_map + (fun ctx rg -> + let ctx, abs_id = C.fresh_abstraction_id ctx in + (ctx, (rg.A.id, abs_id))) + ctx sg.regions_hierarchy + in + let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t = + List.fold_left + (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp) + A.RegionGroupId.Map.empty rg_abs_ids_bindings + in + let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id = + A.RegionGroupId.Map.find rg_id asubst_map + in + (* Generate fresh regions and their substitutions *) + let ctx, _, rsubst, _ = + Subst.fresh_regions_with_substs sg.region_params ctx + in + (* Generate the type substitution + * Note that we need the substitution to map the type variables to + * [rty] types (not [ety]). In order to do that, we convert the + * type parameters to types with regions. This is possible only + * if those types don't contain any regions. + * This is a current limitation of the analysis: there is still some + * work to do to properly handle full type parametrization. + * *) + let rtype_params = List.map ety_no_regions_to_rty type_params in + let tsubst = + Subst.make_type_subst + (List.map (fun v -> v.T.index) sg.type_params) + rtype_params + in + (* Substitute the signature *) + let inst_sig = Subst.substitute_signature asubst rsubst tsubst sg in + (* Return *) + (ctx, inst_sig) + (** Evaluate a statement *) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result list = @@ -661,7 +709,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in (* 2. Push the input values *) - let input_locals, locals = Utilities.list_split_at locals def.A.arg_count in + let input_locals, locals = Utils.list_split_at locals def.A.arg_count in let inputs = List.combine input_locals args in (* Note that this function checks that the variables and their values have the same type (this is important) *) @@ -697,43 +745,9 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) (* Retrieve the (correctly instantiated) signature *) let def = C.ctx_lookup_fun_def ctx fid in let sg = def.A.signature in - (* Generate fresh abstraction ids and create a substitution from region - * group ids to abstraction ids *) - let ctx, rg_abs_ids_bindings = - List.fold_left_map - (fun ctx rg -> - let ctx, abs_id = C.fresh_abstraction_id ctx in - (ctx, (rg.A.id, abs_id))) - ctx sg.regions_hierarchy - in - let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t = - List.fold_left - (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp) - A.RegionGroupId.Map.empty rg_abs_ids_bindings - in - let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id = - A.RegionGroupId.Map.find rg_id asubst_map - in - (* Generate fresh regions and their substitutions *) - let ctx, _, rsubst, _ = - Subst.fresh_regions_with_substs sg.region_params ctx - in - (* Generate the type substitution - * Note that we need the substitution to map the type variables to - * [rty] types (not [ety]). In order to do that, we convert the - * type parameters to types with regions. This is possible only - * if those types don't contain any regions. - * This is a current limitation of the analysis: there is still some - * work to do to properly handle full type parametrization. - * *) - let rtype_params = List.map ety_no_regions_to_rty type_params in - let tsubst = - Subst.make_type_subst - (List.map (fun v -> v.T.index) sg.type_params) - rtype_params - in - (* Substitute the signature *) - let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in + (* Instantiate the signature and introduce fresh abstraction and region ids + * while doing so *) + let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in (* Sanity check *) assert (List.length args = def.A.arg_count); (* Evaluate the function call *) @@ -755,10 +769,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx in let ret_value = mk_typed_value_from_proj_comp ret_spc in - let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in - let ret_av : V.typed_avalue = - { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty } - in + let ret_av = mk_aproj_loans_from_symbolic_value ret_spc.V.svalue in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in let args_with_rtypes = List.combine args inst_sg.A.inputs in @@ -768,8 +779,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (fun ((arg, rty) : V.typed_value * T.rty) -> arg.V.ty = Subst.erase_regions rty) args_with_rtypes); - (* Generate the abstractions from the region groups and add them to the context *) - let gen_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = + (* Create the abstractions from the region groups and add them to the context *) + let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = let abs_id = rg.A.id in let parents = List.fold_left @@ -797,7 +808,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (* Return *) ctx in - let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in + let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in (* Move the return value to its destination *) let ctx = assign_to_place config ctx ret_value dest in (* Synthesis *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 5e0375d0..cc54cd24 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -37,11 +37,17 @@ let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var let mk_place_from_var_id (var_id : V.VarId.id) : E.place = { var_id; projection = [] } +(** Create a fresh symbolic value *) +let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) : + C.eval_ctx * V.symbolic_value = + let ctx, sv_id = C.fresh_symbolic_value_id ctx in + let svalue = { V.sv_id; V.sv_ty = ty } in + (ctx, svalue) + (** Create a fresh symbolic proj comp *) let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp = - let ctx, sv_id = C.fresh_symbolic_value_id ctx in - let svalue = { V.sv_id; V.sv_ty = ty } in + let ctx, svalue = mk_fresh_symbolic_value ty ctx in let sv = { V.svalue; rset_ended = ended_regions } in (ctx, sv) @@ -64,12 +70,24 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in mk_typed_value_from_proj_comp spc -let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue = - let ty = sv.V.svalue.V.sv_ty in - let proj = V.AProjLoans sv.V.svalue in +let mk_aproj_loans_from_proj_comp (spc : V.symbolic_proj_comp) : V.typed_avalue + = + let ty = spc.V.svalue.V.sv_ty in + let proj = V.AProjLoans spc.V.svalue in let value = V.ASymbolic proj in { V.value; ty } +(** Create a Loans projector from a symbolic value. + + Initializes the set of ended regions with `empty`. + *) +let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) : + V.typed_avalue = + let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in + let av = V.ASymbolic (V.AProjLoans spc.V.svalue) in + let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in + av + (** TODO: move *) let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool = diff --git a/src/Print.ml b/src/Print.ml index 90f3946b..de1952e1 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -843,7 +843,7 @@ module CfimAst = struct (* Arguments *) let inputs = List.tl def.locals in - let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in + let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in let args = List.combine inputs sg.inputs in let args = List.map diff --git a/src/Utilities.ml b/src/Utilities.ml deleted file mode 100644 index 6452d56f..00000000 --- a/src/Utilities.ml +++ /dev/null @@ -1,16 +0,0 @@ -(* Split a list at a given index [i] (the first list contains all the elements - up to element of index [i], not included, the second one contains the remaining - elements. Note that the first returned list has length [i]. - *) -let rec list_split_at (ls : 'a list) (i : int) = - if i < 0 then raise (Invalid_argument "list_split_at take positive integers") - else if i = 0 then ([], ls) - else - match ls with - | [] -> - raise - (Failure - "The int given to list_split_at should be <= the list's length") - | x :: ls' -> - let ls1, ls2 = list_split_at ls' (i - 1) in - (x :: ls1, ls2) diff --git a/src/Utils.ml b/src/Utils.ml index a285e869..16ee7252 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -1,3 +1,20 @@ +(* Split a list at a given index [i] (the first list contains all the elements + up to element of index [i], not included, the second one contains the remaining + elements. Note that the first returned list has length [i]. +*) +let rec list_split_at (ls : 'a list) (i : int) = + if i < 0 then raise (Invalid_argument "list_split_at take positive integers") + else if i = 0 then ([], ls) + else + match ls with + | [] -> + raise + (Failure + "The int given to list_split_at should be <= the list's length") + | x :: ls' -> + let ls1, ls2 = list_split_at ls' (i - 1) in + (x :: ls1, ls2) + exception Found (** Utility exception diff --git a/src/main.ml b/src/main.ml index 2d2518c7..b4537c3a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -46,4 +46,4 @@ let () = log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); (* Test the unit functions *) - I.Test.test_all_unit_functions m.types m.functions + I.Test.test_unit_functions m.types m.functions |