Did some refactoring, fixed minor issues, and made it apply the more advanced verification result caching even for implementations with errors.

4 files changed, 199 insertions, 6 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9a871e93..2f4b4e8a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2617,6 +2617,71 @@ namespace Microsoft.Boogie {
     public List<Block/*!*/> OriginalBlocks;

     public List<Variable> OriginalLocVars;

 

+    ISet<byte[]> assertionChecksums;

+    public ISet<byte[]> AssertionChecksums

+    {

+      get

+      {

+        return assertionChecksums;

+      }

+    }

+

+    sealed class ChecksumComparer : IEqualityComparer<byte[]>

+    {

+      static IEqualityComparer<byte[]> defaultComparer;

+      public static IEqualityComparer<byte[]> Default

+      {

+        get

+        {

+          if (defaultComparer == null)

+          {

+            defaultComparer = new ChecksumComparer();

+          }

+          return defaultComparer;

+        }

+      }

+

+      public bool Equals(byte[] x, byte[] y)

+      {

+        if (x == null || y == null)

+        {

+          return x == y;

+        }

+        else

+        {

+          return x.SequenceEqual(y);

+        }

+      }

+

+      public int GetHashCode(byte[] checksum)

+      {

+        if (checksum == null)

+        {

+          throw new ArgumentNullException("checksum");

+        }

+        else

+        {

+          var result = 17;

+          for (int i = 0; i < checksum.Length; i++)

+          {

+            result = result * 23 + checksum[i];

+          }

+          return result;

+        }

+      }

+    }

+

+    public void AddAssertionChecksum(byte[] checksum)

+    {

+      if (assertionChecksums == null)

+      {

+        assertionChecksums = new HashSet<byte[]>(ChecksumComparer.Default);

+      }

+      assertionChecksums.Add(checksum);

+    }

+

+    public ISet<byte[]> AssertionChecksumsInPreviousSnapshot { get; set; }

+

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

     [ContractInvariantMethod]

@@ -2688,14 +2753,18 @@ namespace Microsoft.Boogie {
       }

     }

 

-    // TODO(wuestholz): Make this a 'List<Counterexample>'.

-    public IList<object> ErrorsInCachedSnapshot { get; set; }

+    public ISet<byte[]> ErrorChecksumsInCachedSnapshot { get; private set; }

+

+    public void SetErrorChecksumsInCachedSnapshot(IEnumerable<byte[]> errorChecksums)

+    {

+      ErrorChecksumsInCachedSnapshot = new HashSet<byte[]>(errorChecksums, ChecksumComparer.Default);

+    }

 

     public bool NoErrorsInCachedSnapshot

     {

       get

       {

-        return ErrorsInCachedSnapshot != null && !ErrorsInCachedSnapshot.Any();

+        return ErrorChecksumsInCachedSnapshot != null && !ErrorChecksumsInCachedSnapshot.Any();

       }

     }

 

@@ -2703,7 +2772,7 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        return ErrorsInCachedSnapshot != null && ErrorsInCachedSnapshot.Any();

+        return ErrorChecksumsInCachedSnapshot != null && ErrorChecksumsInCachedSnapshot.Any();

       }

     }

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index a7693b00..869c0dfa 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -800,6 +800,8 @@ namespace Microsoft.Boogie {
     [Rep]  //PM: needed to verify Traverse.Visit

     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)

 

+    public byte[] Checksum;

+

     // Abstract interpretation

 

     // public bool currentlyTraversed;

@@ -937,8 +939,104 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

   }

+

+  public static class ChecksumHelper

