From 373ad4a6efcb6cd0ecd30e7c131640b9783f1269 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 20 Dec 2020 14:30:47 +0100 Subject: Fix the Asmblock/Asm proof --- aarch64/Asmblockdeps.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index f5dd46ee..670a7d06 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1051,8 +1051,7 @@ Definition trans_control (ctl: control) : inst := | Ptbz sz r n lbl => [(#PC, Op (Control (Otbz sz n lbl)) (PReg(#r) @ PReg(#PC) @ Enil))] | Pbtbl r tbl => [(#X16, Op (Constant Vundef) Enil); (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil)); - (#X16, Op (Constant Vundef) Enil); - (#X17, Op (Constant Vundef) Enil)] + (#X16, Op (Constant Vundef) Enil)] | Pbuiltin ef args res => [] end. @@ -1923,10 +1922,9 @@ Proof. try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz)); try reflexivity; discriminate_ppos. Simpl sr. destruct (PregEq.eq X16 rr); [ subst; Simpl_update |]; - destruct (PregEq.eq X17 rr); [ subst; Simpl_update |]; destruct (PregEq.eq PC rr); [ subst; Simpl_update |]. rewrite !Pregmap.gso; auto; - apply ppos_discr in n0; apply ppos_discr in n1; apply ppos_discr in n2; + apply ppos_discr in n0; apply ppos_discr in n1; rewrite !assign_diff; auto. Qed. @@ -2044,11 +2042,11 @@ Proof. Qed. Lemma incrPC_undef_regs_commut l : forall d rs, - incrPC d (undef_regs (map preg_of l) rs) = undef_regs (map preg_of l) (incrPC d rs). + incrPC d (undef_regs l rs) = undef_regs l (incrPC d rs). Proof. induction l; simpl; auto. intros. rewrite IHl. unfold incrPC. - destruct (PregEq.eq (preg_of a) PC). + destruct (PregEq.eq a PC). - rewrite e. rewrite Pregmap.gss. simpl. apply f_equal. unfold Pregmap.set. apply functional_extensionality. intros x. @@ -2056,7 +2054,9 @@ Proof. - rewrite Pregmap.gso; auto. apply f_equal. unfold Pregmap.set. apply functional_extensionality. intros x. - destruct (PregEq.eq x PC); subst; auto. + destruct (PregEq.eq x PC). + + subst. destruct a; simpl; auto. congruence. + + auto. Qed. Lemma bblock_simu_reduce: -- cgit