extracted/traces.mli

   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 -> Joint_semantics.genv
 158   -> 'a1) -> evaluation_params -> 'a1
 159
 160 val evaluation_params_rect_Type5 :
 161   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
 162   -> 'a1) -> evaluation_params -> 'a1
 163
 164 val evaluation_params_rect_Type3 :
 165   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
 166   -> 'a1) -> evaluation_params -> 'a1
 167
 168 val evaluation_params_rect_Type2 :
 169   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
 170   -> 'a1) -> evaluation_params -> 'a1
 171
 172 val evaluation_params_rect_Type1 :
 173   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
 174   -> 'a1) -> evaluation_params -> 'a1
 175
 176 val evaluation_params_rect_Type0 :
 177   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
 178   -> 'a1) -> evaluation_params -> 'a1
 179
 180 val globals :
 181   Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list
 182
 183 val ev_genv :
 184   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
 185
 186 val evaluation_params_inv_rect_Type4 :
 187   Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
 188   Joint_semantics.genv -> __ -> 'a1) -> 'a1
 189
 190 val evaluation_params_inv_rect_Type3 :
 191   Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
 192   Joint_semantics.genv -> __ -> 'a1) -> 'a1
 193
 194 val evaluation_params_inv_rect_Type2 :
 195   Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
 196   Joint_semantics.genv -> __ -> 'a1) -> 'a1
 197
 198 val evaluation_params_inv_rect_Type1 :
 199   Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
 200   Joint_semantics.genv -> __ -> 'a1) -> 'a1
 201
 202 val evaluation_params_inv_rect_Type0 :
 203   Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
 204   Joint_semantics.genv -> __ -> 'a1) -> 'a1
 205
 206 val evaluation_params_discr :
 207   Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
 208
 209 val evaluation_params_jmdiscr :
 210   Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
 211
 212 val dpi1__o__ev_genv__o__inject :
 213   Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 214   Joint_semantics.genv Types.sig0
 215
 216 val dpi1__o__ev_genv__o__ge__o__inject :
 217   Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 218   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 219   Types.sig0
 220
 221 val dpi1__o__ev_genv__o__ge :
 222   Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 223   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 224
 225 val eject__o__ev_genv__o__inject :
 226   Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 227   Joint_semantics.genv Types.sig0
 228
 229 val eject__o__ev_genv__o__ge__o__inject :
 230   Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 231   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 232   Types.sig0
 233
 234 val eject__o__ev_genv__o__ge :
 235   Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 236   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 237
 238 val ev_genv__o__ge :
 239   Joint_semantics.sem_params -> evaluation_params ->
 240   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 241
 242 val ev_genv__o__ge__o__inject :
 243   Joint_semantics.sem_params -> evaluation_params ->
 244   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
 245   Types.sig0
 246
 247 val ev_genv__o__inject :
 248   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
 249   Types.sig0
 250
 251 val dpi1__o__ev_genv :
 252   Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
 253   Joint_semantics.genv
 254
 255 val eject__o__ev_genv :
 256   Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
 257   Joint_semantics.genv
 258
 259 type prog_params = { prog_spars : Joint_semantics.sem_params;
 260                      prog : Joint.joint_program;
 261                      stack_sizes : (AST.ident -> Nat.nat Types.option) }
 262
 263 val prog_params_rect_Type4 :
 264   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 265   Types.option) -> 'a1) -> prog_params -> 'a1
 266
 267 val prog_params_rect_Type5 :
 268   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 269   Types.option) -> 'a1) -> prog_params -> 'a1
 270
 271 val prog_params_rect_Type3 :
 272   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 273   Types.option) -> 'a1) -> prog_params -> 'a1
 274
 275 val prog_params_rect_Type2 :
 276   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 277   Types.option) -> 'a1) -> prog_params -> 'a1
 278
 279 val prog_params_rect_Type1 :
 280   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 281   Types.option) -> 'a1) -> prog_params -> 'a1
 282
 283 val prog_params_rect_Type0 :
 284   (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 285   Types.option) -> 'a1) -> prog_params -> 'a1
 286
 287 val prog_spars : prog_params -> Joint_semantics.sem_params
 288
 289 val prog : prog_params -> Joint.joint_program
 290
 291 val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option
 292
 293 val prog_params_inv_rect_Type4 :
 294   prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 295   (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
 296
 297 val prog_params_inv_rect_Type3 :
 298   prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 299   (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
 300
 301 val prog_params_inv_rect_Type2 :
 302   prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 303   (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
 304
 305 val prog_params_inv_rect_Type1 :
 306   prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 307   (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
 308
 309 val prog_params_inv_rect_Type0 :
 310   prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
 311   (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
 312
 313 val prog_params_jmdiscr : prog_params -> prog_params -> __
 314
 315 val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params
 316
 317 val prog_spars__o__spp'__o__msu_pars :
 318   prog_params -> Joint.joint_closed_internal_function
 319   Joint_semantics.sem_unserialized_params
 320
 321 val prog_spars__o__spp'__o__msu_pars__o__st_pars :
 322   prog_params -> Joint_semantics.sem_state_params
 323
 324 val prog_spars__o__spp'__o__spp : prog_params -> Joint.params
 325
 326 val prog_spars__o__spp'__o__spp__o__stmt_pars :
 327   prog_params -> Joint.stmt_params
 328
 329 val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
 330   prog_params -> Joint.uns_params
 331
 332 val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
 333   prog_params -> Joint.unserialized_params
 334
 335 val joint_make_global : prog_params -> evaluation_params
 336
 337 val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv
 338
 339 val joint_make_global__o__ev_genv__o__ge :
 340   prog_params -> Joint.joint_closed_internal_function AST.fundef
 341   Globalenvs.genv_t
 342
 343 val joint_make_global__o__ev_genv__o__ge__o__inject :
 344   prog_params -> Joint.joint_closed_internal_function AST.fundef
 345   Globalenvs.genv_t Types.sig0
 346
 347 val joint_make_global__o__ev_genv__o__inject :
 348   prog_params -> Joint_semantics.genv Types.sig0
 349
 350 val joint_make_global__o__inject :
 351   prog_params -> evaluation_params Types.sig0
 352
 353 val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res
 354
 355 val joint_classify_step :
 356   Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
 357   StructuredTraces.status_class
 358
 359 val joint_classify_final :
 360   Joint.unserialized_params -> Joint.joint_fin_step ->
 361   StructuredTraces.status_class
 362
 363 val joint_classify :
 364   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
 365   -> StructuredTraces.status_class
 366
 367 val joint_call_ident :
 368   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
 369   -> AST.ident
 370
 371 val joint_tailcall_ident :
 372   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
 373   -> AST.ident
 374
 375 val pcDeq : Deqsets.deqSet
 376
 377 val cost_label_of_stmt :
 378   Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
 379   CostLabel.costlabel Types.option
 380
 381 val joint_label_of_pc :
 382   Joint_semantics.sem_params -> evaluation_params ->
 383   ByteValues.program_counter -> CostLabel.costlabel Types.option
 384
 385 val exit_pc' : ByteValues.program_counter
 386
 387 val joint_final :
 388   Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
 389   -> Integers.int Types.option
 390
 391 val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
 392
 393 val joint_status :
 394   Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 395   Types.option) -> StructuredTraces.abstract_status
 396