diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 17:25:36 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 17:25:36 +0200 |
| commit | 76af54d8ae77f843b7f6f15f9a0fc6124df47ebb (patch) | |
| tree | 8375bead74972832b8fab6ce9e5d30fcde7357b1 /mppa_k1c/lib | |
| parent | 9d94664fa180d909c43992a4cbdf6808fb9c4289 (diff) | |
| download | compcert-kvx-76af54d8ae77f843b7f6f15f9a0fc6124df47ebb.tar.gz compcert-kvx-76af54d8ae77f843b7f6f15f9a0fc6124df47ebb.zip | |
#91 Removed completely the duplicated semantics in Asmblock
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 8a83521c..a44c40d8 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -14,6 +14,7 @@ Require Import Machblock. Require Import Asmblock. Require Import Asmblockgen. Require Import Conventions1. +Require Import Axioms. Module MB:=Machblock. Module AB:=Asmvliw. @@ -943,10 +944,10 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold exec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). - 1-10: try (unfold exec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. - 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. @@ -997,6 +998,13 @@ Proof. + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto. Qed. *) + +Lemma regset_same_assign (rs: regset) r: + rs # r <- (rs r) = rs. +Proof. + apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl. +Qed. + Lemma exec_straight_through_singleinst: forall a b rs1 m1 rs2 m2 rs2' m2' lb, bblock_single_inst (PBasic a) = b -> @@ -1005,10 +1013,12 @@ Lemma exec_straight_through_singleinst: exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. Proof. intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - simpl. auto. + simpl. rewrite regset_same_assign. auto. simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto. Qed. + + (** The following lemmas show that straight-line executions (predicate [exec_straight_blocks]) correspond to correct Asm executions. *) |