AB: removing bregs

5 files changed, 73 insertions, 97 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 2720f3e5..f066a1a2 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -63,34 +63,18 @@ Proof. decide equality. Defined.
 (** We model the following registers of the RISC-V architecture. *)
 
 (** basic register *)
-Inductive breg: Type :=
-  | IR: gpreg -> breg                   (**r integer registers *)
-  | FR: gpreg -> breg                   (**r float registers   *)
-  | RA: breg
-  .
-
-Coercion IR: gpreg >-> breg.
-Coercion FR: gpreg >-> breg.
-
-Lemma breg_eq: forall (x y: breg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_eq. Defined.
-
-
-Module BregEq.
-  Definition t  := breg.
-  Definition eq := breg_eq.
-End BregEq.
-
-Module Bregmap := EMap(BregEq).
-
 Inductive preg: Type :=
-  | BaR: breg -> preg                   (**r basic registers   *)
-  | PC: preg.                           (**r program counter   *)
+  | IR: gpreg -> preg                   (**r integer registers *)
+  | FR: gpreg -> preg                   (**r float registers   *)
+  | RA: preg
+  | PC: preg
+  .
 
-Coercion BaR: breg >-> preg.
+Coercion IR: gpreg >-> preg.
+Coercion FR: gpreg >-> preg.
 
 Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply breg_eq. Defined.
+Proof. decide equality. apply ireg_eq. apply freg_eq. Defined.
 
 Module PregEq.
   Definition t  := preg.
@@ -378,8 +362,8 @@ Inductive basic : Type :=
   | PStore          (i: st_instruction)
   | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
   | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
-  | Pget    (rd: ireg) (rs: breg)                   (**r get system register *)
-  | Pset    (rd: breg) (rs: ireg)                   (**r set system register *)
+  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
+  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
   | Pnop                                            (**r virtual instruction that does nothing *)
 .
 
@@ -514,42 +498,29 @@ Qed.
   type [Tint] or [Tlong] (in 64 bit mode),
   and float registers to values of type [Tsingle] or [Tfloat]. *)
 
-Definition bregset := Bregmap.t val.
 Definition regset := Pregmap.t val.
 
-Definition bregset_cast (rs: regset): bregset
-  := fun r => rs (BaR r).
-
-Coercion bregset_cast: regset >->  bregset.
-
 Definition genv := Genv.t fundef unit.
 
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a # b <- c" := (Bregmap.set b c a) (at level 1, b at next level) : asm.
-Notation "a # b <-- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
 
 Open Scope asm.
 
-Definition pregs_to_bregs {A} (rs: Pregmap.t A): (Bregmap.t A)
-  := fun r => rs (BaR r).
-
-Definition update_pregs {A} (rs1: Pregmap.t A) (rs2:Bregmap.t A): Pregmap.t A 
-  := fun r => match r with BaR r => rs2 r | _ => rs1 r end.
-
 (** Undefining some registers *)
 
 Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
   match l with
   | nil => rs
