diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-02 17:13:50 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-02 17:13:50 +0100 |
| commit | 241da496839a9101e843ce7b1da4a668f998498a (patch) | |
| tree | eafa2250ce4f5a8bb96e16afa6ebd9a7149e9435 /aarch64/Asm.v | |
| parent | 8de1a1f5811470bc1d7d1a7b2f0e5193de40698e (diff) | |
| download | compcert-kvx-241da496839a9101e843ce7b1da4a668f998498a.tar.gz compcert-kvx-241da496839a9101e843ce7b1da4a668f998498a.zip | |
Preparation for postpass in aarch64 and refactoring
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 22ab0222..5dafb01f 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -77,8 +77,8 @@ Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. Inductive dreg : Type := - | IR': iregsp -> dreg (**r 64- or 32-bit integer registers *) - | FR': freg -> dreg. (**r double- or single-precision float registers *) + | IR: iregsp -> dreg (**r 64- or 32-bit integer registers *) + | FR: freg -> dreg. (**r double- or single-precision float registers *) (** We model the following registers of the ARM architecture. *) @@ -88,8 +88,8 @@ Inductive preg: Type := | PC: preg. (**r program counter *) (* XXX: ireg no longer coerces to preg *) -Coercion IR': iregsp >-> dreg. -Coercion FR': freg >-> dreg. +Coercion IR: iregsp >-> dreg. +Coercion FR: freg >-> dreg. Coercion DR: dreg >-> preg. Definition SP:preg := XSP. Coercion CR: crbit >-> preg. @@ -108,7 +108,7 @@ End PregEq. Module Pregmap := EMap(PregEq). Definition preg_of_iregsp (r: iregsp) : preg := - match r with RR1 r => IR' r | XSP => SP end. + match r with RR1 r => IR r | XSP => SP end. (** Conventional name for return address ([RA]) *) @@ -359,7 +359,7 @@ Definition regset := Pregmap.t val. or 0. *) Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val := - match r with RR0 r => rs (IR' r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. + match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. (** Concise notations for accessing and updating the values of registers. *) @@ -1357,10 +1357,10 @@ Qed. Definition data_preg (r: preg) : bool := match r with - | DR (IR' X16) => false - | DR (IR' X30) => false - | DR (IR' _) => true - | DR (FR' _) => true + | DR (IR X16) => false + | DR (IR X30) => false + | DR (IR _) => true + | DR (FR _) => true | CR _ => false (* | SP => true; subsumed by IR (iregsp) *) | PC => false |