lustrec / src / pathConditions.ml @ 8cacf677
History  View  Annotate  Download (11.4 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 vl 
162  
163 
and gen_mcdc_cond_guard expr = 
164 
report ~level:1 (fun fmt > 
165 
Format.fprintf fmt".. Generating MC/DC cond for guard %a@." 
166 
Printers.pp_expr expr); 
167 
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in 
168 
if List.length leafs_n_neg_expr > 1 then ( 
169 
List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) > 
170 
(mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu 
171 
) vl leafs_n_neg_expr) 
172 
else 
173 
vl 
174 

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

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

312 
(* Local Variables: *) 
313 
(* compilecommand:"make C .." *) 
314 
(* End: *) 
315  
316 
