Revision 3e1d20e0
Added by PierreLoïc Garoche over 4 years ago
src/pathConditions.ml  

7  7  
8  8 
let inout_vars = ref [] 
9  9  
10 
let print_tautology_var fmt v = 

11 
match (Types.repr v.var_type).Types.tdesc with 

12 
 Types.Tbool > Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id 

13 
 Types.Tint > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id 

14 
 Types.Treal > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id 

15 
 _ > Format.fprintf fmt "(true)" 

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

16  19  
17 
let print_path arg = match !inout_vars with


18 
 [] > Format.printf "%t@." arg


19 
 l > Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem > print_tautology_var fmt elem)) l


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


20  23  
21  24 
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ] 
22  25  
23 
let rec print_pre fmt nb_pre = 

24 
if nb_pre <= 0 then () 

25 
else ( 

26 
Format.fprintf fmt "pre "; 

27 
print_pre fmt (nb_pre1) 

28 
) 

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 


29  39 
(* 
30 
let combine2 f sub1 sub2 = 

31 
let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in


32 
let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in


33 
let common = IdSet.inter elem_e1 elem_e2 in


34 
let sub1_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub1 in


35 
let sub2_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub2 in


36 
(List.map (fun (v, negv) > (v, f negv e2)) sub1_filtered) @


37 
(List.map (fun (v, negv) > (v, f e1 negv)) sub2_filtered) @


38 
(List.map (fun v > (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) )


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

39  49 
*) 
40  50  
41  51 
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) = 
...  ...  
53  63 
v, f (select v active_subs subs orig) 
54  64 
) (IdSet.elements all) 
55  65  
56 
let rec compute_neg_expr cpt_pre expr = 

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 

57  98 
match expr.expr_desc with 
58  99 
 Expr_tuple l > 
59 
let neg = List.map (compute_neg_expr cpt_pre) l in


60 
combine (fun l' > {expr with expr_desc = Expr_tuple l'}) neg l 

61  
100 
let vl, neg = neg_list l in


101 
vl, combine (fun l' > {expr with expr_desc = Expr_tuple l'}) neg l


102 


62  103 
 Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool > ( 
63  104 
let list = [i; t; e] in 
64 
let neg = List.map (compute_neg_expr cpt_pre) list in


65 
combine (fun l > 

105 
let vl, neg = neg_list list in


106 
vl, combine (fun l >


66  107 
match l with 
67  108 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
68  109 
 _ > assert false 
69  110 
) neg list 
70  111 
) 
71  112 
 Expr_ite (i,t,e) > ( (* We return the guard as a new guard *) 
72 
gen_mcdc_cond_guard i;


113 
let vl = gen_mcdc_cond_guard i in


73  114 
let list = [i; t; e] in 
74 
let neg = List.map (compute_neg_expr cpt_pre) list in


75 
combine (fun l > 

115 
let vl', neg = neg_list list in


116 
vl@vl', combine (fun l >


76  117 
match l with 
77  118 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
78  119 
 _ > assert false 
79  120 
) neg list 
80  121 
) 
81  122 
 Expr_arrow (e1, e2) > 
82 
let e1' = compute_neg_expr cpt_pre e1 in 

83 
let e2' = compute_neg_expr cpt_pre e2 in 

84 
combine (fun l > match l with 

85 
 [x;y] > { expr with expr_desc = Expr_arrow (x, y) } 

86 
 _ > assert false 

87 
) [e1'; e2'] [e1; e2] 

88 
 Expr_pre e > 

89 
List.map 

90 
(fun (v, negv) > (v, { expr with expr_desc = Expr_pre negv } )) 

91 
(compute_neg_expr (cpt_pre+1) e) 

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' 

92  134  
93  135 
 Expr_appl (op_name, args, r) when List.mem op_name rel_op > 
94 
[(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] 

136 
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]


95  137  
96 
 Expr_appl (op_name, args, r) > 

97 
List.map 

98 
(fun (v, negv) > (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } )) 

