extracted/lINToASM.mli

   1 open Preamble
   2
   3 open Deqsets
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open BitVector
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open BitVectorTrie
  46
  47 open BitVectorTrieSet
  48
  49 open State
  50
  51 open String
  52
  53 open Exp
  54
  55 open Arithmetic
  56
  57 open Integers
  58
  59 open AST
  60
  61 open LabelledObjects
  62
  63 open Proper
  64
  65 open PositiveMap
  66
  67 open ErrorMessages
  68
  69 open PreIdentifiers
  70
  71 open Errors
  72
  73 open Extralib
  74
  75 open Lists
  76
  77 open Positive
  78
  79 open Identifiers
  80
  81 open CostLabel
  82
  83 open ASM
  84
  85 open Extra_bool
  86
  87 open Coqlib
  88
  89 open Values
  90
  91 open FrontEndVal
  92
  93 open GenMem
  94
  95 open FrontEndMem
  96
  97 open Globalenvs
  98
  99 open Sets
 100
 101 open Listb
 102
 103 open Graphs
 104
 105 open I8051
 106
 107 open Order
 108
 109 open Registers
 110
 111 open Hide
 112
 113 open Division
 114
 115 open Z
 116
 117 open BitVectorZ
 118
 119 open Pointers
 120
 121 open ByteValues
 122
 123 open BackEndOps
 124
 125 open Joint
 126
 127 open Joint_LTL_LIN
 128
 129 open LIN
 130
 131 type aSM_universe = { id_univ : Identifiers.universe;
 132                       current_funct : AST.ident;
 133                       ident_map : ASM.identifier Identifiers.identifier_map;
 134                       label_map : ASM.identifier Identifiers.identifier_map
 135                                   Identifiers.identifier_map;
 136                       fresh_cost_label : Positive.pos }
 137
 138 val aSM_universe_rect_Type4 :
 139   (Identifiers.universe -> AST.ident -> ASM.identifier
 140   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 141   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 142
 143 val aSM_universe_rect_Type5 :
 144   (Identifiers.universe -> AST.ident -> ASM.identifier
 145   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 146   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 147
 148 val aSM_universe_rect_Type3 :
 149   (Identifiers.universe -> AST.ident -> ASM.identifier
 150   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 151   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 152
 153 val aSM_universe_rect_Type2 :
 154   (Identifiers.universe -> AST.ident -> ASM.identifier
 155   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 156   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 157
 158 val aSM_universe_rect_Type1 :
 159   (Identifiers.universe -> AST.ident -> ASM.identifier
 160   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 161   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 162
 163 val aSM_universe_rect_Type0 :
 164   (Identifiers.universe -> AST.ident -> ASM.identifier
 165   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 166   Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
 167
 168 val id_univ : aSM_universe -> Identifiers.universe
 169
 170 val current_funct : aSM_universe -> AST.ident
 171
 172 val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map
 173
 174 val label_map :
 175   aSM_universe -> ASM.identifier Identifiers.identifier_map
 176   Identifiers.identifier_map
 177
 178 val fresh_cost_label : aSM_universe -> Positive.pos
 179
 180 val aSM_universe_inv_rect_Type4 :
 181   aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 182   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 183   Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
 184
 185 val aSM_universe_inv_rect_Type3 :
 186   aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 187   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 188   Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
 189
 190 val aSM_universe_inv_rect_Type2 :
 191   aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 192   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 193   Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
 194
 195 val aSM_universe_inv_rect_Type1 :
 196   aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 197   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 198   Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
 199
 200 val aSM_universe_inv_rect_Type0 :
 201   aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 202   Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 203   Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
 204
 205 val aSM_universe_discr : aSM_universe -> aSM_universe -> __
 206
 207 val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __
 208
 209 val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad
 210
 211 val identifier_of_label :
 212   Graphs.label -> ASM.identifier Monad.smax_def__o__monad
 213
 214 val identifier_of_ident :
 215   AST.ident -> ASM.identifier Monad.smax_def__o__monad
 216
 217 val new_ASM_universe : Joint.joint_program -> aSM_universe
 218
 219 val start_funct_translation :
 220   AST.ident List.list -> AST.ident List.list -> (AST.ident,
 221   Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad
 222
 223 val aSM_fresh : ASM.identifier Monad.smax_def__o__monad
 224
 225 val register_address : I8051.register -> ASM.subaddressing_mode
 226
 227 val vector_cast :
 228   Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
 229
 230 val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
 231
 232 type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
 233
 234 val data_of_int : BitVector.byte -> ASM.addressing_mode
 235
 236 val data16_of_int : Nat.nat -> ASM.addressing_mode
 237
 238 val accumulator_address : ASM.addressing_mode
 239
 240 val asm_other_bit : ASM.addressing_mode
 241
 242 val one_word : BitVector.word
 243
 244 val translate_statements :
 245   AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
 246   Monad.smax_def__o__monad
 247
 248 val build_translated_statement : AST.ident List.list -> lin_statement -> __
 249
 250 val translate_code : AST.ident List.list -> lin_statement List.list -> __
 251
 252 val translate_fun_def :
 253   AST.ident List.list -> AST.ident List.list -> (AST.ident,
 254   Joint.joint_function) Types.prod -> __
 255
 256 type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
 257                       actual_dptr : (ASM.identifier, Z.z) Types.prod;
 258                       built_code : ASM.labelled_instruction List.list
 259                                    List.list;
 260                       built_preamble : (ASM.identifier, BitVector.word)
 261                                        Types.prod List.list }
 262
 263 val init_mutable_rect_Type4 :
 264   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 265   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 266   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 267
 268 val init_mutable_rect_Type5 :
 269   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 270   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 271   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 272
 273 val init_mutable_rect_Type3 :
 274   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 275   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 276   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 277
 278 val init_mutable_rect_Type2 :
 279   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 280   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 281   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 282
 283 val init_mutable_rect_Type1 :
 284   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 285   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 286   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 287
 288 val init_mutable_rect_Type0 :
 289   ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
 290   ASM.labelled_instruction List.list List.list -> (ASM.identifier,
 291   BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
 292
 293 val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
 294
 295 val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
 296
 297 val built_code : init_mutable -> ASM.labelled_instruction List.list List.list
 298
 299 val built_preamble :
 300   init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list
 301
 302 val init_mutable_inv_rect_Type4 :
 303   init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
 304   Types.prod -> ASM.labelled_instruction List.list List.list ->
 305   (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
 306
 307 val init_mutable_inv_rect_Type3 :
 308   init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
 309   Types.prod -> ASM.labelled_instruction List.list List.list ->
 310   (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
 311
 312 val init_mutable_inv_rect_Type2 :
 313   init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
 314   Types.prod -> ASM.labelled_instruction List.list List.list ->
 315   (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
 316
 317 val init_mutable_inv_rect_Type1 :
 318   init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
 319   Types.prod -> ASM.labelled_instruction List.list List.list ->
 320   (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
 321
 322 val init_mutable_inv_rect_Type0 :
 323   init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
 324   Types.prod -> ASM.labelled_instruction List.list List.list ->
 325   (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
 326
 327 val init_mutable_discr : init_mutable -> init_mutable -> __
 328
 329 val init_mutable_jmdiscr : init_mutable -> init_mutable -> __
 330
 331 val store_byte_or_Identifier :
 332   (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
 333   init_mutable -> init_mutable
 334
 335 val do_store_init_data :
 336   init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
 337   Monad.smax_def__o__monad
 338
 339 val do_store_global :
 340   init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
 341   Types.prod, AST.init_data List.list) Types.prod -> init_mutable
 342   Monad.smax_def__o__monad
 343
 344 val reversed_flatten_aux :
 345   'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list
 346
 347 val translate_premain :
 348   LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
 349   (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
 350   Monad.smax_def__o__monad
 351
 352 val get_symboltable :
 353   (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad
 354
 355 val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
 356