From 75cdf16714372ec03f1697450c135acdd3df9db3 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 29 Sep 2009 06:39:10 +0000 Subject: Fixed some bugs in the generation of bitvector input for Z3. Deleted/ignored some binaries in the Binaries directory. --- Binaries/..svnbridge/Microsoft.SpecSharp.pdb | 1 - Binaries/..svnbridge/Mscorlib.Contracts.dll | 1 - Binaries/..svnbridge/System.Compiler.Contracts.dll | 1 - .../System.Compiler.Framework.Contracts.dll | 1 - Binaries/..svnbridge/System.Compiler.Framework.dll | 1 - Binaries/..svnbridge/System.Compiler.Framework.pdb | 1 - Binaries/..svnbridge/System.Compiler.dll | 1 - Binaries/..svnbridge/System.Compiler.pdb | 1 - Binaries/..svnbridge/System.Contracts.dll | 1 - Binaries/..svnbridge/System.Xml.Contracts.dll | 1 - Binaries/..svnbridge/microsoft.specsharp.dll | 1 - Binaries/Microsoft.SpecSharp.pdb | Bin 615936 -> 0 bytes Binaries/Mscorlib.Contracts.dll | Bin 884736 -> 0 bytes Binaries/System.Compiler.Contracts.dll | Bin 57344 -> 0 bytes Binaries/System.Compiler.Framework.Contracts.dll | Bin 16384 -> 0 bytes Binaries/System.Compiler.Framework.dll | Bin 1187840 -> 0 bytes Binaries/System.Compiler.Framework.pdb | Bin 2569728 -> 0 bytes Binaries/System.Compiler.dll | Bin 872448 -> 0 bytes Binaries/System.Compiler.pdb | Bin 2270720 -> 0 bytes Binaries/System.Contracts.dll | Bin 237568 -> 0 bytes Binaries/System.Xml.Contracts.dll | Bin 20480 -> 0 bytes Binaries/microsoft.specsharp.dll | Bin 491520 -> 0 bytes Source/Provers/Z3/TypeDeclCollector.ssc | 2 +- Source/VCExpr/SimplifyLikeLineariser.ssc | 4 +- Source/VCExpr/VCExprAST.ssc | 47 +++++++++++++++++---- Source/VCExpr/VCExprASTVisitors.ssc | 2 +- Test/bitvectors/Answer | 3 ++ Test/bitvectors/bv8.bpl | 23 ++++++++++ Test/bitvectors/runtest.bat | 9 ++-- 29 files changed, 72 insertions(+), 29 deletions(-) delete mode 100644 Binaries/..svnbridge/Microsoft.SpecSharp.pdb delete mode 100644 Binaries/..svnbridge/Mscorlib.Contracts.dll delete mode 100644 Binaries/..svnbridge/System.Compiler.Contracts.dll delete mode 100644 Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll delete mode 100644 Binaries/..svnbridge/System.Compiler.Framework.dll delete mode 100644 Binaries/..svnbridge/System.Compiler.Framework.pdb delete mode 100644 Binaries/..svnbridge/System.Compiler.dll delete mode 100644 Binaries/..svnbridge/System.Compiler.pdb delete mode 100644 Binaries/..svnbridge/System.Contracts.dll delete mode 100644 Binaries/..svnbridge/System.Xml.Contracts.dll delete mode 100644 Binaries/..svnbridge/microsoft.specsharp.dll delete mode 100644 Binaries/Microsoft.SpecSharp.pdb delete mode 100644 Binaries/Mscorlib.Contracts.dll delete mode 100644 Binaries/System.Compiler.Contracts.dll delete mode 100644 Binaries/System.Compiler.Framework.Contracts.dll delete mode 100644 Binaries/System.Compiler.Framework.dll delete mode 100644 Binaries/System.Compiler.Framework.pdb delete mode 100644 Binaries/System.Compiler.dll delete mode 100644 Binaries/System.Compiler.pdb delete mode 100644 Binaries/System.Contracts.dll delete mode 100644 Binaries/System.Xml.Contracts.dll delete mode 100644 Binaries/microsoft.specsharp.dll create mode 100644 Test/bitvectors/bv8.bpl diff --git a/Binaries/..svnbridge/Microsoft.SpecSharp.pdb b/Binaries/..svnbridge/Microsoft.SpecSharp.pdb deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/Microsoft.SpecSharp.pdb +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/Mscorlib.Contracts.dll b/Binaries/..svnbridge/Mscorlib.Contracts.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/Mscorlib.Contracts.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.Contracts.dll b/Binaries/..svnbridge/System.Compiler.Contracts.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.Contracts.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll b/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.Framework.dll b/Binaries/..svnbridge/System.Compiler.Framework.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.Framework.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.Framework.pdb b/Binaries/..svnbridge/System.Compiler.Framework.pdb deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.Framework.pdb +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.dll b/Binaries/..svnbridge/System.Compiler.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Compiler.pdb b/Binaries/..svnbridge/System.Compiler.pdb deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Compiler.pdb +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Contracts.dll b/Binaries/..svnbridge/System.Contracts.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Contracts.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/System.Xml.Contracts.dll b/Binaries/..svnbridge/System.Xml.Contracts.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/System.Xml.Contracts.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/..svnbridge/microsoft.specsharp.dll b/Binaries/..svnbridge/microsoft.specsharp.dll deleted file mode 100644 index 08149303..00000000 --- a/Binaries/..svnbridge/microsoft.specsharp.dll +++ /dev/null @@ -1 +0,0 @@ -svn:mime-typeapplication/octet-stream \ No newline at end of file diff --git a/Binaries/Microsoft.SpecSharp.pdb b/Binaries/Microsoft.SpecSharp.pdb deleted file mode 100644 index 9fa6f932..00000000 Binary files a/Binaries/Microsoft.SpecSharp.pdb and /dev/null differ diff --git a/Binaries/Mscorlib.Contracts.dll b/Binaries/Mscorlib.Contracts.dll deleted file mode 100644 index b0aeeb5f..00000000 Binary files a/Binaries/Mscorlib.Contracts.dll and /dev/null differ diff --git a/Binaries/System.Compiler.Contracts.dll b/Binaries/System.Compiler.Contracts.dll deleted file mode 100644 index 6a573ef8..00000000 Binary files a/Binaries/System.Compiler.Contracts.dll and /dev/null differ diff --git a/Binaries/System.Compiler.Framework.Contracts.dll b/Binaries/System.Compiler.Framework.Contracts.dll deleted file mode 100644 index 50726f3e..00000000 Binary files a/Binaries/System.Compiler.Framework.Contracts.dll and /dev/null differ diff --git a/Binaries/System.Compiler.Framework.dll b/Binaries/System.Compiler.Framework.dll deleted file mode 100644 index 0c891dd0..00000000 Binary files a/Binaries/System.Compiler.Framework.dll and /dev/null differ diff --git a/Binaries/System.Compiler.Framework.pdb b/Binaries/System.Compiler.Framework.pdb deleted file mode 100644 index 7e580bd1..00000000 Binary files a/Binaries/System.Compiler.Framework.pdb and /dev/null differ diff --git a/Binaries/System.Compiler.dll b/Binaries/System.Compiler.dll deleted file mode 100644 index 645853a1..00000000 Binary files a/Binaries/System.Compiler.dll and /dev/null differ diff --git a/Binaries/System.Compiler.pdb b/Binaries/System.Compiler.pdb deleted file mode 100644 index 328e2aa4..00000000 Binary files a/Binaries/System.Compiler.pdb and /dev/null differ diff --git a/Binaries/System.Contracts.dll b/Binaries/System.Contracts.dll deleted file mode 100644 index ed1ae103..00000000 Binary files a/Binaries/System.Contracts.dll and /dev/null differ diff --git a/Binaries/System.Xml.Contracts.dll b/Binaries/System.Xml.Contracts.dll deleted file mode 100644 index 1ba5ec57..00000000 Binary files a/Binaries/System.Xml.Contracts.dll and /dev/null differ diff --git a/Binaries/microsoft.specsharp.dll b/Binaries/microsoft.specsharp.dll deleted file mode 100644 index b63cc192..00000000 Binary files a/Binaries/microsoft.specsharp.dll and /dev/null differ diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc index 86307b45..8173f7f3 100644 --- a/Source/Provers/Z3/TypeDeclCollector.ssc +++ b/Source/Provers/Z3/TypeDeclCollector.ssc @@ -117,7 +117,7 @@ namespace Microsoft.Boogie.Z3 // there are a couple of cases where operators have to be // registered by generating appropriate Z3 statements - if (node.Op.Equals(VCExpressionGenerator.BvConcatOp)) { + if (node.Op is VCExprBvConcatOp) { // if (NativeBv) { RegisterType(node[0].Type); diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 7aff8e87..7b6bb5c8 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -218,7 +218,7 @@ namespace Microsoft.Boogie.VCExprAST } public static string! BvConcatOpName(VCExprNAry! node) - requires node.Op.Equals(VCExpressionGenerator.BvConcatOp); { + requires node.Op is VCExprBvConcatOp; { int bits1 = node[0].Type.BvBits; int bits2 = node[1].Type.BvBits; return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]"; @@ -227,7 +227,7 @@ namespace Microsoft.Boogie.VCExprAST public static string! BvExtractOpName(VCExprNAry! node) requires node.Op is VCExprBvExtractOp; { VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op; - return "$bv" + node.Type.BvBits + "_extract[" + op.Start + ":" + op.End + "]"; + return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]"; } internal void WriteId(string! s) { diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc index 330c76c4..4d9d4c20 100644 --- a/Source/VCExpr/VCExprAST.ssc +++ b/Source/VCExpr/VCExprAST.ssc @@ -202,12 +202,11 @@ namespace Microsoft.Boogie } public VCExpr! BvExtract(VCExpr! bv, int bits, int start, int end) { - return Function(new VCExprBvExtractOp (start, end), bv); + return Function(new VCExprBvExtractOp(start, end, bits), bv); } - public static readonly VCExprBvConcatOp! BvConcatOp = new VCExprBvConcatOp(); public VCExpr! BvConcat(VCExpr! bv1, VCExpr! bv2) { - return Function(BvConcatOp, bv1, bv2); + return Function(new VCExprBvConcatOp(bv1.Type.BvBits, bv2.Type.BvBits), bv1, bv2); } public VCExpr! AtMost(VCExpr! smaller, VCExpr! greater) { @@ -244,7 +243,6 @@ namespace Microsoft.Boogie SingletonOpDict.Add(GeOp, SingletonOp.GeOp); SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp); SingletonOpDict.Add(Subtype3Op,SingletonOp.Subtype3Op); - SingletonOpDict.Add(BvConcatOp,SingletonOp.BvConcatOp); } //////////////////////////////////////////////////////////////////////////////// @@ -995,6 +993,7 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprBvExtractOp : VCExprOp { public readonly int Start; public readonly int End; + public readonly int Total; // the number of bits from which the End-Start bits are extracted public override int Arity { get { return 1; } } public override int TypeParamArity { get { return 0; } } @@ -1008,18 +1007,21 @@ namespace Microsoft.Boogie.VCExprAST return true; if (that is VCExprBvExtractOp) { VCExprBvExtractOp! thatExtract = (VCExprBvExtractOp)that; - return this.Start == thatExtract.Start && this.End == thatExtract.End; + return this.Start == thatExtract.Start && this.End == thatExtract.End && this.Total == thatExtract.Total; } return false; } [Pure] public override int GetHashCode() { - return Start * 81912 + End * 978132; + return Start * 81912 + End * 978132 + Total * 571289; } - internal VCExprBvExtractOp(int start, int end) { + internal VCExprBvExtractOp(int start, int end, int total) + requires 0 <= start && start <= end && end <= total; + { this.Start = start; this.End = end; + this.Total = total; } public override Result Accept (VCExprNAry! expr, IVCExprOpVisitor! visitor, Arg arg) { @@ -1027,14 +1029,41 @@ namespace Microsoft.Boogie.VCExprAST } } - // singleton class public class VCExprBvConcatOp : VCExprOp { + public readonly int LeftSize; + public readonly int RightSize; + public override int Arity { get { return 2; } } public override int TypeParamArity { get { return 0; } } public override Type! InferType(List! args, List! typeArgs) { return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits); } - internal VCExprBvConcatOp() {} + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprBvConcatOp) { + VCExprBvConcatOp thatConcat = (VCExprBvConcatOp)that; + return this.LeftSize == thatConcat.LeftSize && this.RightSize == thatConcat.RightSize; + } + return false; + } + [Pure] + public override int GetHashCode() { + return LeftSize * 81912 + RightSize * 978132; + } + + internal VCExprBvConcatOp(int leftSize, int rightSize) + requires 0 <= leftSize && 0 <= rightSize; + { + this.LeftSize = leftSize; + this.RightSize = rightSize; + } + public override Result Accept + (VCExprNAry! expr, IVCExprOpVisitor! visitor, Arg arg) { + return visitor.VisitBvConcatOp(expr, arg); + } } ///////////////////////////////////////////////////////////////////////////////// diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc index cbb4ab8f..47865747 100644 --- a/Source/VCExpr/VCExprASTVisitors.ssc +++ b/Source/VCExpr/VCExprASTVisitors.ssc @@ -81,7 +81,7 @@ namespace Microsoft.Boogie.VCExprAST VCExprOp! op = node.Op; IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); - enumerator.MoveNext(); + enumerator.MoveNext(); // skip the node itself while (enumerator.MoveNext()) { VCExpr! expr = (VCExpr!)enumerator.Current; diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index 9ad91f5b..251853ca 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -60,3 +60,6 @@ Execution trace: bv6.bpl(5,5): anon0 Boogie program verifier finished with 0 verified, 1 error +-------------------- bv8.bpl -------------------- + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl new file mode 100644 index 00000000..7295f684 --- /dev/null +++ b/Test/bitvectors/bv8.bpl @@ -0,0 +1,23 @@ +// This file includes some tests for which Boogie once generated bad Z3 input + +procedure foo() +{ + var r: bv3; + var s: bv6; + var u: bv15; + var t: bv24; + + t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; + t := (r ++ s) ++ u; + t := t[16: 0] ++ t[8: 0]; +} + +procedure bar() +{ + var a: bv64; + var b: bv32; + var c: bv8; + + c := a[8:0]; + c := b[8:0]; +} diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat index 0b05e986..0fc17990 100644 --- a/Test/bitvectors/runtest.bat +++ b/Test/bitvectors/runtest.bat @@ -14,8 +14,7 @@ echo -------------------- vcc0.bpl - toInt -------------------- echo -------------------- bv4.bpl - /bv:n -------------------- %BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl -echo -------------------- bv5.bpl -------------------- -%BGEXE% /bv:z %* /logPrefix:-1 bv5.bpl - -echo -------------------- bv6.bpl -------------------- -%BGEXE% /bv:z %* /logPrefix:-1 bv6.bpl +for %%f in (bv5.bpl bv6.bpl bv8.bpl) do ( + echo -------------------- %%f -------------------- + %BGEXE% %* %%f +) -- cgit v1.2.3