source: src/joint/semantics.ma @ 1312

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

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

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