source: src/joint/semantics.ma @ 1233

Last change on this file since 1233 was 1233, checked in by sacerdot, 9 years ago

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

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 ≝ λp:params.λglobals. (genv_t Genv) (joint_function p globals).
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 (p: params) (globals: list ident): 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 p globals → 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
78 ; more_sparams2:> more_sem_params2 p2 globals
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
208(*CSC: move elsewhere *)
209definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
210 λA,P,c. match c with [ dp w _ ⇒ w ].
211coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
212
213definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals → state p → IO io_out io_in (trace × (state p)) ≝
214 λglobals,p,ge,st.
215  ! s ← fetch_statement … st;
216  match s with
217    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
218    | joint_st_sequential seq l ⇒
219      match seq with
220      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, next … l st〉
221      | joint_instr_comment c ⇒ ret ? 〈E0, next … l st〉
222      | joint_instr_int dest v ⇒
223        ! st ← greg_store ? dest (BVByte v) st;
224          ret ? 〈E0, next … l st〉
225      | joint_instr_load dst addrl addrh ⇒
226        ! vaddrh ← dph_retrieve … st addrh;
227        ! vaddrl ← dpl_retrieve … st addrl;
228        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
229        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
230        ! st ← acca_store … dst v st;
231          ret ? 〈E0, next … l st〉
232      | joint_instr_store addrl addrh src ⇒
233        ! vaddrh ← dph_retrieve … st addrh;
234        ! vaddrl ← dpl_retrieve … st addrl;
235        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
236        ! v ← acca_retrieve … st src;
237        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
238          ret ? 〈E0, next … l (set_m … m' st)〉
239      | joint_instr_cond src ltrue ⇒
240        ! v ← acca_retrieve … st src;
241        ! b ← bool_of_beval v;
242          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
243      | joint_instr_address ident prf ldest hdest ⇒
244        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
245        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
246        ! st ← dpl_store … ldest laddr st;
247        ! st ← dph_store … hdest haddr st;
248          ret ? 〈E0, next … l st〉
249      | joint_instr_op1 op acc_a ⇒
250        ! v ← acca_retrieve … st acc_a;
251        ! v ← Byte_of_val v;
252          let v' ≝ BVByte (op1 eval op v) in
253        ! st ← acca_store … acc_a v' st;
254          ret ? 〈E0, next … l st〉
255      | joint_instr_op2 op acc_a src ⇒
256        ! v1 ← acca_retrieve … st acc_a;
257        ! v1 ← Byte_of_val v1;
258        ! v2 ← greg_retrieve … st src;
259        ! v2 ← Byte_of_val v2;
260        ! carry ← bool_of_beval (carry … st);
261          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
262          let v' ≝ BVByte v' in
263          let carry ≝ beval_of_bool carry in
264        ! st ← acca_store … acc_a v' st;
265          ret ? 〈E0, next … l (set_carry … carry st)〉
266      | joint_instr_clear_carry ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
267      | joint_instr_set_carry ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
268      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
269        ! v1 ← acca_retrieve … st acc_a_reg;
270        ! v1 ← Byte_of_val v1;
271        ! v2 ← accb_retrieve … st acc_b_reg;
272        ! v2 ← Byte_of_val v2;
273          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
274          let v1' ≝ BVByte v1' in
275          let v2' ≝ BVByte v2' in
276        ! st ← acca_store … acc_a_reg v1' st;
277        ! st ← accb_store … acc_b_reg v2' st;
278          ret ? 〈E0, next … l st〉
279      | joint_instr_pop dst ⇒
280        ! 〈st,v〉 ← pop … st;
281        ! st ← acca_store … dst v st;
282          ret ? 〈E0, next … l st〉
283      | joint_instr_push src ⇒
284        ! v ← acca_retrieve … st src;
285        ! st ← push … st v;
286          ret ? 〈E0, next … l st〉
287      | joint_instr_move dst_src ⇒
288          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
289      | joint_instr_call_id id argsno ⇒
290        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
291        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
292          match fd with
293          [ Internal fn ⇒
294            ! st ← save_ra … st l;
295              let st ≝ save_frame … st in
296              let regs ≝ init_locals (sem_params_of_sem_params2 globals p) … (joint_if_locals … fn) in
297              let l' ≝ joint_if_entry … fn in
298             ret ? 〈 E0, goto … l' (set_regs … 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    | joint_st_return ⇒
310      ! st ← pop_frame … st;
311      ! 〈st,pch〉 ← pop … st;
312      ! 〈st,pcl〉 ← pop … st;
313        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
314    | joint_st_extension c ⇒ exec_extended … p ge c st ].
315cases addr //
316qed.
317
318definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
319 λglobals,p,exit,registersno,st. res_to_opt … (
320  do s ← fetch_statement … st;
321  match s with
322   [ joint_st_return ⇒
323      do 〈st,l〉 ← fetch_ra … st;
324      if eq_address l exit then
325       do val ← fetch_result … st registersno;
326       match val with
327        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
328        | _ ⇒ Error ? []]
329      else
330       Error ? []
331   | _ ⇒ Error ? []]).
332
333record evaluation_parameters : Type[1] ≝
334 { globals: list ident
335 ; sparams2: sem_params2 globals
336 ; exit: address
337 ; registersno: nat
338 ; genv2: genv sparams2 globals
339 }.
340
341definition joint_exec: trans_system io_out io_in ≝
342  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
343   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
344   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
345
346definition make_global :
347 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
348  joint_program pars → evaluation_parameters
349
350 λpars,sparams.
351  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
352[1,2: cases daemon ]
353qed.
354
355definition make_initial_state :
356 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
357 ∀p: joint_program … pars. res (state (mk_sem_params pars (sparams p))) ≝
358λpars,sparams,p.
359  let ge ≝ genv2 (make_global pars sparams p) in
360  do m ← init_mem Genv … (λx.[Init_space x]) p;
361  let main ≝ prog_main … p in
362  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
363  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
364  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
365cases daemon qed.
366(*
367RTL:
368 init_prog == init_mem
369 init_sp: inizializzare lo stack pointer
370 init_isp: inizializzare l'altro stack pointer
371 init_renv: inizializzare i registri fisici
372 init_main_call: chiamata di funzione
373   --- init_fun_call: cambia fra ERTL e LTL
374 change_carry: a 0
375*)
376
377definition joint_fullexec :
378 ∀pars:params.
379 ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
380 fullexec io_out io_in ≝
381 λpars,sparams.
382  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.