Fix lowering proofs

jasmin-lang · Mar 12, 2024 · fbec7b1 · fbec7b1
1 parent e4993a2
commit fbec7b1
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 22 deletions.
diff --git a/proofs/compiler/arm_lowering.v b/proofs/compiler/arm_lowering.v
@@ -74,8 +74,8 @@ Definition flags_of_mn (mn : arm_mnemonic) : seq var :=
   in
   map (fun x => x fv) ids.
 
-Definition lflags_of_mn (mn : arm_mnemonic) : seq lval :=
-  to_lvals (flags_of_mn mn).
+Definition lflags_of_mn (vi : var_info) (mn : arm_mnemonic) : seq lval :=
+  [seq Lvar {| v_var := x; v_info := vi; |} | x <- flags_of_mn mn ].
 
 Definition lower_TST (e0 e1 : pexpr) : option (seq pexpr) :=
   match e0, e1 with
@@ -87,13 +87,16 @@ Definition lower_TST (e0 e1 : pexpr) : option (seq pexpr) :=
 
 (* TODO_ARM: CMP and TST take register shifts. *)
 Definition lower_condition_Papp2
-  (vi : var_info) (op : sop2) (e0 e1 : pexpr) : option (arm_mnemonic * pexpr * seq pexpr) :=
+  (vi : var_info)
+  (op : sop2)
+  (e0 e1 : pexpr) :
+  option (arm_mnemonic * pexpr * seq pexpr) :=
   let%opt (cf, ws) := cf_of_condition op in
   let%opt _ := chk_ws_reg ws in
   let cmp := (CMP, pexpr_of_cf cf vi (fresh_flags fv), [:: e0; e1 ]) in
   match op with
   | Oeq (Op_w _) =>
-      let zf_var := {| v_var := (fvZF fv); v_info := vi |} in
+      let zf_var := {| v_var := fvZF fv; v_info := vi |} in
       let eZF := Pvar (mk_lvar zf_var) in
       Some (if lower_TST e0 e1 is Some es then (TST, eZF, es) else cmp)
   | Oneq (Op_w _)
