1
|
open Lustre_types
|
2
|
open Corelang
|
3
|
open Log
|
4
|
|
5
|
module IdSet = Set.Make (struct
|
6
|
type t = expr * int
|
7
|
|
8
|
let compare = compare
|
9
|
end)
|
10
|
|
11
|
let inout_vars = ref []
|
12
|
|
13
|
(* This was used to add inout variables in the final signature. May have to be
|
14
|
reactivated later *)
|
15
|
|
16
|
(* let print_tautology_var fmt v = *)
|
17
|
(* match (Types.repr v.var_type).Types.tdesc with *)
|
18
|
(* | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
|
19
|
(* | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
|
20
|
(* | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
|
21
|
(* | _ -> Format.fprintf fmt "(true)" *)
|
22
|
|
23
|
(* let print_path arg = match !inout_vars with *)
|
24
|
(* | [] -> Format.printf "%t@." arg *)
|
25
|
(* | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun
|
26
|
fmt elem -> print_tautology_var fmt elem)) l *)
|
27
|
|
28
|
let rel_op = [ "="; "!="; "<"; "<="; ">"; ">=" ]
|
29
|
|
30
|
(* Used when we were printing the expression directly. Now we are constructing
|
31
|
them as regular expressions.
|
32
|
|
33
|
let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf
|
34
|
fmt "pre "; print_pre fmt (nb_pre-1) ) *)
|
35
|
|
36
|
let mk_pre n e = if n <= 0 then e else mkexpr e.expr_loc (Expr_pre e)
|
37
|
|
38
|
(* let combine2 f sub1 sub2 = let elem_e1 = List.fold_right IdSet.add (List.map
|
39
|
fst sub1) IdSet.empty in let elem_e2 = List.fold_right IdSet.add (List.map
|
40
|
fst sub2) IdSet.empty in let common = IdSet.inter elem_e1 elem_e2 in let
|
41
|
sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
|
42
|
let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2
|
43
|
in (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @ (List.map
|
44
|
(fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @ (List.map (fun v -> (v,
|
45
|
{expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)})
|
46
|
(IdSet.elements common)) ) *)
|
47
|
|
48
|
let rec select (v : expr * int) (active : bool list)
|
49
|
(modified : ((expr * int) * expr) list list) (orig : expr list) =
|
50
|
match active, modified, orig with
|
51
|
| true :: active_tl, e :: modified_tl, _ :: orig_tl ->
|
52
|
List.assoc v e :: select v active_tl modified_tl orig_tl
|
53
|
| false :: active_tl, _ :: modified_tl, e :: orig_tl ->
|
54
|
e :: select v active_tl modified_tl orig_tl
|
55
|
| [], [], [] ->
|
56
|
[]
|
57
|
| _ ->
|
58
|
assert false
|
59
|
|
60
|
let combine (f : expr list -> expr) subs orig : ((expr * int) * expr) list =
|
61
|
let elems =
|
62
|
List.map
|
63
|
(fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty)
|
64
|
subs
|
65
|
in
|
66
|
let all = List.fold_right IdSet.union elems IdSet.empty in
|
67
|
List.map
|
68
|
(fun v ->
|
69
|
let active_subs = List.map (IdSet.mem v) elems in
|
70
|
v, f (select v active_subs subs orig))
|
71
|
(IdSet.elements all)
|
72
|
|
73
|
(* In a previous version, the printer was introducing fake description, ie
|
74
|
tautologies, over inout variables to make sure they were not suppresed by
|
75
|
some other algorithms *)
|
76
|
|
77
|
(* Takes the variable on which these coverage criteria will apply, as well as
|
78
|
the expression and its negated version. Returns the expr and the variable
|
79
|
expression, as well as the two new boolean expressions descibing the two
|
80
|
associated modes. *)
|
81
|
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
|
82
|
let loc = expr.expr_loc in
|
83
|
let not_vi_as_expr = mkpredef_call loc "not" [ vi_as_expr ] in
|
84
|
let expr1, expr2 =
|
85
|
if nb_elems > 1 then
|
86
|
let changed_expr = mkpredef_call loc "!=" [ expr; expr_neg_vi ] in
|
87
|
let expr1 = mkpredef_call loc "&&" [ vi_as_expr; changed_expr ] in
|
88
|
let expr2 = mkpredef_call loc "&&" [ not_vi_as_expr; changed_expr ] in
|
89
|
expr1, expr2
|
90
|
else vi_as_expr, not_vi_as_expr
|
91
|
in
|
92
|
(expr, vi_as_expr), [ true, expr1; false, expr2 ]
|
93
|
(* expr1 corresponds to atom true while expr2 corresponds to atom false *)
|
94
|
|
95
|
(* Format.printf "%a@." Printers.pp_expr expr1; *)
|
96
|
(* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
|
97
|
(* Printers.pp_expr vi_as_expr *)
|
98
|
(* Printers.pp_expr expr (\*v*\) *)
|
99
|
(* Printers.pp_expr expr_neg_vi); *)
|
100
|
(* Format.printf "%a@." Printers.pp_expr expr2; *)
|
101
|
(* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
|
102
|
(* Printers.pp_expr vi_as_expr *)
|
103
|
(* Printers.pp_expr expr (\*v*\) *)
|
104
|
(* Printers.pp_expr expr_neg_vi) *)
|
105
|
|
106
|
let rec compute_neg_expr cpt_pre (expr : Lustre_types.expr) =
|
107
|
let neg_list l =
|
108
|
List.fold_right
|
109
|
(fun e (vl, el) ->
|
110
|
let vl', e' = compute_neg_expr cpt_pre e in
|
111
|
vl' @ vl, e' :: el)
|
112
|
l ([], [])
|
113
|
in
|
114
|
match expr.expr_desc with
|
115
|
| Expr_tuple l ->
|
116
|
let vl, neg = neg_list l in
|
117
|
vl, combine (fun l' -> { expr with expr_desc = Expr_tuple l' }) neg l
|
118
|
| Expr_ite (i, t, e) when Types.is_bool_type t.expr_type ->
|
119
|
let list = [ i; t; e ] in
|
120
|
let vl, neg = neg_list list in
|
121
|
( vl,
|
122
|
combine
|
123
|
(fun l ->
|
124
|
match l with
|
125
|
| [ i'; t'; e' ] ->
|
126
|
{ expr with expr_desc = Expr_ite (i', t', e') }
|
127
|
| _ ->
|
128
|
assert false)
|
129
|
neg list )
|
130
|
| Expr_ite (i, t, e) ->
|
131
|
(* We return the guard as a new guard *)
|
132
|
let vl = gen_mcdc_cond_guard i in
|
133
|
let list = [ i; t; e ] in
|
134
|
let vl', neg = neg_list list in
|
135
|
( vl @ vl',
|
136
|
combine
|
137
|
(fun l ->
|
138
|
match l with
|
139
|
| [ i'; t'; e' ] ->
|
140
|
{ expr with expr_desc = Expr_ite (i', t', e') }
|
141
|
| _ ->
|
142
|
assert false)
|
143
|
neg list )
|
144
|
| Expr_arrow (e1, e2) ->
|
145
|
let vl1, e1' = compute_neg_expr cpt_pre e1 in
|
146
|
let vl2, e2' = compute_neg_expr cpt_pre e2 in
|
147
|
( vl1 @ vl2,
|
148
|
combine
|
149
|
(fun l ->
|
150
|
match l with
|
151
|
| [ x; y ] ->
|
152
|
{ expr with expr_desc = Expr_arrow (x, y) }
|
153
|
| _ ->
|
154
|
assert false)
|
155
|
[ e1'; e2' ] [ e1; e2 ] )
|
156
|
| Expr_pre e ->
|
157
|
let vl, e' = compute_neg_expr (cpt_pre + 1) e in
|
158
|
( vl,
|
159
|
List.map (fun (v, negv) -> v, { expr with expr_desc = Expr_pre negv }) e'
|
160
|
)
|
161
|
| Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
|
162
|
[], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
|
163
|
| Expr_appl (op_name, args, r) ->
|
164
|
let vl, args' = compute_neg_expr cpt_pre args in
|
165
|
( vl,
|
166
|
List.map
|
167
|
(fun (v, negv) ->
|
168
|
v, { expr with expr_desc = Expr_appl (op_name, negv, r) })
|
169
|
args' )
|
170
|
| Expr_ident _ when Types.is_bool_type expr.expr_type ->
|
171
|
[], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
|
172
|
| _ ->
|
173
|
[] (* empty vars *), []
|
174
|
|
175
|
and gen_mcdc_cond_var v expr =
|
176
|
report ~level:1 (fun fmt ->
|
177
|
Format.fprintf fmt
|
178
|
".. Generating MC/DC cond for boolean flow %s and expression %a@." v
|
179
|
Printers.pp_expr expr);
|
180
|
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
|
181
|
let len = List.length leafs_n_neg_expr in
|
182
|
if len >= 1 then
|
183
|
List.fold_left
|
184
|
(fun accu ((vi, nb_pre), expr_neg_vi) ->
|
185
|
mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi :: accu)
|
186
|
vl leafs_n_neg_expr
|
187
|
else vl
|
188
|
|
189
|
and gen_mcdc_cond_guard expr =
|
190
|
report ~level:1 (fun fmt ->
|
191
|
Format.fprintf fmt ".. Generating MC/DC cond for guard %a@."
|
192
|
Printers.pp_expr expr);
|
193
|
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
|
194
|
let len = List.length leafs_n_neg_expr in
|
195
|
if len >= 1 then
|
196
|
List.fold_left
|
197
|
(fun accu ((vi, nb_pre), expr_neg_vi) ->
|
198
|
mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi :: accu)
|
199
|
vl leafs_n_neg_expr
|
200
|
else vl
|
201
|
|
202
|
let rec mcdc_expr cpt_pre expr =
|
203
|
match expr.expr_desc with
|
204
|
| Expr_tuple l ->
|
205
|
let vl =
|
206
|
List.fold_right
|
207
|
(fun e accu_v ->
|
208
|
let vl = mcdc_expr cpt_pre e in
|
209
|
vl @ accu_v)
|
210
|
l []
|
211
|
in
|
212
|
vl
|
213
|
| Expr_ite (i, t, e) ->
|
214
|
let vl_i = gen_mcdc_cond_guard i in
|
215
|
let vl_t = mcdc_expr cpt_pre t in
|
216
|
let vl_e = mcdc_expr cpt_pre e in
|
217
|
vl_i @ vl_t @ vl_e
|
218
|
| Expr_arrow (e1, e2) ->
|
219
|
let vl1 = mcdc_expr cpt_pre e1 in
|
220
|
let vl2 = mcdc_expr cpt_pre e2 in
|
221
|
vl1 @ vl2
|
222
|
| Expr_pre e ->
|
223
|
let vl = mcdc_expr (cpt_pre + 1) e in
|
224
|
vl
|
225
|
| Expr_appl (_, args, _) ->
|
226
|
let vl = mcdc_expr cpt_pre args in
|
227
|
vl
|
228
|
| _ ->
|
229
|
[]
|
230
|
|
231
|
let mcdc_var_def v expr =
|
232
|
if Types.is_bool_type expr.expr_type then
|
233
|
let vl = gen_mcdc_cond_var v expr in
|
234
|
vl
|
235
|
else
|
236
|
let vl = mcdc_expr 0 expr in
|
237
|
vl
|
238
|
|
239
|
let mcdc_node_eq eq =
|
240
|
let vl =
|
241
|
match
|
242
|
( eq.eq_lhs,
|
243
|
Types.is_bool_type eq.eq_rhs.expr_type,
|
244
|
(Types.repr eq.eq_rhs.expr_type).Types.tdesc,
|
245
|
eq.eq_rhs.expr_desc )
|
246
|
with
|
247
|
| [ lhs ], true, _, _ ->
|
248
|
gen_mcdc_cond_var lhs eq.eq_rhs
|
249
|
| _ :: _, false, Types.Ttuple _, Expr_tuple rhs ->
|
250
|
(* We iterate trough pairs, but accumulate variables aside. The resulting
|
251
|
expression shall remain a tuple defintion *)
|
252
|
let vl =
|
253
|
List.fold_right2
|
254
|
(fun lhs rhs accu ->
|
255
|
let v = mcdc_var_def lhs rhs in
|
256
|
(* we don't care about the expression it. We focus on the coverage
|
257
|
expressions in v *)
|
258
|
v @ accu)
|
259
|
eq.eq_lhs rhs []
|
260
|
in
|
261
|
vl
|
262
|
| _ ->
|
263
|
mcdc_expr 0 eq.eq_rhs
|
264
|
in
|
265
|
vl
|
266
|
|
267
|
let mcdc_node_stmt stmt =
|
268
|
match stmt with
|
269
|
| Eq eq ->
|
270
|
let vl = mcdc_node_eq eq in
|
271
|
vl
|
272
|
| Aut _ ->
|
273
|
assert false
|
274
|
|
275
|
let mcdc_top_decl td =
|
276
|
match td.top_decl_desc with
|
277
|
| Node nd ->
|
278
|
let new_coverage_exprs =
|
279
|
List.fold_right
|
280
|
(fun s accu_v ->
|
281
|
let vl' = mcdc_node_stmt s in
|
282
|
vl' @ accu_v)
|
283
|
nd.node_stmts []
|
284
|
in
|
285
|
(* We add coverage vars as boolean internal flows. *)
|
286
|
let fresh_cov_defs =
|
287
|
List.flatten
|
288
|
(List.map
|
289
|
(fun ((_, atom), expr_l) ->
|
290
|
List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l)
|
291
|
new_coverage_exprs)
|
292
|
in
|
293
|
let nb_total = List.length fresh_cov_defs in
|
294
|
let fresh_cov_vars =
|
295
|
List.mapi
|
296
|
(fun i (atom, atom_valid, cov_expr) ->
|
297
|
let loc = cov_expr.expr_loc in
|
298
|
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
|
299
|
let cov_id = Format.flush_str_formatter () in
|
300
|
let cov_var =
|
301
|
mkvar_decl loc
|
302
|
( cov_id,
|
303
|
mktyp loc Tydec_bool,
|
304
|
mkclock loc Ckdec_any,
|
305
|
false,
|
306
|
None,
|
307
|
None )
|
308
|
in
|
309
|
let cov_def = Eq (mkeq loc ([ cov_id ], cov_expr)) in
|
310
|
cov_var, cov_def, atom, atom_valid)
|
311
|
fresh_cov_defs
|
312
|
in
|
313
|
let fresh_vars, fresh_eqs =
|
314
|
List.fold_right
|
315
|
(fun (v, eq, _, _) (accuv, accueq) -> v :: accuv, eq :: accueq)
|
316
|
fresh_cov_vars ([], [])
|
317
|
in
|
318
|
let fresh_annots =
|
319
|
(* We produce two sets of annotations: PROPERTY ones for kind2, and
|
320
|
regular ones to keep track of the nature of the annotations. *)
|
321
|
List.map
|
322
|
(fun (v, _, atom, atom_valid) ->
|
323
|
let e = expr_of_vdecl v in
|
324
|
let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [ e ]) in
|
325
|
{
|
326
|
annots =
|
327
|
[
|
328
|
[ "PROPERTY" ], neg_ee;
|
329
|
(* Using negated property to force model-checker to produce a
|
330
|
suitable covering trace *)
|
331
|
(let loc = Location.dummy_loc in
|
332
|
let valid_e =
|
333
|
let open Corelang in
|
334
|
mkexpr loc (Expr_const (const_of_bool atom_valid))
|
335
|
in
|
336
|
( [ "coverage"; "mcdc"; v.var_id ],
|
337
|
expr_to_eexpr
|
338
|
(Corelang.expr_of_expr_list loc [ e; atom; valid_e ]) ));
|
339
|
];
|
340
|
annot_loc = v.var_loc;
|
341
|
})
|
342
|
fresh_cov_vars
|
343
|
in
|
344
|
Format.printf "%i coverage criteria generated for node %s@ " nb_total
|
345
|
nd.node_id;
|
346
|
(* And add them as annotations --%PROPERTY: var TODO *)
|
347
|
{
|
348
|
td with
|
349
|
top_decl_desc =
|
350
|
Node
|
351
|
{
|
352
|
nd with
|
353
|
node_locals = nd.node_locals @ fresh_vars;
|
354
|
node_stmts = nd.node_stmts @ fresh_eqs;
|
355
|
node_annot = nd.node_annot @ fresh_annots;
|
356
|
};
|
357
|
}
|
358
|
| _ ->
|
359
|
td
|
360
|
|
361
|
let mcdc prog =
|
362
|
(* If main node is provided add silly constraints to show in/out variables in
|
363
|
the path condition *)
|
364
|
(if !Options.main_node <> "" then
|
365
|
inout_vars :=
|
366
|
let top =
|
367
|
List.find
|
368
|
(fun td ->
|
369
|
match td.top_decl_desc with
|
370
|
| Node nd when nd.node_id = !Options.main_node ->
|
371
|
true
|
372
|
| _ ->
|
373
|
false)
|
374
|
prog
|
375
|
in
|
376
|
match top.top_decl_desc with
|
377
|
| Node nd ->
|
378
|
nd.node_inputs @ nd.node_outputs
|
379
|
| _ ->
|
380
|
assert false);
|
381
|
List.map mcdc_top_decl prog
|
382
|
|
383
|
(* Local Variables: *)
|
384
|
(* compile-command:"make -C .." *)
|
385
|
(* End: *)
|