Make /typeEncoding:m work with arrays

7 files changed, 117 insertions, 42 deletions

diff --git a/Source/Core/AbsyType.ssc b/Source/Core/AbsyType.ssc
index 3d2ab73a..6079163a 100644
--- a/Source/Core/AbsyType.ssc
+++ b/Source/Core/AbsyType.ssc
@@ -2131,7 +2131,8 @@ namespace Microsoft.Boogie
     public override void Emit(TokenTextWriter! stream, int contextBindingStrength) 

     {

       stream.SetToken(this);

-      CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);

+      ExpandedType.Emit(stream, contextBindingStrength);      

+      // CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);

     }

 

     //-----------  Resolution  ----------------------------------

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 35e182e6..97167e18 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -153,6 +153,7 @@ namespace Microsoft.Boogie
     public BvHandling Bitvectors = BvHandling.Z3Native;

     

     public bool UseArrayTheory = false;

+    public bool MonomorphicArrays { get { return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; } }

     public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically

 

     public bool DoModSetAnalysis = false;
@@ -1324,7 +1325,7 @@ namespace Microsoft.Boogie
         OwnershipModelEncoding = OwnershipModelOption.Trivial;

       }

       

-      if (UseArrayTheory) {

+      if (MonomorphicArrays) {

         Monomorphize = true;

       }

       

diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index 3baa1d26..5dfa6468 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -132,27 +132,35 @@ void ObjectInvariant()
     {

       Contract.Requires(type != null);

       if (KnownTypes.ContainsKey(type)) return;

-      

-      if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {

+

+      if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {

         KnownTypes.Add(type, true);

         string declString = "";

         MapType mapType = type.AsMap;

-        Contract.Assert(mapType!=null);

-        

-        declString += "(DEFTYPE " +  TypeToString(type) + " :BUILTIN Array ";

-		foreach (Type t in mapType.Arguments) {

-      Contract.Assert(t!=null);

-		  RegisterType(t);

-		  declString += TypeToString(t);

-		  declString += " ";

-		}

-		RegisterType(mapType.Result);

-		declString += TypeToString(mapType.Result);

-		declString += ")";

-		AddDeclaration(declString);		

-		return;

+        Contract.Assert(mapType != null);

+

+        foreach (Type t in mapType.Arguments) {

+          Contract.Assert(t != null);

+          RegisterType(t);

+        }

+        RegisterType(mapType.Result);

+

+        declString += "(DEFTYPE " + TypeToString(type);

+

+        if (CommandLineOptions.Clo.UseArrayTheory) {

+          declString += " :BUILTIN Array ";

+          foreach (Type t in mapType.Arguments) {

+            declString += TypeToString(t);

+            declString += " ";

+          }

+          declString += TypeToString(mapType.Result);

+        }

+

+        declString += ")";

+        AddDeclaration(declString);

+        return;

       }

-      

+

       if (type.IsBv && NativeBv) {

         int bits = type.BvBits;

         string name = TypeToString(type);

@@ -212,34 +220,87 @@ void ObjectInvariant()
         }

         //

       } else if (node.Op is VCExprStoreOp) {

-        //

-        RegisterType(node[0].Type);

-        RegisterType(node[1].Type);

-        RegisterType(node[2].Type);

-        RegisterType(node.Type);

+        RegisterType(node.Type);        // this is the map type, registering it should register also the index and value types

         string name = SimplifyLikeExprLineariser.StoreOpName(node);

         if (!KnownStoreFunctions.ContainsKey(name)) {

-          AddDeclaration("(DEFOP " + name + 

-                         " " + TypeToString(node[0].Type) + 

-                         " " + TypeToString(node[1].Type) +

-                         " " + TypeToString(node[2].Type) + 

-                         " " + TypeToString(node.Type) + 

-                         " :BUILTIN store)");

+          string decl = "(DEFOP " + name;

+

+          foreach (VCExpr ch in node) {

+            decl += " " + TypeToString(ch.Type);

+          }

+          decl += " " + TypeToString(node.Type);

+

+          if (CommandLineOptions.Clo.UseArrayTheory)

+            decl += " :BUILTIN store";

+          decl += ")";

+          AddDeclaration(decl);

+

+          if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

+            var sel = SimplifyLikeExprLineariser.SelectOpName(node);

+

+            if (!KnownSelectFunctions.ContainsKey(name)) {

+              // need to declare it before reference

+              string seldecl = "(DEFOP " + sel;

+              foreach (VCExpr ch in node) {

+                seldecl += " " + TypeToString(ch.Type);

+              }

+              AddDeclaration(seldecl + ")");

+              KnownSelectFunctions.Add(name, true);

+            }

+

+            var eq = "EQ";

+            if (node[node.Arity - 1].Type.IsBool)

+              eq = "IFF";

+

+            string ax1 = "(BG_PUSH (FORALL (";

+            string ax2 = "(BG_PUSH (FORALL (";

+            string argX = "", argY = "";

+            string dist = "";

+            for (int i = 0; i < node.Arity; i++) {

+              var t = " :TYPE " + TypeToString(node[i].Type);

+              var x = " x" + i;

+              var y = " y" + i;

+              ax1 += x + t;

+              ax2 += x + t;

+              if (i != 0 && i != node.Arity - 1) {

+                argX += x;

+                argY += y;

+                ax2 += y + t;

+                dist += " (NEQ" + x + y + ")";

+              }

+            }

+            string v = " x" + (node.Arity - 1);

+            ax1 += ") ";

+            ax1 += "(" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argX + ") " + v + ")";

+            ax1 += "))";

+

+            ax2 += ") ";

+            ax2 += "(IMPLIES (OR " + dist + ") (" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argY + ") (" + sel + " x0" + argY + ")))";

+            ax2 += "))";

+

+            AddDeclaration(ax1);

+            AddDeclaration(ax2);

+          }

+          

           KnownStoreFunctions.Add(name, true);

         }

         //

       } else if (node.Op is VCExprSelectOp) {

         //

         RegisterType(node[0].Type);

-        RegisterType(node[1].Type);

-        RegisterType(node.Type);

         string name = SimplifyLikeExprLineariser.SelectOpName(node);

         if (!KnownSelectFunctions.ContainsKey(name)) {

-          AddDeclaration("(DEFOP " + name + 

-                         " " + TypeToString(node[0].Type) + 

-                         " " + TypeToString(node[1].Type) +

-                         " " + TypeToString(node.Type) + 

-                         " :BUILTIN select)");

+          string decl = "(DEFOP " + name;

+

+          foreach (VCExpr ch in node) {

+            decl += " " + TypeToString(ch.Type);

+          }

+          decl += " " + TypeToString(node.Type);

+

+          if (CommandLineOptions.Clo.UseArrayTheory)

+            decl += " :BUILTIN select";

+          decl += ")";

+          AddDeclaration(decl);

           KnownSelectFunctions.Add(name, true);

         }

         //

@@ -277,7 +338,18 @@ void ObjectInvariant()
         //

       }

 

-      return base.Visit(node, arg);

+      // What happens in base.Visit() just seems wrong. It seems to use some hack to enumerate 

+      // recursive children of current node, which doesn't seem to work for nested store expressions

+      // (the store expressions themselves get skipped).

+      var res = StandardResult(node, arg);

+      foreach (VCExpr n in node)

+      {

+        n.Accept(this, arg);

+      }

+

+      return res;

+

+      // return base.Visit(node, arg);

     }

 

     private string ExtractBuiltin(Function f) {

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index c4deb76c..5029ba53 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -727,7 +727,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
     [Pure]

     public override bool UnchangedType(Type type) {

       Contract.Requires(type != null);

-      return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.UseArrayTheory);

+      return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);

     }

 

     public VCExpr Cast(VCExpr expr, Type toType) {

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index c1a32aba..62bc72ea 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -192,7 +192,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
         storeTypes[i] = AxBuilder.T;

       }

       // Fill in the map type

