Commit 5b976de6 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] fix issue in translating actions into statement for deterministic case

Determistic C translation is now a series of `if ... else if ... else ...`
This avoids the need for auxiliary variables and inadvertently updating an
auxiliary variable that is used in a subsequent test.

Additionally, we have a marginally better ordering of tests wrt state numbering
parent 5d76b835
......@@ -835,12 +835,14 @@ let is_state_pred state =
(Req,one_term(),
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
let is_state_stmt (state,copy) loc =
if Aorai_option.Deterministic.get ()
then
mkStmtOneInstr
~ghost:true (Set (Cil.var copy, int2enumstate_exp loc state.nums, loc))
else mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc))
let is_state_non_det_stmt (_,copy) loc =
mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc))
let is_state_det_stmt state loc =
let var = Data_for_aorai.get_varinfo curState in
mkStmtOneInstr
~ghost:true (Set (Cil.var var, int2enumstate_exp loc state.nums, loc))
let is_state_exp state loc =
if Aorai_option.Deterministic.get ()
......@@ -1901,173 +1903,173 @@ let act_convert loc act res =
in
List.map treat_one_act act
let copy_stmt s =
let vis = new Visitor.frama_c_refresh (Project.current()) in
Visitor.visitFramacStmt vis s
let mk_transitions_stmt generated_kf loc f st res trans =
List.fold_right
(fun trans
(aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) ->
let (tr_stmts, tr_vars, tr_funcs, exp) =
crosscond_to_exp generated_kf f st loc trans.cross res
in
let cond = Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp in
(tr_stmts @ aux_stmts,
tr_vars @ aux_vars,
Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
Cil.mkBinOp loc LOr exp_from_trans cond,
(Cil.copy_exp cond, act_convert loc trans.actions res)
:: stmt_from_action))
trans
([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, [])
let mkIfStmt loc exp1 block1 block2 =
Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
let mk_deterministic_stmt
generated_kf loc auto f fst status ret state
(other_stmts, other_funcs, other_vars, trans_stmts as res) =
if is_reachable state status then begin
let trans = get_accessible_transitions auto state status in
let aux_stmts, aux_vars, aux_funcs, _, stmt_from_action =
mk_transitions_stmt generated_kf loc f fst ret trans
in
let stmts =
List.fold_left
(fun acc (cond, stmt_act) ->
[mkIfStmt loc cond
(mkBlock (is_state_det_stmt state loc :: stmt_act))
(mkBlock acc)])
trans_stmts
(List.rev stmt_from_action)
in
aux_stmts @ other_stmts,
Cil_datatype.Varinfo.Set.union aux_funcs other_funcs,
aux_vars @ other_vars,
stmts
end else res
(* mk_stmt loc (states, tr) f fst status state
(* mk_non_deterministic_stmt loc (states, tr) f fst status state
Generates the statement updating the variable representing
the state argument.
If state is reachable, generates a "If then else" statement, else it is
just an assignment.
Used in auto_func_block. *)
let mk_stmt generated_kf loc (states, tr) f fst status ((st,_) as state) res =
let mk_non_deterministic_stmt
generated_kf loc (states, tr) f fst status ((st,_) as state) res =
if is_reachable st status then begin
let useful_trans = get_accessible_transitions (states,tr) st status in
let aux_stmts, new_vars, new_funcs, exp_from_trans,stmt_from_action =
List.fold_right
(fun trans
(aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) ->
let (tr_stmts, tr_vars, tr_funcs, exp) =
crosscond_to_exp generated_kf f fst loc trans.cross res
in
(tr_stmts @ aux_stmts,
tr_vars @ aux_vars,
Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp
::exp_from_trans,
act_convert loc trans.actions res :: stmt_from_action))
useful_trans
([],[],Cil_datatype.Varinfo.Set.empty, [], [])
in
let mkIfStmt exp1 block1 block2 =
Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
in
let if_cond =
List.fold_left
(fun acc exp -> Cil.mkBinOp loc LOr exp acc)
(List.hd exp_from_trans)
(List.tl exp_from_trans)
in
let then_stmt = is_state_stmt state loc in
let else_stmt =
if Aorai_option.Deterministic.get () then []
else [is_out_of_state_stmt state loc]
let aux_stmts, new_vars, new_funcs, cond,stmt_from_action =
mk_transitions_stmt generated_kf loc f fst res useful_trans
in
let then_stmt = is_state_non_det_stmt state loc in
let else_stmt = [is_out_of_state_stmt state loc] in
let trans_stmts =
if Aorai_option.Deterministic.get () then
List.fold_left2
(fun acc cond stmt_act ->
[mkIfStmt cond
(mkBlock (copy_stmt then_stmt :: stmt_act)) (mkBlock acc)])
else_stmt
(List.rev exp_from_trans)
let actions =
List.fold_left
(fun acc (cond, stmt_act) ->
if stmt_act = [] then acc
else
(mkIfStmt loc cond (mkBlock stmt_act) (mkBlock []))::acc)
[]
(List.rev stmt_from_action)
else
let actions =
List.fold_left2
(fun acc cond stmt_act ->
if stmt_act = [] then acc
else
(mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
[]
(List.rev exp_from_trans)
(List.rev stmt_from_action)
in
mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
in
mkIfStmt loc cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
in
new_funcs, new_vars, aux_stmts @ trans_stmts
end else
if Aorai_option.Deterministic.get () then
Cil_datatype.Varinfo.Set.empty, [], []
else Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc]
Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc]
let auto_func_block generated_kf loc f st status res =
let dkey = func_body_dkey in
let call_or_ret =
match st with
| Promelaast.Call -> "call"
| Promelaast.Return -> "return"
let equalsStmt lval exp loc = (* assignment *)
Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc))
let mk_deterministic_body generated_kf loc f st status res =
let (states, _ as auto) = Data_for_aorai.getGraph() in
let aux_stmts, aux_funcs, aux_vars, trans_stmts =
List.fold_right
(mk_deterministic_stmt generated_kf loc auto f st status res)
states
([], Cil_datatype.Varinfo.Set.empty, [],[])
in
Aorai_option.debug
~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret;
let (states, _) as auto = Data_for_aorai.getGraph() in
aux_funcs, aux_vars, aux_stmts @ trans_stmts
let mk_non_deterministic_body generated_kf loc f st status res =
(* For the following tests, we need a copy of every state. *)
let (states, _) as auto = Data_for_aorai.getGraph() in
let copies, local_var =
if Aorai_option.Deterministic.get () then begin
let orig = Data_for_aorai.get_varinfo curState in
let copy = Cil.copyVarinfo orig (orig.vname ^ "_tmp") in
copy.vglob <- false;
List.map (fun st -> (st, copy)) states, [copy]
end else begin
let bindings =
List.map
(fun st ->
let state_var = Data_for_aorai.get_state_var st in
let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in
copy.vglob <- false;
(st,copy))
states
in bindings, snd (List.split bindings)
end
in
let equalsStmt lval exp = (* assignment *)
Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc))
in
let stmt_begin_list =
[
(* First statement : what is the current status : called or return ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus)) (* current status... *)
(Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))); (* ... equals to what it is *)
(* Second statement : what is the current operation, i.e. which function ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp)) (* current operation ... *)
(Cil.new_exp loc (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f)))) (* ...equals to what it is *)
]
let bindings =
List.map
(fun st ->
let state_var = Data_for_aorai.get_state_var st in
let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in
copy.vglob <- false;
(st,copy))
states
in bindings, snd (List.split bindings)
in
(* As we work on copies, they need to be set to their actual values *)
let copies_update =
if Aorai_option.Deterministic.get () then
let orig = Data_for_aorai.get_varinfo curState in
[ equalsStmt (Cil.var (List.hd local_var)) (Cil.evar ~loc orig) ]
else
List.map
(fun (st,copy) ->
equalsStmt (Cil.var copy)
(Cil.evar ~loc (Data_for_aorai.get_state_var st)))
copies
List.map
(fun (st,copy) ->
equalsStmt (Cil.var copy)
(Cil.evar ~loc (Data_for_aorai.get_state_var st)) loc)
copies
in
(* For each state, we have to generate the statement that will update its copy. *)
let new_funcs, local_var, main_stmt =
List.fold_left
(fun (new_funcs, aux_vars, stmts) state ->
let my_funcs, my_vars, my_stmts =
mk_stmt generated_kf loc auto f st status state res
mk_non_deterministic_stmt generated_kf loc auto f st status state res
in
Cil_datatype.Varinfo.Set.union my_funcs new_funcs,
my_vars @ aux_vars,
my_stmts@stmts )
(Cil_datatype.Varinfo.Set.empty, local_var, [])
copies
in
(* Finally, we replace the state var values by the ones computed in copies. *)
let stvar_update =
if Aorai_option.Deterministic.get () then
let orig = Data_for_aorai.get_varinfo curState in
[ equalsStmt (Cil.var orig) (Cil.evar (List.hd local_var))]
List.map
(fun (state,copy) ->
equalsStmt
(Cil.var (Data_for_aorai.get_state_var state))
(Cil.evar ~loc copy) loc)
copies
in
new_funcs, local_var, copies_update @ main_stmt @ stvar_update
let auto_func_block generated_kf loc f st status res =
let dkey = func_body_dkey in
let call_or_ret =
match st with
| Promelaast.Call -> "call"
| Promelaast.Return -> "return"
in
Aorai_option.debug
~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret;
let stmt_begin_list =
[
(* First statement : what is the current status : called or return ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus))
(Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))) loc;
(* Second statement : what is the current operation,
i.e. which function ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp))
(Cil.new_exp loc
(Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f))))
loc
]
in
let new_funcs, local_var, main_stmt =
if Aorai_option.Deterministic.get() then
mk_deterministic_body generated_kf loc f st status res
else
List.map
(fun (state,copy) ->
equalsStmt
(Cil.var (Data_for_aorai.get_state_var state))
(Cil.evar ~loc copy))
copies
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 res_block =
(Cil.mkBlock
( stmt_begin_list @ copies_update @ main_stmt @ stvar_update @ ret))
( stmt_begin_list @ main_stmt @ ret))
in
res_block.blocals <- local_var;
Aorai_option.debug ~dkey "Generated body is:@\n%a"
......
......@@ -71,9 +71,6 @@ val host_state_term: unit -> Cil_types.term_lval
corresponding state. *)
val is_state_pred: state -> predicate
(** Returns the statement saying the state is affected *)
val is_state_stmt: state * Cil_types.varinfo -> location -> Cil_types.stmt
(** Returns the boolean expression saying the state is affected *)
val is_state_exp: state -> location -> Cil_types.exp
......
......@@ -60,12 +60,9 @@ int X;
@/
void f_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates) aorai_CurStates_tmp = S_in_f;
aorai_CurStates = aorai_CurStates_tmp;
if (3 == aorai_CurStates) aorai_CurStates = S_in_f;
return;
}
......@@ -99,12 +96,9 @@ int X;
@/
void f_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (2 == aorai_CurStates) aorai_CurStates_tmp = in_main;
aorai_CurStates = aorai_CurStates_tmp;
if (2 == aorai_CurStates) aorai_CurStates = in_main;
return;
}
......@@ -151,12 +145,9 @@ void f(void)
@/
void main_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (0 == aorai_CurStates) aorai_CurStates_tmp = Sf;
aorai_CurStates = aorai_CurStates_tmp;
if (0 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
......@@ -190,12 +181,9 @@ void f(void)
@/
void main_post_func(int res)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) aorai_CurStates_tmp = S2;
aorai_CurStates = aorai_CurStates_tmp;
if (4 == aorai_CurStates) aorai_CurStates = S2;
return;
}
......
......@@ -61,12 +61,9 @@ check lemma I_deterministic_trans{L}:
@/
void main_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (0 == aorai_CurStates) aorai_CurStates_tmp = I;
aorai_CurStates = aorai_CurStates_tmp;
if (0 == aorai_CurStates) aorai_CurStates = I;
return;
}
......@@ -88,12 +85,9 @@ check lemma I_deterministic_trans{L}:
@/
void main_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (0 == aorai_CurStates) aorai_CurStates_tmp = I;
aorai_CurStates = aorai_CurStates_tmp;
if (0 == aorai_CurStates) aorai_CurStates = I;
return;
}
......
......@@ -105,15 +105,16 @@ check lemma S0_deterministic_trans{L}:
@/
void g_pre_func(int x)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates)
if (x == 5) aorai_CurStates_tmp = S5;
if (3 == aorai_CurStates)
if (x == 4) aorai_CurStates_tmp = S4;
aorai_CurStates = aorai_CurStates_tmp;
if (3 == aorai_CurStates) {
if (x == 4) aorai_CurStates = S4; else goto _LAND;
}
else {
_LAND: ;
if (3 == aorai_CurStates)
if (x == 5) aorai_CurStates = S5;
}
return;
}
......@@ -161,13 +162,11 @@ check lemma S0_deterministic_trans{L}:
@/
void g_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) aorai_CurStates_tmp = S3;
if (5 == aorai_CurStates) aorai_CurStates_tmp = S1;
aorai_CurStates = aorai_CurStates_tmp;
if (5 == aorai_CurStates) aorai_CurStates = S1;
else
if (4 == aorai_CurStates) aorai_CurStates = S3;
return;
}
......@@ -230,13 +229,10 @@ void g(int x)
@/
void f_pre_func(int x)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates)
if (x == 4) aorai_CurStates_tmp = S3;
aorai_CurStates = aorai_CurStates_tmp;
if (x == 4) aorai_CurStates = S3;
return;
}
......@@ -280,14 +276,11 @@ void g(int x)
@/
void f_post_func(int res)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates)
if (res == 0)
if (X == 5) aorai_CurStates_tmp = S2;
aorai_CurStates = aorai_CurStates_tmp;
if (X == 5) aorai_CurStates = S2;
return;
}
......@@ -356,15 +349,16 @@ int f(int x)
@/
void real_main_pre_func(int c)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
aorai_CurStates_tmp = aorai_CurStates;
if (0 == aorai_CurStates)
if (c == 0) aorai_CurStates_tmp = S2;
if (0 == aorai_CurStates)
if (c != 0) aorai_CurStates_tmp = S1;
aorai_CurStates = aorai_CurStates_tmp;
if (0 == aorai_CurStates) {
if (c != 0) aorai_CurStates = S1; else goto _LAND;
}
else {
_LAND: ;
if (0 == aorai_CurStates)
if (c == 0) aorai_CurStates = S2;
}
return;
}
......@@ -407,12 +401,9 @@ int f(int x)
@/
void real_main_post_func(int res)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_real_main;
aorai_CurStates_tmp = aorai_CurStates;
if (2 == aorai_CurStates) aorai_CurStates_tmp = Sf;
aorai_CurStates = aorai_CurStates_tmp;
if (2 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
......@@ -471,12 +462,9 @@ int real_main(int c)
@/
void main_pre_func(int c)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (7 == aorai_CurStates) aorai_CurStates_tmp = S0;
aorai_CurStates = aorai_CurStates_tmp;
if (7 == aorai_CurStates) aorai_CurStates = S0;
return;
}
......@@ -519,12 +507,9 @@ int real_main(int c)
@/
void main_post_func(int res)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (6 == aorai_CurStates) aorai_CurStates_tmp = Sf;
aorai_CurStates = aorai_CurStates_tmp;
if (6 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
......
......@@ -124,21 +124,23 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_pre_func(int x)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (7 == aorai_CurStates)
if (x == 3) {
aorai_CurStates_tmp = aorai_intermediate_state_2;
aorai_x_0 = x;
}
if (7 == aorai_CurStates)
if (7 == aorai_CurStates) {
if (x == 1) {
aorai_CurStates_tmp = aorai_intermediate_state;
aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
aorai_CurStates = aorai_CurStates_tmp;
else goto _LAND;
}
else {
_LAND: ;
if (7 == aorai_CurStates)
if (x == 3) {
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
}
}
return;
}
......@@ -209,24 +211,30 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_post_func(int res)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) {
if (aorai_x_0 != 3) aorai_CurStates_tmp = aorai_reject;
else goto _LAND;
if (aorai_x_0 == 3) aorai_CurStates = OK; else goto _LAND_1;
}
else {
_LAND: ;
if (1 == aorai_CurStates)
if (aorai_x != 1) aorai_CurStates_tmp = aorai_reject;
_LAND_1: ;
if (1 == aorai_CurStates) {
if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
else goto _LAND_0;
}
else {