source: extracted/aSMCosts.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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