From 49d6b208ac32a71a592e25474dcbc6c24ad43fc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 20 Sep 2023 16:21:07 +0200
Subject: [PATCH] [autodetect] Detect binaries only in tests/bin path.
---
src/autodetect.ml | 25 ++++++++++++++++---------
tests/aimos.t | 1 +
tests/autodetect.t | 24 +-----------------------
tests/cvc5.t | 3 ++-
tests/dataset.t | 1 +
tests/define.t | 1 +
tests/interpretation_acasxu.t | 1 +
tests/interpretation_dataset.t | 1 +
tests/marabou.t | 1 +
tests/pyrat.t | 1 +
tests/pyrat_onnx.t | 1 +
tests/saver.t | 1 +
tests/verify_json.t | 1 +
tests/xgboost.t | 4 ++--
14 files changed, 31 insertions(+), 35 deletions(-)
diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3ab29fc..52f38e5 100644
--- a/src/autodetect.ml
+++ b/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
diff --git a/tests/aimos.t b/tests/aimos.t
index 0ac8203..a80cf6d 100644
--- a/tests/aimos.t
+++ b/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
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 5fee7ec..8d28c23 100644
--- a/tests/autodetect.t
+++ b/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
diff --git a/tests/cvc5.t b/tests/cvc5.t
index e55696f..cd2a68e 100644
--- a/tests/cvc5.t
+++ b/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
diff --git a/tests/dataset.t b/tests/dataset.t
index 0e96584..3a886a0 100644
--- a/tests/dataset.t
+++ b/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
diff --git a/tests/define.t b/tests/define.t
index b698beb..262c674 100644
--- a/tests/define.t
+++ b/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
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 28695a7..5f2dc73 100644
--- a/tests/interpretation_acasxu.t
+++ b/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
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 8ce1d60..e9551bf 100644
--- a/tests/interpretation_dataset.t
+++ b/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
diff --git a/tests/marabou.t b/tests/marabou.t
index 8ded847..bc9dc99 100644
--- a/tests/marabou.t
+++ b/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
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 4c36cd0..6a9ba93 100644
--- a/tests/pyrat.t
+++ b/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
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index f6512e2..422a318 100644
--- a/tests/pyrat_onnx.t
+++ b/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
diff --git a/tests/saver.t b/tests/saver.t
index a05fc8d..94d471b 100644
--- a/tests/saver.t
+++ b/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
diff --git a/tests/verify_json.t b/tests/verify_json.t
index 39773a8..e0cf12c 100644
--- a/tests/verify_json.t
+++ b/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:
diff --git a/tests/xgboost.t b/tests/xgboost.t
index ca7e090..de83fad 100644
--- a/tests/xgboost.t
+++ b/tests/xgboost.t
@@ -1,6 +1,6 @@
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
--
GitLab