Added functionality for race error reporting.

5 files changed, 338 insertions, 66 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index af7a6cdb..31b7c776 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -353,6 +353,7 @@ namespace GPUVerify
 

         internal void doit()

         {

+            File.Delete(Path.GetFileNameWithoutExtension(CommandLineOptions.inputFiles[0]) + ".loc"); 

             if (CommandLineOptions.Unstructured)

             {

                 Microsoft.Boogie.CommandLineOptions.Clo.PrintUnstructured = 2;

@@ -1669,6 +1670,16 @@ namespace GPUVerify
             return new GlobalVariable(v.tok, new TypedIdent(v.tok, MakeOffsetVariableName(v.Name, ReadOrWrite), IndexType(v)));

         }

 

+        internal static string MakeSourceVariableName(string Name, string AccessType)

+        {

+          return "_" + AccessType + "_SOURCE_" + Name;

+        }

+

+        internal static GlobalVariable MakeSourceVariable(Variable v, string ReadOrWrite)

+        {

+          return new GlobalVariable(v.tok, new TypedIdent(v.tok, MakeSourceVariableName(v.Name, ReadOrWrite), IndexType(v)));

+        }

+

         public static Microsoft.Boogie.Type IndexType(Variable v)

         {

             Debug.Assert(v.TypedIdent.Type is MapType);

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index b6d6acc4..cc13fb00 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -1,5 +1,6 @@
 using System;

 using System.Collections.Generic;

+using System.IO;

 using System.Linq;

 using System.Text;

 using System.Diagnostics;

@@ -13,6 +14,8 @@ namespace GPUVerify {
 

     private QKeyValue SourceLocationAttributes = null;

 

+    private int CurrStmtNo = 1;

+

     public IKernelArrayInfo NonLocalStateToCheck;

 

     private Dictionary<string, Procedure> RaceCheckingProcedures = new Dictionary<string, Procedure>();

@@ -363,8 +366,11 @@ namespace GPUVerify {
     }

 

     private void AddLogAndCheckCalls(CmdSeq result, AccessRecord ar, string Access) {

-      ExprSeq inParams = new ExprSeq();

-      inParams.Add(ar.Index);

+      ExprSeq inParamsLog = new ExprSeq();

+      ExprSeq inParamsChk = new ExprSeq();

+      inParamsChk.Add(ar.Index);

+      inParamsLog.Add(ar.Index);

+      inParamsLog.Add(new LiteralExpr(Token.NoToken, BigNum.FromInt(CurrStmtNo), 32));

 

       Procedure logProcedure = GetRaceCheckingProcedure(Token.NoToken, "_LOG_" + Access + "_" + ar.v.Name);

       Procedure checkProcedure = GetRaceCheckingProcedure(Token.NoToken, "_CHECK_" + Access + "_" + ar.v.Name);

@@ -372,15 +378,26 @@ namespace GPUVerify {
       verifier.OnlyThread1.Add(logProcedure.Name);

       verifier.OnlyThread2.Add(checkProcedure.Name);

 

-      CallCmd logAccessCallCmd = new CallCmd(Token.NoToken, logProcedure.Name, inParams, new IdentifierExprSeq());

+      CallCmd logAccessCallCmd = new CallCmd(Token.NoToken, logProcedure.Name, inParamsLog, new IdentifierExprSeq());

       logAccessCallCmd.Proc = logProcedure;

 

-      CallCmd checkAccessCallCmd = new CallCmd(Token.NoToken, checkProcedure.Name, inParams, new IdentifierExprSeq());

+      CallCmd checkAccessCallCmd = new CallCmd(Token.NoToken, checkProcedure.Name, inParamsChk, new IdentifierExprSeq());

       checkAccessCallCmd.Proc = checkProcedure;

       checkAccessCallCmd.Attributes = SourceLocationAttributes;

 

       result.Add(logAccessCallCmd);

       result.Add(checkAccessCallCmd);

+

+      string fname = QKeyValue.FindStringAttribute(SourceLocationAttributes, "fname");

+      if (fname != null)

+      {

+        writeSourceLocToFile(SourceLocationAttributes, Path.GetFileNameWithoutExtension(CommandLineOptions.inputFiles[0]) + ".loc");

+      }

+      else

+      {

+        Debug.Assert(false, "RaceInstrumenter.AddLogAndCheckCalls: Could not write sourceloc to file as filename could not be found.\n");

+      }

+      CurrStmtNo++;

     }

 

     private BigBlock AddRaceCheckCalls(BigBlock bb) {

@@ -446,10 +463,12 @@ namespace GPUVerify {
       MapType mt = v.TypedIdent.Type as MapType;

       Debug.Assert(mt.Arguments.Length == 1);

       Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Variable SourceParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_source", mt.Arguments[0]));

       Debug.Assert(!(mt.Result is MapType));

 

       inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

       inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

+      inParams.Add(new VariableDualiser(1, null, null).VisitVariable(SourceParameter.Clone() as Variable));

 

       string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;

 

@@ -612,6 +631,7 @@ namespace GPUVerify {
 

       Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);

       Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);

+      Variable AccessSourceVariable = GPUVerifier.MakeSourceVariable(v, Access);

 

       Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

@@ -619,6 +639,7 @@ namespace GPUVerify {
       MapType mt = v.TypedIdent.Type as MapType;

       Debug.Assert(mt.Arguments.Length == 1);

       Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Variable SourceParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_source", mt.Arguments[0]));

       Debug.Assert(!(mt.Result is MapType));

 

       VariableSeq locals = new VariableSeq();

@@ -636,6 +657,9 @@ namespace GPUVerify {
       simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable),

           Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),

           new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));

+      simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessSourceVariable),

+          Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),

+          new IdentifierExpr(v.tok, VariableForThread(1, SourceParameter))));

 

       bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));

 

