extracted/rTLabs_syntax.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Proper
  12
  13 open PositiveMap
  14
  15 open Deqsets
  16
  17 open ErrorMessages
  18
  19 open PreIdentifiers
  20
  21 open Errors
  22
  23 open Extralib
  24
  25 open Lists
  26
  27 open Positive
  28
  29 open Identifiers
  30
  31 open Exp
  32
  33 open Arithmetic
  34
  35 open Vector
  36
  37 open Div_and_mod
  38
  39 open Util
  40
  41 open FoldStuff
  42
  43 open BitVector
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Setoids
  52
  53 open Monad
  54
  55 open Option
  56
  57 open Extranat
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Integers
  66
  67 open Types
  68
  69 open AST
  70
  71 open CostLabel
  72
  73 open FrontEndVal
  74
  75 open Hide
  76
  77 open ByteValues
  78
  79 open GenMem
  80
  81 open FrontEndMem
  82
  83 open Division
  84
  85 open Z
  86
  87 open BitVectorZ
  88
  89 open Pointers
  90
  91 open Coqlib
  92
  93 open Values
  94
  95 open FrontEndOps
  96
  97 open Order
  98
  99 open Registers
 100
 101 open BitVectorTrie
 102
 103 open Graphs
 104
 105 type statement =
 106 | St_skip of Graphs.label
 107 | St_cost of CostLabel.costlabel * Graphs.label
 108 | St_const of AST.typ * Registers.register * FrontEndOps.constant
 109    * Graphs.label
 110 | St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
 111    * Registers.register * Registers.register * Graphs.label
 112 | St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
 113    * Registers.register * Registers.register * Registers.register
 114    * Graphs.label
 115 | St_load of AST.typ * Registers.register * Registers.register * Graphs.label
 116 | St_store of AST.typ * Registers.register * Registers.register
 117    * Graphs.label
 118 | St_call_id of AST.ident * Registers.register List.list
 119    * Registers.register Types.option * Graphs.label
 120 | St_call_ptr of Registers.register * Registers.register List.list
 121    * Registers.register Types.option * Graphs.label
 122 | St_cond of Registers.register * Graphs.label * Graphs.label
 123 | St_return
 124
 125 val statement_rect_Type4 :
 126   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 127   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 128   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 129   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 130   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 131   Registers.register -> Registers.register -> Registers.register ->
 132   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 133   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 134   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 135   (AST.ident -> Registers.register List.list -> Registers.register
 136   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 137   Registers.register List.list -> Registers.register Types.option ->
 138   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 139   -> 'a1) -> 'a1 -> statement -> 'a1
 140
 141 val statement_rect_Type5 :
 142   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 143   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 144   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 145   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 146   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 147   Registers.register -> Registers.register -> Registers.register ->
 148   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 149   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 150   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 151   (AST.ident -> Registers.register List.list -> Registers.register
 152   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 153   Registers.register List.list -> Registers.register Types.option ->
 154   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 155   -> 'a1) -> 'a1 -> statement -> 'a1
 156
 157 val statement_rect_Type3 :
 158   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 159   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 160   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 161   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 162   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 163   Registers.register -> Registers.register -> Registers.register ->
 164   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 165   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 166   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 167   (AST.ident -> Registers.register List.list -> Registers.register
 168   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 169   Registers.register List.list -> Registers.register Types.option ->
 170   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 171   -> 'a1) -> 'a1 -> statement -> 'a1
 172
 173 val statement_rect_Type2 :
 174   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 175   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 176   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 177   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 178   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 179   Registers.register -> Registers.register -> Registers.register ->
 180   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 181   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 182   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 183   (AST.ident -> Registers.register List.list -> Registers.register
 184   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 185   Registers.register List.list -> Registers.register Types.option ->
 186   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 187   -> 'a1) -> 'a1 -> statement -> 'a1
 188
 189 val statement_rect_Type1 :
 190   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 191   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 192   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 193   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 194   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 195   Registers.register -> Registers.register -> Registers.register ->
 196   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 197   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 198   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 199   (AST.ident -> Registers.register List.list -> Registers.register
 200   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 201   Registers.register List.list -> Registers.register Types.option ->
 202   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 203   -> 'a1) -> 'a1 -> statement -> 'a1
 204
 205 val statement_rect_Type0 :
 206   (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 207   (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 208   'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 209   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 210   (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 211   Registers.register -> Registers.register -> Registers.register ->
 212   Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 213   Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 214   Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 215   (AST.ident -> Registers.register List.list -> Registers.register
 216   Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 217   Registers.register List.list -> Registers.register Types.option ->
 218   Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
 219   -> 'a1) -> 'a1 -> statement -> 'a1
 220
 221 val statement_inv_rect_Type4 :
 222   statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 223   Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 224   FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 225   -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
 226   -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
 227   FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
 228   Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
 229   Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 230   (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
 231   -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
 232   Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 233   Registers.register List.list -> Registers.register Types.option ->
 234   Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
 235   Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 236
 237 val statement_inv_rect_Type3 :
 238   statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 239   Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 240   FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 241   -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
 242   -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
 243   FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
 244   Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
 245   Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 246   (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
 247   -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
 248   Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 249   Registers.register List.list -> Registers.register Types.option ->
 250   Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
 251   Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 252
 253 val statement_inv_rect_Type2 :
 254   statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 255   Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 256   FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 257   -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
 258   -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
 259   FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
 260   Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
 261   Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 262   (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
 263   -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
 264   Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 265   Registers.register List.list -> Registers.register Types.option ->
 266   Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
 267   Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 268
 269 val statement_inv_rect_Type1 :
 270   statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 271   Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 272   FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 273   -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
 274   -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
 275   FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
 276   Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
 277   Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 278   (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
 279   -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
 280   Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 281   Registers.register List.list -> Registers.register Types.option ->
 282   Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
 283   Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 284
 285 val statement_inv_rect_Type0 :
 286   statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 287   Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 288   FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 289   -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
 290   -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
 291   FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
 292   Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
 293   Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 294   (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
 295   -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
 296   Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 297   Registers.register List.list -> Registers.register Types.option ->
 298   Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
 299   Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 300
 301 val statement_jmdiscr : statement -> statement -> __
 302
 303 type internal_function = { f_labgen : Identifiers.universe;
 304                            f_reggen : Identifiers.universe;
 305                            f_result : (Registers.register, AST.typ)
 306                                       Types.prod Types.option;
 307                            f_params : (Registers.register, AST.typ)
 308                                       Types.prod List.list;
 309                            f_locals : (Registers.register, AST.typ)
 310                                       Types.prod List.list;
 311                            f_stacksize : Nat.nat;
 312                            f_graph : statement Graphs.graph;
 313                            f_entry : Graphs.label Types.sig0;
 314                            f_exit : Graphs.label Types.sig0 }
 315
 316 val internal_function_rect_Type4 :
 317   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 318   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 319   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 320   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 321   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 322
 323 val internal_function_rect_Type5 :
 324   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 325   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 326   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 327   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 328   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 329
 330 val internal_function_rect_Type3 :
 331   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 332   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 333   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 334   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 335   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 336
 337 val internal_function_rect_Type2 :
 338   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 339   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 340   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 341   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 342   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 343
 344 val internal_function_rect_Type1 :
 345   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 346   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 347   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 348   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 349   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 350
 351 val internal_function_rect_Type0 :
 352   (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 353   AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 354   Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
 355   -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
 356   -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
 357
 358 val f_labgen : internal_function -> Identifiers.universe
 359
 360 val f_reggen : internal_function -> Identifiers.universe
 361
 362 val f_result :
 363   internal_function -> (Registers.register, AST.typ) Types.prod Types.option
 364
 365 val f_params :
 366   internal_function -> (Registers.register, AST.typ) Types.prod List.list
 367
 368 val f_locals :
 369   internal_function -> (Registers.register, AST.typ) Types.prod List.list
 370
 371 val f_stacksize : internal_function -> Nat.nat
 372
 373 val f_graph : internal_function -> statement Graphs.graph
 374
 375 val f_entry : internal_function -> Graphs.label Types.sig0
 376
 377 val f_exit : internal_function -> Graphs.label Types.sig0
 378
 379 val internal_function_inv_rect_Type4 :
 380   internal_function -> (Identifiers.universe -> Identifiers.universe ->
 381   (Registers.register, AST.typ) Types.prod Types.option ->
 382   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 383   AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
 384   __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
 385   'a1) -> 'a1
 386
 387 val internal_function_inv_rect_Type3 :
 388   internal_function -> (Identifiers.universe -> Identifiers.universe ->
 389   (Registers.register, AST.typ) Types.prod Types.option ->
 390   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 391   AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
 392   __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
 393   'a1) -> 'a1
 394
 395 val internal_function_inv_rect_Type2 :
 396   internal_function -> (Identifiers.universe -> Identifiers.universe ->
 397   (Registers.register, AST.typ) Types.prod Types.option ->
 398   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 399   AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
 400   __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
 401   'a1) -> 'a1
 402
 403 val internal_function_inv_rect_Type1 :
 404   internal_function -> (Identifiers.universe -> Identifiers.universe ->
 405   (Registers.register, AST.typ) Types.prod Types.option ->
 406   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 407   AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
 408   __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
 409   'a1) -> 'a1
 410
 411 val internal_function_inv_rect_Type0 :
 412   internal_function -> (Identifiers.universe -> Identifiers.universe ->
 413   (Registers.register, AST.typ) Types.prod Types.option ->
 414   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 415   AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
 416   __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
 417   'a1) -> 'a1
 418
 419 val internal_function_jmdiscr : internal_function -> internal_function -> __
 420
 421 type rTLabs_program =
 422   (internal_function AST.fundef, AST.init_data List.list) AST.program
 423