source: extracted/interpret2.ml @ 2905

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

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File size: 5.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 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  let cm = Fetch.load_code_memory c.ASM.oc in
166  mk_preclassified_system_of_abstract_status
167    (ASMCosts.oC_abstract_status cm c.ASM.costlabels) (fun st ->
168    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
169      (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
170    (Obj.magic (Status.initialise_status cm))
171
172open Assembly
173
174(** val execute_1_pseudo_instruction' :
175    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
176    (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
177    Status.pseudoStatus **)
178let execute_1_pseudo_instruction' cm sigma policy status =
179  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
180    Assembly.ticks_of cm sigma policy x) status
181
182(** val classify_pseudo_instruction :
183    ASM.pseudo_instruction -> StructuredTraces.status_class **)
184let classify_pseudo_instruction = function
185| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
186| ASM.Comment x -> StructuredTraces.Cl_other
187| ASM.Cost x -> StructuredTraces.Cl_other
188| ASM.Jmp x -> StructuredTraces.Cl_other
189| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
190| ASM.MovSuccessor (x, x0, x1) -> StructuredTraces.Cl_other
191| ASM.Call x -> StructuredTraces.Cl_call
192| ASM.Mov (x, x0) -> StructuredTraces.Cl_other
193
194(** val aSM_classify :
195    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
196    StructuredTraces.status_class **)
197let aSM_classify cm s =
198  classify_pseudo_instruction
199    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
200
201(** val aSM_as_label_of_pc :
202    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
203    Types.option **)
204let aSM_as_label_of_pc prog pc =
205  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
206  | ASM.Instruction x -> Types.None
207  | ASM.Comment x -> Types.None
208  | ASM.Cost label -> Types.Some label
209  | ASM.Jmp x -> Types.None
210  | ASM.Jnz (x, x0, x1) -> Types.None
211  | ASM.MovSuccessor (x, x0, x1) -> Types.None
212  | ASM.Call x -> Types.None
213  | ASM.Mov (x, x0) -> Types.None
214
215(** val aSM_abstract_status :
216    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
217    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
218let aSM_abstract_status prog sigma policy =
219  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
220    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
221    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
222    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
223    StructuredTraces.as_result = (fun x -> Types.None);
224    StructuredTraces.as_call_ident = (fun x -> Positive.One
225    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
226    assert false (* absurd case *)) }
227
228(** val aSM_preclassified_system :
229    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
230    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
231let aSM_preclassified_system c sigma policy =
232  mk_preclassified_system_of_abstract_status
233    (aSM_abstract_status c sigma policy) (fun st ->
234    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
235      (execute_1_pseudo_instruction' c sigma policy (Obj.magic st)))
236    (Obj.magic (Status.initialise_status c))
237
Note: See TracBrowser for help on using the repository browser.