Operators and addressing modes. The abstract syntax and dynamic semantics for the CminorSel, RTL, LTL and Mach languages depend on the following types, defined in this library:

condition: boolean conditions for conditional branches;
operation: arithmetic and logical operations;
addressing: addressing modes for load and store operations.

These types are processor-specific and correspond roughly to what the processor can compute in one instruction. In other terms, these types reflect the state of the program after instruction selection. For a processor-independent set of operations, see the abstract syntax and dynamic semantics of the Cminor language.

Require Import BoolEqual Coqlib.
Require Import Errors.
Open Scope error_monad_scope.
Require Import AST Integers Floats.
Require Import Values Memory Globalenvs Events.
Require ExtValues.
Require Import Unityping.

Set Implicit Arguments.

Local Open Scope option_monad_scope.

Conditions (boolean-valued operators).

Type to modelize the use of a special register in arith operations

Inductive oreg: Type :=
  | X0_L: oreg
  | X0_R: oreg.

Inductive condition : Type :=
  | Ccomp (c: comparison) (* signed integer comparison *)
  | Ccompu (c: comparison) (* unsigned integer comparison *)
  | Ccompimm (c: comparison) (n: int) (* signed integer comparison with a constant *)
  | Ccompuimm (c: comparison) (n: int) (* unsigned integer comparison with a constant *)
  | Ccompl (c: comparison) (* signed 64-bit integer comparison *)
  | Ccomplu (c: comparison) (* unsigned 64-bit integer comparison *)
  | Ccomplimm (c: comparison) (n: int64) (* signed 64-bit integer comparison with a constant *)
  | Ccompluimm (c: comparison) (n: int64) (* unsigned 64-bit integer comparison with a constant *)
  | Ccompf (c: comparison) (* 64-bit floating-point comparison *)
  | Cnotcompf (c: comparison) (* negation of a floating-point comparison *)
  | Ccompfs (c: comparison) (* 32-bit floating-point comparison *)
  | Cnotcompfs (c: comparison) (* negation of a floating-point comparison *)
  | CEbeqw (optR: option oreg) (* branch-if-equal signed *)
  | CEbnew (optR: option oreg) (* branch-if-not-equal signed *)
  | CEbequw (optR: option oreg) (* branch-if-equal unsigned *)
  | CEbneuw (optR: option oreg) (* branch-if-not-equal unsigned *)
  | CEbltw (optR: option oreg) (* branch-if-less signed *)
  | CEbltuw (optR: option oreg) (* branch-if-less unsigned *)
  | CEbgew (optR: option oreg) (* branch-if-greater-or-equal signed *)
  | CEbgeuw (optR: option oreg) (* branch-if-greater-or-equal unsigned *)
  | CEbeql (optR: option oreg) (* branch-if-equal signed *)
  | CEbnel (optR: option oreg) (* branch-if-not-equal signed *)
  | CEbequl (optR: option oreg) (* branch-if-equal unsigned *)
  | CEbneul (optR: option oreg) (* branch-if-not-equal unsigned *)
  | CEbltl (optR: option oreg) (* branch-if-less signed *)
  | CEbltul (optR: option oreg) (* branch-if-less unsigned *)
  | CEbgel (optR: option oreg) (* branch-if-greater-or-equal signed *)
  | CEbgeul (optR: option oreg). (* branch-if-greater-or-equal unsigned *)

Inductive mayundef: Type :=
  | MUint: mayundef
  | MUlong: mayundef
  | MUshrx: int -> mayundef
  | MUshrxl: int -> mayundef.

Arithmetic and logical operations. In the descriptions, rd is the result of the operation and r1, r2, etc, are the arguments.

Addressing modes. r1, r2, etc, are the arguments to the addressing.

Inductive addressing: Type :=
  | Aindexed: ptrofs -> addressing (* Address is r1 + offset *)
  | Aglobal: qualident -> ptrofs -> addressing (* Address is global plus offset *)
  | Ainstack: ptrofs -> addressing. (* Address is stack_pointer + offset *)
Definition Aindexed' i := Aindexed (Ptrofs.of_int i).

Comparison functions (used in modules CSE and Allocation).

Definition oreg_eq: forall (x y: oreg), {x=y} + {x<>y}.

Proof.

decide equality. Defined.

Definition eq_condition (x y: condition) : {x=y} + {x<>y}.

Proof.

  generalize Int.eq_dec Int64.eq_dec bool_dec oreg_eq; intros.
  assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
  decide equality.
  all: destruct optR, optR0; decide equality.
Defined.

Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.

Proof.

generalize ident_eq Ptrofs.eq_dec QualIdent.eq; intros.
repeat decide equality.
Defined.

Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.

Proof.

generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq oreg_eq QualIdent.eq; intros.
repeat decide equality.
Defined.

Global Opaque eq_condition eq_addressing eq_operation.

Generic function to evaluate an instruction according to the given specific register

Definition zero32 := (Vint Int.zero).
Definition zero64 := (Vlong Int64.zero).

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

Mayundef evaluation according to the above defined type

Evaluation functions

Evaluation of conditions, operators and addressing modes applied to lists of values. Return None when the computation can trigger an error, e.g. integer division by zero. eval_condition returns a boolean, eval_operation and eval_addressing return a value.

Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
  match cond, vl with
  | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
  | Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 v2
  | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n)
  | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n)
  | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2
  | Ccomplu c, v1 :: v2 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
  | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n)
  | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n)
  | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2
  | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
  | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
  | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
  | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32
  | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32
  | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
  | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
  | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32
  | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32
  | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32
  | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32
  | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64
  | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64
  | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
  | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
  | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64
  | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64
  | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64
  | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64
  | _, _ => None
  end.

Assert sp is a pointer

Definition get_sp sp :=
  match sp with
  | Vptr _ _ => sp
  | _ => Vundef
  end.

