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

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

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 11.1 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 | 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 : execstep ≝
290  mk_execstep … ? is_final mem_of_state eval_statement.
291
292definition make_initial_state : RTLabs_program → res (genv × state) ≝
293λp.
294  do ge ← globalenv Genv ?? p;
295  do m ← init_mem Genv ?? p;
296  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
297  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
298  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
299
300definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
301λp.
302  match make_initial_state p with
303  [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
304  | _ ⇒ e_wrong ???
305  ].
Note: See TracBrowser for help on using the repository browser.