source: src/RTLabs/semantics.ma @ 765

Last change on this file since 765 was 765, checked in by campbell, 9 years ago

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

File size: 9.0 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "common/Errors.ma".
6include "common/Globalenvs.ma".
7include "common/IO.ma".
8include "common/SmallstepExec.ma".
9
10include "RTLabs/syntax.ma".
11
12definition genv ≝ (genv_t Genv) (fundef internal_function).
13
14record frame : Type[0] ≝
15{ func   : internal_function
16; locals : register_env val
17; next   : label
18; sp     : block
19; retdst : option register
20}.
21
22definition adv : label → frame → frame ≝
23λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f).
24
25inductive state : Type[0] ≝
26| State :
27   ∀   f : frame.
28   ∀  fs : list frame.
29   ∀   m : mem.
30   state
31| Callstate :
32   ∀  fd : fundef internal_function.
33   ∀args : list val.
34   ∀ dst : option register.
35   ∀ stk : list frame.
36   ∀   m : mem.
37   state
38| Returnstate :
39   ∀ rtv : option val.
40   ∀ dst : option register.
41   ∀ stk : list frame.
42   ∀   m : mem.
43   state.
44
45definition mem_of_state : state → mem ≝
46λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
47
48definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
49
50definition init_locals : list register → register_env val ≝
51foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
52
53definition reg_store ≝
54λreg,v,locals.
55  update RegisterTag val locals reg v.
56
57let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
58match rs with
59[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
60| cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
61  let locals' ≝ add RegisterTag val locals r v in
62  params_store rst vst locals'
63] ].
64
65definition reg_retrieve : register_env ? → register → res val ≝
66λlocals,reg. opt_to_res … (lookup ?? locals reg).
67
68(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
69
70definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
71λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
72[ Aindexed i ⇒ λargs.
73    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
74    opt_to_res … (ev_add v (Vint i))
75| Aindexed2 ⇒ λargs.
76    do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
77    do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
78    opt_to_res … (ev_add v1 v2)
79| Aglobal id off ⇒ λargs.
80    do loc ← opt_to_res … (find_symbol ?? ge id);
81    OK ? (Vptr Any loc ? (shift_offset zero_offset off))
82| Abased id off ⇒ λargs.
83    do loc ← opt_to_res … (find_symbol ?? ge id);
84    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
85    opt_to_res … (ev_add (Vptr Any loc ? zero_offset) v)
86| Ainstack off ⇒ λargs.
87    OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
88]
89. /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
90
91
92(* XXX put somewhere sensible *)
93let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
94match l with
95[ nil ⇒ None ?
96| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
97].
98
99definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
100λge,st.
101match st with
102[ State f fs m ⇒
103  ! s ← lookup ?? (f_graph (func f)) (next f);
104  match s with
105  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
106  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
107  | St_const r cst l ⇒
108      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
109      ! locals ← reg_store r v (locals f);
110      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
111  | St_op1 op dst src l ⇒
112      ! v ← reg_retrieve (locals f) src;
113      ! v' ← opt_to_res … (eval_unop op v);
114      ! locals ← reg_store dst v' (locals f);
115      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
116  | St_op2 op dst src1 src2 l ⇒
117      ! v1 ← reg_retrieve (locals f) src1;
118      ! v2 ← reg_retrieve (locals f) src2;
119      ! v' ← opt_to_res … (eval_binop op v1 v2);
120      ! locals ← reg_store dst v' (locals f);
121      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
122  | St_load chunk mode args dst l ⇒
123      ! vaddr ← eval_addr ge f mode args;
124      ! v ← opt_to_res … (loadv chunk m vaddr);
125      ! locals ← reg_store dst v (locals f);
126      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
127  | St_store chunk mode args src l ⇒
128      ! vaddr ← eval_addr ge f mode args;
129      ! v ← reg_retrieve (locals f) src;
130      ! m' ← opt_to_res … (storev chunk m vaddr v);
131      ret ? 〈E0, build_state f fs m' l〉
132
133  | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
134      ! b ← opt_to_res … (find_symbol ?? ge id);
135      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
136      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
137      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
138  | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
139      ! fv ← reg_retrieve (locals f) frs;
140      ! fd ← opt_to_res … (find_funct ?? ge fv);
141      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
142      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
143  | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
144      ! b ← opt_to_res … (find_symbol ?? ge id);
145      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
146      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
147      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
148  | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
149      ! fv ← reg_retrieve (locals f) frs;
150      ! fd ← opt_to_res … (find_funct ?? ge fv);
151      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
152      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
153
154  | St_condcst cst ltrue lfalse ⇒
155      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
156      ! b ← eval_bool_of_val v;
157      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
158  | St_cond1 op src ltrue lfalse ⇒
159      ! v ← reg_retrieve (locals f) src;
160      ! v' ← opt_to_res … (eval_unop op v);
161      ! b ← eval_bool_of_val v';
162      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
163  | St_cond2 op src1 src2 ltrue lfalse ⇒
164      ! v1 ← reg_retrieve (locals f) src1;
165      ! v2 ← reg_retrieve (locals f) src2;
166      ! v' ← opt_to_res … (eval_binop op v1 v2);
167      ! b ← eval_bool_of_val v';
168      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
169
170  | St_jumptable r ls ⇒
171      ! v ← reg_retrieve (locals f) r;
172      match v with
173      [ Vint i ⇒
174          ! l ← nth_opt ? (nat_of_bitvector ? i) ls;
175          ret ? 〈E0, build_state f fs m l〉
176      | _ ⇒ Wrong ???
177      ]
178
179  | St_return ⇒
180      ! v ← match f_result (func f) with
181            [ None ⇒ ret ? (None ?)
182            | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
183            ];
184      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
185  ]
186| Callstate fd params dst fs m ⇒
187    match fd with
188    [ Internal fn ⇒
189        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
190        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
191        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
192    | External fn ⇒
193        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
194        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
195        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
196    ]
197| Returnstate v dst fs m ⇒
198    match fs with
199    [ nil ⇒ Error ? (* Already in final state *)
200    | cons f fs' ⇒
201        ! locals ← match dst with
202                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
203                                         | _ ⇒ Error ? ]
204                   | Some d ⇒ match v with [ None ⇒ Error ?
205                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
206        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
207    ]
208].
209
210definition is_final : state → option int ≝
211λs. match s with
212[ State _ _ _ ⇒ None ?
213| Callstate _ _ _ _ _ ⇒ None ?
214| Returnstate v _ fs _ ⇒
215    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
216].
217
218definition RTLabs_exec : execstep io_out io_in ≝
219  mk_execstep … ? is_final mem_of_state eval_statement.
220
221definition make_initial_state : RTLabs_program → res (genv × state) ≝
222λp.
223  do ge ← globalenv Genv ?? p;
224  do m ← init_mem Genv ?? p;
225  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
226  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
227  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
228
229definition RTLabs_fullexec : fullexec io_out io_in ≝
230  mk_fullexec … RTLabs_exec ? make_initial_state.
231
Note: See TracBrowser for help on using the repository browser.