Revised semantics and compilation of 2-argument C operators to better match

"the usual binary conversions" and be more robust towards future extensions
e.g. with 32-bit float values.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 152 insertions, 194 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index d085350..e7ffc89 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -449,105 +449,72 @@ Definition sem_notint (v: val) (ty: type): option val :=
 
 (** ** Binary operators *)
 
-(** For binary operations, the "usual binary conversions", adapted to a 32-bit
-  platform, state that:
-- If both arguments are of integer type, an integer operation is performed.
-  For operations that behave differently at unsigned and signed types
-  (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/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
+(** For binary operations, the "usual binary conversions" consist in
+- determining the type at which the operation is to be performed
+  (a form of least upper bound of the types of the two arguments);
+- casting the two arguments to this common type;
+- performing the operation at that 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.
+  | bin_case_i (s: signedness)         (**r at int type *)
+  | bin_case_l (s: signedness)         (**r at long int type *)
+  | bin_case_f                         (**r at float type *)
+  | bin_default.                       (**r error *)
 
 Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
-  match typeconv ty1, typeconv ty2 with
-  | 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
+  match ty1, ty2 with
+  | Tint I32 Unsigned _, Tint _ _ _ => bin_case_i Unsigned
+  | Tint _ _ _, Tint I32 Unsigned _ => bin_case_i Unsigned
+  | Tint _ _ _, Tint _ _ _ => bin_case_i Signed
+  | Tlong Signed _, Tlong Signed _ => bin_case_l Signed
+  | Tlong _ _, Tlong _ _ => bin_case_l Unsigned
+  | Tlong sg _, Tint _ _ _ => bin_case_l sg
+  | Tint _ _ _, Tlong sg _ => bin_case_l sg
+  | Tfloat _ _, (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => bin_case_f
+  | (Tint _ _ _ | Tlong _ _), Tfloat _ _ => bin_case_f
   | _, _ => bin_default
   end.
 
+Definition binarith_type (c: binarith_cases) : type :=
+  match c with
+  | bin_case_i sg => Tint I32 sg noattr
+  | bin_case_l sg => Tlong sg noattr
+  | bin_case_f    => Tfloat F64 noattr
+  | bin_default   => Tvoid
+  end.
+
 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 :=
+  let c := classify_binarith t1 t2 in
+  let t := binarith_type c in
+  match sem_cast v1 t1 t with
+  | None => None
+  | Some v1' =>
+  match sem_cast v2 t2 t with
+  | None => None
+  | Some v2' =>
   match classify_binarith t1 t2 with
-  | bin_case_ii sg =>
-      match v1, v2 with
+  | bin_case_i sg =>
+      match v1', v2' with
       | Vint n1, Vint n2 => sem_int sg n1 n2
       | _,  _ => None
       end
-  | bin_case_ff =>
-      match v1, v2 with
+  | bin_case_f =>
+      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
+  | bin_case_l 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, Vlong n2 => sem_long sg2 (cast_int_long sg1 n1) n2
-      | _,  _ => None
-      end
-  | bin_case_li sg1 sg2 =>
-      match v1, v2 with
-      | Vlong n1, Vint n2 => sem_long sg1 n1 (cast_int_long sg2 n2)
-      | _,  _ => None
-      end
-  | bin_case_lf sg =>
-      match v1, v2 with
-      | Vlong n1, Vfloat n2 => sem_float (cast_long_float sg n1) n2
-      | _, _ => None
-      end
-  | bin_case_fl sg =>
-      match v1, v2 with
-      | Vfloat n1, Vlong n2 => sem_float n1 (cast_long_float sg n2)
-      | _, _ => None
-      end
   | bin_default => None
-  end.
+  end end end.
 
 (** *** Addition *)
 
@@ -957,6 +924,22 @@ Ltac TrivialInject :=
   | _ => idtac
   end.
 
+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 sem_unary_operation_inject:
   forall op v1 ty v tv1,
   sem_unary_operation op v1 ty = Some v ->
@@ -992,8 +975,15 @@ Proof.
   {
     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.
+  unfold sem_binarith in *.
+  set (c := classify_binarith t1 t2) in *.
+  set (t := binarith_type c) in *.
+  destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate.
+  destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate.
+  exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1).
+  exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2).
+  rewrite C1'; rewrite C2'.
+  destruct c; inv INJ1; inv INJ2; discriminate || eauto.
 Qed.
 
 Remark sem_shift_inject:
@@ -1119,22 +1109,6 @@ Proof.
 - 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 ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index c45e094..ad89a2d 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -84,9 +84,6 @@ Definition make_longoffloat (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Olonguoffloat e
   end.
 
-(** [make_boolean e ty] returns a Csharpminor expression that evaluates
-   to the boolean value of [e].  *)
-
 Definition make_cmp_ne_zero (e: expr) :=
   match e with
   | Ebinop (Ocmp c) e1 e2 => e
@@ -97,6 +94,49 @@ Definition make_cmp_ne_zero (e: expr) :=
   | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
   end.
 
+(** [make_cast from to e] applies to [e] the numeric conversions needed
+   to transform a result of type [from] to a result of type [to]. *)
+
+Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
+  match sz, si with
+  | I8, Signed => Eunop Ocast8signed e  
+  | I8, Unsigned => Eunop Ocast8unsigned e  
+  | I16, Signed => Eunop Ocast16signed e  
+  | I16, Unsigned => Eunop Ocast16unsigned e  
+  | I32, _ => e
+  | IBool, _ => make_cmp_ne_zero e
+  end.
+
+Definition make_cast_float (e: expr) (sz: floatsize) :=
+  match sz with
+  | F32 => Eunop Osingleoffloat e
+  | F64 => e
+  end.
+
+Definition make_cast (from to: type) (e: expr) :=
+  match classify_cast from to with
+  | cast_case_neutral => OK e
+  | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
+  | cast_case_f2f sz2 => OK (make_cast_float e sz2)
+  | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2)
+  | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
+  | cast_case_l2l => OK e
+  | cast_case_i2l si1 => OK (make_longofint e si1)
+  | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
+  | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2)
+  | cast_case_f2l si2 => OK (make_longoffloat e si2)
+  | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
+  | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
+  | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
+  | cast_case_struct id1 fld1 id2 fld2 => OK e
+  | cast_case_union id1 fld1 id2 fld2 => OK e
+  | cast_case_void => OK e
+  | cast_case_default => Error (msg "Cshmgen.make_cast")
+  end.
+
+(** [make_boolean e ty] returns a Csharpminor expression that evaluates
+   to the boolean value of [e].  *)
+
 Definition make_boolean (e: expr) (ty: type) :=
   match classify_bool ty with
   | bool_case_i => make_cmp_ne_zero e
@@ -106,6 +146,8 @@ Definition make_boolean (e: expr) (ty: type) :=
   | bool_default => e   (**r should not happen *)
   end.
 
+(** Unary operators *)
+
 Definition make_notbool (e: expr) (ty: type) :=
   match classify_bool ty with
   | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero))
