make conditions a parameter in CSE3

2 files changed, 12 insertions, 3 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index f3a0af24..6cb43085 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -15,6 +15,7 @@ Require Import AST Linking.
 Require Import Memory Registers Op RTL Maps CSE2deps.
 Require Import CSE3analysis HashedSet.
 Require Import RTLtyping.
+Require Compopts.
 
 Local Open Scope error_monad_scope.
 
@@ -139,3 +140,9 @@ Definition param_transf_program (p: program) : res program :=
   transform_partial_program param_transf_fundef p.
 
 End PARAMS.
+
+Definition cmdline_params (_ : unit) :=
+  mkcse3params
+    (Compopts.optim_CSE3_conditions tt).
+
+Definition transf_program p := param_transf_program (cmdline_params tt) p.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 2e9f99c5..1168374a 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -31,11 +31,11 @@ Require Import RTLtyping.
 Section PARAMS.
   Variable params : cse3params.
   
-Definition match_prog (p tp: RTL.program) :=
+Definition param_match_prog (p tp: RTL.program) :=
   match_program (fun ctx f tf => param_transf_fundef params f = OK tf) eq p tp.
 
 Lemma transf_program_match:
-  forall p tp, param_transf_program params p = OK tp -> match_prog p tp.
+  forall p tp, param_transf_program params p = OK tp -> param_match_prog p tp.
 Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
@@ -43,7 +43,7 @@ Qed.
 Section PRESERVATION.
 
 Variables prog tprog: program.
-Hypothesis TRANSF: match_prog prog tprog.
+Hypothesis TRANSF: param_match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
@@ -1217,3 +1217,5 @@ Qed.
 
 End PRESERVATION.
 End PARAMS.
+
+Definition match_prog := param_match_prog (cmdline_params tt).