1

open Lustre_types

2

open Corelang

3

open Log

4


5

module IdSet = Set.Make (struct

6

type t = expr * int

7


8

let compare = compare

9

end)

10


11

let inout_vars = ref []

12


13

(* This was used to add inout variables in the final signature. May have to be

14

reactivated later *)

15


16

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

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


23

(* let print_path arg = match !inout_vars with *)

24

(*  [] > Format.printf "%t@." arg *)

25

(*  l > Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun

26

fmt elem > print_tautology_var fmt elem)) l *)

27


28

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

29


30

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

fmt "pre "; print_pre fmt (nb_pre1) ) *)

35


36

let mk_pre n e = if n <= 0 then e else mkexpr e.expr_loc (Expr_pre e)

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

47


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

59


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

81

let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =

82

let loc = expr.expr_loc in

83

let not_vi_as_expr = mkpredef_call loc "not" [ vi_as_expr ] in

84

let expr1, expr2 =

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

89

expr1, expr2

90

else vi_as_expr, not_vi_as_expr

91

in

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

105


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 ([], [])

113

in

114

match expr.expr_desc with

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

120

let vl, neg = neg_list list in

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

132

let vl = gen_mcdc_cond_guard i in

133

let list = [ i; t; e ] in

134

let vl', neg = neg_list list in

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

156

 Expr_pre e >

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

)

161

 Expr_appl (op_name, _, _) when List.mem op_name rel_op >

162

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

163

 Expr_appl (op_name, args, r) >

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 *), []

174


175

and gen_mcdc_cond_var v expr =

176

report ~level:1 (fun fmt >

177

Format.fprintf fmt

178

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

179

Printers.pp_expr expr);

180

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

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

188


189

and gen_mcdc_cond_guard expr =

190

report ~level:1 (fun fmt >

191

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

192

Printers.pp_expr expr);

193

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

194

let len = List.length leafs_n_neg_expr in

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

201


202

let rec mcdc_expr cpt_pre expr =

203

match expr.expr_desc with

204

 Expr_tuple l >

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

218

 Expr_arrow (e1, e2) >

219

let vl1 = mcdc_expr cpt_pre e1 in

220

let vl2 = mcdc_expr cpt_pre e2 in

221

vl1 @ vl2

222

 Expr_pre e >

223

let vl = mcdc_expr (cpt_pre + 1) e in

224

vl

225

 Expr_appl (_, args, _) >

226

let vl = mcdc_expr cpt_pre args in

227

vl

228

 _ >

229

[]

230


231

let mcdc_var_def v expr =

232

if Types.is_bool_type expr.expr_type then

233

let vl = gen_mcdc_cond_var v expr in

234

vl

235

else

236

let vl = mcdc_expr 0 expr in

237

vl

238


239

let mcdc_node_eq eq =

240

let vl =

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

264

in

265

vl

266


267

let mcdc_node_stmt stmt =

268

match stmt with

269

 Eq eq >

270

let vl = mcdc_node_eq eq in

271

vl

272

 Aut _ >

273

assert false

274


275

let mcdc_top_decl td =

276

match td.top_decl_desc with

277

 Node nd >

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

360


361

let mcdc prog =

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

381

List.map mcdc_top_decl prog

382


383

(* Local Variables: *)

384

(* compilecommand:"make C .." *)

385

(* End: *)
