Changeset 1103


Ignore:
Timestamp:
Aug 5, 2011, 1:47:34 PM (8 years ago)
Author:
boender
Message:
  • reverted to old policy
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1054 r1103  
    441441  let 〈p1, p2〉 ≝ split ? 5 11 pc in
    442442   if eq_bv ? a1 p1 then (* we're in the same segment *)
    443     〈3, 2, address, Some ? medium_jump〉
     443    〈2, 2, address, Some ? medium_jump〉
    444444   else
    445     〈3, 3, address, Some ? long_jump〉.
     445    〈2, 3, address, Some ? long_jump〉.
    446446   
    447 lemma frc_ok:
     447(* lemma frc_ok:
    448448  ∀pc.∀j_addr.
    449449  let 〈i1,i2,addr,jl〉 ≝ find_right_call pc j_addr in
     
    462462 [ %1 [ @refl | @(eq_bv_eq … H) ]
    463463 | %1 [ @refl | // ] ]
    464 qed.
     464qed. *)
    465465       
    466466definition distance ≝
     
    474474  let pa ≝ nat_of_bitvector ? address in
    475475   if ltb (distance pn pa) 127 then
    476     〈2, 3, address, Some ? short_jump〉
     476    〈2, 2, address, Some ? short_jump〉
    477477   else
    478478    find_right_call pc address.
    479479
    480 lemma frj_ok:
     480(* lemma frj_ok:
    481481  ∀pc.∀j_addr.
    482482  let 〈i1,i2,addr,jl〉 ≝ find_right_jump pc j_addr in
     
    502502   ]
    503503  ]
    504 qed.
     504qed. *)
    505505   
    506506definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) →
     
    508508 λpc.λlabels.λjmp.
    509509 match lookup_opt ? ? jmp labels with
    510  [ None ⇒ 〈3, 3, pc, Some ? long_jump〉
     510 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉
    511511 | Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ].
    512512 
    513 lemma frrj_ok:
     513(* lemma frrj_ok:
    514514  ∀pc.∀labels.∀j_id.
    515515  let 〈i1,i2,addr,jl〉 ≝ find_right_relative_jump pc labels j_id in
     
    536536   ]
    537537 ]
    538 qed.
     538qed. *)
    539539     
    540540definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝
     
    553553         〈l, l, pc, None …〉 ].
    554554
    555 definition jgeq_opt ≝
    556  λa:jump_length.λb:option (Word × jump_length).
    557  match a with
    558  [ short_jump ⇒ match b with
    559    [ None ⇒ (* XXX *) False
    560    | Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump
    561    ]
    562  | medium_jump ⇒ match b with
    563   [ None ⇒  (* XXX *) False
    564   | Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump ∨ j = medium_jump ]
    565  | long_jump ⇒ True
    566  ].
    567 
    568555definition is_long_jump ≝
    569556 λj.match j with
     
    573560
    574561definition policy_safe ≝
    575  λp:BitVectorTrie (Word × Word × jump_length) 16.
    576   forall ? ? p (λ_.λx.let 〈pc,addr,j〉 ≝ x in
     562 (λ_:Word.λx:Word×Word×jump_length.let 〈pc,addr,j〉 ≝ x in
    577563   match j with
    578564   [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127
     
    583569
    584570definition jump_expansion_policy ≝
    585   Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.policy_safe policy.
     571  Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.
     572    forall ? ? policy policy_safe.
    586573 
    587574definition inject_jump_expansion_policy:
    588  ∀x:BitVectorTrie (Word × Word × jump_length) 16.
    589   policy_safe x → jump_expansion_policy ≝ inject ….
     575 ∀p:BitVectorTrie (Word × Word × jump_length) 16.
     576  forall ? ? p policy_safe → jump_expansion_policy ≝ inject ….
    590577 
    591578coercion inject_jump_expansion_policy:
    592  ∀x:BitVectorTrie (Word × Word × jump_length) 16.
    593   policy_safe x → jump_expansion_policy ≝ inject_jump_expansion_policy
    594  on x:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy.
     579 ∀p:BitVectorTrie (Word × Word × jump_length) 16.
     580  forall ? ? p policy_safe → jump_expansion_policy ≝ inject_jump_expansion_policy
     581 on p:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy.
     582 
     583(* the jump length in a is greater than or equal to the jump length in b *)
     584definition jump_length_decrease ≝
     585 λa:jump_length.λb:jump_length.
     586 match a with
     587 [ short_jump ⇒ b = short_jump
     588 | medium_jump ⇒ b = short_jump ∨ b = medium_jump
     589 | long_jump ⇒ True
     590 ].
    595591
    596592definition jump_expansion_policy_internal: pseudo_assembly_program →
    597593 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy →
    598594 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16).
    599   let 〈x,p〉 ≝ res in policy_safe p ≝
     595  let 〈x,p〉 ≝ res in
     596  True ≝
    600597 λprogram.λold_labels.λold_policy.
    601598   let res ≝
    602599   foldl_strong (option Identifier × pseudo_instruction)
    603     (λprefix.Σresult:(Word × Word) × ((BitVectorTrie (Word × Identifier) 16) ×
    604       (BitVectorTrie (Word × Word × jump_length) 16)).
    605       let 〈x,y,z,p〉 ≝ result in policy_safe p
    606     )
     600    (λprefix.Σres.True)
    607601    (\snd program)
    608602    (λprefix.λi.λtl.λprf.λacc.   
     
    616610      [ Call c ⇒
    617611        match lookup_opt ? ? c new_labels with
    618          [ None   ⇒ 〈3, 3, pc, Some ? long_jump〉
     612         [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
    619613         | Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ]
    620614      | Jmp j ⇒
    621615        match lookup_opt ? ? j new_labels with
    622          [ None   ⇒ 〈3, 3, pc, Some ? long_jump〉
     616         [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
    623617         | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ]
    624618      | Instruction i ⇒ jep_relative pc new_labels i
     
    636630   let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in
    637631   〈nlabels, npolicy〉.
    638    [ cases res in p -res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb;
     632   //.
     633(* [ cases res in p -res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb;
    639634     >Hb in Ha; normalize nodelta #H @H
    640635   | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
     
    715710     @H
    716711   | generalize in match (sig2 … old_policy) #H @H
    717    ]
    718 qed.
    719    
     712   ] *)
     713qed.
     714
     715(* lemma short_jumps_ok:
     716  ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
     717  forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
     718    (λk.λx.let 〈pc,addr,j〉 ≝ x in
     719      j = short_jump →
     720      distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
     721 #program #l #p @lookup_forall
     722  #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
     723  cases j in Hl; #Hl #Hj
     724  [2,3: destruct (Hj)
     725  |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
     726    #res cases res -res #r #res normalize nodelta #Hf #Hl
     727    normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
     728    normalize #H @H
     729  ]   
     730qed. *)
     731
     732(* lemma medium_jumps_ok:
     733  ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
     734  forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
     735    (λk.λx.let 〈pc,addr,j〉 ≝ x in
     736      j = medium_jump →
     737      distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
     738 #program #l #p @lookup_forall
     739  #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
     740  cases j in Hl; #Hl #Hj
     741  [2,3: destruct (Hj)
     742  |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
     743    #res cases res -res #r #res normalize nodelta #Hf #Hl
     744    normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
     745    normalize #H @H
     746  ]   
     747qed. *)
     748     
    720749definition expand_relative_jump_internal:
    721750 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     
    848877let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
    849878 (old_labels: BitVectorTrie (Word × Identifier) 16)
    850  (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.policy_safe bla)
     879 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.
     880   forall ? ? bla policy_safe)
    851881 on n: BitVectorTrie jump_length 16 ≝
    852882 match n with
     
    855885   old_policy (Stub ? ?)
    856886 | S n' ⇒
    857     (* let 〈x,y〉 ≝ jump_expansion_policy_internal program old_labels old_policy in *)
    858     jump_expansion_internal n' program (* x y *)
     887    jump_expansion_internal n' program
    859888    (\fst (jump_expansion_policy_internal program old_labels old_policy))
    860889    (\snd (jump_expansion_policy_internal program old_labels old_policy))
     
    864893 #a cases a #xx #pp normalize nodelta
    865894 #H #H2 normalize nodelta @H2
    866 qed.
    867  
     895qed.
     896
     897
     898
     899 
    868900(**************************************** START OF POLICY ABSTRACTION ********************)
    869901
Note: See TracChangeset for help on using the changeset viewer.