diff options
| -rw-r--r-- | src/Assumed.ml | 2 | ||||
| -rw-r--r-- | src/Identifiers.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 3 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 42 | ||||
| -rw-r--r-- | src/Translate.ml | 158 | ||||
| -rw-r--r-- | src/main.ml | 1 |
6 files changed, 178 insertions, 29 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index c40387ea..fd11f30b 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -61,7 +61,7 @@ let box_deref_mut_sig = box_deref_sig true Rk.: following what is written above, we don't include `Box::free`. *) -let assumed_functions : (A.assumed_fun_id * A.fun_sig) list = +let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list = [ (BoxNew, box_new_sig); (BoxDeref, box_deref_shared_sig); diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 3a900643..757c9df5 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -44,6 +44,7 @@ module type Id = sig val of_int : int -> id val nth : 'a list -> id -> 'a + (* TODO: change the signature (invert the index and the list *) val nth_opt : 'a list -> id -> 'a option diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c7e67f0a..b0d4e5e0 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -561,6 +561,9 @@ let eval_non_local_function_call_concrete (config : C.config) evaluating in symbolic mode of course. Note: there are no region parameters, because they should be erased. + + **Rk.:** this function is **stateful** and generates fresh abstraction ids + for the region groups. *) let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) : A.inst_fun_sig = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index be8730a3..41df82f6 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -224,7 +224,7 @@ type fs_ctx = { } (** Function synthesis context - TODO: merge with bs_ctx? + TODO: remove *) let fs_ctx_to_bs_ctx (fs_ctx : fs_ctx) : bs_ctx = @@ -273,6 +273,12 @@ let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def = FunDefId.Map.find id ctx.fun_context.cfim_fun_defs +(* 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 bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) (ctx : bs_ctx) : bs_ctx = let calls = ctx.calls in @@ -558,6 +564,19 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl +(** This generates a fresh variable **which is not to be linked to any symbolic value** *) +let fresh_var (ty : ty) (ctx : bs_ctx) : bs_ctx * var = + (* Generate the fresh variable *) + let id, var_counter = VarId.fresh ctx.var_counter in + let var = { id; ty } in + (* Update the context *) + let ctx = { ctx with var_counter } in + (* Return *) + (ctx, var) + +let fresh_vars (tys : ty list) (ctx : bs_ctx) : bs_ctx * var list = + List.fold_left_map (fun ctx ty -> fresh_var ty ctx) ctx tys + let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var @@ -1175,21 +1194,14 @@ 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 +let translate_fun_def (def : A.fun_def) (ctx : bs_ctx) (body : S.expression) : + fun_def = + let bid = ctx.bid in (* Translate the function *) let def_id = def.A.def_id 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 + let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in + let body = translate_expression body ctx in (* Compute the list of (properly ordered) input variables *) let backward_inputs : var list = match bid with @@ -1201,10 +1213,10 @@ let translate_fun_def (fs_ctx : fs_ctx) (body : S.expression) : fun_def = let backward_ids = List.append parents_ids [ back_id ] in List.concat (List.map - (fun id -> T.RegionGroupId.Map.find id bs_ctx.backward_inputs) + (fun id -> T.RegionGroupId.Map.find id ctx.backward_inputs) backward_ids) in - let inputs = List.append bs_ctx.forward_inputs backward_inputs in + let inputs = List.append ctx.forward_inputs backward_inputs in (* Sanity check *) assert ( List.for_all diff --git a/src/Translate.ml b/src/Translate.ml index 69e09334..b3dcf522 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -1,18 +1,20 @@ +open Errors +open Cps +open InterpreterUtils +open InterpreterStatements +open Interpreter module L = Logging module T = Types module A = CfimAst module M = Modules module SA = SymbolicAst -open Errors -open Cps -open InterpreterUtils -open InterpreterStatements (** The local logger *) let log = L.translate_log (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, - for the forward function and the backward functions. *) + for the forward function and the backward functions. + *) let translate_function_to_symbolics (config : C.partial_config) (m : M.cfim_module) (fid : A.FunDefId.id) : SA.expression * SA.expression list = @@ -25,23 +27,153 @@ let translate_function_to_symbolics (config : C.partial_config) ("translate_function_to_symbolics: " ^ Print.name_to_string fdef.A.name)); (* Evaluate *) + let synthesize = true in let evaluate = evaluate_function_symbolic config synthesize m fid in (* Execute the forward function *) - let forward = evaluate None in + let forward = Option.get (evaluate None) in (* Execute the backward functions *) let backwards = T.RegionGroupId.mapi - (fun gid _ -> evaluate (Some gid)) + (fun gid _ -> Option.get (evaluate (Some gid))) fdef.signature.regions_hierarchy in (* Return *) (forward, backwards) -(*let translate (config : C.partial_config) (m : M.cfim_module) : unit = - (* Translate all the type definitions *) - let type_defs = SymbolicToPure.translate_type_defs m.type_defs in +(** Translate a function, by generating its forward and backward translations. + + TODO: we shouldn't need to take m as parameter (we actually recompute the + type and function contexts in [translate_function_to_symbolics]...) + *) +let translate_function (config : C.partial_config) (m : M.cfim_module) + (type_context : C.type_context) (fun_context : C.fun_context) + (fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t) + (fdef : A.fun_def) : Pure.fun_def * Pure.fun_def list = + let def_id = fdef.def_id in + + (* Compute the symbolic ASTs *) + let symbolic_forward, symbolic_backwards = + translate_function_to_symbolics config m fdef.def_id + in + + (* Convert the symbolic ASTs to pure ASTs: *) + + (* Initialize the context *) + let sv_to_var = V.SymbolicValueId.Map.empty in + let var_counter = Pure.VarId.generator_zero in + let calls = V.FunCallId.Map.empty in + let abstractions = V.AbstractionId.Map.empty in + let type_context = + { + SymbolicToPure.types_infos = type_context.type_infos; + cfim_type_defs = type_context.type_defs; + } + in + let fun_context = + { SymbolicToPure.cfim_fun_defs = fun_context.fun_defs; fun_sigs } + in + let ctx = + { + SymbolicToPure.bid = None; + (* Dummy for now *) + sv_to_var; + var_counter; + type_context; + fun_context; + forward_inputs = []; + (* Empty for now *) + backward_inputs = T.RegionGroupId.Map.empty; + (* Empty for now *) + backward_outputs = T.RegionGroupId.Map.empty; + (* Empty for now *) + calls; + abstractions; + } + in + + (* We need to initialize the input/output variables. First, the inputs + * for the forward function *) + let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in + let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in + let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_sg.inputs ctx in - (* Translate all the function signatures *) - let fun_defs = SymbolicToPure.translate_fun_signatures types_infos - raise Unimplemented*) + let ctx = { ctx with forward_inputs } in + + (* Translate the forward function *) + let pure_forward = + SymbolicToPure.translate_fun_def fdef ctx symbolic_forward + in + + (* Translate the backward functions *) + let translate_backward (rg : T.region_var_group) : Pure.fun_def = + (* For the backward inputs/outputs initialization: we use the fact that + * there are no nested borrows for now, and so that the region groups + * can't have parents *) + assert (rg.parents = []); + (* TODO: the computation of the backward inputs is a bit awckward... *) + let back_id = rg.id in + let backward_sg = + RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs + in + let _, backward_inputs = + Collections.List.split_at backward_sg.inputs (List.length forward_inputs) + in + let ctx, backward_inputs = SymbolicToPure.fresh_vars backward_inputs ctx in + let backward_outputs = backward_sg.outputs in + let ctx, backward_outputs = + SymbolicToPure.fresh_vars backward_outputs ctx + in + let backward_inputs = + T.RegionGroupId.Map.singleton back_id backward_inputs + in + let backward_outputs = + T.RegionGroupId.Map.singleton back_id backward_outputs + in + + (* Put everything in the context *) + let ctx = + { ctx with bid = Some back_id; backward_inputs; backward_outputs } + in + + (* Translate *) + let symbolic = T.RegionGroupId.nth symbolic_backwards back_id in + SymbolicToPure.translate_fun_def fdef ctx symbolic + in + let pure_backwards = + List.map translate_backward fdef.signature.regions_hierarchy + in + + (* Return *) + (pure_forward, pure_backwards) + +let translate_module (config : C.partial_config) (m : M.cfim_module) : unit = + (* Compute the type and function contexts *) + let type_context, fun_context = compute_type_fun_contexts m in + + (* Translate all the type definitions *) + let type_defs = SymbolicToPure.translate_type_defs m.types in + + (* Translate all the function *signatures* *) + let assumed_sigs = + List.map (fun (id, sg) -> (A.Assumed id, sg)) Assumed.assumed_sigs + in + let local_sigs = + List.map + (fun (fdef : A.fun_def) -> (A.Local fdef.def_id, fdef.signature)) + m.functions + in + let sigs = List.append assumed_sigs local_sigs in + let fun_sigs = + SymbolicToPure.translate_fun_signatures type_context.type_infos sigs + in + + (* Translate all the functions *) + let fun_defs = + List.map + (fun (fdef : A.fun_def) -> + ( fdef.def_id, + translate_function config m type_context fun_context fun_sigs )) + m.functions + in + raise Unimplemented diff --git a/src/main.ml b/src/main.ml index ea4ab23f..db57b5a7 100644 --- a/src/main.ml +++ b/src/main.ml @@ -9,6 +9,7 @@ module TA = TypesAnalysis module P = Pure open PrintSymbolicAst open SymbolicToPure +open Translate (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. |