Changeset 2717 for extracted/aSMCosts.ml
- Timestamp:
- Feb 23, 2013, 1:16:55 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/aSMCosts.ml
r2649 r2717 5 5 open LabelledObjects 6 6 7 open BitVectorTrie 8 9 open Exp 10 7 11 open Arithmetic 8 12 … … 74 78 75 79 open ASM 76 77 open BitVectorTrie78 80 79 81 open Fetch … … 141 143 | StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) -> 142 144 Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call) 143 | StructuredTraces.Tal_base_tailcall (x, x0, x1, x4) -> 144 assert false (* absurd case *) 145 | StructuredTraces.Tal_base_tailcall 146 (pre_fun_call, start_fun_call, final, x1) -> 147 Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call) 145 148 | StructuredTraces.Tal_step_call 146 149 (end_flag, pre_fun_call, start_fun_call, after_fun_call, final, … … 184 187 | Nat.S program_size' -> 185 188 (fun _ -> 186 (let { Types.fst = eta 24805; Types.snd = ticks } =189 (let { Types.fst = eta31521; Types.snd = ticks } = 187 190 Fetch.fetch code_memory' program_counter' 188 191 in 189 192 let { Types.fst = instruction0; Types.snd = program_counter'' } = 190 eta 24805193 eta31521 191 194 in 192 195 (fun _ -> … … 247 250 (block_cost' code_memory' jump_target program_size' 248 251 cost_labels Bool.False))) 249 | ASM.JMP addr ->250 (fun _ ->251 Nat.plus ticks252 (Types.pi1253 (block_cost' code_memory' program_counter''254 program_size' cost_labels Bool.False)))255 252 | ASM.MOVC (src, trgt) -> 256 253 (fun _ -> … … 428 425 (Types.pi1 429 426 (block_cost' code_memory' program_counter'' 427 program_size' cost_labels Bool.False))) 428 | ASM.JMP addr -> 429 (fun _ -> 430 Nat.plus ticks 431 (Types.pi1 432 (block_cost' code_memory' program_counter'' 430 433 program_size' cost_labels Bool.False)))) __)) 431 434 __)) … … 440 443 let cost_of_block = 441 444 block_cost' code_memory program_counter0 442 ( Util.exponential (Nat.S (Nat.S Nat.O))(Nat.S (Nat.S (Nat.S (Nat.S445 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 443 446 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 444 (Nat.S (Nat.SNat.O))))))))))))))))) cost_labels Bool.True447 (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True 445 448 in 446 449 cost_of_block
Note: See TracChangeset
for help on using the changeset viewer.