From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 35 +++---- cfrontend/Cexec.v | 181 ++++++++++++++++++------------------ cfrontend/Cminorgenproof.v | 51 +++++----- cfrontend/Cshmgenproof.v | 10 +- cfrontend/Cstrategy.v | 30 +++--- cfrontend/Initializersproof.v | 68 ++++++++------ cfrontend/PrintClight.ml | 3 +- cfrontend/PrintCsyntax.ml | 2 +- cfrontend/SimplExpr.v | 134 +++++++++++++------------- cfrontend/SimplExprproof.v | 112 +++++++++++----------- cfrontend/SimplExprspec.v | 212 +++++++++++++++++++++--------------------- cfrontend/SimplLocalsproof.v | 52 +++++------ 12 files changed, 454 insertions(+), 436 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d425693..3830ca7 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -125,16 +125,12 @@ let name_for_string_literal env s = id let typeStringLiteral s = - Tarray(Tint(I8, Unsigned, noattr), - z_of_camlint(Int32.of_int(String.length s + 1)), - noattr) + Tarray(Tint(I8, Unsigned, noattr), Z.of_uint (String.length s + 1), noattr) let global_for_string s id = let init = ref [] in let add_char c = - init := - AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))) - :: !init in + init := AST.Init_int8(Z.of_uint(Char.code c)) :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; @@ -344,8 +340,8 @@ let supported_return_type env ty = (** Floating point constants *) let z_of_str hex str fst = - let res = ref BinInt.Z0 in - let base = if hex then 16l else 10l in + let res = ref Z.Z0 in + let base = if hex then 16 else 10 in for i = fst to String.length str - 1 do let d = int_of_char str.[i] in let d = @@ -356,27 +352,25 @@ let z_of_str hex str fst = else d - int_of_char '0' in - let d = Int32.of_int d in - assert (d >= 0l && d < base); - res := BinInt.coq_Zplus - (BinInt.coq_Zmult (z_of_camlint base) !res) (z_of_camlint d) + assert (d >= 0 && d < base); + res := Z.add (Z.mul (Z.of_uint base) !res) (Z.of_uint d) done; !res let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in match mant with - | BinInt.Z0 -> Float.zero - | BinInt.Zpos mant -> + | Z.Z0 -> Float.zero + | Z.Zpos mant -> let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in let exp = z_of_str false f.C.exp (if sgExp then 1 else 0) in - let exp = if f.C.exp.[0] = '-' then BinInt.coq_Zopp exp else exp in + let exp = if f.C.exp.[0] = '-' then Z.neg exp else exp in let shift_exp = - Int32.of_int ((if f.C.hex then 4 else 1) * String.length f.C.fracPart) in - let exp = BinInt.coq_Zminus exp (z_of_camlint shift_exp) in + (if f.C.hex then 4 else 1) * String.length f.C.fracPart in + let exp = Z.sub exp (Z.of_uint shift_exp) in - let base = positive_of_camlint (if f.C.hex then 16l else 10l) in + let base = P.of_int (if f.C.hex then 16 else 10) in begin match kind with | FFloat -> @@ -384,7 +378,8 @@ let convertFloat f kind = | FDouble | FLongDouble -> Float.build_from_parsed64 base mant exp end - | BinInt.Zneg _ -> assert false + + | Z.Zneg _ -> assert false (** Expressions *) @@ -752,7 +747,7 @@ let string_of_errmsg msg = let string_of_err = function | Errors.MSG s -> camlstring_of_coqstring s | Errors.CTX i -> extern_atom i - | Errors.POS i -> sprintf "%ld" (camlint_of_positive i) + | Errors.POS i -> Z.to_string (Z.Zpos i) in String.concat "" (List.map string_of_err msg) let rec convertInit env init = diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index c370c60..ded6b72 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -132,7 +132,7 @@ Proof. intros. destruct v; destruct t; simpl in H; inv H. constructor. constructor. - destruct (Genv.invert_symbol ge b) as [id|]_eqn; inv H1. + destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. constructor. apply Genv.invert_find_symbol; auto. Qed. @@ -148,8 +148,8 @@ Lemma list_eventval_of_val_sound: Proof with try discriminate. induction vl; destruct tl; simpl; intros; inv H. constructor. - destruct (eventval_of_val a t) as [ev1|]_eqn... - destruct (list_eventval_of_val vl tl) as [evl'|]_eqn... + destruct (eventval_of_val a t) as [ev1|] eqn:?... + destruct (list_eventval_of_val vl tl) as [evl'|] eqn:?... inv H1. constructor. apply eventval_of_val_sound; auto. eauto. Qed. @@ -166,7 +166,7 @@ Proof. intros. destruct ev; destruct t; simpl in H; inv H. constructor. constructor. - destruct (Genv.find_symbol ge i) as [b|]_eqn; inv H1. + destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. constructor. auto. Qed. @@ -207,8 +207,8 @@ Ltac mydestr := match goal with | [ |- None = Some _ -> _ ] => intro X; discriminate | [ |- Some _ = Some _ -> _ ] => intro X; inv X - | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr - | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr + | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr + | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr | _ => idtac end. @@ -331,7 +331,7 @@ 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) as []_eqn; mydestr. + 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. @@ -356,7 +356,7 @@ 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) as []_eqn; mydestr. + 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]]. @@ -558,7 +558,7 @@ Proof with try congruence. intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... - destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr. + 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... @@ -1170,7 +1170,7 @@ Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop Ltac monadInv := match goal with | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] => - destruct x as []_eqn; [monadInv|discriminate] + destruct x eqn:?; [monadInv|discriminate] | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] => destruct x; [monadInv|discriminate] | _ => idtac @@ -1338,8 +1338,8 @@ 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. - destruct (is_val r1) as [[v ty]|]_eqn; try discriminate. - destruct (is_val_list al) as [vtl'|]_eqn; try discriminate. + 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. Qed. @@ -1360,91 +1360,91 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* Eval *) split; intros. tauto. simpl; congruence. (* Evar *) - destruct (e!x) as [[b ty']|]_eqn. + destruct (e!x) as [[b ty']|] eqn:?. destruct (type_eq ty ty')... subst. apply topred_ok; auto. apply red_var_local; auto. - destruct (Genv.find_symbol ge x) as [b|]_eqn... - destruct (type_of_global ge b) as [ty'|]_eqn... + destruct (Genv.find_symbol ge x) as [b|] eqn:?... + destruct (type_of_global ge b) as [ty'|] eqn:?... destruct (type_eq ty ty')... subst. apply topred_ok; auto. apply red_var_global; auto. (* Efield *) - destruct (is_val a) as [[v ty'] | ]_eqn. + destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). destruct v... destruct ty'... (* top struct *) - destruct (field_offset f f0) as [delta|]_eqn... + destruct (field_offset f f0) as [delta|] eqn:?... apply topred_ok; auto. apply red_field_struct; auto. (* top union *) apply topred_ok; auto. apply red_field_union; auto. (* in depth *) eapply incontext_ok; eauto. (* Evalof *) - 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. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?. exploit do_deref_loc_sound; eauto. intros [A B]. apply topred_ok; auto. red. split. apply red_rvalof; auto. exists w'; auto. apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence. (* depth *) eapply incontext_ok; eauto. (* Ederef *) - 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 v... apply topred_ok; auto. apply red_deref; auto. (* depth *) eapply incontext_ok; eauto. (* Eaddrof *) - 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 *) apply topred_ok; auto. split. apply red_addrof; auto. exists w; constructor. (* 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') as [v'|]_eqn... + destruct (sem_unary_operation op v ty') as [v'|] eqn:?... 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 a2) as [[v2 ty2] | ]_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). (* top *) - destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|]_eqn... + destruct (sem_binary_operation 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. (* 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... + destruct (sem_cast v ty' ty) as [v'|] eqn:?... 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') as [v'|]_eqn... destruct v'. + destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor. (* 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') as [v'|]_eqn... destruct v'. + destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor. (* 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') as [v'|]_eqn... + destruct (bool_val v ty') as [v'|] eqn:?... apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1453,13 +1453,13 @@ 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. - destruct (sem_cast v2 ty2 ty) as [v|]_eqn... - destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|]_eqn. + destruct (sem_cast v2 ty2 ty) as [v|] eqn:?... + destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?. exploit do_assign_loc_sound; eauto. intros [P Q]. apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto. apply not_invert_ok; simpl; intros; myinv. exploit do_assign_loc_complete; eauto. congruence. @@ -1467,12 +1467,12 @@ 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. + 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. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?. exploit do_deref_loc_sound; eauto. intros [A B]. apply topred_ok; auto. red. split. apply red_assignop; auto. exists w'; auto. apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence. @@ -1480,30 +1480,30 @@ 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. + destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?. exploit do_deref_loc_sound; eauto. intros [A B]. apply topred_ok; auto. red. split. apply red_postincr; auto. exists w'; auto. apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. 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|]_eqn... - destruct (Genv.find_funct ge vf) as [fd|]_eqn... - destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... + destruct (classify_fun tyf) as [tyargs tyres|] eqn:?... + destruct (Genv.find_funct ge vf) as [fd|] eqn:?... + destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))... apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. eapply sem_cast_arguments_sound; eauto. @@ -1516,11 +1516,11 @@ 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 (do_external ef w vargs m) as [[[[? ?] v] m'] | ]_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. eapply sem_cast_arguments_sound; eauto. @@ -1537,9 +1537,9 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* 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' ty) as [v'|]_eqn... + destruct (sem_cast v ty' ty) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1556,8 +1556,8 @@ Lemma step_exprlist_val_list: Proof. induction al; simpl; intros. auto. - destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence. - destruct (is_val_list al) as []_eqn; try congruence. + destruct (is_val r1) as [[v1 ty1]|] eqn:?; try congruence. + destruct (is_val_list al) eqn:?; try congruence. rewrite (is_val_inv _ _ _ Heqo). rewrite IHal. auto. congruence. Qed. @@ -1717,75 +1717,78 @@ with step_exprlist_context: Proof. induction 1; simpl; intros. (* top *) - red. destruct (step_expr k a m); auto. intros. - replace (fun x => C1 x) with C1; auto. apply extensionality; auto. + red. destruct (step_expr k a m); auto. + try (* no eta in 8.3 *) + (intros; + replace (fun x => C1 x) with C1 by (apply extensionality; auto); + auto). (* deref *) eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* field *) eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* valof *) eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto. (* addrof *) eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto. (* unop *) eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* binop left *) eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* binop right *) eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto. - destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. + destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto. + destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto. (* cast *) eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* seqand *) eapply reducts_incl_trans with (C' := fun x => Eseqand x r2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* seqor *) eapply reducts_incl_trans with (C' := fun x => Eseqor x r2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* condition *) eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* assign left *) eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto. (* assign right *) eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto. - destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto. + destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto. (* assignop left *) eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto. (* assignop right *) eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto. - destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. - destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto. + destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto. (* postincr *) eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto. - destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto. (* call left *) eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; 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. - destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. - destruct (is_val_list (C a)) as [vl|]_eqn; eauto. + 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. - destruct (is_val_list (C a)) as [vl|]_eqn; eauto. + destruct (is_val_list (C a)) as [vl|] eqn:?; eauto. (* comma *) eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* paren *) eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto. - destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. induction 1; simpl; intros. (* cons left *) @@ -1804,7 +1807,7 @@ Lemma not_stuckred_imm_safe: (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]. - destruct (step_expr k a m) as [|[C rd] res]_eqn. + 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. @@ -1889,7 +1892,7 @@ Lemma do_alloc_variables_sound: Proof. induction l; intros; simpl. constructor. - destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1]_eqn; simpl. + destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1] eqn:?; simpl. econstructor; eauto. Qed. @@ -2053,8 +2056,8 @@ Ltac myinv := [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] - | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x as []_eqn; myinv - | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x as []_eqn; myinv + | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv + | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv | _ => idtac end. @@ -2078,7 +2081,7 @@ Proof with try (left; right; econstructor; eauto; fail). (* goto *) destruct p as [s' k']. myinv... (* ExprState *) - destruct (is_val r) as [[v ty]|]_eqn. + destruct (is_val r) as [[v ty]|] eqn:?. (* expression is a value *) rewrite (is_val_inv _ _ _ Heqo). destruct k; myinv... @@ -2102,7 +2105,7 @@ Proof with try (left; right; econstructor; eauto; fail). (* callstate *) destruct fd; myinv. (* internal *) - destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn. + 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. apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 62690d6..cff5b06 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -398,11 +398,11 @@ Proof. else false end end). - destruct (List.existsb pred (PTree.elements e)) as []_eqn. + destruct (List.existsb pred (PTree.elements e)) eqn:?. (* yes *) rewrite List.existsb_exists in Heqb. destruct Heqb as [[id [b sz]] [A B]]. - simpl in B. destruct (f b) as [[sp' delta] |]_eqn; try discriminate. + simpl in B. destruct (f b) as [[sp' delta] |] eqn:?; try discriminate. destruct (eq_block sp sp'); try discriminate. destruct (andb_prop _ _ B). left. apply is_reachable_intro with id b sz delta. @@ -646,13 +646,13 @@ Proof. constructor. auto. auto. eapply match_temps_invariant; eauto. eapply match_env_invariant; eauto. - red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|]_eqn. + red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?. exploit INCR; eauto. congruence. exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. intros. assert (lo <= hi) by (eapply me_low_high; eauto). - destruct (f1 b) as [[b' delta']|]_eqn. + destruct (f1 b) as [[b' delta']|] eqn:?. apply INCR; auto. - destruct (f2 b) as [[b' delta']|]_eqn; auto. + destruct (f2 b) as [[b' delta']|] eqn:?; auto. exploit SEPARATED; eauto. intros [A B]. elim A. red. omega. eapply match_bounds_invariant; eauto. intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. omega. @@ -884,7 +884,7 @@ Proof. intros. destruct (In_dec peq id (map fst vars)). apply cenv_remove_gss; auto. rewrite cenv_remove_gso; auto. - destruct (cenv!id) as [ofs|]_eqn; auto. elim n; eauto. + destruct (cenv!id) as [ofs|] eqn:?; auto. elim n; eauto. eapply Mem.alloc_right_inject; eauto. Qed. @@ -917,7 +917,7 @@ Proof. simpl; intros. inv H. omega. Opaque assign_variable. destruct a as [id s]. simpl. intros. - destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1]_eqn. + destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. Transparent assign_variable. Qed. @@ -1014,7 +1014,7 @@ Proof. destruct a as [id sz]. simpl in H0. inv H0. rewrite in_app in H6. rewrite list_norepet_app in H7. destruct H7 as [P [Q R]]. - destruct (assign_variable (cenv1, sz1) (id, sz)) as [cenv' sz']_eqn. + destruct (assign_variable (cenv1, sz1) (id, sz)) as [cenv' sz'] eqn:?. exploit assign_variable_sound. eauto. instantiate (1 := vars). tauto. @@ -1377,12 +1377,12 @@ Proof. intros. apply (val_match_approx_increasing Int1 a v); auto. intros; unfold Approx.bitwise_and. - destruct (Approx.bge Int1 a1) as []_eqn. simpl. apply Y; eauto. compute; auto. - destruct (Approx.bge Int1 a2) as []_eqn. simpl. apply X; eauto. compute; auto. - destruct (Approx.bge Int8u a1) as []_eqn. simpl. apply Y; eauto. compute; auto. - destruct (Approx.bge Int8u a2) as []_eqn. simpl. apply X; eauto. compute; auto. - destruct (Approx.bge Int16u a1) as []_eqn. simpl. apply Y; eauto. compute; auto. - destruct (Approx.bge Int16u a2) as []_eqn. simpl. apply X; eauto. compute; auto. + destruct (Approx.bge Int1 a1) eqn:?. simpl. apply Y; eauto. compute; auto. + destruct (Approx.bge Int1 a2) eqn:?. simpl. apply X; eauto. compute; auto. + destruct (Approx.bge Int8u a1) eqn:?. simpl. apply Y; eauto. compute; auto. + destruct (Approx.bge Int8u a2) eqn:?. simpl. apply X; eauto. compute; auto. + destruct (Approx.bge Int16u a1) eqn:?. simpl. apply Y; eauto. compute; auto. + destruct (Approx.bge Int16u a2) eqn:?. simpl. apply X; eauto. compute; auto. simpl; auto. Qed. @@ -1404,19 +1404,19 @@ Proof. unfold Approx.bitwise_or. - destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) as []_eqn. + destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) eqn:?. destruct (andb_prop _ _ Heqb). simpl. apply X. compute; auto. apply (val_match_approx_increasing Int1 a1 v1); auto. apply (val_match_approx_increasing Int1 a2 v2); auto. - destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) as []_eqn. + destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) eqn:?. destruct (andb_prop _ _ Heqb0). simpl. apply X. compute; auto. apply (val_match_approx_increasing Int8u a1 v1); auto. apply (val_match_approx_increasing Int8u a2 v2); auto. - destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) as []_eqn. + destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) eqn:?. destruct (andb_prop _ _ Heqb1). simpl. apply X. compute; auto. apply (val_match_approx_increasing Int16u a1 v1); auto. @@ -1574,8 +1574,8 @@ Proof. apply val_inject_val_of_optbool. Opaque Int.add. unfold Val.cmpu. simpl. - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; simpl; auto. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; simpl; auto. + destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto. + destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto. exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. intros V1. rewrite V1. exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. @@ -1859,13 +1859,20 @@ Proof. (forall b ofs, Mem.store chunk m1 b ofs v1 = Mem.store chunk m1 b ofs v1') -> Mem.storev chunk m1 a1 v1' = Some n1). intros. rewrite <- H0. destruct a1; simpl; auto. - inv H2; (eapply Mem.storev_mapped_inject; [eauto|idtac|eauto|eauto]); - auto; apply H3; intros. + inv H2; eapply Mem.storev_mapped_inject; + try eapply H; try eapply H1; try apply H3; intros. rewrite <- Mem.store_int8_sign_ext. rewrite H4. apply Mem.store_int8_sign_ext. + auto. rewrite <- Mem.store_int8_zero_ext. rewrite H4. apply Mem.store_int8_zero_ext. + auto. rewrite <- Mem.store_int16_sign_ext. rewrite H4. apply Mem.store_int16_sign_ext. + auto. rewrite <- Mem.store_int16_zero_ext. rewrite H4. apply Mem.store_int16_zero_ext. + auto. rewrite <- Mem.store_float32_truncate. rewrite H4. apply Mem.store_float32_truncate. + auto. + eauto. + auto. Qed. Lemma make_store_correct: @@ -2053,7 +2060,7 @@ Proof. (* Eunop *) exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]]. unfold Csharpminor.eval_unop in H0. - destruct (Approx.unop_is_redundant op x0) as []_eqn; inv EQ0. + destruct (Approx.unop_is_redundant op x0) eqn:?; inv EQ0. (* -- eliminated *) exploit approx_unop_is_redundant_sound; eauto. intros. replace v with v1 by congruence. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 42eae5d..74a6da5 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -732,10 +732,10 @@ Lemma block_is_volatile_preserved: forall b, block_is_volatile tge b = block_is_volatile ge b. Proof. intros. unfold block_is_volatile. - destruct (Genv.find_var_info ge b) as []_eqn. + destruct (Genv.find_var_info ge b) eqn:?. exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. unfold transf_globvar in B. monadInv B. auto. - destruct (Genv.find_var_info tge b) as []_eqn. + destruct (Genv.find_var_info tge b) eqn:?. exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence. auto. Qed. @@ -761,7 +761,7 @@ Lemma match_env_globals: e!id = None -> te!id = None. Proof. - intros. destruct (te!id) as [[b sz] | ]_eqn; auto. + intros. destruct (te!id) as [[b sz] | ] eqn:?; auto. exploit me_local_inv; eauto. intros [ty EQ]. congruence. Qed. @@ -1284,7 +1284,7 @@ Proof. destruct H0. inv MK. econstructor; split. eapply plus_left. - destruct H0; subst ts'; constructor. + destruct H0; subst ts'. 2:constructor. constructor. apply star_one. constructor. traceEq. econstructor; eauto. constructor. econstructor; eauto. @@ -1355,7 +1355,7 @@ Proof. destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. econstructor; split. - apply plus_one. destruct H0; subst ts'; constructor. + apply plus_one. destruct H0; subst ts'. 2:constructor. constructor. eapply match_states_skip; eauto. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index b28409d..7988dfa 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -816,7 +816,7 @@ Ltac StepR REC C' a := (* field *) StepR IHa (fun x => C(Efield x f0 ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. - intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) as []_eqn; try contradiction. + intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction. destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. exists b; exists ofs; econstructor; eauto. (* valof *) @@ -1075,7 +1075,7 @@ Ltac Base := Kind. Rec H RV C (fun x => Efield x f0 ty). (* rvalof *) Kind. Rec H LV C (fun x => Evalof x ty). - destruct (type_is_volatile (typeof l)) as []_eqn. + destruct (type_is_volatile (typeof l)) eqn:?. Base. rewrite H2; auto. (* deref *) Kind. Rec H RV C (fun x => Ederef x ty). @@ -1198,7 +1198,7 @@ Proof. eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto. eapply plus_left. left; apply step_rred; auto. econstructor; eauto. - destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|]_eqn. + destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?. eapply star_left. left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. apply star_one. @@ -1326,8 +1326,8 @@ Proof. exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto. intros [v [E2 S2]]. exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]]. - destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|]_eqn. - destruct (sem_cast v3 tyres (typeof b1)) as [v4|]_eqn. + destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?. + destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). destruct H2 as [t2 [m' D]]. econstructor; econstructor; eapply step_assignop; eauto. @@ -1341,8 +1341,8 @@ Proof. exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. intros [b1 [ofs [E1 S1]]]. exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]]. - destruct (sem_incrdecr id v1 ty) as [v2|]_eqn. - destruct (sem_cast v2 (typeconv ty) ty) as [v3|]_eqn. + destruct (sem_incrdecr id v1 ty) as [v2|] eqn:?. + destruct (sem_cast v2 (typeconv ty) ty) as [v3|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')). destruct H0 as [t2 [m' D]]. econstructor; econstructor; eapply step_postincr; eauto. @@ -1493,8 +1493,8 @@ Proof. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. - destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn. + destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1506,8 +1506,8 @@ Proof. rewrite Heqo; auto. (* assignop stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn. + destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1522,8 +1522,8 @@ Proof. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. - destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn. - destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn. + destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?. + destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. @@ -1535,8 +1535,8 @@ Proof. rewrite Heqo; auto. (* postincr stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn. - destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn. + destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?. + destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 9bc1dd7..ca9c5b0 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -12,7 +12,6 @@ (** Compile-time evaluation of initializers for global C variables. *) -Require Import Coq.Program.Equality. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -268,42 +267,58 @@ Proof. induction 2; simpl; try tauto. Qed. +Lemma compat_eval_steps_aux f r e m r' m' s2 : + simple r -> + star step ge s2 nil (ExprState f r' Kstop e m') -> + estep ge (ExprState f r Kstop e m) nil s2 -> + exists r1, + s2 = ExprState f r1 Kstop e m /\ + compat_eval RV e r r1 m /\ simple r1. +Proof. + intros. + inv H1. + (* lred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit lred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply lred_simple; eauto. + (* rred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit rred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply rred_simple; eauto. + (* callred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + inv H8; simpl in S; contradiction. + (* stuckred *) + inv H0. destruct H1; inv H0. +Qed. + Lemma compat_eval_steps: forall f r e m r' m', star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') -> simple r -> m' = m /\ compat_eval RV e r r' m. Proof. - intros. dependent induction H. + intros. + remember (ExprState f r Kstop e m) as S1. + remember E0 as t. + remember (ExprState f r' Kstop e m') as S2. + revert S1 t S2 H r m r' m' HeqS1 Heqt HeqS2 H0. + induction 1; intros; subst. (* base case *) - split. auto. red; auto. + inv HeqS2. split. auto. red; auto. (* inductive case *) destruct (app_eq_nil t1 t2); auto. subst. inv H. (* expression step *) - assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1). - inv H3. - (* lred *) - assert (S: simple a) by (eapply simple_context_1; eauto). - exploit lred_compat; eauto. intros [A B]. subst m'0. - econstructor; split. eauto. split. - eapply compat_eval_context; eauto. - eapply simple_context_2; eauto. eapply lred_simple; eauto. - (* rred *) - assert (S: simple a) by (eapply simple_context_1; eauto). - exploit rred_compat; eauto. intros [A B]. subst m'0. - econstructor; split. eauto. split. - eapply compat_eval_context; eauto. - eapply simple_context_2; eauto. eapply rred_simple; eauto. - (* callred *) - assert (S: simple a) by (eapply simple_context_1; eauto). - inv H9; simpl in S; contradiction. - (* stuckred *) - inv H2. destruct H; inv H. - destruct X as [r1 [A [B C]]]. subst s2. - exploit IHstar; eauto. intros [D E]. + exploit compat_eval_steps_aux; eauto. + intros [r1 [A [B C]]]. subst s2. + exploit IHstar; eauto. intros [D E]. split. auto. destruct B; destruct E. split. congruence. auto. (* statement steps *) - inv H3. + inv H1. Qed. Theorem eval_simple_steps: @@ -438,7 +453,7 @@ Lemma sem_cast_match: forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> match_val v2' v2. Proof. - intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] _eqn; inv H1. + intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:?; inv H1. unfold sem_cast in H; functional inversion Heqo; subst. rewrite H2 in H. inv H0. inv H. constructor. rewrite H2 in H. inv H0. inv H. constructor; auto. @@ -888,3 +903,4 @@ Qed. End SOUNDNESS. + diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 0e8b494..b05876a 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -40,8 +40,7 @@ let register_struct_union id fld = (* Naming temporaries *) -let temp_name (id: ident) = - Printf.sprintf "$%ld" (camlint_of_positive id) +let temp_name (id: ident) = Z.to_string (Z.Zpos id) (* Declarator (identifier + type) -- reuse from PrintCsyntax *) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 7858545..67efd1b 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -396,7 +396,7 @@ let string_of_init id = let chop_last_nul id = match List.rev id with - | Init_int8 BinInt.Z0 :: tl -> List.rev tl + | Init_int8 Z.Z0 :: tl -> List.rev tl | _ -> id let print_init p = function diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index ab35445..2dbd97e 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -24,8 +24,6 @@ Require Import Cop. Require Import Csyntax. Require Import Clight. -Module C := Csyntax. - Open Local Scope string_scope. (** State and error monad for generating fresh identifiers. *) @@ -208,46 +206,46 @@ Definition finish (dst: destination) (sl: list statement) (a: expr) := | For_set tyl tmp => (sl ++ do_set tmp tyl a, a) end. -Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr) := +Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with - | C.Eloc b ofs ty => - error (msg "SimplExpr.transl_expr: C.Eloc") - | C.Evar x ty => + | Csyntax.Eloc b ofs ty => + error (msg "SimplExpr.transl_expr: Eloc") + | Csyntax.Evar x ty => ret (finish dst nil (Evar x ty)) - | C.Ederef r ty => + | Csyntax.Ederef r ty => do (sl, a) <- transl_expr For_val r; ret (finish dst sl (Ederef a ty)) - | C.Efield r f ty => + | Csyntax.Efield r f ty => do (sl, a) <- transl_expr For_val r; ret (finish dst sl (Efield a f ty)) - | C.Eval (Vint n) ty => + | Csyntax.Eval (Vint n) ty => ret (finish dst nil (Econst_int n ty)) - | C.Eval (Vfloat n) ty => + | Csyntax.Eval (Vfloat n) ty => ret (finish dst nil (Econst_float n ty)) - | C.Eval _ ty => - error (msg "SimplExpr.transl_expr: val") - | C.Esizeof ty' ty => + | Csyntax.Eval _ ty => + error (msg "SimplExpr.transl_expr: Eval") + | Csyntax.Esizeof ty' ty => ret (finish dst nil (Esizeof ty' ty)) - | C.Ealignof ty' ty => + | Csyntax.Ealignof ty' ty => ret (finish dst nil (Ealignof ty' ty)) - | C.Evalof l ty => + | Csyntax.Evalof l ty => do (sl1, a1) <- transl_expr For_val l; - do (sl2, a2) <- transl_valof (C.typeof l) a1; + do (sl2, a2) <- transl_valof (Csyntax.typeof l) a1; ret (finish dst (sl1 ++ sl2) a2) - | C.Eaddrof l ty => + | Csyntax.Eaddrof l ty => do (sl, a) <- transl_expr For_val l; ret (finish dst sl (Eaddrof a ty)) - | C.Eunop op r1 ty => + | Csyntax.Eunop op r1 ty => do (sl1, a1) <- transl_expr For_val r1; ret (finish dst sl1 (Eunop op a1 ty)) - | C.Ebinop op r1 r2 ty => + | Csyntax.Ebinop op r1 r2 ty => do (sl1, a1) <- transl_expr For_val r1; do (sl2, a2) <- transl_expr For_val r2; ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty)) - | C.Ecast r1 ty => + | Csyntax.Ecast r1 ty => do (sl1, a1) <- transl_expr For_val r1; ret (finish dst sl1 (Ecast a1 ty)) - | C.Eseqand r1 r2 ty => + | Csyntax.Eseqand r1 r2 ty => do (sl1, a1) <- transl_expr For_val r1; match dst with | For_val => @@ -265,7 +263,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil, dummy_expr) end - | C.Eseqor r1 r2 ty => + | Csyntax.Eseqor r1 r2 ty => do (sl1, a1) <- transl_expr For_val r1; match dst with | For_val => @@ -283,7 +281,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil, dummy_expr) end - | C.Econdition r1 r2 r3 ty => + | Csyntax.Econdition r1 r2 r3 ty => do (sl1, a1) <- transl_expr For_val r1; match dst with | For_val => @@ -303,11 +301,11 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, dummy_expr) end - | C.Eassign l1 r2 ty => + | Csyntax.Eassign l1 r2 ty => do (sl1, a1) <- transl_expr For_val l1; do (sl2, a2) <- transl_expr For_val r2; - let ty1 := C.typeof l1 in - let ty2 := C.typeof r2 in + let ty1 := Csyntax.typeof l1 in + let ty2 := Csyntax.typeof r2 in match dst with | For_val | For_set _ _ => do t <- gensym ty2; @@ -318,8 +316,8 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil, dummy_expr) end - | C.Eassignop op l1 r2 tyres ty => - let ty1 := C.typeof l1 in + | Csyntax.Eassignop op l1 r2 tyres ty => + let ty1 := Csyntax.typeof l1 in do (sl1, a1) <- transl_expr For_val l1; do (sl2, a2) <- transl_expr For_val r2; do (sl3, a3) <- transl_valof ty1 a1; @@ -335,8 +333,8 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil, dummy_expr) end - | C.Epostincr id l1 ty => - let ty1 := C.typeof l1 in + | Csyntax.Epostincr id l1 ty => + let ty1 := Csyntax.typeof l1 in do (sl1, a1) <- transl_expr For_val l1; match dst with | For_val | For_set _ _ => @@ -350,11 +348,11 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr ret (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil, dummy_expr) end - | C.Ecomma r1 r2 ty => + | Csyntax.Ecomma r1 r2 ty => do (sl1, a1) <- transl_expr For_effects r1; do (sl2, a2) <- transl_expr dst r2; ret (sl1 ++ sl2, a2) - | C.Ecall r1 rl2 ty => + | Csyntax.Ecall r1 rl2 ty => do (sl1, a1) <- transl_expr For_val r1; do (sl2, al2) <- transl_exprlist rl2; match dst with @@ -365,7 +363,7 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr | For_effects => ret (sl1 ++ sl2 ++ Scall None a1 al2 :: nil, dummy_expr) end - | C.Ebuiltin ef tyargs rl ty => + | Csyntax.Ebuiltin ef tyargs rl ty => do (sl, al) <- transl_exprlist rl; match dst with | For_val | For_set _ _ => @@ -375,33 +373,33 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr | For_effects => ret (sl ++ Sbuiltin None ef tyargs al :: nil, dummy_expr) end - | C.Eparen r1 ty => + | Csyntax.Eparen r1 ty => error (msg "SimplExpr.transl_expr: paren") end with transl_exprlist (rl: exprlist) : mon (list statement * list expr) := match rl with - | C.Enil => + | Csyntax.Enil => ret (nil, nil) - | C.Econs r1 rl2 => + | Csyntax.Econs r1 rl2 => do (sl1, a1) <- transl_expr For_val r1; do (sl2, al2) <- transl_exprlist rl2; ret (sl1 ++ sl2, a1 :: al2) end. -Definition transl_expression (r: C.expr) : mon (statement * expr) := +Definition transl_expression (r: Csyntax.expr) : mon (statement * expr) := do (sl, a) <- transl_expr For_val r; ret (makeseq sl, a). -Definition transl_expr_stmt (r: C.expr) : mon statement := +Definition transl_expr_stmt (r: Csyntax.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 := +Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement := do (sl, a) <- transl_expr For_val r; ret (makeseq (sl ++ makeif a s1 s2 :: nil)). *) -Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement := +Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement := do (sl, a) <- transl_expr For_val r; ret (makeseq (sl ++ makeif a s1 s2 :: nil)). @@ -410,33 +408,33 @@ Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement := Definition expr_true := Econst_int Int.one type_int32s. Definition is_Sskip: - forall s, {s = C.Sskip} + {s <> C.Sskip}. + forall s, {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}. Proof. destruct s; ((left; reflexivity) || (right; congruence)). Defined. -Fixpoint transl_stmt (s: C.statement) : mon statement := +Fixpoint transl_stmt (s: Csyntax.statement) : mon statement := match s with - | C.Sskip => ret Sskip - | C.Sdo e => transl_expr_stmt e - | C.Ssequence s1 s2 => + | Csyntax.Sskip => ret Sskip + | Csyntax.Sdo e => transl_expr_stmt e + | Csyntax.Ssequence s1 s2 => do ts1 <- transl_stmt s1; do ts2 <- transl_stmt s2; ret (Ssequence ts1 ts2) - | C.Sifthenelse e s1 s2 => + | Csyntax.Sifthenelse e s1 s2 => do ts1 <- transl_stmt s1; do ts2 <- transl_stmt s2; do (s', a) <- transl_expression e; ret (Ssequence s' (Sifthenelse a ts1 ts2)) - | C.Swhile e s1 => + | Csyntax.Swhile e s1 => do s' <- transl_if e Sskip Sbreak; do ts1 <- transl_stmt s1; ret (Sloop (Ssequence s' ts1) Sskip) - | C.Sdowhile e s1 => + | Csyntax.Sdowhile e s1 => do s' <- transl_if e Sskip Sbreak; do ts1 <- transl_stmt s1; ret (Sloop ts1 s') - | C.Sfor s1 e2 s3 s4 => + | Csyntax.Sfor s1 e2 s3 s4 => do ts1 <- transl_stmt s1; do s' <- transl_if e2 Sskip Sbreak; do ts3 <- transl_stmt s3; @@ -445,32 +443,32 @@ Fixpoint transl_stmt (s: C.statement) : mon statement := ret (Sloop (Ssequence s' ts4) ts3) else ret (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3)) - | C.Sbreak => + | Csyntax.Sbreak => ret Sbreak - | C.Scontinue => + | Csyntax.Scontinue => ret Scontinue - | C.Sreturn None => + | Csyntax.Sreturn None => ret (Sreturn None) - | C.Sreturn (Some e) => + | Csyntax.Sreturn (Some e) => do (s', a) <- transl_expression e; ret (Ssequence s' (Sreturn (Some a))) - | C.Sswitch e ls => + | Csyntax.Sswitch e ls => do (s', a) <- transl_expression e; do tls <- transl_lblstmt ls; ret (Ssequence s' (Sswitch a tls)) - | C.Slabel lbl s1 => + | Csyntax.Slabel lbl s1 => do ts1 <- transl_stmt s1; ret (Slabel lbl ts1) - | C.Sgoto lbl => + | Csyntax.Sgoto lbl => ret (Sgoto lbl) end -with transl_lblstmt (ls: C.labeled_statements) : mon labeled_statements := +with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements := match ls with - | C.LSdefault s => + | Csyntax.LSdefault s => do ts <- transl_stmt s; ret (LSdefault ts) - | C.LScase n s ls1 => + | Csyntax.LScase n s ls1 => do ts <- transl_stmt s; do tls1 <- transl_lblstmt ls1; ret (LScase n ts tls1) @@ -478,30 +476,30 @@ with transl_lblstmt (ls: C.labeled_statements) : mon labeled_statements := (** Translation of a function *) -Definition transl_function (f: C.function) : res function := - match transl_stmt f.(C.fn_body) (initial_generator tt) with +Definition transl_function (f: Csyntax.function) : res function := + match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with | Err msg => Error msg | Res tbody g i => OK (mkfunction - f.(C.fn_return) - f.(C.fn_params) - f.(C.fn_vars) + f.(Csyntax.fn_return) + f.(Csyntax.fn_params) + f.(Csyntax.fn_vars) g.(gen_trail) tbody) end. Local Open Scope error_monad_scope. -Definition transl_fundef (fd: C.fundef) : res fundef := +Definition transl_fundef (fd: Csyntax.fundef) : res fundef := match fd with - | C.Internal f => + | Csyntax.Internal f => do tf <- transl_function f; OK (Internal tf) - | C.External ef targs tres => + | Csyntax.External ef targs tres => OK (External ef targs tres) end. -Definition transl_program (p: C.program) : res program := +Definition transl_program (p: Csyntax.program) : res program := transform_partial_program transl_fundef p. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 59fc9bc..150ed76 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -33,7 +33,7 @@ Require Import SimplExprspec. Section PRESERVATION. -Variable prog: C.program. +Variable prog: Csyntax.program. Variable tprog: Clight.program. Hypothesis TRANSL: transl_program prog = OK tprog. @@ -76,20 +76,20 @@ Qed. Lemma type_of_fundef_preserved: forall f tf, transl_fundef f = OK tf -> - type_of_fundef tf = C.type_of_fundef f. + type_of_fundef tf = Csyntax.type_of_fundef f. Proof. intros. destruct f; monadInv H. exploit transl_function_spec; eauto. intros [A [B [C D]]]. - simpl. unfold type_of_function, C.type_of_function. congruence. + simpl. unfold type_of_function, Csyntax.type_of_function. congruence. auto. Qed. Lemma function_return_preserved: forall f tf, transl_function f = OK tf -> - fn_return tf = C.fn_return f. + fn_return tf = Csyntax.fn_return f. Proof. intros. unfold transl_function in H. - destruct (transl_stmt (C.fn_body f) (initial_generator tt)); inv H. + destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H. auto. Qed. @@ -190,11 +190,11 @@ Lemma tr_simple: forall le dst sl a tmps, tr_expr le dst r sl a tmps -> match dst with - | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil | For_set tyl t => exists b, sl = do_set t tyl b - /\ C.typeof r = typeof b + /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end) /\ @@ -202,7 +202,7 @@ Lemma tr_simple: eval_simple_lvalue ge e m l b ofs -> forall le sl a tmps, tr_expr le For_val l sl a tmps -> - sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs). + sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs). Proof. Opaque makeif. intros e m. @@ -275,11 +275,11 @@ Lemma tr_simple_rvalue: forall le dst sl a tmps, tr_expr le dst r sl a tmps -> match dst with - | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil | For_set tyl t => exists b, sl = do_set t tyl b - /\ C.typeof r = typeof b + /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end. Proof. @@ -291,7 +291,7 @@ Lemma tr_simple_lvalue: eval_simple_lvalue ge e m l b ofs -> forall le sl a tmps, tr_expr le For_val l sl a tmps -> - sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs. + sl = nil /\ Csyntax.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs. Proof. intros e m. exact (proj2 (tr_simple e m)). Qed. @@ -315,8 +315,8 @@ Qed. Lemma typeof_context: forall k1 k2 C, leftcontext k1 k2 C -> - forall e1 e2, C.typeof e1 = C.typeof e2 -> - C.typeof (C e1) = C.typeof (C e2). + forall e1 e2, Csyntax.typeof e1 = Csyntax.typeof e2 -> + Csyntax.typeof (C e1) = Csyntax.typeof (C e2). Proof. induction 1; intros; auto. Qed. @@ -337,7 +337,7 @@ Lemma tr_expr_leftcontext_rec: /\ (forall le' e' sl3, tr_expr le' dst' e' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof e' = C.typeof e -> + Csyntax.typeof e' = Csyntax.typeof e -> tr_expr le' dst (C e') (sl3 ++ sl2) a tmps) ) /\ ( forall from C, leftcontextlist from C -> @@ -350,7 +350,7 @@ Lemma tr_expr_leftcontext_rec: /\ (forall le' e' sl3, tr_expr le' dst' e' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof e' = C.typeof e -> + Csyntax.typeof e' = Csyntax.typeof e -> tr_exprlist le' (C e') (sl3 ++ sl2) a tmps) ). Proof. @@ -695,7 +695,7 @@ Theorem tr_expr_leftcontext: /\ (forall le' r' sl3, tr_expr le' dst' r' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof r' = C.typeof r -> + Csyntax.typeof r' = Csyntax.typeof r -> tr_expr le' dst (C r') (sl3 ++ sl2) a tmps). Proof. intros. eapply (proj1 tr_expr_leftcontext_rec); eauto. @@ -714,7 +714,7 @@ Theorem tr_top_leftcontext: /\ (forall le' m' r' sl3, tr_expr le' dst' r' sl3 a' tmp' -> (forall id, ~In id tmp' -> le'!id = le!id) -> - C.typeof r' = C.typeof r -> + Csyntax.typeof r' = Csyntax.typeof r -> tr_top tge e le' m' dst (C r') (sl3 ++ sl2) a tmps). Proof. induction 1; intros. @@ -895,7 +895,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop := | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps, transl_function f = Errors.OK tf -> leftcontext RV RV C -> - (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (C.Eval v ty)) sl a tmps) -> + (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) -> match_cont_exp dest a k tk -> match_cont (Csem.Kcall f e C ty k) (Kcall optid tf e le (Kseqlist sl tk)) @@ -1220,10 +1220,10 @@ Proof. (* for not skip *) rename s' into sr. rewrite (tr_find_label_if _ _ H3); auto. - exploit (IHs1 (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)); eauto. + exploit (IHs1 (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)); eauto. econstructor; eauto. econstructor; eauto. destruct (Csem.find_label lbl s1 - (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)) as [[s' k'] | ]. + (Csem.Kseq (Csyntax.Sfor Csyntax.Sskip e s2 s3) k)) as [[s' k'] | ]. intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. intro EQ; rewrite EQ. exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto. @@ -1265,49 +1265,49 @@ End FIND_LABEL. Sdo a, k ---> a, Kdo k ---> rval v, Kdo k ---> Sskip, k >> but the translation, which is [Sskip], makes no transitions. -- The reduction [C.Ecomma (C.Eval v) r2 --> r2]. -- The reduction [C.Eparen (C.Eval v) --> C.Eval v] in a [For_effects] context. +- The reduction [Ecomma (Eval v) r2 --> r2]. +- The reduction [Eparen (Eval v) --> Eval v] in a [For_effects] context. The following measure decreases for these stuttering steps. *) -Fixpoint esize (a: C.expr) : nat := +Fixpoint esize (a: Csyntax.expr) : nat := match a with - | C.Eloc _ _ _ => 1%nat - | C.Evar _ _ => 1%nat - | C.Ederef r1 _ => S(esize r1) - | C.Efield l1 _ _ => S(esize l1) - | C.Eval _ _ => O - | C.Evalof l1 _ => S(esize l1) - | C.Eaddrof l1 _ => S(esize l1) - | C.Eunop _ r1 _ => S(esize r1) - | C.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat - | C.Ecast r1 _ => S(esize r1) - | C.Eseqand r1 _ _ => S(esize r1) - | C.Eseqor r1 _ _ => S(esize r1) - | C.Econdition r1 _ _ _ => S(esize r1) - | C.Esizeof _ _ => 1%nat - | C.Ealignof _ _ => 1%nat - | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat - | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat - | C.Epostincr _ l1 _ => S(esize l1) - | C.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat - | C.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat - | C.Ebuiltin ef _ rl _ => S(esizelist rl)%nat - | C.Eparen r1 _ => S(esize r1) + | Csyntax.Eloc _ _ _ => 1%nat + | Csyntax.Evar _ _ => 1%nat + | Csyntax.Ederef r1 _ => S(esize r1) + | Csyntax.Efield l1 _ _ => S(esize l1) + | Csyntax.Eval _ _ => O + | Csyntax.Evalof l1 _ => S(esize l1) + | Csyntax.Eaddrof l1 _ => S(esize l1) + | Csyntax.Eunop _ r1 _ => S(esize r1) + | Csyntax.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat + | Csyntax.Ecast r1 _ => S(esize r1) + | Csyntax.Eseqand r1 _ _ => S(esize r1) + | Csyntax.Eseqor r1 _ _ => S(esize r1) + | Csyntax.Econdition r1 _ _ _ => S(esize r1) + | Csyntax.Esizeof _ _ => 1%nat + | Csyntax.Ealignof _ _ => 1%nat + | Csyntax.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat + | Csyntax.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat + | Csyntax.Epostincr _ l1 _ => S(esize l1) + | Csyntax.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat + | Csyntax.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat + | Csyntax.Ebuiltin ef _ rl _ => S(esizelist rl)%nat + | Csyntax.Eparen r1 _ => S(esize r1) end -with esizelist (el: C.exprlist) : nat := +with esizelist (el: Csyntax.exprlist) : nat := match el with - | C.Enil => O - | C.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat + | Csyntax.Enil => O + | Csyntax.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat end. Definition measure (st: Csem.state) : nat := match st with | Csem.ExprState _ r _ _ _ => (esize r + 1)%nat - | Csem.State _ C.Sskip _ _ _ => 0%nat - | Csem.State _ (C.Sdo r) _ _ _ => (esize r + 2)%nat - | Csem.State _ (C.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat + | Csem.State _ Csyntax.Sskip _ _ _ => 0%nat + | Csem.State _ (Csyntax.Sdo r) _ _ _ => (esize r + 2)%nat + | Csem.State _ (Csyntax.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat | _ => 0%nat end. @@ -1338,7 +1338,7 @@ Lemma tr_val_gen: (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 dst (C.Eval v ty) (final dst a) a tmp. + tr_expr le dst (Csyntax.Eval v ty) (final dst a) a tmp. Proof. intros. destruct dst; simpl; econstructor; auto. Qed. @@ -1378,7 +1378,7 @@ Proof. econstructor; split. left. eapply plus_two. constructor. eapply step_make_set; eauto. traceEq. econstructor; eauto. - change (final dst' (Etempvar t0 (C.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (C.typeof l)) ++ sl2)). + change (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (Csyntax.typeof l)) ++ sl2)). apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss. intros. apply PTree.gso. red; intros; subst; elim H5; auto. @@ -1784,7 +1784,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor. econstructor; eauto. rewrite <- TY1; eauto. traceEq. econstructor; eauto. - change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S. + change sl2 with (final For_val (Etempvar t (Csyntax.typeof r)) ++ sl2). apply S. constructor. auto. intros. constructor. rewrite H2; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. @@ -1877,7 +1877,7 @@ Qed. Lemma tr_top_val_for_val_inv: forall e le m v ty sl a tmps, - tr_top tge e le m For_val (C.Eval v ty) sl a tmps -> + tr_top tge e le m For_val (Csyntax.Eval v ty) sl a tmps -> sl = nil /\ typeof a = ty /\ eval_expr tge e le m a v. Proof. intros. inv H. auto. inv H0. auto. @@ -2087,7 +2087,7 @@ Proof. inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. econstructor. eauto. - replace (fn_return tf) with (C.fn_return f). eauto. + replace (fn_return tf) with (Csyntax.fn_return f). eauto. exploit transl_function_spec; eauto. intuition congruence. eauto. traceEq. constructor. apply match_cont_call; auto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 571a937..5cb0f18 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -35,9 +35,9 @@ Local Open Scope gensym_monad_scope. (** This specification covers: - all cases of [transl_lvalue] and [transl_rvalue]; -- two additional cases for [C.Eparen], so that reductions of [C.Econdition] +- two additional cases for [Csyntax.Eparen], so that reductions of [Csyntax.Econdition] expressions are properly tracked; -- three additional cases allowing [C.Eval v] C expressions to match +- three additional cases allowing [Csyntax.Eval v] C expressions to match any Clight expression [a] that evaluates to [v] in any environment matching the given temporary environment [le]. *) @@ -57,69 +57,69 @@ Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Pro type_is_volatile ty = true -> In t tmp -> tr_rvalof ty a (make_set t a :: nil) (Etempvar t ty) tmp. -Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop := | tr_var: forall le dst id ty tmp, - tr_expr le dst (C.Evar id ty) + tr_expr le dst (Csyntax.Evar id ty) (final dst (Evar id ty)) (Evar id ty) tmp | tr_deref: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Ederef e1 ty) + tr_expr le dst (Csyntax.Ederef e1 ty) (sl1 ++ final dst (Ederef a1 ty)) (Ederef a1 ty) tmp | tr_field: forall le dst e1 f ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Efield e1 f ty) + tr_expr le dst (Csyntax.Efield e1 f ty) (sl1 ++ final dst (Efield a1 f ty)) (Efield a1 f ty) tmp | tr_val_effect: forall le v ty any tmp, - tr_expr le For_effects (C.Eval v ty) nil any tmp + tr_expr le For_effects (Csyntax.Eval v ty) nil any tmp | tr_val_value: forall le v ty a 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_val (C.Eval v ty) + tr_expr le For_val (Csyntax.Eval v ty) nil a tmp | tr_val_set: forall le tyl t 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_set tyl t) (C.Eval v ty) + tr_expr le (For_set tyl t) (Csyntax.Eval v ty) (do_set t tyl a) any tmp | tr_sizeof: forall le dst ty' ty tmp, - tr_expr le dst (C.Esizeof ty' ty) + tr_expr le dst (Csyntax.Esizeof ty' ty) (final dst (Esizeof ty' ty)) (Esizeof ty' ty) tmp | tr_alignof: forall le dst ty' ty tmp, - tr_expr le dst (C.Ealignof ty' ty) + tr_expr le dst (Csyntax.Ealignof ty' ty) (final dst (Ealignof ty' ty)) (Ealignof ty' ty) tmp | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 -> + tr_rvalof (Csyntax.typeof e1) a1 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Evalof e1 ty) + tr_expr le dst (Csyntax.Evalof e1 ty) (sl1 ++ sl2 ++ final dst a2) a2 tmp | tr_addrof: forall le dst e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Eaddrof e1 ty) + tr_expr le dst (Csyntax.Eaddrof e1 ty) (sl1 ++ final dst (Eaddrof a1 ty)) (Eaddrof a1 ty) tmp | tr_unop: forall le dst op e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Eunop op e1 ty) + tr_expr le dst (Csyntax.Eunop op e1 ty) (sl1 ++ final dst (Eunop op a1 ty)) (Eunop op a1 ty) tmp | tr_binop: forall le dst op e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ebinop op e1 e2 ty) + tr_expr le dst (Csyntax.Ebinop op e1 e2 ty) (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty)) (Ebinop op a1 a2 ty) tmp | tr_cast: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> - tr_expr le dst (C.Ecast e1 ty) + tr_expr le dst (Csyntax.Ecast e1 ty) (sl1 ++ final dst (Ecast a1 ty)) (Ecast a1 ty) tmp | tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp, @@ -127,7 +127,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le For_val (C.Eseqand e1 e2 ty) + tr_expr le For_val (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil) (Etempvar t ty) tmp @@ -136,7 +136,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_effects e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eseqand e1 e2 ty) + tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil) any tmp | tr_seqand_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -144,7 +144,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eseqand e1 e2 ty) + tr_expr le (For_set tyl t) (Csyntax.Eseqand e1 e2 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil) any tmp @@ -153,7 +153,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le For_val (C.Eseqor e1 e2 ty) + tr_expr le For_val (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil) (Etempvar t ty) tmp @@ -162,7 +162,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_effects e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eseqor e1 e2 ty) + tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil) any tmp | tr_seqor_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -170,7 +170,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eseqor e1 e2 ty) + tr_expr le (For_set tyl t) (Csyntax.Eseqor e1 e2 ty) (sl1 ++ makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil) any tmp @@ -181,7 +181,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> - tr_expr le For_val (C.Econdition e1 e2 e3 ty) + tr_expr le For_val (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) (Etempvar t ty) tmp | tr_condition_effects: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, @@ -191,7 +191,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> - tr_expr le For_effects (C.Econdition e1 e2 e3 ty) + tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) any tmp | tr_condition_set: forall le tyl t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, @@ -201,7 +201,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Econdition e1 e2 e3 ty) + tr_expr le (For_set tyl t) (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) any tmp | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, @@ -209,7 +209,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le For_val e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Eassign e1 e2 ty) + tr_expr le For_effects (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ make_assign a1 a2 :: nil) any tmp | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2, @@ -218,9 +218,9 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - incl tmp1 tmp -> incl tmp2 tmp -> list_disjoint tmp1 tmp2 -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> - ty1 = C.typeof e1 -> - ty2 = C.typeof e2 -> - tr_expr le dst (C.Eassign e1 e2 ty) + ty1 = Csyntax.typeof e1 -> + ty2 = Csyntax.typeof e2 -> + tr_expr le dst (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: @@ -229,11 +229,11 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> - ty1 = C.typeof e1 -> + ty1 = Csyntax.typeof e1 -> tr_rvalof ty1 a1 sl3 a3 tmp3 -> list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> - tr_expr le For_effects (C.Eassignop op e1 e2 tyres ty) + tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil) any tmp | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1, @@ -243,8 +243,8 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 -> - ty1 = C.typeof e1 -> - tr_expr le dst (C.Eassignop op e1 e2 tyres ty) + ty1 = Csyntax.typeof e1 -> + tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ Sset t (Ebinop op a3 a2 tyres) :: make_assign a1 (Etempvar t tyres) :: @@ -253,17 +253,17 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_rvalof ty1 a1 sl2 a2 tmp2 -> - ty1 = C.typeof e1 -> + ty1 = Csyntax.typeof e1 -> incl tmp1 tmp -> incl tmp2 tmp -> list_disjoint tmp1 tmp2 -> - tr_expr le For_effects (C.Epostincr id e1 ty) + tr_expr le For_effects (Csyntax.Epostincr id e1 ty) (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil) any tmp | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> incl tmp1 tmp -> In t tmp -> ~In t tmp1 -> - ty1 = C.typeof e1 -> - tr_expr le dst (C.Epostincr id e1 ty) + ty1 = Csyntax.typeof e1 -> + tr_expr le dst (Csyntax.Epostincr id e1 ty) (sl1 ++ make_set t a1 :: make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: final dst (Etempvar t ty1)) @@ -273,13 +273,13 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le dst e2 sl2 a2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp + tr_expr le dst (Csyntax.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp | tr_call_effects: forall le e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le For_effects (C.Ecall e1 el2 ty) + tr_expr le For_effects (Csyntax.Ecall e1 el2 ty) (sl1 ++ sl2 ++ Scall None a1 al2 :: nil) any tmp | tr_call_val: forall le dst e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 t tmp, @@ -288,45 +288,45 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> In t tmp -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_expr le dst (C.Ecall e1 el2 ty) + tr_expr le dst (Csyntax.Ecall e1 el2 ty) (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: final dst (Etempvar t ty)) (Etempvar t ty) tmp | tr_builtin_effects: forall le ef tyargs el ty sl al tmp1 any tmp, tr_exprlist le el sl al tmp1 -> incl tmp1 tmp -> - tr_expr le For_effects (C.Ebuiltin ef tyargs el ty) + tr_expr le For_effects (Csyntax.Ebuiltin ef tyargs el ty) (sl ++ Sbuiltin None ef tyargs al :: nil) any tmp | tr_builtin_val: forall le dst ef tyargs el ty sl al tmp1 t tmp, dst <> For_effects -> tr_exprlist le el sl al tmp1 -> In t tmp -> incl tmp1 tmp -> - tr_expr le dst (C.Ebuiltin ef tyargs el ty) + tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty) (sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty)) (Etempvar t ty) tmp | tr_paren_val: forall le e1 ty sl1 a1 t tmp, tr_expr le (For_set (ty :: nil) t) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le For_val (C.Eparen e1 ty) + tr_expr le For_val (Csyntax.Eparen e1 ty) sl1 (Etempvar t ty) tmp | tr_paren_effects: forall le e1 ty sl1 a1 tmp any, tr_expr le For_effects e1 sl1 a1 tmp -> - tr_expr le For_effects (C.Eparen e1 ty) sl1 any tmp + tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp | tr_paren_set: forall le tyl t e1 ty sl1 a1 tmp any, tr_expr le (For_set (ty::tyl) t) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le (For_set tyl t) (C.Eparen e1 ty) sl1 any tmp + tr_expr le (For_set tyl t) (Csyntax.Eparen e1 ty) sl1 any tmp -with tr_exprlist: temp_env -> C.exprlist -> list statement -> list expr -> list ident -> Prop := +with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop := | tr_nil: forall le tmp, - tr_exprlist le C.Enil nil nil tmp + tr_exprlist le Csyntax.Enil nil nil tmp | tr_cons: forall le e1 el2 sl1 a1 tmp1 sl2 al2 tmp2 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_exprlist le el2 sl2 al2 tmp2 -> list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> - tr_exprlist le (C.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp. + tr_exprlist le (Csyntax.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp. Scheme tr_expr_ind2 := Minimality for tr_expr Sort Prop with tr_exprlist_ind2 := Minimality for tr_exprlist Sort Prop. @@ -372,11 +372,11 @@ Qed. (** The "top-level" translation is equivalent to [tr_expr] above for source terms. It brings additional flexibility in the matching - between C values and Cminor expressions: in the case of + between Csyntax values and Cminor expressions: in the case of [tr_expr], the Cminor expression must not depend on memory, while in the case of [tr_top] it can depend on the current memory state. This special case is extended to values occurring under - one or several [C.Eparen]. *) + one or several [Csyntax.Eparen]. *) Section TR_TOP. @@ -385,14 +385,14 @@ Variable e: env. Variable le: temp_env. Variable m: mem. -Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident -> Prop := +Inductive tr_top: destination -> Csyntax.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 For_val (Csyntax.Eval v ty) nil a tmp (* | tr_top_val_set: forall t tyl v ty a any tmp, typeof a = ty -> eval_expr ge e le m a v -> - tr_top (For_set tyl t) (C.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp + tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp *) | tr_top_base: forall dst r sl a tmp, tr_expr le dst r sl a tmp -> @@ -400,92 +400,92 @@ Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident (* | tr_top_paren_test: forall tyl t r ty sl a tmp, tr_top (For_set (ty :: tyl) t) r sl a tmp -> - tr_top (For_set tyl t) (C.Eparen r ty) sl a tmp. + tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp. *) End TR_TOP. (** ** Translation of statements *) -Inductive tr_expression: C.expr -> statement -> expr -> Prop := +Inductive tr_expression: Csyntax.expr -> statement -> expr -> Prop := | tr_expression_intro: forall r sl a tmps, (forall ge e le m, tr_top ge e le m For_val r sl a tmps) -> tr_expression r (makeseq sl) a. -Inductive tr_expr_stmt: C.expr -> statement -> Prop := +Inductive tr_expr_stmt: Csyntax.expr -> statement -> Prop := | tr_expr_stmt_intro: forall r sl a tmps, (forall ge e le m, tr_top ge e le m For_effects r sl a tmps) -> tr_expr_stmt r (makeseq sl). -Inductive tr_if: C.expr -> statement -> statement -> statement -> Prop := +Inductive tr_if: Csyntax.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_val r sl a tmps) -> tr_if r s1 s2 (makeseq (sl ++ makeif a s1 s2 :: nil)). -Inductive tr_stmt: C.statement -> statement -> Prop := +Inductive tr_stmt: Csyntax.statement -> statement -> Prop := | tr_skip: - tr_stmt C.Sskip Sskip + tr_stmt Csyntax.Sskip Sskip | tr_do: forall r s, tr_expr_stmt r s -> - tr_stmt (C.Sdo r) s + tr_stmt (Csyntax.Sdo r) s | tr_seq: forall s1 s2 ts1 ts2, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> - tr_stmt (C.Ssequence s1 s2) (Ssequence ts1 ts2) + tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2) | tr_ifthenelse: forall r s1 s2 s' a ts1 ts2, tr_expression r s' a -> tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> - tr_stmt (C.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2)) + tr_stmt (Csyntax.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2)) | tr_while: forall r s1 s' ts1, tr_if r Sskip Sbreak s' -> tr_stmt s1 ts1 -> - tr_stmt (C.Swhile r s1) + tr_stmt (Csyntax.Swhile r s1) (Sloop (Ssequence s' ts1) Sskip) | tr_dowhile: forall r s1 s' ts1, tr_if r Sskip Sbreak s' -> tr_stmt s1 ts1 -> - tr_stmt (C.Sdowhile r s1) + tr_stmt (Csyntax.Sdowhile r s1) (Sloop ts1 s') | tr_for_1: forall r s3 s4 s' ts3 ts4, tr_if r Sskip Sbreak s' -> tr_stmt s3 ts3 -> tr_stmt s4 ts4 -> - tr_stmt (C.Sfor C.Sskip r s3 s4) + tr_stmt (Csyntax.Sfor Csyntax.Sskip r s3 s4) (Sloop (Ssequence s' ts4) ts3) | tr_for_2: forall s1 r s3 s4 s' ts1 ts3 ts4, tr_if r Sskip Sbreak s' -> - s1 <> C.Sskip -> + s1 <> Csyntax.Sskip -> tr_stmt s1 ts1 -> tr_stmt s3 ts3 -> tr_stmt s4 ts4 -> - tr_stmt (C.Sfor s1 r s3 s4) + tr_stmt (Csyntax.Sfor s1 r s3 s4) (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3)) | tr_break: - tr_stmt C.Sbreak Sbreak + tr_stmt Csyntax.Sbreak Sbreak | tr_continue: - tr_stmt C.Scontinue Scontinue + tr_stmt Csyntax.Scontinue Scontinue | tr_return_none: - tr_stmt (C.Sreturn None) (Sreturn None) + tr_stmt (Csyntax.Sreturn None) (Sreturn None) | tr_return_some: forall r s' a, tr_expression r s' a -> - tr_stmt (C.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a))) + tr_stmt (Csyntax.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a))) | tr_switch: forall r ls s' a tls, tr_expression r s' a -> tr_lblstmts ls tls -> - tr_stmt (C.Sswitch r ls) (Ssequence s' (Sswitch a tls)) + tr_stmt (Csyntax.Sswitch r ls) (Ssequence s' (Sswitch a tls)) | tr_label: forall lbl s ts, tr_stmt s ts -> - tr_stmt (C.Slabel lbl s) (Slabel lbl ts) + tr_stmt (Csyntax.Slabel lbl s) (Slabel lbl ts) | tr_goto: forall lbl, - tr_stmt (C.Sgoto lbl) (Sgoto lbl) + tr_stmt (Csyntax.Sgoto lbl) (Sgoto lbl) -with tr_lblstmts: C.labeled_statements -> labeled_statements -> Prop := +with tr_lblstmts: Csyntax.labeled_statements -> labeled_statements -> Prop := | tr_default: forall s ts, tr_stmt s ts -> - tr_lblstmts (C.LSdefault s) (LSdefault ts) + tr_lblstmts (Csyntax.LSdefault s) (LSdefault ts) | tr_case: forall n s ls ts tls, tr_stmt s ts -> tr_lblstmts ls tls -> - tr_lblstmts (C.LScase n s ls) (LScase n ts tls). + tr_lblstmts (Csyntax.LScase n s ls) (LScase n ts tls). (** * Correctness proof with respect to the specification. *) @@ -504,7 +504,7 @@ Proof. Qed. Remark bind2_inversion: - forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (y: C) (z1 z3: generator) I, + forall (A B Csyntax: Type) (f: mon (A*B)) (g: A -> B -> mon Csyntax) (y: Csyntax) (z1 z3: generator) I, bind2 f g z1 = Res y z3 I -> exists x1, exists x2, exists z2, exists I1, exists I2, f z1 = Res (x1,x2) z2 I1 /\ g x1 x2 z2 = Res y z3 I2. @@ -632,7 +632,7 @@ Lemma contained_disjoint: contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2. Proof. intros; red; intros. red; intro; subst y. - exploit H; eauto. intros [A B]. exploit H0; eauto. intros [C D]. + exploit H; eauto. intros [A B]. exploit H0; eauto. intros [Csyntax D]. elim (Plt_strict x). apply Plt_Ple_trans with (gen_next g2); auto. Qed. @@ -640,7 +640,7 @@ Lemma contained_notin: forall g1 l g2 id g3, contained l g1 g2 -> within id g2 g3 -> ~In id l. Proof. - intros; red; intros. exploit H; eauto. intros [C D]. destruct H0 as [A B]. + intros; red; intros. exploit H; eauto. intros [Csyntax D]. destruct H0 as [A B]. elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto. Qed. @@ -737,13 +737,13 @@ Lemma transl_valof_meets_spec: exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'. Proof. unfold transl_valof; intros. - destruct (type_is_volatile ty) as []_eqn; monadInv H. + destruct (type_is_volatile ty) eqn:?; monadInv H. exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib. exists (@nil ident); split; eauto with gensym. constructor; auto. Qed. -Scheme expr_ind2 := Induction for C.expr Sort Prop - with exprlist_ind2 := Induction for C.exprlist Sort Prop. +Scheme expr_ind2 := Induction for Csyntax.expr Sort Prop + with exprlist_ind2 := Induction for Csyntax.exprlist Sort Prop. Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2. Lemma transl_meets_spec: @@ -775,7 +775,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* valof *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. - exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. UseFinish. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -790,7 +790,7 @@ Opaque makeif. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* binop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. UseFinish. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. @@ -801,7 +801,7 @@ Opaque makeif. monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. intros; eapply tr_seqand_val; eauto with gensym. @@ -809,13 +809,13 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for set *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_set; eauto with gensym. @@ -825,7 +825,7 @@ Opaque makeif. monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. intros; eapply tr_seqor_val; eauto with gensym. @@ -833,13 +833,13 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for set *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_set; eauto with gensym. @@ -849,7 +849,7 @@ Opaque makeif. monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exploit H1; eauto with gensym. intros [tmp3 [E F]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split. @@ -860,14 +860,14 @@ Opaque makeif. apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit H1; eauto. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. intros; eapply tr_condition_effects; eauto with gensym. apply contained_app; eauto with gensym. (* for test *) - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exploit H1; eauto with gensym. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. @@ -883,7 +883,7 @@ Opaque makeif. exists (@nil ident); split; auto with gensym. constructor. (* assign *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) exists (x1 :: tmp1 ++ tmp2); split. @@ -902,7 +902,7 @@ Opaque makeif. apply contained_app; eauto with gensym. (* assignop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. destruct dst; monadInv EQ3; simpl add_dest in *. (* for value *) @@ -928,7 +928,7 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. (* for effects *) - exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. @@ -939,7 +939,7 @@ Opaque makeif. apply contained_cons; eauto with gensym. (* comma *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto with gensym. intros [tmp2 [C D]]. + exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. destruct dst; simpl; eauto with gensym. @@ -949,7 +949,7 @@ Opaque makeif. apply contained_app; eauto with gensym. (* call *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) exists (x1 :: tmp1 ++ tmp2); split. @@ -988,7 +988,7 @@ Opaque makeif. monadInv H; exists (@nil ident); split; auto with gensym. constructor. (* cons *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. - exploit H0; eauto. intros [tmp2 [C D]]. + exploit H0; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. @@ -1054,13 +1054,13 @@ Qed. Theorem transl_function_spec: forall f tf, transl_function f = OK tf -> - tr_stmt f.(C.fn_body) tf.(fn_body) - /\ fn_return tf = C.fn_return f - /\ fn_params tf = C.fn_params f - /\ fn_vars tf = C.fn_vars f. + tr_stmt f.(Csyntax.fn_body) tf.(fn_body) + /\ fn_return tf = Csyntax.fn_return f + /\ fn_params tf = Csyntax.fn_params f + /\ fn_vars tf = Csyntax.fn_vars f. Proof. intros until tf. unfold transl_function. - case_eq (transl_stmt (C.fn_body f) (initial_generator tt)); intros; inv H0. + case_eq (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); intros; inv H0. simpl. intuition. eapply transl_stmt_meets_spec; eauto. Qed. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index f58a213..8df7b6e 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -83,7 +83,7 @@ Lemma type_of_global_preserved: Proof. unfold type_of_global; intros. rewrite varinfo_preserved. destruct (Genv.find_var_info ge id). auto. - destruct (Genv.find_funct_ptr ge id) as [fd|]_eqn; inv H. + destruct (Genv.find_funct_ptr ge id) as [fd|] eqn:?; inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. rewrite A. decEq. apply type_of_fundef_preserved; auto. Qed. @@ -183,12 +183,12 @@ Lemma match_envs_extcall: Proof. intros. eapply match_envs_invariant; eauto. intros. destruct H0. eapply H8. intros; red. auto. auto. - red in H2. intros. destruct (f b) as [[b' delta]|]_eqn. + red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?. eapply H1; eauto. - destruct (f' b) as [[b' delta]|]_eqn; auto. + destruct (f' b) as [[b' delta]|] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. - intros. destruct (f b) as [[b'' delta']|]_eqn. eauto. + intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. Qed. @@ -405,7 +405,7 @@ Lemma match_envs_set_temp: match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi. Proof. intros. unfold check_temp in H1. - destruct (VSet.mem id cenv) as []_eqn; monadInv H1. + destruct (VSet.mem id cenv) eqn:?; monadInv H1. destruct H. constructor; eauto; intros. (* vars *) generalize (me_vars0 id0); intros MV; inv MV. @@ -477,8 +477,8 @@ Remark add_local_variable_charact: VSet.In id1 cenv \/ exists chunk, access_mode ty = By_value chunk /\ id = id1 /\ VSet.mem id atk = false. Proof. intros. unfold add_local_variable. split; intros. - destruct (access_mode ty) as []_eqn; auto. - destruct (VSet.mem id atk) as []_eqn; auto. + destruct (access_mode ty) eqn:?; auto. + destruct (VSet.mem id atk) eqn:?; auto. rewrite VSF.add_iff in H. destruct H; auto. right; exists m; auto. destruct H as [A | [chunk [A [B C]]]]. destruct (access_mode ty); auto. destruct (VSet.mem id atk); auto. rewrite VSF.add_iff; auto. @@ -639,7 +639,7 @@ Proof. (* inductive case *) simpl in H1. inv H1. simpl. - destruct (VSet.mem id cenv) as []_eqn. simpl. + destruct (VSet.mem id cenv) eqn:?. simpl. (* variable is lifted out of memory *) exploit Mem.alloc_left_unmapped_inject; eauto. intros [j1 [A [B [C D]]]]. @@ -782,7 +782,7 @@ Proof. assert (forall id l1 l2, (In id (var_names l1) -> In id (var_names l2)) -> (create_undef_temps l1)!id = None \/ (create_undef_temps l1)!id = (create_undef_temps l2)!id). - intros. destruct ((create_undef_temps l1)!id) as [v1|]_eqn; auto. + intros. destruct ((create_undef_temps l1)!id) as [v1|] eqn:?; auto. exploit create_undef_temps_inv; eauto. intros [A B]. subst v1. exploit list_in_map_inv. unfold var_names in H. apply H. eexact B. intros [[id1 ty1] [P Q]]. simpl in P; subst id1. @@ -813,7 +813,7 @@ Remark filter_charact: In x (List.filter f l) <-> In x l /\ f x = true. Proof. induction l; simpl. tauto. - destruct (f a) as []_eqn. + destruct (f a) eqn:?. simpl. rewrite IHl. intuition congruence. intuition congruence. Qed. @@ -902,7 +902,7 @@ Proof. unfold var_names in i. exploit list_in_map_inv; eauto. intros [[id' ty] [EQ IN]]; simpl in EQ; subst id'. exploit F; eauto. intros [b [P R]]. - destruct (VSet.mem id cenv) as []_eqn. + destruct (VSet.mem id cenv) eqn:?. (* local var, lifted *) destruct R as [U V]. exploit H2; eauto. intros [chunk X]. eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto. @@ -918,7 +918,7 @@ Proof. (* non-local var *) exploit G; eauto. unfold empty_env. rewrite PTree.gempty. intros [U V]. eapply match_var_not_local; eauto. - destruct (VSet.mem id cenv) as []_eqn; auto. + destruct (VSet.mem id cenv) eqn:?; auto. elim n; eauto. (* temps *) @@ -1072,7 +1072,7 @@ Proof. (* inductive case *) inv NOREPET. inv CASTED. inv VINJ. exploit me_vars; eauto. instantiate (1 := id); intros MV. - destruct (VSet.mem id cenv) as []_eqn. + destruct (VSet.mem id cenv) eqn:?. (* lifted to temp *) eapply IHbind_parameters with (tle1 := PTree.set id v' tle1); eauto. eapply match_envs_assign_lifted; eauto. @@ -1164,7 +1164,7 @@ Proof. induction l; simpl; intros. contradiction. destruct a as [[b1 lo1] hi1]. - destruct (Mem.free m b1 lo1 hi1) as [m1|]_eqn; try discriminate. + destruct (Mem.free m b1 lo1 hi1) as [m1|] eqn:?; try discriminate. destruct H0. inv H0. eapply Mem.free_range_perm; eauto. red; intros. eapply Mem.perm_free_3; eauto. eapply IHl; eauto. Qed. @@ -1209,7 +1209,7 @@ Lemma free_list_right_inject: Proof. induction l; simpl; intros. congruence. - destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|]_eqn; try discriminate. + destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|] eqn:?; try discriminate. eapply IHl with (m2 := m21); eauto. eapply Mem.free_right_inject; eauto. Qed. @@ -1380,8 +1380,8 @@ Proof. destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. destruct (Int.eq i Int.zero); try discriminate; auto. destruct (Int.eq i Int.zero); try discriminate; auto. - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; try discriminate. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; try discriminate. + destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate. + destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. simpl in H3. rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb). rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0). @@ -1509,7 +1509,7 @@ Proof. (* addrof *) exploit eval_simpl_lvalue; eauto. destruct a; auto with compat. - destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. + destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. elim (H0 i). apply VSet.singleton_2. auto. apply VSet.mem_2. auto. intros [b' [ofs' [A B]]]. exists (Vptr b' ofs'); split; auto. constructor; auto. @@ -1529,7 +1529,7 @@ Proof. (* rval *) assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true) \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)). - destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. left; exists i; exists t; auto. + destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. left; exists i; exists t; auto. destruct EITHER as [ [id [ty [EQ OPT]]] | NONOPT ]. (* a variable pulled out of memory *) subst a. simpl. rewrite OPT. @@ -1696,10 +1696,10 @@ Lemma match_cont_extcall: Proof. intros. eapply match_cont_invariant; eauto. destruct H0. intros. eapply H5; eauto. - red in H2. intros. destruct (f b) as [[b' delta] | ]_eqn. auto. - destruct (f' b) as [[b' delta] | ]_eqn; auto. + red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto. + destruct (f' b) as [[b' delta] | ] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. - red in H2. intros. destruct (f b) as [[b'' delta''] | ]_eqn. auto. + red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. Qed. @@ -1752,7 +1752,7 @@ Remark free_list_nextblock: Proof. induction l; simpl; intros. congruence. - destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate. + destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate. transitivity (Mem.nextblock m1). eauto. eapply Mem.nextblock_free; eauto. Qed. @@ -1764,7 +1764,7 @@ Remark free_list_load: Proof. induction l; simpl; intros. inv H; auto. - destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate. + destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate. transitivity (Mem.load chunk m1 b' 0). eauto. eapply Mem.load_free. eauto. left. assert (b' < b) by eauto. unfold block; omega. Qed. @@ -1860,7 +1860,7 @@ Remark is_liftable_var_charact: end. Proof. intros. destruct a; simpl; auto. - destruct (VSet.mem i cenv) as []_eqn. + destruct (VSet.mem i cenv) eqn:?. exists t; auto. auto. Qed. @@ -2202,7 +2202,7 @@ Proof. apply val_list_inject_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. - intros. destruct (create_undef_temps (fn_temps f))!id as [v|]_eqn; auto. + intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto. intros [tel [tm1 [P [Q [R [S T]]]]]]. change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f)) -- cgit v1.2.3