Make progress on translation

5 files changed, 147 insertions, 75 deletions

diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index 96410dde..430678f1 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -1,5 +1,6 @@
 open CfimAst
 open Utils
+module T = Types
 
 (** Check if a [statement] contains loops *)
 let statement_has_loops (st : statement) : bool =
@@ -17,3 +18,34 @@ let statement_has_loops (st : statement) : bool =
 
 (** Check if a [fun_def] contains loops *)
 let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body
+
+(** 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 (sg : fun_sig) (gid : T.RegionGroupId.id) :
+    T.RegionGroupId.Set.t =
+  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 sg gid in
+        (* Parents U current region *)
+        let parents = T.RegionGroupId.Set.add gid parents in
+        (* Make the union with the accumulator *)
+        T.RegionGroupId.Set.union s parents)
+      T.RegionGroupId.Set.empty rg.parents
+  in
+  parents
+
+(** Small utility: same as [list_parent_region_groups], but returns an ordered list.  *)
+let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id)
+    : T.RegionGroupId.id list =
+  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)
+      sg.regions_hierarchy
+  in
+  let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
+  parents
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 74e4e815..617f6211 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -5,6 +5,7 @@ module M = Modules
 module SA = SymbolicAst
 open Cps
 open InterpreterUtils
+open InterpreterExpressions
 open InterpreterStatements
 
 (** The local logger *)
@@ -97,6 +98,66 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) :
   (* Return *)
   ctx
 
+(** Evaluate a function with the symbolic interpreter *)
+let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
+    (m : M.cfim_module) (fid : A.FunDefId.id)
+    (back_id : T.RegionGroupId.id option) : unit =
+  (* Retrieve the function declaration *)
+  let fdef = A.FunDefId.nth m.functions fid in
+
+  (* Debug *)
+  let name_to_string () =
+    Print.name_to_string fdef.A.name
+    ^ " ("
+    ^ Print.option_to_string T.RegionGroupId.to_string back_id
+    ^ ")"
+  in
+  log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
+
+  (* Create the evaluation context *)
+  let ctx = initialize_symbolic_context_for_fun m fdef in
+
+  (* Create the continuation to finish the evaluation *)
+  let config = C.config_of_partial C.SymbolicMode config in
+  let cf_finish res ctx =
+    match res with
+    | Return ->
+        if synthesize then
+          (* There are two cases:
+           * - if this is a forward translation, we retrieve the returned value.
+           * - if this is a backward translation, we introduce "return"
+           *   abstractions to consume the return value, then end all the
+           *   abstractions up to the one in which we are interested.
+           *)
+          match back_id with
+          | None ->
+              (* Forward translation *)
+              (* Move the return value *)
+              let ret_vid = V.VarId.zero in
+              let cf_move =
+                eval_operand config (E.Move (mk_place_from_var_id ret_vid))
+              in
+              (* Generate the Return node *)
+              let cf_return ret_value : m_fun =
+               fun _ -> Some (SA.Return ret_value)
+              in
+              (* Apply *)
+              cf_move cf_return ctx
+          | Some back_id ->
+              (* Backward translation *) 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 ("evaluate_function_symbolic failed on: " ^ name_to_string ())
+  in
+
+  (* Evaluate the function *)
+  let _ = eval_function_body config fdef.A.body cf_finish ctx in
+  ()
+
 module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
