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

4 files changed, 112 insertions, 42 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index dc1faddd..4de1a9d0 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -836,10 +836,10 @@ Qed.
 
 Definition data_preg (r: preg) : bool :=
   match r with
-  | IR X16 => false
-  | IR X30 => false
-  | IR _ => true
-  | 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
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
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index e1a38c45..4e81a936 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -30,19 +30,19 @@ Module Asmblock_TRANSF.
 
 Definition ireg_of_preg (p : Asmblock.preg) : res ireg :=
   match p with
-  | IR (RR1 r) => OK r
+  | DR (IR' (RR1 r)) => OK r
   | _ => Error (msg "Asmgen.ireg_of_preg")
   end.
 
 Definition freg_of_preg (p : Asmblock.preg) : res freg :=
   match p with
-  | FR r => OK r
+  | DR (FR' r) => OK r
   | _ => Error (msg "Asmgen.freg_of_preg")
   end.
 
 Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp :=
   match p with
-  | IR r => OK r
+  | DR (IR' r) => OK r
   | _ => Error (msg "Asmgen.iregsp_of_preg")
   end.
 
@@ -219,11 +219,11 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
   | PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1)
   | PArith (Pcsel rd r1 r2 c) =>
       match r1, r2 with
-      | IR r1', IR r2' => do rd' <- ireg_of_preg rd;
+      | IR' r1', IR' r2' => do rd' <- ireg_of_preg rd;
                           do r1'' <- ireg_of_preg r1';
                           do r2'' <- ireg_of_preg r2';
                           OK (Asm.Pcsel rd' r1'' r2'' c)
-      | FR r1', IR r2' => do rd' <- freg_of_preg rd;
+      | FR' r1', IR' r2' => do rd' <- freg_of_preg rd;
                           do r1'' <- freg_of_preg r1';
                           do r2'' <- freg_of_preg r2';
                           OK (Asm.Pfsel rd' r1'' r2'' c)
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 2ee33568..5092d99b 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -913,10 +913,73 @@ Proof.
     eapply plus_star; eauto.
 Qed.
 
+Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
+  (BASIC: exec_arith_instr lk ai rs = rs'),
+  rs PC = rs' PC.
+Proof.
+  destruct ai; simpl; intros;
+  try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate).
+  - destruct i; simpl in BASIC.
+    + unfold compare_long in BASIC; rewrite <- BASIC.
+      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
+    + unfold compare_long in BASIC; rewrite <- BASIC.
+      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
+    + destruct sz;
+      try (unfold compare_single in BASIC || unfold compare_float in BASIC);
+      destruct (rs r1), (rs r2);
+      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC; destruct is;
+      try (unfold compare_int in BASIC || unfold compare_long in BASIC);
+      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC; destruct sz;
+    try (unfold compare_single in BASIC || unfold compare_float in BASIC);
+    destruct (rs r1);
+    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
+  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
+Qed.
+
+Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
+  (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
+  rs PC = rs' PC.
+Proof.
+  destruct bi; simpl; intros.
+  - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto.
+  - unfold exec_load in BASIC.
+    destruct Mem.loadv. 2: { discriminate BASIC. }
+    inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+  - unfold exec_store in BASIC.
+    destruct Mem.storev. 2: { discriminate BASIC. }
+    inv BASIC; reflexivity.
+  - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. }
+    inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity.
+  - destruct Mem.loadv. 2: { discriminate BASIC. }
+    destruct rs, Mem.free; try discriminate BASIC.
+    inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+Qed.
+
+Lemma exec_body_dont_move_PC_aux:
+  forall bis rs m rs' m'
+  (BODY: exec_body lk ge bis rs m = Next rs' m'),
+  rs PC = rs' PC.
+Proof.
+  induction bis.
+  - intros; inv BODY; reflexivity.
+  - simpl; intros.
+    remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. }
+    symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI.
+    exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC.
+    eapply IHbis; eauto.
+Qed.
+
 Lemma exec_body_dont_move_PC bb rs m rs' m': forall
   (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
   rs PC = rs' PC.
-Admitted.
+Proof. apply exec_body_dont_move_PC_aux. Qed.
 
 Lemma list_nth_z_range_exceeded A (l : list A) n:
   n >= list_length_z l ->