From c3b79e0caf84e40d3b669aa89dad5e2b15f6e328 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Fri, 3 Mar 2023 16:09:26 +0900
Subject: [PATCH] Update the test architecture to handle JSON config
---
README.md | 19 ++-
lustrec_tests/dune | 13 ++
.../Abs1_PP.LUSTREC.lus | 0
.../Assignment1.LUSTREC.lus | 0
.../BitwiseXOR_int8_PP.LUSTREC.lus | 0
.../Clock_PP.LUSTREC.lus | 0
.../ForEach1_PP.LUSTREC.lus | 0
.../LookupTable1D_2points_PP.LUSTREC.lus | 0
.../Product1.LUSTREC.lus | 0
.../SYNAPSE_1.lus | 0
.../UnitDelay_PP.LUSTREC.lus | 0
.../_6counter.lus | 0
.../clocks1.lus | 0
lustrec_tests/minimal_tests/config.json | 5 +
lustrec_tests/minimal_tests/dune | 1 +
.../hysteresis_1.lus | 0
.../inv_M_2x2.LUSTREC.lus | 0
.../test.ml | 0
.../two_counters.lus | 0
lustrec_tests/minimal_tests_O1/dune | 13 --
lustrec_tests/minimal_tests_O1/ignored | 0
.../minimal_tests_O2/Abs1_PP.LUSTREC.lus | 1 -
.../minimal_tests_O2/Assignment1.LUSTREC.lus | 1 -
.../BitwiseXOR_int8_PP.LUSTREC.lus | 1 -
.../minimal_tests_O2/Clock_PP.LUSTREC.lus | 1 -
.../minimal_tests_O2/ForEach1_PP.LUSTREC.lus | 1 -
.../LookupTable1D_2points_PP.LUSTREC.lus | 1 -
.../minimal_tests_O2/Product1.LUSTREC.lus | 1 -
lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus | 1 -
.../minimal_tests_O2/UnitDelay_PP.LUSTREC.lus | 1 -
lustrec_tests/minimal_tests_O2/_6counter.lus | 1 -
lustrec_tests/minimal_tests_O2/clocks1.lus | 1 -
lustrec_tests/minimal_tests_O2/dune | 13 --
.../minimal_tests_O2/hysteresis_1.lus | 1 -
lustrec_tests/minimal_tests_O2/ignored | 0
.../minimal_tests_O2/inv_M_2x2.LUSTREC.lus | 1 -
.../minimal_tests_O2/two_counters.lus | 1 -
.../minimal_tests_O3/Abs1_PP.LUSTREC.lus | 1 -
.../minimal_tests_O3/Assignment1.LUSTREC.lus | 1 -
.../BitwiseXOR_int8_PP.LUSTREC.lus | 1 -
.../minimal_tests_O3/Clock_PP.LUSTREC.lus | 1 -
.../minimal_tests_O3/ForEach1_PP.LUSTREC.lus | 1 -
.../LookupTable1D_2points_PP.LUSTREC.lus | 1 -
.../minimal_tests_O3/Product1.LUSTREC.lus | 1 -
lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus | 1 -
.../minimal_tests_O3/UnitDelay_PP.LUSTREC.lus | 1 -
lustrec_tests/minimal_tests_O3/_6counter.lus | 1 -
lustrec_tests/minimal_tests_O3/clocks1.lus | 1 -
lustrec_tests/minimal_tests_O3/dune | 13 --
.../minimal_tests_O3/hysteresis_1.lus | 1 -
lustrec_tests/minimal_tests_O3/ignored | 0
.../minimal_tests_O3/inv_M_2x2.LUSTREC.lus | 1 -
lustrec_tests/minimal_tests_O3/test.ml | 1 -
.../minimal_tests_O3/two_counters.lus | 1 -
.../Abs1_PP.LUSTREC.lus | 1 -
.../Assignment1.LUSTREC.lus | 1 -
.../BitwiseXOR_int8_PP.LUSTREC.lus | 1 -
.../Clock_PP.LUSTREC.lus | 1 -
.../ForEach1_PP.LUSTREC.lus | 1 -
.../LookupTable1D_2points_PP.LUSTREC.lus | 1 -
.../Product1.LUSTREC.lus | 1 -
.../SYNAPSE_1.lus | 1 -
.../UnitDelay_PP.LUSTREC.lus | 1 -
.../_6counter.lus | 1 -
.../clocks1.lus | 1 -
.../minimal_tests_wo_optimizations/dune | 13 --
.../hysteresis_1.lus | 1 -
.../minimal_tests_wo_optimizations/ignored | 0
.../inv_M_2x2.LUSTREC.lus | 1 -
.../minimal_tests_wo_optimizations/test.ml | 1 -
.../two_counters.lus | 1 -
lustrec_tests/offline_tests/config.json | 5 +
lustrec_tests/offline_tests/dune | 14 +-
lustrec_tests/stopwatch_test/config.json | 4 +
lustrec_tests/stopwatch_test/dune | 1 +
.../simple_stopwatch.lus | 0
.../test.ml | 0
lustrec_tests/stopwatch_test_O1/dune | 13 --
lustrec_tests/stopwatch_test_O1/ignored | 0
lustrec_tests/stopwatch_test_O1/test.ml | 1 -
lustrec_tests/stopwatch_test_O2/dune | 13 --
lustrec_tests/stopwatch_test_O2/ignored | 0
.../stopwatch_test_O2/simple_stopwatch.lus | 1 -
lustrec_tests/stopwatch_test_O2/test.ml | 1 -
lustrec_tests/stopwatch_test_O3/dune | 13 --
lustrec_tests/stopwatch_test_O3/ignored | 0
.../stopwatch_test_O3/simple_stopwatch.lus | 1 -
lustrec_tests/stopwatch_test_O3/test.ml | 1 -
.../stopwatch_test_wo_optimizations/dune | 13 --
.../stopwatch_test_wo_optimizations/ignored | 0
.../simple_stopwatch.lus | 1 -
.../stopwatch_test_wo_optimizations/test.ml | 1 -
lustrec_tests/test.ml | 131 +++++++++++-------
93 files changed, 124 insertions(+), 224 deletions(-)
create mode 100644 lustrec_tests/dune
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/Abs1_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/Assignment1.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/BitwiseXOR_int8_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/Clock_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/ForEach1_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/LookupTable1D_2points_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/Product1.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/SYNAPSE_1.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/UnitDelay_PP.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/_6counter.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/clocks1.lus (100%)
create mode 100644 lustrec_tests/minimal_tests/config.json
create mode 120000 lustrec_tests/minimal_tests/dune
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/hysteresis_1.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/inv_M_2x2.LUSTREC.lus (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/test.ml (100%)
rename lustrec_tests/{minimal_tests_O1 => minimal_tests}/two_counters.lus (100%)
delete mode 100644 lustrec_tests/minimal_tests_O1/dune
delete mode 100644 lustrec_tests/minimal_tests_O1/ignored
delete mode 120000 lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/_6counter.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/clocks1.lus
delete mode 100644 lustrec_tests/minimal_tests_O2/dune
delete mode 120000 lustrec_tests/minimal_tests_O2/hysteresis_1.lus
delete mode 100644 lustrec_tests/minimal_tests_O2/ignored
delete mode 120000 lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O2/two_counters.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/_6counter.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/clocks1.lus
delete mode 100644 lustrec_tests/minimal_tests_O3/dune
delete mode 120000 lustrec_tests/minimal_tests_O3/hysteresis_1.lus
delete mode 100644 lustrec_tests/minimal_tests_O3/ignored
delete mode 120000 lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_O3/test.ml
delete mode 120000 lustrec_tests/minimal_tests_O3/two_counters.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus
delete mode 100644 lustrec_tests/minimal_tests_wo_optimizations/dune
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus
delete mode 100644 lustrec_tests/minimal_tests_wo_optimizations/ignored
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/test.ml
delete mode 120000 lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus
create mode 100644 lustrec_tests/offline_tests/config.json
mode change 100644 => 120000 lustrec_tests/offline_tests/dune
create mode 100644 lustrec_tests/stopwatch_test/config.json
create mode 120000 lustrec_tests/stopwatch_test/dune
rename lustrec_tests/{stopwatch_test_O1 => stopwatch_test}/simple_stopwatch.lus (100%)
rename lustrec_tests/{minimal_tests_O2 => stopwatch_test}/test.ml (100%)
delete mode 100644 lustrec_tests/stopwatch_test_O1/dune
delete mode 100644 lustrec_tests/stopwatch_test_O1/ignored
delete mode 120000 lustrec_tests/stopwatch_test_O1/test.ml
delete mode 100644 lustrec_tests/stopwatch_test_O2/dune
delete mode 100644 lustrec_tests/stopwatch_test_O2/ignored
delete mode 120000 lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus
delete mode 120000 lustrec_tests/stopwatch_test_O2/test.ml
delete mode 100644 lustrec_tests/stopwatch_test_O3/dune
delete mode 100644 lustrec_tests/stopwatch_test_O3/ignored
delete mode 120000 lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus
delete mode 120000 lustrec_tests/stopwatch_test_O3/test.ml
delete mode 100644 lustrec_tests/stopwatch_test_wo_optimizations/dune
delete mode 100644 lustrec_tests/stopwatch_test_wo_optimizations/ignored
delete mode 120000 lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus
delete mode 120000 lustrec_tests/stopwatch_test_wo_optimizations/test.ml
diff --git a/README.md b/README.md
index 4c47961f..8578ceb2 100644
--- a/README.md
+++ b/README.md
@@ -155,19 +155,30 @@ apt install xsltproc
Then launch tests:
```
-dune build @tests/regression_tests/runtest --no-buffer
+dune runtest tests/regression_tests --no-buffer
```
### ACSL verification tests
+To launch verification tests, create a directory `<my_dir>/` in
+`lustrec_tests/`. The directory must contain symbolic links to
+`lustrec_tests/{test.ml,dune}` and to relevant Lustre files in
+`lustrec_tests/lustre_files`, and a JSON configuration file `config.json`. See
+`lustrec_tests/{stopwatch_test,minimal_tests,offline_tests}` for example setups.
+The fields of the configuration file are all optional (default values are
+provided).
+
+To launch the tests:
```
-dune build @offline_tests/runtest --no-buffer
+dune runtest lustrec_tests/<my_dir> --no-buffer --display quiet
```
+The results can be found in the `results/` directory.
+
## Developing and hacking LustreC
If you want to hack LustreC, you should use
-[dune](https://dune.readthedocs.io/en/latest/ "Link to dune
-documentation") to build and execute it.
+[dune](https://dune.readthedocs.io/en/latest/ "Link to dune documentation") to
+build and execute it.
To build LustreC with dune:
diff --git a/lustrec_tests/dune b/lustrec_tests/dune
new file mode 100644
index 00000000..5b79b1ca
--- /dev/null
+++ b/lustrec_tests/dune
@@ -0,0 +1,13 @@
+(env
+ (dev
+ (flags (:standard -w -32))))
+
+(test
+ (name test)
+ (libraries re unix yojson)
+ (deps
+ (:lus (glob_files *.lus))
+ (:cfg config.json)
+ (glob_files *)) ; to include `ignored` if its present
+ (action
+ (run %{test} %{project_root} %{bin:lustrec} %{cfg} "%{lus}")))
diff --git a/lustrec_tests/minimal_tests_O1/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/Abs1_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Abs1_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Abs1_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests/Assignment1.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Assignment1.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Assignment1.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/BitwiseXOR_int8_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/BitwiseXOR_int8_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/BitwiseXOR_int8_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/Clock_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Clock_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Clock_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/ForEach1_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/ForEach1_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/ForEach1_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/LookupTable1D_2points_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/LookupTable1D_2points_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/LookupTable1D_2points_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests/Product1.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Product1.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Product1.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/SYNAPSE_1.lus b/lustrec_tests/minimal_tests/SYNAPSE_1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/SYNAPSE_1.lus
rename to lustrec_tests/minimal_tests/SYNAPSE_1.lus
diff --git a/lustrec_tests/minimal_tests_O1/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/UnitDelay_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/UnitDelay_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/UnitDelay_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/_6counter.lus b/lustrec_tests/minimal_tests/_6counter.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/_6counter.lus
rename to lustrec_tests/minimal_tests/_6counter.lus
diff --git a/lustrec_tests/minimal_tests_O1/clocks1.lus b/lustrec_tests/minimal_tests/clocks1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/clocks1.lus
rename to lustrec_tests/minimal_tests/clocks1.lus
diff --git a/lustrec_tests/minimal_tests/config.json b/lustrec_tests/minimal_tests/config.json
new file mode 100644
index 00000000..75d2d8ea
--- /dev/null
+++ b/lustrec_tests/minimal_tests/config.json
@@ -0,0 +1,5 @@
+{
+ "initial_timeout": 240,
+ "optimization_level": 1,
+ "ignored_file": null
+}
diff --git a/lustrec_tests/minimal_tests/dune b/lustrec_tests/minimal_tests/dune
new file mode 120000
index 00000000..55afef87
--- /dev/null
+++ b/lustrec_tests/minimal_tests/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O1/hysteresis_1.lus b/lustrec_tests/minimal_tests/hysteresis_1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/hysteresis_1.lus
rename to lustrec_tests/minimal_tests/hysteresis_1.lus
diff --git a/lustrec_tests/minimal_tests_O1/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests/inv_M_2x2.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/inv_M_2x2.LUSTREC.lus
rename to lustrec_tests/minimal_tests/inv_M_2x2.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/test.ml b/lustrec_tests/minimal_tests/test.ml
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/test.ml
rename to lustrec_tests/minimal_tests/test.ml
diff --git a/lustrec_tests/minimal_tests_O1/two_counters.lus b/lustrec_tests/minimal_tests/two_counters.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/two_counters.lus
rename to lustrec_tests/minimal_tests/two_counters.lus
diff --git a/lustrec_tests/minimal_tests_O1/dune b/lustrec_tests/minimal_tests_O1/dune
deleted file mode 100644
index 954cbd74..00000000
--- a/lustrec_tests/minimal_tests_O1/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O1")))
diff --git a/lustrec_tests/minimal_tests_O1/ignored b/lustrec_tests/minimal_tests_O1/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076..00000000
--- a/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53d..00000000
--- a/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f..00000000
--- a/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046..00000000
--- a/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea31..00000000
--- a/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff..00000000
--- a/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9f..00000000
--- a/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00..00000000
--- a/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f64..00000000
--- a/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/_6counter.lus b/lustrec_tests/minimal_tests_O2/_6counter.lus
deleted file mode 120000
index b146d803..00000000
--- a/lustrec_tests/minimal_tests_O2/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/clocks1.lus b/lustrec_tests/minimal_tests_O2/clocks1.lus
deleted file mode 120000
index b0c8f629..00000000
--- a/lustrec_tests/minimal_tests_O2/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/dune b/lustrec_tests/minimal_tests_O2/dune
deleted file mode 100644
index 4a6e21dd..00000000
--- a/lustrec_tests/minimal_tests_O2/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O2")))
diff --git a/lustrec_tests/minimal_tests_O2/hysteresis_1.lus b/lustrec_tests/minimal_tests_O2/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a..00000000
--- a/lustrec_tests/minimal_tests_O2/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/ignored b/lustrec_tests/minimal_tests_O2/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699..00000000
--- a/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/two_counters.lus b/lustrec_tests/minimal_tests_O2/two_counters.lus
deleted file mode 120000
index 65993869..00000000
--- a/lustrec_tests/minimal_tests_O2/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076..00000000
--- a/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53d..00000000
--- a/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f..00000000
--- a/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046..00000000
--- a/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea31..00000000
--- a/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff..00000000
--- a/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9f..00000000
--- a/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00..00000000
--- a/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f64..00000000
--- a/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/_6counter.lus b/lustrec_tests/minimal_tests_O3/_6counter.lus
deleted file mode 120000
index b146d803..00000000
--- a/lustrec_tests/minimal_tests_O3/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/clocks1.lus b/lustrec_tests/minimal_tests_O3/clocks1.lus
deleted file mode 120000
index b0c8f629..00000000
--- a/lustrec_tests/minimal_tests_O3/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/dune b/lustrec_tests/minimal_tests_O3/dune
deleted file mode 100644
index 770302df..00000000
--- a/lustrec_tests/minimal_tests_O3/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O3")))
diff --git a/lustrec_tests/minimal_tests_O3/hysteresis_1.lus b/lustrec_tests/minimal_tests_O3/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a..00000000
--- a/lustrec_tests/minimal_tests_O3/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/ignored b/lustrec_tests/minimal_tests_O3/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699..00000000
--- a/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/test.ml b/lustrec_tests/minimal_tests_O3/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/minimal_tests_O3/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/two_counters.lus b/lustrec_tests/minimal_tests_O3/two_counters.lus
deleted file mode 120000
index 65993869..00000000
--- a/lustrec_tests/minimal_tests_O3/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53d..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea31..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9f..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f64..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus b/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus
deleted file mode 120000
index b146d803..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus b/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus
deleted file mode 120000
index b0c8f629..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/dune b/lustrec_tests/minimal_tests_wo_optimizations/dune
deleted file mode 100644
index fd6ebfc4..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O-1")))
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus b/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/ignored b/lustrec_tests/minimal_tests_wo_optimizations/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/test.ml b/lustrec_tests/minimal_tests_wo_optimizations/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus b/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus
deleted file mode 120000
index 65993869..00000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/offline_tests/config.json b/lustrec_tests/offline_tests/config.json
new file mode 100644
index 00000000..e22e1630
--- /dev/null
+++ b/lustrec_tests/offline_tests/config.json
@@ -0,0 +1,5 @@
+{
+ "initial_timeout": 30,
+ "optimization_level": 1,
+ "ignored_file": "ignored"
+}
diff --git a/lustrec_tests/offline_tests/dune b/lustrec_tests/offline_tests/dune
deleted file mode 100644
index 776c4856..00000000
--- a/lustrec_tests/offline_tests/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "offline_tests" 15360 "O2")))
diff --git a/lustrec_tests/offline_tests/dune b/lustrec_tests/offline_tests/dune
new file mode 120000
index 00000000..55afef87
--- /dev/null
+++ b/lustrec_tests/offline_tests/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test/config.json b/lustrec_tests/stopwatch_test/config.json
new file mode 100644
index 00000000..45a14ce0
--- /dev/null
+++ b/lustrec_tests/stopwatch_test/config.json
@@ -0,0 +1,4 @@
+{
+ "initial_timeout": 60,
+ "optimization_level": 1
+}
diff --git a/lustrec_tests/stopwatch_test/dune b/lustrec_tests/stopwatch_test/dune
new file mode 120000
index 00000000..55afef87
--- /dev/null
+++ b/lustrec_tests/stopwatch_test/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O1/simple_stopwatch.lus b/lustrec_tests/stopwatch_test/simple_stopwatch.lus
similarity index 100%
rename from lustrec_tests/stopwatch_test_O1/simple_stopwatch.lus
rename to lustrec_tests/stopwatch_test/simple_stopwatch.lus
diff --git a/lustrec_tests/minimal_tests_O2/test.ml b/lustrec_tests/stopwatch_test/test.ml
similarity index 100%
rename from lustrec_tests/minimal_tests_O2/test.ml
rename to lustrec_tests/stopwatch_test/test.ml
diff --git a/lustrec_tests/stopwatch_test_O1/dune b/lustrec_tests/stopwatch_test_O1/dune
deleted file mode 100644
index 9b925493..00000000
--- a/lustrec_tests/stopwatch_test_O1/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O1")))
diff --git a/lustrec_tests/stopwatch_test_O1/ignored b/lustrec_tests/stopwatch_test_O1/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/stopwatch_test_O1/test.ml b/lustrec_tests/stopwatch_test_O1/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/stopwatch_test_O1/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O2/dune b/lustrec_tests/stopwatch_test_O2/dune
deleted file mode 100644
index a3f05791..00000000
--- a/lustrec_tests/stopwatch_test_O2/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O2")))
diff --git a/lustrec_tests/stopwatch_test_O2/ignored b/lustrec_tests/stopwatch_test_O2/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f..00000000
--- a/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O2/test.ml b/lustrec_tests/stopwatch_test_O2/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/stopwatch_test_O2/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O3/dune b/lustrec_tests/stopwatch_test_O3/dune
deleted file mode 100644
index 58e70106..00000000
--- a/lustrec_tests/stopwatch_test_O3/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O3")))
diff --git a/lustrec_tests/stopwatch_test_O3/ignored b/lustrec_tests/stopwatch_test_O3/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f..00000000
--- a/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O3/test.ml b/lustrec_tests/stopwatch_test_O3/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/stopwatch_test_O3/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/dune b/lustrec_tests/stopwatch_test_wo_optimizations/dune
deleted file mode 100644
index 6dc4eac5..00000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O-1")))
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/ignored b/lustrec_tests/stopwatch_test_wo_optimizations/ignored
deleted file mode 100644
index e69de29b..00000000
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f..00000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/test.ml b/lustrec_tests/stopwatch_test_wo_optimizations/test.ml
deleted file mode 120000
index 9536c050..00000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/test.ml b/lustrec_tests/test.ml
index 61688931..c7b9c6e5 100644
--- a/lustrec_tests/test.ml
+++ b/lustrec_tests/test.ml
@@ -1,6 +1,8 @@
open Format
open Unix
+module Y = Yojson.Basic
+
module S = struct
include Set.Make (String)
@@ -52,29 +54,22 @@ let empty_report =
ninits = S.empty;
}
-let initial_timeout = int_of_string Sys.argv.(5)
-let optimization_level = match Sys.argv.(6) with
- | "O2" -> None
- | "O-1" -> Some (-1)
- | "O1" -> Some 1
- | "O3" -> Some 3
- | _ -> failwith
- "optimization option not supported. Choose between O-1, O1, O2, O3"
-let result_dir = "../../../../results/"
-let _ = try Unix.mkdir result_dir 0o755 with _ -> ()
-let dir = result_dir ^ Sys.argv.(4) ^ "_" ^
- match Sys.argv.(6) with
- | "O-1" -> "wo_optimizations"
- | other -> other
-let _ = try Unix.mkdir dir 0o755 with _ -> ()
-let report_f = Filename.concat dir "report"
+type config = {
+ initial_timeout: int;
+ optimization_level: int;
+ ignored_file: string option;
+ results_directory: string;
+}
+
+let report_file cfg = Filename.concat cfg.results_directory "report"
+
let section h = "# " ^ h
let end_section = "##"
let compiled_section = section "COMPILED"
let ninit_section = section "BAD_INIT"
-let next_timeout r =
- 2 * M.fold (fun i _ n -> max i n) r.verified (initial_timeout / 2)
+let next_timeout cfg r =
+ 2 * M.fold (fun i _ n -> max i n) r.verified (cfg.initial_timeout / 2)
let timeout_section i = section (sprintf "TIMEOUT %d" i)
@@ -111,9 +106,9 @@ let is_failed report f = STF.exists (fun (x, _) -> x = f) report.failed
let add_failed report ?goals f =
{ report with failed = STF.add (f, goals) report.failed }
-let parse_report () =
+let parse_report cfg =
try
- let ic = open_in report_f in
+ let ic = open_in (report_file cfg) in
let rec read_compiled r =
try
match input_line ic with
@@ -229,8 +224,8 @@ let pp_report fmt report =
pp_verified
report
-let write_report report =
- let oc = open_out report_f in
+let write_report cfg report =
+ let oc = open_out (report_file cfg) in
let fmt = formatter_of_out_channel oc in
pp_report fmt report;
close_out oc
@@ -279,14 +274,15 @@ let print_result p f fmt_str check =
let print_results ok ko w n =
printf "OK: @{<green>%d@} (@{<red>%d@} + @{<magenta>%d@}) / %d@." ok ko w n
-let lustrec_params f =
- let ps = [ "-acsl-spec"; "-d"; dir; f ] in
- Option.fold
- ~none:ps
- ~some:(fun x -> "-O" :: string_of_int x :: ps)
- optimization_level
+let lustrec_params cfg f =
+ [
+ "-acsl-spec";
+ "-d"; cfg.results_directory;
+ "-O"; cfg.optimization_level |> string_of_int;
+ f
+ ]
-let compile report lustrec fs =
+let compile cfg report lustrec fs =
printf "@.%a@." pp_header "Compilation tests";
max_l :=
List.fold_left
@@ -316,7 +312,7 @@ let compile report lustrec fs =
else if is_ninit report f then ninit report
else
let cmd =
- Filename.quote_command ~stderr:err_f lustrec (lustrec_params f)
+ Filename.quote_command ~stderr:err_f lustrec (lustrec_params cfg f)
in
let ic = open_process_in cmd in
let b =
@@ -329,7 +325,7 @@ let compile report lustrec fs =
else fail report log
in
print_result p f fmt_str check;
- write_report report;
+ write_report cfg report;
report, ok, ko, ninits, i')
(report, 0, 0, 0, 0)
fs
@@ -429,7 +425,7 @@ let rec rmrf path =
else Sys.remove path
with _ -> ()
-let rec verify report timeout fs =
+let rec verify cfg report timeout fs =
if fs <> [] then (
printf
"@.%a@."
@@ -441,7 +437,7 @@ let rec verify report timeout fs =
List.fold_left
(fun (report, ok, ko, tm, i, fs) f ->
let f' = Filename.remove_extension f ^ ".c" in
- let f'' = Filename.concat dir f' in
+ let f'' = Filename.concat cfg.results_directory f' in
let i' = i + 1 in
let p = float_of_int i' *. 100. /. n_f in
let success ?(already = false) r : _ * _ * _ * _ * _ format * _ * _ =
@@ -495,35 +491,66 @@ let rec verify report timeout fs =
fail (add_failed report f'))
in
print_result p f' fmt_str check;
- write_report report;
+ write_report cfg report;
report, ok, ko, tm, i', fs)
(report, 0, 0, 0, 0, [])
fs
in
print_results ok ko tm n;
- verify report (timeout * 2) fs)
+ verify cfg report (timeout * 2) fs)
let print_ignored fs =
- printf
- "@.@[<v 2>%a@;%a@]@."
- pp_header
- "Ignored tests"
- (pp_print_list pp_print_string)
- fs
+ if fs <> [] then
+ printf
+ "@.@[<v 2>%a@;%a@]@."
+ pp_header
+ "Ignored tests"
+ (pp_print_list pp_print_string)
+ fs
+
+let read_config root =
+ let open Yojson.Basic.Util in
+ let json = Sys.argv.(3) |> Y.from_file in
+ let get field f = json |> member field |> f in
+ let get_default field f default =
+ Option.fold ~none:default ~some:Fun.id (get field (to_option f))
+ in
+ let tests_directory = Sys.getcwd () |> Filename.basename in
+ let optimization_level = get_default "optimization_level" to_int 2 in
+ let result_dir = root ^ "/../../results/" in
+ (try Unix.mkdir result_dir 0o755 with _ -> ());
+ let results_directory =
+ result_dir ^ tests_directory ^ "_" ^
+ (if optimization_level < 0 then "wo_optimization"
+ else "O" ^ string_of_int optimization_level)
+ in
+ (try Unix.mkdir results_directory 0o755 with _ -> ());
+ {
+ initial_timeout = get_default "initial_timeout" to_int 30;
+ optimization_level;
+ results_directory;
+ ignored_file = get "ignored_file" to_string_option;
+ }
let () =
- let lustrec = Sys.argv.(1) in
- let lus_fs = Sys.argv.(2) |> Re.Str.(split (regexp_string " ")) in
- let ignored_f = Sys.argv.(3) in
+ let root = Sys.argv.(1) in
+ let lustrec = Sys.argv.(2) in
+ let cfg = read_config root in
+ let lus_fs = Sys.argv.(4) |> Re.Str.(split (regexp_string " ")) in
let ignored_fs =
- let ic = open_in ignored_f in
- let rec read fs = try read (input_line ic :: fs) with End_of_file -> fs in
- let fs = read [] in
- close_in ic;
- fs
+ Option.fold ~none:[]
+ ~some:(fun ignored_f ->
+ let ic = open_in ignored_f in
+ let rec read fs =
+ try read (input_line ic :: fs) with End_of_file -> fs
+ in
+ let fs = read [] in
+ close_in ic;
+ fs)
+ cfg.ignored_file
in
- let report = parse_report () in
- let report = compile report lustrec lus_fs in
+ let report = parse_report cfg in
+ let report = compile cfg report lustrec lus_fs in
let ignored_fs =
ignored_fs @ List.map Filename.chop_extension (S.elements report.ninits)
in
@@ -536,4 +563,4 @@ let () =
(fun f -> not (mem (Filename.chop_extension f) ignored_fs))
lus_fs))
in
- verify report (next_timeout report) lus_fs
+ verify cfg report (next_timeout cfg report) lus_fs
--
GitLab