Ignore:
Timestamp:
Jan 4, 2012, 7:19:09 PM (8 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/test/search.Cminor.ma

    r1226 r1633  
    22include "common/Animation.ma".
    33
     4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
     5
    46
    57
    68definition id__div32u := ident_of_nat 0.
    7 definition id__div32u_quo := ident_of_nat 4.
    8 definition id__div32u_rem := ident_of_nat 5.
    9 definition id__div32u_x := ident_of_nat 6.
    10 definition id__div32u_y := ident_of_nat 7.
    11 definition C_cost2 := costlabel_of_nat 3.
    12 definition C_cost0 := costlabel_of_nat 2.
     9definition id__div32u_quo := ident_of_nat 6.
     10definition id__div32u_rem := ident_of_nat 7.
     11definition id__div32u_x := ident_of_nat 8.
     12definition id__div32u_y := ident_of_nat 9.
     13definition C_cost2 := costlabel_of_nat 5.
     14definition L_tmp_0 := label_of_nat 4.
     15definition C_cost0 := costlabel_of_nat 3.
     16definition L_tmp_1 := label_of_nat 2.
    1317definition C_cost1 := costlabel_of_nat 1.
    1418definition f__div32u := Internal ? (mk_internal_function
    1519  (Some ? (ASTint I32 Unsigned))
    16   [pair ?? id__div32u_x (ASTint I32 Unsigned); pair ?? id__div32u_y (ASTint I32 Unsigned)]
    17   [pair ?? id__div32u_quo (ASTint I32 Unsigned); pair ?? id__div32u_rem (ASTint I32 Unsigned)]
    18   0 (
     20  [mk_Prod ?? id__div32u_x (ASTint I32 Unsigned); mk_Prod ?? id__div32u_y (ASTint I32 Unsigned)]
     21  [mk_Prod ?? id__div32u_quo (ASTint I32 Unsigned); mk_Prod ?? id__div32u_rem (ASTint I32 Unsigned)]
     22  (match daemon in False with [ ])
     230 (
    1924  St_cost C_cost2 (
    2025  St_seq (
    21     St_assign (ASTint I32 Unsigned) id__div32u_quo (Op1 (ASTint I8 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     26    St_assign (ASTint I32 Unsigned) id__div32u_quo (Op1 (ASTint I8 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    2227  ) (
    2328  St_seq (
     
    2631  St_seq (
    2732    St_seq (
    28       St_block (
    29         St_loop (
    30           St_seq (
    31             St_ifthenelse I32 Signed (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onotbool (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocmpu Cge) (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))) (
    32               St_exit 0
    33             ) (
    34               St_skip            )
    35           ) (
    36           St_block (
    37             St_cost C_cost0 (
    38             St_seq (
    39               St_assign (ASTint I32 Unsigned) id__div32u_rem (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Osub (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))
    40             ) (
    41             St_assign (ASTint I32 Unsigned) id__div32u_quo (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Oadd (Id (ASTint I32 Unsigned) id__div32u_quo) (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    42             )
    43             )
    44           )
    45           )
    46         )
     33      St_seq (
     34        St_label L_tmp_0 (
     35        St_seq (
     36          St_ifthenelse I32 Signed (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocmpu Cge) (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y)) (
     37            St_skip          ) (
     38            St_goto L_tmp_1
     39          )
     40        ) (
     41        St_seq (
     42          St_cost C_cost0 (
     43          St_seq (
     44            St_assign (ASTint I32 Unsigned) id__div32u_rem (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Osub (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))
     45          ) (
     46          St_assign (ASTint I32 Unsigned) id__div32u_quo (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Oadd (Id (ASTint I32 Unsigned) id__div32u_quo) (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
     47          )
     48          )
     49        ) (
     50        St_goto L_tmp_0
     51        )
     52        )
     53        )
     54      ) (
     55      St_label L_tmp_1 (
     56      St_skip      )
    4757      )
    4858    ) (
     
    5161    )
    5262  ) (
    53   St_return (Some ? (dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32u_quo)))
    54   )
    55   )
    56   )
    57   )
    58 
    59 )).
    60 
    61 definition id__div32s := ident_of_nat 8.
    62 definition id__div32s__tmp2 := ident_of_nat 14.
    63 definition id__div32s_sign := ident_of_nat 15.
    64 definition id__div32s_x1 := ident_of_nat 16.
    65 definition id__div32s_y1 := ident_of_nat 17.
    66 definition id__div32s__tmp_0 := ident_of_nat 18.
    67 definition id__div32s_x := ident_of_nat 19.
    68 definition id__div32s_y := ident_of_nat 20.
    69 definition C_cost7 := costlabel_of_nat 13.
    70 definition C_cost5 := costlabel_of_nat 12.
    71 definition C_cost6 := costlabel_of_nat 11.
    72 definition C_cost3 := costlabel_of_nat 10.
    73 definition C_cost4 := costlabel_of_nat 9.
     63  St_return (Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32u_quo)))
     64  )
     65  )
     66  )
     67  )
     68
     69) (match daemon in False with [ ])).
     70
     71definition id__div32s := ident_of_nat 10.
     72definition id__div32s__tmp2 := ident_of_nat 16.
     73definition id__div32s_sign := ident_of_nat 17.
     74definition id__div32s_x1 := ident_of_nat 18.
     75definition id__div32s_y1 := ident_of_nat 19.
     76definition id__div32s__tmp_2 := ident_of_nat 20.
     77definition id__div32s_x := ident_of_nat 21.
     78definition id__div32s_y := ident_of_nat 22.
     79definition C_cost7 := costlabel_of_nat 15.
     80definition C_cost5 := costlabel_of_nat 14.
     81definition C_cost6 := costlabel_of_nat 13.
     82definition C_cost3 := costlabel_of_nat 12.
     83definition C_cost4 := costlabel_of_nat 11.
    7484definition f__div32s := Internal ? (mk_internal_function
    7585  (Some ? (ASTint I32 Signed))
    76   [pair ?? id__div32s_x (ASTint I32 Signed); pair ?? id__div32s_y (ASTint I32 Signed)]
    77   [pair ?? id__div32s__tmp2 (ASTint I32 Unsigned); pair ?? id__div32s_sign (ASTint I32 Signed); pair ?? id__div32s_x1 (ASTint I32 Unsigned); pair ?? id__div32s_y1 (ASTint I32 Unsigned); pair ?? id__div32s__tmp_0 (ASTint I32 Unsigned)]
    78   0 (
     86  [mk_Prod ?? id__div32s_x (ASTint I32 Signed); mk_Prod ?? id__div32s_y (ASTint I32 Signed)]
     87  [mk_Prod ?? id__div32s__tmp2 (ASTint I32 Unsigned); mk_Prod ?? id__div32s_sign (ASTint I32 Signed); mk_Prod ?? id__div32s_x1 (ASTint I32 Unsigned); mk_Prod ?? id__div32s_y1 (ASTint I32 Unsigned); mk_Prod ?? id__div32s__tmp_2 (ASTint I32 Unsigned)]
     88  (match daemon in False with [ ])
     890 (
    7990  St_cost C_cost7 (
    8091  St_seq (
    81     St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Id (ASTint I32 Signed) id__div32s_x))
    82   ) (
    83   St_seq (
    84     St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Id (ASTint I32 Signed) id__div32s_y))
    85   ) (
    86   St_seq (
    87     St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
     92    St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id__div32s_x))
     93  ) (
     94  St_seq (
     95    St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id__div32s_y))
     96  ) (
     97  St_seq (
     98    St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
    8899  ) (
    89100  St_seq (
     
    91102      St_cost C_cost5 (
    92103      St_seq (
    93         St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_x)))
     104        St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_x)))
    94105      ) (
    95       St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     106      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_sign))
    96107      )
    97108      )
     
    105116      St_cost C_cost3 (
    106117      St_seq (
    107         St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_y)))
     118        St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_y)))
    108119      ) (
    109       St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     120      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Id (ASTint I32 Signed) id__div32s_sign))
    110121      )
    111122      )
     
    117128  St_seq (
    118129    St_seq (
    119       St_call (Some ? id__div32s__tmp_0) (Cst ? (Oaddrsymbol id__div32u 0)) [dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_x1); dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_y1)]
    120     ) (
    121     St_assign (ASTint I32 Unsigned) id__div32s__tmp2 (Id (ASTint I32 Unsigned) id__div32s__tmp_0)
    122     )
    123   ) (
    124   St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id__div32s_sign) (Op1 (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I32 Unsigned) id__div32s__tmp2)))))
    125   )
    126   )
    127   )
    128   )
    129   )
    130   )
    131   )
    132 
    133 )).
    134 
    135 definition id_search := ident_of_nat 21.
    136 definition id_search__tmp4 := ident_of_nat 31.
    137 definition id_search_high := ident_of_nat 32.
    138 definition id_search_i := ident_of_nat 33.
    139 definition id_search_low := ident_of_nat 34.
    140 definition id_search__tmp_1 := ident_of_nat 35.
    141 definition id_search_tab := ident_of_nat 36.
    142 definition id_search_size := ident_of_nat 37.
    143 definition id_search_to_find := ident_of_nat 38.
    144 definition C_cost16 := costlabel_of_nat 30.
    145 definition C_cost14 := costlabel_of_nat 29.
    146 definition C_cost12 := costlabel_of_nat 28.
    147 definition C_cost13 := costlabel_of_nat 27.
    148 definition C_cost10 := costlabel_of_nat 26.
    149 definition C_cost11 := costlabel_of_nat 25.
    150 definition C_cost8 := costlabel_of_nat 24.
    151 definition C_cost9 := costlabel_of_nat 23.
    152 definition C_cost15 := costlabel_of_nat 22.
     130      St_call (Some ? (mk_Prod ?? id__div32s__tmp_2 (ASTint I32 Unsigned))) (Cst ? (Oaddrsymbol id__div32u 0)) [mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_x1); mk_DPair ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_y1)]
     131    ) (
     132    St_assign (ASTint I32 Unsigned) id__div32s__tmp2 (Id (ASTint I32 Unsigned) id__div32s__tmp_2)
     133    )
     134  ) (
     135  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id__div32s_sign) (Op1 (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I32 Unsigned) id__div32s__tmp2)))))
     136  )
     137  )
     138  )
     139  )
     140  )
     141  )
     142  )
     143
     144) (match daemon in False with [ ])).
     145
     146definition id_search := ident_of_nat 23.
     147definition id_search__tmp4 := ident_of_nat 35.
     148definition id_search_high := ident_of_nat 36.
     149definition id_search_i := ident_of_nat 37.
     150definition id_search_low := ident_of_nat 38.
     151definition id_search__tmp_5 := ident_of_nat 39.
     152definition id_search_tab := ident_of_nat 40.
     153definition id_search_size := ident_of_nat 41.
     154definition id_search_to_find := ident_of_nat 42.
     155definition C_cost16 := costlabel_of_nat 34.
     156definition L_tmp_3 := label_of_nat 33.
     157definition C_cost14 := costlabel_of_nat 32.
     158definition C_cost12 := costlabel_of_nat 31.
     159definition C_cost13 := costlabel_of_nat 30.
     160definition C_cost10 := costlabel_of_nat 29.
     161definition C_cost11 := costlabel_of_nat 28.
     162definition C_cost8 := costlabel_of_nat 27.
     163definition C_cost9 := costlabel_of_nat 26.
     164definition L_tmp_4 := label_of_nat 25.
     165definition C_cost15 := costlabel_of_nat 24.
    153166definition f_search := Internal ? (mk_internal_function
    154167  (Some ? (ASTint I8 Unsigned))
    155   [pair ?? id_search_tab (ASTptr Any); pair ?? id_search_size (ASTint I8 Unsigned); pair ?? id_search_to_find (ASTint I8 Unsigned)]
    156   [pair ?? id_search__tmp4 (ASTint I32 Signed); pair ?? id_search_high (ASTint I8 Unsigned); pair ?? id_search_i (ASTint I8 Unsigned); pair ?? id_search_low (ASTint I8 Unsigned); pair ?? id_search__tmp_1 (ASTint I32 Signed)]
    157   0 (
     168  [mk_Prod ?? id_search_tab (ASTptr Any); mk_Prod ?? id_search_size (ASTint I8 Unsigned); mk_Prod ?? id_search_to_find (ASTint I8 Unsigned)]
     169  [mk_Prod ?? id_search__tmp4 (ASTint I32 Signed); mk_Prod ?? id_search_high (ASTint I8 Unsigned); mk_Prod ?? id_search_i (ASTint I8 Unsigned); mk_Prod ?? id_search_low (ASTint I8 Unsigned); mk_Prod ?? id_search__tmp_5 (ASTint I32 Signed)]
     170  (match daemon in False with [ ])
     1710 (
    158172  St_cost C_cost16 (
    159173  St_seq (
    160     St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    161   ) (
    162   St_seq (
    163     St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_size)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
     174    St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     175  ) (
     176  St_seq (
     177    St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_size)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    164178  ) (
    165179  St_seq (
    166180    St_seq (
    167       St_block (
    168         St_loop (
    169           St_seq (
    170             St_ifthenelse I32 Signed (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onotbool (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cge) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_low)))) (
    171               St_exit 0
     181      St_seq (
     182        St_label L_tmp_3 (
     183        St_seq (
     184          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cge) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_low))) (
     185            St_skip          ) (
     186            St_goto L_tmp_4
     187          )
     188        ) (
     189        St_seq (
     190          St_cost C_cost14 (
     191          St_seq (
     192            St_seq (
     193              St_call (Some ? (mk_Prod ?? id_search__tmp_5 (ASTint I32 Signed))) (Cst ? (Oaddrsymbol id__div32s 0)) [mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_low))); mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))]
    172194            ) (
    173               St_skip            )
    174           ) (
    175           St_block (
    176             St_cost C_cost14 (
    177             St_seq (
    178               St_seq (
    179                 St_call (Some ? id_search__tmp_1) (Cst ? (Oaddrsymbol id__div32s 0)) [dp ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_low))); dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))]
    180               ) (
    181               St_assign (ASTint I32 Signed) id_search__tmp4 (Id (ASTint I32 Signed) id_search__tmp_1)
     195            St_assign (ASTint I32 Signed) id_search__tmp4 (Id (ASTint I32 Signed) id_search__tmp_5)
     196            )
     197          ) (
     198          St_seq (
     199            St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Id (ASTint I32 Signed) id_search__tmp4))
     200          ) (
     201          St_seq (
     202            St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Ceq) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     203              St_cost C_cost12 (
     204              St_return (Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
    182205              )
    183206            ) (
    184             St_seq (
    185               St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Id (ASTint I32 Signed) id_search__tmp4))
    186             ) (
    187             St_seq (
    188               St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Ceq) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
    189                 St_cost C_cost12 (
    190                 St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
    191                 )
    192               ) (
    193                 St_cost C_cost13 (
    194                 St_skip                )
     207              St_cost C_cost13 (
     208              St_skip              )
     209            )
     210          ) (
     211          St_seq (
     212            St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     213              St_cost C_cost10 (
     214              St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    195215              )
    196216            ) (
    197             St_seq (
    198               St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
    199                 St_cost C_cost10 (
    200                 St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    201                 )
    202               ) (
    203                 St_cost C_cost11 (
    204                 St_skip                )
    205               )
    206             ) (
    207             St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
    208               St_cost C_cost8 (
    209               St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    210               )
    211             ) (
    212               St_cost C_cost9 (
     217              St_cost C_cost11 (
    213218              St_skip              )
    214219            )
     220          ) (
     221          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     222            St_cost C_cost8 (
     223            St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    215224            )
    216             )
    217             )
    218             )
    219             )
    220           )
    221           )
    222         )
     225          ) (
     226            St_cost C_cost9 (
     227            St_skip            )
     228          )
     229          )
     230          )
     231          )
     232          )
     233          )
     234        ) (
     235        St_goto L_tmp_3
     236        )
     237        )
     238        )
     239      ) (
     240      St_label L_tmp_4 (
     241      St_skip      )
    223242      )
    224243    ) (
     
    227246    )
    228247  ) (
    229   St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))))
    230   )
    231   )
    232   )
    233   )
    234 
    235 )).
    236 
    237 definition id_main := ident_of_nat 39.
    238 definition id_main_res := ident_of_nat 41.
    239 definition id_main__tmp_2 := ident_of_nat 42.
    240 definition C_cost17 := costlabel_of_nat 40.
     248  St_return (Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) (Onegint ??) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))))
     249  )
     250  )
     251  )
     252  )
     253
     254) (match daemon in False with [ ])).
     255
     256definition id_main := ident_of_nat 43.
     257definition id_main_res := ident_of_nat 45.
     258definition id_main__tmp_6 := ident_of_nat 46.
     259definition C_cost17 := costlabel_of_nat 44.
    241260definition f_main := Internal ? (mk_internal_function
    242261  (Some ? (ASTint I32 Signed))
    243262  []
    244   [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp_2 (ASTint I8 Unsigned)]
    245   5 (
     263  [mk_Prod ?? id_main_res (ASTint I8 Unsigned); mk_Prod ?? id_main__tmp_6 (ASTint I8 Unsigned)]
     264  (match daemon in False with [ ])
     2655 (
    246266  St_cost C_cost17 (
    247267  St_seq (
    248     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    249   ) (
    250   St_seq (
    251     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
    252   ) (
    253   St_seq (
    254     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 2))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
    255   ) (
    256   St_seq (
    257     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 3))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
    258   ) (
    259   St_seq (
    260     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 4))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
     268    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     269  ) (
     270  St_seq (
     271    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
     272  ) (
     273  St_seq (
     274    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 2))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
     275  ) (
     276  St_seq (
     277    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 3))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
     278  ) (
     279  St_seq (
     280    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 4))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
    261281  ) (
    262282  St_seq (
    263283    St_seq (
    264       St_call (Some ? id_main__tmp_2) (Cst ? (Oaddrsymbol id_search 0)) [dp ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 5)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))]
    265     ) (
    266     St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp_2)
    267     )
    268   ) (
    269   St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_main_res))))
    270   )
    271   )
    272   )
    273   )
    274   )
    275   )
    276   )
    277 
    278 )).
     284      St_call (Some ? (mk_Prod ?? id_main__tmp_6 (ASTint I8 Unsigned))) (Cst ? (Oaddrsymbol id_search 0)) [mk_DPair ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))); mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 5)))); mk_DPair ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))]
     285    ) (
     286    St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp_6)
     287    )
     288  ) (
     289  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint ????) (Id (ASTint I8 Unsigned) id_main_res))))
     290  )
     291  )
     292  )
     293  )
     294  )
     295  )
     296  )
     297
     298) (match daemon in False with [ ])).
    279299
    280300
     
    282302definition myprog : Cminor_program :=
    283303mk_program ?? [] [
    284   (pair ?? id__div32u f__div32u);
    285   (pair ?? id__div32s f__div32s);
    286   (pair ?? id_search f_search);
    287   (pair ?? id_main f_main)
     304  (mk_Prod ?? id__div32u f__div32u);
     305  (mk_Prod ?? id__div32s f__div32s);
     306  (mk_Prod ?? id_search f_search);
     307  (mk_Prod ?? id_main f_main)
    288308]  id_main
    289309.
Note: See TracChangeset for help on using the changeset viewer.