From 7cedbba8d80a6b1ce9291d62f88289bb5a0e7b05 Mon Sep 17 00:00:00 2001
From: Pierre Wilke <pierre.wilke@centralesupelec.fr>
Date: Wed, 25 Mar 2020 17:15:30 +0100
Subject: [PATCH] Fix performance issue with LTL run
---
src/Makefile | 4 +-
src/ltl_debug.ml | 8 +-
src/ltl_run.ml | 198 +++++++++++++++++++++++++----------------------
src/main.ml | 12 ++-
src/riscv.ml | 10 ++-
src/utils.ml | 15 ++--
tests/test.py | 5 +-
7 files changed, 137 insertions(+), 115 deletions(-)
diff --git a/src/Makefile b/src/Makefile
index 2221741..f972d56 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -9,10 +9,12 @@ symbols.ml utils.ml
TG = main.native
+PROF:=$(if $(PROF),-ocamlopt ocamloptp,)
+
all: $(TG)
$(TG): $(SRC)
- ocamlbuild -cflags -warn-error,"+a-26" -cflags -w,"-26" -use-ocamlfind $(TG)
+ ocamlbuild $(PROF) -cflags -warn-error,"+a-26" -cflags -w,"-26" -use-ocamlfind $(TG)
test_lexer: $(SRC)
ocamlbuild -use-ocamlfind test_lexer.native
diff --git a/src/ltl_debug.ml b/src/ltl_debug.ml
index 73fb9a3..b3d870a 100644
--- a/src/ltl_debug.ml
+++ b/src/ltl_debug.ml
@@ -78,9 +78,9 @@ let rec json_summary j =
| `List l -> `List (List.map json_summary l)
| _ -> j
let trace_regs st =
- Hashtbl.fold (fun r v acc ->
+ Array.fold_lefti (fun acc r v ->
(string_of_reg r, `Int v) :: acc
- ) st.regs []
+ ) [] st.regs
|> fun l -> `Assoc l
let make_trace ip (st: ltl_state) out () =
@@ -177,10 +177,10 @@ let debugger_message progname breaks state st prog rstop client : unit Lwt.t =
) funinfo))
]) :: acc
) !st.funs [] |> fun funboundaries ->
- Hashtbl.fold (fun ip ins acc ->
+ Array.fold_lefti (fun acc ip ins ->
(Format.fprintf Format.str_formatter "%a" dump_ltl_instr ins);
(string_of_int ip, `String (Format.flush_str_formatter ())) :: acc
- ) !st.code [] |> fun code ->
+ ) [] !st.code |> fun code ->
`List ( [`Assoc [("progname", `String progname);
("params", `List (List.map (fun x -> `Int x) params))];
`Assoc [("funboundaries", `List funboundaries)];
diff --git a/src/ltl_run.ml b/src/ltl_run.ml
index b2c2e43..669033d 100644
--- a/src/ltl_run.ml
+++ b/src/ltl_run.ml
@@ -41,29 +41,27 @@ type fun_location = {
}
type ltl_state = {
- code: (int, ltl_instr) Hashtbl.t;
+ code: ltl_instr Array.t;
funs: (string, fun_location) Hashtbl.t;
- regs: (ltl_reg, int) Hashtbl.t;
+ regs: int array;
+ labels : (string, int) Hashtbl.t;
mem: Mem.t;
numstep: int ref;
}
(* Finds the position of a label in the code. *)
-let find_label (code: (int, ltl_instr) Hashtbl.t) (l: string) =
- Hashtbl.fold (fun k v acc ->
- match acc with
- | OK x -> acc
- | Error _ -> if v = LLabel l then OK k else acc
- ) code (Error (Format.sprintf "Label %s not found." l))
+let find_label (labels: (string, int) Hashtbl.t) (l: string) =
+ match Hashtbl.find_option labels l with
+ | Some ip -> OK ip
+ | None -> Error (Format.sprintf "Label %s not found." l)
(* For most instructions, the next instruction to execute is the one at [ip +
1]. *)
let next ip = OK (Some (ip + 1))
(* Helper function to get value of register [r] in state [st]. *)
-let get_reg st r =
- Hashtbl.find_option st.regs r >>
- (Format.sprintf "uninitialized register %s\n" (print_reg r))
+let get_reg st r f =
+ f (Array.get st.regs r)
(* Execution of one LTL instruction.
@@ -79,99 +77,112 @@ let get_reg st r =
let exec_ltl_instr oc ip st : (int option) res =
let open Utils in
- match Hashtbl.find_option st.code ip with
- | None -> Error (Format.sprintf
- "Could not find next instruction to execute at ip=%d \
- [in exec_ltl_instr]" ip)
- | Some i ->
- match i with
- | LAddi(rd, rs, i) ->
- get_reg st rs $ fun vs ->
- Hashtbl.replace st.regs rd (vs + i);
- next ip
- | LSubi(rd, rs, i) ->
- get_reg st rs $ fun vs ->
- Hashtbl.replace st.regs rd (vs - i);
+ match Array.get st.code ip with
+ | exception Invalid_argument _ -> Error (Format.sprintf
+ "Could not find next instruction to execute at ip=%d \
+ [in exec_ltl_instr]" ip)
+ | LAddi(rd, rs, i) ->
+ get_reg st rs $ fun vs ->
+ Array.set st.regs rd (vs + i);
+ next ip
+ | LSubi(rd, rs, i) ->
+ get_reg st rs $ fun vs ->
+ Array.set st.regs rd (vs - i);
+ next ip
+ | LBinop(b, rd, rs1, rs2) ->
+ get_reg st rs1 $ fun vs1 ->
+ get_reg st rs2 $ fun vs2 ->
+ Array.set st.regs rd (eval_binop b vs1 vs2);
next ip
- | LBinop(b, rd, rs1, rs2) ->
- get_reg st rs1 $ fun vs1 ->
- get_reg st rs2 $ fun vs2 ->
- Hashtbl.replace st.regs rd (eval_binop b vs1 vs2);
- next ip
- | LUnop(u, rd, rs) ->
+ | LUnop(u, rd, rs) ->
+ get_reg st rs $ fun vs ->
+ Array.set st.regs rd (eval_unop u vs);
+ next ip
+ | LStore(rt, i, rs, sz) ->
+ get_reg st rt $ fun vt ->
get_reg st rs $ fun vs ->
- Hashtbl.replace st.regs rd (eval_unop u vs);
+ Mem.write_bytes st.mem (vt + i) (split_bytes sz vs) >>= fun _ ->
next ip
- | LStore(rt, i, rs, sz) ->
- get_reg st rt $ fun vt ->
- get_reg st rs $ fun vs ->
- Mem.write_bytes st.mem (vt + i) (split_bytes sz vs) >>= fun _ ->
- next ip
- | LLoad(rd, rt, i, sz) ->
- get_reg st rt $ fun vt ->
- Mem.read_bytes_as_int st.mem (vt + i) sz >>= fun (v) ->
- Hashtbl.replace st.regs rd v;
+ | LLoad(rd, rt, i, sz) ->
+ get_reg st rt $ fun vt ->
+ Mem.read_bytes_as_int st.mem (vt + i) sz >>= fun (v) ->
+ Array.set st.regs rd v;
+ next ip
+ | LMov(rd, rs) ->
+ get_reg st rs $ fun vs ->
+ Array.set st.regs rd vs;
+ next ip
+ | LLabel l -> next ip
+ | LJmp l -> find_label st.labels l >>= fun n -> OK (Some n)
+ | LJmpr r ->
+ get_reg st reg_ra $ fun ra ->
+ OK (Some ra)
+ | LConst (rd, i) -> Array.set st.regs rd i; next ip
+ | LComment _ -> next ip
+ | LBranch(cmp, rs1, rs2, s) ->
+ get_reg st rs1 $ fun vs1 ->
+ get_reg st rs2 $ fun vs2 ->
+ let b = eval_rtl_cmp cmp vs1 vs2 in
+ if b
+ then find_label st.labels s >>= fun n -> OK (Some n)
+ else next ip
+ | LCall callee_name ->
+ begin match Hashtbl.find_option st.funs callee_name with
+ Some {funstart} ->
+ Array.set st.regs reg_ra (ip+1);
+ OK (Some funstart)
+ | None ->
+ do_builtin oc st.mem callee_name
+ (list_ints_desc number_of_arguments_passed_in_registers |> List.rev |>
+ List.map (fun i -> i + starting_arg_register) |>
+ List.map (fun i -> Array.get st.regs i)) >>=
+ fun v ->
+ begin match v with
+ | None -> ()
+ | Some v -> Array.set st.regs reg_ret v
+ end;
next ip
- | LMov(rd, rs) ->
- get_reg st rs $ fun vs ->
- Hashtbl.replace st.regs rd vs;
- next ip
- | LLabel l -> next ip
- | LJmp l -> find_label st.code l >>= fun n -> OK (Some n)
- | LJmpr r ->
- get_reg st reg_ra $ fun ra -> OK (Some ra)
- | LConst (rd, i) -> Hashtbl.replace st.regs rd i; next ip
- | LComment _ -> next ip
- | LBranch(cmp, rs1, rs2, s) ->
- get_reg st rs1 $ fun vs1 ->
- get_reg st rs2 $ fun vs2 ->
- let b = eval_rtl_cmp cmp vs1 vs2 in
- if b
- then find_label st.code s >>= fun n -> OK (Some n)
- else next ip
- | LCall callee_name ->
- begin match Hashtbl.find_option st.funs callee_name with
- Some {funstart} ->
- Hashtbl.replace st.regs reg_ra (ip+1);
- OK (Some funstart)
- | None ->
- do_builtin oc st.mem callee_name
- (list_ints_desc number_of_arguments_passed_in_registers |> List.rev |>
- List.map (fun i -> i + starting_arg_register) |>
- List.map (fun i -> Hashtbl.find_default st.regs i 0)) >>=
- fun v ->
- begin match v with
- | None -> ()
- | Some v -> Hashtbl.replace st.regs reg_ret v
- end;
- next ip
- end
- | LHalt -> OK None
+ end
+ | LHalt -> OK None
(* Initialize regs [0,n[ *)
let rec init_regs n =
- let regs = Hashtbl.create n in
- range n |> List.iter (fun n -> Hashtbl.replace regs n 0);
+ let regs = Array.init n (fun _ -> 0) in
regs
let init_state memsize lp params =
- let code : (int, ltl_instr) Hashtbl.t = Hashtbl.create 17 in
+ let lp = (("__halt", Gfun {ltlfunargs = 0;
+ ltlfunbody = [LHalt];
+ ltlfuninfo = [];
+ ltlregalloc = [];
+ })::lp) in
+ let codesize = List.fold_left (fun sz (name, def) ->
+ match def with
+ | Gfun f ->
+ sz + List.length f.ltlfunbody
+ ) 0 lp in
+ let code : ltl_instr Array.t = Array.init codesize (fun _ -> LHalt) in
let funs : (string, fun_location) Hashtbl.t = Hashtbl.create 17 in
+ let labels : (string, int) Hashtbl.t = Hashtbl.create 17 in
let mem = Mem.init memsize in
let regs = init_regs 32 in
- let sp = memsize - !Archi.wordsize in
- Hashtbl.replace regs reg_sp sp;
- Hashtbl.replace regs reg_fp sp;
- Hashtbl.replace regs reg_ra 0;
+ let sp = memsize in
+ Array.set regs reg_sp sp;
+ Array.set regs reg_fp sp;
+ Array.set regs reg_ra 0;
let codesize = List.fold_left (fun ofs (name, def) ->
match def with
| Gfun f ->
let funstart = ofs in
let funend = List.fold_left (fun ofs ins ->
- Hashtbl.replace code ofs ins;
+ code.(ofs) <- ins;
(* write dummy instruction in memory. *)
Mem.write_char mem ofs 0x90 >>! fun _ ->
+ begin match ins with
+ | LLabel l -> Hashtbl.replace labels l ofs
+ | _ -> ()
+ end;
ofs + 1
) ofs f.ltlfunbody in
Hashtbl.replace funs name {
@@ -180,32 +191,31 @@ let init_state memsize lp params =
funregalloc = f.ltlregalloc
};
funend
- ) 0 (("__halt", Gfun {ltlfunargs = 0;
- ltlfunbody = [LHalt];
- ltlfuninfo = [];
- ltlregalloc = [];
- })::lp)
+ ) 0 lp
in
let codesize = (codesize / 8 + 1) * 8 in
- Hashtbl.replace regs reg_gp codesize;
+ Array.set regs reg_gp codesize;
(* write arguments, relative to sp *)
List.iteri (fun i p ->
if i >= number_of_arguments_passed_in_registers
then begin
- let sp = Hashtbl.find regs reg_sp - !Archi.wordsize in
- Hashtbl.replace regs reg_sp sp;
+ let sp = Array.get regs reg_sp - !Archi.wordsize in
+ Array.set regs reg_sp sp;
Mem.write_bytes mem sp (split_bytes !Archi.wordsize p) >>!
ignore
end else
begin
- Hashtbl.replace regs (starting_arg_register + i) p
+ Array.set regs (starting_arg_register + i) p
end
) params;
let mem_next = ref (codesize + 8) in
Mem.write_bytes mem codesize (split_bytes !Archi.wordsize !mem_next) >>!
- fun _ -> { code; funs; mem ; regs ; numstep = ref 0}
+ fun _ ->
+ Printf.eprintf "numlabels = %d\n" (Hashtbl.length labels);
+ Printf.eprintf "labels = %s\n" (Hashtbl.keys labels |> List.of_enum |> String.concat ", ");
+ { code; funs; mem ; labels; regs ; numstep = ref 0}
let rec exec_ltl_at oc ip st =
@@ -220,5 +230,5 @@ let exec_ltl_prog oc lp memsize params : int option res =
| None -> Error (Format.sprintf "Could not find function main.")
| Some {funstart} ->
exec_ltl_at oc funstart st >>= fun st ->
- OK (Hashtbl.find_option st.regs reg_ret)
+ OK (Some (Array.get st.regs reg_ret))
diff --git a/src/main.ml b/src/main.ml
index f9a4a22..dcc6443 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -104,6 +104,7 @@ type run_result = {
retval: int option;
output: string;
error: string option;
+ time: float;
}
type compile_result = {
@@ -120,14 +121,16 @@ let results = ref []
let run step flag eval p =
if flag then begin
+ let starttime = Unix.gettimeofday () in
let res = match eval Format.str_formatter p !heapsize !params with
| exception e ->
Error (Printexc.to_string e)
| e -> e in
+ let timerun = Unix.gettimeofday () -. starttime in
begin match res with
| OK v ->
let output = Format.flush_str_formatter () in
- results := !results @ [RunRes { step ; retval = v; output; error = None}];
+ results := !results @ [RunRes { step ; retval = v; output; error = None; time = timerun}];
add_to_report step ("Run " ^ step) (
Paragraph
(
@@ -135,11 +138,12 @@ let run step flag eval p =
^ Printf.sprintf "Mem size : %d bytes<br>\n" !heapsize
^ Printf.sprintf "Return value : %s<br>\n" (match v with | Some v -> string_of_int v | _ -> "none")
^ Printf.sprintf "Output : <pre style=\"padding: 1em; background-color: #ccc;\">%s</pre>\n" output
+ ^ Printf.sprintf "Time : %f seconds<br>\n" timerun
)
)
| Error msg ->
let output = Format.flush_str_formatter () in
- results := !results @ [RunRes { step ; retval = None; output; error = Some msg}];
+ results := !results @ [RunRes { step ; retval = None; output; error = Some msg; time = timerun}];
add_to_report step ("Run " ^ step) (
Paragraph
(
@@ -148,6 +152,7 @@ let run step flag eval p =
^ Printf.sprintf "Return value : none<br>\n"
^ Printf.sprintf "Output : <pre style=\"padding: 1em; background-color: #ccc;\">%s</pre>\n" output
^ Printf.sprintf "Error : <pre style=\"padding: 1em; background-color: #fcc;\">\n%s</pre>\n" msg
+ ^ Printf.sprintf "Time : %f seconds<br>\n" timerun
)
)
@@ -369,11 +374,12 @@ let _ =
| Some s -> `String s
in
let j = `List (List.map (function
- | RunRes { step; retval; output; error; } ->
+ | RunRes { step; retval; output; error; time } ->
`Assoc [("runstep",`String step);
("retval", match retval with Some r -> `Int r | None -> `Null);
("output", `String output);
("error", jstring_of_ostring error);
+ ("time", `Float time)
]
| CompRes { step; error; data } ->
`Assoc [("compstep",`String step);
diff --git a/src/riscv.ml b/src/riscv.ml
index 185fd78..e4c426e 100644
--- a/src/riscv.ml
+++ b/src/riscv.ml
@@ -159,16 +159,18 @@ let riscv_load_args oc : unit res =
call atoi
sd a0, -8*arg(fp)
*)
- let l1 = nargs |>
+ let l1 = (nargs |>
List.map (fun i ->
[LConst(reg_a0, i);
LCall("load_int_arg");
- LBranch(Rceq, reg_a0, reg_zero, Printf.sprintf "riscv_load_arg_%d" i);
+ LBranch(Rceq, reg_a0, reg_zero, Printf.sprintf "riscv_load_arg_end");
LCall("atoi");
LStore(reg_fp, - !Archi.wordsize*i,
reg_a0, !Archi.wordsize);
- LLabel(Printf.sprintf "riscv_load_arg_%d" i);
- ]) in
+ ]))
+ @
+ [[LLabel(Printf.sprintf "riscv_load_arg_end")]]
+ in
(* for each arg in [1..8]
ld a{arg-1}, -8*arg(fp)
*)
diff --git a/src/utils.ml b/src/utils.ml
index f779879..a954803 100644
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -134,21 +134,22 @@ module Mem : sig
end = struct
type t = int array * int list ref * (int * int) list ref
let write_bytes (m,rl,wl) addr bytes =
- write_mem_bytes m addr bytes >>= fun w -> wl := !wl @ w; OK ()
+ write_mem_bytes m addr bytes >>= fun w ->
+ wl := w @ !wl; OK ()
let write_char (m,rl,wl) addr c =
- write_mem_char m addr c >>= fun w -> wl := !wl @ w; OK ()
+ write_mem_char m addr c >>= fun w -> wl := w @ !wl; OK ()
let read_bytes (m,rl,wl) addr len =
read_mem_bytes m addr len >>= fun (vl,addrl) ->
- rl := !rl @ addrl; OK vl
+ rl := addrl @ !rl ; OK vl
let read_bytes_as_int (m,rl,wl) addr len =
read_mem_bytes_as_int m addr len >>= fun (v,addrl) ->
- rl := !rl @ addrl; OK v
+ rl := addrl @ !rl; OK v
let read_char (m,rl,wl) addr =
read_mem_char m addr >>= fun (v,addrl) ->
- rl := !rl @ addrl; OK v
+ rl := addrl @ !rl; OK v
let init n = Array.init n (fun _ -> 0), ref [], ref []
- let read_log (_,rl,_) () = let r = !rl in rl := []; r
- let write_log (_,_,wl) () = let w = !wl in wl := []; w
+ let read_log (_,rl,_) () = let r = !rl in rl := []; List.rev r
+ let write_log (_,_,wl) () = let w = !wl in wl := []; List.rev w
end
let assoc_opti k l =
diff --git a/tests/test.py b/tests/test.py
index 5126c19..a0b2589 100755
--- a/tests/test.py
+++ b/tests/test.py
@@ -183,9 +183,10 @@ class CommandExecutor(Thread):
cls = ""
if cls == "good":
self.lastcorrectstep = curcol
- self.s += make_td(["Ret = {}.<br>Output = <pre>'{}'</pre>{}".
+ self.s += make_td(["Ret = {}.<br>Output = <pre>'{}'</pre>{}<br>Time: {:.2f} seconds.<br>".
format(r['retval'], r['output'],
- "Error: "+r['error'] if r['error'] != None else ""),
+ "Error: "+r['error'] if r['error'] != None else "",
+ r['time']),
"class=\"{}\"".format(cls)])
curcol+=1
elif "compstep" in r:
--
GitLab