Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

6 files changed, 227 insertions, 65 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 37527940..dbfe5e5d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -153,14 +153,10 @@ let ais_annot_functions =
       true);]
   else
     []
-
-let builtin_ternary suffix typ =
-  ("__builtin_ternary_" ^ suffix),
-  (typ, [TInt(IInt, []); typ; typ], false);;
   
 let builtins_generic = {
-  Builtins.typedefs = [];
-  Builtins.functions =
+  builtin_typedefs = [];
+  builtin_functions =
     ais_annot_functions
       @
     [
@@ -184,15 +180,12 @@ let builtins_generic = {
             TPtr(TVoid [AConst], []);
             TInt(IULong, []);
             TInt(IULong, [])],
-           false);
-    (* Ternary operator *)
-    builtin_ternary "uint" (TInt(IUInt, []));
-    builtin_ternary "ulong" (TInt(IULong, []));
-    builtin_ternary "int" (TInt(IInt, []));
-    builtin_ternary "long" (TInt(ILong, []));
-    builtin_ternary "double" (TFloat(FDouble, []));
-    builtin_ternary "float" (TFloat(FFloat, []));
-	    
+          false);
+    (* Selection *)
+    "__builtin_sel",
+        (TVoid [],
+           [TInt(C.IBool, [])],
+           true);
     (* Annotations *)
     "__builtin_annot",
         (TVoid [],
@@ -336,9 +329,12 @@ let builtins_generic = {
 
 (* Add processor-dependent builtins *)
 
-let builtins =
-  Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
-    functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions })
+let builtins = {
+  builtin_typedefs =
+    builtins_generic.builtin_typedefs @ CBuiltins.builtins.builtin_typedefs;
+  builtin_functions =
+    builtins_generic.builtin_functions @ CBuiltins.builtins.builtin_functions
+}
 
 (** ** The known attributes *)
 
@@ -632,6 +628,12 @@ and convertParams env = function
     | [] -> Tnil
     | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem)
 
+(* Convert types for the arguments to a function call.  The types for
+   fixed arguments are taken from the function prototype.  The types
+   for other arguments (variable-argument function or unprototyped K&R
+   functions) are taken from the types of the function arguments,
+   after default argument conversion. *)
+
 let rec convertTypArgs env tl el =
   match tl, el with
   | _, [] -> Tnil
@@ -641,6 +643,20 @@ let rec convertTypArgs env tl el =
   | (id, t1) :: tl, e1 :: el ->
       Tcons(convertTyp env t1, convertTypArgs env tl el)
 
+(* Convert types for the arguments to inline asm statements and to
+   the special built-in functions __builtin_annot, __builtin_ais_annot_
+   and __builtin_debug.  The types are taken from the types of the
+   arguments, after performing the usual unary conversions.
+   Hence char becomes int but float remains float and is not promoted
+   to double.  The goal is to preserve the representation of the arguments
+   and avoid inserting compiled code to convert the arguments. *)
+
+let rec convertTypAnnotArgs env = function
+  | [] -> Tnil
+  | e1 :: el ->
+      Tcons(convertTyp env (Cutil.unary_conversion env e1.etyp),
+            convertTypAnnotArgs env el)
+
 let convertField env f =
   if f.fld_bitfield <> None then
     unsupported "bit field in struct or union (consider adding option [-fbitfields])";
@@ -881,7 +897,7 @@ let rec convertExpr env e =
         | {edesc = C.EVar id} :: args2 -> (id.name, args2)
         | _::args2 -> error "argument 2 of '__builtin_debug' must be either a string literal or a variable"; ("", args2)
         | [] -> assert false (* catched earlier *) in
-      let targs2 = convertTypArgs env [] args2 in
+      let targs2 = convertTypAnnotArgs env args2 in
       Ebuiltin(
          AST.EF_debug(P.of_int64 kind, intern_string text,
                  typlist_of_typelist targs2),
@@ -890,7 +906,7 @@ let rec convertExpr env e =
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
-          let targs1 = convertTypArgs env [] args1 in
+          let targs1 = convertTypAnnotArgs env args1 in
           Ebuiltin(
              AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1),
             targs1, convertExprList env args1, convertTyp env e.etyp)
