extracted/rTL_semantics.mli

   1 open Preamble
   2
   3 open ExtraMonads
   4
   5 open Deqsets_extra
   6
   7 open State
   8
   9 open Bind_new
  10
  11 open BindLists
  12
  13 open Blocks
  14
  15 open TranslateUtils
  16
  17 open ExtraGlobalenvs
  18
  19 open I8051bis
  20
  21 open String
  22
  23 open Sets
  24
  25 open Listb
  26
  27 open LabelledObjects
  28
  29 open BitVectorTrie
  30
  31 open Graphs
  32
  33 open I8051
  34
  35 open Order
  36
  37 open Registers
  38
  39 open BackEndOps
  40
  41 open Joint
  42
  43 open BEMem
  44
  45 open CostLabel
  46
  47 open Events
  48
  49 open IOMonad
  50
  51 open IO
  52
  53 open Extra_bool
  54
  55 open Coqlib
  56
  57 open Values
  58
  59 open FrontEndVal
  60
  61 open Hide
  62
  63 open ByteValues
  64
  65 open Division
  66
  67 open Z
  68
  69 open BitVectorZ
  70
  71 open Pointers
  72
  73 open GenMem
  74
  75 open FrontEndMem
  76
  77 open Proper
  78
  79 open PositiveMap
  80
  81 open Deqsets
  82
  83 open Extralib
  84
  85 open Lists
  86
  87 open Identifiers
  88
  89 open Exp
  90
  91 open Arithmetic
  92
  93 open Vector
  94
  95 open Div_and_mod
  96
  97 open Util
  98
  99 open FoldStuff
 100
 101 open BitVector
 102
 103 open Extranat
 104
 105 open Integers
 106
 107 open AST
 108
 109 open ErrorMessages
 110
 111 open Option
 112
 113 open Setoids
 114
 115 open Monad
 116
 117 open Jmeq
 118
 119 open Russell
 120
 121 open Positive
 122
 123 open PreIdentifiers
 124
 125 open Bool
 126
 127 open Relations
 128
 129 open Nat
 130
 131 open List
 132
 133 open Hints_declaration
 134
 135 open Core_notation
 136
 137 open Pts
 138
 139 open Logic
 140
 141 open Types
 142
 143 open Errors
 144
 145 open Globalenvs
 146
 147 open Joint_semantics
 148
 149 open SemanticsUtils
 150
 151 open RTL
 152
 153 type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
 154                 stackp : ByteValues.xpointer }
 155
 156 val reg_sp_rect_Type4 :
 157   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 158   -> reg_sp -> 'a1
 159
 160 val reg_sp_rect_Type5 :
 161   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 162   -> reg_sp -> 'a1
 163
 164 val reg_sp_rect_Type3 :
 165   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 166   -> reg_sp -> 'a1
 167
 168 val reg_sp_rect_Type2 :
 169   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 170   -> reg_sp -> 'a1
 171
 172 val reg_sp_rect_Type1 :
 173   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 174   -> reg_sp -> 'a1
 175
 176 val reg_sp_rect_Type0 :
 177   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
 178   -> reg_sp -> 'a1
 179
 180 val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
 181
 182 val stackp : reg_sp -> ByteValues.xpointer
 183
 184 val reg_sp_inv_rect_Type4 :
 185   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 186   ByteValues.xpointer -> __ -> 'a1) -> 'a1
 187
 188 val reg_sp_inv_rect_Type3 :
 189   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 190   ByteValues.xpointer -> __ -> 'a1) -> 'a1
 191
 192 val reg_sp_inv_rect_Type2 :
 193   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 194   ByteValues.xpointer -> __ -> 'a1) -> 'a1
 195
 196 val reg_sp_inv_rect_Type1 :
 197   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 198   ByteValues.xpointer -> __ -> 'a1) -> 'a1
 199
 200 val reg_sp_inv_rect_Type0 :
 201   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 202   ByteValues.xpointer -> __ -> 'a1) -> 'a1
 203
 204 val reg_sp_discr : reg_sp -> reg_sp -> __
 205
 206 val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
 207
 208 val dpi1__o__reg_sp_env__o__inject :
 209   (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
 210   Types.sig0
 211
 212 val eject__o__reg_sp_env__o__inject :
 213   reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
 214
 215 val reg_sp_env__o__inject :
 216   reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
 217
 218 val dpi1__o__reg_sp_env :
 219   (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
 220
 221 val eject__o__reg_sp_env :
 222   reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
 223
 224 val reg_sp_store :
 225   PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
 226
 227 val reg_sp_retrieve :
 228   reg_sp -> Registers.register -> ByteValues.beval Errors.res
 229
 230 val reg_sp_empty : ByteValues.xpointer -> reg_sp
 231
 232 type frame = { fr_ret_regs : Registers.register List.list;
 233                fr_pc : ByteValues.program_counter;
 234                fr_carry : ByteValues.bebit; fr_regs : reg_sp }
 235
 236 val frame_rect_Type4 :
 237   (Registers.register List.list -> ByteValues.program_counter ->
 238   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 239
 240 val frame_rect_Type5 :
 241   (Registers.register List.list -> ByteValues.program_counter ->
 242   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 243
 244 val frame_rect_Type3 :
 245   (Registers.register List.list -> ByteValues.program_counter ->
 246   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 247
 248 val frame_rect_Type2 :
 249   (Registers.register List.list -> ByteValues.program_counter ->
 250   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 251
 252 val frame_rect_Type1 :
 253   (Registers.register List.list -> ByteValues.program_counter ->
 254   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 255
 256 val frame_rect_Type0 :
 257   (Registers.register List.list -> ByteValues.program_counter ->
 258   ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
 259
 260 val fr_ret_regs : frame -> Registers.register List.list
 261
 262 val fr_pc : frame -> ByteValues.program_counter
 263
 264 val fr_carry : frame -> ByteValues.bebit
 265
 266 val fr_regs : frame -> reg_sp
 267
 268 val frame_inv_rect_Type4 :
 269   frame -> (Registers.register List.list -> ByteValues.program_counter ->
 270   ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
 271
 272 val frame_inv_rect_Type3 :
 273   frame -> (Registers.register List.list -> ByteValues.program_counter ->
 274   ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
 275
 276 val frame_inv_rect_Type2 :
 277   frame -> (Registers.register List.list -> ByteValues.program_counter ->
 278   ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
 279
 280 val frame_inv_rect_Type1 :
 281   frame -> (Registers.register List.list -> ByteValues.program_counter ->
 282   ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
 283
 284 val frame_inv_rect_Type0 :
 285   frame -> (Registers.register List.list -> ByteValues.program_counter ->
 286   ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
 287
 288 val frame_discr : frame -> frame -> __
 289
 290 val frame_jmdiscr : frame -> frame -> __
 291
 292 val rTL_state_params : Joint_semantics.sem_state_params
 293
 294 type rTL_state = Joint_semantics.state
 295
 296 val rtl_arg_retrieve :
 297   reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
 298
 299 val rtl_fetch_ra :
 300   rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res
 301
 302 val rtl_init_local : Registers.register -> reg_sp -> reg_sp
 303
 304 val rtl_setup_call_separate :
 305   Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
 306   rTL_state -> rTL_state Errors.res
 307
 308 val rtl_setup_call_separate_overflow :
 309   Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
 310   rTL_state -> rTL_state Errors.res
 311
 312 val rtl_setup_call_unique :
 313   Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
 314   rTL_state -> rTL_state Errors.res
 315
 316 type rTL_state_pc = Joint_semantics.state_pc
 317
 318 val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __
 319
 320 val rtl_fetch_external_args :
 321   AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
 322   Values.val0 List.list Errors.res
 323
 324 val rtl_set_result :
 325   Values.val0 List.list -> Registers.register List.list -> rTL_state ->
 326   rTL_state Errors.res
 327
 328 val rtl_reg_store :
 329   PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
 330   Joint_semantics.state
 331
 332 val rtl_reg_retrieve :
 333   Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res
 334
 335 val rtl_read_result :
 336   Registers.register List.list -> rTL_state -> ByteValues.beval List.list
 337   Errors.res
 338
 339 val rtl_pop_frame_separate :
 340   Registers.register List.list -> rTL_state -> (rTL_state,
 341   ByteValues.program_counter) Types.prod Errors.res
 342
 343 val rtl_pop_frame_unique :
 344   Registers.register List.list -> rTL_state -> (rTL_state,
 345   ByteValues.program_counter) Types.prod Errors.res
 346
 347 val block_of_register_pair :
 348   Registers.register -> Registers.register -> rTL_state -> Pointers.block
 349   Errors.res
 350
 351 val eval_rtl_seq :
 352   RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res
 353
 354 val reg_res_store :
 355   PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
 356   Errors.res
 357
 358 val rTL_semantics_separate : SemanticsUtils.sem_graph_params
 359
 360 val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params
 361
 362 val rTL_semantics_unique : SemanticsUtils.sem_graph_params
 363