extracted/rTLabs_abstract.mli

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open Graphs
   6
   7 open Order
   8
   9 open Registers
  10
  11 open FrontEndOps
  12
  13 open RTLabs_syntax
  14
  15 open SmallstepExec
  16
  17 open CostLabel
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Extra_bool
  26
  27 open Coqlib
  28
  29 open Values
  30
  31 open FrontEndVal
  32
  33 open Hide
  34
  35 open ByteValues
  36
  37 open Division
  38
  39 open Z
  40
  41 open BitVectorZ
  42
  43 open Pointers
  44
  45 open GenMem
  46
  47 open FrontEndMem
  48
  49 open Proper
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open Extralib
  56
  57 open Lists
  58
  59 open Identifiers
  60
  61 open Exp
  62
  63 open Arithmetic
  64
  65 open Vector
  66
  67 open Div_and_mod
  68
  69 open Util
  70
  71 open FoldStuff
  72
  73 open BitVector
  74
  75 open Extranat
  76
  77 open Integers
  78
  79 open AST
  80
  81 open Globalenvs
  82
  83 open ErrorMessages
  84
  85 open Option
  86
  87 open Setoids
  88
  89 open Monad
  90
  91 open Jmeq
  92
  93 open Russell
  94
  95 open Positive
  96
  97 open PreIdentifiers
  98
  99 open Errors
 100
 101 open Bool
 102
 103 open Relations
 104
 105 open Nat
 106
 107 open Hints_declaration
 108
 109 open Core_notation
 110
 111 open Pts
 112
 113 open Logic
 114
 115 open Types
 116
 117 open List
 118
 119 open RTLabs_semantics
 120
 121 type rTLabs_state = RTLabs_semantics.state
 122
 123 type rTLabs_genv = RTLabs_semantics.genv
 124
 125 open Sets
 126
 127 open Listb
 128
 129 open StructuredTraces
 130
 131 open CostSpec
 132
 133 open Deqsets_extra
 134
 135 val status_class_jmdiscr :
 136   StructuredTraces.status_class -> StructuredTraces.status_class -> __
 137
 138 type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
 139                           ras_fn_stack : Pointers.block List.list }
 140
 141 val rTLabs_ext_state_rect_Type4 :
 142   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 143   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 144
 145 val rTLabs_ext_state_rect_Type5 :
 146   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 147   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 148
 149 val rTLabs_ext_state_rect_Type3 :
 150   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 151   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 152
 153 val rTLabs_ext_state_rect_Type2 :
 154   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 155   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 156
 157 val rTLabs_ext_state_rect_Type1 :
 158   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 159   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 160
 161 val rTLabs_ext_state_rect_Type0 :
 162   RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 163   List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
 164
 165 val ras_state :
 166   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
 167
 168 val ras_fn_stack :
 169   RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list
 170
 171 val rTLabs_ext_state_inv_rect_Type4 :
 172   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 173   Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
 174
 175 val rTLabs_ext_state_inv_rect_Type3 :
 176   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 177   Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
 178
 179 val rTLabs_ext_state_inv_rect_Type2 :
 180   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 181   Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
 182
 183 val rTLabs_ext_state_inv_rect_Type1 :
 184   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 185   Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
 186
 187 val rTLabs_ext_state_inv_rect_Type0 :
 188   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 189   Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
 190
 191 val rTLabs_ext_state_discr :
 192   RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
 193
 194 val rTLabs_ext_state_jmdiscr :
 195   RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
 196
 197 val dpi1__o__Ras_state__o__inject :
 198   RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
 199   RTLabs_semantics.state Types.sig0
 200
 201 val eject__o__Ras_state__o__inject :
 202   RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
 203   RTLabs_semantics.state Types.sig0
 204
 205 val ras_state__o__inject :
 206   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
 207   Types.sig0
 208
 209 val dpi1__o__Ras_state :
 210   RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
 211   RTLabs_semantics.state
 212
 213 val eject__o__Ras_state :
 214   RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
 215   RTLabs_semantics.state
 216
 217 val next_state :
 218   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
 219   Events.trace -> rTLabs_ext_state
 220
 221 val rTLabs_classify : RTLabs_semantics.state -> StructuredTraces.status_class
 222
 223 val rTLabs_cost : RTLabs_semantics.state -> Bool.bool
 224
 225 val rTLabs_cost_label :
 226   RTLabs_semantics.state -> CostLabel.costlabel Types.option
 227
 228 type rTLabs_pc =
 229 | Rapc_state of Pointers.block * Graphs.label
 230 | Rapc_call of Graphs.label Types.option * Pointers.block
 231 | Rapc_ret of Pointers.block Types.option
 232 | Rapc_fin
 233
 234 val rTLabs_pc_rect_Type4 :
 235   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 236   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 237   rTLabs_pc -> 'a1
 238
 239 val rTLabs_pc_rect_Type5 :
 240   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 241   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 242   rTLabs_pc -> 'a1
 243
 244 val rTLabs_pc_rect_Type3 :
 245   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 246   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 247   rTLabs_pc -> 'a1
 248
 249 val rTLabs_pc_rect_Type2 :
 250   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 251   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 252   rTLabs_pc -> 'a1
 253
 254 val rTLabs_pc_rect_Type1 :
 255   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 256   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 257   rTLabs_pc -> 'a1
 258
 259 val rTLabs_pc_rect_Type0 :
 260   (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 261   Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 262   rTLabs_pc -> 'a1
 263
 264 val rTLabs_pc_inv_rect_Type4 :
 265   rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
 266   Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
 267   Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 268
 269 val rTLabs_pc_inv_rect_Type3 :
 270   rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
 271   Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
 272   Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 273
 274 val rTLabs_pc_inv_rect_Type2 :
 275   rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
 276   Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
 277   Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 278
 279 val rTLabs_pc_inv_rect_Type1 :
 280   rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
 281   Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
 282   Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 283
 284 val rTLabs_pc_inv_rect_Type0 :
 285   rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
 286   Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
 287   Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 288
 289 val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __
 290
 291 val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __
 292
 293 val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool
 294
 295 val rTLabs_deqset : Deqsets.deqSet
 296
 297 val rTLabs_ext_state_to_pc : RTLabs_semantics.genv -> rTLabs_ext_state -> __
 298
 299 val rTLabs_pc_to_cost_label :
 300   RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
 301   -> CostLabel.costlabel Types.option
 302
 303 val rTLabs_call_ident :
 304   RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident
 305
 306 val rTLabs_status : RTLabs_semantics.genv -> StructuredTraces.abstract_status
 307
 308 val eval_ext_statement :
 309   RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
 310   (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO
 311
 312 val rTLabs_ext_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
 313
 314 val make_ext_initial_state :
 315   RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res
 316
 317 val rTLabs_ext_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
 318