Changeset 3039 for src/ASM/Interpret2.ma

Timestamp:

Mar 29, 2013, 5:45:14 PM (8 years ago)

Author:

tranquil

Message:

• merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

• JMP now correctly uses ACCDPTR argument
• LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

File:

• src/ASM/Interpret2.ma (modified) (6 diffs)

src/ASM/Interpret2.ma

@@ -51 +51 @@
 (* Move next function in interpret? *)
 definition execute_1_pseudo_instruction':
- ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
- λcm,sigma,policy,status.
+ ∀cm.(Identifier → Word) → (Identifier → Word) →
+ ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
+ λcm,addr_of_label,addr_of_symbol,sigma,policy,status.
   execute_1_pseudo_instruction cm
-   (ticks_of cm  sigma policy) status ….
+   (ticks_of cm  sigma policy) addr_of_label addr_of_symbol status ….
 cases daemon (*CSC: we need to prove that we remain inside the program
  (code closed), which is impossible in case of function pointers.
@@ -68 +69 @@
   | Jmp _ ⇒ cl_other
   | Jnz _ _ _ ⇒ cl_jump
-  | MovSuccessor _ _ _ ⇒ cl_other
   | Call _ ⇒ cl_call
-  | Mov _ _ ⇒ cl_other ].
+  | Mov _ _ _ ⇒ cl_other ].
 
 definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
@@ -108 +108 @@
 
 definition ASM_as_call_ident:
- ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
+ ∀prog.(Identifier → Word) → (Identifier → Word) →
+ ∀sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
 ≝
- λprog,sigma,policy,s0.
-  let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
+ λprog,addr_of_label,addr_of_symbol,sigma,policy,s0.
+  let st ≝ execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol
+    sigma policy s0 in
   let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
   match lbl with
@@ -122 +124 @@
 
 definition ASM_abstract_status:
- ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
-  λprog,sigma,policy.
+ ∀prog:pseudo_assembly_program.
+  (Identifier → Word) →
+  (Identifier → Word) → 
+ ∀sigma,policy.abstract_status ≝
+  λprog,addr_of_label,addr_of_symbol,sigma,policy.
     mk_abstract_status
       (PseudoStatus prog)
-      (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
+      (λs1,s2. execute_1_pseudo_instruction' … addr_of_label addr_of_symbol
+        sigma policy s1 = s2)
       word_deqset
       (program_counter …)
@@ -133 +139 @@
       (ASM_next_instruction_properly_relates_program_counters prog)
       (ASM_as_result …)
-      (ASM_as_call_ident prog sigma policy …)
+      (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
       ?.
  * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
@@ -142 +148 @@
  pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
  λc,sigma,policy.
+  let label_map ≝ \fst (create_label_cost_map (code … c)) in
+  let symbol_map ≝ construct_datalabels (preamble … c) in
+  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
+  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
   mk_preclassified_system_of_abstract_status
    (pseudo_assembly_program × (Word → Word) × (Word → bool))
-   (ASM_abstract_status c sigma policy)
-   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
+   (ASM_abstract_status c addr_of_label addr_of_symbol sigma policy)
+   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    (initialise_status … c).