@@ -130,22 +172,20 @@ Definition make_notint (e: expr) (ty: type) :=
   | _ => Error (msg "Cshmgen.make_notint")
   end.
 
+(** Binary operators *)
+
 Definition make_binarith (iop iopu fop lop lopu: binary_operation)
                          (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_binarith ty1 ty2 with
-  | bin_case_ii Signed => OK (Ebinop iop e1 e2)
-  | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2)
-  | bin_case_ff => OK (Ebinop fop e1 e2)
-  | bin_case_if sg => OK (Ebinop fop (make_floatofint e1 sg) e2)
-  | bin_case_fi sg => OK (Ebinop fop e1 (make_floatofint e2 sg))
-  | bin_case_ll Signed => OK (Ebinop lop e1 e2)
-  | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2)
-  | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2)
-  | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2)
-  | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2))
-  | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2))
-  | bin_case_lf sg => OK (Ebinop fop (make_floatoflong e1 sg) e2)
-  | bin_case_fl sg => OK (Ebinop fop e1 (make_floatoflong e2 sg))
+  let c := classify_binarith ty1 ty2 in
+  let ty := binarith_type c in
+  do e1' <- make_cast ty1 ty e1;
+  do e2' <- make_cast ty2 ty e2;
+  match c with
+  | bin_case_i Signed => OK (Ebinop iop e1' e2')
+  | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
+  | bin_case_f => OK (Ebinop fop e1' e2')
+  | bin_case_l Signed => OK (Ebinop lop e1' e2')
+  | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
   | bin_default => Error (msg "Cshmgen.make_binarith")
   end.
 
@@ -190,16 +230,16 @@ Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 
 Definition make_binarith_int (iop iopu lop lopu: binary_operation)
                              (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_binarith ty1 ty2 with
-  | bin_case_ii Signed => OK (Ebinop iop e1 e2)
-  | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2)
-  | bin_case_ll Signed => OK (Ebinop lop e1 e2)
-  | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2)
-  | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2)
-  | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2)
-  | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2))
-  | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2))
-  | _ => Error (msg "Cshmgen.make_binarith_int")
+  let c := classify_binarith ty1 ty2 in
+  let ty := binarith_type c in
+  do e1' <- make_cast ty1 ty e1;
+  do e2' <- make_cast ty2 ty e2;
+  match c with
+  | bin_case_i Signed => OK (Ebinop iop e1' e2')
+  | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
+  | bin_case_l Signed => OK (Ebinop lop e1' e2')
+  | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
+  | bin_case_f | bin_default => Error (msg "Cshmgen.make_binarith_int")
   end.
 
 Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -214,22 +254,6 @@ Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   make_binarith_int Oxor Oxor Oxorl Oxorl e1 ty1 e2 ty2.
 
