source: src/RTL/semantics.ma @ 1257

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

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File size: 11.6 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: external functions never fail (??) and always return something of the
15   size of one register, both in the frontend and in the backend.
16   Is this reasonable??? In OCaml it always return a list, but in the frontend
17   only the head is kept (or Undef if the list is empty) ??? *)
18
19(* CSC: carries are values and booleans are not values; so we use integers.
20   But why using values at all? To have undef? *)
21(* CSC: ???????????? *)
22axiom smerge: val → val → res val.
23(* CSC: ???????????? In OCaml: IntValue.Int32.merge
24   Note also that the translation can fail; so it should be a res int! *)
25axiom smerge2: list val → int.
26(* CSC: I have a byte, I need a value, but it is complex to do so *)
27axiom val_of_Byte: Byte → val.
28axiom Byte_of_val: val → res Byte.
29(* Map from the front-end memory model to the back-end memory model *)
30axiom represent_block: block → val × val.
31(* CSC: fixed size chunk *)
32axiom chunk: memory_chunk.
33
34definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
35
36(* CSC: added carry *)
37record frame : Type[0] ≝
38{ func   : rtl_internal_function
39; locals : register_env val
40; next   : label
41; sp     : block
42; retdst : list register
43; carry  : val
44}.
45
46(* CSC: added carry *)
47definition adv : label → frame → frame ≝
48λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
49
50inductive state : Type[0] ≝
51| State :
52   ∀   f : frame.
53   ∀  fs : list frame.
54   ∀   m : mem.
55   state
56| Callstate :
57   ∀  fd : fundef rtl_internal_function.
58   ∀args : list val.
59   ∀ dst : list register. (* CSC: changed from option to list *)
60   ∀ stk : list frame.
61   ∀   m : mem.
62   state
63| Returnstate :
64   (* CSC: the two lists should have the same length, but this is
65      enforced only by the semantics *)
66   ∀ rtv : list val. (* CSC: changed from option to list *)
67   ∀ dst : list register. (* CSC: changed from option to list *)
68   ∀ stk : list frame.
69   ∀   m : mem.
70   state.
71
72definition mem_of_state : state → mem ≝
73λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
74
75definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
76
77(* CSC: modified to take in input a list of registers (untyped) *)
78definition init_locals : list register → register_env val ≝
79foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
80
81definition reg_store ≝
82λreg,v,locals.
83  update RegisterTag val locals reg v.
84
85axiom WrongNumberOfParameters : String.
86
87(* CSC: modified to take in input a list of registers (untyped) *)
88let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
89match rs with
90[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
91| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
92  let locals' ≝ add RegisterTag val locals r v in
93  params_store rst vst locals'
94] ].
95
96axiom BadRegister : String.
97
98definition reg_retrieve : register_env ? → register → res val ≝
99λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
100
101axiom FailedOp : String.
102axiom MissingSymbol : String.
103
104axiom MissingStatement : String.
105axiom FailedConstant : String.
106axiom FailedLoad : String.
107axiom FailedStore : String.
108axiom BadFunction : String.
109axiom BadJumpTable : String.
110axiom BadJumpValue : String.
111axiom FinalState : String.
112axiom ReturnMismatch : String.
113
114definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
115λge,st.
116match st with
117[ State f fs m ⇒
118  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
119  match s with
120  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
121  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
122  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
123      ! vaddrh ← reg_retrieve (locals f) addrh;
124      ! vaddrl ← reg_retrieve (locals f) addrl;
125      ! vaddr ← smerge vaddrl vaddrh;
126      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
127      ! locals ← reg_store dst v (locals f);
128      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
129  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
130      ! vaddrh ← reg_retrieve (locals f) addrh;
131      ! vaddrl ← reg_retrieve (locals f) addrl;
132      ! vaddr ← smerge vaddrl vaddrh;
133      ! v ← reg_retrieve (locals f) src;
134      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
135      ret ? 〈E0, build_state f fs m' l〉
136  | rtl_st_call_id id args dst l ⇒
137      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
138      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
139      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
140      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
141  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
142      ! hfv ← reg_retrieve (locals f) hfrs;
143      ! lfv ← reg_retrieve (locals f) lfrs;
144      ! fv  ← smerge lfv hfv;
145      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
146      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
147      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
148  | rtl_st_tailcall_id id args ⇒
149      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
150      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
151      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
152      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
153  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
154      ! hfv ← reg_retrieve (locals f) hfrs;
155      ! lfv ← reg_retrieve (locals f) lfrs;
156      ! fv  ← smerge lfv hfv;
157      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
158      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
159      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
160  | rtl_st_return ⇒
161      (* CSC: rtl_if_result/f_result; list vs option *)
162      let dest ≝ rtl_if_result (func f) in
163      ! v ←  mmap … (reg_retrieve (locals f)) dest;
164      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
165  | rtl_st_cond src ltrue lfalse ⇒
166      ! v ← reg_retrieve (locals f) src;
167      ! b ← eval_bool_of_val v;
168      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
169  (* CSC: mismatch between the memory models and failures for the next two opx *)
170  | rtl_st_op1 op dst src l ⇒
171     ! v ← reg_retrieve (locals f) src;
172     ! v ← Byte_of_val v;
173     let v' ≝ val_of_Byte (op1 eval op v) in
174     ! locals ← reg_store dst v' (locals f);
175     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
176  | rtl_st_op2 op dst src1 src2 l ⇒
177     ! v1 ← reg_retrieve (locals f) src1;
178     ! v1 ← Byte_of_val v1;
179     ! v2 ← reg_retrieve (locals f) src2;
180     ! v2 ← Byte_of_val v2;
181     ! carry ← eval_bool_of_val (carry f);
182     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
183     let v' ≝ val_of_Byte v' in
184     let carry ≝ of_bool carry in
185     ! locals ← reg_store dst v' (locals f);
186     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
187
188  (* CSC: Removed: St_jumptable *)
189  (* CSC: Added: *)
190 
191  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
192  | rtl_st_addr ldest hdest id l ⇒
193     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
194     let 〈laddr,haddr〉 ≝ represent_block addr in
195     ! locals ← reg_store ldest laddr (locals f);
196     ! locals ← reg_store hdest haddr locals;
197     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
198  | rtl_st_stack_addr ldest hdest l ⇒
199     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
200     ! locals ← reg_store ldest laddr (locals f);
201     ! locals ← reg_store hdest haddr locals;
202     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
203  | rtl_st_int dest v l ⇒
204     ! locals ← reg_store dest (val_of_Byte v) (locals f);
205     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
206
207  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
208  | rtl_st_move dst src l ⇒
209     ! v ← reg_retrieve (locals f) src;
210     ! locals ← reg_store dst v (locals f);
211     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
212  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
213  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
214     ! v1 ← reg_retrieve (locals f) sacc;
215     ! v1 ← Byte_of_val v1;
216     ! v2 ← reg_retrieve (locals f) sbacc;
217     ! v2 ← Byte_of_val v2;
218     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
219     let v1' ≝ val_of_Byte v1' in
220     let v2' ≝ val_of_Byte v2' in
221     ! locals ← reg_store dacc v1' (locals f);
222     ! locals ← reg_store dbacc v2' locals;
223     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
224 
225  | rtl_st_clear_carry l ⇒
226    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
227  | rtl_st_set_carry l ⇒
228    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
229  ]
230| Callstate fd params dst fs m ⇒
231    match fd with
232    [ Internal fn ⇒
233        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
234        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
235        (* CSC: added carry *)
236        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
237    | External fn ⇒
238        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
239        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
240        (* CSC: return type changed from option to list *)
241        (* CSC: XXX bug here; I think I should split it into Byte-long
242           components; instead I am making a singleton out of it *)
243        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
244    ]
245| Returnstate v dst fs m ⇒
246    match fs with
247    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
248    | cons f fs' ⇒
249       ! locals ←
250         mfold_left2 ???
251          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
252        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
253    ]
254].
255
256axiom WrongReturnValueType: String.
257
258definition is_final : state → option ((*CSC: why not res*) int) ≝
259λs. match s with
260[ State _ _ _ ⇒ None ?
261| Callstate _ _ _ _ _ ⇒ None ?
262| Returnstate v _ fs _ ⇒
263    match fs with
264     [ nil ⇒ Some ? (smerge2 v)
265     | _ ⇒ None ? ]].
266(*
267definition RTL_exec : execstep io_out io_in ≝
268  mk_execstep … ? is_final mem_of_state eval_statement.
269*)
270(* CSC: XXX the program type does not fit with the globalenv and init_mem
271definition make_initial_state : rtl_program → res (genv × state) ≝
272λp.
273  do ge ← globalenv Genv ?? p;
274  do m ← init_mem Genv ?? p;
275  let main ≝ rtl_pr_main ?? p in
276  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
277  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
278  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
279
280definition RTL_fullexec : fullexec io_out io_in ≝
281  mk_fullexec … RTL_exec ? make_initial_state.
282*)
Note: See TracBrowser for help on using the repository browser.