source: src/RTLabs/RTLabs-sem.ma @ 744

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

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 "RTLabs/RTLabs-syntax.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12definition genv ≝ (genv_t Genv) (fundef internal_function).
13
14record frame : Type[0] ≝
15{ func   : internal_function
16; locals : register_env split_val
17; next   : label
18; sp     : block
19; retdst : registers (* XXX: not optional? *)
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 : registers.
35   ∀ stk : list frame.
36   ∀   m : mem.
37   state
38| Returnstate :
39   ∀ rtv : val.
40   ∀ dst : registers.
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 reg_store ≝
51λrs,v,locals. match rs with [ dp n regs ⇒
52  do vs ← break n v;
53  OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
54].
55
56let rec params_store (rs:list registers) (vs:list val) (locals : register_env split_val) : res (register_env split_val) ≝
57match rs with
58[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
59| cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
60  do locals' ← reg_store r v locals;
61  params_store rst vst locals'
62] ].
63
64definition reg_retrieve : register_env ? → registers → res val ≝
65λlocals,rs. match rs with [ dp n regs ⇒
66  do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
67  merge n vs
68].
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 registers (addr_mode_args m) → res val ≝
73λge,f,m. match m return λm'.Vector registers (addr_mode_args m') → ? with
74[ Aindexed i ⇒ λargs.
75    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
76    opt_to_res … (ev_add 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_add 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_add (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
93definition is_true_val : val → res bool ≝
94λv. match v with
95[ Vint i ⇒ OK ? (notb (eq i zero))
96| Vnull _ ⇒ OK ? false
97| Vptr _ _ _ _ ⇒ OK ? true
98| _ ⇒ Error ?
99].
100
101
102(* XXX put somewhere sensible *)
103let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
104match l with
105[ nil ⇒ None ?
106| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
107].
108
109definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
110λge,st.
111match st with
112[ State f fs m ⇒
113  ! s ← lookup ?? (f_graph (func f)) (next f);
114  match s with
115  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
116  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
117  | St_const rs cst l ⇒
118      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
119      ! locals ← reg_store rs v (locals f);
120      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
121  | St_op1 op dst src l ⇒
122      ! v ← reg_retrieve (locals f) src;
123      ! v' ← opt_to_res … (eval_unop op v);
124      ! locals ← reg_store dst v' (locals f);
125      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
126  | St_op2 op dst src1 src2 l ⇒
127      ! v1 ← reg_retrieve (locals f) src1;
128      ! v2 ← reg_retrieve (locals f) src2;
129      ! v' ← opt_to_res … (eval_binop op v1 v2);
130      ! locals ← reg_store dst v' (locals f);
131      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
132  | St_load chunk mode args dst l ⇒
133      ! vaddr ← eval_addr ge f mode args;
134      ! v ← opt_to_res … (loadv chunk m vaddr);
135      ! locals ← reg_store dst v (locals f);
136      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
137  | St_store chunk mode args src l ⇒
138      ! vaddr ← eval_addr ge f mode args;
139      ! v ← reg_retrieve (locals f) src;
140      ! m' ← opt_to_res … (storev chunk m vaddr v);
141      ret ? 〈E0, build_state f fs m' l〉
142
143  | St_call_id id args dst sig l ⇒ (* 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 dst (adv l f::fs) m〉
148  | St_call_ptr frs args dst sig l ⇒  (* 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 dst (adv l f::fs) m〉
153  | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
154      ! b ← opt_to_res … (find_symbol ?? ge id);
155      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
156      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
157      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
158  | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
159      ! fv ← reg_retrieve (locals f) frs;
160      ! fd ← opt_to_res … (find_funct ?? ge fv);
161      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
162      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
163
164  | St_condcst cst ltrue lfalse ⇒
165      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
166      ! b ← is_true_val v;
167      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
168  | St_cond1 op src ltrue lfalse ⇒
169      ! v ← reg_retrieve (locals f) src;
170      ! v' ← opt_to_res … (eval_unop op v);
171      ! b ← is_true_val v';
172      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
173  | St_cond2 op src1 src2 ltrue lfalse ⇒
174      ! v1 ← reg_retrieve (locals f) src1;
175      ! v2 ← reg_retrieve (locals f) src2;
176      ! v' ← opt_to_res … (eval_binop op v1 v2);
177      ! b ← is_true_val v';
178      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
179
180  | St_jumptable rs ls ⇒
181      ! v ← reg_retrieve (locals f) rs;
182      match v with
183      [ Vint i ⇒
184          ! l ← nth_opt ? (nat_of_bitvector ? i) ls;
185          ret ? 〈E0, build_state f fs m l〉
186      | _ ⇒ Wrong ???
187      ]
188
189  | St_return src ⇒
190      ! v ← reg_retrieve (locals f) src;
191      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
192  ]
193| Callstate fd params dst fs m ⇒
194    match fd with
195    [ Internal fn ⇒
196        ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
197        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
198        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
199    | External fn ⇒
200        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
201        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
202        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
203
204    ]
205| Returnstate v dst fs m ⇒
206    match fs with
207    [ nil ⇒ Error ? (* Already in final state *)
208    | cons f fs' ⇒
209        ! locals ← reg_store dst v (locals f);
210        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
211    ]
212].
213
214definition is_final : state → option int ≝
215λs. match s with
216[ State _ _ _ ⇒ None ?
217| Callstate _ _ _ _ _ ⇒ None ?
218| Returnstate v _ fs _ ⇒
219    match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
220].
221
222definition RTLabs_exec : execstep io_out io_in ≝
223  mk_execstep … ? is_final mem_of_state eval_statement.
224
225definition make_initial_state : RTLabs_program → res (genv × state) ≝
226λp.
227  do ge ← globalenv Genv ?? p;
228  do m ← init_mem Genv ?? p;
229  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
230  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
231  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
232
233definition RTLabs_fullexec : fullexec io_out io_in ≝
234  mk_fullexec … RTLabs_exec ? make_initial_state.
235
Note: See TracBrowser for help on using the repository browser.