source: src/RTL/semantics.ma @ 1300

Last change on this file since 1300 was 1300, checked in by sacerdot, 8 years ago

More (graph) axioms implemented. Look at the comments marked with XXX for
potential problems in the proof of preservation of the semantics.

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