diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-12-20 09:24:17 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-12-20 09:24:17 +0000 |
| commit | 1951165d1787228d6f3571930d4d582d354c7c2c (patch) | |
| tree | 7c09bbad003110e132aa1f4d7f47ecc1c9b70d67 /Source | |
| parent | 23471ff664051f15faee787eb25ca72b74acfab5 (diff) | |
| parent | 5820d0619e8cfeb38e6fae4d6f1fd6df5537b425 (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 82 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 16 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 5 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 17 | ||||
| -rw-r--r-- | Source/Core/LoopUnroll.cs | 21 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 1797 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 266 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 211 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.csproj | 5 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 12 |
12 files changed, 2346 insertions, 90 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 402b5c68..1f5d7abd 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -591,7 +591,7 @@ namespace Microsoft.Boogie { Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
- program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
+ program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);
}
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
@@ -616,40 +616,58 @@ namespace Microsoft.Boogie { }
#region Run Houdini and verify
- if (CommandLineOptions.Clo.ContractInfer) {
- Houdini.Houdini houdini = new Houdini.Houdini(program);
- Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- if (CommandLineOptions.Clo.PrintAssignment) {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
+ if (CommandLineOptions.Clo.ContractInfer)
+ {
+ if (CommandLineOptions.Clo.AbstractHoudini != null)
+ {
+ CommandLineOptions.Clo.PrintErrorModel = 1;
+ CommandLineOptions.Clo.UseArrayTheory = true;
+ CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
+
+ // Run Abstract Houdini
+ Houdini.PredicateAbs.Initialize(program);
+ var abs = new Houdini.AbstractHoudini(program);
+ abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
+
+ return PipelineOutcome.Done;
}
- }
- if (CommandLineOptions.Clo.Trace)
- {
- int numTrueAssigns = 0;
- foreach (var x in outcome.assignment) {
- if (x.Value)
- numTrueAssigns++;
+ Houdini.Houdini houdini = new Houdini.Houdini(program);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment)
+ {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
+ }
+ if (CommandLineOptions.Clo.Trace)
+ {
+ int numTrueAssigns = 0;
+ foreach (var x in outcome.assignment)
+ {
+ if (x.Value)
+ numTrueAssigns++;
+ }
+ Console.WriteLine("Number of true assignments = " + numTrueAssigns);
+ Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
}
- Console.WriteLine("Number of true assignments = " + numTrueAssigns);
- Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
- Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
- Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
- Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
- }
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) {
- ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
- }
- //errorCount = outcome.ErrorCount;
- //verified = outcome.Verified;
- //inconclusives = outcome.Inconclusives;
- //timeOuts = outcome.TimeOuts;
- //outOfMemories = 0;
- return PipelineOutcome.Done;
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
+ }
+ //errorCount = outcome.ErrorCount;
+ //verified = outcome.Verified;
+ //inconclusives = outcome.Inconclusives;
+ //timeOuts = outcome.TimeOuts;
+ //outOfMemories = 0;
+ return PipelineOutcome.Done;
}
#endregion
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c8c052b7..c5534aba 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -341,7 +341,7 @@ namespace Microsoft.Boogie { }
}
- public void UnrollLoops(int n) {
+ public void UnrollLoops(int n, bool uc) {
Contract.Requires(0 <= n);
foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
@@ -351,7 +351,7 @@ namespace Microsoft.Boogie { Block start = impl.Blocks[0];
Contract.Assume(start != null);
Contract.Assume(cce.IsConsistent(start));
- impl.Blocks = LoopUnroll.UnrollLoops(start, n);
+ impl.Blocks = LoopUnroll.UnrollLoops(start, n, uc);
}
cce.EndExpose();
}
@@ -522,7 +522,7 @@ namespace Microsoft.Boogie { // header_last block that was created because of splitting header.
Dictionary<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();
- bool headRecursion = false; // testing an option to put recursive call before loop body
+ bool headRecursion = false; // testing an option to put recursive call before loop body
IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();
foreach (Block/*!*/ header in sortedHeaders)
@@ -816,6 +816,13 @@ namespace Microsoft.Boogie { public Dictionary<string, Dictionary<string, Block>> ExtractLoops()
{
+ HashSet<string> procsWithIrreducibleLoops = null;
+ return ExtractLoops(out procsWithIrreducibleLoops);
+ }
+
+ public Dictionary<string, Dictionary<string, Block>> ExtractLoops(out HashSet<string> procsWithIrreducibleLoops)
+ {
+ procsWithIrreducibleLoops = new HashSet<string>();
List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
foreach (Declaration d in this.TopLevelDeclarations)
@@ -832,6 +839,7 @@ namespace Microsoft.Boogie { {
System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));
fullMap[impl.Name] = null;
+ procsWithIrreducibleLoops.Add(impl.Name);
// statically unroll loops in this procedure
@@ -841,7 +849,7 @@ namespace Microsoft.Boogie { // unroll
Block start = impl.Blocks[0];
- impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound);
+ impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound, false);
// Now construct the "map back" information
// Resulting block label -> original block
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index ff84b501..5d7a404e 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1744,6 +1744,11 @@ namespace Microsoft.Boogie { void ObjectInvariant() {
Contract.Invariant(name != null);
}
+
+ public FunctionCall createUnresolvedCopy()
+ {
+ return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type));
+ }
[Pure]
public override string ToString() {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 4192259d..82768cf6 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -393,6 +393,9 @@ namespace Microsoft.Boogie { public int /*(0:3)*/ ErrorTrace = 1;
public bool IntraproceduralInfer = true;
public bool ContractInfer = false;
+ public bool ExplainHoudini = false;
+ public bool HoudiniUseCrossDependencies = false;
+ public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
public bool PrintAssignment = false;
public int InlineDepth = -1;
@@ -437,6 +440,7 @@ namespace Microsoft.Boogie { }
public int LoopUnrollCount = -1; // -1 means don't unroll loops
+ public bool SoundLoopUnrolling = false;
public int LoopFrameConditions = -1; // -1 means not specified -- this will be replaced by the "implications" section below
public int ModifiesDefault = 5;
public bool LocalModifiesChecks = true;
@@ -849,6 +853,14 @@ namespace Microsoft.Boogie { return true;
}
+ case "abstractHoudini":
+ {
+ if (ps.ConfirmArgumentCount(1))
+ {
+ AbstractHoudini = args[ps.i];
+ }
+ return true;
+ }
case "vc":
if (ps.ConfirmArgumentCount(1)) {
switch (args[ps.i]) {
@@ -1182,6 +1194,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||
ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||
ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) ||
+ ps.CheckBooleanFlag("soundLoopUnrolling", ref SoundLoopUnrolling) ||
ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) ||
ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) ||
ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) ||
@@ -1198,6 +1211,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
+ ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||
+ ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
@@ -1421,6 +1436,8 @@ namespace Microsoft.Boogie { /loopUnroll:<n>
unroll loops, following up to n back edges (and then some)
+ /soundLoopUnrolling
+ sound loop unrolling
/printModel:<n>
0 (default) - do not print Z3's error model
1 - print Z3's error model
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index 580cbdc5..ed523840 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -10,7 +10,7 @@ using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie {
public class LoopUnroll {
- public static List<Block/*!*/>/*!*/ UnrollLoops(Block start, int unrollMaxDepth) {
+ public static List<Block/*!*/>/*!*/ UnrollLoops(Block start, int unrollMaxDepth, bool soundLoopUnrolling) {
Contract.Requires(start != null);
Contract.Requires(0 <= unrollMaxDepth);
@@ -32,7 +32,7 @@ namespace Microsoft.Boogie { }
}
- LoopUnroll lu = new LoopUnroll(unrollMaxDepth, containingSCC, new List<Block/*!*/>());
+ LoopUnroll lu = new LoopUnroll(unrollMaxDepth, soundLoopUnrolling, containingSCC, new List<Block/*!*/>());
lu.Visit(gStart);
lu.newBlockSeqGlobal.Reverse();
return lu.newBlockSeqGlobal;
@@ -172,6 +172,7 @@ namespace Microsoft.Boogie { readonly List<Block/*!*/>/*!*/ newBlockSeqGlobal;
readonly Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ containingSCC;
readonly int c;
+ readonly bool soundLoopUnrolling;
readonly LoopUnroll next;
readonly LoopUnroll/*!*/ head;
@@ -185,7 +186,7 @@ namespace Microsoft.Boogie { [NotDelayed]
- private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)
+ private LoopUnroll(int unrollMaxDepth, bool soundLoopUnrolling, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)
: base() {//BASEMOVE DANGER
Contract.Requires(cce.NonNullElements(newBlockSeqGlobal));
Contract.Requires(cce.NonNullDictionaryAndValues(scc) && Contract.ForAll(scc.Values, v => cce.NonNullElements(v)));
@@ -196,21 +197,22 @@ namespace Microsoft.Boogie { //:base();
this.head = this;
if (unrollMaxDepth != 0) {
- next = new LoopUnroll(unrollMaxDepth - 1, scc, newBlockSeqGlobal, this);
+ next = new LoopUnroll(unrollMaxDepth - 1, soundLoopUnrolling, scc, newBlockSeqGlobal, this);
}
}
- private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal, LoopUnroll head) {
+ private LoopUnroll(int unrollMaxDepth, bool soundLoopUnrolling, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal, LoopUnroll head) {
Contract.Requires(head != null);
Contract.Requires(cce.NonNullDictionaryAndValues(scc));
Contract.Requires(cce.NonNullElements(newBlockSeqGlobal));
Contract.Requires(0 <= unrollMaxDepth);
this.newBlockSeqGlobal = newBlockSeqGlobal;
this.c = unrollMaxDepth;
+ this.soundLoopUnrolling = soundLoopUnrolling;
this.containingSCC = scc;
this.head = head;
if (unrollMaxDepth != 0) {
- next = new LoopUnroll(unrollMaxDepth - 1, scc, newBlockSeqGlobal, head);
+ next = new LoopUnroll(unrollMaxDepth - 1, soundLoopUnrolling, scc, newBlockSeqGlobal, head);
}
}
@@ -238,8 +240,11 @@ namespace Microsoft.Boogie { break;
}
}
- body.Add(new AssumeCmd(orig.tok, Bpl.Expr.False));
-
+ if (soundLoopUnrolling) {
+ body.Add(new AssertCmd(orig.tok, Bpl.Expr.False));
+ } else {
+ body.Add(new AssumeCmd(orig.tok, Bpl.Expr.False));
+ }
tcmd = new ReturnCmd(orig.TransferCmd.tok);
} else {
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 80f78d16..e7679a11 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -543,7 +543,7 @@ namespace Microsoft.Dafny }
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
- program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
+ program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);
}
if (CommandLineOptions.Clo.PrintInstrumented) {
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs new file mode 100644 index 00000000..7da06430 --- /dev/null +++ b/Source/Houdini/AbstractHoudini.cs @@ -0,0 +1,1797 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using VC;
+using Outcome = VC.VCGen.Outcome;
+using Bpl = Microsoft.Boogie;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie.Houdini {
+
+ public class AbstractHoudini
+ {
+ // Input Program
+ Program program;
+ // Impl -> VC
+ Dictionary<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, 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 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, VCExprNAry>>>();
+ this.impl2Summary = new Dictionary<string, ISummaryElement>();
+ this.name2Impl = SimpleUtil.nameImplMapping(program);
+
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+ this.reporter = new AbstractHoudiniErrorReporter();
+
+ this.proverTime = TimeSpan.Zero;
+ this.numProverQueries = 0;
+
+ if (CommandLineOptions.Clo.AbstractHoudini == "0")
+ UseBilateralAlgo = false;
+ }
+
+ public void computeSummaries(ISummaryElement summaryClass)
+ {
+ this.summaryClass = summaryClass;
+
+ name2Impl.Values.Iter(attachEnsures);
+
+ program.TopLevelDeclarations
+ .OfType<Implementation>()
+ .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.TopLevelDeclarations.OfType<Implementation>())
+ {
+ 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.TopLevelDeclarations.OfType<Implementation>())
+ {
+ var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,
+ impl.InParams, impl.OutParams, new VariableSeq(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();
+ }
+
+ // Obtain the summary expression for a procedure: used programmatically by clients
+ // of AbstractHoudini
+ private 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ 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; });
+ }
+
+ // 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.TopLevelDeclarations.OfType<Procedure>())
+ {
+ var nensures = new EnsuresSeq();
+ 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("assume", en.Attributes);
+
+ proc.Ensures = nensures;
+ }
+
+ var decls = new List<Declaration>();
+ copy.Values.Iter(impl => decls.Add(impl));
+ program.TopLevelDeclarations.Where(decl => !(decl is Implementation))
+ .Iter(decl => decls.Add(decl));
+ program.TopLevelDeclarations = decls;
+ var name2Proc = new Dictionary<string, Procedure>();
+ foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
+ {
+ 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))
+ {
+ program.Emit(wt);
+ }
+
+ // Replace SummaryPreds with their definition
+ foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ {
+ 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ 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))
+ {
+ 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)
+ {
+ InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
+ inlineRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
+ freeRequiresVisitor.Visit(impl);
+ }
+
+ 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 (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || impl.SkipVerification) continue;
+ callGraph.AddSource(impl);
+ procToImpls[impl.Proc].Add(impl);
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || 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.Item3), prover.VCExprGen);
+ env = gen.AndSimp(env, gen.Eq(tup.Item3, calleeSummary));
+ }
+
+ var upper = impl2Summary[impl.Name].GetTrueSummary(program, impl);
+
+ while(true)
+ {
+ var usedLower = true;
+ var query = impl2Summary[impl.Name];
+
+ // 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.Item3), 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}", impl.Name, query);
+ }
+
+ var start = DateTime.Now;
+
+ prover.BeginCheck(impl.Name, vc, reporter);
+ ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter);
+
+ proverTime += (DateTime.Now - start);
+ numProverQueries++;
+
+ if (UseBilateralAlgo)
+ {
+ if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
+ {
+ if(CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name);
+ impl2Summary[impl.Name] = upper;
+ ret = true;
+ 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);
+ impl2Summary[impl.Name] = impl2Summary[impl.Name].GetTrueSummary(program, impl);
+ ret = true;
+ 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ if (ret.ContainsKey(g.Name)) { cnt++; continue; }
+
+ ret.Add(string.Format("{0}", g.Name), summaryPred[cnt]);
+ cnt++;
+ }
+
+ // Constants
+ foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
+ {
+ 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ 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.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ 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.TopLevelDeclarations.OfType<Constant>())
+ {
+ 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());
+ }
+ else if (arg is VCExprVar)
+ {
+ var el = model.GetFunc(prover.Context.Lookup(arg as VCExprVar));
+ Debug.Assert(el.Arity == 0 && el.AppCount == 1);
+ return el.Apps.First().Result;
+ }
+ else
+ {
+ Debug.Assert(false);
+ return null;
+ }
+ }
+
+ private void attachEnsures(Implementation impl)
+ {
+ VariableSeq functionInterfaceVars = new VariableSeq();
+ foreach (Variable v in vcgen.program.GlobalVariables())
+ {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.InParams)
+ {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.OutParams)
+ {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies)
+ {
+ if (e.Decl == null) continue;
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
+ }
+ Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
+ var function = new Function(Token.NoToken, impl.Name + summaryPredSuffix, functionInterfaceVars, returnVar);
+ prover.Context.DeclareFunction(function, "");
+
+ ExprSeq exprs = new ExprSeq();
+ foreach (Variable v in vcgen.program.GlobalVariables())
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable v in impl.Proc.InParams)
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (Variable v in impl.Proc.OutParams)
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (IdentifierExpr ie in impl.Proc.Modifies)
+ {
+ Contract.Assert(ie != null);
+ if (ie.Decl == null)
+ continue;
+ exprs.Add(ie);
+ }
+ Expr postExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
+ impl.Proc.Ensures.Add(
+ new Ensures(Token.NoToken, false, postExpr, "",
+ new QKeyValue(Token.NoToken, "ah", new List<object>(), null)));
+ }
+
+ private void GenVC(Implementation impl)
+ {
+ ModelViewInfo mvInfo;
+ System.Collections.Hashtable 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);
+
+ // Create a macro so that the VC can sit with the theorem prover
+ Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
+ prover.DefineMacro(macro, vcexpr);
+
+ // Store VC
+ impl2VC.Add(impl.Name, gen.Function(macro));
+
+ //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
+
+ // Find the assert
+ impl2EndStateVars.Add(impl.Name, new List<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)));
+ }
+ }
+ Debug.Assert(found);
+
+ // Grab summary predicates
+ var visitor = new FindSummaryPred(prover.VCExprGen, assertId);
+ visitor.Mutate(vcexpr, true);
+
+ // 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, VCExprNAry>>());
+ visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup));
+ }
+ }
+
+ public interface ISummaryElement
+ {
+ 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
+ }
+
+ 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, List<NamedExpr>> PostPreds { get; private set; }
+ private static HashSet<string> boolConstants;
+ // 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>>();
+ boolConstants = new HashSet<string>();
+
+ program.TopLevelDeclarations.OfType<Constant>()
+ .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 tempP = new HashSet<Procedure>();
+ foreach (var proc in
+ program.TopLevelDeclarations.OfType<Procedure>()
+ .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template")))
+ {
+ tempP.Add(proc);
+ foreach (var ens in proc.Ensures.OfType<Ensures>())
+ {
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre"))
+ preT.Add(new NamedExpr(null, ens.Condition));
+ 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));
+
+ s = QKeyValue.FindStringAttribute(ens.Attributes, "post");
+ if (s != null)
+ postT.Add(new NamedExpr(s, ens.Condition));
+ }
+ }
+
+ program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl));
+
+ foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ {
+ PrePreds.Add(impl.Name, new List<NamedExpr>());
+ PostPreds.Add(impl.Name, new List<NamedExpr>());
+
+ preT.Iter(e => PrePreds[impl.Name].Add(e));
+ postT.Iter(e => PostPreds[impl.Name].Add(e));
+
+ // Pick up per-procedure pre-post
+ var nens = new EnsuresSeq();
+ foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())
+ {
+ string s = null;
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre"))
+ {
+ PrePreds[impl.Name].Add(new NamedExpr(ens.Condition));
+ }
+ 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));
+ }
+ else if ((s = QKeyValue.FindStringAttribute(ens.Attributes, "post")) != null)
+ {
+ PostPreds[impl.Name].Add(new NamedExpr(s, ens.Condition));
+ }
+ else
+ {
+ nens.Add(ens);
+ }
+ }
+ impl.Proc.Ensures = nens;
+ }
+
+ //Console.WriteLine("Running Abstract Houdini");
+ //PostPreds.Iter(expr => Console.WriteLine("\tPost: {0}", expr));
+ //PrePreds.Iter(expr => Console.WriteLine("\tPre: {0}", expr));
+ }
+
+ 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.Length == 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 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");
+ }
+
+ private object ToValue(Model.Element elem)
+ {
+ if (elem is Model.Integer)
+ {
+ return Microsoft.Basetypes.BigNum.FromInt((elem as Model.Integer).AsInt());
+ }
+ if (elem is Model.Boolean)
+ {
+ return (elem as Model.Boolean).Value;
+ }
+ throw new NotImplementedException("Cannot yet handle this Model.Element type");
+ }
+
+ private 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");
+ }
+
+ 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 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.Length == 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 VCExprOp Translate(BinaryOperator op)
+ {
+ switch (op.Op)
+ {
+ case BinaryOperator.Opcode.Add:
+ return VCExpressionGenerator.AddIOp;
+ case BinaryOperator.Opcode.Sub:
+ return VCExpressionGenerator.SubIOp;
+ case BinaryOperator.Opcode.Mul:
+ return VCExpressionGenerator.MulIOp;
+ case BinaryOperator.Opcode.Div:
+ return VCExpressionGenerator.DivIOp;
+ case BinaryOperator.Opcode.Mod:
+ return VCExpressionGenerator.ModOp;
+ case BinaryOperator.Opcode.Eq:
+ case BinaryOperator.Opcode.Iff:
+ // we don't distinguish between equality and equivalence at this point
+ return VCExpressionGenerator.EqOp;
+ case BinaryOperator.Opcode.Neq:
+ return VCExpressionGenerator.NeqOp;
+ case BinaryOperator.Opcode.Lt:
+ return VCExpressionGenerator.LtOp;
+ case BinaryOperator.Opcode.Le:
+ return VCExpressionGenerator.LeOp;
+ case BinaryOperator.Opcode.Ge:
+ return VCExpressionGenerator.GeOp;
+ case BinaryOperator.Opcode.Gt:
+ return VCExpressionGenerator.GtOp;
+ case BinaryOperator.Opcode.Imp:
+ return VCExpressionGenerator.ImpliesOp;
+ case BinaryOperator.Opcode.And:
+ return VCExpressionGenerator.AndOp;
+ case BinaryOperator.Opcode.Or:
+ return VCExpressionGenerator.OrOp;
+ case BinaryOperator.Opcode.Subtype:
+ return VCExpressionGenerator.SubtypeOp;
+ default:
+ Contract.Assert(false);
+ throw new NotImplementedException();
+ }
+
+ }
+
+ public override string ToString()
+ {
+ var ret = "";
+ if (isFalse) return "false";
+ var first = true;
+ PredicateAbsConjunct.tempProcName = procName;
+ 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 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);
+
+ 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);
+ if (!postPredsVal[i])
+ {
+ newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j]));
+ }
+
+ if (isFalse)
+ value[i] = newDisj;
+ else
+ value[i] = PredicateAbsDisjunct.And(value[i], newDisj);
+ }
+
+ isFalse = false;
+
+ //Console.WriteLine("Result of Join: {0}", this.ToString());
+ }
+
+ // Precondition: the upper guys are just {true/false} ==> 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++)
+ {
+ // check precondition
+ if (!value[i].isTrue && !value[i].isFalse)
+ throw new NotImplementedException("Invalid upper domain element");
+ if (!other.value[i].isTrue && !other.value[i].isFalse)
+ throw new NotImplementedException("Invalid upper domain element");
+
+ if (value[i].isFalse && other.value[i].isTrue)
+ value[i] = new PredicateAbsDisjunct(true);
+ }
+ }
+
+ public bool IsEqual(ISummaryElement other)
+ {
+ return false;
+ }
+
+ // Precondition: the upper guys are just {true/false} ==> post-pred
+ // Postcondition: the returned value is also of this form
+ public ISummaryElement AbstractConsequence(ISummaryElement iupper)
+ {
+ var upper = iupper as PredicateAbs;
+
+ for (int i = 0; i < PostPreds[this.procName].Count; i++)
+ {
+ // check precondition
+ if (!upper.value[i].isTrue && !upper.value[i].isFalse)
+ throw new NotImplementedException("Invalid upper domain element");
+
+ if (upper.value[i].isTrue)
+ continue;
+
+ 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);
+
+ ret.value[i] = new PredicateAbsDisjunct(true);
+
+ // check that this \lesseq ret
+ if (isFalse) return ret;
+
+ if (value[i].isTrue)
+ 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
+ }
+
+ class PredicateAbsDisjunct
+ {
+ List<PredicateAbsConjunct> conjuncts;
+ public bool isTrue {get; private set;}
+ public bool isFalse
+ {
+ get
+ {
+ if (isTrue) return false;
+ return conjuncts.Count == 0;
+ }
+ }
+
+ public PredicateAbsDisjunct(bool isTrue)
+ {
+ this.isTrue = isTrue;
+ conjuncts = new List<PredicateAbsConjunct>();
+ }
+
+ private PredicateAbsDisjunct(List<PredicateAbsConjunct> conjuncts)
+ {
+ isTrue = false;
+ this.conjuncts = conjuncts;
+ }
+
+ // Disjunct of singleton conjuncts
+ public PredicateAbsDisjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ {
+ conjuncts = new List<PredicateAbsConjunct>();
+ isTrue = false;
+ pos.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, true)));
+ neg.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, false)));
+ }
+
+ public static PredicateAbsDisjunct And(PredicateAbsDisjunct v1, PredicateAbsDisjunct v2)
+ {
+ if (v1.isTrue) return v2;
+ if (v2.isTrue) return v1;
+
+ var result = new List<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);
+ }
+
+ 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;
+ }
+ }
+
+ class PredicateAbsConjunct
+ {
+ static int ConjunctBound = 3;
+ public static string tempProcName = null;
+
+ public bool isFalse { get; private set; }
+ HashSet<int> posPreds;
+ HashSet<int> negPreds;
+
+ public static void Initialize(int bound)
+ {
+ ConjunctBound = bound;
+ }
+
+ private void Normalize()
+ {
+ if (posPreds.Intersect(negPreds).Any() || negPreds.Intersect(posPreds).Any() || (posPreds.Count + negPreds.Count > ConjunctBound))
+ {
+ isFalse = true;
+ posPreds = new HashSet<int>();
+ negPreds = new HashSet<int>();
+ }
+ }
+
+ public PredicateAbsConjunct(bool isFalse)
+ {
+ posPreds = new HashSet<int>();
+ negPreds = new HashSet<int>();
+ this.isFalse = isFalse;
+ }
+
+ public static PredicateAbsConjunct Singleton(int v, bool isPositive)
+ {
+ if (isPositive)
+ return new PredicateAbsConjunct(new int[] { v }, new HashSet<int>());
+ else
+ return new PredicateAbsConjunct(new HashSet<int>(), new int[] { v });
+ }
+
+ public PredicateAbsConjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ {
+ isFalse = false;
+ posPreds = new HashSet<int>(pos);
+ negPreds = new HashSet<int>(neg);
+ Normalize();
+ }
+
+ public static PredicateAbsConjunct And(PredicateAbsConjunct v1, PredicateAbsConjunct v2)
+ {
+ if (v1.isFalse || v2.isFalse) return new PredicateAbsConjunct(true);
+ return new PredicateAbsConjunct(v1.posPreds.Union(v2.posPreds), v1.negPreds.Union(v2.negPreds));
+ }
+
+ public bool implies(PredicateAbsConjunct v)
+ {
+ if (isFalse) return true;
+ if (v.isFalse) return false;
+ return (posPreds.IsSupersetOf(v.posPreds) && negPreds.IsSupersetOf(v.negPreds));
+ }
+
+ public VCExpr ToVcExpr(Func<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;
+ posPreds.Iter(p => ret = Expr.And(ret, predToExpr(p)));
+ negPreds.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[tempProcName][p]);
+ first = false;
+ }
+ foreach (var p in negPreds)
+ {
+ ret += string.Format("{0}!{1}", first ? "" : " && ", PredicateAbs.PrePreds[tempProcName][p]);
+ first = false;
+ }
+ return ret;
+ }
+ }
+
+ class FindSummaryPred : MutatingVCExprVisitor<bool>
+ {
+ public List<Tuple<string, bool, VCExprNAry>> summaryPreds;
+ int assertId;
+
+ public FindSummaryPred(VCExpressionGenerator gen, int assertId)
+ : base(gen)
+ {
+ summaryPreds = new List<Tuple<string, bool, 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;
+ var selfSummary = false;
+
+ 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;
+
+ selfSummary = true;
+ retnary = subexpr;
+ }
+
+ string calleeName = op.Func.Name;
+
+ if (!calleeName.EndsWith(AbstractHoudini.summaryPredSuffix))
+ return ret;
+
+ if (selfSummary)
+ {
+ // This summary pred would have been found twice
+ var nlist = new List<Tuple<string, bool, VCExprNAry>>();
+ foreach (var tup in summaryPreds)
+ {
+ if (tup.Item3 != retnary) nlist.Add(tup);
+ }
+ summaryPreds = nlist;
+ }
+
+ summaryPreds.Add(Tuple.Create(calleeName.Substring(0, calleeName.Length - AbstractHoudini.summaryPredSuffix.Length), selfSummary, retnary));
+
+
+ return ret;
+ }
+
+ }
+
+ class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
+ {
+ public Model model;
+
+ public AbstractHoudiniErrorReporter()
+ {
+ model = null;
+ }
+
+ public override void OnModel(IList<string> labels, Model model)
+ {
+ Debug.Assert(model != null);
+ //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 (Declaration d in p.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ Implementation impl = d as Implementation;
+ m.Add(impl.Name, impl);
+ }
+ }
+
+ return m;
+ }
+
+ // is "assert true"?
+ public static bool isAssertTrue(Cmd cmd)
+ {
+ var acmd = cmd as AssertCmd;
+ if (acmd == null) return false;
+ var le = acmd.Expr as LiteralExpr;
+ if (le == null) return false;
+ if (le.IsTrue) return true;
+ return false;
+ }
+ }
+
+}
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 7832da89..940b355f 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -13,20 +13,36 @@ using System.Collections; using System.IO;
using System.Threading;
using VC;
+using System.Linq;
namespace Microsoft.Boogie.Houdini {
public class ExistentialConstantCollector : StandardVisitor {
- public static HashSet<Variable> CollectHoudiniConstants(Houdini houdini, Implementation impl) {
- ExistentialConstantCollector collector = new ExistentialConstantCollector(houdini);
- collector.VisitImplementation(impl);
- return collector.houdiniConstants;
- }
+ 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.houdiniConstants = new HashSet<Variable>();
+ this.houdiniAssertConstants = new HashSet<Variable>();
+ this.houdiniAssumeConstants = new HashSet<Variable>();
+
+ this.explainNegative = new HashSet<Variable>();
+ this.explainPositive = new HashSet<Variable>();
+ this.constToControl = new Dictionary<string, Tuple<Variable, Variable>>();
}
private Houdini houdini;
- private HashSet<Variable> houdiniConstants;
+ public HashSet<Variable> houdiniAssertConstants;
+ public HashSet<Variable> houdiniAssumeConstants;
+
+ // Explain Houdini stuff
+ public HashSet<Variable> explainPositive;
+ public HashSet<Variable> explainNegative;
+ public Dictionary<string, Tuple<Variable, Variable>> constToControl;
+ Implementation impl;
+
public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
AddHoudiniConstant(node);
return base.VisitAssertRequiresCmd(node);
@@ -43,10 +59,38 @@ namespace Microsoft.Boogie.Houdini { AddHoudiniConstant(node);
return base.VisitAssumeCmd(node);
}
- private void AddHoudiniConstant(PredicateCmd node) {
- Variable houdiniConstant;
- if (houdini.MatchCandidate(node.Expr, out houdiniConstant))
- houdiniConstants.Add(houdiniConstant);
+ 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<Variable, Variable> 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);
}
}
@@ -63,6 +107,14 @@ namespace Microsoft.Boogie.Houdini { ConditionGeneration.CounterexampleCollector collector;
HashSet<Variable> unsatCoreSet;
HashSet<Variable> houdiniConstants;
+ public HashSet<Variable> houdiniAssertConstants;
+ private HashSet<Variable> houdiniAssumeConstants;
+
+ // Extra constants created for ExplainHoudini
+ private HashSet<Variable> explainConstantsPositive;
+ private HashSet<Variable> explainConstantsNegative;
+ private Dictionary<string, Tuple<Variable, Variable>> constantToControl;
+
Houdini houdini;
Implementation implementation;
@@ -84,7 +136,17 @@ namespace Microsoft.Boogie.Houdini { ModelViewInfo mvInfo;
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
- houdiniConstants = ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl);
+ 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<Variable>();
+ houdiniConstants.UnionWith(houdiniAssertConstants);
+ houdiniConstants.UnionWith(houdiniAssumeConstants);
var exprGen = proverInterface.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
@@ -130,6 +192,15 @@ namespace Microsoft.Boogie.Houdini { }
}
+ 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);
@@ -167,7 +238,176 @@ namespace Microsoft.Boogie.Houdini { return proverOutcome;
}
- public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Variable, bool> assignment) {
+ // MAXSAT
+ public void Explain(ProverInterface proverInterface,
+ Dictionary<Variable, bool> 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<VCExpr>();
+ var softAssumptions = new List<VCExpr>();
+
+ 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<int> 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<string>();
+ 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<VCExpr>();
+ 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<int>();
+ 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()));
+ 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, implementation.Name);
+ }
+ } 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", implementation.Name);
+ }
+
+ CommandLineOptions.Clo.ProverCCLimit = el;
+
+ double queryTime = (DateTime.UtcNow - now).TotalSeconds;
+ proverTime += queryTime;
+ numProverQueries++;
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Time taken = " + queryTime);
+ }
+ }
+
+ public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Variable, bool> assignment)
+ {
DateTime now = DateTime.UtcNow;
Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 5271a6a3..17b537eb 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -311,8 +311,11 @@ namespace Microsoft.Boogie.Houdini { private Graph<Implementation> callGraph;
private HashSet<Implementation> vcgenFailures;
private HoudiniState currentHoudiniState;
+ private CrossDependencies crossDependencies;
- public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } }
+ public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } }
+
+ public static TextWriter explainHoudiniDottyFile;
public Houdini(Program program) {
this.program = program;
@@ -327,8 +330,15 @@ namespace Microsoft.Boogie.Houdini { if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
+ if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
+ {
+ if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
+ this.crossDependencies = new CrossDependencies(this.houdiniConstants);
+ this.crossDependencies.Visit(program);
+ }
+
Inline();
-
+
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
@@ -351,6 +361,16 @@ namespace Microsoft.Boogie.Houdini { }
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
+
+ if (CommandLineOptions.Clo.ExplainHoudini)
+ {
+ // Print results of ExplainHoudini to a dotty file
+ explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
+ explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
+ foreach (var constant in houdiniConstants)
+ explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
+ explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
+ }
}
private void Inline() {
@@ -425,6 +445,58 @@ namespace Microsoft.Boogie.Houdini { return existentialConstants;
}
+ // Compute dependencies between candidates
+ public class CrossDependencies : StandardVisitor
+ {
+ public CrossDependencies(HashSet<Variable> constants)
+ {
+ this.constants = constants;
+ }
+
+ public override Program VisitProgram(Program node)
+ {
+ assumedInImpl = new Dictionary<string, HashSet<Implementation>>();
+ inAssume = false;
+ return base.VisitProgram(node);
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ curImpl = node;
+ return base.VisitImplementation(node);
+ }
+
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ inAssume = true;
+ var res = base.VisitAssumeCmd(node);
+ inAssume = false;
+ return res;
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ if (node is Constant)
+ {
+ var constant = node as Constant;
+ if (constants.Contains(constant))
+ {
+ if (!assumedInImpl.ContainsKey(constant.Name))
+ assumedInImpl[constant.Name] = new HashSet<Implementation>();
+ assumedInImpl[constant.Name].Add(curImpl);
+ }
+ }
+ return base.VisitVariable(node);
+ }
+
+ HashSet<Variable> constants;
+ Implementation curImpl;
+ bool inAssume;
+
+ // contant -> set of implementations that have an assume command with that constant
+ public Dictionary<string, HashSet<Implementation>> assumedInImpl { get; private set; }
+ }
+
private Graph<Implementation> BuildCallGraph() {
Graph<Implementation> callGraph = new Graph<Implementation>();
Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
@@ -501,6 +573,30 @@ namespace Microsoft.Boogie.Houdini { return false;
}
+ // For Explain houdini: it decorates the condition \phi as (vpos && (\phi || \not vneg))
+ // Precondition: MatchCandidate returns true
+ public Expr InsertCandidateControl(Expr boogieExpr, Variable vpos, Variable vneg)
+ {
+ Contract.Assert(CommandLineOptions.Clo.ExplainHoudini);
+
+ NAryExpr e = boogieExpr as NAryExpr;
+ if (e != null && e.Fun is BinaryOperator && ((BinaryOperator)e.Fun).Op == BinaryOperator.Opcode.Imp)
+ {
+ Expr antecedent = e.Args[0];
+ Expr consequent = e.Args[1];
+
+ IdentifierExpr id = antecedent as IdentifierExpr;
+ if (id != null && id.Decl is Constant && houdiniConstants.Contains((Constant)id.Decl))
+ {
+ return Expr.Imp(antecedent, Expr.And(Expr.Ident(vpos), Expr.Or(consequent, Expr.Not(Expr.Ident(vneg)))));
+ }
+
+ return Expr.Imp(antecedent, InsertCandidateControl(consequent, vpos, vneg));
+ }
+ Contract.Assert(false);
+ return null;
+ }
+
private Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants) {
Dictionary<Variable, bool> initial = new Dictionary<Variable, bool>();
foreach (var constant in constants)
@@ -593,40 +689,59 @@ namespace Microsoft.Boogie.Houdini { Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;
- switch (outcome) {
- case ProverInterface.Outcome.Valid:
- //yeah, dequeue
- break;
- case ProverInterface.Outcome.Invalid:
- Contract.Assume(errors != null);
- foreach (Counterexample error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation != null) { // some candidate annotation removed
- AddRelatedToWorkList(refutedAnnotation);
- UpdateAssignment(refutedAnnotation);
- dequeue = false;
- #region Extra debugging output
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ //yeah, dequeue
+ break;
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors)
+ {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null)
+ { // some candidate annotation removed
+ AddRelatedToWorkList(refutedAnnotation);
+ UpdateAssignment(refutedAnnotation);
+ dequeue = false;
+ #region Extra debugging output
+ if (CommandLineOptions.Clo.Trace)
+ {
+ using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ {
+ cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
+ cexWriter.Write(error.ToString());
+ cexWriter.WriteLine();
+ using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
+ foreach (Microsoft.Boogie.Block blk in error.Trace)
+ blk.Emit(writer, 15);
+ //cexWriter.WriteLine();
+ }
+ }
+ #endregion
+
+ }
+ }
+ break;
+ default:
if (CommandLineOptions.Clo.Trace)
{
- using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
+ }
+ HoudiniSession houdiniSession;
+ houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
+ foreach (Variable v in houdiniSession.houdiniAssertConstants)
+ {
+ if (CommandLineOptions.Clo.Trace)
{
- cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
- cexWriter.Write(error.ToString());
- cexWriter.WriteLine();
- using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
- foreach (Microsoft.Boogie.Block blk in error.Trace)
- blk.Emit(writer, 15);
- //cexWriter.WriteLine();
+ Console.WriteLine("Removing " + v);
}
+ currentHoudiniState.Assignment.Remove(v);
+ currentHoudiniState.Assignment.Add(v, false);
+ this.NotifyConstant(v.Name);
}
- #endregion
-
- }
- }
- break;
- default:
- currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
- break;
+ currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
+ break;
}
return dequeue;
@@ -720,6 +835,11 @@ namespace Microsoft.Boogie.Houdini { currentHoudiniState.Outcome.assignment = assignment;
vcgen.Close();
proverInterface.Close();
+ if (CommandLineOptions.Clo.ExplainHoudini)
+ {
+ explainHoudiniDottyFile.WriteLine("};");
+ explainHoudiniDottyFile.Close();
+ }
return currentHoudiniState.Outcome;
}
@@ -743,6 +863,15 @@ namespace Microsoft.Boogie.Houdini { }
break;
case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
+ if (CommandLineOptions.Clo.HoudiniUseCrossDependencies && crossDependencies.assumedInImpl.ContainsKey(refutedAnnotation.Constant.Name))
+ {
+ foreach (var impl in crossDependencies.assumedInImpl[refutedAnnotation.Constant.Name])
+ {
+ houdiniSessions.TryGetValue(impl, out session);
+ if (session.InUnsatCore(refutedAnnotation.Constant))
+ implementations.Add(impl);
+ }
+ }
break;
default:
throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
@@ -881,6 +1010,26 @@ namespace Microsoft.Boogie.Houdini { DebugRefutedCandidates(currentHoudiniState.Implementation, errors);
+ #region Explain Houdini
+ if (CommandLineOptions.Clo.ExplainHoudini && outcome == ProverInterface.Outcome.Invalid)
+ {
+ Contract.Assume(errors != null);
+ // make a copy of this variable
+ errors = new List<Counterexample>(errors);
+ var refutedAnnotations = new List<RefutedAnnotation>();
+ foreach (Counterexample error in errors)
+ {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation.Kind == RefutedAnnotationKind.ASSERT) continue;
+ refutedAnnotations.Add(refutedAnnotation);
+ }
+ foreach (var refutedAnnotation in refutedAnnotations)
+ {
+ session.Explain(proverInterface, currentHoudiniState.Assignment, refutedAnnotation.Constant);
+ }
+ }
+ #endregion
+
if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort
currentHoudiniState.WorkQueue.Dequeue();
this.NotifyDequeue();
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 97d26001..2d2b0373 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -78,6 +78,7 @@ <Compile Include="..\version.cs">
<Link>version.cs</Link>
</Compile>
+ <Compile Include="AbstractHoudini.cs" />
<Compile Include="Checker.cs" />
<Compile Include="Houdini.cs" />
</ItemGroup>
@@ -98,6 +99,10 @@ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
+ <ProjectReference Include="..\Model\Model.csproj">
+ <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
+ <Name>Model</Name>
+ </ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
<Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 4d002956..b1cef239 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -45,7 +45,7 @@ namespace Microsoft.Boogie.SMTLib public bool OptimizeForBv = false;
public bool ProduceModel() {
- return !CommandLineOptions.Clo.UseLabels ||
+ return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini ||
ExpectingModel();
}
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 5dfec676..addfa3de 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -36,6 +36,18 @@ namespace Microsoft.Boogie.SMTLib {
Contract.Ensures(_proverPath != null);
+ // Command line option 'z3exe' always has priority if set
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ if (!File.Exists(_proverPath)) {
+ throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);
+ }
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
var proverExe = "z3.exe";
if (_proverPath == null) {
|