UndecidabilityofStaticAnalysis
`WilliamLandi
`SiemensCorporateResearchInc
`CollegeRdEast
`Princeton,NJ
`wlandi@scr.siemens.com
`Abstract
`StaticAnalysisofprogramsisindispensabletoanysoftwaretool,environment,orsystem
`thatrequirescompiletimeinformationaboutthesemanticsofprograms.Withthe
`emergenceoflanguageslikeCandLISP,StaticAnalysisofprogramswithdynamic
`storageandrecursivedatastructureshasbecomea(cid:12)eldofactiveresearch.Suchanalysis
`isdi(cid:14)cult,andtheStaticAnalysiscommunityhasrecognizedtheneedforsimplifying
`assumptionsandapproximatesolutions.However,evenunderthecommonsimplifying
`assumptions,suchanalysesareharderthanpreviouslyrecognized.Twofundamental
`StaticAnalysisproblemsareMayAliasandMustAlias.Theformerisnotrecursive
`(i.e.,isundecidable)andthelatterisnotrecursivelyenumerable(i.e.,isuncomputable),
`evenwhenallpathsareexecutableintheprogrambeinganalyzedforlanguageswith
`if-statements,loops,dynamicstorage,andrecursivedatastructures.
`CategoriesandSubjectDescriptors:D. . [ProgrammingLanguages]:Processors;F. . [Com-
`putationbyAbstractDevices]:ModelsofComputation(cid:0)bounded-actiondevices;F.. [Math
`LogicandFormalLanguages]:MathematicalLogic(cid:0)computabilitytheory
`GeneralTerms:Languages,Theory
`AdditionalKeyWordsandPhrases:Aliasanalysis,data(cid:13)owanalysis,abstractinterpretation,
`haltingproblem
`FromacmLettersonProgrammingLanguagesandSystems,
`Vol. ,No.,December ,Pages  - .
`Permissiontocopywithoutfeeallorpartofthismaterialisgranted
`providedthatthecopiesarenotmadeordistributedfordirectcommercial
`advantage,theACMcopyrightnoticeandthetitleofthepublicationand
`itsdateappear,andnoticeisgiventhatcopyingisbypermissionofthe
`AssociationforComputingMachinery.Tocopyotherwise,ortorepublish,
`requiresafreeand/orspeci(cid:12)cpermission.
`c(cid:13) ACM - / / -  $ .
`
`
`Columbia Ex 2038-1
`Symantec v Columbia
`IPR2015-00375
`
`

`
`Introduction
`
`StaticAnalysisistheprocessesofextractingsemanticinformationaboutaprogramatcompile
`time.Oneclassicalexampleisthelivevariables[]problem;avariablexisliveatastatement
`si(cid:11)onsomeexecutionxisused(accessed)aftersisexecutedwithoutbeingrede(cid:12)ned.Other
`classicalproblemsincludereachingde(cid:12)nitions,availableexpressions,andverybusyexpressions[].
`TherearetwomainframeworksfordoingStaticAnalysis:DataFlowAnalysis[]andAbstract
`Interpretation[ ].Theframeworkisnotrelevanttothispaper,asweshowthattwofundamental
`StaticAnalysisproblemsareharderthanpreviouslyacknowledged,regardlessoftheframework
`used.WeviewthesolutiontoaStaticAnalysisproblemasthesetof\facts"thatholdforagiven
`program.Thus,forlivevariablesthesolutionisf(x;s)jvariablexisliveatstatementsg.With
`thatinmind,wereviewafewde(cid:12)nitions:
`(cid:15)Asetisrecursivei(cid:11)itcanbeacceptedbyaTuringmachinethathaltsonallinputs.
`(cid:15)Asetisrecursivelyenumerablei(cid:11)itcanbeacceptedbyaTuringmachinewhichmayormay
`nothaltonallinputs.
`StaticAnalysisoriginallyconcentratedonFORTRAN,andwaspredominatelycon(cid:12)nedtoa
`singleprocedure(intraproceduralanalysis)[, , ].However,eventhissimpleformofStatic
`Analysisisnotrecursive.Thedi(cid:14)cultyliesinconditionals.Thereare,ingeneral,manypaths
`throughaprocedure,butnotallpathscorrespondtoanexecution.Forexample,consider
`if(x>- )y= ;
`if(x<)y=- ;
`Executionofthisfragmentalwaysexecutesexactlyonethenbranch.Itisimpossibleforbothor
`neitherthenbranchestobeexecuted.StaticAnalysisisnotrecursivesincedeterminingwhich
`pathsareexecutableisnotrecursive.Toovercomethisproblem,StaticAnalysisisperformed
`assumingthatallpathsthroughtheprogramareexecutable[].Thisassumptionisnotalways
`valid,butitissafe[]. Also,itsimpli(cid:12)estheproblemandallowsStaticAnalysisofFORTRAN
`procedurestobedonefairlye(cid:14)ciently.Someapproaches(forexample[ ])categorizesomepaths
`asnotexecutable.However,thesetechniqueshavelimitedapplicability,andoftenmustassume
`thatpathsareexecutable.
`Withabasisofa(cid:12)rmunderstandingofintraproceduralStaticAnalysisofFORTRAN,Static
`Analysisofentireprograms(interproceduralanalysis)wasinvestigated.Myers[ ]cameupwith
`thenegativeresultthatmanyinterproceduralStaticAnalysisproblemsareNPcomplete.Prac-
`tically,thismeansthatinterproceduralStaticAnalysismustmakefurtherapproximationsover
`intraproceduralanalysisortakeanexponentialamountoftime.
`WiththeemergenceofpopularlanguageslikeCandLISP,theStaticAnalysiscommunityhas
`turneditsattentiontolanguageswithpointers,dynamicstorage,andrecursivedatastructures.It
`iswidelyacceptedthatStaticAnalysisundertheseconditionsishard.Thegeneralfeelingisthat
`itisprobablyNPcomplete[ , , ];thisisincorrect.Recently,theproblemof(cid:12)ndingaliases
`wasshowntobeP-spacehard[ ].Unfortunately,thisisstillanunderestimate.
` Thetermconservativeisusedin[]insteadofsafe.
`
`Columbia Ex 2038-2
`Symantec v Columbia
`IPR2015-00375
`
`