Definition eval_operation
    (F V: Type) (genv: Genv.t F V) (sp: val)
    (op: operation) (vl: list val) (m: mem): option val :=
  match op, vl with
  | Omove, v1::nil => Some v1
  | Ocopy, v1::v2::nil => Some v1
  | Ocopyimm _, v1::nil => Some v1
  | (Owelldef ty), v1::nil => Val.welldefined v1 ty
  | Ointconst n, nil => Some (Vint n)
  | Olongconst n, nil => Some (Vlong n)
  | Ofloatconst n, nil => Some (Vfloat n)
  | Osingleconst n, nil => Some (Vsingle n)
  | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs)
  | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs)
  | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
  | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
  | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
  | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n))
  | Oneg, v1 :: nil => Some (Val.neg v1)
  | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
  | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
  | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
  | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
  | Odiv, v1 :: v2 :: nil => Some (Val.maketotal (Val.divs v1 v2))
  | Odivu, v1 :: v2 :: nil => Some (Val.maketotal (Val.divu v1 v2))
  | Omod, v1 :: v2 :: nil => Some (Val.maketotal (Val.mods v1 v2))
  | Omodu, v1 :: v2 :: nil => Some (Val.maketotal (Val.modu v1 v2))
  | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
  | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n))
  | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2)
  | Oorimm n, v1 :: nil => Some (Val.or v1 (Vint n))
  | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2)
  | Oxorimm n, v1 :: nil => Some (Val.xor v1 (Vint n))
  | Oshl, v1 :: v2 :: nil => Some (Val.shl v1 v2)
  | Oshlimm n, v1 :: nil => Some (Val.shl v1 (Vint n))
  | Oshr, v1 :: v2 :: nil => Some (Val.shr v1 v2)
  | Oshrimm n, v1 :: nil => Some (Val.shr v1 (Vint n))
  | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2)
  | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n))
  | Oshrximm n, v1::nil => Some (Val.maketotal (Val.shrx v1 (Vint n)))
  | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2)
  | Olowlong, v1::nil => Some (Val.loword v1)
  | Ohighlong, v1::nil => Some (Val.hiword v1)
  | Ocast32signed, v1 :: nil => Some (Val.longofint v1)
  | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1)
  | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2)
  | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
  | Onegl, v1::nil => Some (Val.negl v1)
  | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
  | Omull, v1::v2::nil => Some (Val.mull v1 v2)
  | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
  | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
  | Odivl, v1::v2::nil => Some (Val.maketotal (Val.divls v1 v2))
  | Odivlu, v1::v2::nil => Some (Val.maketotal (Val.divlu v1 v2))
  | Omodl, v1::v2::nil => Some (Val.maketotal (Val.modls v1 v2))
  | Omodlu, v1::v2::nil => Some (Val.maketotal (Val.modlu v1 v2))
  | Oandl, v1::v2::nil => Some(Val.andl v1 v2)
  | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n))
  | Oorl, v1::v2::nil => Some(Val.orl v1 v2)
  | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n))
  | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2)
  | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n))
  | Oshll, v1::v2::nil => Some (Val.shll v1 v2)
  | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n))
  | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2)
  | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n))
  | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
  | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
  | Oshrxlimm n, v1::nil => Some (Val.maketotal (Val.shrxl v1 (Vint n)))
  | Onegf, v1::nil => Some (Val.negf v1)
  | Oabsf, v1::nil => Some (Val.absf v1)
  | Oaddf, v1::v2::nil => Some (Val.addf v1 v2)
  | Osubf, v1::v2::nil => Some (Val.subf v1 v2)
  | Omulf, v1::v2::nil => Some (Val.mulf v1 v2)
  | Odivf, v1::v2::nil => Some (Val.divf v1 v2)
  | Osqrtf, v1::nil => Some (Val.sqrtf v1)
  | Onegfs, v1::nil => Some (Val.negfs v1)
  | Oabsfs, v1::nil => Some (Val.absfs v1)
  | Oaddfs, v1::v2::nil => Some (Val.addfs v1 v2)
  | Osubfs, v1::v2::nil => Some (Val.subfs v1 v2)
  | Omulfs, v1::v2::nil => Some (Val.mulfs v1 v2)
  | Odivfs, v1::v2::nil => Some (Val.divfs v1 v2)
  | Osqrtfs, v1::nil => Some (Val.sqrtfs v1)
  | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
  | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
  | Ointoffloat, v1::nil => Some (Val.maketotal (Val.intoffloat v1))
  | Ointuoffloat, v1::nil => Some (Val.maketotal (Val.intuoffloat v1))
  | Ofloatofint, v1::nil => Some (Val.maketotal (Val.floatofint v1))
  | Ofloatofintu, v1::nil => Some (Val.maketotal (Val.floatofintu v1))
  | Ointofsingle, v1::nil => Some (Val.maketotal (Val.intofsingle v1))
  | Ointuofsingle, v1::nil => Some (Val.maketotal (Val.intuofsingle v1))
  | Osingleofint, v1::nil => Some (Val.maketotal (Val.singleofint v1))
  | Osingleofintu, v1::nil => Some (Val.maketotal (Val.singleofintu v1))
  | Olongoffloat, v1::nil => Some (Val.maketotal (Val.longoffloat v1))
  | Olonguoffloat, v1::nil => Some (Val.maketotal (Val.longuoffloat v1))
  | Ofloatoflong, v1::nil => Some (Val.maketotal (Val.floatoflong v1))
  | Ofloatoflongu, v1::nil => Some (Val.maketotal (Val.floatoflongu v1))
  | Olongofsingle, v1::nil => Some (Val.maketotal (Val.longofsingle v1))
  | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
  | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
  | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
  | Obits_of_single, v1::nil => Some (Val.bits_of_single v1)
  | Obits_of_float, v1::nil => Some (Val.bits_of_float v1)
  | Osingle_of_bits, v1::nil => Some (Val.single_of_bits v1)
  | Ofloat_of_bits, v1::nil => Some (Val.float_of_bits v1)
  | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
  | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32)
  | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32)
  | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
  | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
  | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32)
  | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
  | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
  | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
  | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
  | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
  | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32)
  | OEaddiw optR n, v1::nil => Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef)
  | OEandiw n, v1::nil => Some (Val.and (Vint n) v1)
  | OEoriw n, v1::nil => Some (Val.or (Vint n) v1)
  | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64))
  | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64))
  | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
  | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
  | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64))
  | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64))
  | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
  | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
  | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
  | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
  | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64)
  | OEaddil optR n, v1::nil => Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef)
  | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1)
  | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1)
  | OEloadli n, nil => Some (Vlong n)
  | OEmayundef mu, v1 :: v2 :: nil => Some (eval_may_undef mu v1 v2)
  | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
  | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
  | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2)
  | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2)
  | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2)
  | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2)
  | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
  | Ogetcanary, nil => Some (canary_val tt)
  | _, _ => None
  end.

Definition eval_addressing
    (F V: Type) (genv: Genv.t F V) (sp: val)
    (addr: addressing) (vl: list val) : option val :=
  match addr, vl with
  | Aindexed n, v1 :: nil => Some (Val.offset_ptr v1 n)
  | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs)
  | Ainstack n, nil => Some (Val.offset_ptr sp n)
  | _, _ => None
  end.

Remark eval_addressing_Ainstack:
  forall (F V: Type) (genv: Genv.t F V) sp ofs,
  eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs).

Proof.

intros. reflexivity.
Qed.

Remark eval_addressing_Ainstack_inv:
forall (F V: Type) (genv: Genv.t F V) sp ofs vl v,
eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs.

Proof.

unfold eval_addressing; intros; destruct vl; inv H; auto.
Qed.

Static typing of conditions, operators and addressing modes.

The type of mayundef and addsp is dynamic

Definition type_of_mayundef mu :=
  match mu with
  | MUint | MUshrx _ => (Tint :: Tint :: nil, Tint)
  | MUlong => (Tlong :: Tint :: nil, Tint)
  | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong)
  end.

