path: root/Source/GPUVerify/RaceInstrumenter.cs

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie;
using Microsoft.Basetypes;

namespace GPUVerify {
  class RaceInstrumenter : IRaceInstrumenter {
    protected GPUVerifier verifier;

    private QKeyValue SourceLocationAttributes = null;

    public IKernelArrayInfo NonLocalStateToCheck;

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

    public void setVerifier(GPUVerifier verifier) {
      this.verifier = verifier;
      NonLocalStateToCheck = new KernelArrayInfoLists();
      foreach (Variable v in verifier.KernelArrayInfo.getGlobalArrays()) {
        NonLocalStateToCheck.getGlobalArrays().Add(v);
      }
      foreach (Variable v in verifier.KernelArrayInfo.getGroupSharedArrays()) {
        NonLocalStateToCheck.getGroupSharedArrays().Add(v);
      }
    }

    private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v) {
      // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the
      // loop then there is no point adding an invariant
      //
      // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not
      // contain a barrier, then it is almost certain that a read CAN be
      // pending at the loop head, so the invariant will not hold
      //
      // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will
      // be in the modifies set, but there may not be a live read at the loop
      // head, so it is worth adding the loop invariant candidate.
      //
      // The same reasoning applies for WRITE

      if (verifier.ContainsBarrierCall(region)) {
        if (verifier.ContainsNamedVariable(
            LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ"))) {
          AddNoReadOrWriteCandidateInvariant(region, v, "READ");
        }

        if (verifier.ContainsNamedVariable(
            LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE"))) {
          AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");
        }
      }
    }

    private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v) {
      AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");
      AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");
    }

    private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v) {
      AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");
      AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
    }

