From 8d592f4be1b73af61c43097db691c432d62fa91e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sun, 26 Dec 2021 19:12:06 +0100
Subject: [PATCH] [aorai] fix loop invariant generation
and remove some nearly duplicated code
---
src/plugins/aorai/aorai_visitors.ml | 18 ++----------------
.../aorai/tests/ya/oracle/bts1289.1.res.oracle | 3 +--
.../tests/ya/oracle/loop_bts1050.res.oracle | 4 +---
.../aorai/tests/ya/oracle/observed.res.oracle | 5 +++--
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 4 +---
5 files changed, 8 insertions(+), 26 deletions(-)
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index aadd8a359bd..08dff72aecd 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -560,21 +560,6 @@ class visit_adding_pre_post_from_buch treatloops =
predicate_to_invariant kf stmt pred
end
in
- let impossible_states_preds start possible_states my_state =
- let treat_one_start_state state start_state end_states acc =
- if not (Data_for_aorai.Aorai_state.Map.mem state end_states) then
- Logic_const.pimplies
- (Logic_const.pat(Aorai_utils.is_state_pred start_state, start),
- Aorai_utils.is_out_of_state_pred state)
- :: acc
- else acc
- in
- let treat_one_state state _ acc =
- Data_for_aorai.Aorai_state.Map.fold
- (treat_one_start_state state) my_state acc
- in
- Data_for_aorai.Aorai_state.Map.fold treat_one_state possible_states []
- in
let impossible_states_preds_inv start possible_states my_state =
let treat_one_start_state state start_state end_states acc =
if Data_for_aorai.Aorai_state.Map.mem state end_states then
@@ -1064,7 +1049,8 @@ class visit_adding_pre_post_from_buch treatloops =
condition_to_invariant kf possible_states new_loop;
let init_preds =
- impossible_states_preds Logic_const.pre_label possible_states init_state
+ impossible_states_preds_inv
+ Logic_const.pre_label possible_states init_state
in
let treat_init_pred pred =
let pred = mk_imply Rneq pred in
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index 835b432fec2..ad209874b35 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -325,8 +325,7 @@ void main(void)
loop invariant Aorai: 0 ≡ aorai_intermediate_state_0;
loop invariant Aorai: 0 ≡ init;
loop invariant Aorai: 1 ≡ S ∨ 1 ≡ T;
- loop invariant
- Aorai: aorai_Loop_Init_4 ≢ 0 ⇒ \at(1 ≡ init,Pre) ⇒ 0 ≡ T;
+ loop invariant Aorai: aorai_Loop_Init_4 ≢ 0 ⇒ 0 ≡ T;
loop assigns i, aorai_Loop_Init_4, aorai_CurOpStatus,
aorai_CurOperation, S, T, aorai_intermediate_state,
aorai_intermediate_state_0, init;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 87d2fbbdcfd..82b0886cf1f 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -610,9 +610,7 @@ int main(int c)
Aorai:
1 ≡ aorai_intermediate_state ∨ 1 ≡ aorai_intermediate_state_0;
loop invariant
- Aorai:
- aorai_Loop_Init_13 ≢ 0 ⇒
- \at(1 ≡ S0,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+ Aorai: aorai_Loop_Init_13 ≢ 0 ⇒ 0 ≡ aorai_intermediate_state_0;
loop invariant
Aorai: aorai_Loop_Init_13 ≡ 0 ⇒ 0 ≡ aorai_intermediate_state;
loop invariant
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index d02c3691359..ffb2b1dba40 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -200,11 +200,12 @@ void g(void)
loop invariant
Aorai:
aorai_Loop_Init_4 ≢ 0 ⇒
- \at(1 ≡ aorai_intermediate_state_0,Pre) ⇒ 0 ≡ first_step;
+ \at(0 ≡ first_step,Pre) ⇒ 0 ≡ first_step;
loop invariant
Aorai:
aorai_Loop_Init_4 ≢ 0 ⇒
- \at(1 ≡ first_step,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+ \at(0 ≡ aorai_intermediate_state_0,Pre) ⇒
+ 0 ≡ aorai_intermediate_state_0;
loop invariant
Aorai:
aorai_Loop_Init_4 ≡ 0 ⇒
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index fa3c9b2b57c..1a827b61513 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -615,9 +615,7 @@ int main(int c)
Aorai:
1 ≡ aorai_intermediate_state ∨ 1 ≡ aorai_intermediate_state_0;
loop invariant
- Aorai:
- aorai_Loop_Init_14 ≢ 0 ⇒
- \at(1 ≡ S0,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+ Aorai: aorai_Loop_Init_14 ≢ 0 ⇒ 0 ≡ aorai_intermediate_state_0;
loop invariant
Aorai: aorai_Loop_Init_14 ≡ 0 ⇒ 0 ≡ aorai_intermediate_state;
loop invariant
--
GitLab