Changeset 755


Ignore:
Timestamp:
Apr 15, 2011, 4:26:23 PM (9 years ago)
Author:
campbell
Message:

An experimental branch of the Cminor semantics.

Location:
Deliverables/D3.3
Files:
4 added
1 edited
3 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Cminor-experiment/semantics.ma

    r754 r755  
    1111definition genv ≝ (genv_t Genv) (fundef internal_function).
    1212
    13 inductive cont : Type[0] ≝
    14 | Kstop : cont
    15 | Kseq : stmt → cont → cont
    16 | Kblock : cont → cont
    17 | Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.
     13inductive cont : nat → Type[0] ≝
     14| Kstop : cont O
     15| Kseq : ∀n. stmt n → cont n → cont n
     16| Kblock : ∀n. cont n → cont (S n)
     17| Kcall : option ident → internal_function → block (* sp *) → env → ∀n. cont n → cont O.
    1818
    1919inductive state : Type[0] ≝
    2020| State:
    2121    ∀    f: internal_function.
    22     ∀    s: stmt.
     22    ∀    n: nat.
     23    ∀    s: stmt n.
    2324    ∀   en: env.
    2425    ∀    m: mem.
    2526    ∀   sp: block.
    26     ∀    k: cont.
     27    ∀    k: cont n.
    2728            state
    2829| Callstate:
     
    3031    ∀ args: list val.
    3132    ∀    m: mem.
    32     ∀    k: cont.
     33    ∀    k: cont O.
    3334            state
    3435| Returnstate:
    3536    ∀    v: option val.
    3637    ∀    m: mem.
    37     ∀    k: cont.
     38    ∀    k: cont O.
    3839            state.
    3940
    4041definition mem_of_state : state → mem ≝
    4142λst. match st with
    42 [ State _ _ _ m _ _ ⇒ m
     43[ State _ _ _ _ m _ _ ⇒ m
    4344| Callstate _ _ m _ ⇒ m
    4445| Returnstate _ m _ ⇒ m
     
    7677].
    7778
    78 let rec k_exit (n:nat) (k:cont) on k : res cont ≝
    79 match k with
    80 [ Kstop ⇒ Error ?
    81 | Kseq _ k' ⇒ k_exit n k'
    82 | Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
    83 | Kcall _ _ _ _ _ ⇒ Error ?
    84 ].
     79let rec k_exit (n:nat) (m:Fin n) (k:cont n) on k : Sig nat cont ≝
     80(match k return λx.λ_.Fin x → Sig nat cont with
     81[ Kstop ⇒ λm.?
     82| Kseq n' _ k' ⇒ λm. k_exit ? m k'
     83| Kblock n' k' ⇒ λm.match m return λx.λ_.match x with [ O ⇒ True | S y ⇒ (Fin y → Sig nat cont) → Sig nat cont ] with [ FO _ ⇒ λ_.dp ??? k' | FS n' m' ⇒ λr.r m' ] (λm'. k_exit ? m' k')
     84| Kcall _ _ _ _ _ _ ⇒ λm.?
     85]) m.
     86@(match m return λx.λ_.match x return λ_.Type[0] with [ O ⇒ Sig nat cont | S _ ⇒ True] with [ FO x ⇒ I | FS x y ⇒ I ])
     87qed.
     88
    8589
    8690let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
     
    9296].
    9397
    94 let rec call_cont (k:cont) : cont ≝
    95 match k with
    96 [ Kseq _ k' ⇒ call_cont k'
    97 | Kblock k' ⇒ call_cont k'
    98 | _ ⇒ k
    99 ].
    100 
    101 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    102 match s with
    103 [ St_seq s1 s2 ⇒
    104     match find_label l s1 (Kseq s2 k) with
    105     [ None ⇒ find_label l s2 k
     98let rec call_cont (n:nat) (k:cont n) on k : cont O ≝
     99match k return λ_.λ_.cont O with
     100[ Kseq _ _ k' ⇒ call_cont ? k'
     101| Kblock _ k' ⇒ call_cont ? k'
     102| Kstop ⇒ Kstop
     103| Kcall a b c d e f ⇒ Kcall a b c d e f
     104].
     105
     106let rec find_label (l:ident) (n:nat) (s:stmt n) (k:cont n) on s : option (Sig nat (λn.stmt n × (cont n))) ≝
     107(match s with
     108[ St_seq _ s1 s2 ⇒ λk.
     109    match find_label l ? s1 (Kseq ? s2 k) with
     110    [ None ⇒ find_label l ? s2 k
    106111    | Some sk ⇒ Some ? sk
    107112    ]
    108 | St_ifthenelse _ s1 s2 ⇒
    109     match find_label l s1 k with
    110     [ None ⇒ find_label l s2 k
     113| St_ifthenelse _ _ s1 s2 ⇒ λk.
     114    match find_label l ? s1 k with
     115    [ None ⇒ find_label l ? s2 k
    111116    | Some sk ⇒ Some ? sk
    112117    ]
    113 | St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
    114 | St_block s' ⇒ find_label l s' (Kblock k)
    115 | St_label l' s' ⇒
     118| St_loop _ s' ⇒ λk. find_label l ? s' (Kseq ? (St_loop ? s') k)
     119| St_block _ s' ⇒ λk. find_label l ? s' (Kblock ? k)
     120| St_label l' _ s' ⇒ λk.
    116121    match ident_eq l l' with
    117     [ inl _ ⇒ Some ? 〈s',k〉
    118     | inr _ ⇒ find_label l s' k
    119     ]
    120 | St_cost _ s' ⇒ find_label l s' k
    121 | _ ⇒ None ?
    122 ].
     122    [ inl _ ⇒ Some ? (dp … 〈s',k〉)
     123    | inr _ ⇒ find_label l ? s' k
     124    ]
     125| St_cost _ _ s' ⇒ λk. find_label l ? s' k
     126| _ ⇒ λk. None ?
     127]) k.
    123128
    124129let rec bind_params (vs:list val) (ids:list ident) : res env ≝
     
    137142λge,st.
    138143match st with
    139 [ State f s en m sp k ⇒
    140     match s with
    141     [ St_skip
     144[ State f n0 s en m sp k ⇒
     145    (match s return λx.λ_. cont x → IO io_out io_in (trace × state) with
     146    [ St_skip n ⇒ λk.
    142147        match k with
    143148        [ Kstop ⇒ Wrong ???
    144         | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
    145         | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
     149        | Kseq n' s' k' ⇒ ret ? 〈E0, State f n' s' en m sp k'〉
     150        | Kblock n' k' ⇒ ret ? 〈E0, State f n' (St_skip ?) en m sp k'〉
    146151          (* cminor allows functions without an explicit return statement *)
    147         | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k
    148         ]
    149     | St_assign id e
     152        | Kcall a b c d e f ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (Kcall a b c d e f)
     153        ]
     154    | St_assign id e n ⇒ λk.
    150155        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    151         ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
    152     | St_store chunk edst e
     156        ret ? 〈tr, State f n (St_skip ?) (add ?? en id v) m sp k〉
     157    | St_store chunk edst e n ⇒ λk.
    153158        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    154159        ! 〈tr',v〉 ← eval_expr ge e en sp m;
    155160        ! m' ← opt_to_res … (storev chunk m vdst v);
    156         ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    157 
    158     | St_call dst ef args sig (* XXX sig unused? *)
     161        ret ? 〈tr ⧺ tr', State f n (St_skip ?) en m' sp k〉
     162
     163    | St_call dst ef args sig n ⇒ λk. (* XXX sig unused? *)
    159164        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    160165        ! fd ← opt_to_res … (find_funct ?? ge vf);
    161166        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    162         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    163     | St_tailcall ef args sig
     167        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en n k)〉
     168    | St_tailcall ef args sig n ⇒ λk.
    164169        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    165170        ! fd ← opt_to_res … (find_funct ?? ge vf);
    166171        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    167         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) k
     172        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont ? k)
    168173       
    169     | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    170     | St_ifthenelse e strue sfalse ⇒
     174    | St_seq n s1 s2 ⇒ λk. ret ? 〈E0, State f n s1 en m sp (Kseq ? s2 k)〉
     175    | St_ifthenelse e n strue sfalse ⇒ λk.
    171176        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    172177        ! b ← eval_bool_of_val v;
    173         ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
    174     | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
    175     | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
    176     | St_exit n ⇒
    177         ! k' ← k_exit n k;
    178         ret ? 〈E0, State f St_skip en m sp k'〉
    179     | St_switch e cs default ⇒
     178        ret ? 〈tr, State f n (if b then strue else sfalse) en m sp k〉
     179    | St_loop n s ⇒ λk. ret ? 〈E0, State f n s en m sp (Kseq ? (St_loop ? s) k)〉
     180    | St_block n s ⇒ λk. ret ? 〈E0, State f ? s en m sp (Kblock ? k)〉
     181    | St_exit n x ⇒ λk.
     182        match k_exit n x k with
     183        [ dp n' k' ⇒
     184            ret ? 〈E0, State f ? (St_skip ?) en m sp k'〉
     185        ]
     186    | St_switch e n cs default ⇒ λk.
    180187        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    181188        match v with
    182189        [ Vint i ⇒
    183             ! k' ← k_exit (find_case ? i cs default) k;
    184             ret ? 〈tr, State f St_skip en m sp k'〉
     190            match k_exit ? (find_case ? i cs default) k with
     191            [ dp n k' ⇒
     192                ret ? 〈tr, State f n (St_skip ?) en m sp k'〉
     193            ]
    185194        | _ ⇒ Wrong ???
    186195        ]
    187     | St_return eo
     196    | St_return eo n ⇒ λk.
    188197        match eo with
    189         [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
     198        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont ? k)〉
    190199        | Some e ⇒
    191200            ! 〈tr,v〉 ← eval_expr ge e en sp m;
    192             ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
    193         ]
    194     | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    195     | St_goto l ⇒
    196         ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k));
    197         ret ? 〈E0, State f s' en m sp k'〉
    198     | St_cost l s' ⇒
    199         ret ? 〈Echarge l, State f s' en m sp k〉
    200     ]
     201            ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont ? k)〉
     202        ]
     203    | St_label l n s' ⇒ λk. ret ? 〈E0, State f ? s' en m sp k〉
     204    | St_goto l n ⇒ λk.
     205        ! x ← opt_to_res … (find_label l ? (f_body f) (call_cont ? k));
     206        match x with [ dp n' x' ⇒ let 〈s', k'〉 ≝ x' in
     207          ret ? 〈E0, State f ? s' en m sp k'〉
     208        ]
     209    | St_cost l n s' ⇒ λk.
     210        ret ? 〈Echarge l, State f n s' en m sp k〉
     211    ]) k
    201212| Callstate fd args m k ⇒
    202213    match fd with
     
    204215        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    205216        ! en ← bind_params args (f_params f);
    206         ret ? 〈E0, State f (f_body f) en m' sp k〉
     217        ret ? 〈E0, State f O (f_body f) en m' sp k〉
    207218    | External fn ⇒
    208219        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     
    213224| Returnstate res m k ⇒
    214225    match k with
    215     [ Kcall dst f sp en k' ⇒
     226    [ Kcall dst f sp en n k' ⇒
    216227        ! en' ← match res with
    217228                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
     
    219230                                          | Some id ⇒ OK ? (add ?? en id v) ]
    220231                ];
    221         ret ? 〈E0, State f St_skip en' m sp k'〉
     232        ret ? 〈E0, State f n (St_skip ?) en' m sp k'〉
    222233    | _ ⇒ Wrong ???
    223234    ]
  • Deliverables/D3.3/Cminor-experiment/syntax.ma

    r754 r755  
    1212| Ecost : costlabel → expr → expr.
    1313
    14 inductive stmt : Type[0] ≝
    15 | St_skip : stmt
    16 | St_assign : ident → expr → stmt
    17 | St_store : memory_chunk → expr → expr → stmt
     14inductive Fin : nat → Type[0] ≝
     15| FO : ∀n. Fin (S n)
     16| FS : ∀n. Fin n → Fin (S n).
     17
     18inductive stmt : ∀blockdepth:nat. Type[0] ≝
     19| St_skip : ∀n. stmt n
     20| St_assign : ident → expr → ∀n. stmt n
     21| St_store : memory_chunk → expr → expr → ∀n. stmt n
    1822(* ident for returned value, expression to identify fn, args, signature. *)
    19 | St_call : option ident → expr → list expr → signature → stmt
    20 | St_tailcall : expr → list expr → signature → stmt
    21 | St_seq : stmt → stmt → stmt
    22 | St_ifthenelse : expr → stmt → stmt → stmt
    23 | St_loop : stmt → stmt
    24 | St_block : stmt → stmt
    25 | St_exit : nat → stmt
     23| St_call : option ident → expr → list expr → signature → ∀n. stmt n
     24| St_tailcall : expr → list expr → signature → ∀n. stmt n
     25| St_seq : ∀n. stmt n → stmt n → stmt n
     26| St_ifthenelse : expr → ∀n. stmt n → stmt n → stmt n
     27| St_loop : ∀n. stmt n → stmt n
     28| St_block : ∀n. stmt (S n) → stmt n
     29| St_exit : ∀n. Fin n → stmt n
    2630(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    27 | St_switch : expr → list (int × nat) → nat → stmt
    28 | St_return : option expr → stmt
    29 | St_label : ident → stmt → stmt
    30 | St_goto : ident → stmt
    31 | St_cost : costlabel → stmt → stmt.
     31| St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n
     32| St_return : option expr → ∀n. stmt n
     33| St_label : ident → ∀n. stmt n → stmt n
     34| St_goto : ident → ∀n. stmt n
     35| St_cost : costlabel → ∀n. stmt n → stmt n.
    3236
    3337record internal_function : Type[0] ≝
     
    3741; f_ptrs      : list ident
    3842; f_stacksize : nat
    39 ; f_body      : stmt
     43; f_body      : stmt O
    4044}.
    4145(* XXX: matita interpretations bug workaround *)
  • Deliverables/D3.3/Cminor-experiment/test/search.ma

    r751 r755  
    2525  [id_search_tab]
    2626  0 (
    27   St_cost C_cost8 (
    28   St_seq (
    29     St_assign id_search_low (Cst (Ointconst (repr 0)))
     27  St_cost C_cost8 ? (
     28  St_seq ? (
     29    St_assign id_search_low (Cst (Ointconst (repr 0))) ?
    3030  ) (
    31   St_seq (
    32     St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_size)) (Cst (Ointconst (repr 1))))
     31  St_seq ? (
     32    St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_size)) (Cst (Ointconst (repr 1)))) ?
    3333  ) (
    34   St_seq (
    35     St_seq (
    36       St_block (
    37         St_loop (
    38           St_seq (
    39             St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cge) (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low)))) (
    40               St_exit 0
     34  St_seq ? (
     35    St_seq ? (
     36      St_block ? (
     37        St_loop ? (
     38          St_seq ? (
     39            St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cge) (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low)))) ? (
     40              St_exit ? (FO ?)
    4141            ) (
    42               St_skip            )
     42              St_skip ?           )
    4343          ) (
    44           St_block (
    45             St_cost C_cost6 (
    46             St_seq (
    47               St_assign id_search_i (Op2 Odiv (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low))) (Cst (Ointconst (repr 2))))
     44          St_block ? (
     45            St_cost C_cost6 ? (
     46            St_seq ? (
     47              St_assign id_search_i (Op2 Odiv (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low))) (Cst (Ointconst (repr 2)))) ?
    4848            ) (
    49             St_seq (
    50               St_ifthenelse (Op2 (Ocmp Ceq) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
    51                 St_cost C_cost4 (
    52                 St_return (Some ? (Id id_search_i))
     49            St_seq ? (
     50              St_ifthenelse (Op2 (Ocmp Ceq) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? (
     51                St_cost C_cost4 ? (
     52                St_return (Some ? (Id id_search_i)) ?
    5353                )
    5454              ) (
    55                 St_cost C_cost5 (
    56                 St_skip                )
     55                St_cost C_cost5 ? (
     56                St_skip         ?       )
    5757              )
    5858            ) (
    59             St_seq (
    60               St_ifthenelse (Op2 (Ocmp Cgt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
    61                 St_cost C_cost2 (
    62                 St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1))))
     59            St_seq ? (
     60              St_ifthenelse (Op2 (Ocmp Cgt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? (
     61                St_cost C_cost2 ? (
     62                St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) ?
    6363                )
    6464              ) (
    65                 St_cost C_cost3 (
    66                 St_skip                )
     65                St_cost C_cost3 ? (
     66                St_skip         ?       )
    6767              )
    6868            ) (
    69             St_ifthenelse (Op2 (Ocmp Clt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
    70               St_cost C_cost0 (
    71               St_assign id_search_low (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1))))
     69            St_ifthenelse (Op2 (Ocmp Clt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? (
     70              St_cost C_cost0 ? (
     71              St_assign id_search_low (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) ?
    7272              )
    7373            ) (
    74               St_cost C_cost1 (
    75               St_skip              )
     74              St_cost C_cost1 ? (
     75              St_skip         ?     )
    7676            )
    7777            )
     
    8484      )
    8585    ) (
    86     St_cost C_cost7 (
    87     St_skip    )
     86    St_cost C_cost7 ? (
     87    St_skip  ?  )
    8888    )
    8989  ) (
    90   St_return (Some ? (Op1 Onegint (Cst (Ointconst (repr 1)))))
     90  St_return (Some ? (Op1 Onegint (Cst (Ointconst (repr 1))))) ?
    9191  )
    9292  )
     
    106106  []
    107107  5 (
    108   St_cost C_cost9 (
    109   St_seq (
    110     St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 0)))
     108  St_cost C_cost9 ? (
     109  St_seq ? (
     110    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 0))) ?
    111111  ) (
    112   St_seq (
    113     St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 1))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 18)))
     112  St_seq ? (
     113    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 1))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 18))) ?
    114114  ) (
    115   St_seq (
    116     St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 2))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 23)))
     115  St_seq ? (
     116    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 2))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 23))) ?
    117117  ) (
    118   St_seq (
    119     St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 3))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 57)))
     118  St_seq ? (
     119    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 3))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 57))) ?
    120120  ) (
    121   St_seq (
    122     St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 4))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 120)))
     121  St_seq ? (
     122    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 4))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 120))) ?
    123123  ) (
    124   St_seq (
    125     St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
     124  St_seq ? (
     125    St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) ?
    126126  ) (
    127   St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res)))
     127  St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res))) ?
    128128  )
    129129  )
Note: See TracChangeset for help on using the changeset viewer.