Module NeedOp


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 op3 (nv: nval) := nv :: nv :: nv :: nil.
Definition op4 (nv: nval) := nv :: nv :: nv :: nv :: nil.
Definition op2shift (s: shift) (nv: nval) := nv :: needs_of_shift s nv :: nil.

Definition clearf lsb sz post :=
  if ExtValues.is_bitfield lsb sz
  then andimm post (Int.not (ExtValues.bitfield_mask lsb sz))
  else Nothing.

Lemma clearf_sound:
  forall lsb sz v w post,
  vagree v w (clearf lsb sz post) ->
  vagree (ExtValues.clearf lsb sz v) (ExtValues.clearf lsb sz w) post.
Proof.
  intros. unfold ExtValues.clearf, clearf in *.
  destruct (ExtValues.is_bitfield lsb sz); cycle 1.
  { apply vagree_same. }
  apply andimm_sound. assumption.
Qed.

Definition insf1 lsb sz post :=
  if ExtValues.is_bitfield lsb sz
  then andimm (bitwise post) (Int.not (ExtValues.bitfield_mask lsb sz))
  else Nothing.

Definition insf2 lsb sz post :=
  if ExtValues.is_bitfield lsb sz
  then shlimm (andimm (bitwise post) (ExtValues.bitfield_mask lsb sz)) lsb
  else Nothing.

Lemma insf_sound:
  forall lsb sz v1 w1 v2 w2 post,
  vagree v1 w1 (insf1 lsb sz post) ->
  vagree v2 w2 (insf2 lsb sz post) ->
  vagree (ExtValues.insf lsb sz v1 v2) (ExtValues.insf lsb sz w1 w2) post.
Proof.
  unfold insf1, insf2, ExtValues.insf. intros.
  destruct (ExtValues.is_bitfield lsb sz); cycle 1.
  { apply vagree_same. }
  apply or_sound.
  - apply andimm_sound. assumption.
  - apply andimm_sound. apply shlimm_sound. assumption.
Qed.

Definition needs_of_operation (op: operation) (nv: nval): list nval :=
  match op with
  | Omove => nv::nil
  | Ocopy => op2 (default nv)
  | Ocopyimm _ => op1 (default nv)
  | Ointconst n => nil
  | Ofloatconst n => nil
  | Osingleconst 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
  | Omls => op3 (default nv)
  | 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 | Oror => op2 (default nv)
  | Oshift s => op1 (needs_of_shift s nv)
  | Oshrximm _ => op1 (default nv)
  | Onegf | Oabsf | Osqrtf => op1 (default nv)
  | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
  | Omlaf | Omlsf => op3 (default nv)
  | Onegfs | Oabsfs | Osqrtfs => op1 (default nv)
  | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
  | Omlafs | Omlsfs => op3 (default nv)
  | Ofloatofsingle | Osingleoffloat => op1 (default nv)
  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
  | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
  | Omakelong => makelong_hi nv :: makelong_lo nv :: nil
  | Olowlong => op1 (loword nv)
  | Ohighlong => op1 (hiword nv)
  | Ocmp c => needs_of_condition c
  | Osel c => nv :: nv :: needs_of_condition c
  | Oselimm c _ => nv :: needs_of_condition c
  | Oselimm2 c _ _ => needs_of_condition c
  | Oclz => op1 (default nv)
  | Oreverse_bits => op1 (default nv)
  | Obswap32 => op1 (default nv)
  | Obits_of_single => op1 (default nv)
  | Osingle_of_bits => op1 (default nv)
  | Ohibits_of_float => op1 (default nv)
  | Osbfx _ _ | Oubfx _ _ => op1 (default nv)
  | Obfc lsb sz => op1 (clearf lsb sz nv)
  | Obfi lsb sz => (insf1 lsb sz nv)::(insf2 lsb sz nv)::nil
  | Oaddimm_reg _ => op1 (modarith nv)
  | Ogetcanary => nil
  | OEaddimm _ => nil
  | OEsubimm _ => nil
  | OErsbimm _ => nil
  | OEandimm _ => nil
  | OEbicimm _ => nil
  | OEorrimm _ => nil
  | OEeorimm _ => nil
  | OEmovimm _ => nil
  | OEmvnimm _ => nil
  | Ocmpcarryu _ => op4 (default nv)
  | Ocmpcarry _ => op4 (default nv)
  end.

Definition clearf_redundant lsb sz (x: nval) :=
  andimm_redundant x (Int.not (ExtValues.bitfield_mask lsb sz)).

Lemma clearf_redundant_sound:
  forall lsb sz v w x,
  clearf_redundant lsb sz x = true ->
  vagree v w (clearf lsb sz x) ->
  vagree (ExtValues.clearf lsb sz v) w x.
Proof.
  unfold clearf, ExtValues.clearf, clearf_redundant. intros.
  destruct (ExtValues.is_bitfield lsb sz).
  - apply andimm_redundant_sound; assumption.
  - apply vagree_lessdef. constructor.
