59 open Hints_declaration
140 AST.ident List.list -> (Registers.register, I8051.register) Types.prod
141 List.list -> Joint.joint_seq List.list **)
142 let save_hdws globals =
143 let save_hdws_internal = fun destr_srcr -> Joint.MOVE
144 (Obj.magic { Types.fst = (ERTL.PSD destr_srcr.Types.fst); Types.snd =
145 (ERTL.move_src_from_dst (ERTL.HDW destr_srcr.Types.snd)) })
147 List.map save_hdws_internal
149 (** val restore_hdws :
150 AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
151 List.list -> Joint.joint_seq List.list **)
152 let restore_hdws globals =
153 let restore_hdws_internal = fun destr_srcr -> Joint.MOVE
154 (Obj.magic { Types.fst = (ERTL.HDW destr_srcr.Types.snd); Types.snd =
155 (ERTL.psd_argument_move_src destr_srcr.Types.fst) })
157 List.map restore_hdws_internal
159 (** val get_params_hdw :
160 AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
162 let get_params_hdw globals params =
163 save_hdws globals (Util.zip_pottier params I8051.registerParams)
165 (** val get_param_stack :
166 AST.ident List.list -> Registers.register -> Registers.register ->
167 Registers.register -> Joint.joint_seq List.list **)
168 let get_param_stack globals addr1 addr2 destr =
169 List.Cons ((Joint.LOAD ((Obj.magic destr),
170 (Obj.magic (Joint.psd_argument_from_reg addr1)),
171 (Obj.magic (Joint.psd_argument_from_reg addr2)))), (List.Cons ((Joint.OP2
172 (BackEndOps.Add, (Obj.magic addr1),
173 (Obj.magic (Joint.psd_argument_from_reg addr1)),
174 (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
175 (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
176 (Obj.magic (Joint.psd_argument_from_reg addr2)),
177 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
180 (** val get_params_stack :
181 AST.ident List.list -> Registers.register -> Registers.register ->
182 Registers.register -> Registers.register List.list -> Joint.joint_seq
184 let get_params_stack globals tmpr addr1 addr2 params =
185 let params_length_byte =
186 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
187 (Nat.S (Nat.S Nat.O)))))))) (List.length params)
189 List.append (List.Cons
191 ERTL.ertl_seq_joint globals (Obj.magic (ERTL.Ertl_frame_size tmpr))
193 x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
194 (BackEndOps.Sub, (Obj.magic tmpr),
195 (Obj.magic (Joint.psd_argument_from_reg tmpr)),
196 (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
197 (List.Cons ((Joint.MOVE
198 (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
199 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })), (List.Cons
201 (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
202 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })), (List.Cons
203 ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
204 (Obj.magic (Joint.psd_argument_from_reg addr1)),
205 (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons ((Joint.OP2
206 (BackEndOps.Addc, (Obj.magic addr2),
207 (Obj.magic (Joint.psd_argument_from_reg addr2)),
208 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
209 List.Nil))))))))))))))
210 (List.flatten (List.map (get_param_stack globals addr1 addr2) params))
213 AST.ident List.list -> Registers.register -> Registers.register ->
214 Registers.register -> Registers.register List.list -> Joint.joint_seq
216 let get_params globals tmpr addr1 addr2 params =
217 let n = Nat.min (List.length params) (List.length I8051.registerParams) in
218 let { Types.fst = hdw_params; Types.snd = stack_params } =
219 Util.list_split n params
221 List.append (get_params_hdw globals hdw_params)
222 (get_params_stack globals tmpr addr1 addr2 stack_params)
224 (** val save_return :
225 AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
227 let save_return globals ret_regs =
228 let crl = Util.reduce_strong I8051.registerSTS ret_regs in
229 let commonl = crl.Types.fst.Types.fst in
230 let commonr = crl.Types.snd.Types.fst in
231 let restl = crl.Types.fst.Types.snd in
233 (Util.map2 (fun st r -> Joint.MOVE
234 (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
235 (ERTL.psd_argument_move_src r) })) commonl commonr)
236 (List.map (fun st -> Joint.MOVE
237 (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
238 (ERTL.byte_to_ertl_snd_argument__o__psd_argument_to_move_src
239 Joint.zero_byte) })) restl)
241 (** val assign_result : AST.ident List.list -> Joint.joint_seq List.list **)
242 let assign_result globals =
243 let crl = Util.reduce_strong I8051.registerRets I8051.registerSTS in
244 let commonl = crl.Types.fst.Types.fst in
245 let commonr = crl.Types.snd.Types.fst in
246 Util.map2 (fun ret st -> Joint.MOVE
247 (Obj.magic { Types.fst = (ERTL.HDW ret); Types.snd =
248 (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl commonr
251 AST.ident List.list -> Registers.register List.list -> Registers.register
252 -> Registers.register -> (Registers.register, I8051.register) Types.prod
253 List.list -> Joint.joint_seq List.list Types.sig0 **)
254 let epilogue globals ret_regs sral srah sregs =
256 (save_return globals (List.map (fun x -> Joint.Reg x) ret_regs))
258 (restore_hdws globals
259 (List.map (fun pr -> { Types.fst = (Joint.Reg pr.Types.fst);
260 Types.snd = pr.Types.snd }) sregs))
261 (List.append (List.Cons ((Joint.PUSH
262 (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons
263 ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))),
265 ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
266 List.Nil)))))) (assign_result globals)))
269 AST.ident List.list -> Registers.register List.list -> Registers.register
270 -> Registers.register -> Registers.register -> Registers.register ->
271 Registers.register -> (Registers.register, I8051.register) Types.prod
272 List.list -> (Registers.register, Joint.joint_seq List.list)
273 Bind_new.bind_new **)
274 let prologue globals params sral srah tmpr addr1 addr2 sregs =
276 List.append (List.Cons
277 ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
279 x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP
280 (Obj.magic sral)), List.Nil))))))
281 (List.append (save_hdws globals sregs)
282 (get_params globals tmpr addr1 addr2 params))
286 (** val set_params_hdw :
287 AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
289 let set_params_hdw globals params =
290 restore_hdws globals (Util.zip_pottier params I8051.registerParams)
292 (** val set_param_stack :
293 AST.ident List.list -> Registers.register -> Registers.register ->
294 Joint.psd_argument -> Joint.joint_seq List.list **)
295 let set_param_stack globals addr1 addr2 arg =
296 List.Cons ((Joint.STORE ((Obj.magic (Joint.psd_argument_from_reg addr1)),
297 (Obj.magic (Joint.psd_argument_from_reg addr2)), (Obj.magic arg))),
298 (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
299 (Obj.magic (Joint.psd_argument_from_reg addr1)),
300 (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
301 (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
302 (Obj.magic (Joint.psd_argument_from_reg addr2)),
303 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
306 (** val set_params_stack :
307 AST.ident List.list -> Joint.psd_argument List.list ->
308 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
309 let set_params_stack globals params =
310 Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
311 let params_length_byte =
312 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
313 (Nat.S (Nat.S Nat.O)))))))) (List.length params)
316 List.append (List.Cons ((Joint.MOVE
317 (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
318 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
319 (List.Cons ((Joint.MOVE
320 (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
321 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
322 (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
323 (BackEndOps.Sub, (Obj.magic addr1),
324 (Obj.magic (Joint.psd_argument_from_reg addr1)),
325 (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
326 (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic addr2),
327 (Obj.magic (Joint.psd_argument_from_reg addr2)),
328 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
331 (List.map (set_param_stack globals addr1 addr2) params))
336 AST.ident List.list -> Joint.psd_argument List.list ->
337 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
339 let set_params globals params =
340 let n = Nat.min (List.length params) (List.length I8051.registerParams) in
341 let hdw_stack_params = List.split params n in
342 let hdw_params = hdw_stack_params.Types.fst in
343 let stack_params = hdw_stack_params.Types.snd in
345 (let l = set_params_hdw globals hdw_params in Bind_new.Bret l)
346 (set_params_stack globals stack_params)
348 (** val fetch_result :
349 AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
350 List.list Types.sig0 **)
351 let fetch_result globals ret_regs =
352 (let crl = Util.reduce_strong I8051.registerSTS I8051.registerRets in
354 let commonl = crl.Types.fst.Types.fst in
355 let commonr = crl.Types.snd.Types.fst in
357 (Util.map2 (fun st r -> Joint.MOVE
358 (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
359 (ERTL.move_src_from_dst (ERTL.HDW r)) })) commonl commonr)
360 (let crl0 = Util.reduce_strong ret_regs I8051.registerSTS in
361 let commonl0 = crl0.Types.fst.Types.fst in
362 let commonr0 = crl0.Types.snd.Types.fst in
363 Util.map2 (fun ret st -> Joint.MOVE
364 (Obj.magic { Types.fst = (ERTL.PSD ret); Types.snd =
365 (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl0 commonr0))) __
367 (** val translate_step :
368 AST.ident List.list -> Graphs.label -> Joint.joint_step ->
369 Blocks.bind_step_block **)
370 let translate_step globals x = function
371 | Joint.COST_LABEL lbl ->
372 Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
373 Joint.COST_LABEL lbl) }; Types.snd = List.Nil }
374 | Joint.CALL (f, args, ret_regs) ->
376 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
377 (Types.pi1 (Obj.magic (set_params globals (Obj.magic args))))
379 Obj.magic (Bind_new.Bret { Types.fst = { Types.fst =
380 (Blocks.add_dummy_variance pref); Types.snd = (fun x0 -> Joint.CALL
381 (f, (Obj.magic (List.length (Obj.magic args))),
382 (Obj.magic Types.It))) }; Types.snd =
383 (Types.pi1 (fetch_result globals (Obj.magic ret_regs))) })))
384 | Joint.COND (r, ltrue) ->
385 Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
386 Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
387 | Joint.Step_seq s0 ->
390 | Joint.COMMENT msg ->
391 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
392 globals (List.Cons ((Joint.COMMENT msg), List.Nil))
394 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
395 globals (List.Cons ((Joint.MOVE
396 (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
398 (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
401 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
404 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
406 | Joint.ADDRESS (x0, off, r1, r2) ->
407 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
408 globals (List.Cons ((Joint.ADDRESS (x0, off, r1, r2)), List.Nil))
409 | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
410 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
411 globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
413 | Joint.OP1 (op1, destr, srcr) ->
414 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
415 globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))
416 | Joint.OP2 (op2, destr, srcr1, srcr2) ->
417 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
418 globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
420 | Joint.CLEAR_CARRY ->
421 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
422 globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
424 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
425 globals (List.Cons (Joint.SET_CARRY, List.Nil))
426 | Joint.LOAD (destr, addr1, addr2) ->
427 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
428 globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil))
429 | Joint.STORE (addr1, addr2, srcr) ->
430 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
431 globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil))
432 | Joint.Extension_seq ext ->
433 let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
434 Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
435 globals (List.Cons ((Joint.MOVE
436 (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
437 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
438 (List.Cons ((Joint.MOVE
439 (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
440 (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
443 (** val translate_fin_step :
444 AST.ident List.list -> Registers.register List.list -> Registers.register
445 -> Registers.register -> (Registers.register, I8051.register) Types.prod
446 List.list -> Graphs.label -> Joint.joint_fin_step ->
447 Blocks.bind_fin_block **)
448 let translate_fin_step globals ret_regs ral rah to_restore x = function
450 Bind_new.Bret { Types.fst = List.Nil; Types.snd = (Joint.GOTO lbl') }
452 Bind_new.Bret { Types.fst =
453 (Types.pi1 (epilogue globals ret_regs ral rah to_restore)); Types.snd =
455 | Joint.TAILCALL (x0, x1) -> assert false (* absurd case *)
457 (** val allocate_regs :
458 ((Registers.register, I8051.register) Types.prod List.list ->
459 (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
460 Bind_new.bind_new **)
461 let allocate_regs f =
462 let allocate_regs_internal = fun acc r ->
463 Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
464 Obj.magic (Bind_new.Bnew (fun r' ->
466 (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
467 ({ Types.fst = r'; Types.snd = r }, tl))))))
470 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
471 (Util.foldl allocate_regs_internal
472 (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
473 I8051.registerCalleeSaved) (fun to_save -> Obj.magic f to_save))
475 (** val translate_data :
476 AST.ident List.list -> Joint.joint_closed_internal_function ->
477 TranslateUtils.bound_b_graph_translate_data **)
478 let translate_data globals def =
479 let params = (Types.pi1 def).Joint.joint_if_params in
481 Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
482 (Nat.minus (List.length (Obj.magic params))
483 (List.length I8051.registerParams))
485 allocate_regs (fun to_save -> Bind_new.Bnew (fun ral -> Bind_new.Bnew
486 (fun rah -> Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 ->
487 Bind_new.Bnew (fun addr2 ->
489 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
491 (prologue globals (Obj.magic params) ral rah tmpr addr1 addr2
492 to_save)) (fun prologue0 ->
493 Monad.m_return0 (Monad.max_def Bind_new.bindNew)
494 { TranslateUtils.init_ret = (Obj.magic Types.It);
495 TranslateUtils.init_params =
496 (Obj.magic (List.length (Obj.magic params)));
497 TranslateUtils.init_stack_size = new_stacksize;
498 TranslateUtils.added_prologue = prologue0;
499 TranslateUtils.new_regs =
500 (List.reverse (List.Cons (addr2, (List.Cons (addr1, (List.Cons
501 (tmpr, (List.Cons (rah, (List.Cons (ral,
502 (List.map (fun x -> x.Types.fst) to_save))))))))))));
503 TranslateUtils.f_step = (translate_step globals);
504 TranslateUtils.f_fin =
505 (translate_fin_step globals
506 (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
509 (** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
511 TranslateUtils.b_graph_transform_program RTL.rTL ERTL.eRTL translate_data