Ignore:
Timestamp:
Jul 17, 2012, 6:00:03 PM (8 years ago)
Author:
tranquil
Message:
  • updated joint semantics: generation of linear and graph semantics
  • opened two axioms in BitVectorZ
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r2186 r2200  
    308308record more_sem_params (pp : params) : Type[1] ≝
    309309  { msg_pars :> more_sem_genv_params pp
    310   ; offset_of_point : code_point pp → offset
    311   ; point_of_offset : offset → option (code_point pp)
    312   ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
    313   ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
     310  ; offset_of_point : code_point pp → option offset (* can overflow *)
     311  ; point_of_offset : offset → code_point pp
     312  ; point_of_offset_of_point :
     313    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
     314  ; offset_of_point_of_offset :
     315    ∀o.offset_of_point (point_of_offset o) = Some ? o
    314316  }.
    315317
     318axiom CodePointerOverflow : String.
     319
    316320definition pointer_of_point : ∀p.more_sem_params p →
    317   cpointer→ code_point p → cpointer ≝
     321  cpointer→ code_point p → res cpointer ≝
    318322  λp,msp,ptr,pt.
    319     mk_pointer (pblock ptr) (offset_of_point p msp pt).
     323  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
     324  return «mk_pointer (pblock ptr) o, ?».
    320325elim ptr #ptr' #EQ <EQ % qed.
    321326
    322 axiom BadOffsetForCodePoint : String.
    323 
    324327definition point_of_pointer :
    325   ∀p.more_sem_params p → cpointer → res (code_point p) ≝
    326   λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
    327     (point_of_offset p msp (poff ptr)).
     328  ∀p.more_sem_params p → cpointer → code_point p ≝
     329  λp,msp,ptr.point_of_offset p msp (poff ptr).
    328330
    329331lemma point_of_pointer_of_point :
    330   ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
    331 #p #msp #ptr #pt normalize
    332 >point_of_offset_of_point %
     332  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     333  pointer_of_point p msp ptr1 pt = return ptr2 →
     334  point_of_pointer p msp ptr2 = pt.
     335#p #msp #ptr1 #ptr2 #pt normalize
     336lapply (point_of_offset_of_point p msp pt)
     337cases (offset_of_point ???) normalize
     338[ * #ABS destruct(ABS)
     339| #o #EQ1 #EQ2 destruct %
     340]
    333341qed.
    334342
    335343lemma pointer_of_point_block :
    336   ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
    337 / by refl/
     344  ∀p,msp,ptr1,ptr2,pt.
     345  pointer_of_point p msp ptr1 pt = return ptr2 →
     346  pblock ptr2 = pblock ptr1.
     347#p #msp #ptr1 #ptr2 #pt normalize
     348cases (offset_of_point ???) normalize
     349[ #ABS destruct(ABS)
     350| #o #EQ destruct(EQ) %
     351]
    338352qed.
    339353
     
    346360
    347361lemma pointer_of_point_of_pointer :
    348   ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
    349     pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
    350     pointer_of_point p msp ptr2 pt = ptr1.
     362  ∀p,msp.∀ptr1,ptr2 : cpointer.
     363    pblock ptr1 = pblock ptr2 →
     364    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
    351365#p #msp ** #b1 #o1 #EQ1
    352366        ** #b2 #o2 #EQ2
    353 #pt #EQ3
    354 destruct
    355 lapply (offset_of_point_of_offset p msp o1)
    356 normalize
    357 elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
    358 #pt' #EQ #EQ' destruct %
     367#EQ3 destruct
     368normalize >offset_of_point_of_offset normalize %
    359369qed.
    360 
    361370
    362371axiom ProgramCounterOutOfCode : String.
     
    367376  genv globals p → cpointer → res (joint_statement p globals) ≝
    368377  λp,msp,globals,ge,ptr.
    369   ! pt ← point_of_pointer ? msp ptr ;
     378  let pt ≝ point_of_pointer ? msp ptr in
    370379  ! fn ← fetch_function … ge ptr ;
    371380  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     
    377386  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    378387            (point_of_label … (joint_if_code … fn) lbl) ;
    379   return (mk_pointer(mk_block Code (block_id (pblock ptr)))
    380     (offset_of_point p msp pt) : Σp.?). // qed.
     388  pointer_of_point p msp ptr pt.
    381389
    382390definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
    383391  cpointer → succ p → res cpointer ≝
    384392  λp,msp,ptr,nxt.
    385   ! curr ← point_of_pointer p msp ptr ;
    386   return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
     393  let curr ≝ point_of_pointer p msp ptr in
     394  pointer_of_point p msp ptr (point_of_succ p curr nxt).
    387395
    388396record sem_params : Type[1] ≝
     
    564572    let st' ≝ set_regs p regs st in
    565573    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    566     let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     574    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
    567575    return mk_state_pc ? st' pc. % qed.
    568576
Note: See TracChangeset for help on using the changeset viewer.