Changeset 836 for src/ASM/Assembly.ma

Timestamp:

May 25, 2011, 11:43:42 AM (9 years ago)

Author:

mulligan

Message:

changes to assembly functions

File:

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

src/ASM/Assembly.ma

@@ -544 +544 @@
   λi.
   let expansion ≝ jump_expansion_policy program pc in
-    match (expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i) with
+    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     [ None ⇒ None ?
-    | Some pseudos ⇒ Some ? (flatten ? (map ? ? assembly1 pseudos))
+    | Some pseudos ⇒
+      let mapped ≝ map ? ? assembly1 pseudos in
+      let flattened ≝ flatten ? mapped in
+      let len ≝ length ? flattened in
+        Some ? (〈len, flattened〉)
     ].
 
@@ -588 +592 @@
   | _ ⇒
     let pc_bv ≝ bitvector_of_nat ? program_counter in
-    let assembled ≝ assembly_1_pseudoinstruction program pc_bv
-                     lookup_labels lookup_datalabels i in
-    match assembled with
+    let pc_delta_assembled ≝
+      assembly_1_pseudoinstruction program pc_bv
+        lookup_labels lookup_datalabels i
+    in
+    match pc_delta_assembled with
     [ None ⇒ None ?
-    | Some assembled ⇒
+    | Some pc_delta_assembled ⇒
+      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
       let code_memory ≝ load_code_memory assembled in
       let pc ≝ foldr ? ? (λy. λpc.
@@ -636 +643 @@
   ].
 
-definition assembly ≝
+definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
   λp.
-  λpc.
     let 〈preamble, instr_list〉 ≝ p in
     match build_maps p with
@@ -651 +657 @@
         let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
         let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
-        let to_flatten ≝
-         map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list
-        in
-         foldr ? ? (λx. λy.
+        let result ≝ foldr ? ? (λx. λy.
             match y with
             [ None ⇒ None ?
             | Some lst ⇒
+              let 〈pc, y〉 ≝ lst in
+              let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
               match x with
               [ None ⇒ None ?
-              | Some x ⇒ Some ? (x @ lst)
+              | Some x ⇒
+                let 〈pc_delta, program〉 ≝ x in
+                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
+                  Some ? 〈new_pc, (program @ y)〉
               ]
-            ]) (Some ? [ ]) to_flatten ]].
+            ]) (Some ? 〈(zero ?), [ ]〉) instr_list
+        in
+          match result with
+          [ None ⇒ None ?
+          | Some result ⇒ Some ? (〈\snd result, costs〉)
+          ]
+      ]
+    ].
 
 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