From f8caf5f7564886dc43246c7477c4c22a7572e60d Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 11 Jan 2019 11:41:09 +0100
Subject: [BROKEN] trying to link the test in mppa_k1c/unittest/postpass_test

---
 mppa_k1c/PostpassSchedulingOracle.ml | 51 +++++++++++++-----------------------
 mppa_k1c/TargetPrinter.ml            |  3 +--
 mppa_k1c/unittest/Makefile           | 12 +++++++++
 mppa_k1c/unittest/postpass_test.ml   | 12 +++++++++
 4 files changed, 43 insertions(+), 35 deletions(-)
 create mode 100644 mppa_k1c/unittest/Makefile
 create mode 100644 mppa_k1c/unittest/postpass_test.ml

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index ac53f5a4..c647fc15 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -2,7 +2,9 @@ open Asmblock
 open Printf
 open Camlcoq
 open InstructionScheduler
-(* open TargetPrinter.Target *)
+open TargetPrinter.Target
+
+let debug = true
 
 (**
  * Extracting infos from Asmblock instructions
@@ -19,37 +21,6 @@ type ab_inst_rec = {
 
 (** Asmblock constructor to string functions *)
 
-(* Because of a bug (from OCaml?), I cannot use TargetPrinter.Target.icond_name (unbound value error). Copy pasting instead *)
-let icond_name = function
-  | ITne | ITneu -> "ne"
-  | ITeq | ITequ -> "eq"
-  | ITlt   -> "lt"
-  | ITge   -> "ge"
-  | ITle   -> "le"
-  | ITgt   -> "gt"
-  | ITltu  -> "ltu"
-  | ITgeu  -> "geu"
-  | ITleu  -> "leu"
-  | ITgtu  -> "gtu"
-  | ITall  -> "all"
-  | ITnall -> "nall"
-  | ITany  -> "any"
-  | ITnone -> "none"
-
-let bcond_name = function
-  | BTwnez -> "wnez"
-  | BTweqz -> "weqz"
-  | BTwltz -> "wltz"
-  | BTwgez -> "wgez"
-  | BTwlez -> "wlez"
-  | BTwgtz -> "wgtz"
-  | BTdnez -> "dnez"
-  | BTdeqz -> "deqz"
-  | BTdltz -> "dltz"
-  | BTdgez -> "dgez"
-  | BTdlez -> "dlez"
-  | BTdgtz -> "dgtz"
-
 let arith_rrr_str = function
   | Pcompw it -> "Pcompw" ^ (icond_name it)
   | Pcompl it -> "Pcompl" ^ (icond_name it)
@@ -392,12 +363,24 @@ let bundlize_solution bb sol =
     !lbb
   end
 
+let print_inst oc = function
+  | Asm.Pallocframe(sz, ofs) -> fprintf oc "	Pallocframe\n"
+  | Asm.Pfreeframe(sz, ofs) -> fprintf oc "	Pfreeframe\n"
+  | i -> print_instruction oc i
+
+let print_bb bb =
+  let asm_instructions = Asm.unfold_bblock bb
+  in List.iter (print_inst stdout) asm_instructions
+
+(* let[@warning "-26"] smart_schedule bb = print_bb bb; failwith "done" *)
 let smart_schedule bb =
+  ( printf "Attempting to schedule the basicblock:\n"; print_bb bb; printf "-----------------------------------\n";
   let problem = build_problem bb
   in let solution = validated_scheduler list_scheduler problem
   in match solution with
   | None -> failwith "Could not find a valid schedule"
   | Some sol -> bundlize_solution bb sol
+  )
 
 (**
  * Dumb schedule if the above doesn't work
@@ -423,7 +406,8 @@ let dumb_schedule (bb : bblock) : bblock list = bundlize_label bb.header @ bundl
 (** Called schedule function from Coq *)
 
 let schedule bb = 
-  try smart_schedule bb
+  ( if debug then print_bb bb;
+    try smart_schedule bb
   with e ->
     let msg = Printexc.to_string e
     and stack = Printexc.get_backtrace ()
@@ -432,3 +416,4 @@ let schedule bb =
       Printf.eprintf "Issuing one instruction per bundle instead\n\n";
       dumb_schedule bb
     end
+  )
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 4f67ea65..cdede1ef 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -27,7 +27,7 @@ open Fileinfo
 
 (* Module containing the printing functions *)
 
-module Target : TARGET =
+module Target (*: TARGET*) =
   struct
 
 (* Basic printing functions *)
@@ -412,7 +412,6 @@ module Target : TARGET =
       current_function_sig := fn.fn_sig;
       List.iter (print_instruction oc) fn.fn_code
 
-
 (* Data *)
 
     let address = if Archi.ptr64 then ".quad" else ".long"
diff --git a/mppa_k1c/unittest/Makefile b/mppa_k1c/unittest/Makefile
new file mode 100644
index 00000000..fc7a51ac
--- /dev/null
+++ b/mppa_k1c/unittest/Makefile
@@ -0,0 +1,12 @@
+# Needs to be called from CompCert root directory
+# $ make -f mppa_k1c/unittest/Makefile postpass_test
+
+include Makefile.extr
+
+TEST_CMX=mppa_k1c/unittest/postpass_test.cmx
+
+UNITTEST_OBJS:=$(shell $(MODORDER) $(TEST_CMX))
+
+postpass_test: $(TEST_CMX) $(UNITTEST_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
diff --git a/mppa_k1c/unittest/postpass_test.ml b/mppa_k1c/unittest/postpass_test.ml
new file mode 100644
index 00000000..434bfaf7
--- /dev/null
+++ b/mppa_k1c/unittest/postpass_test.ml
@@ -0,0 +1,12 @@
+open Printf
+open Asmblock
+open Integers
+open PostpassSchedulingOracle
+open BinNums
+
+let test_schedule_sd =
+  let sd_inst = PStore (PStoreRRO (Psd, GPR12, GPR16, (Ofsimm (Ptrofs.of_int @@ Int.intval Z0))))
+  in let bb = { header = []; body = [sd_inst]; exit = None }
+  in List.iter print_bb (smart_schedule bb)
+
+let _ = test_schedule_sd; printf "Done\n"
-- 
cgit