lustrec / src / pathConditions.ml @ e6b644f4
History  View  Annotate  Download (11.7 KB)
1 
open Lustre_types 

2 
open Corelang 
3 
open Log 
4 
open Format 
5  
6 
module IdSet = Set.Make (struct type t = expr * int let compare = compare end) 
7  
8 
let inout_vars = ref [] 
9  
10 
(* This was used to add inout variables in the final signature. May have to be 
11 
reactivated later *) 
12 

13 
(* let print_tautology_var fmt v = *) 
14 
(* match (Types.repr v.var_type).Types.tdesc with *) 
15 
(*  Types.Tbool > Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *) 
16 
(*  Types.Tint > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *) 
17 
(*  Types.Treal > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *) 
18 
(*  _ > Format.fprintf fmt "(true)" *) 
19  
20 
(* let print_path arg = match !inout_vars with *) 
21 
(*  [] > Format.printf "%t@." arg *) 
22 
(*  l > Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem > print_tautology_var fmt elem)) l *) 
23  
24 
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ] 
25  
26 
(* Used when we were printing the expression directly. Now we are constructing 
27 
them as regular expressions. 
28  
29 
let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf 
30 
fmt "pre "; print_pre fmt (nb_pre1) ) 
31 
*) 
32 

33 
let rec mk_pre n e = 
34 
if n <= 0 then 
35 
e 
36 
else 
37 
mkexpr e.expr_loc (Expr_pre e) 
38 

39 
(* 
40 
let combine2 f sub1 sub2 = 
41 
let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in 
42 
let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in 
43 
let common = IdSet.inter elem_e1 elem_e2 in 
44 
let sub1_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub1 in 
45 
let sub2_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub2 in 
46 
(List.map (fun (v, negv) > (v, f negv e2)) sub1_filtered) @ 
47 
(List.map (fun (v, negv) > (v, f e1 negv)) sub2_filtered) @ 
48 
(List.map (fun v > (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) ) 
49 
*) 
50  
51 
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) = 
52 
match active, modified, orig with 
53 
 true::active_tl, e::modified_tl, _::orig_tl > (List.assoc v e)::(select v active_tl modified_tl orig_tl) 
54 
 false::active_tl, _::modified_tl, e::orig_tl > e::(select v active_tl modified_tl orig_tl) 
55 
 [], [], [] > [] 
56 
 _ > assert false 
57 

58 
let combine (f: expr list > expr ) subs orig : ((expr * int) * expr) list = 
59 
let elems = List.map (fun sub_i > List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in 
60 
let all = List.fold_right IdSet.union elems IdSet.empty in 
61 
List.map (fun v > 
62 
let active_subs = List.map (IdSet.mem v) elems in 
63 
v, f (select v active_subs subs orig) 
64 
) (IdSet.elements all) 
65  
66  
67 
(* In a previous version, the printer was introducing fake 
68 
description, ie tautologies, over inout variables to make sure they 
69 
were not suppresed by some other algorithms *) 
70  
71 
(* Takes the variable on which these coverage criteria will apply, as 
72 
well as the expression and its negated version. Returns the expr 
73 
and the variable expression, as well as the two new boolean 
74 
expressions descibing the two associated modes. *) 
75 
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi = 
76 
let loc = expr.expr_loc in 
77 
let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in 
78 
let expr1, expr2 = 
79 
if nb_elems > 1 then 
80 
let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in 
81 
let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in 
82 
let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in 
83 
expr1, expr2 
84 
else 
85 
vi_as_expr, not_vi_as_expr 
86 
in 
87 
((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom 
88 
true while expr2 
89 
corresponds to atom 
90 
false *) 
91  
92 
(* Format.printf "%a@." Printers.pp_expr expr1; *) 
93 
(* print_path (fun fmt > Format.fprintf fmt "%a and (%a != %a)" *) 
94 
(* Printers.pp_expr vi_as_expr *) 
95 
(* Printers.pp_expr expr (\*v*\) *) 
96 
(* Printers.pp_expr expr_neg_vi); *) 
97 
(* Format.printf "%a@." Printers.pp_expr expr2; *) 
98 
(* print_path (fun fmt > Format.fprintf fmt "(not %a) and (%a != %a)" *) 
99 
(* Printers.pp_expr vi_as_expr *) 
100 
(* Printers.pp_expr expr (\*v*\) *) 
101 
(* Printers.pp_expr expr_neg_vi) *) 
102 

103 
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) = 
104 
let neg_list l = 
105 
List.fold_right (fun e (vl,el) > let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], []) 
106 
in 
107 
match expr.expr_desc with 
108 
 Expr_tuple l > 
