From 3688596f27a1ba461f48e88446b8812ec73f1a2f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 19:09:16 +0100
Subject: Add an option to split the fwd/back functions and fix a minor issue

---
 Makefile                   | 19 +++++++++++++++++--
 compiler/Main.ml           |  3 +++
 compiler/SymbolicToPure.ml | 19 ++++++++++++-------
 tests/Makefile             |  2 +-
 4 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index 37408554..3ea8cda3 100644
--- a/Makefile
+++ b/Makefile
@@ -256,14 +256,29 @@ testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 .PHONY: tfstar-%
 tfstar-%: OPTIONS += -backend fstar
 tfstar-%: BACKEND_SUBDIR := fstar
-tfstar-%:
+tfstar-%: tsplit-fstar-%
 	$(AENEAS_CMD)
 
 # "p" stands for "Polonius"
 .PHONY: tfstarp-%
 tfstarp-%: OPTIONS += -backend fstar
 tfstarp-%: BACKEND_SUBDIR := fstar
-tfstarp-%:
+tfstarp-%: tsplit-fstarp-%
+	$(AENEAS_CMD)
+
+# Test where we split the forward/backward functions
+.PHONY: tsplit-fstar-%
+tsplit-fstar-%: OPTIONS += -backend fstar -split-fwd-back
+tsplit-fstar-%: BACKEND_SUBDIR := fstar-split
+tsplit-fstar-%:
+	$(AENEAS_CMD)
+
+# Test where we split the forward/backward functions
+# "p" stands for "Polonius"
+.PHONY: tsplit-fstarp-%
+tsplit-fstarp-%: OPTIONS += -backend fstar -split-fwd-back
+tsplit-fstarp-%: BACKEND_SUBDIR := fstar-split
+tsplit-fstarp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tcoq-%
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 835b9088..abc27b46 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -120,6 +120,9 @@ let () =
         " Generate a default lakefile.lean (Lean only)" );
       ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
       ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error");
+      ( "-split-fwd-back",
+        Arg.Clear return_back_funs,
+        " Split the forward and backward functions." );
     ]
   in
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 41922cb5..4674b61c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1076,16 +1076,20 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
     let inputs_no_state =
       List.map (fun ty -> (Some "ret", ty)) inputs_no_state
     in
-    (* We consider the backward function as stateful and potentially failing
+    (* In case we merge the forward/backward functions:
+       we consider the backward function as stateful and potentially failing
        **only if it has inputs** (for the "potentially failing": if it has
        not inputs, we directly evaluate it in the body of the forward function).
     *)
     let back_effect_info =
-      {
-        back_effect_info with
-        stateful = back_effect_info.stateful && inputs_no_state <> [];
-        can_fail = back_effect_info.can_fail && inputs_no_state <> [];
-      }
+      if !Config.return_back_funs then
+        let b = inputs_no_state <> [] in
+        {
+          back_effect_info with
+          stateful = back_effect_info.stateful && b;
+          can_fail = back_effect_info.can_fail && b;
+        }
+      else back_effect_info
     in
     let state =
       if back_effect_info.stateful then [ (None, mk_state_ty) ] else []
@@ -1093,7 +1097,8 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
     let inputs = inputs_no_state @ state in
     let output_names, outputs = compute_back_outputs_for_gid gid in
     let filter =
-      !Config.simplify_merged_fwd_backs && inputs = [] && outputs = []
+      !Config.simplify_merged_fwd_backs
+      && !Config.return_back_funs && inputs = [] && outputs = []
     in
     let info =
       {
diff --git a/tests/Makefile b/tests/Makefile
index 8d40e8da..ccdbf652 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,4 +1,4 @@
-all: test-fstar test-coq test-lean test-hol4
+all: test-fstar test-fstar-split test-coq test-lean test-hol4
 
 test-%:
 	cd $* && $(MAKE) all
-- 
cgit v1.2.3