(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

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

(** Value analysis for RISC V operators *)

Definition zero32 := (I Int.zero).
Definition zero64 := (L Int64.zero).

(** Functions to select a special register (see Op.v) *)

Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
  match optR with
  | None => sem v1 v2
  | Some X0_L => sem vz v1
  | Some X0_R => sem v1 vz
  end.

Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
  match mu with
  | MUint => match v1, v2 with
             | I _, I _ => v2
             | _, _ => Ifptr Ptop
             end
  | MUlong => match v1, v2 with
              | L _, I _ => v2
              | _, _ => Ifptr Ptop
              end
  | MUshrx i =>
      match v1, v2 with
      | I _, I _ =>
          if Int.ltu i (Int.repr 31) then v2 else Ifptr Ptop
      | _, _ => Ifptr Ptop
      end
  | MUshrxl i =>
      match v1, v2 with
      | L _, L _ =>
          if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop
      | _, _ => Ifptr Ptop
      end
  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
  | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n)
  | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n)
  | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2
  | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2
  | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n)
  | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n)
  | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2
  | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
  | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
  | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
  | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32
  | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32
  | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32
  | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32
  | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32
  | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32
  | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32
  | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32
  | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64
  | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64
  | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64
  | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64
  | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64
  | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64
  | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64
  | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64
  | _, _ => Bnone
  end.

Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
  match addr, vl with
  | Aindexed n, v1::nil => offset_ptr v1 n
  | Aglobal s ofs, nil => Ptr (Gl s ofs)
  | Ainstack ofs, nil => Ptr (Stk ofs)
  | _, _ => Vbot
  end.

Definition bits_of_single (v : aval) : aval :=
  match v with
  | FS f => I (Float32.to_bits f)
  | _ => ntop1 v
  end.

Definition bits_of_float (v : aval) : aval :=
  match v with
  | F f => L (Float.to_bits f)
  | _ => ntop1 v
  end.

Definition single_of_bits (v : aval) : aval :=
  match v with
  | I f => FS (Float32.of_bits f)
  | _ => ntop1 v
  end.

Definition float_of_bits (v : aval) : aval :=
  match v with
  | L f => F (Float.of_bits f)
  | _ => ntop1 v
  end.

Definition select01_long (vb : aval) (vt : aval) (vf : aval) :=
  match vb with
  | I b =>
    if Int.eq b Int.one then add_undef vt
    else if Int.eq b Int.zero then add_undef vf
         else add_undef (vlub vt vf)
  | _ => add_undef (vlub vt vf)
  end.

