Module Intervalpropproof



Correctness proof for interval propagation.

Require Import Coqlib Maps Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Values Builtins Events Memory Globalenvs Smallstep.
Require Compopts Machregs.
Require Import Op Registers RTL.
Require Import Liveness ZIntervalDomain ZIntervalAOp RTL_ZIntervalAnalysis.
Require Import IntervalpropOp IntervalpropOpproof Intervalprop.

Definition match_prog (prog tprog: program) :=
  match_program (fun cu f tf => tf = transf_fundef f) eq prog tprog.

Lemma transf_program_match:
  forall prog, match_prog prog (transf_program prog).
Proof.
  intros. apply match_transform_program.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Correctness of the code transformation


We now show that the transformed code after constant propagation has the same semantics as the original code.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).

Lemma sig_preserved:
  forall f, funsig (transf_fundef f) = funsig f.
Proof.
  destruct f; trivial.
Qed.

Lemma find_function_translated:
  forall ros rs fd,
  find_function ge ros rs = Some fd ->
  find_function tge ros rs = Some (transf_fundef fd).
Proof.
  unfold find_function; intros. destruct ros as [r|id].
  eapply functions_translated; eauto.
  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
  eapply function_ptr_translated; eauto.
Qed.

Lemma init_regs_lessdef:
  forall rl vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl).
Proof.
  induction rl; simpl; intros.
  red; intros. rewrite Regmap.gi. auto.
  inv H. red; intros. rewrite Regmap.gi. auto.
  apply set_reg_lessdef; auto.
