source: src/joint/semantics.ma @ 1281

Last change on this file since 1281 was 1281, checked in by sacerdot, 10 years ago

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

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