extracted/csem.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open Hide
  12
  13 open ByteValues
  14
  15 open Division
  16
  17 open Z
  18
  19 open BitVectorZ
  20
  21 open Pointers
  22
  23 open GenMem
  24
  25 open FrontEndMem
  26
  27 open Proper
  28
  29 open PositiveMap
  30
  31 open Deqsets
  32
  33 open Extralib
  34
  35 open Lists
  36
  37 open Identifiers
  38
  39 open Exp
  40
  41 open Arithmetic
  42
  43 open Vector
  44
  45 open Div_and_mod
  46
  47 open Util
  48
  49 open FoldStuff
  50
  51 open BitVector
  52
  53 open Extranat
  54
  55 open Integers
  56
  57 open AST
  58
  59 open ErrorMessages
  60
  61 open Option
  62
  63 open Setoids
  64
  65 open Monad
  66
  67 open Jmeq
  68
  69 open Russell
  70
  71 open Positive
  72
  73 open PreIdentifiers
  74
  75 open Bool
  76
  77 open Relations
  78
  79 open Nat
  80
  81 open List
  82
  83 open Hints_declaration
  84
  85 open Core_notation
  86
  87 open Pts
  88
  89 open Logic
  90
  91 open Types
  92
  93 open Errors
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open Csyntax
 100
 101 open Events
 102
 103 open Smallstep
 104
 105 open TypeComparison
 106
 107 open ClassifyOp
 108
 109 val sem_neg : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
 110
 111 val sem_notint : Values.val0 -> Values.val0 Types.option
 112
 113 val sem_notbool : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
 114
 115 val sem_add :
 116   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
 117   Types.option
 118
 119 val sem_sub :
 120   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 121   Csyntax.type0 -> Values.val0 Types.option
 122
 123 val sem_mul :
 124   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
 125   Types.option
 126
 127 val sem_div :
 128   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
 129   Types.option
 130
 131 val sem_mod :
 132   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
 133   Types.option
 134
 135 val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
 136
 137 val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
 138
 139 val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
 140
 141 val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
 142
 143 val sem_shr :
 144   Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
 145   Types.option
 146
 147 val sem_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
 148
 149 val sem_cmp_match : Integers.comparison -> Values.val0 Types.option
 150
 151 val sem_cmp :
 152   Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
 153   Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option
 154
 155 val cast_bool_to_target :
 156   Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option
 157
 158 val sem_unary_operation :
 159   Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
 160   Types.option
 161
 162 val sem_binary_operation :
 163   Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
 164   Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0 Types.option
 165
 166 val cast_int_int :
 167   AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
 168   BitVector.bitVector
 169
 170 type genv = Csyntax.clight_fundef Globalenvs.genv_t
 171
 172 type env = Pointers.block Identifiers.identifier_map
 173
 174 val empty_env : env
 175
 176 val load_value_of_type :
 177   Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
 178   Values.val0 Types.option
 179
 180 val store_value_of_type :
 181   Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
 182   Values.val0 -> GenMem.mem Types.option
 183
 184 val blocks_of_env : env -> Pointers.block List.list
 185
 186 val select_switch :
 187   AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
 188   Csyntax.labeled_statements Types.option
 189
 190 val seq_of_labeled_statement :
 191   Csyntax.labeled_statements -> Csyntax.statement
 192
 193 type cont =
 194 | Kstop
 195 | Kseq of Csyntax.statement * cont
 196 | Kwhile of Csyntax.expr * Csyntax.statement * cont
 197 | Kdowhile of Csyntax.expr * Csyntax.statement * cont
 198 | Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
 199 | Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
 200 | Kswitch of cont
 201 | Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
 202            Types.prod Types.option * Csyntax.function0 * env * cont
 203
 204 val cont_rect_Type4 :
 205   'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 206   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 207   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 208   Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 209   (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 210   'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 211   Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
 212   env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
 213
 214 val cont_rect_Type3 :
 215   'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 216   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 217   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 218   Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 219   (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 220   'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 221   Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
 222   env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
 223
 224 val cont_rect_Type2 :
 225   'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 226   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 227   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 228   Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 229   (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 230   'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 231   Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
 232   env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
 233
 234 val cont_rect_Type1 :
 235   'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 236   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 237   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 238   Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 239   (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 240   'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 241   Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
 242   env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
 243
 244 val cont_rect_Type0 :
 245   'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 246   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 247   Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 248   Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 249   (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 250   'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 251   Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
 252   env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
 253
 254 val cont_inv_rect_Type4 :
 255   cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 256   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 257   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 258   'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
 259   (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
 260   Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
 261   'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 262   Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
 263   -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 264
 265 val cont_inv_rect_Type3 :
 266   cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 267   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 268   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 269   'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
 270   (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
 271   Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
 272   'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 273   Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
 274   -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 275
 276 val cont_inv_rect_Type2 :
 277   cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 278   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 279   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 280   'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
 281   (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
 282   Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
 283   'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 284   Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
 285   -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 286
 287 val cont_inv_rect_Type1 :
 288   cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 289   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 290   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 291   'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
 292   (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
 293   Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
 294   'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 295   Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
 296   -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 297
 298 val cont_inv_rect_Type0 :
 299   cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 300   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 301   'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 302   'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
 303   (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
 304   Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
 305   'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 306   Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
 307   -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 308
 309 val cont_discr : cont -> cont -> __
 310
 311 val cont_jmdiscr : cont -> cont -> __
 312
 313 val call_cont : cont -> cont
 314
 315 type state =
 316 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
 317 | Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
 318    * cont * GenMem.mem
 319 | Returnstate of Values.val0 * cont * GenMem.mem
 320 | Finalstate of Integers.int
 321
 322 val state_rect_Type4 :
 323   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 324   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 325   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 326   (Integers.int -> 'a1) -> state -> 'a1
 327
 328 val state_rect_Type5 :
 329   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 330   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 331   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 332   (Integers.int -> 'a1) -> state -> 'a1
 333
 334 val state_rect_Type3 :
 335   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 336   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 337   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 338   (Integers.int -> 'a1) -> state -> 'a1
 339
 340 val state_rect_Type2 :
 341   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 342   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 343   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 344   (Integers.int -> 'a1) -> state -> 'a1
 345
 346 val state_rect_Type1 :
 347   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 348   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 349   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 350   (Integers.int -> 'a1) -> state -> 'a1
 351
 352 val state_rect_Type0 :
 353   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
 354   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
 355   cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
 356   (Integers.int -> 'a1) -> state -> 'a1
 357
 358 val state_inv_rect_Type4 :
 359   state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
 360   GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
 361   Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
 362   -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
 363
 364 val state_inv_rect_Type3 :
 365   state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
 366   GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
 367   Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
 368   -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
 369
 370 val state_inv_rect_Type2 :
 371   state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
 372   GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
 373   Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
 374   -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
 375
 376 val state_inv_rect_Type1 :
 377   state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
 378   GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
 379   Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
 380   -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
 381
 382 val state_inv_rect_Type0 :
 383   state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
 384   GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
 385   Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
 386   -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
 387
 388 val state_discr : state -> state -> __
 389
 390 val state_jmdiscr : state -> state -> __
 391
 392 val find_label_ls :
 393   Csyntax.label -> Csyntax.labeled_statements -> cont -> (Csyntax.statement,
 394   cont) Types.prod Types.option
 395
 396 val find_label :
 397   Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
 398   Types.prod Types.option
 399
 400 val fun_typeof : Csyntax.expr -> Csyntax.type0
 401