Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Values_symbolictype.
Require Import Ctypes.
Require Import Values_symbolic.
Require Import NormaliseSpec.
Require Import Memory.

Syntax of operators.

Inductive unary_operation : Type :=
  | Onotbool : unary_operation (* boolean negation (! in C) *)
  | Onotint : unary_operation (* integer complement (~ in C) *)
  | Oneg : unary_operation (* opposite (unary -) *)
  | Oabsfloat : unary_operation. (* floating-point absolute value *)

Inductive binary_operation : Type :=
  | Oadd : binary_operation (* addition (binary +) *)
  | Osub : binary_operation (* subtraction (binary -) *)
  | Omul : binary_operation (* multiplication (binary *) *)
  | Odiv : binary_operation (* division (/) *)
  | Omod : binary_operation (* remainder (%) *)
  | Oand : binary_operation (* bitwise and (&) *)
  | Oor : binary_operation (* bitwise or (|) *)
  | Oxor : binary_operation (* bitwise xor (^) *)
  | Oshl : binary_operation (* left shift (<<) *)
  | Oshr : binary_operation (* right shift (>>) *)
  | Oeq: binary_operation (* comparison (==) *)
  | One: binary_operation (* comparison (!=) *)
  | Olt: binary_operation (* comparison (<) *)
  | Ogt: binary_operation (* comparison (>) *)
  | Ole: binary_operation (* comparison (<=) *)
  | Oge: binary_operation. (* comparison (>=) *)

Inductive incr_or_decr : Type := Incr | Decr.

Type classification and semantics of operators.

Casts and truth values

Inductive classify_cast_cases : Type :=
  | cast_case_neutral (* int|pointer -> int32|pointer *)
  | cast_case_i2i (sz2:intsize) (si2:signedness) (* int -> int *)
  | cast_case_f2f (* double -> double *)
  | cast_case_s2s (* single -> single *)
  | cast_case_f2s (* double -> single *)
  | cast_case_s2f (* single -> double *)
  | cast_case_i2f (si1: signedness) (* int -> double *)
  | cast_case_i2s (si1: signedness) (* int -> single *)
  | cast_case_f2i (sz2:intsize) (si2:signedness) (* double -> int *)
  | cast_case_s2i (sz2:intsize) (si2:signedness) (* single -> int *)
  | cast_case_l2l (* long -> long *)
  | cast_case_i2l (si1: signedness) (* int -> long *)
  | cast_case_l2i (sz2: intsize) (si2: signedness) (* long -> int *)
  | cast_case_l2f (si1: signedness) (* long -> double *)
  | cast_case_l2s (si1: signedness) (* long -> single *)
  | cast_case_f2l (si2:signedness) (* double -> long *)
  | cast_case_s2l (si2:signedness) (* single -> long *)
  | cast_case_f2bool (* double -> bool *)
  | cast_case_s2bool (* single -> bool *)
  | cast_case_l2bool (* long -> bool *)
  | cast_case_p2bool (* pointer -> bool *)
  | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (* struct -> struct *)
  | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (* union -> union *)
  | cast_case_void (* any -> void *)
  | cast_case_default.

Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
  match tto, tfrom with
  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
  | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool
  | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool
  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
  | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
  | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2
  | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2
  | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f
  | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s
  | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
  | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
  | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1
  | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1
  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
  | Tlong _ _, Tlong _ _ => cast_case_l2l
  | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
  | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
  | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
  | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2
  | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2
  | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1
  | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1
  | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
  | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
  | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
  | Tvoid, _ => cast_case_void
  | _, _ => cast_case_default
  end.


Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
  match sz, sg with
  | I8, Signed => Int.sign_ext 8 i
  | I8, Unsigned => Int.zero_ext 8 i
  | I16, Signed => Int.sign_ext 16 i
  | I16, Unsigned => Int.zero_ext 16 i
  | I32, _ => i
  | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
  end.

Definition cast_int_float (si: signedness) (i: int) : float :=
  match si with
  | Signed => Float.of_int i
  | Unsigned => Float.of_intu i
  end.

Definition cast_float_int (si : signedness) (f: float) : option int :=
  match si with
  | Signed => Float.to_int f
  | Unsigned => Float.to_intu f
  end.

Definition cast_int_single (si: signedness) (i: int) : float32 :=
  match si with
  | Signed => Float32.of_int i
  | Unsigned => Float32.of_intu i
  end.

Definition cast_single_int (si : signedness) (f: float32) : option int :=
  match si with
  | Signed => Float32.to_int f
  | Unsigned => Float32.to_intu f
  end.

Definition cast_int_long (si: signedness) (i: int) : int64 :=
  match si with
  | Signed => Int64.repr (Int.signed i)
  | Unsigned => Int64.repr (Int.unsigned i)
  end.

Definition cast_long_float (si: signedness) (i: int64) : float :=
  match si with
  | Signed => Float.of_long i
  | Unsigned => Float.of_longu i
  end.

Definition cast_long_single (si: signedness) (i: int64) : float32 :=
  match si with
  | Signed => Float32.of_long i
  | Unsigned => Float32.of_longu i
  end.

Definition cast_float_long (si : signedness) (f: float) : option int64 :=
  match si with
  | Signed => Float.to_long f
  | Unsigned => Float.to_longu f
  end.

Definition cast_single_long (si : signedness) (f: float32) : option int64 :=
  match si with
  | Signed => Float32.to_long f
  | Unsigned => Float32.to_longu f
  end.

Definition sem_cast (valid_ptr: block -> int -> bool) (v: val) (t1 t2: type) : option val :=
  match classify_cast t1 t2 with
  | cast_case_neutral =>
      match v with
      | Vint _ | Vptr _ _ => Some v
      | _ => 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_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_p2bool =>
      match v with
      | Vint i => Some (Vint (cast_int_int IBool Signed i))
      | Vptr b o => if valid_ptr b o
                    then Some (Vint Int.one)
                    else None
      | _ => 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_l2bool =>
      match v with
      | Vlong n =>
          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
      | _ => 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 fld1 id2 fld2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
      | _ => None
      end
  | cast_case_union id1 fld1 id2 fld2 =>
      match v with
      | Vptr b ofs =>
          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
      | _ => None
      end
  | cast_case_void =>
      Some v
  | cast_case_default =>
      None
  end.

Require Import Values_symbolictype.

Definition expr_cast_int_int sz2 si2 (e:expr_sym) : expr_sym :=
  match sz2 with
      IBool => Eunop OpBoolval Tint e
    | I32 => e
    | _ => Eunop (match si2 with
                      Signed => OpSignext
                    | Unsigned => OpZeroext
                  end match sz2 with
                          I8 => 8 | I16 => 16 | I32 => 32 | _ => 1
                      end)
                 Tint e
  end.

Definition sg_conv (s:signedness) :=
  match s with
      Signed => SESigned
    | Unsigned => SEUnsigned
  end.

Definition expr_cast_gen (fromt: styp) (froms:signedness)
           (tot: styp) (tos:signedness) (e:expr_sym) : expr_sym :=
  Eunop (OpConvert (sg_conv froms) (tot,sg_conv tos)) fromt e.