@@ -674,6 +698,7 @@ namespace GPUVerify {
         WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

         WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),

                                         new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+

         if (!verifier.ArrayModelledAdversarially(v)) {

           WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(

               MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

@@ -688,8 +713,8 @@ namespace GPUVerify {
         WriteReadGuard = Expr.Not(WriteReadGuard);

 

         Requires NoWriteReadRaceRequires = new Requires(false, WriteReadGuard);

-        NoWriteReadRaceRequires.Attributes = new QKeyValue(Token.NoToken, "write_read_race",

-          new List<object>(new object[] { }), null);

+        QKeyValue kv = new QKeyValue(Token.NoToken, "write_read", new List<object>(), null);

+        NoWriteReadRaceRequires.Attributes = new QKeyValue(Token.NoToken, "race", new List<object>(), kv);

         CheckAccessProcedure.Requires.Add(NoWriteReadRaceRequires);

       }

       else {

@@ -716,8 +741,8 @@ namespace GPUVerify {
 

         WriteWriteGuard = Expr.Not(WriteWriteGuard);

         Requires NoWriteWriteRaceRequires = new Requires(false, WriteWriteGuard);

-        NoWriteWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "write_write_race",

-          new List<object>(new object[] { }), null);

+        QKeyValue kv = new QKeyValue(Token.NoToken, "write_write", new List<object>(), null);

+        NoWriteWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "race", new List<object>(), kv);

         CheckAccessProcedure.Requires.Add(NoWriteWriteRaceRequires);

 

         // Check write by thread 2 does not conflict with read by thread 1

@@ -741,8 +766,8 @@ namespace GPUVerify {
 

         ReadWriteGuard = Expr.Not(ReadWriteGuard);

         Requires NoReadWriteRaceRequires = new Requires(false, ReadWriteGuard);

-        NoReadWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "read_write_race",

-          new List<object>(new object[] { }), null);

+        kv = new QKeyValue(Token.NoToken, "read_write", new List<object>(), null);

+        NoReadWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "race", new List<object>(), kv);

         CheckAccessProcedure.Requires.Add(NoReadWriteRaceRequires);

 

       }

@@ -897,6 +922,15 @@ namespace GPUVerify {
       return implication;

     }

 

