Module Op

Require Import Coqlib.
Require Import Ast.
Require Import Integers.
Require Import Floats.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Events.

Set Implicit Arguments.

Inductive atomic_statement : Type :=
  | AScas: atomic_statement (* compare and swap *)
  | ASlkinc: atomic_statement. (* locked increment *)


Inductive condition : Type :=
  | Ccomp: comparison -> condition (* signed integer comparison *)
  | Ccompu: comparison -> condition (* unsigned integer comparison *)
  | Ccompimm: comparison -> int -> condition (* signed integer comparison with a constant *)
  | Ccompuimm: comparison -> int -> condition (* unsigned integer comparison with a constant *)
  | Ccompf: comparison -> condition (* floating-point comparison *)
  | Cnotcompf: comparison -> condition (* negation of a floating-point comparison *)
  | Cmaskzero: int -> condition (* test (arg & constant) == 0 *)
  | Cmasknotzero: int -> condition. (* test (arg & constant) != 0 *)


Inductive addressing: Type :=
  | Aindexed: int -> addressing (* Address is r1 + offset *)
  | Aindexed2: int -> addressing (* Address is r1 + r2 + offset *)
  | Ascaled: int -> int -> addressing (* Address is r1 * scale + offset *)
  | Aindexed2scaled: int -> int -> addressing
  | Aindexed2scaledrev: int -> int -> addressing
  | Aglobal: ident -> int -> addressing (* Address is symbol + offset *)
  | Abased: ident -> int -> addressing (* Address is symbol + offset + r1 *)
  | Abasedscaled: int -> ident -> int -> addressing (* Address is symbol + offset + r1 * scale *)
  | Ainstack: int -> addressing. (* Address is stack_pointer + offset *)


Inductive operation : Type :=
  | Omove: operation (* rd = r1 *)
  | Ointconst: int -> operation (* rd is set to the given integer constant *)
  | Ofloatconst: float -> operation (* rd is set to the given float constant *)
  | Ocast8signed: operation (* rd is 8-bit sign extension of r1 *)
  | Ocast8unsigned: operation (* rd is 8-bit zero extension of r1 *)
  | Ocast16signed: operation (* rd is 16-bit sign extension of r1 *)
  | Ocast16unsigned: operation (* rd is 16-bit zero extension of r1 *)
  | Oneg: operation (* rd = - r1 *)
  | Osub: operation (* rd = r1 - r2 *)
  | Omul: operation (* rd = r1 * r2 *)
  | Omulimm: int -> operation (* rd = r1 * n *)
  | Odiv: operation (* rd = r1 / r2 (signed) *)
  | Odivu: operation (* rd = r1 / r2 (unsigned) *)
  | Omod: operation (* rd = r1 % r2 (signed) *)
  | Omodu: operation (* rd = r1 % r2 (unsigned) *)
  | Oand: operation (* rd = r1 & r2 *)
  | Oandimm: int -> operation (* rd = r1 & n *)
  | Oor: operation (* rd = r1 | r2 *)
  | Oorimm: int -> operation (* rd = r1 | n *)
  | Oxor: operation (* rd = r1 ^ r2 *)
  | Oxorimm: int -> operation (* rd = r1 ^ n *)
  | Oshl: operation (* rd = r1 << r2 *)
  | Oshlimm: int -> operation (* rd = r1 << n *)
  | Oshr: operation (* rd = r1 >> r2 (signed) *)
  | Oshrimm: int -> operation (* rd = r1 >> n (signed) *)
  | Oshrximm: int -> operation (* rd = r1 / 2^n (signed) *)
  | Oshru: operation (* rd = r1 >> r2 (unsigned) *)
  | Oshruimm: int -> operation (* rd = r1 >> n (unsigned) *)
  | Ororimm: int -> operation (* rotate right immediate *)
  | Olea: addressing -> operation (* effective address *)
  | Onegf: operation (* rd = - r1 *)
  | Oaddf: operation (* rd = r1 + r2 *)
  | Osubf: operation (* rd = r1 - r2 *)
  | Omulf: operation (* rd = r1 * r2 *)
  | Odivf: operation (* rd = r1 / r2 *)
  | Osingleoffloat: operation (* rd is r1 truncated to single-precision float *)
  | Ointoffloat: operation (* rd = signed_int_of_float(r1) *)
  | Ofloatofint: operation (* rd = float_of_signed_int(r1) *)
  | Ointuoffloat: operation (* rd = unsigned_int_of_float(r1) *)
  | Ofloatofintu: operation (* rd = float_of_unsigned_int(r1) *)
  | Ocmp: condition -> operation. (* rd = 1 if condition holds, rd = 0 otherwise. *)


Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs).
Definition Oaddimm (n: int) : operation := Olea (Aindexed n).


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

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


