diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 38 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 655 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd1.bpl | 18 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd10.bpl | 22 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd11.bpl | 13 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd12.bpl | 58 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd2.bpl | 27 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd3.bpl | 27 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd4.bpl | 27 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd5.bpl | 29 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd6.bpl | 44 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd7.bpl | 35 | ||||
| -rw-r--r-- | Test/AbsHoudini/houd8.bpl | 29 | ||||
| -rw-r--r-- | Test/AbsHoudini/runtest.bat | 9 | ||||
| -rw-r--r-- | Test/AbsHoudini/test1.bpl | 36 | ||||
| -rw-r--r-- | Test/AbsHoudini/test10.bpl | 47 | ||||
| -rw-r--r-- | Test/AbsHoudini/test2.bpl | 38 | ||||
| -rw-r--r-- | Test/AbsHoudini/test7.bpl | 15 | ||||
| -rw-r--r-- | Test/AbsHoudini/test8.bpl | 21 | ||||
| -rw-r--r-- | Test/AbsHoudini/test9.bpl | 73 |
20 files changed, 1255 insertions, 6 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9d1038f5..9b31c31e 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -639,15 +639,45 @@ namespace Microsoft.Boogie { {
if (CommandLineOptions.Clo.AbstractHoudini != null)
{
- CommandLineOptions.Clo.PrintErrorModel = 1;
+ //CommandLineOptions.Clo.PrintErrorModel = 1;
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
CommandLineOptions.Clo.ProverCCLimit = 1;
+ CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never;
+
+ // Declare abstract domains
+ var domains = new List<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {
+ System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>() as Houdini.IAbstractDomain)
+ });
+
+ domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2));
+
+ // Find the abstract domain
+ Houdini.IAbstractDomain domain = null;
+ foreach (var tup in domains)
+ {
+ if (tup.Item1 == CommandLineOptions.Clo.AbstractHoudini)
+ {
+ 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 Houdini.AbsHoudiniInternalError("Domain not found");
+ }
// Run Abstract Houdini
- Houdini.PredicateAbs.Initialize(program);
- var abs = new Houdini.AbstractHoudini(program);
- abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
+ var abs = new Houdini.AbsHoudini(program, domain);
+ abs.ComputeSummaries();
+
+ //Houdini.PredicateAbs.Initialize(program);
+ //var abs = new Houdini.AbstractHoudini(program);
+ //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
return PipelineOutcome.Done;
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 31141c85..e35e4a5c 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -13,6 +13,610 @@ using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie.Houdini {
+ public class AbsHoudini
+ {
+ // An element of the abstract domain
+ IAbstractDomain domainElement;
+ Dictionary<string, Function> existentialFunctions;
+ Program program;
+ Dictionary<string, Implementation> name2Impl;
+ Dictionary<string, VCExpr> impl2VC;
+ Dictionary<string, List<Tuple<string, Constant, NAryExpr>>> impl2FuncCalls;
+ // constant -> the naryexpr that it replaced
+ Dictionary<string, NAryExpr> constant2FuncCall;
+
+ // function -> its abstract value
+ Dictionary<string, IAbstractDomain> function2Value;
+
+ // impl -> functions assumed/asserted
+ Dictionary<string, HashSet<string>> impl2functionsAsserted, impl2functionsAssumed;
+
+ // funtions -> impls where assumed/asserted
+ Dictionary<string, HashSet<string>> function2implAssumed, function2implAsserted;
+
+ // impl -> handler, collector
+ Dictionary<string, Tuple<ProverInterface.ErrorHandler, ConditionGeneration.CounterexampleCollector>> impl2ErrorHandler;
+
+ // Essentials: VCGen, Prover
+ VCGen vcgen;
+ ProverInterface prover;
+
+ // Stats
+ TimeSpan proverTime;
+ int numProverQueries;
+
+ public AbsHoudini(Program program, IAbstractDomain elem)
+ {
+ this.program = program;
+ this.domainElement = elem;
+ this.impl2VC = new Dictionary<string, VCExpr>();
+ this.impl2FuncCalls = new Dictionary<string, List<Tuple<string, Constant, NAryExpr>>>();
+ this.existentialFunctions = new Dictionary<string, Function>();
+ this.name2Impl = new Dictionary<string, Implementation>();
+ this.impl2functionsAsserted = new Dictionary<string, HashSet<string>>();
+ this.impl2functionsAssumed = new Dictionary<string, HashSet<string>>();
+ this.function2implAsserted = new Dictionary<string, HashSet<string>>();
+ this.function2implAssumed = new Dictionary<string, HashSet<string>>();
+ this.impl2ErrorHandler = new Dictionary<string, Tuple<ProverInterface.ErrorHandler, ConditionGeneration.CounterexampleCollector>>();
+ this.constant2FuncCall = new Dictionary<string, NAryExpr>();
+
+ // Find the existential functions
+ foreach (var func in program.TopLevelDeclarations.OfType<Function>()
+ .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))
+ existentialFunctions.Add(func.Name, func);
+
+ this.function2Value = new Dictionary<string, IAbstractDomain>();
+ existentialFunctions.Keys.Iter(f => function2Value.Add(f, domainElement.Bottom()));
+ existentialFunctions.Keys.Iter(f => function2implAssumed.Add(f, new HashSet<string>()));
+ existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet<string>()));
+
+ // type check
+ existentialFunctions.Values.Iter(func =>
+ {
+ if (func.OutParams.Length != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)
+ 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));
+ });
+
+ if (CommandLineOptions.Clo.ProverKillTime > 0)
+ CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
+
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
+
+ this.proverTime = TimeSpan.Zero;
+ this.numProverQueries = 0;
+
+ program.TopLevelDeclarations.OfType<Implementation>()
+ .Iter(impl => name2Impl.Add(impl.Name, impl));
+
+ // Let's do VC Gen (and also build dependencies)
+ name2Impl.Values.Iter(GenVC);
+ }
+
+ public void ComputeSummaries()
+ {
+ var worklist = new Queue<string>();
+ name2Impl.Keys.Iter(k => worklist.Enqueue(k));
+
+ while (worklist.Any())
+ {
+ var impl = worklist.Dequeue();
+ var gen = prover.VCExprGen;
+ Expr env = Expr.True;
+
+ foreach (var tup in impl2FuncCalls[impl])
+ {
+ var controlVar = tup.Item2;
+ var exprVars = tup.Item3;
+ var varList = new List<Expr>();
+ exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v));
+
+ env = Expr.And(env,
+ Expr.Eq(Expr.Ident(controlVar), function2Value[tup.Item1].Gamma(varList)));
+ }
+
+ env.Typecheck(new TypecheckingContext((IErrorSink)null));
+ var envVC = prover.Context.BoogieExprTranslator.Translate(env);
+ //Console.WriteLine("env: {0}", envVC);
+
+ var vc = gen.Implies(envVC, impl2VC[impl]);
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.Write("Verifying {0}: ", impl);
+
+ var handler = impl2ErrorHandler[impl].Item1;
+ var collector = impl2ErrorHandler[impl].Item2;
+ collector.examples.Clear();
+
+ var start = DateTime.Now;
+
+ prover.Push();
+ prover.Assert(gen.Not(vc), true);
+ prover.FlushAxiomsToTheoremProver();
+ prover.Check();
+ ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
+
+ //prover.BeginCheck(impl, vc, handler);
+ //ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
+
+ var inc = (DateTime.Now - start);
+ proverTime += inc;
+ numProverQueries++;
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());
+
+ if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
+ throw new AbsHoudiniInternalError("Timeout/Spaceout while verifying " + impl);
+
+
+ if (collector.examples.Count == 0)
+ {
+ if (CommandLineOptions.Clo.Trace) Console.WriteLine("UNSAT");
+ prover.Pop();
+ continue;
+ }
+
+ if (CommandLineOptions.Clo.Trace) Console.WriteLine("SAT");
+ Debug.Assert(collector.examples.Count == 1);
+ var error = collector.examples[0];
+
+ // Find the failing assert -- need to do a join there
+ var cex = ExtractState(impl, error);
+ var funcsChanged = new HashSet<string>();
+ foreach (var tup in cex)
+ {
+ function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2);
+ funcsChanged.Add(tup.Item1);
+ }
+
+ // propagate dependent guys back into the worklist, including self
+ var deps = new HashSet<string>();
+ deps.Add(impl);
+ funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f]));
+
+ deps.RemoveWhere(s => worklist.Contains(s));
+ deps.Iter(s => worklist.Enqueue(s));
+
+ prover.Pop();
+ }
+
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ // Print the answer
+ var tt = new TokenTextWriter(Console.Out);
+ foreach (var function in existentialFunctions.Values)
+ {
+ var invars = new List<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));
+ function.Body = function2Value[function.Name].Gamma(invars);
+ function.Emit(tt, 0);
+ }
+ tt.Close();
+ }
+ }
+
+ private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Counterexample error)
+ {
+ var lastBlock = error.Trace.Last() as Block;
+ AssertCmd failingAssert = null;
+
+ CallCounterexample callCounterexample = error as CallCounterexample;
+ if (callCounterexample != null)
+ {
+ Procedure failingProcedure = callCounterexample.FailingCall.Proc;
+ Requires failingRequires = callCounterexample.FailingRequires;
+ failingAssert = lastBlock.Cmds.OfType<AssertRequiresCmd>().FirstOrDefault(ac => ac.Requires == failingRequires);
+ }
+ ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
+ if (returnCounterexample != null)
+ {
+ Ensures failingEnsures = returnCounterexample.FailingEnsures;
+ failingAssert = lastBlock.Cmds.OfType<AssertEnsuresCmd>().FirstOrDefault(ac => ac.Ensures == failingEnsures);
+ }
+ AssertCounterexample assertCounterexample = error as AssertCounterexample;
+ if (assertCounterexample != null)
+ {
+ failingAssert = lastBlock.Cmds.OfType<AssertCmd>().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert);
+ }
+
+ Debug.Assert(failingAssert != null);
+ return ExtractState(impl, failingAssert.Expr, error.Model);
+ }
+
+ private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Expr expr, Model model)
+ {
+ var collect = new VariableCollector();
+ collect.VisitExpr(expr);
+
+ var ret = new List<Tuple<string, List<Model.Element>>>();
+
+ foreach (var constant in collect.usedVars.OfType<Constant>().Where(c => constant2FuncCall.ContainsKey(c.Name)))
+ {
+ var func = constant2FuncCall[constant.Name];
+ var funcName = (func.Fun as FunctionCall).FunctionName;
+ var vals = new List<Model.Element>();
+ prover.Context.BoogieExprTranslator.Translate(func.Args).Iter(ve => vals.Add(getValue(ve, model)));
+
+ ret.Add(Tuple.Create(funcName, vals));
+ }
+
+ return ret;
+ }
+
+ private Model.Element getValue(VCExpr arg, Model model)
+ {
+
+ if (arg is VCExprLiteral)
+ {
+ //return model.GetElement(arg.ToString());
+ return model.MkElement(arg.ToString());
+ }
+ else if (arg is VCExprVar)
+ {
+ var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
+ if (el != null)
+ {
+ Debug.Assert(el.Arity == 0 && el.AppCount == 1);
+ return el.Apps.First().Result;
+ }
+ else
+ {
+ // Variable not defined; assign arbitrary value
+ if (arg.Type.IsBool)
+ return model.MkElement("false");
+ else if (arg.Type.IsInt)
+ return model.MkIntElement(0);
+ else
+ return null;
+ }
+ }
+ else
+ {
+ var val = prover.Evaluate(arg);
+ if (val is int || val is bool)
+ {
+ return model.MkElement(val.ToString());
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return null;
+ }
+ }
+
+ private void GenVC(Implementation impl)
+ {
+ ModelViewInfo mvInfo;
+ System.Collections.Hashtable label2absy;
+ var collector = new ConditionGeneration.CounterexampleCollector();
+ collector.OnProgress("HdnVCGen", 0, 0, 0.0);
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Generating VC of {0}", impl.Name);
+ }
+
+ vcgen.ConvertCFG2DAG(impl);
+ var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
+
+ // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants
+ var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);
+ var fv = new ReplaceFunctionCalls(existentialFunctionNames);
+ fv.VisitBlockList(impl.Blocks);
+
+ impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);
+ impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);
+
+ fv.functionsAssumed.Iter(f => function2implAssumed[f].Add(impl.Name));
+ fv.functionsAsserted.Iter(f => function2implAsserted[f].Add(impl.Name));
+
+ impl2FuncCalls.Add(impl.Name, fv.functionsUsed);
+ fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3));
+
+ var gen = prover.VCExprGen;
+ var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context);
+
+ ProverInterface.ErrorHandler handler = null;
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
+ handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
+ else
+ handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
+
+ impl2ErrorHandler.Add(impl.Name, Tuple.Create(handler, collector));
+
+ //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
+
+ // Create a macro so that the VC can sit with the theorem prover
+ Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
+ prover.DefineMacro(macro, vcexpr);
+
+ // Store VC
+ impl2VC.Add(impl.Name, gen.Function(macro));
+ }
+
+
+ }
+
+ class ReplaceFunctionCalls : StandardVisitor
+ {
+ public List<Tuple<string, Constant, NAryExpr>> functionsUsed;
+ public List<Constant> boolConstants;
+
+ public HashSet<string> functionsAssumed;
+ public HashSet<string> functionsAsserted;
+ HashSet<string> functionsToReplace;
+
+ private bool inAssume;
+ private bool inAssert;
+ private static int IdCounter = 0;
+
+ public ReplaceFunctionCalls(HashSet<string> functionsToReplace)
+ {
+ this.functionsUsed = new List<Tuple<string, Constant, NAryExpr>>();
+ this.functionsToReplace = functionsToReplace;
+ this.functionsAsserted = new HashSet<string>();
+ this.functionsAssumed = new HashSet<string>();
+ this.boolConstants = new List<Constant>();
+
+ inAssume = false;
+ inAssert = false;
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ inAssert = true;
+ var ret = base.VisitAssertCmd(node);
+ inAssert = false;
+ return ret;
+ }
+
+ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
+ {
+ return this.VisitAssertCmd(node);
+ }
+
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
+ {
+ return this.VisitAssertCmd(node);
+ }
+
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ inAssume = true;
+ var ret = base.VisitAssumeCmd(node);
+ inAssume = false;
+ return ret;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is FunctionCall && functionsToReplace.Contains((node.Fun as FunctionCall).FunctionName))
+ {
+ found((node.Fun as FunctionCall).FunctionName);
+ // create boolean constant to replace this guy
+ var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "AbsHoudiniConstant" + IdCounter, Microsoft.Boogie.Type.Bool), false);
+ IdCounter++;
+
+ functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).FunctionName, constant, node));
+ boolConstants.Add(constant);
+ return Expr.Ident(constant);
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ private void found(string func)
+ {
+ if (inAssume) functionsAssumed.Add(func);
+ if (inAssert) functionsAsserted.Add(func);
+ }
+
+ }
+
+ public class ConstantProp : IAbstractDomain
+ {
+ object val;
+ bool isBottom;
+ bool isTop;
+
+ private ConstantProp(object val, bool isTop, bool isBottom)
+ {
+ this.val = val;
+ this.isBottom = isBottom;
+ this.isTop = isTop;
+ Debug.Assert(!(isTop && isBottom));
+ Debug.Assert(val == null || (val is int) || (val is bool));
+ }
+
+ public static ConstantProp GetExtObj(object val)
+ {
+ Debug.Assert(val != null);
+ return new ConstantProp(val, false, false);
+ }
+
+ public static ConstantProp GetTop()
+ {
+ return new ConstantProp(null, true, false);
+ }
+
+ public static ConstantProp GetBottom()
+ {
+ return new ConstantProp(null, false, true);
+ }
+
+ private ConstantProp Join(ConstantProp that)
+ {
+ if (isBottom) return that;
+ if (isTop) return this;
+ if (that.isBottom) return this;
+ if (that.isTop) return that;
+
+ if ((val is int) && !(that.val is int))
+ throw new AbsHoudiniInternalError("Type mismatch in ExtObj");
+
+ if ((val is bool) && !(that.val is bool))
+ throw new AbsHoudiniInternalError("Type mismatch in ExtObj");
+
+ if (val is int)
+ {
+ var v1 = (int)val;
+ var v2 = (int)that.val;
+ if (v1 != v2) return GetTop();
+ return this;
+ }
+ else if (val is bool)
+ {
+ var v1 = (bool)val;
+ var v2 = (bool)that.val;
+ if (v1 != v2) return GetTop();
+ return this;
+ }
+ throw new AbsHoudiniInternalError("Illegal val type in ExtObj");
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return GetBottom();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0];
+ ConstantProp that = null;
+
+ if (state is Model.Integer)
+ {
+ that = GetExtObj((state as Model.Integer).AsInt());
+ }
+ else if (state is Model.Boolean)
+ {
+ that = GetExtObj((state as Model.Boolean).Value);
+ }
+ else
+ {
+ throw new AbsHoudiniInternalError("Illegal type " + state.GetType().ToString());
+ }
+
+ return Join(that);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 1);
+ var v = vars[0];
+ if (isBottom) return Expr.False;
+ if (isTop) return Expr.True;
+ if (val is int)
+ return Expr.Eq(v, Expr.Literal((int)val));
+ if (val is bool && (bool)val)
+ return v;
+ if (val is bool && !(bool)val)
+ return Expr.Not(v);
+
+ return null;
+ }
+ }
+
+
+ public class IndependentAttribute<T> : IAbstractDomain where T : class, IAbstractDomain
+ {
+ bool isBottom;
+ int numVars;
+ List<T> varVal;
+ T underlyingInstance;
+
+ public IndependentAttribute()
+ {
+ isBottom = true;
+ numVars = 0;
+ varVal = new List<T>();
+ underlyingInstance = null;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new IndependentAttribute<T>();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> state)
+ {
+ SetUnderlyingInstance();
+
+ if (!isBottom && numVars != state.Count)
+ {
+ throw new AbsHoudiniInternalError(
+ string.Format("Got illegal number of arguments ({0}), expected {1}", state.Count, numVars));
+ }
+
+ var ret = new IndependentAttribute<T>();
+ ret.isBottom = false;
+ ret.numVars = state.Count;
+ for(int i = 0; i < state.Count; i++)
+ {
+ var sl = new List<Model.Element>();
+ sl.Add(state[i]);
+ T prev = isBottom ? underlyingInstance.Bottom() as T : varVal[i];
+ ret.varVal.Add(prev.Join(sl) as T);
+ }
+
+ return ret;
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isBottom) return Expr.False;
+ if (numVars != vars.Count)
+ throw new AbsHoudiniInternalError(
+ string.Format("Got illegal number of arguments ({0}), expected {1}", vars.Count, numVars));
+
+ Expr ret = Expr.True;
+ for (int i = 0; i < numVars; i++)
+ {
+ var sl = new List<Expr>(); sl.Add(vars[i]);
+ ret = Expr.And(ret, varVal[i].Gamma(sl));
+ }
+
+ return ret;
+ }
+
+ private void SetUnderlyingInstance()
+ {
+ if (underlyingInstance != null) return;
+ var tt = typeof(T);
+ underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T;
+ }
+ }
+
+ public class AbstractDomainFactory
+ {
+ // Type name -> Instance
+ private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();
+
+ public static void Register(IAbstractDomain instance)
+ {
+ var Name = instance.GetType().FullName;
+ Debug.Assert(!abstractDomainInstances.ContainsKey(Name));
+ abstractDomainInstances.Add(Name, instance);
+ }
+
+ public static IAbstractDomain GetInstance(System.Type type)
+ {
+ var Name = type.FullName;
+ Debug.Assert(abstractDomainInstances.ContainsKey(Name));
+ return abstractDomainInstances[Name] as IAbstractDomain;
+ }
+ }
+
+ public interface IAbstractDomain
+ {
+ IAbstractDomain Bottom();
+ IAbstractDomain Join(List<Model.Element> state);
+ Expr Gamma(List<Expr> vars);
+ }
+
public class AbstractHoudini
{
// Input Program
@@ -2379,6 +2983,54 @@ namespace Microsoft.Boogie.Houdini { }
+ class FindExistentialFunctions : MutatingVCExprVisitor<bool>
+ {
+ public List<Tuple<string, VCExprVar, VCExprNAry>> funcCalls;
+ private HashSet<string> existentialFunctions;
+ private static int CounterId = 0;
+
+ public FindExistentialFunctions(VCExpressionGenerator gen, HashSet<string> existentialFunctions)
+ : base(gen)
+ {
+ funcCalls = new List<Tuple<string, VCExprVar, VCExprNAry>>();
+ this.existentialFunctions = existentialFunctions;
+ }
+
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg)
+ {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprNAry retnary = ret as VCExprNAry;
+ if (retnary == null) return ret;
+ var op = retnary.Op as VCExprBoogieFunctionOp;
+ if (op == null) return ret;
+
+ string calleeName = op.Func.Name;
+
+ if (!existentialFunctions.Contains(calleeName))
+ return ret;
+
+ var controlConst = Gen.Variable("AbsHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool);
+ CounterId++;
+
+ funcCalls.Add(Tuple.Create(calleeName, controlConst, retnary));
+
+ return controlConst;
+ }
+
+ }
+
class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
{
public Model model;
@@ -2396,6 +3048,9 @@ namespace Microsoft.Boogie.Houdini { }
}
+ public class AbsHoudiniAssemblyLocator
+ {
+ }
public class AbsHoudiniInternalError : System.ApplicationException
{
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl new file mode 100644 index 00000000..099c6f09 --- /dev/null +++ b/Test/AbsHoudini/houd1.bpl @@ -0,0 +1,18 @@ +function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+// comment
+ensures b1(myVar>0);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected output: Correct
+// expected end assigment: b1(x) = x
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl new file mode 100644 index 00000000..bb0c65e7 --- /dev/null +++ b/Test/AbsHoudini/houd10.bpl @@ -0,0 +1,22 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var fooVar: int;
+var xVar: int;
+
+procedure foo()
+modifies fooVar;
+modifies xVar;
+ensures b1() || fooVar==0;
+ensures b3() || xVar<0;
+{
+ fooVar:=5;
+ call bar();
+}
+
+procedure bar();
+modifies xVar;
+requires Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl new file mode 100644 index 00000000..78087744 --- /dev/null +++ b/Test/AbsHoudini/houd11.bpl @@ -0,0 +1,13 @@ +function {:existential true} Assert() : bool;
+
+var fooVar: int;
+
+procedure foo()
+modifies fooVar;
+{
+ fooVar:=5;
+ assert Assert() || (fooVar==4);
+ assert Assert() || (fooVar==3);
+}
+
+// expected assigment: Assert -> true
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl new file mode 100644 index 00000000..b3a1a6db --- /dev/null +++ b/Test/AbsHoudini/houd12.bpl @@ -0,0 +1,58 @@ +// Example to test candidate annotations on loops
+
+function {:existential true} Assert(): bool;
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+
+var x: int;
+var y: int;
+
+
+procedure foo()
+modifies x;
+modifies y;
+ensures (b4() || x == 0);
+ensures (b5() || y == 10);
+ensures (b6() || x == 10);
+ensures (b7() || y == 11);
+
+{
+ x := 10;
+ y := 0;
+
+ goto Head;
+
+Head:
+
+ //loop invariants
+ assert (b1() || x < 0);
+ assert (b2() || x >= 0);
+ assert (b3() || x + y == 10);
+ goto Body, Exit;
+
+Body:
+ assume x > 0;
+ x := x - 1;
+ y := y + 1;
+
+
+ goto Head;
+
+Exit:
+ assume !(x > 0);
+ return;
+}
+
+// expected assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl new file mode 100644 index 00000000..fd2611e2 --- /dev/null +++ b/Test/AbsHoudini/houd2.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert(x:bool) : bool;
+function {:existential true} b1 (x:bool):bool;
+function {:existential true} b2 (x:bool):bool;
+
+
+var myVar: int;
+
+procedure bar(i:int)
+modifies myVar;
+ensures Assert(myVar>0);
+{
+ call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl new file mode 100644 index 00000000..81f11018 --- /dev/null +++ b/Test/AbsHoudini/houd3.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert(x: bool) : bool;
+function {:existential true} b1(x: bool) : bool;
+function {:existential true} b2(x: bool) : bool;
+
+
+var myVar: int;
+
+procedure bar(i:int)
+modifies myVar;
+ensures b2(myVar>0);
+{
+ call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl new file mode 100644 index 00000000..01ee6707 --- /dev/null +++ b/Test/AbsHoudini/houd4.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert() : bool;
+function {:existential true} b1():bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b2(i > 0);
+ensures b3(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b4(j > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]);
+{
+ call foo(j);
+ result := array[j];
+}
+
+// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl new file mode 100644 index 00000000..afbaa81c --- /dev/null +++ b/Test/AbsHoudini/houd5.bpl @@ -0,0 +1,29 @@ +function {:existential true} b1(x:bool):bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+function {:existential true} b5():bool;
+function {:existential true} Assert():bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b1(i == 0);
+requires b2(i > 0);
+requires b3(i < 0);
+ensures b4(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b5() || (j > 0);
+modifies array;
+{
+ call foo(j);
+ result := array[j];
+}
+
+// expected assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl new file mode 100644 index 00000000..e4927901 --- /dev/null +++ b/Test/AbsHoudini/houd6.bpl @@ -0,0 +1,44 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+function {:existential true} b8():bool;
+function {:existential true} Assert(): bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b6() || i < 0;
+requires b5() || i == 0;
+requires b2() || i > 0;
+ensures b3() || array[i] > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b8() || j < 0;
+requires b7() || j == 0;
+requires b4() || j > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]);
+ensures b1() || array[j] == old(array)[j];
+{
+ call foo(j);
+ result := array[j];
+}
+
+var p:int;
+
+procedure main() returns (result: int)
+modifies array;
+{
+ call result:= bar(p);
+}
+
+// expected assigment: Assert -> false, bi->true forall i
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl new file mode 100644 index 00000000..ef3293db --- /dev/null +++ b/Test/AbsHoudini/houd7.bpl @@ -0,0 +1,35 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var myVar: int;
+
+procedure foo(i:int)
+requires b1() || i>0;
+requires b2() || i==0;
+requires b3() || i<0;
+modifies myVar;
+ensures Assert() || myVar>0;
+{
+ myVar:=5;
+}
+
+procedure bar(i:int)
+modifies myVar;
+{
+ call foo(5);
+}
+// expected outcome: Correct
+// expected Assigment: Assert = false, b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl new file mode 100644 index 00000000..8be7f3db --- /dev/null +++ b/Test/AbsHoudini/houd8.bpl @@ -0,0 +1,29 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+
+var myVar: int;
+
+procedure foo(i:int)
+modifies myVar;
+ensures b1() || myVar>0;
+ensures b2() || myVar==0;
+ensures b3() || myVar<0;
+{
+ myVar:=5;
+}
+
+// expected assigment: b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index 34308e4e..b9816bb9 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -3,9 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (f1.bpl) do (
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f
)
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f
+)
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl new file mode 100644 index 00000000..e6ce06c9 --- /dev/null +++ b/Test/AbsHoudini/test1.bpl @@ -0,0 +1,36 @@ +var g: bool;
+
+procedure foo()
+modifies g;
+ensures b0 ==> (!old(g) ==> old(g) == g);
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1 ==> old(g) == g;
+{
+ g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2 ==> old(g) == g;
+{
+ g := false;
+}
+
+procedure main()
+modifies g;
+{
+ g := false;
+ call foo();
+ assert !g;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl new file mode 100644 index 00000000..abb993f7 --- /dev/null +++ b/Test/AbsHoudini/test10.bpl @@ -0,0 +1,47 @@ +var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+ sdv_21 := sdv_7;
+ sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := sdv_21;
+ havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7));
+{
+ call push(2);
+ call pop();
+ call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate} b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+ call push(1);
+ call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := 0;
+ call foo();
+}
+
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl new file mode 100644 index 00000000..febb28e6 --- /dev/null +++ b/Test/AbsHoudini/test2.bpl @@ -0,0 +1,38 @@ +var g: int;
+var h: int;
+
+procedure foo()
+modifies g, h;
+ensures b0 ==> old(g) == g;
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1 ==> old(g) == g;
+{
+ h := g;
+ g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2 ==> old(g) == g;
+{
+ g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+ g := 0;
+ call foo();
+ assert g == 0;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl new file mode 100644 index 00000000..b5c6a4c6 --- /dev/null +++ b/Test/AbsHoudini/test7.bpl @@ -0,0 +1,15 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure foo()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl new file mode 100644 index 00000000..12eab481 --- /dev/null +++ b/Test/AbsHoudini/test8.bpl @@ -0,0 +1,21 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure {:inline 1} foo()
+modifies g;
+{
+ call bar();
+}
+
+procedure bar()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl new file mode 100644 index 00000000..24eb66e8 --- /dev/null +++ b/Test/AbsHoudini/test9.bpl @@ -0,0 +1,73 @@ +var v1: int;
+var v2: int;
+var v3: int;
+const{:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+const{:existential true} b5: bool;
+const{:existential true} b6: bool;
+const{:existential true} b7: bool;
+const{:existential true} b8: bool;
+const{:existential true} b9: bool;
+const{:existential true} b10: bool;
+const{:existential true} b11: bool;
+const{:existential true} b12: bool;
+const{:existential true} b13: bool;
+const{:existential true} b14: bool;
+const{:existential true} b15: bool;
+const{:existential true} b16: bool;
+
+procedure push()
+requires {:candidate} b1 ==> v1 == 0;
+requires {:candidate} b2 ==> v1 == 1;
+ensures {:candidate} b3 ==> v1 == 0;
+ensures {:candidate} b4 ==> v1 == 1;
+modifies v1,v2;
+{
+ v2 := v1;
+ v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5 ==> v1 == 0;
+requires {:candidate} b6 ==> v1 == 1;
+ensures {:candidate} b7 ==> v1 == 0;
+ensures {:candidate} b8 ==> v1 == 1;
+{
+ v1 := v2;
+ havoc v2;
+}
+
+procedure foo()
+modifies v1,v2;
+requires {:candidate} b9 ==> v1 == 0;
+requires {:candidate} b10 ==> v1 == 1;
+ensures {:candidate} b11 ==> v1 == 0;
+ensures {:candidate} b12 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13 ==> v1 == 0;
+requires {:candidate} b14 ==> v1 == 1;
+ensures {:candidate} b15 ==> v1 == 0;
+ensures {:candidate} b16 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure main()
+modifies v1,v2;
+{
+ v1 := 1;
+ call foo();
+ havoc v1;
+ call bar();
+}
+
|