Ignore:
Timestamp:
Mar 13, 2013, 11:12:29 PM (8 years ago)
Author:
sacerdot
Message:

New extraction after indianess bug fixes by Paolo.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabsToRTL.ml

    r2854 r2867  
    150150    -> 'a1) -> register_type -> 'a1 **)
    151151let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    152 | Register_int x_2144 -> h_register_int x_2144
    153 | Register_ptr (x_2146, x_2145) -> h_register_ptr x_2146 x_2145
     152| Register_int x_21128 -> h_register_int x_21128
     153| Register_ptr (x_21130, x_21129) -> h_register_ptr x_21130 x_21129
    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_2150 -> h_register_int x_2150
    160 | Register_ptr (x_2152, x_2151) -> h_register_ptr x_2152 x_2151
     159| Register_int x_21134 -> h_register_int x_21134
     160| Register_ptr (x_21136, x_21135) -> h_register_ptr x_21136 x_21135
    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_2156 -> h_register_int x_2156
    167 | Register_ptr (x_2158, x_2157) -> h_register_ptr x_2158 x_2157
     166| Register_int x_21140 -> h_register_int x_21140
     167| Register_ptr (x_21142, x_21141) -> h_register_ptr x_21142 x_21141
    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_2162 -> h_register_int x_2162
    174 | Register_ptr (x_2164, x_2163) -> h_register_ptr x_2164 x_2163
     173| Register_int x_21146 -> h_register_int x_21146
     174| Register_ptr (x_21148, x_21147) -> h_register_ptr x_21148 x_21147
    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_2168 -> h_register_int x_2168
    181 | Register_ptr (x_2170, x_2169) -> h_register_ptr x_2170 x_2169
     180| Register_int x_21152 -> h_register_int x_21152
     181| Register_ptr (x_21154, x_21153) -> h_register_ptr x_21154 x_21153
    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_2174 -> h_register_int x_2174
    188 | Register_ptr (x_2176, x_2175) -> h_register_ptr x_2176 x_2175
     187| Register_int x_21158 -> h_register_int x_21158
     188| Register_ptr (x_21160, x_21159) -> h_register_ptr x_21160 x_21159
    189189
    190190(** val register_type_inv_rect_Type4 :
     
    362362(** val split_into_bytes :
    363363    AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 **)
    364 let split_into_bytes size =
    365   vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    366     (Nat.S (Nat.S Nat.O))))))))
     364let split_into_bytes size int =
     365  List.reverse
     366    (Types.pi1
     367      (vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     368        (Nat.S (Nat.S (Nat.S Nat.O)))))))) int))
    367369
    368370(** val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **)
     
    373375     (fun _ -> List.Cons (hd, (list_inject_All_aux tl)))) __
    374376
     377(** val translate_op_aux :
     378    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
     379    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
     380    Joint.joint_seq List.list **)
     381let translate_op_aux globals op destrs srcrs1 srcrs2 =
     382  Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1)) (Obj.magic destrs)
     383    (Obj.magic srcrs1) (Obj.magic srcrs2)
     384
    375385(** val translate_op :
    376386    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
     
    378388    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    379389let translate_op globals op destrs srcrs1 srcrs2 =
    380   let l =
    381     List.append
    382       (match op with
    383        | BackEndOps.Add -> List.Nil
    384        | BackEndOps.Addc -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
    385        | BackEndOps.Sub -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
    386        | BackEndOps.And -> List.Nil
    387        | BackEndOps.Or -> List.Nil
    388        | BackEndOps.Xor -> List.Nil)
    389       (Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1))
    390         (Obj.magic destrs) (Obj.magic srcrs1) (Obj.magic srcrs2))
    391   in
    392   Bind_new.Bret l
     390  (match op with
     391   | 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)) __)) __)) __)
     412   | 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)
     419   | 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)
     426   | BackEndOps.And ->
     427     (fun _ _ _ ->
     428       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
     429       Bind_new.Bret l)
     430   | BackEndOps.Or ->
     431     (fun _ _ _ ->
     432       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
     433       Bind_new.Bret l)
     434   | BackEndOps.Xor ->
     435     (fun _ _ _ ->
     436       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
     437       Bind_new.Bret l)) __ __ __
    393438
    394439(** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
     
    416461  translate_op globals op destrs srcrs1' srcrs2'
    417462
    418 (** val nat_to_args :
    419     Nat.nat -> Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
    420 let rec nat_to_args size k =
    421   (match size with
    422    | Nat.O -> (fun _ -> List.Nil)
    423    | Nat.S size' ->
    424      (fun _ -> List.Cons
    425        ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat k) in x),
    426        (Types.pi1
    427          (nat_to_args size'
    428            (Util.division k (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    429              (Nat.S Nat.O)))))))))))))) __
     463(** val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
     464let zero_args size =
     465  List.make_list (Joint.psd_argument_from_byte Joint.zero_byte) size
     466
     467(** val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
     468let one_args = function
     469| Nat.O -> List.Nil
     470| Nat.S k ->
     471  List.Cons
     472    ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O))
     473      in
     474     x), (Types.pi1 (zero_args k)))
    430475
    431476(** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
     
    534579    List.list **)
    535580let translate_fill_with_zero globals destrs =
    536   let res = nat_to_args (List.length destrs) Nat.O in
    537   translate_move globals destrs res
     581  translate_move globals destrs (Types.pi1 (zero_args (List.length destrs)))
    538582
    539583(** val last : 'a1 List.list -> 'a1 Types.option **)
     
    625669    (translate_op globals BackEndOps.Add destrs
    626670      (List.map (fun x -> Joint.Reg x) destrs)
    627       (Types.pi1 (nat_to_args (List.length destrs) (Nat.S Nat.O))))
     671      (Types.pi1 (one_args (List.length destrs))))
    628672
    629673(** val translate_notbool :
Note: See TracChangeset for help on using the changeset viewer.