1

open Lustre_types

2

open Corelang

3

open Log

4


5

module IdSet = Set.Make (struct type t = expr * int let compare = compare end)

6


7

let inout_vars = ref []

8


9

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

10

reactivated later *)

11


12

(* let print_tautology_var fmt v = *)

13

(* match (Types.repr v.var_type).Types.tdesc with *)

14

(*  Types.Tbool > Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)

15

(*  Types.Tint > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)

16

(*  Types.Treal > Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)

17

(*  _ > Format.fprintf fmt "(true)" *)

18


19

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

20

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

21

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

22


23

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

24


25

(* Used when we were printing the expression directly. Now we are constructing

26

them as regular expressions.

27


28

let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf

29

fmt "pre "; print_pre fmt (nb_pre1) )

30

*)

31


32

let mk_pre n e =

33

if n <= 0 then

34

e

35

else

36

mkexpr e.expr_loc (Expr_pre e)

37


38

(*

39

let combine2 f sub1 sub2 =

40

let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in

41

let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in

42

let common = IdSet.inter elem_e1 elem_e2 in

43

let sub1_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub1 in

44

let sub2_filtered = List.filter (fun (v, _) > not (IdSet.mem v common)) sub2 in

45

(List.map (fun (v, negv) > (v, f negv e2)) sub1_filtered) @

46

(List.map (fun (v, negv) > (v, f e1 negv)) sub2_filtered) @

47

(List.map (fun v > (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) )

48

*)

49


50

let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =

51

match active, modified, orig with

52

 true::active_tl, e::modified_tl, _::orig_tl > (List.assoc v e)::(select v active_tl modified_tl orig_tl)

53

 false::active_tl, _::modified_tl, e::orig_tl > e::(select v active_tl modified_tl orig_tl)

54

 [], [], [] > []

55

 _ > assert false

56


57

let combine (f: expr list > expr ) subs orig : ((expr * int) * expr) list =

58

let elems = List.map (fun sub_i > List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in

59

let all = List.fold_right IdSet.union elems IdSet.empty in

60

List.map (fun v >

61

let active_subs = List.map (IdSet.mem v) elems in

62

v, f (select v active_subs subs orig)

63

) (IdSet.elements all)

64


65


66

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

67

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

68

were not suppresed by some other algorithms *)

69


70

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

71

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

72

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

73

expressions descibing the two associated modes. *)

74

let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =

75

let loc = expr.expr_loc in

76

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

77

let expr1, expr2 =

78

if nb_elems > 1 then

79

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

80

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

81

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

82

expr1, expr2

83

else

84

vi_as_expr, not_vi_as_expr

85

in

86

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

87

true while expr2

88

corresponds to atom

89

false *)

90


91

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

92

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

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

97

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

98

(* Printers.pp_expr vi_as_expr *)

99

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

100

(* Printers.pp_expr expr_neg_vi) *)

101


102

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

103

let neg_list l =

104

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

105

in

106

match expr.expr_desc with

107

 Expr_tuple l >

108

let vl, neg = neg_list l in

109

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

110


111

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

112

let list = [i; t; e] in

113

let vl, neg = neg_list list in

114

vl, combine (fun l >

115

match l with

116

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

117

 _ > assert false

118

) neg list

119

)

120

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

121

let vl = gen_mcdc_cond_guard i in

122

let list = [i; t; e] in

123

let vl', neg = neg_list list in

124

vl@vl', combine (fun l >

125

match l with

126

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

127

 _ > assert false

128

) neg list

129

)

130

 Expr_arrow (e1, e2) >

131

let vl1, e1' = compute_neg_expr cpt_pre e1 in

132

let vl2, e2' = compute_neg_expr cpt_pre e2 in

133

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

134

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

135

 _ > assert false

136

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

137


138

 Expr_pre e >

139

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

140

vl, List.map

141

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

142


143

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

144

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

145


146

 Expr_appl (op_name, args, r) >

147

let vl, args' = compute_neg_expr cpt_pre args in

148

vl, List.map

149

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

150

args'

151


152

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

153

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

154

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

155

and gen_mcdc_cond_var v expr =

156

report ~level:1 (fun fmt >

157

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

158

v

159

Printers.pp_expr expr);

160

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

161

let len = List.length leafs_n_neg_expr in

162

