From 0faac5618039d3617b676c24e9465f712072adf3 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 00:29:15 +0000 Subject: Boogie: Graph port 3/3: Committing changed references; also, adding back cce files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min. --- Source/AIFramework/AIFramework.csproj | 4 +- Source/AIFramework/cce.cs | 8 +- Source/AbsInt/AbsInt.csproj | 1 + Source/Boogie.sln | 24 ++-- Source/BoogieDriver/BoogieDriver.csproj | 5 +- Source/Core/Core.csproj | 5 +- Source/Core/cce.cs | 30 +++-- Source/Provers/Isabelle/Isabelle.csproj | 1 + Source/Provers/Isabelle/cce.cs | 193 ++++++++++++++++++++++++++++++++ Source/Provers/SMTLib/SMTLib.csproj | 1 + Source/Provers/SMTLib/cce.cs | 193 ++++++++++++++++++++++++++++++++ Source/Provers/Simplify/Simplify.csproj | 5 +- Source/Provers/Simplify/cce.cs | 193 ++++++++++++++++++++++++++++++++ Source/Provers/Z3/Z3.csproj | 1 + Source/Provers/Z3/cce.cs | 193 ++++++++++++++++++++++++++++++++ Source/VCExpr/VCExpr.csproj | 1 + Source/VCExpr/cce.cs | 117 ++++++++++++++----- Source/VCGeneration/VCGeneration.csproj | 5 +- 18 files changed, 916 insertions(+), 64 deletions(-) create mode 100644 Source/Provers/Isabelle/cce.cs create mode 100644 Source/Provers/SMTLib/cce.cs create mode 100644 Source/Provers/Simplify/cce.cs create mode 100644 Source/Provers/Z3/cce.cs (limited to 'Source') diff --git a/Source/AIFramework/AIFramework.csproj b/Source/AIFramework/AIFramework.csproj index bddd07f2..224be513 100644 --- a/Source/AIFramework/AIFramework.csproj +++ b/Source/AIFramework/AIFramework.csproj @@ -70,7 +70,9 @@ - + + Code + diff --git a/Source/AIFramework/cce.cs b/Source/AIFramework/cce.cs index 76deba32..ef594484 100644 --- a/Source/AIFramework/cce.cs +++ b/Source/AIFramework/cce.cs @@ -3,7 +3,7 @@ using SA=System.Attribute; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Text; -using Microsoft.Boogie; +//using Microsoft.Boogie; /// /// A class containing static methods to extend the functionality of Code Contracts @@ -131,9 +131,9 @@ public static class cce { // return toRet; //} - internal static bool NonNullElements(Set set) { - return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); - } + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} } public class PeerAttribute : SA { diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index c5601053..62d90dff 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -81,6 +81,7 @@ + diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 9020382d..8ac6b180 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -5,8 +5,6 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758 EndProject Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Basetypes", "Basetypes\Basetypes.sscproj", "{0C692837-77EC-415F-BF04-395E3ED06E9A}" EndProject -Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Graph", "Graph\Graph.sscproj", "{4C28FB90-630E-4B55-A937-11A011B79765}" -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}" EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}" @@ -29,6 +27,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3api", "Provers\Z3api\Z3ap EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AIFramework", "AIFramework\AIFramework.csproj", "{39B0658D-C955-41C5-9A43-48C97A1EF5FD}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj", "{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|.NET = Debug|.NET @@ -49,16 +49,6 @@ Global {0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Any CPU.ActiveCfg = Release|.NET {0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.ActiveCfg = Release|.NET {0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.Build.0 = Release|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.ActiveCfg = Debug|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.Build.0 = Debug|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Any CPU.ActiveCfg = Debug|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.Build.0 = Debug|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.ActiveCfg = Release|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.Build.0 = Release|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Release|Any CPU.ActiveCfg = Release|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.ActiveCfg = Release|.NET - {4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.Build.0 = Release|.NET {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU @@ -175,6 +165,16 @@ Global {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.Build.0 = Release|Any CPU {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|.NET.ActiveCfg = Debug|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Any CPU.Build.0 = Debug|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|.NET.ActiveCfg = Release|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.ActiveCfg = Release|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.Build.0 = Release|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Mixed Platforms.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index a31019db..5b08ba0d 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -87,6 +87,7 @@ + @@ -105,8 +106,8 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core - - {4C28FB90-630E-4B55-A937-11A011B79765} + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 54bc2cab..212e8208 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -92,6 +92,7 @@ + @@ -121,8 +122,8 @@ {0C692837-77EC-415F-BF04-395E3ED06E9A} Basetypes - - {4C28FB90-630E-4B55-A937-11A011B79765} + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph diff --git a/Source/Core/cce.cs b/Source/Core/cce.cs index 7aade95e..ef594484 100644 --- a/Source/Core/cce.cs +++ b/Source/Core/cce.cs @@ -3,7 +3,7 @@ using SA=System.Attribute; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Text; -using Microsoft.Boogie; +//using Microsoft.Boogie; /// /// A class containing static methods to extend the functionality of Code Contracts @@ -27,10 +27,10 @@ public static class cce { public static bool NonNullElements(IDictionary collection) { return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); } - [Pure] - public static bool NonNullElements(VariableSeq collection) { - return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} /// /// For possibly-null lists of non-null elements /// @@ -123,13 +123,17 @@ public static class cce { //public static bool IsValid(Microsoft.Dafny.Expression expression) { // return true; //} - public static List toList(PureCollections.Sequence s) { - List toRet = new List(); - foreach (T t in s.elems) - if(t!=null) - toRet.Add(t); - return toRet; - } + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} } public class PeerAttribute : SA { @@ -184,4 +188,6 @@ public class SpecPublicAttribute : SA { public class ElementsPeerAttribute : SA { } public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj index bcf367b7..e48b0fa7 100644 --- a/Source/Provers/Isabelle/Isabelle.csproj +++ b/Source/Provers/Isabelle/Isabelle.csproj @@ -69,6 +69,7 @@ + diff --git a/Source/Provers/Isabelle/cce.cs b/Source/Provers/Isabelle/cce.cs new file mode 100644 index 00000000..ef594484 --- /dev/null +++ b/Source/Provers/Isabelle/cce.cs @@ -0,0 +1,193 @@ +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { +} \ No newline at end of file diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index de0b7227..738e2cf7 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -79,6 +79,7 @@ + diff --git a/Source/Provers/SMTLib/cce.cs b/Source/Provers/SMTLib/cce.cs new file mode 100644 index 00000000..ef594484 --- /dev/null +++ b/Source/Provers/SMTLib/cce.cs @@ -0,0 +1,193 @@ +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { +} \ No newline at end of file diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj index 652f8eec..c15ef55a 100644 --- a/Source/Provers/Simplify/Simplify.csproj +++ b/Source/Provers/Simplify/Simplify.csproj @@ -73,6 +73,7 @@ + @@ -91,8 +92,8 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core - - {4C28FB90-630E-4B55-A937-11A011B79765} + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph diff --git a/Source/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs new file mode 100644 index 00000000..ef594484 --- /dev/null +++ b/Source/Provers/Simplify/cce.cs @@ -0,0 +1,193 @@ +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { +} \ No newline at end of file diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj index ba065013..ce7c280e 100644 --- a/Source/Provers/Z3/Z3.csproj +++ b/Source/Provers/Z3/Z3.csproj @@ -76,6 +76,7 @@ + diff --git a/Source/Provers/Z3/cce.cs b/Source/Provers/Z3/cce.cs new file mode 100644 index 00000000..ef594484 --- /dev/null +++ b/Source/Provers/Z3/cce.cs @@ -0,0 +1,193 @@ +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { +} \ No newline at end of file diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 05b12234..b2f61e8c 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -75,6 +75,7 @@ + diff --git a/Source/VCExpr/cce.cs b/Source/VCExpr/cce.cs index ff619b7c..ef594484 100644 --- a/Source/VCExpr/cce.cs +++ b/Source/VCExpr/cce.cs @@ -1,14 +1,19 @@ using System; +using SA=System.Attribute; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Text; -using Microsoft.Boogie; +//using Microsoft.Boogie; - /// - /// A class containing static methods to extend the functionality of Code Contracts - /// +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} [Pure] public static T NonNull(T t) { Contract.Assert(t != null); @@ -22,20 +27,39 @@ public static class cce { public static bool NonNullElements(IDictionary collection) { return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); } - [Pure] - public static bool NonNullElements(VariableSeq collection) { - return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - } //[Pure] - //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + } [Pure] public static bool NonNullElements(KeyValuePair kvp) { return kvp.Key != null && kvp.Value != null; } - + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} [Pure] public static void BeginExpose(object o) { } @@ -58,6 +82,10 @@ public static class cce { public static bool IsExposed(object o) { return true; } + [Pure] + public static bool IsNew(object o) { + return true; + } public static class Owner { [Pure] public static bool Same(object o, object p) { @@ -74,12 +102,19 @@ public static class cce { public static bool None(object o) { return true; } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } } [Pure] public static void LoopInvariant(bool p) { Contract.Assert(p); } - public class UnreachableException : Exception { public UnreachableException() { } @@ -88,43 +123,71 @@ public static class cce { //public static bool IsValid(Microsoft.Dafny.Expression expression) { // return true; //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} - internal static bool NonNullElements(IEnumerator iEnumerator) { - return iEnumerator != null; - } + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} } -public class PeerAttribute : System.Attribute { +public class PeerAttribute : SA { } -public class RepAttribute : System.Attribute { +public class RepAttribute : SA { } -public class CapturedAttribute : System.Attribute { +public class CapturedAttribute : SA { } -public class NotDelayedAttribute : System.Attribute { +public class NotDelayedAttribute : SA { } -public class NoDefaultContractAttribute : System.Attribute { +public class NoDefaultContractAttribute : SA { } -public class VerifyAttribute : System.Attribute { +public class VerifyAttribute : SA { public VerifyAttribute(bool b) { } } -public class StrictReadonlyAttribute : System.Attribute { - } -public class AdditiveAttribute : System.Attribute { +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { } -public class ReadsAttribute : System.Attribute { +public class ReadsAttribute : SA { public enum Reads { Nothing, + Everything, }; public ReadsAttribute(object o) { } } -public class GlobalAccessAttribute : System.Attribute { +public class GlobalAccessAttribute : SA { public GlobalAccessAttribute(bool b) { } } -public class EscapesAttribute : System.Attribute { +public class EscapesAttribute : SA { public EscapesAttribute(bool b, bool b_2) { } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index d6890363..d06cb13f 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -77,6 +77,7 @@ + @@ -101,8 +102,8 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core - - {4C28FB90-630E-4B55-A937-11A011B79765} + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph -- cgit v1.2.3