[sledge] Test infra improvements

Reviewed By: jvillard

Differential Revision: D25936865

fbshipit-source-id: c71fb73e5

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 )

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 =

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'

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 <timeout(sec)> <memout(MB)> <command> <testdir/testname>
+# usage: wrap.sh <timeout(sec)> <memout(GB)> <command> <testdir/testname>
 
 set -u
 
 timeout=$1
-memout=$(( $2*1024 ))
+memout=$(( $2*1024*1024 ))
 command=${@: 3: $#-3}
 test=${@: -1}