source: src/joint/semantics.ma @ 1213

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

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

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