diff options
Diffstat (limited to 'backend')
32 files changed, 331 insertions, 268 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 3ac99a47..cf62295d 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -404,11 +404,11 @@ Module OrderedEquation <: OrderedType. (OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. @@ -466,11 +466,11 @@ Module OrderedEquation' <: OrderedType. (Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 29dbcbe8..585fb0da 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2445,7 +2445,7 @@ Proof. (* internal function *) - monadInv FUN. simpl in *. destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl. intros [m'' [U V]]. assert (WTRS: wt_regset env (init_regs args (fn_params f))). { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 53ecf73a..f6f03868 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -103,7 +103,7 @@ Lemma nextinstr_set_preg: (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one. Proof. intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. + rewrite Pregmap.gso. auto. apply not_eq_sym. apply preg_of_not_PC. Qed. Lemma undef_regs_other: @@ -211,7 +211,7 @@ Lemma agree_set_mreg: agree (Regmap.set r v ms) sp rs'. Proof. intros. destruct H. split; auto. - rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP. + rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP. intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. rewrite H1. auto. apply preg_of_data. red; intros; elim n. eapply preg_of_injective; eauto. @@ -285,6 +285,23 @@ Proof. exploit preg_of_injective; eauto. congruence. Qed. +Lemma agree_undef_regs2: + forall ms sp rl rs rs', + agree (Mach.undef_regs rl ms) sp rs -> + (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> + agree (Mach.undef_regs rl ms) sp rs'. +Proof. + intros. destruct H. split; auto. + rewrite <- agree_sp0. apply H0; auto. + rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. + intros. destruct (In_dec mreg_eq r rl). + rewrite Mach.undef_regs_same; auto. + rewrite H0; auto. + apply preg_of_data. + rewrite preg_notin_charact. intros; red; intros. elim n. + exploit preg_of_injective; eauto. congruence. +Qed. + Lemma agree_set_undef_mreg: forall ms sp rs r v rl rs', agree ms sp rs -> @@ -738,6 +755,18 @@ Ltac TailNoLabel := | _ => idtac end. +Remark tail_nolabel_find_label: + forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k. +Proof. + intros. destruct H. auto. +Qed. + +Remark tail_nolabel_is_tail: + forall k c, tail_nolabel k c -> is_tail k c. +Proof. + intros. destruct H. auto. +Qed. + (** * Execution of straight-line code *) Section STRAIGHTLINE. diff --git a/backend/Bounds.v b/backend/Bounds.v index 93a4b504..fa695234 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -136,7 +136,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := end. Definition max_over_list {A: Type} (valu: A -> Z) (l: list A) : Z := - List.fold_left (fun m l => Zmax m (valu l)) l 0. + List.fold_left (fun m l => Z.max m (valu l)) l 0. Definition max_over_instrs (valu: instruction -> Z) : Z := max_over_list valu f.(fn_code). @@ -161,10 +161,10 @@ Lemma max_over_list_pos: max_over_list valu l >= 0. Proof. intros until valu. unfold max_over_list. - assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z). + assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z). induction l; simpl; intros. - omega. apply Zge_trans with (Zmax z (valu a)). - auto. apply Zle_ge. apply Zmax1. auto. + omega. apply Zge_trans with (Z.max z (valu a)). + auto. apply Z.le_ge. apply Z.le_max_l. auto. Qed. Lemma max_over_slots_of_funct_pos: @@ -225,18 +225,18 @@ Qed. Program Definition function_bounds := {| used_callee_save := RegSet.elements record_regs_of_function; bound_local := max_over_slots_of_funct local_slot; - bound_outgoing := Zmax (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot); - bound_stack_data := Zmax f.(fn_stacksize) 0 + bound_outgoing := Z.max (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot); + bound_stack_data := Z.max f.(fn_stacksize) 0 |}. Next Obligation. apply max_over_slots_of_funct_pos. Qed. Next Obligation. - apply Zle_ge. eapply Zle_trans. 2: apply Zmax2. - apply Zge_le. apply max_over_slots_of_funct_pos. + apply Z.le_ge. eapply Z.le_trans. 2: apply Z.le_max_r. + apply Z.ge_le. apply max_over_slots_of_funct_pos. Qed. Next Obligation. - apply Zle_ge. apply Zmax2. + apply Z.le_ge. apply Z.le_max_r. Qed. Next Obligation. generalize (RegSet.elements_3w record_regs_of_function). @@ -304,15 +304,15 @@ Lemma max_over_list_bound: Proof. intros until x. unfold max_over_list. assert (forall c z, - let f := fold_left (fun x y => Zmax x (valu y)) c z in + let f := fold_left (fun x y => Z.max x (valu y)) c z in z <= f /\ (In x c -> valu x <= f)). induction c; simpl; intros. split. omega. tauto. - elim (IHc (Zmax z (valu a))); intros. - split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto. + elim (IHc (Z.max z (valu a))); intros. + split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto. intro H1; elim H1; intro. - subst a. apply Zle_trans with (Zmax z (valu x)). - apply Zmax2. auto. auto. + subst a. apply Z.le_trans with (Z.max z (valu x)). + apply Z.le_max_r. auto. auto. intro. elim (H l 0); intros. auto. Qed. @@ -329,7 +329,7 @@ Lemma max_over_slots_of_funct_bound: valu s <= max_over_slots_of_funct valu. Proof. intros. unfold max_over_slots_of_funct. - apply Zle_trans with (max_over_slots_of_instr valu i). + apply Z.le_trans with (max_over_slots_of_instr valu i). unfold max_over_slots_of_instr. apply max_over_list_bound. auto. apply max_over_instrs_bound. auto. Qed. @@ -447,9 +447,9 @@ Proof. Local Opaque mreg_type. induction l as [ | r l]; intros; simpl. - omega. -- eapply Zle_trans. 2: apply IHl. +- eapply Z.le_trans. 2: apply IHl. generalize (AST.typesize_pos (mreg_type r)); intros. - apply Zle_trans with (align ofs (AST.typesize (mreg_type r))). + apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))). apply align_le; auto. omega. Qed. diff --git a/backend/CSE.v b/backend/CSE.v index 4fa1bd6c..6d3f6f33 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -50,7 +50,7 @@ Definition valnum_reg (n: numbering) (r: reg) : numbering * valnum := | Some v => (n, v) | None => let v := n.(num_next) in - ( {| num_next := Psucc v; + ( {| num_next := Pos.succ v; num_eqs := n.(num_eqs); num_reg := PTree.set r v n.(num_reg); num_val := PMap.set v (r :: nil) n.(num_val) |}, @@ -161,7 +161,7 @@ Definition add_rhs (n: numbering) (rd: reg) (rh: rhs) : numbering := num_reg := PTree.set rd vres n.(num_reg); num_val := update_reg n rd vres |} | None => - {| num_next := Psucc n.(num_next); + {| num_next := Pos.succ n.(num_next); num_eqs := Eq n.(num_next) true rh :: n.(num_eqs); num_reg := PTree.set rd n.(num_next) n.(num_reg); num_val := update_reg n rd n.(num_next) |} @@ -331,7 +331,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) := let j := i + delta in if zle src i && zle (i + size_chunk chunk) (src + sz) - && zeq (Zmod delta (align_chunk chunk)) 0 + && zeq (Z.modulo delta (align_chunk chunk)) 0 && zle 0 j && zle j Ptrofs.max_unsigned then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil)) @@ -486,7 +486,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ | EF_annot_val _ _ | EF_debug _ _ _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ => set_res_unknown before res end | Icond cond args ifso ifnot => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 8516e384..d6bde348 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -35,8 +35,8 @@ Remark wf_equation_incr: wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e. Proof. unfold wf_equation; intros; destruct e. destruct H. split. - apply Plt_le_trans with next1; auto. - red; intros. apply Plt_le_trans with next1; auto. apply H1; auto. + apply Pos.lt_le_trans with next1; auto. + red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto. Qed. (** Extensionality with respect to valuations. *) @@ -95,7 +95,7 @@ Proof. - auto. - apply equation_holds_exten. auto. eapply wf_equation_incr; eauto with cse. -- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. +- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto. Qed. End EXTEN. @@ -523,7 +523,7 @@ Proof. exists valu3. constructor; simpl; intros. + constructor; simpl; intros; eauto with cse. destruct H4; eauto with cse. subst e. split. - eapply Plt_le_trans; eauto. + eapply Pos.lt_le_trans; eauto. red; simpl; intros. auto. + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src). apply load_eval_to with a. rewrite <- Q; auto. @@ -1187,7 +1187,7 @@ Proof. - (* internal function *) monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ. destruct (analyze cu f) as [approx|] eqn:?; inv EQ. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros (m'' & A & B). econstructor; split. eapply exec_function_internal; simpl; eauto. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b14c4be0..e28519ca 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -493,7 +493,7 @@ Opaque builtin_strength_reduction. assert (C: cmatch (eval_condition cond rs ## args m) ac) by (eapply eval_static_condition_sound; eauto with va). rewrite H0 in C. - generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)). + generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (eq_refl _)). destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args']. intros EV1 TCODE. left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'); split. @@ -532,7 +532,7 @@ Opaque builtin_strength_reduction. destruct or; simpl; auto. - (* internal function *) - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. simpl. unfold transf_function. left; exists O; econstructor; split. diff --git a/backend/Deadcode.v b/backend/Deadcode.v index f491d678..2286876e 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -102,7 +102,7 @@ Function transfer_builtin (app: VA.t) (ef: external_function) nmem_add (nmem_remove nm (aaddr_arg app dst) sz) (aaddr_arg app src) sz) args else (ne, nm) - | (EF_annot _ _ | EF_annot_val _ _), _ => + | (EF_annot _ _ _ | EF_annot_val _ _ _), _ => transfer_builtin_args (kill_builtin_res res ne, nm) args | EF_debug _ _ _, _ => (kill_builtin_res res ne, nm) @@ -143,7 +143,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) | Some(Ibuiltin ef args res s) => transfer_builtin approx!!pc ef args res ne nm | Some(Icond cond args s1 s2) => - (add_needs args (needs_of_condition cond) ne, nm) + if peq s1 s2 then after else + (add_needs args (needs_of_condition cond) ne, nm) | Some(Ijumptable arg tbl) => (add_need_all arg ne, nm) | Some(Ireturn optarg) => @@ -191,6 +192,8 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) if nmem_contains (snd an!!pc) (aaddr_arg approx!!pc dst) sz then instr else Inop s + | Icond cond args s1 s2 => + if peq s1 s2 then Inop s1 else instr | _ => instr end. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 28ca27fa..199ac922 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -70,7 +70,7 @@ Proof. - replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. - eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. - rewrite Zplus_0_r. auto. + rewrite Z.add_0_r. auto. - auto. Qed. @@ -80,9 +80,9 @@ Lemma magree_extends: magree m1 m2 P -> Mem.extends m1 m2. Proof. intros. destruct H0. constructor; auto. constructor; unfold inject_id; intros. -- inv H0. rewrite Zplus_0_r. eauto. -- inv H0. apply Zdivide_0. -- inv H0. rewrite Zplus_0_r. eapply ma_memval0; eauto. +- inv H0. rewrite Z.add_0_r. eauto. +- inv H0. apply Z.divide_0_r. +- inv H0. rewrite Z.add_0_r. eapply ma_memval0; eauto. Qed. Lemma magree_loadbytes: @@ -98,7 +98,7 @@ Proof. { induction n; intros; simpl. constructor. - rewrite inj_S in H. constructor. + rewrite Nat2Z.inj_succ in H. constructor. apply H. omega. apply IHn. intros; apply H; omega. } @@ -132,7 +132,7 @@ Lemma magree_storebytes_parallel: magree m1 m2 P -> Mem.storebytes m1 b ofs bytes1 = Some m1' -> (forall b' i, Q b' i -> - b' <> b \/ i < ofs \/ ofs + Z_of_nat (length bytes1) <= i -> + b' <> b \/ i < ofs \/ ofs + Z.of_nat (length bytes1) <= i -> P b' i) -> list_forall2 memval_lessdef bytes1 bytes2 -> exists m2', Mem.storebytes m2 b ofs bytes2 = Some m2' /\ magree m1' m2' Q. @@ -147,7 +147,7 @@ Proof. { induction 1; intros; simpl. - apply H; auto. simpl. omega. - - simpl length in H1; rewrite inj_S in H1. + - simpl length in H1; rewrite Nat2Z.inj_succ in H1. apply IHlist_forall2; auto. intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto. apply H1; auto. unfold ZIndexed.t in *; omega. @@ -201,7 +201,7 @@ Lemma magree_storebytes_left: forall m1 m2 P b ofs bytes1 m1', magree m1 m2 P -> Mem.storebytes m1 b ofs bytes1 = Some m1' -> - (forall i, ofs <= i < ofs + Z_of_nat (length bytes1) -> ~(P b i)) -> + (forall i, ofs <= i < ofs + Z.of_nat (length bytes1) -> ~(P b i)) -> magree m1' m2 P. Proof. intros. constructor; intros. @@ -995,7 +995,7 @@ Ltac UseTransfer := erewrite Mem.loadbytes_length in H0 by eauto. rewrite nat_of_Z_eq in H0 by omega. auto. + (* annot *) - destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. @@ -1007,7 +1007,7 @@ Ltac UseTransfer := eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* annot val *) - destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. inv B. inv H6. @@ -1047,8 +1047,12 @@ Ltac UseTransfer := eapply mextends_agree; eauto. - (* conditional *) - TransfInstr; UseTransfer. + TransfInstr; UseTransfer. destruct (peq ifso ifnot). ++ replace (if b then ifso else ifnot) with ifso by (destruct b; congruence). econstructor; split. + eapply exec_Inop; eauto. + eapply match_succ_states; eauto. simpl; auto. ++ econstructor; split. eapply exec_Icond; eauto. eapply needs_of_condition_sound. eapply ma_perm; eauto. eauto. eauto with na. eapply match_succ_states; eauto 2 with na. @@ -1078,7 +1082,7 @@ Ltac UseTransfer := - (* internal function *) monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'. destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros (tm' & A & B). econstructor; split. econstructor; simpl; eauto. diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index 0b8ff3c7..d31c63ec 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -157,11 +157,11 @@ Proof. - intuition congruence. - destruct (Pos.compare_spec v v0); simpl in H1. + subst v0. destruct H1. inv H1; auto. right; split. - apply sym_not_equal. apply Plt_ne. eapply H; eauto. + apply not_eq_sym. apply Plt_ne. eapply H; eauto. auto. + destruct H1. inv H1; auto. - destruct H1. inv H1. right; split; auto. apply sym_not_equal. apply Plt_ne. auto. - right; split; auto. apply sym_not_equal. apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. right; split; auto. apply not_eq_sym. apply Plt_ne. auto. + right; split; auto. apply not_eq_sym. apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. right; split; auto. apply Plt_ne. auto. destruct IHwf_avail as [A | [A B]]; auto. Qed. @@ -211,9 +211,9 @@ Proof. induction 1; simpl; intros. - contradiction. - destruct (Pos.compare_spec v v0); simpl in H1. -+ subst v0. split; auto. apply sym_not_equal; apply Plt_ne; eauto. -+ destruct H1. inv H1. split; auto. apply sym_not_equal; apply Plt_ne; eauto. - split; auto. apply sym_not_equal; apply Plt_ne. apply Plt_trans with v0; eauto. ++ subst v0. split; auto. apply not_eq_sym; apply Plt_ne; eauto. ++ destruct H1. inv H1. split; auto. apply not_eq_sym; apply Plt_ne; eauto. + split; auto. apply not_eq_sym; apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. split; auto. apply Plt_ne; auto. destruct IHwf_avail as [A B] ; auto. Qed. diff --git a/backend/Inlining.v b/backend/Inlining.v index 17139dbd..91cc119d 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -113,7 +113,7 @@ Program Definition add_instr (i: instruction): mon node := fun s => let pc := s.(st_nextnode) in R pc - (mkstate s.(st_nextreg) (Psucc pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) + (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -122,7 +122,7 @@ Qed. Program Definition reserve_nodes (numnodes: positive): mon positive := fun s => R s.(st_nextnode) - (mkstate s.(st_nextreg) (Pplus s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) + (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -131,7 +131,7 @@ Qed. Program Definition reserve_regs (numregs: positive): mon positive := fun s => R s.(st_nextreg) - (mkstate (Pplus s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) + (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -140,7 +140,7 @@ Qed. Program Definition request_stack (sz: Z): mon unit := fun s => R tt - (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Zmax s.(st_stksize) sz)) + (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -181,7 +181,7 @@ Record context: Type := mkcontext { (** The following functions "shift" (relocate) PCs, registers, operations, etc. *) -Definition shiftpos (p amount: positive) := Ppred (Pplus p amount). +Definition shiftpos (p amount: positive) := Pos.pred (Pos.add p amount). Definition spc (ctx: context) (pc: node) := shiftpos pc ctx.(dpc). @@ -220,7 +220,7 @@ Definition initcontext (dpc dreg nreg: positive) (sz: Z) := dreg := dreg; dstk := 0; mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := None |}. (** The context used to inline a call to another function. *) @@ -237,7 +237,7 @@ Definition callcontext (ctx: context) dreg := dreg; dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz); mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := Some (spc ctx retpc, sreg ctx retreg) |}. (** The context used to inline a tail call to another function. *) @@ -247,7 +247,7 @@ Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) := dreg := dreg; dstk := align ctx.(dstk) (min_alignment sz); mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := ctx.(retinfo) |}. (** ** Recursive expansion and copying of a CFG *) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index c3b0cfc3..2dcb8956 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -184,7 +184,7 @@ Proof. unfold agree_regs; intros. destruct H. split; intros. rewrite H0. auto. apply shiftpos_above. - eapply Plt_le_trans. apply shiftpos_below. xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. xomega. apply H1; auto. Qed. @@ -242,7 +242,7 @@ Proof. split. destruct H3 as [[P Q] | [P Q]]. subst a1. eapply agree_set_reg_undef; eauto. eapply agree_set_reg; eauto. rewrite C; auto. apply context_below_lt; auto. - intros. rewrite Regmap.gso. auto. apply sym_not_equal. eapply sreg_below_diff; eauto. + intros. rewrite Regmap.gso. auto. apply not_eq_sym. eapply sreg_below_diff; eauto. destruct H2; discriminate. Qed. @@ -290,10 +290,10 @@ Lemma range_private_alloc_left: Mem.alloc m 0 sz = (m1, sp) -> F1 sp = Some(sp', base) -> (forall b, b <> sp -> F1 b = F b) -> - range_private F1 m1 m' sp' (base + Zmax sz 0) hi. + range_private F1 m1 m' sp' (base + Z.max sz 0) hi. Proof. intros; red; intros. - exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B]. + exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B]. split; auto. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b sp); intros. @@ -304,14 +304,14 @@ Qed. Lemma range_private_free_left: forall F m m' sp base sz hi b m1, - range_private F m m' sp (base + Zmax sz 0) hi -> + range_private F m m' sp (base + Z.max sz 0) hi -> Mem.free m b 0 sz = Some m1 -> F b = Some(sp, base) -> Mem.inject F m m' -> range_private F m1 m' sp base hi. Proof. intros; red; intros. - destruct (zlt ofs (base + Zmax sz 0)) as [z|z]. + destruct (zlt ofs (base + Z.max sz 0)) as [z|z]. red; split. replace ofs with ((ofs - base) + base) by omega. eapply Mem.perm_inject; eauto. @@ -560,8 +560,8 @@ Lemma match_stacks_bound: Proof. intros. inv H. apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto. - eapply match_stacks_cons; eauto. eapply Plt_le_trans; eauto. - eapply match_stacks_untailcall; eauto. eapply Plt_le_trans; eauto. + eapply match_stacks_cons; eauto. eapply Pos.lt_le_trans; eauto. + eapply match_stacks_untailcall; eauto. eapply Pos.lt_le_trans; eauto. Qed. Variable F1: meminj. @@ -602,7 +602,7 @@ Proof. (* nil *) apply match_stacks_nil with (bound1 := bound1). inv MG. constructor; auto. - intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto. + intros. apply IMAGE with delta. eapply INJ; eauto. eapply Pos.lt_le_trans; eauto. auto. auto. (* cons *) apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto. @@ -768,8 +768,8 @@ Proof. destruct (zle sz 4). omegaContradiction. auto. destruct chunk; simpl in *; auto. - apply Zone_divide. - apply Zone_divide. + apply Z.divide_1_l. + apply Z.divide_1_l. apply H2; omega. apply H2; omega. Qed. @@ -845,7 +845,7 @@ Proof. intros. inv H. (* base *) eapply match_stacks_inside_base; eauto. congruence. - rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Zdivide_0. + rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Z.divide_0_r. (* inlined *) assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos. eapply match_stacks_inside_inlined; eauto. @@ -1164,7 +1164,7 @@ Proof. assert (TR: tr_function prog f f'). { eapply tr_function_linkorder; eauto. } inversion TR; subst. - exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. + exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. instantiate (1 := fn_stacksize f'). inv H1. xomega. intros [F' [m1' [sp' [A [B [C [D E]]]]]]]. left; econstructor; split. @@ -1203,7 +1203,7 @@ Proof. (* sp' is valid *) instantiate (1 := sp'). auto. (* offset is representable *) - instantiate (1 := dstk ctx). generalize (Zmax2 (fn_stacksize f) 0). omega. + instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega. (* size of target block is representable *) intros. right. exploit SSZ2; eauto with mem. inv FB; omega. (* we have full permissions on sp' at and above dstk ctx *) diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index d79132d6..6e8a94a6 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -105,7 +105,7 @@ Proof. Qed. Lemma shiftpos_below: - forall x n, Plt (shiftpos x n) (Pplus x n). + forall x n, Plt (shiftpos x n) (Pos.add x n). Proof. intros. unfold Plt; zify. rewrite shiftpos_eq. omega. Qed. @@ -250,7 +250,7 @@ Section INLINING_SPEC. Variable fenv: funenv. Definition context_below (ctx1 ctx2: context): Prop := - Ple (Pplus ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg). + Ple (Pos.add ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg). Definition context_stack_call (ctx1 ctx2: context): Prop := ctx1.(mstk) >= 0 /\ ctx1.(dstk) + ctx1.(mstk) <= ctx2.(dstk). @@ -331,7 +331,7 @@ with tr_funbody: context -> function -> code -> Prop := | tr_funbody_intro: forall ctx f c, (forall r, In r f.(fn_params) -> Ple r ctx.(mreg)) -> (forall pc i, f.(fn_code)!pc = Some i -> tr_instr ctx pc i c) -> - ctx.(mstk) = Zmax f.(fn_stacksize) 0 -> + ctx.(mstk) = Z.max f.(fn_stacksize) 0 -> (min_alignment f.(fn_stacksize) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> ctx.(dstk) + ctx.(mstk) <= stacksize -> tr_funbody ctx f c. @@ -451,9 +451,9 @@ Hypothesis rec_spec: fenv_agree fe' -> Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_reg_function f -> - Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> + Ple (Pos.add ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -599,7 +599,7 @@ Proof. elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto. (* older pc *) inv_incr. eapply IHl; eauto. - intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega. + intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega. intros; eapply Ple_trans; eauto. intros. apply H7; auto. xomega. Qed. @@ -611,7 +611,7 @@ Lemma expand_cfg_rec_spec: ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -629,13 +629,13 @@ Proof. intros. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Plt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. subst s0; simpl; auto. intros. apply H8; auto. subst s0; simpl in H11; xomega. intros. apply H8. apply shiftpos_above. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega. apply PTree.elements_correct; auto. auto. auto. auto. inversion INCR0. subst s0; simpl in STKSIZE; xomega. @@ -664,7 +664,7 @@ Lemma expand_cfg_spec: ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -724,7 +724,7 @@ Opaque initstate. unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega. simpl. xomega. - simpl. apply Zdivide_0. + simpl. apply Z.divide_0_r. simpl. omega. simpl. omega. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. diff --git a/backend/Kildall.v b/backend/Kildall.v index a2b49d56..8e712c05 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1373,7 +1373,7 @@ Proof. replace (st1.(aval)!!pc) with res!!pc. fold l. destruct (basic_block_map s) eqn:BB. rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. - elim (C H0 (refl_equal _)). intros X Y. rewrite Y. apply L.refl_ge. + elim (C H0 (eq_refl _)). intros X Y. rewrite Y. apply L.refl_ge. elim (U pc); intros E F. rewrite F. reflexivity. destruct (In_dec peq pc (successors instr)). right. eapply no_self_loop; eauto. diff --git a/backend/Locations.v b/backend/Locations.v index ca148761..c437df5d 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -471,11 +471,11 @@ Module OrderedLoc <: OrderedType. (ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2))) end. Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. @@ -542,12 +542,12 @@ Module OrderedLoc <: OrderedType. intros. destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto. - assert (IndexedMreg.index mr <> IndexedMreg.index mr'). - { destruct H. apply sym_not_equal. apply Plt_ne; auto. apply Plt_ne; auto. } + { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. } congruence. - assert (RANGE: forall ty, 1 <= typesize ty <= 2). { intros; unfold typesize. destruct ty0; omega. } destruct H. - + destruct H. left. apply sym_not_equal. apply OrderedSlot.lt_not_eq; auto. + + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto. destruct H. right. destruct H0. right. generalize (RANGE ty'); omega. destruct H0. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 8e8b9c0b..d431f3d8 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -329,7 +329,7 @@ Lemma eqmod_iagree: Proof. intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. } rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. destruct (zlt i (Int.size m)). @@ -347,7 +347,7 @@ Lemma iagree_eqmod: Proof. intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. } rewrite EQ; rewrite <- two_power_nat_two_p. apply Int.eqmod_same_bits. intros. apply H. omega. unfold complete_mask. rewrite Int.bits_zero_ext by omega. @@ -829,7 +829,7 @@ Let weak_valid_pointer_no_overflow: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - unfold inject_id; intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Let valid_different_pointers_inj: @@ -1003,9 +1003,9 @@ Module NVal <: SEMILATTICE. Definition t := nval. Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Definition eq_refl: forall x, eq x x := (@eq_refl t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq (x y: t) : bool := proj_sumbool (eq_nval x y). Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. unfold beq; intros. InvBooleans. auto. Qed. diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 0e9eadcb..465b8791 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -108,6 +108,23 @@ module Printer(Target:TARGET) = | Gfun (External ef) -> () | Gvar v -> print_var oc name v + let print_ais_annot oc = + let annots = List.rev !ais_annot_list in + if annots <> [] then begin + Target.section oc Section_ais_annotation; + let annot_part oc lbl = function + | Str.Delim _ -> + fprintf oc " .byte 7,%d\n" (if Archi.ptr64 then 8 else 4) ; + fprintf oc " %s %a\n" Target.address Target.label lbl + | Str.Text a -> fprintf oc " .ascii %S\n" a in + let annot oc (lbl,str) = + List.iter (annot_part oc lbl) str; + fprintf oc " .ascii \"\\n\"\n" + in + List.iter (annot oc) annots + end; + ais_annot_list := [] + module DwarfTarget: DwarfTypes.DWARF_TARGET = struct let label = Target.label @@ -128,6 +145,7 @@ let print_program oc p = Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; + Printer.print_ais_annot oc; if !Clflags.option_g then begin let atom_to_s s = diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index f54c8698..07ab4bed 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -150,62 +150,71 @@ let ptrofs oc n = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -let rec print_annot print_preg sp_reg_name oc = function - | BA x -> print_preg oc x - | BA_int n -> fprintf oc "%ld" (camlint_of_coqint n) - | BA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) - | BA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) - | BA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) +let rec annot_arg preg_string sp_reg_name = function + | BA x -> preg_string x + | BA_int n -> sprintf "%ld" (camlint_of_coqint n) + | BA_long n -> sprintf "%Ld" (camlint64_of_coqint n) + | BA_float n -> sprintf "%.18g" (camlfloat_of_coqfloat n) + | BA_single n -> sprintf "%.18g" (camlfloat_of_coqfloat32 n) | BA_loadstack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" + sprintf "mem(%s + %ld, %ld)" sp_reg_name (camlint_of_coqint ofs) (camlint_of_coqint (size_chunk chunk)) | BA_addrstack ofs -> - fprintf oc "(%s + %ld)" + sprintf "(%s + %ld)" sp_reg_name (camlint_of_coqint ofs) | BA_loadglobal(chunk, id, ofs) -> - fprintf oc "mem(\"%s\" + %ld, %ld)" + sprintf "mem(\"%s\" + %ld, %ld)" (extern_atom id) (camlint_of_coqint ofs) (camlint_of_coqint (size_chunk chunk)) | BA_addrglobal(id, ofs) -> - fprintf oc "(\"%s\" + %ld)" + sprintf "(\"%s\" + %ld)" (extern_atom id) (camlint_of_coqint ofs) | BA_splitlong(hi, lo) -> - fprintf oc "(%a * 0x100000000 + %a)" - (print_annot print_preg sp_reg_name) hi - (print_annot print_preg sp_reg_name) lo + sprintf "(%s * 0x100000000 + %s)" + (annot_arg preg_string sp_reg_name hi) + (annot_arg preg_string sp_reg_name lo) | BA_addptr(a1, a2) -> - fprintf oc "(%a + %a)" - (print_annot print_preg sp_reg_name) a1 - (print_annot print_preg sp_reg_name) a2 + sprintf "(%s + %s)" + (annot_arg preg_string sp_reg_name a1) + (annot_arg preg_string sp_reg_name a2) -let print_annot_text print_preg sp_reg_name oc txt args = - let print_fragment = function +let annot_text preg_string sp_reg_name txt args = + let fragment = function | Str.Text s -> - output_string oc s + s | Str.Delim "%%" -> - output_char oc '%' + "%" | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - print_annot print_preg sp_reg_name oc (List.nth args (n-1)) + annot_arg preg_string sp_reg_name (List.nth args (n-1)) with Failure _ -> - fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" + sprintf "<bad parameter %s>" s in + String.concat "" (List.map fragment (Str.full_split re_annot_param txt)) + +let ais_annot_list: (int * Str.split_result list) list ref = ref [] + +let re_annot_addr = Str.regexp "%addr" + +let ais_annot_text lbl preg_string sp_reg_name txt args = + let annot = annot_text preg_string sp_reg_name txt args in + let annots = Str.full_split re_annot_addr annot in + ais_annot_list := (lbl,annots)::!ais_annot_list; + annot (* Printing of [EF_debug] info. To be completed. *) let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" -let print_debug_info comment print_line print_preg sp_name oc kind txt args = +let print_debug_info comment print_line preg_string sp_name oc kind txt args = let print_debug_args oc args = List.iter - (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a) + (fun a -> fprintf oc " %s" (annot_arg preg_string sp_name a)) args in match kind with | 1 -> (* line number *) diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index d50e07a3..c5418d9d 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -272,15 +272,15 @@ let rec print_stmt p s = | Sexit n -> fprintf p "exit %d;" (Nat.to_int n) | Sswitch(long, e, cases, dfl) -> + let print_case (n,x) = + let x = Nat.to_int x in + if long then + fprintf p "@ case %LdLL: exit %d;" (Z.to_int64 n) x + else + fprintf p "@ case %ld: exit %d;" (Z.to_int32 n) x in fprintf p "@[<v 2>switch%s (%a) {" (if long then "l" else "") print_expr e; - List.iter - (fun (n, x) -> - fprintf p "@ case %s%s: exit %d;" - (Z.to_string n) - (if long then "LL" else "") - (Nat.to_int x)) - cases; + List.iter print_case cases; fprintf p "@ default: exit %d;\n" (Nat.to_int dfl); fprintf p "@;<0 -2>}@]" | Sreturn None -> diff --git a/backend/RTL.v b/backend/RTL.v index d191918c..16723d96 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -437,7 +437,7 @@ Definition instr_defs (i: instruction) : option reg := the CFG of [f] are between 1 and [max_pc_function f] (inclusive). *) Definition max_pc_function (f: function) := - PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive. + PTree.fold (fun m pc i => Pos.max m pc) f.(fn_code) 1%positive. Lemma max_pc_function_sound: forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f). @@ -461,32 +461,32 @@ Qed. Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := match i with | Inop s => m - | Iop op args res s => fold_left Pmax args (Pmax res m) - | Iload chunk addr args dst s => fold_left Pmax args (Pmax dst m) - | Istore chunk addr args src s => fold_left Pmax args (Pmax src m) - | Icall sig (inl r) args res s => fold_left Pmax args (Pmax r (Pmax res m)) - | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m) - | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) - | Itailcall sig (inr id) args => fold_left Pmax args m + | Iop op args res s => fold_left Pos.max args (Pos.max res m) + | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) + | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m) + | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) + | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) + | Itailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m) + | Itailcall sig (inr id) args => fold_left Pos.max args m | Ibuiltin ef args res s => - fold_left Pmax (params_of_builtin_args args) - (fold_left Pmax (params_of_builtin_res res) m) - | Icond cond args ifso ifnot => fold_left Pmax args m - | Ijumptable arg tbl => Pmax arg m + fold_left Pos.max (params_of_builtin_args args) + (fold_left Pos.max (params_of_builtin_res res) m) + | Icond cond args ifso ifnot => fold_left Pos.max args m + | Ijumptable arg tbl => Pos.max arg m | Ireturn None => m - | Ireturn (Some arg) => Pmax arg m + | Ireturn (Some arg) => Pos.max arg m end. Definition max_reg_function (f: function) := - Pmax + Pos.max (PTree.fold max_reg_instr f.(fn_code) 1%positive) - (fold_left Pmax f.(fn_params) 1%positive). + (fold_left Pos.max f.(fn_params) 1%positive). Remark max_reg_instr_ge: forall m pc i, Ple m (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, Ple m n -> Ple m (fold_left Pmax l n)). + assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)). { induction l; simpl; intros. auto. apply IHl. xomega. } @@ -498,7 +498,7 @@ Remark max_reg_instr_def: forall m pc i r, instr_defs i = Some r -> Ple r (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. xomega. apply IHl. xomega. } destruct i; simpl in *; inv H. - apply X. xomega. @@ -511,7 +511,7 @@ Remark max_reg_instr_uses: forall m pc i r, In r (instr_uses i) -> Ple r (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } @@ -564,11 +564,11 @@ Lemma max_reg_function_params: forall f r, In r f.(fn_params) -> Ple r (max_reg_function f). Proof. intros. - assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } - assert (Y: Ple r (fold_left Pmax f.(fn_params) 1%positive)). + assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)). { apply X; auto. } unfold max_reg_function. xomega. Qed. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 6d81f84b..9d7a8506 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -161,7 +161,7 @@ Definition init_state : state := Remark add_instr_wf: forall s i pc, let n := s.(st_nextnode) in - Plt pc (Psucc n) \/ (PTree.set n i s.(st_code))!pc = None. + Plt pc (Pos.succ n) \/ (PTree.set n i s.(st_code))!pc = None. Proof. intros. case (peq pc n); intro. subst pc; left; apply Plt_succ. @@ -175,7 +175,7 @@ Remark add_instr_incr: forall s i, let n := s.(st_nextnode) in state_incr s (mkstate s.(st_nextreg) - (Psucc n) + (Pos.succ n) (PTree.set n i s.(st_code)) (add_instr_wf s i)). Proof. @@ -189,7 +189,7 @@ Definition add_instr (i: instruction) : mon node := fun s => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) + (mkstate s.(st_nextreg) (Pos.succ n) (PTree.set n i s.(st_code)) (add_instr_wf s i)) (add_instr_incr s i). @@ -199,7 +199,7 @@ Definition add_instr (i: instruction) : mon node := Remark reserve_instr_wf: forall s pc, - Plt pc (Psucc s.(st_nextnode)) \/ s.(st_code)!pc = None. + Plt pc (Pos.succ s.(st_nextnode)) \/ s.(st_code)!pc = None. Proof. intros. elim (st_wf s pc); intro. left; apply Plt_trans_succ; auto. @@ -210,7 +210,7 @@ Remark reserve_instr_incr: forall s, let n := s.(st_nextnode) in state_incr s (mkstate s.(st_nextreg) - (Psucc n) + (Pos.succ n) s.(st_code) (reserve_instr_wf s)). Proof. @@ -224,7 +224,7 @@ Definition reserve_instr: mon node := fun (s: state) => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) (Psucc n) s.(st_code) (reserve_instr_wf s)) + (mkstate s.(st_nextreg) (Pos.succ n) s.(st_code) (reserve_instr_wf s)) (reserve_instr_incr s). Remark update_instr_wf: @@ -275,7 +275,7 @@ Definition update_instr (n: node) (i: instruction) : mon unit := Remark new_reg_incr: forall s, - state_incr s (mkstate (Psucc s.(st_nextreg)) + state_incr s (mkstate (Pos.succ s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)). Proof. constructor; simpl. apply Ple_refl. apply Ple_succ. auto. @@ -284,7 +284,7 @@ Qed. Definition new_reg : mon reg := fun s => OK s.(st_nextreg) - (mkstate (Psucc s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)) + (mkstate (Pos.succ s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)) (new_reg_incr s). (** ** Operations on mappings *) @@ -651,7 +651,7 @@ Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap * let (map, s) := maps in let n := s.(st_nextnode) in (PTree.set lbl n map, - mkstate s.(st_nextreg) (Psucc s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)). + mkstate s.(st_nextreg) (Pos.succ s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)). Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) {struct s} : labelmap * state := diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 93f209b7..072db138 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -301,7 +301,7 @@ Proof. destruct (map_letvars x0). auto. simpl in me_letvars0. inversion me_letvars0. intros. rewrite Regmap.gso. apply UNDEF. apply reg_fresh_decr with s2; eauto with rtlg. - apply sym_not_equal. apply valid_fresh_different with s2; auto. + apply not_eq_sym. apply valid_fresh_different with s2; auto. Qed. Lemma match_set_locals: @@ -1535,7 +1535,7 @@ Proof. assert (map_valid init_mapping s0) by apply init_mapping_valid. exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Zle_refl. + edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Z.le_refl. econstructor; split. left; apply plus_one. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index fef74706..8336d1bf 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -132,7 +132,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ibuiltin: forall ef args res s, match ef with - | EF_annot _ _ | EF_debug _ _ _ => True + | EF_annot _ _ _ | EF_debug _ _ _ => True | _ => map type_of_builtin_arg args = (ef_sig ef).(sig_args) end -> type_of_builtin_res res = proj_sig_res (ef_sig ef) -> @@ -308,7 +308,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; do e1 <- match ef with - | EF_annot _ _ | EF_debug _ _ _ => OK e + | EF_annot _ _ _ | EF_debug _ _ _ => OK e | _ => type_builtin_args e args sig.(sig_args) end; type_builtin_res e1 res (proj_sig_res sig) @@ -702,7 +702,7 @@ Proof. exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]]. exploit type_builtin_res_complete. eexact H. instantiate (1 := res). intros [e3 [E F]]. rewrite check_successor_complete by auto. simpl. - exists (match ef with EF_annot _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split. + exists (match ef with EF_annot _ _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split. rewrite H1 in C, E. destruct ef; try (rewrite <- H0; rewrite A); simpl; auto. destruct ef; auto. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index fe5bfe28..75713289 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -36,7 +36,7 @@ Lemma Zdiv_mul_pos: two_p (N+l) <= m * d <= two_p (N+l) + two_p l -> forall n, 0 <= n < two_p N -> - Zdiv n d = Zdiv (m * n) (two_p (N + l)). + Z.div n d = Z.div (m * n) (two_p (N + l)). Proof. intros m l l_pos [LO HI] n RANGE. exploit (Z_div_mod_eq n d). auto. @@ -54,9 +54,9 @@ Proof. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. assert (0 <= k * n). - apply Zmult_le_0_compat; omega. + apply Z.mul_nonneg_nonneg; omega. assert (k * n <= two_p (N + l) - two_p l). - apply Zle_trans with (two_p l * n). + apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. replace (N + l) with (l + N) by omega. rewrite two_p_is_exp. @@ -66,7 +66,7 @@ Proof. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. omega. omega. assert (0 <= two_p (N + l) * r). - apply Zmult_le_0_compat. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). @@ -81,7 +81,7 @@ Proof. assert (m * n - two_p (N + l) * q < two_p (N + l)). apply Zmult_lt_reg_r with d. omega. rewrite H2. - apply Zle_lt_trans with (two_p (N + l) * d - two_p l). + apply Z.le_lt_trans with (two_p (N + l) * d - two_p l). omega. exploit (two_p_gt_ZERO l). omega. omega. symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). @@ -89,7 +89,7 @@ Proof. Qed. Lemma Zdiv_unique_2: - forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1. + forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1. Proof. intros. apply Zdiv_unique with (x - (q - 1) * y). ring. replace ((q - 1) * y) with (y * q - y) by ring. omega. @@ -101,7 +101,7 @@ Lemma Zdiv_mul_opp: two_p (N+l) < m * d <= two_p (N+l) + two_p l -> forall n, 0 < n <= two_p N -> - Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1. + Z.div n d = - Z.div (m * (-n)) (two_p (N + l)) - 1. Proof. intros m l l_pos [LO HI] n RANGE. replace (m * (-n)) with (- (m * n)) by ring. @@ -114,7 +114,7 @@ Proof. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. exploit (two_p_gt_ZERO (N + l)). omega. omega. - cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1). + cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1). omega. apply Zdiv_unique_2. apply two_p_gt_ZERO. omega. @@ -130,15 +130,15 @@ Proof. apply Zmult_lt_reg_r with d. omega. replace (0 * d) with 0 by omega. rewrite H2. - assert (0 < k * n). apply Zmult_lt_0_compat; omega. + assert (0 < k * n). apply Z.mul_pos_pos; omega. assert (0 <= two_p (N + l) * r). - apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega. omega. apply Zmult_le_reg_r with d. omega. rewrite H2. assert (k * n <= two_p (N + l)). - rewrite Zplus_comm. rewrite two_p_is_exp; try omega. - apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. + rewrite Z.add_comm. rewrite two_p_is_exp; try omega. + apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) @@ -156,7 +156,7 @@ Lemma Zquot_mul: two_p (N+l) < m * d <= two_p (N+l) + two_p l -> forall n, - two_p N <= n < two_p N -> - Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). Proof. intros. destruct (zlt n 0). exploit (Zdiv_mul_opp m l H H0 (-n)). omega. @@ -164,7 +164,7 @@ Proof. replace (Z.quot n d) with (- Z.quot (-n) d). rewrite Zquot_Zdiv_pos by omega. omega. rewrite Z.quot_opp_l by omega. ring. - rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. + rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega. apply Zdiv_mul_pos; omega. Qed. @@ -178,7 +178,7 @@ Lemma divs_mul_params_sound: 0 <= m < Int.modulus /\ 0 <= p < 32 /\ forall n, Int.min_signed <= n <= Int.max_signed -> - Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). Proof with (try discriminate). unfold divs_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize @@ -207,7 +207,7 @@ Lemma divu_mul_params_sound: 0 <= m < Int.modulus /\ 0 <= p < 32 /\ forall n, 0 <= n < Int.modulus -> - Zdiv n d = Zdiv (m * n) (two_p (32 + p)). + Z.div n d = Z.div (m * n) (two_p (32 + p)). Proof with (try discriminate). unfold divu_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize @@ -246,9 +246,9 @@ Proof. unfold Int.max_signed; omega. apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. apply Int.modulus_pos. - split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. + split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto. - apply Zle_lt_trans with (Int.half_modulus * m). + apply Z.le_lt_trans with (Int.half_modulus * m). apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto. apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. assert (32 < Int.max_unsigned) by (compute; auto). omega. @@ -310,7 +310,7 @@ Proof. unfold Int.max_unsigned; omega. apply Zdiv_interval_1. omega. compute; auto. compute; auto. split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. - apply Zle_lt_trans with (Int.modulus * m). + apply Z.le_lt_trans with (Int.modulus * m). apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. apply Zmult_lt_compat_l. compute; auto. omega. unfold Int.max_unsigned; omega. @@ -325,7 +325,7 @@ Lemma divls_mul_params_sound: 0 <= m < Int64.modulus /\ 0 <= p < 64 /\ forall n, Int64.min_signed <= n <= Int64.max_signed -> - Z.quot n d = Zdiv (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0). Proof with (try discriminate). unfold divls_mul_params; intros d m' p'. destruct (find_div_mul_params Int64.wordsize @@ -354,7 +354,7 @@ Lemma divlu_mul_params_sound: 0 <= m < Int64.modulus /\ 0 <= p < 64 /\ forall n, 0 <= n < Int64.modulus -> - Zdiv n d = Zdiv (m * n) (two_p (64 + p)). + Z.div n d = Z.div (m * n) (two_p (64 + p)). Proof with (try discriminate). unfold divlu_mul_params; intros d m' p'. destruct (find_div_mul_params Int64.wordsize @@ -399,9 +399,9 @@ Proof. unfold Int64.max_signed; omega. apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos. apply Int64.modulus_pos. - split. apply Zle_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega. + split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega. apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto. - apply Zle_lt_trans with (Int64.half_modulus * m). + apply Z.le_lt_trans with (Int64.half_modulus * m). apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto. apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto. assert (64 < Int.max_unsigned) by (compute; auto). omega. @@ -469,7 +469,7 @@ Proof. unfold Int64.max_unsigned; omega. apply Zdiv_interval_1. omega. compute; auto. compute; auto. split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega. - apply Zle_lt_trans with (Int64.modulus * m). + apply Z.le_lt_trans with (Int64.modulus * m). apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega. apply Zmult_lt_compat_l. compute; auto. omega. unfold Int64.max_unsigned; omega. diff --git a/backend/Selection.v b/backend/Selection.v index f278ed0b..4520cb0c 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -376,21 +376,21 @@ Local Open Scope string_scope. Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := let globs := record_globdefs defmap in - do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ; - do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ; - do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ; - do i64_utod <- lookup_helper globs "__i64_utod" sig_l_f ; - do i64_stof <- lookup_helper globs "__i64_stof" sig_l_s ; - do i64_utof <- lookup_helper globs "__i64_utof" sig_l_s ; - do i64_sdiv <- lookup_helper globs "__i64_sdiv" sig_ll_l ; - do i64_udiv <- lookup_helper globs "__i64_udiv" sig_ll_l ; - do i64_smod <- lookup_helper globs "__i64_smod" sig_ll_l ; - do i64_umod <- lookup_helper globs "__i64_umod" sig_ll_l ; - do i64_shl <- lookup_helper globs "__i64_shl" sig_li_l ; - do i64_shr <- lookup_helper globs "__i64_shr" sig_li_l ; - do i64_sar <- lookup_helper globs "__i64_sar" sig_li_l ; - do i64_umulh <- lookup_helper globs "__i64_umulh" sig_ll_l ; - do i64_smulh <- lookup_helper globs "__i64_smulh" sig_ll_l ; + do i64_dtos <- lookup_helper globs "__compcert_i64_dtos" sig_f_l ; + do i64_dtou <- lookup_helper globs "__compcert_i64_dtou" sig_f_l ; + do i64_stod <- lookup_helper globs "__compcert_i64_stod" sig_l_f ; + do i64_utod <- lookup_helper globs "__compcert_i64_utod" sig_l_f ; + do i64_stof <- lookup_helper globs "__compcert_i64_stof" sig_l_s ; + do i64_utof <- lookup_helper globs "__compcert_i64_utof" sig_l_s ; + do i64_sdiv <- lookup_helper globs "__compcert_i64_sdiv" sig_ll_l ; + do i64_udiv <- lookup_helper globs "__compcert_i64_udiv" sig_ll_l ; + do i64_smod <- lookup_helper globs "__compcert_i64_smod" sig_ll_l ; + do i64_umod <- lookup_helper globs "__compcert_i64_umod" sig_ll_l ; + do i64_shl <- lookup_helper globs "__compcert_i64_shl" sig_li_l ; + do i64_shr <- lookup_helper globs "__compcert_i64_shr" sig_li_l ; + do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ; + do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ; + do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 69480013..dc01ad20 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -210,7 +210,7 @@ Lemma eval_load: Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. unfold load. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a). intros [vl [EV EQ]]. eapply eval_Eload; eauto. Qed. @@ -225,7 +225,7 @@ Lemma eval_store: Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a1). intros [vl [EV EQ]]. eapply step_store; eauto. Qed. @@ -1037,7 +1037,7 @@ Proof. - (* internal function *) destruct TF as (hf & HF & TF). specialize (MC cunit hf). monadInv TF. generalize EQ; intros TF; monadInv TF. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. left; econstructor; split. econstructor; simpl; eauto. diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index fd1fdebd..f1e8b590 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -32,45 +32,45 @@ Definition builtin_implements (name: string) (sg: signature) (vargs: list val) ( external_call (EF_builtin name sg) ge vargs m E0 vres m. Axiom i64_helpers_correct : - (forall x z, Val.longoffloat x = Some z -> external_implements "__i64_dtos" sig_f_l (x::nil) z) - /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__i64_dtou" sig_f_l (x::nil) z) - /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__i64_stod" sig_l_f (x::nil) z) - /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__i64_utod" sig_l_f (x::nil) z) - /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__i64_stof" sig_l_s (x::nil) z) - /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__i64_utof" sig_l_s (x::nil) z) + (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z) + /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z) + /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z) + /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z) + /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z) + /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z) /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y)) - /\ (forall x y z, Val.divls x y = Some z -> external_implements "__i64_sdiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__i64_udiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements "__i64_smod" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__i64_umod" sig_ll_l (x::y::nil) z) - /\ (forall x y, external_implements "__i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) - /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) - /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) - /\ (forall x y, external_implements "__i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) - /\ (forall x y, external_implements "__i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)). + /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z) + /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) + /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) + /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) + /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) + /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)). Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := - helper_declared p i64_dtos "__i64_dtos" sig_f_l - /\ helper_declared p i64_dtou "__i64_dtou" sig_f_l - /\ helper_declared p i64_stod "__i64_stod" sig_l_f - /\ helper_declared p i64_utod "__i64_utod" sig_l_f - /\ helper_declared p i64_stof "__i64_stof" sig_l_s - /\ helper_declared p i64_utof "__i64_utof" sig_l_s - /\ helper_declared p i64_sdiv "__i64_sdiv" sig_ll_l - /\ helper_declared p i64_udiv "__i64_udiv" sig_ll_l - /\ helper_declared p i64_smod "__i64_smod" sig_ll_l - /\ helper_declared p i64_umod "__i64_umod" sig_ll_l - /\ helper_declared p i64_shl "__i64_shl" sig_li_l - /\ helper_declared p i64_shr "__i64_shr" sig_li_l - /\ helper_declared p i64_sar "__i64_sar" sig_li_l - /\ helper_declared p i64_umulh "__i64_umulh" sig_ll_l - /\ helper_declared p i64_smulh "__i64_smulh" sig_ll_l. + helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l + /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l + /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f + /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f + /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s + /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s + /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l + /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l + /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l + /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l + /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l + /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l + /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l + /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l + /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. (** * Correctness of the instruction selection functions for 64-bit operators *) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d3d901b6..f7570f57 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -133,7 +133,7 @@ Qed. Remark bound_stack_data_stacksize: f.(Linear.fn_stacksize) <= b.(bound_stack_data). Proof. - unfold b, function_bounds, bound_stack_data. apply Zmax1. + unfold b, function_bounds, bound_stack_data. apply Z.le_max_l. Qed. (** * Memory assertions used to describe the contents of stack frames *) @@ -217,7 +217,7 @@ Proof. - red; intros. apply Mem.perm_implies with Freeable; auto with mem. apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. - rewrite align_type_chunk. apply Z.divide_add_r. - apply Zdivide_trans with 8; auto. + apply Z.divide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. apply Z.mul_divide_mono_l. auto. Qed. @@ -962,7 +962,7 @@ Local Opaque mreg_type. assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr). assert (POS1: pos <= pos1) by (apply align_le; auto). assert (AL1: (align_chunk (chunk_of_type ty) | pos1)). - { unfold pos1. apply Zdivide_trans with sz. + { unfold pos1. apply Z.divide_trans with sz. unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. apply align_divides; auto. } apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. @@ -1984,7 +1984,7 @@ Proof. econstructor; eauto with coqlib. apply Val.Vptr_has_type. intros; red. - apply Zle_trans with (size_arguments (Linear.funsig f')); auto. + apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. apply loc_arguments_bounded; auto. simpl; red; auto. simpl. rewrite sep_assoc. exact SEP. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 6acf2bbd..c6644ceb 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -505,7 +505,7 @@ Proof. eapply exec_Lreturn; eauto. constructor; eauto using return_regs_lessdef, match_parent_locset. - (* internal function *) - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros (tm' & ALLOC & MEM'). left; simpl; econstructor; split. eapply exec_function_internal; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 446ffb7f..7899a04c 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -835,7 +835,7 @@ Proof. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. -- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. +- simpl in H. exploit Mem.load_inject; eauto. rewrite Z.add_0_r. intros (v' & A & B). exists v'; auto with barg. - econstructor; split; eauto with barg. simpl. econstructor; eauto. rewrite Ptrofs.add_zero; auto. - assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). @@ -956,7 +956,7 @@ Proof. eapply match_stacks_preserves_globals; eauto. eauto. destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto. intros (A & B). - exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D). econstructor; split. eapply exec_Itailcall; eauto. econstructor; eauto. @@ -999,7 +999,7 @@ Proof. econstructor; eauto. - (* return *) - exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D). econstructor; split. eapply exec_Ireturn; eauto. econstructor; eauto. @@ -1011,7 +1011,7 @@ Proof. destruct or; simpl; auto. - (* internal function *) - exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros (j' & tm' & tstk & C & D & E & F & G). assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto). @@ -1124,7 +1124,7 @@ Lemma Mem_getN_forall2: Proof. induction n; simpl Mem.getN; intros. - simpl in H1. omegaContradiction. -- inv H. rewrite inj_S in H1. destruct (zeq i p0). +- inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0). + congruence. + apply IHn with (p0 + 1); auto. omega. omega. Qed. @@ -1145,7 +1145,7 @@ Proof. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. apply P2. omega. - exploit init_meminj_invert; eauto. intros (A & id & B & C). - subst delta. apply Zdivide_0. + subst delta. apply Z.divide_0_r. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). exploit (Genv.init_mem_characterization_gen p); eauto. exploit (Genv.init_mem_characterization_gen tp); eauto. @@ -1159,7 +1159,7 @@ Proof. Local Transparent Mem.loadbytes. generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1. generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. - rewrite Zplus_0_r. + rewrite Z.add_0_r. apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). rewrite H3, H4. apply bytes_of_init_inject. auto. omega. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 08adff2b..3c3aecfd 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -100,9 +100,9 @@ Definition transfer_builtin let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in VA.State (set_builtin_res res ntop ae) am' - | (EF_annot _ _ | EF_debug _ _ _), _ => + | (EF_annot _ _ _ | EF_debug _ _ _), _ => VA.State (set_builtin_res res ntop ae) am - | EF_annot_val _ _, v :: nil => + | EF_annot_val _ _ _, v :: nil => let av := abuiltin_arg ae am rm v in VA.State (set_builtin_res res av ae) am | _, _ => @@ -876,7 +876,7 @@ Proof. apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r. + (* below *) red; simpl; intros. destruct (eq_block b sp). - subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. + subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten; eauto. @@ -1009,7 +1009,7 @@ Proof. + apply SMTOP; auto. + apply SMTOP; auto. + red; simpl; intros. destruct (plt b (Mem.nextblock m)). - eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. + eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto. destruct (j' b) as [[bx deltax] | ] eqn:J'. eapply Mem.valid_block_inject_1; eauto. congruence. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index c71b515c..7cf947ba 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -751,7 +751,7 @@ Definition sgn (p: aptr) (n: Z) : aval := if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Ifptr p. Lemma vmatch_uns': - forall p i n, is_uns (Zmax 0 n) i -> vmatch (Vint i) (uns p n). + forall p i n, is_uns (Z.max 0 n) i -> vmatch (Vint i) (uns p n). Proof. intros. assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va). @@ -781,7 +781,7 @@ Proof. Qed. Lemma vmatch_sgn': - forall p i n, is_sgn (Zmax 1 n) i -> vmatch (Vint i) (sgn p n). + forall p i n, is_sgn (Z.max 1 n) i -> vmatch (Vint i) (sgn p n). Proof. intros. assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va). @@ -3477,7 +3477,7 @@ Lemma ablock_storebytes_contents: forall ab p i sz j chunk' av', (ablock_storebytes ab p i sz).(ab_contents)##j = Some(ACval chunk' av') -> ab.(ab_contents)##j = Some (ACval chunk' av') - /\ (j + size_chunk chunk' <= i \/ i + Zmax sz 0 <= j). + /\ (j + size_chunk chunk' <= i \/ i + Z.max sz 0 <= j). Proof. unfold ablock_storebytes; simpl; intros. exploit inval_before_contents; eauto. clear H. intros [A B]. @@ -4285,13 +4285,13 @@ Proof. intros. constructor. constructor. - (* perms *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. auto. + rewrite Z.add_0_r. auto. - (* alignment *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - apply Zdivide_0. + apply Z.divide_0_r. - (* contents *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. + rewrite Z.add_0_r. set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))). assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)). { @@ -4318,10 +4318,10 @@ Proof. auto. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. split. omega. apply Ptrofs.unsigned_range_2. + rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r in H2. auto. + rewrite Z.add_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: @@ -4372,9 +4372,9 @@ Module AVal <: SEMILATTICE_WITH_TOP. Definition t := aval. Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Definition eq_refl: forall x, eq x x := (@eq_refl t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq (x y: t) : bool := proj_sumbool (eq_aval x y). Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. unfold beq; intros. InvBooleans. auto. Qed. |