Definition eval_static_operation (op: operation) (vl: list aval): aval :=
  match op, vl with
  | Omove, v1::nil => v1
  | Ointconst n, nil => I n
  | Olongconst n, nil => L 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
  | Oaddimm n, v1::nil => add v1 (I n)
  | Oneg, v1::nil => neg v1
  | Osub, v1::v2::nil => sub v1 v2
  | Omul, v1::v2::nil => mul v1 v2
  | Omulhs, v1::v2::nil => mulhs v1 v2
  | Omulhu, v1::v2::nil => mulhu v1 v2
  | Odiv, v1::v2::nil => divs_total v1 v2
  | Odivu, v1::v2::nil => divu_total v1 v2
  | Omod, v1::v2::nil => mods_total v1 v2
  | Omodu, v1::v2::nil => modu_total v1 v2
  | Oand, v1::v2::nil => and v1 v2
  | Oandimm n, v1::nil => and v1 (I n)
  | Oor, v1::v2::nil => or v1 v2
  | Oorimm n, v1::nil => or v1 (I n)
  | Oxor, v1::v2::nil => xor v1 v2
  | Oxorimm n, v1::nil => xor v1 (I n)
  | Oshl, v1::v2::nil => shl v1 v2
  | Oshlimm n, v1::nil => shl v1 (I n)
  | Oshr, v1::v2::nil => shr v1 v2
  | Oshrimm n, v1::nil => shr v1 (I n)
  | Oshru, v1::v2::nil => shru v1 v2
  | Oshruimm n, v1::nil => shru v1 (I n)
  | Oshrximm n, v1::nil => shrx v1 (I n)
  | Omakelong, v1::v2::nil => longofwords v1 v2
  | Olowlong, v1::nil => loword v1
  | Ohighlong, v1::nil => hiword v1
  | Ocast32signed, v1::nil => longofint v1
  | Ocast32unsigned, v1::nil => longofintu v1
  | Oaddl, v1::v2::nil => addl v1 v2
  | Oaddlimm n, v1::nil => addl v1 (L n)
  | Onegl, v1::nil => negl v1
  | Osubl, v1::v2::nil => subl v1 v2
  | Omull, v1::v2::nil => mull v1 v2
  | Omullhs, v1::v2::nil => mullhs v1 v2
  | Omullhu, v1::v2::nil => mullhu v1 v2
  | Odivl, v1::v2::nil => divls_total v1 v2
  | Odivlu, v1::v2::nil => divlu_total v1 v2
  | Omodl, v1::v2::nil => modls_total v1 v2
  | Omodlu, v1::v2::nil => modlu_total v1 v2
  | Oandl, v1::v2::nil => andl v1 v2
  | Oandlimm n, v1::nil => andl v1 (L n)
  | Oorl, v1::v2::nil => orl v1 v2
  | Oorlimm n, v1::nil => orl v1 (L n)
  | Oxorl, v1::v2::nil => xorl v1 v2
  | Oxorlimm n, v1::nil => xorl v1 (L n)
  | Oshll, v1::v2::nil => shll v1 v2
  | Oshllimm n, v1::nil => shll v1 (I n)
  | Oshrl, v1::v2::nil => shrl v1 v2
  | Oshrlimm n, v1::nil => shrl v1 (I n)
  | Oshrlu, v1::v2::nil => shrlu v1 v2
  | Oshrluimm n, v1::nil => shrlu v1 (I n)
  | Oshrxlimm n, v1::nil => shrxl 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
  | 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
  | Osingleoffloat, v1::nil => singleoffloat v1
  | Ofloatofsingle, v1::nil => floatofsingle v1
  | Ointoffloat, v1::nil => intoffloat_total v1
  | Ointuoffloat, v1::nil => intuoffloat_total v1
  | Ofloatofint, v1::nil => floatofint v1
  | Ofloatofintu, v1::nil => floatofintu v1
  | Ointofsingle, v1::nil => intofsingle_total v1
  | Ointuofsingle, v1::nil => intuofsingle_total v1
  | Osingleofint, v1::nil => singleofint v1
  | Osingleofintu, v1::nil => singleofintu v1
  | Olongoffloat, v1::nil => longoffloat_total v1
  | Olonguoffloat, v1::nil => longuoffloat_total v1
  | Ofloatoflong, v1::nil => floatoflong v1
  | Ofloatoflongu, v1::nil => floatoflongu v1
  | Olongofsingle, v1::nil => longofsingle_total v1
  | Olonguofsingle, v1::nil => longuofsingle_total v1
  | Osingleoflong, v1::nil => singleoflong v1
  | Osingleoflongu, v1::nil => singleoflongu v1
  | Ocmp c, _ => of_optbool (eval_static_condition c vl)
  | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32)
  | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32)
  | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32)
  | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32)
  | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32)
  | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32)
  | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
  | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
  | OExoriw n, v1::nil => xor v1 (I n)
  | OEluiw n, nil => shl (I n) (I (Int.repr 12))
  | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32
  | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (I n) (Ifptr Ptop)
  | OEandiw n, v1::nil => and (I n) v1
  | OEoriw n, v1::nil => or (I n) v1
  | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64)
  | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64)
  | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64)
  | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64)
  | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64)
  | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64)
  | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
  | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
  | OEandil n, v1::nil => andl (L n) v1
  | OEoril n, v1::nil => orl (L n) v1
  | OExoril n, v1::nil => xorl v1 (L n)
  | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
  | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64
  | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (L n) (Ifptr Ptop)
  | OEloadli n, nil => L (n)
  | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2
  | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
  | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
  | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2)
  | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2)
  | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2)
  | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2)
  | Obits_of_single, v1::nil => bits_of_single v1
  | Obits_of_float, v1::nil => bits_of_float v1
  | Osingle_of_bits, v1::nil => single_of_bits v1
  | Ofloat_of_bits, v1::nil => float_of_bits v1
  | Oselectl, vb::vt::vf::nil => select01_long vb vt vf
  | _, _ => Vbot
  end.

Section SOUNDNESS.

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

Lemma bits_of_single_sound:
  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_single v) (bits_of_single x).
Proof.
  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
Qed.

Lemma bits_of_float_sound:
  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_float v) (bits_of_float x).
Proof.
  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
Qed.

Lemma single_of_bits_sound:
  forall v x, vmatch bc v x -> vmatch bc (ExtValues.single_of_bits v) (single_of_bits x).
Proof.
  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
Qed.

Lemma float_of_bits_sound:
  forall v x, vmatch bc v x -> vmatch bc (ExtValues.float_of_bits v) (float_of_bits x).
Proof.
  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
