diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-17 19:44:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-17 19:44:22 +0200 |
| commit | f1637021cd51505796e878a21d1b30df0b42e236 (patch) | |
| tree | 9d87ecd26f560cee6be1f0a1fe410d4d6d0f4609 /powerpc/Asmgenproof1.v | |
| parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
| download | compcert-kvx-f1637021cd51505796e878a21d1b30df0b42e236.tar.gz compcert-kvx-f1637021cd51505796e878a21d1b30df0b42e236.zip | |
Model GPR0 in isel (#199)
If the first argument to `isel` is GPR0, it reads as the constant 0.
This cannot occur in code generated by CompCert, due to the fact that
GPR0 is not available as register for register allocation. However the
assembler semantics should be as close as possible to the actual
hardware.
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
1 files changed, 3 insertions, 1 deletions
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. |