Ignore:
Timestamp:
Jul 6, 2012, 5:26:21 PM (8 years ago)
Author:
mulligan
Message:

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2157 r2160  
    384384qed.
    385385
     386inductive upper_lower: Type[0] ≝
     387  | upper: upper_lower
     388  | lower: upper_lower.
     389
     390definition eq_upper_lower:
     391    upper_lower → upper_lower → bool ≝
     392  λleft: upper_lower.
     393  λright: upper_lower.
     394  match left with
     395  [ upper ⇒
     396    match right with
     397    [ upper ⇒ true
     398    | _     ⇒ false
     399    ]
     400  | lower ⇒
     401    match right with
     402    [ lower ⇒ true
     403    | _     ⇒ false
     404    ]
     405  ].
     406
     407lemma eq_upper_lower_true_to_eq:
     408  ∀left: upper_lower.
     409  ∀right: upper_lower.
     410    eq_upper_lower left right = true → left = right.
     411  * * normalize try (#_ %)
     412  #absurd destruct(absurd)
     413qed.
     414
     415lemma eq_upper_lower_false_to_neq:
     416  ∀left: upper_lower.
     417  ∀right: upper_lower.
     418    eq_upper_lower left right = false → left ≠ right.
     419  * * normalize try (#absurd destruct(absurd))
     420  @nmk #absurd destruct(absurd)
     421qed.
     422
     423inductive accumulator_address_map_entry: Type[0] ≝
     424  | data: accumulator_address_map_entry
     425  | address: upper_lower → Word → accumulator_address_map_entry.
     426
     427definition eq_accumulator_address_map_entry:
     428    accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
     429  λleft: accumulator_address_map_entry.
     430  λright: accumulator_address_map_entry.
     431    match left with
     432    [ data                     ⇒
     433      match right with
     434      [ data ⇒ true
     435      | _    ⇒ false
     436      ]
     437    | address upper_lower word ⇒
     438      match right with
     439      [ address upper_lower' word' ⇒
     440          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
     441      | _                          ⇒ false
     442      ]
     443    ].
     444
     445lemma eq_accumulator_address_map_entry_true_to_eq:
     446  ∀left: accumulator_address_map_entry.
     447  ∀right: accumulator_address_map_entry.
     448    eq_accumulator_address_map_entry left right = true → left = right.
     449  #left #right cases left cases right
     450  [1:
     451    #_ %
     452  |2,3:
     453    #upper_lower #word normalize #absurd destruct(absurd)
     454  |4:
     455    #upper_lower #word #upper_lower' #word' normalize
     456    cases upper_lower' normalize nodelta
     457    cases upper_lower normalize
     458    [2,3:
     459      #absurd destruct(absurd)
     460    ]
     461    change with (eq_bv 16 ?? = true → ?)
     462    #relevant lapply (eq_bv_eq … relevant)
     463    #word_refl >word_refl %
     464  ]
     465qed.
     466
     467lemma eq_bv_false_to_neq:
     468  ∀n: nat.
     469  ∀left, right: BitVector n.
     470    eq_bv n left right = false → left ≠ right.
     471  #n #left elim left
     472  [1:
     473    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
     474  |2:
     475    #n' #hd #tl #inductive_hypothesis #right
     476    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
     477    >right_refl normalize
     478    cases hd normalize nodelta
     479    cases hd' normalize nodelta
     480    [2,3:
     481      #_ @nmk #absurd destruct(absurd)
     482    ]
     483    change with (eq_bv ??? = false → ?)
     484    #relevant lapply (inductive_hypothesis … relevant)
     485    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
     486    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
     487  ]
     488qed.
     489   
     490lemma eq_accumulator_address_map_entry_false_to_neq:
     491  ∀left: accumulator_address_map_entry.
     492  ∀right: accumulator_address_map_entry.
     493    eq_accumulator_address_map_entry left right = false → left ≠ right.
     494  #left #right cases left cases right
     495  [1:
     496    normalize #absurd destruct(absurd)
     497  |2,3:
     498    #upper_lower #word normalize #_
     499    @nmk #absurd destruct(absurd)
     500  |4:
     501    #upper_lower #word #upper_lower' #word' normalize
     502    cases upper_lower' normalize nodelta
     503    cases upper_lower normalize nodelta
     504    [2,3:
     505      #_ @nmk #absurd destruct(absurd)
     506    ]
     507    change with (eq_bv ??? = false → ?)
     508    #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
     509    #word_neq_assm @nmk #address_eq_assm cases word_neq_assm
     510    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
     511  ]
     512qed.
     513
    386514(* XXX: changed this type.  Bool specifies whether byte is first or second
    387515        component of an address, and the Word is the pseudoaddress that it
     
    389517        A.
    390518*)
    391 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
     519definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
    392520
    393521include alias "ASM/BitVectorTrie.ma".
     
    402530
    403531axiom low_internal_ram_of_pseudo_internal_ram_hit:
    404  ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
    405   assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
     532 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
     533  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
    406534   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    407535   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
     
    409537   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
    410538   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
    411      if high then
     539     if eq_upper_lower upper_lower upper then
    412540       (pbl = higher) ∧ (bl = phigher)
    413541     else
     
    426554   match addr with
    427555    [ DIRECT d ⇒
    428        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    429        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     556        if eq_bv … d (bitvector_of_nat … 224) then
     557          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
     558        else
     559         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    430560    | INDIRECT i ⇒
    431561       let d ≝ get_register … s [[false;false;i]] in
    432        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    433        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     562       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
    434563    | EXT_INDIRECT _ ⇒ true
    435     | REGISTER _ ⇒ true
    436     | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
     564    | REGISTER r ⇒
     565        let address ≝ bit_address_of_register … s r in
     566          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
     567    | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
    437568    | ACC_B ⇒ true
    438569    | DPTR ⇒ true
     
    448579    | RELATIVE _ ⇒ true
    449580    | ADDR11 _ ⇒ true
    450     | ADDR16 _ ⇒ true ].
     581    | ADDR16 _ ⇒ true
     582    ].
    451583   
    452584definition next_internal_pseudo_address_map0 ≝
     
    464596      let a' ≝ addr_of a s in
    465597      let 〈callM, accM〉 ≝ M in
    466          Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
    467                  〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
     598         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
     599                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
    468600    | Mov _ _ ⇒ Some … M
    469601    | Instruction instr ⇒
    470        match instr with
    471         [ ADD addr1 addr2 ⇒
    472            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     602      match instr return λx. option internal_pseudo_address_map with
     603       [ ADD addr1 addr2 ⇒
     604         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     605           Some ? M
     606         else
     607           None ?
     608       | ADDC addr1 addr2 ⇒
     609         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     610           Some ? M
     611         else
     612           None ?
     613       | SUBB addr1 addr2 ⇒
     614         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     615           Some ? M
     616         else
     617           None ?
     618       | INC addr1 ⇒
     619         if addressing_mode_ok T M ? s addr1 then
     620           Some ? M
     621         else
     622           None ?
     623       | DEC addr1 ⇒
     624         if addressing_mode_ok T M … s addr1 then
     625           Some ? M
     626         else
     627           None ?
     628       | MUL addr1 addr2 ⇒
     629         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     630           Some ? M
     631         else
     632           None ?
     633       | DIV addr1 addr2 ⇒
     634         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     635           Some ? M
     636         else
     637           None ?
     638       | DA addr1 ⇒
     639         if addressing_mode_ok T M … s addr1 then
     640           Some ? M
     641         else
     642           None ?
     643       | JC addr1 ⇒ Some ? M
     644       | JNC addr1 ⇒ Some ? M
     645       | JB addr1 addr2 ⇒ Some ? M
     646       | JNB addr1 addr2 ⇒ Some ? M
     647       | JBC addr1 addr2 ⇒ Some ? M
     648       | JZ addr1 ⇒ Some ? M
     649       | JNZ addr1 ⇒ Some ? M
     650       | CJNE addr1 addr2 ⇒
     651         match addr1 with
     652         [ inl l ⇒
     653           let 〈left, right〉 ≝ l in
     654             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     655               Some ? M
     656             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     657               Some ? M
     658             else
     659               None ?
     660         | inr r ⇒
     661           let 〈left, right〉 ≝ r in
     662             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     663               Some ? M
     664             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     665               Some ? M
     666             else
     667               None ?
     668         ]
     669       | DJNZ addr1 addr2 ⇒
     670         if addressing_mode_ok T M … s addr1 then
     671           Some ? M
     672         else
     673           None ?
     674       | CLR addr1 ⇒
     675         if addressing_mode_ok T M … s addr1 then
     676           Some ? M
     677         else
     678           None ?
     679       | CPL addr1 ⇒
     680         if addressing_mode_ok T M … s addr1 then
     681           Some ? M
     682         else
     683           None ?
     684       | RL addr1 ⇒
     685         if addressing_mode_ok T M … s addr1 then
     686           Some ? M
     687         else
     688           None ?
     689       | RLC addr1 ⇒
     690         if addressing_mode_ok T M … s addr1 then
     691           Some ? M
     692         else
     693           None ?
     694       | RR addr1 ⇒
     695         if addressing_mode_ok T M … s addr1 then
     696           Some ? M
     697         else
     698           None ?
     699       | RRC addr1 ⇒
     700         if addressing_mode_ok T M … s addr1 then
     701           Some ? M
     702         else
     703           None ?
     704       | SWAP addr1 ⇒
     705         if addressing_mode_ok T M … s addr1 then
     706           Some ? M
     707         else
     708           None ?
     709       | SETB addr1 ⇒
     710         if addressing_mode_ok T M … s addr1 then
     711           Some ? M
     712         else
     713           None ?
     714       (* XXX: need to track addresses pushed and popped off the stack? *)
     715       | PUSH addr1 ⇒
     716         let 〈callM, accM〉 ≝ M in
     717         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
     718         [ DIRECT d ⇒ λproof.
     719           let extended ≝ pad 8 8 d in
     720             Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
     721         | _ ⇒ λother: False. ⊥
     722         ] (subaddressing_modein … addr1)
     723       | POP addr1 ⇒ Some … M
     724       | XCH addr1 addr2 ⇒
     725         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     726           Some ? M
     727         else
     728           None ?
     729       | XCHD addr1 addr2 ⇒
     730         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     731           Some ? M
     732         else
     733           None ?
     734      | RET ⇒
     735        let 〈callM, accM〉 ≝ M in
     736        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     737        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     738          if sp_plus_1 ∧ sp_plus_2 then
     739            Some … M
     740          else
     741            None ?
     742      | RETI ⇒
     743        let 〈callM, accM〉 ≝ M in
     744        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     745        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     746          if sp_plus_1 ∧ sp_plus_2 then
     747            Some … M
     748          else
     749            None ?
     750      | NOP ⇒ Some … M
     751      | MOVX addr1 ⇒ Some … M
     752      | XRL addr1 ⇒
     753        match addr1 with
     754        [ inl l ⇒
     755          let 〈acc_a, others〉 ≝ l in
     756          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     757          let others_ok ≝ addressing_mode_ok T M … s others in
     758          if acc_a_ok ∧ others_ok then
    473759            Some ? M
    474            else
     760          else
    475761            None ?
    476         | ADDC addr1 addr2 ⇒
    477            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     762        | inr r ⇒
     763          let 〈direct, others〉 ≝ r in
     764          let direct_ok ≝ addressing_mode_ok T M … s direct in
     765          let others_ok ≝ addressing_mode_ok T M … s others in
     766          if direct_ok ∧ others_ok then
    478767            Some ? M
    479            else
     768          else
    480769            None ?
    481         | SUBB addr1 addr2 ⇒
    482            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     770        ]
     771      | ORL addr1 ⇒
     772        match addr1 with
     773        [ inl l ⇒
     774          match l with
     775          [ inl l ⇒
     776            let 〈acc_a, others〉 ≝ l in
     777            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     778            let others_ok ≝ addressing_mode_ok T M … s others in
     779            if acc_a_ok ∧ others_ok then
     780              Some ? M
     781            else
     782              None ?
     783          | inr r ⇒
     784            let 〈direct, others〉 ≝ r in
     785            let direct_ok ≝ addressing_mode_ok T M … s direct in
     786            let others_ok ≝ addressing_mode_ok T M … s others in
     787            if direct_ok ∧ others_ok then
     788              Some ? M
     789            else
     790              None ?
     791          ]
     792        | inr r ⇒
     793          let 〈carry, others〉 ≝ r in
     794          let carry_ok ≝ addressing_mode_ok T M … s carry in
     795          let others_ok ≝ addressing_mode_ok T M … s others in
     796          if carry_ok ∧ others_ok then
    483797            Some ? M
    484            else
    485             None ?       
    486         | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
     798          else
     799            None ?
     800        ]
     801      | ANL addr1 ⇒
     802        match addr1 with
     803        [ inl l ⇒
     804          match l with
     805          [ inl l ⇒
     806            let 〈acc_a, others〉 ≝ l in
     807            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     808            let others_ok ≝ addressing_mode_ok T M … s others in
     809            if acc_a_ok ∧ others_ok then
     810              Some ? M
     811            else
     812              None ?
     813          | inr r ⇒
     814            let 〈direct, others〉 ≝ r in
     815            let direct_ok ≝ addressing_mode_ok T M … s direct in
     816            let others_ok ≝ addressing_mode_ok T M … s others in
     817            if direct_ok ∧ others_ok then
     818              Some ? M
     819            else
     820              None ?
     821          ]
     822        | inr r ⇒
     823          let 〈carry, others〉 ≝ r in
     824          let carry_ok ≝ addressing_mode_ok T M … s carry in
     825          let others_ok ≝ addressing_mode_ok T M … s others in
     826          if carry_ok ∧ others_ok then
     827            Some ? M
     828          else
     829            None ?
     830        ]
     831      | MOV addr1 ⇒ Some … M
     832      ]
     833    ].
     834    cases other
     835qed.
    487836
    488837definition next_internal_pseudo_address_map ≝
     
    509858  λsigma: Word → Word.
    510859    match \snd M with
    511     [ None ⇒ sfrs
    512     | Some s ⇒
    513       let 〈high, address〉 ≝ s in
     860    [ data ⇒ sfrs
     861    | address upper_lower address ⇒
    514862      let index ≝ sfr_8051_index SFR_ACC_A in
    515       let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
    516         if high then
    517           set_index Byte 19 sfrs index upper ?
     863      let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
     864        if eq_upper_lower upper_lower upper then
     865          set_index Byte 19 sfrs index high ?
    518866        else
    519           set_index Byte 19 sfrs index lower ?
     867          set_index Byte 19 sfrs index low ?
    520868    ].
    521869  //
     
    640988*)
    641989
    642 (* XXX: check values returned for conditional jumps below! *)
     990(* XXX: check values returned for conditional jumps below! They are wrong,
     991        find correct values *)
    643992definition ticks_of0:
    644993    ∀p:pseudo_assembly_program.
    645       (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     994      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
    646995  λprogram: pseudo_assembly_program.
     996  λlookup_labels: Identifier → Word.
    647997  λsigma.
    648998  λpolicy.
     
    6531003      match instr with
    6541004      [ JC lbl ⇒
    655         if policy ppc then
    656           〈4, 4〉
    657         else
    658           〈2, 2〉
     1005        let lookup_address ≝ sigma (lookup_labels lbl) in
     1006        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1007        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1008          if sj_possible then
     1009            〈2, 2〉
     1010          else
     1011            〈4, 4〉
    6591012      | JNC lbl ⇒
    660         if policy ppc then
    661           〈4, 4〉
    662         else
    663           〈2, 2〉
     1013        let lookup_address ≝ sigma (lookup_labels lbl) in
     1014        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1015        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1016          if sj_possible then
     1017            〈2, 2〉
     1018          else
     1019            〈4, 4〉
    6641020      | JB bit lbl ⇒
    665         if policy ppc then
    666           〈4, 4〉
    667         else
    668           〈2, 2〉
     1021        let lookup_address ≝ sigma (lookup_labels lbl) in
     1022        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1023        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1024          if sj_possible then
     1025            〈2, 2〉
     1026          else
     1027            〈4, 4〉
    6691028      | JNB bit lbl ⇒
    670         if policy ppc then
    671           〈4, 4〉
    672         else
    673           〈2, 2〉
     1029        let lookup_address ≝ sigma (lookup_labels lbl) in
     1030        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1031        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1032          if sj_possible then
     1033            〈2, 2〉
     1034          else
     1035            〈4, 4〉
    6741036      | JBC bit lbl ⇒
    675         if policy ppc then
    676           〈4, 4〉
    677         else
    678           〈2, 2〉
     1037        let lookup_address ≝ sigma (lookup_labels lbl) in
     1038        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1039        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1040          if sj_possible then
     1041            〈2, 2〉
     1042          else
     1043            〈4, 4〉
    6791044      | JZ lbl ⇒
    680         if policy ppc then
    681           〈4, 4〉
    682         else
    683           〈2, 2〉
     1045        let lookup_address ≝ sigma (lookup_labels lbl) in
     1046        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1047        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1048          if sj_possible then
     1049            〈2, 2〉
     1050          else
     1051            〈4, 4〉
    6841052      | JNZ lbl ⇒
    685         if policy ppc then
    686           〈4, 4〉
    687         else
    688           〈2, 2〉
     1053        let lookup_address ≝ sigma (lookup_labels lbl) in
     1054        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1055        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1056          if sj_possible then
     1057            〈2, 2〉
     1058          else
     1059            〈4, 4〉
    6891060      | CJNE arg lbl ⇒
    690         if policy ppc then
    691           〈4, 4〉
    692         else
    693           〈2, 2〉
     1061        let lookup_address ≝ sigma (lookup_labels lbl) in
     1062        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1063        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1064          if sj_possible then
     1065            〈2, 2〉
     1066          else
     1067            〈4, 4〉
    6941068      | DJNZ arg lbl ⇒
    695         if policy ppc then
    696           〈4, 4〉
    697         else
    698           〈2, 2〉
     1069        let lookup_address ≝ sigma (lookup_labels lbl) in
     1070        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1071        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1072          if sj_possible then
     1073            〈2, 2〉
     1074          else
     1075            〈4, 4〉
    6991076      | ADD arg1 arg2 ⇒
    7001077        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     
    7851162    | Cost cost ⇒ 〈0, 0〉
    7861163    | Jmp jmp ⇒
    787       if policy ppc then
    788         〈4, 4〉
     1164      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1165      let do_a_long ≝ policy ppc in
     1166      let lookup_address ≝ sigma (lookup_labels jmp) in
     1167      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1168        if sj_possible ∧ ¬ do_a_long then
     1169          〈2, 2〉 (* XXX: SJMP *)
     1170        else
     1171        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1172          if mj_possible ∧ ¬ do_a_long then
     1173            〈2, 2〉 (* XXX: AJMP *)
     1174          else
     1175            〈2, 2〉 (* XXX: LJMP *)
     1176    | Call call ⇒
     1177      (* XXX: collapse the branches as they are identical? *)
     1178      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1179      let lookup_address ≝ sigma (lookup_labels call) in
     1180      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1181      let do_a_long ≝ policy ppc in
     1182      if mj_possible ∧ ¬ do_a_long then
     1183        〈2, 2〉 (* ACALL *)
    7891184      else
    790         〈2, 2〉
    791     | Call call ⇒
    792       if policy ppc then
    793         〈4, 4〉
    794       else
    795         〈2, 2〉
     1185        〈2, 2〉 (* LCALL *)
    7961186    | Mov dptr tgt ⇒ 〈2, 2〉
    7971187    ].
     
    7991189definition ticks_of:
    8001190    ∀p:pseudo_assembly_program.
    801       (Word → Word) → (Word → bool) → ∀ppc:Word.
     1191      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
    8021192       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    8031193  λprogram: pseudo_assembly_program.
     1194  λlookup_labels.
    8041195  λsigma.
    8051196  λpolicy.
     
    8071198    let pseudo ≝ \snd program in
    8081199    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    809      ticks_of0 program sigma policy ppc fetched.
     1200     ticks_of0 program lookup_labels sigma policy ppc fetched.
    8101201
    8111202(*
Note: See TracChangeset for help on using the changeset viewer.