A relational approach to interprocedural shape ana

ARelationalApproachtoInterproceduralShapeAnalysisBertrandJeannet,AlexeyLoginov,ThomasReps,andMoolySagivIRISA;[e-mail].,Univ.ofWisconsin;alexey,[e-mail].,Tel-AvivUniv.;[e-mail]ificationofpropertiesofimperativeprogramswithrecursiveprocedurecalls,heap-allocatedstorage,anddestructiveupdatingofpointer-valuedfields—i.e.,interproceduralshapeanalysis.Itpresentsawaytoapplysomepreviouslyknownapproachestointerproceduraldataflowanalysis—whichinpastworkhavebeenap-pliedonlytoamuchlessrichsetting—sothattheycanbeappliedtoprogramsthatuseheap-allocatedstorageandperformdestructiveupdating.1IntroductionThispaperconcernstechniquesforstaticanalysisofrecursiveprogramsthatmanipulateheap-allocatedstorageandperformdestructiveupdatingofpointer-valuedfields.Thegoalistorecovershapedescriptorsthatprovideinformationaboutthecharacteristicsofthedatastructuresthataprogram’spointervariablescanpointto.Suchinformationcanbeusedtohelpprogrammersunderstandcertainaspectsoftheprogram’sbehavior,toverifypropertiesoftheprogram,andtooptimizeorparallelizetheprogram.Theworkreportedinthepaperbuildsonpastworkbyseveraloftheauthorsonstaticanalysisbasedon-valuedlogic[20,12,16].Inthissetting,tworelatedlogicscomeintoplay:anordinary-valuedlogic,aswellasarelated-valuedlogic.Amemoryconfiguration,orstore,ismodeledbywhatlogicianscallalogicalstructure,whichconsistsofapredicate(i.e.,arelationofappropriatearity)foreachpredicatesymbolofavocabulary.Astoreismodeledbya-valuedlogicalstructure;asetofstoresisabstractedbya(finite)setofbounded-size-valuedlogicalstructures.Anindividualofa-valuedstructure’suniverseeithermodelsasinglememorycellor,inthecaseofasummaryindividual,acollectionofmemorycells.Theconstraintofworkingwithlimited-sizedescriptorsentailsalossofinformationaboutthestore.Certainpropertiesofconcreteindividualsarelostduetoabstraction,whichgroupstogethermultipleindividualsintosummaryindividuals:apropertycanbetrueforsomeconcreteindividualsofthegroupbutfalseforotherindividuals.Itisforthisreasonthat-valuedlogicisused;uncertaintyaboutaproperty’svalueiscapturedbymeansofthethirdtruthvalue,.Oneoftheopportunitiesforscalingupthisapproachistoexploitthecompositionalstructureofprograms.Ininterproceduraldataflowanalysis,oneavenueforaccomplish-ingthisistocreateasummarytransformerforeachprocedure,andusethesummarytransformerateachcallsiteatwhichiscalled.Eachsummarytransformermustcapture(anover-approximationof)theneteffectofacallon.Tobeabletocreatesummarytransformers,theabstracttransformersforindividualtransitionsmusthavea“composablerepresentation”;thatis,giventherepresentationsoftwoabstracttrans-formers,itmustbepossibletorepresenttheircompositionasanobjectofroughlythesamesize.Onethencarriesoutafixed-point-findingprocedureonacollectionofequa-tionsinwhicheachvariableintheequationsethasatransformer-valuedvalue—i.e.,avaluedrawnfromthedomainoftransformers—ratherthanadataflowvalueproper.Anumberofapproachestointerproceduraldataflowanalysisbasedonsummarytransformersareknown[4,21,11,15,19,17].However,notallprogram-analysisprob-lemshaveabstracttransformersthathaveacomposablerepresentation.Forsomeproblems,itispossibletoaddressthisissuebyworkingpointwise,tabulat-ingcomposedtransformersassetsofpairsofinput/outputvalues[15,19,2].However,forinterproceduralshapeanalysis,thisapproachfailstoproduceusefulinformation.The-valued-logicapproachtoshapeanalysisisastorelessone:individuals,whichmodelmemorycells,donothavefixedidentities;theyareidentifiedonlyuptotheir“distinguishingcharacteristics”,namely,theirvaluesforaspecificsetofunarypredi-cates.Becausethese“distinguishingcharacteristics”canchangeduringthecourseofaprocedurecall,thereisnowaytoidentifyindividualsinaninputabstractstructurewiththeircorrespondingindividualsintheoutputabstractstructure.Inessence,apairofinput/output-valuedstructureslosestrackofthecorrelationsbetweentheinputandoutputvaluesofanindividual’sunarypredicates.Consequently,anapproachbasedontabulatingcomposedtransformersassetsofpairsof-valuedstructuresisnotpromis-ing:therepresentationprovidesonlyaweakcharacterizationofaprocedure’sneteffect.Allisnotlost,however:insteadof“abstractingandthenpairing”(asdiscussedabove),thesolutionisto“pairandthenabstract”.Observation1.Byusing-valuedstructuresoveradoubledvocabulary,whereanddenotesdisjointunion,oneobtainsafiniteabstractionthatrelatesthepredicatevaluesforanindividualatthebeginningofatransitiontothepredicatevaluesfortheindividualattheendofthetransition.Thisabstractionprovidesawaytocreatemuchmoreaccuratecomposablerepresen-tationsoftransformers,andhencemuchmoreaccuratesummarytransformers,forabroadclassofproblems.Moreover,byextendingtheabstractdomainof-valuedlog-icalstructures[20]withsomenewoperations,itispossibletoperformabstractinter-pretationofcallandreturnstatementswithoutlosingtoomuchprecision(see4).Wehaveusedtheseideastocreateacontext-sensitiveshape-analysisalgorithmforrecur-siveprogramsthatmanipulateheap-