diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 15:54:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 15:54:51 +0200 |
| commit | 9d94664fa180d909c43992a4cbdf6808fb9c4289 (patch) | |
| tree | dd6216f214debcbeeee32378d7b4b670e9de695d /mppa_k1c/Asmblockdeps.v | |
| parent | 7cf2665680872984dd62468b3e921276196d0290 (diff) | |
| download | compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.tar.gz compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.zip | |
#90 Asmvliw/Asmblock refactoring attempt
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 92630772..32e5e5bb 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -633,7 +633,7 @@ Fixpoint trans_body (b: list basic) : list L.inst := Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k. -Definition trans_block (b: Asmblock.bblock) : L.bblock := +Definition trans_block (b: Asmvliw.bblock) : L.bblock := trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil). Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. @@ -649,7 +649,7 @@ Qed. Definition state := L.mem. Definition exec := L.run. -Definition match_states (s: Asmblock.state) (s': state) := +Definition match_states (s: Asmvliw.state) (s': state) := let (rs, m) := s in s' pmem = Memstate m /\ forall r, s' (#r) = Val (rs r). @@ -662,7 +662,7 @@ Definition match_outcome (o:outcome) (s: option state) := Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity). -Definition trans_state (s: Asmblock.state) : state := +Definition trans_state (s: Asmvliw.state) : state := let (rs, m) := s in fun x => if (Pos.eq_dec x pmem) then Memstate m else match (inv_ppos x) with @@ -1537,7 +1537,7 @@ Definition string_of_op (op: P.op): ?? pstring := | Fail => RET (Str "Fail") end. -Definition bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool := +Definition bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then IDT.verb_bblock_eq_test string_of_name string_of_op (trans_block p1) (trans_block p2) else @@ -1556,7 +1556,7 @@ Hint Resolve bblock_eq_test_correct: wlp. Import UnsafeImpure. -Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2). +Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2). Theorem pure_bblock_eq_test_correct verb p1 p2: forall ge fn, Ge = Genv ge fn -> @@ -1566,7 +1566,7 @@ Proof. apply unsafe_coerce_not_really_correct; eauto. Qed. -Definition bblock_equivb: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_eq_test true. +Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_eq_test true. Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. @@ -1576,7 +1576,7 @@ End SECT. Module PChk := ParallelChecks L PosPseudoRegSet. -Definition bblock_para_check (p: Asmblock.bblock) : bool := +Definition bblock_para_check (p: Asmvliw.bblock) : bool := PChk.is_parallelizable (trans_block p). Require Import Asmvliw Permutation. |