Definition type_of_operation (op: operation) : list typ * typ :=
  match op with
  | Omove => (Tint :: nil, Tint)
  | Ocopy => (Tint :: Tint :: nil, Tint)
  | Ocopyimm uid => (Tint :: nil, Tint)
  | Owelldef ty => (ty :: nil, ty)
  | Ointconst _ => (nil, Tint)
  | Olongconst _ => (nil, Tlong)
  | Ofloatconst f => (nil, Tfloat)
  | Osingleconst f => (nil, Tsingle)
  | Oaddrsymbol _ _ => (nil, Tptr)
  | Oaddrstack _ => (nil, Tptr)
  | Ocast8signed => (Tint :: nil, Tint)
  | Ocast16signed => (Tint :: nil, Tint)
  | Oadd => (Tint :: Tint :: nil, Tint)
  | Oaddimm _ => (Tint :: nil, Tint)
  | Oneg => (Tint :: nil, Tint)
  | Osub => (Tint :: Tint :: nil, Tint)
  | Omul => (Tint :: Tint :: nil, Tint)
  | Omulhs => (Tint :: Tint :: nil, Tint)
  | Omulhu => (Tint :: Tint :: nil, Tint)
  | Odiv => (Tint :: Tint :: nil, Tint)
  | Odivu => (Tint :: Tint :: nil, Tint)
  | Omod => (Tint :: Tint :: nil, Tint)
  | Omodu => (Tint :: Tint :: nil, Tint)
  | Oand => (Tint :: Tint :: nil, Tint)
  | Oandimm _ => (Tint :: nil, Tint)
  | Oor => (Tint :: Tint :: nil, Tint)
  | Oorimm _ => (Tint :: nil, Tint)
  | Oxor => (Tint :: Tint :: nil, Tint)
  | Oxorimm _ => (Tint :: nil, Tint)
  | Oshl => (Tint :: Tint :: nil, Tint)
  | Oshlimm _ => (Tint :: nil, Tint)
  | Oshr => (Tint :: Tint :: nil, Tint)
  | Oshrimm _ => (Tint :: nil, Tint)
  | Oshru => (Tint :: Tint :: nil, Tint)
  | Oshruimm _ => (Tint :: nil, Tint)
  | Oshrximm _ => (Tint :: nil, Tint)
  | Omakelong => (Tint :: Tint :: nil, Tlong)
  | Olowlong => (Tlong :: nil, Tint)
  | Ohighlong => (Tlong :: nil, Tint)
  | Ocast32signed => (Tint :: nil, Tlong)
  | Ocast32unsigned => (Tint :: nil, Tlong)
  | Oaddl => (Tlong :: Tlong :: nil, Tlong)
  | Oaddlimm _ => (Tlong :: nil, Tlong)
  | Onegl => (Tlong :: nil, Tlong)
  | Osubl => (Tlong :: Tlong :: nil, Tlong)
  | Omull => (Tlong :: Tlong :: nil, Tlong)
  | Omullhs => (Tlong :: Tlong :: nil, Tlong)
  | Omullhu => (Tlong :: Tlong :: nil, Tlong)
  | Odivl => (Tlong :: Tlong :: nil, Tlong)
  | Odivlu => (Tlong :: Tlong :: nil, Tlong)
  | Omodl => (Tlong :: Tlong :: nil, Tlong)
  | Omodlu => (Tlong :: Tlong :: nil, Tlong)
  | Oandl => (Tlong :: Tlong :: nil, Tlong)
  | Oandlimm _ => (Tlong :: nil, Tlong)
  | Oorl => (Tlong :: Tlong :: nil, Tlong)
  | Oorlimm _ => (Tlong :: nil, Tlong)
  | Oxorl => (Tlong :: Tlong :: nil, Tlong)
  | Oxorlimm _ => (Tlong :: nil, Tlong)
  | Oshll => (Tlong :: Tint :: nil, Tlong)
  | Oshllimm _ => (Tlong :: nil, Tlong)
  | Oshrl => (Tlong :: Tint :: nil, Tlong)
  | Oshrlimm _ => (Tlong :: nil, Tlong)
  | Oshrlu => (Tlong :: Tint :: nil, Tlong)
  | Oshrluimm _ => (Tlong :: nil, Tlong)
  | Oshrxlimm _ => (Tlong :: nil, Tlong)
  | Onegf => (Tfloat :: nil, Tfloat)
  | Oabsf => (Tfloat :: nil, Tfloat)
  | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Osqrtf => (Tfloat :: nil, Tfloat)
  | Onegfs => (Tsingle :: nil, Tsingle)
  | Oabsfs => (Tsingle :: nil, Tsingle)
  | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
  | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle)
  | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle)
  | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle)
  | Osqrtfs => (Tsingle :: nil, Tsingle)
  | Osingleoffloat => (Tfloat :: nil, Tsingle)
  | Ofloatofsingle => (Tsingle :: nil, Tfloat)
  | Ointoffloat => (Tfloat :: nil, Tint)
  | Ointuoffloat => (Tfloat :: nil, Tint)
  | Ofloatofint => (Tint :: nil, Tfloat)
  | Ofloatofintu => (Tint :: nil, Tfloat)
  | Ointofsingle => (Tsingle :: nil, Tint)
  | Ointuofsingle => (Tsingle :: nil, Tint)
  | Osingleofint => (Tint :: nil, Tsingle)
  | Osingleofintu => (Tint :: nil, Tsingle)
  | Olongoffloat => (Tfloat :: nil, Tlong)
  | Olonguoffloat => (Tfloat :: nil, Tlong)
  | Ofloatoflong => (Tlong :: nil, Tfloat)
  | Ofloatoflongu => (Tlong :: nil, Tfloat)
  | Olongofsingle => (Tsingle :: nil, Tlong)
  | Olonguofsingle => (Tsingle :: nil, Tlong)
  | Osingleoflong => (Tlong :: nil, Tsingle)
  | Osingleoflongu => (Tlong :: nil, Tsingle)
  | Ocmp c => (type_of_condition c, Tint)
  | OEseqw _ => (Tint :: Tint :: nil, Tint)
  | OEsnew _ => (Tint :: Tint :: nil, Tint)
  | OEsequw _ => (Tint :: Tint :: nil, Tint)
  | OEsneuw _ => (Tint :: Tint :: nil, Tint)
  | OEsltw _ => (Tint :: Tint :: nil, Tint)
  | OEsltuw _ => (Tint :: Tint :: nil, Tint)
  | OEsltiw _ => (Tint :: nil, Tint)
  | OEsltiuw _ => (Tint :: nil, Tint)
  | OExoriw _ => (Tint :: nil, Tint)
  | OEluiw _ => (nil, Tint)
  | OEaddiw None _ => (Tint :: nil, Tint)
  | OEaddiw (Some _) _ => (nil, Tint)
  | OEandiw _ => (Tint :: nil, Tint)
  | OEoriw _ => (Tint :: nil, Tint)
  | OEseql _ => (Tlong :: Tlong :: nil, Tint)
  | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
  | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
  | OEsneul _ => (Tlong :: Tlong :: nil, Tint)
  | OEsltl _ => (Tlong :: Tlong :: nil, Tint)
  | OEsltul _ => (Tlong :: Tlong :: nil, Tint)
  | OEsltil _ => (Tlong :: nil, Tint)
  | OEsltiul _ => (Tlong :: nil, Tint)
  | OEandil _ => (Tlong :: nil, Tlong)
  | OEoril _ => (Tlong :: nil, Tlong)
  | OExoril _ => (Tlong :: nil, Tlong)
  | OEluil _ => (nil, Tlong)
  | OEaddil None _ => (Tlong :: nil, Tlong)
  | OEaddil (Some _) _ => (nil, Tlong)
  | OEloadli _ => (nil, Tlong)
  | OEmayundef mu => type_of_mayundef mu
  | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
  | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
  | OEfled => (Tfloat :: Tfloat :: nil, Tint)
  | OEfeqs => (Tsingle :: Tsingle :: nil, Tint)
  | OEflts => (Tsingle :: Tsingle :: nil, Tint)
  | OEfles => (Tsingle :: Tsingle :: nil, Tint)
  | Obits_of_single => (Tsingle :: nil, Tint)
  | Obits_of_float => (Tfloat :: nil, Tlong)
  | Osingle_of_bits => (Tint :: nil, Tsingle)
  | Ofloat_of_bits => (Tlong :: nil, Tfloat)
  | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong)
  | Ogetcanary => (nil, canary_type)
  end.

Definition type_of_addressing (addr: addressing) : list typ :=
  match addr with
  | Aindexed _ => Tptr :: nil
  | Aglobal _ _ => nil
  | Ainstack _ => nil
  end.

Inductive wt_special_op : operation -> list typ -> typ -> Prop :=
| wt_Omove : forall ty,
    wt_special_op Omove (ty :: nil) ty
| wt_Ocopy : forall ty,
    wt_special_op Ocopy (ty :: Tint :: nil) ty
| wt_Ocopyimm : forall uid ty,
    wt_special_op (Ocopyimm uid) (ty :: nil) ty.

Module RTLtypes <: TYPE_ALGEBRA.

Definition t := typ.
Definition eq := typ_eq.
Definition default := Tint.

End RTLtypes.

Module S := UniSolver(RTLtypes).

