diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index b037dc7dfbafd53ebc5792187a54f59a0007f232..5d475c6435cb059535e113a8995c2447ea1fcad7 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1629,27 +1629,59 @@ let get_accessible_transitions auto state status =
Data_for_aorai.Aorai_state.Set.fold
(fun s acc -> Path_analysis.get_edges s state auto @ acc) previous_set []
+let rec get_aux_var_bhv_name = function
+ | TVar v, _ ->
+ Data_for_aorai.get_fresh (v.lv_name ^ "_unchanged")
+ | lv ->
+ Aorai_option.fatal "unexpected lval for action variable: %a"
+ Printer.pp_term_lval lv
+
(* Assumes that we don't have a multi-state here.
pebbles are handled elsewhere
*)
-let mk_unchanged_aux_vars trans =
- let my_aux_vars = Cil_datatype.Term_lval.Set.empty in
- let add_one_action acc = function
- | Counter_init lv | Counter_incr lv | Copy_value (lv,_) ->
- Cil_datatype.Term_lval.Set.add lv acc
- | Pebble_init _ | Pebble_move _ -> acc
+let mk_unchanged_aux_vars_bhvs loc f st status =
+ let (states,_ as auto) = Data_for_aorai.getGraph() in
+ let add_state_trans acc state =
+ let trans = get_reachable_trans state st auto status in
+ List.rev_append trans acc
in
- let add_one_trans acc tr =
- List.fold_left add_one_action acc tr.actions
+ let crossable_trans =
+ List.fold_left add_state_trans [] states
in
- let my_aux_vars = List.fold_left add_one_trans my_aux_vars trans in
- let treat_lval lv acc =
+ let add_trans_aux_var trans map = function
+ | Counter_init lv | Counter_incr lv | Copy_value (lv,_) ->
+ let other_trans =
+ match Cil_datatype.Term_lval.Map.find_opt lv map with
+ | Some l -> l
+ | None -> []
+ in
+ Cil_datatype.Term_lval.Map.add lv (trans :: other_trans) map
+ | Pebble_init _ | Pebble_move _ -> map
+ in
+ let add_trans_aux_vars map trans =
+ List.fold_left (add_trans_aux_var trans) map trans.actions
+ in
+ let possible_actions =
+ List.fold_left add_trans_aux_vars
+ Cil_datatype.Term_lval.Map.empty
+ crossable_trans
+ in
+ let out_trans trans =
+ Logic_const.new_predicate
+ (Logic_const.por ~loc
+ (is_out_of_state_pred trans.start,
+ Logic_const.pnot (crosscond_to_pred trans.cross f st)))
+ in
+ let mk_behavior lv trans acc =
+ let name = get_aux_var_bhv_name lv in
+ let assumes = List.map out_trans trans in
let t = Data_for_aorai.tlval lv in
let ot = Logic_const.told t in
let p = Logic_const.prel (Req,t,ot) in
- (Normal, Logic_const.new_predicate p) :: acc
+ let post_cond = [Normal, Logic_const.new_predicate p] in
+ Cil.mk_behavior ~name ~assumes ~post_cond () :: acc
in
- Cil_datatype.Term_lval.Set.fold treat_lval my_aux_vars []
+ Cil_datatype.Term_lval.Map.fold mk_behavior possible_actions []
let mk_behavior ~loc auto kf e status state =
Aorai_option.debug "analysis of state %s (%d)"
@@ -1779,7 +1811,7 @@ let mk_behavior ~loc auto kf e status state =
else begin
let post_cond =
match state.multi_state with
- | None -> mk_unchanged_aux_vars my_trans
+ | None -> [] (* Done elsewhere *)
| Some (set,_) ->
let set =
Data_for_aorai.pebble_set_at set Logic_const.here_label
@@ -1874,8 +1906,11 @@ let auto_func_behaviors loc f st state =
let global_behavior =
Cil.mk_behavior ~requires ~post_cond ~assigns ()
in
+ let non_action_behaviors =
+ mk_unchanged_aux_vars_bhvs loc f st state
+ in
(* Keep behaviors ordered according to the states they describe *)
- global_behavior :: (List.rev behaviors)
+ global_behavior :: (List.rev_append behaviors non_action_behaviors)
let act_convert loc act res =
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 4e41dd7f696e65d3b5b363d4a952c1560a6d5b9f..0b99905eb22e9a6695591a121fd351424d8c7826 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -95,7 +95,6 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
behavior buch_state_aorai_intermediate_state_out:
assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 1);
ensures aorai_CurStates ≢ aorai_intermediate_state;
- ensures aorai_x ≡ \old(aorai_x);
behavior buch_state_aorai_intermediate_state_0_out:
ensures aorai_CurStates ≢ aorai_intermediate_state_0;
@@ -111,7 +110,6 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
behavior buch_state_aorai_intermediate_state_2_out:
assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 3);
ensures aorai_CurStates ≢ aorai_intermediate_state_2;
- ensures aorai_x_0 ≡ \old(aorai_x_0);
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -121,6 +119,14 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
behavior buch_state_main_0_out:
ensures aorai_CurStates ≢ main_0;
+
+ behavior aorai_x_0_unchanged:
+ assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 3);
+ ensures aorai_x_0 ≡ \old(aorai_x_0);
+
+ behavior aorai_x_unchanged:
+ assumes aorai_CurStates ≢ main_0 ∨ ¬(x ≡ 1);
+ ensures aorai_x ≡ \old(aorai_x);
@/
void f_pre_func(int x)
{
@@ -334,7 +340,6 @@ int f(int x)
behavior buch_state_aorai_intermediate_state_1_out:
assumes aorai_CurStates ≢ aorai_intermediate_state_0;
ensures aorai_CurStates ≢ aorai_intermediate_state_1;
- ensures aorai_y ≡ \old(aorai_y);
behavior buch_state_aorai_intermediate_state_2_out:
ensures aorai_CurStates ≢ aorai_intermediate_state_2;
@@ -352,6 +357,10 @@ int f(int x)
behavior buch_state_main_0_out:
ensures aorai_CurStates ≢ main_0;
+
+ behavior aorai_y_unchanged:
+ assumes aorai_CurStates ≢ aorai_intermediate_state_0;
+ ensures aorai_y ≡ \old(aorai_y);
@/
void g_pre_func(int y)
{
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 04b434bbf6da11f31a874aaceca1c219eb90348e..8057befb9f5e9705eece6bcb9985cbe67a5a3cd2 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -63,13 +63,17 @@ enum aorai_OpStatusList {
(0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5)) ∧
0 ≡ aorai_intermediate_state;
ensures 0 ≡ aorai_intermediate_state_1;
- ensures aorai_counter ≡ \old(aorai_counter);
behavior buch_state_aorai_intermediate_state_2_out:
ensures 0 ≡ aorai_intermediate_state_2;
behavior buch_state_aorai_intermediate_state_3_out:
ensures 0 ≡ aorai_intermediate_state_3;
+
+ behavior aorai_counter_unchanged:
+ assumes 0 ≡ aorai_intermediate_state;
+ assumes 0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5);
+ ensures aorai_counter ≡ \old(aorai_counter);
@/
void f_pre_func(void)
{
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index 2f740e907d67b768924e4ecbe361e49c581f4c00..543ee451c494793e3f05f1cb65edb164ebf9134b 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -80,8 +80,6 @@ check lemma e_deterministic_trans{L}:
behavior buch_state_c_out:
assumes aorai_CurStates ≢ b;
ensures aorai_CurStates ≢ c;
- ensures aorai_y ≡ \old(aorai_y);
- ensures aorai_x ≡ \old(aorai_x);
behavior buch_state_d_out:
ensures aorai_CurStates ≢ d;
@@ -100,6 +98,14 @@ check lemma e_deterministic_trans{L}:
behavior buch_state_i_0_out:
ensures aorai_CurStates ≢ i_0;
+
+ behavior aorai_y_unchanged:
+ assumes aorai_CurStates ≢ b;
+ ensures aorai_y ≡ \old(aorai_y);
+
+ behavior aorai_x_unchanged:
+ assumes aorai_CurStates ≢ b;
+ ensures aorai_x ≡ \old(aorai_x);
@/
void f_pre_func(int x)
{
@@ -476,8 +482,6 @@ void h(int x)
behavior buch_state_e_out:
assumes aorai_CurStates ≢ h_0;
ensures aorai_CurStates ≢ e;
- ensures aorai_y ≡ \old(aorai_y);
- ensures aorai_x ≡ \old(aorai_x);
behavior buch_state_f_0_out:
ensures aorai_CurStates ≢ f_0;
@@ -490,6 +494,14 @@ void h(int x)
behavior buch_state_i_0_out:
ensures aorai_CurStates ≢ i_0;
+
+ behavior aorai_y_unchanged_0:
+ assumes aorai_CurStates ≢ h_0;
+ ensures aorai_y ≡ \old(aorai_y);
+
+ behavior aorai_x_unchanged_0:
+ assumes aorai_CurStates ≢ h_0;
+ ensures aorai_x ≡ \old(aorai_x);
@/
void i_post_func(void)
{
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index ef2675cd7f075668a39ea9d309c2c53fe921c317..b8816b350cc8bac60112c601bb17d0db9ee1b4fe 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -253,6 +253,11 @@ void f(void)
(0 ≡ aorai_intermediate_state_2 ∨ ¬(aorai_counter < 2)) ∧
0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ aorai_intermediate_state;
ensures 0 ≡ aorai_intermediate_state_3;
+
+ behavior aorai_counter_unchanged:
+ assumes 0 ≡ aorai_intermediate_state;
+ assumes 0 ≡ aorai_intermediate_state_0;
+ assumes 0 ≡ aorai_intermediate_state_2 ∨ ¬(aorai_counter < 2);
ensures aorai_counter ≡ \old(aorai_counter);
@/
void g_pre_func(void)
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 3e600a02555ac40005422af1968c929809712c56..51f26c9c67fd769cf96b4a89a86f25d9f89cfaab 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -63,13 +63,17 @@ enum aorai_OpStatusList {
(0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5)) ∧
0 ≡ aorai_intermediate_state;
ensures 0 ≡ aorai_intermediate_state_1;
- ensures aorai_counter ≡ \old(aorai_counter);
behavior buch_state_aorai_intermediate_state_2_out:
ensures 0 ≡ aorai_intermediate_state_2;
behavior buch_state_aorai_intermediate_state_3_out:
ensures 0 ≡ aorai_intermediate_state_3;
+
+ behavior aorai_counter_unchanged:
+ assumes 0 ≡ aorai_intermediate_state;
+ assumes 0 ≡ aorai_intermediate_state_0 ∨ ¬(aorai_counter < 5);
+ ensures aorai_counter ≡ \old(aorai_counter);
@/
void f_pre_func(void)
{
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index d036e4e44939b3d91ffec9da6606f8670f5c7463..348940aafcf7f5754cd84c890a7c42c92b20aee0 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -119,13 +119,17 @@ check lemma emptying_stack_deterministic_trans{L}:
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ filling_stack;
ensures aorai_CurStates ≢ filled_stack;
- ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
+
+ behavior aorai_n_unchanged:
+ assumes aorai_CurStates ≢ filling_stack;
+ assumes aorai_CurStates ≢ filling_stack;
+ ensures aorai_n ≡ \old(aorai_n);
@/
void push_post_func(void)
{
@@ -226,7 +230,6 @@ void push(void)
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1);
ensures aorai_CurStates ≢ empty_stack;
- ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
@@ -239,13 +242,17 @@ void push(void)
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1);
ensures aorai_CurStates ≢ filled_stack;
- ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
+
+ behavior aorai_n_unchanged_0:
+ assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1);
+ assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1);
+ ensures aorai_n ≡ \old(aorai_n);
@/
void pop_post_func(void)
{
@@ -315,7 +322,6 @@ void pop(void)
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ init;
ensures aorai_CurStates ≢ empty_stack;
- ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
@@ -328,6 +334,10 @@ void pop(void)
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
+
+ behavior aorai_n_unchanged_1:
+ assumes aorai_CurStates ≢ init;
+ ensures aorai_n ≡ \old(aorai_n);
@/
void main_pre_func(void)
{
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ad8ddcef2ca5c41625a8a4dec207a6a71cdf6be6
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/ya/stack.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards