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 | |
| parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
| download | compcert-f1637021cd51505796e878a21d1b30df0b42e236.tar.gz compcert-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')
| -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. |