    private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite) {
      Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
      verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());
    }

    public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region) {
      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
        AddNoReadOrWriteCandidateInvariants(region, v);
        AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");
        AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");
        AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));
        AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));
      }
    }

    private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag) {
      Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
      verifier.AddCandidateInvariant(region, candidate, tag);
    }

    private bool DoesNotReferTo(Expr expr, string v) {
      FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);
      visitor.VisitExpr(expr);
      return !visitor.found;
    }

    private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType) {
      var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));
      var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);
      var offsetPreds = new List<Expr>();

      foreach (var offset in GetOffsetsAccessed(region, v, accessType)) {
        bool isConstant;
        var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);
        if (def == null)
          continue;

        if (isConstant) {
          offsetPreds.Add(Expr.Eq(offsetExpr, def));
        }
        else {
          var sc = StrideConstraint.FromExpr(verifier, impl, def);
          var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);
          if (pred != null)
            offsetPreds.Add(pred);
        }
      }

      return offsetPreds;
    }

    private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType) {
      KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
      if (iLessThanC.Key != null) {
        foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {
          if (HasFormIPlusLocalIdTimesC(e, iLessThanC, impl)) {
            AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);
            break;
          }
        }

        foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {
          if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl)) {
            AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);
            break;
          }
        }

      }


    }

    private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {
      if (!(e is NAryExpr)) {
        return false;
      }

      NAryExpr nary = e as NAryExpr;

      if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {
        return false;
      }

      return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
          IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
          (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
          IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
    }

    private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl) {
      if (!(maybeLocalIdTimesConstant is NAryExpr)) {
        return false;
      }
      NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;
      if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {
        return false;
      }

      return
          (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||
          (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));
    }


    private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {
      if (!(e is NAryExpr)) {
        return false;
      }

      NAryExpr nary = e as NAryExpr;

      if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {
        return false;
      }

      return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
          IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
          (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
          IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
    }

    private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl) {
      if (!(maybeGlobalIdTimesConstant is NAryExpr)) {
        return false;
      }
      NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;
      if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {
        return false;
      }

      return
          (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||
          (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));
    }


    private bool SameConstant(Expr expr, Expr constant) {
      if (constant is IdentifierExpr) {
        IdentifierExpr identifierExpr = constant as IdentifierExpr;
        Debug.Assert(identifierExpr.Decl is Constant);
        return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);
      }
      else {
        Debug.Assert(constant is LiteralExpr);
        LiteralExpr literalExpr = constant as LiteralExpr;
        if (!(expr is LiteralExpr)) {
          return false;
        }
        if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst)) {
          return false;
        }

        return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;
      }
    }

    private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr) {
      if (!(expr is IdentifierExpr)) {
        return false;
      }
      return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);
    }

    private KeyValuePair<IdentifierExpr, Expr> GetILessThanC(Expr expr) {

      if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool")) {
        expr = (expr as NAryExpr).Args[0];
      }

      if (!(expr is NAryExpr)) {
        return new KeyValuePair<IdentifierExpr, Expr>(null, null);
      }

      NAryExpr nary = expr as NAryExpr;

      if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT"))) {
        return new KeyValuePair<IdentifierExpr, Expr>(null, null);
      }

      if (!(nary.Args[0] is IdentifierExpr)) {
        return new KeyValuePair<IdentifierExpr, Expr>(null, null);
      }

      if (!IsConstant(nary.Args[1])) {
        return new KeyValuePair<IdentifierExpr, Expr>(null, null);
      }

      return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);

    }

    private static bool IsConstant(Expr e) {
      return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);
    }

    private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v) {
      AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
      AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);
    }

    private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v) {
      AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);
      AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
    }

    public void AddKernelPrecondition() {
      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
        AddRequiresNoPendingAccess(v);

        if (!verifier.ArrayModelledAdversarially(v)) {
          IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
          IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
          verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));
        }
      }
    }

    public void AddRaceCheckingInstrumentation() {

      foreach (Declaration d in verifier.Program.TopLevelDeclarations) {
        if (d is Implementation) {
          AddRaceCheckCalls(d as Implementation);
        }
      }

    }

    private void AddRaceCheckingDecsAndProcsForVar(Variable v) {
      AddLogRaceDeclarations(v, "READ");
      AddLogRaceDeclarations(v, "WRITE");
      AddLogAccessProcedure(v, "READ");
      AddCheckAccessProcedure(v, "READ");
      AddLogAccessProcedure(v, "WRITE");
      AddCheckAccessProcedure(v, "WRITE");
    }

    private StmtList AddRaceCheckCalls(StmtList stmtList) {
      Contract.Requires(stmtList != null);

      StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);

      foreach (BigBlock bodyBlock in stmtList.BigBlocks) {
        result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
      }
      return result;
    }

    private Block AddRaceCheckCalls(Block b) {
      b.Cmds = AddRaceCheckCalls(b.Cmds);
      return b;
    }

    private void AddRaceCheckCalls(Implementation impl) {
      if (CommandLineOptions.Unstructured)
        impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
      else
        impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
    }

    private CmdSeq AddRaceCheckCalls(CmdSeq cs) {
      var result = new CmdSeq();
      foreach (Cmd c in cs) {
        result.Add(c);

        if (c is AssertCmd) {
          AssertCmd assertion = c as AssertCmd;
          if (QKeyValue.FindBoolAttribute(assertion.Attributes, "sourceloc")) {
            SourceLocationAttributes = assertion.Attributes;
          }
        }

        if (c is AssignCmd) {
          AssignCmd assign = c as AssignCmd;

          ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
          foreach (var rhs in assign.Rhss)
            rc.Visit(rhs);
          if (rc.accesses.Count > 0) {
            foreach (AccessRecord ar in rc.accesses) {

              ExprSeq inParams = new ExprSeq();
              inParams.Add(ar.Index);

              Procedure logProcedure = GetRaceCheckingProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
              Procedure checkProcedure = GetRaceCheckingProcedure(c.tok, "_CHECK_READ_" + ar.v.Name);

              verifier.OnlyThread1.Add(logProcedure.Name);
              verifier.OnlyThread2.Add(checkProcedure.Name);

              CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
              logAccessCallCmd.Proc = logProcedure;

              CallCmd checkAccessCallCmd = new CallCmd(c.tok, checkProcedure.Name, inParams, new IdentifierExprSeq());
              checkAccessCallCmd.Proc = checkProcedure;
              checkAccessCallCmd.Attributes = SourceLocationAttributes;

              result.Add(logAccessCallCmd);
              result.Add(checkAccessCallCmd);

            }
          }

          foreach (var lhs in assign.Lhss) {
            WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
            wc.Visit(lhs);
            if (wc.GetAccess() != null) {
              AccessRecord ar = wc.GetAccess();

              ExprSeq inParams = new ExprSeq();
              inParams.Add(ar.Index);

              Procedure logProcedure = GetRaceCheckingProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
              Procedure checkProcedure = GetRaceCheckingProcedure(c.tok, "_CHECK_WRITE_" + ar.v.Name);

              verifier.OnlyThread1.Add(logProcedure.Name);
              verifier.OnlyThread2.Add(checkProcedure.Name);

              CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
              CallCmd checkAccessCallCmd = new CallCmd(c.tok, checkProcedure.Name, inParams, new IdentifierExprSeq());

              logAccessCallCmd.Proc = logProcedure;
              checkAccessCallCmd.Proc = checkProcedure;

              result.Add(logAccessCallCmd);
              result.Add(checkAccessCallCmd);

            }
          }
        }
      }
      return result;
    }

    private BigBlock AddRaceCheckCalls(BigBlock bb) {
      BigBlock result = new BigBlock(bb.tok, bb.LabelName, AddRaceCheckCalls(bb.simpleCmds), null, bb.tc);

      if (bb.ec is WhileCmd) {
        WhileCmd WhileCommand = bb.ec as WhileCmd;
        result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard,
                WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));
      }
      else if (bb.ec is IfCmd) {
        IfCmd IfCommand = bb.ec as IfCmd;
        Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
        result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);
      }
      else if (bb.ec is BreakCmd) {
        result.ec = bb.ec;
      }
      else {
        Debug.Assert(bb.ec == null);
      }

      return result;
    }

    private Procedure GetRaceCheckingProcedure(IToken tok, string name) {
      if (RaceCheckingProcedures.ContainsKey(name)) {
        return RaceCheckingProcedures[name];
      }
      Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
      RaceCheckingProcedures[name] = newProcedure;
      return newProcedure;
    }


    public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) {
      BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
      if (Thread == 2) {
        return result;
      }

      Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
      Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

      if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {
        ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
        ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
      }

      result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
      result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));
      return result;
    }

    protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite) {
      VariableSeq inParams = new VariableSeq();

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

      Debug.Assert(v.TypedIdent.Type is MapType);
      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]));
      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));

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

      Procedure result = GetRaceCheckingProcedure(v.tok, LogProcedureName);

      result.InParams = inParams;

      result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

      return result;
    }

    protected Procedure MakeCheckAccessProcedureHeader(Variable v, string ReadOrWrite) {
      VariableSeq inParams = new VariableSeq();

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

      Debug.Assert(v.TypedIdent.Type is MapType);
      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]));
      Debug.Assert(!(mt.Result is MapType));

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

      string CheckProcedureName = "_CHECK_" + ReadOrWrite + "_" + v.Name;

      Procedure result = GetRaceCheckingProcedure(v.tok, CheckProcedureName);

      result.InParams = inParams;

      result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

      return result;
    }

    public void AddRaceCheckingCandidateRequires(Procedure Proc) {
      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
        AddNoReadOrWriteCandidateRequires(Proc, v);
        AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
      }

      DoHoudiniPointerAnalysis(Proc);

    }

    private void DoHoudiniPointerAnalysis(Procedure Proc) {
      HashSet<string> alreadyConsidered = new HashSet<string>();

      foreach (Variable v in Proc.InParams) {
        string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);
        if (alreadyConsidered.Contains(strippedVarName)) {
          continue;
        }
        alreadyConsidered.Add(strippedVarName);
        if (v.TypedIdent.Type is CtorType) {
          CtorType ct = v.TypedIdent.Type as CtorType;
          if (ct.Decl.Name.Equals("ptr")) {
            foreach (var arrayCollection in new ICollection<Variable>[] { 
                            verifier.KernelArrayInfo.getGlobalArrays(), verifier.KernelArrayInfo.getGroupSharedArrays(),
                            verifier.KernelArrayInfo.getPrivateArrays() }) {
              if (arrayCollection.Count == 0) {
                continue;
              }

              // This will need to be adapted to work with uniformity analysis
              foreach (string thread in new string[] { "1", "2" }) {
                Expr DisjunctionOverPointerSet = null;
                foreach (var array in arrayCollection) {
                  Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));
                  DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));
                  verifier.AddCandidateRequires(Proc,
                      Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
                          Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));
                }
                Debug.Assert(DisjunctionOverPointerSet != null);
                verifier.AddCandidateRequires(Proc,
                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
                             DisjunctionOverPointerSet));
                verifier.AddCandidateRequires(Proc,
                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
                            Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));
              }
            }
          }
        }
      }
    }

    private static IdentifierExpr MakeArrayIdExpr(Variable array) {
      return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);
    }

    private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread) {
      return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),
                                                  new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
    }

    private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread) {
      return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),
                                                  new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
    }

    public void AddRaceCheckingCandidateEnsures(Procedure Proc) {
      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
        AddNoReadOrWriteCandidateEnsures(Proc, v);
        AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
      }
    }

    private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {
      verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
    }

    private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {
      verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
    }

    private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType) {
      HashSet<Expr> result = new HashSet<Expr>();

      foreach (Cmd c in region.Cmds()) {
        if (c is CallCmd) {
          CallCmd call = c as CallCmd;

          if (call.callee == "_LOG_" + AccessType + "_" + v.Name) {
            // Ins[0] is thread 1's predicate,
            // Ins[1] is the offset to be read
            // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),
            // we are looking for the second parameter to this BV32_ADD
            Expr offset = call.Ins[1];
            if (offset is NAryExpr) {
              var nExpr = (NAryExpr)offset;
              if (nExpr.Fun.FunctionName == "BV32_ADD" &&
                  nExpr.Args[0] is NAryExpr) {
                var n0Expr = (NAryExpr)nExpr.Args[0];
                if (n0Expr.Fun.FunctionName.StartsWith("offset#"))
                  offset = nExpr.Args[1];
              }
            }
            result.Add(offset);
          }

        }

      }

      return result;
    }

    public void AddRaceCheckingDeclarations() {
      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
        AddRaceCheckingDecsAndProcsForVar(v);
      }
    }

    protected void AddLogAccessProcedure(Variable v, string Access) {
      Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

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

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

      Debug.Assert(v.TypedIdent.Type is MapType);
      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]));
      Debug.Assert(!(mt.Result is MapType));

      VariableSeq locals = new VariableSeq();
      Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
      locals.Add(TrackVariable);

      List<BigBlock> bigblocks = new List<BigBlock>();

      CmdSeq simpleCmds = new CmdSeq();

      simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));

      simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable),
          Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));
      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))));

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

      LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));
      LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));

      Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));
      LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

      LogAccessImplementation.Proc = LogAccessProcedure;

      verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
      verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
    }


    protected void AddCheckAccessProcedure(Variable v, string Access) {
      Procedure CheckAccessProcedure = MakeCheckAccessProcedureHeader(v, Access);

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

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

      Debug.Assert(v.TypedIdent.Type is MapType);
      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]));
      Debug.Assert(!(mt.Result is MapType));

      if (Access.Equals("READ")) {
        // Check read by thread 2 does not conflict with write by thread 1
        Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
        Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");
        Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
        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"),
              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
              ));
        }

        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
          WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
        }

        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);
        CheckAccessProcedure.Requires.Add(NoWriteReadRaceRequires);
      }
      else {
        Debug.Assert(Access.Equals("WRITE"));

        // Check write by thread 2 does not conflict with write by thread 1
        Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
        Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

        Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
        WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
        WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),
                                        new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
        if (!verifier.ArrayModelledAdversarially(v)) {
          WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
              ));
        }

        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
          WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
        }

        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);
        CheckAccessProcedure.Requires.Add(NoWriteWriteRaceRequires);

        // Check write by thread 2 does not conflict with read by thread 1
        Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
        Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "READ");

        Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
        ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
        ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)),
                                        new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
        if (!verifier.ArrayModelledAdversarially(v)) {
          ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),
              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
              ));
        }

        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
          ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
        }

        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);
        CheckAccessProcedure.Requires.Add(NoReadWriteRaceRequires);

      }
      verifier.Program.TopLevelDeclarations.Add(CheckAccessProcedure);
    }



    private Variable VariableForThread(int thread, Variable v) {
      return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
    }

    protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite) {
      verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);

      Debug.Assert(v.TypedIdent.Type is MapType);
      MapType mt = v.TypedIdent.Type as MapType;
      Debug.Assert(mt.Arguments.Length == 1);

      verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);

    }


    private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs) {
      List<AssignLhs> lhss = new List<AssignLhs>();
      List<Expr> rhss = new List<Expr>();
      lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));
      rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));
      return new AssignCmd(lhs.tok, lhss, rhss);
    }

    private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType) {
      Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));
      Debug.Assert(v.TypedIdent.Type is MapType);
      MapType mt = v.TypedIdent.Type as MapType;
      Debug.Assert(mt.Arguments.Length == 1);

      result = Expr.Select(result,
          new Expr[] { offsetExpr });
      Debug.Assert(!(mt.Result is MapType));
      return result;
    }

    protected void AddRequiresNoPendingAccess(Variable v) {
      IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
      IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));

      verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));
    }

    protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo) {
      Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
      ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
      ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;
      Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));
      return expr;
    }


    protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds) {
      if (preds.Count != 0) {
        Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);
        verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");
      }
    }

    private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {
      return Expr.Imp(
              new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
              offsets.Aggregate(Expr.Or));
    }

    private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread) {
      Expr expr = null;
      if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {
        expr = Expr.Imp(
                new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
                Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
      }
      return expr;
    }

    private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread) {
      Expr expr = null;
      if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {
        expr = Expr.Imp(
                new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
                Expr.Eq(
                    new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),
                    GlobalIdExpr("X", Thread)
                    )
                    );
      }
      return expr;
    }

    private Expr GlobalIdExpr(string dimension, int Thread) {
      return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
    }

    protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {
      Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
      verifier.AddCandidateInvariant(region,
          expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
    }

    private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread) {
      Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr,
          new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

      Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
          new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

      Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));

      Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);

      return Expr.Imp(
              AccessHasOccurred(v, ReadOrWrite, Thread),
              Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));
    }

    private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread) {
      return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));
    }

    private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread) {
      return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));
    }

    protected void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {
      Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
      verifier.AddCandidateInvariant(region,
          expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
    }

    private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread) {
      Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,
          GlobalIdExpr("X", Thread));

      Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
          GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

      Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));

      Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);

      Expr implication = Expr.Imp(
              AccessHasOccurred(v, ReadOrWrite, Thread),
              Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));
      return implication;
    }

    protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {
      Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
      if (expr != null) {
        verifier.AddCandidateRequires(Proc, expr);
      }
    }

    protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {
      Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
      if (expr != null) {
        verifier.AddCandidateEnsures(Proc, expr);
      }
    }



  }



  class FindReferencesToNamedVariableVisitor : StandardVisitor {
    internal bool found = false;
    private string name;

    internal FindReferencesToNamedVariableVisitor(string name) {
      this.name = name;
    }

    public override Variable VisitVariable(Variable node) {
      if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name)) {
        found = true;
      }
      return base.VisitVariable(node);
    }
  }



}