extracted/rTLabsToRTL.mli

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open Graphs
   6
   7 open Order
   8
   9 open Registers
  10
  11 open FrontEndVal
  12
  13 open Hide
  14
  15 open ByteValues
  16
  17 open GenMem
  18
  19 open FrontEndMem
  20
  21 open Division
  22
  23 open Z
  24
  25 open BitVectorZ
  26
  27 open Pointers
  28
  29 open Coqlib
  30
  31 open Values
  32
  33 open FrontEndOps
  34
  35 open CostLabel
  36
  37 open Proper
  38
  39 open PositiveMap
  40
  41 open Deqsets
  42
  43 open ErrorMessages
  44
  45 open PreIdentifiers
  46
  47 open Errors
  48
  49 open Extralib
  50
  51 open Lists
  52
  53 open Positive
  54
  55 open Identifiers
  56
  57 open Exp
  58
  59 open Arithmetic
  60
  61 open Vector
  62
  63 open Div_and_mod
  64
  65 open Util
  66
  67 open FoldStuff
  68
  69 open BitVector
  70
  71 open Jmeq
  72
  73 open Russell
  74
  75 open List
  76
  77 open Setoids
  78
  79 open Monad
  80
  81 open Option
  82
  83 open Extranat
  84
  85 open Bool
  86
  87 open Relations
  88
  89 open Nat
  90
  91 open Integers
  92
  93 open Types
  94
  95 open AST
  96
  97 open Hints_declaration
  98
  99 open Core_notation
 100
 101 open Pts
 102
 103 open Logic
 104
 105 open RTLabs_syntax
 106
 107 open Extra_bool
 108
 109 open Globalenvs
 110
 111 open String
 112
 113 open Sets
 114
 115 open Listb
 116
 117 open LabelledObjects
 118
 119 open I8051
 120
 121 open BackEndOps
 122
 123 open Joint
 124
 125 open RTL
 126
 127 open Deqsets_extra
 128
 129 open State
 130
 131 open Bind_new
 132
 133 open BindLists
 134
 135 open Blocks
 136
 137 open TranslateUtils
 138
 139 val size_of_sig_type : AST.typ -> Nat.nat
 140
 141 val sign_of_sig_type : AST.typ -> AST.signedness
 142
 143 type register_type =
 144 | Register_int of Registers.register
 145 | Register_ptr of Registers.register * Registers.register
 146
 147 val register_type_rect_Type4 :
 148   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 149   'a1) -> register_type -> 'a1
 150
 151 val register_type_rect_Type5 :
 152   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 153   'a1) -> register_type -> 'a1
 154
 155 val register_type_rect_Type3 :
 156   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 157   'a1) -> register_type -> 'a1
 158
 159 val register_type_rect_Type2 :
 160   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 161   'a1) -> register_type -> 'a1
 162
 163 val register_type_rect_Type1 :
 164   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 165   'a1) -> register_type -> 'a1
 166
 167 val register_type_rect_Type0 :
 168   (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
 169   'a1) -> register_type -> 'a1
 170
 171 val register_type_inv_rect_Type4 :
 172   register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 173   -> Registers.register -> __ -> 'a1) -> 'a1
 174
 175 val register_type_inv_rect_Type3 :
 176   register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 177   -> Registers.register -> __ -> 'a1) -> 'a1
 178
 179 val register_type_inv_rect_Type2 :
 180   register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 181   -> Registers.register -> __ -> 'a1) -> 'a1
 182
 183 val register_type_inv_rect_Type1 :
 184   register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 185   -> Registers.register -> __ -> 'a1) -> 'a1
 186
 187 val register_type_inv_rect_Type0 :
 188   register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 189   -> Registers.register -> __ -> 'a1) -> 'a1
 190
 191 val register_type_discr : register_type -> register_type -> __
 192
 193 val register_type_jmdiscr : register_type -> register_type -> __
 194
 195 type local_env = Registers.register List.list Identifiers.identifier_map
 196
 197 val find_local_env :
 198   PreIdentifiers.identifier -> local_env -> Registers.register List.list
 199
 200 val find_local_env_arg :
 201   Registers.register -> local_env -> Joint.psd_argument List.list
 202
 203 val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __
 204
 205 val fresh_registers :
 206   Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
 207   List.list Monad.smax_def__o__monad
 208
 209 val map_list_local_env :
 210   Registers.register List.list Identifiers.identifier_map ->
 211   (Registers.register, AST.typ) Types.prod List.list -> Registers.register
 212   List.list
 213
 214 val initialize_local_env :
 215   AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
 216   -> local_env Monad.smax_def__o__monad
 217
 218 val initialize_locals_params_ret :
 219   AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
 220   -> (Registers.register, AST.typ) Types.prod List.list ->
 221   (Registers.register, AST.typ) Types.prod Types.option -> local_env
 222   Monad.smax_def__o__monad
 223
 224 val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod
 225
 226 val find_and_addr :
 227   PreIdentifiers.identifier -> local_env -> (Registers.register,
 228   Registers.register) Types.prod
 229
 230 val find_and_addr_arg :
 231   Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument)
 232   Types.prod
 233
 234 val rtl_args :
 235   Registers.register List.list -> local_env -> Joint.psd_argument List.list
 236
 237 val vrsplit :
 238   Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
 239   Types.sig0
 240
 241 val split_into_bytes :
 242   AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0
 243
 244 val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
 245
 246 val translate_op_aux :
 247   AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 248   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 249   Joint.joint_seq List.list
 250
 251 val translate_op :
 252   AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 253   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 254   Joint.joint_seq List.list
 255
 256 val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
 257
 258 val translate_op_asym_unsigned :
 259   AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 260   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 261   Joint.joint_seq List.list
 262
 263 val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
 264
 265 val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
 266
 267 val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
 268
 269 val translate_cst :
 270   AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
 271   Registers.register List.list -> (Registers.register, Joint.joint_seq
 272   List.list) Bind_new.bind_new
 273
 274 val translate_move :
 275   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 276   List.list -> Joint.joint_seq List.list
 277
 278 val sign_mask :
 279   AST.ident List.list -> Registers.register -> Joint.psd_argument ->
 280   Joint.joint_seq List.list
 281
 282 val translate_cast_signed :
 283   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 284   -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 285
 286 val translate_fill_with_zero :
 287   AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 288   List.list
 289
 290 val last : 'a1 List.list -> 'a1 Types.option
 291
 292 val translate_op_asym_signed :
 293   AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 294   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 295   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 296
 297 val translate_cast :
 298   AST.ident List.list -> AST.signedness -> Registers.register List.list ->
 299   Registers.register List.list -> (Registers.register, Joint.joint_seq
 300   List.list) Bind_new.bind_new
 301
 302 val translate_notint :
 303   AST.ident List.list -> Registers.register List.list -> Registers.register
 304   List.list -> Joint.joint_seq List.list
 305
 306 val translate_negint :
 307   AST.ident List.list -> Registers.register List.list -> Registers.register
 308   List.list -> Joint.joint_seq List.list
 309
 310 val translate_notbool :
 311   AST.ident List.list -> Registers.register List.list -> Registers.register
 312   List.list -> (Registers.register, Joint.joint_seq List.list)
 313   Bind_new.bind_new
 314
 315 val translate_op1 :
 316   AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 317   Registers.register List.list -> Registers.register List.list ->
 318   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 319
 320 val translate_mul_i :
 321   AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
 322   -> Registers.register List.list -> Joint.psd_argument List.list ->
 323   Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
 324   Joint.joint_seq List.list -> Joint.joint_seq List.list
 325
 326 val translate_mul :
 327   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 328   List.list -> Joint.psd_argument List.list -> (Registers.register,
 329   Joint.joint_seq List.list) Bind_new.bind_new
 330
 331 val translate_divumodu8 :
 332   AST.ident List.list -> Bool.bool -> Registers.register List.list ->
 333   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 334   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 335
 336 val foldr2 :
 337   ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
 338
 339 val translate_ne :
 340   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 341   List.list -> Joint.psd_argument List.list -> (Registers.register,
 342   Joint.joint_seq List.list) Bind_new.bind_new
 343
 344 val translate_toggle_bool :
 345   AST.ident List.list -> Registers.register List.list -> (Registers.register,
 346   Joint.joint_seq List.list) Bind_new.bind_new
 347
 348 val translate_lt_unsigned :
 349   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 350   List.list -> Joint.psd_argument List.list -> (Registers.register,
 351   Joint.joint_seq List.list) Bind_new.bind_new
 352
 353 val shift_signed :
 354   AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
 355   -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
 356   Types.sig0
 357
 358 val translate_lt_signed :
 359   AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 360   List.list -> Joint.psd_argument List.list -> (Registers.register,
 361   Joint.joint_seq List.list) Bind_new.bind_new
 362
 363 val translate_lt :
 364   Bool.bool -> AST.ident List.list -> Registers.register List.list ->
 365   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 366   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 367
 368 val translate_cmp :
 369   Bool.bool -> AST.ident List.list -> Integers.comparison ->
 370   Registers.register List.list -> Joint.psd_argument List.list ->
 371   Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
 372   BindLists.bind_list
 373
 374 val translate_op2 :
 375   AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
 376   FrontEndOps.binary_operation -> Registers.register List.list ->
 377   Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 378   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 379
 380 val translate_cond :
 381   AST.ident List.list -> Registers.register List.list -> Graphs.label ->
 382   Blocks.bind_step_block
 383
 384 val translate_load :
 385   AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
 386   List.list -> (Registers.register, Joint.joint_seq List.list)
 387   Bind_new.bind_new
 388
 389 val translate_store :
 390   AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
 391   List.list -> (Registers.register, Joint.joint_seq List.list)
 392   Bind_new.bind_new
 393
 394 val ensure_bind_step_block :
 395   Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
 396   List.list) Bind_new.bind_new -> Blocks.bind_step_block
 397
 398 val translate_statement :
 399   AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
 400   -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
 401   Blocks.bind_fin_block) Types.sum, __) Types.dPair
 402
 403 val translate_internal :
 404   AST.ident List.list -> RTLabs_syntax.internal_function ->
 405   Joint.joint_closed_internal_function
 406
 407 val rtlabs_to_rtl :
 408   CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program
 409