diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-20 17:39:52 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-20 17:39:52 +0100 |
commit | 04fa6896dfdf8c63be9adaec99091a2061c027b4 (patch) | |
tree | edb3972ead2ef5d11e2e7fc0592c3a269b393913 /mppa_k1c | |
parent | 3e29c4e58853653bf1f3bd374157147d1e1cd75b (diff) | |
download | compcert-kvx-04fa6896dfdf8c63be9adaec99091a2061c027b4.tar.gz compcert-kvx-04fa6896dfdf8c63be9adaec99091a2061c027b4.zip |
Finished the compilation of Asmblock to Abstractbb
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 72 |
1 files changed, 41 insertions, 31 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 41c87441..bb107574 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -90,6 +90,8 @@ Inductive op_wrap := | Store (so: store_op) | Control (co: control_op) | Allocframe (sz: Z) (pos: ptrofs) + | Freeframe (sz: Z) (pos: ptrofs) + | Freeframe2 (sz: Z) (pos: ptrofs) | Constant (v: val) . @@ -334,6 +336,32 @@ Definition op_eval (o: op) (l: list value) := | None => None | Some m => Some (Memstate m) end + | Freeframe sz pos, [Val spv; Memstate m] => + match Mem.loadv Mptr m (Val.offset_ptr spv pos) with + | None => None + | Some v => + match spv with + | Vptr stk ofs => + match Mem.free m stk 0 sz with + | None => None + | Some m' => Some (Memstate m') + end + | _ => None + end + end + | Freeframe2 sz pos, [Val spv; Memstate m] => + match Mem.loadv Mptr m (Val.offset_ptr spv pos) with + | None => None + | Some v => + match spv with + | Vptr stk ofs => + match Mem.free m stk 0 sz with + | None => None + | Some m' => Some (Val v) + end + | _ => None + end + end | Constant v, [] => Some (Val v) | _, _ => None end. @@ -417,6 +445,9 @@ Definition op_eq (o1 o2: op): ?? bool := | Store i1, Store i2 => store_op_eq i1 i2 | Control i1, Control i2 => control_op_eq i1 i2 | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) + | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) + | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) + | Constant c1, Constant c2 => phys_eq c1 c2 | _, _ => RET false end. @@ -429,6 +460,9 @@ Proof. - simpl in Hexta. exploit store_op_eq_correct. eassumption. eauto. congruence. - simpl in Hexta. exploit control_op_eq_correct. eassumption. eauto. congruence. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + - congruence. Qed. End IMPPARAM. @@ -519,45 +553,21 @@ Definition trans_basic (b: basic) : macro := | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (Name (#s) @ Name (#a) @ Name pmem @ Enil))] | Pallocframe sz pos => [(pmem, Op (Allocframe sz pos) (Name (#SP) @ Name pmem @ Enil)); (#FP, Name (#SP)); (#SP, Name (#RTMP)); (#RTMP, Op (Constant Vundef) Enil)] - | _ => [] + | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (Name (#SP) @ Name pmem @ Enil)); + (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); + (#RTMP, Op (Constant Vundef) Enil)] + | Pget rd ra => [(#rd, Name (#ra))] + | Pset ra rd => [(#ra, Name (#rd))] + | Pnop => [] end. -(* - | Pfreeframe sz pos => - match Mem.loadv Mptr m (Val.offset_ptr rs#SP pos) with - | None => Stuck - | Some v => - match rs SP with - | Vptr stk ofs => - match Mem.free m stk 0 sz with - | None => Stuck - | Some m' => Next (rs#SP <- v #RTMP <- Vundef) m' - end - | _ => Stuck - end - end - | Pget rd ra => - match ra with - | RA => Next (rs#rd <- (rs#ra)) m - | _ => Stuck - end - | Pset ra rd => - match ra with - | RA => Next (rs#ra <- (rs#rd)) m - | _ => Stuck - end - | Pnop => Next rs m - end. *) - Fixpoint trans_body (b: list basic) : list L.macro := match b with | nil => nil | b :: lb => (trans_basic b) :: (trans_body lb) end. -(* Definition trans_block (b: bblock) : L.bblock := +Definition trans_block (b: Asmblock.bblock) : L.bblock := trans_body (body b) ++ trans_exit (exit b). -. - *) End SECT. |