Module ValueAOp

Require Import Coqlib.
Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import ValueDomain.
Require Import RTL.
Require Import ExtValues.


Definition filter_static_condition (cond: condition) (vl: list aval): list aval :=
  match cond, vl with
  | (Ccomp Ceq | Ccompu Ceq), v1 :: v2 :: nil =>
      let v := vglb v1 v2 in
      v :: v :: nil
  | (Ccompimm Ceq n | Ccompuimm Ceq n), v1 :: nil =>
      (vglb v1 (I n))::nil
  | _, _ => vl
  end.

Definition eval_static_shift (s: shift) (v: aval): aval :=
  match s with
  | Slsl x => shl v (I x)
  | Slsr x => shru v (I x)
  | Sasr x => shr v (I x)
  | Sror x => ror v (I x)
  end.

Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
  match cond, vl with
  | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
  | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2
  | Ccompshift c s, v1 :: v2 :: nil => cmp_bool c v1 (eval_static_shift s v2)
  | Ccompushift c s, v1 :: v2 :: nil => cmpu_bool c v1 (eval_static_shift s v2)
  | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n)
  | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n)
  | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2
  | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
  | Ccompfzero c, v1 :: nil => cmpf_bool c v1 (F Float.zero)
  | Cnotcompfzero c, v1 :: nil => cnot (cmpf_bool c v1 (F Float.zero))
  | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
  | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
  | Ccompfszero c, v1 :: nil => cmpfs_bool c v1 (FS Float32.zero)
  | Cnotcompfszero c, v1 :: nil => cnot (cmpfs_bool c v1 (FS Float32.zero))
  | Cmaskzero n, v1 :: nil => maskzero v1 n
  | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n)
  | Ccompcarryu _, _ :: _ :: _ :: _ :: nil => Btop
  | Ccompcarry _, _ :: _ :: _ :: _ :: nil => Btop
  | _, _ => Bnone
  end.

Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
  match addr, vl with
  | Aindexed n, v1::nil => add v1 (I n)
  | Aindexed2, v1::v2::nil => add v1 v2
  | Aindexed2shift s, v1::v2::nil => add v1 (eval_static_shift s v2)
  | Ainstack ofs, nil => Ptr(Stk ofs)
  | _, _ => Vbot
  end.

Definition eval_static_insf lsb sz prev fld :=
  let mask := I (Int.shl (Int.repr (Z.ones (Int.unsigned sz))) lsb) in
  if is_bitfield lsb sz
  then
    or (and prev (notint mask))
       (and (shl fld (I lsb)) mask)
  else Vtop.

Definition eval_static_clearf lsb sz prev :=
  let mask := I (Int.shl (Int.repr (Z.ones (Int.unsigned sz))) lsb) in
  if is_bitfield lsb sz
  then and prev (notint mask)
  else Vtop.

