diff options
Diffstat (limited to 'Source/Houdini/AbstractHoudini.cs')
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 9323 |
1 files changed, 4714 insertions, 4609 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index de3d3779..e3625dcc 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -1,4609 +1,4714 @@ -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<string, Function> existentialFunctions;
- Program program;
- Dictionary<string, Implementation> name2Impl;
- Dictionary<string, VCExpr> impl2VC;
- Dictionary<string, List<Tuple<string, Function, NAryExpr>>> impl2FuncCalls;
- // constant -> the naryexpr that it replaced
- Dictionary<string, NAryExpr> constant2FuncCall;
-
- // function -> its abstract value
- Dictionary<string, IAbstractDomain> function2Value;
-
- // impl -> functions assumed/asserted
- Dictionary<string, HashSet<string>> impl2functionsAsserted, impl2functionsAssumed;
-
- // funtions -> impls where assumed/asserted
- Dictionary<string, HashSet<string>> function2implAssumed, function2implAsserted;
-
- // impl -> handler, collector
- Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>> impl2ErrorHandler;
-
- // Essentials: VCGen, Prover
- VCGen vcgen;
- ProverInterface prover;
-
- // Stats
- TimeSpan proverTime;
- int numProverQueries;
-
- public AbsHoudini(Program program, IAbstractDomain defaultElem)
- {
- this.program = program;
- this.impl2VC = new Dictionary<string, VCExpr>();
- this.impl2FuncCalls = new Dictionary<string, List<Tuple<string, Function, NAryExpr>>>();
- this.existentialFunctions = new Dictionary<string, Function>();
- this.name2Impl = new Dictionary<string, Implementation>();
- this.impl2functionsAsserted = new Dictionary<string, HashSet<string>>();
- this.impl2functionsAssumed = new Dictionary<string, HashSet<string>>();
- this.function2implAsserted = new Dictionary<string, HashSet<string>>();
- this.function2implAssumed = new Dictionary<string, HashSet<string>>();
- this.impl2ErrorHandler = new Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>>();
- this.constant2FuncCall = new Dictionary<string, NAryExpr>();
-
- // Find the existential functions
- foreach (var func in program.Functions
- .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))
- existentialFunctions.Add(func.Name, func);
-
- this.function2Value = new Dictionary<string, IAbstractDomain>();
- 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<string>()));
- existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet<string>()));
-
- // 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<Type>();
- 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<Checker>());
- 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<Counterexample>());
-
- // Compute SCCs and determine a priority order for impls
- var Succ = new Dictionary<string, HashSet<string>>();
- var Pred = new Dictionary<string, HashSet<string>>();
- name2Impl.Keys.Iter(s => Succ[s] = new HashSet<string>());
- name2Impl.Keys.Iter(s => Pred[s] = new HashSet<string>());
-
- foreach(var impl in name2Impl.Keys) {
- Succ[impl] = new HashSet<string>();
- impl2functionsAsserted[impl].Iter(f =>
- function2implAssumed[f].Iter(succ =>
- {
- Succ[impl].Add(succ);
- Pred[succ].Add(impl);
- }));
- }
-
- var sccs = new StronglyConnectedComponents<string>(name2Impl.Keys,
- new Adjacency<string>(n => Pred[n]),
- new Adjacency<string>(n => Succ[n]));
- sccs.Compute();
-
- // impl -> priority
- var impl2Priority = new Dictionary<string, int>();
- int p = 0;
- foreach (var scc in sccs)
- {
- foreach (var impl in scc)
- {
- impl2Priority.Add(impl, p);
- p++;
- }
- }
-
- var worklist = new SortedSet<Tuple<int, string>>();
- name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k)));
-
- while (worklist.Any())
- {
- var impl = worklist.First().Item2;
- worklist.Remove(worklist.First());
-
- var gen = prover.VCExprGen;
- var terms = new List<Expr>();
- foreach (var tup in impl2FuncCalls[impl])
- {
- var controlVar = tup.Item2;
- var exprVars = tup.Item3;
- var varList = new List<Expr>();
- exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v));
-
- var args = new List<Expr>();
- 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<Variable>(controlVar.InParams.ToArray()),
- new Trigger(Token.NoToken, true, new List<Expr> { 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<string>();
- impl2FuncCalls[impl].Iter(tup => envFuncs.Add(tup.Item1));
- envFuncs.Iter(f => PrintFunction(existentialFunctions[f]));
- }
-
- var handler = impl2ErrorHandler[impl].Item1;
- var collector = impl2ErrorHandler[impl].Item2;
- collector.Reset(impl);
-
- var start = DateTime.Now;
-
- prover.Push();
- prover.Assert(gen.Not(vc), true);
- prover.FlushAxiomsToTheoremProver();
- prover.Check();
- ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
-
- //prover.BeginCheck(impl, vc, handler);
- //ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
-
- var inc = (DateTime.Now - start);
- proverTime += inc;
- numProverQueries++;
-
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());
-
- if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
- {
- // 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<Counterexample>());
- }
-
- 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<string>();
- deps.Add(impl);
- funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f]));
-
- deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s)));
- }
-
- prover.Pop();
- }
-
- if (CommandLineOptions.Clo.Trace)
- {
- Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2"));
- Console.WriteLine("Number of prover queries = " + numProverQueries);
- }
-
- if (CommandLineOptions.Clo.PrintAssignment)
- {
- // Print the answer
- existentialFunctions.Values.Iter(PrintFunction);
- }
-
- return overallOutcome;
- }
-
-
- public IEnumerable<Function> GetAssignment()
- {
- var ret = new List<Function>();
- foreach (var func in existentialFunctions.Values)
- {
- var invars = new List<Expr>(func.InParams.OfType<Variable>().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<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));
- function.Body = function2Value[function.Name].Gamma(invars);
- function.Emit(tt, 0);
- tt.Close();
- }
-
- public HashSet<string> HandleCounterExample(string impl, Counterexample error)
- {
- var funcsChanged = new HashSet<string>();
- // Find the failing assert -- need to do a join there
- // return the set of functions whose definition has changed
- var cex = ExtractState(impl, error);
- foreach (var tup in cex)
- {
- function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2);
- funcsChanged.Add(tup.Item1);
- }
- return funcsChanged;
- }
-
- private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Counterexample error)
- {
- var lastBlock = error.Trace.Last() as Block;
- AssertCmd failingAssert = null;
-
- CallCounterexample callCounterexample = error as CallCounterexample;
- if (callCounterexample != null)
- {
- Procedure failingProcedure = callCounterexample.FailingCall.Proc;
- Requires failingRequires = callCounterexample.FailingRequires;
- failingAssert = lastBlock.Cmds.OfType<AssertRequiresCmd>().FirstOrDefault(ac => ac.Requires == failingRequires);
- }
- ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
- if (returnCounterexample != null)
- {
- Ensures failingEnsures = returnCounterexample.FailingEnsures;
- failingAssert = lastBlock.Cmds.OfType<AssertEnsuresCmd>().FirstOrDefault(ac => ac.Ensures == failingEnsures);
- }
- AssertCounterexample assertCounterexample = error as AssertCounterexample;
- if (assertCounterexample != null)
- {
- failingAssert = lastBlock.Cmds.OfType<AssertCmd>().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert);
- }
-
- Debug.Assert(failingAssert != null);
- return ExtractState(impl, failingAssert.Expr, error.Model);
- }
-
- private static int existentialConstCounter = 0;
-
- private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Expr expr, Model model)
- {
- var funcsUsed = FunctionCollector.Collect(expr);
-
- var ret = new List<Tuple<string, List<Model.Element>>>();
-
- 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<Model.Element>();
- 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<Expr>();
- tup3.Item3.Args.OfType<Expr>().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<string, Constant>();
- foreach (var f in boundExpr.Dummies.OfType<Variable>())
- 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<Model.Element>();
- foreach (var funcArg in func.Args.OfType<Expr>())
- {
- 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<Function> ahFuncs;
-
- public ExistentialExprModelMassage()
- {
- ahFuncs = new List<Function>();
- }
-
- public static Tuple<Expr, List<Function>> 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<Tuple<Function, ExistsExpr>> functionsUsed;
- ExistsExpr existentialExpr;
-
- public FunctionCollector()
- {
- functionsUsed = new List<Tuple<Function, ExistsExpr>>();
- existentialExpr = null;
- }
-
- public static List<Tuple<Function, ExistsExpr>> 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<Function, ExistsExpr>((node.Fun as FunctionCall).Func, null));
- }
-
- return base.VisitNAryExpr(node);
- }
- }
-
- class AbsHoudiniCounterexampleCollector : VerifierCallback
- {
- public HashSet<string> funcsChanged;
- public string currImpl;
- public int numErrors;
- public List<Counterexample> errors;
-
- AbsHoudini container;
-
- public AbsHoudiniCounterexampleCollector(AbsHoudini container)
- {
- this.container = container;
- Reset(null);
- }
-
- public void Reset(string impl)
- {
- funcsChanged = new HashSet<string>();
- currImpl = impl;
- numErrors = 0;
- errors = new List<Counterexample>();
- }
-
- 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<int, Absy> 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<string>(existentialFunctions.Keys);
- var fv = new ReplaceFunctionCalls(existentialFunctionNames);
- fv.VisitBlockList(impl.Blocks);
-
- impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);
- impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);
-
- fv.functionsAssumed.Iter(f => function2implAssumed[f].Add(impl.Name));
- fv.functionsAsserted.Iter(f => function2implAsserted[f].Add(impl.Name));
-
- impl2FuncCalls.Add(impl.Name, fv.functionsUsed);
- fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3));
-
- var gen = prover.VCExprGen;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO);
-
- var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context);
- if (!CommandLineOptions.Clo.UseLabels)
- {
- VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO));
- VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vcexpr = gen.Implies(eqExpr, vcexpr);
- }
-
- ProverInterface.ErrorHandler handler = null;
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
- handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
- else
- handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
-
- impl2ErrorHandler.Add(impl.Name, Tuple.Create(handler, collector));
-
- //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
-
- // Create a macro so that the VC can sit with the theorem prover
- Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), 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<string>(existentialFunctions.Keys);
- foreach (var blk in impl.Blocks)
- {
- foreach (var acmd in blk.Cmds.OfType<AssertCmd>())
- {
- 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<string>(existentialFunctions.Keys);
- foreach (var blk in impl.Blocks)
- {
- foreach (var acmd in blk.Cmds.OfType<AssertCmd>())
- {
- 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<Implementation> oldCallGraph = callGraph;
- callGraph = new Graph<Implementation>();
- foreach (Implementation impl in oldCallGraph.Nodes)
- {
- callGraph.AddSource(impl);
- }
- foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
- {
- callGraph.AddEdge(edge.Item1, edge.Item2);
- }
- int count = CommandLineOptions.Clo.InlineDepth;
- while (count > 0)
- {
- foreach (Implementation impl in oldCallGraph.Nodes)
- {
- List<Implementation> newNodes = new List<Implementation>();
- foreach (Implementation succ in callGraph.Successors(impl))
- {
- newNodes.AddRange(oldCallGraph.Successors(succ));
- }
- foreach (Implementation newNode in newNodes)
- {
- callGraph.AddEdge(impl, newNode);
- }
- }
- count--;
- }
- }
-
- private Graph<Implementation> BuildCallGraph()
- {
- Graph<Implementation> callGraph = new Graph<Implementation>();
- Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- foreach (var proc in program.Procedures)
- {
- procToImpls[proc] = new HashSet<Implementation>();
- }
- 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<string> inlinedFunctionsStack;
-
- public InlineFunctionCalls()
- {
- inlinedFunctionsStack = new Stack<string>();
- }
-
- 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<Variable, Expr>();
- 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<Tuple<string, Function, NAryExpr>> functionsUsed;
- public List<Function> boolConstants;
-
- public HashSet<string> functionsAssumed;
- public HashSet<string> functionsAsserted;
- HashSet<string> functionsToReplace;
-
- private bool inAssume;
- private bool inAssert;
- private bool inFunction;
- private List<Dictionary<string, Variable>> boundVars;
- private static int IdCounter = 0;
-
- public ReplaceFunctionCalls(HashSet<string> functionsToReplace)
- {
- this.functionsUsed = new List<Tuple<string, Function, NAryExpr>>();
- this.functionsToReplace = functionsToReplace;
- this.functionsAsserted = new HashSet<string>();
- this.functionsAssumed = new HashSet<string>();
- this.boolConstants = new List<Function>();
- this.boundVars = new List<Dictionary<string, Variable>>();
-
- 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<string, Variable>();
- 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<Variable>();
- 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<Expr>();
- bound.OfType<Variable>().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<string> existentialFunctions;
- bool insideExistential;
- Dictionary<Constant, Expr> newConstants;
-
- private ExtractQuantifiers(HashSet<string> existentialFunctions)
- {
- this.existentialFunctions = existentialFunctions;
- insideExistential = false;
- newConstants = new Dictionary<Constant, Expr>();
- }
-
- public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> 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<string> existentialFunctions;
- Dictionary<string, LocalVariable> subst;
- List<LocalVariable> LocalsToAdd;
-
- private StripQuantifiers(HashSet<string> existentialFunctions)
- {
- this.existentialFunctions = existentialFunctions;
- insideQuantifier = 0;
- searchExistentialFunction = false;
- foundExistentialFunction = false;
- LocalsToAdd = new List<LocalVariable>();
- subst = null;
- }
-
- public static Tuple<Expr,List<LocalVariable>> Run(Expr expr, HashSet<string> 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<string, LocalVariable>();
- foreach (var bv in node.Dummies.OfType<Variable>())
- {
- 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<Model.Element> states)
- {
- Debug.Assert(states.Count == 1);
- var state = states[0] as Model.Integer;
- if (state == null)
- throw new AbsHoudiniInternalError("Incorrect type, expected int");
- var intval = state.AsInt();
-
- if (isBottom)
- {
- return new Intervals(intval, intval, 1);
- }
-
- if(intval >= lower && intval <= upper)
- return this;
-
- if (nJoin > maxJoin)
- {
- // widen
- if (intval > upper)
- return new Intervals(lower, Int32.MaxValue, 1);
- if(intval < lower)
- return new Intervals(Int32.MinValue, upper, 1);
-
- Debug.Assert(false);
- }
-
- if (intval > upper)
- return new Intervals(lower, intval, nJoin + 1);
- if (intval < lower)
- return new Intervals(intval, upper, nJoin + 1);
-
- Debug.Assert(false);
- return null;
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- Debug.Assert(vars.Count == 1);
- var v = vars[0];
- if (isBottom) return Expr.False;
- Expr ret = Expr.True;
- if (lower != Int32.MinValue)
- ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower)));
- if (upper != Int32.MaxValue)
- ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper)));
- return ret;
- }
-
- public bool TypeCheck(List<Type> 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<int> pos;
- HashSet<int> neg;
- bool isTrue;
-
- public Disjunct()
- {
- isTrue = true;
- pos = new HashSet<int>();
- neg = new HashSet<int>();
- }
-
- public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
- {
- this.isTrue = false;
- this.pos = new HashSet<int>(pos);
- this.neg = new HashSet<int>(neg);
- if (this.pos.Overlaps(this.neg))
- {
- this.isTrue = true;
- this.pos = new HashSet<int>();
- this.neg = new HashSet<int>();
- }
- if (this.pos.Count + this.neg.Count > DisjunctBound)
- {
- // Set to true
- this.isTrue = true;
- this.pos = new HashSet<int>();
- this.neg = new HashSet<int>();
- }
-
- }
-
- public Disjunct OR(Disjunct that)
- {
- if (isTrue)
- return this;
- if (that.isTrue)
- return that;
-
- return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
- }
-
- public bool Implies(Disjunct that)
- {
- if (isTrue) return that.isTrue;
- if (that.isTrue) return true;
-
- return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg);
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- if (isTrue) return Expr.True;
- Expr ret = Expr.False;
- pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i]));
- neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i])));
- return ret;
- }
- }
-
- // Conjunction of Disjuncts
- List<Disjunct> conjuncts;
- bool isFalse;
-
- public PredicateAbsElem()
- {
- this.conjuncts = new List<Disjunct>();
- this.isFalse = true;
- }
-
- public IAbstractDomain Bottom()
- {
- return new PredicateAbsElem();
- }
-
- public IAbstractDomain 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<Model.Element> state)
- {
- if (state.Any(me => !(me is Model.Boolean)))
- throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool");
-
- // quick return if this == true
- if (!this.isFalse && conjuncts.Count == 0)
- return this;
-
- var ret = new PredicateAbsElem();
- ret.isFalse = false;
-
- for (int i = 0; i < state.Count; i++)
- {
- var b = (state[i] as Model.Boolean).Value;
- Disjunct d = null;
- if (b) d = new Disjunct(new int[] { i }, new int[] { });
- else d = new Disjunct(new int[] { }, new int[] { i });
-
- if (isFalse)
- ret.AddDisjunct(d);
- else
- {
- conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
- }
- }
-
- return ret;
-
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- if (isFalse) return Expr.False;
- Expr ret = Expr.True;
-
- foreach (var c in conjuncts)
- {
- ret = ExprExt.AndSimp(ret, c.Gamma(vars));
- }
-
- return ret;
- }
-
- public bool TypeCheck(List<Type> 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<Model.Element> states)
- {
- Debug.Assert(states.Count == 1);
- var state = states[0];
-
- if (isTop) return this;
-
- if (state is Model.Boolean)
- {
- if ((state as Model.Boolean).Value)
- return GetExtObj();
- }
-
- return GetTop();
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- Debug.Assert(vars.Count == 1);
- var v = vars[0];
- if (isBottom) return Expr.False;
- if (isTop) return Expr.True;
- return v;
- }
-
- public bool TypeCheck(List<Type> 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<Model.Element> 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<Expr> 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<Expr> { 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<Type> 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<HashSet<int>> equalities;
-
- public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq)
- {
- this.isBottom = isBottom;
- this.equalities = eq;
- }
-
- public static IAbstractDomain GetBottom()
- {
- return new EqualitiesDomain(true, new List<HashSet<int>>());
- }
-
- 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<HashSet<int>>());
- }
-
- IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
- {
- // find the guys that are equal
- var eq = new List<HashSet<int>>();
- 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<int>(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<int>(m2[i].Intersect(m1[i]));
-
-
- // map from representative to set
- var repToSet = new Dictionary<int, HashSet<int>>();
-
- 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<HashSet<int>>();
- repToSet.Values.Iter(s => ret.Add(s));
-
- return new EqualitiesDomain(false, ret);
- }
-
- Expr IAbstractDomain.Gamma(List<Expr> 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<Type> 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<int>[] GetMap(List<HashSet<int>> eq, int n)
- {
- var ret = new HashSet<int>[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<Model.Element> 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<Expr> 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<Type> 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<Model.Element> states)
- {
- Debug.Assert(states.Count == 1);
- var state = states[0];
- ConstantProp that = null;
-
- if (state is Model.Integer)
- {
- that = GetExtObj((state as Model.Integer).AsInt());
- }
- else if (state is Model.Boolean)
- {
- that = GetExtObj((state as Model.Boolean).Value);
- }
- else
- {
- throw new AbsHoudiniInternalError("Illegal type " + state.GetType().ToString());
- }
-
- return Join(that);
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- Debug.Assert(vars.Count == 1);
- var v = vars[0];
- if (isBottom) return Expr.False;
- if (isTop) return Expr.True;
- if (val is int)
- return Expr.Eq(v, Expr.Literal((int)val));
- if (val is bool && (bool)val)
- return v;
- if (val is bool && !(bool)val)
- return Expr.Not(v);
-
- return null;
- }
-
- public bool TypeCheck(List<Type> 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<T> : IAbstractDomain where T : class, IAbstractDomain
- {
- bool isBottom;
- int numVars;
- List<T> varVal;
- T underlyingInstance;
-
- public IndependentAttribute()
- {
- isBottom = true;
- numVars = 0;
- varVal = new List<T>();
- underlyingInstance = null;
- }
-
- public IAbstractDomain Bottom()
- {
- return new IndependentAttribute<T>();
- }
-
- public IAbstractDomain MakeTop(out bool changed)
- {
- var mt = new Func<IAbstractDomain>(() =>
- {
- var ret = new IndependentAttribute<T>();
- ret.isBottom = true;
- ret.numVars = numVars;
- ret.underlyingInstance = underlyingInstance;
- ret.varVal = new List<T>();
- 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<Model.Element> state)
- {
- SetUnderlyingInstance();
-
- if (!isBottom && numVars != state.Count)
- {
- throw new AbsHoudiniInternalError(
- string.Format("Got illegal number of arguments ({0}), expected {1}", state.Count, numVars));
- }
-
- var ret = new IndependentAttribute<T>();
- ret.isBottom = false;
- ret.numVars = state.Count;
- for(int i = 0; i < state.Count; i++)
- {
- var sl = new List<Model.Element>();
- sl.Add(state[i]);
- T prev = isBottom ? underlyingInstance.Bottom() as T : varVal[i];
- ret.varVal.Add(prev.Join(sl) as T);
- }
-
- return ret;
- }
-
- public Expr Gamma(List<Expr> vars)
- {
- if (isBottom) return Expr.False;
- if (numVars != vars.Count)
- throw new AbsHoudiniInternalError(
- string.Format("Got illegal number of arguments ({0}), expected {1}", vars.Count, numVars));
-
- Expr ret = Expr.True;
- for (int i = 0; i < numVars; i++)
- {
- var sl = new List<Expr>(); sl.Add(vars[i]);
- ret = Expr.And(ret, varVal[i].Gamma(sl));
- }
-
- return ret;
- }
-
- private void SetUnderlyingInstance()
- {
- if (underlyingInstance != null) return;
- var tt = typeof(T);
- underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T;
- }
-
- public bool TypeCheck(List<Type> argTypes, out string msg)
- {
- SetUnderlyingInstance();
-
- msg = "";
- foreach(var t in argTypes)
- {
- if(!underlyingInstance.TypeCheck(new List<Type>(new Type[] { t }), out msg))
- return false;
- }
- return true;
- }
- }
-
- public class AbstractDomainFactory
- {
- // Type name -> Instance
- private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();
- private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>();
-
- // bitvector operations
- public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>();
-
- 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<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {
- 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<HoudiniConst>() as IAbstractDomain),
- System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>() as IAbstractDomain),
- System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>() as IAbstractDomain),
- System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() 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<Model.Element> state);
- Expr Gamma(List<Expr> vars);
- bool TypeCheck(List<Type> argTypes, out string msg);
- }
-
- public class AbstractHoudini
- {
- // Input Program
- Program program;
- // Impl -> VC
- Dictionary<string, VCExpr> impl2VC;
- // Impl -> Vars at end of the impl
- Dictionary<string, List<VCExpr>> impl2EndStateVars;
- // Impl -> (callee,summary pred)
- Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>> impl2CalleeSummaries;
- // pointer to summary class
- ISummaryElement summaryClass;
- // impl -> summary
- Dictionary<string, ISummaryElement> impl2Summary;
- // name -> impl
- Dictionary<string, Implementation> 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<string, VCExpr>();
- this.impl2EndStateVars = new Dictionary<string, List<VCExpr>>();
- this.impl2CalleeSummaries = new Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>>();
- this.impl2Summary = new Dictionary<string, ISummaryElement>();
- this.name2Impl = SimpleUtil.nameImplMapping(program);
-
- if (CommandLineOptions.Clo.ProverKillTime > 0)
- CommandLineOptions.Clo.ProverOptions = CommandLineOptions.Clo.ProverOptions.Concat1(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
-
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
- 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<Implementation, HashSet<Implementation>>();
- var Pred = new Dictionary<Implementation, HashSet<Implementation>>();
- name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet<Implementation>()));
- name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>()));
-
- foreach (var impl in program.Implementations)
- {
- foreach (var blk in impl.Blocks)
- {
- foreach (var cmd in blk.Cmds.OfType<CallCmd>())
- {
- if (!name2Impl.ContainsKey(cmd.callee)) continue;
- Succ[impl].Add(name2Impl[cmd.callee]);
- Pred[name2Impl[cmd.callee]].Add(impl);
- }
- }
- }
-
- // Build SCC
- var sccs = new StronglyConnectedComponents<Implementation>(name2Impl.Values,
- new Adjacency<Implementation>(n => Pred[n]),
- new Adjacency<Implementation>(n => Succ[n]));
- sccs.Compute();
-
- // impl -> priority
- var impl2Priority = new Dictionary<string, int>();
- int p = 0;
- foreach (var scc in sccs)
- {
- foreach (var impl in scc)
- {
- impl2Priority.Add(impl.Name, p);
- p++;
- }
- }
-
-
- Inline();
-
- #region Witness generation setup
- // Create a copy of the program
- var copy = new Dictionary<string, Implementation>();
- 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<Variable>(impl.LocVars), new List<Block>());
- 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<Tuple<int, Implementation>>();
- 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<Tuple<int, string>>();
- 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<string> GetPredicates()
- {
- var ret = new HashSet<string>();
- 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<string, Expr>();
- foreach (var g in program.GlobalVariables)
- vars.Add(g.Name, Expr.Ident(g));
- foreach (var v in proc.InParams.OfType<Variable>())
- vars.Add(v.Name, Expr.Ident(v));
- foreach (var v in proc.OutParams.OfType<Variable>())
- 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<string, Implementation> copy)
- {
- if (WitnessFile == null)
- return;
-
- foreach (var proc in program.Procedures)
- {
- var nensures = new List<Ensures>();
- proc.Ensures.OfType<Ensures>()
- .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<Declaration>(copy.Values);
- decls.AddRange(program.TopLevelDeclarations.Where(decl => !(decl is Implementation)));
- program.TopLevelDeclarations = decls;
- var name2Proc = new Dictionary<string, Procedure>();
- 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<string, Expr>(s => null), new Func<string, Expr>(s => null)));
- ens.Attributes = new QKeyValue(Token.NoToken, "inferred", new List<object>(), 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<AssumeCmd>())
- {
- 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<string, Expr>();
- var always = new Dictionary<string, Expr>();
- 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<Variable>())
- {
- always.Add(v.Name, expr.Args[i]);
- i++;
- }
- foreach (var v in callee.OutParams.OfType<Variable>())
- {
- always.Add(v.Name, expr.Args[i]);
- i++;
- }
- foreach (var ie in name2Proc[calleeName].Modifies.OfType<IdentifierExpr>())
- {
- 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<Implementation> oldCallGraph = callGraph;
- callGraph = new Graph<Implementation>();
- foreach (Implementation impl in oldCallGraph.Nodes)
- {
- callGraph.AddSource(impl);
- }
- foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
- {
- callGraph.AddEdge(edge.Item1, edge.Item2);
- }
- int count = CommandLineOptions.Clo.InlineDepth;
- while (count > 0)
- {
- foreach (Implementation impl in oldCallGraph.Nodes)
- {
- List<Implementation> newNodes = new List<Implementation>();
- foreach (Implementation succ in callGraph.Successors(impl))
- {
- newNodes.AddRange(oldCallGraph.Successors(succ));
- }
- foreach (Implementation newNode in newNodes)
- {
- callGraph.AddEdge(impl, newNode);
- }
- }
- count--;
- }
- }
-
- private Graph<Implementation> BuildCallGraph()
- {
- Graph<Implementation> callGraph = new Graph<Implementation>();
- Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- foreach (var proc in program.Procedures)
- {
- procToImpls[proc] = new HashSet<Implementation>();
- }
- 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<string, VCExpr> GetVarMapping(Implementation impl, VCExprNAry summaryPred)
- {
- var ret = new Dictionary<string, VCExpr>();
-
- 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<Variable>().Concat(
- impl.OutParams.OfType<Variable>().Concat(
- impl.Proc.Modifies.OfType<IdentifierExpr>().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<string, Model.Element> CollectState(Implementation impl)
- {
- var ret = new Dictionary<string, Model.Element>();
-
- 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<Variable>().Concat(
- impl.OutParams.OfType<Variable>().Concat(
- impl.Proc.Modifies.OfType<IdentifierExpr>().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<Variable> functionInterfaceVars = new List<Variable>();
- 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<Expr> exprs = new List<Expr>();
- 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<object>(), null)));
- }
-
- private void GenVC(Implementation impl)
- {
- ModelViewInfo mvInfo;
- Dictionary<int, Absy> 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<VCExpr>());
- var found = false;
- var assertId = -1;
- foreach (var blk in impl.Blocks)
- {
- foreach (var cmd in blk.Cmds.OfType<AssertCmd>())
- {
- 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<Expr>()
- .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<Variable>(), 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<Tuple<string, bool, VCExprVar, VCExprNAry>>());
- visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup));
- }
- }
-
- public interface ISummaryElement
- {
- ISummaryElement Copy();
- ISummaryElement GetFlaseSummary(Program program, Implementation impl);
- void Join(Dictionary<string, Model.Element> state, Model model);
- VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen);
- Expr GetSummaryExpr(Func<string, Expr> always, Func<string, Expr> 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<string, HashSet<int>> val;
- // set of vars
- HashSet<Variable> vars;
-
- public static readonly int MAX = 3;
-
- public ConstantVal()
- {
- // this is just a place holder
- val = new Dictionary<string, HashSet<int>>();
- vars = new HashSet<Variable>();
- }
-
- private ConstantVal(Program program, Implementation impl)
- {
- this.program = program;
- this.impl = impl;
- this.val = new Dictionary<string, HashSet<int>>();
-
- vars = new HashSet<Variable>();
- impl.Proc.Modifies
- .OfType<IdentifierExpr>()
- .Select(ie => ie.Decl)
- .Where(v => v.TypedIdent.Type.IsInt)
- .Iter(v => vars.Add(v));
- impl.OutParams.OfType<Variable>()
- .Where(v => v.TypedIdent.Type.IsInt)
- .Iter(v => vars.Add(v));
-
- vars.Iter(v => val.Add(v.Name, null));
- }
-
-
- public void Join(Dictionary<string, Model.Element> 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<int>();
- val[v].Add(newv);
- }
- else if(oldv.Count > 0)
- {
- val[v].Add(newv);
- if (val[v].Count > MAX)
- val[v] = new HashSet<int>();
- }
-
- }
- }
-
- public VCExpr GetSummaryExpr(Dictionary<string, VCExpr> 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<string, Expr> always, Func<string, Expr> 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<string, List<NamedExpr>> PrePreds { get; private set; }
- public static Dictionary<string, HashSet<int>> PosPrePreds { get; private set; }
- public static Dictionary<string, List<NamedExpr>> PostPreds { get; private set; }
- public static Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>> UpperCandidates;
- private static HashSet<string> boolConstants;
- // {proc, pred-pair} -> polariry
- public static HashSet<Tuple<string, int, int, bool, bool>> unsatPrePredPairs;
- public static HashSet<Tuple<string, int, int, bool, bool>> 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<string, List<NamedExpr>>();
- PostPreds = new Dictionary<string, List<NamedExpr>>();
- PosPrePreds = new Dictionary<string, HashSet<int>>();
-
- boolConstants = new HashSet<string>();
- UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>();
-
- 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<NamedExpr>();
- var postT = new List<NamedExpr>();
- var posPreT = new HashSet<int>();
- var tempP = new HashSet<Procedure>();
- foreach (var proc in
- program.Procedures
- .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template")))
- {
- tempP.Add(proc);
- foreach (var ens in proc.Ensures.OfType<Ensures>())
- {
- 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<string, List<Expr>>();
-
- foreach (var impl in program.Implementations)
- {
- PrePreds.Add(impl.Name, new List<NamedExpr>());
- PostPreds.Add(impl.Name, new List<NamedExpr>());
- PosPrePreds.Add(impl.Name, new HashSet<int>());
-
- // 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<Ensures>();
- foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())
- {
- 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<Expr>());
- 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<string, int>();
- 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<PredicateAbsDisjunct>());
- 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<PredicateAbsDisjunct>());
- 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<PredicateAbsDisjunct, Expr> 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<int>();
- var neg = new HashSet<int>();
-
- 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<PredicateAbsConjunct>();
- conjls.Add(conj);
-
- return Tuple.Create(new PredicateAbsDisjunct(conjls, procName), postExpr);
- }
-
- // blah && blah ==> {blah, blah}
- static IEnumerable<Expr> DecomposeOuterAnd(Expr expr)
- {
- var ret = new List<Expr>();
-
- 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<string, Model.Element> 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<string, Model.Element> 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<string, VCExpr> 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<Tuple<string, int, int, bool, bool>>();
- unsatPostPredPairs = new HashSet<Tuple<string, int, int, bool, bool>>();
-
- var cachePos = new HashSet<Tuple<string, string>>();
- var cacheNeg = new HashSet<Tuple<string, string>>();
- var record = new Action<object, string, int, int, bool, bool>(
- (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<Dictionary<string, List<NamedExpr>>>();
- 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<Variable>();
- var setb = new HashSet<Variable>();
- 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<string, VCExpr>();
- 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<Tuple<Variable, Expr>> literals;
- bool inOld;
-
- public GatherLiterals()
- {
- literals = new List<Tuple<Variable, Expr>>();
- 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<string, Expr> always, Func<string, Expr> 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<string, VCExpr> 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<string> GetPredicates(Program program, VCExpressionGenerator gen, ProverInterface prover)
- {
- var ret = new HashSet<string>();
- 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<Requires>().Where(req => req.Free))
- {
- freeSummary = Expr.And(freeSummary, MakeOld(req.Condition));
- }
- foreach (var ens in proc.Ensures.OfType<Ensures>().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<string, Model.Element> 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<int>();
- 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<string, VCExpr> 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<string, Expr> always, Func<string, Expr> 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<PredicateAbsConjunct> 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<PredicateAbsConjunct>();
- }
-
- public PredicateAbsDisjunct(List<PredicateAbsConjunct> conjuncts, string ProcName)
- {
- isTrue = false;
- this.conjuncts = conjuncts;
- this.ProcName = ProcName;
- }
-
- // Disjunct of singleton conjuncts
- public PredicateAbsDisjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName)
- {
- this.ProcName = ProcName;
- conjuncts = new List<PredicateAbsConjunct>();
- 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<PredicateAbsConjunct>();
-
- 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<PredicateAbsConjunct>();
- 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<PredicateAbsConjunct>();
- 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<PredicateAbsConjunct>();
- 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<int, VCExpr> 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<int, Expr> 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<PredicateAbsConjunct>();
- foreach (var c1 in conjuncts)
- {
- if (that.conjuncts.Any(c2 => c1.implies(c2)))
- continue;
- ncon.Add(c1);
- }
- conjuncts = ncon;
- }
-
- public IEnumerable<PredicateAbsConjunct> GetConjuncts()
- {
- return conjuncts;
- }
-
- }
-
- public class PredicateAbsConjunct
- {
- static int ConjunctBound = 3;
-
- public bool isFalse { get; private set; }
- HashSet<int> posPreds;
- HashSet<int> 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<int>();
- negPreds = new HashSet<int>();
- }
- }
-
- // Do this step only once in a while?
- private void StrongNormalize()
- {
- if (isFalse) return;
-
- var candidates = new List<Tuple<int, bool>>();
- posPreds.Iter(p => candidates.Add(Tuple.Create(p, true)));
- negPreds.Iter(p => candidates.Add(Tuple.Create(p, false)));
- var drop = new HashSet<int>();
- 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<int>();
- negPreds = new HashSet<int>();
- 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<int>();
- negPreds = new HashSet<int>();
- 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<int>(), ProcName);
- else
- return new PredicateAbsConjunct(new HashSet<int>(), new int[] { v }, ProcName);
- }
-
- public PredicateAbsConjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName)
- {
- isFalse = false;
- posPreds = new HashSet<int>(pos);
- negPreds = new HashSet<int>(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<int, VCExpr> 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<int, Expr> 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<bool>
- {
- public List<Tuple<string, bool, VCExprVar, VCExprNAry>> summaryPreds;
- int assertId;
- private static int CounterId = 0;
-
- public FindSummaryPred(VCExpressionGenerator gen, int assertId)
- : base(gen)
- {
- summaryPreds = new List<Tuple<string, bool, VCExprVar, VCExprNAry>>();
- this.assertId = assertId;
- }
-
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg)
- {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprNAry retnary = ret as VCExprNAry;
- if (retnary == null) return ret;
- var op = retnary.Op as VCExprBoogieFunctionOp;
-
- if (op == null)
- {
- 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<bool>
- {
- public List<Tuple<string, VCExprVar, VCExprNAry>> funcCalls;
- private HashSet<string> existentialFunctions;
- private static int CounterId = 0;
-
- public FindExistentialFunctions(VCExpressionGenerator gen, HashSet<string> existentialFunctions)
- : base(gen)
- {
- funcCalls = new List<Tuple<string, VCExprVar, VCExprNAry>>();
- this.existentialFunctions = existentialFunctions;
- }
-
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg)
- {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprNAry retnary = ret as VCExprNAry;
- if (retnary == null) return ret;
- var op = retnary.Op as VCExprBoogieFunctionOp;
- if (op == null) return ret;
-
- string calleeName = op.Func.Name;
-
- if (!existentialFunctions.Contains(calleeName))
- return ret;
-
- var controlConst = Gen.Variable("AbsHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool);
- CounterId++;
-
- funcCalls.Add(Tuple.Create(calleeName, controlConst, retnary));
-
- return controlConst;
- }
-
- }
-
- class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
- {
- public Model model;
-
- public AbstractHoudiniErrorReporter()
- {
- model = null;
- }
-
- public override void OnModel(IList<string> 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<string, Implementation> nameImplMapping(Program p)
- {
- var m = new Dictionary<string, Implementation>();
- 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;
- }
- }
-
-}
+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<string, Function> existentialFunctions; + Program program; + Dictionary<string, Implementation> name2Impl; + Dictionary<string, VCExpr> impl2VC; + Dictionary<string, List<Tuple<string, Function, NAryExpr>>> impl2FuncCalls; + // constant -> the naryexpr that it replaced + Dictionary<string, NAryExpr> constant2FuncCall; + + // function -> its abstract value + Dictionary<string, IAbstractDomain> function2Value; + + // impl -> functions assumed/asserted + Dictionary<string, HashSet<string>> impl2functionsAsserted, impl2functionsAssumed; + + // funtions -> impls where assumed/asserted + Dictionary<string, HashSet<string>> function2implAssumed, function2implAsserted; + + // impl -> handler, collector + Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>> impl2ErrorHandler; + + // Essentials: VCGen, Prover + VCGen vcgen; + ProverInterface prover; + + // Stats + TimeSpan proverTime; + int numProverQueries; + + public AbsHoudini(Program program, IAbstractDomain defaultElem) + { + this.program = program; + this.impl2VC = new Dictionary<string, VCExpr>(); + this.impl2FuncCalls = new Dictionary<string, List<Tuple<string, Function, NAryExpr>>>(); + this.existentialFunctions = new Dictionary<string, Function>(); + this.name2Impl = new Dictionary<string, Implementation>(); + this.impl2functionsAsserted = new Dictionary<string, HashSet<string>>(); + this.impl2functionsAssumed = new Dictionary<string, HashSet<string>>(); + this.function2implAsserted = new Dictionary<string, HashSet<string>>(); + this.function2implAssumed = new Dictionary<string, HashSet<string>>(); + this.impl2ErrorHandler = new Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>>(); + this.constant2FuncCall = new Dictionary<string, NAryExpr>(); + + // Find the existential functions + foreach (var func in program.Functions + .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential"))) + existentialFunctions.Add(func.Name, func); + + this.function2Value = new Dictionary<string, IAbstractDomain>(); + 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<string>())); + existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet<string>())); + + // 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<Type>(); + 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<Checker>()); + 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<Counterexample>()); + + // Compute SCCs and determine a priority order for impls + var Succ = new Dictionary<string, HashSet<string>>(); + var Pred = new Dictionary<string, HashSet<string>>(); + name2Impl.Keys.Iter(s => Succ[s] = new HashSet<string>()); + name2Impl.Keys.Iter(s => Pred[s] = new HashSet<string>()); + + foreach(var impl in name2Impl.Keys) { + Succ[impl] = new HashSet<string>(); + impl2functionsAsserted[impl].Iter(f => + function2implAssumed[f].Iter(succ => + { + Succ[impl].Add(succ); + Pred[succ].Add(impl); + })); + } + + var sccs = new StronglyConnectedComponents<string>(name2Impl.Keys, + new Adjacency<string>(n => Pred[n]), + new Adjacency<string>(n => Succ[n])); + sccs.Compute(); + + // impl -> priority + var impl2Priority = new Dictionary<string, int>(); + int p = 0; + foreach (var scc in sccs) + { + foreach (var impl in scc) + { + impl2Priority.Add(impl, p); + p++; + } + } + + var worklist = new SortedSet<Tuple<int, string>>(); + name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k))); + + while (worklist.Any()) + { + var impl = worklist.First().Item2; + worklist.Remove(worklist.First()); + + var gen = prover.VCExprGen; + var terms = new List<Expr>(); + foreach (var tup in impl2FuncCalls[impl]) + { + var controlVar = tup.Item2; + var exprVars = tup.Item3; + var varList = new List<Expr>(); + exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v)); + + var args = new List<Expr>(); + 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<Variable>(controlVar.InParams.ToArray()), + new Trigger(Token.NoToken, true, new List<Expr> { 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<string>(); + impl2FuncCalls[impl].Iter(tup => envFuncs.Add(tup.Item1)); + envFuncs.Iter(f => PrintFunction(existentialFunctions[f])); + } + + var handler = impl2ErrorHandler[impl].Item1; + var collector = impl2ErrorHandler[impl].Item2; + collector.Reset(impl); + + var start = DateTime.Now; + + prover.Push(); + prover.Assert(gen.Not(vc), true); + prover.FlushAxiomsToTheoremProver(); + prover.Check(); + ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler); + + //prover.BeginCheck(impl, vc, handler); + //ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler); + + var inc = (DateTime.Now - start); + proverTime += inc; + numProverQueries++; + + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString()); + + if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory) + { + // 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<Counterexample>()); + } + + 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<string>(); + deps.Add(impl); + funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f])); + + deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s))); + } + + prover.Pop(); + } + + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2")); + Console.WriteLine("Number of prover queries = " + numProverQueries); + } + + if (CommandLineOptions.Clo.PrintAssignment) + { + // Print the answer + existentialFunctions.Values.Iter(PrintFunction); + } + + return overallOutcome; + } + + + public IEnumerable<Function> GetAssignment() + { + var ret = new List<Function>(); + foreach (var func in existentialFunctions.Values) + { + var invars = new List<Expr>(func.InParams.OfType<Variable>().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<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v))); + function.Body = function2Value[function.Name].Gamma(invars); + function.Emit(tt, 0); + tt.Close(); + } + + public HashSet<string> HandleCounterExample(string impl, Counterexample error) + { + var funcsChanged = new HashSet<string>(); + // Find the failing assert -- need to do a join there + // return the set of functions whose definition has changed + var cex = ExtractState(impl, error); + foreach (var tup in cex) + { + function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2); + funcsChanged.Add(tup.Item1); + } + return funcsChanged; + } + + private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Counterexample error) + { + var lastBlock = error.Trace.Last() as Block; + AssertCmd failingAssert = null; + + CallCounterexample callCounterexample = error as CallCounterexample; + if (callCounterexample != null) + { + Procedure failingProcedure = callCounterexample.FailingCall.Proc; + Requires failingRequires = callCounterexample.FailingRequires; + failingAssert = lastBlock.Cmds.OfType<AssertRequiresCmd>().FirstOrDefault(ac => ac.Requires == failingRequires); + } + ReturnCounterexample returnCounterexample = error as ReturnCounterexample; + if (returnCounterexample != null) + { + Ensures failingEnsures = returnCounterexample.FailingEnsures; + failingAssert = lastBlock.Cmds.OfType<AssertEnsuresCmd>().FirstOrDefault(ac => ac.Ensures == failingEnsures); + } + AssertCounterexample assertCounterexample = error as AssertCounterexample; + if (assertCounterexample != null) + { + failingAssert = lastBlock.Cmds.OfType<AssertCmd>().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert); + } + + Debug.Assert(failingAssert != null); + return ExtractState(impl, failingAssert.Expr, error.Model); + } + + private static int existentialConstCounter = 0; + + private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Expr expr, Model model) + { + var funcsUsed = FunctionCollector.Collect(expr); + + var ret = new List<Tuple<string, List<Model.Element>>>(); + + 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<Model.Element>(); + 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<Expr>(); + tup3.Item3.Args.OfType<Expr>().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<string, Constant>(); + foreach (var f in boundExpr.Dummies.OfType<Variable>()) + 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<Model.Element>(); + foreach (var funcArg in func.Args.OfType<Expr>()) + { + 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; + } + } + + object val; + + try + { + val = prover.Evaluate(arg); + } + catch (ProverInterface.VCExprEvaluationException) + { + Console.WriteLine("AbsHoudni: Error evaluating expression {0}", arg); + throw; + } + + 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<Function> ahFuncs; + + public ExistentialExprModelMassage() + { + ahFuncs = new List<Function>(); + } + + public static Tuple<Expr, List<Function>> 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<Tuple<Function, ExistsExpr>> functionsUsed; + ExistsExpr existentialExpr; + + public FunctionCollector() + { + functionsUsed = new List<Tuple<Function, ExistsExpr>>(); + existentialExpr = null; + } + + public static List<Tuple<Function, ExistsExpr>> 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<Function, ExistsExpr>((node.Fun as FunctionCall).Func, null)); + } + + return base.VisitNAryExpr(node); + } + } + + class AbsHoudiniCounterexampleCollector : VerifierCallback + { + public HashSet<string> funcsChanged; + public string currImpl; + public int numErrors; + public List<Counterexample> errors; + + AbsHoudini container; + + public AbsHoudiniCounterexampleCollector(AbsHoudini container) + { + this.container = container; + Reset(null); + } + + public void Reset(string impl) + { + funcsChanged = new HashSet<string>(); + currImpl = impl; + numErrors = 0; + errors = new List<Counterexample>(); + } + + 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<int, Absy> 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); + + + StripOutermostForall(impl); + //ExtractQuantifiedExprs(impl); + ExtractBoolExprs(impl); + + //CommandLineOptions.Clo.PrintInstrumented = true; + //using (var tt = new TokenTextWriter(Console.Out)) + // impl.Emit(tt, 0); + + // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants + var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys); + var fv = new ReplaceFunctionCalls(existentialFunctionNames); + fv.VisitBlockList(impl.Blocks); + + //using (var tt = new TokenTextWriter(Console.Out)) + // impl.Emit(tt, 0); + + + 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<Variable>(), 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<string>(existentialFunctions.Keys); + foreach (var blk in impl.Blocks) + { + foreach (var acmd in blk.Cmds.OfType<AssertCmd>()) + { + var ret = ExtractQuantifiers.Extract(acmd.Expr, funcs); + acmd.Expr = ret.Item1; + impl.LocVars.AddRange(ret.Item2); + } + } + } + + // convert "foo(... e ...) to: + // (p iff e) ==> foo(... p ...) + // where p is a fresh boolean variable, foo is an existential constant + // and e is a Boolean-typed argument of foo + private void ExtractBoolExprs(Implementation impl) + { + var funcs = new HashSet<string>(existentialFunctions.Keys); + foreach (var blk in impl.Blocks) + { + foreach (var acmd in blk.Cmds.OfType<AssertCmd>()) + { + var ret = ExtractBoolArgs.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<string>(existentialFunctions.Keys); + foreach (var blk in impl.Blocks) + { + foreach (var acmd in blk.Cmds.OfType<AssertCmd>()) + { + 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<Implementation> oldCallGraph = callGraph; + callGraph = new Graph<Implementation>(); + foreach (Implementation impl in oldCallGraph.Nodes) + { + callGraph.AddSource(impl); + } + foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) + { + callGraph.AddEdge(edge.Item1, edge.Item2); + } + int count = CommandLineOptions.Clo.InlineDepth; + while (count > 0) + { + foreach (Implementation impl in oldCallGraph.Nodes) + { + List<Implementation> newNodes = new List<Implementation>(); + foreach (Implementation succ in callGraph.Successors(impl)) + { + newNodes.AddRange(oldCallGraph.Successors(succ)); + } + foreach (Implementation newNode in newNodes) + { + callGraph.AddEdge(impl, newNode); + } + } + count--; + } + } + + private Graph<Implementation> BuildCallGraph() + { + Graph<Implementation> callGraph = new Graph<Implementation>(); + Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>(); + foreach (var proc in program.Procedures) + { + procToImpls[proc] = new HashSet<Implementation>(); + } + 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<string> inlinedFunctionsStack; + + public InlineFunctionCalls() + { + inlinedFunctionsStack = new Stack<string>(); + } + + 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<Variable, Expr>(); + 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<Tuple<string, Function, NAryExpr>> functionsUsed; + public List<Function> boolConstants; + + public HashSet<string> functionsAssumed; + public HashSet<string> functionsAsserted; + HashSet<string> functionsToReplace; + + private bool inAssume; + private bool inAssert; + private bool inFunction; + private List<Dictionary<string, Variable>> boundVars; + private static int IdCounter = 0; + + public ReplaceFunctionCalls(HashSet<string> functionsToReplace) + { + this.functionsUsed = new List<Tuple<string, Function, NAryExpr>>(); + this.functionsToReplace = functionsToReplace; + this.functionsAsserted = new HashSet<string>(); + this.functionsAssumed = new HashSet<string>(); + this.boolConstants = new List<Function>(); + this.boundVars = new List<Dictionary<string, Variable>>(); + + 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<string, Variable>(); + 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<Variable>(); + 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<Expr>(); + bound.OfType<Variable>().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(... e ...) to: + // (p iff e) ==> foo(... p ...) + // where p is a fresh boolean variable, foo is an existential constant + // and e is a Boolean-typed argument of foo + class ExtractBoolArgs : StandardVisitor + { + static int freshConstCounter = 0; + HashSet<string> existentialFunctions; + HashSet<Constant> newConstants; + + private ExtractBoolArgs(HashSet<string> existentialFunctions) + { + this.existentialFunctions = existentialFunctions; + this.newConstants = new HashSet<Constant>(); + } + + public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> existentialFunctions) + { + var eq = new ExtractBoolArgs(existentialFunctions); + expr = eq.VisitExpr(expr); + return Tuple.Create(expr, eq.newConstants.AsEnumerable()); + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName)) + { + var constants = new Dictionary<Constant, Expr>(); + for (int i = 0; i < node.Args.Count; i++) + { + if (node.Args[i].Type == Type.Bool) + { + var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, + "boolArg@const" + freshConstCounter, Microsoft.Boogie.Type.Bool), false); + freshConstCounter++; + constants.Add(constant, node.Args[i]); + node.Args[i] = Expr.Ident(constant); + } + } + + newConstants.UnionWith(constants.Keys); + + Expr ret = Expr.True; + foreach (var tup in constants) + { + ret = Expr.And(ret, Expr.Eq(Expr.Ident(tup.Key), tup.Value)); + } + return Expr.Imp(ret, node); + } + + return base.VisitNAryExpr(node); + } + } + + + // 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<string> existentialFunctions; + bool insideExistential; + Dictionary<Constant, Expr> newConstants; + + private ExtractQuantifiers(HashSet<string> existentialFunctions) + { + this.existentialFunctions = existentialFunctions; + insideExistential = false; + newConstants = new Dictionary<Constant, Expr>(); + } + + public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> 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<string> existentialFunctions; + Dictionary<string, LocalVariable> subst; + List<LocalVariable> LocalsToAdd; + + private StripQuantifiers(HashSet<string> existentialFunctions) + { + this.existentialFunctions = existentialFunctions; + insideQuantifier = 0; + searchExistentialFunction = false; + foundExistentialFunction = false; + LocalsToAdd = new List<LocalVariable>(); + subst = null; + } + + public static Tuple<Expr,List<LocalVariable>> Run(Expr expr, HashSet<string> 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<string, LocalVariable>(); + foreach (var bv in node.Dummies.OfType<Variable>()) + { + 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<Model.Element> states) + { + Debug.Assert(states.Count == 1); + var state = states[0] as Model.Integer; + if (state == null) + throw new AbsHoudiniInternalError("Incorrect type, expected int"); + var intval = state.AsInt(); + + if (isBottom) + { + return new Intervals(intval, intval, 1); + } + + if(intval >= lower && intval <= upper) + return this; + + if (nJoin > maxJoin) + { + // widen + if (intval > upper) + return new Intervals(lower, Int32.MaxValue, 1); + if(intval < lower) + return new Intervals(Int32.MinValue, upper, 1); + + Debug.Assert(false); + } + + if (intval > upper) + return new Intervals(lower, intval, nJoin + 1); + if (intval < lower) + return new Intervals(intval, upper, nJoin + 1); + + Debug.Assert(false); + return null; + } + + public Expr Gamma(List<Expr> vars) + { + Debug.Assert(vars.Count == 1); + var v = vars[0]; + if (isBottom) return Expr.False; + Expr ret = Expr.True; + if (lower != Int32.MinValue) + ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower))); + if (upper != Int32.MaxValue) + ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper))); + return ret; + } + + public bool TypeCheck(List<Type> 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 PredicateAbsFullElem : PredicateAbsElem + { + public PredicateAbsFullElem() + : base(1000) + { } + } + + 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 + { + HashSet<int> pos; + HashSet<int> neg; + bool isTrue; + + public Disjunct() + { + isTrue = true; + pos = new HashSet<int>(); + neg = new HashSet<int>(); + } + + public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg, int bound) + { + this.isTrue = false; + this.pos = new HashSet<int>(pos); + this.neg = new HashSet<int>(neg); + if (this.pos.Overlaps(this.neg)) + { + this.isTrue = true; + this.pos = new HashSet<int>(); + this.neg = new HashSet<int>(); + } + if (this.pos.Count + this.neg.Count > bound) + { + // Set to true + this.isTrue = true; + this.pos = new HashSet<int>(); + this.neg = new HashSet<int>(); + } + + } + + public Disjunct OR(Disjunct that, int bound) + { + if (isTrue) + return this; + if (that.isTrue) + return that; + + return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg), bound); + } + + public bool Implies(Disjunct that) + { + if (isTrue) return that.isTrue; + if (that.isTrue) return true; + + return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg); + } + + public Expr Gamma(List<Expr> vars) + { + if (isTrue) return Expr.True; + Expr ret = Expr.False; + pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i])); + neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i]))); + return ret; + } + } + + // Conjunction of Disjuncts + List<Disjunct> conjuncts; + int DisjunctBound; + bool isFalse; + + public PredicateAbsElem() + { + this.conjuncts = new List<Disjunct>(); + this.isFalse = true; + this.DisjunctBound = 3; + } + + public PredicateAbsElem(int bound) + { + this.conjuncts = new List<Disjunct>(); + this.isFalse = true; + this.DisjunctBound = bound; + } + + public IAbstractDomain Bottom() + { + return new PredicateAbsElem(DisjunctBound); + } + + public IAbstractDomain MakeTop(out bool changed) + { + if (conjuncts.Count == 0) + { + changed = false; + return this; + } + changed = true; + var ret = new PredicateAbsElem(DisjunctBound); + ret.isFalse = false; + return ret; + } + + public IAbstractDomain Join(List<Model.Element> state) + { + if (state.Any(me => !(me is Model.Boolean))) + throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool"); + + // quick return if this == true + if (!this.isFalse && conjuncts.Count == 0) + return this; + + var ret = new PredicateAbsElem(DisjunctBound); + 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[] { }, DisjunctBound); + else d = new Disjunct(new int[] { }, new int[] { i }, DisjunctBound); + + if (isFalse) + ret.AddDisjunct(d); + else + { + conjuncts.Iter(c => ret.AddDisjunct(c.OR(d, DisjunctBound))); + } + } + + return ret; + + } + + public Expr Gamma(List<Expr> vars) + { + if (isFalse) return Expr.False; + Expr ret = Expr.True; + + foreach (var c in conjuncts) + { + ret = ExprExt.AndSimp(ret, c.Gamma(vars)); + } + + return ret; + } + + public bool TypeCheck(List<Type> 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<Model.Element> states) + { + Debug.Assert(states.Count == 1); + var state = states[0]; + + if (isTop) return this; + + if (state is Model.Boolean) + { + if ((state as Model.Boolean).Value) + return GetExtObj(); + } + + return GetTop(); + } + + public Expr Gamma(List<Expr> vars) + { + Debug.Assert(vars.Count == 1); + var v = vars[0]; + if (isBottom) return Expr.False; + if (isTop) return Expr.True; + return v; + } + + public bool TypeCheck(List<Type> 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<Model.Element> 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<Expr> 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<Expr> { 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<Type> 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<HashSet<int>> equalities; + + public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq) + { + this.isBottom = isBottom; + this.equalities = eq; + } + + public static IAbstractDomain GetBottom() + { + return new EqualitiesDomain(true, new List<HashSet<int>>()); + } + + 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<HashSet<int>>()); + } + + IAbstractDomain IAbstractDomain.Join(List<Model.Element> state) + { + // find the guys that are equal + var eq = new List<HashSet<int>>(); + 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<int>(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<int>(m2[i].Intersect(m1[i])); + + + // map from representative to set + var repToSet = new Dictionary<int, HashSet<int>>(); + + 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<HashSet<int>>(); + repToSet.Values.Iter(s => ret.Add(s)); + + return new EqualitiesDomain(false, ret); + } + + Expr IAbstractDomain.Gamma(List<Expr> 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<Type> 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<int>[] GetMap(List<HashSet<int>> eq, int n) + { + var ret = new HashSet<int>[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<Model.Element> 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<Expr> 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<Type> 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<Model.Element> states) + { + Debug.Assert(states.Count == 1); + var state = states[0]; + ConstantProp that = null; + + if (state is Model.Integer) + { + that = GetExtObj((state as Model.Integer).AsInt()); + } + else if (state is Model.Boolean) + { + that = GetExtObj((state as Model.Boolean).Value); + } + else + { + throw new AbsHoudiniInternalError("Illegal type " + state.GetType().ToString()); + } + + return Join(that); + } + + public Expr Gamma(List<Expr> vars) + { + Debug.Assert(vars.Count == 1); + var v = vars[0]; + if (isBottom) return Expr.False; + if (isTop) return Expr.True; + if (val is int) + return Expr.Eq(v, Expr.Literal((int)val)); + if (val is bool && (bool)val) + return v; + if (val is bool && !(bool)val) + return Expr.Not(v); + + return null; + } + + public bool TypeCheck(List<Type> 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<T> : IAbstractDomain where T : class, IAbstractDomain + { + bool isBottom; + int numVars; + List<T> varVal; + T underlyingInstance; + + public IndependentAttribute() + { + isBottom = true; + numVars = 0; + varVal = new List<T>(); + underlyingInstance = null; + } + + public IAbstractDomain Bottom() + { + return new IndependentAttribute<T>(); + } + + public IAbstractDomain MakeTop(out bool changed) + { + var mt = new Func<IAbstractDomain>(() => + { + var ret = new IndependentAttribute<T>(); + ret.isBottom = true; + ret.numVars = numVars; + ret.underlyingInstance = underlyingInstance; + ret.varVal = new List<T>(); + 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<Model.Element> state) + { + SetUnderlyingInstance(); + + if (!isBottom && numVars != state.Count) + { + throw new AbsHoudiniInternalError( + string.Format("Got illegal number of arguments ({0}), expected {1}", state.Count, numVars)); + } + + var ret = new IndependentAttribute<T>(); + ret.isBottom = false; + ret.numVars = state.Count; + for(int i = 0; i < state.Count; i++) + { + var sl = new List<Model.Element>(); + sl.Add(state[i]); + T prev = isBottom ? underlyingInstance.Bottom() as T : varVal[i]; + ret.varVal.Add(prev.Join(sl) as T); + } + + return ret; + } + + public Expr Gamma(List<Expr> vars) + { + if (isBottom) return Expr.False; + if (numVars != vars.Count) + throw new AbsHoudiniInternalError( + string.Format("Got illegal number of arguments ({0}), expected {1}", vars.Count, numVars)); + + Expr ret = Expr.True; + for (int i = 0; i < numVars; i++) + { + var sl = new List<Expr>(); sl.Add(vars[i]); + ret = Expr.And(ret, varVal[i].Gamma(sl)); + } + + return ret; + } + + private void SetUnderlyingInstance() + { + if (underlyingInstance != null) return; + var tt = typeof(T); + underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T; + } + + public bool TypeCheck(List<Type> argTypes, out string msg) + { + SetUnderlyingInstance(); + + msg = ""; + foreach(var t in argTypes) + { + if(!underlyingInstance.TypeCheck(new List<Type>(new Type[] { t }), out msg)) + return false; + } + return true; + } + } + + public class AbstractDomainFactory + { + // Type name -> Instance + private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>(); + private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>(); + + // bitvector operations + public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>(); + + 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<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] { + 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("PredicateAbsFull", new PredicateAbsFullElem() 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<HoudiniConst>() as IAbstractDomain), + System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>() as IAbstractDomain), + System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>() as IAbstractDomain), + System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() 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<Model.Element> state); + Expr Gamma(List<Expr> vars); + bool TypeCheck(List<Type> argTypes, out string msg); + } + + public class AbstractHoudini + { + // Input Program + Program program; + // Impl -> VC + Dictionary<string, VCExpr> impl2VC; + // Impl -> Vars at end of the impl + Dictionary<string, List<VCExpr>> impl2EndStateVars; + // Impl -> (callee,summary pred) + Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>> impl2CalleeSummaries; + // pointer to summary class + ISummaryElement summaryClass; + // impl -> summary + Dictionary<string, ISummaryElement> impl2Summary; + // name -> impl + Dictionary<string, Implementation> 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<string, VCExpr>(); + this.impl2EndStateVars = new Dictionary<string, List<VCExpr>>(); + this.impl2CalleeSummaries = new Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>>(); + this.impl2Summary = new Dictionary<string, ISummaryElement>(); + this.name2Impl = SimpleUtil.nameImplMapping(program); + + if (CommandLineOptions.Clo.ProverKillTime > 0) + CommandLineOptions.Clo.ProverOptions = CommandLineOptions.Clo.ProverOptions.Concat1(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); + + this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>()); + 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<Implementation, HashSet<Implementation>>(); + var Pred = new Dictionary<Implementation, HashSet<Implementation>>(); + name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet<Implementation>())); + name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>())); + + foreach (var impl in program.Implementations) + { + foreach (var blk in impl.Blocks) + { + foreach (var cmd in blk.Cmds.OfType<CallCmd>()) + { + if (!name2Impl.ContainsKey(cmd.callee)) continue; + Succ[impl].Add(name2Impl[cmd.callee]); + Pred[name2Impl[cmd.callee]].Add(impl); + } + } + } + + // Build SCC + var sccs = new StronglyConnectedComponents<Implementation>(name2Impl.Values, + new Adjacency<Implementation>(n => Pred[n]), + new Adjacency<Implementation>(n => Succ[n])); + sccs.Compute(); + + // impl -> priority + var impl2Priority = new Dictionary<string, int>(); + int p = 0; + foreach (var scc in sccs) + { + foreach (var impl in scc) + { + impl2Priority.Add(impl.Name, p); + p++; + } + } + + + Inline(); + + #region Witness generation setup + // Create a copy of the program + var copy = new Dictionary<string, Implementation>(); + 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<Variable>(impl.LocVars), new List<Block>()); + 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<Tuple<int, Implementation>>(); + 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<Tuple<int, string>>(); + 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<string> GetPredicates() + { + var ret = new HashSet<string>(); + 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<string, Expr>(); + foreach (var g in program.GlobalVariables) + vars.Add(g.Name, Expr.Ident(g)); + foreach (var v in proc.InParams.OfType<Variable>()) + vars.Add(v.Name, Expr.Ident(v)); + foreach (var v in proc.OutParams.OfType<Variable>()) + 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<string, Implementation> copy) + { + if (WitnessFile == null) + return; + + foreach (var proc in program.Procedures) + { + var nensures = new List<Ensures>(); + proc.Ensures.OfType<Ensures>() + .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<Declaration>(copy.Values); + decls.AddRange(program.TopLevelDeclarations.Where(decl => !(decl is Implementation))); + program.TopLevelDeclarations = decls; + var name2Proc = new Dictionary<string, Procedure>(); + 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<string, Expr>(s => null), new Func<string, Expr>(s => null))); + ens.Attributes = new QKeyValue(Token.NoToken, "inferred", new List<object>(), 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<AssumeCmd>()) + { + 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<string, Expr>(); + var always = new Dictionary<string, Expr>(); + 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<Variable>()) + { + always.Add(v.Name, expr.Args[i]); + i++; + } + foreach (var v in callee.OutParams.OfType<Variable>()) + { + always.Add(v.Name, expr.Args[i]); + i++; + } + foreach (var ie in name2Proc[calleeName].Modifies.OfType<IdentifierExpr>()) + { + 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<Implementation> oldCallGraph = callGraph; + callGraph = new Graph<Implementation>(); + foreach (Implementation impl in oldCallGraph.Nodes) + { + callGraph.AddSource(impl); + } + foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) + { + callGraph.AddEdge(edge.Item1, edge.Item2); + } + int count = CommandLineOptions.Clo.InlineDepth; + while (count > 0) + { + foreach (Implementation impl in oldCallGraph.Nodes) + { + List<Implementation> newNodes = new List<Implementation>(); + foreach (Implementation succ in callGraph.Successors(impl)) + { + newNodes.AddRange(oldCallGraph.Successors(succ)); + } + foreach (Implementation newNode in newNodes) + { + callGraph.AddEdge(impl, newNode); + } + } + count--; + } + } + + private Graph<Implementation> BuildCallGraph() + { + Graph<Implementation> callGraph = new Graph<Implementation>(); + Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>(); + foreach (var proc in program.Procedures) + { + procToImpls[proc] = new HashSet<Implementation>(); + } + 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<string, VCExpr> GetVarMapping(Implementation impl, VCExprNAry summaryPred) + { + var ret = new Dictionary<string, VCExpr>(); + + 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<Variable>().Concat( + impl.OutParams.OfType<Variable>().Concat( + impl.Proc.Modifies.OfType<IdentifierExpr>().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<string, Model.Element> CollectState(Implementation impl) + { + var ret = new Dictionary<string, Model.Element>(); + + 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<Variable>().Concat( + impl.OutParams.OfType<Variable>().Concat( + impl.Proc.Modifies.OfType<IdentifierExpr>().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<Variable> functionInterfaceVars = new List<Variable>(); + 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<Expr> exprs = new List<Expr>(); + 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<object>(), null))); + } + + private void GenVC(Implementation impl) + { + ModelViewInfo mvInfo; + Dictionary<int, Absy> 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<VCExpr>()); + var found = false; + var assertId = -1; + foreach (var blk in impl.Blocks) + { + foreach (var cmd in blk.Cmds.OfType<AssertCmd>()) + { + 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<Expr>() + .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<Variable>(), 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<Tuple<string, bool, VCExprVar, VCExprNAry>>()); + visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup)); + } + } + + public interface ISummaryElement + { + ISummaryElement Copy(); + ISummaryElement GetFlaseSummary(Program program, Implementation impl); + void Join(Dictionary<string, Model.Element> state, Model model); + VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen); + Expr GetSummaryExpr(Func<string, Expr> always, Func<string, Expr> 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<string, HashSet<int>> val; + // set of vars + HashSet<Variable> vars; + + public static readonly int MAX = 3; + + public ConstantVal() + { + // this is just a place holder + val = new Dictionary<string, HashSet<int>>(); + vars = new HashSet<Variable>(); + } + + private ConstantVal(Program program, Implementation impl) + { + this.program = program; + this.impl = impl; + this.val = new Dictionary<string, HashSet<int>>(); + + vars = new HashSet<Variable>(); + impl.Proc.Modifies + .OfType<IdentifierExpr>() + .Select(ie => ie.Decl) + .Where(v => v.TypedIdent.Type.IsInt) + .Iter(v => vars.Add(v)); + impl.OutParams.OfType<Variable>() + .Where(v => v.TypedIdent.Type.IsInt) + .Iter(v => vars.Add(v)); + + vars.Iter(v => val.Add(v.Name, null)); + } + + + public void Join(Dictionary<string, Model.Element> 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<int>(); + val[v].Add(newv); + } + else if(oldv.Count > 0) + { + val[v].Add(newv); + if (val[v].Count > MAX) + val[v] = new HashSet<int>(); + } + + } + } + + public VCExpr GetSummaryExpr(Dictionary<string, VCExpr> 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<string, Expr> always, Func<string, Expr> 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<string, List<NamedExpr>> PrePreds { get; private set; } + public static Dictionary<string, HashSet<int>> PosPrePreds { get; private set; } + public static Dictionary<string, List<NamedExpr>> PostPreds { get; private set; } + public static Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>> UpperCandidates; + private static HashSet<string> boolConstants; + // {proc, pred-pair} -> polariry + public static HashSet<Tuple<string, int, int, bool, bool>> unsatPrePredPairs; + public static HashSet<Tuple<string, int, int, bool, bool>> 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<string, List<NamedExpr>>(); + PostPreds = new Dictionary<string, List<NamedExpr>>(); + PosPrePreds = new Dictionary<string, HashSet<int>>(); + + boolConstants = new HashSet<string>(); + UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>(); + + 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<NamedExpr>(); + var postT = new List<NamedExpr>(); + var posPreT = new HashSet<int>(); + var tempP = new HashSet<Procedure>(); + foreach (var proc in + program.Procedures + .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template"))) + { + tempP.Add(proc); + foreach (var ens in proc.Ensures.OfType<Ensures>()) + { + 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<string, List<Expr>>(); + + foreach (var impl in program.Implementations) + { + PrePreds.Add(impl.Name, new List<NamedExpr>()); + PostPreds.Add(impl.Name, new List<NamedExpr>()); + PosPrePreds.Add(impl.Name, new HashSet<int>()); + + // 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<Ensures>(); + foreach (var ens in impl.Proc.Ensures.OfType<Ensures>()) + { + 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<Expr>()); + 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<string, int>(); + 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<PredicateAbsDisjunct>()); + 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<PredicateAbsDisjunct>()); + 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<PredicateAbsDisjunct, Expr> 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<int>(); + var neg = new HashSet<int>(); + + 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<PredicateAbsConjunct>(); + conjls.Add(conj); + + return Tuple.Create(new PredicateAbsDisjunct(conjls, procName), postExpr); + } + + // blah && blah ==> {blah, blah} + static IEnumerable<Expr> DecomposeOuterAnd(Expr expr) + { + var ret = new List<Expr>(); + + 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<string, Model.Element> 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<string, Model.Element> 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<string, VCExpr> 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<Tuple<string, int, int, bool, bool>>(); + unsatPostPredPairs = new HashSet<Tuple<string, int, int, bool, bool>>(); + + var cachePos = new HashSet<Tuple<string, string>>(); + var cacheNeg = new HashSet<Tuple<string, string>>(); + var record = new Action<object, string, int, int, bool, bool>( + (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<Dictionary<string, List<NamedExpr>>>(); + 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<Variable>(); + var setb = new HashSet<Variable>(); + 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<string, VCExpr>(); + 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<Tuple<Variable, Expr>> literals; + bool inOld; + + public GatherLiterals() + { + literals = new List<Tuple<Variable, Expr>>(); + 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<string, Expr> always, Func<string, Expr> 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<string, VCExpr> 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<string> GetPredicates(Program program, VCExpressionGenerator gen, ProverInterface prover) + { + var ret = new HashSet<string>(); + 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<Requires>().Where(req => req.Free)) + { + freeSummary = Expr.And(freeSummary, MakeOld(req.Condition)); + } + foreach (var ens in proc.Ensures.OfType<Ensures>().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<string, Model.Element> 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<int>(); + 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<string, VCExpr> 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<string, Expr> always, Func<string, Expr> 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<PredicateAbsConjunct> 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<PredicateAbsConjunct>(); + } + + public PredicateAbsDisjunct(List<PredicateAbsConjunct> conjuncts, string ProcName) + { + isTrue = false; + this.conjuncts = conjuncts; + this.ProcName = ProcName; + } + + // Disjunct of singleton conjuncts + public PredicateAbsDisjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName) + { + this.ProcName = ProcName; + conjuncts = new List<PredicateAbsConjunct>(); + 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<PredicateAbsConjunct>(); + + 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<PredicateAbsConjunct>(); + 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<PredicateAbsConjunct>(); + 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<PredicateAbsConjunct>(); + 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<int, VCExpr> 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<int, Expr> 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<PredicateAbsConjunct>(); + foreach (var c1 in conjuncts) + { + if (that.conjuncts.Any(c2 => c1.implies(c2))) + continue; + ncon.Add(c1); + } + conjuncts = ncon; + } + + public IEnumerable<PredicateAbsConjunct> GetConjuncts() + { + return conjuncts; + } + + } + + public class PredicateAbsConjunct + { + static int ConjunctBound = 3; + + public bool isFalse { get; private set; } + HashSet<int> posPreds; + HashSet<int> 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<int>(); + negPreds = new HashSet<int>(); + } + } + + // Do this step only once in a while? + private void StrongNormalize() + { + if (isFalse) return; + + var candidates = new List<Tuple<int, bool>>(); + posPreds.Iter(p => candidates.Add(Tuple.Create(p, true))); + negPreds.Iter(p => candidates.Add(Tuple.Create(p, false))); + var drop = new HashSet<int>(); + 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<int>(); + negPreds = new HashSet<int>(); + 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<int>(); + negPreds = new HashSet<int>(); + 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<int>(), ProcName); + else + return new PredicateAbsConjunct(new HashSet<int>(), new int[] { v }, ProcName); + } + + public PredicateAbsConjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName) + { + isFalse = false; + posPreds = new HashSet<int>(pos); + negPreds = new HashSet<int>(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<int, VCExpr> 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<int, Expr> 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<bool> + { + public List<Tuple<string, bool, VCExprVar, VCExprNAry>> summaryPreds; + int assertId; + private static int CounterId = 0; + + public FindSummaryPred(VCExpressionGenerator gen, int assertId) + : base(gen) + { + summaryPreds = new List<Tuple<string, bool, VCExprVar, VCExprNAry>>(); + this.assertId = assertId; + } + + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, + List<VCExpr/*!*/>/*!*/ newSubExprs, + // has any of the subexpressions changed? + bool changed, + bool arg) + { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + VCExpr ret; + if (changed) + ret = Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + else + ret = originalNode; + + VCExprNAry retnary = ret as VCExprNAry; + if (retnary == null) return ret; + var op = retnary.Op as VCExprBoogieFunctionOp; + + if (op == null) + { + 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<bool> + { + public List<Tuple<string, VCExprVar, VCExprNAry>> funcCalls; + private HashSet<string> existentialFunctions; + private static int CounterId = 0; + + public FindExistentialFunctions(VCExpressionGenerator gen, HashSet<string> existentialFunctions) + : base(gen) + { + funcCalls = new List<Tuple<string, VCExprVar, VCExprNAry>>(); + this.existentialFunctions = existentialFunctions; + } + + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, + List<VCExpr/*!*/>/*!*/ newSubExprs, + // has any of the subexpressions changed? + bool changed, + bool arg) + { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + VCExpr ret; + if (changed) + ret = Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + else + ret = originalNode; + + VCExprNAry retnary = ret as VCExprNAry; + if (retnary == null) return ret; + var op = retnary.Op as VCExprBoogieFunctionOp; + if (op == null) return ret; + + string calleeName = op.Func.Name; + + if (!existentialFunctions.Contains(calleeName)) + return ret; + + var controlConst = Gen.Variable("AbsHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool); + CounterId++; + + funcCalls.Add(Tuple.Create(calleeName, controlConst, retnary)); + + return controlConst; + } + + } + + class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler + { + public Model model; + + public AbstractHoudiniErrorReporter() + { + model = null; + } + + public override void OnModel(IList<string> 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<string, Implementation> nameImplMapping(Program p) + { + var m = new Dictionary<string, Implementation>(); + 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; + } + } + +} |