source: extracted/aSMCosts.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 17.7 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open Fetch
82
83open StructuredTraces
84
85open AbstractStatus
86
87open Status
88
89open StatusProofs
90
91open Sets
92
93open Listb
94
95open Interpret
96
97(** val aSM_abstract_status :
98    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
99    BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status **)
100let aSM_abstract_status code_memory cost_labels =
101  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
102    StructuredTraces.as_pc_of =
103    (Obj.magic (Status.program_counter code_memory));
104    StructuredTraces.as_classify = (fun s -> Types.Some
105    (AbstractStatus.aSM_classify code_memory (Obj.magic s)));
106    StructuredTraces.as_label_of_pc = (fun pc ->
107    BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
108      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
109      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
110    StructuredTraces.as_call_ident = (assert false (* absurd case *));
111    StructuredTraces.as_tailcall_ident = (assert false (* absurd case *)) }
112
113(** val trace_any_label_length :
114    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
115    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
116    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
117    Nat.nat **)
118let trace_any_label_length code_memory cost_labels trace_ends_flag start_status final_status the_trace =
119  StructuredTraces.as_trace_any_label_length'
120    (aSM_abstract_status code_memory cost_labels) trace_ends_flag
121    (Obj.magic start_status) (Obj.magic final_status) the_trace
122
123(** val all_program_counter_list :
124    Nat.nat -> BitVector.bitVector List.list **)
125let rec all_program_counter_list = function
126| Nat.O -> List.Nil
127| Nat.S n' ->
128  List.Cons
129    ((Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131       Nat.O)))))))))))))))) n'), (all_program_counter_list n'))
132
133(** val compute_paid_trace_any_label :
134    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
135    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
136    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
137    Nat.nat **)
138let rec compute_paid_trace_any_label code_memory cost_labels trace_ends_flag start_status final_status = function
139| StructuredTraces.Tal_base_not_return (the_status, x) ->
140  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
141| StructuredTraces.Tal_base_return (the_status, x) ->
142  Interpret.current_instruction_cost code_memory (Obj.magic the_status)
143| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
144  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
145| StructuredTraces.Tal_base_tailcall
146    (pre_fun_call, start_fun_call, final, x1) ->
147  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
148| StructuredTraces.Tal_step_call
149    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
150     call_trace, final_trace) ->
151  let current_instruction_cost0 =
152    Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
153  in
154  let final_trace_cost =
155    compute_paid_trace_any_label code_memory cost_labels end_flag
156      (Obj.magic after_fun_call) (Obj.magic final) final_trace
157  in
158  Nat.plus current_instruction_cost0 final_trace_cost
159| StructuredTraces.Tal_step_default
160    (end_flag, status_pre, status_init, status_end, tail_trace) ->
161  let current_instruction_cost0 =
162    Interpret.current_instruction_cost code_memory (Obj.magic status_pre)
163  in
164  let tail_trace_cost =
165    compute_paid_trace_any_label code_memory cost_labels end_flag
166      (Obj.magic status_init) (Obj.magic status_end) tail_trace
167  in
168  Nat.plus current_instruction_cost0 tail_trace_cost
169
170(** val compute_paid_trace_label_label :
171    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
172    BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
173    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
174    Nat.nat **)
175let compute_paid_trace_label_label code_memory cost_labels trace_ends_flag start_status final_status = function
176| StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
177  compute_paid_trace_any_label code_memory cost_labels ends_flag
178    (Obj.magic initial) (Obj.magic final) given_trace
179
180(** val block_cost' :
181    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat
182    -> CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool ->
183    Nat.nat Types.sig0 **)
184let rec block_cost' code_memory' program_counter' program_size cost_labels first_time_around =
185  (match program_size with
186   | Nat.O -> (fun _ -> Nat.O)
187   | Nat.S program_size' ->
188     (fun _ ->
189       (let { Types.fst = eta31746; Types.snd = ticks } =
190          Fetch.fetch code_memory' program_counter'
191        in
192       let { Types.fst = instruction0; Types.snd = program_counter'' } =
193         eta31746
194       in
195       (fun _ ->
196       let to_continue =
197         match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
198                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
199                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
200                 cost_labels with
201         | Types.None -> Bool.True
202         | Types.Some x -> first_time_around
203       in
204       let x =
205         (match to_continue with
206          | Bool.True ->
207            (fun _ ->
208              Types.pi1
209                ((match instruction0 with
210                  | ASM.ACALL addr ->
211                    (fun _ ->
212                      Nat.plus ticks
213                        (Types.pi1
214                          (block_cost' code_memory' program_counter''
215                            program_size' cost_labels Bool.False)))
216                  | ASM.LCALL addr ->
217                    (fun _ ->
218                      Nat.plus ticks
219                        (Types.pi1
220                          (block_cost' code_memory' program_counter''
221                            program_size' cost_labels Bool.False)))
222                  | ASM.AJMP addr ->
223                    (fun _ ->
224                      let jump_target =
225                        Interpret.compute_target_of_unconditional_jump
226                          program_counter'' instruction0
227                      in
228                      Nat.plus ticks
229                        (Types.pi1
230                          (block_cost' code_memory' jump_target program_size'
231                            cost_labels Bool.False)))
232                  | ASM.LJMP addr ->
233                    (fun _ ->
234                      let jump_target =
235                        Interpret.compute_target_of_unconditional_jump
236                          program_counter'' instruction0
237                      in
238                      Nat.plus ticks
239                        (Types.pi1
240                          (block_cost' code_memory' jump_target program_size'
241                            cost_labels Bool.False)))
242                  | ASM.SJMP addr ->
243                    (fun _ ->
244                      let jump_target =
245                        Interpret.compute_target_of_unconditional_jump
246                          program_counter'' instruction0
247                      in
248                      Nat.plus ticks
249                        (Types.pi1
250                          (block_cost' code_memory' jump_target program_size'
251                            cost_labels Bool.False)))
252                  | ASM.MOVC (src, trgt) ->
253                    (fun _ ->
254                      Nat.plus ticks
255                        (Types.pi1
256                          (block_cost' code_memory' program_counter''
257                            program_size' cost_labels Bool.False)))
258                  | ASM.RealInstruction real_instruction ->
259                    (fun _ ->
260                      (match real_instruction with
261                       | ASM.ADD (x, x0) ->
262                         (fun _ ->
263                           Nat.plus ticks
264                             (Types.pi1
265                               (block_cost' code_memory' program_counter''
266                                 program_size' cost_labels Bool.False)))
267                       | ASM.ADDC (x, x0) ->
268                         (fun _ ->
269                           Nat.plus ticks
270                             (Types.pi1
271                               (block_cost' code_memory' program_counter''
272                                 program_size' cost_labels Bool.False)))
273                       | ASM.SUBB (x, x0) ->
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.INC x ->
280                         (fun _ ->
281                           Nat.plus ticks
282                             (Types.pi1
283                               (block_cost' code_memory' program_counter''
284                                 program_size' cost_labels Bool.False)))
285                       | ASM.DEC x ->
286                         (fun _ ->
287                           Nat.plus ticks
288                             (Types.pi1
289                               (block_cost' code_memory' program_counter''
290                                 program_size' cost_labels Bool.False)))
291                       | ASM.MUL (x, x0) ->
292                         (fun _ ->
293                           Nat.plus ticks
294                             (Types.pi1
295                               (block_cost' code_memory' program_counter''
296                                 program_size' cost_labels Bool.False)))
297                       | ASM.DIV (x, x0) ->
298                         (fun _ ->
299                           Nat.plus ticks
300                             (Types.pi1
301                               (block_cost' code_memory' program_counter''
302                                 program_size' cost_labels Bool.False)))
303                       | ASM.DA x ->
304                         (fun _ ->
305                           Nat.plus ticks
306                             (Types.pi1
307                               (block_cost' code_memory' program_counter''
308                                 program_size' cost_labels Bool.False)))
309                       | ASM.JC relative -> (fun _ -> ticks)
310                       | ASM.JNC relative -> (fun _ -> ticks)
311                       | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
312                       | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
313                       | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
314                       | ASM.JZ relative -> (fun _ -> ticks)
315                       | ASM.JNZ relative -> (fun _ -> ticks)
316                       | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
317                       | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
318                       | ASM.ANL x ->
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.ORL 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.XRL x ->
331                         (fun _ ->
332                           Nat.plus ticks
333                             (Types.pi1
334                               (block_cost' code_memory' program_counter''
335                                 program_size' cost_labels Bool.False)))
336                       | ASM.CLR x ->
337                         (fun _ ->
338                           Nat.plus ticks
339                             (Types.pi1
340                               (block_cost' code_memory' program_counter''
341                                 program_size' cost_labels Bool.False)))
342                       | ASM.CPL x ->
343                         (fun _ ->
344                           Nat.plus ticks
345                             (Types.pi1
346                               (block_cost' code_memory' program_counter''
347                                 program_size' cost_labels Bool.False)))
348                       | ASM.RL x ->
349                         (fun _ ->
350                           Nat.plus ticks
351                             (Types.pi1
352                               (block_cost' code_memory' program_counter''
353                                 program_size' cost_labels Bool.False)))
354                       | ASM.RLC x ->
355                         (fun _ ->
356                           Nat.plus ticks
357                             (Types.pi1
358                               (block_cost' code_memory' program_counter''
359                                 program_size' cost_labels Bool.False)))
360                       | ASM.RR x ->
361                         (fun _ ->
362                           Nat.plus ticks
363                             (Types.pi1
364                               (block_cost' code_memory' program_counter''
365                                 program_size' cost_labels Bool.False)))
366                       | ASM.RRC x ->
367                         (fun _ ->
368                           Nat.plus ticks
369                             (Types.pi1
370                               (block_cost' code_memory' program_counter''
371                                 program_size' cost_labels Bool.False)))
372                       | ASM.SWAP x ->
373                         (fun _ ->
374                           Nat.plus ticks
375                             (Types.pi1
376                               (block_cost' code_memory' program_counter''
377                                 program_size' cost_labels Bool.False)))
378                       | ASM.MOV x ->
379                         (fun _ ->
380                           Nat.plus ticks
381                             (Types.pi1
382                               (block_cost' code_memory' program_counter''
383                                 program_size' cost_labels Bool.False)))
384                       | ASM.MOVX x ->
385                         (fun _ ->
386                           Nat.plus ticks
387                             (Types.pi1
388                               (block_cost' code_memory' program_counter''
389                                 program_size' cost_labels Bool.False)))
390                       | ASM.SETB x ->
391                         (fun _ ->
392                           Nat.plus ticks
393                             (Types.pi1
394                               (block_cost' code_memory' program_counter''
395                                 program_size' cost_labels Bool.False)))
396                       | ASM.PUSH x ->
397                         (fun _ ->
398                           Nat.plus ticks
399                             (Types.pi1
400                               (block_cost' code_memory' program_counter''
401                                 program_size' cost_labels Bool.False)))
402                       | ASM.POP x ->
403                         (fun _ ->
404                           Nat.plus ticks
405                             (Types.pi1
406                               (block_cost' code_memory' program_counter''
407                                 program_size' cost_labels Bool.False)))
408                       | ASM.XCH (x, x0) ->
409                         (fun _ ->
410                           Nat.plus ticks
411                             (Types.pi1
412                               (block_cost' code_memory' program_counter''
413                                 program_size' cost_labels Bool.False)))
414                       | ASM.XCHD (x, x0) ->
415                         (fun _ ->
416                           Nat.plus ticks
417                             (Types.pi1
418                               (block_cost' code_memory' program_counter''
419                                 program_size' cost_labels Bool.False)))
420                       | ASM.RET -> (fun _ -> ticks)
421                       | ASM.RETI -> (fun _ -> ticks)
422                       | ASM.NOP ->
423                         (fun _ ->
424                           Nat.plus ticks
425                             (Types.pi1
426                               (block_cost' code_memory' program_counter''
427                                 program_size' cost_labels Bool.False)))
428                       | ASM.JMP addr ->
429                         (fun _ ->
430                           Nat.plus ticks
431                             (Types.pi1
432                               (block_cost' code_memory' program_counter''
433                                 program_size' cost_labels Bool.False)))) __))
434                  __))
435          | Bool.False -> (fun _ -> Nat.O)) __
436       in
437       x)) __)) __
438
439(** val block_cost :
440    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
441    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0 **)
442let block_cost code_memory program_counter0 cost_labels =
443  let cost_of_block =
444    block_cost' code_memory program_counter0
445      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
447        (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
448  in
449  cost_of_block
450
Note: See TracBrowser for help on using the repository browser.