Changeset 3064

Timestamp:

Apr 2, 2013, 1:02:59 PM (7 years ago)

Author:

sacerdot

Message:

Efficiency of the semantics of assembly improved by avoiding the recomputation
of address_of_word_labels maps at every step.

Files:

• extracted/fetch.ml (modified) (1 diff)
• extracted/interpret.ml (modified) (1 diff)
• extracted/interpret2.ml (modified) (2 diffs)
• extracted/interpret2.mli (modified) (1 diff)
• src/ASM/Interpret.ma (modified) (1 diff)
• src/ASM/Interpret2.ma (modified) (2 diffs)

extracted/fetch.ml

@@ -138 +138 @@
     BitVectorTrie.bitVectorTrie) Types.prod **)
 let create_label_cost_map program =
+prerr_endline "CREATE_LABEL_COST_MAP";
   Types.pi1 (create_label_cost_map0 program)
 

extracted/interpret.ml

@@ -4255 +4255 @@
     match instr with
     | ASM.Instruction instr0 ->
-      execute_1_preinstruction ticks cm (fun x y ->
-        Fetch.address_of_word_labels cm.ASM.code x) instr0 s0
+      execute_1_preinstruction ticks cm (fun x y -> addr_of_label x) instr0
+        s0
     | ASM.Comment cmt ->
       Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)

extracted/interpret2.ml

@@ -214 +214 @@
 
 (** val aSM_as_result :
-    ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
-    Types.option **)
-let aSM_as_result prog st =
-  let finaladdr =
-    Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
-  in
+    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
+    Status.pseudoStatus -> Integers.int Types.option **)
+let aSM_as_result prog addr_of_labels st =
+  let finaladdr = addr_of_labels prog.ASM.final_label in
   ASMCosts.as_result_of_finaladdr prog st finaladdr
 
@@ -258 +256 @@
     StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
     StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
-    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
+    StructuredTraces.as_result =
+    (Obj.magic (aSM_as_result prog addr_of_label));
     StructuredTraces.as_call_ident =
     (Obj.magic

extracted/interpret2.mli

@@ -159 +159 @@
 
 val aSM_as_result :
-  ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
-  Types.option
+  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
+  Status.pseudoStatus -> Integers.int Types.option
 
 open AssocList

src/ASM/Interpret.ma

@@ -1198 +1198 @@
   let s ≝
     match instr with
-    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s
+    [ Instruction instr ⇒
+       execute_1_preinstruction ticks …
+        (λx, y. addr_of_label x) instr s
     | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
     | Cost cst ⇒ s

src/ASM/Interpret2.ma

@@ -100 +100 @@
 qed.
 
-definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝
- λprog,st.
-  let finaladdr ≝ address_of_word_labels (code prog) (final_label … prog) in
+definition ASM_as_result: ∀prog. (Identifier → Word) → PseudoStatus prog → option int ≝
+ λprog,addr_of_labels,st.
+  let finaladdr ≝ addr_of_labels (final_label … prog) in
    as_result_of_finaladdr … st finaladdr.
 
@@ -138 +138 @@
       (ASM_as_label_of_pc prog …)
       (ASM_next_instruction_properly_relates_program_counters prog)
-      (ASM_as_result …)
+      (ASM_as_result … addr_of_label)
       (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
       ?.