Definition eval_compare_mismatch (c: comparison) : option bool :=
  match c with Ceq => Some false | Cne => Some true | _ => None end.

Definition eval_compare_null (c: comparison) (n: int) : option bool :=
  if Int.eq n Int.zero then eval_compare_mismatch c else None.

Definition eval_condition (cond: condition) (vl: list val):
               option bool :=
  match cond, vl with
  | Ccomp c, Vint n1 :: Vint n2 :: nil =>
      Some (Int.cmp c n1 n2)
   | Ccomp c, Vptr p1 :: Vptr p2 :: nil =>
    Val.option_bool_of_bool3 (Ptr.cmp c p1 p2)
  | Ccomp c, Vptr _ :: Vint n2 :: nil =>
      eval_compare_null c n2
  | Ccomp c, Vint n1 :: Vptr _ :: nil =>
      eval_compare_null c n1
  | Ccompu c, Vint n1 :: Vint n2 :: nil =>
      Some (Int.cmpu c n1 n2)
  | Ccompu c, Vptr p1 :: Vptr p2 :: nil =>
      Val.option_bool_of_bool3 (Ptr.cmpu c p1 p2)
  | Ccompimm c n, Vint n1 :: nil =>
      Some (Int.cmp c n1 n)
  | Ccompimm c n, Vptr _ :: nil =>
      eval_compare_null c n
  | Ccompuimm c n, Vint n1 :: nil =>
      Some (Int.cmpu c n1 n)
  | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
      Some (Float.cmp c f1 f2)
  | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil =>
      Some (negb (Float.cmp c f1 f2))
  | Cmaskzero n, Vint n1 :: nil =>
      Some (Int.eq (Int.and n1 n) Int.zero)
  | Cmasknotzero n, Vint n1 :: nil =>
      Some (negb (Int.eq (Int.and n1 n) Int.zero))
  | _, _ =>
      None
  end.

Definition offset_sp (sp: option pointer) (delta: int) : option val :=
  match sp with
  | Some ptr => Some (Vptr (Ptr.add ptr delta))
  | _ => None
  end.

Definition eval_addressing
    (F: Type) (genv: Genv.t F) (sp: option pointer)
    (addr: addressing) (vl: list val) : option val :=
  match addr, vl with
  | Aindexed n, Vint n1 :: nil =>
      Some (Vint (Int.add n1 n))
  | Aindexed n, Vptr (Ptr b1 n1) :: nil =>
      Some (Vptr (Ptr b1 (Int.add n1 n)))
  | Aindexed2 n, Vint n1 :: Vint n2 :: nil =>
      Some (Vint (Int.add (Int.add n1 n2) n))
  | Aindexed2 n, Vptr (Ptr b1 n1) :: Vint n2 :: nil =>
      Some (Vptr (Ptr b1 (Int.add (Int.add n1 n2) n)))
  | Aindexed2 n, Vint n1 :: Vptr (Ptr b2 n2) :: nil =>
      Some (Vptr (Ptr b2 (Int.add (Int.add n2 n1) n)))
  | Ascaled sc ofs, Vint n1 :: nil =>
      Some (Vint (Int.add (Int.mul n1 sc) ofs))
  | Aindexed2scaled sc ofs, Vint n1 :: Vint n2 :: nil =>
      Some (Vint (Int.add n1 (Int.add (Int.mul n2 sc) ofs)))
  | Aindexed2scaled sc ofs, Vptr (Ptr b1 n1) :: Vint n2 :: nil =>
      Some (Vptr (Ptr b1 (Int.add n1 (Int.add (Int.mul n2 sc) ofs))))
  | Aindexed2scaledrev sc ofs, Vint n2 :: Vint n1 :: nil =>
      Some (Vint (Int.add n1 (Int.add (Int.mul n2 sc) ofs)))
  | Aindexed2scaledrev sc ofs, Vint n2 :: Vptr (Ptr b1 n1) :: nil =>
      Some (Vptr (Ptr b1 (Int.add n1 (Int.add (Int.mul n2 sc) ofs))))
  | Aglobal s ofs, nil =>
      match Genv.find_symbol genv s with
      | None => None
      | Some p => Some (Vptr (Ptr.add p ofs))
      end
  | Abased s ofs, Vint n1 :: nil =>
      match Genv.find_symbol genv s with
      | None => None
      | Some p => Some (Vptr (Ptr.add p (Int.add ofs n1)))
      end
  | Abasedscaled sc s ofs, Vint n1 :: nil =>
      match Genv.find_symbol genv s with
      | None => None
      | Some p => Some (Vptr (Ptr.add p (Int.add ofs (Int.mul n1 sc))))
      end
  | Ainstack ofs, nil =>
      offset_sp sp ofs
  | _, _ => None
  end.

