using System; using System.Collections.Generic; using System.Linq; using System.Text; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using VC; using Outcome = VC.VCGen.Outcome; using Bpl = Microsoft.Boogie; using System.Diagnostics; using System.Diagnostics.Contracts; using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie.Houdini { public class AbsHoudini { Dictionary existentialFunctions; Program program; Dictionary name2Impl; Dictionary impl2VC; Dictionary>> impl2FuncCalls; // constant -> the naryexpr that it replaced Dictionary constant2FuncCall; // function -> its abstract value Dictionary function2Value; // impl -> functions assumed/asserted Dictionary> impl2functionsAsserted, impl2functionsAssumed; // funtions -> impls where assumed/asserted Dictionary> function2implAssumed, function2implAsserted; // impl -> handler, collector Dictionary> impl2ErrorHandler; // Essentials: VCGen, Prover VCGen vcgen; ProverInterface prover; // Stats TimeSpan proverTime; int numProverQueries; public AbsHoudini(Program program, IAbstractDomain defaultElem) { this.program = program; this.impl2VC = new Dictionary(); this.impl2FuncCalls = new Dictionary>>(); this.existentialFunctions = new Dictionary(); this.name2Impl = new Dictionary(); this.impl2functionsAsserted = new Dictionary>(); this.impl2functionsAssumed = new Dictionary>(); this.function2implAsserted = new Dictionary>(); this.function2implAssumed = new Dictionary>(); this.impl2ErrorHandler = new Dictionary>(); this.constant2FuncCall = new Dictionary(); // Find the existential functions foreach (var func in program.Functions .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential"))) existentialFunctions.Add(func.Name, func); this.function2Value = new Dictionary(); 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())); // type check existentialFunctions.Values.Iter(func => { if (func.OutParams.Count != 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)); 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) // CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); 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, CommandLineOptions.Clo.ProverKillTime); this.proverTime = TimeSpan.Zero; this.numProverQueries = 0; program.Implementations .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 VCGenOutcome ComputeSummaries() { var overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Valid, new List()); // Compute SCCs and determine a priority order for impls var Succ = new Dictionary>(); var Pred = new Dictionary>(); name2Impl.Keys.Iter(s => Succ[s] = new HashSet()); name2Impl.Keys.Iter(s => Pred[s] = new HashSet()); foreach(var impl in name2Impl.Keys) { Succ[impl] = new HashSet(); impl2functionsAsserted[impl].Iter(f => function2implAssumed[f].Iter(succ => { Succ[impl].Add(succ); Pred[succ].Add(impl); })); } var sccs = new StronglyConnectedComponents(name2Impl.Keys, new Adjacency(n => Pred[n]), new Adjacency(n => Succ[n])); sccs.Compute(); // impl -> priority var impl2Priority = new Dictionary(); int p = 0; foreach (var scc in sccs) { foreach (var impl in scc) { impl2Priority.Add(impl, p); p++; } } var worklist = new SortedSet>(); 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; var terms = new List(); foreach (var tup in impl2FuncCalls[impl]) { var controlVar = tup.Item2; var exprVars = tup.Item3; var varList = new List(); exprVars.Args.OfType().Iter(v => varList.Add(v)); var args = new List(); controlVar.InParams.Iter(v => args.Add(Expr.Ident(v))); Expr term = Expr.Eq(new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args), function2Value[tup.Item1].Gamma(varList)); if (controlVar.InParams.Count != 0) { term = new ForallExpr(Token.NoToken, new List(controlVar.InParams.ToArray()), new Trigger(Token.NoToken, true, new List { new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args) }), term); } terms.Add(term); } var env = Expr.BinaryTreeAnd(terms); 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(); 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) { // 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"); if (collector.numErrors > 0) { var funcsChanged = collector.funcsChanged; if (funcsChanged.Count == 0) { overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Invalid, collector.errors); break; } // propagate dependent guys back into the worklist, including self var deps = new HashSet(); 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); } return overallOutcome; } public IEnumerable GetAssignment() { var ret = new List(); foreach (var func in existentialFunctions.Values) { var invars = new List(func.InParams.OfType().Select(v => Expr.Ident(v))); func.Body = function2Value[func.Name].Gamma(invars); ret.Add(func); } return ret; } private void PrintFunction(Function function) { var tt = new TokenTextWriter(Console.Out, /*pretty=*/ false); var invars = new List(function.InParams.OfType().Select(v => Expr.Ident(v))); function.Body = function2Value[function.Name].Gamma(invars); function.Emit(tt, 0); tt.Close(); } public HashSet HandleCounterExample(string impl, Counterexample error) { var funcsChanged = new HashSet(); // 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>> 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().FirstOrDefault(ac => ac.Requires == failingRequires); } ReturnCounterexample returnCounterexample = error as ReturnCounterexample; if (returnCounterexample != null) { Ensures failingEnsures = returnCounterexample.FailingEnsures; failingAssert = lastBlock.Cmds.OfType().FirstOrDefault(ac => ac.Ensures == failingEnsures); } AssertCounterexample assertCounterexample = error as AssertCounterexample; if (assertCounterexample != null) { failingAssert = lastBlock.Cmds.OfType().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert); } Debug.Assert(failingAssert != null); return ExtractState(impl, failingAssert.Expr, error.Model); } private static int existentialConstCounter = 0; private List>> ExtractState(string impl, Expr expr, Model model) { var funcsUsed = FunctionCollector.Collect(expr); var ret = new List>>(); foreach (var tup in funcsUsed.Where(t => t.Item2 == null)) { var constant = tup.Item1; if (!constant2FuncCall.ContainsKey(constant.Name)) continue; var func = constant2FuncCall[constant.Name]; var funcName = (func.Fun as FunctionCall).FunctionName; var vals = new List(); prover.Context.BoogieExprTranslator.Translate(func.Args).Iter(ve => vals.Add(getValue(ve, model))); ret.Add(Tuple.Create(funcName, vals)); } foreach (var tup in funcsUsed.Where(t => t.Item2 != null)) { var constant = tup.Item1; var boundExpr = tup.Item2; if (!constant2FuncCall.ContainsKey(constant.Name)) continue; // There are some bound variables (because the existential function was inside an \exists). // We must find an assignment for bound varibles // First, peice apart the existential functions var cd = new Duplicator(); var tup2 = ExistentialExprModelMassage.Massage(cd.VisitExpr(boundExpr.Body)); var be = tup2.Item1; Expr env = Expr.True; foreach (var ahFunc in tup2.Item2) { var tup3 = impl2FuncCalls[impl].First(t => t.Item2.Name == ahFunc.Name); var varList = new List(); tup3.Item3.Args.OfType().Iter(v => varList.Add(v)); env = Expr.And(env, function2Value[tup3.Item1].Gamma(varList)); } be = Expr.And(be, Expr.Not(env)); // map formals to constants var formalToConstant = new Dictionary(); foreach (var f in boundExpr.Dummies.OfType()) formalToConstant.Add(f.Name, new Constant(Token.NoToken, new TypedIdent(Token.NoToken, f.Name + "@subst@" + (existentialConstCounter++), f.TypedIdent.Type), false)); be = Substituter.Apply(new Substitution(v => formalToConstant.ContainsKey(v.Name) ? Expr.Ident(formalToConstant[v.Name]) : Expr.Ident(v)), be); formalToConstant.Values.Iter(v => prover.Context.DeclareConstant(v, false, null)); var reporter = new AbstractHoudiniErrorReporter(); var ve = prover.Context.BoogieExprTranslator.Translate(be); prover.Assert(ve, true); prover.Check(); var proverOutcome = prover.CheckOutcomeCore(reporter); if (proverOutcome != ProverInterface.Outcome.Invalid) continue; model = reporter.model; var func = constant2FuncCall[constant.Name]; var funcName = (func.Fun as FunctionCall).FunctionName; var vals = new List(); foreach (var funcArg in func.Args.OfType()) { var arg = Substituter.Apply(new Substitution(v => formalToConstant.ContainsKey(v.Name) ? Expr.Ident(formalToConstant[v.Name]) : Expr.Ident(v)), funcArg); vals.Add(getValue(prover.Context.BoogieExprTranslator.Translate(arg), 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 if (arg is VCExprNAry && (arg as VCExprNAry).Op is VCExprBvOp) { // support for BV constants var bvc = (arg as VCExprNAry)[0] as VCExprLiteral; if (bvc != null) { var ret = model.TryMkElement(bvc.ToString() + arg.Type.ToString()); if (ret != null && (ret is Model.BitVector)) return ret; } } 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; } // Remove functions AbsHoudiniConstant from the expressions and substitute them with "true" class ExistentialExprModelMassage : StandardVisitor { List ahFuncs; public ExistentialExprModelMassage() { ahFuncs = new List(); } public static Tuple> Massage(Expr expr) { var ee = new ExistentialExprModelMassage(); expr = ee.VisitExpr(expr); return Tuple.Create(expr, ee.ahFuncs); } public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall && (node.Fun as FunctionCall).FunctionName.StartsWith("AbsHoudiniConstant")) { ahFuncs.Add((node.Fun as FunctionCall).Func); return Expr.True; } return base.VisitNAryExpr(node); } } class FunctionCollector : ReadOnlyVisitor { public List> functionsUsed; ExistsExpr existentialExpr; public FunctionCollector() { functionsUsed = new List>(); existentialExpr = null; } public static List> Collect(Expr expr) { var fv = new FunctionCollector(); fv.VisitExpr(expr); return fv.functionsUsed; } public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { var oldE = existentialExpr; if (node is ExistsExpr) existentialExpr = (node as ExistsExpr); node = base.VisitQuantifierExpr(node); existentialExpr = oldE; return node; } public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall) { var collector = new VariableCollector(); collector.Visit(node); if(existentialExpr != null && existentialExpr.Dummies.Intersect(collector.usedVars).Any()) functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).Func, existentialExpr)); else functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).Func, null)); } return base.VisitNAryExpr(node); } } class AbsHoudiniCounterexampleCollector : VerifierCallback { public HashSet funcsChanged; public string currImpl; public int numErrors; public List errors; AbsHoudini container; public AbsHoudiniCounterexampleCollector(AbsHoudini container) { this.container = container; Reset(null); } public void Reset(string impl) { funcsChanged = new HashSet(); currImpl = impl; numErrors = 0; errors = new List(); } public override void OnCounterexample(Counterexample ce, string reason) { numErrors++; errors.Add(ce); funcsChanged.UnionWith( container.HandleCounterExample(currImpl, ce)); } } private void GenVC(Implementation impl) { ModelViewInfo mvInfo; Dictionary 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); // Inline functions (new InlineFunctionCalls()).VisitBlockList(impl.Blocks); ExtractQuantifiedExprs(impl); StripOutermostForall(impl); //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(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 List(), 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) { // Ignore ones with bound varibles if (tup.Item2.InParams.Count > 0) continue; var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3); tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt); prover.Assert(tt, true); } } // convert "foo(... forall e ...) to: // (p iff forall e) ==> foo(... p ...) // where p is a fresh boolean variable and foo is an existential constant private void ExtractQuantifiedExprs(Implementation impl) { var funcs = new HashSet(existentialFunctions.Keys); foreach (var blk in impl.Blocks) { foreach (var acmd in blk.Cmds.OfType()) { var ret = ExtractQuantifiers.Extract(acmd.Expr, funcs); acmd.Expr = ret.Item1; impl.LocVars.AddRange(ret.Item2); } } } // convert "assert e1 && forall x: e2" to // assert e1 && e2[x <- x@bound] private void StripOutermostForall(Implementation impl) { var funcs = new HashSet(existentialFunctions.Keys); foreach (var blk in impl.Blocks) { foreach (var acmd in blk.Cmds.OfType()) { var ret = StripQuantifiers.Run(acmd.Expr, funcs); acmd.Expr = ret.Item1; impl.LocVars.AddRange(ret.Item2); } } } private void Inline() { if (CommandLineOptions.Clo.InlineDepth < 0) return; var callGraph = BuildCallGraph(); 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 oldCallGraph = callGraph; callGraph = new Graph(); foreach (Implementation impl in oldCallGraph.Nodes) { callGraph.AddSource(impl); } foreach (Tuple 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 newNodes = new List(); foreach (Implementation succ in callGraph.Successors(impl)) { newNodes.AddRange(oldCallGraph.Successors(succ)); } foreach (Implementation newNode in newNodes) { callGraph.AddEdge(impl, newNode); } } count--; } } private Graph BuildCallGraph() { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); foreach (var proc in program.Procedures) { procToImpls[proc] = new HashSet(); } foreach (var impl in program.Implementations) { if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } foreach (var impl in program.Implementations) { if (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 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; public List boolConstants; public HashSet functionsAssumed; public HashSet functionsAsserted; HashSet functionsToReplace; private bool inAssume; private bool inAssert; private bool inFunction; private List> boundVars; private static int IdCounter = 0; public ReplaceFunctionCalls(HashSet functionsToReplace) { this.functionsUsed = new List>(); this.functionsToReplace = functionsToReplace; this.functionsAsserted = new HashSet(); this.functionsAssumed = new HashSet(); this.boolConstants = new List(); this.boundVars = new List>(); inAssume = false; inAssert = false; inFunction = 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 QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { // gather the quantified variables var dummies = new Dictionary(); node.Dummies.Iter(v => dummies.Add(v.Name, v)); boundVars.Add(dummies); node = base.VisitQuantifierExpr(node); boundVars.RemoveAt(boundVars.Count - 1); return node; } public override Expr VisitNAryExpr(NAryExpr node) { var inF = inFunction; if (node.Fun is FunctionCall && functionsToReplace.Contains((node.Fun as FunctionCall).FunctionName)) { found((node.Fun as FunctionCall).FunctionName); inFunction = true; // collect all the variables used by this function var collector = new VariableCollector(); collector.VisitExpr(node); // Find the outermost bound variables var bound = new List(); if(boundVars.Count > 0) bound.AddRange(collector.usedVars.Intersect(boundVars[0].Values)); // create boolean function to replace this guy var constant = new Function(Token.NoToken, "AbsHoudiniConstant" + IdCounter, bound, new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "r", Microsoft.Boogie.Type.Bool), false)); IdCounter++; functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).FunctionName, constant, node)); boolConstants.Add(constant); var args = new List(); bound.OfType().Select(v => Expr.Ident(v)).Iter(v => args.Add(v)); return new NAryExpr(Token.NoToken, new FunctionCall(constant), args); } var ret = base.VisitNAryExpr(node); inFunction = inF; return ret; } public override Expr VisitIdentifierExpr(IdentifierExpr node) { if (inFunction) { // Inside functions we can only refer to the outermost bound variables for (int i = boundVars.Count - 1; i >= 1; i--) { if (boundVars[i].ContainsKey(node.Name)) throw new AbsHoudiniInternalError("Existential functions can only refer to outermost bound variables in an expression"); } } return base.VisitIdentifierExpr(node); } private void found(string func) { if (inAssume) functionsAssumed.Add(func); if (inAssert) functionsAsserted.Add(func); } } // convert "foo(... forall e ...) to: // (p iff forall e) ==> foo(... p ...) // where p is a fresh boolean variable and foo is an existential constant class ExtractQuantifiers : StandardVisitor { static int freshConstCounter = 0; HashSet existentialFunctions; bool insideExistential; Dictionary newConstants; private ExtractQuantifiers(HashSet existentialFunctions) { this.existentialFunctions = existentialFunctions; insideExistential = false; newConstants = new Dictionary(); } public static Tuple> Extract(Expr expr, HashSet existentialFunctions) { var eq = new ExtractQuantifiers(existentialFunctions); expr = eq.VisitExpr(expr); Expr ret = Expr.True; foreach (var tup in eq.newConstants) { ret = Expr.And(ret, Expr.Eq(Expr.Ident(tup.Key), tup.Value)); } ret = Expr.Imp(ret, expr); return Tuple.Create(ret, eq.newConstants.Keys.AsEnumerable()); } public override Expr VisitNAryExpr(NAryExpr node) { var oldIE = insideExistential; if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName)) insideExistential = true; var ret = base.VisitNAryExpr(node); insideExistential = oldIE; return ret; } public override Expr VisitExpr(Expr node) { if (node is QuantifierExpr) { return MyVisitQuantifierExpr(node as QuantifierExpr); } return base.VisitExpr(node); } public Expr MyVisitQuantifierExpr(QuantifierExpr node) { node = base.VisitQuantifierExpr(node); if (insideExistential) { var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "quant@const" + freshConstCounter, Microsoft.Boogie.Type.Bool), false); freshConstCounter++; newConstants.Add(constant, node); return Expr.Ident(constant); } return node; } } // convert "assert e1 && forall x: e2" to // assert e1 && e2[x <- x@bound] // only if e2 has an existential function class StripQuantifiers : StandardVisitor { static int boundVarCounter = 0; // 0 -> None, 1 -> Forall, 2 -> Exists, 3 -> Nested int insideQuantifier; bool searchExistentialFunction; bool foundExistentialFunction; HashSet existentialFunctions; Dictionary subst; List LocalsToAdd; private StripQuantifiers(HashSet existentialFunctions) { this.existentialFunctions = existentialFunctions; insideQuantifier = 0; searchExistentialFunction = false; foundExistentialFunction = false; LocalsToAdd = new List(); subst = null; } public static Tuple> Run(Expr expr, HashSet existentialFunctions) { // check for type errors first var sq = new StripQuantifiers(existentialFunctions); var ret = sq.VisitExpr(expr); return Tuple.Create(ret, sq.LocalsToAdd); } public override Expr VisitExpr(Expr node) { if (node is QuantifierExpr) { return MyVisitQuantifierExpr(node as QuantifierExpr); } return base.VisitExpr(node); } private Expr MyVisitQuantifierExpr(QuantifierExpr node) { var oldIQ = insideQuantifier; Expr ret = node; // update "insideQuantifier" if (insideQuantifier == 0) { if (node is ForallExpr) insideQuantifier = 1; else insideQuantifier = 2; } else if (insideQuantifier > 0) { insideQuantifier = 3; } // Going inside Forall? if (insideQuantifier == 1) { // see if there is any existential function inside searchExistentialFunction = true; foundExistentialFunction = false; base.VisitQuantifierExpr(node); if (foundExistentialFunction) { // create substitution to apply subst = new Dictionary(); foreach (var bv in node.Dummies.OfType()) { var lv = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, bv + "@bound" + boundVarCounter, bv.TypedIdent.Type)); boundVarCounter++; subst.Add(bv.Name, lv); LocalsToAdd.Add(lv); } // apply the subst var body = base.VisitExpr(node.Body); ret = body; subst = null; } else { ret = base.VisitQuantifierExpr(node); } searchExistentialFunction = false; foundExistentialFunction = false; } else { ret = base.VisitQuantifierExpr(node); } insideQuantifier = oldIQ; return ret; } public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName)) { if (insideQuantifier == 3) throw new AbsHoudiniInternalError("Existential function found inside exists, or nested foralls"); if (searchExistentialFunction) foundExistentialFunction = true; } return base.VisitNAryExpr(node); } public override Expr VisitIdentifierExpr(IdentifierExpr node) { if (subst != null && subst.ContainsKey(node.Name)) return Expr.Ident(subst[node.Name]); return base.VisitIdentifierExpr(node); } } 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 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); 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 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 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 { 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 pos; HashSet neg; bool isTrue; public Disjunct() { isTrue = true; pos = new HashSet(); neg = new HashSet(); } public Disjunct(IEnumerable pos, IEnumerable neg) { this.isTrue = false; this.pos = new HashSet(pos); this.neg = new HashSet(neg); if (this.pos.Overlaps(this.neg)) { this.isTrue = true; this.pos = new HashSet(); this.neg = new HashSet(); } if (this.pos.Count + this.neg.Count > DisjunctBound) { // Set to true this.isTrue = true; this.pos = new HashSet(); this.neg = new HashSet(); } } 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 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 conjuncts; bool isFalse; public PredicateAbsElem() { this.conjuncts = new List(); this.isFalse = true; } public IAbstractDomain Bottom() { 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))) 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 vars) { if (isFalse) return Expr.False; Expr ret = Expr.True; foreach (var c in conjuncts) { ret = ExprExt.AndSimp(ret, c.Gamma(vars)); } 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))) 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 MakeTop(out bool changed) { changed = false; if (isTop) return this; changed = true; return GetTop(); } public IAbstractDomain Join(List 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 vars) { Debug.Assert(vars.Count == 1); var v = vars[0]; if (isBottom) return Expr.False; 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; } } // foo(x) = x < 2^j for some j <= 16 public class PowDomain : IAbstractDomain { enum Val { FALSE, NEITHER, TRUE }; Val tlevel; bool isBottom { get { return tlevel == Val.FALSE; } } bool isTop { get { return tlevel == Val.TRUE; } } readonly int Max = 16; int upper; // <= Max private PowDomain(Val tlevel) : this(tlevel, 0) { } private PowDomain(Val tlevel, int upper) { this.tlevel = tlevel; this.upper = upper; } public static IAbstractDomain GetBottom() { 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(); } IAbstractDomain IAbstractDomain.Join(List state) { if (isTop) return this; int v = 0; if (state[0] is Model.BitVector) v = (state[0] as Model.BitVector).AsInt(); else if (state[0] is Model.Integer) v = (state[0] as Model.Integer).AsInt(); else Debug.Assert(false); var nupper = upper; while ((1 << nupper) < v) nupper++; var ntlevel = Val.NEITHER; if (nupper > Max) ntlevel = Val.TRUE; return new PowDomain(ntlevel, nupper); } Expr IAbstractDomain.Gamma(List vars) { if (isBottom) return Expr.False; if (isTop) return Expr.True; var v = vars[0]; if (v.Type.IsBv) { var bits = v.Type.BvBits; if (!AbstractDomainFactory.bvslt.ContainsKey(bits)) throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString()); var bvslt = AbstractDomainFactory.bvslt[bits]; return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new List { v, new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32) }); } else { return Expr.Lt(v, Expr.Literal(1 << (upper+1))); } } bool IAbstractDomain.TypeCheck(List argTypes, out string msg) { msg = ""; if (argTypes.Count != 1) { msg = "Illegal number of arguments, expecting 1"; return false; } if (argTypes.Any(tt => !tt.IsInt && !tt.IsBv)) { msg = "Illegal type, expecting int or bv"; return false; } return true; } } // foo(x_i) = all equalities that hold public class EqualitiesDomain : IAbstractDomain { bool isBottom; List> equalities; public EqualitiesDomain(bool isBottom, List> eq) { this.isBottom = isBottom; this.equalities = eq; } public static IAbstractDomain GetBottom() { return new EqualitiesDomain(true, new List>()); } IAbstractDomain IAbstractDomain.Bottom() { 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 var eq = new List>(); for (int i = 0; i < state.Count; i++) { var added = false; foreach (var s in eq) { var sv = s.First(); if (state[i].ToString() == state[sv].ToString()) { s.Add(i); added = true; break; } } if (!added) eq.Add(new HashSet(new int[] { i })); } if (isBottom) { return new EqualitiesDomain(false, eq); } // intersect two partitions equalities and eq var m1 = GetMap(equalities, state.Count); var m2 = GetMap(eq, state.Count); for (int i = 0; i < state.Count; i++) m2[i] = new HashSet(m2[i].Intersect(m1[i])); // map from representative to set var repToSet = new Dictionary>(); for (int i = 0; i < state.Count; i++) { var rep = m2[i].Min(); if (!repToSet.ContainsKey(rep)) repToSet[rep] = m2[i]; } var ret = new List>(); repToSet.Values.Iter(s => ret.Add(s)); return new EqualitiesDomain(false, ret); } Expr IAbstractDomain.Gamma(List vars) { if (isBottom) return Expr.False; Expr ret = Expr.True; foreach (var eq in equalities.Select(hs => hs.ToList())) { if (eq.Count == 1) continue; var prev = eq[0]; for (int i = 1; i < eq.Count; i++) { ret = Expr.And(ret, Expr.Eq(vars[prev], vars[eq[i]])); prev = eq[i]; } } return ret; } bool IAbstractDomain.TypeCheck(List argTypes, out string msg) { msg = ""; if (argTypes.Count == 0) return true; var ot = argTypes[0]; if (argTypes.Any(tt => !tt.Equals(ot))) { msg = string.Format("Illegal type, expecting type {0}, got {1}", ot, argTypes.First(tt => !tt.Equals(ot))); return false; } return true; } private HashSet[] GetMap(List> eq, int n) { var ret = new HashSet[n]; foreach (var s in eq) { foreach (var i in s) ret[i] = s; } return ret; } } // foo(a,b) \in {false, \not a, a ==> b, true} public class ImplicationDomain : IAbstractDomain { enum Val {FALSE, NOT_A, A_IMP_B, TRUE}; Val val; private ImplicationDomain(Val val) { this.val = val; } public static ImplicationDomain GetBottom() { return new ImplicationDomain(Val.FALSE); } public IAbstractDomain Bottom() { 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); var v1 = (states[0] as Model.Boolean).Value; var v2 = (states[1] as Model.Boolean).Value; if (val == Val.TRUE) return this; var that = Val.TRUE; if (!v1) that = Val.NOT_A; else if (!v1 || v2) that = Val.A_IMP_B; if (that == Val.TRUE || val == Val.FALSE) return new ImplicationDomain(that); // Now, neither this or that is FALSE or TRUE if (val == that) return this; Debug.Assert(val == Val.A_IMP_B || that == Val.A_IMP_B); return new ImplicationDomain(Val.A_IMP_B); } public Expr Gamma(List vars) { Debug.Assert(vars.Count == 2); var v1 = vars[0]; var v2 = vars[1]; if (val == Val.FALSE) return Expr.False; if (val == Val.TRUE) return Expr.True; if (val == Val.NOT_A) return Expr.Not(v1); return Expr.Imp(v1, v2); } public bool TypeCheck(List argTypes, out string msg) { msg = ""; if (argTypes.Count != 2) { msg = "Illegal number of arguments, expecting 2"; return false; } if (argTypes.Any(tt => !tt.IsBool)) { msg = "Illegal type, expecting bool"; return false; } return true; } } 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); } 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; 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 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 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 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; } } public class IndependentAttribute : IAbstractDomain where T : class, IAbstractDomain { bool isBottom; int numVars; List varVal; T underlyingInstance; public IndependentAttribute() { isBottom = true; numVars = 0; varVal = new List(); underlyingInstance = null; } public IAbstractDomain Bottom() { 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(); 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(); ret.isBottom = false; ret.numVars = state.Count; for(int i = 0; i < state.Count; i++) { var sl = new List(); 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 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(); 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 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(); // bitvector operations public static Dictionary bvslt = new Dictionary(); 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) { var Name = type.FullName; Debug.Assert(abstractDomainInstances.ContainsKey(Name)); return abstractDomainInstances[Name] as IAbstractDomain; } public static IAbstractDomain GetInstance(string friendlyName) { if (!abstractDomainInstancesFriendly.ContainsKey(friendlyName)) { Console.WriteLine("Domain {0} not found", friendlyName); 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(Program program) { // Declare abstract domains var domains = new List>(new System.Tuple[] { System.Tuple.Create("HoudiniConst", HoudiniConst.GetBottom() as IAbstractDomain), System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain), System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain), System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain), System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain), System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain), System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain), System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute() as IAbstractDomain), System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute() as IAbstractDomain), System.Tuple.Create("IA[Intervals]", new IndependentAttribute() as IAbstractDomain), System.Tuple.Create("IA[PowDomain]", new IndependentAttribute() as IAbstractDomain), }); domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2)); program.Functions.Iter(RegisterFunction); } private static void RegisterFunction(Function func) { var attr = QKeyValue.FindStringAttribute(func.Attributes, "bvbuiltin"); if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv) bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func); } } 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); } public class AbstractHoudini { // Input Program Program program; // Impl -> VC Dictionary impl2VC; // Impl -> Vars at end of the impl Dictionary> impl2EndStateVars; // Impl -> (callee,summary pred) Dictionary>> impl2CalleeSummaries; // pointer to summary class ISummaryElement summaryClass; // impl -> summary Dictionary impl2Summary; // name -> impl Dictionary name2Impl; // Use Bilateral algorithm public static bool UseBilateralAlgo = true; public static int iterTimeLimit = -1; // ms public static readonly string summaryPredSuffix = "SummaryPred"; // Essentials: VCGen, Prover, and reporter VCGen vcgen; ProverInterface prover; AbstractHoudiniErrorReporter reporter; // Stats TimeSpan proverTime; int numProverQueries; // Produce witness for correctness: can be set programmatically public static string WitnessFile = "absHoudiniWitness.bpl"; public AbstractHoudini(Program program) { this.program = program; this.impl2VC = new Dictionary(); this.impl2EndStateVars = new Dictionary>(); this.impl2CalleeSummaries = new Dictionary>>(); this.impl2Summary = new Dictionary(); this.name2Impl = SimpleUtil.nameImplMapping(program); if (CommandLineOptions.Clo.ProverKillTime > 0) CommandLineOptions.Clo.AddProverOption(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); 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.reporter = new AbstractHoudiniErrorReporter(); this.proverTime = TimeSpan.Zero; this.numProverQueries = 0; if (CommandLineOptions.Clo.AbstractHoudini == "0") UseBilateralAlgo = false; } public void computeSummaries(ISummaryElement summaryClass) { // TODO: move this some place else PredicateAbs.FindUnsatPairs(prover.VCExprGen, prover); this.summaryClass = summaryClass; name2Impl.Values.Iter(attachEnsures); program.Implementations .Iter(impl => impl2Summary.Add(impl.Name, summaryClass.GetFlaseSummary(program, impl))); // Build call graph var Succ = new Dictionary>(); var Pred = new Dictionary>(); name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet())); name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet())); foreach (var impl in program.Implementations) { foreach (var blk in impl.Blocks) { foreach (var cmd in blk.Cmds.OfType()) { if (!name2Impl.ContainsKey(cmd.callee)) continue; Succ[impl].Add(name2Impl[cmd.callee]); Pred[name2Impl[cmd.callee]].Add(impl); } } } // Build SCC var sccs = new StronglyConnectedComponents(name2Impl.Values, new Adjacency(n => Pred[n]), new Adjacency(n => Succ[n])); sccs.Compute(); // impl -> priority var impl2Priority = new Dictionary(); int p = 0; foreach (var scc in sccs) { foreach (var impl in scc) { impl2Priority.Add(impl.Name, p); p++; } } Inline(); #region Witness generation setup // Create a copy of the program var copy = new Dictionary(); if (WitnessFile != null) { foreach (var impl in program.Implementations) { var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, new List(impl.LocVars), new List()); foreach (var blk in impl.Blocks) { var cd = new CodeCopier(); nimpl.Blocks.Add(new Block(Token.NoToken, blk.Label, cd.CopyCmdSeq(blk.Cmds), cd.CopyTransferCmd(blk.TransferCmd))); } copy.Add(impl.Name, nimpl); } } #endregion // Turn off subsumption. Why? Because then I see multiple occurences of the // attached ensures in the VC CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never; // Create all VCs name2Impl.Values .Iter(GenVC); // Start the iteration var worklist = new SortedSet>(); name2Impl.Values .Iter(impl => worklist.Add(Tuple.Create(impl2Priority[impl.Name], impl))); while (worklist.Any()) { var impl = worklist.First().Item2; worklist.Remove(worklist.First()); var changed = ProcessImpl(impl); if (changed) { Pred[impl].Where(pred => UseBilateralAlgo || pred != impl).Iter(pred => worklist.Add(Tuple.Create(impl2Priority[pred.Name], pred))); } } var allImpls = new SortedSet>(); name2Impl.Values.Iter(impl => allImpls.Add(Tuple.Create(impl2Priority[impl.Name], impl.Name))); if (CommandLineOptions.Clo.Trace) { foreach (var tup in allImpls) { Console.WriteLine("Summary of {0}:", tup.Item2); Console.WriteLine("{0}", impl2Summary[tup.Item2]); } Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2")); Console.WriteLine("Number of prover queries = " + numProverQueries); } ProduceWitness(copy); prover.Close(); CommandLineOptions.Clo.TheProverFactory.Close(); } public HashSet GetPredicates() { var ret = new HashSet(); prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1); foreach (var tup in impl2Summary) { 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(); CommandLineOptions.Clo.TheProverFactory.Close(); return ret; } // Obtain the summary expression for a procedure: used programmatically by clients // of AbstractHoudini public Expr GetSummary(Program program, Procedure proc) { if (!impl2Summary.ContainsKey(proc.Name)) return Expr.True; var vars = new Dictionary(); foreach (var g in program.GlobalVariables) vars.Add(g.Name, Expr.Ident(g)); foreach (var v in proc.InParams.OfType()) vars.Add(v.Name, Expr.Ident(v)); foreach (var v in proc.OutParams.OfType()) vars.Add(v.Name, Expr.Ident(v)); return impl2Summary[proc.Name].GetSummaryExpr( v => { if (vars.ContainsKey(v)) return vars[v]; else return null; }, v => { if (vars.ContainsKey(v)) return new OldExpr(Token.NoToken, vars[v]); else return null; }); } public ISummaryElement GetSummaryLowLevel(Procedure proc) { if (!impl2Summary.ContainsKey(proc.Name)) return null; return impl2Summary[proc.Name]; } // Produce a witness that proves that the inferred annotations are correct private void ProduceWitness(Dictionary copy) { if (WitnessFile == null) return; foreach (var proc in program.Procedures) { var nensures = new List(); proc.Ensures.OfType() .Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") && !QKeyValue.FindBoolAttribute(ens.Attributes, "pre") && !QKeyValue.FindBoolAttribute(ens.Attributes, "post") && QKeyValue.FindStringAttribute(ens.Attributes, "pre") == null && QKeyValue.FindStringAttribute(ens.Attributes, "post") == null) .Iter(ens => nensures.Add(ens)); foreach (Ensures en in nensures) en.Attributes = removeAttr("InlineAssume", en.Attributes); proc.Ensures = nensures; } var decls = new List(copy.Values); decls.AddRange(program.TopLevelDeclarations.Where(decl => !(decl is Implementation))); program.TopLevelDeclarations = decls; var name2Proc = new Dictionary(); foreach (var proc in program.Procedures) { name2Proc.Add(proc.Name, proc); if (impl2Summary.ContainsKey(proc.Name)) { var ens = new Ensures(false, impl2Summary[proc.Name].GetSummaryExpr( new Func(s => null), new Func(s => null))); ens.Attributes = new QKeyValue(Token.NoToken, "inferred", new List(), ens.Attributes); proc.Ensures.Add(ens); } } using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false)) { program.Emit(wt); } // Replace SummaryPreds with their definition foreach (var impl in program.Implementations) { foreach (var blk in impl.Blocks) { foreach (var cmd in blk.Cmds.OfType()) { var expr = cmd.Expr as NAryExpr; if (expr == null) continue; var op = expr.Fun as FunctionCall; if (op == null || !op.FunctionName.EndsWith(summaryPredSuffix)) continue; var calleeName = op.FunctionName.Substring(0, op.FunctionName.Length - summaryPredSuffix.Length); if (!impl2Summary.ContainsKey(calleeName)) continue; var callee = name2Impl[calleeName]; // variable order: globals, ins, outs, modifies var forold = new Dictionary(); var always = new Dictionary(); int i = 0; foreach (var g in program.GlobalVariables) { forold.Add(g.Name, expr.Args[i]); always.Add(g.Name, expr.Args[i]); i++; } foreach (var v in callee.InParams.OfType()) { always.Add(v.Name, expr.Args[i]); i++; } foreach (var v in callee.OutParams.OfType()) { always.Add(v.Name, expr.Args[i]); i++; } foreach (var ie in name2Proc[calleeName].Modifies.OfType()) { always[ie.Name] = expr.Args[i]; i++; } cmd.Expr = impl2Summary[calleeName].GetSummaryExpr( v => { if (always.ContainsKey(v)) return always[v]; else return null; }, v => { if (forold.ContainsKey(v)) return forold[v]; else return null; }); } } } using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false)) { program.Emit(wt); } if (CommandLineOptions.Clo.Trace) Console.WriteLine("Witness written to {0}", WitnessFile); } private QKeyValue removeAttr(string key, QKeyValue attr) { if (attr == null) return attr; if (attr.Key == key) return removeAttr(key, attr.Next); attr.Next = removeAttr(key, attr.Next); return attr; } private void Inline() { if (CommandLineOptions.Clo.InlineDepth < 0) return; var callGraph = BuildCallGraph(); 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 oldCallGraph = callGraph; callGraph = new Graph(); foreach (Implementation impl in oldCallGraph.Nodes) { callGraph.AddSource(impl); } foreach (Tuple 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 newNodes = new List(); foreach (Implementation succ in callGraph.Successors(impl)) { newNodes.AddRange(oldCallGraph.Successors(succ)); } foreach (Implementation newNode in newNodes) { callGraph.AddEdge(impl, newNode); } } count--; } } private Graph BuildCallGraph() { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); foreach (var proc in program.Procedures) { procToImpls[proc] = new HashSet(); } foreach (var impl in program.Implementations) { if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } foreach (var impl in program.Implementations) { if (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; } private bool ProcessImpl(Implementation impl) { var ret = false; var gen = prover.VCExprGen; // construct summaries var env = VCExpressionGenerator.True; foreach (var tup in impl2CalleeSummaries[impl.Name]) { // Not Bilateral: then reject self predicates if (UseBilateralAlgo == false && tup.Item1 == impl.Name) continue; // Bilateral: only reject self summary if (UseBilateralAlgo == true && tup.Item1 == impl.Name && tup.Item2) continue; var calleeSummary = impl2Summary[tup.Item1].GetSummaryExpr( GetVarMapping(name2Impl[tup.Item1], tup.Item4), prover.VCExprGen); env = gen.AndSimp(env, gen.Eq(tup.Item3, calleeSummary)); } var prev = impl2Summary[impl.Name].Copy(); var upper = impl2Summary[impl.Name].GetTrueSummary(program, impl); var sw = new Stopwatch(); sw.Start(); var lowerTime = TimeSpan.Zero; while(true) { var usedLower = true; var query = impl2Summary[impl.Name]; sw.Restart(); // construct self summaries var summaryExpr = VCExpressionGenerator.True; foreach (var tup in impl2CalleeSummaries[impl.Name]) { if (UseBilateralAlgo == false && tup.Item1 != impl.Name) continue; if (UseBilateralAlgo == true && (tup.Item1 != impl.Name || !tup.Item2)) continue; if (UseBilateralAlgo) { query = query.AbstractConsequence(upper); if (query == null) query = impl2Summary[tup.Item1]; else usedLower = false; } var ts = query.GetSummaryExpr( GetVarMapping(name2Impl[tup.Item1], tup.Item4), prover.VCExprGen); summaryExpr = gen.AndSimp(summaryExpr, gen.Eq(tup.Item3, ts)); } //Console.WriteLine("Trying summary for {0}: {1}", impl.Name, summaryExpr); reporter.model = null; var vc = gen.AndSimp(env, summaryExpr); vc = gen.Implies(vc, impl2VC[impl.Name]); //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) { if (CommandLineOptions.Clo.Trace) Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); ret = prev.IsEqual(upper) ? false : true; impl2Summary[impl.Name] = upper; break; } else { if (CommandLineOptions.Clo.Trace) Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); var tt = impl2Summary[impl.Name].GetTrueSummary(program, impl); ret = prev.IsEqual(tt) ? false : true; ; impl2Summary[impl.Name] = tt; break; } } var start = DateTime.Now; //prover.Push(); //prover.Assert(gen.Not(vc), true); //prover.FlushAxiomsToTheoremProver(); //prover.Check(); //ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter); //prover.Pop(); prover.BeginCheck(impl.Name, vc, reporter); ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter); var inc = (DateTime.Now - start); proverTime += inc; numProverQueries++; sw.Stop(); if (usedLower) lowerTime += sw.Elapsed; if(CommandLineOptions.Clo.Trace) Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString()); if (UseBilateralAlgo) { if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory) { if(CommandLineOptions.Clo.Trace) Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); ret = prev.IsEqual(upper) ? false : true; impl2Summary[impl.Name] = upper; break; } if (reporter.model == null && usedLower) break; if (reporter.model == null) { upper.Meet(query); } else { var state = CollectState(impl); impl2Summary[impl.Name].Join(state, reporter.model); ret = true; } } else { if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory) { if (CommandLineOptions.Clo.Trace) Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); var tt = impl2Summary[impl.Name].GetTrueSummary(program, impl); ret = prev.IsEqual(tt) ? false : true; ; impl2Summary[impl.Name] = tt; break; } if (reporter.model == null) break; //reporter.model.Write(Console.Out); var state = CollectState(impl); impl2Summary[impl.Name].Join(state, reporter.model); ret = true; } } return ret; } private Dictionary GetVarMapping(Implementation impl, VCExprNAry summaryPred) { var ret = new Dictionary(); var cnt = 0; foreach (var g in program.GlobalVariables) { ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]); cnt++; } foreach (var v in impl.InParams.OfType().Concat( impl.OutParams.OfType().Concat( impl.Proc.Modifies.OfType().Select(ie => ie.Decl)))) { ret.Add(v.Name, summaryPred[cnt]); cnt++; } // Fill up values of globals that are not modified cnt = 0; foreach (var g in program.GlobalVariables) { if (ret.ContainsKey(g.Name)) { cnt++; continue; } ret.Add(string.Format("{0}", g.Name), summaryPred[cnt]); cnt++; } // Constants foreach (var c in program.Constants) { var value = prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c)); ret.Add(string.Format("{0}", c.Name), value); ret.Add(string.Format("old({0})", c.Name), value); } return ret; } private Dictionary CollectState(Implementation impl) { var ret = new Dictionary(); var model = reporter.model; var implVars = impl2EndStateVars[impl.Name]; var cnt = 0; foreach (var g in program.GlobalVariables) { ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model)); cnt++; } foreach (var v in impl.InParams.OfType().Concat( impl.OutParams.OfType().Concat( impl.Proc.Modifies.OfType().Select(ie => ie.Decl)))) { ret.Add(v.Name, getValue(implVars[cnt], model)); cnt++; } // Fill up values of globals that are not modified cnt = 0; foreach (var g in program.GlobalVariables) { if (ret.ContainsKey(g.Name)) { cnt++; continue; } ret.Add(string.Format("{0}", g.Name), getValue(implVars[cnt], model)); cnt++; } // Constants foreach (var c in program.Constants) { try { var value = getValue(prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c)), model); ret.Add(string.Format("{0}", c.Name), value); ret.Add(string.Format("old({0})", c.Name), value); } catch (Exception) { // constant not assigned a value: add a default value Model.Element value = null; if (c.TypedIdent.Type.IsInt) value = model.MkIntElement(0); else if (c.TypedIdent.Type.IsBool) value = model.MkElement("false"); ret.Add(string.Format("{0}", c.Name), value); ret.Add(string.Format("old({0})", c.Name), value); } } 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 { Debug.Assert(false); return null; } } private void attachEnsures(Implementation impl) { List functionInterfaceVars = new List(); foreach (Variable v in vcgen.program.GlobalVariables) { functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true)); } foreach (Variable v in impl.InParams) { functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true)); } foreach (Variable v in impl.OutParams) { functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true)); } foreach (IdentifierExpr e in impl.Proc.Modifies) { if (e.Decl == null) continue; functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true)); } Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false); var function = new Function(Token.NoToken, impl.Name + summaryPredSuffix, functionInterfaceVars, returnVar); prover.Context.DeclareFunction(function, ""); List exprs = new List(); foreach (Variable v in vcgen.program.GlobalVariables) { Contract.Assert(v != null); exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); } foreach (Variable v in impl.Proc.InParams) { Contract.Assert(v != null); exprs.Add(new IdentifierExpr(Token.NoToken, v)); } foreach (Variable v in impl.Proc.OutParams) { Contract.Assert(v != null); exprs.Add(new IdentifierExpr(Token.NoToken, v)); } foreach (IdentifierExpr ie in impl.Proc.Modifies) { Contract.Assert(ie != null); if (ie.Decl == null) continue; exprs.Add(ie); } Expr postExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs); impl.Proc.Ensures.Add( new Ensures(Token.NoToken, false, postExpr, "", new QKeyValue(Token.NoToken, "ah", new List(), null))); } private void GenVC(Implementation impl) { ModelViewInfo mvInfo; Dictionary label2absy; if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Generating VC of {0}", impl.Name); } vcgen.ConvertCFG2DAG(impl); vcgen.PassifyImpl(impl, out mvInfo); var gen = prover.VCExprGen; var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context); // Find the assert impl2EndStateVars.Add(impl.Name, new List()); var found = false; var assertId = -1; foreach (var blk in impl.Blocks) { foreach (var cmd in blk.Cmds.OfType()) { if (SimpleUtil.isAssertTrue(cmd)) continue; var nary = cmd.Expr as NAryExpr; if (nary == null) continue; var pred = nary.Fun as FunctionCall; if (pred == null || pred.FunctionName != (impl.Name + (AbstractHoudini.summaryPredSuffix))) continue; Debug.Assert(!found); found = true; assertId = cmd.UniqueId; //Console.WriteLine("assert cmd id: {0}", cmd.UniqueId); nary.Args.OfType() .Iter(expr => impl2EndStateVars[impl.Name].Add(prover.Context.BoogieExprTranslator.Translate(expr))); } } // It is possible that no assert is found in the procedure. It happens when the // procedure doesn't return. //Debug.Assert(found); // Grab summary predicates var visitor = new FindSummaryPred(prover.VCExprGen, assertId); vcexpr = visitor.Mutate(vcexpr, true); // Create a macro so that the VC can sit with the theorem prover Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List(), 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)); //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr); // check sanity: only one predicate for self-summary // (There may be none when the procedure doesn't return) Debug.Assert(visitor.summaryPreds.Count(tup => tup.Item2) <= 1); impl2CalleeSummaries.Add(impl.Name, new List>()); visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup)); } } public interface ISummaryElement { ISummaryElement Copy(); ISummaryElement GetFlaseSummary(Program program, Implementation impl); void Join(Dictionary state, Model model); VCExpr GetSummaryExpr(Dictionary incarnations, VCExpressionGenerator gen); Expr GetSummaryExpr(Func always, Func forold); // For Bilateral ISummaryElement GetTrueSummary(Program program, Implementation impl); void Meet(ISummaryElement other); bool IsEqual(ISummaryElement other); ISummaryElement AbstractConsequence(ISummaryElement upper); } public class ConstantVal : ISummaryElement { Program program; Implementation impl; // var -> const set Dictionary> val; // set of vars HashSet vars; public static readonly int MAX = 3; public ConstantVal() { // this is just a place holder val = new Dictionary>(); vars = new HashSet(); } private ConstantVal(Program program, Implementation impl) { this.program = program; this.impl = impl; this.val = new Dictionary>(); vars = new HashSet(); impl.Proc.Modifies .OfType() .Select(ie => ie.Decl) .Where(v => v.TypedIdent.Type.IsInt) .Iter(v => vars.Add(v)); impl.OutParams.OfType() .Where(v => v.TypedIdent.Type.IsInt) .Iter(v => vars.Add(v)); vars.Iter(v => val.Add(v.Name, null)); } public void Join(Dictionary state, Model model) { foreach (var vv in vars) { var v = vv.Name; var newv = state[v].AsInt(); var oldv = val[v]; if (oldv == null) { val[v] = new HashSet(); val[v].Add(newv); } else if(oldv.Count > 0) { val[v].Add(newv); if (val[v].Count > MAX) val[v] = new HashSet(); } } } public VCExpr GetSummaryExpr(Dictionary incarnations, VCExpressionGenerator gen) { VCExpr ret = VCExpressionGenerator.True; if (val.Values.Any(v => v == null)) return VCExpressionGenerator.False; foreach (var v in vars) { var consts = val[v.Name]; Debug.Assert(consts != null); if (consts.Count == 0) continue; var vexpr = VCExpressionGenerator.False; consts.Iter(c => vexpr = gen.OrSimp(vexpr, gen.Eq(incarnations[v.Name], gen.Integer(Microsoft.Basetypes.BigNum.FromInt(c))))); ret = gen.AndSimp(ret, vexpr); } return ret; } public override string ToString() { var ret = "true"; if (val.Values.Any(v => v == null)) return "false"; foreach (var v in vars) { var consts = val[v.Name]; Debug.Assert(consts != null); if (consts.Count == 0) continue; var vexpr = "false"; consts.Iter(c => vexpr = string.Format("{0} OR ({1} == {2})", vexpr, v.Name, c)); ret = string.Format("{0} AND ({1})", ret, vexpr); } return ret; } public ISummaryElement GetFlaseSummary(Program program, Implementation impl) { return new ConstantVal(program, impl); } #region ISummaryElement (Bilateral) Members public ISummaryElement GetTrueSummary(Program program, Implementation impl) { throw new NotImplementedException(); } public void Meet(ISummaryElement other) { throw new NotImplementedException(); } public bool IsEqual(ISummaryElement other) { throw new NotImplementedException(); } public ISummaryElement AbstractConsequence(ISummaryElement upper) { throw new NotImplementedException(); } #endregion #region ISummaryElement Members public Expr GetSummaryExpr(Func always, Func forold) { throw new NotImplementedException(); } #endregion #region ISummaryElement Members public ISummaryElement Copy() { throw new NotImplementedException(); } #endregion } public class NamedExpr { public string name; public Expr expr; public NamedExpr(string name, Expr expr) { this.name = name; this.expr = expr; } public NamedExpr(Expr expr) { this.name = null; this.expr = expr; } public override string ToString() { if (name != null) return name; return expr.ToString(); } } public class PredicateAbs : ISummaryElement { public static Dictionary> PrePreds { get; private set; } public static Dictionary> PosPrePreds { get; private set; } public static Dictionary> PostPreds { get; private set; } public static Dictionary, List> UpperCandidates; private static HashSet boolConstants; // {proc, pred-pair} -> polariry public static HashSet> unsatPrePredPairs; public static HashSet> unsatPostPredPairs; // Temporary: used during eval private static Model model = null; string procName; PredicateAbsDisjunct[] value; bool isFalse; public PredicateAbs(string procName) { this.procName = procName; isFalse = true; value = new PredicateAbsDisjunct[PostPreds[this.procName].Count]; for (int i = 0; i < PostPreds[this.procName].Count; i++) value[i] = null; } public static void Initialize(Program program) { PrePreds = new Dictionary>(); PostPreds = new Dictionary>(); PosPrePreds = new Dictionary>(); boolConstants = new HashSet(); UpperCandidates = new Dictionary, List>(); program.Constants .Where(c => c.TypedIdent.Type.IsBool) .Iter(c => boolConstants.Add(c.Name)); // Add template pre-post to all procedures var preT = new List(); var postT = new List(); var posPreT = new HashSet(); var tempP = new HashSet(); foreach (var proc in program.Procedures .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template"))) { tempP.Add(proc); foreach (var ens in proc.Ensures.OfType()) { var pos = QKeyValue.FindBoolAttribute(ens.Attributes, "positive"); if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre")) { preT.Add(new NamedExpr(null, ens.Condition)); if (pos) posPreT.Add(preT.Count - 1); } if (QKeyValue.FindBoolAttribute(ens.Attributes, "post")) postT.Add(new NamedExpr(null, ens.Condition)); var s = QKeyValue.FindStringAttribute(ens.Attributes, "pre"); if (s != null) { preT.Add(new NamedExpr(s, ens.Condition)); if (pos) posPreT.Add(preT.Count - 1); } s = QKeyValue.FindStringAttribute(ens.Attributes, "post"); if (s != null) postT.Add(new NamedExpr(s, ens.Condition)); } } program.RemoveTopLevelDeclarations(decl => tempP.Contains(decl)); var upperPreds = new Dictionary>(); foreach (var impl in program.Implementations) { PrePreds.Add(impl.Name, new List()); PostPreds.Add(impl.Name, new List()); PosPrePreds.Add(impl.Name, new HashSet()); // Add "false" as the first post predicate //PostPreds[impl.Name].Add(new NamedExpr(Expr.False)); preT.Iter(e => PrePreds[impl.Name].Add(e)); postT.Iter(e => PostPreds[impl.Name].Add(e)); PosPrePreds[impl.Name].UnionWith(posPreT); // Pick up per-procedure pre-post var nens = new List(); foreach (var ens in impl.Proc.Ensures.OfType()) { string s = null; var pos = QKeyValue.FindBoolAttribute(ens.Attributes, "positive"); if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre")) { PrePreds[impl.Name].Add(new NamedExpr(ens.Condition)); PosPrePreds[impl.Name].Add(PrePreds[impl.Name].Count - 1); } else if (QKeyValue.FindBoolAttribute(ens.Attributes, "post")) { PostPreds[impl.Name].Add(new NamedExpr(ens.Condition)); } else if ((s = QKeyValue.FindStringAttribute(ens.Attributes, "pre")) != null) { PrePreds[impl.Name].Add(new NamedExpr(s, ens.Condition)); PosPrePreds[impl.Name].Add(PrePreds[impl.Name].Count - 1); } else if ((s = QKeyValue.FindStringAttribute(ens.Attributes, "post")) != null) { PostPreds[impl.Name].Add(new NamedExpr(s, ens.Condition)); } else if (QKeyValue.FindBoolAttribute(ens.Attributes, "upper")) { var key = impl.Name; if (!upperPreds.ContainsKey(key)) upperPreds.Add(key, new List()); upperPreds[key].Add(ens.Condition); } else { nens.Add(ens); } } impl.Proc.Ensures = nens; } foreach (var tup in upperPreds) { var procName = tup.Key; var candidates = tup.Value; if (!candidates.Any()) continue; var strToPost = new Dictionary(); for (int i = 0; i < PostPreds[procName].Count; i++) { strToPost.Add(PostPreds[procName][i].expr.ToString(), i); } foreach (var expr in candidates) { if (strToPost.ContainsKey(expr.ToString())) { var key = Tuple.Create(procName, strToPost[expr.ToString()]); if (!UpperCandidates.ContainsKey(key)) UpperCandidates.Add(key, new List()); UpperCandidates[key].Add(new PredicateAbsDisjunct(true, procName)); } else { // Try parsing the expression as (pre-conjunct ==> post-pred) var parsed = ParseExpr(expr, procName); if (parsed != null && strToPost.ContainsKey(parsed.Item2.ToString())) { var key = Tuple.Create(procName, strToPost[parsed.Item2.ToString()]); if (!UpperCandidates.ContainsKey(key)) UpperCandidates.Add(key, new List()); UpperCandidates[key].Add(parsed.Item1); } } } } //Console.WriteLine("Running Abstract Houdini"); //PostPreds.Iter(expr => Console.WriteLine("\tPost: {0}", expr)); //PrePreds.Iter(expr => Console.WriteLine("\tPre: {0}", expr)); } // Try parsing the expression as (pre-conjunct ==> post-pred) private static Tuple ParseExpr(Expr expr, string procName) { Expr postExpr = null; Expr preExpr = null; // Decompose outer Implies var nexpr = expr as NAryExpr; if (nexpr != null && (nexpr.Fun is BinaryOperator) && (nexpr.Fun as BinaryOperator).Op == BinaryOperator.Opcode.Imp && (nexpr.Args.Count == 2)) { postExpr = nexpr.Args[1]; preExpr = nexpr.Args[0]; } else { if(CommandLineOptions.Clo.Trace) Console.WriteLine("Failed to parse {0} (ignoring)", expr); return null; } var atoms = DecomposeOuterAnd(preExpr); var pos = new HashSet(); var neg = new HashSet(); foreach (var atom in atoms) { var index = PrePreds[procName].FindIndex(ne => ne.expr.ToString() == atom.ToString()); if (index == -1) { index = PrePreds[procName].FindIndex(ne => Expr.Not(ne.expr).ToString() == atom.ToString()); if (index == -1) { if(CommandLineOptions.Clo.Trace) Console.WriteLine("Failed to parse {0} (ignoring)", atom); return null; } else { neg.Add(index); } } else { pos.Add(index); } } var conj = new PredicateAbsConjunct(pos, neg, procName); var conjls = new List(); conjls.Add(conj); return Tuple.Create(new PredicateAbsDisjunct(conjls, procName), postExpr); } // blah && blah ==> {blah, blah} static IEnumerable DecomposeOuterAnd(Expr expr) { var ret = new List(); var nexpr = expr as NAryExpr; if (nexpr == null || !(nexpr.Fun is BinaryOperator) || (nexpr.Fun as BinaryOperator).Op != BinaryOperator.Opcode.And) { ret.Add(expr); } else { foreach (Expr a in nexpr.Args) ret.AddRange(DecomposeOuterAnd(a)); } return ret; } private Model.Element Eval(Expr expr, Dictionary state) { if (expr is LiteralExpr) { return ToElem((expr as LiteralExpr).Val); } if (expr is IdentifierExpr) { return LookupVariable((expr as IdentifierExpr).Name, state, false); } if (expr is OldExpr) { var ide = (expr as OldExpr).Expr as IdentifierExpr; Debug.Assert(ide != null); return LookupVariable(ide.Name, state, true); } if (expr is NAryExpr) { var nary = expr as NAryExpr; if (nary.Fun is UnaryOperator) { return ToElem((nary.Fun as UnaryOperator).Evaluate(ToValue(Eval(nary.Args[0], state)))); } if (nary.Fun is BinaryOperator) { return ToElem((nary.Fun as BinaryOperator).Evaluate(ToValue(Eval(nary.Args[0], state)), ToValue(Eval(nary.Args[1], state)))); } if (nary.Fun is MapSelect && nary.Args.Count == 2) { var index = Eval(nary.Args[1], state); var map = Eval(nary.Args[0], state) as Model.Array; Debug.Assert(map != null, "Variable of map type must have an Array-typed value"); var ret = map.Value.TryEval(index as Model.Element); if (ret == null) ret = map.Value.Else; Debug.Assert(ret != null); return ret; } Debug.Assert(false, "No other op is handled"); } throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString())); } private Model.Element LookupVariable(string v, Dictionary state, bool tryOld) { if (tryOld) { var oldv = string.Format("old({0})", v); if (state.ContainsKey(oldv)) { return state[oldv]; } throw new AbsHoudiniInternalError("Cannot handle this case"); } if (state.ContainsKey(v)) { return state[v]; } /* if (boolConstants.Contains(v)) { // value of this constant is immaterial, return true return model.MkElement("true"); } */ throw new AbsHoudiniInternalError("Cannot handle this case"); } private static VCExpr ToVcVar(string v, Dictionary incarnations, bool tryOld) { if (tryOld) { var oldv = string.Format("old({0})", v); if (incarnations.ContainsKey(oldv)) { return incarnations[oldv]; } throw new AbsHoudiniInternalError("Cannot handle this case"); } if (incarnations.ContainsKey(v)) { return incarnations[v]; } throw new AbsHoudiniInternalError("Cannot handle this case"); } public static void FindUnsatPairs(VCExpressionGenerator gen, ProverInterface prover) { unsatPrePredPairs = new HashSet>(); unsatPostPredPairs = new HashSet>(); var cachePos = new HashSet>(); var cacheNeg = new HashSet>(); var record = new Action( (map, proc, e1, e2, p1, p2) => { var key = Tuple.Create(proc, e1, e2, p1, p2); if (map == PrePreds) unsatPrePredPairs.Add(key); else unsatPostPredPairs.Add(key); } ); var predMaps = new List>>(); predMaps.Add(PrePreds); predMaps.Add(PostPreds); foreach (var map in predMaps) { foreach (var proc in map.Keys) { for (int i = 0; i < 2 * map[proc].Count(); i++) { var p1 = (i % 2); // polarity var e1 = map[proc][i / 2].expr; if (p1 == 0) e1 = Expr.Not(e1); for (int j = 2 * ((i / 2) + 1); j < 2 * map[proc].Count(); j++) { var p2 = (j % 2); // polarity var e2 = map[proc][j / 2].expr; if (p2 == 0) e2 = Expr.Not(e2); var key = Tuple.Create(e1.ToString(), e2.ToString()); if (cachePos.Contains(key)) { record(map, proc, i / 2, j / 2, p1 == 1, p2 == 1); continue; } else if (cacheNeg.Contains(key)) { continue; } if (!CheckIfUnsat(e1, e2, gen, prover)) { cacheNeg.Add(key); continue; } cachePos.Add(key); record(map, proc, i / 2, j / 2, p1 == 1, p2 == 1); if (CommandLineOptions.Clo.Trace) Console.WriteLine("Proved UNSAT: {0} {1}", e1, e2); } } } } } // Is a ^ b UNSAT? private static bool CheckIfUnsat(Expr a, Expr b, VCExpressionGenerator gen, ProverInterface prover) { var gatherLitA = new GatherLiterals(); var gatherLitB = new GatherLiterals(); gatherLitA.Visit(a); gatherLitB.Visit(b); var seta = new HashSet(); var setb = new HashSet(); gatherLitA.literals.Iter(tup => seta.Add(tup.Item1)); gatherLitB.literals.Iter(tup => setb.Add(tup.Item1)); seta.IntersectWith(setb); if (!seta.Any()) return false; // Create fresh variables return CheckIfUnsat(Expr.And(a, b), gen, prover); } // Is a UNSAT? private static bool CheckIfUnsat(Expr a, VCExpressionGenerator gen, ProverInterface prover) { var gatherLitA = new GatherLiterals(); gatherLitA.Visit(a); // Create fresh variables var counter = 0; var incarnations = new Dictionary(); foreach (var literal in gatherLitA.literals) { if (incarnations.ContainsKey(literal.Item2.ToString())) continue; //if(!literal.Item1.TypedIdent.Type.IsInt && !literal.Item1.TypedIdent.Type.IsBool) var v = gen.Variable("UNSATCheck" + counter, literal.Item1.TypedIdent.Type); incarnations.Add(literal.Item2.ToString(), v); counter++; } var vc1 = ToVcExpr(a, incarnations, gen); var vc = gen.LabelPos("Temp", vc1); // check prover.AssertAxioms(); prover.Push(); prover.Assert(vc, true); prover.Check(); var outcome = prover.CheckOutcomeCore(new AbstractHoudiniErrorReporter()); prover.Pop(); if (outcome == ProverInterface.Outcome.Valid) return true; return false; } class GatherLiterals : ReadOnlyVisitor { public List> literals; bool inOld; public GatherLiterals() { literals = new List>(); inOld = false; } public override Expr VisitOldExpr(OldExpr node) { var prev = inOld; inOld = true; var ret = base.VisitOldExpr(node); inOld = prev; return ret; } public override Expr VisitIdentifierExpr(IdentifierExpr node) { if (inOld) literals.Add(Tuple.Create(node.Decl, new OldExpr(Token.NoToken, node) as Expr)); else literals.Add(Tuple.Create(node.Decl, node as Expr)); return node; } } private object ToValue(Model.Element elem) { if (elem is Model.Integer) { return Microsoft.Basetypes.BigNum.FromInt((elem as Model.Integer).AsInt()); } if (elem is Model.Boolean) { return (elem as Model.Boolean).Value; } if (elem is Model.DatatypeValue && (elem as Model.DatatypeValue).Arguments.Length == 1 && (elem as Model.DatatypeValue).ConstructorName == "-" && (elem as Model.DatatypeValue).Arguments[0] is Model.Integer) { // negative number as "-" @ int return Microsoft.Basetypes.BigNum.FromInt(-1 * ((elem as Model.DatatypeValue).Arguments[0] as Model.Integer).AsInt()); } throw new NotImplementedException("Cannot yet handle this Model.Element type"); } private Model.Element ToElem(object val) { if (val is bool || val is int || val is Basetypes.BigNum) return model.MkElement(val.ToString()); throw new NotImplementedException("Cannot yet handle this value type"); } // replace v by old(v) private static Expr MakeOld(Expr expr) { var substalways = new Substitution(v => new OldExpr(Token.NoToken, Expr.Ident(v))); var substold = new Substitution(v => Expr.Ident(v)); return Substituter.ApplyReplacingOldExprs(substalways, substold, expr); } private static Expr ToExpr(Expr expr, Func always, Func forold) { var substalways = new Substitution(v => { var ret = always(v.Name); if (ret != null) return ret; else return Expr.Ident(v); }); var substold = new Substitution(v => { var ret = forold(v.Name); if (ret != null) return ret; else return new OldExpr(Token.NoToken, Expr.Ident(v)); }); return Substituter.ApplyReplacingOldExprs(substalways, substold, expr); } private static VCExpr ToVcExpr(Expr expr, Dictionary incarnations, VCExpressionGenerator gen) { if (expr is LiteralExpr) { var val = (expr as LiteralExpr).Val; if (val is bool) { if ((bool)val) { return VCExpressionGenerator.True; } else { return VCExpressionGenerator.False; } } else if (val is Microsoft.Basetypes.BigNum) { return gen.Integer((Microsoft.Basetypes.BigNum)val); } throw new NotImplementedException("Cannot handle literals of this type"); } if (expr is IdentifierExpr) { return ToVcVar((expr as IdentifierExpr).Name, incarnations, false); } if (expr is OldExpr) { var ide = (expr as OldExpr).Expr as IdentifierExpr; Debug.Assert(ide != null); return ToVcVar(ide.Name, incarnations, true); } if (expr is NAryExpr) { var nary = expr as NAryExpr; if (nary.Fun is UnaryOperator) { if ((nary.Fun as UnaryOperator).Op == UnaryOperator.Opcode.Not) return gen.Not(ToVcExpr(nary.Args[0], incarnations, gen)); else if ((nary.Fun as UnaryOperator).Op == UnaryOperator.Opcode.Neg) return gen.Function(VCExpressionGenerator.SubIOp, gen.Integer(Basetypes.BigNum.FromInt(0)), ToVcExpr(nary.Args[0], incarnations, gen)); else Debug.Assert(false, "No other unary op is handled"); } if (nary.Fun is BinaryOperator) { return gen.Function(Translate(nary.Fun as BinaryOperator), ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen)); } if (nary.Fun is MapSelect && nary.Args.Count == 2) { return gen.Select(ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen)); } Debug.Assert(false, "No other op is handled"); } throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString())); } private static VCExprOp Translate(BinaryOperator op) { switch (op.Op) { case BinaryOperator.Opcode.Add: return VCExpressionGenerator.AddIOp; case BinaryOperator.Opcode.Sub: return VCExpressionGenerator.SubIOp; case BinaryOperator.Opcode.Mul: return VCExpressionGenerator.MulIOp; case BinaryOperator.Opcode.Div: return VCExpressionGenerator.DivIOp; case BinaryOperator.Opcode.Mod: return VCExpressionGenerator.ModOp; case BinaryOperator.Opcode.Eq: case BinaryOperator.Opcode.Iff: // we don't distinguish between equality and equivalence at this point return VCExpressionGenerator.EqOp; case BinaryOperator.Opcode.Neq: return VCExpressionGenerator.NeqOp; case BinaryOperator.Opcode.Lt: return VCExpressionGenerator.LtOp; case BinaryOperator.Opcode.Le: return VCExpressionGenerator.LeOp; case BinaryOperator.Opcode.Ge: return VCExpressionGenerator.GeOp; case BinaryOperator.Opcode.Gt: return VCExpressionGenerator.GtOp; case BinaryOperator.Opcode.Imp: return VCExpressionGenerator.ImpliesOp; case BinaryOperator.Opcode.And: return VCExpressionGenerator.AndOp; case BinaryOperator.Opcode.Or: return VCExpressionGenerator.OrOp; case BinaryOperator.Opcode.Subtype: return VCExpressionGenerator.SubtypeOp; default: Contract.Assert(false); throw new NotImplementedException(); } } // If "false" is a post-predicate, then remove its "pre" constraint from all others, whenever possible public void Simplify() { // find "false" var findex = PostPreds[procName].FindIndex(ne => (ne.expr is LiteralExpr) && (ne.expr as LiteralExpr).IsFalse); if (findex < 0) return; if (value[findex].isTrue) { // procedure doesn't return for (int i = 0; i < value.Length; i++) if (i != findex) value[i] = new PredicateAbsDisjunct(false, procName); return; } if (value[findex].isFalse) return; for (int i = 0; i < value.Length; i++) if (i != findex) value[i].Subtract(value[findex]); } public HashSet GetPredicates(Program program, VCExpressionGenerator gen, ProverInterface prover) { var ret = new HashSet(); if (isFalse) return ret; Simplify(); // Find the free expressions var proc = program.Procedures.FirstOrDefault(p => p.Name == procName); Contract.Assert(proc != null); Expr freeSummary = Expr.True; foreach (var req in proc.Requires.OfType().Where(req => req.Free)) { freeSummary = Expr.And(freeSummary, MakeOld(req.Condition)); } foreach (var ens in proc.Ensures.OfType().Where(ens => ens.Free)) { freeSummary = Expr.And(freeSummary, ens.Condition); } for (int i = 0; i < PostPreds[procName].Count; i++) { if (value[i].isFalse) continue; if (PostPreds[procName][i].expr is LiteralExpr && (PostPreds[procName][i].expr as LiteralExpr).IsFalse) continue; if (value[i].isTrue) ret.Add(PostPreds[procName][i].expr.ToString()); else { foreach (var c in value[i].GetConjuncts()) { var s = Expr.Imp(c.ToExpr(j => PrePreds[procName][j].expr), PostPreds[procName][i].expr); if (CheckIfUnsat(Expr.And(freeSummary, Expr.Not(s)), gen, prover)) continue; ret.Add(s.ToString()); } } } return ret; } public override string ToString() { var ret = ""; if (isFalse) return "false"; var first = true; for(int i = 0; i < PostPreds[procName].Count; i++) { if(value[i].isFalse) continue; if(value[i].isTrue) ret += string.Format("{0}{1}", first ? "" : " && ", PostPreds[procName][i]); else ret += string.Format("{0}({1} ==> {2})", first ? "" : " && ", value[i], PostPreds[procName][i]); first = false; } if (ret == "") ret = "true"; return ret; } #region ISummaryElement Members public ISummaryElement Copy() { var ret = new PredicateAbs(procName); ret.isFalse = isFalse; ret.value = new PredicateAbsDisjunct[value.Length]; for (int i = 0; i < value.Length; i++) ret.value[i] = value[i]; return ret; } public ISummaryElement GetFlaseSummary(Program program, Implementation impl) { return new PredicateAbs(impl.Name); } public ISummaryElement GetTrueSummary(Program program, Implementation impl) { var ret = new PredicateAbs(impl.Name); ret.isFalse = false; for (int i = 0; i < PostPreds[this.procName].Count; i++) ret.value[i] = new PredicateAbsDisjunct(false, impl.Name); return ret; } public void Join(Dictionary state, Model model) { PredicateAbs.model = model; // Evaluate each predicate on the state var prePredsVal = new bool[PrePreds[procName].Count]; var postPredsVal = new bool[PostPreds[procName].Count]; var indexSeq = new List(); for (int i = 0; i < PrePreds[procName].Count; i++) indexSeq.Add(i); for (int i = 0; i < PrePreds[procName].Count; i++) { var v = ToValue(Eval(PrePreds[procName][i].expr, state)); Debug.Assert(v is bool); prePredsVal[i] = (bool)v; } for (int i = 0; i < PostPreds[procName].Count; i++) { var v = ToValue(Eval(PostPreds[procName][i].expr, state)); Debug.Assert(v is bool); postPredsVal[i] = (bool)v; } for (int i = 0; i < PostPreds[procName].Count; i++) { // No hope for this post pred? if (!isFalse && value[i].isFalse) continue; var newDisj = new PredicateAbsDisjunct(true, procName); if (!postPredsVal[i]) { newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j] && !PosPrePreds[procName].Contains(j)), procName); } if (isFalse) value[i] = newDisj; else value[i] = PredicateAbsDisjunct.And(value[i], newDisj); } /* // do beta(model) var that = new PredicateAbsDisjunct[PostPreds[procName].Count]; for (int i = 0; i < PostPreds[procName].Count; i++) { if (postPredsVal[i]) that[i] = new PredicateAbsDisjunct(true, procName); else if (i == 0) { Debug.Assert(PostPreds[procName][0].ToString() == "false"); var newDisj = new PredicateAbsDisjunct(true, procName); newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j]), procName); that[i] = newDisj; } else { // false that[i] = new PredicateAbsDisjunct(false, procName); } } // Do join for (int i = 0; i < PostPreds[procName].Count; i++) { if (isFalse) value[i] = that[i]; else { if (i == 0) value[i] = PredicateAbsDisjunct.And(value[i], that[i]); else { var c1 = PredicateAbsDisjunct.And(value[i], that[i]); var c2 = PredicateAbsDisjunct.And(value[i], that[0]); var c3 = PredicateAbsDisjunct.And(value[0], that[i]); value[i] = PredicateAbsDisjunct.Or(c1, c2); value[i] = PredicateAbsDisjunct.Or(value[i], c3); } } } */ isFalse = false; //Console.WriteLine("Result of Join: {0}", this.ToString()); } // Precondition: the upper guys are just {true/false/upper-candidate} ==> post-pred public void Meet(ISummaryElement iother) { var other = iother as PredicateAbs; if (isFalse) return; if (other.isFalse) { isFalse = true; for (int i = 0; i < PostPreds[this.procName].Count; i++) value[i] = null; return; } Debug.Assert(this.procName == other.procName); for (int i = 0; i < PostPreds[this.procName].Count; i++) { value[i] = PredicateAbsDisjunct.Or(value[i], other.value[i]); } } public bool IsEqual(ISummaryElement other) { var that = other as PredicateAbs; if (isFalse && that.isFalse) return true; if (isFalse || that.isFalse) return false; for (int i = 0; i < PostPreds[procName].Count; i++) { if (!PredicateAbsDisjunct.syntacticLessThan(value[i], that.value[i]) || !PredicateAbsDisjunct.syntacticLessThan(that.value[i], value[i])) return false; } return true; } // Precondition: the upper guys are just {true/false/upper-candidate} ==> post-pred // Postcondition: the returned value is also of this form (for just one post-pred) public ISummaryElement AbstractConsequence(ISummaryElement iupper) { var upper = iupper as PredicateAbs; for (int i = 0; i < PostPreds[this.procName].Count; i++) { if (upper.value[i].isTrue) continue; if (!UpperCandidates.ContainsKey(Tuple.Create(procName, i))) continue; foreach (var candidate in UpperCandidates[Tuple.Create(procName, i)]) { if (PredicateAbsDisjunct.syntacticLessThan(candidate, upper.value[i])) continue; if (!this.isFalse && !PredicateAbsDisjunct.syntacticLessThan(candidate, this.value[i])) continue; var ret = new PredicateAbs(this.procName); ret.isFalse = false; for (int j = 0; j < PostPreds[this.procName].Count; j++) ret.value[j] = new PredicateAbsDisjunct(false, this.procName); ret.value[i] = candidate; return ret; } } // Giveup: the abstract consequence is too difficult to compute return null; } public VCExpr GetSummaryExpr(Dictionary incarnations, VCExpressionGenerator gen) { if (isFalse) return VCExpressionGenerator.False; var ret = VCExpressionGenerator.True; for(int i = 0; i < PostPreds[procName].Count; i++) { ret = gen.AndSimp(ret, gen.ImpliesSimp(value[i].ToVcExpr(j => ToVcExpr(PrePreds[procName][j].expr, incarnations, gen), gen), ToVcExpr(PostPreds[procName][i].expr, incarnations, gen))); } return ret; } public Expr GetSummaryExpr(Func always, Func forold) { if (isFalse) return Expr.False; Expr ret = Expr.True; for (int i = 0; i < PostPreds[procName].Count; i++) { ret = Expr.And(ret, Expr.Imp(value[i].ToExpr(j => ToExpr(PrePreds[procName][j].expr, always, forold)), ToExpr(PostPreds[procName][i].expr, always, forold))); } return ret; } #endregion } public class PredicateAbsDisjunct { List conjuncts; string ProcName; public bool isTrue {get; private set;} public bool isFalse { get { if (isTrue) return false; return conjuncts.Count == 0; } } public PredicateAbsDisjunct(bool isTrue, string ProcName) { this.isTrue = isTrue; this.ProcName = ProcName; conjuncts = new List(); } public PredicateAbsDisjunct(List conjuncts, string ProcName) { isTrue = false; this.conjuncts = conjuncts; this.ProcName = ProcName; } // Disjunct of singleton conjuncts public PredicateAbsDisjunct(IEnumerable pos, IEnumerable neg, string ProcName) { this.ProcName = ProcName; conjuncts = new List(); isTrue = false; pos.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, true, ProcName))); neg.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, false, ProcName))); } // Does d1 describe a smaller set of states than d2? This is true when every conjunct of d1 // is smaller than some conjunct of d2 public static bool syntacticLessThan(PredicateAbsDisjunct d1, PredicateAbsDisjunct d2) { if (d2.isTrue) return true; if (d1.isTrue) return false; if (d1.isFalse) return true; if (d2.isFalse) return false; foreach (var c1 in d1.conjuncts) { if (d2.conjuncts.Any(c2 => PredicateAbsConjunct.syntacticLessThan(c1, c2))) continue; else return false; } return true; } public static PredicateAbsDisjunct And(PredicateAbsDisjunct v1, PredicateAbsDisjunct v2) { if (v1.isTrue) return v2; if (v2.isTrue) return v1; var result = new List(); foreach (var c1 in v1.conjuncts) { foreach (var c2 in v2.conjuncts) { var c = PredicateAbsConjunct.And(c1, c2); if (c.isFalse) continue; if (result.Any(cprime => c.implies(cprime))) continue; var tmp = new List(); tmp.Add(c); result.Where(cprime => !cprime.implies(c)).Iter(cprime => tmp.Add(cprime)); result = tmp; } } return new PredicateAbsDisjunct(result, v1.ProcName); } public static PredicateAbsDisjunct Or(PredicateAbsDisjunct v1, PredicateAbsDisjunct v2) { if (v1.isTrue) return v1; if (v2.isTrue) return v2; if (v1.isFalse) return v2; if (v2.isFalse) return v1; var result = new List(); v1.conjuncts.Iter(c => result.Add(c)); foreach (var c in v2.conjuncts) { if (result.Any(cprime => c.implies(cprime))) continue; var tmp = new List(); tmp.Add(c); result.Where(cprime => !cprime.implies(c)).Iter(cprime => tmp.Add(cprime)); result = tmp; } return new PredicateAbsDisjunct(result, v1.ProcName); } public VCExpr ToVcExpr(Func predToExpr, VCExpressionGenerator gen) { if (isTrue) return VCExpressionGenerator.True; var ret = VCExpressionGenerator.False; conjuncts.Iter(c => ret = gen.OrSimp(ret, c.ToVcExpr(predToExpr, gen))); return ret; } public Expr ToExpr(Func predToExpr) { if (isTrue) return Expr.True; Expr ret = Expr.False; conjuncts.Iter(c => ret = Expr.Or(ret, c.ToExpr(predToExpr))); return ret; } public override string ToString() { if(isTrue) return "true"; var ret = ""; var first = true; foreach (var c in conjuncts) { if (c.isFalse) continue; ret += string.Format("{0}{1}", first ? "" : " || ", c); first = false; } return ret; } public void Subtract(PredicateAbsDisjunct that) { var ncon = new List(); foreach (var c1 in conjuncts) { if (that.conjuncts.Any(c2 => c1.implies(c2))) continue; ncon.Add(c1); } conjuncts = ncon; } public IEnumerable GetConjuncts() { return conjuncts; } } public class PredicateAbsConjunct { static int ConjunctBound = 3; public bool isFalse { get; private set; } HashSet posPreds; HashSet negPreds; string ProcName; public static void Initialize(int bound) { ConjunctBound = bound; } private void Normalize() { if (posPreds.Intersect(negPreds).Any() || negPreds.Intersect(posPreds).Any() || (posPreds.Count + negPreds.Count > ConjunctBound)) { isFalse = true; posPreds = new HashSet(); negPreds = new HashSet(); } } // Do this step only once in a while? private void StrongNormalize() { if (isFalse) return; var candidates = new List>(); posPreds.Iter(p => candidates.Add(Tuple.Create(p, true))); negPreds.Iter(p => candidates.Add(Tuple.Create(p, false))); var drop = new HashSet(); for (int i = 0; i < candidates.Count; i++) { for (int j = 0; j < candidates.Count; j++) { if (i == j) continue; var key = Tuple.Create(ProcName, candidates[i].Item1, candidates[j].Item1, candidates[i].Item2, candidates[j].Item2); if (PredicateAbs.unsatPrePredPairs.Contains(key)) { isFalse = true; posPreds = new HashSet(); negPreds = new HashSet(); return; } key = Tuple.Create(ProcName, candidates[i].Item1, candidates[j].Item1, candidates[i].Item2, !candidates[j].Item2); if (PredicateAbs.unsatPrePredPairs.Contains(key)) drop.Add(candidates[j].Item1); } } posPreds.ExceptWith(drop); negPreds.ExceptWith(drop); } public PredicateAbsConjunct(bool isFalse, string ProcName) { posPreds = new HashSet(); negPreds = new HashSet(); this.isFalse = isFalse; this.ProcName = ProcName; } // do we know that c1 is surely less than or equal to c2? That is, c1 describes a smaller // concretization. We check that c2 is a sub-conjunct of c1 public static bool syntacticLessThan(PredicateAbsConjunct c1, PredicateAbsConjunct c2) { if (c1.isFalse) return true; if (c2.isFalse) return false; return (c2.posPreds.IsSubsetOf(c1.posPreds) && c2.negPreds.IsSubsetOf(c1.negPreds)); } public static PredicateAbsConjunct Singleton(int v, bool isPositive, string ProcName) { if (isPositive) return new PredicateAbsConjunct(new int[] { v }, new HashSet(), ProcName); else return new PredicateAbsConjunct(new HashSet(), new int[] { v }, ProcName); } public PredicateAbsConjunct(IEnumerable pos, IEnumerable neg, string ProcName) { isFalse = false; posPreds = new HashSet(pos); negPreds = new HashSet(neg); this.ProcName = ProcName; Normalize(); } public static PredicateAbsConjunct And(PredicateAbsConjunct v1, PredicateAbsConjunct v2) { if (v1.isFalse || v2.isFalse) return new PredicateAbsConjunct(true, v1.ProcName); var ret = new PredicateAbsConjunct(v1.posPreds.Union(v2.posPreds), v1.negPreds.Union(v2.negPreds), v1.ProcName); ret.StrongNormalize(); return ret; } public bool implies(PredicateAbsConjunct v) { if (isFalse) return true; if (v.isFalse) return false; return (posPreds.IsSupersetOf(v.posPreds) && negPreds.IsSupersetOf(v.negPreds)); } public VCExpr ToVcExpr(Func predToExpr, VCExpressionGenerator gen) { if (isFalse) return VCExpressionGenerator.False; var ret = VCExpressionGenerator.True; posPreds.Iter(p => ret = gen.AndSimp(ret, predToExpr(p))); negPreds.Iter(p => ret = gen.AndSimp(ret, gen.Not(predToExpr(p)))); return ret; } public Expr ToExpr(Func predToExpr) { if (isFalse) return Expr.False; Expr ret = Expr.True; 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; } public override string ToString() { if (isFalse) return "false"; var ret = ""; var first = true; foreach (var p in posPreds) { ret += string.Format("{0}{1}", first ? "" : " && ", PredicateAbs.PrePreds[ProcName][p]); first = false; } foreach (var p in negPreds) { ret += string.Format("{0}!{1}", first ? "" : " && ", PredicateAbs.PrePreds[ProcName][p]); first = false; } return ret; } } class FindSummaryPred : MutatingVCExprVisitor { public List> summaryPreds; int assertId; private static int CounterId = 0; public FindSummaryPred(VCExpressionGenerator gen, int assertId) : base(gen) { summaryPreds = new List>(); this.assertId = assertId; } protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List/*!*/ newSubExprs, // has any of the subexpressions changed? bool changed, bool arg) { Contract.Ensures(Contract.Result() != 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) { var lop = retnary.Op as VCExprLabelOp; if (lop == null) return ret; if (lop.pos) return ret; if (!lop.label.Equals("@" + assertId.ToString())) return ret; //var subexpr = retnary[0] as VCExprNAry; //if (subexpr == null) return ret; //op = subexpr.Op as VCExprBoogieFunctionOp; //if (op == null) return ret; var subexpr = retnary[0] as VCExprVar; if (subexpr == null) return ret; if (!subexpr.Name.StartsWith("AbstractHoudiniControl")) return ret; for (int i = 0; i < summaryPreds.Count; i++) { if (summaryPreds[i].Item3 == subexpr) summaryPreds[i] = Tuple.Create(summaryPreds[i].Item1, true, summaryPreds[i].Item3, summaryPreds[i].Item4); } return ret; } string calleeName = op.Func.Name; if (!calleeName.EndsWith(AbstractHoudini.summaryPredSuffix)) return ret; var controlConst = Gen.Variable("AbstractHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool); CounterId++; summaryPreds.Add(Tuple.Create(calleeName.Substring(0, calleeName.Length - AbstractHoudini.summaryPredSuffix.Length), false, controlConst, retnary)); return controlConst; //return ret; } } class FindExistentialFunctions : MutatingVCExprVisitor { public List> funcCalls; private HashSet existentialFunctions; private static int CounterId = 0; public FindExistentialFunctions(VCExpressionGenerator gen, HashSet existentialFunctions) : base(gen) { funcCalls = new List>(); this.existentialFunctions = existentialFunctions; } protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List/*!*/ newSubExprs, // has any of the subexpressions changed? bool changed, bool arg) { Contract.Ensures(Contract.Result() != 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; public AbstractHoudiniErrorReporter() { model = null; } public override void OnModel(IList labels, Model model, ProverInterface.Outcome proverOutcome) { Debug.Assert(model != null); if(CommandLineOptions.Clo.PrintErrorModel >= 1) model.Write(Console.Out); this.model = model; } } public class AbsHoudiniInternalError : System.ApplicationException { public AbsHoudiniInternalError(string msg) : base(msg) { } }; public class SimpleUtil { // Constructs a mapping from procedure names to the implementation public static Dictionary nameImplMapping(Program p) { var m = new Dictionary(); foreach (var impl in p.Implementations) { m.Add(impl.Name, impl); } return m; } // is "assert true"? public static bool isAssertTrue(Cmd cmd) { var acmd = cmd as AssertCmd; if (acmd == null) return false; var le = acmd.Expr as LiteralExpr; if (le == null) return false; if (le.IsTrue) return true; return false; } } }