source: driver/extracted/rTLabs_abstract.ml @ 3106

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

New extraction

File size: 21.6 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open Graphs
6
7open Order
8
9open Registers
10
11open FrontEndOps
12
13open RTLabs_syntax
14
15open SmallstepExec
16
17open CostLabel
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Extra_bool
26
27open Coqlib
28
29open Values
30
31open FrontEndVal
32
33open Hide
34
35open ByteValues
36
37open Division
38
39open Z
40
41open BitVectorZ
42
43open Pointers
44
45open GenMem
46
47open FrontEndMem
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open Extralib
56
57open Lists
58
59open Identifiers
60
61open Exp
62
63open Arithmetic
64
65open Vector
66
67open Div_and_mod
68
69open Util
70
71open FoldStuff
72
73open BitVector
74
75open Extranat
76
77open Integers
78
79open AST
80
81open Globalenvs
82
83open ErrorMessages
84
85open Option
86
87open Setoids
88
89open Monad
90
91open Jmeq
92
93open Russell
94
95open Positive
96
97open PreIdentifiers
98
99open Errors
100
101open Bool
102
103open Relations
104
105open Nat
106
107open Hints_declaration
108
109open Core_notation
110
111open Pts
112
113open Logic
114
115open Types
116
117open List
118
119open RTLabs_semantics
120
121type rTLabs_state = RTLabs_semantics.state
122
123type rTLabs_genv = RTLabs_semantics.genv
124
125open Sets
126
127open Listb
128
129open StructuredTraces
130
131open CostSpec
132
133open Deqsets_extra
134
135(** val status_class_jmdiscr :
136    StructuredTraces.status_class -> StructuredTraces.status_class -> __ **)
137let status_class_jmdiscr x y =
138  Logic.eq_rect_Type2 x
139    (match x with
140     | StructuredTraces.Cl_return -> Obj.magic (fun _ dH -> dH)
141     | StructuredTraces.Cl_jump -> Obj.magic (fun _ dH -> dH)
142     | StructuredTraces.Cl_call -> Obj.magic (fun _ dH -> dH)
143     | StructuredTraces.Cl_tailcall -> Obj.magic (fun _ dH -> dH)
144     | StructuredTraces.Cl_other -> Obj.magic (fun _ dH -> dH)) y
145
146type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
147                          ras_fn_stack : Pointers.block List.list }
148
149(** val rTLabs_ext_state_rect_Type4 :
150    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
151    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
152let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_24320 =
153  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24320 in
154  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
155
156(** val rTLabs_ext_state_rect_Type5 :
157    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
158    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
159let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_24322 =
160  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24322 in
161  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
162
163(** val rTLabs_ext_state_rect_Type3 :
164    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
165    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
166let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_24324 =
167  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24324 in
168  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
169
170(** val rTLabs_ext_state_rect_Type2 :
171    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
172    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
173let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_24326 =
174  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24326 in
175  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
176
177(** val rTLabs_ext_state_rect_Type1 :
178    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
179    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
180let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_24328 =
181  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24328 in
182  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
183
184(** val rTLabs_ext_state_rect_Type0 :
185    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
186    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
187let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_24330 =
188  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24330 in
189  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
190
191(** val ras_state :
192    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state **)
193let rec ras_state ge xxx =
194  xxx.ras_state
195
196(** val ras_fn_stack :
197    RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list **)
198let rec ras_fn_stack ge xxx =
199  xxx.ras_fn_stack
200
201(** val rTLabs_ext_state_inv_rect_Type4 :
202    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
203    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
204let rTLabs_ext_state_inv_rect_Type4 x1 hterm h1 =
205  let hcut = rTLabs_ext_state_rect_Type4 x1 h1 hterm in hcut __
206
207(** val rTLabs_ext_state_inv_rect_Type3 :
208    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
209    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
210let rTLabs_ext_state_inv_rect_Type3 x1 hterm h1 =
211  let hcut = rTLabs_ext_state_rect_Type3 x1 h1 hterm in hcut __
212
213(** val rTLabs_ext_state_inv_rect_Type2 :
214    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
215    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
216let rTLabs_ext_state_inv_rect_Type2 x1 hterm h1 =
217  let hcut = rTLabs_ext_state_rect_Type2 x1 h1 hterm in hcut __
218
219(** val rTLabs_ext_state_inv_rect_Type1 :
220    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
221    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
222let rTLabs_ext_state_inv_rect_Type1 x1 hterm h1 =
223  let hcut = rTLabs_ext_state_rect_Type1 x1 h1 hterm in hcut __
224
225(** val rTLabs_ext_state_inv_rect_Type0 :
226    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
227    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
228let rTLabs_ext_state_inv_rect_Type0 x1 hterm h1 =
229  let hcut = rTLabs_ext_state_rect_Type0 x1 h1 hterm in hcut __
230
231(** val rTLabs_ext_state_discr :
232    RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
233let rTLabs_ext_state_discr a1 x y =
234  Logic.eq_rect_Type2 x
235    (let { ras_state = a0; ras_fn_stack = a10 } = x in
236    Obj.magic (fun _ dH -> dH __ __ __)) y
237
238(** val rTLabs_ext_state_jmdiscr :
239    RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
240let rTLabs_ext_state_jmdiscr a1 x y =
241  Logic.eq_rect_Type2 x
242    (let { ras_state = a0; ras_fn_stack = a10 } = x in
243    Obj.magic (fun _ dH -> dH __ __ __)) y
244
245(** val dpi1__o__Ras_state__o__inject :
246    RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
247    RTLabs_semantics.state Types.sig0 **)
248let dpi1__o__Ras_state__o__inject x1 x3 =
249  x3.Types.dpi1.ras_state
250
251(** val eject__o__Ras_state__o__inject :
252    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
253    RTLabs_semantics.state Types.sig0 **)
254let eject__o__Ras_state__o__inject x1 x3 =
255  (Types.pi1 x3).ras_state
256
257(** val ras_state__o__inject :
258    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
259    Types.sig0 **)
260let ras_state__o__inject x1 x2 =
261  x2.ras_state
262
263(** val dpi1__o__Ras_state :
264    RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
265    RTLabs_semantics.state **)
266let dpi1__o__Ras_state x0 x2 =
267  x2.Types.dpi1.ras_state
268
269(** val eject__o__Ras_state :
270    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
271    RTLabs_semantics.state **)
272let eject__o__Ras_state x0 x2 =
273  (Types.pi1 x2).ras_state
274
275(** val next_state :
276    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
277    Events.trace -> rTLabs_ext_state **)
278let next_state ge s s' t =
279  { ras_state = s'; ras_fn_stack =
280    ((match s' with
281      | RTLabs_semantics.State (x, x0, x1) -> (fun _ -> s.ras_fn_stack)
282      | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
283        (fun _ -> List.Cons
284          ((Types.pi1
285             (RTLabs_semantics.func_block_of_exec ge s.ras_state t x x0 x1 x2
286               x3 x4)), s.ras_fn_stack))
287      | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
288        (fun _ -> List.tail s.ras_fn_stack)
289      | RTLabs_semantics.Finalstate x -> (fun _ -> List.Nil)) __) }
290
291(** val rTLabs_classify :
292    RTLabs_semantics.state -> StructuredTraces.status_class **)
293let rTLabs_classify = function
294| RTLabs_semantics.State (f, x, x0) ->
295  (match RTLabs_semantics.next_instruction f with
296   | RTLabs_syntax.St_skip x1 -> StructuredTraces.Cl_other
297   | RTLabs_syntax.St_cost (x1, x2) -> StructuredTraces.Cl_other
298   | RTLabs_syntax.St_const (x1, x2, x3, x4) -> StructuredTraces.Cl_other
299   | RTLabs_syntax.St_op1 (x1, x2, x3, x4, x5, x6) ->
300     StructuredTraces.Cl_other
301   | RTLabs_syntax.St_op2 (x1, x2, x3, x4, x5, x6, x7, x8) ->
302     StructuredTraces.Cl_other
303   | RTLabs_syntax.St_load (x1, x2, x3, x4) -> StructuredTraces.Cl_other
304   | RTLabs_syntax.St_store (x1, x2, x3, x4) -> StructuredTraces.Cl_other
305   | RTLabs_syntax.St_call_id (x1, x2, x3, x4) -> StructuredTraces.Cl_other
306   | RTLabs_syntax.St_call_ptr (x1, x2, x3, x4) -> StructuredTraces.Cl_other
307   | RTLabs_syntax.St_cond (x1, x2, x3) -> StructuredTraces.Cl_jump
308   | RTLabs_syntax.St_return -> StructuredTraces.Cl_other)
309| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
310  StructuredTraces.Cl_call
311| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> StructuredTraces.Cl_return
312| RTLabs_semantics.Finalstate x -> StructuredTraces.Cl_other
313
314(** val rTLabs_cost : RTLabs_semantics.state -> Bool.bool **)
315let rTLabs_cost = function
316| RTLabs_semantics.State (f, fs, m) ->
317  CostSpec.is_cost_label (RTLabs_semantics.next_instruction f)
318| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Bool.False
319| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Bool.False
320| RTLabs_semantics.Finalstate x -> Bool.False
321
322(** val rTLabs_cost_label :
323    RTLabs_semantics.state -> CostLabel.costlabel Types.option **)
324let rTLabs_cost_label = function
325| RTLabs_semantics.State (f, fs, m) ->
326  CostSpec.cost_label_of (RTLabs_semantics.next_instruction f)
327| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Types.None
328| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
329| RTLabs_semantics.Finalstate x -> Types.None
330
331type rTLabs_pc =
332| Rapc_state of Pointers.block * Graphs.label
333| Rapc_call of Graphs.label Types.option * Pointers.block
334| Rapc_ret of Pointers.block Types.option
335| Rapc_fin
336
337(** val rTLabs_pc_rect_Type4 :
338    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
339    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
340    rTLabs_pc -> 'a1 **)
341let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
342| Rapc_state (x_24356, x_24355) -> h_rapc_state x_24356 x_24355
343| Rapc_call (x_24358, x_24357) -> h_rapc_call x_24358 x_24357
344| Rapc_ret x_24359 -> h_rapc_ret x_24359
345| Rapc_fin -> h_rapc_fin
346
347(** val rTLabs_pc_rect_Type5 :
348    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
349    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
350    rTLabs_pc -> 'a1 **)
351let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
352| Rapc_state (x_24366, x_24365) -> h_rapc_state x_24366 x_24365
353| Rapc_call (x_24368, x_24367) -> h_rapc_call x_24368 x_24367
354| Rapc_ret x_24369 -> h_rapc_ret x_24369
355| Rapc_fin -> h_rapc_fin
356
357(** val rTLabs_pc_rect_Type3 :
358    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
359    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
360    rTLabs_pc -> 'a1 **)
361let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
362| Rapc_state (x_24376, x_24375) -> h_rapc_state x_24376 x_24375
363| Rapc_call (x_24378, x_24377) -> h_rapc_call x_24378 x_24377
364| Rapc_ret x_24379 -> h_rapc_ret x_24379
365| Rapc_fin -> h_rapc_fin
366
367(** val rTLabs_pc_rect_Type2 :
368    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
369    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
370    rTLabs_pc -> 'a1 **)
371let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
372| Rapc_state (x_24386, x_24385) -> h_rapc_state x_24386 x_24385
373| Rapc_call (x_24388, x_24387) -> h_rapc_call x_24388 x_24387
374| Rapc_ret x_24389 -> h_rapc_ret x_24389
375| Rapc_fin -> h_rapc_fin
376
377(** val rTLabs_pc_rect_Type1 :
378    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
379    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
380    rTLabs_pc -> 'a1 **)
381let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
382| Rapc_state (x_24396, x_24395) -> h_rapc_state x_24396 x_24395
383| Rapc_call (x_24398, x_24397) -> h_rapc_call x_24398 x_24397
384| Rapc_ret x_24399 -> h_rapc_ret x_24399
385| Rapc_fin -> h_rapc_fin
386
387(** val rTLabs_pc_rect_Type0 :
388    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
389    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
390    rTLabs_pc -> 'a1 **)
391let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
392| Rapc_state (x_24406, x_24405) -> h_rapc_state x_24406 x_24405
393| Rapc_call (x_24408, x_24407) -> h_rapc_call x_24408 x_24407
394| Rapc_ret x_24409 -> h_rapc_ret x_24409
395| Rapc_fin -> h_rapc_fin
396
397(** val rTLabs_pc_inv_rect_Type4 :
398    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
399    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
400    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
401let rTLabs_pc_inv_rect_Type4 hterm h1 h2 h3 h4 =
402  let hcut = rTLabs_pc_rect_Type4 h1 h2 h3 h4 hterm in hcut __
403
404(** val rTLabs_pc_inv_rect_Type3 :
405    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
406    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
407    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
408let rTLabs_pc_inv_rect_Type3 hterm h1 h2 h3 h4 =
409  let hcut = rTLabs_pc_rect_Type3 h1 h2 h3 h4 hterm in hcut __
410
411(** val rTLabs_pc_inv_rect_Type2 :
412    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
413    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
414    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
415let rTLabs_pc_inv_rect_Type2 hterm h1 h2 h3 h4 =
416  let hcut = rTLabs_pc_rect_Type2 h1 h2 h3 h4 hterm in hcut __
417
418(** val rTLabs_pc_inv_rect_Type1 :
419    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
420    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
421    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
422let rTLabs_pc_inv_rect_Type1 hterm h1 h2 h3 h4 =
423  let hcut = rTLabs_pc_rect_Type1 h1 h2 h3 h4 hterm in hcut __
424
425(** val rTLabs_pc_inv_rect_Type0 :
426    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
427    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
428    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
429let rTLabs_pc_inv_rect_Type0 hterm h1 h2 h3 h4 =
430  let hcut = rTLabs_pc_rect_Type0 h1 h2 h3 h4 hterm in hcut __
431
432(** val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __ **)
433let rTLabs_pc_discr x y =
434  Logic.eq_rect_Type2 x
435    (match x with
436     | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
437     | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
438     | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
439     | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y
440
441(** val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __ **)
442let rTLabs_pc_jmdiscr x y =
443  Logic.eq_rect_Type2 x
444    (match x with
445     | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
446     | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
447     | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
448     | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y
449
450(** val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool **)
451let rTLabs_pc_eq x y =
452  match x with
453  | Rapc_state (b1, l1) ->
454    (match y with
455     | Rapc_state (b2, l2) ->
456       Bool.andb (Pointers.eq_block b1 b2)
457         (Identifiers.eq_identifier PreIdentifiers.LabelTag l1 l2)
458     | Rapc_call (x0, x1) -> Bool.False
459     | Rapc_ret x0 -> Bool.False
460     | Rapc_fin -> Bool.False)
461  | Rapc_call (o1, b1) ->
462    (match y with
463     | Rapc_state (x0, x1) -> Bool.False
464     | Rapc_call (o2, b2) ->
465       Bool.andb
466         (Deqsets.eqb
467           (Deqsets.deqOption
468             (Identifiers.deq_identifier PreIdentifiers.LabelTag))
469           (Obj.magic o1) (Obj.magic o2)) (Pointers.eq_block b1 b2)
470     | Rapc_ret x0 -> Bool.False
471     | Rapc_fin -> Bool.False)
472  | Rapc_ret b1 ->
473    (match y with
474     | Rapc_state (x0, x1) -> Bool.False
475     | Rapc_call (x0, x1) -> Bool.False
476     | Rapc_ret b2 ->
477       Deqsets.eqb (Deqsets.deqOption Pointers.block_eq) (Obj.magic b1)
478         (Obj.magic b2)
479     | Rapc_fin -> Bool.False)
480  | Rapc_fin ->
481    (match y with
482     | Rapc_state (x0, x1) -> Bool.False
483     | Rapc_call (x0, x1) -> Bool.False
484     | Rapc_ret x0 -> Bool.False
485     | Rapc_fin -> Bool.True)
486
487(** val rTLabs_deqset : Deqsets.deqSet **)
488let rTLabs_deqset =
489  Obj.magic rTLabs_pc_eq
490
491(** val rTLabs_ext_state_to_pc :
492    RTLabs_semantics.genv -> rTLabs_ext_state -> __ **)
493let rTLabs_ext_state_to_pc ge s =
494  let { ras_state = s'; ras_fn_stack = stk } = s in
495  (match s' with
496   | RTLabs_semantics.State (f, fs, m) ->
497     (match stk with
498      | List.Nil -> (fun _ -> assert false (* absurd case *))
499      | List.Cons (b, x) ->
500        (fun _ -> Obj.magic (Rapc_state (b, f.RTLabs_semantics.next))))
501   | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
502     (match stk with
503      | List.Nil -> (fun _ _ -> assert false (* absurd case *))
504      | List.Cons (b, x4) ->
505        (fun _ _ ->
506          Obj.magic (Rapc_call
507            ((match fs with
508              | List.Nil -> Types.None
509              | List.Cons (f, x6) -> Types.Some f.RTLabs_semantics.next), b))))
510       __
511   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
512     (match stk with
513      | List.Nil -> (fun _ -> Obj.magic (Rapc_ret Types.None))
514      | List.Cons (b, x3) -> (fun _ -> Obj.magic (Rapc_ret (Types.Some b))))
515   | RTLabs_semantics.Finalstate x -> (fun _ -> Obj.magic Rapc_fin)) __
516
517(** val rTLabs_pc_to_cost_label :
518    RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
519    -> CostLabel.costlabel Types.option **)
520let rTLabs_pc_to_cost_label ge = function
521| Rapc_state (b, l) ->
522  (match Globalenvs.find_funct_ptr ge b with
523   | Types.None -> Types.None
524   | Types.Some fd ->
525     (match fd with
526      | AST.Internal f ->
527        (match Identifiers.lookup PreIdentifiers.LabelTag
528                 f.RTLabs_syntax.f_graph l with
529         | Types.None -> Types.None
530         | Types.Some s -> CostSpec.cost_label_of s)
531      | AST.External x -> Types.None))
532| Rapc_call (x, x0) -> Types.None
533| Rapc_ret x -> Types.None
534| Rapc_fin -> Types.None
535
536(** val rTLabs_call_ident :
537    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident **)
538let rTLabs_call_ident ge s =
539  let s0 = s in
540  (let { ras_state = s'; ras_fn_stack = stk } = s0 in
541  (match s' with
542   | RTLabs_semantics.State (f, x, x0) ->
543     (fun _ -> assert false (* absurd case *))
544   | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid)
545   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
546     (fun _ -> assert false (* absurd case *))
547   | RTLabs_semantics.Finalstate x ->
548     (fun _ -> assert false (* absurd case *)))) __
549
550(** val rTLabs_status :
551    RTLabs_semantics.genv -> StructuredTraces.abstract_status **)
552let rTLabs_status ge =
553  { StructuredTraces.as_pc = rTLabs_deqset; StructuredTraces.as_pc_of =
554    (Obj.magic (rTLabs_ext_state_to_pc ge)); StructuredTraces.as_classify =
555    (fun h -> rTLabs_classify (Obj.magic h).ras_state);
556    StructuredTraces.as_label_of_pc =
557    (Obj.magic (rTLabs_pc_to_cost_label ge)); StructuredTraces.as_result =
558    (fun h -> RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
559    StructuredTraces.as_call_ident = (Obj.magic (rTLabs_call_ident ge));
560    StructuredTraces.as_tailcall_ident = (fun s -> assert false
561    (* absurd case *)) }
562
563(** val eval_ext_statement :
564    RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
565    (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO **)
566let eval_ext_statement ge s =
567  (match RTLabs_semantics.eval_statement ge s.ras_state with
568   | IOMonad.Interact (o, k) ->
569     (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.UnexpectedIO))
570   | IOMonad.Value ts ->
571     (fun next -> IOMonad.Value { Types.fst = ts.Types.fst; Types.snd =
572       (next ts.Types.snd ts.Types.fst __) })
573   | IOMonad.Wrong m -> (fun x -> IOMonad.Wrong m)) (fun x x0 _ ->
574    next_state ge s x x0)
575
576(** val rTLabs_ext_exec :
577    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
578let rTLabs_ext_exec =
579  { SmallstepExec.is_final = (fun x h ->
580    RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
581    SmallstepExec.step = (Obj.magic eval_ext_statement) }
582
583(** val make_ext_initial_state :
584    RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res **)
585let make_ext_initial_state p =
586  let ge = RTLabs_semantics.make_global p in
587  Obj.magic
588    (Monad.m_bind0 (Monad.max_def Errors.res0)
589      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
590      let main = p.AST.prog_main in
591      Obj.magic
592        (Errors.bind_eq
593          (Errors.opt_to_res (List.Cons ((Errors.MSG
594            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
595            (PreIdentifiers.SymbolTag, main)), List.Nil))))
596            (Globalenvs.find_symbol ge main)) (fun b _ ->
597          Errors.bind_eq
598            (Errors.opt_to_res (List.Cons ((Errors.MSG
599              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
600              (PreIdentifiers.SymbolTag, main)), List.Nil))))
601              (Globalenvs.find_funct_ptr ge b)) (fun f _ ->
602            let s = RTLabs_semantics.Callstate (main, f, List.Nil,
603              Types.None, List.Nil, m)
604            in
605            Obj.magic
606              (Monad.m_return0 (Monad.max_def Errors.res0) { ras_state = s;
607                ras_fn_stack = (List.Cons (b, List.Nil)) }))))))
608
609(** val rTLabs_ext_fullexec :
610    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
611let rTLabs_ext_fullexec =
612  { SmallstepExec.es1 = rTLabs_ext_exec; SmallstepExec.make_global =
613    (Obj.magic RTLabs_semantics.make_global);
614    SmallstepExec.make_initial_state = (Obj.magic make_ext_initial_state) }
615
Note: See TracBrowser for help on using the repository browser.