source: src/RTL/semantics.ma @ 1114

Last change on this file since 1114 was 1114, checked in by sacerdot, 9 years ago

some more operations implemented

File size: 9.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 "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
13
14(* CSC: carries are values and booleans are not values; so we use integers.
15   But why using values at all? To have undef? *)
16(* CSC: ???????????? *)
17axiom smerge: val → val → res val.
18(* CSC: fixed size chunk *)
19axiom chunk: memory_chunk.
20
21definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
22
23(* CSC: added carry *)
24record frame : Type[0] ≝
25{ func   : rtl_internal_function
26; locals : register_env val
27; next   : label
28; sp     : block
29; retdst : list register
30; carry  : val
31}.
32
33(* CSC: added carry *)
34definition adv : label → frame → frame ≝
35λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
36
37inductive state : Type[0] ≝
38| State :
39   ∀   f : frame.
40   ∀  fs : list frame.
41   ∀   m : mem.
42   state
43| Callstate :
44   ∀  fd : fundef rtl_internal_function.
45   ∀args : list val.
46   ∀ dst : list register. (* CSC: changed from option to list *)
47   ∀ stk : list frame.
48   ∀   m : mem.
49   state
50| Returnstate :
51   ∀ rtv : list val. (* CSC: changed from option to list *)
52   ∀ dst : list register. (* CSC: changed from option to list *)
53   ∀ stk : list frame.
54   ∀   m : mem.
55   state.
56
57definition mem_of_state : state → mem ≝
58λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
59
60definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
61
62definition init_locals : list (register × typ) → register_env val ≝
63foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
64
65definition reg_store ≝
66λreg,v,locals.
67  update RegisterTag val locals reg v.
68
69axiom WrongNumberOfParameters : String.
70
71let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
72match rs with
73[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
74| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
75  let 〈r,ty〉 ≝ rt in
76  let locals' ≝ add RegisterTag val locals r v in
77  params_store rst vst locals'
78] ].
79
80axiom BadRegister : String.
81
82definition reg_retrieve : register_env ? → register → res val ≝
83λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
84
85axiom FailedOp : String.
86axiom MissingSymbol : String.
87
88axiom MissingStatement : String.
89axiom FailedConstant : String.
90axiom FailedLoad : String.
91axiom FailedStore : String.
92axiom BadFunction : String.
93axiom BadJumpTable : String.
94axiom BadJumpValue : String.
95axiom FinalState : String.
96axiom ReturnMismatch : String.
97
98definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
99λge,st.
100match st with
101[ State f fs m ⇒
102  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
103  match s with
104  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
105  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
106  | rtl_st_load addrh addrl dst l ⇒  (* CSC: pairs of regs vs reg *)
107      ! vaddrh ← reg_retrieve (locals f) addrh;
108      ! vaddrl ← reg_retrieve (locals f) addrl;
109      ! vaddr ← smerge vaddrh vaddrl;
110      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
111      ! locals ← reg_store dst v (locals f);
112      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
113  | rtl_st_store addrh addrl src l ⇒  (* CSC: pairs of regs vs reg *)
114      ! vaddrh ← reg_retrieve (locals f) addrh;
115      ! vaddrl ← reg_retrieve (locals f) addrl;
116      ! vaddr ← smerge vaddrh vaddrl;
117      ! v ← reg_retrieve (locals f) src;
118      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
119      ret ? 〈E0, build_state f fs m' l〉
120  | rtl_st_call_id id args dst l ⇒
121      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
122      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
123      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
124      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
125  | rtl_st_call_ptr hfrs lfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
126      ! hfv ← reg_retrieve (locals f) hfrs;
127      ! lfv ← reg_retrieve (locals f) lfrs;
128      ! fv  ← smerge hfv lfv;
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  | rtl_st_tailcall_id id args ⇒
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  | rtl_st_tailcall_ptr hfrs lfrs args ⇒ (* CSC: pairs of regs vs reg *)
138      ! hfv ← reg_retrieve (locals f) hfrs;
139      ! lfv ← reg_retrieve (locals f) lfrs;
140      ! fv  ← smerge hfv lfv;
141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
142      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
143      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
144  | rtl_st_return ⇒
145      (* CSC: rtl_if_result/f_result; list vs option *)
146      let dest ≝ rtl_if_result (func f) in
147      ! v ←  mmap … (reg_retrieve (locals f)) dest;
148      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
149  | rtl_st_cond src ltrue lfalse ⇒
150      ! v ← reg_retrieve (locals f) src;
151      ! b ← eval_bool_of_val v;
152      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
153
154  (*
155  | St_const r cst l ⇒
156      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
157      ! locals ← reg_store r v (locals f);
158      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
159  | St_op1 op dst src l ⇒
160      ! v ← reg_retrieve (locals f) src;
161      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
162      ! locals ← reg_store dst v' (locals f);
163      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
164  | St_op2 op dst src1 src2 l ⇒
165      ! v1 ← reg_retrieve (locals f) src1;
166      ! v2 ← reg_retrieve (locals f) src2;
167      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
168      ! locals ← reg_store dst v' (locals f);
169      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
170  (* CSC: Removed: St_jumptable *)
171  (* CSC: Added: *)
172  | rtl_st_clear_carry l ⇒
173    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
174  | rtl_st_set_carry l ⇒
175    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
176  | _ ⇒ ? ] (*
177  ] *)
178| Callstate fd params dst fs m ⇒ ? (* CSC: XXXXXXXXXXXX
179    match fd with
180    [ Internal fn ⇒
181        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
182        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
183        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst Vundef) fs m'〉
184    | External fn ⇒
185        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
186        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
187        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
188    ] *)
189| Returnstate v dst fs m ⇒ ? (* CSC: XXXXXXXXXXXXXXXXXX
190    match fs with
191    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
192    | cons f fs' ⇒
193        ! locals ← match dst with
194                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
195                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
196                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
197                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
198        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
199    ] *)
200].
201
202definition is_final : state → option int ≝
203λs. match s with
204[ State _ _ _ ⇒ None ?
205| Callstate _ _ _ _ _ ⇒ None ?
206| Returnstate v _ fs _ ⇒
207    match fs with [ nil ⇒
208      match v with [ Some v' ⇒
209        match v' with
210        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
211        | _ ⇒ None ? ]
212      | None ⇒ None ? ]
213    | cons _ _ ⇒ None ? ]
214].
215
216definition RTLabs_exec : execstep io_out io_in ≝
217  mk_execstep … ? is_final mem_of_state eval_statement.
218
219definition make_initial_state : RTLabs_program → res (genv × state) ≝
220λp.
221  do ge ← globalenv Genv ?? p;
222  do m ← init_mem Genv ?? 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 ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
227
228definition RTLabs_fullexec : fullexec io_out io_in ≝
229  mk_fullexec … RTLabs_exec ? make_initial_state.
230
Note: See TracBrowser for help on using the repository browser.