Qed.

Definition insf_redundant := clearf_redundant.

Lemma vagree_vundef: forall b c, vagree Vundef b c.
Proof.
  intros. apply vagree_lessdef. constructor.
Qed.

Lemma insf_redundant_sound:
  forall lsb sz v1 w1 v2 x
  (REDUNDANT : insf_redundant lsb sz x = true)
  (AGREE1 : vagree v1 w1 (insf1 lsb sz x)),
  vagree (ExtValues.insf lsb sz v1 v2) w1 x.
Proof.
  unfold ExtValues.insf. intros.
  destruct (ExtValues.is_bitfield lsb sz) eqn:IS_BITFIELD; cycle 1.
  { apply vagree_vundef. }
  destruct x; cbn in *; trivial; try discriminate.
  destruct Int.eq_dec as [EQ | NEQ] in REDUNDANT; [clear REDUNDANT | discriminate].
  rewrite Int.not_involutive in EQ.
  unfold insf1 in AGREE1.
  rewrite IS_BITFIELD in AGREE1.
  unfold andimm, bitwise in AGREE1. cbn in AGREE1.
  destruct v1; cbn; trivial.
  destruct w1; cbn; try contradiction.
  destruct v2; cbn; trivial.
  destruct (Int.ltu lsb Int.iwordsize) eqn:LTU; cbn; trivial.
  set (mask := (ExtValues.bitfield_mask lsb sz)) in *.
  unfold iagree in *.
  intros k kRANGE kTEST.
  rewrite Int.bits_or by assumption.
  rewrite Int.bits_and by assumption.
  rewrite Int.bits_not by assumption.
  rewrite Int.bits_and by assumption.
  destruct (Int.testbit mask k) eqn:MASK.
  - assert (Int.testbit (Int.and m mask) k = true) as ABSURD.
    { rewrite Int.bits_and by assumption.
      rewrite kTEST. rewrite MASK. reflexivity. }
    rewrite EQ in ABSURD. rewrite Int.bits_zero in ABSURD.
    discriminate.
  - rewrite andb_false_r; rewrite andb_true_r ; cbn.
    rewrite orb_false_r. apply AGREE1. assumption.
    rewrite Int.bits_and by assumption.
    rewrite kTEST. cbn. rewrite Int.bits_not by assumption.
    rewrite MASK. reflexivity.
Qed.
     
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
  | Obfc lsb sz => clearf_redundant lsb sz nv
  | Obfi lsb sz => insf_redundant lsb sz 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 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 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 makelong_sound; auto.
- apply loword_sound; auto.
- apply hiword_sound; auto.
- 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.
- destruct (eval_condition c args m) as [b|] eqn:EC.
  erewrite needs_of_condition_sound by eauto.
  apply select_sound; auto with na.
  simpl; auto with na.
- apply clearf_sound; auto.
- apply insf_sound; auto.
- apply add_sound; auto with na.
- (* Ocmpcarryu *)
  assert (D: default nv = All) by (destruct nv; simpl; congruence).
  rewrite D in *.
  apply lessdef_vagree in H6, H4, H5, H7.
  apply vagree_lessdef.
  pose proof (Val.longofwords_lessdef _ _ _ _ H6 H4) as L1.
  pose proof (Val.longofwords_lessdef _ _ _ _ H5 H7) as L2.
  destruct (Val.cmplu_bool (fun _ _ => true) c (Val.longofwords v0 v1)
                           (Val.longofwords v2 v3)) as [b|] eqn:CMP.
  + erewrite Val.cmplu_bool_lessdef
      with (v1' := Val.longofwords v5 v6)
           (v2' := Val.longofwords v7 v8)
           (valid_ptr' := fun _ _ => true);
    eauto.
  + cbn. apply Val.lessdef_undef.
- (* Ocmpcarry *)
  assert (D: default nv = All) by (destruct nv; simpl; congruence).
  rewrite D in *.
  apply lessdef_vagree in H6, H4, H5, H7.
  apply vagree_lessdef.
  pose proof (Val.longofwords_lessdef _ _ _ _ H6 H4) as L1.
  pose proof (Val.longofwords_lessdef _ _ _ _ H5 H7) as L2.
  inv L1; cbn.
  + inv L2; cbn.
    * apply Val.lessdef_refl.
    * destruct (Val.longofwords v0 v1); cbn; apply Val.lessdef_undef.
  + destruct (Val.longofwords v5 v6); cbn; apply Val.lessdef_undef.
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. lia.
- apply sign_ext_redundant_sound; auto. lia.
- apply andimm_redundant_sound; auto.
- apply orimm_redundant_sound; auto.
- apply clearf_redundant_sound; auto.
- apply insf_redundant_sound; auto.
Qed.

End SOUNDNESS.
Generated by coq2html