extracted/traces.ml

   1 open Preamble
   2
   3 open ExtraMonads
   4
   5 open Deqsets_extra
   6
   7 open State
   8
   9 open Bind_new
  10
  11 open BindLists
  12
  13 open Blocks
  14
  15 open TranslateUtils
  16
  17 open ExtraGlobalenvs
  18
  19 open I8051bis
  20
  21 open String
  22
  23 open Sets
  24
  25 open Listb
  26
  27 open LabelledObjects
  28
  29 open BitVectorTrie
  30
  31 open Graphs
  32
  33 open I8051
  34
  35 open Order
  36
  37 open Registers
  38
  39 open BackEndOps
  40
  41 open Joint
  42
  43 open BEMem
  44
  45 open CostLabel
  46
  47 open Events
  48
  49 open IOMonad
  50
  51 open IO
  52
  53 open Extra_bool
  54
  55 open Coqlib
  56
  57 open Values
  58
  59 open FrontEndVal
  60
  61 open Hide
  62
  63 open ByteValues
  64
  65 open Division
  66
  67 open Z
  68
  69 open BitVectorZ
  70
  71 open Pointers
  72
  73 open GenMem
  74
  75 open FrontEndMem
  76
  77 open Proper
  78
  79 open PositiveMap
  80
  81 open Deqsets
  82
  83 open Extralib
  84
  85 open Lists
  86
  87 open Identifiers
  88
  89 open Exp
  90
  91 open Arithmetic
  92
  93 open Vector
  94
  95 open Div_and_mod
  96
  97 open Util
  98
  99 open FoldStuff
 100
 101 open BitVector
 102
 103 open Extranat
 104
 105 open Integers
 106
 107 open AST
 108
 109 open ErrorMessages
 110
 111 open Option
 112
 113 open Setoids
 114
 115 open Monad
 116
 117 open Jmeq
 118
 119 open Russell
 120
 121 open Positive
 122
 123 open PreIdentifiers
 124
 125 open Bool
 126
 127 open Relations
 128
 129 open Nat
 130
 131 open List
 132
 133 open Hints_declaration
 134
 135 open Core_notation
 136
 137 open Pts
 138
 139 open Logic
 140
 141 open Types
 142
 143 open Errors
 144
 145 open Globalenvs
 146
 147 open Joint_semantics
 148
 149 open SemanticsUtils
 150
 151 open StructuredTraces
 152
 153 type evaluation_params = { globals : AST.ident List.list;
 154                            ev_genv : Joint_semantics.genv }
 155
 156 (** val evaluation_params_rect_Type4 :
 157     Joint_semantics.sem_params -> (AST.ident List.list ->
 158     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
 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
 162
 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
 169
 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
 176
 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
 183
 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
 190
 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
 197
 198 (** val globals :
 199     Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
 200 let rec globals p xxx =
 201   xxx.globals
 202
 203 (** val ev_genv :
 204     Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
 205 let rec ev_genv p xxx =
 206   xxx.ev_genv
 207
 208 (** val evaluation_params_inv_rect_Type4 :
 209     Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
 210     -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
 211 let evaluation_params_inv_rect_Type4 x1 hterm h1 =
 212   let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __
 213
 214 (** val evaluation_params_inv_rect_Type3 :
 215     Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
 216     -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
 217 let evaluation_params_inv_rect_Type3 x1 hterm h1 =
 218   let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __
 219
 220 (** val evaluation_params_inv_rect_Type2 :
 221     Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
 222     -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
 223 let evaluation_params_inv_rect_Type2 x1 hterm h1 =
 224   let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __
 225
 226 (** val evaluation_params_inv_rect_Type1 :
 227     Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
 228     -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
 229 let evaluation_params_inv_rect_Type1 x1 hterm h1 =
 230   let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __
 231
 232 (** val evaluation_params_inv_rect_Type0 :
 233     Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
 234     -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
 235 let evaluation_params_inv_rect_Type0 x1 hterm h1 =
 236   let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __
 237
 238 (** val evaluation_params_discr :
 239     Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
 240     __ **)
 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
 245
 246 (** val evaluation_params_jmdiscr :
 247     Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
 248     __ **)
 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
 253
 254 (** val dpi1__o__ev_genv__o__inject :
 255     Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 256     Joint_semantics.genv Types.sig0 **)
 257 let dpi1__o__ev_genv__o__inject x0 x2 =
 258   x2.Types.dpi1.ev_genv
 259
 260 (** val dpi1__o__ev_genv__o__ge__o__inject :
 261     Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 262     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 263     Types.sig0 **)
 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
 266
 267 (** val dpi1__o__ev_genv__o__ge :
 268     Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 269     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
 270 let dpi1__o__ev_genv__o__ge x0 x2 =
 271   x2.Types.dpi1.ev_genv.Joint_semantics.ge
 272
 273 (** val eject__o__ev_genv__o__inject :
 274     Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 275     Joint_semantics.genv Types.sig0 **)
 276 let eject__o__ev_genv__o__inject x0 x2 =
 277   (Types.pi1 x2).ev_genv
 278
 279 (** val eject__o__ev_genv__o__ge__o__inject :
 280     Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 281     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 282     Types.sig0 **)
 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
 285
 286 (** val eject__o__ev_genv__o__ge :
 287     Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 288     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
 289 let eject__o__ev_genv__o__ge x0 x2 =
 290   (Types.pi1 x2).ev_genv.Joint_semantics.ge
 291
 292 (** val ev_genv__o__ge :
 293     Joint_semantics.sem_params -> evaluation_params ->
 294     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
 295 let ev_genv__o__ge x0 x1 =
 296   x1.ev_genv.Joint_semantics.ge
 297
 298 (** val ev_genv__o__ge__o__inject :
 299     Joint_semantics.sem_params -> evaluation_params ->
 300     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 301     Types.sig0 **)
 302 let ev_genv__o__ge__o__inject x0 x1 =
 303   Joint_semantics.ge__o__inject x1.globals x1.ev_genv
 304
 305 (** val ev_genv__o__inject :
 306     Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
 307     Types.sig0 **)
 308 let ev_genv__o__inject x0 x1 =
 309   x1.ev_genv
 310
 311 (** val dpi1__o__ev_genv :
 312     Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 313     Joint_semantics.genv **)
 314 let dpi1__o__ev_genv x0 x2 =
 315   x2.Types.dpi1.ev_genv
 316
 317 (** val eject__o__ev_genv :
 318     Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 319     Joint_semantics.genv **)
 320 let eject__o__ev_genv x0 x2 =
 321   (Types.pi1 x2).ev_genv
 322
 323 type prog_params = { prog_spars : Joint_semantics.sem_params;
 324                      prog : Joint.joint_program;
 325                      stack_sizes : (AST.ident -> Nat.nat Types.option) }
 326
 327 (** val prog_params_rect_Type4 :
 328     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 329     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 333   in
 334   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 335
 336 (** val prog_params_rect_Type5 :
 337     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 338     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 342   in
 343   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 344
 345 (** val prog_params_rect_Type3 :
 346     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 347     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 351   in
 352   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 353
 354 (** val prog_params_rect_Type2 :
 355     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 356     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 360   in
 361   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 362
 363 (** val prog_params_rect_Type1 :
 364     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 365     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 369   in
 370   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 371
 372 (** val prog_params_rect_Type0 :
 373     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 374     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
 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
 378   in
 379   h_mk_prog_params prog_spars0 prog0 stack_sizes0
 380
 381 (** val prog_spars : prog_params -> Joint_semantics.sem_params **)
 382 let rec prog_spars xxx =
 383   xxx.prog_spars
 384
 385 (** val prog : prog_params -> Joint.joint_program **)
 386 let rec prog xxx =
 387   xxx.prog
 388
 389 (** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
 390 let rec stack_sizes xxx =
 391   xxx.stack_sizes
 392
 393 (** val prog_params_inv_rect_Type4 :
 394     prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 395     (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
 396 let prog_params_inv_rect_Type4 hterm h1 =
 397   let hcut = prog_params_rect_Type4 h1 hterm in hcut __
 398
 399 (** val prog_params_inv_rect_Type3 :
 400     prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 401     (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
 402 let prog_params_inv_rect_Type3 hterm h1 =
 403   let hcut = prog_params_rect_Type3 h1 hterm in hcut __
 404
 405 (** val prog_params_inv_rect_Type2 :
 406     prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 407     (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
 408 let prog_params_inv_rect_Type2 hterm h1 =
 409   let hcut = prog_params_rect_Type2 h1 hterm in hcut __
 410
 411 (** val prog_params_inv_rect_Type1 :
 412     prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 413     (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
 414 let prog_params_inv_rect_Type1 hterm h1 =
 415   let hcut = prog_params_rect_Type1 h1 hterm in hcut __
 416
 417 (** val prog_params_inv_rect_Type0 :
 418     prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 419     (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
 420 let prog_params_inv_rect_Type0 hterm h1 =
 421   let hcut = prog_params_rect_Type0 h1 hterm in hcut __
 422
 423 (** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
 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
 428
 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'
 433
 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
 439
 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
 444
 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
 448
 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
 453
 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
 458
 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
 463     x0.prog_spars
 464
 465 (** val joint_make_global : prog_params -> evaluation_params **)
 466 let joint_make_global p =
 467   { globals =
 468     (Joint.prog_names (Joint_semantics.spp'__o__spp p.prog_spars) p.prog);
 469     ev_genv =
 470     (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }
 471
 472 (** val joint_make_global__o__ev_genv :
 473     prog_params -> Joint_semantics.genv **)
 474 let joint_make_global__o__ev_genv x0 =
 475   (joint_make_global x0).ev_genv
 476
 477 (** val joint_make_global__o__ev_genv__o__ge :
 478     prog_params -> Joint.joint_closed_internal_function AST.fundef
 479     Globalenvs.genv_t **)
 480 let joint_make_global__o__ev_genv__o__ge x0 =
 481   ev_genv__o__ge x0.prog_spars (joint_make_global x0)
 482
 483 (** val joint_make_global__o__ev_genv__o__ge__o__inject :
 484     prog_params -> Joint.joint_closed_internal_function AST.fundef
 485     Globalenvs.genv_t Types.sig0 **)
 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)
 488
 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)
 493
 494 (** val joint_make_global__o__inject :
 495     prog_params -> evaluation_params Types.sig0 **)
 496 let joint_make_global__o__inject x0 =
 497   joint_make_global x0
 498
 499 (** val make_initial_state :
 500     prog_params -> Joint_semantics.state_pc Errors.res **)
 501 let make_initial_state pars =
 502   let p = pars.prog in
 503   let ge = ev_genv pars.prog_spars in
 504   Obj.magic
 505     (Monad.m_bind0 (Monad.max_def Errors.res0)
 506       (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
 507       (fun m0 ->
 508       (let { Types.fst = m; Types.snd = spb } =
 509          GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
 510        in
 511       (fun _ ->
 512       let globals_size =
 513         Joint.globals_stacksize
 514           (Joint_semantics.spp'__o__spp pars.prog_spars) p
 515       in
 516       let spp = { Pointers.pblock = spb; Pointers.poff =
 517         (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 518           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 519           (Nat.S Nat.O))))))))))))))))
 520           (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
 521       in
 522       let main = p.Joint.joint_prog.AST.prog_main in
 523       let st = { Joint_semantics.st_frms = (Types.Some
 524         (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
 525         Joint_semantics.istack = Joint_semantics.Empty_is;
 526         Joint_semantics.carry = (ByteValues.BBbit Bool.False);
 527         Joint_semantics.regs =
 528         ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
 529           spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
 530         globals_size }
 531       in
 532       Monad.m_return0 (Monad.max_def Errors.res0)
 533         { Joint_semantics.st_no_pc =
 534         (Joint_semantics.set_sp
 535           (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
 536         Joint_semantics.pc = Joint_semantics.init_pc;
 537         Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
 538         __))
 539
 540 (** val joint_classify_step :
 541     Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
 542     StructuredTraces.status_class **)
 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
 548
 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
 556
 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) ->
 566        joint_classify_step
 567          (Joint.uns_pars__o__u_pars
 568            (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
 569      | Joint.Final s ->
 570        joint_classify_final
 571          (Joint.uns_pars__o__u_pars
 572            (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
 573      | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
 574   | Errors.Error x -> StructuredTraces.Cl_other
 575
 576 (** val joint_call_ident :
 577     Joint_semantics.sem_params -> evaluation_params ->
 578     Joint_semantics.state_pc -> AST.ident **)
 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
 583    | Errors.OK x ->
 584      (match x.Types.snd with
 585       | Joint.Sequential (s, next) ->
 586         (match s with
 587          | Joint.COST_LABEL x0 -> dummy
 588          | Joint.CALL (f', args, dest) ->
 589            (match Obj.magic
 590                     (Monad.m_bind0 (Monad.max_def Errors.res0)
 591                       (Joint_semantics.block_of_call p pars.globals
 592                         pars.ev_genv f' st.Joint_semantics.st_no_pc)
 593                       (fun bl ->
 594                       Obj.magic
 595                         (Joint_semantics.fetch_internal_function pars.globals
 596                           pars.ev_genv bl))) with
 597             | Errors.OK i_f -> i_f.Types.fst
 598             | Errors.Error x0 -> dummy)
 599          | Joint.COND (x0, x1) -> dummy
 600          | Joint.Step_seq x0 -> dummy)
 601       | Joint.Final x0 -> dummy
 602       | Joint.FCOND (x0, x1, x2) -> dummy)
 603    | Errors.Error x -> dummy)
 604
 605 (** val joint_tailcall_ident :
 606     Joint_semantics.sem_params -> evaluation_params ->
 607     Joint_semantics.state_pc -> AST.ident **)
 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
 612    | Errors.OK x ->
 613      (match x.Types.snd with
 614       | Joint.Sequential (x0, x1) -> dummy
 615       | Joint.Final s ->
 616         (match s with
 617          | Joint.GOTO x0 -> dummy
 618          | Joint.RETURN -> dummy
 619          | Joint.TAILCALL (f', args) ->
 620            (match Obj.magic
 621                     (Monad.m_bind0 (Monad.max_def Errors.res0)
 622                       (Joint_semantics.block_of_call p pars.globals
 623                         pars.ev_genv f' st.Joint_semantics.st_no_pc)
 624                       (fun bl ->
 625                       Obj.magic
 626                         (Joint_semantics.fetch_internal_function pars.globals
 627                           pars.ev_genv bl))) with
 628             | Errors.OK i_f -> i_f.Types.fst
 629             | Errors.Error x0 -> dummy))
 630       | Joint.FCOND (x0, x1, x2) -> dummy)
 631    | Errors.Error x -> dummy)
 632
 633 (** val pcDeq : Deqsets.deqSet **)
 634 let pcDeq =
 635   Obj.magic ByteValues.eq_program_counter
 636
 637 (** val cost_label_of_stmt :
 638     Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
 639     CostLabel.costlabel Types.option **)
 640 let cost_label_of_stmt p g = function
 641 | Joint.Sequential (s0, x) ->
 642   (match s0 with
 643    | Joint.COST_LABEL lbl -> Types.Some lbl
 644    | Joint.CALL (x0, x1, x2) -> Types.None
 645    | Joint.COND (x0, x1) -> Types.None
 646    | Joint.Step_seq x0 -> Types.None)
 647 | Joint.Final x -> Types.None
 648 | Joint.FCOND (x0, x1, x2) -> Types.None
 649
 650 (** val joint_label_of_pc :
 651     Joint_semantics.sem_params -> evaluation_params ->
 652     ByteValues.program_counter -> CostLabel.costlabel Types.option **)
 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
 659
 660 (** val exit_pc' : ByteValues.program_counter **)
 661 let exit_pc' =
 662   { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
 663     ByteValues.pc_offset = (Positive.P1 Positive.One) }
 664
 665 (** val joint_final :
 666     Joint_semantics.sem_params -> evaluation_params ->
 667     Joint_semantics.state_pc -> Integers.int Types.option **)
 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
 671    | Bool.True ->
 672      let ret =
 673        (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
 674      in
 675      (match Obj.magic
 676               (Monad.m_bind0 (Monad.max_def Errors.res0)
 677                 (Obj.magic
 678                   (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
 679                     pars.globals ge.Joint_semantics.ge ret
 680                     st.Joint_semantics.st_no_pc)) (fun vals ->
 681                 Obj.magic (ByteValues.word_of_list_beval vals))) with
 682       | Errors.OK v -> Types.Some v
 683       | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
 684    | Bool.False -> Types.None)
 685
 686 (** val joint_abstract_status :
 687     prog_params -> StructuredTraces.abstract_status **)
 688 let joint_abstract_status p =
 689   { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
 690     (Obj.magic
 691       (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
 692     StructuredTraces.as_classify =
 693     (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
 694     StructuredTraces.as_label_of_pc =
 695     (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
 696     StructuredTraces.as_result =
 697     (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
 698     StructuredTraces.as_call_ident = (fun st ->
 699     joint_call_ident p.prog_spars (joint_make_global p)
 700       (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
 701     (fun st ->
 702     joint_tailcall_ident p.prog_spars (joint_make_global p)
 703       (Types.pi1 (Obj.magic st))) }
 704
 705 (** val joint_status :
 706     Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 707     Nat.nat Types.option) -> StructuredTraces.abstract_status **)
 708 let joint_status p prog0 stacksizes =
 709   joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
 710     stacksizes }
 711