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 ExprEval.
Require Import Memory.
Require Import Memperm.

Syntax of operators.

Require Export CopSyntax.
Require Export CopGeneric.

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 => Eunop (OpZeroext 32) Tint 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 (Val.sign_ext 32 v)
    | cast_case_i2i sz2 si2 => Some (expr_cast_int_int sz2 si2 v)
    | cast_case_f2f => Some (expr_cast_gen Tfloat Signed Tfloat Signed v)
    | cast_case_s2s => Some (expr_cast_gen Tsingle Signed Tsingle Signed 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 (Vfloat Float.zero))))
    | cast_case_s2bool =>
      Some (Eunop OpNotbool Tint
                  (Ebinop (OpCmp SESigned Ceq) Tsingle Tsingle v (Eval (Vsingle Float32.zero))))
    | cast_case_p2bool =>
      Some (Eunop OpNotbool Tint
                  (Ebinop (OpCmp SEUnsigned Ceq) Tint Tint v (Eval (Vint Int.zero))))
    | cast_case_l2l => Some (expr_cast_gen Tlong Signed Tlong Signed 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 (Vlong 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.

Definition norm_eq_compat (m: mem) (e:expr_sym) (v:val) : Prop :=
  Mem.mem_norm m e = Mem.mem_norm m (Eval 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).

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 (Eval v) t1 t2 = Some v'' /\
      norm_eq_compat m v'' v'.


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 (Vint Int.zero))
  | bool_case_f =>
    Ebinop (OpCmp SESigned Cne) Tfloat Tfloat v (Eval (Vfloat Float.zero))
  | bool_case_s =>
    Ebinop (OpCmp SESigned Cne) Tsingle Tsingle v (Eval (Vsingle Float32.zero))
  | bool_case_p =>
    Ebinop (OpCmp SEUnsigned Cne) Tint Tint v (Eval (Vint Int.zero))
  | bool_case_l =>
    Ebinop (OpCmp SESigned Cne) Tlong Tlong v (Eval (Vlong Int64.zero))
  | bool_default =>
    Ebinop (OpCmp SESigned Cne) Tint Tint v (Eval (Vint 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 (Eval v) t = v'' /\
      norm_eq_compat m v'' (Values.Val.of_bool v').

Unary operators

Boolean negation

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 (Vfloat Float.zero))
  | bool_case_s =>
    Ebinop (OpCmp SESigned Ceq) Tsingle Tsingle v (Eval (Vsingle Float32.zero))
  | bool_case_p =>
    Eunop OpNotbool Tint v
  | bool_case_l =>
    Ebinop (OpCmp SESigned Ceq) Tlong Tlong v (Eval (Vlong 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 (Eval v) t = v'' /\
      norm_eq_compat m v'' v'.

Opposite and absolute value

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 (Eval v) t = v'' /\
      same_eval (Eval v') v''.

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 (Eval v) t = v'' /\
      same_eval (Eval v') v''.

Bitwise complement

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 (Eval v) t = v'' /\
      same_eval (Eval v') v''.

Binary operators

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'
                        (Eval v1) t1
                        (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Addition

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 (Vint (Int.repr (sizeof ty))))))
  | add_case_ip ty => (* integer plus pointer *)
    Some (Ebinop OpAdd Tint Tint v2 (Ebinop OpMul Tint Tint v1 (Eval (Vint (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 (Vint (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 (Vint (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.



Ltac rew_tt H0 :=
  match type of H0 with
    context[Mem.mem_norm ?m (Eval ?v)] =>
    rewrite Mem.norm_val in H0
  end.

Ltac rewrite_norm :=
  match goal with
  | |- context [eSexpr ?al ?em ?v] =>
        match goal with
        | H:Mem.mem_norm _ v = _, H1:Mem.compat_m ?m ?sz ?al
          |- _ =>
              let x := fresh "H" in
              let A := fresh "A" in
              let B := fresh "B" in
              generalize (Mem.norm_correct m v); rewrite H; intro x;
              generalize (Mem.eval_ok_m _ _ _ x _ em H1); simpl; intro A; inv A
        end
  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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Subtraction

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 (Vint (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 (Vint (Int.repr (sizeof ty))))))
  | sub_case_pp ty => (* pointer minus pointer *)
    Some (Ebinop (OpDiv SEUnsigned) Tint Tint
                 (Ebinop OpSub Tint Tint v1 v2)
                 (Eval (Vint (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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.
 

Multiplication, division, modulus

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.

Ltac autonorm :=
  repeat rewrite Mem.norm_val in *;
  apply Mem.eq_norm; try congruence; constructor; red; simpl; intros; auto;
  repeat rewrite_norm; simpl; auto.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.


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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.


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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Shifts

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',
                     same_eval n2 n2' ->
                     same_eval (si' sg n1 n2) (si' sg n1 n2'))
         (sl_expr: forall sg n1 n2 n2',
                     same_eval n2 n2' ->
                     same_eval (sl' sg n1 n2) (sl' sg n1 n2'))
         (si_same: forall sg n1 n2 v1 v2,
                       norm_eq_compat m v1 (Vint n1) ->
                       norm_eq_compat m v2 (Vint n2) ->
                       Int.ltu n2 Int.iwordsize = true ->
                       norm_eq_compat m (si' sg v1 v2) (Vint (si sg n1 n2)))
         (sl_same: forall sg n1 n2 v1 v2,
                       norm_eq_compat m v1 (Vlong n1) ->
                       norm_eq_compat m v2 (Vlong n2) ->
                       Int64.ltu n2 Int64.iwordsize = true ->
                       norm_eq_compat m (sl' sg v1 v2) (Vlong (sl sg n1 n2))),
    sem_shift si sl v1 t1 v2 t2 = Some v' ->
    exists v'',
      sem_shift_expr si' sl'
                     (Eval v1) t1
                     (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat vptr v'' v'.

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 (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

Comparisons

Definition sem_cmp_expr (c:comparison)
                  (v1: expr_sym) (t1: type) (v2: expr_sym) (t2: type)
: 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.
Require Import Psatz.


Ltac elim_div_mod :=
  unfold Zmod, Zdiv;
  match goal with
    | |- context [Z.div_eucl ?X ?Y] =>
      let x := fresh "X" in
      (let y := fresh "Y" in
       (let eqx := fresh "EQX" in
        (let eqy := fresh "EQY" in
         (remember X as x eqn:eqx;
          remember Y as y eqn:eqy ;
          generalize (Z_div_mod_full x y) ;
          unfold Remainder ;
          generalize (Z.div_eucl x y) ;
          (let p := fresh "P" in intro p ; destruct p)
         ))))
  end.

Require Import Psatz.

Lemma compat_conserve_cmp:
  forall c al sz msk b i i0 q (qinf: q <= Int.max_unsigned)
         (COMPAT: compat q sz msk al)
        (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 q (qinf: q <= Int.max_unsigned)
         (COMPAT: compat q sz msk al)
         (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 (Mem.valid_pointer m) = Some v' ->
    exists v'',
      sem_cmp_expr c (Eval v1) t1
                   (Eval v2) t2 = Some v'' /\
      norm_eq_compat m v'' v'.

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

Combined semantics of unary and binary operators

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 (Eval v) ty = v'' /\
      norm_eq_compat m v'' v'.

Definition sem_binary_operation_expr
    (op: binary_operation)
    (v1: expr_sym) (t1: type) (v2: expr_sym) (t2:type)
: 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
  | One => sem_cmp_expr Cne v1 t1 v2 t2
  | Olt => sem_cmp_expr Clt v1 t1 v2 t2
  | Ogt => sem_cmp_expr Cgt v1 t1 v2 t2
  | Ole => sem_cmp_expr Cle v1 t1 v2 t2
  | Oge => sem_cmp_expr Cge v1 t1 v2 t2
  end.

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

Lemma norm_undef:
  forall m,
    Mem.mem_norm m (Eval Vundef) = Vundef.

Lemma norm_eq_compat_norm:
  forall m e v,
    norm_eq_compat m e v ->
    Mem.mem_norm m e = v.

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

Definition sem_incrdecr_expr (id: incr_or_decr) (v: expr_sym) (ty: type) :=
  match id with
  | Incr => sem_add_expr v ty (Eval (Vint Int.one)) type_int32s
  | Decr => sem_sub_expr v ty (Eval (Vint 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 (Eval v1) t1 = Some v'' /\
      norm_eq_compat m v'' v'.

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 (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
    (SC: sem_cast vptr1 v1 ty1 ty = Some v)
    (VI: val_inject f v1 tv1),
  exists tv, sem_cast vptr2 tv1 ty1 ty = Some tv /\
        val_inject f v tv.


Ltac inject_auto :=
  repeat match goal with
             H: wf_inj ?ei |- ?ei _ (Eunop _ _ _) (Eunop _ _ _ ) =>
             apply (ei_unop _ H); auto
           | H: wf_inj ?ei |- ?ei _ (Ebinop _ _ _ _ _) (Ebinop _ _ _ _ _ ) =>
             apply (ei_binop _ H); auto
           | H: wf_inj ?ei |- ?ei _ (Eval _) (Eval _) =>
             apply (vi_ei _ H); simpl; auto
         end.

Lemma sem_cast_expr_inject:
  forall ei (wf: wf_inj ei) v1 ty1 ty v tv1,
    sem_cast_expr v1 ty1 ty = Some v ->
    ei f v1 tv1 ->
    exists tv, sem_cast_expr tv1 ty1 ty = Some tv /\ ei 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 ei (wf: wf_inj ei) op v1 ty v tv1,
  sem_unary_operation_expr op v1 ty = v ->
  ei f v1 tv1 ->
  exists tv, sem_unary_operation_expr op tv1 ty = tv /\ ei 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 (ei: _ -> _ -> _ -> Prop) (f: meminj), ei 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 ei (wf: wf_inj ei) f v1 v2 v1' v2' v',
    ei f v1 v1' ->
    ei f v2 v2' ->
    sem v1 v2 = Some v' ->
    exists v'',
      sem v1' v2' = Some v'' /\
      ei f v' v''.

Remark sem_binarith_expr_inject:
  forall ei (wf: wf_inj ei) 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: ei f v1 v1')
         (EI2: ei 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' /\
             ei 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 ei (wf: wf_inj ei) f v1 v2 v1' v2',
    ei f v1 v1' ->
    ei f v2 v2' ->
    ei f (sem v1 v2) (sem v1' v2').

Remark sem_shift_expr_inject:
  forall ei (wf: wf_inj ei) 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: ei f v1 v1')
         (EI2: ei 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' /\ ei f v v'.

Remark sem_cmp_inj:
  forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
  sem_cmp cmp v1 ty1 v2 ty2 (Mem.valid_pointer m) = Some v ->
  val_inject f v1 tv1 ->
  val_inject f v2 tv2 ->
  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 (Mem.valid_pointer m') = Some tv /\ val_inject f v tv.


Remark sem_cmp_expr_inj:
  forall ei (wf: wf_inj ei) cmp v1 tv1 ty1 v2 tv2 ty2 v,
  sem_cmp_expr cmp v1 ty1 v2 ty2 = Some v ->
  ei f v1 tv1 ->
  ei f v2 tv2 ->
  exists tv, sem_cmp_expr cmp tv1 ty1 tv2 ty2 = Some tv /\ ei 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 (Mem.valid_pointer m) = Some v ->
  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 (Mem.valid_pointer m') = Some tv /\ val_inject f v tv.

Lemma sem_binary_operation_expr_inj:
  forall ei (wf: wf_inj ei) op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation_expr op v1 ty1 v2 ty2 = Some v ->
    ei f v1 tv1 -> ei f v2 tv2 ->
  exists tv, sem_binary_operation_expr op tv1 ty1 tv2 ty2 = Some tv /\ ei 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 sm ei (wf: wf_inj ei) f m m' op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation op v1 ty1 v2 ty2 (Mem.valid_pointer m) = Some v ->
  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
  Mem.inject sm ei f m m' ->
  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 (Mem.valid_pointer m') = Some tv /\ val_inject f v tv.


Lemma sem_binary_operation_expr_inject:
  forall sm ei (wf: wf_inj ei) f m m' op v1 ty1 v2 ty2 v tv1 tv2,
  sem_binary_operation_expr op v1 ty1 v2 ty2 = Some v ->
  ei f v1 tv1 -> ei f v2 tv2 ->
  Mem.inject sm ei f m m' ->
  exists tv, sem_binary_operation_expr op tv1 ty1 tv2 ty2 = Some tv /\ ei f v tv.

Some properties of operator semantics

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



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


Lemma sem_unary_operation_expr_se:
  forall u t e e',
    same_eval e e' ->
    same_eval (sem_unary_operation_expr u e t)
                   (sem_unary_operation_expr u e' t).

Lemma expr_cast_int_int_se:
  forall sz2 si2 e e',
    same_eval e e' ->
    same_eval (expr_cast_int_int sz2 si2 e)
                   (expr_cast_int_int sz2 si2 e').

Lemma expr_cast_gen_se:
  forall t s t' s' e e',
    same_eval e e' ->
    same_eval (expr_cast_gen t s t' s' e)
                   (expr_cast_gen t s t' s' e').

Ltac se_rew' :=
  repeat ((apply unop_same_eval; simpl; auto)
            ||
            (apply binop_same_eval; simpl; eauto)
            ||
            (apply expr_cast_int_int_se; simpl; eauto)
            ||
            (apply expr_cast_gen_se; simpl; eauto)
            || reflexivity || auto).


Definition conserves_same_eval_unary (f: expr_sym -> option expr_sym) : Prop :=
  forall e e',
    same_eval e e' ->
    match
      f e, f e'
    with
       | Some a, Some b => same_eval a b
       | None, None => True
       | _, _ => False
    end.

Lemma sem_cast_expr_se:
  forall t t',
    conserves_same_eval_unary (fun e => sem_cast_expr e t t').

Lemma sem_binarith_expr_se:
  forall si sl sf ss t t'
         (si_norm: forall s, conserves_same_eval (si s))
         (sl_norm: forall s, conserves_same_eval (sl s))
         (sf_norm: conserves_same_eval sf)
         (ss_norm: conserves_same_eval ss),
    conserves_same_eval (fun e f => sem_binarith_expr si sl sf ss e t f t').

Lemma sem_shift_expr_se:
  forall si sl t t'
         (si_norm: forall s a b c d,
                     same_eval a b ->
                     same_eval c d ->
                     same_eval (si s a c) (si s b d))
         (sl_norm: forall s a b c d,
                     same_eval a b ->
                     same_eval c d ->
                     same_eval (sl s a c) (sl s b d)),
    conserves_same_eval (fun e f => sem_shift_expr si sl e t f t').


Lemma sem_binary_operation_expr_se:
  forall b t t' e e' f f',
    same_eval e e' ->
    same_eval f f' ->
    match sem_binary_operation_expr b e t f t', sem_binary_operation_expr b e' t f' t' with
        Some a, Some b => same_eval a b
      | None, None => True
      | _ , _ => False
    end.


Lemma bool_expr_se:
  forall v v' t,
    same_eval v v' ->
    same_eval (bool_expr v t) (bool_expr v' t).