diff options
| author |  allydonaldson <unknown> | 2013-04-30 15:45:47 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-04-30 15:45:47 +0100 |
| commit | 77aeb920de2c3cd22a1296700305539f28f6761c (patch) | |
| tree | cf140a2c6ced506e28d10f3e2d8937815354e652 /Source/Houdini | |
| parent | 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 (diff) | |
| parent | 8d06e693c56205a1d2ba4c25d850c7c6676e19a8 (diff) | |
Merge
Diffstat (limited to 'Source/Houdini')
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 1182 |
1 files changed, 1175 insertions, 7 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 98667bec..a730ec8f 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -13,6 +13,1121 @@ 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, AbsHoudiniCounterexampleCollector>> 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, AbsHoudiniCounterexampleCollector>>();
+ 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));
+
+ Inline();
+
+ 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>()
+ .Where(impl => !impl.SkipVerification)
+ .Iter(impl => name2Impl.Add(impl.Name, impl));
+
+ // Let's do VC Gen (and also build dependencies)
+ name2Impl.Values.Iter(GenVC);
+ }
+
+ public void ComputeSummaries()
+ {
+ // Compute SCCs and determine a priority order for impls
+ var Succ = new Dictionary<string, HashSet<string>>();
+ var Pred = new Dictionary<string, HashSet<string>>();
+ name2Impl.Keys.Iter(s => Succ[s] = new HashSet<string>());
+ name2Impl.Keys.Iter(s => Pred[s] = new HashSet<string>());
+
+ foreach(var impl in name2Impl.Keys) {
+ Succ[impl] = new HashSet<string>();
+ impl2functionsAsserted[impl].Iter(f =>
+ function2implAssumed[f].Iter(succ =>
+ {
+ Succ[impl].Add(succ);
+ Pred[succ].Add(impl);
+ }));
+ }
+
+ var sccs = new StronglyConnectedComponents<string>(name2Impl.Keys,
+ new Adjacency<string>(n => Pred[n]),
+ new Adjacency<string>(n => Succ[n]));
+ sccs.Compute();
+
+ // impl -> priority
+ var impl2Priority = new Dictionary<string, int>();
+ int p = 0;
+ foreach (var scc in sccs)
+ {
+ foreach (var impl in scc)
+ {
+ impl2Priority.Add(impl, p);
+ p++;
+ }
+ }
+
+ var worklist = new SortedSet<Tuple<int, string>>();
+ name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k)));
+
+ while (worklist.Any())
+ {
+ var impl = worklist.First().Item2;
+ worklist.Remove(worklist.First());
+
+ 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);
+
+ var vc = gen.Implies(envVC, impl2VC[impl]);
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Verifying {0}: ", impl);
+ //Console.WriteLine("env: {0}", envVC);
+ var envFuncs = new HashSet<string>();
+ impl2FuncCalls[impl].Iter(tup => envFuncs.Add(tup.Item1));
+ envFuncs.Iter(f => PrintFunction(existentialFunctions[f]));
+ }
+
+ var handler = impl2ErrorHandler[impl].Item1;
+ var collector = impl2ErrorHandler[impl].Item2;
+ collector.Reset(impl);
+
+ 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 (CommandLineOptions.Clo.Trace)
+ Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT");
+
+ if (collector.numErrors > 0)
+ {
+ var funcsChanged = collector.funcsChanged;
+
+ // 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.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s)));
+ }
+
+ prover.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + numProverQueries);
+ }
+
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ // Print the answer
+ existentialFunctions.Values.Iter(PrintFunction);
+ }
+ }
+
+ private void PrintFunction(Function function)
+ {
+ var tt = new TokenTextWriter(Console.Out);
+ 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();
+ }
+
+ public HashSet<string> HandleCounterExample(string impl, Counterexample error)
+ {
+ var funcsChanged = new HashSet<string>();
+ // Find the failing assert -- need to do a join there
+ // return the set of functions whose definition has changed
+ var cex = ExtractState(impl, error);
+ foreach (var tup in cex)
+ {
+ function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2);
+ funcsChanged.Add(tup.Item1);
+ }
+ return funcsChanged;
+ }
+
+ 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 || val is Microsoft.Basetypes.BigNum)
+ {
+ return model.MkElement(val.ToString());
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return null;
+ }
+ }
+
+ class AbsHoudiniCounterexampleCollector : VerifierCallback
+ {
+ public HashSet<string> funcsChanged;
+ public string currImpl;
+ public int numErrors;
+
+ AbsHoudini container;
+
+ public AbsHoudiniCounterexampleCollector(AbsHoudini container)
+ {
+ this.container = container;
+ Reset(null);
+ }
+
+ public void Reset(string impl)
+ {
+ funcsChanged = new HashSet<string>();
+ currImpl = impl;
+ numErrors = 0;
+ }
+
+ public override void OnCounterexample(Counterexample ce, string reason)
+ {
+ numErrors++;
+
+ funcsChanged.UnionWith(
+ container.HandleCounterExample(currImpl, ce));
+ }
+ }
+
+ private void GenVC(Implementation impl)
+ {
+ ModelViewInfo mvInfo;
+ System.Collections.Hashtable label2absy;
+ var collector = new AbsHoudiniCounterexampleCollector(this);
+ 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);
+
+ //CommandLineOptions.Clo.PrintInstrumented = true;
+ //var tt = new TokenTextWriter(Console.Out);
+ //impl.Emit(tt, 0);
+ //tt.Close();
+
+ // 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;
+ VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO);
+
+ var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context);
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO));
+ VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vcexpr = gen.Implies(eqExpr, vcexpr);
+ }
+
+ 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));
+
+ // HACK: push the definitions of constants involved in function calls
+ // It is possible that some constants only appear in function calls. Thus, when
+ // they are replaced by Boolean constants, it is possible that (get-value) will
+ // fail if the expression involves such constants. All we need to do is make sure
+ // these constants are declared, because otherwise, semantically we are doing
+ // the right thing.
+ foreach (var tup in fv.functionsUsed)
+ {
+ var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
+ tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
+ prover.Assert(tt, true);
+ }
+ }
+
+ private void Inline()
+ {
+ if (CommandLineOptions.Clo.InlineDepth < 0)
+ return;
+
+ var callGraph = BuildCallGraph();
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
+ inlineRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
+ freeRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
+ inlineEnsuresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
+ CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
+ Inliner.ProcessImplementationForHoudini(program, impl);
+ CommandLineOptions.Clo.ProcedureInlining = savedOption;
+ }
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+
+ Graph<Implementation> oldCallGraph = callGraph;
+ callGraph = new Graph<Implementation>();
+ foreach (Implementation impl in oldCallGraph.Nodes)
+ {
+ callGraph.AddSource(impl);
+ }
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
+ {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ int count = CommandLineOptions.Clo.InlineDepth;
+ while (count > 0)
+ {
+ foreach (Implementation impl in oldCallGraph.Nodes)
+ {
+ List<Implementation> newNodes = new List<Implementation>();
+ foreach (Implementation succ in callGraph.Successors(impl))
+ {
+ newNodes.AddRange(oldCallGraph.Successors(succ));
+ }
+ foreach (Implementation newNode in newNodes)
+ {
+ callGraph.AddEdge(impl, newNode);
+ }
+ }
+ count--;
+ }
+ }
+
+ private Graph<Implementation> BuildCallGraph()
+ {
+ Graph<Implementation> callGraph = new Graph<Implementation>();
+ Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || impl.SkipVerification) continue;
+ callGraph.AddSource(impl);
+ procToImpls[impl.Proc].Add(impl);
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || impl.SkipVerification) continue;
+ foreach (Block b in impl.Blocks)
+ {
+ foreach (Cmd c in b.Cmds)
+ {
+ CallCmd cc = c as CallCmd;
+ if (cc == null) continue;
+ foreach (Implementation callee in procToImpls[cc.Proc])
+ {
+ callGraph.AddEdge(impl, callee);
+ }
+ }
+ }
+ }
+ return callGraph;
+ }
+
+ }
+
+ 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 Intervals : IAbstractDomain
+ {
+ // [lower, upper]
+ int upper;
+ int lower;
+ // or: \bot
+ bool isBottom;
+ // number of times join has been performed
+ int nJoin;
+ // number of times before we widen
+ readonly static int maxJoin = 5;
+
+ public Intervals()
+ {
+ this.upper = 0;
+ this.lower = 0;
+ this.nJoin = 0;
+ this.isBottom = true;
+ }
+
+ private Intervals(int lower, int upper, int nJoin)
+ {
+ this.upper = upper;
+ this.lower = lower;
+ this.nJoin = nJoin;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new Intervals();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0] as Model.Integer;
+ if (state == null)
+ throw new AbsHoudiniInternalError("Incorrect type, expected int");
+ var intval = state.AsInt();
+
+ if (isBottom)
+ {
+ return new Intervals(intval, intval, 1);
+ }
+
+ if(intval >= lower && intval <= upper)
+ return this;
+
+ if (nJoin > maxJoin)
+ {
+ // widen
+ if (intval > upper)
+ return new Intervals(lower, Int32.MaxValue, 1);
+ if(intval < lower)
+ return new Intervals(Int32.MinValue, upper, 1);
+
+ Debug.Assert(false);
+ }
+
+ if (intval > upper)
+ return new Intervals(lower, intval, nJoin + 1);
+ if (intval < lower)
+ return new Intervals(intval, upper, nJoin + 1);
+
+ Debug.Assert(false);
+ return null;
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 1);
+ var v = vars[0];
+ if (isBottom) return Expr.False;
+ Expr ret = Expr.True;
+ if (lower != Int32.MinValue)
+ ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower)));
+ if (upper != Int32.MaxValue)
+ ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper)));
+ return ret;
+ }
+
+ }
+
+ public class PredicateAbsElem : IAbstractDomain
+ {
+ public static class ExprExt
+ {
+ public static Expr AndSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.True) return e2;
+ if (e2 == Expr.True) return e1;
+ if (e1 == Expr.False || e2 == Expr.False) return Expr.False;
+ return Expr.And(e1, e2);
+ }
+
+ public static Expr OrSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.False) return e2;
+ if (e2 == Expr.False) return e1;
+ if (e1 == Expr.True || e2 == Expr.True) return Expr.True;
+ return Expr.Or(e1, e2);
+ }
+ }
+
+ class Disjunct
+ {
+ public static int DisjunctBound = 3;
+ HashSet<int> pos;
+ HashSet<int> neg;
+ bool isTrue;
+
+ public Disjunct()
+ {
+ isTrue = true;
+ pos = new HashSet<int>();
+ neg = new HashSet<int>();
+ }
+
+ public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ {
+ this.isTrue = false;
+ this.pos = new HashSet<int>(pos);
+ this.neg = new HashSet<int>(neg);
+ if (this.pos.Overlaps(this.neg))
+ {
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+ if (this.pos.Count + this.neg.Count > DisjunctBound)
+ {
+ // Set to true
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+
+ }
+
+ public Disjunct OR(Disjunct that)
+ {
+ if (isTrue)
+ return this;
+ if (that.isTrue)
+ return that;
+
+ return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
+ }
+
+ public bool Implies(Disjunct that)
+ {
+ if (isTrue) return that.isTrue;
+ if (that.isTrue) return true;
+
+ return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isTrue) return Expr.True;
+ Expr ret = Expr.False;
+ pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i]));
+ neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i])));
+ return ret;
+ }
+ }
+
+ // Conjunction of Disjuncts
+ List<Disjunct> conjuncts;
+ bool isFalse;
+
+ public PredicateAbsElem()
+ {
+ this.conjuncts = new List<Disjunct>();
+ this.isFalse = true;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new PredicateAbsElem();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> state)
+ {
+ if (state.Any(me => !(me is Model.Boolean)))
+ throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool");
+
+ // quick return if this == true
+ if (!this.isFalse && conjuncts.Count == 0)
+ return this;
+
+ var ret = new PredicateAbsElem();
+ ret.isFalse = false;
+
+ for (int i = 0; i < state.Count; i++)
+ {
+ var b = (state[i] as Model.Boolean).Value;
+ Disjunct d = null;
+ if (b) d = new Disjunct(new int[] { i }, new int[] { });
+ else d = new Disjunct(new int[] { }, new int[] { i });
+
+ if (isFalse)
+ ret.AddDisjunct(d);
+ else
+ {
+ conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
+ }
+ }
+
+ return ret;
+
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isFalse) return Expr.False;
+ Expr ret = Expr.True;
+
+ foreach (var c in conjuncts)
+ {
+ ret = ExprExt.AndSimp(ret, c.Gamma(vars));
+ }
+
+ return ret;
+ }
+
+ private void AddDisjunct(Disjunct d)
+ {
+ if (conjuncts.Any(c => c.Implies(d)))
+ return;
+
+ conjuncts.RemoveAll(c => d.Implies(c));
+ conjuncts.Add(d);
+ }
+ }
+
+ // [false -- (x == true) -- true]
+ public class HoudiniConst : IAbstractDomain
+ {
+ bool isBottom;
+ bool isTop;
+
+ private HoudiniConst(bool isTop, bool isBottom)
+ {
+ this.isBottom = isBottom;
+ this.isTop = isTop;
+ Debug.Assert(!(isTop && isBottom));
+ }
+
+ public static HoudiniConst GetExtObj()
+ {
+ return new HoudiniConst(false, false);
+ }
+
+ public static HoudiniConst GetTop()
+ {
+ return new HoudiniConst(true, false);
+ }
+
+ public static HoudiniConst GetBottom()
+ {
+ return new HoudiniConst(false, true);
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return GetBottom();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0];
+
+ if (isTop) return this;
+
+ if (state is Model.Boolean)
+ {
+ if ((state as Model.Boolean).Value)
+ return GetExtObj();
+ }
+
+ return GetTop();
+ }
+
+ 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;
+ return v;
+ }
+ }
+
+
+ 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
@@ -200,6 +1315,9 @@ namespace Microsoft.Boogie.Houdini { var s = tup.Value as PredicateAbs;
if (s == null) continue;
ret.UnionWith(s.GetPredicates(program, prover.VCExprGen, prover));
+ // debug output
+ //Console.WriteLine("Summary of {0}:", tup.Key);
+ //Console.WriteLine("{0}", tup.Value);
}
prover.Close();
@@ -516,10 +1634,8 @@ namespace Microsoft.Boogie.Houdini { //Console.WriteLine("Checking: {0}", vc);
if (CommandLineOptions.Clo.Trace)
- {
Console.WriteLine("Verifying {0} ({1}): {2}", impl.Name, usedLower ? "lower" : "ac", query);
- }
-
+
if (usedLower && lowerTime.TotalMilliseconds >= iterTimeLimit && iterTimeLimit >= 0)
{
if (UseBilateralAlgo)
@@ -1772,7 +2888,6 @@ namespace Microsoft.Boogie.Houdini { var ret = "";
if (isFalse) return "false";
var first = true;
- Simplify();
for(int i = 0; i < PostPreds[procName].Count; i++)
{
@@ -2158,7 +3273,7 @@ namespace Microsoft.Boogie.Houdini { public class PredicateAbsConjunct
{
- static int ConjunctBound = 2;
+ static int ConjunctBound = 3;
public bool isFalse { get; private set; }
HashSet<int> posPreds;
@@ -2279,8 +3394,10 @@ namespace Microsoft.Boogie.Houdini { {
if (isFalse) return Expr.False;
Expr ret = Expr.True;
- posPreds.Iter(p => ret = Expr.And(ret, predToExpr(p)));
- negPreds.Iter(p => ret = Expr.And(ret, Expr.Not(predToExpr(p))));
+ var pp = posPreds.ToList(); pp.Sort();
+ var np = negPreds.ToList(); np.Sort();
+ pp.Iter(p => ret = Expr.And(ret, predToExpr(p)));
+ np.Iter(p => ret = Expr.And(ret, Expr.Not(predToExpr(p))));
return ret;
}
@@ -2377,6 +3494,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;
@@ -2394,6 +3559,9 @@ namespace Microsoft.Boogie.Houdini { }
}
+ public class AbsHoudiniAssemblyLocator
+ {
+ }
public class AbsHoudiniInternalError : System.ApplicationException
{
|