Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import FMemory.
Require Import Ctypes.
Require Archi.
Require Import Cop.

Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val :=
  match classify_cast t1 t2 with
  | cast_case_pointer =>
      match v with
      | Vptr _ _ => Some v
      | Vint _ => if Archi.ptr64 then None else Some v
      | Vlong _ => if Archi.ptr64 then Some v else None
      | _ => None
      end
  | cast_case_i2i sz2 si2 =>
      match v with
      | Vint i => Some (Vint (cast_int_int sz2 si2 i))
      | _ => None
      end
  | cast_case_f2f =>
      match v with
      | Vfloat f => Some (Vfloat f)
      | _ => None
      end
  | cast_case_s2s =>
      match v with
      | Vsingle f => Some (Vsingle f)
      | _ => None
      end
  | cast_case_s2f =>
      match v with
      | Vsingle f => Some (Vfloat (Float.of_single f))
      | _ => None
      end
  | cast_case_f2s =>
      match v with
      | Vfloat f => Some (Vsingle (Float.to_single f))
      | _ => None
      end
  | cast_case_i2f si1 =>
      match v with
      | Vint i => Some (Vfloat (cast_int_float si1 i))
      | _ => None
      end
  | cast_case_i2s si1 =>
      match v with
      | Vint i => Some (Vsingle (cast_int_single si1 i))
      | _ => None
      end
  | cast_case_f2i sz2 si2 =>
      match v with
      | Vfloat f =>
          match cast_float_int si2 f with
          | Some i => Some (Vint (cast_int_int sz2 si2 i))
          | None => None
          end
      | _ => None
      end
  | cast_case_s2i sz2 si2 =>
      match v with
      | Vsingle f =>
          match cast_single_int si2 f with
          | Some i => Some (Vint (cast_int_int sz2 si2 i))
          | None => None
          end
      | _ => None
      end
  | cast_case_i2bool =>
      match v with
      | Vint n =>
          Some(Vint(if Int.eq n Int.zero then Int.zero else Int.one))
      | Vptr b ofs =>
          if Archi.ptr64 then None else
          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None
      | _ => None
      end
  | cast_case_l2bool =>
      match v with
      | Vlong n =>
          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
      | Vptr b ofs =>
          if negb Archi.ptr64 then None else
          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None

      | _ => None
      end
  | cast_case_f2bool =>
      match v with
      | Vfloat f =>
          Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one))
      | _ => None
      end
  | cast_case_s2bool =>
      match v with
      | Vsingle f =>
          Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one))
      | _ => None
      end
  | cast_case_l2l =>
      match v with
      | Vlong n => Some (Vlong n)
      | _ => None
      end
  | cast_case_i2l si =>
      match v with
      | Vint n => Some(Vlong (cast_int_long si n))
      | _ => None
      end
  | cast_case_l2i sz si =>
      match v with
      | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n))))
      | _ => None
      end
  | cast_case_l2f si1 =>
      match v with
      | Vlong i => Some (Vfloat (cast_long_float si1 i))
      | _ => None
      end
  | cast_case_l2s si1 =>
      match v with
      | Vlong i => Some (Vsingle (cast_long_single si1 i))
      | _ => None
      end
  | cast_case_f2l si2 =>
      match v with
      | Vfloat f =>
          match cast_float_long si2 f with
          | Some i => Some (Vlong i)
          | None => None
          end
      | _ => None
      end
  | cast_case_s2l si2 =>
      match v with
      | Vsingle f =>
          match cast_single_long si2 f with
          | Some i => Some (Vlong i)
          | None => None
          end
      | _ => None
      end
  | cast_case_struct id1 id2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 then Some v else None
      | _ => None
      end
  | cast_case_union id1 id2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 then Some v else None
      | _ => None
      end
  | cast_case_void =>
      Some v
  | cast_case_default =>
      None
  end.