if len >= 1 then (

163

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

164

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

165

) vl leafs_n_neg_expr

166

)

167

else

168

vl

169


170

and gen_mcdc_cond_guard expr =

171

report ~level:1 (fun fmt >

172

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

173

Printers.pp_expr expr);

174

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

175

let len = List.length leafs_n_neg_expr in

176

if len >= 1 then (

177

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

178

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

179

) vl leafs_n_neg_expr)

180

else

181

vl

182


183


184

let rec mcdc_expr cpt_pre expr =

185

match expr.expr_desc with

186

 Expr_tuple l >

187

let vl =

188

List.fold_right (fun e accu_v >

189

let vl = mcdc_expr cpt_pre e in

190

(vl@accu_v))

191

l

192

[]

193

in

194

vl

195

 Expr_ite (i,t,e) >

196

let vl_i = gen_mcdc_cond_guard i in

197

let vl_t = mcdc_expr cpt_pre t in

198

let vl_e = mcdc_expr cpt_pre e in

199

vl_i@vl_t@vl_e

200

 Expr_arrow (e1, e2) >

201

let vl1 = mcdc_expr cpt_pre e1 in

202

let vl2 = mcdc_expr cpt_pre e2 in

203

vl1@vl2

204

 Expr_pre e >

205

let vl = mcdc_expr (cpt_pre+1) e in

206

vl

207

 Expr_appl (_, args, _) >

208

let vl = mcdc_expr cpt_pre args in

209

vl

210

 _ > []

211


212

let mcdc_var_def v expr =

213

if Types.is_bool_type expr.expr_type then

214

let vl = gen_mcdc_cond_var v expr in

215

vl

216

else

217

let vl = mcdc_expr 0 expr in

218

vl

219


220

let mcdc_node_eq eq =

221

let vl =

222

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

223

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

224

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

225

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

226

expression shall remain a tuple defintion *)

227

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

228

let v = mcdc_var_def lhs rhs in

229

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

230

expressions in v *)

231

v@accu

232

) eq.eq_lhs rhs []

233

in

234

vl

235

 _ > mcdc_expr 0 eq.eq_rhs

236

in

237

vl

238


239

let mcdc_node_stmt stmt =

240

match stmt with

241

 Eq eq > let vl = mcdc_node_eq eq in vl

242

 Aut _ > assert false

243


244

let mcdc_top_decl td =

245

match td.top_decl_desc with

246

 Node nd >

247

let new_coverage_exprs =

248

List.fold_right (

249

fun s accu_v >

250

let vl' = mcdc_node_stmt s in

251

vl'@accu_v

252

) nd.node_stmts []

253

in

254

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

255

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

256

let nb_total = List.length fresh_cov_defs in

257

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

258

let loc = cov_expr.expr_loc in

259

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

260

let cov_id = Format.flush_str_formatter () in

261

let cov_var = mkvar_decl loc

262

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

263

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

264

cov_var, cov_def, atom, atom_valid

265

) fresh_cov_defs

266

in

267

let fresh_vars, fresh_eqs =

268

List.fold_right

269

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

270

fresh_cov_vars

271

([], [])

272

in

273

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

274

kind2, and regular ones to keep track of the nature

275

of the annotations. *)

276

List.map

277

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

278

let e = expr_of_vdecl v in

279

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

280

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

281

modelchecker to produce a

282

suitable covering trace *)

283

let loc = Location.dummy_loc in

284

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

285

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

286

];

287

annot_loc = v.var_loc})

288

fresh_cov_vars

289

in

290

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

291

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

292

{td with top_decl_desc = Node {nd with

293

node_locals = nd.node_locals@fresh_vars;

294

node_stmts = nd.node_stmts@fresh_eqs;

295

node_annot = nd.node_annot@fresh_annots

296

}}

297

 _ > td

298


299


300

let mcdc prog =

301

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

302

if !Options.main_node <> "" then (

303

inout_vars :=

304

let top = List.find

305

(fun td >

306

match td.top_decl_desc with

307

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

308

 _ > false)

309

prog

310

in

311

match top.top_decl_desc with

312

 Node nd > nd.node_inputs @ nd.node_outputs

313

 _ > assert false);

314

List.map mcdc_top_decl prog

315


316


317


318

(* Local Variables: *)

319

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

320

(* End: *)

321


322

