Require Import FunInd.
Require Import Coqlib Maps Integers Floats Lattice.
Require Import Compopts AST Linking.
Require Import Values Memory Globalenvs Builtins Events.
Require Import Registers Op RTL.
Require Import ValueDomain ValueAOp Liveness.
Require Import Axioms.
Require Kildall MultiFixpoint.
Require Import OptionMonad.

The dataflow analysis

Definition areg (ae: aenv) (r: reg) : aval := AE.get r ae.
Definition aregs (ae: aenv) (rl: list reg) : list aval := List.map (areg ae) rl.


Fixpoint ae_set_multiple (regs : list reg) (avals : list aval) (ae : aenv): aenv :=
  match regs, avals with
  | (r::regs0), (av::avals0) =>
      ae_set_multiple regs0 avals0 (AE.set r av ae)
  | nil, _ | _, nil => ae
  end.

Lemma ematch_restrict:
  forall bc e ae (av : aval) r
         (VMATCH : vmatch bc (e # r) av)
         (EMATCH : ematch bc e ae),
    ematch bc e (AE.set r av ae).

Lemma ematch_restrict_multiple bc:
  forall regs avals e ae
  (ARG_MATCH : list_forall2 (vmatch bc) (e ## regs) avals)
  (EMATCH : ematch bc e ae),
  ematch bc e (ae_set_multiple regs avals ae).


Definition mafter_public_call : amem := mtop.

Definition mafter_private_call (am_before: amem) : amem :=
  {| am_stack := am_before.(am_stack);
     am_glob := PTree.empty _;
     am_nonstack := Nonstack;
     am_top := plub (ab_summary (am_stack am_before)) Nonstack |}.

Definition analyze_call (am: amem) (aargs: list aval) :=
  if pincl am.(am_nonstack) Nonstack
  && forallb (fun av => vpincl av Nonstack) aargs
  then (Ifptr Nonstack, mafter_private_call am)
  else (Vtop, mafter_public_call).

Definition filter_condition (cond: condition) (regs: list reg) (ae : aenv) : aenv :=
  ae_set_multiple regs (filter_static_condition cond (aregs ae regs)) ae.

Definition transfer_condition (cond : condition) (args : list reg) ae am : VA.t * VA.t :=
  match eval_static_condition cond (aregs ae args) with
  | Bnone =>
      if Compopts.va_strict tt
      then (VA.Bot, VA.Bot)
      else (VA.State ae am, VA.State ae am)
  | Just true =>
      (VA.State ae am, VA.Bot)
  | Maybe true =>
      if Compopts.va_strict tt
      then (VA.State ae am, VA.Bot)
      else (VA.State ae am, VA.State ae am)
  | Just false =>
      (VA.Bot, VA.State ae am)
  | Maybe false =>
      if Compopts.va_strict tt
      then (VA.Bot, VA.State ae am)
      else (VA.State ae am, VA.State ae am)
  | Btop =>
      (VA.State (filter_condition cond args ae) am,
        VA.State (filter_condition (negate_condition cond) args ae) am)
  end.

Definition transfer_call (ae: aenv) (am: amem) (args: list reg) (res: reg) :=
  let (av, am') := analyze_call am (aregs ae args) in
  VA.State (AE.set res av ae) am'.


Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) : aval :=
  match ba with
  | BA r => areg ae r
  | BA_int n => I n
  | BA_long n => L n
  | BA_float n => F n
  | BA_single n => FS n
  | BA_loadstack chunk ofs => loadv chunk rm am (Ptr (Stk ofs))
  | BA_addrstack ofs => Ptr (Stk ofs)
  | BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs))
  | BA_addrglobal id ofs => Ptr (Gl id ofs)
  | BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
  | BA_addptr ba1 ba2 =>
      let v1 := abuiltin_arg ae am rm ba1 in
      let v2 := abuiltin_arg ae am rm ba2 in
      if Archi.ptr64 then addl v1 v2 else add v1 v2
  end.

Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv :=
  match br with
  | BR r => AE.set r av ae
  | _ => ae
  end.

Definition transfer_builtin_default
              (ae: aenv) (am: amem) (rm: romem)
              (args: list (builtin_arg reg)) (res: builtin_res reg) :=
  let (av, am') := analyze_call am (map (abuiltin_arg ae am rm) args) in
  VA.State (set_builtin_res res av ae) am'.

Definition eval_static_builtin_function
              (ae: aenv) (am: amem) (rm: romem)
              (bf: builtin_function) (args: list (builtin_arg reg)) :=
  match builtin_function_sem bf
                 (map val_of_aval (map (abuiltin_arg ae am rm) args)) with
  | Some v => aval_of_val v
  | None => None
  end.

Definition transfer_builtin
              (ae: aenv) (am: amem) (rm: romem) (ef: external_function)
              (args: list (builtin_arg reg)) (res: builtin_res reg) :=
  match ef, args with
  | EF_vload chunk, addr :: nil =>
      let aaddr := abuiltin_arg ae am rm addr in
      let a :=
        if va_strict tt
        then vlub (loadv chunk rm am aaddr) (vnormalize chunk (Ifptr Glob))
        else vnormalize chunk Vtop in
      VA.State (set_builtin_res res a ae) am
  | EF_vstore chunk, addr :: v :: nil =>
      let aaddr := abuiltin_arg ae am rm addr in
      let av := abuiltin_arg ae am rm v in
      let am' := storev chunk am aaddr av in
      VA.State (set_builtin_res res ntop ae) (mlub am am')
  | EF_memcpy sz al, dst :: src :: nil =>
      let adst := abuiltin_arg ae am rm dst in
      let asrc := abuiltin_arg ae am rm src in
      let p := loadbytes am rm (aptr_of_aval asrc) in
      let am' := storebytes am (aptr_of_aval adst) sz p in
      VA.State (set_builtin_res res ntop ae) am'
  | (EF_annot _ _ _ | EF_debug _ _ _ | EF_profiling _ _), _ =>
      VA.State (set_builtin_res res ntop ae) am
  | EF_annot_val _ _ _, v :: nil =>
      let av := abuiltin_arg ae am rm v in
      VA.State (set_builtin_res res av ae) am
  | EF_observe _, _ =>
      VA.State (set_builtin_res res Vtop ae) am
  | EF_builtin name sg, _ =>
      match lookup_builtin_function name sg with
      | Some bf =>
          let av := match eval_static_builtin_function ae am rm bf args with
                    | Some av => av | None => Vtop end
          in VA.State (set_builtin_res res av ae) am
      | None => transfer_builtin_default ae am rm args res
      end
  | _, _ =>
      transfer_builtin_default ae am rm args res
  end.


Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : list (node * VA.t) :=
  match f.(fn_code)!pc with
  | None => nil
  | Some(Inop s) => (s, (VA.State ae am)) :: nil
  | Some(Iop op args res s) =>
      let a := eval_static_operation op (aregs ae args) in
      (s, VA.State (AE.set res a ae) am) :: nil
  | Some(Iload TRAP chunk addr args dst s) =>
      let a := loadv chunk rm am
                     (eval_static_addressing addr (aregs ae args)) in
      (s, (VA.State (AE.set dst a ae) am)) :: nil

               
  | Some(Iload NOTRAP chunk addr args dst s) =>
      (s, (VA.State (AE.set dst Vtop ae) am)) :: nil
  | Some(Istore chunk addr args src s) =>
      let am' := storev chunk am (eval_static_addressing addr (aregs ae args)) (areg ae src) in
      (s, (VA.State ae am')) :: nil
  | Some(Icall sig ros args res s) =>
      (s, (transfer_call ae am args res)) :: nil
  | Some(Itailcall sig ros args) => nil
  | Some(Ibuiltin ef args res s) =>
      (s, (transfer_builtin ae am rm ef args res)) :: nil
  | Some(Icond cond args s1 s2 _) =>
      match transfer_condition cond args ae am with
      | (va1, va2) => (s1, va1) :: (s2, va2) :: nil
      end
  | Some(Ijumptable arg tbl) =>
      mapi (fun i s => (s, (VA.State (AE.set arg (I (Int.repr i)) ae) am))) tbl
  | Some(Ireturn arg) => nil
  | Some(Iassert cond args s1) =>
      (s1, VA.State ae am) :: nil
  end.

Definition relax_ae kills ae :=
  match kills with
  | None => ae
  | Some regs => eforget regs ae
  end.

Lemma relax_ae_ge :
  forall kills ae am va
         (GE : VA.ge va (VA.State (relax_ae kills ae) am)),
    VA.ge va (VA.State ae am).

Definition relax_next kills (va : node * VA.t) :=
  ((fst va),
           match snd va with
           | VA.Bot => VA.Bot
           | VA.State ae' am' =>
               VA.State (relax_ae kills ae') am'
           end).

Local Open Scope option_monad_scope.

Definition transfer' (f: function) (lastuses: option (PTree.t (list reg))) (rm: romem)
                     (pc: node) (before: VA.t) : list (node * VA.t) :=
  match before with
  | VA.Bot => nil
  | VA.State ae am =>
      List.map (relax_next (SOME lu <- lastuses IN lu!pc)) (transfer f rm pc ae am)
  end.


Module VAW <: SEMILATTICE_WITH_WIDENING.
  Include ValueDomain.VA.
  Definition widen := lub.
  Definition ge_widen_left := ge_lub_left.
  Definition ge_widen_right := ge_lub_right.
End VAW.

Module MDS := MultiFixpoint.Solver(Kildall.NodeSetForward)(VAW).

Definition mfunction_entry :=
  {| am_stack := ablock_init Pbot;
     am_glob := PTree.empty _;
     am_nonstack := Nonstack;
     am_top := Nonstack |}.


Definition analyze (relax:bool) (rm: romem) (f: function): PMap.t VA.t :=
  let lu := ASSERT relax IN Some (last_uses f) in
  let entry := (f.(fn_entrypoint),
                 VA.State (einit_regs f.(fn_params) f.(fn_sig).(sig_args)) mfunction_entry) :: nil in
  match MDS.solution_opt (fun (_ : node) => true) (transfer' f lu rm) entry
                    with
  | None => PMap.init (VA.State AE.top mtop)
  | Some res => res
  end.


Definition store_init_data (ab: ablock) (p: Z) (id: init_data) : ablock :=
  match id with
  | Init_int8 n => ablock_store Mint8unsigned ab p (I n)
  | Init_int16 n => ablock_store Mint16unsigned ab p (I n)
  | Init_int32 n => ablock_store Mint32 ab p (I n)
  | Init_int64 n => ablock_store Mint64 ab p (L n)
  | Init_float32 n => ablock_store Mfloat32 ab p
                        (if propagate_float_constants tt then FS n else ntop)
  | Init_float64 n => ablock_store Mfloat64 ab p
                        (if propagate_float_constants tt then F n else ntop)
  | Init_addrof symb ofs => ablock_store Mptr ab p (Ptr (Gl symb ofs))
  | Init_space n => ab
  end.

Fixpoint store_init_data_list (ab: ablock) (p: Z) (idl: list init_data)
                              {struct idl}: ablock :=
  match idl with
  | nil => ab
  | id :: idl' => store_init_data_list (store_init_data ab p id) (p + init_data_size id) idl'
  end.


Definition definitive_initializer (init: list init_data) : bool :=
  match init with
  | nil => false
  | Init_space _ :: nil => false
  | _ => true
  end.

Definition alloc_global {fdef: Type} (rm: romem) (idg: qualident * globdef fdef unit): romem :=
  match idg with
  | (id, Gfun f) =>
      QITree.remove id rm
  | (id, Gvar v) =>
      if v.(gvar_readonly) && negb v.(gvar_volatile)
      then
         let oab := if definitive_initializer v.(gvar_init)
                   then Some (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init))
                   else None in
         QITree.set id oab rm
      else QITree.remove id rm
  end.

Definition romem_for {genF : Type} (p: AST.program genF unit) : romem :=
  List.fold_left alloc_global p.(prog_defs) (PTree.empty _).

Soundness proof

Lemma analyze_entrypoint:
  forall relax rm f vl m bc,
  (forall v, In v vl -> vmatch bc v (Ifptr Nonstack)) ->
  Val.has_argtype_list vl f.(fn_sig).(sig_args) ->
  mmatch bc m mfunction_entry ->
  exists ae am,
     (analyze relax rm f)!!(fn_entrypoint f) = VA.State ae am
  /\ ematch bc (init_regs vl (fn_params f)) ae
  /\ mmatch bc m am.

Lemma analyze_successor:
  forall relax f n ae am s rm ae' am'
  (CURRENT : (analyze relax rm f)!!n = VA.State ae am),
  In (s, VA.State ae' am') (transfer f rm n ae am) ->
  VA.ge (analyze relax rm f)!!s (VA.State ae' am').

Lemma analyze_succ:
  forall relax e m rm f n ae am s ae' am' bc
  (ANALYZE : (analyze relax rm f)!!n = VA.State ae am)
  (HIN : In (s, (VA.State ae' am')) (transfer f rm n ae am)),
  ematch bc e ae' ->
  mmatch bc m am' ->
  exists ae'' am'',
     (analyze relax rm f)!!s = VA.State ae'' am''
  /\ ematch bc e ae''
  /\ mmatch bc m am''.

Analysis of registers and builtin arguments

Lemma areg_sound:
  forall bc e ae r, ematch bc e ae -> vmatch bc (e#r) (areg ae r).

Lemma aregs_sound:
  forall bc e ae rl, ematch bc e ae -> list_forall2 (vmatch bc) (e##rl) (aregs ae rl).

Global Hint Resolve areg_sound aregs_sound: va.

Lemma abuiltin_arg_sound:
  forall {F V : Type} (ge : Genv.t F V) bc rs sp m ae rm am,
  ematch bc rs ae ->
  romatch bc m rm ->
  mmatch bc m am ->
  genv_match bc ge ->
  bc sp = BCstack ->
  forall a v,
  eval_builtin_arg ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m a v ->
  vmatch bc v (abuiltin_arg ae am rm a).

Lemma abuiltin_args_sound:
  forall {F V : Type} (ge : Genv.t F V) bc rs sp m ae rm am,
  ematch bc rs ae ->
  romatch bc m rm ->
  mmatch bc m am ->
  genv_match bc ge ->
  bc sp = BCstack ->
  forall al vl,
  eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl ->
  list_forall2 (vmatch bc) vl (map (abuiltin_arg ae am rm) al).

Lemma set_builtin_res_sound:
  forall bc rs ae v av res,
  ematch bc rs ae ->
  vmatch bc v av ->
  ematch bc (regmap_setres res v rs) (set_builtin_res res av ae).

Lemma eval_static_builtin_function_sound:
  forall {F V : Type} (ge : Genv.t F V)
         bc rs sp m ae rm am (bf: builtin_function) al vl v va,
  ematch bc rs ae ->
  romatch bc m rm ->
  mmatch bc m am ->
  genv_match bc ge ->
  bc sp = BCstack ->
  eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl ->
  eval_static_builtin_function ae am rm bf al = Some va ->
  builtin_function_sem bf vl = Some v ->
  vmatch bc v va.

Constructing block classifications

Definition bc_nostack (bc: block_classification) : Prop :=
  forall b, bc b <> BCstack.

Section NOSTACK.

Variable bc: block_classification.
Hypothesis NOSTACK: bc_nostack bc.

Lemma pmatch_no_stack: forall b ofs p, pmatch bc b ofs p -> pmatch bc b ofs Nonstack.

Lemma vmatch_no_stack: forall v x, vmatch bc v x -> vmatch bc v (Ifptr Nonstack).

Lemma smatch_no_stack: forall m b p, smatch bc m b p -> smatch bc m b Nonstack.

Lemma mmatch_no_stack: forall m am astk,
  mmatch bc m am -> mmatch bc m {| am_stack := astk; am_glob := PTree.empty _; am_nonstack := Nonstack; am_top := Nonstack |}.

End NOSTACK.

Construction 1: allocating the stack frame at function entry

Ltac splitall := repeat (match goal with |- _ /\ _ => split end).

Theorem allocate_stack:
  forall {F V : Type} (ge : Genv.t F V) m sz m' sp bc rm am,
  Mem.alloc m 0 sz = (m', sp) ->
  genv_match bc ge ->
  romatch bc m rm ->
  mmatch bc m am ->
  bc_nostack bc ->
  exists bc',
     bc_incr bc bc'
  /\ bc' sp = BCstack
  /\ genv_match bc' ge
  /\ romatch bc' m' rm
  /\ mmatch bc' m' mfunction_entry
  /\ (forall b, Plt b sp -> bc' b = bc b)
  /\ (forall v x, vmatch bc v x -> vmatch bc' v (Ifptr Nonstack)).


Theorem anonymize_stack:
  forall {F V : Type} (ge : Genv.t F V) m sp bc rm am,
  genv_match bc ge ->
  romatch bc m rm ->
  mmatch bc m am ->
  bc sp = BCstack ->
  exists bc',
     bc_nostack bc'
  /\ bc' sp = BCother
  /\ (forall b, b <> sp -> bc' b = bc b)
  /\ (forall v x, vmatch bc v x -> vmatch bc' v Vtop)
  /\ genv_match bc' ge
  /\ romatch bc' m rm
  /\ mmatch bc' m mtop.


Theorem hide_stack:
  forall {F V : Type} (ge : Genv.t F V) m sp bc rm am,
  genv_match bc ge ->
  romatch bc m rm ->
  mmatch bc m am ->
  bc sp = BCstack ->
  pge Nonstack am.(am_nonstack) ->
  exists bc',
     bc_nostack bc'
  /\ bc' sp = BCinvalid
  /\ (forall b, b <> sp -> bc' b = bc b)
  /\ (forall v x, vge (Ifptr Nonstack) x -> vmatch bc v x -> vmatch bc' v Vtop)
  /\ genv_match bc' ge
  /\ romatch bc' m rm
  /\ mmatch bc' m mtop.


Theorem return_from_public_call:
  forall {F V : Type} (ge : Genv.t F V)
         (caller callee: block_classification) bound sp e ae v m rm,
  bc_below caller bound ->
  callee sp = BCother ->
  caller sp = BCstack ->
  (forall b, Plt b bound -> b <> sp -> caller b = callee b) ->
  genv_match caller ge ->
  ematch caller e ae ->
  Ple bound (Mem.nextblock m) ->
  vmatch callee v Vtop ->
  romatch callee m rm ->
  mmatch callee m mtop ->
  genv_match callee ge ->
  bc_nostack callee ->
  exists bc,
      vmatch bc v Vtop
   /\ ematch bc e ae
   /\ romatch bc m rm
   /\ mmatch bc m mafter_public_call
   /\ genv_match bc ge
   /\ bc sp = BCstack
   /\ (forall b, Plt b sp -> bc b = caller b)
   /\ (forall b, Plt b bound -> bc b = caller b).


Theorem return_from_private_call:
  forall {F V : Type} (ge : Genv.t F V) (caller callee: block_classification) bound sp e ae v m rm am,
  bc_below caller bound ->
  callee sp = BCinvalid ->
  caller sp = BCstack ->
  (forall b, Plt b bound -> b <> sp -> caller b = callee b) ->
  genv_match caller ge ->
  ematch caller e ae ->
  bmatch caller m sp am.(am_stack) ->
  Ple bound (Mem.nextblock m) ->
  vmatch callee v Vtop ->
  romatch callee m rm ->
  mmatch callee m mtop ->
  genv_match callee ge ->
  bc_nostack callee ->
  exists bc,
      vmatch bc v (Ifptr Nonstack)
   /\ ematch bc e ae
   /\ romatch bc m rm
   /\ mmatch bc m (mafter_private_call am)
   /\ genv_match bc ge
   /\ bc sp = BCstack
   /\ (forall b, Plt b sp -> bc b = caller b)
   /\ (forall b, Plt b bound -> bc b = caller b).


Theorem external_call_match:
  forall {F V : Type} (ge : Genv.t F V) ef vargs m t vres m' bc rm am,
  external_call ef ge vargs m t vres m' ->
  genv_match bc ge ->
  (forall v, In v vargs -> vmatch bc v Vtop) ->
  romatch bc m rm ->
  mmatch bc m am ->
  bc_nostack bc ->
  exists bc',
     bc_incr bc bc'
  /\ (forall b, Plt b (Mem.nextblock m) -> bc' b = bc b)
  /\ vmatch bc' vres Vtop
  /\ genv_match bc' ge
  /\ romatch bc' m' rm
  /\ mmatch bc' m' mtop
  /\ bc_nostack bc'
  /\ (forall b ofs n, Mem.valid_block m b -> bc b = BCinvalid -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n).

Semantic invariant

Section BUILTINS.

Inductive stack_preserving (bc : block_classification) m bound
                           (bc' : block_classification) m' bound' : Prop :=
  stack_preserving_intro
    (P_BC: forall b, Plt b bound -> bc' b = bc b)
    (P_LOAD: forall b ofs n bytes,
               Plt b bound -> bc b = BCinvalid -> n >= 0 ->
               Mem.loadbytes m' b ofs n = Some bytes ->
               Mem.loadbytes m b ofs n = Some bytes)
    (P_BOUND: Ple bound bound')
    .

Lemma stack_preserving_refl bc m bound:
  stack_preserving bc m bound bc m bound.

Lemma storev_stack_preserving chunk m addr v m' bc aaddr bound
  (STORE: Mem.storev chunk m addr v = Some m')
  (MATCH: vmatch bc addr aaddr):
  stack_preserving bc m bound bc m' bound.

Lemma storebytes_stack_preserving m b ofs bytes m' bc aaddr bound
  (STORE: Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m')
  (MATCH: vmatch bc (Vptr b ofs) aaddr):
  stack_preserving bc m bound bc m' bound.

Definition is_tr_default (ef: external_function) (args: list (builtin_arg reg)) :=
  match ef, args with
  | EF_vload _, _ :: nil
  | EF_vstore _, _ :: _ :: nil
  | EF_memcpy _ _, _ :: _ :: nil
  | EF_annot_val _ _ _, _ :: nil => false
  | (EF_annot _ _ _ | EF_debug _ _ _ | EF_profiling _ _ | EF_observe _), _ => false
  | EF_builtin name sg, _ =>
      match lookup_builtin_function name sg with
      | Some bf => false
      | None => true
      end
  | _, _ => true
  end.

Definition bc_unchanged_builtin (ef: external_function): bool :=
  match ef with
  | EF_vload _ | EF_vstore _ | EF_memcpy _ _ | EF_annot_val _ _ _ | EF_observe _ => true
  | _ => negb (is_tr_default ef nil)
  end.

Lemma sound_exec_builtin_aux
  (genF genV : Type) (ge : Genv.t genF genV)
  (rm : romem) sp bc e ae m am ef args vargs res vres m' t
  (EM: ematch bc e ae)
  (RO: romatch bc m rm)
  (MM: mmatch bc m am)
  (GE: genv_match bc ge)
  (SP: bc sp = BCstack)
  (EVAL : eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m args vargs)
  (CALL : external_call ef ge vargs m t vres m'):
  let e' := regmap_setres res vres e in
  exists bc' ae' am',
    transfer_builtin ae am rm ef args res = VA.State ae' am' /\
    ematch bc' e' ae' /\
    romatch bc' m' rm /\
    mmatch bc' m' am' /\
    genv_match bc' ge /\
    bc' sp = BCstack /\
    stack_preserving bc m sp bc' m' sp /\
    (bc_unchanged_builtin ef = true -> bc'=bc) /\
    (forall b, Plt b (Mem.nextblock m) -> bc' b = bc b).

Lemma sound_exec_builtin
  (genF genV : Type) (ge : Genv.t genF genV)
  (rm : romem) sp bc e ae m am ef args vargs res vres m' t
  (EM: ematch bc e ae)
  (RO: romatch bc m rm)
  (MM: mmatch bc m am)
  (GE: genv_match bc ge)
  (SP: bc sp = BCstack)
  (EVAL : eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m args vargs)
  (CALL : external_call ef ge vargs m t vres m'):
  let e' := regmap_setres res vres e in
  exists bc' ae' am',
    transfer_builtin ae am rm ef args res = VA.State ae' am' /\
    ematch bc' e' ae' /\
    romatch bc' m' rm /\
    mmatch bc' m' am' /\
    genv_match bc' ge /\
    bc' sp = BCstack /\
    stack_preserving bc m sp bc' m' sp.

End BUILTINS.

Section SOUNDNESS.

Variable relax: bool.
Variable prog: program.
Variable ge: genv.

Let rm := romem_for prog.

Inductive sound_stack: block_classification -> list stackframe -> mem -> block -> Prop :=
  | sound_stack_nil: forall bc m bound,
      sound_stack bc nil m bound
  | sound_stack_public_call:
      forall (bc: block_classification) res f sp pc e stk m bound bc' bound' ae
        (STK: sound_stack bc' stk m sp)
        (INCR: Ple bound' bound)
        (BELOW: bc_below bc' bound')
        (SP: bc sp = BCother)
        (SP': bc' sp = BCstack)
        (SAME: forall b, Plt b bound' -> b <> sp -> bc b = bc' b)
        (GE: genv_match bc' ge)
        (AN: VA.ge (analyze relax rm f)!!pc (VA.State (AE.set res Vtop ae) mafter_public_call))
        (EM: ematch bc' e ae),
      sound_stack bc (Stackframe res f (Vptr sp Ptrofs.zero) pc e :: stk) m bound
  | sound_stack_private_call:
     forall (bc: block_classification) res f sp pc e stk m bound bc' bound' ae am
        (STK: sound_stack bc' stk m sp)
        (INCR: Ple bound' bound)
        (BELOW: bc_below bc' bound')
        (SP: bc sp = BCinvalid)
        (SP': bc' sp = BCstack)
        (SAME: forall b, Plt b bound' -> b <> sp -> bc b = bc' b)
        (GE: genv_match bc' ge)
        (AN: VA.ge (analyze relax rm f)!!pc (VA.State (AE.set res (Ifptr Nonstack) ae) (mafter_private_call am)))
        (EM: ematch bc' e ae)
        (CONTENTS: bmatch bc' m sp am.(am_stack)),
      sound_stack bc (Stackframe res f (Vptr sp Ptrofs.zero) pc e :: stk) m bound.

Inductive sound_state_base (bc: block_classification): state -> Prop :=
  | sound_regular_state:
      forall s f sp pc e m ae am
        (STK: sound_stack bc s m sp)
        (AN: (analyze relax rm f)!!pc = VA.State ae am)
        (EM: ematch bc e ae)
        (RO: romatch bc m rm)
        (MM: mmatch bc m am)
        (GE: genv_match bc ge)
        (SP: bc sp = BCstack),
      sound_state_base bc (State s f (Vptr sp Ptrofs.zero) pc e m)
  | sound_call_state:
      forall s fd args m
        (STK: sound_stack bc s m (Mem.nextblock m))
        (ARGS: forall v, In v args -> vmatch bc v Vtop)
        (RO: romatch bc m rm)
        (MM: mmatch bc m mtop)
        (GE: genv_match bc ge)
        (NOSTK: bc_nostack bc),
      sound_state_base bc (Callstate s fd args m)
  | sound_return_state:
      forall s v m
        (STK: sound_stack bc s m (Mem.nextblock m))
        (RES: vmatch bc v Vtop)
        (RO: romatch bc m rm)
        (MM: mmatch bc m mtop)
        (GE: genv_match bc ge)
        (NOSTK: bc_nostack bc),
      sound_state_base bc (Returnstate s v m).


Lemma sound_stack_ext:
  forall m' bc stk m bound,
  sound_stack bc stk m bound ->
  (forall b ofs n bytes,
       Plt b bound -> bc b = BCinvalid -> n >= 0 ->
       Mem.loadbytes m' b ofs n = Some bytes ->
       Mem.loadbytes m b ofs n = Some bytes) ->
  sound_stack bc stk m' bound.

Lemma sound_stack_new_bound:
  forall bc stk m bound bound',
  sound_stack bc stk m bound ->
  Ple bound bound' ->
  sound_stack bc stk m bound'.

Lemma sound_stack_exten:
  forall bc stk m bound (bc1: block_classification),
  sound_stack bc stk m bound ->
  (forall b, Plt b bound -> bc1 b = bc b) ->
  sound_stack bc1 stk m bound.

Lemma sound_stack_preserved stk bc m bound bc' m' bound':
  sound_stack bc stk m bound ->
  stack_preserving bc m bound bc' m' bound' ->
  sound_stack bc' stk m' bound'.

Lemma sound_stack_inv:
  forall m' bc stk m bound,
  sound_stack bc stk m bound ->
  (forall b ofs n, Plt b bound -> bc b = BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
  sound_stack bc stk m' bound.

Lemma sound_stack_storev:
  forall chunk m addr v m' bc aaddr stk bound,
  Mem.storev chunk m addr v = Some m' ->
  vmatch bc addr aaddr ->
  sound_stack bc stk m bound ->
  sound_stack bc stk m' bound.

Lemma sound_stack_free:
  forall m b lo hi m' bc stk bound,
  Mem.free m b lo hi = Some m' ->
  sound_stack bc stk m bound ->
  sound_stack bc stk m' bound.

Preservation of the semantic invariant by one step of execution

Lemma sound_succ_state:
  forall bc pc ae am instr ae' am' s f sp pc' e' m'
  (ANALYZE : (analyze relax rm f)!!pc = VA.State ae am)
  (INSTR : f.(fn_code)!pc = Some instr)
  (TRANSFER : In (pc', (VA.State ae' am')) (transfer f rm pc ae am))
  (EM : ematch bc e' ae')
  (MM : mmatch bc m' am')
  (RO : romatch bc m' rm)
  (GENV : genv_match bc ge)
  (BC : bc sp = BCstack)
  (STACK : sound_stack bc s m' sp),
  sound_state_base bc (State s f (Vptr sp Ptrofs.zero) pc' e' m').

Lemma filter_condition_sound bc rs cond args ae m
    (EMATCH : ematch bc rs ae)
    (COND : eval_condition cond (rs ## args) m = Some true):
  ematch bc rs (filter_condition cond args ae).

Lemma transfer_condition_sound_true:
  forall bc (cond : condition) (args : list reg) rs ae m am
         (EVAL : eval_condition cond (rs ## args) m = Some true)
         (EMATCH : ematch bc rs ae)
         (MMATCH : mmatch bc m am),
  exists ae', (fst (transfer_condition cond args ae am)) =
                (VA.State ae' am) /\
                (ematch bc rs ae').

Lemma transfer_condition_sound_false:
  forall bc (cond : condition) (args : list reg) rs ae m am
         (EVAL : eval_condition cond (rs ## args) m = Some false)
         (EMATCH : ematch bc rs ae)
         (MMATCH : mmatch bc m am),
  exists ae', (snd (transfer_condition cond args ae am)) =
                (VA.State ae' am) /\
                (ematch bc rs ae').

Definition bc_unchanged (st: state): bool :=
  match st with
  | State _ f _ pc _ _ =>
     match (fn_code f)!pc with
     | Some (Icall _ _ _ _ _) | Some (Itailcall _ _ _) | Some (Ireturn _) => false
     | Some (Ibuiltin ef _ _ _) => bc_unchanged_builtin ef
     | _ => true
     end
  | _ => false
  end.

Theorem sound_step_base:
  forall bc st t st', RTL.step ge st t st' -> sound_state_base bc st ->
     exists bc', sound_state_base bc' st' /\ (bc_unchanged st = true -> bc'=bc).

End SOUNDNESS.

Extension to separate compilation

Section LINKING.

Variable relax: bool.
Variable prog: program.
Let ge := Genv.globalenv prog.

Inductive sound_state: state -> Prop :=
  | sound_state_intro: forall st,
      (forall cunit, linkorder cunit prog -> exists bc, sound_state_base relax cunit ge bc st) ->
      sound_state st.

Theorem sound_step:
  forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'.

Remark sound_state_inv:
  forall st cunit,
  sound_state st -> linkorder cunit prog -> exists bc, sound_state_base relax cunit ge bc st.

End LINKING.

Soundness of the initial memory abstraction

Section INITIAL.
Variable genF : Type.
Variable prog: AST.program genF unit.
Local Definition genv := Genv.t genF unit.

Let ge := Genv.globalenv prog.

Lemma initial_block_classification:
  forall m,
  Genv.init_mem prog = Some m ->
  exists bc,
     genv_match bc ge
  /\ bc_below bc (Mem.nextblock m)
  /\ bc_nostack bc
  /\ (forall b id, bc b = BCglob id -> Genv.find_symbol ge id = Some b)
  /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid).

Section INIT.

Variable bc: block_classification.
Hypothesis GMATCH: genv_match bc ge.

Lemma store_init_data_summary:
  forall ab p id,
  pge Glob (ab_summary ab) ->
  pge Glob (ab_summary (store_init_data ab p id)).

Lemma store_init_data_list_summary:
  forall idl ab p,
  pge Glob (ab_summary ab) ->
  pge Glob (ab_summary (store_init_data_list ab p idl)).

Lemma store_init_data_sound:
  forall m b p id m' ab,
  Genv.store_init_data ge m b p id = Some m' ->
  bmatch bc m b ab ->
  bmatch bc m' b (store_init_data ab p id).

Lemma store_init_data_list_sound:
  forall idl m b p m' ab,
  Genv.store_init_data_list ge m b p idl = Some m' ->
  bmatch bc m b ab ->
  bmatch bc m' b (store_init_data_list ab p idl).

Lemma store_init_data_other:
  forall m b p id m' ab b',
  Genv.store_init_data ge m b p id = Some m' ->
  b' <> b ->
  bmatch bc m b' ab ->
  bmatch bc m' b' ab.

Lemma store_init_data_list_other:
  forall b b' ab idl m p m',
  Genv.store_init_data_list ge m b p idl = Some m' ->
  b' <> b ->
  bmatch bc m b' ab ->
  bmatch bc m' b' ab.

Lemma store_zeros_same:
  forall p m b pos n m',
  store_zeros m b pos n = Some m' ->
  smatch bc m b p ->
  smatch bc m' b p.

Lemma store_zeros_other:
  forall b' ab m b p n m',
  store_zeros m b p n = Some m' ->
  b' <> b ->
  bmatch bc m b' ab ->
  bmatch bc m' b' ab.

Definition initial_mem_match (bc: block_classification) (m: mem) (g : genv) :=
  forall id b v,
  Genv.find_symbol g id = Some b -> Genv.find_var_info g b = Some v ->
  v.(gvar_volatile) = false -> v.(gvar_readonly) = true ->
  bmatch bc m b (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)).

Lemma alloc_global_match:
  forall m g idg m',
  Genv.genv_next g = Mem.nextblock m ->
  initial_mem_match bc m g ->
  Genv.alloc_global ge m idg = Some m' ->
  initial_mem_match bc m' (Genv.add_global g idg).

Lemma alloc_globals_match:
  forall gl m g m',
  Genv.genv_next g = Mem.nextblock m ->
  initial_mem_match bc m g ->
  Genv.alloc_globals ge m gl = Some m' ->
  initial_mem_match bc m' (Genv.add_globals g gl).

Definition romem_consistent (defmap: QITree.t (globdef genF unit)) (rm: romem) :=
  forall id ab,
  rm!.id = Some ab ->
  exists v,
     defmap!.id = Some (Gvar v)
  /\ v.(gvar_readonly) = true
  /\ v.(gvar_volatile) = false
  /\ (ab <> None -> (definitive_initializer v.(gvar_init) = true /\ ab = Some (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)))).

Lemma alloc_global_consistent:
  forall dm rm idg,
  romem_consistent dm rm ->
  romem_consistent (QITree.set (fst idg) (snd idg) dm) (alloc_global rm idg).

Lemma romem_for_consistent:
  forall cunit, romem_consistent (prog_defmap cunit) (romem_for cunit).

End INIT.
End INITIAL.

Arguments romem_consistent {genF}.
Arguments romem_for_consistent {genF}.
Arguments initial_mem_match {genF}.
Arguments alloc_globals_match {genF}.

Section INITIAL2.
Variable prog: program.

Let ge := Genv.globalenv prog.

Lemma romem_for_consistent_2:
  forall (cunit : program), linkorder cunit prog -> romem_consistent (prog_defmap prog) (romem_for cunit).

Lemma genv_find_empty : forall genF genV x b,
  Genv.find_var_info (Genv.empty_genv genF genV x) b = None.

Theorem initial_mem_matches:
  forall m
  (INIT : Genv.init_mem prog = Some m),
  exists bc,
     genv_match bc ge
  /\ bc_below bc (Mem.nextblock m)
  /\ bc_nostack bc
  /\ (forall cunit, linkorder cunit prog -> romatch bc m (romem_for cunit))
  /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid).

Theorem sound_initial:
  forall relax st, initial_state prog st -> sound_state relax prog st.
End INITIAL2.

Global Hint Resolve areg_sound aregs_sound: va.

Interface with other optimizations

Ltac InvSoundState :=
  match goal with
  | H1: sound_state ?relax ?prog ?st, H2: linkorder ?cunit ?prog |- _ =>
      let bc := fresh "bc" in let S := fresh "S" in generalize (sound_state_inv _ _ _ _ H1 H2); intros (bc & S); inv S
  end.

Definition avalue (a: VA.t) (r: reg) : aval :=
  match a with
  | VA.Bot => Vbot
  | VA.State ae am => AE.get r ae
  end.

Lemma avalue_sound:
  forall relax cunit prog s f sp pc e m r,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  exists bc,
     vmatch bc e#r (avalue (analyze relax (romem_for cunit) f)!!pc r)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.

Definition aaddr (a: VA.t) (r: reg) : aptr :=
  match a with
  | VA.Bot => Pbot
  | VA.State ae am => aptr_of_aval (AE.get r ae)
  end.

Lemma aaddr_sound:
  forall relax cunit prog s f sp pc e m r b ofs,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  e#r = Vptr b ofs ->
  exists bc,
     pmatch bc b ofs (aaddr (analyze relax (romem_for cunit) f)!!pc r)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.

Definition vaddressing (a: VA.t) (addr: addressing) (args: list reg) : aval :=
  match a with
  | VA.Bot => Vbot
  | VA.State ae am => eval_static_addressing addr (aregs ae args)
  end.

Lemma vaddressing_sound:
  forall relax cunit prog s f sp pc e m addr args v,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  eval_addressing (Genv.globalenv prog) (Vptr sp Ptrofs.zero) addr e##args = Some v ->
  exists bc,
     vmatch bc v (vaddressing (analyze relax (romem_for cunit) f)!!pc addr args)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.


Definition aaddressing (a: VA.t) (addr: addressing) (args: list reg) : aptr :=
  aptr_of_aval (vaddressing a addr args).

Lemma aaddressing_sound:
  forall relax cunit prog s f sp pc e m addr args b ofs,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  eval_addressing (Genv.globalenv prog) (Vptr sp Ptrofs.zero) addr e##args = Some (Vptr b ofs) ->
  exists bc,
     pmatch bc b ofs (aaddressing (analyze relax (romem_for cunit) f)!!pc addr args)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.


Definition aaddr_arg (a: VA.t) (ba: builtin_arg reg) : aptr :=
  match a with
  | VA.Bot => Pbot
  | VA.State ae am =>
      match ba with
      | BA r => aptr_of_aval (AE.get r ae)
      | BA_addrstack ofs => Stk ofs
      | BA_addrglobal id ofs => Gl id ofs
      | _ => Ptop
      end
  end.

Lemma aaddr_arg_sound_1:
  forall {F V : Type} (ge : Genv.t F V) bc rs ae m rm am sp a b ofs,
  ematch bc rs ae ->
  romatch bc m rm ->
  mmatch bc m am ->
  genv_match bc ge ->
  bc sp = BCstack ->
  eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m a (Vptr b ofs) ->
  pmatch bc b ofs (aaddr_arg (VA.State ae am) a).

Lemma aaddr_arg_sound:
  forall relax cunit prog s f sp pc e m a b ofs,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  eval_builtin_arg (Genv.globalenv prog) (fun r => e#r) (Vptr sp Ptrofs.zero) m a (Vptr b ofs) ->
  exists bc,
     pmatch bc b ofs (aaddr_arg (analyze relax (romem_for cunit) f)!!pc a)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.

Definition xaaddr_arg (rm: romem) (a: VA.t) (ba: builtin_arg reg) : aptr :=
  match a with
  | VA.Bot => Pbot
  | VA.State ae am => aptr_of_aval (abuiltin_arg ae am rm ba)
  end.

Lemma xaaddr_arg_sound_1:
  forall {F V : Type} (ge : Genv.t F V) bc rs ae m rm am sp a b ofs,
  ematch bc rs ae ->
  romatch bc m rm ->
  mmatch bc m am ->
  genv_match bc ge ->
  bc sp = BCstack ->
  eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m a (Vptr b ofs) ->
  pmatch bc b ofs (xaaddr_arg rm (VA.State ae am) a).

Lemma xaaddr_arg_sound:
  forall relax cunit prog s f sp pc e m a b ofs,
  sound_state relax prog (State s f (Vptr sp Ptrofs.zero) pc e m) ->
  linkorder cunit prog ->
  eval_builtin_arg (Genv.globalenv prog) (fun r => e#r) (Vptr sp Ptrofs.zero) m a (Vptr b ofs) ->
  exists bc,
     pmatch bc b ofs (xaaddr_arg (romem_for cunit) (analyze relax (romem_for cunit) f)!!pc a)
  /\ genv_match bc (Genv.globalenv prog)
  /\ bc sp = BCstack.