source: src/RTLabs/syntax.ma @ 1656

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

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File size: 3.2 KB
Line 
1include "basics/logic.ma".
2
3include "common/AST.ma".
4include "common/CostLabel.ma".
5include "common/FrontEndOps.ma".
6include "common/Registers.ma".
7
8include "ASM/Vector.ma".
9include "common/Graphs.ma".
10
11inductive statement : Type[0] ≝
12| St_skip : label → statement
13| St_cost : costlabel → label → statement
14| St_const : register → constant → label → statement
15| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
16| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
17| St_load : memory_chunk → register → register → label → statement
18| St_store : memory_chunk → register → register → label → statement
19| St_call_id : ident → list register → option register → label → statement
20| St_call_ptr : register → list register → option register → label → statement
21| St_tailcall_id : ident → list register → statement
22| St_tailcall_ptr : register → list register → statement
23| St_cond : register → label → label → statement
24| St_jumptable : register → list label → statement
25| St_return : statement
26.
27
28definition env_has : list (register × typ) → register → typ → Prop ≝
29λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
30
31definition statement_typed : list (register × typ) → statement → Prop ≝
32λe,s. match s with
33[ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
34| _ ⇒ True
35].
36
37definition labels_P : (label → Prop) → statement → Prop ≝
38λP,s. match s with
39[ St_skip l ⇒ P l
40| St_cost _ l ⇒ P l
41| St_const _ _ l ⇒ P l
42| St_op1 _ _ _ _ _ l ⇒ P l
43| St_op2 _ _ _ _ l ⇒ P l
44| St_load _ _ _ l ⇒ P l
45| St_store _ _ _ l ⇒ P l
46| St_call_id _ _ _ l ⇒ P l
47| St_call_ptr _ _ _ l ⇒ P l
48| St_tailcall_id _ _ ⇒ True
49| St_tailcall_ptr _ _ ⇒ True
50| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
51| St_jumptable _ ls ⇒ All ? P ls
52| St_return ⇒ True
53].
54
55lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
56#P #Q #H * /3/
57#r #l #l' * /3/
58qed.
59
60definition labels_present : graph statement → statement → Prop ≝
61λg,s. labels_P (present ?? g) s.
62
63definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
64λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
65
66definition graph_closed : graph statement → Prop ≝
67  λg. forall_nodes ? (labels_present g) g.
68definition graph_typed : list (register × typ) → graph statement → Prop ≝
69  λe. forall_nodes ? (statement_typed e).
70
71record internal_function : Type[0] ≝
72{ f_labgen    : universe LabelTag
73; f_reggen    : universe RegisterTag
74; f_result    : option (register × typ)
75; f_params    : list (register × typ)
76; f_locals    : list (register × typ)
77; f_stacksize : nat
78; f_graph     : graph statement
79; f_closed    : graph_closed f_graph
80; f_typed     : graph_typed (f_locals @ f_params) f_graph
81; f_entry     : Σl:label. present ?? f_graph l
82; f_exit      : Σl:label. present ?? f_graph l
83}.
84
85(* Note that the global variables will be initialised by the code in main
86   by this stage, so the only initialisation data is the amount of space to
87   allocate. *)
88
89definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.