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 with
  | Ccomp _ => vl
  | _ => vl
  end.

Definition eval_static_condition (cond: condition) (vl: list ival): ibool :=
  match cond with
  | Ccomp _ => Btop
  | _ => Btop
  end.

Definition eval_static_operation (op: operation) (vl: list ival): ival :=
  match op with
  | Omove => Itop
  | _ => Itop
  end.

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

Theorem filter_static_condition_sound:
  forall 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:
  forall cond vargs m aargs,
  list_forall2 vmatch vargs aargs ->
  cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).

Hint Resolve eval_static_condition_sound : ival.

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}.