Add support for identifying unnecessary assumes.

9 files changed, 109 insertions, 16 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d2243085..8be4f24e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -696,6 +696,8 @@ namespace Microsoft.Boogie {
       }
     }
 
+    public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+
     public IEnumerable<Block> Blocks()
     {
       return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 404945a9..c33f0743 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie {
       } finally {
         rc.TypeBinderState = previousTypeBinderState;
       }
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
 
     public override void AddAssignedVariables(List<Variable> vars) {
@@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie {
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       Expr.Resolve(rc);
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
     public override void AddAssignedVariables(List<Variable> vars) {
       //Contract.Requires(vars != null);
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 3892bbc0..e9aa3ceb 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -479,6 +479,8 @@ namespace Microsoft.Boogie {
     public string AbstractHoudini = null;
     public bool UseUnsatCoreForContractInfer = false;
     public bool PrintAssignment = false;
+    // TODO(wuestholz): Add documentation for this flag.
+    public bool PrintNecessaryAssumes = false;
     public int InlineDepth = -1;
     public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
     public bool UseUncheckedContracts = false;
@@ -1619,6 +1621,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+              ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) ||
               ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
       varContext = varContext.ParentContext;
     }
 
+    public readonly ISet<string> StatementIds = new HashSet<string>();
+
+    public void AddStatementId(IToken tok, string name)
+    {
+      if (StatementIds.Contains(name))
+      {
+        Error(tok, "more than one statement with same id: " + name);
+        return;
+      }
+      StatementIds.Add(name);
+    }
+
     public void AddVariable(Variable var, bool global) {
       Contract.Requires(var != null);
       var previous = FindVariable(cce.NonNull(var.Name), !global);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 9623139a..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1008,6 +1008,11 @@ namespace Microsoft.Boogie
         CleanupCheckers(requestId);
       }
 
+      if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any())
+      {
+        Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes));
+      }
+
       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
 
       outputCollector.WriteMoreOutput();
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..cb8442e5 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -246,9 +246,9 @@ namespace Microsoft.Boogie.SMTLib
 
         // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value
         // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )
-        if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)))
         {
-          SendThisVC("(set-option :produce-unsat-cores true)");
+          SendCommon("(set-option :produce-unsat-cores true)");
           this.usingUnsatCore = true;
         }
 
@@ -408,6 +408,15 @@ namespace Microsoft.Boogie.SMTLib
 
       SendThisVC("(push 1)");
       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
+      if (NamedAssumeVars != null)
+      {
+        foreach (var v in NamedAssumeVars)
+        {
+          SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name));
+        }
+      }
+
       SendThisVC(vcString);
       FlushLogFile();
 
@@ -446,6 +455,7 @@ namespace Microsoft.Boogie.SMTLib
       if (options.Solver == SolverKind.Z3)
       {
         this.gen = gen;
+        SendThisVC("(reset)");
         Namer.Reset();
         common.Clear();
         SetupAxiomBuilder(gen);
@@ -1264,6 +1274,22 @@ namespace Microsoft.Boogie.SMTLib
             
             result = GetResponse();
 
+            var reporter = handler as VC.VCGen.ErrorReporter;
+            // TODO(wuestholz): Is the reporter ever null?
+            if (NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
+            {
+              SendThisVC("(get-unsat-core)");
+              var resp = Process.GetProverResponse();
+              if (resp.Name != "")
+              {
+                 reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+              }
+              foreach (var arg in resp.Arguments)
+              {
+                reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+              }
+            }
+
             if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
             {
               #region Run timeout diagnostics
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..da445a00 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(descriptiveName != null);
       Contract.Requires(vc != null);
       Contract.Requires(handler != null);
@@ -357,9 +357,18 @@ namespace Microsoft.Boogie {
       outputExn = null;
       this.handler = handler;
 
-      thmProver.Reset(gen);
+      if (namedAssumeVars != null && namedAssumeVars.Any())
+      {
+        // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug.
+        thmProver.FullReset(gen);
+      }
+      else
+      {
+        thmProver.Reset(gen);
+      }
       SetTimeout();
       proverStart = DateTime.UtcNow;
+      thmProver.NamedAssumeVars = namedAssumeVars;
       thmProver.BeginCheck(descriptiveName, vc, handler);
       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy
 
@@ -386,6 +395,9 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------
 
   public abstract class ProverInterface {
+
+    public IList<VCExprVar> NamedAssumeVars;
+
     public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
       Contract.Requires(prog != null);
 
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 79f56934..2762fc72 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,7 +1386,8 @@ namespace VC {
         var exprGen = ctx.ExprGen;
         VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
 
-        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
+        var namedAssumeVars = new List<VCExprVar>();
+        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
         Contract.Assert(vc != null);
 
         if (!CommandLineOptions.Clo.UseLabels)
@@ -1414,7 +1415,7 @@ namespace VC {
         string desc = cce.NonNull(impl.Name);
         if (no >= 0)
           desc += "_split" + no;
-        checker.BeginCheck(desc, vc, reporter);
+        checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
       }
 
       private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1519,7 +1520,7 @@ namespace VC {
         }
     }
 
-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
     {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
@@ -1527,10 +1528,10 @@ namespace VC {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       label2absy = new Dictionary<int, Absy>();
-      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
     }
 
-    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1567,7 +1568,8 @@ namespace VC {
           }
           break;
         case CommandLineOptions.VCVariety.DagIterative:
-          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
+          // TODO(wuestholz): Support named assume statements not just for this encoding.
+          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
           break;
         case CommandLineOptions.VCVariety.Doomed:
           vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -2021,6 +2023,16 @@ namespace VC {
       protected ProverContext/*!*/ context;
       Program/*!*/ program;
 
+      public IEnumerable<string> NecessaryAssumes
+      {
+        get { return program.NecessaryAssumes; }
+      }
+
+      public void AddNecessaryAssume(string id)
+      {
+        program.NecessaryAssumes.Add(id);
+      }
+
       public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
           Dictionary<int, Absy>/*!*/ label2absy,
           List<Block/*!*/>/*!*/ blocks,
@@ -3192,7 +3204,7 @@ namespace VC {
                                  Dictionary<int, Absy> label2absy,
                                  ProverContext proverCtxt,
                                  out int assertionCount,
-                                 bool isPositiveContext = true)
+                                 bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
     {
       Contract.Requires(blocks != null);
       Contract.Requires(proverCtxt != null);
@@ -3252,7 +3264,7 @@ namespace VC {
         }
 
         VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
-        VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+        VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
         assertionCount += context.AssertionCount;
 
         VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..74b77188 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -48,7 +48,7 @@ namespace VC {
   
   public class Wlp
   {
-    public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
+    public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null)
       //modifies ctxt.*;
     {
       Contract.Requires(b != null);
@@ -63,7 +63,7 @@ namespace VC {
 
       for (int i = b.Cmds.Count; --i >= 0; )
       {
-        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
+        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars);
       }
       
       int id = b.UniqueId;
@@ -87,7 +87,7 @@ namespace VC {
     /// <summary>
     /// Computes the wlp for an assert or assume command "cmd".
     /// </summary>
-    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+    internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(cmd != null);
       Contract.Requires(N != null);
       Contract.Requires(ctxt != null);
@@ -190,7 +190,16 @@ namespace VC {
             }
           }
         }
-        return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+        var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+        
+        var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (aid != null && namedAssumeVars != null)
+        {
+          var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+          namedAssumeVars.Add(v);
+          expr = gen.ImpliesSimp(v, expr);
+        }
+        return gen.ImpliesSimp(expr, N);
       } else {
         Console.WriteLine(cmd.ToString());
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command