-  | r :: l' => undef_regs l' (rs#r <-- Vundef)
+  | r :: l' => undef_regs l' (rs#r <- Vundef)
   end.
 
 
 (** Assigning a register pair *)
 Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   match p with
-  | One r => rs#r <-- v
-  | Twolong rhi rlo => rs#rhi <-- (Val.hiword v) #rlo <-- (Val.loword v)
+  | One r => rs#r <- v
+  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
   end.
 
 (* TODO: Is it still useful ?? *)
@@ -567,7 +538,7 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
 
 Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
-  | BR r => rs#r <-- v
+  | BR r => rs#r <- v
   | BR_none => rs
   | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
@@ -713,7 +684,7 @@ FIXME: replace parameter "m" by a function corresponding to the resul of "(Mem.v
 Variable ge: genv.
 
 
-Definition exec_arith_instr (ai: ar_instruction) (rs: bregset) (m: mem) : bregset :=
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset :=
   match ai with
   | PArithR n d =>
       match n with
@@ -817,15 +788,15 @@ Definition eval_offset (ofs: offset) : ptrofs :=
   | Ofslow id delta => low_half ge id delta
   end.
 
-Definition exec_load (chunk: memory_chunk) (rs: bregset) (m: mem)
-                     (d: breg) (a: ireg) (ofs: offset) :=
+Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
+                     (d: ireg) (a: ireg) (ofs: offset) :=
   match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with
   | None => Stuck
   | Some v => Next (rs#d <- v) m
   end.
 
-Definition exec_store (chunk: memory_chunk) (rs: bregset) (m: mem)
-                      (s: breg) (a: ireg) (ofs: offset) :=
+Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
+                      (s: ireg) (a: ireg) (ofs: offset) :=
   match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with
   | None => Stuck
   | Some m' => Next rs m'
@@ -833,7 +804,7 @@ Definition exec_store (chunk: memory_chunk) (rs: bregset) (m: mem)
 
 (** * basic instructions *)
 
-Definition exec_basic_instr (bi: basic) (rs: bregset) (m: mem) : outcome bregset :=
+Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :=
  match bi with
  | PArith ai => Next (exec_arith_instr ai rs m) m
 
@@ -897,7 +868,7 @@ Definition exec_basic_instr (bi: basic) (rs: bregset) (m: mem) : outcome bregset
   | Pnop => Next rs m
 end.
 
-Fixpoint exec_body (body: list basic) (rs: bregset) (m: mem): outcome bregset :=
+Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome regset :=
   match body with
   | nil => Next rs m
   | bi::body' => 
@@ -911,7 +882,7 @@ Fixpoint exec_body (body: list basic) (rs: bregset) (m: mem): outcome bregset :=
   instruction ([nextblock]) or branching to a label ([goto_label]). *)
 
 Definition nextblock (b:bblock) (rs: regset) :=
-  rs#PC <-- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))).
+  rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))).
 
 (** Looking up bblocks in a code sequence by position. *)
 Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
@@ -962,7 +933,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome
   | None => Stuck
   | Some pos =>
       match rs#PC with
