Extraction issue

5 files changed, 29 insertions, 11 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 23fef3f2..62c4a702 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -26,7 +26,9 @@ let emit i = current_code := i :: !current_code
 
 (* Generation of fresh labels *)
 
-let dummy_function = { fn_code = []; fn_sig = signature_main }
+(** dummy_funtion is now defined in Asm.v *)
+(* let dummy_function = { fn_code = []; fn_sig = signature_main } *)
+
 let current_function = ref dummy_function
 let next_label = ref (None: label option)
 
@@ -39,7 +41,7 @@ let new_label () =
         List.fold_left
           (fun next instr ->
             match instr with
-            | PExpand (Plabel l) -> if P.lt l next then next else P.succ l
+            | Plabel l -> if P.lt l next then next else P.succ l
             | _ -> next)
           P.one (!current_function).fn_code
   in
@@ -100,17 +102,17 @@ let expand_debug id sp preg simple l =
   let get_lbl = function
     | None ->
         let lbl = new_label () in
-        emit (PExpand (Plabel lbl));
+        emit (Plabel lbl);
         lbl
     | Some lbl -> lbl in
   let rec  aux lbl scopes = function
     | [] -> ()
-    | (PExpand (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i))::rest ->
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
         begin
           match kind with
           | 1->
-              emit (PExpand i);aux lbl scopes rest
+              emit i; aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
@@ -142,11 +144,11 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
-    | (PExpand (Plabel lbl))::rest -> simple (PExpand (Plabel lbl)); aux (Some lbl) scopes rest
+    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
-    | (PExpand (Pbuiltin(EF_debug (kind,_,_),_,_)) as i)::rest ->
+    | (Pbuiltin(EF_debug (kind,_,_),_,_)) as i::rest ->
         let kind = (P.to_int kind) in
         if kind = 1 then
           move_debug acc (i::bcc) rest (* Do not move debug line *)
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 8ac776ef..9b124a10 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -167,7 +167,8 @@ Set Extraction AccessOpaque.
 Cd "extraction".
 
 Separate Extraction
-   Asmgen.addptrofs
+(*   Asmgen.addptrofs *)
+   Asm.dummy_function
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
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".
+*)