Changeset 1197 for Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma
- Timestamp:
- Sep 7, 2011, 12:10:27 PM (10 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1151-1152,1154-1183,1185-1188,1191-1196
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma
r1153 r1197 21 21 (* CSC: ???????????? *) 22 22 axiom smerge: val → val → res val. 23 (*24 23 (* CSC: ???????????? In OCaml: IntValue.Int32.merge 25 24 Note also that the translation can fail; so it should be a res int! *) 26 25 axiom smerge2: list val → int. 27 *)28 26 (* CSC: I have a byte, I need a value, but it is complex to do so *) 29 27 axiom val_of_Byte: Byte → val. 30 28 axiom Byte_of_val: val → res Byte. 29 axiom val_of_nat: nat → val. 31 30 (* Map from the front-end memory model to the back-end memory model *) 32 31 axiom represent_block: block → val × val. … … 38 37 axiom val_of_address: address → val. (* CSC: only to shift the sp *) 39 38 axiom address_of_val: val → address. (* CSC: only to shift the sp *) 39 axiom addr_sub: address → nat → address. 40 axiom addr_add: address → nat → address. 40 41 (* CSC: ??? *) 41 42 axiom address_of_label: mem → label → address. … … 43 44 axiom label_of_address_chunks: Byte → Byte → label. 44 45 axiom address_of_address_chunks: Byte → Byte → address. 46 axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *) 45 47 axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *) 46 48 axiom hwreg_retrieve : mRegisterMap → Register → res val. 47 49 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap. 48 50 49 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).51 definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)). 50 52 51 53 (* CSC: frame reduced to this *) 52 54 definition frame: Type[0] ≝ register_env val. 53 55 56 (* CSC: exit not put in the state, like in OCaml. It is constant througout 57 execution *) 54 58 record state : Type[0] ≝ 55 59 { st_frms: list frame 56 60 ; pc: address 57 61 ; sp: address 58 (* ; exit: address *)59 62 ; locals: register_env val 60 63 ; carry: val … … 134 137 135 138 (*CSC: To be implemented *) 136 axiom fetch_statement: state → res ertl_statement. 139 140 axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals). 141 axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals). 137 142 138 143 definition init_locals : list register → register_env val ≝ … … 142 147 λreg,v,locals. update RegisterTag val locals reg v. 143 148 144 (*145 axiom WrongNumberOfParameters : String.146 147 (* CSC: modified to take in input a list of registers (untyped) *)148 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝149 match rs with150 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]151 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒152 let locals' ≝ add RegisterTag val locals r v in153 params_store rst vst locals'154 ] ].155 *)156 157 149 axiom BadRegister : String. 158 150 … … 160 152 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg). 161 153 162 (*163 axiom FailedOp : String.164 *)165 154 axiom MissingSymbol : String. 166 (*167 axiom MissingStatement : String.168 axiom FailedConstant : String. *)169 155 axiom FailedLoad : String. 170 156 axiom BadFunction : String. 171 (*axiom BadJumpTable : String.172 axiom BadJumpValue : String.173 axiom FinalState : String.174 axiom ReturnMismatch : String.175 *)176 157 177 158 (*CSC: to be implemented *) … … 200 181 (λregs.OK ? (set_regs regs st)). 201 182 202 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝ 203 λge,st. 204 ! s ← fetch_statement st; 183 definition fetch_result: state → nat → res (list val) ≝ 184 λst,registersno. 185 let retregs ≝ prefix … registersno RegisterRets in 186 mmap … (λr. hwreg_retrieve (regs st) r) retregs. 187 188 definition framesize: list ident → state → res nat ≝ 189 λglobals: list ident. 190 λst. 191 (* CSC: monadic notation missing here *) 192 bind ?? (fetch_function globals st) (λf. 193 OK ? (ertl_if_stacksize globals f)). 194 195 definition get_hwsp : state → res address ≝ 196 λst. 197 (* CSC: monadic notation missing here *) 198 bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl. 199 (* CSC: monadic notation missing here *) 200 bind ?? (Byte_of_val spl) (λspl. 201 (* CSC: monadic notation missing here *) 202 bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph. 203 (* CSC: monadic notation missing here *) 204 bind ?? (Byte_of_val sph) (λsph. 205 OK ? (address_of_address_chunks spl sph))))). 206 207 definition set_hwsp : address → state → res state ≝ 208 λsp,st. 209 let 〈spl,sph〉 ≝ address_chunks_of_address sp in 210 (* CSC: monadic notation missing here *) 211 bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs. 212 (* CSC: monadic notation missing here *) 213 bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs. 214 OK ? (set_regs regs st))). 215 216 definition retrieve: state → move_registers → res val ≝ 217 λst. 218 λr. 219 match r with 220 [ pseudo src ⇒ reg_retrieve (locals st) src 221 | hardware src ⇒ hwreg_retrieve (regs st) src 222 ]. 223 224 definition store ≝ 225 λst. 226 λv. 227 λr. 228 match r with 229 [ pseudo dst ⇒ 230 ! locals ← reg_store dst v (locals st); 231 ret ? (set_locals locals st) 232 | hardware dst ⇒ 233 ! regs ← hwreg_store dst v (regs st); 234 ret ? (set_regs regs st) 235 ]. 236 237 definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝ 238 λglobals. λge,st. 239 ! s ← fetch_statement globals st; 205 240 match s with 206 [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉 207 | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉 208 | ertl_st_int dest v l ⇒ 209 ! locals ← reg_store dest (val_of_Byte v) (locals st); 210 ret ? 〈E0, goto l (set_locals locals st)〉 211 | ertl_st_load addrl addrh dst l ⇒ 212 ! vaddrh ← reg_retrieve (locals st) addrh; 213 ! vaddrl ← reg_retrieve (locals st) addrl; 214 ! vaddr ← smerge vaddrl vaddrh; 215 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr); 216 ! locals ← reg_store dst v (locals st); 241 [ ertl_st_lift_pre pre ⇒ 242 match pre with 243 [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉 244 | joint_st_sequential seq l ⇒ 245 match seq with 246 [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉 247 | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉 248 | joint_instr_int dest v ⇒ 249 ! locals ← reg_store dest (val_of_Byte v) (locals st); 250 ret ? 〈E0, goto l (set_locals locals st)〉 251 | joint_instr_load addrl addrh dst ⇒ 252 ! vaddrh ← reg_retrieve (locals st) addrh; 253 ! vaddrl ← reg_retrieve (locals st) addrl; 254 ! vaddr ← smerge vaddrl vaddrh; 255 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr); 256 ! locals ← reg_store dst v (locals st); 257 ret ? 〈E0, goto l (set_locals locals st)〉 258 | joint_instr_store addrl addrh src ⇒ 259 ! vaddrh ← reg_retrieve (locals st) addrh; 260 ! vaddrl ← reg_retrieve (locals st) addrl; 261 ! vaddr ← smerge vaddrl vaddrh; 262 ! v ← reg_retrieve (locals st) src; 263 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v); 264 ret ? 〈E0, goto l (set_m m' st)〉 265 | joint_instr_cond src ltrue ⇒ 266 ! v ← reg_retrieve (locals st) src; 267 ! b ← eval_bool_of_val v; 268 ret ? 〈E0, goto (if b then ltrue else l) st〉 269 | joint_instr_address ident prf ldest hdest ⇒ 270 ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident); 271 let 〈laddr,haddr〉 ≝ represent_block addr in 272 ! locals ← reg_store ldest laddr (locals st); 273 ! locals ← reg_store hdest haddr locals; 274 ret ? 〈E0, goto l (set_locals locals st)〉 275 | joint_instr_op1 op acc_a ⇒ 276 ! v ← reg_retrieve (locals st) acc_a; 277 ! v ← Byte_of_val v; 278 let v' ≝ val_of_Byte (op1 eval op v) in 279 ! locals ← reg_store acc_a v' (locals st); 280 ret ? 〈E0, goto l (set_locals locals st)〉 281 | joint_instr_op2 op acc_a_reg dest ⇒ 282 ! v1 ← reg_retrieve (locals st) acc_a_reg; 283 ! v1 ← Byte_of_val v1; 284 ! v2 ← reg_retrieve (locals st) acc_a_reg; 285 ! v2 ← Byte_of_val v2; 286 ! carry ← eval_bool_of_val (carry st); 287 let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in 288 let v' ≝ val_of_Byte v' in 289 let carry ≝ of_bool carry in 290 ! locals ← reg_store dest v' (locals st); 291 ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉 292 | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉 293 | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉 294 | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒ 295 ! v1 ← reg_retrieve (locals st) acc_a_reg; 296 ! v1 ← Byte_of_val v1; 297 ! v2 ← reg_retrieve (locals st) acc_b_reg; 298 ! v2 ← Byte_of_val v2; 299 let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in 300 let v1' ≝ val_of_Byte v1' in 301 let v2' ≝ val_of_Byte v2' in 302 ! locals ← reg_store acc_a_reg v1' (locals st); 303 ! locals ← reg_store acc_b_reg v2' locals; 304 ret ? 〈E0, goto l (set_locals locals st)〉 305 | joint_instr_pop dst ⇒ 306 ! 〈st,v〉 ← pop st; 307 ! locals ← reg_store dst (val_of_Byte v) (locals st); 308 ret ? 〈E0, goto l (set_locals locals st)〉 309 | joint_instr_push src ⇒ 310 ! v ← reg_retrieve (locals st) src; 311 ! v ← Byte_of_val v; 312 ! st ← push st v; 313 ret ? 〈E0, goto l st〉 314 | joint_instr_move dst_src ⇒ 315 let 〈dst, src〉 ≝ dst_src in 316 ! v ← retrieve st src; 317 ! st ← store st v dst; 318 ret ? 〈E0, goto l st〉 319 (* CSC: changed, where the meat is *) 320 | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *) 321 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 322 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 323 match fd with 324 [ Internal fn ⇒ 325 ! st ← save_ra st l; 326 let st ≝ save_frame st in 327 let locals ≝ init_locals (ertl_if_locals globals fn) in 328 let l' ≝ ertl_if_entry globals fn in 329 ret ? 〈 E0, goto l' (set_locals locals st)〉 330 | External fn ⇒ 331 ! params ← fetch_external_args fn st; 332 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); 333 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 334 (* CSC: XXX bug here; I think I should split it into Byte-long 335 components; instead I am making a singleton out of it *) 336 let vs ≝ [mk_val ? evres] in 337 ! st ← set_result vs st; 338 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉 339 ] 340 ] 341 (* CSC: changed, where the meat is *) 342 | joint_st_return ⇒ 343 ! st ← pop_frame st; 344 ! 〈st,pch〉 ← pop st; 345 ! 〈st,pcl〉 ← pop st; 346 let pc ≝ address_of_address_chunks pcl pch in 347 ret ? 〈E0,set_pc pc st〉 348 | _ ⇒ ? 349 ] 350 | ertl_st_new_frame l ⇒ 351 ! v ← framesize globals st; 352 ! sp ← get_hwsp st; 353 let newsp ≝ addr_sub sp v in 354 ! st ← set_hwsp newsp st; 355 ret ? 〈E0,goto l st〉 356 | ertl_st_del_frame l ⇒ 357 ! v ← framesize globals st; 358 ! sp ← get_hwsp st; 359 let newsp ≝ addr_add sp v in 360 ! st ← set_hwsp newsp st; 361 ret ? 〈E0,goto l st〉 362 | ertl_st_frame_size dst l ⇒ 363 ! v ← framesize globals st; 364 ! locals ← reg_store dst (val_of_nat v) (locals st); 217 365 ret ? 〈E0, goto l (set_locals locals st)〉 218 | ertl_st_store addrl addrh src l ⇒219 ! vaddrh ← reg_retrieve (locals st) addrh;220 ! vaddrl ← reg_retrieve (locals st) addrl;221 ! vaddr ← smerge vaddrl vaddrh;222 ! v ← reg_retrieve (locals st) src;223 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);224 ret ? 〈E0, goto l (set_m m' st)〉225 | ertl_st_cond src ltrue lfalse ⇒226 ! v ← reg_retrieve (locals st) src;227 ! b ← eval_bool_of_val v;228 ret ? 〈E0, goto (if b then ltrue else lfalse) st〉229 | ertl_st_addr ldest hdest id l ⇒230 ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);231 let 〈laddr,haddr〉 ≝ represent_block addr in232 ! locals ← reg_store ldest laddr (locals st);233 ! locals ← reg_store hdest haddr locals;234 ret ? 〈E0, goto l (set_locals locals st)〉235 | ertl_st_op1 op dst src l ⇒236 ! v ← reg_retrieve (locals st) src;237 ! v ← Byte_of_val v;238 let v' ≝ val_of_Byte (op1 eval op v) in239 ! locals ← reg_store dst v' (locals st);240 ret ? 〈E0, goto l (set_locals locals st)〉241 | ertl_st_op2 op dst src1 src2 l ⇒242 ! v1 ← reg_retrieve (locals st) src1;243 ! v1 ← Byte_of_val v1;244 ! v2 ← reg_retrieve (locals st) src2;245 ! v2 ← Byte_of_val v2;246 ! carry ← eval_bool_of_val (carry st);247 let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in248 let v' ≝ val_of_Byte v' in249 let carry ≝ of_bool carry in250 ! locals ← reg_store dst v' (locals st);251 ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉252 | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒253 ! v1 ← reg_retrieve (locals st) sacc;254 ! v1 ← Byte_of_val v1;255 ! v2 ← reg_retrieve (locals st) sbacc;256 ! v2 ← Byte_of_val v2;257 let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in258 let v1' ≝ val_of_Byte v1' in259 let v2' ≝ val_of_Byte v2' in260 ! locals ← reg_store dacc v1' (locals st);261 ! locals ← reg_store dbacc v2' locals;262 ret ? 〈E0, goto l (set_locals locals st)〉263 | ertl_st_clear_carry l ⇒264 ret ? 〈E0, goto l (set_carry Vfalse st)〉265 | ertl_st_set_carry l ⇒266 ret ? 〈E0, goto l (set_carry Vtrue st)〉267 268 (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,269 ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would270 be more than enough... *)271 | ertl_st_move dst src l ⇒272 ! v ← reg_retrieve (locals st) src;273 ! locals ← reg_store dst v (locals st);274 ret ? 〈E0, goto l (set_locals locals st)〉275 | ertl_st_hdw_to_hdw dst src l ⇒276 ! v ← hwreg_retrieve (regs st) src;277 ! regs ← hwreg_store dst v (regs st);278 ret ? 〈E0, goto l (set_regs regs st)〉279 | ertl_st_get_hdw dst src l ⇒280 ! v ← hwreg_retrieve (regs st) src;281 ! locals ← reg_store dst v (locals st);282 ret ? 〈E0, goto l (set_locals locals st)〉283 | ertl_st_set_hdw dst src l ⇒284 ! v ← reg_retrieve (locals st) src;285 ! regs ← hwreg_store dst v (regs st);286 ret ? 〈E0, goto l (set_regs regs st)〉287 288 366 (* CSC: Dropped: 289 367 - rtl_st_stackaddr (becomes two get_hdw) 290 368 - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM) 291 369 - rtl_st_call_ptr (unimplemented ATM) *) 370 ]. 292 371 293 (* CSC: changed, where the meat is *) 294 | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *) 295 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 296 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 297 match fd with 298 [ Internal fn ⇒ 299 ! st ← save_ra st l; 300 let st ≝ save_frame st in 301 let locals ≝ init_locals (ertl_if_locals fn) in 302 let l' ≝ ertl_if_entry fn in 303 ret ? 〈 E0, goto l' (set_locals locals st)〉 304 | External fn ⇒ 305 ! params ← fetch_external_args fn st; 306 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); 307 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 308 (* CSC: XXX bug here; I think I should split it into Byte-long 309 components; instead I am making a singleton out of it *) 310 let vs ≝ [mk_val ? evres] in 311 ! st ← set_result vs st; 312 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉 372 axiom WrongReturnValueType: String. 373 374 definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝ 375 λglobals: list ident. 376 λexit. 377 λregistersno. 378 λst. 379 (* CSC: monadic notation missing here *) 380 match fetch_statement globals st with 381 [ Error _ ⇒ None ? 382 | OK s ⇒ 383 match s with 384 [ ertl_st_lift_pre pre ⇒ 385 match pre with 386 [ joint_st_return ⇒ 387 match fetch_ra st with 388 [ Error _ ⇒ None ? 389 | OK st_l ⇒ 390 let 〈st,l〉 ≝ st_l in 391 match label_eq l exit with 392 [ inl _ ⇒ 393 (* CSC: monadic notation missing here *) 394 match fetch_result st registersno with 395 [ Error _ ⇒ None ? 396 | OK vals ⇒ Some ? (smerge2 vals) 397 ] 398 | inr _ ⇒ None ? 399 ] 400 ] 401 | _ ⇒ None ? 313 402 ] 314 | ertl_st_return ⇒ 315 ! st ← pop_frame st; 316 ! 〈st,pch〉 ← pop st; 317 ! 〈st,pcl〉 ← pop st; 318 let pc ≝ address_of_address_chunks pcl pch in 319 ret ? 〈E0,set_pc pc st〉 320 321 (* CSC: new stuff *) 322 | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉 323 | ertl_st_new_frame _ ⇒ ? 324 | ertl_st_del_frame _ ⇒ ? 325 | ertl_st_frame_size _ _ ⇒ ? 326 | ertl_st_pop dst l ⇒ 327 ! 〈st,v〉 ← pop st; 328 ! locals ← reg_store dst (val_of_Byte v) (locals st); 329 ret ? 〈E0, goto l (set_locals locals st)〉 330 | ertl_st_push src l ⇒ 331 ! v ← reg_retrieve (locals st) src; 332 ! v ← Byte_of_val v; 333 ! st ← push st v; 334 ret ? 〈E0, goto l st〉 403 | _ ⇒ None ? 404 ] 335 405 ]. 336 406 337 axiom WrongReturnValueType: String. 338 339 definition is_final : state → option ((*CSC: why not res*) int) ≝ 340 λs. match s with 341 [ State _ _ _ ⇒ None ? 342 | Callstate _ _ _ _ _ ⇒ None ? 343 | Returnstate v _ fs _ ⇒ 344 match fs with 345 [ nil ⇒ Some ? (smerge2 v) 346 | _ ⇒ None ? ]]. 347 348 definition RTL_exec : execstep io_out io_in ≝ 349 mk_execstep … ? is_final mem_of_state eval_statement. 407 definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝ 408 λglobals. 409 λexit. 410 λregistersno. 411 mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals). 350 412 351 413 (* CSC: XXX the program type does not fit with the globalenv and init_mem
Note: See TracChangeset
for help on using the changeset viewer.