source: src/joint/semantics.ma @ 1383

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

Potential bug fixed and bug found: the way pointers and labels are put in
bijection must be different between LIN and graph-like languages (bug fixed).
Moreover, in both cases it must be possible to retrieve the function from the
address and the easiest (only?) way to do that is to use the block of the
address to store the block of the function, and put the offsets in bijection
with labels/offsets, preventing pointer mangling since the pointer is in
the Code region (found, to be fixed).

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