summaryrefslogtreecommitdiff
path: root/src/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Translate.ml')
-rw-r--r--src/Translate.ml158
1 files changed, 145 insertions, 13 deletions
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