Prove exec_body_dont_move_PC

Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be
a misnomer since not all iregs are data regs)
TODO: Adjust names of PArithP, PArithPP and the like

1 files changed, 39 insertions, 32 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index be776323..8f859d55 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -21,7 +21,7 @@ WORK IN PROGRESS: we want to define an Asmblock syntax, with an Asmblock semanti
 (e.g. we don't need the parallel semantics of Asmvliw)
 
 
-NOTE: this file is inspired from 
+NOTE: this file is inspired from
    - aarch64/Asm.v
    - kvx/Asmvliw.v (only the Asmblock syntax)
    - kvx/Asmblock.v
@@ -88,22 +88,29 @@ Inductive crbit: Type :=
 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 *)
+
 (** We model the following registers of the ARM architecture. *)
 
 Inductive preg: Type :=
-  | IR: iregsp -> preg   (**r 64- or 32-bit integer registers *)
-  | FR: freg -> preg     (**r double- or single-precision float registers *)
+  | DR: dreg -> preg     (** see dreg **)
   | CR: crbit -> preg    (**r bits in the condition register *)
   | PC: preg.            (**r program counter *)
 
 (* XXX: ireg no longer coerces to preg *)
-Coercion IR: iregsp >-> preg.
+Coercion IR': iregsp >-> dreg.
+Coercion FR': freg >-> dreg.
+Coercion DR: dreg >-> preg.
 Definition SP:preg := XSP.
-Coercion FR: freg >-> preg.
 Coercion CR: crbit >-> preg.
 
+Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}.
+Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined.
+
 Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply iregsp_eq. apply freg_eq. apply crbit_eq. Defined.
+Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined.
 
 Module PregEq.
   Definition t := preg.
@@ -113,7 +120,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]) *)
 
@@ -182,7 +189,7 @@ Inductive extend_op: Type :=
    see example of loads below.
 *)
 
-(** Control Flow instructions 
+(** Control Flow instructions
 
 *)
 Inductive cf_instruction : Type :=
@@ -199,7 +206,7 @@ Inductive cf_instruction : Type :=
   | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label)                  (**r branch if bit n is zero *)
   (** Pseudo-instructions *)
   | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
-  . 
+  .
 
 (*
 A builtin is considered as a control-flow instruction, because it could emit a trace (cf. Machblock semantics).
@@ -217,8 +224,8 @@ Coercion PCtlFlow: cf_instruction >-> control.
 
 (** Basic instructions *)
 
-(* Loads waiting for (rd: preg) (a: addressing) 
- * XXX Use preg because exec_load is defined in terms of it, thus allowing us to
+(* Loads waiting for (rd: dreg) (a: addressing)
+ * XXX Use dreg because exec_load is defined in terms of it, thus allowing us to
  * treat integer and floating point loads the same. *)
 Inductive load_rd_a: Type :=
   (* Integer load *)
@@ -239,7 +246,7 @@ Inductive load_rd_a: Type :=
   .
 
 (* Actually, Pldp is not used in the aarch64/Asm semantics!
- 
+
 Thus we skip this particular case:
 
 Inductive ld_instruction: Type :=
@@ -426,9 +433,9 @@ Inductive arith_arrrr0 : Type :=
  *             Instead, the condition register is mutated.
  *)
 Inductive ar_instruction : Type :=
-  | PArithP (i : arith_p) (rd : preg)
-  | PArithPP (i : arith_pp) (rd rs : preg)
-  | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
+  | PArithP (i : arith_p) (rd : dreg)
+  | PArithPP (i : arith_pp) (rd rs : dreg)
+  | PArithPPP (i : arith_ppp) (rd r1 r2 : dreg)
   | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0)
   | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
@@ -436,24 +443,24 @@ Inductive ar_instruction : Type :=
   | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *)
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
   | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *)
-  | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
+  | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : dreg)
   | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
+  | PArithComparisonP (i : arith_comparison_p) (r1 : dreg)
   (* Instructions without indirection sine they would be the only ones *)
   (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *)
   | Pcset (rd : ireg) (c : testcond)                                  (**r set to 1/0 if cond is true/false *)
   (* PArithFR0 *)
   | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)                     (**r copy int reg to FP reg *)
   (* PArithCPPP *)