Definition eval_operation
    (F: Type) (genv: Genv.t F) (sp: option pointer)
    (op: operation) (vl: list val): option val :=
  match op, vl with
  | Omove, v1::nil => Some v1
  | Ointconst n, nil => Some (Vint n)
  | Ofloatconst n, nil => Some (Vfloat n)
  | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
  | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
  | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
  | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
  | Oneg, Vint n1 :: nil => Some (Vint (Int.neg n1))
  | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2))
  | Osub, Vptr (Ptr b1 n1) :: Vint n2 :: nil => Some (Vptr (Ptr b1 (Int.sub n1 n2)))
  | Osub, Vptr (Ptr b1 n1) :: Vptr (Ptr b2 n2) :: nil =>
      if Z_eq_dec b1 b2 then Some (Vint (Int.sub n1 n2)) else None
  | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2))
  | Omulimm n, Vint n1 :: nil => Some (Vint (Int.mul n1 n))
  | Odiv, Vint n1 :: Vint n2 :: nil =>
      if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2))
  | Odivu, Vint n1 :: Vint n2 :: nil =>
      if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
  | Omod, Vint n1 :: Vint n2 :: nil =>
      if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
  | Omodu, Vint n1 :: Vint n2 :: nil =>
      if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
  | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2))
  | Oandimm n, Vint n1 :: nil => Some (Vint (Int.and n1 n))
  | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2))
  | Oorimm n, Vint n1 :: nil => Some (Vint (Int.or n1 n))
  | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2))
  | Oxorimm n, Vint n1 :: nil => Some (Vint (Int.xor n1 n))
  | Oshl, Vint n1 :: Vint n2 :: nil =>
      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
  | Oshlimm n, Vint n1 :: nil =>
      if Int.ltu n (Int.repr 32) then Some (Vint (Int.shl n1 n)) else None
  | Oshr, Vint n1 :: Vint n2 :: nil =>
      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
  | Oshrimm n, Vint n1 :: nil =>
      if Int.ltu n (Int.repr 32) then Some (Vint (Int.shr n1 n)) else None
  | Oshrximm n, Vint n1 :: nil =>
      if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None
  | Oshru, Vint n1 :: Vint n2 :: nil =>
      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
  | Oshruimm n, Vint n1 :: nil =>
      if Int.ltu n (Int.repr 32) then Some (Vint (Int.shru n1 n)) else None
  | Ororimm n, Vint n1 :: nil =>
      if Int.ltu n (Int.repr 32) then Some (Vint (Int.ror n1 n)) else None
  | Olea addr, _ =>
      eval_addressing genv sp addr vl
  | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
  | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2))
  | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
  | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
  | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
  | Osingleoffloat, v1 :: nil =>
      Some (Val.singleoffloat v1)
  | Ointoffloat, Vfloat f1 :: nil =>
      Some (Vint (Float.intoffloat f1))
  | Ofloatofint, Vint n1 :: nil =>
      Some (Vfloat (Float.floatofint n1))
  | Ointuoffloat, Vfloat f1 :: nil =>
      Some (Vint (Float.intuoffloat f1))
  | Ofloatofintu, Vint n1 :: nil =>
      Some (Vfloat (Float.floatofintu n1))
  | Ocmp c, _ =>
      match eval_condition c vl with
      | None => None
      | Some false => Some Vfalse
      | Some true => Some Vtrue
      end
  | _, _ => None
  end.

