From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cop.v | 953 ++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 643 insertions(+), 310 deletions(-) (limited to 'cfrontend/Cop.v') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index af7aaa86..c6e07b75 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -76,23 +76,35 @@ Inductive classify_cast_cases : Type := | cast_case_f2f (sz2:floatsize) (**r float -> float *) | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_l2l (**r long -> long *) + | cast_case_i2l (si1: signedness) (**r int -> long *) + | cast_case_l2i (sz2: intsize) (si2: signedness) (**r long -> int *) + | cast_case_l2f (si1: signedness) (sz2: floatsize) (**r long -> float *) + | cast_case_f2l (si2: signedness) (**r float -> long *) | cast_case_f2bool (**r float -> bool *) + | cast_case_l2bool (**r long -> bool *) | cast_case_p2bool (**r pointer -> bool *) | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) | cast_case_void (**r any -> void *) | cast_case_default. -Function classify_cast (tfrom tto: type) : classify_cast_cases := +Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool + | 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 sz1 _ => cast_case_f2i sz2 si2 | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | (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 sz1 _ => cast_case_f2l si2 + | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2 | 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 @@ -131,7 +143,25 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. -Function sem_cast (v: val) (t1 t2: type) : option val := +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.floatoflong i + | Unsigned => Float.floatoflongu i + end. + +Definition cast_float_long (si : signedness) (f: float) : option int64 := + match si with + | Signed => Float.longoffloat f + | Unsigned => Float.longuoffloat f + end. + +Definition sem_cast (v: val) (t1 t2: type) : option val := match classify_cast t1 t2 with | cast_case_neutral => match v with @@ -174,10 +204,53 @@ Function sem_cast (v: val) (t1 t2: type) : option val := | Vptr _ _ => Some (Vint Int.one) | _ => None end + | cast_case_l2l => + match v with + | Vlong n => Some (Vlong n) + | _ => None + end + | cast_case_i2l si => + match v with + | Vint n => Some(Vlong (cast_int_long si n)) + | _ => None + end + | cast_case_l2i sz si => + match v with + | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) + | _ => None + end + | cast_case_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 sz2 => + match v with + | Vlong i => Some (Vfloat (cast_float_float sz2 (cast_long_float 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_struct id1 fld1 id2 fld2 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + 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 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + 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 => @@ -192,13 +265,15 @@ Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) | bool_case_f (**r float *) | bool_case_p (**r pointer *) + | bool_case_l (**r long *) | bool_default. Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p + | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p | Tfloat _ _ => bool_case_f + | Tlong _ _ => bool_case_l | _ => bool_default end. @@ -207,7 +282,7 @@ Definition classify_bool (ty: type) : classify_bool_cases := considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Function bool_val (v: val) (t: type) : option bool := +Definition bool_val (v: val) (t: type) : option bool := match classify_bool t with | bool_case_i => match v with @@ -225,6 +300,11 @@ Function bool_val (v: val) (t: type) : option bool := | Vptr b ofs => Some true | _ => None end + | bool_case_l => + match v with + | Vlong n => Some (negb (Int64.eq n Int64.zero)) + | _ => None + end | bool_default => None end. @@ -239,25 +319,29 @@ Proof. assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p + | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p | Tfloat _ _ => bool_case_f + | Tlong _ _ => bool_case_l | _ => bool_default end). - unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto. - + { + unfold classify_bool; destruct t; simpl; auto. destruct i; auto. + } unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i0 Int.zero); auto. + destruct (Int64.eq i Int64.zero); auto. destruct (Float.cmp Ceq f0 Float.zero); auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i0 Int.zero); auto. Qed. (** ** Unary operators *) (** *** Boolean negation *) -Function sem_notbool (v: val) (ty: type) : option val := +Definition sem_notbool (v: val) (ty: type) : option val := match classify_bool ty with | bool_case_i => match v with @@ -275,6 +359,11 @@ Function sem_notbool (v: val) (ty: type) : option val := | Vptr _ _ => Some Vfalse | _ => None end + | bool_case_l => + match v with + | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero)) + | _ => None + end | bool_default => None end. @@ -294,6 +383,7 @@ Qed. Inductive classify_neg_cases : Type := | neg_case_i(s: signedness) (**r int *) | neg_case_f (**r float *) + | neg_case_l(s: signedness) (**r long *) | neg_default. Definition classify_neg (ty: type) : classify_neg_cases := @@ -301,10 +391,11 @@ Definition classify_neg (ty: type) : classify_neg_cases := | Tint I32 Unsigned _ => neg_case_i Unsigned | Tint _ _ _ => neg_case_i Signed | Tfloat _ _ => neg_case_f + | Tlong si _ => neg_case_l si | _ => neg_default end. -Function sem_neg (v: val) (ty: type) : option val := +Definition sem_neg (v: val) (ty: type) : option val := match classify_neg ty with | neg_case_i sg => match v with @@ -316,6 +407,11 @@ Function sem_neg (v: val) (ty: type) : option val := | Vfloat f => Some (Vfloat (Float.neg f)) | _ => None end + | neg_case_l sg => + match v with + | Vlong n => Some (Vlong (Int64.neg n)) + | _ => None + end | neg_default => None end. @@ -323,20 +419,27 @@ Function sem_neg (v: val) (ty: type) : option val := Inductive classify_notint_cases : Type := | notint_case_i(s: signedness) (**r int *) + | notint_case_l(s: signedness) (**r long *) | notint_default. Definition classify_notint (ty: type) : classify_notint_cases := match ty with | Tint I32 Unsigned _ => notint_case_i Unsigned | Tint _ _ _ => notint_case_i Signed + | Tlong si _ => notint_case_l si | _ => notint_default end. -Function sem_notint (v: val) (ty: type): option val := +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.xor n Int.mone)) + | 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 @@ -351,59 +454,119 @@ Function sem_notint (v: val) (ty: type): option val := (e.g. division, modulus, comparisons), the unsigned operation is selected if at least one of the arguments is of type "unsigned int32", otherwise the signed operation is performed. +- Likewise if both arguments are of long integer type. - If both arguments are of float type, a float operation is performed. We choose to perform all float arithmetic in double precision, even if both arguments are single-precision floats. -- If one argument has integer type and the other has float type, +- If one argument has integer/long type and the other has float type, we convert the integer argument to float, then perform the float operation. +- If one argument has long integer type and the other integer type, + we convert the integer argument to long, then perform the long operation *) -(** *** Addition *) - -Inductive classify_add_cases : Type := - | add_case_ii(s: signedness) (**r int, int *) - | add_case_ff (**r float, float *) - | add_case_if(s: signedness) (**r int, float *) - | add_case_fi(s: signedness) (**r float, int *) - | add_case_pi(ty: type)(a: attr) (**r pointer, int *) - | add_case_ip(ty: type)(a: attr) (**r int, pointer *) - | add_default. - -Definition classify_add (ty1: type) (ty2: type) := +Inductive binarith_cases: Type := + | bin_case_ii(s: signedness) (**r int, int *) + | bin_case_ff (**r float, float *) + | bin_case_if(s: signedness) (**r int, float *) + | bin_case_fi(s: signedness) (**r float, int *) + | bin_case_ll(s: signedness) (**r long, long *) + | bin_case_il(s1 s2: signedness) (**r int, long *) + | bin_case_li(s1 s2: signedness) (**r long, int *) + | bin_case_lf(s: signedness) (**r long, float *) + | bin_case_fl(s: signedness) (**r float, long *) + | bin_default. + +Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => add_case_ii Signed - | Tfloat _ _, Tfloat _ _ => add_case_ff - | Tint _ sg _, Tfloat _ _ => add_case_if sg - | Tfloat _ _, Tint _ sg _ => add_case_fi sg - | Tpointer ty a, Tint _ _ _ => add_case_pi ty a - | Tint _ _ _, Tpointer ty a => add_case_ip ty a - | _, _ => add_default + | Tint I32 Unsigned _, Tint _ _ _ => bin_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => bin_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => bin_case_ii Signed + | Tfloat _ _, Tfloat _ _ => bin_case_ff + | Tint _ sg _, Tfloat _ _ => bin_case_if sg + | Tfloat _ _, Tint _ sg _ => bin_case_fi sg + | Tlong Signed _, Tlong Signed _ => bin_case_ll Signed + | Tlong _ _, Tlong _ _ => bin_case_ll Unsigned + | Tint _ s1 _, Tlong s2 _ => bin_case_il s1 s2 + | Tlong s1 _, Tint _ s2 _ => bin_case_li s1 s2 + | Tlong sg _, Tfloat _ _ => bin_case_lf sg + | Tfloat _ _, Tlong sg _ => bin_case_fl sg + | _, _ => bin_default end. -Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_add t1 t2 with - | add_case_ii sg => (**r integer addition *) +Definition sem_binarith + (sem_int: signedness -> int -> int -> option val) + (sem_long: signedness -> int64 -> int64 -> option val) + (sem_float: float -> float -> option val) + (v1: val) (t1: type) (v2: val) (t2: type) : option val := + match classify_binarith t1 t2 with + | bin_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => sem_int sg n1 n2 + | _, _ => None + end + | bin_case_ff => + match v1, v2 with + | Vfloat n1, Vfloat n2 => sem_float n1 n2 + | _, _ => None + end + | bin_case_if sg => + match v1, v2 with + | Vint n1, Vfloat n2 => sem_float (cast_int_float sg n1) n2 + | _, _ => None + end + | bin_case_fi sg => + match v1, v2 with + | Vfloat n1, Vint n2 => sem_float n1 (cast_int_float sg n2) + | _, _ => None + end + | bin_case_ll sg => + match v1, v2 with + | Vlong n1, Vlong n2 => sem_long sg n1 n2 + | _, _ => None + end + | bin_case_il sg1 sg2 => match v1, v2 with - | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) + | Vint n1, Vlong n2 => sem_long sg2 (cast_int_long sg1 n1) n2 | _, _ => None end - | add_case_ff => (**r float addition *) + | bin_case_li sg1 sg2 => match v1, v2 with - | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2)) + | Vlong n1, Vint n2 => sem_long sg1 n1 (cast_int_long sg2 n2) | _, _ => None end - | add_case_if sg => (**r int plus float *) + | bin_case_lf sg => match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2)) + | Vlong n1, Vfloat n2 => sem_float (cast_long_float sg n1) n2 | _, _ => None end - | add_case_fi sg => (**r float plus int *) + | bin_case_fl sg => match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2))) + | Vfloat n1, Vlong n2 => sem_float n1 (cast_long_float sg n2) | _, _ => None end + | bin_default => None + end. + +(** *** Addition *) + +Inductive classify_add_cases : Type := + | add_case_pi(ty: type)(a: attr) (**r pointer, int *) + | add_case_ip(ty: type)(a: attr) (**r int, pointer *) + | add_case_pl(ty: type)(a: attr) (**r pointer, long *) + | add_case_lp(ty: type)(a: attr) (**r long, pointer *) + | add_default. (**r numerical type, numerical type *) + +Definition classify_add (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tpointer ty a, Tint _ _ _ => add_case_pi ty a + | Tint _ _ _, Tpointer ty a => add_case_ip ty a + | Tpointer ty a, Tlong _ _ => add_case_pl ty a + | Tlong _ _, Tpointer ty a => add_case_lp ty a + | _, _ => add_default + end. + +Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_add t1 t2 with | add_case_pi ty _ => (**r pointer plus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => @@ -416,59 +579,57 @@ Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) | _, _ => None end - | add_default => None -end. + | add_case_pl ty _ => (**r 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 _ => (**r 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 + (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))) + v1 t1 v2 t2 + end. (** *** Subtraction *) Inductive classify_sub_cases : Type := - | sub_case_ii(s: signedness) (**r int , int *) - | sub_case_ff (**r float , float *) - | sub_case_if(s: signedness) (**r int, float *) - | sub_case_fi(s: signedness) (**r float, int *) - | sub_case_pi(ty: type) (**r pointer, int *) + | sub_case_pi(ty: type)(a: attr) (**r pointer, int *) | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_default. + | sub_case_pl(ty: type)(a: attr) (**r pointer, long *) + | sub_default. (**r numerical type, numerical type *) Definition classify_sub (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => sub_case_ff - | Tint _ sg _, Tfloat _ _ => sub_case_if sg - | Tfloat _ _, Tint _ sg _ => sub_case_fi sg - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty + | Tpointer ty a, Tint _ _ _ => sub_case_pi ty a | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty - | _ ,_ => sub_default + | Tpointer ty a, Tlong _ _ => sub_case_pl ty a + | _, _ => sub_default end. -Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := match classify_sub t1 t2 with - | sub_case_ii sg => (**r integer subtraction *) - match v1,v2 with - | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2)) - | _, _ => None - end - | sub_case_ff => (**r float subtraction *) + | sub_case_pi ty attr => (**r pointer minus integer *) match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2)) + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) | _, _ => None end - | sub_case_if sg => (**r int minus float *) - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2)) - | _, _ => None - end - | sub_case_fi sg => (**r float minus int *) - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2))) - | _, _ => None - end - | sub_case_pi ty => (**r pointer minus integer *) + | sub_case_pl ty attr => (**r pointer minus long *) match v1,v2 with - | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | 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 => (**r pointer minus pointer *) @@ -480,255 +641,187 @@ Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := else None | _, _ => None end - | sub_default => None + | sub_default => + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.sub n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2))) + (fun n1 n2 => Some(Vfloat(Float.sub n1 n2))) + v1 t1 v2 t2 end. -(** *** Multiplication *) - -Inductive classify_mul_cases : Type:= - | mul_case_ii(s: signedness) (**r int , int *) - | mul_case_ff (**r float , float *) - | mul_case_if(s: signedness) (**r int, float *) - | mul_case_fi(s: signedness) (**r float, int *) - | mul_default. - -Definition classify_mul (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => mul_case_ff - | Tint _ sg _, Tfloat _ _ => mul_case_if sg - | Tfloat _ _, Tint _ sg _ => mul_case_fi sg - | _,_ => mul_default -end. - -Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_mul t1 t2 with - | mul_case_ii sg => - match v1,v2 with - | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2)) - | _, _ => None - end - | mul_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2)) - | _, _ => None - end - | mul_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2)) - | _, _ => None - end - | mul_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2))) - | _, _ => None - end - | mul_default => - None -end. - -(** *** Division *) - -Inductive classify_div_cases : Type:= - | div_case_ii(s: signedness) (**r int , int *) - | div_case_ff (**r float , float *) - | div_case_if(s: signedness) (**r int, float *) - | div_case_fi(s: signedness) (**r float, int *) - | div_default. - -Definition classify_div (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => div_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => div_case_ff - | Tint _ sg _, Tfloat _ _ => div_case_if sg - | Tfloat _ _, Tint _ sg _ => div_case_fi sg - | _,_ => div_default -end. - -Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_div t1 t2 with - | div_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | _,_ => None - end - | div_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => +(** *** Multiplication, division, modulus *) + +Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.mul n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2))) + (fun n1 n2 => Some(Vfloat(Float.mul n1 n2))) + v1 t1 v2 t2. + +Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => + match sg with + | Signed => if Int.eq n2 Int.zero || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone - then None else Some (Vint(Int.divs n1 n2)) - | _,_ => None - end - | div_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2)) - | _, _ => None - end - | div_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2)) - | _, _ => None - end - | div_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2))) - | _, _ => None - end - | div_default => - None -end. - -(** *** Integer-only binary operations: modulus, bitwise "and", "or", and "xor" *) - -Inductive classify_binint_cases : Type:= - | binint_case_ii(s: signedness) (**r int , int *) - | binint_default. - -Definition classify_binint (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed - | _,_ => binint_default -end. - -Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii Unsigned => - match v1, v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) - | _, _ => None - end - | binint_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => + 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))) + v1 t1 v2 t2. + +Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => + match sg with + | Signed => if Int.eq n2 Int.zero || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone - then None else Some (Vint (Int.mods n1 n2)) - | _, _ => None - end - | binint_default => - None - end. - -Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2)) - | _, _ => None - end - | binint_default => None - end. - -Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2)) - | _, _ => None - end - | binint_default => None - end. - -Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2)) - | _, _ => None - end - | binint_default => None - end. + 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) + v1 t1 v2 t2. + +Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.and n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. + +Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.or n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. + +Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.xor n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. (** *** Shifts *) +(** Shifts do not perform the usual binary conversions. Instead, + each argument is converted independently, and the signedness + of the result is always that of the first argument. *) + Inductive classify_shift_cases : Type:= - | shift_case_ii(s: signedness) (**r int , int *) + | shift_case_ii(s: signedness) (**r int , int *) + | shift_case_ll(s: signedness) (**r long, long *) + | shift_case_il(s: signedness) (**r int, long *) + | shift_case_li(s: signedness) (**r long, int *) | shift_default. Definition classify_shift (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed + | Tint I32 Unsigned _, Tlong _ _ => shift_case_il Unsigned + | Tint _ _ _, Tlong _ _ => shift_case_il Signed + | Tlong s _, Tint _ _ _ => shift_case_li s + | Tlong s _, Tlong _ _ => shift_case_ll s | _,_ => shift_default -end. + end. -Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val := +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(Int.shl n1 n2)) else None + | 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. -Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val := - match classify_shift t1 t2 with - | shift_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None - | _,_ => None - end - | shift_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None - | _, _ => None - end - | shift_default => - None - end. +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_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. (** *** Comparisons *) -Inductive classify_cmp_cases : Type:= - | cmp_case_ii(s: signedness) (**r int, int *) - | cmp_case_pp (**r pointer, pointer *) - | cmp_case_ff (**r float , float *) - | cmp_case_if(s: signedness) (**r int, float *) - | cmp_case_fi(s: signedness) (**r float, int *) - | cmp_default. +Inductive classify_cmp_cases : Type := + | cmp_case_pp (**r pointer, pointer *) + | cmp_default. (**r numerical, numerical *) Definition classify_cmp (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => cmp_case_ff - | Tint _ sg _, Tfloat _ _ => cmp_case_if sg - | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg | Tpointer _ _ , Tpointer _ _ => cmp_case_pp | Tpointer _ _ , Tint _ _ _ => cmp_case_pp | Tint _ _ _, Tpointer _ _ => cmp_case_pp - | _ , _ => cmp_default + | _, _ => cmp_default end. -Function sem_cmp (c:comparison) +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_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) - | _, _ => None - end - | cmp_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) - | _, _ => None - end | cmp_case_pp => + option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) +(* match v1,v2 with | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) | Vptr b1 ofs1, Vptr b2 ofs2 => @@ -752,22 +845,16 @@ Function sem_cmp (c:comparison) else None | _, _ => None end - | cmp_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2)) - | _, _ => None - end - | cmp_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2)) - | _, _ => None - end - | cmp_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2))) - | _, _ => None - end - | cmp_default => None +*) + | cmp_default => + sem_binarith + (fun sg n1 n2 => + Some(Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end))) + (fun sg n1 n2 => + Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end))) + (fun n1 n2 => + Some(Val.of_bool(Float.cmp c n1 n2))) + v1 t1 v2 t2 end. (** ** Function applications *) @@ -821,3 +908,249 @@ Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) := | Incr => sem_add v ty (Vint Int.one) type_int32s | Decr => sem_sub v ty (Vint Int.one) type_int32s end. + +(** * Compatibility with extensions and injections *) + +Section GENERIC_INJECTION. + +Variable f: meminj. +Variables m m': mem. + +Hypothesis valid_pointer_inj: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.valid_pointer m b1 (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. +Proof. unfold Vtrue; auto. Qed. + +Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. +Proof. unfold Vfalse; auto. Qed. + +Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. +Qed. + +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. + +Lemma sem_unary_operation_inject: + forall op v1 ty v tv1, + sem_unary_operation op v1 ty = Some v -> + val_inject f v1 tv1 -> + exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. +Proof. + unfold sem_unary_operation; intros. destruct op. + (* notbool *) + unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. + (* notint *) + unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. + (* neg *) + unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. +Qed. + +Definition optval_self_injects (ov: option val) : Prop := + match ov with + | Some (Vptr b ofs) => False + | _ => True + end. + +Remark sem_binarith_inject: + forall sem_int sem_long sem_float v1 t1 v2 t2 v v1' v2', + sem_binarith sem_int sem_long sem_float 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)) -> + exists v', sem_binarith sem_int sem_long sem_float v1' t1 v2' t2 = Some v' /\ val_inject f v v'. +Proof. + intros. + assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). + { + intros. subst ov; simpl in H6. destruct v0; contradiction || constructor. + } + exists v. + unfold sem_binarith in *; destruct (classify_binarith t1 t2); inv H0; inv H1; discriminate || eauto. +Qed. + +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'. +Proof. + intros. exists v. + unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate. + destruct (Int.ltu i0 Int.iwordsize); inv H; auto. + destruct (Int64.ltu i0 Int64.iwordsize); inv H; auto. + destruct (Int64.ltu i0 (Int64.repr 32)); inv H; auto. + destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto. +Qed. + +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. +Proof. + intros. + unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). +- (* pointer - pointer *) + destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. + replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). + simpl. TrivialInject. + symmetry. eapply val_cmpu_bool_inject; eauto. +- (* numerical - numerical *) + assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). + { + destruct b; exact I. + } + eapply sem_binarith_inject; eauto. +Qed. + +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. +Proof. + unfold sem_binary_operation; intros; destruct op. +- (* add *) + unfold sem_add in *; destruct (classify_add ty1 ty2). + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + eapply sem_binarith_inject; eauto; intros; exact I. +- (* sub *) + unfold sem_sub in *; destruct (classify_sub ty1 ty2). + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. rewrite Int.sub_add_l. auto. + + inv H0; inv H1; inv H. TrivialInject. + destruct (zeq b1 b0); try discriminate. subst b1. + rewrite H0 in H2; inv H2. rewrite zeq_true. + destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. + rewrite Int.sub_shifted. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. rewrite Int.sub_add_l. auto. + + eapply sem_binarith_inject; eauto; intros; exact I. +- (* mul *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* div *) + eapply sem_binarith_inject; eauto; intros. + destruct sg. + destruct (Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I. + destruct (Int.eq n2 Int.zero); exact I. + destruct sg. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. + destruct (Int64.eq n2 Int64.zero); exact I. + exact I. +- (* mod *) + eapply sem_binarith_inject; eauto; intros. + destruct sg. + destruct (Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I. + destruct (Int.eq n2 Int.zero); exact I. + destruct sg. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. + destruct (Int64.eq n2 Int64.zero); exact I. + exact I. +- (* and *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* or *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* xor *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* shl *) + eapply sem_shift_inject; eauto. +- (* shr *) + eapply sem_shift_inject; eauto. + (* comparisons *) +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +Qed. + +Lemma sem_cast_inject: + forall v1 ty1 ty v tv1, + sem_cast v1 ty1 ty = Some v -> + val_inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. +Proof. + unfold sem_cast; intros; destruct (classify_cast ty1 ty); + inv H0; inv H; TrivialInject. +- econstructor; eauto. +- destruct (cast_float_int si2 f0); inv H1; TrivialInject. +- destruct (cast_float_long si2 f0); inv H1; TrivialInject. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- econstructor; eauto. +Qed. + +Lemma bool_val_inject: + forall v ty b tv, + bool_val v ty = Some b -> + val_inject f v tv -> + bool_val tv ty = Some b. +Proof. + unfold bool_val; intros. + destruct (classify_bool ty); inv H0; congruence. +Qed. + +End GENERIC_INJECTION. + +Lemma sem_binary_operation_inject: + forall 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 f m m' -> + exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. +Proof. + intros. eapply sem_binary_operation_inj; eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. +Qed. + + + -- cgit