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

    r2775 r2797  
    111111    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    112112let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    113 | Rtl_stack_address (x_20710, x_20709) -> h_rtl_stack_address x_20710 x_20709
     113| Rtl_stack_address (x_20789, x_20788) -> h_rtl_stack_address x_20789 x_20788
    114114
    115115(** val rtl_seq_rect_Type5 :
    116116    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    117117let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    118 | Rtl_stack_address (x_20714, x_20713) -> h_rtl_stack_address x_20714 x_20713
     118| Rtl_stack_address (x_20793, x_20792) -> h_rtl_stack_address x_20793 x_20792
    119119
    120120(** val rtl_seq_rect_Type3 :
    121121    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    122122let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    123 | Rtl_stack_address (x_20718, x_20717) -> h_rtl_stack_address x_20718 x_20717
     123| Rtl_stack_address (x_20797, x_20796) -> h_rtl_stack_address x_20797 x_20796
    124124
    125125(** val rtl_seq_rect_Type2 :
    126126    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    127127let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    128 | Rtl_stack_address (x_20722, x_20721) -> h_rtl_stack_address x_20722 x_20721
     128| Rtl_stack_address (x_20801, x_20800) -> h_rtl_stack_address x_20801 x_20800
    129129
    130130(** val rtl_seq_rect_Type1 :
    131131    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    132132let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    133 | Rtl_stack_address (x_20726, x_20725) -> h_rtl_stack_address x_20726 x_20725
     133| Rtl_stack_address (x_20805, x_20804) -> h_rtl_stack_address x_20805 x_20804
    134134
    135135(** val rtl_seq_rect_Type0 :
    136136    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    137137let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    138 | Rtl_stack_address (x_20730, x_20729) -> h_rtl_stack_address x_20730 x_20729
     138| Rtl_stack_address (x_20809, x_20808) -> h_rtl_stack_address x_20809 x_20808
    139139
    140140(** val rtl_seq_inv_rect_Type4 :
     
    180180    Bool.False }
    181181
     182(** val rTL_functs : Joint.get_pseudo_reg_functs **)
     183let rTL_functs =
     184  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     185    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
     186    Joint.acc_a_args = (fun a ->
     187    match Obj.magic a with
     188    | Joint.Reg r -> List.Cons (r, List.Nil)
     189    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun a ->
     190    match Obj.magic a with
     191    | Joint.Reg r -> List.Cons (r, List.Nil)
     192    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
     193    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
     194    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun a ->
     195    match Obj.magic a with
     196    | Joint.Reg r -> List.Cons (r, List.Nil)
     197    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun a ->
     198    match Obj.magic a with
     199    | Joint.Reg r -> List.Cons (r, List.Nil)
     200    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun a ->
     201    match Obj.magic a with
     202    | Joint.Reg r -> List.Cons (r, List.Nil)
     203    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
     204    List.append (List.Cons ((Obj.magic x).Types.fst, List.Nil))
     205      (match (Obj.magic x).Types.snd with
     206       | Joint.Reg r -> List.Cons (r, List.Nil)
     207       | Joint.Imm x0 -> List.Nil)); Joint.f_call_args = (fun l ->
     208    Util.foldl (fun l1 a ->
     209      List.append l1
     210        (match a with
     211         | Joint.Reg r -> List.Cons (r, List.Nil)
     212         | Joint.Imm x -> List.Nil)) List.Nil (Obj.magic l));
     213    Joint.f_call_dest = (fun x -> Obj.magic x); Joint.ext_seq_regs =
     214    (fun ext ->
     215    let Rtl_stack_address (r1, r2) = Obj.magic ext in
     216    List.Cons (r1, (List.Cons (r2, List.Nil)))); Joint.params_regs =
     217    (fun x -> Obj.magic x) }
     218
    182219(** val rTL : Joint.graph_params **)
    183220let rTL =
    184   rTL_uns
     221  { Joint.u_pars = rTL_uns; Joint.functs = rTL_functs }
    185222
    186223type rtl_program = Joint.joint_program
Note: See TracChangeset for help on using the changeset viewer.