extracted/toCminor.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Fresh
  82
  83 val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set
  84
  85 val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set
  86
  87 val gather_mem_vars_ls :
  88   Csyntax.labeled_statements -> Identifiers.identifier_set
  89
  90 val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set
  91
  92 type var_type =
  93 | Global of AST.region
  94 | Stack of Nat.nat
  95 | Local
  96
  97 val var_type_rect_Type4 :
  98   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
  99
 100 val var_type_rect_Type5 :
 101   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
 102
 103 val var_type_rect_Type3 :
 104   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
 105
 106 val var_type_rect_Type2 :
 107   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
 108
 109 val var_type_rect_Type1 :
 110   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
 111
 112 val var_type_rect_Type0 :
 113   (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
 114
 115 val var_type_inv_rect_Type4 :
 116   var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 117   'a1) -> 'a1
 118
 119 val var_type_inv_rect_Type3 :
 120   var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 121   'a1) -> 'a1
 122
 123 val var_type_inv_rect_Type2 :
 124   var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 125   'a1) -> 'a1
 126
 127 val var_type_inv_rect_Type1 :
 128   var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 129   'a1) -> 'a1
 130
 131 val var_type_inv_rect_Type0 :
 132   var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 133   'a1) -> 'a1
 134
 135 val var_type_discr : var_type -> var_type -> __
 136
 137 val var_type_jmdiscr : var_type -> var_type -> __
 138
 139 type var_types =
 140   (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
 141
 142 val lookup' :
 143   var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
 144   Types.prod Errors.res
 145
 146 val always_alloc : Csyntax.type0 -> Bool.bool
 147
 148 val characterise_vars :
 149   ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list ->
 150   Csyntax.function0 -> (var_types, Nat.nat) Types.prod
 151
 152 open FrontEndVal
 153
 154 open Hide
 155
 156 open ByteValues
 157
 158 open GenMem
 159
 160 open FrontEndMem
 161
 162 open Division
 163
 164 open Z
 165
 166 open BitVectorZ
 167
 168 open Pointers
 169
 170 open Values
 171
 172 open FrontEndOps
 173
 174 open Cminor_syntax
 175
 176 val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res
 177
 178 val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res
 179
 180 val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res
 181
 182 val translate_unop :
 183   AST.typ -> AST.typ -> Csyntax.unary_operation ->
 184   FrontEndOps.unary_operation Errors.res
 185
 186 val fix_ptr_type :
 187   Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
 188   Cminor_syntax.expr
 189
 190 val translate_add :
 191   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 192   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 193
 194 val translate_sub :
 195   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 196   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 197
 198 val translate_mul :
 199   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 200   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 201
 202 val translate_div :
 203   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 204   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 205
 206 val translate_mod :
 207   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 208   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 209
 210 val translate_shr :
 211   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 212   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 213
 214 val complete_cmp :
 215   Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 216
 217 val translate_cmp :
 218   Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
 219   Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 220
 221 val translate_misc_aop :
 222   Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
 223   AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
 224   Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
 225
 226 val translate_binop :
 227   Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
 228   Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr
 229   Errors.res
 230
 231 val translate_cast :
 232   Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
 233   Cminor_syntax.expr Types.sig0 Errors.res
 234
 235 val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr
 236
 237 val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr
 238
 239 val translate_addr :
 240   var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
 241
 242 val translate_expr :
 243   var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
 244
 245 type destination =
 246 | IdDest of AST.ident
 247 | MemDest of Cminor_syntax.expr Types.sig0
 248
 249 val destination_rect_Type4 :
 250   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 251   Types.sig0 -> 'a1) -> destination -> 'a1
 252
 253 val destination_rect_Type5 :
 254   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 255   Types.sig0 -> 'a1) -> destination -> 'a1
 256
 257 val destination_rect_Type3 :
 258   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 259   Types.sig0 -> 'a1) -> destination -> 'a1
 260
 261 val destination_rect_Type2 :
 262   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 263   Types.sig0 -> 'a1) -> destination -> 'a1
 264
 265 val destination_rect_Type1 :
 266   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 267   Types.sig0 -> 'a1) -> destination -> 'a1
 268
 269 val destination_rect_Type0 :
 270   var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
 271   Types.sig0 -> 'a1) -> destination -> 'a1
 272
 273 val destination_inv_rect_Type4 :
 274   var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
 275   (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
 276
 277 val destination_inv_rect_Type3 :
 278   var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
 279   (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
 280
 281 val destination_inv_rect_Type2 :
 282   var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
 283   (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
 284
 285 val destination_inv_rect_Type1 :
 286   var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
 287   (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
 288
 289 val destination_inv_rect_Type0 :
 290   var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
 291   (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
 292
 293 val destination_discr :
 294   var_types -> AST.typ -> destination -> destination -> __
 295
 296 val destination_jmdiscr :
 297   var_types -> AST.typ -> destination -> destination -> __
 298
 299 val translate_dest : var_types -> Csyntax.expr -> destination Errors.res
 300
 301 type lenv = PreIdentifiers.identifier Identifiers.identifier_map
 302
 303 val lookup_label :
 304   lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res
 305
 306 type labgen = { labuniverse : Identifiers.universe;
 307                 label_genlist : PreIdentifiers.identifier List.list }
 308
 309 val labgen_rect_Type4 :
 310   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 311   -> labgen -> 'a1
 312
 313 val labgen_rect_Type5 :
 314   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 315   -> labgen -> 'a1
 316
 317 val labgen_rect_Type3 :
 318   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 319   -> labgen -> 'a1
 320
 321 val labgen_rect_Type2 :
 322   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 323   -> labgen -> 'a1
 324
 325 val labgen_rect_Type1 :
 326   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 327   -> labgen -> 'a1
 328
 329 val labgen_rect_Type0 :
 330   (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
 331   -> labgen -> 'a1
 332
 333 val labuniverse : labgen -> Identifiers.universe
 334
 335 val label_genlist : labgen -> PreIdentifiers.identifier List.list
 336
 337 val labgen_inv_rect_Type4 :
 338   labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
 339   __ -> __ -> 'a1) -> 'a1
 340
 341 val labgen_inv_rect_Type3 :
 342   labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
 343   __ -> __ -> 'a1) -> 'a1
 344
 345 val labgen_inv_rect_Type2 :
 346   labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
 347   __ -> __ -> 'a1) -> 'a1
 348
 349 val labgen_inv_rect_Type1 :
 350   labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
 351   __ -> __ -> 'a1) -> 'a1
 352
 353 val labgen_inv_rect_Type0 :
 354   labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
 355   __ -> __ -> 'a1) -> 'a1
 356
 357 val labgen_discr : labgen -> labgen -> __
 358
 359 val labgen_jmdiscr : labgen -> labgen -> __
 360
 361 val generate_fresh_label :
 362   labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0
 363
 364 val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list
 365
 366 val labels_defined : Csyntax.statement -> AST.ident List.list
 367
 368 val m_option_map :
 369   ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res
 370
 371 val translate_expr_sigma :
 372   var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
 373   Types.sig0 Errors.res
 374
 375 val add_tmps :
 376   var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types
 377
 378 type tmpgen = { tmp_universe : Identifiers.universe;
 379                 tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
 380
 381 val tmpgen_rect_Type4 :
 382   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 383   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 384
 385 val tmpgen_rect_Type5 :
 386   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 387   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 388
 389 val tmpgen_rect_Type3 :
 390   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 391   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 392
 393 val tmpgen_rect_Type2 :
 394   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 395   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 396
 397 val tmpgen_rect_Type1 :
 398   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 399   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 400
 401 val tmpgen_rect_Type0 :
 402   var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
 403   List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
 404
 405 val tmp_universe : var_types -> tmpgen -> Identifiers.universe
 406
 407 val tmp_env :
 408   var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list
 409
 410 val tmpgen_inv_rect_Type4 :
 411   var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
 412   Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
 413
 414 val tmpgen_inv_rect_Type3 :
 415   var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
 416   Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
 417
 418 val tmpgen_inv_rect_Type2 :
 419   var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
 420   Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
 421
 422 val tmpgen_inv_rect_Type1 :
 423   var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
 424   Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
 425
 426 val tmpgen_inv_rect_Type0 :
 427   var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
 428   Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
 429
 430 val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __
 431
 432 val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __
 433
 434 val alloc_tmp :
 435   var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod
 436
 437 val mklabels :
 438   labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
 439   Types.prod, labgen) Types.prod
 440
 441 type convert_flag =
 442 | DoNotConvert
 443 | ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
 444
 445 val convert_flag_rect_Type4 :
 446   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 447   convert_flag -> 'a1
 448
 449 val convert_flag_rect_Type5 :
 450   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 451   convert_flag -> 'a1
 452
 453 val convert_flag_rect_Type3 :
 454   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 455   convert_flag -> 'a1
 456
 457 val convert_flag_rect_Type2 :
 458   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 459   convert_flag -> 'a1
 460
 461 val convert_flag_rect_Type1 :
 462   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 463   convert_flag -> 'a1
 464
 465 val convert_flag_rect_Type0 :
 466   'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
 467   convert_flag -> 'a1
 468
 469 val convert_flag_inv_rect_Type4 :
 470   convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
 471   PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
 472
 473 val convert_flag_inv_rect_Type3 :
 474   convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
 475   PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
 476
 477 val convert_flag_inv_rect_Type2 :
 478   convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
 479   PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
 480
 481 val convert_flag_inv_rect_Type1 :
 482   convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
 483   PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
 484
 485 val convert_flag_inv_rect_Type0 :
 486   convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
 487   PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
 488
 489 val convert_flag_discr : convert_flag -> convert_flag -> __
 490
 491 val convert_flag_jmdiscr : convert_flag -> convert_flag -> __
 492
 493 val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list
 494
 495 val translate_statement :
 496   var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
 497   Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
 498   Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res
 499
 500 val alloc_params_main :
 501   var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
 502   Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
 503   ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
 504   ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
 505   Errors.res
 506
 507 val alloc_params :
 508   var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
 509   Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
 510   ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
 511   ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
 512   Errors.res
 513
 514 val populate_lenv :
 515   AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
 516   Types.prod Errors.res
 517
 518 val build_label_env :
 519   Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res
 520
 521 val translate_function :
 522   Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
 523   Types.prod List.list -> Csyntax.function0 ->
 524   Cminor_syntax.internal_function Errors.res
 525
 526 val translate_fundef :
 527   Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
 528   Types.prod List.list -> Csyntax.clight_fundef ->
 529   Cminor_syntax.internal_function AST.fundef Errors.res
 530
 531 val map_partial_All :
 532   ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res
 533
 534 val clight_to_cminor :
 535   Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res
 536