source: src/RTLabs/RTLabs_abstract.ma

Last change on this file was 3031, checked in by campbell, 7 years ago

Tidy up RTLabs preclassified_system definitions.

File size: 16.0 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_extra.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 fid fd _ _ fs _ ⇒
38      match fn_stack with
39      [ nil ⇒ False
40      | cons h t ⇒
41          find_symbol … ge fid = Some ? h ∧
42          find_funct_ptr ? ge h = Some ? fd ∧
43          All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
44      ]
45  | Returnstate _ _ fs _ ⇒
46      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
47  | Finalstate _ ⇒ fn_stack = [ ]
48  ].
49
50record RTLabs_ext_state (ge:genv) : Type[0] ≝ {
51  Ras_state :> state;
52  Ras_fn_stack : list block;
53  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
54}.
55
56(* Given a plain step of the RTLabs semantics, give the next state along with
57   the shadow stack of function block numbers.  Carefully defined so that the
58   coercion back to the plain state always reduces. *)
59definition next_state : ∀ge. ∀s:RTLabs_ext_state ge. ∀s':state. ∀t.
60  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
61λge,s,s',t,EX. mk_RTLabs_ext_state ge s'
62 (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)
63 ?.
64cases s' in EX ⊢ %;
65[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
66  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
67    whd cases stk in mtc ⊢ %; [ * ]
68    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
69    | @M2 ]
70  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
71  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
72    whd cases stk in mtc ⊢ %; [ * ]
73    #hd #tl * * /3/
74  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
75  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
76    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
77    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
78  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
79  ]
80| -s' #fid #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
81  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
82  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
83  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
84    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
85    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
86  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
87  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
88  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
89  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
90  ]
91| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
92  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
93  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
94  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
95  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
96    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
97  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
98  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
99  ]
100| #r #EX whd @refl
101] qed.
102
103
104(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
105       will be added later (LTL → LIN). *)
106
107definition RTLabs_classify : state → status_class ≝
108λs. match s with
109[ State f _ _ ⇒
110    match next_instruction f with
111    [ St_cond _ _ _ ⇒ cl_jump
112(*    | St_jumptable _ _ ⇒ cl_jump*)
113    | _ ⇒ cl_other
114    ]
115| Callstate _ _ _ _ _ _ ⇒ cl_call
116| Returnstate _ _ _ _ ⇒ cl_return
117| Finalstate _ ⇒ cl_other
118].
119
120(* As with is_cost_label/cost_label_of we define a boolean function as well
121   as one which extracts the cost label so that we can use it in hypotheses
122   without naming the cost label. *)
123
124definition RTLabs_cost : state → bool ≝
125λs. match s with
126[ State f fs m ⇒
127    is_cost_label (next_instruction f)
128| _ ⇒ false
129].
130
131definition RTLabs_cost_label : state → option costlabel ≝
132λs. match s with
133[ State f fs m ⇒
134    cost_label_of (next_instruction f)
135| _ ⇒ None ?
136].
137
138(* "Program counters" need to identify the current state, either as a pair of
139   the function and current instruction, or the function being entered or
140   left.  Functions are identified by their function pointer block because
141   this avoids introducing functions to map back pointers to function ids using
142   the global environment.  (See the comment at the start of this file, too.)
143   
144   Calls also get the caller's instruction label (or None for the initial call)
145   so that we can distinguish different calls.  This is used only for the
146   t.*_unrepeating property, which includes the pc for call states.
147    *)
148
149inductive RTLabs_pc : Type[0] ≝
150| rapc_state : block → label → RTLabs_pc
151| rapc_call : option label → block → RTLabs_pc
152| rapc_ret : option block → RTLabs_pc
153| rapc_fin : RTLabs_pc
154.
155
156definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
157λx,y. match x with
158[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
159| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
160    eqb ? o1 o2
161    ∧ eq_block b1 b2
162  | _ ⇒ false ]
163| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
164| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
165].
166
167definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
168whd in match RTLabs_pc_eq;
169* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
170* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
171normalize nodelta
172[ @eq_block_elim [ #E destruct | * #NE ] ]
173[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
174[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
175[ @eq_block_elim [ #E destruct | * #NE ] ]
176normalize % #E destruct try (cases (NE (refl ??))) @refl
177qed.
178
179definition RTLabs_ext_state_to_pc : ∀ge. RTLabs_ext_state ge → RTLabs_deqset ≝
180λge,s. match s with [ mk_RTLabs_ext_state s' stk mtc0 ⇒
181match s' return λs'. Ras_Fn_Match ? s' ? → ? with
182[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
183| 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 ]
184| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
185| Finalstate _ ⇒ λmtc. rapc_fin
186] mtc0 ].
187whd in mtc; cases mtc
188qed.
189
190definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
191λge,pc.
192match pc with
193[ rapc_state b l ⇒
194  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
195    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
196| _ ⇒ None ?
197].
198
199(* After returning from a function, we should be ready to execute the next
200   instruction of the caller and the shadow stack should be preserved (we have
201   to take the top element off because the Callstate includes the callee); *or*
202   we're in the final state.
203 *)
204
205definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
206λge,s,s'.
207  match s with
208  [ mk_Sig s p ⇒
209    match s return λs. RTLabs_classify s = cl_call → ? with
210    [ Callstate _ fd args dst stk m ⇒
211      λ_. match s' with
212      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
213          next h = next f ∧
214          f_graph (func h) = f_graph (func f) ∧
215          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
216      | Finalstate r ⇒ stk = [ ]
217      | _ ⇒ False
218      ]
219   | State f fs m ⇒ λH.⊥
220   | _ ⇒ λH.⊥
221   ] p
222 ].
223[ whd in H:(??%?);
224  cases (next_instruction f) in H;
225  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
226| normalize in H; destruct
227| normalize in H; destruct
228] qed.
229
230definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → ident ≝
231λge,s.
232  match s with
233  [ mk_Sig s p ⇒
234    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
235    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
236      match s' return λs'. RTLabs_classify s' = cl_call → ident with
237      [ Callstate fid _ _ _ _ _ ⇒ λ_. fid
238      | State f _ _ ⇒ λH.⊥
239      | _ ⇒ λH.⊥
240      ]
241    ] p
242  ].
243[ whd in H:(??%?);
244  cases (next_instruction f) in H;
245  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
246| *: normalize in H; destruct (H)
247] qed.
248
249lemma RTLabs_notail : ∀s.
250  RTLabs_classify s = cl_tailcall →
251  False.
252* [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ]
253normalize
254#a try #b try #c try #d try #e try #g try #h try #i try #j destruct
255qed.
256
257(* Roughly corresponding to as_classifier *)
258lemma RTLabs_notail' : ∀s.
259  RTLabs_classify s = cl_tailcall →
260  False.
261#s #E @(RTLabs_notail … s)
262generalize in match (RTLabs_classify s) in E ⊢ %;
263#c #E' destruct %
264qed.
265
266definition RTLabs_status : genv → abstract_status ≝
267λge.
268  mk_abstract_status
269    (RTLabs_ext_state ge)
270    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
271    RTLabs_deqset
272    (RTLabs_ext_state_to_pc ge)
273    (RTLabs_classify)
274    (RTLabs_pc_to_cost_label ge)
275    (RTLabs_after_return ge)
276    (RTLabs_is_final)
277    (RTLabs_call_ident ge)
278    (λs. ⊥).
279(* No tailcalls here for now. *)
280cases s @RTLabs_notail'
281qed.
282
283(* Allow us to move between the different notions of when a state is cost
284   labelled. *)
285
286lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
287  RTLabs_cost s = true ↔
288  as_costed (RTLabs_status ge) s.
289cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
290#ge * *
291[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
292  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
293  whd in match (as_pc_of ??);
294  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
295  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
296  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
297  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
298  % cases (lookup_present ?? (f_graph func) ??) normalize
299  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
300  try (% #E' destruct)
301  cases (NONE ?) assumption
302| #vf #fd #args #dst #fs #m #stk #mtc %
303  [ #E normalize in E; destruct
304  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
305    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
306    #H cases (NONE H)
307  ]
308| #v #dst #fs #m #stk #mtc %
309  [ #E normalize in E; destruct
310  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
311    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
312    #H cases (NONE H)
313  ]
314| #r #stk #mtc %
315  [ #E normalize in E; destruct
316  | #E normalize in E; cases (NONE E)
317  ]
318] qed.
319
320lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
321  RTLabs_cost s = false →
322  ¬ as_costed (RTLabs_status ge) s.
323#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
324qed.
325
326(* Build a fullexec for the extended semantics, so that we can go on to make
327   a preclassified system later. *)
328
329
330definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
331λge,s.
332match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with
333[ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉
334| Wrong m ⇒ λ_. Wrong ??? m
335| Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO)
336] (next_state ge s).
337//
338qed.
339
340lemma drop_exec_ext : ∀ge,s,tr,s'.
341  eval_ext_statement ge s = return 〈tr,s'〉 →
342  eval_statement ge s = return 〈tr,Ras_state … s'〉.
343#ge #s #tr #s'
344whd in ⊢ (??%? → ?);
345letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
346cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
347[ // ]
348generalize in match f; -f
349cases (eval_statement ge s)
350[ #o #k #n #N #E whd in E:(??%%); destruct
351| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
352| #m #n #N #E whd in E:(??%%); destruct
353] qed.
354
355lemma as_eval_ext_statement : ∀ge,s,tr,s'.
356  eval_ext_statement ge s = Value … 〈tr,s'〉 →
357  as_execute (RTLabs_status ge) s s'.
358#ge #s #tr #s' #EX
359whd %{tr} %{(drop_exec_ext … EX)}
360whd in EX:(??%?);
361letin ns ≝ (next_state ge s) in EX; #EX
362change with (ns s' tr ?) in match (next_state ge s s' tr ?);
363generalize in match (drop_exec_ext ?????);
364#EX'
365generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
366#E destruct @e1
367qed.
368
369definition RTLabs_ext_exec : trans_system io_out io_in ≝
370  mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement.
371
372definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
373λp.
374  let ge ≝ make_global p in
375  do m ← init_mem … (λx.x) p;
376  let main ≝ prog_main ?? p in
377  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
378  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
379  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
380  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
381% [ % assumption | % ]
382qed.
383
384lemma initial_states_OK : ∀p,s.
385  make_ext_initial_state p = return s →
386  make_initial_state p = return (Ras_state … s).
387#p #s #E
388cases (bind_inversion ????? E) -E #m * #E1 #E
389cases (bind_as_inversion ????? E) -E #b * #Eb #E
390cases (bind_as_inversion ????? E) -E #f * #Ef #E
391whd in ⊢ (??%?); >E1
392whd in ⊢ (??%?); >Eb
393whd in ⊢ (??%?); >Ef
394whd in E:(??%%) ⊢ (??%?); destruct
395%
396qed.
397
398lemma initial_states_OK' : ∀p,s.
399  make_initial_state p = return s →
400  ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M).
401#p #s #E
402cases (bind_inversion ????? E) -E #m * #E1 #E
403cases (bind_inversion ????? E) -E #b * #Eb #E
404cases (bind_inversion ????? E) -E #f * #Ef #E
405whd in E:(??%%); destruct
406%{[b]} % [ % [ % assumption | % ] ]
407whd in ⊢ (??%?); >E1
408whd in ⊢ (??%?); generalize in match (refl ??);
409>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
410whd in ⊢ (??%?); generalize in match (refl ??);
411>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
412qed.
413
414
415definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
416  mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
417
Note: See TracBrowser for help on using the repository browser.