source: extracted/traces.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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