diff options
Diffstat (limited to 'cfrontend/Cstrategy.v')
-rw-r--r-- | cfrontend/Cstrategy.v | 59 |
1 files changed, 30 insertions, 29 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index c235031f..6365f85c 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -1553,13 +1554,13 @@ Proof. exploit external_call_trace_length; eauto. destruct t1; simpl; intros. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. econstructor; econstructor. left; eapply step_builtin; eauto. - omegaContradiction. + extlia. (* external calls *) inv H1. exploit external_call_trace_length; eauto. destruct t1; simpl; intros. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto. - omegaContradiction. + extlia. (* well-behaved traces *) red; intros. inv H; inv H0; simpl; auto. (* valof volatile *) @@ -1582,10 +1583,10 @@ Proof. exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. (* builtins *) exploit external_call_trace_length; eauto. - destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. + destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia. (* external calls *) exploit external_call_trace_length; eauto. - destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. + destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia. Qed. (** The main simulation result. *) @@ -2734,7 +2735,7 @@ Proof. cofix COEL. intros. inv H. (* cons left *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)). eauto. eapply leftcontext_compose; eauto. constructor. auto. apply exprlist_app_leftcontext; auto. traceEq. @@ -2745,7 +2746,7 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. auto. apply exprlist_app_leftcontext; auto. eapply forever_N_star with (a2 := (esizelist al0)). - eexact R. simpl; omega. + eexact R. simpl; lia. change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0). rewrite <- exprlist_app_assoc. eapply COEL. eauto. auto. auto. @@ -2754,42 +2755,42 @@ Proof. intros. inv H. (* field *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Efield x f0 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* valof *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Evalof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* deref *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ederef x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* addrof *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eaddrof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* unop *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eunop op x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* cast *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecast x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand 2 *) @@ -2802,7 +2803,7 @@ Proof. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor 2 *) @@ -2815,7 +2816,7 @@ Proof. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition top *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition *) @@ -2828,33 +2829,33 @@ Proof. eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* assignop left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assignop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* postincr *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Epostincr id x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma right *) @@ -2865,14 +2866,14 @@ Proof. left; eapply step_comma; eauto. reflexivity. eapply COE with (C := C); eauto. traceEq. (* call left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* call right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; lia. eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq. (* call *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k) |