source: extracted/traces.ml @ 2960

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

New extraction, it diverges in RTL execution now.

File size: 24.1 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
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
149open SemanticsUtils
150
151open StructuredTraces
152
153type evaluation_params = { globals : AST.ident List.list;
154                           ev_genv : Joint_semantics.genv }
155
156(** val evaluation_params_rect_Type4 :
157    Joint_semantics.sem_params -> (AST.ident List.list ->
158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_55 =
160  let { globals = globals0; ev_genv = ev_genv0 } = x_55 in
161  h_mk_evaluation_params globals0 ev_genv0
162
163(** val evaluation_params_rect_Type5 :
164    Joint_semantics.sem_params -> (AST.ident List.list ->
165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_57 =
167  let { globals = globals0; ev_genv = ev_genv0 } = x_57 in
168  h_mk_evaluation_params globals0 ev_genv0
169
170(** val evaluation_params_rect_Type3 :
171    Joint_semantics.sem_params -> (AST.ident List.list ->
172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_59 =
174  let { globals = globals0; ev_genv = ev_genv0 } = x_59 in
175  h_mk_evaluation_params globals0 ev_genv0
176
177(** val evaluation_params_rect_Type2 :
178    Joint_semantics.sem_params -> (AST.ident List.list ->
179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_61 =
181  let { globals = globals0; ev_genv = ev_genv0 } = x_61 in
182  h_mk_evaluation_params globals0 ev_genv0
183
184(** val evaluation_params_rect_Type1 :
185    Joint_semantics.sem_params -> (AST.ident List.list ->
186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_63 =
188  let { globals = globals0; ev_genv = ev_genv0 } = x_63 in
189  h_mk_evaluation_params globals0 ev_genv0
190
191(** val evaluation_params_rect_Type0 :
192    Joint_semantics.sem_params -> (AST.ident List.list ->
193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_65 =
195  let { globals = globals0; ev_genv = ev_genv0 } = x_65 in
196  h_mk_evaluation_params globals0 ev_genv0
197
198(** val globals :
199    Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
200let rec globals p xxx =
201  xxx.globals
202
203(** val ev_genv :
204    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
205let rec ev_genv p xxx =
206  xxx.ev_genv
207
208(** val evaluation_params_inv_rect_Type4 :
209    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
210    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
211let evaluation_params_inv_rect_Type4 x1 hterm h1 =
212  let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __
213
214(** val evaluation_params_inv_rect_Type3 :
215    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
216    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
217let evaluation_params_inv_rect_Type3 x1 hterm h1 =
218  let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __
219
220(** val evaluation_params_inv_rect_Type2 :
221    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
222    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
223let evaluation_params_inv_rect_Type2 x1 hterm h1 =
224  let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __
225
226(** val evaluation_params_inv_rect_Type1 :
227    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
228    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
229let evaluation_params_inv_rect_Type1 x1 hterm h1 =
230  let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __
231
232(** val evaluation_params_inv_rect_Type0 :
233    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
234    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
235let evaluation_params_inv_rect_Type0 x1 hterm h1 =
236  let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __
237
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
246(** val evaluation_params_jmdiscr :
247    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
248    __ **)
249let evaluation_params_jmdiscr a1 x y =
250  Logic.eq_rect_Type2 x
251    (let { globals = a0; ev_genv = a10 } = x in
252    Obj.magic (fun _ dH -> dH __ __)) y
253
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
259
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
267
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
275
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
281
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
289
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
297
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
304
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
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 **)
338let rec prog_params_rect_Type4 h_mk_prog_params x_81 =
339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
340    stack_sizes0 } = x_81
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 **)
347let rec prog_params_rect_Type5 h_mk_prog_params x_83 =
348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
349    stack_sizes0 } = x_83
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 **)
356let rec prog_params_rect_Type3 h_mk_prog_params x_85 =
357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
358    stack_sizes0 } = x_85
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 **)
365let rec prog_params_rect_Type2 h_mk_prog_params x_87 =
366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
367    stack_sizes0 } = x_87
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 **)
374let rec prog_params_rect_Type1 h_mk_prog_params x_89 =
375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
376    stack_sizes0 } = x_89
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 **)
383let rec prog_params_rect_Type0 h_mk_prog_params x_91 =
384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
385    stack_sizes0 } = x_91
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
437(** val prog_spars__o__spp' :
438    prog_params -> Joint_semantics.serialized_params **)
439let prog_spars__o__spp' x0 =
440  x0.prog_spars.Joint_semantics.spp'
441
442(** val prog_spars__o__spp'__o__msu_pars :
443    prog_params -> Joint.joint_closed_internal_function
444    Joint_semantics.sem_unserialized_params **)
445let prog_spars__o__spp'__o__msu_pars x0 =
446  Joint_semantics.spp'__o__msu_pars x0.prog_spars
447
448(** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
449    prog_params -> Joint_semantics.sem_state_params **)
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
452
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
456
457(** val prog_spars__o__spp'__o__spp__o__stmt_pars :
458    prog_params -> Joint.stmt_params **)
459let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
460  Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars
461
462(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
463    prog_params -> Joint.uns_params **)
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
466
467(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
468    prog_params -> Joint.unserialized_params **)
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
472
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
505(** val make_initial_state : prog_params -> Joint_semantics.state_pc **)
506let make_initial_state pars =
507  let p = pars.prog in
508  let ge = ev_genv pars.prog_spars in
509  let m0 =
510    (Globalenvs.globalenv_allocmem (fun x -> x) p.Joint.joint_prog).Types.snd
511  in
512  (let { Types.fst = m; Types.snd = spb } =
513     GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
514   in
515  (fun _ ->
516  let globals_size =
517    Joint.globals_stacksize (Joint_semantics.spp'__o__spp pars.prog_spars) p
518  in
519  let spp = { Pointers.pblock = spb; Pointers.poff =
520    (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522      Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
523  in
524  let main = p.Joint.joint_prog.AST.prog_main in
525  let st = { Joint_semantics.st_frms = (Types.Some
526    (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
527    Joint_semantics.istack = Joint_semantics.Empty_is;
528    Joint_semantics.carry = (ByteValues.BBbit Bool.False);
529    Joint_semantics.regs =
530    ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
531      spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
532    globals_size }
533  in
534  { Joint_semantics.st_no_pc =
535  (Joint_semantics.set_sp (prog_spars__o__spp'__o__msu_pars__o__st_pars pars)
536    spp st); Joint_semantics.pc = Joint_semantics.init_pc;
537  Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) })) __
538
539(** val joint_classify_step :
540    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
541    StructuredTraces.status_class **)
542let joint_classify_step p g = function
543| Joint.COST_LABEL x -> StructuredTraces.Cl_other
544| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
545| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
546| Joint.Step_seq x -> StructuredTraces.Cl_other
547
548(** val joint_classify_final :
549    Joint.unserialized_params -> Joint.joint_fin_step ->
550    StructuredTraces.status_class **)
551let joint_classify_final p = function
552| Joint.GOTO x -> StructuredTraces.Cl_other
553| Joint.RETURN -> StructuredTraces.Cl_return
554| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall
555
556(** val joint_classify :
557    Joint_semantics.sem_params -> evaluation_params ->
558    Joint_semantics.state_pc -> StructuredTraces.status_class **)
559let joint_classify p pars st =
560  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
561          st.Joint_semantics.pc with
562  | Errors.OK i_fn_s ->
563    (match i_fn_s.Types.snd with
564     | Joint.Sequential (s, x) ->
565       joint_classify_step
566         (Joint.uns_pars__o__u_pars
567           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
568     | Joint.Final s ->
569       joint_classify_final
570         (Joint.uns_pars__o__u_pars
571           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
572     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
573  | Errors.Error x -> StructuredTraces.Cl_other
574
575(** val joint_call_ident :
576    Joint_semantics.sem_params -> evaluation_params ->
577    Joint_semantics.state_pc -> AST.ident **)
578let joint_call_ident p pars st =
579  let dummy = Positive.One in
580  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
581           st.Joint_semantics.pc with
582   | Errors.OK x ->
583     (match x.Types.snd with
584      | Joint.Sequential (s, next) ->
585        (match s with
586         | Joint.COST_LABEL x0 -> dummy
587         | Joint.CALL (f', args, dest) ->
588           (match Obj.magic
589                    (Monad.m_bind0 (Monad.max_def Errors.res0)
590                      (Joint_semantics.block_of_call p pars.globals
591                        (let p0 = Joint_semantics.spp'__o__spp p in
592                        let globals0 = pars.globals in
593                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
594                        st.Joint_semantics.st_no_pc) (fun bl ->
595                      Obj.magic
596                        (Joint_semantics.fetch_internal_function pars.globals
597                          pars.ev_genv bl))) with
598            | Errors.OK i_f -> i_f.Types.fst
599            | Errors.Error x0 -> dummy)
600         | Joint.COND (x0, x1) -> dummy
601         | Joint.Step_seq x0 -> dummy)
602      | Joint.Final x0 -> dummy
603      | Joint.FCOND (x0, x1, x2) -> dummy)
604   | Errors.Error x -> dummy)
605
606(** val joint_tailcall_ident :
607    Joint_semantics.sem_params -> evaluation_params ->
608    Joint_semantics.state_pc -> AST.ident **)
609let joint_tailcall_ident p pars st =
610  let dummy = Positive.One in
611  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
612           st.Joint_semantics.pc with
613   | Errors.OK x ->
614     (match x.Types.snd with
615      | Joint.Sequential (x0, x1) -> dummy
616      | Joint.Final s ->
617        (match s with
618         | Joint.GOTO x0 -> dummy
619         | Joint.RETURN -> dummy
620         | Joint.TAILCALL (f', args) ->
621           (match Obj.magic
622                    (Monad.m_bind0 (Monad.max_def Errors.res0)
623                      (Joint_semantics.block_of_call p pars.globals
624                        (let p0 = Joint_semantics.spp'__o__spp p in
625                        let globals0 = pars.globals in
626                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
627                        st.Joint_semantics.st_no_pc) (fun bl ->
628                      Obj.magic
629                        (Joint_semantics.fetch_internal_function pars.globals
630                          pars.ev_genv bl))) with
631            | Errors.OK i_f -> i_f.Types.fst
632            | Errors.Error x0 -> dummy))
633      | Joint.FCOND (x0, x1, x2) -> dummy)
634   | Errors.Error x -> dummy)
635
636(** val pcDeq : Deqsets.deqSet **)
637let pcDeq =
638  Obj.magic ByteValues.eq_program_counter
639
640(** val cost_label_of_stmt :
641    Joint_semantics.sem_params -> evaluation_params -> Joint.joint_statement
642    -> CostLabel.costlabel Types.option **)
643let cost_label_of_stmt p pars = function
644| Joint.Sequential (s0, x) ->
645  (match s0 with
646   | Joint.COST_LABEL lbl -> Types.Some lbl
647   | Joint.CALL (x0, x1, x2) -> Types.None
648   | Joint.COND (x0, x1) -> Types.None
649   | Joint.Step_seq x0 -> Types.None)
650| Joint.Final x -> Types.None
651| Joint.FCOND (x0, x1, x2) -> Types.None
652
653(** val joint_label_of_pc :
654    Joint_semantics.sem_params -> evaluation_params ->
655    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
656let joint_label_of_pc p pars pc =
657  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
658  | Errors.OK fn_stmt -> cost_label_of_stmt p pars fn_stmt.Types.snd
659  | Errors.Error x -> Types.None
660
661(** val exit_pc' : ByteValues.program_counter **)
662let exit_pc' =
663  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
664    ByteValues.pc_offset = (Positive.P1 Positive.One) }
665
666(** val joint_final :
667    Joint_semantics.sem_params -> evaluation_params ->
668    Joint_semantics.state_pc -> Integers.int Types.option **)
669let joint_final p pars st =
670  let ge = pars.ev_genv in
671  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
672   | Bool.True ->
673     let ret =
674       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
675     in
676     Errors.res_to_opt
677       (Obj.magic
678         (Monad.m_bind0 (Monad.max_def Errors.res0)
679           (Obj.magic
680             (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
681               pars.globals
682               (let p0 = Joint_semantics.spp'__o__spp p in
683               let globals0 = pars.globals in
684               let g = ge in g.Joint_semantics.ge) ret
685               st.Joint_semantics.st_no_pc)) (fun vals ->
686           Obj.magic (ByteValues.word_of_list_beval vals))))
687   | Bool.False -> Types.None)
688
689(** val joint_abstract_status :
690    prog_params -> StructuredTraces.abstract_status **)
691let joint_abstract_status p =
692  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
693    (Obj.magic
694      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
695    StructuredTraces.as_classify =
696    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
697    StructuredTraces.as_label_of_pc =
698    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
699    StructuredTraces.as_result =
700    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
701    StructuredTraces.as_call_ident = (fun st ->
702    joint_call_ident p.prog_spars (joint_make_global p)
703      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
704    (fun st ->
705    joint_tailcall_ident p.prog_spars (joint_make_global p)
706      (Types.pi1 (Obj.magic st))) }
707
708(** val joint_status :
709    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
710    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
711let joint_status p prog0 stacksizes =
712  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
713    stacksizes }
714
Note: See TracBrowser for help on using the repository browser.