source: src/joint/semantics.ma @ 1324

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

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

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) → succ p → 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 l 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.