Definition negate_condition (cond: condition): condition :=
  match cond with
  | Ccomp c => Ccomp(negate_comparison c)
  | Ccompu c => Ccompu(negate_comparison c)
  | Ccompimm c n => Ccompimm (negate_comparison c) n
  | Ccompuimm c n => Ccompuimm (negate_comparison c) n
  | Ccompf c => Cnotcompf c
  | Cnotcompf c => Ccompf c
  | Cmaskzero n => Cmasknotzero n
  | Cmasknotzero n => Cmaskzero n
  end.

Inductive atomic_statement_mem_event :
  atomic_statement -> list val -> val -> mem_event -> Prop:=
  | atomic_statement_mem_event_cas: forall p v o n
    (NUo : o <> Vundef)
    (NUn : n <> Vundef)
    (HTo : Val.has_type o Tint)
    (HTn : Val.has_type n Tint),
    atomic_statement_mem_event AScas (Vptr p :: n :: o :: nil) v
                               (MErmw p Mint32 v (rmw_CAS o n))
  | atomic_statement_mem_event_lkinc: forall p v,
    atomic_statement_mem_event ASlkinc (Vptr p :: nil) v
                               (MErmw p Mint32 v (rmw_ADD (Vint Int.one))).

Ltac FuncInv := clarify;
  match goal with
  | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
      destruct x; simpl in H; FuncInv
  | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ => _ end = Some _) |- _ =>
      destruct v as [| | | []]; simpl in H; FuncInv
  | _ => idtac
  end.

Remark eval_negate_compare_mismatch:
  forall c b,
  eval_compare_mismatch c = Some b ->
  eval_compare_mismatch (negate_comparison c) = Some (negb b).

Remark eval_negate_compare_null:
  forall c i b,
  eval_compare_null c i = Some b ->
  eval_compare_null (negate_comparison c) i = Some (negb b).

Lemma eval_negate_condition:
  forall (cond: condition) (vl: list val) (b: bool),
  eval_condition cond vl = Some b ->
  eval_condition (negate_condition cond) vl = Some (negb b).


Section GENV_TRANSF.

Variable F1 F2: Type.
Variable ge1: Genv.t F1.
Variable ge2: Genv.t F2.
Hypothesis agree_on_symbols:
  forall (s: ident), 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.

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

End GENV_TRANSF.


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.


Definition type_of_condition (c: condition) : list typ :=
  match c with
  | Ccomp _ => Tint :: Tint :: nil
  | Ccompu _ => Tint :: Tint :: nil
  | Ccompimm _ _ => Tint :: nil
  | Ccompuimm _ _ => Tint :: nil
  | Ccompf _ => Tfloat :: Tfloat :: nil
  | Cnotcompf _ => Tfloat :: Tfloat :: nil
  | Cmaskzero _ => Tint :: nil
  | Cmasknotzero _ => Tint :: nil
  end.

Definition type_of_addressing (addr: addressing) : list typ :=
  match addr with
  | Aindexed _ => Tint :: nil
  | Aindexed2 _ => Tint :: Tint :: nil
  | Ascaled _ _ => Tint :: nil
  | Aindexed2scaled _ _ => Tint :: Tint :: nil
  | Aindexed2scaledrev _ _ => Tint :: Tint :: nil
  | Aglobal _ _ => nil
  | Abased _ _ => Tint :: nil
  | Abasedscaled _ _ _ => Tint :: nil
  | Ainstack _ => nil
  end.

