Library ConstpropOpproof

Correctness proof for constant propagation (processor-dependent part).





Require Import Coqlib.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Mem.

Require Import Globalenvs.

Require Import Op.

Require Import Registers.

Require Import RTL.

Require Import ConstpropOp.

Require Import Constprop.

Correctness of the static analysis





Section ANALYSIS.




Variable ge: genv.

We first show that the dataflow analysis is correct with respect to the dynamic semantics: the approximations (sets of values) of a register at a program point predicted by the static analysis are a superset of the values actually encountered during concrete executions. We formalize this correspondence between run-time values and compile-time approximations by the following predicate.





Definition val_match_approx (a: approx) (v: val) : Prop :=

  match a with

  | Unknown => True

  | I p => v = Vint p

  | F p => v = Vfloat p

  | S symb ofs => exists b, Genv.find_symbol ge symb = Some b /\ v = Vptr b ofs

  | _ => False

  end.




Inductive val_list_match_approx: list approx -> list val -> Prop :=

  | vlma_nil:

      val_list_match_approx nil nil

  | vlma_cons:

      forall a al v vl,

      val_match_approx a v ->

      val_list_match_approx al vl ->

      val_list_match_approx (a :: al) (v :: vl).




Ltac SimplVMA :=

  match goal with

  | H: (val_match_approx (I _) ?v) |- _ =>

      simpl in H; (try subst v); SimplVMA

  | H: (val_match_approx (F _) ?v) |- _ =>

      simpl in H; (try subst v); SimplVMA

  | H: (val_match_approx (S _ _) ?v) |- _ =>

      simpl in H; 

      (try (elim H;

            let b := fresh "b" in let A := fresh in let B := fresh in

            (intros b [A B]; subst v; clear H)));

      SimplVMA

  | _ =>

      idtac

  end.




Ltac InvVLMA :=

  match goal with

  | H: (val_list_match_approx nil ?vl) |- _ =>

      inversion H

  | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>

      inversion H; SimplVMA; InvVLMA

  | _ =>

      idtac

  end.

We then show that eval_static_operation is a correct abstract interpretations of eval_operation: if the concrete arguments match the given approximations, the concrete results match the approximations returned by eval_static_operation.





Lemma eval_static_condition_correct:

  forall cond al vl b,

  val_list_match_approx al vl ->

  eval_static_condition cond al = Some b ->

  eval_condition cond vl = Some b.






Lemma eval_static_operation_correct:

  forall op sp al vl v,

  val_list_match_approx al vl ->

  eval_operation ge sp op vl = Some v ->

  val_match_approx (eval_static_operation op al) v.

Correctness of strength reduction

We now show that strength reduction over operators and addressing modes preserve semantics: the strength-reduced operations and addressings evaluate to the same values as the original ones if the actual arguments match the static approximations used for strength reduction.





Section STRENGTH_REDUCTION.




Variable app: reg -> approx.

Variable sp: val.

Variable rs: regset.

Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.




Lemma intval_correct:

  forall r n,

  intval app r = Some n -> rs#r = Vint n.






Lemma cond_strength_reduction_correct:

  forall cond args,

  let (cond', args') := cond_strength_reduction app cond args in

  eval_condition cond' rs##args' = eval_condition cond rs##args.






Lemma make_addimm_correct:

  forall n r v,

  let (op, args) := make_addimm n r in

  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_shlimm_correct:

  forall n r v,

  let (op, args) := make_shlimm n r in

  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_shrimm_correct:

  forall n r v,

  let (op, args) := make_shrimm n r in

  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_shruimm_correct:

  forall n r v,

  let (op, args) := make_shruimm n r in

  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_mulimm_correct:

  forall n r v,

  let (op, args) := make_mulimm n r in

  eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_andimm_correct:

  forall n r v,

  let (op, args) := make_andimm n r in

  eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_orimm_correct:

  forall n r v,

  let (op, args) := make_orimm n r in

  eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma make_xorimm_correct:

  forall n r v,

  let (op, args) := make_xorimm n r in

  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->

  eval_operation ge sp op rs##args = Some v.






Lemma op_strength_reduction_correct:

  forall op args v,

  let (op', args') := op_strength_reduction app op args in

  eval_operation ge sp op rs##args = Some v ->

  eval_operation ge sp op' rs##args' = Some v.






Ltac KnownApprox :=

  match goal with

  | H: ?approx ?r = ?a |- _ =>

      generalize (MATCH r); rewrite H; intro; clear H; KnownApprox

  | _ => idtac

  end.




Lemma addr_strength_reduction_correct:

  forall addr args,

  let (addr', args') := addr_strength_reduction app addr args in

  eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.






End STRENGTH_REDUCTION.




End ANALYSIS.