Module BTL_BlockSimulationproof

Proof of BTL Block Simulation modulo Gluing (Symbolic) Invariants. Simulation diagram (for the "main" lemma iblock_step_simulation)


(0) = Initial symbolic states: sis_source_correct & sis_target_correct
(1) = Source symbolic execution: sexec_correct
(2) = Symbolic simulation test
(3) = Coming back to concrete states: sexec_exact.
(4) = final_step_simulation + sfv_equiv

       stk0          stk0                     stk1          stk1
        f0            f0                       f1            f1
               . . . . . . . . . . . . . . . . . . . . .
             .                                           .
           .                                               .
         .    (0)                                     (0)    .
       cs0 +++++++++ ss0                      ss1 ++++++++++ cs1
        |             |                        |              |
        |             |                        |              |
        |             |                        |              |
        |    (1)      |                        |      (3)     |
        |             |                        |              |
        |             |                        |              |
        |             |                        |              |
        |             |                        |              |
        V             V          (2)           V              V
       cf0' ++++++++ sf0 ==================== sf1' ++++++++ cf1'
        |                                                     |
        |                                                     |
        |                        (4)                          |
        V                                                     V
       cs0' . . . . . . . . . . . . . . . . . . . . . . . . cs1'

  Legend:
    - cs* -> concrete states
    - cf* -> concrete final states (i.e. concrete state + final value)
    - ss* -> symbolic states
    - sf* -> symbolic final states (i.e. symbolic state + symbolic final value)
    - *0  -> Source initial state
    - *1  -> Target initial state
    - *0' -> Source final state
    - *1' -> Target final state
    - "...." is match_invs / match_states
    - "++++" is sem_sistates (+ sfv_equiv for final states)
    - "====" is match_sexec_si

  Remark:
   - cs0 = <sp,rs0,m0>
   - tr_sis is used to define ssS and ssI using tr_sis_elim_match_si
     and to deduce properties on the concrete states from match_sexec_si
     using tr_sis_intro_match_si

Require Import AST Linking IPass Values Maps Globalenvs Smallstep Registers.
Require Import Coqlib Events Errors OptionMonad.
Require Import RTL BTL BTL_SEtheory.
Require Import BTLmatchRTL BTL_BlockSimulation.
Require Import ValueDomain.
Require BTL_ResetAnnots BTL_AnalysisLib.

Module BTL_BlockSimulationproof (B: BTL_BlockSimulationConfig).

Include BTL_BlockSimulation B.

Definition match_prog (p tp: program) :=
match_program (fun cu f tf => transf_fundef f = OK tf) eq p tp.

Definition pass := mkpass match_prog.

Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.

Proof.

intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.

Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.

Proof.

rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved:
Senv.equiv pge tpge.

Proof.

eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct pge v = Some f ->
  exists tf cunit,
    transf_fundef f = OK tf /\
    Genv.find_funct tpge v = Some tf /\
    linkorder cunit prog.

Proof.

  intros. exploit (Genv.find_funct_match TRANSL); eauto.
  intros (cu & tf & A & B & C).
  exists tf. exists cu.
  intuition eauto.
Qed.

Lemma transf_function_correct f f':
transf_function f = OK f' -> match_function f f'.