Qed.

Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   match_stackframe_intro:
    forall res sp pc rs f rs'
      (REGS : regs_lessdef rs rs'),
    match_stackframes
        (Stackframe res f (Vptr sp Ptrofs.zero) pc rs)
        (Stackframe res (transf_function f) (Vptr sp Ptrofs.zero) pc rs').

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
    forall s sp pc rs m f s' rs' m'
           (STACKS: list_forall2 match_stackframes s s')
           (REGS: regs_lessdef rs rs')
           (MEM: Mem.extends m m'),
      match_states (State s f (Vptr sp Ptrofs.zero) pc rs m)
                   (State s' (transf_function f) (Vptr sp Ptrofs.zero) pc rs' m')
  | match_states_call:
      forall s f args m s' args' m'
           (STACKS: list_forall2 match_stackframes s s')
           (ARGS: Val.lessdef_list args args')
           (MEM: Mem.extends m m'),
      match_states (Callstate s f args m)
                   (Callstate s' (transf_fundef f) args' m')
  | match_states_return:
      forall s v m s' v' m'
           (STACKS: list_forall2 match_stackframes s s')
           (RES: Val.lessdef v v')
           (MEM: Mem.extends m m'),
      match_states (Returnstate s v m)
                   (Returnstate s' v' m').

Lemma transf_instr_at:
  forall f pc i,
  f.(fn_code)!pc = Some i ->
  (transf_function f).(fn_code)!pc = Some(transf_instr f (AA.analyze tt f) pc i).
Proof.
  intros. simpl. rewrite PTree.gmap. rewrite H. auto.
Qed.

Ltac TransfInstr :=
  match goal with
  | H1: (PTree.get ?pc (fn_code ?f) = Some ?instr),
      H2: (AA.analyze ?pinfo ?f)#?pc = AA.Astate ?aa |- _ => unfold transf_function; cbn; unfold transf_instr; rewrite PTree.gmap; unfold option_map; rewrite H1; change (option aenv) with AA.VA.t; change (AA.get_prog_info prog) with tt in H2; rewrite H2; try reflexivity
  end.

Ltac TransfAnalyze :=
  match goal with
  | H1: (PTree.get ?pc (fn_code ?f) = Some ?instr),
      H2: (AA.analyze ?pinfo ?f)#?pc = AA.Astate ?ae |- _ =>
      exploit AA.analyze_succ; [exact H2 | cbn; rewrite H1; cbn; reflexivity | cbn; auto | idtac | intros (ae' & ANALYZE' & EMATCH')]
  end.

The proof of simulation proceeds by case analysis on the transition taken in the source code.

Definition match_states_full S1 S1' :=
  AA.sound_state prog S1 /\ match_states S1 S1'.

Opaque op_strength_reduction.

Lemma find_function_same:
  forall ros rs rs' fd
    (LESS_REGS : regs_lessdef rs rs')
    (FIND : find_function ge ros rs = Some fd),
    find_function ge ros rs' = Some fd.
Proof.
  intros. destruct ros; cbn in *.
  - pose proof (LESS_REGS r) as LESS.
    inv LESS.
    + assumption.
    + rewrite <- H0 in FIND. cbn in FIND. discriminate.
  - assumption.
Qed.

                                        
Lemma step_simulation0:
  forall S1 t S2, RTL.step ge S1 t S2 ->
  forall S1', AA.sound_state prog S1 -> match_states S1 S1' ->
              exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
Proof.
  induction 1; intros S1' SOUND MS; inv MS.
  all: inv SOUND; destruct (SOUND0 prog (linkorder_refl prog)) as (gh & SOUND); inv SOUND.
  - (* Inop *)
    exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' m').
    split.
    + apply exec_Inop. TransfInstr.
    + TransfAnalyze. eassumption. econstructor; eauto.

  - (* Iop *)
    rename H0 into EVAL.
    exploit (eval_static_operation_sound ge); try eassumption.
    { apply ZIntervalAnalysis.aregs_sound. eassumption. }
    intro VMATCH.
    pose proof (transf_instr_at _ _ _ H) as TRANS.
    unfold transf_instr in TRANS.
    change (AA.get_prog_info prog) with tt in AN.
    change (option aenv) with AA.VA.t in TRANS.
    rewrite AN in TRANS.
    Local Opaque transf_function.
    cbn in TRANS.
    Local Transparent transf_function.
    destruct (const_for_result _) as [op' | ] eqn:CONST.
    + destruct (const_for_result_correct ge sp0 m _ _ _ CONST VMATCH) as (v' & EVAL' & LESSDEF).
      exploit eval_operation_lessdef.
      { apply Val.lessdef_list_nil. }
      eassumption.
      exact EVAL'.
      intros (v'' & EVAL'' & LESSDEF').
      pose proof (Val.lessdef_trans _ _ _ LESSDEF LESSDEF') as ADDR_LESSDEF''.
      clear LESSDEF LESSDEF'.
      exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' # res <- v'' m').
      split.
      * apply exec_Iop with (op:=op') (args:=nil); try eassumption.
        rewrite eval_operation_preserved with (ge1:=ge) by apply symbols_preserved.
        exact EVAL''.
      * constructor; try eassumption.
        apply set_reg_lessdef; eassumption.
    + exploit (op_strength_reduction_correct ge sp0 aa); eauto.
      intro STRENGTH_RED.
      destruct (op_strength_reduction op args _) as (op' & args') eqn:RED.
      destruct STRENGTH_RED as (v' & EVAL' & LESSDEF).
      exploit eval_operation_lessdef.
      { apply regs_lessdef_regs. eassumption. }
      eassumption.
      exact EVAL'.
      intros (v'' & EVAL'' & LESSDEF').
      TransfAnalyze.
      { left. reflexivity. }
      { apply ematch_update; eassumption. }
      exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' # res <- v'' m').
      split.
      * apply exec_Iop with (op:=op') (args:=args').
        assumption.
        rewrite eval_operation_preserved with (ge1:=ge) by apply symbols_preserved.
        eassumption.
      * constructor; try eassumption.
        apply set_reg_lessdef. 2: eassumption.
        eapply Val.lessdef_trans; eassumption.

  - (* Iload *)
    rename H0 into LOADED.
    inv LOADED.
    + exploit (addr_strength_reduction_correct ge sp0 aa); eauto.
      intro STRENGTH_RED.
      destruct (addr_strength_reduction addr args _) as (addr' & args') eqn:RED.
      destruct STRENGTH_RED as (v' & ADDR' & LESSDEF).
      exploit eval_addressing_lessdef.
      { apply regs_lessdef_regs. eassumption. }
      exact ADDR'.
      intros (a'' & ADDR'' & LESSDEF').
      pose proof (Val.lessdef_trans _ _ _ LESSDEF LESSDEF') as ADDR_LESSDEF''.
      clear LESSDEF LESSDEF'.
      exploit Mem.loadv_extends; try eassumption.
      intros (v'' & LOAD'' & LESSDEF'').
      eexists. split.
      * apply exec_Iload with (trap:=trap) (chunk:=chunk) (addr:=addr') (args:=args').
        TransfInstr. cbn.
        change (ZIntervalAnalysis.aregs aa args) with (map (fun r : positive => AE.get r aa) args).
        rewrite RED. reflexivity.
        eapply has_loaded_normal.
        rewrite eval_addressing_preserved with (ge1:=ge) by apply symbols_preserved.
        eassumption. eassumption.
      * constructor; try eassumption.
        apply set_reg_lessdef; auto.
    + destruct (eval_addressing ge (Vptr sp0 Ptrofs.zero) addr rs ## args) as [a | ] eqn:ADDR.
      * exploit (addr_strength_reduction_correct ge sp0 aa); eauto.
        intro STRENGTH_RED.
        destruct (addr_strength_reduction addr args _) as (addr' & args') eqn:RED.
        destruct STRENGTH_RED as (v' & ADDR' & LESSDEF).
        exploit eval_addressing_lessdef.
        { apply regs_lessdef_regs. eassumption. }
        exact ADDR'.
        intros (a'' & ADDR'' & LESSDEF').
        pose proof (Val.lessdef_trans _ _ _ LESSDEF LESSDEF') as ADDR_LESSDEF''.
        clear LESSDEF LESSDEF'.
        destruct (Mem.loadv chunk m' a'') as [v'' | ] eqn:LOAD''.
        -- eexists. split.
           ++ apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr') (args:=args').
              TransfInstr. cbn.
              change (ZIntervalAnalysis.aregs aa args) with (map (fun r : positive => AE.get r aa) args).
              rewrite RED. reflexivity.
              eapply has_loaded_normal.
              rewrite eval_addressing_preserved with (ge1:=ge) by apply symbols_preserved.
              eassumption. eassumption.
           ++ constructor; try eassumption.
              apply set_reg_lessdef; auto.
        -- eexists. split.
           ++ apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr') (args:=args').
              TransfInstr. cbn.
              change (ZIntervalAnalysis.aregs aa args) with (map (fun r : positive => AE.get r aa) args).
              rewrite RED. reflexivity.
              apply has_loaded_default. 2: reflexivity.
              intros a''0 ADDR''0.
              rewrite eval_addressing_preserved with (ge1:=ge) in ADDR''0 by apply symbols_preserved.
              congruence.
           ++ constructor; try eassumption.
              apply set_reg_lessdef; auto.
      * exploit eval_addressing_lessdef_none; try eassumption.
        { apply regs_lessdef_regs. eassumption. }
        intro ADDR_NONE.
        destruct (addr_strength_reduction addr args (ZIntervalAnalysis.aregs aa args)) as (addr' & args') eqn:RED.
        destruct (eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs' ## args') as [a' | ] eqn:ADDR'.
        -- destruct (Mem.loadv chunk m' a') as [v' | ] eqn:LOAD'.
           ++ eexists. split.
              ** apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr') (args:=args').
                 TransfInstr. cbn. rewrite RED. reflexivity.
                 apply has_loaded_normal with (a:=a').
                 { rewrite eval_addressing_preserved with (ge1:=ge) by apply symbols_preserved.
                   assumption. }
                 exact LOAD'.
              ** constructor; try eassumption.
                 apply set_reg_lessdef; auto.
           ++ eexists. split.
              ** apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr') (args:=args').
                 TransfInstr. cbn. rewrite RED. reflexivity.
                 apply has_loaded_default. 2: reflexivity.
                 intros a'0 ADDR'0.
                 rewrite eval_addressing_preserved with (ge1:=ge) in ADDR'0 by apply symbols_preserved.
                 congruence.
               ** constructor; try eassumption.
                  apply set_reg_lessdef; auto.
        -- eexists. split.
           ** apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr') (args:=args').
              TransfInstr. cbn. rewrite RED. reflexivity.
              apply has_loaded_default. 2: reflexivity.
              intros a'0 ADDR'0.
              rewrite eval_addressing_preserved with (ge1:=ge) in ADDR'0 by apply symbols_preserved.
              exfalso. congruence.
           ** constructor; try eassumption.
              apply set_reg_lessdef; auto.
              
  - (* Istore *)
    rename H0 into ADDR.
    rename H1 into STORE.
    exploit (addr_strength_reduction_correct ge sp0 aa); eauto.
    intro STRENGTH_RED.
    destruct (addr_strength_reduction addr args _) as (addr' & args') eqn:RED.
        destruct STRENGTH_RED as (v' & ADDR' & LESSDEF).
    exploit eval_addressing_lessdef.
    { apply regs_lessdef_regs. eassumption. }
    exact ADDR'.
    intros (a'' & ADDR'' & LESSDEF').
    pose proof (Val.lessdef_trans _ _ _ LESSDEF LESSDEF') as LESSDEF''.
    clear LESSDEF LESSDEF'.
    exploit Mem.storev_extends; try eassumption.
    { exact (REGS src). }
    intros (m2' & STORE' & EXTENDS').
    eexists. split.
    + apply exec_Istore with (chunk:=chunk) (addr:=addr') (args:=args') (src:=src) (a:=a'').
      * TransfInstr. cbn.
        change (ZIntervalAnalysis.aregs aa args) with (map (fun r : positive => AE.get r aa) args).
        rewrite RED.
        reflexivity.
      * rewrite eval_addressing_preserved with (ge1:=ge) by apply symbols_preserved.
        assumption.
      * eassumption.
    + constructor; assumption.

  - (* Icall *)
    eexists. split.
    + apply exec_Icall with (sig:=(funsig fd)) (ros:=ros).
      TransfInstr.
      * apply find_function_translated; try eassumption.
        apply find_function_same with (rs:=rs); eassumption.
      * apply sig_preserved.
    + constructor; try eassumption.
      * constructor; try eassumption.
        constructor; try eassumption.
      * auto using regs_lessdef_regs.

  - (* Itailcall *)
    exploit Mem.free_parallel_extends; try eassumption.
    intros (m2' & FREE' & EXTENDS').
    eexists. split.
    + apply exec_Itailcall with (sig:=(funsig fd)) (ros:=ros).
      TransfInstr.
      * apply find_function_translated; try eassumption.
        apply find_function_same with (rs:=rs); eassumption.
      * apply sig_preserved.
      * eassumption.
    + constructor; try eassumption.
      auto using regs_lessdef_regs.

  - (* Ibuiltin *)
    exploit eval_builtin_args_lessdef; try eassumption.
    exact REGS.
    intros (vargs' & EVAL' & LESSDEF_ARGS).
    exploit external_call_mem_extends; try eassumption.
    intros (vres' & m2' & EXTCALL' & LESSDEF_RES & EXTENDS' & UNCHANGED).
    exploit AA.transfer_builtin_correct; try eassumption.
    eexists. split.
    + apply exec_Ibuiltin with (ef:=ef) (args:=args) (vargs:=vargs').
      TransfInstr.
      apply eval_builtin_args_preserved with (ge1:=ge); try eassumption.
      { apply symbols_preserved. }
      apply external_call_symbols_preserved with (ge1:=ge).
      { apply senv_preserved. }
      eassumption.
    + constructor; try eassumption.
      auto using set_res_lessdef.
      
  - (* Icond *)
    rename H0 into COND.
    pose proof (transf_instr_at _ _ _ H) as TRANS.
    unfold transf_instr in TRANS.
    change (AA.get_prog_info prog) with tt in AN.
    change (option aenv) with AA.VA.t in TRANS.
    rewrite AN in TRANS.
    Local Opaque transf_function.
    cbn in TRANS.
    Local Transparent transf_function.
    exploit (eval_static_condition_sound cond rs ## args m (ZIntervalAnalysis.aregs aa args)).
    { apply ZIntervalAnalysis.aregs_sound; assumption. }
    intro STATIC.
    destruct ibool_cases_of.
    + inv STATIC.
      eexists. split.
      * apply exec_Inop. eassumption.
      * replace b with true by congruence.
        constructor; assumption.
    + inv STATIC.
      eexists. split.
      * apply exec_Inop. eassumption.
      * replace b with false by congruence.
        constructor; assumption.
    + exploit (cond_strength_reduction_correct aa rs m); eauto.
      intro COND'.
      destruct (cond_strength_reduction cond args _) as (cond' & args') eqn:RED.
      exploit eval_condition_lessdef.
      { apply regs_lessdef_regs. eassumption. }
      eassumption.
      exact COND'.
      intro COND''.
      exploit AA.transfer_condition_correct.
      { eauto; fail. }
      exact COND.
      intros (aa' & TRANSFER & MATCH').
      change (AA.get_prog_info prog) with tt in TRANSFER.
      assert (In (if b then ifso else ifnot, AA.Astate aa')
         (AA.transfer_instr tt (Icond cond args ifso ifnot predb) aa)) as IN.
      { cbn. destruct AA.transfer_condition. rewrite <- TRANSFER.
        destruct b; intuition. }
      destruct (AA.analyze_succ AN H (n':=if b then ifso else ifnot) IN MATCH') as (aa'' & AN'' & MATCH'').
      exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m').
      split.
      * apply exec_Icond with (cond:=cond') (args:=args') (ifso:=ifso) (ifnot:=ifnot) (b:=b) (predb:=predb); try assumption. reflexivity.
      * constructor; assumption.
  - (* Ijumptable *)
    eexists. split.
    + apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n).
      TransfInstr.
      * pose proof (REGS arg) as LESS.
        rewrite H0 in LESS. inv LESS. reflexivity.
      * eassumption.
    + constructor; eassumption.
  - (* Ireturn *)
    exploit Mem.free_parallel_extends; try eassumption.
    intros (m2' & FREE' & EXTENDS').
    eexists. split.
    + apply exec_Ireturn. TransfInstr. eassumption.
    + constructor; try eassumption.
      destruct or; cbn; auto.
  - (* internal call *)
    assert (0 <= 0) as LO by lia.
    assert (fn_stacksize f <= fn_stacksize f) as HI by lia.
    exploit Mem.alloc_extends; try eassumption.
    intros (m2' & ALLOC' & EXTENDS').
    eexists. split.
    + apply exec_function_internal. eassumption.
    + constructor; eauto using init_regs_lessdef.
  - (* external call *)
    exploit external_call_mem_extends; try eassumption.
    intros (vres' & m2' & EXTCALL & LESSDEF & EXTENDS & UNCHANGED).
    eexists. split.
    + apply exec_function_external.
      apply external_call_symbols_preserved with (ge1:=ge).
      { apply senv_preserved. }
      eassumption.
    + constructor; eassumption.
  - (* return *)
    inv STACKS. inv H1.
    eexists. split.
    + apply exec_return.
    + econstructor; try eassumption.
      apply set_reg_lessdef; assumption.
Unshelve.
      exact ge. exact gh. exact sp0. exact m. exact res.
Qed.

Lemma step_simulation:
  forall S1 t S2, RTL.step ge S1 t S2 ->
  forall S1', match_states_full S1 S1' ->
              exists S2', RTL.step tge S1' t S2' /\ match_states_full S2 S2'.
Proof.
  unfold match_states_full; intros until S1'.
  intros (SOUND & MATCH).
  exploit AA.sound_step; try eassumption.
  intro SOUND'.
  exploit step_simulation0; try eassumption.
  intros (S2' & STEP & MATCH').
  exists S2'. auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states_full st1 st2.
Proof.
  intros. inversion H.
  exploit function_ptr_translated; eauto. intro FIND.
  exists (Callstate nil (transf_fundef f) nil m0); split.
  econstructor; eauto.
  - apply (Genv.init_mem_match TRANSL); auto.
  - replace (prog_main tprog) with (prog_main prog).
    + rewrite symbols_preserved. eauto.
    + symmetry. eapply match_program_main. eassumption.
  - rewrite <- H3. apply sig_preserved.
  - split.
    + apply AA.sound_initial.
      econstructor; eassumption.
    + constructor. auto. constructor. constructor. apply Mem.extends_refl.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states_full st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
  intros until r. intros (SOUND & MATCH). intro FINAL.
  inv FINAL. inv MATCH. inv RES. inv STACKS. constructor.
Qed.

The preservation of the observable behavior of the program then follows.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_step.
  - apply senv_preserved.
  - eexact transf_initial_states.
  - eexact transf_final_states.
  - intros. eapply step_simulation; eauto.
Qed.

End PRESERVATION.
Generated by coq2html