@@ -918,7 +934,7 @@ let rec convertExpr env e =
         let file,line = !currentLocation in
         let fun_name = !currentFunction in
         let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in
-        let targs1 = convertTypArgs env [] args1 in
+        let targs1 = convertTypAnnotArgs env args1 in
         AisAnnot.validate_ais_annot env !currentLocation txt args1;
           Ebuiltin(
              AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1),
@@ -954,6 +970,10 @@ let rec convertExpr env e =
                Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)),
                Tvoid)
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_sel"}}, [arg1; arg2; arg3]) ->
+      ewrap (Ctyping.eselection (convertExpr env arg1)
+                                (convertExpr env arg2) (convertExpr env arg3))
+
   | C.ECall({edesc = C.EVar {name = "printf"}}, args)
     when !Clflags.option_interp ->
       let targs = convertTypArgs env [] args
@@ -1019,14 +1039,14 @@ let convertAsm loc env txt outputs inputs clobber =
     match output' with None -> TVoid [] | Some e -> e.etyp in
   (* Build the Ebuiltin expression *)
   let e =
-    let tinputs = convertTypArgs env [] inputs' in
+    let tinputs = convertTypAnnotArgs env inputs' in
     let toutput = convertTyp env ty_res in
     Ebuiltin( AST.EF_inline_asm(coqstring_of_camlstring txt',
                            signature_of_type tinputs toutput  AST.cc_default,
                            clobber'),
              tinputs,
              convertExprList env inputs',
-             convertTyp env ty_res) in
+             toutput) in
   (* Add an assignment to the output, if any *)
   match output' with
   | None -> e
@@ -1257,7 +1277,7 @@ let convertFundecl env (sto, id, ty, optinit) =
       then  AST.EF_runtime(id'', sg)
       else
     if Str.string_match re_builtin id.name 0
-    && List.mem_assoc id.name builtins.Builtins.functions
+    && List.mem_assoc id.name builtins.builtin_functions
     then AST.EF_builtin(id'', sg)
     else AST.EF_external(id'', sg) in
   (id',  AST.Gfun(Ctypes.External(ef, args, res, cconv)))
@@ -1456,7 +1476,7 @@ let convertProgram p =
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear wstringTable;
-  let p = cleanupGlobals (Builtins.declarations() @ p) in
+  let p = cleanupGlobals (Env.initial_declarations() @ p) in
   try
     let env = translEnv Env.empty p in
     let typs = convertCompositedefs env [] p in
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7f5fe355..e6bf2129 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -16,7 +16,7 @@ Require Import FunInd.
 Require Import Axioms Classical.
 Require Import String Coqlib Decidableplus.
 Require Import Errors Maps Integers Floats.
-Require Import AST Values Memory Events Globalenvs Determinism.
+Require Import AST Values Memory Events Globalenvs Builtins Determinism.
 Require Import Ctypes Cop Csyntax Csem.
 Require Cstrategy.
 
@@ -501,12 +501,19 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   Some(w, E0, Vundef, m).
 
+Definition do_builtin_or_external (name: string) (sg: signature)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match lookup_builtin_function name sg with
+  | Some bf => match builtin_function_sem bf vargs with Some v => Some(w, E0, v, m) | None => None end
+  | None    => do_external_function name sg ge w vargs m
+  end.
+
 Definition do_external (ef: external_function):
        world -> list val -> mem -> option (world * trace * val * mem) :=
   match ef with
   | EF_external name sg => do_external_function name sg ge
-  | EF_builtin name sg => do_external_function name sg ge
-  | EF_runtime name sg => do_external_function name sg ge
+  | EF_builtin name sg => do_builtin_or_external name sg
+  | EF_runtime name sg => do_builtin_or_external name sg
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
   | EF_malloc => do_ef_malloc
@@ -523,17 +530,26 @@ Lemma do_ef_external_sound:
   do_external ef w vargs m = Some(w', t, vres, m') ->
   external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
 Proof with try congruence.
+  intros until m'.
   assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz).
   { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; 
     intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. }
