diff options
-rw-r--r-- | backend/Duplicateproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 6 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 6 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 2 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpSimuTest.v | 14 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpHCons.v | 4 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 8 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/SeqSimuTheory.v | 11 | ||||
-rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 4 | ||||
-rw-r--r-- | mppa_k1c/lib/ForwardSimulationBlock.v | 6 | ||||
-rw-r--r-- | mppa_k1c/lib/Machblockgen.v | 8 | ||||
-rw-r--r-- | mppa_k1c/lib/Machblockgenproof.v | 20 |
15 files changed, 54 insertions, 49 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index a8e9b16b..466b4b75 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -378,7 +378,7 @@ Theorem step_simulation: step tge s2 t s2' /\ match_states s1' s2'. Proof. - Local Hint Resolve transf_fundef_correct. + Local Hint Resolve transf_fundef_correct: core. induction 1; intros; inv MS. (* Inop *) - eapply dupmap_correct in DUPLIC; eauto. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 02f9141b..01eda623 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -339,7 +339,7 @@ Proof. } destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence. Qed. - + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None @@ -1005,7 +1005,7 @@ Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi: Proof. (* a little tactic to automate reasoning on preg_eq *) -Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr. +Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core. Local Ltac preg_eq_discr r rd := destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto); rewrite (assign_diff _ (#rd) (#r) _); auto; @@ -1053,7 +1053,7 @@ Local Ltac preg_eq_discr r rd := preg_eq_discr r rd0. } (* Load Octuple word *) - + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr. + + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core. unfold parexec_load_o_offset. destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl. rewrite H0, H. @@ -1423,7 +1423,7 @@ Section SECT_BBLOCK_EQUIV. Variable Ge: genv. -Local Hint Resolve trans_state_match. +Local Hint Resolve trans_state_match: core. Lemma bblock_simu_reduce: forall p1 p2 ge fn, diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 50637723..36269954 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -28,6 +28,8 @@ Require Import Chunks. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Import PArithCoercions. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index ecb4629b..5b44ddaa 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -23,6 +23,8 @@ Require Import Op Locations Machblock Conventions. Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops. Require Import Chunks. +Import PArithCoercions. + (** Decomposition of integer constants. *) Lemma make_immed32_sound: @@ -859,7 +861,7 @@ Proof. destruct cmp; discriminate. Qed. -Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct. +Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core. Lemma transl_cbranch_correct_1: forall cond args lbl k c m ms b sp rs m' tbb, @@ -1163,7 +1165,7 @@ Proof. split; intros; Simpl. Qed. -Local Hint Resolve Val_cmpu_correct Val_cmplu_correct. +Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core. Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e042d95a..946007c1 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -555,6 +555,8 @@ Inductive ar_instruction : Type := | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . +Module PArithCoercions. + Coercion PArithR: arith_name_r >-> Funclass. Coercion PArithRR: arith_name_rr >-> Funclass. Coercion PArithRI32: arith_name_ri32 >-> Funclass. @@ -569,6 +571,8 @@ Coercion PArithARR: arith_name_arr >-> Funclass. Coercion PArithARRI32: arith_name_arri32 >-> Funclass. Coercion PArithARRI64: arith_name_arri64 >-> Funclass. +End PArithCoercions. + Inductive basic : Type := | PArith (i: ar_instruction) | PLoad (i: ld_instruction) @@ -1709,7 +1713,7 @@ Proof. Qed. -Local Hint Resolve parexec_bblock_write_in_order. +Local Hint Resolve parexec_bblock_write_in_order: core. Lemma det_parexec_write_in_order f b rs m rs' m': det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index fbb06c9b..3b123c75 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -567,7 +567,7 @@ Proof. unfold builtin_alone in H0. erewrite H0; eauto. Qed. -Local Hint Resolve verified_schedule_nob_checks_alls_bundles. +Local Hint Resolve verified_schedule_nob_checks_alls_bundles: core. Lemma verified_schedule_checks_alls_bundles bb lb bundle: verified_schedule bb = OK lb -> diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 5c94d435..cf46072f 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -403,7 +403,7 @@ Proof. * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto. * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto. Qed. -Local Hint Resolve app_fail_allvalid_correct. +Local Hint Resolve app_fail_allvalid_correct: core. Lemma app_fail_correct l pt t1 t2: match_pt t1 pt -> diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v index ea55b735..7a77ec15 100644 --- a/mppa_k1c/abstractbb/ImpSimuTest.v +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -304,12 +304,12 @@ Proof. rewrite <- EQT; eauto. + exploit smem_valid_set_decompose_1; eauto. - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl. - Local Hint Resolve smem_valid_set_decompose_1. + Local Hint Resolve smem_valid_set_decompose_1: core. intros; case (R.eq_dec x x0). + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. + intros; rewrite !Dict.set_spec_diff; simpl; eauto. Qed. -Local Hint Resolve naive_set_correct. +Local Hint Resolve naive_set_correct: core. Definition equiv_hsmem ge (hd1 hd2: hsmem) := (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m) @@ -523,7 +523,7 @@ Lemma hinst_smem_correct i: forall hd hod, WHEN hinst_smem i hd hod ~> hd' THEN forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'. Proof. - Local Hint Resolve smem_valid_set_proof. + Local Hint Resolve smem_valid_set_proof: core. induction i; simpl; wlp_simplify; eauto 15 with wlp. Qed. Global Opaque hinst_smem. @@ -563,7 +563,7 @@ Definition bblock_hsmem: bblock -> ?? hsmem Lemma bblock_hsmem_correct p: WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd. Proof. - Local Hint Resolve hsmem_empty_correct. + Local Hint Resolve hsmem_empty_correct: core. wlp_simplify. Qed. Global Opaque bblock_hsmem. @@ -775,7 +775,7 @@ Proof. intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid. Qed. -Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv. +Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv: core. Program Definition bblock_simu_test (p1 p2: bblock): ?? bool := DO log <~ count_logger ();; @@ -802,7 +802,7 @@ Obligation 2. wlp_simplify. Qed. -Local Hint Resolve g_bblock_simu_test_correct. +Local Hint Resolve g_bblock_simu_test_correct: core. Theorem bblock_simu_test_correct p1 p2: WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. @@ -1123,7 +1123,7 @@ Definition get {A} (d:t A) (x:R.t): option A Definition set {A} (d:t A) (x:R.t) (v:A): t A := PositiveMap.add x v d. -Local Hint Unfold PositiveMap.E.eq. +Local Hint Unfold PositiveMap.E.eq: core. Lemma set_spec_eq A d x (v: A): get (set d x v) x = Some v. diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v index d8002375..637116cc 100644 --- a/mppa_k1c/abstractbb/Impure/ImpHCons.v +++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v @@ -95,7 +95,7 @@ Proof. wlp_simplify. Qed. Global Opaque assert_list_incl. -Hint Resolve assert_list_incl_correct. +Hint Resolve assert_list_incl_correct: wlp. End Sets. @@ -165,7 +165,7 @@ Lemma hConsV_correct A (hasheq: A -> A -> ?? bool): (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data). Proof. - Local Hint Resolve f_equal2. + Local Hint Resolve f_equal2: core. wlp_simplify. exploit H; eauto. + wlp_simplify. diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index 22809095..30904b5d 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -332,7 +332,7 @@ Fixpoint bblock_wframe(p:bblock): list R.t := | i::p' => (inst_wframe i)++(bblock_wframe p') end. -Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm. +Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm: core. Lemma bblock_wframe_Permutation p p': Permutation p p' -> Permutation (bblock_wframe p) (bblock_wframe p'). @@ -620,7 +620,7 @@ Include ParallelizablityChecking L. Section PARALLEL2. Variable ge: genv. -Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame. +Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame: core. (** Now, refinement of each operation toward parallelizable *) @@ -659,14 +659,14 @@ Fixpoint inst_sframe (i: inst): S.t := | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i')) end. -Local Hint Resolve exp_sframe_correct. +Local Hint Resolve exp_sframe_correct: core. Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i). Proof. induction i as [|[y e] i']; simpl; auto. Qed. -Local Hint Resolve inst_wsframe_correct inst_sframe_correct. +Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core. Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool := match p with diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v index 649dd083..e234883f 100644 --- a/mppa_k1c/abstractbb/SeqSimuTheory.v +++ b/mppa_k1c/abstractbb/SeqSimuTheory.v @@ -102,9 +102,6 @@ Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem := let d':=inst_smem i d d in bblock_smem_rec p' d' end. -(* -Local Hint Resolve smem_eval_empty. -*) Definition bblock_smem: bblock -> smem := fun p => bblock_smem_rec p smem_empty. @@ -124,7 +121,7 @@ Proof. intros d a H; eapply inst_smem_pre_monotonic; eauto. Qed. -Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic. +Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic: core. Lemma term_eval_exp e (od:smem) m0 old: (forall x, term_eval ge (od x) m0 = Some (old x)) -> @@ -185,7 +182,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x). Proof. - Local Hint Resolve inst_smem_Some_correct1. + Local Hint Resolve inst_smem_Some_correct1: core. induction p as [ | i p]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. @@ -299,7 +296,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> pre (bblock_smem_rec p d) ge m0. Proof. - Local Hint Resolve inst_valid. + Local Hint Resolve inst_valid: core. induction p as [ | i p]; simpl; intros m1 d H; auto. intros H0 H1. destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. @@ -326,7 +323,7 @@ Theorem bblock_smem_simu p1 p2: smem_simu (bblock_smem p1) (bblock_smem p2) -> bblock_simu ge p1 p2. Proof. - Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1. + Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core. intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-. destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 940c6563..58455ada 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -414,7 +414,7 @@ Proof. Qed. -Local Hint Resolve code_tail_0 code_tail_S. +Local Hint Resolve code_tail_0 code_tail_S: core. Lemma code_tail_next: forall fn ofs c0, @@ -458,7 +458,7 @@ Proof. omega. Qed. -Local Hint Resolve code_tail_next. +Local Hint Resolve code_tail_next: core. Lemma code_tail_next_int: forall fn ofs bi c, diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v index 39dd2234..224eda0a 100644 --- a/mppa_k1c/lib/ForwardSimulationBlock.v +++ b/mppa_k1c/lib/ForwardSimulationBlock.v @@ -21,7 +21,7 @@ Section starN_lemma. Variable L: semantics. -Local Hint Resolve starN_refl starN_step Eapp_assoc. +Local Hint Resolve starN_refl starN_step Eapp_assoc: core. Lemma starN_split n s t s': starN (step L) (globalenv L) n s t s' -> @@ -93,7 +93,7 @@ Hypothesis simu_end_block: (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) -Local Hint Resolve starN_refl starN_step. +Local Hint Resolve starN_refl starN_step: core. Definition follows_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current @@ -164,7 +164,7 @@ Inductive is_well_memorized (s s': memostate): Prop := memorized s' = None -> is_well_memorized s s'. -Local Hint Resolve StartBloc MidBloc ExitBloc. +Local Hint Resolve StartBloc MidBloc ExitBloc: core. Definition memoL1 := {| state := memostate; diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v index a65b218f..2ba42814 100644 --- a/mppa_k1c/lib/Machblockgen.v +++ b/mppa_k1c/lib/Machblockgen.v @@ -105,7 +105,7 @@ Inductive is_end_block: Machblock_inst -> code -> Prop := | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl) | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. -Local Hint Resolve End_empty End_basic End_cfi. +Local Hint Resolve End_empty End_basic End_cfi: core. Inductive is_trans_code: Mach.code -> code -> Prop := | Tr_nil: is_trans_code nil nil @@ -123,7 +123,7 @@ Inductive is_trans_code: Mach.code -> code -> Prop := header bh = nil -> is_trans_code (i::c) (add_basic bi bh::bl). -Local Hint Resolve Tr_nil Tr_end_block. +Local Hint Resolve Tr_nil Tr_end_block: core. Lemma add_to_code_is_trans_code i c bl: is_trans_code c bl -> @@ -145,7 +145,7 @@ Proof. rewrite <- Heqti. eapply End_cfi. congruence. Qed. -Local Hint Resolve add_to_code_is_trans_code. +Local Hint Resolve add_to_code_is_trans_code: core. Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, is_trans_code c2 mbi -> @@ -185,7 +185,7 @@ Proof. exists mbi1. split; congruence. Qed. -Local Hint Resolve trans_code_is_trans_code. +Local Hint Resolve trans_code_is_trans_code: core. Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). Proof. diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v index 91be5e2e..0de2df52 100644 --- a/mppa_k1c/lib/Machblockgenproof.v +++ b/mppa_k1c/lib/Machblockgenproof.v @@ -72,7 +72,7 @@ Proof. apply match_states_trans_state. Qed. -Local Hint Resolve match_states_trans_state. +Local Hint Resolve match_states_trans_state: core. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -284,7 +284,7 @@ Proof. Qed. Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated - parent_sp_preserved. + parent_sp_preserved: core. Definition dist_end_block_code (c: Mach.code) := @@ -299,8 +299,8 @@ Definition dist_end_block (s: Mach.state): nat := | _ => 0 end. -Local Hint Resolve exec_nil_body exec_cons_body. -Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore. +Local Hint Resolve exec_nil_body exec_cons_body: core. +Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core. Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. Proof. @@ -336,7 +336,7 @@ Proof. omega. Qed. -Local Hint Resolve dist_end_block_code_simu_mid_block. +Local Hint Resolve dist_end_block_code_simu_mid_block: core. Lemma size_nonzero c b bl: @@ -392,8 +392,8 @@ destruct i; congruence. Qed. -Local Hint Resolve Mlabel_is_not_cfi. -Local Hint Resolve MBbasic_is_not_cfi. +Local Hint Resolve Mlabel_is_not_cfi: core. +Local Hint Resolve MBbasic_is_not_cfi: core. Lemma add_to_new_block_is_label i: header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l. @@ -408,7 +408,7 @@ Proof. + unfold cfi_bblock in H; simpl in H; congruence. Qed. -Local Hint Resolve Mlabel_is_not_basic. +Local Hint Resolve Mlabel_is_not_basic: core. Lemma trans_code_decompose c: forall b bl, is_trans_code c (b::bl) -> @@ -510,8 +510,8 @@ Proof. rewrite Hs2, Hb2; eauto. Qed. -Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit. -Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same. +Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit: core. +Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core. Lemma match_states_concat_trans_code st f sp c rs m h: |