## lustrec / src / pathConditions.ml @ e8250987

History | View | Annotate | Download (11.5 KB)

1 | 8446bf03 | ploc | open Lustre_types |
---|---|---|---|

2 | 40d33d55 | xavier.thirioux | 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 | 3e1d20e0 | ploc | (* 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 | 40d33d55 | xavier.thirioux | |

20 | 3e1d20e0 | ploc | (* 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 | 40d33d55 | xavier.thirioux | |

24 | let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ] |
||

25 | |||

26 | 3e1d20e0 | ploc | (* 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_pre-1) ) |
||

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 | 40d33d55 | xavier.thirioux | (* |

40 | 3e1d20e0 | ploc | 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 | 40d33d55 | xavier.thirioux | *) |

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 | 3e1d20e0 | ploc | |

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 | 8cacf677 | ploc | ((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom |

82 | true while expr2 |
||

83 | corresponds to atom |
||

84 | false *) |
||

85 | 3e1d20e0 | ploc | |

86 | (* Format.printf "%a@." Printers.pp_expr expr1; *) |
||

87 | (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *) |
||

88 | (* Printers.pp_expr vi_as_expr *) |
||

89 | (* Printers.pp_expr expr (\*v*\) *) |
||

90 | (* Printers.pp_expr expr_neg_vi); *) |
||

91 | (* Format.printf "%a@." Printers.pp_expr expr2; *) |
||

92 | (* print_path (fun fmt -> Format.fprintf fmt "(not %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 | |||

97 | 8446bf03 | ploc | let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) = |

98 | 3e1d20e0 | ploc | let neg_list l = |

99 | List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], []) |
||

100 | in |
||

101 | 40d33d55 | xavier.thirioux | match expr.expr_desc with |

102 | | Expr_tuple l -> |
||

103 | 3e1d20e0 | ploc | let vl, neg = neg_list l in |

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

105 | |||

106 | 66359a5e | ploc | | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> ( |

107 | 40d33d55 | xavier.thirioux | let list = [i; t; e] in |

108 | 3e1d20e0 | ploc | let vl, neg = neg_list list in |

109 | vl, combine (fun l -> |
||

110 | 2fdbc781 | ploc | match l with |

111 | | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')} |
||

112 | | _ -> assert false |
||

113 | ) neg list |
||

114 | ) |
||

115 | 40d33d55 | xavier.thirioux | | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *) |

116 | 3e1d20e0 | ploc | let vl = gen_mcdc_cond_guard i in |

117 | 40d33d55 | xavier.thirioux | let list = [i; t; e] in |

118 | 3e1d20e0 | ploc | let vl', neg = neg_list list in |

119 | vl@vl', combine (fun l -> |
||

120 | 2fdbc781 | ploc | match l with |

121 | | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')} |
||

122 | | _ -> assert false |
||

123 | ) neg list |
||

124 | 40d33d55 | xavier.thirioux | ) |

125 | | Expr_arrow (e1, e2) -> |
||

126 | 3e1d20e0 | ploc | let vl1, e1' = compute_neg_expr cpt_pre e1 in |

127 | let vl2, e2' = compute_neg_expr cpt_pre e2 in |
||

128 | vl1@vl2, combine (fun l -> match l with |
||

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

130 | | _ -> assert false |
||

131 | ) [e1'; e2'] [e1; e2] |
||

132 | |||

133 | | Expr_pre e -> |
||

134 | let vl, e' = compute_neg_expr (cpt_pre+1) e in |
||

135 | vl, List.map |
||