-      if (CommandLineOptions.Clo.UseArrayTheory) {

+      if (CommandLineOptions.Clo.MonomorphicArrays) {

         selectTypes[i] = abstractedType;

         storeTypes[i] = abstractedType;

       } else {

@@ -223,7 +223,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
       }

       i++;

       // Fill in the map type which is the output of the store function

-      if (CommandLineOptions.Clo.UseArrayTheory)

+      if (CommandLineOptions.Clo.MonomorphicArrays)

         storeTypes[i] = abstractedType;

       else

         storeTypes[i] = AxBuilder.U;

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 9d5eef26..cf0bcaa4 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -634,7 +634,7 @@ Contract.Requires(var != null);
         mapTypeParams.Add(var);

       }

 

-      if (CommandLineOptions.Clo.UseArrayTheory)

+      if (CommandLineOptions.Clo.MonomorphicArrays)

         mapTypeSynonym = abstractedType;

       else

         mapTypeSynonym = new CtorType(Token.NoToken, synonymDecl, mapTypeParams);

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 4a13cbb5..1675a3a7 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -256,6 +256,7 @@ namespace Microsoft.Boogie.VCExprAST {
 Contract.Requires(node != null);

       Result res = StandardResult(node, arg);

 

+

       if (node.TypeParamArity == 0) {

         Contract.Assert(node.Op != null);

         VCExprOp op = node.Op;