`
`Analiasoccursatsomepointduringexecutionofaprogramwhentwoormorenamesexistfor
`thesamestoragelocation.Forexample,theCstatement\p=&v"createsanaliasbetween(cid:3)pand
`v.Aliasesareassociatedwithprogrampoints,indicatingnotonlythat(cid:3)pandvrefertothesame
`locationduringexecution,butalsowhereintheprogramtheyrefertothesamelocation.Aliasing,
`statically(cid:12)ndingaliases,isafundamentalproblemofStaticAnalysis.Considertheproblemof
`(cid:12)ndinglivevariablesfor:
`v= ;
`s :
`p=&v;
`s:
`w=;
`s :
`printf("%d",(cid:3)p);
`s:
`Thevariablevisliveats onlybecause(cid:3)pisaliasedtovwhenprogrampointsisexecuted.
`Aliasingalsoin(cid:13)uencesmostinterestingStaticAnalysisproblems.Anyproblemthatisin(cid:13)uenced
`byaliasingisatleastashardasaliasing.Therearetwotypesofaliasing.
`MayAliasFindthealiasesthatoccurduringsomeexecutionoftheprogram.
`MustAliasFindthealiasesthatoccuronallexecutionsoftheprogram.
`Findingthealiasescanmeandeterminingthesetofallaliaseswhichholdatsomeassociated
`programpoints,ordeterminingwhetherxandyarenamesforthesamelocationataparticular
`programpoints.Weusethelattermeaningas,ingeneral,thesetofallaliasesmaybein(cid:12)nitein
`size.Weformallyde(cid:12)neMayAliasasabooleanfunction:
`may-aliasP(s;hx;yi)istruei(cid:11)thereisanexecutionofprogramPtoprogrampoints
`(includingthee(cid:11)ectsofexecutings)onwhichxandyrefertothesamelocation.
`MustAliasisde(cid:12)nedanalogously.Weshowthat,forlanguageswithif-statements,loops,dynamic
`storage,andrecursivedatastructures,IntraproceduralMayAliasisnotrecursive(i.e.,isundecid-
`able)andIntraproceduralMustAliasisnotrecursivelyenumerable(i.e.,isuncomputable)even
`whenallpathsinaprogramareexecutablebyreducing([],p.  - )thehaltingprobleminto
`analiasproblem.Thisisadi(cid:11)erentfromtheresultofKamandUllman[]thattheMOPsolution
`isundecidableformonotoneframeworks.
`ReductionoftheHaltingProblemtoanAliasProblem
`ADeterministicTuringMachine(DTM)[ ]isatuple(Q,T,I,(cid:14),(cid:12),q,qf)where:
`(cid:15)Q=fq ,q,...,qnQgisthesetofstates
`(cid:15)T=f(cid:27) ;(cid:27);:::;(cid:27)nTgisthesetoftapesymbols
`(cid:15)I(cid:26)Tisthesetofinputsymbols
`(cid:15)(cid:14):(Q(cid:2)T)!(Q(cid:2)T(cid:2)fL,R,Sg)isthetransitionfunction
`
`
`Columbia Ex 2038-3
`Symantec v Columbia
`IPR2015-00375
`
`

`
`(cid:15)(cid:12)T(cid:0)Iistheblanksymbol
`(cid:15)qQisthestartstate
`(cid:15)qfQisthe(cid:12)nalstate
`Weassumethat(cid:14)isatotalfunctionandthattheDTMwillnotmoveo(cid:11)theleftendofthetape.In
`general,neitheroftheseassumptionsaretrue,butanyTuringmachinecanbemodi(cid:12)edtoconform
`tothem.
`Inthissection,wespecifyamachinereduce(Figure )whichtakesaDTMMandinputstring
`wandproceduresaprogramCsuchthat
`(cid:15)may-aliasC(s;h(cid:3)(cid:3)currentstate,validsimulationi)istruei(cid:11)Mhaltsonw.
`(cid:15)must-aliasC(s;h(cid:3)(cid:3)currentstate,notvalidi)istruei(cid:11)Mdoesnothaltonw.
`(cid:15)allpathsthroughCareexecutable
`. RepresentinganID
`AnInstantaneousDescription(ID)isanencodingofthefollowinginformation:
`(cid:15)contentsoftheDTM'stape
`(cid:15)currentstateoftheDTM
`(cid:15)locationofthetapehead
`AnIDisusuallyrepresentedbyastringxqiyT(cid:3)QT(cid:3)wherethetapecontainsxyin(cid:12)nitelypadded
`totherightwithblanks,thecurrentstateisqi,andthetapeheadisscanningthe(cid:12)rstcharacterof
`y. Weencodethisinformationinthealiaspatternofaprogramexecution.Byaliaspattern,we
`meantherelationshipofnamestoeachother.
`prev
`sym
`next
`WeuseadoublylinkedlisttorepresentthetapeofaDTM:
`.For
`each(cid:27)iTwecreateavariable(cid:27)i.The\sym"(cid:12)eldpointsto(cid:27)ii(cid:11)thetapelocationcontains(cid:27)i.
`Thus,thetapethatcontained\hello"paddedtotherightwithblanks((cid:12))isrepresentedbythe
`aliaspattern:
`r
`r
`(cid:27)
`r
`(cid:27)
`(cid:27)
`r
`(cid:27)
`r
`(cid:27)
`r
`r
`r
`r
`r
`r
`r
`-
`-
`-
`-
`-
`r
`r
`r
`r
`r
`r
`@@R(cid:0)(cid:0)(cid:9)l:
`o:?(cid:12):?
`h:?e:?
`Lmovestapeheadleft,Rmovestapeheadright,andSleavesthetapeheadwhereitis.
` qiisunderlinedinxqiytomakethestatestandoutfromthetapestring.
`
`
`Columbia Ex 2038-4
`Symantec v Columbia
`IPR2015-00375
`
`

`
`ForeachqiQwecreateavariableqiandtherearetwoadditionalvariables,currentstate
`andtapehead.Currentstatepointstothecurrentstateofthemachine,andtapehead
`indicatesthetapeheadlocationbypointingintothelistrepresentingthetape.TheID=heqllo
`isrepresentedby:
`r?
`tapehead:
`r?
`currentstate:
`(cid:27)
`(cid:27)
`(cid:27)
`(cid:27)
`(cid:27)
`r
`r
`r
`r
`r
`r
`r
`r
`r
`r
`r
`r
`r
`-
`r
`-
`r
`-
`r
`r
`-
`r
`-
`@@R(cid:0)(cid:0)(cid:9)l:
`q:
`...qnQ:
`q :
`h:?e:?
`o:?(cid:12):?
`.ProgrammingLanguage
`Inordertoperformtherequiredreduction,weneedtoconstructaprogramfromaDTM.The
`programisinC,butitcouldbeanylanguagewithif-statements,loops,dynamicstorage,and
`recursivedatastructures.Weusetheaddressoperator(&)butitisnotfundamentallynecessary
`totheproof.TospecifyaCprogramfromaDTM,weneedthemeta-statements:#forand#if.
`Thesyntaxandmeaningofthesearerelativelystraightforwardandshouldbeapparentfromthe
`followingexamples:
` >=>;represents><>:
`#fori= to
`x = ;
`xi=i;
`x=;
`#endfor
`x = ;
` >>>>>>>=>>>>>>>;represents>>>>><>>>>>:
`#fori= to
`x = ;
`xi=i;
`y = ;
`#ifiisodd
`x=;
`yi=i;
`x = ;
`#endif
`y = ;
`#endfor
`Also,weusenextboolforreadingprograminput.Itreturnsthenextbooleanvaluefromtheinput
`stream.Iftheendofthestreamhasbeenencountered,itreturns.
`. SimulatingaDTM
`InSection. ,weshowedhowwerepresentanIDwithaliases.Inthissection,weshowhowto
`simulateaDTMwiththealiaspatternofexecutionsofaparticularprogram.Wenowspecifyreduce
`(Figure )whichconstructsaprogramfromaDTMM=(Q,T,I,(cid:14),(cid:12),q,qf)withinitialinputw
`
`
`Columbia Ex 2038-5
`Symantec v Columbia
`IPR2015-00375
`
`

`
`/(cid:3)GivenaDTM,M=(Q,T,I,(cid:14),(cid:12),q,qf)andwI(cid:3)(cid:3)/
`Figure
`Generatevariabledeclarationandinitialization
`Figure
`GeneratecodeforcreatingtheinitialInstantaneousDescription
`Figure
`Generatecodeforsimulatingthetransitionfunction
`Figure
`Generatecodeforvalidatingtheresult
`s:
`Figure :Outlineofthemachinereduce
`I(cid:3)suchthat(cid:3)(cid:3)currentstateisaliasedtovalidsimulationonsomeexecutiontoprogrampoint
`si(cid:11)machineMhaltsoninputw=x x:::xnw.
`Lemma. ThecodegeneratedbyFigure createsthedatastructurethatrepresentstheinitial
`con(cid:12)gurationofM(qx x:::xnw)inthemannerdescribedinSection. .
`Thisisevidentfrominspectionofthecode.\currentstate=&q;"pointscurrentstate
`toq.tapeheadpointstothe(cid:12)rstelementofthelinkedlistwhichcorrespondstothetapehead
`ofMbeingonthebeginningofthetape.Finally,NEXTSYM(i)pointsthe\sym"(cid:12)eldofthe
`ithelementofthelinkedlisttothevariablerepresentingtheithsymbolonthetape(xi).Thisis
`exactlywhatisrequiredbySection. fortheinitialIDqx x:::xnw.
`Asanexample,considerthecasewhereT=fh,e,l,o,(cid:12)g,w=\hello",andq=q.Theinitial
`IDisqhelloandthecodegeneratedbyFigure produces:
`r
`r?
`tapehead:
`back:
`r?
`currentstate:
`?
`r
`(cid:27)
`r
`(cid:27)
`r
`(cid:27)
`r
`r
`(cid:27)
`r
`(cid:27)
`r
`r
`r
`r
`r
`r
`-
`r
`r
`-
`r
`-
`r
`-
`r
`-
`r
`@@R(cid:0)(cid:0)(cid:9)l:
`q :
`q:
`...qnQ:
`o:?(cid:12):?
`h:?e:?
`Noticethatbackpointstotheendofthelinkedlistrepresentingthetape.Thisallowsustoadd
`anewtapeelementtotheendofthetapeand,asseenlater,isusedtoensurethatweneverrun
`o(cid:11)therightendofthetape.
`ThedeclarationandinitializationofthevariablesoftheprogramusedtosimulateaDTMare
`speci(cid:12)edinFigure.Allthevariablesexceptyes,no,notvalid,andvalidsimulationhave
`
`
`Columbia Ex 2038-6
`Symantec v Columbia
`IPR2015-00375
`
`

`
`/(cid:3)GivenaDTM,M=(Q,T,I,(cid:14),(cid:12),q,qf)andwI(cid:3)(cid:3)/
`typedefint**state;
`typedefint**letter;
`structtapef
`letter*sym;
`structtape*next,*prev;
`g*back,*tapehead;
`state*currentstate;
`intnotvalid,validsimulation;
`int*yes=&validsimulation;
`int*no=&notvalid;
`#fori= tonQ
`stateqi=&yes;
`#endfor
`#fori= tonT
`letter(cid:27)i=&yes;
`#endfor
`Figure:Variabledeclarationandinitialization
`/(cid:3)GivenaDTM,M=(Q,T,I,(cid:14),(cid:12),q,qf)andwI(cid:3)(cid:3)/
`currentstate=&q;
`back=malloc(sizeof(structtape));
`tapehead=back;
`tapehead->prev=NULL;
`tapehead->next=NULL;
`tapehead->sym=&(cid:12);
`/*initializetapetow=x x:::xnw*/
`#fori= tonw
` >>>>>>>=>>>>>>>;NEXTSYM(i)
`back->next=malloc(sizeof(structtape));
`back->sym=&xi;
`back->next->prev=back;
`back=back->next;
`back->next=NULL;
`back->sym=&(cid:12);
`#endforFigure :InitialInstantaneousDescription(ID)
`
`
`Columbia Ex 2038-7
`Symantec v Columbia
`IPR2015-00375
`
`

`
`/(cid:3)GivenaDTM,M=(Q,T,I,(cid:14),(cid:12),q,qf)andwI(cid:3)(cid:3)/
`/(cid:3)nextboolreturnsthenextbooleanvaluefromtheinputstream.(cid:3)/
` >>>>>=>>>>>;
`back->next=malloc(sizeof(structtape));
`back->next->prev=back;
`ADDTOEND
`back=back->next;
`back->next=NULL;
`back->sym=&(cid:12);
`#fori= tonQ/*onceforeachstateqiQ*/
`#forj= tonT/*onceforeachletter(cid:27)jT*/
`/*let(cid:14)(qi;(cid:27)j)=(qi;(cid:27)j;d)*/
`if(nextbool== )f
` >>>>>>>>>>>>>>>>>>>>>>>>>=>>>>>>>>>>>>>>>>>>>>>>>>>;
`qi=&no;
`(cid:27)j=&no;
`(cid:3)(cid:3)currentstate=&notvalid;
`(cid:3)(cid:3)(tapehead->sym)=&notvalid;
`currentstate=&qi;
`tapehead->sym=&(cid:27)j;
`#ifd=R
`DELTA(i,j)
`tapehead=tapehead->next;
`#endif
`#ifd=L
`tapehead=tapehead->prev;
`#endif
`qi=&yes;
`(cid:27)j=&yes;
`gelse
`#endfor
`#endforyes=&notvalid;/(cid:3)Thisistheelsepartofthelast
`(cid:3)if-then-elseproducedabove.*/
`gno=&notvalid;/(cid:3)(cid:3)noalreadyisnotvalid,butthe
` >>>>>>>=>>>>>>>;CHECKANSWER
`(cid:3)assignmentmakestheproofsimpler(cid:3)/
`#fori= tonQ
`qi=&no;
`#endfor
`qf=&yes;
`/(cid:3)(cid:3)(cid:3)currentstateisvalidsimulationherei(cid:11)Mhaltsonw(cid:3)/
`Figure:Representationofthetransitionfunction
`
`
`s:
`
`Columbia Ex 2038-8
`Symantec v Columbia
`IPR2015-00375
`
`

`
`alreadybeenexplainedinSection. .Threeofthefournewvariablesaresimplytorecordif
`thecurrentpathisavalidsimulationofM.Yespointstovalidsimulationi(cid:11)thecurrentpath
`isasimulationofMandyespointstonotvalidotherwise.Thefourthvariable(no)isjusta
`\don'tcare"locationforpointersthatmustrefertosomethingotherthanyes.Noalwayspoints
`tonotvalid.Continuingourexample,theinitializationspeci(cid:12)edinFigurefollowedbythecode
`speci(cid:12)edinFigure forT=fh,e,l,o,(cid:12)g,w=\hello",andq=q,produces:
`r
`r?
`tapehead:
`back:
`r?
`currentstate:
`?
`r
`r
`(cid:27)
`r
`(cid:27)
`r
`(cid:27)
`(cid:27)
`r
`(cid:27)
`r
`r
`r
`r
`r
`r
`r
`r
`-
`r
`r
`-
`r
`-
`r
`-
`-
`r
`@@R(cid:0)(cid:0)(cid:9)l:
`r?q:
`r?...qnQ:
`r?
`q :
`h:?r?e:?r?
`o:?r?(cid:12):?r?
`r?
`-yes:
`r?
`r?
`no:
`notvalid:
`validsimulation:
`Theremainderoftheprogramcreatedbyreduceismostlyawhileloop(Figure).Eachpass
`throughthebodyofthelooprepresentsoneapplicationofthetransitionfunction((cid:14)).The(cid:12)rst
`partthetheloop(ADDTOEND)simplyaddsanewtapelocation,initiallyblank,totheright
`endofthetape.ThisensuresthatwheneverthesimulatedDTMmovesrightonthetape,atape
`locationisavailabletoit.Theremainderoftheloopisanestedif-then-else-if
`if(nextbool== )DELTA( , );
`elseif(nextbool== )DELTA( ,);
`...elseif(nextbool== )DELTA(nQ,nT);
`elseyes=&notvalid;
`whereDELTA(i,j)(explainedbelow)isthecodetoimplement(cid:14)(qi;(cid:27)j).Thecode
`if(nextbool== )DELTA( , );
`if(nextbool== )DELTA( ,);
`...if(nextbool== )DELTA(nQ,nT);
`wouldalsobevalidanddoesnotrequireanarti(cid:12)ciallydeepif-then-else-ifnesting.However,inthe
`former,apassthroughtheloopeitherisnotavalidsimulationorrepresentsexactlyonetransition
`oftheDTMM.Inthelater,apassthroughtheloopisaninvalidsimulationorrepresentsalegal
`sequenceoftonQ(cid:3)nTtransitionsofM.Theformerispreferablebecauseitmakestheproofof
`correctnesseasier.
`
`
`Columbia Ex 2038-9
`Symantec v Columbia
`IPR2015-00375
`
`

`
`Lemma.Ifyespointstonotvalidbeforetheloopspeci(cid:12)edinFigureisexecutedthenyes
`stillpointstonotvalidafterexecutionoftheloop.
`Inspectionofthecoderevealsthatinthewhilelooponly&notvalidcanbeassignedtoyes.
`ThenextlemmabasicallystatesthatiftheexecutionisavalidsimulationofMbeforeexecuting
`theloopgeneratedbyFigure,thenonepaththroughtheloopsimulatesthenexttransitionofM
`andallotherpathsarenotavalidsimulation.
`Lemma. Ifbeforetheloopspeci(cid:12)edinFigureisexecuted,yespointstovalidsimulation,
`theIDencodedbythealiaspatternisxqiy,andxqiy`Mxqjythenonallbutonepaththroughthe
`loopyespointstonotvalidandontheremainingpath,yespointstovalidsimulationandthe
`aliaspatternrepresentstheIDxqjy.
`Weillustratethisproofwiththeexampleheqllo`Mhq eelo(therefore(cid:14)(q,l)=(q ,e,L)).For
`thisexample,thealiaspatternbeforeexecutionoftheloopis:
`r?
`r?
`back:
`tapehead:
`r?
`currentstate:
`r
`r
`(cid:27)
`r
`(cid:27)
`r
`(cid:27)
`(cid:27)
`r
`-(cid:27)-(cid:27)
`r
`
`r
`r
`r
`r
`r
`...
`r
`-
`-
`-
`-
`r
`r
`r
`r
`r
`r
`@@R(cid:0)(cid:0)(cid:9)l:
`r?q:
`r?...qnQ:
`r?
`q :
`h:?r?e:?r?
`o:?r?
`(cid:12):?r?
`r?
`-yes:
`r?
`r?
`no:
`notvalid:
`validsimulation:
`Beforeexecutionofthewhileloop,all(cid:27)TandallqQpointtoyes.The(cid:12)rstpart
`oftheloop,asstatedearlierjustexpandsthetape.Thelastelse-clausesimplypointsyesto
`notvalidsignalinganinvalidsimulation.NowconsiderthecodeforDELTA(i,j)whichrepresents
`theapplicationof(cid:14)(qi;(cid:27)j).NoticethatwecanonlyusethisruleifMisinstateqiandthetape
`headisreading(cid:27)j.Thuswewouldliketosay(inpseudo-C)
`if((cid:3)currentstate=qior(cid:3)tapehead->sym=(cid:27)j)
`( )
`yes=&notvalid/(cid:3)i.e.,notavalidsimulation(cid:3)/
`butthiswouldcreatepathswhicharenotexecutableintheprogram.The(cid:12)rstfourstatements
`ofDELTA(i,j)doexactly( )withoutusingaconditional.Thestatements\qi=&no;(cid:27)j=&no"
`Wehavenotproventhishere,butitfollowsfromasimpleinductiveproofonnumberofiterationsofthewhile
`loop.
`
`
`Columbia Ex 2038-10
`Symantec v Columbia
`IPR2015-00375
`
`

`
`pointqiand(cid:27)jtono.Allotherstatesandalphabetsymbolsstillpointtoyes.Inourrunning
`example(whereqi=qand(cid:27)j=l)wehave:
`r?
`r?
`tapehead:
`back:
`r?
`currentstate:
`r
`r
`(cid:27)
`r
`(cid:27)
`r
`(cid:27)
`(cid:27)
`r
`-(cid:27)-(cid:27)
`r
`
`...
`r
`r
`r
`r
`r
`r
`r
`r
`-
`r
`r
`-
`r
`-
`r
`-
`@@R(cid:0)(cid:0)(cid:9)l:
`
`r?
`r?q:r(cid:0)(cid:0)(cid:0)(cid:0)
`...qnQ:
`q :
`h:?r?e:?r?
`o:?r?
`(cid:12):?r?
`r@@@R
`-yes:
`(cid:27)
`r?
`r?
`no:
`notvalid:
`validsimulation:
`Thestatements,\(cid:3)(cid:3)currentstate=&notvalid"and\(cid:3)(cid:3)(tapehead->sym)=&notvalid",
`makesurethattheapplicationof(cid:14)(qi,(cid:27)j)isapplicable.Therearetwocasesthatcanoccur:
`(cid:15)Thetapeheadisscanning(cid:27)j(l)andMisinstateqi(q)
`Thismeansthat(cid:3)(cid:3)currentstateisnoand(cid:3)(cid:3)(tapehead->sym)isalsono.Thusbothof
`thesestatementse(cid:11)ectivelyare\no=&notvalid"andthevalueofyesisunchangedand
`stillpointstovalidsimulation.Thisisthepaththroughtheloopthatisavalidsimulation
`ofM.Foralli,jthereisexactlyonesuchpathsinceMisaDTM.
`(cid:15)Eitherthetapeheadisnotscanning(cid:27)j(l)orMisnotinstateqi(q)
`Inthe(cid:12)rstcase,(cid:3)(cid:3)currentstateisyes.Thus\(cid:3)(cid:3)currentstate=&notvalid"causes
`yestopointtonotvalidinsteadofvalidsimulation.Inthesecondcase(cid:3)(cid:3)(tapehead-
`>sym)isyesand\(cid:3)(cid:3)(tapehead->sym)=&notvalid"causesyestopointtonotvalid.
`Thelemmaissatis(cid:12)edregardlessofthesubsequentcodebecauseyespointstonotvalid.
`WenowproceedassumingthatMisscanning(cid:27)j(l)andisinstateqi(q).Since(cid:14)(qi,(cid:27)j)=(qi,(cid:27)j,d)
`wewanttoshifttostateqi(\currentstate=&qi"),write(cid:27)jtothetape(\tapehead->sym=
`&(cid:27)j"),andmovethetapeheadoneunitindirectiond:
`#ifd=R
`#ifd=L
`tapehead=tapehead->next;
`tapehead=tapehead->prev;
`#endif
`#endif
`Finally,thestatements\qi=&yes;(cid:27)j=&yes"restoretheconditionthatallstateandalpha-
`betvariablespointtoyes.To(cid:12)nishourexamplewhere(cid:14)(q,l)=(q ,e,L),theprogramstorenow
`is:
`
`
`Columbia Ex 2038-11
`Symantec v Columbia
`IPR2015-00375
`
`

