extracted/cminor_semantics.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Extralib
  12
  13 open Lists
  14
  15 open Identifiers
  16
  17 open Integers
  18
  19 open AST
  20
  21 open Division
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open FoldStuff
  32
  33 open BitVector
  34
  35 open Z
  36
  37 open BitVectorZ
  38
  39 open Pointers
  40
  41 open ErrorMessages
  42
  43 open Option
  44
  45 open Setoids
  46
  47 open Monad
  48
  49 open Positive
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Div_and_mod
  56
  57 open Jmeq
  58
  59 open Russell
  60
  61 open Util
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open List
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Coqlib
  82
  83 open Values
  84
  85 open Events
  86
  87 open FrontEndVal
  88
  89 open Hide
  90
  91 open ByteValues
  92
  93 open GenMem
  94
  95 open FrontEndMem
  96
  97 open IOMonad
  98
  99 open IO
 100
 101 open Extra_bool
 102
 103 open Globalenvs
 104
 105 open SmallstepExec
 106
 107 open FrontEndOps
 108
 109 open Cminor_syntax
 110
 111 type env = Values.val0 Identifiers.identifier_map
 112
 113 type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
 114
 115 type cont =
 116 | Kend
 117 | Kseq of Cminor_syntax.stmt * cont
 118 | Kblock of cont
 119
 120 val cont_rect_Type4 :
 121   'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 122   -> cont -> 'a1
 123
 124 val cont_rect_Type3 :
 125   'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 126   -> cont -> 'a1
 127
 128 val cont_rect_Type2 :
 129   'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 130   -> cont -> 'a1
 131
 132 val cont_rect_Type1 :
 133   'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 134   -> cont -> 'a1
 135
 136 val cont_rect_Type0 :
 137   'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 138   -> cont -> 'a1
 139
 140 val cont_inv_rect_Type4 :
 141   cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
 142   'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 143
 144 val cont_inv_rect_Type3 :
 145   cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
 146   'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 147
 148 val cont_inv_rect_Type2 :
 149   cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
 150   'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 151
 152 val cont_inv_rect_Type1 :
 153   cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
 154   'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 155
 156 val cont_inv_rect_Type0 :
 157   cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
 158   'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 159
 160 val cont_discr : cont -> cont -> __
 161
 162 val cont_jmdiscr : cont -> cont -> __
 163
 164 type stack =
 165 | SStop
 166 | Scall of (AST.ident, AST.typ) Types.prod Types.option
 167    * Cminor_syntax.internal_function * Pointers.block * env * cont *
 168    stack
 169
 170 val stack_rect_Type4 :
 171   'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 172   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 173   cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
 174
 175 val stack_rect_Type3 :
 176   'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 177   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 178   cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
 179
 180 val stack_rect_Type2 :
 181   'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 182   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 183   cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
 184
 185 val stack_rect_Type1 :
 186   'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 187   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 188   cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
 189
 190 val stack_rect_Type0 :
 191   'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 192   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 193   cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
 194
 195 val stack_inv_rect_Type4 :
 196   stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 197   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 198   cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 199
 200 val stack_inv_rect_Type3 :
 201   stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 202   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 203   cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 204
 205 val stack_inv_rect_Type2 :
 206   stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 207   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 208   cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 209
 210 val stack_inv_rect_Type1 :
 211   stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 212   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 213   cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 214
 215 val stack_inv_rect_Type0 :
 216   stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 217   Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 218   cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 219
 220 val stack_jmdiscr : stack -> stack -> __
 221
 222 type state =
 223 | State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
 224    * GenMem.mem * Pointers.block * cont * stack
 225 | Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
 226    * Values.val0 List.list * GenMem.mem * stack
 227 | Returnstate of Values.val0 Types.option * GenMem.mem * stack
 228 | Finalstate of Integers.int
 229
 230 val state_rect_Type4 :
 231   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 232   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 233   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 234   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 235   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 236
 237 val state_rect_Type5 :
 238   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 239   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 240   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 241   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 242   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 243
 244 val state_rect_Type3 :
 245   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 246   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 247   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 248   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 249   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 250
 251 val state_rect_Type2 :
 252   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 253   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 254   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 255   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 256   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 257
 258 val state_rect_Type1 :
 259   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 260   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 261   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 262   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 263   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 264
 265 val state_rect_Type0 :
 266   (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 267   -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 268   (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 269   List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 270   GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 271
 272 val state_inv_rect_Type4 :
 273   state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 274   __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 275   'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 276   Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
 277   Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
 278   'a1) -> 'a1
 279
 280 val state_inv_rect_Type3 :
 281   state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 282   __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 283   'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 284   Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
 285   Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
 286   'a1) -> 'a1
 287
 288 val state_inv_rect_Type2 :
 289   state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 290   __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 291   'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 292   Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
 293   Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
 294   'a1) -> 'a1
 295
 296 val state_inv_rect_Type1 :
 297   state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 298   __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 299   'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 300   Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
 301   Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
 302   'a1) -> 'a1
 303
 304 val state_inv_rect_Type0 :
 305   state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 306   __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 307   'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 308   Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
 309   Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
 310   'a1) -> 'a1
 311
 312 val state_jmdiscr : state -> state -> __
 313
 314 val eval_expr :
 315   genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
 316   GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res
 317
 318 val k_exit :
 319   Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
 320   Types.sig0 Errors.res
 321
 322 val find_case :
 323   AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1 ->
 324   'a1
 325
 326 val find_label :
 327   PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
 328   Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
 329   Types.prod Types.sig0 Types.option
 330
 331 val find_label_always :
 332   PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
 333   Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
 334   Types.prod Types.sig0
 335
 336 val bind_params :
 337   Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
 338   Types.sig0 Errors.res
 339
 340 val init_locals : env -> (AST.ident, AST.typ) Types.prod List.list -> env
 341
 342 val trace_map_inv :
 343   ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
 344   -> (Events.trace, 'a2 List.list) Types.prod Errors.res
 345
 346 val eval_step :
 347   genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
 348   IOMonad.iO
 349
 350 val is_final : state -> Integers.int Types.option
 351
 352 val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
 353
 354 val make_global : Cminor_syntax.cminor_program -> genv
 355
 356 val make_initial_state : Cminor_syntax.cminor_program -> state Errors.res
 357
 358 val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
 359
 360 val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv
 361
 362 val make_initial_noinit_state :
 363   Cminor_syntax.cminor_noinit_program -> state Errors.res
 364
 365 val cminor_noinit_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
 366