Definition type_special_op (e: S.typenv) (op: operation) args res : Errors.res S.typenv :=
  match op with
  | Omove | Ocopyimm _ =>
      match args with
      | arg :: nil => do (changed, e') <- S.move e res arg; OK e'
      | _ => Error (msg "ill-formed move")
      end
  | Ocopy =>
      match args with
      | arg :: uid :: nil =>
          do e' <- S.set e uid Tint;
          do (changed, e') <- S.move e' res arg;
          OK e'
      | _ => Error (msg "ill-formed copy")
      end
  | _ => Error (msg "non-special instruction")
  end.

Lemma type_special_op_incr:
  forall e op args res e' te,
    type_special_op e op args res = OK e' -> S.satisf te e' -> S.satisf te e.

Proof.

  intros ? [] * TYP SAT; simpl in TYP; try congruence.
  all:repeat (destruct args as [|? args]; try congruence; []).
  all:monadInv TYP.
  all:eauto using S.move_incr, S.set_incr, S.set_list_incr.
Qed.

Lemma type_special_op_sound:
  forall e op args res e' te,
  type_special_op e op args res = OK e' ->
  S.satisf te e' ->
  wt_special_op op (map te args) (te res).

Proof.

  intros ? [] * TYP SATISF; simpl in TYP; try congruence.
  all:repeat (destruct args as [|? args]; try congruence; []).
  all:monadInv TYP; simpl.
  - (* move *)
    eapply S.move_sound in EQ as <-; eauto. constructor.
  - (* copy *)
    eapply S.set_sound with (te:=te) in EQ as ->; eauto using S.move_incr.
    eapply S.move_sound in EQ1 as <-; eauto. constructor.
  - (* copyimm *)
    eapply S.move_sound in EQ as <-; eauto. constructor.
Qed.

Lemma type_special_op_complete:
  forall te e op args res,
    S.satisf te e ->
    wt_special_op op (map te args) (te res) ->
    exists e', type_special_op e op args res = OK e' /\ S.satisf te e'.

Proof.

  intros * SAT WT; inv WT; simpl.
  all:repeat (destruct args as [|? args]; simpl in *; try congruence; []).
  all:repeat (match goal with H:_::_ = _::_ |- _ => inv H end).
  - (* move *)
    edestruct S.move_complete as (?&?&->&?SAT); eauto; simpl.
    do 2 esplit; eauto.
  - (* copy *)
    edestruct S.set_complete as (?&->&?SAT); eauto; simpl.
    edestruct S.move_complete as (?&?&->&?SAT); eauto; simpl.
    do 2 esplit; eauto.
  - (* copyimm *)
    edestruct S.move_complete as (?&?&->&?SAT); eauto; simpl.
    do 2 esplit; eauto.
Qed.

Weak type soundness results for eval_operation: the result values, when defined, are always of the type predicted by type_of_operation.

Section SOUNDNESS.

Variable A V: Type.
Variable genv: Genv.t A V.

Remark type_add:
forall v1 v2, Val.has_type (Val.add v1 v2) Tint.

Proof.

intros. unfold Val.has_type, Val.add. destruct Archi.ptr64, v1, v2; auto.
Qed.

Remark type_addl:
forall v1 v2, Val.has_type (Val.addl v1 v2) Tlong.

Proof.

intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto.
Qed.

Remark type_mayundef:
forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) (snd (type_of_mayundef mu)).

Proof.

  intros. unfold eval_may_undef.
  destruct mu eqn:EQMU, v1, v2; simpl; auto.
  all: destruct Int.ltu; simpl; auto.
Qed.

Definition is_special_op op :=
  match op with
  | Omove | Ocopy | Ocopyimm _ => true
  | _ => false
  end.

Lemma type_of_operation_sound:
  forall op vl sp v m,
  is_special_op op = false ->
  eval_operation genv sp op vl m = Some v ->
  Val.has_type v (snd (type_of_operation op)).

Proof with

(try exact I; try reflexivity; auto using Val.Vptr_has_type).
  intros.
  destruct op; simpl; simpl in H0; FuncInv; subst; simpl in *; try congruence.
  (* welldef *)
  - apply Val.welldefined_type with (v:=v0); assumption.
  (* intconst, longconst, floatconst, singleconst *)
  - exact I.
  - exact I.
  - exact I.
  - exact I.
  (* addrsymbol *)
  - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)...
  (* addrstack *)
  - destruct sp... apply Val.Vptr_has_type.
  (* castsigned *)
  - destruct v0...
  - destruct v0...
  (* add, addimm *)
  - apply type_add.
  - apply type_add.
  (* neg, sub *)
  - destruct v0...
  - unfold Val.sub. destruct v0; destruct v1...
    unfold Val.has_type; destruct Archi.ptr64...
    destruct Archi.ptr64... destruct (eq_block b b0)...
  (* mul, mulhs, mulhu *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* div, divu *)
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int.eq i0 Int.zero
         || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial.
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int.eq i0 Int.zero); cbn; trivial.
  (* mod, modu *)
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int.eq i0 Int.zero
         || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial.
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int.eq i0 Int.zero); cbn; trivial.
  (* and, andimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* or, orimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* xor, xorimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* shl, shlimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
  (* shr, shrimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
  (* shru, shruimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
  (* shrx *)
  - destruct v0; cbn; trivial.
    destruct (Int.ltu n (Int.repr 31)); cbn; trivial.
  (* makelong, lowlong, highlong *)
  - destruct v0; destruct v1...
  - destruct v0...
  - destruct v0...
  (* cast32 *)
  - destruct v0...
  - destruct v0...
  (* addl, addlimm *)
  - apply type_addl.
  - apply type_addl.
  (* negl, subl *)
  - destruct v0...
  - unfold Val.subl. destruct v0; destruct v1...
    unfold Val.has_type; destruct Archi.ptr64...
    destruct Archi.ptr64... destruct (eq_block b b0)...
  (* mull, mullhs, mullhu *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* divl, divlu *)
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int64.eq i0 Int64.zero
         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
            Int64.eq i0 Int64.mone); cbn; trivial.
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int64.eq i0 Int64.zero); cbn; trivial.
  (* modl, modlu *)
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int64.eq i0 Int64.zero
         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
            Int64.eq i0 Int64.mone); cbn; trivial.
  - destruct v0; destruct v1; cbn; trivial.
    destruct (Int64.eq i0 Int64.zero); cbn; trivial.
  (* andl, andlimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* orl, orlimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* xorl, xorlimm *)
  - destruct v0; destruct v1...
  - destruct v0...
  (* shll, shllimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
  (* shr, shrimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
  (* shru, shruimm *)
  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
  (* shrxl *)
  - destruct v0; cbn; trivial.
    destruct (Int.ltu n (Int.repr 63)); cbn; trivial.
  (* negf, absf *)
  - destruct v0...
  - destruct v0...
  (* addf, subf *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* mulf, divf *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* sqrtf *)
  - destruct v0...
  (* negfs, absfs *)
  - destruct v0...
  - destruct v0...
  (* addfs, subfs *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* mulfs, divfs *)
  - destruct v0; destruct v1...
  - destruct v0; destruct v1...
  (* sqrtfs *)
  - destruct v0...
  (* singleoffloat, floatofsingle *)
  - destruct v0...
  - destruct v0...
  (* intoffloat, intuoffloat *)
  - destruct v0; cbn; trivial.
    destruct (Float.to_int f); cbn; trivial.
  - destruct v0; cbn; trivial.
    destruct (Float.to_intu f); cbn; trivial.
  (* floatofint, floatofintu *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* intofsingle, intuofsingle *)
  - destruct v0; cbn; trivial.
    destruct (Float32.to_int f); cbn; trivial.
  - destruct v0; cbn; trivial.
    destruct (Float32.to_intu f); cbn; trivial.
  (* singleofint, singleofintu *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* longoffloat, longuoffloat *)
  - destruct v0; cbn; trivial.
    destruct (Float.to_long f); cbn; trivial.
  - destruct v0; cbn; trivial.
    destruct (Float.to_longu f); cbn; trivial.
  (* floatoflong, floatoflongu *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* longofsingle, longuofsingle *)
  - destruct v0; cbn; trivial.
    destruct (Float32.to_long f); cbn; trivial.
  - destruct v0; cbn; trivial.
    destruct (Float32.to_longu f); cbn; trivial.
  (* singleoflong, singleoflongu *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* cmp *)
  - destruct (eval_condition cond vl m)... destruct b...
  (* OEseqw *)
  - destruct optR as [[]|]; simpl; unfold Val.cmp;
    destruct Val.cmp_bool... all: destruct b...
  (* OEsnew *)
  - destruct optR as [[]|]; simpl; unfold Val.cmp;
    destruct Val.cmp_bool... all: destruct b...
  (* OEsequw *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpu;
    destruct Val.cmpu_bool... all: destruct b...
  (* OEsneuw *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpu;
    destruct Val.cmpu_bool... all: destruct b...
  (* OEsltw *)
  - destruct optR as [[]|]; simpl; unfold Val.cmp;
    destruct Val.cmp_bool... all: destruct b...
  (* OEsltuw *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpu;
    destruct Val.cmpu_bool... all: destruct b...
  (* OEsltiw *)
  - unfold Val.cmp; destruct Val.cmp_bool...
    all: destruct b...
  (* OEsltiuw *)
  - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
  (* OEaddiw *)
  - destruct optR as [[]|]; simpl in *; trivial.
  - destruct optR as [[]|]; simpl in *; trivial;
    apply type_add.
  (* OEandiw *)
  - destruct v0...
  (* OEoriw *)
  - destruct v0...
  (* OExoriw *)
  - destruct v0...
  (* OEluiw *)
  - destruct (Int.ltu _ _); cbn; trivial.
  (* OEseql *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpl;
    destruct Val.cmpl_bool... all: destruct b...
  (* OEsnel *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpl;
    destruct Val.cmpl_bool... all: destruct b...
  (* OEsequl *)
  - destruct optR as [[]|]; simpl; unfold Val.cmplu;
    destruct Val.cmplu_bool... all: destruct b...
  (* OEsneul *)
  - destruct optR as [[]|]; simpl; unfold Val.cmplu;
    destruct Val.cmplu_bool... all: destruct b...
  (* OEsltl *)
  - destruct optR as [[]|]; simpl; unfold Val.cmpl;
    destruct Val.cmpl_bool... all: destruct b...
  (* OEsltul *)
  - destruct optR as [[]|]; simpl; unfold Val.cmplu;
    destruct Val.cmplu_bool... all: destruct b...
  (* OEsltil *)
  - unfold Val.cmpl; destruct Val.cmpl_bool...
    all: destruct b...
  (* OEsltiul *)
  - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
  (* OEaddil *)
  - destruct optR as [[]|]; simpl in *; trivial.
  - destruct optR as [[]|]; simpl in *; trivial;
    apply type_addl.
  (* OEandil *)
  - destruct v0...
  (* OEoril *)
  - destruct v0...
  (* OExoril *)
  - destruct v0...
  (* OEluil *)
  - simpl; trivial.
  (* OEloadli *)
  - trivial.
  (* OEmayundef *)
  - apply type_mayundef.
  (* OEfeqd *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float.cmp; cbn; auto.
  (* OEfltd *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float.cmp; cbn; auto.
  (* OEfled *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float.cmp; cbn; auto.
  (* OEfeqs *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float32.cmp; cbn; auto.
  (* OEflts *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float32.cmp; cbn; auto.
  (* OEfles *)
  - destruct v0; destruct v1; cbn; auto.
    destruct Float32.cmp; cbn; auto.
  (* Bits_of_single, float *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* single, float of bits *)
  - destruct v0; cbn; trivial.
  - destruct v0; cbn; trivial.
  (* selectl *)
  - destruct v0; cbn; trivial.
    destruct Int.eq; cbn.
    apply Val.normalize_type.
    destruct Int.eq; cbn; trivial.
    apply Val.normalize_type.
  (* getcanary *)
  - apply canary_has_type.
Qed.

Definition is_trapping_op (op : operation) :=
  match op with
  | Omove => false
  | Owelldef _ => true
  | _ => false
  end.

Definition args_of_operation op :=
  if eq_operation op Omove
  then 1%nat
  else List.length (fst (type_of_operation op)).

Lemma is_trapping_op_sound:
  forall op vl sp m,
    is_trapping_op op = false ->
    (List.length vl) = args_of_operation op ->
    eval_operation genv sp op vl m <> None.

Proof.

  unfold args_of_operation.
  destruct op eqn:E; destruct eq_operation; intros; simpl in *; try congruence.
  all: try (destruct vl as [ | vh1 vl1]; try discriminate).
  all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
  all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
  all: try (destruct vl3 as [ | vh4 vl4]; try discriminate).
  all: try destruct optR as [[]|]; simpl in H0; try discriminate.
  all: try destruct Archi.ptr64; simpl in *; try discriminate.
  all: try destruct mu; simpl in *; try discriminate.
Qed.

Lemma wt_exec_special_op:
  forall sp op targs tres args m v,
  wt_special_op op targs tres ->
  eval_operation genv sp op args m = Some v ->
  list_forall2 Val.has_type args targs ->
  Val.has_type v tres.

Proof.

  inversion 1; subst; intros * EVAL WTREGS; simpl in *.
  all:repeat (destruct args as [|? args]; simpl in *; try congruence; []).
  all:repeat (match goal with
              | H:list_forall2 _ (_::_) _ |- _ => inv H
              | H: Some _ = Some _ |- _ => inv H
              end); auto.
  (* - (* select *) *)
  (*   unfold Val.select. destruct eval_condition as [[]|]; auto. *)
  (*   constructor. *)
Qed.

End SOUNDNESS.

Manipulating and transforming operations

Recognition of move operations.

Definition is_move_operation
    (A: Type) (op: operation) (args: list A) : option A :=
  match op, args with
  | Omove, arg :: nil => Some arg
  | _, _ => None
  end.

Lemma is_move_operation_correct:
  forall (A: Type) (op: operation) (args: list A) (a: A),
  is_move_operation op args = Some a ->
  op = Omove /\ args = a :: nil.

Proof.

  intros until a. unfold is_move_operation; destruct op;
  try (intros; discriminate).
  destruct args. intros; discriminate.
  destruct args. intros. intuition congruence.
  intros; discriminate.
Qed.

negate_condition cond returns a condition that is logically equivalent to the negation of cond.

Proof.

  intros. destruct cond; simpl.
  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
  repeat (destruct vl; auto).
  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto.
  repeat (destruct vl; auto).
  repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.

  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|];
  apply Val.negate_cmp_bool.
  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|];
  apply Val.negate_cmp_bool.
  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|];
  apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|];
  apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|];
  apply Val.negate_cmp_bool.
  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|];
  apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|];
  apply Val.negate_cmp_bool.
  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|];
  apply Val.negate_cmpu_bool.
  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|];
  apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|];
  apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|];
  apply Val.negate_cmplu_bool.
  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|];
  apply Val.negate_cmplu_bool.
  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|];
  apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|];
  apply Val.negate_cmplu_bool.
  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|];
  apply Val.negate_cmpl_bool.
  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|];
  apply Val.negate_cmplu_bool.