+    private void writeSourceLocToFile(QKeyValue kv, string path) {

+      TextWriter tw = new StreamWriter(path, true);

+      tw.Write("\n" + QKeyValue.FindIntAttribute(SourceLocationAttributes, "line", -1) 

+                    + "#" + QKeyValue.FindIntAttribute(SourceLocationAttributes, "col", -1) 

+                    + "#" + QKeyValue.FindStringAttribute(SourceLocationAttributes, "fname") 

+                    + "#" + QKeyValue.FindStringAttribute(SourceLocationAttributes, "dir"));

+      tw.Close();

+    }

+    

     protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {

       Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);

       if (expr != null) {

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
index a3423b42..cf34c132 100644
--- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
@@ -11,10 +11,12 @@
 namespace Microsoft.Boogie

 {

   using System;

-  using System.IO;

   using System.Collections;

   using System.Collections.Generic;

+  using System.IO;

+  using System.Text.RegularExpressions;

   using PureCollections;

+  using Microsoft.Basetypes;

   using Microsoft.Boogie;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

@@ -271,6 +273,27 @@ namespace Microsoft.Boogie
           ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

     }

 

+    static QKeyValue GetAttributes(Absy a)

+    {

+      if (a is PredicateCmd)

+      {

+        return (a as PredicateCmd).Attributes;

+      }

+      else if (a is Requires)

+      {

+        return (a as Requires).Attributes;

+      }

+      else if (a is Ensures)

+      {

+        return (a as Ensures).Attributes;

+      }

+      else if (a is CallCmd)

+      {

+        return (a as CallCmd).Attributes;

+      }

+      //Debug.Assert(false);

+      return null;

+    }

 

     /// <summary>

     /// Inform the user about something and proceed with translation normally.

@@ -322,35 +345,14 @@ namespace Microsoft.Boogie
       string failFile = null;

       string locinfo  = null;

 

-      if (node is PredicateCmd)

-      {

-        PredicateCmd c = (PredicateCmd)node;

-        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

-        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

-        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

-      }

-      else if (node is Requires)

+      QKeyValue attrs = GetAttributes(node);

+      if (node != null)

       {

-        Requires c = (Requires)node;

-        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

-        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

-        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

+        failLine = QKeyValue.FindIntAttribute(attrs, "line", -1);

+        failCol = QKeyValue.FindIntAttribute(attrs, "col", -1);

+        failFile = QKeyValue.FindStringAttribute(attrs, "fname");

       }

-      else if (node is Ensures)

-      {

-        Ensures c = (Ensures)node;

-        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

-        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

-        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

-      }

-      else if (node is CallCmd)

-      {

-        CallCmd c = (CallCmd)node;

-        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

-        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

-        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

-      }

-

+      

       if (showBplLocation && failLine != -1 && failCol != -1 && failFile != null)

       {

         locinfo = "File: \t"  + failFile +

@@ -570,7 +572,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    static QKeyValue extractSourcelocAttrs(BlockSeq s)

+    static QKeyValue ExtractAsertSourceLocFromTrace(BlockSeq s)

     {

       foreach (Block b in s)

       {

@@ -588,6 +590,141 @@ namespace Microsoft.Boogie
       return null;

     }

 

+    static QKeyValue CreateSourceLocQKV(int line, int col, string fname, string dir)

+    {

+      QKeyValue dirkv = new QKeyValue(Token.NoToken, "dir", new List<object>(new object[] { dir }), null);

+      QKeyValue fnamekv = new QKeyValue(Token.NoToken, "fname", new List<object>(new object[] { fname }), dirkv);

+      QKeyValue colkv = new QKeyValue(Token.NoToken, "col", new List<object>(new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(col)) }), fnamekv);

+      QKeyValue linekv = new QKeyValue(Token.NoToken, "line", new List<object>(new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(line)) }), colkv);

+      return linekv;

+    }

+

