1 | include "basics/logic.ma". |
---|
2 | |
---|
3 | include "common/AST.ma". |
---|
4 | include "common/CostLabel.ma". |
---|
5 | include "common/FrontEndOps.ma". |
---|
6 | include "common/Registers.ma". |
---|
7 | |
---|
8 | include "ASM/Vector.ma". |
---|
9 | include "common/Graphs.ma". |
---|
10 | |
---|
11 | inductive 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 | |
---|
30 | definition env_has : list (register × typ) → register → typ → Prop ≝ |
---|
31 | λl,r,t. Exists ? (λx. 〈r,t〉 = x) l. |
---|
32 | |
---|
33 | definition 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 | |
---|
39 | definition 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 | |
---|
59 | lemma 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/ |
---|
62 | qed. |
---|
63 | |
---|
64 | definition labels_present : graph statement → statement → Prop ≝ |
---|
65 | λg,s. labels_P (present ?? g) s. |
---|
66 | |
---|
67 | definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝ |
---|
68 | λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n. |
---|
69 | |
---|
70 | definition graph_closed : graph statement → Prop ≝ |
---|
71 | λg. forall_nodes ? (labels_present g) g. |
---|
72 | definition graph_typed : list (register × typ) → graph statement → Prop ≝ |
---|
73 | λe. forall_nodes ? (statement_typed e). |
---|
74 | |
---|
75 | record 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 | |
---|
93 | definition RTLabs_program ≝ program (λ_.fundef internal_function) nat. |
---|
94 | |
---|
95 | |
---|
96 | |
---|
97 | |
---|
98 | (* Define a notion of sound labellings of RTLabs programs. *) |
---|
99 | |
---|
100 | let rec successors (s : statement) : list label ≝ |
---|
101 | match 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 | |
---|
120 | definition is_cost_label : statement → bool ≝ |
---|
121 | λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. |
---|
122 | |
---|
123 | inductive 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 | |
---|
129 | discriminator nat. |
---|
130 | |
---|
131 | lemma 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 | |
---|
140 | definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. |
---|
141 | |
---|
142 | let rec soundly_labelled_fn (fn : internal_function) : Prop ≝ |
---|
143 | soundly_labelled_pc (f_graph fn) (f_entry fn). |
---|
144 | |
---|