From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- Makefile | 10 +- aarch64/Asm.v | 66 +------- aarch64/Asmblockdeps.v | 12 +- aarch64/Asmblockgen.v | 2 +- aarch64/Asmblockgenproof0.v | 1 - aarch64/Asmblockgenproof1.v | 34 ++-- aarch64/Asmgenproof.v | 243 +++++++++++----------------- common/Values.v | 49 ++++++ lib/Coqlib.v | 35 ++++ lib/IterList.v | 15 ++ scheduling/postpass_lib/Machblockgenproof.v | 27 +--- 11 files changed, 240 insertions(+), 254 deletions(-) diff --git a/Makefile b/Makefile index 616c808f..de9da384 100644 --- a/Makefile +++ b/Makefile @@ -274,10 +274,14 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod a-w $*.v +# this trick aims to allow extraction to depend on the target processor +# (currently: export extra Coq-functions for OCaml code, depending on the target) extraction/extraction.v: Makefile extraction/extraction.vexpand - cat extraction/extraction.vexpand > extraction/extraction.v - echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v - echo "." >> extraction/extraction.v + (echo "(* WARNING: this file is generated from extraction.vexpand *)"; \ + echo "(* by the Makefile -- target \"extraction/extraction.v\" *)\n"; \ + cat extraction/extraction.vexpand; \ + echo "$(EXTRA_EXTRACTION)"; \ + echo ".") > extraction/extraction.v driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand tools/compiler_expand driver/Compiler.vexpand $@ diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 30bac2a4..dc1f025f 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -416,60 +416,6 @@ Definition outcome := option state. Definition Next rs m: outcome := Some (State rs m). Definition Stuck: outcome := None. - -(* a few lemma on comparisons of unsigned (e.g. pointers) - -TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!) -*) - -Definition Val_cmpu_bool cmp v1 v2: option bool := - Val.cmpu_bool (fun _ _ => true) cmp v1 v2. - -Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmpu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). - -Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) - (Val_cmpu cmp v1 v2). -Proof. - unfold Val.cmpu, Val_cmpu. - remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob; simpl. - - erewrite Val_cmpu_bool_correct; eauto. - econstructor. - - econstructor. -Qed. - -Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) - := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). - -Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmplu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). - -Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) - (Val_cmplu cmp v1 v2). -Proof. - unfold Val.cmplu, Val_cmplu. - remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob as [b|]; simpl. - - erewrite Val_cmplu_bool_correct; eauto. - simpl. econstructor. - - econstructor. -Qed. - (** Testing a condition *) Definition eval_testcond (c: testcond) (rs: regset) : option bool := @@ -540,8 +486,8 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := Definition eval_testzero (sz: isize) (v: val): option bool := match sz with - | W => Val_cmpu_bool Ceq v (Vint Int.zero) - | X => Val_cmplu_bool Ceq v (Vlong Int64.zero) + | W => Val.mxcmpu_bool Ceq v (Vint Int.zero) + | X => Val.mxcmplu_bool Ceq v (Vlong Int64.zero) end. (** Integer "bit is set?" test *) @@ -557,14 +503,14 @@ Definition eval_testbit (sz: isize) (v: val) (n: int): option bool := Definition compare_int (rs: regset) (v1 v2: val) := rs#CN <- (Val.negative (Val.sub v1 v2)) - #CZ <- (Val_cmpu Ceq v1 v2) - #CC <- (Val_cmpu Cge v1 v2) + #CZ <- (Val.mxcmpu Ceq v1 v2) + #CC <- (Val.mxcmpu Cge v1 v2) #CV <- (Val.sub_overflow v1 v2). Definition compare_long (rs: regset) (v1 v2: val) := rs#CN <- (Val.negativel (Val.subl v1 v2)) - #CZ <- (Val_cmplu Ceq v1 v2) - #CC <- (Val_cmplu Cge v1 v2) + #CZ <- (Val.mxcmplu Ceq v1 v2) + #CC <- (Val.mxcmplu Cge v1 v2) #CV <- (Val.subl_overflow v1 v2). (** Semantics of [fcmp] instructions: diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 670a7d06..e1d591df 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -211,14 +211,14 @@ Coercion Control: control_op >-> op_wrap. Definition v_compare_int (v1 v2: val) : CRflags := {| _CN := (Val.negative (Val.sub v1 v2)); - _CZ := (Val_cmpu Ceq v1 v2); - _CC := (Val_cmpu Cge v1 v2); + _CZ := (Val.mxcmpu Ceq v1 v2); + _CC := (Val.mxcmpu Cge v1 v2); _CV := (Val.sub_overflow v1 v2) |}. Definition v_compare_long (v1 v2: val) : CRflags := {| _CN := (Val.negativel (Val.subl v1 v2)); - _CZ := (Val_cmplu Ceq v1 v2); - _CC := (Val_cmplu Cge v1 v2); + _CZ := (Val.mxcmplu Ceq v1 v2); + _CC := (Val.mxcmplu Cge v1 v2); _CV := (Val.subl_overflow v1 v2) |}. Definition v_compare_float (v1 v2: val) : CRflags := @@ -1842,8 +1842,8 @@ Proof. destruct (PregEq.eq r PC); [ rewrite e; destruct sz0; simpl; Simpl sr | destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0; - try (destruct (Val_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); - try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); + try (destruct (Val.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); + try (destruct (Val.mxcmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr); diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index b55a1195..acb5a1e6 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -1245,7 +1245,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function := else OK tf. Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) + transf_partial_fundef transf_function f. Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 4217f526..03d863a3 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -37,7 +37,6 @@ Require Import Asmblock. Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. -Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) Require Import Asmblockprops. Module MB:=Machblock. diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index 754b49d6..61d77881 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -896,8 +896,8 @@ Ltac TranslOpBase := Lemma compare_int_spec: forall rs v1 v2, let rs' := compare_int rs v1 v2 in rs'#CN = (Val.negative (Val.sub v1 v2)) - /\ rs'#CZ = (Val_cmpu Ceq v1 v2) - /\ rs'#CC = (Val_cmpu Cge v1 v2) + /\ rs'#CZ = (Val.mxcmpu Ceq v1 v2) + /\ rs'#CC = (Val.mxcmpu Cge v1 v2) /\ rs'#CV = (Val.sub_overflow v1 v2). Proof. intros; unfold rs'; auto. @@ -912,7 +912,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmpu; simpl. destruct c; simpl. + unfold Val.mxcmpu; simpl. destruct c; simpl. - destruct (Int.eq i i0); auto. - destruct (Int.eq i i0); auto. - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. @@ -924,7 +924,7 @@ Proof. Qed. Lemma eval_testcond_compare_uint: forall c v1 v2 b rs, - Val_cmpu_bool c v1 v2 = Some b -> + Val.mxcmpu_bool c v1 v2 = Some b -> eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b. Proof. intros. generalize (compare_int_spec rs v1 v2). @@ -932,7 +932,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmpu; simpl. destruct c; simpl. + unfold Val.mxcmpu; simpl. destruct c; simpl. - destruct (Int.eq i i0); auto. - destruct (Int.eq i i0); auto. - destruct (Int.ltu i i0); auto. @@ -944,8 +944,8 @@ Qed. Lemma compare_long_spec: forall rs v1 v2, let rs' := compare_long rs v1 v2 in rs'#CN = (Val.negativel (Val.subl v1 v2)) - /\ rs'#CZ = (Val_cmplu Ceq v1 v2) - /\ rs'#CC = (Val_cmplu Cge v1 v2) + /\ rs'#CZ = (Val.mxcmplu Ceq v1 v2) + /\ rs'#CC = (Val.mxcmplu Cge v1 v2) /\ rs'#CV = (Val.subl_overflow v1 v2). Proof. intros; unfold rs'; auto. @@ -977,7 +977,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmplu; simpl. destruct c; simpl. + unfold Val.mxcmplu; simpl. destruct c; simpl. - destruct (Int64.eq i i0); auto. - destruct (Int64.eq i i0); auto. - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. @@ -989,12 +989,12 @@ Proof. Qed. Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs, - Val_cmplu_bool c v1 v2 = Some b -> + Val.mxcmplu_bool c v1 v2 = Some b -> eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b. Proof. intros. generalize (compare_long_spec rs v1 v2). set (rs' := compare_long rs v1 v2). intros (B & C & D & E). - unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu. + unfold eval_testcond; rewrite B, C, D, E; unfold Val.mxcmplu. destruct v1; try discriminate; destruct v2; try discriminate; simpl in H. - (* int-int *) inv H. destruct c; simpl. @@ -1207,7 +1207,7 @@ Proof. - (* Ccomplu *) econstructor; split. apply exec_straight_one. simpl; eauto. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. - (* Ccomplimm *) destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. @@ -1228,19 +1228,19 @@ Proof. destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. + econstructor; split. apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - (* Ccomplshift *) econstructor; split. apply exec_straight_one. simpl; eauto. @@ -1249,7 +1249,7 @@ Proof. - (* Ccomplushift *) econstructor; split. apply exec_straight_one. simpl; eauto. split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. - (* Cmasklzero *) destruct (is_logical_imm64 n). @@ -1368,7 +1368,7 @@ Local Opaque transl_cond transl_cond_branch_default. apply Int.same_if_eq in N0; subst n; ArgsInv. + (* Ccompuimm Cne 0 *) econstructor; split. econstructor. - split; auto. simpl. apply Val_cmpu_bool_correct in EV. + split; auto. simpl. apply Val.mxcmpu_bool_correct in EV. unfold incrPC. Simpl. rewrite EV. auto. + (* Ccompuimm Ceq 0 *) monadInv TR. ArgsInv. simpl in *. @@ -1408,7 +1408,7 @@ Local Opaque transl_cond transl_cond_branch_default. apply Int64.same_if_eq in N0; subst n; ArgsInv. + (* Ccompluimm Cne 0 *) econstructor; split. econstructor. - split; auto. simpl. apply Val_cmplu_bool_correct in EV. + split; auto. simpl. apply Val.mxcmplu_bool_correct in EV. unfold incrPC. Simpl. rewrite EV. auto. + (* Ccompluimm Ceq 0 *) econstructor; split. econstructor. diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index cec8ea69..a33f90b3 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -23,7 +23,7 @@ Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof. Require Import Asmgen. Require Import Axioms. Require Import IterList. -Require Import Ring. +Require Import Ring Lia. Module Asmblock_PRESERVATION. @@ -107,7 +107,7 @@ Proof. destruct (zlt _ _); try congruence. inv EQ. inv EQ0. eexists; intuition eauto. - omega. + lia. Qed. @@ -220,14 +220,14 @@ Proof. - inversion TRANSf. - unfold max_pos. assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. } - rewrite H; omega. + rewrite H; lia. Qed. Lemma one_le_max_unsigned: 1 <= Ptrofs.max_unsigned. Proof. unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize; - unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega. + unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; lia. Qed. (* NB: does not seem useful anymore, with the [exec_header_simulation] proof below @@ -256,7 +256,7 @@ Proof. * apply one_le_max_unsigned. + split. * apply Z.ge_le; assumption. - * rewrite <- functions_bound_max_pos; eauto; omega. + * rewrite <- functions_bound_max_pos; eauto; lia. Qed. *) @@ -287,16 +287,16 @@ Lemma list_length_z_aux_increase A (l: list A): forall acc, list_length_z_aux l acc >= acc. Proof. induction l; simpl; intros. - - omega. - - generalize (IHl (Z.succ acc)). omega. + - lia. + - generalize (IHl (Z.succ acc)). lia. Qed. Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1. Proof. destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl; - try (congruence || omega); + try (congruence || lia); unfold list_length_z; simpl; - generalize (list_length_z_aux_increase _ tl 1); omega. + generalize (list_length_z_aux_increase _ tl 1); lia. Qed. @@ -306,7 +306,7 @@ Proof. unfold list_length_z, list_length_z_aux. simpl. fold list_length_z_aux. rewrite (list_length_z_aux_shift l acc 0). - omega. + lia. Qed. Lemma list_length_z_cons A hd (tl : list A): @@ -315,14 +315,6 @@ Proof. unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity. Qed. -(*Lemma length_agree A (l : list A):*) - (*list_length_z l = Z.of_nat (length l).*) -(*Proof.*) - (*induction l as [| ? l IH]; intros.*) - (*- unfold list_length_z; reflexivity.*) - (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*) -(*Qed.*) - Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). Proof. unfold size. @@ -335,14 +327,14 @@ Proof. rewrite bblock_size_aux. generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT]. - destruct (body bb); try contradiction; rewrite list_length_z_cons; - repeat rewrite list_length_z_nat; omega. - - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega. + repeat rewrite list_length_z_nat; lia. + - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; lia. Qed. Lemma body_size_le_block_size bb: list_length_z (body bb) <= size bb. Proof. - rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega. + rewrite bblock_size_aux; repeat rewrite list_length_z_nat; lia. Qed. @@ -351,7 +343,7 @@ Proof. rewrite (bblock_size_aux bb). generalize (bblock_size_aux_pos bb). generalize (list_length_z_pos (header bb)). - omega. + lia. Qed. Lemma unfold_car_cdr bb bbs tc: @@ -470,7 +462,7 @@ Lemma list_nth_z_neg A (l: list A): forall n, n < 0 -> list_nth_z l n = None. Proof. induction l; simpl; auto. - intros n H; destruct (zeq _ _); (try eapply IHl); omega. + intros n H; destruct (zeq _ _); (try eapply IHl); lia. Qed. Lemma find_bblock_neg bbs: forall pos, @@ -539,12 +531,12 @@ Proof. + inv FINDBB. exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE. repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add. - omega. + lia. + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH. exploit bblock_size_preserved; eauto; intros SIZE. repeat (rewrite list_length_z_nat); rewrite app_length. rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat). - omega. + lia. Qed. Lemma size_of_blocks_max_pos pos f tf bi: @@ -565,7 +557,7 @@ Lemma unfold_bblock_not_nil bb: Proof. intros. exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE. - generalize (bblock_size_pos bb). intros SIZE'. omega. + generalize (bblock_size_pos bb). intros SIZE'. lia. Qed. (* same proof as list_nth_z_range (Coqlib) *) @@ -576,8 +568,8 @@ Proof. induction c; simpl; intros. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). - generalize (list_length_z_pos c); omega. - exploit IHc; eauto. omega. + generalize (list_length_z_pos c); lia. + exploit IHc; eauto. lia. Qed. Lemma find_instr_tail: @@ -590,8 +582,8 @@ Proof. - intros. rewrite list_length_z_cons. simpl. destruct (zeq (pos + (list_length_z tbb + 1)) 0). + exploit find_instr_range; eauto. intros POS_RANGE. - generalize (list_length_z_pos tbb). omega. - + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega. + generalize (list_length_z_pos tbb). lia. + + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. eapply IHtbb; eauto. Qed. @@ -604,7 +596,7 @@ Proof. intros (tf & _ & TRANSf). assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. } assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. } - omega. + lia. Qed. Lemma find_instr_bblock_tail: @@ -619,10 +611,10 @@ Proof. destruct (zeq (pos + size bb) 0). + (* absurd *) exploit find_instr_range; eauto. intros POS_RANGE. - generalize (bblock_size_pos bb). intros SIZE. omega. + generalize (bblock_size_pos bb). intros SIZE. lia. + erewrite bblock_size_preserved; eauto. rewrite list_length_z_cons. - replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega. + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. apply find_instr_tail; auto. Qed. @@ -671,14 +663,14 @@ Lemma list_nth_z_find_bi_with_header: Proof. induction ll. - unfold list_length_z. simpl. intros. - replace (n - 0) with n in H by omega. eapply list_nth_z_find_bi; eauto. + replace (n - 0) with n in H by lia. eapply list_nth_z_find_bi; eauto. - intros. simpl. destruct (zeq n 0). + rewrite list_length_z_cons in H. rewrite e in H. - replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by omega. + replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by lia. generalize (list_length_z_pos ll). intros. - rewrite list_nth_z_neg in H; try omega. inversion H. + rewrite list_nth_z_neg in H; try lia. inversion H. + rewrite list_length_z_cons in H. - replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by omega. + replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by lia. eapply IHll; eauto. Qed. @@ -689,13 +681,13 @@ Lemma range_list_nth_z: exists x, list_nth_z l n = Some x. Proof. induction l. - - intros. unfold list_length_z in H. simpl in H. omega. + - intros. unfold list_length_z in H. simpl in H. lia. - intros n. destruct (zeq n 0). + intros. simpl. destruct (zeq n 0). { eauto. } contradiction. + intros H. rewrite list_length_z_cons in H. simpl. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) by omega. - eapply IHl; omega. + replace (Z.pred n) with (n - 1) by lia. + eapply IHl; lia. Qed. Lemma list_nth_z_n_too_big: @@ -705,17 +697,17 @@ Lemma list_nth_z_n_too_big: n >= list_length_z l. Proof. induction l. - - intros. unfold list_length_z. simpl. omega. + - intros. unfold list_length_z. simpl. lia. - intros. rewrite list_length_z_cons. simpl in H0. destruct (zeq n 0) as [N | N]. + inversion H0. + (* XXX there must be a more elegant way to prove this simple fact *) - assert (n > 0). { omega. } - assert (0 <= n - 1). { omega. } + assert (n > 0). { lia. } + assert (0 <= n - 1). { lia. } generalize (IHl (n - 1)). intros IH. assert (n - 1 >= list_length_z l). { auto. } - assert (n > list_length_z l); omega. + assert (n > list_length_z l); lia. Qed. Lemma find_instr_past_header: @@ -729,9 +721,9 @@ Proof. - intros. simpl. destruct (zeq n 0) as [N | N]. + rewrite N in H. inversion H. + rewrite list_length_z_cons. - replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by omega. + replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by lia. simpl in H. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) in H by omega. + replace (Z.pred n) with (n - 1) in H by lia. apply IH; auto. Qed. @@ -753,9 +745,9 @@ Proof. simpl; destruct (zeq n 0) as [N|N]. + rewrite N in NTH; inversion NTH. + rewrite list_length_z_cons. - replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by omega. + replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by lia. simpl in NTH. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) in NTH by omega. + replace (Z.pred n) with (n - 1) in NTH by lia. apply IHlbi; auto. Qed. @@ -767,15 +759,15 @@ Lemma n_beyond_body: n >= Z.of_nat (length (header bb) + length (body bb)). Proof. intros. - assert (0 <= n). { omega. } + assert (0 <= n). { lia. } generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros. generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros. unfold size in H. - assert (0 <= n - list_length_z (header bb)). { omega. } + assert (0 <= n - list_length_z (header bb)). { lia. } assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. } - assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. } + assert (n >= list_length_z (header bb) + list_length_z (body bb)). { lia. } rewrite Nat2Z.inj_add. repeat (rewrite <- list_length_z_nat). assumption. Qed. @@ -910,20 +902,20 @@ Proof. repeat (rewrite Nat2Z.inj_add in UPPER). repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER. - assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. } + assert (n = list_length_z (header bb) + list_length_z (body bb)). { lia. } assert (n = size bb - 1). { unfold size. rewrite <- EXIT. simpl. - repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega. + repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. lia. } symmetry in EXIT. eexists; split. ** eapply is_nth_ctlflow; eauto. ** simpl. destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. } - (* absurd *) omega. + (* absurd *) lia. ++ (* absurd *) unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. - destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega. + destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. lia. + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. inversion UNFOLD as (UNFOLD'). apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). @@ -933,9 +925,9 @@ Proof. destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto. eexists; split. * apply IH_is_nth. - * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by omega. + * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by lia. eapply find_instr_bblock_tail; try assumption. - replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by omega. + replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by lia. apply IH_find_instr. + (* absurd *) generalize (Pos2Z.neg_is_neg p). intros. exploit (find_bblock_neg (b :: lb)); eauto. @@ -963,11 +955,11 @@ Proof. + (* header one *) assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. } exploit (find_instr_bblock 0); eauto. - { generalize (bblock_size_pos bb). omega. } + { generalize (bblock_size_pos bb). lia. } intros (i & NTH & FIND_INSTR). inv NTH. * rewrite EQhead in H; simpl in H. inv H. - replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by omega. + replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by lia. eexists. split. - eapply star_one. eapply Asm.exec_step_internal; eauto. @@ -975,12 +967,12 @@ Proof. - unfold list_length_z; simpl. split; eauto. intros r; destruct r; simpl; congruence || auto. * (* absurd case *) - erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega]. + erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; lia]. * (* absurd case *) - rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega. + rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). lia. + (* absurd case *) unfold list_length_z in BNDhead. simpl in *. - generalize (list_length_z_aux_increase _ l1 2); omega. + generalize (list_length_z_aux_increase _ l1 2); lia. Qed. Lemma eval_addressing_preserved a rs1 rs2: @@ -1406,57 +1398,18 @@ Proof. assert (tc' = tc) by congruence; subst. exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto. { unfold size; split. - - rewrite list_length_z_nat; omega. - - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. } + - rewrite list_length_z_nat; lia. + - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). lia. } intros (i & NTH & FIND_INSTR). exists i; intros. inv NTH. - - (* absurd *) apply list_nth_z_range in H; omega. + - (* absurd *) apply list_nth_z_range in H; lia. - exists bi; rewrite Z.add_simpl_l in H; rewrite Z.add_assoc in FIND_INSTR; intuition. - (* absurd *) rewrite bblock_size_aux in H0; - rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega. -Qed. - -(** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *) - -Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1). -Proof. - intros; eapply Machblockgenproof.is_tail_app_inv; econstructor. -Qed. - -Lemma is_tail_app_def A (l1 l2: list A): - is_tail l1 l2 -> exists l3, l2 = l3 ++ l1. -Proof. - induction 1 as [|x l1 l2]; simpl. - - exists nil; simpl; auto. - - destruct IHis_tail as (l3 & EQ); rewrite EQ. - exists (x::l3); simpl; auto. -Qed. - -Lemma is_tail_bound A (l1 l2: list A): - is_tail l1 l2 -> (length l1 <= length l2)%nat. -Proof. - intros H; destruct (is_tail_app_def _ _ _ H) as (l3 & EQ). - subst; rewrite app_length. - omega. -Qed. - -Lemma is_tail_list_nth_z A (l1 l2: list A): - is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0. -Proof. - induction 1; simpl. - - replace (list_length_z c - list_length_z c) with 0; omega || auto. - - assert (X: list_length_z (i :: c2) > list_length_z c1). - { rewrite !list_length_z_nat, <- Nat2Z.inj_gt. - exploit is_tail_bound; simpl; eauto. - omega. } - destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega. - replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto. - rewrite list_length_z_cons. - omega. + rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; lia. Qed. (* TODO: remplacer find_basic_instructions directement par ce lemme ? *) @@ -1474,9 +1427,9 @@ Lemma find_basic_instructions_alt b ofs f bb tc n: forall = Some i. Proof. intros; assert ((Z.to_nat n) < length (body bb))%nat. - { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try omega. } + { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try lia. } exploit find_basic_instructions; eauto. - rewrite Z2Nat.id; try omega. intros (i & bi & X). + rewrite Z2Nat.id; try lia. intros (i & bi & X). eexists; eexists; intuition eauto. Qed. @@ -1491,11 +1444,11 @@ Proof. assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos. assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. - assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega. + assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by lia. unfold size in BBSIZE. rewrite !Nat2Z.inj_add in BBSIZE. rewrite <- !list_length_z_nat in BBSIZE. - omega. + lia. Qed. (* A more general version of the exec_body_simulation_plus lemma below. @@ -1515,9 +1468,9 @@ Proof. induction li as [|a li]; simpl; try congruence. intros. assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). { - assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try omega. + assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try lia. rewrite !list_length_z_nat; split. - - rewrite <- Nat2Z.inj_lt. simpl. omega. + - rewrite <- Nat2Z.inj_lt. simpl. lia. - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto. } exploit internal_functions_unfold; eauto. @@ -1549,18 +1502,18 @@ Proof. exploit (Asm.exec_step_internal tge b); eauto. { rewrite Ptrofs.add_unsigned. - repeat (rewrite Ptrofs.unsigned_repr); try omega. + repeat (rewrite Ptrofs.unsigned_repr); try lia. 2: { assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size. assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. } - omega. } + lia. } try rewrite list_length_z_nat; try split; simpl; rewrite <- !list_length_z_nat; replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) + - (list_length_z (body bb) - list_length_z (a :: li))) by omega; - try assumption; try omega. } + (list_length_z (body bb) - list_length_z (a :: li))) by lia; + try assumption; try lia. } (* This is our STEP hypothesis. *) intros STEP_NEXT. @@ -1574,18 +1527,18 @@ Proof. apply f_equal. apply f_equal. rewrite bblock_size_aux, list_length_z_cons; simpl. - omega. + lia. - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto. + exploit is_tail_app_def; eauto. intros (l3 & EQ); rewrite EQ. - exploit (is_tail_app_right _ (l3 ++ a::nil)). + exploit (is_tail_app_right (l3 ++ a::nil)). rewrite <- app_assoc; simpl; eauto. + constructor; auto. rewrite ATPC_NEXT. apply f_equal. apply f_equal. rewrite! list_length_z_cons; simpl. - omega. + lia. + intros (s2' & LAST_STEPS & LAST_MATCHS). eexists. split; eauto. eapply plus_left'; eauto. @@ -1605,7 +1558,7 @@ Proof. exploit exec_body_simulation_plus_gen; eauto. - constructor. - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto. - omega. + lia. Qed. Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall @@ -1623,7 +1576,7 @@ Proof. eexists. split. eapply star_refl; eauto. assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)). - { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. omega. } + { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. lia. } rewrite EQ; eauto. - exploit exec_body_simulation_plus; congruence || eauto. { rewrite Hbb; eauto. } @@ -1639,7 +1592,7 @@ Proof. intros N. remember (list_nth_z l n) as opt eqn:H. symmetry in H. destruct opt; auto. - exploit list_nth_z_range; eauto. omega. + exploit list_nth_z_range; eauto. lia. Qed. Lemma label_in_header_list lbl a: @@ -1651,9 +1604,9 @@ Proof. - eapply in_nil in H. contradiction. - rewrite list_length_z_cons in H0. assert (list_length_z l0 >= 0) by eapply list_length_z_pos. - assert (list_length_z l0 = 0) by omega. + assert (list_length_z l0 = 0) by lia. rewrite list_length_z_nat in H2. - assert (Datatypes.length l0 = 0%nat) by omega. + assert (Datatypes.length l0 = 0%nat) by lia. eapply length_zero_iff_nil in H3. subst. unfold In in H. destruct H. + subst; eauto. @@ -1684,7 +1637,7 @@ Proof. - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *. erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto. erewrite Zpos_P_of_succ_nat. - apply f_equal2; auto. omega. + apply f_equal2; auto. lia. Qed. Lemma asm_label_pos_header: forall z a x0 x1 lbl @@ -1696,7 +1649,7 @@ Proof. unfold size. rewrite <- plus_assoc. rewrite Nat2Z.inj_add. rewrite list_length_z_nat. - replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega. + replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by lia. eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. Qed. @@ -1707,8 +1660,8 @@ Proof. intros. destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE. assert (list_length_z l1 >= 0) by eapply list_length_z_pos. - assert (list_length_z l1 + 1 + 1 >= 2) by omega. - assert (2 <= 1) by omega. contradiction H1. omega. + assert (list_length_z l1 + 1 + 1 >= 2) by lia. + assert (2 <= 1) by lia. contradiction H1. lia. Qed. Lemma label_pos_preserved_gen bbs: forall lbl c z @@ -1727,7 +1680,7 @@ Proof. unfold is_label in *. destruct (header a). * replace (z + list_length_z (@nil label)) with (z); eauto. - unfold list_length_z. simpl. omega. + unfold list_length_z. simpl. lia. * eapply header_size_cons_nil in l as HL1. subst. simpl in *. destruct (in_dec _ _); try congruence. simpl in *. @@ -1782,7 +1735,7 @@ Proof. intros; simpl in *; unfold incrPC in NEXT; inv_matchi; assert (size bb >= 1) by eapply bblock_size_pos; - assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega; + assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by lia; inversion NEXT; subst; eexists; eexists; split; eauto. assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). { @@ -1790,9 +1743,9 @@ Proof. intros x. destruct (PregEq.eq x PC). -- unfold Asm.nextinstr. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned. - rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. rewrite Ptrofs.unsigned_one. - replace (size bb - 1 + 1) with (size bb) by omega. + replace (size bb - 1 + 1) with (size bb) by lia. rewrite e. rewrite Pregmap.gss. reflexivity. -- eapply nextinstr_agree_but_pc; eauto. } @@ -1850,8 +1803,8 @@ Proof. * rewrite symbol_addresses_preserved. reflexivity. * destruct (PregEq.eq x X30). -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. - unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try omega. - replace (size bb - 1 + 1) with (size bb) by omega. reflexivity. + unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try lia. + replace (size bb - 1 + 1) with (size bb) by lia. reflexivity. -- inv MATCHI; rewrite AG; try assumption; reflexivity. } rewrite EQRS; inv MATCHI; reflexivity. - (* Pbs *) @@ -1877,7 +1830,7 @@ Proof. - destruct (PregEq.eq x X30) as [X' | X']. + inversion MATCHI; subst. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. unfold Ptrofs.one. - rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try omega. rewrite Ptrofs.unsigned_repr; try omega. + rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try lia. rewrite Ptrofs.unsigned_repr; try lia. rewrite Z.sub_add; reflexivity. + inv_matchi. } rewrite EQRS. inv_matchi. @@ -1961,10 +1914,10 @@ Lemma last_instruction_cannot_be_label bb: list_nth_z (header bb) (size bb - 1) = None. Proof. assert (list_length_z (header bb) <= size bb - 1). { - rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega. + rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). lia. } remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto; - exploit list_nth_z_range; eauto; omega. + exploit list_nth_z_range; eauto; lia. Qed. Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m @@ -1993,8 +1946,8 @@ Proof. with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. unfold Ptrofs.add. - rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. - rewrite Ptrofs.unsigned_repr; omega. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try lia. + rewrite Ptrofs.unsigned_repr; lia. Qed. Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1 @@ -2127,7 +2080,7 @@ Proof. intros (tc & FINDtf & TRANStf & _). exploit (find_instr_bblock (size bb - 1)); eauto. - { generalize (bblock_size_pos bb). omega. } + { generalize (bblock_size_pos bb). lia. } intros (i' & NTH & FIND_INSTR). inv NTH. @@ -2136,12 +2089,12 @@ Proof. rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *. (* XXX: Is there a better way to simplify this expression i.e. automatically? *) replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 - - list_length_z (header bb)) with (list_length_z (body bb)) in H by omega. - rewrite list_nth_z_range_exceeded in H; try omega. discriminate. + list_length_z (header bb)) with (list_length_z (body bb)) in H by lia. + rewrite list_nth_z_range_exceeded in H; try lia. discriminate. + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). { eapply size_of_blocks_bounds; eauto. } - assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. } + assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); lia. } destruct cfi. * (* control flow instruction *) destruct s2. @@ -2179,9 +2132,9 @@ Proof. { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. rewrite Ptrofs.add_assoc. unfold Ptrofs.add. assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. - rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. rewrite Ptrofs.unsigned_one. - replace (size bb - 1 + 1) with (size bb) by omega. + replace (size bb - 1 + 1) with (size bb) by lia. reflexivity. } apply set_builtin_res_dont_move_pc_gen. -- erewrite !set_builtin_map_not_pc. @@ -2216,7 +2169,7 @@ Proof. apply functional_extensionality. intros x. destruct (PregEq.eq x PC) as [X|]. - rewrite X. rewrite <- AGPC. simpl. - replace (size bb - 0) with (size bb) by omega. reflexivity. + replace (size bb - 0) with (size bb) by lia. reflexivity. - rewrite AG; try assumption. reflexivity. } destruct X. diff --git a/common/Values.v b/common/Values.v index 41138e8e..4146dd59 100644 --- a/common/Values.v +++ b/common/Values.v @@ -2613,6 +2613,55 @@ Qed. End VAL_INJ_OPS. +(* Specializations of cmpu_bool, cmpu, cmplu_bool, and cmplu for maximal pointer validity *) + +Definition mxcmpu_bool cmp v1 v2: option bool := + cmpu_bool (fun _ _ => true) cmp v1 v2. + +Lemma mxcmpu_bool_correct vptr (cmp: comparison) (v1 v2: val) b: + cmpu_bool vptr cmp v1 v2 = Some b + -> mxcmpu_bool cmp v1 v2 = Some b. +Proof. + intros; eapply cmpu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition mxcmpu cmp v1 v2 := of_optbool (mxcmpu_bool cmp v1 v2). + +Lemma mxcmpu_correct vptr (cmp: comparison) (v1 v2: val): + lessdef (cmpu vptr cmp v1 v2) (mxcmpu cmp v1 v2). +Proof. + unfold cmpu, mxcmpu. + remember (cmpu_bool _ cmp v1 v2) as ob. + destruct ob; simpl. + - erewrite mxcmpu_bool_correct; eauto. + econstructor. + - econstructor. +Qed. + +Definition mxcmplu_bool (cmp: comparison) (v1 v2: val) + := (cmplu_bool (fun _ _ => true) cmp v1 v2). + +Lemma mxcmplu_bool_correct vptr (cmp: comparison) (v1 v2: val) b: + (cmplu_bool vptr cmp v1 v2) = Some b + -> (mxcmplu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply cmplu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition mxcmplu cmp v1 v2 := of_optbool (mxcmplu_bool cmp v1 v2). + +Lemma mxcmplu_correct vptr (cmp: comparison) (v1 v2: val): + lessdef (maketotal (cmplu vptr cmp v1 v2)) + (mxcmplu cmp v1 v2). +Proof. + unfold cmplu, mxcmplu. + remember (cmplu_bool _ cmp v1 v2) as ob. + destruct ob as [b|]; simpl. + - erewrite mxcmplu_bool_correct; eauto. + simpl. econstructor. + - econstructor. +Qed. + End Val. Notation meminj := Val.meminj. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 16d880fa..7a7261a3 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1053,6 +1053,41 @@ Proof. induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto. Qed. +Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). +Proof. + induction l1; cbn; auto with coqlib. +Qed. +Hint Resolve is_tail_app: coqlib. + +Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. +Proof. + induction l1; cbn; auto with coqlib. + intros l2 l3 H; inversion H; eauto with coqlib. +Qed. +Hint Resolve is_tail_app_inv: coqlib. + +Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1). +Proof. + intros; eauto with coqlib. +Qed. + +Lemma is_tail_app_def A (l1 l2: list A): + is_tail l1 l2 -> exists l3, l2 = l3 ++ l1. +Proof. + induction 1 as [|x l1 l2]; simpl. + - exists nil; simpl; auto. + - destruct IHis_tail as (l3 & EQ); rewrite EQ. + exists (x::l3); simpl; auto. +Qed. + +Lemma is_tail_bound A (l1 l2: list A): + is_tail l1 l2 -> (length l1 <= length l2)%nat. +Proof. + intros H; destruct (is_tail_app_def H) as (l3 & EQ). + subst; rewrite app_length. + omega. +Qed. + (** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and [P xi yi] holds for all [i]. *) diff --git a/lib/IterList.v b/lib/IterList.v index 49beb1c5..bde47068 100644 --- a/lib/IterList.v +++ b/lib/IterList.v @@ -94,3 +94,18 @@ Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_ Proof. intros; rewrite list_length_z_nat, Nat2Z.id. auto. Qed. + +Lemma is_tail_list_nth_z A (l1 l2: list A): + is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0. +Proof. + induction 1; simpl. + - replace (list_length_z c - list_length_z c) with 0; omega || auto. + - assert (X: list_length_z (i :: c2) > list_length_z c1). + { rewrite !list_length_z_nat, <- Nat2Z.inj_gt. + exploit is_tail_bound; simpl; eauto. + omega. } + destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega. + replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto. + rewrite list_length_z_cons. + omega. +Qed. diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v index fc722887..d121a54b 100644 --- a/scheduling/postpass_lib/Machblockgenproof.v +++ b/scheduling/postpass_lib/Machblockgenproof.v @@ -190,7 +190,7 @@ Proof. intros H H0 H1. unfold find_label. remember (is_label l _) as b. - cutrewrite (b = false); auto. + replace b with false; auto. subst; unfold is_label. destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). inversion H. @@ -286,7 +286,7 @@ Lemma find_label_preserved: Mach.find_label l (Mach.fn_code f) = Some c -> exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)). Proof. - intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto. + intros. replace (fn_code (transf_function f)) with (trans_code (Mach.fn_code f)); eauto. apply find_label_transcode_preserved; auto. Qed. @@ -661,7 +661,7 @@ Proof. inversion H1; subst; clear H1. inversion_clear H0; cbn. - (* function_internal*) - cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. + replace (trans_code (Mach.fn_code f0)) with (fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. rewrite <- parent_sp_preserved; eauto. rewrite <- parent_ra_preserved; eauto. @@ -733,12 +733,12 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + - (*i=lbl *) replace (i ) with (Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). exists nil; cbn; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. - cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. + replace ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. @@ -748,7 +748,7 @@ Proof. - (*i=cfi*) destruct i; try(cbn in Heqti; congruence). all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; - cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; + replace ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; rewrite Heqti; eapply Tr_end_block; eauto; rewrite <-Heqti; @@ -765,21 +765,6 @@ Proof. eauto. Qed. -(* FIXME: these two lemma should go into [Coqlib.v] *) -Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). -Proof. - induction l1; cbn; auto with coqlib. -Qed. -Hint Resolve is_tail_app: coqlib. - -Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. -Proof. - induction l1; cbn; auto with coqlib. - intros l2 l3 H; inversion H; eauto with coqlib. -Qed. -Hint Resolve is_tail_app_inv: coqlib. - - Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> exists b, is_tail (b :: trans_code c) (trans_code c2). Proof. -- cgit