source: src/Clight/RTLabs/RTLabs-sem.ma @ 694

Last change on this file since 694 was 693, checked in by campbell, 10 years ago

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

File size: 10.6 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 "Values.ma".
8include "Errors.ma".
9include "Events.ma".
10include "Globalenvs.ma".
11include "IOMonad.ma".
12include "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 | 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 | ASTfloat ⇒ λv.EVfloat v ].
112
113definition mk_val: ∀ty:typ. eventval_type ty → val ≝
114λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
115
116lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
117  eventval_match (mk_eventval ty v) ty (mk_val ty v).
118#ty cases ty; normalize; //; qed.
119
120definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
121λev,ty.
122match ty with
123[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
124| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
125| _ ⇒ Error ?
126].
127
128definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
129λv,ty.
130match ty with
131[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
132| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
133| _ ⇒ Some ? (Error ?)
134].
135
136let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
137match vs with
138[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
139| cons v vt ⇒
140  match tys with
141  [ nil ⇒ Error ?
142  | cons ty tyt ⇒
143    do ev ← check_eventval' v ty;
144    do evt ← check_eventval_list vt tyt;
145    OK ? (ev::evt)
146  ]
147].
148
149(* IO monad *)
150
151(* Interactions are function calls that return a value and do not change
152   the rest of the Clight program's state. *)
153record io_out : Type[0] ≝
154{ io_function: ident
155; io_args: list eventval
156; io_in_typ: typ
157}.
158
159definition io_in ≝ λo. eventval_type (io_in_typ o).
160
161definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
162λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
163
164definition ret: ∀T. T → (IO io_out io_in T) ≝
165λT,x.(Value ?? T x).
166
167(* XXX above is from Cexec, should make common abstraction. *)
168
169(* XXX put somewhere sensible *)
170let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
171match l with
172[ nil ⇒ None ?
173| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
174].
175
176definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
177λge,st.
178match st with
179[ State f fs m ⇒
180  ! s ← graph_lookup ? (f_graph (func f)) (next f);
181  match s with
182  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
183  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
184  | St_const rs cst l ⇒
185      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
186      ! locals ← reg_store rs v (locals f);
187      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
188  | St_op1 op dst src l ⇒
189      ! v ← reg_retrieve (locals f) src;
190      ! v' ← opt_to_res … (eval_unop op v);
191      ! locals ← reg_store dst v' (locals f);
192      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
193  | St_op2 op dst src1 src2 l ⇒
194      ! v1 ← reg_retrieve (locals f) src1;
195      ! v2 ← reg_retrieve (locals f) src2;
196      ! v' ← opt_to_res … (eval_binop op v1 v2);
197      ! locals ← reg_store dst v' (locals f);
198      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
199  | St_load chunk mode args dst l ⇒
200      ! vaddr ← eval_addr ge f mode args;
201      ! v ← opt_to_res … (loadv chunk m vaddr);
202      ! locals ← reg_store dst v (locals f);
203      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
204  | St_store chunk mode args src l ⇒
205      ! vaddr ← eval_addr ge f mode args;
206      ! v ← reg_retrieve (locals f) src;
207      ! m' ← opt_to_res … (storev chunk m vaddr v);
208      ret ? 〈E0, build_state f fs m' l〉
209
210  | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
211      ! b ← opt_to_res … (find_symbol ?? ge id);
212      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
213      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
214      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
215  | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
216      ! fv ← reg_retrieve (locals f) frs;
217      ! fd ← opt_to_res … (find_funct ?? ge fv);
218      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
219      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
220  | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
221      ! b ← opt_to_res … (find_symbol ?? ge id);
222      ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
223      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
224      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
225  | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
226      ! fv ← reg_retrieve (locals f) frs;
227      ! fd ← opt_to_res … (find_funct ?? ge fv);
228      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
229      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
230
231  | St_condcst cst ltrue lfalse ⇒
232      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
233      ! b ← is_true_val v;
234      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
235  | St_cond1 op src ltrue lfalse ⇒
236      ! v ← reg_retrieve (locals f) src;
237      ! v' ← opt_to_res … (eval_unop op v);
238      ! b ← is_true_val v';
239      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
240  | St_cond2 op src1 src2 ltrue lfalse ⇒
241      ! v1 ← reg_retrieve (locals f) src1;
242      ! v2 ← reg_retrieve (locals f) src2;
243      ! v' ← opt_to_res … (eval_binop op v1 v2);
244      ! b ← is_true_val v';
245      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
246
247  | St_jumptable rs ls ⇒
248      ! v ← reg_retrieve (locals f) rs;
249      match v with
250      [ Vint i ⇒
251          ! l ← nth_opt ? (abs (unsigned i)) ls;
252          ret ? 〈E0, build_state f fs m l〉
253      | _ ⇒ Wrong ???
254      ]
255
256  | St_return src ⇒
257      ! v ← reg_retrieve (locals f) src;
258      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
259  ]
260| Callstate fd params dst fs m ⇒
261    match fd with
262    [ Internal fn ⇒
263        ! locals ← params_store (f_params fn) params (register_empty ?);
264        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
265        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
266    | External fn ⇒
267        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
268        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
269        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
270
271    ]
272| Returnstate v dst fs m ⇒
273    match fs with
274    [ nil ⇒ Error ? (* Already in final state *)
275    | cons f fs' ⇒
276        ! locals ← reg_store dst v (locals f);
277        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs m〉
278    ]
279].
280
281definition is_final : state → option int ≝
282λs. match s with
283[ State _ _ _ ⇒ None ?
284| Callstate _ _ _ _ _ ⇒ None ?
285| Returnstate v _ fs _ ⇒
286    match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
287].
288
289definition RTLabs_exec : RTLabs_program → execstep ≝
290λp. mk_execstep … ? is_final mem_of_state eval_statement.
Note: See TracBrowser for help on using the repository browser.