Changeset 922 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 9, 2011, 3:38:47 PM (9 years ago)
Author:
mulligan
Message:

changes to get assemblyproof to compile

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r920 r922  
    654654definition assembly_1_pseudoinstruction ≝
    655655  λprogram: pseudo_assembly_program.
     656  λppc: Word.
    656657  λpc: Word.
    657658  λlookup_labels.
    658659  λlookup_datalabels.
    659660  λi.
    660   let expansion ≝ jump_expansion pc program in
     661  let expansion ≝ jump_expansion ppc program in
    661662    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    662663    [ None ⇒ None ?
     
    664665      let mapped ≝ map ? ? assembly1 pseudos in
    665666      let flattened ≝ flatten ? mapped in
    666       let len ≝ length ? flattened in
    667         Some ? (〈len, flattened〉)
     667      let pc_len ≝ length ? flattened in
     668        Some ? (〈pc_len, flattened〉)
    668669    ].
    669670 
     
    680681definition construct_costs ≝
    681682  λprogram.
     683  λpseudo_program_counter: nat.
    682684  λprogram_counter: nat.
    683685  λlookup_labels.
     
    691693  | _ ⇒
    692694    let pc_bv ≝ bitvector_of_nat ? program_counter in
     695    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
    693696    let pc_delta_assembled ≝
    694       assembly_1_pseudoinstruction program pc_bv
     697      assembly_1_pseudoinstruction program ppc_bv pc_bv
    695698        lookup_labels lookup_datalabels i
    696699    in
     
    705708definition build_maps ≝
    706709  λinstr_list.
    707   let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ?
     710  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ?
    708711    (λt. λi.
    709712       let 〈label, i〉 ≝ i in
     
    711714       [ None ⇒ None ?
    712715       | Some t ⇒
    713          let 〈labels, pc_costs〉 ≝ t in
    714          let 〈program_counter, costs〉 ≝ pc_costs in
     716         let 〈labels, pc_ppc_costs〉 ≝ t in
     717         let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in
     718         let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in
    715719         let labels ≝
    716720           match label with
     
    721725           ]
    722726         in
    723            match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with
     727           match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with
    724728           [ None ⇒ None ?
    725            | Some construct ⇒ Some ? 〈labels, construct
     729           | Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉
    726730           ]
    727        ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
     731       ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in
    728732  match result with
    729733  [ None ⇒ None ?
    730734  | Some result ⇒
    731     let 〈labels, pc_costs〉 ≝ result in
    732     let 〈pc, costs〉 ≝ pc_costs in
     735    let 〈labels, pc_ppc_costs〉 ≝ result in
     736    let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in
     737    let 〈ppc, costs〉 ≝ ppc_costs in
    733738      if gtb pc (2^16) then
    734739        None ?
     
    751756            [ None ⇒ None ?
    752757            | Some lst ⇒
    753               let 〈pc, y〉 ≝ lst in
    754               let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
     758              let 〈pc, ppc_y〉 ≝ lst in
     759              let 〈ppc, y〉 ≝ ppc_y in
     760              let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
    755761              match x with
    756762              [ None ⇒ None ?
     
    758764                let 〈pc_delta, program〉 ≝ x in
    759765                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    760                   Some ? 〈new_pc, (program @ y)〉
     766                let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     767                  Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
    761768              ]
    762             ]) (Some ? 〈(zero ?), [ ]〉) instr_list
     769            ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
    763770        in
    764771          match result with
    765772          [ None ⇒ None ?
    766           | Some result ⇒ Some ? (〈\snd result, costs〉)
     773          | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)
    767774          ]
    768775      ].
Note: See TracChangeset for help on using the changeset viewer.