source: extracted/interpret2.ml @ 2993

Last change on this file since 2993 was 2993, checked in by sacerdot, 7 years ago
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
File size: 15.0 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
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  let lcm =(Fetch.load_code_memory c.ASM.oc) in
168  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
169    (fun st ->
170    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
171      (Interpret.execute_1 lcm (Obj.magic st))
172    )
173    (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
174
175open Assembly
176
177(** val execute_1_pseudo_instruction' :
178    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
179    (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
180    Status.pseudoStatus **)
181let execute_1_pseudo_instruction' cm sigma policy status =
182  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
183    Assembly.ticks_of cm sigma policy x) 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.MovSuccessor (x, x0, x1) -> StructuredTraces.Cl_other
194| ASM.Call x -> StructuredTraces.Cl_call
195| ASM.Mov (x, x0) -> StructuredTraces.Cl_other
196
197(** val aSM_classify :
198    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
199    StructuredTraces.status_class **)
200let aSM_classify cm s =
201  classify_pseudo_instruction
202    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
203
204(** val aSM_as_label_of_pc :
205    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
206    Types.option **)
207let aSM_as_label_of_pc prog pc =
208  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
209  | ASM.Instruction x -> Types.None
210  | ASM.Comment x -> Types.None
211  | ASM.Cost label -> Types.Some label
212  | ASM.Jmp x -> Types.None
213  | ASM.Jnz (x, x0, x1) -> Types.None
214  | ASM.MovSuccessor (x, x0, x1) -> Types.None
215  | ASM.Call x -> Types.None
216  | ASM.Mov (x, x0) -> Types.None
217
218(** val aSM_as_result :
219    ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
220    Types.option **)
221let aSM_as_result prog st =
222  let finaladdr =
223    Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
224  in
225  ASMCosts.as_result_of_finaladdr prog st finaladdr
226
227open AssocList
228
229(** val aSM_as_call_ident :
230    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
231    (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
232    AST.ident **)
233let aSM_as_call_ident prog sigma policy s0 =
234  let st = execute_1_pseudo_instruction' prog sigma policy (Types.pi1 s0) 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 -> (BitVector.word -> BitVector.word) ->
252    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
253let aSM_abstract_status prog sigma policy =
254  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
255    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
256    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
257    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
258    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
259    StructuredTraces.as_call_ident =
260    (Obj.magic (aSM_as_call_ident prog sigma policy));
261    StructuredTraces.as_tailcall_ident = (fun clearme ->
262    let st = clearme in
263    (match (ASM.fetch_pseudo_instruction prog.ASM.code
264             (Obj.magic st).Status.program_counter).Types.fst with
265     | ASM.Instruction clearme0 ->
266       (match clearme0 with
267        | ASM.ADD (x, y) ->
268          (fun _ ->
269            Obj.magic StructuredTraces.status_class_discr
270              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
271        | ASM.ADDC (x, y) ->
272          (fun _ ->
273            Obj.magic StructuredTraces.status_class_discr
274              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
275        | ASM.SUBB (x, y) ->
276          (fun _ ->
277            Obj.magic StructuredTraces.status_class_discr
278              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
279        | ASM.INC x ->
280          (fun _ ->
281            Obj.magic StructuredTraces.status_class_discr
282              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
283        | ASM.DEC x ->
284          (fun _ ->
285            Obj.magic StructuredTraces.status_class_discr
286              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
287        | ASM.MUL (x, y) ->
288          (fun _ ->
289            Obj.magic StructuredTraces.status_class_discr
290              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
291        | ASM.DIV (x, y) ->
292          (fun _ ->
293            Obj.magic StructuredTraces.status_class_discr
294              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
295        | ASM.DA x ->
296          (fun _ ->
297            Obj.magic StructuredTraces.status_class_discr
298              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
299        | ASM.JC x ->
300          (fun _ ->
301            Obj.magic StructuredTraces.status_class_discr
302              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
303        | ASM.JNC x ->
304          (fun _ ->
305            Obj.magic StructuredTraces.status_class_discr
306              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
307        | ASM.JB (x, y) ->
308          (fun _ ->
309            Obj.magic StructuredTraces.status_class_discr
310              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
311        | ASM.JNB (x, y) ->
312          (fun _ ->
313            Obj.magic StructuredTraces.status_class_discr
314              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
315        | ASM.JBC (x, y) ->
316          (fun _ ->
317            Obj.magic StructuredTraces.status_class_discr
318              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
319        | ASM.JZ x ->
320          (fun _ ->
321            Obj.magic StructuredTraces.status_class_discr
322              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
323        | ASM.JNZ x ->
324          (fun _ ->
325            Obj.magic StructuredTraces.status_class_discr
326              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
327        | ASM.CJNE (x, y) ->
328          (fun _ ->
329            Obj.magic StructuredTraces.status_class_discr
330              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
331        | ASM.DJNZ (x, y) ->
332          (fun _ ->
333            Obj.magic StructuredTraces.status_class_discr
334              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
335        | ASM.ANL x ->
336          (fun _ ->
337            Obj.magic StructuredTraces.status_class_discr
338              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
339        | ASM.ORL x ->
340          (fun _ ->
341            Obj.magic StructuredTraces.status_class_discr
342              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
343        | ASM.XRL x ->
344          (fun _ ->
345            Obj.magic StructuredTraces.status_class_discr
346              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
347        | ASM.CLR x ->
348          (fun _ ->
349            Obj.magic StructuredTraces.status_class_discr
350              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
351        | ASM.CPL x ->
352          (fun _ ->
353            Obj.magic StructuredTraces.status_class_discr
354              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
355        | ASM.RL x ->
356          (fun _ ->
357            Obj.magic StructuredTraces.status_class_discr
358              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
359        | ASM.RLC x ->
360          (fun _ ->
361            Obj.magic StructuredTraces.status_class_discr
362              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
363        | ASM.RR x ->
364          (fun _ ->
365            Obj.magic StructuredTraces.status_class_discr
366              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
367        | ASM.RRC x ->
368          (fun _ ->
369            Obj.magic StructuredTraces.status_class_discr
370              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
371        | ASM.SWAP x ->
372          (fun _ ->
373            Obj.magic StructuredTraces.status_class_discr
374              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
375        | ASM.MOV x ->
376          (fun _ ->
377            Obj.magic StructuredTraces.status_class_discr
378              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
379        | ASM.MOVX x ->
380          (fun _ ->
381            Obj.magic StructuredTraces.status_class_discr
382              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
383        | ASM.SETB x ->
384          (fun _ ->
385            Obj.magic StructuredTraces.status_class_discr
386              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
387        | ASM.PUSH x ->
388          (fun _ ->
389            Obj.magic StructuredTraces.status_class_discr
390              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
391        | ASM.POP x ->
392          (fun _ ->
393            Obj.magic StructuredTraces.status_class_discr
394              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
395        | ASM.XCH (x, y) ->
396          (fun _ ->
397            Obj.magic StructuredTraces.status_class_discr
398              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
399        | ASM.XCHD (x, y) ->
400          (fun _ ->
401            Obj.magic StructuredTraces.status_class_discr
402              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
403        | ASM.RET ->
404          (fun _ ->
405            Obj.magic StructuredTraces.status_class_discr
406              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
407        | ASM.RETI ->
408          (fun _ ->
409            Obj.magic StructuredTraces.status_class_discr
410              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
411        | ASM.NOP ->
412          (fun _ ->
413            Obj.magic StructuredTraces.status_class_discr
414              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
415        | ASM.JMP x ->
416          (fun _ ->
417            Obj.magic StructuredTraces.status_class_discr
418              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
419     | ASM.Comment x ->
420       (fun _ ->
421         Obj.magic StructuredTraces.status_class_discr
422           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
423     | ASM.Cost x ->
424       (fun _ ->
425         Obj.magic StructuredTraces.status_class_discr
426           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
427     | ASM.Jmp x ->
428       (fun _ ->
429         Obj.magic StructuredTraces.status_class_discr
430           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
431     | ASM.Jnz (x, y, abs) ->
432       (fun _ ->
433         Obj.magic StructuredTraces.status_class_discr
434           StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
435     | ASM.MovSuccessor (x, y, abs) ->
436       (fun _ ->
437         Obj.magic StructuredTraces.status_class_discr
438           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
439     | ASM.Call x ->
440       (fun _ ->
441         Obj.magic StructuredTraces.status_class_discr
442           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
443     | ASM.Mov (x, y) ->
444       (fun _ ->
445         Obj.magic StructuredTraces.status_class_discr
446           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
447
448(** val aSM_preclassified_system :
449    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
450    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
451let aSM_preclassified_system c sigma policy =
452  mk_preclassified_system_of_abstract_status
453    (aSM_abstract_status c sigma policy) (fun st ->
454    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
455      (execute_1_pseudo_instruction' c sigma policy (Obj.magic st)))
456    (Obj.magic (Status.initialise_status c))
457
Note: See TracBrowser for help on using the repository browser.