From b748b38c8b3a998f018477d7375ae16997318769 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 10 Feb 2020 18:30:07 +0100 Subject: Removing from Asmblockgenproof0 architecture specific definitions --- configure | 2 +- mppa_k1c/Asmblock.v | 13 ++++ mppa_k1c/Asmblockdeps.v | 10 +-- mppa_k1c/Asmblockgenproof.v | 2 +- mppa_k1c/Asmblockgenproof0.v | 124 ++---------------------------------- mppa_k1c/Asmblockgenproof1.v | 2 +- mppa_k1c/Asmblockprops.v | 126 +++++++++++++++++++++++++++++++++++++ mppa_k1c/PostpassScheduling.v | 2 +- mppa_k1c/PostpassSchedulingproof.v | 2 +- 9 files changed, 153 insertions(+), 130 deletions(-) create mode 100644 mppa_k1c/Asmblockprops.v diff --git a/configure b/configure index 9d5bfcf9..f13d1af3 100755 --- a/configure +++ b/configure @@ -845,7 +845,7 @@ EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index cce180ac..a05d4726 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -33,6 +33,19 @@ Require Import Conventions. Require Import Errors. Require Export Asmvliw. +(* Notations necessary to hook Asmvliw definitions *) +Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs. +Notation regset := Asmvliw.regset. +Notation extcall_arg := Asmvliw.extcall_arg. +Notation extcall_arg_pair := Asmvliw.extcall_arg_pair. +Notation extcall_arguments := Asmvliw.extcall_arguments. +Notation set_res := Asmvliw.set_res. +Notation function := Asmvliw.function. +Notation bblocks := Asmvliw.bblocks. +Notation header := Asmvliw.header. +Notation body := Asmvliw.body. +Notation exit := Asmvliw.exit. +Notation correct := Asmvliw.correct. (** * Auxiliary utilies on basic blocks *) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 584f2339..02f9141b 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -7,7 +7,7 @@ Require Import AST. Require Import Asmblock. -Require Import Asmblockgenproof0. +Require Import Asmblockgenproof0 Asmblockprops. Require Import Values. Require Import Globalenvs. Require Import Memory. @@ -1429,7 +1429,7 @@ Lemma bblock_simu_reduce: forall p1 p2 ge fn, Ge = Genv ge fn -> L.bblock_simu Ge (trans_block p1) (trans_block p2) -> - Asmblockgenproof0.bblock_simu ge fn p1 p2. + Asmblockprops.bblock_simu ge fn p1 p2. Proof. unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK. generalize (H2 (trans_state (State rs m))); clear H2. @@ -1787,7 +1787,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. Theorem bblock_simu_test_correct verb p1 p2 : - WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockgenproof0.bblock_simu ge fn p1 p2. + WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2. Proof. wlp_simplify. Qed. @@ -1803,7 +1803,7 @@ Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := | None => false end. -Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. +Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2. Proof. unfold pure_bblock_simu_test. destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate. @@ -1813,7 +1813,7 @@ Qed. Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true. -Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. +Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2. Proof. eapply (pure_bblock_simu_test_correct true). Qed. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 220ae08b..1a427112 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -16,7 +16,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. -Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1. +Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops. Require Import Axioms. Module MB := Machblock. diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index d2450a9a..940c6563 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -22,16 +22,10 @@ Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) +Require Import Asmblockprops. Module MB:=Machblock. -Module AB:=Asmvliw. - -Hint Extern 2 (_ <> _) => congruence: asmgen. - -Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := - forall rs m, - exec_bblock ge f bb rs m <> Stuck -> - exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m. +Module AB:=Asmblock. Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. @@ -51,53 +45,6 @@ Proof. destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. Qed. -Lemma preg_of_data: - forall r, data_preg (preg_of r) = true. -Proof. - intros. destruct r; reflexivity. -Qed. -Hint Resolve preg_of_data: asmgen. - -Lemma data_diff: - forall r r', - data_preg r = true -> data_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. -Hint Resolve data_diff: asmgen. - -Lemma preg_of_not_SP: - forall r, preg_of r <> SP. -Proof. - intros. unfold preg_of; destruct r; simpl; congruence. -Qed. - -Lemma preg_of_not_PC: - forall r, preg_of r <> PC. -Proof. - intros. apply data_diff; auto with asmgen. -Qed. - -Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. - -Lemma nextblock_pc: - forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)). -Proof. - intros. apply Pregmap.gss. -Qed. - -Lemma nextblock_inv: - forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r. -Proof. - intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto. -Qed. - -Lemma nextblock_inv1: - forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r. -Proof. - intros. apply nextblock_inv. red; intro; subst; discriminate. -Qed. - Lemma undef_regs_other: forall r rl rs, (forall r', In r' rl -> r <> r') -> @@ -294,9 +241,9 @@ Qed. Lemma agree_undef_caller_save_regs: forall ms sp rs, agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs). + agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split. + intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. - unfold proj_sumbool; rewrite dec_eq_true. auto. - auto. - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). @@ -752,69 +699,6 @@ Proof. intros. destruct H. auto. Qed. -Ltac Simplif := - ((rewrite nextblock_inv by eauto with asmgen) - || (rewrite nextblock_inv1 by eauto with asmgen) - || (rewrite Pregmap.gss) - || (rewrite nextblock_pc) - || (rewrite Pregmap.gso by eauto with asmgen) - ); auto with asmgen. - -Ltac Simpl := repeat Simplif. - -Theorem exec_basic_instr_pc: - forall ge b rs1 m1 rs2 m2, - exec_basic_instr ge b rs1 m1 = Next rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - intros. destruct b; try destruct i; try destruct i. - all: try (inv H; Simpl). - 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - { (* PLoadQRRO *) - unfold parexec_load_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - { (* PLoadORRO *) - unfold parexec_load_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - 1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail. - 1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - 1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - - { (* PStoreQRRO *) - unfold parexec_store_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - { (* PStoreORRO *) - unfold parexec_store_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. - destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. - - destruct rs; try discriminate. inv H1. Simpl. - - destruct rd; try discriminate. inv H1; Simpl. - - reflexivity. -Qed. - Lemma exec_body_pc: forall ge l rs1 m1 rs2 m2, exec_body ge l rs1 m1 = Next rs2 m2 -> diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index c0a05ab3..ecb4629b 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -20,7 +20,7 @@ Require Import Coqlib Errors Maps. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op Locations Machblock Conventions. -Require Import Asmblock Asmblockgen Asmblockgenproof0. +Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops. Require Import Chunks. (** Decomposition of integer constants. *) diff --git a/mppa_k1c/Asmblockprops.v b/mppa_k1c/Asmblockprops.v new file mode 100644 index 00000000..7f6e33db --- /dev/null +++ b/mppa_k1c/Asmblockprops.v @@ -0,0 +1,126 @@ +(** Common definition and proofs on Asmblock required by various modules *) + +Require Import Coqlib. +Require Import Integers. +Require Import Memory. +Require Import Globalenvs. +Require Import Values. +Require Import Asmblock. + +Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := + forall rs m, + exec_bblock ge f bb rs m <> Stuck -> + exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m. + +Hint Extern 2 (_ <> _) => congruence: asmgen. + +Lemma preg_of_data: + forall r, data_preg (preg_of r) = true. +Proof. + intros. destruct r; reflexivity. +Qed. +Hint Resolve preg_of_data: asmgen. + +Lemma data_diff: + forall r r', + data_preg r = true -> data_preg r' = false -> r <> r'. +Proof. + congruence. +Qed. +Hint Resolve data_diff: asmgen. + +Lemma preg_of_not_PC: + forall r, preg_of r <> PC. +Proof. + intros. apply data_diff; auto with asmgen. +Qed. + +Lemma preg_of_not_SP: + forall r, preg_of r <> SP. +Proof. + intros. unfold preg_of; destruct r; simpl; congruence. +Qed. + +Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. + + +Lemma nextblock_pc: + forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)). +Proof. + intros. apply Pregmap.gss. +Qed. + +Lemma nextblock_inv: + forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r. +Proof. + intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto. +Qed. + +Lemma nextblock_inv1: + forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r. +Proof. + intros. apply nextblock_inv. red; intro; subst; discriminate. +Qed. + +Ltac Simplif := + ((rewrite nextblock_inv by eauto with asmgen) + || (rewrite nextblock_inv1 by eauto with asmgen) + || (rewrite Pregmap.gss) + || (rewrite nextblock_pc) + || (rewrite Pregmap.gso by eauto with asmgen) + ); auto with asmgen. + +Ltac Simpl := repeat Simplif. + +Theorem exec_basic_instr_pc: + forall ge b rs1 m1 rs2 m2, + exec_basic_instr ge b rs1 m1 = Next rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + intros. destruct b; try destruct i; try destruct i. + all: try (inv H; Simpl). + 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + + 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + + { (* PLoadQRRO *) + unfold parexec_load_q_offset in H1. + destruct (gpreg_q_expand _) as [r0 r1] in H1. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + inv H1. Simpl. } + { (* PLoadORRO *) + unfold parexec_load_o_offset in H1. + destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + inv H1. Simpl. } + 1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail. + 1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. + 1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. + + { (* PStoreQRRO *) + unfold parexec_store_q_offset in H1. + destruct (gpreg_q_expand _) as [r0 r1] in H1. + unfold eval_offset in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. } + { (* PStoreORRO *) + unfold parexec_store_o_offset in H1. + destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. + unfold eval_offset in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. } + - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. + - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. + destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. + - destruct rs; try discriminate. inv H1. Simpl. + - destruct rd; try discriminate. inv H1; Simpl. + - reflexivity. +Qed. \ No newline at end of file diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 8b6de1e2..31180cea 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -12,7 +12,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. -Require Import Asmblockdeps Asmblockgenproof0. +Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. Require Peephole. Local Open Scope error_monad_scope. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index cdf8829f..f1166a38 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. -Require Import Asmblockgenproof0. +Require Import Asmblockgenproof0 Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. -- cgit