Merge branch 'fix/virgile/aorai-project-crash' into 'master'

[aorai] avoid removing initial state of automaton (fixes #586)

Closes #586

See merge request frama-c/frama-c!2102

src/plugins/aorai/data_for_aorai.ml

@@ -2018,7 +2018,8 @@ let removeUnusedTransitionsAndStates () =
       (Aorai_state.Set.add state set)
   in
   let reached _ state set = Aorai_state.Map.fold treat_one_state state set in
-  let reached_states = Pre_state.fold reached Aorai_state.Set.empty in
+  let init = Path_analysis.get_init_states (getAutomata ()) in
+  let reached_states = Pre_state.fold reached (Aorai_state.Set.of_list init) in
   let reached_states = Post_state.fold reached reached_states in
   let reached_states = Loop_init_state.fold reached reached_states in
   let reached_states = Loop_invariant_state.fold reached reached_states in

src/plugins/aorai/tests/aorai/monostate.i

+/* 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 f(void) {}
+
+void main(void) {
+  while (1) f();
+}

src/plugins/aorai/tests/aorai/monostate.ya

+%init : Init;
+%deterministic;
+%accept: Init;
+
+Init  :
+  { main() } -> Init
+| other -> Init
+;

src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle

 [kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
 [aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] Warning: No state of the automaton is reachable. Program and specification are incompatible, instrumentation will not be generated.
 [kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
 /* Generated by Frama-C */
+enum aorai_ListOper {
+    op_a = 1,
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost int S = 0; */
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_a;
+    assigns aorai_CurOpStatus, aorai_CurOperation, S;
+    
+    behavior buch_state_S_out:
+      ensures 0 ≡ S;
+ */
+void a_pre_func(void)
+{
+  /*@ ghost int S_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_a;
+  S_tmp = S;
+  S_tmp = 0;
+  S = S_tmp;
+  return;
+}
+
+/*@ requires \false;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_a;
+    assigns aorai_CurOpStatus, aorai_CurOperation, S;
+    
+    behavior buch_state_S_out:
+      ensures 0 ≡ S;
+ */
+void a_post_func(void)
+{
+  /*@ ghost int S_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_a;
+  S_tmp = S;
+  S_tmp = 0;
+  S = S_tmp;
+  return;
+}
+
+/*@ requires \false;
+    
+    behavior Buchi_behavior_out_0:
+      ensures 0 ≡ S; */
 void a(void)
 {
+  a_pre_func();
+  a_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, S;
+    
+    behavior buch_state_S_out:
+      ensures 0 ≡ S;
+ */
+void main_pre_func(void)
+{
+  /*@ ghost int S_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_main;
+  S_tmp = S;
+  S_tmp = 0;
+  S = S_tmp;
+  return;
+}
+
+/*@ requires \false;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, S;
+    
+    behavior buch_state_S_out:
+      ensures 0 ≡ S;
+ */
+void main_post_func(void)
+{
+  /*@ ghost int S_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_main;
+  S_tmp = S;
+  S_tmp = 0;
+  S = S_tmp;
   return;
 }
 
+/*@ requires \false;
+    
+    behavior Buchi_behavior_out_0:
+      ensures 0 ≡ S; */
 void main(void)
 {
+  int aorai_Loop_Init_4;
+  main_pre_func();
   int i = 0;
-  /*@ loop assigns i; */
+  /*@ ghost aorai_Loop_Init_4 = 1; */
+  aorai_loop_4:
+  /*@ loop invariant Aorai: 0 ≡ S;
+      loop assigns i, aorai_Loop_Init_4, aorai_CurOpStatus,
+                   aorai_CurOperation, S;
+      loop assigns aorai_Loop_Init_4 \from \nothing;
+  */
   while (i < 10) {
+    /*@ ghost aorai_Loop_Init_4 = 0; */
     a();
     i ++;
   }
+  main_post_func();
   return;
 }
 

src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle

 [kernel] Parsing tests/aorai/incorrect.i (no preprocessing)
 [aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] Warning: No state of the automaton is reachable. Program and specification are incompatible, instrumentation will not be generated.
 [kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
 /* Generated by Frama-C */
+enum aorai_States {
+    aorai_reject_state = -2,
+    s0 = 0
+};
+enum aorai_ListOper {
+    op_f = 1,
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ lemma s0_deterministic_trans{L}: \true;
+ */
 int f(void);
 
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost int aorai_CurStates = s0; */
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_s0_out:
+      ensures aorai_CurStates ≢ s0;
+ */
+void main_pre_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_s0_out:
+      ensures aorai_CurStates ≢ s0;
+ */
+void main_post_func(int res)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false; */
 int main(void)
 {
   int tmp;
+  main_pre_func();
   tmp = f();
+  main_post_func(tmp);
   return tmp;
 }
 

src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle

+[kernel] Parsing tests/aorai/monostate.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
+[aorai] tests/aorai/monostate.i:8: Warning: 
+  Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
+[kernel] Parsing /tmp/aorai_monostate_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_States {
+    aorai_reject_state = -2,
+    Init = 0,
+    aorai_intermediate_state = 1,
+    aorai_reject = 2
+};
+enum aorai_ListOper {
+    op_f = 1,
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ lemma aorai_reject_deterministic_trans{L}: \true;
+ */
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@
+lemma aorai_intermediate_state_deterministic_trans{L}:
+  ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+     ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
+        \at(aorai_CurOpStatus,L) ≡ aorai_Terminated));
+ */
+/*@
+lemma Init_deterministic_trans{L}:
+  ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
+     ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
+        \at(aorai_CurOpStatus,L) ≡ aorai_Called));
+ */
+/*@ ghost int aorai_CurStates = Init; */
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_f;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_Init_out:
+      ensures aorai_CurStates ≢ Init;
+    
+    behavior buch_state_aorai_intermediate_state_out:
+      ensures aorai_CurStates ≢ aorai_intermediate_state;
+    
+    behavior buch_state_aorai_reject_in:
+      assumes
+        aorai_CurStates ≡ aorai_reject ∨
+        aorai_CurStates ≡ aorai_intermediate_state;
+      ensures aorai_CurStates ≡ aorai_reject;
+    
+    behavior buch_state_aorai_reject_out:
+      assumes
+        aorai_CurStates ≢ aorai_reject ∧
+        aorai_CurStates ≢ aorai_intermediate_state;
+      ensures aorai_CurStates ≢ aorai_reject;
+ */
+void f_pre_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_f;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
+  else 
+    if (1 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_f;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_Init_out:
+      ensures aorai_CurStates ≢ Init;
+    
+    behavior buch_state_aorai_intermediate_state_out:
+      ensures aorai_CurStates ≢ aorai_intermediate_state;
+    
+    behavior buch_state_aorai_reject_in:
+      assumes aorai_CurStates ≡ aorai_reject;
+      ensures aorai_CurStates ≡ aorai_reject;
+    
+    behavior buch_state_aorai_reject_out:
+      assumes aorai_CurStates ≢ aorai_reject;
+      ensures aorai_CurStates ≢ aorai_reject;
+ */
+void f_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_f;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false;
+    requires
+      aorai_CurStates ≡ aorai_reject ∨ aorai_CurStates ≢ aorai_reject;
+    requires
+      aorai_CurStates ≡ aorai_intermediate_state ∨
+      aorai_CurStates ≢ aorai_intermediate_state;
+    ensures \false;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ aorai_reject;
+ */
+void f(void)
+{
+  f_pre_func();
+  f_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_Init_out:
+      ensures aorai_CurStates ≢ Init;
+    
+    behavior buch_state_aorai_intermediate_state_out:
+      ensures aorai_CurStates ≢ aorai_intermediate_state;
+    
+    behavior buch_state_aorai_reject_out:
+      ensures aorai_CurStates ≢ aorai_reject;
+ */
+void main_pre_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_Init_out:
+      ensures aorai_CurStates ≢ Init;
+    
+    behavior buch_state_aorai_intermediate_state_out:
+      ensures aorai_CurStates ≢ aorai_intermediate_state;
+    
+    behavior buch_state_aorai_reject_out:
+      ensures aorai_CurStates ≢ aorai_reject;
+ */
+void main_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires \false; */
+void main(void)
+{
+  int aorai_Loop_Init_3;
+  main_pre_func();
+  /*@ ghost aorai_Loop_Init_3 = 1; */
+  aorai_loop_3:
+  /*@ loop invariant Aorai: aorai_CurStates ≢ Init;
+      loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state;
+      loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
+  */
+  while (1) {
+    /*@ ghost aorai_Loop_Init_3 = 0; */
+    f();
+  }
+  main_post_func();
+  return;
+}
+
+