99 open Hints_declaration
117 (** val aSMRegisterRets : ASM.subaddressing_mode List.list **)
118 let aSMRegisterRets =
119 List.Cons ((ASM.DIRECT
120 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
121 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
122 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
123 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
124 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
125 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
126 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
127 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
128 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
129 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
132 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
133 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
134 (Nat.S (Nat.S (Nat.S (Nat.S
135 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
136 (List.Cons ((ASM.DIRECT
137 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
138 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
139 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
140 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
141 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
142 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
143 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
144 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
145 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
146 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
147 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
148 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
149 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
150 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
151 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
152 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
153 (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
154 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
155 (Nat.O, Bool.False, Vector.VEmpty))))))), (List.Cons ((ASM.REGISTER
156 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
157 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
158 Vector.VEmpty))))))), List.Nil)))))))
160 (** val as_result_of_finaladdr :
161 'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int
163 let as_result_of_finaladdr cm st finaladdr =
164 match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
166 Nat.O)))))))))))))))) st.Status.program_counter finaladdr with
170 Status.get_arg_8 cm st Bool.False
171 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
172 Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
173 (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
174 ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
175 (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
176 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
177 (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
178 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
179 ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
180 (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
181 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
182 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
183 ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
184 ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
185 ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
186 (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
187 (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
191 BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
194 let first_byte = fun l ->
196 | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil }
197 | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl }
199 let { Types.fst = b1; Types.snd = tl1 } = first_byte vals in
200 let { Types.fst = b2; Types.snd = tl2 } = first_byte tl1 in
201 let { Types.fst = b3; Types.snd = tl3 } = first_byte tl2 in
202 let { Types.fst = b4; Types.snd = tl4 } = first_byte tl3 in
204 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
206 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
208 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
209 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
210 (Nat.S Nat.O)))))))))) b4
211 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
213 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
214 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
215 (Nat.S Nat.O))))))))) b3
216 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
217 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
218 (Nat.S (Nat.S Nat.O)))))))) b2 b1)))
219 | Bool.False -> Types.None
221 (** val oC_as_call_ident :
222 ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
223 Status.status Types.sig0 -> AST.ident **)
224 let oC_as_call_ident prog cm s0 =
226 (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter
228 (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
229 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
230 (Nat.S Nat.O)))))))))))))))) pc prog.ASM.symboltable with
231 | Types.None -> assert false (* absurd case *)
232 | Types.Some id -> id)
234 (** val oC_abstract_status :
235 ASM.labelled_object_code -> StructuredTraces.abstract_status **)
236 let oC_abstract_status prog =
237 { StructuredTraces.as_pc = AbstractStatus.word_deqset;
238 StructuredTraces.as_pc_of =
239 (Obj.magic (Status.program_counter prog.ASM.cm));
240 StructuredTraces.as_classify =
241 (Obj.magic (AbstractStatus.oC_classify prog.ASM.cm));
242 StructuredTraces.as_label_of_pc = (fun pc ->
243 BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
244 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
245 Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
246 StructuredTraces.as_result = (fun st ->
247 as_result_of_finaladdr prog.ASM.cm (Obj.magic st) prog.ASM.final_pc);
248 StructuredTraces.as_call_ident =
249 (Obj.magic (oC_as_call_ident prog prog.ASM.cm));
250 StructuredTraces.as_tailcall_ident = (fun clearme ->
252 (match AbstractStatus.current_instruction prog.ASM.cm (Obj.magic st) with
255 Obj.magic StructuredTraces.status_class_discr
256 StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
259 Obj.magic StructuredTraces.status_class_discr
260 StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
263 Obj.magic StructuredTraces.status_class_discr
264 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
267 Obj.magic StructuredTraces.status_class_discr
268 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
271 Obj.magic StructuredTraces.status_class_discr
272 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
275 Obj.magic StructuredTraces.status_class_discr
276 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
277 | ASM.RealInstruction clearme0 ->
281 Obj.magic StructuredTraces.status_class_discr
282 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
285 Obj.magic StructuredTraces.status_class_discr
286 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
289 Obj.magic StructuredTraces.status_class_discr
290 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
293 Obj.magic StructuredTraces.status_class_discr
294 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
297 Obj.magic StructuredTraces.status_class_discr
298 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
301 Obj.magic StructuredTraces.status_class_discr
302 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
305 Obj.magic StructuredTraces.status_class_discr
306 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
309 Obj.magic StructuredTraces.status_class_discr
310 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
313 Obj.magic StructuredTraces.status_class_discr
314 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
317 Obj.magic StructuredTraces.status_class_discr
318 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
321 Obj.magic StructuredTraces.status_class_discr
322 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
325 Obj.magic StructuredTraces.status_class_discr
326 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
329 Obj.magic StructuredTraces.status_class_discr
330 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
333 Obj.magic StructuredTraces.status_class_discr
334 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
337 Obj.magic StructuredTraces.status_class_discr
338 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
341 Obj.magic StructuredTraces.status_class_discr
342 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
345 Obj.magic StructuredTraces.status_class_discr
346 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
349 Obj.magic StructuredTraces.status_class_discr
350 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
353 Obj.magic StructuredTraces.status_class_discr
354 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
357 Obj.magic StructuredTraces.status_class_discr
358 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
361 Obj.magic StructuredTraces.status_class_discr
362 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
365 Obj.magic StructuredTraces.status_class_discr
366 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
369 Obj.magic StructuredTraces.status_class_discr
370 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
373 Obj.magic StructuredTraces.status_class_discr
374 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
377 Obj.magic StructuredTraces.status_class_discr
378 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
381 Obj.magic StructuredTraces.status_class_discr
382 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
385 Obj.magic StructuredTraces.status_class_discr
386 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
389 Obj.magic StructuredTraces.status_class_discr
390 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
393 Obj.magic StructuredTraces.status_class_discr
394 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
397 Obj.magic StructuredTraces.status_class_discr
398 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
401 Obj.magic StructuredTraces.status_class_discr
402 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
405 Obj.magic StructuredTraces.status_class_discr
406 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
409 Obj.magic StructuredTraces.status_class_discr
410 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
413 Obj.magic StructuredTraces.status_class_discr
414 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
417 Obj.magic StructuredTraces.status_class_discr
418 StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
421 Obj.magic StructuredTraces.status_class_discr
422 StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
425 Obj.magic StructuredTraces.status_class_discr
426 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
429 Obj.magic StructuredTraces.status_class_discr
430 StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
432 (** val trace_any_label_length :
433 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
434 Status.status -> Status.status -> StructuredTraces.trace_any_label ->
436 let trace_any_label_length prog trace_ends_flag start_status final_status the_trace =
437 StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog)
438 trace_ends_flag (Obj.magic start_status) (Obj.magic final_status)
441 (** val all_program_counter_list :
442 Nat.nat -> BitVector.bitVector List.list **)
443 let rec all_program_counter_list = function
447 ((Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
448 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
449 Nat.O)))))))))))))))) n'), (all_program_counter_list n'))
451 (** val compute_paid_trace_any_label :
452 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
453 Status.status -> Status.status -> StructuredTraces.trace_any_label ->
455 let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function
456 | StructuredTraces.Tal_base_not_return (the_status, x) ->
457 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
458 | StructuredTraces.Tal_base_return (the_status, x) ->
459 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
460 | StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
461 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
462 | StructuredTraces.Tal_base_tailcall
463 (pre_fun_call, start_fun_call, final, x1) ->
464 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
465 | StructuredTraces.Tal_step_call
466 (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
467 call_trace, final_trace) ->
468 let current_instruction_cost =
469 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
471 let final_trace_cost =
472 compute_paid_trace_any_label prog end_flag (Obj.magic after_fun_call)
473 (Obj.magic final) final_trace
475 Nat.plus current_instruction_cost final_trace_cost
476 | StructuredTraces.Tal_step_default
477 (end_flag, status_pre, status_init, status_end, tail_trace) ->
478 let current_instruction_cost =
479 Interpret.current_instruction_cost prog.ASM.cm (Obj.magic status_pre)
481 let tail_trace_cost =
482 compute_paid_trace_any_label prog end_flag (Obj.magic status_init)
483 (Obj.magic status_end) tail_trace
485 Nat.plus current_instruction_cost tail_trace_cost
487 (** val compute_paid_trace_label_label :
488 ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
489 Status.status -> Status.status -> StructuredTraces.trace_label_label ->
491 let compute_paid_trace_label_label prog trace_ends_flag start_status final_status = function
492 | StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
493 compute_paid_trace_any_label prog ends_flag (Obj.magic initial)
494 (Obj.magic final) given_trace
496 (** val block_cost' :
497 ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
498 Nat.nat Types.sig0 **)
499 let rec block_cost' prog program_counter' program_size first_time_around =
500 (match program_size with
501 | Nat.O -> (fun _ -> Nat.O)
502 | Nat.S program_size' ->
504 (let { Types.fst = eta31588; Types.snd = ticks } =
505 Fetch.fetch prog.ASM.cm program_counter'
507 let { Types.fst = instruction; Types.snd = program_counter'' } =
512 match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
513 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
515 prog.ASM.costlabels with
516 | Types.None -> Bool.True
517 | Types.Some x -> first_time_around
520 (match to_continue with
524 ((match instruction with
529 (block_cost' prog program_counter'' program_size'
535 (block_cost' prog program_counter'' program_size'
540 Interpret.compute_target_of_unconditional_jump
541 program_counter'' instruction
545 (block_cost' prog jump_target program_size'
550 Interpret.compute_target_of_unconditional_jump
551 program_counter'' instruction
555 (block_cost' prog jump_target program_size'
560 Interpret.compute_target_of_unconditional_jump
561 program_counter'' instruction
565 (block_cost' prog jump_target program_size'
567 | ASM.MOVC (src, trgt) ->
571 (block_cost' prog program_counter'' program_size'
573 | ASM.RealInstruction real_instruction ->
575 (match real_instruction with
580 (block_cost' prog program_counter''
581 program_size' Bool.False)))
582 | ASM.ADDC (x, x0) ->
586 (block_cost' prog program_counter''
587 program_size' Bool.False)))
588 | ASM.SUBB (x, x0) ->
592 (block_cost' prog program_counter''
593 program_size' Bool.False)))
598 (block_cost' prog program_counter''
599 program_size' Bool.False)))
604 (block_cost' prog program_counter''
605 program_size' Bool.False)))
610 (block_cost' prog program_counter''
611 program_size' Bool.False)))
616 (block_cost' prog program_counter''
617 program_size' Bool.False)))
622 (block_cost' prog program_counter''
623 program_size' Bool.False)))
624 | ASM.JC relative -> (fun _ -> ticks)
625 | ASM.JNC relative -> (fun _ -> ticks)
626 | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
627 | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
628 | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
629 | ASM.JZ relative -> (fun _ -> ticks)
630 | ASM.JNZ relative -> (fun _ -> ticks)
631 | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
632 | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
637 (block_cost' prog program_counter''
638 program_size' Bool.False)))
643 (block_cost' prog program_counter''
644 program_size' Bool.False)))
649 (block_cost' prog program_counter''
650 program_size' Bool.False)))
655 (block_cost' prog program_counter''
656 program_size' Bool.False)))
661 (block_cost' prog program_counter''
662 program_size' Bool.False)))
667 (block_cost' prog program_counter''
668 program_size' Bool.False)))
673 (block_cost' prog program_counter''
674 program_size' Bool.False)))
679 (block_cost' prog program_counter''
680 program_size' Bool.False)))
685 (block_cost' prog program_counter''
686 program_size' Bool.False)))
691 (block_cost' prog program_counter''
692 program_size' Bool.False)))
697 (block_cost' prog program_counter''
698 program_size' Bool.False)))
703 (block_cost' prog program_counter''
704 program_size' Bool.False)))
709 (block_cost' prog program_counter''
710 program_size' Bool.False)))
715 (block_cost' prog program_counter''
716 program_size' Bool.False)))
721 (block_cost' prog program_counter''
722 program_size' Bool.False)))
727 (block_cost' prog program_counter''
728 program_size' Bool.False)))
729 | ASM.XCHD (x, x0) ->
733 (block_cost' prog program_counter''
734 program_size' Bool.False)))
735 | ASM.RET -> (fun _ -> ticks)
736 | ASM.RETI -> (fun _ -> ticks)
741 (block_cost' prog program_counter''
742 program_size' Bool.False)))
747 (block_cost' prog program_counter''
748 program_size' Bool.False)))) __)) __))
749 | Bool.False -> (fun _ -> Nat.O)) __
754 ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
755 let block_cost prog program_counter =
757 block_cost' prog program_counter
758 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
759 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
760 (Nat.S Nat.O))))))))))))))))) Bool.True