Qed.

Shifting stack-relative references. This is used in Stacking.

Definition shift_stack_addressing (delta: Z) (addr: addressing) :=
  match addr with
  | Ainstack ofs => Ainstack (Ptrofs.add ofs (Ptrofs.repr delta))
  | _ => addr
  end.

Definition shift_stack_operation (delta: Z) (op: operation) :=
  match op with
  | Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta))
  | _ => op
  end.

Lemma type_shift_stack_addressing:
  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.

Proof.

intros. destruct addr; auto.
Qed.

Lemma type_shift_stack_operation:
forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.

Proof.

intros. destruct op; auto;
try destruct optR as [[]|]; simpl; auto.
Qed.

Lemma eval_shift_stack_addressing:
  forall F V (ge: Genv.t F V) sp addr vl delta,
  eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
  eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl.

Proof.

intros. destruct addr; simpl; auto. destruct vl; auto.
rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
Qed.

Lemma eval_shift_stack_operation:
  forall F V (ge: Genv.t F V) sp op vl m delta,
  eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m =
  eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.

Proof.

intros. destruct op eqn:E; simpl; auto; destruct vl; auto.
rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
Qed.

Offset an addressing mode addr by a quantity delta, so that it designates the pointer delta bytes past the pointer designated by addr. May be undefined, in which case None is returned.

Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
  match addr with
  | Aindexed n => Some(Aindexed (Ptrofs.add n (Ptrofs.repr delta)))
  | Aglobal id n => Some(Aglobal id (Ptrofs.add n (Ptrofs.repr delta)))
  | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta)))
  end.

