From a335e621aaa85a7f73b16c121261dbecf8e68340 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Jul 2011 16:17:08 +0000 Subject: In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 223 ++++++++++++++++++++++++------------------------------- 1 file changed, 96 insertions(+), 127 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 21dd57e1..5461353f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -30,7 +30,7 @@ Require Import Smallstep. (** * Semantics of type-dependent operations *) -(** Semantics of casts. [cast v1 t1 t2 v2] holds if value [v1], +(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], viewed with static type [t1], can be cast to type [t2], resulting in value [v2]. *) @@ -61,75 +61,52 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. -Inductive neutral_for_cast: type -> Prop := - | nfc_int: forall sg, - neutral_for_cast (Tint I32 sg) - | nfc_ptr: forall ty, - neutral_for_cast (Tpointer ty) - | nfc_array: forall ty sz, - neutral_for_cast (Tarray ty sz) - | nfc_fun: forall targs tres, - neutral_for_cast (Tfunction targs tres). - -Inductive cast : val -> type -> type -> val -> Prop := - | cast_ii: forall i sz2 sz1 si1 si2, (**r int to int *) - cast (Vint i) (Tint sz1 si1) (Tint sz2 si2) - (Vint (cast_int_int sz2 si2 i)) - | cast_fi: forall f sz1 sz2 si2 i, (**r float to int *) - cast_float_int si2 f = Some i -> - cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2) - (Vint (cast_int_int sz2 si2 i)) - | cast_if: forall i sz1 sz2 si1, (**r int to float *) - cast (Vint i) (Tint sz1 si1) (Tfloat sz2) - (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) - | cast_ff: forall f sz1 sz2, (**r float to float *) - cast (Vfloat f) (Tfloat sz1) (Tfloat sz2) - (Vfloat (cast_float_float sz2 f)) - | cast_nn_p: forall b ofs t1 t2, (**r no change in data representation *) - neutral_for_cast t1 -> neutral_for_cast t2 -> - cast (Vptr b ofs) t1 t2 (Vptr b ofs) - | cast_nn_i: forall n t1 t2, (**r no change in data representation *) - neutral_for_cast t1 -> neutral_for_cast t2 -> - cast (Vint n) t1 t2 (Vint n). +Definition neutral_for_cast (t: type) : bool := + match t with + | Tint I32 sg => true + | Tpointer ty => true + | Tarray ty sz => true + | Tfunction targs tres => true + | _ => false + end. + +Function sem_cast (v: val) (t1 t2: type) : option val := + match v, t1, t2 with + | Vint i, Tint sz1 si1, Tint sz2 si2 => (**r int to int *) + Some (Vint (cast_int_int sz2 si2 i)) + | Vfloat f, Tfloat sz1, Tint sz2 si2 => (**r float to int *) + match cast_float_int si2 f with + | Some i => Some (Vint (cast_int_int sz2 si2 i)) + | None => None + end + | Vint i, Tint sz1 si1, Tfloat sz2 => (**r int to float *) + Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | Vfloat f, Tfloat sz1, Tfloat sz2 => (**r float to float *) + Some (Vfloat (cast_float_float sz2 f)) + | Vptr b ofs, _, _ => (**r int32|pointer to int32|pointer *) + if neutral_for_cast t1 && neutral_for_cast t2 + then Some(Vptr b ofs) else None + | Vint n, _, _ => (**r int32|pointer to int32|pointer *) + if neutral_for_cast t1 && neutral_for_cast t2 + then Some(Vint n) else None + | _, _, _ => + None + end. (** Interpretation of values as truth values. Non-zero integers, non-zero floats and non-null pointers are considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Inductive is_false: val -> type -> Prop := - | is_false_int: forall sz sg, - is_false (Vint Int.zero) (Tint sz sg) - | is_false_pointer: forall t, - is_false (Vint Int.zero) (Tpointer t) - | is_false_float: forall sz f, - Float.cmp Ceq f Float.zero = true -> - is_false (Vfloat f) (Tfloat sz). - -Inductive is_true: val -> type -> Prop := - | is_true_int_int: forall n sz sg, - n <> Int.zero -> - is_true (Vint n) (Tint sz sg) - | is_true_pointer_int: forall b ofs sz sg, - is_true (Vptr b ofs) (Tint sz sg) - | is_true_int_pointer: forall n t, - n <> Int.zero -> - is_true (Vint n) (Tpointer t) - | is_true_pointer_pointer: forall b ofs t, - is_true (Vptr b ofs) (Tpointer t) - | is_true_float: forall f sz, - Float.cmp Ceq f Float.zero = false -> - is_true (Vfloat f) (Tfloat sz). - -(* -Inductive bool_of_val : val -> type -> val -> Prop := - | bool_of_val_true: forall v ty, - is_true v ty -> - bool_of_val v ty Vtrue - | bool_of_val_false: forall v ty, - is_false v ty -> - bool_of_val v ty Vfalse. -*) +Function bool_val (v: val) (t: type) : option bool := + match v, t with + | Vint n, Tint sz sg => Some (negb (Int.eq n Int.zero)) + | Vint n, Tpointer t' => Some (negb (Int.eq n Int.zero)) + | Vptr b ofs, Tint sz sg => Some true + | Vptr b ofs, Tpointer t' => Some true + | Vfloat f, Tfloat sz => Some (negb(Float.cmp Ceq f Float.zero)) + | _, _ => None + end. (** The following [sem_] functions compute the result of an operator application. Since operators are overloaded, the result depends @@ -139,7 +116,7 @@ Inductive bool_of_val : val -> type -> val -> Prop := - 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 int 32", otherwise + if at least one of the arguments is of type "unsigned int32", otherwise the signed operation is performed. - If both arguments are of float type, a float operation is performed. We choose to perform all float arithmetic in double precision, @@ -669,36 +646,32 @@ Inductive rred: expr -> mem -> expr -> mem -> Prop := rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m (Eval v ty) m | red_cast: forall ty v1 ty1 m v, - cast v1 ty1 ty v -> + sem_cast v1 ty1 ty = Some v -> rred (Ecast (Eval v1 ty1) ty) m (Eval v ty) m - | red_condition_true: forall v1 ty1 r1 r2 ty m, - is_true v1 ty1 -> typeof r1 = ty -> + | red_condition: forall v1 ty1 r1 r2 ty b m, + bool_val v1 ty1 = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m - (Eparen r1 ty) m - | red_condition_false: forall v1 ty1 r1 r2 ty m, - is_false v1 ty1 -> typeof r2 = ty -> - rred (Econdition (Eval v1 ty1) r1 r2 ty) m - (Eparen r2 ty) m + (Eparen (if b then r1 else r2) ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m (Eval (Vint (Int.repr (sizeof ty1))) ty) m | red_assign: forall b ofs ty1 v2 ty2 m v m', - cast v2 ty2 ty1 v -> + sem_cast v2 ty2 ty1 = Some v -> store_value_of_type ty1 m b ofs v = Some m' -> rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m (Eval v ty1) m' | red_assignop: forall op b ofs ty1 v2 ty2 tyres m v1 v v' m', load_value_of_type ty1 m b ofs = Some v1 -> sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> - cast v tyres ty1 v' -> + sem_cast v tyres ty1 = Some v' -> store_value_of_type ty1 m b ofs v' = Some m' -> rred (Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty1) m (Eval v' ty1) m' | red_postincr: forall id b ofs ty m v1 v2 v3 m', load_value_of_type ty m b ofs = Some v1 -> sem_incrdecr id v1 ty = Some v2 -> - cast v2 (typeconv ty) ty v3 -> + sem_cast v2 (typeconv ty) ty = Some v3 -> store_value_of_type ty m b ofs v3 = Some m' -> rred (Epostincr id (Eloc b ofs ty) ty) m (Eval v1 ty) m' @@ -706,10 +679,10 @@ Inductive rred: expr -> mem -> expr -> mem -> Prop := typeof r2 = ty -> rred (Ecomma (Eval v ty1) r2 ty) m r2 m - | red_paren: forall r ty m, - typeof r = ty -> - rred (Eparen r ty) m - r m. + | red_paren: forall v1 ty1 ty m v, + sem_cast v1 ty1 ty = Some v -> + rred (Eparen (Eval v1 ty1) ty) m + (Eval v ty) m. (** Head reduction for function calls. (More exactly, identification of function calls that can reduce.) *) @@ -718,7 +691,7 @@ Inductive cast_arguments: exprlist -> typelist -> list val -> Prop := | cast_args_nil: cast_arguments Enil Tnil nil | cast_args_cons: forall v ty el targ1 targs v1 vl, - cast v ty targ1 v1 -> cast_arguments el targs vl -> + sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl -> cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). Inductive callred: expr -> fundef -> list val -> type -> Prop := @@ -1004,45 +977,41 @@ Inductive sstep: state -> trace -> state -> Prop := | step_do_1: forall f x k e m, sstep (State f (Sdo x) k e m) - E0 (ExprState f x (Kdo k) e m) + E0 (ExprState f x (Kdo k) e m) | step_do_2: forall f v ty k e m, sstep (ExprState f (Eval v ty) (Kdo k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_seq: forall f s1 s2 k e m, sstep (State f (Ssequence s1 s2) k e m) - E0 (State f s1 (Kseq s2 k) e m) + E0 (State f s1 (Kseq s2 k) e m) | step_skip_seq: forall f s k e m, sstep (State f Sskip (Kseq s k) e m) - E0 (State f s k e m) + E0 (State f s k e m) | step_continue_seq: forall f s k e m, sstep (State f Scontinue (Kseq s k) e m) - E0 (State f Scontinue k e m) + E0 (State f Scontinue k e m) | step_break_seq: forall f s k e m, sstep (State f Sbreak (Kseq s k) e m) - E0 (State f Sbreak k e m) + E0 (State f Sbreak k e m) - | step_ifthenelse: forall f a s1 s2 k e m, + | step_ifthenelse_1: forall f a s1 s2 k e m, sstep (State f (Sifthenelse a s1 s2) k e m) - E0 (ExprState f a (Kifthenelse s1 s2 k) e m) - | step_ifthenelse_true: forall f v ty s1 s2 k e m, - is_true v ty -> + E0 (ExprState f a (Kifthenelse s1 s2 k) e m) + | step_ifthenelse_2: forall f v ty s1 s2 k e m b, + bool_val v ty = Some b -> sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m) - E0 (State f s1 k e m) - | step_ifthenelse_false: forall f v ty s1 s2 k e m, - is_false v ty -> - sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m) - E0 (State f s2 k e m) + E0 (State f (if b then s1 else s2) k e m) | step_while: forall f x s k e m, sstep (State f (Swhile x s) k e m) E0 (ExprState f x (Kwhile1 x s k) e m) | step_while_false: forall f v ty x s k e m, - is_false v ty -> + bool_val v ty = Some false -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f Sskip k e m) | step_while_true: forall f v ty x s k e m , - is_true v ty -> + bool_val v ty = Some true -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f s (Kwhile2 x s k) e m) | step_skip_or_continue_while: forall f s0 x s k e m, @@ -1059,102 +1028,102 @@ Inductive sstep: state -> trace -> state -> Prop := | step_skip_or_continue_dowhile: forall f s0 x s k e m, s0 = Sskip \/ s0 = Scontinue -> sstep (State f s0 (Kdowhile1 x s k) e m) - E0 (ExprState f x (Kdowhile2 x s k) e m) + E0 (ExprState f x (Kdowhile2 x s k) e m) | step_dowhile_false: forall f v ty x s k e m, - is_false v ty -> + bool_val v ty = Some false -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_dowhile_true: forall f v ty x s k e m, - is_true v ty -> + bool_val v ty = Some true -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) - E0 (State f (Sdowhile x s) k e m) + E0 (State f (Sdowhile x s) k e m) | step_break_dowhile: forall f a s k e m, sstep (State f Sbreak (Kdowhile1 a s k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_for_start: forall f a1 a2 a3 s k e m, a1 <> Sskip -> sstep (State f (Sfor a1 a2 a3 s) k e m) - E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) | step_for: forall f a2 a3 s k e m, sstep (State f (Sfor Sskip a2 a3 s) k e m) - E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m) + E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m) | step_for_false: forall f v ty a2 a3 s k e m, - is_false v ty -> + bool_val v ty = Some false -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_for_true: forall f v ty a2 a3 s k e m, - is_true v ty -> + bool_val v ty = Some true -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) - E0 (State f s (Kfor3 a2 a3 s k) e m) + E0 (State f s (Kfor3 a2 a3 s k) e m) | step_skip_or_continue_for3: forall f x a2 a3 s k e m, x = Sskip \/ x = Scontinue -> sstep (State f x (Kfor3 a2 a3 s k) e m) - E0 (State f a3 (Kfor4 a2 a3 s k) e m) + E0 (State f a3 (Kfor4 a2 a3 s k) e m) | step_break_for3: forall f a2 a3 s k e m, sstep (State f Sbreak (Kfor3 a2 a3 s k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_skip_for4: forall f a2 a3 s k e m, sstep (State f Sskip (Kfor4 a2 a3 s k) e m) - E0 (State f (Sfor Sskip a2 a3 s) k e m) + E0 (State f (Sfor Sskip a2 a3 s) k e m) | step_return_0: forall f k e m m', Mem.free_list m (blocks_of_env e) = Some m' -> sstep (State f (Sreturn None) k e m) - E0 (Returnstate Vundef (call_cont k) m') + E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f x k e m, sstep (State f (Sreturn (Some x)) k e m) - E0 (ExprState f x (Kreturn k) e m) + E0 (ExprState f x (Kreturn k) e m) | step_return_2: forall f v1 ty k e m v2 m', - cast v1 ty f.(fn_return) v2 -> + sem_cast v1 ty f.(fn_return) = Some v2 -> Mem.free_list m (blocks_of_env e) = Some m' -> sstep (ExprState f (Eval v1 ty) (Kreturn k) e m) - E0 (Returnstate v2 (call_cont k) m') + E0 (Returnstate v2 (call_cont k) m') | step_skip_call: forall f k e m m', is_call_cont k -> f.(fn_return) = Tvoid -> Mem.free_list m (blocks_of_env e) = Some m' -> sstep (State f Sskip k e m) - E0 (Returnstate Vundef k m') + E0 (Returnstate Vundef k m') | step_switch: forall f x sl k e m, sstep (State f (Sswitch x sl) k e m) - E0 (ExprState f x (Kswitch1 sl k) e m) + E0 (ExprState f x (Kswitch1 sl k) e m) | step_expr_switch: forall f n ty sl k e m, sstep (ExprState f (Eval (Vint n) ty) (Kswitch1 sl k) e m) - E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) + E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) | step_skip_break_switch: forall f x k e m, x = Sskip \/ x = Sbreak -> sstep (State f x (Kswitch2 k) e m) - E0 (State f Sskip k e m) + E0 (State f Sskip k e m) | step_continue_switch: forall f k e m, sstep (State f Scontinue (Kswitch2 k) e m) - E0 (State f Scontinue k e m) + E0 (State f Scontinue k e m) | step_label: forall f lbl s k e m, sstep (State f (Slabel lbl s) k e m) - E0 (State f s k e m) + E0 (State f s k e m) | step_goto: forall f lbl k e m s' k', find_label lbl f.(fn_body) (call_cont k) = Some (s', k') -> sstep (State f (Sgoto lbl) k e m) - E0 (State f s' k' e m) + E0 (State f s' k' e m) | step_internal_function: forall f vargs k m e m1 m2, list_norepet (var_names (fn_params f) ++ var_names (fn_vars f)) -> alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> sstep (Callstate (Internal f) vargs k m) - E0 (State f f.(fn_body) k e m2) + E0 (State f f.(fn_body) k e m2) | step_external_function: forall ef targs tres vargs k m vres t m', external_call ef ge vargs m t vres m' -> sstep (Callstate (External ef targs tres) vargs k m) - t (Returnstate vres k m') + t (Returnstate vres k m') | step_returnstate: forall v f e C ty k m, sstep (Returnstate v (Kcall f e C ty k) m) - E0 (ExprState f (C (Eval v ty)) k e m). + E0 (ExprState f (C (Eval v ty)) k e m). Definition step (S: state) (t: trace) (S': state) : Prop := estep S t S' \/ sstep S t S'. -- cgit