+    static QKeyValue GetSourceLocInfo(Counterexample error) {

+      string sourceVarName = null;

+      int sourceLocLineNo = -1;

+      int currLineNo = -1;

+      string fileLine;

+      string[] slocTokens = null;

+      int line = -1;

+      int col = -1;

+      string fname = null;

+      string dir = null;

+      TextReader tr = new StreamReader(Path.GetFileNameWithoutExtension(CommandLineOptions.Clo.Files[0]) + ".loc");

+

+      foreach (Block b in error.Trace)

+      {

+        foreach (Cmd c in b.Cmds)

+        {

+          if (c.ToString().Contains("_SOURCE_")) 

+          {

+            sourceVarName = Regex.Split(c.ToString(), " ")[1];

+          }

+        }

+      }

+      sourceLocLineNo = error.Model.TryGetFunc(sourceVarName).GetConstant().AsInt();

+

+      if (sourceLocLineNo != 0)

+      {

+        while ((fileLine = tr.ReadLine()) != null)

+        {

+          currLineNo++;

+          if (currLineNo == sourceLocLineNo)

+          {

+            break;

+          }

+        }

+        if (currLineNo < sourceLocLineNo)

+        {

+          fileLine = null;

+          Console.WriteLine("sourceLocLineNo greater than number of lines in .loc file ({0} > {1})\n", sourceLocLineNo, (currLineNo + 1));

+          return null;

+        }

+        if (fileLine != null)

+        {

+          slocTokens = Regex.Split(fileLine, "#");

+          line = System.Convert.ToInt32(slocTokens[0]);

+          col = System.Convert.ToInt32(slocTokens[1]);

+          fname = slocTokens[2];

+          dir = slocTokens[3];

+          return CreateSourceLocQKV(line, col, fname, dir);

+        }

+      }

+      else

+      {

+        Console.WriteLine("sourceLocLineNo is 0. No sourceloc at that location.\n");

+        return null;

+      } 

+      tr.Close();

+      return null;

+    }

+

+    static bool IsRepeatedKV(QKeyValue attrs, List<QKeyValue> alreadySeen)

+    {

+      //return false;

+      if (attrs == null)

+      {

+        return false;

+      }

+      string key = null;

+      foreach (QKeyValue qkv in alreadySeen)

+      {

+        QKeyValue kv = qkv.Clone() as QKeyValue;

+        if (kv.Params.Count != attrs.Params.Count) 

+        {

+          return false;

+        }

+        for (; kv != null; kv = kv.Next) {

+          key = kv.Key;

+          if (key != "thread") {

+            if (kv.Params.Count == 0)

+            {

+              if (QKeyValue.FindBoolAttribute(attrs, key))

+              {

+                continue;

+              }

+              else

+              {

+                return false;

+              }

+

+            }

+            else if (kv.Params[0] is LiteralExpr)

+            { // int

+              LiteralExpr l = kv.Params[0] as LiteralExpr;

+              int i = l.asBigNum.ToIntSafe;

+              if (QKeyValue.FindIntAttribute(attrs, key, -1) == i)

+              {

+                continue;

+              }

+              else

+              {

+                return false;

+              }

+            }

+            else if (kv.Params[0] is string)

+            { // string

+              string s = kv.Params[0] as string;

+              if (QKeyValue.FindStringAttribute(attrs, key) == s)

+              {

+                continue;

+              }

+              else

+              {

+                return false;

+              }

+            }

+            else

+            {

+              Debug.Assert(false);

+              return false;

+            }

+          }

+        }

+        return true;

+      }

+      return false;

+    }

+

     static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

                        ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories)

     {

@@ -640,6 +777,15 @@ namespace Microsoft.Boogie
             // BP5xxx: Verification errors

 

             errors.Sort(new CounterexampleComparer());

+            List<QKeyValue> seenAssertAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenReqAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenEnsAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenInvEAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenInvMAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenWWRaceAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenWRRaceAttrs = new List<QKeyValue>();

+            List<QKeyValue> seenRWRaceAttrs = new List<QKeyValue>();

+            bool incrementErrors = true;

             foreach (Counterexample error in errors)

             {

               if (error is CallCounterexample)

@@ -653,10 +799,60 @@ namespace Microsoft.Boogie
                 {

                   ReportBplError(err.FailingCall, "Barrier Divergence Error: \nThe following barrier is reached by non-uniform control flow:", true, true);

                 }

+                else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "race"))

