source: extracted/traces.ml @ 2933

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

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 22.8 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_3 =
145  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_3 in
146  h_mk_evaluation_params globals0 sparams0 ev_genv0
147
148(** val evaluation_params_rect_Type5 :
149    (AST.ident List.list -> Joint_semantics.sem_params ->
150    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
151let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_5 =
152  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5 in
153  h_mk_evaluation_params globals0 sparams0 ev_genv0
154
155(** val evaluation_params_rect_Type3 :
156    (AST.ident List.list -> Joint_semantics.sem_params ->
157    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
158let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_7 =
159  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_7 in
160  h_mk_evaluation_params globals0 sparams0 ev_genv0
161
162(** val evaluation_params_rect_Type2 :
163    (AST.ident List.list -> Joint_semantics.sem_params ->
164    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
165let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_9 =
166  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_9 in
167  h_mk_evaluation_params globals0 sparams0 ev_genv0
168
169(** val evaluation_params_rect_Type1 :
170    (AST.ident List.list -> Joint_semantics.sem_params ->
171    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
172let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_11 =
173  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_11
174  in
175  h_mk_evaluation_params globals0 sparams0 ev_genv0
176
177(** val evaluation_params_rect_Type0 :
178    (AST.ident List.list -> Joint_semantics.sem_params ->
179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
180let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_13 =
181  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_13
182  in
183  h_mk_evaluation_params globals0 sparams0 ev_genv0
184
185(** val globals : evaluation_params -> AST.ident List.list **)
186let rec globals xxx =
187  xxx.globals
188
189(** val sparams : evaluation_params -> Joint_semantics.sem_params **)
190let rec sparams xxx =
191  xxx.sparams
192
193(** val ev_genv : evaluation_params -> Joint_semantics.genv **)
194let rec ev_genv xxx =
195  xxx.ev_genv
196
197(** val evaluation_params_inv_rect_Type4 :
198    evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
199    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
200let evaluation_params_inv_rect_Type4 hterm h1 =
201  let hcut = evaluation_params_rect_Type4 h1 hterm in hcut __
202
203(** val evaluation_params_inv_rect_Type3 :
204    evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
205    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
206let evaluation_params_inv_rect_Type3 hterm h1 =
207  let hcut = evaluation_params_rect_Type3 h1 hterm in hcut __
208
209(** val evaluation_params_inv_rect_Type2 :
210    evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
211    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
212let evaluation_params_inv_rect_Type2 hterm h1 =
213  let hcut = evaluation_params_rect_Type2 h1 hterm in hcut __
214
215(** val evaluation_params_inv_rect_Type1 :
216    evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
217    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
218let evaluation_params_inv_rect_Type1 hterm h1 =
219  let hcut = evaluation_params_rect_Type1 h1 hterm in hcut __
220
221(** val evaluation_params_inv_rect_Type0 :
222    evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
223    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
224let evaluation_params_inv_rect_Type0 hterm h1 =
225  let hcut = evaluation_params_rect_Type0 h1 hterm in hcut __
226
227(** val evaluation_params_jmdiscr :
228    evaluation_params -> evaluation_params -> __ **)
229let evaluation_params_jmdiscr x y =
230  Logic.eq_rect_Type2 x
231    (let { globals = a0; sparams = a1; ev_genv = a2 } = x in
232    Obj.magic (fun _ dH -> dH __ __ __)) y
233
234(** val sparams__o__msu_pars :
235    evaluation_params -> Joint.joint_closed_internal_function
236    Joint_semantics.sem_unserialized_params **)
237let sparams__o__msu_pars x0 =
238  x0.sparams.Joint_semantics.msu_pars
239
240(** val sparams__o__msu_pars__o__st_pars :
241    evaluation_params -> Joint_semantics.sem_state_params **)
242let sparams__o__msu_pars__o__st_pars x0 =
243  Joint_semantics.msu_pars__o__st_pars x0.sparams
244
245(** val sparams__o__spp : evaluation_params -> Joint.params **)
246let sparams__o__spp x0 =
247  x0.sparams.Joint_semantics.spp
248
249(** val sparams__o__spp__o__stmt_pars :
250    evaluation_params -> Joint.stmt_params **)
251let sparams__o__spp__o__stmt_pars x0 =
252  Joint_semantics.spp__o__stmt_pars x0.sparams
253
254(** val sparams__o__spp__o__stmt_pars__o__uns_pars :
255    evaluation_params -> Joint.uns_params **)
256let sparams__o__spp__o__stmt_pars__o__uns_pars x0 =
257  Joint_semantics.spp__o__stmt_pars__o__uns_pars x0.sparams
258
259(** val sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
260    evaluation_params -> Joint.unserialized_params **)
261let sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
262  Joint_semantics.spp__o__stmt_pars__o__uns_pars__o__u_pars x0.sparams
263
264type prog_params = { prog_spars : Joint_semantics.sem_params;
265                     prog : Joint.joint_program;
266                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
267
268(** val prog_params_rect_Type4 :
269    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
270    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
271let rec prog_params_rect_Type4 h_mk_prog_params x_29 =
272  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
273    stack_sizes0 } = x_29
274  in
275  h_mk_prog_params prog_spars0 prog0 stack_sizes0
276
277(** val prog_params_rect_Type5 :
278    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
279    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
280let rec prog_params_rect_Type5 h_mk_prog_params x_31 =
281  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
282    stack_sizes0 } = x_31
283  in
284  h_mk_prog_params prog_spars0 prog0 stack_sizes0
285
286(** val prog_params_rect_Type3 :
287    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
288    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
289let rec prog_params_rect_Type3 h_mk_prog_params x_33 =
290  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
291    stack_sizes0 } = x_33
292  in
293  h_mk_prog_params prog_spars0 prog0 stack_sizes0
294
295(** val prog_params_rect_Type2 :
296    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
297    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
298let rec prog_params_rect_Type2 h_mk_prog_params x_35 =
299  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
300    stack_sizes0 } = x_35
301  in
302  h_mk_prog_params prog_spars0 prog0 stack_sizes0
303
304(** val prog_params_rect_Type1 :
305    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
306    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
307let rec prog_params_rect_Type1 h_mk_prog_params x_37 =
308  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
309    stack_sizes0 } = x_37
310  in
311  h_mk_prog_params prog_spars0 prog0 stack_sizes0
312
313(** val prog_params_rect_Type0 :
314    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
315    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
316let rec prog_params_rect_Type0 h_mk_prog_params x_39 =
317  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
318    stack_sizes0 } = x_39
319  in
320  h_mk_prog_params prog_spars0 prog0 stack_sizes0
321
322(** val prog_spars : prog_params -> Joint_semantics.sem_params **)
323let rec prog_spars xxx =
324  xxx.prog_spars
325
326(** val prog : prog_params -> Joint.joint_program **)
327let rec prog xxx =
328  xxx.prog
329
330(** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
331let rec stack_sizes xxx =
332  xxx.stack_sizes
333
334(** val prog_params_inv_rect_Type4 :
335    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
336    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
337let prog_params_inv_rect_Type4 hterm h1 =
338  let hcut = prog_params_rect_Type4 h1 hterm in hcut __
339
340(** val prog_params_inv_rect_Type3 :
341    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
342    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
343let prog_params_inv_rect_Type3 hterm h1 =
344  let hcut = prog_params_rect_Type3 h1 hterm in hcut __
345
346(** val prog_params_inv_rect_Type2 :
347    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
348    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
349let prog_params_inv_rect_Type2 hterm h1 =
350  let hcut = prog_params_rect_Type2 h1 hterm in hcut __
351
352(** val prog_params_inv_rect_Type1 :
353    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
354    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
355let prog_params_inv_rect_Type1 hterm h1 =
356  let hcut = prog_params_rect_Type1 h1 hterm in hcut __
357
358(** val prog_params_inv_rect_Type0 :
359    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
360    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
361let prog_params_inv_rect_Type0 hterm h1 =
362  let hcut = prog_params_rect_Type0 h1 hterm in hcut __
363
364(** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
365let prog_params_jmdiscr x y =
366  Logic.eq_rect_Type2 x
367    (let { prog_spars = a0; prog = a1; stack_sizes = a2 } = x in
368    Obj.magic (fun _ dH -> dH __ __ __)) y
369
370(** val make_global : prog_params -> evaluation_params **)
371let make_global pars =
372  let p = pars.prog in
373  let spars = pars.prog_spars in
374  let genv = Globalenvs.globalenv_noinit p in
375  let get_pc_lbl = fun id lbl ->
376    Monad.m_bind0 (Monad.max_def Errors.res0)
377      (Obj.magic
378        (Joint_semantics.block_of_funct_id
379          (Joint_semantics.msu_pars__o__st_pars spars) genv id)) (fun bl ->
380      Obj.magic
381        (Joint_semantics.pc_of_label pars.prog_spars (AST.prog_var_names p)
382          genv bl lbl))
383  in
384  { globals = (AST.prog_var_names p); sparams = spars; ev_genv =
385  { Joint_semantics.ge = genv; Joint_semantics.stack_sizes =
386  pars.stack_sizes; Joint_semantics.get_pc_from_label =
387  (Obj.magic get_pc_lbl) } }
388
389(** val prog_params_to_ev_params__o__sparams :
390    prog_params -> Joint_semantics.sem_params **)
391let prog_params_to_ev_params__o__sparams x0 =
392  (make_global x0).sparams
393
394(** val prog_params_to_ev_params__o__sparams__o__msu_pars :
395    prog_params -> Joint.joint_closed_internal_function
396    Joint_semantics.sem_unserialized_params **)
397let prog_params_to_ev_params__o__sparams__o__msu_pars x0 =
398  sparams__o__msu_pars (make_global x0)
399
400(** val prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars :
401    prog_params -> Joint_semantics.sem_state_params **)
402let prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars x0 =
403  sparams__o__msu_pars__o__st_pars (make_global x0)
404
405(** val prog_params_to_ev_params__o__sparams__o__spp :
406    prog_params -> Joint.params **)
407let prog_params_to_ev_params__o__sparams__o__spp x0 =
408  sparams__o__spp (make_global x0)
409
410(** val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars :
411    prog_params -> Joint.stmt_params **)
412let prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars x0 =
413  sparams__o__spp__o__stmt_pars (make_global x0)
414
415(** val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
416    prog_params -> Joint.uns_params **)
417let prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars x0 =
418  sparams__o__spp__o__stmt_pars__o__uns_pars (make_global x0)
419
420(** val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
421    prog_params -> Joint.unserialized_params **)
422let prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
423  sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars (make_global x0)
424
425(** val make_initial_state :
426    prog_params -> Joint_semantics.state_pc Errors.res **)
427let make_initial_state pars =
428  let p = pars.prog in
429  let sem_globals = make_global pars in
430  let ge = sem_globals.ev_genv in
431  let m0 = Globalenvs.alloc_mem p in
432  (let { Types.fst = m; Types.snd = spb } =
433     GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
434   in
435  (fun _ ->
436  let globals_size =
437    Joint.globals_stacksize pars.prog_spars.Joint_semantics.spp p
438  in
439  let spp = { Pointers.pblock = spb; Pointers.poff =
440    (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442      Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
443  in
444  let main = p.AST.prog_main in
445  let st0 = { Joint_semantics.st_frms = (Types.Some
446    (prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
447    Joint_semantics.istack = Joint_semantics.Empty_is;
448    Joint_semantics.carry = (ByteValues.BBbit Bool.False);
449    Joint_semantics.regs =
450    ((prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
451      spp); Joint_semantics.m = m }
452  in
453  let st0' = { Joint_semantics.st_no_pc =
454    (Joint_semantics.set_sp
455      (prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars pars)
456      spp st0); Joint_semantics.pc = Joint_semantics.exit_pc;
457    Joint_semantics.last_pop = Joint_semantics.exit_pc }
458  in
459  Obj.magic
460    (Monad.m_bind0 (Monad.max_def Errors.res0)
461      (Obj.magic
462        ((sparams__o__msu_pars sem_globals).Joint_semantics.save_frame
463          Joint_semantics.ID
464          (prog_params_to_ev_params__o__sparams__o__msu_pars pars).Joint_semantics.call_dest_for_main
465          st0')) (fun st0_no_pc ->
466      let st0'' =
467        Joint_semantics.set_no_pc
468          (sparams__o__msu_pars sem_globals).Joint_semantics.st_pars
469          st0_no_pc st0'
470      in
471      Monad.m_bind0 (Monad.max_def Errors.res0)
472        (Joint_semantics.block_of_call sem_globals.sparams
473          sem_globals.globals
474          (let p0 = sem_globals.sparams.Joint_semantics.spp in
475          let globals0 = sem_globals.globals in
476          let g = ge in g.Joint_semantics.ge) (Types.Inl main)
477          st0''.Joint_semantics.st_no_pc) (fun bl ->
478        Monad.m_bind2 (Monad.max_def Errors.res0)
479          (Obj.magic
480            (Joint_semantics.fetch_function
481              (let p0 = sem_globals.sparams.Joint_semantics.spp in
482              let globals0 = sem_globals.globals in
483              let g = ge in g.Joint_semantics.ge) bl)) (fun i fn ->
484          match fn with
485          | AST.Internal ifn ->
486            Monad.m_bind0 (Monad.max_def Errors.res0)
487              (Joint_semantics.eval_internal_call sem_globals.sparams
488                sem_globals.globals ge i (Types.pi1 ifn)
489                (prog_params_to_ev_params__o__sparams__o__msu_pars pars).Joint_semantics.call_args_for_main
490                st0''.Joint_semantics.st_no_pc) (fun st' ->
491              let pc' =
492                Joint_semantics.pc_of_point sem_globals.sparams bl
493                  (Types.pi1 ifn).Joint.joint_if_entry
494              in
495              Monad.m_return0 (Monad.max_def Errors.res0)
496                { Joint_semantics.st_no_pc = st'; Joint_semantics.pc = pc';
497                Joint_semantics.last_pop = Joint_semantics.exit_pc })
498          | AST.External x ->
499            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
500              ErrorMessages.BadMain), (List.Cons ((Errors.CTX
501              (PreIdentifiers.SymbolTag, main)), List.Nil))))))))))) __
502
503(** val joint_classify_step :
504    evaluation_params -> Joint.joint_step -> StructuredTraces.status_class **)
505let joint_classify_step p = function
506| Joint.COST_LABEL x -> StructuredTraces.Cl_other
507| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
508| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
509| Joint.Step_seq x -> StructuredTraces.Cl_other
510
511(** val joint_classify_final :
512    evaluation_params -> Joint.joint_fin_step ->
513    StructuredTraces.status_class **)
514let joint_classify_final p = function
515| Joint.GOTO x -> StructuredTraces.Cl_other
516| Joint.RETURN -> StructuredTraces.Cl_return
517| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall
518
519(** val joint_classify :
520    evaluation_params -> Joint_semantics.state_pc ->
521    StructuredTraces.status_class **)
522let joint_classify p st =
523  match Joint_semantics.fetch_statement p.sparams p.globals
524          (let p0 = p.sparams.Joint_semantics.spp in
525          let globals0 = p.globals in
526          let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with
527  | Errors.OK i_fn_s ->
528    (match i_fn_s.Types.snd with
529     | Joint.Sequential (s, x) -> joint_classify_step p s
530     | Joint.Final s -> joint_classify_final p s
531     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
532  | Errors.Error x -> StructuredTraces.Cl_other
533
534(** val joint_call_ident :
535    evaluation_params -> Joint_semantics.state_pc -> AST.ident **)
536let joint_call_ident p st =
537  let dummy = Positive.One in
538  (match Joint_semantics.fetch_statement p.sparams p.globals
539           (let p0 = p.sparams.Joint_semantics.spp in
540           let globals0 = p.globals in
541           let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with
542   | Errors.OK x ->
543     (match x.Types.snd with
544      | Joint.Sequential (s, next) ->
545        (match s with
546         | Joint.COST_LABEL x0 -> dummy
547         | Joint.CALL (f', args, dest) ->
548           (match Obj.magic
549                    (Monad.m_bind0 (Monad.max_def Errors.res0)
550                      (Joint_semantics.block_of_call p.sparams p.globals
551                        (let p0 = p.sparams.Joint_semantics.spp in
552                        let globals0 = p.globals in
553                        let g = p.ev_genv in g.Joint_semantics.ge) f'
554                        st.Joint_semantics.st_no_pc) (fun bl ->
555                      Obj.magic
556                        (Joint_semantics.fetch_internal_function
557                          (let p0 = p.sparams.Joint_semantics.spp in
558                          let globals0 = p.globals in
559                          let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
560            | Errors.OK i_f -> i_f.Types.fst
561            | Errors.Error x0 -> dummy)
562         | Joint.COND (x0, x1) -> dummy
563         | Joint.Step_seq x0 -> dummy)
564      | Joint.Final x0 -> dummy
565      | Joint.FCOND (x0, x1, x2) -> dummy)
566   | Errors.Error x -> dummy)
567
568(** val joint_tailcall_ident :
569    evaluation_params -> Joint_semantics.state_pc -> AST.ident **)
570let joint_tailcall_ident p st =
571  let dummy = Positive.One in
572  (match Joint_semantics.fetch_statement p.sparams p.globals
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) st.Joint_semantics.pc with
576   | Errors.OK x ->
577     (match x.Types.snd with
578      | Joint.Sequential (x0, x1) -> dummy
579      | Joint.Final s ->
580        (match s with
581         | Joint.GOTO x0 -> dummy
582         | Joint.RETURN -> dummy
583         | Joint.TAILCALL (f', args) ->
584           (match Obj.magic
585                    (Monad.m_bind0 (Monad.max_def Errors.res0)
586                      (Joint_semantics.block_of_call p.sparams p.globals
587                        (let p0 = p.sparams.Joint_semantics.spp in
588                        let globals0 = p.globals in
589                        let g = p.ev_genv in g.Joint_semantics.ge) f'
590                        st.Joint_semantics.st_no_pc) (fun bl ->
591                      Obj.magic
592                        (Joint_semantics.fetch_internal_function
593                          (let p0 = p.sparams.Joint_semantics.spp in
594                          let globals0 = p.globals in
595                          let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
596            | Errors.OK i_f -> i_f.Types.fst
597            | Errors.Error x0 -> dummy))
598      | Joint.FCOND (x0, x1, x2) -> dummy)
599   | Errors.Error x -> dummy)
600
601(** val pcDeq : Deqsets.deqSet **)
602let pcDeq =
603  Obj.magic ByteValues.eq_program_counter
604
605(** val cost_label_of_stmt :
606    evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
607    Types.option **)
608let cost_label_of_stmt p = function
609| Joint.Sequential (s0, x) ->
610  (match s0 with
611   | Joint.COST_LABEL lbl -> Types.Some lbl
612   | Joint.CALL (x0, x1, x2) -> Types.None
613   | Joint.COND (x0, x1) -> Types.None
614   | Joint.Step_seq x0 -> Types.None)
615| Joint.Final x -> Types.None
616| Joint.FCOND (x0, x1, x2) -> Types.None
617
618(** val joint_label_of_pc :
619    evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
620    Types.option **)
621let joint_label_of_pc p pc =
622  match Joint_semantics.fetch_statement p.sparams p.globals
623          (let p0 = p.sparams.Joint_semantics.spp in
624          let globals0 = p.globals in
625          let g = p.ev_genv in g.Joint_semantics.ge) pc with
626  | Errors.OK fn_stmt -> cost_label_of_stmt p fn_stmt.Types.snd
627  | Errors.Error x -> Types.None
628
629(** val joint_abstract_status :
630    prog_params -> StructuredTraces.abstract_status **)
631let joint_abstract_status p =
632  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
633    (Obj.magic
634      (Joint_semantics.pc
635        (prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars p)));
636    StructuredTraces.as_classify =
637    (Obj.magic (joint_classify (make_global p)));
638    StructuredTraces.as_label_of_pc =
639    (Obj.magic (joint_label_of_pc (make_global p)));
640    StructuredTraces.as_result =
641    (Obj.magic
642      (Joint_semantics.is_final (prog_params_to_ev_params__o__sparams p)
643        (make_global p).globals (make_global p).ev_genv
644        Joint_semantics.exit_pc)); StructuredTraces.as_call_ident =
645    (fun st -> joint_call_ident (make_global p) (Types.pi1 (Obj.magic st)));
646    StructuredTraces.as_tailcall_ident = (fun st ->
647    joint_tailcall_ident (make_global p) (Types.pi1 (Obj.magic st))) }
648
649(** val joint_status :
650    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
651    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
652let joint_status p prog0 stacksizes =
653  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
654    stacksizes }
655
Note: See TracBrowser for help on using the repository browser.