source: src/LTL/semantics.ma @ 1303

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