Definition sem_cast_expr (v: expr_sym) (t1 t2: type) : option expr_sym :=
  match classify_cast t1 t2 with
    | cast_case_neutral => Some v
    | cast_case_i2i sz2 si2 => Some (expr_cast_int_int sz2 si2 v)
    | cast_case_f2f => Some v
    | cast_case_s2s => Some v
    | cast_case_s2f => Some (expr_cast_gen Tsingle Signed Tfloat Signed v)
    | cast_case_f2s => Some (expr_cast_gen Tfloat Signed Tsingle Signed v)
    | cast_case_i2f si1 => Some (expr_cast_gen Tint si1 Tfloat Signed v)
    | cast_case_i2s si1 => Some (expr_cast_gen Tint si1 Tsingle Signed v)
    | cast_case_f2i sz2 si2 =>
      Some (expr_cast_int_int sz2 si2 (expr_cast_gen Tfloat Signed Tint si2 v))
    | cast_case_s2i sz2 si2 =>
      Some (expr_cast_int_int sz2 si2 (expr_cast_gen Tsingle Signed Tint si2 v))
    | cast_case_f2bool =>
      Some (
          Eunop OpNotbool Tint
                (Ebinop (OpCmp SESigned Ceq) Tfloat Tfloat v (Eval (Efloat Float.zero))))
    | cast_case_s2bool =>
      Some (Eunop OpNotbool Tint
                  (Ebinop (OpCmp SESigned Ceq) Tsingle Tsingle v (Eval (Esingle Float32.zero))))
    | cast_case_p2bool =>
      Some (Eunop OpNotbool Tint
                  (Ebinop (OpCmp SEUnsigned Ceq) Tint Tint v (Eval (Eint Int.zero))))
    | cast_case_l2l => Some v
    | cast_case_i2l si => Some (expr_cast_gen Tint si Tlong Signed v)
    | cast_case_l2i sz si => Some (expr_cast_int_int sz si (Val.loword v))
    | cast_case_l2bool =>
      Some (Eunop OpNotbool Tint
                  (Ebinop (OpCmp SESigned Ceq) Tlong Tlong v (Eval (Elong Int64.zero))))
    | cast_case_l2f si1 =>
      Some (expr_cast_gen Tlong si1 Tfloat Signed v)
    | cast_case_l2s si1 =>
      Some (expr_cast_gen Tlong si1 Tsingle Signed v)
    | cast_case_f2l si2 =>
      Some (expr_cast_gen Tfloat Signed Tlong si2 v)
    | cast_case_s2l si2 =>
      Some (expr_cast_gen Tsingle Signed Tlong si2 v)
    | cast_case_struct id1 fld1 id2 fld2 =>
      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
    | cast_case_union id1 fld1 id2 fld2 =>
      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
    | cast_case_void => Some v
    | cast_case_default => None
  end.

Lemma normalise_boolval:
  forall i,
    Normalise.eq_modulo_normalise
      (Eunop OpBoolval Tint (Eval (Eint i)))
      (Eval (Eint (if Int.eq i Int.zero then Int.zero else Int.one))).

Lemma normalise_f2s:
  forall f,
    Normalise.eq_modulo_normalise
      (Eval (Esingle (Float.to_single f)))
      (Eunop (OpConvert SESigned (Tsingle, SESigned)) Tfloat (Eval (Efloat f))).

Lemma normalise_s2f:
  forall f,
    Normalise.eq_modulo_normalise
      (Eval (Efloat (Float.of_single f)))
      (Eunop (OpConvert SESigned (Tfloat,SESigned)) Tsingle (Eval (Esingle f))).

Definition result_of_val (v:val) : result :=
  match v with
      Vint _ => Int
    | Vptr _ _ => Ptr
    | Vlong _ => Long
    | Vfloat _ => Float
    | Vsingle _ => Single
    | Vundef => Int
  end.

Notation expr_of_val v :=
  (Eval (NormaliseSpec.sval_of_val v)).

Definition norm_eq_compat (m: mem) (e:expr_sym) (v:val) : Prop :=
  Normalise.normalise (Mem.bounds_of_block m) (Mem.nat_mask m) e (result_of_val v) =
  Normalise.normalise (Mem.bounds_of_block m) (Mem.nat_mask m) (expr_of_val v) (result_of_val v).


Definition vptr (m: mem) :=
  fun b i => Mem.valid_pointer m b (Int.unsigned i).

Lemma valid_pointer:
  forall m b i,
    Mem.valid_pointer m b i = true ->
    in_bound i (Mem.bounds_of_block m b).

Ltac rew_tt H0 :=
  match type of H0 with
      context[Normalise.normalise ?sz ?msk (Eval ?v) ?t] =>
      first [
          erewrite Normalise.normalise_int_int in H0; eauto
        | erewrite Normalise.normalise_long_long in H0; eauto
        | erewrite Normalise.normalise_float_float in H0; eauto
        | erewrite Normalise.normalise_single_single in H0; eauto
        ]
  end.

Ltac norm_eval_wt :=
  match goal with
      H: Normalise.normalise _ _ ?v ?t = _ |- _ =>
      match goal with
          H1: tcheck_expr v = _ |- _ => fail 1
        | _ => destruct (tcheck_expr_dec v (NormaliseSpec.typ_of_result t));
              [| rewrite Normalise.expr_wt in H; try congruence; auto; fail]
      end
  end.

