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_pre1) ) 

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_pre1) ) *) 

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 
modelchecker 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 modelchecker 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 
(* compilecommand:"make C .." *) 
320  385 
(* End: *) 
321  
322 

Also available in: Unified diff
reformatting