source: extracted/joint_fullexec.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 19.3 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open ExtraMonads
6
7open Deqsets_extra
8
9open State
10
11open Bind_new
12
13open BindLists
14
15open Blocks
16
17open TranslateUtils
18
19open ExtraGlobalenvs
20
21open I8051bis
22
23open String
24
25open Sets
26
27open Listb
28
29open LabelledObjects
30
31open BitVectorTrie
32
33open Graphs
34
35open I8051
36
37open Order
38
39open Registers
40
41open BackEndOps
42
43open Joint
44
45open BEMem
46
47open CostLabel
48
49open Events
50
51open IOMonad
52
53open IO
54
55open Extra_bool
56
57open Coqlib
58
59open Values
60
61open FrontEndVal
62
63open Hide
64
65open ByteValues
66
67open Division
68
69open Z
70
71open BitVectorZ
72
73open Pointers
74
75open GenMem
76
77open FrontEndMem
78
79open Proper
80
81open PositiveMap
82
83open Deqsets
84
85open Extralib
86
87open Lists
88
89open Identifiers
90
91open Exp
92
93open Arithmetic
94
95open Vector
96
97open Div_and_mod
98
99open Util
100
101open FoldStuff
102
103open BitVector
104
105open Extranat
106
107open Integers
108
109open AST
110
111open ErrorMessages
112
113open Option
114
115open Setoids
116
117open Monad
118
119open Jmeq
120
121open Russell
122
123open Positive
124
125open PreIdentifiers
126
127open Bool
128
129open Relations
130
131open Nat
132
133open List
134
135open Hints_declaration
136
137open Core_notation
138
139open Pts
140
141open Logic
142
143open Types
144
145open Errors
146
147open Globalenvs
148
149open Joint_semantics
150
151open SemanticsUtils
152
153open Traces
154
155open Stacksize
156
157open SmallstepExec
158
159open Executions
160
161open Measurable
162
163type joint_global = { jglobals : AST.ident List.list;
164                      jgenv : Joint_semantics.genv }
165
166(** val joint_global_rect_Type4 :
167    Joint_semantics.sem_params -> (AST.ident List.list ->
168    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
169let rec joint_global_rect_Type4 p h_mk_joint_global x_6006 =
170  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6006 in
171  h_mk_joint_global jglobals0 jgenv0
172
173(** val joint_global_rect_Type5 :
174    Joint_semantics.sem_params -> (AST.ident List.list ->
175    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
176let rec joint_global_rect_Type5 p h_mk_joint_global x_6008 =
177  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6008 in
178  h_mk_joint_global jglobals0 jgenv0
179
180(** val joint_global_rect_Type3 :
181    Joint_semantics.sem_params -> (AST.ident List.list ->
182    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
183let rec joint_global_rect_Type3 p h_mk_joint_global x_6010 =
184  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6010 in
185  h_mk_joint_global jglobals0 jgenv0
186
187(** val joint_global_rect_Type2 :
188    Joint_semantics.sem_params -> (AST.ident List.list ->
189    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
190let rec joint_global_rect_Type2 p h_mk_joint_global x_6012 =
191  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6012 in
192  h_mk_joint_global jglobals0 jgenv0
193
194(** val joint_global_rect_Type1 :
195    Joint_semantics.sem_params -> (AST.ident List.list ->
196    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
197let rec joint_global_rect_Type1 p h_mk_joint_global x_6014 =
198  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6014 in
199  h_mk_joint_global jglobals0 jgenv0
200
201(** val joint_global_rect_Type0 :
202    Joint_semantics.sem_params -> (AST.ident List.list ->
203    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
204let rec joint_global_rect_Type0 p h_mk_joint_global x_6016 =
205  let { jglobals = jglobals0; jgenv = jgenv0 } = x_6016 in
206  h_mk_joint_global jglobals0 jgenv0
207
208(** val jglobals :
209    Joint_semantics.sem_params -> joint_global -> AST.ident List.list **)
210let rec jglobals p xxx =
211  xxx.jglobals
212
213(** val jgenv :
214    Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv **)
215let rec jgenv p xxx =
216  xxx.jgenv
217
218(** val joint_global_inv_rect_Type4 :
219    Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
220    Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
221let joint_global_inv_rect_Type4 x1 hterm h1 =
222  let hcut = joint_global_rect_Type4 x1 h1 hterm in hcut __
223
224(** val joint_global_inv_rect_Type3 :
225    Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
226    Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
227let joint_global_inv_rect_Type3 x1 hterm h1 =
228  let hcut = joint_global_rect_Type3 x1 h1 hterm in hcut __
229
230(** val joint_global_inv_rect_Type2 :
231    Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
232    Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
233let joint_global_inv_rect_Type2 x1 hterm h1 =
234  let hcut = joint_global_rect_Type2 x1 h1 hterm in hcut __
235
236(** val joint_global_inv_rect_Type1 :
237    Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
238    Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
239let joint_global_inv_rect_Type1 x1 hterm h1 =
240  let hcut = joint_global_rect_Type1 x1 h1 hterm in hcut __
241
242(** val joint_global_inv_rect_Type0 :
243    Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
244    Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
245let joint_global_inv_rect_Type0 x1 hterm h1 =
246  let hcut = joint_global_rect_Type0 x1 h1 hterm in hcut __
247
248(** val joint_global_discr :
249    Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
250let joint_global_discr a1 x y =
251  Logic.eq_rect_Type2 x
252    (let { jglobals = a0; jgenv = a10 } = x in
253    Obj.magic (fun _ dH -> dH __ __)) y
254
255(** val joint_global_jmdiscr :
256    Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
257let joint_global_jmdiscr a1 x y =
258  Logic.eq_rect_Type2 x
259    (let { jglobals = a0; jgenv = a10 } = x in
260    Obj.magic (fun _ dH -> dH __ __)) y
261
262(** val dpi1__o__jgenv__o__inject :
263    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
264    Joint_semantics.genv Types.sig0 **)
265let dpi1__o__jgenv__o__inject x0 x2 =
266  x2.Types.dpi1.jgenv
267
268(** val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
269    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
270    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
271    Types.sig0 **)
272let dpi1__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
273  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
274    x2.Types.dpi1.jglobals x2.Types.dpi1.jgenv
275
276(** val dpi1__o__jgenv__o__genv_to_genv_t :
277    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
278    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
279let dpi1__o__jgenv__o__genv_to_genv_t x0 x2 =
280  let p = Joint_semantics.spp'__o__spp x0 in
281  let globals = x2.Types.dpi1.jglobals in
282  let g = x2.Types.dpi1.jgenv in g.Joint_semantics.ge
283
284(** val eject__o__jgenv__o__inject :
285    Joint_semantics.sem_params -> joint_global Types.sig0 ->
286    Joint_semantics.genv Types.sig0 **)
287let eject__o__jgenv__o__inject x0 x2 =
288  (Types.pi1 x2).jgenv
289
290(** val eject__o__jgenv__o__genv_to_genv_t__o__inject :
291    Joint_semantics.sem_params -> joint_global Types.sig0 ->
292    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
293    Types.sig0 **)
294let eject__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
295  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
296    (Types.pi1 x2).jglobals (Types.pi1 x2).jgenv
297
298(** val eject__o__jgenv__o__genv_to_genv_t :
299    Joint_semantics.sem_params -> joint_global Types.sig0 ->
300    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
301let eject__o__jgenv__o__genv_to_genv_t x0 x2 =
302  let p = Joint_semantics.spp'__o__spp x0 in
303  let globals = (Types.pi1 x2).jglobals in
304  let g = (Types.pi1 x2).jgenv in g.Joint_semantics.ge
305
306(** val jgenv__o__genv_to_genv_t :
307    Joint_semantics.sem_params -> joint_global ->
308    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
309let jgenv__o__genv_to_genv_t x0 x1 =
310  let p = Joint_semantics.spp'__o__spp x0 in
311  let globals = x1.jglobals in let g = x1.jgenv in g.Joint_semantics.ge
312
313(** val jgenv__o__genv_to_genv_t__o__inject :
314    Joint_semantics.sem_params -> joint_global ->
315    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
316    Types.sig0 **)
317let jgenv__o__genv_to_genv_t__o__inject x0 x1 =
318  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
319    x1.jglobals x1.jgenv
320
321(** val jgenv__o__inject :
322    Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
323    Types.sig0 **)
324let jgenv__o__inject x0 x1 =
325  x1.jgenv
326
327(** val dpi1__o__jgenv :
328    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
329    Joint_semantics.genv **)
330let dpi1__o__jgenv x0 x2 =
331  x2.Types.dpi1.jgenv
332
333(** val eject__o__jgenv :
334    Joint_semantics.sem_params -> joint_global Types.sig0 ->
335    Joint_semantics.genv **)
336let eject__o__jgenv x0 x2 =
337  (Types.pi1 x2).jgenv
338
339(** val eval_params_of_global :
340    Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params **)
341let eval_params_of_global p gl =
342  { Traces.globals = gl.jglobals; Traces.sparams = p; Traces.ev_genv =
343    gl.jgenv }
344
345(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
346    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
347    Joint.unserialized_params **)
348let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
349  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
350    (eval_params_of_global x0 x2.Types.dpi1)
351
352(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
353    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
354    Joint.uns_params **)
355let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
356  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
357    (eval_params_of_global x0 x2.Types.dpi1)
358
359(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
360    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
361    Joint.stmt_params **)
362let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
363  Traces.sparams__o__spp'__o__spp__o__stmt_pars
364    (eval_params_of_global x0 x2.Types.dpi1)
365
366(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
367    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
368    Joint.params **)
369let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
370  Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x2.Types.dpi1)
371
372(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
373    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
374    Joint_semantics.sem_state_params **)
375let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
376  Traces.sparams__o__spp'__o__msu_pars__o__st_pars
377    (eval_params_of_global x0 x2.Types.dpi1)
378
379(** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
380    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
381    Joint.joint_closed_internal_function
382    Joint_semantics.sem_unserialized_params **)
383let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
384  Traces.sparams__o__spp'__o__msu_pars
385    (eval_params_of_global x0 x2.Types.dpi1)
386
387(** val dpi1__o__eval_params_of_global__o__sparams__o__spp' :
388    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
389    Joint_semantics.serialized_params **)
390let dpi1__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
391  Traces.sparams__o__spp' (eval_params_of_global x0 x2.Types.dpi1)
392
393(** val dpi1__o__eval_params_of_global__o__sparams :
394    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
395    Joint_semantics.sem_params **)
396let dpi1__o__eval_params_of_global__o__sparams x0 x2 =
397  (eval_params_of_global x0 x2.Types.dpi1).Traces.sparams
398
399(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
400    Joint_semantics.sem_params -> joint_global Types.sig0 ->
401    Joint.unserialized_params **)
402let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
403  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
404    (eval_params_of_global x0 (Types.pi1 x2))
405
406(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
407    Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params **)
408let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
409  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
410    (eval_params_of_global x0 (Types.pi1 x2))
411
412(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
413    Joint_semantics.sem_params -> joint_global Types.sig0 ->
414    Joint.stmt_params **)
415let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
416  Traces.sparams__o__spp'__o__spp__o__stmt_pars
417    (eval_params_of_global x0 (Types.pi1 x2))
418
419(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
420    Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params **)
421let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
422  Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 (Types.pi1 x2))
423
424(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
425    Joint_semantics.sem_params -> joint_global Types.sig0 ->
426    Joint_semantics.sem_state_params **)
427let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
428  Traces.sparams__o__spp'__o__msu_pars__o__st_pars
429    (eval_params_of_global x0 (Types.pi1 x2))
430
431(** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
432    Joint_semantics.sem_params -> joint_global Types.sig0 ->
433    Joint.joint_closed_internal_function
434    Joint_semantics.sem_unserialized_params **)
435let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
436  Traces.sparams__o__spp'__o__msu_pars
437    (eval_params_of_global x0 (Types.pi1 x2))
438
439(** val eject__o__eval_params_of_global__o__sparams__o__spp' :
440    Joint_semantics.sem_params -> joint_global Types.sig0 ->
441    Joint_semantics.serialized_params **)
442let eject__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
443  Traces.sparams__o__spp' (eval_params_of_global x0 (Types.pi1 x2))
444
445(** val eject__o__eval_params_of_global__o__sparams :
446    Joint_semantics.sem_params -> joint_global Types.sig0 ->
447    Joint_semantics.sem_params **)
448let eject__o__eval_params_of_global__o__sparams x0 x2 =
449  (eval_params_of_global x0 (Types.pi1 x2)).Traces.sparams
450
451(** val eval_params_of_global__o__sparams :
452    Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params **)
453let eval_params_of_global__o__sparams x0 x1 =
454  (eval_params_of_global x0 x1).Traces.sparams
455
456(** val eval_params_of_global__o__sparams__o__spp' :
457    Joint_semantics.sem_params -> joint_global ->
458    Joint_semantics.serialized_params **)
459let eval_params_of_global__o__sparams__o__spp' x0 x1 =
460  Traces.sparams__o__spp' (eval_params_of_global x0 x1)
461
462(** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
463    Joint_semantics.sem_params -> joint_global ->
464    Joint.joint_closed_internal_function
465    Joint_semantics.sem_unserialized_params **)
466let eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x1 =
467  Traces.sparams__o__spp'__o__msu_pars (eval_params_of_global x0 x1)
468
469(** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
470    Joint_semantics.sem_params -> joint_global ->
471    Joint_semantics.sem_state_params **)
472let eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x1 =
473  Traces.sparams__o__spp'__o__msu_pars__o__st_pars
474    (eval_params_of_global x0 x1)
475
476(** val eval_params_of_global__o__sparams__o__spp'__o__spp :
477    Joint_semantics.sem_params -> joint_global -> Joint.params **)
478let eval_params_of_global__o__sparams__o__spp'__o__spp x0 x1 =
479  Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x1)
480
481(** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
482    Joint_semantics.sem_params -> joint_global -> Joint.stmt_params **)
483let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x1 =
484  Traces.sparams__o__spp'__o__spp__o__stmt_pars (eval_params_of_global x0 x1)
485
486(** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
487    Joint_semantics.sem_params -> joint_global -> Joint.uns_params **)
488let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x1 =
489  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
490    (eval_params_of_global x0 x1)
491
492(** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
493    Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params **)
494let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x1 =
495  Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
496    (eval_params_of_global x0 x1)
497
498(** val dpi1__o__eval_params_of_global :
499    Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
500    Traces.evaluation_params **)
501let dpi1__o__eval_params_of_global x0 x2 =
502  eval_params_of_global x0 x2.Types.dpi1
503
504(** val eject__o__eval_params_of_global :
505    Joint_semantics.sem_params -> joint_global Types.sig0 ->
506    Traces.evaluation_params **)
507let eject__o__eval_params_of_global x0 x2 =
508  eval_params_of_global x0 (Types.pi1 x2)
509
510(** val make_joint_global :
511    Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
512    Types.option) Types.prod -> joint_global **)
513let make_joint_global pars p_stack =
514  let p = p_stack.Types.fst in
515  let stack_sizes = p_stack.Types.snd in
516  let ev_pars =
517    Traces.make_global { Traces.prog_spars = pars; Traces.prog = p;
518      Traces.stack_sizes = stack_sizes }
519  in
520  { jglobals = ev_pars.Traces.globals; jgenv = ev_pars.Traces.ev_genv }
521
522(** val joint_exec :
523    Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
524    SmallstepExec.trans_system **)
525let joint_exec g =
526  { SmallstepExec.is_final = (fun env ->
527    Obj.magic
528      (Traces.joint_final g (Obj.magic env).jglobals (Obj.magic env).jgenv));
529    SmallstepExec.step = (fun env st ->
530    Obj.magic
531      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
532        (Obj.magic
533          (Joint_semantics.eval_state g (Obj.magic env).jglobals
534            (Obj.magic env).jgenv (Obj.magic st))) (fun st' ->
535        let charge =
536          match Traces.joint_label_of_pc
537                  (eval_params_of_global g (Obj.magic env))
538                  (Obj.magic st).Joint_semantics.pc with
539          | Types.None -> Events.e0
540          | Types.Some c -> Events.echarge c
541        in
542        Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = charge;
543          Types.snd = st' }))) }
544
545(** val joint_fullexec :
546    Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
547    SmallstepExec.fullexec **)
548let joint_fullexec g =
549  { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
550    (Obj.magic (make_joint_global g)); SmallstepExec.make_initial_state =
551    (fun p_stacks ->
552    Obj.magic
553      (Monad.m_return0 (Monad.max_def Errors.res0)
554        (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
555          (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
556          (Obj.magic p_stacks).Types.snd }))) }
557
558(** val joint_preclassified_system :
559    Joint_semantics.sem_params -> Measurable.preclassified_system **)
560let joint_preclassified_system g =
561  { Measurable.pcs_exec = (joint_fullexec g); Measurable.pcs_labelled =
562    (fun env st ->
563    Bool.notb
564      (PositiveMap.is_none
565        (Traces.joint_label_of_pc (eval_params_of_global g (Obj.magic env))
566          (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
567    (fun env ->
568    Obj.magic
569      (Traces.joint_classify (eval_params_of_global g (Obj.magic env))));
570    Measurable.pcs_callee = (fun env s _ ->
571    Traces.joint_call_ident (eval_params_of_global g (Obj.magic env))
572      (Obj.magic s)) }
573
Note: See TracBrowser for help on using the repository browser.