From 2c6bff5639a45f8f7ceca060ffcbfe4f68ae8092 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 8 Oct 2020 12:33:14 +0200
Subject: [PATCH] [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.
---
src/plugins/aorai/aorai_utils.ml | 63 ++++++++++++++-----
.../aorai/tests/ya/oracle/formals.res.oracle | 15 ++++-
.../tests/ya/oracle/loop_bts1050.res.oracle | 6 +-
.../ya/oracle/metavariables-right.res.oracle | 20 ++++--
.../aorai/tests/ya/oracle/seq.res.oracle | 5 ++
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 6 +-
.../aorai/tests/ya/oracle/stack.res.oracle | 18 ++++--
.../tests/ya/oracle_prove/stack.res.oracle | 4 ++
8 files changed, 110 insertions(+), 27 deletions(-)
create mode 100644 src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index b037dc7dfba..5d475c6435c 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 4e41dd7f696..0b99905eb22 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 04b434bbf6d..8057befb9f5 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 2f740e907d6..543ee451c49 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 ef2675cd7f0..b8816b350cc 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 3e600a02555..51f26c9c67f 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 d036e4e4493..348940aafcf 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 00000000000..ad8ddcef2ca
--- /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
--
GitLab