fixed problems with datatypes

removed stale contracts in stratified inlining
added test to datatypes

5 files changed, 64 insertions, 47 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index fc28100e..500cb0ca 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -214,39 +214,27 @@ namespace Microsoft.Boogie {
     }

 

     void CreateDatatypeSelectorsAndTesters() {

-      HashSet<string> functions = new HashSet<string>();

-      List<Function> constructors = new List<Function>();

+      Dictionary<string, Function> constructors = new Dictionary<string, Function>();

+      List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();

       foreach (Declaration decl in TopLevelDeclarations) {

         Function func = decl as Function;

-        if (func == null) continue;

-        functions.Add(func.Name);

-        if (QKeyValue.FindBoolAttribute(func.Attributes, "constructor"))

-          constructors.Add(func);

-      }

-

-      foreach (Function f in constructors) {

-        foreach (Variable v in f.InParams) {

-          Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-          Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);

-          Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);

-          selector.AddAttribute("selector");

-          for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-            if (kv.Key == "constructor") continue;

-            selector.AddAttribute(kv.Key, kv.Params.ToArray());

-          }

-          if (!functions.Contains(selector.Name))

-            TopLevelDeclarations.Add(selector);

+        if (func == null || !QKeyValue.FindBoolAttribute(decl.Attributes, "constructor")) {

+          prunedTopLevelDeclarations.Add(decl);

+          continue;

         }

-        Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-        Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);

-        Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);

-        for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-          if (kv.Key == "constructor") continue;

-          isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());

+        if (constructors.ContainsKey(func.Name)) continue;

+        constructors.Add(func.Name, func);

+        prunedTopLevelDeclarations.Add(func);

+      }

+      TopLevelDeclarations = prunedTopLevelDeclarations;

+

+      foreach (Function f in constructors.Values) {

+        for (int i = 0; i < f.InParams.Length; i++) {

+          DatatypeSelector selector = new DatatypeSelector(f, i);

+          TopLevelDeclarations.Add(selector);

         }

-        isConstructor.AddAttribute("membership");

-        if (!functions.Contains(isConstructor.Name))

-          TopLevelDeclarations.Add(isConstructor);

+        DatatypeMembership membership = new DatatypeMembership(f);

+        TopLevelDeclarations.Add(membership);

       }

     }

 

@@ -1803,7 +1791,34 @@ namespace Microsoft.Boogie {
     }

   }

 

-  

+  public class DatatypeSelector : Function {

+    public Function constructor;

+    public int index;

+    public DatatypeSelector(Function constructor, int index)

+      : base(constructor.tok, 

+             constructor.InParams[index].Name + "#" + constructor.Name,

+             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.InParams[index].TypedIdent.Type), false)) 

+    {

+      this.constructor = constructor;

+      this.index = index;

+    }

+    public override void Emit(TokenTextWriter stream, int level) { }

+  }

+

+  public class DatatypeMembership : Function {

+    public Function constructor;

+    public DatatypeMembership(Function constructor)

+      : base(constructor.tok, 

+             "is#" + constructor.Name,

+             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new Formal(constructor.tok, new TypedIdent(constructor.tok, "", Type.Bool), false)) 

+    {

+      this.constructor = constructor;

+    }

+    public override void Emit(TokenTextWriter stream, int level) {

+    }

+  }

 

   public class Function : DeclWithFormals {

     public string Comment;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d3448b5d..dab0807f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -206,13 +206,15 @@ namespace Microsoft.Boogie.SMTLib
           foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {

             datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";

             foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {

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

               if (f.InParams.Length == 0) {

-                datatypeString += Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += quotedConstructorName + " ";

               }

               else {

-                datatypeString += "(" + Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += "(" + quotedConstructorName + " ";

                 foreach (Variable v in f.InParams) {

-                  datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

+                  string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);

+                  datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

                 }

                 datatypeString += ") ";

               }

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 8d4a4256..635280d1 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -660,11 +660,14 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       private string ExtractDatatype(Function func) {

-        if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {

-          return func.Name.Remove(func.Name.IndexOf('#'));

-        }

-        else if (QKeyValue.FindBoolAttribute(func.Attributes, "membership")) {

-          return func.Name.Replace('#', '-');

+        if (func is DatatypeSelector) {

+          DatatypeSelector selector = (DatatypeSelector) func;

+          Variable v = selector.constructor.InParams[selector.index];

+          return ExprLineariser.Namer.GetQuotedName(v, v.Name + "#" + selector.constructor.Name);

+        }

+        else if (func is DatatypeMembership) {

+          DatatypeMembership membership = (DatatypeMembership)func;

+          return ExprLineariser.Namer.GetQuotedName(membership, "is-" + membership.constructor.Name);

         }

         else {

           return null;

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 0bc41c2a..4a4ecfb6 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -171,7 +171,7 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-        if (op != null && !IsDatatypeConstructor(op.Func) && !KnownFunctions.Contains(op.Func)) {

+        if (op != null && !IsDatatypeFunction(op.Func) && !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -264,12 +264,11 @@ void ObjectInvariant()
       return QKeyValue.FindBoolAttribute(ctorType.Decl.Attributes, "datatype");

     }

 

-    public static bool IsDatatypeConstructor(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "constructor");

-    }

-

-    public static bool IsDatatypeSelector(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "selector");

+    public static bool IsDatatypeFunction(Function f) {

+      return

+        QKeyValue.FindBoolAttribute(f.Attributes, "constructor") ||

+        f is DatatypeSelector ||

+        f is DatatypeMembership;

     }

 

     private void RegisterSelect(VCExprNAry node)

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 26361cdf..ed698d5f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -25,12 +25,10 @@ namespace Microsoft.Boogie {
 

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(counterexample != null);

       Contract.Invariant(cce.NonNullElements(args));

     }

 

     public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {

-      Contract.Requires(cex != null);

       Contract.Requires(cce.NonNullElements(x));

       counterexample = cex;

       args = x;