-  intros until m'.
+  assert (BF_EX: forall name sg,
+    do_builtin_or_external name sg w vargs m = Some (w', t, vres, m') ->
+    builtin_or_external_sem name sg ge vargs m t vres m' /\ possible_trace w t w').
+  { unfold do_builtin_or_external, builtin_or_external_sem; intros. 
+    destruct (lookup_builtin_function name sg ) as [bf|].
+  - destruct (builtin_function_sem bf vargs) as [vres1|] eqn:BF; inv H.
+    split. constructor; auto. constructor.
+  - eapply do_external_function_sound; eauto.
+  }
   destruct ef; simpl.
 (* EF_external *)
   eapply do_external_function_sound; eauto.
 (* EF_builtin *)
-  eapply do_external_function_sound; eauto.
+  eapply BF_EX; eauto.
 (* EF_runtime *)
-  eapply do_external_function_sound; eauto.
+  eapply BF_EX; eauto.
 (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -575,17 +591,26 @@ Lemma do_ef_external_complete:
   external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
   do_external ef w vargs m = Some(w', t, vres, m').
 Proof.
+  intros.
   assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n).
   { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. 
     rewrite Ptrofs.of_int64_to_int64; auto.
     rewrite Ptrofs.of_int_to_int; auto. }
-  intros. destruct ef; simpl in *.
+  assert (BF_EX: forall name sg,
+    builtin_or_external_sem name sg ge vargs m t vres m' ->
+    do_builtin_or_external name sg w vargs m = Some (w', t, vres, m')).
+  { unfold do_builtin_or_external, builtin_or_external_sem; intros.
+    destruct (lookup_builtin_function name sg) as [bf|].
+  - inv H1. inv H0. rewrite H2. auto.
+  - eapply do_external_function_complete; eauto.
+  }
+  destruct ef; simpl in *.
 (* EF_external *)
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
-  eapply do_external_function_complete; eauto.
+  eapply BF_EX; eauto.
 (* EF_runtime *)
