[aorai] add smoke tests asserting that there's always an active state

src/plugins/aorai/aorai_option.ml

@@ -150,6 +150,14 @@ module Deterministic=
       let default () = false
     end)
 
+module SmokeTests=
+  False
+    (struct
+      let option_name = "-aorai-smoke-tests"
+      let help = "Add assertion in the generated functions to ensure \
+                  that the automaton is always in at least one state"
+    end)
+
 module InstrumentationHistory =
   Int
     (struct

src/plugins/aorai/aorai_option.mli

@@ -39,6 +39,13 @@ module ConsiderAcceptance: Parameter_sig.Bool
 module AutomataSimplification: Parameter_sig.Bool
 module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
 
+(** if [true], adds assertion at the end of the generated function
+    to check that the automaton is not in the rejecting state (in
+    the deterministic case), or that at least one non-rejecting state
+    is active (in the non-deterministic state).
+*)
+module SmokeTests: Parameter_sig.Bool
+
 (** [true] if the user declares that its ya automaton is deterministic. *)
 module Deterministic: State_builder.Ref with type data = bool
 

src/plugins/aorai/aorai_utils.ml

@@ -874,6 +874,24 @@ let is_out_of_state_exp state loc =
       (Cil.evar (Data_for_aorai.get_state_var state))
       (mk_int_exp 0)
 
+let assert_alive_automaton kf stmt =
+  let pred =
+    if Aorai_option.Deterministic.get() then
+      let reject_state = Data_for_aorai.get_reject_state() in
+      is_out_of_state_pred reject_state
+    else begin
+      let valid_states =
+        List.filter
+          (fun x -> not (Data_for_aorai.is_reject_state x))
+          (fst (Data_for_aorai.getGraph ()))
+      in
+      let valid_preds = List.map is_state_pred valid_states in
+      Logic_const.pors valid_preds
+    end
+  in
+  let pred = { pred with pred_name = "aorai_smoke_test" :: pred.pred_name } in
+  Annotations.add_assert Aorai_option.emitter ~kf stmt pred
+
 (* Utilities for other globals *)
 
 let mk_global_comment txt = add_global (GText (txt))
@@ -2126,10 +2144,15 @@ let auto_func_block generated_kf loc f st status res =
     else
       mk_non_deterministic_body generated_kf loc f st status res
   in
-  let ret = [ Cil.mkStmt ~ghost:true (Cil_types.Return(None,loc)) ] in
+  let ret =
+    Cil.mkStmt ~ghost:true ~valid_sid:true (Cil_types.Return(None,loc))
+  in
+  if Aorai_option.SmokeTests.get () then begin
+    assert_alive_automaton generated_kf ret;
+  end;
   let res_block =
     (Cil.mkBlock
-       ( stmt_begin_list @ stmt_history_update @ main_stmt @ ret))
+       ( stmt_begin_list @ stmt_history_update @ main_stmt @ [ret]))
   in
   res_block.blocals <- local_var;
   Aorai_option.debug ~dkey "Generated body is:@\n%a"

src/plugins/aorai/tests/ya/oracle/serial.res.oracle

@@ -21,33 +21,20 @@
 [eva] tests/ya/serial.c:58: starting to merge loop iterations
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 100 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 300 states
-[aorai] tests/ya/serial.c:92: aorai_reject <- aorai_reject <- Complete
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:92: aorai_reject <- Error <- Complete
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
+[eva:alarm] tests/ya/serial.c:33: Warning: 
+  assertion 'Aorai,aorai_smoke_test' got status invalid (stopping propagation).
 [aorai] tests/ya/serial.c:92: Wait1 <- Wait1 <- Complete
 [aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:92: aorai_reject <- aorai_reject <- Complete
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
-[aorai] tests/ya/serial.c:92: aorai_reject <- Error <- Complete
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
 [aorai] tests/ya/serial.c:92: Wait1 <- Wait1 <- Complete
 [aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 500 states
-[eva:alarm] tests/ya/serial.c:65: Warning: 
-  accessing uninitialized left-value. assert \initialized(&status);
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 700 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 900 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1200 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1400 states
-[aorai] tests/ya/serial.c:92: aorai_reject <- aorai_reject <- aorai_reject
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:92: aorai_reject <- aorai_reject <- aorai_reject
-[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1500 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1600 states
 [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1700 states
-[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1800 states
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function input_data_post_func:
@@ -84,15 +71,15 @@
   aorai_y2 ∈ [0..2147483647]
   aorai_CurOperation ∈ {2}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 24}
-  aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13; 24}
+  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6}
+  aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13}
 [eva:final-states] Values at end of function input_data_pre_func:
   aorai_CurOperation ∈ {2}
   aorai_CurOpStatus ∈ {0}
-  aorai_CurStates ∈ {1; 2; 3; 4; 5; 6; 24}
-  aorai_StatesHistory_1 ∈ {8; 9; 10; 11; 12; 13; 24}
-  aorai_StatesHistory_2 ∈ {14; 15; 16; 17; 18; 24}
+  aorai_CurStates ∈ {1; 2; 3; 4; 5; 6}
+  aorai_StatesHistory_1 ∈ {8; 9; 10; 11; 12; 13}
+  aorai_StatesHistory_2 ∈ {14; 15; 16; 17; 18}
 [eva:final-states] Values at end of function input_data:
   Frama_C_entropy_source ∈ [--..--]
   aorai_x1 ∈
@@ -128,46 +115,46 @@
   aorai_y2 ∈ [0..2147483647]
   aorai_CurOperation ∈ {2}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 24}
