source: extracted/joint_fullexec.ml @ 2829

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

Semantics files committed.

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