Changeset 1393 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Oct 17, 2011, 3:50:50 PM (8 years ago)
Author:
boender
Message:
  • added invariant for policy trie to assembly
  • change (syntax only) to status in order to make it compile
  • added lemma + renaming to bitvectortrie
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1363 r1393  
    414414
    415415(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
    416 definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16.
     416definition jump_expansion_policy ≝ BitVectorTrie ( × jump_length) 16.
    417417
    418418definition expand_relative_jump_internal:
     
    545545
    546546(* label_trie: identifier ↦ 〈instruction number, address〉 *)
    547 definition label_trie ≝ BitVectorTrie (nat × Word) 16.
    548 
    549 definition add_instruction_size: Word → jump_length → pseudo_instruction → Word
     547definition label_trie ≝ BitVectorTrie (nat × nat) 16.
     548
     549definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ
    550550  λpc.λjmp_len.λinstr.
    551   let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in
     551  let bv_pc ≝ bitvector_of_nat 16 pc in
     552  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
    552553  let bv: list (BitVector 8) ≝ match ilist with
    553554    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
    554555    | Some l ⇒ flatten … (map … assembly1 l)
    555556    ] in
    556   let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
    557   new_pc.
    558 
     557  pc + (|bv|).
     558 
    559559definition is_label ≝
    560560  λx:labelled_instruction.λl:Identifier.
     
    631631 ]
    632632qed. 
     633
     634lemma coerc_pair_sigma:
     635 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
     636#A #B #P * #a #b #p % [@a | /2/]
     637qed.
     638coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
     639≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
    633640     
    634 definition create_label_trie: list labelled_instruction → jump_expansion_policy →
    635   label_trie ≝
    636   λprogram.λpolicy.
     641let rec create_label_trie (program: list labelled_instruction)
     642  (policy: jump_expansion_policy):
     643  (Σlabels:label_trie.
     644    ∀i:ℕ.i < |program| →
     645    ∀l.occurs_exactly_once l program →
     646    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
     647    ∃a.lookup_opt … l labels = Some ? 〈i,a〉
     648  ) ≝
    637649  let 〈final_pc, final_labels〉 ≝
    638650    foldl_strong (option Identifier × pseudo_instruction)
    639     (λprefix.Σres.
    640       let 〈pc,labels〉 ≝ res in
     651    (λprefix.ℕ × (Σlabels.
    641652      ∀i:ℕ.i < |prefix| →
    642       ∀l.occurs_exactly_once l prefix ->
     653      ∀l.occurs_exactly_once l prefix
    643654      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    644       ∃a.lookup_opt … l labels = Some ? 〈i,a〉
     655      ∃a.lookup_opt … l labels = Some ? 〈i,a〉)
    645656    )
    646657    program
     
    648659     let 〈pc,labels〉 ≝ acc in
    649660     let 〈label,instr〉 ≝ x in
    650      let new_labels ≝
    651        match label with
    652        [ None   ⇒ labels
    653        | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
    654        ] in
    655      let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in
    656      let new_pc ≝ add_instruction_size pc jmp_len instr in
    657      〈new_pc, new_labels〉
    658     ) 〈zero ?, Stub ? ?〉 in
     661          let new_labels ≝
     662          match label with
     663          [ None   ⇒ labels
     664          | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
     665          ] in
     666          let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
     667          〈add_instruction_size pc jmp_len instr, new_labels〉
     668    ) 〈0, Stub ? ?〉 in
    659669    final_labels.
    660 [ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length
    661   <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    662   [ #Hi #l cases label
     670[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     671  [ #Hi #l normalize nodelta; cases label normalize nodelta
    663672    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    664       lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr
     673      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    665674      % [ @addr | @Haddr ]
    666675    | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
     
    669678        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    670679        @⊥ @(absurd … Hocc)
    671       | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?)
    672         [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
    673         | @Hocc
    674         | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]   
     680      | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
     681        [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]
     682        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
    675683        ]
    676684      ]
     
    678686    ]
    679687  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
    680     [ <minus_n_n #Hl normalize in Hl; cases label in Hl;
     688    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
    681689      [ normalize nodelta #H @⊥ @H
    682       | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]
     690      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ]
    683691      ]
    684692    | @le_n
     
    689697qed.
    690698
    691 definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝
     699definition select_reljump_length: label_trie → → Identifier → jump_length ≝
    692700  λlabels.λpc.λlbl.
    693701  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
    694   if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *)
    695   then short_jump
    696   else long_jump.
    697 
    698 definition select_call_length: label_trie → Word → Identifier → jump_length ≝
    699   λlabels.λpc.λlbl.
    700   let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     702  if leb pc addr (* forward jump *)
     703  then if leb (addr - pc) 126
     704       then short_jump
     705       else long_jump
     706  else if leb (pc - addr) 129
     707       then short_jump
     708       else long_jump.
     709
     710definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝
     711  λlabels.λpc_nat.λlbl.
     712  let pc ≝ bitvector_of_nat 16 pc_nat in
     713  let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) in
    701714  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    702715  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     
    705718  else long_jump.
    706719 
    707 definition select_jump_length: label_trie → Word → Identifier → jump_length ≝
     720definition select_jump_length: label_trie → → Identifier → jump_length ≝
    708721  λlabels.λpc.λlbl.
    709722  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
    710   if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *)
    711   then short_jump
    712   else
    713     let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
    714     let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    715     let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    716     if eq_bv ? fst_5_addr fst_5_pc
    717     then medium_jump
    718     else long_jump.
     723  if leb pc addr
     724  then if leb (addr - pc) 126
     725       then short_jump
     726       else select_call_length labels pc lbl
     727  else if leb (pc - addr) 129
     728       then short_jump
     729       else select_call_length labels pc lbl.
    719730 
    720 definition jump_expansion_step_instruction: label_trie → Word
     731definition jump_expansion_step_instruction: label_trie →
    721732  preinstruction Identifier → option jump_length ≝
    722733  λlabels.λpc.λi.
     
    745756  | short_jump  ⇒ j2
    746757  ].
    747      
    748 definition jump_expansion_step: list labelled_instruction →
    749   jump_expansion_policy → jump_expansion_policy ≝
    750   λprogram.λpolicy.
    751   let labels ≝ create_label_trie program policy in
    752   let 〈final_n, final_pc, final_policy〉 ≝
     758
     759definition jmpleq: jump_length → jump_length → Prop ≝
     760  λj1.λj2.
     761  match j1 with
     762  [ short_jump  ⇒ True
     763  | medium_jump ⇒
     764    match j2 with
     765    [ short_jump ⇒ False
     766    | _          ⇒ True
     767    ]
     768  | long_jump   ⇒
     769    match j2 with
     770    [ long_jump ⇒ True
     771    | _         ⇒ False
     772    ]
     773  ].
     774
     775definition is_jump' ≝
     776  λx:preinstruction Identifier.
     777  match x with
     778  [ JC _ ⇒ True
     779  | JNC _ ⇒ True
     780  | JZ _ ⇒ True
     781  | JNZ _ ⇒ True
     782  | JB _ _ ⇒ True
     783  | JNB _ _ ⇒ True
     784  | JBC _ _ ⇒ True
     785  | CJNE _ _ ⇒ True
     786  | DJNZ _ _ ⇒ True
     787  | _ ⇒ False
     788  ].
     789 
     790definition is_jump ≝
     791  λx:labelled_instruction.
     792  let 〈label,instr〉 ≝ x in
     793  match instr with
     794  [ Instruction i   ⇒ is_jump' i
     795  | Call _ ⇒ True
     796  | Jmp _ ⇒ True
     797  | _ ⇒ False
     798  ].
     799 
     800axiom bitvector_of_nat_ok:
     801  ∀x,y,n.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y.
     802 
     803let rec jump_expansion_step (program: list labelled_instruction)
     804  (old_policy: jump_expansion_policy):
     805  (Σpolicy.∀i:ℕ.i < |program| →
     806    is_jump (nth i ? program 〈None ?, Comment [ ]〉) →
     807    ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉
     808  ) ≝
     809  let labels ≝ create_label_trie program old_policy in
     810  let 〈final_pc, final_policy〉 ≝
    753811    foldl_strong (option Identifier × pseudo_instruction)
    754     (λprefix.Σres.True)
     812    (λprefix.ℕ × Σpolicy.∀i:ℕ.i < |prefix| →
     813      is_jump (nth i ? prefix 〈None ?, Comment [ ]〉) →
     814      ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉
     815    )
    755816    program
    756817    (λprefix.λx.λtl.λprf.λacc.
    757       let 〈n, pc, policy〉 ≝ acc in
     818      let 〈pc, policy〉 ≝ acc in
    758819      let 〈label,instr〉 ≝ x in
    759       let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in
     820      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in
    760821      let add_instr ≝
    761822        match instr with
     
    766827        ] in
    767828      let 〈new_pc, new_policy〉 ≝
    768         let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in
     829        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in
    769830        match add_instr with
    770831        [ None    ⇒ (* i.e. it's not a jump *)
     
    772833        | Some ai ⇒
    773834          let new_length ≝ max_length old_length ai in
    774           〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉
     835          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
    775836        ] in
    776       〈S n, new_pc, new_policy〉
    777     ) 〈0, zero ?, Stub ? ?〉 in
     837      〈new_pc, new_policy〉
     838    ) 〈0, Stub ? ?〉 in
    778839    final_policy.
    779  @I
     840[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     841  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
     842    lapply (sig2 … policy) #Hacc elim (Hacc i (le_S_S_to_le … Hi) Hj) #henk #ingrid elim ingrid
     843    -ingrid #ingrid #Hingrid
     844    % [ @henk | % [ @ingrid | normalize nodelta cases instr normalize nodelta
     845    [2,3: #x cases (lookup ??? policy ?) #y #z @Hingrid
     846    |6: #x #y cases (lookup ??? policy ?) #w #z @Hingrid
     847    |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???)
     848      [ @Hingrid
     849      | #z normalize nodelta <Hingrid @lookup_opt_insert_miss
     850        @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
     851        [ @(bitvector_of_nat_ok … H)
     852        | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     853        ] ]
     854      ]
     855    |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hingrid
     856      @lookup_opt_insert_miss @notb_elim >eq_bv_false
     857      [1,3: //
     858      |2,4: @nmk #H @(absurd (i = (|prefix|)))
     859        [1,3: @(bitvector_of_nat_ok … H)
     860        |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     861        ] ]
     862    ] ] ]
     863  | #Hi >nth_append_second >(injective_S … Hi)
     864    [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
     865      [2,3: #x #Hj @⊥ @Hj
     866      |6: #x #y #Hj @⊥ @Hj
     867      |1: #pi cases pi
     868        [35,36,37: #Hj @⊥ @Hj
     869        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
     870        |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
     871        |9,10,14,15: #j normalize nodelta #_
     872          % [1,3,5,7: @pc
     873            |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
     874              cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
     875              #x #y #Hl normalize nodelta
     876          % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     877            |2,4,6,8: @lookup_opt_insert_hit
     878            ] ]
     879        |11,12,13,16,17: #x #j normalize nodelta #_
     880          % [1,3,5,7,9: @pc
     881            |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
     882              cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
     883              #x #y #Hl normalize nodelta
     884          % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     885            |2,4,6,8,10: @lookup_opt_insert_hit
     886            ] ]
     887        ]
     888      |4,5: #j normalize nodelta #_
     889        % [1,3: @pc
     890          |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
     891              #x #y normalize nodelta
     892          % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
     893            |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
     894            |2,4: @lookup_opt_insert_hit
     895            ]
     896          ]
     897      ]
     898    | @le_n
     899    ]
     900  ]
     901| #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
     902]
    780903qed.
    781904 
     
    791914 λprogram.λpc.
    792915  let policy ≝ jump_expansion_internal (\snd program) in
    793   let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in
     916  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
    794917    j.
    795918 
Note: See TracChangeset for help on using the changeset viewer.