`
`r?
`r
`back:
`tapehead:
`r(cid:8)(cid:8)(cid:8)(cid:8)(cid:25)
`currentstate:
`?
`-(cid:27)-(cid:27)
`(cid:27)
`(cid:27)
`(cid:27)
`r
`r
`r
`r
`
`r
`r
`(cid:27)
`r
`r
`r
`r
`...
`r
`r
`-
`-
`-
`-
`r
`r
`r
`r
`r
`r
`(cid:0)(cid:0)(cid:9)l:
`(cid:0)(cid:0)(cid:0)(cid:27)
`r?
`r?q:
`r?...qnQ:
`q :
`o:?r?
`(cid:12):?r?
`h:?r?e:?r?
`r?
`-yes:
`r?
`r?
`no:
`notvalid:
`validsimulation:
`TherestofFigureisaddressedinthefollowinglemma:
`Lemma.Mhaltsonwi(cid:11)onsomepathtos,intheprogramgeneratedbyreduce,
`(cid:3)(cid:3)currentstateisvalidsimulation.
`ConsidertheprogramCgeneratedbyreduce.Byaninductiveargumentitiseasytoshowthat:
` .onallpathstothetopofthewhilelooponwhichyespointstovalidsimulation,ifthe
`aliaspatternrepresentsxqiythenqw`(cid:3)Mxqiy.
`.ifqw`(cid:3)Mxqiythenthereisatleastonepathtothetopofthewhileloopgeneratedby
`Figureonwhichyespointstovalidsimulationandthealiaspatternrepresentsxqiy.
`Theproofsarebyinductiononthenumberoftimesthepathhaspassedthroughthetopofthe
`loopandonnumberofstepsMhastakentoderivexqiy.Inbothproofs,thebasecaseisshown
`byLemma. andtheinductionstepcanbeshownbyappealingtoLemma.andLemma. .
`Mhaltsonwi(cid:11)qw`(cid:3)Mxqfy(somex,y);thusMhaltsonwi(cid:11)thereexistsapathtothetopof
`thelooponwhichyespointstovalidsimulationandcurrentstatepointstoqf.
`Considerthee(cid:11)ectsofCHECKANSWERinFigure.
`(cid:15)Ifcurrentstatedoesnotpointtoqfthen**currentstatemustbenotvalid.
`(cid:15)Ifyespointstonotvalidthen**currentstatemustbenotvalid.
`(cid:15)Ifcurrentstatepointstoqfandyespointstovalidsimulationthen**currentstate
`mustbevalidsimulation.
`ThismeansthatMhaltsonwi(cid:11)onsomepathtos(cid:3)(cid:3)currentstateisvalidsimulation.
`exactlyonepathunlessxqiy`+Mxqiy.
` 
`
`Columbia Ex 2038-12
`Symantec v Columbia
`IPR2015-00375
`
`

