source: extracted/aSMCosts.ml @ 2833

Last change on this file since 2833 was 2833, checked in by sacerdot, 8 years ago

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