Lemma eval_offset_addressing:
  forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
  offset_addressing addr delta = Some addr' ->
  eval_addressing ge sp addr args = Some v ->
  Archi.ptr64 = false ->
  eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))).

Proof.

  intros.
  assert (A: forall x n,
             Val.offset_ptr x (Ptrofs.add n (Ptrofs.repr delta)) =
             Val.add (Val.offset_ptr x n) (Vint (Int.repr delta))).
  { intros; destruct x; simpl; auto. rewrite H1.
    rewrite Ptrofs.add_assoc. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. }
  destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
- rewrite A; auto.
- unfold Genv.symbol_address. destruct (Genv.find_symbol ge q); auto.
  simpl. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs.
- rewrite A; auto.
Qed.

Operations that are so cheap to recompute that CSE should not factor them out.

Operations that depend on the memory state.

Proof.

  intros until m2.
  destruct cond; cbn; try congruence.
  all: unfold Val.cmpu_bool, Val.cmplu_bool.
  all: destruct Archi.ptr64; cbn; intro SF; try discriminate.
  all: reflexivity.
Qed.

Lemma op_depends_on_memory_correct:
  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
  op_depends_on_memory op = false ->
  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.

Proof.

  intros until m2. destruct op; simpl; try congruence.
  intro DEPEND.
  f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
  all: intros; repeat (destruct args; auto);
       unfold Val.cmpu, Val.cmpu_bool, Val.cmplu, Val.cmplu_bool;
       try destruct optR as [[]|]; simpl;
       destruct v; try destruct v0; simpl; auto;
       try apply negb_false_iff in H; try rewrite H; auto.
Qed.

Lemma cond_valid_pointer_eq:
  forall cond args m1 m2,
  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
  eval_condition cond args m1 = eval_condition cond args m2.

Proof.

  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
  all: repeat (destruct args; simpl; try congruence);
       try destruct optR as [[]|]; simpl;
       try destruct v, v0; try rewrite !MEM; auto;
       try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
Qed.

Lemma op_valid_pointer_eq:
  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.

Proof.

  intros until m2. destruct op; simpl; try congruence.
  intro MEM; erewrite cond_valid_pointer_eq; eauto.
  all: intros MEM; repeat (destruct args; simpl; try congruence);
       try destruct optR as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto;
       unfold Val.cmpu, Val.cmplu;
       erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
Qed.

Global variables mentioned in an operation or addressing mode

Definition globals_addressing (addr: addressing) : list qualident :=
  match addr with
  | Aglobal s ofs => s :: nil
  | _ => nil
  end.

Definition globals_operation (op: operation) : list qualident :=
  match op with
  | Oaddrsymbol s ofs => s :: nil
  | _ => nil
  end.

Invariance and compatibility properties.

eval_operation and eval_addressing depend on a global environment for resolving references to global symbols. We show that they give the same results if a global environment is replaced by another that assigns the same addresses to the same symbols.

Section GENV_TRANSF.

Variable F1 F2 V1 V2: Type.
Variable ge1: Genv.t F1 V1.
Variable ge2: Genv.t F2 V2.
Hypothesis agree_on_symbols:
  forall (s: qualident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.

Lemma eval_addressing_preserved:
  forall sp addr vl,
  eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.

Proof.

  intros.
  unfold eval_addressing; destruct addr; auto. destruct vl; auto.
  unfold Genv.symbol_address. rewrite agree_on_symbols; auto.
Qed.

Lemma eval_operation_preserved:
forall sp op vl m,
eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.

Proof.

  intros.
  unfold eval_operation; destruct op; auto. destruct vl; auto.
  unfold Genv.symbol_address. rewrite agree_on_symbols; auto.
Qed.

End GENV_TRANSF.

Compatibility of the evaluation functions with value injections.

Section EVAL_COMPAT.

Variable F1 F2 V1 V2: Type.
Variable ge1: Genv.t F1 V1.
Variable ge2: Genv.t F2 V2.
Variable f: meminj.

Variable m1: mem.
Variable m2: mem.

Hypothesis valid_pointer_inj:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Hypothesis weak_valid_pointer_inj:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Hypothesis weak_valid_pointer_no_overflow:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Hypothesis valid_different_pointers_inj:
  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  b1 <> b2 ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).

Ltac InvInject :=
  match goal with
  | [ H: Val.inject _ (Vint _) _ |- _ ] =>
      inv H; InvInject
  | [ H: Val.inject _ (Vfloat _) _ |- _ ] =>
      inv H; InvInject
  | [ H: Val.inject _ (Vptr _ _) _ |- _ ] =>
      inv H; InvInject
  | [ H: Val.inject_list _ nil _ |- _ ] =>
      inv H; InvInject
  | [ H: Val.inject_list _ (_ :: _) _ |- _ ] =>
      inv H; InvInject
  | _ => idtac
  end.

Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0',
  Val.inject f v v' ->
  Val.inject f v0 v0' ->
  Val.cmpu_bool (Mem.valid_pointer m1) c v v0 = Some b ->
  Val.cmpu_bool (Mem.valid_pointer m2) c v' v0' = Some b.

Proof.

intros.
eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
Qed.

Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0,
  Val.inject f v v' ->
  Val.inject f v0 v'0 ->
  Val.inject f (Val.cmpu (Mem.valid_pointer m1) c v v0)
  (Val.cmpu (Mem.valid_pointer m2) c v' v'0).

Proof.

  intros until v'0. intros HV1 HV2.
  unfold Val.cmpu;
  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto.
  exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
  intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.

Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR,
  Val.inject f v v' ->
  Val.inject f v0 v'0 ->
  Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
  (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32).

Proof.

  intros until optR. intros HV1 HV2.
  destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu;
  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto;
  assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int.
  + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
  + exploit eval_cmpu_bool_inj'. eapply HV1. instantiate (1:=v'0).
    eauto. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.

Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0',
  Val.inject f v v' ->
  Val.inject f v0 v0' ->
  Val.cmplu_bool (Mem.valid_pointer m1) c v v0 = Some b ->
  Val.cmplu_bool (Mem.valid_pointer m2) c v' v0' = Some b.

Proof.

intros.
eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
Qed.

Lemma eval_cmplu_bool_inj: forall c v v' v0 v'0,
  Val.inject f v v' ->
  Val.inject f v0 v'0 ->
  Val.inject f (Val.maketotal (Val.cmplu (Mem.valid_pointer m1) c v v0))
  (Val.maketotal (Val.cmplu (Mem.valid_pointer m2) c v' v'0)).

Proof.

  intros until v'0. intros HV1 HV2.
  unfold Val.cmplu;
  destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto.
  exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
  intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.

Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR,
  Val.inject f v v' ->
  Val.inject f v0 v'0 ->
  Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64))
  (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)).

Proof.

  intros until optR. intros HV1 HV2.
  destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu;
  destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto;
  assert (HVI: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long.
  + exploit eval_cmplu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
  + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
  + exploit eval_cmplu_bool_inj'. eapply HV1. instantiate (1:=v'0).
    eauto. eapply Heqo.
    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.

Lemma eval_condition_inj:
  forall cond vl1 vl2 b,
  Val.inject_list f vl1 vl2 ->
  eval_condition cond vl1 m1 = Some b ->
  eval_condition cond vl2 m2 = Some b.