+                {        

+                  int lidx1 = -1, lidy1 = -1, lidz1 = -1, lidx2 = -1, lidy2 = -1, lidz2 = -1;

+                  string thread1 = null, thread2 = null;

+                  if (error.Model != null) 

+                  {

+                    lidx1 = error.Model.TryGetFunc("local_id_x$1").GetConstant().AsInt();

+                    lidy1 = error.Model.TryGetFunc("local_id_y$1").GetConstant().AsInt();

+                    lidz1 = error.Model.TryGetFunc("local_id_z$1").GetConstant().AsInt();

+                    lidx2 = error.Model.TryGetFunc("local_id_x$2").GetConstant().AsInt();

+                    lidy2 = error.Model.TryGetFunc("local_id_y$2").GetConstant().AsInt();

+                    lidz2 = error.Model.TryGetFunc("local_id_z$2").GetConstant().AsInt();

+                    thread1 = "(" + lidx1 + ", " + lidy1 + ", " + lidz1 + ")";

+                    thread2 = "(" + lidx2 + ", " + lidy2 + ", " + lidz2 + ")";

+                  }

+                  if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_read"))

+                  {

+                    err.FailingRequires.Attributes = GetSourceLocInfo(error);

+                    ReportBplError(err.FailingCall, "Race Error: \nWrite-read race caused by thread " 

+                                                        + thread2 + " executing statement at:" , true, true);

+                    ReportBplError(err.FailingRequires, "The conflicting statement executed by thread "

+                                                    + thread1 + " is:", true, true);

+                  }

+                  else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "read_write"))

+                  {

+                    err.FailingRequires.Attributes = GetSourceLocInfo(error);

+                    ReportBplError(err.FailingCall, "Race Error: \nRead-write race caused by thread "

+                                                        + thread2 + " executing statement at:", true, true);

+                    ReportBplError(err.FailingRequires, "The conflicting statement executed by thread "

+                                                    + thread1 + " is:", true, true);

+

+                  }

+                  else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_write"))

+                  {

+                    err.FailingRequires.Attributes = GetSourceLocInfo(error);

+                    ReportBplError(err.FailingCall, "Race Error: \nWrite-write race caused by thread "

+                                                        + thread2 + " executing statement at:", true, true);

+                    ReportBplError(err.FailingRequires, "The conflicting statement executed by thread "

+                                                    + thread1 + " is:", true, true);

+

+                  }

+                }

                 else

                 {

-                  ReportBplError(err.FailingCall, "Requires Error: A precondition for this call might not hold.", true, true);

-                  ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                  if (!IsRepeatedKV(err.FailingRequires.Attributes, seenReqAttrs))

+                  {

+                    ReportBplError(err.FailingCall, "Requires Error: A precondition for this call might not hold.", true, true);

+                    ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                    seenReqAttrs.Add(err.FailingRequires.Attributes);

+                  }

+                  else

+                  {

+                    incrementErrors = false;

+                  }

                 }

                 if (CommandLineOptions.Clo.XmlSink != null)

                 {

@@ -672,8 +868,15 @@ namespace Microsoft.Boogie
                 }

                 else

                 {

-                  ReportBplError(err.FailingReturn, "Ensures Error: A postcondition might not hold on this return path.", true, true);

-                  ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                  if (!IsRepeatedKV(err.FailingEnsures.Attributes, seenEnsAttrs)) {

+                    ReportBplError(err.FailingReturn, "Ensures Error: A postcondition might not hold on this return path.", true, true);

+                    ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                    seenEnsAttrs.Add(err.FailingEnsures.Attributes);

+                  }

+                  else

+                  {

+                    incrementErrors = false;

+                  }

                 }

                 if (CommandLineOptions.Clo.XmlSink != null)

                 {

@@ -685,19 +888,33 @@ namespace Microsoft.Boogie
                 AssertCounterexample err = (AssertCounterexample)error;

                 if (err.FailingAssert is LoopInitAssertCmd)

                 {

-                  ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not hold on entry.", true, true);

-                  if (CommandLineOptions.Clo.XmlSink != null)

+                  if (!IsRepeatedKV(err.FailingAssert.Attributes, seenInvEAttrs)) {

+                    ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not hold on entry.", true, true);

+                    if (CommandLineOptions.Clo.XmlSink != null)

+                    {

+                      CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

+                    }

+                    seenInvEAttrs.Add(err.FailingAssert.Attributes);

+                  }

+                  else

                   {

-                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

+                    incrementErrors = false;

                   }

                 }

                 else if (err.FailingAssert is LoopInvMaintainedAssertCmd)

                 {

                   // this assertion is a loop invariant which is not maintained

-                  ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not be maintained by the loop.", true, true);

-                  if (CommandLineOptions.Clo.XmlSink != null)

+                  if (!IsRepeatedKV(err.FailingAssert.Attributes, seenInvMAttrs)) {

+                    ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not be maintained by the loop.", true, true);

+                    if (CommandLineOptions.Clo.XmlSink != null)

+                    {

+                      CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

+                    }

+                    seenInvMAttrs.Add(err.FailingAssert.Attributes);

+                  }

+                  else

                   {

-                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

+                    incrementErrors = false;

                   }

                 }

                 else

@@ -710,24 +927,17 @@ namespace Microsoft.Boogie
                   {

                     ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

                   }

-                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "write_read_race")) 

