Changeset 1157


Ignore:
Timestamp:
Aug 31, 2011, 12:15:39 PM (8 years ago)
Author:
campbell
Message:

Update pretty printers and examples.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r965 r1157  
    367367
    368368let print_globvar p (((id, init), ty)) =
    369   fprintf p "@[<hov 2>〈〈〈ident_of_nat %i (* %s *),@ %a〉,@ Any〉,@ %s〉@]"
     369  fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ Any〉,@ 〈%a,@ %s〉〉@]"
    370370    (id_i id)
    371371    id
     
    466466  collect_program prog;
    467467  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
    468   fprintf p "@[<v 2>definition myprog := mk_program clight_fundef type@ ";
     468  fprintf p "@[<v 2>definition myprog := mk_program clight_fundef ((list init_data) × type)@ ";
    469469(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    470470  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
  • src/Clight/test/duff.c.ma

    r965 r1157  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* copy *), CL_Internal (
    66     mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     
    409409
    410410example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    411 normalize @refl
     411normalize  (* you can examine the result here *)
     412@refl
    412413qed.
  • src/Clight/test/factorial.c.ma

    r978 r1157  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    66  〈ident_of_nat 1 (* main *), CL_Internal (
     
    4141example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    4242normalize  (* you can examine the result here *)
    43 @refl qed.
     43@refl
     44qed.
  • src/Cminor/cminorMatitaPrinter.ml

    r966 r1157  
    2828
    2929let print_var n (id, sz, init) =
    30   Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
     30  Printf.sprintf "(pair ?? (pair ?? id_%s Any) [%s])"
    3131    id
    3232    (match init with
  • src/Cminor/test/search.Cminor.ma

    r966 r1157  
    44
    55
    6 definition id_search := ident_of_nat 0.
    7 definition id_search_high := ident_of_nat 10.
    8 definition id_search_i := ident_of_nat 11.
    9 definition id_search_low := ident_of_nat 12.
    10 definition id_search_tab := ident_of_nat 13.
    11 definition id_search_size := ident_of_nat 14.
    12 definition id_search_to_find := ident_of_nat 15.
    13 definition C_cost8 := costlabel_of_nat 9.
    14 definition C_cost6 := costlabel_of_nat 8.
    15 definition C_cost4 := costlabel_of_nat 7.
    16 definition C_cost5 := costlabel_of_nat 6.
    17 definition C_cost2 := costlabel_of_nat 5.
    18 definition C_cost3 := costlabel_of_nat 4.
    19 definition C_cost0 := costlabel_of_nat 3.
    20 definition C_cost1 := costlabel_of_nat 2.
    21 definition C_cost7 := costlabel_of_nat 1.
    22 definition f_search := Internal ? (mk_internal_function
    23   (Some ? (ASTint I8 Unsigned))
    24   [pair ?? id_search_tab (ASTptr Any); pair ?? id_search_size (ASTint I8 Unsigned); pair ?? id_search_to_find (ASTint I8 Unsigned)]
    25   [pair ?? id_search_high (ASTint I8 Unsigned); pair ?? id_search_i (ASTint I8 Unsigned); pair ?? id_search_low (ASTint I8 Unsigned)]
     6definition id__div32u := ident_of_nat 0.
     7definition id__div32u_quo := ident_of_nat 4.
     8definition id__div32u_rem := ident_of_nat 5.
     9definition id__div32u_x := ident_of_nat 6.
     10definition id__div32u_y := ident_of_nat 7.
     11definition C_cost2 := costlabel_of_nat 3.
     12definition C_cost0 := costlabel_of_nat 2.
     13definition C_cost1 := costlabel_of_nat 1.
     14definition f__div32u := Internal ? (mk_internal_function
     15  (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)]
    2618  0 (
    27   St_cost C_cost8 (
    28   St_seq (
    29     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))))
    30   ) (
    31   St_seq (
    32     St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_size) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     19  St_cost C_cost2 (
     20  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))))
     22  ) (
     23  St_seq (
     24    St_assign (ASTint I32 Unsigned) id__div32u_rem (Id (ASTint I32 Unsigned) id__div32u_x)
    3325  ) (
    3426  St_seq (
     
    3729        St_loop (
    3830          St_seq (
    39             St_ifthenelse I8 Unsigned (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Onotbool (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cge) (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) id_search_low))) (
     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))) (
    4032              St_exit 0
    4133            ) (
     
    4335          ) (
    4436          St_block (
    45             St_cost C_cost6 (
    46             St_seq (
    47               St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Odivu (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) id_search_low)) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 2)))))
    48             ) (
    49             St_seq (
    50               St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Ceq) (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)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    51                 St_cost C_cost4 (
     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        )
     47      )
     48    ) (
     49    St_cost C_cost1 (
     50    St_skip    )
     51    )
     52  ) (
     53  St_return (Some ? (dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32u_quo)))
     54  )
     55  )
     56  )
     57  )
     58
     59)).
     60
     61definition id__div32s := ident_of_nat 8.
     62definition id__div32s__tmp2 := ident_of_nat 14.
     63definition id__div32s_sign := ident_of_nat 15.
     64definition id__div32s_x1 := ident_of_nat 16.
     65definition id__div32s_y1 := ident_of_nat 17.
     66definition id__div32s__tmp_0 := ident_of_nat 18.
     67definition id__div32s_x := ident_of_nat 19.
     68definition id__div32s_y := ident_of_nat 20.
     69definition C_cost7 := costlabel_of_nat 13.
     70definition C_cost5 := costlabel_of_nat 12.
     71definition C_cost6 := costlabel_of_nat 11.
     72definition C_cost3 := costlabel_of_nat 10.
     73definition C_cost4 := costlabel_of_nat 9.
     74definition f__div32s := Internal ? (mk_internal_function
     75  (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 (
     79  St_cost C_cost7 (
     80  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))))
     88  ) (
     89  St_seq (
     90    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_x) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
     91      St_cost C_cost5 (
     92      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)))
     94      ) (
     95      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     96      )
     97      )
     98    ) (
     99      St_cost C_cost6 (
     100      St_skip      )
     101    )
     102  ) (
     103  St_seq (
     104    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_y) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
     105      St_cost C_cost3 (
     106      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)))
     108      ) (
     109      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     110      )
     111      )
     112    ) (
     113      St_cost C_cost4 (
     114      St_skip      )
     115    )
     116  ) (
     117  St_seq (
     118    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
     135definition id_search := ident_of_nat 21.
     136definition id_search__tmp4 := ident_of_nat 31.
     137definition id_search_high := ident_of_nat 32.
     138definition id_search_i := ident_of_nat 33.
     139definition id_search_low := ident_of_nat 34.
     140definition id_search__tmp_1 := ident_of_nat 35.
     141definition id_search_tab := ident_of_nat 36.
     142definition id_search_size := ident_of_nat 37.
     143definition id_search_to_find := ident_of_nat 38.
     144definition C_cost16 := costlabel_of_nat 30.
     145definition C_cost14 := costlabel_of_nat 29.
     146definition C_cost12 := costlabel_of_nat 28.
     147definition C_cost13 := costlabel_of_nat 27.
     148definition C_cost10 := costlabel_of_nat 26.
     149definition C_cost11 := costlabel_of_nat 25.
     150definition C_cost8 := costlabel_of_nat 24.
     151definition C_cost9 := costlabel_of_nat 23.
     152definition C_cost15 := costlabel_of_nat 22.
     153definition f_search := Internal ? (mk_internal_function
     154  (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 (
     158  St_cost C_cost16 (
     159  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)))))
     164  ) (
     165  St_seq (
     166    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
     172            ) (
     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)
     182              )
     183            ) (
     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 (
    52190                St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
    53191                )
    54192              ) (
    55                 St_cost C_cost5 (
     193                St_cost C_cost13 (
    56194                St_skip                )
    57195              )
    58196            ) (
    59197            St_seq (
    60               St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cgt) (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)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    61                 St_cost C_cost2 (
    62                 St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     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)))))
    63201                )
    64202              ) (
    65                 St_cost C_cost3 (
     203                St_cost C_cost11 (
    66204                St_skip                )
    67205              )
    68206            ) (
    69             St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Clt) (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)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    70               St_cost C_cost0 (
    71               St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     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)))))
    72210              )
    73211            ) (
    74               St_cost C_cost1 (
     212              St_cost C_cost9 (
    75213              St_skip              )
     214            )
    76215            )
    77216            )
     
    84223      )
    85224    ) (
    86     St_cost C_cost7 (
     225    St_cost C_cost15 (
    87226    St_skip    )
    88227    )
    89228  ) (
    90   St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op1 (ASTint I8 Signed) (ASTint I8 Signed) Onegint (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))))
     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)))))))
    91230  )
    92231  )
     
    96235)).
    97236
    98 definition id_main := ident_of_nat 16.
    99 definition id_main_res := ident_of_nat 18.
    100 definition id_main__tmp0 := ident_of_nat 19.
    101 definition C_cost9 := costlabel_of_nat 17.
     237definition id_main := ident_of_nat 39.
     238definition id_main_res := ident_of_nat 41.
     239definition id_main__tmp_2 := ident_of_nat 42.
     240definition C_cost17 := costlabel_of_nat 40.
    102241definition f_main := Internal ? (mk_internal_function
    103242  (Some ? (ASTint I32 Signed))
    104243  []
    105   [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp0 (ASTint I8 Unsigned)]
     244  [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp_2 (ASTint I8 Unsigned)]
    106245  5 (
    107   St_cost C_cost9 (
    108   St_seq (
    109     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 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 I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    110   ) (
    111   St_seq (
    112     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 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 I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
    113   ) (
    114   St_seq (
    115     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 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 I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
    116   ) (
    117   St_seq (
    118     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 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 I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 3))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
    119   ) (
    120   St_seq (
    121     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 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 I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 4))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
     246  St_cost C_cost17 (
     247  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))))
    122261  ) (
    123262  St_seq (
    124263    St_seq (
    125       St_call (Some ? id_main__tmp0) (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))))]
    126     ) (
    127     St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp0)
     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)
    128267    )
    129268  ) (
     
    143282definition myprog : Cminor_program :=
    144283mk_program ?? [
     284  (pair ?? id__div32u f__div32u);
     285  (pair ?? id__div32s f__div32s);
    145286  (pair ?? id_search f_search);
    146287  (pair ?? id_main f_main)
     
    157298include "RTLabs/semantics.ma".
    158299
    159 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
     300example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    160301normalize  (* you can examine the result here *)
    161302@refl
    162303qed.
    163304
     305
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r967 r1157  
    1616
    1717let print_global (x, size) =
    18   Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x
     18  Printf.sprintf "pair ?? (pair ?? id_%s Any) %d" x
    1919    (Driver.RTLabsMemory.concrete_size size)
    2020
     
    2525    (MiscPottier.string_of_list (";\n"^n_spaces n) print_global globs)
    2626
     27let print_label l = "lbl_" ^ l
    2728
    2829let rec print_args args =
     
    130131let rec print_table = function
    131132  | [] -> ""
    132   | [lbl] -> lbl
    133   | lbl :: tbl -> lbl ^ "; " ^ (print_table tbl)
     133  | [lbl] -> print_label lbl
     134  | lbl :: tbl -> (print_label lbl) ^ "; " ^ (print_table tbl)
    134135
    135136
    136137let print_statement lookup_type = function
    137   | RTLabs.St_skip lbl -> "make_St_skip " ^ lbl
     138  | RTLabs.St_skip lbl -> "make_St_skip " ^ (print_label lbl)
    138139  | RTLabs.St_cost (cost_lbl, lbl) ->
    139       Printf.sprintf "make_St_cost C%s %s" cost_lbl lbl
     140      Printf.sprintf "make_St_cost C%s %s" cost_lbl (print_label lbl)
    140141  | RTLabs.St_cst (dests, cst, lbl) ->
    141142      Printf.sprintf "make_St_const %s (%s) %s"
    142143        (Register.print dests)
    143144        (print_constant (lookup_type dests) cst)
    144         lbl
     145        (print_label lbl)
    145146  | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
    146147      Printf.sprintf "make_St_op1 %s %s %s %s"
     
    148149        (Register.print dests)
    149150        (Register.print srcs)
    150         lbl
     151        (print_label lbl)
    151152  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    152153      Printf.sprintf "make_St_op2 %s %s %s %s %s"
     
    155156        (Register.print srcs1)
    156157        (Register.print srcs2)
    157         lbl
     158        (print_label lbl)
    158159  | RTLabs.St_load (chunk, addr, dests, lbl) ->
    159160      Printf.sprintf "make_St_load %s %s %s %s"
     
    161162        (Register.print addr)
    162163        (Register.print dests)
    163         lbl
     164        (print_label lbl)
    164165  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
    165166      Printf.sprintf "make_St_store %s %s %s %s"
     
    167168        (Register.print addr)
    168169        (Register.print srcs)
    169         lbl
     170        (print_label lbl)
    170171  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    171172      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
     
    173174        (print_params args)
    174175        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
    175         lbl
     176        (print_label lbl)
    176177  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    177178      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
     
    179180        (print_params args)
    180181        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
    181         lbl
     182        (print_label lbl)
    182183  | RTLabs.St_tailcall_id (f, args, sg) ->
    183184      Printf.sprintf "make_St_tailcall_id id_%s %s"
     
    191192      Printf.sprintf "make_St_cond %s %s %s"
    192193        (Register.print srcs)
    193         lbl_true
    194         lbl_false
     194        (print_label lbl_true)
     195        (print_label lbl_false)
    195196  | RTLabs.St_jumptable (rs, tbl) ->
    196197      Printf.sprintf "make_St_jumptable %s [%s]"
     
    218219    Printf.sprintf "%sdefinition %s := %d.\n%s"
    219220      (n_spaces n)
    220       lbl
     221      (print_label lbl)
    221222      i
    222223      s
     
    228229    Printf.sprintf "%s(pair ?? %s (%s))%s\n%s"
    229230      (n_spaces n)
    230       lbl
     231      (print_label lbl)
    231232      (print_statement lookup_type stmt)
    232233      (if s = "" then "\n]" else ";")
     
    259260    (print_graph (n+2) lookup_type def.RTLabs.f_graph)
    260261    (n_spaces (n+2))
    261     def.RTLabs.f_entry
    262     (n_spaces (n+2))
    263     def.RTLabs.f_exit
     262    (print_label def.RTLabs.f_entry)
     263    (n_spaces (n+2))
     264    (print_label def.RTLabs.f_exit)
    264265
    265266
  • src/RTLabs/test/search.RTLabs.ma

    r967 r1157  
    55
    66
    7   definition id_search := ident_of_nat 0.
    8   definition search9 := 50.
    9   definition search8 := 49.
    10   definition search7 := 48.
    11   definition search6 := 47.
    12   definition search50 := 46.
    13   definition search5 := 45.
    14   definition search49 := 44.
    15   definition search48 := 43.
    16   definition search47 := 42.
    17   definition search46 := 41.
    18   definition search45 := 40.
    19   definition search44 := 39.
    20   definition search43 := 38.
    21   definition search42 := 37.
    22   definition search41 := 36.
    23   definition search40 := 35.
    24   definition search4 := 34.
    25   definition search39 := 33.
    26   definition search38 := 32.
    27   definition search37 := 31.
    28   definition search36 := 30.
    29   definition search35 := 29.
    30   definition search34 := 28.
    31   definition search33 := 27.
    32   definition search32 := 26.
    33   definition search31 := 25.
    34   definition search30 := 24.
    35   definition search3 := 23.
    36   definition search29 := 22.
    37   definition search28 := 21.
    38   definition search27 := 20.
    39   definition search26 := 19.
    40   definition search25 := 18.
    41   definition search24 := 17.
    42   definition search23 := 16.
    43   definition search22 := 15.
    44   definition search21 := 14.
    45   definition search20 := 13.
    46   definition search2 := 12.
    47   definition search19 := 11.
    48   definition search18 := 10.
    49   definition search17 := 9.
    50   definition search16 := 8.
    51   definition search15 := 7.
    52   definition search14 := 6.
    53   definition search13 := 5.
    54   definition search12 := 4.
    55   definition search11 := 3.
    56   definition search10 := 2.
    57   definition search1 := 1.
    58   definition search0 := 0.
    59   definition C_cost1 := costlabel_of_nat 8.
    60   definition C_cost8 := costlabel_of_nat 7.
    61   definition C_cost6 := costlabel_of_nat 6.
    62   definition C_cost7 := costlabel_of_nat 5.
    63   definition C_cost4 := costlabel_of_nat 4.
    64   definition C_cost5 := costlabel_of_nat 3.
    65   definition C_cost2 := costlabel_of_nat 2.
    66   definition C_cost3 := costlabel_of_nat 1.
    67   definition C_cost0 := costlabel_of_nat 0.
    68 
    69 
    70   definition pre_search := mk_pre_internal_function
    71     (Some ? (pair ?? 6 (ASTint I8 Unsigned)))
    72     [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
    73     [(pair ?? 3 (ASTint I8 Unsigned)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTint I8 Signed)); (pair ?? 9 (ASTint I8 Unsigned)); (pair ?? 10 (ASTint I8 Unsigned)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Unsigned)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Unsigned)); (pair ?? 16 (ASTint I8 Unsigned)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTptr Any)); (pair ?? 21 (ASTint I8 Unsigned)); (pair ?? 22 (ASTint I8 Unsigned)); (pair ?? 23 (ASTint I8 Unsigned)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I8 Unsigned)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTint I8 Unsigned)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I8 Unsigned)); (pair ?? 32 (ASTint I8 Unsigned)); (pair ?? 33 (ASTint I8 Unsigned)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTint I8 Signed))]
     7  definition id__div32u := ident_of_nat 0.
     8  definition lbl__div32u9 := 15.
     9  definition lbl__div32u8 := 14.
     10  definition lbl__div32u7 := 13.
     11  definition lbl__div32u6 := 12.
     12  definition lbl__div32u5 := 11.
     13  definition lbl__div32u4 := 10.
     14  definition lbl__div32u3 := 9.
     15  definition lbl__div32u2 := 8.
     16  definition lbl__div32u15 := 7.
     17  definition lbl__div32u14 := 6.
     18  definition lbl__div32u13 := 5.
     19  definition lbl__div32u12 := 4.
     20  definition lbl__div32u11 := 3.
     21  definition lbl__div32u10 := 2.
     22  definition lbl__div32u1 := 1.
     23  definition lbl__div32u0 := 0.
     24  definition C_cost0 := costlabel_of_nat 2.
     25  definition C_cost1 := costlabel_of_nat 1.
     26  definition C_cost2 := costlabel_of_nat 0.
     27
     28
     29  definition pre__div32u := mk_pre_internal_function
     30    (Some ? (pair ?? 4 (ASTint I32 Unsigned)))
     31    [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))]
     32    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))]
    7433    0
    7534    [
    76     (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8));
    77     (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7));
    78     (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5));
    79     (pair ?? search6 (make_St_cost C_cost1 search5));
    80     (pair ?? search50 (make_St_cost C_cost8 search49));
    81     (pair ?? search5 (make_St_skip search44));
    82     (pair ?? search49 (make_St_const 35 (Ointconst I8 (repr ? 0)) search48));
    83     (pair ?? search48 (make_St_op1 (Ocastint Signed I8) 5 35 search47));
    84     (pair ?? search47 (make_St_const 34 (Ointconst I8 (repr ? 1)) search46));
    85     (pair ?? search46 (make_St_op2 Osub 33 1 34 search45));
    86     (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5));
    87     (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43));
    88     (pair ?? search43 (make_St_op1 Onotbool 31 32 search42));
    89     (pair ?? search42 (make_St_cond 31 search4 search41));
    90     (pair ?? search41 (make_St_cost C_cost6 search40));
    91     (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39));
    92     (pair ?? search4 (make_St_cost C_cost7 search3));
    93     (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38));
    94     (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37));
    95     (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36));
    96     (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35));
    97     (pair ?? search35 (make_St_op2 Omul 26 4 27 search34));
    98     (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33));
    99     (pair ?? search33 (make_St_load Mint8unsigned 25 24 search32));
    100     (pair ?? search32 (make_St_op2 (Ocmpu Ceq) 23 24 2 search31));
    101     (pair ?? search31 (make_St_cond 23 search30 search28));
    102     (pair ?? search30 (make_St_cost C_cost4 search29));
    103     (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2));
    104     (pair ?? search29 (make_St_op1 Oid 6 4 search0));
    105     (pair ?? search28 (make_St_cost C_cost5 search27));
    106     (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26));
    107     (pair ?? search26 (make_St_op2 Omul 21 4 22 search25));
    108     (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24));
    109     (pair ?? search24 (make_St_load Mint8unsigned 20 19 search23));
    110     (pair ?? search23 (make_St_op2 (Ocmpu Cgt) 18 19 2 search22));
    111     (pair ?? search22 (make_St_cond 18 search21 search17));
    112     (pair ?? search21 (make_St_cost C_cost2 search20));
    113     (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19));
    114     (pair ?? search2 (make_St_op1 Onegint 7 8 search1));
    115     (pair ?? search19 (make_St_op2 Osub 16 4 17 search18));
    116     (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16));
    117     (pair ?? search17 (make_St_cost C_cost3 search16));
    118     (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15));
    119     (pair ?? search15 (make_St_op2 Omul 14 4 15 search14));
    120     (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13));
    121     (pair ?? search13 (make_St_load Mint8unsigned 13 12 search12));
    122     (pair ?? search12 (make_St_op2 (Ocmpu Clt) 11 12 2 search11));
    123     (pair ?? search11 (make_St_cond 11 search10 search6));
    124     (pair ?? search10 (make_St_cost C_cost0 search9));
    125     (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0));
    126     (pair ?? search0 (make_St_return))
     35    (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8));
     36    (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7));
     37    (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6));
     38    (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5));
     39    (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4));
     40    (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3));
     41    (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11));
     42    (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1));
     43    (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14));
     44    (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13));
     45    (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12));
     46    (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3));
     47    (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10));
     48    (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9));
     49    (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0));
     50    (pair ?? lbl__div32u0 (make_St_return))
    12751]
    12852
    129     search50
    130     search0.
    131 
    132   definition id_main := ident_of_nat 1.
    133   definition main9 := 61.
    134   definition main8 := 60.
    135   definition main7 := 59.
    136   definition main61 := 58.
    137   definition main60 := 57.
    138   definition main6 := 56.
    139   definition main59 := 55.
    140   definition main58 := 54.
    141   definition main57 := 53.
    142   definition main56 := 52.
    143   definition main55 := 51.
    144   definition main54 := 50.
    145   definition main53 := 49.
    146   definition main52 := 48.
    147   definition main51 := 47.
    148   definition main50 := 46.
    149   definition main5 := 45.
    150   definition main49 := 44.
    151   definition main48 := 43.
    152   definition main47 := 42.
    153   definition main46 := 41.
    154   definition main45 := 40.
    155   definition main44 := 39.
    156   definition main43 := 38.
    157   definition main42 := 37.
    158   definition main41 := 36.
    159   definition main40 := 35.
    160   definition main4 := 34.
    161   definition main39 := 33.
    162   definition main38 := 32.
    163   definition main37 := 31.
    164   definition main36 := 30.
    165   definition main35 := 29.
    166   definition main34 := 28.
    167   definition main33 := 27.
    168   definition main32 := 26.
    169   definition main31 := 25.
    170   definition main30 := 24.
    171   definition main3 := 23.
    172   definition main29 := 22.
    173   definition main28 := 21.
    174   definition main27 := 20.
    175   definition main26 := 19.
    176   definition main25 := 18.
    177   definition main24 := 17.
    178   definition main23 := 16.
    179   definition main22 := 15.
    180   definition main21 := 14.
    181   definition main20 := 13.
    182   definition main2 := 12.
    183   definition main19 := 11.
    184   definition main18 := 10.
    185   definition main17 := 9.
    186   definition main16 := 8.
    187   definition main15 := 7.
    188   definition main14 := 6.
    189   definition main13 := 5.
    190   definition main12 := 4.
    191   definition main11 := 3.
    192   definition main10 := 2.
    193   definition main1 := 1.
    194   definition main0 := 0.
    195   definition C_cost9 := costlabel_of_nat 0.
     53    lbl__div32u15
     54    lbl__div32u0.
     55
     56  definition id__div32s := ident_of_nat 1.
     57  definition lbl__div32s9 := 25.
     58  definition lbl__div32s8 := 24.
     59  definition lbl__div32s7 := 23.
     60  definition lbl__div32s6 := 22.
     61  definition lbl__div32s5 := 21.
     62  definition lbl__div32s4 := 20.
     63  definition lbl__div32s3 := 19.
     64  definition lbl__div32s25 := 18.
     65  definition lbl__div32s24 := 17.
     66  definition lbl__div32s23 := 16.
     67  definition lbl__div32s22 := 15.
     68  definition lbl__div32s21 := 14.
     69  definition lbl__div32s20 := 13.
     70  definition lbl__div32s2 := 12.
     71  definition lbl__div32s19 := 11.
     72  definition lbl__div32s18 := 10.
     73  definition lbl__div32s17 := 9.
     74  definition lbl__div32s16 := 8.
     75  definition lbl__div32s15 := 7.
     76  definition lbl__div32s14 := 6.
     77  definition lbl__div32s13 := 5.
     78  definition lbl__div32s12 := 4.
     79  definition lbl__div32s11 := 3.
     80  definition lbl__div32s10 := 2.
     81  definition lbl__div32s1 := 1.
     82  definition lbl__div32s0 := 0.
     83  definition C_cost3 := costlabel_of_nat 4.
     84  definition C_cost4 := costlabel_of_nat 3.
     85  definition C_cost7 := costlabel_of_nat 2.
     86  definition C_cost5 := costlabel_of_nat 1.
     87  definition C_cost6 := costlabel_of_nat 0.
     88
     89
     90  definition pre__div32s := mk_pre_internal_function
     91    (Some ? (pair ?? 7 (ASTint I32 Signed)))
     92    [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))]
     93    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))]
     94    0
     95    [
     96    (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8));
     97    (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7));
     98    (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6));
     99    (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4));
     100    (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4));
     101    (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3));
     102    (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2));
     103    (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24));
     104    (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23));
     105    (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22));
     106    (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21));
     107    (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20));
     108    (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19));
     109    (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1));
     110    (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18));
     111    (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13));
     112    (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16));
     113    (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15));
     114    (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14));
     115    (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12));
     116    (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12));
     117    (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11));
     118    (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10));
     119    (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5));
     120    (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0));
     121    (pair ?? lbl__div32s0 (make_St_return))
     122]
     123
     124    lbl__div32s25
     125    lbl__div32s0.
     126
     127  definition id_search := ident_of_nat 2.
     128  definition lbl_search9 := 65.
     129  definition lbl_search8 := 64.
     130  definition lbl_search7 := 63.
     131  definition lbl_search65 := 62.
     132  definition lbl_search64 := 61.
     133  definition lbl_search63 := 60.
     134  definition lbl_search62 := 59.
     135  definition lbl_search61 := 58.
     136  definition lbl_search60 := 57.
     137  definition lbl_search6 := 56.
     138  definition lbl_search59 := 55.
     139  definition lbl_search58 := 54.
     140  definition lbl_search57 := 53.
     141  definition lbl_search56 := 52.
     142  definition lbl_search55 := 51.
     143  definition lbl_search54 := 50.
     144  definition lbl_search53 := 49.
     145  definition lbl_search52 := 48.
     146  definition lbl_search51 := 47.
     147  definition lbl_search50 := 46.
     148  definition lbl_search5 := 45.
     149  definition lbl_search49 := 44.
     150  definition lbl_search48 := 43.
     151  definition lbl_search47 := 42.
     152  definition lbl_search46 := 41.
     153  definition lbl_search45 := 40.
     154  definition lbl_search44 := 39.
     155  definition lbl_search43 := 38.
     156  definition lbl_search42 := 37.
     157  definition lbl_search41 := 36.
     158  definition lbl_search40 := 35.
     159  definition lbl_search4 := 34.
     160  definition lbl_search39 := 33.
     161  definition lbl_search38 := 32.
     162  definition lbl_search37 := 31.
     163  definition lbl_search36 := 30.
     164  definition lbl_search35 := 29.
     165  definition lbl_search34 := 28.
     166  definition lbl_search33 := 27.
     167  definition lbl_search32 := 26.
     168  definition lbl_search31 := 25.
     169  definition lbl_search30 := 24.
     170  definition lbl_search3 := 23.
     171  definition lbl_search29 := 22.
     172  definition lbl_search28 := 21.
     173  definition lbl_search27 := 20.
     174  definition lbl_search26 := 19.
     175  definition lbl_search25 := 18.
     176  definition lbl_search24 := 17.
     177  definition lbl_search23 := 16.
     178  definition lbl_search22 := 15.
     179  definition lbl_search21 := 14.
     180  definition lbl_search20 := 13.
     181  definition lbl_search2 := 12.
     182  definition lbl_search19 := 11.
     183  definition lbl_search18 := 10.
     184  definition lbl_search17 := 9.
     185  definition lbl_search16 := 8.
     186  definition lbl_search15 := 7.
     187  definition lbl_search14 := 6.
     188  definition lbl_search13 := 5.
     189  definition lbl_search12 := 4.
     190  definition lbl_search11 := 3.
     191  definition lbl_search10 := 2.
     192  definition lbl_search1 := 1.
     193  definition lbl_search0 := 0.
     194  definition C_cost16 := costlabel_of_nat 8.
     195  definition C_cost9 := costlabel_of_nat 7.
     196  definition C_cost14 := costlabel_of_nat 6.
     197  definition C_cost15 := costlabel_of_nat 5.
     198  definition C_cost12 := costlabel_of_nat 4.
     199  definition C_cost13 := costlabel_of_nat 3.
     200  definition C_cost10 := costlabel_of_nat 2.
     201  definition C_cost11 := costlabel_of_nat 1.
     202  definition C_cost8 := costlabel_of_nat 0.
     203
     204
     205  definition pre_search := mk_pre_internal_function
     206    (Some ? (pair ?? 8 (ASTint I8 Unsigned)))
     207    [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
     208    [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))]
     209    0
     210    [
     211    (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8));
     212    (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7));
     213    (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5));
     214    (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64));
     215    (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63));
     216    (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62));
     217    (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61));
     218    (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60));
     219    (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59));
     220    (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5));
     221    (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5));
     222    (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57));
     223    (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56));
     224    (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55));
     225    (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54));
     226    (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53));
     227    (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52));
     228    (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51));
     229    (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50));
     230    (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49));
     231    (pair ?? lbl_search5 (make_St_skip lbl_search58));
     232    (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48));
     233    (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47));
     234    (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46));
     235    (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45));
     236    (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44));
     237    (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43));
     238    (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42));
     239    (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41));
     240    (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40));
     241    (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39));
     242    (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3));
     243    (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38));
     244    (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37));
     245    (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34));
     246    (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35));
     247    (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0));
     248    (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33));
     249    (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32));
     250    (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31));
     251    (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30));
     252    (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29));
     253    (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2));
     254    (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28));
     255    (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27));
     256    (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26));
     257    (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20));
     258    (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24));
     259    (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23));
     260    (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22));
     261    (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21));
     262    (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19));
     263    (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19));
     264    (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1));
     265    (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18));
     266    (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17));
     267    (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16));
     268    (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15));
     269    (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14));
     270    (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13));
     271    (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12));
     272    (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6));
     273    (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10));
     274    (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9));
     275    (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0));
     276    (pair ?? lbl_search0 (make_St_return))
     277]
     278
     279    lbl_search65
     280    lbl_search0.
     281
     282  definition id_main := ident_of_nat 3.
     283  definition lbl_main9 := 61.
     284  definition lbl_main8 := 60.
     285  definition lbl_main7 := 59.
     286  definition lbl_main61 := 58.
     287  definition lbl_main60 := 57.
     288  definition lbl_main6 := 56.
     289  definition lbl_main59 := 55.
     290  definition lbl_main58 := 54.
     291  definition lbl_main57 := 53.
     292  definition lbl_main56 := 52.
     293  definition lbl_main55 := 51.
     294  definition lbl_main54 := 50.
     295  definition lbl_main53 := 49.
     296  definition lbl_main52 := 48.
     297  definition lbl_main51 := 47.
     298  definition lbl_main50 := 46.
     299  definition lbl_main5 := 45.
     300  definition lbl_main49 := 44.
     301  definition lbl_main48 := 43.
     302  definition lbl_main47 := 42.
     303  definition lbl_main46 := 41.
     304  definition lbl_main45 := 40.
     305  definition lbl_main44 := 39.
     306  definition lbl_main43 := 38.
     307  definition lbl_main42 := 37.
     308  definition lbl_main41 := 36.
     309  definition lbl_main40 := 35.
     310  definition lbl_main4 := 34.
     311  definition lbl_main39 := 33.
     312  definition lbl_main38 := 32.
     313  definition lbl_main37 := 31.
     314  definition lbl_main36 := 30.
     315  definition lbl_main35 := 29.
     316  definition lbl_main34 := 28.
     317  definition lbl_main33 := 27.
     318  definition lbl_main32 := 26.
     319  definition lbl_main31 := 25.
     320  definition lbl_main30 := 24.
     321  definition lbl_main3 := 23.
     322  definition lbl_main29 := 22.
     323  definition lbl_main28 := 21.
     324  definition lbl_main27 := 20.
     325  definition lbl_main26 := 19.
     326  definition lbl_main25 := 18.
     327  definition lbl_main24 := 17.
     328  definition lbl_main23 := 16.
     329  definition lbl_main22 := 15.
     330  definition lbl_main21 := 14.
     331  definition lbl_main20 := 13.
     332  definition lbl_main2 := 12.
     333  definition lbl_main19 := 11.
     334  definition lbl_main18 := 10.
     335  definition lbl_main17 := 9.
     336  definition lbl_main16 := 8.
     337  definition lbl_main15 := 7.
     338  definition lbl_main14 := 6.
     339  definition lbl_main13 := 5.
     340  definition lbl_main12 := 4.
     341  definition lbl_main11 := 3.
     342  definition lbl_main10 := 2.
     343  definition lbl_main1 := 1.
     344  definition lbl_main0 := 0.
     345  definition C_cost17 := costlabel_of_nat 0.
    196346
    197347
     
    199349    (Some ? (pair ?? 2 (ASTint I32 Signed)))
    200350    []
    201     [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Signed)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I8 Signed)); (pair ?? 24 (ASTint I8 Signed)); (pair ?? 25 (ASTint I8 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I8 Signed)); (pair ?? 33 (ASTint I8 Signed)); (pair ?? 34 (ASTint I8 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I8 Signed)); (pair ?? 42 (ASTint I8 Signed)); (pair ?? 43 (ASTint I8 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I8 Signed)); (pair ?? 51 (ASTint I8 Signed)); (pair ?? 52 (ASTint I8 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
     351    [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
    202352    5
    203353    [
    204     (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) main8));
    205     (pair ?? main8 (make_St_op2 Oaddp 3 8 9 main7));
    206     (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) main6));
    207     (pair ?? main61 (make_St_cost C_cost9 main60));
    208     (pair ?? main60 (make_St_const 53 (Oaddrstack 0) main59));
    209     (pair ?? main6 (make_St_op1 (Ocastint Signed I8) 4 7 main5));
    210     (pair ?? main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) main58));
    211     (pair ?? main58 (make_St_op2 Oaddp 49 53 54 main57));
    212     (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0)) main56));
    213     (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1)) main55));
    214     (pair ?? main55 (make_St_op2 Omul 50 51 52 main54));
    215     (pair ?? main54 (make_St_op2 Oaddp 46 49 50 main53));
    216     (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) main52));
    217     (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48 main51));
    218     (pair ?? main51 (make_St_store Mint8unsigned 46 47 main50));
    219     (pair ?? main50 (make_St_const 44 (Oaddrstack 0) main49));
    220     (pair ?? main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) main4));
    221     (pair ?? main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) main48));
    222     (pair ?? main48 (make_St_op2 Oaddp 40 44 45 main47));
    223     (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1)) main46));
    224     (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1)) main45));
    225     (pair ?? main45 (make_St_op2 Omul 41 42 43 main44));
    226     (pair ?? main44 (make_St_op2 Oaddp 37 40 41 main43));
    227     (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) main42));
    228     (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39 main41));
    229     (pair ?? main41 (make_St_store Mint8unsigned 37 38 main40));
    230     (pair ?? main40 (make_St_const 35 (Oaddrstack 0) main39));
    231     (pair ?? main4 (make_St_op1 (Ocastint Signed I8) 5 6 main3));
    232     (pair ?? main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) main38));
    233     (pair ?? main38 (make_St_op2 Oaddp 31 35 36 main37));
    234     (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2)) main36));
    235     (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1)) main35));
    236     (pair ?? main35 (make_St_op2 Omul 32 33 34 main34));
    237     (pair ?? main34 (make_St_op2 Oaddp 28 31 32 main33));
    238     (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) main32));
    239     (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30 main31));
    240     (pair ?? main31 (make_St_store Mint8unsigned 28 29 main30));
    241     (pair ?? main30 (make_St_const 26 (Oaddrstack 0) main29));
    242     (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main2));
    243     (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) main28));
    244     (pair ?? main28 (make_St_op2 Oaddp 22 26 27 main27));
    245     (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3)) main26));
    246     (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1)) main25));
    247     (pair ?? main25 (make_St_op2 Omul 23 24 25 main24));
    248     (pair ?? main24 (make_St_op2 Oaddp 19 22 23 main23));
    249     (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) main22));
    250     (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21 main21));
    251     (pair ?? main21 (make_St_store Mint8unsigned 19 20 main20));
    252     (pair ?? main20 (make_St_const 17 (Oaddrstack 0) main19));
    253     (pair ?? main2 (make_St_op1 Oid 0 1 main1));
    254     (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) main18));
    255     (pair ?? main18 (make_St_op2 Oaddp 13 17 18 main17));
    256     (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4)) main16));
    257     (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1)) main15));
    258     (pair ?? main15 (make_St_op2 Omul 14 15 16 main14));
    259     (pair ?? main14 (make_St_op2 Oaddp 10 13 14 main13));
    260     (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) main12));
    261     (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12 main11));
    262     (pair ?? main11 (make_St_store Mint8unsigned 10 11 main10));
    263     (pair ?? main10 (make_St_const 8 (Oaddrstack 0) main9));
    264     (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 main0));
    265     (pair ?? main0 (make_St_return))
     354    (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8));
     355    (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7));
     356    (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6));
     357    (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60));
     358    (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59));
     359    (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5));
     360    (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58));
     361    (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57));
     362    (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56));
     363    (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55));
     364    (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54));
     365    (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53));
     366    (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52));
     367    (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51));
     368    (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50));
     369    (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49));
     370    (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4));
     371    (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48));
     372    (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47));
     373    (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46));
     374    (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45));
     375    (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44));
     376    (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43));
     377    (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42));
     378    (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41));
     379    (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40));
     380    (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39));
     381    (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3));
     382    (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38));
     383    (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37));
     384    (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36));
     385    (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35));
     386    (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34));
     387    (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33));
     388    (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32));
     389    (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31));
     390    (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30));
     391    (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29));
     392    (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2));
     393    (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28));
     394    (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27));
     395    (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26));
     396    (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25));
     397    (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24));
     398    (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23));
     399    (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22));
     400    (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21));
     401    (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20));
     402    (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19));
     403    (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1));
     404    (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18));
     405    (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17));
     406    (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16));
     407    (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15));
     408    (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14));
     409    (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13));
     410    (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12));
     411    (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11));
     412    (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10));
     413    (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9));
     414    (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0));
     415    (pair ?? lbl_main0 (make_St_return))
    266416]
    267417
    268     main61
    269     main0.
     418    lbl_main61
     419    lbl_main0.
    270420
    271421
     
    274424  do f_main \larr make_internal_function pre_main;
    275425  do f_search \larr make_internal_function pre_search;
     426  do f__div32s \larr make_internal_function pre__div32s;
     427  do f__div32u \larr make_internal_function pre__div32u;
    276428
    277429OK ? (mk_program ??
    278430(  (pair ?? id_main f_main)::
    279431  (pair ?? id_search f_search)::
     432  (pair ?? id__div32s f__div32s)::
     433  (pair ?? id__div32u f__div32u)::
    280434(nil ?))
    281435  id_main
     
    287441   normalize  (* you can examine the result here *)
    288442   @refl qed.
    289 
Note: See TracChangeset for help on using the changeset viewer.