Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Ast.
Require Import Integers.
Require Import Floats.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import TSOmachine.
Require Import Simulations.
Require Import TSOsimulation.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Machconcr.
Require Import Machtyping.
Require Import Asm.
Require Import Asmgen.
Require Import Asmgenretaddr.
Require Import Asmgenproof1.
Require Import Memcomp Traces.
Require Import Libtactics.

Definition genv_rel : Mach.genv -> Asm.genv -> Prop :=
 (fun x y => Genv.genv_match (fun a b => transf_fundef a = OK b) y x).

Section PRESERVATION.

Variable ge: Mach.genv.
Variable tge: Asm.genv.
Hypothesis TRANSF: genv_rel ge tge.

Let lts := (mklts thread_labels (Machconcr.mc_step ge)).
Let tlts := (mklts thread_labels (Asm.x86_step tge)).

Definition wt_genv :=
  forall f, match (Genv.find_funct ge f) with
    | Some x => wt_fundef x
    | None => True
    end.

Hypothesis WTGENV : wt_genv.

Lemma symbols_preserved:
  forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.

Lemma function_ptr_translated:
  forall {v f}
    (H: Genv.find_funct_ptr ge v = Some f),
  exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = Errors.OK tf.

Lemma functions_transl:
  forall f tf b,
    Genv.find_funct_ptr ge b = Some (Internal f) ->
    transf_function f = OK tf ->
    Genv.find_funct_ptr tge b = Some (Internal tf).

Lemma functions_transl_no_overflow:
  forall f sig tf b,
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  transf_function f = OK (sig,tf) ->
  code_size tf <= Int.max_unsigned.

Hint Immediate functions_transl_no_overflow : x86gen.


Inductive transl_code_at_pc: val -> Mach.function -> Mach.code ->
                                    Asm.code -> Asm.code -> Prop :=
  transl_code_at_pc_intro:
    forall b ofs f c sig tf tc
      (GFUN: Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f))
      (HTF: transf_function f = OK (sig,tf))
      (HTF: transl_code f c = OK tc)
      (GOFS: code_tail (Int.unsigned ofs) tf tc),
    transl_code_at_pc (Vptr (Ptr b ofs)) f c tf tc.

Hint Resolve transl_code_at_pc_intro: x86gen.


Lemma return_address_offset_correct:
  forall b ofs f c tf tc ofs',
  transl_code_at_pc (Vptr (Ptr b ofs)) f c tf tc ->
  return_address_offset f c ofs' ->
  ofs' = ofs.

Proof of semantic preservation