-  eapply do_external_function_complete; eauto.
+  eapply BF_EX; eauto.
 (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index c395a2cb..782fb32a 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -1580,6 +1580,27 @@ Proof.
   intros. apply cast_val_casted. eapply cast_val_is_casted; eauto.
 Qed.
 
+(** Moreover, casted values belong to the machine type corresponding to the
+    C type. *)
+
+Lemma val_casted_has_type:
+  forall v ty, val_casted v ty -> ty <> Tvoid -> Val.has_type v (typ_of_type ty).
+Proof.
+  intros. inv H; simpl typ_of_type.
+- exact I.
+- exact I.
+- exact I.
+- exact I.
+- apply Val.Vptr_has_type.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- apply Val.Vptr_has_type.
+- apply Val.Vptr_has_type.
+- congruence.
+Qed.
+
 (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *)
 
 Module ArithConv.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 0c3e00de..a76a14ba 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -15,19 +15,9 @@
 
 (** Dynamic semantics for the Compcert C language *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
+Require Import Coqlib Errors Maps.
+Require Import Integers Floats Values AST Memory Builtins Events Globalenvs.
+Require Import Ctypes Cop Csyntax.
 Require Import Smallstep.
 
 (** * Operational semantics *)
@@ -437,6 +427,59 @@ Definition not_stuck (e: expr) (m: mem) : Prop :=
   forall k C e' ,
   context k RV C -> e = C e' -> imm_safe k e' m.
 
+(** ** Derived forms. *)
+
+(** The following are admissible reduction rules for some derived forms
+  of the CompCert C language.  They help showing that the derived forms
+  make sense. *)
+
+Lemma red_selection:
+  forall v1 ty1 v2 ty2 v3 ty3 ty m b v2' v3',
+  ty <> Tvoid ->
+  bool_val v1 ty1 m = Some b ->
+  sem_cast v2 ty2 ty m = Some v2' ->
+  sem_cast v3 ty3 ty m = Some v3' ->
+  rred (Eselection (Eval v1 ty1) (Eval v2 ty2) (Eval v3 ty3) ty) m
+    E0 (Eval (if b then v2' else v3') ty) m.
+Proof.
+  intros. unfold Eselection.
+  set (t := typ_of_type ty).
+  set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default).
+  assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))).
+  { unfold sg, t; destruct ty as   [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
+    simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
+  set (v' := if b then v2' else v3').
+  assert (C: val_casted v' ty).
+  { unfold v'; destruct b; eapply cast_val_is_casted; eauto. }
+  assert (EQ: Val.normalize v' t = v').
+  { apply Val.normalize_idem. apply val_casted_has_type; auto. }
+  econstructor.
+- constructor. rewrite cast_bool_bool_val, H0. eauto.
+  constructor. eauto.
+  constructor. eauto.
+  constructor.
+- red. red. rewrite LK. constructor. simpl. rewrite <- EQ.
+  destruct b; auto.
+Qed.
+
+Lemma ctx_selection_1:
+  forall k C r2 r3 ty, context k RV C -> context k RV (fun x => Eselection (C x) r2 r3 ty).
+Proof.
+  intros. apply ctx_builtin. constructor; auto.
+Qed.
+
+Lemma ctx_selection_2:
+  forall k r1 C r3 ty, context k RV C -> context k RV (fun x => Eselection r1 (C x) r3 ty).
+Proof.
+  intros. apply ctx_builtin. constructor; constructor; auto.
+Qed.
+
+Lemma ctx_selection_3:
+  forall k r1 r2 C ty, context k RV C -> context k RV (fun x => Eselection r1 r2 (C x) ty).
+Proof.
+  intros. apply ctx_builtin. constructor; constructor; constructor; auto.
+Qed.
+
 End EXPR.
 
 (** ** Transition semantics. *)
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 00565309..c34a5e13 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -100,6 +100,18 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
   Eassignop (match id with Incr => Oadd | Decr => Osub end)
             l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty.
 
+(** Selection is a conditional expression that always evaluates both arms
+  and can be implemented by "conditional move" instructions.
+  It is expressed as an invocation of a builtin function. *)
+
+Definition Eselection (r1 r2 r3: expr) (ty: type) :=
+  let t := typ_of_type ty in
+  let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+  Ebuiltin (EF_builtin "__builtin_sel"%string sg)
+           (Tcons type_bool (Tcons ty (Tcons ty Tnil)))
+           (Econs r1 (Econs r2 (Econs r3 Enil)))
+           ty.
+
 (** Extract the type part of a type-annotated expression. *)
 
 Definition typeof (a: expr) : type :=
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index ba1d34fb..b92a9bac 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -18,7 +18,7 @@
 Require Import String.
 Require Import Coqlib Maps Integers Floats Errors.
 Require Import AST Linking.
-Require Import Values Memory Globalenvs Events.
+Require Import Values Memory Globalenvs Builtins Events.
 Require Import Ctypes Cop Csyntax Csem.
 
 Local Open Scope error_monad_scope.
@@ -392,13 +392,17 @@ Inductive wt_rvalue : expr -> Prop :=
       classify_fun (typeof r1) = fun_case_f tyargs tyres cconv ->
       wt_arguments rargs tyargs ->
       wt_rvalue (Ecall r1 rargs tyres)
-  | wt_Ebuiltin: forall ef tyargs rargs,
+  | wt_Ebuiltin: forall ef tyargs rargs ty,
       wt_exprlist rargs ->
       wt_arguments rargs tyargs ->
-      (* This is specialized to builtins returning void, the only
-         case generated by C2C. *)
-      sig_res (ef_sig ef) = None ->
-      wt_rvalue (Ebuiltin ef tyargs rargs Tvoid)
+      (* This typing rule is specialized to the builtin invocations generated
+         by C2C, which are either __builtin_sel or builtins returning void. *)
+         (ty = Tvoid /\ sig_res (ef_sig ef) = None)
+      \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil))
+          /\ let t := typ_of_type ty in
+             let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+             ef = EF_builtin "__builtin_sel"%string sg) ->
+      wt_rvalue (Ebuiltin ef tyargs rargs ty)
   | wt_Eparen: forall r tycast ty,
       wt_rvalue r ->
       wt_cast (typeof r) tycast -> subtype tycast ty ->
@@ -745,6 +749,12 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist)
   then OK (Ebuiltin ef tyargs args tyres)
   else Error (msg "builtin: wrong type decoration").
 
+Definition eselection (r1 r2 r3: expr) : res expr :=
+  do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
+  do y1 <- check_bool (typeof r1);
+  do ty <- type_conditional (typeof r2) (typeof r3);
+  OK (Eselection r1 r2 r3 ty).
+
 Definition sdo (a: expr) : res statement :=
   do x <- check_rval a; OK (Sdo a).
 
@@ -981,6 +991,15 @@ Proof.
   destruct i; auto.
 Qed.
 
+Lemma wt_bool_cast:
+  forall ty, wt_bool ty -> wt_cast ty type_bool.
+Proof.
+  unfold wt_bool, wt_cast; unfold classify_bool; intros.
+  destruct ty; simpl in *; try congruence;
+  try (destruct Archi.ptr64; congruence).
+  destruct f; congruence.
+Qed.
+
 Lemma wt_cast_int:
   forall i1 s1 a1 i2 s2 a2, wt_cast (Tint i1 s1 a1) (Tint i2 s2 a2).
 Proof.
@@ -1225,6 +1244,17 @@ Proof.
   econstructor; eauto. eapply check_arguments_sound; eauto.
 Qed.
 
+Lemma eselection_sound:
+  forall r1 r2 r3 a, eselection r1 r2 r3 = OK a ->
+  wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.
+Proof.
+  intros. monadInv H. apply type_conditional_cast in EQ3. destruct EQ3.
+  eapply wt_Ebuiltin.
+  repeat (constructor; eauto with ty).
+  repeat (constructor; eauto with ty). apply wt_bool_cast; eauto with ty.
+  right; auto.
+Qed.
+
 Lemma sdo_sound:
   forall a s, sdo a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s.
 Proof.
@@ -1632,15 +1662,6 @@ Proof.
   destruct f; discriminate.
 Qed.
 
-Lemma wt_bool_cast:
-  forall ty, wt_bool ty -> wt_cast ty type_bool.
-Proof.
-  unfold wt_bool, wt_cast; unfold classify_bool; intros.
-  destruct ty; simpl in *; try congruence;
-  try (destruct Archi.ptr64; congruence).
-  destruct f; congruence.
-Qed.
-
 Lemma wt_cast_self:
   forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2.
 Proof.
@@ -1725,7 +1746,27 @@ Proof.
   constructor; auto.
 - (* comma *) auto.
 - (* paren *) inv H3. constructor. apply H5. eapply pres_sem_cast; eauto.
-- (* builtin *) subst. auto with ty.
+- (* builtin *) subst. destruct H7 as [(A & B) | (A & B)].
++ subst ty. auto with ty.
++ simpl in B. set (T := typ_of_type ty) in *. 
+  set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *.
+  assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))).
+  { unfold sg, T; destruct ty as   [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
+    simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
+  subst ef. red in H0. red in H0. rewrite LK in H0. inv H0. 
+  inv H. inv H8. inv H9. inv H10. simpl in H1.
+  assert (A: val_casted v1 type_bool) by (eapply cast_val_is_casted; eauto).
+  inv A. 
+  set (v' := if Int.eq n Int.zero then v4 else v2) in *.
+  constructor.
+  destruct (type_eq ty Tvoid).
+  subst. constructor.
+  inv H1.
+  assert (C: val_casted v' ty).
+  { unfold v'; destruct (Int.eq n Int.zero); eapply cast_val_is_casted; eauto. }
+  assert (EQ: Val.normalize v' T = v').
+  { apply Val.normalize_idem. apply val_casted_has_type; auto. }
+  rewrite EQ. apply wt_val_casted; auto.
 Qed.
 
 Lemma wt_lred:
@@ -1767,8 +1808,8 @@ with wt_subexprlist:
   wt_exprlist cenv tenv (C a) ->
   wt_expr_kind cenv tenv from a.
 Proof.
-  destruct 1; intros WT; auto; inv WT; eauto.
-  destruct 1; intros WT; inv WT; eauto.
+- destruct 1; intros WT; auto; inv WT; eauto.
+- destruct 1; intros WT; inv WT; eauto.
 Qed.
 
 Lemma typeof_context: