source: src/RTLabs/semantics.ma @ 774

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

Separate out the different forms of addition and subtraction in the frontend ops.

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