source: src/joint/semantics.ma @ 1217

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

Only one axiom left.

File size: 13.8 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 sem_params: Type[1] ≝
20 { p:> params
21 ; framesT: Type[0]
22 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
23 
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
42definition address_of_label: sem_params → label → address.
43 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label p l)))
44 cases (beval_pair_of_pointer (pointer_of_label p l)) in ⊢ (???% → ?)
45  [ #res #_ @res
46  | #msg cases (pointer_of_label p l) * * #q #com #off #E1 #E2 destruct ]
47qed.
48
49record state (p: sem_params): Type[0] ≝
50 { st_frms: framesT p
51 ; pc: address
52 ; sp: pointer
53 ; carry: beval
54 ; regs: regsT p
55 ; m: bemem
56 }.
57
58definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
59
60record sem_params2 (globals: list ident): Type[1] ≝
61 { sparams:> sem_params
62 ; pre_sem_params:> sem_params_ sparams globals
63 
64 ; fetch_statement: state sparams → res (joint_statement sparams globals)
65 ; fetch_external_args: external_function → state sparams → res (list val)
66 ; set_result: list val → state sparams → res (state sparams)
67 ; fetch_result: state sparams → nat → res val
68
69 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
70 }.
71
72definition set_m: ∀p. bemem → state p → state p ≝
73 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
74
75definition set_regs: ∀p. regsT p → state p → state p ≝
76 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
77
78definition set_sp: ∀p. pointer → state p → state p ≝
79 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
80
81definition set_carry: ∀p. beval → state p → state p ≝
82 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
83
84definition set_pc: ∀p. address → state p → state p ≝
85 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
86
87definition set_frms: ∀p. framesT p → state p → state p ≝
88 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
89
90definition goto: ∀p:sem_params. label → state p → state p ≝
91 λp,l,st. set_pc … (address_of_label p l) st.
92
93definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
94 λp,dst,v,st.
95  do regs  ← greg_store_ … dst v (regs … st);
96  OK ? (set_regs … regs st).
97
98definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
99 λp,st,dst.greg_retrieve_ … (regs … st) dst.
100
101definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
102 λp,dst,v,st.
103  do regs ← acca_store_ … dst v (regs … st);
104  OK ? (set_regs … regs st).
105
106definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
107 λp,st,dst.acca_retrieve_ … (regs … st) dst.
108
109definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
110 λp,dst,v,st.
111  do regs ← accb_store_ … dst v (regs … st);
112  OK ? (set_regs … regs st).
113
114definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
115 λp,st,dst.accb_retrieve_ … (regs … st) dst.
116
117definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
118 λp,dst,v,st.
119  do regs ← dpl_store_ … dst v (regs … st);
120  OK ? (set_regs … regs st).
121
122definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
123 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
124
125definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
126 λp,dst,v,st.
127  do regs ← dph_store_ … dst v (regs … st);
128  OK ? (set_regs … regs st).
129
130definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
131 λp,st,dst.dph_retrieve_ … (regs … st) dst.
132
133definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
134 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
135
136definition save_frame: ∀p:sem_params. state p → state p ≝
137 λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
138
139(* removes the top frame from the frames list *)
140definition pop_frame: ∀p. state p → res (state p) ≝
141 λp,st.
142  do frames ← pop_frame_ p (st_frms … st);
143  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
144
145axiom FailedStore: String.
146
147definition push: ∀p. state p → beval → res (state p) ≝
148 λp,st,v.
149  let sp ≝ sp … st in
150  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
151  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
152  OK … (set_m … m (set_sp … sp st)).
153
154definition pop: ∀p. state p → res (state p × beval) ≝
155 λp,st.
156  let sp ≝ sp ? st in
157  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
158  let st ≝ set_sp … sp st in
159  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
160  OK ? 〈st,v〉.
161
162definition save_ra : ∀p. state p → label → res (state p) ≝
163 λp,st,l.
164  let 〈addrl,addrh〉 ≝ address_of_label p l in
165  do st ← push … st addrl;
166  push … st addrh.
167
168definition fetch_ra : ∀p.state p → res (state p × address) ≝
169 λp,st.
170  do 〈st,addrh〉 ← pop … st;
171  do 〈st,addrl〉 ← pop … st;
172  OK ? 〈st, 〈addrl,addrh〉〉.
173
174axiom MissingSymbol : String.
175axiom FailedLoad : String.
176axiom BadFunction : String.
177
178(*CSC: move elsewhere *)
179definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
180 λA,P,c. match c with [ dp w _ ⇒ w ].
181coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
182
183definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
184  λglobals,p. λge,st.
185  ! s ← fetch_statement globals p st;
186  match s with
187    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
188    | joint_st_sequential seq l ⇒
189      match seq with
190      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto … l st〉
191      | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
192      | joint_instr_int dest v ⇒
193        ! st ← greg_store … dest (BVByte v) st;
194          ret ? 〈E0, goto … l st〉
195      | joint_instr_load dst addrl addrh ⇒
196        ! vaddrh ← dph_retrieve … st addrh;
197        ! vaddrl ← dpl_retrieve … st addrl;
198        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
199        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
200        ! st ← acca_store … dst v st;
201          ret ? 〈E0, goto … l st〉
202      | joint_instr_store addrl addrh src ⇒
203        ! vaddrh ← dph_retrieve … st addrh;
204        ! vaddrl ← dpl_retrieve … st addrl;
205        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
206        ! v ← acca_retrieve … st src;
207        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
208          ret ? 〈E0, goto … l (set_m … m' st)〉
209      | joint_instr_cond src ltrue ⇒
210        ! v ← acca_retrieve … st src;
211        ! b ← bool_of_beval v;
212          ret ? 〈E0, goto … (if b then ltrue else l) st〉
213      | joint_instr_address ident prf ldest hdest ⇒
214        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
215        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
216        ! st ← dpl_store … ldest laddr st;
217        ! st ← dph_store … hdest haddr st;
218          ret ? 〈E0, goto … l st〉
219      | joint_instr_op1 op acc_a ⇒
220        ! v ← acca_retrieve … st acc_a;
221        ! v ← Byte_of_val v;
222          let v' ≝ BVByte (op1 eval op v) in
223        ! st ← acca_store … acc_a v' st;
224          ret ? 〈E0, goto … l st〉
225      | joint_instr_op2 op acc_a src ⇒
226        ! v1 ← acca_retrieve … st acc_a;
227        ! v1 ← Byte_of_val v1;
228        ! v2 ← greg_retrieve … st src;
229        ! v2 ← Byte_of_val v2;
230        ! carry ← bool_of_beval (carry … st);
231          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
232          let v' ≝ BVByte v' in
233          let carry ≝ beval_of_bool carry in
234        ! st ← acca_store … acc_a v' st;
235          ret ? 〈E0, goto … l (set_carry … carry st)〉
236      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVfalse st)〉
237      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVtrue st)〉
238      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
239        ! v1 ← acca_retrieve … st acc_a_reg;
240        ! v1 ← Byte_of_val v1;
241        ! v2 ← accb_retrieve … st acc_b_reg;
242        ! v2 ← Byte_of_val v2;
243          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
244          let v1' ≝ BVByte v1' in
245          let v2' ≝ BVByte v2' in
246        ! st ← acca_store … acc_a_reg v1' st;
247        ! st ← accb_store … acc_b_reg v2' st;
248          ret ? 〈E0, goto … l st〉
249      | joint_instr_pop dst ⇒
250        ! 〈st,v〉 ← pop … st;
251        ! st ← acca_store … dst v st;
252          ret ? 〈E0, goto … l st〉
253      | joint_instr_push src ⇒
254        ! v ← acca_retrieve … st src;
255        ! st ← push … st v;
256          ret ? 〈E0, goto … l st〉
257      | joint_instr_move dst_src ⇒
258          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
259      | joint_instr_call_id id argsno ⇒
260        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
261        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
262          match fd with
263          [ Internal fn ⇒
264            ! st ← save_ra … st l;
265              let st ≝ save_frame … st in
266              let regs ≝ init_locals p (joint_if_locals … fn) in
267              let l' ≝ joint_if_entry … fn in
268             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
269          | External fn ⇒
270            ! params ← fetch_external_args … fn st;
271            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
272            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
273            (* CSC: XXX bug here; I think I should split it into Byte-long
274               components; instead I am making a singleton out of it *)
275              let vs ≝ [mk_val ? evres] in
276            ! st ← set_result … vs st;
277              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
278          ]]
279    | joint_st_return ⇒
280      ! st ← pop_frame … st;
281      ! 〈st,pch〉 ← pop … st;
282      ! 〈st,pcl〉 ← pop … st;
283        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
284    | joint_st_extension c ⇒ exec_extended … p ge c st ].
285cases addr //
286qed.
287
288definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
289  λglobals,p,exit,registersno,st. res_to_opt … (
290  do s ← fetch_statement … st;
291  match s with
292   [ joint_st_return ⇒
293      do 〈st,l〉 ← fetch_ra … st;
294      if eq_address l exit then
295       do val ← fetch_result globals p st registersno;
296       match val with
297        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
298        | _ ⇒ Error ? []]
299      else
300       Error ? []
301   | _ ⇒ Error ? []]).
302
303definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
304  λglobals,p.
305  λexit.
306  λregistersno.
307  mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).
308
309(* CSC: XXX the program type does not fit with the globalenv and init_mem *)
310axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝
311λp.
312  do ge ← globalenv Genv ?? p;
313  do m ← init_mem Genv ?? p;
314  let main ≝ rtl_pr_main ?? p in
315  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
316  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
317  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
318*)
319
320definition joint_fullexec :
321 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
322 λglobals,p,program.
323  let exit ≝ ? in
324  let registersno ≝ ? in
325  mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).
Note: See TracBrowser for help on using the repository browser.