Qed.

  
Lemma select01_long_sound:
  forall vb xb vt xt vf xf
         (MATCH_b : vmatch bc vb xb)
         (MATCH_t : vmatch bc vt xt)
         (MATCH_f : vmatch bc vf xf),
    vmatch bc (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
              (select01_long xb xt xf).
Proof.
  intros.
  inv MATCH_b; cbn; try apply add_undef_undef.
  - destruct (Int.eq i Int.one). { apply add_undef_normalize; trivial. }
    destruct (Int.eq i Int.zero). { apply add_undef_normalize; trivial. }
    cbn. apply add_undef_undef.
  - destruct (Int.eq i Int.one).
    { apply add_undef_normalize.
      apply vmatch_lub_l.
      trivial. }
    destruct (Int.eq i Int.zero).
    { apply add_undef_normalize.
      apply vmatch_lub_r.
      trivial. }
    cbn. apply add_undef_undef.
  - destruct (Int.eq i Int.one).
    { apply add_undef_normalize.
      apply vmatch_lub_l.
      trivial. }
    destruct (Int.eq i Int.zero).
    { apply add_undef_normalize.
      apply vmatch_lub_r.
      trivial. }
    cbn. apply add_undef_undef.
  - destruct (Int.eq i Int.one).
    { apply add_undef_normalize.
      apply vmatch_lub_l.
      trivial. }
    destruct (Int.eq i Int.zero).
    { apply add_undef_normalize.
      apply vmatch_lub_r.
      trivial. }
    cbn. apply add_undef_undef.
Qed.

Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound select01_long_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).
Proof.
  intros until aargs; intros VM. inv VM.
  destruct cond; auto with va.
  inv H0.
  destruct cond; simpl; eauto with va.
  inv H2.
  destruct cond; simpl; eauto with va.
  17: destruct cond; simpl; eauto with va.
  all: destruct optR as [[]|]; unfold apply_bin_oreg, Op.apply_bin_oreg;
       unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va.
Qed.

Lemma symbol_address_sound:
  forall id ofs,
  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
Proof.
  intros; apply symbol_address_sound; apply GENV.
Qed.

Lemma symbol_address_sound_2:
  forall id ofs,
  vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)).
Proof.
  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F.
  constructor. constructor. apply GENV; auto.
  constructor.
Qed.

Hint Resolve symbol_address_sound symbol_address_sound_2: 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
  | [H: (if Archi.ptr64 then _ else _) = Some _ |- _] => destruct Archi.ptr64 eqn:?; 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).
Proof.
  unfold eval_addressing, eval_static_addressing; intros;
  destruct addr; InvHyps; eauto with va.
  rewrite Ptrofs.add_zero_l; eauto with va.
Qed.

Lemma of_optbool_maketotal_sound:
  forall ob ab, cmatch ob ab -> vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (of_optbool ab).
Proof.
  intros.
  assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)).
  {
    destruct ob; simpl; auto with va.
    destruct b; constructor; try lia.
    change 1 with (usize Int.one). apply is_uns_usize.
    red; intros. apply Int.bits_zero.
  }
  inv H; auto. simpl. destruct b; constructor.
Qed.

Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m,
  c = Ceq \/ c = Cne \/ c = Clt->
  vmatch bc a1 b1 ->
  vmatch bc a0 b0 ->
  vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32)
  (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)).
Proof.
  intros.
  destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
Qed.

Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m,
  c = Ceq \/ c = Cne \/ c = Clt->
  vmatch bc a1 b1 ->
  vmatch bc a0 b0 ->
  vmatch bc
    (Val.maketotal
       (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0
          Op.zero64))
    (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)).
Proof.
  intros.
  destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
Qed.

Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp,
  vmatch bc a1 b1 ->
  vmatch bc a0 b0 ->
  vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32)
  (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)).
Proof.
  intros.
  destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
Qed.

Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp,
  vmatch bc a1 b1 ->
  vmatch bc a0 b0 ->
  vmatch bc
    (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64))
    (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)).
Proof.
  intros.
  destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
Qed.

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).
Proof.
  unfold eval_operation, eval_static_operation; intros;
  destruct op; InvHyps; eauto with va.
  destruct (propagate_float_constants tt); constructor.
  destruct (propagate_float_constants tt); constructor.
  rewrite Ptrofs.add_zero_l; eauto with va.
  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.

  3,4,6: apply eval_cmpu_sound; auto.
  1,2,3: apply eval_cmp_sound; auto.
  unfold Val.cmp; apply of_optbool_sound; eauto with va.
  unfold Val.cmpu; apply of_optbool_sound; eauto with va.
  
  { destruct optR as [[]|]; simpl; eauto with va. }
  { destruct optR as [[]|];
    unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. }
  { fold (Val.and (Vint n) a1); eauto with va. }
  { fold (Val.or (Vint n) a1); eauto with va. }
  { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
  try apply vmatch_ifptr_undef. }
  9: { destruct optR as [[]|]; simpl; eauto with va. }
  9: { destruct optR as [[]|];
    unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. }
  9: { fold (Val.andl (Vlong n) a1); eauto with va. }
  9: { fold (Val.orl (Vlong n) a1); eauto with va. }
  9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
  apply vmatch_ifptr_l. }
  
  1,10: simpl; eauto with va.
  10:
    unfold Op.eval_may_undef, eval_may_undef; destruct mu;
    inv H1; inv H0; eauto with va;
    try destruct (Int.ltu _ _); simpl;
    try eapply vmatch_ifptr_p, pmatch_top'; eauto with va.
  
  4,5,7: apply eval_cmplu_sound; auto.
  1,3,4: apply eval_cmpl_sound; auto.
  2: { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. }
  2: { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. }
  all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
Qed.

End SOUNDNESS.