Changeset 2470


Ignore:
Timestamp:
Nov 15, 2012, 7:06:45 PM (7 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

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2462 r2470  
    1010unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    1111unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     12
     13(* this is like a code pointer, but with unbounded offset.
     14   used only in the back-end, they become code pointers in LIN → ASM *)
     15record program_counter : Type[0] ≝
     16  { pc_block : Σb : block.block_region b = Code
     17  ; pc_offset : Pos
     18  }.
     19
     20definition eq_program_counter : program_counter → program_counter → bool ≝
     21λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
     22         eqb (pc_offset pc1) (pc_offset pc2).
     23
     24lemma eq_program_counter_elim : ∀P:bool→Prop.
     25  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
     26#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
     27#Heq #Hneq whd in ⊢ (?%);
     28@eq_block_elim #EQ1
     29[ @eqb_elim #EQ2 ]
     30[ @Heq destruct %
     31|*: @Hneq % #ABS destruct
     32  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
     33] qed.
     34
     35lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
     36** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.
     37
     38definition bitvector_from_pos :
     39  ∀n.Pos → BitVector n ≝
     40  λn,p.bitvector_of_Z n (Zpred (pos p)).
     41
     42definition pos_from_bitvector :
     43  ∀n.BitVector n → Pos ≝
     44  λn,v.
     45  match Zsucc (Z_of_unsigned_bitvector n v)
     46  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
     47  with
     48  [ OZ ⇒ λprf.⊥
     49  | pos x ⇒ λ_. x
     50  | neg x ⇒ λprf.⊥
     51  ] (refl …).
     52@hide_prf
     53elim v in prf;
     54[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
     55
     56definition cpointer_of_pc : program_counter → option cpointer ≝
     57  λpc.
     58  let pc_off ≝ pc_offset pc in
     59  if leb pc_off (two_power_nat offset_size) then
     60    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
     61  else
     62    None ?.
     63elim (pc_block pc) #bl #H @H qed.
    1264
    1365record part (*r: region*): Type[0] ≝
     
    4395  | BVnull: (*∀r:region.*) part  → beval
    4496  | BVptr: pointer → part → beval
    45   | BVpc: cpointer → part → beval. (* only used in back end, needed to separate
     97  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
    4698                                      program counters that go in the stack from
    4799                                      function pointers, as they are linked with
     
    89141  ].
    90142
    91 definition pc_of_bevals: list beval → res cpointer ≝
     143definition pc_of_bevals: list beval → res program_counter ≝
    92144 λl.
    93145 match l with
     
    104156          match bv2 with
    105157          [ BVpc ptr2 p2 ⇒
    106             if eqb p1 0 ∧ eqb p2 1 ∧ eq_pointer ptr1 ptr2 then
     158            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
    107159              return ptr2
    108160            else Error … [MSG CorruptedPointer]
     
    120172
    121173definition bevals_of_pc ≝
    122  λp:cpointer.
     174 λp:program_counter.
    123175 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
    124176
     
    138190whd in match (bevals_of_pc ?);
    139191whd in ⊢ (??%?);
    140 >reflexive_eq_pointer
     192>reflexive_eq_program_counter
    141193%
    142194qed.
     
    162214   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    163215
    164 definition beval_pair_of_pc: cpointer → beval × beval ≝
     216definition beval_pair_of_pc: program_counter → beval × beval ≝
    165217 λp. list_to_pair ? (bevals_of_pc p) (refl …).
    166218
  • src/joint/Traces.ma

    r2457 r2470  
    55 { globals: list ident
    66 ; sparams:> sem_params
    7  ; exit: cpointer
     7 ; exit: program_counter
    88 ; ev_genv: genv sparams globals
    99(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    11 
    12 axiom is_internal_function_of_program :
    13   ∀p:params.joint_program p → ident → Prop.
    14 
    15 axiom is_internal_function_of_program_ok :
    16   ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i →
    17   is_internal_function_of_program p prog i.
     11 
     12
     13(* move elsewhere *)
     14definition is_internal_function_of_program :
     15  ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝
     16  λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉.
     17
     18lemma opt_elim : ∀A.∀m : option A.∀P : option A → Prop.
     19 (m = None ? → P (None ?)) →
     20 (∀x.m = Some ? x → P (Some ? x)) → P m.
     21#A * [2: #x] #P #H1 #H2
     22[ @H2 | @H1 ] % qed.
     23
     24axiom find_funct_ptr_symbol_inversion:
     25    ∀F,V,init. ∀p: program F V.
     26    ∀id: ident. ∀b: block. ∀f: F ?.
     27    find_symbol ? (globalenv ?? init p) id = Some ? b →
     28    find_funct_ptr ? (globalenv ?? init p) b = Some ? f →
     29    In … (prog_funct ?? p) 〈id, f〉.
     30
     31lemma is_internal_function_of_program_ok :
     32  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.
     33  is_internal_function ?? (globalenv ?? init prog) i →
     34  is_internal_function_of_program ?? prog i.
     35#A #B #init #prog #i whd in ⊢ (%→%); * #ifn
     36@(opt_elim … (find_symbol … i)) [#_ #ABS normalize in ABS; destruct(ABS) ]
     37#bl #EQbl >m_return_bind #EQfind %{ifn}
     38@(find_funct_ptr_symbol_inversion … EQbl EQfind)
     39qed.
    1840
    1941record prog_params : Type[1] ≝
    2042 { prog_spars : sem_params
    2143 ; prog : joint_program prog_spars
    22  ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
     44 ; stack_sizes : (Σi.is_internal_function_of_program ?? prog i) → ℕ
    2345(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    2446 }.
     
    2951(* Invariant: a -1 block is unused in common/Globalenvs *)
    3052let b ≝ mk_block Code (-1) in
    31 let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
     53let ptr ≝ mk_program_counter «b, refl …» one in
    3254let p ≝ prog pars in
    3355mk_evaluation_params
    3456  (prog_var_names … p)
    3557  (prog_spars pars)
    36   «ptr, refl …»
     58  ptr
    3759  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
    3860 (* (prog_io pars) *).
    39 [ @is_internal_function_of_program_ok @(pi2 … i)
     61[ @(is_internal_function_of_program_ok … (pi2 … i))
    4062| (* TODO or TOBEFOUND *)
    4163  cases daemon
     
    5678  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    5779  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    58   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
     80  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    5981  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
    6082(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
     
    7092    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
    7193    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
    72     ! pc' ← eval_internal_call_pc … ge main ;
     94    let pc' ≝ eval_internal_call_pc … ge main in
    7395    return mk_state_pc … st' pc'
    7496  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    7597  ] (refl …).
    76   [ %
    77   | @(description_of_internal_function … prf)
     98  [ @(description_of_internal_function … prf)
    7899  | cases spb normalize //
    79100  ]
     
    179200qed.
    180201
    181 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
    182 *#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
     202definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
     203*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
    183204[ #EQ destruct % #H %
    184205| * #NEQ % #ABS destruct elim (NEQ ?) %
     
    220241   (* as_execute ≝ *)
    221242    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    222    (* as_pc ≝ *) cpointerDeq
     243   (* as_pc ≝ *) pcDeq
    223244   (* as_pc_of ≝ *) (pc …)
    224245   (* as_classify ≝ *) (joint_classify p)
     
    233254      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
    234255      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
    235       succ_pc p p (pc … s1) nxt = return pc … s2)
     256      succ_pc p p (pc … s1) nxt = pc … s2)
    236257   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    237258   (* as_call_ident ≝ *) (joint_call_ident p).
  • 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 }.
  • src/joint/semanticsUtils.ma

    r2457 r2470  
    6767(******************************** GRAPHS **************************************)
    6868
    69 definition bitvector_from_pos :
    70   ∀n.Pos → BitVector n ≝
    71   λn,p.bitvector_of_Z n (Zpred (pos p)).
    72 
    73 definition pos_from_bitvector :
    74   ∀n.BitVector n → Pos ≝
    75   λn,v.
    76   match Zsucc (Z_of_unsigned_bitvector n v)
    77   return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
    78   with
    79   [ OZ ⇒ λprf.⊥
    80   | pos x ⇒ λ_. x
    81   | neg x ⇒ λprf.⊥
    82   ] (refl …).
    83 @hide_prf
    84 elim v in prf;
    85 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
    86 
    87 lemma pos_pos_from_bitvector :
    88   ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
    89 #n #bv elim bv -n
    90 [ %
    91 | #n * #bv #IH [ % | @IH ]
    92 ]
    93 qed.
    94 
    95 lemma bitvector_from_pos_from_bitvector :
    96   ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
    97 #n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
    98 >Zpred_Zsucc //
    99 qed.
    100 
    101 lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
    102   (∀q,r.
    103     ppos m = natp_plus (natp_times q (ppos n)) r →
    104     natp_lt r n →
    105     P (〈q,r〉)) →
    106   P (divide m n).
    107 #P #m #n #H
    108 lapply (refl … (divide m n))
    109 cases (divide ??) in ⊢ (???%→%);
    110 #q #r #EQ elim (divide_ok … EQ) -EQ @H
    111 qed.
    112 
    113 lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
    114   p < q → \snd (divide p q) = ppos p.
    115 #p #q #H @divide_elim * [2: #quot ]
    116 * [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
    117 @⊥ elim (lt_to_not_le ?? H) #H @H -H -H
    118 [ @(transitive_le … (quot*q)) ] /2 by /
    119 qed.
    120 
    121 lemma pos_from_bitvector_from_pos :
    122   ∀n,p.
    123   p ≤ two_power_nat n →
    124   pos_from_bitvector n (bitvector_from_pos n p) = p.
    125 #n #p #H
    126 cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
    127 [2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
    128 >pos_pos_from_bitvector
    129 whd in match (bitvector_from_pos ??);
    130 >Z_of_unsigned_bitvector_of_Z
    131 cases p in H ⊢ %;
    132 [ #_ %
    133 |*: #p' #H
    134   whd in match (Zpred ?);
    135   whd in match (Z_two_power_nat ?);
    136   whd in ⊢ (??(?%)?);
    137   >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
    138   whd
    139   <succ_pred_n try assumption % #ABS destruct(ABS)
    140 ]
    141 qed.
    142 
    143 lemma pos_from_bitvector_max : ∀n,bv.
    144   pos_from_bitvector n bv ≤ two_power_nat n.
    145 #n #bv
    146 change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
    147 >pos_pos_from_bitvector
    148 @Zlt_to_Zle
    149 @bv_Z_unsigned_max
    150 qed.
    151 
    152 definition graph_offset_of_label : label → option offset ≝
    153   λl.let p ≝ word_of_identifier … l in
    154   if leb p (two_power_nat offset_size) then
    155     return mk_offset (bitvector_from_pos … p)
    156   else
    157     None ?.
    158 
    159 definition graph_label_of_offset: offset → label ≝
    160  λo.an_identifier ? (pos_from_bitvector ? (offv o)).
    161 
    16269definition make_sem_graph_params :
    16370  ∀pars : unserialized_params.
     
    17178      g_pars
    17279      (spars ?)
    173       graph_offset_of_label
    174       graph_label_of_offset
    175       ??
     80      (word_of_identifier ?)
     81      (an_identifier ?)
     82      ? (refl …)
    17683    ).
    177 whd in match graph_label_of_offset;
    178 whd in match graph_offset_of_label;
    179 whd in match word_of_identifier;
    180 normalize nodelta * #x
    181 @(leb_elim ? (two_power_nat ?)) normalize nodelta
    182 [ #_ >bitvector_from_pos_from_bitvector %
    183 | #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
    184 | #H whd >(pos_from_bitvector_from_pos … H) %
    185 | #_ %
    186 ]
    187 qed.
     84* #p % qed.
    18885
    18986(******************************** LINEAR **************************************)
    19087
    191 definition lin_offset_of_nat : ℕ → option offset ≝
    192   λn.
    193   if leb (S n) (2^offset_size) then
    194     return mk_offset (bitvector_of_nat ? n)
    195   else
    196     None ?.
     88lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
     89@pos_elim [%]
     90#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    19791
    198 definition lin_nat_of_offset : offset → ℕ ≝
    199   λo.nat_of_bitvector ? (offv o).
    20092
    20193definition make_sem_lin_params :
     
    210102      lin_pars
    211103      (spars ?)
    212       lin_offset_of_nat
    213       lin_nat_of_offset
     104      succ_pos_of_nat
     105      (λp.pred (nat_of_pos p))
    214106      ??
    215107    ).
    216 [ * ] #x
    217 whd in match lin_offset_of_nat;
    218 whd in match lin_nat_of_offset;
    219 normalize nodelta
    220 @leb_elim normalize nodelta #H
    221 [ >bitvector_of_nat_inverse_nat_of_bitvector %
    222 | @⊥ cases H #H @H -H -H //
    223 | whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
    224 | %
    225 ]
    226 qed.
     108[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     109| #n >nat_succ_pos %
     110] qed.
Note: See TracChangeset for help on using the changeset viewer.