Changeset 1486 for src/ASM/ASMCosts.ma

Timestamp:

Nov 3, 2011, 2:36:37 PM (8 years ago)

Author:

mulligan

Message:

finished asm costs

File:

• src/ASM/ASMCosts.ma (modified) (1 diff)

src/ASM/ASMCosts.ma

@@ +1 @@
+include "ASM/ASM.ma".
+include "ASM/Arithmetic.ma".
+include "ASM/Fetch.ma".
+include "ASM/Interpret.ma".
+
+inductive instruction_nature: Type[0] ≝
+  | goto: Word → instruction_nature
+  | branch: Word → instruction_nature
+  | direct_fun_call: Word → instruction_nature
+  | ret: instruction_nature
+  | other: instruction_nature.
+
+definition addr16_of_addr11: Word → Word11 → Word ≝
+  λpc: Word.
+  λa: Word11.
+  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
+  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
+  let 〈b123, b〉 ≝ split … 3 8 a in
+  let b1 ≝ get_index_v … b123 0 ? in
+  let b2 ≝ get_index_v … b123 1 ? in
+  let b3 ≝ get_index_v … b123 2 ? in
+  let p5 ≝ get_index_v … n2 0 ? in
+    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
+  //
+qed.
+
+definition instruction_info:
+    BitVectorTrie Byte 16 → Word → ? ≝
+  λmem.
+  λpc.
+  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
+  let 〈nature, next_pcs〉 ≝
+    match inst with
+    [ RealInstruction ri ⇒
+      match ri with
+      [ RET ⇒ 〈ret, [ ]〉
+      | RETI ⇒ 〈ret, [ ]〉
+      | JC addr ⇒
+        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr)
+      | JNC addr ⇒
+        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr)
+      | JZ addr ⇒
+        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr)
+      | JNZ addr ⇒
+        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr)
+      | JB addr1 addr2 ⇒
+        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr2)
+      | JNB addr1 addr2 ⇒
+        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr2)
+      | JBC addr1 addr2 ⇒
+        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr2)
+      | DJNZ addr1 addr2 ⇒
+        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr2)
+      | CJNE addr1 addr2 ⇒
+        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+        [ RELATIVE addr ⇒ λ_.
+          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
+            〈branch addr, [ next_pc; addr ]〉
+        | _ ⇒ λp. match p in False with [ ]
+        ] (subaddressing_modein … addr2)
+      | _ ⇒ 〈other, [ next_pc ]〉
+      ]
+    | ACALL addr ⇒
+      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
+      [ ADDR11 addr ⇒ λ_.
+        let addr ≝ addr16_of_addr11 pc addr in
+          〈direct_fun_call addr, [ next_pc ]〉
+      | _ ⇒ λp. match p in False with [ ]
+      ] (subaddressing_modein … addr)
+    | LCALL addr ⇒
+      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
+      [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉
+      | _ ⇒ λp. match p in False with [ ]
+      ] (subaddressing_modein … addr)
+    | AJMP addr ⇒
+      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
+      [ ADDR11 addr ⇒ λ_.
+        let addr ≝ addr16_of_addr11 pc addr in
+          〈goto addr, [ addr ]〉
+      | _ ⇒ λp. match p in False with [ ]
+      ] (subaddressing_modein … addr)
+    | LJMP addr ⇒
+      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
+      [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉
+      | _ ⇒ λp. match p in False with [ ]
+      ] (subaddressing_modein … addr)
+    | SJMP addr ⇒
+      match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
+      [ RELATIVE addr ⇒ λ_.
+        let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
+          〈goto addr, [ addr ]〉
+      | _ ⇒ λp. match p in False with [ ]
+      ] (subaddressing_modein … addr)
+    | JMP addr ⇒ 〈other, [ next_pc ]〉
+    | MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉
+    ]
+  in
+    〈nature, next_pc, next_pcs, inst_cost〉.
+
+let rec compare
+  (a: Type[0]) (the_list: list (a × nat))
+    on the_list: nat ≝
+  match the_list with
+  [ nil ⇒ ⊥ (* XXX: was assert false *)
+  | cons hd tl ⇒
+    match tl with
+    [ nil ⇒
+      let 〈pc, cost〉 ≝ hd in
+        cost
+    | cons hd' tl' ⇒
+      let 〈pc1, cost1〉 ≝ hd in
+      let 〈pc2, cost2〉 ≝ hd' in
+        match eq_nat cost1 cost2 with
+        [ true ⇒ max cost1 (compare … tl)
+        | false ⇒ compare … tl'
+        ]
+    ]
+  ].
+  cases daemon
+qed.
+
+let rec block_cost
+  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
+    (the_list: list Word) (program_size: nat)
+      on program_size: nat ≝
+  match program_size with
+  [ O ⇒ 0 (* XXX: empty program *)
+  | S program_size ⇒
+    match the_list with
+    [ nil ⇒ 0 (* XXX: should be empty program *)
+    | cons pc tl ⇒
+      match tl with
+      [ nil ⇒
+        match lookup_opt … pc cost_labels with
+        [ None ⇒
+          let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in
+          let tail ≝ block_cost mem cost_labels next_pcs program_size in
+            cost + tail
+        | Some _ ⇒ O
+        ]
+      | _   ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list)
+      ]
+    ]
+  ].
+
+let rec traverse_code_internal
+  (program: list Byte) (mem: BitVectorTrie Byte 16)
+    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
+      on program: BitVectorTrie nat 8 ≝
+  let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in
+  match program with
+  [ nil ⇒ Stub …
+  | cons hd tl ⇒
+    match lookup_opt … pc cost_labels with
+    [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
+    | Some lbl ⇒
+      let cost ≝ block_cost mem cost_labels [ pc ] program_size in
+      let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
+        insert … lbl cost cost_mapping
+    ]
+  ].
+
+definition traverse_code ≝
+  λprogram: list Byte.
+  λmem: BitVectorTrie Byte 16.
+  λcost_labels.
+  λprogram_size: nat.
+    traverse_code_internal program mem cost_labels (zero …) program_size.
+
+let rec first_cost_label_internal
+  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
+    (program_size: nat) (oldpc: Word)
+      on program_size: (Byte × nat) ≝
+  match program_size with
+  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
+  | S program_size ⇒
+    match lookup_opt … oldpc cost_labels with
+    [ None ⇒
+      let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in
+        match nature with
+        [ direct_fun_call addr ⇒
+          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
+            〈lbl, inst_cost + cost〉
+        | other ⇒
+          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
+            〈lbl, inst_cost + cost〉
+        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
+        ]
+    | Some cost ⇒ 〈cost, 0〉
+    ]
+  ].
+  cases daemon
+qed.
+
+definition first_cost_label ≝
+  λmem: BitVectorTrie Byte 16.
+  λcost_labels: BitVectorTrie Byte 16.
+  λprogram_size: nat.
+    first_cost_label_internal mem cost_labels program_size (zero …).
+
+definition initialize_costs ≝
+  λmem: BitVectorTrie Byte 16.
+  λcost_labels: BitVectorTrie Byte 16.
+  λcost_mapping: BitVectorTrie nat 8.
+  λprogram_size: nat.
+  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
+  let old_cost ≝
+    match lookup_opt … lbl cost_mapping with
+    [ None ⇒ 0
+    | Some cost ⇒ cost
+    ]
+  in
+  let new_cost ≝ old_cost + cost in
+    insert … lbl new_cost cost_mapping.
+
+definition compute_costs ≝
+  λprogram: list Byte.
+  λcost_labels: BitVectorTrie Byte 16.
+  λhas_main: bool.
+  let program_size ≝ |program| in
+  let memory ≝ load_code_memory program in
+  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
+    match has_main with
+    [ true ⇒
+      initialize_costs memory cost_labels costs_mapping program_size
+    | false ⇒ costs_mapping
+    ].