From 8cc5d9cc9d455b42fc19881f29da47a08f10d8e1 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 5 Nov 2012 15:52:27 +0530 Subject: Added Abstract Houdini: an implementation of Houdini based on abstract domains. Currently only predicate-abstraction domain is supported. --- Source/BoogieDriver/BoogieDriver.cs | 10 + Source/Core/CommandLineOptions.cs | 9 + Source/Houdini/AbstractHoudini.cs | 1062 +++++++++++++++++++++++++++++++++++ Source/Houdini/Houdini.csproj | 5 + Test/AbsHoudini/Answer | 19 + Test/AbsHoudini/f1.bpl | 32 ++ Test/AbsHoudini/runtest.bat | 11 + Test/alltests.txt | 1 + 8 files changed, 1149 insertions(+) create mode 100644 Source/Houdini/AbstractHoudini.cs create mode 100644 Test/AbsHoudini/Answer create mode 100644 Test/AbsHoudini/f1.bpl create mode 100644 Test/AbsHoudini/runtest.bat diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 6729532e..035eb549 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -617,6 +617,16 @@ namespace Microsoft.Boogie { #region Run Houdini and verify if (CommandLineOptions.Clo.ContractInfer) { + if (CommandLineOptions.Clo.AbstractHoudini != null) + { + CommandLineOptions.Clo.PrintErrorModel = 1; + // Run Abstract Houdini + Houdini.PredicateAbs.Initialize(program); + var abs = new Houdini.AbstractHoudini(program); + abs.computeSummaries(new Houdini.PredicateAbs()); + + return PipelineOutcome.Done; + } Houdini.Houdini houdini = new Houdini.Houdini(program); Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); if (CommandLineOptions.Clo.PrintAssignment) { diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 06474981..1c00077d 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -393,6 +393,7 @@ namespace Microsoft.Boogie { public int /*(0:3)*/ ErrorTrace = 1; public bool IntraproceduralInfer = true; public bool ContractInfer = false; + public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; public int InlineDepth = -1; @@ -850,6 +851,14 @@ namespace Microsoft.Boogie { return true; } + case "abstractHoudini": + { + if (ps.ConfirmArgumentCount(1)) + { + AbstractHoudini = args[ps.i]; + } + return true; + } case "vc": if (ps.ConfirmArgumentCount(1)) { switch (args[ps.i]) { diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs new file mode 100644 index 00000000..967e353f --- /dev/null +++ b/Source/Houdini/AbstractHoudini.cs @@ -0,0 +1,1062 @@ +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 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; + + public static readonly string summaryPredSuffix = "SummaryPred"; + + // Essentials: VCGen, Prover, and reporter + VCGen vcgen; + ProverInterface prover; + AbstractHoudiniErrorReporter reporter; + + 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 = BoogieUtil.nameImplMapping(program); + + 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.reporter = new AbstractHoudiniErrorReporter(); + + var impls = new List( + program.TopLevelDeclarations.OfType()); + + // Create all VCs + impls + .Iter(attachEnsures); + + impls + .Iter(GenVC); + + } + + public void computeSummaries(ISummaryElement summaryClass) + { + this.summaryClass = summaryClass; + + var main = program.TopLevelDeclarations + .OfType() + .Where(impl => QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) + .FirstOrDefault(); + + Debug.Assert(main != null); + + program.TopLevelDeclarations + .OfType() + .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.TopLevelDeclarations.OfType()) + { + 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 => Succ[n]), + new Adjacency(n => Pred[n])); + sccs.Compute(); + + // impl -> priority + var impl2Priority = new Dictionary(); + int p = 0; + foreach (var scc in sccs) + { + scc.Iter(n => impl2Priority.Add(n.Name, p)); + p++; + } + + 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].Iter(pred => worklist.Add(Tuple.Create(impl2Priority[pred.Name], pred))); + } + } + + foreach (var tup in impl2Summary) + { + Console.WriteLine("Summary of {0}:", tup.Key); + Console.WriteLine("{0}", tup.Value); + } + + prover.Close(); + CommandLineOptions.Clo.TheProverFactory.Close(); + } + + 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]) + { + if (tup.Item1 == impl.Name) + continue; + + var calleeSummary = + impl2Summary[tup.Item1].GetSummaryExpr( + GetVarMapping(name2Impl[tup.Item1], tup.Item2), prover.VCExprGen); + env = gen.AndSimp(env, gen.Eq(tup.Item2, calleeSummary)); + } + + while(true) + { + // construct self summaries + var summaryExpr = VCExpressionGenerator.True; + foreach (var tup in impl2CalleeSummaries[impl.Name]) + { + if (tup.Item1 != impl.Name) + continue; + + var ts = + impl2Summary[tup.Item1].GetSummaryExpr( + GetVarMapping(name2Impl[tup.Item1], tup.Item2), prover.VCExprGen); + summaryExpr = gen.AndSimp(summaryExpr, gen.Eq(tup.Item2, 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); + + prover.BeginCheck(impl.Name, vc, reporter); + ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter); + if (reporter.model == null) + break; + + var state = CollectState(impl); + impl2Summary[impl.Name].Join(state); + ret = true; + } + return ret; + } + + private Dictionary GetVarMapping(Implementation impl, VCExprNAry summaryPred) + { + var ret = new Dictionary(); + + var cnt = 0; + foreach (var g in program.TopLevelDeclarations.OfType()) + { + 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++; + } + + 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.TopLevelDeclarations.OfType()) + { + 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++; + } + + return ret; + } + + private Model.Element getValue(VCExpr arg, Model model) + { + if (arg is VCExprLiteral) + { + return model.GetElement(arg.ToString()); + } + else if (arg is VCExprVar) + { + var el = model.GetFunc(prover.Context.Lookup(arg as VCExprVar)); + Debug.Assert(el.Arity == 0 && el.AppCount == 1); + return el.Apps.First().Result; + } + else + { + Debug.Assert(false); + return null; + } + } + + private void attachEnsures(Implementation impl) + { + VariableSeq functionInterfaceVars = new VariableSeq(); + 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, ""); + + ExprSeq exprs = new ExprSeq(); + 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, "")); + } + + private void GenVC(Implementation impl) + { + ModelViewInfo mvInfo; + System.Collections.Hashtable label2absy; + + vcgen.ConvertCFG2DAG(impl); + vcgen.PassifyImpl(impl, out mvInfo); + + var gen = prover.VCExprGen; + var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context); + + // Create a macro so that the VC can sit with the theorem prover + Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false)); + prover.DefineMacro(macro, vcexpr); + + // Store VC + impl2VC.Add(impl.Name, gen.Function(macro)); + + //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr); + + // Find the assert + impl2EndStateVars.Add(impl.Name, new List()); + var found = false; + foreach (var blk in impl.Blocks) + { + foreach (var cmd in blk.Cmds.OfType()) + { + if (BoogieUtil.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; + nary.Args.OfType() + .Iter(expr => impl2EndStateVars[impl.Name].Add(prover.Context.BoogieExprTranslator.Translate(expr))); + } + } + Debug.Assert(found); + + // Grab summary predicates + var visitor = new FindSummaryPred(prover.VCExprGen); + visitor.Mutate(vcexpr, true); + + impl2CalleeSummaries.Add(impl.Name, new List>()); + visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup)); + } + } + + public interface ISummaryElement + { + ISummaryElement GetFlaseSummary(Program program, Implementation impl); + void Join(Dictionary state); + VCExpr GetSummaryExpr(Dictionary incarnations, VCExpressionGenerator gen); + } + + 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) + { + 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); + } + } + + public class PredicateAbs : ISummaryElement + { + public static List PrePreds { get; private set; } + public static List PostPreds { get; private set; } + + PredicateAbsDisjunct[] value; + bool isFalse; + + public PredicateAbs() + { + isFalse = true; + value = new PredicateAbsDisjunct[PostPreds.Count]; + for (int i = 0; i < PostPreds.Count; i++) value[i] = null; + } + + public static void Initialize(Program program) + { + PrePreds = new List(); + PostPreds = new List(); + + foreach (var proc in + program.TopLevelDeclarations.OfType() + .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template"))) + { + foreach (var ens in proc.Ensures.OfType()) + { + if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre")) + PrePreds.Add(ens.Condition); + else + PostPreds.Add(ens.Condition); + } + } + + Console.WriteLine("Running Abstract Houdini"); + PostPreds.Iter(expr => Console.WriteLine("\tPost: {0}", expr)); + PrePreds.Iter(expr => Console.WriteLine("\tPre: {0}", expr)); + } + + private object Eval(Expr expr, Dictionary state) + { + if (expr is LiteralExpr) + { + return (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 (nary.Fun as UnaryOperator).Evaluate(Eval(nary.Args[0], state)); + } + if (nary.Fun is BinaryOperator) + { + return (nary.Fun as BinaryOperator).Evaluate(Eval(nary.Args[0], state), Eval(nary.Args[1], state)); + } + Debug.Assert(false, "No other op is handled"); + } + throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString())); + } + + private object LookupVariable(string v, Dictionary state, bool tryOld) + { + if (tryOld) + { + var oldv = string.Format("old({0})", v); + if (state.ContainsKey(oldv)) + { + return ToValue(state[oldv]); + } + throw new InternalError("Cannot handle this case"); + } + + if (state.ContainsKey(v)) + { + return ToValue(state[v]); + } + + throw new InternalError("Cannot handle this case"); + } + + private 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 InternalError("Cannot handle this case"); + } + + if (incarnations.ContainsKey(v)) + { + return incarnations[v]; + } + + throw new InternalError("Cannot handle this case"); + } + + 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; + } + throw new NotImplementedException("Cannot yet handle this Model.Element type"); + } + + private 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) + { + Debug.Assert((nary.Fun as UnaryOperator).Op == UnaryOperator.Opcode.Not); + return gen.Not(ToVcExpr(nary.Args[0], incarnations, gen)); + } + 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)); + } + Debug.Assert(false, "No other op is handled"); + } + throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString())); + } + + private 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(); + } + + } + + public override string ToString() + { + var ret = ""; + if (isFalse) return "false"; + var first = true; + for(int i = 0; i < PostPreds.Count; i++) + { + if(value[i].isFalse) continue; + + if(value[i].isTrue) + ret += string.Format("{0}{1}", first ? "" : " && ", PostPreds[i]); + else + ret += string.Format("{0}({1} ==> {2})", first ? "" : " && ", value[i], PostPreds[i]); + + first = false; + } + return ret; + } + + + #region ISummaryElement Members + + public ISummaryElement GetFlaseSummary(Program program, Implementation impl) + { + return new PredicateAbs(); + } + + public void Join(Dictionary state) + { + // Evaluate each predicate on the state + var prePredsVal = new bool[PrePreds.Count]; + var postPredsVal = new bool[PostPreds.Count]; + + var indexSeq = new List(); + for(int i = 0; i < PrePreds.Count; i++) indexSeq.Add(i); + + for (int i = 0; i < PrePreds.Count; i++) + { + var v = Eval(PrePreds[i], state); + Debug.Assert(v is bool); + prePredsVal[i] = (bool)v; + } + + for (int i = 0; i < PostPreds.Count; i++) + { + var v = Eval(PostPreds[i], state); + Debug.Assert(v is bool); + postPredsVal[i] = (bool)v; + } + + for (int i = 0; i < PostPreds.Count; i++) + { + // No hope for this post pred? + if (!isFalse && value[i].isFalse) continue; + + var newDisj = new PredicateAbsDisjunct(true); + if (!postPredsVal[i]) + { + newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j])); + } + + if (isFalse) + value[i] = newDisj; + else + value[i] = PredicateAbsDisjunct.And(value[i], newDisj); + } + + isFalse = false; + } + + public VCExpr GetSummaryExpr(Dictionary incarnations, VCExpressionGenerator gen) + { + if (isFalse) + return VCExpressionGenerator.False; + + var ret = VCExpressionGenerator.True; + + for(int i = 0; i < PostPreds.Count; i++) + { + ret = gen.AndSimp(ret, gen.ImpliesSimp(value[i].ToVcExpr(j => ToVcExpr(PrePreds[j], incarnations, gen), gen), ToVcExpr(PostPreds[i], incarnations, gen))); + } + + return ret; + } + + #endregion + } + + class PredicateAbsDisjunct + { + List conjuncts; + public bool isTrue {get; private set;} + public bool isFalse + { + get + { + if (isTrue) return false; + return conjuncts.Count == 0; + } + } + + public PredicateAbsDisjunct(bool isTrue) + { + this.isTrue = isTrue; + conjuncts = new List(); + } + + private PredicateAbsDisjunct(List conjuncts) + { + isTrue = false; + this.conjuncts = conjuncts; + } + + // Disjunct of singleton conjuncts + public PredicateAbsDisjunct(IEnumerable pos, IEnumerable neg) + { + conjuncts = new List(); + isTrue = false; + pos.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, true))); + neg.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, false))); + } + + 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); + } + + 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 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; + } + } + + class PredicateAbsConjunct + { + static int ConjunctBound = 3; + + public bool isFalse { get; private set; } + HashSet posPreds; + HashSet negPreds; + + 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(); + } + } + + public PredicateAbsConjunct(bool isFalse) + { + posPreds = new HashSet(); + negPreds = new HashSet(); + this.isFalse = isFalse; + } + + public static PredicateAbsConjunct Singleton(int v, bool isPositive) + { + if (isPositive) + return new PredicateAbsConjunct(new int[] { v }, new HashSet()); + else + return new PredicateAbsConjunct(new HashSet(), new int[] { v }); + } + + public PredicateAbsConjunct(IEnumerable pos, IEnumerable neg) + { + isFalse = false; + posPreds = new HashSet(pos); + negPreds = new HashSet(neg); + 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)); + } + + 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 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[p]); + first = false; + } + foreach (var p in negPreds) + { + ret += string.Format("{0}!{1}", first ? "" : " && ", PredicateAbs.PrePreds[p]); + first = false; + } + return ret; + } + } + + class FindSummaryPred : MutatingVCExprVisitor + { + public List> summaryPreds; + + public FindSummaryPred(VCExpressionGenerator gen) + : base(gen) + { + summaryPreds = new List>(); + } + + 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 (!calleeName.EndsWith(AbstractHoudini.summaryPredSuffix)) + return ret; + + summaryPreds.Add(Tuple.Create(calleeName.Substring(0, calleeName.Length - AbstractHoudini.summaryPredSuffix.Length), retnary)); + + return ret; + } + + } + + class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler + { + public Model model; + + public AbstractHoudiniErrorReporter() + { + model = null; + } + + public override void OnModel(IList labels, Model model) + { + Debug.Assert(model != null); + //model.Write(Console.Out); + this.model = model; + } + } + + + public class InternalError : System.ApplicationException + { + public InternalError(string msg) : base(msg) { } + + }; + + public class BoogieUtil + { + // Constructs a mapping from procedure names to the implementation + public static Dictionary nameImplMapping(Program p) + { + var m = new Dictionary(); + foreach (Declaration d in p.TopLevelDeclarations) + { + if (d is Implementation) + { + Implementation impl = d as Implementation; + 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; + } + } + +} diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 97d26001..2d2b0373 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -78,6 +78,7 @@ version.cs + @@ -98,6 +99,10 @@ {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph + + {acef88d5-dadd-46da-bae1-2144d63f4c83} + Model + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} ParserHelper diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer new file mode 100644 index 00000000..376d9f3a --- /dev/null +++ b/Test/AbsHoudini/Answer @@ -0,0 +1,19 @@ + +-------------------- f1.bpl -------------------- +Running Abstract Houdini + Post: g == old(g) + 1 + Post: g == old(g) + 2 + Post: g == old(g) + 3 + Pre: old(g) == 0 +Trying summary for foo: (And (== (fooSummaryPred g g@0) false) (== (fooSummaryPred g g@0) false)) +Trying summary for foo: (And (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))) (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3)))))) +Trying summary for foo: (And (== (fooSummaryPred g g@0) (== g@0 (+ g 1))) (== (fooSummaryPred g g@0) (== g@0 (+ g 1)))) +Trying summary for main: (And (== (mainSummaryPred g g@3) false) (== (mainSummaryPred g g@3) false)) +Trying summary for main: (And (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))) (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3)))))) +Trying summary for main: (And (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))) (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1))))) +Summary of main: +(old(g) == 0 ==> g == old(g) + 1) +Summary of foo: +g == old(g) + 1 + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl new file mode 100644 index 00000000..5ea6797b --- /dev/null +++ b/Test/AbsHoudini/f1.bpl @@ -0,0 +1,32 @@ +var g: int; + +procedure {:entrypoint} main() + modifies g; +{ + var x: int; + var c: bool; + + g := 1; + + if(c) { + g := g + 1; + } else { + g := 3; + } + + call foo(); + + if(old(g) == 0) { g := 1; } +} + +procedure foo() + modifies g; +{ + g := g + 1; +} + +procedure {:template} summaryTemplate(); + ensures g == old(g) + 1; + ensures g == old(g) + 2; + ensures g == old(g) + 3; + ensures {:pre} old(g) == 0; diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat new file mode 100644 index 00000000..34308e4e --- /dev/null +++ b/Test/AbsHoudini/runtest.bat @@ -0,0 +1,11 @@ +@echo off +setlocal + +set BGEXE=..\..\Binaries\Boogie.exe + +for %%f in (f1.bpl) do ( + echo. + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f +) + diff --git a/Test/alltests.txt b/Test/alltests.txt index 63b4fe5b..1cd0da4f 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -34,3 +34,4 @@ VSI-Benchmarks Use Solutions to Verified Software Initiative verification c vacid0 Use Dafny attempts to VACID Edition 0 benchmarks vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems +AbsHoudini Postponed Test for abstract houdini -- cgit v1.2.3