Commit c191e621 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[aorai] forbid multiple assignement to the same variable in transitions

parent 029c9438
......@@ -26,9 +26,25 @@
open Cil_types
open Promelaast
let dkey = Aorai_option.register_category "check-metavar"
let dkey_metavar_init = Aorai_option.register_category "metavar-init"
module VarSet = Cil_datatype.Varinfo.Set
let pretty_set fmt set =
let l = VarSet.elements set in
Pretty_utils.pp_list ~sep:", " Cil_printer.pp_varinfo fmt l
let pretty_state fmt st =
Format.pp_print_string fmt st.Promelaast.name
let pretty_trans fmt tr =
Format.fprintf fmt "from %a to %a:@\n{ @[%a@] } %a"
pretty_state tr.start
pretty_state tr.stop
Promelaoutput.Typed.print_condition tr.cross
Promelaoutput.Typed.print_actionl tr.actions
module type InitAnalysisParam =
sig
......@@ -41,12 +57,9 @@ struct
type edge = Aorai_graph.E.t
type g = Aorai_graph.t
module Set = Cil_datatype.Varinfo.Set
type data = Bottom | InitializedSet of Set.t
let dkey = dkey_metavar_init
type data = Bottom | InitializedSet of VarSet.t
let top = InitializedSet Set.empty
let top = InitializedSet VarSet.empty
let init v =
if v.Promelaast.init = Bool3.True then top else Bottom
......@@ -56,49 +69,34 @@ struct
let equal d1 d2 =
match d1, d2 with
| Bottom, d | d, Bottom -> d = Bottom
| InitializedSet s1, InitializedSet s2 -> Set.equal s1 s2
| InitializedSet s1, InitializedSet s2 -> VarSet.equal s1 s2
let join d1 d2 =
match d1, d2 with
| Bottom, d | d, Bottom -> d
| InitializedSet s1, InitializedSet s2 ->
InitializedSet (Set.inter s1 s2)
let pretty_state fmt st =
Format.pp_print_string fmt st.Promelaast.name
let pretty_trans fmt tr =
Promelaoutput.Typed.print_condition fmt tr.cross;
if tr.actions <> [] then
Format.fprintf fmt "{@[%a@]}" Promelaoutput.Typed.print_actionl tr.actions
let pretty_set fmt set =
let l = Set.elements set in
Pretty_utils.pp_list ~sep:", " Cil_printer.pp_varinfo fmt l
InitializedSet (VarSet.inter s1 s2)
let _pretty_data fmt = function
| Bottom -> Format.printf "Bottom"
| InitializedSet set -> pretty_set fmt set
let check (src,tr,dst) used initialized =
let diff = Set.diff used initialized in
if not (Set.is_empty diff) then
let check tr used initialized =
let diff = VarSet.diff used initialized in
if not (VarSet.is_empty diff) then
Aorai_option.abort
"The metavariables %a may not be initialized before the transition \
from %a to %a:@\n%a"
"The metavariables %a may not be initialized before the transition %a"
pretty_set diff
pretty_state src
pretty_state dst
pretty_trans tr
let term_mvars t =
let result = ref Set.empty in
let result = ref VarSet.empty in
let v = object
inherit Visitor.frama_c_inplace
method!vlogic_var_use lv =
match lv.lv_origin with
| Some vi when Env.is_metavariable vi ->
result := Set.add vi !result;
result := VarSet.add vi !result;
Cil.SkipChildren
| _ -> Cil.SkipChildren
end in
......@@ -106,27 +104,27 @@ struct
!result
let rec cond_mvars = function
| TAnd (c1,c2) | TOr (c1,c2) -> Set.union (cond_mvars c1) (cond_mvars c2)
| TAnd (c1,c2) | TOr (c1,c2) -> VarSet.union (cond_mvars c1) (cond_mvars c2)
| TNot (c) -> cond_mvars c
| TRel (_,t1,t2) -> Set.union (term_mvars t1) (term_mvars t2)
| TCall _ | TReturn _ | TTrue | TFalse -> Set.empty
| TRel (_,t1,t2) -> VarSet.union (term_mvars t1) (term_mvars t2)
| TCall _ | TReturn _ | TTrue | TFalse -> VarSet.empty
let analyze ((src,tr,dst) as edge) = function
let analyze (_,tr,_) = function
| Bottom -> Bottom
| InitializedSet initialized ->
(* Check that the condition uses only initialized variables *)
check edge (cond_mvars tr.cross) (initialized);
check tr (cond_mvars tr.cross) (initialized);
(* Add initialized variables and check the right hand side *)
let add initialized = function
| Copy_value ((TVar({lv_origin = Some vi}),_),t) ->
check edge (term_mvars t) initialized;
Set.add vi initialized
check tr (term_mvars t) initialized;
VarSet.add vi initialized
| _ -> initialized
in
let initialized' = List.fold_left add initialized tr.actions in
Aorai_option.debug ~dkey "%a {%a} -> %a {%a}"
pretty_state src pretty_set initialized
pretty_state dst pretty_set initialized';
pretty_state tr.start pretty_set initialized
pretty_state tr.stop pretty_set initialized';
InitializedSet initialized'
end
......@@ -144,3 +142,20 @@ let checkInitialization auto =
let g = Aorai_graph.of_automaton auto in
let _result = Fixpoint.analyze A.init g in
()
let checkSingleAssignment auto =
let check_action tr assigned = function
| Copy_value ((TVar({lv_origin = Some vi}),_),_) ->
if VarSet.mem vi assigned then
Aorai_option.abort
"The metavariable %a may not be assigned several times during the \
transition %a"
Cil_printer.pp_varinfo vi
pretty_trans tr;
VarSet.add vi assigned
| _ -> assigned
in
let check_trans tr =
ignore (List.fold_left (check_action tr) VarSet.empty tr.actions)
in
List.iter check_trans auto.trans
......@@ -24,3 +24,5 @@
(**************************************************************************)
val checkInitialization : Promelaast.typed_automaton -> unit
val checkSingleAssignment : Promelaast.typed_automaton -> unit
......@@ -1561,7 +1561,8 @@ let setAutomata auto =
(* all transitions have a true parameterized guard, i.e. [[]] *)
cond_of_parametrizedTransitions :=
Array.make (getNumberOfTransitions ()) [[]] ;
Aorai_metavariables.checkInitialization auto
Aorai_metavariables.checkInitialization auto ;
Aorai_metavariables.checkSingleAssignment auto
let getState num =
List.find (fun st -> st.nums = num) (getAutomata ()).states
......
[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
(Call(h))
and
((aorai_x) > (0))
{ (Call(h)) and ((aorai_x) > (0)) }
[kernel] Plug-in aorai aborted: invalid user input.
[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
a = 0,
b = 1,
c = 2
};
enum aorai_ListOper {
op_main = 0
};
enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
/*@ check lemma c_deterministic_trans{L}: \true;
*/
/*@ check lemma b_deterministic_trans{L}: \true;
*/
/*@ check lemma a_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@ ghost int aorai_CurStates = a; */
/*@ ghost int aorai_x = 0; */
/*@ ghost int aorai_y = 0; */
/*@ ghost
/@ requires aorai_CurStates ≡ a;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
behavior buch_state_b_in_0:
assumes aorai_CurStates ≡ a;
ensures aorai_CurStates ≡ b;
ensures aorai_x ≡ \old(*x);
ensures aorai_y ≡ \old(*y);
behavior buch_state_b_out:
assumes aorai_CurStates ≢ a;
ensures aorai_CurStates ≢ b;
behavior buch_state_c_out:
ensures aorai_CurStates ≢ c;
behavior aorai_y_unchanged:
assumes aorai_CurStates ≢ a;
ensures aorai_y ≡ \old(aorai_y);
behavior aorai_x_unchanged:
assumes aorai_CurStates ≢ a;
ensures aorai_x ≡ \old(aorai_x);
@/
void main_pre_func(int *x, int *y)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) {
aorai_CurStates = b;
aorai_x = *x;
aorai_y = *y;
}
return;
}
*/
/*@ ghost
/@ requires aorai_CurStates ≡ b;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
behavior buch_state_c_in_0:
assumes aorai_CurStates ≡ b;
ensures aorai_CurStates ≡ c;
ensures aorai_x ≡ \old(aorai_y);
ensures aorai_y ≡ aorai_x;
behavior buch_state_c_out:
assumes aorai_CurStates ≢ b;
ensures aorai_CurStates ≢ c;
behavior aorai_y_unchanged_0:
assumes aorai_CurStates ≢ b;
ensures aorai_y ≡ \old(aorai_y);
behavior aorai_x_unchanged_0:
assumes aorai_CurStates ≢ b;
ensures aorai_x ≡ \old(aorai_x);
@/
void main_post_func(void)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (1 == aorai_CurStates) {
aorai_CurStates = c;
aorai_x = aorai_y;
aorai_y = aorai_x;
}
return;
}
*/
/*@ requires aorai_CurStates ≡ a;
behavior Buchi_property_behavior:
ensures aorai_CurStates ≡ c;
ensures
\at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ c ⇒
aorai_y ≡ \at(*x,Pre) + 0;
ensures
\at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ c ⇒
aorai_x ≡ \at(*y,Pre) + 0;
*/
void main(int *x, int *y)
{
/*@ ghost main_pre_func(x,y); */
int t = *x;
*x = *y;
*y = t;
/*@ ghost main_post_func(); */
return;
}
[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariable aorai_x may not be assigned several times during the transition from a to b:
{ Call(main) } aorai_x <- x
aorai_x <- aorai_x + 1
[kernel] Plug-in aorai aborted: invalid user input.
[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
(Call(h))
and
((aorai_x) > (0))
{ (Call(h)) and ((aorai_x) > (0)) }
[kernel] Plug-in aorai aborted: invalid user input.
[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariable aorai_x may not be assigned several times during the transition from a to b:
{ Call(main) } aorai_x <- x
aorai_x <- aorai_x + 1
[kernel] Plug-in aorai aborted: invalid user input.
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(int *x, int *y)
{
int t = *x;
*x = *y;
*y = t;
}
%init: a;
%accept: c;
%deterministic;
$x : int;
$y : int;
a : { CALL(main) } $x := *x; $y := *y -> b;
b : { RETURN(main) } $x := $y; $y := $x -> c;
c : -> c;
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int main(int x)
{
return x;
}
%init: a;
%accept: c;
%deterministic;
$x : int;
a : { CALL(main) } $x := x; $x := $x + 1 -> b;
b : { RETURN(main) } -> c;
c : -> c;
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