From 1c6787216e2036ac40659538c452d70bf8bc0c98 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 2 Jun 2023 12:31:02 +0200
Subject: [PATCH] [config] Use %{config} also for driver locations in detection
config file.
---
config/caisar-detection-data.conf | 18 +++++++++---------
src/verification.ml | 16 +++++++---------
2 files changed, 16 insertions(+), 18 deletions(-)
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index b762961..c560676 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -50,7 +50,7 @@ version_switch = "--version"
version_regexp = "\\([0-9.+]+\\)"
version_ok = "1.0.+"
command = "%e %{nnet-onnx} %f --timeout %t --snc --initial-divides=4 --num-online-divides=4 --initial-timeout=0"
-driver = "caisar_drivers/marabou.drv"
+driver = "%{config}/drivers/marabou.drv"
use_at_auto_level = 1
[ATP pyrat]
@@ -61,7 +61,7 @@ version_switch = "--version"
version_regexp = "PyRAT \\([0-9.]+\\)"
version_ok = "1.1"
command = "%e -mp %{nnet-onnx} -pp %f --timeout %t"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
use_at_auto_level = 1
[ATP pyrat-vnnlib]
@@ -73,7 +73,7 @@ version_switch = "--version"
version_regexp = "PyRAT \\([0-9.]+\\)"
version_ok = "1.1"
command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono poly --split"
-driver = "caisar_drivers/pyrat_vnnlib.drv"
+driver = "%{config}/drivers/pyrat_vnnlib.drv"
use_at_auto_level = 1
[ATP pyrat-acas]
@@ -85,7 +85,7 @@ version_switch = "--version"
version_regexp = "PyRAT \\([0-9.]+\\)"
version_ok = "1.1"
command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono --split --scorer coef"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
use_at_auto_level = 1
[ATP nnenum]
@@ -95,7 +95,7 @@ version_switch = "--version"
version_regexp = "\\(dummy-version\\)"
version_ok = "dummy-version"
command = "%e %{nnet-onnx} %f"
-driver = "caisar_drivers/nnenum.drv"
+driver = "%{config}/drivers/nnenum.drv"
use_at_auto_level = 1
[ATP abcrown]
@@ -105,7 +105,7 @@ version_switch = "--version"
version_regexp = "\\(dummy-version\\)"
version_ok = "dummy-version"
command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %t"
-driver = "caisar_drivers/abcrown.drv"
+driver = "%{config}/drivers/abcrown.drv"
use_at_auto_level = 1
[ATP abcrown]
@@ -116,7 +116,7 @@ version_switch = "--version"
version_regexp = "\\(dummy-version\\)"
version_ok = "dummy-version"
command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --config %{config}/abcrown/acasxu.yaml --timeout %t"
-driver = "caisar_drivers/abcrown.drv"
+driver = "%{config}/drivers/abcrown.drv"
use_at_auto_level = 1
[ATP saver]
@@ -126,7 +126,7 @@ version_switch = "--version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)"
version_regexp = "\\(v[0-9.]+\\)"
version_ok = "v1.0"
command = "%e %{svm} %{dataset} %{abstraction} %{distance} %{epsilon}"
-driver = "caisar_drivers/saver.drv"
+driver = "%{config}/drivers/saver.drv"
use_at_auto_level = 1
[ATP aimos]
@@ -136,5 +136,5 @@ version_switch = "--version"
version_regexp = "AIMOS \\([0-9.]+\\)"
version_ok = "1.0"
command = "%e --config %{aimos_file} --no-verbose"
-driver = "caisar_drivers/aimos.drv"
+driver = "%{config}/drivers/aimos.drv"
use_at_auto_level = 1
diff --git a/src/verification.ml b/src/verification.ml
index 77f6e2b..93df264 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -341,15 +341,13 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
altern)
in
let driver =
- match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with
- | None -> Driver.load_driver_for_prover main env config_prover
- | Some file ->
- let file =
- Filename.concat
- (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
- file
- in
- Driver.load_driver_file_and_extras main env file
+ Re__Core.replace_string re_config ~by:config_site config_prover.driver
+ in
+ let driver =
+ if String.equal driver config_prover.driver
+ then Driver.load_driver_for_prover main env config_prover
+ else
+ Driver.load_driver_file_and_extras main env driver
config_prover.extra_drivers
in
let cwd, mstr_theory = open_file ?format env file in
--
GitLab