-  aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13; 24}
+  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6}
+  aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13}
 [eva:final-states] Values at end of function input_status_post_func:
   aorai_CurOperation ∈ {1}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18; 24}
-  aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23; 24}
+  aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18}
+  aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23}
 [eva:final-states] Values at end of function input_status_pre_func:
   aorai_CurOperation ∈ {1}
   aorai_CurOpStatus ∈ {0}
-  aorai_CurStates ∈ {14; 15; 16; 17; 18; 24}
-  aorai_StatesHistory_1 ∈ {0; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_2 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19; 24}
+  aorai_CurStates ∈ {14; 15; 16; 17; 18}
+  aorai_StatesHistory_1 ∈ {0; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_2 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 19}
 [eva:final-states] Values at end of function input_status:
   Frama_C_entropy_source ∈ [--..--]
   aorai_CurOperation ∈ {1}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18; 24}
-  aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23; 24}
+  aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18}
+  aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23}
 [eva:final-states] Values at end of function output_post_func:
   aorai_CurOperation ∈ {0}
   aorai_CurOpStatus ∈ {1}
   aorai_CurStates ∈ {19; 24}
-  aorai_StatesHistory_1 ∈ {7; 19; 24}
-  aorai_StatesHistory_2 ∈ {0; 24}
+  aorai_StatesHistory_1 ∈ {7; 19}
+  aorai_StatesHistory_2 ∈ {0}
 [eva:final-states] Values at end of function output_pre_func:
   aorai_CurOperation ∈ {0}
   aorai_CurOpStatus ∈ {0}
   aorai_CurStates ∈ {7; 19; 24}
-  aorai_StatesHistory_1 ∈ {0; 24}
-  aorai_StatesHistory_2 ∈ {5; 24}
+  aorai_StatesHistory_1 ∈ {0}
+  aorai_StatesHistory_2 ∈ {5}
 [eva:final-states] Values at end of function output:
   aorai_CurOperation ∈ {0}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {19; 24}
-  aorai_StatesHistory_1 ∈ {7; 19; 24}
-  aorai_StatesHistory_2 ∈ {0; 24}
+  aorai_CurStates ∈ {19}
+  aorai_StatesHistory_1 ∈ {19}
+  aorai_StatesHistory_2 ∈ {0}
 [eva:final-states] Values at end of function read:
   Frama_C_entropy_source ∈ [--..--]
   s ∈
@@ -223,9 +210,9 @@
   aorai_y2 ∈ [0..2147483647]
   aorai_CurOperation ∈ {1; 2}
   aorai_CurOpStatus ∈ {1}
-  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 24}
-  aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
+  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18}
+  aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   buffer[0] ∈
@@ -283,25 +270,24 @@
   aorai_y2 ∈ [0..2147483647]
   aorai_CurOperation ∈ {0; 1; 2}
   aorai_CurOpStatus ∈ {0; 1}
-  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
-  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19; 24}
-  aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
+  aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
+  aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 19}
+  aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
   11 functions analyzed (out of 11): 100% coverage.
-  In these functions, 222 statements reached (out of 261): 85% coverage.
+  In these functions, 206 statements reached (out of 261): 78% coverage.
   ----------------------------------------------------------------------------
   Some errors and warnings have been raised during the analysis:
     by the Eva analyzer:      0 errors    0 warnings
     by the Frama-C kernel:    0 errors    1 warning
   ----------------------------------------------------------------------------
-  1 alarm generated by the analysis:
-       1 access to uninitialized left-values
+  0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis:
-    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Assertions        4 valid     2 unknown     0 invalid      6 total
     Preconditions     2 valid     0 unknown     0 invalid      2 total
-  100% of the logical properties reached have been proven.
+  75% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
 [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
 /* Generated by Frama-C */
@@ -575,6 +561,8 @@ int n = 0;
                         else 
                           if (13 == aorai_CurStates) aorai_CurStates = StatusReq5;
                           else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -628,6 +616,8 @@ int n = 0;
                                 if (18 == aorai_CurStates && (res & 1) == 0) 
                                   aorai_CurStates = Wait5;
                                 else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -677,6 +667,8 @@ int input_status(void)
                       else 
                         if (19 == aorai_CurStates) aorai_CurStates = Error;
                         else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -738,6 +730,8 @@ int input_status(void)
                                     aorai_y1 = res;
                                   }
                                   else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -799,6 +793,8 @@ int input_data(void)
                                                               128 * aorai_y2)) 
                               aorai_CurStates = Wait1;
                             else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -814,6 +810,8 @@ int input_data(void)
     aorai_StatesHistory_1 = aorai_CurStates;
     if (19 == aorai_CurStates) aorai_CurStates = Wait1;
     else aorai_CurStates = aorai_reject;
+    /@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
+    ;
     return;
   }
 
@@ -851,7 +849,6 @@ void main(void)
     int data = read(& status);
     if (data != -1) {
       int tmp_0;
-      /*@ assert Eva: initialization: \initialized(&status); */ ;
       if (status != 0) {
         n = 0;
         continue;

src/plugins/aorai/tests/ya/serial.c

 /* run.config
-  OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
+  OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
 */
 /* run.config_prove
-OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
+OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -load-module tests/Aorai_test.cmxs  -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
 */
 
 #include "__fc_builtin.h"