133 open Hints_declaration
151 open StructuredTraces
153 type evaluation_params = { globals : AST.ident List.list;
154 ev_genv : Joint_semantics.genv }
156 (** val evaluation_params_rect_Type4 :
157 Joint_semantics.sem_params -> (AST.ident List.list ->
158 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
159 let 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
163 (** val evaluation_params_rect_Type5 :
164 Joint_semantics.sem_params -> (AST.ident List.list ->
165 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
166 let 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
170 (** val evaluation_params_rect_Type3 :
171 Joint_semantics.sem_params -> (AST.ident List.list ->
172 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
173 let 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
177 (** val evaluation_params_rect_Type2 :
178 Joint_semantics.sem_params -> (AST.ident List.list ->
179 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
180 let 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
184 (** val evaluation_params_rect_Type1 :
185 Joint_semantics.sem_params -> (AST.ident List.list ->
186 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
187 let 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
191 (** val evaluation_params_rect_Type0 :
192 Joint_semantics.sem_params -> (AST.ident List.list ->
193 Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
194 let 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
199 Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
200 let rec globals p xxx =
204 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
205 let rec ev_genv p xxx =
208 (** val evaluation_params_inv_rect_Type4 :
209 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
210 -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
211 let evaluation_params_inv_rect_Type4 x1 hterm h1 =
212 let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __
214 (** val evaluation_params_inv_rect_Type3 :
215 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
216 -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
217 let evaluation_params_inv_rect_Type3 x1 hterm h1 =
218 let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __
220 (** val evaluation_params_inv_rect_Type2 :
221 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
222 -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
223 let evaluation_params_inv_rect_Type2 x1 hterm h1 =
224 let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __
226 (** val evaluation_params_inv_rect_Type1 :
227 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
228 -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
229 let evaluation_params_inv_rect_Type1 x1 hterm h1 =
230 let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __
232 (** val evaluation_params_inv_rect_Type0 :
233 Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
234 -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
235 let evaluation_params_inv_rect_Type0 x1 hterm h1 =
236 let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __
238 (** val evaluation_params_discr :
239 Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
241 let 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
246 (** val evaluation_params_jmdiscr :
247 Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
249 let 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
254 (** val dpi1__o__ev_genv__o__inject :
255 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
256 Joint_semantics.genv Types.sig0 **)
257 let dpi1__o__ev_genv__o__inject x0 x2 =
258 x2.Types.dpi1.ev_genv
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
264 let 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
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 **)
270 let dpi1__o__ev_genv__o__ge x0 x2 =
271 x2.Types.dpi1.ev_genv.Joint_semantics.ge
273 (** val eject__o__ev_genv__o__inject :
274 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
275 Joint_semantics.genv Types.sig0 **)
276 let eject__o__ev_genv__o__inject x0 x2 =
277 (Types.pi1 x2).ev_genv
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
283 let 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
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 **)
289 let eject__o__ev_genv__o__ge x0 x2 =
290 (Types.pi1 x2).ev_genv.Joint_semantics.ge
292 (** val ev_genv__o__ge :
293 Joint_semantics.sem_params -> evaluation_params ->
294 Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
295 let ev_genv__o__ge x0 x1 =
296 x1.ev_genv.Joint_semantics.ge
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
302 let ev_genv__o__ge__o__inject x0 x1 =
303 Joint_semantics.ge__o__inject x1.globals x1.ev_genv
305 (** val ev_genv__o__inject :
306 Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
308 let ev_genv__o__inject x0 x1 =
311 (** val dpi1__o__ev_genv :
312 Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
313 Joint_semantics.genv **)
314 let dpi1__o__ev_genv x0 x2 =
315 x2.Types.dpi1.ev_genv
317 (** val eject__o__ev_genv :
318 Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
319 Joint_semantics.genv **)
320 let eject__o__ev_genv x0 x2 =
321 (Types.pi1 x2).ev_genv
323 type prog_params = { prog_spars : Joint_semantics.sem_params;
324 prog : Joint.joint_program;
325 stack_sizes : (AST.ident -> Nat.nat Types.option) }
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 **)
330 let 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
334 h_mk_prog_params prog_spars0 prog0 stack_sizes0
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 **)
339 let 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
343 h_mk_prog_params prog_spars0 prog0 stack_sizes0
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 **)
348 let 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
352 h_mk_prog_params prog_spars0 prog0 stack_sizes0
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 **)
357 let 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
361 h_mk_prog_params prog_spars0 prog0 stack_sizes0
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 **)
366 let 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
370 h_mk_prog_params prog_spars0 prog0 stack_sizes0
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 **)
375 let 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
379 h_mk_prog_params prog_spars0 prog0 stack_sizes0
381 (** val prog_spars : prog_params -> Joint_semantics.sem_params **)
382 let rec prog_spars xxx =
385 (** val prog : prog_params -> Joint.joint_program **)
389 (** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
390 let rec stack_sizes xxx =
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 **)
396 let prog_params_inv_rect_Type4 hterm h1 =
397 let hcut = prog_params_rect_Type4 h1 hterm in hcut __
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 **)
402 let prog_params_inv_rect_Type3 hterm h1 =
403 let hcut = prog_params_rect_Type3 h1 hterm in hcut __
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 **)
408 let prog_params_inv_rect_Type2 hterm h1 =
409 let hcut = prog_params_rect_Type2 h1 hterm in hcut __
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 **)
414 let prog_params_inv_rect_Type1 hterm h1 =
415 let hcut = prog_params_rect_Type1 h1 hterm in hcut __
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 **)
420 let prog_params_inv_rect_Type0 hterm h1 =
421 let hcut = prog_params_rect_Type0 h1 hterm in hcut __
423 (** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
424 let 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
429 (** val prog_spars__o__spp' :
430 prog_params -> Joint_semantics.serialized_params **)
431 let prog_spars__o__spp' x0 =
432 x0.prog_spars.Joint_semantics.spp'
434 (** val prog_spars__o__spp'__o__msu_pars :
435 prog_params -> Joint.joint_closed_internal_function
436 Joint_semantics.sem_unserialized_params **)
437 let prog_spars__o__spp'__o__msu_pars x0 =
438 Joint_semantics.spp'__o__msu_pars x0.prog_spars
440 (** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
441 prog_params -> Joint_semantics.sem_state_params **)
442 let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 =
443 Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars
445 (** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **)
446 let prog_spars__o__spp'__o__spp x0 =
447 Joint_semantics.spp'__o__spp x0.prog_spars
449 (** val prog_spars__o__spp'__o__spp__o__stmt_pars :
450 prog_params -> Joint.stmt_params **)
451 let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
452 Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars
454 (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
455 prog_params -> Joint.uns_params **)
456 let 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
459 (** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
460 prog_params -> Joint.unserialized_params **)
461 let 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
465 (** val joint_make_global : prog_params -> evaluation_params **)
466 let joint_make_global p =
468 (Joint.prog_names (Joint_semantics.spp'__o__spp p.prog_spars) p.prog);
470 (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }
472 (** val joint_make_global__o__ev_genv :
473 prog_params -> Joint_semantics.genv **)
474 let joint_make_global__o__ev_genv x0 =
475 (joint_make_global x0).ev_genv
477 (** val joint_make_global__o__ev_genv__o__ge :
478 prog_params -> Joint.joint_closed_internal_function AST.fundef
479 Globalenvs.genv_t **)
480 let joint_make_global__o__ev_genv__o__ge x0 =
481 ev_genv__o__ge x0.prog_spars (joint_make_global x0)
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 **)
486 let 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)
489 (** val joint_make_global__o__ev_genv__o__inject :
490 prog_params -> Joint_semantics.genv Types.sig0 **)
491 let joint_make_global__o__ev_genv__o__inject x0 =
492 ev_genv__o__inject x0.prog_spars (joint_make_global x0)
494 (** val joint_make_global__o__inject :
495 prog_params -> evaluation_params Types.sig0 **)
496 let joint_make_global__o__inject x0 =
499 (** val make_initial_state :
500 prog_params -> Joint_semantics.state_pc Errors.res **)
501 let make_initial_state pars =
503 let ge = ev_genv pars.prog_spars in
505 (Monad.m_bind0 (Monad.max_def Errors.res0)
506 (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
508 (let { Types.fst = m; Types.snd = spb } =
509 GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
513 Joint.globals_stacksize
514 (Joint_semantics.spp'__o__spp pars.prog_spars) p
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)))) }
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 =
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) }))
540 (** val joint_classify_step :
541 Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
542 StructuredTraces.status_class **)
543 let 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
549 (** val joint_classify_final :
550 Joint.unserialized_params -> Joint.joint_fin_step ->
551 StructuredTraces.status_class **)
552 let 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
557 (** val joint_classify :
558 Joint_semantics.sem_params -> evaluation_params ->
559 Joint_semantics.state_pc -> StructuredTraces.status_class **)
560 let 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) ->
567 (Joint.uns_pars__o__u_pars
568 (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
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
576 (** val joint_call_ident :
577 Joint_semantics.sem_params -> evaluation_params ->
578 Joint_semantics.state_pc -> AST.ident **)
579 let 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
584 (match x.Types.snd with
585 | Joint.Sequential (s, next) ->
587 | Joint.COST_LABEL x0 -> dummy
588 | Joint.CALL (f', args, dest) ->
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)
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)
605 (** val joint_tailcall_ident :
606 Joint_semantics.sem_params -> evaluation_params ->
607 Joint_semantics.state_pc -> AST.ident **)
608 let 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
613 (match x.Types.snd with
614 | Joint.Sequential (x0, x1) -> dummy
617 | Joint.GOTO x0 -> dummy
618 | Joint.RETURN -> dummy
619 | Joint.TAILCALL (f', args) ->
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)
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)
633 (** val pcDeq : Deqsets.deqSet **)
635 Obj.magic ByteValues.eq_program_counter
637 (** val cost_label_of_stmt :
638 Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
639 CostLabel.costlabel Types.option **)
640 let cost_label_of_stmt p g = function
641 | Joint.Sequential (s0, x) ->
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
650 (** val joint_label_of_pc :
651 Joint_semantics.sem_params -> evaluation_params ->
652 ByteValues.program_counter -> CostLabel.costlabel Types.option **)
653 let 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
660 (** val exit_pc' : ByteValues.program_counter **)
662 { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
663 ByteValues.pc_offset = (Positive.P1 Positive.One) }
665 (** val joint_final :
666 Joint_semantics.sem_params -> evaluation_params ->
667 Joint_semantics.state_pc -> Integers.int Types.option **)
668 let 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
673 (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
676 (Monad.m_bind0 (Monad.max_def Errors.res0)
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)
686 (** val joint_abstract_status :
687 prog_params -> StructuredTraces.abstract_status **)
688 let joint_abstract_status p =
689 { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
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 =
702 joint_tailcall_ident p.prog_spars (joint_make_global p)
703 (Types.pi1 (Obj.magic st))) }
705 (** val joint_status :
706 Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
707 Nat.nat Types.option) -> StructuredTraces.abstract_status **)
708 let joint_status p prog0 stacksizes =
709 joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =