From e11b548d94b247b5359960b8d31027b53ee0dffc Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 20:47:25 +0200
Subject: rm condition parametrization in CSE3analysis

---
 backend/CSE3analysis.v      |  7 ++-----
 backend/CSE3analysisproof.v | 12 ++++--------
 2 files changed, 6 insertions(+), 13 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 75e00f67..9a6c9c0d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -477,13 +477,10 @@ Section OPERATIONS.
     end.
 
   Definition apply_cond cond args (rel : RELATION.t) : RB.t :=
-    if Compopts.optim_CSE3_conditions tt
-    then 
-      match apply_cond1 cond args rel with
+    match apply_cond1 cond args rel with
       | Some rel => Some (apply_cond0 cond args rel)
       | None => RB.bot
-      end
-    else Some rel.
+    end.
       
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 382c9f4c..523b52df 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1350,14 +1350,10 @@ Section SOUNDNESS.
   Proof.
     unfold apply_cond.
     intros.
-    destruct (Compopts.optim_CSE3_conditions tt).
-    {
-      pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
-      destruct apply_cond1 eqn:COND1.
-      { apply apply_cond0_sound; auto. }
-      exact SOUND1.
-    }
-    exact REL.
+    pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
+    destruct apply_cond1 eqn:COND1.
+    { apply apply_cond0_sound; auto. }
+    exact SOUND1.
   Qed.
   
   (*
-- 
cgit 


From 7b34d3c03fea76b85ec72d5ee82c53353960e2b2 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:11:34 +0200
Subject: make CSE3 condition parametric

---
 backend/CSE3.v      | 12 ++++++++++-
 backend/CSE3proof.v | 59 ++++++++++++++++++++++++++++-------------------------
 2 files changed, 42 insertions(+), 29 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 746ba399..5d05821a 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -20,6 +20,14 @@ Local Open Scope error_monad_scope.
 
 Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
 
+Record cse3params : Type :=
+  mkcse3params
+    { cse3_conditions : bool;
+    }.
+
+Section PARAMS.
+  Variable params : cse3params.
+
 Section REWRITE.
   Context {ctx : eq_context}.
 
@@ -54,7 +62,7 @@ Definition subst_args fmap pc xl :=
   forward_move_l_b (PMap.get pc fmap) xl.
 
 Definition find_cond_in_fmap fmap pc cond args :=
-  if Compopts.optim_CSE3_conditions tt
+  if cse3_conditions params
   then
     match PMap.get pc fmap with
     | Some rel =>
@@ -129,3 +137,5 @@ Definition transf_fundef (fd: fundef) : res fundef :=
 
 Definition transf_program (p: program) : res program :=
   transform_partial_program transf_fundef p.
+
+End PARAMS.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 0722f904..2d9992c6 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -28,12 +28,14 @@ Require Import Registers Op RTL.
 Require Import CSE3 CSE3analysis CSE3analysisproof.
 Require Import RTLtyping.
 
-
+Section PARAMS.
+  Variable params : cse3params.
+  
 Definition match_prog (p tp: RTL.program) :=
-  match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp.
+  match_program (fun ctx f tf => transf_fundef params f = OK tf) eq p tp.
 
 Lemma transf_program_match:
-  forall p tp, transf_program p = OK tp -> match_prog p tp.
+  forall p tp, transf_program params p = OK tp -> match_prog p tp.
 Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
@@ -111,7 +113,7 @@ Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
-    Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+    Genv.find_funct tge v = Some tf /\ transf_fundef params f = OK tf.
 Proof.
   apply (Genv.find_funct_transf_partial TRANSF).
 Qed.
@@ -120,7 +122,7 @@ Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef params f = OK tf.
 Proof.
   apply (Genv.find_funct_ptr_transf_partial TRANSF).
 Qed.
@@ -139,7 +141,7 @@ Proof.
 Qed.
 
 Lemma sig_preserved:
-  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
+  forall f tf, transf_fundef params f = OK tf -> funsig tf = funsig f.
 Proof.
   destruct f; simpl; intros.
   - monadInv H.
@@ -154,7 +156,7 @@ Proof.
 Qed.
 
 Lemma stacksize_preserved:
-  forall f tf, transf_function f = OK tf -> fn_stacksize tf = fn_stacksize f.
+  forall f tf, transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -166,7 +168,7 @@ Proof.
 Qed.
 
 Lemma params_preserved:
-  forall f tf, transf_function f = OK tf -> fn_params tf = fn_params f.
+  forall f tf, transf_function params f = OK tf -> fn_params tf = fn_params f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -178,7 +180,7 @@ Proof.
 Qed.
 
 Lemma entrypoint_preserved:
-  forall f tf, transf_function f = OK tf -> fn_entrypoint tf = fn_entrypoint f.
+  forall f tf, transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -190,7 +192,7 @@ Proof.
 Qed.
 
 Lemma sig_preserved2:
-  forall f tf, transf_function f = OK tf -> fn_sig tf = fn_sig f.
+  forall f tf, transf_function params f = OK tf -> fn_sig tf = fn_sig f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -202,7 +204,7 @@ Proof.
 Qed.
 
 Lemma transf_function_is_typable:
-  forall f tf, transf_function f = OK tf ->
+  forall f tf, transf_function params f = OK tf ->
                exists tenv, type_function f = OK tenv.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
@@ -211,7 +213,7 @@ Proof.
   assumption.
 Qed.
 Lemma transf_function_invariants_inductive:
-  forall f tf tenv, transf_function f = OK tf ->
+  forall f tf tenv, transf_function params f = OK tf ->
     type_function f = OK tenv ->
     check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f))))
                         f tenv (fst (preanalysis tenv f)) = true.
