Library Constpropproof

Correctness proof for constant propagation.





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Events.

Require Import Mem.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Op.

Require Import Registers.

Require Import RTL.

Require Import Lattice.

Require Import Kildall.

Require Import ConstpropOp.

Require Import Constprop.

Require Import ConstpropOpproof.

Correctness of the static analysis





Section ANALYSIS.




Variable ge: genv.




Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=

  forall r, val_match_approx ge (D.get r a) rs#r.




Lemma regs_match_approx_top:

  forall rs, regs_match_approx D.top rs.






Lemma val_match_approx_increasing:

  forall a1 a2 v,

  Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v.






Lemma regs_match_approx_increasing:

  forall a1 a2 rs,

  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.






Lemma regs_match_approx_update:

  forall ra rs a v r,

  val_match_approx ge a v ->

  regs_match_approx ra rs ->

  regs_match_approx (D.set r a ra) (rs#r <- v).






Lemma approx_regs_val_list:

  forall ra rs rl,

  regs_match_approx ra rs ->

  val_list_match_approx ge (approx_regs ra rl) rs##rl.

The correctness of the static analysis follows from the results of module ConstpropOpproof and the fact that the result of the static analysis is a solution of the forward dataflow inequations.





Lemma analyze_correct_1:

  forall f pc rs pc' i,

  f.(fn_code)!pc = Some i ->

  In pc' (successors_instr i) ->

  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->

  regs_match_approx (analyze f)!!pc' rs.






Lemma analyze_correct_3:

  forall f rs,

  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.






End ANALYSIS.

Correctness of the code transformation

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





Section PRESERVATION.




Variable prog: program.

Let tprog := transf_program prog.

Let ge := Genv.globalenv prog.

Let tge := Genv.globalenv tprog.




Lemma symbols_preserved:

  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.






Lemma functions_translated:

  forall (v: val) (f: fundef),

  Genv.find_funct ge v = Some f ->

  Genv.find_funct tge v = Some (transf_fundef f).






Lemma function_ptr_translated:

  forall (b: block) (f: fundef),

  Genv.find_funct_ptr ge b = Some f ->

  Genv.find_funct_ptr tge b = Some (transf_fundef f).






Lemma sig_function_translated:

  forall f,

  funsig (transf_fundef f) = funsig f.






Lemma transf_ros_correct:

  forall ros rs f approx,

  regs_match_approx ge approx rs ->

  find_function ge ros rs = Some f ->

  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).

The proof of semantic preservation is a simulation argument based on diagrams of the following form:

           st1 --------------- st2
            |                   |
           t|                   |t
            |                   |
            v                   v
           st1'--------------- st2'

The left vertical arrow represents a transition in the original RTL code. The top horizontal bar is the match_states invariant between the initial state st1 in the original RTL code and an initial state st2 in the transformed code. This invariant expresses that all code fragments appearing in st2 are obtained by transf_code transformation of the corresponding fragments in st1. Moreover, the values of registers in st1 must match their compile-time approximations at the current program point. These two parts of the diagram are the hypotheses. In conclusions, we want to prove the other two parts: the right vertical arrow, which is a transition in the transformed RTL code, and the bottom horizontal bar, which means that the match_state predicate holds between the final states st1' and st2'.





Inductive match_stackframes: stackframe -> stackframe -> Prop :=

   match_stackframe_intro:

      forall res c sp pc rs f,

      c = f.(RTL.fn_code) ->

      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->

    match_stackframes

        (Stackframe res c sp pc rs)

        (Stackframe res (transf_code (analyze f) c) sp pc rs).




Inductive match_states: state -> state -> Prop :=

  | match_states_intro:

      forall s c sp pc rs m f s'

           (CF: c = f.(RTL.fn_code))

           (MATCH: regs_match_approx ge (analyze f)!!pc rs)

           (STACKS: list_forall2 match_stackframes s s'),

      match_states (State s c sp pc rs m)

                   (State s' (transf_code (analyze f) c) sp pc rs m)

  | match_states_call:

      forall s f args m s',

      list_forall2 match_stackframes s s' ->

      match_states (Callstate s f args m)

                   (Callstate s' (transf_fundef f) args m)

  | match_states_return:

      forall s s' v m,

      list_forall2 match_stackframes s s' ->

      match_states (Returnstate s v m)

                   (Returnstate s' v m).




Ltac TransfInstr :=

  match goal with

  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>

      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));

      [ simpl
      | unfold transf_code; rewrite PTree.gmap; 
        unfold option_map; rewrite H1; reflexivity ]

  end.

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





Lemma transf_step_correct:

  forall s1 t s2,

  step ge s1 t s2 ->

  forall s1' (MS: match_states s1 s1'),

  exists s2', step tge s1' t s2' /\ match_states s2 s2'.






Lemma transf_initial_states:

  forall st1, initial_state prog st1 ->

  exists st2, initial_state tprog st2 /\ match_states st1 st2.






Lemma transf_final_states:

  forall st1 st2 r, 

  match_states st1 st2 -> final_state st1 r -> final_state st2 r.

The preservation of the observable behavior of the program then follows, using the generic preservation theorem Smallstep.simulation_step_preservation.





Theorem transf_program_correct:

  forall (beh: program_behavior), not_wrong beh ->

  exec_program prog beh -> exec_program tprog beh.






End PRESERVATION.