Changeset 2268


Ignore:
Timestamp:
Jul 26, 2012, 2:56:58 PM (7 years ago)
Author:
mulligan
Message:

Bug spotted in instruction_size (lookup_datalabels cannot just be a constant function!). Fixed rest of file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2264 r2268  
    575575definition instruction_size ≝
    576576  λlookup_labels.
     577  λlookup_datalabels.
    577578  λsigma: Word → Word.
    578579  λpolicy: Word → bool.
    579580  λppc.
    580581  λi.
    581     \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
    582 
     582    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i).
    583583 
    584584(* Labels *)
     
    622622  sigma (zero …) = zero … ∧
    623623  let instr_list ≝ \snd program in
     624  let preamble ≝ \fst program in
    624625  ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
    625626    let pc ≝ sigma ppc in
    626627    let labels ≝ \fst (create_label_cost_map instr_list) in
    627628    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
     629    let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (zero …) in
    628630    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    629631    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    630      next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
     632     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction))
    631633     ∧
    632      (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
     634     (nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction < 2^16
    633635     ∨
    634636     (∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc < nat_of_bitvector … ppc' →
    635637       let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
    636        instruction_size lookup_labels sigma policy ppc' instruction' = 0)
     638       instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0)
    637639     ∧
    638      nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
     640     nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction = 2^16).
    639641
    640642
     
    823825          (|pre| < 2^16 → ∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc ≤ nat_of_bitvector … ppc' →
    824826            let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
    825             instruction_size lookup_labels sigma policy ppc' instruction' = 0)
     827            instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0)
    826828         ) ∧
    827829         ∀ppc'.∀ppc_ok'.
     
    884886      @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2)
    885887      @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok
    886     cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
     888    cut (pc_delta = instruction_size lookup_labels lookup_datalabels sigma policy ppc (\snd hd))
    887889    [ whd in match instruction_size; normalize nodelta
    888890      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
Note: See TracChangeset for help on using the changeset viewer.