Changeset 2268 for src/ASM

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:

• src/ASM/Assembly.ma (modified) (4 diffs)

src/ASM/Assembly.ma

@@ -575 +575 @@
 definition instruction_size ≝
   λlookup_labels.
+  λlookup_datalabels.
   λsigma: Word → Word.
   λpolicy: Word → bool.
   λppc.
   λi.
-    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
-
+    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i).
   
 (* Labels *) 
@@ -622 +622 @@
   sigma (zero …) = zero … ∧
   let instr_list ≝ \snd program in
+  let preamble ≝ \fst program in
   ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
     let pc ≝ sigma ppc in
     let labels ≝ \fst (create_label_cost_map instr_list) in
     let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
+    let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (zero …) in
     let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
     let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
-     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
+     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction))
      ∧
-     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
+     (nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction < 2^16
      ∨
      (∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc < nat_of_bitvector … ppc' →
        let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
-       instruction_size lookup_labels sigma policy ppc' instruction' = 0)
+       instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0)
      ∧
-     nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
+     nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction = 2^16).
 
 
@@ -823 +825 @@
           (|pre| < 2^16 → ∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc ≤ nat_of_bitvector … ppc' →
             let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
-            instruction_size lookup_labels sigma policy ppc' instruction' = 0)
+            instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0)
          ) ∧
          ∀ppc'.∀ppc_ok'.
@@ -884 +886 @@
       @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2)
       @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok
-    cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
+    cut (pc_delta = instruction_size lookup_labels lookup_datalabels sigma policy ppc (\snd hd))
     [ whd in match instruction_size; normalize nodelta
       >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]