-                  {

-                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

-                    ReportBplError(err.FailingAssert, "Race Error: Write-read race caused by statement at:", true, true);

-                  }

-                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "read_write_race")) 

-                  {

-                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

-                    ReportBplError(err.FailingAssert, "Race Error: Read-write race caused by statement at:", true, true);

-                  }

-                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "write_write_race")) 

-                  {

-                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

-                    ReportBplError(err.FailingAssert, "Race Error: Write-write race caused by statement at:", true, true);

-                  }

                   else

                   {

-                    ReportBplError(err.FailingAssert, "Assertion Error: This assertion might not hold.", true, true);

+                    if (!IsRepeatedKV(err.FailingAssert.Attributes, seenAssertAttrs)) 

+                    {

+                      ReportBplError(err.FailingAssert, "Assertion Error: This assertion might not hold.", true, true);

+                      seenAssertAttrs.Add(err.FailingAssert.Attributes.Clone() as QKeyValue);

+                    }

+                    else

+                    {

+                      incrementErrors = false;

+                    }

                   }

                   if (CommandLineOptions.Clo.XmlSink != null)

                   {

@@ -743,16 +953,23 @@ namespace Microsoft.Boogie
                   Console.WriteLine("       " + info);

                 }

               }

+              /* Get rid of this, as we are only using /enhancedErrorMessages to pass the model through. 

+               * We don't actually want to see the enhanced error messages.

+               * 

               if (CommandLineOptions.Clo.ErrorTrace > 0)

               {

                 Console.WriteLine("Execution trace:");

                 error.Print(4);

               }

+               */

               if (CommandLineOptions.Clo.ModelViewFile != null)

               {

                 error.PrintModel();

               }

-              errorCount++;

+              if (incrementErrors)

+              {

+                errorCount++;

+              }

             }

             //}

             Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj
index c4ab1b6f..6f616936 100644
--- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj
@@ -55,6 +55,10 @@
       <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>

       <Name>AIFramework</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Basetypes\Basetypes.csproj">

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

+      <Name>Basetypes</Name>

+    </ProjectReference>

     <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

       <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

       <Name>CodeContractsExtender</Name>

@@ -71,6 +75,10 @@
       <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

       <Name>Houdini</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/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 4fa7f0b7..2ac8dc83 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1819,9 +1819,11 @@ namespace VC {
             if (a is AssertCmd) {

               Bpl.AssertCmd c = (AssertCmd) a;

               Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);

+              b.Attributes = c.Attributes;

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsInit.Add(b);

               b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+              b.Attributes = c.Attributes; 

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsMaintained.Add(b);

               header.Cmds[i] = new AssumeCmd(c.tok,c.Expr);