Changeset 2797 for extracted/eRTL.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTL.ml

    r2775 r2797  
    112112    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    113113let rec move_dst_rect_Type4 h_PSD h_HDW = function
    114 | PSD x_21042 -> h_PSD x_21042
    115 | HDW x_21043 -> h_HDW x_21043
     114| PSD x_21121 -> h_PSD x_21121
     115| HDW x_21122 -> h_HDW x_21122
    116116
    117117(** val move_dst_rect_Type5 :
    118118    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    119119let rec move_dst_rect_Type5 h_PSD h_HDW = function
    120 | PSD x_21047 -> h_PSD x_21047
    121 | HDW x_21048 -> h_HDW x_21048
     120| PSD x_21126 -> h_PSD x_21126
     121| HDW x_21127 -> h_HDW x_21127
    122122
    123123(** val move_dst_rect_Type3 :
    124124    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    125125let rec move_dst_rect_Type3 h_PSD h_HDW = function
    126 | PSD x_21052 -> h_PSD x_21052
    127 | HDW x_21053 -> h_HDW x_21053
     126| PSD x_21131 -> h_PSD x_21131
     127| HDW x_21132 -> h_HDW x_21132
    128128
    129129(** val move_dst_rect_Type2 :
    130130    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    131131let rec move_dst_rect_Type2 h_PSD h_HDW = function
    132 | PSD x_21057 -> h_PSD x_21057
    133 | HDW x_21058 -> h_HDW x_21058
     132| PSD x_21136 -> h_PSD x_21136
     133| HDW x_21137 -> h_HDW x_21137
    134134
    135135(** val move_dst_rect_Type1 :
    136136    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    137137let rec move_dst_rect_Type1 h_PSD h_HDW = function
    138 | PSD x_21062 -> h_PSD x_21062
    139 | HDW x_21063 -> h_HDW x_21063
     138| PSD x_21141 -> h_PSD x_21141
     139| HDW x_21142 -> h_HDW x_21142
    140140
    141141(** val move_dst_rect_Type0 :
    142142    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    143143let rec move_dst_rect_Type0 h_PSD h_HDW = function
    144 | PSD x_21067 -> h_PSD x_21067
    145 | HDW x_21068 -> h_HDW x_21068
     144| PSD x_21146 -> h_PSD x_21146
     145| HDW x_21147 -> h_HDW x_21147
    146146
    147147(** val move_dst_inv_rect_Type4 :
     
    338338| Ertl_new_frame -> h_ertl_new_frame
    339339| Ertl_del_frame -> h_ertl_del_frame
    340 | Ertl_frame_size x_21107 -> h_ertl_frame_size x_21107
     340| Ertl_frame_size x_21186 -> h_ertl_frame_size x_21186
    341341
    342342(** val ertl_seq_rect_Type5 :
     
    345345| Ertl_new_frame -> h_ertl_new_frame
    346346| Ertl_del_frame -> h_ertl_del_frame
    347 | Ertl_frame_size x_21112 -> h_ertl_frame_size x_21112
     347| Ertl_frame_size x_21191 -> h_ertl_frame_size x_21191
    348348
    349349(** val ertl_seq_rect_Type3 :
     
    352352| Ertl_new_frame -> h_ertl_new_frame
    353353| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_21117 -> h_ertl_frame_size x_21117
     354| Ertl_frame_size x_21196 -> h_ertl_frame_size x_21196
    355355
    356356(** val ertl_seq_rect_Type2 :
     
    359359| Ertl_new_frame -> h_ertl_new_frame
    360360| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_21122 -> h_ertl_frame_size x_21122
     361| Ertl_frame_size x_21201 -> h_ertl_frame_size x_21201
    362362
    363363(** val ertl_seq_rect_Type1 :
     
    366366| Ertl_new_frame -> h_ertl_new_frame
    367367| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_21127 -> h_ertl_frame_size x_21127
     368| Ertl_frame_size x_21206 -> h_ertl_frame_size x_21206
    369369
    370370(** val ertl_seq_rect_Type0 :
     
    373373| Ertl_new_frame -> h_ertl_new_frame
    374374| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_21132 -> h_ertl_frame_size x_21132
     375| Ertl_frame_size x_21211 -> h_ertl_frame_size x_21211
    376376
    377377(** val ertl_seq_inv_rect_Type4 :
     
    426426    Bool.False }
    427427
     428(** val regs_from_move_dst : move_dst -> Registers.register List.list **)
     429let regs_from_move_dst = function
     430| PSD r -> List.Cons (r, List.Nil)
     431| HDW x -> List.Nil
     432
     433(** val regs_from_move_src : move_src -> Registers.register List.list **)
     434let regs_from_move_src = function
     435| Joint.Reg r ->
     436  (match r with
     437   | PSD r1 -> List.Cons (r1, List.Nil)
     438   | HDW x -> List.Nil)
     439| Joint.Imm x -> List.Nil
     440
     441(** val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list **)
     442let ertl_ext_seq_regs = function
     443| Ertl_new_frame -> List.Nil
     444| Ertl_del_frame -> List.Nil
     445| Ertl_frame_size r -> List.Cons (r, List.Nil)
     446
     447(** val eRTL_functs : Joint.get_pseudo_reg_functs **)
     448let eRTL_functs =
     449  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     450    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     451    Joint.acc_a_args = (fun arg ->
     452    match Obj.magic arg with
     453    | Joint.Reg r -> List.Cons (r, List.Nil)
     454    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
     455    match Obj.magic arg with
     456    | Joint.Reg r -> List.Cons (r, List.Nil)
     457    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
     458    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
     459    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
     460    match Obj.magic arg with
     461    | Joint.Reg r -> List.Cons (r, List.Nil)
     462    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
     463    match Obj.magic arg with
     464    | Joint.Reg r -> List.Cons (r, List.Nil)
     465    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
     466    match Obj.magic arg with
     467    | Joint.Reg r -> List.Cons (r, List.Nil)
     468    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
     469    List.append (regs_from_move_dst (Obj.magic x).Types.fst)
     470      (regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
     471    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
     472    Joint.ext_seq_regs = (Obj.magic ertl_ext_seq_regs); Joint.params_regs =
     473    (fun x -> List.Nil) }
     474
    428475(** val eRTL : Joint.graph_params **)
    429476let eRTL =
    430   eRTL_uns
     477  { Joint.u_pars = eRTL_uns; Joint.functs = eRTL_functs }
    431478
    432479type ertl_program = Joint.joint_program
     
    561608let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
    562609  Joint.seq_to_step__o__inject
    563     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
     610    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
    564611    (ertl_seq_joint x1 x2.Types.dpi1)
    565612
     
    578625let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
    579626  Joint.seq_to_step__o__inject
    580     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
     627    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
    581628    (ertl_seq_joint x1 (Types.pi1 x2))
    582629
     
    595642let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
    596643  Joint.seq_to_step__o__inject
    597     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x0 (ertl_seq_joint x0 x1)
     644    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x0
     645    (ertl_seq_joint x0 x1)
    598646
    599647(** val ertl_seq_to_joint_seq__o__inject :
Note: See TracChangeset for help on using the changeset viewer.