Definition type_of_operation (op: operation) : list typ * typ :=
  match op with
  | Omove => (nil, Tint)
  | Ointconst _ => (nil, Tint)
  | Ofloatconst _ => (nil, Tfloat)
  | Ocast8signed => (Tint :: nil, Tint)
  | Ocast8unsigned => (Tint :: nil, Tint)
  | Ocast16signed => (Tint :: nil, Tint)
  | Ocast16unsigned => (Tint :: nil, Tint)
  | Oneg => (Tint :: nil, Tint)
  | Osub => (Tint :: Tint :: nil, Tint)
  | Omul => (Tint :: Tint :: nil, Tint)
  | Omulimm _ => (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)
  | Oshrximm _ => (Tint :: nil, Tint)
  | Oshru => (Tint :: Tint :: nil, Tint)
  | Oshruimm _ => (Tint :: nil, Tint)
  | Ororimm _ => (Tint :: nil, Tint)
  | Olea addr => (type_of_addressing addr, Tint)
  | Onegf => (Tfloat :: nil, Tfloat)
  | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
  | Osingleoffloat => (Tfloat :: nil, Tfloat)
  | Ointoffloat => (Tfloat :: nil, Tint)
  | Ofloatofint => (Tint :: nil, Tfloat)
  | Ointuoffloat => (Tfloat :: nil, Tint)
  | Ofloatofintu => (Tint :: nil, Tfloat)
  | Ocmp c => (type_of_condition c, Tint)
  end.

Definition type_of_atomic_statement (aop: atomic_statement) : list typ * typ :=
  match aop with
  | AScas => (Tint :: Tint :: Tint :: nil, Tint)
  | ASlkinc => (Tint :: nil, Tint)
  end.


Section SOUNDNESS.

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

Lemma type_of_addressing_sound:
  forall addr vl sp v,
  eval_addressing genv sp addr vl = Some v ->
  Val.has_type v Tint.

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

End SOUNDNESS.


Section EVAL_OP_TOTAL.

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

Definition find_symbol_offset (id: ident) (ofs: int) : val :=
  match Genv.find_symbol genv id with
  | Some b => Vptr (Ptr.add b ofs)
  | None => Vundef
  end.

Definition eval_condition_total (cond: condition) (vl: list val) : val :=
  match cond, vl with
  | Ccomp c, v1::v2::nil => Val.cmp c v1 v2
  | Ccompu c, v1::v2::nil => Val.cmpu c v1 v2
  | Ccompimm c n, v1::nil => Val.cmp c v1 (Vint n)
  | Ccompuimm c n, v1::nil => Val.cmpu c v1 (Vint n)
  | Ccompf c, v1::v2::nil => Val.cmpf c v1 v2
  | Cnotcompf c, v1::v2::nil => Val.notbool(Val.cmpf c v1 v2)
  | Cmaskzero n, v1::nil => Val.notbool (Val.and v1 (Vint n))
  | Cmasknotzero n, v1::nil => Val.notbool(Val.notbool (Val.and v1 (Vint n)))
  | _, _ => Vundef
  end.