@@ -228,7 +230,7 @@ Lemma find_function_translated:
   forall ros rs fd,
     find_function ge ros rs = Some fd ->
     exists tfd,
-      find_function tge ros rs = Some tfd /\ transf_fundef fd = OK tfd.
+      find_function tge ros rs = Some tfd /\ transf_fundef params fd = OK tfd.
 Proof.
   unfold find_function; intros. destruct ros as [r|id].
   eapply functions_translated; eauto.
@@ -243,7 +245,7 @@ Inductive match_stackframes: list stackframe -> list stackframe -> signature ->
   | match_stackframes_cons:
       forall res f sp pc rs s tf ts sg tenv
         (STACKS: match_stackframes s ts (fn_sig tf))
-        (FUN: transf_function f = OK tf)
+        (FUN: transf_function params f = OK tf)
         (WTF: type_function f = OK tenv)
         (WTRS: wt_regset tenv rs)
         (WTRES: tenv res = proj_sig_res sg)
@@ -260,7 +262,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s f sp pc rs m ts tf tenv
         (STACKS: match_stackframes s ts (fn_sig tf))
-        (FUN: transf_function f = OK tf)
+        (FUN: transf_function params f = OK tf)
         (WTF: type_function f = OK tenv)
         (WTRS: wt_regset tenv rs)
         (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m),
@@ -269,7 +271,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_call:
       forall s f args m ts tf
         (STACKS: match_stackframes s ts (funsig tf))