@@ -163,26 +224,8 @@ module Test = struct
     log#ldebug
       (lazy ("test_function_symbolic: " ^ 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
+    (* Execute *)
+    let _ = evaluate_function_symbolic config synthesize m fid None in
     ()
 
   (** Execute the symbolic interpreter on a list of functions.
diff --git a/src/Pure.ml b/src/Pure.ml
index 9a16264d..068a2127 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -134,7 +134,19 @@ type fun_id =
   | Unop of unop
   | Binop of E.binop * T.integer_type
 
-type call = { func : fun_id; type_params : ty list; args : typed_rvalue list }
+type call = {
+  func : fun_id;
+  type_params : ty list;
+  args : typed_rvalue list;
+      (** Note that at this point, some functions have no arguments. For instance:
+          ```
+          fn f();
+          ```
+
+          In the extracted code, we add a unit argument. This is unit argument is
+          added later, when going from the "pure" AST to the "extracted" AST.
+       *)
+}
 
 type let_bindings =
   | Call of typed_lvalue list * call
@@ -216,7 +228,12 @@ type inst_fun_sig = { inputs : ty list; outputs : ty list }
 
 type fun_def = {
   def_id : FunDefId.id;
-  name : name;
+  basename : name;
+      (** The "base" name of the function.
+  
+          The base name is the original name of the Rust function. We add suffixes
+          (to identify the forward/backward functions) later.
+       *)
   signature : fun_sig;
   body : expression;
 }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 46beb5c8..51d3c170 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1,4 +1,6 @@
 open Errors
+open Pure
+open CfimAstUtils
 module Id = Identifiers
 module T = Types
 module V = Values
@@ -8,7 +10,6 @@ module M = Modules
 module S = SymbolicAst
 module TA = TypesAnalysis
 module L = Logging
-open Pure
 
 (** The local logger *)
 let log = L.symbolic_to_pure_log
@@ -148,7 +149,7 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
   let outputs = List.map subst sg.outputs in
   { inputs; outputs }
 
-type regular_fun_id = { fun_id : A.fun_id; back_id : T.RegionGroupId.id option }
+type regular_fun_id = A.fun_id * T.RegionGroupId.id option
 [@@deriving show, ord]
 (** We use this type as a key for lookups *)
 
@@ -189,7 +190,6 @@ type call_info = {
 type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
-  fun_def : A.fun_def;
   bid : T.RegionGroupId.id option;
   sv_to_var : var V.SymbolicValueId.Map.t;
       (** Whenever we encounter a new symbolic value (introduced because of
@@ -239,7 +239,6 @@ let fs_ctx_to_bs_ctx (fs_ctx : fs_ctx) : bs_ctx =
   let calls = V.FunCallId.Map.empty in
   let abstractions = V.AbstractionId.Map.empty in
   {
-    fun_def;
     bid;
     sv_to_var;
     var_counter;
@@ -255,7 +254,7 @@ let get_instantiated_fun_sig (fun_id : A.fun_id)
     (back_id : T.RegionGroupId.id option) (tys : ty list) (ctx : bs_ctx) :
     inst_fun_sig =
   (* Lookup the non-instantiated function signature *)
-  let sg = RegularFunIdMap.find { fun_id; back_id } ctx.fun_context.fun_sigs in
+  let sg = RegularFunIdMap.find (fun_id, back_id) ctx.fun_context.fun_sigs in
   (* Create the substitution *)
   let tsubst = make_type_subst sg.type_params tys in
   (* Apply *)
@@ -439,37 +438,6 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
   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 (sg : A.fun_sig) (gid : T.RegionGroupId.id) :
-    T.RegionGroupId.Set.t =
-  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 sg gid in
-        (* Parents U current region *)
-        let parents = T.RegionGroupId.Set.add gid parents in
-        (* Make the union with the accumulator *)
-        T.RegionGroupId.Set.union s parents)
-      T.RegionGroupId.Set.empty rg.parents
-  in
-  parents
-
-(** Small utility: same as [list_parent_region_groups], but returns an ordered list.  *)
-let list_ordered_parent_region_groups (sg : A.fun_sig)
-    (gid : T.RegionGroupId.id) : T.RegionGroupId.id list =
-  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)
-      sg.regions_hierarchy
-  in
-  let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
-  parents
-
 let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) :
     V.AbstractionId.id list =
   (* We could do something more "elegant" without references, but it is
@@ -1128,20 +1096,22 @@ 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
   (* Translate the function *)
   let def_id = def.A.def_id in
-  let name = translate_fun_name 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 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
-  { def_id; name; signature; body }
+  { def_id; basename; signature; body }
 
 let translate_type_defs (type_defs : T.type_def list) : type_def TypeDefId.Map.t
     =
@@ -1161,13 +1131,13 @@ let translate_fun_signatures (types_infos : TA.type_infos)
       (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
+    let fwd_id = (fun_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
+          let id = (fun_id, Some rg.id) in
           (id, tsg))
         sg.regions_hierarchy
     in
diff --git a/src/Translate.ml b/src/Translate.ml
index 8c6a6def..efdad619 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -3,6 +3,7 @@ module T = Types
 module A = CfimAst
 module M = Modules
 module SA = SymbolicAst
+open Errors
 open Cps
 open InterpreterUtils
 open InterpreterStatements
@@ -10,18 +11,21 @@ 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 =
+(** Execute the symbolic interpreter on a function to generate a symbolic AST. *)
+let translate_function_to_symbolic (config : C.partial_config)
+    (m : M.cfim_module) (fid : A.FunDefId.id)
+    (back_id : T.RegionGroupId.id option) : 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));
+    (lazy
+      ("translate_function_to_pure: "
+      ^ Print.name_to_string fdef.A.name
+      ^ " ("
+      ^ Print.option_to_string T.RegionGroupId.to_string back_id
+      ^ ")"));
 
   (* Create the evaluation context *)
   let ctx = initialize_symbolic_context_for_fun m fdef in
@@ -29,7 +33,7 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module)
   (* 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
+    | Return -> raise Errors.Unimplemented
     | Panic ->
         (* Note that as we explore all the execution branches, one of
          * the executions can lead to a panic *)
@@ -44,3 +48,9 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module)
   let config = C.config_of_partial C.SymbolicMode config in
   let _ = eval_function_body config fdef.A.body cf_check ctx in
   ()
+
+let translate (config : C.partial_config) (m : M.cfim_module) : unit =
+  (* Translate all the type definitions *)
+
+  (* Translate all the function signatures *)
+  raise Unimplemented