- Timestamp:
- Sep 2, 2011, 4:09:02 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r1173 r1174 33 33 axiom val_of_nat: nat → val. 34 34 (* Map from the front-end memory model to the back-end memory model *) 35 *) 35 36 axiom represent_block: block → val × val. 36 *)37 37 (* CSC: fixed size chunk *) 38 38 axiom chunk: memory_chunk. … … 47 47 (* CSC: ??? *) 48 48 axiom address_of_label: mem → label → address. 49 (*50 49 axiom address_chunks_of_label: mem → label → Byte × Byte. 50 (* 51 51 axiom label_of_address_chunks: Byte → Byte → label. 52 52 *) … … 70 70 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *) 71 71 ; pop_frame_: framesT → res framesT 72 ; save_frame_: framesT → regsT → framesT 72 73 ; greg_store_: generic_reg p → val → regsT → res regsT 73 74 ; greg_retrieve_: regsT → generic_reg p → res val … … 80 81 ; dph_store_: dph_reg p → val → regsT → res regsT 81 82 ; dph_retrieve_: regsT → dph_reg p → res val 83 ; pair_reg_move_: regsT → pair_reg p → regsT 82 84 }. 83 85 … … 100 102 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st). 101 103 102 (* 103 definition set_carry: val → state → state ≝ 104 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st). 105 *) 104 definition set_carry: ∀p. val → state p → state p ≝ 105 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st). 106 106 107 107 definition set_pc: ∀p. address → state p → state p ≝ 108 108 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st). 109 110 definition set_frms: ∀p. framesT p → state p → state p ≝ 111 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st). 109 112 110 113 (* CSC: was build_state in RTL *) … … 157 160 λp,st,dst.dph_retrieve_ … (regs … st) dst. 158 161 159 (* 160 definition save_frame: state → state ≝ λst.st. (* CSC *) 161 162 axiom FailedPopFrame: String. 163 *) 162 definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝ 163 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st. 164 165 definition save_frame: ∀p:sem_params. state p → state p ≝ 166 λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st. 164 167 165 168 (* removes the top frame from the frames list *) … … 191 194 (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)). 192 195 193 (* 194 definition save_ra : state → label → res state ≝ 195 λst,l. 196 let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in 196 definition save_ra : ∀p. state p → label → res (state p) ≝ 197 λp,st,l. 198 let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in 197 199 (* No monadic notation here *) 198 bind ?? (push st addrl) (λst.push st addrh). 199 200 bind ?? (push … st addrl) (λst.push … st addrh). 201 202 (* 200 203 (*CSC: unused now 201 204 definition fetch_ra : state → res (state × label) ≝ … … 211 214 axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *) 212 215 axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *) 213 214 definition init_locals : list register → register_env val ≝ 216 *) 217 218 definition init_locals : ∀p.list register → regsT p ≝ 215 219 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??). 216 220 221 (* 217 222 definition reg_store ≝ 218 223 λreg,v,locals. update RegisterTag val locals reg v. … … 222 227 definition reg_retrieve : register_env val → register → res val ≝ 223 228 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg). 229 *) 224 230 225 231 axiom MissingSymbol : String. 226 *) 232 227 233 axiom FailedLoad : String. 228 (* 234 229 235 axiom BadFunction : String. 230 236 237 (* 231 238 (*CSC: to be implemented *) 232 239 axiom fetch_external_args: external_function → state → res (list val).(* ≝ … … 286 293 bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs. 287 294 OK ? (set_regs regs st))). 288 289 (*290 (* CSC: completely different because different type for registers_move *)291 definition retrieve: state → registers_move → res val ≝292 λst.293 λr.294 match r with295 [ pseudo src ⇒ reg_retrieve (locals st) src296 | from_acc src ⇒ hwreg_retrieve (regs st) src297 ].298 299 definition store ≝300 λst.301 λv.302 λr.303 match r with304 [ pseudo dst ⇒305 ! locals ← reg_store dst v (locals st);306 ret ? (set_locals locals st)307 | hardware dst ⇒308 ! regs ← hwreg_store dst v (regs st);309 ret ? (set_regs regs st)310 ].311 *)312 295 *) 313 296 … … 333 316 ! st ← acca_store … dst v st; 334 317 ret ? 〈E0, goto … l st〉 335 (*| joint_instr_store addrl addrh src ⇒336 ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)337 ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)318 | joint_instr_store addrl addrh src ⇒ 319 ! vaddrh ← dph_retrieve … st addrh; 320 ! vaddrl ← dpl_retrieve … st addrl; 338 321 ! vaddr ← smerge vaddrl vaddrh; 339 ! v ← hwreg_retrieve (regs st) src; (*CSC*)340 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);341 ret ? 〈E0, goto l (set_mm' st)〉322 ! v ← acca_retrieve … st src; 323 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m … st) vaddr v); 324 ret ? 〈E0, goto … l (set_m … m' st)〉 342 325 | joint_instr_cond src ltrue ⇒ 343 ! v ← hwreg_retrieve (regs st) src; (*CSC*)326 ! v ← acca_retrieve … st src; 344 327 ! b ← eval_bool_of_val v; 345 ret ? 〈E0, goto (if b then ltrue else l) st〉328 ret ? 〈E0, goto … (if b then ltrue else l) st〉 346 329 | joint_instr_address ident prf ldest hdest ⇒ 347 330 ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident); 348 331 let 〈laddr,haddr〉 ≝ represent_block addr in 349 ! locals ← reg_store ldest laddr (locals st);350 ! locals ← reg_store hdest haddr locals;351 ret ? 〈E0, goto l (set_locals locals st)〉332 ! st ← dpl_store … ldest laddr st; 333 ! st ← dph_store … hdest haddr st; 334 ret ? 〈E0, goto … l st〉 352 335 | joint_instr_op1 op acc_a ⇒ 353 ! v ← reg_retrieve (locals st)acc_a;336 ! v ← acca_retrieve … st acc_a; 354 337 ! v ← Byte_of_val v; 355 338 let v' ≝ val_of_Byte (op1 eval op v) in 356 ! locals ← reg_store acc_a v' (locals st);357 ret ? 〈E0, goto l (set_locals locals st)〉358 | joint_instr_op2 op acc_a _reg dest⇒359 ! v1 ← reg_retrieve (locals st) acc_a_reg;339 ! st ← acca_store … acc_a v' st; 340 ret ? 〈E0, goto … l st〉 341 | joint_instr_op2 op acc_a src ⇒ 342 ! v1 ← acca_retrieve … st acc_a; 360 343 ! v1 ← Byte_of_val v1; 361 ! v2 ← reg_retrieve (locals st) acc_a_reg;344 ! v2 ← greg_retrieve … src; 362 345 ! v2 ← Byte_of_val v2; 363 ! carry ← eval_bool_of_val (carry st);346 ! carry ← eval_bool_of_val (carry … st); 364 347 let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in 365 348 let v' ≝ val_of_Byte v' in 366 349 let carry ≝ of_bool carry in 367 ! locals ← reg_store dest v' (locals st);368 ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉369 | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carryVfalse st)〉370 | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carryVtrue st)〉350 ! st ← acca_store … acc_a v' st; 351 ret ? 〈E0, goto … l (set_carry … carry st)〉 352 | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vfalse st)〉 353 | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue st)〉 371 354 | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒ 372 ! v1 ← reg_retrieve (locals st)acc_a_reg;355 ! v1 ← acca_retrieve … st acc_a_reg; 373 356 ! v1 ← Byte_of_val v1; 374 ! v2 ← reg_retrieve (locals st)acc_b_reg;357 ! v2 ← accb_retrieve … st acc_b_reg; 375 358 ! v2 ← Byte_of_val v2; 376 359 let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in 377 360 let v1' ≝ val_of_Byte v1' in 378 361 let v2' ≝ val_of_Byte v2' in 379 ! locals ← reg_store acc_a_reg v1' (locals st);380 ! locals ← reg_store acc_b_reg v2' locals;381 ret ? 〈E0, goto l (set_locals locals st)〉362 ! st ← acca_store … acc_a_reg v1' st; 363 ! st ← accb_store … acc_b_reg v2' st; 364 ret ? 〈E0, goto … l st〉 382 365 | joint_instr_pop dst ⇒ 383 ! 〈st,v〉 ← pop st;384 ! locals ← reg_store dst (val_of_Byte v) (locals st);385 ret ? 〈E0, goto l (set_locals locals st)〉366 ! 〈st,v〉 ← pop … st; 367 ! st ← acca_store … dst (val_of_Byte v) st; 368 ret ? 〈E0, goto … l st〉 386 369 | joint_instr_push src ⇒ 387 ! v ← reg_retrieve (locals st)src;370 ! v ← acca_retrieve … st src; 388 371 ! v ← Byte_of_val v; 389 ! st ← push st v;390 ret ? 〈E0, goto l st〉372 ! st ← push … st v; 373 ret ? 〈E0, goto … l st〉 391 374 | joint_instr_move dst_src ⇒ 392 let 〈dst, src〉 ≝ dst_src in 393 ! v ← retrieve st src; 394 ! st ← store st v dst; 395 ret ? 〈E0, goto l st〉 375 ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉 396 376 | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *) 397 377 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); … … 400 380 [ Internal fn ⇒ 401 381 ! st ← save_ra st l; 402 let st ≝ save_frame st in403 let locals ≝ init_locals(ertl_if_locals globals fn) in382 let st ≝ save_frame … st in 383 let regs ≝ init_locals … (ertl_if_locals globals fn) in 404 384 let l' ≝ ertl_if_entry globals fn in 405 ret ? 〈 E0, goto l' (set_locals locals st)〉385 ret ? 〈 E0, goto … l' (set_regs … regs st)〉 406 386 | External fn ⇒ 407 387 ! params ← fetch_external_args fn st; … … 413 393 ! st ← set_result vs st; 414 394 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉 415 *)416 | _ ⇒ ?417 395 ] 396 ] 418 397 | joint_st_return ⇒ 419 398 ! st ← pop_frame … st;
Note: See TracChangeset
for help on using the changeset viewer.