-        (FUN: transf_fundef f = OK tf)
+        (FUN: transf_fundef params f = OK tf)
         (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
       match_states (Callstate s f args m)
                    (Callstate ts tf args m)
@@ -294,12 +296,12 @@ Qed.
 
 Lemma transf_function_at:
   forall f tf pc tenv instr
-    (TF : transf_function f = OK tf)
+    (TF : transf_function params f = OK tf)
     (TYPE : type_function f = OK tenv)
     (PC : (fn_code f) ! pc = Some instr),
     (fn_code tf) ! pc = Some (transf_instr
        (ctx := (context_from_hints (snd (preanalysis tenv f))))
-       (fst (preanalysis tenv f))
+       params (fst (preanalysis tenv f))
        pc instr).
 Proof.
   intros.
@@ -498,8 +500,8 @@ Proof.
       
   - (* Iop *)
     exists (State ts tf sp pc' (rs # res <- v) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity.
+    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
+      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity.
       unfold transf_instr, find_op_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
@@ -581,8 +583,8 @@ Proof.
       (* END INVARIANT *)
   - (* Iload *)
     exists (State ts tf sp pc' (rs # dst <- v) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
+    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
+      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
       unfold transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
@@ -659,8 +661,8 @@ Proof.
         
   - (* Iload notrap1 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
       unfold transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
@@ -735,8 +737,8 @@ Proof.
         
   - (* Iload notrap2 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
       unfold transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
@@ -941,7 +943,7 @@ Proof.
         eapply external_call_sound; unfold ctx; eauto with cse3.
         
   - (* Icond *)
-    destruct (find_cond_in_fmap (ctx := ctx) invs pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
+    destruct (find_cond_in_fmap (ctx := ctx) params invs pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
     + econstructor; split.
       * eapply exec_Inop; try eassumption.
         TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
@@ -983,7 +985,7 @@ Proof.
         unfold find_cond_in_fmap in FIND_COND.
         change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
         rewrite FIND_REL in FIND_COND.
-        destruct (Compopts.optim_CSE3_conditions tt).
+        destruct (cse3_conditions params).
         2: discriminate.
         destruct (is_condition_present pc rel cond args).
         { rewrite COND_PRESENT_TRUE in H0 by trivial.
@@ -1214,3 +1216,4 @@ Proof.
 Qed.
 
 End PRESERVATION.
+End PARAMS.
-- 
cgit 


From 10f3467291b5a1e7ed195906eb23ef1ac57a0bd7 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:19:32 +0200
Subject: rename parameterized versions

---
 backend/CSE3.v      | 14 ++++++------
 backend/CSE3proof.v | 62 ++++++++++++++++++++++++++---------------------------
 2 files changed, 38 insertions(+), 38 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 5d05821a..f3a0af24 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -82,7 +82,7 @@ Definition find_cond_in_fmap fmap pc cond args :=
     end
   else None.
 
-Definition transf_instr (fmap : PMap.t RB.t)
+Definition param_transf_instr (fmap : PMap.t RB.t)
            (pc: node) (instr: instruction) :=
   match instr with
   | Iop op args dst s =>
@@ -118,7 +118,7 @@ Definition transf_instr (fmap : PMap.t RB.t)
   end.
 End REWRITE.
 
-Definition transf_function (f: function) : res function :=
+Definition param_transf_function (f: function) : res function :=
   do tenv <- type_function f;
   let (invariants, hints) := preanalysis tenv f in
   let ctx := context_from_hints hints in
@@ -127,15 +127,15 @@ Definition transf_function (f: function) : res function :=
     OK {| fn_sig := f.(fn_sig);
           fn_params := f.(fn_params);
           fn_stacksize := f.(fn_stacksize);
-          fn_code := PTree.map (transf_instr (ctx := ctx) invariants)
+          fn_code := PTree.map (param_transf_instr (ctx := ctx) invariants)
                                f.(fn_code);
           fn_entrypoint := f.(fn_entrypoint) |}
   else Error (msg "cse3: not inductive").
 
-Definition transf_fundef (fd: fundef) : res fundef :=
-  AST.transf_partial_fundef transf_function fd.
+Definition param_transf_fundef (fd: fundef) : res fundef :=
+  AST.transf_partial_fundef param_transf_function fd.
 
-Definition transf_program (p: program) : res program :=
-  transform_partial_program transf_fundef p.
+Definition param_transf_program (p: program) : res program :=
+  transform_partial_program param_transf_fundef p.
 
 End PARAMS.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 2d9992c6..2e9f99c5 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -32,10 +32,10 @@ Section PARAMS.
   Variable params : cse3params.
   
 Definition match_prog (p tp: RTL.program) :=
-  match_program (fun ctx f tf => transf_fundef params f = OK tf) eq p tp.
+  match_program (fun ctx f tf => param_transf_fundef params f = OK tf) eq p tp.
 
 Lemma transf_program_match:
-  forall p tp, transf_program params p = OK tp -> match_prog p tp.
+  forall p tp, param_transf_program params p = OK tp -> match_prog p tp.
 Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
@@ -113,7 +113,7 @@ Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
-    Genv.find_funct tge v = Some tf /\ transf_fundef params f = OK tf.
+    Genv.find_funct tge v = Some tf /\ param_transf_fundef params f = OK tf.
 Proof.
   apply (Genv.find_funct_transf_partial TRANSF).
 Qed.
@@ -122,7 +122,7 @@ Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef params f = OK tf.
+  Genv.find_funct_ptr tge b = Some tf /\ param_transf_fundef params f = OK tf.
 Proof.
   apply (Genv.find_funct_ptr_transf_partial TRANSF).
 Qed.
@@ -141,7 +141,7 @@ Proof.
 Qed.
 
 Lemma sig_preserved:
-  forall f tf, transf_fundef params f = OK tf -> funsig tf = funsig f.
+  forall f tf, param_transf_fundef params f = OK tf -> funsig tf = funsig f.
 Proof.
   destruct f; simpl; intros.
   - monadInv H.
@@ -156,7 +156,7 @@ Proof.
 Qed.
 
 Lemma stacksize_preserved:
-  forall f tf, transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f.
+  forall f tf, param_transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -168,7 +168,7 @@ Proof.
 Qed.
 
 Lemma params_preserved:
-  forall f tf, transf_function params f = OK tf -> fn_params tf = fn_params f.
+  forall f tf, param_transf_function params f = OK tf -> fn_params tf = fn_params f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -180,7 +180,7 @@ Proof.
 Qed.
 
 Lemma entrypoint_preserved:
-  forall f tf, transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f.
+  forall f tf, param_transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -192,7 +192,7 @@ Proof.
 Qed.
 
 Lemma sig_preserved2:
-  forall f tf, transf_function params f = OK tf -> fn_sig tf = fn_sig f.
+  forall f tf, param_transf_function params f = OK tf -> fn_sig tf = fn_sig f.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
   monadInv H.
@@ -204,7 +204,7 @@ Proof.
 Qed.
 
 Lemma transf_function_is_typable:
-  forall f tf, transf_function params f = OK tf ->
+  forall f tf, param_transf_function params f = OK tf ->
                exists tenv, type_function f = OK tenv.
 Proof.
   unfold transf_function; destruct f; simpl; intros.
@@ -213,7 +213,7 @@ Proof.
   assumption.
 Qed.
 Lemma transf_function_invariants_inductive:
-  forall f tf tenv, transf_function params f = OK tf ->
+  forall f tf tenv, param_transf_function params f = OK tf ->
     type_function f = OK tenv ->
     check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f))))
                         f tenv (fst (preanalysis tenv f)) = true.
@@ -230,7 +230,7 @@ Lemma find_function_translated:
   forall ros rs fd,
     find_function ge ros rs = Some fd ->
     exists tfd,
-      find_function tge ros rs = Some tfd /\ transf_fundef params fd = OK tfd.
+      find_function tge ros rs = Some tfd /\ param_transf_fundef params fd = OK tfd.
 Proof.
   unfold find_function; intros. destruct ros as [r|id].
   eapply functions_translated; eauto.
@@ -245,7 +245,7 @@ Inductive match_stackframes: list stackframe -> list stackframe -> signature ->
   | match_stackframes_cons:
       forall res f sp pc rs s tf ts sg tenv
         (STACKS: match_stackframes s ts (fn_sig tf))
-        (FUN: transf_function params f = OK tf)
+        (FUN: param_transf_function params f = OK tf)
         (WTF: type_function f = OK tenv)
         (WTRS: wt_regset tenv rs)
         (WTRES: tenv res = proj_sig_res sg)
@@ -262,7 +262,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s f sp pc rs m ts tf tenv
         (STACKS: match_stackframes s ts (fn_sig tf))
-        (FUN: transf_function params f = OK tf)
+        (FUN: param_transf_function params f = OK tf)
         (WTF: type_function f = OK tenv)
         (WTRS: wt_regset tenv rs)
         (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m),
@@ -271,7 +271,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_call:
       forall s f args m ts tf
         (STACKS: match_stackframes s ts (funsig tf))
-        (FUN: transf_fundef params f = OK tf)
+        (FUN: param_transf_fundef params f = OK tf)
         (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
       match_states (Callstate s f args m)
                    (Callstate ts tf args m)
@@ -296,10 +296,10 @@ Qed.
 
 Lemma transf_function_at:
   forall f tf pc tenv instr
-    (TF : transf_function params f = OK tf)
+    (TF : param_transf_function params f = OK tf)
     (TYPE : type_function f = OK tenv)
     (PC : (fn_code f) ! pc = Some instr),
-    (fn_code tf) ! pc = Some (transf_instr
+    (fn_code tf) ! pc = Some (param_transf_instr
        (ctx := (context_from_hints (snd (preanalysis tenv f))))
        params (fst (preanalysis tenv f))
        pc instr).
@@ -500,9 +500,9 @@ Proof.
       
   - (* Iop *)
     exists (State ts tf sp pc' (rs # res <- v) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity.
-      unfold transf_instr, find_op_in_fmap in instr'.
+    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
+      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity.
+      unfold param_transf_instr, find_op_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
@@ -583,9 +583,9 @@ Proof.
       (* END INVARIANT *)
   - (* Iload *)
     exists (State ts tf sp pc' (rs # dst <- v) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
-      unfold transf_instr, find_load_in_fmap in instr'.
+    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
+      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
+      unfold param_transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
@@ -661,9 +661,9 @@ Proof.
         
   - (* Iload notrap1 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
-      unfold transf_instr, find_load_in_fmap in instr'.
+    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+      unfold param_transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
@@ -737,9 +737,9 @@ Proof.
         
   - (* Iload notrap2 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
-      unfold transf_instr, find_load_in_fmap in instr'.
+    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+      unfold param_transf_instr, find_load_in_fmap in instr'.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
@@ -946,7 +946,7 @@ Proof.
     destruct (find_cond_in_fmap (ctx := ctx) params invs pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
     + econstructor; split.
       * eapply exec_Inop; try eassumption.
-        TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
+        TR_AT. unfold param_transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
       * replace bfound with b.
         { econstructor; eauto.
           (* BEGIN INVARIANT *)
@@ -1037,7 +1037,7 @@ Proof.
         discriminate.
    + econstructor; split.        
       * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
-        ** TR_AT. unfold transf_instr. fold invs. fold ctx.
+        ** TR_AT. unfold param_transf_instr. fold invs. fold ctx.
            rewrite FIND_COND.
            reflexivity.
         ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
-- 
cgit 


From 73741034932cebf4138d867678dca117fd1c8acd Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:29:25 +0200
Subject: make conditions a parameter in CSE3

---
 backend/CSE3.v      | 7 +++++++
 backend/CSE3proof.v | 8 +++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'backend')

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).
-- 
cgit 


From bd561273f2ff471f2d42552e20035b5ae5281453 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:37:49 +0200
Subject: make trivial ops parametric

---
 backend/CSE3.v      | 9 +++++----
 backend/CSE3proof.v | 4 ++--
 2 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 6cb43085..21067720 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -24,6 +24,7 @@ Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
 Record cse3params : Type :=
   mkcse3params
     { cse3_conditions : bool;
+      cse3_trivial_ops : bool;
     }.
 
 Section PARAMS.
@@ -63,7 +64,7 @@ Definition subst_args fmap pc xl :=
   forward_move_l_b (PMap.get pc fmap) xl.
 
 Definition find_cond_in_fmap fmap pc cond args :=
-  if cse3_conditions params
+  if params.(cse3_conditions)
   then
     match PMap.get pc fmap with
     | Some rel =>
@@ -88,7 +89,7 @@ Definition param_transf_instr (fmap : PMap.t RB.t)
   match instr with
   | Iop op args dst s =>
     let args' := subst_args fmap pc args in
-    match (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
+    match (if (negb params.(cse3_trivial_ops)) && (is_trivial_op op)
            then None else find_op_in_fmap fmap pc op args') with
     | None => Iop op args' dst s
     | Some src => Iop Omove (src::nil) dst s
@@ -142,7 +143,7 @@ Definition param_transf_program (p: program) : res program :=
 End PARAMS.
 
 Definition cmdline_params (_ : unit) :=
-  mkcse3params
-    (Compopts.optim_CSE3_conditions tt).
+  {| cse3_conditions := Compopts.optim_CSE3_conditions tt;
+     cse3_trivial_ops := Compopts.optim_CSE3_trivial_ops tt |}.
 
 Definition transf_program p := param_transf_program (cmdline_params tt) p.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 1168374a..3568f770 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -506,12 +506,12 @@ Proof.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
+      * destruct (if (negb (params.(cse3_trivial_ops))) && (is_trivial_op op)
                then None
                else
                 rhs_find pc (SOp op)
                   (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND.
-        ** destruct ((negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)). discriminate.
+        ** destruct ((negb (params.(cse3_trivial_ops))) && (is_trivial_op op)). discriminate.
            apply exec_Iop with (op := Omove) (args := r :: nil).
            TR_AT.
            subst instr'.
-- 
cgit 


From 7bcf7240186f670786c9daba0ffff768c180fd83 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 21:52:22 +0200
Subject: make operations cse3 parametric

---
 backend/CSE3.v      | 10 +++++++---
 backend/CSE3proof.v |  6 +++---
 2 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 21067720..54a8a3bc 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -24,7 +24,9 @@ Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
 Record cse3params : Type :=
   mkcse3params
     { cse3_conditions : bool;
-      cse3_trivial_ops : bool;
+      cse3_operations : bool;
+      cse3_loads      : bool;
+      cse3_trivial_ops: bool;
     }.
 
 Section PARAMS.
@@ -89,7 +91,7 @@ Definition param_transf_instr (fmap : PMap.t RB.t)
   match instr with
   | Iop op args dst s =>
     let args' := subst_args fmap pc args in
-    match (if (negb params.(cse3_trivial_ops)) && (is_trivial_op op)
+    match (if (negb params.(cse3_operations) || ((negb params.(cse3_trivial_ops)) && (is_trivial_op op)))
            then None else find_op_in_fmap fmap pc op args') with
     | None => Iop op args' dst s
     | Some src => Iop Omove (src::nil) dst s
@@ -144,6 +146,8 @@ End PARAMS.
 
 Definition cmdline_params (_ : unit) :=
   {| cse3_conditions := Compopts.optim_CSE3_conditions tt;
-     cse3_trivial_ops := Compopts.optim_CSE3_trivial_ops tt |}.
+     cse3_operations := true;
+     cse3_loads      := true;
+     cse3_trivial_ops:= Compopts.optim_CSE3_trivial_ops tt |}.
 
 Definition transf_program p := param_transf_program (cmdline_params tt) p.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 3568f770..a601d5d5 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -506,12 +506,12 @@ Proof.
       destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
       pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
                 (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct (if (negb (params.(cse3_trivial_ops))) && (is_trivial_op op)
+      * destruct (if (negb params.(cse3_operations) || (negb (params.(cse3_trivial_ops))) && (is_trivial_op op))
                then None
                else
                 rhs_find pc (SOp op)
                   (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND.
-        ** destruct ((negb (params.(cse3_trivial_ops))) && (is_trivial_op op)). discriminate.
+        ** destruct (negb params.(cse3_operations) || ((negb (params.(cse3_trivial_ops))) && (is_trivial_op op))). discriminate.
            apply exec_Iop with (op := Omove) (args := r :: nil).
            TR_AT.
            subst instr'.
@@ -985,7 +985,7 @@ Proof.
         unfold find_cond_in_fmap in FIND_COND.
         change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
         rewrite FIND_REL in FIND_COND.
-        destruct (cse3_conditions params).
+        destruct (params.(cse3_conditions)).
         2: discriminate.
         destruct (is_condition_present pc rel cond args).
         { rewrite COND_PRESENT_TRUE in H0 by trivial.
-- 
cgit 


From cb4ddeeeaca4736c2baceecec0511f8f99f465fc Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 22:04:34 +0200
Subject: more parameterization

---
 backend/CSE3.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 54a8a3bc..2f73a1a7 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -25,7 +25,6 @@ Record cse3params : Type :=
   mkcse3params
     { cse3_conditions : bool;
       cse3_operations : bool;
-      cse3_loads      : bool;
       cse3_trivial_ops: bool;
     }.
 
@@ -147,7 +146,6 @@ End PARAMS.
 Definition cmdline_params (_ : unit) :=
   {| cse3_conditions := Compopts.optim_CSE3_conditions tt;
      cse3_operations := true;
-     cse3_loads      := true;
      cse3_trivial_ops:= Compopts.optim_CSE3_trivial_ops tt |}.
 
 Definition transf_program p := param_transf_program (cmdline_params tt) p.
-- 
cgit