99 
(compute_neg_expr cpt_pre args) 

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' 

100  143  
101  144 
 Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool > 
102 
[(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] 

103 
 _ > [] 

104  
105 
and 

106 
gen_mcdc_cond_var v expr = 

107 
report ~level:1 (fun fmt > Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr); 

108 
let leafs_n_neg_expr = compute_neg_expr 0 expr in 

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 

109  153 
if List.length leafs_n_neg_expr > 1 then ( 
110 
List.iter (fun ((vi, nb_pre), expr_neg_vi) > 

111 
print_path (fun fmt > Format.fprintf fmt "%a%a and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi); 

112 
print_path (fun fmt > Format.fprintf fmt "(not %a%a) and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi) 

113 
) leafs_n_neg_expr 

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 

114  157 
) 
158 
else vl 

115  159  
116  160 
and gen_mcdc_cond_guard expr = 
117 
report ~level:1 (fun fmt > Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr); 

118 
let leafs_n_neg_expr = compute_neg_expr 0 expr in 

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 

119  165 
if List.length leafs_n_neg_expr > 1 then ( 
120 
List.iter (fun ((vi, nb_pre), expr_neg_vi) > 

121 
print_path (fun fmt > Format.fprintf fmt "%a%a and (%a != %a)" print_pre nb_pre Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi); 

122 
print_path (fun fmt > Format.fprintf fmt "(not %a%a) and (%a != %a)" print_pre nb_pre Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi) 

123 


124 
) leafs_n_neg_expr 

125 
) 

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 

126  171 

127  172  
128  173 
let rec mcdc_expr cpt_pre expr = 
129  174 
match expr.expr_desc with 
130 
 Expr_tuple l > List.iter (mcdc_expr cpt_pre) l 

131 
 Expr_ite (i,t,e) > (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e]) 

132 
 Expr_arrow (e1, e2) > List.iter (mcdc_expr cpt_pre) [e1; e2] 

133 
 Expr_pre e > mcdc_expr (cpt_pre+1) e 

134 
 Expr_appl (_, args, _) > mcdc_expr cpt_pre args 

135 
 _ > () 

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 
 _ > [] 

136  200  
137  201 
let mcdc_var_def v expr = 
138  202 
match (Types.repr expr.expr_type).Types.tdesc with 
139 
 Types.Tbool > gen_mcdc_cond_var v expr 

140 
 _ > mcdc_expr 0 expr 

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 

141  208  
142  209 
let mcdc_node_eq eq = 
143 
match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with 

144 
 [lhs], Types.Tbool, _ > gen_mcdc_cond_var lhs eq.eq_rhs 

145 
 _::_, Types.Ttuple tl, Expr_tuple rhs > List.iter2 mcdc_var_def eq.eq_lhs rhs 

146 
 _ > mcdc_expr 0 eq.eq_rhs 

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 

147  227  
148  228 
let mcdc_node_stmt stmt = 
149  229 
match stmt with 
150 
 Eq eq > mcdc_node_eq eq


230 
 Eq eq > let vl = mcdc_node_eq eq in vl


151  231 
 Aut aut > assert false 
152  232  
153  233 
let mcdc_top_decl td = 
154  234 
match td.top_decl_desc with 
155 
 Node nd > List.iter mcdc_node_stmt nd.node_stmts 

156 
 _ > () 

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 

157  269  
158  270  
159  271 
let mcdc prog = 
...  ...  
170  282 
match top.top_decl_desc with 
171  283 
 Node nd > nd.node_inputs @ nd.node_outputs 
172  284 
 _ > assert false); 
173 
List.iter mcdc_top_decl prog


285 
List.map mcdc_top_decl prog


174  286  
175  287 
(* Local Variables: *) 
176  288 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
[MCDC] Solved some issues and transformed the code from iterators to fold