Changeset 2797 for extracted/eRTLptr.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/eRTLptr.ml

    r2775 r2797  
    116116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_21176 -> h_ertlptr_ertl x_21176
    119 | LOW_ADDRESS (x_21178, x_21177) -> h_LOW_ADDRESS x_21178 x_21177
    120 | HIGH_ADDRESS (x_21180, x_21179) -> h_HIGH_ADDRESS x_21180 x_21179
     118| Ertlptr_ertl x_21255 -> h_ertlptr_ertl x_21255
     119| LOW_ADDRESS (x_21257, x_21256) -> h_LOW_ADDRESS x_21257 x_21256
     120| HIGH_ADDRESS (x_21259, x_21258) -> h_HIGH_ADDRESS x_21259 x_21258
    121121
    122122(** val ertlptr_seq_rect_Type5 :
     
    124124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_21185 -> h_ertlptr_ertl x_21185
    127 | LOW_ADDRESS (x_21187, x_21186) -> h_LOW_ADDRESS x_21187 x_21186
    128 | HIGH_ADDRESS (x_21189, x_21188) -> h_HIGH_ADDRESS x_21189 x_21188
     126| Ertlptr_ertl x_21264 -> h_ertlptr_ertl x_21264
     127| LOW_ADDRESS (x_21266, x_21265) -> h_LOW_ADDRESS x_21266 x_21265
     128| HIGH_ADDRESS (x_21268, x_21267) -> h_HIGH_ADDRESS x_21268 x_21267
    129129
    130130(** val ertlptr_seq_rect_Type3 :
     
    132132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_21194 -> h_ertlptr_ertl x_21194
    135 | LOW_ADDRESS (x_21196, x_21195) -> h_LOW_ADDRESS x_21196 x_21195
    136 | HIGH_ADDRESS (x_21198, x_21197) -> h_HIGH_ADDRESS x_21198 x_21197
     134| Ertlptr_ertl x_21273 -> h_ertlptr_ertl x_21273
     135| LOW_ADDRESS (x_21275, x_21274) -> h_LOW_ADDRESS x_21275 x_21274
     136| HIGH_ADDRESS (x_21277, x_21276) -> h_HIGH_ADDRESS x_21277 x_21276
    137137
    138138(** val ertlptr_seq_rect_Type2 :
     
    140140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_21203 -> h_ertlptr_ertl x_21203
    143 | LOW_ADDRESS (x_21205, x_21204) -> h_LOW_ADDRESS x_21205 x_21204
    144 | HIGH_ADDRESS (x_21207, x_21206) -> h_HIGH_ADDRESS x_21207 x_21206
     142| Ertlptr_ertl x_21282 -> h_ertlptr_ertl x_21282
     143| LOW_ADDRESS (x_21284, x_21283) -> h_LOW_ADDRESS x_21284 x_21283
     144| HIGH_ADDRESS (x_21286, x_21285) -> h_HIGH_ADDRESS x_21286 x_21285
    145145
    146146(** val ertlptr_seq_rect_Type1 :
     
    148148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_21212 -> h_ertlptr_ertl x_21212
    151 | LOW_ADDRESS (x_21214, x_21213) -> h_LOW_ADDRESS x_21214 x_21213
    152 | HIGH_ADDRESS (x_21216, x_21215) -> h_HIGH_ADDRESS x_21216 x_21215
     150| Ertlptr_ertl x_21291 -> h_ertlptr_ertl x_21291
     151| LOW_ADDRESS (x_21293, x_21292) -> h_LOW_ADDRESS x_21293 x_21292
     152| HIGH_ADDRESS (x_21295, x_21294) -> h_HIGH_ADDRESS x_21295 x_21294
    153153
    154154(** val ertlptr_seq_rect_Type0 :
     
    156156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_21221 -> h_ertlptr_ertl x_21221
    159 | LOW_ADDRESS (x_21223, x_21222) -> h_LOW_ADDRESS x_21223 x_21222
    160 | HIGH_ADDRESS (x_21225, x_21224) -> h_HIGH_ADDRESS x_21225 x_21224
     158| Ertlptr_ertl x_21300 -> h_ertlptr_ertl x_21300
     159| LOW_ADDRESS (x_21302, x_21301) -> h_LOW_ADDRESS x_21302 x_21301
     160| HIGH_ADDRESS (x_21304, x_21303) -> h_HIGH_ADDRESS x_21304 x_21303
    161161
    162162(** val ertlptr_seq_inv_rect_Type4 :
     
    220220    Bool.False }
    221221
     222(** val eRTLptr_functs : Joint.get_pseudo_reg_functs **)
     223let eRTLptr_functs =
     224  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     225    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     226    Joint.acc_a_args = (fun arg ->
     227    match Obj.magic arg with
     228    | Joint.Reg r -> List.Cons (r, List.Nil)
     229    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
     230    match Obj.magic arg with
     231    | Joint.Reg r -> List.Cons (r, List.Nil)
     232    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
     233    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
     234    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
     235    match Obj.magic arg with
     236    | Joint.Reg r -> List.Cons (r, List.Nil)
     237    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
     238    match Obj.magic arg with
     239    | Joint.Reg r -> List.Cons (r, List.Nil)
     240    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
     241    match Obj.magic arg with
     242    | Joint.Reg r -> List.Cons (r, List.Nil)
     243    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
     244    List.append (ERTL.regs_from_move_dst (Obj.magic x).Types.fst)
     245      (ERTL.regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
     246    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
     247    Joint.ext_seq_regs = (fun s ->
     248    match Obj.magic s with
     249    | Ertlptr_ertl s' -> ERTL.ertl_ext_seq_regs s'
     250    | LOW_ADDRESS (r, x) -> List.Cons (r, List.Nil)
     251    | HIGH_ADDRESS (r, x) -> List.Cons (r, List.Nil)); Joint.params_regs =
     252    (fun x -> List.Nil) }
     253
    222254(** val eRTLptr : Joint.graph_params **)
    223255let eRTLptr =
    224   eRTLptr_uns
     256  { Joint.u_pars = eRTLptr_uns; Joint.functs = eRTLptr_functs }
    225257
    226258type ertlptr_program = Joint.joint_program
     
    241273let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
    242274  Joint.seq_to_step__o__inject
    243     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
     275    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
    244276    (ertlptr_seq_joint x1 x2.Types.dpi1)
    245277
     
    258290let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
    259291  Joint.seq_to_step__o__inject
    260     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
     292    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x1
    261293    (ertlptr_seq_joint x1 (Types.pi1 x2))
    262294
     
    275307let ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
    276308  Joint.seq_to_step__o__inject
    277     (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x0
     309    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTLptr) x0
    278310    (ertlptr_seq_joint x0 x1)
    279311
Note: See TracChangeset for help on using the changeset viewer.