Changeset 1633


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

Update Cminor pretty printer and examples.

Location:
src
Files:
3 added
3 deleted
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r1226 r1633  
    265265              print_stmt s1
    266266              print_stmt s2
    267   | Swhile(e, s) ->
     267  | Swhile(_, e, s) ->
    268268      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
    269269              print_expr e
    270270              print_stmt s
    271   | Sdowhile(e, s) ->
     271  | Sdowhile(_, e, s) ->
    272272      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
    273273              print_expr e
    274274              print_stmt s
    275   | Sfor(s_init, e, s_iter, s_body) ->
     275  | Sfor(_, s_init, e, s_iter, s_body) ->
    276276      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
    277277              print_stmt s_init
     
    417417  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
    418418  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
    419   | Swhile(e, s) -> collect_expr e; collect_stmt s
    420   | Sdowhile(e, s) -> collect_stmt s; collect_expr e
    421   | Sfor(s_init, e, s_iter, s_body) ->
     419  | Swhile(_, e, s) -> collect_expr e; collect_stmt s
     420  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
     421  | Sfor(_, s_init, e, s_iter, s_body) ->
    422422      collect_stmt s_init; collect_expr e;
    423423      collect_stmt s_iter; collect_stmt s_body
  • 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
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r1226 r1633  
    136136
    137137let print_statement lookup_type = function
    138   | RTLabs.St_skip lbl -> "make_St_skip " ^ (print_label lbl)
     138  | RTLabs.St_skip lbl
     139  | RTLabs.St_ind_0 (_, lbl)
     140  | RTLabs.St_ind_inc (_, lbl)
     141     -> "make_St_skip " ^ (print_label lbl)
    139142  | RTLabs.St_cost (cost_lbl, lbl) ->
    140       Printf.sprintf "make_St_cost C%s %s" cost_lbl (print_label lbl)
     143      Printf.sprintf "make_St_cost C%s %s"
     144        cost_lbl.CostLabel.name (print_label lbl)
    141145  | RTLabs.St_cst (dests, cst, lbl) ->
    142146      Printf.sprintf "make_St_const %s (%s) %s"
     
    198202        (Register.print rs)
    199203        (print_table tbl)
    200   | RTLabs.St_return rs -> "make_St_return" (* rs should always be the function's result register, anyway *)
     204  | RTLabs.St_return -> "make_St_return"
    201205
    202206let print_cost_labels n c =
  • src/RTLabs/import.ma

    r1612 r1633  
    1717; pf_locals    : list (pre_register × typ)
    1818; pf_stacksize : nat
    19 ; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
     19; pf_graph     : list (nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement))
    2020; pf_entry     : nat
    2121; pf_exit      : nat
     
    2323
    2424definition make_register :
    25   (pre_register → option register) → pre_register → universe RegisterTag →
    26   (nat → option register) × (universe RegisterTag) × register ≝
    27 λm,reg,g.
     25  (pre_register → option (register×typ)) → pre_register → typ → universe RegisterTag →
     26  (nat → option (register×typ)) × (universe RegisterTag) × register ≝
     27λm,reg,ty,g.
    2828  match m reg with
    29   [ Some r' ⇒ 〈〈m,g〉,r'〉
     29  [ Some r' ⇒ 〈〈m,g〉,\fst r'〉
    3030  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
    31              〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     31             〈〈λn. if eqb reg n then Some ? 〈r',ty〉 else m n,g'〉,r'〉
    3232  ]
    3333.
    3434
    3535definition make_registers_list :
    36   (nat → option register) → list (pre_register × typ) → universe RegisterTag →
    37     (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝
     36  (nat → option (register×typ)) → list (pre_register × typ) → universe RegisterTag →
     37    (nat → option (register×typ)) × (universe RegisterTag) × (list (register×typ)) ≝
    3838λm,lrs,g.
    3939foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
    4040                    let 〈rs,ty〉 ≝ rst in
    4141                    let 〈m,g〉 ≝ acc' in
    42                     let 〈mg,rs'〉 ≝ make_register m rs g in
     42                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
    4343                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    4444
     
    5252  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
    5353                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
    54                            | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
     54                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) (\snd rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
    5555                           ] in
    5656  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
     
    6363  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
    6464  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    65   do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
     65  do graph ← foldr ?? (λp:nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement).λg0.
    6666                         do g ← g0;
    6767                         let 〈l,s〉 ≝ p in
     
    8888         (pf_stacksize pre_f)
    8989         graph
     90         ?
     91         ?
    9092         (mk_Sig ?? entry p)
    9193         (mk_Sig ?? exit q)
    9294         )))
    9395   .
    94 % #E destruct (E)
     96[ 1,2: % #E destruct (E)
     97| 3,4: cases daemon
     98]
    9599qed.
    96100
    97 definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
    98 λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
     101definition make_reg_list : (nat → res (register×typ)) → list pre_register → res (list register) ≝
     102λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do 〈r,t〉 ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
    99103
    100104(* XXX move somewhere sensible *)
     
    107111].
    108112
    109 definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
    110 λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
     113definition make_opt_reg : (pre_register → res (register×typ)) → option pre_register → res (option register) ≝
     114λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do 〈r',t'〉 ← m r; OK ? (Some ? r') ].
    111115
    112 let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
    113 let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
    114 let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
    115 let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src' ← r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
    116 let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src1' ← r src1; do src2' ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
    117 let rec make_St_load chunk addr dst l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do dst' ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
    118 let rec make_St_store chunk addr src l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do src' ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
    119 let rec make_St_call_id id args dst l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
    120 let rec make_St_call_ptr frs args dst l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
    121 let rec make_St_tailcall_id id args ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
    122 let rec make_St_tailcall_ptr frs args ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
    123 let rec make_St_cond src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
    124 let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
    125 definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
     116inductive pre_op1 : Type[0] ≝
     117  | POcastint: intsize → signedness → intsize → pre_op1
     118  | POnegint:  pre_op1
     119  | POnotbool: pre_op1
     120  | POnotint:  pre_op1
     121  | POid: pre_op1
     122  | POptrofint: pre_op1
     123  | POintofptr: pre_op1
     124.
    126125
     126axiom TypeMismatch : String.
     127
     128(* duplicated from Clight/toCminor.ma. *)
     129definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
     130* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     131qed.
     132
     133definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
     134* [ #sz1 #sg1 | #r1 | #sz1 ]
     135* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     136[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
     137  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     138| *; #P #p @(region_should_eq r1 ?? p)
     139| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     140] qed.
     141
     142definition is_bool_src : ∀ty. res (boolsrc ty) ≝
     143λty. match ty return λt.res (boolsrc t) with [ ASTint _ _ ⇒ OK ? I | ASTptr _ ⇒ OK ? I | _ ⇒ Error ? (msg TypeMismatch) ].
     144
     145definition make_op1 : ∀t,t'. pre_op1 → res (unary_operation t' t) ≝
     146λt,t',op.
     147  match op with
     148  [ POcastint sz sg sz' ⇒
     149      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     150        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Ocastint sz sg sz' sg2);
     151               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     152      | _ ⇒ Error ? (msg TypeMismatch) ]
     153  | POnegint ⇒
     154      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     155        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onegint sz2 sg2);
     156               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     157      | _ ⇒ Error ? (msg TypeMismatch) ]
     158  | POnotbool ⇒
     159      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     160        do p ← is_bool_src t';
     161               OK ? (Onotbool t' sz2 sg2 p)
     162      | _ ⇒ Error ? (msg TypeMismatch) ]
     163  | POnotint ⇒
     164      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     165        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onotint sz2 sg2);
     166               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     167      | _ ⇒ Error ? (msg TypeMismatch) ]
     168  | POid ⇒ typ_should_eq t t' (λt'. unary_operation t' t) (Oid t)
     169  | POptrofint ⇒
     170      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     171      match t return λt. res (unary_operation ? t) with [ ASTptr r1 ⇒
     172        OK ? (Optrofint …)
     173      | _ ⇒ Error ? (msg TypeMismatch) ]
     174      | _ ⇒ Error ? (msg TypeMismatch) ]
     175  | POintofptr ⇒
     176      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     177      match t' return λt'. res (unary_operation t' ?) with [ ASTptr r1 ⇒
     178        OK ? (Ointofptr …)
     179      | _ ⇒ Error ? (msg TypeMismatch) ]
     180      | _ ⇒ Error ? (msg TypeMismatch) ]
     181  ].
     182
     183let rec make_St_skip l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_skip l').
     184let rec make_St_cost cl l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
     185let rec make_St_const rs cst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',ty'〉 ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
     186let rec make_St_op1 op dst src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src',sty〉 ← r src; do l' ← f l; do op ← make_op1 dty sty op; OK ? (St_op1 dty sty op dst' src' l').
     187let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src1',sty1〉 ← r src1; do 〈src2',sty2〉 ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
     188let rec make_St_load chunk addr dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈dst',dty〉 ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
     189let rec make_St_store chunk addr src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈src',sty〉 ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
     190let rec make_St_call_id id args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
     191let rec make_St_call_ptr frs args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
     192let rec make_St_tailcall_id id args ≝ λr:nat → res (register×typ).λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
     193let rec make_St_tailcall_ptr frs args ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
     194let rec make_St_cond src ltrue lfalse ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈src',sty〉 ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
     195let rec make_St_jumptable rs ls ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',rty〉 ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
     196definition make_St_return ≝ λr:nat → res (register×typ).λf:nat → res label. OK statement St_return.
     197
  • src/acc-matita-printers.patch

    r1158 r1633  
    1 diff --git a/Deliverables/D2.2/8051/myocamlbuild_config.ml b/Deliverables/D2.2/8051/myocamlbuild_config.ml
    2 index 4abced7..9b3b756 100644
    3 --- a/Deliverables/D2.2/8051/myocamlbuild_config.ml
    4 +++ b/Deliverables/D2.2/8051/myocamlbuild_config.ml
    5 @@ -1 +1 @@
    6 -let parser_lib = "/home/akuma/Work/CerCo/Bologna/Deliverables/D2.2/8051/lib"
    7 +let parser_lib = "/home/bcampbe2/afs/cerco/cerco-git/Deliverables/D2.2/8051/lib"
    81diff --git a/Deliverables/D2.2/8051/src/acc.ml b/Deliverables/D2.2/8051/src/acc.ml
    9 index 6962751..59f03ca 100644
     2index 0a95ef0..56d0cb9 100644
    103--- a/Deliverables/D2.2/8051/src/acc.ml
    114+++ b/Deliverables/D2.2/8051/src/acc.ml
    12 @@ -25,15 +25,17 @@ let process filename =
    13    let _ = Printf.eprintf "Processing %s.\n%!" filename in
    14    let src_language    = Options.get_source_language () in
    15    let tgt_language    = Options.get_target_language () in
    16 -  let input_ast       = Languages.parse src_language filename in
    17 -  let input_ast       = Languages.add_runtime input_ast in
    18 -  let input_ast       = Languages.labelize input_ast in
     5@@ -27,18 +27,20 @@ let process filename =
     6   let tgt_language = Options.get_target_language () in
     7   let is_lustre_file = Options.is_lustre_file () in
     8   let remove_lustre_externals = Options.is_remove_lustre_externals () in
     9-  let input_ast =
     10-    Languages.parse ~is_lustre_file ~remove_lustre_externals
     11-      src_language filename in
     12-  let input_ast = Languages.add_runtime input_ast in
     13-  let input_ast = Languages.labelize input_ast in
    1914   let (exact_output, output_filename) = match Options.get_output_files () with
    2015     | None -> (false, filename)
    2116     | Some filename' -> (true, filename') in
    2217-  let save ?(suffix="") ast =
    23 -    Languages.save exact_output output_filename suffix ast
     18-    Languages.save
    2419+  let save ?(suffix="") ?(matita=false) ast =
    25 +    Languages.save ~matita exact_output output_filename suffix ast
     20+    Languages.save ~matita
     21       (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    2622   in
    27 +  let input_ast       = Languages.parse src_language filename in
     23+  let input_ast =
     24+    Languages.parse ~is_lustre_file ~remove_lustre_externals
     25+      src_language filename in
    2826+  if tgt_language = Languages.Clight &&
    29 +     Options.is_matita_output_enabled () then save ~matita:true input_ast;
    30 +  let input_ast       = Languages.add_runtime input_ast in
    31 +  let input_ast       = Languages.labelize input_ast in
     27+       Options.is_matita_output_enabled () then save ~matita:true input_ast;
     28+  let input_ast = Languages.add_runtime input_ast in
     29+  let input_ast = Languages.labelize input_ast in
    3230   let target_asts =
    3331     (** If debugging is enabled, the compilation function returns all
    3432        the intermediate programs. *)
    35 @@ -42,6 +44,8 @@ let process filename =
     33@@ -49,6 +51,8 @@ let process filename =
    3634   in
    3735   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
     
    4139   if Options.annotation_requested () then
    4240     begin
    43        let (annotated_input_ast, cost_id, cost_incr) =
    44 @@ -50,8 +54,11 @@ let process filename =
    45           Languages.save_cost output_filename cost_id cost_incr);
     41       let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
     42@@ -59,8 +63,11 @@ let process filename =
     43            extern_cost_variables);
    4644     end;
    47                                             
    48 -  if Options.is_debug_enabled () then 
     45 
     46-  if Options.is_debug_enabled () then
    4947+  if Options.is_debug_enabled () then begin
    5048     List.iter save intermediate_asts;
    5149+    if Options.is_matita_output_enabled () then
    52 +      List.iter (save ~matita:true) intermediate_asts;
     50+      List.iter (save ~matita:true) intermediate_asts
    5351+  end;
    5452 
    55    if Options.interpretation_requested () || Options.is_debug_enabled () then
     53   if Options.interpretations_requested () then
    5654     begin
    5755diff --git a/Deliverables/D2.2/8051/src/clight/clightFromC.ml b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
    58 index f6c274d..f5f0da8 100644
     56index 0b54437..1c84dca 100644
    5957--- a/Deliverables/D2.2/8051/src/clight/clightFromC.ml
    6058+++ b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
     
    8583 (* The target architecture: the Intel 8051. *)
    8684diff --git a/Deliverables/D2.2/8051/src/languages.ml b/Deliverables/D2.2/8051/src/languages.ml
    87 index dc01a18..0120b68 100644
     85index 3048d99..ef7b876 100644
    8886--- a/Deliverables/D2.2/8051/src/languages.ml
    8987+++ b/Deliverables/D2.2/8051/src/languages.ml
    90 @@ -245,7 +245,25 @@ let string_output = function
    91    | AstASM p ->
    92      [Pretty.print_program p ; ASMPrinter.print_program p]
     88@@ -257,7 +257,26 @@ let string_output asm_pretty = function
     89      else ["Pretty print not requested"]) @
     90     [ASMPrinter.print_program p]
    9391 
    94 -let save exact_output filename suffix ast =
     92-let save asm_pretty exact_output filename suffix ast =
    9593+let string_output_matita = function
    96 +  | AstClight p ->
    97 +    [ClightPrintMatita.print_program p]
    98 +  | AstCminor p ->
    99 +    [CminorMatitaPrinter.print_program p]
    100 +  | AstRTLabs p ->
    101 +    [RTLabsMatitaPrinter.print_program p]
    102 +  | AstRTL p ->
    103 +    [RTLPrinter.print_program p]
    104 +  | AstERTL p ->
    105 +    [ERTLPrinter.print_program p]
    106 +  | AstLTL p ->
    107 +    [LTLPrinter.print_program p]
    108 +  | AstLIN p ->
    109 +    [LINPrinter.print_program p]
    110 +  | AstASM p ->
    111 +    [Pretty.print_program p ; ASMPrinter.print_program p]
     94+ | AstClight p ->
     95+   [ClightPrintMatita.print_program p]
     96+ | AstCminor p ->
     97+   [CminorMatitaPrinter.print_program p]
     98+ | AstRTLabs p ->
     99+   [RTLabsPrinter.print_program p]
     100+   (*[RTLabsMatitaPrinter.print_program p]*)
     101+ | AstRTL p ->
     102+   [RTLPrinter.print_program p]
     103+ | AstERTL p ->
     104+   [ERTLPrinter.print_program p]
     105+ | AstLTL p ->
     106+   [LTLPrinter.print_program p]
     107+ | AstLIN p ->
     108+   [LINPrinter.print_program p]
     109+ | AstASM p ->
     110+   [Pretty.print_program p ; ASMPrinter.print_program p]
    112111+
    113 +let save exact_output ?(matita=false) filename suffix ast =
     112+let save asm_pretty ?(matita=false) exact_output filename suffix ast =
    114113   let ext_chopped_filename =
    115114     if exact_output then filename
    116115     else
    117 @@ -253,12 +271,16 @@ let save exact_output filename suffix ast =
     116@@ -265,12 +284,16 @@ let save asm_pretty exact_output filename suffix ast =
    118117       with Invalid_argument ("Filename.chop_extension") -> filename in
    119118   let ext_chopped_filename = ext_chopped_filename ^ suffix in
     
    127126     if exact_output then ext_filenames
    128127     else List.map Misc.SysExt.alternative ext_filenames in
    129 -  let output_strings = string_output ast in
     128-  let output_strings = string_output asm_pretty ast in
    130129+  let output_strings =
    131130+    if matita then string_output_matita ast
    132 +              else string_output ast in
     131+              else string_output asm_pretty ast in
    133132   let f filename s =
    134133     let cout = open_out filename in
    135134     output_string cout s;
    136135diff --git a/Deliverables/D2.2/8051/src/languages.mli b/Deliverables/D2.2/8051/src/languages.mli
    137 index b96784b..1eb6cbb 100644
     136index 26b5a0f..121c53f 100644
    138137--- a/Deliverables/D2.2/8051/src/languages.mli
    139138+++ b/Deliverables/D2.2/8051/src/languages.mli
    140 @@ -79,7 +79,7 @@ val interpret : bool -> ast -> AST.trace
    141      whose name is prefixed by [filename] and whose extension is deduced from the
    142      language of the AST. If [exact_output] is false then the written file will
    143      be fresh. *)
    144 -val save : bool -> string -> string -> ast -> unit
    145 +val save : bool -> ?matita:bool -> string -> string -> ast -> unit
     139@@ -90,7 +90,7 @@ val interpret : bool -> ast -> AST.trace
     140     whose extension is deduced from the language of the AST. If [exact_output]
     141     is false then the written file will be fresh. If [asm_pretty] is true, then
     142     an additional pretty-printed assembly file is output. *)
     143-val save : bool -> bool -> string -> string -> ast -> unit
     144+val save : bool -> ?matita:bool -> bool -> string -> string -> ast -> unit
    146145 
    147  (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    148      cost variable and then the name [cost_incr] of the cost increment function
     146 (** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
     147     prints the name [cost_id] of the cost variable, then the name [cost_incr] of
    149148diff --git a/Deliverables/D2.2/8051/src/options.ml b/Deliverables/D2.2/8051/src/options.ml
    150 index a13083c..5ca6481 100644
     149index 77a7735..b4a2d05 100644
    151150--- a/Deliverables/D2.2/8051/src/options.ml
    152151+++ b/Deliverables/D2.2/8051/src/options.ml
    153 @@ -43,6 +43,9 @@ let debug_flag                        = ref false
    154  let set_debug                  = (:=) debug_flag
    155  let is_debug_enabled ()                = !debug_flag
     152@@ -98,6 +98,9 @@ let set_lustre_test_max_int     = (:=) lustre_test_max_int
     153 let get_lustre_test_max_int ()         = !lustre_test_max_int
     154 
    156155 
    157156+let matita_flag                        = ref false
     
    161160 let print_result_flag          = ref false
    162161 let set_print_result           = (:=) print_result_flag
    163 @@ -83,4 +86,7 @@ let options = OptionsParsing.register [
     162@@ -233,4 +236,7 @@ let options = OptionsParsing.register [
    164163 
    165164   "-dev", Arg.Set dev_test,
     
    170169 ]
    171170diff --git a/Deliverables/D2.2/8051/src/options.mli b/Deliverables/D2.2/8051/src/options.mli
    172 index a00c940..13a88c3 100644
     171index 2f75755..3af36c9 100644
    173172--- a/Deliverables/D2.2/8051/src/options.mli
    174173+++ b/Deliverables/D2.2/8051/src/options.mli
    175 @@ -34,3 +34,6 @@ val is_print_result_enabled : unit -> bool
     174@@ -75,3 +75,6 @@ val is_print_result_enabled : unit -> bool
    176175 
    177176 (** {2 Developers' playground} *)
Note: See TracChangeset for help on using the changeset viewer.