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

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

Enough fixes to let an RTLabs program run.

File size: 11.2 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/Values.ma".
8include "common/Errors.ma".
9include "common/Events.ma".
10include "common/Globalenvs.ma".
11include "common/IOMonad.ma".
12include "common/SmallstepExec.ma".
13
14definition genv ≝ (genv_t Genv) (fundef internal_function).
15
16record frame : Type[0] ≝
17{ func   : internal_function
18; locals : register_env split_val
19; next   : label
20; sp     : block
21; retdst : registers (* XXX: not optional? *)
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 : registers.
37   ∀ stk : list frame.
38   ∀   m : mem.
39   state
40| Returnstate :
41   ∀ rtv : val.
42   ∀ dst : registers.
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 reg_store ≝
53λrs,v,locals. match rs with [ dp n regs ⇒
54  do vs ← break n v;
55  OK ? (fold_right2_i ??? (λ_. register_update split_val) locals n regs vs)
56].
57
58let rec params_store (rs:list registers) (vs:list val) (locals : register_env split_val) : res (register_env split_val) ≝
59match rs with
60[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
61| cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
62  do locals' ← reg_store r v locals;
63  params_store rst vst locals'
64] ].
65
66definition reg_retrieve : register_env ? → registers → res val ≝
67λlocals,rs. match rs with [ dp n regs ⇒
68  do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (register_lookup ? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
69  merge n vs
70].
71
72(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
73
74definition eval_addr : genv → frame → ∀m:addressing. Vector registers (addr_mode_args m) → res val ≝
75λge,f,m. match m return λm'.Vector registers (addr_mode_args m') → ? with
76[ Aindexed i ⇒ λargs.
77    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
78    opt_to_res … (ev_add v (Vint i))
79| Aindexed2 ⇒ λargs.
80    do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
81    do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
82    opt_to_res … (ev_add v1 v2)
83| Aglobal id off ⇒ λargs.
84    do loc ← opt_to_res … (find_symbol ?? ge id);
85    OK ? (Vptr Any loc ? (shift_offset zero_offset off))
86| Abased id off ⇒ λargs.
87    do loc ← opt_to_res … (find_symbol ?? ge id);
88    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
89    opt_to_res … (ev_add (Vptr Any loc ? zero_offset) v)
90| Ainstack off ⇒ λargs.
91    OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
92]
93. /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
94
95definition is_true_val : val → res bool ≝
96λv. match v with
97[ Vint i ⇒ OK ? (notb (eq i zero))
98| Vnull _ ⇒ OK ? false
99| Vptr _ _ _ _ ⇒ OK ? true
100| _ ⇒ Error ?
101].
102
103(* XXX below is from Cexec, should have common abstraction. *)
104
105(* Checking types of values given to / received from an external function call. *)
106
107definition eventval_type : ∀ty:typ. Type[0] ≝
108λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
109
110definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
111λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
112*; qed.
113
114definition mk_val: ∀ty:typ. eventval_type ty → val ≝
115λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
116*; qed.
117
118lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
119  eventval_match (mk_eventval ty v) ty (mk_val ty v).
120#ty cases ty; normalize; //; * *; qed.
121
122definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
123λev,ty.
124match ty with
125[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
126| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
127| _ ⇒ Error ?
128].
129
130definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
131λv,ty.
132match ty with
133[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
134| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
135| _ ⇒ Error ?
136].
137
138let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
139match vs with
140[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
141| cons v vt ⇒
142  match tys with
143  [ nil ⇒ Error ?
144  | cons ty tyt ⇒
145    do ev ← check_eventval' v ty;
146    do evt ← check_eventval_list vt tyt;
147    OK ? (ev::evt)
148  ]
149].
150
151(* IO monad *)
152
153(* Interactions are function calls that return a value and do not change
154   the rest of the Clight program's state. *)
155record io_out : Type[0] ≝
156{ io_function: ident
157; io_args: list eventval
158; io_in_typ: typ
159}.
160
161definition io_in ≝ λo. eventval_type (io_in_typ o).
162
163definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
164λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
165
166definition ret: ∀T. T → (IO io_out io_in T) ≝
167λT,x.(Value ?? T x).
168
169(* XXX above is from Cexec, should make common abstraction. *)
170
171(* XXX put somewhere sensible *)
172let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
173match l with
174[ nil ⇒ None ?
175| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
176].
177
178definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
179λge,st.
180match st with
181[ State f fs m ⇒
182  ! s ← graph_lookup ? (f_graph (func f)) (next f);
183  match s with
184  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
185  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
186  | St_const rs cst l ⇒
187      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
188      ! locals ← reg_store rs v (locals f);
189      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
190  | St_op1 op dst src l ⇒
191      ! v ← reg_retrieve (locals f) src;
192      ! v' ← opt_to_res … (eval_unop op v);
193      ! locals ← reg_store dst v' (locals f);
194      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
195  | St_op2 op dst src1 src2 l ⇒
196      ! v1 ← reg_retrieve (locals f) src1;
197      ! v2 ← reg_retrieve (locals f) src2;
198      ! v' ← opt_to_res … (eval_binop op v1 v2);
199      ! locals ← reg_store dst v' (locals f);
200      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
201  | St_load chunk mode args dst l ⇒
202      ! vaddr ← eval_addr ge f mode args;
203      ! v ← opt_to_res … (loadv chunk m vaddr);
204      ! locals ← reg_store dst v (locals f);
205      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
206  | St_store chunk mode args src l ⇒
207      ! vaddr ← eval_addr ge f mode args;
208      ! v ← reg_retrieve (locals f) src;
209      ! m' ← opt_to_res … (storev chunk m vaddr v);
210      ret ? 〈E0, build_state f fs m' l〉
211
212  | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
213      ! b ← opt_to_res … (find_symbol ?? ge id);
214      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
215      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
216      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
217  | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
218      ! fv ← reg_retrieve (locals f) frs;
219      ! fd ← opt_to_res … (find_funct ?? ge fv);
220      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
221      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
222  | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
223      ! b ← opt_to_res … (find_symbol ?? ge id);
224      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
225      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
226      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
227  | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
228      ! fv ← reg_retrieve (locals f) frs;
229      ! fd ← opt_to_res … (find_funct ?? ge fv);
230      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
231      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
232
233  | St_condcst cst ltrue lfalse ⇒
234      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
235      ! b ← is_true_val v;
236      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
237  | St_cond1 op src ltrue lfalse ⇒
238      ! v ← reg_retrieve (locals f) src;
239      ! v' ← opt_to_res … (eval_unop op v);
240      ! b ← is_true_val v';
241      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
242  | St_cond2 op src1 src2 ltrue lfalse ⇒
243      ! v1 ← reg_retrieve (locals f) src1;
244      ! v2 ← reg_retrieve (locals f) src2;
245      ! v' ← opt_to_res … (eval_binop op v1 v2);
246      ! b ← is_true_val v';
247      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
248
249  | St_jumptable rs ls ⇒
250      ! v ← reg_retrieve (locals f) rs;
251      match v with
252      [ Vint i ⇒
253          ! l ← nth_opt ? (abs (unsigned i)) ls;
254          ret ? 〈E0, build_state f fs m l〉
255      | _ ⇒ Wrong ???
256      ]
257
258  | St_return src ⇒
259      ! v ← reg_retrieve (locals f) src;
260      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
261  ]
262| Callstate fd params dst fs m ⇒
263    match fd with
264    [ Internal fn ⇒
265        ! locals ← params_store (f_params fn) params (register_empty ?);
266        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
267        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
268    | External fn ⇒
269        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
270        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
271        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
272
273    ]
274| Returnstate v dst fs m ⇒
275    match fs with
276    [ nil ⇒ Error ? (* Already in final state *)
277    | cons f fs' ⇒
278        ! locals ← reg_store dst v (locals f);
279        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
280    ]
281].
282
283definition is_final : state → option int ≝
284λs. match s with
285[ State _ _ _ ⇒ None ?
286| Callstate _ _ _ _ _ ⇒ None ?
287| Returnstate v _ fs _ ⇒
288    match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
289].
290
291definition RTLabs_exec : execstep ≝
292  mk_execstep … ? is_final mem_of_state eval_statement.
293
294definition make_initial_state : RTLabs_program → res (genv × state) ≝
295λp.
296  do ge ← globalenv Genv ?? p;
297  do m ← init_mem Genv ?? p;
298  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
299  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
300  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
301
302definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
303λp.
304  match make_initial_state p with
305  [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
306  | _ ⇒ e_wrong ???
307  ].
Note: See TracBrowser for help on using the repository browser.