aboutsummaryrefslogtreecommitdiffstats
path: root/verilog/NeedOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'verilog/NeedOp.v')
-rw-r--r--verilog/NeedOp.v259
1 files changed, 259 insertions, 0 deletions
diff --git a/verilog/NeedOp.v b/verilog/NeedOp.v
new file mode 100644
index 00000000..d9a58fbb
--- /dev/null
+++ b/verilog/NeedOp.v
@@ -0,0 +1,259 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris *)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(** Neededness analysis for x86_64 operators *)
+
+Require Import Coqlib.
+Require Import AST Integers Floats Values Memory Globalenvs.
+Require Import Op NeedDomain RTL.
+
+Definition op1 (nv: nval) := nv :: nil.
+Definition op2 (nv: nval) := nv :: nv :: nil.
+
+Definition needs_of_condition (cond: condition): list nval :=
+ match cond with
+ | Cmaskzero n | Cmasknotzero n => op1 (maskzero n)
+ | _ => nil
+ end.
+
+Definition needs_of_addressing_32 (addr: addressing) (nv: nval): list nval :=
+ match addr with
+ | Aindexed n => op1 (modarith nv)
+ | Aindexed2 n => op2 (modarith nv)
+ | Ascaled sc ofs => op1 (modarith (modarith nv))
+ | Aindexed2scaled sc ofs => op2 (modarith nv)
+ | Aglobal s ofs => nil
+ | Abased s ofs => op1 (modarith nv)
+ | Abasedscaled sc s ofs => op1 (modarith (modarith nv))
+ | Ainstack ofs => nil
+ end.
+
+Definition needs_of_addressing_64 (addr: addressing) (nv: nval): list nval :=
+ match addr with
+ | Aindexed n => op1 (default nv)
+ | Aindexed2 n => op2 (default nv)
+ | Ascaled sc ofs => op1 (default nv)
+ | Aindexed2scaled sc ofs => op2 (default nv)
+ | Aglobal s ofs => nil
+ | Abased s ofs => op1 (default nv)
+ | Abasedscaled sc s ofs => op1 (default nv)
+ | Ainstack ofs => nil
+ end.
+
+Definition needs_of_addressing (addr: addressing) (nv: nval): list nval :=
+ if Archi.ptr64 then needs_of_addressing_64 addr nv else needs_of_addressing_32 addr nv.
+
+Definition needs_of_operation (op: operation) (nv: nval): list nval :=
+ match op with
+ | Omove => op1 nv
+ | Ointconst n => nil
+ | Olongconst n => nil
+ | Ofloatconst n => nil
+ | Osingleconst n => nil
+ | Oindirectsymbol id => nil
+ | Ocast8signed => op1 (sign_ext 8 nv)
+ | Ocast8unsigned => op1 (zero_ext 8 nv)
+ | Ocast16signed => op1 (sign_ext 16 nv)
+ | Ocast16unsigned => op1 (zero_ext 16 nv)
+ | Oneg => op1 (modarith nv)
+ | Osub => op2 (default nv)
+ | Omul => op2 (modarith nv)
+ | Omulimm n => op1 (modarith nv)
+ | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
+ | Oand => op2 (bitwise nv)
+ | Oandimm n => op1 (andimm nv n)
+ | Oor => op2 (bitwise nv)
+ | Oorimm n => op1 (orimm nv n)
+ | Oxor => op2 (bitwise nv)
+ | Oxorimm n => op1 (bitwise nv)
+ | Onot => op1 (bitwise nv)
+ | Oshl => op2 (default nv)
+ | Oshlimm n => op1 (shlimm nv n)
+ | Oshr => op2 (default nv)
+ | Oshrimm n => op1 (shrimm nv n)
+ | Oshrximm n => op1 (default nv)
+ | Oshru => op2 (default nv)
+ | Oshruimm n => op1 (shruimm nv n)
+ | Ororimm n => op1 (ror nv n)
+ | Oshldimm n => op1 (default nv)
+ | Olea addr => needs_of_addressing_32 addr nv
+ | Omakelong => op2 (default nv)
+ | Olowlong | Ohighlong => op1 (default nv)
+ | Ocast32signed => op1 (default nv)
+ | Ocast32unsigned => op1 (default nv)
+ | Onegl => op1 (default nv)
+ | Oaddlimm _ => op1 (default nv)
+ | Osubl => op2 (default nv)
+ | Omull => op2 (default nv)
+ | Omullimm _ => op1 (default nv)
+ | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
+ | Oandl => op2 (default nv)
+ | Oandlimm _ => op1 (default nv)
+ | Oorl => op2 (default nv)
+ | Oorlimm _ => op1 (default nv)
+ | Oxorl => op2 (default nv)
+ | Oxorlimm _ => op1 (default nv)
+ | Onotl => op1 (default nv)
+ | Oshll => op2 (default nv)
+ | Oshllimm _ => op1 (default nv)
+ | Oshrl => op2 (default nv)
+ | Oshrlimm _ => op1 (default nv)
+ | Oshrxlimm n => op1 (default nv)
+ | Oshrlu => op2 (default nv)
+ | Oshrluimm _ => op1 (default nv)
+ | Ororlimm _ => op1 (default nv)
+ | Oleal addr => needs_of_addressing_64 addr nv
+ | Onegf | Oabsf => op1 (default nv)
+ | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+ | Onegfs | Oabsfs => op1 (default nv)
+ | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
+ | Osingleoffloat | Ofloatofsingle => op1 (default nv)
+ | Ointoffloat | Ofloatofint | Ointofsingle | Osingleofint => op1 (default nv)
+ | Olongoffloat | Ofloatoflong | Olongofsingle | Osingleoflong => op1 (default nv)
+ | Ocmp c => needs_of_condition c
+ | Osel c ty => nv :: nv :: needs_of_condition c
+ end.
+
+Definition operation_is_redundant (op: operation) (nv: nval): bool :=
+ match op with
+ | Ocast8signed => sign_ext_redundant 8 nv
+ | Ocast8unsigned => zero_ext_redundant 8 nv
+ | Ocast16signed => sign_ext_redundant 16 nv
+ | Ocast16unsigned => zero_ext_redundant 16 nv
+ | Oandimm n => andimm_redundant nv n
+ | Oorimm n => orimm_redundant nv n
+ | _ => 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. destruct cond; simpl in H;
+ try (eapply default_needs_of_condition_sound; eauto; fail);
+ simpl in *; FuncInv; InvAgree.
+- eapply maskzero_sound; eauto.
+- destruct (Val.maskzero_bool v n) as [b'|] eqn:MZ; try discriminate.
+ erewrite maskzero_sound; eauto.
+Qed.
+
+Lemma needs_of_addressing_32_sound:
+ forall sp addr args v nv args',
+ eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args = Some v ->
+ vagree_list args args' (needs_of_addressing_32 addr nv) ->
+ exists v',
+ eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args' = Some v'
+ /\ vagree v v' nv.
+Proof.
+ unfold needs_of_addressing_32; intros.
+ destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists;
+ auto using add_sound, mul_sound with na.
+ apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto.
+ apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na.
+ apply mul_sound; rewrite modarith_idem; auto with na.
+Qed.
+
+(*
+Lemma needs_of_addressing_64_sound:
+ forall sp addr args v nv args',
+ eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args = Some v ->
+ vagree_list args args' (needs_of_addressing_64 addr nv) ->
+ exists v',
+ eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args' = Some v'
+ /\ vagree v v' nv.
+*)
+
+Lemma needs_of_operation_sound:
+ forall op args v nv args',
+ eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v ->
+ vagree_list args args' (needs_of_operation op nv) ->
+ nv <> Nothing ->
+ exists v',
+ eval_operation ge (Vptr sp Ptrofs.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 zero_ext_sound; auto. omega.
+- apply sign_ext_sound; auto. compute; auto.
+- apply zero_ext_sound; auto. omega.
+- apply neg_sound; auto.
+- apply mul_sound; auto.
+- apply mul_sound; auto with na.
+- apply and_sound; auto.
+- apply andimm_sound; auto.
+- apply or_sound; auto.
+- apply orimm_sound; auto.
+- apply xor_sound; auto.
+- apply xor_sound; auto with na.
+- apply notint_sound; auto.
+- apply shlimm_sound; auto.
+- apply shrimm_sound; auto.
+- apply shruimm_sound; auto.
+- apply ror_sound; auto.
+- eapply needs_of_addressing_32_sound; eauto.
+- change (eval_addressing64 ge (Vptr sp Ptrofs.zero) a args')
+ with (eval_operation ge (Vptr sp Ptrofs.zero) (Oleal a) args' m').
+ eapply default_needs_of_operation_sound; eauto.
+ destruct a; simpl in H0; auto.
+- destruct (eval_condition cond args m) as [b|] eqn:EC; simpl in H2.
+ erewrite needs_of_condition_sound by eauto.
+ subst v; simpl. auto with na.
+ subst v; auto with na.
+- destruct (eval_condition c args m) as [b|] eqn:EC.
+ erewrite needs_of_condition_sound by eauto.
+ apply select_sound; auto.
+ simpl; auto with na.
+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 Ptrofs.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 zero_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. omega.
+- apply zero_ext_redundant_sound; auto. omega.
+- apply andimm_redundant_sound; auto.
+- apply orimm_redundant_sound; auto.
+Qed.
+
+End SOUNDNESS.
+
+
generated by cgit (git 2.34.1) at 2024-05-09 15:04:46 +0000