Add support for identifying unnecessary assumes.

4 files changed, 29 insertions, 0 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);