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

82

true while expr2

83

corresponds to atom

84

false *)

85


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

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

98

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

match expr.expr_desc with

102

 Expr_tuple l >

103

let vl, neg = neg_list l in

104

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

105


106

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

107

let list = [i; t; e] in

108

let vl, neg = neg_list list in

109

vl, combine (fun l >

110

match l with

111

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

112

 _ > assert false

113

) neg list

114

)

115

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

116

let vl = gen_mcdc_cond_guard i in

117

let list = [i; t; e] in

118

let vl', neg = neg_list list in

119

vl@vl', combine (fun l >

120

match l with

121

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

122

 _ > assert false

123

) neg list

124

)

125

 Expr_arrow (e1, e2) >

126

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


138

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

139

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

140


141

 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


147

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

148

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

if List.length leafs_n_neg_expr >= 1 then (

157

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

)

161

else

162

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

163

vl

164


165

and gen_mcdc_cond_guard expr =

166

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

if List.length leafs_n_neg_expr >= 1 then (

171

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

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

176

vl

177


178


179

let rec mcdc_expr cpt_pre expr =

180

match expr.expr_desc with

181

 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


207

let mcdc_var_def v expr =

208

if Types.is_bool_type expr.expr_type then

209

let vl = gen_mcdc_cond_var v expr in

210

vl

211

else

212

let vl = mcdc_expr 0 expr in

213

vl

214


215

let mcdc_node_eq eq =

216

let vl =

217

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

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

219

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

220

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


234

let mcdc_node_stmt stmt =

235

match stmt with

236

 Eq eq > let vl = mcdc_node_eq eq in vl

237

 Aut aut > assert false

238


239

let mcdc_top_decl td =

240

match td.top_decl_desc with

241

 Node nd >

242

let new_coverage_exprs =

243

List.fold_right (

244

fun s accu_v >

245

let vl' = mcdc_node_stmt s in

246

vl'@accu_v

247

) nd.node_stmts []

248

in

249

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

let nb_total = List.length fresh_cov_defs in

252

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

in

262

let fresh_vars, fresh_eqs =

263

List.fold_right

264

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

265

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

List.map

272

(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

modelchecker to produce a

277

suitable covering trace *)

278

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

];

282

annot_loc = v.var_loc})

283

fresh_cov_vars

284

in

285

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

286

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

287

{td with top_decl_desc = Node {nd with

288

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

 _ > td

293


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

List.map mcdc_top_decl prog

310


311


312


313

(* Local Variables: *)

314

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

315

(* End: *)

316


317

