source: extracted/traces.ml @ 3019

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

New extraction after ERTLptr abortion.

File size: 24.6 KB
RevLine 
[2829]1open Preamble
2
[2951]3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
[2829]17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
[2951]149open SemanticsUtils
150
[2829]151open StructuredTraces
152
153type evaluation_params = { globals : AST.ident List.list;
154                           ev_genv : Joint_semantics.genv }
155
156(** val evaluation_params_rect_Type4 :
[2960]157    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_316 =
160  let { globals = globals0; ev_genv = ev_genv0 } = x_316 in
[2960]161  h_mk_evaluation_params globals0 ev_genv0
[2829]162
163(** val evaluation_params_rect_Type5 :
[2960]164    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_318 =
167  let { globals = globals0; ev_genv = ev_genv0 } = x_318 in
[2960]168  h_mk_evaluation_params globals0 ev_genv0
[2829]169
170(** val evaluation_params_rect_Type3 :
[2960]171    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_320 =
174  let { globals = globals0; ev_genv = ev_genv0 } = x_320 in
[2960]175  h_mk_evaluation_params globals0 ev_genv0
[2829]176
177(** val evaluation_params_rect_Type2 :
[2960]178    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_322 =
181  let { globals = globals0; ev_genv = ev_genv0 } = x_322 in
[2960]182  h_mk_evaluation_params globals0 ev_genv0
[2829]183
184(** val evaluation_params_rect_Type1 :
[2960]185    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_324 =
188  let { globals = globals0; ev_genv = ev_genv0 } = x_324 in
[2960]189  h_mk_evaluation_params globals0 ev_genv0
[2829]190
191(** val evaluation_params_rect_Type0 :
[2960]192    Joint_semantics.sem_params -> (AST.ident List.list ->
[2829]193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
[3019]194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_326 =
195  let { globals = globals0; ev_genv = ev_genv0 } = x_326 in
[2960]196  h_mk_evaluation_params globals0 ev_genv0
[2829]197
[2960]198(** val globals :
199    Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
200let rec globals p xxx =
[2829]201  xxx.globals
202
[2960]203(** val ev_genv :
204    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
205let rec ev_genv p xxx =
[2829]206  xxx.ev_genv
207
208(** val evaluation_params_inv_rect_Type4 :
[2960]209    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
[2829]210    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
[2960]211let evaluation_params_inv_rect_Type4 x1 hterm h1 =
212  let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __
[2829]213
214(** val evaluation_params_inv_rect_Type3 :
[2960]215    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
[2829]216    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
[2960]217let evaluation_params_inv_rect_Type3 x1 hterm h1 =
218  let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __
[2829]219
220(** val evaluation_params_inv_rect_Type2 :
[2960]221    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
[2829]222    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
[2960]223let evaluation_params_inv_rect_Type2 x1 hterm h1 =
224  let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __
[2829]225
226(** val evaluation_params_inv_rect_Type1 :
[2960]227    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
[2829]228    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
[2960]229let evaluation_params_inv_rect_Type1 x1 hterm h1 =
230  let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __
[2829]231
232(** val evaluation_params_inv_rect_Type0 :
[2960]233    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
[2829]234    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
[2960]235let evaluation_params_inv_rect_Type0 x1 hterm h1 =
236  let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __
[2829]237
[2960]238(** val evaluation_params_discr :
239    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
240    __ **)
241let evaluation_params_discr a1 x y =
242  Logic.eq_rect_Type2 x
243    (let { globals = a0; ev_genv = a10 } = x in
244    Obj.magic (fun _ dH -> dH __ __)) y
245
[2829]246(** val evaluation_params_jmdiscr :
[2960]247    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
248    __ **)
249let evaluation_params_jmdiscr a1 x y =
[2829]250  Logic.eq_rect_Type2 x
[2960]251    (let { globals = a0; ev_genv = a10 } = x in
252    Obj.magic (fun _ dH -> dH __ __)) y
[2829]253
[2960]254(** val dpi1__o__ev_genv__o__inject :
255    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
256    Joint_semantics.genv Types.sig0 **)
257let dpi1__o__ev_genv__o__inject x0 x2 =
258  x2.Types.dpi1.ev_genv
[2951]259
[2960]260(** val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject :
261    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
262    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
263    Types.sig0 **)
264let dpi1__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 =
265  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
266    x2.Types.dpi1.globals x2.Types.dpi1.ev_genv
[2829]267
[2960]268(** val dpi1__o__ev_genv__o__genv_to_genv_t :
269    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
270    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
271let dpi1__o__ev_genv__o__genv_to_genv_t x0 x2 =
272  let p = Joint_semantics.spp'__o__spp x0 in
273  let globals0 = x2.Types.dpi1.globals in
274  let g = x2.Types.dpi1.ev_genv in g.Joint_semantics.ge
[2829]275
[2960]276(** val eject__o__ev_genv__o__inject :
277    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
278    Joint_semantics.genv Types.sig0 **)
279let eject__o__ev_genv__o__inject x0 x2 =
280  (Types.pi1 x2).ev_genv
[2829]281
[2960]282(** val eject__o__ev_genv__o__genv_to_genv_t__o__inject :
283    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
284    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
285    Types.sig0 **)
286let eject__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 =
287  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
288    (Types.pi1 x2).globals (Types.pi1 x2).ev_genv
[2829]289
[2960]290(** val eject__o__ev_genv__o__genv_to_genv_t :
291    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
292    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
293let eject__o__ev_genv__o__genv_to_genv_t x0 x2 =
294  let p = Joint_semantics.spp'__o__spp x0 in
295  let globals0 = (Types.pi1 x2).globals in
296  let g = (Types.pi1 x2).ev_genv in g.Joint_semantics.ge
[2829]297
[2960]298(** val ev_genv__o__genv_to_genv_t :
299    Joint_semantics.sem_params -> evaluation_params ->
300    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
301let ev_genv__o__genv_to_genv_t x0 x1 =
302  let p = Joint_semantics.spp'__o__spp x0 in
303  let globals0 = x1.globals in let g = x1.ev_genv in g.Joint_semantics.ge
[2829]304
[2960]305(** val ev_genv__o__genv_to_genv_t__o__inject :
306    Joint_semantics.sem_params -> evaluation_params ->
307    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
308    Types.sig0 **)
309let ev_genv__o__genv_to_genv_t__o__inject x0 x1 =
310  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
311    x1.globals x1.ev_genv
312
313(** val ev_genv__o__inject :
314    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
315    Types.sig0 **)
316let ev_genv__o__inject x0 x1 =
317  x1.ev_genv
318
319(** val dpi1__o__ev_genv :
320    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
321    Joint_semantics.genv **)
322let dpi1__o__ev_genv x0 x2 =
323  x2.Types.dpi1.ev_genv
324
325(** val eject__o__ev_genv :
326    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
327    Joint_semantics.genv **)
328let eject__o__ev_genv x0 x2 =
329  (Types.pi1 x2).ev_genv
330
[2829]331type prog_params = { prog_spars : Joint_semantics.sem_params;
332                     prog : Joint.joint_program;
333                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
334
335(** val prog_params_rect_Type4 :
336    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
337    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]338let rec prog_params_rect_Type4 h_mk_prog_params x_342 =
[2829]339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]340    stack_sizes0 } = x_342
[2829]341  in
342  h_mk_prog_params prog_spars0 prog0 stack_sizes0
343
344(** val prog_params_rect_Type5 :
345    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
346    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]347let rec prog_params_rect_Type5 h_mk_prog_params x_344 =
[2829]348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]349    stack_sizes0 } = x_344
[2829]350  in
351  h_mk_prog_params prog_spars0 prog0 stack_sizes0
352
353(** val prog_params_rect_Type3 :
354    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
355    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]356let rec prog_params_rect_Type3 h_mk_prog_params x_346 =
[2829]357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]358    stack_sizes0 } = x_346
[2829]359  in
360  h_mk_prog_params prog_spars0 prog0 stack_sizes0
361
362(** val prog_params_rect_Type2 :
363    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
364    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]365let rec prog_params_rect_Type2 h_mk_prog_params x_348 =
[2829]366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]367    stack_sizes0 } = x_348
[2829]368  in
369  h_mk_prog_params prog_spars0 prog0 stack_sizes0
370
371(** val prog_params_rect_Type1 :
372    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
373    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]374let rec prog_params_rect_Type1 h_mk_prog_params x_350 =
[2829]375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]376    stack_sizes0 } = x_350
[2829]377  in
378  h_mk_prog_params prog_spars0 prog0 stack_sizes0
379
380(** val prog_params_rect_Type0 :
381    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
382    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
[3019]383let rec prog_params_rect_Type0 h_mk_prog_params x_352 =
[2829]384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
[3019]385    stack_sizes0 } = x_352
[2829]386  in
387  h_mk_prog_params prog_spars0 prog0 stack_sizes0
388
389(** val prog_spars : prog_params -> Joint_semantics.sem_params **)
390let rec prog_spars xxx =
391  xxx.prog_spars
392
393(** val prog : prog_params -> Joint.joint_program **)
394let rec prog xxx =
395  xxx.prog
396
397(** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
398let rec stack_sizes xxx =
399  xxx.stack_sizes
400
401(** val prog_params_inv_rect_Type4 :
402    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
403    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
404let prog_params_inv_rect_Type4 hterm h1 =
405  let hcut = prog_params_rect_Type4 h1 hterm in hcut __
406
407(** val prog_params_inv_rect_Type3 :
408    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
409    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
410let prog_params_inv_rect_Type3 hterm h1 =
411  let hcut = prog_params_rect_Type3 h1 hterm in hcut __
412
413(** val prog_params_inv_rect_Type2 :
414    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
415    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
416let prog_params_inv_rect_Type2 hterm h1 =
417  let hcut = prog_params_rect_Type2 h1 hterm in hcut __
418
419(** val prog_params_inv_rect_Type1 :
420    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
421    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
422let prog_params_inv_rect_Type1 hterm h1 =
423  let hcut = prog_params_rect_Type1 h1 hterm in hcut __
424
425(** val prog_params_inv_rect_Type0 :
426    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
427    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
428let prog_params_inv_rect_Type0 hterm h1 =
429  let hcut = prog_params_rect_Type0 h1 hterm in hcut __
430
431(** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
432let prog_params_jmdiscr x y =
433  Logic.eq_rect_Type2 x
434    (let { prog_spars = a0; prog = a1; stack_sizes = a2 } = x in
435    Obj.magic (fun _ dH -> dH __ __ __)) y
436
[2960]437(** val prog_spars__o__spp' :
[2951]438    prog_params -> Joint_semantics.serialized_params **)
[2960]439let prog_spars__o__spp' x0 =
440  x0.prog_spars.Joint_semantics.spp'
[2951]441
[2960]442(** val prog_spars__o__spp'__o__msu_pars :
[2829]443    prog_params -> Joint.joint_closed_internal_function
444    Joint_semantics.sem_unserialized_params **)
[2960]445let prog_spars__o__spp'__o__msu_pars x0 =
446  Joint_semantics.spp'__o__msu_pars x0.prog_spars
[2829]447
[2960]448(** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
[2829]449    prog_params -> Joint_semantics.sem_state_params **)
[2960]450let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 =
451  Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars
[2829]452
[2960]453(** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **)
454let prog_spars__o__spp'__o__spp x0 =
455  Joint_semantics.spp'__o__spp x0.prog_spars
[2829]456
[2960]457(** val prog_spars__o__spp'__o__spp__o__stmt_pars :
[2829]458    prog_params -> Joint.stmt_params **)
[2960]459let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
460  Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars
[2829]461
[2960]462(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
[2829]463    prog_params -> Joint.uns_params **)
[2960]464let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
465  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars
[2829]466
[2960]467(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
[2829]468    prog_params -> Joint.unserialized_params **)
[2960]469let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
470  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
471    x0.prog_spars
[2829]472
[2960]473(** val joint_make_global : prog_params -> evaluation_params **)
474let joint_make_global p =
475  { globals = (AST.prog_var_names p.prog.Joint.joint_prog); ev_genv =
476    (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }
477
478(** val joint_make_global__o__ev_genv :
479    prog_params -> Joint_semantics.genv **)
480let joint_make_global__o__ev_genv x0 =
481  (joint_make_global x0).ev_genv
482
483(** val joint_make_global__o__ev_genv__o__genv_to_genv_t :
484    prog_params -> Joint.joint_closed_internal_function AST.fundef
485    Globalenvs.genv_t **)
486let joint_make_global__o__ev_genv__o__genv_to_genv_t x0 =
487  ev_genv__o__genv_to_genv_t x0.prog_spars (joint_make_global x0)
488
489(** val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject :
490    prog_params -> Joint.joint_closed_internal_function AST.fundef
491    Globalenvs.genv_t Types.sig0 **)
492let joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject x0 =
493  ev_genv__o__genv_to_genv_t__o__inject x0.prog_spars (joint_make_global x0)
494
495(** val joint_make_global__o__ev_genv__o__inject :
496    prog_params -> Joint_semantics.genv Types.sig0 **)
497let joint_make_global__o__ev_genv__o__inject x0 =
498  ev_genv__o__inject x0.prog_spars (joint_make_global x0)
499
500(** val joint_make_global__o__inject :
501    prog_params -> evaluation_params Types.sig0 **)
502let joint_make_global__o__inject x0 =
503  joint_make_global x0
504
[2968]505(** val make_initial_state :
506    prog_params -> Joint_semantics.state_pc Errors.res **)
[2829]507let make_initial_state pars =
508  let p = pars.prog in
[2960]509  let ge = ev_genv pars.prog_spars in
[2968]510  Obj.magic
511    (Monad.m_bind0 (Monad.max_def Errors.res0)
512      (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
513      (fun m0 ->
514      (let { Types.fst = m; Types.snd = spb } =
515         GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
516       in
517      (fun _ ->
518      let globals_size =
519        Joint.globals_stacksize
520          (Joint_semantics.spp'__o__spp pars.prog_spars) p
521      in
522      let spp = { Pointers.pblock = spb; Pointers.poff =
523        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
524          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
[3019]525          (Nat.S Nat.O))))))))))))))))
526          (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
[2968]527      in
[3001]528      let main = AST.prog_main p.Joint.joint_prog in
[2968]529      let st = { Joint_semantics.st_frms = (Types.Some
530        (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
531        Joint_semantics.istack = Joint_semantics.Empty_is;
532        Joint_semantics.carry = (ByteValues.BBbit Bool.False);
533        Joint_semantics.regs =
534        ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
535          spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
536        globals_size }
537      in
538      Monad.m_return0 (Monad.max_def Errors.res0)
539        { Joint_semantics.st_no_pc =
540        (Joint_semantics.set_sp
541          (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
542        Joint_semantics.pc = Joint_semantics.init_pc;
543        Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
544        __))
[2829]545
546(** val joint_classify_step :
[2960]547    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
548    StructuredTraces.status_class **)
549let joint_classify_step p g = function
[2829]550| Joint.COST_LABEL x -> StructuredTraces.Cl_other
551| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
552| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
553| Joint.Step_seq x -> StructuredTraces.Cl_other
554
555(** val joint_classify_final :
[2960]556    Joint.unserialized_params -> Joint.joint_fin_step ->
[2829]557    StructuredTraces.status_class **)
558let joint_classify_final p = function
559| Joint.GOTO x -> StructuredTraces.Cl_other
560| Joint.RETURN -> StructuredTraces.Cl_return
561| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall
562
563(** val joint_classify :
[2960]564    Joint_semantics.sem_params -> evaluation_params ->
565    Joint_semantics.state_pc -> StructuredTraces.status_class **)
566let joint_classify p pars st =
567  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
568          st.Joint_semantics.pc with
[2829]569  | Errors.OK i_fn_s ->
570    (match i_fn_s.Types.snd with
[2960]571     | Joint.Sequential (s, x) ->
572       joint_classify_step
573         (Joint.uns_pars__o__u_pars
574           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
575     | Joint.Final s ->
576       joint_classify_final
577         (Joint.uns_pars__o__u_pars
578           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
[2829]579     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
580  | Errors.Error x -> StructuredTraces.Cl_other
581
582(** val joint_call_ident :
[2960]583    Joint_semantics.sem_params -> evaluation_params ->
584    Joint_semantics.state_pc -> AST.ident **)
585let joint_call_ident p pars st =
[2829]586  let dummy = Positive.One in
[2960]587  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
588           st.Joint_semantics.pc with
[2829]589   | Errors.OK x ->
590     (match x.Types.snd with
591      | Joint.Sequential (s, next) ->
592        (match s with
593         | Joint.COST_LABEL x0 -> dummy
[2933]594         | Joint.CALL (f', args, dest) ->
595           (match Obj.magic
596                    (Monad.m_bind0 (Monad.max_def Errors.res0)
[2960]597                      (Joint_semantics.block_of_call p pars.globals
598                        (let p0 = Joint_semantics.spp'__o__spp p in
599                        let globals0 = pars.globals in
600                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
[2933]601                        st.Joint_semantics.st_no_pc) (fun bl ->
602                      Obj.magic
[2960]603                        (Joint_semantics.fetch_internal_function pars.globals
604                          pars.ev_genv bl))) with
[2933]605            | Errors.OK i_f -> i_f.Types.fst
606            | Errors.Error x0 -> dummy)
[2829]607         | Joint.COND (x0, x1) -> dummy
[2933]608         | Joint.Step_seq x0 -> dummy)
[2829]609      | Joint.Final x0 -> dummy
610      | Joint.FCOND (x0, x1, x2) -> dummy)
611   | Errors.Error x -> dummy)
612
613(** val joint_tailcall_ident :
[2960]614    Joint_semantics.sem_params -> evaluation_params ->
615    Joint_semantics.state_pc -> AST.ident **)
616let joint_tailcall_ident p pars st =
[2829]617  let dummy = Positive.One in
[2960]618  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
619           st.Joint_semantics.pc with
[2829]620   | Errors.OK x ->
621     (match x.Types.snd with
622      | Joint.Sequential (x0, x1) -> dummy
623      | Joint.Final s ->
624        (match s with
625         | Joint.GOTO x0 -> dummy
626         | Joint.RETURN -> dummy
627         | Joint.TAILCALL (f', args) ->
628           (match Obj.magic
629                    (Monad.m_bind0 (Monad.max_def Errors.res0)
[2960]630                      (Joint_semantics.block_of_call p pars.globals
631                        (let p0 = Joint_semantics.spp'__o__spp p in
632                        let globals0 = pars.globals in
633                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
[2829]634                        st.Joint_semantics.st_no_pc) (fun bl ->
635                      Obj.magic
[2960]636                        (Joint_semantics.fetch_internal_function pars.globals
637                          pars.ev_genv bl))) with
[2829]638            | Errors.OK i_f -> i_f.Types.fst
639            | Errors.Error x0 -> dummy))
640      | Joint.FCOND (x0, x1, x2) -> dummy)
641   | Errors.Error x -> dummy)
642
643(** val pcDeq : Deqsets.deqSet **)
644let pcDeq =
645  Obj.magic ByteValues.eq_program_counter
646
647(** val cost_label_of_stmt :
[2997]648    Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
649    CostLabel.costlabel Types.option **)
650let cost_label_of_stmt p g = function
[2829]651| Joint.Sequential (s0, x) ->
652  (match s0 with
653   | Joint.COST_LABEL lbl -> Types.Some lbl
654   | Joint.CALL (x0, x1, x2) -> Types.None
655   | Joint.COND (x0, x1) -> Types.None
656   | Joint.Step_seq x0 -> Types.None)
657| Joint.Final x -> Types.None
658| Joint.FCOND (x0, x1, x2) -> Types.None
659
660(** val joint_label_of_pc :
[2960]661    Joint_semantics.sem_params -> evaluation_params ->
662    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
663let joint_label_of_pc p pars pc =
664  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
[2997]665  | Errors.OK fn_stmt ->
666    cost_label_of_stmt (Joint_semantics.spp'__o__spp__o__stmt_pars p)
667      pars.globals fn_stmt.Types.snd
[2829]668  | Errors.Error x -> Types.None
669
[2951]670(** val exit_pc' : ByteValues.program_counter **)
671let exit_pc' =
672  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
673    ByteValues.pc_offset = (Positive.P1 Positive.One) }
674
675(** val joint_final :
[2960]676    Joint_semantics.sem_params -> evaluation_params ->
677    Joint_semantics.state_pc -> Integers.int Types.option **)
678let joint_final p pars st =
679  let ge = pars.ev_genv in
680  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
681   | Bool.True ->
682     let ret =
683       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
684     in
[2967]685     (match Obj.magic
686              (Monad.m_bind0 (Monad.max_def Errors.res0)
687                (Obj.magic
688                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
689                    pars.globals
690                    (let p0 = Joint_semantics.spp'__o__spp p in
691                    let globals0 = pars.globals in
692                    let g = ge in g.Joint_semantics.ge) ret
693                    st.Joint_semantics.st_no_pc)) (fun vals ->
694                Obj.magic (ByteValues.word_of_list_beval vals))) with
695      | Errors.OK v -> Types.Some v
696      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
[2960]697   | Bool.False -> Types.None)
[2951]698
[2829]699(** val joint_abstract_status :
700    prog_params -> StructuredTraces.abstract_status **)
701let joint_abstract_status p =
702  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
703    (Obj.magic
[2960]704      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
705    StructuredTraces.as_classify =
706    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
[2829]707    StructuredTraces.as_label_of_pc =
[2960]708    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
[2829]709    StructuredTraces.as_result =
[2960]710    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
[2951]711    StructuredTraces.as_call_ident = (fun st ->
[2960]712    joint_call_ident p.prog_spars (joint_make_global p)
713      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
714    (fun st ->
715    joint_tailcall_ident p.prog_spars (joint_make_global p)
716      (Types.pi1 (Obj.magic st))) }
[2829]717
718(** val joint_status :
719    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
720    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
721let joint_status p prog0 stacksizes =
722  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
723    stacksizes }
724
Note: See TracBrowser for help on using the repository browser.