diff options
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 51 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 3 | ||||
| -rw-r--r-- | mppa_k1c/unittest/Makefile | 12 | ||||
| -rw-r--r-- | mppa_k1c/unittest/postpass_test.ml | 12 |
4 files changed, 43 insertions, 35 deletions
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" |