source: src/RTLabs/semantics.ma @ 1559

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

Add a notion of flat traces with evidence for RTLabs.

File size: 8.9 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; next_ok: present ?? (f_graph func) next
21; sp     : block
22; retdst : option register
23}.
24
25definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝
26λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f).
27
28inductive state : Type[0] ≝
29| State :
30   ∀   f : frame.
31   ∀  fs : list frame.
32   ∀   m : mem.
33   state
34| Callstate :
35   ∀  fd : fundef internal_function.
36   ∀args : list val.
37   ∀ dst : option register.
38   ∀ stk : list frame.
39   ∀   m : mem.
40   state
41| Returnstate :
42   ∀ rtv : option val.
43   ∀ dst : option register.
44   ∀ stk : list frame.
45   ∀   m : mem.
46   state.
47
48definition mem_of_state : state → mem ≝
49λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
50
51definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
52
53definition init_locals : list (register × typ) → register_env val ≝
54foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
55
56definition reg_store ≝
57λreg,v,locals.
58  update RegisterTag val locals reg v.
59
60axiom WrongNumberOfParameters : String.
61
62let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
63match rs with
64[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
65| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
66  let 〈r,ty〉 ≝ rt in
67  let locals' ≝ add RegisterTag val locals r v in
68  params_store rst vst locals'
69] ].
70
71axiom BadRegister : String.
72
73definition reg_retrieve : register_env ? → register → res val ≝
74λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
75
76axiom FailedOp : String.
77axiom MissingSymbol : String.
78
79axiom MissingStatement : String.
80axiom FailedConstant : String.
81axiom FailedLoad : String.
82axiom FailedStore : String.
83axiom BadFunction : String.
84axiom BadJumpTable : String.
85axiom BadJumpValue : String.
86axiom FinalState : String.
87axiom ReturnMismatch : String.
88
89definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
90λge,st.
91match st with
92[ State f fs m ⇒
93  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
94  match s return λs. labels_present ? s → ? with
95  [ St_skip l ⇒ λH. ret ? 〈E0, build_state f fs m l ?〉
96  | St_cost cl l ⇒ λH. ret ? 〈Echarge cl, build_state f fs m l ?〉
97  | St_const r cst l ⇒ λH.
98      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
99      ! locals ← reg_store r v (locals f);
100      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
101  | St_op1 _ _ op dst src l ⇒ λH.
102      ! v ← reg_retrieve (locals f) src;
103      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
104      ! locals ← reg_store dst v' (locals f);
105      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
106  | St_op2 op dst src1 src2 l ⇒ λH.
107      ! v1 ← reg_retrieve (locals f) src1;
108      ! v2 ← reg_retrieve (locals f) src2;
109      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
110      ! locals ← reg_store dst v' (locals f);
111      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
112  | St_load chunk addr dst l ⇒ λH.
113      ! vaddr ← reg_retrieve (locals f) addr;
114      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
115      ! locals ← reg_store dst v (locals f);
116      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
117  | St_store chunk addr src l ⇒ λH.
118      ! vaddr ← reg_retrieve (locals f) addr;
119      ! v ← reg_retrieve (locals f) src;
120      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
121      ret ? 〈E0, build_state f fs m' l ?〉
122  | St_call_id id args dst l ⇒ λH.
123      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
124      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
125      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
126      ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
127  | St_call_ptr frs args dst l ⇒ λH.
128      ! fv ← reg_retrieve (locals f) frs;
129      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
130      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
131      ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
132  | St_tailcall_id id args ⇒ λH.
133      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
134      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
135      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
136      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
137  | St_tailcall_ptr frs args ⇒ λH.
138      ! fv ← reg_retrieve (locals f) frs;
139      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
140      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
141      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
142
143  | St_cond src ltrue lfalse ⇒ λH.
144      ! v ← reg_retrieve (locals f) src;
145      ! b ← eval_bool_of_val v;
146      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
147
148  | St_jumptable r ls ⇒ λH.
149      ! v ← reg_retrieve (locals f) r;
150      match v with
151      [ Vint _ i ⇒
152          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
153          [ None ⇒ λ_. Wrong ??? (msg BadJumpTable)
154          | Some l ⇒ λE. ret ? 〈E0, build_state f fs m l ?〉
155          ] (refl ??)
156      | _ ⇒ Wrong ??? (msg BadJumpValue)
157      ]
158
159  | St_return ⇒ λH.
160      ! v ← match f_result (func f) with
161            [ None ⇒ ret ? (None ?)
162            | Some rt ⇒
163                let 〈r,ty〉 ≝ rt in
164                ! v ← reg_retrieve (locals f) r;
165                ret ? (Some ? v)
166            ];
167      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
168  ] (f_closed (func f) (next f) s ?)
169| Callstate fd params dst fs m ⇒
170    match fd with
171    [ Internal fn ⇒
172        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
173        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
174           here *)
175        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
176        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
177    | External fn ⇒
178        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
179        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
180        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
181    ]
182| Returnstate v dst fs m ⇒
183    match fs with
184    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
185    | cons f fs' ⇒
186        ! locals ← match dst with
187                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
188                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
189                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
190                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
191        ret ? 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
192    ]
193]. try @(next_ok f) try @lookup_lookup_present try @H
194[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
195| whd in H; @(All_nth … H ? E)
196| cases (f_entry fn) //
197] qed.
198
199definition RTLabs_is_final : state → option int ≝
200λs. match s with
201[ State _ _ _ ⇒ None ?
202| Callstate _ _ _ _ _ ⇒ None ?
203| Returnstate v _ fs _ ⇒
204    match fs with [ nil ⇒
205      match v with [ Some v' ⇒
206        match v' with
207        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
208        | _ ⇒ None ? ]
209      | None ⇒ None ? ]
210    | cons _ _ ⇒ None ? ]
211].
212
213definition RTLabs_exec : trans_system io_out io_in ≝
214  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
215
216definition make_global : RTLabs_program → genv ≝
217λp. globalenv Genv ?? (λx.[Init_space x]) p.
218
219definition make_initial_state : RTLabs_program → res state ≝
220λp.
221  let ge ≝ make_global p in
222  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
223  let main ≝ prog_main ?? p in
224  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
225  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
226  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
227
228definition RTLabs_fullexec : fullexec io_out io_in ≝
229  mk_fullexec … RTLabs_exec make_global make_initial_state.
230
Note: See TracBrowser for help on using the repository browser.