Require Import Coqlib.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Asm.
Require Import Asmgen.
Require Import Asmgenproof0.
Require Import Conventions.

Open Local Scope error_monad_scope.

Correspondence between Mach registers and IA32 registers

Lemma agree_nextinstr_nf:
  forall ms sp rs,
  agree ms sp rs -> agree ms sp (nextinstr_nf rs).


Lemma nextinstr_nf_inv:
  forall r rs,
  match r with PC => False | CR _ => False | _ => True end ->
  (nextinstr_nf rs)#r = rs#r.

Lemma nextinstr_nf_inv1:
  forall r rs,
  data_preg r = true -> (nextinstr_nf rs)#r = rs#r.

Lemma nextinstr_nf_set_preg:
  forall rs m v,
  (nextinstr_nf (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone.


Ltac Simplif :=
  match goal with
  | [ |- nextinstr_nf _ _ = _ ] =>
      ((rewrite nextinstr_nf_inv by auto with asmgen)
       || (rewrite nextinstr_nf_inv1 by auto with asmgen)); auto
  | [ |- nextinstr _ _ = _ ] =>
      ((rewrite nextinstr_inv by auto with asmgen)
       || (rewrite nextinstr_inv1 by auto with asmgen)); auto
  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] =>
      rewrite Pregmap.gss; auto
  | [ |- Pregmap.set ?x _ _ ?x = _ ] =>
      rewrite Pregmap.gss; auto
  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] =>
      rewrite Pregmap.gso by (auto with asmgen); auto
  | [ |- Pregmap.set _ _ _ _ = _ ] =>
      rewrite Pregmap.gso by (auto with asmgen); auto
  end.

Ltac Simplifs := repeat Simplif.

Correctness of IA32 constructor functions

Section CONSTRUCTORS.

Variable ge: genv.
Variable fn: function.


Lemma mk_mov_correct:
  forall rd rs k c rs1 m,
  mk_mov rd rs k = OK c ->
  exists rs2,
     exec_straight ge fn c rs1 m k rs2 m
  /\ rs2#rd = rs1#rs
  /\ forall r, data_preg r = true -> r <> rd -> rs2#r = rs1#r.


Remark divs_mods_exist:
  forall v1 v2,
  match Val.divs v1 v2, Val.mods v1 v2 with
  | Some _, Some _ => True
  | None, None => True
  | _, _ => False
  end.

Remark divu_modu_exist:
  forall v1 v2,
  match Val.divu v1 v2, Val.modu v1 v2 with
  | Some _, Some _ => True
  | None, None => True
  | _, _ => False
  end.