Ltac unfold_eval :=
    repeat (unfold NormaliseSpec.ebinop, NormaliseSpec.binop,
            NormaliseSpec.fun_of_binop, NormaliseSpec.fun_of_binop',
            NormaliseSpec.eunop, NormaliseSpec.unop,
            NormaliseSpec.fun_of_unop, NormaliseSpec.fun_of_unop'; simpl).

Ltac rewrite_norm :=
  repeat match goal with
      |- context[NormaliseSpec.eSexpr ?al ?em _ _ ?t ?v] =>
      repeat match goal with
          H: Normalise.normalise _ _ v ?tt = _ ,
          H1 : NormaliseSpec.compat ?al ?sz ?msk |- _ =>
          let x := fresh "H" in
          let A := fresh "A" in
          let B := fresh "B" in
          generalize (Normalise.norm_correct2 sz msk v tt);
            try rewrite H; intro x;
            edestruct (NormaliseSpec.IsNorm2.eval_ok eu eb sz msk v tt _ x)
                      as [|[A B]]
            ; eauto; try congruence; simpl in *; rewrite B; simpl
      end
  end.

Lemma sem_cast_expr_ok:
  forall v t1 t2 v' m,
    sem_cast (vptr m) v t1 t2 = Some v' ->
    exists v'',
      sem_cast_expr (expr_of_val v) t1 t2 = Some v'' /\
      norm_eq_compat m v'' v'.


Inductive classify_bool_cases : Type :=
  | bool_case_i (* integer *)
  | bool_case_f (* double float *)
  | bool_case_s (* single float *)
  | bool_case_p (* pointer *)
  | bool_case_l (* long *)
  | bool_default.

Definition classify_bool (ty: type) : classify_bool_cases :=
  match typeconv ty with
  | Ctypes.Tint _ _ _ => bool_case_i
  | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p
  | Ctypes.Tfloat F64 _ => bool_case_f
  | Ctypes.Tfloat F32 _ => bool_case_s
  | Ctypes.Tlong _ _ => bool_case_l
  | _ => bool_default
  end.


Definition bool_val (vptr: block -> int -> bool) (v: val) (t: type) : option bool :=
  match classify_bool t with
  | bool_case_i =>
      match v with
      | Vint n => Some (negb (Int.eq n Int.zero))
      | _ => 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_case_p =>
      match v with
      | Vint n => Some (negb (Int.eq n Int.zero))
      | Vptr b ofs => if vptr b ofs then Some true else None
      | _ => None
      end
  | bool_case_l =>
      match v with
      | Vlong n => Some (negb (Int64.eq n Int64.zero))
      | _ => None
      end
  | bool_default => None
  end.

Definition bool_expr (v: expr_sym) (t: type) : expr_sym :=
  match classify_bool t with
  | bool_case_i =>
    Ebinop (OpCmp SESigned Cne) Tint Tint v (Eval (Eint Int.zero))
  | bool_case_f =>
    Ebinop (OpCmp SESigned Cne) Tfloat Tfloat v (Eval (Efloat Float.zero))
  | bool_case_s =>
    Ebinop (OpCmp SESigned Cne) Tsingle Tsingle v (Eval (Esingle Float32.zero))
  | bool_case_p =>
    Ebinop (OpCmp SEUnsigned Cne) Tint Tint v (Eval (Eint Int.zero))
  | bool_case_l =>
    Ebinop (OpCmp SESigned Cne) Tlong Tlong v (Eval (Elong Int64.zero))
  | bool_default =>
    Ebinop (OpCmp SESigned Cne) Tint Tint v (Eval (Eint Int.zero))
  end.

Lemma bool_val_expr_ok:
  forall m v t v',
    bool_val (vptr m) v t = Some v' ->
    exists v'',
      bool_expr (expr_of_val v) t = v'' /\
      norm_eq_compat m v'' (Values.Val.of_bool v').

Unary operators

Boolean negation

Definition sem_notbool (vptr: block -> int -> bool) (v: val) (ty: type) : option val :=
  match classify_bool ty with
  | bool_case_i =>
      match v with
      | Vint n => Some (Values.Val.of_bool (Int.eq n Int.zero))
      | _ => None
      end
  | bool_case_f =>
      match v with
      | Vfloat f => Some (Values.Val.of_bool (Float.cmp Ceq f Float.zero))
      | _ => None
      end
  | bool_case_s =>
      match v with
      | Vsingle f => Some (Values.Val.of_bool (Float32.cmp Ceq f Float32.zero))
      | _ => None
      end
  | bool_case_p =>
      match v with
      | Vint n => Some (Values.Val.of_bool (Int.eq n Int.zero))
      | Vptr b ofs => if vptr b ofs then Some Vfalse else None
      | _ => None
      end
  | bool_case_l =>
      match v with
      | Vlong n => Some (Values.Val.of_bool (Int64.eq n Int64.zero))
      | _ => None
      end
  | bool_default => None
  end.

Definition sem_notbool_expr (v: expr_sym) (ty: type) : expr_sym :=
  match classify_bool ty with
  | bool_case_i =>
    Eunop OpNotbool Tint v
  | bool_case_f =>
    Ebinop (OpCmp SESigned Ceq) Tfloat Tfloat v (Eval (Efloat Float.zero))
  | bool_case_s =>
    Ebinop (OpCmp SESigned Ceq) Tsingle Tsingle v (Eval (Esingle Float32.zero))
  | bool_case_p =>
    Eunop OpNotbool Tint v
  | bool_case_l =>
    Ebinop (OpCmp SESigned Ceq) Tlong Tlong v (Eval (Elong Int64.zero))
  | bool_default =>
    Eunop OpNotbool Tint v
  end.


Lemma notbool_expr_ok:
  forall m v t v',
    sem_notbool (vptr m) v t = Some v' ->
    exists v'',
      sem_notbool_expr (expr_of_val v) t = v'' /\
      norm_eq_compat m v'' v'.

Opposite and absolute value

Inductive classify_neg_cases : Type :=
  | neg_case_i(s: signedness) (* int *)
  | neg_case_f (* double float *)
  | neg_case_s (* single float *)
  | neg_case_l(s: signedness) (* long *)
  | neg_default.

Definition classify_neg (ty: type) : classify_neg_cases :=
  match ty with
  | Ctypes.Tint I32 Unsigned _ => neg_case_i Unsigned
  | Ctypes.Tint _ _ _ => neg_case_i Signed
  | Ctypes.Tfloat F64 _ => neg_case_f
  | Ctypes.Tfloat F32 _ => neg_case_s
  | Ctypes.Tlong si _ => neg_case_l si
  | _ => neg_default
  end.

Definition sem_neg (v: val) (ty: type) : option val :=
  match classify_neg ty with
  | neg_case_i sg =>
      match v with
      | Vint n => Some (Vint (Int.neg n))
      | _ => None
      end
  | neg_case_f =>
      match v with
      | Vfloat f => Some (Vfloat (Float.neg f))
      | _ => None
      end
  | neg_case_s =>
      match v with
      | Vsingle f => Some (Vsingle (Float32.neg f))
      | _ => None
      end
  | neg_case_l sg =>
      match v with
      | Vlong n => Some (Vlong (Int64.neg n))
      | _ => None
      end
  | neg_default => None
  end.


Definition sem_neg_expr (v: expr_sym) (ty: type) : expr_sym :=
  match classify_neg ty with
  | neg_case_i sg => Eunop OpNeg Tint v
  | neg_case_f => Eunop OpNeg Tfloat v
  | neg_case_s => Eunop OpNeg Tsingle v
  | neg_case_l sg => Eunop OpNeg Tlong v
  | neg_default => Eunop OpNeg Tint v
  end.

Lemma neg_expr_ok:
  forall v t v',
    sem_neg v t = Some v' ->
    exists v'',
      sem_neg_expr (expr_of_val v) t = v'' /\
      Normalise.eq_modulo_normalise (expr_of_val v') v''.

Definition sem_absfloat (v: val) (ty: type) : option val :=
  match classify_neg ty with
  | neg_case_i sg =>
      match v with
      | Vint n => Some (Vfloat (Float.abs (cast_int_float sg n)))
      | _ => None
      end
  | neg_case_f =>
      match v with
      | Vfloat f => Some (Vfloat (Float.abs f))
      | _ => None
      end
  | neg_case_s =>
      match v with
      | Vsingle f => Some (Vfloat (Float.abs (Float.of_single f)))
      | _ => None
      end
  | neg_case_l sg =>
      match v with
      | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg n)))
      | _ => None
      end
  | neg_default => None
  end.

Definition sem_absfloat_expr (v: expr_sym) (ty: type) : expr_sym :=
  match classify_neg ty with
  | neg_case_i sg =>
    Eunop OpAbsf Tfloat (expr_cast_gen Tint sg Tfloat Signed v)
  | neg_case_f =>
    Eunop OpAbsf Tfloat v
  | neg_case_s =>
    Eunop OpAbsf Tfloat (expr_cast_gen Tsingle Signed Tfloat Signed v)
  | neg_case_l sg =>
    Eunop OpAbsf Tfloat (expr_cast_gen Tlong sg Tfloat Signed v)
  | neg_default =>
    Eunop OpAbsf Tfloat (expr_cast_gen Tint Signed Tfloat Signed v)
  end.


