source: src/RTLabs/semantics.ma @ 1139

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 8.3 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        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
171           here *)
172        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
173        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
174    | External fn ⇒
175        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
176        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
177        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
178    ]
179| Returnstate v dst fs m ⇒
180    match fs with
181    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
182    | cons f fs' ⇒
183        ! locals ← match dst with
184                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
185                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
186                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
187                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
188        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
189    ]
190].
191
192definition is_final : state → option int ≝
193λs. match s with
194[ State _ _ _ ⇒ None ?
195| Callstate _ _ _ _ _ ⇒ None ?
196| Returnstate v _ fs _ ⇒
197    match fs with [ nil ⇒
198      match v with [ Some v' ⇒
199        match v' with
200        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
201        | _ ⇒ None ? ]
202      | None ⇒ None ? ]
203    | cons _ _ ⇒ None ? ]
204].
205
206definition RTLabs_exec : execstep io_out io_in ≝
207  mk_execstep … ? is_final mem_of_state eval_statement.
208
209definition make_initial_state : RTLabs_program → res (genv × state) ≝
210λp.
211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
212  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
213  let main ≝ prog_main ?? p in
214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
215  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
216  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
217
218definition RTLabs_fullexec : fullexec io_out io_in ≝
219  mk_fullexec … RTLabs_exec ? make_initial_state.
220
Note: See TracBrowser for help on using the repository browser.