source: extracted/interpret2.ml @ 2910

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

Abstract statuses for ASM and OC completed.
A simple test program can now be run in every pass of the compiler, always
showing the same behaviour (up to initialization).

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