Changeset 410

Timestamp:

Dec 13, 2010, 5:00:02 PM (9 years ago)

Author:

mulligan

Message:

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

Location:

Deliverables/D4.1/Matita

Files:

• ASM.ma (modified) (1 diff)
• Assembly.ma (modified) (2 diffs)
• BitVector.ma (modified) (2 diffs)
• Compare.ma (added)
• Map.ma (added)
• Nat.ma (modified) (1 diff)
• depends (modified) (1 diff)

Deliverables/D4.1/Matita/ASM.ma

@@ -195 +195 @@
  | Call: String → labelled_instruction
  | Mov: [[dptr]] → String → labelled_instruction
- | WithLabel: preinstruction String → labelled_instruction.
+ | Label: String → labelled_instruction
+ | WithLabel: jump String → labelled_instruction.
 
 ndefinition preamble ≝ List (String × Nat).

Deliverables/D4.1/Matita/Assembly.ma

@@ -1 +1 @@
 include "ASM.ma".
+include "BitVectorTrie.ma".
 
 ndefinition assembly1 ≝
@@ -400 +401 @@
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
 
+include "Arithmetic.ma".
+include "Fetch.ma".
+include "Status.ma".
+
+ndefinition assembly_jump ≝
+  λA, B: Type[0].
+  λj.
+  λaddr_of: A → B.
+    match j with
+      [ JC jmp ⇒ JC ? (addr_of jmp)
+      | JNC jmp ⇒ JNC ? (addr_of jmp)
+      | JZ jmp ⇒ JZ ? (addr_of jmp)
+      | JNZ jmp ⇒ JNZ ? (addr_of jmp)
+      | JB jmp jmp' ⇒ JB ? jmp (addr_of jmp')
+      | JNB jmp jmp' ⇒ JNB ? jmp (addr_of jmp')
+      | JBC jmp jmp' ⇒ JBC ? jmp (addr_of jmp')
+      | CJNE jmp jmp' ⇒ CJNE ? jmp (addr_of jmp')
+      | DJNZ jmp jmp' ⇒ DJNZ ? jmp (addr_of jmp')
+      ].
+
+ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝
+  λp.
+    let 〈preamble, instr_list〉 ≝ p in
+    let 〈datalabels, ignore〉 ≝
+      fold_left ? ? (
+        λt. λpreamble.
+          let 〈datalabels, addr〉 ≝ t in
+          let 〈name, size〉 ≝ preamble in
+          let addr_sixteen ≝ bitvector_of_nat sixteen addr in
+            〈insert ? ? addr_sixteen name datalabels, addr + size〉)
+              〈(Stub ? ?), Z〉 preamble in
+    let 〈pc_labels, costs〉 ≝
+      fold_left ? ? (
+        λt. λi.
+          let 〈pc_labels, costs〉 ≝ t in
+          let 〈program_counter, labels〉 ≝ pc_labels in
+            match i with
+              [ Instruction instr ⇒
+                let code_memory ≝ load_code_memory (assembly1 instr) in
+                let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
+                let 〈instr', program_counter'〉 ≝ instr_pc' in
+                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
+                  〈〈program_counter + program_counter_n', labels〉, costs〉
+              | Label label ⇒
+                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
+                  〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉
+              | Cost cost ⇒
+                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
+                  〈pc_labels, (insert ? ? program_counter_bv cost costs)〉
+              | Jmp jmp ⇒
+                  〈〈program_counter + three, labels〉, costs〉
+              | Call call ⇒
+                  〈〈program_counter + three, labels〉, costs〉
+              | Mov dptr trgt ⇒ t
+              | WithLabel jmp ⇒ ? (*
+                let fake_addr ≝ RELATIVE (zero eight) in
+                let fake_jump ≝ assembly_jump ? ? jmp (λx. fake_addr) in
+                let code_memory ≝ load_code_memory (assembly1 (Jump relative fake_jump)) in
+                let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
+                let 〈instr', program_counter'〉 ≝ instr_pc' in
+                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
+                  〈〈program_counter + program_counter_n', labels〉, costs〉 *)
+              ]
+          ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
+    let 〈program_counter, labels〉 ≝ pc_labels in
+      if greater_than_b program_counter
+                        sixty_five_thousand_five_hundred_and_thirty_six then
+        Nothing ?
+      else
+        let flat_list ≝
+          flatten ? (
+            map ? ? (
+              λi: labelled_instruction.
+                match i with
+                  [ Cost cost ⇒ [ ]
+                  | Label label ⇒ [ ]
+                  | Call call ⇒
+                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
+                    let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in
+                      assembly1 (LCALL address)
+                  | _ ⇒ ?
+                  ]
+            ) instr_list
+          ) in
+        Just ? 〈flat_list, costs〉.
+
 (*
 let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty

Deliverables/D4.1/Matita/BitVector.ma

@@ -7 +7 @@
 
 include "Vector.ma".
+include "String.ma".
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -217 +218 @@
         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     ].
+    
+naxiom bitvector_of_string:
+  ∀n: Nat.
+  ∀s: String.
+    BitVector n.
+    
+naxiom string_of_bitvector:
+  ∀n: Nat.
+  ∀b: BitVector n.
+    String.

Deliverables/D4.1/Matita/Nat.ma

@@ -719 +719 @@
 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
 ndefinition two_hundred_and_fifty_six ≝
-  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
+  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.
+ndefinition sixty_five_thousand_five_hundred_and_thirty_six ≝
+  two_hundred_and_fifty_six * two_hundred_and_fifty_six.

Deliverables/D4.1/Matita/depends

@@ -15 +15 @@
 Connectives.ma Plogic/equality.ma
 Bool.ma Universes.ma
-Assembly.ma ASM.ma
+Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
 List.ma Maybe.ma Util.ma
 Interpret.ma Fetch.ma Status.ma
 Util.ma Nat.ma
-BitVector.ma Vector.ma
+BitVector.ma String.ma Vector.ma
 String.ma Char.ma List.ma
 Plogic/equality.ma Universes.ma