extracted/semanticsUtils.mli

   1 open Preamble
   2
   3 open ExtraGlobalenvs
   4
   5 open I8051bis
   6
   7 open String
   8
   9 open Sets
  10
  11 open Listb
  12
  13 open LabelledObjects
  14
  15 open BitVectorTrie
  16
  17 open Graphs
  18
  19 open I8051
  20
  21 open Order
  22
  23 open Registers
  24
  25 open BackEndOps
  26
  27 open Joint
  28
  29 open BEMem
  30
  31 open CostLabel
  32
  33 open Events
  34
  35 open IOMonad
  36
  37 open IO
  38
  39 open Extra_bool
  40
  41 open Coqlib
  42
  43 open Values
  44
  45 open FrontEndVal
  46
  47 open Hide
  48
  49 open ByteValues
  50
  51 open Division
  52
  53 open Z
  54
  55 open BitVectorZ
  56
  57 open Pointers
  58
  59 open GenMem
  60
  61 open FrontEndMem
  62
  63 open Proper
  64
  65 open PositiveMap
  66
  67 open Deqsets
  68
  69 open Extralib
  70
  71 open Lists
  72
  73 open Identifiers
  74
  75 open Exp
  76
  77 open Arithmetic
  78
  79 open Vector
  80
  81 open Div_and_mod
  82
  83 open Util
  84
  85 open FoldStuff
  86
  87 open BitVector
  88
  89 open Extranat
  90
  91 open Integers
  92
  93 open AST
  94
  95 open ErrorMessages
  96
  97 open Option
  98
  99 open Setoids
 100
 101 open Monad
 102
 103 open Jmeq
 104
 105 open Russell
 106
 107 open Positive
 108
 109 open PreIdentifiers
 110
 111 open Bool
 112
 113 open Relations
 114
 115 open Nat
 116
 117 open List
 118
 119 open Hints_declaration
 120
 121 open Core_notation
 122
 123 open Pts
 124
 125 open Logic
 126
 127 open Types
 128
 129 open Errors
 130
 131 open Globalenvs
 132
 133 open Joint_semantics
 134
 135 open Deqsets_extra
 136
 137 open State
 138
 139 open Bind_new
 140
 141 open BindLists
 142
 143 open Blocks
 144
 145 open TranslateUtils
 146
 147 open ExtraMonads
 148
 149 val reg_store :
 150   PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
 151   Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
 152
 153 val reg_retrieve :
 154   ByteValues.beval Registers.register_env -> Registers.register ->
 155   ByteValues.beval Errors.res
 156
 157 type hw_register_env = { reg_env : ByteValues.beval
 158                                    BitVectorTrie.bitVectorTrie;
 159                          other_bit : ByteValues.bebit }
 160
 161 val hw_register_env_rect_Type4 :
 162   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 163   -> hw_register_env -> 'a1
 164
 165 val hw_register_env_rect_Type5 :
 166   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 167   -> hw_register_env -> 'a1
 168
 169 val hw_register_env_rect_Type3 :
 170   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 171   -> hw_register_env -> 'a1
 172
 173 val hw_register_env_rect_Type2 :
 174   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 175   -> hw_register_env -> 'a1
 176
 177 val hw_register_env_rect_Type1 :
 178   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 179   -> hw_register_env -> 'a1
 180
 181 val hw_register_env_rect_Type0 :
 182   (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 183   -> hw_register_env -> 'a1
 184
 185 val reg_env : hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie
 186
 187 val other_bit : hw_register_env -> ByteValues.bebit
 188
 189 val hw_register_env_inv_rect_Type4 :
 190   hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 191   ByteValues.bebit -> __ -> 'a1) -> 'a1
 192
 193 val hw_register_env_inv_rect_Type3 :
 194   hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 195   ByteValues.bebit -> __ -> 'a1) -> 'a1
 196
 197 val hw_register_env_inv_rect_Type2 :
 198   hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 199   ByteValues.bebit -> __ -> 'a1) -> 'a1
 200
 201 val hw_register_env_inv_rect_Type1 :
 202   hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 203   ByteValues.bebit -> __ -> 'a1) -> 'a1
 204
 205 val hw_register_env_inv_rect_Type0 :
 206   hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 207   ByteValues.bebit -> __ -> 'a1) -> 'a1
 208
 209 val hw_register_env_discr : hw_register_env -> hw_register_env -> __
 210
 211 val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __
 212
 213 val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval
 214
 215 val hwreg_store :
 216   I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env
 217
 218 val hwreg_set_other : ByteValues.bebit -> hw_register_env -> hw_register_env
 219
 220 val hwreg_retrieve_sp : hw_register_env -> ByteValues.xpointer Errors.res
 221
 222 val hwreg_store_sp :
 223   hw_register_env -> ByteValues.xpointer -> hw_register_env
 224
 225 val init_hw_register_env : ByteValues.xpointer -> hw_register_env
 226
 227 type sem_graph_params = { sgp_pars : Joint.uns_params;
 228                           sgp_sup : (__ -> __
 229                                     Joint_semantics.sem_unserialized_params);
 230                           graph_pre_main_generator : (Joint.joint_program ->
 231                                                      Joint.joint_closed_internal_function) }
 232
 233 val sem_graph_params_rect_Type4 :
 234   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 235   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 236   sem_graph_params -> 'a1
 237
 238 val sem_graph_params_rect_Type5 :
 239   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 240   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 241   sem_graph_params -> 'a1
 242
 243 val sem_graph_params_rect_Type3 :
 244   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 245   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 246   sem_graph_params -> 'a1
 247
 248 val sem_graph_params_rect_Type2 :
 249   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 250   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 251   sem_graph_params -> 'a1
 252
 253 val sem_graph_params_rect_Type1 :
 254   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 255   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 256   sem_graph_params -> 'a1
 257
 258 val sem_graph_params_rect_Type0 :
 259   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 260   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 261   sem_graph_params -> 'a1
 262
 263 val sgp_pars : sem_graph_params -> Joint.uns_params
 264
 265 val sgp_sup0 :
 266   sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params
 267
 268 val graph_pre_main_generator :
 269   sem_graph_params -> Joint.joint_program ->
 270   Joint.joint_closed_internal_function
 271
 272 val sem_graph_params_inv_rect_Type4 :
 273   sem_graph_params -> (Joint.uns_params -> (__ -> __
 274   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 275   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 276
 277 val sem_graph_params_inv_rect_Type3 :
 278   sem_graph_params -> (Joint.uns_params -> (__ -> __
 279   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 280   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 281
 282 val sem_graph_params_inv_rect_Type2 :
 283   sem_graph_params -> (Joint.uns_params -> (__ -> __
 284   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 285   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 286
 287 val sem_graph_params_inv_rect_Type1 :
 288   sem_graph_params -> (Joint.uns_params -> (__ -> __
 289   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 290   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 291
 292 val sem_graph_params_inv_rect_Type0 :
 293   sem_graph_params -> (Joint.uns_params -> (__ -> __
 294   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 295   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 296
 297 val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __
 298
 299 val sem_graph_params_to_graph_params : sem_graph_params -> Joint.graph_params
 300
 301 val sem_graph_params_to_sem_params :
 302   sem_graph_params -> Joint_semantics.sem_params
 303
 304 val sem_params_from_sem_graph_params__o__spp' :
 305   sem_graph_params -> Joint_semantics.serialized_params
 306
 307 val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
 308   sem_graph_params -> Joint.joint_closed_internal_function
 309   Joint_semantics.sem_unserialized_params
 310
 311 val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
 312   sem_graph_params -> Joint_semantics.sem_state_params
 313
 314 val sem_params_from_sem_graph_params__o__spp'__o__spp :
 315   sem_graph_params -> Joint.params
 316
 317 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
 318   sem_graph_params -> Joint.stmt_params
 319
 320 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
 321   sem_graph_params -> Joint.uns_params
 322
 323 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
 324   sem_graph_params -> Joint.unserialized_params
 325
 326 type sem_lin_params = { slp_pars : Joint.uns_params;
 327                         slp_sup : (__ -> __
 328                                   Joint_semantics.sem_unserialized_params);
 329                         lin_pre_main_generator : (Joint.joint_program ->
 330                                                  Joint.joint_closed_internal_function) }
 331
 332 val sem_lin_params_rect_Type4 :
 333   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 334   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 335   sem_lin_params -> 'a1
 336
 337 val sem_lin_params_rect_Type5 :
 338   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 339   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 340   sem_lin_params -> 'a1
 341
 342 val sem_lin_params_rect_Type3 :
 343   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 344   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 345   sem_lin_params -> 'a1
 346
 347 val sem_lin_params_rect_Type2 :
 348   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 349   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 350   sem_lin_params -> 'a1
 351
 352 val sem_lin_params_rect_Type1 :
 353   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 354   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 355   sem_lin_params -> 'a1
 356
 357 val sem_lin_params_rect_Type0 :
 358   (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
 359   (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
 360   sem_lin_params -> 'a1
 361
 362 val slp_pars : sem_lin_params -> Joint.uns_params
 363
 364 val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params
 365
 366 val lin_pre_main_generator :
 367   sem_lin_params -> Joint.joint_program ->
 368   Joint.joint_closed_internal_function
 369
 370 val sem_lin_params_inv_rect_Type4 :
 371   sem_lin_params -> (Joint.uns_params -> (__ -> __
 372   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 373   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 374
 375 val sem_lin_params_inv_rect_Type3 :
 376   sem_lin_params -> (Joint.uns_params -> (__ -> __
 377   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 378   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 379
 380 val sem_lin_params_inv_rect_Type2 :
 381   sem_lin_params -> (Joint.uns_params -> (__ -> __
 382   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 383   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 384
 385 val sem_lin_params_inv_rect_Type1 :
 386   sem_lin_params -> (Joint.uns_params -> (__ -> __
 387   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 388   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 389
 390 val sem_lin_params_inv_rect_Type0 :
 391   sem_lin_params -> (Joint.uns_params -> (__ -> __
 392   Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 393   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
 394
 395 val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __
 396
 397 val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params
 398
 399 val sem_lin_params_to_sem_params :
 400   sem_lin_params -> Joint_semantics.sem_params
 401
 402 val sem_params_from_sem_lin_params__o__spp' :
 403   sem_lin_params -> Joint_semantics.serialized_params
 404
 405 val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
 406   sem_lin_params -> Joint.joint_closed_internal_function
 407   Joint_semantics.sem_unserialized_params
 408
 409 val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
 410   sem_lin_params -> Joint_semantics.sem_state_params
 411
 412 val sem_params_from_sem_lin_params__o__spp'__o__spp :
 413   sem_lin_params -> Joint.params
 414
 415 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
 416   sem_lin_params -> Joint.stmt_params
 417
 418 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
 419   sem_lin_params -> Joint.uns_params
 420
 421 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
 422   sem_lin_params -> Joint.unserialized_params
 423
 424 val match_genv_t_rect_Type4 :
 425   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 426   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 427
 428 val match_genv_t_rect_Type5 :
 429   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 430   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 431
 432 val match_genv_t_rect_Type3 :
 433   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 434   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 435
 436 val match_genv_t_rect_Type2 :
 437   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 438   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 439
 440 val match_genv_t_rect_Type1 :
 441   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 442   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 443
 444 val match_genv_t_rect_Type0 :
 445   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 446   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
 447
 448 val match_genv_t_inv_rect_Type4 :
 449   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 450   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 451
 452 val match_genv_t_inv_rect_Type3 :
 453   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 454   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 455
 456 val match_genv_t_inv_rect_Type2 :
 457   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 458   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 459
 460 val match_genv_t_inv_rect_Type1 :
 461   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 462   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 463
 464 val match_genv_t_inv_rect_Type0 :
 465   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 466   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 467
 468 val match_genv_t_discr :
 469   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 470   Globalenvs.genv_t -> __
 471
 472 val match_genv_t_jmdiscr :
 473   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 474   Globalenvs.genv_t -> __
 475
 476 val joint_globalenv :
 477   Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
 478   Types.option) -> Joint_semantics.genv
 479