From 5568558f61a13754cc9f80d5e9641c6e9e9bc742 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 28 Nov 2018 14:24:01 +0100 Subject: mppa_k1c compiles --- mppa_k1c/Asmexpand.ml | 5 ++--- mppa_k1c/Asmgen.v | 7 +------ 2 files changed, 3 insertions(+), 9 deletions(-) (limited to 'mppa_k1c') 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). -- cgit