Fixed some bugs in the generation of bitvector input for Z3.

Deleted/ignored some binaries in the Binaries directory.

29 files changed, 72 insertions, 29 deletions

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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ 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
--- a/Binaries/Microsoft.SpecSharp.pdb
+++ /dev/null
diff --git a/Binaries/Mscorlib.Contracts.dll b/Binaries/Mscorlib.Contracts.dll
deleted file mode 100644
index b0aeeb5f..00000000
--- a/Binaries/Mscorlib.Contracts.dll
+++ /dev/null
diff --git a/Binaries/System.Compiler.Contracts.dll b/Binaries/System.Compiler.Contracts.dll
deleted file mode 100644
index 6a573ef8..00000000
--- a/Binaries/System.Compiler.Contracts.dll
+++ /dev/null
diff --git a/Binaries/System.Compiler.Framework.Contracts.dll b/Binaries/System.Compiler.Framework.Contracts.dll
deleted file mode 100644
index 50726f3e..00000000
--- a/Binaries/System.Compiler.Framework.Contracts.dll
+++ /dev/null
diff --git a/Binaries/System.Compiler.Framework.dll b/Binaries/System.Compiler.Framework.dll
deleted file mode 100644
index 0c891dd0..00000000
--- a/Binaries/System.Compiler.Framework.dll
+++ /dev/null
diff --git a/Binaries/System.Compiler.Framework.pdb b/Binaries/System.Compiler.Framework.pdb
deleted file mode 100644
index 7e580bd1..00000000
--- a/Binaries/System.Compiler.Framework.pdb
+++ /dev/null
diff --git a/Binaries/System.Compiler.dll b/Binaries/System.Compiler.dll
deleted file mode 100644
index 645853a1..00000000
--- a/Binaries/System.Compiler.dll
+++ /dev/null
diff --git a/Binaries/System.Compiler.pdb b/Binaries/System.Compiler.pdb
deleted file mode 100644
index 328e2aa4..00000000
--- a/Binaries/System.Compiler.pdb
+++ /dev/null
diff --git a/Binaries/System.Contracts.dll b/Binaries/System.Contracts.dll
deleted file mode 100644
index ed1ae103..00000000
--- a/Binaries/System.Contracts.dll
+++ /dev/null
diff --git a/Binaries/System.Xml.Contracts.dll b/Binaries/System.Xml.Contracts.dll
deleted file mode 100644
index 1ba5ec57..00000000
--- a/Binaries/System.Xml.Contracts.dll
+++ /dev/null
diff --git a/Binaries/microsoft.specsharp.dll b/Binaries/microsoft.specsharp.dll
deleted file mode 100644
index b63cc192..00000000
--- a/Binaries/microsoft.specsharp.dll
+++ /dev/null
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<Result, Arg>

            (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! 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<VCExpr!>! args, List<Type!>! 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<Result, Arg>

+           (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! 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

+)