Changeset 750


Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r739 r750  
    3636  prototype, except that we use the universe's name as a tag for the type of
    3737  identifiers to provide some extra type safety.
     38
     3908/04/2011:
     40  Make return register optional in RTLabs
  • src/RTLabs/RTLabs-sem.ma

    r744 r750  
    1414record frame : Type[0] ≝
    1515{ func   : internal_function
    16 ; locals : register_env split_val
     16; locals : register_env val
    1717; next   : label
    1818; sp     : block
    19 ; retdst : registers (* XXX: not optional? *)
     19; retdst : option register
    2020}.
    2121
     
    3232   ∀  fd : fundef internal_function.
    3333   ∀args : list val.
    34    ∀ dst : registers.
     34   ∀ dst : option register.
    3535   ∀ stk : list frame.
    3636   ∀   m : mem.
     
    3838| Returnstate :
    3939   ∀ rtv : val.
    40    ∀ dst : registers.
     40   ∀ dst : option register.
    4141   ∀ stk : list frame.
    4242   ∀   m : mem.
     
    4949
    5050definition reg_store ≝
    51 λrs,v,locals. match rs with [ dp n regs ⇒
    52   do vs ← break n v;
    53   OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
    54 ].
    55 
    56 let rec params_store (rs:list registers) (vs:list val) (locals : register_env split_val) : res (register_env split_val) ≝
     51λreg,v,locals.
     52  OK ? (add RegisterTag val locals reg v)
     53.
     54
     55let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    5756match rs with
    5857[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
     
    6261] ].
    6362
    64 definition reg_retrieve : register_env ? → registers → res val ≝
    65 λlocals,rs. match rs with [ dp n regs ⇒
    66   do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
    67   merge n vs
    68 ].
     63definition reg_retrieve : register_env ? → register → res val ≝
     64λlocals,reg. opt_to_res … (lookup ?? locals reg).
    6965
    7066(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
    7167
    72 definition eval_addr : genv → frame → ∀m:addressing. Vector registers (addr_mode_args m) → res val ≝
    73 λge,f,m. match m return λm'.Vector registers (addr_mode_args m') → ? with
     68definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
     69λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
    7470[ Aindexed i ⇒ λargs.
    7571    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
     
    115111  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    116112  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    117   | St_const rs cst l ⇒
     113  | St_const r cst l ⇒
    118114      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
    119       ! locals ← reg_store rs v (locals f);
     115      ! locals ← reg_store r v (locals f);
    120116      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    121117  | St_op1 op dst src l ⇒
     
    178174      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    179175
    180   | St_jumptable rs ls ⇒
    181       ! v ← reg_retrieve (locals f) rs;
     176  | St_jumptable r ls ⇒
     177      ! v ← reg_retrieve (locals f) r;
    182178      match v with
    183179      [ Vint i ⇒
     
    207203    [ nil ⇒ Error ? (* Already in final state *)
    208204    | cons f fs' ⇒
    209         ! locals ← reg_store dst v (locals f);
     205        ! locals ← match dst with [ None ⇒ OK ? (locals f)
     206                                  | Some d ⇒ reg_store d v (locals f) ];
    210207        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    211208    ]
     
    229226  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    230227  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    231   OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
     228  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
    232229
    233230definition RTLabs_fullexec : fullexec io_out io_in ≝
  • src/RTLabs/RTLabs-syntax.ma

    r747 r750  
    1313
    1414definition immediate : Type[0] ≝ int.
    15 definition registers ≝ Sig nat (Vector register).
    1615
    1716(* Addressing modes *)
     
    3433].
    3534
    36 definition addr ≝ λm.Vector registers (addr_mode_args m).
     35definition addr ≝ λm.Vector register (addr_mode_args m).
    3736
    3837(* Statements, including the label of successor(s). *)
     
    4140| St_skip : label → statement
    4241| St_cost : costlabel → label → statement
    43 | St_const : registers → constant → label → statement
    44 | St_op1 : unary_operation → registers → registers → label → statement
    45 | St_op2 : binary_operation → registers → registers → registers → label → statement
    46 | St_load : memory_chunk → ∀m:addressing. addr m → registers → label → statement
    47 | St_store : memory_chunk → ∀m:addressing. addr m → registers → label → statement
    48 | St_call_id : ident → list registers → registers → signature → label → statement
    49 | St_call_ptr : registers → list registers → registers → signature → label → statement
    50 | St_tailcall_id : ident → list registers → signature → statement
    51 | St_tailcall_ptr : registers → list registers → signature → statement
     42| St_const : register → constant → label → statement
     43| St_op1 : unary_operation → register → register → label → statement
     44| St_op2 : binary_operation → register → register → register → label → statement
     45| St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
     46| St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
     47| St_call_id : ident → list register → option register → signature → label → statement
     48| St_call_ptr : register → list register → option register → signature → label → statement
     49| St_tailcall_id : ident → list register → signature → statement
     50| St_tailcall_ptr : register → list register → signature → statement
    5251(* Um, what? *)
    5352| St_condcst : constant → label → label → statement
    54 | St_cond1 : unary_operation → registers → label → label → statement
    55 | St_cond2 : binary_operation → registers → registers → label → label → statement
    56 | St_jumptable : registers → list label → statement
    57 | St_return : registers → statement
     53| St_cond1 : unary_operation → register → label → label → statement
     54| St_cond2 : binary_operation → register → register → label → label → statement
     55| St_jumptable : register → list label → statement
     56| St_return : register → statement
    5857.
    5958
     
    6261; f_reggen    : universe RegisterTag
    6362; f_sig       : signature
    64 ; f_result    : registers
    65 ; f_params    : list registers
    66 ; f_locals    : list registers
     63; f_result    : option register
     64; f_params    : list register
     65; f_locals    : list register
     66; f_ptrs      : list register
    6767; f_stacksize : nat
    6868; f_graph     : graph statement
     
    7272(* XXX: matita interpretations bug workaround *)
    7373definition f_stacksize : internal_function → nat ≝
    74 λf.match f with [ mk_internal_function _ _ _ _ _ _ s _ _  _ ⇒ s ].
     74λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
    7575
    7676(* Global variables only need to be given their size at this stage of
     
    8484     return and jump tables?)
    8585   - seems like load and store ought to have types that control the size of the
    86      registers list based on the addressing mode; similarly, memory_chunk and
    87      registers are probably related.
     86     register list based on the addressing mode; similarly, memory_chunk and
     87     register are probably related.
    8888   - label and register generation really tell us something about the sets of
    89      labels and registers that may appear, perhaps it should be renamed, or the
     89     labels and register that may appear, perhaps it should be renamed, or the
    9090     graph made dependent on them to make it obvious, etc.
    9191 *)
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r737 r750  
    1313
    1414
    15 let print_reg_list rl =
    16   Printf.sprintf "(dp ?? %d [[%s]])" (List.length rl) (MiscPottier.string_of_list " ; " Register.print rl)
    17 
    1815let rec print_args args =
    19   Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " print_reg_list args)
    20 
    21 let print_result rl = print_reg_list rl
     16  Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " Register.print args)
     17
     18let print_result rl = Register.print rl
    2219
    2320let print_params rl =
    24   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_reg_list rl)
     21  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
    2522
    2623let print_locals rl =
    27   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_reg_list rl)
    28 
    29 
     24  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
     25
     26let print_quantity = function
     27  | Memory.QInt 1 -> "Mint8unsigned"
     28  | Memory.QInt 2 -> "Mint16unsigned"
     29  | Memory.QInt 4 -> "Mint32"
     30  | Memory.QPtr -> "Mpointer Any"
     31(*
    3032let print_memory_q = function
    3133  | Memory.MQ_int8signed    -> "Mint8signed"
     
    3840  | Memory.MQ_pointer       -> "Mpointer Any"
    3941  | Memory.MQ_chunk         -> "MXXX"
    40 
     42*)
    4143
    4244
     
    131133  | RTLabs.St_cst (dests, cst, lbl) ->
    132134      Printf.sprintf "make_St_const %s (%s) %s"
    133         (print_reg_list dests)
     135        (Register.print dests)
    134136        (print_cst cst)
    135137        lbl
     
    137139      Printf.sprintf "make_St_op1 %s %s %s %s"
    138140        (print_op1 op1)
    139         (print_reg_list dests)
    140         (print_reg_list srcs)
     141        (Register.print dests)
     142        (Register.print srcs)
    141143        lbl
    142144  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    143145      Printf.sprintf "make_St_op2 %s %s %s %s %s"
    144146        (print_op2 op2)
    145         (print_reg_list dests)
    146         (print_reg_list srcs1)
    147         (print_reg_list srcs2)
     147        (Register.print dests)
     148        (Register.print srcs1)
     149        (Register.print srcs2)
    148150        lbl
    149151  | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
    150152      Printf.sprintf "make_St_load %s (%s) %s %s %s"
    151         (print_memory_q chunk)
     153        (print_quantity chunk)
    152154        (print_addressing mode)
    153155        (print_args args)
    154         (print_reg_list dests)
     156        (Register.print dests)
    155157        lbl
    156158  | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
    157159      Printf.sprintf "make_St_store %s (%s) %s %s %s"
    158         (print_memory_q chunk)
     160        (print_quantity chunk)
    159161        (print_addressing mode)
    160162        (print_args args)
    161         (print_reg_list srcs)
     163        (Register.print srcs)
    162164        lbl
    163165  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    164       Printf.sprintf "make_St_call_id id_%s %s %s (%s) %s"
     166      Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) (%s) %s"
    165167        f
    166168        (print_params args)
    167         (print_reg_list res)
     169        (Register.print res)
    168170        (print_sig sg)
    169171        lbl
    170172  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    171       Printf.sprintf "make_St_call_ptr %s %s %s (%s) %s"
    172         (print_reg_list f)
     173      Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) (%s) %s"
     174        (Register.print f)
    173175        (print_params args)
    174         (print_reg_list res)
     176        (Register.print res)
    175177        (print_sig sg)
    176178        lbl
     
    182184  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    183185      Printf.sprintf "make_St_tailcall_ptr %s %s (%s)"
    184         (print_reg_list f)
     186        (Register.print f)
    185187        (print_params args)
    186188        (print_sig sg)
     
    193195      Printf.sprintf "make_St_cond1 %s %s %s %s"
    194196        (print_op1 op1)
    195         (print_reg_list srcs)
     197        (Register.print srcs)
    196198        lbl_true
    197199        lbl_false
     
    199201      Printf.sprintf "make_St_cond2 %s %s %s %s %s"
    200202        (print_op2 op2)
    201         (print_reg_list srcs1)
    202         (print_reg_list srcs2)
     203        (Register.print srcs1)
     204        (Register.print srcs2)
    203205        lbl_true
    204206        lbl_false
    205207  | RTLabs.St_jumptable (rs, tbl) ->
    206208      Printf.sprintf "make_St_jumptable %s [%s]"
    207         (print_reg_list rs)
     209        (Register.print rs)
    208210        (print_table tbl)
    209   | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (print_reg_list rs)
     211  | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (Register.print rs)
    210212
    211213let print_cost_labels n c =
     
    246248let print_internal_decl n f def m =
    247249  Printf.sprintf
    248     "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s(%s)\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
     250    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s(%s)\n%s(Some ? %s)\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
    249251    (n_spaces n)
    250252    f
     
    262264    (n_spaces (n+2))
    263265    (print_locals def.RTLabs.f_locals)
     266    (n_spaces (n+2))
     267    (print_locals def.RTLabs.f_ptrs)
    264268    (n_spaces (n+2))
    265269    def.RTLabs.f_stacksize
  • src/RTLabs/import.ma

    r738 r750  
    1010].
    1111
    12 definition pre_registers ≝ Sig nat (Vector nat).
     12definition pre_register ≝ nat.
    1313
    1414record pre_internal_function : Type[0] ≝
    1515{ pf_sig       : signature
    16 ; pf_result    : pre_registers
    17 ; pf_params    : list pre_registers
    18 ; pf_locals    : list pre_registers
     16; pf_result    : option pre_register
     17; pf_params    : list pre_register
     18; pf_locals    : list pre_register
     19; pf_ptrs      : list pre_register
    1920; pf_stacksize : nat
    20 ; pf_graph     : list (nat × ((nat → res register) → (nat → res label) → res statement))
     21; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
    2122; pf_entry     : nat
    2223; pf_exit      : nat
    2324}.
    2425(* XXX projection generation with nat broken *)
    25 definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ s _ _ _ ⇒ s ].
    26 definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ g _ _ ⇒ g ].
    27 definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ e _ ⇒ e ].
    28 definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e ⇒ e ].
     26definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].
     27definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].
     28definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].
     29definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].
    2930
    30 definition make_registers :
    31   (nat → option register) → pre_registers → universe RegisterTag →
    32   res ((nat → option register) × (universe RegisterTag) × registers) ≝
    33 λm,rs0,g.
    34 match rs0 with [ dp n rs ⇒
    35   do 〈m,grs〉 ← fold_right_i ??? (λn,r,mr.
    36                   do 〈m,grs〉 ← mr;
    37                   let 〈g,rs〉 ≝ grs in
    38                   match m r with
    39                   [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
    40                   | None ⇒ do 〈r',g'〉 ← fresh ? g;
    41                            OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
    42                   ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
    43   let 〈g',rs'〉 ≝ grs in
    44     OK ? 〈〈m,g'〉,dp ?? n rs'〉
    45 ].
     31definition make_register :
     32  (pre_register → option register) → pre_register → universe RegisterTag →
     33  res ((nat → option register) × (universe RegisterTag) × register) ≝
     34λm,reg,g.
     35  match m reg with
     36  [ Some r' ⇒ OK ? 〈〈m,g〉,r'〉
     37  | None ⇒ do 〈r',g'〉 ← fresh ? g;
     38           OK ? 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     39  ]
     40.
    4641
    4742definition make_registers_list :
    48   (nat → option register) → list pre_registers → universe RegisterTag →
    49   res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
     43  (nat → option register) → list pre_register → universe RegisterTag →
     44  res ((nat → option register) × (universe RegisterTag) × (list register)) ≝
    5045λm,lrs,g.
    5146foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
    5247                   let 〈m,g〉 ≝ acc' in
    53                    do 〈mg,rs'〉 ← make_registers m rs g;
     48                   do 〈mg,rs'〉 ← make_register m rs g;
    5449                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    5550
     
    5752λpre_f.
    5853  let rgen0 ≝ new_universe RegisterTag in
    59   do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0;
     54  do 〈rmapgen1, result〉 ← match pf_result pre_f with
     55                          [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
     56                          | Some r ⇒ do 〈x,y〉 ← make_register (λ_.None ?) r rgen0; OK ? 〈x,Some ? y〉
     57                          ];
    6058  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
    6159  do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
     
    6361  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
    6462  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
    65   let rmap ≝ λn. opt_to_res … (rmap3 n) in
     63  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
     64  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
     65  let rmap ≝ λn. opt_to_res … (rmap4 n) in
    6666  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    6767  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
     
    7676  OK ? (Internal ? (mk_internal_function
    7777         gen
    78          rgen3
     78         rgen4
    7979         (pf_sig pre_f)
    8080         result
    8181         params
    8282         locals
     83         ptrs
    8384         (pf_stacksize pre_f)
    8485         graph
     
    8788         )).
    8889
    89 definition make_regs : (nat → res register) → pre_registers → res registers ≝
    90 λm,p.
    91 match p with
    92 [ dp n ps ⇒
    93     do rs ← fold_right_i ??? (λn,r,rs0.
    94                   do rs ← rs0;
    95                   do r' ← m r;
    96                   OK ? (r':::rs)) (OK ? [[ ]]) ps;
    97     OK ? (dp ?? n rs)
    98 ].
    99 
    100 definition make_regs_list : (nat → res register) → list pre_registers → res (list registers) ≝
    101 λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps.
     90definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
     91λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
    10292
    10393(* XXX move somewhere sensible *)
     
    110100].
    111101
    112 definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝
    113 λmp,m. mmap_vec ?? (make_regs mp) ?.
     102definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_register (addr_mode_args m) → res (addr m) ≝
     103λmp,m. mmap_vec ?? mp ?.
     104
     105definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
     106λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
    114107
    115108let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
    116109let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
    117 let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do l' ← f l; OK ? (St_const rs' cst l').
    118 let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src' ← make_regs r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
    119 let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src1' ← make_regs r src1; do src2' ← make_regs r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
    120 let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
    121 let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
    122 let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l').
    123 let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l').
    124 let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_regs_list r args; OK statement (St_tailcall_id id args' sig).
    125 let rec make_St_tailcall_ptr frs args sig ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; OK statement (St_tailcall_ptr frs' args' sig).
     110let 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').
     111let 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').
     112let 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').
     113let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
     114let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
     115let rec make_St_call_id id args dst sig 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' sig l').
     116let rec make_St_call_ptr frs args dst sig 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' sig l').
     117let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args' sig).
     118let rec make_St_tailcall_ptr frs args sig ≝ λ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' sig).
    126119let rec make_St_condcst cst ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_condcst cst ltrue' lfalse').
    127 let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond1 op src' ltrue' lfalse').
    128 let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← make_regs r src1; do src2' ← make_regs r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
    129 let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
    130 let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; OK statement (St_return src').
     120let rec make_St_cond1 op 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_cond1 op src' ltrue' lfalse').
     121let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← r src1; do src2' ← r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
     122let 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').
     123let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
    131124
  • src/RTLabs/test/search.ma

    r737 r750  
    66
    77  definition id_search := ident_of_nat 0.
    8   definition search9 := 40.
    9   definition search8 := 39.
    10   definition search7 := 38.
    11   definition search6 := 37.
    12   definition search5 := 36.
     8  definition search9 := 53.
     9  definition search8 := 52.
     10  definition search7 := 51.
     11  definition search6 := 50.
     12  definition search53 := 49.
     13  definition search52 := 48.
     14  definition search51 := 47.
     15  definition search50 := 46.
     16  definition search5 := 45.
     17  definition search49 := 44.
     18  definition search48 := 43.
     19  definition search47 := 42.
     20  definition search46 := 41.
     21  definition search45 := 40.
     22  definition search44 := 39.
     23  definition search43 := 38.
     24  definition search42 := 37.
     25  definition search41 := 36.
    1326  definition search40 := 35.
    1427  definition search4 := 34.
     
    4861  definition search0 := 0.
    4962  definition C_cost0 := costlabel_of_nat 8.
    50   definition C_cost1 := costlabel_of_nat 7.
    51   definition C_cost8 := costlabel_of_nat 6.
     63  definition C_cost8 := costlabel_of_nat 7.
     64  definition C_cost1 := costlabel_of_nat 6.
    5265  definition C_cost6 := costlabel_of_nat 5.
    53   definition C_cost7 := costlabel_of_nat 4.
    54   definition C_cost4 := costlabel_of_nat 3.
     66  definition C_cost4 := costlabel_of_nat 4.
     67  definition C_cost7 := costlabel_of_nat 3.
    5568  definition C_cost5 := costlabel_of_nat 2.
    5669  definition C_cost2 := costlabel_of_nat 1.
     
    6073  definition pre_search := mk_pre_internal_function
    6174    (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
    62     (dp ?? 1 [[10]])
    63     [(dp ?? 2 [[9 ; 8]]); (dp ?? 1 [[2]]); (dp ?? 1 [[3]])]
    64     [(dp ?? 1 [[4]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]]); (dp ?? 1 [[7]]); (dp ?? 2 [[9 ; 8]]); (dp ?? 1 [[10]]); (dp ?? 1 [[11]]); (dp ?? 1 [[12]]); (dp ?? 1 [[13]]); (dp ?? 2 [[15 ; 14]]); (dp ?? 1 [[16]]); (dp ?? 1 [[17]]); (dp ?? 1 [[18]]); (dp ?? 1 [[19]]); (dp ?? 2 [[21 ; 20]]); (dp ?? 1 [[22]]); (dp ?? 1 [[23]]); (dp ?? 1 [[24]]); (dp ?? 2 [[26 ; 25]]); (dp ?? 1 [[27]]); (dp ?? 1 [[28]]); (dp ?? 1 [[29]]); (dp ?? 1 [[30]]); (dp ?? 1 [[31]]); (dp ?? 1 [[32]])]
     75    (Some ? 8)
     76    [7; 1; 2]
     77    [3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35; 36; 37; 38; 39; 40]
     78    [7; 15; 23; 29]
    6579    0
    6680    [
    67     (pair ?? search9 (make_St_cond2 (Ocmp Clt) (dp ?? 1 [[13]]) (dp ?? 1 [[3]]) search8 search5));
    68     (pair ?? search8 (make_St_cost C_cost0 search7));
    69     (pair ?? search7 (make_St_const (dp ?? 1 [[12]]) (Ointconst (repr 1)) search6));
    70     (pair ?? search6 (make_St_op2 Oadd (dp ?? 1 [[5]]) (dp ?? 1 [[7]]) (dp ?? 1 [[12]]) search4));
     81    (pair ?? search9 (make_St_cost C_cost0 search8));
     82    (pair ?? search8 (make_St_op1 Ocast8unsigned 10 6 search7));
     83    (pair ?? search7 (make_St_const 11 (Ointconst (repr 1)) search6));
     84    (pair ?? search6 (make_St_op2 Oadd 4 10 11 search4));
     85    (pair ?? search53 (make_St_cost C_cost8 search52));
     86    (pair ?? search52 (make_St_const 4 (Ointconst (repr 0)) search51));
     87    (pair ?? search51 (make_St_op1 Ocast8unsigned 39 1 search50));
     88    (pair ?? search50 (make_St_const 40 (Ointconst (repr 1)) search49));
    7189    (pair ?? search5 (make_St_cost C_cost1 search4));
    72     (pair ?? search40 (make_St_cost C_cost8 search39));
    73     (pair ?? search4 (make_St_skip search36));
    74     (pair ?? search39 (make_St_const (dp ?? 1 [[5]]) (Ointconst (repr 0)) search38));
    75     (pair ?? search38 (make_St_const (dp ?? 1 [[32]]) (Ointconst (repr 1)) search37));
    76     (pair ?? search37 (make_St_op2 Osub (dp ?? 1 [[6]]) (dp ?? 1 [[2]]) (dp ?? 1 [[32]]) search4));
    77     (pair ?? search36 (make_St_op2 (Ocmp Cge) (dp ?? 1 [[31]]) (dp ?? 1 [[6]]) (dp ?? 1 [[5]]) search35));
    78     (pair ?? search35 (make_St_cond1 Onotbool (dp ?? 1 [[31]]) search3 search34));
    79     (pair ?? search34 (make_St_cost C_cost6 search33));
    80     (pair ?? search33 (make_St_op2 Oadd (dp ?? 1 [[29]]) (dp ?? 1 [[6]]) (dp ?? 1 [[5]]) search32));
    81     (pair ?? search32 (make_St_const (dp ?? 1 [[30]]) (Ointconst (repr 2)) search31));
    82     (pair ?? search31 (make_St_op2 Odivu (dp ?? 1 [[7]]) (dp ?? 1 [[29]]) (dp ?? 1 [[30]]) search30));
    83     (pair ?? search30 (make_St_const (dp ?? 1 [[28]]) (Ointconst (repr 1)) search29));
     90    (pair ?? search49 (make_St_op2 Osub 5 39 40 search4));
     91    (pair ?? search48 (make_St_op1 Ocast8unsigned 37 5 search47));
     92    (pair ?? search47 (make_St_op1 Ocast8unsigned 38 4 search46));
     93    (pair ?? search46 (make_St_op2 (Ocmp Cge) 36 37 38 search45));
     94    (pair ?? search45 (make_St_cond1 Onotbool 36 search3 search44));
     95    (pair ?? search44 (make_St_cost C_cost6 search43));
     96    (pair ?? search43 (make_St_op1 Ocast8unsigned 34 5 search42));
     97    (pair ?? search42 (make_St_op1 Ocast8unsigned 35 4 search41));
     98    (pair ?? search41 (make_St_op2 Oadd 32 34 35 search40));
     99    (pair ?? search40 (make_St_const 33 (Ointconst (repr 2)) search39));
     100    (pair ?? search4 (make_St_skip search48));
     101    (pair ?? search39 (make_St_op2 Odiv 6 32 33 search38));
     102    (pair ?? search38 (make_St_const 31 (Ointconst (repr 1)) search37));
     103    (pair ?? search37 (make_St_op2 Omul 30 6 31 search36));
     104    (pair ?? search36 (make_St_op2 Oaddp 29 7 30 search35));
     105    (pair ?? search35 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[29]] 28 search34));
     106    (pair ?? search34 (make_St_op1 Ocast8unsigned 26 28 search33));
     107    (pair ?? search33 (make_St_op1 Ocast8unsigned 27 2 search32));
     108    (pair ?? search32 (make_St_cond2 (Ocmp Ceq) 26 27 search31 search29));
     109    (pair ?? search31 (make_St_cost C_cost4 search30));
     110    (pair ?? search30 (make_St_op1 Oid 8 6 search0));
    84111    (pair ?? search3 (make_St_cost C_cost7 search2));
    85     (pair ?? search29 (make_St_op2 Omul (dp ?? 1 [[27]]) (dp ?? 1 [[7]]) (dp ?? 1 [[28]]) search28));
    86     (pair ?? search28 (make_St_op2 Oaddp (dp ?? 2 [[26 ; 25]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[27]]) search27));
    87     (pair ?? search27 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[26 ; 25]])]] (dp ?? 1 [[24]]) search26));
    88     (pair ?? search26 (make_St_cond2 (Ocmp Ceq) (dp ?? 1 [[24]]) (dp ?? 1 [[3]]) search25 search23));
    89     (pair ?? search25 (make_St_cost C_cost4 search24));
    90     (pair ?? search24 (make_St_op1 Oid (dp ?? 1 [[10]]) (dp ?? 1 [[7]]) search0));
    91     (pair ?? search23 (make_St_cost C_cost5 search22));
    92     (pair ?? search22 (make_St_const (dp ?? 1 [[23]]) (Ointconst (repr 1)) search21));
    93     (pair ?? search21 (make_St_op2 Omul (dp ?? 1 [[22]]) (dp ?? 1 [[7]]) (dp ?? 1 [[23]]) search20));
    94     (pair ?? search20 (make_St_op2 Oaddp (dp ?? 2 [[21 ; 20]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[22]]) search19));
    95     (pair ?? search2 (make_St_const (dp ?? 1 [[11]]) (Ointconst (repr 1)) search1));
    96     (pair ?? search19 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[21 ; 20]])]] (dp ?? 1 [[19]]) search18));
    97     (pair ?? search18 (make_St_cond2 (Ocmp Cgt) (dp ?? 1 [[19]]) (dp ?? 1 [[3]]) search17 search14));
    98     (pair ?? search17 (make_St_cost C_cost2 search16));
    99     (pair ?? search16 (make_St_const (dp ?? 1 [[18]]) (Ointconst (repr 1)) search15));
    100     (pair ?? search15 (make_St_op2 Osub (dp ?? 1 [[6]]) (dp ?? 1 [[7]]) (dp ?? 1 [[18]]) search13));
    101     (pair ?? search14 (make_St_cost C_cost3 search13));
    102     (pair ?? search13 (make_St_const (dp ?? 1 [[17]]) (Ointconst (repr 1)) search12));
    103     (pair ?? search12 (make_St_op2 Omul (dp ?? 1 [[16]]) (dp ?? 1 [[7]]) (dp ?? 1 [[17]]) search11));
    104     (pair ?? search11 (make_St_op2 Oaddp (dp ?? 2 [[15 ; 14]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[16]]) search10));
    105     (pair ?? search10 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[15 ; 14]])]] (dp ?? 1 [[13]]) search9));
    106     (pair ?? search1 (make_St_op1 Onegint (dp ?? 1 [[10]]) (dp ?? 1 [[11]]) search0));
    107     (pair ?? search0 (make_St_return (dp ?? 1 [[10]])))
     112    (pair ?? search29 (make_St_cost C_cost5 search28));
     113    (pair ?? search28 (make_St_const 25 (Ointconst (repr 1)) search27));
     114    (pair ?? search27 (make_St_op2 Omul 24 6 25 search26));
     115    (pair ?? search26 (make_St_op2 Oaddp 23 7 24 search25));
     116    (pair ?? search25 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[23]] 22 search24));
     117    (pair ?? search24 (make_St_op1 Ocast8unsigned 20 22 search23));
     118    (pair ?? search23 (make_St_op1 Ocast8unsigned 21 2 search22));
     119    (pair ?? search22 (make_St_cond2 (Ocmp Cgt) 20 21 search21 search17));
     120    (pair ?? search21 (make_St_cost C_cost2 search20));
     121    (pair ?? search20 (make_St_op1 Ocast8unsigned 18 6 search19));
     122    (pair ?? search2 (make_St_const 9 (Ointconst (repr 1)) search1));
     123    (pair ?? search19 (make_St_const 19 (Ointconst (repr 1)) search18));
     124    (pair ?? search18 (make_St_op2 Osub 5 18 19 search16));
     125    (pair ?? search17 (make_St_cost C_cost3 search16));
     126    (pair ?? search16 (make_St_const 17 (Ointconst (repr 1)) search15));
     127    (pair ?? search15 (make_St_op2 Omul 16 6 17 search14));
     128    (pair ?? search14 (make_St_op2 Oaddp 15 7 16 search13));
     129    (pair ?? search13 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[15]] 14 search12));
     130    (pair ?? search12 (make_St_op1 Ocast8unsigned 12 14 search11));
     131    (pair ?? search11 (make_St_op1 Ocast8unsigned 13 2 search10));
     132    (pair ?? search10 (make_St_cond2 (Ocmp Clt) 12 13 search9 search5));
     133    (pair ?? search1 (make_St_op1 Onegint 8 9 search0));
     134    (pair ?? search0 (make_St_return 8))
    108135]
    109136
    110     search40
     137    search53
    111138    search0.
    112139
     
    159186  definition pre_main := mk_pre_internal_function
    160187    (mk_signature [] (Some ? ASTint))
    161     (dp ?? 1 [[2]])
     188    (Some ? 2)
    162189    []
    163     [(dp ?? 1 [[0]]); (dp ?? 1 [[1]]); (dp ?? 1 [[2]]); (dp ?? 2 [[4 ; 3]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]]); (dp ?? 2 [[8 ; 7]]); (dp ?? 1 [[9]]); (dp ?? 2 [[11 ; 10]]); (dp ?? 1 [[12]]); (dp ?? 1 [[13]]); (dp ?? 1 [[14]]); (dp ?? 2 [[16 ; 15]]); (dp ?? 1 [[17]]); (dp ?? 2 [[19 ; 18]]); (dp ?? 1 [[20]]); (dp ?? 1 [[21]]); (dp ?? 1 [[22]]); (dp ?? 2 [[24 ; 23]]); (dp ?? 1 [[25]]); (dp ?? 2 [[27 ; 26]]); (dp ?? 1 [[28]]); (dp ?? 1 [[29]]); (dp ?? 1 [[30]]); (dp ?? 2 [[32 ; 31]]); (dp ?? 1 [[33]]); (dp ?? 2 [[35 ; 34]]); (dp ?? 1 [[36]]); (dp ?? 1 [[37]]); (dp ?? 1 [[38]]); (dp ?? 2 [[40 ; 39]]); (dp ?? 1 [[41]]); (dp ?? 2 [[43 ; 42]]); (dp ?? 1 [[44]]); (dp ?? 1 [[45]]); (dp ?? 1 [[46]])]
     190    [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35]
     191    [3; 6; 8; 12; 14; 18; 20; 24; 26; 30; 32]
    164192    5
    165193    [
    166     (pair ?? main9 (make_St_op2 Omul (dp ?? 1 [[12]]) (dp ?? 1 [[13]]) (dp ?? 1 [[14]]) main8));
    167     (pair ?? main8 (make_St_op2 Oaddp (dp ?? 2 [[8 ; 7]]) (dp ?? 2 [[11 ; 10]]) (dp ?? 1 [[12]]) main7));
    168     (pair ?? main7 (make_St_const (dp ?? 1 [[9]]) (Ointconst (repr 120)) main6));
    169     (pair ?? main6 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[8 ; 7]])]] (dp ?? 1 [[9]]) main5));
    170     (pair ?? main5 (make_St_const (dp ?? 2 [[4 ; 3]]) (Oaddrstack (repr 0)) main4));
     194    (pair ?? main9 (make_St_op2 Omul 9 10 11 main8));
     195    (pair ?? main8 (make_St_op2 Oaddp 6 8 9 main7));
     196    (pair ?? main7 (make_St_const 7 (Ointconst (repr 120)) main6));
     197    (pair ?? main6 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[6]] 7 main5));
     198    (pair ?? main5 (make_St_const 3 (Oaddrstack (repr 0)) main4));
    171199    (pair ?? main41 (make_St_cost C_cost9 main40));
    172     (pair ?? main40 (make_St_const (dp ?? 2 [[43 ; 42]]) (Oaddrstack (repr 0)) main39));
    173     (pair ?? main4 (make_St_const (dp ?? 1 [[5]]) (Ointconst (repr 5)) main3));
    174     (pair ?? main39 (make_St_const (dp ?? 1 [[45]]) (Ointconst (repr 0)) main38));
    175     (pair ?? main38 (make_St_const (dp ?? 1 [[46]]) (Ointconst (repr 1)) main37));
    176     (pair ?? main37 (make_St_op2 Omul (dp ?? 1 [[44]]) (dp ?? 1 [[45]]) (dp ?? 1 [[46]]) main36));
    177     (pair ?? main36 (make_St_op2 Oaddp (dp ?? 2 [[40 ; 39]]) (dp ?? 2 [[43 ; 42]]) (dp ?? 1 [[44]]) main35));
    178     (pair ?? main35 (make_St_const (dp ?? 1 [[41]]) (Ointconst (repr 0)) main34));
    179     (pair ?? main34 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[40 ; 39]])]] (dp ?? 1 [[41]]) main33));
    180     (pair ?? main33 (make_St_const (dp ?? 2 [[35 ; 34]]) (Oaddrstack (repr 0)) main32));
    181     (pair ?? main32 (make_St_const (dp ?? 1 [[37]]) (Ointconst (repr 1)) main31));
    182     (pair ?? main31 (make_St_const (dp ?? 1 [[38]]) (Ointconst (repr 1)) main30));
    183     (pair ?? main30 (make_St_op2 Omul (dp ?? 1 [[36]]) (dp ?? 1 [[37]]) (dp ?? 1 [[38]]) main29));
    184     (pair ?? main3 (make_St_const (dp ?? 1 [[6]]) (Ointconst (repr 57)) main2));
    185     (pair ?? main29 (make_St_op2 Oaddp (dp ?? 2 [[32 ; 31]]) (dp ?? 2 [[35 ; 34]]) (dp ?? 1 [[36]]) main28));
    186     (pair ?? main28 (make_St_const (dp ?? 1 [[33]]) (Ointconst (repr 18)) main27));
    187     (pair ?? main27 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[32 ; 31]])]] (dp ?? 1 [[33]]) main26));
    188     (pair ?? main26 (make_St_const (dp ?? 2 [[27 ; 26]]) (Oaddrstack (repr 0)) main25));
    189     (pair ?? main25 (make_St_const (dp ?? 1 [[29]]) (Ointconst (repr 2)) main24));
    190     (pair ?? main24 (make_St_const (dp ?? 1 [[30]]) (Ointconst (repr 1)) main23));
    191     (pair ?? main23 (make_St_op2 Omul (dp ?? 1 [[28]]) (dp ?? 1 [[29]]) (dp ?? 1 [[30]]) main22));
    192     (pair ?? main22 (make_St_op2 Oaddp (dp ?? 2 [[24 ; 23]]) (dp ?? 2 [[27 ; 26]]) (dp ?? 1 [[28]]) main21));
    193     (pair ?? main21 (make_St_const (dp ?? 1 [[25]]) (Ointconst (repr 23)) main20));
    194     (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[24 ; 23]])]] (dp ?? 1 [[25]]) main19));
    195     (pair ?? main2 (make_St_call_id id_search [(dp ?? 2 [[4 ; 3]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]])] (dp ?? 1 [[1]]) (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) main1));
    196     (pair ?? main19 (make_St_const (dp ?? 2 [[19 ; 18]]) (Oaddrstack (repr 0)) main18));
    197     (pair ?? main18 (make_St_const (dp ?? 1 [[21]]) (Ointconst (repr 3)) main17));
    198     (pair ?? main17 (make_St_const (dp ?? 1 [[22]]) (Ointconst (repr 1)) main16));
    199     (pair ?? main16 (make_St_op2 Omul (dp ?? 1 [[20]]) (dp ?? 1 [[21]]) (dp ?? 1 [[22]]) main15));
    200     (pair ?? main15 (make_St_op2 Oaddp (dp ?? 2 [[16 ; 15]]) (dp ?? 2 [[19 ; 18]]) (dp ?? 1 [[20]]) main14));
    201     (pair ?? main14 (make_St_const (dp ?? 1 [[17]]) (Ointconst (repr 57)) main13));
    202     (pair ?? main13 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[16 ; 15]])]] (dp ?? 1 [[17]]) main12));
    203     (pair ?? main12 (make_St_const (dp ?? 2 [[11 ; 10]]) (Oaddrstack (repr 0)) main11));
    204     (pair ?? main11 (make_St_const (dp ?? 1 [[13]]) (Ointconst (repr 4)) main10));
    205     (pair ?? main10 (make_St_const (dp ?? 1 [[14]]) (Ointconst (repr 1)) main9));
    206     (pair ?? main1 (make_St_op1 Oid (dp ?? 1 [[2]]) (dp ?? 1 [[1]]) main0));
    207     (pair ?? main0 (make_St_return (dp ?? 1 [[2]])))
     200    (pair ?? main40 (make_St_const 32 (Oaddrstack (repr 0)) main39));
     201    (pair ?? main4 (make_St_const 4 (Ointconst (repr 5)) main3));
     202    (pair ?? main39 (make_St_const 34 (Ointconst (repr 0)) main38));
     203    (pair ?? main38 (make_St_const 35 (Ointconst (repr 1)) main37));
     204    (pair ?? main37 (make_St_op2 Omul 33 34 35 main36));
     205    (pair ?? main36 (make_St_op2 Oaddp 30 32 33 main35));
     206    (pair ?? main35 (make_St_const 31 (Ointconst (repr 0)) main34));
     207    (pair ?? main34 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[30]] 31 main33));
     208    (pair ?? main33 (make_St_const 26 (Oaddrstack (repr 0)) main32));
     209    (pair ?? main32 (make_St_const 28 (Ointconst (repr 1)) main31));
     210    (pair ?? main31 (make_St_const 29 (Ointconst (repr 1)) main30));
     211    (pair ?? main30 (make_St_op2 Omul 27 28 29 main29));
     212    (pair ?? main3 (make_St_const 5 (Ointconst (repr 57)) main2));
     213    (pair ?? main29 (make_St_op2 Oaddp 24 26 27 main28));
     214    (pair ?? main28 (make_St_const 25 (Ointconst (repr 18)) main27));
     215    (pair ?? main27 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[24]] 25 main26));
     216    (pair ?? main26 (make_St_const 20 (Oaddrstack (repr 0)) main25));
     217    (pair ?? main25 (make_St_const 22 (Ointconst (repr 2)) main24));
     218    (pair ?? main24 (make_St_const 23 (Ointconst (repr 1)) main23));
     219    (pair ?? main23 (make_St_op2 Omul 21 22 23 main22));
     220    (pair ?? main22 (make_St_op2 Oaddp 18 20 21 main21));
     221    (pair ?? main21 (make_St_const 19 (Ointconst (repr 23)) main20));
     222    (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[18]] 19 main19));
     223    (pair ?? main2 (make_St_call_id id_search [3; 4; 5] (Some ? 1) (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) main1));
     224    (pair ?? main19 (make_St_const 14 (Oaddrstack (repr 0)) main18));
     225    (pair ?? main18 (make_St_const 16 (Ointconst (repr 3)) main17));
     226    (pair ?? main17 (make_St_const 17 (Ointconst (repr 1)) main16));
     227    (pair ?? main16 (make_St_op2 Omul 15 16 17 main15));
     228    (pair ?? main15 (make_St_op2 Oaddp 12 14 15 main14));
     229    (pair ?? main14 (make_St_const 13 (Ointconst (repr 57)) main13));
     230    (pair ?? main13 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[12]] 13 main12));
     231    (pair ?? main12 (make_St_const 8 (Oaddrstack (repr 0)) main11));
     232    (pair ?? main11 (make_St_const 10 (Ointconst (repr 4)) main10));
     233    (pair ?? main10 (make_St_const 11 (Ointconst (repr 1)) main9));
     234    (pair ?? main1 (make_St_op1 Ocast8unsigned 2 1 main0));
     235    (pair ?? main0 (make_St_return 2))
    208236]
    209237
     
    226254).
    227255
    228    example exec: result ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 100 [ ]; OK ? r).
     256   example exec: finishes_with (repr 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
    229257   normalize  (* you can examine the result here *)
    230    % qed.
     258   @refl qed.
Note: See TracChangeset for help on using the changeset viewer.