+  {

+    public static void ComputeChecksums(Cmd cmd, Implementation impl, byte[] currentChecksum = null, bool unordered = false)

+    {

+      if (CommandLineOptions.Clo.VerifySnapshots < 2)

+      {

+        return;

+      }

+

+      var assumeCmd = cmd as AssumeCmd;

+      if (assumeCmd != null

+          && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization"))

+      {

+        // Ignore assumption variable initializations.

+        assumeCmd.Checksum = currentChecksum;

+        return;

+      }

+

+      using (var strWr = new System.IO.StringWriter())

+      using (var tokTxtWr = new TokenTextWriter("<no file>", strWr, false, false))

+      {

+        tokTxtWr.UseForComputingChecksums = true;

+        cmd.Emit(tokTxtWr, 0);

+        var md5 = System.Security.Cryptography.MD5.Create();

+        var str = strWr.ToString();

+        if (str.Any())

+        {

+          var data = System.Text.Encoding.UTF8.GetBytes(str);

+          var checksum = md5.ComputeHash(data);

+          currentChecksum = currentChecksum != null ? CombineChecksums(currentChecksum, checksum, unordered) : checksum;

+        }

+        cmd.Checksum = currentChecksum;

+      }

+

+      var assertCmd = cmd as AssertCmd;

+      if (assertCmd != null && assertCmd.Checksum != null)

+      {

+        var assertRequiresCmd = assertCmd as AssertRequiresCmd;

+        if (assertRequiresCmd != null)

+        {

+          // Add the checksum of the call instead of the assertion itself

+          // because a corresponding counterexample will also have the

+          // checksum of the failing call.

+          impl.AddAssertionChecksum(assertRequiresCmd.Call.Checksum);

+        }

+        else

+        {

+          impl.AddAssertionChecksum(assertCmd.Checksum);

+        }

+      }

+

+      var sugaredCmd = cmd as SugaredCmd;

+      if (sugaredCmd != null)

+      {

+        // The checksum of a sugared command should not depend on the desugaring itself.

+        var stateCmd = sugaredCmd.Desugaring as StateCmd;

+        if (stateCmd != null)

+        {

+          foreach (var c in stateCmd.Cmds)

+          {

+            ComputeChecksums(c, impl, currentChecksum, unordered);

+            currentChecksum = c.Checksum;

+          }

+          sugaredCmd.DesugaringChecksum = currentChecksum;

+        }

+        else

+        {

+          ComputeChecksums(sugaredCmd.Desugaring, impl, currentChecksum, unordered);

+          sugaredCmd.DesugaringChecksum = sugaredCmd.Desugaring.Checksum;

+        }

+      }

+    }

+

+    public static byte[] CombineChecksums(byte[] first, byte[] second, bool unordered = false)

+    {

+      Contract.Requires(first != null && (second == null || first.Length == second.Length));

+

+      var result = (byte[])(first.Clone());

+      for (int i = 0; second != null && i < second.Length; i++)

+      {

+        if (unordered)

+        {

+          result[i] += second[i];

+        }

+        else

+        {

+          result[i] = (byte)(result[i] * 31 ^ second[i]);

+        }

+      }

+      return result;

+    }

+  }

+

   [ContractClass(typeof(CmdContracts))]

   public abstract class Cmd : Absy {

+    public byte[] Checksum { get; internal set; }

+

     public Cmd(IToken/*!*/ tok)

       : base(tok) {

       Contract.Assert(tok != null);

@@ -1046,6 +1144,9 @@ namespace Microsoft.Boogie {
     /// </summary>

     public static void EmitAttributes(TokenTextWriter stream, QKeyValue attributes) {

       Contract.Requires(stream != null);

+

+      if (stream.UseForComputingChecksums) { return; }

+

       for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {

         kv.Emit(stream);

         stream.Write(" ");

@@ -1170,6 +1271,14 @@ namespace Microsoft.Boogie {
     }

 

     public override void Emit(TokenTextWriter stream, int level) {

+      if (stream.UseForComputingChecksums)

+      {

+        var lhs = Lhss.FirstOrDefault() as SimpleAssignLhs;

+        if (lhs != null && lhs.AssignedVariable.Decl != null && QKeyValue.FindBoolAttribute(lhs.AssignedVariable.Decl.Attributes, "assumption"))

+        {

+          return;

+        }

+      }

       

       stream.Write(this, level, "");

 

@@ -1651,6 +1760,8 @@ namespace Microsoft.Boogie {
   abstract public class SugaredCmd : Cmd {

     private Cmd desugaring;  // null until desugared

 

+    public byte[] DesugaringChecksum { get; set; }

+

     public SugaredCmd(IToken/*!*/ tok)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -1702,7 +1813,7 @@ namespace Microsoft.Boogie {
 

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

-      if (CommandLineOptions.Clo.PrintDesugarings) {

+      if (CommandLineOptions.Clo.PrintDesugarings && !stream.UseForComputingChecksums) {

         stream.WriteLine(this, level, "/*** desugaring:");

         Desugaring.Emit(stream, level);

         stream.WriteLine(level, "**** end desugaring */");

@@ -2429,7 +2540,7 @@ namespace Microsoft.Boogie {
       return Conjunction(ensures);

     }

 

-    public Expr Precondition(Procedure procedure, Program program)

+    public Expr CheckedPrecondition(Procedure procedure, Program program)

     {

       Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

 

@@ -2583,6 +2694,11 @@ namespace Microsoft.Boogie {
       stream.Write(this, level, "assert ");

       EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

+      if (1 < CommandLineOptions.Clo.VerifySnapshots && !stream.UseForComputingChecksums)

+      {

+        var cs = Checksum != null ? BitConverter.ToString(Checksum) : "<unknown>";

+        stream.Write(string.Format(" /* checksum: {0} */ ", cs));

+      }

       stream.WriteLine(";");

     }

     public override void Resolve(ResolutionContext rc) {

@@ -2737,6 +2853,9 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

+

+      if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

+

       stream.Write(this, level, "assume ");

       EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index d6dd17c9..ffd95f77 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1802,6 +1802,10 @@ namespace Microsoft.Boogie {
       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

       this.name.Emit(stream, 0xF0, false);

+      if (stream.UseForComputingChecksums && Func.DependenciesChecksum != null)

+      {

+        stream.Write(string.Format("[dependencies_checksum:{0}]", Func.DependenciesChecksum));

+      }

       stream.Write("(");

       args.Emit(stream);

       stream.Write(")");

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 66eefd8c..6aafec7f 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -80,6 +80,7 @@ namespace Microsoft.Boogie {
     bool setTokens = true;

     int line = 1;

     int col;

+    public bool UseForComputingChecksums;

 

     private const int indent_size = 2;

     protected static string Indent(int level) {