source: src/ERTL/semantics.ma @ 1415

Last change on this file since 1415 was 1415, checked in by sacerdot, 9 years ago
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
File size: 5.1 KB
RevLine 
[1302]1include "joint/SemanticUtils.ma".
2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
[1359]3include alias "common/Identifiers.ma".
[1130]4
[1302]5definition ps_reg_store ≝
6 λr,v.λlocal_env:(register_env beval) × hw_register_env.
7  do res ← reg_store r v (\fst local_env) ;
8  OK … 〈res, \snd local_env〉.
[1130]9
[1302]10definition ps_reg_retrieve ≝
11 λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
[1130]12
[1302]13definition hw_reg_store ≝
14 λr,v.λlocal_env:(register_env beval) × hw_register_env.
[1415]15  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
[1130]16
[1302]17definition hw_reg_retrieve ≝
[1415]18 λlocal_env:(register_env beval) × hw_register_env.λreg.
19  OK … (hwreg_retrieve … (\snd local_env) reg).
[1302]20
21definition ertl_more_sem_params: more_sem_params ertl_params_ :=
22 mk_more_sem_params ertl_params_
[1408]23  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
[1415]24   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
[1408]25   graph_succ_p
[1302]26   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
27    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
28     (λlocals,dest_src.
29       do v ←
30        match \snd dest_src with
31        [ pseudo reg ⇒ ps_reg_retrieve locals reg
32        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
33       match \fst dest_src with
34       [ pseudo reg ⇒ ps_reg_store reg v locals
35       | hardware reg ⇒ hw_reg_store reg v locals])
36     pointer_of_label.
37definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
38
[1318]39definition ertl_init_locals :
40 list register →
41  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
42 λlocals,lenv.
43  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
[1313]44
[1318]45(*CSC: could we use here a dependent type to avoid the Error case? *)
46axiom EmptyStack: String.
[1385]47definition ertl_pop_frame:
48 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
49 λglobals,ge,st.
[1318]50  let frms ≝ st_frms ? st in
51  match frms with
52  [ nil ⇒ Error ? [MSG EmptyStack]
53  | cons hd tl ⇒
[1384]54     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
[1318]55
[1377]56definition ertl_save_frame:
57 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
58 λl.λ_.λ_.λ_.λ_.λst.
59  do st ← save_ra … st l ;
[1371]60  OK …
61   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
62    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
[1318]63
[1390]64definition ertl_result_regs:
65 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
[1388]66 λglobals,ge,st.
67  do fn ← graph_fetch_function … globals ge st ;
[1390]68  OK … (joint_if_result … fn).
[1302]69
70(*CSC: XXXX, for external functions only*)
71axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
72axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
73
[1389]74definition framesize:
75 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
76  λglobals,ge,st.
77   do f ← graph_fetch_function … ge st ;
78   OK ? (joint_if_stacksize globals … f).
[1302]79
[1415]80definition get_hwsp : state ertl_sem_params → address ≝
[1327]81 λst.
[1415]82  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
83  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
84   〈spl,sph〉.
[1327]85
[1415]86definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params ≝
[1327]87 λsp,st.
88  let 〈spl,sph〉 ≝ sp in
[1415]89  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
90  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
91  set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
[1327]92
93definition ertl_exec_extended:
94 ∀globals. genv globals (ertl_params globals) →
95  ertl_statement_extension → label → state ertl_sem_params →
96   IO io_out io_in (trace × (state ertl_sem_params)) ≝
97 λglobals,ge,stm,l,st.
98  match stm with
99   [ ertl_st_ext_new_frame ⇒
[1389]100      ! v ← framesize globals … ge st;
[1415]101      let sp ≝ get_hwsp st in
[1329]102      ! newsp ← addr_sub sp v;
[1415]103      let st ≝ set_hwsp newsp st in
[1327]104        ret ? 〈E0,goto … l st〉
105   | ertl_st_ext_del_frame ⇒
[1389]106      ! v ← framesize … ge st;
[1415]107      let sp ≝ get_hwsp st in
[1329]108      ! newsp ← addr_add sp v;
[1415]109      let st ≝ set_hwsp newsp st in
[1327]110        ret ? 〈E0,goto … l st〉
111   | ertl_st_ext_frame_size dst ⇒
[1389]112      ! v ← framesize … ge st;
[1327]113      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
114        ret ? 〈E0, goto … l st〉
115   ].
116
[1302]117definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
118 λglobals.
[1411]119  mk_more_sem_params2 …
120   (mk_more_sem_params1 … ertl_more_sem_params
121    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
122    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
123    ertl_fetch_external_args ertl_set_result)
124   (ertl_exec_extended …).
[1302]125
126definition ertl_fullexec ≝
127 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.