From cc4e446a2aaa9a79aa064f911b4e99ca2e7f2d95 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 18 Oct 2022 12:59:07 +0200
Subject: [PATCH] [cmdline] Move time and memory limit conversion functions
into main module.
---
src/main.ml | 64 +++++++++++++++++++++++++++++++++++++++-----
src/verification.ml | 59 ++--------------------------------------
src/verification.mli | 4 +--
3 files changed, 62 insertions(+), 65 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index cf20bdd..dc4fb18 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -87,11 +87,62 @@ let config detect () =
Whyconf.print_prover Pp.nothing)
provers))
+(* conversion string -> int for memlimit and timeout *)
+(* auxiliary functions, TODO move to a better place *)
+(* first, find the first non-numerical character, and return a couple of
+ substrings *)
+let rec find_first_non_num (s : string) (i : int) (m : int) =
+ (* MUST be called with m = String.length s*)
+ if i >= m
+ then i
+ else
+ match s.[i] with
+ | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' ->
+ find_first_non_num s (i + 1) m
+ | _ -> i
+
+let split_non_num (s : string) =
+ let m = String.length s in
+ let x = find_first_non_num s 0 m in
+ if x = m
+ then (s, "")
+ else (String.sub s ~pos:0 ~len:x, String.sub s ~pos:x ~len:(m - x))
+
+let find_mult_memlimit = function
+ | "" -> 1
+ | "M" | "MB" | "mega" | "megabytes" -> 1
+ | "G" | "GB" | "giga" | "gigabytes" -> 1000
+ | "T" | "TB" | "tera" | "terabytes" -> 1000000
+ | _ -> failwith "Unknown unit for memory limit"
+
+let find_mult_timeout = function
+ | "" -> 1
+ | "s" | "seconds" -> 1
+ | "min" | "minutes" -> 60
+ | "h" | "hours" -> 3600
+ | _ -> failwith "Unknown unit for timeout"
+
+let convert_memlimit (s : string option) : int option =
+ match s with
+ | None -> None
+ | Some s ->
+ let mem1, mem2 = split_non_num (String.strip s) in
+ Some (Int.of_string mem1 * find_mult_memlimit mem2)
+
+let convert_timelimit s =
+ match s with
+ | None -> None
+ | Some s ->
+ let time1, time2 = split_non_num (String.strip s) in
+ Some (Int.of_string time1 * find_mult_timeout time2)
+
let verify format loadpath memlimit timeout prover dataset_csv files =
let debug = log_level_is_debug () in
+ let memlimit = convert_memlimit memlimit in
+ let timelimit = convert_timelimit timeout in
List.iter
~f:
- (Verification.verify ~debug format loadpath ?memlimit ?timeout prover
+ (Verification.verify ~debug format loadpath ?memlimit ?timelimit prover
?dataset_csv)
files
@@ -164,7 +215,7 @@ let verify_cmd =
& opt (some string) None
& info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
in
- let timeout =
+ let timelimit =
let doc =
"Time limit. $(docv) is intended in seconds (s) by default, but \
minutes (m) and hours (h) may also be specified instead."
@@ -196,12 +247,13 @@ let verify_cmd =
Term.(
ret
(const
- (fun format loadpath memlimit timeout prover dataset_csv files _ ->
+ (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
`Ok
(exec_cmd cmdname (fun () ->
- verify format loadpath memlimit timeout prover dataset_csv files)))
- $ format $ loadpath $ memlimit $ timeout $ prover $ dataset_csv $ files
- $ setup_logs))
+ verify format loadpath memlimit timelimit prover dataset_csv
+ files)))
+ $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv
+ $ files $ setup_logs))
in
Cmd.v info term
diff --git a/src/verification.ml b/src/verification.ml
index 570f269..33ff2c4 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -136,69 +136,14 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
Fmt.(option ~none:nop (any " " ++ string))
additional_info)
-
-(* conversion string -> int for memlimit and timeout *)
-(* auxiliary functions, TODO move to a better place *)
- (* first, find the first non-numerical character, and return a couple of substrings *)
-let rec find_first_non_num (s:string) (i: int) (m:int) =
- (* MUST be called with m = String.length s*)
- if i >= m
- then i
- else
- begin
- match s.[i] with
- | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' -> find_first_non_num s (i+1) m
- | _ -> i
- end
-
-let split_non_num (s:string) =
- let m = String.length s in
- let x = find_first_non_num s 0 m in
- if x = m
- then (s,"")
- else (String.sub s ~pos:0 ~len:x, String.sub s ~pos:x ~len:(m-x))
-
-let find_mult_memlimit = function
- "" -> 1
- | "M" | "MB" | "mega" | "megabytes" -> 1
- | "G" | "GB" | "giga" | "gigabytes" -> 1000
- | "T" | "TB" | "tera" | "terabytes" -> 1000000
- | _ -> failwith "Unkown unit for memory limit"
-
-let find_mult_timeout = function
- "" -> 1
- | "s" | "seconds" -> 1
- | "min" | "minutes" -> 60
- | "h" | "hours" -> 3600
- | _ -> failwith "Unkown unit for timeout"
-
-let convert_memlimit (s:string option) : int option =
- match s with
- None -> None
- | Some s ->
- let (mem1,mem2) = split_non_num s in (*(String.trim s) in*)
- Some ((Int.of_string mem1) * (find_mult_memlimit mem2))
-
-let convert_timeout (s:string option) : int option=
- match s with
- None -> None
- | Some s ->
- let (time1,time2) = split_non_num s in
- Some ((Int.of_string time1) * (find_mult_timeout time2))
-
-
-let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
+let verify ?(debug = false) format loadpath ?memlimit ?timelimit prover
?dataset_csv file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
-
- let memlimit = convert_memlimit memlimit in
- let timeout = convert_timeout timeout in
-
let env, config = create_env ~debug loadpath in
let limit =
let main = Whyconf.get_main config in
let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
- let timelimit = Option.value timeout ~default:(Whyconf.timelimit main) in
+ let timelimit = Option.value timelimit ~default:(Whyconf.timelimit main) in
let def = Call_provers.empty_limit in
{
Call_provers.limit_time = timelimit;
diff --git a/src/verification.mli b/src/verification.mli
index 7c86cb5..5087e63 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -31,8 +31,8 @@ val verify :
?debug:bool ->
string option ->
string list ->
- ?memlimit:string ->
- ?timeout:string ->
+ ?memlimit:int ->
+ ?timelimit:int ->
Prover.t ->
?dataset_csv:string ->
File.t ->
--
GitLab