diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-16 16:17:08 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-16 16:17:08 +0000 |
| commit | a335e621aaa85a7f73b16c121261dbecf8e68340 (patch) | |
| tree | 31312a22aafc7f66818c0c82f4c96e88ff391595 /cfrontend | |
| parent | 93b89122000e42ac57abc39734fdf05d3a89e83c (diff) | |
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
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Clight.v | 124 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 223 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 6 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 183 | ||||
| -rw-r--r-- | cfrontend/Cstrategy.v | 214 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 61 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 103 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 60 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 241 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 44 |
10 files changed, 528 insertions, 731 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index a61d706..76f6ff6 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -249,19 +249,15 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr a2 v2 -> sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v -> eval_expr (Ebinop op a1 a2 ty) v - | eval_Econdition_true: forall a1 a2 a3 ty v1 v2, + | eval_Econdition: forall a1 a2 a3 ty v1 b v' v, eval_expr a1 v1 -> - is_true v1 (typeof a1) -> - eval_expr a2 v2 -> - eval_expr (Econdition a1 a2 a3 ty) v2 - | eval_Econdition_false: forall a1 a2 a3 ty v1 v3, - eval_expr a1 v1 -> - is_false v1 (typeof a1) -> - eval_expr a3 v3 -> - eval_expr (Econdition a1 a2 a3 ty) v3 + bool_val v1 (typeof a1) = Some b -> + eval_expr (if b then a2 else a3) v' -> + sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> + eval_expr (Econdition a1 a2 a3 ty) v | eval_Ecast: forall a ty v1 v, eval_expr a v1 -> - cast v1 (typeof a) ty v -> + sem_cast v1 (typeof a) ty = Some v -> eval_expr (Ecast a ty) v | eval_Elvalue: forall a loc ofs v, eval_lvalue a loc ofs -> @@ -308,7 +304,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop := eval_exprlist nil Tnil nil | eval_Econs: forall a bl ty tyl v1 v2 vl, eval_expr a v1 -> - cast v1 (typeof a) ty v2 -> + sem_cast v1 (typeof a) ty = Some v2 -> eval_exprlist bl tyl vl -> eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl). @@ -422,7 +418,7 @@ Inductive step: state -> trace -> state -> Prop := | step_assign: forall f a1 a2 k e le m loc ofs v2 v m', eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> - cast v2 (typeof a2) (typeof a1) v -> + sem_cast v2 (typeof a2) (typeof a1) = Some v -> store_value_of_type (typeof a1) m loc ofs v = Some m' -> step (State f (Sassign a1 a2) k e le m) E0 (State f Sskip k e le m') @@ -454,25 +450,20 @@ Inductive step: state -> trace -> state -> Prop := step (State f Sbreak (Kseq s k) e le m) E0 (State f Sbreak k e le m) - | step_ifthenelse_true: forall f a s1 s2 k e le m v1, - eval_expr e le m a v1 -> - is_true v1 (typeof a) -> - step (State f (Sifthenelse a s1 s2) k e le m) - E0 (State f s1 k e le m) - | step_ifthenelse_false: forall f a s1 s2 k e le m v1, + | step_ifthenelse: forall f a s1 s2 k e le m v1 b, eval_expr e le m a v1 -> - is_false v1 (typeof a) -> + bool_val v1 (typeof a) = Some b -> step (State f (Sifthenelse a s1 s2) k e le m) - E0 (State f s2 k e le m) + E0 (State f (if b then s1 else s2) k e le m) | step_while_false: forall f a s k e le m v, eval_expr e le m a v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> step (State f (Swhile a s) k e le m) E0 (State f Sskip k e le m) | step_while_true: forall f a s k e le m v, eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> step (State f (Swhile a s) k e le m) E0 (State f s (Kwhile a s k) e le m) | step_skip_or_continue_while: forall f x a s k e le m, @@ -489,13 +480,13 @@ Inductive step: state -> trace -> state -> Prop := | step_skip_or_continue_dowhile_false: forall f x a s k e le m v, x = Sskip \/ x = Scontinue -> eval_expr e le m a v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> step (State f x (Kdowhile a s k) e le m) E0 (State f Sskip k e le m) | step_skip_or_continue_dowhile_true: forall f x a s k e le m v, x = Sskip \/ x = Scontinue -> eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> step (State f x (Kdowhile a s k) e le m) E0 (State f (Sdowhile a s) k e le m) | step_break_dowhile: forall f a s k e le m, @@ -504,12 +495,12 @@ Inductive step: state -> trace -> state -> Prop := | step_for_false: forall f a2 a3 s k e le m v, eval_expr e le m a2 v -> - is_false v (typeof a2) -> + bool_val v (typeof a2) = Some false -> step (State f (Sfor' a2 a3 s) k e le m) E0 (State f Sskip k e le m) | step_for_true: forall f a2 a3 s k e le m v, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> step (State f (Sfor' a2 a3 s) k e le m) E0 (State f s (Kfor2 a2 a3 s k) e le m) | step_skip_or_continue_for2: forall f x a2 a3 s k e le m, @@ -532,7 +523,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v v' m', eval_expr e le m a v -> - cast v (typeof a) f.(fn_return) v' -> + sem_cast v (typeof a) f.(fn_return) = Some v' -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) E0 (Returnstate v' (call_cont k) m') @@ -617,7 +608,7 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v',t')), ty => ty <> Tvoid /\ cast v' t' t v + | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v | _, _ => False end. @@ -634,7 +625,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> | exec_Sassign: forall e le m a1 a2 loc ofs v2 v m', eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> - cast v2 (typeof a2) (typeof a1) v -> + sem_cast v2 (typeof a2) (typeof a1) = Some v -> store_value_of_type (typeof a1) m loc ofs v = Some m' -> exec_stmt e le m (Sassign a1 a2) E0 le m' Out_normal @@ -670,16 +661,10 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> out <> Out_normal -> exec_stmt e le m (Ssequence s1 s2) t1 le1 m1 out - | exec_Sifthenelse_true: forall e le m a s1 s2 v1 t le' m' out, + | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out, eval_expr e le m a v1 -> - is_true v1 (typeof a) -> - exec_stmt e le m s1 t le' m' out -> - exec_stmt e le m (Sifthenelse a s1 s2) - t le' m' out - | exec_Sifthenelse_false: forall e le m a s1 s2 v1 t le' m' out, - eval_expr e le m a v1 -> - is_false v1 (typeof a) -> - exec_stmt e le m s2 t le' m' out -> + bool_val v1 (typeof a) = Some b -> + exec_stmt e le m (if b then s1 else s2) t le' m' out -> exec_stmt e le m (Sifthenelse a s1 s2) t le' m' out | exec_Sreturn_none: forall e le m, @@ -697,19 +682,19 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> E0 le m Out_continue | exec_Swhile_false: forall e le m a s v, eval_expr e le m a v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> exec_stmt e le m (Swhile a s) E0 le m Out_normal | exec_Swhile_stop: forall e le m a v s t le' m' out' out, eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e le m s t le' m' out' -> out_break_or_return out' out -> exec_stmt e le m (Swhile a s) t le' m' out | exec_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2 le2 m2 out, eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e le1 m1 (Swhile a s) t2 le2 m2 out -> @@ -719,7 +704,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> exec_stmt e le m s t le1 m1 out1 -> out_normal_or_continue out1 -> eval_expr e le1 m1 a v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> exec_stmt e le m (Sdowhile a s) t le1 m1 Out_normal | exec_Sdowhile_stop: forall e le m s a t le1 m1 out1 out, @@ -731,26 +716,26 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> eval_expr e le1 m1 a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e le1 m1 (Sdowhile a s) t2 le2 m2 out -> exec_stmt e le m (Sdowhile a s) (t1 ** t2) le2 m2 out | exec_Sfor_false: forall e le m s a2 a3 v, eval_expr e le m a2 v -> - is_false v (typeof a2) -> + bool_val v (typeof a2) = Some false -> exec_stmt e le m (Sfor' a2 a3 s) E0 le m Out_normal | exec_Sfor_stop: forall e le m s a2 a3 v le1 m1 t out1 out, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e le m s t le1 m1 out1 -> out_break_or_return out1 out -> exec_stmt e le m (Sfor' a2 a3 s) t le1 m1 out | exec_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 le3 m3 t1 t2 t3 out1 out, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal -> @@ -814,24 +799,19 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro exec_stmt e le m s1 t1 le1 m1 Out_normal -> execinf_stmt e le1 m1 s2 t2 -> execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2) - | execinf_Sifthenelse_true: forall e le m a s1 s2 v1 t, - eval_expr e le m a v1 -> - is_true v1 (typeof a) -> - execinf_stmt e le m s1 t -> - execinf_stmt e le m (Sifthenelse a s1 s2) t - | execinf_Sifthenelse_false: forall e le m a s1 s2 v1 t, + | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t, eval_expr e le m a v1 -> - is_false v1 (typeof a) -> - execinf_stmt e le m s2 t -> + bool_val v1 (typeof a) = Some b -> + execinf_stmt e le m (if b then s1 else s2) t -> execinf_stmt e le m (Sifthenelse a s1 s2) t | execinf_Swhile_body: forall e le m a v s t, eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> execinf_stmt e le m s t -> execinf_stmt e le m (Swhile a s) t | execinf_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2, eval_expr e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> execinf_stmt e le1 m1 (Swhile a s) t2 -> @@ -843,24 +823,24 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> eval_expr e le1 m1 a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> execinf_stmt e le1 m1 (Sdowhile a s) t2 -> execinf_stmt e le m (Sdowhile a s) (t1 *** t2) | execinf_Sfor_body: forall e le m s a2 a3 v t, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> execinf_stmt e le m s t -> execinf_stmt e le m (Sfor' a2 a3 s) t | execinf_Sfor_next: forall e le m s a2 a3 v le1 m1 t1 t2 out1, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> execinf_stmt e le1 m1 a3 t2 -> execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2) | execinf_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 t1 t2 t3 out1, eval_expr e le m a2 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e le m s t1 le1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal -> @@ -962,9 +942,9 @@ Let ge : genv := Genv.globalenv prog. Definition exec_stmt_eval_funcall_ind (PS: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop) (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) := - fun a b c d e f g h i j k l m n o p q r s t u v w x y => - conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) - (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). + fun a b c d e f g h i j k l m n o p q r s t u v w x => + conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x) + (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x). Inductive outcome_state_match (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := @@ -1056,16 +1036,10 @@ Proof. reflexivity. traceEq. unfold S2; inv B1; congruence || econstructor; eauto. -(* ifthenelse true *) - destruct (H2 f k) as [S1 [A1 B1]]. - exists S1; split. - eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. - auto. - -(* ifthenelse false *) +(* ifthenelse *) destruct (H2 f k) as [S1 [A1 B1]]. exists S1; split. - eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. + eapply star_left. 2: eexact A1. eapply step_ifthenelse; eauto. traceEq. auto. (* return none *) @@ -1285,13 +1259,9 @@ Proof. apply star_one. constructor. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. -(* ifthenelse true *) - eapply forever_N_plus. - apply plus_one. eapply step_ifthenelse_true; eauto. - apply CIH_STMT; eauto. traceEq. -(* ifthenelse false *) +(* ifthenelse *) eapply forever_N_plus. - apply plus_one. eapply step_ifthenelse_false; eauto. + apply plus_one. eapply step_ifthenelse with (b := b); eauto. apply CIH_STMT; eauto. traceEq. (* while body *) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 21dd57e..5461353 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'. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cc24316..e32001b 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -355,11 +355,13 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := | Clight.Ecast b ty => do tb <- transl_expr b; OK (make_cast (typeof b) ty tb) - | Clight.Econdition b c d _ => + | Clight.Econdition b c d ty => do tb <- transl_expr b; do tc <- transl_expr c; do td <- transl_expr d; - OK(Econdition (make_boolean tb (typeof b)) tc td) + OK(Econdition (make_boolean tb (typeof b)) + (make_cast (typeof c) ty tc) + (make_cast (typeof d) ty td)) | Clight.Esizeof ty _ => OK(make_intconst (Int.repr (Csyntax.sizeof ty))) | Clight.Efield b i ty => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 28e6dad..11d8d59 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -134,28 +134,34 @@ Qed. Remark neutral_for_cast_chunk: forall ty chunk, - neutral_for_cast ty -> access_mode ty = By_value chunk -> chunk = Mint32. + neutral_for_cast ty = true -> access_mode ty = By_value chunk -> chunk = Mint32. Proof. - induction 1; simpl; intros; inv H; auto. + intros. destruct ty; inv H; simpl in H0. + destruct i; inv H2. congruence. + congruence. + congruence. + congruence. Qed. Lemma cast_result_normalized: forall chunk v1 ty1 ty2 v2, - cast v1 ty1 ty2 v2 -> + sem_cast v1 ty1 ty2 = Some v2 -> access_mode ty2 = By_value chunk -> val_normalized v2 chunk. Proof. - induction 1; intros; simpl. + intros. functional inversion H; subst. apply cast_int_int_normalized; auto. apply cast_int_int_normalized; auto. apply cast_float_float_normalized; auto. apply cast_float_float_normalized; auto. - rewrite (neutral_for_cast_chunk _ _ H0 H1). red; auto. - rewrite (neutral_for_cast_chunk _ _ H0 H1). red; auto. + destruct (andb_prop _ _ H8). + rewrite (neutral_for_cast_chunk _ _ H2 H0). red; auto. + destruct (andb_prop _ _ H9). + rewrite (neutral_for_cast_chunk _ _ H2 H0). red; auto. Qed. Definition val_casted (v: val) (ty: type) : Prop := - exists v0, exists ty0, cast v0 ty0 ty v. + exists v0, exists ty0, sem_cast v0 ty0 ty = Some v. Lemma val_casted_normalized: forall v ty chunk, @@ -386,40 +392,28 @@ Proof. simpl. auto. Qed. -Lemma make_boolean_correct_true: - forall e le m a v ty, - eval_expr ge e le m a v -> - is_true v ty -> - exists vb, - eval_expr ge e le m (make_boolean a ty) vb - /\ Val.is_true vb. -Proof. - intros until ty; intros EXEC VTRUE. - destruct ty; simpl; - try (exists v; intuition; inversion VTRUE; simpl; auto; fail). - exists Vtrue; split. - eapply eval_Ebinop; eauto with cshm. - inversion VTRUE; simpl. - rewrite Float.cmp_ne_eq. rewrite H1. auto. - apply Vtrue_is_true. -Qed. - -Lemma make_boolean_correct_false: - forall e le m a v ty, +Lemma make_boolean_correct: + forall e le m a v ty b, eval_expr ge e le m a v -> - is_false v ty -> + bool_val v ty = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb - /\ Val.is_false vb. -Proof. - intros until ty; intros EXEC VFALSE. - destruct ty; simpl; - try (exists v; intuition; inversion VFALSE; simpl; auto; fail). - exists Vfalse; split. - eapply eval_Ebinop; eauto with cshm. - inversion VFALSE; simpl. - rewrite Float.cmp_ne_eq. rewrite H1. auto. - apply Vfalse_is_false. + /\ Val.bool_of_val vb b. +Proof. + assert (VBI: forall n, Val.bool_of_val (Vint n) (negb (Int.eq n Int.zero))). + intros. predSpec Int.eq Int.eq_spec n Int.zero; simpl. + subst. constructor. + constructor. auto. + intros. functional inversion H0; subst; simpl. + exists (Vint n); split; auto. + exists (Vint n); split; auto. + exists (Vptr b0 ofs); split; auto. constructor. + exists (Vptr b0 ofs); split; auto. constructor. + rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero) as []_eqn. + exists Vtrue; split. eapply eval_Ebinop; eauto with cshm. simpl. rewrite Heqb; auto. + constructor. apply Int.one_not_zero. + exists Vfalse; split. eapply eval_Ebinop; eauto with cshm. simpl. rewrite Heqb; auto. + constructor. Qed. Lemma make_neg_correct: @@ -650,15 +644,25 @@ Proof. eapply make_cmp_correct; eauto. Qed. +Lemma make_cast_neutral: + forall ty1 ty2 a, + neutral_for_cast ty1 && neutral_for_cast ty2 = true -> + make_cast ty1 ty2 a = a. +Proof. + intros. destruct (andb_prop _ _ H). + unfold make_cast. + replace (make_cast1 ty1 ty2 a) with a. + unfold make_cast2. destruct ty2; simpl in H1; inv H1; auto. destruct i; inv H3; auto. + unfold make_cast1. destruct ty1; simpl in H0; inv H0; auto. destruct ty2; simpl in H1; inv H1; auto. +Qed. + Lemma make_cast_correct: forall e le m a v ty1 ty2 v', eval_expr ge e le m a v -> - cast v ty1 ty2 v' -> + sem_cast v ty1 ty2 = Some v' -> eval_expr ge e le m (make_cast ty1 ty2 a) v'. Proof. - unfold make_cast, make_cast1, make_cast2. - intros until v'; intros EVAL CAST. - inversion CAST; clear CAST; subst. + intros. functional inversion H0; subst; simpl. (* cast_int_int *) destruct sz2; destruct si2; repeat econstructor; eauto with cshm. (* cast_float_int *) @@ -669,9 +673,9 @@ Proof. (* cast_float_float *) destruct sz2; repeat econstructor; eauto with cshm. (* neutral, ptr *) - inversion H0; auto; inversion H; auto. + rewrite make_cast_neutral; auto. (* neutral, int *) - inversion H0; auto; inversion H; auto. + rewrite make_cast_neutral; auto. Qed. Lemma make_load_correct: @@ -1092,16 +1096,11 @@ Proof. eapply transl_unop_correct; eauto. (* binop *) eapply transl_binop_correct; eauto. -(* condition true *) - exploit make_boolean_correct_true. eapply H0; eauto. eauto. - intros [vb [EVAL ISTRUE]]. - eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. - simpl. eauto. -(* condition false *) - exploit make_boolean_correct_false. eapply H0; eauto. eauto. - intros [vb [EVAL ISFALSE]]. - eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. - simpl. eauto. +(* condition *) + exploit make_boolean_correct. eapply H0; eauto. eauto. + intros [vb [EVAL BVAL]]. + eapply eval_Econdition; eauto. + destruct b; eapply make_cast_correct; eauto. (* cast *) eapply make_cast_correct; eauto. (* rvalue out of lvalue *) @@ -1159,71 +1158,46 @@ Qed. End EXPR. -Lemma is_constant_bool_true: - forall te le m a v ty, +Lemma is_constant_bool_sound: + forall te le m a v ty b, Csharpminor.eval_expr tge te le m a v -> - is_true v ty -> - is_constant_bool a <> Some false. + bool_val v ty = Some b -> + is_constant_bool a = Some b \/ is_constant_bool a = None. Proof. - intros. unfold is_constant_bool. destruct a; try congruence. destruct c; try congruence. - inv H. simpl in H2. inv H2. rewrite Int.eq_false. simpl; congruence. - inv H0; auto. -Qed. - -Lemma is_constant_bool_false: - forall te le m a v ty, - Csharpminor.eval_expr tge te le m a v -> - is_false v ty -> - is_constant_bool a <> Some true. -Proof. - intros. unfold is_constant_bool. destruct a; try congruence. destruct c; try congruence. - inv H. simpl in H2. inv H2. - assert (i = Int.zero). inv H0; auto. - subst i. simpl. congruence. + intros. unfold is_constant_bool. destruct a; auto. destruct c; auto. + left. decEq. inv H. simpl in H2. inv H2. functional inversion H0; auto. Qed. Lemma exit_if_false_true: forall a ts e le m v te f tk, exit_if_false a = OK ts -> Clight.eval_expr ge e le m a v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> match_env e te -> star step tge (State f ts tk te le m) E0 (State f Sskip tk te le m). Proof. intros. monadInv H. exploit transl_expr_correct; eauto. intros EV. - generalize (is_constant_bool_true _ _ _ _ _ _ EV H1); intros ICB. - destruct (is_constant_bool x). destruct b. - inv EQ0. apply star_refl. - congruence. - inv EQ0. - exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]]. - apply star_one. - change Sskip with (if true then Sskip else Sexit 0). - eapply step_ifthenelse; eauto. - apply Val.bool_of_true_val; eauto. + exploit is_constant_bool_sound; eauto. intros [P | P]; rewrite P in EQ0; inv EQ0. + constructor. + exploit make_boolean_correct; eauto. intros [vb [EV' VB]]. + apply star_one. apply step_ifthenelse with (v := vb) (b := true); auto. Qed. Lemma exit_if_false_false: forall a ts e le m v te f tk, exit_if_false a = OK ts -> Clight.eval_expr ge e le m a v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> match_env e te -> star step tge (State f ts tk te le m) E0 (State f (Sexit 0) tk te le m). Proof. intros. monadInv H. exploit transl_expr_correct; eauto. intros EV. - generalize (is_constant_bool_false _ _ _ _ _ _ EV H1); intros ICB. - destruct (is_constant_bool x). destruct b. - congruence. - inv EQ0. apply star_refl. - inv EQ0. - exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]]. - apply star_one. - change (Sexit 0) with (if false then Sskip else Sexit 0). - eapply step_ifthenelse; eauto. - apply Val.bool_of_false_val; eauto. + exploit is_constant_bool_sound; eauto. intros [P | P]; rewrite P in EQ0; inv EQ0. + constructor. + exploit make_boolean_correct; eauto. intros [vb [EV' VB]]. + apply star_one. apply step_ifthenelse with (v := vb) (b := false); auto. Qed. (** ** Semantic preservation for statements *) @@ -1556,25 +1530,14 @@ Proof. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. -(* ifthenelse true *) - monadInv TR. inv MTR. - exploit make_boolean_correct_true; eauto. - exploit transl_expr_correct; eauto. - intros [v [A B]]. - econstructor; split. - apply plus_one. apply step_ifthenelse with (v := v) (b := true). - auto. apply Val.bool_of_true_val. auto. - econstructor; eauto. constructor. - -(* ifthenelse false *) +(* ifthenelse *) monadInv TR. inv MTR. - exploit make_boolean_correct_false; eauto. + exploit make_boolean_correct; eauto. exploit transl_expr_correct; eauto. intros [v [A B]]. econstructor; split. - apply plus_one. apply step_ifthenelse with (v := v) (b := false). - auto. apply Val.bool_of_false_val. auto. - econstructor; eauto. constructor. + apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto. + destruct b; econstructor; eauto; constructor. (* while false *) monadInv TR. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index c0dd3a3..8b66ef9 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -123,7 +123,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - cast v1 (typeof r1) ty v -> + sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))). @@ -132,7 +132,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := | esrl_nil: eval_simple_list Enil Tnil nil | esrl_cons: forall r rl ty tyl v vl v', - eval_simple_rvalue r v' -> cast v' (typeof r) ty v -> + eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v -> eval_simple_list rl tyl vl -> eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl). @@ -222,27 +222,18 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f r k e m) E0 (ExprState f (Eval v ty) k e m) - | step_condition_true: forall f C r1 r2 r3 ty k e m v, + | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - is_true v (typeof r1) -> - typeof r2 = ty -> + bool_val v (typeof r1) = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) - E0 (ExprState f (C (Eparen r2 ty)) k e m) - - | step_condition_false: forall f C r1 r2 r3 ty k e m v, - leftcontext RV RV C -> - eval_simple_rvalue e m r1 v -> - is_false v (typeof r1) -> - typeof r3 = ty -> - estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) - E0 (ExprState f (C (Eparen r3 ty)) k e m) + E0 (ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m) | step_assign: forall f C l r ty k e m b ofs v v' m', leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> eval_simple_rvalue e m r v -> - cast v (typeof r) (typeof l) v' -> + sem_cast v (typeof r) (typeof l) = Some v' -> store_value_of_type (typeof l) m b ofs v' = Some m' -> ty = typeof l -> estep (ExprState f (C (Eassign l r ty)) k e m) @@ -254,7 +245,7 @@ Inductive estep: state -> trace -> state -> Prop := load_value_of_type (typeof l) m b ofs = Some v1 -> eval_simple_rvalue e m r v2 -> sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 -> - cast v3 tyres (typeof l) v4 -> + sem_cast v3 tyres (typeof l) = Some v4 -> store_value_of_type (typeof l) m b ofs v4 = Some m' -> ty = typeof l -> estep (ExprState f (C (Eassignop op l r tyres ty)) k e m) @@ -265,7 +256,7 @@ Inductive estep: state -> trace -> state -> Prop := eval_simple_lvalue e m l b ofs -> 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' -> ty = typeof l -> estep (ExprState f (C (Epostincr id l ty)) k e m) @@ -278,10 +269,10 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Ecomma r1 r2 ty)) k e m) E0 (ExprState f (C r2) k e m) - | step_paren: forall f C r ty k e m v, + | step_paren: forall f C r ty k e m v1 v, leftcontext RV RV C -> - eval_simple_rvalue e m r v -> - ty = typeof r -> + eval_simple_rvalue e m r v1 -> + sem_cast v1 (typeof r) ty = Some v -> estep (ExprState f (C (Eparen r ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) @@ -472,30 +463,30 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => - exists v, cast v1 ty1 ty v + exists v, sem_cast v1 ty1 ty = Some v | Econdition (Eval v1 ty1) r1 r2 ty => - ((is_true v1 ty1 /\ typeof r1 = ty) \/ (is_false v1 ty1 /\ typeof r2 = ty)) + exists b, bool_val v1 ty1 = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', - ty = ty1 /\ cast v2 ty2 ty1 v /\ store_value_of_type ty1 m b ofs v = Some m' + ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ store_value_of_type ty1 m b ofs v = Some m' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => exists v1, exists v, exists v', exists m', ty = ty1 /\ 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' | Epostincr id (Eloc b ofs ty1) ty => exists v1, exists v2, exists v3, exists m', ty = ty1 /\ 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' | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty - | Eparen (Eval v ty1) ty => - ty = ty1 + | Eparen (Eval v1 ty1) ty => + exists v, sem_cast v1 ty1 ty = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs, exists tyres, exists fd, exists vl, @@ -524,10 +515,11 @@ Proof. exists v; auto. exists v; auto. exists v; auto. + exists b; auto. exists v; exists m'; auto. exists v1; exists v; exists v'; exists m'; auto. exists v1; exists v2; exists v3; exists m'; auto. - destruct r; auto. + exists v; auto. Qed. Lemma callred_invert: @@ -558,7 +550,7 @@ Proof. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. - destruct (C a); auto; contradiction. + auto. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct e1; auto; destruct (C a); auto; contradiction. @@ -1035,14 +1027,10 @@ Proof. exploit eval_simple_rvalue_steps; eauto. simpl; intros STEPS. exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; auto. inversion EQ1. rewrite <- H3 in H2; contradiction. -(* condition true *) - eapply plus_safe; eauto. - eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 (typeof r2))); eauto. - intros. apply plus_one. left; apply step_rred; eauto. apply red_condition_true; auto. -(* condition false *) +(* condition *) eapply plus_safe; eauto. - eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 (typeof r3))); eauto. - intros. apply plus_one. left; apply step_rred; eauto. apply red_condition_false; auto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 ty)); eauto. + intros. apply plus_one. left; apply step_rred; eauto. constructor; auto. (* assign *) eapply plus_safe; eauto. eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto. @@ -1065,7 +1053,7 @@ Proof. intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. (* paren *) eapply plus_safe; eauto. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x (typeof r))); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x ty)); eauto. intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. (* call *) exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. @@ -1093,9 +1081,8 @@ Proof. (* condition *) exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto. intros [v1 [E1 S1]]. - exploit safe_inv. eexact S1. eauto. simpl. intros [[T TY] | [F TY]]. - econstructor; eapply step_condition_true; eauto. - econstructor; eapply step_condition_false; eauto. + exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. + econstructor. eapply step_condition; eauto. (* assign *) destruct Q. exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassign x b2 ty))); eauto. @@ -1139,7 +1126,7 @@ Proof. (* paren *) exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto. intros [v1 [E1 S1]]. - exploit safe_inv. eexact S1. eauto. simpl. intros EQ. + exploit safe_inv. eexact S1. eauto. simpl. intros [v CAST]. econstructor; eapply step_paren; eauto. Qed. @@ -1262,7 +1249,7 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ cast v' ty' ty v + | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v | _, _ => False end. @@ -1302,15 +1289,11 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := | eval_cast: forall e m a t m' a' ty, eval_expr e m RV a t m' a' -> eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) - | eval_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a2' v, - eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_true v1 (typeof a1) -> - eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v -> - ty = typeof a2 -> - eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) - | eval_condition_false: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a3' v, - eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_false v1 (typeof a1) -> - eval_expr e m' RV a3 t2 m'' a3' -> eval_simple_rvalue ge e m'' a3' v -> - ty = typeof a3 -> + | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some b -> + eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> + sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) | eval_sizeof: forall e m ty' ty, eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty) @@ -1318,7 +1301,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> eval_simple_lvalue ge e m2 l' b ofs -> eval_simple_rvalue ge e m2 r' v -> - cast v (typeof r) (typeof l) v' -> + sem_cast v (typeof r) (typeof l) = Some v' -> store_value_of_type (typeof l) m2 b ofs v' = Some m3 -> ty = typeof l -> eval_expr e m RV (Eassign l r ty) (t1**t2) m3 (Eval v' ty) @@ -1329,7 +1312,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := load_value_of_type (typeof l) m2 b ofs = Some v1 -> eval_simple_rvalue ge e m2 r' v2 -> sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> - cast v3 tyres (typeof l) v4 -> + sem_cast v3 tyres (typeof l) = Some v4 -> store_value_of_type (typeof l) m2 b ofs v4 = Some m3 -> ty = typeof l -> eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2) m3 (Eval v4 ty) @@ -1338,7 +1321,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_simple_lvalue ge e m1 l' b ofs -> load_value_of_type ty m1 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 m1 b ofs v3 = Some m2 -> ty = typeof l -> eval_expr e m RV (Epostincr id l ty) t m2 (Eval v1 ty) @@ -1390,16 +1373,10 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := out <> Out_normal -> exec_stmt e m (Ssequence s1 s2) t1 m1 out - | exec_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2 m2 out, - eval_expression e m a t1 m1 v1 -> - is_true v1 (typeof a) -> - exec_stmt e m1 s1 t2 m2 out -> - exec_stmt e m (Sifthenelse a s1 s2) - (t1**t2) m2 out - | exec_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2 m2 out, + | exec_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 m2 b out, eval_expression e m a t1 m1 v1 -> - is_false v1 (typeof a) -> - exec_stmt e m1 s2 t2 m2 out -> + bool_val v1 (typeof a) = Some b -> + exec_stmt e m1 (if b then s1 else s2) t2 m2 out -> exec_stmt e m (Sifthenelse a s1 s2) (t1**t2) m2 out | exec_Sreturn_none: forall e m, @@ -1417,19 +1394,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := E0 m Out_continue | exec_Swhile_false: forall e m a s t m' v, eval_expression e m a t m' v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> exec_stmt e m (Swhile a s) t m' Out_normal | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, eval_expression e m a t1 m1 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e m1 s t2 m2 out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) (t1**t2) m2 out | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, eval_expression e m a t1 m1 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 (Swhile a s) t3 m3 out -> @@ -1439,7 +1416,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - is_false v (typeof a) -> + bool_val v (typeof a) = Some false -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, @@ -1451,7 +1428,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out @@ -1462,19 +1439,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> - is_false v (typeof a2) -> + bool_val v (typeof a2) = Some false -> exec_stmt e m (Sfor Sskip a2 a3 s) t m' Out_normal | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, eval_expression e m a2 t1 m1 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, eval_expression e m a2 t1 m1 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1546,15 +1523,10 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := | evalinf_condition: forall e m a1 a2 a3 ty t1, evalinf_expr e m RV a1 t1 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 - | evalinf_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2, - eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_true v1 (typeof a1) -> - evalinf_expr e m' RV a2 t2 -> - ty = typeof a2 -> - evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) - | evalinf_condition_false: forall e m a1 a2 a3 ty t1 m' a1' v1 t2, - eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_false v1 (typeof a1) -> - evalinf_expr e m' RV a3 t2 -> - ty = typeof a3 -> + | evalinf_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> + bool_val v1 (typeof a1) = Some b -> + evalinf_expr e m' RV (if b then a2 else a3) t2 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) | evalinf_assign_left: forall e m a1 t1 a2 ty, evalinf_expr e m LV a1 t1 -> @@ -1622,15 +1594,10 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := | execinf_Sifthenelse_test: forall e m a s1 s2 t1, evalinf_expr e m RV a t1 -> execinf_stmt e m (Sifthenelse a s1 s2) t1 - | execinf_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2, + | execinf_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 b, eval_expression e m a t1 m1 v1 -> - is_true v1 (typeof a) -> - execinf_stmt e m1 s1 t2 -> - execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) - | execinf_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2, - eval_expression e m a t1 m1 v1 -> - is_false v1 (typeof a) -> - execinf_stmt e m1 s2 t2 -> + bool_val v1 (typeof a) = Some b -> + execinf_stmt e m1 (if b then s1 else s2) t2 -> execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) | execinf_Sreturn_some: forall e m a t, evalinf_expr e m RV a t -> @@ -1640,12 +1607,12 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Swhile a s) t1 | execinf_Swhile_body: forall e m a s t1 m1 v t2, eval_expression e m a t1 m1 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Swhile a s) (t1***t2) | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, eval_expression e m a t1 m1 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 (Swhile a s) t3 -> @@ -1662,7 +1629,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - is_true v (typeof a) -> + bool_val v (typeof a) = Some true -> execinf_stmt e m2 (Sdowhile a s) t3 -> execinf_stmt e m (Sdowhile a s) (t1***t2***t3) | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, @@ -1677,19 +1644,19 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, eval_expression e m a2 t1 m1 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, eval_expression e m a2 t1 m1 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 a3 t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, eval_expression e m a2 t1 m1 v -> - is_true v (typeof a2) -> + bool_val v (typeof a2) = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1845,18 +1812,8 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. simpl; intuition. eapply star_trans. eexact D. - eapply star_left. left; eapply step_condition_true; eauto. congruence. - eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. - reflexivity. reflexivity. traceEq. -(* condition false *) - exploit (H0 (fun x => C(Econdition x a2 a3 ty))). - eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H4 (fun x => C(Eparen x ty))). - eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. - simpl; intuition. - eapply star_trans. eexact D. - eapply star_left. left; eapply step_condition_false; eauto. congruence. - eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. + eapply star_left. left; eapply step_condition; eauto. rewrite B; eauto. + eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. reflexivity. reflexivity. traceEq. (* sizeof *) simpl; intuition. apply star_refl. @@ -1962,23 +1919,12 @@ Proof. reflexivity. traceEq. unfold S2; inv B1; congruence || econstructor; eauto. -(* ifthenelse true *) - destruct (H3 f k) as [S1 [A1 B1]]; auto. - exists S1; split. - eapply star_left. right; apply step_ifthenelse. - eapply star_trans. eapply H0. - eapply star_left. right; eapply step_ifthenelse_true; eauto. - eexact A1. - reflexivity. reflexivity. traceEq. - auto. - -(* ifthenelse false *) +(* ifthenelse *) destruct (H3 f k) as [S1 [A1 B1]]; auto. exists S1; split. - eapply star_left. right; apply step_ifthenelse. + eapply star_left. right; apply step_ifthenelse_1. eapply star_trans. eapply H0. - eapply star_left. right; eapply step_ifthenelse_false; eauto. - eexact A1. + eapply star_left. 2: eexact A1. right; eapply step_ifthenelse_2; eauto. reflexivity. reflexivity. traceEq. auto. @@ -2355,23 +2301,14 @@ Proof. eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. -(* condition true *) - destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 (typeof a2))) f k) - as [P [Q R]]. - eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_plus. eapply plus_right. eexact R. - left; eapply step_condition_true; eauto. congruence. - reflexivity. - eapply COE with (C := fun x => (C (Eparen x (typeof a2)))). eauto. - eapply leftcontext_compose; eauto. repeat constructor. traceEq. -(* condition false *) - destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 (typeof a3))) f k) +(* condition *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_plus. eapply plus_right. eexact R. - left; eapply step_condition_false; eauto. congruence. + left; eapply step_condition; eauto. rewrite Q; eauto. reflexivity. - eapply COE with (C := fun x => (C (Eparen x (typeof a3)))). eauto. + eapply COE with (C := fun x => (C (Eparen x ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. @@ -2449,18 +2386,11 @@ Proof. (* if test *) eapply forever_N_plus. apply plus_one; right; constructor. eapply COE with (C := fun x => x); eauto. constructor. traceEq. -(* if true *) - eapply forever_N_plus. - eapply plus_left. right; constructor. - eapply star_right. eapply eval_expression_to_steps; eauto. - right. apply step_ifthenelse_true. auto. - reflexivity. reflexivity. - eapply COS; eauto. traceEq. -(* if false *) +(* if true/false *) eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_right. eapply eval_expression_to_steps; eauto. - right. apply step_ifthenelse_false. auto. + right. eapply step_ifthenelse_2 with (b := b). auto. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* return some *) diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 5df8243..223d75c 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -26,50 +26,6 @@ Open Scope error_monad_scope. (** * Evaluation of compile-time constant expressions *) -(** Computing the predicates [cast], [is_true], and [is_false]. *) - -Definition bool_val (v: val) (t: type) : res bool := - match v, t with - | Vint n, Tint sz sg => OK (negb (Int.eq n Int.zero)) - | Vint n, Tpointer t' => OK (negb (Int.eq n Int.zero)) - | Vptr b ofs, Tint sz sg => OK true - | Vptr b ofs, Tpointer t' => OK true - | Vfloat f, Tfloat sz => OK (negb(Float.cmp Ceq f Float.zero)) - | _, _ => Error(msg "undefined conditional") - end. - -Definition is_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. - -Definition do_cast (v: val) (t1 t2: type) : res val := - match v, t1, t2 with - | Vint i, Tint sz1 si1, Tint sz2 si2 => - OK (Vint (cast_int_int sz2 si2 i)) - | Vfloat f, Tfloat sz1, Tint sz2 si2 => - match cast_float_int si2 f with - | Some i => OK (Vint (cast_int_int sz2 si2 i)) - | None => Error(msg "overflow in float-to-int cast") - end - | Vint i, Tint sz1 si1, Tfloat sz2 => - OK (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) - | Vfloat f, Tfloat sz1, Tfloat sz2 => - OK (Vfloat (cast_float_float sz2 f)) - | Vptr b ofs, _, _ => - if is_neutral_for_cast t1 && is_neutral_for_cast t2 - then OK(Vptr b ofs) else Error(msg "undefined cast") - | Vint n, _, _ => - if is_neutral_for_cast t1 && is_neutral_for_cast t2 - then OK(Vint n) else Error(msg "undefined cast") - | _, _, _ => - Error(msg "undefined cast") - end. - (** To evaluate constant expressions at compile-time, we use the same [value] type and the same [sem_*] functions that are used in CompCert C's semantics (module [Csem]). However, we interpret pointer values symbolically: @@ -87,6 +43,12 @@ If [a] is a l-value, the returned value denotes: - [Vptr id ofs]: global variable [id] plus byte offset [ofs] *) +Definition do_cast (v: val) (t1 t2: type) : res val := + match sem_cast v t1 t2 with + | Some v' => OK v' + | None => Error(msg "undefined cast") + end. + Fixpoint constval (a: expr) : res val := match a with | Eval v ty => @@ -115,15 +77,18 @@ Fixpoint constval (a: expr) : res val := | None => Error(msg "undefined binary operation") end | Ecast r ty => - do v <- constval r; do_cast v (typeof r) ty + do v1 <- constval r; do_cast v1 (typeof r) ty | Esizeof ty1 ty => OK (Vint (Int.repr (sizeof ty1))) | Econdition r1 r2 r3 ty => do v1 <- constval r1; - do b1 <- bool_val v1 (typeof r1); do v2 <- constval r2; do v3 <- constval r3; - OK (if b1 then v2 else v3) + match bool_val v1 (typeof r1) with + | Some true => do_cast v2 (typeof r2) ty + | Some false => do_cast v3 (typeof r3) ty + | None => Error(msg "condition is undefined") + end | Ecomma r1 r2 ty => do v1 <- constval r1; constval r2 | Evar x ty => @@ -142,7 +107,7 @@ Fixpoint constval (a: expr) : res val := Error(msg "ill-typed field access") end | Eparen r ty => - constval r + do v <- constval r; do_cast v (typeof r) ty | _ => Error(msg "not a compile-time constant") end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 10206af..d321ac5 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -116,22 +116,21 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - cast v1 (typeof r1) ty v -> + sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) - | esr_condition_true: forall r1 r2 r3 ty v v1, - eval_simple_rvalue r1 v1 -> is_true v1 (typeof r1) -> eval_simple_rvalue r2 v -> - eval_simple_rvalue (Econdition r1 r2 r3 ty) v - | esr_condition_false: forall r1 r2 r3 ty v v1, - eval_simple_rvalue r1 v1 -> is_false v1 (typeof r1) -> eval_simple_rvalue r3 v -> + | esr_condition: forall r1 r2 r3 ty v v1 b v', + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some b -> + eval_simple_rvalue (if b then r2 else r3) v' -> + sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v | esr_comma: forall r1 r2 ty v1 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> eval_simple_rvalue (Ecomma r1 r2 ty) v - | esr_paren: forall r ty v, - eval_simple_rvalue r v -> - eval_simple_rvalue (Eparen r ty) v. + | esr_paren: forall r ty v v', + eval_simple_rvalue r v -> sem_cast v (typeof r) ty = Some v' -> + eval_simple_rvalue (Eparen r ty) v'. End SIMPLE_EXPRS. @@ -169,7 +168,7 @@ Qed. Lemma rred_simple: forall r m r' m', rred r m r' m' -> simple r -> simple r'. Proof. - induction 1; simpl; tauto. + induction 1; simpl; intuition. destruct b; auto. Qed. Lemma rred_compat: @@ -183,11 +182,10 @@ Proof. inv EV. econstructor; eauto. constructor. inv EV. econstructor; eauto. constructor. constructor. inv EV. econstructor; eauto. constructor. - inv EV. eapply esr_condition_true; eauto. constructor. - inv EV. eapply esr_condition_false; eauto. constructor. + inv EV. eapply esr_condition; eauto. constructor. inv EV. constructor. econstructor; eauto. constructor. - constructor; auto. + inv EV. econstructor. constructor. auto. Qed. Lemma compat_eval_context: @@ -208,9 +206,7 @@ Proof. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. - inv H0. - eapply esr_condition_true; eauto. congruence. - eapply esr_condition_false; eauto. congruence. + inv H0. eapply esr_condition; eauto. congruence. inv H0. inv H0. inv H0. @@ -219,7 +215,7 @@ Proof. inv H0. red; split; intros. auto. inv H0. inv H0. econstructor; eauto. - inv H0. constructor. auto. + inv H0. econstructor; eauto. congruence. Qed. Lemma simple_context_1: @@ -397,49 +393,31 @@ Proof. eapply sem_cmp_match; eauto. Qed. -Lemma is_neutral_for_cast_correct: - forall t, neutral_for_cast t -> is_neutral_for_cast t = true. -Proof. - induction 1; simpl; auto. -Qed. - -Lemma cast_match: - forall v1 ty1 ty2 v2, cast v1 ty1 ty2 v2 -> +Lemma sem_cast_match: + forall v1 ty1 ty2 v2, sem_cast v1 ty1 ty2 = Some v2 -> forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> match_val v2' v2. Proof. - induction 1; intros v1' v2' MV DC; inv MV; simpl in DC. - inv DC; constructor. - rewrite H in DC. inv DC. constructor. - inv DC; constructor. - inv DC; constructor. - rewrite (is_neutral_for_cast_correct _ H) in DC. - rewrite (is_neutral_for_cast_correct _ H0) in DC. - simpl in DC. inv DC. constructor; auto. - rewrite (is_neutral_for_cast_correct _ H) in DC. - rewrite (is_neutral_for_cast_correct _ H0) in DC. - simpl in DC. - assert (OK v2' = OK (Vint n)). - inv H; auto. inv H0; auto. - inv H1. constructor. -Qed. - -Lemma bool_val_true: - forall v v' ty, is_true v' ty -> match_val v v' -> bool_val v ty = OK true. -Proof. - induction 1; intros MV; inv MV; simpl; auto. - predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. - predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. - rewrite H; auto. + intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] _eqn; inv H1. + inv H0. + replace v2' with v2 by congruence. + functional inversion H; subst; constructor. + replace v2' with v2 by congruence. + functional inversion H; subst; constructor. + simpl in H; simpl in Heqo. + destruct (neutral_for_cast ty1 && neutral_for_cast ty2); inv H; inv Heqo. + constructor; auto. + functional inversion H. Qed. -Lemma bool_val_false: - forall v v' ty, is_false v' ty -> match_val v v' -> bool_val v ty = OK false. +Lemma bool_val_match: + forall v v' ty, + match_val v v' -> + bool_val v ty = bool_val v' ty. Proof. - induction 1; intros MV; inv MV; simpl; auto. - rewrite H; auto. + intros. inv H; auto. Qed. - + (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -456,7 +434,7 @@ with constval_lvalue: match_val v' (Vptr b ofs). Proof. (* rvalue *) - induction 1; intros v' CV; simpl in CV; try (monadInv CV). + induction 1; intros vres CV; simpl in CV; try (monadInv CV). (* val *) destruct v; monadInv CV; constructor. (* rval *) @@ -471,17 +449,16 @@ Proof. revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2. eapply sem_binary_match; eauto. (* cast *) - eapply cast_match; eauto. + eapply sem_cast_match; eauto. (* sizeof *) constructor. - (* conditional true *) - assert (x0 = true). exploit bool_val_true; eauto. congruence. subst x0. auto. - (* conditional false *) - assert (x0 = false). exploit bool_val_false; eauto. congruence. subst x0. auto. + (* conditional *) + rewrite (bool_val_match x v1 (typeof r1)) in EQ3; auto. + rewrite H0 in EQ3. destruct b; eapply sem_cast_match; eauto. (* comma *) auto. (* paren *) - auto. + eapply sem_cast_match; eauto. (* lvalue *) induction 1; intros v' CV; simpl in CV; try (monadInv CV). @@ -528,14 +505,14 @@ Theorem transl_init_single_steps: forall ty a data f m w v1 ty1 m' v chunk b ofs m'', transl_init_single ty a = OK data -> star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') -> - cast v1 ty1 ty v -> + sem_cast v1 ty1 ty = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> Genv.store_init_data ge m b ofs data = Some m''. Proof. intros. monadInv H. exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. - exploit cast_match; eauto. intros D. + exploit sem_cast_match; eauto. intros D. unfold Genv.store_init_data. inv D. (* int *) @@ -725,7 +702,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'', star step ge (ExprState dummy_function a Kstop empty_env m) E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') -> - cast v1 ty1 ty v -> + sem_cast v1 ty1 ty = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> exec_init m b ofs ty (Init_single a) m'' diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a10e55e..a2e810b 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -20,6 +20,7 @@ Require Import Floats. Require Import Values. Require Import AST. Require Import Csyntax. +Require Import Csem. Require Import Clight. Module C := Csyntax. @@ -102,10 +103,26 @@ Definition makeseq (l: list statement) : statement := (** Smart constructor for [if ... then ... else]. *) -Function makeif (a: expr) (s1 s2: statement) : statement := +Function eval_simpl_expr (a: expr) : option val := match a with - | Econst_int n _ => if Int.eq_dec n Int.zero then s2 else s1 - | _ => Sifthenelse a s1 s2 + | Econst_int n _ => Some(Vint n) + | Econst_float n _ => Some(Vfloat n) + | Ecast b ty => + match eval_simpl_expr b with + | None => None + | Some v => sem_cast v (typeof b) ty + end + | _ => None + end. + +Function makeif (a: expr) (s1 s2: statement) : statement := + match eval_simpl_expr a with + | Some v => + match bool_val v (typeof a) with + | Some b => if b then s1 else s2 + | None => Sifthenelse a s1 s2 + end + | None => Sifthenelse a s1 s2 end. (** Translation of pre/post-increment/decrement. *) @@ -130,21 +147,28 @@ Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr := of the original expression. [a] is meaningless. *) -Inductive purpose : Type := +Inductive destination : Type := | For_val | For_effects - | For_test (s1 s2: statement). + | For_test (tyl: list type) (s1 s2: statement). Definition dummy_expr := Econst_int Int.zero (Tint I32 Signed). -Definition finish (dst: purpose) (sl: list statement) (a: expr) := +Definition finish (dst: destination) (sl: list statement) (a: expr) := match dst with | For_val => (sl, a) | For_effects => (sl, a) - | For_test s1 s2 => (sl ++ makeif a s1 s2 :: nil, a) + | For_test tyl s1 s2 => (sl ++ makeif (fold_left Ecast tyl a) s1 s2 :: nil, a) end. -Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := +Definition cast_destination (ty: type) (dst: destination) := + match dst with + | For_val => For_val + | For_effects => For_effects + | For_test tyl s1 s2 => For_test (ty :: tyl) s1 s2 + end. + +Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr) := match a with | C.Eloc b ofs ty => error (msg "SimplExpr.transl_expr: C.Eloc") @@ -182,15 +206,15 @@ Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := ret (finish dst sl1 (Ecast a1 ty)) | C.Econdition r1 r2 r3 ty => do (sl1, a1) <- transl_expr For_val r1; - do (sl2, a2) <- transl_expr dst r2; - do (sl3, a3) <- transl_expr dst r3; + do (sl2, a2) <- transl_expr (cast_destination ty dst) r2; + do (sl3, a3) <- transl_expr (cast_destination ty dst) r3; match dst with | For_val => do t <- gensym ty; - ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t a2)) - (Ssequence (makeseq sl3) (Sset t a3)) :: nil, + ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty))) + (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil, Etempvar t ty) - | For_effects | For_test _ _ => + | For_effects | For_test _ _ _ => ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, dummy_expr) end @@ -200,7 +224,7 @@ Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := let ty1 := C.typeof l1 in let ty2 := C.typeof r2 in match dst with - | For_val | For_test _ _ => + | For_val | For_test _ _ _ => do t <- gensym ty2; ret (finish dst (sl1 ++ sl2 ++ Sset t a2 :: Sassign a1 (Etempvar t ty2) :: nil) @@ -214,7 +238,7 @@ Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := do (sl2, a2) <- transl_expr For_val r2; let ty1 := C.typeof l1 in match dst with - | For_val | For_test _ _ => + | For_val | For_test _ _ _ => do t <- gensym tyres; ret (finish dst (sl1 ++ sl2 ++ @@ -229,7 +253,7 @@ Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := do (sl1, a1) <- transl_expr For_val l1; let ty1 := C.typeof l1 in match dst with - | For_val | For_test _ _ => + | For_val | For_test _ _ _ => do t <- gensym ty1; ret (finish dst (sl1 ++ Sset t a1 :: @@ -247,7 +271,7 @@ Fixpoint transl_expr (dst: purpose) (a: C.expr) : mon (list statement * expr) := do (sl1, a1) <- transl_expr For_val r1; do (sl2, al2) <- transl_exprlist rl2; match dst with - | For_val | For_test _ _ => + | For_val | For_test _ _ _ => do t <- gensym ty; ret (finish dst (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: nil) (Etempvar t ty)) @@ -275,7 +299,7 @@ Definition transl_expr_stmt (r: C.expr) : mon statement := do (sl, a) <- transl_expr For_effects r; ret (makeseq sl). Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement := - do (sl, a) <- transl_expr (For_test s1 s2) r; ret (makeseq sl). + do (sl, a) <- transl_expr (For_test nil s1 s2) r; ret (makeseq sl). (** Translation of statements *) diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index ca45b4d..2372d02 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -143,8 +143,10 @@ Lemma tr_simple: match dst with | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil - | For_test s1 s2 => - exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v + | For_test tyl s1 s2 => + exists b, sl = makeif (fold_left Ecast tyl b) s1 s2 :: nil + /\ C.typeof r = typeof b + /\ eval_expr tge e le m b v end) /\ (forall l b ofs, @@ -217,8 +219,8 @@ Lemma tr_simple_rvalue: match dst with | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil - | For_test s1 s2 => - exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v + | For_test tyl s1 s2 => + exists b, sl = makeif (fold_left Ecast tyl b) s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v end. Proof. intros e m. exact (proj1 (tr_simple e m)). @@ -259,7 +261,7 @@ Proof. induction 1; intros; auto. Qed. -Inductive compat_dest: (C.expr -> C.expr) -> purpose -> purpose -> list statement -> Prop := +Inductive compat_dest: (C.expr -> C.expr) -> destination -> destination -> list statement -> Prop := | compat_dest_base: forall dst, compat_dest (fun x => x) dst dst nil | compat_dest_val: forall C dst sl, @@ -267,7 +269,7 @@ Inductive compat_dest: (C.expr -> C.expr) -> purpose -> purpose -> list statemen | compat_dest_effects: forall C dst sl, compat_dest C For_effects dst sl | compat_dest_paren: forall C ty dst' dst sl, - compat_dest C dst' dst sl -> + compat_dest C dst' (cast_destination ty dst) sl -> compat_dest (fun x => C.Eparen (C x) ty) dst' dst sl. Lemma compat_dest_not_test: @@ -277,6 +279,7 @@ Lemma compat_dest_not_test: dst' = For_val \/ dst' = For_effects. Proof. induction 1; intros; auto. + apply IHcompat_dest. destruct H0; subst; auto. Qed. Lemma compat_dest_change: @@ -288,6 +291,18 @@ Proof. intros. exploit compat_dest_not_test; eauto. intros [A | A]; subst dst'; constructor. Qed. +Lemma compat_dest_test: + forall C tyl s1 s2 dst sl, + compat_dest C (For_test tyl s1 s2) dst sl -> + exists tyl', exists tyl'', dst = For_test tyl'' s1 s2 /\ tyl = tyl' ++ tyl''. +Proof. + intros. dependent induction H. + exists (@nil type); exists tyl; auto. + exploit IHcompat_dest; eauto. intros [l1 [l2 [A B]]]. + destruct dst; simpl in A; inv A. + exists (l1 ++ ty :: nil); exists tyl0; split; auto. rewrite app_ass. auto. +Qed. + Scheme leftcontext_ind2 := Minimality for leftcontext Sort Prop with leftcontextlist_ind2 := Minimality for leftcontextlist Sort Prop. Combined Scheme leftcontext_leftcontextlist_ind from leftcontext_ind2, leftcontextlist_ind2. @@ -314,7 +329,7 @@ Lemma tr_expr_leftcontext_rec: exists dst', exists sl1, exists sl2, exists a', exists tmp', tr_expr le dst' e sl1 a' tmp' /\ sl = sl1 ++ sl2 - /\ match dst' with For_test _ _ => False | _ => True end + /\ match dst' with For_test _ _ _ => False | _ => True end /\ incl tmp' tmps /\ (forall le' e' sl3, tr_expr le' dst' e' sl3 a' tmp' -> @@ -618,7 +633,7 @@ Proof. intros. rewrite <- app_nil_end. constructor; auto. (* val for test *) inv H2; inv H1. - exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor. + exists (For_test tyl s1 s2); econstructor; econstructor; econstructor; econstructor. split. apply tr_top_val_test; eauto. split. instantiate (1 := nil); auto. split. constructor. @@ -634,7 +649,7 @@ Proof. (* paren *) inv H1; inv H0. (* at top *) - exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor. + exists (For_test tyl s1 s2); econstructor; econstructor; econstructor; econstructor. split. apply tr_top_paren_test; eauto. split. instantiate (1 := nil). rewrite <- app_nil_end; auto. split. constructor. @@ -652,45 +667,43 @@ Proof. Qed. Theorem tr_top_testcontext: - forall C s1 s2 dst sl2 r sl1 a tmps e le m, - compat_dest C (For_test s1 s2) dst sl2 -> - tr_top tge e le m (For_test s1 s2) r sl1 a tmps -> - dst = For_test s1 s2 /\ tr_top tge e le m dst (C r) (sl1 ++ sl2) a tmps. + forall C tyl s1 s2 dst sl2 r sl1 a tmps e le m, + compat_dest C (For_test tyl s1 s2) dst sl2 -> + tr_top tge e le m (For_test tyl s1 s2) r sl1 a tmps -> + tr_top tge e le m dst (C r) (sl1 ++ sl2) a tmps. Proof. intros. dependent induction H. - split. auto. rewrite <- app_nil_end. auto. - exploit IHcompat_dest; eauto. intros [A B]. - split. auto. subst dst. apply tr_top_paren_test. auto. + rewrite <- app_nil_end. auto. + exploit compat_dest_test; eauto. intros [l1 [l2 [A B]]]. + destruct dst; simpl in A; inv A. + apply tr_top_paren_test. eapply IHcompat_dest; eauto. Qed. (** Semantics of smart constructors *) -Lemma step_makeif_true: - forall f a s1 s2 k e le m v1, - eval_expr tge e le m a v1 -> - is_true v1 (typeof a) -> - star step tge (State f (makeif a s1 s2) k e le m) - E0 (State f s1 k e le m). +Lemma eval_simpl_expr_sound: + forall e le m a v, eval_expr tge e le m a v -> + match eval_simpl_expr a with Some v' => v' = v | None => True end. Proof. - intros. functional induction (makeif a s1 s2). - inversion H. subst v1. inversion H0. congruence. congruence. - inversion H1. - apply star_refl. - apply star_one. apply step_ifthenelse_true with v1; auto. + induction 1; simpl; auto. + destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto. + inv H; simpl; auto. Qed. -Lemma step_makeif_false: - forall f a s1 s2 k e le m v1, +Lemma step_makeif: + forall f a s1 s2 k e le m v1 b, eval_expr tge e le m a v1 -> - is_false v1 (typeof a) -> + bool_val v1 (typeof a) = Some b -> star step tge (State f (makeif a s1 s2) k e le m) - E0 (State f s2 k e le m). + E0 (State f (if b then s1 else s2) k e le m). Proof. intros. functional induction (makeif a s1 s2). - apply star_refl. - inversion H. subst v1. inversion H0. congruence. congruence. - inversion H1. - apply star_one. apply step_ifthenelse_false with v1; auto. + exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + rewrite e1 in H0. inv H0. constructor. + exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + rewrite e1 in H0. inv H0. constructor. + apply star_one. eapply step_ifthenelse; eauto. + apply star_one. eapply step_ifthenelse; eauto. Qed. (** Matching between continuations *) @@ -759,7 +772,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop := match_cont (Csem.Kcall f e C ty k) (Kcall (Some dst) tf e le (Kseqlist sl tk)) -with match_cont_exp : purpose -> expr -> Csem.cont -> cont -> Prop := +with match_cont_exp : destination -> expr -> Csem.cont -> cont -> Prop := | match_Kdo: forall k a tk, match_cont k tk -> match_cont_exp For_effects a (Csem.Kdo k) tk @@ -770,19 +783,19 @@ with match_cont_exp : purpose -> expr -> Csem.cont -> cont -> Prop := | match_Kifthenelse_2: forall a s1 s2 k ts1 ts2 tk, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> match_cont k tk -> - match_cont_exp (For_test ts1 ts2) a (Csem.Kifthenelse s1 s2 k) tk + match_cont_exp (For_test nil ts1 ts2) a (Csem.Kifthenelse s1 s2 k) tk | match_Kwhile1: forall r s k s' a ts tk, tr_if r Sskip Sbreak s' -> tr_stmt s ts -> match_cont k tk -> - match_cont_exp (For_test Sskip Sbreak) a + match_cont_exp (For_test nil Sskip Sbreak) a (Csem.Kwhile1 r s k) (Kseq ts (Kwhile expr_true (Ssequence s' ts) tk)) | match_Kdowhile2: forall r s k s' a ts tk, tr_if r Sskip Sbreak s' -> tr_stmt s ts -> match_cont k tk -> - match_cont_exp (For_test Sskip Sbreak) a + match_cont_exp (For_test nil Sskip Sbreak) a (Csem.Kdowhile2 r s k) (Kfor3 expr_true s' ts tk) | match_Kfor2: forall r s3 s k s' a ts3 ts tk, @@ -790,7 +803,7 @@ with match_cont_exp : purpose -> expr -> Csem.cont -> cont -> Prop := tr_stmt s3 ts3 -> tr_stmt s ts -> match_cont k tk -> - match_cont_exp (For_test Sskip Sbreak) a + match_cont_exp (For_test nil Sskip Sbreak) a (Csem.Kfor2 r s3 s k) (Kseq ts (Kfor2 expr_true ts3 (Ssequence s' ts) tk)) | match_Kswitch1: forall ls k a tls tk, @@ -810,9 +823,9 @@ Proof. Qed. Lemma match_cont_exp_for_test_inv: - forall s1 s2 a a' k tk, - match_cont_exp (For_test s1 s2) a k tk -> - match_cont_exp (For_test s1 s2) a' k tk. + forall tyl s1 s2 a a' k tk, + match_cont_exp (For_test tyl s1 s2) a k tk -> + match_cont_exp (For_test tyl s1 s2) a' k tk. Proof. intros. inv H; econstructor; eauto. Qed. @@ -915,13 +928,14 @@ Lemma makeif_nolabel: Proof. intros. functional induction (makeif a s1 s2); auto. red; simpl; intros. rewrite H; auto. + red; simpl; intros. rewrite H; auto. Qed. -Definition nolabel_dest (dst: purpose) : Prop := +Definition nolabel_dest (dst: destination) : Prop := match dst with | For_val => True | For_effects => True - | For_test s1 s2 => nolabel s1 /\ nolabel s2 + | For_test tyl s1 s2 => nolabel s1 /\ nolabel s2 end. Lemma nolabel_final: @@ -931,6 +945,12 @@ Proof. split; auto. destruct H. apply makeif_nolabel; auto. Qed. +Lemma nolabel_dest_cast: + forall ty dst, nolabel_dest dst -> nolabel_dest (cast_destination ty dst). +Proof. + unfold nolabel_dest; intros; destruct dst; auto. +Qed. + Ltac NoLabelTac := match goal with | [ |- nolabel_list nil ] => exact I @@ -955,8 +975,9 @@ Proof. rewrite (makeseq_nolabel sl2); auto. rewrite (makeseq_nolabel sl3); auto. apply makeif_nolabel; NoLabelTac. - rewrite (makeseq_nolabel sl2); auto. - rewrite (makeseq_nolabel sl3); auto. + rewrite (makeseq_nolabel sl2). auto. apply H3. apply nolabel_dest_cast; auto. + rewrite (makeseq_nolabel sl3). auto. apply H5. apply nolabel_dest_cast; auto. + apply nolabel_dest_cast; auto. Qed. Lemma tr_find_label_top: @@ -1215,29 +1236,38 @@ Proof. intros A. subst sl. apply tr_top_base. constructor. intros [b [A [B C]]]. subst sl. apply tr_top_val_test; auto. (* condition true *) - exploit tr_top_leftcontext; eauto. clear H10. + exploit tr_top_leftcontext; eauto. clear H9. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. inv P. inv H2. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. - subst sl0; simpl Kseqlist. + subst sl0; simpl Kseqlist. destruct b. econstructor; split. left. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_true with v; auto. congruence. - eapply star_left. constructor. apply push_seq. - reflexivity. reflexivity. traceEq. - replace (Kseqlist sl3 (Kseq (Sset t a2) (Kseqlist sl2 tk))) - with (Kseqlist (sl3 ++ Sset t a2 :: sl2) tk). + eapply star_trans. apply step_makeif with (b := true) (v1 := v); auto. congruence. + eapply star_left. constructor. apply push_seq. reflexivity. reflexivity. traceEq. + replace (Kseqlist sl3 (Kseq (Sset t (Ecast a2 ty)) (Kseqlist sl2 tk))) + with (Kseqlist (sl3 ++ Sset t (Ecast a2 ty) :: sl2) tk). eapply match_exprstates; eauto. - change (Sset t a2 :: sl2) with ((Sset t a2 :: nil) ++ sl2). rewrite <- app_ass. + change (Sset t (Ecast a2 ty) :: sl2) with ((Sset t (Ecast a2 ty) :: nil) ++ sl2). rewrite <- app_ass. apply S. econstructor; eauto. auto. auto. - rewrite Kseqlist_app. auto. - (* for effects *) + rewrite Kseqlist_app. auto. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_trans. apply step_makeif with (b := false) (v1 := v); auto. congruence. + eapply star_left. constructor. apply push_seq. reflexivity. reflexivity. traceEq. + replace (Kseqlist sl4 (Kseq (Sset t (Ecast a3 ty)) (Kseqlist sl2 tk))) + with (Kseqlist (sl4 ++ Sset t (Ecast a3 ty) :: sl2) tk). + eapply match_exprstates; eauto. + change (Sset t (Ecast a3 ty) :: sl2) with ((Sset t (Ecast a3 ty) :: nil) ++ sl2). rewrite <- app_ass. + apply S. econstructor; eauto. auto. auto. + rewrite Kseqlist_app. auto. + (* for effects *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. - subst sl0; simpl Kseqlist. + subst sl0; simpl Kseqlist. destruct b. econstructor; split. left. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_true with v; auto. congruence. + eapply star_trans. apply step_makeif with (b := true) (v1 := v); auto. congruence. apply push_seq. reflexivity. traceEq. rewrite <- Kseqlist_app. @@ -1245,36 +1275,16 @@ Proof. econstructor; eauto. apply tr_expr_monotone with tmp2; eauto. econstructor; eauto. auto. auto. -(* condition false *) - exploit tr_top_leftcontext; eauto. clear H10. - intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. - inv P. inv H2. - (* for value *) - exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. - subst sl0; simpl Kseqlist. econstructor; split. left. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_false with v; auto. congruence. - eapply star_left. constructor. apply push_seq. - reflexivity. reflexivity. traceEq. - replace (Kseqlist sl4 (Kseq (Sset t a3) (Kseqlist sl2 tk))) - with (Kseqlist (sl4 ++ Sset t a3 :: sl2) tk). - eapply match_exprstates; eauto. - change (Sset t a3 :: sl2) with ((Sset t a3 :: nil) ++ sl2). rewrite <- app_ass. - apply S. econstructor; eauto. auto. auto. - rewrite Kseqlist_app. auto. - (* for effects *) - exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. - subst sl0; simpl Kseqlist. - econstructor; split. - left. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_false with v; auto. congruence. + eapply star_trans. apply step_makeif with (b := false) (v1 := v); auto. congruence. apply push_seq. reflexivity. traceEq. rewrite <- Kseqlist_app. econstructor. eauto. apply S. econstructor; eauto. apply tr_expr_monotone with tmp3; eauto. - auto. auto. auto. + econstructor; eauto. + auto. auto. (* assign *) exploit tr_top_leftcontext; eauto. clear H12. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. @@ -1408,15 +1418,16 @@ Proof. (* paren *) exploit tr_top_leftcontext; eauto. clear H9. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. - inv P. inv H1. + inv P. inv H2. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]]. subst sl0; simpl Kseqlist. econstructor; split. left. eapply plus_left. constructor. apply star_one. - econstructor. eauto. traceEq. - econstructor; eauto. change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S. - constructor. auto. intros. constructor. rewrite H1; auto. apply PTree.gss. + econstructor. econstructor; eauto. rewrite <- TY1; eauto. traceEq. + econstructor; eauto. + change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S. + constructor. auto. intros. constructor. rewrite H2; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. (* for effects *) @@ -1424,7 +1435,7 @@ Proof. right; split. apply star_refl. simpl. apply plus_lt_compat_r. apply (leftcontext_size _ _ _ H). simpl. omega. econstructor; eauto. - exploit tr_simple_rvalue; eauto. destruct dst'. + exploit tr_simple_rvalue; eauto. destruct dst'; simpl. (* dst' = For_val: impossible *) congruence. (* dst' = For_effects: easy *) @@ -1433,16 +1444,16 @@ Proof. so we can apply tr_top_paren. *) intros [b [A [B D]]]. eapply tr_top_testcontext; eauto. - subst sl1. apply tr_top_val_test; auto. + subst sl1. apply tr_top_val_test; auto. econstructor; eauto. rewrite <- B; auto. (* already reduced *) econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. apply (leftcontext_size _ _ _ H). simpl. omega. econstructor; eauto. instantiate (1 := @nil ident). - inv H7. - inv H0. eapply tr_top_testcontext; eauto. constructor. auto. auto. + inv H9. + inv H0. eapply tr_top_testcontext; eauto. simpl. constructor. auto. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros [b [A [B D]]]. - eapply tr_top_testcontext; eauto. subst sl1. apply tr_top_val_test. auto. auto. + eapply tr_top_testcontext; eauto. subst sl1. apply tr_top_val_test. auto. econstructor; eauto. congruence. inv H0. (* call *) exploit tr_top_leftcontext; eauto. clear H12. @@ -1492,7 +1503,7 @@ Qed. Lemma tr_top_val_for_test_inv: forall s1 s2 e le m v ty sl a tmps, - tr_top tge e le m (For_test s1 s2) (C.Eval v ty) sl a tmps -> + tr_top tge e le m (For_test nil s1 s2) (C.Eval v ty) sl a tmps -> exists b, sl = makeif b s1 s2 :: nil /\ typeof b = ty /\ eval_expr tge e le m b v. Proof. intros. inv H. exists a0; auto. @@ -1546,40 +1557,26 @@ Proof. inv H10. econstructor; split. right; split. apply push_seq. simpl. omega. econstructor; eauto. constructor; auto. -(* ifthenelse true *) - inv H8. - (* not optimized *) - exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. - econstructor; split. - left. eapply plus_two. constructor. - apply step_ifthenelse_true with v; auto. traceEq. - econstructor; eauto. - (* optimized *) - exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. - econstructor; split. - left. simpl. eapply plus_left. constructor. - apply step_makeif_true with v; auto. traceEq. - econstructor; eauto. -(* ifthenelse false *) +(* ifthenelse *) inv H8. (* not optimized *) exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. - apply step_ifthenelse_false with v; auto. traceEq. - econstructor; eauto. + apply step_ifthenelse with (v1 := v) (b := b); auto. traceEq. + destruct b; econstructor; eauto. (* optimized *) - exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + exploit tr_top_val_for_test_inv; eauto. intros [c [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - apply step_makeif_false with v; auto. traceEq. + apply step_makeif with (v1 := v) (b := b); auto. traceEq. econstructor; eauto. + destruct b; auto. (* while *) inv H6. inv H1. econstructor; split. - left. eapply plus_left. eapply step_while_true. constructor. - simpl. constructor. apply Int.one_not_zero. - eapply star_left. constructor. + left. eapply plus_left. eapply step_while_true. constructor. + auto. eapply star_left. constructor. apply push_seq. reflexivity. traceEq. econstructor; eauto. econstructor; eauto. econstructor; eauto. @@ -1588,7 +1585,7 @@ Proof. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_false with v; auto. + eapply star_trans. apply step_makeif with (v1 := v) (b := false); auto. eapply star_two. constructor. apply step_break_while. reflexivity. reflexivity. traceEq. constructor; auto. constructor. @@ -1597,7 +1594,7 @@ Proof. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_right. apply step_makeif_true with v; auto. + eapply star_right. apply step_makeif with (v1 := v) (b := true); auto. constructor. reflexivity. traceEq. constructor; auto. constructor; auto. @@ -1617,7 +1614,7 @@ Proof. inv H6. econstructor; split. left. apply plus_one. - apply step_for_true with (Vint Int.one). constructor. simpl; constructor. apply Int.one_not_zero. + apply step_for_true with (Vint Int.one). constructor. auto. constructor; auto. constructor; auto. (* skip_or_continue dowhile *) assert (ts = Sskip \/ ts = Scontinue). destruct H; subst s0; inv H7; auto. @@ -1632,7 +1629,7 @@ Proof. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_right. apply step_makeif_false with v; auto. + eapply star_right. apply step_makeif with (v1 := v) (b := false); auto. constructor. reflexivity. traceEq. constructor; auto. constructor. @@ -1641,7 +1638,7 @@ Proof. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_right. apply step_makeif_true with v; auto. + eapply star_right. apply step_makeif with (v1 := v) (b := true); auto. constructor. reflexivity. traceEq. constructor; auto. constructor; auto. @@ -1660,7 +1657,7 @@ Proof. inv H6; try congruence. inv H2. econstructor; split. left. eapply plus_left. apply step_for_true with (Vint Int.one). - constructor. simpl; constructor. apply Int.one_not_zero. + constructor. auto. eapply star_left. constructor. apply push_seq. reflexivity. traceEq. econstructor; eauto. constructor; auto. econstructor; eauto. @@ -1668,7 +1665,7 @@ Proof. inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_trans. apply step_makeif_false with v; auto. + eapply star_trans. apply step_makeif with (v1 := v) (b := false); auto. eapply star_two. constructor. apply step_break_for2. reflexivity. reflexivity. traceEq. constructor; auto. constructor. @@ -1676,7 +1673,7 @@ Proof. inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. econstructor; split. left. simpl. eapply plus_left. constructor. - eapply star_right. apply step_makeif_true with v; auto. + eapply star_right. apply step_makeif with (v1 := v) (b := true); auto. constructor. reflexivity. traceEq. constructor; auto. constructor; auto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 7829c24..1224ea9 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -41,14 +41,14 @@ Local Open Scope gensym_monad_scope. matching the given temporary environment [le]. *) -Definition final (dst: purpose) (a: expr) : list statement := +Definition final (dst: destination) (a: expr) : list statement := match dst with | For_val => nil | For_effects => nil - | For_test s1 s2 => makeif a s1 s2 :: nil + | For_test tyl s1 s2 => makeif (fold_left Ecast tyl a) s1 s2 :: nil end. -Inductive tr_expr: temp_env -> purpose -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop := | tr_var: forall le dst id ty tmp, tr_expr le dst (C.Evar id ty) (final dst (Evar id ty)) (Evar id ty) tmp @@ -69,13 +69,13 @@ Inductive tr_expr: temp_env -> purpose -> C.expr -> list statement -> expr -> li eval_expr tge e le' m a v) -> tr_expr le For_val (C.Eval v ty) nil a tmp - | tr_val_test: forall le s1 s2 v ty a any tmp, + | tr_val_test: forall le tyl s1 s2 v ty a any tmp, typeof a = ty -> (forall tge e le' m, (forall id, In id tmp -> le'!id = le!id) -> eval_expr tge e le' m a v) -> - tr_expr le (For_test s1 s2) (C.Eval v ty) - (makeif a s1 s2 :: nil) any tmp + tr_expr le (For_test tyl s1 s2) (C.Eval v ty) + (makeif (fold_left Ecast tyl a) s1 s2 :: nil) any tmp | tr_sizeof: forall le dst ty' ty tmp, tr_expr le dst (C.Esizeof ty' ty) (final dst (Esizeof ty' ty)) @@ -117,14 +117,14 @@ Inductive tr_expr: temp_env -> purpose -> C.expr -> list statement -> expr -> li In t tmp -> ~In t tmp1 -> tr_expr le For_val (C.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 - (Ssequence (makeseq sl2) (Sset t a2)) - (Ssequence (makeseq sl3) (Sset t a3)) :: nil) + (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty))) + (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil) (Etempvar t ty) tmp | tr_condition_effects: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, dst <> For_val -> tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le dst e2 sl2 a2 tmp2 -> - tr_expr le dst e3 sl3 a3 tmp3 -> + tr_expr le (cast_destination ty dst) e2 sl2 a2 tmp2 -> + tr_expr le (cast_destination ty dst) e3 sl3 a3 tmp3 -> list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> @@ -215,11 +215,11 @@ Inductive tr_expr: temp_env -> purpose -> C.expr -> list statement -> expr -> li tr_expr le For_val e1 sl1 a1 tmp1 -> incl tmp1 tmp -> In t tmp -> tr_expr le For_val (C.Eparen e1 ty) - (sl1 ++ Sset t a1 :: nil) + (sl1 ++ Sset t (Ecast a1 ty) :: nil) (Etempvar t ty) tmp | tr_paren_effects: forall le dst e1 ty sl1 a1 tmp any, dst <> For_val -> - tr_expr le dst e1 sl1 a1 tmp -> + tr_expr le (cast_destination ty dst) e1 sl1 a1 tmp -> tr_expr le dst (C.Eparen e1 ty) sl1 any tmp with tr_exprlist: temp_env -> C.exprlist -> list statement -> list expr -> list ident -> Prop := @@ -249,7 +249,7 @@ with tr_exprlist_invariant: Proof. induction 1; intros; econstructor; eauto. intros. apply H0. intros. transitivity (le'!id); auto. - intros. apply H0. intros. transitivity (le'!id); auto. + intros. apply H0. auto. intros. transitivity (le'!id); auto. induction 1; intros; econstructor; eauto. Qed. @@ -281,19 +281,19 @@ Variable e: env. Variable le: temp_env. Variable m: mem. -Inductive tr_top: purpose -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident -> Prop := | tr_top_val_val: forall v ty a tmp, typeof a = ty -> eval_expr ge e le m a v -> tr_top For_val (C.Eval v ty) nil a tmp - | tr_top_val_test: forall s1 s2 v ty a any tmp, + | tr_top_val_test: forall tyl s1 s2 v ty a any tmp, typeof a = ty -> eval_expr ge e le m a v -> - tr_top (For_test s1 s2) (C.Eval v ty) (makeif a s1 s2 :: nil) any tmp + tr_top (For_test tyl s1 s2) (C.Eval v ty) (makeif (fold_left Ecast tyl a) s1 s2 :: nil) any tmp | tr_top_base: forall dst r sl a tmp, tr_expr le dst r sl a tmp -> tr_top dst r sl a tmp - | tr_top_paren_test: forall s1 s2 r ty sl a tmp, - tr_top (For_test s1 s2) r sl a tmp -> - tr_top (For_test s1 s2) (C.Eparen r ty) sl a tmp. + | tr_top_paren_test: forall tyl s1 s2 r ty sl a tmp, + tr_top (For_test (ty :: tyl) s1 s2) r sl a tmp -> + tr_top (For_test tyl s1 s2) (C.Eparen r ty) sl a tmp. End TR_TOP. @@ -311,7 +311,7 @@ Inductive tr_expr_stmt: C.expr -> statement -> Prop := Inductive tr_if: C.expr -> statement -> statement -> statement -> Prop := | tr_if_intro: forall r s1 s2 sl a tmps, - (forall ge e le m, tr_top ge e le m (For_test s1 s2) r sl a tmps) -> + (forall ge e le m, tr_top ge e le m (For_test nil s1 s2) r sl a tmps) -> tr_if r s1 s2 (makeseq sl). Inductive tr_stmt: C.statement -> statement -> Prop := @@ -662,7 +662,7 @@ Opaque makeif. (* for test *) exists (x1 :: tmp1 ++ tmp2); split. repeat rewrite app_ass. simpl. - intros. eapply tr_assign_val with (dst := For_test s1 s2); eauto with gensym. + intros. eapply tr_assign_val with (dst := For_test tyl s1 s2); eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* assignop *) @@ -681,7 +681,7 @@ Opaque makeif. (* for test *) exists (x1 :: tmp1 ++ tmp2); split. repeat rewrite app_ass. simpl. - intros. eapply tr_assignop_val with (dst := For_test s1 s2); eauto with gensym. + intros. eapply tr_assignop_val with (dst := For_test tyl s1 s2); eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* postincr *) |