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