source: src/joint/semantics.ma @ 1382

Last change on this file since 1382 was 1382, checked in by sacerdot, 8 years ago
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
File size: 16.4 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint.ma".
6include "joint/BEMem.ma".
7
8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
13record more_sem_params (p:params_): Type[1] ≝
14 { framesT: Type[0]
15 ; regsT: Type[0]
16
17 ; succ_pc: succ p → address → res address
18 ; greg_store_: generic_reg p → beval → regsT → res regsT
19 ; greg_retrieve_: regsT → generic_reg p → res beval
20 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
21 ; acca_retrieve_: regsT → acc_a_reg p → res beval
22 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
23 ; accb_retrieve_: regsT → acc_b_reg p → res beval
24 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
25 ; dpl_retrieve_: regsT → dpl_reg p → res beval
26 ; dph_store_: dph_reg p → beval → regsT → res regsT
27 ; dph_retrieve_: regsT → dph_reg p → res beval
28 ; pair_reg_move_: regsT → pair_reg p → res regsT
29 
30 ; pointer_of_label: label → Σp:pointer. ptype p = Code
31 }.
32
33record sem_params: Type[1] ≝
34 { spp :> params_
35 ; more_sem_pars :> more_sem_params spp
36 }.
37
38record state (p: sem_params): Type[0] ≝
39 { st_frms: framesT ? p
40 ; pc: address
41 ; sp: pointer
42 ; carry: beval
43 ; regs: regsT ? p
44 ; m: bemem
45 }.
46
47record more_sem_params1 (succT: Type[0]) (p:params1): Type[1] ≝
48 { more_sparams :> more_sem_params (mk_params_ p succT)
49
50 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
51 ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
52   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
53     type of arguments. To be fixed using a dependent type *)
54 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
55 }.
56
57record sem_params1: Type[1] ≝
58 { spp1 :> params1
59 ; ssucc_ : Type[0]
60 ; more_sem_params1 :> more_sem_params1 ssucc_ spp1
61 }.
62
63definition sem_params_of_sem_params1 ≝ λsp1: sem_params1. mk_sem_params … sp1.
64coercion sem_params_of_sem_params1 : ∀_x:sem_params1. sem_params
65 ≝ sem_params_of_sem_params1 on _x: sem_params1 to sem_params.
66
67definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
68
69record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
70 { more_sparams1 :> more_sem_params1 (succ p) p
71
72 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
73 ; fetch_result: state (mk_sem_params … more_sparams1) → res (list beval)
74
75 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
76 ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
77
78 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
79 }.
80
81record sem_params2 (globals: list ident): Type[1] ≝
82 { p2:> params globals
83 ; more_sparams2:> more_sem_params2 globals p2
84 }.
85
86definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
87coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
88 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
89(*
90unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
91   S ≟ sem_params_of_sem_params2 globals p
92(* ---------------------------------------- *) ⊢
93   pars_ (spp (mk_sem_params (p2 globals p)
94    (more_sparams (p2 globals p) globals
95    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
96*)
97definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 sp2 (succ sp2) sp2.
98coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1
99 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1.
100
101definition address_of_label: sem_params → label → address.
102 #p #l generalize in match (refl … (address_of_pointer (pointer_of_label … p l)))
103 cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
104  [ #res #_ @res
105  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 try destruct
106    normalize in E2; destruct ]
107qed.
108
109definition set_m: ∀p. bemem → state p → state p ≝
110 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
111
112definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
113 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
114
115definition set_sp: ∀p. pointer → state p → state p ≝
116 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
117
118definition set_carry: ∀p. beval → state p → state p ≝
119 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
120
121definition set_pc: ∀p. address → state p → state p ≝
122 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
123
124definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
125 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
126
127definition goto: ∀p:sem_params. label → state p → state p ≝
128 λp,l,st. set_pc … (address_of_label p l) st.
129
130definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
131 λp,l,st.
132  do l' ← succ_pc … (more_sem_pars p) l (pc … st) ;
133  OK … (set_pc … l' st).
134
135definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
136 λp,dst,v,st.
137  do regs  ← greg_store_ … dst v (regs … st);
138  OK ? (set_regs … regs st).
139
140definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
141 λp,st,dst.greg_retrieve_ … (regs … st) dst.
142
143definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
144 λp,dst,v,st.
145  do regs ← acca_store_ … dst v (regs … st);
146  OK ? (set_regs … regs st).
147
148definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
149 λp,st,dst.acca_retrieve_ … (regs … st) dst.
150
151definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
152 λp,dst,v,st.
153  do regs ← accb_store_ … dst v (regs … st);
154  OK ? (set_regs … regs st).
155
156definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
157 λp,st,dst.accb_retrieve_ … (regs … st) dst.
158
159definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
160 λp,dst,v,st.
161  do regs ← dpl_store_ … dst v (regs … st);
162  OK ? (set_regs … regs st).
163
164definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
165 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
166
167definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
168 λp,dst,v,st.
169  do regs ← dph_store_ … dst v (regs … st);
170  OK ? (set_regs … regs st).
171
172definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
173 λp,st,dst.dph_retrieve_ … (regs … st) dst.
174
175definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
176 λp,st,rs.
177  do regs ← pair_reg_move_ … (regs … st) rs;
178  OK … (set_regs … regs st).
179
180axiom FailedStore: String.
181
182definition push: ∀p. state p → beval → res (state p) ≝
183 λp,st,v.
184  let sp ≝ sp … st in
185  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
186  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
187  OK … (set_m … m (set_sp … sp st)).
188
189definition pop: ∀p. state p → res (state p × beval) ≝
190 λp,st.
191  let sp ≝ sp ? st in
192  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
193  let st ≝ set_sp … sp st in
194  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
195  OK ? 〈st,v〉.
196
197definition save_ra : ∀p. state p → address → res (state p) ≝
198 λp,st,l.
199  let 〈addrl,addrh〉 ≝ l in
200  do st ← push … st addrl;
201  push … st addrh.
202
203definition fetch_ra : ∀p.state p → res (state p × address) ≝
204 λp,st.
205  do 〈st,addrh〉 ← pop … st;
206  do 〈st,addrl〉 ← pop … st;
207  OK ? 〈st, 〈addrl,addrh〉〉.
208
209axiom MissingSymbol : String.
210axiom FailedLoad : String.
211axiom BadFunction : String.
212
213definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
214 λglobals,p,ge,st.
215  ! s ← fetch_statement … ge st;
216  match s with
217    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
218    | sequential seq l ⇒
219      match seq with
220      [ extension c ⇒ exec_extended … p ge c l st
221      | COST_LABEL cl ⇒
222         ! st ← next … l st ;
223         ret ? 〈Echarge cl, st〉
224      | COMMENT c ⇒
225         ! st ← next … l st ;
226         ret ? 〈E0, st〉
227      | INT dest v ⇒
228         ! st ← greg_store p dest (BVByte v) st;
229         ! st ← next … l st ;
230          ret ? 〈E0, st〉
231      | LOAD dst addrl addrh ⇒
232        ! vaddrh ← dph_retrieve … st addrh;
233        ! vaddrl ← dpl_retrieve … st addrl;
234        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
235        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
236        ! st ← acca_store p … dst v st;
237        ! st ← next … l st ;
238          ret ? 〈E0, st〉
239      | STORE addrl addrh src ⇒
240        ! vaddrh ← dph_retrieve … st addrh;
241        ! vaddrl ← dpl_retrieve … st addrl;
242        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
243        ! v ← acca_retrieve … st src;
244        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
245        let st ≝ set_m … m' st in
246        ! st ← next … l st ;
247          ret ? 〈E0, st〉
248      | COND src ltrue ⇒
249        ! v ← acca_retrieve … st src;
250        ! b ← bool_of_beval v;
251        if b then
252         ret ? 〈E0, goto … ltrue st〉
253        else
254         ! st ← next … l st ;
255         ret ? 〈E0, st〉
256      | ADDRESS ident prf ldest hdest ⇒
257        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
258        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
259        ! st ← dpl_store p ldest laddr st;
260        ! st ← dph_store p hdest haddr st;
261        ! st ← next … l st ;
262          ret ? 〈E0, st〉
263      | OP1 op dacc_a sacc_a ⇒
264        ! v ← acca_retrieve … st sacc_a;
265        ! v ← Byte_of_val v;
266          let v' ≝ BVByte (op1 eval op v) in
267        ! st ← acca_store p dacc_a v' st;
268        ! st ← next … l st ;
269          ret ? 〈E0, st〉
270      | OP2 op dacc_a sacc_a src ⇒
271        ! v1 ← acca_retrieve … st sacc_a;
272        ! v1 ← Byte_of_val v1;
273        ! v2 ← greg_retrieve … st src;
274        ! v2 ← Byte_of_val v2;
275        ! carry ← bool_of_beval (carry … st);
276          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
277          let v' ≝ BVByte v' in
278          let carry ≝ beval_of_bool carry in
279        ! st ← acca_store p dacc_a v' st;
280          let st ≝ set_carry … carry st in
281        ! st ← next … l st ;
282          ret ? 〈E0, st〉
283      | CLEAR_CARRY ⇒
284        ! st ← next … l (set_carry … BVfalse st) ;
285         ret ? 〈E0, st〉
286      | SET_CARRY ⇒
287        ! st ← next … l (set_carry … BVtrue st) ;
288         ret ? 〈E0, st〉
289      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
290        ! v1 ← acca_retrieve … st sacc_a_reg;
291        ! v1 ← Byte_of_val v1;
292        ! v2 ← accb_retrieve … st sacc_b_reg;
293        ! v2 ← Byte_of_val v2;
294          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
295          let v1' ≝ BVByte v1' in
296          let v2' ≝ BVByte v2' in
297        ! st ← acca_store p dacc_a_reg v1' st;
298        ! st ← accb_store p dacc_b_reg v2' st;
299        ! st ← next … l st ;
300          ret ? 〈E0, st〉
301      | POP dst ⇒
302        ! 〈st,v〉 ← pop … st;
303        ! st ← acca_store p dst v st;
304        ! st ← next … l st ;
305          ret ? 〈E0, st〉
306      | PUSH src ⇒
307        ! v ← acca_retrieve … st src;
308        ! st ← push … st v;
309        ! st ← next … l st ;
310          ret ? 〈E0, st〉
311      | MOVE dst_src ⇒
312        ! st ← pair_reg_move … st dst_src ;
313        ! st ← next … l st ;
314          ret ? 〈E0, st〉
315      | CALL_ID id args dest ⇒
316        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
317        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
318          match fd with
319          [ Internal fn ⇒
320            ! l ← succ_pc … (more_sem_pars p) l (pc … st) ;
321            ! st ← save_frame … l (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
322            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
323            let l' ≝ joint_if_entry … fn in
324             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
325          | External fn ⇒
326            ! params ← fetch_external_args … fn st;
327            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
328            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
329            (* CSC: XXX bug here; I think I should split it into Byte-long
330               components; instead I am making a singleton out of it *)
331              let vs ≝ [mk_val ? evres] in
332            ! st ← set_result … vs st;
333            ! st ← next … l st ;
334              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
335          ]]
336    | RETURN ⇒
337      ! 〈st,ra〉 ← pop_frame … st;
338        ret ? 〈E0,set_pc … ra st〉].
339cases addr //
340qed.
341
342definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
343 λglobals,p,ge,exit,st.res_to_opt ? (
344  do s ← fetch_statement … ge st;
345  match s with
346   [ RETURN ⇒
347      do 〈st,l〉 ← fetch_ra … st;
348      if eq_address l exit then
349       do vals ← fetch_result … st ;
350       Word_of_list_beval vals
351      else
352       Error ? []
353   | _ ⇒ Error ? []]).
354
355record evaluation_parameters : Type[1] ≝
356 { globals: list ident
357 ; sparams2: sem_params2 globals
358 ; exit: address
359 ; genv2: genv globals sparams2
360 }.
361
362definition joint_exec: trans_system io_out io_in ≝
363  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
364   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
365   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
366
367definition make_global :
368 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
369  joint_program pars → evaluation_parameters
370
371 λpars,sparams.
372  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ? (globalenv Genv … (λx.[Init_space x]) p)).
373cases daemon (*CSC: XXXXXXXXXXXXX*)
374qed.
375
376definition make_initial_state :
377 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
378 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
379λpars,sparams,p.
380  let ge ≝ genv2 (make_global pars sparams p) in
381  do m ← init_mem Genv … (λx.[Init_space x]) p;
382  let main ≝ prog_main … p in
383  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
384  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
385  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
386cases daemon qed.
387(*
388RTL:
389 init_prog == init_mem
390 init_sp: inizializzare lo stack pointer
391 init_isp: inizializzare l'altro stack pointer
392 init_renv: inizializzare i registri fisici
393 init_main_call: chiamata di funzione
394   --- init_fun_call: cambia fra ERTL e LTL
395 change_carry: a 0
396*)
397
398definition joint_fullexec :
399 ∀pars:∀globals.params globals.
400 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
401 fullexec io_out io_in ≝
402 λpars,sparams.
403  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.