locked
Code Contracts: uncaught exception. RRS feed

  • Question

  • I am getting the following uncaught exception while using code contracts version 1.4.31130.0. I also have the VS 2010 editor extensions installed. I am using the full commercial version in Visual Studio 2010 Ultimate. I can email the entire project for help in reproducing this error, if needed. This is a blocking bug - Code Contracts is no longer functional for this project.

    In addition, please note the two suggested preconditions. These don't appear to make sense. The return value of that function should be null if parsing failed.

    C:\[path hidden]\UTLoggerLib\Models\IMessageProvider.cs(81,4): message : CodeContracts: Suggested precondition: Contract.Requires(m != null);
    
    C:\[path hidden]\UTLoggerLib\Models\IMessageProvider.cs(81,4): message : CodeContracts: Suggested precondition: Contract.Requires(m != null);
    
    CodeContracts: UTLoggerLib: Failed with uncaught exception: Index was outside the bounds of the array.
    
    CodeContracts: UTLoggerLib: Stack trace: at Microsoft.Research.AbstractDomains.Numerical.LinearEqualitiesEnvironment`2.IsEmpty()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.AbstractDomains.Numerical.LinearEqualitiesEnvironment`2.get_IsBottom()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.AbstractDomains.ReducedCartesianAbstractDomain`2.get_IsBottom()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.AbstractDomains.Numerical.SubPolyhedra`2.get_IsBottom()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.AbstractDomains.Numerical.SubPolyhedra`2.ReduceInternal(LinearEqualitiesForSubpolyhedraEnvironment`2 left, IntervalEnvironment`2 right, Boolean forceSimplex)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.AbstractDomains.Numerical.SubPolyhedra`2.Widening(IAbstractDomain prev)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.HelperForWidening(AbstractDomain newState, AbstractDomain prevState, Pair`2 edge)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.GenericValueAnalysis`2.Join(Pair`2 edge, AbstractDomain newState, AbstractDomain prevState, Boolean& changed, Boolean widen)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ForwardAnalysisSolver`2.Join(Pair`2 edge, AState newState, AState existingState, AState& joinedState, Boolean widen)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.DFARoot`2.JoinStateAtBlock(Pair`2 edge, AState state)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.DFARoot`2.PushState(APC current, APC next, AState state)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ForwardAnalysisSolver`2.PushState(APC pc, APC next, AState state)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.DFARoot`2.ComputeFixpoint()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ForwardDFA`2.Run(AState startState)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.RunTheAnalysis[AbstractDomain,Options](String methodName, IMethodDriver`13 driver, GenericValueAnalysis`2 analysis)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.RunTheAnalysis[Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,Expression,Variable,Options](String methodName, DomainKind adomain, IMethodDriver`13 driver, Options options)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.NumericalAnalysis`1.<FixpointInfo>d__c.MoveNext()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.AILogicInferenceWithRefinements`1.IsTrue(APC pc, BoxedExpression condition)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ComposedFactQuery`1.IsTrue(APC pc, BoxedExpression condition)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ComposedFactQuery`1.IsTrue(APC pc, BoxedExpression condition)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation(IMethodDriver`13 mdriver, IFactQuery`2 facts, Int32 maxPathSize, APC pc, BoxedExpression goalExpression)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.TypeBinder`12.DischargeObligation(IMethodDriver`13 mdriver, IFactQuery`2 facts, Int32 maxPathSize, APC pc, Variable goal)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.WeakestPreconditionProver.Discharge[Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,Expression,Variable,LogOptions](APC pc, Variable goal, Int32 maxPathSize, IMethodDriver`13 mdriver, IFactQuery`2 facts)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Analyzers.NonNull.TypeBindings`11.NonNullProofObligation.Validate(IFactQuery`2 query, IOutputResults output)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.ProofObligations`13.Validate(IOutputResults output, IFactQuery`2 query)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Analyzers.NonNull.TypeBindings`11.Analysis.ValidateImplicitAssertions(IFactQuery`2 facts, IOutputResults output)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Analyzers.NonNull.TypeBindings`11.AnalysisForArrays.ValidateImplicitAssertions(IFactQuery`2 facts, IOutputResults output, IFixpointInfo`2 fixpointInfo)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.AnalysisWrapper.TypeBindings`11.ArrayAnalysis`2.ValidateImplicitAssertions(IFactQuery`2 facts, IOutputResults output)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeNonIteratorMethodInternal(Method method)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal(Method method)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethod(Method method)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeAssembly(String assemblyName, Set`1 assembliesUnderAnalysis)
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.InternalAnalyze()
    
    CodeContracts: UTLoggerLib: at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.Analyze()
    
    CodeContracts: UTLoggerLib: 
    
    CodeContracts: UTLoggerLib: Background contract analysis done.

    Here is another exception I am getting:

    CodeContracts: UTLoggerLib: Failed with uncaught exception: Index was outside the bounds of the array.
    CodeContracts: UTLoggerLib: Stack trace:  at Microsoft.Research.CodeAnalysis.StackInfo`1.Pop(Int32 slots)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackInfo.Pop(Int32 slots)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.Microsoft.Research.CodeAnalysis.IVisitMSIL<Microsoft.Research.CodeAnalysis.APC,Local,Parameter,Method,Field,Type,Microsoft.Research.DataStructures.Unit,Microsoft.Research.DataStructures.Unit,Microsoft.Research.CodeAnalysis.StackInfo,Microsoft.Research.CodeAnalysis.StackInfo>.Call[TypeList,ArgList](APC pc, Method method, Boolean tail, Boolean virt, TypeList extraVarargs, Unit dest, ArgList args, StackInfo data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.APCDecoder`9.RemoveBranchDelegator`3.Call[TypeList,ArgList](APC pc, Method method, Boolean tail, Boolean virt, TypeList extraVarargs, Unit dest, ArgList args, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.BlockWithLabels`1.LabelAdapter`3.Call[TypeList,ArgList](Label pc, Method method, Boolean tail, Boolean virt, TypeList extraVarargs, Unit dest, ArgList args, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.OptimisticHeapAnalyzer`9.Domain.PathElement`1.Decode[Data,Result,Visitor,PC,Local2,Parameter2,Method2,Field2,Type2](PC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.ClousotExpressionCodeProvider`5.Decode[Visitor,Data,Result](PC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.BlockWithLabels`1.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.APCDecoder`9.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.ComputeStackDepth(Subroutine subroutine)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.GetStackDepthMap(Subroutine subroutine)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.Lookup(APC apc)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.StackDecoder`3.Ldarg(APC pc, Parameter argument, Boolean ignoredIsOld, Unit dest, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.APCDecoder`9.RemoveBranchDelegator`3.Ldarg(APC pc, Parameter argument, Boolean isOld, Unit dest, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.BlockWithLabels`1.LabelAdapter`3.Ldarg(Label pc, Parameter argument, Boolean isOld, Unit dest, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.OptimisticHeapAnalyzer`9.Domain.ParameterPathElement.Decode[Data,Result,Visitor,PC,Local2,Parameter2,Method2,Field2,Type2](PC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.ClousotExpressionCodeProvider`5.Decode[Visitor,Data,Result](PC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.BlockWithLabels`1.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.EnsuresBlock`1.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodCache`9.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.APCDecoder`9.ForwardDecode[Data,Result,Visitor](APC pc, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.StackDepthProvider`10.ForwardDecode[Data,Result,Visitor](APC lab, Visitor visitor, Data data)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodHasher`10.HashSubroutine(Subroutine subroutine)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodHasher`10.HashSubroutine(Subroutine subroutine)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodHasher`10.HashSubroutine(Subroutine subroutine)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.MethodHasher`10.GetHash(Byte[] AdditionalOptionsToHash)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.CacheManager`9.StartMethod(IMethodDriver`13 mDriver)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeNonIteratorMethodInternal(Method method)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethodInternal(Method method)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeMethod(Method method)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.AnalyzeAssembly(String assemblyName, Set`1 assembliesUnderAnalysis)
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.InternalAnalyze()
    CodeContracts: UTLoggerLib:  at Microsoft.Research.CodeAnalysis.Clousot.TypeBinder`9.Analyze()
    CodeContracts: UTLoggerLib: 
    CodeContracts: UTLoggerLib: Background contract analysis done.
    Monday, February 7, 2011 5:46 PM

Answers

  • Hello,

      thank you very much for the repro and the message. We think it is now fixed.

     

    Thanks,

    f

    Wednesday, February 9, 2011 12:36 AM

All replies

  • By adding "-show progress" to the static scanner options and plain old trial and error, I have narrowed down the second exception to a call to this function, which I've stripped down to the bare minimum version that still triggers the exception:

    		private static string GetProduct(Dictionary<string, string> keyValuePairs, out bool validProduct)
    		{
    			string ret = "???";
    			validProduct = false;
    			return ret;
    		}
    

    Calling this function from almost anywhere seems to trigger the exception just after it outputs the calling method in the output (with the "-show progress" option on). After I refactored the function to follow this signature, the exception goes away:

    		private static bool GetProduct(Dictionary<string, string> keyValuePairs, out string product)
    		{
    			product = "???";
    			bool ret = false;
    			return ret;
    		}
    
    The first exception is semi-unreliable in that, sometimes I can reproduce it 100% of the time. Then, other times, I will reproduce it a couple of times, and then it will go away with a rebuild. However, I haven't been able to reproduce it since making the above change to fix the second exception, so I'm not sure if they are related or if it's just a coincidence.
    Monday, February 7, 2011 11:02 PM
  • Hello,

      thank you very much for the repro and the message. We think it is now fixed.

     

    Thanks,

    f

    Wednesday, February 9, 2011 12:36 AM