Changeset 2462 for src/joint


Ignore:
Timestamp:
Nov 14, 2012, 10:31:55 AM (7 years ago)
Author:
tranquil
Message:

separated in back end values program counters from code pointers (intended to hold function pointers only): same signature, but separation needed the proof of some passes

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2457 r2462  
    410410  λp,globals.
    411411    Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
     412
     413unification 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)).
    412416
    413417definition set_joint_code ≝
  • src/joint/semantics.ma

    r2457 r2462  
    7373  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
    7474  λ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)).
    8275
    8376record sem_state_params : Type[1] ≝
     
    239232qed.
    240233
     234(* bevals hold a function pointer (BVptr) *)
    241235definition funct_of_bevals : ∀F,globals,ge.
    242236  beval → beval → option (Σi.is_function F globals ge i) ≝
    243237λF,globals,ge,dpl,dph.
    244238! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
    245 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
     239if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
    246240   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then
    247241   funct_of_block … (pblock ptr)
     
    370364definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    371365 λp,st,l.
    372   let 〈addrl,addrh〉 ≝  beval_pair_of_pointer l in
     366  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
    373367  ! st' ← push … st addrl;
    374368  push … st' addrh.
     
    376370definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
    377371 λ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''〉.
    385376
    386377(* parameters that are defined by serialization *)
Note: See TracChangeset for help on using the changeset viewer.