Implement Translate.translate_function

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.