source: src/joint/semantics.ma @ 1419

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