diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-20 14:30:47 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-20 14:30:47 +0100 |
| commit | 373ad4a6efcb6cd0ecd30e7c131640b9783f1269 (patch) | |
| tree | dc555a7401a74790f629aae02bb919834e1faf94 /aarch64/Asmblockdeps.v | |
| parent | 32abc8049ce030f0e338f526f7d16c585d84025f (diff) | |
| download | compcert-kvx-373ad4a6efcb6cd0ecd30e7c131640b9783f1269.tar.gz compcert-kvx-373ad4a6efcb6cd0ecd30e7c131640b9783f1269.zip | |
Fix the Asmblock/Asm proof
Diffstat (limited to 'aarch64/Asmblockdeps.v')
| -rw-r--r-- | aarch64/Asmblockdeps.v | 14 |
1 files changed, 7 insertions, 7 deletions
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: |