Definition bool_val (v: val) (t: type) (m: mem) : option bool :=
  match classify_bool t with
  | bool_case_i =>
      match v with
      | Vint n => Some (negb (Int.eq n Int.zero))
      | Vptr b ofs =>
          if Archi.ptr64 then None else
          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None
      | _ => None
      end
  | bool_case_l =>
      match v with
      | Vlong n => Some (negb (Int64.eq n Int64.zero))
      | Vptr b ofs =>
          if negb Archi.ptr64 then None else
          if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None
      | _ => None
      end
  | bool_case_f =>
      match v with
      | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero))
      | _ => None
      end
  | bool_case_s =>
      match v with
      | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero))
      | _ => None
      end
  | bool_default => None
  end.

Definition sem_notbool (v: val) (ty: type) (m: mem): option val :=
  option_map (fun b => Val.of_bool (negb b)) (bool_val v ty m).

Definition sem_binarith
    (sem_int: signedness -> int -> int -> option val)
    (sem_long: signedness -> int64 -> int64 -> option val)
    (sem_float: float -> float -> option val)
    (sem_single: float32 -> float32 -> option val)
    (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val :=
  let c := classify_binarith t1 t2 in
  let t := binarith_type c in
  match sem_cast v1 t1 t m with
  | None => None
  | Some v1' =>
  match sem_cast v2 t2 t m with
  | None => None
  | Some v2' =>
  match c with
  | bin_case_i sg =>
      match v1', v2' with
      | Vint n1, Vint n2 => sem_int sg n1 n2
      | _, _ => None
      end
  | bin_case_f =>
      match v1', v2' with
      | Vfloat n1, Vfloat n2 => sem_float n1 n2
      | _, _ => None
      end
  | bin_case_s =>
      match v1', v2' with
      | Vsingle n1, Vsingle n2 => sem_single n1 n2
      | _, _ => None
      end
  | bin_case_l sg =>
      match v1', v2' with
      | Vlong n1, Vlong n2 => sem_long sg n1 n2
      | _, _ => None
      end
  | bin_default => None
  end end end.

Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val :=
  match classify_add t1 t2 with
  | add_case_pi ty si => (* pointer plus integer *)
      sem_add_ptr_int cenv ty si v1 v2
  | add_case_pl ty => (* pointer plus long *)
      sem_add_ptr_long cenv ty v1 v2
  | add_case_ip si ty => (* integer plus pointer *)
      sem_add_ptr_int cenv ty si v2 v1
  | add_case_lp ty => (* long plus pointer *)
      sem_add_ptr_long cenv ty v2 v1
  | add_default =>
      sem_binarith
        (fun sg n1 n2 => Some(Vint(Int.add n1 n2)))
        (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2)))
        (fun n1 n2 => Some(Vfloat(Float.add n1 n2)))
        (fun n1 n2 => Some(Vsingle(Float32.add n1 n2)))
        v1 t1 v2 t2 m
  end.

Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val :=
  match classify_sub t1 t2 with
  | sub_case_pi ty si => (* pointer minus integer *)
      match v1, v2 with
      | Vptr b1 ofs1, Vint n2 =>
          let n2 := ptrofs_of_int si n2 in
          Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
      | Vint n1, Vint n2 =>
          if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
      | Vlong n1, Vint n2 =>
          let n2 := cast_int_long si n2 in
          if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
      | _, _ => None
      end
  | sub_case_pl ty => (* pointer minus long *)
      match v1, v2 with
      | Vptr b1 ofs1, Vlong n2 =>
          let n2 := Ptrofs.of_int64 n2 in
          Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2)))
      | Vint n1, Vlong n2 =>
          let n2 := Int.repr (Int64.unsigned n2) in
          if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
      | Vlong n1, Vlong n2 =>
          if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None
      | _, _ => None
      end
  | sub_case_pp ty => (* pointer minus pointer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vptr b2 ofs2 =>
          if eq_block b1 b2 then
            let sz := sizeof cenv ty in
            if zlt 0 sz && zle sz Ptrofs.max_signed
            then Some (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr sz)))
            else None
          else None
      | _, _ => None
      end
  | sub_default =>
      sem_binarith
        (fun sg n1 n2 => Some(Vint(Int.sub n1 n2)))
        (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2)))
        (fun n1 n2 => Some(Vfloat(Float.sub n1 n2)))
        (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2)))
        v1 t1 v2 t2 m
  end.

