extracted/joint_LTL_LIN.ml

   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 type registers_move =
 122 | From_acc of I8051.register * Types.unit0
 123 | To_acc of Types.unit0 * I8051.register
 124 | Int_to_reg of I8051.register * BitVector.byte
 125 | Int_to_acc of Types.unit0 * BitVector.byte
 126
 127 (** val registers_move_rect_Type4 :
 128     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 129     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 130     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 131 let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 132 | From_acc (x_18638, x_18637) -> h_from_acc x_18638 x_18637
 133 | To_acc (x_18640, x_18639) -> h_to_acc x_18640 x_18639
 134 | Int_to_reg (x_18642, x_18641) -> h_int_to_reg x_18642 x_18641
 135 | Int_to_acc (x_18644, x_18643) -> h_int_to_acc x_18644 x_18643
 136
 137 (** val registers_move_rect_Type5 :
 138     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 139     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 140     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 141 let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 142 | From_acc (x_18651, x_18650) -> h_from_acc x_18651 x_18650
 143 | To_acc (x_18653, x_18652) -> h_to_acc x_18653 x_18652
 144 | Int_to_reg (x_18655, x_18654) -> h_int_to_reg x_18655 x_18654
 145 | Int_to_acc (x_18657, x_18656) -> h_int_to_acc x_18657 x_18656
 146
 147 (** val registers_move_rect_Type3 :
 148     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 149     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 150     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 151 let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 152 | From_acc (x_18664, x_18663) -> h_from_acc x_18664 x_18663
 153 | To_acc (x_18666, x_18665) -> h_to_acc x_18666 x_18665
 154 | Int_to_reg (x_18668, x_18667) -> h_int_to_reg x_18668 x_18667
 155 | Int_to_acc (x_18670, x_18669) -> h_int_to_acc x_18670 x_18669
 156
 157 (** val registers_move_rect_Type2 :
 158     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 159     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 160     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 161 let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 162 | From_acc (x_18677, x_18676) -> h_from_acc x_18677 x_18676
 163 | To_acc (x_18679, x_18678) -> h_to_acc x_18679 x_18678
 164 | Int_to_reg (x_18681, x_18680) -> h_int_to_reg x_18681 x_18680
 165 | Int_to_acc (x_18683, x_18682) -> h_int_to_acc x_18683 x_18682
 166
 167 (** val registers_move_rect_Type1 :
 168     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 169     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 170     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 171 let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 172 | From_acc (x_18690, x_18689) -> h_from_acc x_18690 x_18689
 173 | To_acc (x_18692, x_18691) -> h_to_acc x_18692 x_18691
 174 | Int_to_reg (x_18694, x_18693) -> h_int_to_reg x_18694 x_18693
 175 | Int_to_acc (x_18696, x_18695) -> h_int_to_acc x_18696 x_18695
 176
 177 (** val registers_move_rect_Type0 :
 178     (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
 179     -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
 180     BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
 181 let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
 182 | From_acc (x_18703, x_18702) -> h_from_acc x_18703 x_18702
 183 | To_acc (x_18705, x_18704) -> h_to_acc x_18705 x_18704
 184 | Int_to_reg (x_18707, x_18706) -> h_int_to_reg x_18707 x_18706
 185 | Int_to_acc (x_18709, x_18708) -> h_int_to_acc x_18709 x_18708
 186
 187 (** val registers_move_inv_rect_Type4 :
 188     registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
 189     (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
 190     BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
 191     'a1) -> 'a1 **)
 192 let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
 193   let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 194
 195 (** val registers_move_inv_rect_Type3 :
 196     registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
 197     (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
 198     BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
 199     'a1) -> 'a1 **)
 200 let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
 201   let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 202
 203 (** val registers_move_inv_rect_Type2 :
 204     registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
 205     (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
 206     BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
 207     'a1) -> 'a1 **)
 208 let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
 209   let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 210
 211 (** val registers_move_inv_rect_Type1 :
 212     registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
 213     (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
 214     BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
 215     'a1) -> 'a1 **)
 216 let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
 217   let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 218
 219 (** val registers_move_inv_rect_Type0 :
 220     registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
 221     (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
 222     BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
 223     'a1) -> 'a1 **)
 224 let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
 225   let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 226
 227 (** val registers_move_discr : registers_move -> registers_move -> __ **)
 228 let registers_move_discr x y =
 229   Logic.eq_rect_Type2 x
 230     (match x with
 231      | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 232      | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 233      | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 234      | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 235
 236 (** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
 237 let registers_move_jmdiscr x y =
 238   Logic.eq_rect_Type2 x
 239     (match x with
 240      | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 241      | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 242      | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 243      | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 244
 245 type ltl_lin_seq =
 246 | SAVE_CARRY
 247 | RESTORE_CARRY
 248 | LOW_ADDRESS of Graphs.label
 249 | HIGH_ADDRESS of Graphs.label
 250
 251 (** val ltl_lin_seq_rect_Type4 :
 252     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 253     ltl_lin_seq -> 'a1 **)
 254 let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 255 | SAVE_CARRY -> h_SAVE_CARRY
 256 | RESTORE_CARRY -> h_RESTORE_CARRY
 257 | LOW_ADDRESS x_18800 -> h_LOW_ADDRESS x_18800
 258 | HIGH_ADDRESS x_18801 -> h_HIGH_ADDRESS x_18801
 259
 260 (** val ltl_lin_seq_rect_Type5 :
 261     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 262     ltl_lin_seq -> 'a1 **)
 263 let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 264 | SAVE_CARRY -> h_SAVE_CARRY
 265 | RESTORE_CARRY -> h_RESTORE_CARRY
 266 | LOW_ADDRESS x_18807 -> h_LOW_ADDRESS x_18807
 267 | HIGH_ADDRESS x_18808 -> h_HIGH_ADDRESS x_18808
 268
 269 (** val ltl_lin_seq_rect_Type3 :
 270     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 271     ltl_lin_seq -> 'a1 **)
 272 let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 273 | SAVE_CARRY -> h_SAVE_CARRY
 274 | RESTORE_CARRY -> h_RESTORE_CARRY
 275 | LOW_ADDRESS x_18814 -> h_LOW_ADDRESS x_18814
 276 | HIGH_ADDRESS x_18815 -> h_HIGH_ADDRESS x_18815
 277
 278 (** val ltl_lin_seq_rect_Type2 :
 279     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 280     ltl_lin_seq -> 'a1 **)
 281 let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 282 | SAVE_CARRY -> h_SAVE_CARRY
 283 | RESTORE_CARRY -> h_RESTORE_CARRY
 284 | LOW_ADDRESS x_18821 -> h_LOW_ADDRESS x_18821
 285 | HIGH_ADDRESS x_18822 -> h_HIGH_ADDRESS x_18822
 286
 287 (** val ltl_lin_seq_rect_Type1 :
 288     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 289     ltl_lin_seq -> 'a1 **)
 290 let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 291 | SAVE_CARRY -> h_SAVE_CARRY
 292 | RESTORE_CARRY -> h_RESTORE_CARRY
 293 | LOW_ADDRESS x_18828 -> h_LOW_ADDRESS x_18828
 294 | HIGH_ADDRESS x_18829 -> h_HIGH_ADDRESS x_18829
 295
 296 (** val ltl_lin_seq_rect_Type0 :
 297     'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
 298     ltl_lin_seq -> 'a1 **)
 299 let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
 300 | SAVE_CARRY -> h_SAVE_CARRY
 301 | RESTORE_CARRY -> h_RESTORE_CARRY
 302 | LOW_ADDRESS x_18835 -> h_LOW_ADDRESS x_18835
 303 | HIGH_ADDRESS x_18836 -> h_HIGH_ADDRESS x_18836
 304
 305 (** val ltl_lin_seq_inv_rect_Type4 :
 306     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
 307     -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
 308 let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
 309   let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 310
 311 (** val ltl_lin_seq_inv_rect_Type3 :
 312     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
 313     -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
 314 let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
 315   let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 316
 317 (** val ltl_lin_seq_inv_rect_Type2 :
 318     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
 319     -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
 320 let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
 321   let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 322
 323 (** val ltl_lin_seq_inv_rect_Type1 :
 324     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
 325     -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
 326 let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
 327   let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 328
 329 (** val ltl_lin_seq_inv_rect_Type0 :
 330     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
 331     -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
 332 let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
 333   let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 334
 335 (** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
 336 let ltl_lin_seq_discr x y =
 337   Logic.eq_rect_Type2 x
 338     (match x with
 339      | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
 340      | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
 341      | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
 342      | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
 343
 344 (** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
 345 let ltl_lin_seq_jmdiscr x y =
 346   Logic.eq_rect_Type2 x
 347     (match x with
 348      | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
 349      | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
 350      | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
 351      | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
 352
 353 (** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
 354 let ltl_lin_seq_labels = function
 355 | SAVE_CARRY -> List.Nil
 356 | RESTORE_CARRY -> List.Nil
 357 | LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
 358 | HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)
 359
 360 (** val lTL_LIN_uns : Joint.unserialized_params **)
 361 let lTL_LIN_uns =
 362   { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
 363     Joint.has_tailcalls = Bool.False }
 364
 365 (** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
 366 let lTL_LIN_functs =
 367   { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
 368     List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
 369     (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
 370     Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
 371     List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
 372     (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
 373     Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
 374     List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
 375     (fun x -> List.Nil) }
 376
 377 (** val lTL_LIN : Joint.uns_params **)
 378 let lTL_LIN =
 379   { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }
 380