-(*
-Definition make_shift (iop iopu lop lopu: binary_operation)
-                      (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_shift ty1 ty2 with
-  | shift_case_ii Signed => OK (Ebinop iop e1 e2)
-  | shift_case_ii Unsigned => OK (Ebinop iopu e1 e2)
-  | shift_case_li Signed => OK (Ebinop lop e1 e2)
-  | shift_case_li Unsigned => OK (Ebinop lopu e1 e2)
-  | shift_case_il Signed => OK (Ebinop iop e1 (Eunop Ointoflong e2))
-  | shift_case_il Unsigned => OK (Ebinop iopu e1 (Eunop Ointoflong e2))
-  | shift_case_ll Signed => OK (Ebinop lop e1 (Eunop Ointoflong e2))
-  | shift_case_ll Unsigned => OK (Ebinop lopu e1 (Eunop Ointoflong e2))
-  | shift_default => Error (msg "Cshmgen.make_shift")
-  end.
-*)
-
 Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_shift ty1 ty2 with
   | shift_case_ii _ => OK (Ebinop Oshl e1 e2)
@@ -261,46 +285,6 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
       make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2
   end.
 
-(** [make_cast from to e] applies to [e] the numeric conversions needed
-   to transform a result of type [from] to a result of type [to]. *)
-
-Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
-  match sz, si with
-  | I8, Signed => Eunop Ocast8signed e  
-  | I8, Unsigned => Eunop Ocast8unsigned e  
-  | I16, Signed => Eunop Ocast16signed e  
-  | I16, Unsigned => Eunop Ocast16unsigned e  
-  | I32, _ => e
-  | IBool, _ => make_cmp_ne_zero e
-  end.
-
-Definition make_cast_float (e: expr) (sz: floatsize) :=
-  match sz with
-  | F32 => Eunop Osingleoffloat e
-  | F64 => e
-  end.
-
-Definition make_cast (from to: type) (e: expr) :=
-  match classify_cast from to with
-  | cast_case_neutral => OK e
-  | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
-  | cast_case_f2f sz2 => OK (make_cast_float e sz2)
-  | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2)
-  | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
-  | cast_case_l2l => OK e
-  | cast_case_i2l si1 => OK (make_longofint e si1)
-  | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
-  | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2)
-  | cast_case_f2l si2 => OK (make_longoffloat e si2)
-  | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
-  | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
-  | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
-  | cast_case_struct id1 fld1 id2 fld2 => OK e
-  | cast_case_union id1 fld1 id2 fld2 => OK e
-  | cast_case_void => OK e
-  | cast_case_default => Error (msg "Cshmgen.make_cast")
-  end.
-
 (** [make_load addr ty_res] loads a value of type [ty_res] from
    the memory location denoted by the Csharpminor expression [addr].
    If [ty_res] is an array or function type, returns [addr] instead,
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index de3b8df..953e690 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -377,21 +377,19 @@ Lemma make_binarith_correct:
     (sem_binarith sem_int sem_long sem_float).
 Proof.
   red; unfold make_binarith, sem_binarith;
-  intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_binarith tya tyb); inv MAKE;
-  destruct va; try discriminate; destruct vb; try discriminate.
+  intros until m; intros SEM MAKE EV1 EV2.
+  set (cls := classify_binarith tya tyb) in *.
+  set (ty := binarith_type cls) in *.
+  monadInv MAKE.
+  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
+  exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
+  destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
 - destruct s; inv H0; econstructor; eauto with cshm. 
   rewrite iop_ok; auto. rewrite iopu_ok; auto.
-- erewrite <- fop_ok in SEM; eauto with cshm.
-- erewrite <- fop_ok in SEM; eauto with cshm.
-- erewrite <- fop_ok in SEM; eauto with cshm.
 - destruct s; inv H0; econstructor; eauto with cshm. 
   rewrite lop_ok; auto. rewrite lopu_ok; auto.
-- destruct s2; inv H0; econstructor; eauto with cshm. 
-  rewrite lop_ok; auto. rewrite lopu_ok; auto.
-- destruct s1; inv H0; econstructor; eauto with cshm. 
-  rewrite lop_ok; auto. rewrite lopu_ok; auto.
-- erewrite <- fop_ok in SEM; eauto with cshm.
 - erewrite <- fop_ok in SEM; eauto with cshm.
 Qed.
 
@@ -401,17 +399,19 @@ Lemma make_binarith_int_correct:
     (sem_binarith sem_int sem_long (fun x y => None)).
 Proof.
   red; unfold make_binarith_int, sem_binarith;
-  intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_binarith tya tyb); inv MAKE;
-  destruct va; try discriminate; destruct vb; try discriminate.
+  intros until m; intros SEM MAKE EV1 EV2.
+  set (cls := classify_binarith tya tyb) in *.
+  set (ty := binarith_type cls) in *.
+  monadInv MAKE.
+  destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate.
+  destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate.
+  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
+  exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
+  destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
 - destruct s; inv H0; econstructor; eauto with cshm. 
   rewrite iop_ok; auto. rewrite iopu_ok; auto.
 - destruct s; inv H0; econstructor; eauto with cshm. 
   rewrite lop_ok; auto. rewrite lopu_ok; auto.
-- destruct s2; inv H0; econstructor; eauto with cshm. 
-  rewrite lop_ok; auto. rewrite lopu_ok; auto.
-- destruct s1; inv H0; econstructor; eauto with cshm. 
-  rewrite lop_ok; auto. rewrite lopu_ok; auto.
 Qed.
 
 End MAKE_BIN.