Multiplication, division, modulus

Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 => Some(Vint(Int.mul n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2)))
    (fun n1 n2 => Some(Vfloat(Float.mul n1 n2)))
    (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
    v1 t1 v2 t2 m.

Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int.eq n2 Int.zero
          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
          then None else Some(Vint(Int.divs n1 n2))
      | Unsigned =>
          if Int.eq n2 Int.zero
          then None else Some(Vint(Int.divu n1 n2))
      end)
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int64.eq n2 Int64.zero
          || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
          then None else Some(Vlong(Int64.divs n1 n2))
      | Unsigned =>
          if Int64.eq n2 Int64.zero
          then None else Some(Vlong(Int64.divu n1 n2))
      end)
    (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
    (fun n1 n2 => Some(Vsingle(Float32.div n1 n2)))
    v1 t1 v2 t2 m.

Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int.eq n2 Int.zero
          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
          then None else Some(Vint(Int.mods n1 n2))
      | Unsigned =>
          if Int.eq n2 Int.zero
          then None else Some(Vint(Int.modu n1 n2))
      end)
    (fun sg n1 n2 =>
      match sg with
      | Signed =>
          if Int64.eq n2 Int64.zero
          || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
          then None else Some(Vlong(Int64.mods n1 n2))
      | Unsigned =>
          if Int64.eq n2 Int64.zero
          then None else Some(Vlong(Int64.modu n1 n2))
      end)
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2 m.

Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 => Some(Vint(Int.and n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2 m.

Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 => Some(Vint(Int.or n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2 m.

Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
  sem_binarith
    (fun sg n1 n2 => Some(Vint(Int.xor n1 n2)))
    (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2)))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2 m.

Definition cmp_ptr (m: mem) (c: comparison) (v1 v2: val): option val :=
  option_map Val.of_bool
   (if Archi.ptr64
    then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
    else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2).

Definition sem_cmp (c:comparison)
                  (v1: val) (t1: type) (v2: val) (t2: type)
                  (m: mem): option val :=
  match classify_cmp t1 t2 with
  | cmp_case_pp =>
      cmp_ptr m c v1 v2
  | cmp_case_pi si =>
      match v2 with
      | Vint n2 =>
          let v2' := Vptrofs (ptrofs_of_int si n2) in
          cmp_ptr m c v1 v2'
      | Vptr b ofs =>
          if Archi.ptr64 then None else cmp_ptr m c v1 v2
      | _ =>
          None
      end
  | cmp_case_ip si =>
      match v1 with
      | Vint n1 =>
          let v1' := Vptrofs (ptrofs_of_int si n1) in
          cmp_ptr m c v1' v2
      | Vptr b ofs =>
          if Archi.ptr64 then None else cmp_ptr m c v1 v2
      | _ =>
          None
      end
  | cmp_case_pl =>
      match v2 with
      | Vlong n2 =>
          let v2' := Vptrofs (Ptrofs.of_int64 n2) in
          cmp_ptr m c v1 v2'
      | Vptr b ofs =>
          if Archi.ptr64 then cmp_ptr m c v1 v2 else None
      | _ =>
          None
      end
  | cmp_case_lp =>
      match v1 with
      | Vlong n1 =>
          let v1' := Vptrofs (Ptrofs.of_int64 n1) in
          cmp_ptr m c v1' v2
      | Vptr b ofs =>
          if Archi.ptr64 then cmp_ptr m c v1 v2 else None
      | _ =>
          None
      end
  | cmp_default =>
      sem_binarith
        (fun sg n1 n2 =>
            Some(Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end)))
        (fun sg n1 n2 =>
            Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end)))
        (fun n1 n2 =>
            Some(Val.of_bool(Float.cmp c n1 n2)))
        (fun n1 n2 =>
            Some(Val.of_bool(Float32.cmp c n1 n2)))
        v1 t1 v2 t2 m
  end.

