From 3c8dfce3c60953b5095f74d6d151f4a9266f9de4 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 25 Jun 2019 19:30:43 +0200
Subject: [PATCH] [Aorai] Add a check to prevent the use of metavariables with
non-deterministic automata
---
src/plugins/aorai/data_for_aorai.ml | 19 +++++++++++++++++++
.../tests/ya/metavariables-incompatible.i | 6 ++++++
.../tests/ya/metavariables-incompatible.ya | 9 +++++++++
.../metavariables-incompatible.res.oracle | 4 ++++
4 files changed, 38 insertions(+)
create mode 100644 src/plugins/aorai/tests/ya/metavariables-incompatible.i
create mode 100644 src/plugins/aorai/tests/ya/metavariables-incompatible.ya
create mode 100644 src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 24e1876a48b..56f2d69b042 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1536,9 +1536,28 @@ let type_cond_auto auto =
{ original_auto with states = List.rev states; trans = List.rev trans }
+(* Check Metavariable compatibility *)
+let checkMetavariableCompatibility auto =
+ let is_extended_trans trans =
+ match trans.cross with
+ | Otherwise -> false
+ | Seq [ elt ] ->
+ elt.nested <> [] || not (is_single elt)
+ | Seq _ -> true
+ in
+ let has_metavariables = not (Datatype.String.Map.is_empty auto.metavariables)
+ and deterministic = Aorai_option.Deterministic.get ()
+ and uses_extended_guards = List.exists is_extended_trans auto.trans in
+ if has_metavariables && (not deterministic || uses_extended_guards) then
+ Aorai_option.abort
+ "The use of metavariables is incompatible with non-deterministic \
+ automata, such as automa using extended transitions."
+
+
(** Stores the buchi automaton and its variables and
functions as it is returned by the parsing *)
let setAutomata auto =
+ checkMetavariableCompatibility auto;
let auto = type_cond_auto auto in
automata:=Some auto;
check_states "typed automata";
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
new file mode 100644
index 00000000000..e572c484699
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
@@ -0,0 +1,6 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void main(void) {}
+
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.ya b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya
new file mode 100644
index 00000000000..059f0d555ba
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya
@@ -0,0 +1,9 @@
+%init: a;
+%accept: b;
+%deterministic;
+
+$x : int;
+
+a : { CALL(main)* } -> b;
+
+b : -> b;
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
new file mode 100644
index 00000000000..cba15445f48
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/aorai/metavariables-incompatible.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions.
+[kernel] Plug-in aorai aborted: invalid user input.
--
GitLab