extracted/rTLabs_semantics.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open ErrorMessages
  22
  23 open Option
  24
  25 open Setoids
  26
  27 open Monad
  28
  29 open Jmeq
  30
  31 open Russell
  32
  33 open Positive
  34
  35 open PreIdentifiers
  36
  37 open Errors
  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 Globalenvs
  96
  97 open CostLabel
  98
  99 open Events
 100
 101 open IOMonad
 102
 103 open IO
 104
 105 open SmallstepExec
 106
 107 open BitVectorTrie
 108
 109 open Graphs
 110
 111 open Order
 112
 113 open Registers
 114
 115 open FrontEndOps
 116
 117 open RTLabs_syntax
 118
 119 type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
 120
 121 type frame = { func : RTLabs_syntax.internal_function;
 122                locals : Values.val0 Registers.register_env;
 123                next : Graphs.label; sp : Pointers.block;
 124                retdst : Registers.register Types.option }
 125
 126 val frame_rect_Type4 :
 127   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 128   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 129   'a1) -> frame -> 'a1
 130
 131 val frame_rect_Type5 :
 132   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 133   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 134   'a1) -> frame -> 'a1
 135
 136 val frame_rect_Type3 :
 137   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 138   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 139   'a1) -> frame -> 'a1
 140
 141 val frame_rect_Type2 :
 142   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 143   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 144   'a1) -> frame -> 'a1
 145
 146 val frame_rect_Type1 :
 147   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 148   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 149   'a1) -> frame -> 'a1
 150
 151 val frame_rect_Type0 :
 152   (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 153   Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
 154   'a1) -> frame -> 'a1
 155
 156 val func : frame -> RTLabs_syntax.internal_function
 157
 158 val locals : frame -> Values.val0 Registers.register_env
 159
 160 val next : frame -> Graphs.label
 161
 162 val sp : frame -> Pointers.block
 163
 164 val retdst : frame -> Registers.register Types.option
 165
 166 val frame_inv_rect_Type4 :
 167   frame -> (RTLabs_syntax.internal_function -> Values.val0
 168   Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 169   Registers.register Types.option -> __ -> 'a1) -> 'a1
 170
 171 val frame_inv_rect_Type3 :
 172   frame -> (RTLabs_syntax.internal_function -> Values.val0
 173   Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 174   Registers.register Types.option -> __ -> 'a1) -> 'a1
 175
 176 val frame_inv_rect_Type2 :
 177   frame -> (RTLabs_syntax.internal_function -> Values.val0
 178   Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 179   Registers.register Types.option -> __ -> 'a1) -> 'a1
 180
 181 val frame_inv_rect_Type1 :
 182   frame -> (RTLabs_syntax.internal_function -> Values.val0
 183   Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 184   Registers.register Types.option -> __ -> 'a1) -> 'a1
 185
 186 val frame_inv_rect_Type0 :
 187   frame -> (RTLabs_syntax.internal_function -> Values.val0
 188   Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 189   Registers.register Types.option -> __ -> 'a1) -> 'a1
 190
 191 val frame_jmdiscr : frame -> frame -> __
 192
 193 val adv : Graphs.label -> frame -> frame
 194
 195 type state =
 196 | State of frame * frame List.list * GenMem.mem
 197 | Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
 198    * Values.val0 List.list * Registers.register Types.option
 199    * frame List.list * GenMem.mem
 200 | Returnstate of Values.val0 Types.option * Registers.register Types.option
 201    * frame List.list * GenMem.mem
 202 | Finalstate of Integers.int
 203
 204 val state_rect_Type4 :
 205   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 206   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 207   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 208   (Values.val0 Types.option -> Registers.register Types.option -> frame
 209   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 210
 211 val state_rect_Type5 :
 212   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 213   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 214   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 215   (Values.val0 Types.option -> Registers.register Types.option -> frame
 216   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 217
 218 val state_rect_Type3 :
 219   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 220   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 221   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 222   (Values.val0 Types.option -> Registers.register Types.option -> frame
 223   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 224
 225 val state_rect_Type2 :
 226   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 227   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 228   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 229   (Values.val0 Types.option -> Registers.register Types.option -> frame
 230   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 231
 232 val state_rect_Type1 :
 233   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 234   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 235   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 236   (Values.val0 Types.option -> Registers.register Types.option -> frame
 237   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 238
 239 val state_rect_Type0 :
 240   (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 241   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 242   Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
 243   (Values.val0 Types.option -> Registers.register Types.option -> frame
 244   List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
 245
 246 val state_inv_rect_Type4 :
 247   state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 248   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 249   List.list -> Registers.register Types.option -> frame List.list ->
 250   GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
 251   Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 252   (Integers.int -> __ -> 'a1) -> 'a1
 253
 254 val state_inv_rect_Type3 :
 255   state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 256   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 257   List.list -> Registers.register Types.option -> frame List.list ->
 258   GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
 259   Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 260   (Integers.int -> __ -> 'a1) -> 'a1
 261
 262 val state_inv_rect_Type2 :
 263   state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 264   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 265   List.list -> Registers.register Types.option -> frame List.list ->
 266   GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
 267   Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 268   (Integers.int -> __ -> 'a1) -> 'a1
 269
 270 val state_inv_rect_Type1 :
 271   state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 272   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 273   List.list -> Registers.register Types.option -> frame List.list ->
 274   GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
 275   Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 276   (Integers.int -> __ -> 'a1) -> 'a1
 277
 278 val state_inv_rect_Type0 :
 279   state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 280   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 281   List.list -> Registers.register Types.option -> frame List.list ->
 282   GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
 283   Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 284   (Integers.int -> __ -> 'a1) -> 'a1
 285
 286 val state_jmdiscr : state -> state -> __
 287
 288 val build_state :
 289   frame -> frame List.list -> GenMem.mem -> Graphs.label -> state
 290
 291 val next_instruction : frame -> RTLabs_syntax.statement
 292
 293 val init_locals :
 294   (Registers.register, AST.typ) Types.prod List.list -> Values.val0
 295   Registers.register_env
 296
 297 val reg_store :
 298   PreIdentifiers.identifier -> Values.val0 -> Values.val0
 299   Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
 300   Errors.res
 301
 302 val params_store :
 303   (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list
 304   -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env
 305   Errors.res
 306
 307 val reg_retrieve :
 308   Values.val0 Registers.register_env -> Registers.register -> Values.val0
 309   Errors.res
 310
 311 val eval_statement :
 312   genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
 313   IOMonad.iO
 314
 315 val rTLabs_is_final : state -> Integers.int Types.option
 316
 317 val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
 318
 319 val make_global : RTLabs_syntax.rTLabs_program -> genv
 320
 321 val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res
 322
 323 val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
 324
 325 val bind_ok :
 326   'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
 327   'a3) -> 'a3
 328
 329 val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
 330
 331 val func_block_of_exec :
 332   genv -> state -> Events.trace -> AST.ident ->
 333   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 334   Registers.register Types.option -> frame List.list -> GenMem.mem ->
 335   Pointers.block Types.sig0
 336