source: src/RTLabs/semantics.ma @ 879

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

Refine "AST" types to include size/signedness information.

File size: 9.7 KB
RevLine 
[639]1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
[766]5include "utilities/lists.ma".
6
[702]7include "common/Errors.ma".
8include "common/Globalenvs.ma".
[731]9include "common/IO.ma".
[702]10include "common/SmallstepExec.ma".
[639]11
[762]12include "RTLabs/syntax.ma".
[751]13
[639]14definition genv ≝ (genv_t Genv) (fundef internal_function).
15
16record frame : Type[0] ≝
[693]17{ func   : internal_function
[750]18; locals : register_env val
[639]19; next   : label
20; sp     : block
[750]21; retdst : option register
[639]22}.
23
24definition adv : label → frame → frame ≝
[693]25λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f).
[639]26
27inductive state : Type[0] ≝
[693]28| State :
29   ∀   f : frame.
30   ∀  fs : list frame.
31   ∀   m : mem.
32   state
[639]33| Callstate :
34   ∀  fd : fundef internal_function.
35   ∀args : list val.
[750]36   ∀ dst : option register.
[639]37   ∀ stk : list frame.
38   ∀   m : mem.
39   state
40| Returnstate :
[765]41   ∀ rtv : option val.
[750]42   ∀ dst : option register.
[639]43   ∀ stk : list frame.
44   ∀   m : mem.
45   state.
46
[693]47definition mem_of_state : state → mem ≝
48λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
49
[639]50definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
51
[761]52definition init_locals : list register → register_env val ≝
53foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
54
[639]55definition reg_store ≝
[750]56λreg,v,locals.
[761]57  update RegisterTag val locals reg v.
[639]58
[797]59axiom WrongNumberOfParameters : String.
60
[750]61let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
[639]62match rs with
[797]63[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
64| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
[761]65  let locals' ≝ add RegisterTag val locals r v in
[639]66  params_store rst vst locals'
67] ].
68
[797]69axiom BadRegister : String.
70
[750]71definition reg_retrieve : register_env ? → register → res val ≝
[797]72λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
[639]73
[797]74axiom FailedOp : String.
75axiom MissingSymbol : String.
76
[639]77(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
78
[750]79definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
80λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
[639]81[ Aindexed i ⇒ λargs.
82    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
[797]83    opt_to_res … (msg FailedOp) (ev_addp v (Vint i))
[639]84| Aindexed2 ⇒ λargs.
85    do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
86    do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
[797]87    opt_to_res … (msg FailedOp) (ev_addp v1 v2)
[639]88| Aglobal id off ⇒ λargs.
[797]89    do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
[639]90    OK ? (Vptr Any loc ? (shift_offset zero_offset off))
91| Abased id off ⇒ λargs.
[797]92    do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
[639]93    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
[797]94    opt_to_res … (msg FailedOp) (ev_addp (Vptr Any loc ? zero_offset) v)
[639]95| Ainstack off ⇒ λargs.
96    OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
97]
98. /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
99
100
[797]101axiom MissingStatement : String.
102axiom FailedConstant : String.
103axiom FailedLoad : String.
104axiom FailedStore : String.
105axiom BadFunction : String.
106axiom BadJumpTable : String.
107axiom BadJumpValue : String.
108axiom FinalState : String.
109axiom ReturnMismatch : String.
[639]110
[693]111definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
112λge,st.
[639]113match st with
114[ State f fs m ⇒
[797]115  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (f_graph (func f)) (next f));
[639]116  match s with
117  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
118  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
[750]119  | St_const r cst l ⇒
[797]120      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
[750]121      ! locals ← reg_store r v (locals f);
[693]122      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
[639]123  | St_op1 op dst src l ⇒
124      ! v ← reg_retrieve (locals f) src;
[797]125      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
[639]126      ! locals ← reg_store dst v' (locals f);
[693]127      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
[639]128  | St_op2 op dst src1 src2 l ⇒
129      ! v1 ← reg_retrieve (locals f) src1;
130      ! v2 ← reg_retrieve (locals f) src2;
[797]131      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
[639]132      ! locals ← reg_store dst v' (locals f);
[693]133      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
[639]134  | St_load chunk mode args dst l ⇒
135      ! vaddr ← eval_addr ge f mode args;
[797]136      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
[639]137      ! locals ← reg_store dst v (locals f);
[693]138      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
[639]139  | St_store chunk mode args src l ⇒
140      ! vaddr ← eval_addr ge f mode args;
141      ! v ← reg_retrieve (locals f) src;
[797]142      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
[639]143      ret ? 〈E0, build_state f fs m' l〉
[816]144  | St_call_id id args dst l ⇒
[797]145      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
146      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
[639]147      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
148      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
[816]149  | St_call_ptr frs args dst l ⇒
[639]150      ! fv ← reg_retrieve (locals f) frs;
[797]151      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
[639]152      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
153      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
[816]154  | St_tailcall_id id args ⇒
[797]155      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
156      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
[639]157      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
158      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
[816]159  | St_tailcall_ptr frs args ⇒
[639]160      ! fv ← reg_retrieve (locals f) frs;
[797]161      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
[639]162      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
163      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
164
165  | St_condcst cst ltrue lfalse ⇒
[797]166      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
[751]167      ! b ← eval_bool_of_val v;
[639]168      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
169  | St_cond1 op src ltrue lfalse ⇒
170      ! v ← reg_retrieve (locals f) src;
[797]171      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
[751]172      ! b ← eval_bool_of_val v';
[639]173      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
174  | St_cond2 op src1 src2 ltrue lfalse ⇒
175      ! v1 ← reg_retrieve (locals f) src1;
176      ! v2 ← reg_retrieve (locals f) src2;
[797]177      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
[751]178      ! b ← eval_bool_of_val v';
[639]179      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
180
[750]181  | St_jumptable r ls ⇒
182      ! v ← reg_retrieve (locals f) r;
[639]183      match v with
184      [ Vint i ⇒
[797]185          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
[639]186          ret ? 〈E0, build_state f fs m l〉
[797]187      | _ ⇒ Wrong ??? (msg BadJumpValue)
[639]188      ]
189
[765]190  | St_return ⇒
191      ! v ← match f_result (func f) with
192            [ None ⇒ ret ? (None ?)
193            | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
194            ];
[639]195      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
196  ]
197| Callstate fd params dst fs m ⇒
198    match fd with
199    [ Internal fn ⇒
[761]200        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
[639]201        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
[693]202        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
[639]203    | External fn ⇒
204        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
[879]205        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
[765]206        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
[639]207    ]
208| Returnstate v dst fs m ⇒
209    match fs with
[797]210    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
[639]211    | cons f fs' ⇒
[765]212        ! locals ← match dst with
213                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
[797]214                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
215                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
[765]216                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
[727]217        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
[639]218    ]
219].
[693]220
221definition is_final : state → option int ≝
222λs. match s with
223[ State _ _ _ ⇒ None ?
224| Callstate _ _ _ _ _ ⇒ None ?
225| Returnstate v _ fs _ ⇒
[765]226    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
[693]227].
228
[731]229definition RTLabs_exec : execstep io_out io_in ≝
[702]230  mk_execstep … ? is_final mem_of_state eval_statement.
231
232definition make_initial_state : RTLabs_program → res (genv × state) ≝
233λp.
234  do ge ← globalenv Genv ?? p;
235  do m ← init_mem Genv ?? p;
[797]236  let main ≝ prog_main ?? p in
237  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
238  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
[750]239  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
[702]240
[731]241definition RTLabs_fullexec : fullexec io_out io_in ≝
242  mk_fullexec … RTLabs_exec ? make_initial_state.
243
Note: See TracBrowser for help on using the repository browser.