From 6f9b68c8de22fe540bfe85c2fabec4b967c6a80d Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:58:24 +0000 Subject: Removed useless constraints on return type at Sreturn instructions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cstrategy.v | 43 ++++++++++++++++++------------------------- 1 file changed, 18 insertions(+), 25 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3d81899f..ad991625 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -1971,11 +1971,13 @@ Lemma bigstep_to_steps: /\(forall e m s t m' out, exec_stmt e m s t m' out -> forall f k, +(* match out with | Out_return None => fn_return f = Tvoid | Out_return (Some(v, ty)) => fn_return f <> Tvoid | _ => True end -> +*) exists S, star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S) /\(forall m fd args t m' res, @@ -2176,7 +2178,7 @@ Proof. (* return some *) econstructor; split. - eapply star_left. right; apply step_return_1. auto. + eapply star_left. right; apply step_return_1. eapply H0. traceEq. econstructor; eauto. @@ -2194,7 +2196,7 @@ Proof. constructor. (* while stop *) - destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. set (S2 := match out' with | Out_break => State f Sskip k e m2 @@ -2212,7 +2214,7 @@ Proof. unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. (* while loop *) - destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. destruct (H6 f k) as [S2 [A2 B2]]; auto. exists S2; split. eapply star_left. right; apply step_while. @@ -2226,7 +2228,7 @@ Proof. auto. (* dowhile false *) - destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. exists (State f Sskip k e m2); split. eapply star_left. right; constructor. eapply star_trans. eexact A1. @@ -2238,7 +2240,7 @@ Proof. constructor. (* dowhile stop *) - destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. set (S2 := match out1 with | Out_break => State f Sskip k e m1 @@ -2254,7 +2256,7 @@ Proof. unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. (* dowhile loop *) - destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. destruct (H6 f k) as [S2 [A2 B2]]; auto. exists S2; split. eapply star_left. right; constructor. @@ -2269,7 +2271,7 @@ Proof. (* for start *) assert (a1 = Sskip \/ a1 <> Sskip). destruct a1; auto; right; congruence. - destruct H4. + destruct H3. subst a1. inv H. apply H2; auto. destruct (H0 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]; auto. inv B1. destruct (H2 f k) as [S2 [A2 B2]]; auto. @@ -2288,7 +2290,7 @@ Proof. constructor. (* for stop *) - destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. set (S2 := match out1 with | Out_break => State f Sskip k e m2 @@ -2306,7 +2308,7 @@ Proof. unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. (* for loop *) - destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. destruct (H6 f (Kfor4 a2 a3 s k)) as [S2 [A2 B2]]; auto. inv B2. destruct (H8 f k) as [S3 [A3 B3]]; auto. exists S3; split. @@ -2326,7 +2328,7 @@ Proof. auto. (* switch *) - destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]]. destruct out; auto. + destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_normal => State f Sskip k e m2 @@ -2350,8 +2352,6 @@ Proof. (* call internal *) destruct (H3 f k) as [S1 [A1 B1]]. - red in H4. destruct out; auto. destruct o as [[v' ty'] | ]. - tauto. destruct (fn_return f); tauto. eapply star_left. right; eapply step_internal_function; eauto. eapply star_right. eexact A1. inv B1; simpl in H4; try contradiction. @@ -2403,11 +2403,6 @@ Lemma exec_stmt_to_steps: forall e m s t m' out, exec_stmt e m s t m' out -> forall f k, - match out with - | Out_return None => fn_return f = Tvoid - | Out_return (Some(v, ty)) => fn_return f <> Tvoid - | _ => True - end -> exists S, star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S. Proof (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))). @@ -2465,8 +2460,6 @@ Proof. induction 1; intros; simpl; auto with arith. exploit leftcontext_size; eauto. auto with arith. Qed. -Axiom ADMITTED: forall (P: Prop), P. - Lemma evalinf_funcall_steps: forall m fd args t k, evalinf_funcall m fd args t -> @@ -2662,7 +2655,7 @@ Proof. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* return some *) - eapply forever_N_plus. apply plus_one; right; constructor. apply ADMITTED. + eapply forever_N_plus. apply plus_one; right; constructor. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* while test *) eapply forever_N_plus. apply plus_one; right; constructor. @@ -2675,7 +2668,7 @@ Proof. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* while loop *) - destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_trans. eapply eval_expression_to_steps; eauto. @@ -2688,7 +2681,7 @@ Proof. eapply forever_N_plus. apply plus_one; right; constructor. eapply COS; eauto. traceEq. (* dowhile test *) - destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_trans. eexact A1. @@ -2696,7 +2689,7 @@ Proof. reflexivity. reflexivity. eapply COE with (C := fun x => x); eauto. constructor. traceEq. (* dowhile loop *) - destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_trans. eexact A1. @@ -2728,7 +2721,7 @@ Proof. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* for next *) - destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. eapply forever_N_plus. eapply plus_left. right; apply step_for. eapply star_trans. eapply eval_expression_to_steps; eauto. @@ -2738,7 +2731,7 @@ Proof. reflexivity. reflexivity. reflexivity. reflexivity. eapply COS; eauto. traceEq. (* for loop *) - destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. destruct (exec_stmt_to_steps _ _ _ _ _ _ H4 f (Kfor4 a2 a3 s0 k)) as [S2 [A2 B2]]; auto. inv B2. eapply forever_N_plus. eapply plus_left. right; apply step_for. -- cgit