source: extracted/interpret2.ml @ 2999

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

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File size: 14.9 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 -> StructuredTraces.as_result s);
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 -> StructuredTraces.as_classify s);
161    Measurable.pcs_callee = (fun x st _ ->
162    StructuredTraces.as_call_ident s 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 -> (BitVector.word -> BitVector.word) ->
177    (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
178    Status.pseudoStatus **)
179let execute_1_pseudo_instruction' cm sigma policy status =
180  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
181    Assembly.ticks_of cm sigma policy x) status
182
183(** val classify_pseudo_instruction :
184    ASM.pseudo_instruction -> StructuredTraces.status_class **)
185let classify_pseudo_instruction = function
186| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
187| ASM.Comment x -> StructuredTraces.Cl_other
188| ASM.Cost x -> StructuredTraces.Cl_other
189| ASM.Jmp x -> StructuredTraces.Cl_other
190| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
191| ASM.MovSuccessor (x, x0, x1) -> StructuredTraces.Cl_other
192| ASM.Call x -> StructuredTraces.Cl_call
193| ASM.Mov (x, x0) -> StructuredTraces.Cl_other
194
195(** val aSM_classify :
196    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
197    StructuredTraces.status_class **)
198let aSM_classify cm s =
199  classify_pseudo_instruction
200    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
201
202(** val aSM_as_label_of_pc :
203    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
204    Types.option **)
205let aSM_as_label_of_pc prog pc =
206  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
207  | ASM.Instruction x -> Types.None
208  | ASM.Comment x -> Types.None
209  | ASM.Cost label -> Types.Some label
210  | ASM.Jmp x -> Types.None
211  | ASM.Jnz (x, x0, x1) -> Types.None
212  | ASM.MovSuccessor (x, x0, x1) -> Types.None
213  | ASM.Call x -> Types.None
214  | ASM.Mov (x, x0) -> Types.None
215
216(** val aSM_as_result :
217    ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
218    Types.option **)
219let aSM_as_result prog st =
220  let finaladdr =
221    Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
222  in
223  ASMCosts.as_result_of_finaladdr prog st finaladdr
224
225open AssocList
226
227(** val aSM_as_call_ident :
228    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
229    (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
230    AST.ident **)
231let aSM_as_call_ident prog sigma policy s0 =
232  let st = execute_1_pseudo_instruction' prog sigma policy (Types.pi1 s0) in
233  let { Types.fst = lbl; Types.snd = instr } =
234    Util.nth_safe
235      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
236        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
237        Nat.O)))))))))))))))) st.Status.program_counter) prog.ASM.code
238  in
239  (match lbl with
240   | Types.None -> assert false (* absurd case *)
241   | Types.Some lbl' ->
242     (match AssocList.assoc_list_lookup lbl'
243              (Identifiers.eq_identifier PreIdentifiers.ASMTag)
244              prog.ASM.renamed_symbols with
245      | Types.None -> assert false (* absurd case *)
246      | Types.Some id -> id))
247
248(** val aSM_abstract_status :
249    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
250    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
251let aSM_abstract_status prog sigma policy =
252  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
253    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
254    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
255    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
256    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
257    StructuredTraces.as_call_ident =
258    (Obj.magic (aSM_as_call_ident prog sigma policy));
259    StructuredTraces.as_tailcall_ident = (fun clearme ->
260    let st = clearme in
261    (match (ASM.fetch_pseudo_instruction prog.ASM.code
262             (Obj.magic st).Status.program_counter).Types.fst with
263     | ASM.Instruction clearme0 ->
264       (match clearme0 with
265        | ASM.ADD (x, y) ->
266          (fun _ ->
267            Obj.magic StructuredTraces.status_class_discr
268              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
269        | ASM.ADDC (x, y) ->
270          (fun _ ->
271            Obj.magic StructuredTraces.status_class_discr
272              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
273        | ASM.SUBB (x, y) ->
274          (fun _ ->
275            Obj.magic StructuredTraces.status_class_discr
276              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
277        | ASM.INC x ->
278          (fun _ ->
279            Obj.magic StructuredTraces.status_class_discr
280              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
281        | ASM.DEC x ->
282          (fun _ ->
283            Obj.magic StructuredTraces.status_class_discr
284              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
285        | ASM.MUL (x, y) ->
286          (fun _ ->
287            Obj.magic StructuredTraces.status_class_discr
288              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
289        | ASM.DIV (x, y) ->
290          (fun _ ->
291            Obj.magic StructuredTraces.status_class_discr
292              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
293        | ASM.DA x ->
294          (fun _ ->
295            Obj.magic StructuredTraces.status_class_discr
296              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
297        | ASM.JC x ->
298          (fun _ ->
299            Obj.magic StructuredTraces.status_class_discr
300              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
301        | ASM.JNC x ->
302          (fun _ ->
303            Obj.magic StructuredTraces.status_class_discr
304              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
305        | ASM.JB (x, y) ->
306          (fun _ ->
307            Obj.magic StructuredTraces.status_class_discr
308              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
309        | ASM.JNB (x, y) ->
310          (fun _ ->
311            Obj.magic StructuredTraces.status_class_discr
312              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
313        | ASM.JBC (x, y) ->
314          (fun _ ->
315            Obj.magic StructuredTraces.status_class_discr
316              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
317        | ASM.JZ x ->
318          (fun _ ->
319            Obj.magic StructuredTraces.status_class_discr
320              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
321        | ASM.JNZ x ->
322          (fun _ ->
323            Obj.magic StructuredTraces.status_class_discr
324              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
325        | ASM.CJNE (x, y) ->
326          (fun _ ->
327            Obj.magic StructuredTraces.status_class_discr
328              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
329        | ASM.DJNZ (x, y) ->
330          (fun _ ->
331            Obj.magic StructuredTraces.status_class_discr
332              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
333        | ASM.ANL x ->
334          (fun _ ->
335            Obj.magic StructuredTraces.status_class_discr
336              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
337        | ASM.ORL x ->
338          (fun _ ->
339            Obj.magic StructuredTraces.status_class_discr
340              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
341        | ASM.XRL x ->
342          (fun _ ->
343            Obj.magic StructuredTraces.status_class_discr
344              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
345        | ASM.CLR x ->
346          (fun _ ->
347            Obj.magic StructuredTraces.status_class_discr
348              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
349        | ASM.CPL x ->
350          (fun _ ->
351            Obj.magic StructuredTraces.status_class_discr
352              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
353        | ASM.RL x ->
354          (fun _ ->
355            Obj.magic StructuredTraces.status_class_discr
356              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
357        | ASM.RLC x ->
358          (fun _ ->
359            Obj.magic StructuredTraces.status_class_discr
360              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
361        | ASM.RR x ->
362          (fun _ ->
363            Obj.magic StructuredTraces.status_class_discr
364              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
365        | ASM.RRC x ->
366          (fun _ ->
367            Obj.magic StructuredTraces.status_class_discr
368              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
369        | ASM.SWAP x ->
370          (fun _ ->
371            Obj.magic StructuredTraces.status_class_discr
372              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
373        | ASM.MOV x ->
374          (fun _ ->
375            Obj.magic StructuredTraces.status_class_discr
376              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
377        | ASM.MOVX x ->
378          (fun _ ->
379            Obj.magic StructuredTraces.status_class_discr
380              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
381        | ASM.SETB x ->
382          (fun _ ->
383            Obj.magic StructuredTraces.status_class_discr
384              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
385        | ASM.PUSH x ->
386          (fun _ ->
387            Obj.magic StructuredTraces.status_class_discr
388              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
389        | ASM.POP x ->
390          (fun _ ->
391            Obj.magic StructuredTraces.status_class_discr
392              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
393        | ASM.XCH (x, y) ->
394          (fun _ ->
395            Obj.magic StructuredTraces.status_class_discr
396              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
397        | ASM.XCHD (x, y) ->
398          (fun _ ->
399            Obj.magic StructuredTraces.status_class_discr
400              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
401        | ASM.RET ->
402          (fun _ ->
403            Obj.magic StructuredTraces.status_class_discr
404              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
405        | ASM.RETI ->
406          (fun _ ->
407            Obj.magic StructuredTraces.status_class_discr
408              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
409        | ASM.NOP ->
410          (fun _ ->
411            Obj.magic StructuredTraces.status_class_discr
412              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
413        | ASM.JMP x ->
414          (fun _ ->
415            Obj.magic StructuredTraces.status_class_discr
416              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
417     | ASM.Comment x ->
418       (fun _ ->
419         Obj.magic StructuredTraces.status_class_discr
420           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
421     | ASM.Cost x ->
422       (fun _ ->
423         Obj.magic StructuredTraces.status_class_discr
424           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
425     | ASM.Jmp x ->
426       (fun _ ->
427         Obj.magic StructuredTraces.status_class_discr
428           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
429     | ASM.Jnz (x, y, abs) ->
430       (fun _ ->
431         Obj.magic StructuredTraces.status_class_discr
432           StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
433     | ASM.MovSuccessor (x, y, abs) ->
434       (fun _ ->
435         Obj.magic StructuredTraces.status_class_discr
436           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
437     | ASM.Call x ->
438       (fun _ ->
439         Obj.magic StructuredTraces.status_class_discr
440           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
441     | ASM.Mov (x, y) ->
442       (fun _ ->
443         Obj.magic StructuredTraces.status_class_discr
444           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
445
446(** val aSM_preclassified_system :
447    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
448    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
449let aSM_preclassified_system c sigma policy =
450  mk_preclassified_system_of_abstract_status
451    (aSM_abstract_status c sigma policy) (fun st ->
452    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
453      (execute_1_pseudo_instruction' c sigma policy (Obj.magic st)))
454    (Obj.magic (Status.initialise_status c))
455
Note: See TracBrowser for help on using the repository browser.