 Timestamp:
 Nov 14, 2012, 10:31:55 AM (8 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r2457 r2462 410 410 λp,globals. 411 411 Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def). 412 413 unification hint 0 ≔ p,g ⊢ 414 joint_closed_internal_function p g ≡ 415 Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)). 412 416 413 417 definition set_joint_code ≝ 
src/joint/semantics.ma
r2457 r2462 73 73 ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝ 74 74 λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?. 75 definition cpointer ≝ Σp.ptype p = Code.76 definition xpointer ≝ Σp.ptype p = XData.77 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).78 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).79 unification hint 0 ≔ p,g ⊢80 joint_closed_internal_function p g ≡81 Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).82 75 83 76 record sem_state_params : Type[1] ≝ … … 239 232 qed. 240 233 234 (* bevals hold a function pointer (BVptr) *) 241 235 definition funct_of_bevals : ∀F,globals,ge. 242 236 beval → beval → option (Σi.is_function F globals ge i) ≝ 243 237 λF,globals,ge,dpl,dph. 244 238 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 245 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ 239 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *) 246 240 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 247 241 funct_of_block … (pblock ptr) … … 370 364 definition save_ra : ∀p. state p → cpointer → res (state p) ≝ 371 365 λp,st,l. 372 let 〈addrl,addrh〉 ≝ beval_pair_of_p ointerl in366 let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in 373 367 ! st' ← push … st addrl; 374 368 push … st' addrh. … … 376 370 definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝ 377 371 λp,st. 378 do 〈addrh, st'〉 ← pop … st; 379 do 〈addrl, st''〉 ← pop … st'; 380 do pr ← pointer_of_address 〈addrh, addrl〉; 381 match ptype pr return λx.ptype pr = x → res (cpointer × ?) with 382 [ Code ⇒ λprf.return 〈«pr,prf», st''〉 383  _ ⇒ λ_.Error … [MSG BadPointer] 384 ] (refl …). 372 ! 〈addrh, st'〉 ← pop … st; 373 ! 〈addrl, st''〉 ← pop … st'; 374 ! pr ← pc_of_bevals [addrh; addrl]; 375 return 〈pr, st''〉. 385 376 386 377 (* parameters that are defined by serialization *)
Note: See TracChangeset
for help on using the changeset viewer.