1

open LustreSpec

2

open Corelang

3


4

let check_node_name id = (fun t >

5

match t.top_decl_desc with

6

 Node nd > nd.node_id = id

7

 _ > false)

8


9


10

(*

11

expr, locals', eqs = inline_call id args' reset locals nodes

12


13

We select the called node equations and variables.

14

renamed_inputs = args

15

renamed_eqs

16


17

the resulting expression is tuple_of_renamed_outputs

18


19

TODO: convert the specification/annotation/assert and inject them

20

TODO: deal with reset

21

*)

22

let inline_call orig_expr args reset locals node =

23

let loc = orig_expr.expr_loc in

24

let uid = orig_expr.expr_tag in

25

let rename v =

26

Format.fprintf Format.str_formatter "%s_%i_%s"

27

node.node_id uid v;

28

Format.flush_str_formatter ()

29

in

30

let eqs' = List.map

31

(fun eq > { eq with

32

eq_lhs = List.map rename eq.eq_lhs;

33

eq_rhs = expr_replace_var rename eq.eq_rhs

34

} ) node.node_eqs

35

in

36

let rename_var v = { v with var_id = rename v.var_id } in

37

let inputs' = List.map rename_var node.node_inputs in

38

let outputs' = List.map rename_var node.node_outputs in

39

let locals' = List.map rename_var node.node_locals in

40


41

(* checking we are at the appropriate (early) step: node_checks and

42

node_gencalls should be empty (not yet assigned) *)

43

assert (node.node_checks = []);

44

assert (node.node_gencalls = []);

45


46

(* Bug included: todo deal with reset *)

47

assert (reset = None);

48


49

