source: src/joint/semantics.ma @ 1395

Last change on this file since 1395 was 1395, checked in by sacerdot, 9 years ago

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

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