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

Deleted/ignored some binaries in the Binaries directory.

4 files changed, 42 insertions, 13 deletions

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;