source: src/joint/semantics.ma @ 1215

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

1) Added shifting directly on pointers
2) More temporary axioms closed.

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