Lemma mk_shrximm_correct:
  forall n k c (rs1: regset) v m,
  mk_shrximm n k = OK c ->
  Val.shrx (rs1#EAX) (Vint n) = Some v ->
  exists rs2,
     exec_straight ge fn c rs1 m k rs2 m
  /\ rs2#EAX = v
  /\ forall r, data_preg r = true -> r <> EAX -> r <> ECX -> rs2#r = rs1#r.


Lemma mk_intconv_correct:
  forall mk sem rd rs k c rs1 m,
  mk_intconv mk rd rs k = OK c ->
  (forall c rd rs r m,
   exec_instr ge c (mk rd rs) r m = Next (nextinstr (r#rd <- (sem r#rs))) m) ->
  exists rs2,
     exec_straight ge fn c rs1 m k rs2 m
  /\ rs2#rd = sem rs1#rs
  /\ forall r, data_preg r = true -> r <> rd -> r <> EAX -> rs2#r = rs1#r.


Lemma addressing_mentions_correct:
  forall a r (rs1 rs2: regset),
  (forall (r': ireg), r' <> r -> rs1 r' = rs2 r') ->
  addressing_mentions a r = false ->
  eval_addrmode ge a rs1 = eval_addrmode ge a rs2.

Lemma mk_smallstore_correct:
  forall chunk sto addr r k c rs1 m1 m2,
  mk_smallstore sto addr r k = OK c ->
  Mem.storev chunk m1 (eval_addrmode ge addr rs1) (rs1 r) = Some m2 ->
  (forall c r addr rs m,
   exec_instr ge c (sto addr r) rs m = exec_store ge chunk m addr rs r nil) ->
  exists rs2,
     exec_straight ge fn c rs1 m1 k rs2 m2
  /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> rs2#r = rs1#r.


Lemma loadind_correct:
  forall (base: ireg) ofs ty dst k (rs: regset) c m v,
  loadind base ofs ty dst k = OK c ->
  Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
  exists rs',
     exec_straight ge fn c rs m k rs' m
  /\ rs'#(preg_of dst) = v
  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.

Lemma storeind_correct:
  forall (base: ireg) ofs ty src k (rs: regset) c m m',
  storeind src base ofs ty k = OK c ->
  Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
  exists rs',
     exec_straight ge fn c rs m k rs' m'
  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r.


Lemma transl_addressing_mode_correct:
  forall addr args am (rs: regset) v,
  transl_addressing addr args = OK am ->
  eval_addressing ge (rs ESP) addr (List.map rs (List.map preg_of args)) = Some v ->
  Val.lessdef v (eval_addrmode ge am rs).


Lemma compare_ints_spec:
  forall rs v1 v2 m,
  let rs' := nextinstr (compare_ints v1 v2 rs m) in
     rs'#ZF = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
  /\ rs'#CF = Val.cmpu (Mem.valid_pointer m) Clt v1 v2
  /\ rs'#SF = Val.negative (Val.sub v1 v2)
  /\ rs'#OF = Val.sub_overflow v1 v2
  /\ (forall r, data_preg r = true -> rs'#r = rs#r).

Lemma int_signed_eq:
  forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y).

Lemma int_not_lt:
  forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y).

Lemma int_lt_not:
  forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y).

Lemma int_not_ltu:
  forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y).

Lemma int_ltu_not:
  forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y).

Lemma testcond_for_signed_comparison_correct:
  forall c v1 v2 rs m b,
  Val.cmp_bool c v1 v2 = Some b ->
  eval_testcond (testcond_for_signed_comparison c)
                (nextinstr (compare_ints v1 v2 rs m)) = Some b.

Lemma testcond_for_unsigned_comparison_correct:
  forall c v1 v2 rs m b,
  Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
  eval_testcond (testcond_for_unsigned_comparison c)
                (nextinstr (compare_ints v1 v2 rs m)) = Some b.

Lemma compare_floats_spec:
  forall rs n1 n2,
  let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in
     rs'#ZF = Val.of_bool (negb (Float.cmp Cne n1 n2))
  /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2))
  /\ rs'#PF = Val.of_bool (negb (Float.cmp Ceq n1 n2 || Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2))
  /\ (forall r, data_preg r = true -> rs'#r = rs#r).

Lemma compare_floats32_spec:
  forall rs n1 n2,
  let rs' := nextinstr (compare_floats32 (Vsingle n1) (Vsingle n2) rs) in
     rs'#ZF = Val.of_bool (negb (Float32.cmp Cne n1 n2))
  /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2))
  /\ rs'#PF = Val.of_bool (negb (Float32.cmp Ceq n1 n2 || Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2))
  /\ (forall r, data_preg r = true -> rs'#r = rs#r).

Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
  match xc with
  | Cond_base c =>
      eval_testcond c rs
  | Cond_and c1 c2 =>
      match eval_testcond c1 rs, eval_testcond c2 rs with
      | Some b1, Some b2 => Some (b1 && b2)
      | _, _ => None
      end
  | Cond_or c1 c2 =>
      match eval_testcond c1 rs, eval_testcond c2 rs with
      | Some b1, Some b2 => Some (b1 || b2)
      | _, _ => None
      end
  end.

Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A :=
  match c with
  | Clt | Cle => n2
  | Ceq | Cne | Cgt | Cge => n1
  end.

Lemma testcond_for_float_comparison_correct:
  forall c n1 n2 rs,
  eval_extcond (testcond_for_condition (Ccompf c))
               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
                                          (Vfloat (swap_floats c n2 n1)) rs)) =
  Some(Float.cmp c n1 n2).

