From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Houdini/Checker.cs | 911 +++++++++++++++++++++++----------------------- 1 file changed, 456 insertions(+), 455 deletions(-) (limited to 'Source/Houdini/Checker.cs') diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 30056d99..73842019 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -1,456 +1,457 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Diagnostics.Contracts; -using System.Collections.Generic; -using Microsoft.Boogie; -using Microsoft.Boogie.VCExprAST; -using Microsoft.Basetypes; -using System.Collections; -using System.IO; -using System.Threading; -using VC; -using System.Linq; - -namespace Microsoft.Boogie.Houdini { - public class ExistentialConstantCollector : ReadOnlyVisitor { - public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out ExistentialConstantCollector collector) - { - collector = new ExistentialConstantCollector(houdini); - collector.impl = impl; - collector.VisitImplementation(impl); - } - - private ExistentialConstantCollector(Houdini houdini) { - this.houdini = houdini; - this.houdiniAssertConstants = new HashSet(); - this.houdiniAssumeConstants = new HashSet(); - - this.explainNegative = new HashSet(); - this.explainPositive = new HashSet(); - this.constToControl = new Dictionary>(); - } - private Houdini houdini; - public HashSet houdiniAssertConstants; - public HashSet houdiniAssumeConstants; - - // Explain Houdini stuff - public HashSet explainPositive; - public HashSet explainNegative; - public Dictionary> constToControl; - Implementation impl; - - public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { - AddHoudiniConstant(node); - return base.VisitAssertRequiresCmd(node); - } - public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { - AddHoudiniConstant(node); - return base.VisitAssertEnsuresCmd(node); - } - public override Cmd VisitAssertCmd(AssertCmd node) { - AddHoudiniConstant(node); - return base.VisitAssertCmd(node); - } - public override Cmd VisitAssumeCmd(AssumeCmd node) { - AddHoudiniConstant(node); - return base.VisitAssumeCmd(node); - } - private void AddHoudiniConstant(AssertCmd assertCmd) - { - Variable houdiniConstant; - if (houdini.MatchCandidate(assertCmd.Expr, out houdiniConstant)) - houdiniAssertConstants.Add(houdiniConstant); - - if (houdiniConstant != null && CommandLineOptions.Clo.ExplainHoudini && !constToControl.ContainsKey(houdiniConstant.Name)) - { - // For each houdini constant c, create two more constants c_pos and c_neg. - // Then change the asserted condition (c ==> \phi) to - // (c ==> (c_pos && (\phi || \not c_neg)) - var control = createNewExplainConstants(houdiniConstant); - assertCmd.Expr = houdini.InsertCandidateControl(assertCmd.Expr, control.Item1, control.Item2); - explainPositive.Add(control.Item1); - explainNegative.Add(control.Item2); - constToControl.Add(houdiniConstant.Name, control); - } - } - private void AddHoudiniConstant(AssumeCmd assumeCmd) - { - Variable houdiniConstant; - if (houdini.MatchCandidate(assumeCmd.Expr, out houdiniConstant)) - houdiniAssumeConstants.Add(houdiniConstant); - } - private Tuple createNewExplainConstants(Variable v) - { - Contract.Assert(impl != null); - Contract.Assert(CommandLineOptions.Clo.ExplainHoudini); - Variable v1 = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}_{2}", v.Name, impl.Name, "pos"), Microsoft.Boogie.BasicType.Bool)); - Variable v2 = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}_{2}", v.Name, impl.Name, "neg"), Microsoft.Boogie.BasicType.Bool)); - - return Tuple.Create(v1, v2); - } - } - - - - public class HoudiniSession { - - public class HoudiniStatistics { - public double proverTime = 0; - public int numProverQueries = 0; - public double unsatCoreProverTime = 0; - public int numUnsatCoreProverQueries = 0; - public int numUnsatCorePrunings = 0; - } - - public string descriptiveName; - public HoudiniStatistics stats; - private VCExpr conjecture; - private ProverInterface.ErrorHandler handler; - ConditionGeneration.CounterexampleCollector collector; - HashSet unsatCoreSet; - HashSet houdiniConstants; - public HashSet houdiniAssertConstants; - private HashSet houdiniAssumeConstants; - - // Extra constants created for ExplainHoudini - private HashSet explainConstantsPositive; - private HashSet explainConstantsNegative; - private Dictionary> constantToControl; - - public bool InUnsatCore(Variable constant) { - if (unsatCoreSet == null) - return true; - if (unsatCoreSet.Contains(constant)) - return true; - stats.numUnsatCorePrunings++; - return false; - } - - public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) { - this.descriptiveName = impl.Name; - this.stats = stats; - collector = new ConditionGeneration.CounterexampleCollector(); - collector.OnProgress("HdnVCGen", 0, 0, 0.0); - - vcgen.ConvertCFG2DAG(impl, taskID: taskID); - ModelViewInfo mvInfo; - var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo); - - ExistentialConstantCollector ecollector; - ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out ecollector); - this.houdiniAssertConstants = ecollector.houdiniAssertConstants; - this.houdiniAssumeConstants = ecollector.houdiniAssumeConstants; - this.explainConstantsNegative = ecollector.explainNegative; - this.explainConstantsPositive = ecollector.explainPositive; - this.constantToControl = ecollector.constToControl; - - houdiniConstants = new HashSet(); - houdiniConstants.UnionWith(houdiniAssertConstants); - houdiniConstants.UnionWith(houdiniAssumeConstants); - - var exprGen = proverInterface.Context.ExprGen; - VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - - Dictionary label2absy; - conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context); - if (!CommandLineOptions.Clo.UseLabels) { - VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); - VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); - conjecture = exprGen.Implies(eqExpr, conjecture); - } - - Macro macro = new Macro(Token.NoToken, descriptiveName, new List(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); - proverInterface.DefineMacro(macro, conjecture); - conjecture = exprGen.Function(macro); - - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { - handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); - } - else { - handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); - } - - } - - private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary currentAssignment) { - ProverContext proverContext = proverInterface.Context; - Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator; - VCExpressionGenerator exprGen = proverInterface.VCExprGen; - - VCExpr expr = VCExpressionGenerator.True; - - foreach (KeyValuePair kv in currentAssignment) { - Variable constant = kv.Key; - VCExprVar exprVar = exprTranslator.LookupVariable(constant); - if (kv.Value) { - expr = exprGen.And(expr, exprVar); - } - else { - expr = exprGen.And(expr, exprGen.Not(exprVar)); - } - } - - if (CommandLineOptions.Clo.ExplainHoudini) - { - // default values for ExplainHoudini control variables - foreach (var constant in explainConstantsNegative.Concat(explainConstantsPositive)) - { - expr = exprGen.And(expr, exprTranslator.LookupVariable(constant)); - } - } - - /* - foreach (Variable constant in this.houdiniConstants) { - VCExprVar exprVar = exprTranslator.LookupVariable(constant); - if (currentAssignment[constant]) { - expr = exprGen.And(expr, exprVar); - } - else { - expr = exprGen.And(expr, exprGen.Not(exprVar)); - } - } - */ - - if(CommandLineOptions.Clo.Trace) { - Console.WriteLine("Houdini assignment axiom: " + expr); - } - - return expr; - } - - public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary assignment, out List errors, int taskID = -1) { - collector.examples.Clear(); - - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Verifying " + descriptiveName); - } - DateTime now = DateTime.UtcNow; - - VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture); - proverInterface.BeginCheck(descriptiveName, vc, handler); - ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, taskID: taskID); - - double queryTime = (DateTime.UtcNow - now).TotalSeconds; - stats.proverTime += queryTime; - stats.numProverQueries++; - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Time taken = " + queryTime); - } - - errors = collector.examples; - return proverOutcome; - } - - // MAXSAT - public void Explain(ProverInterface proverInterface, - Dictionary assignment, Variable refutedConstant) - { - Contract.Assert(CommandLineOptions.Clo.ExplainHoudini); - - collector.examples.Clear(); - - // debugging - houdiniAssertConstants.Iter(v => System.Diagnostics.Debug.Assert(assignment.ContainsKey(v))); - houdiniAssumeConstants.Iter(v => System.Diagnostics.Debug.Assert(assignment.ContainsKey(v))); - Contract.Assert(assignment.ContainsKey(refutedConstant)); - Contract.Assert(houdiniAssertConstants.Contains(refutedConstant)); - - var hardAssumptions = new List(); - var softAssumptions = new List(); - - Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator; - VCExpressionGenerator exprGen = proverInterface.VCExprGen; - var controlExpr = VCExpressionGenerator.True; - - foreach (var tup in assignment) - { - Variable constant = tup.Key; - VCExprVar exprVar = exprTranslator.LookupVariable(constant); - var val = tup.Value; - - if (houdiniAssumeConstants.Contains(constant)) - { - if (tup.Value) - hardAssumptions.Add(exprVar); - else - // Previously removed assumed candidates are the soft constraints - softAssumptions.Add(exprVar); - } - else if (houdiniAssertConstants.Contains(constant)) - { - if (constant == refutedConstant) - hardAssumptions.Add(exprVar); - else - hardAssumptions.Add(exprGen.Not(exprVar)); - } - else - { - if (tup.Value) - hardAssumptions.Add(exprVar); - else - hardAssumptions.Add(exprGen.Not(exprVar)); - } - - // For an asserted condition (c ==> \phi), - // ExplainHoudini's extra control constants (c_pos, c_neg) are used as follows: - // (true, true): "assert \phi" - // (false, _): "assert false" - // (true, false): "assert true" - if (constant != refutedConstant && constantToControl.ContainsKey(constant.Name)) - { - var posControl = constantToControl[constant.Name].Item1; - var negControl = constantToControl[constant.Name].Item2; - - // Handle self-recursion - if (houdiniAssertConstants.Contains(constant) && houdiniAssumeConstants.Contains(constant)) - { - // disable this assert - controlExpr = exprGen.And(controlExpr, exprGen.And(exprTranslator.LookupVariable(posControl), exprGen.Not(exprTranslator.LookupVariable(negControl)))); - } - else - { - // default values for control variables - controlExpr = exprGen.And(controlExpr, exprGen.And(exprTranslator.LookupVariable(posControl), exprTranslator.LookupVariable(negControl))); - } - } - } - - hardAssumptions.Add(exprGen.Not(conjecture)); - - // default values for control variables - Contract.Assert(constantToControl.ContainsKey(refutedConstant.Name)); - var pc = constantToControl[refutedConstant.Name].Item1; - var nc = constantToControl[refutedConstant.Name].Item2; - - var controlExprNoop = exprGen.And(controlExpr, - exprGen.And(exprTranslator.LookupVariable(pc), exprTranslator.LookupVariable(nc))); - - var controlExprFalse = exprGen.And(controlExpr, - exprGen.And(exprGen.Not(exprTranslator.LookupVariable(pc)), exprGen.Not(exprTranslator.LookupVariable(nc)))); - - if (CommandLineOptions.Clo.Trace) - { - Console.WriteLine("Verifying (MaxSat) " + descriptiveName); - } - DateTime now = DateTime.UtcNow; - - var el = CommandLineOptions.Clo.ProverCCLimit; - CommandLineOptions.Clo.ProverCCLimit = 1; - - var outcome = ProverInterface.Outcome.Undetermined; - - do - { - List unsatisfiedSoftAssumptions; - - hardAssumptions.Add(controlExprNoop); - outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, handler); - hardAssumptions.RemoveAt(hardAssumptions.Count - 1); - - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) - break; - - var reason = new HashSet(); - unsatisfiedSoftAssumptions.Iter(i => reason.Add(softAssumptions[i].ToString())); - if (CommandLineOptions.Clo.Trace) - { - Console.Write("Reason for removal of {0}: ", refutedConstant.Name); - reason.Iter(r => Console.Write("{0} ", r)); - Console.WriteLine(); - } - - // Get rid of those constants from the "reason" that can even make - // "assert false" pass - - hardAssumptions.Add(controlExprFalse); - var softAssumptions2 = new List(); - for (int i = 0; i < softAssumptions.Count; i++) - { - if (unsatisfiedSoftAssumptions.Contains(i)) - { - softAssumptions2.Add(softAssumptions[i]); - continue; - } - hardAssumptions.Add(softAssumptions[i]); - } - - var unsatisfiedSoftAssumptions2 = new List(); - outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2, handler); - - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) - break; - - unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString())); - var reason1 = new HashSet(); //these are the reasons for inconsistency - unsatisfiedSoftAssumptions2.Iter(i => reason1.Add(softAssumptions2[i].ToString())); - - if (CommandLineOptions.Clo.Trace) - { - Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name); - reason.Iter(r => Console.Write("{0} ", r)); - Console.WriteLine(); - } - foreach (var r in reason) - { - Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName); - } - //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0) - foreach (var r in reason1) - { - Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];", refutedConstant.Name, r, descriptiveName); - } - } while (false); - - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) - { - Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", descriptiveName); - } - - CommandLineOptions.Clo.ProverCCLimit = el; - - double queryTime = (DateTime.UtcNow - now).TotalSeconds; - stats.proverTime += queryTime; - stats.numProverQueries++; - if (CommandLineOptions.Clo.Trace) - { - Console.WriteLine("Time taken = " + queryTime); - } - } - - public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary assignment) - { - DateTime now = DateTime.UtcNow; - - Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator; - proverInterface.Push(); - proverInterface.Assert(conjecture, false); - foreach (var v in assignment.Keys) { - if (assignment[v]) continue; - proverInterface.Assert(exprTranslator.LookupVariable(v), false); - } - List assumptionVars = new List(); - List assumptionExprs = new List(); - foreach (var v in assignment.Keys) { - if (!assignment[v]) continue; - assumptionVars.Add(v); - assumptionExprs.Add(exprTranslator.LookupVariable(v)); - } - List unsatCore; - ProverInterface.Outcome tmp = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler); - System.Diagnostics.Debug.Assert(tmp == ProverInterface.Outcome.Valid); - unsatCoreSet = new HashSet(); - foreach (int i in unsatCore) - unsatCoreSet.Add(assumptionVars[i]); - proverInterface.Pop(); - - double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds; - stats.unsatCoreProverTime += unsatCoreQueryTime; - stats.numUnsatCoreProverQueries++; - } - - } +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Diagnostics.Contracts; +using System.Collections.Generic; +using Microsoft.Boogie; +using Microsoft.Boogie.VCExprAST; +using Microsoft.Basetypes; +using System.Collections; +using System.IO; +using System.Threading; +using VC; +using System.Linq; + +namespace Microsoft.Boogie.Houdini { + public class ExistentialConstantCollector : ReadOnlyVisitor { + public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out ExistentialConstantCollector collector) + { + collector = new ExistentialConstantCollector(houdini); + collector.impl = impl; + collector.VisitImplementation(impl); + } + + private ExistentialConstantCollector(Houdini houdini) { + this.houdini = houdini; + this.houdiniAssertConstants = new HashSet(); + this.houdiniAssumeConstants = new HashSet(); + + this.explainNegative = new HashSet(); + this.explainPositive = new HashSet(); + this.constToControl = new Dictionary>(); + } + private Houdini houdini; + public HashSet houdiniAssertConstants; + public HashSet houdiniAssumeConstants; + + // Explain Houdini stuff + public HashSet explainPositive; + public HashSet explainNegative; + public Dictionary> constToControl; + Implementation impl; + + public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertRequiresCmd(node); + } + public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertEnsuresCmd(node); + } + public override Cmd VisitAssertCmd(AssertCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertCmd(node); + } + public override Cmd VisitAssumeCmd(AssumeCmd node) { + AddHoudiniConstant(node); + return base.VisitAssumeCmd(node); + } + private void AddHoudiniConstant(AssertCmd assertCmd) + { + Variable houdiniConstant; + if (houdini.MatchCandidate(assertCmd.Expr, out houdiniConstant)) + houdiniAssertConstants.Add(houdiniConstant); + + if (houdiniConstant != null && CommandLineOptions.Clo.ExplainHoudini && !constToControl.ContainsKey(houdiniConstant.Name)) + { + // For each houdini constant c, create two more constants c_pos and c_neg. + // Then change the asserted condition (c ==> \phi) to + // (c ==> (c_pos && (\phi || \not c_neg)) + var control = createNewExplainConstants(houdiniConstant); + assertCmd.Expr = houdini.InsertCandidateControl(assertCmd.Expr, control.Item1, control.Item2); + explainPositive.Add(control.Item1); + explainNegative.Add(control.Item2); + constToControl.Add(houdiniConstant.Name, control); + } + } + private void AddHoudiniConstant(AssumeCmd assumeCmd) + { + Variable houdiniConstant; + if (houdini.MatchCandidate(assumeCmd.Expr, out houdiniConstant)) + houdiniAssumeConstants.Add(houdiniConstant); + } + private Tuple createNewExplainConstants(Variable v) + { + Contract.Assert(impl != null); + Contract.Assert(CommandLineOptions.Clo.ExplainHoudini); + Variable v1 = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}_{2}", v.Name, impl.Name, "pos"), Microsoft.Boogie.BasicType.Bool)); + Variable v2 = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}_{2}", v.Name, impl.Name, "neg"), Microsoft.Boogie.BasicType.Bool)); + + return Tuple.Create(v1, v2); + } + } + + + + public class HoudiniSession { + + public class HoudiniStatistics { + public double proverTime = 0; + public int numProverQueries = 0; + public double unsatCoreProverTime = 0; + public int numUnsatCoreProverQueries = 0; + public int numUnsatCorePrunings = 0; + } + + public string descriptiveName; + public HoudiniStatistics stats; + private VCExpr conjecture; + private ProverInterface.ErrorHandler handler; + ConditionGeneration.CounterexampleCollector collector; + HashSet unsatCoreSet; + HashSet houdiniConstants; + public HashSet houdiniAssertConstants; + private HashSet houdiniAssumeConstants; + + // Extra constants created for ExplainHoudini + private HashSet explainConstantsPositive; + private HashSet explainConstantsNegative; + private Dictionary> constantToControl; + + public bool InUnsatCore(Variable constant) { + if (unsatCoreSet == null) + return true; + if (unsatCoreSet.Contains(constant)) + return true; + stats.numUnsatCorePrunings++; + return false; + } + + public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) { + this.descriptiveName = impl.Name; + this.stats = stats; + collector = new ConditionGeneration.CounterexampleCollector(); + collector.OnProgress("HdnVCGen", 0, 0, 0.0); + + vcgen.ConvertCFG2DAG(impl, taskID: taskID); + ModelViewInfo mvInfo; + var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo); + + ExistentialConstantCollector ecollector; + ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out ecollector); + this.houdiniAssertConstants = ecollector.houdiniAssertConstants; + this.houdiniAssumeConstants = ecollector.houdiniAssumeConstants; + this.explainConstantsNegative = ecollector.explainNegative; + this.explainConstantsPositive = ecollector.explainPositive; + this.constantToControl = ecollector.constToControl; + + houdiniConstants = new HashSet(); + houdiniConstants.UnionWith(houdiniAssertConstants); + houdiniConstants.UnionWith(houdiniAssumeConstants); + + var exprGen = proverInterface.Context.ExprGen; + VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); + + Dictionary label2absy; + conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context); + if (!CommandLineOptions.Clo.UseLabels) { + VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); + VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))); + conjecture = exprGen.Implies(eqExpr, conjecture); + } + + Macro macro = new Macro(Token.NoToken, descriptiveName, new List(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); + proverInterface.DefineMacro(macro, conjecture); + conjecture = exprGen.Function(macro); + + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { + handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); + } + else { + handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program); + } + + } + + private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary currentAssignment) { + ProverContext proverContext = proverInterface.Context; + Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator; + VCExpressionGenerator exprGen = proverInterface.VCExprGen; + + VCExpr expr = VCExpressionGenerator.True; + + foreach (KeyValuePair kv in currentAssignment) { + Variable constant = kv.Key; + VCExprVar exprVar = exprTranslator.LookupVariable(constant); + if (kv.Value) { + expr = exprGen.And(expr, exprVar); + } + else { + expr = exprGen.And(expr, exprGen.Not(exprVar)); + } + } + + if (CommandLineOptions.Clo.ExplainHoudini) + { + // default values for ExplainHoudini control variables + foreach (var constant in explainConstantsNegative.Concat(explainConstantsPositive)) + { + expr = exprGen.And(expr, exprTranslator.LookupVariable(constant)); + } + } + + /* + foreach (Variable constant in this.houdiniConstants) { + VCExprVar exprVar = exprTranslator.LookupVariable(constant); + if (currentAssignment[constant]) { + expr = exprGen.And(expr, exprVar); + } + else { + expr = exprGen.And(expr, exprGen.Not(exprVar)); + } + } + */ + + if(CommandLineOptions.Clo.Trace) { + Console.WriteLine("Houdini assignment axiom: " + expr); + } + + return expr; + } + + public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary assignment, out List errors, int taskID = -1) { + collector.examples.Clear(); + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Verifying " + descriptiveName); + } + DateTime now = DateTime.UtcNow; + + VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture); + proverInterface.BeginCheck(descriptiveName, vc, handler); + ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, taskID: taskID); + + double queryTime = (DateTime.UtcNow - now).TotalSeconds; + stats.proverTime += queryTime; + stats.numProverQueries++; + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Outcome = " + proverOutcome); + Console.WriteLine("Time taken = " + queryTime); + } + + errors = collector.examples; + return proverOutcome; + } + + // MAXSAT + public void Explain(ProverInterface proverInterface, + Dictionary assignment, Variable refutedConstant) + { + Contract.Assert(CommandLineOptions.Clo.ExplainHoudini); + + collector.examples.Clear(); + + // debugging + houdiniAssertConstants.Iter(v => System.Diagnostics.Debug.Assert(assignment.ContainsKey(v))); + houdiniAssumeConstants.Iter(v => System.Diagnostics.Debug.Assert(assignment.ContainsKey(v))); + Contract.Assert(assignment.ContainsKey(refutedConstant)); + Contract.Assert(houdiniAssertConstants.Contains(refutedConstant)); + + var hardAssumptions = new List(); + var softAssumptions = new List(); + + Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator; + VCExpressionGenerator exprGen = proverInterface.VCExprGen; + var controlExpr = VCExpressionGenerator.True; + + foreach (var tup in assignment) + { + Variable constant = tup.Key; + VCExprVar exprVar = exprTranslator.LookupVariable(constant); + var val = tup.Value; + + if (houdiniAssumeConstants.Contains(constant)) + { + if (tup.Value) + hardAssumptions.Add(exprVar); + else + // Previously removed assumed candidates are the soft constraints + softAssumptions.Add(exprVar); + } + else if (houdiniAssertConstants.Contains(constant)) + { + if (constant == refutedConstant) + hardAssumptions.Add(exprVar); + else + hardAssumptions.Add(exprGen.Not(exprVar)); + } + else + { + if (tup.Value) + hardAssumptions.Add(exprVar); + else + hardAssumptions.Add(exprGen.Not(exprVar)); + } + + // For an asserted condition (c ==> \phi), + // ExplainHoudini's extra control constants (c_pos, c_neg) are used as follows: + // (true, true): "assert \phi" + // (false, _): "assert false" + // (true, false): "assert true" + if (constant != refutedConstant && constantToControl.ContainsKey(constant.Name)) + { + var posControl = constantToControl[constant.Name].Item1; + var negControl = constantToControl[constant.Name].Item2; + + // Handle self-recursion + if (houdiniAssertConstants.Contains(constant) && houdiniAssumeConstants.Contains(constant)) + { + // disable this assert + controlExpr = exprGen.And(controlExpr, exprGen.And(exprTranslator.LookupVariable(posControl), exprGen.Not(exprTranslator.LookupVariable(negControl)))); + } + else + { + // default values for control variables + controlExpr = exprGen.And(controlExpr, exprGen.And(exprTranslator.LookupVariable(posControl), exprTranslator.LookupVariable(negControl))); + } + } + } + + hardAssumptions.Add(exprGen.Not(conjecture)); + + // default values for control variables + Contract.Assert(constantToControl.ContainsKey(refutedConstant.Name)); + var pc = constantToControl[refutedConstant.Name].Item1; + var nc = constantToControl[refutedConstant.Name].Item2; + + var controlExprNoop = exprGen.And(controlExpr, + exprGen.And(exprTranslator.LookupVariable(pc), exprTranslator.LookupVariable(nc))); + + var controlExprFalse = exprGen.And(controlExpr, + exprGen.And(exprGen.Not(exprTranslator.LookupVariable(pc)), exprGen.Not(exprTranslator.LookupVariable(nc)))); + + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Verifying (MaxSat) " + descriptiveName); + } + DateTime now = DateTime.UtcNow; + + var el = CommandLineOptions.Clo.ProverCCLimit; + CommandLineOptions.Clo.ProverCCLimit = 1; + + var outcome = ProverInterface.Outcome.Undetermined; + + do + { + List unsatisfiedSoftAssumptions; + + hardAssumptions.Add(controlExprNoop); + outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, handler); + hardAssumptions.RemoveAt(hardAssumptions.Count - 1); + + if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) + break; + + var reason = new HashSet(); + unsatisfiedSoftAssumptions.Iter(i => reason.Add(softAssumptions[i].ToString())); + if (CommandLineOptions.Clo.Trace) + { + Console.Write("Reason for removal of {0}: ", refutedConstant.Name); + reason.Iter(r => Console.Write("{0} ", r)); + Console.WriteLine(); + } + + // Get rid of those constants from the "reason" that can even make + // "assert false" pass + + hardAssumptions.Add(controlExprFalse); + var softAssumptions2 = new List(); + for (int i = 0; i < softAssumptions.Count; i++) + { + if (unsatisfiedSoftAssumptions.Contains(i)) + { + softAssumptions2.Add(softAssumptions[i]); + continue; + } + hardAssumptions.Add(softAssumptions[i]); + } + + var unsatisfiedSoftAssumptions2 = new List(); + outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2, handler); + + if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) + break; + + unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString())); + var reason1 = new HashSet(); //these are the reasons for inconsistency + unsatisfiedSoftAssumptions2.Iter(i => reason1.Add(softAssumptions2[i].ToString())); + + if (CommandLineOptions.Clo.Trace) + { + Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name); + reason.Iter(r => Console.Write("{0} ", r)); + Console.WriteLine(); + } + foreach (var r in reason) + { + Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName); + } + //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0) + foreach (var r in reason1) + { + Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];", refutedConstant.Name, r, descriptiveName); + } + } while (false); + + if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined) + { + Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", descriptiveName); + } + + CommandLineOptions.Clo.ProverCCLimit = el; + + double queryTime = (DateTime.UtcNow - now).TotalSeconds; + stats.proverTime += queryTime; + stats.numProverQueries++; + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Time taken = " + queryTime); + } + } + + public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary assignment) + { + DateTime now = DateTime.UtcNow; + + Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator; + proverInterface.Push(); + proverInterface.Assert(conjecture, false); + foreach (var v in assignment.Keys) { + if (assignment[v]) continue; + proverInterface.Assert(exprTranslator.LookupVariable(v), false); + } + List assumptionVars = new List(); + List assumptionExprs = new List(); + foreach (var v in assignment.Keys) { + if (!assignment[v]) continue; + assumptionVars.Add(v); + assumptionExprs.Add(exprTranslator.LookupVariable(v)); + } + List unsatCore; + ProverInterface.Outcome tmp = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler); + System.Diagnostics.Debug.Assert(tmp == ProverInterface.Outcome.Valid); + unsatCoreSet = new HashSet(); + foreach (int i in unsatCore) + unsatCoreSet.Add(assumptionVars[i]); + proverInterface.Pop(); + + double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds; + stats.unsatCoreProverTime += unsatCoreQueryTime; + stats.numUnsatCoreProverQueries++; + } + + } } \ No newline at end of file -- cgit v1.2.3