From fefb3292b1b4838446910cfea01c0d307dbac97e Mon Sep 17 00:00:00 2001 From: akashlal Date: Sat, 2 Nov 2013 19:28:33 +0530 Subject: AbsHoudini: Support timeout, MakeTop, InlineFunctions --- Source/Houdini/AbstractHoudini.cs | 169 +++++++++++++++++++++++++++++++++++++- 1 file changed, 167 insertions(+), 2 deletions(-) (limited to 'Source/Houdini') diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 7acd2f6f..ac5ba95f 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -99,7 +99,7 @@ namespace Microsoft.Boogie.Houdini { Inline(); this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List()); - this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1); + this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime); this.proverTime = TimeSpan.Zero; this.numProverQueries = 0; @@ -219,7 +219,17 @@ namespace Microsoft.Boogie.Houdini { Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString()); if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory) - return new VCGenOutcome(proverOutcome, new List()); + { + // pick some function; make it true and keep going + bool changed = false; + foreach (var f in impl2functionsAsserted[impl]) + { + function2Value[f] = function2Value[f].MakeTop(out changed); + if (changed) break; + } + if(!changed) + return new VCGenOutcome(proverOutcome, new List()); + } if (CommandLineOptions.Clo.Trace) Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT"); @@ -577,6 +587,9 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl); var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo); + // Inline functions + (new InlineFunctionCalls()).VisitBlockList(impl.Blocks); + ExtractQuantifiedExprs(impl); StripOutermostForall(impl); @@ -787,6 +800,48 @@ namespace Microsoft.Boogie.Houdini { } + class InlineFunctionCalls : StandardVisitor + { + public Stack inlinedFunctionsStack; + + public InlineFunctionCalls() + { + inlinedFunctionsStack = new Stack(); + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + var fc = node.Fun as FunctionCall; + if (fc != null && fc.Func.Body != null && QKeyValue.FindBoolAttribute(fc.Func.Attributes, "inline")) + { + if (inlinedFunctionsStack.Contains(fc.Func.Name)) + { + // recursion detected + throw new AbsHoudiniInternalError("Recursion detected in function declarations"); + } + + // create a substitution + var subst = new Dictionary(); + for (int i = 0; i < node.Args.Count; i++) + { + subst.Add(fc.Func.InParams[i], node.Args[i]); + } + + var e = + Substituter.Apply(new Substitution(v => subst.ContainsKey(v) ? subst[v] : Expr.Ident(v)), fc.Func.Body); + + inlinedFunctionsStack.Push(fc.Func.Name); + + e = base.VisitExpr(e); + + inlinedFunctionsStack.Pop(); + + return e; + } + return base.VisitNAryExpr(node); + } + } + class ReplaceFunctionCalls : StandardVisitor { public List> functionsUsed; @@ -1150,6 +1205,17 @@ namespace Microsoft.Boogie.Houdini { return new Intervals(); } + public IAbstractDomain MakeTop(out bool changed) + { + if (lower == Int32.MinValue && upper == Int32.MaxValue) + { + changed = false; + return this; + } + changed = true; + return new Intervals(Int32.MinValue, Int32.MaxValue, 0); + } + public IAbstractDomain Join(List states) { Debug.Assert(states.Count == 1); @@ -1315,6 +1381,19 @@ namespace Microsoft.Boogie.Houdini { return new PredicateAbsElem(); } + public IAbstractDomain MakeTop(out bool changed) + { + if (conjuncts.Count == 0) + { + changed = false; + return this; + } + changed = true; + var ret = new PredicateAbsElem(); + ret.isFalse = false; + return ret; + } + public IAbstractDomain Join(List state) { if (state.Any(me => !(me is Model.Boolean))) @@ -1413,6 +1492,14 @@ namespace Microsoft.Boogie.Houdini { return GetBottom(); } + public IAbstractDomain MakeTop(out bool changed) + { + changed = false; + if (isTop) return this; + changed = true; + return GetTop(); + } + public IAbstractDomain Join(List states) { Debug.Assert(states.Count == 1); @@ -1481,6 +1568,17 @@ namespace Microsoft.Boogie.Houdini { return new PowDomain(Val.FALSE) as IAbstractDomain; } + public IAbstractDomain MakeTop(out bool changed) + { + if (isTop) + { + changed = false; + return this; + } + changed = true; + return new PowDomain(Val.TRUE); + } + IAbstractDomain IAbstractDomain.Bottom() { return GetBottom(); @@ -1563,6 +1661,17 @@ namespace Microsoft.Boogie.Houdini { return GetBottom(); } + public IAbstractDomain MakeTop(out bool changed) + { + if (equalities.Count == 0) + { + changed = false; + return this; + } + changed = true; + return new EqualitiesDomain(false, new List>()); + } + IAbstractDomain IAbstractDomain.Join(List state) { // find the guys that are equal @@ -1676,6 +1785,16 @@ namespace Microsoft.Boogie.Houdini { return GetBottom(); } + public IAbstractDomain MakeTop(out bool changed) + { + if(val == Val.TRUE) { + changed = false; + return this; + } + changed = true; + return new ImplicationDomain(Val.TRUE); + } + public IAbstractDomain Join(List states) { Debug.Assert(states.Count == 2); @@ -1760,6 +1879,16 @@ namespace Microsoft.Boogie.Houdini { return new ConstantProp(null, false, true); } + public IAbstractDomain MakeTop(out bool changed) { + if (isTop) + { + changed = false; + return this; + } + changed = true; + return GetTop(); + } + private ConstantProp Join(ConstantProp that) { if (isBottom) return that; @@ -1871,6 +2000,41 @@ namespace Microsoft.Boogie.Houdini { return new IndependentAttribute(); } + public IAbstractDomain MakeTop(out bool changed) + { + var mt = new Func(() => + { + var ret = new IndependentAttribute(); + ret.isBottom = true; + ret.numVars = numVars; + ret.underlyingInstance = underlyingInstance; + ret.varVal = new List(); + bool tmp; + for (int i = 0; i < varVal.Count; i++) + ret.varVal.Add(varVal[i].MakeTop(out tmp) as T); + return ret; + }); + + if (!isBottom) + { + foreach (var t in varVal) + { + var top = t.MakeTop(out changed); + if (changed) + { + return mt(); + } + } + } + else + { + changed = true; + return mt(); + } + + changed = false; + return this; + } public IAbstractDomain Join(List state) { SetUnderlyingInstance(); @@ -2002,6 +2166,7 @@ namespace Microsoft.Boogie.Houdini { public interface IAbstractDomain { IAbstractDomain Bottom(); + IAbstractDomain MakeTop(out bool changed); IAbstractDomain Join(List state); Expr Gamma(List vars); bool TypeCheck(List argTypes, out string msg); -- cgit v1.2.3