source: extracted/aSMCosts.ml @ 2649

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

...

File size: 17.6 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open Arithmetic
8
9open Integers
10
11open AST
12
13open CostLabel
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open ErrorMessages
22
23open PreIdentifiers
24
25open Errors
26
27open Extralib
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Lists
36
37open Positive
38
39open Identifiers
40
41open Extranat
42
43open Vector
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Types
52
53open List
54
55open Util
56
57open FoldStuff
58
59open Bool
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Relations
70
71open Nat
72
73open BitVector
74
75open ASM
76
77open BitVectorTrie
78
79open Fetch
80
81open StructuredTraces
82
83open AbstractStatus
84
85open Status
86
87open StatusProofs
88
89open Sets
90
91open Listb
92
93open Interpret
94
95(** val aSM_abstract_status :
96    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
97    BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status **)
98let aSM_abstract_status code_memory cost_labels =
99  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
100    StructuredTraces.as_pc_of =
101    (Obj.magic (Status.program_counter code_memory));
102    StructuredTraces.as_classify = (fun s -> Types.Some
103    (AbstractStatus.aSM_classify code_memory (Obj.magic s)));
104    StructuredTraces.as_label_of_pc = (fun pc ->
105    BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
106      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
107      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
108    StructuredTraces.as_call_ident = (assert false (* absurd case *));
109    StructuredTraces.as_tailcall_ident = (assert false (* absurd case *)) }
110
111(** val trace_any_label_length :
112    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
113    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
114    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
115    Nat.nat **)
116let trace_any_label_length code_memory cost_labels trace_ends_flag start_status final_status the_trace =
117  StructuredTraces.as_trace_any_label_length'
118    (aSM_abstract_status code_memory cost_labels) trace_ends_flag
119    (Obj.magic start_status) (Obj.magic final_status) the_trace
120
121(** val all_program_counter_list :
122    Nat.nat -> BitVector.bitVector List.list **)
123let rec all_program_counter_list = function
124| Nat.O -> List.Nil
125| Nat.S n' ->
126  List.Cons
127    ((Arithmetic.bitvector_of_nat (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.O)))))))))))))))) n'), (all_program_counter_list n'))
130
131(** val compute_paid_trace_any_label :
132    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
133    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
134    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
135    Nat.nat **)
136let rec compute_paid_trace_any_label code_memory cost_labels trace_ends_flag start_status final_status = function
137| StructuredTraces.Tal_base_not_return (the_status, x) ->
138  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
139| StructuredTraces.Tal_base_return (the_status, x) ->
140  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
141| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
142  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
143| StructuredTraces.Tal_base_tailcall (x, x0, x1, x4) ->
144  assert false (* absurd case *)
145| StructuredTraces.Tal_step_call
146    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
147     call_trace, final_trace) ->
148  let current_instruction_cost0 =
149    Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
150  in
151  let final_trace_cost =
152    compute_paid_trace_any_label code_memory cost_labels end_flag
153      (Obj.magic after_fun_call) (Obj.magic final) final_trace
154  in
155  Nat.plus current_instruction_cost0 final_trace_cost
156| StructuredTraces.Tal_step_default
157    (end_flag, status_pre, status_init, status_end, tail_trace) ->
158  let current_instruction_cost0 =
159    Interpret.current_instruction_cost code_memory (Obj.magic status_pre)
160  in
161  let tail_trace_cost =
162    compute_paid_trace_any_label code_memory cost_labels end_flag
163      (Obj.magic status_init) (Obj.magic status_end) tail_trace
164  in
165  Nat.plus current_instruction_cost0 tail_trace_cost
166
167(** val compute_paid_trace_label_label :
168    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
169    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
170    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
171    Nat.nat **)
172let compute_paid_trace_label_label code_memory cost_labels trace_ends_flag start_status final_status = function
173| StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
174  compute_paid_trace_any_label code_memory cost_labels ends_flag
175    (Obj.magic initial) (Obj.magic final) given_trace
176
177(** val block_cost' :
178    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat
179    -> CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool ->
180    Nat.nat Types.sig0 **)
181let rec block_cost' code_memory' program_counter' program_size cost_labels first_time_around =
182  (match program_size with
183   | Nat.O -> (fun _ -> Nat.O)
184   | Nat.S program_size' ->
185     (fun _ ->
186       (let { Types.fst = eta24805; Types.snd = ticks } =
187          Fetch.fetch code_memory' program_counter'
188        in
189       let { Types.fst = instruction0; Types.snd = program_counter'' } =
190         eta24805
191       in
192       (fun _ ->
193       let to_continue =
194         match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
195                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
196                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
197                 cost_labels with
198         | Types.None -> Bool.True
199         | Types.Some x -> first_time_around
200       in
201       let x =
202         (match to_continue with
203          | Bool.True ->
204            (fun _ ->
205              Types.pi1
206                ((match instruction0 with
207                  | ASM.ACALL addr ->
208                    (fun _ ->
209                      Nat.plus ticks
210                        (Types.pi1
211                          (block_cost' code_memory' program_counter''
212                            program_size' cost_labels Bool.False)))
213                  | ASM.LCALL addr ->
214                    (fun _ ->
215                      Nat.plus ticks
216                        (Types.pi1
217                          (block_cost' code_memory' program_counter''
218                            program_size' cost_labels Bool.False)))
219                  | ASM.AJMP addr ->
220                    (fun _ ->
221                      let jump_target =
222                        Interpret.compute_target_of_unconditional_jump
223                          program_counter'' instruction0
224                      in
225                      Nat.plus ticks
226                        (Types.pi1
227                          (block_cost' code_memory' jump_target program_size'
228                            cost_labels Bool.False)))
229                  | ASM.LJMP addr ->
230                    (fun _ ->
231                      let jump_target =
232                        Interpret.compute_target_of_unconditional_jump
233                          program_counter'' instruction0
234                      in
235                      Nat.plus ticks
236                        (Types.pi1
237                          (block_cost' code_memory' jump_target program_size'
238                            cost_labels Bool.False)))
239                  | ASM.SJMP addr ->
240                    (fun _ ->
241                      let jump_target =
242                        Interpret.compute_target_of_unconditional_jump
243                          program_counter'' instruction0
244                      in
245                      Nat.plus ticks
246                        (Types.pi1
247                          (block_cost' code_memory' jump_target program_size'
248                            cost_labels Bool.False)))
249                  | ASM.JMP addr ->
250                    (fun _ ->
251                      Nat.plus ticks
252                        (Types.pi1
253                          (block_cost' code_memory' program_counter''
254                            program_size' cost_labels Bool.False)))
255                  | ASM.MOVC (src, trgt) ->
256                    (fun _ ->
257                      Nat.plus ticks
258                        (Types.pi1
259                          (block_cost' code_memory' program_counter''
260                            program_size' cost_labels Bool.False)))
261                  | ASM.RealInstruction real_instruction ->
262                    (fun _ ->
263                      (match real_instruction with
264                       | ASM.ADD (x, x0) ->
265                         (fun _ ->
266                           Nat.plus ticks
267                             (Types.pi1
268                               (block_cost' code_memory' program_counter''
269                                 program_size' cost_labels Bool.False)))
270                       | ASM.ADDC (x, x0) ->
271                         (fun _ ->
272                           Nat.plus ticks
273                             (Types.pi1
274                               (block_cost' code_memory' program_counter''
275                                 program_size' cost_labels Bool.False)))
276                       | ASM.SUBB (x, x0) ->
277                         (fun _ ->
278                           Nat.plus ticks
279                             (Types.pi1
280                               (block_cost' code_memory' program_counter''
281                                 program_size' cost_labels Bool.False)))
282                       | ASM.INC x ->
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.DEC x ->
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.MUL (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.DIV (x, x0) ->
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.DA 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.JC relative -> (fun _ -> ticks)
313                       | ASM.JNC relative -> (fun _ -> ticks)
314                       | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
315                       | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
316                       | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
317                       | ASM.JZ relative -> (fun _ -> ticks)
318                       | ASM.JNZ relative -> (fun _ -> ticks)
319                       | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
320                       | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
321                       | ASM.ANL x ->
322                         (fun _ ->
323                           Nat.plus ticks
324                             (Types.pi1
325                               (block_cost' code_memory' program_counter''
326                                 program_size' cost_labels Bool.False)))
327                       | ASM.ORL x ->
328                         (fun _ ->
329                           Nat.plus ticks
330                             (Types.pi1
331                               (block_cost' code_memory' program_counter''
332                                 program_size' cost_labels Bool.False)))
333                       | ASM.XRL x ->
334                         (fun _ ->
335                           Nat.plus ticks
336                             (Types.pi1
337                               (block_cost' code_memory' program_counter''
338                                 program_size' cost_labels Bool.False)))
339                       | ASM.CLR 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.CPL 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.RL 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.RLC 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.RR 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.RRC 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.SWAP 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.MOV 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.MOVX 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.SETB 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.PUSH 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.POP 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.XCH (x, x0) ->
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.XCHD (x, x0) ->
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.RET -> (fun _ -> ticks)
424                       | ASM.RETI -> (fun _ -> ticks)
425                       | ASM.NOP ->
426                         (fun _ ->
427                           Nat.plus ticks
428                             (Types.pi1
429                               (block_cost' code_memory' program_counter''
430                                 program_size' cost_labels Bool.False)))) __))
431                  __))
432          | Bool.False -> (fun _ -> Nat.O)) __
433       in
434       x)) __)) __
435
436(** val block_cost :
437    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
438    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0 **)
439let block_cost code_memory program_counter0 cost_labels =
440  let cost_of_block =
441    block_cost' code_memory program_counter0
442      (Util.exponential (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
443        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
444        (Nat.S (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
445  in
446  cost_of_block
447
Note: See TracBrowser for help on using the repository browser.