[autodetect] Detect binaries only in tests/bin path.

src/autodetect.ml

@@ -30,6 +30,13 @@ let rec lookup_file dirs filename =
     let file = Stdlib.Filename.concat dir filename in
     if Stdlib.Sys.file_exists file then file else lookup_file dirs filename
 
+let filter_binaries =
+  let d = lazy (Sys.getenv "CAISAR_AUTODETECT_TEST") in
+  fun path ->
+    match Lazy.force d with
+    | Some d -> String.equal (Stdlib.Filename.dirname path) d
+    | None -> true
+
 let autodetection () =
   let debug = Logging.(is_debug_level src_autodetect) in
   if debug then Debug.set_flag Autodetection.debug;
@@ -39,15 +46,15 @@ let autodetection () =
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
   let provers = Autodetection.find_provers data in
   let provers =
-    List.fold_left ~init:[] provers ~f:(fun acc (path, name, version) ->
-      {
-        Autodetection.Partial.name;
-        path;
-        version;
-        shortcut = None;
-        manual = false;
-      }
-      :: acc)
+    List.filter_map provers ~f:(fun (path, name, version) ->
+      Option.some_if (filter_binaries path)
+        {
+          Autodetection.Partial.name;
+          path;
+          version;
+          shortcut = None;
+          manual = false;
+        })
   in
   let config = Whyconf.init_config (Some Stdlib.Filename.null) in
   let provers = Autodetection.compute_builtin_prover provers config data in

tests/aimos.t

@@ -11,6 +11,7 @@ Test verify
   AIMOS 1.0
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
   > theory ACASXU_P5

tests/autodetect.t

@@ -32,29 +32,7 @@ Test autodetect
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar config -d --ltag=Autodetect -v 2>&1 | ./filter_tmpdir.sh
-  <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/aimos --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/abcrown.sh --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
-  <autodetect>Run: ($TESTCASE_ROOT/bin/cvc5 --version) > $TMPFILE 2>&1
-  <autodetect>0 prover(s) added
-  <autodetect>Generating strategies:
-  <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
-  <autodetect>Found prover CVC5 version 1.0.2, OK.
-  <autodetect>Found prover Marabou version 1.0.+, OK.
-  <autodetect>Found prover PyRAT version 1.1, OK.
-  <autodetect>Found prover PyRAT version 1.1 (alternative: VNNLIB)
-  <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
-  <autodetect>Found prover nnenum version dummy-version, OK.
-  <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
-  <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
-  <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>Found prover AIMOS version 1.0, OK.
-  <autodetect>11 prover(s) added
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin caisar config -d -v 2>&1 | ./filter_tmpdir.sh
   AIMOS 1.0
   Alt-Ergo 2.4.0
   CVC5 1.0.2

tests/cvc5.t

@@ -5,6 +5,7 @@ Test verify
   This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory CVC5
@@ -231,4 +232,4 @@ Test verify
   (check-sat)
   (get-info :reason-unknown)
   
-  Goal G: Unknown (unknown)
+  Goal G: Timeout

tests/dataset.t

@@ -13,6 +13,7 @@ Test verify on dataset
   1.0.+
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T

tests/define.t

@@ -6,6 +6,7 @@ Test interpretation of on-the-fly definition of toplevel constants
   PyRAT 1.1
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ cat > file.mlw <<EOF
   > theory T

tests/interpretation_acasxu.t

@@ -6,6 +6,7 @@ Test interpret on acasxu
   PyRAT 1.1
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T

tests/interpretation_dataset.t

@@ -10,6 +10,7 @@ Test interpret on dataset
   1.0.+
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T

tests/marabou.t

@@ -5,6 +5,7 @@ Test verify
   1.0.+
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T

tests/pyrat.t

@@ -5,6 +5,7 @@ Test verify
   PyRAT 1.1
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory PyRAT

tests/pyrat_onnx.t

@@ -5,6 +5,7 @@ Test verify
   PyRAT 1.1
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory PyRAT_ONNX

tests/saver.t

@@ -10,6 +10,7 @@ Test verify
   v1.0
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify -L . --format whyml --prover=SAVer --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T

tests/verify_json.t

@@ -13,6 +13,7 @@ Test verify-json
   PyRAT 1.1
 
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify-json --ltag=ProverSpec config.json 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:

tests/xgboost.t

 Test verify
   $ PATH=$(pwd)/bin:$PATH
+  $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
 
   $ caisar verify-xgboost ../lib/xgboost/example/california.json ../lib/xgboost/example/california.csv --prover CVC5 2>&1 | ./filter_tmpdir.sh
-  result: Unknown
-  (unknown)
+  result: Valid