Changeset 2921


Ignore:
Timestamp:
Mar 21, 2013, 12:56:57 AM (7 years ago)
Author:
sacerdot
Message:

Extracted again.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • extracted/rTLabsToRTL.ml

    r2913 r2921  
    150150    -> 'a1) -> register_type -> 'a1 **)
    151151let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    152 | Register_int x_21297 -> h_register_int x_21297
    153 | Register_ptr (x_21299, x_21298) -> h_register_ptr x_21299 x_21298
     152| Register_int x_8 -> h_register_int x_8
     153| Register_ptr (x_10, x_9) -> h_register_ptr x_10 x_9
    154154
    155155(** val register_type_rect_Type5 :
    … …  
    157157    -> 'a1) -> register_type -> 'a1 **)
    158158let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    159 | Register_int x_21303 -> h_register_int x_21303
    160 | Register_ptr (x_21305, x_21304) -> h_register_ptr x_21305 x_21304
     159| Register_int x_14 -> h_register_int x_14
     160| Register_ptr (x_16, x_15) -> h_register_ptr x_16 x_15
    161161
    162162(** val register_type_rect_Type3 :
    … …  
    164164    -> 'a1) -> register_type -> 'a1 **)
    165165let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    166 | Register_int x_21309 -> h_register_int x_21309
    167 | Register_ptr (x_21311, x_21310) -> h_register_ptr x_21311 x_21310
     166| Register_int x_20 -> h_register_int x_20
     167| Register_ptr (x_22, x_21) -> h_register_ptr x_22 x_21
    168168
    169169(** val register_type_rect_Type2 :
    … …  
    171171    -> 'a1) -> register_type -> 'a1 **)
    172172let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    173 | Register_int x_21315 -> h_register_int x_21315
    174 | Register_ptr (x_21317, x_21316) -> h_register_ptr x_21317 x_21316
     173| Register_int x_26 -> h_register_int x_26
     174| Register_ptr (x_28, x_27) -> h_register_ptr x_28 x_27
    175175
    176176(** val register_type_rect_Type1 :
    … …  
    178178    -> 'a1) -> register_type -> 'a1 **)
    179179let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    180 | Register_int x_21321 -> h_register_int x_21321
    181 | Register_ptr (x_21323, x_21322) -> h_register_ptr x_21323 x_21322
     180| Register_int x_32 -> h_register_int x_32
     181| Register_ptr (x_34, x_33) -> h_register_ptr x_34 x_33
    182182
    183183(** val register_type_rect_Type0 :
    … …  
    185185    -> 'a1) -> register_type -> 'a1 **)
    186186let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    187 | Register_int x_21327 -> h_register_int x_21327
    188 | Register_ptr (x_21329, x_21328) -> h_register_ptr x_21329 x_21328
     187| Register_int x_38 -> h_register_int x_38
     188| Register_ptr (x_40, x_39) -> h_register_ptr x_40 x_39
    189189
    190190(** val register_type_inv_rect_Type4 :
    … …  
    386386    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    387387    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    388     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
     388    Joint.joint_seq List.list **)
    389389let translate_op globals op destrs srcrs1 srcrs2 =
    390390  (match op with
    391391   | BackEndOps.Add ->
    392      (fun _ ->
    393        (match destrs with
    394         | List.Nil -> (fun _ _ _ -> let l = List.Nil in Bind_new.Bret l)
    395         | List.Cons (destr, destrs') ->
    396           (fun _ ->
    397             (match srcrs1 with
    398              | List.Nil -> (fun _ _ -> assert false (* absurd case *))
    399              | List.Cons (srcr1, srcrs1') ->
    400                (fun _ _ ->
    401                  (match srcrs2 with
    402                   | List.Nil -> (fun _ _ -> assert false (* absurd case *))
    403                   | List.Cons (srcr2, srcrs2') ->
    404                     (fun _ _ ->
    405                       let l = List.Cons ((Joint.OP2 (BackEndOps.Add,
    406                         (Obj.magic destr), (Obj.magic srcr1),
    407                         (Obj.magic srcr2))),
    408                         (translate_op_aux globals BackEndOps.Addc destrs'
    409                           srcrs1' srcrs2'))
    410                       in
    411                       Bind_new.Bret l)) __)) __)) __)
     392     (match destrs with
     393      | List.Nil -> (fun _ _ -> List.Nil)
     394      | List.Cons (destr, destrs') ->
     395        (match srcrs1 with
     396         | List.Nil -> (fun _ -> assert false (* absurd case *))
     397         | List.Cons (srcr1, srcrs1') ->
     398           (fun _ ->
     399             match srcrs2 with
     400             | List.Nil -> (fun _ -> assert false (* absurd case *))
     401             | List.Cons (srcr2, srcrs2') ->
     402               (fun _ -> List.Cons ((Joint.OP2 (BackEndOps.Add,
     403                 (Obj.magic destr), (Obj.magic srcr1), (Obj.magic srcr2))),
     404                 (translate_op_aux globals BackEndOps.Addc destrs' srcrs1'
     405                   srcrs2'))))))
    412406   | BackEndOps.Addc ->
    413      (fun _ _ _ ->
    414        let l =
    415          List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
    416            (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2)
    417        in
    418        Bind_new.Bret l)
     407     (fun _ _ ->
     408       List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
     409         (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2))
    419410   | BackEndOps.Sub ->
    420      (fun _ _ _ ->
    421        let l =
    422          List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
    423            (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2)
    424        in
    425        Bind_new.Bret l)
     411     (fun _ _ ->
     412       List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
     413         (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2))
    426414   | BackEndOps.And ->
    427      (fun _ _ _ ->
    428        let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
    429        Bind_new.Bret l)
     415     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
    430416   | BackEndOps.Or ->
    431      (fun _ _ _ ->
    432        let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
    433        Bind_new.Bret l)
     417     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
    434418   | BackEndOps.Xor ->
    435      (fun _ _ _ ->
    436        let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
    437        Bind_new.Bret l)) __ __ __
     419     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)) __ __
    438420
    439421(** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
    … …  
    448430    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    449431    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    450     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
     432    Joint.joint_seq List.list **)
    451433let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
    452434  let l = List.length destrs in
    … …  
    497479         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
    498480         List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))),
    499          (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
    500          (Obj.magic (Joint.psd_argument_from_reg r1)),
    501          (Obj.magic
    502            (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
    503          (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
    504          (Obj.magic (Joint.psd_argument_from_reg r2)),
    505          (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    506          List.Nil))))))
     481         (match Nat.eqb offset Nat.O with
     482          | Bool.True -> List.Nil
     483          | Bool.False ->
     484            translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons
     485              (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1),
     486              (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil))))
     487              (List.Cons
     488              ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)),
     489              (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
     490              List.Nil)))))))
    507491     | FrontEndOps.Oaddrstack offset ->
    508492       (fun _ _ ->
    … …  
    512496             (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
    513497           in
    514           x), (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
    515          (Obj.magic (Joint.psd_argument_from_reg r1)),
    516          (Obj.magic
    517            (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
    518          (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
    519          (Obj.magic (Joint.psd_argument_from_reg r2)),
    520          (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    521          List.Nil))))))) __ __
     498          x),
     499         (match Nat.eqb offset Nat.O with
     500          | Bool.True -> List.Nil
     501          | Bool.False ->
     502            translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons
     503              (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1),
     504              (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil))))
     505              (List.Cons
     506              ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)),
     507              (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
     508              List.Nil)))))))) __ __
    522509  in
    523510  Bind_new.Bret l
    … …  
    618605    BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
    619606      (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
    620         (translate_op globals op destrs srcrs1init.Types.fst
    621           srcrs2init.Types.fst))))
     607        (let l0 =
     608           translate_op globals op destrs srcrs1init.Types.fst
     609             srcrs2init.Types.fst
     610         in
     611        Bind_new.Bret l0))))
    622612
    623613(** val translate_cast :
    … …  
    651641          let l = translate_fill_with_zero globals dst_rest in
    652642          Bind_new.Bret l)
    653      | List.Cons (x, x0) ->
    654 let l = List.Nil in Bind_new.Bret l)
     643     | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)
    655644
    656645(** val translate_notint :
    … …  
    663652(** val translate_negint :
    664653    AST.ident List.list -> Registers.register List.list -> Registers.register
    665     List.list -> (Registers.register, Joint.joint_seq List.list)
    666     Bind_new.bind_new **)
     654    List.list -> Joint.joint_seq List.list **)
    667655let translate_negint globals destrs srcrs =
    668   BindLists.bappend
    669     (let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
     656  List.append (translate_notint globals destrs srcrs)
    670657    (translate_op globals BackEndOps.Add destrs
    671658      (List.map (fun x -> Joint.Reg x) destrs)
    … …  
    723710     (fun _ _ -> translate_cast globals src_sign destrs srcrs)
    724711   | FrontEndOps.Onegint (sz, sg) ->
    725      (fun _ _ -> translate_negint globals destrs srcrs)
     712     (fun _ _ ->
     713       let l = translate_negint globals destrs srcrs in Bind_new.Bret l)
    726714   | FrontEndOps.Onotbool (x, x0, x1) ->
    727715     (fun _ _ -> translate_notbool globals destrs srcrs)
    … …  
    745733    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
    746734    -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
    747     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
    748     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
     735    Joint.joint_seq List.list -> Joint.joint_seq List.list **)
    749736let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
    750737  let i = i_sig in
    … …  
    757744  in
    758745  let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
    759   BindLists.bappend
    760     (let l = List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
    761        (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
    762        (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil)
    763      in
    764     Bind_new.Bret l)
    765     (BindLists.bappend
     746  List.append (List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
     747    (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
     748    (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil))
     749    (List.append
    766750      (translate_op globals BackEndOps.Add tmp_destrs_view
    767751        (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)
    … …  
    782766            srcrs2 k) acc (Lists.range_strong (Nat.S k))
    783767      in
    784       BindLists.bappend
    785         (let l = translate_fill_with_zero globals tmp_destrs in
    786         Bind_new.Bret l)
    787         (BindLists.bappend
    788           (List.foldr translate_mul_k (let l = List.Nil in Bind_new.Bret l)
    789             (Lists.range_strong (List.length destrs)))
    790           (let l =
    791              translate_move globals destrs
    792                (List.map (fun x -> Joint.Reg x) tmp_destrs)
    793            in
    794           Bind_new.Bret l))))))
     768      let l =
     769        List.append (translate_fill_with_zero globals tmp_destrs)
     770          (List.append
     771            (List.foldr translate_mul_k List.Nil
     772              (Lists.range_strong (List.length destrs)))
     773            (translate_move globals destrs
     774              (List.map (fun x -> Joint.Reg x) tmp_destrs)))
     775      in
     776      Bind_new.Bret l))))
    795777
    796778(** val translate_divumodu8 :
    … …  
    919901        (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
    920902        (BindLists.bappend
    921           (translate_op globals BackEndOps.Sub
    922             (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2)
     903          (let l =
     904             translate_op globals BackEndOps.Sub
     905               (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2
     906           in
     907          Bind_new.Bret l)
    923908          (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
    924909             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
    … …  
    1008993  (match op2 with
    1009994   | FrontEndOps.Oadd (sz, sg) ->
    1010      (fun _ _ _ -> translate_op globals BackEndOps.Add destrs srcrs1 srcrs2)
     995     (fun _ _ _ ->
     996       let l = translate_op globals BackEndOps.Add destrs srcrs1 srcrs2 in
     997       Bind_new.Bret l)
    1011998   | FrontEndOps.Osub (sz, sg) ->
    1012      (fun _ _ _ -> translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2)
     999     (fun _ _ _ ->
     1000       let l = translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2 in
     1001       Bind_new.Bret l)
    10131002   | FrontEndOps.Omul (sz, sg) ->
    10141003     (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
    … …  
    10221011       translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
    10231012   | FrontEndOps.Oand (sz, sg) ->
    1024      (fun _ _ _ -> translate_op globals BackEndOps.And destrs srcrs1 srcrs2)
     1013     (fun _ _ _ ->
     1014       let l = translate_op globals BackEndOps.And destrs srcrs1 srcrs2 in
     1015       Bind_new.Bret l)
    10251016   | FrontEndOps.Oor (sz, sg) ->
    1026      (fun _ _ _ -> translate_op globals BackEndOps.Or destrs srcrs1 srcrs2)
     1017     (fun _ _ _ ->
     1018       let l = translate_op globals BackEndOps.Or destrs srcrs1 srcrs2 in
     1019       Bind_new.Bret l)
    10271020   | FrontEndOps.Oxor (sz, sg) ->
    1028      (fun _ _ _ -> translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2)
     1021     (fun _ _ _ ->
     1022       let l = translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2 in
     1023       Bind_new.Bret l)
    10291024   | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
    10301025   | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
    … …  
    10451040   | FrontEndOps.Osubpp sz ->
    10461041     (fun _ _ _ ->
    1047        translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1 srcrs2)
     1042       let l =
     1043         translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1
     1044           srcrs2
     1045       in
     1046       Bind_new.Bret l)
    10481047   | FrontEndOps.Ocmpp (sg, c) ->
    1049      (fun _ _ _ ->
    1050        let is_Ocmpp = Nat.O in
    1051        translate_cmp Bool.True globals c destrs srcrs1 srcrs2)) __ __ __
     1048     (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2))
     1049    __ __ __
    10521050
    10531051(** val translate_cond :
    … …  
    10931091           Bind_new.Bret l)
    10941092           (BindLists.bappend
    1095              (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
    1096                (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
    1097                ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
    1098                ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
    1099                (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
    1100                (List.Cons
    1101                ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
    1102                List.Nil))))) acc)
     1093             (let l =
     1094                translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
     1095                  (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
     1096                  ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
     1097                  ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
     1098                  (List.Cons
     1099                  ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
     1100                  (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
     1101                  List.Nil))))
     1102              in
     1103             Bind_new.Bret l) acc)
    11031104       in
    11041105      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))
    … …  
    11241125           Bind_new.Bret l)
    11251126           (BindLists.bappend
    1126              (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
    1127                (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
    1128                ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
    1129                ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
    1130                (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
    1131                (List.Cons
    1132                ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
    1133                List.Nil))))) acc)
     1127             (let l =
     1128                translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
     1129                  (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
     1130                  ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
     1131                  ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
     1132                  (List.Cons
     1133                  ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
     1134                  (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
     1135                  List.Nil))))
     1136              in
     1137             Bind_new.Bret l) acc)
    11341138       in
    11351139      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))

  • extracted/rTLabsToRTL.mli

    r2867 r2921  
    246246  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    247247  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    248   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
     248  Joint.joint_seq List.list
    249249
    250250val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
    … …  
    253253  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    254254  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    255   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
     255  Joint.joint_seq List.list
    256256
    257257val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
    … …  
    300300val translate_negint :
    301301  AST.ident List.list -> Registers.register List.list -> Registers.register
    302   List.list -> (Registers.register, Joint.joint_seq List.list)
    303   Bind_new.bind_new
     302  List.list -> Joint.joint_seq List.list
    304303
    305304val translate_notbool :
    … …  
    317316  -> Registers.register List.list -> Joint.psd_argument List.list ->
    318317  Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
    319   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
    320   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
     318  Joint.joint_seq List.list -> Joint.joint_seq List.list
    321319
    322320val translate_mul :
Note: See TracChangeset for help on using the changeset viewer.