From c20bbd8ff28c917a43ecfea2b4b8079270ab3677 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 22 Jan 2021 19:41:20 +0100
Subject: [PATCH] [aorai] add smoke tests asserting that there's always an
active state
---
src/plugins/aorai/aorai_option.ml | 8 ++
src/plugins/aorai/aorai_option.mli | 7 ++
src/plugins/aorai/aorai_utils.ml | 27 ++++-
.../aorai/tests/ya/oracle/serial.res.oracle | 101 +++++++++---------
src/plugins/aorai/tests/ya/serial.c | 4 +-
5 files changed, 91 insertions(+), 56 deletions(-)
diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 307652ff225..90946d86242 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/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
diff --git a/src/plugins/aorai/aorai_option.mli b/src/plugins/aorai/aorai_option.mli
index 633950adb90..b6b220f0fe3 100644
--- a/src/plugins/aorai/aorai_option.mli
+++ b/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
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index d2691257484..dd533767fdd 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/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"
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 2692e58379b..dbf366abac3 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/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;
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 98795b7b3d5..9efe13a270b 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -1,8 +1,8 @@
/* 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"
--
GitLab