Lemma testcond_for_neg_float_comparison_correct:
  forall c n1 n2 rs,
  eval_extcond (testcond_for_condition (Cnotcompf c))
               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
                                          (Vfloat (swap_floats c n2 n1)) rs)) =
  Some(negb(Float.cmp c n1 n2)).

Lemma testcond_for_float32_comparison_correct:
  forall c n1 n2 rs,
  eval_extcond (testcond_for_condition (Ccompfs c))
               (nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
                                            (Vsingle (swap_floats c n2 n1)) rs)) =
  Some(Float32.cmp c n1 n2).

Lemma testcond_for_neg_float32_comparison_correct:
  forall c n1 n2 rs,
  eval_extcond (testcond_for_condition (Cnotcompfs c))
               (nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
                                            (Vsingle (swap_floats c n2 n1)) rs)) =
  Some(negb(Float32.cmp c n1 n2)).

Remark swap_floats_commut:
  forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y).

Remark compare_floats_inv:
  forall vx vy rs r,
  r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
  compare_floats vx vy rs r = rs r.

Remark compare_floats32_inv:
  forall vx vy rs r,
  r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
  compare_floats32 vx vy rs r = rs r.

Lemma transl_cond_correct:
  forall cond args k c rs m,
  transl_cond cond args k = OK c ->
  exists rs',
     exec_straight ge fn c rs m k rs' m
  /\ match eval_condition cond (map rs (map preg_of args)) m with
     | None => True
     | Some b => eval_extcond (testcond_for_condition cond) rs' = Some b
     end
  /\ forall r, data_preg r = true -> rs'#r = rs r.

Remark eval_testcond_nextinstr:
  forall c rs, eval_testcond c (nextinstr rs) = eval_testcond c rs.

Remark eval_testcond_set_ireg:
  forall c rs r v, eval_testcond c (rs#(IR r) <- v) = eval_testcond c rs.

Lemma mk_setcc_base_correct:
  forall cond rd k rs1 m,
  exists rs2,
  exec_straight ge fn (mk_setcc_base cond rd k) rs1 m k rs2 m
  /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
  /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> r <> rd -> rs2#r = rs1#r.

Lemma mk_setcc_correct:
  forall cond rd k rs1 m,
  exists rs2,
  exec_straight ge fn (mk_setcc cond rd k) rs1 m k rs2 m
  /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
  /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> r <> rd -> rs2#r = rs1#r.


Ltac ArgsInv :=
  match goal with
  | [ H: Error _ = OK _ |- _ ] => discriminate
  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args; ArgsInv
  | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv
  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; clear H; ArgsInv
  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *; clear H; ArgsInv
  | _ => idtac
  end.

Ltac TranslOp :=
  econstructor; split;
  [ apply exec_straight_one; [ simpl; eauto | auto ]
  | split; [ Simplifs | intros; Simplifs ]].

Lemma transl_op_correct:
  forall op args res k c (rs: regset) m v,
  transl_op op args res k = OK c ->
  eval_operation ge (rs#ESP) op (map rs (map preg_of args)) m = Some v ->
  exists rs',
     exec_straight ge fn c rs m k rs' m
  /\ Val.lessdef v rs'#(preg_of res)
  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.


Lemma transl_load_correct:
  forall chunk addr args dest k c (rs: regset) m a v,
  transl_load chunk addr args dest k = OK c ->
  eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists rs',
     exec_straight ge fn c rs m k rs' m
  /\ rs'#(preg_of dest) = v
  /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.

Lemma transl_store_correct:
  forall chunk addr args src k c (rs: regset) m a m',
  transl_store chunk addr args src k = OK c ->
  eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a ->
  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
  exists rs',
     exec_straight ge fn c rs m k rs' m'
  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.

End CONSTRUCTORS.