1

open Lustre_types

2

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

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


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

23


24

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

25


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


39

(*

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

49

*)

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


67

(* In a previous version, the printer was introducing fake

68

description, ie tautologies, over inout variables to make sure they

69

were not suppresed by some other algorithms *)

70


71

(* Takes the variable on which these coverage criteria will apply, as

72

well as the expression and its negated version. Returns the expr

73

and the variable expression, as well as the two new boolean

74

expressions descibing the two associated modes. *)

75

let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =

76

let loc = expr.expr_loc in

77

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

78

let expr1, expr2 =

79

if nb_elems > 1 then

80

let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in

81

let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in

82

let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in

83

expr1, expr2

84

else

85

vi_as_expr, not_vi_as_expr

86

in

87

((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom

88

true while expr2

89

corresponds to atom

90

false *)

91


92

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

93

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

94

(* Printers.pp_expr vi_as_expr *)

95

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

96

(* Printers.pp_expr expr_neg_vi); *)

97

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

98

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

99

(* Printers.pp_expr vi_as_expr *)

100

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

101

(* Printers.pp_expr expr_neg_vi) *)

102


103

let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =

104

let neg_list l =

105

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

106

in

107

match expr.expr_desc with

108

 Expr_tuple l >

109

let vl, neg = neg_list l in

110

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

111


112

 Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) > (

113

let list = [i; t; e] in

114

let vl, neg = neg_list list in

115

vl, combine (fun l >

116

match l with

117

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

118

 _ > assert false

119

) neg list

120

)

121

 Expr_ite (i,t,e) > ( (* We return the guard as a new guard *)

122

let vl = gen_mcdc_cond_guard i in

123

let list = [i; t; e] in

124

let vl', neg = neg_list list in

125

vl@vl', combine (fun l >

126

match l with

127

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

128

 _ > assert false

129

) neg list

130

)

131

 Expr_arrow (e1, e2) >

132

let vl1, e1' = compute_neg_expr cpt_pre e1 in

133

let vl2, e2' = compute_neg_expr cpt_pre e2 in

134

vl1@vl2, combine (fun l > match l with

135

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

136

 _ > assert false

137

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

138


139

 Expr_pre e >

140

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

141

vl, List.map

142

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

143


144

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

145

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

146


147

 Expr_appl (op_name, args, r) >

148

let vl, args' = compute_neg_expr cpt_pre args in

149

vl, List.map

150

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

151

args'

152


153

 Expr_ident _ when (Types.is_bool_type expr.expr_type) >

154

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

155

 _ > [] (* empty vars *) , []

156

and gen_mcdc_cond_var v expr =

157

report ~level:1 (fun fmt >

158

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

159

v

160

Printers.pp_expr expr);

161

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

162

let len = List.length leafs_n_neg_expr in

163

if len >= 1 then (

164

List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) >

165

(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu

166

) vl leafs_n_neg_expr

167

)

168

else

169

vl

170


171

and gen_mcdc_cond_guard expr =

172

report ~level:1 (fun fmt >

173

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

174

Printers.pp_expr expr);

175

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

176

let len = List.length leafs_n_neg_expr in

177

if len >= 1 then (

178

List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) >

179

(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu

180

) vl leafs_n_neg_expr)

181

else

182

vl

183


184


185

let rec mcdc_expr cpt_pre expr =

186

match expr.expr_desc with

187

 Expr_tuple l >

188

let vl =

189

List.fold_right (fun e accu_v >

190

let vl = mcdc_expr cpt_pre e in

191

(vl@accu_v))

192

l

193

[]

194

in

195

vl

196

 Expr_ite (i,t,e) >

197

let vl_i = gen_mcdc_cond_guard i in

198

let vl_t = mcdc_expr cpt_pre t in

199

let vl_e = mcdc_expr cpt_pre e in

200

vl_i@vl_t@vl_e

201

 Expr_arrow (e1, e2) >

202

let vl1 = mcdc_expr cpt_pre e1 in

203

let vl2 = mcdc_expr cpt_pre e2 in

204

vl1@vl2

205

 Expr_pre e >

206

let vl = mcdc_expr (cpt_pre+1) e in

207

vl

208

 Expr_appl (f, args, r) >

209

let vl = mcdc_expr cpt_pre args in

210

vl

211

 _ > []

212


213

let mcdc_var_def v expr =

214

if Types.is_bool_type expr.expr_type then

215

let vl = gen_mcdc_cond_var v expr in

216

vl

217

else

218

let vl = mcdc_expr 0 expr in

219

vl

220


221

let mcdc_node_eq eq =

222

let vl =

223

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

224

 [lhs], true, _, _ > gen_mcdc_cond_var lhs eq.eq_rhs

225

 _::_, false, Types.Ttuple tl, Expr_tuple rhs >

226

(* We iterate trough pairs, but accumulate variables aside. The resulting

227

expression shall remain a tuple defintion *)

228

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

229

let v = mcdc_var_def lhs rhs in

230

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

231

expressions in v *)

232

v@accu

233

) eq.eq_lhs rhs []

234

in

235

vl

236

 _ > mcdc_expr 0 eq.eq_rhs

237

in

238

vl

239


240

let mcdc_node_stmt stmt =

241

match stmt with

242

 Eq eq > let vl = mcdc_node_eq eq in vl

243

 Aut aut > assert false

244


245

let mcdc_top_decl td =

246

match td.top_decl_desc with

247

 Node nd >

248

let new_coverage_exprs =

249

List.fold_right (

250

fun s accu_v >

251

let vl' = mcdc_node_stmt s in

252

vl'@accu_v

253

) nd.node_stmts []

254

in

255

(* We add coverage vars as boolean internal flows. *)

256

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

257

let nb_total = List.length fresh_cov_defs in

258

let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) >

259

let loc = cov_expr.expr_loc in

260

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

261

let cov_id = Format.flush_str_formatter () in

262

let cov_var = mkvar_decl loc

263

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

264

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

265

cov_var, cov_def, atom, atom_valid

266

) fresh_cov_defs

267

in

268

let fresh_vars, fresh_eqs =

269

List.fold_right

270

(fun (v,eq,_,_) (accuv, accueq)> v::accuv, eq::accueq )

271

fresh_cov_vars

272

([], [])

273

in

274

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

275

kind2, and regular ones to keep track of the nature

276

of the annotations. *)

277

List.map

278

(fun (v, _, atom, atom_valid) >

279

let e = expr_of_vdecl v in

280

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

281

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

282

modelchecker to produce a

283

suitable covering trace *)

284

let loc = Location.dummy_loc in

285

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

286

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

287

];

288

annot_loc = v.var_loc})

289

fresh_cov_vars

290

in

291

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

292

(* And add them as annotations %PROPERTY: var TODO *)

293

{td with top_decl_desc = Node {nd with

294

node_locals = nd.node_locals@fresh_vars;

295

node_stmts = nd.node_stmts@fresh_eqs;

296

node_annot = nd.node_annot@fresh_annots

297

}}

298

 _ > td

299


300


301

let mcdc prog =

302

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

303

if !Options.main_node <> "" then (

304

inout_vars :=

305

let top = List.find

306

(fun td >

307

match td.top_decl_desc with

308

 Node nd when nd.node_id = !Options.main_node > true

309

 _ > false)

310

prog

311

in

312

match top.top_decl_desc with

313

 Node nd > nd.node_inputs @ nd.node_outputs

314

 _ > assert false);

315

List.map mcdc_top_decl prog

316


317


318


319

(* Local Variables: *)

320

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

321

(* End: *)

322


323