-  | Pcsel (rd r1 r2 : preg) (c : testcond)                            (**r int/float conditional move *)
+  | Pcsel (rd r1 r2 : dreg) (c : testcond)                            (**r int/float conditional move *)
   (* PArithAFFF *)
   | Pfnmul (fsz : fsize) (rd r1 r2 : freg)                            (**r multiply-negate *)
 .
 
 Inductive basic : Type :=
   | PArith (i: ar_instruction)                                        (**r TODO *)
-  | PLoad (ld: load_rd_a) (rd: preg) (a: addressing)                  (**r TODO *)
-  | PStore (st: store_rs_a) (r: preg) (a: addressing)                 (**r TODO *)
+  | PLoad (ld: load_rd_a) (rd: dreg) (a: addressing)                  (**r TODO *)
+  | PStore (st: store_rs_a) (r: dreg) (a: addressing)                 (**r TODO *)
   | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
   | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
   | Ploadsymbol (rd: ireg) (id: ident)                                (**r load the address of [id] *)
@@ -694,7 +701,7 @@ Definition genv := Genv.t fundef unit.
     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. *)
 
@@ -735,7 +742,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
 
-(** See "Parameters" of the same names in Asm.v *) 
+(** See "Parameters" of the same names in Asm.v *)
 Record aarch64_linker: Type := {
   symbol_low: ident -> ptrofs -> val;
   symbol_high: ident -> ptrofs -> val
@@ -759,7 +766,7 @@ Definition Next rs m: outcome := Some (State rs m).
 Definition Stuck: outcome := None.
 Local Open Scope option_monad_scope.
 
-(* a few lemma on comparisons of unsigned (e.g. pointers) 
+(* a few lemma on comparisons of unsigned (e.g. pointers)
 
 TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
 *)
@@ -963,7 +970,7 @@ Definition eval_addressing (a: addressing) (rs: regset): val :=
 (** Auxiliaries for memory accesses *)
 
 Definition exec_load (chunk: memory_chunk) (transf: val -> val)
-                     (a: addressing) (r: preg) (rs: regset) (m: mem) :=
+                     (a: addressing) (r: dreg) (rs: regset) (m: mem) :=
   SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN
   Next (rs#r <- (transf v)) m.
 
@@ -1034,12 +1041,12 @@ Definition float64_of_bits (v: val): val :=
   | _ => Vundef
   end.
 
-(** execution of loads 
+(** execution of loads
 *)
 
 Definition chunk_load_rd_a (ld: load_rd_a): memory_chunk :=
   match ld with
-  | Pldrw => Mint32 
+  | Pldrw => Mint32
   | Pldrw_a => Many32
   | Pldrx => Mint64
   | Pldrx_a => Many64
@@ -1094,13 +1101,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool :=
   if in_dec lbl (header bb) then true else false.
 
 Lemma is_label_correct_true lbl bb:
-  List.In lbl (header bb) <-> is_label lbl bb = true. 
+  List.In lbl (header bb) <-> is_label lbl bb = true.
 Proof.
   unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
 Qed.
 
 Lemma is_label_correct_false lbl bb:
-  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
+  ~(List.In lbl (header bb)) <-> is_label lbl bb = false.
 Proof.
   unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
 Qed.
@@ -1119,7 +1126,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
   | _ => Stuck
   end.
 
-(** Evaluating a branch 
+(** Evaluating a branch
 
 Warning: PC is assumed to be already pointing on the next instruction !
 
@@ -1879,7 +1886,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfnmadd _ _ _ _ _
   | Pfnmsub _ _ _ _ _
   | Pnop
-  | Pcfi_adjust _ 
+  | Pcfi_adjust _
   | Pcfi_rel_offset _ =>
       Stuck
   end.
@@ -1956,7 +1963,7 @@ Definition loc_external_result (sg: signature) : rpair preg :=
 Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
   | nil => Next rs m
-  | bi::body' => 
+  | bi::body' =>
      SOME o <- exec_basic bi rs m IN
      exec_body body' (_rs o) (_m o)
   end.
@@ -1986,7 +1993,7 @@ Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace)
 Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
   match lb with
   | nil => None
-  | b :: il => 
+  | b :: il =>
     if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
     else if zeq pos 0 then Some b
     else find_bblock (pos - (size b)) il