Ignore:
Timestamp:
Nov 15, 2012, 7:06:45 PM (8 years ago)
Author:
tranquil
Message:

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2462 r2470  
    117117record state_pc (semp : sem_state_params) : Type[0] ≝
    118118  { st_no_pc :> state semp
    119   ; pc : cpointer
     119  ; pc : program_counter
    120120  }.
    121121
     
    265265 ∀globals.
    266266 ∀ge : genv pars globals.
    267   cpointer →
     267  program_counter →
    268268  res (Σi.is_internal_function … ge i) ≝
    269269 λpars,globals,ge,p.
    270270 opt_to_res … [MSG BadFunction; MSG BadPointer]
    271     (int_funct_of_block … ge (pblock p)).
     271    (int_funct_of_block … ge (pc_block p)).
    272272
    273273record sem_unserialized_params
     
    290290  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    291291  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    292   ; fetch_ra: state st_pars → res (cpointer × (state st_pars))
     292  ; fetch_ra: state st_pars → res (program_counter × (state st_pars))
    293293
    294294  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    295295  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    296   ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
     296  ; save_frame: program_counter → call_dest uns_pars → state st_pars → res (state st_pars)
    297297   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    298298     type of arguments. To be fixed using a dependent type *)
     
    362362 return 〈bv, set_istack … is st〉.
    363363
    364 definition save_ra : ∀p. state p → cpointer → res (state p) ≝
     364definition save_ra : ∀p. state p → program_counter → res (state p) ≝
    365365 λp,st,l.
    366366  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
     
    368368  push … st' addrh.
    369369
    370 definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
     370definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
    371371 λp,st.
    372372  ! 〈addrh, st'〉 ← pop … st;
     
    378378record more_sem_params (pp : params) : Type[1] ≝
    379379  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    380   ; offset_of_point : code_point pp → option offset (* can overflow *)
    381   ; point_of_offset : offset → code_point pp
     380  ; offset_of_point : code_point pp → Pos
     381  ; point_of_offset : Pos → code_point pp
    382382  ; point_of_offset_of_point :
    383     ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
     383    ∀pt.point_of_offset (offset_of_point pt) = pt
    384384  ; offset_of_point_of_offset :
    385     ∀o.offset_of_point (point_of_offset o) = Some ? o
     385    ∀o.offset_of_point (point_of_offset o) = o
    386386  }.
    387387
     
    399399ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
    400400
    401 axiom CodePointerOverflow : String.
    402 
    403 definition pointer_of_point : ∀p.more_sem_params p →
    404   cpointer→ code_point p → res cpointer ≝
     401definition pc_of_point : ∀p.more_sem_params p →
     402  program_counter → code_point p → program_counter ≝
    405403  λp,msp,ptr,pt.
    406   ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
    407   return «mk_pointer (pblock ptr) o, ?».
    408 elim ptr #ptr' #EQ <EQ % qed.
    409 
    410 definition point_of_pointer :
    411   ∀p.more_sem_params p → cpointer → code_point p ≝
    412   λp,msp,ptr.point_of_offset p msp (poff ptr).
     404  mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
     405
     406definition point_of_pc :
     407  ∀p.more_sem_params p → program_counter → code_point p ≝
     408  λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
    413409
    414410lemma point_of_pointer_of_point :
    415   ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
    416   pointer_of_point p msp ptr1 pt = return ptr2 →
    417   point_of_pointer p msp ptr2 = pt.
    418 #p #msp #ptr1 #ptr2 #pt normalize
    419 lapply (point_of_offset_of_point p msp pt)
    420 cases (offset_of_point ???) normalize
    421 [ * #ABS destruct(ABS)
    422 | #o #EQ1 #EQ2 destruct %
    423 ]
    424 qed.
     411  ∀p,msp.∀ptr,pt.
     412  point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
     413#p #msp #ptr #pt normalize // qed.
    425414
    426415lemma pointer_of_point_block :
    427   ∀p,msp,ptr1,ptr2,pt.
    428   pointer_of_point p msp ptr1 pt = return ptr2 →
    429   pblock ptr2 = pblock ptr1.
    430 #p #msp #ptr1 #ptr2 #pt normalize
    431 cases (offset_of_point ???) normalize
    432 [ #ABS destruct(ABS)
    433 | #o #EQ destruct(EQ) %
    434 ]
    435 qed.
     416  ∀p,msp,ptr,pt.
     417  pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
     418#p #msp #ptr #pt % qed. (* can probably do without *)
    436419
    437420lemma pointer_of_point_uses_block :
    438   ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
    439 #p #msp ** #b1 #o1 #EQ1
    440         ** #b2 #o2 #EQ2
    441 #pt #EQ3 destruct normalize //
    442 qed.
     421  ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
     422    pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
     423#p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
    443424
    444425lemma pointer_of_point_of_pointer :
    445   ∀p,msp.∀ptr1,ptr2 : cpointer.
    446     pblock ptr1 = pblock ptr2 →
    447     pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
    448 #p #msp ** #b1 #o1 #EQ1
    449         ** #b2 #o2 #EQ2
    450 #EQ3 destruct
    451 normalize >offset_of_point_of_offset normalize %
    452 qed.
     426  ∀p,msp.∀ptr1,ptr2.
     427    pc_block ptr1 = pc_block ptr2 →
     428    pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
     429#p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
    453430
    454431definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    455   ∀ge:genv p globals. cpointer →
     432  ∀ge:genv p globals. program_counter →
    456433  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    457434  λp,msp,globals,ge,ptr.
    458   let bl ≝ pblock ptr in
    459   ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer]
    460     (int_funct_of_block … ge bl) ;
     435  ! f ← fetch_function … ge ptr ;
    461436  let fn ≝ if_of_function … f in
    462   let pt ≝ point_of_pointer ? msp ptr in
     437  let pt ≝ point_of_pc ? msp ptr in
    463438  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
    464439  return 〈f, stmt〉.
    465440
    466 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    467   genv p globals → cpointer → label → res cpointer ≝
     441definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     442  genv p globals → program_counter → label → res program_counter ≝
    468443  λp,msp,globals,ge,ptr,lbl.
    469444  ! f ← fetch_function … ge ptr ;
     
    471446  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    472447            (point_of_label … (joint_if_code … fn) lbl) ;
    473   pointer_of_point p msp ptr pt.
     448  return pc_of_point p msp ptr pt.
    474449
    475450definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
    476   cpointer → succ p → res cpointer ≝
     451  program_counter → succ p → program_counter ≝
    477452  λp,msp,ptr,nxt.
    478   let curr ≝ point_of_pointer p msp ptr in
    479   pointer_of_point p msp ptr (point_of_succ p curr nxt).
     453  let curr ≝ point_of_pc p msp ptr in
     454  pc_of_point p msp ptr (point_of_succ p curr nxt).
    480455
    481456record sem_params : Type[1] ≝
     
    517492
    518493definition goto: ∀globals.∀p : sem_params.
    519   genv p globals → label → state p → cpointer → res (state_pc p) ≝
     494  genv p globals → label → state p → program_counter → res (state_pc p) ≝
    520495 λglobals,p,ge,l,st,b.
    521   ! newpc ← pointer_of_label ? p … ge b l ;
     496  ! newpc ← pc_of_label ? p … ge b l ;
    522497  return mk_state_pc ? st newpc.
    523498
     
    527502*)
    528503
    529 definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p)
     504definition next : ∀p : sem_params.succ p → state p → program_counter → state_pc p
    530505 λp,l,st,pc.
    531  ! newpc ← succ_pc ? p … pc l ;
    532  return mk_state_pc … st newpc.
     506 let newpc ≝ succ_pc ? p … pc l in
     507 mk_state_pc … st newpc.
    533508
    534509
     
    572547let fn ≝ if_of_function … ge i in
    573548let l' ≝ joint_if_entry ?? fn in
    574 let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in
    575 pointer_of_point ? p … pointer_in_fn l'.
     549mk_program_counter (block_of_funct_ident … ge (pi1 … i)) (offset_of_point ? p … l').
    576550[ @block_of_funct_ident_is_code
    577551| cases i /2 by internal_function_is_function/
     
    589563definition eval_seq_no_pc :
    590564 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
    591   state p → cpointer → joint_seq p globals →
     565  state p → program_counter → joint_seq p globals →
    592566  IO io_out io_in (state p) ≝
    593567 λp,globals,ge,curr_fn,st,next,seq.
     
    662636definition eval_seq_pc :
    663637 ∀p:sem_params.∀globals.∀ge:genv p globals.
    664   state p → cpointer → joint_seq p globals →
    665   res cpointer ≝
     638  state p → program_counter → joint_seq p globals →
     639  res program_counter ≝
    666640  λp,globals,ge,st,next,s.
    667641  match s with
     
    669643    ! fn ← function_of_call … ge st f;
    670644    match ? return λx.description_of_function … fn = x → ? with
    671     [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?»
     645    [ Internal _ ⇒ λprf.return eval_internal_call_pc … ge «fn, ?»
    672646    | External _ ⇒ λ_.return next
    673647    ] (refl …)
     
    685659  match s with
    686660  [ sequential s next ⇒
    687     ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;
     661    let next_ptr ≝ succ_pc ? p (pc … st) next in
    688662    match s return λ_.IO ??? with
    689663    [ step_seq s ⇒
     
    696670      ! pc' ←
    697671        if b then
    698           pointer_of_label ? p … ge (pc … st) l
     672          pc_of_label ? p … ge (pc … st) l
    699673        else
    700           succ_pc ? p (pc … st) next ;
     674          return succ_pc ? p (pc … st) next ;
    701675      return mk_state_pc … st pc'
    702676    ]
     
    704678    match s with
    705679    [ GOTO l ⇒
    706       ! pc' ← pointer_of_label ? p ? ge (pc … st) l ;
     680      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
    707681      return mk_state_pc … st pc'
    708682    | RETURN ⇒
     
    714688      match ? return λx.description_of_function … fn = x → ? with
    715689      [ Internal _ ⇒ λprf.
    716         ! pc' ← eval_internal_call_pc … ge «fn, ?» ;
     690        let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
    717691        return mk_state_pc … st pc'
    718692      | External fd ⇒ λ_.
     
    738712  not static... *)
    739713definition is_final: ∀globals:list ident. ∀p: sem_params.
    740   genv p globals → cpointer → state_pc p → option int ≝
     714  genv p globals → program_counter → state_pc p → option int ≝
    741715 λglobals,p,ge,exit,st.res_to_opt ? (
    742716  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
     
    747721    [ RETURN ⇒
    748722      do 〈ra, st'〉 ← fetch_ra … st;
    749       if eq_pointer ra exit then
     723      if eq_program_counter ra exit then
    750724       do vals ← read_result … ge (joint_if_result … fn) st' ;
    751725       Word_of_list_beval vals
     
    761735 { globals: list ident
    762736 ; sparams:> sem_params
    763  ; exit: cpointer
     737 ; exit: program_counter
    764738 ; genv2: genv globals sparams
    765739 }.
Note: See TracChangeset for help on using the changeset viewer.