source: extracted/aSMCosts.ml @ 2967

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 30.2 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 Jmeq
78
79open Russell
80
81open Util
82
83open List
84
85open Lists
86
87open Bool
88
89open Relations
90
91open Nat
92
93open Positive
94
95open Hints_declaration
96
97open Core_notation
98
99open Pts
100
101open Logic
102
103open Types
104
105open Identifiers
106
107open CostLabel
108
109open ASM
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
130      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
131    (List.Cons ((ASM.DIRECT
132    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
133      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
134      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
135      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
136      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
137      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
138      (Nat.S (Nat.S (Nat.S (Nat.S (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
142      Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
143    (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
144    Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
145    (Nat.O, Bool.False, Vector.VEmpty))))))), (List.Cons ((ASM.REGISTER
146    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
147    Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
148    Vector.VEmpty))))))), List.Nil)))))))
149
150(** val as_result_of_finaladdr :
151    'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int
152    Types.option **)
153let as_result_of_finaladdr cm st finaladdr =
154  match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
155          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
156          Nat.O)))))))))))))))) st.Status.program_counter finaladdr with
157  | Bool.True ->
158    let vals =
159      List.map (fun h ->
160        Status.get_arg_8 cm st Bool.False
161          (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
162            Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
163            (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
164            ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
165            (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
166            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
167            (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
168            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
169            ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
170            (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
171            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
172            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
173            ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
174            ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
175            ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
176            (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
177            (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
178            h)) aSMRegisterRets
179    in
180    let dummy =
181      BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
182        Nat.O))))))))
183    in
184    let first_byte = fun l ->
185      match l with
186      | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil }
187      | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl }
188    in
189    let { Types.fst = b1; Types.snd = tl1 } = first_byte vals in
190    let { Types.fst = b2; Types.snd = tl2 } = first_byte tl1 in
191    let { Types.fst = b3; Types.snd = tl3 } = first_byte tl2 in
192    let { Types.fst = b4; Types.snd = tl4 } = first_byte tl3 in
193    Types.Some
194    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
195      Nat.O))))))))
196      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
197        Nat.O))))))))
198        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
199          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
200          (Nat.S Nat.O)))))))))) b4
201      (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
202        Nat.O))))))))
203        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
204          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
205          (Nat.S Nat.O))))))))) b3
206        (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
207          (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
208          (Nat.S (Nat.S Nat.O)))))))) b2 b1)))
209  | Bool.False -> Types.None
210
211(** val oC_as_call_ident :
212    ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
213    Status.status Types.sig0 -> AST.ident **)
214let oC_as_call_ident prog cm s0 =
215  let pc =
216    (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter
217  in
218  (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
219           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
220           (Nat.S Nat.O)))))))))))))))) pc prog.ASM.symboltable with
221   | Types.None -> assert false (* absurd case *)
222   | Types.Some id -> id)
223
224(** val oC_abstract_status :
225    ASM.labelled_object_code -> StructuredTraces.abstract_status **)
226let oC_abstract_status prog =
227  let code_memory = Fetch.load_code_memory prog.ASM.oc in
228  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
229  StructuredTraces.as_pc_of =
230  (Obj.magic (Status.program_counter (Fetch.load_code_memory prog.ASM.oc)));
231  StructuredTraces.as_classify =
232  (Obj.magic (AbstractStatus.oC_classify code_memory));
233  StructuredTraces.as_label_of_pc = (fun pc ->
234  BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
235    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
236    Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
237  StructuredTraces.as_result = (fun st ->
238  as_result_of_finaladdr (Fetch.load_code_memory prog.ASM.oc) (Obj.magic st)
239    prog.ASM.final_pc); StructuredTraces.as_call_ident =
240  (Obj.magic (oC_as_call_ident prog code_memory));
241  StructuredTraces.as_tailcall_ident = (fun clearme ->
242  let st = clearme in
243  (match AbstractStatus.current_instruction code_memory (Obj.magic st) with
244   | ASM.ACALL x ->
245     (fun _ ->
246       Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
247         StructuredTraces.Cl_tailcall __)
248   | ASM.LCALL x ->
249     (fun _ ->
250       Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
251         StructuredTraces.Cl_tailcall __)
252   | ASM.AJMP x ->
253     (fun _ ->
254       Obj.magic StructuredTraces.status_class_discr
255         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
256   | ASM.LJMP x ->
257     (fun _ ->
258       Obj.magic StructuredTraces.status_class_discr
259         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
260   | ASM.SJMP x ->
261     (fun _ ->
262       Obj.magic StructuredTraces.status_class_discr
263         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
264   | ASM.MOVC (x, y) ->
265     (fun _ ->
266       Obj.magic StructuredTraces.status_class_discr
267         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
268   | ASM.RealInstruction clearme0 ->
269     (match clearme0 with
270      | ASM.ADD (x, y) ->
271        (fun _ ->
272          Obj.magic StructuredTraces.status_class_discr
273            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
274      | ASM.ADDC (x, y) ->
275        (fun _ ->
276          Obj.magic StructuredTraces.status_class_discr
277            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
278      | ASM.SUBB (x, y) ->
279        (fun _ ->
280          Obj.magic StructuredTraces.status_class_discr
281            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
282      | ASM.INC x ->
283        (fun _ ->
284          Obj.magic StructuredTraces.status_class_discr
285            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
286      | ASM.DEC x ->
287        (fun _ ->
288          Obj.magic StructuredTraces.status_class_discr
289            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
290      | ASM.MUL (x, y) ->
291        (fun _ ->
292          Obj.magic StructuredTraces.status_class_discr
293            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
294      | ASM.DIV (x, y) ->
295        (fun _ ->
296          Obj.magic StructuredTraces.status_class_discr
297            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
298      | ASM.DA x ->
299        (fun _ ->
300          Obj.magic StructuredTraces.status_class_discr
301            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
302      | ASM.JC x ->
303        (fun _ ->
304          Obj.magic StructuredTraces.status_class_discr
305            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
306      | ASM.JNC x ->
307        (fun _ ->
308          Obj.magic StructuredTraces.status_class_discr
309            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
310      | ASM.JB (x, y) ->
311        (fun _ ->
312          Obj.magic StructuredTraces.status_class_discr
313            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
314      | ASM.JNB (x, y) ->
315        (fun _ ->
316          Obj.magic StructuredTraces.status_class_discr
317            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
318      | ASM.JBC (x, y) ->
319        (fun _ ->
320          Obj.magic StructuredTraces.status_class_discr
321            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
322      | ASM.JZ x ->
323        (fun _ ->
324          Obj.magic StructuredTraces.status_class_discr
325            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
326      | ASM.JNZ x ->
327        (fun _ ->
328          Obj.magic StructuredTraces.status_class_discr
329            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
330      | ASM.CJNE (x, y) ->
331        (fun _ ->
332          Obj.magic StructuredTraces.status_class_discr
333            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
334      | ASM.DJNZ (x, y) ->
335        (fun _ ->
336          Obj.magic StructuredTraces.status_class_discr
337            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
338      | ASM.ANL x ->
339        (fun _ ->
340          Obj.magic StructuredTraces.status_class_discr
341            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
342      | ASM.ORL x ->
343        (fun _ ->
344          Obj.magic StructuredTraces.status_class_discr
345            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
346      | ASM.XRL x ->
347        (fun _ ->
348          Obj.magic StructuredTraces.status_class_discr
349            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
350      | ASM.CLR x ->
351        (fun _ ->
352          Obj.magic StructuredTraces.status_class_discr
353            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
354      | ASM.CPL x ->
355        (fun _ ->
356          Obj.magic StructuredTraces.status_class_discr
357            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
358      | ASM.RL x ->
359        (fun _ ->
360          Obj.magic StructuredTraces.status_class_discr
361            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
362      | ASM.RLC x ->
363        (fun _ ->
364          Obj.magic StructuredTraces.status_class_discr
365            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
366      | ASM.RR x ->
367        (fun _ ->
368          Obj.magic StructuredTraces.status_class_discr
369            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
370      | ASM.RRC x ->
371        (fun _ ->
372          Obj.magic StructuredTraces.status_class_discr
373            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
374      | ASM.SWAP x ->
375        (fun _ ->
376          Obj.magic StructuredTraces.status_class_discr
377            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
378      | ASM.MOV x ->
379        (fun _ ->
380          Obj.magic StructuredTraces.status_class_discr
381            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
382      | ASM.MOVX x ->
383        (fun _ ->
384          Obj.magic StructuredTraces.status_class_discr
385            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
386      | ASM.SETB x ->
387        (fun _ ->
388          Obj.magic StructuredTraces.status_class_discr
389            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
390      | ASM.PUSH x ->
391        (fun _ ->
392          Obj.magic StructuredTraces.status_class_discr
393            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
394      | ASM.POP x ->
395        (fun _ ->
396          Obj.magic StructuredTraces.status_class_discr
397            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
398      | ASM.XCH (x, y) ->
399        (fun _ ->
400          Obj.magic StructuredTraces.status_class_discr
401            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
402      | ASM.XCHD (x, y) ->
403        (fun _ ->
404          Obj.magic StructuredTraces.status_class_discr
405            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
406      | ASM.RET ->
407        (fun _ ->
408          Obj.magic StructuredTraces.status_class_discr
409            StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
410      | ASM.RETI ->
411        (fun _ ->
412          Obj.magic StructuredTraces.status_class_discr
413            StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
414      | ASM.NOP ->
415        (fun _ ->
416          Obj.magic StructuredTraces.status_class_discr
417            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
418      | ASM.JMP x ->
419        (fun _ ->
420          Obj.magic StructuredTraces.status_class_discr
421            StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
422
423(** val trace_any_label_length :
424    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
425    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
426    Nat.nat **)
427let trace_any_label_length prog =
428  let code_memory = Fetch.load_code_memory prog.ASM.oc in
429  (fun trace_ends_flag start_status final_status the_trace ->
430  StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog)
431    trace_ends_flag (Obj.magic start_status) (Obj.magic final_status)
432    the_trace)
433
434(** val all_program_counter_list :
435    Nat.nat -> BitVector.bitVector List.list **)
436let rec all_program_counter_list = function
437| Nat.O -> List.Nil
438| Nat.S n' ->
439  List.Cons
440    ((Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442       Nat.O)))))))))))))))) n'), (all_program_counter_list n'))
443
444(** val compute_paid_trace_any_label :
445    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
446    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
447    Nat.nat **)
448let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function
449| StructuredTraces.Tal_base_not_return (the_status, x) ->
450  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
451    (Obj.magic the_status)
452| StructuredTraces.Tal_base_return (the_status, x) ->
453  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
454    (Obj.magic the_status)
455| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
456  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
457    (Obj.magic pre_fun_call)
458| StructuredTraces.Tal_base_tailcall
459    (pre_fun_call, start_fun_call, final, x1) ->
460  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
461    (Obj.magic pre_fun_call)
462| StructuredTraces.Tal_step_call
463    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
464     call_trace, final_trace) ->
465  let current_instruction_cost =
466    Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
467      (Obj.magic pre_fun_call)
468  in
469  let final_trace_cost =
470    compute_paid_trace_any_label prog end_flag (Obj.magic after_fun_call)
471      (Obj.magic final) final_trace
472  in
473  Nat.plus current_instruction_cost final_trace_cost
474| StructuredTraces.Tal_step_default
475    (end_flag, status_pre, status_init, status_end, tail_trace) ->
476  let current_instruction_cost =
477    Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
478      (Obj.magic status_pre)
479  in
480  let tail_trace_cost =
481    compute_paid_trace_any_label prog end_flag (Obj.magic status_init)
482      (Obj.magic status_end) tail_trace
483  in
484  Nat.plus current_instruction_cost tail_trace_cost
485
486(** val compute_paid_trace_label_label :
487    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
488    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
489    Nat.nat **)
490let compute_paid_trace_label_label prog =
491  let code_memory = Fetch.load_code_memory prog.ASM.oc in
492  (fun trace_ends_flag start_status final_status the_trace ->
493  let StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) =
494    the_trace
495  in
496  compute_paid_trace_any_label prog ends_flag (Obj.magic initial)
497    (Obj.magic final) given_trace)
498
499(** val block_cost' :
500    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
501    Nat.nat Types.sig0 **)
502let rec block_cost' prog program_counter' program_size first_time_around =
503  let code_memory' = Fetch.load_code_memory prog.ASM.oc in
504  (match program_size with
505   | Nat.O -> (fun _ -> Nat.O)
506   | Nat.S program_size' ->
507     (fun _ ->
508       (let { Types.fst = eta27505; Types.snd = ticks } =
509          Fetch.fetch (Fetch.load_code_memory prog.ASM.oc) program_counter'
510        in
511       let { Types.fst = instruction; Types.snd = program_counter'' } =
512         eta27505
513       in
514       (fun _ ->
515       let to_continue =
516         match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
519                 prog.ASM.costlabels with
520         | Types.None -> Bool.True
521         | Types.Some x -> first_time_around
522       in
523       let x =
524         (match to_continue with
525          | Bool.True ->
526            (fun _ ->
527              Types.pi1
528                ((match instruction with
529                  | ASM.ACALL addr ->
530                    (fun _ ->
531                      Nat.plus ticks
532                        (Types.pi1
533                          (block_cost' prog program_counter'' program_size'
534                            Bool.False)))
535                  | ASM.LCALL addr ->
536                    (fun _ ->
537                      Nat.plus ticks
538                        (Types.pi1
539                          (block_cost' prog program_counter'' program_size'
540                            Bool.False)))
541                  | ASM.AJMP addr ->
542                    (fun _ ->
543                      let jump_target =
544                        Interpret.compute_target_of_unconditional_jump
545                          program_counter'' instruction
546                      in
547                      Nat.plus ticks
548                        (Types.pi1
549                          (block_cost' prog jump_target program_size'
550                            Bool.False)))
551                  | ASM.LJMP addr ->
552                    (fun _ ->
553                      let jump_target =
554                        Interpret.compute_target_of_unconditional_jump
555                          program_counter'' instruction
556                      in
557                      Nat.plus ticks
558                        (Types.pi1
559                          (block_cost' prog jump_target program_size'
560                            Bool.False)))
561                  | ASM.SJMP addr ->
562                    (fun _ ->
563                      let jump_target =
564                        Interpret.compute_target_of_unconditional_jump
565                          program_counter'' instruction
566                      in
567                      Nat.plus ticks
568                        (Types.pi1
569                          (block_cost' prog jump_target program_size'
570                            Bool.False)))
571                  | ASM.MOVC (src, trgt) ->
572                    (fun _ ->
573                      Nat.plus ticks
574                        (Types.pi1
575                          (block_cost' prog program_counter'' program_size'
576                            Bool.False)))
577                  | ASM.RealInstruction real_instruction ->
578                    (fun _ ->
579                      (match real_instruction with
580                       | ASM.ADD (x, x0) ->
581                         (fun _ ->
582                           Nat.plus ticks
583                             (Types.pi1
584                               (block_cost' prog program_counter''
585                                 program_size' Bool.False)))
586                       | ASM.ADDC (x, x0) ->
587                         (fun _ ->
588                           Nat.plus ticks
589                             (Types.pi1
590                               (block_cost' prog program_counter''
591                                 program_size' Bool.False)))
592                       | ASM.SUBB (x, x0) ->
593                         (fun _ ->
594                           Nat.plus ticks
595                             (Types.pi1
596                               (block_cost' prog program_counter''
597                                 program_size' Bool.False)))
598                       | ASM.INC x ->
599                         (fun _ ->
600                           Nat.plus ticks
601                             (Types.pi1
602                               (block_cost' prog program_counter''
603                                 program_size' Bool.False)))
604                       | ASM.DEC x ->
605                         (fun _ ->
606                           Nat.plus ticks
607                             (Types.pi1
608                               (block_cost' prog program_counter''
609                                 program_size' Bool.False)))
610                       | ASM.MUL (x, x0) ->
611                         (fun _ ->
612                           Nat.plus ticks
613                             (Types.pi1
614                               (block_cost' prog program_counter''
615                                 program_size' Bool.False)))
616                       | ASM.DIV (x, x0) ->
617                         (fun _ ->
618                           Nat.plus ticks
619                             (Types.pi1
620                               (block_cost' prog program_counter''
621                                 program_size' Bool.False)))
622                       | ASM.DA x ->
623                         (fun _ ->
624                           Nat.plus ticks
625                             (Types.pi1
626                               (block_cost' prog program_counter''
627                                 program_size' Bool.False)))
628                       | ASM.JC relative -> (fun _ -> ticks)
629                       | ASM.JNC relative -> (fun _ -> ticks)
630                       | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
631                       | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
632                       | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
633                       | ASM.JZ relative -> (fun _ -> ticks)
634                       | ASM.JNZ relative -> (fun _ -> ticks)
635                       | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
636                       | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
637                       | ASM.ANL x ->
638                         (fun _ ->
639                           Nat.plus ticks
640                             (Types.pi1
641                               (block_cost' prog program_counter''
642                                 program_size' Bool.False)))
643                       | ASM.ORL x ->
644                         (fun _ ->
645                           Nat.plus ticks
646                             (Types.pi1
647                               (block_cost' prog program_counter''
648                                 program_size' Bool.False)))
649                       | ASM.XRL x ->
650                         (fun _ ->
651                           Nat.plus ticks
652                             (Types.pi1
653                               (block_cost' prog program_counter''
654                                 program_size' Bool.False)))
655                       | ASM.CLR x ->
656                         (fun _ ->
657                           Nat.plus ticks
658                             (Types.pi1
659                               (block_cost' prog program_counter''
660                                 program_size' Bool.False)))
661                       | ASM.CPL x ->
662                         (fun _ ->
663                           Nat.plus ticks
664                             (Types.pi1
665                               (block_cost' prog program_counter''
666                                 program_size' Bool.False)))
667                       | ASM.RL x ->
668                         (fun _ ->
669                           Nat.plus ticks
670                             (Types.pi1
671                               (block_cost' prog program_counter''
672                                 program_size' Bool.False)))
673                       | ASM.RLC x ->
674                         (fun _ ->
675                           Nat.plus ticks
676                             (Types.pi1
677                               (block_cost' prog program_counter''
678                                 program_size' Bool.False)))
679                       | ASM.RR x ->
680                         (fun _ ->
681                           Nat.plus ticks
682                             (Types.pi1
683                               (block_cost' prog program_counter''
684                                 program_size' Bool.False)))
685                       | ASM.RRC x ->
686                         (fun _ ->
687                           Nat.plus ticks
688                             (Types.pi1
689                               (block_cost' prog program_counter''
690                                 program_size' Bool.False)))
691                       | ASM.SWAP x ->
692                         (fun _ ->
693                           Nat.plus ticks
694                             (Types.pi1
695                               (block_cost' prog program_counter''
696                                 program_size' Bool.False)))
697                       | ASM.MOV x ->
698                         (fun _ ->
699                           Nat.plus ticks
700                             (Types.pi1
701                               (block_cost' prog program_counter''
702                                 program_size' Bool.False)))
703                       | ASM.MOVX x ->
704                         (fun _ ->
705                           Nat.plus ticks
706                             (Types.pi1
707                               (block_cost' prog program_counter''
708                                 program_size' Bool.False)))
709                       | ASM.SETB x ->
710                         (fun _ ->
711                           Nat.plus ticks
712                             (Types.pi1
713                               (block_cost' prog program_counter''
714                                 program_size' Bool.False)))
715                       | ASM.PUSH x ->
716                         (fun _ ->
717                           Nat.plus ticks
718                             (Types.pi1
719                               (block_cost' prog program_counter''
720                                 program_size' Bool.False)))
721                       | ASM.POP x ->
722                         (fun _ ->
723                           Nat.plus ticks
724                             (Types.pi1
725                               (block_cost' prog program_counter''
726                                 program_size' Bool.False)))
727                       | ASM.XCH (x, x0) ->
728                         (fun _ ->
729                           Nat.plus ticks
730                             (Types.pi1
731                               (block_cost' prog program_counter''
732                                 program_size' Bool.False)))
733                       | ASM.XCHD (x, x0) ->
734                         (fun _ ->
735                           Nat.plus ticks
736                             (Types.pi1
737                               (block_cost' prog program_counter''
738                                 program_size' Bool.False)))
739                       | ASM.RET -> (fun _ -> ticks)
740                       | ASM.RETI -> (fun _ -> ticks)
741                       | ASM.NOP ->
742                         (fun _ ->
743                           Nat.plus ticks
744                             (Types.pi1
745                               (block_cost' prog program_counter''
746                                 program_size' Bool.False)))
747                       | ASM.JMP addr ->
748                         (fun _ ->
749                           Nat.plus ticks
750                             (Types.pi1
751                               (block_cost' prog program_counter''
752                                 program_size' Bool.False)))) __)) __))
753          | Bool.False -> (fun _ -> Nat.O)) __
754       in
755       x)) __)) __
756
757(** val block_cost :
758    ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
759let block_cost prog program_counter =
760  let cost_of_block =
761    block_cost' prog program_counter
762      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
763        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
764        (Nat.S Nat.O))))))))))))))))) Bool.True
765  in
766  cost_of_block
767
Note: See TracBrowser for help on using the repository browser.