Proof.

  unfold transf_function. intros H.
  assert (OH: transf_function f = OK f') by auto.
  destruct (btl_optim_oracle f); destruct p;
  monadInv H.
  exploit transf_function_only_liveness; intuition eauto.
  simpl in *; econstructor; eauto.
  eapply check_symbolic_simu_correct; eauto.
Qed.

Lemma transf_fundef_correct f f':
transf_fundef f = OK f' -> match_fundef f f'.

Proof.

  intros TRANSF; destruct f; simpl; inv TRANSF.
  + monadInv H0. exploit transf_function_correct; eauto.
    intros. econstructor; eauto.
  + eapply match_External.
Qed.

Lemma function_ptr_translated:
  forall b f,
  Genv.find_funct_ptr pge b = Some f ->
  exists cunit tf, Genv.find_funct_ptr tpge b = Some tf
                   /\ transf_fundef f = OK tf
                   /\ linkorder cunit prog.

Proof.

intros.
exploit (Genv.find_funct_ptr_match TRANSL); eauto.
Qed.

Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = funsig f.

Proof.

intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
symmetry; erewrite preserv_fnsig; eauto.
Qed.

Theorem transf_initial_states:
forall s1, initial_state prog s1 ->
exists s2, initial_state tprog s2 /\ match_states pge s1 s2.

Proof.

  intros. inv H.
  exploit function_ptr_translated; eauto. intros (cu & tf & FIND & TRANSF & LINK).
  eexists. split.
  - econstructor; eauto.
    + intros; apply (Genv.init_mem_match TRANSL); eauto.
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
      symmetry. eapply match_program_main. eauto.
    + erewrite function_sig_translated; eauto.
  - apply transf_fundef_correct in TRANSF. inv TRANSF;
    repeat (econstructor; eauto).
Qed.

Lemma transf_final_states s1 s2 r:
match_states pge s1 s2 -> final_state s1 r -> final_state s2 r.

Proof.

intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Lemma symbols_preserved_rev s: Genv.find_symbol pge s = Genv.find_symbol tpge s.

Proof.

symmetry; apply symbols_preserved.
Qed.

Section FINAL_STEP.

Lemma find_function_v_preserved fp fd:
  find_function_v pge fp = Some fd ->
  exists tf,
    find_function_v tpge fp = Some tf /\
    transf_fundef fd = OK tf.

Proof.

  destruct fp; simpl.
  - intros; ecase functions_translated as (tf & cu & TF & TPGE & _); eauto.
  - rewrite symbols_preserved. repeat autodestruct. intros.
    ecase function_ptr_translated as (tf & cu & TF & TPGE & _); eauto.
Qed.

Variables (f0 f1 : function) (sp0 : val) (rs0 rs1 : regset)
          (m0 m1 : Memory.Mem.mem) (bc : block_classification).

Let ctx := Bcctx pge sp0 rs0 rs1 m1 bc.

Lemma final_step_simulation stk0 stk1 (fin : finalA val) t s0
  (MF : match_function f0 f1)
  (STACK : list_forall2 (match_stackframes pge) stk0 stk1)
  (MATCH_H : let (P, S) := si_sfv_set (fun pc => history (fn_gm f1 pc)) fin in
             P /\ forall si, S si -> match_si ctx si rs0)
  (MATCH_G : let (P, S) := si_sfv_set (fun pc => glue (fn_gm f1 pc)) fin in
             P /\ forall si, S si -> match_si ctx si rs1)
  (MATCH_M : let (P, S) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
             P /\ forall im, S im -> match_meminv ctx im m0)
  (FINAL : final_step_v pge stk0 f0 sp0 rs0 m0 bc fin t s0):
  exists s1,
    final_step_v tpge stk1 f1 sp0 rs1 m1 bc fin t s1 /\
    match_states pge s0 s1.

Proof.

  Local Ltac intro_goal :=
    eexists; split; [econstructor; simpl; eauto|constructor; simpl; auto].
  apply preserv_fnstacksize in MF as SZ.
  assert (MATCH :
      let (p_H, s_H) := si_sfv_set (fun pc => history (fn_gm f1 pc)) fin in
      let (p_G, s_G) := si_sfv_set (fun pc => glue (fn_gm f1 pc)) fin in
      let (p_M, s_M) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
      p_H /\ p_G /\ p_M /\
      forall inv, s_H inv.(history) -> s_G inv.(glue) -> s_M inv.(meminv) ->
      match_invs ctx inv m0). {
    do 3 autodestruct; intros; unfold match_invs; intuition.
  }
  (* This lemma prove the equality of the memories where it is needed (for instance before a call). *)
  assert (MEM_EQ:
      let (_, s) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
      s nil -> m0 = cm1 ctx). {
    autodestruct; intros _ NIL.
    apply MATCH_M in NIL; injection NIL as ->; reflexivity.
  }
  clear MATCH_H MATCH_G MATCH_M.

  inversion FINAL; subst; simpl in *;
    try (case MEM_EQ; [reflexivity|]).
  - intro_goal.
    + apply MATCH; eauto.
  - intro_goal.
    + rewrite <- SZ. eassumption.
  - eapply find_function_v_preserved in H as (tf & FIND & TF).
    apply transf_fundef_correct in TF as TMF.
    intro_goal.
    + eapply function_sig_translated; eassumption.
    + do 2 (constructor; auto); intros.
      case MATCH as (? & ? & ? & INV).
      eapply clobbered_compat_matchinvs_preserv; eauto using test_clobberable_correct.
  - eapply find_function_v_preserved in H as (tf & FIND & TF).
    apply transf_fundef_correct in TF as TMF.
    intro_goal.
    + eapply function_sig_translated; eassumption.
    + rewrite <- SZ. eassumption.
  - intro_goal.
    + eapply eval_builtin_args_preserved.
      * apply senv_preserved.
      * eassumption.
    + eapply external_call_symbols_preserved; eauto.
      apply senv_preserved.
    + destruct (reg_builtin_res res) eqn:EQBR.
      * replace res with (BR r)
          by (destruct res eqn:HBR in EQBR; inv EQBR; auto).
        case MATCH as (? & ? & ? & INV).
        eapply clobbered_compat_matchinvs_preserv; eauto using test_clobberable_correct.
      * assert (NORES: forall rs, regmap_setres res vres rs = rs)
          by (revert EQBR; destruct res; try inversion 1; reflexivity).
        rewrite !NORES.
        case MATCH as (? & ? & ? & INV).
        eapply matchinvs_update_m; eauto using test_csifreem_correct.
  - intro_goal.
    + apply list_nth_z_in in H0 as PC.
      apply MATCH; eauto.
Qed.

End FINAL_STEP.

Theorem iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m m' bc ibf1 t csE pc
  (ISTEP: iblock_step AnnotUndef pge stk1 f1 sp rs m bc ibf1.(entry) t csE)
  (PC: (fn_code f1) ! pc = Some ibf1)
  (MF: match_function f1 f2)
  (MATCHI: match_invs (Bcctx pge sp rs rs' m' bc) (f2.(fn_gm) pc) m)
  (STACKS: list_forall2 (match_stackframes pge) stk1 stk2)
  :exists ibf2 ssIE',
    (fn_code f2) ! pc = Some ibf2
    /\ iblock_step AnnotUndef tpge stk2 f2 sp rs' m' bc ibf2.(entry) t ssIE'
    /\ match_states pge csE ssIE'.

Proof.

  pose (ctx:=Sctx pge tpge symbols_preserved_rev sp rs rs' m' bc).
  change ({| cge := pge |}) with (bcctx1 ctx) in MATCHI.
  eapply match_sexec_ok in MF as IB_MATCH; eauto. case IB_MATCH as (ibf2 & -> & IB_MATCH).
  exists ibf2.
  destruct ibf1 as [ib1 ?], ibf2 as [ib2 ?]; simpl in *.
  apply sis_source_correct in MATCHI as SIS_0.
  apply sis_target_correct in MATCHI as SIS_I.
    rewrite sem_sistate_preserved in SIS_I.
  specialize (IB_MATCH (bcctx1 ctx)); unfold match_sexec_si in IB_MATCH.
  case get_soutcome as [sis1E sfv1] eqn:OUT1 in IB_MATCH.
  case IB_MATCH as (HYP1 & MATCH).
  case ISTEP as (rsE & mE & fin1 & ISTEP1 & FIN1).
  (* symbolic execution of the source iblock *)
  eapply sexec_correct with (ctx := Bfctx f1 (bcctx1 ctx)) in SIS_0 as (SIS_1E & SFV1); simpl in *;
    try solve [reflexivity | eassumption].
  case get_soutcome as (sis2IE & sfv2) eqn:OUT2 in MATCH.
  set (sisE := set_smem _ sis1E) in MATCH.
  case MATCH as (HYP2 & OK2 & SFV_SIMU & MATCH_H & MATCH_G & MATCH_M).
    { eapply sem_sis_ok, SIS_1E. }
    rewrite get_soutcome_preserved in OUT2.
    rewrite okpred_preserved in HYP2.
    rewrite sis_ok_preserved in OK2.
  (* symbolic execution of the target iblock *)
  eapply sexec_exact with (ctx := Bfctx f2 (bcctx2 ctx)) in SIS_I as SIS_IE; eauto.
  case SIS_IE as (rsIE & mIE & fin2 & ISTEP2 & SIS_2IE & SFV2); simpl in *.
    eapply sem_sistate_preserved in SIS_2IE.
  assert (total_sreg sis2IE). {
    apply sexec_total_sreg in OUT2; auto.
    apply tr_sis_total.
  }
  (* state with the final regset of the source and the final memory of the target *)
  assert (SIS_E : sem_sistate (bcctx1 ctx) sisE rsE mIE). {
    split; [|split]; simpl.
    - eapply sem_sis_ok, SIS_1E.
    - apply SIS_2IE.
    - apply SIS_1E.
  }
  assert (total_sreg sisE). {
    apply sexec_total_sreg in OUT1; auto.
    apply tr_sis_total.
  }
  (* final step *)
  unfold sfv_equiv in SFV1, SFV2; simpl in SFV1, SFV2.
  case SFV1 as (fin_v & FIN_V & FIN1_IFF); apply FIN1_IFF in FIN1.
  apply ex_Some_iff in SFV2.
    apply sfv_simu_eval in SFV_SIMU.
    rewrite <- eval_final_sval_preserved, <- SFV_SIMU, FIN_V in SFV2; simpl in SFV2.
  unfold match_tr_si_sfv in MATCH_H, MATCH_G.
  erewrite -> si_sfv_set_map_final in MATCH_H, MATCH_G by exact FIN_V.
  erewrite -> meminv_sfv_set_map_final in MATCH_M by exact FIN_V.

  eapply final_step_simulation with (rs0 := rsE) (rs1 := rsIE) (m0 := mE) (m1 := mIE)
    in FIN1 as (s1 & FIN2 & MATCH); eauto;
  cycle 1. 1-3:autodestruct; intros _; split; [tauto|intros ? HP].
  - apply MATCH_H in HP.
    apply HP in SIS_E as SIS_H.
    eapply match_si_rstrg_preserv. apply siof_trg_free.
    eapply tr_sis_intro_match_si in SIS_H; eauto.
  - apply MATCH_G in HP.
    apply HP in SIS_2IE as SIS_G.
    eapply match_si_rstrg_preserv. apply siof_trg_free.
    eapply tr_sis_intro_match_si in SIS_G; eauto.
  - apply MATCH_M in HP; unfold match_meminv.
    case SIS_1E as (_ & <- & _).
    rewrite HP.
    erewrite sem_sis_sm_subst_trg by eauto.
    eapply smdep_preserv.
    intros [|] ? DEP. reflexivity. exfalso.
    eapply imem_subst_src_free; eauto.
  - apply SFV2 in FIN2; simpl in *.
    exists s1; split; [|split]; auto.
    exists rsIE, mIE, fin2; split; auto.
Qed.

Local Hint Constructors step: core.

Theorem step_simulation s1 s1' t s2
  (STEP: step AnnotUndef pge s1 t s1')
  (MS: match_states pge s1 s2)
  :exists s2',
    step AnnotUndef tpge s2 t s2'
  /\ match_states pge s1' s2'.

Proof.

  destruct STEP as [stack ibf f sp n rs m bc t s PC STEP | | | ]; inv MS.
  - (* iblock *)
    simplify_someHyps. intros PC.
    exploit iblock_step_simulation; eauto.
    intros (ibf' & s2 & PC2 & STEP2 & MS2).
    eexists; split; eauto.
  - (* function internal *)
    inversion TRANSF as [xf tf MF |]; subst.
    eexists; split.
    + econstructor.
      -- erewrite <- preserv_fnsig by eassumption. assumption.
      -- erewrite <- preserv_fnstacksize; eauto.
    + generalize (trivial_glueinv_entrypoint _ _ MF)
                 (trivial_histinv_entrypoint _ _ MF)
                 (trivial_meminv_entrypoint _ _ MF).
      erewrite preserv_fnparams; eauto.
      erewrite preserv_entrypoint; eauto.
      intros ONLYh ONLYg ONLYm.
      econstructor; eauto.
      eapply only_liveness_match_invs; eauto.
  - (* function external *)
    inv TRANSF. eexists; split; econstructor; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  - (* return *)
    inv STACKS. destruct b1 as [res' f' sp' pc' rs'].
    eexists; split.
    + econstructor.
    + inv H1. econstructor; eauto.
Qed.

Theorem transf_program_correct:
forward_simulation (sem AnnotUndef prog) (sem AnnotUndef tprog).

Proof.

  eapply forward_simulation_step with (match_states pge); simpl; eauto. (* lock-step with respect to match_states *)
  - eapply senv_preserved.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - intros; eapply step_simulation; eauto.
Qed.

End PRESERVATION.

Program Definition ipass : IPass (BTL.sem AnnotUndef) (BTL.sem AnnotUndef) :=
  {|
    ipass_spec := pass;
    ipass_impl := transf_program;
  |}.

Next Obligation.

apply transf_program_match; assumption. Qed.

Next Obligation.

apply transf_program_correct; assumption. Qed.

End BTL_BlockSimulationproof.

Module Type BTL_BlockSimulationCompConfig.
  Include BTL_BlockSimulationConfig.
  Parameter analyse : IPass (BTL.sem AnnotTrap) (BTL.sem AnnotTrap).
End BTL_BlockSimulationCompConfig.

Module BTL_BlockSimulationComp (B: BTL_BlockSimulationCompConfig).
  Export B.
  Module Simu := BTL_BlockSimulationproof B.

  Local Open Scope ipass_scope.

  Definition ipass : IPass (BTL.sem AnnotNone) (BTL.sem AnnotNone) :=
    BTL_ResetAnnots.ipass _ :::
    analyse :::
    ipass_simu Trap_to_Undef.transf_program :::
    Simu.ipass :::
    ipass_simu Undef_to_Lax.transf_program.

End BTL_BlockSimulationComp.