source: driver/extracted/interpret2.ml @ 3106

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

New extraction.

File size: 16.5 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 Util
78
79open List
80
81open Lists
82
83open Bool
84
85open Relations
86
87open Nat
88
89open Positive
90
91open Identifiers
92
93open CostLabel
94
95open ASM
96
97open Types
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Jmeq
108
109open Russell
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117open ASMCosts
118
119open Stacksize
120
121open SmallstepExec
122
123open Executions
124
125open Measurable
126
127(** val mk_trans_system_of_abstract_status :
128    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
129    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
130let mk_trans_system_of_abstract_status s as_eval =
131  { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
132    SmallstepExec.step = (fun x status ->
133    let tr =
134      match StructuredTraces.as_label s status with
135      | Types.None -> Events.e0
136      | Types.Some cst -> Events.echarge cst
137    in
138    Obj.magic
139      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (as_eval status)
140        (fun status' ->
141        Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = tr;
142          Types.snd = status' }))) }
143
144(** val mk_fullexec_of_abstract_status :
145    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
146    __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
147let mk_fullexec_of_abstract_status s as_eval as_init =
148  { SmallstepExec.es1 = (mk_trans_system_of_abstract_status s as_eval);
149    SmallstepExec.make_global = (fun x -> Obj.magic Types.It);
150    SmallstepExec.make_initial_state = (fun x ->
151    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) as_init)) }
152
153(** val mk_preclassified_system_of_abstract_status :
154    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
155    __ -> Measurable.preclassified_system **)
156let mk_preclassified_system_of_abstract_status s as_eval as_init =
157  { Measurable.pcs_exec = (mk_fullexec_of_abstract_status s as_eval as_init);
158    Measurable.pcs_labelled = (fun x st ->
159    Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
160    Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
161    Measurable.pcs_callee = (fun x st _ ->
162    s.StructuredTraces.as_call_ident st) }
163
164(** val oC_preclassified_system :
165    ASM.labelled_object_code -> Measurable.preclassified_system **)
166let oC_preclassified_system c =
167  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
168    (fun st ->
169    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
170      (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
171    (Obj.magic (Status.initialise_status c.ASM.cm))
172
173open Assembly
174
175(** val execute_1_pseudo_instruction' :
176    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
177    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
178    -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
179    Status.pseudoStatus **)
180let execute_1_pseudo_instruction' cm addr_of_label addr_of_symbol sigma policy status =
181  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
182    Assembly.ticks_of cm addr_of_label sigma policy x) addr_of_label
183    addr_of_symbol status
184
185(** val classify_pseudo_instruction :
186    ASM.pseudo_instruction -> StructuredTraces.status_class **)
187let classify_pseudo_instruction = function
188| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
189| ASM.Comment x -> StructuredTraces.Cl_other
190| ASM.Cost x -> StructuredTraces.Cl_other
191| ASM.Jmp x -> StructuredTraces.Cl_other
192| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
193| ASM.Call x -> StructuredTraces.Cl_call
194| ASM.Mov (x, x0, x1) -> StructuredTraces.Cl_other
195
196(** val aSM_classify :
197    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
198    StructuredTraces.status_class **)
199let aSM_classify cm s =
200  classify_pseudo_instruction
201    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
202
203(** val aSM_as_label_of_pc :
204    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
205    Types.option **)
206let aSM_as_label_of_pc prog pc =
207  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
208  | ASM.Instruction x -> Types.None
209  | ASM.Comment x -> Types.None
210  | ASM.Cost label -> Types.Some label
211  | ASM.Jmp x -> Types.None
212  | ASM.Jnz (x, x0, x1) -> Types.None
213  | ASM.Call x -> Types.None
214  | ASM.Mov (x, x0, x1) -> Types.None
215
216(** val aSM_as_result :
217    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
218    Status.pseudoStatus -> Integers.int Types.option **)
219let aSM_as_result prog addr_of_labels st =
220  let finaladdr = addr_of_labels prog.ASM.final_label in
221  ASMCosts.as_result_of_finaladdr prog st finaladdr
222
223open AssocList
224
225(** val aSM_as_call_ident :
226    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
227    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
228    -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
229    AST.ident **)
230let aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy s0 =
231  let st =
232    execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol sigma
233      policy (Types.pi1 s0)
234  in
235  let { Types.fst = lbl; Types.snd = instr } =
236    Util.nth_safe
237      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
238        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
239        Nat.O)))))))))))))))) st.Status.program_counter) prog.ASM.code
240  in
241  (match lbl with
242   | Types.None -> assert false (* absurd case *)
243   | Types.Some lbl' ->
244     (match AssocList.assoc_list_lookup lbl'
245              (Identifiers.eq_identifier PreIdentifiers.ASMTag)
246              prog.ASM.renamed_symbols with
247      | Types.None -> assert false (* absurd case *)
248      | Types.Some id -> id))
249
250(** val aSM_abstract_status :
251    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
252    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
253    -> (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
254let aSM_abstract_status prog addr_of_label addr_of_symbol sigma policy =
255  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
256    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
257    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
258    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
259    StructuredTraces.as_result =
260    (Obj.magic (aSM_as_result prog addr_of_label));
261    StructuredTraces.as_call_ident =
262    (Obj.magic
263      (aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy));
264    StructuredTraces.as_tailcall_ident = (fun clearme ->
265    let st = clearme in
266    (match (ASM.fetch_pseudo_instruction prog.ASM.code
267             (Obj.magic st).Status.program_counter).Types.fst with
268     | ASM.Instruction clearme0 ->
269       (match clearme0 with
270        | ASM.ADD (x, y) ->
271          (fun _ ->
272            Obj.magic StructuredTraces.status_class_discr
273              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
274        | ASM.ADDC (x, y) ->
275          (fun _ ->
276            Obj.magic StructuredTraces.status_class_discr
277              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
278        | ASM.SUBB (x, y) ->
279          (fun _ ->
280            Obj.magic StructuredTraces.status_class_discr
281              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
282        | ASM.INC x ->
283          (fun _ ->
284            Obj.magic StructuredTraces.status_class_discr
285              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
286        | ASM.DEC x ->
287          (fun _ ->
288            Obj.magic StructuredTraces.status_class_discr
289              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
290        | ASM.MUL (x, y) ->
291          (fun _ ->
292            Obj.magic StructuredTraces.status_class_discr
293              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
294        | ASM.DIV (x, y) ->
295          (fun _ ->
296            Obj.magic StructuredTraces.status_class_discr
297              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
298        | ASM.DA x ->
299          (fun _ ->
300            Obj.magic StructuredTraces.status_class_discr
301              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
302        | ASM.JC x ->
303          (fun _ ->
304            Obj.magic StructuredTraces.status_class_discr
305              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
306        | ASM.JNC x ->
307          (fun _ ->
308            Obj.magic StructuredTraces.status_class_discr
309              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
310        | ASM.JB (x, y) ->
311          (fun _ ->
312            Obj.magic StructuredTraces.status_class_discr
313              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
314        | ASM.JNB (x, y) ->
315          (fun _ ->
316            Obj.magic StructuredTraces.status_class_discr
317              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
318        | ASM.JBC (x, y) ->
319          (fun _ ->
320            Obj.magic StructuredTraces.status_class_discr
321              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
322        | ASM.JZ x ->
323          (fun _ ->
324            Obj.magic StructuredTraces.status_class_discr
325              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
326        | ASM.JNZ x ->
327          (fun _ ->
328            Obj.magic StructuredTraces.status_class_discr
329              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
330        | ASM.CJNE (x, y) ->
331          (fun _ ->
332            Obj.magic StructuredTraces.status_class_discr
333              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
334        | ASM.DJNZ (x, y) ->
335          (fun _ ->
336            Obj.magic StructuredTraces.status_class_discr
337              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
338        | ASM.ANL x ->
339          (fun _ ->
340            Obj.magic StructuredTraces.status_class_discr
341              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
342        | ASM.ORL x ->
343          (fun _ ->
344            Obj.magic StructuredTraces.status_class_discr
345              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
346        | ASM.XRL x ->
347          (fun _ ->
348            Obj.magic StructuredTraces.status_class_discr
349              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
350        | ASM.CLR x ->
351          (fun _ ->
352            Obj.magic StructuredTraces.status_class_discr
353              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
354        | ASM.CPL x ->
355          (fun _ ->
356            Obj.magic StructuredTraces.status_class_discr
357              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
358        | ASM.RL x ->
359          (fun _ ->
360            Obj.magic StructuredTraces.status_class_discr
361              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
362        | ASM.RLC x ->
363          (fun _ ->
364            Obj.magic StructuredTraces.status_class_discr
365              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
366        | ASM.RR x ->
367          (fun _ ->
368            Obj.magic StructuredTraces.status_class_discr
369              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
370        | ASM.RRC x ->
371          (fun _ ->
372            Obj.magic StructuredTraces.status_class_discr
373              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
374        | ASM.SWAP x ->
375          (fun _ ->
376            Obj.magic StructuredTraces.status_class_discr
377              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
378        | ASM.MOV x ->
379          (fun _ ->
380            Obj.magic StructuredTraces.status_class_discr
381              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
382        | ASM.MOVX x ->
383          (fun _ ->
384            Obj.magic StructuredTraces.status_class_discr
385              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
386        | ASM.SETB x ->
387          (fun _ ->
388            Obj.magic StructuredTraces.status_class_discr
389              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
390        | ASM.PUSH x ->
391          (fun _ ->
392            Obj.magic StructuredTraces.status_class_discr
393              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
394        | ASM.POP x ->
395          (fun _ ->
396            Obj.magic StructuredTraces.status_class_discr
397              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
398        | ASM.XCH (x, y) ->
399          (fun _ ->
400            Obj.magic StructuredTraces.status_class_discr
401              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
402        | ASM.XCHD (x, y) ->
403          (fun _ ->
404            Obj.magic StructuredTraces.status_class_discr
405              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
406        | ASM.RET ->
407          (fun _ ->
408            Obj.magic StructuredTraces.status_class_discr
409              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
410        | ASM.RETI ->
411          (fun _ ->
412            Obj.magic StructuredTraces.status_class_discr
413              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
414        | ASM.NOP ->
415          (fun _ ->
416            Obj.magic StructuredTraces.status_class_discr
417              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
418        | ASM.JMP x ->
419          (fun _ ->
420            Obj.magic StructuredTraces.status_class_discr
421              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
422     | ASM.Comment x ->
423       (fun _ ->
424         Obj.magic StructuredTraces.status_class_discr
425           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
426     | ASM.Cost x ->
427       (fun _ ->
428         Obj.magic StructuredTraces.status_class_discr
429           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
430     | ASM.Jmp x ->
431       (fun _ ->
432         Obj.magic StructuredTraces.status_class_discr
433           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
434     | ASM.Jnz (x, y, abs) ->
435       (fun _ ->
436         Obj.magic StructuredTraces.status_class_discr
437           StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
438     | ASM.Call x ->
439       (fun _ ->
440         Obj.magic StructuredTraces.status_class_discr
441           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
442     | ASM.Mov (x, y, abs) ->
443       (fun _ ->
444         Obj.magic StructuredTraces.status_class_discr
445           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
446
447(** val aSM_preclassified_system :
448    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
449    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
450let aSM_preclassified_system c sigma policy =
451  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
452  let symbol_map = Status.construct_datalabels c.ASM.preamble in
453  let addr_of_label = fun x ->
454    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456      Nat.O))))))))))))))))
457      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
458  in
459  let addr_of_symbol = fun x ->
460    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
461      (addr_of_label x)
462  in
463  mk_preclassified_system_of_abstract_status
464    (aSM_abstract_status c addr_of_label addr_of_symbol sigma policy)
465    (fun st ->
466    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
467      (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
468        policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
469
470(** val aSM_status :
471    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
472    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
473let aSM_status c sigma policy =
474  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
475  let symbol_map = Status.construct_datalabels c.ASM.preamble in
476  let addr_of_label = fun x ->
477    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
478      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
479      Nat.O))))))))))))))))
480      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
481  in
482  let addr_of_symbol = fun x ->
483    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
484      (addr_of_label x)
485  in
486  aSM_abstract_status c addr_of_label addr_of_symbol sigma policy
487
Note: See TracBrowser for help on using the repository browser.