-fall-loads-nontrap

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.
@@ -394,6 +401,8 @@ Ltac DestructM :=
   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.
     eapply Tunnelingproof.transf_program_correct; eassumption.
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".