136 | (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e' |
||

137 | 40d33d55 | xavier.thirioux | |

138 | | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> |
||

139 | 3e1d20e0 | ploc | [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |

140 | 40d33d55 | xavier.thirioux | |

141 | 3e1d20e0 | ploc | | Expr_appl (op_name, args, r) -> |

142 | let vl, args' = compute_neg_expr cpt_pre args in |
||

143 | vl, List.map |
||

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

145 | args' |
||

146 | 40d33d55 | xavier.thirioux | |

147 | 66359a5e | ploc | | Expr_ident _ when (Types.is_bool_type expr.expr_type) -> |

148 | 3e1d20e0 | ploc | [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |

149 | | _ -> [] (* empty vars *) , [] |
||

150 | and gen_mcdc_cond_var v expr = |
||

151 | report ~level:1 (fun fmt -> |
||

152 | Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." |
||

153 | v |
||

154 | Printers.pp_expr expr); |
||

155 | let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |
||

156 | ff6ba54e | ploc | if List.length leafs_n_neg_expr >= 1 then ( |

157 | 3e1d20e0 | ploc | List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) -> |

158 | (mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu |
||

159 | ) vl leafs_n_neg_expr |
||

160 | 40d33d55 | xavier.thirioux | ) |

161 | ff6ba54e | ploc | else |

162 | (* TODO: deal with the case length xxx = 1 with a simpler condition *) |
||

163 | vl |
||

164 | 40d33d55 | xavier.thirioux | |

165 | and gen_mcdc_cond_guard expr = |
||

166 | 3e1d20e0 | ploc | report ~level:1 (fun fmt -> |

167 | Format.fprintf fmt".. Generating MC/DC cond for guard %a@." |
||

168 | Printers.pp_expr expr); |
||

169 | let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |
||

170 | ff6ba54e | ploc | if List.length leafs_n_neg_expr >= 1 then ( |

171 | 3e1d20e0 | ploc | List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) -> |

172 | (mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu |
||

173 | ) vl leafs_n_neg_expr) |
||

174 | else |
||

175 | ff6ba54e | ploc | (* TODO: deal with the case length xxx = 1 with a simpler condition *) |

176 | 3e1d20e0 | ploc | vl |

177 | 40d33d55 | xavier.thirioux | |

178 | |||

179 | let rec mcdc_expr cpt_pre expr = |
||

180 | match expr.expr_desc with |
||

181 | 3e1d20e0 | ploc | | Expr_tuple l -> |

182 | let vl = |
||

183 | List.fold_right (fun e accu_v -> |
||

184 | let vl = mcdc_expr cpt_pre e in |
||

185 | (vl@accu_v)) |
||

186 | l |
||

187 | [] |
||

188 | in |
||

189 | vl |
||

190 | | Expr_ite (i,t,e) -> |
||

191 | let vl_i = gen_mcdc_cond_guard i in |
||

192 | let vl_t = mcdc_expr cpt_pre t in |
||

193 | let vl_e = mcdc_expr cpt_pre e in |
||

194 | vl_i@vl_t@vl_e |
||

195 | | Expr_arrow (e1, e2) -> |
||

196 | let vl1 = mcdc_expr cpt_pre e1 in |
||

197 | let vl2 = mcdc_expr cpt_pre e2 in |
||

198 | vl1@vl2 |
||

199 | | Expr_pre e -> |
||

200 | let vl = mcdc_expr (cpt_pre+1) e in |
||

201 | vl |
||

202 | | Expr_appl (f, args, r) -> |
||

203 | let vl = mcdc_expr cpt_pre args in |
||

204 | vl |
||

205 | | _ -> [] |
||

206 | 40d33d55 | xavier.thirioux | |

207 | let mcdc_var_def v expr = |
||

208 | 66359a5e | ploc | if Types.is_bool_type expr.expr_type then |

209 | 3e1d20e0 | ploc | let vl = gen_mcdc_cond_var v expr in |

210 | vl |
||

211 | 66359a5e | ploc | else |

212 | let vl = mcdc_expr 0 expr in |
||

213 | vl |
||

214 | |||

215 | 40d33d55 | xavier.thirioux | let mcdc_node_eq eq = |

216 | 3e1d20e0 | ploc | let vl = |

217 | 66359a5e | ploc | 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 |

218 | 8cacf677 | ploc | | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs |

219 | 66359a5e | ploc | | _::_, false, Types.Ttuple tl, Expr_tuple rhs -> |

220 | 3e1d20e0 | ploc | (* We iterate trough pairs, but accumulate variables aside. The resulting |

221 | expression shall remain a tuple defintion *) |
||

222 | let vl = List.fold_right2 (fun lhs rhs accu -> |
||

223 | let v = mcdc_var_def lhs rhs in |
||

224 | (* we don't care about the expression it. We focus on the coverage |
||

225 | expressions in v *) |
||

226 | v@accu |
||

227 | ) eq.eq_lhs rhs [] |
||

228 | in |
||

229 | vl |
||

230 | | _ -> mcdc_expr 0 eq.eq_rhs |
||

231 | in |
||

232 | vl |
||

233 | 40d33d55 | xavier.thirioux | |

234 | bde99c3f | xavier.thirioux | let mcdc_node_stmt stmt = |

235 | match stmt with |
||

236 | 3e1d20e0 | ploc | | Eq eq -> let vl = mcdc_node_eq eq in vl |

237 | bde99c3f | xavier.thirioux | | Aut aut -> assert false |

238 | |||

239 | 40d33d55 | xavier.thirioux | let mcdc_top_decl td = |

240 | match td.top_decl_desc with |
||

241 | 3e1d20e0 | ploc | | Node nd -> |

242 | let new_coverage_exprs = |
||

243 | List.fold_right ( |
||

244 | 8cacf677 | ploc | fun s accu_v -> |

245 | 3e1d20e0 | ploc | let vl' = mcdc_node_stmt s in |

246 | vl'@accu_v |
||

247 | 8cacf677 | ploc | ) nd.node_stmts [] |

248 | 3e1d20e0 | ploc | in |

249 | 8cacf677 | ploc | (* We add coverage vars as boolean internal flows. *) |

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

251 | 3e1d20e0 | ploc | let nb_total = List.length fresh_cov_defs in |

252 | 8cacf677 | ploc | let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) -> |

