From e8352f0bd13a2999064eece8af4214c540fbc156 Mon Sep 17 00:00:00 2001 From: Alexander Chebaturkin Date: Thu, 14 Jul 2011 02:47:34 +0400 Subject: [PATCH] The base architecture for code-contracts analysis --- man/cccheck.1 | 67 + .../Mono.CodeContracts-net_4_0.csproj | 415 +++- .../CodeVisitor.cs | 81 + .../DefaultNodeVisitor.cs | 467 +++++ .../IAggregateVisitor.cs | 35 + .../ICodeConsumer.cs | 35 + .../IExpressionILVisitor.cs | 38 + .../IILVisitor.cs | 102 + .../ILVisitorBase.cs | 371 ++++ .../IMethodCodeConsumer.cs | 35 + .../ISymbolicExpressionVisitor.cs | 34 + .../ISyntheticILVisitor.cs | 42 + .../NodeInspector.cs | 436 +++++ .../NodeVisitor.cs | 46 + .../ValueCodeVisitor.cs | 36 + .../ArrayTypeNode.cs | 38 + .../AssemblyNode.cs | 86 + .../AssignmentStatement.cs | 46 + .../BinaryExpression.cs | 56 + .../BinaryOperator.cs | 64 + .../Mono.CodeContracts.Static.AST/Block.cs | 50 + .../BlockExpression.cs | 50 + .../BodyParser.cs | 856 +++++++++ .../Mono.CodeContracts.Static.AST/Branch.cs | 64 + .../CatchFilter.cs | 45 + .../Mono.CodeContracts.Static.AST/Class.cs | 66 + .../Construct.cs | 46 + .../CoreSystemTypes.cs | 206 ++ .../EndFinally.cs | 35 + .../Mono.CodeContracts.Static.AST/Ensures.cs | 47 + .../ExceptionHandler.cs | 43 + .../Expression.cs | 48 + .../ExpressionStatement.cs | 48 + .../FaultHandler.cs | 42 + .../Mono.CodeContracts.Static.AST/Field.cs | 107 ++ .../Mono.CodeContracts.Static.AST/Literal.cs | 55 + .../Mono.CodeContracts.Static.AST/Local.cs | 65 + .../Mono.CodeContracts.Static.AST/Member.cs | 46 + .../MemberBinding.cs | 58 + .../Mono.CodeContracts.Static.AST/Method.cs | 345 ++++ .../MethodCall.cs | 57 + .../MethodContract.cs | 66 + .../MethodContractElement.cs | 39 + .../Mono.CodeContracts.Static.AST/Module.cs | 69 + .../NaryExpression.cs | 45 + .../Mono.CodeContracts.Static.AST/Node.cs | 38 + .../Mono.CodeContracts.Static.AST/NodeType.cs | 105 + .../OperatorExtensions.cs | 58 + .../Parameter.cs | 85 + .../Mono.CodeContracts.Static.AST/Property.cs | 143 ++ .../Reference.cs | 56 + .../Mono.CodeContracts.Static.AST/Requires.cs | 47 + .../Mono.CodeContracts.Static.AST/Return.cs | 47 + .../Statement.cs | 40 + .../Mono.CodeContracts.Static.AST/This.cs | 58 + .../Mono.CodeContracts.Static.AST/TypeNode.cs | 335 ++++ .../UnaryExpression.cs | 55 + .../UnaryOperator.cs | 47 + .../Mono.CodeContracts.Static.AST/Variable.cs | 36 + .../AnalysisDriver.cs | 62 + .../BasicAnalysisDriver.cs | 66 + .../BasicMethodDriver.cs | 137 ++ .../CodeContractsAnalysisDriver.cs | 146 ++ .../IBasicAnalysisDriver.cs | 38 + .../IBasicMethodDriver.cs | 42 + .../IMethodAnalysis.cs | 40 + .../IMethodAnalysisFixPoint.cs | 37 + .../IMethodDriver.cs | 53 + .../IMethodResult.cs | 37 + .../FullExpressionDecoder.cs | 157 ++ .../IFullExpressionDecoder.cs | 49 + .../QueryVisitor.cs | 79 + .../VisitorForIsBinaryExpression.cs | 61 + .../VisitorForIsInst.cs | 58 + .../VisitorForIsNull.cs | 49 + .../VisitorForIsUnaryExpression.cs | 56 + .../VisitorForSizeOf.cs | 54 + .../VisitorForUnderlyingVariable.cs | 88 + .../VisitorForValueOf.cs | 64 + .../VisitorForVariable.cs | 52 + .../VisitorForVariablesIn.cs | 100 + .../BinaryExpr.cs | 98 + .../ConstExpr.cs | 85 + .../Expr.cs | 57 + .../IsInstExpr.cs | 87 + .../NullExpr.cs | 79 + .../SizeOfExpr.cs | 85 + .../UnaryExpr.cs | 92 + .../AnalysisDecoder.cs | 98 + .../AssumeDecoder.cs | 100 + .../ExprDomain.cs | 121 ++ .../ExpressionAnalysisFacade.cs | 88 + .../ExpressionDecoder.cs | 165 ++ .../ExpressionDecoderAdapter.cs | 57 + .../ExpressionPrinterFactory.cs | 132 ++ .../ILDecoderAdapter.cs | 411 ++++ .../ValueAnalysis.cs | 122 ++ .../AccessPathFilter.cs | 112 ++ .../IVisibilityCheck.cs | 35 + .../MethodCallPathElement.cs | 69 + .../ParameterPathElement.cs | 67 + .../PathElement.cs | 63 + .../PathElementBase.cs | 43 + .../PathElement`1.cs | 205 ++ .../PathExtensions.cs | 110 ++ .../SpecialPathElement.cs | 103 + .../SpecialPathElementKind.cs | 34 + .../AbstractDomainUpdate.cs | 87 + .../EdgeUpdate.cs | 97 + .../EliminateEdgeUpdate.cs | 79 + .../EqualityPair.cs | 64 + .../EqualityUpdate.cs | 60 + .../IMergeInfo.cs | 53 + .../MergeInfo.cs | 516 +++++ .../MultiEdge.cs | 71 + .../MultiEdgeUpdate.cs | 60 + .../SymGraph.cs | 908 +++++++++ .../SymGraphTerm.cs | 62 + .../Update.cs | 53 + .../AbstractType.cs | 174 ++ .../AnalysisDecoder.cs | 1262 ++++++++++++ .../Domain.cs | 1635 ++++++++++++++++ .../FunctionsTable.cs | 185 ++ .../HeapAnalysis.cs | 254 +++ .../IAbstractDomainForEGraph.cs | 35 + .../IConstantInfo.cs | 33 + .../ISymGraph.cs | 63 + .../LabeledSymbol.cs | 64 + .../MethodWrapper.cs | 48 + .../ParameterWrapper.cs | 72 + .../StackToSymbolicAdapter.cs | 572 ++++++ .../SymFunction.cs | 78 + .../SymValue.cs | 79 + .../SymbolicValue.cs | 99 + .../TypeCache.cs | 57 + .../ValueContextProvider.cs | 184 ++ .../ValueDecoder.cs | 91 + .../Wrapper.cs | 191 ++ .../Analysis.cs | 418 ++++ .../Domain.cs | 58 + .../ExpressionAssertDischarger.cs | 133 ++ .../ExpressionAssumeDecoder.cs | 153 ++ .../NonNullAnalysisFacade.cs | 53 + .../APCMap.cs | 92 + .../SequenceGenerator.cs | 67 + .../StackDecoder.cs | 606 ++++++ .../StackDepthFactory.cs | 41 + .../StackDepthProvider.cs | 707 +++++++ .../StackInfo.cs | 127 ++ .../StackInfo`1.cs | 82 + .../CodeLayer.cs | 90 + .../CodeLayerFactory.cs | 57 + .../ICodeLayer.cs | 49 + .../IExpressionContext.cs | 50 + .../IExpressionContextProvider.cs | 34 + .../ILPrinter.cs | 33 + .../IMethodContext.cs | 41 + .../IMethodContextProvider.cs | 33 + .../IStackContext.cs | 35 + .../IStackContextProvider.cs | 33 + .../IValueContext.cs | 44 + .../IValueContextProvider.cs | 33 + .../PrinterFactory.cs | 469 +++++ .../ContractExtractor.cs | 234 +++ .../ContractNodes.cs | 221 +++ .../GatherLocals.cs | 91 + .../HelperMethods.cs | 332 ++++ .../RepresentationForAttribute.cs | 48 + .../AssumeBlock.cs | 57 + .../BlockBase.cs | 42 + .../BlockWithLabels.cs | 110 ++ .../CatchFilterEntryBlock.cs | 38 + .../EnsuresBlock.cs | 215 +++ .../EntryBlock.cs | 47 + .../EntryExitBlock.cs | 43 + .../LabelAdapter.cs | 394 ++++ .../MethodCallBlock.cs | 67 + .../NewObjCallBlock.cs | 44 + .../BlockBuilder.cs | 195 ++ .../BlockStartGatherer.cs | 164 ++ .../EnsuresFactory.cs | 73 + .../RequiresFactory.cs | 83 + .../SimpleSubroutineBuilder.cs | 100 + .../SubroutineBuilder.cs | 193 ++ .../SubroutineFactory.cs | 75 + .../SubroutineWithHandlersBuilder.cs | 221 +++ .../EnsuresSubroutine.cs | 152 ++ .../FaultFinallySubroutineBase.cs | 52 + .../FaultSubroutine.cs | 43 + .../FinallySubroutine.cs | 43 + .../MethodContractSubroutine.cs | 63 + .../MethodSubroutine.cs | 136 ++ .../OldScanStateMachine.cs | 160 ++ .../OldValueSubroutine.cs | 85 + .../RequiresSubroutine.cs | 85 + .../SimpleSubroutine.cs | 58 + .../SubroutineBase.cs | 782 ++++++++ .../SubroutineFacade.cs | 130 ++ .../SubroutineWithHandlers.cs | 208 ++ .../APC.cs | 289 +++ .../APCDecoder.cs | 105 + .../CFGBlock.cs | 83 + .../ContractFilteredCFG.cs | 163 ++ .../ControlFlowGraph.cs | 194 ++ .../Edge.cs | 52 + .../EdgeMap.cs | 222 +++ .../EdgeTag.cs | 64 + .../EdgeTagExtensions.cs | 36 + .../EdgeVisitor.cs | 32 + .../ICFG.cs | 64 + .../IConstantInfo.cs | 35 + .../IHandlerFilter.cs | 36 + .../IMethodInfo.cs | 35 + .../IStackInfo.cs | 33 + .../RemoveBranchDelegator.cs | 420 ++++ .../Subroutine.cs | 186 ++ .../SubroutineKind.cs | 41 + .../DataFlowAnalysisBase.cs | 164 ++ .../EdgeBasedWidening.cs | 46 + .../EdgeConverter.cs | 31 + .../ForwardAnalysis.cs | 151 ++ .../ForwardDataFlowAnalysisBase.cs | 155 ++ .../IAnalysis.cs | 45 + .../IFixPointInfo.cs | 34 + .../IWidenStrategy.cs | 35 + .../Joiner.cs | 33 + .../StepWidening.cs | 60 + .../AbstractWorkList.cs | 75 + .../DecoratorHelper.cs | 67 + .../DepthFirst.cs | 229 +++ .../DoubleDictionary.cs | 90 + .../DoubleImmutableMap.cs | 126 ++ .../Dummy.cs | 42 + .../EdgeVisitor.cs | 31 + .../GraphWrapper.cs | 55 + .../IGraph.cs | 36 + .../IImmutableIntMap.cs | 46 + .../IImmutableMap.cs | 48 + .../IImmutableSet.cs | 48 + .../IIndexable.cs | 34 + .../ITypedProperties.cs | 35 + .../IWorkList.cs | 35 + .../ImmutableIntKeyMap.cs | 114 ++ .../ImmutableIntMap.cs | 146 ++ .../ImmutableMap.cs | 143 ++ .../ImmutableSet.cs | 169 ++ .../ImmutableSetExtensions.cs | 51 + .../Indexable.cs | 54 + .../LispList.cs | 131 ++ .../LispListExtensions.cs | 116 ++ .../Optional.cs | 46 + .../Pair.cs | 71 + .../PriorityQueue.cs | 110 ++ .../TypedKey.cs | 57 + .../TypedProperties.cs | 60 + .../VisitStatus.cs | 34 + .../WorkList.cs | 61 + .../Extensions.cs | 11 + .../EnvironmentDomain.cs | 221 +++ .../FlatDomain.cs | 196 ++ .../IAbstractDomain.cs | 80 + .../SetDomain.cs | 157 ++ .../CodeContractDecoder.cs | 86 + .../CodeProviderImpl.cs | 543 ++++++ .../ICodeProvider.cs | 11 + .../IContractProvider.cs | 44 + .../IILDecoder.cs | 41 + .../IMetaDataProvider.cs | 169 ++ .../IMethodCodeProvider.cs | 49 + .../MetaDataProvider.cs | 692 +++++++ .../AssertionFinder.cs | 140 ++ .../BasicFacts.cs | 135 ++ .../BoxedExpression.cs | 1688 +++++++++++++++++ .../BoxedExpressionExtensions.cs | 56 + .../ComposedFactQuery.cs | 184 ++ .../ConstantPropagationFactQuery.cs | 212 +++ .../IFactBase.cs | 37 + .../IFactQuery.cs | 42 + .../SimpleLogicInference.cs | 115 ++ .../Mono.CodeContracts.Static/CheckOptions.cs | 44 + .../Mono.CodeContracts.Static/CheckResults.cs | 68 + .../Mono.CodeContracts.Static/Checker.cs | 136 ++ .../Mono.CodeContracts.Static/DebugOptions.cs | 33 + .../Mono.CodeContracts.Static/ProofOutcome.cs | 36 + .../ProofOutcomeExtensions.cs | 73 + .../Mono.CodeContracts.dll.sources | 284 ++- mcs/tools/Makefile | 1 + mcs/tools/cccheck/Makefile | 9 + mcs/tools/cccheck/Program.cs | 66 + mcs/tools/cccheck/cccheck.exe.sources | 3 + 290 files changed, 37226 insertions(+), 69 deletions(-) create mode 100644 man/cccheck.1 create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/CodeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/DefaultNodeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IAggregateVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ICodeConsumer.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IExpressionILVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IILVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ILVisitorBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IMethodCodeConsumer.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ISymbolicExpressionVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ISyntheticILVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/NodeInspector.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/NodeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ValueCodeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ArrayTypeNode.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/AssemblyNode.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/AssignmentStatement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BinaryExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BinaryOperator.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Block.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BlockExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BodyParser.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Branch.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/CatchFilter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Class.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Construct.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/CoreSystemTypes.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/EndFinally.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Ensures.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ExceptionHandler.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Expression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ExpressionStatement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/FaultHandler.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Field.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Literal.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Local.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Member.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MemberBinding.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Method.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodCall.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodContract.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodContractElement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Module.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/NaryExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Node.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/NodeType.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/OperatorExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Parameter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Property.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Reference.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Requires.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Return.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Statement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/This.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/TypeNode.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/UnaryExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/UnaryOperator.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Variable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/AnalysisDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/BasicAnalysisDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/BasicMethodDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/CodeContractsAnalysisDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IBasicAnalysisDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IBasicMethodDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodAnalysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodAnalysisFixPoint.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodDriver.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodResult.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/FullExpressionDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/IFullExpressionDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/QueryVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsBinaryExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsInst.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsNull.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsUnaryExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForSizeOf.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForUnderlyingVariable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForValueOf.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForVariable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForVariablesIn.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/BinaryExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/ConstExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/Expr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/IsInstExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/NullExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/SizeOfExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/UnaryExpr.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/AnalysisDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/AssumeDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExprDomain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionAnalysisFacade.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionDecoderAdapter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionPrinterFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ILDecoderAdapter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ValueAnalysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/AccessPathFilter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/IVisibilityCheck.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/MethodCallPathElement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/ParameterPathElement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElementBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElement`1.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/SpecialPathElement.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/SpecialPathElementKind.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/AbstractDomainUpdate.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EdgeUpdate.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EliminateEdgeUpdate.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EqualityPair.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EqualityUpdate.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/IMergeInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MergeInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MultiEdge.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MultiEdgeUpdate.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/SymGraph.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/SymGraphTerm.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/Update.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/AbstractType.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/AnalysisDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/Domain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/FunctionsTable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/HeapAnalysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/IAbstractDomainForEGraph.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/IConstantInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ISymGraph.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/LabeledSymbol.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/MethodWrapper.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ParameterWrapper.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/StackToSymbolicAdapter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymFunction.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymValue.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymbolicValue.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/TypeCache.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ValueContextProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ValueDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/Wrapper.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/Analysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/Domain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/ExpressionAssertDischarger.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/ExpressionAssumeDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/NonNullAnalysisFacade.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/APCMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/SequenceGenerator.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDepthFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDepthProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackInfo`1.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/CodeLayer.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/CodeLayerFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/ICodeLayer.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IExpressionContext.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IExpressionContextProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/ILPrinter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IMethodContext.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IMethodContextProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IStackContext.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IStackContextProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IValueContext.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IValueContextProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/PrinterFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/ContractExtractor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/ContractNodes.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/GatherLocals.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/HelperMethods.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/RepresentationForAttribute.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/AssumeBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/BlockBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/BlockWithLabels.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/CatchFilterEntryBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EnsuresBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EntryBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EntryExitBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/LabelAdapter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/MethodCallBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/NewObjCallBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/BlockBuilder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/BlockStartGatherer.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/EnsuresFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/RequiresFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SimpleSubroutineBuilder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineBuilder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineFactory.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineWithHandlersBuilder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/EnsuresSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FaultFinallySubroutineBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FaultSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FinallySubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/MethodContractSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/MethodSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/OldScanStateMachine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/OldValueSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/RequiresSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SimpleSubroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineFacade.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineWithHandlers.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/APC.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/APCDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/CFGBlock.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ContractFilteredCFG.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ControlFlowGraph.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Edge.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTag.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTagExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ICFG.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IConstantInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IHandlerFilter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IMethodInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IStackInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/RemoveBranchDelegator.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Subroutine.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/SubroutineKind.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/DataFlowAnalysisBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeBasedWidening.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeConverter.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardDataFlowAnalysisBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IAnalysis.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IFixPointInfo.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IWidenStrategy.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/Joiner.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/StepWidening.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/AbstractWorkList.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DecoratorHelper.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DepthFirst.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DoubleDictionary.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DoubleImmutableMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Dummy.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/EdgeVisitor.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/GraphWrapper.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IGraph.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableIntMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableSet.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IIndexable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ITypedProperties.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IWorkList.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableIntKeyMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableIntMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableMap.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableSet.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableSetExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Indexable.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/LispList.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/LispListExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Optional.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Pair.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/PriorityQueue.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/TypedKey.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/TypedProperties.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/VisitStatus.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/WorkList.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Extensions/Extensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/EnvironmentDomain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/FlatDomain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/IAbstractDomain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/SetDomain.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/CodeContractDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/CodeProviderImpl.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/ICodeProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IContractProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IILDecoder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IMetaDataProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IMethodCodeProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/MetaDataProvider.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/AssertionFinder.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BasicFacts.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpression.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpressionExtensions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ComposedFactQuery.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ConstantPropagationFactQuery.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactBase.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactQuery.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/SimpleLogicInference.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/CheckOptions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/CheckResults.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/Checker.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/DebugOptions.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/ProofOutcome.cs create mode 100644 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/ProofOutcomeExtensions.cs create mode 100644 mcs/tools/cccheck/Makefile create mode 100644 mcs/tools/cccheck/Program.cs create mode 100644 mcs/tools/cccheck/cccheck.exe.sources diff --git a/man/cccheck.1 b/man/cccheck.1 new file mode 100644 index 00000000000..aead19a58d0 --- /dev/null +++ b/man/cccheck.1 @@ -0,0 +1,67 @@ +.\" +.\" cccheck manual page. +.\" Copyright (C) 2011 Alexander Chebaturkin +.\" Author: +.\" Alexander Chebaturkin (chebaturkin@gmail.com) +.\" +.TH Mono "cccheck" +.SH NAME +cccheck \- Perform static code contracts verification for CLR assemblies. +.SH SYNOPSIS +.PP +.B cccheck --assembly= [options] +.SH DESCRIPTION +Perform static code contracts verification to find bugs and inconsistences +between code and specification. This includes non-null, integer analyses. +.PP +The assembly must have been built with the symbol CONTRACTS_FULL defined, +otherwise the calls to the contract methods will have been removed +by the compiler. +.PP +Currently only Contract.Assume() and Contract.Assert() methods are +supported. Only non-null analysis is supported, the consecutive analyses are +in development. An error message will be shown if cccheck is unable to process +all or some of the methods of specified assembly. +.SH CONFIGURATION OPTIONS +.TP +.I "--assembly " +The assembly to perform static verification. +.TP +.I "--debug" +Shows debug information about process of proving the assertions. It shows +four layers of abstraction, raw layer, stack layer, heap layer, +and substituted expression level. +.TP +.I "--method=" +String for finding method. It filters all methods in assembly where method +name has this parameter as a substring. +.TP +.I "--help" +Show help for cccheck, listing configuration options. + +.SH EXAMPLES +.TP +Suppose you have a method: + void Method() { + object x = null; + int y = 1; + if (y % 2 == 1) + x = new object(); + else + x = new string(); + + Contract.Assert(x != null); +} + +After the verification the tool will have results in following format: +"Assertion at : [Subroutine: Block PC ] : + is (true|false|unproven|unreachable)". +(PC is a program counter) + +.SH AUTHOR +Written by Alexander Chebaturkin +.SH COPYRIGHT +Copyright 2011 Alexander Chebaturkin. +Released under MIT license. +.SH WEB SITE +Visit http://www.mono-project.com for details diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts-net_4_0.csproj b/mcs/class/Mono.CodeContracts/Mono.CodeContracts-net_4_0.csproj index dfc6f823036..f7bccdc7c69 100644 --- a/mcs/class/Mono.CodeContracts/Mono.CodeContracts-net_4_0.csproj +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts-net_4_0.csproj @@ -1,5 +1,5 @@ - - + + Debug AnyCPU @@ -11,11 +11,10 @@ ./../../class/lib/net_4_0 NET_1_1;NET_2_0;NET_3_0;NET_3_5;NET_4_0 true - Properties mscorlib Mono.CodeContracts - v3.5 + v4.0 512 @@ -41,44 +40,326 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {2})", this.From, this.Tag, this.To); + } + + public Edge Reversed () + { + return new Edge (this.To, this.From, this.Tag); + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeMap.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeMap.cs new file mode 100644 index 00000000000..8cbe88c1255 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeMap.cs @@ -0,0 +1,222 @@ +// +// EdgeMap.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.ControlFlow { + class EdgeMap : IEnumerable>, IGraph { + private readonly List> edges; + + public EdgeMap (List> edges) + { + this.edges = edges; + Resort (); + } + + public ICollection> this [CFGBlock node] + { + get { return new Successors (this, FindStartIndex (node)); } + } + + #region IEnumerable> Members + public IEnumerator> GetEnumerator () + { + return this.edges.GetEnumerator (); + } + + IEnumerator IEnumerable.GetEnumerator () + { + return GetEnumerator (); + } + #endregion + + #region IGraph Members + IEnumerable IGraph.Nodes + { + get { throw new InvalidOperationException(); } + } + + IEnumerable> IGraph.Successors (CFGBlock node) + { + return this [node]; + } + #endregion + + public EdgeMap Reverse () + { + var newEdges = new List> (this.edges.Count); + + newEdges.AddRange (this.edges.Select (edge => edge.Reversed ())); + + return new EdgeMap (newEdges); + } + + private static int CompareFirstBlockIndex (Edge edge1, Edge edge2) + { + int cmp = edge1.From.Index - edge2.From.Index; + if (cmp == 0) + cmp = edge1.To.Index - edge2.To.Index; + + return cmp; + } + + private int FindStartIndex (CFGBlock from) + { + //binary search + int l = 0; + int r = this.edges.Count; + while (l < r) { + int median = (l + r)/2; + int medianBlockIndex = this.edges [median].From.Index; + + if (medianBlockIndex == from.Index) { + while (median > 0 && this.edges [median - 1].From.Index == medianBlockIndex) + --median; + return median; + } + + if (medianBlockIndex < from.Index) + l = median + 1; + else + r = median; + } + + return this.edges.Count; + } + + public void Filter (Predicate> keep) + { + var notKeepEdges = new List (); + for (int i = 0; i < this.edges.Count; i++) { + if (!keep (this.edges [i])) + notKeepEdges.Add (i); + } + + if (notKeepEdges.Count == 0) + return; + + int ix = 0; + foreach (int i in notKeepEdges) { + this.edges.RemoveAt (i - ix); + ix++; + } + } + + public void Resort () + { + this.edges.Sort (CompareFirstBlockIndex); + } + + #region Nested type: Successors + private struct Successors : ICollection> { + private readonly int start_index; + private readonly EdgeMap underlying; + + public Successors (EdgeMap underlying, int startIndex) + { + this.underlying = underlying; + this.start_index = startIndex; + } + + #region ICollection> Members + public IEnumerator> GetEnumerator () + { + List> edges = this.underlying.edges; + if (this.start_index < edges.Count) { + int index = this.start_index; + int blockIndex = edges [index].From.Index; + do { + yield return new Pair (edges [index].Tag, edges [index].To); + ++index; + } while (index < edges.Count && edges [index].From.Index == blockIndex); + } + } + + IEnumerator IEnumerable.GetEnumerator () + { + return GetEnumerator (); + } + + public void Add (Pair item) + { + throw new InvalidOperationException (); + } + + public void Clear () + { + throw new InvalidOperationException (); + } + + public bool Contains (Pair item) + { + throw new NotImplementedException (); + } + + public void CopyTo (Pair[] array, int arrayIndex) + { + throw new NotImplementedException (); + } + + public bool Remove (Pair item) + { + throw new InvalidOperationException (); + } + + public int Count + { + get + { + int index = this.start_index; + List> edges = this.underlying.edges; + if (index >= edges.Count) + return 0; + int blockIndex = edges [index].From.Index; + + int count = 0; + do { + ++count; + ++index; + } while (index < edges.Count && edges [index].From.Index == blockIndex); + + return count; + } + } + + public bool IsReadOnly + { + get { return true; } + } + #endregion + } + #endregion + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTag.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTag.cs new file mode 100644 index 00000000000..62e10488c03 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTag.cs @@ -0,0 +1,64 @@ +// +// EdgeTag.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; + +namespace Mono.CodeContracts.Static.ControlFlow { + [Flags] + enum EdgeTag : uint { + None = 0, + FallThroughReturn = 1, + Branch = 1 << 1, + Return = 1 << 2, + EndSubroutine = 1 << 3, + True = 1 << 4, + False = 1 << 5, + FallThrough = 1 << 6, + Entry = 1 << 7, + AfterNewObj = 1 << 8 | AfterMask, + AfterCall = 1 << 9 | AfterMask, + Exit = 1 << 10, + Finally = 1 << 11, + Inherited = 1 << 12 | InheritedMask, + BeforeCall = 1 << 13 | BeforeMask, + BeforeNewObj = 1 << 14 | BeforeMask, + Requires = 1 << 15, + Assume = 1 << 16, + Assert = 1 << 17, + Invariant = 1 << 18, + OldManifest = 1 << 19 | OldMask, + Old = 1 << 20 | OldMask, + EndOld = 1 << 21, + + BeforeMask = 1 << 22, + AfterMask = 1 << 23, + InheritedMask = 1 << 24, + ExtraMask = 1 << 25, + OldMask = 1 << 26, + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTagExtensions.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTagExtensions.cs new file mode 100644 index 00000000000..fc136dad64d --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTagExtensions.cs @@ -0,0 +1,36 @@ +// +// EdgeTagExtensions.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +namespace Mono.CodeContracts.Static.ControlFlow { + static class EdgeTagExtensions { + public static bool Is (this EdgeTag current, EdgeTag mask) + { + return (current & mask) != EdgeTag.None; + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeVisitor.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeVisitor.cs new file mode 100644 index 00000000000..ef28638c1e8 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeVisitor.cs @@ -0,0 +1,32 @@ +// +// EdgeVisitor.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +namespace Mono.CodeContracts.Static.ControlFlow +{ + delegate void EdgeVisitor(Node source, Info info, Node target); +} \ No newline at end of file diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ICFG.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ICFG.cs new file mode 100644 index 00000000000..89869ce9bc9 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ICFG.cs @@ -0,0 +1,64 @@ +// +// ICFG.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.Collections.Generic; +using System.IO; +using Mono.CodeContracts.Static.Analysis; +using Mono.CodeContracts.Static.DataStructures; +using Mono.CodeContracts.Static.Providers; + +namespace Mono.CodeContracts.Static.ControlFlow { + interface ICFG { + APC Entry { get; } + APC EntryAfterRequires { get; } + APC NormalExit { get; } + APC ExceptionExit { get; } + Subroutine Subroutine { get; } + + APC Next (APC pc); + + IEnumerable Successors (APC pc); + bool HasSingleSuccessor (APC pc, out APC ifFound); + + IEnumerable Predecessors (APC pc); + bool HasSinglePredecessor (APC pc, out APC ifFound); + + bool IsJoinPoint (APC pc); + bool IsSplitPoint (APC pc); + + bool IsBlockStart (APC pc); + bool IsBlockEnd (APC pc); + + IILDecoder GetDecoder (IMetaDataProvider metaDataProvider); + + void Print (TextWriter tw, ILPrinter printer, + Func>>> contextLookup, + LispList> context); + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IConstantInfo.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IConstantInfo.cs new file mode 100644 index 00000000000..1b333ecac29 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IConstantInfo.cs @@ -0,0 +1,35 @@ +// +// IConstantInfo.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.ControlFlow { + interface IEdgeSubroutineAdaptor { + LispList> GetOrdinaryEdgeSubroutinesInternal (CFGBlock @from, CFGBlock to, LispList> context); + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IHandlerFilter.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IHandlerFilter.cs new file mode 100644 index 00000000000..e8ce17dc157 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IHandlerFilter.cs @@ -0,0 +1,36 @@ +// +// IHandlerFilter.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using Mono.CodeContracts.Static.AST; + +namespace Mono.CodeContracts.Static.ControlFlow { + interface IHandlerFilter { + bool Catch (Data data, TypeNode exception, out bool stopPropagation); + bool Filter (Data data, APC filterCode, out bool stopPropagation); + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IMethodInfo.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IMethodInfo.cs new file mode 100644 index 00000000000..40dd57a5531 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IMethodInfo.cs @@ -0,0 +1,35 @@ +// +// IMethodInfo.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using Mono.CodeContracts.Static.AST; + +namespace Mono.CodeContracts.Static.ControlFlow { + interface IMethodInfo { + Method Method { get; } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IStackInfo.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IStackInfo.cs new file mode 100644 index 00000000000..01c8a0de318 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IStackInfo.cs @@ -0,0 +1,33 @@ +// +// IStackInfo.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +namespace Mono.CodeContracts.Static.ControlFlow { + interface IStackInfo { + bool IsCallOnThis (APC pc); + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/RemoveBranchDelegator.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/RemoveBranchDelegator.cs new file mode 100644 index 00000000000..35e12e42f00 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/RemoveBranchDelegator.cs @@ -0,0 +1,420 @@ +// +// RemoveBranchDelegator.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System.Collections.Generic; +using Mono.CodeContracts.Static.AST; +using Mono.CodeContracts.Static.AST.Visitors; +using Mono.CodeContracts.Static.DataStructures; +using Mono.CodeContracts.Static.Providers; + +namespace Mono.CodeContracts.Static.ControlFlow { + /// + /// This class wraps underlying visitor. + /// Replaces: branches to nop; branchCond to binary. + /// + /// EdgeTag.Requires: (inside method) => assume, (outside method) => assert + /// EdgeTag.Ensures: (inside method) => assert, (outside method) => assume + /// + struct RemoveBranchDelegator : IILVisitor + where Visitor : IILVisitor { + private readonly IMetaDataProvider meta_data_provider; + private readonly Visitor visitor; + + public RemoveBranchDelegator (Visitor visitor, + IMetaDataProvider metaDataProvider) + { + this.visitor = visitor; + this.meta_data_provider = metaDataProvider; + } + + #region IILVisitor Members + public Result Binary (APC pc, BinaryOperator op, Dummy dest, Dummy operand1, Dummy operand2, Data data) + { + return this.visitor.Binary (pc, op, dest, operand1, operand2, data); + } + + public Result Isinst (APC pc, TypeNode type, Dummy dest, Dummy obj, Data data) + { + return this.visitor.Isinst (pc, type, dest, obj, data); + } + + public Result LoadNull (APC pc, Dummy dest, Data polarity) + { + return this.visitor.LoadNull (pc, dest, polarity); + } + + public Result LoadConst (APC pc, TypeNode type, object constant, Dummy dest, Data data) + { + return this.visitor.LoadConst (pc, type, constant, dest, data); + } + + public Result Sizeof (APC pc, TypeNode type, Dummy dest, Data data) + { + return this.visitor.Sizeof (pc, type, dest, data); + } + + public Result Unary (APC pc, UnaryOperator op, bool unsigned, Dummy dest, Dummy source, Data data) + { + return this.visitor.Unary (pc, op, unsigned, dest, source, data); + } + + public Result Entry (APC pc, Method method, Data data) + { + return this.visitor.Entry (pc, method, data); + } + + public Result Assume (APC pc, EdgeTag tag, Dummy condition, Data data) + { + if (tag == EdgeTag.Requires && pc.InsideRequiresAtCall || tag == EdgeTag.Invariant && pc.InsideInvariantOnExit) + return this.visitor.Assert (pc, tag, condition, data); + + return this.visitor.Assume (pc, tag, condition, data); + } + + public Result Assert (APC pc, EdgeTag tag, Dummy condition, Data data) + { + if (pc.InsideEnsuresAtCall) + return this.visitor.Assume (pc, tag, condition, data); + + return this.visitor.Assert (pc, tag, condition, data); + } + + public Result BeginOld (APC pc, APC matchingEnd, Data data) + { + return this.visitor.BeginOld (pc, matchingEnd, data); + } + + public Result EndOld (APC pc, APC matchingBegin, TypeNode type, Dummy dest, Dummy source, Data data) + { + return this.visitor.EndOld (pc, matchingBegin, type, dest, source, data); + } + + public Result LoadStack (APC pc, int offset, Dummy dest, Dummy source, bool isOld, Data data) + { + return this.visitor.LoadStack (pc, offset, dest, source, isOld, data); + } + + public Result LoadStackAddress (APC pc, int offset, Dummy dest, Dummy source, TypeNode type, bool isOld, Data data) + { + return this.visitor.LoadStackAddress (pc, offset, dest, source, type, isOld, data); + } + + public Result LoadResult (APC pc, TypeNode type, Dummy dest, Dummy source, Data data) + { + return this.visitor.LoadResult (pc, type, dest, source, data); + } + + public Result Arglist (APC pc, Dummy dest, Data data) + { + return this.visitor.Arglist (pc, dest, data); + } + + public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data) + { + return this.visitor.Nop (pc, data); + } + + public Result BranchCond (APC pc, APC target, BranchOperator bop, Dummy value1, Dummy value2, Data data) + { + Dummy dest = Dummy.Value; + switch (bop) { + case BranchOperator.Beq: + return this.visitor.Binary (pc, BinaryOperator.Ceq, dest, value1, value2, data); + case BranchOperator.Bge: + return this.visitor.Binary (pc, BinaryOperator.Cge, dest, value1, value2, data); + case BranchOperator.Bge_Un: + return this.visitor.Binary (pc, BinaryOperator.Cge_Un, dest, value1, value2, data); + case BranchOperator.Bgt: + return this.visitor.Binary (pc, BinaryOperator.Cgt, dest, value1, value2, data); + case BranchOperator.Bgt_Un: + return this.visitor.Binary (pc, BinaryOperator.Cgt_Un, dest, value1, value2, data); + case BranchOperator.Ble: + return this.visitor.Binary (pc, BinaryOperator.Cle, dest, value1, value2, data); + case BranchOperator.Ble_Un: + return this.visitor.Binary (pc, BinaryOperator.Cle_Un, dest, value1, value2, data); + case BranchOperator.Blt: + return this.visitor.Binary (pc, BinaryOperator.Clt, dest, value1, value2, data); + case BranchOperator.Blt_Un: + return this.visitor.Binary (pc, BinaryOperator.Clt_Un, dest, value1, value2, data); + case BranchOperator.Bne_un: + return this.visitor.Binary (pc, BinaryOperator.Cne_Un, dest, value1, value2, data); + default: + return this.visitor.Nop (pc, data); + } + } + + public Result BranchTrue (APC pc, APC target, Dummy cond, Data data) + { + return this.visitor.Nop (pc, data); + } + + public Result BranchFalse (APC pc, APC target, Dummy cond, Data data) + { + return this.visitor.Nop (pc, data); + } + + public Result Break (APC pc, Data data) + { + return this.visitor.Break (pc, data); + } + + public Result Call (APC pc, Method method, bool virt, TypeList extraVarargs, Dummy dest, ArgList args, Data data) + where TypeList : IIndexable + where ArgList : IIndexable + { + TypeNode declaringType = this.meta_data_provider.DeclaringType (method); + if (MethodIsReferenceEquals (method, args, declaringType)) + return this.visitor.Binary (pc, BinaryOperator.Ceq, dest, args [0], args [1], data); + + return this.visitor.Call (pc, method, virt, extraVarargs, dest, args, data); + } + + public Result Calli (APC pc, TypeNode returnType, TypeList argTypes, bool instance, Dummy dest, Dummy functionPointer, ArgList args, Data data) + where TypeList : IIndexable + where ArgList : IIndexable + { + return this.visitor.Calli (pc, returnType, argTypes, instance, dest, functionPointer, args, data); + } + + public Result CheckFinite (APC pc, Dummy dest, Dummy source, Data data) + { + return this.visitor.CheckFinite (pc, dest, source, data); + } + + public Result CopyBlock (APC pc, Dummy destAddress, Dummy srcAddress, Dummy len, Data data) + { + return this.visitor.CopyBlock (pc, destAddress, srcAddress, len, data); + } + + public Result EndFilter (APC pc, Dummy decision, Data data) + { + return this.visitor.EndFilter (pc, decision, data); + } + + public Result EndFinally (APC pc, Data data) + { + return this.visitor.EndFinally (pc, data); + } + + public Result Jmp (APC pc, Method method, Data data) + { + return this.visitor.Jmp (pc, method, data); + } + + public Result LoadArg (APC pc, Parameter argument, bool isOld, Dummy dest, Data data) + { + return this.visitor.LoadArg (pc, argument, isOld, dest, data); + } + + public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, Dummy dest, Data data) + { + return this.visitor.LoadArgAddress (pc, argument, isOld, dest, data); + } + + public Result LoadLocal (APC pc, Local local, Dummy dest, Data data) + { + return this.visitor.LoadLocal (pc, local, dest, data); + } + + public Result LoadLocalAddress (APC pc, Local local, Dummy dest, Data data) + { + return this.visitor.LoadLocalAddress (pc, local, dest, data); + } + + public Result LoadElement (APC pc, TypeNode type, Dummy dest, Dummy array, Dummy index, Data data) + { + return this.visitor.LoadElement (pc, type, dest, array, index, data); + } + + public Result LoadField (APC pc, Field field, Dummy dest, Dummy obj, Data data) + { + return this.visitor.LoadField (pc, field, dest, obj, data); + } + + public Result LoadFieldAddress (APC pc, Field field, Dummy dest, Dummy obj, Data data) + { + return this.visitor.LoadFieldAddress (pc, field, dest, obj, data); + } + + public Result LoadLength (APC pc, Dummy dest, Dummy array, Data data) + { + return this.visitor.LoadLength (pc, dest, array, data); + } + + public Result LoadStaticField (APC pc, Field field, Dummy dest, Data data) + { + return this.visitor.LoadStaticField (pc, field, dest, data); + } + + public Result LoadStaticFieldAddress (APC pc, Field field, Dummy dest, Data data) + { + return this.visitor.LoadStaticFieldAddress (pc, field, dest, data); + } + + public Result LoadTypeToken (APC pc, TypeNode type, Dummy dest, Data data) + { + return this.visitor.LoadTypeToken (pc, type, dest, data); + } + + public Result LoadFieldToken (APC pc, Field type, Dummy dest, Data data) + { + return this.visitor.LoadFieldToken (pc, type, dest, data); + } + + public Result LoadMethodToken (APC pc, Method type, Dummy dest, Data data) + { + return this.visitor.LoadMethodToken (pc, type, dest, data); + } + + public Result Nop (APC pc, Data data) + { + return this.visitor.Nop (pc, data); + } + + public Result Pop (APC pc, Dummy source, Data data) + { + return this.visitor.Pop (pc, source, data); + } + + public Result Return (APC pc, Dummy source, Data data) + { + return this.visitor.Return (pc, source, data); + } + + public Result StoreArg (APC pc, Parameter argument, Dummy source, Data data) + { + return this.visitor.StoreArg (pc, argument, source, data); + } + + public Result StoreLocal (APC pc, Local local, Dummy source, Data data) + { + return this.visitor.StoreLocal (pc, local, source, data); + } + + public Result StoreElement (APC pc, TypeNode type, Dummy array, Dummy index, Dummy value, Data data) + { + return this.visitor.StoreElement (pc, type, array, index, value, data); + } + + public Result StoreField (APC pc, Field field, Dummy obj, Dummy value, Data data) + { + return this.visitor.StoreField (pc, field, obj, value, data); + } + + public Result StoreStaticField (APC pc, Field field, Dummy value, Data data) + { + return this.visitor.StoreStaticField (pc, field, value, data); + } + + public Result Switch (APC pc, TypeNode type, IEnumerable> cases, Dummy value, Data data) + { + return this.visitor.Nop (pc, data); + } + + public Result Box (APC pc, TypeNode type, Dummy dest, Dummy source, Data data) + { + return this.visitor.Box (pc, type, dest, source, data); + } + + public Result ConstrainedCallvirt (APC pc, Method method, TypeNode constraint, TypeList extraVarargs, Dummy dest, ArgList args, Data data) + where TypeList : IIndexable + where ArgList : IIndexable + { + return this.visitor.ConstrainedCallvirt (pc, method, constraint, extraVarargs, dest, args, data); + } + + public Result CastClass (APC pc, TypeNode type, Dummy dest, Dummy obj, Data data) + { + return this.visitor.CastClass (pc, type, dest, obj, data); + } + + public Result CopyObj (APC pc, TypeNode type, Dummy destPtr, Dummy sourcePtr, Data data) + { + return this.visitor.CopyObj (pc, type, destPtr, sourcePtr, data); + } + + public Result Initobj (APC pc, TypeNode type, Dummy ptr, Data data) + { + return this.visitor.Initobj (pc, type, ptr, data); + } + + public Result NewArray (APC pc, TypeNode type, Dummy dest, ArgList lengths, Data data) where ArgList : IIndexable + { + return this.visitor.NewArray (pc, type, dest, lengths, data); + } + + public Result NewObj (APC pc, Method ctor, Dummy dest, ArgList args, Data data) where ArgList : IIndexable + { + return this.visitor.NewObj (pc, ctor, dest, args, data); + } + + public Result MkRefAny (APC pc, TypeNode type, Dummy dest, Dummy obj, Data data) + { + return this.visitor.MkRefAny (pc, type, dest, obj, data); + } + + public Result RefAnyType (APC pc, Dummy dest, Dummy source, Data data) + { + return this.visitor.RefAnyType (pc, dest, source, data); + } + + public Result RefAnyVal (APC pc, TypeNode type, Dummy dest, Dummy source, Data data) + { + return this.visitor.RefAnyVal (pc, type, dest, source, data); + } + + public Result Rethrow (APC pc, Data data) + { + return this.visitor.Rethrow (pc, data); + } + + public Result Throw (APC pc, Dummy exception, Data data) + { + return this.visitor.Throw (pc, exception, data); + } + + public Result Unbox (APC pc, TypeNode type, Dummy dest, Dummy obj, Data data) + { + return this.visitor.Unbox (pc, type, dest, obj, data); + } + + public Result UnboxAny (APC pc, TypeNode type, Dummy dest, Dummy obj, Data data) + { + return this.visitor.UnboxAny (pc, type, dest, obj, data); + } + #endregion + + private bool MethodIsReferenceEquals (Method method, ArgList args, TypeNode declaringType) + where ArgList : IIndexable + { + return args.Count == 2 && this.meta_data_provider.IsStatic (method) + && this.meta_data_provider.Equal (declaringType, this.meta_data_provider.System_Object) + && this.meta_data_provider.Name (method) == "ReferenceEquals"; + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Subroutine.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Subroutine.cs new file mode 100644 index 00000000000..b4351223491 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Subroutine.cs @@ -0,0 +1,186 @@ +// +// Subroutine.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.Collections.Generic; +using System.IO; +using Mono.CodeContracts.Static.Analysis; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.ControlFlow { + abstract class Subroutine : ITypedProperties, IEquatable { + private static int _subroutineIdGenerator; + private readonly TypedProperties properties = new TypedProperties (); + private readonly int subroutine_id = _subroutineIdGenerator++; + + public virtual SubroutineKind Kind + { + get { return SubroutineKind.Unknown; } + } + + public int Id + { + get { return this.subroutine_id; } + } + + public abstract CFGBlock Entry { get; } + public abstract CFGBlock EntryAfterRequires { get; } + public abstract CFGBlock Exit { get; } + public abstract CFGBlock ExceptionExit { get; } + public abstract string Name { get; } + public abstract int BlockCount { get; } + public abstract IEnumerable Blocks { get; } + + public virtual bool IsRequires + { + get { return false; } + } + + public virtual bool IsEnsures + { + get { return false; } + } + + public virtual bool IsOldValue + { + get { return false; } + } + + public virtual bool IsMethod + { + get { return false; } + } + + public virtual bool IsConstructor + { + get { return false; } + } + + public virtual bool IsInvariant + { + get { return false; } + } + + public virtual bool IsContract + { + get { return false; } + } + + public bool IsEnsuresOrOldValue + { + get { return IsEnsures || IsOldValue; } + } + + public abstract EdgeMap SuccessorEdges { get; } + public abstract EdgeMap PredecessorEdges { get; } + public abstract DepthFirst.Visitor EdgeInfo { get; } + + public virtual bool IsFaultFinally + { + get { return false; } + } + + public abstract bool HasReturnValue { get; } + public abstract bool HasContextDependentStackDepth { get; } + + public abstract int StackDelta { get; } + + #region ITypedProperties Members + public bool TryGetValue (TypedKey key, out T value) + { + return this.properties.TryGetValue (key, out value); + } + #endregion + + #region Implementation of ITypedProperties + public bool Contains (TypedKey key) + { + return this.properties.Contains (key); + } + + public void Add (TypedKey key, T value) + { + this.properties.Add (key, value); + } + #endregion + + public override string ToString () + { + return string.Format ("SR {0}: BlockCount:{1}, Kind:{2}", Id, BlockCount, Kind); + } + + public abstract IEnumerable SuccessorBlocks (CFGBlock block); + + public IEnumerable> SuccessorEdgesFor (CFGBlock block) + { + return SuccessorEdges [block]; + } + + public abstract IEnumerable PredecessorBlocks (CFGBlock block); + + public abstract bool IsJoinPoint (CFGBlock block); + public abstract bool IsSplitPoint (CFGBlock block); + public abstract bool HasSingleSuccessor (APC point, out APC ifFound); + public abstract bool HasSinglePredecessor (APC point, out APC ifFound); + + public abstract void AddEdgeSubroutine (CFGBlock from, CFGBlock to, Subroutine subroutine, EdgeTag tag); + + public abstract IEnumerable Successors (APC pc); + public abstract IEnumerable Predecessors (APC pc); + + public abstract bool IsSubroutineEnd (CFGBlock block); + public abstract bool IsSubroutineStart (CFGBlock block); + public abstract bool IsCatchFilterHeader (CFGBlock block); + + public abstract APC ComputeTargetFinallyContext (APC pc, CFGBlock succ); + public abstract LispList> EdgeSubroutinesOuterToInner (CFGBlock current, CFGBlock succ, out bool isExceptionHandlerEdge, LispList> context); + public abstract LispList> GetOrdinaryEdgeSubroutines (CFGBlock current, CFGBlock succ, LispList> context); + public abstract void Initialize (); + public abstract IEnumerable UsedSubroutines (HashSet alreadySeen); + + public IEnumerable UsedSubroutines () + { + return UsedSubroutines (new HashSet ()); + } + + public abstract IEnumerable ExceptionHandlers (CFGBlock block, Subroutine innerSubroutine, + Data data, IHandlerFilter handlerPredicate); + + public abstract void Print (TextWriter tw, ILPrinter printer, + Func>>> contextLookup, + LispList> context, + HashSet>>> set); + + #region Implementation of IEquatable + public bool Equals (Subroutine other) + { + return Id == other.Id; + } + #endregion + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/SubroutineKind.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/SubroutineKind.cs new file mode 100644 index 00000000000..d802d0443aa --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/SubroutineKind.cs @@ -0,0 +1,41 @@ +// +// SubroutineKind.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +namespace Mono.CodeContracts.Static.ControlFlow { + enum SubroutineKind { + Unknown, + Requires, + Ensures, + Method, + Entry, + Fault, + Finally, + Simple, + Old + } +} \ No newline at end of file diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/DataFlowAnalysisBase.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/DataFlowAnalysisBase.cs new file mode 100644 index 00000000000..9dfc61c321a --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/DataFlowAnalysisBase.cs @@ -0,0 +1,164 @@ +// +// DataFlowAnalysisBase.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.Collections.Generic; +using System.IO; +using Mono.CodeContracts.Static.ControlFlow; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + abstract class DataFlowAnalysisBase : + IEqualityComparer { + protected ICFG CFG; + protected Dictionary JoinState; + protected PriorityQueue pending; + private IWidenStrategy widen_strategy; + + protected DataFlowAnalysisBase (ICFG cfg) + { + this.CFG = cfg; + this.pending = new PriorityQueue (WorkingListComparer); + this.JoinState = new Dictionary (this); + this.widen_strategy = null; + } + + #region IEqualityComparer Members + bool IEqualityComparer.Equals (APC x, APC y) + { + return x.Equals (y); + } + + int IEqualityComparer.GetHashCode (APC obj) + { + return obj.GetHashCode (); + } + #endregion + + public void Initialize (APC entryPoint, AState state) + { + this.JoinState.Add (entryPoint, state); + this.pending.Enqueue (entryPoint); + } + + public virtual void ComputeFixPoint () + { + this.widen_strategy = new EdgeBasedWidening (20); + + while (this.pending.Count > 0) { + APC next = this.pending.Dequeue (); + AState state = MutableVersion (this.JoinState [next], next); + + APC cur; + bool repeatOuter = false; + do { + cur = next; + if (!IsBottom (cur, state)) { + state = Transfer (cur, state); + } else { + repeatOuter = true; + break; + } + } while (HasSingleSuccessor (cur, out next) && !RequiresJoining (next)); + + if (repeatOuter) + continue; + + foreach (APC successorAPC in Successors (cur)) { + if (!IsBottom (successorAPC, state)) + PushState (cur, successorAPC, state); + } + } + } + + protected virtual void Dump (AState state) + { + } + + public IEnumerable> States () + { + return this.JoinState; + } + + protected abstract IEnumerable Successors (APC pc); + + protected virtual void PushState (APC current, APC next, AState state) + { + state = ImmutableVersion (state, next); + if (RequiresJoining (next)) { + if (!JoinStateAtBlock (new Pair (current, next), state)) + return; + this.pending.Enqueue (next); + } else { + this.JoinState [next] = state; + this.pending.Enqueue (next); + } + } + + private bool JoinStateAtBlock (Pair edge, AState state) + { + AState existingState; + if (this.JoinState.TryGetValue (edge.Value, out existingState)) { + bool widen = this.widen_strategy.WantToWiden (edge.Key, edge.Value, IsBackEdge (edge.Key, edge.Value)); + AState joinedState; + bool result = Join (edge, state, existingState, out joinedState, widen); + if (result) + this.JoinState [edge.Value] = ImmutableVersion (joinedState, edge.Value); + return result; + } + + this.JoinState.Add (edge.Value, state); + return true; + } + + protected abstract bool IsBackEdge (APC from, APC to); + + protected abstract int WorkingListComparer (APC a, APC b); + + protected abstract bool Join (Pair edge, AState newState, AState existingState, out AState joinedState, bool widen); + + protected abstract bool RequiresJoining (APC pc); + + protected abstract bool HasSingleSuccessor (APC pc, out APC next); + + protected abstract bool IsBottom (APC pc, AState state); + + protected abstract AState Transfer (APC pc, AState state); + + protected abstract AState MutableVersion (AState state, APC at); + protected abstract AState ImmutableVersion (AState state, APC at); + + public void PrintStatesAtJoinPoints (TextWriter tw) + { + foreach (APC apc in this.JoinState.Keys) { + string str = this.JoinState [apc].ToString ().Replace (Environment.NewLine, Environment.NewLine + " "); + tw.WriteLine ("Block {0}, PC {1}: {2}", apc.Block, apc.Index, str); + } + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeBasedWidening.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeBasedWidening.cs new file mode 100644 index 00000000000..22e74f0976d --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeBasedWidening.cs @@ -0,0 +1,46 @@ +// +// EdgeBasedWidening.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using Mono.CodeContracts.Static.ControlFlow; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + class EdgeBasedWidening : StepWidening> { + public EdgeBasedWidening (int n) + : base (n) + { + } + + #region Overrides of StepWidening> + protected override Pair MakeIndex (APC from, APC to) + { + return new Pair (from, to); + } + #endregion + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeConverter.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeConverter.cs new file mode 100644 index 00000000000..37d6e338532 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeConverter.cs @@ -0,0 +1,31 @@ +// +// EdgeConverter.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + delegate AbstractState EdgeConverter (Label from, Label to, bool isJoinPoint, EdgeData data, AbstractState newState); +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs new file mode 100644 index 00000000000..ec6c23d4544 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs @@ -0,0 +1,151 @@ +// +// ForwardAnalysis.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.IO; +using Mono.CodeContracts.Static.AST.Visitors; +using Mono.CodeContracts.Static.Analysis; +using Mono.CodeContracts.Static.ControlFlow; +using Mono.CodeContracts.Static.DataStructures; +using Mono.CodeContracts.Static.Providers; + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + class ForwardAnalysis : + ForwardDataFlowAnalysisBase, + IFixPointInfo { + private readonly Action> dumper; + private readonly EdgeConverter edge_converter; + private readonly Func edge_data_getter; + private readonly Func immutable_version; + private readonly Func is_bottom; + private readonly Joiner joiner; + private readonly Func mutable_version; + private readonly Func transfer; + + public ForwardAnalysis (ICFG cfg, + Func transfer, + Joiner joiner, + Func immutableVersion, + Func mutableVersion, + EdgeConverter edgeConverter, + Func edgeDataGetter, + Func isBottom, + Action> dumper) : base (cfg) + { + this.transfer = transfer; + this.joiner = joiner; + this.immutable_version = immutableVersion; + this.mutable_version = mutableVersion; + this.edge_converter = edgeConverter; + this.edge_data_getter = edgeDataGetter; + this.is_bottom = isBottom; + this.dumper = dumper; + } + + #region IFixPointInfo Members + public bool PreStateLookup (APC pc, out AState state) + { + return GetPreState (pc, out state); + } + + public bool PostStateLookup (APC pc, out AState state) + { + return GetPostState (pc, out state); + } + #endregion + + public static ForwardAnalysis Make ( + IILDecoder decoder, + IAnalysis, EdgeData> analysis) + where Context : IMethodContextProvider + { + IILVisitor visitor = analysis.GetVisitor (); + var forwardAnalysisSolver = new ForwardAnalysis ( + decoder.ContextProvider.MethodContext.CFG, + (pc, state) => decoder.ForwardDecode> (pc, visitor, state), + analysis.Join, + analysis.ImmutableVersion, + analysis.MutableVersion, + analysis.EdgeConversion, + decoder.EdgeData, + (pc, state) => { + if (!decoder.IsUnreachable (pc)) + return analysis.IsBottom (pc, state); + + return true; + }, + analysis.Dump + ); + + analysis.SaveFixPointInfo (forwardAnalysisSolver); + return forwardAnalysisSolver; + } + + protected override void Dump (AState state) + { + this.dumper (new Pair (state, Console.Out)); + } + + protected override void PushState (APC from, APC next, AState state) + { + EdgeData data = this.edge_data_getter (from, next); + AState pushState = this.edge_converter (from, next, RequiresJoining (next), data, state); + base.PushState (from, next, pushState); + } + + protected override bool Join (Pair edge, AState newState, AState existingState, out AState joinedState, bool widen) + { + bool weaker; + joinedState = this.joiner (edge, newState, existingState, out weaker, widen); + + return weaker; + } + + protected override bool IsBottom (APC pc, AState state) + { + return this.is_bottom (pc, state); + } + + protected override AState Transfer (APC pc, AState state) + { + AState resultState = this.transfer (pc, state); + + return resultState; + } + + protected override AState MutableVersion (AState state, APC at) + { + return this.mutable_version (state); + } + + protected override AState ImmutableVersion (AState state, APC at) + { + return this.immutable_version (state); + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardDataFlowAnalysisBase.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardDataFlowAnalysisBase.cs new file mode 100644 index 00000000000..b82f8f182df --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardDataFlowAnalysisBase.cs @@ -0,0 +1,155 @@ +// +// ForwardDataFlowAnalysisBase.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System.Collections.Generic; +using Mono.CodeContracts.Static.ControlFlow; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + abstract class ForwardDataFlowAnalysisBase : DataFlowAnalysisBase { + private readonly Dictionary post_state = new Dictionary (); + + protected ForwardDataFlowAnalysisBase (ICFG cfg) : base (cfg) + { + } + + public bool GetPreState (APC pc, out AState state) + { + bool noInfo; + state = GetPreState (pc, default(AState), out noInfo); + return !noInfo; + } + + public AState GetPreStateWithDefault (APC apc, AState ifMissing) + { + bool noInfo; + AState preState = GetPreState (apc, default(AState), out noInfo); + return noInfo ? ifMissing : preState; + } + + private AState GetPreState (APC apc, AState ifMissing, out bool noInfo) + { + LispList rest = null; + APC tmp = apc; + APC singlePredecessor; + AState state; + bool weHaveState; + while (!(weHaveState = this.JoinState.TryGetValue (tmp, out state)) && + !RequiresJoining (tmp) && this.CFG.HasSinglePredecessor (tmp, out singlePredecessor)) { + tmp = singlePredecessor; + + rest = rest.Cons (tmp); + } + + if (!weHaveState) { + noInfo = true; + return ifMissing; + } + + bool listWasNotEmpty = rest != null; + while (rest != null) { + if (IsBottom (rest.Head, state)) { + noInfo = false; + return state; + } + state = MutableVersion (state, rest.Head); + state = Transfer (rest.Head, state); + if (IsBottom (rest.Head, state)) { + noInfo = false; + return state; + } + + rest = rest.Tail; + if (rest != null) + this.JoinState.Add (rest.Head, ImmutableVersion (state, rest.Head)); + } + + if (listWasNotEmpty) + this.JoinState.Add (apc, ImmutableVersion (state, apc)); + + noInfo = false; + return state; + } + + public bool GetPostState (APC apc, out AState result) + { + if (this.post_state.TryGetValue (apc, out result)) + return true; + + APC singleSuccessor; + if (apc.Block.Count <= apc.Index) + return GetPreState (apc, out result); + + if (this.CFG.HasSingleSuccessor (apc, out singleSuccessor) && !RequiresJoining (singleSuccessor)) + return GetPreState (singleSuccessor, out result); + + AState ifFound; + if (!GetPreState (apc, out ifFound)) + return false; + + result = MutableVersion (ifFound, apc); + result = Transfer (apc, result); + + this.post_state.Add (apc, result); + return true; + } + + public void Run (AState startState) + { + Initialize (this.CFG.Entry, startState); + ComputeFixPoint (); + } + + protected override int WorkingListComparer (APC a, APC b) + { + return b.Block.ReversePostOrderIndex - a.Block.ReversePostOrderIndex; + } + + protected override bool RequiresJoining (APC pc) + { + return this.CFG.IsJoinPoint (pc); + } + + protected override bool HasSingleSuccessor (APC pc, out APC next) + { + return this.CFG.HasSingleSuccessor (pc, out next); + } + + protected override IEnumerable Successors (APC pc) + { + return this.CFG.Successors (pc); + } + + protected override bool IsBackEdge (APC from, APC to) + { + //todo: implement this + //can't be false, because back edges means having cycles, so we definitely have to widen + return true; + } + } +} diff --git a/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IAnalysis.cs b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IAnalysis.cs new file mode 100644 index 00000000000..b3027b86408 --- /dev/null +++ b/mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IAnalysis.cs @@ -0,0 +1,45 @@ +// +// IAnalysis.cs +// +// Authors: +// Alexander Chebaturkin (chebaturkin@gmail.com) +// +// Copyright (C) 2011 Alexander Chebaturkin +// +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: +// +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +// + +using System; +using System.IO; +using Mono.CodeContracts.Static.ControlFlow; +using Mono.CodeContracts.Static.DataStructures; + +namespace Mono.CodeContracts.Static.DataFlowAnalysis { + interface IAnalysis { + Visitor GetVisitor (); + AbstractState Join (Pair edge, AbstractState newstate, AbstractState prevstate, out bool weaker, bool widen); + AbstractState ImmutableVersion (AbstractState arg); + AbstractState MutableVersion (AbstractState arg); + AbstractState EdgeConversion (APC from, APC to, bool isJoinPoint, EdgeData data, AbstractState state); + bool IsBottom (Label pc, AbstractState state); + Predicate