source: src/LTL/semantics.ma @ 1312

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

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

File size: 17.0 KB
Line 
1include "joint/SemanticUtils.ma".
2include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition ltl_more_sem_params: more_sem_params ltl_params_ :=
5 mk_more_sem_params ltl_params_
6  unit hw_register_env graph_succ_p
7   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
8    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
9    (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
10    (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
11     (λlocals,dest_src.
12       match dest_src with
13       [ from_acc reg ⇒
14          do v ← hwreg_retrieve locals RegisterA ;
15          hwreg_store reg v locals
16       | to_acc reg ⇒
17          do v ← hwreg_retrieve locals reg ;
18          hwreg_store RegisterA v locals ])
19     pointer_of_label.
20definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.
21
22definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
23definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st.
24definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st.
25
26definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
27 mk_more_sem_params1 ? ltl_params1 ltl_more_sem_params
28  ltl_init_locals ltl_pop_frame ltl_save_frame.
29
30(*CSC: XXXXX, for is_final only *)
31axiom ltl_fetch_result: state ltl_sem_params → nat → res val.
32
33(*CSC: XXXX, for external functions only*)
34axiom ltl_fetch_external_args: external_function → state ltl_sem_params → res (list val).
35axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).
36
37definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
38 ≝ λglobals,ge,abs. ⊥.
39@abs qed.
40
41definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝
42 λglobals.
43  mk_more_sem_params2 … ltl_more_sem_params1
44   (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result
45    (ltl_exec_extended …).
46
47definition ltl_fullexec ≝
48 joint_fullexec … (λp. ltl_more_sem_params2 (prog_var_names … p)).
49
50
51(*
52(* CSC: external functions never fail (??) and always return something of the
53   size of one register, both in the frontend and in the backend.
54   Is this reasonable??? In OCaml it always return a list, but in the frontend
55   only the head is kept (or Undef if the list is empty) ??? *)
56
57(* CSC: carries are values and booleans are not values; so we use integers.
58   But why using values at all? To have undef? *)
59(* CSC: ???????????? *)
60axiom smerge: val → val → res val.
61(* CSC: ???????????? In OCaml: IntValue.Int32.merge
62   Note also that the translation can fail; so it should be a res int! *)
63axiom smerge2: list val → int.
64(* CSC: I have a byte, I need a value, but it is complex to do so *)
65axiom val_of_Byte: Byte → val.
66axiom Byte_of_val: val → res Byte.
67axiom val_of_nat: nat → val.
68(* Map from the front-end memory model to the back-end memory model *)
69axiom represent_block: block → val × val.
70(* CSC: fixed size chunk *)
71axiom chunk: memory_chunk.
72axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
73
74axiom address: Type[0].
75axiom val_of_address: address → val. (* CSC: only to shift the sp *)
76axiom address_of_val: val → address. (* CSC: only to shift the sp *)
77axiom addr_sub: address → nat → address.
78axiom addr_add: address → nat → address.
79(* CSC: ??? *)
80axiom address_of_label: mem → label → address.
81axiom address_chunks_of_label: mem → label → Byte × Byte.
82axiom label_of_address_chunks: Byte → Byte → label.
83axiom address_of_address_chunks: Byte → Byte → address.
84axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
85axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
86axiom hwreg_retrieve : mRegisterMap → Register → res val.
87axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
88
89definition genv ≝ λglobals. (genv_t Genv) (fundef (ltl_internal_function globals)).
90
91(* CSC: frame reduced to this
92definition frame: Type[0] ≝ unit.
93*)
94
95record state : Type[0] ≝
96 { st_frms: unit (* CSC: frames are no longer useful *)
97 ; pc: address
98 ; sp: address
99 ; locals: unit (* CSC: no more locals *)
100 ; carry: val
101 ; regs: mRegisterMap
102 ; m: mem
103 }.
104
105definition set_m: mem → state → state ≝
106 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
107
108definition set_locals: (*CSC *) unit → state → state ≝
109 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
110
111definition set_regs: mRegisterMap → state → state ≝
112 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
113
114definition set_sp: address → state → state ≝
115 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
116
117definition set_carry: val → state → state ≝
118 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
119
120definition set_pc: address → state → state ≝
121 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
122
123(* CSC: was build_state in RTL *)
124definition goto: label → state → state ≝
125 λl,st. set_pc (address_of_label (m st) l) st.
126
127definition save_frame: state → state ≝ λst.st. (* CSC *)
128
129axiom FailedPopFrame: String.
130
131(* removes the top frame from the frames list *)
132definition pop_frame: state → res state ≝ λst.OK ? st. (* CSC *)
133
134axiom FailedStore: String.
135
136definition push: state → Byte → res state ≝
137 λst,v.
138  let sp ≝ val_of_address (sp st) in
139  (*CSC: no monadic notation here *)
140  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
141   (λm.
142    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
143    OK ? (set_m m (set_sp sp st))).
144
145
146definition pop: state → res (state × Byte) ≝
147 λst:state.
148  let sp ≝ val_of_address (sp st) in
149  let sp ≝ sub sp (val_of_memory_chunk chunk) in
150  let st ≝ set_sp (address_of_val sp) st in
151  (*CSC: no monadic notation here *)
152  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
153   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
154
155definition save_ra : state → label → res state ≝
156 λst,l.
157  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
158  (* No monadic notation here *)
159  bind ?? (push st addrl) (λst.push st addrh).
160
161(*CSC: unused now
162definition fetch_ra : state → res (state × label) ≝
163 λst.
164  (* No monadic notation here *)
165  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
166  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
167   OK ? 〈st, label_of_address_chunks addrl addrh〉)). *)
168
169(*CSC: To be implemented *)
170
171axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
172axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
173
174definition init_locals : list register → register_env val ≝
175foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
176
177definition reg_store ≝
178λreg,v,locals. update RegisterTag val locals reg v.
179
180axiom BadRegister : String.
181
182definition reg_retrieve : register_env val → register → res val ≝
183λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
184
185axiom MissingSymbol : String.
186axiom FailedLoad : String.
187axiom BadFunction : String.
188
189(*CSC: to be implemented *)
190axiom fetch_external_args: external_function → state → res (list val).(* ≝
191 λfn,st.
192  let registerno ≝ ? fn in
193  ! vs ←
194   mmap …
195    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
196  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
197  ?.*)
198
199(*CSC: to be implemented; fails if the first list is longer *)
200axiom fold_left2_first_not_longer:
201 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
202  ∀acc:C. ∀l1:list A. ∀l2: list B.
203   res C.
204
205(* CSC: the list should be a vector or have an upper bounded length *)
206definition set_result: list val → state → res state ≝
207 λvs,st.
208  (* CSC: monadic notation not used *)
209  bind ?? (
210   fold_left2_first_not_longer …
211    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
212  (λregs.OK ? (set_regs regs st)).
213
214definition fetch_result: state → nat → res (list val) ≝
215 λst,registersno.
216  let retregs ≝ prefix … registersno RegisterRets in
217  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
218
219definition framesize: list ident → state → res nat ≝
220  λglobals: list ident.
221  λst.
222  (* CSC: monadic notation missing here *)
223    bind ?? (fetch_function globals st) (λf.
224    OK ? (ltl_if_stacksize globals f)).
225
226definition get_hwsp : state → res address ≝
227 λst.
228  (* CSC: monadic notation missing here *)
229  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
230  (* CSC: monadic notation missing here *)
231  bind ?? (Byte_of_val spl) (λspl.
232  (* CSC: monadic notation missing here *)
233  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
234  (* CSC: monadic notation missing here *)
235  bind ?? (Byte_of_val sph) (λsph.
236  OK ? (address_of_address_chunks spl sph))))).
237
238definition set_hwsp : address → state → res state ≝
239 λsp,st.
240  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
241  (* CSC: monadic notation missing here *) 
242  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
243  (* CSC: monadic notation missing here *) 
244  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
245  OK ? (set_regs regs st))).
246
247(*
248(* CSC: completely different because different type for registers_move *)
249definition retrieve: state → registers_move → res val ≝
250  λst.
251  λr.
252  match r with
253  [ pseudo   src ⇒ reg_retrieve (locals st) src
254  | from_acc src ⇒ hwreg_retrieve (regs st) src
255  ].
256
257definition store ≝
258  λst.
259  λv.
260  λr.
261  match r with
262  [ pseudo   dst ⇒
263    ! locals ← reg_store dst v (locals st);
264      ret ? (set_locals locals st)
265  | hardware dst ⇒
266    ! regs ← hwreg_store dst v (regs st);
267      ret ? (set_regs regs st)
268  ].
269*)
270
271definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
272  λglobals. λge,st.
273  ! s ← fetch_statement globals st;
274  match s with
275    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
276    | joint_st_sequential seq l ⇒
277      match seq with
278      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
279      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
280      | joint_instr_int dest v ⇒
281        ! locals ← reg_store dest (val_of_Byte v) (locals st);
282          ret ? 〈E0, goto l (set_locals locals st)〉
283      | joint_instr_load addrl addrh dst ⇒
284        ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
285        ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
286        ! vaddr ← smerge vaddrl vaddrh;
287        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
288        ! regs ← hwreg_store dst v (regs st); (*CSC*)
289          ret ? 〈E0, goto l (set_regs regs st)〉
290      | joint_instr_store addrl addrh src ⇒
291        ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
292        ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
293        ! vaddr ← smerge vaddrl vaddrh;
294        ! v ← hwreg_retrieve (regs st) src; (*CSC*)
295        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
296          ret ? 〈E0, goto l (set_m m' st)〉
297      | joint_instr_cond src ltrue ⇒
298        ! v ← hwreg_retrieve (regs st) src; (*CSC*)
299        ! b ← eval_bool_of_val v;
300          ret ? 〈E0, goto (if b then ltrue else l) st〉
301      | joint_instr_address ident prf ldest hdest ⇒
302        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
303          let 〈laddr,haddr〉 ≝ represent_block addr in
304        ! locals ← reg_store ldest laddr (locals st);
305        ! locals ← reg_store hdest haddr locals;
306          ret ? 〈E0, goto l (set_locals locals st)〉
307      | joint_instr_op1 op acc_a ⇒
308        ! v ← reg_retrieve (locals st) acc_a;
309        ! v ← Byte_of_val v;
310          let v' ≝ val_of_Byte (op1 eval op v) in
311        ! locals ← reg_store acc_a v' (locals st);
312          ret ? 〈E0, goto l (set_locals locals st)〉
313      | joint_instr_op2 op acc_a_reg dest ⇒
314        ! v1 ← reg_retrieve (locals st) acc_a_reg;
315        ! v1 ← Byte_of_val v1;
316        ! v2 ← reg_retrieve (locals st) acc_a_reg;
317        ! v2 ← Byte_of_val v2;
318        ! carry ← eval_bool_of_val (carry st);
319          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
320          let v' ≝ val_of_Byte v' in
321          let carry ≝ of_bool carry in
322        ! locals ← reg_store dest v' (locals st);
323          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
324      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
325      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
326      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
327        ! v1 ← reg_retrieve (locals st) acc_a_reg;
328        ! v1 ← Byte_of_val v1;
329        ! v2 ← reg_retrieve (locals st) acc_b_reg;
330        ! v2 ← Byte_of_val v2;
331          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
332          let v1' ≝ val_of_Byte v1' in
333          let v2' ≝ val_of_Byte v2' in
334        ! locals ← reg_store acc_a_reg v1' (locals st);
335        ! locals ← reg_store acc_b_reg v2' locals;
336          ret ? 〈E0, goto l (set_locals locals st)〉
337      | joint_instr_pop dst ⇒
338        ! 〈st,v〉 ← pop st;
339        ! locals ← reg_store dst (val_of_Byte v) (locals st);
340          ret ? 〈E0, goto l (set_locals locals st)〉
341      | joint_instr_push src ⇒
342        ! v ← reg_retrieve (locals st) src;
343        ! v ← Byte_of_val v;
344        ! st ← push st v;
345          ret ? 〈E0, goto l st〉
346      | joint_instr_move dst_src ⇒
347        let 〈dst, src〉 ≝ dst_src in
348        ! v ← retrieve st src;
349        ! st ← store st v dst;
350          ret ? 〈E0, goto l st〉
351(*
352      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
353        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
354        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
355          match fd with
356          [ Internal fn ⇒
357            ! st ← save_ra st l;
358              let st ≝ save_frame st in
359              let locals ≝ init_locals (ertl_if_locals globals fn) in
360              let l' ≝ ertl_if_entry globals fn in
361              ret ? 〈 E0, goto l' (set_locals locals st)〉
362          | External fn ⇒
363            ! params ← fetch_external_args fn st;
364            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
365            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
366            (* CSC: XXX bug here; I think I should split it into Byte-long
367               components; instead I am making a singleton out of it *)
368              let vs ≝ [mk_val ? evres] in
369            ! st ← set_result vs st;
370              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
371          ]
372*)
373      | _ ⇒ ?
374      ]
375    (* CSC: changed, where the meat is *)
376    | joint_st_return ⇒
377      ! st ← pop_frame st;
378      ! 〈st,pch〉 ← pop st;
379      ! 〈st,pcl〉 ← pop st;
380        let pc ≝ address_of_address_chunks pcl pch in
381        ret ? 〈E0,set_pc pc st〉
382    ].
383  ].
384     
385axiom WrongReturnValueType: String.
386
387definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
388  λglobals: list ident.
389  λexit.
390  λregistersno.
391  λst.
392 (* CSC: monadic notation missing here *)
393  match fetch_statement globals st with
394  [ Error _ ⇒ None ?
395  | OK s ⇒
396    match s with
397    [ ertl_st_lift_pre pre ⇒
398      match pre with
399      [ joint_st_return ⇒
400        match fetch_ra st with
401         [ Error _ ⇒ None ?
402         | OK st_l ⇒
403           let 〈st,l〉 ≝ st_l in
404           match label_eq l exit with
405           [ inl _ ⇒
406             (* CSC: monadic notation missing here *)
407             match fetch_result st registersno with
408             [ Error _ ⇒ None ?
409             | OK vals ⇒ Some ? (smerge2 vals)
410             ]
411           | inr _ ⇒ None ?
412           ]
413         ]
414      | _ ⇒ None ?
415      ]
416    | _ ⇒ None ?
417    ]
418  ].
419
420definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
421  λglobals.
422  λexit.
423  λregistersno.
424  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
425
426(* CSC: XXX the program type does not fit with the globalenv and init_mem
427definition make_initial_state : rtl_program → res (genv × state) ≝
428λp.
429  do ge ← globalenv Genv ?? p;
430  do m ← init_mem Genv ?? p;
431  let main ≝ rtl_pr_main ?? p in
432  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
433  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
434  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
435
436definition RTL_fullexec : fullexec io_out io_in ≝
437  mk_fullexec … (λ_.RTL_exec) ? make_initial_state.
438*)
439*)
Note: See TracBrowser for help on using the repository browser.