Definition eval_static_operation (op: operation) (vl: list aval): aval :=
  match op, vl with
  | Omove, v1::nil => v1
  | Ocopy, v1::v2::nil => copy v1
  | Ocopyimm _, v1::nil => copy v1
  | Ointconst n, nil => I n
  | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop
  | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop
  | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs)
  | Oaddrstack ofs, nil => Ptr (Stk ofs)
  | Ocast8signed, v1 :: nil => sign_ext 8 v1
  | Ocast16signed, v1 :: nil => sign_ext 16 v1
  | Oadd, v1::v2::nil => add v1 v2
  | Oaddshift s, v1::v2::nil => add v1 (eval_static_shift s v2)
  | Oaddimm n, v1::nil => add v1 (I n)
  | Osub, v1::v2::nil => sub v1 v2
  | Osubshift s, v1::v2::nil => sub v1 (eval_static_shift s v2)
  | Orsubshift s, v1::v2::nil => sub (eval_static_shift s v2) v1
  | Orsubimm n, v1::nil => sub (I n) v1
  | Omul, v1::v2::nil => mul v1 v2
  | Omla, v1::v2::v3::nil => add (mul v1 v2) v3
  | Omls, v1::v2::v3::nil => sub v3 (mul v1 v2)
  | Omulhs, v1::v2::nil => mulhs v1 v2
  | Omulhu, v1::v2::nil => mulhu v1 v2
  | Odiv, v1::v2::nil => divs v1 v2
  | Odivu, v1::v2::nil => divu v1 v2
  | Oand, v1::v2::nil => and v1 v2
  | Oandshift s, v1::v2::nil => and v1 (eval_static_shift s v2)
  | Oandimm n, v1::nil => and v1 (I n)
  | Oor, v1::v2::nil => or v1 v2
  | Oorshift s, v1::v2::nil => or v1 (eval_static_shift s v2)
  | Oorimm n, v1::nil => or v1 (I n)
  | Oxor, v1::v2::nil => xor v1 v2
  | Oxorshift s, v1::v2::nil => xor v1 (eval_static_shift s v2)
  | Oxorimm n, v1::nil => xor v1 (I n)
  | Obic, v1::v2::nil => and v1 (notint v2)
  | Obicshift s, v1::v2::nil => and v1 (notint (eval_static_shift s v2))
  | Onot, v1::nil => notint v1
  | Onotshift s, v1::nil => notint (eval_static_shift s v1)
  | Oshl, v1::v2::nil => shl v1 v2
  | Oshr, v1::v2::nil => shr v1 v2
  | Oshru, v1::v2::nil => shru v1 v2
  | Oror, v1::v2::nil => ror v1 v2
  | Oshift s, v1::nil => eval_static_shift s v1
  | Oshrximm n, v1::nil => shrx v1 (I n)
  | Onegf, v1::nil => negf v1
  | Oabsf, v1::nil => absf v1
  | Oaddf, v1::v2::nil => addf v1 v2
  | Osubf, v1::v2::nil => subf v1 v2
  | Omulf, v1::v2::nil => mulf v1 v2
  | Odivf, v1::v2::nil => divf v1 v2
  | Osqrtf, v1::nil => sqrtf v1
  | Omlaf, v1::v2::v3::nil => addf v1 (mulf v2 v3)
  | Omlsf, v1::v2::v3::nil => subf v1 (mulf v2 v3)
  | Onegfs, v1::nil => negfs v1
  | Oabsfs, v1::nil => absfs v1
  | Oaddfs, v1::v2::nil => addfs v1 v2
  | Osubfs, v1::v2::nil => subfs v1 v2
  | Omulfs, v1::v2::nil => mulfs v1 v2
  | Odivfs, v1::v2::nil => divfs v1 v2
  | Osqrtfs, v1::nil => sqrtfs v1
  | Omlafs, v1::v2::v3::nil => addfs v1 (mulfs v2 v3)
  | Omlsfs, v1::v2::v3::nil => subfs v1 (mulfs v2 v3)
  | Osingleoffloat, v1::nil => singleoffloat v1
  | Ofloatofsingle, v1::nil => floatofsingle v1
  | Ointoffloat, v1::nil => intoffloat v1
  | Ointuoffloat, v1::nil => intuoffloat v1
  | Ofloatofint, v1::nil => floatofint v1
  | Ofloatofintu, v1::nil => floatofintu v1
  | Ointofsingle, v1::nil => intofsingle v1
  | Ointuofsingle, v1::nil => intuofsingle v1
  | Osingleofint, v1::nil => singleofint v1
  | Osingleofintu, v1::nil => singleofintu v1
  | Omakelong, v1::v2::nil => longofwords v1 v2
  | Olowlong, v1::nil => loword v1
  | Ohighlong, v1::nil => hiword v1
  | Ocmp c, _ => of_optbool (eval_static_condition c vl)
  | Osel c, v1::v2::vl => select (eval_static_condition c vl) v1 v2
  | Oselimm c imm, v1::vl => select (eval_static_condition c vl) v1 (I imm)
  | Oselimm2 c imm1 imm2, vl => select (eval_static_condition c vl) (I imm1) (I imm2)
  | Oclz, v1::nil => match v1 with I n => I (Int.clz n) | _ => Vtop end
  | Oreverse_bits, v1::nil => match v1 with I n => I (Int.reverse_bits n) | _ => Vtop end
  | Obswap32, v1::nil => match v1 with I n => I (Int.bswap32 n) | _ => Vtop end
  | Obits_of_single, v1::nil => bits_of_single v1
  | Osingle_of_bits, v1::nil => single_of_bits v1
  | Ohibits_of_float, v1::nil => hiword (bits_of_float v1)
  | (Osbfx lsb sz), v1::nil =>
       sign_ext (Int.unsigned sz) (shru v1 (I lsb))
  | (Oubfx lsb sz), v1::nil =>
      zero_ext (Int.unsigned sz) (shru v1 (I lsb))
  | (Obfi lsb sz), v1::v2::nil =>
      eval_static_insf lsb sz v1 v2
  | (Obfc lsb sz), v1::nil =>
      eval_static_clearf lsb sz v1
  | Ogetcanary, nil => canary_aval
  | Oaddimm_reg n, v1::nil => add v1 (I n)
  | OEaddimm n, v1::nil => add v1 (I n)
  | OEsubimm n, v1::nil => sub v1 (I n)
  | OErsbimm n, v1::nil => sub (I n) v1
  | OEandimm n, v1::nil => and v1 (I n)
  | OEbicimm n, v1::nil => and v1 (notint (I n))
  | OEorrimm n, v1::nil => or v1 (I n)
  | OEeorimm n, v1::nil => xor v1 (I n)
  | OEmovimm n, nil => I n
  | OEmvnimm n, nil => notint (I n)
  | Ocmpcarryu _, _::_::_::_::nil => Vtop
  | Ocmpcarry _, _::_::_::_::nil => Vtop
  | _, _ => Vbot
  end.

