implementing datatypes

5 files changed, 114 insertions, 4 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 5a1f8dc5..722bc99e 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -139,6 +139,28 @@ namespace Microsoft.Boogie {
       Dafny

     };

 

+    static void CreateDatatypeSelectors(Program program) {

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

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        if (decl is Function && QKeyValue.FindBoolAttribute(decl.Attributes, "constructor"))

+          constructors.Add((Function)decl);

+      }

+

+      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");

+          program.TopLevelDeclarations.Add(selector);

+        }

+        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);

+        program.TopLevelDeclarations.Add(isConstructor);

+      }

+    }

+

     static void ProcessFiles(List<string> fileNames) {

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

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {

@@ -150,6 +172,8 @@ namespace Microsoft.Boogie {
           PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

         }

 

+        CreateDatatypeSelectors(program);

+

         PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 9b4429f9..acad7833 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -161,6 +161,32 @@ namespace Microsoft.Boogie.SMTLib
 

         SendCommon("; done setting options\n");

         SendCommon(_backgroundPredicates);

+

+        

+        if (ctx.KnownDatatypeConstructors.Count > 0) {

+          string datatypeString = "";

+          foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {

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

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

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

+                datatypeString += f.Name + " ";

+              }

+              else {

+                datatypeString += "(" + f.Name + " ";

+                foreach (Variable v in f.InParams) {

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

+                }

+                datatypeString += ") ";

+              }

+            }

+            datatypeString += ") ";

+          }

+          List<string> decls = DeclCollector.GetNewDeclarations();

+          foreach (string decl in decls) {

+            SendCommon(decl);

+          }

+          SendCommon("(declare-datatypes () (" + datatypeString + "))");

+        }

       }

 

       if (!AxiomsAreSetup) {

@@ -524,6 +550,8 @@ namespace Microsoft.Boogie.SMTLib
       DeclCollector.Collect(sortedExpr);

       FeedTypeDeclsToProver();

 

+      

+

       AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));

       string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);

       Contract.Assert(res != null);

@@ -638,6 +666,8 @@ namespace Microsoft.Boogie.SMTLib
   {

     internal SMTLibProcessTheoremProver parent;

 

+    public readonly Dictionary<CtorType, List<Function>> KnownDatatypeConstructors = new Dictionary<CtorType, List<Function>>();

+

     public SMTLibProverContext(VCExpressionGenerator gen,

                                VCGenerationOptions genOptions)

       : base(gen, genOptions)

@@ -662,6 +692,16 @@ namespace Microsoft.Boogie.SMTLib
       }

       return parent.Namer.Lookup(var);

     }

+

+    public override void DeclareFunction(Function f, string attributes) {

+      if (QKeyValue.FindBoolAttribute(f.Attributes, "constructor")) {

+        CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type;

+        if (!KnownDatatypeConstructors.ContainsKey(datatype))

+          KnownDatatypeConstructors[datatype] = new List<Function>();

+        KnownDatatypeConstructors[datatype].Add(f);

+      }

+      base.DeclareFunction(f, attributes);

+    }

   }

 

   public class Factory : ProverFactory

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 36df38e3..f008bb88 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -655,14 +655,26 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      private string ExtractDatatypeSelector(Function func) {

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

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

+        }

+        else {

+          return null;

+        }

+      }

+

       public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op != null);

         string printedName;

 

         var builtin = ExtractBuiltin(op.Func);

+        var datatype = ExtractDatatypeSelector(op.Func);

         if (builtin != null)

           printedName = builtin;

+        else if (datatype != null)

+          printedName = datatype;

         else

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

         Contract.Assert(printedName != null);

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index c64dbf5e..23475242 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -55,7 +55,6 @@ void ObjectInvariant()
     private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();

     private readonly HashSet<string> KnownLBL = new HashSet<string>();

 

-

     public List<string/*!>!*/> AllDeclarations { get {

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));

 

@@ -92,7 +91,7 @@ void ObjectInvariant()
       return SMTLibExprLineariser.TypeToString(t);

     }

 

-    private string TypeToStringReg(Type t)

+    public string TypeToStringReg(Type t)

     {

       RegisterType(t);

       return TypeToString(t);

@@ -105,7 +104,7 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

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

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

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -184,13 +183,28 @@ void ObjectInvariant()
       if (type.IsBool || type.IsInt || type.IsBv)

         return;

 

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

+      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic && !IsDatatype(type)) {

         AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");

         KnownTypes.Add(type);

         return;

       }

     }

 

+    public static bool IsDatatype(Type t) {

+      CtorType ctorType = t.AsCtor;

+      if (t == null)

+        return false;

+      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");

+    }

+

     private void RegisterSelect(VCExprNAry node)

     {

       RegisterType(node[0].Type);

diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl
new file mode 100644
index 00000000..61409465
--- /dev/null
+++ b/Test/datatypes/t1.bpl
@@ -0,0 +1,20 @@
+type TT;

+type {:datatype} Tree;

+function {:constructor} leaf() : Tree;

+function {:constructor} node(value:TT, children:TreeList) : Tree;

+

+type {:datatype} TreeList;

+function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;

+function {:constructor} nil() : TreeList;

+

+procedure foo() 

+{

+  var a: Tree;

+  var b: TreeList;

+  var x: TT;

+

+  assert value#node(node(x, nil())) == x;

+  assert children#node(node(x, nil())) == nil();

+  

+  assert (cons(leaf(), nil()) == nil());

+}
\ No newline at end of file