From b26291885e4ffe24bfe49bc728f12cf5690373a0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Aug 2022 15:56:54 +0200
Subject: [PATCH] [aorai] fix handling of unlimited sequences
---
src/plugins/aorai/data_for_aorai.ml | 9 +-
.../tests/ya/oracle/seq_unlimited.res.oracle | 168 +++++++++++++++---
.../ya/oracle_prove/seq_unlimited.res.oracle | 5 -
3 files changed, 153 insertions(+), 29 deletions(-)
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 5fa579e6e7a..2615a5a92b6 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1177,11 +1177,14 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let trans = Path_analysis.get_transitions_of_state st auto in
if st.nums = inner_start.nums then begin
let loop_trans =
- if needs_counter then begin
+ if has_loop then begin
List.fold_left
(fun acc tr ->
- let init_action = Counter_init (make_counter tr.stop) in
- let init_actions = init_action :: tr.actions in
+ let init_actions =
+ if needs_counter then
+ Counter_init (make_counter tr.stop) :: tr.actions
+ else tr.actions
+ in
let init_trans =
new_trans st tr.stop tr.cross init_actions
in
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
index 0c4ab2b08ea..34b512d7005 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -1,17 +1,15 @@
[kernel] Parsing seq_unlimited.i (no preprocessing)
-[aorai] seq_unlimited.i:21: Warning:
- Call to find does not follow automaton's specification. This path is assumed to be dead
-[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] seq_unlimited.i:23: Warning:
- Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_seq_unlimited_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_intermediate_state = 0,
- aorai_reject = 1,
- b = 2,
- c = 3,
- fst = 4
+ aorai_intermediate_state_0 = 1,
+ aorai_intermediate_state_1 = 2,
+ aorai_reject = 3,
+ b = 4,
+ c = 5,
+ fst = 6,
+ ok = 7
};
enum aorai_ListOper {
op_find = 2,
@@ -22,6 +20,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
+/*@ check lemma ok_deterministic_trans{L}: \true;
+ */
/*@ check lemma fst_deterministic_trans{L}: \true;
*/
/*@ check lemma c_deterministic_trans{L}: \true;
@@ -34,6 +34,20 @@ enum aorai_OpStatusList {
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
+/*@
+check lemma aorai_intermediate_state_1_deterministic_trans{L}:
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated));
+ */
+/*@
+check lemma aorai_intermediate_state_0_deterministic_trans{L}:
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
+ \at(aorai_CurOperation,L) ≡ op_main ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated);
+ */
/*@ ghost int aorai_CurStates = fst; */
/*@ ghost
/@ requires aorai_CurStates ≡ b;
@@ -49,6 +63,12 @@ enum aorai_OpStatusList {
assumes aorai_CurStates ≢ b;
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -60,13 +80,16 @@ enum aorai_OpStatusList {
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
@/
void init_pre_func(int *a, int n)
{
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_init;
- if (2 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
+ if (4 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
else aorai_CurStates = aorai_reject;
return;
}
@@ -82,6 +105,12 @@ enum aorai_OpStatusList {
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -98,6 +127,9 @@ enum aorai_OpStatusList {
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
@/
void init_post_func(void)
{
@@ -124,10 +156,13 @@ void init(int *a, int n)
/*@ ghost aorai_Loop_Init_2 = 1; */
aorai_loop_2:
/*@ loop invariant Aorai: aorai_CurStates ≡ aorai_intermediate_state;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_0;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_1;
loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
loop invariant Aorai: aorai_CurStates ≢ b;
loop invariant Aorai: aorai_CurStates ≢ c;
loop invariant Aorai: aorai_CurStates ≢ fst;
+ loop invariant Aorai: aorai_CurStates ≢ ok;
*/
while (i < n) {
/*@ ghost aorai_Loop_Init_2 = 0; */
@@ -139,7 +174,9 @@ void init(int *a, int n)
}
/*@ ghost
- /@ requires \false;
+ /@ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≡ c;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_find;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
@@ -147,6 +184,21 @@ void init(int *a, int n)
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_in:
+ assumes
+ aorai_CurStates ≡ c ∨
+ aorai_CurStates ≡ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≡ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ assumes
+ aorai_CurStates ≢ c ∧
+ aorai_CurStates ≢ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -158,20 +210,26 @@ void init(int *a, int n)
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
@/
void find_pre_func(int *a, int n, int k)
{
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_find;
- aorai_CurStates = aorai_reject;
+ if (5 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_1;
+ else
+ if (1 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_1;
+ else aorai_CurStates = aorai_reject;
return;
}
*/
/*@ ghost
- /@ requires \false;
+ /@ requires aorai_CurStates ≡ aorai_intermediate_state_1;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_find;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
@@ -179,6 +237,17 @@ void init(int *a, int n)
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_in:
+ assumes aorai_CurStates ≡ aorai_intermediate_state_1;
+ ensures aorai_CurStates ≡ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ assumes aorai_CurStates ≢ aorai_intermediate_state_1;
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -190,19 +259,33 @@ void init(int *a, int n)
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
@/
void find_post_func(int res)
{
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_find;
- aorai_CurStates = aorai_reject;
+ if (2 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_0;
+ else aorai_CurStates = aorai_reject;
return;
}
*/
-/*@ requires \false; */
+/*@ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≡ c;
+ requires aorai_CurStates ≡ c ∨ aorai_CurStates ≢ c;
+ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior Buchi_property_behavior:
+ ensures aorai_CurStates ≡ aorai_intermediate_state_0;
+ */
int find(int *a, int n, int k)
{
int __retres;
@@ -213,10 +296,19 @@ int find(int *a, int n, int k)
/*@ ghost aorai_Loop_Init_12 = 1; */
aorai_loop_12:
/*@ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_0;
+ loop invariant Aorai: aorai_CurStates ≡ aorai_intermediate_state_1;
loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
loop invariant Aorai: aorai_CurStates ≢ b;
loop invariant Aorai: aorai_CurStates ≢ c;
loop invariant Aorai: aorai_CurStates ≢ fst;
+ loop invariant Aorai: aorai_CurStates ≢ ok;
+ loop invariant
+ Aorai:
+ aorai_Loop_Init_12 ≢ 0 ⇒
+ \at(aorai_CurStates ≢ aorai_intermediate_state_0,Pre) ∧
+ \at(aorai_CurStates ≢ c,Pre) ⇒
+ aorai_CurStates ≢ aorai_intermediate_state_1;
*/
while (i < n) {
/*@ ghost aorai_Loop_Init_12 = 0; */
@@ -235,7 +327,7 @@ int find(int *a, int n, int k)
}
/*@ ghost
- /@ requires \false;
+ /@ requires aorai_CurStates ≡ fst;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
@@ -243,10 +335,21 @@ int find(int *a, int n, int k)
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
+ behavior buch_state_b_in:
+ assumes aorai_CurStates ≡ fst;
+ ensures aorai_CurStates ≡ b;
+
behavior buch_state_b_out:
+ assumes aorai_CurStates ≢ fst;
ensures aorai_CurStates ≢ b;
behavior buch_state_c_out:
@@ -254,20 +357,24 @@ int find(int *a, int n, int k)
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
@/
void main_pre_func(void)
{
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates = aorai_reject;
+ if (6 == aorai_CurStates) aorai_CurStates = b;
+ else aorai_CurStates = aorai_reject;
return;
}
*/
/*@ ghost
- /@ requires \false;
+ /@ requires aorai_CurStates ≡ aorai_intermediate_state_0;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
@@ -275,6 +382,12 @@ int find(int *a, int n, int k)
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -286,22 +399,35 @@ int find(int *a, int n, int k)
behavior buch_state_fst_out:
ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_in:
+ assumes aorai_CurStates ≡ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≡ ok;
+
+ behavior buch_state_ok_out:
+ assumes aorai_CurStates ≢ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≢ ok;
@/
void main_post_func(int res)
{
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates = aorai_reject;
+ if (1 == aorai_CurStates) aorai_CurStates = ok;
+ else aorai_CurStates = aorai_reject;
return;
}
*/
-/*@ requires \false;
+/*@ requires aorai_CurStates ≡ fst;
behavior aorai_acceptance:
- ensures \false; */
+ ensures aorai_CurStates ≡ ok;
+
+ behavior Buchi_property_behavior:
+ ensures aorai_CurStates ≡ ok;
+ */
int main(void)
{
int __retres;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
index 719a33db757..3bd12d5c212 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
@@ -1,8 +1,3 @@
[kernel] Parsing seq_unlimited.i (no preprocessing)
-[aorai] seq_unlimited.i:21: Warning:
- Call to find does not follow automaton's specification. This path is assumed to be dead
-[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] seq_unlimited.i:23: Warning:
- Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_seq_unlimited_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
--
GitLab