Definition sem_unary_operation
            (op: unary_operation) (v: val) (ty: type) (m: mem): option val :=
  match op with
  | Onotbool => sem_notbool v ty m
  | Onotint => sem_notint v ty
  | Oneg => sem_neg v ty
  | Oabsfloat => sem_absfloat v ty
  end.

Definition sem_binary_operation
    (cenv: composite_env)
    (op: binary_operation)
    (v1: val) (t1: type) (v2: val) (t2:type)
    (m: mem): option val :=
  match op with
  | Oadd => sem_add cenv v1 t1 v2 t2 m
  | Osub => sem_sub cenv v1 t1 v2 t2 m
  | Omul => sem_mul v1 t1 v2 t2 m
  | Omod => sem_mod v1 t1 v2 t2 m
  | Odiv => sem_div v1 t1 v2 t2 m
  | Oand => sem_and v1 t1 v2 t2 m
  | Oor => sem_or v1 t1 v2 t2 m
  | Oxor => sem_xor v1 t1 v2 t2 m
  | Oshl => sem_shl v1 t1 v2 t2
  | Oshr => sem_shr v1 t1 v2 t2
  | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
  | One => sem_cmp Cne v1 t1 v2 t2 m
  | Olt => sem_cmp Clt v1 t1 v2 t2 m
  | Ogt => sem_cmp Cgt v1 t1 v2 t2 m
  | Ole => sem_cmp Cle v1 t1 v2 t2 m
  | Oge => sem_cmp Cge v1 t1 v2 t2 m
  end.

Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) :=
  match id with
  | Incr => sem_add cenv v ty (Vint Int.one) type_int32s m
  | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s m
  end.

Compatibility with extensions and injections

Section GENERIC_INJECTION.

Variable f: meminj.
Variables m m': mem.

Hypothesis valid_pointer_inj:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
  Mem.valid_pointer m' 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 m b1 (Ptrofs.unsigned ofs) = true ->
  Mem.weak_valid_pointer m' 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 m 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 m b1 (Ptrofs.unsigned ofs1) = true ->
  Mem.valid_pointer m 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)).

Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue.

Remark val_inject_vfalse: forall f, Val.inject f Vfalse Vfalse.

Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b).

Remark val_inject_vptrofs: forall n, Val.inject f (Vptrofs n) (Vptrofs n).

Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs.

Ltac TrivialInject :=
  match goal with
  | [ H: None = Some _ |- _ ] => discriminate
  | [ H: Some _ = Some _ |- _ ] => inv H; TrivialInject
  | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x; TrivialInject
  | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; TrivialInject
  | [ |- exists v', Some ?v = Some v' /\ _ ] => exists v; split; auto
  | _ => idtac
  end.

Lemma sem_cast_inj:
  forall v1 ty1 ty v tv1,
  sem_cast v1 ty1 ty m = Some v ->
  Val.inject f v1 tv1 ->
  exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv.

Lemma bool_val_inj:
  forall v ty b tv,
  bool_val v ty m = Some b ->
  Val.inject f v tv ->
  bool_val tv ty m' = Some b.

Lemma sem_unary_operation_inj:
  forall op v1 ty v tv1,
  sem_unary_operation op v1 ty m = Some v ->
  Val.inject f v1 tv1 ->
  exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv.

Definition optval_self_injects (ov: option val) : Prop :=
  match ov with
  | Some (Vptr b ofs) => False
  | _ => True
  end.

