Handle bitvectors

3 files changed, 64 insertions, 15 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 8389ed50..a8297583 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -120,7 +120,6 @@ namespace Microsoft.Boogie.SMTLib
 

     }

 

-

     public static string TypeToString(Type t)

     {

       Contract.Requires(t != null);

@@ -131,8 +130,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsInt)

         return "Int";

       else if (t.IsBv) {

-        Contract.Assert(false);

-        return "$bv" + t.BvBits;

+        return "(_ BitVec " + t.BvBits + ")";

       } else {

         StringBuilder sb = new StringBuilder();

         sb.Append("T@");

@@ -141,7 +139,16 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-

+    public static string ExtractBuiltin(Function f)

+    {

+      Contract.Requires(f != null);

+      string retVal = null;

+      retVal = f.FindStringAttribute("bvbuiltin");

+      if (retVal == null) {

+        retVal = f.FindStringAttribute("builtin");

+      }

+      return retVal;

+    }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

@@ -508,19 +515,42 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' };

       public bool VisitBvOp(VCExprNAry node, LineariserOptions options)

       {

-       { Contract.Assert(false); throw new NotImplementedException(); }       // TODO

+        var lit = (VCExprIntLit)node[0];

+        var bytes = lit.Val.ToByteArray();

+        if (node.Type.BvBits % 8 == 0) {

+          wr.Write("#x");

+          for (var pos = node.Type.BvBits / 8 - 1; pos >= 0; pos--) {

+            var k = pos < bytes.Length ? bytes[pos] : 0;

+            wr.Write(hex[k >> 4]);

+            wr.Write(hex[k & 0xf]);

+          }

+        } else {

+          wr.Write("#b");

+          for (var pos = node.Type.BvBits - 1; pos >= 0; pos--) {

+            var i = pos >> 3;

+            var k = i < bytes.Length ? bytes[i] : 0;

+            wr.Write((k & (1 << (pos & 7))) == 0 ? '0' : '1');

+          }

+        }

+        return true;

       }

 

       public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options)

       {

-       { Contract.Assert(false); throw new NotImplementedException(); }       // TODO

+        var op = (VCExprBvExtractOp)node.Op;

+        wr.Write("((_ extract {0} {1}) ", op.End - 1, op.Start);

+        ExprLineariser.Linearise(node[0], options);

+        wr.Write(")");

+        return true;

       }

 

       public bool VisitBvConcatOp(VCExprNAry node, LineariserOptions options)

       {

-       { Contract.Assert(false); throw new NotImplementedException(); }       // TODO

+        WriteApplication("concat", node, options);

+        return true;

       }

 

       public bool VisitAddOp(VCExprNAry node, LineariserOptions options)

@@ -593,7 +623,13 @@ namespace Microsoft.Boogie.SMTLib
       {

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op != null);

-        string printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);

+        string printedName;

+

+        var builtin = ExtractBuiltin(op.Func);

+        if (builtin != null)

+          printedName = builtin;

+        else

+          printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);

         Contract.Assert(printedName != null);

 

         WriteApplication(printedName, node, options);

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 80de8e3f..8a40bd84 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -25,6 +25,15 @@ namespace Microsoft.Boogie.SMTLib
       "=>", // implies (sic!)

       // Integers

       "Int", "*", "/", "-", "+", "<", "<=", ">", ">=",

+      // Bitvectors

+      "extract", "concat", 

+      "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",

+      // Z3 (and not only?) extensions to bitvectors

+      "bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0",

+      "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",

+      "bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend", 

+      "repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr",

+      "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int",

       // SMT v1 stuff

       "flet", "implies", "!=", "if_then_else",

       // Z3 extensions

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index a4af7f40..327b2f70 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -110,13 +110,17 @@ void ObjectInvariant()
         if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

-          string printedName = Namer.GetQuotedName(f, f.Name);

-          Contract.Assert(printedName != null);

-

-          Contract.Assert(f.OutParams.Length == 1);

-          var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

-          string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

-          AddDeclaration(decl);

+          

+          var builtin = SMTLibExprLineariser.ExtractBuiltin(f);

+          if (builtin == null) {

+            string printedName = Namer.GetQuotedName(f, f.Name);

+            Contract.Assert(printedName != null);

+

+            Contract.Assert(f.OutParams.Length == 1);

+            var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

+            string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

+            AddDeclaration(decl);

+          }

           KnownFunctions.Add(f, true);

         } else {

           var lab = node.Op as VCExprLabelOp;