extracted/rTLabsToRTL.ml

   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 let size_of_sig_type = function
 141 | AST.ASTint (isize, sign) ->
 142   (match isize with
 143    | AST.I8 -> Nat.S Nat.O
 144    | AST.I16 -> Nat.S (Nat.S Nat.O)
 145    | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 146 | AST.ASTptr -> Nat.S (Nat.S Nat.O)
 147
 148 (** val sign_of_sig_type : AST.typ -> AST.signedness **)
 149 let sign_of_sig_type = function
 150 | AST.ASTint (x, sign) -> sign
 151 | AST.ASTptr -> AST.Unsigned
 152
 153 type register_type =
 154 | Register_int of Registers.register
 155 | Register_ptr of Registers.register * Registers.register
 156
 157 (** val register_type_rect_Type4 :
 158     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 159     -> 'a1) -> register_type -> 'a1 **)
 160 let rec register_type_rect_Type4 h_register_int h_register_ptr = function
 161 | Register_int x_18380 -> h_register_int x_18380
 162 | Register_ptr (x_18382, x_18381) -> h_register_ptr x_18382 x_18381
 163
 164 (** val register_type_rect_Type5 :
 165     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 166     -> 'a1) -> register_type -> 'a1 **)
 167 let rec register_type_rect_Type5 h_register_int h_register_ptr = function
 168 | Register_int x_18386 -> h_register_int x_18386
 169 | Register_ptr (x_18388, x_18387) -> h_register_ptr x_18388 x_18387
 170
 171 (** val register_type_rect_Type3 :
 172     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 173     -> 'a1) -> register_type -> 'a1 **)
 174 let rec register_type_rect_Type3 h_register_int h_register_ptr = function
 175 | Register_int x_18392 -> h_register_int x_18392
 176 | Register_ptr (x_18394, x_18393) -> h_register_ptr x_18394 x_18393
 177
 178 (** val register_type_rect_Type2 :
 179     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 180     -> 'a1) -> register_type -> 'a1 **)
 181 let rec register_type_rect_Type2 h_register_int h_register_ptr = function
 182 | Register_int x_18398 -> h_register_int x_18398
 183 | Register_ptr (x_18400, x_18399) -> h_register_ptr x_18400 x_18399
 184
 185 (** val register_type_rect_Type1 :
 186     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 187     -> 'a1) -> register_type -> 'a1 **)
 188 let rec register_type_rect_Type1 h_register_int h_register_ptr = function
 189 | Register_int x_18404 -> h_register_int x_18404
 190 | Register_ptr (x_18406, x_18405) -> h_register_ptr x_18406 x_18405
 191
 192 (** val register_type_rect_Type0 :
 193     (Registers.register -> 'a1) -> (Registers.register -> Registers.register
 194     -> 'a1) -> register_type -> 'a1 **)
 195 let rec register_type_rect_Type0 h_register_int h_register_ptr = function
 196 | Register_int x_18410 -> h_register_int x_18410
 197 | Register_ptr (x_18412, x_18411) -> h_register_ptr x_18412 x_18411
 198
 199 (** val register_type_inv_rect_Type4 :
 200     register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 201     -> Registers.register -> __ -> 'a1) -> 'a1 **)
 202 let register_type_inv_rect_Type4 hterm h1 h2 =
 203   let hcut = register_type_rect_Type4 h1 h2 hterm in hcut __
 204
 205 (** val register_type_inv_rect_Type3 :
 206     register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 207     -> Registers.register -> __ -> 'a1) -> 'a1 **)
 208 let register_type_inv_rect_Type3 hterm h1 h2 =
 209   let hcut = register_type_rect_Type3 h1 h2 hterm in hcut __
 210
 211 (** val register_type_inv_rect_Type2 :
 212     register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 213     -> Registers.register -> __ -> 'a1) -> 'a1 **)
 214 let register_type_inv_rect_Type2 hterm h1 h2 =
 215   let hcut = register_type_rect_Type2 h1 h2 hterm in hcut __
 216
 217 (** val register_type_inv_rect_Type1 :
 218     register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 219     -> Registers.register -> __ -> 'a1) -> 'a1 **)
 220 let register_type_inv_rect_Type1 hterm h1 h2 =
 221   let hcut = register_type_rect_Type1 h1 h2 hterm in hcut __
 222
 223 (** val register_type_inv_rect_Type0 :
 224     register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
 225     -> Registers.register -> __ -> 'a1) -> 'a1 **)
 226 let register_type_inv_rect_Type0 hterm h1 h2 =
 227   let hcut = register_type_rect_Type0 h1 h2 hterm in hcut __
 228
 229 (** val register_type_discr : register_type -> register_type -> __ **)
 230 let register_type_discr x y =
 231   Logic.eq_rect_Type2 x
 232     (match x with
 233      | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
 234      | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 235
 236 (** val register_type_jmdiscr : register_type -> register_type -> __ **)
 237 let register_type_jmdiscr x y =
 238   Logic.eq_rect_Type2 x
 239     (match x with
 240      | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
 241      | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 242
 243 type local_env = Registers.register List.list Identifiers.identifier_map
 244
 245 (** val find_local_env :
 246     PreIdentifiers.identifier -> local_env -> Registers.register List.list **)
 247 let find_local_env r lenv =
 248   Option.opt_safe (Identifiers.lookup PreIdentifiers.RegisterTag lenv r)
 249
 250 (** val find_local_env_arg :
 251     Registers.register -> local_env -> Joint.psd_argument List.list **)
 252 let find_local_env_arg r lenv =
 253   List.map (fun x -> Joint.Reg x) (find_local_env r lenv)
 254
 255 (** val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __ **)
 256 let rec m_iter m f n m0 =
 257   match n with
 258   | Nat.O -> m0
 259   | Nat.S k -> Monad.m_bind0 m m0 (fun v -> m_iter m f k (f v))
 260
 261 (** val fresh_registers :
 262     Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
 263     List.list Monad.smax_def__o__monad **)
 264 let fresh_registers p g n =
 265   let f = fun acc ->
 266     Monad.m_bind0 (Monad.smax_def State.state_monad)
 267       (TranslateUtils.fresh_register p g) (fun m ->
 268       Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc)))
 269   in
 270   m_iter (Monad.smax_def State.state_monad) f n
 271     (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
 272
 273 (** val map_list_local_env :
 274     Registers.register List.list Identifiers.identifier_map ->
 275     (Registers.register, AST.typ) Types.prod List.list -> Registers.register
 276     List.list **)
 277 let rec map_list_local_env lenv regs =
 278   (match regs with
 279    | List.Nil -> (fun _ -> List.Nil)
 280    | List.Cons (hd, tl) ->
 281      (fun _ ->
 282        List.append (find_local_env hd.Types.fst lenv)
 283          (map_list_local_env lenv tl))) __
 284
 285 (** val initialize_local_env :
 286     AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
 287     -> local_env Monad.smax_def__o__monad **)
 288 let initialize_local_env globals registers =
 289   let f = fun r_sig lenv ->
 290     let { Types.fst = r; Types.snd = sig0 } = r_sig in
 291     let size = size_of_sig_type sig0 in
 292     Monad.m_bind0 (Monad.smax_def State.state_monad)
 293       (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size)
 294       (fun regs ->
 295       Monad.m_return0 (Monad.smax_def State.state_monad)
 296         (Identifiers.add PreIdentifiers.RegisterTag lenv r regs))
 297   in
 298   Monad.m_fold (Monad.smax_def State.state_monad) f registers
 299     (Identifiers.empty_map PreIdentifiers.RegisterTag)
 300
 301 (** val initialize_locals_params_ret :
 302     AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
 303     -> (Registers.register, AST.typ) Types.prod List.list ->
 304     (Registers.register, AST.typ) Types.prod Types.option -> local_env
 305     Monad.smax_def__o__monad **)
 306 let initialize_locals_params_ret globals locals params ret =
 307   Obj.magic (fun def ->
 308     (let { Types.fst = def'; Types.snd = lenv } =
 309        Obj.magic initialize_local_env globals
 310          (List.append
 311            (match ret with
 312             | Types.None -> List.Nil
 313             | Types.Some r_sig -> List.Cons (r_sig, List.Nil))
 314            (List.append locals params)) def
 315      in
 316     (fun _ ->
 317     let params' = map_list_local_env lenv params in
 318     let ret' =
 319       (match ret with
 320        | Types.None -> (fun _ -> List.Nil)
 321        | Types.Some r_sig -> (fun _ -> find_local_env r_sig.Types.fst lenv))
 322         __
 323     in
 324     let def'' = { Joint.joint_if_luniverse = def'.Joint.joint_if_luniverse;
 325       Joint.joint_if_runiverse = def'.Joint.joint_if_runiverse;
 326       Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
 327       (Obj.magic params'); Joint.joint_if_stacksize =
 328       def'.Joint.joint_if_stacksize; Joint.joint_if_local_stacksize =
 329       def'.Joint.joint_if_local_stacksize; Joint.joint_if_code =
 330       def'.Joint.joint_if_code; Joint.joint_if_entry =
 331       def'.Joint.joint_if_entry }
 332     in
 333     { Types.fst = def''; Types.snd = lenv })) __)
 334
 335 (** val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod **)
 336 let make_addr lst =
 337   { Types.fst = (Util.nth_safe Nat.O lst); Types.snd =
 338     (Util.nth_safe (Nat.S Nat.O) lst) }
 339
 340 (** val find_and_addr :
 341     PreIdentifiers.identifier -> local_env -> (Registers.register,
 342     Registers.register) Types.prod **)
 343 let find_and_addr r lenv =
 344   make_addr (find_local_env r lenv)
 345
 346 (** val find_and_addr_arg :
 347     Registers.register -> local_env -> (Joint.psd_argument,
 348     Joint.psd_argument) Types.prod **)
 349 let find_and_addr_arg r lenv =
 350   make_addr (find_local_env_arg r lenv)
 351
 352 (** val rtl_args :
 353     Registers.register List.list -> local_env -> Joint.psd_argument List.list **)
 354 let rec rtl_args args env =
 355   (match args with
 356    | List.Nil -> (fun _ -> List.Nil)
 357    | List.Cons (hd, tl) ->
 358      (fun _ -> List.append (find_local_env_arg hd env) (rtl_args tl env))) __
 359
 360 (** val vrsplit :
 361     Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
 362     Types.sig0 **)
 363 let rec vrsplit m n =
 364   match m with
 365   | Nat.O -> (fun v -> List.Nil)
 366   | Nat.S k ->
 367     (fun v ->
 368       let spl = Vector.vsplit n (Nat.times k n) v in
 369       List.Cons (spl.Types.fst, (Types.pi1 (vrsplit k n spl.Types.snd))))
 370
 371 (** val split_into_bytes :
 372     AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 **)
 373 let split_into_bytes size int =
 374   List.reverse
 375     (Types.pi1
 376       (vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 377         (Nat.S (Nat.S (Nat.S Nat.O)))))))) int))
 378
 379 (** val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **)
 380 let rec list_inject_All_aux l =
 381   (match l with
 382    | List.Nil -> (fun _ -> List.Nil)
 383    | List.Cons (hd, tl) ->
 384      (fun _ -> List.Cons (hd, (list_inject_All_aux tl)))) __
 385
 386 (** val translate_op_aux :
 387     AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 388     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 389     Joint.joint_seq List.list **)
 390 let translate_op_aux globals op destrs srcrs1 srcrs2 =
 391   Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1)) (Obj.magic destrs)
 392     (Obj.magic srcrs1) (Obj.magic srcrs2)
 393
 394 (** val translate_op :
 395     AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 396     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 397     Joint.joint_seq List.list **)
 398 let translate_op globals op destrs srcrs1 srcrs2 =
 399   (match op with
 400    | BackEndOps.Add ->
 401      (match destrs with
 402       | List.Nil -> (fun _ _ -> List.Nil)
 403       | List.Cons (destr, destrs') ->
 404         (match srcrs1 with
 405          | List.Nil -> (fun _ -> assert false (* absurd case *))
 406          | List.Cons (srcr1, srcrs1') ->
 407            (fun _ ->
 408              match srcrs2 with
 409              | List.Nil -> (fun _ -> assert false (* absurd case *))
 410              | List.Cons (srcr2, srcrs2') ->
 411                (fun _ -> List.Cons ((Joint.OP2 (BackEndOps.Add,
 412                  (Obj.magic destr), (Obj.magic srcr1), (Obj.magic srcr2))),
 413                  (translate_op_aux globals BackEndOps.Addc destrs' srcrs1'
 414                    srcrs2'))))))
 415    | BackEndOps.Addc ->
 416      (fun _ _ ->
 417        List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
 418          (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2))
 419    | BackEndOps.Sub ->
 420      (fun _ _ ->
 421        List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
 422          (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2))
 423    | BackEndOps.And ->
 424      (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
 425    | BackEndOps.Or ->
 426      (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
 427    | BackEndOps.Xor ->
 428      (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)) __ __
 429
 430 (** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
 431 let cast_list deflt new_length l =
 432   match Nat.leb (List.length l) new_length with
 433   | Bool.True ->
 434     List.append l
 435       (List.make_list deflt (Nat.minus new_length (List.length l)))
 436   | Bool.False -> List.lhd l new_length
 437
 438 (** val translate_op_asym_unsigned :
 439     AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 440     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 441     Joint.joint_seq List.list **)
 442 let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
 443   let l = List.length destrs in
 444   let srcrs1' =
 445     cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
 446       srcrs1
 447   in
 448   let srcrs2' =
 449     cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
 450       srcrs2
 451   in
 452   translate_op globals op destrs srcrs1' srcrs2'
 453
 454 (** val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
 455 let zero_args size =
 456   List.make_list (Joint.psd_argument_from_byte Joint.zero_byte) size
 457
 458 (** val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
 459 let one_args = function
 460 | Nat.O -> List.Nil
 461 | Nat.S k ->
 462   List.Cons
 463     ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O))
 464       in
 465      x), (Types.pi1 (zero_args k)))
 466
 467 (** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
 468 let size_of_cst typ = function
 469 | FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
 470 | FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
 471 | FrontEndOps.Oaddrstack x -> Nat.S (Nat.S Nat.O)
 472
 473 (** val translate_cst :
 474     AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
 475     Registers.register List.list -> (Registers.register, Joint.joint_seq
 476     List.list) Bind_new.bind_new **)
 477 let translate_cst ty globals cst_sig destrs =
 478   let l =
 479     (match Types.pi1 cst_sig with
 480      | FrontEndOps.Ointconst (size, sign, const) ->
 481        (fun _ _ ->
 482          Util.map2 (fun r b -> Joint.MOVE
 483            (Obj.magic { Types.fst = r; Types.snd =
 484              (Joint.psd_argument_from_byte b) })) destrs
 485            (Types.pi1 (split_into_bytes size const)))
 486      | FrontEndOps.Oaddrsymbol (id, offset) ->
 487        (fun _ _ ->
 488          let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
 489          let off =
 490            Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 491              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 492              (Nat.S (Nat.S Nat.O)))))))))))))))) offset
 493          in
 494          List.Cons ((Joint.ADDRESS (id, off, (Obj.magic r1),
 495          (Obj.magic r2))), List.Nil))
 496      | FrontEndOps.Oaddrstack offset ->
 497        (fun _ _ ->
 498          let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
 499          List.Cons
 500          ((let x = Joint.Extension_seq
 501              (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
 502            in
 503           x),
 504          (match Nat.eqb offset Nat.O with
 505           | Bool.True -> List.Nil
 506           | Bool.False ->
 507             translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons
 508               (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1),
 509               (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil))))
 510               (List.Cons
 511               ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)),
 512               (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
 513               List.Nil)))))))) __ __
 514   in
 515   Bind_new.Bret l
 516
 517 (** val translate_move :
 518     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 519     List.list -> Joint.joint_seq List.list **)
 520 let translate_move globals destrs srcrs =
 521   Util.map2 (fun dst src -> Joint.MOVE
 522     (Obj.magic { Types.fst = dst; Types.snd = src })) destrs srcrs
 523
 524 (** val sign_mask :
 525     AST.ident List.list -> Registers.register -> Joint.psd_argument ->
 526     Joint.joint_seq List.list **)
 527 let sign_mask globals destr = function
 528 | Joint.Reg srcr ->
 529   let byte_127 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 530     (Nat.S Nat.O))))))), Bool.False,
 531     (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 532       Nat.O)))))))))
 533   in
 534   List.Cons ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
 535   (Obj.magic (Joint.psd_argument_from_reg srcr)),
 536   (Obj.magic (Joint.psd_argument_from_byte byte_127)))), (List.Cons
 537   ((Joint.OP1 (BackEndOps.Rl, (Obj.magic destr), (Obj.magic destr))),
 538   (List.Cons ((Joint.OP1 (BackEndOps.Inc, (Obj.magic destr),
 539   (Obj.magic destr))), (List.Cons ((Joint.OP1 (BackEndOps.Cmpl,
 540   (Obj.magic destr), (Obj.magic destr))), List.Nil)))))))
 541 | Joint.Imm b ->
 542   (match Arithmetic.sign_bit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 543            (Nat.S Nat.O)))))))) b with
 544    | Bool.True ->
 545      List.Cons ((Joint.MOVE
 546        (Obj.magic { Types.fst = destr; Types.snd =
 547          (let x =
 548             BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 549               (Nat.S (Nat.S Nat.O))))))))
 550           in
 551          Joint.psd_argument_from_byte x) })), List.Nil)
 552    | Bool.False ->
 553      List.Cons ((Joint.MOVE
 554        (Obj.magic { Types.fst = destr; Types.snd =
 555          (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil))
 556
 557 (** val translate_cast_signed :
 558     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 559     -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 560 let translate_cast_signed globals destrs srca =
 561   Bind_new.Bnew (fun tmp ->
 562     let l =
 563       List.append (sign_mask globals tmp srca)
 564         (translate_move globals destrs
 565           (List.make_list (Joint.Reg tmp) (List.length destrs)))
 566     in
 567     Bind_new.Bret l)
 568
 569 (** val translate_fill_with_zero :
 570     AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 571     List.list **)
 572 let translate_fill_with_zero globals destrs =
 573   translate_move globals destrs (Types.pi1 (zero_args (List.length destrs)))
 574
 575 (** val last : 'a1 List.list -> 'a1 Types.option **)
 576 let rec last = function
 577 | List.Nil -> Types.None
 578 | List.Cons (hd, tl) ->
 579   (match tl with
 580    | List.Nil -> Types.Some hd
 581    | List.Cons (x, x0) -> last tl)
 582
 583 (** val translate_op_asym_signed :
 584     AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
 585     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 586     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 587 let translate_op_asym_signed globals op destrs srcrs1 srcrs2 =
 588   Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
 589     let l = List.length destrs in
 590     let cast_srcrs = fun srcrs tmp ->
 591       let srcrs_l = List.length srcrs in
 592       (match Nat.leb (Nat.S srcrs_l) l with
 593        | Bool.True ->
 594          (match last srcrs with
 595           | Types.None ->
 596             { Types.fst =
 597               (List.make_list
 598                 (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
 599                 l); Types.snd = List.Nil }
 600           | Types.Some last0 ->
 601             { Types.fst =
 602               (List.append srcrs
 603                 (List.make_list (Joint.Reg tmp) (Nat.minus l srcrs_l)));
 604               Types.snd = (sign_mask globals tmp last0) })
 605        | Bool.False ->
 606          { Types.fst = (List.lhd srcrs l); Types.snd = List.Nil })
 607     in
 608     let srcrs1init = cast_srcrs srcrs1 tmp1 in
 609     let srcrs2init = cast_srcrs srcrs2 tmp2 in
 610     BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
 611       (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
 612         (let l0 =
 613            translate_op globals op destrs srcrs1init.Types.fst
 614              srcrs2init.Types.fst
 615          in
 616         Bind_new.Bret l0))))
 617
 618 (** val translate_cast :
 619     AST.ident List.list -> AST.signedness -> Registers.register List.list ->
 620     Registers.register List.list -> (Registers.register, Joint.joint_seq
 621     List.list) Bind_new.bind_new **)
 622 let translate_cast globals src_sign destrs srcrs =
 623   let t = Util.reduce_strong srcrs destrs in
 624   let src_common = t.Types.fst.Types.fst in
 625   let src_rest = t.Types.fst.Types.snd in
 626   let dst_common = t.Types.snd.Types.fst in
 627   let dst_rest = t.Types.snd.Types.snd in
 628   BindLists.bappend
 629     (let l =
 630        translate_move globals dst_common
 631          (List.map (fun x -> Joint.Reg x) src_common)
 632      in
 633     Bind_new.Bret l)
 634     (match src_rest with
 635      | List.Nil ->
 636        (match src_sign with
 637         | AST.Signed ->
 638           (match last srcrs with
 639            | Types.None ->
 640              let l = translate_fill_with_zero globals dst_rest in
 641              Bind_new.Bret l
 642            | Types.Some src_last ->
 643              translate_cast_signed globals dst_rest
 644                (Joint.psd_argument_from_reg src_last))
 645         | AST.Unsigned ->
 646           let l = translate_fill_with_zero globals dst_rest in
 647           Bind_new.Bret l)
 648      | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)
 649
 650 (** val translate_notint :
 651     AST.ident List.list -> Registers.register List.list -> Registers.register
 652     List.list -> Joint.joint_seq List.list **)
 653 let translate_notint globals destrs srcrs =
 654   Util.map2 (fun x x0 -> Joint.OP1 (BackEndOps.Cmpl, x, x0))
 655     (Obj.magic destrs) (Obj.magic srcrs)
 656
 657 (** val translate_negint :
 658     AST.ident List.list -> Registers.register List.list -> Registers.register
 659     List.list -> Joint.joint_seq List.list **)
 660 let translate_negint globals destrs srcrs =
 661   List.append (translate_notint globals destrs srcrs)
 662     (translate_op globals BackEndOps.Add destrs
 663       (List.map (fun x -> Joint.Reg x) destrs)
 664       (Types.pi1 (one_args (List.length destrs))))
 665
 666 (** val translate_notbool :
 667     AST.ident List.list -> Registers.register List.list -> Registers.register
 668     List.list -> (Registers.register, Joint.joint_seq List.list)
 669     Bind_new.bind_new **)
 670 let translate_notbool globals destrs srcrs =
 671   match destrs with
 672   | List.Nil -> let l = List.Nil in Bind_new.Bret l
 673   | List.Cons (destr, destrs') ->
 674     BindLists.bappend
 675       (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
 676       (match srcrs with
 677        | List.Nil ->
 678          let l = List.Cons ((Joint.MOVE
 679            (Obj.magic { Types.fst = destr; Types.snd =
 680              (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil)
 681          in
 682          Bind_new.Bret l
 683        | List.Cons (srcr, srcrs') ->
 684          BindLists.bappend
 685            (BindLists.bcons (Joint.MOVE
 686              (Obj.magic { Types.fst = destr; Types.snd =
 687                (Joint.psd_argument_from_reg srcr) }))
 688              (let l =
 689                 List.map (fun r -> Joint.OP2 (BackEndOps.Or,
 690                   (Obj.magic destr),
 691                   (Obj.magic (Joint.psd_argument_from_reg destr)),
 692                   (Obj.magic (Joint.psd_argument_from_reg r)))) srcrs'
 693               in
 694              Bind_new.Bret l))
 695            (BindLists.bcons Joint.CLEAR_CARRY (Bind_new.Bnew (fun tmp ->
 696              let l = List.Cons ((Joint.MOVE
 697                (Obj.magic { Types.fst = tmp; Types.snd =
 698                  (Joint.psd_argument_from_byte Joint.zero_byte) })),
 699                (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic destr),
 700                (Obj.magic (Joint.psd_argument_from_reg tmp)),
 701                (Obj.magic (Joint.psd_argument_from_reg tmp)))), (List.Cons
 702                ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
 703                (Obj.magic (Joint.psd_argument_from_reg tmp)),
 704                (Obj.magic (Joint.psd_argument_from_reg tmp)))), List.Nil)))))
 705              in
 706              Bind_new.Bret l))))
 707
 708 (** val translate_op1 :
 709     AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation
 710     -> Registers.register List.list -> Registers.register List.list ->
 711     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 712 let translate_op1 globals ty ty' op1 destrs srcrs =
 713   (match op1 with
 714    | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
 715      (fun _ _ -> translate_cast globals src_sign destrs srcrs)
 716    | FrontEndOps.Onegint (sz, sg) ->
 717      (fun _ _ ->
 718        let l = translate_negint globals destrs srcrs in Bind_new.Bret l)
 719    | FrontEndOps.Onotbool (x, x0, x1) ->
 720      (fun _ _ -> translate_notbool globals destrs srcrs)
 721    | FrontEndOps.Onotint (sz, sg) ->
 722      (fun _ _ ->
 723        let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
 724    | FrontEndOps.Oid t ->
 725      (fun _ _ ->
 726        let l =
 727          translate_move globals destrs
 728            (List.map (fun x -> Joint.Reg x) srcrs)
 729        in
 730        Bind_new.Bret l)
 731    | FrontEndOps.Optrofint (sz, sg) ->
 732      (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)
 733    | FrontEndOps.Ointofptr (sz, sg) ->
 734      (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)) __ __
 735
 736 (** val translate_mul_i :
 737     AST.ident List.list -> Registers.register -> Registers.register ->
 738     Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
 739     -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
 740     Joint.joint_seq List.list -> Joint.joint_seq List.list **)
 741 let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
 742   let i = i_sig in
 743   let args =
 744     List.append (List.Cons ((Joint.Reg a), (List.Cons ((Joint.Reg b),
 745       List.Nil))))
 746       (List.make_list
 747         (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
 748         (Nat.minus (Nat.minus n (Nat.S Nat.O)) k))
 749   in
 750   let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
 751   List.append (List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
 752     (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
 753     (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil))
 754     (List.append
 755       (translate_op globals BackEndOps.Add tmp_destrs_view
 756         (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)
 757
 758 (** val translate_mul :
 759     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 760     List.list -> Joint.psd_argument List.list -> (Registers.register,
 761     Joint.joint_seq List.list) Bind_new.bind_new **)
 762 let translate_mul globals destrs srcrs1 srcrs2 =
 763   Bind_new.Bnew (fun a -> Bind_new.Bnew (fun b ->
 764     Bind_new.bnews_strong (List.length destrs) (fun tmp_destrs _ ->
 765       Bind_new.Bnew (fun dummy ->
 766       BindLists.bcons (Joint.MOVE
 767         (Obj.magic { Types.fst = dummy; Types.snd =
 768           (Joint.psd_argument_from_byte (Joint.byte_of_nat Nat.O)) }))
 769         (let translate_mul_k = fun k_sig acc ->
 770            let k = k_sig in
 771            List.foldr
 772              (translate_mul_i globals a b (List.length destrs)
 773                (List.append tmp_destrs (List.Cons (dummy, List.Nil))) srcrs1
 774                srcrs2 k) acc (Lists.range_strong (Nat.S k))
 775          in
 776         let l =
 777           List.append (translate_fill_with_zero globals tmp_destrs)
 778             (List.append
 779               (List.foldr translate_mul_k List.Nil
 780                 (Lists.range_strong (List.length destrs)))
 781               (translate_move globals destrs
 782                 (List.map (fun x -> Joint.Reg x) tmp_destrs)))
 783         in
 784         Bind_new.Bret l)))))
 785
 786 (** val translate_divumodu8 :
 787     AST.ident List.list -> Bool.bool -> Registers.register List.list ->
 788     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 789     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 790 let translate_divumodu8 globals div_not_mod destrs srcrs1 srcrs2 =
 791   (match destrs with
 792    | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
 793    | List.Cons (destr, destrs') ->
 794      (fun _ ->
 795        match destrs' with
 796        | List.Nil ->
 797          (match srcrs1 with
 798           | List.Nil -> (fun _ -> assert false (* absurd case *))
 799           | List.Cons (srcr1, srcrs1') ->
 800             (fun _ ->
 801               (match srcrs2 with
 802                | List.Nil -> (fun _ -> assert false (* absurd case *))
 803                | List.Cons (srcr2, srcrs2') ->
 804                  (fun _ -> Bind_new.Bnew (fun dummy ->
 805                    let l =
 806                      let { Types.fst = destr1; Types.snd = destr2 } =
 807                        match div_not_mod with
 808                        | Bool.True ->
 809                          { Types.fst = destr; Types.snd = dummy }
 810                        | Bool.False ->
 811                          { Types.fst = dummy; Types.snd = destr }
 812                      in
 813                      List.Cons ((Joint.OPACCS (BackEndOps.DivuModu,
 814                      (Obj.magic destr1), (Obj.magic destr2),
 815                      (Obj.magic srcr1), (Obj.magic srcr2))), List.Nil)
 816                    in
 817                    Bind_new.Bret l))) __)) __
 818        | List.Cons (x, x0) -> Logic.false_rect_Type0 __)) __
 819
 820 (** val foldr2 :
 821     ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list ->
 822     'a3 **)
 823 let rec foldr2 f init l1 l2 =
 824   (match l1 with
 825    | List.Nil -> (fun _ -> init)
 826    | List.Cons (a, l1') ->
 827      (fun _ ->
 828        (match l2 with
 829         | List.Nil -> (fun _ -> assert false (* absurd case *))
 830         | List.Cons (b, l2') -> (fun _ -> f a b (foldr2 f init l1' l2'))) __))
 831     __
 832
 833 (** val translate_ne :
 834     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 835     List.list -> Joint.psd_argument List.list -> (Registers.register,
 836     Joint.joint_seq List.list) Bind_new.bind_new **)
 837 let translate_ne globals destrs srcrs1 srcrs2 =
 838   (match destrs with
 839    | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
 840    | List.Cons (destr, destrs') ->
 841      (fun _ ->
 842        BindLists.bappend
 843          (let l = translate_fill_with_zero globals destrs' in
 844          Bind_new.Bret l)
 845          ((match srcrs1 with
 846            | List.Nil ->
 847              (fun _ ->
 848                let l = List.Cons ((Joint.MOVE
 849                  (Obj.magic { Types.fst = destr; Types.snd =
 850                    (Joint.psd_argument_from_byte Joint.zero_byte) })),
 851                  List.Nil)
 852                in
 853                Bind_new.Bret l)
 854            | List.Cons (srcr1, srcrs1') ->
 855              (match srcrs2 with
 856               | List.Nil -> (fun _ -> assert false (* absurd case *))
 857               | List.Cons (srcr2, srcrs2') ->
 858                 (fun _ -> Bind_new.Bnew (fun tmpr ->
 859                   let f = fun s1 s2 acc -> List.Cons ((Joint.OP2
 860                     (BackEndOps.Xor, (Obj.magic tmpr), s1, s2)), (List.Cons
 861                     ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
 862                     (Obj.magic (Joint.psd_argument_from_reg destr)),
 863                     (Obj.magic (Joint.psd_argument_from_reg tmpr)))), acc)))
 864                   in
 865                   let epilogue = List.Cons (Joint.CLEAR_CARRY, (List.Cons
 866                     ((Joint.OP2 (BackEndOps.Sub, (Obj.magic tmpr),
 867                     (Obj.magic
 868                       (Joint.psd_argument_from_byte Joint.zero_byte)),
 869                     (Obj.magic (Joint.psd_argument_from_reg destr)))),
 870                     (List.Cons ((Joint.OP2 (BackEndOps.Addc,
 871                     (Obj.magic destr),
 872                     (Obj.magic
 873                       (Joint.psd_argument_from_byte Joint.zero_byte)),
 874                     (Obj.magic
 875                       (Joint.psd_argument_from_byte Joint.zero_byte)))),
 876                     List.Nil)))))
 877                   in
 878                   let l = List.Cons ((Joint.OP2 (BackEndOps.Xor,
 879                     (Obj.magic destr), (Obj.magic srcr1),
 880                     (Obj.magic srcr2))),
 881                     (foldr2 f epilogue (Obj.magic srcrs1')
 882                       (Obj.magic srcrs2')))
 883                   in
 884                   Bind_new.Bret l)))) __))) __
 885
 886 (** val translate_toggle_bool :
 887     AST.ident List.list -> Registers.register List.list ->
 888     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 889 let translate_toggle_bool globals destrs =
 890   (match destrs with
 891    | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
 892    | List.Cons (destr, x) ->
 893      (fun _ ->
 894        let l = List.Cons ((Joint.OP2 (BackEndOps.Xor, (Obj.magic destr),
 895          (Obj.magic (Joint.psd_argument_from_reg destr)),
 896          (Obj.magic
 897            (Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O)))))),
 898          List.Nil)
 899        in
 900        Bind_new.Bret l)) __
 901
 902 (** val translate_lt_unsigned :
 903     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 904     List.list -> Joint.psd_argument List.list -> (Registers.register,
 905     Joint.joint_seq List.list) Bind_new.bind_new **)
 906 let translate_lt_unsigned globals destrs srcrs1 srcrs2 =
 907   match destrs with
 908   | List.Nil -> let l = List.Nil in Bind_new.Bret l
 909   | List.Cons (destr, destrs') ->
 910     Bind_new.Bnew (fun tmpr ->
 911       BindLists.bappend
 912         (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
 913         (BindLists.bappend
 914           (let l =
 915              translate_op globals BackEndOps.Sub
 916                (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2
 917            in
 918           Bind_new.Bret l)
 919           (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
 920              (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
 921              (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
 922              List.Nil)
 923            in
 924           Bind_new.Bret l)))
 925
 926 (** val shift_signed :
 927     AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
 928     -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
 929     Types.sig0 **)
 930 let rec shift_signed globals tmp srcrs =
 931   let byte_128 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 932     (Nat.S Nat.O))))))), Bool.True,
 933     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 934       Nat.O)))))))))
 935   in
 936   (match srcrs with
 937    | List.Nil -> (fun _ -> { Types.fst = List.Nil; Types.snd = List.Nil })
 938    | List.Cons (srcr, srcrs') ->
 939      (fun _ ->
 940        (match srcrs' with
 941         | List.Nil ->
 942           (fun _ -> { Types.fst = (List.Cons ((Joint.Reg tmp), List.Nil));
 943             Types.snd = (List.Cons ((Joint.OP2 (BackEndOps.Add,
 944             (Obj.magic tmp), (Obj.magic srcr),
 945             (Obj.magic (Joint.psd_argument_from_byte byte_128)))),
 946             List.Nil)) })
 947         | List.Cons (x, x0) ->
 948           (fun _ ->
 949             let re = shift_signed globals tmp srcrs' in
 950             { Types.fst = (List.Cons (srcr, (Types.pi1 re).Types.fst));
 951             Types.snd = (Types.pi1 re).Types.snd })) __)) __
 952
 953 (** val translate_lt_signed :
 954     AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
 955     List.list -> Joint.psd_argument List.list -> (Registers.register,
 956     Joint.joint_seq List.list) Bind_new.bind_new **)
 957 let translate_lt_signed globals destrs srcrs1 srcrs2 =
 958   Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
 959     let p1 = shift_signed globals tmp_last_s1 srcrs1 in
 960     let new_srcrs1 = (Types.pi1 p1).Types.fst in
 961     let shift_srcrs1 = (Types.pi1 p1).Types.snd in
 962     let p2 = shift_signed globals tmp_last_s2 srcrs2 in
 963     let new_srcrs2 = (Types.pi1 p2).Types.fst in
 964     let shift_srcrs2 = (Types.pi1 p2).Types.snd in
 965     BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
 966       (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
 967         (translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2))))
 968
 969 (** val translate_lt :
 970     Bool.bool -> AST.ident List.list -> Registers.register List.list ->
 971     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
 972     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 973 let translate_lt is_unsigned globals destrs srcrs1 srcrs2 =
 974   match is_unsigned with
 975   | Bool.True -> translate_lt_unsigned globals destrs srcrs1 srcrs2
 976   | Bool.False -> translate_lt_signed globals destrs srcrs1 srcrs2
 977
 978 (** val translate_cmp :
 979     Bool.bool -> AST.ident List.list -> Integers.comparison ->
 980     Registers.register List.list -> Joint.psd_argument List.list ->
 981     Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
 982     BindLists.bind_list **)
 983 let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 =
 984   match cmp with
 985   | Integers.Ceq ->
 986     BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
 987       (translate_toggle_bool globals destrs)
 988   | Integers.Cne -> translate_ne globals destrs srcrs1 srcrs2
 989   | Integers.Clt -> translate_lt is_unsigned globals destrs srcrs1 srcrs2
 990   | Integers.Cle ->
 991     BindLists.bappend (translate_lt is_unsigned globals destrs srcrs2 srcrs1)
 992       (translate_toggle_bool globals destrs)
 993   | Integers.Cgt -> translate_lt is_unsigned globals destrs srcrs2 srcrs1
 994   | Integers.Cge ->
 995     BindLists.bappend (translate_lt is_unsigned globals destrs srcrs1 srcrs2)
 996       (translate_toggle_bool globals destrs)
 997
 998 (** val translate_op2 :
 999     AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
1000     FrontEndOps.binary_operation -> Registers.register List.list ->
1001     Joint.psd_argument List.list -> Joint.psd_argument List.list ->
1002     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
1003 let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 =
1004   (match op2 with
1005    | FrontEndOps.Oadd (sz, sg) ->
1006      (fun _ _ _ ->
1007        let l = translate_op globals BackEndOps.Add destrs srcrs1 srcrs2 in
1008        Bind_new.Bret l)
1009    | FrontEndOps.Osub (sz, sg) ->
1010      (fun _ _ _ ->
1011        let l = translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2 in
1012        Bind_new.Bret l)
1013    | FrontEndOps.Omul (sz, sg) ->
1014      (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
1015    | FrontEndOps.Odiv x -> assert false (* absurd case *)
1016    | FrontEndOps.Odivu sz ->
1017      (fun _ _ _ ->
1018        translate_divumodu8 globals Bool.True destrs srcrs1 srcrs2)
1019    | FrontEndOps.Omod x -> assert false (* absurd case *)
1020    | FrontEndOps.Omodu sz ->
1021      (fun _ _ _ ->
1022        translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
1023    | FrontEndOps.Oand (sz, sg) ->
1024      (fun _ _ _ ->
1025        let l = translate_op globals BackEndOps.And destrs srcrs1 srcrs2 in
1026        Bind_new.Bret l)
1027    | FrontEndOps.Oor (sz, sg) ->
1028      (fun _ _ _ ->
1029        let l = translate_op globals BackEndOps.Or destrs srcrs1 srcrs2 in
1030        Bind_new.Bret l)
1031    | FrontEndOps.Oxor (sz, sg) ->
1032      (fun _ _ _ ->
1033        let l = translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2 in
1034        Bind_new.Bret l)
1035    | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
1036    | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
1037    | FrontEndOps.Oshru (x, x0) -> assert false (* absurd case *)
1038    | FrontEndOps.Ocmp (sz, sg1, sg2, c) ->
1039      (fun _ _ _ -> translate_cmp Bool.False globals c destrs srcrs1 srcrs2)
1040    | FrontEndOps.Ocmpu (sz, sg, c) ->
1041      (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)
1042    | FrontEndOps.Oaddpi sz ->
1043      (fun _ _ _ ->
1044        translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1045    | FrontEndOps.Oaddip sz ->
1046      (fun _ _ _ ->
1047        translate_op_asym_signed globals BackEndOps.Add destrs srcrs2 srcrs1)
1048    | FrontEndOps.Osubpi sz ->
1049      (fun _ _ _ ->
1050        translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1051    | FrontEndOps.Osubpp sz ->
1052      (fun _ _ _ ->
1053        let l =
1054          translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1
1055            srcrs2
1056        in
1057        Bind_new.Bret l)
1058    | FrontEndOps.Ocmpp (sg, c) ->
1059      (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2))
1060     __ __ __
1061
1062 (** val translate_cond :
1063     AST.ident List.list -> Registers.register List.list -> Graphs.label ->
1064     Blocks.bind_step_block **)
1065 let translate_cond globals srcrs lbl_true =
1066   match srcrs with
1067   | List.Nil ->
1068     Bind_new.Bret
1069       (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1070         globals List.Nil)
1071   | List.Cons (srcr, srcrs') ->
1072     Bind_new.Bnew (fun tmpr ->
1073       let f = fun r x -> Joint.OP2 (BackEndOps.Or, (Obj.magic tmpr),
1074         (Obj.magic (Joint.psd_argument_from_reg tmpr)),
1075         (Obj.magic (Joint.psd_argument_from_reg r)))
1076       in
1077       Bind_new.Bret { Types.fst = { Types.fst = (List.Cons ((fun x ->
1078       Joint.MOVE
1079       (Obj.magic { Types.fst = tmpr; Types.snd =
1080         (Joint.psd_argument_from_reg srcr) })), (List.map f srcrs')));
1081       Types.snd = (fun x -> Joint.COND ((Obj.magic tmpr), lbl_true)) };
1082       Types.snd = List.Nil })
1083
1084 (** val translate_load :
1085     AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
1086     List.list -> (Registers.register, Joint.joint_seq List.list)
1087     Bind_new.bind_new **)
1088 let translate_load globals addr destrs =
1089   Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1090     BindLists.bappend
1091       (let l =
1092          translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1093            (tmp_addr_h, List.Nil)))) addr
1094        in
1095       Bind_new.Bret l)
1096       (let f = fun destr acc ->
1097          BindLists.bappend
1098            (let l = List.Cons ((Joint.LOAD (destr,
1099               (Obj.magic (Joint.Reg tmp_addr_l)),
1100               (Obj.magic (Joint.Reg tmp_addr_h)))), List.Nil)
1101             in
1102            Bind_new.Bret l)
1103            (BindLists.bappend
1104              (let l =
1105                 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1106                   (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1107                   ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1108                   ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1109                   (List.Cons
1110                   ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1111                   (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1112                   List.Nil))))
1113               in
1114              Bind_new.Bret l) acc)
1115        in
1116       List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))
1117
1118 (** val translate_store :
1119     AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
1120     List.list -> (Registers.register, Joint.joint_seq List.list)
1121     Bind_new.bind_new **)
1122 let translate_store globals addr srcrs =
1123   Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1124     BindLists.bappend
1125       (let l =
1126          translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1127            (tmp_addr_h, List.Nil)))) addr
1128        in
1129       Bind_new.Bret l)
1130       (let f = fun srcr acc ->
1131          BindLists.bappend
1132            (let l = List.Cons ((Joint.STORE
1133               ((Obj.magic (Joint.Reg tmp_addr_l)),
1134               (Obj.magic (Joint.Reg tmp_addr_h)), srcr)), List.Nil)
1135             in
1136            Bind_new.Bret l)
1137            (BindLists.bappend
1138              (let l =
1139                 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1140                   (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1141                   ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1142                   ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1143                   (List.Cons
1144                   ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1145                   (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1146                   List.Nil))))
1147               in
1148              Bind_new.Bret l) acc)
1149        in
1150       List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))
1151
1152 (** val ensure_bind_step_block :
1153     Joint.params -> AST.ident List.list -> (Registers.register,
1154     Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
1155 let ensure_bind_step_block p g b =
1156   Obj.magic
1157     (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
1158       Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l))))
1159
1160 (** val translate_statement :
1161     AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
1162     -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
1163     Blocks.bind_fin_block) Types.sum, __) Types.dPair **)
1164 let translate_statement globals locals lenv stmt =
1165   (match stmt with
1166    | RTLabs_syntax.St_skip lbl' ->
1167      (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret
1168        (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1169          globals List.Nil))); Types.dpi2 = (Obj.magic lbl') })
1170    | RTLabs_syntax.St_cost (cost_lbl, lbl') ->
1171      (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1172        { Types.fst = List.Nil; Types.snd = (fun x -> Joint.COST_LABEL
1173        cost_lbl) }; Types.snd = List.Nil })); Types.dpi2 =
1174        (Obj.magic lbl') })
1175    | RTLabs_syntax.St_const (ty, destr, cst, lbl') ->
1176      (fun _ -> { Types.dpi1 = (Types.Inl
1177        (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1178          (translate_cst ty globals cst (find_local_env destr lenv))));
1179        Types.dpi2 = (Obj.magic lbl') })
1180    | RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') ->
1181      (fun _ -> { Types.dpi1 = (Types.Inl
1182        (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1183          (translate_op1 globals ty' ty op1 (find_local_env destr lenv)
1184            (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1185    | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') ->
1186      (fun _ -> { Types.dpi1 = (Types.Inl
1187        (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1188          (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv)
1189            (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
1190        Types.dpi2 = (Obj.magic lbl') })
1191    | RTLabs_syntax.St_load (ignore, addr, destr, lbl') ->
1192      (fun _ -> { Types.dpi1 = (Types.Inl
1193        (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1194          (translate_load globals (find_local_env_arg addr lenv)
1195            (find_local_env destr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1196    | RTLabs_syntax.St_store (ignore, addr, srcr, lbl') ->
1197      (fun _ -> { Types.dpi1 = (Types.Inl
1198        (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1199          (translate_store globals (find_local_env_arg addr lenv)
1200            (find_local_env_arg srcr lenv)))); Types.dpi2 =
1201        (Obj.magic lbl') })
1202    | RTLabs_syntax.St_call_id (f, args, retr, lbl') ->
1203      (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1204        { Types.fst = List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inl
1205        f), (Obj.magic (rtl_args args lenv)),
1206        (match retr with
1207         | Types.None -> Obj.magic List.Nil
1208         | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1209        Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1210    | RTLabs_syntax.St_call_ptr (f, args, retr, lbl') ->
1211      (fun _ ->
1212        let fs = find_and_addr_arg f lenv in
1213        { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst = { Types.fst =
1214        List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inr
1215        (Obj.magic fs)), (Obj.magic (rtl_args args lenv)),
1216        (match retr with
1217         | Types.None -> Obj.magic List.Nil
1218         | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1219        Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1220    | RTLabs_syntax.St_cond (r, lbl_true, lbl_false) ->
1221      (fun _ -> { Types.dpi1 = (Types.Inl
1222        (translate_cond globals (find_local_env r lenv) lbl_true));
1223        Types.dpi2 = (Obj.magic lbl_false) })
1224    | RTLabs_syntax.St_return ->
1225      (fun _ -> { Types.dpi1 = (Types.Inr (Bind_new.Bret { Types.fst =
1226        List.Nil; Types.snd = Joint.RETURN })); Types.dpi2 =
1227        (Obj.magic Types.It) })) __
1228
1229 (** val translate_internal :
1230     AST.ident List.list -> RTLabs_syntax.internal_function ->
1231     Joint.joint_closed_internal_function **)
1232 let translate_internal globals def =
1233   let runiverse' = def.RTLabs_syntax.f_reggen in
1234   let luniverse' = def.RTLabs_syntax.f_labgen in
1235   let stack_size' = def.RTLabs_syntax.f_stacksize in
1236   let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
1237   let init = { Joint.joint_if_luniverse = luniverse';
1238     Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
1239     (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
1240     Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
1241     stack_size'; Joint.joint_if_code =
1242     (Obj.magic
1243       (Identifiers.add PreIdentifiers.LabelTag
1244         (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
1245         Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
1246   in
1247   (let { Types.fst = init'; Types.snd = lenv } =
1248      Obj.magic initialize_locals_params_ret globals
1249        def.RTLabs_syntax.f_locals def.RTLabs_syntax.f_params
1250        def.RTLabs_syntax.f_result init
1251    in
1252   (fun _ ->
1253   let vars =
1254     List.append def.RTLabs_syntax.f_locals
1255       (List.append def.RTLabs_syntax.f_params
1256         (match def.RTLabs_syntax.f_result with
1257          | Types.None -> List.Nil
1258          | Types.Some x -> List.Cons (x, List.Nil)))
1259   in
1260   let f_trans = fun lbl stmt def0 ->
1261     let pr = translate_statement globals vars lenv stmt in
1262     (match pr.Types.dpi1 with
1263      | Types.Inl instrs ->
1264        (fun lbl' ->
1265          TranslateUtils.b_adds_graph RTL.rTL globals instrs lbl
1266            (Obj.magic lbl') def0)
1267      | Types.Inr instrs ->
1268        (fun x ->
1269          TranslateUtils.b_fin_adds_graph RTL.rTL globals instrs lbl def0))
1270       pr.Types.dpi2
1271   in
1272   Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph
1273     init')) __
1274
1275 (** val rtlabs_to_rtl :
1276     CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
1277 let rtlabs_to_rtl init_cost p =
1278   { Joint.jp_functions = (AST.prog_funct_names p); Joint.joint_prog =
1279     (AST.transform_program p (fun varnames ->
1280       AST.transf_fundef
1281         (translate_internal (List.append varnames (AST.prog_funct_names p)))));
1282     Joint.init_cost_label = init_cost }
1283