1 | |
---|
2 | include "basics/logic.ma". |
---|
3 | |
---|
4 | include "common/AST.ma". |
---|
5 | include "common/CostLabel.ma". |
---|
6 | include "common/FrontEndOps.ma". |
---|
7 | include "common/Registers.ma". |
---|
8 | |
---|
9 | include "ASM/Vector.ma". |
---|
10 | include "common/Graphs.ma". |
---|
11 | |
---|
12 | (* XXX: ASTish stuff *) |
---|
13 | |
---|
14 | definition immediate : Type[0] ≝ int. |
---|
15 | |
---|
16 | (* Addressing modes *) |
---|
17 | |
---|
18 | inductive addressing : Type[0] ≝ |
---|
19 | | Aindexed : immediate → addressing (* r1 + offset *) |
---|
20 | | Aindexed2 : addressing (* r1 + r2 *) |
---|
21 | | Aglobal : ident → immediate → addressing (* global + offset *) |
---|
22 | | Abased : ident → immediate → addressing (* global + offset + r1 *) |
---|
23 | | Ainstack : immediate → addressing (* stack + offset *) |
---|
24 | . |
---|
25 | |
---|
26 | definition addr_mode_args : addressing → nat ≝ |
---|
27 | λa. match a with |
---|
28 | [ Aindexed _ ⇒ 1 |
---|
29 | | Aindexed2 ⇒ 2 |
---|
30 | | Aglobal _ _ ⇒ 0 |
---|
31 | | Abased _ _ ⇒ 1 |
---|
32 | | Ainstack _ ⇒ 0 |
---|
33 | ]. |
---|
34 | |
---|
35 | definition addr ≝ λm.Vector register (addr_mode_args m). |
---|
36 | |
---|
37 | (* Statements, including the label of successor(s). *) |
---|
38 | |
---|
39 | inductive statement : Type[0] ≝ |
---|
40 | | St_skip : label → statement |
---|
41 | | St_cost : costlabel → label → statement |
---|
42 | | St_const : register → constant → label → statement |
---|
43 | | St_op1 : unary_operation → register → register → label → statement |
---|
44 | | St_op2 : binary_operation → register → register → register → label → statement |
---|
45 | | St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement |
---|
46 | | St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement |
---|
47 | | St_call_id : ident → list register → option register → label → statement |
---|
48 | | St_call_ptr : register → list register → option register → label → statement |
---|
49 | | St_tailcall_id : ident → list register → statement |
---|
50 | | St_tailcall_ptr : register → list register → statement |
---|
51 | (* Um, what? *) |
---|
52 | | St_condcst : constant → label → label → statement |
---|
53 | | St_cond1 : unary_operation → register → label → label → statement |
---|
54 | | St_cond2 : binary_operation → register → register → label → label → statement |
---|
55 | | St_jumptable : register → list label → statement |
---|
56 | | St_return : statement |
---|
57 | . |
---|
58 | |
---|
59 | record internal_function : Type[0] ≝ |
---|
60 | { f_labgen : universe LabelTag |
---|
61 | ; f_reggen : universe RegisterTag |
---|
62 | ; f_sig : signature |
---|
63 | ; f_result : option register |
---|
64 | ; f_params : list register |
---|
65 | ; f_locals : list register |
---|
66 | ; f_ptrs : list register |
---|
67 | ; f_stacksize : nat |
---|
68 | ; f_graph : graph statement |
---|
69 | ; f_entry : label |
---|
70 | ; f_exit : label |
---|
71 | }. |
---|
72 | |
---|
73 | (* Note that the global variables will be initialised by the code in main |
---|
74 | by this stage. All initialisation data should only reserve space. *) |
---|
75 | |
---|
76 | definition RTLabs_program ≝ program (fundef internal_function) unit. |
---|
77 | |
---|
78 | (* TO CONSIDER: |
---|
79 | |
---|
80 | - removing most successor labels from the statements (bit icky, what about |
---|
81 | return and jump tables?) |
---|
82 | - seems like load and store ought to have types that control the size of the |
---|
83 | register list based on the addressing mode; similarly, memory_chunk and |
---|
84 | register are probably related. |
---|
85 | - label and register generation really tell us something about the sets of |
---|
86 | labels and register that may appear, perhaps it should be renamed, or the |
---|
87 | graph made dependent on them to make it obvious, etc. |
---|
88 | *) |
---|