source: src/RTLabs/syntax.ma @ 1692

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

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

File size: 4.9 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(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
24*)
25| St_cond : register → label → label → statement
26| St_jumptable : register → list label → statement
27| St_return : statement
28.
29
30definition env_has : list (register × typ) → register → typ → Prop ≝
31λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
32
33definition statement_typed : list (register × typ) → statement → Prop ≝
34λe,s. match s with
35[ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
36| _ ⇒ True
37].
38
39definition labels_P : (label → Prop) → statement → Prop ≝
40λP,s. match s with
41[ St_skip l ⇒ P l
42| St_cost _ l ⇒ P l
43| St_const _ _ l ⇒ P l
44| St_op1 _ _ _ _ _ l ⇒ P l
45| St_op2 _ _ _ _ l ⇒ P l
46| St_load _ _ _ l ⇒ P l
47| St_store _ _ _ l ⇒ P l
48| St_call_id _ _ _ l ⇒ P l
49| St_call_ptr _ _ _ l ⇒ P l
50(*
51| St_tailcall_id _ _ ⇒ True
52| St_tailcall_ptr _ _ ⇒ True
53*)
54| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
55| St_jumptable _ ls ⇒ All ? P ls
56| St_return ⇒ True
57].
58
59lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
60#P #Q #H * /3/
61#r #l #l' * /3/
62qed.
63
64definition labels_present : graph statement → statement → Prop ≝
65λg,s. labels_P (present ?? g) s.
66
67definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
68λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
69
70definition graph_closed : graph statement → Prop ≝
71  λg. forall_nodes ? (labels_present g) g.
72definition graph_typed : list (register × typ) → graph statement → Prop ≝
73  λe. forall_nodes ? (statement_typed e).
74
75record internal_function : Type[0] ≝
76{ f_labgen    : universe LabelTag
77; f_reggen    : universe RegisterTag
78; f_result    : option (register × typ)
79; f_params    : list (register × typ)
80; f_locals    : list (register × typ)
81; f_stacksize : nat
82; f_graph     : graph statement
83; f_closed    : graph_closed f_graph
84; f_typed     : graph_typed (f_locals @ f_params) f_graph
85; f_entry     : Σl:label. present ?? f_graph l
86; f_exit      : Σl:label. present ?? f_graph l
87}.
88
89(* Note that the global variables will be initialised by the code in main
90   by this stage, so the only initialisation data is the amount of space to
91   allocate. *)
92
93definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
94
95
96
97
98(* Define a notion of sound labellings of RTLabs programs. *)
99
100let rec successors (s : statement) : list label ≝
101match s with
102[ St_skip l ⇒ [l]
103| St_cost _ l ⇒ [l]
104| St_const _ _ l ⇒ [l]
105| St_op1 _ _ _ _ _ l ⇒ [l]
106| St_op2 _ _ _ _ l ⇒ [l]
107| St_load _ _ _ l ⇒ [l]
108| St_store _ _ _ l ⇒ [l]
109| St_call_id _ _ _ l ⇒ [l]
110| St_call_ptr _ _ _ l ⇒ [l]
111(*
112| St_tailcall_id _ _ ⇒ [ ]
113| St_tailcall_ptr _ _ ⇒ [ ]
114*)
115| St_cond _ l1 l2 ⇒ [l1; l2]
116| St_jumptable _ ls ⇒ ls
117| St_return ⇒ [ ]
118].
119
120definition is_cost_label : statement → bool ≝
121λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
122
123inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
124| stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n
125| stlb_step : ∀l,n,H.
126    (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) →
127    steps_to_label_bound g l (S n).
128   
129discriminator nat.
130
131lemma steps_to_label_bound_inv_step : ∀g,l,n.
132  steps_to_label_bound g l n →
133  ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) →
134    (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)).
135#g #l0 #n0 #H1 inversion H1
136[ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
137| #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH
138] qed.
139
140definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
141
142let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
143  soundly_labelled_pc (f_graph fn) (f_entry fn).
144
Note: See TracBrowser for help on using the repository browser.