source: src/joint/semantics.ma @ 1352

Last change on this file since 1352 was 1352, checked in by sacerdot, 8 years ago

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File size: 16.2 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 ; succ_pc: succ p → address → address
18 ; greg_store_: generic_reg p → beval → regsT → res regsT
19 ; greg_retrieve_: regsT → generic_reg p → res beval
20 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
21 ; acca_retrieve_: regsT → acc_a_reg p → res beval
22 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
23 ; accb_retrieve_: regsT → acc_b_reg p → res beval
24 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
25 ; dpl_retrieve_: regsT → dpl_reg p → res beval
26 ; dph_store_: dph_reg p → beval → regsT → res regsT
27 ; dph_retrieve_: regsT → dph_reg p → res beval
28 ; pair_reg_move_: regsT → pair_reg p → res regsT
29 
30 ; pointer_of_label: label → Σp:pointer. ptype p = Code
31 }.
32
33record sem_params: Type[1] ≝
34 { spp :> params_
35 ; more_sem_pars :> more_sem_params spp
36 }.
37
38record state (p: sem_params): Type[0] ≝
39 { st_frms: framesT ? p
40 ; pc: address
41 ; sp: pointer
42 ; carry: beval
43 ; regs: regsT ? p
44 ; m: bemem
45 }.
46
47record more_sem_params1 (succT: Type[0]) (p:params1): Type[1] ≝
48 { more_sparams :> more_sem_params (mk_params_ p succT)
49
50   (* Functions that manipulate the st_frms component of the state *)
51 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
52 ; pop_frame: state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
53 ; save_frame: state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
54 }.
55
56record sem_params1: Type[1] ≝
57 { spp1 :> params1
58 ; ssucc_ : Type[0]
59 ; more_sem_params1 :> more_sem_params1 ssucc_ spp1
60 }.
61
62definition sem_params_of_sem_params1 ≝ λsp1: sem_params1. mk_sem_params … sp1.
63coercion sem_params_of_sem_params1 : ∀_x:sem_params1. sem_params
64 ≝ sem_params_of_sem_params1 on _x: sem_params1 to sem_params.
65
66definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
67
68record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
69 { more_sparams1 :> more_sem_params1 (succ p) p
70
71 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
72 ; fetch_result: state (mk_sem_params … more_sparams1) → nat → res val
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(*
89unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
90   S ≟ sem_params_of_sem_params2 globals p
91(* ---------------------------------------- *) ⊢
92   pars_ (spp (mk_sem_params (p2 globals p)
93    (more_sparams (p2 globals p) globals
94    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
95*)
96definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 sp2 (succ sp2) sp2.
97coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1
98 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1.
99
100definition address_of_label: sem_params → label → address.
101 #p #l generalize in match (refl … (address_of_pointer (pointer_of_label … p l)))
102 cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
103  [ #res #_ @res
104  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
105qed.
106
107definition set_m: ∀p. bemem → state p → state p ≝
108 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
109
110definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
111 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
112
113definition set_sp: ∀p. pointer → state p → state p ≝
114 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
115
116definition set_carry: ∀p. beval → state p → state p ≝
117 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
118
119definition set_pc: ∀p. address → state p → state p ≝
120 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
121
122definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
123 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
124
125definition goto: ∀p:sem_params. label → state p → state p ≝
126 λp,l,st. set_pc … (address_of_label p l) st.
127
128definition next: ∀p:sem_params. succ … p → state p → state p ≝
129 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) 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 → succ p → res (state p) ≝
194 λp,st,l.
195  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
196  do st ← push … st addrl;
197  push … st addrh.
198
199definition fetch_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.
208
209definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
210 λglobals,p,ge,st.
211  ! s ← fetch_statement … ge st;
212  match s with
213    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
214    | sequential seq l ⇒
215      match seq with
216      [ extension c ⇒ exec_extended … p ge c l st
217      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
218      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
219      | INT dest v ⇒
220        ! st ← greg_store p dest (BVByte v) st;
221          ret ? 〈E0, next … l st〉
222      | LOAD dst addrl addrh ⇒
223        ! vaddrh ← dph_retrieve … st addrh;
224        ! vaddrl ← dpl_retrieve … st addrl;
225        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
226        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
227        ! st ← acca_store p … dst v st;
228          ret ? 〈E0, next … l st〉
229      | STORE addrl addrh src ⇒
230        ! vaddrh ← dph_retrieve … st addrh;
231        ! vaddrl ← dpl_retrieve … st addrl;
232        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
233        ! v ← acca_retrieve … st src;
234        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
235          ret ? 〈E0, next … l (set_m … m' st)〉
236      | COND src ltrue ⇒
237        ! v ← acca_retrieve … st src;
238        ! b ← bool_of_beval v;
239          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
240      | ADDRESS ident prf ldest hdest ⇒
241        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
242        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
243        ! st ← dpl_store p ldest laddr st;
244        ! st ← dph_store p hdest haddr st;
245          ret ? 〈E0, next … l st〉
246      | OP1 op dacc_a sacc_a ⇒
247        ! v ← acca_retrieve … st sacc_a;
248        ! v ← Byte_of_val v;
249          let v' ≝ BVByte (op1 eval op v) in
250        ! st ← acca_store p dacc_a v' st;
251          ret ? 〈E0, next … l st〉
252      | OP2 op dacc_a sacc_a src ⇒
253        ! v1 ← acca_retrieve … st sacc_a;
254        ! v1 ← Byte_of_val v1;
255        ! v2 ← greg_retrieve … st src;
256        ! v2 ← Byte_of_val v2;
257        ! carry ← bool_of_beval (carry … st);
258          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
259          let v' ≝ BVByte v' in
260          let carry ≝ beval_of_bool carry in
261        ! st ← acca_store p dacc_a v' st;
262          ret ? 〈E0, next … l (set_carry … carry st)〉
263      | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
264      | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
265      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
266        ! v1 ← acca_retrieve … st sacc_a_reg;
267        ! v1 ← Byte_of_val v1;
268        ! v2 ← accb_retrieve … st sacc_b_reg;
269        ! v2 ← Byte_of_val v2;
270          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
271          let v1' ≝ BVByte v1' in
272          let v2' ≝ BVByte v2' in
273        ! st ← acca_store p dacc_a_reg v1' st;
274        ! st ← accb_store p dacc_b_reg v2' st;
275          ret ? 〈E0, next … l st〉
276      | POP dst ⇒
277        ! 〈st,v〉 ← pop … st;
278        ! st ← acca_store p dst v st;
279          ret ? 〈E0, next … l st〉
280      | PUSH src ⇒
281        ! v ← acca_retrieve … st src;
282        ! st ← push … st v;
283          ret ? 〈E0, next … l st〉
284      | MOVE dst_src ⇒
285        ! st ← pair_reg_move … st dst_src ;
286          ret ? 〈E0, next … l st〉
287      | CALL_ID id argsno dest ⇒
288        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
289        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
290          match fd with
291          [ Internal fn ⇒
292            ! st ← save_ra … st l;
293              let st ≝ save_frame … dest st in
294              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
295+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
296+ ALLOCARE LO STACK FRAME
297              let l' ≝ joint_if_entry … fn in
298             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
299          | External fn ⇒
300            ! params ← fetch_external_args … fn st;
301            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
302            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
303            (* CSC: XXX bug here; I think I should split it into Byte-long
304               components; instead I am making a singleton out of it *)
305              let vs ≝ [mk_val ? evres] in
306            ! st ← set_result … vs st;
307              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
308          ]]
309    | RETURN ⇒
310+ CHIAMARE UNA FUNZIONE PER ANDARE A SOSTITUIRE IL VALORE TROVATO NEL REGISTRO
311DI RITORNO DELLA FUNZIONE AL POSTO GIUSTO
312+ DEALLOCARE LO STACK FRAME
313      ! st ← pop_frame … st;
314      ! 〈st,pch〉 ← pop … st;
315      ! 〈st,pcl〉 ← pop … st;
316        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
317cases addr //
318qed.
319
320definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → nat → state p → option int ≝
321 λglobals,p,ge,exit,registersno,st.res_to_opt … (
322  do s ← fetch_statement … ge st;
323  match s with
324   [ RETURN ⇒
325      do 〈st,l〉 ← fetch_ra … st;
326      if eq_address l exit then
327       do val ← fetch_result … st registersno;
328       match val with
329        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
330        | _ ⇒ Error ? []]
331      else
332       Error ? []
333   | _ ⇒ Error ? []]).
334
335record evaluation_parameters : Type[1] ≝
336 { globals: list ident
337 ; sparams2: sem_params2 globals
338 ; exit: address
339 ; registersno: nat
340 ; genv2: genv globals sparams2
341 }.
342
343definition joint_exec: trans_system io_out io_in ≝
344  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
345   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G) (registersno G))
346   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
347
348definition make_global :
349 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
350  joint_program pars → evaluation_parameters
351
352 λpars,sparams.
353  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
354[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
355qed.
356
357definition make_initial_state :
358 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
359 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
360λpars,sparams,p.
361  let ge ≝ genv2 (make_global pars sparams p) in
362  do m ← init_mem Genv … (λx.[Init_space x]) p;
363  let main ≝ prog_main … p in
364  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
365  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
366  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
367cases daemon qed.
368(*
369RTL:
370 init_prog == init_mem
371 init_sp: inizializzare lo stack pointer
372 init_isp: inizializzare l'altro stack pointer
373 init_renv: inizializzare i registri fisici
374 init_main_call: chiamata di funzione
375   --- init_fun_call: cambia fra ERTL e LTL
376 change_carry: a 0
377*)
378
379definition joint_fullexec :
380 ∀pars:∀globals.params globals.
381 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
382 fullexec io_out io_in ≝
383 λpars,sparams.
384  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.