From 6034514fd981b1135c2da03906eba22bd2ac0a6e Mon Sep 17 00:00:00 2001 From: jeroen-mostert Date: Tue, 1 Mar 2016 23:07:39 +0100 Subject: [PATCH 1/7] Add missing preconditions --- .../MsCorlib/System.Text.Encoding.cs | 43 +++++++++++++------ 1 file changed, 29 insertions(+), 14 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs b/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs index d73e6084..6bb19c4e 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs @@ -158,6 +158,8 @@ extern virtual public bool IsBrowserDisplay public virtual string GetString(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); + Contract.Requires(index >= 0 && index <= bytes.Length); + Contract.Requires(count >= 0 && index + count <= bytes.Length); Contract.Ensures(Contract.Result() != null); return default(string); @@ -173,14 +175,16 @@ public virtual string GetString(byte[] bytes) } #endif [Pure] - public virtual int GetMaxCharCount(int arg0) + public virtual int GetMaxCharCount(int byteCount) { + Contract.Requires(byteCount >= 0); Contract.Ensures(Contract.Result() >= 0); return default(int); } [Pure] - public virtual int GetMaxByteCount(int arg0) + public virtual int GetMaxByteCount(int charCount) { + Contract.Requires(charCount >= 0); Contract.Ensures(Contract.Result() >= 0); return default(int); } @@ -199,12 +203,10 @@ public virtual Decoder GetDecoder() public virtual int GetChars(byte[] bytes, int byteIndex, int byteCount, char[] chars, int charIndex) { Contract.Requires(bytes != null); + Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); + Contract.Requires(byteCount >= 0 && byteIndex + byteCount <= bytes.Length); Contract.Requires(chars != null); - Contract.Requires(byteIndex >= 0); - Contract.Requires(byteCount >= 0); - Contract.Requires(charIndex >= 0); - Contract.Requires(byteIndex + byteCount <= bytes.Length); - Contract.Requires(charIndex <= chars.Length); + Contract.Requires(charIndex >= 0 && charIndex <= chars.Length); Contract.Ensures(Contract.Result() >= 0); @@ -214,9 +216,8 @@ public virtual int GetChars(byte[] bytes, int byteIndex, int byteCount, char[] c public virtual char[] GetChars(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); - Contract.Requires(index >= 0); - Contract.Requires(count >= 0); - Contract.Requires(index + count <= bytes.Length); + Contract.Requires(index >= 0 && index <= bytes.Length); + Contract.Requires(count >= 0 && index + count <= bytes.Length); Contract.Ensures(Contract.Result() != null); return default(char[]); @@ -233,10 +234,8 @@ public virtual char[] GetChars(byte[] bytes) public virtual int GetCharCount(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); - Contract.Requires(index >= 0); - Contract.Requires(count >= 0); - Contract.Requires(index + count <= bytes.Length); - + Contract.Requires(index >= 0 && index <= bytes.Length); + Contract.Requires(count >= 0 && index + count <= bytes.Length); Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -252,6 +251,11 @@ public virtual int GetCharCount(byte[] bytes) public virtual int GetBytes(string s, int charIndex, int charCount, byte[] bytes, int byteIndex) { Contract.Requires(s != null); + Contract.Requires(charIndex >= 0 && charIndex <= s.Length); + Contract.Requires(charCount >= 0 && charIndex + charCount <= s.Length); + Contract.Requires(bytes != null); + Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); + Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -267,6 +271,11 @@ public virtual byte[] GetBytes(string s) public virtual int GetBytes(char[] chars, int charIndex, int charCount, byte[] bytes, int byteIndex) { Contract.Requires(chars != null); + Contract.Requires(charIndex >= 0 && charIndex <= chars.Length); + Contract.Requires(charCount >= 0 && charIndex + charCount <= chars.Length); + Contract.Requires(bytes != null); + Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); + Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -275,6 +284,8 @@ public virtual int GetBytes(char[] chars, int charIndex, int charCount, byte[] b public virtual byte[] GetBytes(char[] chars, int index, int count) { Contract.Requires(chars != null); + Contract.Requires(index >= 0 && index <= chars.Length); + Contract.Requires(count >= 0 && index + count <= chars.Length); Contract.Ensures(Contract.Result() != null); return default(byte[]); @@ -291,6 +302,8 @@ public virtual byte[] GetBytes(char[] chars) public virtual int GetByteCount(char[] chars, int index, int count) { Contract.Requires(chars != null); + Contract.Requires(index >= 0 && index <= chars.Length); + Contract.Requires(count >= 0 && index + count <= chars.Length); Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -340,6 +353,8 @@ public static byte[] Convert(Encoding srcEncoding, Encoding dstEncoding, byte[] Contract.Requires(srcEncoding != null); Contract.Requires(dstEncoding != null); Contract.Requires(bytes != null); + Contract.Requires(index >= 0 && index <= bytes.Length); + Contract.Requires(count >= 0 && index + count <= bytes.Length); Contract.Ensures(Contract.Result() != null); return default(byte[]); } From b19896233e4fb392376f1a10979727f778982b38 Mon Sep 17 00:00:00 2001 From: jeroen-mostert Date: Tue, 1 Mar 2016 23:39:03 +0100 Subject: [PATCH 2/7] Rearrange terms to avoid failing on overflow; do null checks first --- .../MsCorlib/System.Text.Encoding.cs | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs b/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs index 6bb19c4e..665f95ee 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Text.Encoding.cs @@ -159,7 +159,7 @@ public virtual string GetString(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); Contract.Requires(index >= 0 && index <= bytes.Length); - Contract.Requires(count >= 0 && index + count <= bytes.Length); + Contract.Requires(count >= 0 && count <= bytes.Length - index); Contract.Ensures(Contract.Result() != null); return default(string); @@ -203,9 +203,9 @@ public virtual Decoder GetDecoder() public virtual int GetChars(byte[] bytes, int byteIndex, int byteCount, char[] chars, int charIndex) { Contract.Requires(bytes != null); - Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); - Contract.Requires(byteCount >= 0 && byteIndex + byteCount <= bytes.Length); Contract.Requires(chars != null); + Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); + Contract.Requires(byteCount >= 0 && byteCount <= bytes.Length - byteIndex); Contract.Requires(charIndex >= 0 && charIndex <= chars.Length); Contract.Ensures(Contract.Result() >= 0); @@ -217,7 +217,7 @@ public virtual char[] GetChars(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); Contract.Requires(index >= 0 && index <= bytes.Length); - Contract.Requires(count >= 0 && index + count <= bytes.Length); + Contract.Requires(count >= 0 && count <= bytes.Length - index); Contract.Ensures(Contract.Result() != null); return default(char[]); @@ -235,7 +235,7 @@ public virtual int GetCharCount(byte[] bytes, int index, int count) { Contract.Requires(bytes != null); Contract.Requires(index >= 0 && index <= bytes.Length); - Contract.Requires(count >= 0 && index + count <= bytes.Length); + Contract.Requires(count >= 0 && count <= bytes.Length - index); Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -251,9 +251,9 @@ public virtual int GetCharCount(byte[] bytes) public virtual int GetBytes(string s, int charIndex, int charCount, byte[] bytes, int byteIndex) { Contract.Requires(s != null); - Contract.Requires(charIndex >= 0 && charIndex <= s.Length); - Contract.Requires(charCount >= 0 && charIndex + charCount <= s.Length); Contract.Requires(bytes != null); + Contract.Requires(charIndex >= 0 && charIndex <= s.Length); + Contract.Requires(charCount >= 0 && charCount <= s.Length - charIndex); Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); Contract.Ensures(Contract.Result() >= 0); @@ -271,9 +271,9 @@ public virtual byte[] GetBytes(string s) public virtual int GetBytes(char[] chars, int charIndex, int charCount, byte[] bytes, int byteIndex) { Contract.Requires(chars != null); - Contract.Requires(charIndex >= 0 && charIndex <= chars.Length); - Contract.Requires(charCount >= 0 && charIndex + charCount <= chars.Length); Contract.Requires(bytes != null); + Contract.Requires(charIndex >= 0 && charIndex <= chars.Length); + Contract.Requires(charCount >= 0 && charCount <= chars.Length - charIndex); Contract.Requires(byteIndex >= 0 && byteIndex <= bytes.Length); Contract.Ensures(Contract.Result() >= 0); @@ -285,7 +285,7 @@ public virtual byte[] GetBytes(char[] chars, int index, int count) { Contract.Requires(chars != null); Contract.Requires(index >= 0 && index <= chars.Length); - Contract.Requires(count >= 0 && index + count <= chars.Length); + Contract.Requires(count >= 0 && count <= chars.Length - index); Contract.Ensures(Contract.Result() != null); return default(byte[]); @@ -303,7 +303,7 @@ public virtual int GetByteCount(char[] chars, int index, int count) { Contract.Requires(chars != null); Contract.Requires(index >= 0 && index <= chars.Length); - Contract.Requires(count >= 0 && index + count <= chars.Length); + Contract.Requires(count >= 0 && count <= chars.Length - index); Contract.Ensures(Contract.Result() >= 0); return default(int); @@ -354,7 +354,7 @@ public static byte[] Convert(Encoding srcEncoding, Encoding dstEncoding, byte[] Contract.Requires(dstEncoding != null); Contract.Requires(bytes != null); Contract.Requires(index >= 0 && index <= bytes.Length); - Contract.Requires(count >= 0 && index + count <= bytes.Length); + Contract.Requires(count >= 0 && count <= bytes.Length - index); Contract.Ensures(Contract.Result() != null); return default(byte[]); } From e904c8d4531baa2b9b97b5e76f7d02e5eb476840 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Valentin=20W=C3=BCstholz?= Date: Tue, 14 Jun 2016 20:10:20 -0500 Subject: [PATCH 3/7] Minor changes --- Microsoft.Research/RegressionTest/MaxCalls/MaxCalls.cs | 4 ++-- Microsoft.Research/RegressionTest/MaxCalls/MaxCalls0.cs | 4 ++-- Microsoft.Research/RegressionTest/MaxCalls/MaxCalls1.cs | 4 ++-- Microsoft.Research/RegressionTest/MaxJoins/MaxJoins.cs | 6 +++--- Microsoft.Research/RegressionTest/MaxJoins/MaxJoins0.cs | 4 ++-- Microsoft.Research/RegressionTest/MaxJoins/MaxJoins1.cs | 6 +++--- Microsoft.Research/RegressionTest/MaxJoins/MaxJoins2.cs | 6 +++--- .../RegressionTest/MaxWidenings/MaxWidenings0.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings1.cs | 6 +++--- .../RegressionTest/MaxWidenings/MaxWidenings2.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings3.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings4.cs | 6 +++--- .../RegressionTest/MaxWidenings/MaxWidenings5.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings6.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings7.cs | 4 ++-- .../RegressionTest/MaxWidenings/MaxWidenings8.cs | 4 ++-- 16 files changed, 37 insertions(+), 37 deletions(-) diff --git a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls.cs b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls.cs index b9aed0f4..a3cebb0c 100644 --- a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls.cs +++ b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace CallDepth +namespace MaxCalls { - public class CallDepth + public class MaxCalls { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 38, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls0.cs b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls0.cs index e777cb4b..bf82578f 100644 --- a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls0.cs +++ b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls0.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace CallDepth +namespace MaxCalls { - public class CallDepth + public class MaxCalls { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 38, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls1.cs b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls1.cs index e777cb4b..bf82578f 100644 --- a/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls1.cs +++ b/Microsoft.Research/RegressionTest/MaxCalls/MaxCalls1.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace CallDepth +namespace MaxCalls { - public class CallDepth + public class MaxCalls { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 38, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins.cs b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins.cs index 481e41bd..5d36b038 100644 --- a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins.cs +++ b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace JoinDepthTest +namespace MaxJoins { - public class JoinDepth + public class MaxJoins { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 29, MethodILOffset = 0)] @@ -51,4 +51,4 @@ private void Test1(int x, int y) Contract.Assert(s1 != null); } } -} \ No newline at end of file +} diff --git a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins0.cs b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins0.cs index 7aaab1cc..8ac099b1 100644 --- a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins0.cs +++ b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins0.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace JoinDepth +namespace MaxJoins { - public class JoinDepth + public class MaxJoins { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.False, Message = @"assert is false", PrimaryILOffset = 29, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins1.cs b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins1.cs index 15ea1eb7..37bf58e1 100644 --- a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins1.cs +++ b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins1.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace JoinDepth +namespace MaxJoins { - public class JoinDepth + public class MaxJoins { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 29, MethodILOffset = 0)] @@ -51,4 +51,4 @@ private void Test1(int x, int y) Contract.Assert(s1 != null); } } -} \ No newline at end of file +} diff --git a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins2.cs b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins2.cs index 4d4c5b8a..5d36b038 100644 --- a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins2.cs +++ b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins2.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace JoinDepth +namespace MaxJoins { - public class JoinDepth + public class MaxJoins { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 29, MethodILOffset = 0)] @@ -51,4 +51,4 @@ private void Test1(int x, int y) Contract.Assert(s1 != null); } } -} \ No newline at end of file +} diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings0.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings0.cs index e21b8cb1..05067aee 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings0.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings0.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 13, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings1.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings1.cs index b53dfdd1..05067aee 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings1.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings1.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 13, MethodILOffset = 0)] @@ -34,4 +34,4 @@ private void Test0(int x, int N) Contract.Assert(y <= x); } } -} \ No newline at end of file +} diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings2.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings2.cs index 77f923fc..9648d33c 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings2.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings2.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 76, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings3.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings3.cs index 9e82f328..9d4a9180 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings3.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings3.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 76, MethodILOffset = 0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings4.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings4.cs index 4a1b95ac..9d4a9180 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings4.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings4.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 76, MethodILOffset = 0)] @@ -53,4 +53,4 @@ public static long Exp_Reflector(long x, long y) return num; } } -} \ No newline at end of file +} diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings5.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings5.cs index a75f91f0..620971f5 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings5.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings5.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome=ProofOutcome.True,Message="assert is valid",PrimaryILOffset=33,MethodILOffset=0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings6.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings6.cs index bf225d7f..36131fd0 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings6.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings6.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome=ProofOutcome.Top,Message="assert unproven",PrimaryILOffset=33,MethodILOffset=0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings7.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings7.cs index 7387500e..dbe67f8f 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings7.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings7.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] diff --git a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings8.cs b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings8.cs index 504bcb9c..f7668c17 100644 --- a/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings8.cs +++ b/Microsoft.Research/RegressionTest/MaxWidenings/MaxWidenings8.cs @@ -16,9 +16,9 @@ using System.Diagnostics.Contracts; using Microsoft.Research.ClousotRegression; -namespace WideningDepth +namespace MaxWidenings { - public class WideningDepth + public class MaxWidenings { [ClousotRegressionTest] [RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as receiver)",PrimaryILOffset=1,MethodILOffset=0)] From 6cc1fafd925d87c60dfc754f63e2e249170807c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Valentin=20W=C3=BCstholz?= Date: Tue, 14 Jun 2016 20:43:53 -0500 Subject: [PATCH 4/7] Add a test. --- .../RegressionTest/ClousotTests/Tests.cs | 9 +++ .../RegressionTest/MaxJoins/MaxJoins3.cs | 81 +++++++++++++++++++ 2 files changed, 90 insertions(+) create mode 100644 Microsoft.Research/RegressionTest/MaxJoins/MaxJoins3.cs diff --git a/Microsoft.Research/RegressionTest/ClousotTests/Tests.cs b/Microsoft.Research/RegressionTest/ClousotTests/Tests.cs index e1ebf938..5aeef80b 100644 --- a/Microsoft.Research/RegressionTest/ClousotTests/Tests.cs +++ b/Microsoft.Research/RegressionTest/ClousotTests/Tests.cs @@ -63,6 +63,15 @@ private static IEnumerable TestRunDataSource references: new string[0], libPaths: new string[0], compilerCode: "CS"); + yield return new Options( + sourceFile: @"Microsoft.Research\RegressionTest\MaxJoins\MaxJoins3.cs", + clousotOptions: @"-nobox -nologo -nopex -stats=!! -stats controller -suggest=!! -infer autopropertiesensures -infer methodensures -warninglevel full -assemblyMode=standard -wp=true -premode combined -adaptive -show validations -nonnull -bounds:type:Intervals -arithmetic:type:Intervals,obl=div0,obl=negMin,obl=floatEq,obl=divOverflow,obl=intOverflow -trace suspended -maxJoins 0", + useContractReferenceAssemblies: false, + useExe: false, + compilerOptions: @"/unsafe", + references: new string[0], + libPaths: new string[0], + compilerCode: "CS"); #endregion #region MaxWidenings diff --git a/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins3.cs b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins3.cs new file mode 100644 index 00000000..722208e0 --- /dev/null +++ b/Microsoft.Research/RegressionTest/MaxJoins/MaxJoins3.cs @@ -0,0 +1,81 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// 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.Diagnostics.Contracts; +using Microsoft.Research.ClousotRegression; + +namespace MaxJoins +{ + public class MaxJoins + { + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 12, MethodILOffset = 0)] + private void Test0(bool b) + { + string s = Foo(b); + Contract.Assert(s == null); + } + + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.True, Message = @"assert is valid", PrimaryILOffset = 15, MethodILOffset = 0)] + private void Test1(int i) + { + string s = Bar(i); + Contract.Assert(s != null); + } + + [ClousotRegressionTest] + [RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"assert unproven", PrimaryILOffset = 15, MethodILOffset = 0)] + private void Test2(int i) + { + string s = FooBar(i); + Contract.Assert(s != null); + } + + [ClousotRegressionTest] + private static string Foo(bool b) + { + string result = "non-null"; + if (b) { + result = null; + } + return result; + } + + [ClousotRegressionTest] + private static string Bar(int i) + { + string x = null; + if (i < 1) { + x = "non-null"; + } else if (i < 3) { + x = Bar(i - 1); + } + return x; + } + + [ClousotRegressionTest] + private static string FooBar(int i) + { + string x = null; + if (i < 3) { + x = FooBar(i - 1); + } else if (i < 1) { + x = "non-null"; + } + return x; + } + } +} From fd0e5ffc9440f2dcf36bb63f1dfc64ee5707e56b Mon Sep 17 00:00:00 2001 From: tom-englert Date: Tue, 28 Jun 2016 16:58:01 +0200 Subject: [PATCH 5/7] Additional fix for #340: Type arguments can't start with a reserved char, so fall back to standard behavior in this case. --- System.Compiler/Reader.cs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/System.Compiler/Reader.cs b/System.Compiler/Reader.cs index b95ad1d4..1402c9fc 100644 --- a/System.Compiler/Reader.cs +++ b/System.Compiler/Reader.cs @@ -4264,10 +4264,12 @@ private string GetIdentifier(TypeNameIdentifiers identifierType) { // If processing non-type argument or a type argument with assembly name, // process the characters after the comma as an assembly name. // - // If the next character is whitespace, assume that it delineates the start of an assembly name so + // Only continue parsing the string if the next chunk of the string is the name of a type argument. + // If the next character is not a literal, it is not a type argument, so // end the current identifier by going to done label. - if (this.currentItr < this.typeNameString.Length && char.IsWhiteSpace(this.typeNameString[this.currentItr])) - { + if (this.currentItr < this.typeNameString.Length) { + var next = this.typeNameString[this.currentItr]; + if (char.IsWhiteSpace(next) || IsTypeNameReservedChar(next)) goto done; } break; From f7c92fbc56026910822903a728a6d66b6e808011 Mon Sep 17 00:00:00 2001 From: tom-englert Date: Tue, 28 Jun 2016 20:32:47 +0200 Subject: [PATCH 6/7] Add a test case and revert changes in reader as it breaks the tests. --- Foxtrot/Tests/RewriterTests/RewriterTest.cs | 11 +++ ...SystemCompilerReadGenericTypeAttributes.cs | 89 +++++++++++++++++++ System.Compiler/Reader.cs | 14 --- 3 files changed, 100 insertions(+), 14 deletions(-) create mode 100644 Foxtrot/Tests/Sources/SystemCompilerReadGenericTypeAttributes.cs diff --git a/Foxtrot/Tests/RewriterTests/RewriterTest.cs b/Foxtrot/Tests/RewriterTests/RewriterTest.cs index 39b8e626..ed0ed93c 100644 --- a/Foxtrot/Tests/RewriterTests/RewriterTest.cs +++ b/Foxtrot/Tests/RewriterTests/RewriterTest.cs @@ -1001,6 +1001,17 @@ private static IEnumerable TestFileData useBinDir: false, useExe: true, mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\SystemCompilerReadGenericTypeAttributes.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); } } diff --git a/Foxtrot/Tests/Sources/SystemCompilerReadGenericTypeAttributes.cs b/Foxtrot/Tests/Sources/SystemCompilerReadGenericTypeAttributes.cs new file mode 100644 index 00000000..dcbf1790 --- /dev/null +++ b/Foxtrot/Tests/Sources/SystemCompilerReadGenericTypeAttributes.cs @@ -0,0 +1,89 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// 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.Linq; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +using System.Threading; + +namespace Tests.Sources +{ + // a dummy class, just to make the test framework happy + public class Foo + { + public void Method(params string[] strings) + { + Contract.Requires(Contract.ForAll(strings, s => s.Length > 0)); + Console.WriteLine("Method"); + } + } + + public class C1 + { + } + public class C2 + { + } + public class C3 + { + } + + public interface I1 + { + } + + public class A1 : System.Attribute + { + public A1(Type t) + { + T = t; + } + + public Type T {get;set;} + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + new Foo().Method("1", "2", "3"); + } + else + { + new Foo().Method("1", ""); + } + } + + private interface I2 + { + } + + [A1(typeof(I1))] + private class Inner1 : I1 + { + } + + [A1(typeof(I2))] + private class Inner2 : I2 + { + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition; + public string NegativeExpectedCondition = "Contract.ForAll(strings, s => s.Length > 0)"; + } +} diff --git a/System.Compiler/Reader.cs b/System.Compiler/Reader.cs index 1402c9fc..13eb611a 100644 --- a/System.Compiler/Reader.cs +++ b/System.Compiler/Reader.cs @@ -4259,20 +4259,6 @@ private string GetIdentifier(TypeNameIdentifiers identifierType) { this.currentItr++; switch (c) { case ',': - // A comma may separate a type name from its assembly name or a type argument from - // another type argument. - // If processing non-type argument or a type argument with assembly name, - // process the characters after the comma as an assembly name. - // - // Only continue parsing the string if the next chunk of the string is the name of a type argument. - // If the next character is not a literal, it is not a type argument, so - // end the current identifier by going to done label. - if (this.currentItr < this.typeNameString.Length) { - var next = this.typeNameString[this.currentItr]; - if (char.IsWhiteSpace(next) || IsTypeNameReservedChar(next)) - goto done; - } - break; case '[': case ']': case '&': From fc1623cfa2cc334f08c45020f6e1ded046f59d50 Mon Sep 17 00:00:00 2001 From: Martin Kraus Date: Tue, 26 Jul 2016 14:20:16 +0200 Subject: [PATCH 7/7] Forced AssemblyRef flags to be ECMA compatible when writing output --- System.Compiler/Writer.cs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/System.Compiler/Writer.cs b/System.Compiler/Writer.cs index 02cefbfe..4d0b0898 100644 --- a/System.Compiler/Writer.cs +++ b/System.Compiler/Writer.cs @@ -616,6 +616,10 @@ int GetAssemblyRefIndex(AssemblyNode/*!*/ assembly) { aref.HashValue = null; aref.Flags = aref.Flags & ~AssemblyFlags.PublicKey; } + + // make sure that written flags are ECMA compatible + aref.Flags = aref.Flags & (AssemblyFlags.PublicKey | AssemblyFlags.Retargetable | AssemblyFlags.DisableJITcompileOptimizer | AssemblyFlags.EnableJITcompileTracking); + this.assemblyRefEntries.Add(aref); this.assemblyRefIndex[assembly.UniqueKey] = index; }