source: src/joint/semantics.ma @ 2176

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

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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