From 1780ee94238d722401f43791736b769cead01c43 Mon Sep 17 00:00:00 2001 From: akashlal Date: Sun, 5 May 2013 14:25:09 +0530 Subject: AbsHoudini: Each function can specify its own abstract domain. Also added typechecking --- Source/BoogieDriver/BoogieDriver.cs | 3 +- Source/Houdini/AbstractHoudini.cs | 135 ++++++++++++++++++++++++++++-------- Test/AbsHoudini/pred4.bpl | 21 ++++++ 3 files changed, 131 insertions(+), 28 deletions(-) create mode 100644 Test/AbsHoudini/pred4.bpl diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 41c175ef..b0af542b 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -671,7 +671,8 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ModelViewFile = "z3model"; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; - var domain = Houdini.AbstractDomainFactory.Initialize(CommandLineOptions.Clo.AbstractHoudini); + Houdini.AbstractDomainFactory.Initialize(); + var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini); // Run Abstract Houdini var abs = new Houdini.AbsHoudini(program, domain); diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 6d7d67e7..91b89262 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -15,8 +15,6 @@ namespace Microsoft.Boogie.Houdini { public class AbsHoudini { - // An element of the abstract domain - IAbstractDomain domainElement; Dictionary existentialFunctions; Program program; Dictionary name2Impl; @@ -45,10 +43,9 @@ namespace Microsoft.Boogie.Houdini { TimeSpan proverTime; int numProverQueries; - public AbsHoudini(Program program, IAbstractDomain elem) + public AbsHoudini(Program program, IAbstractDomain defaultElem) { this.program = program; - this.domainElement = elem; this.impl2VC = new Dictionary(); this.impl2FuncCalls = new Dictionary>>(); this.existentialFunctions = new Dictionary(); @@ -66,7 +63,19 @@ namespace Microsoft.Boogie.Houdini { existentialFunctions.Add(func.Name, func); this.function2Value = new Dictionary(); - existentialFunctions.Keys.Iter(f => function2Value.Add(f, domainElement.Bottom())); + foreach (var func in existentialFunctions.Values) + { + // Find if the function wishes to use a specific abstract domain + var domain = QKeyValue.FindStringAttribute(func.Attributes, "absdomain"); + if (domain == null) + { + function2Value[func.Name] = defaultElem.Bottom(); + } + else + { + function2Value[func.Name] = AbstractDomainFactory.GetInstance(domain); + } + } existentialFunctions.Keys.Iter(f => function2implAssumed.Add(f, new HashSet())); existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet())); @@ -77,6 +86,11 @@ namespace Microsoft.Boogie.Houdini { throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name)); if(func.Body != null) throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name)); + var args = new List(); + func.InParams.Iter(v => args.Add(v.TypedIdent.Type)); + string msg = ""; + if (!function2Value[func.Name].TypeCheck(args, out msg)) + throw new AbsHoudiniInternalError("TypeError: " + msg); }); //if (CommandLineOptions.Clo.ProverKillTime > 0) @@ -723,6 +737,21 @@ namespace Microsoft.Boogie.Houdini { return ret; } + public bool TypeCheck(List argTypes, out string msg) + { + msg = ""; + if (argTypes.Count != 1) + { + msg = "Illegal number of arguments"; + return false; + } + if (!argTypes[0].IsInt) + { + msg = "Illegal type, expecting int"; + return false; + } + return true; + } } public class PredicateAbsElem : IAbstractDomain @@ -868,6 +897,17 @@ namespace Microsoft.Boogie.Houdini { return ret; } + public bool TypeCheck(List argTypes, out string msg) + { + msg = ""; + if (argTypes.Any(t => !t.IsBool)) + { + msg = "Illegal type, expecting bool"; + return false; + } + return true; + } + private void AddDisjunct(Disjunct d) { if (conjuncts.Any(c => c.Implies(d))) @@ -935,6 +975,22 @@ namespace Microsoft.Boogie.Houdini { if (isTop) return Expr.True; return v; } + + public bool TypeCheck(List argTypes, out string msg) + { + msg = ""; + if (argTypes.Count != 1) + { + msg = "Illegal number of arguments, expecting 1"; + return false; + } + if (!argTypes[0].IsBool) + { + msg = "Illegal type, expecting bool"; + return false; + } + return true; + } } @@ -1041,6 +1097,22 @@ namespace Microsoft.Boogie.Houdini { return null; } + + public bool TypeCheck(List argTypes, out string msg) + { + msg = ""; + if (argTypes.Count != 1) + { + msg = "Illegal number of arguments, expecting 1"; + return false; + } + if (!argTypes[0].IsInt && ! argTypes[0].IsBool) + { + msg = "Illegal type, expecting int or bool"; + return false; + } + return true; + } } @@ -1111,18 +1183,33 @@ namespace Microsoft.Boogie.Houdini { var tt = typeof(T); underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T; } + + public bool TypeCheck(List argTypes, out string msg) + { + SetUnderlyingInstance(); + + msg = ""; + foreach(var t in argTypes) + { + if(!underlyingInstance.TypeCheck(new List(new Type[] { t }), out msg)) + return false; + } + return true; + } } public class AbstractDomainFactory { // Type name -> Instance private static Dictionary abstractDomainInstances = new Dictionary(); + private static Dictionary abstractDomainInstancesFriendly = new Dictionary(); - public static void Register(IAbstractDomain instance) + public static void Register(string friendlyName, IAbstractDomain instance) { var Name = instance.GetType().FullName; Debug.Assert(!abstractDomainInstances.ContainsKey(Name)); abstractDomainInstances.Add(Name, instance); + abstractDomainInstancesFriendly.Add(friendlyName, instance); } public static IAbstractDomain GetInstance(System.Type type) @@ -1132,7 +1219,19 @@ namespace Microsoft.Boogie.Houdini { return abstractDomainInstances[Name] as IAbstractDomain; } - public static IAbstractDomain Initialize(string domainName) + public static IAbstractDomain GetInstance(string friendlyName) + { + if (!abstractDomainInstancesFriendly.ContainsKey(friendlyName)) + { + Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini); + Console.WriteLine("Supported domains are:"); + abstractDomainInstancesFriendly.Keys.Iter(tup => Console.WriteLine(" {0}", tup)); + throw new AbsHoudiniInternalError("Domain not found"); + } + return abstractDomainInstancesFriendly[friendlyName] as IAbstractDomain; + } + + public static void Initialize() { // Declare abstract domains var domains = new List>(new System.Tuple[] { @@ -1145,26 +1244,7 @@ namespace Microsoft.Boogie.Houdini { System.Tuple.Create("IA[Intervals]", new IndependentAttribute() as IAbstractDomain) }); - domains.Iter(tup => AbstractDomainFactory.Register(tup.Item2)); - - // Find the abstract domain - IAbstractDomain domain = null; - foreach (var tup in domains) - { - if (tup.Item1 == domainName) - { - domain = tup.Item2; - break; - } - } - if (domain == null) - { - Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini); - Console.WriteLine("Supported domains are:"); - domains.Iter(tup => Console.WriteLine(" {0}", tup.Item1)); - throw new AbsHoudiniInternalError("Domain not found"); - } - return domain; + domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2)); } } @@ -1174,6 +1254,7 @@ namespace Microsoft.Boogie.Houdini { IAbstractDomain Bottom(); IAbstractDomain Join(List state); Expr Gamma(List vars); + bool TypeCheck(List argTypes, out string msg); } public class AbstractHoudini diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl new file mode 100644 index 00000000..d4741720 --- /dev/null +++ b/Test/AbsHoudini/pred4.bpl @@ -0,0 +1,21 @@ +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} {:absdomain "Intervals"} b3(x:int): bool; + +var g: int; + +procedure main() +modifies g; +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b3(g); +{ + assume g != 5; +} + -- cgit v1.2.3