source: src/RTLabs/RTLabs_abstract.ma @ 2716

Last change on this file since 2716 was 2716, checked in by sacerdot, 7 years ago

utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction

File size: 13.1 KB
Line 
1include "RTLabs/RTLabs_semantics.ma".
2
3(* Avoid aliasing in interstage proofs *)
4
5definition RTLabs_state ≝ state.
6definition RTLabs_genv ≝ genv.
7
8(* Build a full abstract status record that can be used with structured traces. *)
9
10include "common/StructuredTraces.ma".
11include "RTLabs/CostSpec.ma". (* TODO: relocate definitions? *)
12include "utilities/deqsets_extras.ma".
13discriminator status_class.
14
15(* We augment states with a stack of function blocks (i.e. pointers) so that we
16   can make sensible "program counters" for the abstract state definition, along
17   with a proof that we will get the correct code when we do the lookup (which
18   is done to find cost labels given a pc).
19   
20   Adding them to the semantics is an alternative, more direct approach.
21   However, it makes animating the semantics extremely difficult, because it
22   is hard to avoid normalising and displaying irrelevant parts of the global
23   environment and proofs.
24   
25   We use blocks rather than identifiers because the global environments go
26
27     identifier → block → definition
28   
29   and we'd have to introduce backwards lookups to find identifiers for
30   function pointers.
31 *)
32
33definition Ras_Fn_Match ≝
34λge,state,fn_stack.
35  match state with
36  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
37  | Callstate _ fd _ _ fs _ ⇒
38      match fn_stack with
39      [ nil ⇒ False
40      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
41        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
42      ]
43  | Returnstate _ _ fs _ ⇒
44      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
45  | Finalstate _ ⇒ fn_stack = [ ]
46  ].
47
48record RTLabs_ext_state (ge:genv) : Type[0] ≝ {
49  Ras_state :> state;
50  Ras_fn_stack : list block;
51  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
52}.
53
54(* Given a plain step of the RTLabs semantics, give the next state along with
55   the shadow stack of function block numbers.  Carefully defined so that the
56   coercion back to the plain state always reduces. *)
57definition next_state : ∀ge. ∀s:RTLabs_ext_state ge. ∀s':state. ∀t.
58  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
59λge,s,s',t,EX. mk_RTLabs_ext_state ge s'
60 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
61 ?.
62cases s' in EX ⊢ %;
63[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
64  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
65    whd cases stk in mtc ⊢ %; [ * ]
66    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
67    | @M2 ]
68  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
69  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
70    whd cases stk in mtc ⊢ %; [ * ]
71    #hd #tl #H @H
72  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
73  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
74    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
75    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
76  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
77  ]
78| -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
79  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
80  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
81  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
82    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
83    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
84  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
85  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
86  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
87  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
88  ]
89| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
90  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
91  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
92  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
93  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
94    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
95  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
96  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
97  ]
98| #r #EX whd @refl
99] qed.
100
101
102(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
103       will be added later (LTL → LIN). *)
104
105definition RTLabs_classify : state → status_class ≝
106λs. match s with
107[ State f _ _ ⇒
108    match next_instruction f with
109    [ St_cond _ _ _ ⇒ cl_jump
110(*    | St_jumptable _ _ ⇒ cl_jump*)
111    | _ ⇒ cl_other
112    ]
113| Callstate _ _ _ _ _ _ ⇒ cl_call
114| Returnstate _ _ _ _ ⇒ cl_return
115| Finalstate _ ⇒ cl_other
116].
117
118(* As with is_cost_label/cost_label_of we define a boolean function as well
119   as one which extracts the cost label so that we can use it in hypotheses
120   without naming the cost label. *)
121
122definition RTLabs_cost : state → bool ≝
123λs. match s with
124[ State f fs m ⇒
125    is_cost_label (next_instruction f)
126| _ ⇒ false
127].
128
129definition RTLabs_cost_label : state → option costlabel ≝
130λs. match s with
131[ State f fs m ⇒
132    cost_label_of (next_instruction f)
133| _ ⇒ None ?
134].
135
136(* "Program counters" need to identify the current state, either as a pair of
137   the function and current instruction, or the function being entered or
138   left.  Functions are identified by their function pointer block because
139   this avoids introducing functions to map back pointers to function ids using
140   the global environment.  (See the comment at the start of this file, too.)
141   
142   Calls also get the caller's instruction label (or None for the initial call)
143   so that we can distinguish different calls.  This is used only for the
144   t.*_unrepeating property, which includes the pc for call states.
145    *)
146
147inductive RTLabs_pc : Type[0] ≝
148| rapc_state : block → label → RTLabs_pc
149| rapc_call : option label → block → RTLabs_pc
150| rapc_ret : option block → RTLabs_pc
151| rapc_fin : RTLabs_pc
152.
153
154definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
155λx,y. match x with
156[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
157| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
158    eqb ? o1 o2
159    ∧ eq_block b1 b2
160  | _ ⇒ false ]
161| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
162| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
163].
164
165definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
166whd in match RTLabs_pc_eq;
167* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
168* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
169normalize nodelta
170[ @eq_block_elim [ #E destruct | * #NE ] ]
171[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
172[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
173[ @eq_block_elim [ #E destruct | * #NE ] ]
174normalize % #E destruct try (cases (NE (refl ??))) @refl
175qed.
176
177definition RTLabs_ext_state_to_pc : ∀ge. RTLabs_ext_state ge → RTLabs_deqset ≝
178λge,s. match s with [ mk_RTLabs_ext_state s' stk mtc0 ⇒
179match s' return λs'. Ras_Fn_Match ? s' ? → ? with
180[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
181| Callstate _ _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
182| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
183| Finalstate _ ⇒ λmtc. rapc_fin
184] mtc0 ].
185whd in mtc; cases mtc
186qed.
187
188definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
189λge,pc.
190match pc with
191[ rapc_state b l ⇒
192  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
193    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
194| _ ⇒ None ?
195].
196
197(* After returning from a function, we should be ready to execute the next
198   instruction of the caller and the shadow stack should be preserved (we have
199   to take the top element off because the Callstate includes the callee); *or*
200   we're in the final state.
201 *)
202
203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝
204λge,s,s'.
205  match s with
206  [ mk_Sig s p ⇒
207    match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
208    [ Callstate _ fd args dst stk m ⇒
209      λ_. match s' with
210      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
211          next h = next f ∧
212          f_graph (func h) = f_graph (func f) ∧
213          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
214      | Finalstate r ⇒ stk = [ ]
215      | _ ⇒ False
216      ]
217   | State f fs m ⇒ λH.⊥
218   | _ ⇒ λH.⊥
219   ] p
220 ].
221[ whd in H:(??(??%)?);
222  cases (next_instruction f) in H;
223  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
224| normalize in H; destruct
225| normalize in H; destruct
226] qed.
227
228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
229λge,s.
230  match s with
231  [ mk_Sig s p ⇒
232    match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
234      match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
235      [ Callstate _ fd _ _ _ _ ⇒
236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
237        [ nil ⇒ λmtc. ⊥
238        | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
239        ]
240      | State f _ _ ⇒ λ_. λH.⊥
241      | _ ⇒ λ_. λH.⊥
242      ] mtc0
243    ] p
244  ].
245[ whd in H:(??(??%)?);
246  cases (next_instruction f) in H;
247  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
248| 4,5: normalize in H; destruct (H)
249| cases mtc
250| cases mtc #FFP #_ >FFP % #E destruct (E)
251] qed.
252
253lemma RTLabs_notail : ∀s.
254  RTLabs_classify s = cl_tailcall →
255  False.
256* [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ]
257normalize
258#a try #b try #c try #d try #e try #g try #h try #i try #j destruct
259qed.
260
261(* Roughly corresponding to as_classifier *)
262lemma RTLabs_notail' : ∀s.
263  Some ? (RTLabs_classify s) = Some ? cl_tailcall →
264  False.
265#s #E @(RTLabs_notail … s)
266generalize in match (RTLabs_classify s) in E ⊢ %;
267#c #E' destruct %
268qed.
269
270definition RTLabs_status : genv → abstract_status ≝
271λge.
272  mk_abstract_status
273    (RTLabs_ext_state ge)
274    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
275    RTLabs_deqset
276    (RTLabs_ext_state_to_pc ge)
277    (λs. Some ? (RTLabs_classify s))
278    (RTLabs_pc_to_cost_label ge)
279    (RTLabs_after_return ge)
280    (λs. RTLabs_is_final s ≠ None ?)
281    (RTLabs_call_ident ge)
282    (λs. ⊥).
283(* No tailcalls here for now. *)
284cases s @RTLabs_notail'
285qed.
286
287(* Allow us to move between the different notions of when a state is cost
288   labelled. *)
289
290lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
291  RTLabs_cost s = true ↔
292  as_costed (RTLabs_status ge) s.
293cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
294#ge * *
295[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
296  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
297  whd in match (as_pc_of ??);
298  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
299  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
300  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
301  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
302  % cases (lookup_present ?? (f_graph func) ??) normalize
303  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
304  try (% #E' destruct)
305  cases (NONE ?) assumption
306| #vf #fd #args #dst #fs #m #stk #mtc %
307  [ #E normalize in E; destruct
308  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
309    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
310    #H cases (NONE H)
311  ]
312| #v #dst #fs #m #stk #mtc %
313  [ #E normalize in E; destruct
314  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
315    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
316    #H cases (NONE H)
317  ]
318| #r #stk #mtc %
319  [ #E normalize in E; destruct
320  | #E normalize in E; cases (NONE E)
321  ]
322] qed.
323
324lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
325  RTLabs_cost s = false →
326  ¬ as_costed (RTLabs_status ge) s.
327#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
328qed.
Note: See TracBrowser for help on using the repository browser.