Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file cst.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502(****************************************************************************)(* *)(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)(* *)(* Copyright (C) 2017-2019 The MOPSA Project. *)(* *)(* This program is free software: you can redistribute it and/or modify *)(* it under the terms of the GNU Lesser General Public License as published *)(* by the Free Software Foundation, either version 3 of the License, or *)(* (at your option) any later version. *)(* *)(* This program is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* You should have received a copy of the GNU Lesser General Public License *)(* along with this program. If not, see <http://www.gnu.org/licenses/>. *)(* *)(****************************************************************************)(** Concrete syntax tree for C stubs *)openMopsa_utilsopenMopsa_c_parseropenLocationtypestub=sectionlistwith_range(** {2 Stub sections} *)(** ***************** *)andsection=|S_caseofcasewith_range|S_leafofleafandleaf=|S_localoflocalwith_range|S_assumesofassumeswith_range|S_requiresofrequireswith_range|S_assignsofassignswith_range|S_ensuresofensureswith_range|S_freeoffreewith_range|S_messageofmessagewith_rangeandcase={case_label:string;case_body:leaflist;}(** {2 Stub leaf sections} *)(** ********************** *)andrequires=formulawith_rangeandensures=formulawith_rangeandassumes=formulawith_rangeandlocal={lvar:var;ltyp:c_qual_typ;lval:local_value;}andlocal_value=|L_newofresource|L_callofvarwith_range(** function *)*exprwith_rangelist(* arguments *)andassigns={assign_target:exprwith_range;assign_offset:intervallist;}andfree=exprwith_rangeandmessage={message_kind:message_kind;message_body:string;}andmessage_kind=|WARN|UNSOUND(** {2 Formulas} *)(** ************ *)andformula=|F_exprofexprwith_range|F_boolofbool|F_binopoflog_binop*formulawith_range*formulawith_range|F_notofformulawith_range|F_forallofvar*c_qual_typ*set*formulawith_range|F_existsofvar*c_qual_typ*set*formulawith_range|F_inofexprwith_range*set|F_otherwiseofformulawith_range*exprwith_range|F_ifofformulawith_range*formulawith_range*formulawith_range(** {2 Expressions} *)(** *************** *)andexpr=|E_topofc_qual_typ|E_intofZ.t*int_suffix|E_floatoffloat|E_stringofstring|E_charofint|E_invalid|E_varofvar|E_unopofunop*exprwith_range|E_binopofbinop*exprwith_range*exprwith_range|E_addr_ofofexprwith_range|E_derefofexprwith_range|E_castofc_qual_typ*exprwith_range|E_subscriptofexprwith_range*exprwith_range|E_memberofexprwith_range*string|E_arrowofexprwith_range*string|E_conditionalofexprwith_range*exprwith_range*exprwith_range|E_builtin_callofbuiltin*exprwith_rangelist|E_raiseofstring|E_sizeof_typeofc_qual_typwith_range|E_sizeof_exprofexprwith_range|E_returnandint_suffix=|NO_SUFFIX|LONG|UNSIGNED_LONG|LONG_LONG|UNSIGNED_LONG_LONGandlog_binop=|AND|OR|IMPLIESandbinop=|ADD(* + *)|SUB(* - *)|MUL(* * *)|DIV(* / *)|MOD(* % *)|RSHIFT(* >> *)|LSHIFT(* << *)|LOR(* || *)|LAND(* && *)|LT(* < *)|LE(* <= *)|GT(* > *)|GE(* >= *)|EQ(* == *)|NEQ(* != *)|BOR(* | *)|BAND(* & *)|BXOR(* ^ *)andunop=|PLUS(* + *)|MINUS(* - *)|LNOT(* ! *)|BNOT(* ~ *)andset=|S_intervalofinterval|S_resourceofresourceandinterval={itv_lb:exprwith_range;(** lower bound *)itv_open_lb:bool;(** open lower bound *)itv_ub:exprwith_range;(** upper bound *)itv_open_ub:bool;(** open upper bound *)}andresource=varandvar={vname:string;(** variable name *)vlocal:bool;(** is it a local variable ? *)vuid:int;(** unique identifier *)vtyp:c_qual_typ;(** variable type *)vrange:range;(** declaration location *)}andbuiltin=|PRIMED|LENGTH|INDEX|BYTES|OFFSET|BASE|VALID_FLOAT|FLOAT_INF|FLOAT_NAN|ALIVE|RESOURCE(** {2 Types} *)(* ********* *)andc_qual_typ=c_typ*c_qualandc_typ=|T_void|T_char|T_signed_char|T_unsigned_char|T_signed_short|T_unsigned_short|T_signed_int|T_unsigned_int|T_signed_long|T_unsigned_long|T_signed_long_long|T_unsigned_long_long|T_signed_int128|T_unsigned_int128|T_float|T_double|T_long_double|T_float128|T_arrayofc_qual_typ*array_length|T_structofvar|T_unionofvar|T_typedefofvar|T_pointerofc_qual_typ|T_enumofvar|T_unknownandc_qual={c_qual_const:bool;c_qual_volatile:bool;c_qual_restrict:bool;}andarray_length=|A_no_length|A_constant_lengthofZ.t(** {2 Utility functions} *)(** ********************* *)(* fixed by MOPSA's frontend with the real target *)lettarget_info=ref(Clang_parser.get_target_info(Clang_parser.get_default_target_options()))letcompare_varv1v2=Compare.compose[(fun()->comparev1.vnamev2.vname);(fun()->comparev1.vuidv2.vuid);]letcompare_resource(r1:resource)(r2:resource)=comparer1r2letno_c_qual={c_qual_const=false;c_qual_volatile=false;c_qual_restrict=false;}letconst={no_c_qualwithc_qual_const=true;}letvolatile={no_c_qualwithc_qual_volatile=true;}letrestrict={no_c_qualwithc_qual_restrict=true;}letis_c_qual_non_emptyq=q.c_qual_const||q.c_qual_restrict||q.c_qual_volatileletmerge_c_qualq1q2={c_qual_const=q1.c_qual_const||q2.c_qual_const;c_qual_volatile=q1.c_qual_volatile||q2.c_qual_volatile;c_qual_restrict=q1.c_qual_restrict||q2.c_qual_restrict;}(** {2 Pretty printers} *)(** ******************* *)openFormatletpp_varfmtv=pp_print_stringfmtv.vnameletpp_resourcefmtresource=pp_varfmtresourceletpp_builtinfmtf=matchfwith|BYTES->pp_print_stringfmt"bytes"|LENGTH->pp_print_stringfmt"length"|OFFSET->pp_print_stringfmt"offset"|INDEX->pp_print_stringfmt"index"|BASE->pp_print_stringfmt"base"|PRIMED->pp_print_stringfmt"primed"|VALID_FLOAT->pp_print_stringfmt"valid_float"|FLOAT_INF->pp_print_stringfmt"float_inf"|FLOAT_NAN->pp_print_stringfmt"float_nan"|ALIVE->pp_print_stringfmt"alive"|RESOURCE->pp_print_stringfmt"resource"letpp_listppsepfmtl=pp_print_list~pp_sep:(funfmt()->fprintffmtsep)ppfmtlletrecpp_exprfmtexp=matchget_contentexpwith|E_top(t)->fprintffmt"⊤(%a)"pp_c_qual_typt|E_int(n,suffix)->fprintffmt"%a%a"Z.pp_printnpp_int_suffixsuffix|E_floatf->pp_print_floatfmtf|E_strings->fprintffmt"\"%s\""s|E_charc->ifc>=32&&c<127thenfprintffmt"'%c'"(Char.chrc)elsefprintffmt"%d"c|E_invalid->fprintffmt"INVALID"|E_varv->pp_varfmtv|E_unop(op,e)->fprintffmt"%a %a"pp_unopoppp_expre|E_binop(op,e1,e2)->fprintffmt"%a %a %a"pp_expre1pp_binopoppp_expre2|E_addr_ofe->fprintffmt"&%a"pp_expre|E_derefe->fprintffmt"*%a"pp_expre|E_cast(t,e)->fprintffmt"(%a) %a"pp_c_qual_typtpp_expre|E_subscript(a,i)->fprintffmt"%a[%a]"pp_exprapp_expri|E_member(s,f)->fprintffmt"%a.%s"pp_exprsf|E_arrow(p,f)->fprintffmt"%a->%s"pp_exprpf|E_conditional(c,e1,e2)->fprintffmt"%a?%a:%a"pp_exprcpp_expre1pp_expre2|E_builtin_call(f,args)->fprintffmt"%a(%a)"pp_builtinf(pp_listpp_expr", ")args|E_sizeof_typet->fprintffmt"sizeof(%a)"pp_c_qual_typt.content|E_sizeof_expre->fprintffmt"sizeof(%a)"pp_expre|E_return->pp_print_stringfmt"return"|E_raisemsg->fprintffmt"raise(\"%s\")"msgandpp_int_suffixfmt=function|NO_SUFFIX->()|LONG->fprintffmt"L"|UNSIGNED_LONG->fprintffmt"UL"|LONG_LONG->fprintffmt"LL"|UNSIGNED_LONG_LONG->fprintffmt"ULL"andpp_unopfmt=function|PLUS->pp_print_stringfmt"+"|MINUS->pp_print_stringfmt"-"|LNOT->pp_print_stringfmt"!"|BNOT->pp_print_stringfmt"~"andpp_binopfmt=function|ADD->pp_print_stringfmt"+"|SUB->pp_print_stringfmt"-"|MUL->pp_print_stringfmt"*"|DIV->pp_print_stringfmt"/"|MOD->pp_print_stringfmt"%"|RSHIFT->pp_print_stringfmt">>"|LSHIFT->pp_print_stringfmt"<<"|LOR->pp_print_stringfmt"||"|LAND->pp_print_stringfmt"&&"|LT->pp_print_stringfmt"<"|LE->pp_print_stringfmt"<="|GT->pp_print_stringfmt">"|GE->pp_print_stringfmt">="|EQ->pp_print_stringfmt"=="|NEQ->pp_print_stringfmt"!="|BOR->pp_print_stringfmt"|"|BAND->pp_print_stringfmt"&"|BXOR->pp_print_stringfmt"^"andpp_c_qual_typfmt=function|(t,qual)whenis_c_qual_non_emptyqual->fprintffmt"%a %a"pp_c_qualqualpp_c_typt|(t,qual)->pp_c_typfmttandpp_c_qualfmtq=letl=(ifq.c_qual_constthen["const"]else[])@(ifq.c_qual_volatilethen["volatile"]else[])@(ifq.c_qual_restrictthen["restrict"]else[])inFormat.pp_print_list~pp_sep:(funfmt()->Format.pp_print_stringfmt" ")Format.pp_print_stringfmtlandpp_c_typfmt=function|T_void->pp_print_stringfmt"void"|T_char->pp_print_stringfmt"char"|T_signed_char->pp_print_stringfmt"signed char"|T_unsigned_char->pp_print_stringfmt"unsigned char"|T_signed_short->pp_print_stringfmt"signed short"|T_unsigned_short->pp_print_stringfmt"unsigned short"|T_signed_int->pp_print_stringfmt"signed int"|T_unsigned_int->pp_print_stringfmt"unsigned int"|T_signed_long->pp_print_stringfmt"signed long"|T_unsigned_long->pp_print_stringfmt"unsigned long"|T_signed_long_long->pp_print_stringfmt"signed long long"|T_unsigned_long_long->pp_print_stringfmt"unsigned long long"|T_signed_int128->pp_print_stringfmt"signed int128"|T_unsigned_int128->pp_print_stringfmt"unsigned int128"|T_float->pp_print_stringfmt"float"|T_double->pp_print_stringfmt"double"|T_long_double->pp_print_stringfmt"long double"|T_float128->pp_print_stringfmt"__float128"|T_array(t,A_no_length)->fprintffmt"%a[]"pp_c_qual_typt|T_array(t,A_constant_lengthlen)->fprintffmt"%a[%a]"pp_c_qual_typtZ.pp_printlen|T_struct(s)->fprintffmt"struct %a"pp_vars|T_union(u)->fprintffmt"union %a"pp_varu|T_typedef(t)->pp_varfmtt|T_pointer(t)->fprintffmt"%a *"pp_c_qual_typt|T_enum(e)->fprintffmt"enum %a"pp_vare|T_unknown->fprintffmt"?"letrecpp_formulafmt(f:formulawith_range)=matchget_contentfwith|F_expre->pp_exprfmte|F_booltrue->pp_print_stringfmt"true"|F_boolfalse->pp_print_stringfmt"false"|F_binop(op,f1,f2)->fprintffmt"(%a)@\n%a (%a)"pp_formulaf1pp_log_binopoppp_formulaf2|F_notf->fprintffmt"not (%a)"pp_formulaf|F_forall(x,t,set,f)->fprintffmt"∀ %a %a ∈ %a: @[%a@]"pp_c_qual_typtpp_varxpp_setsetpp_formulaf|F_exists(x,t,set,f)->fprintffmt"∃ %a %a ∈ %a: @[%a@]"pp_c_qual_typtpp_varxpp_setsetpp_formulaf|F_in(x,set)->fprintffmt"%a ∈ %a"pp_exprxpp_setset|F_otherwise(f,e)->fprintffmt"%a otherwise %a"pp_formulafpp_expre|F_if(c,f1,f2)->fprintffmt"if %a then %a else %a end"pp_formulacpp_formulaf1pp_formulaf2andpp_log_binopfmt=function|AND->pp_print_stringfmt"and"|OR->pp_print_stringfmt"or"|IMPLIES->pp_print_stringfmt"implies"andpp_setfmt=function|S_interval(itv)->pp_intervalfmtitv|S_resource(r)->pp_resourcefmtrandpp_intervalfmti=fprintffmt"%s%a, %a%s"(ifi.itv_open_lbthen"]"else"[")pp_expri.itv_lbpp_expri.itv_ub(ifi.itv_open_ubthen"["else"]")letpp_optppfmto=matchowith|None->()|Somex->ppfmtxletrecpp_localfmtlocal=letlocal=get_contentlocalinfprintffmt"local : %a %a = @[%a@];"pp_c_qual_typlocal.ltyppp_varlocal.lvarpp_local_valuelocal.lvalandpp_local_valuefmtv=matchvwith|L_newresource->fprintffmt"new %a"pp_resourceresource|L_call(f,args)->fprintffmt"%a(%a)"pp_varf.content(pp_listpp_expr", ")argsletpp_requiresfmtrequires=fprintffmt"requires : @[%a@];"pp_formularequires.contentletpp_assignsfmtassigns=fprintffmt"assigns : %a%a;"pp_exprassigns.content.assign_target(pp_print_list~pp_sep:(funfmt()->())pp_interval)assigns.content.assign_offsetletpp_assumesfmt(assumes:assumeswith_range)=fprintffmt"assumes : @[%a@];"pp_formulaassumes.contentletpp_ensuresfmtensures=fprintffmt"ensures : @[%a@];"pp_formulaensures.contentletpp_freefmtfree=fprintffmt"free : %a;"pp_exprfree.contentletpp_messagefmtmsg=matchmsg.content.message_kindwith|WARN->fprintffmt"warn: \"%s\";"msg.content.message_body|UNSOUND->fprintffmt"unsound: \"%s\";"msg.content.message_bodyletpp_leaffmtsec=matchsecwith|S_locallocal->pp_localfmtlocal|S_assumesassumes->pp_assumesfmtassumes|S_requiresrequires->pp_requiresfmtrequires|S_assignsassigns->pp_assignsfmtassigns|S_ensuresensures->pp_ensuresfmtensures|S_freefree->pp_freefmtfree|S_messagemsg->pp_messagefmtmsgletpp_casefmtcase=fprintffmt"case \"%s\":@\n @[<v 2>%a@]"case.case_label(pp_listpp_leaf"@\n")case.case_bodyletpp_sectionfmtsec=matchsecwith|S_leafleaf->pp_leaffmtleaf|S_casecase->pp_casefmtcase.contentletpp_sectionsfmtsecs=pp_print_list~pp_sep:(funfmt()->fprintffmt"@\n")pp_sectionfmtsecsletpp_stubfmtstub=pp_sectionsfmtstub.content