diff --git a/sledge/report/sledge_report.ml b/sledge/report/sledge_report.ml index 43a22cddb..7b9c73b30 100644 --- a/sledge/report/sledge_report.ml +++ b/sledge/report/sledge_report.ml @@ -661,7 +661,8 @@ let cmp perf x y = if o <> 0 then o else match (List.hd x.status, List.hd y.status) with - | Some (Safe _ | Unsafe _ | Ok), Some (Safe _ | Unsafe _ | Ok) + | ( Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete) + , Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete) ) when perf -> ( match (x.times_deltas, y.times_deltas) with | Some xtd, Some ytd -> @@ -670,7 +671,8 @@ let cmp perf x y = | Some _, None -> 1 | None, Some _ -> -1 | None, None -> String.compare x.name y.name ) - | Some (Safe _ | Unsafe _ | Ok), Some (Safe _ | Unsafe _ | Ok) -> ( + | ( Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete) + , Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete) ) -> ( match (x.gcs_deltas, y.gcs_deltas) with | Some xgc, Some ygc -> -Float.( @@ -681,8 +683,8 @@ let cmp perf x y = | Some _, None -> 1 | None, Some _ -> -1 | None, None -> String.compare x.name y.name ) - | _, Some (Safe _ | Unsafe _ | Ok) -> -1 - | Some (Safe _ | Unsafe _ | Ok), _ -> 1 + | _, Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete) -> -1 + | Some (Safe _ | Unsafe _ | Ok | Unsound | Incomplete), _ -> 1 | s, t -> Option.compare (Ord.opp Report.compare_status) s t |> fun o -> if o <> 0 then o else String.compare x.name y.name ) diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 29bae90bb..a30f9f16a 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -126,7 +126,7 @@ let process_times () = ; cstime= tms_cstime } let gc_stats () = - let words_to_MB n = n /. float (Sys.word_size / 8) /. (1024. *. 1024.) in + let words_to_MB n = n *. float (Sys.word_size / 8) /. (1024. *. 1024.) in let ctrl = Gc.get () in let stat = Gc.quick_stat () in let allocated = diff --git a/sledge/test/Makefile b/sledge/test/Makefile index b84bdb0c6..77dc5f16f 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -10,15 +10,16 @@ CLANG_ARGS?=-O0 SLEDGE_DBG=$(CURDIR)/../_build/debug/cli/sledge_cli.exe SLEDGE_OPT=$(CURDIR)/../_build/release/cli/sledge_cli.exe -# additional arguments to pass to sledge translate, disassemble, analyze, and smt +# additional arguments to pass to sledge translate, disassemble, analyze, smt, and report SLEDGE_T_ARGS?= SLEDGE_D_ARGS?= SLEDGE_A_ARGS?=-bound 5 SLEDGE_S_ARGS?= +SLEDGE_R_ARGS?= # limits for each test run TIMEOUT?=300 -MEMOUT?=4096 +MEMOUT?=6 sledge_dbg=./wrap.sh $(TIMEOUT) $(MEMOUT) $(SLEDGE_DBG) sledge_opt=./wrap.sh $(TIMEOUT) $(MEMOUT) $(SLEDGE_OPT) @@ -98,7 +99,7 @@ baseline/translate.sexp: translate.sexp cp translate.sexp $@ translate.html: translate.sexp - $(sledge_report) html -baseline baseline/translate.sexp translate.sexp -output $@ + $(sledge_report) html $(SLEDGE_R_ARGS) -baseline baseline/translate.sexp translate.sexp -output $@ translate-status: translate.sexp $(sledge_report) status -baseline baseline/translate.sexp translate.sexp | column -ts$$'\t' @@ -150,19 +151,19 @@ SmtTests:=$(shell find smt -name '*.smt2' 2>/dev/null) smt: -parallel --bar $(sledge_dbg) smt $(SLEDGE_S_ARGS) ::: $(SmtTests) -parallel_sledge_opt_smt=parallel --shuf --bar $(sledge_opt) smt -append-report $(SLEDGE_S_ARGS) ::: +parallel_sledge_opt_smt=parallel --use-cores-instead-of-threads --shuf --bar $(sledge_opt) smt -append-report $(SLEDGE_S_ARGS) ::: smt-perf1: - @$(parallel_sledge_opt_smt) $(SmtTests) + -@$(parallel_sledge_opt_smt) $(SmtTests) smt-perf3: - @$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) + -@$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) smt-perf5: - @$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) + -@$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) smt-perf7: - @$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) + -@$(parallel_sledge_opt_smt) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) $(SmtTests) .PHONY: smt.sexp smt.sexp: @@ -172,7 +173,7 @@ baseline/smt.sexp: smt.sexp cp smt.sexp $@ smt.html: smt.sexp - $(sledge_report) html -baseline baseline/smt.sexp smt.sexp -output $@ + $(sledge_report) html $(SLEDGE_R_ARGS) -baseline baseline/smt.sexp smt.sexp -output $@ smt-status: smt.sexp $(sledge_report) status -baseline baseline/smt.sexp smt.sexp | column -ts$$'\t' @@ -194,7 +195,7 @@ baseline/llvm.sexp: llvm.sexp cp llvm.sexp $@ llvm.html: llvm.sexp - $(sledge_report) html -baseline baseline/llvm.sexp llvm.sexp -output $@ + $(sledge_report) html $(SLEDGE_R_ARGS) -baseline baseline/llvm.sexp llvm.sexp -output $@ llvm-status: llvm.sexp $(sledge_report) status -baseline baseline/llvm.sexp llvm.sexp | column -ts$$'\t' diff --git a/sledge/test/wrap.sh b/sledge/test/wrap.sh index cc271f30d..edc7c4f59 100755 --- a/sledge/test/wrap.sh +++ b/sledge/test/wrap.sh @@ -8,12 +8,12 @@ # wrap execution of sledge with time and memory limits # and add status entries to report in case of an unexpected exit -# usage: wrap.sh +# usage: wrap.sh set -u timeout=$1 -memout=$(( $2*1024 )) +memout=$(( $2*1024*1024 )) command=${@: 3: $#-3} test=${@: -1}