source: src/ERTL/semantics.ma @ 1386

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

Structure of semantic parameters simplified.

File size: 4.9 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.
15  do res ← hwreg_store r v (\snd local_env) ;
16  OK … 〈\fst local_env,res〉.
[1130]17
[1302]18definition hw_reg_retrieve ≝
19 λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env).
20
21definition ertl_more_sem_params: more_sem_params ertl_params_ :=
22 mk_more_sem_params ertl_params_
[1313]23  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
[1302]24   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
25    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
26     (λlocals,dest_src.
27       do v ←
28        match \snd dest_src with
29        [ pseudo reg ⇒ ps_reg_retrieve locals reg
30        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
31       match \fst dest_src with
32       [ pseudo reg ⇒ ps_reg_store reg v locals
33       | hardware reg ⇒ hw_reg_store reg v locals])
34     pointer_of_label.
35definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
36
[1318]37definition ertl_init_locals :
38 list register →
39  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
40 λlocals,lenv.
41  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
[1313]42
[1318]43(*CSC: could we use here a dependent type to avoid the Error case? *)
44axiom EmptyStack: String.
[1385]45definition ertl_pop_frame:
46 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
47 λglobals,ge,st.
[1318]48  let frms ≝ st_frms ? st in
49  match frms with
50  [ nil ⇒ Error ? [MSG EmptyStack]
51  | cons hd tl ⇒
[1384]52     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
[1318]53
[1377]54definition ertl_save_frame:
55 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
56 λl.λ_.λ_.λ_.λ_.λst.
57  do st ← save_ra … st l ;
[1371]58  OK …
59   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
60    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
[1318]61
[1302]62(*CSC: XXXXX, for is_final only *)
[1385]63axiom ertl_fetch_result:
64 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval).
[1302]65
66(*CSC: XXXX, for external functions only*)
67axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
68axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
69
[1327]70(*CSC: XXXX *)
71axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝
72  λglobals: list ident.
73  λst.
74   do f ← fetch_function globals st ;
75   OK ? (joint_if_stacksize globals … f).*)
[1302]76
[1327]77definition get_hwsp : state ertl_sem_params → res address ≝
78 λst.
79  do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ;
80  do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ;
81  OK ? 〈spl,sph〉.
82
83definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝
84 λsp,st.
85  let 〈spl,sph〉 ≝ sp in
86  do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ;
87  do hwregs ← hwreg_store RegisterSPH sph hwregs ;
88  OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st).
89
90definition ertl_exec_extended:
91 ∀globals. genv globals (ertl_params globals) →
92  ertl_statement_extension → label → state ertl_sem_params →
93   IO io_out io_in (trace × (state ertl_sem_params)) ≝
94 λglobals,ge,stm,l,st.
95  match stm with
96   [ ertl_st_ext_new_frame ⇒
97      ! v ← framesize globals st;
98      ! sp ← get_hwsp st;
[1329]99      ! newsp ← addr_sub sp v;
[1327]100      ! st ← set_hwsp newsp st;
101        ret ? 〈E0,goto … l st〉
102   | ertl_st_ext_del_frame ⇒
103      ! v ← framesize globals st;
104      ! sp ← get_hwsp st;
[1329]105      ! newsp ← addr_add sp v;
[1327]106      ! st ← set_hwsp newsp st;
107        ret ? 〈E0,goto … l st〉
108   | ertl_st_ext_frame_size dst ⇒
109      ! v ← framesize globals st;
110      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
111        ret ? 〈E0, goto … l st〉
112   ].
113
[1302]114definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
115 λglobals.
[1386]116  mk_more_sem_params2 … ertl_more_sem_params
[1385]117   (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
[1386]118   ertl_init_locals ertl_save_frame (ertl_pop_frame …)
119   ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
[1302]120
121definition ertl_fullexec ≝
122 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.