Proof.

  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
  all: assert (HVI32: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int;
       assert (HVI64: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long;
       try unfold zero32, zero64.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
- inv H3; simpl in H0; inv H0; auto.
- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
- inv H3; simpl in H0; inv H0; auto.
- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmpu_bool_inj'; eauto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmpu_bool_inj'; eauto.
- destruct optR as [[]|]; simpl;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmpu_bool_inj'; eauto.
- destruct optR as [[]|]; simpl;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmpu_bool_inj'; eauto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmplu_bool_inj'; eauto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmplu_bool_inj'; eauto.
- destruct optR as [[]|]; simpl;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmplu_bool_inj'; eauto.
- destruct optR as [[]|]; simpl;
  inv H3; inv H2; simpl in H0; inv H0; auto.
- destruct optR as [[]|]; unfold apply_bin_oreg in *;
  eapply eval_cmplu_bool_inj'; eauto.
Qed.

Ltac TrivialExists :=
  match goal with
  | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
      exists v1; split; auto
  | _ => idtac
  end.

Lemma eval_operation_inj:
  forall op sp1 vl1 sp2 vl2 v1,
  (forall id ofs,
      In id (globals_operation op) ->
      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
  Val.inject f sp1 sp2 ->
  Val.inject_list f vl1 vl2 ->
  eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2.

Proof.

  intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
  (* welldef *)
  - apply Val.welldefined_inject with (v1:=v); auto.
  (* addrsymbol *)
  - apply GL; simpl; auto.
  (* addrstack *)
  - apply Val.offset_ptr_inject; auto.
  (* castsigned *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* add, addimm *)
  - apply Val.add_inject; auto.
  - apply Val.add_inject; auto.
  (* neg, sub *)
  - inv H4; simpl; auto.
  - apply Val.sub_inject; auto.
  (* mul, mulhs, mulhu *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* div, divu *)
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int.eq i0 Int.zero
              || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_int.
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int.eq i0 Int.zero); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_int.
  (* mod, modu *)
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int.eq i0 Int.zero
              || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_int.
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int.eq i0 Int.zero); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_int.
  (* and, andimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* or, orimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* xor, xorimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* shl, shlimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
  (* shr, shrimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
  (* shru, shruimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
  (* shrx *)
  - inv H4; cbn; try apply Val.val_inject_undef.
    destruct (Int.ltu n (Int.repr 31)); cbn.
    apply Val.inject_int.
    apply Val.val_inject_undef.
  (* makelong, highlong, lowlong *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* cast32 *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* addl, addlimm *)
  - apply Val.addl_inject; auto.
  - apply Val.addl_inject; auto.
  (* negl, subl *)
  - inv H4; simpl; auto.
  - apply Val.subl_inject; auto.
  (* mull, mullhs, mullhu *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* divl, divlu *)
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int64.eq i0 Int64.zero
         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
            Int64.eq i0 Int64.mone); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_long.
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int64.eq i0 Int64.zero); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_long.
  (* modl, modlu *)
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int64.eq i0 Int64.zero
         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
            Int64.eq i0 Int64.mone); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_long.
  - inv H4; inv H2; cbn.
    all: try apply Val.val_inject_undef.
    destruct (Int64.eq i0 Int64.zero); cbn.
    apply Val.val_inject_undef.
    apply Val.inject_long.
  (* andl, andlimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* orl, orlimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* xorl, xorlimm *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; simpl; auto.
  (* shll, shllimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
  (* shr, shrimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
  (* shru, shruimm *)
  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
  (* shrx *)
  - inv H4; cbn; try apply Val.val_inject_undef.
    destruct (Int.ltu n (Int.repr 63)); cbn.
    apply Val.inject_long.
    apply Val.val_inject_undef.
  (* negf, absf *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* addf, subf *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* mulf, divf *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* sqrtf *)
  - inv H4; simpl; auto.
  (* negfs, absfs *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* addfs, subfs *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* mulfs, divfs *)
  - inv H4; inv H2; simpl; auto.
  - inv H4; inv H2; simpl; auto.
  (* sqrtfs *)
  - inv H4; simpl; auto.
  (* singleoffloat, floatofsingle *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* intoffloat, intuoffloat *)
  - inv H4; cbn; auto.
    destruct (Float.to_int f0); cbn; auto.
  - inv H4; cbn; auto.
    destruct (Float.to_intu f0); cbn; auto.
  (* floatofint, floatofintu *)
  - inv H4; cbn; auto.
  - inv H4; cbn; auto.
  (* intofsingle, intuofsingle *)
  - inv H4; cbn; auto.
    destruct (Float32.to_int f0); cbn; auto.
  - inv H4; cbn; auto.
    destruct (Float32.to_intu f0); cbn; auto.
  (* singleofint, singleofintu *)
  - inv H4; cbn; auto.
  - inv H4; cbn; auto.
  (* longoffloat, longuoffloat *)
  - inv H4; cbn; auto.
    destruct (Float.to_long f0); cbn; auto.
  - inv H4; cbn; auto.
    destruct (Float.to_longu f0); cbn; auto.
  (* floatoflong, floatoflongu *)
  - inv H4; cbn; auto.
  - inv H4; cbn; auto.
  (* longofsingle, longuofsingle *)
  - inv H4; cbn; auto.
    destruct (Float32.to_long f0); cbn; auto.
  - inv H4; cbn; auto.
    destruct (Float32.to_longu f0); cbn; auto.
  (* singleoflong, singleoflongu *)
  - inv H4; cbn; auto.
  - inv H4; cbn; auto.
  (* cmp *)
  - subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
    exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
    destruct b; simpl; constructor.
    simpl; constructor.
  (* OEseqw *)
  - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp;
    inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsnew *)
  - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp;
    inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsequw *)
  - apply eval_cmpu_bool_inj_opt; auto.
  (* OEsneuw *)
  - apply eval_cmpu_bool_inj_opt; auto.
  (* OEsltw *)
  - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp;
    inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsltuw *)
  - apply eval_cmpu_bool_inj_opt; auto.
  (* OEsltiw *)
  - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
  (* OEsltiuw *)
  - apply eval_cmpu_bool_inj; auto.
  (* OEaddiw *)
  - destruct optR as [[]|]; auto; simpl.
    rewrite Int.add_zero_l; auto.
    rewrite Int.add_commut, Int.add_zero_l; auto.
  - destruct optR as [[]|]; auto; simpl;
    eapply Val.add_inject; auto.
  (* OEandiw *)
  - inv H4; cbn; auto.
  (* OEoriw *)
  - inv H4; cbn; auto.
  (* OExoriw *)
  - inv H4; simpl; auto.
  (* OEluiw *)
  - destruct (Int.ltu _ _); auto.
  (* OEseql *)
  - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl;
    inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsnel *)
  - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl;
    inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsequl *)
  - apply eval_cmplu_bool_inj_opt; auto.
  (* OEsneul *)
  - apply eval_cmplu_bool_inj_opt; auto.
  (* OEsltl *)
  - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl;
    inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto;
    try apply Val.inject_int.
  (* OEsltul *)
  - apply eval_cmplu_bool_inj_opt; auto.
  (* OEsltil *)
  - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int.
  (* OEsltiul *)
  - apply eval_cmplu_bool_inj; auto.
  (* OEaddil *)
  - destruct optR as [[]|]; auto; simpl.
    rewrite Int64.add_zero_l; auto.
    rewrite Int64.add_commut, Int64.add_zero_l; auto.
  - destruct optR as [[]|]; auto; simpl;
    eapply Val.addl_inject; auto.
  (* OEandil *)
  - inv H4; cbn; auto.
  (* OEoril *)
  - inv H4; cbn; auto.
  (* OExoril *)
  - inv H4; simpl; auto.
  (* OEmayundef *)
  - destruct mu; inv H4; inv H2; simpl; auto;
    try destruct (Int.ltu _ _); simpl; auto.
    all: eapply Val.inject_ptr; eauto.
  (* OEfeqd *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* OEfltd *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* OEfled *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* OEfeqs *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* OEflts *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* OEfles *)
  - inv H4; inv H2; cbn; simpl; auto.
    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
  (* Bits_of_single, double *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* single, double of bits *)
  - inv H4; simpl; auto.
  - inv H4; simpl; auto.
  (* selectl *)
  - inv H4; trivial. cbn.
    destruct (Int.eq i Int.one).
    + auto using Val.normalize_inject.
    + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject.
  (* getcanary *)
  - apply canary_inject.