Inductive match_stack: list Machconcr.stackframe -> Prop :=
  | match_stack_nil:
      match_stack nil
  | match_stack_cons: forall fb sp ra c s f tf tc b ofs,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      wt_function f ->
      incl c f.(fn_code) ->
      transl_code_at_pc (Vptr ra) f c tf tc ->
      ra <> nullptr ->
      ra = Ptr (Int.unsigned b) ofs ->
      fb = Ptr 0 b ->
      match_stack s ->
      match_stack (Stackframe fb sp ra c :: s).

Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
  | match_states_intro:
      forall s fb sp c ms stkr rs f tf tc b ofs
        (STACKS: match_stack s)
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (WTF: wt_function f)
        (INCL: incl c f.(fn_code))
        (ErsEIP: rs EIP = Vptr (Ptr (Int.unsigned b) ofs))
        (Efb: fb = Ptr 0 b)
        (AT: transl_code_at_pc (rs EIP) f c tf tc)
        (AG: agree ms (Vptr sp) rs),
      match_states (Machconcr.State s fb sp c stkr ms)
                   (State rs XPEdone stkr)

  | match_states_call:
      forall s sp ms stkr rs b ofs
        (STACKS: match_stack s)
        (AG: agree ms (Vptr sp) rs)
        (AT: rs EIP = Vptr (Ptr (Int.unsigned ofs) Int.zero)),
      match_states (Machconcr.Callstate s (Ptr b ofs) sp stkr ms)
                   (State rs XPEdone stkr)

  | match_states_return_internal:
      forall s ms sp stkr (rs : regset) f c ofs b tc sig
        (STACKS: match_stack s)
        (AG: agree ms (Vptr sp) rs)

        (INCL: incl c f.(fn_code))

        (AT2: rs EIP = Vptr (Ptr b ofs))
        (AT3: Genv.find_funct_ptr tge (Ptr 0 (Int.repr b)) = Some (Internal (sig,tc)))
        (AT4: find_instr (Int.unsigned ofs) tc = Some (Xret (Cint Int.zero))),

      match_states (Machconcr.Returnstate s sp stkr ms)
                   (State rs XPEdone stkr)

  | match_states_blocked:
      forall s ms sp rs b ofs ef efsig stkr
        (STACKS: match_stack s)
        (AG: agree ms (Vptr sp) rs)
        (AT2: rs EIP = Vptr (Ptr b ofs))
        (AT3: Genv.find_funct_ptr tge (Ptr 0 (Int.repr b)) = Some (External ef))
        (Eefsig : efsig = ef.(ef_sig)),
      match_states (Machconcr.Blockedstate s sp stkr ms efsig)
                   (Asm.Blockedstate rs stkr efsig)

  | match_states_return_external:
      forall s ms sp stkr (rs : regset) ofs b ef
        (STACKS: match_stack s)
        (AG: agree ms (Vptr sp) rs)

        (AT2: rs EIP = Vptr (Ptr b ofs))
        (AT3: Genv.find_funct_ptr tge (Ptr 0 (Int.repr b)) = Some (External ef)),

      match_states (Machconcr.Returnstate s sp stkr ms)
                   (Asm.ReturnExternal rs stkr)

  | match_initstate:
      forall f args args'
      (LD: Val.lessdef_list args args'),
      match_states (Machconcr.Initstate f args)
                   (Asm.Initstate f args')
  | match_initargsstate:
      forall ms sp rs f args args' locs stkr
        (LD: Val.lessdef_list args args')
        (AG: agree ms (Vptr sp) rs),
      match_states (Machconcr.Initargsstate f args locs sp stkr ms)
                   (Asm.Initargsstate f args' locs stkr rs)
  | match_freestackstate:
      forall stkr,
      match_states (Machconcr.Freestackstate stkr)
                   (Asm.Freestackstate stkr)
  | match_exitstate:
      match_states (Machconcr.Exitstate)
                   (Asm.Exitstate)

  | match_states_error:
      forall s,
      match_states Machconcr.Errorstate s.


Definition bsim_rel := @bsr _ lts tlts match_states.
Definition bsim_order := @bsc _ tlts.

Lemma init_fun_funsig_eq:
  forall pfn fn,
  Genv.find_funct_ptr ge pfn = Some fn ->
  exists tfn,
    Genv.find_funct_ptr tge pfn = Some tfn /\
    Mach.funsig fn = funsig tfn.

Hypothesis find_function_block_0:
  forall b ofs,
    match Genv.find_funct_ptr ge (Ptr b ofs) with
      | Some _ => b = 0
      | None => True
    end.


Ltac rgss := rewrite Pregmap.gss.
Ltac rgso := rewrite Pregmap.gso; [|auto with x86gen].

Ltac gs_simpl :=
  repeat (first [rewrite nextinstr_inv; [|done] | rewrite Pregmap.gso; [|done||congruence]
                |rewrite Pregmap.gss]; try done).

Ltac gs_simpl_safe :=
  repeat (first [rewrite nextinstr_inv; [|done] | rewrite Pregmap.gso; [|done||congruence]];
          try done).

Ltac des_teed := destruct thread_event_eq_dec; [auto|vauto].

Ltac unfold_step := simpl; unfold x86_step, xstep_fn, exec_pex_instr.

Ltac try_destruct_args :=
  match goal with
  | args: list mreg,
    Htc: transl_code _ _ = OK _ |- _ =>
      destruct args; monadInv Htc; try destruct args; clarify
  | _ => idtac
  end.

Ltac find_current_instruction :=
  match goal with
  | AT: transl_code_at_pc ?reip _ _ _ _ |- _ =>
      let Heip := fresh "Heip" in
        destruct reip as [] _eqn: Heip; inv AT; clarify'; try_destruct_args
  end.

Ltac reduce_weakstep_2 :=
  match goal with
  | GOFS: code_tail _ _ _ |- _ =>
     rewrite (find_instr_tail _ _ _ _ GOFS); simpl
  end.

Lemma nextinstr1:
  forall rs, (nextinstr rs) EIP = Val.add (rs EIP) Vone.

Lemma val_incr_pointer:
  forall b ofs, Val.add (Vptr (Ptr b ofs)) Vone = Vptr (Ptr b (Int.add ofs Int.one)).

Ltac reduce_internal Heip th :=
  match goal with
  | GFUN: Genv.find_funct_ptr _ _ = _,
    HTF: transf_function _ = OK ?sf |- _ =>
      eapply th; unfold_step;
      repeat first [rewrite nextinstr1 | rewrite Pregmap.gso; [|done]];
      try (rewrite Heip, ?val_incr_pointer, (functions_transl _ _ _ GFUN HTF));
      try reduce_weakstep_2
  end.

Ltac reduce_weakstep Heip :=
  reduce_internal Heip step_weakstep.

Ltac reduce_step_weakstep Heip :=
  reduce_internal Heip steptau_weakstep; des_teed; reduce_internal Heip step_weakstep.

Ltac adjust_nextinstr :=
  match goal with
  | GOFS: code_tail _ _ _ |- _ =>
     eapply code_tail_next_int in GOFS; [|eby eapply functions_transl_no_overflow]
  end.



Lemma exec_Mlabel_correct:
  forall s f sp lbl c stkr rs t
    (MS: match_states (Machconcr.State s f sp (Mlabel lbl :: c) stkr rs) t),
  (exists t' : St tlts,
     weakstep tlts t TEtau t' /\
     match_states (Machconcr.State s f sp c stkr rs) t').

Lemma exec_Mgetstack_correct:
  forall v ty s f sp ofs dst c stkr rs t ptr chunk
    (Eptr : ptr = (sp + ofs)%pointer)
    (Echunk : chunk = chunk_of_ty ty)
    (HT : Val.has_type v (type_of_chunk chunk))
    (MS: match_states
          (Machconcr.State s f sp (Mgetstack ofs ty dst :: c) stkr rs) t),
   exists t' : state,
     weakstep tlts t (TEmem (MEread ptr chunk v)) t' /\
     (forall v' : val,
      Val.lessdef v' v ->
      exists s'' : Machconcr.state,
        mc_step ge
          (Machconcr.State s f sp (Mgetstack ofs ty dst :: c) stkr rs)
          (TEmem (MEread ptr chunk v')) s'' /\ match_states s'' t').

Lemma conv_lessdef_2:
  forall v ty,
    Val.lessdef (Val.conv v ty) v.

Lemma lessdef_trans:
  forall v1 v2 v3,
    Val.lessdef v1 v2 ->
    Val.lessdef v2 v3 ->
    Val.lessdef v1 v3.

Lemma exec_Msetstack_correct:
  forall t s f sp src ofs ty c stkr rs ptr chunk v
    (Eptr : ptr = (sp + ofs)%pointer)
    (Echunk : chunk = chunk_of_ty ty)
    (Ev : v = Val.conv (rs src) (type_of_chunk chunk))
    (HT : Val.has_type v (type_of_chunk chunk))
    (MS : match_states
           (Machconcr.State s f sp (Msetstack src ofs ty :: c) stkr rs) t),
   (exists t' : state,
      exists v' : val,
        Val.lessdef (cast_value_to_chunk chunk v) v' /\
        weakstep tlts t (TEmem (MEwrite ptr chunk v')) t' /\
        match_states (Machconcr.State s f sp c stkr rs) t').

Lemma exec_Mgetparam_correct:
  forall ptr sp ofs chunk ty v s f fb dst c stkr rs t
    (FF : Genv.find_funct_ptr ge fb = Some (Internal f))
    (Eptr : ptr = (sp + parent_offset f + ofs)%pointer)
    (Echunk : chunk = chunk_of_ty ty)
    (HT : Val.has_type v (type_of_chunk chunk))
    (MS : match_states
          (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) stkr rs) t),
   (exists t' : state,
      weakstep tlts t (TEmem (MEread ptr chunk v)) t' /\
      (forall v' : val,
       Val.lessdef v' v ->
       exists s'' : Machconcr.state,
         mc_step ge
           (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) stkr rs)
           (TEmem (MEread ptr chunk v')) s'' /\ match_states s'' t')).

Lemma transl_addressing_mode_correct:
  forall addr args (am: xmem) (ms: mreg -> val) (rs: regset) v (sp: pointer)
    (AG: agree ms (Vptr sp) rs)
    (Hta: transl_addressing addr args = OK am)
    (Hea: eval_addressing ge (Some sp) addr ms ## args = Some v),
    ea tge rs am = v.

Lemma ea_nextinstr:
  forall rs am, ea tge (nextinstr rs) am = ea tge rs am.


Lemma exec_Mload_correct:
  forall t s f sp chunk addr args dst c stkr rs rs' a v
    (EVAL : eval_addressing ge (Some sp) addr rs ## args = Some (Vptr a))
    (HT : Val.has_type v (type_of_chunk chunk))
    (Ers' : rs' = Regmap.set dst v (undef_temps rs))
    (MS : match_states
           (Machconcr.State s f sp (Mload chunk addr args dst :: c) stkr rs) t),
   (exists t' : state,
      weakstep tlts t (TEmem (MEread a chunk v)) t' /\
      (forall v' : val,
       Val.lessdef v' v ->
       exists s'' : Machconcr.state,
         mc_step ge
           (Machconcr.State s f sp (Mload chunk addr args dst :: c) stkr rs)
           (TEmem (MEread a chunk v')) s'' /\ match_states s'' t')).

Lemma exec_Mstore_correct:
  forall t s f sp chunk addr args src c stkr rs a v
    (EVAL : eval_addressing ge (Some sp) addr rs ## args = Some (Vptr a))
    (Ev : v = Val.conv (rs src) (type_of_chunk chunk))
    (MS : match_states
           (Machconcr.State s f sp (Mstore chunk addr args src :: c) stkr rs) t),
   (exists t' : state,
      exists v' : val,
        Val.lessdef (cast_value_to_chunk chunk v) v' /\
        weakstep tlts t (TEmem (MEwrite a chunk v')) t' /\
        match_states (Machconcr.State s f sp c stkr (undef_temps rs)) t').

Lemma exec_Mcall_correct:
  forall t s fb sp sig ros c stkr rs f f' roffs
    (FF : find_function_ptr ge ros rs = Some f')
    (GFF : Genv.find_funct_ptr ge fb = Some (Internal f))
    (RA : return_address_offset f c roffs)
    (MS : match_states (Machconcr.State s fb sp (Mcall sig ros :: c) stkr rs) t)
    (RI : range_inside
           (Ptr.sub_int sp (Int.repr Stacklayout.fe_retaddrsize), Int.zero)
           stkr),
   (exists t' : state,
      exists v' : val,
        Val.lessdef (Vptr (Ptr (Int.unsigned (Ptr.offset fb)) roffs)) v' /\
        weakstep tlts t
          (TEmem
             (MEwrite (Ptr.sub_int sp (Int.repr Stacklayout.fe_retaddrsize))
                Mint32 v')) t' /\
        match_states
          (Callstate
             (Stackframe fb sp (Ptr (Int.unsigned (Ptr.offset fb)) roffs) c
              :: s) f' (Ptr.sub_int sp (Int.repr Stacklayout.fe_retaddrsize))
             stkr rs) t').

Ltac unfold_flags :=
  unfold write_int_result,
         write_result_flags_only,
         write_logical_result,
         write_logical_result_flags_only,
         write_result_erase_flags,
         write_arith_eflags, write_arith_eflags_ZF,
         write_logical_eflags, erase_eflags, write_eflag.

Lemma exec_Mreturn_correct:
  forall t s fb sp c stkr rs sp' f'
    (H : Genv.find_funct_ptr ge fb = Some (Internal f'))
    (H0 : sp' = (sp + total_framesize f')%pointer)
    (INSIDE: range_inside (sp', Int.zero) stkr)
    (MS : match_states (Machconcr.State s fb sp (Mreturn :: c) stkr rs) t),
  (exists t' : state,
     weakstep tlts t TEtau t' /\ match_states (Returnstate s sp' stkr rs) t').

Lemma exec_function_internal_correct:
  forall t s fb stkr rs f sp sp'
    (H : Genv.find_funct_ptr ge fb = Some (Internal f))
    (H0 : sp' = Ptr.sub_int sp (total_framesize f))
    (H1 : range_inside (sp', Int.zero) stkr)
    (MS : match_states (Callstate s fb sp stkr rs) t),
  (exists t' : state,
     weakstep tlts t TEtau t' /\
     match_states (Machconcr.State s fb sp' (fn_code f) stkr rs) t').

Lemma exec_return_correct:
  forall t s f sp ra c stkr rs sp'
    (H : sp' = (sp + Int.repr Stacklayout.fe_retaddrsize)%pointer)
    (MS : match_states (Returnstate (Stackframe f sp' ra c :: s) sp stkr rs) t),
  (exists t' : state,
     weakstep tlts t (TEmem (MEread sp Mint32 (Vptr ra))) t' /\
     (forall v' : val,
      Val.lessdef v' (Vptr ra) ->
      exists s'' : Machconcr.state,
        mc_step ge (Returnstate (Stackframe f sp' ra c :: s) sp stkr rs)
          (TEmem (MEread sp Mint32 v')) s'' /\ match_states s'' t')).


Ltac destruct_code_tail_i_zero :=
  match goal with
  | GOFS: code_tail _ _ (if Int.eq_dec ?i ?j then _ else _) |- _ =>
     destruct (Int.eq_dec i j) as [] _eqn:Hizero; clear Hizero
  | _ => idtac
  end.

Ltac try_destruct_args_cond :=
   match goal with
  | args: list mreg,
    Htc: transl_cond _ _ _ = OK _ |- _ =>
      destruct args; monadInv Htc
  | _ => idtac
  end.

Lemma unsigned_mod_mod :
  forall ofs sig tf c tc f p
   (GOFS : code_tail (Int.unsigned ofs) tf (c::tc))
   ( HTF : transf_function f = OK (sig, tf))
   (FIND : Genv.find_funct_ptr ge p = Some (Internal f)),
  (Int.unsigned ofs + 1 mod Int.modulus) mod Int.modulus = Int.unsigned ofs + 1.

Translation of Conditionals

Definition b3_moredef (b1 : bool3) (b2: bool) :=
  match b1 with
    | b3_true => b2
    | b3_false => negb b2
    | b3_unknown => false
  end.

Lemma cmp_lt:
  forall i j,
      (vi_eq (Val.of_bool (int_msb (Int.sub i j)))
        (word_signed_overflow_sub i j))
    = (if Int.lt i j then b3_false else b3_true).

Lemma cmp_ltu0:
  forall i j, Int.eq (sub_borrow i j) Int.zero = negb (Int.ltu i j).

Lemma cmp_ltu1:
  forall i j, Int.eq (sub_borrow i j) Int.one = Int.ltu i j.


Lemma transl_cond_float_correct:
  forall cond op args ms rs b stkr k fb ofs tf tc sig
    (Hec : eval_condition cond ms ## args = Some b)
    (TRAN : transl_cond cond args k = OK tc)
    (FIND : Genv.find_funct_ptr tge (Ptr 0 fb) = Some (Internal (sig,tf)))
    (AG : forall r : mreg, Val.lessdef (ms r) (rs (preg_of r)))
    (Heip : rs EIP = Vptr (Ptr (Int.unsigned fb) ofs))
    (GOFS : code_tail (Int.unsigned ofs) tf tc)
    (COND : cond = Ccompf op \/ cond = Cnotcompf op),
  exists rs',
     x86_step tge (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr)
  /\ b3_moredef (read_cond rs' (testcond_for_cond cond)) b
  /\ rs' EIP = Val.add (rs EIP) Vone
  /\ forall r, nontemp_preg r = true -> rs' # r = rs # r.


Lemma transl_cond_mask_correct:
  forall cond i args ms rs b stkr k fb ofs tf tc sig
    (Hec : eval_condition cond ms ## args = Some b)
    (TRAN : transl_cond cond args k = OK tc)
    (FIND : Genv.find_funct_ptr tge (Ptr 0 fb) = Some (Internal (sig,tf)))
    (AG : forall r : mreg, Val.lessdef (ms r) (rs (preg_of r)))
    (Heip : rs EIP = Vptr (Ptr (Int.unsigned fb) ofs))
    (GOFS : code_tail (Int.unsigned ofs) tf tc)
    (COND : cond = Cmaskzero i \/ cond = Cmasknotzero i),
  exists rs',
     x86_step tge (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr)
  /\ b3_moredef (read_cond rs' (testcond_for_cond cond)) b
  /\ rs' EIP = Val.add (rs EIP) Vone
  /\ forall r, nontemp_preg r = true -> rs' # r = rs # r.

Lemma eq_sub_zero_eq:
  forall i i', Int.eq (Int.sub i i') Int.zero = Int.eq i i'.

Lemma Ptr_eq_simpl:
  forall a b c d, Ptr.eq (Ptr a b) (Ptr c d) = (if zeq a c then Int.eq b d else false).

Lemma transl_cond_int_correct:
  forall cond op i args ms rs b stkr k fb ofs tf tc sig
    (Hec : eval_condition cond ms ## args = Some b)
    (TRAN : transl_cond cond args k = OK tc)
    (FIND : Genv.find_funct_ptr tge (Ptr 0 fb) = Some (Internal (sig,tf)))
    (AG : forall r : mreg, Val.lessdef (ms r) (rs (preg_of r)))
    (Heip : rs EIP = Vptr (Ptr (Int.unsigned fb) ofs))
    (GOFS : code_tail (Int.unsigned ofs) tf tc)
    (COND : cond = Ccomp op \/ cond = Ccompu op
            \/ cond = Ccompimm op i \/ cond = Ccompuimm op i),
  exists rs',
     x86_step tge (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr)
  /\ b3_moredef (read_cond rs' (testcond_for_cond cond)) b
  /\ rs' EIP = Val.add (rs EIP) Vone
  /\ forall r, nontemp_preg r = true -> rs' # r = rs # r.

Lemma transl_cond_correct:
  forall cond args c ms rs sp b stkr lbl fb s
    (Hec : eval_condition cond ms ## args = Some b)
    (MS : match_states
             (Machconcr.State s fb sp (Mcond cond args lbl :: c) stkr ms)
             (State rs XPEdone stkr)),
  exists rs',
     x86_step tge (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr)
  /\ b3_moredef (read_cond rs' (testcond_for_cond cond)) b
  /\ rs' EIP = Val.add (rs EIP) Vone
  /\ forall r, nontemp_preg r = true -> rs' # r = rs # r.

Lemma transl_cmp_correct:
  forall cond args c ms rs sp b stkr m fb s
    (Hec : eval_condition cond ms ## args = Some b)
    (MS : match_states
             (Machconcr.State s fb sp (Mop (Ocmp cond) args m :: c) stkr ms)
             (State rs XPEdone stkr)),
  exists rs',
     x86_step tge (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr)
  /\ b3_moredef (read_cond rs' (testcond_for_cond cond)) b
  /\ rs' EIP = Val.add (rs EIP) Vone
  /\ forall r, nontemp_preg r = true -> rs' # r = rs # r.

Lemma exec_Mcond_true_correct:
  forall t s fb f sp cond args lbl c stkr rs c'
    (Hec : eval_condition cond rs ## args = Some true)
    (Hff : Genv.find_funct_ptr ge fb = Some (Internal f))
    (Hfl : Mach.find_label lbl (fn_code f) = Some c')
    (MS : match_states
           (Machconcr.State s fb sp (Mcond cond args lbl :: c) stkr rs) t),
  (exists t' : state,
     weakstep tlts t TEtau t' /\
     match_states (Machconcr.State s fb sp c' stkr (undef_temps rs)) t').

Lemma exec_Mcond_false_correct:
  forall t s f sp cond args lbl c stkr rs
    (Hec : eval_condition cond rs ## args = Some false)
    (MS : match_states
         (Machconcr.State s f sp (Mcond cond args lbl :: c) stkr rs) t),
   (exists t' : state,
      weakstep tlts t TEtau t' /\
      match_states (Machconcr.State s f sp c stkr (undef_temps rs)) t').

Plain operations

Lemma exec_binopf_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oaddf \/ op = Osubf \/ op = Omulf \/ op = Odivf),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').


Lemma exec_boolop_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oand \/ op = Oor \/ op = Oxor),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').

Lemma exec_boolopimm_correct:
  forall t s f sp op args res c stkr rs v i
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oandimm i \/ op = Oorimm i \/ op = Oxorimm i),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').


Lemma ltu32_fits_in_8bit:
  forall i, Int.ltu i (Int.repr 32) -> Int.zero_ext 8 i = i.

Lemma exec_shiftop_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oshl \/ op = Oshr \/ op = Oshru),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').

Lemma exec_shiftopimm_correct:
  forall t s f sp op args res c stkr rs v i
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oshlimm i \/ op = Oshrimm i \/ op = Oshruimm i \/ op = Ororimm i),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').


Lemma exec_cast_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Ocast8signed \/ op = Ocast8unsigned \/ op = Ocast16signed \/ op = Ocast16unsigned),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').


Lemma exec_divs_body_correct:
  forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf
  (NEQ : arg <> EDX)
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr b ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf (Xcltd :: Xmonop Xidiv (Xr arg) :: c)),
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EAX = Val.divs (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r).

Lemma exec_mods_body_correct:
  forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf
  (NEQ : arg <> EDX)
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr b ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf (Xcltd :: Xmonop Xidiv (Xr arg) :: c)),
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EDX = Val.mods (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r).

Lemma exec_divu_body_correct:
  forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf
  (NEQ : arg <> EDX)
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr b ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf
             (Xxor_self EDX :: Xmonop Xdiv (Xr arg) :: c)),
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EAX = Val.divu (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r).

Lemma exec_modu_body_correct:
  forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf
  (NEQ : arg <> EDX)
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr b ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf
             (Xxor_self EDX :: Xmonop Xdiv (Xr arg) :: c)),
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EDX = Val.modu (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r).


Lemma exec_mk_div_correct:
  forall op1 op2 compf f (arg res: ireg) c stkr rs b ofs k sig tf tc
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr (Int.unsigned b))) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr (Int.unsigned b) ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf tc)
  (TRANSL: transl_code f c = OK k)
  (NEres : ESP <> res)
  (NEarg : ESP <> arg)
  (DIV : mk_div op1 op2 res arg k = OK tc)
  (EXEC_BODY:
     forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf,
      arg <> EDX ->
      transf_function f = OK (sig, tf) ->
      Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f) ->
      rs # EIP = Vptr (Ptr b ofs) ->
      code_tail (Int.unsigned ofs) tf (op1 :: Xmonop op2 (Xr arg) :: c) ->
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EAX = compf (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r)),
   exists rs', exists ofs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     transl_code_at_pc (rs' EIP) f c tf k /\
     rs' res = compf (rs res) (rs arg) /\
     rs' EIP = Vptr (Ptr (Int.unsigned b) ofs') /\
     rs' ESP = rs ESP /\
     (forall r, nontemp_preg r -> r <> res -> rs' r = rs r).


Lemma exec_mk_mod_correct:
  forall op1 op2 compf f (arg res: ireg) c stkr rs b ofs k sig tf tc
  (HTF : transf_function f = OK (sig, tf))
  (GFUN : Genv.find_funct_ptr ge (Ptr 0 (Int.repr (Int.unsigned b))) = Some (Internal f))
  (Heip : rs # EIP = Vptr (Ptr (Int.unsigned b) ofs))
  (GOFS : code_tail (Int.unsigned ofs) tf tc)
  (TRANSL: transl_code f c = OK k)
  (NEres : ESP <> res)
  (NEarg : ESP <> arg)
  (DIV : mk_mod op1 op2 res arg k = OK tc)
  (EXEC_BODY:
     forall (rs: regset) (arg: ireg) f c stkr sig b ofs tf,
      arg <> EDX ->
      transf_function f = OK (sig, tf) ->
      Genv.find_funct_ptr ge (Ptr 0 (Int.repr b)) = Some (Internal f) ->
      rs # EIP = Vptr (Ptr b ofs) ->
      code_tail (Int.unsigned ofs) tf (op1 :: Xmonop op2 (Xr arg) :: c) ->
   exists rs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     rs' EDX = compf (rs EAX) (rs arg) /\
     rs' EIP = Vptr (Ptr b (Int.add (Int.add ofs Int.one) Int.one)) /\
     rs' ESP = rs ESP /\
     (forall r,
        important_preg r ->
        r <> EAX -> r <> EDX ->
        rs' r = rs r)),
   exists rs', exists ofs',
     weakstep tlts (State rs XPEdone stkr) TEtau (State rs' XPEdone stkr) /\
     transl_code_at_pc (rs' EIP) f c tf k /\
     rs' res = compf (rs res) (rs arg) /\
     rs' EIP = Vptr (Ptr (Int.unsigned b) ofs') /\
     rs' ESP = rs ESP /\
     (forall r, nontemp_preg r -> r <> res -> rs' r = rs r).


Lemma exec_div_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Odiv \/ op = Odivu),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').

Lemma exec_mod_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Omod \/ op = Omodu),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').

Lemma exec_castf_correct:
  forall t s f sp op args res c stkr rs v
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Osingleoffloat \/ op = Ointoffloat \/ op = Ofloatofint \/ op = Ofloatofintu),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').



Lemma exec_shrximm_correct:
  forall t s f sp op args res c stkr rs v i
   (EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t)
   (OP: op = Oshrximm i),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').

Tactic Notation "exec_op_cases" tactic(first) tactic(c) :=
    first; [
      c "exec_Omove" |
      c "exec_Ointconst" |
      c "exec_Ofloatconst" |
      c "exec_Ocast8signed" |
      c "exec_Ocast8unsigned" |
      c "exec_Ocast16signed" |
      c "exec_Ocast16unsigned" |
      c "exec_Oneg" |
      c "exec_Osub" |
      c "exec_Omul" |
      c "exec_Omulimm" |
      c "exec_Odiv" |
      c "exec_Odivu" |
      c "exec_Omod" |
      c "exec_Omodu" |
      c "exec_Oand" |
      c "exec_Oandimm" |
      c "exec_Oor" |
      c "exec_Oorimm" |
      c "exec_Oxor" |
      c "exec_Oxorimm" |
      c "exec_Oshl" |
      c "exec_Oshlimm" |
      c "exec_Oshr" |
      c "exec_Oshrimm" |
      c "exec_Oshrximm" |
      c "exec_Oshru" |
      c "exec_Oshruimm" |
      c "exec_Ororimm" |
      c "exec_Olea" |
      c "exec_Onegf" |
      c "exec_Oaddf" |
      c "exec_Osubf" |
      c "exec_Omulf" |
      c "exec_Odivf" |
      c "exec_Osingleoffloat" |
      c "exec_Ointoffloat" |
      c "exec_Ofloatofint" |
      c "exec_Ointuoffloat" |
      c "exec_Ofloatofintu" |
      c "exec_Ocmp"].



Lemma exec_Mop_correct:
  forall t s f sp op args res c stkr rs v
   ( EVAL : eval_operation ge (Some sp) op rs ## args = Some v)
   (MS : match_states (Machconcr.State s f sp (Mop op args res :: c) stkr rs) t),
 (exists t' : state,
    weakstep tlts t TEtau t' /\
    match_states
      (Machconcr.State s f sp c stkr (Regmap.set res v (undef_op op rs)))
      t').


Lemma transf_step_correct:
   forward_sim_with_undefs2 lts tlts match_states (fun _ _ : St lts => False).


Lemma my_backward_sim_with_undefs:
  @backward_sim_with_undefs thread_labels lts tlts te_ldo te_ldi
     (@bsr thread_labels lts tlts match_states) (@bsc thread_labels tlts).

Lemma lessdef_list_length:
  forall {l l'} (LD : Val.lessdef_list l l'),
  length l = length l'.

Lemma init_sim_succ:
  forall {p vals vals' tinit}
    (INIT: x86_init tge p vals = Some tinit)
    (LD: Val.lessdef_list vals' vals),
    exists sinit, mc_init ge p vals' = Some sinit /\ match_states sinit tinit.

Lemma init_sim_fail:
  forall p vals vals'
    (INIT: x86_init tge p vals = None)
    (LD: Val.lessdef_list vals' vals),
    mc_init ge p vals' = None.

End PRESERVATION.


Definition full_genv_rel ge tge :=
  genv_rel ge tge /\ wt_genv ge /\ (forall (b : Z) (ofs : int),
       match Genv.find_funct_ptr ge (Ptr b ofs) with
       | Some _ => b = 0%Z
       | None => True
       end).

Require Machtyping.

Definition asmgen_match_prg (p : mc_sem.(SEM_PRG))
                              (p' : x86_sem.(SEM_PRG)) : Prop :=
   Machtyping.wt_program p /\
   transf_program p = OK p'.

Theorem asmgen_sim : Sim.sim tso_mm tso_mm mc_sem x86_sem asmgen_match_prg.