253 | let loc = cov_expr.expr_loc in |
||

254 | Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total; |
||

255 | let cov_id = Format.flush_str_formatter () in |
||

256 | let cov_var = mkvar_decl loc |
||

257 | (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in |
||

258 | let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in |
||

259 | cov_var, cov_def, atom, atom_valid |
||

260 | ) fresh_cov_defs |
||

261 | 3e1d20e0 | ploc | in |

262 | 66359a5e | ploc | let fresh_vars, fresh_eqs = |

263 | List.fold_right |
||

264 | 8cacf677 | ploc | (fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq ) |

265 | 66359a5e | ploc | fresh_cov_vars |

266 | ([], []) |
||

267 | in |
||

268 | let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for |
||

269 | kind2, and regular ones to keep track of the nature |
||

270 | of the annotations. *) |
||

271 | 3e1d20e0 | ploc | List.map |

272 | 8cacf677 | ploc | (fun (v, _, atom, atom_valid) -> |

273 | let e = expr_of_vdecl v in |
||

274 | let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in |
||

275 | {annots = [["PROPERTY"], neg_ee; (* Using negated property to force |
||

276 | model-checker to produce a |
||

277 | suitable covering trace *) |
||

278 | c95a441d | ploc | let loc = Location.dummy_loc in |

279 | let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in |
||

280 | ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e]) |
||

281 | 8cacf677 | ploc | ]; |

282 | annot_loc = v.var_loc}) |
||

283 | fresh_cov_vars |
||

284 | 66359a5e | ploc | in |

285 | Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id; |
||

286 | 3e1d20e0 | ploc | (* And add them as annotations --%PROPERTY: var TODO *) |

287 | {td with top_decl_desc = Node {nd with |
||

288 | 8cacf677 | ploc | node_locals = nd.node_locals@fresh_vars; |

289 | node_stmts = nd.node_stmts@fresh_eqs; |
||

290 | node_annot = nd.node_annot@fresh_annots |
||

291 | }} |
||

292 | 3e1d20e0 | ploc | | _ -> td |

293 | 40d33d55 | xavier.thirioux | |

294 | |||

295 | let mcdc prog = |
||

296 | (* If main node is provided add silly constraints to show in/out variables in the path condition *) |
||

297 | if !Options.main_node <> "" then ( |
||

298 | inout_vars := |
||

299 | let top = List.find |
||

300 | (fun td -> |
||

301 | match td.top_decl_desc with |
||

302 | | Node nd when nd.node_id = !Options.main_node -> true |
||

303 | | _ -> false) |
||

304 | prog |
||

305 | in |
||

306 | match top.top_decl_desc with |
||

307 | | Node nd -> nd.node_inputs @ nd.node_outputs |
||

308 | | _ -> assert false); |
||

309 | 3e1d20e0 | ploc | List.map mcdc_top_decl prog |

310 | 40d33d55 | xavier.thirioux | |

311 | 66359a5e | ploc | |

312 | |||

313 | 40d33d55 | xavier.thirioux | (* Local Variables: *) |

314 | (* compile-command:"make -C .." *) |
||

315 | (* End: *) |
||

316 | |||

317 |