source: src/joint/semantics.ma @ 1250

Last change on this file since 1250 was 1250, checked in by sacerdot, 8 years ago
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File size: 16.0 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
13definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)
14
15definition eq_address: address → address → bool ≝
16 λaddr1,addr2.
17  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
18
19record more_sem_params (p:params_): Type[1] ≝
20 { framesT: Type[0]
21 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
22
23 ; succ_pc: succ p → address → address
24 ; pop_frame_: framesT → res framesT
25 ; save_frame_: framesT → regsT → framesT
26 ; greg_store_: generic_reg p → beval → regsT → res regsT
27 ; greg_retrieve_: regsT → generic_reg p → res beval
28 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
29 ; acca_retrieve_: regsT → acc_a_reg p → res beval
30 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
31 ; accb_retrieve_: regsT → acc_b_reg p → res beval
32 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
33 ; dpl_retrieve_: regsT → dpl_reg p → res beval
34 ; dph_store_: dph_reg p → beval → regsT → res regsT
35 ; dph_retrieve_: regsT → dph_reg p → res beval
36 ; pair_reg_move_: regsT → pair_reg p → regsT
37 
38 ; init_locals : localsT p → regsT
39 ; pointer_of_label: label → Σp:pointer. ptype p = Code
40 }.
41
42record sem_params: Type[1] ≝
43 { spp :> params_
44 ; more_sem_pars :> more_sem_params spp
45 }.
46
47record state (p: sem_params): Type[0] ≝
48 { st_frms: framesT ? p
49 ; pc: address
50 ; sp: pointer
51 ; carry: beval
52 ; regs: regsT ? p
53 ; m: bemem
54 }.
55
56definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
57
58(*
59CSC: fetch_statement credo sia implementabile ⇒ globals non e' necessario ⇒ niente
60casino e posso back-trackare il cambiamento in SmallstepExec!!! Togliere del
61tutto il parametro a exec_extended.
62CSC: NO! RTL ha come exec_extended tail_call e (tail_)call_ptr che usa genv
63*)
64
65record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
66 { more_sparams:> more_sem_params p
67 
68 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
69 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
70 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
71 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
72
73 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
74 }.
75
76record sem_params2 (globals: list ident): Type[1] ≝
77 { p2:> params globals
78 ; more_sparams2:> more_sem_params2 globals p2
79 }.
80
81definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
82coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
83 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
84(*
85unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
86   S ≟ sem_params_of_sem_params2 globals p
87(* ---------------------------------------- *) ⊢
88   pars_ (spp (mk_sem_params (p2 globals p)
89    (more_sparams (p2 globals p) globals
90    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
91*)
92definition address_of_label: sem_params → label → address.
93 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
94 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
95  [ #res #_ @res
96  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
97qed.
98
99definition set_m: ∀p. bemem → state p → state p ≝
100 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
101
102definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
103 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
104
105definition set_sp: ∀p. pointer → state p → state p ≝
106 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
107
108definition set_carry: ∀p. beval → state p → state p ≝
109 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
110
111definition set_pc: ∀p. address → state p → state p ≝
112 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
113
114definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
115 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
116
117definition goto: ∀p:sem_params. label → state p → state p ≝
118 λp,l,st. set_pc … (address_of_label p l) st.
119
120definition next: ∀p:sem_params. succ … p → state p → state p ≝
121 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
122
123definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
124 λp,dst,v,st.
125  do regs  ← greg_store_ … dst v (regs … st);
126  OK ? (set_regs … regs st).
127
128definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
129 λp,st,dst.greg_retrieve_ … (regs … st) dst.
130
131definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
132 λp,dst,v,st.
133  do regs ← acca_store_ … dst v (regs … st);
134  OK ? (set_regs … regs st).
135
136definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
137 λp,st,dst.acca_retrieve_ … (regs … st) dst.
138
139definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
140 λp,dst,v,st.
141  do regs ← accb_store_ … dst v (regs … st);
142  OK ? (set_regs … regs st).
143
144definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
145 λp,st,dst.accb_retrieve_ … (regs … st) dst.
146
147definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
148 λp,dst,v,st.
149  do regs ← dpl_store_ … dst v (regs … st);
150  OK ? (set_regs … regs st).
151
152definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
153 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
154
155definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
156 λp,dst,v,st.
157  do regs ← dph_store_ … dst v (regs … st);
158  OK ? (set_regs … regs st).
159
160definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
161 λp,st,dst.dph_retrieve_ … (regs … st) dst.
162
163definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
164 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
165
166definition save_frame: ∀p:sem_params. state p → state p ≝
167 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
168
169(* removes the top frame from the frames list *)
170definition pop_frame: ∀p. state p → res (state p) ≝
171 λp,st.
172  do frames ← pop_frame_ … p (st_frms … st);
173  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
174
175axiom FailedStore: String.
176
177definition push: ∀p. state p → beval → res (state p) ≝
178 λp,st,v.
179  let sp ≝ sp … st in
180  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
181  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
182  OK … (set_m … m (set_sp … sp st)).
183
184definition pop: ∀p. state p → res (state p × beval) ≝
185 λp,st.
186  let sp ≝ sp ? st in
187  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
188  let st ≝ set_sp … sp st in
189  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
190  OK ? 〈st,v〉.
191
192definition save_ra : ∀p. state p → succ p → res (state p) ≝
193 λp,st,l.
194  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
195  do st ← push … st addrl;
196  push … st addrh.
197
198definition fetch_ra : ∀p.state p → res (state p × address) ≝
199 λp,st.
200  do 〈st,addrh〉 ← pop … st;
201  do 〈st,addrl〉 ← pop … st;
202  OK ? 〈st, 〈addrl,addrh〉〉.
203
204axiom MissingSymbol : String.
205axiom FailedLoad : String.
206axiom BadFunction : String.
207
208definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
209 λglobals,p,ge,st.
210  ! s ← fetch_statement … st;
211  match s with
212    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
213    | joint_st_sequential seq l ⇒
214      match seq with
215      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, next … l st〉
216      | joint_instr_comment c ⇒ ret ? 〈E0, next … l st〉
217      | joint_instr_int dest v ⇒
218        ! st ← greg_store ? dest (BVByte v) st;
219          ret ? 〈E0, next … l st〉
220      | joint_instr_load dst addrl addrh ⇒
221        ! vaddrh ← dph_retrieve … st addrh;
222        ! vaddrl ← dpl_retrieve … st addrl;
223        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
224        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
225        ! st ← acca_store … dst v st;
226          ret ? 〈E0, next … l st〉
227      | joint_instr_store addrl addrh src ⇒
228        ! vaddrh ← dph_retrieve … st addrh;
229        ! vaddrl ← dpl_retrieve … st addrl;
230        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
231        ! v ← acca_retrieve … st src;
232        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
233          ret ? 〈E0, next … l (set_m … m' st)〉
234      | joint_instr_cond src ltrue ⇒
235        ! v ← acca_retrieve … st src;
236        ! b ← bool_of_beval v;
237          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
238      | joint_instr_address ident prf ldest hdest ⇒
239        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
240        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
241        ! st ← dpl_store … ldest laddr st;
242        ! st ← dph_store … hdest haddr st;
243          ret ? 〈E0, next … l st〉
244      | joint_instr_op1 op acc_a ⇒
245        ! v ← acca_retrieve … st acc_a;
246        ! v ← Byte_of_val v;
247          let v' ≝ BVByte (op1 eval op v) in
248        ! st ← acca_store … acc_a v' st;
249          ret ? 〈E0, next … l st〉
250      | joint_instr_op2 op acc_a src ⇒
251        ! v1 ← acca_retrieve … st acc_a;
252        ! v1 ← Byte_of_val v1;
253        ! v2 ← greg_retrieve … st src;
254        ! v2 ← Byte_of_val v2;
255        ! carry ← bool_of_beval (carry … st);
256          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
257          let v' ≝ BVByte v' in
258          let carry ≝ beval_of_bool carry in
259        ! st ← acca_store … acc_a v' st;
260          ret ? 〈E0, next … l (set_carry … carry st)〉
261      | joint_instr_clear_carry ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
262      | joint_instr_set_carry ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
263      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
264        ! v1 ← acca_retrieve … st acc_a_reg;
265        ! v1 ← Byte_of_val v1;
266        ! v2 ← accb_retrieve … st acc_b_reg;
267        ! v2 ← Byte_of_val v2;
268          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
269          let v1' ≝ BVByte v1' in
270          let v2' ≝ BVByte v2' in
271        ! st ← acca_store … acc_a_reg v1' st;
272        ! st ← accb_store … acc_b_reg v2' st;
273          ret ? 〈E0, next … l st〉
274      | joint_instr_pop dst ⇒
275        ! 〈st,v〉 ← pop … st;
276        ! st ← acca_store … dst v st;
277          ret ? 〈E0, next … l st〉
278      | joint_instr_push src ⇒
279        ! v ← acca_retrieve … st src;
280        ! st ← push … st v;
281          ret ? 〈E0, next … l st〉
282      | joint_instr_move dst_src ⇒
283          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
284      | joint_instr_call_id id argsno ⇒
285        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
286        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
287          match fd with
288          [ Internal fn ⇒
289            ! st ← save_ra … st l;
290              let st ≝ save_frame … st in
291              let regs ≝ init_locals (sem_params_of_sem_params2 globals p) … (joint_if_locals … fn) in
292              let l' ≝ joint_if_entry … fn in
293             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
294          | External fn ⇒
295            ! params ← fetch_external_args … fn st;
296            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
297            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
298            (* CSC: XXX bug here; I think I should split it into Byte-long
299               components; instead I am making a singleton out of it *)
300              let vs ≝ [mk_val ? evres] in
301            ! st ← set_result … vs st;
302              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
303          ]]
304    | joint_st_return ⇒
305      ! st ← pop_frame … st;
306      ! 〈st,pch〉 ← pop … st;
307      ! 〈st,pcl〉 ← pop … st;
308        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
309    | joint_st_extension c ⇒ exec_extended … p ge c st ].
310cases addr //
311qed.
312
313definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
314 λglobals,p,exit,registersno,st. res_to_opt … (
315  do s ← fetch_statement … st;
316  match s with
317   [ joint_st_return ⇒
318      do 〈st,l〉 ← fetch_ra … st;
319      if eq_address l exit then
320       do val ← fetch_result … st registersno;
321       match val with
322        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
323        | _ ⇒ Error ? []]
324      else
325       Error ? []
326   | _ ⇒ Error ? []]).
327
328record evaluation_parameters : Type[1] ≝
329 { globals: list ident
330 ; sparams2: sem_params2 globals
331 ; exit: address
332 ; registersno: nat
333 ; genv2: genv globals sparams2
334 }.
335
336definition joint_exec: trans_system io_out io_in ≝
337  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
338   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
339   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
340
341definition make_global :
342 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
343  joint_program pars → evaluation_parameters
344
345 λpars,sparams.
346  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
347[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
348qed.
349
350definition make_initial_state :
351 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
352 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
353λpars,sparams,p.
354  let ge ≝ genv2 (make_global pars sparams p) in
355  do m ← init_mem Genv … (λx.[Init_space x]) p;
356  let main ≝ prog_main … p in
357  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
358  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
359  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
360cases daemon qed.
361(*
362RTL:
363 init_prog == init_mem
364 init_sp: inizializzare lo stack pointer
365 init_isp: inizializzare l'altro stack pointer
366 init_renv: inizializzare i registri fisici
367 init_main_call: chiamata di funzione
368   --- init_fun_call: cambia fra ERTL e LTL
369 change_carry: a 0
370*)
371
372definition joint_fullexec :
373 ∀pars:∀globals.params globals.
374 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
375 fullexec io_out io_in ≝
376 λpars,sparams.
377  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.