diff options
| -rw-r--r-- | Makefile | 19 | ||||
| -rw-r--r-- | compiler/Main.ml | 3 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 19 | ||||
| -rw-r--r-- | tests/Makefile | 2 |
4 files changed, 33 insertions, 10 deletions
@@ -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 |