From 92b2d35f701ae55129fe2c34066d59d045460852 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 19:00:36 +0200 Subject: Change the expected types for arguments to __builtin_annot, and extended asm Currently, the arguments to __builtin_annot, __builtin_ais_annot, __builtin_debug, and extended asm statements are treated like arguments to an unprototyped or vararg function call. In particular, arguments of type "float" are converted to "double", generating useless code. To avoid this extra, useless conversion, this commit changes the types expected for the arguments to these built-ins and to extended asm statements. Now they are the types of the arguments themselves, after performing the usual unary conversions (e.g. char -> int), but without the problematic float -> double conversion. This ensures that no code is generated to change the representation of the arguments. --- cfrontend/C2C.ml | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5428d0cc..b81bd022 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -596,6 +596,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 @@ -605,6 +611,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])"; @@ -845,7 +865,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), @@ -854,7 +874,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) @@ -882,7 +902,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), @@ -983,14 +1003,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 -- cgit From fb20aab431a768299118ed30822af59cab13325e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 14:55:31 +0200 Subject: Remove the cparser/Builtins module Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`. --- cfrontend/C2C.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b81bd022..4d0e52e1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -155,8 +155,8 @@ let ais_annot_functions = [] let builtins_generic = { - Builtins.typedefs = []; - Builtins.functions = + builtin_typedefs = []; + builtin_functions = ais_annot_functions @ [ @@ -300,9 +300,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 *) @@ -1233,7 +1236,7 @@ let convertFundecl env (sto, id, ty, optinit) = if id.name = "free" then AST.EF_free else if Str.string_match re_runtime id.name 0 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))) @@ -1432,7 +1435,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 -- cgit From d08b080747225160b80c3f04bdfd9cd67550b425 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 16:25:40 +0200 Subject: Give formal semantics to some built-in functions and run-time functions This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later. --- cfrontend/Cexec.v | 43 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 34 insertions(+), 9 deletions(-) (limited to 'cfrontend') 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. -- cgit From 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 4 Jul 2019 17:49:11 +0200 Subject: Make __builtin_sel available from C source code It is type-checked like a conditional expression then translated to a call to the known builtin function. --- cfrontend/C2C.ml | 9 +++++++ cfrontend/Cop.v | 21 +++++++++++++++ cfrontend/Csem.v | 69 ++++++++++++++++++++++++++++++++++++++--------- cfrontend/Csyntax.v | 12 +++++++++ cfrontend/Ctyping.v | 77 ++++++++++++++++++++++++++++++++++++++++------------- 5 files changed, 157 insertions(+), 31 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4d0e52e1..2e6bbe67 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -181,6 +181,11 @@ let builtins_generic = { TInt(IULong, []); TInt(IULong, [])], false); + (* Selection *) + "__builtin_sel", + (TVoid [], + [TInt(C.IBool, [])], + true); (* Annotations *) "__builtin_annot", (TVoid [], @@ -941,6 +946,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 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: -- cgit