`
` MayAliasisnotrecursive
`Theorem . StaticallydeterminingIntraproceduralMayAliasforlanguageswithif-statements,
`loops,dynamicstorage,andrecursivedatastructuresisrecursivelyenumerablebutnotrecursive
`evenwhenallpathsthroughtheprogramareexecutable.
`ConsidertheprogramCgeneratedbyreduce.AllpathsthroughCareexecutable.Consider
`anypathP,letc c:::ckbeasequencewithauniqueciforeveryconditional(i.e.,ifandwhile
`statements)onPintheorderthattheyappearonP.Letcibe ifthetruebranchofthe
`correspondingconditionalistakenonP,andletcibeotherwise.Clearly,c c:::ckisaninput
`thatexecutespathP.ByLemma.,Mhaltsonwi(cid:11)onsomepathtosinC(cid:3)(cid:3)currentstate
`isvalidsimulation.Therefore,MayAliasisnotrecursiveasitcanbeusedtosolvethehalting
`problemevenforprogramsonwhichallpathsareexecutable.MayAliasisrecursivelyenumerable
`sincewecannondeterministicallygeneraterunsofaprogramandquestionsaboutaliasingduring
`anexecutioncanbeansweredbyexaminingthesymboltableandtheprogramstore.
`Theorem .StaticallydeterminingIntraproceduralMustAliasforlanguageswithif-statements,
`loops,dynamicstorage,andrecursivedatastructuresisnotrecursivelyenumerableevenwhen
`allpathsthroughtheprogramareexecutable.
`Aquicklookattheprogramproducedbyreduce(onwhichallpathsareexecutable;seeproof
`ofTheorem . )showsthatyeseitherpointstonotvalidorvalidsimulation,noalwayspoints
`tonotvalid,qQalwayspointstoyesorno,andcurrentstatealwayspointstoastate.This
`impliesthat(cid:3)(cid:3)currentstateiseithervalidsimulationornotvalid.Sincewealreadyshowed
`thatMhaltsonwi(cid:11)onsomepathtos(cid:3)(cid:3)currentstateisvalidsimulation(Lemma.),it
`followsthatMdoesnothalti(cid:11)(cid:3)(cid:3)currentstateisnotvalidonallpathstos.Thus,MustAlias
`canbeusedtosolvethecomplementofthehaltingproblemwhichisnotrecursivelyenumerable.
`ThismeansthatMustAliasisnotrecursivelyenumerablegiventhelanguagerequirementsstated
`bythetheorem.
`
`
`Columbia Ex 2038-13
`Symantec v Columbia
`IPR2015-00375
`
`

`
`Conclusion
`WehaveshownthatintraproceduralMayAliasisnotrecursiveandintraproceduralMustAliasis
`notrecursivelyenumerableevenforprogramsonwhichallpathsareexecutablegiventhelanguage
`hasdynamicallyallocatedrecursivedatastructures,loops,andif-statements.Thisisanextremely
`negativeresult,consideringthatadoublylinkedlistwastheonlydynamicdatastructureneeded.
`Unfortunately,theproofscanbemodi(cid:12)edtouseonlyasinglylinkedlist.InAppendixA,weshow
`howtomodifyreducesothatonlyasinglylinkedlistisneeded.
`TheseresultsdonotimplythatStaticAnalysisisdead.Theysimplymeanthat,ashasbeen
`knownallalong,someapproximationmustbedone.Whatthenewresultsdoshowisthat,evenif
`weareallowedtowriteexponentialalgorithms,StaticAnalysiswouldstillhavetobeapproximate.
`Itprobablyalsomeansthat,inthepresenceofdynamicallyallocatedrecursivedatastructures,we
`havetoacceptapproximationsoflesserquality,whichalsotakemoretimeandspacetocompute
`thaninFORTRAN.One(cid:12)nalimplicationofourresultsisthatwhiledeterminingthestructureof
`dynamicdatastructures(i.e.,isitatree?linkedlist?...)isimportant,itisnotsu(cid:14)cienttomake
`StaticAnalysisrecursive,becauseourproofsusedonlyprogramswithlinkedlists.
`Currently,StaticAnalysisisinthesamesituationasitwasforFORTRANorsoyearsago.
`Wearedealingwithaproblemwhichisnotrecursive,andneedtocomeupwithagoodsetof
`simplifyingassumptionsandalgorithmsthatyieldreasonablygoodapproximationsquicklyand
`cheaply.InmostworkinStaticAnalysis,theseassumptionsarebeingintroducedinanadhoc
`mannerandareoftennotevenexplicitlystated.Inthefuture,itwouldbenicetohavesimplifying
`assumptionsthatwouldworkforStaticAnalysisisgeneral.Onesuchassumptionisthatonly
`polynomiallengthpathsneedbeconsidered.Thisseemsreasonable,aswealreadyassumethat
`programs\terminatenormally"(forexample,nodivisionby),andnon-polynomialexecutionsare
`generallynottolerated.TheniceresultofthisassumptionisthatitmakesmostStaticAnalyses
`NPcomplete(seeAppendixB).Ontheotherhand,itisdi(cid:14)culttoseehowthiswouldin(cid:13)uence
`thedevelopmentofapproximatealgorithms.
`Acknowledgments:WethankRitaAltucher,BruceLadendorf,TomMarlowe,MichaelPlat-
`o(cid:11),andthereviewersfortheircommentsonthismaterial.
` 
`
`Columbia Ex 2038-14
`Symantec v Columbia
`IPR2015-00375
`
`

`
`References
`[ ]Aho,A.V.,Hopcroft,J.E.,andUllman,J.D.TheDesignandAnalysisofComputerAlgorithms.
`Addison-Wesley, .
`[]Aho,A.V.,Sethi,R.,andUllman,J.D.Compilers:Principles,Techniques,andTools.Addison-Wesley,
` .
`[ ]Cousot,P.,andCousot,R.Abstractinterpretation:Auni(cid:12)edlatticemodelforstaticanalysisofprograms
`byconstructionorapproximationof(cid:12)xpoints.InConferenceRecordoftheFourthAnnualACMSymposiumon
`PrinciplesofProgrammingLanguages(Jan. ),pp. {.
`[]Hecht,M.S.FlowAnalysisofComputerPrograms.ElsevierNorth-Holland, .
`[]Hopcroft,J.E.,andUllman,J.D.
`IntroductiontoAutomataTheory,Languages,andComputation.
`Addison-Wesley,Reading,Mass.,  .
`[]Horwitz,S.,Pfeiffer,P.,andReps,T.Dependenceanalysisforpointervariables.InProceedingsofthe
`ACMSIGPLANSymposiumonCompilerConstruction(June  ),pp.{.
`[]Kam,J.B.,andUllman,J.D.Global(cid:13)owanalysisanditerativealgorithms.JournaloftheACM ,
`( ), {  .
`[]Kam,J.B.,andUllman,J.D.Monotonedata(cid:13)owanalysisframeworks.ActaInformatica( ), { .
`[ ]Kildall,G.Auni(cid:12)edapproachtoglobalprogramoptimization.InConferenceRecordoftheACMSymposium
`onPrinciplesofProgrammingLanguages(Jan.  ),pp. {.
`[ ]Landi,W.InterproceduralAliasinginthePresenceofPointers.PhDthesis,RutgersUniversity,Jan. .
`LCSR-TR- .
`[ ]Landi,W.,andRyder,B.G.Pointer-inducedaliasing:Aproblemclassi(cid:12)cation.InConferenceRecordofthe
`EighteenthAnnualACMSymposiumonPrinciplesofProgrammingLanguages(Jan. ),pp. { .
`[ ]Larus,J.R.RestructuringSymbolicProgramsforConcurrentExecutiononMultiprocessors.PhDthesis,
`UniversityofCaliforniaBerkeley,May  .
`[ ]Larus,J.R.,andHilfinger,P.N.Detectingcon(cid:13)ictsbetweenstructureaccesses.InProceedingsoftheSIG-
`PLAN'ConferenceonProgrammingLanguageDesignandImplementation(July ),pp. { .SIGPLAN
`NOTICES,Vol. ,No..
`[ ]Myers,E.M.Apreciseinterproceduraldata(cid:13)owalgorithm.InConferenceRecordoftheEighthAnnualACM
`SymposiumonPrinciplesofProgrammingLanguages(Jan.  ),pp. { .
`[ ]Ullman,J.D.Fastalgorithmsfortheeliminationofcommonsubexpressions.ActaInformatica, (  ),
` { .
`[ ]Wegman,M.,andZadeck,F.K.Constantpropagationwithconditionalbranches.ACMTransactionson
`ProgrammingLanguagesandSystems ,(Apr. ),  { .
`AModi(cid:12)cationtosinglylinkedlist
`Themachinereduce(Figure )ismodi(cid:12)edtoconstructaprogramwithonlyasinglylinkedlist
`andthatstillsatisfyTheorem . andTheorem .asfollows:
`(cid:15)Removeprev(cid:12)eldfromstructtape.Alsoremoveallstatementsdealingwithprev.
`(cid:15)Addthe(cid:12)eld\int(cid:3)(cid:3)notat"totypestructtape.Pointnotattoyeswheneveranew
`tapeelementiscreated.
` 
`
`Columbia Ex 2038-15
`Symantec v Columbia
`IPR2015-00375
`
`

`
`(cid:15)Addavariable\structtape(cid:3)front"whichwillalwayspointtothe(cid:12)rst(leftmost)element
`ofthelinkedlist.
`(cid:15)Immediatelybeforethewhileloopthatsimulates(cid:14)addthestatement:
`tapehead(cid:0)>notat=&no
`Ingeneral,thenotat(cid:12)eldofthelinkedlistrepresentingthetapepointstoyesexceptat
`tapeheadwhereitpointstono.
`(cid:15)Replacethecodeforwhend=Rintheloopwith:
`#ifd=R
`tapehead->notat=&yes;
`tapehead=tapehead->next;
`tapehead->notat=&no;
`#endif
`(cid:15)Finally,replacethecodeforwhend=Lintheloopwith:
`#ifd=L
`tapehead=front;
`while(nextbool== )f
`ADDTOEND/(cid:3)ThecodeforADDTOENDhere(cid:3)/
`tapehead=tapehead->next;
`g/(cid:3)tapehead->next->notatpointstoyesandthis
`(cid:3)assignmentsignalsinvalidsimulationunless
`(cid:3)tapeheadisoneLEFTofwhereitwas(cid:3)/
`(cid:3)(tapehead->next->notat)=&notvalid;
`tapehead->next->notat=&yes;
`tapehead->notat=&no;
`#endif
`BPolynomialpathsonly
`Whenonlypolynomiallengthpathsareconsidered,MayAliasandthecomplementofMustAlias
`areNPcompleteforprogramsonwhichallpathsareexecutablegiventhelanguagehasdynamically
`allocatedrecursivedatastructures,loops,andif-statements.TheseproblemsareinNPbecause
`wecannondeterministicallygenerateanexecutionoftheprogramandthensimulatetheexecution
`intimelinearinthelengthoftheexecution(asimilarargumentisin[ ]).Fromtheprogramstore
` 
`
`Columbia Ex 2038-16
`Symantec v Columbia
`IPR2015-00375
`
`

`
`wecaneasilyanswerquestionsaboutMayAliasandthecomplementofMustAlias.Thisargument
`worksforStaticAnalysisproblemswhichcanbenondeterministicallyansweredforagivenexecution
`inapolynomialamountoftime,inthesizeoftheprogramandlengthoftheexecutionpath,from
`theprogram,symboltable,andapossiblyaugmentedprogramstore.However,theaugmented
`storemustbepolynomialinthesizeoftheoriginalstore;forexample,[].
`ThefactthatMayAliasandthecomplementofMustAliasarebothNPhardunderthisnew
`assumptionisevidentbecauseouroriginalproofsofthisclaim[ , ]donotcontainanyloops
`andonlylinearlengthpathsexist.SincemostStaticAnalysesarein(cid:13)uencedbyaliases,theyare
`alsoNPhard.
`
` 
`
`Columbia Ex 2038-17
`Symantec v Columbia
`IPR2015-00375