-      | Vptr b ofs => Next (rs#PC <-- (Vptr b (Ptrofs.repr pos))) m
+      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
       | _          => Stuck
       end
   end.
@@ -1003,11 +974,11 @@ Definition exec_control (f: function) (ic: control) (rs: regset) (m: mem) : outc
 
 (** Branch Control Unit instructions *)
   | Pret =>
-      Next (rs#PC <-- (rs#RA)) m
+      Next (rs#PC <- (rs#RA)) m
   | Pcall s =>
-      Next (rs#RA <-- (rs#PC) #PC <-- (Genv.symbol_address ge s Ptrofs.zero)) m
+      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
   | Pgoto s =>
-      Next (rs#PC <-- (Genv.symbol_address ge s Ptrofs.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
   | Pj_l l =>
       goto_label f l rs m
   | Pcb bt r l =>
@@ -1032,7 +1003,7 @@ end.
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome regset :=
   match exec_body (body b) rs0 m with
   | Next rs' m' =>
-    let rs1 := nextblock b (update_pregs rs0 rs') in
+    let rs1 := nextblock b rs' in
     match (exit b) with
     | None => Next rs1 m'
     | Some ic => exec_control f ic rs1 m'
@@ -1046,7 +1017,7 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom
   code.  *)
 
   (* FIXME - R31 is not there *)
-Definition breg_of (r: mreg) : breg :=
+Definition preg_of (r: mreg) : preg :=
   match r with
   | R0  => GPR0  | R1  => GPR1  | R2  => GPR2  | R3  => GPR3  | R4  => GPR4
   | R5  => GPR5  | R6  => GPR6  | R7  => GPR7                 | R9  => GPR9
@@ -1063,15 +1034,13 @@ Definition breg_of (r: mreg) : breg :=
   | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
   end.
 
-Definition preg_of (r: mreg) : preg := breg_of r.
-
 (** Extract the values of the arguments of an external call.
     We exploit the calling conventions from module [Conventions], except that
     we use RISC-V registers instead of locations. *)
 
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
-      extcall_arg rs m (R r) (rs (breg_of r))
+      extcall_arg rs m (R r) (rs (preg_of r))
   | extcall_arg_stack: forall ofs ty bofs v,
       bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
       Mem.loadv (chunk_of_type ty) m
@@ -1124,7 +1093,7 @@ Inductive stepin: option bblock -> state -> trace -> state -> Prop :=
       rs' = nextblock bi
               (set_res res vres
                 (undef_regs (map preg_of (destroyed_by_builtin ef))
-                   (rs#GPR31 <-- Vundef))) ->
+                   (rs#GPR31 <- Vundef))) ->
       stepin (Some bi) (State rs m) t (State rs' m')
   | exec_stepin_external:
       forall b ef args res rs m t rs' m',
@@ -1132,7 +1101,7 @@ Inductive stepin: option bblock -> state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <-- (rs RA) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs RA) ->
       stepin None (State rs m) t (State rs' m')
   .
 
@@ -1159,7 +1128,7 @@ Lemma exec_step_builtin b ofs f ef args res rs m vargs t vres rs' m' bi:
       rs' = nextblock bi
               (set_res res vres
                 (undef_regs (map preg_of (destroyed_by_builtin ef))
-                   (rs#GPR31 <-- Vundef))) ->
+                   (rs#GPR31 <- Vundef))) ->
       step (State rs m) t (State rs' m').
 Proof.
   intros; eexists. eapply exec_stepin_builtin; eauto.
@@ -1170,7 +1139,7 @@ Lemma exec_step_external b ef args res rs m t rs' m':
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <-- (rs RA) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs RA) ->
       step (State rs m) t (State rs' m')
   .
 Proof.
@@ -1187,9 +1156,9 @@ Inductive initial_state (p: program): state -> Prop :=
       let ge := Genv.globalenv p in
       let rs0 :=
         (Pregmap.init Vundef)
-        # PC <-- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
-        # SP <-- Vnullptr
-        # RA <-- Vnullptr in
+        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
+        # SP <- Vnullptr
+        # RA <- Vnullptr in
       Genv.init_mem p = Some m0 ->
       initial_state p (State rs0 m0).
 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index a9604c14..345f71b2 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1103,7 +1103,7 @@ Proof.
                  storeind_ptr GPR8 SP (fn_retaddr_ofs f) ::b x0) in *.
   set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
   set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f))) 
-                          (rs0#FP <-- (parent_sp s) #SP <-- sp #GPR31 <-- Vundef)).
+                          (rs0#FP <- (parent_sp s) #SP <- sp #GPR31 <- Vundef)).
   destruct TODO.
 (*   exploit (Pget_correct tge tf GPR8 RA (storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) rs2 m2'); auto.
   intros (rs' & U' & V').
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index f6e89a36..309dbc2c 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -17,22 +17,24 @@ Require Import Asmblockgen.
 Module MB:=Machblock.
 Module AB:=Asmblock.
 
+Hint Extern 2 (_ <> _) => congruence: asmgen.
+
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
 Proof.
   unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
-  destruct b. all: try discriminate.
+(*   destruct b. all: try discriminate.
   inv H1. auto.
-Qed.
+ *)Qed.
 
 (* FIXME - Replaced FR by IR for MPPA *)
 Lemma freg_of_eq:
   forall r r', freg_of r = OK r' -> preg_of r = IR r'.
 Proof.
   unfold freg_of; intros. destruct (preg_of r); inv H; auto.
-  destruct b. all: try discriminate.
+(*   destruct b. all: try discriminate.
   inv H1. auto.
-Qed.
+ *)Qed.
 
 
 Lemma preg_of_injective:
@@ -173,7 +175,7 @@ Lemma agree_set_other:
   forall ms sp rs r v,
   agree ms sp rs ->
   data_preg r = false ->
-  agree ms sp (rs#r <-- v).
+  agree ms sp (rs#r <- v).
 Proof.
   intros. apply agree_exten with rs. auto.
   intros. apply Pregmap.gso. congruence.
@@ -266,7 +268,7 @@ Qed.
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
-  agree ms sp' (rs#SP <-- sp').
+  agree ms sp' (rs#SP <- sp').
 Proof.
   intros. inv H. split; auto.
   intros. rewrite Pregmap.gso; auto with asmgen.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 8b686676..c996ab1f 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1355,7 +1355,7 @@ Definition noscroll := 0.
 Ltac bsimpl := unfold exec_bblock; simpl.
 
 Lemma Pget_correct:
-  forall (dst: gpreg) (src: breg) k (rs: regset) m,
+  forall (dst: gpreg) (src: preg) k (rs: regset) m,
   src = RA ->
   exists rs',
      exec_straight ge fn (Pget dst src ::b k) rs m k rs' m
@@ -1365,9 +1365,9 @@ Proof.
   intros. econstructor; econstructor; econstructor.
 - rewrite H. bsimpl. auto.
 - Simpl.
-(* - Simpl.
+- Simpl.
 - intros. rewrite H. Simpl.
- *)Admitted.
+Qed.
 
 (*
 
diff --git a/mppa_k1c/Asmbundle.v b/mppa_k1c/Asmbundle.v
index bd531930..cd29d6b2 100644
--- a/mppa_k1c/Asmbundle.v
+++ b/mppa_k1c/Asmbundle.v
@@ -47,17 +47,18 @@ Proof.
   all: repeat ((try (left; reflexivity)); right).
 Qed.
 
-Definition all_bregs := (map IR all_gpregs) ++ (map FR all_gpregs) ++ (RA::nil).
+Definition all_pregs := (map IR all_gpregs) ++ (map FR all_gpregs) ++ (RA::PC::nil).
 
-Fact all_bregs_complete : forall br, List.In br all_bregs.
+Fact all_pregs_complete : forall br, List.In br all_pregs.
 Proof.
   intros. destruct br.
-  - unfold all_bregs. apply in_app_iff. left. apply in_map. apply all_gpregs_complete.
-  - unfold all_bregs. apply in_app_iff. right. apply in_app_iff. left. apply in_map. apply all_gpregs_complete.
-  - unfold all_bregs. repeat (apply in_app_iff; right). simpl. left; auto.
+  - unfold all_pregs. apply in_app_iff. left. apply in_map. apply all_gpregs_complete.
+  - unfold all_pregs. apply in_app_iff. right. apply in_app_iff. left. apply in_map. apply all_gpregs_complete.
+  - unfold all_pregs. repeat (apply in_app_iff; right). simpl. left; auto.
+  - unfold all_pregs. repeat (apply in_app_iff; right). simpl. right; auto.
 Qed.
 
-Definition writeregs (i: instruction): list breg :=
+Definition writeregs (i: instruction): list preg :=
   match i with
   (* Control instructions *)
   | Pset rd rs => rd::nil
@@ -77,25 +78,27 @@ Definition writeregs (i: instruction): list breg :=
   | Pallocframe _ _ => IR FP::IR GPR31::IR SP :: nil
   | Pfreeframe _ _ => IR GPR31::IR SP :: nil
   (* builtins : only implemented in OCaml, we know nothing about them *)
-  | Pbuiltin _ _ _ => all_bregs
+  | Pbuiltin _ _ _ => all_pregs
   (* Instructions that do not write *)
   | Pnop | Pret | Pgoto _ | Pj_l _ | Pcb _ _ _ | Pcbu _ _ _ | PStoreRRO _ _ _ _ => nil
   end.
 
-Lemma update_PC_breg (rs: regset) v (r: breg):
-  (rs#PC <-- v) r = rs r.
+(* Lemma update_PC_breg (rs: regset) v (r: preg):
+  (rs#PC <- v) r = rs r.
 Proof.
- rewrite Pregmap.gso; congruence.
+  rewrite Pregmap.gso; auto. congruence.
 Qed.
+ *)
 
-Lemma update_pregs_diff (rs:regset) rd x r: r <> rd -> update_pregs rs (rs # rd <- x) r = rs r.
+(* Lemma update_pregs_diff (rs:regset) rd x r: r <> rd -> update_pregs rs (rs # rd <- x) r = rs r.
 Proof.
   unfold update_pregs. intro H. rewrite Bregmap.gso; congruence.
 Qed.
- 
-Hint Rewrite update_PC_breg update_pregs_diff: regset_rw.
+ *) 
 
-Fact writeregs_correct f i rs m rs' m' r: 
+(* Hint Rewrite update_PC_breg update_pregs_diff: regset_rw. *)
+
+(* Fact writeregs_correct f i rs m rs' m' r: 
     ~(List.In r (writeregs i)) -> 
     (exec_bblock ge f (bblock_single_inst i) rs m) = Next rs' m' ->
     rs' r = rs r.
@@ -121,8 +124,9 @@ Proof.
   autorewrite with regset_rw; auto.
   - (* ALLOCFRAME *)
 Admitted.
+ *)
 
-Definition readregs (i: instruction) : list breg :=
+Definition readregs (i: instruction) : list preg :=
   match i with
   (* Control instructions *)
   | Pset rd rs => IR rs::nil
@@ -141,14 +145,14 @@ Definition readregs (i: instruction) : list breg :=
   (* Alloc and freeframe (from the semantics) *) 
   | Pallocframe _ _ | Pfreeframe _ _ => IR SP :: nil
   (* builtins : only implemented in OCaml, we know nothing about them *)
-  | Pbuiltin _ _ _ => all_bregs
+  | Pbuiltin _ _ _ => all_pregs
   (* Instructions that do not read *)
   | Pnop | Pcall _ | Pgoto _ | Pj_l _ | PArithR _ _ | PArithRI32 _ _ _ | PArithRI64 _ _ _ => nil
   end.
 
 Axiom TODO: False.
 
-Definition outcome_equiv (r: breg) v (o1 o2: outcome (rgset:=regset))  :=
+(* Definition outcome_equiv (r: preg) v (o1 o2: outcome (rgset:=regset))  :=
   match o1 with
   | Next rs1 m1 => exists rs2, exists m2, o2=Next rs2 m2 /\ (forall r, (rs1#r <-- v) r = rs2 r) /\ (forall chunk p, Mem.loadv chunk m1 p = Mem.loadv chunk m2 p)
   | Stuck => o2 = Stuck
@@ -174,6 +178,7 @@ Proof.
        rewrite! update_PC_breg.
     (* TODO: lemma on  rs # _ <-- _ *)
 Abort.
+ *)
 
 (* alternative definition of disjoint *)
 Definition disjoint_x {A: Type} (l l':list A) : Prop := forall r, In r l -> ~In r l'. (* TODO: use notIn instead ? *)
@@ -213,7 +218,7 @@ Proof.
   repeat (match goal with h:_ \/ _ |- _ => inversion_clear h; [discriminate|] | _ => fail end); contradiction).
 Qed.
 
-Inductive depfree : list breg -> list breg -> list instruction -> Prop :=
+Inductive depfree : list preg -> list preg -> list instruction -> Prop :=
   | depfree_nil : forall lr lw, depfree lr lw nil
   | depfree_cons : forall i lri lwi lw lr l,
                     lri = readregs i -> lwi = writeregs i ->
@@ -224,7 +229,7 @@ Inductive depfree : list breg -> list breg -> list instruction -> Prop :=
   .
 
 (* une version alternative *)
-Inductive depfreex : list breg -> list instruction -> Prop :=
+Inductive depfreex : list preg -> list instruction -> Prop :=
   | depfreex_nil : forall lw, depfreex lw nil
   | depfreex_cons : forall i lri lwi lw l,
                     lri = readregs i -> lwi = writeregs i ->