extracted/eRTL_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 ERTL
 152
 153 type ertl_reg_env =
 154   (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
 155   Types.prod
 156
 157 val ps_reg_store :
 158   PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
 159   (ByteValues.beval Identifiers.identifier_map,
 160   SemanticsUtils.hw_register_env) Types.prod Errors.res
 161
 162 val ps_reg_retrieve :
 163   ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res
 164
 165 val hw_reg_store :
 166   I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
 167   Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
 168   Errors.res
 169
 170 val hw_reg_retrieve :
 171   ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res
 172
 173 val ps_arg_retrieve :
 174   ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
 175   Errors.res
 176
 177 val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res
 178
 179 val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env
 180
 181 val eRTL_state : Joint_semantics.sem_state_params
 182
 183 val ertl_eval_move :
 184   ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod ->
 185   __
 186
 187 val ertl_allocate_local :
 188   PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
 189   Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod
 190
 191 val ertl_save_frame :
 192   Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
 193   Joint_semantics.state Errors.res
 194
 195 val ertl_pop_frame :
 196   Joint_semantics.state -> (Joint_semantics.state,
 197   ByteValues.program_counter) Types.prod Errors.res
 198
 199 val ertl_fetch_external_args :
 200   AST.external_function -> Joint_semantics.state -> __ -> Values.val0
 201   List.list Errors.res
 202
 203 val ertl_set_result :
 204   Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
 205   Joint_semantics.state Errors.res
 206
 207 val ps_reg_store_status :
 208   Registers.register -> ByteValues.beval -> Joint_semantics.state ->
 209   Joint_semantics.state Errors.res
 210
 211 val eval_ertl_seq :
 212   AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
 213   AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res
 214
 215 val eRTL_sem_uns : __ Joint_semantics.sem_unserialized_params
 216
 217 val eRTL_semantics : SemanticsUtils.sem_graph_params
 218