diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 11:43:28 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
| commit | d870e17a7a964b48d8e44195ccd12e4160a63f32 (patch) | |
| tree | 3b16e98d6a1044be90dbff1642e3386ec276cb2d /mppa_k1c | |
| parent | 95926365caa7577f0936cdd4ab705d28b3d1457d (diff) | |
| download | compcert-kvx-d870e17a7a964b48d8e44195ccd12e4160a63f32.tar.gz compcert-kvx-d870e17a7a964b48d8e44195ccd12e4160a63f32.zip | |
Extraction issue
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 15 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/extractionMachdep.v | 2 |
3 files changed, 18 insertions, 3 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f0284c26..5229e364 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -30,10 +30,15 @@ Require Import Smallstep. Require Import Locations.
Require Stacklayout.
Require Import Conventions.
-Require Import Asmblock.
+Require Import Asmblock Asmblockgen.
Require Import Linking.
Require Import Errors.
+(** Definitions for OCaml code *)
+Definition label := positive.
+Definition preg := preg.
+
+(** Syntax *)
Inductive instruction : Type :=
(** pseudo instructions *)
| Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *)
@@ -251,6 +256,11 @@ Definition basic_to_instruction (b: basic) := Section RELSEM.
+(** 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 code := list instruction.
Fixpoint unfold_label (ll: list label) :=
@@ -282,6 +292,9 @@ Fixpoint unfold (lb: bblocks) := Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks; fn_code: code;
correct: unfold fn_blocks = fn_code }.
+(* For OCaml code *)
+Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}.
+
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
Definition genv := Genv.t fundef unit.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index b3a1e836..20abfc38 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -47,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 (Asmgen.addptrofs dst src n []) + List.iter emit (Asm.addptrofs dst src n []) let expand_storeind_ptr src base ofs = - List.iter emit (Asmgen.storeind_ptr src base ofs []) + List.iter emit (Asm.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/extractionMachdep.v b/mppa_k1c/extractionMachdep.v index c9a1040a..e70f51de 100644 --- a/mppa_k1c/extractionMachdep.v +++ b/mppa_k1c/extractionMachdep.v @@ -23,5 +23,7 @@ Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ". Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) (* Asm *) +(* Extract Constant Asm.low_half => "fun _ _ _ -> assert false". Extract Constant Asm.high_half => "fun _ _ _ -> assert false". +*) |