lustrec / src / pathConditions.ml @ 8f9ce6d4
History  View  Annotate  Download (11.5 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 description, ie 
68 
tautologies, over inout variables to make sure they were not suppresed by 
69 
some other algorithms *) 
70  
71 
(* Takes the variable on which these coverage criteria will apply, as well as 
72 
the expression and its negated version. Returns the expr and the variable 
73 
expression, as well as the two new boolean expressions descibing the two 
74 
associated modes. *) 
75 
let mcdc_var vi_as_expr expr expr_neg_vi = 
76 
let loc = expr.expr_loc in 
77 
let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in 
78 
let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in 
79 
let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in 
80 
let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in 
81 
((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom 
82 
true while expr2 
83 
corresponds to atom 
84 
false *) 
85  
86 
(* Format.printf "%a@." Printers.pp_expr expr1; *) 
87 
(* print_path (fun fmt > Format.fprintf fmt "%a and (%a != %a)" *) 
88 
(* Printers.pp_expr vi_as_expr *) 
89 
(* Printers.pp_expr expr (\*v*\) *) 
90 
(* Printers.pp_expr expr_neg_vi); *) 
91 
(* Format.printf "%a@." Printers.pp_expr expr2; *) 
92 
(* print_path (fun fmt > Format.fprintf fmt "(not %a) and (%a != %a)" *) 
93 
(* Printers.pp_expr vi_as_expr *) 
94 
(* Printers.pp_expr expr (\*v*\) *) 
95 
(* Printers.pp_expr expr_neg_vi) *) 
96 

97 
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) = 
98 
let neg_list l = 
99 
List.fold_right (fun e (vl,el) > let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], []) 
100 
in 
101 
match expr.expr_desc with 
102 
 Expr_tuple l > 
103 
let vl, neg = neg_list l in 
104 
vl, combine (fun l' > {expr with expr_desc = Expr_tuple l'}) neg l 
105 

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

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

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

315 
(* Local Variables: *) 
316 
(* compilecommand:"make C .." *) 
317 
(* End: *) 
318  
319 
