From 4392758d3e9032edb1ea4a899b92fef886749fca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Sep 2019 22:34:21 +0200 Subject: -fall-loads-nontrap --- driver/Clflags.ml | 1 + driver/Compiler.v | 13 +++++++++++-- driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + extraction/extraction.v | 4 ++++ 5 files changed, 20 insertions(+), 2 deletions(-) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index cf1220d1..fd8227c9 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -75,3 +75,4 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true +let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..d006a7d1 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -42,6 +42,7 @@ Require Constprop. Require CSE. Require Deadcode. Require Unusedglob. +Require Allnontrap. Require Allocation. Require Tunneling. Require Linearize. @@ -63,6 +64,7 @@ Require Constpropproof. Require CSEproof. Require Deadcodeproof. Require Unusedglobproof. +Require Allnontrapproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -136,6 +138,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 8) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -243,6 +247,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -286,7 +291,8 @@ Proof. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. set (p18 := CleanupLabels.transf_program p17) in *. @@ -307,6 +313,7 @@ Proof. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. + exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. exists p15; split. apply Allocproof.transf_program_match; auto. exists p16; split. apply Tunnelingproof.transf_program_match. exists p17; split. apply Linearizeproof.transf_program_match; auto. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -393,6 +400,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..26d888ae 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,6 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) +Parameter all_loads_nontrap: unit -> bool. \ No newline at end of file diff --git a/driver/Driver.ml b/driver/Driver.ml index 288bb436..59b7b222 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -391,6 +391,7 @@ let cmdline_actions = @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem + @ f_opt "all-loads-nontrap" option_all_loads_nontrap (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index e4c1cb25..17925d8c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -127,6 +127,10 @@ Extract Constant Compopts.optim_addx => "fun _ -> !Clflags.option_faddx". Extract Constant Compopts.optim_coalesce_mem => "fun _ -> !Clflags.option_fcoalesce_mem". +Extract Constant Compopts.va_strict => + "fun _ -> false". +Extract Constant Compopts.all_loads_nontrap => + "fun _ -> !Clflags.option_all_loads_nontrap". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". -- cgit