let assign_inputs = mkeq loc (List.map (fun v > v.var_id) inputs', args) in

50

let expr = expr_of_expr_list

51

loc

52

(List.map (fun v > mkexpr loc (Expr_ident v.var_id)) outputs')

53

in

54

expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs'

55


56


57


58


59

(*

60

new_expr, new_locals, new_eqs = inline_expr expr locals nodes

61


62

Each occurence of a node in nodes in the expr should be replaced by fresh

63

variables and the code of called node instance added to new_eqs

64


65

*)

66

let rec inline_expr expr locals nodes =

67

let inline_tuple el =

68

List.fold_right (fun e (el_tail, locals, eqs) >

69

let e', locals', eqs' = inline_expr e locals nodes in

70

e'::el_tail, locals', eqs'@eqs

71

) el ([], locals, [])

72

in

73

let inline_pair e1 e2 =

74

let el', l', eqs' = inline_tuple [e1;e2] in

75

match el' with

76

 [e1'; e2'] > e1', e2', l', eqs'

77

 _ > assert false

78

in

79

let inline_triple e1 e2 e3 =

80

let el', l', eqs' = inline_tuple [e1;e2;e3] in

81

match el' with

82

 [e1'; e2'; e3'] > e1', e2', e3', l', eqs'

83

 _ > assert false

84

in

85


86

match expr.expr_desc with

87

 Expr_appl (id, args, reset) >

88

let args', locals', eqs' = inline_expr args locals nodes in

89

if List.exists (check_node_name id) nodes then

90

(* The node should be inlined *)

91

(* let _ = Format.eprintf "Inlining call to %s@." id in

92

*) let node = try List.find (check_node_name id) nodes

93

with Not_found > (assert false) in

94

let node = match node.top_decl_desc with Node nd > nd  _ > assert false in

95

let node = inline_node node nodes in

96

let expr, locals', eqs'' =

97

inline_call expr args' reset locals' node in

98

expr, locals', eqs'@eqs''

99

else

100

(* let _ = Format.eprintf "Not inlining call to %s@." id in *)

101

{ expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs'

102


103

(* For other cases, we just keep the structure, but convert subexpressions *)

104

 Expr_const _

105

 Expr_ident _ > expr, locals, []

106

 Expr_tuple el >

107

let el', l', eqs' = inline_tuple el in

108

{ expr with expr_desc = Expr_tuple el' }, l', eqs'

109

 Expr_ite (g, t, e) >

110

let g', t', e', l', eqs' = inline_triple g t e in

111

{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs'

112

 Expr_arrow (e1, e2) >

113

let e1', e2', l', eqs' = inline_pair e1 e2 in

114

{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs'

115

 Expr_fby (e1, e2) >

116

let e1', e2', l', eqs' = inline_pair e1 e2 in

117

{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs'

118

 Expr_array el >

119

let el', l', eqs' = inline_tuple el in

120

{ expr with expr_desc = Expr_array el' }, l', eqs'

121

 Expr_access (e, dim) >

122

let e', l', eqs' = inline_expr e locals nodes in

123

{ expr with expr_desc = Expr_access (e', dim) }, l', eqs'

124

 Expr_power (e, dim) >

125

let e', l', eqs' = inline_expr e locals nodes in

126

{ expr with expr_desc = Expr_power (e', dim) }, l', eqs'

127

 Expr_pre e >

128

let e', l', eqs' = inline_expr e locals nodes in

129

{ expr with expr_desc = Expr_pre e' }, l', eqs'

130

 Expr_when (e, id, label) >

131

let e', l', eqs' = inline_expr e locals nodes in

132

{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs'

133

 Expr_merge (id, branches) >

134

let el, l', eqs' = inline_tuple (List.map snd branches) in

135

let branches' = List.map2 (fun (label, _) v > label, v) branches el in

136

{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs'

137

 Expr_uclock _

138

 Expr_dclock _

139

 Expr_phclock _ > assert false

140

and inline_node nd nodes =

141

let new_locals, eqs =

142

List.fold_left (fun (locals, eqs) eq >

143

let eq_rhs', locals', new_eqs' =

144

inline_expr eq.eq_rhs locals nodes

145

in

146

locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs

147

) (nd.node_locals, []) nd.node_eqs

148

in

149

{ nd with

150

node_locals = new_locals;

151

node_eqs = eqs

152

}

153


154

let inline_all_calls node nodes =

155

let nd = match node.top_decl_desc with Node nd > nd  _ > assert false in

156

{ node with top_decl_desc = Node (inline_node nd nodes) }

157


158


159


160


161


162

let witness filename main_name orig inlined type_env clock_env =

163

let loc = Location.dummy_loc in

164

let rename_local_node nodes prefix id =

165

if List.exists (check_node_name id) nodes then

166

prefix ^ id

167

else

168

id

169

in

170

let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with

171

Node nd > nd  _ > assert false in

172


173

let orig_rename = rename_local_node orig "orig_" in

174

let inlined_rename = rename_local_node inlined "inlined_" in

175

let identity = (fun x > x) in

176

let is_node top = match top.top_decl_desc with Node _ > true  _ > false in

177

let orig = rename_prog orig_rename identity identity orig in

178

let inlined = rename_prog inlined_rename identity identity inlined in

179

let nodes_origs, others = List.partition is_node orig in

180

let nodes_inlined, _ = List.partition is_node inlined in

181


182

(* One ok_i boolean variable per output var *)

183

let nb_outputs = List.length main_orig_node.node_outputs in

184

let ok_i = List.map (fun id >

185

mkvar_decl

186

loc

187

("OK" ^ string_of_int id,

188

{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},

189

{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},

190

false)

191

) (Utils.enumerate nb_outputs)

192

in

193


194

(* OK = ok_1 and ok_2 and ... ok_n1 *)

195

let ok_ident = "OK" in

196

let ok_output = mkvar_decl

197

loc

198

(ok_ident,

199

{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},

200

{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},

201

false)

202

in

203

let main_ok_expr =

204

let mkv x = mkexpr loc (Expr_ident x) in

205

match ok_i with

206

 [] > assert false

207

 [x] > mkv x.var_id

208

 hd::tl >

209

List.fold_left (fun accu elem >

210

mkpredef_call loc "&&" [mkv elem.var_id; accu]

211

) (mkv hd.var_id) tl

212

in

213


214

(* Building main node *)

215


216

let main_node = {

217

node_id = "check";

218

node_type = Types.new_var ();

219

node_clock = Clocks.new_var true;

220

node_inputs = main_orig_node.node_inputs;

221

node_outputs = [ok_output];

222

node_locals = [];

223

node_gencalls = [];

224

node_checks = [];

225

node_asserts = [];

226

node_eqs = [

227

{ eq_loc = loc;

228

eq_lhs = List.map (fun v > v.var_id) ok_i;

229

eq_rhs =

230

let inputs = expr_of_expr_list loc (List.map (fun v > mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in

231

let call_orig =

232

mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in

233

let call_inlined =

234

mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in

235

let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in

236

mkexpr loc (Expr_appl ("=", args, None))

237

};

238

{ eq_loc = loc;

239

eq_lhs = [ok_ident];

240

eq_rhs = main_ok_expr;

241

}

242

];

243

node_dec_stateless = false;

244

node_stateless = None;

245

node_spec = Some

246

{requires = [];

247

ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];

248

behaviors = []

249

};

250

node_annot = None;

251

}

252

in

253

let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in

254

let new_prog = others@nodes_origs@nodes_inlined@main in

255

let _ = Typing.type_prog type_env new_prog in

256

let _ = Clock_calculus.clock_prog clock_env new_prog in

257


258


259

let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in

260

let witness_out = open_out witness_file in

261

let witness_fmt = Format.formatter_of_out_channel witness_out in

262

Format.fprintf witness_fmt

263

"(* Generated lustre file to check validity of inlining process *)@.";

264

Printers.pp_prog witness_fmt new_prog;

265

Format.fprintf witness_fmt "@.";

266

() (* xx *)

267


268

let global_inline basename prog type_env clock_env =

269

(* We select the main node desc *)

270

let main_node, other_nodes, other_tops =

271

List.fold_left

272

(fun (main_opt, nodes, others) top >

273

match top.top_decl_desc with

274

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

275

Some top, nodes, others

276

 Node _ > main_opt, top::nodes, others

277

 _ > main_opt, nodes, top::others)

278

(None, [], []) prog

279

in

280

(* Recursively each call of a node in the top node is replaced *)

281

let main_node = Utils.desome main_node in

282

let main_node' = inline_all_calls main_node other_nodes in

283

let res = main_node'::other_tops in

284

if !Options.witnesses then (

285

witness

286

basename

287

(match main_node.top_decl_desc with Node nd > nd.node_id  _ > assert false)

288

prog res type_env clock_env

289

);

290

res

291


292

(* Local Variables: *)

293

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

294

(* End: *)
