source: Deliverables/D3.1/C-semantics/RTLabs/RTLabs-sem.ma @ 639

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

Preliminary work on RTLabs semantics
Will move to somewhere more appropriate soon.

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