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

Require Import Blockset Footprint InteractionSemantics MemOpFP Op_fp
        Mach_local ASM_local asmgen asmgen_proof0 Asmgenproof1.

Local Open Scope error_monad_scope.

Local Notation footprint := FP.t.
Local Notation empfp := FP.emp.

Correspondence between Mach registers and x86 registers

Correctness of x86-64 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 empfp k rs2 m
  /\ rs2#rd = rs1#rs
  /\ forall r, data_preg r = true -> r <> rd -> rs2#r = rs1#r.



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


Lemma mk_shrxlimm_correct:
  forall n k c (rs1: regset) v m,
  mk_shrxlimm n k = OK c ->
  Val.shrxl (rs1#RAX) (Vint n) = Some v ->
  exists rs2,
     exec_straight ge fn c rs1 m empfp k rs2 m
  /\ rs2#RAX = v
  /\ forall r, data_preg r = true -> r <> RAX -> r <> RDX -> rs2#r = rs1#r.


Lemma mk_intconv_correct:
  forall mk sem rd rs k c rs1 m fp,
    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) ->
    (fp = if Archi.ptr64 || low_ireg rs
         then exec_instr_fp ge fn (mk rd rs) rs1 m
         else exec_instr_fp ge fn (mk rd RAX) (nextinstr rs1 # RAX <- (rs1 rs)) m) ->
    exists rs2,
      exec_straight ge fn c rs1 m fp k rs2 m
      /\ rs2#rd = sem rs1#rs
      /\ forall r, data_preg r = true -> r <> rd -> r <> RAX -> 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_addrmode32 ge a rs1 = eval_addrmode32 ge a rs2.

Lemma mk_storebyte_correct:
  forall addr r k c rs1 m1 m2,
  mk_storebyte addr r k = OK c ->
  Mem.storev Mint8unsigned m1 (eval_addrmode ge addr rs1) (rs1 r) = Some m2 ->
  exists rs2,
    exec_straight ge fn c rs1 m1 (storev_fp Mint8unsigned (eval_addrmode ge addr rs1)) k rs2 m2
    /\ forall r, data_preg r = true -> preg_notin r (if Archi.ptr64 then nil else AX :: CX :: nil) -> rs2#r = rs1#r.


Remark eval_addrmode_indexed:
  forall (base: ireg) ofs (rs: regset),
  match rs#base with Vptr _ _ => True | _ => False end ->
  eval_addrmode ge (Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs))) rs = Val.offset_ptr rs#base ofs.

Ltac loadind_correct_solve :=
  match goal with
  | H: Error _ = OK _ |- _ => discriminate H
  | H: OK _ = OK _ |- _ => inv H
  | H: match ?x with _ => _ end = OK _ |- _ => destruct x eqn:?; loadind_correct_solve
  | _ => idtac
  end.

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.offset_ptr rs#base ofs) = Some v ->
  exists rs',
     exec_straight ge fn c rs m (loadv_fp (chunk_of_type ty) (Val.offset_ptr rs#base ofs)) 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.offset_ptr rs#base ofs) (rs#(preg_of src)) = Some m' ->
  exists rs',
     exec_straight ge fn c rs m (storev_fp (chunk_of_type ty) (Val.offset_ptr rs#base ofs)) k rs' m'
  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r.


Lemma transl_addressing_mode_32_correct:
  forall addr args am (rs: regset) v,
  transl_addressing addr args = OK am ->
  eval_addressing32 ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
  Val.lessdef v (eval_addrmode32 ge am rs).

Lemma transl_addressing_mode_64_correct:
  forall addr args am (rs: regset) v,
  transl_addressing addr args = OK am ->
  eval_addressing64 ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
  Val.lessdef v (eval_addrmode64 ge am rs).

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

Lemma normalize_addrmode_32_correct:
  forall am rs, eval_addrmode32 ge (normalize_addrmode_32 am) rs = eval_addrmode32 ge am rs.

Lemma normalize_addrmode_64_correct:
  forall am rs,
  eval_addrmode64 ge am rs =
  match normalize_addrmode_64 am with
  | (am', None) => eval_addrmode64 ge am' rs
  | (am', Some delta) => Val.addl (eval_addrmode64 ge am' rs) (Vlong delta)
  end.


Lemma loc_union_2:
  forall ls, Locs.union ls ls = ls.
Lemma fp_union_2:
  forall fp, FP.union fp fp = fp.

Ltac SimplifFP :=
  match goal with
  | H: match ?x with _ => _ end = Some _ |- _ => destruct x eqn:C; try inv C; try discriminate
  | H: ?x = Some _ |- context[?x] => destruct x eqn:C; try inv C; try discriminate
  | |- match ?x with _ => _ end = _ => destruct x eqn:C; try inv C; try discriminate
  | |- context[FP.union ?fp empfp] => rewrite FP.fp_union_emp; auto
  | |- context[FP.union ?fp ?fp] => rewrite fp_union_2; auto
  end.

Ltac SimplifFPs := repeat SimplifFP.

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


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 empfp k rs2 m
  /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
  /\ forall r, data_preg r = true -> r <> RAX /\ r <> RCX -> 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 empfp k rs2 m
  /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
  /\ forall r, data_preg r = true -> r <> RAX /\ r <> RCX -> 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 | auto ]
  | split; [ Simplifs | intros; Simplifs ]].

Lemma transl_op_correct:
  forall op args res k c (rs: regset) m v fp,
  transl_op op args res k = OK c ->
  eval_operation ge (rs#RSP) op (map rs (map preg_of args)) m = Some v ->
  eval_operation_fp ge (rs#RSP) op (map rs (map preg_of args)) m = Some fp ->
  exists rs',
     exec_straight ge fn c rs m fp 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#RSP) 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 (loadv_fp chunk a) 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#RSP) 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 (storev_fp chunk a) k rs' m'
  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.

End CONSTRUCTORS.