@@ -109,7 +112,7 @@ Definition lower_condition_pexpr
   (vi : var_info) (e : pexpr) : option (seq lval * sopn * seq pexpr * pexpr) :=
   let%opt (op, e0, e1) := is_Papp2 e in
   let%opt (mn, e', es) := lower_condition_Papp2 vi op e0 e1 in
-  Some (lflags_of_mn mn, Oarm (ARM_op mn default_opts), es, e').
+  Some (lflags_of_mn vi mn, Oarm (ARM_op mn default_opts), es, e').
 
 Definition lower_condition (vi: var_info) (e : pexpr) : seq instr_r * pexpr :=
   if lower_condition_pexpr vi e is Some (lvs, op, es, c)

diff --git a/proofs/compiler/arm_lowering_proof.v b/proofs/compiler/arm_lowering_proof.v
@@ -176,15 +176,15 @@ Proof.
   all: by move: fvars_NF fvars_ZF fvars_CF fvars_VF.
 Qed.
 
-Lemma sem_condition_mn ii tag mn s es ws0 ws1 (w0 : word ws0) (w1 : word ws1) :
+Lemma sem_condition_mn ii vi tag mn s es ws0 ws1 (w0 : word ws0) (w1 : word ws1) :
   mn \in condition_mnemonics
   -> (reg_size <= ws0)%CMP
   -> (reg_size <= ws1)%CMP
   -> sem_pexprs true (p_globs p) s es = ok [:: Vword w0; Vword w1 ]
   -> let w0' := zero_extend reg_size w0 in
      let w1' := zero_extend reg_size w1 in
      let aop := Oarm (ARM_op mn default_opts) in
-     let i := Copn (lflags_of_mn fv mn) tag aop es in
+     let i := Copn (lflags_of_mn fv vi mn) tag aop es in
      sem p' ev s [:: MkI ii i ] (estate_of_condition_mn mn s w0' w1').
 Proof.
   move=> hmn hws0 hws1 hsemes /=.
@@ -211,8 +211,8 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma lower_condition_Papp2P s op e0 e1 mn e es v0 v1 v :
-  lower_condition_Papp2 fv op e0 e1 = Some (mn, e, es)
+Lemma lower_condition_Papp2P vi s op e0 e1 mn e es v0 v1 v :
+  lower_condition_Papp2 fv vi op e0 e1 = Some (mn, e, es)
   -> sem_pexpr true (p_globs p) s e0 = ok v0
   -> sem_pexpr true (p_globs p) s e1 = ok v1
   -> sem_sop2 op v0 v1 = ok v
@@ -334,8 +334,8 @@ Proof.
   by rewrite -word.wltuE leNgt.
 Qed.
 
-Lemma sem_lower_condition_pexpr tag s0 s0' ii e v lvs aop es c :
-  lower_condition_pexpr fv e = Some (lvs, aop, es, c)
+Lemma sem_lower_condition_pexpr vi tag s0 s0' ii e v lvs aop es c :
+  lower_condition_pexpr fv vi e = Some (lvs, aop, es, c)
   -> eq_fv s0' s0
   -> disj_fvars (read_e e)
   -> sem_pexpr true (p_globs p) s0 e = ok v
@@ -359,7 +359,7 @@ Proof.
     lower_condition_Papp2P h hsem0' hsem1' hsemop.
   clear h hsemop hsem0' hsem1'.
 
-  have /= hsem' := sem_condition_mn ii tag hmn hws0 hws1 hsemes.
+  have /= hsem' := sem_condition_mn ii vi tag hmn hws0 hws1 hsemes.
   clear hws0 hws1 hsemes.
 
   eexists;
@@ -370,8 +370,8 @@ Proof.
   exact: (estate_of_condition_mn_eq_fv s0' _ _ hmn).
 Qed.
 
-Lemma sem_lower_condition s0 s0' ii e v pre e' :
-  lower_condition fv e = (pre, e')
+Lemma sem_lower_condition vi s0 s0' ii e v pre e' :
+  lower_condition fv vi e = (pre, e')
   -> eq_fv s0' s0
   -> disj_fvars (read_e e)
   -> sem_pexpr true (p_globs p) s0 e = ok v
@@ -1048,8 +1048,8 @@ Lemma no_preP o pre aop es :
 Proof. case: o => //. by move=> [? ?] [<- <- <-]. Qed.
 
 Lemma sem_lower_pexpr
-  s0 s1 s0' ii ws ws' e pre aop es (w : word ws') lv tag :
-  lower_pexpr ws e = Some (pre, aop, es)
+  s0 s1 s0' ii vi ws ws' e pre aop es (w : word ws') lv tag :
+  lower_pexpr vi ws e = Some (pre, aop, es)
   -> eq_fv s0' s0
   -> (ws <= ws')%CMP
   -> disj_fvars (read_e e)

diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86_lowering_proof.v
@@ -282,7 +282,7 @@ Section PROOF.
     to_word ws v1 = ok w1 ->
     exists s',
       let: i := Copn lflags AT_none (Ox86 (CMP ws)) [:: e0; e1 ] in
-      let: e := pexpr_of_cf cf [:: vof; vcf; vsf; vzf ] in
+      let: e := pexpr_of_cf cf vi [:: vof; vcf; vsf; vzf ] in
       let: b := sem_combine_flags cf bof bcf bsf bzf in
       [/\ sem p' ev s [:: MkI ii i ] s'
         , eq_exc_fresh s' s
@@ -1358,7 +1358,8 @@ Section PROOF.
       move: x Hcond=> [i e'] Hcond.
       clear s2' Hw' Hs2'.
       move: Hv' => /=; t_xrbindP=> b bv Hbv Hb trv1 v1 Hv1 Htr1 trv2 v2 Hv2 Htr2 ?;subst v.
-      have [s2' [Hs2'1 Hs2'2 Hs2'3]] := lower_condition_corr ii Hcond Hs1' Hbv.
+      have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
+        lower_condition_corr ii Hcond Hs1' Hbv.
       have [s3' Hw' Hs3'] := eeq_exc_write_lval Hdisjl Hs2'2 Hw.
       exists s3'; split=> //.
       rewrite map_cat.
@@ -1746,7 +1747,7 @@ Section PROOF.
     move=> s1 s2 e c1 c2 Hz _ Hc ii /= Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_if=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
       lower_condition_corr ii Hcond Hs1' (eeq_exc_sem_pexpr Hdisje Hs1' Hz).
@@ -1765,7 +1766,7 @@ Section PROOF.
     move=> s1 s2 e c1 c2 Hz _ Hc ii /= Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_if=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2 Hs2'3]] :=
       lower_condition_corr ii Hcond Hs1' (eeq_exc_sem_pexpr Hdisje Hs1' Hz).
@@ -1784,7 +1785,7 @@ Section PROOF.
     move=> s1 s2 s3 s4 a c e c' _ Hc Hz _ Hc' _ Hwhile ii Hdisj s1' Hs1' /=.
     have := Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_while=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2]] := Hc Hc1 _ Hs1'.
     have [s3' [Hs3'1 Hs3'2 Hs3'3]] :=
@@ -1811,7 +1812,7 @@ Section PROOF.
     move=> s1 s2 a c e c' _ Hc Hz ii Hdisj s1' Hs1' /=.
     move: Hdisj; rewrite /disj_fvars /x86_lowering.disj_fvars vars_I_while=> /disjoint_union [Hdisje /disjoint_union [Hc1 Hc2]].
     set x := lower_condition _ _ _.
-    have Hcond: x = lower_condition fv dummy_var_info e by [].
+    have Hcond: x = lower_condition fv (var_info_of_ii ii) e by [].
     move: x Hcond=> [i e'] Hcond.
     have [s2' [Hs2'1 Hs2'2]] := Hc Hc1 _ Hs1'.
     have [s3' [Hs3'1 Hs3'2 Hs3'3]] :=