Module ZIntervalAOp

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

Definition filter_static_condition (cond: condition) (vl: list ival): list ival :=
  match cond, vl with
  | Ccomp c, v1 :: v2 :: nil =>
      let v' := filter_cmp c v1 v2 in
      (fst v') :: (snd v') :: nil
  | Ccompu c, v1 :: v2 :: nil =>
      let v' := filter_cmpu c v1 v2 in
      (fst v') :: (snd v') :: nil
  | Ccompimm c n, v1 :: nil =>
      let v' := filter_cmp c v1 (intconst n) in
      (fst v') :: nil
  | Ccompuimm c n, v1 :: nil =>
      let v' := filter_cmpu c v1 (intconst n) in
      (fst v') :: nil
  | Ccompl c, v1 :: v2 :: nil =>
      let v' := filter_cmpl c v1 v2 in
      (fst v') :: (snd v') :: nil
  | Ccomplu c, v1 :: v2 :: nil =>
      let v' := filter_cmplu c v1 v2 in
      (fst v') :: (snd v') :: nil
  | Ccomplimm c n, v1 :: nil =>
      let v' := filter_cmpl c v1 (longconst n) in
      (fst v') :: nil
  | Ccompluimm c n, v1 :: nil =>
      let v' := filter_cmplu c v1 (longconst n) in
      (fst v') :: nil
  | _, _ => vl
  end.

Definition eval_static_condition (cond: condition) (vl: list ival): ibool :=
  match cond, vl with
  | Ccomp c, v1 :: v2 :: nil => Btop
  | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2
  | Ccompimm c n, v1 :: nil => Btop
  | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (intconst n)
  | Ccompl c, v1 :: v2 :: nil => Btop
  | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2
  | Ccomplimm c n, v1 :: nil => Btop
  | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (longconst n)
  | _, _ => Btop
  end.

Definition eval_static_operation (op: operation) (vl: list ival): ival :=
  match op, vl with
  | Omove, v1::nil => v1
  | Ocopy, v1::v2::nil => Itop
  | Ocopyimm _, v1::nil => Itop
  | Ointconst n, nil => intconst n
  | Olongconst n, nil => longconst n
  | Ofloatconst n, nil => Itop
  | Osingleconst n, nil => Itop
  | Oaddrsymbol s ofs, nil => Itop
  | Oaddrstack ofs, nil => Itop
  | Ocast8signed, v1 :: nil => Itop
  | Ocast16signed, v1 :: nil => Itop

  | Oadd, v1 :: v2 :: nil => add v1 v2
  | Oaddimm n, v1 :: nil => add v1 (intconst n)
  | Oneg, v1 :: nil => neg v1
  | Osub, v1 :: v2 :: nil => sub v1 v2
  | Omul, v1 :: v2 :: nil => mul v1 v2
  | Omulhs, v1 :: v2 :: nil => Itop
  | Omulhu, v1 :: v2 :: nil => Itop
  | Odiv, v1 :: v2 :: nil => Itop
  | Odivu, v1 :: v2 :: nil => Itop
  | Omod, v1 :: v2 :: nil => Itop
  | Omodu, v1 :: v2 :: nil => Itop

  | Oand, _ | Oandimm _, _
  | Oor, _ | Oorimm _, _
  | Oxor, _ | Oxorimm _, _ => Itop

  | Oshl, v1 :: v2 :: nil => shl v1 v2
  | Oshlimm n, v1 :: nil => shl v1 (intconst n)
  | Oshr, v1 :: v2 :: nil => Itop
  | Oshrimm n, v1 :: nil => Itop
  | Oshru, v1 :: v2 :: nil => shru v1 v2
  | Oshruimm n, v1 :: nil => shru v1 (intconst n)
  | Oshrximm n, v1 :: nil => Itop

  | Omakelong, v1 :: v2 :: nil => Itop
  | Olowlong, v1 :: nil => loword v1
  | Ohighlong, v1 :: nil => Itop
  | Ocast32signed, v1 :: nil => Itop
  | Ocast32unsigned, v1 :: nil => longofintu v1
  | Oaddl, v1 :: v2 :: nil => addl v1 v2
  | Oaddlimm n, v1 :: nil => addl v1 (longconst n)
  | Onegl, v1 :: nil => negl v1
  | Osubl, v1 :: v2 :: nil => subl v1 v2
  | Omull, v1 :: v2 :: nil => mull v1 v2
  | Omullhs, v1 :: v2 :: nil => Itop
  | Omullhu, v1 :: v2 :: nil => Itop
  | Odivl, v1 :: v2 :: nil => Itop
  | Odivlu, v1 :: v2 :: nil => Itop
  | Omodl, v1 :: v2 :: nil => Itop
  | Omodlu, v1 :: v2 :: nil => Itop

  | Oandl, _ | Oandlimm _, _
  | Oorl, _ | Oorlimm _, _
  | Oxorl, _ | Oxorlimm _, _ => Itop

  | Oshll, v1 :: v2 :: nil => shll v1 v2
  | Oshllimm n, v1 :: nil => shll v1 (intconst n)
  | Oshrl, v1 :: v2 :: nil => Itop
  | Oshrlimm n, v1 :: nil => Itop
  | Oshrlu, v1 :: v2 :: nil => shrlu v1 v2
  | Oshrluimm n, v1 :: nil => shrlu v1 (intconst n)
  | Oshrxlimm n, v1 :: nil => Itop

                         
  | _, _ => Itop
  end.

Section SOUNDNESS.
Variable genF genV: Type.
Variable ge: Genv.t genF genV.
Variable sp: block.

Fixpoint list_forall2_Elim1 [A B : Type] (P : A -> B -> Prop) (u : list A) (Q : list B -> Prop): Prop :=
  match u with
  | nil => Q nil
  | x :: xs => forall y, P x y -> list_forall2_Elim1 P xs (fun ys => Q (y :: ys))
  end.

Lemma elim_forall2_1 [A B : Type] (P : A -> B -> Prop) (u : list A) (Q : list B -> Prop)
                     (H : list_forall2_Elim1 P u Q):
                     forall (v : list B), list_forall2 P u v -> Q v.

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

Theorem eval_static_condition_sound cond vargs m aargs
  (VM : list_forall2 vmatch vargs aargs):
  cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).

Hint Resolve eval_static_condition_sound : ival.

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_operation_sound:
  forall op vargs m vres aargs,
  eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
  list_forall2 vmatch vargs aargs ->
  vmatch vres (eval_static_operation op aargs).

End SOUNDNESS.

Arguments eval_static_operation_sound {genF genV}.