From 44542347498f3dfed6cffb3c17988dbfeb9e93ea Mon Sep 17 00:00:00 2001 From: akashlal Date: Fri, 28 Dec 2012 15:33:34 +0530 Subject: Some more changes to AbsHoudini --- Source/Houdini/AbstractHoudini.cs | 418 ++++++++++++++++++++++++++++++++------ 1 file changed, 357 insertions(+), 61 deletions(-) (limited to 'Source/Houdini/AbstractHoudini.cs') diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index f62e0305..2b166743 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -55,8 +55,12 @@ namespace Microsoft.Boogie.Houdini { this.impl2Summary = new Dictionary(); this.name2Impl = SimpleUtil.nameImplMapping(program); + if (CommandLineOptions.Clo.ProverKillTime > 0) + CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); + this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime); + this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1); + this.reporter = new AbstractHoudiniErrorReporter(); this.proverTime = TimeSpan.Zero; @@ -68,8 +72,8 @@ namespace Microsoft.Boogie.Houdini { public void computeSummaries(ISummaryElement summaryClass) { - //PredicateAbs.FindUnsatPairs(prover.VCExprGen, prover); - //throw new AbsHoudiniInternalError("Done"); + // TODO: move this some place else + PredicateAbs.FindUnsatPairs(prover.VCExprGen, prover); this.summaryClass = summaryClass; @@ -187,7 +191,7 @@ namespace Microsoft.Boogie.Houdini { // Obtain the summary expression for a procedure: used programmatically by clients // of AbstractHoudini - private Expr GetSummary(Program program, Procedure proc) + public Expr GetSummary(Program program, Procedure proc) { if (!impl2Summary.ContainsKey(proc.Name)) return Expr.True; @@ -428,6 +432,7 @@ namespace Microsoft.Boogie.Houdini { { var ret = false; var gen = prover.VCExprGen; + var startTime = DateTime.Now; // construct summaries var env = VCExpressionGenerator.True; @@ -484,7 +489,28 @@ namespace Microsoft.Boogie.Houdini { //Console.WriteLine("Checking: {0}", vc); if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Verifying {0}: {1}", impl.Name, query); + Console.WriteLine("Verifying {0} ({1}): {2}", impl.Name, usedLower ? "lower" : "ac", query); + } + + if ((DateTime.Now - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime && + CommandLineOptions.Clo.ProverKillTime > 0) + { + if (UseBilateralAlgo) + { + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); + impl2Summary[impl.Name] = upper; + ret = true; + break; + } + else + { + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name); + impl2Summary[impl.Name] = impl2Summary[impl.Name].GetTrueSummary(program, impl); + ret = true; + break; + } } var start = DateTime.Now; @@ -989,7 +1015,12 @@ namespace Microsoft.Boogie.Houdini { { public static Dictionary> PrePreds { 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; @@ -1010,6 +1041,7 @@ namespace Microsoft.Boogie.Houdini { PrePreds = new Dictionary>(); PostPreds = new Dictionary>(); boolConstants = new HashSet(); + UpperCandidates = new Dictionary, List>(); program.TopLevelDeclarations.OfType() .Where(c => c.TypedIdent.Type.IsBool) @@ -1042,6 +1074,7 @@ namespace Microsoft.Boogie.Houdini { } program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl)); + var upperPreds = new Dictionary>(); foreach (var impl in program.TopLevelDeclarations.OfType()) { @@ -1072,6 +1105,13 @@ namespace Microsoft.Boogie.Houdini { { 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); @@ -1079,12 +1119,124 @@ namespace Microsoft.Boogie.Houdini { } 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.Length == 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 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) @@ -1181,16 +1333,65 @@ namespace Microsoft.Boogie.Houdini { public static void FindUnsatPairs(VCExpressionGenerator gen, ProverInterface prover) { - for (int i = 0; i < PrePreds["main"].Count(); i++) + 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) { - for (int j = i + 1; j < PrePreds["main"].Count(); j++) + foreach (var proc in map.Keys) { - if (!CheckIfUnsat(PrePreds["main"][i].expr, PrePreds["main"][j].expr, gen, prover)) - continue; - Console.WriteLine("Proved UNSAT: {0} {1}", PrePreds["main"][i].expr, PrePreds["main"][j].expr); + 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? @@ -1202,6 +1403,13 @@ namespace Microsoft.Boogie.Houdini { 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 var counter = 0; var incarnations = new Dictionary(); @@ -1221,7 +1429,7 @@ namespace Microsoft.Boogie.Houdini { var vc = gen.LabelPos("Temp", gen.And(vc1, vc2)); // check - prover.FlushAxiomsToTheoremProver(); + prover.AssertAxioms(); prover.Push(); prover.Assert(vc, true); prover.Check(); @@ -1412,7 +1620,7 @@ namespace Microsoft.Boogie.Houdini { var ret = ""; if (isFalse) return "false"; var first = true; - PredicateAbsConjunct.tempProcName = procName; + for(int i = 0; i < PostPreds[procName].Count; i++) { if(value[i].isFalse) continue; @@ -1440,7 +1648,7 @@ namespace Microsoft.Boogie.Houdini { { 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); + for (int i = 0; i < PostPreds[this.procName].Count; i++) ret.value[i] = new PredicateAbsDisjunct(false, impl.Name); return ret; } @@ -1475,10 +1683,10 @@ namespace Microsoft.Boogie.Houdini { // No hope for this post pred? if (!isFalse && value[i].isFalse) continue; - var newDisj = new PredicateAbsDisjunct(true); + var newDisj = new PredicateAbsDisjunct(true, procName); if (!postPredsVal[i]) { - newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j])); + newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j]), procName); } if (isFalse) @@ -1492,7 +1700,7 @@ namespace Microsoft.Boogie.Houdini { //Console.WriteLine("Result of Join: {0}", this.ToString()); } - // Precondition: the upper guys are just {true/false} ==> post-pred + // Precondition: the upper guys are just {true/false/upper-candidate} ==> post-pred public void Meet(ISummaryElement iother) { var other = iother as PredicateAbs; @@ -1507,14 +1715,7 @@ namespace Microsoft.Boogie.Houdini { for (int i = 0; i < PostPreds[this.procName].Count; i++) { - // check precondition - if (!value[i].isTrue && !value[i].isFalse) - throw new NotImplementedException("Invalid upper domain element"); - if (!other.value[i].isTrue && !other.value[i].isFalse) - throw new NotImplementedException("Invalid upper domain element"); - - if (value[i].isFalse && other.value[i].isTrue) - value[i] = new PredicateAbsDisjunct(true); + value[i] = PredicateAbsDisjunct.Or(value[i], other.value[i]); } } @@ -1523,33 +1724,33 @@ namespace Microsoft.Boogie.Houdini { return false; } - // Precondition: the upper guys are just {true/false} ==> post-pred - // Postcondition: the returned value is also of this form + // 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++) { - // check precondition - if (!upper.value[i].isTrue && !upper.value[i].isFalse) - throw new NotImplementedException("Invalid upper domain element"); + if (upper.value[i].isTrue) continue; + if (!UpperCandidates.ContainsKey(Tuple.Create(procName, i))) continue; - if (upper.value[i].isTrue) - 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); + 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; - ret.value[i] = new PredicateAbsDisjunct(true); + 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); - // check that this \lesseq ret - if (isFalse) return ret; + ret.value[i] = candidate; - if (value[i].isTrue) return ret; + } } // Giveup: the abstract consequence is too difficult to compute @@ -1589,9 +1790,10 @@ namespace Microsoft.Boogie.Houdini { #endregion } - class PredicateAbsDisjunct + public class PredicateAbsDisjunct { List conjuncts; + string ProcName; public bool isTrue {get; private set;} public bool isFalse { @@ -1602,25 +1804,47 @@ namespace Microsoft.Boogie.Houdini { } } - public PredicateAbsDisjunct(bool isTrue) + public PredicateAbsDisjunct(bool isTrue, string ProcName) { this.isTrue = isTrue; + this.ProcName = ProcName; conjuncts = new List(); } - private PredicateAbsDisjunct(List conjuncts) + public PredicateAbsDisjunct(List conjuncts, string ProcName) { isTrue = false; this.conjuncts = conjuncts; + this.ProcName = ProcName; } // Disjunct of singleton conjuncts - public PredicateAbsDisjunct(IEnumerable pos, IEnumerable neg) + 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))); - neg.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, 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) @@ -1644,7 +1868,29 @@ namespace Microsoft.Boogie.Houdini { } } - return new PredicateAbsDisjunct(result); + 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) @@ -1679,14 +1925,14 @@ namespace Microsoft.Boogie.Houdini { } } - class PredicateAbsConjunct + public class PredicateAbsConjunct { - static int ConjunctBound = 3; - public static string tempProcName = null; + static int ConjunctBound = 2; public bool isFalse { get; private set; } HashSet posPreds; HashSet negPreds; + string ProcName; public static void Initialize(int bound) { @@ -1703,33 +1949,83 @@ namespace Microsoft.Boogie.Houdini { } } - public PredicateAbsConjunct(bool isFalse) + // 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; } - public static PredicateAbsConjunct Singleton(int v, bool isPositive) + // 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()); + return new PredicateAbsConjunct(new int[] { v }, new HashSet(), ProcName); else - return new PredicateAbsConjunct(new HashSet(), new int[] { v }); + return new PredicateAbsConjunct(new HashSet(), new int[] { v }, ProcName); } - public PredicateAbsConjunct(IEnumerable pos, IEnumerable neg) + 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); - return new PredicateAbsConjunct(v1.posPreds.Union(v2.posPreds), v1.negPreds.Union(v2.negPreds)); + 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) @@ -1766,12 +2062,12 @@ namespace Microsoft.Boogie.Houdini { var first = true; foreach (var p in posPreds) { - ret += string.Format("{0}{1}", first ? "" : " && ", PredicateAbs.PrePreds[tempProcName][p]); + 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[tempProcName][p]); + ret += string.Format("{0}!{1}", first ? "" : " && ", PredicateAbs.PrePreds[ProcName][p]); first = false; } return ret; -- cgit v1.2.3