source: extracted/traces.ml @ 3069

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

New extraction

File size: 23.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_25115 =
160  let { globals = globals0; ev_genv = ev_genv0 } = x_25115 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_25117 =
167  let { globals = globals0; ev_genv = ev_genv0 } = x_25117 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_25119 =
174  let { globals = globals0; ev_genv = ev_genv0 } = x_25119 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_25121 =
181  let { globals = globals0; ev_genv = ev_genv0 } = x_25121 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_25123 =
188  let { globals = globals0; ev_genv = ev_genv0 } = x_25123 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_25125 =
195  let { globals = globals0; ev_genv = ev_genv0 } = x_25125 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__ge__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__ge__o__inject x0 x2 =
265  Joint_semantics.ge__o__inject x2.Types.dpi1.globals x2.Types.dpi1.ev_genv
266
267(** val dpi1__o__ev_genv__o__ge :
268    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
269    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
270let dpi1__o__ev_genv__o__ge x0 x2 =
271  x2.Types.dpi1.ev_genv.Joint_semantics.ge
272
273(** val eject__o__ev_genv__o__inject :
274    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
275    Joint_semantics.genv Types.sig0 **)
276let eject__o__ev_genv__o__inject x0 x2 =
277  (Types.pi1 x2).ev_genv
278
279(** val eject__o__ev_genv__o__ge__o__inject :
280    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
281    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
282    Types.sig0 **)
283let eject__o__ev_genv__o__ge__o__inject x0 x2 =
284  Joint_semantics.ge__o__inject (Types.pi1 x2).globals (Types.pi1 x2).ev_genv
285
286(** val eject__o__ev_genv__o__ge :
287    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
288    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
289let eject__o__ev_genv__o__ge x0 x2 =
290  (Types.pi1 x2).ev_genv.Joint_semantics.ge
291
292(** val ev_genv__o__ge :
293    Joint_semantics.sem_params -> evaluation_params ->
294    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
295let ev_genv__o__ge x0 x1 =
296  x1.ev_genv.Joint_semantics.ge
297
298(** val ev_genv__o__ge__o__inject :
299    Joint_semantics.sem_params -> evaluation_params ->
300    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
301    Types.sig0 **)
302let ev_genv__o__ge__o__inject x0 x1 =
303  Joint_semantics.ge__o__inject x1.globals x1.ev_genv
304
305(** val ev_genv__o__inject :
306    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
307    Types.sig0 **)
308let ev_genv__o__inject x0 x1 =
309  x1.ev_genv
310
311(** val dpi1__o__ev_genv :
312    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
313    Joint_semantics.genv **)
314let dpi1__o__ev_genv x0 x2 =
315  x2.Types.dpi1.ev_genv
316
317(** val eject__o__ev_genv :
318    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
319    Joint_semantics.genv **)
320let eject__o__ev_genv x0 x2 =
321  (Types.pi1 x2).ev_genv
322
323type prog_params = { prog_spars : Joint_semantics.sem_params;
324                     prog : Joint.joint_program;
325                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
326
327(** val prog_params_rect_Type4 :
328    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
329    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
330let rec prog_params_rect_Type4 h_mk_prog_params x_25141 =
331  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
332    stack_sizes0 } = x_25141
333  in
334  h_mk_prog_params prog_spars0 prog0 stack_sizes0
335
336(** val prog_params_rect_Type5 :
337    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
338    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
339let rec prog_params_rect_Type5 h_mk_prog_params x_25143 =
340  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
341    stack_sizes0 } = x_25143
342  in
343  h_mk_prog_params prog_spars0 prog0 stack_sizes0
344
345(** val prog_params_rect_Type3 :
346    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
347    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
348let rec prog_params_rect_Type3 h_mk_prog_params x_25145 =
349  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
350    stack_sizes0 } = x_25145
351  in
352  h_mk_prog_params prog_spars0 prog0 stack_sizes0
353
354(** val prog_params_rect_Type2 :
355    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
356    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
357let rec prog_params_rect_Type2 h_mk_prog_params x_25147 =
358  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
359    stack_sizes0 } = x_25147
360  in
361  h_mk_prog_params prog_spars0 prog0 stack_sizes0
362
363(** val prog_params_rect_Type1 :
364    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
365    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
366let rec prog_params_rect_Type1 h_mk_prog_params x_25149 =
367  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
368    stack_sizes0 } = x_25149
369  in
370  h_mk_prog_params prog_spars0 prog0 stack_sizes0
371
372(** val prog_params_rect_Type0 :
373    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
374    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
375let rec prog_params_rect_Type0 h_mk_prog_params x_25151 =
376  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
377    stack_sizes0 } = x_25151
378  in
379  h_mk_prog_params prog_spars0 prog0 stack_sizes0
380
381(** val prog_spars : prog_params -> Joint_semantics.sem_params **)
382let rec prog_spars xxx =
383  xxx.prog_spars
384
385(** val prog : prog_params -> Joint.joint_program **)
386let rec prog xxx =
387  xxx.prog
388
389(** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
390let rec stack_sizes xxx =
391  xxx.stack_sizes
392
393(** val prog_params_inv_rect_Type4 :
394    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
395    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
396let prog_params_inv_rect_Type4 hterm h1 =
397  let hcut = prog_params_rect_Type4 h1 hterm in hcut __
398
399(** val prog_params_inv_rect_Type3 :
400    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
401    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
402let prog_params_inv_rect_Type3 hterm h1 =
403  let hcut = prog_params_rect_Type3 h1 hterm in hcut __
404
405(** val prog_params_inv_rect_Type2 :
406    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
407    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
408let prog_params_inv_rect_Type2 hterm h1 =
409  let hcut = prog_params_rect_Type2 h1 hterm in hcut __
410
411(** val prog_params_inv_rect_Type1 :
412    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
413    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
414let prog_params_inv_rect_Type1 hterm h1 =
415  let hcut = prog_params_rect_Type1 h1 hterm in hcut __
416
417(** val prog_params_inv_rect_Type0 :
418    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
419    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
420let prog_params_inv_rect_Type0 hterm h1 =
421  let hcut = prog_params_rect_Type0 h1 hterm in hcut __
422
423(** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
424let prog_params_jmdiscr x y =
425  Logic.eq_rect_Type2 x
426    (let { prog_spars = a0; prog = a1; stack_sizes = a2 } = x in
427    Obj.magic (fun _ dH -> dH __ __ __)) y
428
429(** val prog_spars__o__spp' :
430    prog_params -> Joint_semantics.serialized_params **)
431let prog_spars__o__spp' x0 =
432  x0.prog_spars.Joint_semantics.spp'
433
434(** val prog_spars__o__spp'__o__msu_pars :
435    prog_params -> Joint.joint_closed_internal_function
436    Joint_semantics.sem_unserialized_params **)
437let prog_spars__o__spp'__o__msu_pars x0 =
438  Joint_semantics.spp'__o__msu_pars x0.prog_spars
439
440(** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
441    prog_params -> Joint_semantics.sem_state_params **)
442let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 =
443  Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars
444
445(** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **)
446let prog_spars__o__spp'__o__spp x0 =
447  Joint_semantics.spp'__o__spp x0.prog_spars
448
449(** val prog_spars__o__spp'__o__spp__o__stmt_pars :
450    prog_params -> Joint.stmt_params **)
451let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
452  Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars
453
454(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
455    prog_params -> Joint.uns_params **)
456let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
457  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars
458
459(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
460    prog_params -> Joint.unserialized_params **)
461let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
462  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
463    x0.prog_spars
464
465(** val joint_make_global : prog_params -> evaluation_params **)
466let joint_make_global p =
467  { globals =
468    (Joint.prog_names (Joint_semantics.spp'__o__spp p.prog_spars) p.prog);
469    ev_genv =
470    (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }
471
472(** val joint_make_global__o__ev_genv :
473    prog_params -> Joint_semantics.genv **)
474let joint_make_global__o__ev_genv x0 =
475  (joint_make_global x0).ev_genv
476
477(** val joint_make_global__o__ev_genv__o__ge :
478    prog_params -> Joint.joint_closed_internal_function AST.fundef
479    Globalenvs.genv_t **)
480let joint_make_global__o__ev_genv__o__ge x0 =
481  ev_genv__o__ge x0.prog_spars (joint_make_global x0)
482
483(** val joint_make_global__o__ev_genv__o__ge__o__inject :
484    prog_params -> Joint.joint_closed_internal_function AST.fundef
485    Globalenvs.genv_t Types.sig0 **)
486let joint_make_global__o__ev_genv__o__ge__o__inject x0 =
487  ev_genv__o__ge__o__inject x0.prog_spars (joint_make_global x0)
488
489(** val joint_make_global__o__ev_genv__o__inject :
490    prog_params -> Joint_semantics.genv Types.sig0 **)
491let joint_make_global__o__ev_genv__o__inject x0 =
492  ev_genv__o__inject x0.prog_spars (joint_make_global x0)
493
494(** val joint_make_global__o__inject :
495    prog_params -> evaluation_params Types.sig0 **)
496let joint_make_global__o__inject x0 =
497  joint_make_global x0
498
499(** val make_initial_state :
500    prog_params -> Joint_semantics.state_pc Errors.res **)
501let make_initial_state pars =
502  let p = pars.prog in
503  let ge = ev_genv pars.prog_spars in
504  Obj.magic
505    (Monad.m_bind0 (Monad.max_def Errors.res0)
506      (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
507      (fun m0 ->
508      (let { Types.fst = m; Types.snd = spb } =
509         GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
510       in
511      (fun _ ->
512      let globals_size =
513        Joint.globals_stacksize
514          (Joint_semantics.spp'__o__spp pars.prog_spars) p
515      in
516      let spp = { Pointers.pblock = spb; Pointers.poff =
517        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
519          (Nat.S Nat.O))))))))))))))))
520          (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
521      in
522      let main = p.Joint.joint_prog.AST.prog_main in
523      let st = { Joint_semantics.st_frms = (Types.Some
524        (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
525        Joint_semantics.istack = Joint_semantics.Empty_is;
526        Joint_semantics.carry = (ByteValues.BBbit Bool.False);
527        Joint_semantics.regs =
528        ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
529          spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
530        globals_size }
531      in
532      Monad.m_return0 (Monad.max_def Errors.res0)
533        { Joint_semantics.st_no_pc =
534        (Joint_semantics.set_sp
535          (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
536        Joint_semantics.pc = Joint_semantics.init_pc;
537        Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
538        __))
539
540(** val joint_classify_step :
541    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
542    StructuredTraces.status_class **)
543let joint_classify_step p g = function
544| Joint.COST_LABEL x -> StructuredTraces.Cl_other
545| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
546| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
547| Joint.Step_seq x -> StructuredTraces.Cl_other
548
549(** val joint_classify_final :
550    Joint.unserialized_params -> Joint.joint_fin_step ->
551    StructuredTraces.status_class **)
552let joint_classify_final p = function
553| Joint.GOTO x -> StructuredTraces.Cl_other
554| Joint.RETURN -> StructuredTraces.Cl_return
555| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall
556
557(** val joint_classify :
558    Joint_semantics.sem_params -> evaluation_params ->
559    Joint_semantics.state_pc -> StructuredTraces.status_class **)
560let joint_classify p pars st =
561  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
562          st.Joint_semantics.pc with
563  | Errors.OK i_fn_s ->
564    (match i_fn_s.Types.snd with
565     | Joint.Sequential (s, x) ->
566       joint_classify_step
567         (Joint.uns_pars__o__u_pars
568           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
569     | Joint.Final s ->
570       joint_classify_final
571         (Joint.uns_pars__o__u_pars
572           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
573     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
574  | Errors.Error x -> StructuredTraces.Cl_other
575
576(** val joint_call_ident :
577    Joint_semantics.sem_params -> evaluation_params ->
578    Joint_semantics.state_pc -> AST.ident **)
579let joint_call_ident p pars st =
580  let dummy = Positive.One in
581  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
582           st.Joint_semantics.pc with
583   | Errors.OK x ->
584     (match x.Types.snd with
585      | Joint.Sequential (s, next) ->
586        (match s with
587         | Joint.COST_LABEL x0 -> dummy
588         | Joint.CALL (f', args, dest) ->
589           (match Obj.magic
590                    (Monad.m_bind0 (Monad.max_def Errors.res0)
591                      (Joint_semantics.block_of_call p pars.globals
592                        pars.ev_genv f' st.Joint_semantics.st_no_pc)
593                      (fun bl ->
594                      Obj.magic
595                        (Joint_semantics.fetch_internal_function pars.globals
596                          pars.ev_genv bl))) with
597            | Errors.OK i_f -> i_f.Types.fst
598            | Errors.Error x0 -> dummy)
599         | Joint.COND (x0, x1) -> dummy
600         | Joint.Step_seq x0 -> dummy)
601      | Joint.Final x0 -> dummy
602      | Joint.FCOND (x0, x1, x2) -> dummy)
603   | Errors.Error x -> dummy)
604
605(** val joint_tailcall_ident :
606    Joint_semantics.sem_params -> evaluation_params ->
607    Joint_semantics.state_pc -> AST.ident **)
608let joint_tailcall_ident p pars st =
609  let dummy = Positive.One in
610  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
611           st.Joint_semantics.pc with
612   | Errors.OK x ->
613     (match x.Types.snd with
614      | Joint.Sequential (x0, x1) -> dummy
615      | Joint.Final s ->
616        (match s with
617         | Joint.GOTO x0 -> dummy
618         | Joint.RETURN -> dummy
619         | Joint.TAILCALL (f', args) ->
620           (match Obj.magic
621                    (Monad.m_bind0 (Monad.max_def Errors.res0)
622                      (Joint_semantics.block_of_call p pars.globals
623                        pars.ev_genv f' st.Joint_semantics.st_no_pc)
624                      (fun bl ->
625                      Obj.magic
626                        (Joint_semantics.fetch_internal_function pars.globals
627                          pars.ev_genv bl))) with
628            | Errors.OK i_f -> i_f.Types.fst
629            | Errors.Error x0 -> dummy))
630      | Joint.FCOND (x0, x1, x2) -> dummy)
631   | Errors.Error x -> dummy)
632
633(** val pcDeq : Deqsets.deqSet **)
634let pcDeq =
635  Obj.magic ByteValues.eq_program_counter
636
637(** val cost_label_of_stmt :
638    Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
639    CostLabel.costlabel Types.option **)
640let cost_label_of_stmt p g = function
641| Joint.Sequential (s0, x) ->
642  (match s0 with
643   | Joint.COST_LABEL lbl -> Types.Some lbl
644   | Joint.CALL (x0, x1, x2) -> Types.None
645   | Joint.COND (x0, x1) -> Types.None
646   | Joint.Step_seq x0 -> Types.None)
647| Joint.Final x -> Types.None
648| Joint.FCOND (x0, x1, x2) -> Types.None
649
650(** val joint_label_of_pc :
651    Joint_semantics.sem_params -> evaluation_params ->
652    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
653let joint_label_of_pc p pars pc =
654  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
655  | Errors.OK fn_stmt ->
656    cost_label_of_stmt (Joint_semantics.spp'__o__spp__o__stmt_pars p)
657      pars.globals fn_stmt.Types.snd
658  | Errors.Error x -> Types.None
659
660(** val exit_pc' : ByteValues.program_counter **)
661let exit_pc' =
662  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
663    ByteValues.pc_offset = (Positive.P1 Positive.One) }
664
665(** val joint_final :
666    Joint_semantics.sem_params -> evaluation_params ->
667    Joint_semantics.state_pc -> Integers.int Types.option **)
668let joint_final p pars st =
669  let ge = pars.ev_genv in
670  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
671   | Bool.True ->
672     let ret =
673       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
674     in
675     (match Obj.magic
676              (Monad.m_bind0 (Monad.max_def Errors.res0)
677                (Obj.magic
678                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
679                    pars.globals ge.Joint_semantics.ge ret
680                    st.Joint_semantics.st_no_pc)) (fun vals ->
681                Obj.magic (ByteValues.word_of_list_beval vals))) with
682      | Errors.OK v -> Types.Some v
683      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
684   | Bool.False -> Types.None)
685
686(** val joint_abstract_status :
687    prog_params -> StructuredTraces.abstract_status **)
688let joint_abstract_status p =
689  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
690    (Obj.magic
691      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
692    StructuredTraces.as_classify =
693    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
694    StructuredTraces.as_label_of_pc =
695    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
696    StructuredTraces.as_result =
697    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
698    StructuredTraces.as_call_ident = (fun st ->
699    joint_call_ident p.prog_spars (joint_make_global p)
700      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
701    (fun st ->
702    joint_tailcall_ident p.prog_spars (joint_make_global p)
703      (Types.pi1 (Obj.magic st))) }
704
705(** val joint_status :
706    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
707    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
708let joint_status p prog0 stacksizes =
709  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
710    stacksizes }
711
Note: See TracBrowser for help on using the repository browser.