diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-28 14:24:01 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-28 14:24:01 +0100 |
| commit | 5568558f61a13754cc9f80d5e9641c6e9e9bc742 (patch) | |
| tree | e34df72baf8308857393b2b2b11e8ce2e8b2199e /mppa_k1c | |
| parent | 8d646d93ce0a6611cf55561450e39a82fa464fe6 (diff) | |
| download | compcert-kvx-5568558f61a13754cc9f80d5e9641c6e9e9bc742.tar.gz compcert-kvx-5568558f61a13754cc9f80d5e9641c6e9e9bc742.zip | |
mppa_k1c compiles
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 5 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 7 |
2 files changed, 3 insertions, 9 deletions
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 45fe9b32..0fcc1212 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -20,7 +20,6 @@ of the RISC-V assembly code. *) open Asm -open Asmgen open Asmexpandaux open AST open Camlcoq @@ -48,9 +47,9 @@ let align n a = (n + a - 1) land (-a) List.iter emit (Asmgen.loadimm32 dst n []) *) let expand_addptrofs dst src n = - List.iter emit (addptrofs dst src n :: []) + List.iter emit (basic_to_instruction (Asmblock.PArith (Asmblockgen.addptrofs dst src n)) :: []) let expand_storeind_ptr src base ofs = - List.iter emit (storeind_ptr src base ofs :: []) + List.iter emit (basic_to_instruction (Asmblockgen.storeind_ptr src base ofs) :: []) (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 9b9e6272..6f61747f 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -21,11 +21,6 @@ Require Import Errors. Local Open Scope error_monad_scope. -(** For OCaml code *) -Definition addptrofs (rd rs: ireg) (n: ptrofs) := basic_to_instruction (addptrofs rd rs n). -Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := - basic_to_instruction (storeind_ptr src base ofs). - Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do abp <- Asmblockgen.transf_program mbp; @@ -40,4 +35,4 @@ Definition transl_code (f: Mach.function) (l: Mach.code) : res (list Asm.instruc let mbf := Machblockgen.transf_function f in let mbc := Machblockgen.trans_code l in do abc <- transl_blocks mbf mbc true; - OK (unfold abc).
\ No newline at end of file + OK (unfold abc). |