Section SOUNDNESS.

Variable bc: block_classification.
Variable genF genV: Type.
Variable ge: Genv.t genF genV.

Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.

Theorem filter_static_condition_sound:
  forall cond vargs m aargs
         (MATCH : list_forall2 (vmatch bc) vargs aargs)
         (COND : (eval_condition cond vargs m) = Some true),
     (list_forall2 (vmatch bc) vargs (filter_static_condition cond aargs)).

Lemma eval_static_shift_sound:
  forall s v a,
  vmatch bc v a ->
  vmatch bc (eval_shift s v) (eval_static_shift s a).

Hint Resolve eval_static_shift_sound: va.

Theorem eval_static_condition_sound:
  forall cond vargs m aargs,
  list_forall2 (vmatch bc) vargs aargs ->
  cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).

Lemma symbol_address_sound:
  forall id ofs,
  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).

Hint Resolve symbol_address_sound: va.

Ltac InvHyps :=
  match goal with
  | [H: None = Some _ |- _ ] => discriminate
  | [H: Some _ = Some _ |- _] => inv H
  | [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ ,
     H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps
  | _ => idtac
  end.

Theorem eval_static_addressing_sound:
  forall addr vargs vres aargs,
  eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres ->
  list_forall2 (vmatch bc) vargs aargs ->
  vmatch bc vres (eval_static_addressing addr aargs).

Theorem eval_static_insf_sound:
  forall lsb sz vprev aprev vfld afld
         (pMATCH : vmatch bc vprev aprev)
         (fMATCH : vmatch bc vfld afld),
    (vmatch bc (ExtValues.insf lsb sz vprev vfld)
            (eval_static_insf lsb sz aprev afld)).

Definition eval_static_clearf_sound:
  forall lsb sz vprev aprev
         (pMATCH : vmatch bc vprev aprev),
    (vmatch bc (ExtValues.clearf lsb sz vprev)
            (eval_static_clearf lsb sz aprev)).

Hint Resolve eval_static_insf_sound eval_static_clearf_sound : va.

Theorem eval_static_operation_sound:
  forall op vargs m vres aargs,
  eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
  list_forall2 (vmatch bc) vargs aargs ->
  vmatch bc vres (eval_static_operation op aargs).

End SOUNDNESS.

Arguments eval_static_operation_sound (bc) {genF genV}.
Arguments eval_static_addressing_sound (bc) {genF genV}.