Definition eval_addressing_total
    (sp: val) (addr: addressing) (vl: list val) : val :=
  match addr, vl with
  | Aindexed n, v1::nil => Val.add v1 (Vint n)
  | Aindexed2 n, v1::v2::nil => Val.add (Val.add v1 v2) (Vint n)
  | Ascaled sc ofs, v1::nil => Val.add (Val.mul v1 (Vint sc)) (Vint ofs)
  | Aindexed2scaled sc ofs, v1::v2::nil =>
      Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs))
  | Aindexed2scaledrev sc ofs, v2::v1::nil =>
      Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs))
  | Aglobal s ofs, nil => find_symbol_offset s ofs
  | Abased s ofs, v1::nil => Val.add (find_symbol_offset s ofs) v1
  | Abasedscaled sc s ofs, v1::nil => Val.add (find_symbol_offset s ofs) (Val.mul v1 (Vint sc))
  | Ainstack ofs, nil => Val.add sp (Vint ofs)
  | _, _ => Vundef
  end.

Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :=
  match op, vl with
  | Omove, v1::nil => v1
  | Ointconst n, nil => Vint n
  | Ofloatconst n, nil => Vfloat n
  | Ocast8signed, v1::nil => Val.sign_ext 8 v1
  | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1
  | Ocast16signed, v1::nil => Val.sign_ext 16 v1
  | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1
  | Oneg, v1::nil => Val.neg v1
  | Osub, v1::v2::nil => Val.sub v1 v2
  | Omul, v1::v2::nil => Val.mul v1 v2
  | Omulimm n, v1::nil => Val.mul v1 (Vint n)
  | Odiv, v1::v2::nil => Val.divs v1 v2
  | Odivu, v1::v2::nil => Val.divu v1 v2
  | Omod, v1::v2::nil => Val.mods v1 v2
  | Omodu, v1::v2::nil => Val.modu v1 v2
  | Oand, v1::v2::nil => Val.and v1 v2
  | Oandimm n, v1::nil => Val.and v1 (Vint n)
  | Oor, v1::v2::nil => Val.or v1 v2
  | Oorimm n, v1::nil => Val.or v1 (Vint n)
  | Oxor, v1::v2::nil => Val.xor v1 v2
  | Oxorimm n, v1::nil => Val.xor v1 (Vint n)
  | Oshl, v1::v2::nil => Val.shl v1 v2
  | Oshlimm n, v1::nil => Val.shl v1 (Vint n)
  | Oshr, v1::v2::nil => Val.shr v1 v2
  | Oshrimm n, v1::nil => Val.shr v1 (Vint n)
  | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
  | Oshru, v1::v2::nil => Val.shru v1 v2
  | Oshruimm n, v1::nil => Val.shru v1 (Vint n)
  | Ororimm n, v1::nil => Val.ror v1 (Vint n)
  | Olea addr, _ => eval_addressing_total sp addr vl
  | Onegf, v1::nil => Val.negf v1
  | Oaddf, v1::v2::nil => Val.addf v1 v2
  | Osubf, v1::v2::nil => Val.subf v1 v2
  | Omulf, v1::v2::nil => Val.mulf v1 v2
  | Odivf, v1::v2::nil => Val.divf v1 v2
  | Osingleoffloat, v1::nil => Val.singleoffloat v1
  | Ointoffloat, v1::nil => Val.intoffloat v1
  | Ofloatofint, v1::nil => Val.floatofint v1
  | Ointuoffloat, v1::nil => Val.intuoffloat v1
  | Ofloatofintu, v1::nil => Val.floatofintu v1
  | Ocmp c, _ => eval_condition_total c vl
  | _, _ => Vundef
  end.

Lemma eval_compare_mismatch_weaken:
  forall c b,
  eval_compare_mismatch c = Some b ->
  Val.cmp_mismatch c = Val.of_bool b.

Lemma eval_compare_null_weaken:
  forall n c b,
  eval_compare_null c n = Some b ->
  (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b.

End EVAL_OP_TOTAL.


Section EVAL_LESSDEF.

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

Ltac InvLessdef :=
  try done; match goal with
  | [ H: Val.lessdef (Vint _) _ |- _ ] =>
      inv H; InvLessdef
  | [ H: Val.lessdef (Vfloat _) _ |- _ ] =>
      inv H; InvLessdef
  | [ H: Val.lessdef (Vptr _) _ |- _ ] =>
      inv H; InvLessdef
  | [ H: Val.lessdef_list nil _ |- _ ] =>
      inv H; InvLessdef
  | [ H: Val.lessdef_list (_ :: _) _ |- _ ] =>
      inv H; InvLessdef
  | [ H: (match ?p with Ptr _ _ => _ end) = _ |- _ ] =>
      destruct p; clarify
  | _ => idtac
  end.


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

Lemma eval_condition_lessdef2:
  forall cond vl1 vl2,
  Val.lessdef_list vl2 vl1 ->
  eval_condition cond vl1 = None ->
  eval_condition cond vl2 = None.

Lemma eval_condition_lessdef3:
  forall cond vl1 vl2 b,
  Val.lessdef_list vl2 vl1 ->
  eval_condition cond vl1 = Some b ->
  eval_condition cond vl2 = None \/
  eval_condition cond vl2 = Some b.

Ltac TrivialExists :=
  match goal with
  | [ |- exists v2, Some ?v1 = Some v2 /\ _ ] =>
      exists v1; split; [apply refl_equal | try done ]
  | [ |- exists v2, _ /\ _ ] =>
      eexists; split; [eassumption | try done ]
  end.

Lemma eval_addressing_lessdef:
  forall sp addr vl1 vl2 v1,
  Val.lessdef_list vl1 vl2 ->
  eval_addressing genv sp addr vl1 = Some v1 ->
  eval_addressing genv sp addr vl2 = Some v1.

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

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

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

Lemma eval_operation_lessdef3:
  forall sp op vl1 vl2 v1,
  Val.lessdef_list vl2 vl1 ->
  eval_operation genv sp op vl1 = Some v1 ->
  eval_operation genv sp op vl2 = None
  \/ exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v2 v1.

End EVAL_LESSDEF.


Definition op_for_binary_addressing (addr: addressing) : operation := Olea addr.

Lemma eval_op_for_binary_addressing:
  forall (F: Type) (ge: Genv.t F) sp addr args v,
  (length args >= 2)%nat ->
  eval_addressing ge sp addr args = Some v ->
  eval_operation ge sp (op_for_binary_addressing addr) args = Some v.

Lemma type_op_for_binary_addressing:
  forall addr,
  (length (type_of_addressing addr) >= 2)%nat ->
  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).

