source: src/joint/semantics.ma @ 1186

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

Spurious code removed.
joint_fullexec implemented up to make_initial_state and exit symbol/registersno
for main function.

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