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