Remark sem_binarith_inject:
  forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2',
  sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m = Some v ->
  Val.inject f v1 v1' -> Val.inject f v2 v2' ->
  (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) ->
  (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) ->
  (forall n1 n2, optval_self_injects (sem_float n1 n2)) ->
  (forall n1 n2, optval_self_injects (sem_single n1 n2)) ->
  exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m' = Some v' /\ Val.inject f v v'.

Remark sem_shift_inject:
  forall sem_int sem_long v1 t1 v2 t2 v v1' v2',
  sem_shift sem_int sem_long v1 t1 v2 t2 = Some v ->
  Val.inject f v1 v1' -> Val.inject f v2 v2' ->
  exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.inject f v v'.

Remark sem_cmp_ptr_inj:
  forall c v1 v2 v tv1 tv2,
  cmp_ptr m c v1 v2 = Some v ->
  Val.inject f v1 tv1 ->
  Val.inject f v2 tv2 ->
  exists tv, cmp_ptr m' c tv1 tv2 = Some tv /\ Val.inject f v tv.

Remark sem_cmp_inj:
  forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
  sem_cmp cmp v1 ty1 v2 ty2 m = Some v ->
  Val.inject f v1 tv1 ->
  Val.inject f v2 tv2 ->
  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.

Lemma sem_binary_operation_inj:
  forall cenv op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
  Val.inject f v1 tv1 -> Val.inject f v2 tv2 ->
  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.

End GENERIC_INJECTION.

Lemma sem_cast_inject:
  forall f v1 ty1 ty m v tv1 tm,
  sem_cast v1 ty1 ty m = Some v ->
  Val.inject f v1 tv1 ->
  Mem.inject f m tm ->
  exists tv, sem_cast tv1 ty1 ty tm = Some tv /\ Val.inject f v tv.

Lemma sem_unary_operation_inject:
  forall f m m' op v1 ty1 v tv1,
  sem_unary_operation op v1 ty1 m = Some v ->
  Val.inject f v1 tv1 ->
  Mem.inject f m m' ->
  exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ Val.inject f v tv.

Lemma sem_binary_operation_inject:
  forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v ->
  Val.inject f v1 tv1 -> Val.inject f v2 tv2 ->
  Mem.inject f m m' ->
  exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.

Lemma bool_val_inject:
  forall f m m' v ty b tv,
  bool_val v ty m = Some b ->
  Val.inject f v tv ->
  Mem.inject f m m' ->
  bool_val tv ty m' = Some b.

Some properties of operator semantics

Lemma cast_bool_bool_val:
  forall v t m,
  sem_cast v t (Tint IBool Signed noattr) m =
  match bool_val v t m with None => None | Some b => Some(Val.of_bool b) end.
  intros.
  assert (A: classify_bool t =
    match t with
    | Tint _ _ _ => bool_case_i
    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => if Archi.ptr64 then bool_case_l else bool_case_i
    | Tfloat F64 _ => bool_case_f
    | Tfloat F32 _ => bool_case_s
    | Tlong _ _ => bool_case_l
    | _ => bool_default
    end).
  {
    unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
  }
  unfold bool_val. rewrite A.
  unfold sem_cast, classify_cast; remember Archi.ptr64 as ptr64; destruct t; simpl; auto; destruct v; auto.
  destruct (Int.eq i0 Int.zero); auto.
  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i0)); auto.
  destruct (Int64.eq i Int64.zero); auto.
  destruct (negb ptr64); auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct f; auto.
  destruct f; auto.
  destruct f; auto.
  destruct f; auto.
  destruct (Float.cmp Ceq f0 Float.zero); auto.
  destruct f; auto.
  destruct (Float32.cmp Ceq f0 Float32.zero); auto.
  destruct f; auto.
  destruct ptr64; auto.
  destruct (Int.eq i Int.zero); auto.
  destruct ptr64; auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
  destruct ptr64; auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Int.eq i Int.zero); auto.
  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
  destruct ptr64; auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Int.eq i Int.zero); auto.
  destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto.
  destruct ptr64; auto.
  destruct ptr64; auto.
  destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto.
Qed.