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:
2 added
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • 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.