Require Import Coqlib.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import NormaliseSpec.
Require Import ExprEval.
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.

Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import MemRel.

Hint Resolve wf_mr_ld wf_mr_norm_ld.

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).



Ltac repSplit' T :=
  repeat match goal with
           | |- _ /\ _ => split; T
         end.

Ltac repSplit := repSplit' idtac.

Lemma reg_ptr_undef_regs:
  forall lr rs r b o,
    reg_ptr rs r b o ->
    ~ In r lr ->
    reg_ptr (undef_regs lr rs) r b o.

Lemma ptru_undef_regs:
  forall lr rs r,
    ptr_or_zero rs r ->
    ~ In r lr ->
    ptr_or_zero (undef_regs lr rs) r.

Lemma nextinstr_nf_pc :
  forall rs b o,
    reg_ptr rs PC b o ->
    reg_ptr (nextinstr_nf rs) PC b (incr o).


Lemma nextinstr_nf_pcu :
  forall rs,
    ptr_or_zero rs PC ->
    ptr_or_zero (nextinstr_nf rs) PC.

Correctness of IA32 constructor functions

Ltac pc_trans :=
  repeat match goal with
           | H1: reg_ptr ?rs PC ?b ?o, H2: incr_pc ?rs ?rs2 |- _ =>
             match goal with
                 H: reg_ptr rs2 PC _ _ |- _ => fail 1
               | |- _ => let i := fresh "RP" in
                         generalize (incr_pc_reg_ptr rs rs2 _ _ H2 H1); intro i
             end
         end.


Ltac srp :=
      repeat
      match goal with
        | H:reg_ptr ?rs1 PC ?b ?o
          |- incr_pc _ _ =>
          red; intros; exists b; eexists; split;
          [
          | apply nextinstr_pc; unfold reg_ptr; Simplifs ]
        | |- _ => apply nextinstr_pc; Simplifs; eauto
        | H: reg_ptr ?rs1 PC ?b ?o |- reg_ptr ?rs1 PC ?b _ => eauto
        | |- _ => pc_trans; Simplifs; auto
      end.

Section CONSTRUCTORS.

Variable ge: genv.
Variable fn: function.


