source: src/RTLabs/syntax.ma @ 1045

Last change on this file since 1045 was 1045, checked in by mulligan, 8 years ago

resolved conflict in rtlabs

File size: 2.9 KB
Line 
1
2include "basics/logic.ma".
3
4include "common/AST.ma".
5include "common/CostLabel.ma".
6include "common/FrontEndOps.ma".
7include "common/Registers.ma".
8
9include "ASM/Vector.ma".
10include "common/Graphs.ma".
11
12definition immediate : Type[0] ≝ Byte.
13
14(* Addressing modes *)
15
16inductive 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
25definition 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
34definition addr ≝ λm.Vector register (addr_mode_args m).
35
36inductive 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
53record 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
68definition 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 *)
Note: See TracBrowser for help on using the repository browser.