fixed datatype bug reported by Chris

fixed function body referring to globals bug

6 files changed, 133 insertions, 56 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 967ac4e3..616a0e21 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2009,7 +2009,11 @@ namespace Microsoft.Boogie {
         RegisterFormals(OutParams, rc);

         ResolveAttributes(rc);

         if (Body != null)

-          Body.Resolve(rc);

+        {

+            rc.StateMode = ResolutionContext.State.StateLess;

+            Body.Resolve(rc);

+            rc.StateMode = ResolutionContext.State.Single;

+        }

         rc.PopVarContext();

         Type.CheckBoundVariableOccurrences(TypeParameters,

                                            InParams.ToTypeSeq, OutParams.ToTypeSeq,

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bca0dd80..3df1bd32 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -195,69 +195,123 @@ namespace Microsoft.Boogie.SMTLib
         currentLogFile.WriteLine(s);

     }

 

-    private void PrepareCommon()

+    private void FindDependentTypes(Type type, List<CtorType> dependentTypes)

     {

-      if (common.Length == 0) {

-        SendCommon("(set-option :print-success false)");

-        SendCommon("(set-info :smt-lib-version 2.0)");

-        if (options.ProduceModel())

-          SendCommon("(set-option :produce-models true)");

-        foreach (var opt in options.SmtOptions) {

-          SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

+        MapType mapType = type as MapType;

+        if (mapType != null)

+        {

+            foreach (Type t in mapType.Arguments)

+            {

+                FindDependentTypes(t, dependentTypes);

+            }

+            FindDependentTypes(mapType.Result, dependentTypes);

         }

-

-        if (!string.IsNullOrEmpty(options.Logic)) {

-          SendCommon("(set-logic " + options.Logic + ")");

+        CtorType ctorType = type as CtorType;

+        if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType))

+        {

+            dependentTypes.Add(ctorType);

         }

+    }

 

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

-        SendCommon(_backgroundPredicates);

+    private void PrepareCommon()

+    {

+        if (common.Length == 0)

+        {

+            SendCommon("(set-option :print-success false)");

+            SendCommon("(set-info :smt-lib-version 2.0)");

+            if (options.ProduceModel())

+                SendCommon("(set-option :produce-models true)");

+            foreach (var opt in options.SmtOptions)

+            {

+                SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

+            }

 

-        if (options.UseTickleBool) {

-          SendCommon("(declare-fun tickleBool (Bool) Bool)");

-          SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

-        }

-        

-        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]) {

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

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

-                datatypeString += quotedConstructorName + " ";

-              }

-              else {

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

-                foreach (Variable v in f.InParams) {

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

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

+            if (!string.IsNullOrEmpty(options.Logic))

+            {

+                SendCommon("(set-logic " + options.Logic + ")");

+            }

+

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

+            SendCommon(_backgroundPredicates);

+

+            if (options.UseTickleBool)

+            {

+                SendCommon("(declare-fun tickleBool (Bool) Bool)");

+                SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

+            }

+

+            if (ctx.KnownDatatypeConstructors.Count > 0)

+            {

+                GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();

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

+                {

+                    dependencyGraph.AddSource(datatype);

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

+                    {

+                        List<CtorType> dependentTypes = new List<CtorType>();

+                        foreach (Variable v in f.InParams)

+                        {

+                            FindDependentTypes(v.TypedIdent.Type, dependentTypes);

+                        }

+                        foreach (CtorType result in dependentTypes)

+                        {

+                            dependencyGraph.AddEdge(datatype, result);

+                        }

+                    }

+                }

+                GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);

+                sccs.Compute();

+                foreach (GraphUtil.SCC<CtorType> scc in sccs)

+                {

+                    string datatypeString = "";

+                    foreach (CtorType datatype in scc)

+                    {

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

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

+                        {

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

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

+                            {

+                                datatypeString += quotedConstructorName + " ";

+                            }

+                            else

+                            {

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

+                                foreach (Variable v in f.InParams)

+                                {

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

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

+                                }

+                                datatypeString += ") ";

+                            }

+                        }

+                        datatypeString += ") ";

+                    }

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

+                    foreach (string decl in decls)

+                    {

+                        SendCommon(decl);

+                    }

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

                 }

-                datatypeString += ") ";

-              }

             }

-            datatypeString += ") ";

-          }

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

-          foreach (string decl in decls) {

-            SendCommon(decl);

-          }

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

         }

-      }

 

-      if (!AxiomsAreSetup) {

-        var axioms = ctx.Axioms;

-        var nary = axioms as VCExprNAry;

-        if (nary != null && nary.Op == VCExpressionGenerator.AndOp)

-          foreach (var expr in nary.UniformArguments) {

-            var str = VCExpr2String(expr, -1);

-            if (str != "true")

-              AddAxiom(str);

-          } else

-          AddAxiom(VCExpr2String(axioms, -1));

-        AxiomsAreSetup = true;

-      }

+        if (!AxiomsAreSetup)

+        {

+            var axioms = ctx.Axioms;

+            var nary = axioms as VCExprNAry;

+            if (nary != null && nary.Op == VCExpressionGenerator.AndOp)

+                foreach (var expr in nary.UniformArguments)

+                {

+                    var str = VCExpr2String(expr, -1);

+                    if (str != "true")

+                        AddAxiom(str);

+                }

+            else

+                AddAxiom(VCExpr2String(axioms, -1));

+            AxiomsAreSetup = true;

+        }

     }

 

     public override int FlushAxiomsToTheoremProver()

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index c2d68fc8..c58d3349 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -171,6 +171,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\..\Graph\Graph.csproj">

+      <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>

+      <Name>Graph</Name>

+    </ProjectReference>

     <ProjectReference Include="..\..\Model\Model.csproj">

       <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer
index 7b7b411a..bac8f345 100644
--- a/Test/datatypes/Answer
+++ b/Test/datatypes/Answer
@@ -12,3 +12,7 @@ Execution trace:
     t2.bpl(16,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+

+-------------------- ex.bpl --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/datatypes/ex.bpl b/Test/datatypes/ex.bpl
new file mode 100644
index 00000000..32b302f3
--- /dev/null
+++ b/Test/datatypes/ex.bpl
@@ -0,0 +1,11 @@
+type{:datatype} finite_map;

+function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;

+

+type{:datatype} partition;

+function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;

+

+procedure P(arr:finite_map)

+  requires dom#finite_map(arr)[0];

+  ensures  dom#finite_map(arr)[0];

+{

+}

diff --git a/Test/datatypes/runtest.bat b/Test/datatypes/runtest.bat
index fe2aa09d..2ff4bad8 100644
--- a/Test/datatypes/runtest.bat
+++ b/Test/datatypes/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

-for %%f in (t1.bpl t2.bpl) do (

+for %%f in (t1.bpl t2.bpl ex.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BPLEXE% %* /typeEncoding:m %%f