source: extracted/traces.ml @ 2890

Last change on this file since 2890 was 2890, checked in by sacerdot, 6 years ago

Exported again, now the execution is correct up to LIN for a simple program.

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