source: src/joint/semantics.ma @ 1408

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