source: src/LTL/semantics.ma @ 1377

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

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

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