diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-23 15:58:21 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 8d196f0f3193758a6371d9eb539af350202e0f4f (patch) | |
| tree | 3a434028437588a39c0b6220b85e4732f112dbfc /mppa_k1c | |
| parent | c81c303db03ba732bda8612381e8569db181a541 (diff) | |
| download | compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.tar.gz compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.zip | |
MPPA - Added Mgoto + Pj_l
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
4 files changed, 7 insertions, 9 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 707273a6..82ec101c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -216,8 +216,8 @@ Inductive instruction : Type := | Pcvtw2l (r: ireg) (**r int32 signed -> int64 (pseudo) *) (* Unconditional jumps. Links are always to X1/RA. *) - | Pj_l (l: label) (**r jump to label *) - | Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) +*)| Pj_l (l: label) (**r jump to label *) +(*| Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) | Pj_r (r: ireg) (sg: signature) (**r jump register *) | Pjal_s (symb: ident) (sg: signature) (**r jump-and-link symbol *) | Pjal_r (r: ireg) (sg: signature) (**r jump-and-link register *) @@ -767,9 +767,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r <- (Val.longofint rs#r))) m (** Unconditional jumps. Links are always to X1/RA. *) - | Pj_l l => +*)| Pj_l l => goto_label f l rs m - | Pj_s s sg => +(*| Pj_s s sg => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m | Pj_r r sg => Next (rs#PC <- (rs#r)) m diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index c6f7ef11..69faf1f9 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -837,9 +837,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) | Mlabel lbl => OK (Plabel lbl :: k) -(*| Mgoto lbl => + | Mgoto lbl => OK (Pj_l lbl :: k) - | Mcond cond args lbl => +(*| Mcond cond args lbl => transl_cbranch cond args lbl k | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) *)| Mreturn => diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 88e42d1e..068a2731 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -884,7 +884,6 @@ Local Transparent destroyed_by_op. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H4. -(* exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -894,7 +893,6 @@ Local Transparent destroyed_by_op. econstructor; eauto. eapply agree_exten; eauto with asmgen. congruence. -*) - (* Mcond true *) assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 913127df..280dd17b 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -160,7 +160,7 @@ module Target : TARGET = let print_instruction oc = function | Pcall(s) -> fprintf oc " call %a\n;;\n" symbol s - | Pgoto(s) -> + | Pgoto(s) | Pj_l(s) -> fprintf oc " goto %a\n;;\n" symbol s | Pret -> fprintf oc " ret\n;;\n" |