source: src/LTL/semantics.ma @ 1380

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

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

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