From 233ff7d50dd1e729da0c68b44d84320a5c0f3b50 Mon Sep 17 00:00:00 2001 From: tom-englert Date: Sat, 18 Jul 2015 18:31:44 +0200 Subject: [PATCH 1/2] Fix regression tests (Analyze1FromSourcesV40) Signed-off-by: tom-englert --- .../ClousotTests/ClousotTests.csproj | 6 + .../ClousotTests/Sources/Abbreviators.cs | 2 +- .../ClousotTests/Sources/IOperations.cs | 4 +- .../IteratorSimpleContract.cs | 345 ++++++++-------- .../RegressionTest/TestFrameworkOOB/Purity.cs | 1 + .../TestFrameworkOOB/ReferenceToAllOOBC.cs | 5 +- .../TestFrameworkOOB/UserFeedback.cs | 21 +- .../TestPostconditionInference/Filtering.cs | 371 +++++++++--------- 8 files changed, 393 insertions(+), 362 deletions(-) diff --git a/Microsoft.Research/RegressionTest/ClousotTests/ClousotTests.csproj b/Microsoft.Research/RegressionTest/ClousotTests/ClousotTests.csproj index 6f8867bd..15b9f78c 100644 --- a/Microsoft.Research/RegressionTest/ClousotTests/ClousotTests.csproj +++ b/Microsoft.Research/RegressionTest/ClousotTests/ClousotTests.csproj @@ -179,6 +179,12 @@ Sources\UserFeedback.cs + + Sources\IteratorSimpleContract.cs + + + Sources\Filtering.cs + Sources\ArrayWithNonNullAnalysis.cs diff --git a/Microsoft.Research/RegressionTest/ClousotTests/Sources/Abbreviators.cs b/Microsoft.Research/RegressionTest/ClousotTests/Sources/Abbreviators.cs index 8c7ba9e8..93b955d6 100644 --- a/Microsoft.Research/RegressionTest/ClousotTests/Sources/Abbreviators.cs +++ b/Microsoft.Research/RegressionTest/ClousotTests/Sources/Abbreviators.cs @@ -63,7 +63,7 @@ public void Work3() } [ClousotRegressionTest] - [RegressionOutcome(Outcome = ProofOutcome.False, Message = "ensures is false: this.X == Contract.OldValue(this.X)", PrimaryILOffset = 19, MethodILOffset = 20)] + [RegressionOutcome(Outcome = ProofOutcome.False, Message = "ensures is false: X == Contract.OldValue(X)", PrimaryILOffset = 19, MethodILOffset = 20)] [RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = @"ensures unreachable", PrimaryILOffset = 43, MethodILOffset = 20)] [RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = @"ensures unreachable", PrimaryILOffset = 67, MethodILOffset = 20)] public void Work4() diff --git a/Microsoft.Research/RegressionTest/ClousotTests/Sources/IOperations.cs b/Microsoft.Research/RegressionTest/ClousotTests/Sources/IOperations.cs index 33360e21..be904d29 100644 --- a/Microsoft.Research/RegressionTest/ClousotTests/Sources/IOperations.cs +++ b/Microsoft.Research/RegressionTest/ClousotTests/Sources/IOperations.cs @@ -59,8 +59,8 @@ public Type[] Types [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 8, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 52, MethodILOffset = 36)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 77, MethodILOffset = 36)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 52, MethodILOffset = 31)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 77, MethodILOffset = 31)] public double Do(params object[] operands) { Console.Write(string.Format("We have {0} {1}s\n", operands[1], operands[0])); diff --git a/Microsoft.Research/RegressionTest/IteratorAnalysis/IteratorSimpleContract/IteratorSimpleContract.cs b/Microsoft.Research/RegressionTest/IteratorAnalysis/IteratorSimpleContract/IteratorSimpleContract.cs index fb306242..2995858c 100644 --- a/Microsoft.Research/RegressionTest/IteratorAnalysis/IteratorSimpleContract/IteratorSimpleContract.cs +++ b/Microsoft.Research/RegressionTest/IteratorAnalysis/IteratorSimpleContract/IteratorSimpleContract.cs @@ -21,181 +21,196 @@ using Microsoft.Research.ClousotRegression; using System.Diagnostics.Contracts; -namespace IteratorSimpleContract { - - public class Test2 { - #region Drivers - [ClousotRegressionTestAttribute] - [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: s != null", PrimaryILOffset = 55, MethodILOffset = 49)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 55, MethodILOffset = 20)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 55, MethodILOffset = 28)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 41, MethodILOffset = 0)] - public string Test2a(string s) { - Contract.Requires(s != null); - var strs = Test1a("hello"); // Positive: precondtions of Test1a (s != null) - strs = Test1a(s); // Positive: precondition of Test1a (s != null) - Contract.Assert(strs != null); // assertion is valid from the postcondition of Test1a - strs = Test1a(null); // Negative: postcondition of Test1a (s!= null) - return s; - } +namespace IteratorSimpleContract +{ - [ClousotRegressionTestAttribute] + public class Test2 + { + #region Drivers + [ClousotRegressionTestAttribute] + [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: s != null", PrimaryILOffset = 55, MethodILOffset = 49)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 55, MethodILOffset = 20)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 55, MethodILOffset = 28)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 41, MethodILOffset = 0)] + public string Test2a(string s) + { + Contract.Requires(s != null); + var strs = Test1a("hello"); // Positive: precondtions of Test1a (s != null) + strs = Test1a(s); // Positive: precondition of Test1a (s != null) + Contract.Assert(strs != null); // assertion is valid from the postcondition of Test1a + strs = Test1a(null); // Negative: postcondition of Test1a (s!= null) + return s; + } + + [ClousotRegressionTestAttribute] #if !CLOUSOT2 - [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: s != null", PrimaryILOffset = 63, MethodILOffset = 3)] + [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: s != null", PrimaryILOffset = 63, MethodILOffset = 3)] #else [RegressionOutcome(Outcome=ProofOutcome.False,Message="requires is false: s != null",PrimaryILOffset=44,MethodILOffset=3)] -#endif - public void Test2b(string s) { - Test1b(null); // Negative: legacy precondition of Test1b not satisified: (s!= null) - } - - [ClousotRegressionTestAttribute] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 59, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: input != null", PrimaryILOffset = 59, MethodILOffset = 70)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 59, MethodILOffset = 16)] +#endif + public void Test2b(string s) + { + Test1b(null); // Negative: legacy precondition of Test1b not satisified: (s!= null) + } + + [ClousotRegressionTestAttribute] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 59, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"requires is false: input != null", PrimaryILOffset = 59, MethodILOffset = 70)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"requires is valid", PrimaryILOffset = 59, MethodILOffset = 16)] #if !NETFRAMEWORK_4_0 - #if !CLOUSOT2 - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="requires unproven",PrimaryILOffset=22,MethodILOffset=54)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="requires is valid",PrimaryILOffset=44,MethodILOffset=54)] - #else // CLOUSOT2 +#if !CLOUSOT2 + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "requires unproven", PrimaryILOffset = 22, MethodILOffset = 54)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 44, MethodILOffset = 54)] +#else // CLOUSOT2 [RegressionOutcome(Outcome=ProofOutcome.Top,Message="requires unproven",PrimaryILOffset=3,MethodILOffset=54)] [RegressionOutcome(Outcome=ProofOutcome.True,Message="requires is valid",PrimaryILOffset=25,MethodILOffset=54)] - #endif +#endif #else // .net v4.0 [RegressionOutcome(Outcome=ProofOutcome.Top,Message="requires unproven: collection != null (collection)",PrimaryILOffset=17,MethodILOffset=54)] [RegressionOutcome(Outcome=ProofOutcome.True,Message="requires is valid",PrimaryILOffset=39,MethodILOffset=54)] #endif - public void Test2d(IEnumerable s) { - Contract.Requires(s != null); - IEnumerable resultEnum = Test1d(s); // Precondition is validated - Contract.Assert(Contract.ForAll(resultEnum, (string s1) => s1 != null)); // From postcondition, but cannot prove for now. - s = null; - Test1d(s); // This one fails - } - - // Forall(...) precondition cannot be proven for now in the two cases below. - [ClousotRegressionTestAttribute] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Contract.ForAll(input, (T s) => s != null)", PrimaryILOffset = 67, MethodILOffset = 46)] - public void Test2e(IEnumerable ss) { - Contract.Requires(Contract.ForAll(ss, (string s) => s != null)); - Test1e(ss); // Even we have a precondition in the caller, the precondition of callee is not proven. - } - - [ClousotRegressionTestAttribute] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Contract.ForAll(inputArray, (int x) => x < max)", PrimaryILOffset = 103, MethodILOffset = 24)] - public void Test2f() { - int[] arr = { 1, 2, 3, 4 }; - int max = 5; - Test1f(arr, max); // Forall precondition of the callee is not proven. - } - - [ClousotRegressionTestAttribute] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 16, MethodILOffset = 0)] - public void Test2g() { - IEnumerable singleton = Test1g(2); - Contract.Assert(singleton != null); // Postcondition is proven. - } - - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.False,Message="assert is false",PrimaryILOffset=277,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=237,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=178,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=131,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=88,MethodILOffset=0)] - public IEnumerable TestIteratorPaths(int x) { - Contract.Requires(x > 0); - - Contract.Assert(x > 0); - yield return 1; - - Contract.Assert(x > 0); - x = 2; - yield return 2; - - Contract.Assert(x == 2); - x = x * x; - yield return 2; - - Contract.Assert(x > 0); - yield return 3; - - Contract.Assert(x < 0); - } - #endregion Drivers - - #region Iterator methods with contracts - /// - /// Contract for iterator method: Requires, Ensures, Ensures with forall. - /// Iterator class with closure classes, both in forall and in the code. - /// - public IEnumerable Test1a(string s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result>() != null); - Contract.Ensures(Contract.ForAll(Contract.Result>(), (string s1) => s1 != null)); - int[] x = { 1, 2 }; - x.First(((int y) => y > 0)); - yield return s; - } - /// - /// Contract for iterator method: Legacy precondition, with EndContractBlock(). - /// - /// - /// - public IEnumerable Test1b(string s) { - if (s == null) throw new Exception(""); - Contract.EndContractBlock(); - yield return s; - } - - /// - /// Contract for iterator method with type parameter. - /// Post condition is forall - /// - /// - /// - /// - public IEnumerable Test1d(IEnumerable input) { - Contract.Requires(input != null); - Contract.Ensures(Contract.ForAll(Contract.Result>(), (T s1) => s1 != null)); - foreach (T t in input) - yield return t; - } - - /// - /// Contract for iterator method with type parameters and input ienumerable, precondition is forall. - /// - /// - /// - public IEnumerable Test1e(IEnumerable input) { - Contract.Requires(Contract.ForAll(input, (T s) => s != null)); - foreach (T t in input) { - yield return t; - } - } - - /// - /// Contract for iterator method with closure that captures a parameter. - /// - /// - /// - public IEnumerable Test1f(IEnumerable inputArray, int max) - { - Contract.Requires(Contract.ForAll(inputArray, (int x) => x < max)); - Contract.Ensures(Contract.ForAll(Contract.Result>(), (int y) => y >0)); - foreach (int i in inputArray) { - yield return (max -i); - } - } - - /// - /// Contract for iterator method: simplest post condition: result is non-null; - /// - /// - /// - public IEnumerable Test1g(int x) { - Contract.Ensures(Contract.Result>() != null); - yield return x; + public void Test2d(IEnumerable s) + { + Contract.Requires(s != null); + IEnumerable resultEnum = Test1d(s); // Precondition is validated + Contract.Assert(Contract.ForAll(resultEnum, (string s1) => s1 != null)); // From postcondition, but cannot prove for now. + s = null; + Test1d(s); // This one fails + } + + // Forall(...) precondition cannot be proven for now in the two cases below. + [ClousotRegressionTestAttribute] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Contract.ForAll(input, (T s) => s != null)", PrimaryILOffset = 67, MethodILOffset = 46)] + public void Test2e(IEnumerable ss) + { + Contract.Requires(Contract.ForAll(ss, (string s) => s != null)); + Test1e(ss); // Even we have a precondition in the caller, the precondition of callee is not proven. + } + + [ClousotRegressionTestAttribute] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Contract.ForAll(inputArray, (int x) => x < max)", PrimaryILOffset = 103, MethodILOffset = 24)] + public void Test2f() + { + int[] arr = { 1, 2, 3, 4 }; + int max = 5; + Test1f(arr, max); // Forall precondition of the callee is not proven. + } + + [ClousotRegressionTestAttribute] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 16, MethodILOffset = 0)] + public void Test2g() + { + IEnumerable singleton = Test1g(2); + Contract.Assert(singleton != null); // Postcondition is proven. + } + + [RegressionOutcome(Outcome = ProofOutcome.False, Message = "assert is false", PrimaryILOffset = 277, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 237, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "assert unproven", PrimaryILOffset = 88, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 131, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 88, MethodILOffset = 0)] + public IEnumerable TestIteratorPaths(int x) + { + Contract.Requires(x > 0); + + Contract.Assert(x > 0); + yield return 1; + + Contract.Assert(x > 0); + x = 2; + yield return 2; + + Contract.Assert(x == 2); + x = x * x; + yield return 2; + + Contract.Assert(x > 0); + yield return 3; + + Contract.Assert(x < 0); + } + #endregion Drivers + + #region Iterator methods with contracts + /// + /// Contract for iterator method: Requires, Ensures, Ensures with forall. + /// Iterator class with closure classes, both in forall and in the code. + /// + public IEnumerable Test1a(string s) + { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.ForAll(Contract.Result>(), (string s1) => s1 != null)); + int[] x = { 1, 2 }; + x.First(((int y) => y > 0)); + yield return s; + } + /// + /// Contract for iterator method: Legacy precondition, with EndContractBlock(). + /// + /// + /// + public IEnumerable Test1b(string s) + { + if (s == null) throw new Exception(""); + Contract.EndContractBlock(); + yield return s; + } + + /// + /// Contract for iterator method with type parameter. + /// Post condition is forall + /// + /// + /// + /// + public IEnumerable Test1d(IEnumerable input) + { + Contract.Requires(input != null); + Contract.Ensures(Contract.ForAll(Contract.Result>(), (T s1) => s1 != null)); + foreach (T t in input) + yield return t; + } + + /// + /// Contract for iterator method with type parameters and input ienumerable, precondition is forall. + /// + /// + /// + public IEnumerable Test1e(IEnumerable input) + { + Contract.Requires(Contract.ForAll(input, (T s) => s != null)); + foreach (T t in input) + { + yield return t; + } + } + + /// + /// Contract for iterator method with closure that captures a parameter. + /// + /// + /// + public IEnumerable Test1f(IEnumerable inputArray, int max) + { + Contract.Requires(Contract.ForAll(inputArray, (int x) => x < max)); + Contract.Ensures(Contract.ForAll(Contract.Result>(), (int y) => y > 0)); + foreach (int i in inputArray) + { + yield return (max - i); + } + } + + /// + /// Contract for iterator method: simplest post condition: result is non-null; + /// + /// + /// + public IEnumerable Test1g(int x) + { + Contract.Ensures(Contract.Result>() != null); + yield return x; + } + #endregion Iterator methods with contracts } - #endregion Iterator methods with contracts - } } diff --git a/Microsoft.Research/RegressionTest/TestFrameworkOOB/Purity.cs b/Microsoft.Research/RegressionTest/TestFrameworkOOB/Purity.cs index e2394e26..47182af9 100644 --- a/Microsoft.Research/RegressionTest/TestFrameworkOOB/Purity.cs +++ b/Microsoft.Research/RegressionTest/TestFrameworkOOB/Purity.cs @@ -21,6 +21,7 @@ public static void Test(object a, object b) [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference \'dict\'", PrimaryILOffset = 3, MethodILOffset = 0), RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 16, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 21, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 16)] public static void Test(IDictionary dict, int key) { Contract.Requires(dict.ContainsKey(key)); diff --git a/Microsoft.Research/RegressionTest/TestFrameworkOOB/ReferenceToAllOOBC.cs b/Microsoft.Research/RegressionTest/TestFrameworkOOB/ReferenceToAllOOBC.cs index d854a8b6..3136267c 100644 --- a/Microsoft.Research/RegressionTest/TestFrameworkOOB/ReferenceToAllOOBC.cs +++ b/Microsoft.Research/RegressionTest/TestFrameworkOOB/ReferenceToAllOOBC.cs @@ -56,6 +56,8 @@ public static void Test2() [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 28, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 38, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 51, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 18)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 28)] public static void TestPureLookup(Dictionary dict, int key) { Contract.Requires(dict != null); @@ -73,6 +75,8 @@ public static void TestPureLookup(Dictionary dict, int key) [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 18, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 34, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 54, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 18)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 34)] public static void TestOutByRef() { var d = new Dictionary(); @@ -473,7 +477,6 @@ private static void Test2(IEnumerable elements) [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 100, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 141, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 154, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 166, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 60, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 60, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 15, MethodILOffset = 133)] diff --git a/Microsoft.Research/RegressionTest/TestFrameworkOOB/UserFeedback.cs b/Microsoft.Research/RegressionTest/TestFrameworkOOB/UserFeedback.cs index d07fdbd6..5569ea25 100644 --- a/Microsoft.Research/RegressionTest/TestFrameworkOOB/UserFeedback.cs +++ b/Microsoft.Research/RegressionTest/TestFrameworkOOB/UserFeedback.cs @@ -228,13 +228,13 @@ internal class Some [ClousotRegressionTest("cci2only")] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 2, MethodILOffset = 0)] #if NETFRAMEWORK_4_0 - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 33, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 57, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 72, MethodILOffset = 0)] + [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=33,MethodILOffset=0)] + [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=57,MethodILOffset=0)] + [RegressionOutcome(Outcome=ProofOutcome.Bottom,Message="assert unreachable",PrimaryILOffset=72,MethodILOffset=0)] #else [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 29, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 53, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 68, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = "assert unreachable", PrimaryILOffset = 68, MethodILOffset = 0)] #endif public void WaitFor0() { @@ -259,15 +259,15 @@ public void WaitFor0() [ClousotRegressionTest("cci2only")] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 2, MethodILOffset = 0)] #if NETFRAMEWORK_4_0 - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 33, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 50, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 62, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 77, MethodILOffset = 0)] + [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=33,MethodILOffset=0)] + [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=50,MethodILOffset=0)] + [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=62,MethodILOffset=0)] + [RegressionOutcome(Outcome=ProofOutcome.Bottom,Message="assert unreachable",PrimaryILOffset=77,MethodILOffset=0)] #else [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 29, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 46, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 58, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 73, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = "assert unreachable", PrimaryILOffset = 73, MethodILOffset = 0)] #endif public void WaitFor0WithLockObject() { @@ -344,6 +344,7 @@ private void AddItemToDict(string key, object value) [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference \'this._dict\'", PrimaryILOffset = 8, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 21, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 16, MethodILOffset = 21)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "requires unproven: !ReferenceEquals(key, null)", PrimaryILOffset = 21, MethodILOffset = 8)] private void ProcessItem(string key, object value) { if (!_dict.ContainsKey(key)) @@ -875,7 +876,7 @@ public void Baz() [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as receiver)", PrimaryILOffset = 8, MethodILOffset = 0)] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as receiver)", PrimaryILOffset = 15, MethodILOffset = 0)] - [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: this.Prop2 != 0", PrimaryILOffset = 13, MethodILOffset = 15)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Prop2 != 0", PrimaryILOffset = 13, MethodILOffset = 15)] private static void Test() { Foo foo = new Foo(); diff --git a/Microsoft.Research/RegressionTest/TestPostconditionInference/Filtering.cs b/Microsoft.Research/RegressionTest/TestPostconditionInference/Filtering.cs index db5f8752..94c7a440 100644 --- a/Microsoft.Research/RegressionTest/TestPostconditionInference/Filtering.cs +++ b/Microsoft.Research/RegressionTest/TestPostconditionInference/Filtering.cs @@ -16,214 +16,219 @@ using System; using System.Diagnostics.Contracts; + using Microsoft.Research.ClousotRegression; namespace TestPostconditionInference { - public class TestRangesAreFiltered - { - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == x);")] - public static int IntPostcondition(int x) - { - return x; - } - - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == x);")] - public static long LongPostcondition(long x) - { - return x; - } - - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == u);")] - public static UInt32 UInt32Postcondition(uint u) + public class TestRangesAreFiltered { - return u; + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == x);")] + public static int IntPostcondition(int x) + { + return x; + } + + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == x);")] + public static long LongPostcondition(long x) + { + return x; + } + + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == u);")] + public static uint UInt32Postcondition(uint u) + { + return u; + } + + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == u);")] + public static ulong UInt64Postcondition(ulong u) + { + return u; + } + + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == s);")] + public static sbyte SBytePostcondition(sbyte s) + { + return s; + } + + public long _field; + + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as field receiver)", PrimaryILOffset = 2, MethodILOffset = 0)] + [RegressionOutcome("Contract.Ensures(z == this._field);")] + public void SetField(long z) + { + _field = z; + } } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == u);")] - public static UInt64 UInt64Postcondition(UInt64 u) + public class FilterRedundantPostcondition { - return u; + public string applicationVersion; + + public string ApplicationVersion + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 22, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 6, MethodILOffset = 27)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 16, MethodILOffset = 27)] + get + { + Contract.Ensures(Contract.Result() == applicationVersion); + return applicationVersion; + } + } + + private extern string GetApplicationVersion(); } - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == s);")] - public static SByte SBytePostcondition(SByte s) + public class TimeSpan { - return s; + public long _ticks; + + public double TotalDays + { + // We should emit a range, as this implies that the result is not NaN + // Also the range is the one of longs, which is included in double + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as field receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome("Contract.Ensures(Contract.Result() == (double)(this._ticks) * 1.15740740740741E-12);")] + [RegressionOutcome("Contract.Ensures(-9223372036854775808 <= Contract.Result());")] + [RegressionOutcome("Contract.Ensures(Contract.Result() <= 9223372036854775807);")] + get + { + return (_ticks*1.1574074074074074E-12); + } + } + + // Here we should not emit a range, as d may be NaN or +00 or -oo + [ClousotRegressionTest] + [RegressionOutcome("Contract.Ensures(Contract.Result() == d);")] + public static double DoubleInPostcondition(double d) + { + return d; + } } - - public long _field; - - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message=@"valid non-null reference (as field receiver)",PrimaryILOffset=2,MethodILOffset=0)] - [RegressionOutcome("Contract.Ensures(z == this._field);")] - public void SetField(long z) - { - this._field = z; - } - } - - public class FilterRedundantPostcondition - { - public string applicationVersion; - public string ApplicationVersion +#pragma warning disable 0626 + public class Array { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=22,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=6,MethodILOffset=27)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="ensures is valid",PrimaryILOffset=16,MethodILOffset=27)] - get - { - Contract.Ensures(Contract.Result() == applicationVersion); - return applicationVersion; - } + private extern int Length + { + get; + } + + // We cast from an Int32, so we should get a smaller interval than the range of long + public long LongLength + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome("Contract.Ensures(Contract.Result() == (long)(this.Length));")] + [RegressionOutcome("Contract.Ensures(Contract.Result() == this.Length);")] + [RegressionOutcome("Contract.Ensures(-2147483648 <= Contract.Result());")] + [RegressionOutcome("Contract.Ensures(Contract.Result() <= 2147483647);")] + get + { + return Length; + } + } } - extern string GetApplicationVersion(); - - } - - public class TimeSpan - { - public long _ticks; - - public double TotalDays + public struct TmpStruct { - // We should emit a range, as this implies that the result is not NaN - // Also the range is the one of longs, which is included in double - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message=@"valid non-null reference (as field receiver)",PrimaryILOffset=1,MethodILOffset=0)] - [RegressionOutcome("Contract.Ensures(Contract.Result() == (double)(this._ticks) * 1.15740740740741E-12);")] - [RegressionOutcome("Contract.Ensures(-9223372036854775808 <= Contract.Result());")] - [RegressionOutcome("Contract.Ensures(Contract.Result() <= 9223372036854775807);")] - get - { - return (this._ticks * 1.1574074074074074E-12); - } + public int[] arr; } - // Here we should not emit a range, as d may be NaN or +00 or -oo - [ClousotRegressionTest] - [RegressionOutcome("Contract.Ensures(Contract.Result() == d);")] - public static double DoubleInPostcondition(double d) + public class Tmp { - return d; + public int[] arr; + + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 38, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 38, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 69, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 69, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 95, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 95, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 47, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possible use of a null array 't.arr'", PrimaryILOffset = 52, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 32, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 38, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possible use of a null array 'tstruct.arr'. The static checker determined that the condition 'tstruct.arr != null' should hold on entry. Nevertheless, the condition may be too strong for the callers. If you think it is ok, add a precondition to document it: Contract.Requires(tstruct.arr != null);", PrimaryILOffset = 84, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 69, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 104, MethodILOffset = 0)] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as array)", PrimaryILOffset = 95, MethodILOffset = 0)] + // Should not suggest t.arr.Length >= 0 and tstruct.arr.Length >= 0 + [RegressionOutcome("Contract.Requires(t.arr != null);")] + [RegressionOutcome("Contract.Ensures(t.arr != null);")] + [RegressionOutcome("Contract.Ensures(tstruct.arr != null);")] + public static int RemoveSimpleAccess(Tmp t, TmpStruct tstruct, int[] p) + { + Contract.Requires(t != null); + Contract.Requires(p != null); + + int sum = 0; + for (var i = 0; i < t.arr.Length; i++) + { + sum += t.arr[i]; + } + + for (var i = 0; i < tstruct.arr.Length; i++) + { + sum += tstruct.arr[i]; + } + + for (var i = 0; i < p.Length; i++) + { + sum += p[i]; + } + + return sum; + } } - } -#pragma warning disable 0626 - public class Array - { - extern int Length { get; } - - // We cast from an Int32, so we should get a smaller interval than the range of long - public long LongLength + public class Expression { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message=@"valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] - [RegressionOutcome("Contract.Ensures(Contract.Result() == (long)(this.Length));")] - [RegressionOutcome("Contract.Ensures(Contract.Result() == this.Length);")] - [RegressionOutcome("Contract.Ensures(-2147483648 <= Contract.Result());")] - [RegressionOutcome("Contract.Ensures(Contract.Result() <= 2147483647);")] - get - { - return (long)this.Length; - } - } - } - - public struct TmpStruct - { - public int[] arr; - } - - public class Tmp - { - public int[] arr; - - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=38,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=38,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=69,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=69,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Lower bound access ok",PrimaryILOffset=95,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="Upper bound access ok",PrimaryILOffset=95,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=47,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possible use of a null array 't.arr'",PrimaryILOffset=52,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=32,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=38,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.Top,Message="Possible use of a null array 'tstruct.arr'. The static checker determined that the condition 'tstruct.arr != null' should hold on entry. Nevertheless, the condition may be too strong for the callers. If you think it is ok, add a precondition to document it: Contract.Requires(tstruct.arr != null);",PrimaryILOffset=84,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=69,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=104,MethodILOffset=0)] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as array)",PrimaryILOffset=95,MethodILOffset=0)] - // Should not suggest t.arr.Length >= 0 and tstruct.arr.Length >= 0 - [RegressionOutcome("Contract.Requires(t.arr != null);")] - [RegressionOutcome("Contract.Ensures(t.arr != null);")] - [RegressionOutcome("Contract.Ensures(tstruct.arr != null);")] - public static int RemoveSimpleAccess(Tmp t, TmpStruct tstruct, int[] p) - { - Contract.Requires(t != null); - Contract.Requires(p != null); - - int sum = 0; - for (var i = 0; i < t.arr.Length; i++) - { - sum += t.arr[i]; - } - - for (var i = 0; i < tstruct.arr.Length; i++) - { - sum += tstruct.arr[i]; - } - - for (var i = 0; i < p.Length; i++) - { - sum += p[i]; - } - - return sum; - } - } - - public class Expression { } - - public class ExpandSegment - { - private readonly Expression filter; - - public ExpandSegment(Expression filter) - { - this.filter = filter; - } - - public Expression Filter - { - [ClousotRegressionTest] - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=1,MethodILOffset=0)] - [RegressionOutcome("Contract.Ensures(Contract.Result() == this.filter);")] - get - { - return this.filter; - } } - public bool HasFilter + public class ExpandSegment { - // We used to infer Contract.Result() == ((this.filter == null) == 0)) - [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] - [RegressionOutcome("Contract.Ensures(Contract.Result() == ((this.Filter == null) == false));")] - [RegressionOutcome("Contract.Ensures(this.Filter == this.filter);")] - [ClousotRegressionTest] - get - { - return (this.Filter != null); - } + private readonly Expression filter; + + public ExpandSegment(Expression filter) + { + this.filter = filter; + } + + public Expression Filter + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome("Contract.Ensures(Contract.Result() == this.filter);")] + get + { + return filter; + } + } + + public bool HasFilter + { + // We used to infer Contract.Result() == ((this.filter == null) == 0)) + [RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 1, MethodILOffset = 0)] + [RegressionOutcome("Contract.Ensures(Contract.Result() == ((this.Filter == null) == false));")] + [RegressionOutcome("Contract.Ensures(this.Filter == this.filter);")] + [ClousotRegressionTest] + get + { + return (Filter != null); + } + } } - } } \ No newline at end of file From 61190f03d8bea190ccdd2295f6493743db1b2dcf Mon Sep 17 00:00:00 2001 From: tom-englert Date: Sat, 18 Jul 2015 18:47:26 +0200 Subject: [PATCH 2/2] Some code depends on the current culture, therefore set the main thread to InvariantCulture, so everything behaves the same as in the US. Signed-off-by: tom-englert --- Microsoft.Research/ClousotMain/ClousotMain.cs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Microsoft.Research/ClousotMain/ClousotMain.cs b/Microsoft.Research/ClousotMain/ClousotMain.cs index fb4b84cb..e846b917 100644 --- a/Microsoft.Research/ClousotMain/ClousotMain.cs +++ b/Microsoft.Research/ClousotMain/ClousotMain.cs @@ -36,6 +36,7 @@ using Microsoft.Research.ClousotPulse.Messages; using Microsoft.Research.CodeAnalysis.Inference; using System.IO.Pipes; +using System.Globalization; // Because these classes and methods can be called from different places (Console, Visual Studio, WCF Service, ...) // - do not use Console unless guarded with #if DEBUG. Instead use output @@ -795,6 +796,10 @@ static IOutputFullResults SelectOutput( public int Analyze() { + // String formatting in the analyzer does not specify a culture, therefore some tests fail on systems with non-English culture with e.g. "expected: 2.0, actual: 2,0" + // Setting the threads culture should be removed as soon as issue #149 is fixed. + Thread.CurrentThread.CurrentCulture = CultureInfo.InvariantCulture; + try { return InternalAnalyze();