From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/Cexec.v | 268 +++++++++++++++++++++++++++--------------------------- 1 file changed, 134 insertions(+), 134 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 938454c5..7e966ffe 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -85,7 +85,7 @@ Proof. intros until ty. destruct a; simpl; congruence. Qed. -Local Open Scope option_monad_scope. +Local Open Scope option_monad_scope. Fixpoint is_val_list (al: exprlist) : option (list (val * type)) := match al with @@ -110,7 +110,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval := | Vfloat f, AST.Tfloat => Some (EVfloat f) | Vsingle f, AST.Tsingle => Some (EVsingle f) | Vlong n, AST.Tlong => Some (EVlong n) - | Vptr b ofs, AST.Tint => + | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; check (Genv.public_symbol ge id); Some (EVptr_global id ofs) @@ -153,7 +153,7 @@ Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto. + rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto. Qed. Lemma list_eventval_of_val_sound: @@ -169,7 +169,7 @@ Qed. Lemma list_eventval_of_val_complete: forall evl tl vl, eventval_list_match ge evl tl vl -> list_eventval_of_val vl tl = Some evl. Proof. - induction 1; simpl. auto. + induction 1; simpl. auto. rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto. Qed. @@ -190,7 +190,7 @@ Qed. (** Volatile memory accesses. *) -Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) +Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) : option (world * trace * val) := if Genv.block_is_volatile ge b then do id <- Genv.invert_symbol ge b; @@ -230,11 +230,11 @@ Lemma do_volatile_load_sound: do_volatile_load w chunk m b ofs = Some(w', t, v) -> volatile_load ge chunk m b ofs t v /\ possible_trace w t w'. Proof. - intros until v. unfold do_volatile_load. mydestr. - destruct p as [ev w'']. mydestr. - split. constructor; auto. apply Genv.invert_find_symbol; auto. - apply val_of_eventval_sound; auto. - econstructor. constructor; eauto. constructor. + intros until v. unfold do_volatile_load. mydestr. + destruct p as [ev w'']. mydestr. + split. constructor; auto. apply Genv.invert_find_symbol; auto. + apply val_of_eventval_sound; auto. + econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. Qed. @@ -254,10 +254,10 @@ Lemma do_volatile_store_sound: do_volatile_store w chunk m b ofs v = Some(w', t, m') -> volatile_store ge chunk m b ofs v t m' /\ possible_trace w t w'. Proof. - intros until m'. unfold do_volatile_store. mydestr. - split. constructor; auto. apply Genv.invert_find_symbol; auto. - apply eventval_of_val_sound; auto. - econstructor. constructor; eauto. constructor. + intros until m'. unfold do_volatile_store. mydestr. + split. constructor; auto. apply Genv.invert_find_symbol; auto. + apply eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. Qed. @@ -297,7 +297,7 @@ Remark check_assign_copy: forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. Proof with try (right; intuition omega). - intros. unfold assign_copy_ok. + intros. unfold assign_copy_ok. assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos. destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto... destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto... @@ -314,7 +314,7 @@ Proof with try (right; intuition omega). destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto. destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto. right; intuition omega. - destruct Y... left; intuition omega. + destruct Y... left; intuition omega. Defined. Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) := @@ -343,8 +343,8 @@ Lemma do_deref_loc_sound: deref_loc ge ty m b ofs t v /\ possible_trace w t w'. Proof. unfold do_deref_loc; intros until v. - destruct (access_mode ty) eqn:?; mydestr. - intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. + destruct (access_mode ty) eqn:?; mydestr. + intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. split. eapply deref_loc_value; eauto. constructor. split. eapply deref_loc_reference; eauto. constructor. split. eapply deref_loc_copy; eauto. constructor. @@ -368,10 +368,10 @@ Lemma do_assign_loc_sound: assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'. Proof. unfold do_assign_loc; intros until m'. - destruct (access_mode ty) eqn:?; mydestr. - intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. + destruct (access_mode ty) eqn:?; mydestr. + intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. split. eapply assign_loc_value; eauto. constructor. - destruct v; mydestr. destruct a as [P [Q R]]. + destruct v; mydestr. destruct a as [P [Q R]]. split. eapply assign_loc_copy; eauto. constructor. Qed. @@ -385,7 +385,7 @@ Proof. rewrite H1; rewrite H2. apply do_volatile_store_complete; auto. rewrite H1. destruct (check_assign_copy ty b ofs b' ofs'). inv H0. rewrite H5; rewrite H6; auto. - elim n. red; tauto. + elim n. red; tauto. Qed. (** External calls *) @@ -477,7 +477,7 @@ Remark memcpy_check_args: forall sz al bdst odst bsrc osrc, {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. Proof with try (right; intuition omega). - intros. + intros. assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}). destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto. destruct (zeq al 8); auto... @@ -486,9 +486,9 @@ Proof with try (right; intuition omega). destruct (zle 0 sz)... destruct (Zdivide_dec al sz); auto... assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}). - intros. destruct (zeq sz 0). + intros. destruct (zeq sz 0). left; intros; omegaContradiction. - destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. + destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. destruct (U osrc); auto... destruct (U odst); auto... assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} @@ -555,17 +555,17 @@ Proof with try congruence. intros until m'. destruct ef; simpl. (* EF_external *) - eapply do_external_function_sound; eauto. + eapply do_external_function_sound; eauto. (* EF_builtin *) - eapply do_external_function_sound; eauto. + eapply do_external_function_sound; eauto. (* EF_vload *) - unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... + unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. - exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. + exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. auto. (* EF_vstore *) - unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... - mydestr. destruct p as [[w'' t''] m'']. mydestr. + unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... + mydestr. destruct p as [[w'' t''] m'']. mydestr. exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. auto. (* EF_malloc *) @@ -573,19 +573,19 @@ Proof with try congruence. destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr. split. econstructor; eauto. constructor. (* EF_free *) - unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. destruct v... mydestr. + unfold do_ef_free. destruct vargs... destruct v... destruct vargs... + mydestr. destruct v... mydestr. split. econstructor; eauto. omega. constructor. (* EF_memcpy *) - unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... - destruct v... destruct vargs... mydestr. red in m0. + unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... + destruct v... destruct vargs... mydestr. red in m0. split. econstructor; eauto; tauto. constructor. (* EF_annot *) - unfold do_ef_annot. mydestr. + unfold do_ef_annot. mydestr. split. constructor. apply list_eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. (* EF_annot_val *) - unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. + unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. (* EF_inline_asm *) @@ -611,7 +611,7 @@ Proof. inv H; unfold do_ef_volatile_store. exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. (* EF_malloc *) - inv H; unfold do_ef_malloc. + inv H; unfold do_ef_malloc. inv H0. rewrite H1. rewrite H2. auto. (* EF_free *) inv H; unfold do_ef_free. @@ -619,12 +619,12 @@ Proof. (* EF_memcpy *) inv H; unfold do_ef_memcpy. inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. - red. tauto. + red. tauto. (* EF_annot *) - inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. + inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. rewrite (list_eventval_of_val_complete _ _ _ H1). auto. (* EF_annot_val *) - inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. + inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. (* EF_inline_asm *) eapply do_inline_assembly_complete; eauto. @@ -837,7 +837,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do w',t, v1 <- do_deref_loc w ty m b ofs; let op := match id with Incr => Oadd | Decr => Osub end in let r' := - Ecomma (Eassign (Eloc b ofs ty) + Ecomma (Eassign (Eloc b ofs ty) (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty)) ty) (Eval v1 ty) ty in @@ -922,7 +922,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop := Remark imm_safe_t_imm_safe: forall k a m, imm_safe_t k a m -> imm_safe ge e k a m. Proof. - induction 1. + induction 1. constructor. constructor. eapply imm_safe_lred; eauto. @@ -975,7 +975,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists t, exists v1, exists w', ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w' | Epostincr id (Eloc b ofs ty1) ty => - exists t, exists v1, exists w', + exists t, exists v1, exists w', ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w' | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty @@ -1004,7 +1004,7 @@ Proof. exists b; auto. exists b; auto. exists b; exists ofs; auto. - exists b; exists ofs; split; auto. exists co, delta; auto. + exists b; exists ofs; split; auto. exists co, delta; auto. exists b; exists ofs; split; auto. exists co; auto. Qed. @@ -1072,8 +1072,8 @@ Proof. intros. elim (H0 a m); auto. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. - red; intros. destruct (C a); auto. - red; intros. destruct e1; auto. elim (H0 a m); auto. + red; intros. destruct (C a); auto. + red; intros. destruct e1; auto. elim (H0 a m); auto. Qed. Lemma imm_safe_t_inv: @@ -1086,7 +1086,7 @@ Lemma imm_safe_t_inv: end. Proof. destruct invert_expr_context as [A B]. - intros. inv H. + intros. inv H. auto. auto. assert (invert_expr_prop (C l) m). @@ -1160,7 +1160,7 @@ Proof. induction rargs; simpl; intros. inv H. destruct tyargs; simpl in H0; inv H0. constructor. monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv. - inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. + inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. Qed. Lemma sem_cast_arguments_complete: @@ -1170,7 +1170,7 @@ Lemma sem_cast_arguments_complete: Proof. induction 1. exists (@nil (val * type)); auto. - destruct IHcast_arguments as [vtl [A B]]. + destruct IHcast_arguments as [vtl [A B]]. exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto. Qed. @@ -1179,7 +1179,7 @@ Lemma topred_ok: reduction_ok k a m rd -> reducts_ok k a m (topred rd). Proof. - intros. unfold topred; split; simpl; intros. + intros. unfold topred; split; simpl; intros. destruct H0; try contradiction. inv H0. exists a; exists k; auto. congruence. Qed. @@ -1199,7 +1199,7 @@ Lemma wrong_kind_ok: k <> Cstrategy.expr_kind a -> reducts_ok k a m stuck. Proof. - intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto. + intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto. eapply imm_safe_t_imm_safe; eauto. Qed. @@ -1212,9 +1212,9 @@ Lemma not_invert_ok: end -> reducts_ok k a m stuck. Proof. - intros. apply stuck_ok. red; intros. - exploit imm_safe_t_inv; eauto. destruct a; auto. -Qed. + intros. apply stuck_ok. red; intros. + exploit imm_safe_t_inv; eauto. destruct a; auto. +Qed. Lemma incontext_ok: forall k a m C res k' a', @@ -1272,7 +1272,7 @@ Lemma incontext2_list_ok: reducts_ok RV a1 m res1 -> list_reducts_ok a2 m res2 -> is_val a1 = None \/ is_val_list a2 = None -> - reducts_ok RV (Ecall a1 a2 ty) m + reducts_ok RV (Ecall a1 a2 ty) m (incontext2 (fun x => Ecall x a2 ty) res1 (fun x => Ecall a1 x ty) res2). Proof. @@ -1280,7 +1280,7 @@ Proof. destruct (in_app_or _ _ _ H4). exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. exploit H; eauto. intros [a'' [k'' [U [V W]]]]. - exists a''; exists k''. split. eauto. rewrite V; auto. + exists a''; exists k''. split. eauto. rewrite V; auto. exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. exploit H0; eauto. intros [a'' [k'' [U [V W]]]]. exists a''; exists k''. split. eauto. rewrite V; auto. @@ -1301,7 +1301,7 @@ Proof. destruct (in_app_or _ _ _ H3). exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. exploit H; eauto. intros [a'' [k'' [U [V W]]]]. - exists a''; exists k''. split. eauto. rewrite V; auto. + exists a''; exists k''. split. eauto. rewrite V; auto. exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. exploit H0; eauto. intros [a'' [k'' [U [V W]]]]. exists a''; exists k''. split. eauto. rewrite V; auto. @@ -1312,7 +1312,7 @@ Qed. Lemma is_val_list_all_values: forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al. Proof. - induction al; simpl; intros. auto. + induction al; simpl; intros. auto. destruct (is_val r1) as [[v ty]|] eqn:?; try discriminate. destruct (is_val_list al) as [vtl'|] eqn:?; try discriminate. rewrite (is_val_inv _ _ _ Heqo). eauto. @@ -1344,7 +1344,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). destruct v... - destruct ty'... + destruct ty'... (* top struct *) destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... destruct (field_offset ge f (co_members co)) as [delta|] eqn:?... @@ -1353,7 +1353,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... apply topred_ok; auto. eapply red_field_union; eauto. (* in depth *) - eapply incontext_ok; eauto. + eapply incontext_ok; eauto. (* Evalof *) destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). (* top *) @@ -1367,7 +1367,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* Ederef *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct v... apply topred_ok; auto. apply red_deref; auto. + destruct v... apply topred_ok; auto. apply red_deref; auto. (* depth *) eapply incontext_ok; eauto. (* Eaddrof *) @@ -1377,31 +1377,31 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* depth *) eapply incontext_ok; eauto. (* unop *) - destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?... - apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. + apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* binop *) - destruct (is_val a1) as [[v1 ty1] | ] eqn:?. + destruct (is_val a1) as [[v1 ty1] | ] eqn:?. destruct (is_val a2) as [[v2 ty2] | ] eqn:?. - rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). + rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?... apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor. (* depth *) - eapply incontext2_ok; eauto. - eapply incontext2_ok; eauto. + eapply incontext2_ok; eauto. + eapply incontext2_ok; eauto. (* cast *) - destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (sem_cast v ty' ty) as [v'|] eqn:?... - apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. + apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* seqand *) - destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. @@ -1409,7 +1409,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* depth *) eapply incontext_ok; eauto. (* seqor *) - destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. @@ -1417,7 +1417,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* depth *) eapply incontext_ok; eauto. (* condition *) - destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (bool_val v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. @@ -1428,8 +1428,8 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* alignof *) apply topred_ok; auto. split. apply red_alignof. exists w; constructor. (* assign *) - destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. - destruct (is_val a2) as [[v2 ty2] | ] eqn:?. + destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. + destruct (is_val a2) as [[v2 ty2] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) destruct (type_eq ty1 ty)... subst ty1. @@ -1442,9 +1442,9 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; eapply incontext2_ok; eauto. eapply incontext2_ok; eauto. (* assignop *) - destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. - destruct (is_val a2) as [[v2 ty2] | ] eqn:?. - rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). + destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?. + destruct (is_val a2) as [[v2 ty2] | ] eqn:?. + rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) destruct (type_eq ty1 ty)... subst ty1. destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?. @@ -1455,7 +1455,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; eapply incontext2_ok; eauto. eapply incontext2_ok; eauto. (* postincr *) - destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). + destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo). (* top *) destruct (type_eq ty' ty)... subst ty'. destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?. @@ -1465,22 +1465,22 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* depth *) eapply incontext_ok; eauto. (* comma *) - destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (type_eq (typeof a2) ty)... subst ty. apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. (* call *) - destruct (is_val a) as [[vf tyf] | ] eqn:?. - destruct (is_val_list rargs) as [vtl | ] eqn:?. + destruct (is_val a) as [[vf tyf] | ] eqn:?. + destruct (is_val_list rargs) as [vtl | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL. (* top *) destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?... destruct (Genv.find_funct ge vf) as [fd|] eqn:?... - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... - apply topred_ok; auto. red. split; auto. eapply red_call; eauto. + apply topred_ok; auto. red. split; auto. eapply red_call; eauto. eapply sem_cast_arguments_sound; eauto. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. @@ -1491,31 +1491,31 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; eapply incontext2_list_ok; eauto. eapply incontext2_list_ok; eauto. (* builtin *) - destruct (is_val_list rargs) as [vtl | ] eqn:?. + destruct (is_val_list rargs) as [vtl | ] eqn:?. exploit is_val_list_all_values; eauto. intros ALLVAL. (* top *) - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?... exploit do_ef_external_sound; eauto. intros [EC PT]. - apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. + apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. eapply sem_cast_arguments_sound; eauto. exists w0; auto. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. - assert (x = vargs). + assert (x = vargs). exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence. subst x. exploit do_ef_external_complete; eauto. congruence. - apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence. (* depth *) eapply incontext_list_ok; eauto. - + (* loc *) split; intros. tauto. simpl; congruence. (* paren *) - destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). + destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) destruct (sem_cast v ty' tycast) as [v'|] eqn:?... - apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. + apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1529,7 +1529,7 @@ Qed. Lemma step_exprlist_val_list: forall m al, is_val_list al <> None -> step_exprlist al m = nil. Proof. - induction al; simpl; intros. + induction al; simpl; intros. auto. destruct (is_val r1) as [[v1 ty1]|] eqn:?; try congruence. destruct (is_val_list al) eqn:?; try congruence. @@ -1549,7 +1549,7 @@ Proof. rewrite H. rewrite dec_eq_true. econstructor; eauto. (* var global *) rewrite H; rewrite H0. econstructor; eauto. -(* deref *) +(* deref *) econstructor; eauto. (* field struct *) rewrite H, H0; econstructor; eauto. @@ -1564,7 +1564,7 @@ Lemma rred_topred: Proof. induction 1; simpl; intros. (* valof *) - rewrite dec_eq_true. + rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto. (* addrof *) inv H. econstructor; eauto. @@ -1591,7 +1591,7 @@ Proof. econstructor; eauto. (* assignop *) rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). - econstructor; eauto. + econstructor; eauto. (* postincr *) rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). econstructor; eauto. @@ -1601,7 +1601,7 @@ Proof. inv H0. rewrite H; econstructor; eauto. (* builtin *) exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. - exploit do_ef_external_complete; eauto. intros C. + exploit do_ef_external_complete; eauto. intros C. rewrite A. rewrite B. rewrite C. econstructor; eauto. Qed. @@ -1624,7 +1624,7 @@ Lemma reducts_incl_trans: reducts_incl C' res2 res3 -> reducts_incl (fun x => C'(C x)) res1 res3. Proof. - unfold reducts_incl; intros. auto. + unfold reducts_incl; intros. auto. Qed. Lemma reducts_incl_nil: @@ -1756,11 +1756,11 @@ Proof. eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto. destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* call right *) - eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. + eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto. destruct (is_val_list (C a)) as [vl|] eqn:?; eauto. (* builtin *) - eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto. + eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto. destruct (is_val_list (C a)) as [vl|] eqn:?; eauto. (* comma *) eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. @@ -1785,18 +1785,18 @@ Lemma not_stuckred_imm_safe: forall m a k, (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m. Proof. - intros. generalize (step_expr_sound a k m). intros [A B]. + intros. generalize (step_expr_sound a k m). intros [A B]. destruct (step_expr k a m) as [|[C rd] res] eqn:?. specialize (B (refl_equal _)). destruct k. destruct a; simpl in B; try congruence. constructor. destruct a; simpl in B; try congruence. constructor. assert (NOTSTUCK: rd <> Stuckred). red; intros. elim (H C); subst rd; auto with coqlib. - exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]]. + exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]]. destruct k'; destruct rd; simpl in R; intuition. subst a. eapply imm_safe_t_lred; eauto. - subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto. - subst. eapply imm_safe_t_callred; eauto. + subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto. + subst. eapply imm_safe_t_callred; eauto. Qed. Lemma not_imm_safe_stuck_red: @@ -1805,14 +1805,14 @@ Lemma not_imm_safe_stuck_red: ~imm_safe_t k a m -> exists C', In (C', Stuckred) (step_expr RV (C a) m). Proof. - intros. + intros. assert (exists C', In (C', Stuckred) (step_expr k a m)). destruct (classic (exists C', In (C', Stuckred) (step_expr k a m))); auto. - elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto. + elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto. destruct H1 as [C' IN]. - specialize (step_expr_context _ _ _ H a m). unfold reducts_incl. + specialize (step_expr_context _ _ _ H a m). unfold reducts_incl. intro. - exists (fun x => (C (C' x))). apply H1; auto. + exists (fun x => (C (C' x))). apply H1; auto. Qed. (** Connections between [imm_safe_t] and [imm_safe] *) @@ -1824,12 +1824,12 @@ Lemma imm_safe_imm_safe_t: exists C, exists a1, exists t, exists a1', exists m', context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'. Proof. - intros. inv H. + intros. inv H. left. apply imm_safe_t_val. left. apply imm_safe_t_loc. left. eapply imm_safe_t_lred; eauto. destruct (classic (exists w', possible_trace w t w')) as [[w' A] | A]. - left. eapply imm_safe_t_rred; eauto. + left. eapply imm_safe_t_rred; eauto. right. exists C; exists e0; exists t; exists e'; exists m'; intuition. apply A; exists w'; auto. left. eapply imm_safe_t_callred; eauto. Qed. @@ -1847,10 +1847,10 @@ Theorem not_imm_safe_t: Csem.step ge (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m). Proof. intros. destruct (classic (imm_safe ge e K a m)). - exploit imm_safe_imm_safe_t; eauto. + exploit imm_safe_imm_safe_t; eauto. intros [A | [C1 [a1 [t [a1' [m' [A [B [D E]]]]]]]]]. contradiction. - right. red. exists t; econstructor; split; auto. - left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto. + right. red. exists t; econstructor; split; auto. + left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto. left. left. eapply step_stuck; eauto. Qed. @@ -1862,14 +1862,14 @@ Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l match l with | nil => (e,m) | (id, ty) :: l' => - let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in + let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in do_alloc_variables (PTree.set id (b1, ty) e) m1 l' end. Lemma do_alloc_variables_sound: forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). Proof. - induction l; intros; simpl. + induction l; intros; simpl. constructor. destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl. econstructor; eauto. @@ -1879,12 +1879,12 @@ Lemma do_alloc_variables_complete: forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 -> do_alloc_variables e1 m1 l = (e2, m2). Proof. - induction 1; simpl. + induction 1; simpl. auto. - rewrite H; rewrite IHalloc_variables; auto. + rewrite H; rewrite IHalloc_variables; auto. Qed. -Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val) +Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val) {struct l} : option mem := match l, lv with | nil, nil => Some m @@ -1900,7 +1900,7 @@ Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type end. Lemma sem_bind_parameters_sound : forall w e m l lv m', - sem_bind_parameters w e m l lv = Some m' -> + sem_bind_parameters w e m l lv = Some m' -> bind_parameters ge e m l lv m'. Proof. intros; functional induction (sem_bind_parameters w e m l lv); try discriminate. @@ -1916,7 +1916,7 @@ Proof. rewrite H. rewrite dec_eq_true. assert (possible_trace w E0 w) by constructor. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H2). - simpl. auto. + simpl. auto. Qed. Inductive transition : Type := TR (rule: string) (t: trace) (S': state). @@ -1946,7 +1946,7 @@ Definition do_step (w: world) (s: state) : list transition := do b <- bool_val v ty m; ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => - do b <- bool_val v ty m; + do b <- bool_val v ty m; if b then ret "step_while_true" (State f s (Kwhile2 x s k) e m) else ret "step_while_false" (State f Sskip k e m) @@ -2018,7 +2018,7 @@ Definition do_step (w: world) (s: state) : list transition := ret "step_return_0" (Returnstate Vundef (call_cont k) m') | State f (Sreturn (Some x)) k e m => ret "step_return_1" (ExprState f x (Kreturn k) e m) - | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => + | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => do m' <- Mem.free_list m (blocks_of_env ge e); ret "step_skip_call" (Returnstate Vundef k m') @@ -2057,10 +2057,10 @@ Definition do_step (w: world) (s: state) : list transition := Ltac myinv := match goal with | [ |- In _ nil -> _ ] => intro X; elim X - | [ |- In _ (ret _ _) -> _ ] => + | [ |- In _ (ret _ _) -> _ ] => intro X; elim X; clear X; [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] - | [ |- In _ (_ :: nil) -> _ ] => + | [ |- In _ (_ :: nil) -> _ ] => intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv @@ -2096,7 +2096,7 @@ Proof with try (left; right; econstructor; eauto; fail). generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q]. exploit P; eauto. intros [a' [k' [CTX [EQ RD]]]]. unfold expr_final_state in A. simpl in A. - destruct k'; destruct rd; inv A; simpl in RD; try contradiction. + destruct k'; destruct rd; inv A; simpl in RD; try contradiction. (* lred *) left; left; apply step_lred; auto. (* stuck lred *) @@ -2111,11 +2111,11 @@ Proof with try (left; right; econstructor; eauto; fail). destruct fd; myinv. (* internal *) destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1] eqn:?. - myinv. left; right; apply step_internal_function with m1. auto. - change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. + myinv. left; right; apply step_internal_function with m1. auto. + change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto. (* external *) - destruct p as [[[w' tr] v] m']. myinv. left; right; constructor. + destruct p as [[[w' tr] v] m']. myinv. left; right; constructor. eapply do_ef_external_sound; eauto. (* returnstate *) destruct k; myinv... @@ -2126,10 +2126,10 @@ Qed. Remark estep_not_val: forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None. Proof. - intros. + intros. assert (forall b from to C, context from to C -> (from = to /\ C = fun x => x) \/ is_val (C b) = None). - induction 1; simpl; auto. - inv H. + induction 1; simpl; auto. + inv H. destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto. @@ -2141,7 +2141,7 @@ Theorem do_step_complete: possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S). Proof with (unfold ret; eauto with coqlib). intros until w'; intros PT H. - destruct H. + destruct H. (* Expression step *) inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL. (* lred *) @@ -2170,7 +2170,7 @@ Proof with (unfold ret; eauto with coqlib). change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. - intro. replace C with (fun x => C x). apply H2. + intro. replace C with (fun x => C x). apply H2. rewrite STEP; unfold topred; auto with coqlib. apply extensionality; auto. (* stuck *) @@ -2179,7 +2179,7 @@ Proof with (unfold ret; eauto with coqlib). simpl do_step. rewrite NOTVAL. exists "step_stuck". change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)). - apply in_map. auto. + apply in_map. auto. (* Statement step *) inv H; simpl; econstructor... -- cgit