source: src/RTLabs/semantics.ma @ 888

Last change on this file since 888 was 888, checked in by campbell, 8 years ago

Use simplified conditionals in RTLabs, following the prototype.

File size: 8.1 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "utilities/lists.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12include "RTLabs/syntax.ma".
13
14definition genv ≝ (genv_t Genv) (fundef internal_function).
15
16record frame : Type[0] ≝
17{ func   : internal_function
18; locals : register_env val
19; next   : label
20; sp     : block
21; retdst : option register
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 : option register.
37   ∀ stk : list frame.
38   ∀   m : mem.
39   state
40| Returnstate :
41   ∀ rtv : option val.
42   ∀ dst : option register.
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 init_locals : list (register × typ) → register_env val ≝
53foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
54
55definition reg_store ≝
56λreg,v,locals.
57  update RegisterTag val locals reg v.
58
59axiom WrongNumberOfParameters : String.
60
61let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
62match rs with
63[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
64| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
65  let 〈r,ty〉 ≝ rt in
66  let locals' ≝ add RegisterTag val locals r v in
67  params_store rst vst locals'
68] ].
69
70axiom BadRegister : String.
71
72definition reg_retrieve : register_env ? → register → res val ≝
73λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
74
75axiom FailedOp : String.
76axiom MissingSymbol : String.
77
78axiom MissingStatement : String.
79axiom FailedConstant : String.
80axiom FailedLoad : String.
81axiom FailedStore : String.
82axiom BadFunction : String.
83axiom BadJumpTable : String.
84axiom BadJumpValue : String.
85axiom FinalState : String.
86axiom ReturnMismatch : String.
87
88definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
89λge,st.
90match st with
91[ State f fs m ⇒
92  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (f_graph (func f)) (next f));
93  match s with
94  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
95  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
96  | St_const r cst l ⇒
97      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
98      ! locals ← reg_store r v (locals f);
99      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
100  | St_op1 op dst src l ⇒
101      ! v ← reg_retrieve (locals f) src;
102      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
103      ! locals ← reg_store dst v' (locals f);
104      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
105  | St_op2 op dst src1 src2 l ⇒
106      ! v1 ← reg_retrieve (locals f) src1;
107      ! v2 ← reg_retrieve (locals f) src2;
108      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
109      ! locals ← reg_store dst v' (locals f);
110      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
111  | St_load chunk addr dst l ⇒
112      ! vaddr ← reg_retrieve (locals f) addr;
113      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
114      ! locals ← reg_store dst v (locals f);
115      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
116  | St_store chunk addr src l ⇒
117      ! vaddr ← reg_retrieve (locals f) addr;
118      ! v ← reg_retrieve (locals f) src;
119      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
120      ret ? 〈E0, build_state f fs m' l〉
121  | St_call_id id args dst l ⇒
122      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
123      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
124      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
125      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
126  | St_call_ptr frs args dst l ⇒
127      ! fv ← reg_retrieve (locals f) frs;
128      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
129      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
130      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
131  | St_tailcall_id id args ⇒
132      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
133      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
134      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
135      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
136  | St_tailcall_ptr frs args ⇒
137      ! fv ← reg_retrieve (locals f) frs;
138      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
139      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
140      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
141
142  | St_cond src ltrue lfalse ⇒
143      ! v ← reg_retrieve (locals f) src;
144      ! b ← eval_bool_of_val v;
145      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
146
147  | St_jumptable r ls ⇒
148      ! v ← reg_retrieve (locals f) r;
149      match v with
150      [ Vint i ⇒
151          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
152          ret ? 〈E0, build_state f fs m l〉
153      | _ ⇒ Wrong ??? (msg BadJumpValue)
154      ]
155
156  | St_return ⇒
157      ! v ← match f_result (func f) with
158            [ None ⇒ ret ? (None ?)
159            | Some rt ⇒
160                let 〈r,ty〉 ≝ rt in
161                ! v ← reg_retrieve (locals f) r;
162                ret ? (Some ? v)
163            ];
164      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
165  ]
166| Callstate fd params dst fs m ⇒
167    match fd with
168    [ Internal fn ⇒
169        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
170        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
171        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
172    | External fn ⇒
173        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
174        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
175        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
176    ]
177| Returnstate v dst fs m ⇒
178    match fs with
179    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
180    | cons f fs' ⇒
181        ! locals ← match dst with
182                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
183                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
184                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
185                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
186        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
187    ]
188].
189
190definition is_final : state → option int ≝
191λs. match s with
192[ State _ _ _ ⇒ None ?
193| Callstate _ _ _ _ _ ⇒ None ?
194| Returnstate v _ fs _ ⇒
195    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
196].
197
198definition RTLabs_exec : execstep io_out io_in ≝
199  mk_execstep … ? is_final mem_of_state eval_statement.
200
201definition make_initial_state : RTLabs_program → res (genv × state) ≝
202λp.
203  do ge ← globalenv Genv ?? p;
204  do m ← init_mem Genv ?? p;
205  let main ≝ prog_main ?? p in
206  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
207  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
208  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
209
210definition RTLabs_fullexec : fullexec io_out io_in ≝
211  mk_fullexec … RTLabs_exec ? make_initial_state.
212
Note: See TracBrowser for help on using the repository browser.