source: src/ERTL/ERTLToLTLI.ma @ 1082

Last change on this file since 1082 was 1082, checked in by mulligan, 9 years ago

work from today on ertl -> ltl pass

File size: 3.5 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ASM/Arithmetic.ma".
4
5inductive decision: Type[0] ≝
6  | decision_spill: Byte → decision
7  | decision_colour: Register → decision.
8 
9(* these are supplied to the functor, fill in later *)
10axiom lookup: register → decision.
11axiom generate: ∀globals: list ident. ltl_statement globals → label.
12axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label.
13axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
14axiom num_locals: nat.
15axiom stacksize: nat.
16(* *** *)
17
18definition adjust_off ≝
19  λoff.
20  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
21  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in
22    sub.
23
24definition get_stack ≝
25  λglobals.
26  λr.
27  λoff.
28  λl.
29    let off ≝ adjust_off off in
30    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l)) in
31    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
32    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
33    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
34    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
35    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
36    let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
37      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
38
39definition set_stack ≝
40  λglobals.
41  λoff.
42  λr.
43  λl.
44  let off ≝ adjust_off off in
45  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
46  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l)) in
47  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
48  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
49  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
50  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
51  let l ≝ label_to_ident (generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
52    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
53
54definition write ≝
55  λglobals.
56  λr: register.
57  λl: ident.
58  match lookup r with
59  [ decision_spill off ⇒ 〈RegisterSST, label_to_ident (generate globals (set_stack globals off RegisterSST l))〉
60  | decision_colour hwr ⇒ 〈hwr, l〉
61  ].
62
63definition read ≝
64  λglobals.
65  λr: register.
66  λstmt: Register → ltl_statement globals.
67  match lookup r with
68  [ decision_colour hwr ⇒ generate globals (stmt hwr)
69  | decision_spill off ⇒
70    let temphwr ≝ RegisterSST in
71    let l ≝ generate globals (stmt temphwr) in
72      generate globals (get_stack globals temphwr off (label_to_ident l))
73  ].
74
Note: See TracBrowser for help on using the repository browser.