Qed.

Lemma eval_addressing_inj:
  forall addr sp1 vl1 sp2 vl2 v1,
  (forall id ofs,
      In id (globals_addressing addr) ->
      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
  Val.inject f sp1 sp2 ->
  Val.inject_list f vl1 vl2 ->
  eval_addressing ge1 sp1 addr vl1 = Some v1 ->
  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.

Proof.

  intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
  apply Val.offset_ptr_inject; auto.
  apply H; simpl; auto.
  apply Val.offset_ptr_inject; auto.
Qed.

Lemma eval_addressing_inj_none:
  forall addr sp1 vl1 sp2 vl2,
  (forall id ofs,
      In id (globals_addressing addr) ->
      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
  Val.inject f sp1 sp2 ->
  Val.inject_list f vl1 vl2 ->
  eval_addressing ge1 sp1 addr vl1 = None ->
  eval_addressing ge2 sp2 addr vl2 = None.

Proof.

  intros until vl2. intros Hglobal Hinjsp Hinjvl.
  destruct addr; simpl in *;
  inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate.
Qed.

End EVAL_COMPAT.

Compatibility of the evaluation functions with the ``is less defined'' relation over values.

Section EVAL_LESSDEF.

Variable F V: Type.
Variable genv: Genv.t F V.

Remark valid_pointer_extends:
  forall m1 m2, Mem.extends m1 m2 ->
  forall b1 ofs b2 delta,
  Some(b1, 0) = Some(b2, delta) ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Proof.

intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto.
Qed.

Remark weak_valid_pointer_extends:
  forall m1 m2, Mem.extends m1 m2 ->
  forall b1 ofs b2 delta,
  Some(b1, 0) = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Proof.

intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
Qed.

Remark weak_valid_pointer_no_overflow_extends:
  forall m1 b1 ofs b2 delta,
  Some(b1, 0) = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Proof.

intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
Qed.

Remark valid_different_pointers_extends:
  forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  b1 <> b2 ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
  Some(b1, 0) = Some (b1', delta1) ->
  Some(b2, 0) = Some (b2', delta2) ->
  b1' <> b2' \/
  Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)).

Proof.

intros. inv H2; inv H3. auto.
Qed.

Lemma eval_condition_lessdef:
  forall cond vl1 vl2 b m1 m2,
  Val.lessdef_list vl1 vl2 ->
  Mem.extends m1 m2 ->
  eval_condition cond vl1 m1 = Some b ->
  eval_condition cond vl2 m2 = Some b.

Proof.

  intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
  apply valid_pointer_extends; auto.
  apply weak_valid_pointer_extends; auto.
  apply weak_valid_pointer_no_overflow_extends.
  apply valid_different_pointers_extends; auto.
  rewrite <- val_inject_list_lessdef. eauto. auto.
Qed.

Lemma eval_operation_lessdef:
  forall sp op vl1 vl2 v1 m1 m2,
  Val.lessdef_list vl1 vl2 ->
  Mem.extends m1 m2 ->
  eval_operation genv sp op vl1 m1 = Some v1 ->
  exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.

Proof.

  intros. rewrite val_inject_list_lessdef in H.
  assert (exists v2 : val,
          eval_operation genv sp op vl2 m2 = Some v2
          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
  eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
  apply valid_pointer_extends; auto.
  apply weak_valid_pointer_extends; auto.
  apply weak_valid_pointer_no_overflow_extends.
  apply valid_different_pointers_extends; auto.
  intros. apply val_inject_lessdef. auto.
  apply val_inject_lessdef; auto.
  eauto.
  auto.
  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
Qed.

Lemma eval_addressing_lessdef:
  forall sp addr vl1 vl2 v1,
  Val.lessdef_list vl1 vl2 ->
  eval_addressing genv sp addr vl1 = Some v1 ->
  exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2.

Proof.

  intros. rewrite val_inject_list_lessdef in H.
  assert (exists v2 : val,
          eval_addressing genv sp addr vl2 = Some v2
          /\ Val.inject (fun b => Some(b, 0)) v1 v2).
  eapply eval_addressing_inj with (sp1 := sp).
  intros. rewrite <- val_inject_lessdef; auto.
  rewrite <- val_inject_lessdef; auto.
  eauto. auto.
  destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
Qed.

Lemma eval_addressing_lessdef_none:
  forall sp addr vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  eval_addressing genv sp addr vl1 = None ->
  eval_addressing genv sp addr vl2 = None.

Proof.

  intros until vl2. intros Hlessdef Heval1.
  destruct addr; simpl in *;
  inv Hlessdef; trivial; try discriminate;
  inv H0; trivial; try discriminate;
  inv H2; trivial; try discriminate.
Qed.

End EVAL_LESSDEF.

Compatibility of the evaluation functions with memory injections.

Section EVAL_INJECT.

Variable F V: Type.
Variable genv: Genv.t F V.
Variable f: meminj.
Hypothesis globals: meminj_preserves_globals genv f.
Variable sp1: block.
Variable sp2: block.
Variable delta: Z.
Hypothesis sp_inj: f sp1 = Some(sp2, delta).

Remark symbol_address_inject:
forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).

Proof.

  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
  exploit (proj1 globals); eauto. intros.
  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
Qed.

Lemma eval_condition_inject:
  forall cond vl1 vl2 b m1 m2,
  Val.inject_list f vl1 vl2 ->
  Mem.inject f m1 m2 ->
  eval_condition cond vl1 m1 = Some b ->
  eval_condition cond vl2 m2 = Some b.

Proof.

  intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
  intros; eapply Mem.valid_pointer_inject_val; eauto.
  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
  intros; eapply Mem.different_pointers_inject; eauto.
Qed.

Lemma eval_addressing_inject:
  forall addr vl1 vl2 v1,
  Val.inject_list f vl1 vl2 ->
  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 ->
  exists v2,
     eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2
  /\ Val.inject f v1 v2.

Proof.

  intros.
  rewrite eval_shift_stack_addressing.
  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
  intros. apply symbol_address_inject.
  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
Qed.

Lemma eval_addressing_inject_none:
  forall addr vl1 vl2,
  Val.inject_list f vl1 vl2 ->
  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None ->
  eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None.

Proof.

  intros.
  rewrite eval_shift_stack_addressing.
  eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
  intros. apply symbol_address_inject.
  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
Qed.

Lemma eval_operation_inject:
  forall op vl1 vl2 v1 m1 m2,
  Val.inject_list f vl1 vl2 ->
  Mem.inject f m1 m2 ->
  eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 ->
  exists v2,
     eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2
  /\ Val.inject f v1 v2.

Proof.

  intros.
  rewrite eval_shift_stack_operation. simpl.
  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
  intros; eapply Mem.valid_pointer_inject_val; eauto.
  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
  intros; eapply Mem.different_pointers_inject; eauto.
  intros. apply symbol_address_inject.
  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
Qed.

End EVAL_INJECT.

Handling of builtin arguments

Definition builtin_arg_ok_1
       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
  match c, ba with
  | OK_all, _ => true
  | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true
  | OK_addrstack, BA_addrstack _ => true
  | OK_addressing, BA_addrstack _ => true
  | OK_addressing, BA_addptr (BA _) (BA_int _) => true
  | OK_addressing, BA_addptr (BA _) (BA_long _) => true
  | _, _ => false
  end.

Definition builtin_arg_ok
       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
  match ba with
  | (BA _ | BA_splitlong (BA _) (BA _)) => true
  | _ => builtin_arg_ok_1 ba c
  end.

Definition getcanary : option operation := Some Ogetcanary.
Definition clearcanary := if Archi.canary64 then Olongconst Int64.zero else Ointconst Int.zero.
Definition canary_cmp := if Archi.canary64 then Ccomplu Ceq else Ccompu Ceq.

Module Op

Evaluation functions

Static typing of conditions, operators and addressing modes.

Manipulating and transforming operations

Invariance and compatibility properties.

Handling of builtin arguments