Commit 2c6bff56 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] fix behavior generation for absence of modification of action variables

it turns out that meta-variables can be modified through several transitions,
possibly with distinct end states. It is thus not possible to mention that
they are unchanged in behaviors that are grouped by the state at the end of
the call to the transition function.

This commit creates specific behaviors for indicating in which case an
auxiliary variable is unchanged.
parent 1cec870f
......@@ -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 =
......
......@@ -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)
{
......
......@@ -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)
{
......
......@@ -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)
{
......
......@@ -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)
......
......@@ -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)
{
......
......@@ -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)
{
......
[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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment