Module Asmblockprops

Common definition and proofs on Asmblock required by various modules

Require Import Coqlib.
Require Import Integers.
Require Import Memory.
Require Import Globalenvs.
Require Import Values.
Require Import Asmblock.
Require Import Axioms.

Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
  forall rs m,
    exec_bblock ge f bb rs m <> Stuck ->
    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.

#[global] Hint Extern 2 (_ <> _) => congruence: asmgen.

Lemma preg_of_data:
  forall r, data_preg (preg_of r) = true.

Proof.

intros. destruct r; reflexivity.
Qed.

#[global] Hint Resolve preg_of_data: asmgen.

Lemma data_diff:
forall r r',
data_preg r = true -> data_preg r' = false -> r <> r'.

Proof.

congruence.
Qed.

#[global] Hint Resolve data_diff: asmgen.

Lemma preg_of_not_PC:
forall r, preg_of r <> PC.

Proof.

intros. apply data_diff; auto with asmgen.
Qed.

Lemma preg_of_not_SP:
forall r, preg_of r <> SP.

Proof.

intros. unfold preg_of; destruct r; cbn; congruence.
Qed.

#[global] Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.

Lemma nextblock_pc:
forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).

Proof.

intros. apply Pregmap.gss.
Qed.

Lemma nextblock_inv:
forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.

Proof.

intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
Qed.

Lemma nextblock_inv1:
forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.

Proof.

intros. apply nextblock_inv. red; intro; subst; discriminate.
Qed.

Ltac Simplif :=
  ((rewrite nextblock_inv by eauto with asmgen)
  || (rewrite nextblock_inv1 by eauto with asmgen)
  || (rewrite Pregmap.gss)
  || (rewrite nextblock_pc)
  || (rewrite Pregmap.gso by eauto with asmgen)
  ); auto with asmgen.

Ltac Simpl := repeat Simplif.

Theorem exec_basic_instr_pc:
  forall ge b rs1 m1 rs2 m2,
  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
  rs2 PC = rs1 PC.

Proof.

  intros. destruct b; try destruct i; try destruct i.
  all: try (inv H; Simpl).
  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.

  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.

  { (* PLoadQRRO *)
    unfold parexec_load_q_offset in H1.
    destruct (gpreg_q_expand _) as [r0 r1] in H1.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    inv H1. Simpl. }
  { (* PLoadORRO *)
    unfold parexec_load_o_offset in H1.
    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    destruct (Mem.loadv _ _ _) in H1; try discriminate.
    inv H1. Simpl. }
  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.

  { (* PStoreQRRO *)
    unfold parexec_store_q_offset in H1.
    destruct (gpreg_q_expand _) as [r0 r1] in H1.
    unfold eval_offset in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    inv H1. Simpl. reflexivity. }
  { (* PStoreORRO *)
    unfold parexec_store_o_offset in H1.
    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
    unfold eval_offset in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    destruct (Mem.storev _ _ _) in H1; try discriminate.
    inv H1. Simpl. reflexivity. }
  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
  - destruct rs; try discriminate. inv H1. Simpl.
  - destruct rd; try discriminate. inv H1; Simpl.
  - reflexivity.
Qed.

Lemma regset_double_set:
  forall r1 r2 (rs: regset) v1 v2,
  r1 <> r2 ->
  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).

Proof.

  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
  - destruct (preg_eq r r2).
    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
    + repeat (rewrite Pregmap.gso; auto).
Qed.

Lemma next_eq:
forall (rs rs': regset) m m',
rs = rs' -> m = m' -> Next rs m = Next rs' m'.

Proof.

intros; apply f_equal2; auto.
Qed.

Lemma exec_load_offset_pc_var:
  forall trap t rs m rd ra ofs rs' m' v,
  exec_load_offset trap t rs m rd ra ofs = Next rs' m' ->
  exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - unfold parexec_incorrect_load in *.
    destruct trap; try discriminate.
    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
Qed.

Lemma exec_load_reg_pc_var:
  forall trap t rs m rd ra ro rs' m' v,
    exec_load_reg trap t rs m rd ra ro = Next rs' m' ->
    exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - unfold parexec_incorrect_load in *.
    destruct trap; try discriminate.
    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
Qed.

Lemma exec_load_regxs_pc_var:
  forall trap t rs m rd ra ro rs' m' v,
  exec_load_regxs trap t rs m rd ra ro = Next rs' m' ->
  exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - unfold parexec_incorrect_load in *.
    destruct trap; try discriminate.
    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
Qed.

Lemma exec_load_offset_q_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_load_q_offset rs m rd ra ofs = Next rs' m' ->
  exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *.
  destruct (gpreg_q_expand rd) as [rd0 rd1].
  (* destruct (ireg_eq rd0 ra); try discriminate. *)
  rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  inv H.
  destruct (Mem.loadv _ _ _); try discriminate.
  inv H1. f_equal.
  rewrite (regset_double_set PC rd0) by discriminate.
  rewrite (regset_double_set PC rd1) by discriminate.
  reflexivity.
Qed.

Lemma exec_load_offset_o_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_load_o_offset rs m rd ra ofs = Next rs' m' ->
  exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *.
  destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3].