109 
let vl, neg = neg_list l in 
110 
vl, combine (fun l' > {expr with expr_desc = Expr_tuple l'}) neg l 
111 

112 
 Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) > ( 
113 
let list = [i; t; e] in 
114 
let vl, neg = neg_list list in 
115 
vl, combine (fun l > 
116 
match l with 
117 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
118 
 _ > assert false 
119 
) neg list 
120 
) 
121 
 Expr_ite (i,t,e) > ( (* We return the guard as a new guard *) 
122 
let vl = gen_mcdc_cond_guard i in 
123 
let list = [i; t; e] in 
124 
let vl', neg = neg_list list in 
125 
vl@vl', combine (fun l > 
126 
match l with 
127 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
128 
 _ > assert false 
129 
) neg list 
130 
) 
131 
 Expr_arrow (e1, e2) > 
132 
let vl1, e1' = compute_neg_expr cpt_pre e1 in 
133 
let vl2, e2' = compute_neg_expr cpt_pre e2 in 
134 
vl1@vl2, combine (fun l > match l with 
135 
 [x;y] > { expr with expr_desc = Expr_arrow (x, y) } 
136 
 _ > assert false 
137 
) [e1'; e2'] [e1; e2] 
138  
139 
 Expr_pre e > 
140 
let vl, e' = compute_neg_expr (cpt_pre+1) e in 
141 
vl, List.map 
142 
(fun (v, negv) > (v, { expr with expr_desc = Expr_pre negv } )) e' 
143  
144 
 Expr_appl (op_name, args, r) when List.mem op_name rel_op > 
145 
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] 
146  
147 
 Expr_appl (op_name, args, r) > 
148 
let vl, args' = compute_neg_expr cpt_pre args in 
149 
vl, List.map 
150 
(fun (v, negv) > (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } )) 
151 
args' 
152  
153 
 Expr_ident _ when (Types.is_bool_type expr.expr_type) > 
154 
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] 
155 
 _ > [] (* empty vars *) , [] 
156 
and gen_mcdc_cond_var v expr = 
157 
report ~level:1 (fun fmt > 
158 
Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." 
159 
v 
160 
Printers.pp_expr expr); 
161 
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in 
162 
let len = List.length leafs_n_neg_expr in 
163 
if len >= 1 then ( 
164 
List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) > 
165 
(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu 
166 
) vl leafs_n_neg_expr 
167 
) 
168 
else 
169 
vl 
170  
171 
and gen_mcdc_cond_guard expr = 
172 
report ~level:1 (fun fmt > 
173 
Format.fprintf fmt".. Generating MC/DC cond for guard %a@." 
174 
Printers.pp_expr expr); 
175 
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in 
176 
let len = List.length leafs_n_neg_expr in 
177 
if len >= 1 then ( 
178 
List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) > 
179 
(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu 
180 
) vl leafs_n_neg_expr) 
181 
else 
182 
vl 
183 

184  
185 
let rec mcdc_expr cpt_pre expr = 
186 
match expr.expr_desc with 
187 
 Expr_tuple l > 
188 
let vl = 
189 
List.fold_right (fun e accu_v > 
190 
let vl = mcdc_expr cpt_pre e in 
191 
(vl@accu_v)) 
192 
l 
193 
[] 
194 
in 
195 
vl 
196 
 Expr_ite (i,t,e) > 
197 
let vl_i = gen_mcdc_cond_guard i in 
198 
let vl_t = mcdc_expr cpt_pre t in 
199 
let vl_e = mcdc_expr cpt_pre e in 
200 
vl_i@vl_t@vl_e 
201 
 Expr_arrow (e1, e2) > 
202 
let vl1 = mcdc_expr cpt_pre e1 in 
203 
let vl2 = mcdc_expr cpt_pre e2 in 
204 
vl1@vl2 
205 
 Expr_pre e > 
206 
let vl = mcdc_expr (cpt_pre+1) e in 
207 
vl 
208 
 Expr_appl (f, args, r) > 
209 
let vl = mcdc_expr cpt_pre args in 
210 
vl 
211 
 _ > [] 
