source: extracted/aSMCosts.ml @ 2873

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

Extracted again.

File size: 17.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 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 aSM_abstract_status :
118    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
119    BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status **)
120let aSM_abstract_status code_memory cost_labels =
121  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
122    StructuredTraces.as_pc_of =
123    (Obj.magic (Status.program_counter code_memory));
124    StructuredTraces.as_classify =
125    (Obj.magic (AbstractStatus.aSM_classify code_memory));
126    StructuredTraces.as_label_of_pc = (fun pc ->
127    BitVectorTrie.lookup_opt (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
129      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
130    StructuredTraces.as_result = (fun x -> assert false (* absurd case *));
131    StructuredTraces.as_call_ident = (fun x -> assert false
132    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
133    assert false (* absurd case *)) }
134
135(** val trace_any_label_length :
136    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
137    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
138    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
139    Nat.nat **)
140let trace_any_label_length code_memory cost_labels trace_ends_flag start_status final_status the_trace =
141  StructuredTraces.as_trace_any_label_length'
142    (aSM_abstract_status code_memory cost_labels) trace_ends_flag
143    (Obj.magic start_status) (Obj.magic final_status) the_trace
144
145(** val all_program_counter_list :
146    Nat.nat -> BitVector.bitVector List.list **)
147let rec all_program_counter_list = function
148| Nat.O -> List.Nil
149| Nat.S n' ->
150  List.Cons
151    ((Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
152       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
153       Nat.O)))))))))))))))) n'), (all_program_counter_list n'))
154
155(** val compute_paid_trace_any_label :
156    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
157    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
158    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
159    Nat.nat **)
160let rec compute_paid_trace_any_label code_memory cost_labels trace_ends_flag start_status final_status = function
161| StructuredTraces.Tal_base_not_return (the_status, x) ->
162  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
163| StructuredTraces.Tal_base_return (the_status, x) ->
164  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
165| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
166  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
167| StructuredTraces.Tal_base_tailcall
168    (pre_fun_call, start_fun_call, final, x1) ->
169  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
170| StructuredTraces.Tal_step_call
171    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
172     call_trace, final_trace) ->
173  let current_instruction_cost =
174    Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
175  in
176  let final_trace_cost =
177    compute_paid_trace_any_label code_memory cost_labels end_flag
178      (Obj.magic after_fun_call) (Obj.magic final) final_trace
179  in
180  Nat.plus current_instruction_cost final_trace_cost
181| StructuredTraces.Tal_step_default
182    (end_flag, status_pre, status_init, status_end, tail_trace) ->
183  let current_instruction_cost =
184    Interpret.current_instruction_cost code_memory (Obj.magic status_pre)
185  in
186  let tail_trace_cost =
187    compute_paid_trace_any_label code_memory cost_labels end_flag
188      (Obj.magic status_init) (Obj.magic status_end) tail_trace
189  in
190  Nat.plus current_instruction_cost tail_trace_cost
191
192(** val compute_paid_trace_label_label :
193    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
194    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
195    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
196    Nat.nat **)
197let compute_paid_trace_label_label code_memory cost_labels trace_ends_flag start_status final_status = function
198| StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
199  compute_paid_trace_any_label code_memory cost_labels ends_flag
200    (Obj.magic initial) (Obj.magic final) given_trace
201
202(** val block_cost' :
203    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat
204    -> CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool ->
205    Nat.nat Types.sig0 **)
206let rec block_cost' code_memory' program_counter' program_size cost_labels first_time_around =
207  (match program_size with
208   | Nat.O -> (fun _ -> Nat.O)
209   | Nat.S program_size' ->
210     (fun _ ->
211       (let { Types.fst = eta31796; Types.snd = ticks } =
212          Fetch.fetch code_memory' program_counter'
213        in
214       let { Types.fst = instruction; Types.snd = program_counter'' } =
215         eta31796
216       in
217       (fun _ ->
218       let to_continue =
219         match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
220                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
221                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
222                 cost_labels with
223         | Types.None -> Bool.True
224         | Types.Some x -> first_time_around
225       in
226       let x =
227         (match to_continue with
228          | Bool.True ->
229            (fun _ ->
230              Types.pi1
231                ((match instruction with
232                  | ASM.ACALL addr ->
233                    (fun _ ->
234                      Nat.plus ticks
235                        (Types.pi1
236                          (block_cost' code_memory' program_counter''
237                            program_size' cost_labels Bool.False)))
238                  | ASM.LCALL addr ->
239                    (fun _ ->
240                      Nat.plus ticks
241                        (Types.pi1
242                          (block_cost' code_memory' program_counter''
243                            program_size' cost_labels Bool.False)))
244                  | ASM.AJMP addr ->
245                    (fun _ ->
246                      let jump_target =
247                        Interpret.compute_target_of_unconditional_jump
248                          program_counter'' instruction
249                      in
250                      Nat.plus ticks
251                        (Types.pi1
252                          (block_cost' code_memory' jump_target program_size'
253                            cost_labels Bool.False)))
254                  | ASM.LJMP addr ->
255                    (fun _ ->
256                      let jump_target =
257                        Interpret.compute_target_of_unconditional_jump
258                          program_counter'' instruction
259                      in
260                      Nat.plus ticks
261                        (Types.pi1
262                          (block_cost' code_memory' jump_target program_size'
263                            cost_labels Bool.False)))
264                  | ASM.SJMP addr ->
265                    (fun _ ->
266                      let jump_target =
267                        Interpret.compute_target_of_unconditional_jump
268                          program_counter'' instruction
269                      in
270                      Nat.plus ticks
271                        (Types.pi1
272                          (block_cost' code_memory' jump_target program_size'
273                            cost_labels Bool.False)))
274                  | ASM.MOVC (src, trgt) ->
275                    (fun _ ->
276                      Nat.plus ticks
277                        (Types.pi1
278                          (block_cost' code_memory' program_counter''
279                            program_size' cost_labels Bool.False)))
280                  | ASM.RealInstruction real_instruction ->
281                    (fun _ ->
282                      (match real_instruction with
283                       | ASM.ADD (x, x0) ->
284                         (fun _ ->
285                           Nat.plus ticks
286                             (Types.pi1
287                               (block_cost' code_memory' program_counter''
288                                 program_size' cost_labels Bool.False)))
289                       | ASM.ADDC (x, x0) ->
290                         (fun _ ->
291                           Nat.plus ticks
292                             (Types.pi1
293                               (block_cost' code_memory' program_counter''
294                                 program_size' cost_labels Bool.False)))
295                       | ASM.SUBB (x, x0) ->
296                         (fun _ ->
297                           Nat.plus ticks
298                             (Types.pi1
299                               (block_cost' code_memory' program_counter''
300                                 program_size' cost_labels Bool.False)))
301                       | ASM.INC x ->
302                         (fun _ ->
303                           Nat.plus ticks
304                             (Types.pi1
305                               (block_cost' code_memory' program_counter''
306                                 program_size' cost_labels Bool.False)))
307                       | ASM.DEC x ->
308                         (fun _ ->
309                           Nat.plus ticks
310                             (Types.pi1
311                               (block_cost' code_memory' program_counter''
312                                 program_size' cost_labels Bool.False)))
313                       | ASM.MUL (x, x0) ->
314                         (fun _ ->
315                           Nat.plus ticks
316                             (Types.pi1
317                               (block_cost' code_memory' program_counter''
318                                 program_size' cost_labels Bool.False)))
319                       | ASM.DIV (x, x0) ->
320                         (fun _ ->
321                           Nat.plus ticks
322                             (Types.pi1
323                               (block_cost' code_memory' program_counter''
324                                 program_size' cost_labels Bool.False)))
325                       | ASM.DA x ->
326                         (fun _ ->
327                           Nat.plus ticks
328                             (Types.pi1
329                               (block_cost' code_memory' program_counter''
330                                 program_size' cost_labels Bool.False)))
331                       | ASM.JC relative -> (fun _ -> ticks)
332                       | ASM.JNC relative -> (fun _ -> ticks)
333                       | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
334                       | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
335                       | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
336                       | ASM.JZ relative -> (fun _ -> ticks)
337                       | ASM.JNZ relative -> (fun _ -> ticks)
338                       | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
339                       | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
340                       | ASM.ANL x ->
341                         (fun _ ->
342                           Nat.plus ticks
343                             (Types.pi1
344                               (block_cost' code_memory' program_counter''
345                                 program_size' cost_labels Bool.False)))
346                       | ASM.ORL x ->
347                         (fun _ ->
348                           Nat.plus ticks
349                             (Types.pi1
350                               (block_cost' code_memory' program_counter''
351                                 program_size' cost_labels Bool.False)))
352                       | ASM.XRL x ->
353                         (fun _ ->
354                           Nat.plus ticks
355                             (Types.pi1
356                               (block_cost' code_memory' program_counter''
357                                 program_size' cost_labels Bool.False)))
358                       | ASM.CLR x ->
359                         (fun _ ->
360                           Nat.plus ticks
361                             (Types.pi1
362                               (block_cost' code_memory' program_counter''
363                                 program_size' cost_labels Bool.False)))
364                       | ASM.CPL x ->
365                         (fun _ ->
366                           Nat.plus ticks
367                             (Types.pi1
368                               (block_cost' code_memory' program_counter''
369                                 program_size' cost_labels Bool.False)))
370                       | ASM.RL x ->
371                         (fun _ ->
372                           Nat.plus ticks
373                             (Types.pi1
374                               (block_cost' code_memory' program_counter''
375                                 program_size' cost_labels Bool.False)))
376                       | ASM.RLC x ->
377                         (fun _ ->
378                           Nat.plus ticks
379                             (Types.pi1
380                               (block_cost' code_memory' program_counter''
381                                 program_size' cost_labels Bool.False)))
382                       | ASM.RR x ->
383                         (fun _ ->
384                           Nat.plus ticks
385                             (Types.pi1
386                               (block_cost' code_memory' program_counter''
387                                 program_size' cost_labels Bool.False)))
388                       | ASM.RRC x ->
389                         (fun _ ->
390                           Nat.plus ticks
391                             (Types.pi1
392                               (block_cost' code_memory' program_counter''
393                                 program_size' cost_labels Bool.False)))
394                       | ASM.SWAP x ->
395                         (fun _ ->
396                           Nat.plus ticks
397                             (Types.pi1
398                               (block_cost' code_memory' program_counter''
399                                 program_size' cost_labels Bool.False)))
400                       | ASM.MOV x ->
401                         (fun _ ->
402                           Nat.plus ticks
403                             (Types.pi1
404                               (block_cost' code_memory' program_counter''
405                                 program_size' cost_labels Bool.False)))
406                       | ASM.MOVX x ->
407                         (fun _ ->
408                           Nat.plus ticks
409                             (Types.pi1
410                               (block_cost' code_memory' program_counter''
411                                 program_size' cost_labels Bool.False)))
412                       | ASM.SETB x ->
413                         (fun _ ->
414                           Nat.plus ticks
415                             (Types.pi1
416                               (block_cost' code_memory' program_counter''
417                                 program_size' cost_labels Bool.False)))
418                       | ASM.PUSH x ->
419                         (fun _ ->
420                           Nat.plus ticks
421                             (Types.pi1
422                               (block_cost' code_memory' program_counter''
423                                 program_size' cost_labels Bool.False)))
424                       | ASM.POP x ->
425                         (fun _ ->
426                           Nat.plus ticks
427                             (Types.pi1
428                               (block_cost' code_memory' program_counter''
429                                 program_size' cost_labels Bool.False)))
430                       | ASM.XCH (x, x0) ->
431                         (fun _ ->
432                           Nat.plus ticks
433                             (Types.pi1
434                               (block_cost' code_memory' program_counter''
435                                 program_size' cost_labels Bool.False)))
436                       | ASM.XCHD (x, x0) ->
437                         (fun _ ->
438                           Nat.plus ticks
439                             (Types.pi1
440                               (block_cost' code_memory' program_counter''
441                                 program_size' cost_labels Bool.False)))
442                       | ASM.RET -> (fun _ -> ticks)
443                       | ASM.RETI -> (fun _ -> ticks)
444                       | ASM.NOP ->
445                         (fun _ ->
446                           Nat.plus ticks
447                             (Types.pi1
448                               (block_cost' code_memory' program_counter''
449                                 program_size' cost_labels Bool.False)))
450                       | ASM.JMP addr ->
451                         (fun _ ->
452                           Nat.plus ticks
453                             (Types.pi1
454                               (block_cost' code_memory' program_counter''
455                                 program_size' cost_labels Bool.False)))) __))
456                  __))
457          | Bool.False -> (fun _ -> Nat.O)) __
458       in
459       x)) __)) __
460
461(** val block_cost :
462    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
463    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0 **)
464let block_cost code_memory program_counter cost_labels =
465  let cost_of_block =
466    block_cost' code_memory program_counter
467      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
468        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
469        (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
470  in
471  cost_of_block
472
Note: See TracBrowser for help on using the repository browser.