Changeset 1109


Ignore:
Timestamp:
Aug 24, 2011, 5:12:10 PM (8 years ago)
Author:
campbell
Message:

Update branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/Assembly.ma

    r1054 r1109  
    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
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1084 r1109  
    3232  | ertl_st_load: register → register → register → label → ertl_statement
    3333  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: label → Byte → label → ertl_statement
     34  | ertl_st_call_id: ident → Byte → label → ertl_statement
    3535  | ertl_st_cond: register → label → label → ertl_statement
    36   | ertl_st_return: label → ertl_statement.
     36  | ertl_st_return: ertl_statement.
    3737
    3838definition ertl_statement_graph ≝ graph ertl_statement.
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma

    r1084 r1109  
    231231    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232232      joint_st_sequential ? globals (joint_instr_skip globals) l
    233   | ertl_st_return l ⇒ joint_st_return ? globals
     233  | ertl_st_return ⇒ joint_st_return ? globals
    234234  ].
    235235  cases daemon (* XXX: todo -- proofs regarding gvars *)
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1098 r1109  
    1 
     1include "utilities/Fix.ma".
    22include "ASM/Util.ma".
    33include "ERTL/ERTL.ma".
     
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    3232
    33 definition list_set_member ≝
    34   λA: Type[0].
    35   λeq_a: A → A → bool.
    36   λa: A.
    37   λl: list A.
    38     member A eq_a a l.
     33definition list_set_member ≝ member.
     34
     35definition list_set_fold ≝ foldr.
    3936
    4037definition statement_successors ≝
     
    303300    | Some stmt ⇒ statement_semantics stmt (liveafter label)
    304301    ]
     302  in
     303  let liveafter ≝ λlabel. λliveafter: valuation.
     304    match lookup ? ? (ertl_if_graph int_fun) label with
     305    [ None      ⇒ ?
     306    | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     307        lattice_join (livebefore successor liveafter) accu)
     308        lattice_bottom (statement_successors stmt)
     309    ]
    305310  in ?.
  • Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma

    r1091 r1109  
    2323  | joint_instr_load: joint_instruction globals
    2424  | joint_instr_store: joint_instruction globals
    25   | joint_instr_call_id: label → joint_instruction globals
     25  | joint_instr_call_id: ident → joint_instruction globals
    2626  | joint_instr_cond_acc: label → joint_instruction globals.
    2727
  • Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma

    r1091 r1109  
    2626  | rtl_st_cond: register → label → label → rtl_statement
    2727  | rtl_st_set_carry: label → rtl_statement
    28   | rtl_st_return: label → rtl_statement.
     28  | rtl_st_return: rtl_statement.
    2929 
    3030definition rtl_statement_graph ≝ graph rtl_statement.
  • Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma

    r1081 r1109  
    190190 
    191191definition save_hdws_internal ≝
    192   λdestr_srcr: register × hardware_register.
     192  λdestr_srcr: register × Register.
    193193  λstart_lbl: label.
    194194    let 〈destr, srcr〉 ≝ destr_srcr in
     
    200200   
    201201definition restore_hdws_internal ≝
    202   λdestr_srcr: hardware_register × register.
     202  λdestr_srcr: Register × register.
    203203  λstart_lbl: label.
    204204    let 〈destr, srcr〉 ≝ destr_srcr in
Note: See TracChangeset for help on using the changeset viewer.