From b5295c0bf9e7aee437eed8f8fc57e4fba46cb8ef Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 10:55:40 +0100
Subject: Implement filtering of useless forward functions

---
 src/PureMicroPasses.ml | 74 ++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 68 insertions(+), 6 deletions(-)

(limited to 'src/PureMicroPasses.ml')

diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 59871600..7094d885 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -47,6 +47,20 @@ type config = {
           
           See the comments for [expression_contains_child_call_in_all_paths]
           for additional explanations.
+          
+          TODO: rename to [filter_useless_monadic_calls]
+       *)
+  filter_useless_functions : bool;
+      (** If [filter_unused_monadic_calls] is activated, some functions
+          become useless: if this option is true, we don't extract them.
+
+          The calls to functions which always get filtered are:
+          - the forward functions with unit return value
+          - the backward functions which don't output anything (backward
+            functions coming from rust functions with no mutable borrows
+            as input values - note that if a function doesn't take mutable
+            borrows as inputs, it can't return mutable borrows; we actually
+            dynamically check for that).
        *)
   add_unit_args : bool;
       (** Add unit input arguments to functions with no arguments. *)
@@ -612,11 +626,47 @@ let filter_unused (filter_monadic_calls : bool) (ctx : trans_ctx)
   { def with body; inputs_lvs }
 
 (** Return `None` if the function is a backward function with no outputs (so
-    that we eliminate the definition which is useless) *)
-let filter_if_backward_with_no_outputs (def : fun_def) : fun_def option =
-  if Option.is_some def.back_id && def.signature.outputs = [] then None
+    that we eliminate the definition which is useless).
+
+    Note that the calls to such functions are filtered when translating from
+    symbolic to pure. Here, we remove the definitions altogether, because they
+    are now useless
+  *)
+let filter_if_backward_with_no_outputs (config : config) (def : fun_def) :
+    fun_def option =
+  if
+    config.filter_useless_functions && Option.is_some def.back_id
+    && def.signature.outputs = []
+  then None
   else Some def
 
+(** Return `false` if the forward function is useless and should be filtered.
+
+    - a forward function with no output (comes from a Rust function with
+      unit return type)
+    - the function has mutable borrows as inputs (which is materialized
+      by the fact we generated backward functions which were not filtered).
+
+    In such situation, every call to the Rust function will be translated to:
+    - a call to the forward function which returns nothing
+    - calls to the backward functions
+    As a failing backward function implies the forward function also fails,
+    we can filter the calls to the forward function, which thus becomes
+    useless.
+    In such situation, we can remove the forward function definition
+    altogether.
+  *)
+let keep_forward (config : config) (trans : pure_fun_translation) : bool =
+  let fwd, backs = trans in
+  (* Note that at this point, the output types are no longer seen as tuples:
+   * they should be lists of length 1. *)
+  if
+    config.filter_useless_functions
+    && fwd.signature.outputs = [ mk_result_ty unit_ty ]
+    && backs <> []
+  then false
+  else true
+
 (** Add unit arguments (optionally) to functions with no arguments, and
     change their output type to use `result`
   *)
@@ -852,7 +902,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
    * Note that the calls to those functions should already have been removed,
    * when translating from symbolic to pure. Here, we remove the definitions
    * altogether, because they are now useless *)
-  let def = filter_if_backward_with_no_outputs def in
+  let def = filter_if_backward_with_no_outputs config def in
 
   match def with
   | None -> None
@@ -924,9 +974,21 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
       (* We are done *)
       Some def
 
+(** Return the forward/backward translations on which we applied the micro-passes.
+
+    Also returns a boolean indicating whether the forward function should be kept
+    or not (because useful/useless - `true` means we need to keep the forward
+    function).
+    Note that we don't "filter" the forward function and return a boolean instead,
+    because this function contains useful information to extract the backward
+    functions: keeping it is not necessary but more convenient.
+ *)
 let apply_passes_to_pure_fun_translation (config : config) (ctx : trans_ctx)
-    (trans : pure_fun_translation) : pure_fun_translation =
+    (trans : pure_fun_translation) : bool * pure_fun_translation =
+  (* Apply the passes to the individual functions *)
   let forward, backwards = trans in
   let forward = Option.get (apply_passes_to_def config ctx forward) in
   let backwards = List.filter_map (apply_passes_to_def config ctx) backwards in
-  (forward, backwards)
+  let trans = (forward, backwards) in
+  (* Compute whether we need to filter the forward function or not *)
+  (keep_forward config trans, trans)
-- 
cgit v1.2.3