A Feasibility Study The Succinct Solver v2.0, XSB

AFeasibilityStudyTheSuccinctSolverv2.0,XSBPrologv2.6,andFlow-LogicBasedProgramAnalysisforCarmelAuthors:HenrikPilegaard([e-mail])Date:September30,2003Number:SECSAFE-IMM-008-1.0Classication:InternalAbstract.WeperformadirectcomparisonoftheSuccinctSolverv2.0andXSBPro-logv2.6basedonexperimentswithControlFlowAnalysesofscalableDiscretionaryAmbientprogramsandCarmelprograms.TofacilitatethiscomparisonweexpandALFPclausesacceptedbytheSuccinctSolverintomoregeneralNormalclausesac-ceptedbybothsolversandruntheexperimentsforallthreepossiblecombinationsofinputandsolver.ThisallowsthesolverstobetestedonevengroundandenablesthereuseofexistinganalysesandtheircorrespondingALFPconstraintgenerators.TheperformanceoftheSuccinctSolverisatworstasmallconstantfactorworsethanXSBProlog.InoptimumcasestheSuccinctSolveroutperformsXSBPrologbyhavingasubstantiallylowerasymptoticcomplexity.Contents1Introduction32SolverTechnologies52.1TheSuccinctSolver............................52.2XSBProlog.................................62.3TranslatingALFPProgramstoNormalPrograms...........93TestSetupandProcedure123.1InvestigatedFactors............................123.2TestSuite..................................143.3TimingtheExperiments..........................143.4PresentingtheResults...........................144DiscretionaryAmbients:ScalableRouterPrograms164.1TheLanguage................................164.2TheAnalyses................................164.3RepresentationofConstraints.......................174.4TestPrograms...............................184.5TestResults.................................19SupportedinpartbytheInformationSocietyTechnologiesprogrammeoftheEuropeanCommis-sion,FutureandEmergingTechnologies,undertheIST-1999-29075projectSecSafe;andtheDanishSNF-projectLoST21-02-0507.1|INTERNAL|4.6Discussion..................................235Carmel:Demoney-TheElectronicJavaCardPurse255.1TheLanguage................................255.2TheAnalysis................................255.3ConstraintsandTranslation........................255.4TestPrograms...............................265.5TestResults.................................275.6Discussion..................................326Conclusion33A0-CFAforthe1(m)Programs37A.1IndividualSolvers..............................37A.2SolversCompared.............................38B0-CFAforthes(m)Programs39B.1SchematicDrawing.............................39B.2ProblemInstanceCodeform=2.....................39B.3IndividualSolvers..............................40B.4SolversCompared.............................41C0-CFAforthelvg(m)Programs42C.1IndividualSolvers..............................42C.2SolversCompared.............................43D0-CFAforthesph(m)Programs44D.1IndividualSolvers..............................44D.2SolversCompared.............................45EClosureConditionExamples46E.1da02.....................................46E.2da07.....................................47E.3da07-HornExpanded..........................48FCarmelXSBRuns:demoney49GCarmelXSBRuns:demoney-local50HCarmelXSBRuns:jc212api52ICarmelXSBRuns:API54JCarmelXSBRuns:demoney-impl-api56SECSAFE-IMM-008-1.02|INTERNAL|1IntroductionStaticanalysisofprogramsisoneoftheformalmethodsforprogramvericationthatenjoyswidespreaduse.Formallytheapproachliessomewherebetweenautomatedtheoremprovingandmodelcheckingincorporatingthebestofbothworlds.Analysesareoftenconstructedinatwo-phaseprocess.Therstphaseconcernstheextractionofsetsofconstraintsfromprogramsandthesecondthesolvingofthesesets.Abenetofthisapproachisthatsolvertechnologymaybesharedamongappli-cationsinavarietyofprogramminglanguagesandamongmanyclassesofproblems.Thisemphasizesthefactthatthesolvertechnologyisusually,ifnotalways,thelim-itingfactorand,thus,thatitisimportanttoexamineandcomparedierentsolvertechnologiesinordertominimizethelimitationsimposedbythechoiceoftechnology.AstheuseofstaticanalysisforvericationofJavaCardprogramsisthecornerstoneoftheSecSafeproject,itisclearlyrelevanttoidentifyandevaluateappropriatetechnologies.Thus,thisdocumentinpartconstitutesacomparisonofv2.0oftheSuccinctSolver(SuccinctSolver)ofNielsonandSeidl[10]tov2.6ofthegeneralpurposetabledPrologsystemXSB[15][13],withrespecttotheirusabilityforFlow-logicbasedstaticanalysisofprograms.ThealgorithmicfoundationoftheSuccinctSolverwasdesignedtogivestate-of-the-artasymptoticworst-caseperformancewhileallowingforevenbetterperformanceinbenigncases.Thiswasaconsciousdecisionmotivatedbythebeliefthatstaticanalysisgenerallygivesrisetoproblemswheretheworst-casecomplexityisnotin-herent.Theresultingsolverimplementationembodiesafunctionalimplementation(inNewJerseySML)ofanalgorithmthatcomputesstablemodelsofformulasfromthealternation-freefragmentofLeastFix-pointLogic(ALFPformulas)withthesamecomplexitywithwhichtheyarechecked.Theotherinvestigatedsolver,XSBProlog,hasnottoourknowledgebeende-signedwithsimilarconsiderationsinmind.Still,theXSBPrologsystemisknowntoconstituteahighlyoptimizedlow-levelimplementationofanalgorithmthataimstoexhibitgooddatacomplexitywhencomp