Lemma absfloat_expr_ok:
  forall v t v',
    sem_absfloat v t = Some v' ->
    exists v'',
      sem_absfloat_expr (expr_of_val v) t = v'' /\
      Normalise.eq_modulo_normalise (expr_of_val v') v''.

Bitwise complement

Inductive classify_notint_cases : Type :=
  | notint_case_i(s: signedness) (* int *)
  | notint_case_l(s: signedness) (* long *)
  | notint_default.

Definition classify_notint (ty: type) : classify_notint_cases :=
  match ty with
  | Ctypes.Tint I32 Unsigned _ => notint_case_i Unsigned
  | Ctypes.Tint _ _ _ => notint_case_i Signed
  | Ctypes.Tlong si _ => notint_case_l si
  | _ => notint_default
  end.

Definition sem_notint (v: val) (ty: type): option val :=
  match classify_notint ty with
  | notint_case_i sg =>
      match v with
      | Vint n => Some (Vint (Int.not n))
      | _ => None
      end
  | notint_case_l sg =>
      match v with
      | Vlong n => Some (Vlong (Int64.not n))
      | _ => None
      end
  | notint_default => None
  end.


Definition sem_notint_expr (v: expr_sym) (ty: type): expr_sym :=
  match classify_notint ty with
  | notint_case_i sg =>
    Eunop OpNot Tint v
  | notint_case_l sg =>
    Eunop OpNot Tlong v
  | notint_default =>
    Eunop OpNot Tint v
  end.


Lemma notint_expr_ok:
  forall v t v',
    sem_notint v t = Some v' ->
    exists v'',
      sem_notint_expr (expr_of_val v) t = v'' /\
      Normalise.eq_modulo_normalise (expr_of_val v') v''.

Binary operators

Inductive binarith_cases: Type :=
  | bin_case_i (s: signedness) (* at int type *)
  | bin_case_l (s: signedness) (* at long int type *)
  | bin_case_f (* at double float type *)
  | bin_case_s (* at single float type *)
  | bin_default. (* error *)

Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
  match ty1, ty2 with
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tint _ _ _ => bin_case_i Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint I32 Unsigned _ => bin_case_i Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint _ _ _ => bin_case_i Signed
  | Ctypes.Tlong Signed _, Ctypes.Tlong Signed _ => bin_case_l Signed
  | Ctypes.Tlong _ _, Ctypes.Tlong _ _ => bin_case_l Unsigned
  | Ctypes.Tlong sg _, Ctypes.Tint _ _ _ => bin_case_l sg
  | Ctypes.Tint _ _ _, Ctypes.Tlong sg _ => bin_case_l sg
  | Ctypes.Tfloat F32 _, Ctypes.Tfloat F32 _ => bin_case_s
  | Ctypes.Tfloat _ _, Ctypes.Tfloat _ _ => bin_case_f
  | Ctypes.Tfloat F64 _, (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _) => bin_case_f
  | (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _), Ctypes.Tfloat F64 _ => bin_case_f
  | Ctypes.Tfloat F32 _, (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _) => bin_case_s
  | (Ctypes.Tint _ _ _ | Ctypes.Tlong _ _), Ctypes.Tfloat F32 _ => bin_case_s
  | _, _ => bin_default
  end.


Definition binarith_type (c: binarith_cases) : type :=
  match c with
  | bin_case_i sg => Ctypes.Tint I32 sg noattr
  | bin_case_l sg => Ctypes.Tlong sg noattr
  | bin_case_f => Ctypes.Tfloat F64 noattr
  | bin_case_s => Ctypes.Tfloat F32 noattr
  | bin_default => Tvoid
  end.

Definition sem_binarith
           (vptr: block -> int -> bool)
    (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) : option val :=
  let c := classify_binarith t1 t2 in
  let t := binarith_type c in
  match sem_cast vptr v1 t1 t with
  | None => None
  | Some v1' =>
  match sem_cast vptr v2 t2 t 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_binarith_expr
           (sem_int: signedness -> expr_sym -> expr_sym -> option expr_sym)
           (sem_long: signedness -> expr_sym -> expr_sym -> option expr_sym)
           (sem_float: expr_sym -> expr_sym -> option expr_sym)
           (sem_single: expr_sym -> expr_sym -> option expr_sym)
           (v1: expr_sym) (t1: type) (v2: expr_sym) (t2: type) : option expr_sym :=
  let c := classify_binarith t1 t2 in
  let t := binarith_type c in
  match sem_cast_expr v1 t1 t with
    | None => None
    | Some v1' =>
      match sem_cast_expr v2 t2 t with
        | None => None
        | Some v2' =>
          match c with
            | bin_case_i sg =>
              sem_int sg v1' v2'
            | bin_case_f =>
              sem_float v1' v2'
            | bin_case_s =>
              sem_single v1' v2'
            | bin_case_l sg =>
              sem_long sg v1' v2'
            | bin_default => None
          end
      end
  end.

Lemma expr_binarith_ok:
  forall m si sl sf ss si' sl' sf' ss' v1 t1 v2 t2 v'
         (si_same: forall sg n1 n2 v,
                     si sg n1 n2 = Some v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vint n1) ->
                       norm_eq_compat m v2 (Vint n2) ->
                     exists v',
                       si' sg v1 v2 = Some v' /\
                       norm_eq_compat m v' v)
         (sl_same: forall sg n1 n2 v,
                     sl sg n1 n2 = Some v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vlong n1) ->
                       norm_eq_compat m v2 (Vlong n2) ->
                     exists v',
                       sl' sg v1 v2 = Some v' /\
                       norm_eq_compat m v' v)
         (sf_same: forall n1 n2 v,
                     sf n1 n2 = Some v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vfloat n1) ->
                       norm_eq_compat m v2 (Vfloat n2) ->
                     exists v',
                       sf' v1 v2 = Some v' /\
                       norm_eq_compat m v' v)
         (ss_same: forall n1 n2 v,
                     ss n1 n2 = Some v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vsingle n1) ->
                       norm_eq_compat m v2 (Vsingle n2) ->
                     exists v',
                       ss' v1 v2 = Some v' /\
                       norm_eq_compat m v' v),
    sem_binarith (vptr m) si sl sf ss v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_binarith_expr si' sl' sf' ss'
                        (expr_of_val v1) t1
                        (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Addition

Inductive classify_add_cases : Type :=
  | add_case_pi(ty: type) (* pointer, int *)
  | add_case_ip(ty: type) (* int, pointer *)
  | add_case_pl(ty: type) (* pointer, long *)
  | add_case_lp(ty: type) (* long, pointer *)
  | add_default. (* numerical type, numerical type *)

Definition classify_add (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer ty _, Ctypes.Tint _ _ _ => add_case_pi ty
  | Ctypes.Tint _ _ _, Tpointer ty _ => add_case_ip ty
  | Tpointer ty _, Ctypes.Tlong _ _ => add_case_pl ty
  | Ctypes.Tlong _ _, Tpointer ty _ => add_case_lp ty
  | _, _ => add_default
  end.

Definition sem_add vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_add t1 t2 with
  | add_case_pi ty => (* pointer plus integer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vint n2 =>
        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | add_case_ip ty => (* integer plus pointer *)
      match v1,v2 with
      | Vint n1, Vptr b2 ofs2 =>
        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
      | _, _ => None
      end
  | add_case_pl ty => (* pointer plus long *)
      match v1,v2 with
      | Vptr b1 ofs1, Vlong n2 =>
        let n2 := Int.repr (Int64.unsigned n2) in
        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | add_case_lp ty => (* long plus pointer *)
      match v1,v2 with
      | Vlong n1, Vptr b2 ofs2 =>
        let n1 := Int.repr (Int64.unsigned n1) in
        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
      | _, _ => None
      end
  | add_default =>
      sem_binarith vptr
        (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
  end.

Definition sem_add_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  match classify_add t1 t2 with
  | add_case_pi ty => (* pointer plus integer *)
    Some
      (Ebinop OpAdd Tint Tint v1 (Ebinop OpMul Tint Tint v2 (Eval (Eint (Int.repr (sizeof ty))))))
  | add_case_ip ty => (* integer plus pointer *)
    Some (Ebinop OpAdd Tint Tint v2 (Ebinop OpMul Tint Tint v1 (Eval (Eint (Int.repr (sizeof ty))))))
  | add_case_pl ty => (* pointer plus long *)
    Some (
        Ebinop OpAdd Tint Tint v1 (Ebinop OpMul Tint Tint
                                      (Eunop (OpConvert SEUnsigned (Tint,SEUnsigned)) Tlong v2)
                                      (Eval (Eint (Int.repr (sizeof ty))))))
  | add_case_lp ty => (* long plus pointer *)
    Some (Ebinop OpAdd Tint Tint v2 (Ebinop OpMul Tint Tint
                                      (Eunop (OpConvert SEUnsigned (Tint,SEUnsigned)) Tlong v1)
                                      (Eval (Eint (Int.repr (sizeof ty))))))
  | add_default =>
      sem_binarith_expr
        (fun sg n1 n2 => Some(Ebinop OpAdd Tint Tint n1 n2))
        (fun sg n1 n2 => Some(Ebinop OpAdd Tlong Tlong n1 n2))
        (fun n1 n2 => Some(Ebinop OpAdd Tfloat Tfloat n1 n2))
        (fun n1 n2 => Some(Ebinop OpAdd Tsingle Tsingle n1 n2))
        v1 t1 v2 t2
  end.


Lemma add_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_add (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_add_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Subtraction

Inductive classify_sub_cases : Type :=
  | sub_case_pi(ty: type) (* pointer, int *)
  | sub_case_pp(ty: type) (* pointer, pointer *)
  | sub_case_pl(ty: type) (* pointer, long *)
  | sub_default. (* numerical type, numerical type *)

Definition classify_sub (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer ty _, Ctypes.Tint _ _ _ => sub_case_pi ty
  | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty
  | Tpointer ty _, Ctypes.Tlong _ _ => sub_case_pl ty
  | _, _ => sub_default
  end.

Definition sem_sub vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_sub t1 t2 with
  | sub_case_pi ty => (* pointer minus integer *)
      match v1,v2 with
      | Vptr b1 ofs1, Vint n2 =>
          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | sub_case_pl ty => (* pointer minus long *)
      match v1,v2 with
      | Vptr b1 ofs1, Vlong n2 =>
          let n2 := Int.repr (Int64.unsigned n2) in
          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => 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
            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
          else None
      | _, _ => None
      end
  | sub_default =>
      sem_binarith vptr
        (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
  end.


Definition sem_sub_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  match classify_sub t1 t2 with
  | sub_case_pi ty => (* pointer minus integer *)
    Some (Ebinop OpSub Tint Tint v1
                 (Ebinop OpMul Tint Tint v2
                         (Eval (Eint (Int.repr (sizeof ty))))))
  | sub_case_pl ty => (* pointer minus long *)
    Some (Ebinop OpSub Tint Tint v1
                 (Ebinop OpMul Tint Tint
                         (expr_cast_gen Tlong Unsigned Tint Unsigned v2 )
                         (Eval (Eint (Int.repr (sizeof ty))))))
  | sub_case_pp ty => (* pointer minus pointer *)
    Some (Ebinop (OpDiv SEUnsigned) Tint Tint
                 (Ebinop OpSub Tint Tint v1 v2)
                 (Eval (Eint (Int.repr (sizeof ty)))))
  | sub_default =>
      sem_binarith_expr
        (fun sg n1 n2 => Some(Ebinop OpSub Tint Tint n1 n2))
        (fun sg n1 n2 => Some(Ebinop OpSub Tlong Tlong n1 n2))
        (fun n1 n2 => Some(Ebinop OpSub Tfloat Tfloat n1 n2))
        (fun n1 n2 => Some(Ebinop OpSub Tsingle Tsingle n1 n2))
        v1 t1 v2 t2
  end.


Lemma sub_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_sub (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_sub_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.
 

Multiplication, division, modulus

Definition sem_mul vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.


Definition sem_mul_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some( Ebinop OpMul Tint Tint n1 n2))
    (fun sg n1 n2 => Some( Ebinop OpMul Tlong Tlong n1 n2))
    (fun n1 n2 => Some( Ebinop OpMul Tfloat Tfloat n1 n2))
    (fun n1 n2 => Some( Ebinop OpMul Tsingle Tsingle n1 n2))
    v1 t1 v2 t2.



Lemma mul_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_mul (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_mul_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Definition sem_div vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.

Definition sem_div_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some (Ebinop (OpDiv (match sg with
                                        Signed => SESigned
                                      | Unsigned => SEUnsigned
                                    end))
                            Tint Tint n1 n2))
    (fun sg n1 n2 => Some (Ebinop (OpDiv (match sg with
                                        Signed => SESigned
                                      | Unsigned => SEUnsigned
                                    end))
                            Tlong Tlong n1 n2))
    (fun n1 n2 => Some(Ebinop (OpDiv SESigned) Tfloat Tfloat n1 n2))
    (fun n1 n2 => Some(Ebinop (OpDiv SESigned) Tsingle Tsingle n1 n2))
    v1 t1 v2 t2.

Lemma div_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_div (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_div_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Definition sem_mod vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.


Definition sem_mod_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some (Ebinop (OpMod (match sg with
                                        Signed => SESigned
                                      | Unsigned => SEUnsigned
                                    end))
                            Tint Tint n1 n2))
    (fun sg n1 n2 => Some (Ebinop (OpMod (match sg with
                                        Signed => SESigned
                                      | Unsigned => SEUnsigned
                                    end))
                            Tlong Tlong n1 n2))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.

Lemma mod_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_mod (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_mod_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.
 
Definition sem_and vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.

Definition sem_and_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some(Ebinop OpAnd Tint Tint n1 n2))
    (fun sg n1 n2 => Some(Ebinop OpAnd Tlong Tlong n1 n2))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.


Lemma and_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_and (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_and_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Definition sem_or vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.


Definition sem_or_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some(Ebinop OpOr Tint Tint n1 n2))
    (fun sg n1 n2 => Some(Ebinop OpOr Tlong Tlong n1 n2))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.


Lemma or_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_or (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_or_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.


Definition sem_xor vptr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_binarith vptr
    (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.


Definition sem_xor_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_binarith_expr
    (fun sg n1 n2 => Some(Ebinop OpXor Tint Tint n1 n2))
    (fun sg n1 n2 => Some(Ebinop OpXor Tlong Tlong n1 n2))
    (fun n1 n2 => None)
    (fun n1 n2 => None)
    v1 t1 v2 t2.


Lemma xor_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_xor (vptr m) v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_xor_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Shifts

Inductive classify_shift_cases : Type:=
  | shift_case_ii(s: signedness) (* int , int *)
  | shift_case_ll(s: signedness) (* long, long *)
  | shift_case_il(s: signedness) (* int, long *)
  | shift_case_li(s: signedness) (* long, int *)
  | shift_default.

Definition classify_shift (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tint _ _ _ => shift_case_ii Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tint _ _ _ => shift_case_ii Signed
  | Ctypes.Tint I32 Unsigned _, Ctypes.Tlong _ _ => shift_case_il Unsigned
  | Ctypes.Tint _ _ _, Ctypes.Tlong _ _ => shift_case_il Signed
  | Ctypes.Tlong s _, Ctypes.Tint _ _ _ => shift_case_li s
  | Ctypes.Tlong s _, Ctypes.Tlong _ _ => shift_case_ll s
  | _,_ => shift_default
  end.

Definition sem_shift
    (sem_int: signedness -> int -> int -> int)
    (sem_long: signedness -> int64 -> int64 -> int64)
    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
  match classify_shift t1 t2 with
  | shift_case_ii sg =>
      match v1, v2 with
      | Vint n1, Vint n2 =>
          if Int.ltu n2 Int.iwordsize
          then Some(Vint(sem_int sg n1 n2)) else None
      | _, _ => None
      end
  | shift_case_il sg =>
      match v1, v2 with
      | Vint n1, Vlong n2 =>
          if Int64.ltu n2 (Int64.repr 32)
          then Some(Vint(sem_int sg n1 (Int64.loword n2))) else None
      | _, _ => None
      end
  | shift_case_li sg =>
      match v1, v2 with
      | Vlong n1, Vint n2 =>
          if Int.ltu n2 Int64.iwordsize'
          then Some(Vlong(sem_long sg n1 (Int64.repr (Int.unsigned n2)))) else None
      | _, _ => None
      end
  | shift_case_ll sg =>
      match v1, v2 with
      | Vlong n1, Vlong n2 =>
          if Int64.ltu n2 Int64.iwordsize
          then Some(Vlong(sem_long sg n1 n2)) else None
      | _, _ => None
      end
  | shift_default => None
  end.


Definition sem_shift_expr
    (sem_int: signedness -> expr_sym -> expr_sym -> expr_sym)
    (sem_long: signedness -> expr_sym -> expr_sym -> expr_sym)
    (v1: expr_sym) (t1: type) (v2: expr_sym) (t2: type) : option expr_sym :=
  match classify_shift t1 t2 with
  | shift_case_ii sg => Some (sem_int sg v1 v2)
  | shift_case_il sg => Some (sem_int sg v1 (expr_cast_gen Tlong sg Tint sg v2))
  | shift_case_li sg => Some (sem_long sg v1 (expr_cast_gen Tint Unsigned Tlong Unsigned v2))
  | shift_case_ll sg => Some (sem_long sg v1 v2)
  | shift_default => None
  end.

Lemma expr_shift_sem_ok:
  forall m si sl si' sl' v1 t1 v2 t2 v'
         (si_expr: forall sg n1 n2 n2',
                   (forall alloc em,
                      NormaliseSpec.eSexpr alloc em eb eu Tint n2 =
                      NormaliseSpec.eSexpr alloc em eb eu Tint n2') ->
                   forall alloc em,
                      NormaliseSpec.eSexpr alloc em eb eu Tint (si' sg n1 n2) =
                      NormaliseSpec.eSexpr alloc em eb eu Tint (si' sg n1 n2'))
         (sl_expr: forall sg n1 n2 n2',
                   (forall alloc em,
                      NormaliseSpec.eSexpr alloc em eb eu Tlong n2 =
                      NormaliseSpec.eSexpr alloc em eb eu Tlong n2') ->
                   forall alloc em,
                     NormaliseSpec.eSexpr alloc em eb eu Tlong (sl' sg n1 n2) =
                     NormaliseSpec.eSexpr alloc em eb eu Tlong (sl' sg n1 n2'))
         (si_wt: forall sg n1 n2,
                   tcheck_expr n1 = Some Tint ->
                   tcheck_expr n2 = Some Tint ->
                   tcheck_expr (si' sg n1 n2) = Some Tint)
         (sl_wt: forall sg n1 n2,
                   tcheck_expr n1 = Some Tlong ->
                   tcheck_expr n2 = Some Tlong ->
                   tcheck_expr (sl' sg n1 n2) = Some Tlong)
         (si_same: forall sg n1 n2 v,
                     si sg n1 n2 = v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vint n1) ->
                       norm_eq_compat m v2 (Vint n2) ->
                       Int.ltu n2 Int.iwordsize = true ->
                       exists v',
                         si' sg v1 v2 = v' /\
                         norm_eq_compat m v' (Vint v))
         (sl_same: forall sg n1 n2 v,
                     sl sg n1 n2 = v ->
                     forall v1 v2,
                       norm_eq_compat m v1 (Vlong n1) ->
                       norm_eq_compat m v2 (Vlong n2) ->
                       Int64.ltu n2 Int64.iwordsize = true ->
                       exists v',
                         sl' sg v1 v2 = v' /\
                         norm_eq_compat m v' (Vlong v)),
    sem_shift si sl v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_shift_expr si' sl'
                     (expr_of_val v1) t1
                     (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Definition sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_shift
    (fun sg n1 n2 => Int.shl n1 n2)
    (fun sg n1 n2 => Int64.shl n1 n2)
    v1 t1 v2 t2.

Definition sem_shl_expr(v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_shift_expr
    (fun sg n1 n2 => Ebinop OpShl Tint Tint n1 n2)
    (fun sg n1 n2 => Ebinop OpShl Tlong Tint n1
                            (expr_cast_gen Tlong Unsigned Tint Unsigned n2))
    v1 t1 v2 t2.


Lemma shl_expr_ok:
  forall vptr v1 v2 t1 t2 v',
    sem_shl v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_shl_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat vptr v'' v'.

Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  sem_shift
    (fun sg n1 n2 => match sg with Signed => Int.shr n1 n2 | Unsigned => Int.shru n1 n2 end)
    (fun sg n1 n2 => match sg with Signed => Int64.shr n1 n2 | Unsigned => Int64.shru n1 n2 end)
    v1 t1 v2 t2.


Definition sem_shr_expr (v1:expr_sym) (t1:type) (v2: expr_sym) (t2:type) : option expr_sym :=
  sem_shift_expr
    (fun sg n1 n2 => Ebinop (OpShr match sg with Signed => SESigned
                                              | Unsigned => SEUnsigned
                                   end)
                            Tint Tint n1 n2)
    (fun sg n1 n2 => Ebinop (OpShr match sg with Signed => SESigned
                                              | Unsigned => SEUnsigned
                                   end)
                            Tlong Tint n1 (expr_cast_gen Tlong Unsigned Tint Unsigned n2))
    v1 t1 v2 t2.


Lemma shr_expr_ok:
  forall m v1 v2 t1 t2 v',
    sem_shr v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_shr_expr (expr_of_val v1) t1
                   (expr_of_val v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Comparisons

Inductive classify_cmp_cases : Type :=
  | cmp_case_pp (* pointer, pointer *)
  | cmp_case_pl (* pointer, long *)
  | cmp_case_lp (* long, pointer *)
  | cmp_default. (* numerical, numerical *)

Definition classify_cmp (ty1: type) (ty2: type) :=
  match typeconv ty1, typeconv ty2 with
  | Tpointer _ _ , Tpointer _ _ => cmp_case_pp
  | Tpointer _ _ , Ctypes.Tint _ _ _ => cmp_case_pp
  | Ctypes.Tint _ _ _, Tpointer _ _ => cmp_case_pp
  | Tpointer _ _ , Ctypes.Tlong _ _ => cmp_case_pl
  | Ctypes.Tlong _ _ , Tpointer _ _ => cmp_case_lp
  | _, _ => cmp_default
  end.

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 =>
      option_map Values.Val.of_bool (Values.Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
  | cmp_case_pl =>
      match v2 with
      | Vlong n2 =>
          let n2 := Int.repr (Int64.unsigned n2) in
          option_map Values.Val.of_bool (Values.Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2))
      | _ => None
      end
  | cmp_case_lp =>
      match v1 with
      | Vlong n1 =>
          let n1 := Int.repr (Int64.unsigned n1) in
          option_map Values.Val.of_bool (Values.Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2)
      | _ => None
      end
  | cmp_default =>
      sem_binarith (fun b i => Mem.valid_pointer m b (Int.unsigned i))
        (fun sg n1 n2 =>
            Some(Values.Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end)))
        (fun sg n1 n2 =>
            Some(Values.Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end)))
        (fun n1 n2 =>
            Some(Values.Val.of_bool(Float.cmp c n1 n2)))
        (fun n1 n2 =>
            Some(Values.Val.of_bool(Float32.cmp c n1 n2)))
        v1 t1 v2 t2
  end.


Definition sem_cmp_expr (c:comparison)
                  (v1: expr_sym) (t1: type) (v2: expr_sym) (t2: type)
                  (m: mem): option expr_sym :=
  match classify_cmp t1 t2 with
  | cmp_case_pp =>
    Some (Ebinop (OpCmp SEUnsigned c) Tint Tint v1 v2)
  | cmp_case_pl =>
    Some (Ebinop (OpCmp SEUnsigned c) Tint Tint v1 (expr_cast_gen Tlong Unsigned Tint Unsigned v2))
  | cmp_case_lp =>
    Some (Ebinop (OpCmp SEUnsigned c) Tint Tint (expr_cast_gen Tlong Unsigned Tint Unsigned v1) v2)
  | cmp_default =>
    sem_binarith_expr
      (fun sg n1 n2 =>
         Some(
             Ebinop (OpCmp (match sg with
                                Signed => SESigned
                              | Unsigned => SEUnsigned
                            end) c) Tint Tint n1 n2))
        (fun sg n1 n2 =>
         Some(
             Ebinop (OpCmp (match sg with
                                Signed => SESigned
                              | Unsigned => SEUnsigned
                            end) c) Tlong Tlong n1 n2))
        (fun n1 n2 =>
            Some( Ebinop (OpCmp SESigned c) Tfloat Tfloat n1 n2))
        (fun n1 n2 =>
            Some( Ebinop (OpCmp SESigned c) Tsingle Tsingle n1 n2))
        v1 t1 v2 t2
  end.

Lemma int_eq_true:
  forall i1 i2,
    Int.eq i1 i2 = true ->
    i1 = i2.

Lemma compat_conserve_cmp:
  forall c al sz msk b i i0
         (COMPAT: compat al sz msk)
         (bnd0: forall bb, fst (sz bb) = 0)
         (IB1: in_bound (Int.unsigned i) (sz b))
         (IB2: in_bound (Int.unsigned i0) (sz b)),
    Int.cmpu c (Int.add i (al b)) (Int.add i0 (al b)) = Int.cmpu c i i0.


Lemma compat_conserve_cmp':
  forall c al sz msk b i i0
         (COMPAT: compat al sz msk)
         (bnd0: forall bb, fst (sz bb) = 0)
         (IB1: in_bound (Int.unsigned i) (sz b))
         (IB2: (Int.unsigned i0) = snd (sz b)),
    Int.cmpu c (Int.add i (al b)) (Int.add i0 (al b)) = Int.cmpu c i i0.

Require Import Psatz.

Lemma weak_valid_pointer:
  forall m b0 i0 sz
         (bnds: forall b, sz b = Mem.bounds_of_block m b)
         (bnd0: forall b, fst (sz b) = 0)
         (Hib : forall (b : block) i,
                Mem.valid_pointer m b i = true ->
                in_bound i (sz b))
         (Hnib : forall (b : block) i,
                ~ in_bound i (sz b) ->
                  Mem.valid_pointer m b i = false
         )
         (NVP: Mem.valid_pointer m b0 (Int.unsigned i0) = false)
         (NVP': Mem.valid_pointer m b0 (Int.unsigned i0 - 1) = true),
    Int.unsigned i0 = snd (sz b0) \/ in_bound (Int.unsigned i0) (sz b0).

Lemma cmp_expr_ok:
  forall c v1 v2 t1 t2 m v',
    sem_cmp c v1 t1 v2 t2 m = Some v' ->
    exists v'',
      sem_cmp_expr c (expr_of_val v1) t1
                   (expr_of_val v2) t2 m = Some v'' /\
      norm_eq_compat m v'' v'.

Function applications

Inductive classify_fun_cases : Type :=
  | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (* (pointer to) function *)
  | fun_default.

Definition classify_fun (ty: type) :=
  match ty with
  | Tfunction args res cc => fun_case_f args res cc
  | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc
  | _ => fun_default
  end.

Argument of a switch statement

Inductive classify_switch_cases : Type :=
  | switch_case_i
  | switch_case_l
  | switch_default.

Definition classify_switch (ty: type) :=
  match ty with
  | Ctypes.Tint _ _ _ => switch_case_i
  | Ctypes.Tlong _ _ => switch_case_l
  | _ => switch_default
  end.

Definition sem_switch_arg (m: mem) (v: expr_sym) (ty: type): option Z :=
  match classify_switch ty with
  | switch_case_i =>
      match Mem.mem_norm m v Int with Vint n => Some(Int.unsigned n) | _ => None end
  | switch_case_l =>
      match Mem.mem_norm m v Long with Vlong n => Some(Int64.unsigned n) | _ => None end
  | switch_default =>
      None
  end.

Combined semantics of unary and binary operators

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

Definition sem_unary_operation_expr
            (op: unary_operation) (v: expr_sym) (ty: type): expr_sym :=
  match op with
  | Onotbool => sem_notbool_expr v ty
  | Onotint => sem_notint_expr v ty
  | Oneg => sem_neg_expr v ty
  | Oabsfloat => sem_absfloat_expr v ty
  end.

Lemma expr_unop_ok:
  forall m op v ty v',
    sem_unary_operation (vptr m) op v ty = Some v' ->
    exists v'',
      sem_unary_operation_expr op (expr_of_val v) ty = v'' /\
      norm_eq_compat m v'' v'.

Definition sem_binary_operation
    (op: binary_operation)
    (v1: val) (t1: type) (v2: val) (t2:type)
    (m: mem): option val :=
  let vptr := fun b i => Mem.valid_pointer m b (Int.unsigned i) in
  match op with
  | Oadd => sem_add vptr v1 t1 v2 t2
  | Osub => sem_sub vptr v1 t1 v2 t2
  | Omul => sem_mul vptr v1 t1 v2 t2
  | Omod => sem_mod vptr v1 t1 v2 t2
  | Odiv => sem_div vptr v1 t1 v2 t2
  | Oand => sem_and vptr v1 t1 v2 t2
  | Oor => sem_or vptr v1 t1 v2 t2
  | Oxor => sem_xor vptr v1 t1 v2 t2
  | 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_binary_operation_expr
    (op: binary_operation)
    (v1: expr_sym) (t1: type) (v2: expr_sym) (t2:type)
    (m: mem): option expr_sym :=
  match op with
  | Oadd => sem_add_expr v1 t1 v2 t2
  | Osub => sem_sub_expr v1 t1 v2 t2
  | Omul => sem_mul_expr v1 t1 v2 t2
  | Omod => sem_mod_expr v1 t1 v2 t2
  | Odiv => sem_div_expr v1 t1 v2 t2
  | Oand => sem_and_expr v1 t1 v2 t2
  | Oor => sem_or_expr v1 t1 v2 t2
  | Oxor => sem_xor_expr v1 t1 v2 t2
  | Oshl => sem_shl_expr v1 t1 v2 t2
  | Oshr => sem_shr_expr v1 t1 v2 t2
  | Oeq => sem_cmp_expr Ceq v1 t1 v2 t2 m
  | One => sem_cmp_expr Cne v1 t1 v2 t2 m
  | Olt => sem_cmp_expr Clt v1 t1 v2 t2 m
  | Ogt => sem_cmp_expr Cgt v1 t1 v2 t2 m
  | Ole => sem_cmp_expr Cle v1 t1 v2 t2 m
  | Oge => sem_cmp_expr Cge v1 t1 v2 t2 m
  end.

Definition is_valid_ptr (m:mem) (v: val) : Prop :=
  match v with
      Vptr b o => in_bound (Int.unsigned o) (Mem.bounds_of_block m b)
    | _ => True
  end.

Lemma expr_binop_ok:
  forall op v1 t1 v2 t2 m v',
    sem_binary_operation op v1 t1 v2 t2 m = Some v' ->
    exists v'',
      sem_binary_operation_expr op (expr_of_val v1) t1
                               (expr_of_val v2) t2 m = Some v'' /\
      norm_eq_compat m v'' v'.

Lemma valid_ptr_norm_val:
  forall m v
         (IVP : is_valid_ptr m v),
    Normalise.normalise (Mem.bounds_of_block m) (Mem.nat_mask m)
                        (expr_of_val v) (result_of_val v) = v.

Lemma norm_eq_compat_norm:
  forall m e v,
    norm_eq_compat m e v ->
    is_valid_ptr m v ->
    Mem.mem_norm m e (result_of_val v) = v.

Lemma expr_binop_ok':
  forall op v1 t1 v2 t2 m v',
    sem_binary_operation op v1 t1 v2 t2 m = Some v' ->
    is_valid_ptr m v' ->
    exists v'',
      sem_binary_operation_expr op (expr_of_val v1) t1
                                (expr_of_val v2) t2 m = Some v'' /\
      Mem.mem_norm m v'' (result_of_val v') = v'.


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

Definition sem_incrdecr_expr (id: incr_or_decr) (v: expr_sym) (ty: type) :=
  match id with
  | Incr => sem_add_expr v ty (Eval (Eint Int.one)) type_int32s
  | Decr => sem_sub_expr v ty (Eval (Eint Int.one)) type_int32s
  end.

Lemma incrdecr_expr_ok:
  forall m id v1 t1 v',
    sem_incrdecr (vptr m) id v1 t1 = Some v' ->
    exists v'',
      sem_incrdecr_expr id (expr_of_val v1) t1 = Some v'' /\
      norm_eq_compat m v'' v'.

Definition incrdecr_type (ty: type) :=
  match typeconv ty with
  | Tpointer ty a => Tpointer ty a
  | Ctypes.Tint sz sg a => Ctypes.Tint sz sg noattr
  | Ctypes.Tlong sg a => Ctypes.Tlong sg noattr
  | Ctypes.Tfloat sz a => Ctypes.Tfloat sz noattr
  | _ => Tvoid
  end.

Compatibility with extensions and injections

Section GENERIC_INJECTION.

Variable f: meminj.
Variable p: Val.partial_undef_allocation.
Variables m m': mem.

Hypothesis valid_pointer_inj:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.valid_pointer m b1 (Int.unsigned ofs) = true ->
  Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.

Hypothesis weak_valid_pointer_inj:
  forall b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true ->
  Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.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 (Int.unsigned ofs) = true ->
  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.

Hypothesis valid_different_pointers_inj:
  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  b1 <> b2 ->
  Mem.valid_pointer m b1 (Int.unsigned ofs1) = true ->
  Mem.valid_pointer m b2 (Int.unsigned ofs2) = true ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.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 (Values.Val.of_bool b) (Values.Val.of_bool b).

Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool.

Ltac TrivialInject :=
  match goal with
  | |- exists v', Some ?v = Some v' /\ _ => (exists v; split; auto)
  | _ => idtac
  end.

Definition vptr1 := (fun b i => Mem.valid_pointer m b (Int.unsigned i)).
Definition vptr2 := (fun b i => Mem.valid_pointer m' b (Int.unsigned i)).

Lemma sem_cast_inject:
  forall v1 ty1 ty v tv1,
    sem_cast vptr1 v1 ty1 ty = Some v ->
    val_inject f v1 tv1 ->
    exists tv, sem_cast vptr2 tv1 ty1 ty = Some tv /\
               val_inject f v tv.


Ltac inject_auto :=
  match goal with
      |- Val.expr_inject _ _ (Eunop _ _ _) (Eunop _ _ _) =>
      apply expr_inject_unop; auto
    | |- Val.expr_inject _ _ (Ebinop _ _ _ _ _) (Ebinop _ _ _ _ _) =>
      apply expr_inject_binop; auto
  end.

Lemma sem_cast_expr_inject:
  forall v1 ty1 ty v tv1,
    sem_cast_expr v1 ty1 ty = Some v ->
    Val.expr_inject p f v1 tv1 ->
    exists tv, sem_cast_expr tv1 ty1 ty = Some tv /\ Val.expr_inject p f v tv.

Lemma sem_unary_operation_inject:
  forall op v1 ty v tv1,
  sem_unary_operation vptr1 op v1 ty = Some v ->
  val_inject f v1 tv1 ->
  exists tv, sem_unary_operation vptr2 op tv1 ty = Some tv /\ val_inject f v tv.



Lemma sem_unary_operation_expr_inject:
  forall op v1 ty v tv1,
  sem_unary_operation_expr op v1 ty = v ->
  Val.expr_inject p f v1 tv1 ->
  exists tv, sem_unary_operation_expr op tv1 ty = tv /\ Val.expr_inject p f v tv.


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


Definition optval_self_injects_expr (ov: option expr_sym) : Prop :=
  match ov with
  | Some e => forall p f, Val.expr_inject p f e e
  | _ => True
  end.

Remark sem_binarith_inject:
  forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2',
  sem_binarith vptr1 sem_int sem_long sem_float sem_single v1 t1 v2 t2 = 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 vptr2 sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'.


Definition sem_conserves_inject (sem: expr_sym -> expr_sym -> option expr_sym) : Prop :=
  forall p f v1 v2 v1' v2' v',
    Val.expr_inject p f v1 v1' ->
    Val.expr_inject p f v2 v2' ->
    sem v1 v2 = Some v' ->
    exists v'',
      sem v1' v2' = Some v'' /\
      Val.expr_inject p f v' v''.

Remark sem_binarith_expr_inject:
  forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2'
         (SBE: sem_binarith_expr sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v)
         (EI1: Val.expr_inject p f v1 v1')
         (EI2: Val.expr_inject p f v2 v2')
         (SCIi: forall sg, sem_conserves_inject (sem_int sg))
         (SCIl: forall sg, sem_conserves_inject (sem_long sg))
         (SCIf: sem_conserves_inject sem_float)
         (SCIs: sem_conserves_inject sem_single),
  exists v', sem_binarith_expr sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\
             Val.expr_inject p 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'.



Definition sem_conserves_inject2 (sem: expr_sym -> expr_sym -> expr_sym) : Prop :=
  forall p f v1 v2 v1' v2',
    Val.expr_inject p f v1 v1' ->
    Val.expr_inject p f v2 v2' ->
    Val.expr_inject p f (sem v1 v2) (sem v1' v2').

Remark sem_shift_expr_inject:
  forall sem_int sem_long v1 t1 v2 t2 v v1' v2'
         (SSE:sem_shift_expr sem_int sem_long v1 t1 v2 t2 = Some v)
         (EI1: Val.expr_inject p f v1 v1')
         (EI2:Val.expr_inject p f v2 v2')
         (SCIi: forall sg, sem_conserves_inject2 (sem_int sg))
         (SCIl: forall sg, sem_conserves_inject2 (sem_long sg)),
  exists v', sem_shift_expr sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.expr_inject p f v v'.

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.


Remark sem_cmp_expr_inj:
  forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
  sem_cmp_expr cmp v1 ty1 v2 ty2 m = Some v ->
  Val.expr_inject p f v1 tv1 ->
  Val.expr_inject p f v2 tv2 ->
  exists tv, sem_cmp_expr cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.expr_inject p f v tv.

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

Lemma sem_binary_operation_expr_inj:
  forall op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation_expr op v1 ty1 v2 ty2 m = Some v ->
    Val.expr_inject p f v1 tv1 -> Val.expr_inject p f v2 tv2 ->
  exists tv, sem_binary_operation_expr op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.expr_inject p f v tv.

Lemma bool_val_inject:
  forall v ty b tv,
  bool_val vptr1 v ty = Some b ->
  val_inject f v tv ->
  bool_val vptr2 tv ty = Some b.

End GENERIC_INJECTION.

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


Lemma sem_binary_operation_expr_inject:
  forall p f m m' op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation_expr op v1 ty1 v2 ty2 m = Some v ->
  Val.expr_inject p f v1 tv1 -> Val.expr_inject p f v2 tv2 ->
  Mem.inject p f m m' ->
  exists tv, sem_binary_operation_expr op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.expr_inject p f v tv.

Some properties of operator semantics

Lemma cast_bool_bool_val:
  forall m v t,
  sem_cast (vptr m) v t (Ctypes.Tint IBool Signed noattr) =
  match bool_val (vptr m) v t with None => None | Some b => Some(Values.Val.of_bool b) end.

Lemma cast_bool_bool_val_expr:
  forall v t b,
    sem_cast_expr v t (Ctypes.Tint IBool Signed noattr) = Some b ->
    Normalise.eq_modulo_normalise b (bool_expr v t).



Lemma notbool_bool_val:
  forall vptr v t,
  sem_notbool vptr v t =
  match bool_val vptr v t with None => None | Some b => Some(Values.Val.of_bool (negb b)) end.

Lemma notbool_bool_expr:
  forall v t,
    Normalise.eq_modulo_normalise (sem_notbool_expr v t) (Eunop OpNotbool Tint (bool_expr v t)).



Module ArithConv.


Inductive int_type : Type :=
  | _Bool
  | Char | SChar | UChar
  | Short | UShort
  | Int | UInt
  | Long | ULong
  | Longlong | ULonglong.

Inductive arith_type : Type :=
  | I (it: int_type)
  | Float
  | Double
  | Longdouble.

Definition eq_int_type: forall (x y: int_type), {x=y} + {x<>y}.

Definition is_unsigned (t: int_type) : bool :=
  match t with
  | _Bool => true
  | Char => false (* as in most of CompCert's target ABIs *)
  | SChar => false
  | UChar => true
  | Short => false
  | UShort => true
  | Int => false
  | UInt => true
  | Long => false
  | ULong => true
  | Longlong => false
  | ULonglong => true
  end.

Definition unsigned_type (t: int_type) : int_type :=
  match t with
  | Char => UChar
  | SChar => UChar
  | Short => UShort
  | Int => UInt
  | Long => ULong
  | Longlong => ULonglong
  | _ => t
  end.

Definition int_sizeof (t: int_type) : Z :=
  match t with
  | _Bool | Char | SChar | UChar => 1
  | Short | UShort => 2
  | Int | UInt | Long | ULong => 4
  | Longlong | ULonglong => 8
  end.


Definition rank (t: int_type) : Z :=
  match t with
  | _Bool => 1
  | Char | SChar | UChar => 2
  | Short | UShort => 3
  | Int | UInt => 4
  | Long | ULong => 5
  | Longlong | ULonglong => 6
  end.


Definition integer_promotion (t: int_type) : int_type :=
  if zlt (rank t) (rank Int) then Int else t.


Definition usual_arithmetic_conversion (t1 t2: arith_type) : arith_type :=
  match t1, t2 with
  | Longdouble, _ | _, Longdouble => Longdouble
  | Double, _ | _, Double => Double
  | Float, _ | _, Float => Float
  | I i1, I i2 =>
    let j1 := integer_promotion i1 in
    let j2 := integer_promotion i2 in
    if eq_int_type j1 j2 then I j1 else
    match is_unsigned j1, is_unsigned j2 with
    | true, true | false, false =>
        if zlt (rank j1) (rank j2) then I j2 else I j1
    | true, false =>
        if zle (rank j2) (rank j1) then I j1 else
        if zlt (int_sizeof j1) (int_sizeof j2) then I j2 else
        I (unsigned_type j2)
    | false, true =>
        if zle (rank j1) (rank j2) then I j2 else
        if zlt (int_sizeof j2) (int_sizeof j1) then I j1 else
        I (unsigned_type j1)
    end
  end.


Definition proj_type (t: arith_type) : type :=
  match t with
  | I _Bool => Ctypes.Tint IBool Unsigned noattr
  | I Char => Ctypes.Tint I8 Unsigned noattr
  | I SChar => Ctypes.Tint I8 Signed noattr
  | I UChar => Ctypes.Tint I8 Unsigned noattr
  | I Short => Ctypes.Tint I16 Signed noattr
  | I UShort => Ctypes.Tint I16 Unsigned noattr
  | I Int => Ctypes.Tint I32 Signed noattr
  | I UInt => Ctypes.Tint I32 Unsigned noattr
  | I Long => Ctypes.Tint I32 Signed noattr
  | I ULong => Ctypes.Tint I32 Unsigned noattr
  | I Longlong => Ctypes.Tlong Signed noattr
  | I ULonglong => Ctypes.Tlong Unsigned noattr
  | Float => Ctypes.Tfloat F32 noattr
  | Double => Ctypes.Tfloat F64 noattr
  | Longdouble => Ctypes.Tfloat F64 noattr
  end.


Lemma typeconv_integer_promotion:
  forall i, typeconv (proj_type (I i)) = proj_type (I (integer_promotion i)).


Lemma classify_binarith_arithmetic_conversion:
  forall t1 t2,
  binarith_type (classify_binarith (proj_type t1) (proj_type t2)) =
  proj_type (usual_arithmetic_conversion t1 t2).

End ArithConv.