Module AsmFacts

Require Import Smallstep.
Require Import Machregs.
Require Import Asm.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import Memtype.
Require Import Memory.
Require Import Archi.
Require Import Coqlib.
Require Import AST.
Require Import Globalenvs.
Require Import Events.
Require Import Values.
Require Import Conventions1.
Require Import Asmgen.
Require Asmgenproof0.
Require Import Errors.

Section WITHMEMORYMODEL.


  Existing Instance mem_accessors_default.

  Context {mem} `{external_calls_props: ExternalCallsProps mem}
          `{enable_builtins_instance: !EnableBuiltins (memory_model_ops:=memory_model_ops) mem}.

  Definition stack_invar (i: instruction) :=
    match i with
      Pallocframe _ _ _
    | Pfreeframe _ _
    | Pcall _ _
    | Pret => false
    | _ => true
    end.


  Definition asm_instr_no_rsp (i : Asm.instruction) : Prop :=
    stack_invar i = true ->
    forall (ge: Genv.t Asm.fundef unit) rs1 m1 rs2 m2 f init_stk,
      Asm.exec_instr init_stk ge f i rs1 m1 = Next rs2 m2 ->
      rs2 # RSP = rs1 # RSP.
  
  Definition written_regs i : list preg :=
    match i with
    | Pmov_rr rd _
    | Pmovl_ri rd _
    | Pmovq_ri rd _
    | Pmov_rs rd _
    | Pmovl_rm rd _
    | Pmovq_rm rd _ => IR rd :: nil
    | Pmovl_mr a rs
    | Pmovq_mr a rs => nil
    | Pmovsd_ff rd _
    | Pmovsd_fi rd _
    | Pmovsd_fm rd _ => FR rd :: nil
    | Pmovsd_mf a r1 => nil
    | Pmovss_fi rd _
    | Pmovss_fm rd _ => FR rd :: nil
    | Pmovss_mf a r1 => nil
    | Pfldl_m a => ST0 :: nil
    | Pfstpl_m a => ST0 :: nil
    | Pflds_m a => ST0 :: nil
    | Pfstps_m a => ST0 :: nil
    | Pxchg_rr r1 r2 => IR r1 :: IR r2 :: nil
    | Pmovb_mr a rs
    | Pmovw_mr a rs => nil
    | Pmovzb_rr rd _
    | Pmovzb_rm rd _
    | Pmovsb_rr rd _
    | Pmovsb_rm rd _
    | Pmovzw_rr rd _
    | Pmovzw_rm rd _
    | Pmovsw_rr rd _
    | Pmovsw_rm rd _
    | Pmovzl_rr rd _
    | Pmovsl_rr rd _
    | Pmovls_rr rd => IR rd :: nil
    | Pcvtsd2ss_ff rd _ => FR rd :: nil
    | Pcvtss2sd_ff rd _ => FR rd :: nil
    | Pcvttsd2si_rf rd _=> IR rd :: nil
    | Pcvtsi2sd_fr rd _ => FR rd :: nil
    | Pcvttss2si_rf rd _=> IR rd :: nil
    | Pcvtsi2ss_fr rd _ => FR rd :: nil
    | Pcvttsd2sl_rf rd _=> IR rd :: nil
    | Pcvtsl2sd_fr rd _ => FR rd :: nil
    | Pcvttss2sl_rf rd _ => IR rd :: nil
    | Pcvtsl2ss_fr rd _ => FR rd :: nil
    | Pleal rd _
    | Pleaq rd _
    | Pnegl rd
    | Pnegq rd
    | Paddl_ri rd _
    | Paddq_ri rd _
    | Psubl_ri rd _
    | Psubq_ri rd _
    | Psubl_rr rd _
    | Psubq_rr rd _
    | Pimull_rr rd _
    | Pimulq_rr rd _
    | Pimull_ri rd _
    | Pimulq_ri rd _ => IR rd :: nil
    | Pimull_r r1
    | Pimulq_r r1
    | Pmull_r r1
    | Pmulq_r r1 => IR RAX :: IR RDX :: nil
    | Pcltd
    | Pcqto => IR RDX :: nil
    | Pdivl r1
    | Pdivq r1
    | Pidivl r1
    | Pidivq r1 => IR RAX :: IR RDX :: nil
    | Pandl_rr rd _
    | Pandq_rr rd _
    | Pandl_ri rd _
    | Pandq_ri rd _
    | Porl_rr rd _
    | Porq_rr rd _
    | Porl_ri rd _
    | Porq_ri rd _
    | Pxorl_r rd
    | Pxorq_r rd
    | Pxorl_rr rd _
    | Pxorq_rr rd _
    | Pxorl_ri rd _
    | Pxorq_ri rd _
    | Pnotl rd
    | Pnotq rd
    | Psall_rcl rd
    | Psalq_rcl rd
    | Psall_ri rd _
    | Psalq_ri rd _
    | Pshrl_rcl rd
    | Pshrq_rcl rd
    | Pshrl_ri rd _
    | Pshrq_ri rd _
    | Psarl_rcl rd
    | Psarq_rcl rd
    | Psarl_ri rd _
    | Psarq_ri rd _
    | Pshld_ri rd _ _
    | Prorl_ri rd _
    | Prorq_ri rd _ => IR rd :: nil
    | Pcmpl_rr _ _
    | Pcmpq_rr _ _
    | Pcmpl_ri _ _
    | Pcmpq_ri _ _
    | Ptestl_rr _ _
    | Ptestq_rr _ _
    | Ptestl_ri _ _
    | Ptestq_ri _ _ => nil
    | Pcmov c rd _
    | Psetcc c rd => IR rd :: nil
    | Paddd_ff rd _
    | Psubd_ff rd _
    | Pmuld_ff rd _
    | Pdivd_ff rd _
    | Pnegd rd
    | Pabsd rd => FR rd :: nil
    | Pcomisd_ff r1 r2 => nil
    | Pxorpd_f rd (* xor with self = set to zero *)
    | Padds_ff rd _
    | Psubs_ff rd _
    | Pmuls_ff rd _
    | Pdivs_ff rd _
    | Pnegs rd
    | Pabss rd => FR rd :: nil
    | Pcomiss_ff r1 r2 => nil
    | Pxorps_f rd => FR rd :: nil
    | Pjmp_l _
    | Pjmp _ _
    | Pjcc _ _
    | Pjcc2 _ _ _ => nil
    | Pjmptbl r tbl => IR RAX :: IR RDX :: nil
    | Pcall ros sg => nil
    | Pret => nil
    | Pmov_mr_a _ _
    | Pmovsd_mf_a _ _ => nil
    | Pmov_rm_a rd _ => IR rd :: nil
    | Pmovsd_fm_a rd _ => FR rd :: nil

    | Plabel l => nil
    | Pallocframe _ _ _ => IR RAX :: IR RSP :: nil
    | Pfreeframe sz ofs_ra => IR RSP :: nil
    | Pload_parent_pointer rd _ => IR rd :: nil
    | Pbuiltin ef args res => nil
    | _ => nil
    end.

  Require Import AsmRegs.

  Ltac simpl_not_in NIN :=
    let H1 := fresh in
    let H2 := fresh in
    first [ apply Decidable.not_or in NIN; destruct NIN as [H1 H2]; simpl_not_in H2
          | idtac ].

  Lemma exec_load_rsp:
    forall F V (ge: _ F V) K m1 am rs1 f0 rs2 m2 sz,
      exec_load ge K m1 am rs1 f0 sz = Next rs2 m2 ->
      forall r,
        ~ In r (PC :: RA :: CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: f0 :: nil) ->
      rs2 r = rs1 r.

  Lemma exec_store_rsp:
    forall F V (ge: _ F V) K m1 am rs1 f0 rs2 m2 (l: list preg) sz,
      exec_store ge K m1 am rs1 f0 l sz = Next rs2 m2 ->
      forall r,
        ~ In r (PC :: RA :: CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: l) ->
      rs2 r = rs1 r.
  
  Lemma exec_instr_only_written_regs:
    forall (ge: Genv.t Asm.fundef unit) rs1 m1 rs2 m2 f i init_stk r,
      Asm.exec_instr init_stk ge f i rs1 m1 = Next rs2 m2 ->
      ~ In r (PC :: RA :: CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: written_regs i) ->
      rs2 # r = rs1 # r.

  Definition check_asm_instr_no_rsp i :=
    negb (in_dec preg_eq RSP (written_regs i)).

  Definition check_asm_code_no_rsp c : bool :=
    forallb (fun i => negb (stack_invar i) || check_asm_instr_no_rsp i) c.

  Lemma check_asm_instr_no_rsp_correct i:
    check_asm_instr_no_rsp i = true ->
    asm_instr_no_rsp i.
  
  Definition asm_code_no_rsp (c : Asm.code) : Prop :=
    forall i,
      In i c ->
      asm_instr_no_rsp i.

  Lemma check_asm_code_no_rsp_correct c:
    check_asm_code_no_rsp c = true ->
    asm_code_no_rsp c.


  Lemma preg_of_not_rsp:
    forall m x,
      preg_of m = x ->
      x <> RSP.
  
  Lemma ireg_of_not_rsp:
    forall m x,
      Asmgen.ireg_of m = OK x ->
      IR x <> RSP.

  Lemma freg_of_not_rsp:
    forall m x,
      Asmgen.freg_of m = OK x ->
      FR x <> RSP.


  
  Ltac solve_rs:=
    match goal with
    | |- not (@eq preg _ (IR RSP)) => solve [ eapply preg_of_not_rsp; eauto
                                     | eapply ireg_of_not_rsp; eauto
                                     | eapply freg_of_not_rsp; eauto
                                     | congruence ]
    | |- _ => idtac
    end.

  
  Lemma loadind_no_rsp:
    forall ir o t m ti i
      (IN : In i ti)
      (TI : loadind ir o t m nil = OK ti),
      ~ In (IR RSP) (written_regs i).

  Lemma storeind_no_rsp:
    forall ir o t m ti i
      (IN : In i ti)
      (TI : storeind ir o t m nil = OK ti),
      ~ In (IR RSP) (written_regs i).

  Ltac solve_in_regs :=
    repeat match goal with
           | H: mk_mov _ _ _ = _ |- _ => unfold mk_mov in H; repeat destr_in H
           | H: OK _ = OK _ |- _ => inv H
           | H: mk_intconv _ _ _ _ = _ |- _ => unfold mk_intconv in H
           | H: bind _ _ = _ |- _ => monadInv H
           | IN: In _ (_ :: _) |- _ => destruct IN as [IN | IN]; inv IN; simpl in *
           | IN: In _ (_ ++ _) |- _ => rewrite in_app in IN; destruct IN as [IN|IN]
           | OR: _ \/ _ |- _ => destruct OR as [OR|OR]; inv OR; simpl
           | |- ~ (_ \/ _) => apply Classical_Prop.and_not_or
           | |- ~ _ /\ ~ _ => split; auto
           | H: False |- _ => destruct H
           | H: In _ nil |- _ => destruct H
           | IN: In _ _ |- _ => repeat destr_in IN; simpl in *
           | _ => simpl in *; solve_rs; auto
           end.

  Lemma transl_cond_no_rsp:
    forall cond l c c' i
      (INV: stack_invar i = true)
      (TC : transl_cond cond l c = OK c')
      (IN: In i c'),
      ~ In (IR RSP) (written_regs i) \/ In i c.

  Lemma transl_op_no_rsp:
    forall op l r c' i
      (INV: stack_invar i = true)
      (TC : transl_op op l r nil = OK c')
      (IN: In i c'),
      ~ In (IR RSP) (written_regs i).

  Lemma transl_code_no_rsp:
    forall f c b c' i
      (INV: stack_invar i = true)
      (TC : transl_code f c b = OK c')
      (IN: In i c'),
      ~ In (IR RSP) (written_regs i).
  
  Lemma asmgen_no_change_rsp:
    forall f tf,
      transf_function f = OK tf ->
      check_asm_code_no_rsp (fn_code tf) = true.

      













  




  




  Definition asm_instr_no_stack (i : Asm.instruction) : Prop :=
    stack_invar i = true ->
    forall (ge: Genv.t Asm.fundef unit) rs1 m1 rs2 m2 f init_stk,
      Asm.exec_instr init_stk ge f i rs1 m1 = Next rs2 m2 ->
      Mem.stack m2 = Mem.stack m1 /\ (forall b o k p, Mem.perm m2 b o k p <-> Mem.perm m1 b o k p).

  Lemma exec_store_stack:
    forall (ge: Genv.t Asm.fundef unit) k m1 a rs1 rs l rs2 m2 sz,
      exec_store ge k m1 a rs1 rs l sz = Next rs2 m2 ->
      Mem.stack m2 = Mem.stack m1 /\ (forall b o k p, Mem.perm m2 b o k p <-> Mem.perm m1 b o k p).

  Lemma exec_load_stack:
    forall (ge: Genv.t Asm.fundef unit) k m1 a rs1 rs rs2 m2 sz,
      exec_load ge k m1 a rs1 rs sz = Next rs2 m2 ->
      Mem.stack m2 = Mem.stack m1 /\ (forall b o k p, Mem.perm m2 b o k p <-> Mem.perm m1 b o k p).

  Lemma goto_label_stack:
    forall (ge: Genv.t Asm.fundef unit) f l m1 rs1 rs2 m2,
      goto_label ge f l rs1 m1 = Next rs2 m2 ->
      Mem.stack m2 = Mem.stack m1 /\ (forall b o k p, Mem.perm m2 b o k p <-> Mem.perm m1 b o k p).

  Lemma asmgen_no_change_stack i:
    asm_instr_no_stack i.

  Definition asm_instr_nb_fw i:=
    forall (ge: Genv.t Asm.fundef unit) f rs1 m1 rs2 m2 init_stk,
      Asm.exec_instr init_stk ge f i rs1 m1 = Next rs2 m2 ->
      Ple (Mem.nextblock m1) (Mem.nextblock m2).

  Definition asm_code_nb_fw c :=
    forall i, In i c -> asm_instr_nb_fw i.


    Lemma exec_store_nb:
      forall (ge: Genv.t Asm.fundef unit) k m1 a rs1 rs l rs2 m2 sz,
        exec_store ge k m1 a rs1 rs l sz = Next rs2 m2 ->
        Ple (Mem.nextblock m1) (Mem.nextblock m2).

    Lemma exec_load_nb:
      forall (ge: Genv.t Asm.fundef unit) k m1 a rs1 rs rs2 m2 sz,
        exec_load ge k m1 a rs1 rs sz = Next rs2 m2 ->
        Ple (Mem.nextblock m1) (Mem.nextblock m2).

    Ltac destr_all:=
      repeat match goal with
               H: context[match ?a with _ => _ end] |- _ => repeat destr_in H
             end.

  Lemma asmgen_nextblock_forward i:
    asm_instr_nb_fw i.
  
  Lemma val_inject_set:
    forall j rs1 rs2
      (RINJ: forall r, Val.inject j (rs1 r) (rs2 r))
      v v' (VINJ: Val.inject j v v') r1 r,
      Val.inject j ((rs1 # r1 <- v) r) ((rs2 # r1 <- v') r).

  Lemma val_inject_undef_regs:
    forall l j rs1 rs2
      (RINJ: forall r, Val.inject j (rs1 r) (rs2 r))
      r,
      Val.inject j (undef_regs l rs1 r) (undef_regs l rs2 r).

  Lemma val_inject_nextinstr:
    forall j rs1 rs2 sz
      (RINJ: forall r, Val.inject j (rs1 r) (rs2 r)) r,
      Val.inject j (nextinstr rs1 r sz) (nextinstr rs2 r sz).

  Lemma val_inject_nextinstr_nf:
    forall j rs1 rs2 sz
      (RINJ: forall r, Val.inject j (rs1 r) (rs2 r)) r,
      Val.inject j (nextinstr_nf rs1 r sz) (nextinstr_nf rs2 r sz).

  Lemma exec_load_unchanged_stack:
    forall (ge: Genv.t Asm.fundef unit) chunk m1 a rs1 rd sz rs2 m2 P,
      exec_load ge chunk m1 a rs1 rd sz = Next rs2 m2 ->
      Mem.unchanged_on P m1 m2.

  Lemma public_stack_access_app:
    forall l s b lo hi
      (ND: nodup (l ++ s))
      (PSA: public_stack_access (l ++ s) b lo hi),
      public_stack_access s b lo hi.

  Lemma stack_access_app:
    forall l s b lo hi
      (ND: nodup (l ++ s))
      (PSA: stack_access (l ++ s) b lo hi),
      stack_access s b lo hi.

  Lemma nodup_app:
    forall l1 l2,
      nodup (l1 ++ l2) ->
      forall b, in_stack l1 b -> in_stack l2 b -> False.
  
  Lemma exec_store_unchanged_stack:
    forall (ge: Genv.t Asm.fundef unit) chunk m1 a rs1 rd rds sz rs2 m2 init_stk l,
      Mem.stack m1 = l ++ init_stk ->
      exec_store ge chunk m1 a rs1 rd rds sz = Next rs2 m2 ->
      Mem.unchanged_on (fun (b : block) (o : Z) => ~ stack_access init_stk b o (o + 1)) m1 m2.

  Lemma goto_label_unchanged_stack:
    forall (ge: Genv.t Asm.fundef unit) m1 rs1 f lbl rs2 m2 P,
      goto_label ge f lbl rs1 m1 = Next rs2 m2 ->
      Mem.unchanged_on P m1 m2.
  
  Lemma exec_instr_unchanged_stack:
    forall (ge: Genv.t Asm.fundef unit) f i rs1 m1 rs2 m2 init_stk l,
      Mem.stack m1 = l ++ init_stk ->
      Asm.exec_instr init_stk ge f i rs1 m1 = Next rs2 m2 ->
      Mem.unchanged_on
        (fun b o => ~ stack_access init_stk b o (o+1))
        m1 m2 /\
      (Mem.is_ptr (init_sp init_stk) <> None -> exists l', Mem.stack m2 = l' ++ init_stk).

  Lemma step_unchanged_stack:
    forall (ge: genv) rs1 m1 t rs2 m2 init_stk l,
      Mem.stack m1 = l ++ init_stk ->
      step init_stk ge (State rs1 m1) t (State rs2 m2) ->
      Mem.unchanged_on (fun b o => ~ stack_access init_stk b o (o+1)) m1 m2 /\
      (Mem.is_ptr (init_sp init_stk) <> None -> exists l', Mem.stack m2 = l' ++ init_stk).

  Lemma initial_state_stack_is_app:
    forall (prog: Asm.program) rs m,
      initial_state prog (State rs m) ->
      Mem.stack m = ((None,nil) ::
                                (Some (make_singleton_frame_adt (Genv.genv_next (Genv.globalenv prog)) 0 0 ), nil) :: nil).

End WITHMEMORYMODEL.