diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:58:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:58:24 +0000 |
commit | 6f9b68c8de22fe540bfe85c2fabec4b967c6a80d (patch) | |
tree | bcdc970a7cd51c9edc74cfe2d428b7d2f7205b61 | |
parent | dcaf93a7432304b3479ed191607aa4cd2966baf3 (diff) | |
download | compcert-6f9b68c8de22fe540bfe85c2fabec4b967c6a80d.tar.gz compcert-6f9b68c8de22fe540bfe85c2fabec4b967c6a80d.zip |
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
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | cfrontend/Clight.v | 1 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Csem.v | 2 | ||||
-rw-r--r-- | cfrontend/Csharpminor.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 6 | ||||
-rw-r--r-- | cfrontend/Cstrategy.v | 43 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 5 |
8 files changed, 28 insertions, 36 deletions
@@ -172,6 +172,9 @@ distclean: $(MAKE) clean rm -f Makefile.config +check-admitted: $(FILES) + @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." + include .depend FORCE: diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 4cc97ab2..4f4123e0 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -533,7 +533,6 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f Sskip k e le m) | step_return_0: forall f k e le m m', - f.(fn_return) = Tvoid -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn None) k e le m) E0 (Returnstate Vundef (call_cont k) m') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index e28228ab..5b2ad9b5 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -2965,7 +2965,7 @@ Proof. eapply external_call_nextblock_incr; eauto. eapply external_call_nextblock_incr; eauto. -(* return none *) +(* return *) inv MK. simpl. left; econstructor; split. apply plus_one. econstructor; eauto. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 2858e642..3f299158 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -1092,12 +1092,10 @@ Inductive sstep: state -> trace -> state -> Prop := E0 (State f (Sfor Sskip a2 a3 s) k e m) | step_return_0: forall f k e m m', - f.(fn_return) = Tvoid -> Mem.free_list m (blocks_of_env e) = Some m' -> sstep (State f (Sreturn None) k e m) E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f x k e m, - f.(fn_return) <> Tvoid -> sstep (State f (Sreturn (Some x)) k e m) E0 (ExprState f x (Kreturn k) e m) | step_return_2: forall f v1 ty k e m v2 m', diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 1a362e32..2f05678e 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -512,12 +512,10 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e le m) | step_return_0: forall f k e le m m', - f.(fn_return) = None -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn None) k e le m) E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v m', - f.(fn_return) <> None -> eval_expr e le m a v -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 02fab6fe..4784e1ed 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1691,7 +1691,7 @@ Proof. (* return none *) monadInv TR. inv MTR. econstructor; split. - apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto. + apply plus_one. constructor. eapply match_env_free_blocks; eauto. econstructor; eauto. eapply match_cont_call_cont. eauto. @@ -1699,9 +1699,11 @@ Proof. (* return some *) monadInv TR. inv MTR. econstructor; split. - apply plus_one. constructor. monadInv TRF. simpl. + apply plus_one. constructor. +(* monadInv TRF. simpl. unfold opttyp_of_type. destruct (Clight.fn_return f); try congruence. inv H0. inv H3. inv H3. +*) eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto. eapply match_env_free_blocks; eauto. econstructor; eauto. 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. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 603e2730..cff182d4 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1699,12 +1699,11 @@ Proof. econstructor; eauto. constructor; auto. (* return none *) - inv H8. econstructor; split. + inv H7. econstructor; split. left. apply plus_one. econstructor; eauto. - rewrite <- H. apply function_return_preserved; auto. constructor. apply match_cont_call; auto. (* return some 1 *) - inv H7. inv H1. econstructor; split. + inv H6. inv H0. econstructor; split. left; eapply plus_left. constructor. apply push_seq. traceEq. econstructor; eauto. constructor. auto. (* return some 2 *) |