extracted/translateUtils.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 open State
 122
 123 open Bind_new
 124
 125 open BindLists
 126
 127 open Blocks
 128
 129 open Deqsets_extra
 130
 131 val fresh_label :
 132   Joint.params -> AST.ident List.list -> Graphs.label
 133   Monad.smax_def__o__monad
 134
 135 val fresh_register :
 136   Joint.params -> AST.ident List.list -> Registers.register
 137   Monad.smax_def__o__monad
 138
 139 val adds_graph_pre :
 140   Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
 141   Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
 142   Monad.smax_def__o__monad
 143
 144 val adds_graph_post :
 145   Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
 146   Graphs.label -> Graphs.label Monad.smax_def__o__monad
 147
 148 val adds_graph :
 149   Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
 150   Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
 151   Joint.joint_internal_function
 152
 153 val fin_adds_graph :
 154   Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
 155   Graphs.label -> Joint.joint_internal_function ->
 156   Joint.joint_internal_function
 157
 158 val b_adds_graph :
 159   Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
 160   Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
 161   Joint.joint_internal_function
 162
 163 val b_fin_adds_graph :
 164   Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
 165   Graphs.label -> Joint.joint_internal_function ->
 166   Joint.joint_internal_function
 167
 168 val step_registers :
 169   Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
 170   Registers.register List.list
 171
 172 val fin_step_registers :
 173   Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list
 174
 175 type b_graph_translate_data = { init_ret : __; init_params : __;
 176                                 init_stack_size : Nat.nat;
 177                                 added_prologue : Joint.joint_seq List.list;
 178                                 new_regs : Registers.register List.list;
 179                                 f_step : (Graphs.label -> Joint.joint_step ->
 180                                          Blocks.bind_step_block);
 181                                 f_fin : (Graphs.label -> Joint.joint_fin_step
 182                                         -> Blocks.bind_fin_block) }
 183
 184 val b_graph_translate_data_rect_Type4 :
 185   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 186   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 187   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 188   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 189   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 190
 191 val b_graph_translate_data_rect_Type5 :
 192   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 193   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 194   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 195   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 196   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 197
 198 val b_graph_translate_data_rect_Type3 :
 199   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 200   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 201   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 202   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 203   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 204
 205 val b_graph_translate_data_rect_Type2 :
 206   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 207   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 208   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 209   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 210   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 211
 212 val b_graph_translate_data_rect_Type1 :
 213   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 214   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 215   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 216   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 217   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 218
 219 val b_graph_translate_data_rect_Type0 :
 220   Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
 221   __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
 222   -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
 223   (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
 224   -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
 225
 226 val init_ret :
 227   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 228   b_graph_translate_data -> __
 229
 230 val init_params :
 231   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 232   b_graph_translate_data -> __
 233
 234 val init_stack_size :
 235   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 236   b_graph_translate_data -> Nat.nat
 237
 238 val added_prologue :
 239   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 240   b_graph_translate_data -> Joint.joint_seq List.list
 241
 242 val new_regs :
 243   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 244   b_graph_translate_data -> Registers.register List.list
 245
 246 val f_step :
 247   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 248   b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
 249   Blocks.bind_step_block
 250
 251 val f_fin :
 252   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 253   b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
 254   Blocks.bind_fin_block
 255
 256 val b_graph_translate_data_inv_rect_Type4 :
 257   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 258   b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
 259   -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
 260   Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
 261   Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 262
 263 val b_graph_translate_data_inv_rect_Type3 :
 264   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 265   b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
 266   -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
 267   Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
 268   Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 269
 270 val b_graph_translate_data_inv_rect_Type2 :
 271   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 272   b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
 273   -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
 274   Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
 275   Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 276
 277 val b_graph_translate_data_inv_rect_Type1 :
 278   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 279   b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
 280   -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
 281   Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
 282   Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 283
 284 val b_graph_translate_data_inv_rect_Type0 :
 285   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 286   b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
 287   -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
 288   Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
 289   Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 290
 291 val b_graph_translate_data_jmdiscr :
 292   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 293   b_graph_translate_data -> b_graph_translate_data -> __
 294
 295 type bound_b_graph_translate_data =
 296   (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
 297
 298 val get_first_costlabel_next :
 299   Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
 300   -> (CostLabel.costlabel, __) Types.prod
 301
 302 val get_first_costlabel :
 303   Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
 304   -> CostLabel.costlabel
 305
 306 val not_emptyb : 'a1 List.list -> Bool.bool
 307
 308 val b_graph_translate_props_rect_Type4 :
 309   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 310   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 311   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 312   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 313   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 314
 315 val b_graph_translate_props_rect_Type5 :
 316   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 317   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 318   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 319   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 320   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 321
 322 val b_graph_translate_props_rect_Type3 :
 323   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 324   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 325   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 326   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 327   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 328
 329 val b_graph_translate_props_rect_Type2 :
 330   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 331   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 332   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 333   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 334   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 335
 336 val b_graph_translate_props_rect_Type1 :
 337   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 338   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 339   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 340   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 341   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 342
 343 val b_graph_translate_props_rect_Type0 :
 344   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 345   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 346   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 347   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 348   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 349
 350 val b_graph_translate_props_inv_rect_Type4 :
 351   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 352   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 353   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 354   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 355   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 356
 357 val b_graph_translate_props_inv_rect_Type3 :
 358   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 359   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 360   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 361   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 362   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 363
 364 val b_graph_translate_props_inv_rect_Type2 :
 365   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 366   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 367   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 368   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 369   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 370
 371 val b_graph_translate_props_inv_rect_Type1 :
 372   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 373   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 374   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 375   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 376   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 377
 378 val b_graph_translate_props_inv_rect_Type0 :
 379   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 380   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 381   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 382   List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
 383   -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 384
 385 val b_graph_translate_props_jmdiscr :
 386   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 387   b_graph_translate_data -> Joint.joint_closed_internal_function ->
 388   Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
 389   List.list) -> (Graphs.label -> Registers.register List.list) -> __
 390
 391 val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
 392
 393 val set_entry :
 394   AST.ident List.list -> Joint.params -> Joint.joint_internal_function -> __
 395   -> Joint.joint_internal_function
 396
 397 val b_graph_translate :
 398   Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
 399   bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
 400   Joint.joint_closed_internal_function Types.sig0
 401
 402 val b_graph_transform_program :
 403   Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
 404   Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
 405   Joint.joint_program -> Joint.joint_program
 406
 407 val added_registers :
 408   Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
 409   -> (Graphs.label -> Registers.register List.list) -> Registers.register
 410   List.list
 411