212  
213 
let mcdc_var_def v expr = 
214 
if Types.is_bool_type expr.expr_type then 
215 
let vl = gen_mcdc_cond_var v expr in 
216 
vl 
217 
else 
218 
let vl = mcdc_expr 0 expr in 
219 
vl 
220 

221 
let mcdc_node_eq eq = 
222 
let vl = 
223 
match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with 
224 
 [lhs], true, _, _ > gen_mcdc_cond_var lhs eq.eq_rhs 
225 
 _::_, false, Types.Ttuple tl, Expr_tuple rhs > 
226 
(* We iterate trough pairs, but accumulate variables aside. The resulting 
227 
expression shall remain a tuple defintion *) 
228 
let vl = List.fold_right2 (fun lhs rhs accu > 
229 
let v = mcdc_var_def lhs rhs in 
230 
(* we don't care about the expression it. We focus on the coverage 
231 
expressions in v *) 
232 
v@accu 
233 
) eq.eq_lhs rhs [] 
234 
in 
235 
vl 
236 
 _ > mcdc_expr 0 eq.eq_rhs 
237 
in 
238 
vl 
239  
240 
let mcdc_node_stmt stmt = 
241 
match stmt with 
242 
 Eq eq > let vl = mcdc_node_eq eq in vl 
243 
 Aut aut > assert false 
244  
245 
let mcdc_top_decl td = 
246 
match td.top_decl_desc with 
247 
 Node nd > 
248 
let new_coverage_exprs = 
249 
List.fold_right ( 
250 
fun s accu_v > 
251 
let vl' = mcdc_node_stmt s in 
252 
vl'@accu_v 
253 
) nd.node_stmts [] 
254 
in 
255 
(* We add coverage vars as boolean internal flows. *) 
256 
let fresh_cov_defs = List.flatten (List.map (fun ((_, atom), expr_l) > List.map (fun (atom_valid, case) > atom, atom_valid, case) expr_l) new_coverage_exprs) in 
257 
let nb_total = List.length fresh_cov_defs in 
258 
let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) > 
259 
let loc = cov_expr.expr_loc in 
260 
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total; 
261 
let cov_id = Format.flush_str_formatter () in 
262 
let cov_var = mkvar_decl loc 
263 
(cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in 
264 
let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in 
265 
cov_var, cov_def, atom, atom_valid 
266 
) fresh_cov_defs 
267 
in 
268 
let fresh_vars, fresh_eqs = 
269 
List.fold_right 
270 
(fun (v,eq,_,_) (accuv, accueq)> v::accuv, eq::accueq ) 
271 
fresh_cov_vars 
272 
([], []) 
273 
in 
274 
let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for 
275 
kind2, and regular ones to keep track of the nature 
276 
of the annotations. *) 
277 
List.map 
278 
(fun (v, _, atom, atom_valid) > 
279 
let e = expr_of_vdecl v in 
280 
let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in 
281 
{annots = [["PROPERTY"], neg_ee; (* Using negated property to force 
282 
modelchecker to produce a 
283 
suitable covering trace *) 
284 
let loc = Location.dummy_loc in 
285 
let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in 
286 
["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e]) 
287 
]; 
288 
annot_loc = v.var_loc}) 
289 
fresh_cov_vars 
290 
in 
291 
Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id; 
292 
(* And add them as annotations %PROPERTY: var TODO *) 
293 
{td with top_decl_desc = Node {nd with 
294 
node_locals = nd.node_locals@fresh_vars; 
295 
node_stmts = nd.node_stmts@fresh_eqs; 
296 
node_annot = nd.node_annot@fresh_annots 
297 
}} 
298 
 _ > td 
299  
300  
301 
let mcdc prog = 
302 
(* If main node is provided add silly constraints to show in/out variables in the path condition *) 
303 
if !Options.main_node <> "" then ( 
304 
inout_vars := 
305 
let top = List.find 
306 
(fun td > 
307 
match td.top_decl_desc with 
308 
 Node nd when nd.node_id = !Options.main_node > true 
309 
 _ > false) 
310 
prog 
311 
in 
312 
match top.top_decl_desc with 
313 
 Node nd > nd.node_inputs @ nd.node_outputs 
314 
 _ > assert false); 
315 
List.map mcdc_top_decl prog 
316  
317  
318 

319 
(* Local Variables: *) 
320 
(* compilecommand:"make C .." *) 
321 
(* End: *) 
322  
323 