(*
  destruct (ireg_eq rd0 ra); try discriminate.
  destruct (ireg_eq rd1 ra); try discriminate.
  destruct (ireg_eq rd2 ra); try discriminate.
*)
  rewrite Pregmap.gso; try discriminate.
  cbn in *.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  rewrite (regset_double_set PC rd0) by discriminate.
  rewrite (regset_double_set PC rd1) by discriminate.
  rewrite (regset_double_set PC rd2) by discriminate.
  rewrite (regset_double_set PC rd3) by discriminate.
  inv H.
  trivial.
Qed.

Lemma exec_store_offset_pc_var:
  forall t rs m rd ra ofs rs' m' v,
  exec_store_offset t rs m rd ra ofs = Next rs' m' ->
  exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
  destruct (eval_offset ofs); try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Lemma exec_store_q_offset_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_store_q_offset rs m rd ra ofs = Next rs' m' ->
  exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate.
  cbn in *.
  destruct (gpreg_q_expand _) as [s0 s1].
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  inv H. apply next_eq; auto.
Qed.

Lemma exec_store_o_offset_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_store_o_offset rs m rd ra ofs = Next rs' m' ->
  exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

Proof.

  intros.
  unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *.
  destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3].
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  inv H.
  trivial.
Qed.

Lemma exec_store_reg_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_store_reg t rs m rd ra ro = Next rs' m' ->
  exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Lemma exec_store_regxs_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_store_regxs t rs m rd ra ro = Next rs' m' ->
  exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.

Proof.

  intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Theorem exec_basic_instr_pc_var:
  forall ge i rs m rs' m' v,
  exec_basic_instr ge i rs m = Next rs' m' ->
  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.

Proof.

  intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i.
  - unfold exec_arith_instr in *. destruct i; destruct i.
      all: try (exploreInst; inv H; apply next_eq; auto;
      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
(*
      (* Some cases treated seperately because exploreInst destructs too much *)
      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
  - destruct i.
    + exploreInst; apply exec_load_offset_pc_var; auto.
    + exploreInst; apply exec_load_reg_pc_var; auto.
    + exploreInst; apply exec_load_regxs_pc_var; auto.
    + apply exec_load_offset_q_pc_var; auto.
    + apply exec_load_offset_o_pc_var; auto.
  - destruct i.
    + exploreInst; apply exec_store_offset_pc_var; auto.
    + exploreInst; apply exec_store_reg_pc_var; auto.
    + exploreInst; apply exec_store_regxs_pc_var; auto.
    + apply exec_store_q_offset_pc_var; auto.
    + apply exec_store_o_offset_pc_var; auto.
  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
    destruct (Mem.storev _ _ _ _); try discriminate.
    inv H. apply next_eq; auto. apply functional_extensionality. intros.
    rewrite (regset_double_set GPR32 PC); try discriminate.
    rewrite (regset_double_set GPR12 PC); try discriminate.
    rewrite (regset_double_set FP PC); try discriminate. reflexivity.
  - repeat (rewrite Pregmap.gso; try discriminate).
    destruct (Mem.loadv _ _ _); try discriminate.
    destruct (rs GPR12); try discriminate.
    destruct (Mem.free _ _ _ _); try discriminate.
    inv H. apply next_eq; auto.
    rewrite (regset_double_set GPR32 PC).
    rewrite (regset_double_set GPR12 PC). reflexivity.
    all: discriminate.
  - destruct rs0; try discriminate. inv H. apply next_eq; auto.
    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
  - destruct rd; try discriminate. inv H. apply next_eq; auto.
    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
  - inv H. apply next_eq; auto.
Qed.