Types:Abstract-DomainSelectionBasedonVariableUsage SvenApel1,DirkBeyer1,KarlheinzFriedberger1,FrancoRaimondi2,andAlexandervonRhein1 1UniversityofPassau,Germany2MiddlesexUniversity,London,UK Abstract.Theessofsoftwaremodelcheckingdependsonfindinganappropriateabstractionoftheprogramtoverify.Thechoiceoftheabstractdomainandtheanalysisconfigurationiscurrentlylefttotheuser,whomaynotbefamiliarwiththetradeoffsandperformancedetailsoftheavailableabstractdomains.Weintroducetheconceptofdomaintypes,whichclassifytheprogramvariablesintotypesthataremorefine-grainedthanstandarddeclaredtypes(e.g.,‘int’and‘long’)toguidetheselectionofanappropriateabstractdomainforamodelchecker.Ourimplementationofanexistingverificationframeworkdeterminesthedomaintypeforeachvariableinapre-analysisstep,basedontheusageofvariablesintheprogram,andthenassignseachvariabletoanabstractdomain.Basedonaseriesofexperimentsonprehensivesetofverificationtasksfrominternationalverifipetitions,wedemonstratethatthechoiceoftheabstractdomainpervariable(weconsideroneexplicitandonesymbolicdomain)cansubstantiallyimprovetheverificationintermsofperformanceandprecision. 1Introduction Oneofthemainchallengesinsoftwaremodelcheckingistoautomaticallyselect,foreachprogramvariable,anabstractrepresentation(alsoknownasabstractdomain)thatallowstoeffectivelyprovetheprogramcorrectortoidentifyanerrorpath.Severalabstractdomainshavebeenappliedessfullytosoftware-verificationproblems,withdifferentstrengthsandweaknesses.Abstractdomainscanbebasedonexplicitrepresentations(e.g.,hashtablesforintegers,memorygraphsfortheheap)andsymbolicrepresentations(predicates,binarydecisiondiagrams(BDD)).Forexample,usinganaluedomain[14]wasefficientonmanybenchmarksfromthepetitiononsoftwareverification[9],whileusingaBDDdomain[15]wasmoreefficientoneventcondition-action(ECA)systemsthatinvolveonlysimpleoperationsoverintegersinanpetition[30].Inthecontextofproduct-lineverification,ithasbeenshownthatBDD-encodingsoffeaturevariablesimproveverificationperformance[5,24].Thekeyinsightisthatdifferentabstractdomainsareessfulondifferentprograms,andforeveryabstractdomain,wecanfindprogramsforwhichtheabstractdomainisnotessful. ApreliminaryversionwaspublishedasTechnicalReportMIP-1303inMay2013[3]. V.oandA.Legay(Eds.):HVC2013,LNCS8244,pp.262–278,2013.cSpringerInternationalPublishingSwitzerland2013 DomainTypes:Abstract-DomainSelectionBasedonVariableUsage263 Sofar,thechoiceoftheabstractdomainforagivenverificationproblem(whichoftenimpliesthechoiceofacertainverificationtoolaswell)waslefttotheuser.Ourgoalistoautomatethechoiceofaneffectiveabstractdomain.Weanalyzetheusageofprogramvariablesbeforethemodelcheckerstartsthestate-spaceexplorationandassigneachvariabletoacertaindomaintype.Inadditiontothedeclaredtypeofavariable(e.g.,intandchar),thedomaintyperepresentsinformationaboutthevaluerangeandtheoperationsinwhichthevariableisinvolved. OurapproachisbasedontheCPAverificationframework,inwhicheachabstractdomainhasaprecisionassociatedwithit[11].Weusethedomaintypesfromthepreanalysisasguidanceforassigninganabstractdomaintoeachvariable.Intheexperimentsthatweconductedtoevaluateourapproach,weusetwoabstractdomains:anexplicit-valuedomainandaBDD-baseddomain.Forbothdomains,theprecisionisasetofvariablesthatshouldbetrackedinthedomain.Theprecisionsareinitializedbasedonthevariables’domaintypes.Thedomainassignmentimprovestheoverallverificationperformance,ifeachabstractdomaintracksthekindofvariablesthatitissuitedfor. TheanalysisisimplementedintheverificationframeworkCPACHECKER[13],whichimplementsconfigurableprogramanalysisforCprogramsandprovidesabstractdomainsforanexplicit-valueanalysisandaBDD-basedanalysis(wedonotusethepredicateanalysis).Weevaluateourapproachonsixsetsofverificationtasksfromdifferentapplicationdomains(atotalof2435files)thathavebeenusedbyrecentpetitionsonsoftwaremodelchecking(SV-COMP2013[9],RERSChallenge2012[30]). Ourevaluationrevealsthattheprogramsinthebenchmarksetscontainasignificantnumberofvariablesthathaveamuchnarrowerdomaintypethanthedeclaredtypeofthevariable.Wealsodemonstratethattheverificationperformanceimprovesifthesevariablesaretrackedusingamoresuitableabstractdomain,paredtousingasingleabstractdomainforallvariables.Allresultsareavailableonthesupplementarywebsite1. Example.WeillustrateourapproachontheexampleprograminFig.1.Theprogramcontainsthreevariablesthataredeclaredbytheprogrammerasint.Thevariablesareusedindifferentways:thevariableenabledisusedasaboolean;thevariablesaandbarenumericandusedinaparison,bisalsousedinamultiplication.NeitherthealueanalysisnortheBDD-basedanalysisisableto intenabled,a,b;b=20;if(enabled){ if(a>5){if(a==0){b=0;}assert(b∗b>200); }} efficientlyverifysuchaprogram:Theexplicit-valueFig.1.Examplewithintvariables domainisperfectlysuitedtohandlevariableb,be-ofdifferentdomaintypes causebhasaconcretevalue,andthemultiplication andtheparisoncaneasilyputed;BDDsareknowntobeineffi- cientformultiplication[31].TheBDDdomaincanefficientlyencodethevariablesen- abledanda,whereastheexplicit-valueanalysisisnotgoodatencodingfactslikea>
5. 1/projects/domaintypes/ 264S.Apeletal. Thus,withoutinformationaboutvariablea,theexplicit-valueanalysisdoesnotknowthevalueofvariablebandcannotdeterminetheresultofthemultiplication. Ithasbeenproposedtouseseveralabstractdomainsinparallel,witheachdomainhandlingallvariables(e.g.[17]).Ifthedomainsaremunicating(reducedproduct),thiscouldsolvetheverificationtask,buttheloadoneachdomainwouldbeunnecessarilyhigh,becauseeverydomainhastohandlemorevariablesthannecessary. Contributions.Wemakethefollowingcontributions:–Weintroducedtheconceptofdomaintypesanddevelopedapre-analysisputesthedomaintypesforallprogramvariables.–Weextendedanexistingverificationframeworktousethetwoabstractdomains‘explicit-value’and‘BDD’inparallel,whilecontrollingtheprecisionofeachabstractdomain(thevariablestotrack)separately,basedondomaintypes.–Weevaluateourapproachonverificationbenchmarksfromrecentinternationalsoftware-verifipetitions. 2Background Weinformallyexplaintheconceptsthatweuse,andprovidereferencestotheliteraturefordetails.Ascontext,weassumetoverifyCprogramswithintegervariables. AbstractDomainsandProgramAnalysis.Abstraction-basedsoftwaremodelcheckersautomaticallyextractanabstractmodelofthesubjectprogramandexplorethismodelusingoneormoreabstractdomains.Anabstractdomainrepresentscertainaspectsoftheconcreteprogram’sstatesthatthestateexplorationissupposedtotrack[1].Differentabstractdomainscantrackdifferentaspectsoftheprogramstatespaceplementeachother.Forexample,ashapedomain[12,26,34]stores,foreachtrackedpointer,theshapeofthepointed-todatastructuresontheheap.Anotherexampleistheexplicit-valuedomainthat,foreachtrackedvariable,trackstheexplicitvalueofthevariable[14,28,29].Thesetwoexamplesillustratethatabstractdomainscanrepresentdifferentinformation.However,itisalsopossibletousedifferentabstractdomainstorepresentthesameinformationindifferentways.Consideraprograminwhichthevalueofvariablexrangesfrom3to9.Thiscanbestoredbyanintervaldomain[17]usingtheabstractstatex→[3,9],orbyapredicatedomain[7,10,27]usingtheabstractstatex≥3∧x≤
9. Everyabstractdomainconsistsof(1)arepresentationofsetsofconcretestates,definingtheabstractstates(latticeelements),(2)anoperatortodecideifoneabstractstatesubsumesanotherabstractstate(partialorder),and(3)anoperatorbinestwoabstractstatesintoanewabstractstatethatrepresentsboth(join).Softwareverifiersuseoneorseveralabstractdomainstorepresentthestatesoftheprogram.Thecharacteristicsoftheabstractdomainhaveimplicationsontheeffectivity(lownumberoffailuresandfalseresults)andefficiency(performance)oftheprogramanalysis. Precision.Eachabstractdomaincanoperateatdifferentlevelsofabstraction(i.e.,itcanbemorefine-grainedormorecoarse-grained).Thelevelofabstractionofanabstractdomainisdeterminedbytheabstractionprecision,whichcontrolsiftheanalysisiscoarseorfine.Forexample,theprecisionoftheshapedomaincouldinstructtheanalysiswhichpointerstotrackandhowlargeashapecanmaximallygrow;theprecisionofthe DomainTypes:Abstract-DomainSelectionBasedonVariableUsage265 1intx,y,z;2x=5;3if(y>1){4z=2;5}else{6z=2∗x/5;7}8...
     

  
 
 
 
 Fig.2.Exampleprogram(left),control-flowautomaton(CFA)thatrepresentstheprogram(middle),andabstractreachabilitygraph(ARG,right)fortheexplicit-valuedomain.CFAedgesmodelassumeoperations(e.g.,[y>1])andassignmentoperations(e.g.,z=2;). predicatedomainisasetofpredicatestotrackthatcan,forexample,growbyaddingpredicatesduringrefinementsteps[23]. Next,wedescribethetwoabstractdomainsthatweconsiderinourexperiments. Explicit-ValueDomain.Theexplicit-valuedomainstoresexplicitvaluesforprogramvariables.Eachabstractstateofthisabstractdomainisamapthatassignstoeachprogramvariablethatursintheprecision,anintegervalue(ornovalueifanexplicitvaluecannotbedetermined).Forexample,considerthecode,thecontrol-flowautomaton(CFA),andtheabstractreachabilitygraph(ARG)inFig.2:theassignmentofvalue5tovariablexisstoredinanabstractstateforCFAnode3.Then,aconditionalstatementstartstwopossibleexecutionpaths,whichtheverifierhastoexplore.Theexplicit-valuedomaindoesnotstoreavalueforvariabley,becausethereisnoexplicitvaluefory.AfterbothbranchesoftheCFAareexplored,theARGcontainsa‘frontier’abstractstatethatistheresultofjoiningtheabstractessorsfrombothbranchesforCFAnode8.Theexplicit-valuedomainmightsufferfromalossofinformationifnoexplicitvaluescanbedetermined(e.g.,fory>1).Ontheonehand,thisintroducesimprecisionandpotentiallyfalsealarms.Ontheotherhand,ifvaluesarepresent,alloperationscanbeexecutedextremelyfast.Theprecisioncontrolswhichvariablesaretrackedintheexplicit-valuedomain.ForthecodefragmentinFig.2,wecoulduseaprecision{x,z}andomity,ifweknewbeforehandthatitisnotnecessarytorepresentvariabley. BDDDomain.TheBDDdomainstoresinformationaboutprogramvariablesusingbinarydecisiondiagrams(BDD).EachabstractstateintheBDDdomainisaBDDthatrepresentsapredicateoverthevariablevalues[18].BDDscanbeefficientinrepresentingpredicatesandperformingbooleanoperations.Becauseofthischaracteristic,BDDshavebeenusedinmodelcheckingofsystemswithalargenumberofbooleanvariables,mostprominentlyinhardwareverification[20,31].ValuesofintegervariablescanberepresentedbyBDDsusingabinaryencodingofthevalues(representingtheintegervaluesusing,e.g.,32booleanBDDvariables).WecanrepresentavariablewithevenfewerBDDvariablesifwecanstaticallydeterminethesetofvaluesthatthevariablemightholdatruntimeandthat(non-)equalityistheonlyarithmeticaloperation(nominalscale[37]).Inourexample,thereisonlyonevalueforvariablex(i.e.,x=5),andthusweneedonlyonebooleanvariableforprogramvariablex.ThesizeoftheBDD—andthus,theperformanceoftheBDDoperations—dependsonthenumberofBDDvariables;therefore,itisimportanttokeepthenumberofBDDvariablessmall. 266S.Apeletal.