## lustrec/src/pathConditions.ml @ ca7ff3f7

1 | ca7ff3f7 | Lélio Brun | open Lustre_types |
---|---|---|---|

2 | 40d33d55 | xavier.thirioux | open Corelang |

3 | open Log |
||

4 | |||

5 | ca7ff3f7 | Lélio Brun | module IdSet = Set.Make (struct |

6 | type t = expr * int |
||

7 | 40d33d55 | xavier.thirioux | |

8 | ca7ff3f7 | Lélio Brun | let compare = compare |

9 | end) |
||

10 | |||

11 | let inout_vars = ref [] |
||

12 | 40d33d55 | xavier.thirioux | |

13 | 3e1d20e0 | ploc | ```
(* This was used to add inout variables in the final signature. May have to be
``` |

14 | ```
reactivated later *)
``` |
||

15 | ca7ff3f7 | Lélio Brun | |

16 | 3e1d20e0 | ploc | ```
(* 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 | ca7ff3f7 | Lélio Brun | ```
(* | 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 | 40d33d55 | xavier.thirioux | |

23 | 3e1d20e0 | ploc | ```
(* let print_path arg = match !inout_vars with *)
``` |

24 | ```
(* | [] -> Format.printf "%t@." arg *)
``` |
||

25 | ca7ff3f7 | Lélio Brun | ```
(* | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun
``` |

26 | ```
fmt elem -> print_tautology_var fmt elem)) l *)
``` |
||

27 | 40d33d55 | xavier.thirioux | |

28 | ca7ff3f7 | Lélio Brun | let rel_op = [ "="; "!="; "<"; "<="; ">"; ">=" ] |

29 | 40d33d55 | xavier.thirioux | |

30 | 3e1d20e0 | ploc | ```
(* 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 | ca7ff3f7 | Lélio Brun | ```
fmt "pre "; print_pre fmt (nb_pre-1) ) *)
``` |

35 | 40d33d55 | xavier.thirioux | |

36 | ca7ff3f7 | Lélio Brun | let mk_pre n e = if n <= 0 then e else mkexpr e.expr_loc (Expr_pre e) |

37 | 40d33d55 | xavier.thirioux | |

38 | ca7ff3f7 | Lélio Brun | ```
(* 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 | 3e1d20e0 | ploc | |

48 | ca7ff3f7 | Lélio Brun | 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 | 2104c80a | ploc | |

60 | ca7ff3f7 | Lélio Brun | 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 | 2104c80a | ploc | let mcdc_var vi_as_expr nb_elems expr expr_neg_vi = |

82 | 3e1d20e0 | ploc | let loc = expr.expr_loc in |

83 | ca7ff3f7 | Lélio Brun | let not_vi_as_expr = mkpredef_call loc "not" [ vi_as_expr ] in |

84 | 2104c80a | ploc | let expr1, expr2 = |

85 | ca7ff3f7 | Lélio Brun | 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 | 2104c80a | ploc | expr1, expr2 |

90 | ca7ff3f7 | Lélio Brun | else vi_as_expr, not_vi_as_expr |

91 | 2104c80a | ploc | ```
in
``` |

92 | ca7ff3f7 | Lélio Brun | (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 | 3e1d20e0 | ploc | |

106 | ca7ff3f7 | Lélio Brun | 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 | 3e1d20e0 | ploc | ```
in
``` |

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

115 | ca7ff3f7 | Lélio Brun | | 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 | 3e1d20e0 | ploc | let vl, neg = neg_list list in |

121 | ca7ff3f7 | Lélio Brun | ( 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 | 3e1d20e0 | ploc | let vl = gen_mcdc_cond_guard i in |

133 | ca7ff3f7 | Lélio Brun | let list = [ i; t; e ] in |

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

135 | ca7ff3f7 | Lélio Brun | ( 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 | 3e1d20e0 | ploc | | Expr_pre e -> |

157 | ca7ff3f7 | Lélio Brun | 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 | ca7e8027 | Lélio Brun | | Expr_appl (op_name, _, _) when List.mem op_name rel_op -> |

162 | ca7ff3f7 | Lélio Brun | [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ] |

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

164 | ca7ff3f7 | Lélio Brun | 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 | 40d33d55 | xavier.thirioux | |

175 | 3e1d20e0 | ploc | and gen_mcdc_cond_var v expr = |

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

177 | ca7ff3f7 | Lélio Brun | Format.fprintf fmt |

178 | ".. Generating MC/DC cond for boolean flow %s and expression %a@." v |
||

179 | 2104c80a | ploc | Printers.pp_expr expr); |

180 | 3e1d20e0 | ploc | let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |

181 | ca7ff3f7 | Lélio Brun | 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 | 40d33d55 | xavier.thirioux | |

189 | and gen_mcdc_cond_guard expr = |
||

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

191 | ca7ff3f7 | Lélio Brun | Format.fprintf fmt ".. Generating MC/DC cond for guard %a@." |

192 | 2104c80a | ploc | Printers.pp_expr expr); |

193 | 3e1d20e0 | ploc | let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |

194 | 2104c80a | ploc | let len = List.length leafs_n_neg_expr in |

195 | ca7ff3f7 | Lélio Brun | 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 | 40d33d55 | xavier.thirioux | |

202 | ca7ff3f7 | Lélio Brun | let rec mcdc_expr cpt_pre expr = |

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

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

205 | ca7ff3f7 | Lélio Brun | 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 | 3e1d20e0 | ploc | | Expr_arrow (e1, e2) -> |

219 | ca7ff3f7 | Lélio Brun | let vl1 = mcdc_expr cpt_pre e1 in |

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

221 | vl1 @ vl2 |
||

222 | 3e1d20e0 | ploc | | Expr_pre e -> |

223 | ca7ff3f7 | Lélio Brun | let vl = mcdc_expr (cpt_pre + 1) e in |

224 | ```
vl
``` |
||

225 | ca7e8027 | Lélio Brun | | Expr_appl (_, args, _) -> |

226 | ca7ff3f7 | Lélio Brun | let vl = mcdc_expr cpt_pre args in |

227 | ```
vl
``` |
||

228 | | _ -> |
||

229 | ```
[]
``` |
||

230 | 40d33d55 | xavier.thirioux | |

231 | ca7ff3f7 | Lélio Brun | let mcdc_var_def v expr = |

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

233 | ca7ff3f7 | Lélio Brun | let vl = gen_mcdc_cond_var v expr in |

234 | ```
vl
``` |
||

235 | 66359a5e | ploc | ```
else
``` |

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

237 | ```
vl
``` |
||

238 | ca7ff3f7 | Lélio Brun | |

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

240 | 3e1d20e0 | ploc | let vl = |

241 | ca7ff3f7 | Lélio Brun | ```
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 | 3e1d20e0 | ploc | ```
in
``` |

265 | ```
vl
``` |
||

266 | 40d33d55 | xavier.thirioux | |

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

268 | match stmt with |
||

269 | ca7ff3f7 | Lélio Brun | | Eq eq -> |

270 | let vl = mcdc_node_eq eq in |
||

271 | ```
vl
``` |
||

272 | | Aut _ -> |
||

273 | assert false |
||

274 | bde99c3f | xavier.thirioux | |

275 | ca7ff3f7 | Lélio Brun | let mcdc_top_decl td = |

276 | 40d33d55 | xavier.thirioux | match td.top_decl_desc with |

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

278 | ca7ff3f7 | Lélio Brun | 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 | 40d33d55 | xavier.thirioux | |

361 | let mcdc prog = |
||

362 | ca7ff3f7 | Lélio Brun | ```
(* 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 | 3e1d20e0 | ploc | List.map mcdc_top_decl prog |

382 | 40d33d55 | xavier.thirioux | |

383 | ```
(* Local Variables: *)
``` |
||

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

385 | ```
(* End: *)
``` |