diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /cfrontend/Cstrategy.v | |
parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'cfrontend/Cstrategy.v')
-rw-r--r-- | cfrontend/Cstrategy.v | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index c235031f..30e5c2ae 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -1553,13 +1553,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 +1582,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 +2734,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 +2745,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 +2754,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 +2802,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 +2815,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 +2828,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 +2865,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) |