source: extracted/traces.ml @ 3001

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

New extraction.

File size: 24.6 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_15969 =
160  let { globals = globals0; ev_genv = ev_genv0 } = x_15969 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_15971 =
167  let { globals = globals0; ev_genv = ev_genv0 } = x_15971 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_15973 =
174  let { globals = globals0; ev_genv = ev_genv0 } = x_15973 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_15975 =
181  let { globals = globals0; ev_genv = ev_genv0 } = x_15975 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_15977 =
188  let { globals = globals0; ev_genv = ev_genv0 } = x_15977 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_15979 =
195  let { globals = globals0; ev_genv = ev_genv0 } = x_15979 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_15995 =
339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
340    stack_sizes0 } = x_15995
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_15997 =
348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
349    stack_sizes0 } = x_15997
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_15999 =
357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
358    stack_sizes0 } = x_15999
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_16001 =
366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
367    stack_sizes0 } = x_16001
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_16003 =
375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
376    stack_sizes0 } = x_16003
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_16005 =
384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
385    stack_sizes0 } = x_16005
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 :
506    prog_params -> Joint_semantics.state_pc Errors.res **)
507let make_initial_state pars =
508  let p = pars.prog in
509  let ge = ev_genv pars.prog_spars in
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
525          (Nat.S Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
526      in
527      let main = AST.prog_main p.Joint.joint_prog in
528      let st = { Joint_semantics.st_frms = (Types.Some
529        (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
530        Joint_semantics.istack = Joint_semantics.Empty_is;
531        Joint_semantics.carry = (ByteValues.BBbit Bool.False);
532        Joint_semantics.regs =
533        ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
534          spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
535        globals_size }
536      in
537      Monad.m_return0 (Monad.max_def Errors.res0)
538        { Joint_semantics.st_no_pc =
539        (Joint_semantics.set_sp
540          (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
541        Joint_semantics.pc = Joint_semantics.init_pc;
542        Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
543        __))
544
545(** val joint_classify_step :
546    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
547    StructuredTraces.status_class **)
548let joint_classify_step p g = function
549| Joint.COST_LABEL x -> StructuredTraces.Cl_other
550| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
551| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
552| Joint.Step_seq x -> StructuredTraces.Cl_other
553
554(** val joint_classify_final :
555    Joint.unserialized_params -> Joint.joint_fin_step ->
556    StructuredTraces.status_class **)
557let joint_classify_final p = function
558| Joint.GOTO x -> StructuredTraces.Cl_other
559| Joint.RETURN -> StructuredTraces.Cl_return
560| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall
561
562(** val joint_classify :
563    Joint_semantics.sem_params -> evaluation_params ->
564    Joint_semantics.state_pc -> StructuredTraces.status_class **)
565let joint_classify p pars st =
566  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
567          st.Joint_semantics.pc with
568  | Errors.OK i_fn_s ->
569    (match i_fn_s.Types.snd with
570     | Joint.Sequential (s, x) ->
571       joint_classify_step
572         (Joint.uns_pars__o__u_pars
573           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
574     | Joint.Final s ->
575       joint_classify_final
576         (Joint.uns_pars__o__u_pars
577           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
578     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
579  | Errors.Error x -> StructuredTraces.Cl_other
580
581(** val joint_call_ident :
582    Joint_semantics.sem_params -> evaluation_params ->
583    Joint_semantics.state_pc -> AST.ident **)
584let joint_call_ident p pars st =
585  let dummy = Positive.One in
586  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
587           st.Joint_semantics.pc with
588   | Errors.OK x ->
589     (match x.Types.snd with
590      | Joint.Sequential (s, next) ->
591        (match s with
592         | Joint.COST_LABEL x0 -> dummy
593         | Joint.CALL (f', args, dest) ->
594           (match Obj.magic
595                    (Monad.m_bind0 (Monad.max_def Errors.res0)
596                      (Joint_semantics.block_of_call p pars.globals
597                        (let p0 = Joint_semantics.spp'__o__spp p in
598                        let globals0 = pars.globals in
599                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
600                        st.Joint_semantics.st_no_pc) (fun bl ->
601                      Obj.magic
602                        (Joint_semantics.fetch_internal_function pars.globals
603                          pars.ev_genv bl))) with
604            | Errors.OK i_f -> i_f.Types.fst
605            | Errors.Error x0 -> dummy)
606         | Joint.COND (x0, x1) -> dummy
607         | Joint.Step_seq x0 -> dummy)
608      | Joint.Final x0 -> dummy
609      | Joint.FCOND (x0, x1, x2) -> dummy)
610   | Errors.Error x -> dummy)
611
612(** val joint_tailcall_ident :
613    Joint_semantics.sem_params -> evaluation_params ->
614    Joint_semantics.state_pc -> AST.ident **)
615let joint_tailcall_ident p pars st =
616  let dummy = Positive.One in
617  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
618           st.Joint_semantics.pc with
619   | Errors.OK x ->
620     (match x.Types.snd with
621      | Joint.Sequential (x0, x1) -> dummy
622      | Joint.Final s ->
623        (match s with
624         | Joint.GOTO x0 -> dummy
625         | Joint.RETURN -> dummy
626         | Joint.TAILCALL (f', args) ->
627           (match Obj.magic
628                    (Monad.m_bind0 (Monad.max_def Errors.res0)
629                      (Joint_semantics.block_of_call p pars.globals
630                        (let p0 = Joint_semantics.spp'__o__spp p in
631                        let globals0 = pars.globals in
632                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
633                        st.Joint_semantics.st_no_pc) (fun bl ->
634                      Obj.magic
635                        (Joint_semantics.fetch_internal_function pars.globals
636                          pars.ev_genv bl))) with
637            | Errors.OK i_f -> i_f.Types.fst
638            | Errors.Error x0 -> dummy))
639      | Joint.FCOND (x0, x1, x2) -> dummy)
640   | Errors.Error x -> dummy)
641
642(** val pcDeq : Deqsets.deqSet **)
643let pcDeq =
644  Obj.magic ByteValues.eq_program_counter
645
646(** val cost_label_of_stmt :
647    Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
648    CostLabel.costlabel Types.option **)
649let cost_label_of_stmt p g = function
650| Joint.Sequential (s0, x) ->
651  (match s0 with
652   | Joint.COST_LABEL lbl -> Types.Some lbl
653   | Joint.CALL (x0, x1, x2) -> Types.None
654   | Joint.COND (x0, x1) -> Types.None
655   | Joint.Step_seq x0 -> Types.None)
656| Joint.Final x -> Types.None
657| Joint.FCOND (x0, x1, x2) -> Types.None
658
659(** val joint_label_of_pc :
660    Joint_semantics.sem_params -> evaluation_params ->
661    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
662let joint_label_of_pc p pars pc =
663  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
664  | Errors.OK fn_stmt ->
665    cost_label_of_stmt (Joint_semantics.spp'__o__spp__o__stmt_pars p)
666      pars.globals fn_stmt.Types.snd
667  | Errors.Error x -> Types.None
668
669(** val exit_pc' : ByteValues.program_counter **)
670let exit_pc' =
671  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
672    ByteValues.pc_offset = (Positive.P1 Positive.One) }
673
674(** val joint_final :
675    Joint_semantics.sem_params -> evaluation_params ->
676    Joint_semantics.state_pc -> Integers.int Types.option **)
677let joint_final p pars st =
678  let ge = pars.ev_genv in
679  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
680   | Bool.True ->
681     let ret =
682       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
683     in
684     (match Obj.magic
685              (Monad.m_bind0 (Monad.max_def Errors.res0)
686                (Obj.magic
687                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
688                    pars.globals
689                    (let p0 = Joint_semantics.spp'__o__spp p in
690                    let globals0 = pars.globals in
691                    let g = ge in g.Joint_semantics.ge) ret
692                    st.Joint_semantics.st_no_pc)) (fun vals ->
693                Obj.magic (ByteValues.word_of_list_beval vals))) with
694      | Errors.OK v -> Types.Some v
695      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
696   | Bool.False -> Types.None)
697
698(** val joint_abstract_status :
699    prog_params -> StructuredTraces.abstract_status **)
700let joint_abstract_status p =
701  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
702    (Obj.magic
703      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
704    StructuredTraces.as_classify =
705    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
706    StructuredTraces.as_label_of_pc =
707    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
708    StructuredTraces.as_result =
709    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
710    StructuredTraces.as_call_ident = (fun st ->
711    joint_call_ident p.prog_spars (joint_make_global p)
712      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
713    (fun st ->
714    joint_tailcall_ident p.prog_spars (joint_make_global p)
715      (Types.pi1 (Obj.magic st))) }
716
717(** val joint_status :
718    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
719    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
720let joint_status p prog0 stacksizes =
721  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
722    stacksizes }
723
Note: See TracBrowser for help on using the repository browser.