source: src/joint/Traces.ma @ 3362

Last change on this file since 3362 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 8.1 KB
Line 
1include "joint/semanticsUtils.ma".
2include "common/StructuredTraces.ma".
3
4record evaluation_params (p : sem_params) : Type[0] ≝
5{ globals : list ident
6; ev_genv :> genv p globals
7}.
8
9record prog_params : Type[1] ≝
10 { prog_spars :> sem_params
11 ; prog : joint_program prog_spars
12 ; stack_sizes : ident → option ℕ
13(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
14 }.
15
16definition joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝
17λp.mk_evaluation_params ?
18  (prog_names … (prog p))
19  (joint_globalenv p (prog p) (stack_sizes p)).
20
21coercion joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝
22joint_make_global on p : prog_params to evaluation_params ?.
23
24definition make_initial_state :
25 ∀pars: prog_params.res (state_pc pars) ≝
26λpars.let p ≝ prog pars in
27  let ge ≝ ev_genv pars in
28  (* this is going to change shortly: globals will not reside in globalenv anymore *)
29  ! m0 ← init_mem … (λx.x) p ;
30  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
31  let globals_size ≝ globals_stacksize … p in
32  (* stack pointer should start at 2^16 - |globals|, right?
33     first call to main shuold bring it to 2^16 - |globals| - |main stack|
34     Also, on words 2^16 - |globals| = - |globals| *)
35  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
36  let spp : xpointer ≝
37    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
38     pi2 … spb» in
39(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
40  let main ≝ prog_main … p in
41  let st ≝ mk_state pars
42    (* frames ≝ *)(Some ? (empty_framesT …))
43    (* internal_stack ≝ *) empty_is
44    (* carry ≝ *)(BBbit false)
45    (* regs ≝ *)(empty_regsT … spp)
46    (* mem ≝ *)m
47    (* stack_usage ≝ *)0 in
48  return
49  mk_state_pc ?
50    (* state_no_pc ≝ *)(set_sp … spp st)
51    (* pc ≝ *)init_pc
52    (* last_pop ≝ *)(null_pc one).
53@hide_prf
54cases m0 in H; #m1 #m2 #m3 #H
55whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
56@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/
57qed.
58
59definition joint_classify_step :
60  ∀p,globals.joint_step p globals → status_class ≝
61  λp,g,stmt.
62  match stmt with
63  [ CALL f args dest ⇒ cl_call
64  | COND _ _ ⇒ cl_jump
65  | _ ⇒ cl_other
66  ].
67
68definition joint_classify_final :
69  ∀p.joint_fin_step p → status_class ≝
70  λp,stmt.
71  match stmt with
72  [ GOTO _ ⇒ cl_other
73  | RETURN ⇒ cl_return
74  | TAILCALL _ f args ⇒ cl_tailcall
75  ].
76
77definition joint_classify :
78  ∀p.∀pars : evaluation_params p.state_pc p → status_class ≝
79  λp,pars,st.
80  match fetch_statement … (ev_genv … pars) (pc … st) with
81  [ OK i_fn_s ⇒
82    match \snd i_fn_s with
83    [ sequential s _ ⇒ joint_classify_step … s
84    | final s ⇒ joint_classify_final … s
85    | FCOND _ _ _ _ ⇒ cl_jump
86    ]
87  | _ ⇒ cl_other
88  ].
89
90lemma joint_classify_call : ∀p,pars,st.
91  joint_classify p pars st = cl_call →
92  ∃i_f,f',args,dest,next.
93  fetch_statement … (ev_genv … pars) (pc … st) =
94    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
95#p #pars #st
96whd in match joint_classify; normalize nodelta
97inversion (fetch_statement ????)
98[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
99* #i_f *
100[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
101  normalize nodelta normalize in ⊢ (%→?); #ABS destruct
102]
103* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta
104normalize in ⊢ (%→?); #EQ destruct
105%[|%[|%[|%[|%[| %]]]]]
106qed.
107
108definition joint_after_ret : ∀p : sem_params.∀pars.
109  (Σs : state_pc p.joint_classify p pars s = cl_call) → state_pc p → Prop ≝
110λp,pars,s1,s2.
111match fetch_statement … (ev_genv … pars) (pc … s1) with
112[ OK x ⇒
113  match \snd x with
114  [ sequential s next ⇒
115    last_pop … s2 = pc … s1 ∧
116    pc … s2 = succ_pc p (pc … s1) next
117  | _ ⇒ False (* never happens *)
118  ]
119| _ ⇒ False (* never happens *)
120].
121
122definition joint_call_ident : ∀p : sem_params.∀pars.
123  state_pc p → ident ≝
124(* this is a definition without a dummy ident :
125λp,st.
126match ?
127return λx.
128  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
129  match s with
130  [ sequential s next ⇒
131    match s with
132    [ CALL f' args dest ⇒ function_of_call … (ev_genv p) st f'
133    | _ ⇒ Error … [ ]
134    ]
135  | _ ⇒ Error … [ ]
136  ] = x → ? with
137[ OK v ⇒ λ_.v
138| Error e ⇒ λABS.⊥
139] (refl …).
140@hide_prf
141elim (joint_classify_call … (pi2 … st))
142#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
143lapply ABS -ABS
144>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
145qed. *)
146(* with a dummy ident (which is never used as seen above in the commented script)
147   I think handling of the function is easier *)
148λp,pars,st.
149let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
150match fetch_statement … (ev_genv … pars) (pc … st) with
151[ OK x ⇒
152  match \snd x with
153  [ sequential s next ⇒
154    match s with
155    [ CALL f' args dest ⇒
156      match
157        (! bl ← block_of_call … (ev_genv … pars) f' st;
158         fetch_internal_function … (ev_genv … pars) bl) with
159      [ OK i_f ⇒ \fst i_f
160      | _ ⇒ dummy
161      ]
162    | _ ⇒ dummy
163    ]
164  | _ ⇒ dummy
165  ]
166| _ ⇒ dummy
167].
168
169definition joint_tailcall_ident : ∀p:sem_params.∀pars.
170  state_pc p → ident ≝
171λp,pars,st.
172let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
173match fetch_statement … (ev_genv … pars) (pc … st) with
174[ OK x ⇒
175  match \snd x with
176  [ final s ⇒
177    match s with
178    [ TAILCALL _ f' args ⇒
179      match
180        (! bl ← block_of_call … (ev_genv … pars) f' st;
181         fetch_internal_function … (ev_genv … pars) bl) with
182      [ OK i_f ⇒ \fst i_f
183      | _ ⇒ dummy
184      ]
185    | _ ⇒ dummy
186    ]
187  | _ ⇒ dummy
188  ]
189| _ ⇒ dummy
190].
191
192definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
193*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
194[ #EQ destruct % #H %
195| * #NEQ % #ABS destruct elim (NEQ ?) %
196]
197qed.
198
199(*
200let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
201  match c with
202  [ Value x ⇒ OK … x
203  | Interact o f ⇒
204    ! i ← env o ;
205    io_evaluate O I X env (f i)
206  | Wrong e ⇒ Error … e
207  ].
208*)
209
210definition cost_label_of_stmt :
211  ∀p,globals.joint_statement p globals → option costlabel ≝
212  λp,g,s.match s with
213  [ sequential s _ ⇒
214    match s with
215    [  COST_LABEL lbl ⇒ Some ? lbl
216    | _ ⇒ None ?
217    ]
218  | _ ⇒ None ?
219  ].
220
221definition joint_label_of_pc ≝
222  λp,pars.
223    (λpc.
224      match fetch_statement … (ev_genv p pars) pc with
225      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
226      | _ ⇒ None ?
227      ]).
228
229(* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *)
230definition exit_pc' : program_counter ≝
231mk_program_counter «mk_block (-1), refl …» (p1 one).
232
233definition joint_final: ∀p: sem_params.∀pars.
234  state_pc p → option int ≝
235 λp,pars,st.
236 let ge ≝ ev_genv p pars in
237 if eq_program_counter (pc … st) exit_pc' then
238   let ret ≝ call_dest_for_main ?? p in
239   match (! vals ← read_result … ge ret st ;
240               Word_of_list_beval vals)
241   with
242   [ OK v ⇒ Some ? v
243   | Error _ ⇒ Some … (maximum ?) ]
244 else None ?.
245
246definition joint_abstract_status :
247 ∀p : prog_params.
248 abstract_status ≝
249 λp.
250 mk_abstract_status
251   (* as_status ≝ *) (state_pc p)
252   (* as_execute ≝ *)
253    (λs1,s2.eval_state … (ev_genv … p) s1 = return s2)
254   (* (* as_init ≝ *) (make_initial_state p) *)
255   (* as_pc ≝ *) pcDeq
256   (* as_pc_of ≝ *) (pc …)
257   (* as_classify ≝ *) (joint_classify … p)
258   (* as_label_of_pc ≝ *) (joint_label_of_pc … p)
259   (* as_after_return ≝ *) (joint_after_ret … p)
260   (* as_result ≝ *) (joint_final … p)
261   (* as_call_ident ≝ *) (λst.joint_call_ident … p st)
262   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident … p st).
263
264(* alternative definition with integrated prog_params constructor *)
265definition joint_status :
266 ∀p : sem_params.
267 joint_program p → (ident → option ℕ) → abstract_status ≝
268λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes).
Note: See TracBrowser for help on using the repository browser.