diff options
Diffstat (limited to 'arm/NeedOp.v')
| -rw-r--r-- | arm/NeedOp.v | 204 |
1 files changed, 204 insertions, 0 deletions
diff --git a/arm/NeedOp.v b/arm/NeedOp.v new file mode 100644 index 0000000..3fb0d72 --- /dev/null +++ b/arm/NeedOp.v @@ -0,0 +1,204 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Op. +Require Import NeedDomain. +Require Import RTL. + +(** Neededness analysis for ARM operators *) + +Definition needs_of_condition (cond: condition): list nval := nil. + +Definition needs_of_shift (s: shift) (nv: nval): nval := + match s with + | Slsl x => shlimm nv x + | Slsr x => shruimm nv x + | Sasr x => shrimm nv x + | Sror x => ror nv x + end. + +Definition op1 (nv: nval) := nv :: nil. +Definition op2 (nv: nval) := nv :: nv :: nil. +Definition op2shift (s: shift) (nv: nval) := nv :: needs_of_shift s nv :: nil. + +Definition needs_of_operation (op: operation) (nv: nval): list nval := + match op with + | Omove => nv::nil + | Ointconst n => nil + | Ofloatconst n => nil + | Oaddrsymbol id ofs => nil + | Oaddrstack ofs => nil + | Ocast8signed => op1 (sign_ext 8 nv) + | Ocast16signed => op1 (sign_ext 16 nv) + | Oadd => op2 (modarith nv) + | Oaddshift s => op2shift s (modarith nv) + | Oaddimm _ => op1 (modarith nv) + | Osub => op2 (default nv) + | Osubshift s => op2shift s (default nv) + | Orsubshift s => op2shift s (default nv) + | Orsubimm _ => op1 (default nv) + | Omul => op2 (modarith nv) + | Omla => let n := modarith nv in let n2 := modarith n in n2::n2::n::nil + | Omulhu | Omulhs | Odiv | Odivu => let n := default nv in n::n::nil + | Oand => op2 (bitwise nv) + | Oandshift s => op2shift s (bitwise nv) + | Oandimm n => op1 (andimm nv n) + | Oor => op2 (bitwise nv) + | Oorshift s => op2shift s (bitwise nv) + | Oorimm n => op1 (orimm nv n) + | Oxor => op2 (bitwise nv) + | Oxorshift s => op2shift s (bitwise nv) + | Oxorimm n => op1 (bitwise nv) + | Obic => let n := bitwise nv in n::bitwise n::nil + | Obicshift s => let n := bitwise nv in n::needs_of_shift s (bitwise n)::nil + | Onot => op1 (bitwise nv) + | Onotshift s => op1 (needs_of_shift s (bitwise nv)) + | Oshl | Oshr | Oshru => op2 (default nv) + | Oshift s => op1 (needs_of_shift s nv) + | Oshrximm _ => op1 (default nv) + | Onegf | Oabsf => op1 (default nv) + | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) + | Osingleoffloat => op1 (singleoffloat nv) + | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Omakelong => op2 (default nv) + | Olowlong | Ohighlong => op1 (default nv) + | Ocmp c => needs_of_condition c + end. + +Definition operation_is_redundant (op: operation) (nv: nval): bool := + match op with + | Ocast8signed => sign_ext_redundant 8 nv + | Ocast16signed => sign_ext_redundant 16 nv + | Oandimm n => andimm_redundant nv n + | Oorimm n => orimm_redundant nv n + | Osingleoffloat => singleoffloat_redundant nv + | _ => false + end. + +Ltac InvAgree := + match goal with + | [H: vagree_list nil _ _ |- _ ] => inv H; InvAgree + | [H: vagree_list (_::_) _ _ |- _ ] => inv H; InvAgree + | _ => idtac + end. + +Ltac TrivialExists := + match goal with + | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto + | _ => idtac + end. + +Section SOUNDNESS. + +Variable ge: genv. +Variable sp: block. +Variables m m': mem. +Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. + +Lemma needs_of_condition_sound: + forall cond args b args', + eval_condition cond args m = Some b -> + vagree_list args args' (needs_of_condition cond) -> + eval_condition cond args' m' = Some b. +Proof. + intros. unfold needs_of_condition in H0. + eapply default_needs_of_condition_sound; eauto. +Qed. + +Lemma needs_of_shift_sound: + forall v v' s nv, + vagree v v' (needs_of_shift s nv) -> + vagree (eval_shift s v) (eval_shift s v') nv. +Proof. + intros. destruct s; simpl in *. + apply shlimm_sound; auto. + apply shruimm_sound; auto. + apply shrimm_sound; auto. + apply ror_sound; auto. +Qed. + +Lemma val_sub_lessdef: + forall v1 v1' v2 v2', + Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.sub v1 v2) (Val.sub v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + +Lemma needs_of_operation_sound: + forall op args v nv args', + eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + vagree_list args args' (needs_of_operation op nv) -> + nv <> Nothing -> + exists v', + eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + /\ vagree v v' nv. +Proof. + unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); + simpl in *; FuncInv; InvAgree; TrivialExists. +- apply sign_ext_sound; auto. compute; auto. +- apply sign_ext_sound; auto. compute; auto. +- apply add_sound; auto. +- apply add_sound; auto. apply needs_of_shift_sound; auto. +- apply add_sound; auto with na. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. + apply lessdef_vagree. apply needs_of_shift_sound; auto with na. + destruct nv; simpl; congruence. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. + apply lessdef_vagree. apply needs_of_shift_sound; auto with na. + destruct nv; simpl; congruence. +- apply mul_sound; auto. +- apply add_sound; auto. apply mul_sound; auto. +- apply and_sound; auto. +- apply and_sound; auto. apply needs_of_shift_sound; auto. +- apply andimm_sound; auto. +- apply or_sound; auto. +- apply or_sound; auto. apply needs_of_shift_sound; auto. +- apply orimm_sound; auto. +- apply xor_sound; auto. +- apply xor_sound; auto. apply needs_of_shift_sound; auto. +- apply xor_sound; auto with na. +- apply and_sound; auto. apply notint_sound; auto. +- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. +- apply notint_sound; auto. +- apply notint_sound. apply needs_of_shift_sound; auto. +- apply needs_of_shift_sound; auto. +- apply singleoffloat_sound; auto. +Qed. + +Lemma operation_is_redundant_sound: + forall op nv arg1 args v arg1' args', + operation_is_redundant op nv = true -> + eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> + vagree v arg1' nv. +Proof. + intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. +- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. omega. +- apply andimm_redundant_sound; auto. +- apply orimm_redundant_sound; auto. +- apply singleoffloat_redundant_sound; auto. +Qed. + +End SOUNDNESS. + + + |