lustrec / src / pathConditions.ml @ 3e1d20e0
History  View  Annotate  Download (10.2 KB)
1 
open LustreSpec 

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),[expr1;expr2]) 
82  
83 
(* Format.printf "%a@." Printers.pp_expr expr1; *) 
84 
(* print_path (fun fmt > Format.fprintf fmt "%a and (%a != %a)" *) 
85 
(* Printers.pp_expr vi_as_expr *) 
86 
(* Printers.pp_expr expr (\*v*\) *) 
87 
(* Printers.pp_expr expr_neg_vi); *) 
88 
(* Format.printf "%a@." Printers.pp_expr expr2; *) 
89 
(* print_path (fun fmt > Format.fprintf fmt "(not %a) and (%a != %a)" *) 
90 
(* Printers.pp_expr vi_as_expr *) 
91 
(* Printers.pp_expr expr (\*v*\) *) 
92 
(* Printers.pp_expr expr_neg_vi) *) 
93 

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

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

172  
173 
let rec mcdc_expr cpt_pre expr = 
174 
match expr.expr_desc with 
175 
 Expr_tuple l > 
176 
let vl = 
177 
List.fold_right (fun e accu_v > 
178 
let vl = mcdc_expr cpt_pre e in 
179 
(vl@accu_v)) 
180 
l 
181 
[] 
182 
in 
183 
vl 
184 
 Expr_ite (i,t,e) > 
185 
let vl_i = gen_mcdc_cond_guard i in 
186 
let vl_t = mcdc_expr cpt_pre t in 
187 
let vl_e = mcdc_expr cpt_pre e in 
188 
vl_i@vl_t@vl_e 
189 
 Expr_arrow (e1, e2) > 
190 
let vl1 = mcdc_expr cpt_pre e1 in 
191 
let vl2 = mcdc_expr cpt_pre e2 in 
192 
vl1@vl2 
193 
 Expr_pre e > 
194 
let vl = mcdc_expr (cpt_pre+1) e in 
195 
vl 
196 
 Expr_appl (f, args, r) > 
197 
let vl = mcdc_expr cpt_pre args in 
198 
vl 
199 
 _ > [] 
200  
201 
let mcdc_var_def v expr = 
202 
match (Types.repr expr.expr_type).Types.tdesc with 
203 
 Types.Tbool > 
204 
let vl = gen_mcdc_cond_var v expr in 
205 
vl 
206 
 _ > let vl = mcdc_expr 0 expr in 
207 
vl 
208  
209 
let mcdc_node_eq eq = 
210 
let vl = 
211 
match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with 
212 
 [lhs], Types.Tbool, _ > gen_mcdc_cond_var lhs eq.eq_rhs 
213 
 _::_, Types.Ttuple tl, Expr_tuple rhs > 
214 
(* We iterate trough pairs, but accumulate variables aside. The resulting 
215 
expression shall remain a tuple defintion *) 
216 
let vl = List.fold_right2 (fun lhs rhs accu > 
217 
let v = mcdc_var_def lhs rhs in 
218 
(* we don't care about the expression it. We focus on the coverage 
219 
expressions in v *) 
220 
v@accu 
221 
) eq.eq_lhs rhs [] 
222 
in 
223 
vl 
224 
 _ > mcdc_expr 0 eq.eq_rhs 
225 
in 
226 
vl 
227  
228 
let mcdc_node_stmt stmt = 
229 
match stmt with 
230 
 Eq eq > let vl = mcdc_node_eq eq in vl 
231 
 Aut aut > assert false 
232  
233 
let mcdc_top_decl td = 
234 
match td.top_decl_desc with 
235 
 Node nd > 
236 
let new_coverage_exprs = 
237 
List.fold_right ( 
238 
fun s accu_v > 
239 
let vl' = mcdc_node_stmt s in 
240 
vl'@accu_v 
241 
) nd.node_stmts [] 
242 
in 
243 
(* We add coverage vars as boolean internal flows. TODO *) 
244 
let fresh_cov_defs = List.flatten (List.map snd new_coverage_exprs) in 
245 
let nb_total = List.length fresh_cov_defs in 
246 
let fresh_cov_vars = List.mapi (fun i cov_expr > 
247 
let loc = cov_expr.expr_loc in 
248 
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total; 
249 
let cov_id = Format.flush_str_formatter () in 
250 
let cov_var = mkvar_decl loc 
251 
(cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None) in 
252 
let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in 
253 
cov_var, cov_def 
254 
) fresh_cov_defs 
255 
in 
256 
let fresh_vars, fresh_eqs = List.split fresh_cov_vars in 
257 
let fresh_annots = 
258 
List.map 
259 
(fun v > {annots = [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc}) 
260 
fresh_vars in 
261 
Format.printf "We have %i coverage criteria for node %s@." nb_total nd.node_id; 
262 
(* And add them as annotations %PROPERTY: var TODO *) 
263 
{td with top_decl_desc = Node {nd with 
264 
node_locals = nd.node_locals@fresh_vars; 
265 
node_stmts = nd.node_stmts@fresh_eqs; 
266 
node_annot = nd.node_annot@fresh_annots 
267 
}} 
268 
 _ > td 
269  
270  
271 
let mcdc prog = 
272 
(* If main node is provided add silly constraints to show in/out variables in the path condition *) 
273 
if !Options.main_node <> "" then ( 
274 
inout_vars := 
275 
let top = List.find 
276 
(fun td > 
277 
match td.top_decl_desc with 
278 
 Node nd when nd.node_id = !Options.main_node > true 
279 
 _ > false) 
280 
prog 
281 
in 
282 
match top.top_decl_desc with 
283 
 Node nd > nd.node_inputs @ nd.node_outputs 
284 
 _ > assert false); 
285 
List.map mcdc_top_decl prog 
286  
287 
(* Local Variables: *) 
288 
(* compilecommand:"make C .." *) 
289 
(* End: *) 
290  
291 
