Changeset 1633 for src/Cminor


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

Update Cminor pretty printer and examples.

Location:
src/Cminor
Files:
3 added
3 deleted
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r1226 r1633  
    1313  | Sig_offset -> "ASTint I32 Unsigned"
    1414  | Sig_ptr -> "ASTptr Any"
     15
     16let print_type_return = function
     17  | Type_ret t -> (print_type t)
     18  | Type_void -> "?" (* shouldn't happen *)
    1519
    1620let print_ret_type = function
     
    2832
    2933let print_var n (id, sz, init) =
    30   Printf.sprintf "(pair ?? (pair ?? id_%s Any) [%s])"
     34  Printf.sprintf "(mk_Prod ?? (mk_Prod ?? id_%s Any) [%s])"
    3135    id
    3236    (match init with
     
    6367        (Driver.CminorMemory.concrete_size sz)
    6468
     69(* Matita will figure out the missing information from the types produced
     70   by the caller *)
    6571let print_op1 = function
    66   | AST.Op_cast((_,sg),sz) -> Printf.sprintf "(Ocastint %s I%d)" (print_signedness sg) (8*sz)
    67   | AST.Op_negint -> "Onegint"
    68   | AST.Op_notbool -> "Onotbool"
    69   | AST.Op_notint -> "Onotint"
    70   | AST.Op_id -> "Oid"
    71   | AST.Op_ptrofint -> "(Optrofint Any)"
    72   | AST.Op_intofptr -> "(Ointofptr ?)"
     72  | AST.Op_cast _ -> "(Ocastint ????)"
     73  | AST.Op_negint -> "(Onegint ??)"
     74  | AST.Op_notbool -> "(Onotbool ??? I)"
     75  | AST.Op_notint -> "(Onotint ??)"
     76  | AST.Op_id -> "(Oid ?)"
     77  | AST.Op_ptrofint -> "(Optrofint ?? Any)"
     78  | AST.Op_intofptr -> "(Ointofptr ???)"
    7379
    7480let print_op2 ty = function
     
    104110  | Cminor.Exp_cost (lab, e) ->
    105111      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
    106         lab (fresh ()) (define_expr_labels e)
     112        lab.CostLabel.name (fresh ()) (define_expr_labels e)
    107113  | _ -> ""
    108114
     
    142148        (print_expression p_id e3)
    143149  | Cminor.Exp_cost (lab, e) ->
    144       Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab (print_expression p_id e)
     150      Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab.CostLabel.name (print_expression p_id e)
    145151
    146152let print_arg p_id e =
    147   Printf.sprintf "dp ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
     153  Printf.sprintf "mk_DPair ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
    148154
    149155let rec print_args p_id =
     
    155161
    156162let print_local p_id (id,ty) =
    157   Printf.sprintf "pair ?? %s (%s)" (p_id id) (print_type ty)
     163  Printf.sprintf "mk_Prod ?? %s (%s)" (p_id id) (print_type ty)
    158164
    159165let print_locals p_id vars =
     
    163169let print_table n =
    164170  let f (case, exit) =
    165     Printf.sprintf "(pair ?? (repr ? %d) %d)" case exit
     171    Printf.sprintf "(mk_Prod ?? (repr ? %d) %d)" case exit
    166172  in
    167173  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
     
    174180  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
    175181  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
    176   | Cminor.St_loop s -> define_labels s
    177   | Cminor.St_block s -> define_labels s
    178182  | Cminor.St_switch (e, _, _) -> define_expr_labels e
    179183  | Cminor.St_return (Some e) -> define_expr_labels e
    180184  | Cminor.St_label (l, s) ->
    181       Printf.sprintf "definition L%s := ident_of_nat %d.\n%s"
     185      Printf.sprintf "definition L%s := label_of_nat %d.\n%s"
    182186        l (fresh ()) (define_labels s)
    183187  | Cminor.St_cost (l, s) ->
    184188      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
    185         l (fresh ()) (define_labels s)
     189        l.CostLabel.name (fresh ()) (define_labels s)
     190  | Cminor.St_ind_0 (_, s) -> define_labels s
     191  | Cminor.St_ind_inc (_, s) -> define_labels s
    186192  | _ -> ""
    187193
     
    206212        (print_args p_id args)
    207213  | Cminor.St_call (Some id, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
    208       Printf.sprintf "%sSt_call (Some ? %s) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
     214      Printf.sprintf "%sSt_call (Some ? (mk_Prod ?? %s (%s))) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
    209215        (n_spaces n)
    210216        (p_id id)
     217        (print_type_return sg.AST.res)
    211218        f
    212219        (print_args p_id args)
     
    250257        (print_body p_id (n+2) s2)
    251258        (n_spaces n)
    252   | Cminor.St_loop s ->
    253       Printf.sprintf "%sSt_loop (\n%s%s)\n"
    254         (n_spaces n)
    255         (print_body p_id (n+2) s)
    256         (n_spaces n)
    257   | Cminor.St_block s ->
    258       Printf.sprintf "%sSt_block (\n%s%s)\n"
    259         (n_spaces n)
    260         (print_body p_id (n+2) s)
    261         (n_spaces n)
    262   | Cminor.St_exit i ->
    263       Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
    264   | Cminor.St_switch (e, tbl, dflt) ->
     259  | Cminor.St_switch (e, tbl, dflt) -> assert false
     260(*
    265261      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
    266262      Printf.sprintf "%sSt_switch I%d %s (%s) [\n%s%s] %d\n"
     
    270266        (n_spaces (n+2))
    271267        (print_table ( n+2) tbl)
    272         dflt
     268        dflt*)
    273269  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
    274270  | Cminor.St_return (Some e) ->
     
    284280  | Cminor.St_cost (lbl, s) ->
    285281      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
    286         (n_spaces n) lbl (print_body p_id n s)
     282        (n_spaces n) lbl.CostLabel.name (print_body p_id n s)
    287283        (n_spaces n)
     284  | Cminor.St_ind_0 (_, s) -> print_body p_id n s
     285  | Cminor.St_ind_inc (_, s) -> print_body p_id n s
    288286
    289287let print_ids fname vs =
     
    296294  let fid = fresh () in
    297295  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
    298   Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
     296  Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  %s\n%d (\n%s\n) %s).\n\n"
    299297    f_name
    300298    fid
     
    305303    (print_locals p_id f_def.Cminor.f_params)
    306304    (print_locals p_id f_def.Cminor.f_vars)
     305    "(match daemon in False with [ ])"  (* ewww *)
    307306    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
    308307    (print_body p_id 2 f_def.Cminor.f_body)
     308    "(match daemon in False with [ ])"  (* ewww *)
    309309
    310310let print_sig s =
    311311  Printf.sprintf "mk_signature [%s] (%s)"
    312312    (MiscPottier.string_of_list "; " print_type s.AST.args)
    313     (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
     313    (match s.AST.res with AST.Type_ret t -> "Some ? (" ^ print_type t ^ ")"
    314314                        | AST.Type_void  -> "None ?")
    315315
     
    334334let print_fun' n functs =
    335335  MiscPottier.string_of_list ";\n" (fun (f,def) ->
    336     Printf.sprintf "%s(pair ?? id_%s f_%s)"
     336    Printf.sprintf "%s(mk_Prod ?? id_%s f_%s)"
    337337      (n_spaces n)
    338338      f
     
    352352
    353353let print_program p =
    354   Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
     354  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\ndefinition label_of_nat : nat -> identifier Label := identifier_of_nat ?.\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
    355355    (define_var_ids p.Cminor.vars)
    356356    (print_functs p.Cminor.functs)
  • src/Cminor/test/null-op.Cminor.ma

    r966 r1633  
    11include "Cminor/semantics.ma".
    22include "common/Animation.ma".
     3
     4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
    35
    46
     
    1517  (Some ? (ASTint I32 Signed))
    1618  []
    17   [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)]
    18   1 (
     19  [mk_Prod ?? id_main_p (ASTptr Any); mk_Prod ?? id_main_q (ASTptr Any)]
     20  (match daemon in False with [ ])
     211 (
    1922  St_cost C_cost4 (
    2023  St_seq (
    21     St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     24    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    2225  ) (
    2326  St_seq (
     
    2730    St_ifthenelse I32 Signed (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_q)) (
    2831      St_cost C_cost2 (
    29       St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
     32      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    3033      )
    3134    ) (
     
    3740    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Osubpp I32) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
    3841      St_cost C_cost0 (
    39       St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
     42      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    4043      )
    4144    ) (
     
    4548  ) (
    4649  St_seq (
    47     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (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)))))
     50    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (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)))))
    4851  ) (
    4952  St_seq (
    50     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (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)))))
     53    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (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)))))
    5154  ) (
    5255  St_seq (
    53     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (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)))))
     56    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (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)))))
    5457  ) (
    55   St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0)))))))
     58  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I32 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))))))
    5659  )
    5760  )
     
    6366  )
    6467
    65 )).
     68) (match daemon in False with [ ])).
    6669
    6770
    6871
    6972definition myprog : Cminor_program :=
    70 mk_program ?? [
    71   (pair ?? id_main f_main)
     73mk_program ?? [] [
     74  (mk_Prod ?? id_main f_main)
    7275]  id_main
    73 []
    7476.
    75 
    76 example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    77 normalize  (* you can examine the result here *)
    78 @refl
    79 qed.
    80 
    81 include "Cminor/toRTLabs.ma".
    82 include "RTLabs/semantics.ma".
    83 
    84 example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    85 normalize  (* you can examine the result here *)
    86 @refl
    87 qed.
    88 
  • 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.
  • src/Cminor/test/search.test.ma

    r1226 r1633  
    1010include "RTLabs/semantics.ma".
    1111
    12 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
     12example execRTL: finishes_with (repr 3) ?
     13(bind ? (snapshot state) (cminor_to_rtlabs myprog)
     14  (λmyprog'. exec_up_to RTLabs_fullexec myprog' 1000 [ ])).
    1315normalize  (* you can examine the result here *)
    1416@refl
Note: See TracChangeset for help on using the changeset viewer.