From 513e5b95ee89723f3a2ef52852e5edfd13225526 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 25 Sep 2020 19:13:51 +0200
Subject: [PATCH] [aorai] fixes bug in generation of transition functions
when an action is required for a transition in non-deterministic mode, it was
done before the test for updating the boolean variables representing active
state, leading to a possibly incorrect decision when said test depends on the
value of the variable modified by the action
---
src/plugins/aorai/aorai_utils.ml | 19 +++++++++++--------
.../aorai/oracle/loop_bts1050.res.oracle | 6 +++---
.../aorai/tests/aorai/oracle/seq.res.oracle | 8 ++++----
.../tests/aorai/oracle/seq_loop.res.oracle | 6 +++---
.../oracle_prove/loop_bts1050.res.oracle | 2 --
.../tests/aorai/oracle_prove/seq.res.oracle | 2 --
.../aorai/oracle_prove/seq_loop.res.oracle | 2 --
7 files changed, 21 insertions(+), 24 deletions(-)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index c4a7cda302f..44ef64c7d1d 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1822,14 +1822,17 @@ let mk_stmt loc (states, tr) f fst status ((st,_) as state) res =
(List.rev exp_from_trans)
(List.rev stmt_from_action)
else
- List.fold_left2
- (fun acc cond stmt_act ->
- if stmt_act = [] then acc
- else
- (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
- [mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt)]
- (List.rev exp_from_trans)
- (List.rev stmt_from_action)
+ let actions =
+ List.fold_left2
+ (fun acc cond stmt_act ->
+ if stmt_act = [] then acc
+ else
+ (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
+ []
+ (List.rev exp_from_trans)
+ (List.rev stmt_from_action)
+ in
+ mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
end else
if Aorai_option.Deterministic.get () then []
else [is_out_of_state_stmt state loc]
diff --git a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
index f4ec0edda45..be1dc66d50a 100644
--- a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
@@ -91,15 +91,15 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_counter ++;
- if (aorai_intermediate_state == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
else
if (aorai_intermediate_state_0 == 1)
if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
else aorai_intermediate_state_1_tmp = 0;
else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
index 5fc4bc1ae7b..a5cacc4f933 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
@@ -273,10 +273,6 @@ void f(void)
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
- if (aorai_intermediate_state_2 == 1)
- if (aorai_counter < 2) aorai_counter ++;
- if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
- if (aorai_intermediate_state == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1;
else
if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1;
@@ -285,6 +281,10 @@ void f(void)
if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
else aorai_intermediate_state_3_tmp = 0;
else aorai_intermediate_state_3_tmp = 0;
+ if (aorai_intermediate_state_2 == 1)
+ if (aorai_counter < 2) aorai_counter ++;
+ if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
+ if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
index d2de21821b3..ee365599dac 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
@@ -91,15 +91,15 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_counter ++;
- if (aorai_intermediate_state == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
else
if (aorai_intermediate_state_0 == 1)
if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
else aorai_intermediate_state_1_tmp = 0;
else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
index 7800d93810c..92104920d5c 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
@@ -2,5 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
- 1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
index 7c1aab1abe4..ab5514b69d2 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
@@ -2,5 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
- 1 ≡ aorai_intermediate_state_3 in automaton function g_pre_func
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
index 91bbf9123ac..64b2e8b3540 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
@@ -2,5 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
- 1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func
--
GitLab