Changeset 825


Ignore:
Timestamp:
May 23, 2011, 6:12:51 PM (8 years ago)
Author:
mulligan
Message:

lots of refactoring, finally got something to prove

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r820 r825  
    410410qed.
    411411
    412 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    413   λp.
    414     let 〈preamble, instr_list〉 ≝ p in
    415     let 〈datalabels, ignore〉 ≝
    416       foldl ((BitVectorTrie Identifier 16) × nat) ? (
    417         λt. λpreamble.
    418           let 〈datalabels, addr〉 ≝ t in
    419           let 〈name, size〉 ≝ preamble in
    420           let addr_16 ≝ bitvector_of_nat 16 addr in
    421             〈insert ? ? name addr_16 datalabels, addr + size〉)
    422               〈(Stub ? ?), 0〉 preamble in
    423     let 〈labels,pc_costs〉 ≝
    424       foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
    425         λt. λi.
    426           let 〈label, i〉 ≝ i in
    427           let 〈labels, pc_costs〉 ≝ t in
    428           let 〈program_counter, costs〉 ≝ pc_costs in
    429           let labels ≝ match label with
    430           [ None ⇒ labels
    431           | Some label ⇒
    432             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    433               insert ? ? label program_counter_bv labels
    434           ] in
    435           〈labels,
     412definition assembly_expansion ≝
     413  λi.
     414  λcosts: BitVectorTrie Identifier 16.
     415  λprogram_counter: nat.
    436416            match i with
    437417              [ Instruction instr ⇒
     
    449429              | Call call ⇒
    450430                  〈program_counter + 3, costs〉
    451               | Mov dptr trgt ⇒ pc_costs
    452               ]〉
     431              | Mov dptr trgt ⇒ 〈program_counter, costs〉
     432              ].
     433
     434definition assembly_1_pseudoinstruction ≝
     435  λlookup_labels.
     436  λlookup_datalabels.
     437  λaddress_of.
     438  λi: labelled_instruction.
     439                match \snd i with
     440                  [ Cost cost ⇒ [ ]
     441                  | Comment comment ⇒ [ ]
     442                  | Call call ⇒
     443                    let address ≝ ADDR16 (lookup_labels call) in
     444                      assembly1 (LCALL address)
     445                  | Mov d trgt ⇒
     446                    let address ≝ DATA16 (lookup_datalabels trgt) in
     447                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
     448                  | Instruction instr ⇒ assembly_preinstruction ? address_of instr
     449                  | Jmp jmp ⇒
     450                    let address ≝ ADDR16 (lookup_labels jmp) in
     451                      assembly1 (LJMP address)
     452(*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
     453*)
     454                  ].
     455  @ I
     456qed.
     457
     458definition construct_datalabels ≝
     459  λpreamble.
     460    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
     461    λt. λpreamble.
     462      let 〈datalabels, addr〉 ≝ t in
     463      let 〈name, size〉 ≝ preamble in
     464      let addr_16 ≝ bitvector_of_nat 16 addr in
     465        〈insert ? ? name addr_16 datalabels, addr + size〉)
     466          〈(Stub ? ?), 0〉 preamble).
     467
     468definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     469  λp.
     470    let 〈preamble, instr_list〉 ≝ p in
     471    let datalabels ≝ construct_datalabels preamble in
     472    let 〈labels,pc_costs〉 ≝
     473      foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
     474        λt. λi.
     475          let 〈label, i〉 ≝ i in
     476          let 〈labels, pc_costs〉 ≝ t in
     477          let 〈program_counter, costs〉 ≝ pc_costs in
     478          let labels ≝ match label with
     479          [ None ⇒ labels
     480          | Some label ⇒
     481            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     482              insert ? ? label program_counter_bv labels
     483          ] in
     484          〈labels, assembly_expansion i costs program_counter〉
    453485          ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
    454486    let 〈program_counter, costs〉 ≝ pc_costs in
     
    456488        None ?
    457489      else
    458         let flat_list ≝
    459           flatten ? (
    460             map ? ? (
    461               λi: labelled_instruction.
    462                 match \snd i with
    463                   [ Cost cost ⇒ [ ]
    464                   | Comment comment ⇒ [ ]
    465                   | Call call ⇒
    466                     let pc_offset ≝ lookup ? ? call labels (zero ?) in
    467                     let address ≝ ADDR16 pc_offset in
    468                       assembly1 (LCALL address)
    469                   | Mov d trgt ⇒
    470                     let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in
    471                     let address ≝ DATA16 pc_offset in
    472                       assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
    473                   | Instruction instr ⇒ assembly_preinstruction ? (address_of labels) instr
    474                   | Jmp jmp ⇒
    475                     let pc_offset ≝ lookup ? ? jmp labels (zero ?) in
    476                     let address ≝ ADDR16 pc_offset in
    477                       assembly1 (LJMP address)
    478 (*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
    479 *)
    480                   ]
    481             ) instr_list
    482           ) in
     490        let flat_list ≝ flatten ? (
     491          map ? ? (
     492            assembly_1_pseudoinstruction (
     493              λx. lookup ? ? x labels (zero ?))
     494                (λx. lookup ? ? x datalabels (zero ?))
     495                (address_of labels)) instr_list) in
    483496        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
     497(*
    484498  [2,3,4,5,6:
    485499    normalize; %;
     
    495509      ]
    496510  ]
    497 qed.
     511qed. *)
    498512
    499513definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  • src/ASM/AssemblyProof.ma

    r823 r825  
    22include "ASM/Interpret.ma".
    33
     4let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     5                       (encoding: list Byte) on encoding: Prop ≝
     6  match encoding with
     7  [ nil ⇒ final_pc = pc
     8  | cons hd tl ⇒
     9    let 〈new_pc, byte〉 ≝ next code_memory pc in
     10      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
     11  ].
     12
     13definition invariant:
     14  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
     15  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
     16  λsigma.
     17  λpseudo_assembly_program.
     18  λcode_mem.
     19    ∀pc: Word.
     20      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
     21      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
     22      let address_of ≝ ? in
     23      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
     24      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
     25      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
     26        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
     27      cases not_implemented
     28qed.
  • src/ASM/Interpret.ma

    r822 r825  
    632632qed.
    633633
    634 definition fetch_pseudo_instruction: PseudoStatus → Word → (Word → nat) → ((pseudo_instruction × Word) × nat) ≝
    635   λps: PseudoStatus.
     634definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     635  λcode_mem.
    636636  λpc: Word.
    637   λticks_of: Word → nat.
    638     let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … (code_memory ? ps) ? in
     637    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    639638    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
    640       〈〈instr, new_pc〉, ticks_of pc〉.
     639      〈instr, new_pc〉.
    641640    cases not_implemented.
    642641qed.
     
    668667    ].
    669668
     669definition address_of_word_labels_code_mem ≝
     670  λcode_mem.
     671  λid: Identifier.
     672    bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem).
     673
    670674definition address_of_word_labels ≝
    671675  λps: PseudoStatus.
    672676  λid: Identifier.
    673     bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) (code_memory ? ps)).
     677    address_of_word_labels_code_mem (code_memory ? ps) id.
    674678
    675679definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
    676680  λticks_of.
    677681  λs.
    678   let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) ticks_of in
    679   let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     682  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code_memory ? s) (program_counter ? s) in
     683  let ticks ≝ ticks_of (program_counter ? s) in
    680684  let s ≝ set_clock ? s (clock ? s + ticks) in
    681685  let s ≝ set_program_counter ? s pc in
Note: See TracChangeset for help on using the changeset viewer.