Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontEndOps.ml

    r2827 r2951  
    9999    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    100100    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    101 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13122 = function
    102 | Ointconst (sz, sg, x_13124) -> h_Ointconst sz sg x_13124
    103 | Oaddrsymbol (x_13126, x_13125) -> h_Oaddrsymbol x_13126 x_13125
    104 | Oaddrstack x_13127 -> h_Oaddrstack x_13127
     101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13161 = function
     102| Ointconst (sz, sg, x_13163) -> h_Ointconst sz sg x_13163
     103| Oaddrsymbol (x_13165, x_13164) -> h_Oaddrsymbol x_13165 x_13164
     104| Oaddrstack x_13166 -> h_Oaddrstack x_13166
    105105
    106106(** val constant_rect_Type5 :
    107107    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    108108    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    109 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13131 = function
    110 | Ointconst (sz, sg, x_13133) -> h_Ointconst sz sg x_13133
    111 | Oaddrsymbol (x_13135, x_13134) -> h_Oaddrsymbol x_13135 x_13134
    112 | Oaddrstack x_13136 -> h_Oaddrstack x_13136
     109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13170 = function
     110| Ointconst (sz, sg, x_13172) -> h_Ointconst sz sg x_13172
     111| Oaddrsymbol (x_13174, x_13173) -> h_Oaddrsymbol x_13174 x_13173
     112| Oaddrstack x_13175 -> h_Oaddrstack x_13175
    113113
    114114(** val constant_rect_Type3 :
    115115    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    116116    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    117 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13140 = function
    118 | Ointconst (sz, sg, x_13142) -> h_Ointconst sz sg x_13142
    119 | Oaddrsymbol (x_13144, x_13143) -> h_Oaddrsymbol x_13144 x_13143
    120 | Oaddrstack x_13145 -> h_Oaddrstack x_13145
     117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13179 = function
     118| Ointconst (sz, sg, x_13181) -> h_Ointconst sz sg x_13181
     119| Oaddrsymbol (x_13183, x_13182) -> h_Oaddrsymbol x_13183 x_13182
     120| Oaddrstack x_13184 -> h_Oaddrstack x_13184
    121121
    122122(** val constant_rect_Type2 :
    123123    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    124124    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    125 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13149 = function
    126 | Ointconst (sz, sg, x_13151) -> h_Ointconst sz sg x_13151
    127 | Oaddrsymbol (x_13153, x_13152) -> h_Oaddrsymbol x_13153 x_13152
    128 | Oaddrstack x_13154 -> h_Oaddrstack x_13154
     125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13188 = function
     126| Ointconst (sz, sg, x_13190) -> h_Ointconst sz sg x_13190
     127| Oaddrsymbol (x_13192, x_13191) -> h_Oaddrsymbol x_13192 x_13191
     128| Oaddrstack x_13193 -> h_Oaddrstack x_13193
    129129
    130130(** val constant_rect_Type1 :
    131131    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    132132    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    133 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13158 = function
    134 | Ointconst (sz, sg, x_13160) -> h_Ointconst sz sg x_13160
    135 | Oaddrsymbol (x_13162, x_13161) -> h_Oaddrsymbol x_13162 x_13161
    136 | Oaddrstack x_13163 -> h_Oaddrstack x_13163
     133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13197 = function
     134| Ointconst (sz, sg, x_13199) -> h_Ointconst sz sg x_13199
     135| Oaddrsymbol (x_13201, x_13200) -> h_Oaddrsymbol x_13201 x_13200
     136| Oaddrstack x_13202 -> h_Oaddrstack x_13202
    137137
    138138(** val constant_rect_Type0 :
    139139    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    140140    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    141 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13167 = function
    142 | Ointconst (sz, sg, x_13169) -> h_Ointconst sz sg x_13169
    143 | Oaddrsymbol (x_13171, x_13170) -> h_Oaddrsymbol x_13171 x_13170
    144 | Oaddrstack x_13172 -> h_Oaddrstack x_13172
     141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13206 = function
     142| Ointconst (sz, sg, x_13208) -> h_Ointconst sz sg x_13208
     143| Oaddrsymbol (x_13210, x_13209) -> h_Oaddrsymbol x_13210 x_13209
     144| Oaddrstack x_13211 -> h_Oaddrstack x_13211
    145145
    146146(** val constant_inv_rect_Type4 :
     
    211211    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    212212    unary_operation -> 'a1 **)
    213 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13242 x_13241 = function
     213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13281 x_13280 = function
    214214| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    215215| Onegint (sz, sg) -> h_Onegint sz sg
     
    227227    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    228228    unary_operation -> 'a1 **)
    229 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13253 x_13252 = function
     229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13292 x_13291 = function
    230230| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    231231| Onegint (sz, sg) -> h_Onegint sz sg
     
    243243    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    244244    unary_operation -> 'a1 **)
    245 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13264 x_13263 = function
     245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13303 x_13302 = function
    246246| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    247247| Onegint (sz, sg) -> h_Onegint sz sg
     
    259259    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    260260    unary_operation -> 'a1 **)
    261 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13275 x_13274 = function
     261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13314 x_13313 = function
    262262| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    263263| Onegint (sz, sg) -> h_Onegint sz sg
     
    275275    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    276276    unary_operation -> 'a1 **)
    277 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13286 x_13285 = function
     277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13325 x_13324 = function
    278278| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    279279| Onegint (sz, sg) -> h_Onegint sz sg
     
    291291    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    292292    unary_operation -> 'a1 **)
    293 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13297 x_13296 = function
     293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13336 x_13335 = function
    294294| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    295295| Onegint (sz, sg) -> h_Onegint sz sg
     
    426426    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    427427    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    428 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13402 x_13401 x_13400 = function
     428let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13441 x_13440 x_13439 = function
    429429| Oadd (sz, sg) -> h_Oadd sz sg
    430430| Osub (sz, sg) -> h_Osub sz sg
     
    440440| Oshr (sz, sg) -> h_Oshr sz sg
    441441| Oshru (sz, sg) -> h_Oshru sz sg
    442 | Ocmp (sz, sg, sg', x_13404) -> h_Ocmp sz sg sg' x_13404
    443 | Ocmpu (sz, sg', x_13405) -> h_Ocmpu sz sg' x_13405
     442| Ocmp (sz, sg, sg', x_13443) -> h_Ocmp sz sg sg' x_13443
     443| Ocmpu (sz, sg', x_13444) -> h_Ocmpu sz sg' x_13444
    444444| Oaddpi sz -> h_Oaddpi sz
    445445| Oaddip sz -> h_Oaddip sz
    446446| Osubpi sz -> h_Osubpi sz
    447447| Osubpp sz -> h_Osubpp sz
    448 | Ocmpp (sg', x_13406) -> h_Ocmpp sg' x_13406
     448| Ocmpp (sg', x_13445) -> h_Ocmpp sg' x_13445
    449449
    450450(** val binary_operation_rect_Type5 :
     
    461461    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    462462    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    463 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13429 x_13428 x_13427 = function
     463let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13468 x_13467 x_13466 = function
    464464| Oadd (sz, sg) -> h_Oadd sz sg
    465465| Osub (sz, sg) -> h_Osub sz sg
     
    475475| Oshr (sz, sg) -> h_Oshr sz sg
    476476| Oshru (sz, sg) -> h_Oshru sz sg
    477 | Ocmp (sz, sg, sg', x_13431) -> h_Ocmp sz sg sg' x_13431
    478 | Ocmpu (sz, sg', x_13432) -> h_Ocmpu sz sg' x_13432
     477| Ocmp (sz, sg, sg', x_13470) -> h_Ocmp sz sg sg' x_13470
     478| Ocmpu (sz, sg', x_13471) -> h_Ocmpu sz sg' x_13471
    479479| Oaddpi sz -> h_Oaddpi sz
    480480| Oaddip sz -> h_Oaddip sz
    481481| Osubpi sz -> h_Osubpi sz
    482482| Osubpp sz -> h_Osubpp sz
    483 | Ocmpp (sg', x_13433) -> h_Ocmpp sg' x_13433
     483| Ocmpp (sg', x_13472) -> h_Ocmpp sg' x_13472
    484484
    485485(** val binary_operation_rect_Type3 :
     
    496496    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    497497    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    498 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13456 x_13455 x_13454 = function
     498let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13495 x_13494 x_13493 = function
    499499| Oadd (sz, sg) -> h_Oadd sz sg
    500500| Osub (sz, sg) -> h_Osub sz sg
     
    510510| Oshr (sz, sg) -> h_Oshr sz sg
    511511| Oshru (sz, sg) -> h_Oshru sz sg
    512 | Ocmp (sz, sg, sg', x_13458) -> h_Ocmp sz sg sg' x_13458
    513 | Ocmpu (sz, sg', x_13459) -> h_Ocmpu sz sg' x_13459
     512| Ocmp (sz, sg, sg', x_13497) -> h_Ocmp sz sg sg' x_13497
     513| Ocmpu (sz, sg', x_13498) -> h_Ocmpu sz sg' x_13498
    514514| Oaddpi sz -> h_Oaddpi sz
    515515| Oaddip sz -> h_Oaddip sz
    516516| Osubpi sz -> h_Osubpi sz
    517517| Osubpp sz -> h_Osubpp sz
    518 | Ocmpp (sg', x_13460) -> h_Ocmpp sg' x_13460
     518| Ocmpp (sg', x_13499) -> h_Ocmpp sg' x_13499
    519519
    520520(** val binary_operation_rect_Type2 :
     
    531531    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    532532    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    533 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13483 x_13482 x_13481 = function
     533let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13522 x_13521 x_13520 = function
    534534| Oadd (sz, sg) -> h_Oadd sz sg
    535535| Osub (sz, sg) -> h_Osub sz sg
     
    545545| Oshr (sz, sg) -> h_Oshr sz sg
    546546| Oshru (sz, sg) -> h_Oshru sz sg
    547 | Ocmp (sz, sg, sg', x_13485) -> h_Ocmp sz sg sg' x_13485
    548 | Ocmpu (sz, sg', x_13486) -> h_Ocmpu sz sg' x_13486
     547| Ocmp (sz, sg, sg', x_13524) -> h_Ocmp sz sg sg' x_13524
     548| Ocmpu (sz, sg', x_13525) -> h_Ocmpu sz sg' x_13525
    549549| Oaddpi sz -> h_Oaddpi sz
    550550| Oaddip sz -> h_Oaddip sz
    551551| Osubpi sz -> h_Osubpi sz
    552552| Osubpp sz -> h_Osubpp sz
    553 | Ocmpp (sg', x_13487) -> h_Ocmpp sg' x_13487
     553| Ocmpp (sg', x_13526) -> h_Ocmpp sg' x_13526
    554554
    555555(** val binary_operation_rect_Type1 :
     
    566566    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    567567    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    568 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13510 x_13509 x_13508 = function
     568let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13549 x_13548 x_13547 = function
    569569| Oadd (sz, sg) -> h_Oadd sz sg
    570570| Osub (sz, sg) -> h_Osub sz sg
     
    580580| Oshr (sz, sg) -> h_Oshr sz sg
    581581| Oshru (sz, sg) -> h_Oshru sz sg
    582 | Ocmp (sz, sg, sg', x_13512) -> h_Ocmp sz sg sg' x_13512
    583 | Ocmpu (sz, sg', x_13513) -> h_Ocmpu sz sg' x_13513
     582| Ocmp (sz, sg, sg', x_13551) -> h_Ocmp sz sg sg' x_13551
     583| Ocmpu (sz, sg', x_13552) -> h_Ocmpu sz sg' x_13552
    584584| Oaddpi sz -> h_Oaddpi sz
    585585| Oaddip sz -> h_Oaddip sz
    586586| Osubpi sz -> h_Osubpi sz
    587587| Osubpp sz -> h_Osubpp sz
    588 | Ocmpp (sg', x_13514) -> h_Ocmpp sg' x_13514
     588| Ocmpp (sg', x_13553) -> h_Ocmpp sg' x_13553
    589589
    590590(** val binary_operation_rect_Type0 :
     
    601601    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    602602    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    603 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13537 x_13536 x_13535 = function
     603let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13576 x_13575 x_13574 = function
    604604| Oadd (sz, sg) -> h_Oadd sz sg
    605605| Osub (sz, sg) -> h_Osub sz sg
     
    615615| Oshr (sz, sg) -> h_Oshr sz sg
    616616| Oshru (sz, sg) -> h_Oshru sz sg
    617 | Ocmp (sz, sg, sg', x_13539) -> h_Ocmp sz sg sg' x_13539
    618 | Ocmpu (sz, sg', x_13540) -> h_Ocmpu sz sg' x_13540
     617| Ocmp (sz, sg, sg', x_13578) -> h_Ocmp sz sg sg' x_13578
     618| Ocmpu (sz, sg', x_13579) -> h_Ocmpu sz sg' x_13579
    619619| Oaddpi sz -> h_Oaddpi sz
    620620| Oaddip sz -> h_Oaddip sz
    621621| Osubpi sz -> h_Osubpi sz
    622622| Osubpp sz -> h_Osubpp sz
    623 | Ocmpp (sg', x_13541) -> h_Ocmpp sg' x_13541
     623| Ocmpp (sg', x_13580) -> h_Ocmpp sg' x_13580
    624624
    625625(** val binary_operation_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.