source: src/RTLabs/syntax.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 8 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 2.3 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
12inductive statement : Type[0] ≝
13| St_skip : label → statement
14| St_cost : costlabel → label → statement
15| St_const : register → constant → label → statement
16| St_op1 : unary_operation → register → register → label → statement (* destination source *)
17| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
18| St_load : memory_chunk → register → register → label → statement
19| St_store : memory_chunk → register → register → label → statement
20| St_call_id : ident → list register → option register → label → statement
21| St_call_ptr : register → list register → option register → label → statement
22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
24| St_cond : register → label → label → statement
25| St_jumptable : register → list label → statement
26| St_return : statement
27.
28
29record internal_function : Type[0] ≝
30{ f_labgen    : universe LabelTag
31; f_reggen    : universe RegisterTag
32; f_result    : option (register × typ)
33; f_params    : list (register × typ)
34; f_locals    : list (register × typ)
35; f_stacksize : nat
36; f_graph     : graph statement
37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
39}.
40
41(* Note that the global variables will be initialised by the code in main
42   by this stage, so the only initialisation data is the amount of space to
43   allocate. *)
44
45definition RTLabs_program ≝ program (fundef internal_function) nat.
46
47(* TO CONSIDER:
48
49   - removing most successor labels from the statements (bit icky, what about
50     return and jump tables?)
51   - seems like load and store ought to have types that control the size of the
52     register list based on the addressing mode; similarly, memory_chunk and
53     register are probably related.
54   - label and register generation really tell us something about the sets of
55     labels and register that may appear, perhaps it should be renamed, or the
56     graph made dependent on them to make it obvious, etc.
57 *)
Note: See TracBrowser for help on using the repository browser.