diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:32:32 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-13 14:32:32 +0100 |
| commit | 147fe13100aaacbd0906194f53a140373a7006d3 (patch) | |
| tree | 0b033dc1ffc44fc46937cccec5039537aa242e79 /powerpc | |
| parent | f2cf6d4e0600d4a58677a7531e8516a37fe1d0da (diff) | |
| parent | 40360396c621603af3ea6fb9a2fc89fa7945c79a (diff) | |
| download | compcert-kvx-147fe13100aaacbd0906194f53a140373a7006d3.tar.gz compcert-kvx-147fe13100aaacbd0906194f53a140373a7006d3.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 2 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b9300fd7..4fb38ff8 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -864,7 +864,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pisel rd r1 r2 bit => let v := match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1 + | Vint n => if Int.eq n Int.zero then rs#r2 else (gpr_or_zero rs r1) | _ => Vundef end in Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 884d5366..20cf9c1d 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1284,7 +1284,9 @@ Proof. reflexivity. + Simpl. rewrite <- (C r1), <- (C r2) by auto. - rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + rewrite B, gpr_or_zero_not_zero. + destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + destruct dir; intros e; subst; discriminate. + intros. Simpl. Qed. |