Lemma atomic_statement_determinate:
  forall op args v v' lab lab'
  (ASME : atomic_statement_mem_event op args v lab)
  (HTv : Val.has_type v Tint)
  (ASME' : atomic_statement_mem_event op args v' lab')
  (HTv' : Val.has_type v' Tint),
   te_samekind (TEmem lab) (TEmem lab').

Lemma atomic_statement_determinate_eq:
  forall {op args v v' lab}
  (ASME : atomic_statement_mem_event op args v lab)
  (ASME' : atomic_statement_mem_event op args v' lab),
  v' = v.

Lemma atomic_statement_lessdef_arg:
  forall op args v lab args'
  (ASME : atomic_statement_mem_event op args v lab)
  (LD : Val.lessdef_list args args'),
    args' = args.

Lemma atomic_statement_lessdef_res:
  forall op args v p rmwop v'
  (ASME : atomic_statement_mem_event op args v (MErmw p Mint32 v rmwop))
  (LD : Val.lessdef v' v),
  atomic_statement_mem_event op args v' (MErmw p Mint32 v' rmwop).


Definition two_address_op (op: operation) : bool :=
  match op with
  | Omove => false
  | Ointconst _ => false
  | Ofloatconst _ => false
  | Ocast8signed => false
  | Ocast8unsigned => false
  | Ocast16signed => false
  | Ocast16unsigned => false
  | Oneg => true
  | Osub => true
  | Omul => true
  | Omulimm _ => true
  | Odiv => true
  | Odivu => true
  | Omod => true
  | Omodu => true
  | Oand => true
  | Oandimm _ => true
  | Oor => true
  | Oorimm _ => true
  | Oxor => true
  | Oxorimm _ => true
  | Oshl => true
  | Oshlimm _ => true
  | Oshr => true
  | Oshrimm _ => true
  | Oshrximm _ => true
  | Oshru => true
  | Oshruimm _ => true
  | Ororimm _ => true
  | Olea addr => false
  | Onegf => true
  | Oaddf => true
  | Osubf => true
  | Omulf => true
  | Odivf => true
  | Osingleoffloat => false
  | Ointoffloat => false
  | Ofloatofint => false
  | Ointuoffloat => false
  | Ofloatofintu => false
  | Ocmp c => false
  end.


Definition is_trivial_op (op: operation) : bool :=
  match op with
  | Omove => true
  | Ointconst _ => true
  | Olea (Aglobal _ _) => true
  | Olea (Ainstack _) => true
  | _ => false
  end.


Definition shift_stack_addressing (delta: int) (addr: addressing) :=
  match addr with
  | Ainstack ofs => Ainstack (Int.add delta ofs)
  | _ => addr
  end.

Definition shift_stack_operation (delta: int) (op: operation) :=
  match op with
  | Olea addr => Olea (shift_stack_addressing delta addr)
  | _ => op
  end.



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

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