diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify.sln | 22 | ||||
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 8 | ||||
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 75 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 192 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 16 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 84 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 34 |
13 files changed, 284 insertions, 177 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index ed80f6ac..1827b12e 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -564,6 +564,7 @@ namespace Microsoft.Boogie { public int StratifiedInliningOption = 0;
public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
public int StratifiedInliningVerbose = 0; // verbosity level
+ public bool BctModeForStratifiedInlining = false;
public int RecursionBound = 500;
public bool NonUniformUnfolding = false;
public string inferLeastForUnsat = null;
@@ -1009,6 +1010,12 @@ namespace Microsoft.Boogie { StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));
}
return true;
+ case "siBct":
+ if (ps.ConfirmArgumentCount(1))
+ {
+ BctModeForStratifiedInlining = (Int32.Parse(cce.NonNull(args[ps.i])) == 1);
+ }
+ return true;
case "recursionBound":
if (ps.ConfirmArgumentCount(1)) {
RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));
diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln index a31d8600..4d515300 100644 --- a/Source/GPUVerify.sln +++ b/Source/GPUVerify.sln @@ -15,8 +15,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"
@@ -189,26 +187,6 @@ Global {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Checked|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Checked|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.Build.0 = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 8c090b6a..b2e54dbd 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -44,6 +44,8 @@ namespace GPUVerify public static bool ShowMayBeTidPlusConstantAnalysis = false;
public static bool ShowArrayControlFlowAnalysis = false;
+ public static bool NoLoopPredicateInvariants = false;
+
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -196,6 +198,11 @@ namespace GPUVerify ShowArrayControlFlowAnalysis = true;
break;
+ case "-noLoopPredicateInvariants":
+ case "/noLoopPredicateInvariants":
+ NoLoopPredicateInvariants = true;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index b767816c..9881b0f0 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -152,10 +152,6 @@ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
- <ProjectReference Include="..\BoogieDriver\BoogieDriver.csproj">
- <Project>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</Project>
- <Name>BoogieDriver</Name>
- </ProjectReference>
<ProjectReference Include="..\Core\Core.csproj">
<Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index b70260ce..48cd8a2f 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -28,7 +28,7 @@ namespace GPUVerify if (CommandLineOptions.inputFiles.Count < 1)
{
- OnlyBoogie.ErrorWriteLine("*** Error: No input files were specified.");
+ Console.WriteLine("*** Error: No input files were specified.");
Environment.Exit(1);
}
@@ -41,7 +41,7 @@ namespace GPUVerify }
if (extension != ".gbpl")
{
- OnlyBoogie.AdvisoryWriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);
+ Console.WriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);
}
}
@@ -220,14 +220,14 @@ namespace GPUVerify errorCount = Parser.Parse(bplFileName, defines, out programSnippet);
if (programSnippet == null || errorCount != 0)
{
- OnlyBoogie.ErrorWriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
okay = false;
continue;
}
}
catch (IOException e)
{
- OnlyBoogie.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ Console.WriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
okay = false;
continue;
}
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index 0950cd9a..316a3df6 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -251,7 +251,7 @@ namespace GPUVerify VisitWhileInvariants(whileCmd.Invariants, NewGuard),
VisitStmtList(whileCmd.Body));
- if (NewInvariant != null)
+ if (NewInvariant != null && !CommandLineOptions.NoLoopPredicateInvariants)
{
NewWhile.Invariants.Add(NewInvariant);
}
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index f99c4651..b837e61a 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -22,8 +22,15 @@ namespace Microsoft.Boogie.Houdini { private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
ConditionGeneration.CounterexampleCollector collector;
+ HashSet<Variable> unsatCoreSet;
- public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl) {
+ public bool InUnsatCore(Variable constant) {
+ if (unsatCoreSet == null)
+ return true;
+ return unsatCoreSet.Contains(constant);
+ }
+
+ public HoudiniSession(VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) {
descriptiveName = impl.Name;
collector = new ConditionGeneration.CounterexampleCollector();
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
@@ -33,36 +40,82 @@ namespace Microsoft.Boogie.Houdini { Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo);
Hashtable/*<int, Absy!>*/ label2absy;
- var exprGen = checker.TheoremProver.Context.ExprGen;
+ var exprGen = proverInterface.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker);
-
+ 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 VariableSeq(), 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, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, proverInterface.Context, program);
}
else {
- handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, proverInterface.Context, program);
}
}
- public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {
+ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment) {
+ ProverContext proverContext = proverInterface.Context;
+ Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;
+ VCExpressionGenerator exprGen = proverInterface.VCExprGen;
+
+ VCExpr expr = VCExpressionGenerator.True;
+ foreach (KeyValuePair<Variable, bool> 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));
+ }
+ }
+ return expr;
+ }
+
+ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {
collector.examples.Clear();
- VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);
+ VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);
if (CommandLineOptions.Clo.Trace) {
Console.WriteLine("Verifying " + descriptiveName);
}
DateTime now = DateTime.UtcNow;
- checker.BeginCheck(descriptiveName, vc, handler);
- WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
- ProverInterface.Outcome proverOutcome = checker.ReadOutcome();
+
+ proverInterface.BeginCheck(descriptiveName, vc, handler);
+ ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);
+
+#if UNSAT_CORE
+ 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<Variable> assumptionVars = new List<Variable>();
+ List<VCExpr> assumptionExprs = new List<VCExpr>();
+ foreach (var v in assignment.Keys) {
+ if (!assignment[v]) continue;
+ assumptionVars.Add(v);
+ assumptionExprs.Add(exprTranslator.LookupVariable(v));
+ }
+ List<int> unsatCore;
+ ProverInterface.Outcome proverOutcome = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler);
+ unsatCoreSet = new HashSet<Variable>();
+ foreach (int i in unsatCore)
+ unsatCoreSet.Add(assumptionVars[i]);
+ proverInterface.Pop();
+#endif
+
double queryTime = (DateTime.UtcNow - now).TotalSeconds;
proverTime += queryTime;
numProverQueries++;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index f6c334e7..5f60feff 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -39,7 +39,7 @@ namespace Microsoft.Boogie.Houdini { public virtual void UpdateStart(Program program, int numConstants) { }
public virtual void UpdateIteration() { }
public virtual void UpdateImplementation(Implementation implementation) { }
- public virtual void UpdateAssignment(Dictionary<string, bool> assignment) { }
+ public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment) { }
public virtual void UpdateOutcome(ProverInterface.Outcome outcome) { }
public virtual void UpdateEnqueue(Implementation implementation) { }
public virtual void UpdateDequeue() { }
@@ -141,10 +141,10 @@ namespace Microsoft.Boogie.Houdini { wr.WriteLine("implementation under analysis :" + implementation.Name);
wr.Flush();
}
- public override void UpdateAssignment(Dictionary<string, bool> assignment) {
+ public override void UpdateAssignment(Dictionary<Variable, bool> assignment) {
bool firstTime = true;
wr.Write("assignment under analysis : axiom (");
- foreach (KeyValuePair<string, bool> kv in assignment) {
+ foreach (KeyValuePair<Variable, bool> kv in assignment) {
if (!firstTime) wr.Write(" && "); else firstTime = false;
string valString; // ugliness to get it lower cased
if (kv.Value) valString = "true"; else valString = "false";
@@ -215,7 +215,7 @@ namespace Microsoft.Boogie.Houdini { protected void NotifyImplementation(Implementation implementation) {
Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateImplementation(implementation); });
}
- protected void NotifyAssignment(Dictionary<string, bool> assignment) {
+ protected void NotifyAssignment(Dictionary<Variable, bool> assignment) {
Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });
}
protected void NotifyOutcome(ProverInterface.Outcome outcome) {
@@ -279,6 +279,11 @@ namespace Microsoft.Boogie.Houdini { }
}
+ public class Macro : Function {
+ public Macro(IToken tok, string name, VariableSeq args, Variable result)
+ : base(tok, name, args, result) { }
+ }
+
public class FreeRequiresVisitor : StandardVisitor {
public override Requires VisitRequires(Requires requires) {
if (requires.Free)
@@ -298,13 +303,72 @@ namespace Microsoft.Boogie.Houdini { public class Houdini : ObservableHoudini {
private Program program;
- private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
+ private HashSet<Variable> houdiniConstants;
private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;
private VCGen vcgen;
- private Checker checker;
+ private ProverInterface proverInterface;
private Graph<Implementation> callGraph;
private HashSet<Implementation> vcgenFailures;
+
+ private ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
+ Contract.Requires(prog != null);
+
+ ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
+
+ if (logFilePath != null) {
+ options.LogFilename = logFilePath;
+ if (appendLogFile)
+ options.AppendLogFile = appendLogFile;
+ }
+
+ if (timeout > 0) {
+ options.TimeLimit = timeout * 1000;
+ }
+
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+
+ ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+
+ // set up the context
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ TypeCtorDecl t = decl as TypeCtorDecl;
+ if (t != null) {
+ ctx.DeclareType(t, null);
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ Constant c = decl as Constant;
+ if (c != null) {
+ ctx.DeclareConstant(c, c.Unique, null);
+ }
+ else {
+ Function f = decl as Function;
+ if (f != null) {
+ ctx.DeclareFunction(f, null);
+ }
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ Axiom ax = decl as Axiom;
+ if (ax != null) {
+ ctx.AddAxiom(ax, null);
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ GlobalVariable v = decl as GlobalVariable;
+ if (v != null) {
+ ctx.DeclareGlobalVariable(v, null);
+ }
+ }
+
+ return (ProverInterface) CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
+ }
+
public Houdini(Program program) {
this.program = program;
@@ -321,7 +385,7 @@ namespace Microsoft.Boogie.Houdini { Inline();
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+ this.proverInterface = CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
vcgenFailures = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
@@ -331,7 +395,7 @@ namespace Microsoft.Boogie.Houdini { try {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Generating VC for {0}", impl.Name);
- HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl);
+ HoudiniSession session = new HoudiniSession(vcgen, proverInterface, program, impl);
houdiniSessions.Add(impl, session);
}
catch (VCGenException) {
@@ -395,19 +459,19 @@ namespace Microsoft.Boogie.Houdini { }
}
- private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
- Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
+ private HashSet<Variable> CollectExistentialConstants() {
+ HashSet<Variable> existentialConstants = new HashSet<Variable>();
foreach (Declaration decl in program.TopLevelDeclarations) {
Constant constant = decl as Constant;
if (constant != null) {
bool result = false;
if (constant.CheckBooleanAttribute("existential", ref result)) {
if (result == true)
- existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken, constant));
+ existentialConstants.Add(constant);
}
}
}
- return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);
+ return existentialConstants;
}
private Graph<Implementation> BuildCallGraph() {
@@ -467,44 +531,23 @@ namespace Microsoft.Boogie.Houdini { */
}
- private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
+ private bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) {
candidateConstant = null;
IExpr antecedent;
IExpr expr = boogieExpr as IExpr;
if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
- if (constantFunApp != null && houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name)) {
- candidateConstant = constantFunApp.IdentifierExpr.Name;
+ if (constantFunApp != null && houdiniConstants.Contains(constantFunApp.IdentifierExpr.Decl)) {
+ candidateConstant = constantFunApp.IdentifierExpr.Decl;
return true;
}
}
return false;
}
- private VCExpr BuildAxiom(Dictionary<string, bool> currentAssignment) {
- DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;
- Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;
- VCExpressionGenerator exprGen = checker.VCExprGen;
-
- VCExpr expr = VCExpressionGenerator.True;
- foreach (KeyValuePair<string, bool> kv in currentAssignment) {
- IdentifierExpr constantExpr;
- houdiniConstants.TryGetValue(kv.Key, out constantExpr);
- Contract.Assume(constantExpr != null);
- VCExprVar exprVar = exprTranslator.LookupVariable(constantExpr.Decl);
- if (kv.Value) {
- expr = exprGen.And(expr, exprVar);
- }
- else {
- expr = exprGen.And(expr, exprGen.Not(exprVar));
- }
- }
- return expr;
- }
-
- private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {
- Dictionary<string, bool> initial = new Dictionary<string, bool>();
- foreach (string constant in constants)
+ private Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants) {
+ Dictionary<Variable, bool> initial = new Dictionary<Variable, bool>();
+ foreach (var constant in constants)
initial.Add(constant, true);
return initial;
}
@@ -547,7 +590,6 @@ namespace Microsoft.Boogie.Houdini { private void FlushWorkList(HoudiniState current) {
this.NotifyFlushStart();
- VCExpr axiom = BuildAxiom(current.Assignment);
while (current.WorkQueue.Count > 0) {
this.NotifyIteration();
@@ -557,7 +599,7 @@ namespace Microsoft.Boogie.Houdini { HoudiniSession session;
houdiniSessions.TryGetValue(current.Implementation, out session);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = TryCatchVerify(session, axiom, out errors);
+ ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);
UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
this.NotifyOutcome(outcome);
@@ -573,24 +615,19 @@ namespace Microsoft.Boogie.Houdini { }
current.Assignment.Remove(refAnnot.Constant);
current.Assignment.Add(refAnnot.Constant, false);
- this.NotifyConstant(refAnnot.Constant);
- }
-
- private void AddToWorkList(HoudiniState current, Implementation imp) {
- if (!current.WorkQueue.Contains(imp) && !current.isBlackListed(imp.Name)) {
- current.WorkQueue.Enqueue(imp);
- this.NotifyEnqueue(imp);
- }
+ this.NotifyConstant(refAnnot.Constant.Name);
}
private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {
Contract.Assume(current.Implementation != null);
foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) {
- AddToWorkList(current, implementation);
+ if (!current.isBlackListed(implementation.Name)) {
+ current.WorkQueue.Enqueue(implementation);
+ this.NotifyEnqueue(implementation);
+ }
}
}
-
// Updates the worklist and current assignment
// @return true if the current function is dequeued
private bool UpdateAssignmentWorkList(HoudiniState current,
@@ -654,11 +691,11 @@ namespace Microsoft.Boogie.Houdini { private class HoudiniState {
private WorkQueue _workQueue;
private HashSet<string> blackList;
- private Dictionary<string, bool> _assignment;
+ private Dictionary<Variable, bool> _assignment;
private Implementation _implementation;
private HoudiniOutcome _outcome;
- public HoudiniState(WorkQueue workQueue, Dictionary<string, bool> currentAssignment) {
+ public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {
this._workQueue = workQueue;
this._assignment = currentAssignment;
this._implementation = null;
@@ -669,7 +706,7 @@ namespace Microsoft.Boogie.Houdini { public WorkQueue WorkQueue {
get { return this._workQueue; }
}
- public Dictionary<string, bool> Assignment {
+ public Dictionary<Variable, bool> Assignment {
get { return this._assignment; }
}
public Implementation Implementation {
@@ -688,8 +725,8 @@ namespace Microsoft.Boogie.Houdini { }
public HoudiniOutcome PerformHoudiniInference() {
- HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
+ this.NotifyStart(program, houdiniConstants.Count);
foreach (Implementation impl in vcgenFailures) {
current.addToBlackList(impl.Name);
}
@@ -705,23 +742,31 @@ namespace Microsoft.Boogie.Houdini { HoudiniVerifyCurrent(session, current);
}
this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
+ Dictionary<string, bool> assignment = new Dictionary<string, bool>();
+ foreach (var x in current.Assignment)
+ assignment[x.Key.Name] = x.Value;
+ current.Outcome.assignment = assignment;
return current.Outcome;
}
private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {
+ HoudiniSession session;
List<Implementation> implementations = new List<Implementation>();
switch (refutedAnnotation.Kind) {
case RefutedAnnotationKind.REQUIRES:
foreach (Implementation callee in callGraph.Successors(currentImplementation)) {
+ houdiniSessions.TryGetValue(callee, out session);
Contract.Assume(callee.Proc != null);
- if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
+ if (callee.Proc.Equals(refutedAnnotation.CalleeProc) && session.InUnsatCore(refutedAnnotation.Constant))
implementations.Add(callee);
}
break;
case RefutedAnnotationKind.ENSURES:
- foreach (Implementation caller in callGraph.Predecessors(currentImplementation))
- implementations.Add(caller);
+ foreach (Implementation caller in callGraph.Predecessors(currentImplementation)) {
+ houdiniSessions.TryGetValue(caller, out session);
+ if (session.InUnsatCore(refutedAnnotation.Constant))
+ implementations.Add(caller);
+ }
break;
case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
break;
@@ -734,11 +779,11 @@ namespace Microsoft.Boogie.Houdini { private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };
private class RefutedAnnotation {
- private string _constant;
+ private Variable _constant;
private RefutedAnnotationKind _kind;
private Procedure _callee;
- private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {
+ private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee) {
this._constant = constant;
this._kind = kind;
this._callee = callee;
@@ -746,19 +791,19 @@ namespace Microsoft.Boogie.Houdini { public RefutedAnnotationKind Kind {
get { return this._kind; }
}
- public string Constant {
+ public Variable Constant {
get { return this._constant; }
}
public Procedure CalleeProc {
get { return this._callee; }
}
- public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {
+ public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee) {
return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee);
}
- public static RefutedAnnotation BuildRefutedEnsures(string constant) {
+ public static RefutedAnnotation BuildRefutedEnsures(Variable constant) {
return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null);
}
- public static RefutedAnnotation BuildRefutedAssert(string constant) {
+ public static RefutedAnnotation BuildRefutedAssert(Variable constant) {
return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null);
}
@@ -766,7 +811,7 @@ namespace Microsoft.Boogie.Houdini { private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {
Expr cond = err.FailingRequires.Condition;
- string houdiniConst;
+ Variable houdiniConst;
if (MatchCandidate(cond, out houdiniConst)) {
xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
}
@@ -774,7 +819,7 @@ namespace Microsoft.Boogie.Houdini { private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {
Expr cond = err.FailingEnsures.Condition;
- string houdiniConst;
+ Variable houdiniConst;
if (MatchCandidate(cond, out houdiniConst)) {
xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
}
@@ -782,7 +827,7 @@ namespace Microsoft.Boogie.Houdini { private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {
Expr cond = err.FailingAssert.OrigExpr;
- string houdiniConst;
+ Variable houdiniConst;
if (MatchCandidate(cond, out houdiniConst)) {
xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
}
@@ -809,7 +854,7 @@ namespace Microsoft.Boogie.Houdini { }
private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
- string houdiniConstant;
+ Variable houdiniConstant;
CallCounterexample callCounterexample = error as CallCounterexample;
if (callCounterexample != null) {
Procedure failingProcedure = callCounterexample.FailingCall.Proc;
@@ -839,10 +884,10 @@ namespace Microsoft.Boogie.Houdini { return null;
}
- private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, VCExpr axiom, out List<Counterexample> errors) {
+ private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {
ProverInterface.Outcome outcome;
try {
- outcome = session.Verify(checker, axiom, out errors);
+ outcome = session.Verify(proverInterface, assignment, out errors);
}
catch (UnexpectedProverOutputException upo) {
Contract.Assume(upo != null);
@@ -854,12 +899,11 @@ namespace Microsoft.Boogie.Houdini { private void HoudiniVerifyCurrent(HoudiniSession session, HoudiniState current) {
while (true) {
- VCExpr currentAx = BuildAxiom(current.Assignment);
this.NotifyAssignment(current.Assignment);
//check the VC with the current assignment
List<Counterexample> errors;
- ProverInterface.Outcome outcome = TryCatchVerify(session, currentAx, out errors);
+ ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors);
this.NotifyOutcome(outcome);
DebugRefutedCandidates(current.Implementation, errors);
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 08322ebb..014af458 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -78,14 +78,14 @@ namespace Microsoft.Boogie.SMTLib SetupProcess();
- if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
{
// Prepare for ApiChecker usage
if (options.LogFilename != null && currentLogFile == null)
{
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ProcedureCopyBound > 0)
+ if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
@@ -770,6 +770,14 @@ namespace Microsoft.Boogie.SMTLib SendThisVC(a);
}
+ public override void DefineMacro(Function fun, VCExpr vc) {
+ DeclCollector.AddFunction(fun);
+ string name = Namer.GetName(fun, fun.Name);
+ string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";
+ AssertAxioms();
+ SendThisVC(a);
+ }
+
public override void AssertAxioms()
{
FlushAxioms();
@@ -805,7 +813,9 @@ namespace Microsoft.Boogie.SMTLib nameCounter++;
nameToAssumption.Add(name, i);
- SendThisVC(string.Format("(assert (! {0} :named {1}))", VCExpr2String(vc, 1), name));
+ string vcString = VCExpr2String(vc, 1);
+ AssertAxioms();
+ SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
i++;
}
Check();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 05a6caf3..a4bdee51 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -164,6 +164,11 @@ void ObjectInvariant() return TypeToString(t);
}
+ public void AddFunction(Function func) {
+ if (KnownFunctions.Contains(func))
+ return;
+ KnownFunctions.Add(func);
+ }
public override bool Visit(VCExprNAry node, bool arg) {
Contract.Requires(node != null);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index f9999a74..9ebf4d63 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -851,9 +851,14 @@ namespace Microsoft.Boogie { public abstract ProverContext Context {
get;
}
+
public abstract VCExpressionGenerator VCExprGen {
get;
}
+
+ public virtual void DefineMacro(Function fun, VCExpr vc) {
+ throw new NotImplementedException();
+ }
}
public class ProverInterfaceContracts : ProverInterface {
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 98f20d21..ea17983f 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -210,7 +210,7 @@ namespace VC var bet = ctx.BoogieExprTranslator;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : bet.LookupVariable(info.controlFlowVariable);
- VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker));
+ VCExpr vcexpr = gen.Not(GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context));
Contract.Assert(vcexpr != null);
if (!CommandLineOptions.Clo.UseLabels) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
@@ -438,8 +438,11 @@ namespace VC checker2.Pop();
var end = DateTime.UtcNow;
- Console.WriteLine("Summary computation took {0} sec and inferred {1} of {2} contracts",
- (end - start).TotalSeconds, found, calls.allSummaryConst.Count);
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
+ {
+ Console.WriteLine(">> Summary computation took {0} sec and inferred {1} of {2} contracts",
+ (end - start).TotalSeconds, found, calls.allSummaryConst.Count);
+ }
}
@@ -1263,7 +1266,7 @@ namespace VC Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
var exprGen = checker.TheoremProver.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker);
+ vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker.TheoremProver.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)));
@@ -1570,7 +1573,7 @@ namespace VC foreach (int id in calls.currCandidates)
{
- if (calls.isNonTrivialCandidate(id) && calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)
+ if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)
{
toExpand.Add(id);
}
@@ -1754,7 +1757,14 @@ namespace VC if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
{
Console.Write(">> SI Inlining: ");
- reporter.candidatesToExpand.ForEach(c => Console.Write("{0} ", calls.getProc(c)));
+ reporter.candidatesToExpand.ForEach(c =>
+ { if (!calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });
+
+ Console.WriteLine();
+ Console.Write(">> SI Skipping: ");
+ reporter.candidatesToExpand.ForEach(c =>
+ { if (calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });
+
Console.WriteLine();
}
// Expand and try again
@@ -1790,7 +1800,7 @@ namespace VC Console.WriteLine(">> SI: Calls to Z3: {0}", vState.numQueries);
Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
- Console.WriteLine(">> SI: Nontrivial Candidates left: {0}", calls.numNonTrivialCandidates());
+ Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => calls.isSkipped(i)).Count());
Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
}
#endregion
@@ -2171,11 +2181,11 @@ namespace VC reporter.underapproximationMode = true;
checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
List<VCExpr> assumptions = new List<VCExpr>();
- List<int> ids = new List<int>();
+
foreach (int id in calls.currCandidates)
{
- assumptions.Add(calls.getFalseExpr(id));
- ids.Add(id);
+ if (!calls.isSkipped(id))
+ assumptions.Add(calls.getFalseExpr(id));
}
Outcome ret = checker.CheckAssumptions(assumptions);
checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
@@ -2211,11 +2221,14 @@ namespace VC foreach (int id in calls.currCandidates)
{
+ if (calls.isSkipped(id)) continue;
+
int idBound = calls.getRecursionBound(id);
if (idBound <= bound)
{
if (idBound > 1)
softAssumptions.Add(calls.getFalseExpr(id));
+
if (block.Contains(id))
{
Contract.Assert(useSummary);
@@ -2287,6 +2300,9 @@ namespace VC // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {
+ // Skipped calls don't get inlined
+ candidates = candidates.FindAll(id => !vState.calls.isSkipped(id));
+
vState.expansionCount += candidates.Count;
if (incremental)
@@ -2503,7 +2519,7 @@ namespace VC var exprGen = checker.TheoremProver.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker);
+ vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker.TheoremProver.Context);
if (!CommandLineOptions.Clo.UseLabels) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
@@ -2859,37 +2875,23 @@ namespace VC return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);
}
- // How many of the current candidates represent calls to procedures
- // with non-trivial mod sets.
- // This is only used for statistic purposes
- public bool isNonTrivialCandidate(int id)
+ // Is this candidate a "skipped" call
+ // Currently this is experimental
+ public bool isSkipped(int id)
{
- string proc = getProc(id);
- if (proc == "") return false;
- if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;
- var info = implName2StratifiedInliningInfo[proc];
- if (info.impl.Proc.Modifies.Length != 0) return true;
- return false;
- /*
- foreach (IdentifierExpr ie in info.impl.Proc.Modifies)
- {
- if (ie.Decl.Name.StartsWith("Mem_") || ie.Decl.Name.StartsWith("Res_"))
- {
- return true;
- }
- }
- return false;
- */
- }
+ if (!CommandLineOptions.Clo.BctModeForStratifiedInlining) return false;
- public int numNonTrivialCandidates()
- {
- int ret = 0;
- foreach (int id in currCandidates)
- {
- if (isNonTrivialCandidate(id)) ret++;
- }
- return ret;
+ var proc = getProc(id);
+ if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;
+ var modSet = new HashSet<string>();
+ implName2StratifiedInliningInfo[proc].impl.Proc.Modifies
+ .Cast<IdentifierExpr>()
+ .Select(ie => ie.Decl.Name)
+ .Iter(s => modSet.Add(s));
+ modSet.Remove("$Alloc");
+ modSet.Remove("assertsPassed");
+ modSet.Remove("$Exception");
+ return modSet.Count == 0;
}
// Finds labels and changes them:
@@ -3453,7 +3455,7 @@ namespace VC if (underapproximationMode)
{
var cex = GenerateTraceMain(labels, model, mvInfo);
- Debug.Assert(candidatesToExpand.Count == 0);
+ Debug.Assert(candidatesToExpand.All(calls.isSkipped));
if (cex != null) {
GetModelWithStates(model);
callback.OnCounterexample(cex, null);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 008810cb..5761ca70 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -611,7 +611,7 @@ namespace VC { var exprGen = ch.TheoremProver.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch);
+ VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels) {
@@ -1550,7 +1550,7 @@ namespace VC { var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker);
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels) {
@@ -1630,20 +1630,20 @@ namespace VC { }
#endregion
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)
{
Contract.Requires(impl != null);
- Contract.Requires(ch != null);
+ Contract.Requires(proverContext != null);
Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
label2absy = new Hashtable/*<int, Absy!>*/();
- return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, ch);
+ return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
}
- protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {
+ protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {
Contract.Requires(impl != null);
- Contract.Requires(ch != null);
+ Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
TypecheckingContext tc = new TypecheckingContext(null);
@@ -1653,35 +1653,35 @@ namespace VC { int assertionCount;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Structured:
- vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context, out assertionCount);
+ vc = VCViaStructuredProgram(impl, label2absy, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Block:
- vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context, out assertionCount);
+ vc = FlatBlockVC(impl, label2absy, false, false, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockReach:
- vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context, out assertionCount);
+ vc = FlatBlockVC(impl, label2absy, false, true, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Local:
- vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context, out assertionCount);
+ vc = FlatBlockVC(impl, label2absy, true, false, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNested:
- vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context, out assertionCount);
+ vc = NestedBlockVC(impl, label2absy, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNestedReach:
- vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context, out assertionCount);
+ vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Dag:
if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
- vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
+ vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), proverContext, out assertionCount);
} else {
- vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);
+ vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, ch.TheoremProver.Context, out assertionCount);
+ vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Doomed:
- vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context, out assertionCount);
+ vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
break;
default:
Contract.Assert(false);
|