Module BTL_ValueAnalysis


Require Import Coqlib ZArith Lattice.
Require Import AnalysisDomain.
Require Import ValueDomain ValueAOp.
Require Import Linking AST Op Registers Builtins.
Require Import Values Memory Integers Globalenvs Events.
Require Import OptionMonad.
Require ValueAnalysis BTL BTL_AnalysisLib.
Require Axioms.


Notation areg := ValueAnalysis.areg.
Notation aregs := ValueAnalysis.aregs.
Notation ae_set_multiple := ValueAnalysis.ae_set_multiple.
Notation ematch_restrict := ValueAnalysis.ematch_restrict.
Notation ematch_restrict_multiple := ValueAnalysis.ematch_restrict_multiple.

Lemma match_not_invalid bc b ofs x
  (MATCH : vmatch bc (Vptr b ofs) x):
  bc b <> BCinvalid.
Proof.
  assert (A: pmatch bc b ofs Ptop)
    by (inv MATCH; eapply pmatch_top'; eauto).
  inv A. assumption.
Qed.

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.

Lemma romatch_storev
     : forall (bc : block_classification) (chunk : memory_chunk)
         (m : mem) (ptr v : val)
         (m' : mem) (rm : romem),
       Mem.storev chunk m ptr v = Some m' ->
       romatch bc m rm -> romatch bc m' rm.
Proof.
  intros.
  unfold Mem.storev in *.
  destruct ptr; try discriminate.
  eapply romatch_store; eauto.
Qed.

Local Hint Resolve romatch_storev : va.


Module ValueAADomain (IR : IRspec) <: AADomain IR.
  Module VA := VAW.
 
  Inductive astate' : Type :=
    mk_astate (ae : aenv) (am : amem).
  Definition astate : Type := astate'.
  Definition Astate (aa : astate) : VA.t :=
    let (ae, am) := aa in VA.State ae am.
  Definition filter_astate (aa : VA.t) : option astate :=
    match aa with
    | VA.Bot => None
    | VA.State ae am => Some (mk_astate ae am)
    end.
  Lemma filter_astate_bot: filter_astate VA.bot = None.
  Proof.
reflexivity. Qed.
  Lemma filter_iff_Astate s s': filter_astate s = Some s' <-> s = Astate s'.
  Proof.
    destruct s, s'; unfold Astate; simpl; split; try congruence.
    injection 1 as <- <-; reflexivity.
  Qed.
  Lemma filter_ge s s': VA.ge s s' -> filter_astate s = None -> filter_astate s' = None.
  Proof.
    case s, s'; simpl; solve [tauto|congruence].
  Qed.

  Definition eforget (rl : list reg) (aa : astate) : astate :=
    let (ae, am) := aa in
    mk_astate (ValueDomain.eforget rl ae) am.
  Lemma eforget_ge : forall rl aa,
      VA.ge (Astate (eforget rl aa)) (Astate aa).
  Proof.
    intros. destruct aa as (ae, am). cbn.
    split. 2: auto; fail.
    apply ValueDomain.eforget_ge.
  Qed.

  Definition default_top : VA.t := VA.State AE.top mtop.
  Lemma ge_default_top s': VA.ge default_top s'.
  Proof.
    case s'; simpl; intuition.
    - apply AE.ge_top.
    - eapply mmatch_top'; eassumption.
  Qed.

  Definition entry_state (f : IR.function) : VA.t :=
    VA.State (einit_regs (IR.fn_params f) (IR.fn_sig f).(sig_args)) ValueAnalysis.mfunction_entry.

  Definition program := AST.program (fundef IR.function) unit.
  Definition prog_info : Type := romem.
  Definition get_prog_info (p : program) : prog_info := ValueAnalysis.romem_for p.
 
  Definition transfer_op (_ : prog_info) (op : operation) (args : list reg) (res : reg) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    let a := eval_static_operation op (aregs ae args) in
    VA.State (AE.set res a ae) am.

  Definition transfer_load (rm : prog_info) (trap : trapping_mode) (chunk : memory_chunk) (addr : addressing)
                           (args : list reg) (dst : reg) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    let v := match trap with
             | TRAP => ValueDomain.loadv chunk rm am (eval_static_addressing addr (aregs ae args))
             | NOTRAP => Vtop
             end in
    VA.State (AE.set dst v ae) am.

  Definition transfer_store (_ : prog_info) (chunk : memory_chunk) (addr : addressing) (args : list reg)
                            (src : reg) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    let am' := ValueDomain.storev chunk am
                  (eval_static_addressing addr (aregs ae args))
                  (areg ae src) in
    VA.State ae am'.

  Notation filter_condition := ValueAnalysis.filter_condition.
  Definition transfer_condition (_ : prog_info) (cond : condition) (args : list reg) (aa : astate) : VA.t * VA.t :=
    let (ae, am) := aa in
    match eval_static_condition cond (aregs ae args) with
    | Bnone => (VA.Bot, VA.Bot)
    | (Just true | Maybe true) =>
        (VA.State ae am, VA.Bot)
    | (Just false | Maybe false) =>
        (VA.Bot, 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 (_ : prog_info) (args : list reg) (res : reg) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    ValueAnalysis.transfer_call ae am args res.

  Definition transfer_builtin (rm : prog_info) (ef : external_function) (args : list (builtin_arg reg))
                              (res : builtin_res reg) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    ValueAnalysis.transfer_builtin ae am rm ef args res.

  Definition transfer_jumpi (_ : prog_info) (arg : reg) (i : int) (aa : astate) : VA.t :=
    let (ae, am) := aa in
    VA.State (AE.set arg (I i) ae) am.

  Definition widen_node (_ : IR.function) (_ : IR.node) : bool := false.

Semantics

  Local Notation genv := (Genv.t (fundef IR.function) unit).

  Inductive asmatch' (bc : block_classification) (rm : romem) (ge : genv) (sp : block) (e : RTL.regset) (m : mem)
                     (ae : aenv) (am : amem) : Prop :=
    asmatch_intro
        (EM: ematch bc e ae)
        (RO: romatch bc m rm)
        (MM: mmatch bc m am)
        (GE: genv_match bc ge)
        (SP: bc sp = BCstack).

  Definition asmatch (rm : prog_info) (ge : genv) (bc : ghost_env) (sp : block) (rs : RTL.regset) (m : mem)
                     (aa : astate): Prop :=
    let (ae, am) := aa in
    asmatch' bc rm ge sp rs m ae am.

  Inductive valid_callstate' (bc : block_classification) (rm : romem) (ge : genv) (m : mem) (args : list val)
                             : Prop :=
    valid_callstate_intro
        (ARGS: Forall (fun v => vmatch bc v Vtop) args)
        (RO: romatch bc m rm)
        (MM: mmatch bc m mtop)
        (GE: genv_match bc ge)
        (NOSTK: ValueAnalysis.bc_nostack bc).
      
  Definition valid_callstate (rm : prog_info) (ge : genv) (bc : ghost_env) (m : mem) (args : list val): Prop :=
    valid_callstate' bc rm ge m args.

  Inductive valid_returnstate' (bc : block_classification) (rm : romem) (ge : genv) (m : mem) (vres : val)
                               : Prop :=
    valid_returnstate_intro
        (RES: vmatch bc vres Vtop)
        (RO: romatch bc m rm)
        (MM: mmatch bc m mtop)
        (GE: genv_match bc ge)
        (NOSTK: ValueAnalysis.bc_nostack bc).

  Definition valid_returnstate (rm : prog_info) (ge : genv) (bc : ghost_env) (m : mem) (vres : val): Prop :=
    valid_returnstate' bc rm ge m vres.
  
  Inductive succ_state' (bound : block)
                        (bc0 : block_classification) (m0 : mem) (bc1 : block_classification) (m1 : mem): Prop :=
    succ_state_intro
      (SC_BC: forall b, Plt b bound -> bc1 b = bc0 b)
      (SC_LOAD: forall b ofs n bytes,
                  Plt b bound -> bc0 b = BCinvalid -> n >= 0 ->
                  Mem.loadbytes m1 b ofs n = Some bytes ->
                  Mem.loadbytes m0 b ofs n = Some bytes)
      (SC_NXTB: Ple (Mem.nextblock m0) (Mem.nextblock m1)).
  
  Definition succ_state (_ : prog_info) (_ : genv) (bound : block)
                        (bc0 : ghost_env) (m0 : mem) (bc1 : ghost_env) (m1 : mem): Prop :=
    succ_state' bound bc0 m0 bc1 m1.
  
  Lemma asmatch_ge pi ge gh sp rs m s0 s1
    (GE : VA.ge (Astate s1) (Astate s0))
    (MATCH : asmatch pi ge gh sp rs m s0):
    asmatch pi ge gh sp rs m s1.
  Proof.
    case s0 as (ae0, am0), s1 as (ae1, am1), GE as (GE_E & GE_M).
    destruct MATCH; constructor; eauto using ematch_ge.
  Qed.
 


  Lemma succ_state_refl pi ge bd gh m:
    succ_state pi ge bd gh m gh m.
  Proof.
    constructor; solve [reflexivity|tauto].
  Qed.

  Lemma succ_state_trans pi ge bd gh0 m0 gh1 m1 gh2 m2:
    succ_state pi ge bd gh0 m0 gh1 m1 ->
    succ_state pi ge bd gh1 m1 gh2 m2 ->
    succ_state pi ge bd gh0 m0 gh2 m2.
  Proof.
    intros [A0 B0] [A1 B1]; constructor; intros.
    - rewrite A1, A0 by assumption. reflexivity.
    - apply B0; auto. apply B1; auto.
      rewrite A0; auto.
    - etransitivity; eassumption.
  Qed.

  Lemma succ_state_new_bound bd bd' gh0 m0 gh1 m1:
    succ_state' bd' gh0 m0 gh1 m1 ->
    Ple bd bd' ->
    succ_state' bd gh0 m0 gh1 m1.
  Proof.
    intros [] Le; constructor; intros;
    [eapply SC_BC|eapply SC_LOAD|eassumption]; eauto using Plt_Ple_trans.
  Qed.

  Lemma succ_state_new_bc (bc : block_classification) m bd (bc1 : block_classification)
    (H : forall b : positive, Plt b bd -> bc1 b = bc b):
    succ_state' bd bc m bc1 m.
  Proof.
    constructor; solve [reflexivity|tauto].
  Qed.
  
  Lemma succ_state_free m b lo hi m' bc bd
    (FREE : Mem.free m b lo hi = Some m'):
    succ_state' bd bc m bc m'.
  Proof.
    constructor.
    - reflexivity.
    - intros. eapply Mem.loadbytes_free_2; eauto.
    - erewrite <- Mem.nextblock_free by eauto. reflexivity.
  Qed.
  
  Lemma succ_state_store chk m b ofs v m' (bc : block_classification) bound
    (BC : bc b <> BCinvalid)
    (STORE : Mem.store chk m b ofs v = Some m'):
    succ_state' bound bc m bc m'.
  Proof.
    constructor.
    - reflexivity.
    - intros. rewrite <- H2; symmetry.
      eapply Mem.loadbytes_store_other. eassumption.
      left; congruence.
    - erewrite <- Mem.nextblock_store by eauto. reflexivity.
  Qed.



  Lemma romem_for_consistent_2 (prog cunit : program)
    (LINK : linkorder cunit prog):
    ValueAnalysis.romem_consistent (prog_defmap prog) (ValueAnalysis.romem_for cunit).
  Proof.
    intros; red; intros.
    exploit (ValueAnalysis.romem_for_consistent cunit); eauto.
    intros (v & DM & RO & VO & AB).
    destruct (prog_defmap_linkorder _ _ _ _ LINK DM) as (gd & P & Q).
    inv Q. exists v2.
    split; auto.
    inv H1; simpl in *.
    inv H2; simpl in *; intuition (auto with *).
  Qed.

  Theorem initial_mem_matches (prog : program) m
    (INIT : Genv.init_mem prog = Some m):
    let ge := Genv.globalenv prog in
    exists bc,
       genv_match bc ge
    /\ bc_below bc (Mem.nextblock m)
    /\ ValueAnalysis.bc_nostack bc
    /\ (forall cunit, linkorder cunit prog -> romatch bc m (ValueAnalysis.romem_for cunit))
    /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid).
  Proof.
    intro ge.
    ecase ValueAnalysis.initial_block_classification as (bc & GE & BELOW & NOSTACK & INV & VALID); eauto.
    exists bc; ValueAnalysis.splitall; auto.
    intros.
    assert (A: ValueAnalysis.initial_mem_match bc m ge).
    { eapply (ValueAnalysis.alloc_globals_match prog bc GE) with (m := Mem.empty); auto.
      red. unfold Genv.find_symbol; simpl; intros.
      rewrite ValueAnalysis.genv_find_empty in H1.
      discriminate.
    }
    assert (B: ValueAnalysis.romem_consistent (prog_defmap prog) (ValueAnalysis.romem_for cunit))
        by (apply romem_for_consistent_2; auto).
    red; intros.
    exploit B; eauto. intros (v & DM & RO & NVOL & EQ).
    rewrite Genv.find_def_symbol in DM. destruct DM as (b1 & FS & FD).
    rewrite <- Genv.find_var_info_iff in FD.
    assert (b1 = b).
    { rewrite INV with (b:=b) in FS by auto.
      congruence.
    }
    subst b1.
    split. destruct oab.
    - destruct EQ as (DEFN & X); [congruence | inv X].
      intros ab X. inv X. split.
      * apply ValueAnalysis.store_init_data_list_summary. constructor.
      * split. { eapply A; eauto. }
        intros; eapply ablock_load_sound; eauto.
    - intros ab X; inv X.
    - intros; exploit Genv.init_mem_characterization; eauto.
      intros (P & Q & R1 & R2).
      red; intros. exploit Q; eauto. intros [U V].
      unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V.
  Qed.

  Lemma initial_valid_callstate prog b f m cu:
    let ge := Genv.globalenv prog in
    Genv.init_mem prog = Some m ->
    Genv.find_symbol ge prog.(prog_main) = Some b ->
    Genv.find_funct_ptr ge b = Some f ->
    IR.funsig f = signature_main ->
    forall (LINK : linkorder cu prog),
    exists gh, valid_callstate (get_prog_info cu) (Genv.globalenv prog) gh m nil.
  Proof.
    intros.
    ecase initial_mem_matches as (bc & GE & ? & NS & RO & ?); eauto.
    exists bc; constructor; auto.
    apply mmatch_inj_top with m.
    replace (inj_of_bc bc) with (Mem.flat_inj (Mem.nextblock m)).
    eapply Genv.initmem_inject; eauto.
    symmetry; apply Axioms.extensionality; unfold Mem.flat_inj; intros x.
    destruct (plt x (Mem.nextblock m)).
    apply inj_of_bc_valid; auto.
    unfold inj_of_bc. erewrite bc_below_invalid; eauto.
  Qed.

  
  Lemma sound_tailcall pi ge gh sp m lo hi m' rs aa args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (MEM : Mem.free m sp lo hi = Some m'):
    exists gh',
      valid_callstate pi ge gh' m' (rs ## args) /\
      (forall gh1 m1, succ_state pi ge (Mem.nextblock m') gh' m' gh1 m1 ->
                      succ_state pi ge sp gh m gh1 m1).
  Proof.
    case aa as (ae, am), MATCH.
    ecase (ValueAnalysis.anonymize_stack ge) as (bc' & A & B & C & D & E & F & G); eauto.
    exists bc'; split; [constructor; auto|].
    - apply Forall_map; apply Forall_forall.
      intros r _.
      eapply D; eauto with va.
    - eapply romatch_free; eauto.
    - eapply mmatch_free; eauto.
    - intros ? ? SUCC.
      erewrite Mem.nextblock_free in SUCC by eauto.
      do 2 only 1 : eapply succ_state_trans.
      + eapply succ_state_free; eauto.
      + eapply succ_state_new_bc; intros.
        apply C; apply Plt_ne; assumption.
      + eapply succ_state_new_bound; eauto.
        apply Plt_Ple. eapply mmatch_below; eauto. congruence.
  Qed.
  
  Lemma sound_return pi ge gh sp m lo hi m' rs aa or
    (MATCH : asmatch pi ge gh sp rs m aa)
    (MEM : Mem.free m sp lo hi = Some m'):
    exists gh',
      valid_returnstate pi ge gh' m' (regmap_optget or Vundef rs) /\
      succ_state pi ge sp gh m gh' m'.
  Proof.
    case aa as (ae, am), MATCH.
    ecase (ValueAnalysis.anonymize_stack ge) as (bc' & A & B & C & D & E & F & G); eauto.
    exists bc'; split; [constructor;auto|].
    - destruct or; simpl; eapply D.
      + apply ValueAnalysis.areg_sound. eassumption.
      + apply vmatch_num with (p := Pbot). trivial.
    - eapply romatch_free; eauto.
    - eapply mmatch_free; eauto.
    - eapply succ_state_trans.
      + eapply succ_state_free; eauto.
      + eapply succ_state_new_bc; intros.
        apply C; apply Plt_ne; assumption.
  Qed.
  
  Lemma sound_external_call pi ge gh m args ef t res m'
    (VCS : valid_callstate pi ge gh m args)
    (EXTCALL : external_call ef ge args m t res m'):
    exists gh',
      valid_returnstate pi ge gh' m' res /\
      succ_state pi ge (Mem.nextblock m) gh m gh' m'.
  Proof.
    case VCS as [].
    rewrite Forall_forall in ARGS.
    ecase (ValueAnalysis.external_call_match ge) as (bc' & A & B & C & D & E & F & G & K); eauto.
    exists bc'; split; [constructor; auto|constructor].
    - apply B.
    - intros; rewrite <- K; auto.
    - eapply external_call_nextblock; eassumption.
  Qed.

  Lemma function_init pi ge gh m args f m' sp
    (VCS : valid_callstate pi ge gh m args)
    (ARGTYPE: Val.has_argtype_list args (IR.fn_sig f).(sig_args))
    (ALLOC: Mem.alloc m 0 (IR.fn_stacksize f) = (m', sp)):
    exists aa gh',
      entry_state f = Astate aa /\
      asmatch pi ge gh' sp (RTL.init_regs args (IR.fn_params f)) m' aa /\
      succ_state pi ge sp gh m gh' m'.
  Proof.
    case VCS as [].
    ecase (ValueAnalysis.allocate_stack ge) as (bc' & A & B & C & D & E & F & G); eauto.
    eexists (mk_astate _ _), bc'; split. reflexivity.
    split; [constructor; auto|].
    - apply ematch_init.
      + assumption.
      + apply Forall_forall; eapply Forall_impl. 2:exact ARGS.
        simpl. intro; apply G.
    - constructor.
      + exact F.
      + apply Mem.alloc_result in ALLOC as sp_eq; subst sp.
        intros; erewrite <- Mem.loadbytes_alloc_unchanged; eauto.
      + apply Mem.nextblock_alloc in ALLOC as ->. apply Ple_succ.
  Qed.

  Section TRANSFER_SOUNDNDESS.

    Variables (pi : prog_info) (ge : genv) (gh : ghost_env) (sp : block) (rs : RTL.regset) (m : mem)
              (s0 : astate).

  Lemma transfer_op_correct op args res v
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_operation ge (Vptr sp Ptrofs.zero) op rs ## args m = Some v):
    exists s1,
      transfer_op pi op args res s0 = Astate s1 /\
      asmatch pi ge gh sp (rs#res <- v) m s1.
  Proof.
    case s0 as (ae, am), MATCH.
    eexists (mk_astate _ _); split. reflexivity.
    constructor; auto.
    apply ematch_update; auto.
    eapply eval_static_operation_sound; eauto with va.
  Qed.

  Lemma transfer_load_correct trap chunk addr args res v
    (MATCH : asmatch pi ge gh sp rs m s0)
    (LOAD : RTL.has_loaded ge (Vptr sp Ptrofs.zero) rs m chunk addr args v trap):
    exists s1,
      transfer_load pi trap chunk addr args res s0 = Astate s1 /\
      asmatch pi ge gh sp (rs#res <- v) m s1.
  Proof.
    case s0 as (ae, am), MATCH.
    eexists (mk_astate _ _); split. reflexivity.
    constructor; auto.
    apply ematch_update; auto.
    inv LOAD.
    - (* has_loaded_normal *)
      eapply eval_static_addressing_sound in EVAL; eauto with va.
      eapply loadv_sound in LOAD0; eauto.
      case trap; eauto using vmatch_top.
    - (* has_loaded_default *)
      constructor.
  Qed.

  Lemma transfer_store_correct chunk addr args a src m'
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a)
    (STORE : Mem.storev chunk m a rs # src = Some m'):
    exists s1,
      transfer_store pi chunk addr args src s0 = Astate s1 /\
      asmatch pi ge gh sp rs m' s1 /\
      succ_state pi ge sp gh m gh m'.
  Proof.
    case s0 as (ae, am), MATCH.
    eapply eval_static_addressing_sound in EVAL; eauto with va.
    eexists (mk_astate _ _); split. reflexivity.
    split. constructor; eauto with va.
    - eapply storev_sound; eauto.
    - destruct a; try discriminate STORE; simpl in STORE.
      eapply succ_state_store; eauto.
      eapply match_not_invalid; eauto.
  Qed.

  Lemma filter_condition_sound cond args ae
    (EMATCH : ematch gh rs ae)
    (COND : eval_condition cond (rs ## args) m = Some true):
    ematch gh rs (filter_condition cond args ae).
  Proof.
    unfold filter_condition.
    apply ematch_restrict_multiple. 2: assumption.
    apply filter_static_condition_sound with (m := m). 2: assumption.
    apply ValueAnalysis.aregs_sound.
    assumption.
  Qed.

  Lemma transfer_condition_correct cond args b
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_condition cond rs ## args m = Some b):
    exists s1,
      (let (sso, snot) := transfer_condition pi cond args s0 in
       if b then sso else snot) = Astate s1 /\
      asmatch pi ge gh sp rs m s1.
  Proof.
    case s0 as (ae, am), MATCH.
    assert (EVALN : eval_condition (negate_condition cond) rs ## args m = Some (negb b))
      by (rewrite eval_negate_condition, EVAL; reflexivity).
    assert (ARGS: list_forall2 (vmatch gh) rs ## args (aregs ae args))
      by auto with va.
    pose proof (eval_static_condition_sound gh cond (rs ## args) m (aregs ae args) ARGS) as COND.
    unfold transfer_condition; rewrite EVAL in COND.
    set (sc := eval_static_condition cond (aregs ae args)) in *; clearbody sc.
    inversion COND; subst;
      (destruct b; eexists (mk_astate _ _);
        (split; [reflexivity | try assumption||constructor;auto]));
      apply filter_condition_sound; eauto.
  Qed.

  Lemma transfer_call_correct args res
    (MATCH : asmatch pi ge gh sp rs m s0):
    exists gh_ce0,
      valid_callstate pi ge gh_ce0 m (rs ## args) /\
    forall gh_ce1 m' vres,
      valid_returnstate pi ge gh_ce1 m' vres ->
      succ_state pi ge (Mem.nextblock m) gh_ce0 m gh_ce1 m' ->
    exists s1 gh_cr1,
      transfer_call pi args res s0 = Astate s1 /\
      asmatch pi ge gh_cr1 sp (rs # res <- vres) m' s1 /\
      succ_state pi ge sp gh m gh_cr1 m'.
  Proof.
    case s0 as (ae0, am0), MATCH.
    assert (SP_LT: Plt sp (Mem.nextblock m)).
      { eapply mmatch_below; eauto. congruence. }
    unfold transfer_call, ValueAnalysis.transfer_call, ValueAnalysis.analyze_call.
    case (pincl (am_nonstack am0) Nonstack &&
          forallb (fun av : aval => vpincl av Nonstack) (aregs ae0 args))
         eqn:NOLEAK.
    - (* private call *)
      InvBooleans. rename H into NSTACK, H0 into ARGS.
        rewrite forallb_forall, <- Forall_forall in ARGS; apply Forall_map in ARGS.
      ecase (ValueAnalysis.hide_stack ge) as (bc_ce0 & A & B & C & D & E & F & G); eauto using pincl_ge.
      exists bc_ce0; split.
        { constructor; auto.
          apply Forall_map. eapply Forall_impl. 2:exact ARGS.
          simpl; intros r INCL; apply vpincl_ge in INCL.
          eapply D; eauto. }

      intros bc_ce1 m' vres [] [].
      ecase (ValueAnalysis.return_from_private_call ge)
        with (caller := gh) (callee := bc_ce1) (bound := Mem.nextblock m) (m := m') (am := am0)
        as (bc_cr1 & H & I & J & K & L & M & N & _);
        eauto using mmatch_below.
       { rewrite SC_BC; eauto. }
       { intros. rewrite SC_BC, C by assumption. reflexivity. }
       { eapply bmatch_ext. { apply MM; assumption. }
         intros; apply SC_LOAD; assumption. }
      eexists (mk_astate _ _), bc_cr1; split. reflexivity.
      split. constructor; auto.
      + apply ematch_update; auto.
      + constructor; auto.
        intros. apply SC_LOAD; auto.
        * transitivity sp; auto.
        * rewrite C; auto. apply Plt_ne; assumption.

    - (* public call *)
      ecase (ValueAnalysis.anonymize_stack ge) as (bc_ce0 & A & B & C & D & E & F & G); eauto.
      exists bc_ce0; split.
        { constructor; eauto.
          apply Forall_map; apply Forall_forall.
          intros r _; eapply D; eauto. }

      intros bc_ce1 m' vres [] [].
      ecase (ValueAnalysis.return_from_public_call ge)
        with (caller := gh) (callee := bc_ce1) (bound := Mem.nextblock m) (m := m')
        as (bc_cr1 & H & I & J & K & L & M & N & _);
        eauto using mmatch_below.
       { rewrite SC_BC; eauto. }
       { intros. rewrite SC_BC, C by assumption. reflexivity. }
      eexists (mk_astate _ _), bc_cr1; split. reflexivity.
      split. constructor; auto.
      + apply ematch_update; auto.
      + constructor; auto.
        intros. apply SC_LOAD; auto.
        * transitivity sp; auto.
        * rewrite C; auto. apply Plt_ne; assumption.
  Qed.

  Lemma transfer_builtin_correct args vargs ef t vres m' res
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_builtin_args ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m args vargs)
    (CALL : external_call ef ge vargs m t vres m'):
    exists s1 gh',
      transfer_builtin pi ef args res s0 = Astate s1 /\
      asmatch pi ge gh' sp (regmap_setres res vres rs) m' s1 /\
      succ_state pi ge sp gh m gh' m'.
  Proof.
    case s0 as (ae, am), MATCH.
    unfold transfer_builtin.
    ecase ValueAnalysis.sound_exec_builtin as (bc' & ae' & am' & -> & EM' & RO' & MM' & GE' & SP' & PR); eauto.
    eexists (mk_astate _ _), bc'; split. reflexivity.
    split. constructor; auto.
    destruct PR; constructor; try assumption.
    eapply external_call_nextblock; eassumption.
  Qed.

  Lemma transfer_jumpi_correct arg i
    (MATCH : asmatch pi ge gh sp rs m s0)
    (R_EQ : rs # arg = Vint i):
    exists s1,
      transfer_jumpi pi arg i s0 = Astate s1 /\
      asmatch pi ge gh sp rs m s1.
  Proof.
    case s0 as (ae, am), MATCH.
    eexists (mk_astate _ _); split. reflexivity.
    constructor; auto.
    apply ematch_restrict. 2:assumption.
    rewrite R_EQ.
    constructor.
  Qed.

  End TRANSFER_SOUNDNDESS.

  Global Opaque transfer_op transfer_load transfer_store filter_condition transfer_condition
                transfer_call transfer_builtin transfer_jumpi.
End ValueAADomain.


Module AAD := ValueAADomain BTL_AnalysisLib.BTL_IRspec.
Module AA := BTL_AnalysisLib.BTL_AbstractAnalysis AAD.
Definition analyze : romem -> BTL.function -> Maps.PMap.t VA.t := AA.analyze.


Module Type AnnotConfig.
  Parameter conservative_bot : bool.
End AnnotConfig.

Module BTL_ValueAADomain_Annotate (C : AnnotConfig) <: BTL_AnalysisLib.BTL_AADomain_Annotate.
  Include AAD.
  
  Definition unreachable_inst_promotable (_ : operation + condition) (_ : list reg) := BTL.IPromNone.
  Definition unreachable_addr_aval : option ValueDomain.aval :=
    if C.conservative_bot then None else Some Vbot.
  Definition c_aaddr (a : aval) : option aval :=
    if C.conservative_bot
    then match a with
         | Vbot | I _ | IU _ | L _ | F _ | FS _ | Num _ => None
         | Uns p _ | Sgn p _ | Ptr p | Ifptr p =>
             match p with
             | Pbot => None
             | _ => Some a
             end
         end
    else Some a.

  Lemma c_addr_correct bc v (a: aval):
    vmatch bc v a ->
    if_Some (c_aaddr a) (vmatch bc v).
  Proof.
    unfold c_aaddr; repeat autodestruct; simpl; trivial.
  Qed.

  Definition op_inst_promotable (_ : prog_info) (_ : astate) (_ : operation) (_ : list reg) := BTL.IPromNone.
  Definition cond_inst_promotable (_ : prog_info) (_ : astate) (_ : condition) (_ : list reg) := BTL.IPromNone.
  Definition get_addr_aval (pi : prog_info) (aa : astate) (addr : addressing) (args : list reg) : option aval :=
    let (ae, am) := aa in
    c_aaddr (eval_static_addressing addr (aregs ae args)).

  Section SOUNDNESS.
    Variables (pi : prog_info) (ge : BTL.genv) (gh : ghost_env) (sp : block) (rs : RTL.regset) (m : mem)
              (aa : astate).

  Lemma op_inst_promotable_correct op prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : op_inst_promotable pi aa op args = BTL.IPromotableOp prom)
    (ALIVE : eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m <> None):
    BTL.adp_op_promotable ge (Vptr sp Ptrofs.zero) m op prom rs##args.
  Proof.
discriminate PROM. Qed.
  
  Lemma cond_inst_promotable_correct cond prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : cond_inst_promotable pi aa cond args = BTL.IPromotableCond prom)
    (ALIVE : eval_condition cond rs##args m <> None):
    BTL.adp_cond_promotable m cond prom rs##args.
  Proof.
discriminate PROM. Qed.

  Lemma get_addr_aval_correct addr args aaddr a
    (MATCH : asmatch pi ge gh sp rs m aa)
    (AADDR : get_addr_aval pi aa addr args = Some aaddr)
    (EVAL : eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a):
    vmatch gh a aaddr.
  Proof.
    case aa as (ae, am).
    revert aaddr AADDR. apply if_Some_iff. apply c_addr_correct.
    destruct MATCH.
    eapply eval_static_addressing_sound; eauto with va.
  Qed.

  End SOUNDNESS.

End BTL_ValueAADomain_Annotate.
Generated by coq2html