source: extracted/aSMCosts.ml @ 2993

Last change on this file since 2993 was 2993, checked in by sacerdot, 7 years ago
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
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 code_memory));
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 code_memory (Obj.magic st) prog.ASM.final_pc);
239  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 = eta16; 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'' } = eta16
512       in
513       (fun _ ->
514       let to_continue =
515         match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
518                 prog.ASM.costlabels with
519         | Types.None -> Bool.True
520         | Types.Some x -> first_time_around
521       in
522       let x =
523         (match to_continue with
524          | Bool.True ->
525            (fun _ ->
526              Types.pi1
527                ((match instruction with
528                  | ASM.ACALL addr ->
529                    (fun _ ->
530                      Nat.plus ticks
531                        (Types.pi1
532                          (block_cost' prog program_counter'' program_size'
533                            Bool.False)))
534                  | ASM.LCALL addr ->
535                    (fun _ ->
536                      Nat.plus ticks
537                        (Types.pi1
538                          (block_cost' prog program_counter'' program_size'
539                            Bool.False)))
540                  | ASM.AJMP addr ->
541                    (fun _ ->
542                      let jump_target =
543                        Interpret.compute_target_of_unconditional_jump
544                          program_counter'' instruction
545                      in
546                      Nat.plus ticks
547                        (Types.pi1
548                          (block_cost' prog jump_target program_size'
549                            Bool.False)))
550                  | ASM.LJMP addr ->
551                    (fun _ ->
552                      let jump_target =
553                        Interpret.compute_target_of_unconditional_jump
554                          program_counter'' instruction
555                      in
556                      Nat.plus ticks
557                        (Types.pi1
558                          (block_cost' prog jump_target program_size'
559                            Bool.False)))
560                  | ASM.SJMP addr ->
561                    (fun _ ->
562                      let jump_target =
563                        Interpret.compute_target_of_unconditional_jump
564                          program_counter'' instruction
565                      in
566                      Nat.plus ticks
567                        (Types.pi1
568                          (block_cost' prog jump_target program_size'
569                            Bool.False)))
570                  | ASM.MOVC (src, trgt) ->
571                    (fun _ ->
572                      Nat.plus ticks
573                        (Types.pi1
574                          (block_cost' prog program_counter'' program_size'
575                            Bool.False)))
576                  | ASM.RealInstruction real_instruction ->
577                    (fun _ ->
578                      (match real_instruction with
579                       | ASM.ADD (x, x0) ->
580                         (fun _ ->
581                           Nat.plus ticks
582                             (Types.pi1
583                               (block_cost' prog program_counter''
584                                 program_size' Bool.False)))
585                       | ASM.ADDC (x, x0) ->
586                         (fun _ ->
587                           Nat.plus ticks
588                             (Types.pi1
589                               (block_cost' prog program_counter''
590                                 program_size' Bool.False)))
591                       | ASM.SUBB (x, x0) ->
592                         (fun _ ->
593                           Nat.plus ticks
594                             (Types.pi1
595                               (block_cost' prog program_counter''
596                                 program_size' Bool.False)))
597                       | ASM.INC x ->
598                         (fun _ ->
599                           Nat.plus ticks
600                             (Types.pi1
601                               (block_cost' prog program_counter''
602                                 program_size' Bool.False)))
603                       | ASM.DEC x ->
604                         (fun _ ->
605                           Nat.plus ticks
606                             (Types.pi1
607                               (block_cost' prog program_counter''
608                                 program_size' Bool.False)))
609                       | ASM.MUL (x, x0) ->
610                         (fun _ ->
611                           Nat.plus ticks
612                             (Types.pi1
613                               (block_cost' prog program_counter''
614                                 program_size' Bool.False)))
615                       | ASM.DIV (x, x0) ->
616                         (fun _ ->
617                           Nat.plus ticks
618                             (Types.pi1
619                               (block_cost' prog program_counter''
620                                 program_size' Bool.False)))
621                       | ASM.DA x ->
622                         (fun _ ->
623                           Nat.plus ticks
624                             (Types.pi1
625                               (block_cost' prog program_counter''
626                                 program_size' Bool.False)))
627                       | ASM.JC relative -> (fun _ -> ticks)
628                       | ASM.JNC relative -> (fun _ -> ticks)
629                       | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
630                       | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
631                       | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
632                       | ASM.JZ relative -> (fun _ -> ticks)
633                       | ASM.JNZ relative -> (fun _ -> ticks)
634                       | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
635                       | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
636                       | ASM.ANL x ->
637                         (fun _ ->
638                           Nat.plus ticks
639                             (Types.pi1
640                               (block_cost' prog program_counter''
641                                 program_size' Bool.False)))
642                       | ASM.ORL x ->
643                         (fun _ ->
644                           Nat.plus ticks
645                             (Types.pi1
646                               (block_cost' prog program_counter''
647                                 program_size' Bool.False)))
648                       | ASM.XRL x ->
649                         (fun _ ->
650                           Nat.plus ticks
651                             (Types.pi1
652                               (block_cost' prog program_counter''
653                                 program_size' Bool.False)))
654                       | ASM.CLR x ->
655                         (fun _ ->
656                           Nat.plus ticks
657                             (Types.pi1
658                               (block_cost' prog program_counter''
659                                 program_size' Bool.False)))
660                       | ASM.CPL x ->
661                         (fun _ ->
662                           Nat.plus ticks
663                             (Types.pi1
664                               (block_cost' prog program_counter''
665                                 program_size' Bool.False)))
666                       | ASM.RL x ->
667                         (fun _ ->
668                           Nat.plus ticks
669                             (Types.pi1
670                               (block_cost' prog program_counter''
671                                 program_size' Bool.False)))
672                       | ASM.RLC x ->
673                         (fun _ ->
674                           Nat.plus ticks
675                             (Types.pi1
676                               (block_cost' prog program_counter''
677                                 program_size' Bool.False)))
678                       | ASM.RR x ->
679                         (fun _ ->
680                           Nat.plus ticks
681                             (Types.pi1
682                               (block_cost' prog program_counter''
683                                 program_size' Bool.False)))
684                       | ASM.RRC x ->
685                         (fun _ ->
686                           Nat.plus ticks
687                             (Types.pi1
688                               (block_cost' prog program_counter''
689                                 program_size' Bool.False)))
690                       | ASM.SWAP x ->
691                         (fun _ ->
692                           Nat.plus ticks
693                             (Types.pi1
694                               (block_cost' prog program_counter''
695                                 program_size' Bool.False)))
696                       | ASM.MOV x ->
697                         (fun _ ->
698                           Nat.plus ticks
699                             (Types.pi1
700                               (block_cost' prog program_counter''
701                                 program_size' Bool.False)))
702                       | ASM.MOVX x ->
703                         (fun _ ->
704                           Nat.plus ticks
705                             (Types.pi1
706                               (block_cost' prog program_counter''
707                                 program_size' Bool.False)))
708                       | ASM.SETB x ->
709                         (fun _ ->
710                           Nat.plus ticks
711                             (Types.pi1
712                               (block_cost' prog program_counter''
713                                 program_size' Bool.False)))
714                       | ASM.PUSH x ->
715                         (fun _ ->
716                           Nat.plus ticks
717                             (Types.pi1
718                               (block_cost' prog program_counter''
719                                 program_size' Bool.False)))
720                       | ASM.POP x ->
721                         (fun _ ->
722                           Nat.plus ticks
723                             (Types.pi1
724                               (block_cost' prog program_counter''
725                                 program_size' Bool.False)))
726                       | ASM.XCH (x, x0) ->
727                         (fun _ ->
728                           Nat.plus ticks
729                             (Types.pi1
730                               (block_cost' prog program_counter''
731                                 program_size' Bool.False)))
732                       | ASM.XCHD (x, x0) ->
733                         (fun _ ->
734                           Nat.plus ticks
735                             (Types.pi1
736                               (block_cost' prog program_counter''
737                                 program_size' Bool.False)))
738                       | ASM.RET -> (fun _ -> ticks)
739                       | ASM.RETI -> (fun _ -> ticks)
740                       | ASM.NOP ->
741                         (fun _ ->
742                           Nat.plus ticks
743                             (Types.pi1
744                               (block_cost' prog program_counter''
745                                 program_size' Bool.False)))
746                       | ASM.JMP addr ->
747                         (fun _ ->
748                           Nat.plus ticks
749                             (Types.pi1
750                               (block_cost' prog program_counter''
751                                 program_size' Bool.False)))) __)) __))
752          | Bool.False -> (fun _ -> Nat.O)) __
753       in
754       x)) __)) __
755
756(** val block_cost :
757    ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
758let block_cost prog program_counter =
759  let cost_of_block =
760    block_cost' prog program_counter
761      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
762        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
763        (Nat.S Nat.O))))))))))))))))) Bool.True
764  in
765  cost_of_block
766
Note: See TracBrowser for help on using the repository browser.