source: Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma @ 1105

Last change on this file since 1105 was 1105, checked in by campbell, 9 years ago

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

File size: 3.0 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
17| St_op2 : binary_operation → register → register → register → label → statement
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
29definition labels_P : (label → Prop) → statement → Prop ≝
30λP,s. match s with
31[ St_skip l ⇒ P l
32| St_cost _ l ⇒ P l
33| St_const _ _ l ⇒ P l
34| St_op1 _ _ _ l ⇒ P l
35| St_op2 _ _ _ _ l ⇒ P l
36| St_load _ _ _ l ⇒ P l
37| St_store _ _ _ l ⇒ P l
38| St_call_id _ _ _ l ⇒ P l
39| St_call_ptr _ _ _ l ⇒ P l
40| St_tailcall_id _ _ ⇒ True
41| St_tailcall_ptr _ _ ⇒ True
42| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
43| St_jumptable _ ls ⇒ All ? P ls
44| St_return ⇒ True
45].
46
47lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
48#P #Q #H * /3/
49#r #l #l' * /3/
50qed.
51
52definition labels_present : graph statement → statement → Prop ≝
53λg,s. labels_P (present ?? g) s.
54
55definition graph_closed : graph statement → Prop ≝
56λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
57
58record internal_function : Type[0] ≝
59{ f_labgen    : universe LabelTag
60; f_reggen    : universe RegisterTag
61; f_result    : option (register × typ)
62; f_params    : list (register × typ)
63; f_locals    : list (register × typ)
64; f_stacksize : nat
65; f_graph     : graph statement
66; f_closed    : graph_closed f_graph
67; f_entry     : Σl:label. present ?? f_graph l
68; f_exit      : Σl:label. present ?? f_graph l
69}.
70
71(* Note that the global variables will be initialised by the code in main
72   by this stage.  All initialisation data should only reserve space. *)
73
74definition RTLabs_program ≝ program (fundef internal_function) unit.
75
76(* TO CONSIDER:
77
78   - removing most successor labels from the statements (bit icky, what about
79     return and jump tables?)
80   - seems like load and store ought to have types that control the size of the
81     register list based on the addressing mode; similarly, memory_chunk and
82     register are probably related.
83   - label and register generation really tell us something about the sets of
84     labels and register that may appear, perhaps it should be renamed, or the
85     graph made dependent on them to make it obvious, etc.
86 *)
Note: See TracBrowser for help on using the repository browser.