source: driver/extracted/aSMCosts.ml @ 3106

Last change on this file since 3106 was 3106, checked in by sacerdot, 7 years ago

New extraction.
File size: 30.9 KB
Line 
1open Preamble
2
3open Fetch
4
5open Hide
6
7open Division
8
9open Z
10
11open BitVectorZ
12
13open Pointers
14
15open Coqlib
16
17open Values
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Sets
26
27open Listb
28
29open StructuredTraces
30
31open AbstractStatus
32
33open BitVectorTrie
34
35open String
36
37open Exp
38
39open Arithmetic
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
49open Integers
50
51open AST
52
53open LabelledObjects
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Div_and_mod
76
77open Util
78
79open List
80
81open Lists
82
83open Bool
84
85open Relations
86
87open Nat
88
89open Positive
90
91open Identifiers
92
93open CostLabel
94
95open ASM
96
97open Types
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Jmeq
108
109open Russell
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117(** val aSMRegisterRets : ASM.subaddressing_mode List.list **)
118let 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)))))))
159
160(** val as_result_of_finaladdr :
161    'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int
162    Types.option **)
163let 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
167  | Bool.True ->
168    let vals =
169      List.map (fun h ->
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))))))))))))))))))))
188            h)) aSMRegisterRets
189    in
190    let dummy =
191      BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
192        Nat.O))))))))
193    in
194    let first_byte = fun l ->
195      match l with
196      | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil }
197      | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl }
198    in
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
203    Types.Some
204    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
205      Nat.O))))))))
206      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
207        Nat.O))))))))
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
212        Nat.O))))))))
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
220
221(** val oC_as_call_ident :
222    ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
223    Status.status Types.sig0 -> AST.ident **)
224let oC_as_call_ident prog cm s0 =
225  let pc =
226    (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter
227  in
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)
233
234(** val oC_abstract_status :
235    ASM.labelled_object_code -> StructuredTraces.abstract_status **)
236let 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 ->
251    let st = clearme in
252    (match AbstractStatus.current_instruction prog.ASM.cm (Obj.magic st) with
253     | ASM.ACALL x ->
254       (fun _ ->
255         Obj.magic StructuredTraces.status_class_discr
256           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
257     | ASM.LCALL x ->
258       (fun _ ->
259         Obj.magic StructuredTraces.status_class_discr
260           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
261     | ASM.AJMP x ->
262       (fun _ ->
263         Obj.magic StructuredTraces.status_class_discr
264           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
265     | ASM.LJMP x ->
266       (fun _ ->
267         Obj.magic StructuredTraces.status_class_discr
268           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
269     | ASM.SJMP x ->
270       (fun _ ->
271         Obj.magic StructuredTraces.status_class_discr
272           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
273     | ASM.MOVC (x, y) ->
274       (fun _ ->
275         Obj.magic StructuredTraces.status_class_discr
276           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
277     | ASM.RealInstruction clearme0 ->
278       (match clearme0 with
279        | ASM.ADD (x, y) ->
280          (fun _ ->
281            Obj.magic StructuredTraces.status_class_discr
282              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
283        | ASM.ADDC (x, y) ->
284          (fun _ ->
285            Obj.magic StructuredTraces.status_class_discr
286              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
287        | ASM.SUBB (x, y) ->
288          (fun _ ->
289            Obj.magic StructuredTraces.status_class_discr
290              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
291        | ASM.INC x ->
292          (fun _ ->
293            Obj.magic StructuredTraces.status_class_discr
294              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
295        | ASM.DEC x ->
296          (fun _ ->
297            Obj.magic StructuredTraces.status_class_discr
298              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
299        | ASM.MUL (x, y) ->
300          (fun _ ->
301            Obj.magic StructuredTraces.status_class_discr
302              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
303        | ASM.DIV (x, y) ->
304          (fun _ ->
305            Obj.magic StructuredTraces.status_class_discr
306              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
307        | ASM.DA x ->
308          (fun _ ->
309            Obj.magic StructuredTraces.status_class_discr
310              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
311        | ASM.JC x ->
312          (fun _ ->
313            Obj.magic StructuredTraces.status_class_discr
314              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
315        | ASM.JNC x ->
316          (fun _ ->
317            Obj.magic StructuredTraces.status_class_discr
318              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
319        | ASM.JB (x, y) ->
320          (fun _ ->
321            Obj.magic StructuredTraces.status_class_discr
322              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
323        | ASM.JNB (x, y) ->
324          (fun _ ->
325            Obj.magic StructuredTraces.status_class_discr
326              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
327        | ASM.JBC (x, y) ->
328          (fun _ ->
329            Obj.magic StructuredTraces.status_class_discr
330              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
331        | ASM.JZ x ->
332          (fun _ ->
333            Obj.magic StructuredTraces.status_class_discr
334              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
335        | ASM.JNZ x ->
336          (fun _ ->
337            Obj.magic StructuredTraces.status_class_discr
338              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
339        | ASM.CJNE (x, y) ->
340          (fun _ ->
341            Obj.magic StructuredTraces.status_class_discr
342              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
343        | ASM.DJNZ (x, y) ->
344          (fun _ ->
345            Obj.magic StructuredTraces.status_class_discr
346              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
347        | ASM.ANL x ->
348          (fun _ ->
349            Obj.magic StructuredTraces.status_class_discr
350              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
351        | ASM.ORL x ->
352          (fun _ ->
353            Obj.magic StructuredTraces.status_class_discr
354              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
355        | ASM.XRL x ->
356          (fun _ ->
357            Obj.magic StructuredTraces.status_class_discr
358              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
359        | ASM.CLR x ->
360          (fun _ ->
361            Obj.magic StructuredTraces.status_class_discr
362              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
363        | ASM.CPL x ->
364          (fun _ ->
365            Obj.magic StructuredTraces.status_class_discr
366              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
367        | ASM.RL x ->
368          (fun _ ->
369            Obj.magic StructuredTraces.status_class_discr
370              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
371        | ASM.RLC x ->
372          (fun _ ->
373            Obj.magic StructuredTraces.status_class_discr
374              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
375        | ASM.RR x ->
376          (fun _ ->
377            Obj.magic StructuredTraces.status_class_discr
378              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
379        | ASM.RRC x ->
380          (fun _ ->
381            Obj.magic StructuredTraces.status_class_discr
382              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
383        | ASM.SWAP x ->
384          (fun _ ->
385            Obj.magic StructuredTraces.status_class_discr
386              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
387        | ASM.MOV x ->
388          (fun _ ->
389            Obj.magic StructuredTraces.status_class_discr
390              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
391        | ASM.MOVX x ->
392          (fun _ ->
393            Obj.magic StructuredTraces.status_class_discr
394              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
395        | ASM.SETB x ->
396          (fun _ ->
397            Obj.magic StructuredTraces.status_class_discr
398              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
399        | ASM.PUSH x ->
400          (fun _ ->
401            Obj.magic StructuredTraces.status_class_discr
402              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
403        | ASM.POP x ->
404          (fun _ ->
405            Obj.magic StructuredTraces.status_class_discr
406              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
407        | ASM.XCH (x, y) ->
408          (fun _ ->
409            Obj.magic StructuredTraces.status_class_discr
410              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
411        | ASM.XCHD (x, y) ->
412          (fun _ ->
413            Obj.magic StructuredTraces.status_class_discr
414              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
415        | ASM.RET ->
416          (fun _ ->
417            Obj.magic StructuredTraces.status_class_discr
418              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
419        | ASM.RETI ->
420          (fun _ ->
421            Obj.magic StructuredTraces.status_class_discr
422              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
423        | ASM.NOP ->
424          (fun _ ->
425            Obj.magic StructuredTraces.status_class_discr
426              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
427        | ASM.JMP x ->
428          (fun _ ->
429            Obj.magic StructuredTraces.status_class_discr
430              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
431
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 ->
435    Nat.nat **)
436let 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)
439    the_trace
440
441(** val all_program_counter_list :
442    Nat.nat -> BitVector.bitVector List.list **)
443let rec all_program_counter_list = function
444| Nat.O -> List.Nil
445| Nat.S n' ->
446  List.Cons
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'))
450
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 ->
454    Nat.nat **)
455let 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)
470  in
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
474  in
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)
480  in
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
484  in
485  Nat.plus current_instruction_cost tail_trace_cost
486
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 ->
490    Nat.nat **)
491let 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
495
496(** val block_cost' :
497    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
498    Nat.nat Types.sig0 **)
499let 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' ->
503     (fun _ ->
504       (let { Types.fst = eta302; Types.snd = ticks } =
505          Fetch.fetch prog.ASM.cm program_counter'
506        in
507       let { Types.fst = instruction; Types.snd = program_counter'' } =
508         eta302
509       in
510       (fun _ ->
511       let to_continue =
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
518       in
519       let x =
520         (match to_continue with
521          | Bool.True ->
522            (fun _ ->
523              Types.pi1
524                ((match instruction with
525                  | ASM.ACALL addr ->
526                    (fun _ ->
527                      Nat.plus ticks
528                        (Types.pi1
529                          (block_cost' prog program_counter'' program_size'
530                            Bool.False)))
531                  | ASM.LCALL addr ->
532                    (fun _ ->
533                      Nat.plus ticks
534                        (Types.pi1
535                          (block_cost' prog program_counter'' program_size'
536                            Bool.False)))
537                  | ASM.AJMP addr ->
538                    (fun _ ->
539                      let jump_target =
540                        Interpret.compute_target_of_unconditional_jump
541                          program_counter'' instruction
542                      in
543                      Nat.plus ticks
544                        (Types.pi1
545                          (block_cost' prog jump_target program_size'
546                            Bool.False)))
547                  | ASM.LJMP addr ->
548                    (fun _ ->
549                      let jump_target =
550                        Interpret.compute_target_of_unconditional_jump
551                          program_counter'' instruction
552                      in
553                      Nat.plus ticks
554                        (Types.pi1
555                          (block_cost' prog jump_target program_size'
556                            Bool.False)))
557                  | ASM.SJMP addr ->
558                    (fun _ ->
559                      let jump_target =
560                        Interpret.compute_target_of_unconditional_jump
561                          program_counter'' instruction
562                      in
563                      Nat.plus ticks
564                        (Types.pi1
565                          (block_cost' prog jump_target program_size'
566                            Bool.False)))
567                  | ASM.MOVC (src, trgt) ->
568                    (fun _ ->
569                      Nat.plus ticks
570                        (Types.pi1
571                          (block_cost' prog program_counter'' program_size'
572                            Bool.False)))
573                  | ASM.RealInstruction real_instruction ->
574                    (fun _ ->
575                      (match real_instruction with
576                       | ASM.ADD (x, x0) ->
577                         (fun _ ->
578                           Nat.plus ticks
579                             (Types.pi1
580                               (block_cost' prog program_counter''
581                                 program_size' Bool.False)))
582                       | ASM.ADDC (x, x0) ->
583                         (fun _ ->
584                           Nat.plus ticks
585                             (Types.pi1
586                               (block_cost' prog program_counter''
587                                 program_size' Bool.False)))
588                       | ASM.SUBB (x, x0) ->
589                         (fun _ ->
590                           Nat.plus ticks
591                             (Types.pi1
592                               (block_cost' prog program_counter''
593                                 program_size' Bool.False)))
594                       | ASM.INC x ->
595                         (fun _ ->
596                           Nat.plus ticks
597                             (Types.pi1
598                               (block_cost' prog program_counter''
599                                 program_size' Bool.False)))
600                       | ASM.DEC x ->
601                         (fun _ ->
602                           Nat.plus ticks
603                             (Types.pi1
604                               (block_cost' prog program_counter''
605                                 program_size' Bool.False)))
606                       | ASM.MUL (x, x0) ->
607                         (fun _ ->
608                           Nat.plus ticks
609                             (Types.pi1
610                               (block_cost' prog program_counter''
611                                 program_size' Bool.False)))
612                       | ASM.DIV (x, x0) ->
613                         (fun _ ->
614                           Nat.plus ticks
615                             (Types.pi1
616                               (block_cost' prog program_counter''
617                                 program_size' Bool.False)))
618                       | ASM.DA x ->
619                         (fun _ ->
620                           Nat.plus ticks
621                             (Types.pi1
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)
633                       | ASM.ANL x ->
634                         (fun _ ->
635                           Nat.plus ticks
636                             (Types.pi1
637                               (block_cost' prog program_counter''
638                                 program_size' Bool.False)))
639                       | ASM.ORL x ->
640                         (fun _ ->
641                           Nat.plus ticks
642                             (Types.pi1
643                               (block_cost' prog program_counter''
644                                 program_size' Bool.False)))
645                       | ASM.XRL x ->
646                         (fun _ ->
647                           Nat.plus ticks
648                             (Types.pi1
649                               (block_cost' prog program_counter''
650                                 program_size' Bool.False)))
651                       | ASM.CLR x ->
652                         (fun _ ->
653                           Nat.plus ticks
654                             (Types.pi1
655                               (block_cost' prog program_counter''
656                                 program_size' Bool.False)))
657                       | ASM.CPL x ->
658                         (fun _ ->
659                           Nat.plus ticks
660                             (Types.pi1
661                               (block_cost' prog program_counter''
662                                 program_size' Bool.False)))
663                       | ASM.RL x ->
664                         (fun _ ->
665                           Nat.plus ticks
666                             (Types.pi1
667                               (block_cost' prog program_counter''
668                                 program_size' Bool.False)))
669                       | ASM.RLC x ->
670                         (fun _ ->
671                           Nat.plus ticks
672                             (Types.pi1
673                               (block_cost' prog program_counter''
674                                 program_size' Bool.False)))
675                       | ASM.RR x ->
676                         (fun _ ->
677                           Nat.plus ticks
678                             (Types.pi1
679                               (block_cost' prog program_counter''
680                                 program_size' Bool.False)))
681                       | ASM.RRC x ->
682                         (fun _ ->
683                           Nat.plus ticks
684                             (Types.pi1
685                               (block_cost' prog program_counter''
686                                 program_size' Bool.False)))
687                       | ASM.SWAP x ->
688                         (fun _ ->
689                           Nat.plus ticks
690                             (Types.pi1
691                               (block_cost' prog program_counter''
692                                 program_size' Bool.False)))
693                       | ASM.MOV x ->
694                         (fun _ ->
695                           Nat.plus ticks
696                             (Types.pi1
697                               (block_cost' prog program_counter''
698                                 program_size' Bool.False)))
699                       | ASM.MOVX x ->
700                         (fun _ ->
701                           Nat.plus ticks
702                             (Types.pi1
703                               (block_cost' prog program_counter''
704                                 program_size' Bool.False)))
705                       | ASM.SETB x ->
706                         (fun _ ->
707                           Nat.plus ticks
708                             (Types.pi1
709                               (block_cost' prog program_counter''
710                                 program_size' Bool.False)))
711                       | ASM.PUSH x ->
712                         (fun _ ->
713                           Nat.plus ticks
714                             (Types.pi1
715                               (block_cost' prog program_counter''
716                                 program_size' Bool.False)))
717                       | ASM.POP x ->
718                         (fun _ ->
719                           Nat.plus ticks
720                             (Types.pi1
721                               (block_cost' prog program_counter''
722                                 program_size' Bool.False)))
723                       | ASM.XCH (x, x0) ->
724                         (fun _ ->
725                           Nat.plus ticks
726                             (Types.pi1
727                               (block_cost' prog program_counter''
728                                 program_size' Bool.False)))
729                       | ASM.XCHD (x, x0) ->
730                         (fun _ ->
731                           Nat.plus ticks
732                             (Types.pi1
733                               (block_cost' prog program_counter''
734                                 program_size' Bool.False)))
735                       | ASM.RET -> (fun _ -> ticks)
736                       | ASM.RETI -> (fun _ -> ticks)
737                       | ASM.NOP ->
738                         (fun _ ->
739                           Nat.plus ticks
740                             (Types.pi1
741                               (block_cost' prog program_counter''
742                                 program_size' Bool.False)))
743                       | ASM.JMP addr ->
744                         (fun _ ->
745                           Nat.plus ticks
746                             (Types.pi1
747                               (block_cost' prog program_counter''
748                                 program_size' Bool.False)))) __)) __))
749          | Bool.False -> (fun _ -> Nat.O)) __
750       in
751       x)) __)) __
752
753(** val block_cost :
754    ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
755let block_cost prog program_counter =
756  let cost_of_block =
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
761  in
762  cost_of_block
763
Note: See TracBrowser for help on using the repository browser.