Lemma incr_pc_nextinstr:
  forall rs1 (i: ireg) i0 b o,
    reg_ptr rs1 PC b o ->
    incr_pc rs1 (nextinstr rs1 # i <- i0).


Lemma incr_pc_nextinstr_f:
  forall rs1 (i: freg) i0 b o,
    reg_ptr rs1 PC b o ->
    incr_pc rs1 (nextinstr rs1 # i <- i0).

Lemma mk_mov_correct:
  forall rd rs k c rs1 m b o,
    mk_mov rd rs k = OK c ->
    reg_ptr rs1 PC b o ->
    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.



Theorem shrx_shr:
  forall x y,
    Val.lessdef
      (Val.shrx x y)
      (Val.shr
         (Val.add x
                  (Val.mul
                     (Val.cmp Clt x (Eval (Vint Int.zero)))
                     (Val.sub (Val.shl (Eval (Vint Int.one)) y) (Eval (Vint Int.one))))) y).


Lemma lift_vint:
  forall a: bool,
    (if a then Vtrue else Vfalse) =
    Vint (if a then Int.one else Int.zero).





Lemma mk_shrximm_correct:
  forall n k c (rs1: regset) m b o,
    mk_shrximm n k = OK c ->
    reg_ptr rs1 PC b o ->
    exists rs2,
      exec_straight ge fn c rs1 m k rs2 m
      /\ Val.lessdef (Val.shrx (rs1#EAX) (Eval (Vint n))) rs2#EAX
      /\ 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 b o
         (RP: reg_ptr rs1 PC b o)
         (MI: mk_intconv mk rd rs k = OK c)
         (fEI: 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 eval_addrmode_int:
  forall addr rs alloc em,
    wt_val (eSexpr alloc em (eval_addrmode ge addr rs)) Tint.

Lemma mk_smallstore_correct:
  forall chunk sto addr r k c rs1 m1 m2 b o
         (Rpc: reg_ptr rs1 PC b o)
         (MKSS: mk_smallstore sto addr r k = OK c)
         (SV: Mem.storev chunk m1 (eval_addrmode ge addr rs1) (rs1 r) = Some m2)
         (EIES: 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 loadv_se:
  forall m c ptr ptr',
    same_eval ptr ptr' ->
    Mem.loadv c m ptr = Mem.loadv c m ptr'.
        

Lemma loadind_correct:
  forall (base: ireg) ofs ty dst k (rs: regset) c m v b o
         (Npc: reg_ptr rs PC b o)
         (LI: loadind base ofs ty dst k = OK c)
         (LV: Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Eval (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 storev_se:
  forall m c ptr ptr' v,
    same_eval ptr ptr' ->
    Mem.storev c m ptr v = Mem.storev c m ptr' v.

Lemma storeind_correct:
  forall (base: ireg) ofs ty src k (rs: regset) c m m' b o
         (Rpc: reg_ptr rs PC b o)
         (SI: storeind src base ofs ty k = OK c)
         (SV: Mem.storev (chunk_of_type ty) m
                         (Val.add rs#base (Eval (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 Ceq v1 v2
  /\ rs'#CF = Val.cmpu Clt v1 v2
  /\ rs'#SF = (Ebinop (OpCmp SESigned Clt) Tint Tint (Val.sub v1 v2) (Eval (Vint Int.zero)))
  /\ rs'#OF = (Ebinop OpSubOverflow Tint Tint 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,
    same_eval (Val.cmp_bool c v1 v2)
              (eval_testcond (testcond_for_signed_comparison c)
                             (nextinstr (compare_ints v1 v2 rs m))).


Lemma testcond_for_unsigned_comparison_correct:
  forall c v1 v2 rs m,
    same_eval (Val.cmpu_bool c v1 v2)
              (eval_testcond (testcond_for_unsigned_comparison c)
                             (nextinstr (compare_ints v1 v2 rs m))).

Lemma compare_floats_spec:
  forall rs n1 n2,
  let rs' := nextinstr (compare_floats n1 n2 rs) in
     rs'#ZF = Val.cmpf Ceq n1 n2
     /\ rs'#CF = Val.notbool (Val.cmpf Cge n1 n2)
  /\ rs'#PF = Val.notbool (Val.or (Val.cmpf Ceq n1 n2)
                                  (Val.or (Val.cmpf Clt n1 n2) (Val.cmpf 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 n1 n2 rs) in
     rs'#ZF = Val.cmpfs Ceq n1 n2
  /\ rs'#CF = Val.notbool (Val.cmpfs Cge n1 n2)
  /\ rs'#PF = Val.notbool (Val.or (Val.cmpfs Ceq n1 n2)
                                  (Val.or (Val.cmpfs Clt n1 n2) (Val.cmpfs Cgt n1 n2)))
  /\ (forall r, data_preg r = true -> rs'#r = rs#r).

Definition eval_extcond (xc: extcond) (rs: regset) : expr_sym :=
  match xc with
  | Cond_base c =>
      eval_testcond c rs
  | Cond_and c1 c2 =>
    Val.and (eval_testcond c1 rs) (eval_testcond c2 rs)
  | Cond_or c1 c2 =>
    Val.or (eval_testcond c1 rs) (eval_testcond c2 rs)
  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,
    same_eval (eval_extcond (testcond_for_condition (Ccompf c))
                            (nextinstr (compare_floats ((swap_floats c n1 n2))
                                                       ((swap_floats c n2 n1)) rs)))
              (Val.cmpf c n1 n2).

Lemma testcond_for_neg_float_comparison_correct:
  forall c n1 n2 rs,
    same_eval
      (eval_extcond (testcond_for_condition (Cnotcompf c))
                    (nextinstr (compare_floats ((swap_floats c n1 n2))
                                               ((swap_floats c n2 n1)) rs)))
      (Val.notbool (Val.cmpf c n1 n2)).

Lemma testcond_for_float32_comparison_correct:
  forall c n1 n2 rs,
    same_eval (eval_extcond (testcond_for_condition (Ccompfs c))
                            (nextinstr (compare_floats32 ((swap_floats c n1 n2))
                                                         ((swap_floats c n2 n1)) rs)))
              (Val.cmpfs c n1 n2).

Lemma testcond_for_neg_float32_comparison_correct:
  forall c n1 n2 rs,
    same_eval (eval_extcond (testcond_for_condition (Cnotcompfs c))
                            (nextinstr (compare_floats32 ((swap_floats c n1 n2))
                                                         ((swap_floats c n2 n1)) rs)))
              (Val.notbool (Val.cmpfs 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 b o
         (Rpc: reg_ptr rs PC b o)
         (TC: 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)) with
     | None => False
     | Some b => same_eval (eval_extcond (testcond_for_condition cond) rs') b
     end
  /\ forall r, data_preg r = true -> rs'#r = rs r.


Lemma transl_cond_correct:
  forall cond args k c rs m b o
         (Rpc: reg_ptr rs PC b o)
         (TC: transl_cond cond args k = OK c),
  exists rs' b,
     exec_straight ge fn c rs m k rs' m
     /\ eval_condition cond (map rs (map preg_of args)) = Some b
     /\ same_eval (eval_extcond (testcond_for_condition cond) rs') b
     /\ 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 b o
         (Rpc: reg_ptr rs1 PC b o),
  exists rs2,
    exec_straight ge fn (mk_setcc_base cond rd k) rs1 m k rs2 m
    /\ same_eval rs2#rd (eval_extcond cond rs1)
    /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> r <> rd -> rs2#r = rs1#r.

Lemma sn_minus_n:
  forall (n:nat),
    (Datatypes.S n - n = 1)%nat.

Lemma exec_straight_length:
  forall i rs1 m k rs2 m'
         (RS: exec_straight ge fn i rs1 m k rs2 m'),
    (length i >= length k)%nat.
  
Lemma exec_straight_wfpc:
  forall i rs1 m k rs2 m'
         (ES: exec_straight ge fn i rs1 m k rs2 m')
         b o (Rpc: reg_ptr rs1 PC b o),
    reg_ptr rs2 PC b (Int.add o (Int.repr (Z.of_nat (length i - length k)))).

Lemma sn_minus_sm:
  forall n m,
    (Datatypes.S n - Datatypes.S m = n - m)%nat.

Lemma mk_setcc_base_length:
  forall cond rd k,
    (length (mk_setcc_base cond EAX (Pmov_rr rd EAX :: k)) - Datatypes.S (length k)
    = match cond with
          Cond_base _ => 1
        | _ => 3
      end)%nat.

Lemma mk_setcc_correct:
  forall cond rd k rs1 m b o
         (Rpc: reg_ptr rs1 PC b o),
  exists rs2,
    exec_straight ge fn (mk_setcc cond rd k) rs1 m k rs2 m
    /\ same_eval rs2#rd (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 eqn:?; 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 _ |- _ ] => progress (simpl in *; rewrite (ireg_of_eq _ _ H) in *; ArgsInv)
  | [ H: freg_of _ = OK _ |- _ ] => progress (simpl in *; rewrite (freg_of_eq _ _ H) in *; ArgsInv)
  | _ => idtac
  end.


                                                          

Lemma pos_add_pos:
  forall a b,
    0 <= a -> 0 <= b ->
    0 <= a + b.

Lemma transl_cond_length:
  forall c0 args x k c,
    transl_cond c0 args (mk_setcc (testcond_for_condition c0) x k) = OK c ->
    (length c - length (mk_setcc (testcond_for_condition c0) x k) = 1)%nat.

Opaque plus.

Lemma transl_op_correct:
  forall op args res k c (rs: regset) m v b o
         (Npc: reg_ptr rs PC b o)
         (TR: transl_op op args res k = OK c)
         (EV: eval_operation ge (rs#ESP) op (map rs (map preg_of args)) = 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 b o
         (Rpc: reg_ptr rs PC b o)
         (TL: transl_load chunk addr args dest k = OK c)
         (EVA: eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a)
         (LV: 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' b o
         (Rpc: reg_ptr rs PC b o)
         (TS: transl_store chunk addr args src k = OK c)
         (EVA: eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a)
         (SV: 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.