From 9ab3738ae87a554fb742420b8c81ced4cd3c66c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 8 Sep 2020 13:56:01 +0200 Subject: Changed cc_varargs to an option type Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs. --- cfrontend/C2C.ml | 17 ++++++++++++----- cfrontend/Ctypes.v | 1 + cfrontend/Ctyping.v | 2 +- cfrontend/PrintCsyntax.ml | 8 ++++---- 4 files changed, 18 insertions(+), 10 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index ef028255..186c3155 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -552,10 +552,16 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let convertCallconv va unproto attr = +let convertCallconv _tres targs va attr = + let vararg = + match targs with + | None -> None + | Some tl -> if va then Some (Z.of_uint (List.length tl)) else None in let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } + { AST.cc_vararg = vararg; + AST.cc_unproto = (targs = None); + AST.cc_structret = (sr <> []) } (** Types *) @@ -623,7 +629,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va (targs = None) a) + convertCallconv tres targs va a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -989,7 +995,7 @@ let rec convertExpr env e = and tres = convertTyp env e.etyp in let sg = signature_of_type targs tres - { AST.cc_vararg = true; cc_unproto = false; cc_structret = false} in + { AST.cc_vararg = Some (coqint_of_camlint 1l); cc_unproto = false; cc_structret = false} in Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) @@ -1256,7 +1262,8 @@ let convertFundef loc env fd = a_loc = loc }; (id', AST.Gfun(Ctypes.Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_callconv = convertCallconv fd.fd_ret (Some fd.fd_params) + fd.fd_vararg fd.fd_attrib; fn_params = params; fn_vars = vars; fn_body = body'})) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 664a60c5..7ce50525 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -94,6 +94,7 @@ Proof. decide equality. decide equality. decide equality. + decide equality. Defined. Opaque type_eq typelist_eq. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 00fcf8ab..d9637b6a 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -170,7 +170,7 @@ Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}. Proof. decide equality. Defined. Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention := - if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + if option_eq Z.eq_dec cc1.(cc_vararg) cc2.(cc_vararg) then OK {| cc_vararg := cc1.(cc_vararg); cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); cc_structret := cc1.(cc_structret) |} diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 97a00b09..c49f6cd4 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -111,8 +111,8 @@ let rec name_cdecl id ty = | Tnil -> if first then Buffer.add_string b - (if cconv.cc_vararg then "..." else "void") - else if cconv.cc_vararg then + (if cconv.cc_vararg <> None then "..." else "void") + else if cconv.cc_vararg <> None then Buffer.add_string b ", ..." else () @@ -400,11 +400,11 @@ let name_function_parameters name_param fun_name params cconv = Buffer.add_char b '('; begin match params with | [] -> - Buffer.add_string b (if cconv.cc_vararg then "..." else "void") + Buffer.add_string b (if cconv.cc_vararg <> None then "..." else "void") | _ -> let rec add_params first = function | [] -> - if cconv.cc_vararg then Buffer.add_string b ",..." + if cconv.cc_vararg <> None then Buffer.add_string b ",..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl (name_param id) ty); -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- cfrontend/Cexec.v | 10 ++-- cfrontend/Clight.v | 2 +- cfrontend/Cminorgen.v | 2 +- cfrontend/Cminorgenproof.v | 130 +++++++++++++++++++++--------------------- cfrontend/Csem.v | 8 +-- cfrontend/Cshmgenproof.v | 20 +++---- cfrontend/Cstrategy.v | 50 ++++++++-------- cfrontend/Ctypes.v | 41 +++++++------ cfrontend/Ctyping.v | 24 ++++---- cfrontend/Initializersproof.v | 36 ++++++------ cfrontend/SimplExprproof.v | 18 +++--- cfrontend/SimplLocalsproof.v | 100 ++++++++++++++++---------------- 12 files changed, 222 insertions(+), 219 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b08c3ad7..d763c98c 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -290,7 +290,7 @@ Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': Remark check_assign_copy: forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. -Proof with try (right; intuition omega). +Proof with try (right; intuition lia). intros. unfold assign_copy_ok. destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto... destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto... @@ -306,8 +306,8 @@ Proof with try (right; intuition omega). destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto. destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto. destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto. - right; intuition omega. - destruct Y... left; intuition omega. + right; intuition lia. + destruct Y... left; intuition lia. Defined. Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) := @@ -579,7 +579,7 @@ Proof with try congruence. replace (Vlong Int64.zero) with Vnullptr. split; constructor. unfold Vnullptr; rewrite H0; auto. + destruct vargs... mydestr. - split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. + split. apply SIZE in Heqo0. econstructor; eauto. congruence. lia. constructor. - (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... @@ -636,7 +636,7 @@ Proof. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. - (* EF_free *) inv H; unfold do_ef_free. -+ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. ++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. lia. + inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. - (* EF_memcpy *) inv H; unfold do_ef_memcpy. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8ab29fe9..239ca370 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -739,7 +739,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; simpl; intros. inv H; simpl; try omega. + red; simpl; intros. inv H; simpl; try lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 45c21f96..1b031866 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -240,7 +240,7 @@ Module VarOrder <: TotalLeBool. Theorem leb_total: forall v1 v2, leb v1 v2 = true \/ leb v2 v1 = true. Proof. unfold leb; intros. - assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by omega. + assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by lia. unfold proj_sumbool. destruct H; [left|right]; apply zle_true; auto. Qed. End VarOrder. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5acb996d..bc1c92ca 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -287,7 +287,7 @@ Lemma match_env_external_call: Proof. intros. apply match_env_invariant with f1; auto. intros. eapply inject_incr_separated_same'; eauto. - intros. eapply inject_incr_separated_same; eauto. red. destruct H. xomega. + intros. eapply inject_incr_separated_same; eauto. red. destruct H. extlia. Qed. (** [match_env] and allocations *) @@ -317,18 +317,18 @@ Proof. constructor; eauto. constructor. (* low-high *) - rewrite NEXTBLOCK; xomega. + rewrite NEXTBLOCK; extlia. (* bounded *) intros. rewrite PTree.gsspec in H. destruct (peq id0 id). - inv H. rewrite NEXTBLOCK; xomega. - exploit me_bounded0; eauto. rewrite NEXTBLOCK; xomega. + inv H. rewrite NEXTBLOCK; extlia. + exploit me_bounded0; eauto. rewrite NEXTBLOCK; extlia. (* inv *) intros. destruct (eq_block b (Mem.nextblock m1)). subst b. rewrite SAME in H; inv H. exists id; exists sz. apply PTree.gss. rewrite OTHER in H; auto. exploit me_inv0; eauto. intros [id1 [sz1 EQ]]. exists id1; exists sz1. rewrite PTree.gso; auto. congruence. (* incr *) - intros. rewrite OTHER in H. eauto. unfold block in *; xomega. + intros. rewrite OTHER in H. eauto. unfold block in *; extlia. Qed. (** The sizes of blocks appearing in [e] are respected. *) @@ -512,23 +512,23 @@ Proof. (* base case *) econstructor; eauto. inv H. constructor; intros; eauto. - eapply IMAGE; eauto. eapply H6; eauto. xomega. + eapply IMAGE; eauto. eapply H6; eauto. extlia. (* inductive case *) assert (Ple lo hi) by (eapply me_low_high; eauto). econstructor; eauto. eapply match_temps_invariant; eauto. eapply match_env_invariant; eauto. - intros. apply H3. xomega. + intros. apply H3. extlia. eapply match_bounds_invariant; eauto. intros. eapply H1; eauto. - exploit me_bounded; eauto. xomega. + exploit me_bounded; eauto. extlia. eapply padding_freeable_invariant; eauto. - intros. apply H3. xomega. + intros. apply H3. extlia. eapply IHmatch_callstack; eauto. - intros. eapply H1; eauto. xomega. - intros. eapply H2; eauto. xomega. - intros. eapply H3; eauto. xomega. - intros. eapply H4; eauto. xomega. + intros. eapply H1; eauto. extlia. + intros. eapply H2; eauto. extlia. + intros. eapply H3; eauto. extlia. + intros. eapply H4; eauto. extlia. Qed. Lemma match_callstack_incr_bound: @@ -538,8 +538,8 @@ Lemma match_callstack_incr_bound: match_callstack f m tm cs bound' tbound'. Proof. intros. inv H. - econstructor; eauto. xomega. xomega. - constructor; auto. xomega. xomega. + econstructor; eauto. extlia. extlia. + constructor; auto. extlia. extlia. Qed. (** Assigning a temporary variable. *) @@ -596,17 +596,17 @@ Proof. auto. inv A. assert (Mem.range_perm m b 0 sz Cur Freeable). eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto. - replace ofs with ((ofs - delta) + delta) by omega. - eapply Mem.perm_inject; eauto. apply H3. omega. + replace ofs with ((ofs - delta) + delta) by lia. + eapply Mem.perm_inject; eauto. apply H3. lia. destruct X as [tm' FREE]. exploit nextblock_freelist; eauto. intro NEXT. exploit Mem.nextblock_free; eauto. intro NEXT'. exists tm'. split. auto. split. rewrite NEXT; rewrite NEXT'. - apply match_callstack_incr_bound with lo sp; try omega. + apply match_callstack_incr_bound with lo sp; try lia. apply match_callstack_invariant with f m tm; auto. intros. eapply perm_freelist; eauto. - intros. eapply Mem.perm_free_1; eauto. left; unfold block; xomega. xomega. xomega. + intros. eapply Mem.perm_free_1; eauto. left; unfold block; extlia. extlia. extlia. eapply Mem.free_inject; eauto. intros. exploit me_inv0; eauto. intros [id [sz A]]. exists 0; exists sz; split. @@ -636,21 +636,21 @@ Proof. inv H. constructor; auto. intros. case_eq (f1 b1). intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto. - intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. + intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. extlia. (* inductive case *) constructor. auto. auto. eapply match_temps_invariant; eauto. eapply match_env_invariant; eauto. red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?. exploit INCR; eauto. congruence. - exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. + exploit SEPARATED; eauto. intros [A B]. elim B. red. extlia. intros. assert (Ple lo hi) by (eapply me_low_high; eauto). destruct (f1 b) as [[b' delta']|] eqn:?. apply INCR; auto. destruct (f2 b) as [[b' delta']|] eqn:?; auto. - exploit SEPARATED; eauto. intros [A B]. elim A. red. xomega. + exploit SEPARATED; eauto. intros [A B]. elim A. red. extlia. eapply match_bounds_invariant; eauto. - intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega. + intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. extlia. (* padding-freeable *) red; intros. destruct (is_reachable_from_env_dec f1 e sp ofs). @@ -660,10 +660,10 @@ Proof. red; intros; red; intros. elim H3. exploit me_inv; eauto. intros [id [lv B]]. exploit BOUND0; eauto. intros C. - apply is_reachable_intro with id b0 lv delta; auto; omega. + apply is_reachable_intro with id b0 lv delta; auto; lia. eauto with mem. (* induction *) - eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega. + eapply IHmatch_callstack; eauto. inv MENV; extlia. extlia. Qed. (** [match_callstack] and allocations *) @@ -683,12 +683,12 @@ Proof. exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK. exploit Mem.alloc_result; eauto. intros RES. constructor. - xomega. - unfold block in *; xomega. + extlia. + unfold block in *; extlia. auto. constructor; intros. rewrite H3. rewrite PTree.gempty. constructor. - xomega. + extlia. rewrite PTree.gempty in H4; discriminate. eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto. rewrite RES. change (Mem.valid_block tm tb). eapply Mem.valid_block_inject_2; eauto. @@ -719,23 +719,23 @@ Proof. exploit Mem.alloc_result; eauto. intros RES. assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto). constructor. - xomega. + extlia. auto. eapply match_temps_invariant; eauto. eapply match_env_alloc; eauto. red; intros. rewrite PTree.gsspec in H. destruct (peq id0 id). inversion H. subst b0 sz0 id0. eapply Mem.perm_alloc_3; eauto. eapply BOUND0; eauto. eapply Mem.perm_alloc_4; eauto. - exploit me_bounded; eauto. unfold block in *; xomega. + exploit me_bounded; eauto. unfold block in *; extlia. red; intros. exploit PERM; eauto. intros [A|A]. auto. right. inv A. apply is_reachable_intro with id0 b0 sz0 delta; auto. rewrite PTree.gso. auto. congruence. eapply match_callstack_invariant with (m1 := m1); eauto. intros. eapply Mem.perm_alloc_4; eauto. - unfold block in *; xomega. - intros. apply H4. unfold block in *; xomega. + unfold block in *; extlia. + intros. apply H4. unfold block in *; extlia. intros. destruct (eq_block b0 b). - subst b0. rewrite H3 in H. inv H. xomegaContradiction. + subst b0. rewrite H3 in H. inv H. extlia. rewrite H4 in H; auto. Qed. @@ -828,11 +828,11 @@ Proof. eexact MINJ. eexact H. eexact VALID. - instantiate (1 := ofs). zify. omega. - intros. exploit STKSIZE; eauto. omega. - intros. apply STKPERMS. zify. omega. - replace (sz - 0) with sz by omega. auto. - intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. omega. + instantiate (1 := ofs). zify. lia. + intros. exploit STKSIZE; eauto. lia. + intros. apply STKPERMS. zify. lia. + replace (sz - 0) with sz by lia. auto. + intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. lia. intros [f2 [A [B [C D]]]]. exploit (IHalloc_variables f2); eauto. red; intros. eapply COMPAT. auto with coqlib. @@ -841,7 +841,7 @@ Proof. subst b. rewrite C in H5; inv H5. exploit SEP1. eapply in_eq. eapply in_cons; eauto. eauto. eauto. red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto. - omega. + lia. eapply SEP2. apply in_cons; eauto. eauto. rewrite D in H5; eauto. eauto. auto. intros. rewrite PTree.gso. eapply UNBOUND; eauto with coqlib. @@ -890,9 +890,9 @@ Remark block_alignment_pos: forall sz, block_alignment sz > 0. Proof. unfold block_alignment; intros. - destruct (zlt sz 2). omega. - destruct (zlt sz 4). omega. - destruct (zlt sz 8); omega. + destruct (zlt sz 2). lia. + destruct (zlt sz 4). lia. + destruct (zlt sz 8); lia. Qed. Remark assign_variable_incr: @@ -901,8 +901,8 @@ Remark assign_variable_incr: Proof. simpl; intros. inv H. generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)). - assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega. - omega. + assert (0 <= Z.max 0 sz). apply Zmax_bound_l. lia. + lia. Qed. Remark assign_variables_incr: @@ -910,7 +910,7 @@ Remark assign_variables_incr: assign_variables (cenv, sz) vars = (cenv', sz') -> sz <= sz'. Proof. induction vars; intros until sz'. - simpl; intros. inv H. omega. + simpl; intros. inv H. lia. Opaque assign_variable. destruct a as [id s]. simpl. intros. destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. @@ -931,11 +931,11 @@ Proof. assert (2 | 8). exists 4; auto. assert (4 | 8). exists 2; auto. destruct (zlt sz 2). - destruct chunk; simpl in *; auto; omegaContradiction. + destruct chunk; simpl in *; auto; extlia. destruct (zlt sz 4). - destruct chunk; simpl in *; auto; omegaContradiction. + destruct chunk; simpl in *; auto; extlia. destruct (zlt sz 8). - destruct chunk; simpl in *; auto; omegaContradiction. + destruct chunk; simpl in *; auto; extlia. destruct chunk; simpl; auto. apply align_divides. apply block_alignment_pos. Qed. @@ -948,7 +948,7 @@ Proof. replace (block_alignment sz) with (block_alignment (Z.max 0 sz)). apply inj_offset_aligned_block. rewrite Zmax_spec. destruct (zlt sz 0); auto. - transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega. + transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. lia. Qed. Lemma assign_variable_sound: @@ -976,23 +976,23 @@ Proof. exploit COMPAT; eauto. intros [ofs [A [B [C D]]]]. exists ofs. split. rewrite PTree.gso; auto. - split. auto. split. auto. zify; omega. + split. auto. split. auto. zify; lia. inv P. exists (align sz1 (block_alignment sz)). split. apply PTree.gss. split. apply inj_offset_aligned_block. - split. omega. - omega. + split. lia. + lia. apply EITHER in H; apply EITHER in H0. destruct H as [[P Q] | P]; destruct H0 as [[R S] | R]. rewrite PTree.gso in *; auto. eapply SEP; eauto. inv R. rewrite PTree.gso in H1; auto. rewrite PTree.gss in H2; inv H2. exploit COMPAT; eauto. intros [ofs [A [B [C D]]]]. assert (ofs = ofs1) by congruence. subst ofs. - left. zify; omega. + left. zify; lia. inv P. rewrite PTree.gso in H2; auto. rewrite PTree.gss in H1; inv H1. exploit COMPAT; eauto. intros [ofs [A [B [C D]]]]. assert (ofs = ofs2) by congruence. subst ofs. - right. zify; omega. + right. zify; lia. congruence. Qed. @@ -1023,7 +1023,7 @@ Proof. split. rewrite map_app. apply list_norepet_append_commut. simpl. constructor; auto. rewrite map_app. simpl. red; intros. rewrite in_app in H4. destruct H4. eauto. simpl in H4. destruct H4. subst y. red; intros; subst x. tauto. tauto. - generalize (assign_variable_incr _ _ _ _ _ _ Heqp). omega. + generalize (assign_variable_incr _ _ _ _ _ _ Heqp). lia. auto. auto. rewrite app_ass. auto. Qed. @@ -1054,7 +1054,7 @@ Proof. eexact H. simpl. rewrite app_nil_r. apply permutation_norepet with (map fst vars1); auto. apply Permutation_map. auto. - omega. + lia. red; intros. contradiction. red; intros. contradiction. destruct H1 as [A B]. split. @@ -1680,11 +1680,11 @@ Lemma switch_table_default: /\ snd (switch_table sl base) = (n + base)%nat. Proof. induction sl; simpl; intros. -- exists O; split. constructor. omega. +- exists O; split. constructor. lia. - destruct o. + destruct (IHsl (S base)) as (n & P & Q). exists (S n); split. constructor; auto. - destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. omega. + destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. lia. + exists O; split. constructor. destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. auto. Qed. @@ -1708,11 +1708,11 @@ Proof. exists O; split; auto. constructor. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. lia. auto. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. lia. auto. Qed. @@ -1725,10 +1725,10 @@ Proof. unfold select_switch; intros. generalize (switch_table_case i sl O (snd (switch_table sl O))). destruct (select_switch_case i sl) as [sl'|]. - intros (n & P & Q). replace (n + O)%nat with n in Q by omega. congruence. + intros (n & P & Q). replace (n + O)%nat with n in Q by lia. congruence. intros E; rewrite E. destruct (switch_table_default sl O) as (n & P & Q). - replace (n + O)%nat with n in Q by omega. congruence. + replace (n + O)%nat with n in Q by lia. congruence. Qed. Inductive transl_lblstmt_cont(cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := @@ -2039,7 +2039,7 @@ Proof. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. intros. eapply external_call_max_perm; eauto. - xomega. xomega. + extlia. extlia. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. econstructor; eauto. @@ -2191,7 +2191,7 @@ Opaque PTree.set. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. intros. eapply external_call_max_perm; eauto. - xomega. xomega. + extlia. extlia. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -2235,7 +2235,7 @@ Proof. eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z). auto. eapply Genv.initmem_inject; eauto. - apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega. + apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. extlia. extlia. constructor. red; auto. constructor. Qed. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 6d2b470f..4fa70ae2 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -839,11 +839,11 @@ Proof. unfold semantics; intros; red; simpl; intros. set (ge := globalenv p) in *. assert (DEREF: forall chunk m b ofs t v, deref_loc ge chunk m b ofs t v -> (length t <= 1)%nat). - intros. inv H0; simpl; try omega. inv H3; simpl; try omega. + intros. inv H0; simpl; try lia. inv H3; simpl; try lia. assert (ASSIGN: forall chunk m b ofs t v m', assign_loc ge chunk m b ofs v t m' -> (length t <= 1)%nat). - intros. inv H0; simpl; try omega. inv H3; simpl; try omega. + intros. inv H0; simpl; try lia. inv H3; simpl; try lia. destruct H. - inv H; simpl; try omega. inv H0; eauto; simpl; try omega. + inv H; simpl; try lia. inv H0; eauto; simpl; try lia. eapply external_call_trace_length; eauto. - inv H; simpl; try omega. eapply external_call_trace_length; eauto. + inv H; simpl; try lia. eapply external_call_trace_length; eauto. Qed. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 1ceb8e4d..6e653e01 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -689,32 +689,32 @@ Proof. destruct (zlt 0 sz); try discriminate. destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM. assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz). - { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. } + { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; lia. } destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c. + assert (E: Int64.signed (Int64.repr sz) = sz). { apply Int64.signed_repr. replace Int64.max_signed with Ptrofs.max_signed. - generalize Int64.min_signed_neg; omega. + generalize Int64.min_signed_neg; lia. unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. } econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero. - rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction. + rewrite H in E; rewrite Int64.signed_zero in E; extlia. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone. - rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction. + rewrite H0 in E; rewrite Int64.signed_mone in E; extlia. rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal. symmetry. auto with ptrofs. + assert (E: Int.signed (Int.repr sz) = sz). { apply Int.signed_repr. replace Int.max_signed with Ptrofs.max_signed. - generalize Int.min_signed_neg; omega. + generalize Int.min_signed_neg; lia. unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. } econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. - rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. + rewrite H in E; rewrite Int.signed_zero in E; extlia. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. - rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. + rewrite H0 in E; rewrite Int.signed_mone in E; extlia. rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal. symmetry. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). @@ -772,7 +772,7 @@ Proof. assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { unfold Int64.loword. rewrite Int.unsigned_repr; auto. - comput Int.max_unsigned; omega. + comput Int.max_unsigned; lia. } split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. Qed. @@ -786,7 +786,7 @@ Proof. assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { unfold Int64.loword. rewrite Int.unsigned_repr; auto. - comput Int.max_unsigned; omega. + comput Int.max_unsigned; lia. } unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. Qed. @@ -797,7 +797,7 @@ Lemma small_shift_amount_3: Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i. Proof. intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). - apply Int64.unsigned_repr. comput Int64.max_unsigned; omega. + apply Int64.unsigned_repr. comput Int64.max_unsigned; lia. Qed. Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl. 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) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 7ce50525..0de5075c 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -350,13 +350,16 @@ Fixpoint sizeof (env: composite_env) (t: type) : Z := Lemma sizeof_pos: forall env t, sizeof env t >= 0. Proof. - induction t; simpl; try omega. - destruct i; omega. - destruct f; omega. - destruct Archi.ptr64; omega. - change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. - destruct (env!i). apply co_sizeof_pos. omega. - destruct (env!i). apply co_sizeof_pos. omega. + induction t; simpl. +- lia. +- destruct i; lia. +- lia. +- destruct f; lia. +- destruct Archi.ptr64; lia. +- change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. lia. +- lia. +- destruct (env!i). apply co_sizeof_pos. lia. +- destruct (env!i). apply co_sizeof_pos. lia. Qed. (** The size of a type is an integral multiple of its alignment, @@ -435,18 +438,18 @@ Lemma sizeof_struct_incr: forall env m cur, cur <= sizeof_struct env cur m. Proof. induction m as [|[id t]]; simpl; intros. -- omega. +- lia. - apply Z.le_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. apply Z.le_trans with (align cur (alignof env t) + sizeof env t). - generalize (sizeof_pos env t); omega. + generalize (sizeof_pos env t); lia. apply IHm. Qed. Lemma sizeof_union_pos: forall env m, 0 <= sizeof_union env m. Proof. - induction m as [|[id t]]; simpl; xomega. + induction m as [|[id t]]; simpl; extlia. Qed. (** ** Byte offset for a field of a structure *) @@ -490,7 +493,7 @@ Proof. apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)). - apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. + apply align_le. apply alignof_pos. generalize (sizeof_pos env t). lia. Qed. Lemma field_offset_in_range: @@ -637,7 +640,7 @@ Proof. destruct n; auto. right; right; right. apply Z.min_l. rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ. - change 8 with (two_p 3). apply two_p_monotone. omega. + change 8 with (two_p 3). apply two_p_monotone. lia. } induction ty; simpl. auto. @@ -654,7 +657,7 @@ Qed. Lemma alignof_blockcopy_pos: forall env ty, alignof_blockcopy env ty > 0. Proof. - intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega. + intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition lia. Qed. Lemma sizeof_alignof_blockcopy_compat: @@ -670,8 +673,8 @@ Proof. apply Z.min_case. exists (two_p (Z.of_nat n)). change 8 with (two_p 3). - rewrite <- two_p_is_exp by omega. - rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega. + rewrite <- two_p_is_exp by lia. + rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. lia. apply Z.divide_refl. } induction ty; simpl. @@ -1090,8 +1093,8 @@ Remark rank_type_members: forall ce id t m, In (id, t) m -> (rank_type ce t <= rank_members ce m)%nat. Proof. induction m; simpl; intros; intuition auto. - subst a. xomega. - xomega. + subst a. extlia. + extlia. Qed. Lemma rank_struct_member: @@ -1104,7 +1107,7 @@ Proof. intros; simpl. rewrite H0. erewrite co_consistent_rank by eauto. exploit (rank_type_members ce); eauto. - omega. + lia. Qed. Lemma rank_union_member: @@ -1117,7 +1120,7 @@ Proof. intros; simpl. rewrite H0. erewrite co_consistent_rank by eauto. exploit (rank_type_members ce); eauto. - omega. + lia. Qed. (** * Programs and compilation units *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index d9637b6a..83f3cfe0 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1428,8 +1428,8 @@ Lemma pres_cast_int_int: forall sz sg n, wt_int (cast_int_int sz sg n) sz sg. Proof. intros. unfold cast_int_int. destruct sz; simpl. -- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. -- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia. +- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia. - auto. - destruct (Int.eq n Int.zero); auto. Qed. @@ -1616,12 +1616,12 @@ Proof. unfold access_mode, Val.load_result. remember Archi.ptr64 as ptr64. intros until v; intros AC. destruct ty; simpl in AC; try discriminate AC. - destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl. - destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. - inv AC. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. - destruct f; inv AC; destruct v; auto with ty. - inv AC. unfold Mptr. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. @@ -1637,16 +1637,16 @@ Proof. destruct ty; simpl in ACC; try discriminate. - destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. - inv ACC. unfold decode_val. destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. - destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 272b929f..10ccbeff 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -561,7 +561,7 @@ Local Opaque sizeof. + destruct (zeq sz 0). inv TR. exists (@nil init_data); split; auto. constructor. destruct (zle 0 sz). - inv TR. econstructor; split. constructor. omega. auto. + inv TR. econstructor; split. constructor. lia. auto. discriminate. + monadInv TR. destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). @@ -672,8 +672,8 @@ Remark padding_size: forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. Proof. unfold tr_padding; intros. destruct (zlt frm to). - simpl. xomega. - simpl. omega. + simpl. extlia. + simpl. lia. Qed. Remark idlsize_app: @@ -681,7 +681,7 @@ Remark idlsize_app: Proof. induction d1; simpl; intros. auto. - rewrite IHd1. omega. + rewrite IHd1. lia. Qed. Remark union_field_size: @@ -690,8 +690,8 @@ Proof. induction fl as [|[i t]]; simpl; intros. - inv H. - destruct (ident_eq f i). - + inv H. xomega. - + specialize (IHfl H). xomega. + + inv H. extlia. + + specialize (IHfl H). extlia. Qed. Hypothesis ce_consistent: composite_env_consistent ge. @@ -712,16 +712,16 @@ with tr_init_struct_size: Proof. Local Opaque sizeof. - destruct 1; simpl. -+ erewrite transl_init_single_size by eauto. omega. ++ erewrite transl_init_single_size by eauto. lia. + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. -+ replace (idlsize d) with (idlsize d + 0) by omega. ++ replace (idlsize d) with (idlsize d + 0) by lia. eapply tr_init_struct_size; eauto. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + rewrite idlsize_app, padding_size. - exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. + exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. @@ -730,21 +730,21 @@ Local Opaque sizeof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - destruct 1; simpl. -+ omega. ++ lia. + rewrite Z.mul_comm. assert (0 <= sizeof ge ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } - xomega. + { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. } + extlia. + rewrite idlsize_app. erewrite tr_init_size by eauto. erewrite tr_init_array_size by eauto. ring. - destruct 1; simpl; intros. -+ rewrite padding_size by auto. omega. ++ rewrite padding_size by auto. lia. + rewrite ! idlsize_app, padding_size. erewrite tr_init_size by eauto. - rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega. + rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia. unfold pos1. apply align_le. apply alignof_pos. Qed. @@ -806,7 +806,7 @@ Remark exec_init_array_length: forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> sz >= 0. Proof. - induction 1; omega. + induction 1; lia. Qed. Lemma store_init_data_list_app: @@ -847,10 +847,10 @@ Local Opaque sizeof. inv H3. simpl. erewrite transl_init_single_steps by eauto. auto. - (* array *) inv H1. replace (Z.max 0 sz) with sz in H7. eauto. - assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. + assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia. - (* struct *) inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. - replace ofs with (ofs + 0) by omega. eauto. + replace ofs with (ofs + 0) by lia. eauto. - (* union *) inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. eapply store_init_data_list_app. eauto. @@ -870,7 +870,7 @@ Local Opaque sizeof. inv H4. simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega. + replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 9a3f32ec..2d059ddd 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1449,13 +1449,13 @@ Proof. (* for val *) intros [SL1 [TY1 EV1]]. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_val_val; auto. (* for effects *) intros SL1. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_base. constructor. (* for set *) @@ -1779,7 +1779,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1788,7 +1788,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* postincr *) exploit tr_top_leftcontext; eauto. clear H14. @@ -1846,7 +1846,7 @@ Proof. subst. simpl Kseqlist. econstructor; split. right; split. rewrite app_ass; rewrite Kseqlist_app. eexact EXEC. - simpl; omega. + simpl; lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1863,7 +1863,7 @@ Proof. subst sl0; simpl Kseqlist. econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. auto. auto. @@ -1885,7 +1885,7 @@ Proof. (* for effects *) econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. apply S. constructor; auto. auto. auto. @@ -2015,12 +2015,12 @@ Proof. inv H6. inv H0. econstructor; split. right; split. apply push_seq. - simpl. omega. + simpl. lia. econstructor; eauto. constructor. auto. (* do 2 *) inv H7. inv H6. inv H. econstructor; split. - right; split. apply star_refl. simpl. omega. + right; split. apply star_refl. simpl. lia. econstructor; eauto. constructor. (* seq *) diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 2dd34389..8246a748 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -173,10 +173,10 @@ Proof. eapply H1; eauto. destruct (f' b) as [[b' delta]|] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. - xomegaContradiction. + extlia. intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. - xomegaContradiction. + extlia. Qed. (** Properties of values resulting from a cast *) @@ -606,7 +606,7 @@ Proof. generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ. auto. - right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. + right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. extlia. Qed. Lemma alloc_variables_injective: @@ -622,12 +622,12 @@ Proof. repeat rewrite PTree.gsspec; intros. destruct (peq id1 id); destruct (peq id2 id). congruence. - inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega. - inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega. + inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; extlia. + inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; extlia. eauto. intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). inv H6. - exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega. - exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega. + exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; extlia. + exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; extlia. Qed. Lemma match_alloc_variables: @@ -719,7 +719,7 @@ Proof. eapply Mem.valid_new_block; eauto. eapply Q; eauto. unfold Mem.valid_block in *. exploit Mem.nextblock_alloc. eexact A. exploit Mem.alloc_result. eexact A. - unfold block; xomega. + unfold block; extlia. split. intros. destruct (ident_eq id0 id). (* same var *) subst id0. @@ -760,7 +760,7 @@ Proof. destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto; unfold Mptr; simpl; destruct Archi.ptr64; auto. } - omega. + lia. Qed. Definition env_initial_value (e: env) (m: mem) := @@ -778,7 +778,7 @@ Proof. apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. destruct (peq id0 id). inv H2. eapply Mem.load_alloc_same'; eauto. - omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto. + lia. rewrite Z.add_0_l. eapply sizeof_by_value; eauto. apply Z.divide_0_r. eapply Mem.load_alloc_other; eauto. Qed. @@ -985,7 +985,7 @@ Proof. (* flat *) exploit alloc_variables_range. eexact A. eauto. rewrite PTree.gempty. intros [P|P]. congruence. - exploit K; eauto. unfold Mem.valid_block. xomega. + exploit K; eauto. unfold Mem.valid_block. extlia. intros [id0 [ty0 [U [V W]]]]. split; auto. destruct (ident_eq id id0). congruence. assert (b' <> b'). @@ -1032,34 +1032,34 @@ Proof. + (* special case size = 0 *) assert (bytes = nil). { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)). - omega. congruence. } + lia. congruence. } subst. destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil) as [tm' SB]. - simpl. red; intros; omegaContradiction. + simpl. red; intros; extlia. exists tm'. split. eapply assign_loc_copy; eauto. - intros; omegaContradiction. - intros; omegaContradiction. - rewrite e; right; omega. - apply Mem.loadbytes_empty. omega. + intros; extlia. + intros; extlia. + rewrite e; right; lia. + apply Mem.loadbytes_empty. lia. split. eapply Mem.storebytes_empty_inject; eauto. intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto. left. congruence. + (* general case size > 0 *) exploit Mem.loadbytes_length; eauto. intros LEN. assert (SZPOS: sizeof tge ty > 0). - { generalize (sizeof_pos tge ty); omega. } + { generalize (sizeof_pos tge ty); lia. } assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). replace (sizeof tge ty) with (Z.of_nat (List.length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. - rewrite LEN. apply Z2Nat.id. omega. + rewrite LEN. apply Z2Nat.id. lia. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). - apply RPSRC. omega. + apply RPSRC. lia. assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty). - apply RPDST. omega. + apply RPDST. lia. exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]]. @@ -1244,7 +1244,7 @@ Proof. destruct (Mem.range_perm_free m b lo hi) as [m1 A]; auto. rewrite A. apply IHl; auto. intros. red; intros. eapply Mem.perm_free_1; eauto. - exploit H1; eauto. intros [B|B]. auto. right; omega. + exploit H1; eauto. intros [B|B]. auto. right; lia. eapply H; eauto. Qed. @@ -1276,11 +1276,11 @@ Proof. change id' with (fst (id', (b', ty'))). apply List.in_map; auto. } assert (Mem.perm m b0 0 Max Nonempty). { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable. - eapply PERMS; eauto. omega. auto with mem. } + eapply PERMS; eauto. lia. auto with mem. } assert (Mem.perm m b0' 0 Max Nonempty). { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable. - eapply PERMS; eauto. omega. auto with mem. } - exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. omegaContradiction. + eapply PERMS; eauto. lia. auto with mem. } + exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. extlia. Qed. Lemma free_list_right_inject: @@ -1326,7 +1326,7 @@ Local Opaque ge tge. unfold block_of_binding in EQ; inv EQ. exploit me_mapped; eauto. eapply PTree.elements_complete; eauto. intros [b [A B]]. - change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by omega. + change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by lia. eapply Mem.range_perm_inject; eauto. eapply free_blocks_of_env_perm_2; eauto. - (* no overlap *) @@ -1343,7 +1343,7 @@ Local Opaque ge tge. intros [[id [b' ty]] [EQ IN]]. unfold block_of_binding in EQ. inv EQ. exploit me_flat; eauto. apply PTree.elements_complete; eauto. intros [P Q]. subst delta. eapply free_blocks_of_env_perm_1 with (m := m); eauto. - rewrite <- comp_env_preserved. omega. + rewrite <- comp_env_preserved. lia. Qed. (** Matching global environments *) @@ -1577,17 +1577,17 @@ Proof. induction 1; intros LOAD INCR INJ1 INJ2; econstructor; eauto. (* globalenvs *) inv H. constructor; intros; eauto. - assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. xomega. + assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. extlia. eapply IMAGE; eauto. (* call *) eapply match_envs_invariant; eauto. - intros. apply LOAD; auto. xomega. - intros. apply INJ1; auto; xomega. - intros. eapply INJ2; eauto; xomega. + intros. apply LOAD; auto. extlia. + intros. apply INJ1; auto; extlia. + intros. eapply INJ2; eauto; extlia. eapply IHmatch_cont; eauto. - intros; apply LOAD; auto. inv H0; xomega. - intros; apply INJ1. inv H0; xomega. - intros; eapply INJ2; eauto. inv H0; xomega. + intros; apply LOAD; auto. inv H0; extlia. + intros; apply INJ1. inv H0; extlia. + intros; eapply INJ2; eauto. inv H0; extlia. Qed. (** Invariance by assignment to location "above" *) @@ -1602,9 +1602,9 @@ Proof. intros. eapply match_cont_invariant; eauto. intros. rewrite <- H4. inv H0. (* scalar *) - simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; xomega. + simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; extlia. (* block copy *) - eapply Mem.load_storebytes_other; eauto. left. unfold block; xomega. + eapply Mem.load_storebytes_other; eauto. left. unfold block; extlia. Qed. (** Invariance by external calls *) @@ -1622,9 +1622,9 @@ Proof. intros. eapply Mem.load_unchanged_on; eauto. 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]. xomegaContradiction. + exploit H2; eauto. unfold Mem.valid_block. intros [A B]. extlia. red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. - exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction. + exploit H2; eauto. unfold Mem.valid_block. intros [A B]. extlia. Qed. (** Invariance by change of bounds *) @@ -1636,7 +1636,7 @@ Lemma match_cont_incr_bounds: Ple bound bound' -> Ple tbound tbound' -> match_cont f cenv k tk m bound' tbound'. Proof. - induction 1; intros; econstructor; eauto; xomega. + induction 1; intros; econstructor; eauto; extlia. Qed. (** [match_cont] and call continuations. *) @@ -1690,7 +1690,7 @@ Proof. inv H; auto. 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 (Plt b' b) by eauto. unfold block; xomega. + eapply Mem.load_free. eauto. left. assert (Plt b' b) by eauto. unfold block; extlia. Qed. Lemma match_cont_free_env: @@ -1708,9 +1708,9 @@ Proof. intros. rewrite <- H7. eapply free_list_load; eauto. unfold blocks_of_env; intros. exploit list_in_map_inv; eauto. intros [[id [b1 ty]] [P Q]]. simpl in P. inv P. - exploit me_range; eauto. eapply PTree.elements_complete; eauto. xomega. - rewrite (free_list_nextblock _ _ _ H3). inv H; xomega. - rewrite (free_list_nextblock _ _ _ H4). inv H; xomega. + exploit me_range; eauto. eapply PTree.elements_complete; eauto. extlia. + rewrite (free_list_nextblock _ _ _ H3). inv H; extlia. + rewrite (free_list_nextblock _ _ _ H4). inv H; extlia. Qed. (** Matching of global environments *) @@ -2018,7 +2018,7 @@ Proof. eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto. econstructor; eauto with compat. eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto. - eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega. + eapply match_cont_assign_loc; eauto. exploit me_range; eauto. extlia. inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3. eapply Mem.store_unmapped_inject; eauto. congruence. erewrite assign_loc_nextblock; eauto. @@ -2068,7 +2068,7 @@ Proof. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. eapply match_cont_extcall; eauto. - inv MENV; xomega. inv MENV; xomega. + inv MENV; extlia. inv MENV; extlia. eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. @@ -2212,11 +2212,11 @@ Proof. eapply bind_parameters_load; eauto. intros. exploit alloc_variables_range. eexact H1. eauto. unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence. - red; intros; subst b'. xomega. + red; intros; subst b'. extlia. eapply alloc_variables_load; eauto. apply compat_cenv_for. - rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). xomega. - rewrite T; xomega. + rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). extlia. + rewrite T; extlia. (* external function *) monadInv TRFD. inv FUNTY. @@ -2227,7 +2227,7 @@ Proof. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). - eapply match_cont_extcall; eauto. xomega. xomega. + eapply match_cont_extcall; eauto. extlia. extlia. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -2262,7 +2262,7 @@ Proof. eapply Genv.find_symbol_not_fresh; eauto. eapply Genv.find_funct_ptr_not_fresh; eauto. eapply Genv.find_var_info_not_fresh; eauto. - xomega. xomega. + extlia. extlia. eapply Genv.initmem_inject; eauto. constructor. Qed. -- cgit From 478ece46d8323ea182ded96a531309becf7445bb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 16 Jan 2021 15:27:02 +0100 Subject: Support re-normalization of function parameters at function entry This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to pass arguments that are not normalized. --- cfrontend/SimplLocals.v | 13 +++++++++---- cfrontend/SimplLocalsproof.v | 40 +++++++++++++++++++++++++++------------- 2 files changed, 36 insertions(+), 17 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index f54aa60d..0a164e29 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -18,7 +18,7 @@ Require FSetAVL. Require Import Coqlib Ordered Errors. Require Import AST Linking. Require Import Ctypes Cop Clight. -Require Compopts. +Require Compopts Conventions1. Open Scope error_monad_scope. Open Scope string_scope. @@ -157,15 +157,20 @@ with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_stat end. (** Function parameters that are not lifted to temporaries must be - stored in the corresponding local variable at function entry. *) + stored in the corresponding local variable at function entry. + The other function parameters may need to be normalized to their types, + to support interoperability with code generated by other C compilers. *) Fixpoint store_params (cenv: compilenv) (params: list (ident * type)) (s: statement): statement := match params with | nil => s | (id, ty) :: params' => - if VSet.mem id cenv - then store_params cenv params' s + if VSet.mem id cenv then + if Conventions1.parameter_needs_normalization (rettype_of_type ty) + then Ssequence (Sset id (make_cast (Etempvar id ty) ty)) + (store_params cenv params' s) + else store_params cenv params' s else Ssequence (Sassign (Evar id ty) (Etempvar id ty)) (store_params cenv params' s) end. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8246a748..988988a1 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1108,23 +1108,37 @@ Theorem store_params_correct: /\ match_envs j cenv e le m' lo hi te tle tlo thi /\ Mem.nextblock tm' = Mem.nextblock tm. Proof. +Local Opaque Conventions1.parameter_needs_normalization. induction 1; simpl; intros until targs; intros NOREPET CASTED VINJ MENV MINJ TLE LE. - (* base case *) +- (* base case *) inv VINJ. exists tle2; exists tm; split. apply star_refl. split. auto. split. auto. split. apply match_envs_temps_exten with tle1; auto. auto. - (* inductive case *) +- (* inductive case *) inv NOREPET. inv CASTED. inv VINJ. exploit me_vars; eauto. instantiate (1 := id); intros MV. - 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. - inv MV; try congruence. rewrite ENV in H; inv H. - inv H0; try congruence. - unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto. - intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto. - apply TLE. intuition. - (* still in memory *) + destruct (VSet.mem id cenv) eqn:LIFTED. ++ (* lifted to temp *) + exploit (IHbind_parameters s tm (PTree.set id v' tle1) (PTree.set id v' tle2)). + eauto. eauto. eauto. + eapply match_envs_assign_lifted; eauto. + inv MV; try congruence. rewrite ENV in H; inv H. + inv H0; try congruence. + unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto. + intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto. + apply TLE. intuition. + eauto. + intros (tle & tm' & U & V & X & Y & Z). + exists tle, tm'; split; [|auto]. + destruct (Conventions1.parameter_needs_normalization (rettype_of_type ty)); [|assumption]. + assert (A: tle!id = Some v'). + { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. } + eapply star_left. constructor. + eapply star_left. econstructor. eapply make_cast_correct. + constructor; eauto. apply cast_val_casted; auto. eapply val_casted_inject; eauto. + rewrite PTree.gsident by auto. + eapply star_left. constructor. eassumption. + traceEq. traceEq. traceEq. ++ (* still in memory *) inv MV; try congruence. rewrite ENV in H; inv H. exploit assign_loc_inject; eauto. intros [tm1 [A [B C]]]. @@ -1979,7 +1993,7 @@ Lemma find_label_store_params: forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k. Proof. induction params; simpl. auto. - destruct a as [id ty]. destruct (VSet.mem id cenv); auto. + destruct a as [id ty]. destruct (VSet.mem id cenv); [destruct Conventions1.parameter_needs_normalization|]; auto. Qed. Lemma find_label_add_debug_vars: -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- cfrontend/Ctyping.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 83f3cfe0..87e3506c 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -537,9 +537,9 @@ Inductive wt_program : program -> Prop := wt_fundef p.(prog_comp_env) e fd) -> wt_program p. -Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. -Hint Extern 1 (wt_int _ _ _) => exact I: ty. -Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. +Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. +Global Hint Extern 1 (wt_int _ _ _) => exact I: ty. +Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. Ltac DestructCases := match goal with @@ -955,7 +955,7 @@ Proof. destruct (classify_bool t); congruence. Qed. -Hint Resolve check_cast_sound check_bool_sound: ty. +Global Hint Resolve check_cast_sound check_bool_sound: ty. Lemma check_arguments_sound: forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl. -- cgit From ed89275cb820bb7ab283c51e461d852d1c8bec63 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:00:22 +0100 Subject: Section handling: finer control of variable initialization Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8. --- cfrontend/C2C.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 186c3155..fee3d86e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1333,8 +1333,13 @@ let convertGlobvar loc env (sto, id, ty, optinit) = if sto = C.Storage_extern then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in + let initialized = + if optinit = None then Sections.Uninit else + if List.exists (function AST.Init_addrof _ -> true | _ -> false) init' + then Sections.Init_reloc + else Sections.Init in let (section, access) = - Sections.for_variable env loc id' ty (optinit <> None) in + Sections.for_variable env loc id' ty initialized in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); -- cgit