1

open LustreSpec

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),[expr1;expr2])

82


83

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

84

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

85

(* Printers.pp_expr vi_as_expr *)

86

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

87

(* Printers.pp_expr expr_neg_vi); *)

88

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

89

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

90

(* Printers.pp_expr vi_as_expr *)

91

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

92

(* Printers.pp_expr expr_neg_vi) *)

93


94

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

95

let neg_list l =

96

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

97

in

98

match expr.expr_desc with

99

 Expr_tuple l >

100

let vl, neg = neg_list l in

101

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

102


103

 Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool > (

104

let list = [i; t; e] in

105

let vl, neg = neg_list list in

106

vl, combine (fun l >

107

match l with

108

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

109

 _ > assert false

110

) neg list

111

)

112

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

113

let vl = gen_mcdc_cond_guard i in

114

let list = [i; t; e] in

115

let vl', neg = neg_list list in

116

vl@vl', combine (fun l >

117

match l with

118

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

119

 _ > assert false

120

) neg list

121

)

122

 Expr_arrow (e1, e2) >

123

let vl1, e1' = compute_neg_expr cpt_pre e1 in

124

let vl2, e2' = compute_neg_expr cpt_pre e2 in

125

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

126

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

127

 _ > assert false

128

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

129


130

 Expr_pre e >

131

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

132

vl, List.map

133

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

134


135

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

136

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

137


138

 Expr_appl (op_name, args, r) >

139

let vl, args' = compute_neg_expr cpt_pre args in

140

vl, List.map

141

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

142

args'

143


144

 Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool >

145

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

146

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

147

and gen_mcdc_cond_var v expr =

148

report ~level:1 (fun fmt >

149

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

150

v

151

Printers.pp_expr expr);

152

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

153

if List.length leafs_n_neg_expr > 1 then (

154

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

155

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

156

) vl leafs_n_neg_expr

157

)

158

else vl

159


160

and gen_mcdc_cond_guard expr =

161

report ~level:1 (fun fmt >

162

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

163

Printers.pp_expr expr);

164

let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in

165

if List.length leafs_n_neg_expr > 1 then (

166

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

167

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

168

) vl leafs_n_neg_expr)

169

else

170

vl

171


172


173

let rec mcdc_expr cpt_pre expr =

174

match expr.expr_desc with

175

 Expr_tuple l >

176

let vl =

177

List.fold_right (fun e accu_v >

178

let vl = mcdc_expr cpt_pre e in

179

(vl@accu_v))

180

l

181

[]

182

in

183

vl

184

 Expr_ite (i,t,e) >

185

let vl_i = gen_mcdc_cond_guard i in

186

let vl_t = mcdc_expr cpt_pre t in

187

let vl_e = mcdc_expr cpt_pre e in

188

vl_i@vl_t@vl_e

189

 Expr_arrow (e1, e2) >

190

let vl1 = mcdc_expr cpt_pre e1 in

191

let vl2 = mcdc_expr cpt_pre e2 in

192

vl1@vl2

193

 Expr_pre e >

194

let vl = mcdc_expr (cpt_pre+1) e in

195

vl

196

 Expr_appl (f, args, r) >

197

let vl = mcdc_expr cpt_pre args in

198

vl

199

 _ > []

200


201

let mcdc_var_def v expr =

202

match (Types.repr expr.expr_type).Types.tdesc with

203

 Types.Tbool >

204

let vl = gen_mcdc_cond_var v expr in

205

vl

206

 _ > let vl = mcdc_expr 0 expr in

207

vl

208


209

let mcdc_node_eq eq =

210

let vl =

211

match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with

212

 [lhs], Types.Tbool, _ > gen_mcdc_cond_var lhs eq.eq_rhs

213

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

214

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

215

expression shall remain a tuple defintion *)

216

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

217

let v = mcdc_var_def lhs rhs in

218

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

219

expressions in v *)

220

v@accu

221

) eq.eq_lhs rhs []

222

in

223

vl

224

 _ > mcdc_expr 0 eq.eq_rhs

225

in

226

vl

227


228

let mcdc_node_stmt stmt =

229

match stmt with

230

 Eq eq > let vl = mcdc_node_eq eq in vl

231

 Aut aut > assert false

232


233

let mcdc_top_decl td =

234

match td.top_decl_desc with

235

 Node nd >

236

let new_coverage_exprs =

237

List.fold_right (

238

fun s accu_v >

239

let vl' = mcdc_node_stmt s in

240

vl'@accu_v

241

) nd.node_stmts []

242

in

243

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

244

let fresh_cov_defs = List.flatten (List.map snd new_coverage_exprs) in

245

let nb_total = List.length fresh_cov_defs in

246

let fresh_cov_vars = List.mapi (fun i cov_expr >

247

let loc = cov_expr.expr_loc in

248

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

249

let cov_id = Format.flush_str_formatter () in

250

let cov_var = mkvar_decl loc

251

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

252

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

253

cov_var, cov_def

254

) fresh_cov_defs

255

in

256

let fresh_vars, fresh_eqs = List.split fresh_cov_vars in

257

let fresh_annots =

258

List.map

259

(fun v > {annots = [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc})

260

fresh_vars in

261

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

262

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

263

{td with top_decl_desc = Node {nd with

264

node_locals = nd.node_locals@fresh_vars;

265

node_stmts = nd.node_stmts@fresh_eqs;

266

node_annot = nd.node_annot@fresh_annots

267

}}

268

 _ > td

269


270


271

let mcdc prog =

272

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

273

if !Options.main_node <> "" then (

274

inout_vars :=

275

let top = List.find

276

(fun td >

277

match td.top_decl_desc with

278

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

279

 _ > false)

280

prog

281

in

282

match top.top_decl_desc with

283

 Node nd > nd.node_inputs @ nd.node_outputs

284

 _ > assert false);

285

List.map mcdc_top_decl prog

286


287

(* Local Variables: *)

288

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

289

(* End: *)

290


291

