Changeset 3064
- Timestamp:
- Apr 2, 2013, 1:02:59 PM (8 years ago)
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/fetch.ml
r3059 r3064 138 138 BitVectorTrie.bitVectorTrie) Types.prod **) 139 139 let create_label_cost_map program = 140 prerr_endline "CREATE_LABEL_COST_MAP"; 140 141 Types.pi1 (create_label_cost_map0 program) 141 142 -
extracted/interpret.ml
r3062 r3064 4255 4255 match instr with 4256 4256 | ASM.Instruction instr0 -> 4257 execute_1_preinstruction ticks cm (fun x y -> 4258 Fetch.address_of_word_labels cm.ASM.code x) instr0s04257 execute_1_preinstruction ticks cm (fun x y -> addr_of_label x) instr0 4258 s0 4259 4259 | ASM.Comment cmt -> 4260 4260 Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) -
extracted/interpret2.ml
r3043 r3064 214 214 215 215 (** val aSM_as_result : 216 ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int 217 Types.option **) 218 let aSM_as_result prog st = 219 let finaladdr = 220 Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label 221 in 216 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) -> 217 Status.pseudoStatus -> Integers.int Types.option **) 218 let aSM_as_result prog addr_of_labels st = 219 let finaladdr = addr_of_labels prog.ASM.final_label in 222 220 ASMCosts.as_result_of_finaladdr prog st finaladdr 223 221 … … 258 256 StructuredTraces.as_classify = (Obj.magic (aSM_classify prog)); 259 257 StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog)); 260 StructuredTraces.as_result = (Obj.magic (aSM_as_result prog)); 258 StructuredTraces.as_result = 259 (Obj.magic (aSM_as_result prog addr_of_label)); 261 260 StructuredTraces.as_call_ident = 262 261 (Obj.magic -
extracted/interpret2.mli
r3043 r3064 159 159 160 160 val aSM_as_result : 161 ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int162 Types.option161 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) -> 162 Status.pseudoStatus -> Integers.int Types.option 163 163 164 164 open AssocList -
src/ASM/Interpret.ma
r3062 r3064 1198 1198 let s ≝ 1199 1199 match instr with 1200 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s 1200 [ Instruction instr ⇒ 1201 execute_1_preinstruction ticks … 1202 (λx, y. addr_of_label x) instr s 1201 1203 | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s) 1202 1204 | Cost cst ⇒ s -
src/ASM/Interpret2.ma
r3039 r3064 100 100 qed. 101 101 102 definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝103 λprog, st.104 let finaladdr ≝ addr ess_of_word_labels (code prog)(final_label … prog) in102 definition ASM_as_result: ∀prog. (Identifier → Word) → PseudoStatus prog → option int ≝ 103 λprog,addr_of_labels,st. 104 let finaladdr ≝ addr_of_labels (final_label … prog) in 105 105 as_result_of_finaladdr … st finaladdr. 106 106 … … 138 138 (ASM_as_label_of_pc prog …) 139 139 (ASM_next_instruction_properly_relates_program_counters prog) 140 (ASM_as_result … )140 (ASM_as_result … addr_of_label) 141 141 (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …) 142 142 ?.
Note: See TracChangeset
for help on using the changeset viewer.