diff options
| author |  stefanheule <unknown> | 2012-09-24 15:41:29 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-24 15:41:29 +0200 |
| commit | 91a1008b115b039d9419b08ce5280f107a07a52f (patch) | |
| tree | 71e6f79e7ce95bce539f71aa321731c3b7540509 | |
| parent | a84f635713b65208e81fe8833ac13a60b0631be8 (diff) | |
| parent | 7ac8cf097184160273315971b070f20a142cdb33 (diff) | |
Merge
20 files changed, 1313 insertions, 332 deletions
diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice new file mode 100644 index 00000000..a888b647 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.chalice @@ -0,0 +1,176 @@ +class Node
+{
+ var v:int;
+ var n:Node;
+
+ predicate inv
+ { acc(v) && acc(n) && (n!=null ==> n.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>0;
+ {
+ unfolding inv in (n==null) ? 1 : 1+n.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in (i==0) ? v : n.get(i-1)
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ n:=new Node;
+ n.v:=x; n.n:=null;
+ fold n.inv;
+ }
+ else
+ {
+ call n.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ unfold p.inv;
+ n:=p.c;
+ }
+ else
+ {
+ call n.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len()-1;
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i+1] :: get(j)==old(get(j)));
+ ensures (forall j in [i+1..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold n.inv;
+ n:=n.n;
+ }
+ else
+ {
+ call n.remove(i-1);
+ }
+ fold inv;
+ }
+}
+
+class List
+{
+ var c:Node;
+
+ predicate inv { acc(c) && (c!=null ==> c.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>=0;
+ {
+ unfolding inv in (c==null) ? 0 : c.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in c.get(i)
+ }
+
+ method addFirst(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(0)==x;
+ ensures (forall i:int :: 1<=i && i<len() ==> get(i)==old(get(i-1)));
+ {
+ var p:Node;
+
+ unfold inv;
+ p:=new Node; p.v:=x; p.n:=c; c:=p;
+ fold c.inv;
+ assert c.len()==old(len())+1
+ fold inv;
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ c:=new Node;
+ c.v:=x; c.n:=null;
+ fold c.inv;
+ }
+ else
+ {
+ call c.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ unfold p.inv;
+ c:=p.c;
+ }
+ else
+ {
+ call c.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len();
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i] :: get(j)==old(get(j)));
+ ensures (forall j in [i..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold c.inv;
+ c:=c.n;
+ }
+ else
+ {
+ call c.remove(i-1);
+ }
+ fold inv;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/LinkedList-various.output.txt b/Chalice/tests/predicates/LinkedList-various.output.txt new file mode 100644 index 00000000..a8a90bb8 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.output.txt @@ -0,0 +1,4 @@ +Verification of LinkedList-various.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs index d7841f0e..8e52b9ef 100644 --- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs +++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs @@ -172,8 +172,12 @@ namespace GPUVerify {
CallCmd callCmd = c as CallCmd;
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
+ if (QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "barrier_invariant") ||
+ QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "binary_barrier_invariant")) {
+ foreach (Expr param in callCmd.Ins) {
+ ExprMayAffectControlFlow(impl, param);
+ }
+ } else if(callCmd.callee != verifier.BarrierProcedure.Name) {
Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
@@ -218,6 +222,10 @@ namespace GPUVerify var assumeCmd = c as AssumeCmd;
ExprMayAffectControlFlow(impl, assumeCmd.Expr);
}
+ else if (c is AssertCmd) {
+ var assertCmd = c as AssertCmd;
+ ExprMayAffectControlFlow(impl, assertCmd.Expr);
+ }
}
}
diff --git a/Source/GPUVerify/BarrierInvariantDescriptor.cs b/Source/GPUVerify/BarrierInvariantDescriptor.cs new file mode 100644 index 00000000..a8320b18 --- /dev/null +++ b/Source/GPUVerify/BarrierInvariantDescriptor.cs @@ -0,0 +1,37 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ abstract class BarrierInvariantDescriptor {
+
+ protected Expr Predicate;
+ protected Expr BarrierInvariant;
+ protected KernelDualiser Dualiser;
+
+ public BarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) {
+ this.Predicate = Predicate;
+ this.BarrierInvariant = BarrierInvariant;
+ this.Dualiser = Dualiser;
+ }
+
+ internal abstract AssertCmd GetAssertCmd(QKeyValue Attributes);
+
+ internal abstract List<AssumeCmd> GetInstantiationCmds();
+
+ protected Expr NonNegative(Expr e) {
+ return Dualiser.verifier.MakeBVSge(
+ e, GPUVerifier.ZeroBV());
+ }
+
+ protected Expr NotTooLarge(Expr e) {
+ return Dualiser.verifier.MakeBVSlt(e,
+ new IdentifierExpr(Token.NoToken,
+ Dualiser.verifier.GetGroupSize("X")));
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs new file mode 100644 index 00000000..df84cae8 --- /dev/null +++ b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs @@ -0,0 +1,62 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ class BinaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
+
+ private List<Tuple<Expr, Expr>> InstantiationExprPairs;
+
+ public BinaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
+ base(Predicate, BarrierInvariant, Dualiser) {
+ InstantiationExprPairs = new List<Tuple<Expr, Expr>>();
+ }
+
+ public void AddInstantiationExprPair(Expr first, Expr second) {
+ InstantiationExprPairs.Add(new Tuple<Expr, Expr>(first, second));
+ }
+
+ internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ var vd = new VariableDualiser(1, null, null);
+ return new AssertCmd(
+ Token.NoToken,
+ Expr.Imp(GPUVerifier.ThreadsInSameGroup(),
+ vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant))),
+ Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ }
+
+ internal override List<AssumeCmd> GetInstantiationCmds() {
+ var result = new List<AssumeCmd>();
+ foreach (var Instantiation in InstantiationExprPairs) {
+ foreach (var Thread in new int[] { 1, 2 }) {
+
+ var vd = new VariableDualiser(Thread, null, null);
+
+ var ThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item1);
+ var OtherThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item2);
+
+ var ti = new ThreadPairInstantiator(Dualiser.verifier, ThreadInstantiationExpr, OtherThreadInstantiationExpr, Thread);
+
+ result.Add(new AssumeCmd(
+ Token.NoToken,
+ Expr.Imp(vd.VisitExpr(Predicate),
+ Expr.Imp(
+ Expr.And(
+ Expr.And(
+ Expr.And(NonNegative(ThreadInstantiationExpr),
+ NotTooLarge(ThreadInstantiationExpr)),
+ Expr.And(NonNegative(OtherThreadInstantiationExpr),
+ NotTooLarge(OtherThreadInstantiationExpr))
+ ),
+ Expr.Neq(ThreadInstantiationExpr, OtherThreadInstantiationExpr)),
+ ti.VisitExpr(BarrierInvariant)))));
+ }
+ }
+ return result;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 868bcaa1..94c460fe 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -18,7 +18,7 @@ namespace GPUVerify public Procedure KernelProcedure; public Implementation KernelImplementation; - public Procedure BarrierProcedure; + public Procedure BarrierProcedure;
public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists(); @@ -128,6 +128,42 @@ namespace GPUVerify ResContext.AddProcedure(p); } return p; + }
+
+ private Procedure FindOrCreateBarrierInvariantProcedure() {
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant");
+ if (p == null) {
+ p = new Procedure(Token.NoToken, "barrier_invariant", new TypeVariableSeq(),
+ new VariableSeq(new Variable[] { + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__cond", + Microsoft.Boogie.Type.Bool), true) + }),
+ new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier_invariant", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ ResContext.AddProcedure(p);
+ }
+ return p;
+ }
+
+ private Procedure FindOrCreateBarrierInvariantInstantiationProcedure() {
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant_instantiation");
+ if (p == null) {
+ p = new Procedure(Token.NoToken, "barrier_invariant_instantiation", new TypeVariableSeq(),
+ new VariableSeq(new Variable[] { + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t1", + new BvType(32)), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t2", + new BvType(32)), true) + }),
+ new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier_invariant_instantiation", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ ResContext.AddProcedure(p);
+ }
+ return p;
} private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute) @@ -1376,17 +1412,21 @@ namespace GPUVerify if(KernelArrayInfo.getGroupSharedArrays().Count > 0) { - Expr IfGuard1 = Expr.And(P1, LocalFence1); - Expr IfGuard2 = Expr.And(P2, LocalFence2); - - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), - null)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), - null)); - - bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays())); + bigblocks.AddRange( + MakeResetBlocks(Expr.And(P1, LocalFence1), KernelArrayInfo.getGroupSharedArrays()));
+
+ // This could be relaxed to take into account whether the threads are in different
+ // groups, but for now we keep it relatively simple
+
+ Expr AtLeastOneEnabledWithLocalFence =
+ Expr.Or(Expr.And(P1, LocalFence1), Expr.And(P2, LocalFence2));
+
+ if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGroupSharedArrays())) {
+ bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
+ new IfCmd(Token.NoToken,
+ AtLeastOneEnabledWithLocalFence,
+ new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null));
+ } } if (KernelArrayInfo.getGlobalArrays().Count > 0) @@ -1394,14 +1434,18 @@ namespace GPUVerify Expr IfGuard1 = Expr.And(P1, GlobalFence1); Expr IfGuard2 = Expr.And(P2, GlobalFence2); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), - null)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), - null)); - - bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays())); + bigblocks.AddRange( + MakeResetBlocks(Expr.And(P1, GlobalFence1), KernelArrayInfo.getGlobalArrays()));
+
+ Expr ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence =
+ Expr.And(Expr.And(GPUVerifier.ThreadsInSameGroup(), Expr.And(P1, P2)), Expr.Or(GlobalFence1, GlobalFence2));
+
+ if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGlobalArrays())) {
+ bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
+ new IfCmd(Token.NoToken,
+ ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence,
+ new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null));
+ } } StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok); @@ -1432,16 +1476,16 @@ namespace GPUVerify new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1)); } - private List<BigBlock> MakeResetBlocks(int Thread, ICollection<Variable> variables) + private List<BigBlock> MakeResetBlocks(Expr ResetCondition, ICollection<Variable> variables) { Debug.Assert(variables.Count > 0); - List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>(); + List<BigBlock> result = new List<BigBlock>(); foreach (Variable v in variables) { - ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread)); + result.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, ResetCondition)); } - Debug.Assert(ResetAndHavocBlocks.Count > 0); - return ResetAndHavocBlocks; + Debug.Assert(result.Count > 0); + return result; } private List<BigBlock> MakeHavocBlocks(ICollection<Variable> variables) { @@ -1451,8 +1495,19 @@ namespace GPUVerify if (!ArrayModelledAdversarially(v)) { result.Add(HavocSharedArray(v)); } - } + }
+ Debug.Assert(result.Count > 0); return result; + }
+
+ private bool SomeArrayModelledNonAdversarially(ICollection<Variable> variables) {
+ Debug.Assert(variables.Count > 0);
+ foreach (Variable v in variables) {
+ if (!ArrayModelledAdversarially(v)) {
+ return true;
+ }
+ }
+ return false;
} public static bool HasZDimension(Variable v) @@ -1709,7 +1764,13 @@ namespace GPUVerify if (c is CallCmd) { - CallCmd call = c as CallCmd; + CallCmd call = c as CallCmd;
+
+ if (QKeyValue.FindBoolAttribute(call.Proc.Attributes, "barrier_invariant") ||
+ QKeyValue.FindBoolAttribute(call.Proc.Attributes, "binary_barrier_invariant")) {
+ // Do not pull non-local accesses out of barrier invariants
+ continue;
+ } List<Expr> newIns = new List<Expr>(); @@ -1765,7 +1826,8 @@ namespace GPUVerify } else if (c is AssertCmd) { - result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr, impl))); + // Do not pull non-local accesses out of assert commands
+ continue; } else if (c is AssumeCmd) { @@ -1846,8 +1908,10 @@ namespace GPUVerify List<Declaration> NewTopLevelDeclarations = new List<Declaration>(); - foreach (Declaration d in Program.TopLevelDeclarations) - { + for(int i = 0; i < Program.TopLevelDeclarations.Count; i++) + {
+ Declaration d = Program.TopLevelDeclarations[i]; + if (d is Procedure) { @@ -1982,7 +2046,7 @@ namespace GPUVerify private int Check() { - BarrierProcedure = FindOrCreateBarrierProcedure(); + BarrierProcedure = FindOrCreateBarrierProcedure();
KernelProcedure = CheckExactlyOneKernelProcedure(); if (ErrorCount > 0) @@ -2039,8 +2103,9 @@ namespace GPUVerify { return D as Implementation; } - } - Debug.Assert(false); + }
+ Error(Token.NoToken, "No implementation found for procedure \"" + procedureName + "\"");
+ Environment.Exit(1); return null; } @@ -2207,6 +2272,10 @@ namespace GPUVerify return (expr.Decl is Constant) || (expr.Decl is Formal && ((Formal)expr.Decl).InComing); } + + internal static Expr GroupSharedIndexingExpr(int Thread) {
+ return Thread == 1 ? Expr.True : ThreadsInSameGroup();
+ }
} diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index e7122edf..2bcc5b15 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -1,178 +1,181 @@ -<?xml version="1.0" encoding="utf-8"?> -<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> - <PropertyGroup> - <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> - <Platform Condition=" '$(Platform)' == '' ">x86</Platform> - <ProductVersion>8.0.30703</ProductVersion> - <SchemaVersion>2.0</SchemaVersion> - <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid> - <OutputType>Exe</OutputType> - <AppDesignerFolder>Properties</AppDesignerFolder> - <RootNamespace>GPUVerify</RootNamespace> - <AssemblyName>GPUVerifyVCGen</AssemblyName> - <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> - <TargetFrameworkProfile>Client</TargetFrameworkProfile> - <FileAlignment>512</FileAlignment> - <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' "> - <PlatformTarget>x86</PlatformTarget> - <DebugSymbols>true</DebugSymbols> - <DebugType>full</DebugType> - <Optimize>false</Optimize> - <OutputPath>bin\Debug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking> - <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> - <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> - <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> - <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> - <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> - <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations> - <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations> - <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations> - <CodeContractsEnumObligations>False</CodeContractsEnumObligations> - <CodeContractsPointerObligations>False</CodeContractsPointerObligations> - <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> - <CodeContractsRunInBackground>True</CodeContractsRunInBackground> - <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies> - <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> - <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> - <CodeContractsCustomRewriterAssembly /> - <CodeContractsCustomRewriterClass /> - <CodeContractsLibPaths /> - <CodeContractsExtraRewriteOptions /> - <CodeContractsExtraAnalysisOptions /> - <CodeContractsBaseLineFile /> - <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults> - <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> - <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly> - <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> - <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' "> - <PlatformTarget>x86</PlatformTarget> - <DebugType>pdbonly</DebugType> - <Optimize>true</Optimize> - <OutputPath>bin\Release\</OutputPath> - <DefineConstants>TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - </PropertyGroup> - <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'"> - <DebugSymbols>true</DebugSymbols> - <OutputPath>bin\Debug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <DebugType>full</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> - <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> - <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> - <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules> - <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules> - </PropertyGroup> - <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'"> - <OutputPath>bin\Release\</OutputPath> - <DefineConstants>TRACE</DefineConstants> - <Optimize>true</Optimize> - <DebugType>pdbonly</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> - <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> - </PropertyGroup> - <ItemGroup> - <Reference Include="System" /> - <Reference Include="System.Core" /> - <Reference Include="System.Windows.Forms" /> - <Reference Include="System.Xml.Linq" /> - <Reference Include="System.Data.DataSetExtensions" /> - <Reference Include="Microsoft.CSharp" /> - <Reference Include="System.Data" /> - <Reference Include="System.Xml" /> - </ItemGroup> - <ItemGroup> - <Compile Include="AccessCollector.cs" /> - <Compile Include="AccessRecord.cs" /> - <Compile Include="AdversarialAbstraction.cs" /> - <Compile Include="ArrayControlFlowAnalyser.cs" /> - <Compile Include="AsymmetricExpressionFinder.cs" /> - <Compile Include="StrideConstraint.cs" /> - <Compile Include="ReducedStrengthAnalysis.cs" /> - <Compile Include="UnstructuredRegion.cs" /> - <Compile Include="IRegion.cs" /> - <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" /> - <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" /> - <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" /> - <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" /> - <Compile Include="KernelDualiser.cs" /> - <Compile Include="LiveVariableAnalyser.cs" /> - <Compile Include="LoopInvariantGenerator.cs" /> - <Compile Include="MayBePowerOfTwoAnalyser.cs" /> - <Compile Include="StructuredProgramVisitor.cs" /> - <Compile Include="EnabledToPredicateVisitor.cs" /> - <Compile Include="CommandLineOptions.cs" /> - <Compile Include="GPUVerifier.cs" /> - <Compile Include="IKernelArrayInfo.cs" /> - <Compile Include="IRaceInstrumenter.cs" /> - <Compile Include="Main.cs" /> - <Compile Include="NonLocalAccessCollector.cs" /> - <Compile Include="NonLocalAccessExtractor.cs" /> - <Compile Include="KernelArrayInfoLists.cs" /> - <Compile Include="NullRaceInstrumenter.cs" /> - <Compile Include="Predicator.cs" /> - <Compile Include="Properties\AssemblyInfo.cs" /> - <Compile Include="RaceInstrumenter.cs" /> - <Compile Include="ReadCollector.cs" /> - <Compile Include="VariableDualiser.cs" /> - <Compile Include="VariablesOccurringInExpressionVisitor.cs" /> - <Compile Include="VariableDefinitionAnalysis.cs" /> - <Compile Include="StructuredRegion.cs" /> - <Compile Include="WriteCollector.cs" /> - </ItemGroup> - <ItemGroup> - <ProjectReference Include="..\AIFramework\AIFramework.csproj"> - <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="..\Core\Core.csproj"> - <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> - <Name>Core</Name> - </ProjectReference> - <ProjectReference Include="..\Graph\Graph.csproj"> - <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project> - <Name>Graph</Name> - </ProjectReference> - <ProjectReference Include="..\ParserHelper\ParserHelper.csproj"> - <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project> - <Name>ParserHelper</Name> - </ProjectReference> - <ProjectReference Include="..\VCGeneration\VCGeneration.csproj"> - <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project> - <Name>VCGeneration</Name> - </ProjectReference> - </ItemGroup> - <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" /> +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>GPUVerify</RootNamespace>
+ <AssemblyName>GPUVerifyVCGen</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'">
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Windows.Forms" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="AccessCollector.cs" />
+ <Compile Include="AccessRecord.cs" />
+ <Compile Include="AdversarialAbstraction.cs" />
+ <Compile Include="ArrayControlFlowAnalyser.cs" />
+ <Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="BarrierInvariantDescriptor.cs" />
+ <Compile Include="BinaryBarrierInvariantDescriptor.cs" />
+ <Compile Include="StrideConstraint.cs" />
+ <Compile Include="ReducedStrengthAnalysis.cs" />
+ <Compile Include="UnaryBarrierInvariantDescriptor.cs" />
+ <Compile Include="UnstructuredRegion.cs" />
+ <Compile Include="IRegion.cs" />
+ <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
+ <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
+ <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
+ <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
+ <Compile Include="KernelDualiser.cs" />
+ <Compile Include="LiveVariableAnalyser.cs" />
+ <Compile Include="LoopInvariantGenerator.cs" />
+ <Compile Include="MayBePowerOfTwoAnalyser.cs" />
+ <Compile Include="StructuredProgramVisitor.cs" />
+ <Compile Include="EnabledToPredicateVisitor.cs" />
+ <Compile Include="CommandLineOptions.cs" />
+ <Compile Include="GPUVerifier.cs" />
+ <Compile Include="IKernelArrayInfo.cs" />
+ <Compile Include="IRaceInstrumenter.cs" />
+ <Compile Include="Main.cs" />
+ <Compile Include="NonLocalAccessCollector.cs" />
+ <Compile Include="NonLocalAccessExtractor.cs" />
+ <Compile Include="KernelArrayInfoLists.cs" />
+ <Compile Include="NullRaceInstrumenter.cs" />
+ <Compile Include="Predicator.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="RaceInstrumenter.cs" />
+ <Compile Include="ReadCollector.cs" />
+ <Compile Include="VariableDualiser.cs" />
+ <Compile Include="VariablesOccurringInExpressionVisitor.cs" />
+ <Compile Include="VariableDefinitionAnalysis.cs" />
+ <Compile Include="StructuredRegion.cs" />
+ <Compile Include="WriteCollector.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\AIFramework\AIFramework.csproj">
+ <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="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it. Other similar extension points exist, see Microsoft.Common.targets. <Target Name="BeforeBuild"> </Target> <Target Name="AfterBuild"> </Target> - --> + -->
</Project>
\ No newline at end of file diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs index c85989c9..7f14fcd0 100644 --- a/Source/GPUVerify/IRaceInstrumenter.cs +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -15,7 +15,7 @@ namespace GPUVerify void AddRaceCheckingDeclarations(); - BigBlock MakeResetReadWriteSetStatements(Variable v, int thread); + BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition); void AddRaceCheckingCandidateRequires(Procedure Proc); diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 201018bb..526e39a0 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -9,10 +9,13 @@ using Microsoft.Basetypes; namespace GPUVerify {
class KernelDualiser {
- private GPUVerifier verifier;
+ internal GPUVerifier verifier;
+
+ private List<BarrierInvariantDescriptor> BarrierInvariantDescriptors;
public KernelDualiser(GPUVerifier verifier) {
this.verifier = verifier;
+ BarrierInvariantDescriptors = new List<BarrierInvariantDescriptor>();
}
private string procName = null;
@@ -74,7 +77,7 @@ namespace GPUVerify { return result;
}
- private QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {
+ internal QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {
if (attributes == null) {
return null;
}
@@ -100,6 +103,41 @@ namespace GPUVerify { if (c is CallCmd) {
CallCmd Call = c as CallCmd;
+ if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier_invariant")) {
+ // There should be a predicate, an invariant expression, and at least one instantiation
+ Debug.Assert(Call.Ins.Count >= 3);
+ var BIDescriptor = new UnaryBarrierInvariantDescriptor(Call.Ins[0], + Expr.Neq(Call.Ins[1], + new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ for (var i = 2; i < Call.Ins.Count; i++) {
+ BIDescriptor.AddInstantiationExpr(Call.Ins[i]);
+ }
+ BarrierInvariantDescriptors.Add(BIDescriptor);
+ return;
+ }
+
+ if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "binary_barrier_invariant")) {
+ // There should be a predicate, an invariant expression, and at least one pair of
+ // instantiation expressions
+ Debug.Assert(Call.Ins.Count >= 4);
+ var BIDescriptor = new BinaryBarrierInvariantDescriptor(Call.Ins[0],
+ Expr.Neq(Call.Ins[1],
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ for (var i = 2; i < Call.Ins.Count; i += 2) {
+ BIDescriptor.AddInstantiationExprPair(Call.Ins[i], Call.Ins[i + 1]);
+ }
+ BarrierInvariantDescriptors.Add(BIDescriptor);
+ return;
+ }
+
+
+ if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {
+ // Assert barrier invariants
+ foreach (var BIDescriptor in BarrierInvariantDescriptors) {
+ cs.Add(BIDescriptor.GetAssertCmd(Call.Attributes));
+ }
+ }
+
List<Expr> uniformNewIns = new List<Expr>();
List<Expr> nonUniformNewIns = new List<Expr>();
for (int i = 0; i < Call.Ins.Count; i++) {
@@ -148,6 +186,16 @@ namespace GPUVerify { NewCallCmd.Attributes = Call.Attributes;
cs.Add(NewCallCmd);
+
+ if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {
+ foreach (var BIDescriptor in BarrierInvariantDescriptors) {
+ foreach (var Instantiation in BIDescriptor.GetInstantiationCmds()) {
+ cs.Add(Instantiation);
+ }
+ }
+ BarrierInvariantDescriptors.Clear();
+ }
+
}
else if (c is AssignCmd) {
AssignCmd assign = c as AssignCmd;
@@ -370,4 +418,111 @@ namespace GPUVerify { }
+ class ThreadInstantiator : Duplicator {
+
+ private GPUVerifier verifier;
+ private Expr InstantiationExpr;
+ private int Thread;
+
+ internal ThreadInstantiator(GPUVerifier verifier, Expr InstantiationExpr, int Thread) {
+ this.verifier = verifier;
+ this.InstantiationExpr = InstantiationExpr;
+ this.Thread = Thread;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ Debug.Assert(!(node.Decl is Formal));
+
+ if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {
+ Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));
+ return InstantiationExpr.Clone() as Expr;
+ }
+
+ Debug.Assert(node.Decl is Constant ||
+ verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||
+ verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));
+
+ return base.VisitIdentifierExpr(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is MapSelect) {
+ Debug.Assert((node.Fun as MapSelect).Arity == 1);
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ var v = (node.Args[0] as IdentifierExpr).Decl;
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+
+ }
+
+
+
+ class ThreadPairInstantiator : Duplicator {
+
+ private GPUVerifier verifier;
+ private Tuple<Expr, Expr> InstantiationExprs;
+ private int Thread;
+
+ internal ThreadPairInstantiator(GPUVerifier verifier, Expr InstantiationExpr1, Expr InstantiationExpr2, int Thread) {
+ this.verifier = verifier;
+ this.InstantiationExprs = new Tuple<Expr, Expr>(InstantiationExpr1, InstantiationExpr2);
+ this.Thread = Thread;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+ Debug.Assert(!(node.Decl is Formal));
+
+ if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {
+ Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));
+ return InstantiationExprs.Item1.Clone() as Expr;
+ }
+
+ Debug.Assert(node.Decl is Constant ||
+ verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||
+ verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));
+
+ return base.VisitIdentifierExpr(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ if (node.Fun is MapSelect) {
+ Debug.Assert((node.Fun as MapSelect).Arity == 1);
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ var v = (node.Args[0] as IdentifierExpr).Decl;
+
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));
+ }
+ }
+
+ if (node.Fun is FunctionCall) {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ // Alternate instantiation order for "other thread" functions.
+ // Note that we do not alternatve the "Thread" field, as we are not switching the
+ // thread for which instantiation is being performed
+ if (VariableDualiser.otherFunctionNames.Contains(call.Func.Name)) {
+ return new ThreadPairInstantiator(verifier, InstantiationExprs.Item2, InstantiationExprs.Item1, Thread)
+ .VisitExpr(node.Args[0]);
+ }
+
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+
+ }
+
+
+
}
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs index 6a934899..d1361ff4 100644 --- a/Source/GPUVerify/NonLocalAccessCollector.cs +++ b/Source/GPUVerify/NonLocalAccessCollector.cs @@ -70,7 +70,6 @@ namespace GPUVerify return collector.Accesses.Count > 0;
}
-
public override Expr VisitNAryExpr(NAryExpr node)
{
if (IsNonLocalAccess(node, NonLocalState))
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs index fae08aa3..6452331f 100644 --- a/Source/GPUVerify/NullRaceInstrumenter.cs +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -24,7 +24,7 @@ namespace GPUVerify } - public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) + public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) { return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null); } diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index c73b9b13..71214cb3 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -473,16 +473,17 @@ namespace GPUVerify { } - public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) { + public BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) { 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")))); + Expr ResetReadAssumeGuard = Expr.Imp(ResetCondition, + Expr.Not(new IdentifierExpr(Token.NoToken, + new VariableDualiser(1, null, null).VisitVariable( + GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))))); + Expr ResetWriteAssumeGuard = Expr.Imp(ResetCondition, + 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(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard); diff --git a/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs new file mode 100644 index 00000000..ef87750e --- /dev/null +++ b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs @@ -0,0 +1,49 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ class UnaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
+ private List<Expr> InstantiationExprs;
+
+ public UnaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
+ base(Predicate, BarrierInvariant, Dualiser) {
+ InstantiationExprs = new List<Expr>();
+ }
+
+ public void AddInstantiationExpr(Expr InstantiationExpr) {
+ InstantiationExprs.Add(InstantiationExpr);
+ }
+
+ internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ var vd = new VariableDualiser(1, null, null);
+ return new AssertCmd(
+ Token.NoToken,
+ vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant)),
+ Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ }
+
+ internal override List<AssumeCmd> GetInstantiationCmds() {
+ var result = new List<AssumeCmd>();
+ foreach (var Instantiation in InstantiationExprs) {
+ foreach (var Thread in new int[] { 1, 2 }) {
+ var vd = new VariableDualiser(Thread, null, null);
+ var ThreadInstantiationExpr = vd.VisitExpr(Instantiation);
+ var ti = new ThreadInstantiator(Dualiser.verifier, ThreadInstantiationExpr, Thread);
+
+ result.Add(new AssumeCmd(
+ Token.NoToken,
+ Expr.Imp(vd.VisitExpr(Predicate),
+ Expr.Imp(Expr.And(
+ NonNegative(ThreadInstantiationExpr),
+ NotTooLarge(ThreadInstantiationExpr)),
+ ti.VisitExpr(BarrierInvariant)))));
+ }
+ }
+ return result;
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs index ce5f78ee..d0b04598 100644 --- a/Source/GPUVerify/VariableDualiser.cs +++ b/Source/GPUVerify/VariableDualiser.cs @@ -10,7 +10,7 @@ namespace GPUVerify {
class VariableDualiser : Duplicator
{
- static HashSet<string> otherFunctionNames =
+ static internal HashSet<string> otherFunctionNames =
new HashSet<string>(new string[] { "__other_bool", "__other_bv32", "__other_arrayId" });
private int id;
@@ -91,15 +91,16 @@ namespace GPUVerify if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
- new ExprSeq(new Expr[] { node.Args[0], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));
+ new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(id) })),
+ VisitExpr(node.Args[1]) }));
}
}
- // Avoid dualisation of certain special builtin functions that are cross-thread
if (node.Fun is FunctionCall)
{
FunctionCall call = node.Fun as FunctionCall;
+ // Alternate dualisation for "other thread" functions
if (otherFunctionNames.Contains(call.Func.Name))
{
Debug.Assert(id == 1 || id == 2);
@@ -119,16 +120,13 @@ namespace GPUVerify var v = node.DeepAssignedVariable;
if(QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,
- new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
+ new List<Expr>(new Expr[] { GPUVerifier.GroupSharedIndexingExpr(id) })),
+ node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
}
return base.VisitMapAssignLhs(node);
}
- private Expr GroupSharedIndexingExpr() {
- return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();
- }
-
}
}
diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs index 25549f71..e1da06fb 100644 --- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs +++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs @@ -25,7 +25,7 @@ namespace Microsoft.Boogie using VC;
using AI = Microsoft.AbstractInterpretationFramework;
using BoogiePL = Microsoft.Boogie;
-
+
/*
The following assemblies are referenced because they are needed at runtime, not at compile time:
BaseTypes
@@ -636,30 +636,211 @@ namespace Microsoft.Boogie {
penulFunc = lastFunc;
lastFunc = f;
+ currIncarnationNo = System.Convert.ToInt32(tokens[1]);
}
}
}
return (penulFunc == null) ? lastFunc : penulFunc;
}
- static QKeyValue ExtractAsertSourceLocFromTrace(BlockSeq s)
+ static void PrintDetailedTrace(CallCounterexample err, int colOneLength, int colTwoLength, int colThreeLength, int failElemOffset, int elemWidth, string threadOneFailAccess, string threadTwoFailAccess)
{
- foreach (Block b in s)
+ Model model = err.Model;
+ BlockSeq trace = err.Trace;
+
+ int failCallLineNo = QKeyValue.FindIntAttribute(err.FailingCall.Attributes, "line", -1);
+ int failCallColNo = QKeyValue.FindIntAttribute(err.FailingCall.Attributes, "col", -1);
+ int failReqLineNo = QKeyValue.FindIntAttribute(err.FailingRequires.Attributes, "line", -1);
+ int failReqColNo = QKeyValue.FindIntAttribute(err.FailingRequires.Attributes, "col", -1);
+
+ int lineno = -1;
+ int colno = -1;
+
+ bool checkCallExpected = false;
+ bool colTwoFail = false;
+ bool colThreeFail = false;
+
+ string colOne = null;
+ string colTwo = null;
+ string colThree = null;
+
+ foreach (Block b in trace)
{
- foreach (Cmd c in b.Cmds)
+ if (Regex.IsMatch(b.ToString(), @"inline[$]_LOG_(READ|WRITE)_[$]+\w+[$][0-9]+[$]_LOG_(READ|WRITE)"))
{
- if (c is AssertCmd)
+ int elemOffset = -1;
+ string arrName;
+
+ foreach (Cmd c in b.Cmds)
{
- if (QKeyValue.FindBoolAttribute(((AssertCmd)c).Attributes, "sourceloc"))
+ string access = (Regex.IsMatch(c.ToString(), @"inline[$]_LOG_READ")) ? "READ" : "WRITE";
+
+ if (Regex.IsMatch(c.ToString(), "assume _" + access + "_OFFSET"))
{
- return ((AssertCmd)c).Attributes;
+ elemOffset = ExtractOffsetFromExpr(model, (((c as PredicateCmd).Expr as NAryExpr).Args[1] as NAryExpr).Args[1]);
+ }
+ else if (Regex.IsMatch(c.ToString(), "assume _" + access + "_SOURCE"))
+ {
+ arrName = ExtractArrName(c.ToString());
+ string enParamName = ExtractEnabledArg((c as AssumeCmd).Expr).Name;
+
+ Model.Func enFunc = model.TryGetFunc(enParamName);
+ Debug.Assert(enFunc != null, "PrintDetailedTrace(): could not get enParamName from model: " + enParamName);
+ Debug.Assert(enFunc.AppCount == 1, "PrintDetailedTrace(): enabled parameter function has more that one application.");
+ bool enabled = (enFunc.Apps.ElementAt(0).Result as Model.Boolean).Value;
+ int sourceLocLineNo = (ExtractSourceLineArg((c as AssumeCmd).Expr).Val as BvConst).Value.ToIntSafe;
+
+ string sourceLocLine = FetchCodeLine(GetSourceLocFileName(), sourceLocLineNo + 1);
+
+ string[] slocTokens = Regex.Split(sourceLocLine, "#");
+ lineno = System.Convert.ToInt32(slocTokens[0]);
+ colno = System.Convert.ToInt32(slocTokens[1]);
+ string fname = slocTokens[2];
+
+ colOne = fname + ":" + lineno + ":" + colno + ":";
+ colTwo = enabled ? " " + access.ToLower() + "s ((char*)" + arrName + ")" + "[" + ((elemOffset == -1) ? "?" : "" + CalculateByteOffset(elemOffset, elemWidth)) + "]" : "";
+ colTwoFail = elemOffset == failElemOffset && lineno == failReqLineNo && colno == failReqColNo && access == threadOneFailAccess;
+ }
+ }
+ }
+ else if (Regex.IsMatch(b.ToString(), @"inline[$]_LOG_(READ|WRITE)_[$]+\w+[$][0-9]+[$]Return"))
+ {
+ // Assuming that a LOG call will always be immediately followed by a CHECK call.
+ checkCallExpected = true;
+ continue;
+ }
+ else if (checkCallExpected)
+ {
+ foreach (Cmd c in b.Cmds)
+ {
+ if (Regex.IsMatch(c.ToString(), @"assert[\s]+[!]\(\w+[$][0-9]+(@[0-9]+|[\s]+)[\s]*&&[\s]+_(WRITE|READ)_HAS_OCCURRED"))
+ {
+ string access = Regex.IsMatch((c as AssertRequiresCmd).Call.callee, "_CHECK_READ_") ? "READ" : "WRITE";
+
+ string[] tokens = Regex.Split(c.ToString(), "&&");
+ string arrName = ExtractArrName(tokens[1]);
+ string enParamName = ExtractEnabledParameterName((c as AssertRequiresCmd).Expr);
+
+ Model.Func enFunc = model.TryGetFunc(enParamName);
+ Debug.Assert(enFunc != null, "PrintDetailedTrace(): could not get enParamName from model: " + enParamName);
+ Debug.Assert(enFunc.AppCount == 1, "PrintDetailedTrace(): enabled parameter function has more that one application.");
+ bool enabled = (enFunc.Apps.ElementAt(0).Result as Model.Boolean).Value;
+
+ Expr offsetArg = ExtractOffsetArg((c as AssertRequiresCmd).Expr, "_" + (c.ToString().Contains("WRITE") ? "WRITE" : "READ") + "_OFFSET_");
+
+
+
+ int elemOffset = ExtractOffsetFromExpr(model, offsetArg);
+ colThree = enabled ? " " + access.ToLower() + "s ((char*)" + arrName + ")" + "[" + ((elemOffset == -1) ? "?" : "" + CalculateByteOffset(elemOffset, elemWidth)) + "]" : "";
+ colThreeFail = elemOffset == failElemOffset && lineno == failCallLineNo && colno == failCallColNo && access == threadTwoFailAccess;
+
+ checkCallExpected = false;
+ PrintDetailedTraceLine(colOne, colTwo, colThree, colOneLength, colTwoLength, colThreeLength, colTwoFail, colThreeFail);
+ break;
}
}
}
}
- return null;
}
+ private static LiteralExpr ExtractSourceLineArg(Expr e)
+ {
+ var visitor = new GetThenOfIfThenElseVisitor();
+ visitor.VisitExpr(e);
+ return visitor.getResult();
+ }
+
+ private static Expr ExtractOffsetArg(Expr e, string pattern)
+ {
+ var visitor = new GetRHSOfEqualityVisitor(pattern);
+ visitor.VisitExpr(e);
+ return visitor.getResult();
+ }
+
+ private static IdentifierExpr ExtractEnabledArg(Expr e)
+ {
+ var visitor = new GetIfOfIfThenElseVisitor();
+ visitor.VisitExpr(e);
+ return visitor.getResult();
+ }
+
+ private static string ExtractEnabledParameterName(Expr e)
+ {
+ if (e is IdentifierExpr)
+ {
+ return ((IdentifierExpr)e).Name;
+ }
+ else
+ {
+ Debug.Assert(e is NAryExpr);
+ return ExtractEnabledParameterName(((NAryExpr)e).Args[0]);
+ }
+ }
+
+ private static int ExtractOffsetFromExpr(Model model, Expr offsetArg)
+ {
+ if (offsetArg is LiteralExpr)
+ {
+ return ((offsetArg as LiteralExpr).Val as BvConst).Value.ToIntSafe;
+ }
+ else if (offsetArg is IdentifierExpr)
+ {
+ string offsetname = (offsetArg as IdentifierExpr).Name;
+ Model.Func fo = model.TryGetFunc(offsetname);
+ Debug.Assert(fo != null, "ExtractOffsetFromExpr(): could not get value for the following from model: " + offsetname);
+ Debug.Assert(fo.AppCount == 1, "ExtractOffsetFromExpr(): the following function has more than one application: " + offsetname);
+ return (fo.Apps.ElementAt(0).Result as Model.BitVector).AsInt();
+
+ }
+ else
+ {
+ return -1;
+ }
+ }
+
+ private static void PrintDetailedTraceLine(string colOne, string colTwo, string colThree, int colOneLength, int colTwoLength, int colThreeLength, bool colTwoError, bool colThreeError)
+ {
+ Contract.Requires(colOneLength >= colOne.Length && colTwoLength >= colTwo.Length && colThreeLength >= colThree.Length);
+ Console.Write("{0}|", colOne + Chars(colOneLength - colOne.Length, ' '));
+
+ ConsoleColor col = Console.ForegroundColor;
+ if (colTwoError)
+ {
+ Console.ForegroundColor = ConsoleColor.Red;
+ }
+ Console.Write("{0}", colTwo + Chars(colTwoLength - colTwo.Length, ' '));
+ Console.ForegroundColor = col;
+ Console.Write('|');
+
+ if (colThreeError)
+ {
+ Console.ForegroundColor = ConsoleColor.Red;
+ }
+ Console.WriteLine("{0}", colThree + Chars(colThreeLength - colThree.Length, ' '));
+ Console.ForegroundColor = col;
+
+ }
+
+ private static string GetSourceLocFileName()
+ {
+ return GetFilenamePathPrefix() + GetFileName() + ".loc";
+ }
+
+ private static string GetFileName()
+ {
+ return Path.GetFileNameWithoutExtension(CommandLineOptions.Clo.Files[0]);
+ }
+
+ private static string GetFilenamePathPrefix()
+ {
+ string directoryName = Path.GetDirectoryName(CommandLineOptions.Clo.Files[0]);
+ return ((!String.IsNullOrEmpty(directoryName) && directoryName != ".") ? (directoryName + Path.DirectorySeparatorChar) : "");
+ }
+
+ private static string GetCorrespondingThreadTwoName(string threadOneName)
+ {
+ return threadOneName.Replace("$1", "$2");
+ }
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);
@@ -672,10 +853,6 @@ namespace Microsoft.Boogie static QKeyValue GetSourceLocInfo(Counterexample error, string AccessType) {
string sourceVarName = null;
int sourceLocLineNo = -1;
- string directoryName = Path.GetDirectoryName(CommandLineOptions.Clo.Files[0]);
- string sourceLocFileName = ((!String.IsNullOrEmpty(directoryName) && directoryName != ".") ? (directoryName + Path.DirectorySeparatorChar) : "") + Path.GetFileNameWithoutExtension(CommandLineOptions.Clo.Files[0]) + ".loc";
-
- TextReader tr = new StreamReader(sourceLocFileName);
foreach (Block b in error.Trace)
{
@@ -699,7 +876,7 @@ namespace Microsoft.Boogie if (sourceLocLineNo > 0)
{
// TODO: Make lines in .loc file be indexed from 1 for consistency.
- string fileLine = FetchCodeLine(sourceLocFileName, sourceLocLineNo + 1);
+ string fileLine = FetchCodeLine(GetSourceLocFileName(), sourceLocLineNo + 1);
if (fileLine != null)
{
string[] slocTokens = Regex.Split(fileLine, "#");
@@ -715,7 +892,6 @@ namespace Microsoft.Boogie Console.WriteLine("sourceLocLineNo is {0}. No sourceloc at that location.\n", sourceLocLineNo);
return null;
}
- tr.Close();
return null;
}
@@ -847,71 +1023,95 @@ namespace Microsoft.Boogie CallCounterexample err = (CallCounterexample)error;
if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "barrier_divergence"))
{
- ReportBarrierDivergence(err.FailingCall, true);
+ ReportBarrierDivergence(err.FailingCall);
}
else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "race"))
{
- int byteOffset = -1, elemWidth = -1, elemOffset = -1;
- int lidx1 = -1, lidy1 = -1, lidz1 = -1, lidx2 = -1, lidy2 = -1, lidz2 = -1;
- int gidx1 = -1, gidy1 = -1, gidz1 = -1, gidx2 = -1, gidy2 = -1, gidz2 = -1;
+ int byteOffset = -1, elemOffset = -1, elemWidth = -1;
string thread1 = null, thread2 = null, group1 = null, group2 = null, arrName = null;
+ //TODO: make this a command line argument.
+ bool detailedTrace = false;
+ string threadOneFailAccess = null, threadTwoFailAccess = null;
Variable offsetVar = ExtractOffsetVar(err.FailingRequires.Condition as NAryExpr);
+ /* Right now the offset incarnation that is extracted is the penultimate one if
+ * there is more than one incarnation, or the last one if there is only one incarnation.
+ * TODO: In future, we should know the exact incarnation to extract. This information is
+ * available when the CallCounterexample is created in VC.cs AssertCmdToCounterexample() (line 2405)
+ * The condition of the AssertRequiresCmd contains the incarnation information, so this should be passed
+ * on to the Requires of the created CallCounterexample. This can either be done by replacing the condition
+ * of the Requires with the condition from AssertRequiresCmd (containing incarnation information) or creating
+ * a separate field in the Requires to store this original condition.
+ */
Model.Func offsetFunc = ExtractIncarnationFromModel(error.Model, offsetVar.Name);
Debug.Assert(offsetFunc != null, "ProcessOutcome(): Could not extract incarnation.");
- GetInfoFromVarAndFunc(offsetVar.Attributes, offsetFunc, out byteOffset, out elemWidth, out elemOffset, out arrName);
+ GetInfoFromVarAndFunc(offsetVar.Attributes, offsetFunc, out byteOffset, out elemOffset, out elemWidth, out arrName);
Debug.Assert(error.Model != null, "ProcessOutcome(): null model");
- GetIdsFromModel(error.Model, out lidx1, out lidy1, out lidz1, out lidx2, out lidy2, out lidz2,
- out gidx1, out gidy1, out gidz1, out gidx2, out gidy2, out gidz2);
-
- thread1 = "(" + lidx1 + ", " + lidy1 + ", " + lidz1 + ")";
- thread2 = "(" + lidx2 + ", " + lidy2 + ", " + lidz2 + ")";
+ GetThreadsAndGroupsFromModel(err.Model, out thread1, out thread2, out group1, out group2, true);
- group1 = "(" + gidx1 + ", " + gidy1 + ", " + gidz1 + ")";
- group2 = "(" + gidx2 + ", " + gidy2 + ", " + gidz2 + ")";
-
if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_read"))
{
err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, elemOffset, RaceType.WR, true);
+ threadOneFailAccess = "WRITE";
+ threadTwoFailAccess = "READ";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WR);
}
else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "read_write"))
{
err.FailingRequires.Attributes = GetSourceLocInfo(error, "READ");
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, elemOffset, RaceType.RW, true);
+ threadOneFailAccess = "READ";
+ threadTwoFailAccess = "WRITE";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.RW);
}
else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "write_write"))
{
err.FailingRequires.Attributes = GetSourceLocInfo(error, "WRITE");
- ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, elemOffset, RaceType.WW, true);
+ threadOneFailAccess = "WRITE";
+ threadTwoFailAccess = "WRITE";
+ ReportRace(err.FailingCall, err.FailingRequires, thread1, thread2, group1, group2, arrName, byteOffset, RaceType.WW);
+ }
+
+ if (detailedTrace)
+ {
+ string fname = QKeyValue.FindStringAttribute(err.FailingCall.Attributes, "fname");
+ Debug.Assert(!String.IsNullOrEmpty(fname));
+ int colOneSize = fname.Length + 11;
+ string colTwoHeader = " T " + GetThreadOne(error.Model, false) + " G " + GetGroupOne(error.Model, false) + " ";
+ string colThreeHeader = " T " + GetThreadTwo(error.Model, false) + " G " + GetGroupTwo(error.Model, false) + " ";
+
+ int colTwoSize = colTwoHeader.Length + 2;
+ int colThreeSize = colTwoHeader.Length + 2;
+
+ PrintDetailedTraceHeader(colTwoHeader, colThreeHeader, colOneSize, colTwoSize, colThreeSize);
+ PrintDetailedTrace(err, colOneSize, colTwoSize, colThreeSize, elemOffset, elemWidth, threadOneFailAccess, threadTwoFailAccess);
}
}
else
{
- ReportRequiresFailure(err.FailingCall, err.FailingRequires, true);
+ ReportRequiresFailure(err.FailingCall, err.FailingRequires);
}
}
else if (error is ReturnCounterexample)
{
ReturnCounterexample err = (ReturnCounterexample)error;
- ReportEnsuresFailure(err.FailingEnsures, true);
+ ReportEnsuresFailure(err.FailingEnsures);
}
else
{
AssertCounterexample err = (AssertCounterexample)error;
if (err.FailingAssert is LoopInitAssertCmd)
{
- ReportInvariantEntryFailure(err.FailingAssert, true);
+ ReportInvariantEntryFailure(err.FailingAssert);
}
else if (err.FailingAssert is LoopInvMaintainedAssertCmd)
{
- ReportInvariantMaintedFailure(err.FailingAssert, true);
+ ReportInvariantMaintedFailure(err.FailingAssert);
}
else
{
- ReportFailingAssert(err.FailingAssert, true);
+ ReportFailingAssert(err.FailingAssert);
}
}
errorCount++;
@@ -923,7 +1123,33 @@ namespace Microsoft.Boogie }
}
- private static void ReportFailingAssert(Absy node, bool displayCode)
+ private static void PrintDetailedTraceHeader(string colTwoHeader, string colThreeHeader, int locationColSize, int colTwoSize, int colThreeSize)
+ {
+ Console.Write("\nLocation");
+ PrintNChars(locationColSize - "Location".Length, ' ');
+ Console.WriteLine("|{0}|{1}", colTwoHeader + Chars(colTwoSize - colTwoHeader.Length, ' '), colThreeHeader + Chars(colThreeSize - colThreeHeader.Length, ' '));
+ PrintNChars(locationColSize, '-');
+ Console.Write("|");
+ PrintNChars(colTwoSize, '-');
+ Console.Write("|");
+ PrintNChars(colThreeSize, '-');
+ Console.WriteLine("");
+ }
+
+ private static void PrintNChars(int n, char c)
+ {
+ for (int i = 0; i < n; ++i)
+ {
+ Console.Write(c);
+ }
+ }
+
+ private static string Chars(int n, char c)
+ {
+ return new String(c, n);
+ }
+
+ private static void ReportFailingAssert(Absy node)
{
Console.WriteLine("");
@@ -941,13 +1167,10 @@ namespace Microsoft.Boogie locinfo = failFile + ":" + failLine + ":" + failCol + ":";
ErrorWriteLine(locinfo, "this assertion might not hold", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(FetchCodeLine(failFile, failLine));
- }
+ ErrorWriteLine(FetchCodeLine(failFile, failLine));
}
- private static void ReportInvariantMaintedFailure(Absy node, bool displayCode)
+ private static void ReportInvariantMaintedFailure(Absy node)
{
Console.WriteLine("");
@@ -965,13 +1188,10 @@ namespace Microsoft.Boogie locinfo = failFile + ":" + failLine + ":" + failCol + ":";
ErrorWriteLine(locinfo, "loop invariant might not be maintained by the loop", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(FetchCodeLine(failFile, failLine));
- }
+ ErrorWriteLine(FetchCodeLine(failFile, failLine));
}
- private static void ReportInvariantEntryFailure(Absy node, bool displayCode)
+ private static void ReportInvariantEntryFailure(Absy node)
{
Console.WriteLine("");
@@ -989,13 +1209,10 @@ namespace Microsoft.Boogie locinfo = failFile + ":" + failLine + ":" + failCol + ":";
ErrorWriteLine(locinfo, "loop invariant might not hold on entry", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(FetchCodeLine(failFile, failLine));
- }
+ ErrorWriteLine(FetchCodeLine(failFile, failLine));
}
- private static void ReportEnsuresFailure(Absy node, bool displayCode)
+ private static void ReportEnsuresFailure(Absy node)
{
Console.WriteLine("");
@@ -1013,13 +1230,10 @@ namespace Microsoft.Boogie locinfo = failFile + ":" + failLine + ":" + failCol + ":";
ErrorWriteLine(locinfo, "postcondition might not hold on all return paths", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(FetchCodeLine(failFile, failLine));
- }
+ ErrorWriteLine(FetchCodeLine(failFile, failLine));
}
- private static void ReportRace(Absy callNode, Absy reqNode, string thread1, string thread2, string group1, string group2, string arrName, int byteOffset, int elemOffset, RaceType raceType, bool displayCode)
+ private static void ReportRace(Absy callNode, Absy reqNode, string thread1, string thread2, string group1, string group2, string arrName, int byteOffset, RaceType raceType)
{
Console.WriteLine("");
int failLine1 = -1, failCol1 = -1, failLine2 = -1, failCol2 = -1;
@@ -1071,20 +1285,15 @@ namespace Microsoft.Boogie AddPadding(ref locinfo1, ref locinfo2);
AddPadding(ref access1, ref access2);
- ErrorWriteLine(locinfo1, "thread " + thread2 + " group " + group2 + " " + access2 + " " + arrName + "[" + byteOffset + "] (" + elemOffset + ")", ErrorMsgType.NoError);
- if (displayCode)
- {
- ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile1, failLine1) + "\n", 2));
- }
+ ErrorWriteLine(locinfo1, "thread " + thread2 + " group " + group2 + " " + access2 + " ((char*)" + arrName + ")[" + byteOffset + "]", ErrorMsgType.NoError);
+ ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile1, failLine1) + "\n", 2));
- ErrorWriteLine(locinfo2, "thread " + thread1 + " group " + group1 + " " + access1 + " " + arrName + "[" + byteOffset + "] (" + elemOffset + ")", ErrorMsgType.NoError);
- if (displayCode)
- {
- ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile2, failLine2) + "\n", 2));
- }
+
+ ErrorWriteLine(locinfo2, "thread " + thread1 + " group " + group1 + " " + access1 + " ((char*)" + arrName + ")[" + byteOffset + "]", ErrorMsgType.NoError);
+ ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile2, failLine2) + "\n", 2));
}
- private static void ReportBarrierDivergence(Absy node, bool displayCode)
+ private static void ReportBarrierDivergence(Absy node)
{
Console.WriteLine("");
@@ -1102,19 +1311,11 @@ namespace Microsoft.Boogie locinfo = failFile + ":" + failLine + ":" + failCol + ":";
ErrorWriteLine(locinfo, "barrier may be reached by non-uniform control flow", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(FetchCodeLine(failFile, failLine));
- }
+ ErrorWriteLine(FetchCodeLine(failFile, failLine));
}
- private static void ReportRequiresFailure(Absy callNode, Absy reqNode, bool displayCode)
+ private static void ReportRequiresFailure(Absy callNode, Absy reqNode)
{
- // TODO: Remove code duplication below.
- // bad_pre.cl:16:7: error: a precondition for this call might not hold
- // [codeline]
- // bad_pre.cl:8:24: note: this is the precondition that might not hold
- // [codeline]
Console.WriteLine("");
int failLine1 = -1, failCol1 = -1, failLine2 = -1, failCol2 = -1;
@@ -1138,17 +1339,11 @@ namespace Microsoft.Boogie locinfo2 = failFile2 + ":" + failLine2 + ":" + failCol2 + ":";
ErrorWriteLine(locinfo1, "a precondition for this call might not hold", ErrorMsgType.Error);
- if (displayCode)
- {
- ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile1, failLine1), 2));
- }
+ ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile1, failLine1), 2));
- ErrorWriteLine(locinfo2, "this is the precondition that might not hold", ErrorMsgType.Note);
- if (displayCode)
- {
- ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile2, failLine2), 2));
- }
+ ErrorWriteLine(locinfo2, "this is the precondition that might not hold", ErrorMsgType.Note);
+ ErrorWriteLine(TrimLeadingSpaces(FetchCodeLine(failFile2, failLine2), 2));
}
private static string FetchCodeLine(string path, int lineNo)
@@ -1178,30 +1373,107 @@ namespace Microsoft.Boogie {
failLine = QKeyValue.FindIntAttribute(attrs, "line", -1);
failCol = QKeyValue.FindIntAttribute(attrs, "col", -1);
- failFile = QKeyValue.FindStringAttribute(attrs, "fname");
- string directoryName = Path.GetDirectoryName(CommandLineOptions.Clo.Files[0]);
- failFile = ((!String.IsNullOrEmpty(directoryName) && directoryName != ".") ? (directoryName + Path.DirectorySeparatorChar) : "") + failFile;
+ failFile = GetFilenamePathPrefix() + QKeyValue.FindStringAttribute(attrs, "fname");
+ }
+
+ private static void GetThreadsAndGroupsFromModel(Model model, out string thread1, out string thread2, out string group1, out string group2, bool withSpaces)
+ {
+ thread1 = GetThreadOne(model, withSpaces);
+ thread2 = GetThreadTwo(model, withSpaces);
+ group1 = GetGroupOne(model, withSpaces);
+ group2 = GetGroupTwo(model, withSpaces);
+ }
+
+ private static string GetGroupTwo(Model model, bool withSpaces)
+ {
+ return "("
+ + GetGidX2(model)
+ + "," + (withSpaces ? " " : "")
+ + GetGidY2(model)
+ + "," + (withSpaces ? " " : "")
+ + GetGidZ2(model)
+ + ")";
+ }
+
+ private static int GetGidZ2(Model model)
+ {
+ return model.TryGetFunc("group_id_z$2").GetConstant().AsInt();
+ }
+
+ private static int GetGidY2(Model model)
+ {
+ return model.TryGetFunc("group_id_y$2").GetConstant().AsInt();
+ }
+
+ private static int GetGidX2(Model model)
+ {
+ return model.TryGetFunc("group_id_x$2").GetConstant().AsInt();
+ }
+
+ private static string GetGroupOne(Model model, bool withSpaces)
+ {
+ return "("
+ + GetGidX1(model)
+ + "," + (withSpaces ? " " : "")
+ + GetGidY1(model)
+ + "," + (withSpaces ? " " : "")
+ + GetGidZ1(model)
+ + ")";
}
- private static void GetIdsFromModel(Model model, out int lidx1, out int lidy1, out int lidz1, out int lidx2, out int lidy2, out int lidz2,
- out int gidx1, out int gidy1, out int gidz1, out int gidx2, out int gidy2, out int gidz2)
+ private static int GetGidZ1(Model model)
{
- lidx1 = model.TryGetFunc("local_id_x$1").GetConstant().AsInt();
- lidy1 = model.TryGetFunc("local_id_y$1").GetConstant().AsInt();
- lidz1 = model.TryGetFunc("local_id_z$1").GetConstant().AsInt();
- lidx2 = model.TryGetFunc("local_id_x$2").GetConstant().AsInt();
- lidy2 = model.TryGetFunc("local_id_y$2").GetConstant().AsInt();
- lidz2 = model.TryGetFunc("local_id_z$2").GetConstant().AsInt();
+ return model.TryGetFunc("group_id_z$1").GetConstant().AsInt();
+ }
+
+ private static int GetGidY1(Model model)
+ {
+ return model.TryGetFunc("group_id_y$1").GetConstant().AsInt();
+ }
+
+ private static int GetGidX1(Model model)
+ {
+ return model.TryGetFunc("group_id_x$1").GetConstant().AsInt();
+ }
+
+ private static string GetThreadTwo(Model model, bool withSpaces)
+ {
+ return "("
+ + GetLidX2(model)
+ + "," + (withSpaces ? " " : "")
+ + GetLidY2(model)
+ + "," + (withSpaces ? " " : "")
+ + GetLidZ2(model)
+ + ")";
+ }
- gidx1 = model.TryGetFunc("group_id_x$1").GetConstant().AsInt();
- gidy1 = model.TryGetFunc("group_id_y$1").GetConstant().AsInt();
- gidz1 = model.TryGetFunc("group_id_z$1").GetConstant().AsInt();
- gidx2 = model.TryGetFunc("group_id_x$2").GetConstant().AsInt();
- gidy2 = model.TryGetFunc("group_id_y$2").GetConstant().AsInt();
- gidz2 = model.TryGetFunc("group_id_z$2").GetConstant().AsInt();
+ private static int GetLidZ2(Model model)
+ {
+ return model.TryGetFunc("local_id_z$2").GetConstant().AsInt();
+ }
+
+ private static int GetLidY2(Model model)
+ {
+ return model.TryGetFunc("local_id_y$2").GetConstant().AsInt();
+ }
+
+ private static int GetLidX2(Model model)
+ {
+ return model.TryGetFunc("local_id_x$2").GetConstant().AsInt();
+ }
+
+ private static string GetThreadOne(Model model, bool withSpaces)
+ {
+ return "("
+ + model.TryGetFunc("local_id_x$1").GetConstant().AsInt()
+ + "," + (withSpaces ? " " : "")
+ + model.TryGetFunc("local_id_y$1").GetConstant().AsInt()
+ + "," + (withSpaces ? " " : "")
+ + model.TryGetFunc("local_id_z$1").GetConstant().AsInt()
+ + ")";
}
- private static void GetInfoFromVarAndFunc(QKeyValue attrs, Model.Func f, out int byteOffset, out int elemWidth, out int elemOffset, out string arrName)
+ private static void GetInfoFromVarAndFunc(QKeyValue attrs, Model.Func f, out int byteOffset, out int elemOffset, out int elemWidth, out string arrName)
{
Debug.Assert(f != null && f.AppCount == 1);
elemOffset = f.Apps.FirstOrDefault().Result.AsInt();
diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj index 6f616936..06300e1f 100644 --- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj +++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj @@ -43,6 +43,9 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="GetIfOfIfThenElseVisitor.cs" />
+ <Compile Include="GetRHSOfEqualityVisitor.cs" />
+ <Compile Include="GetThenOfIfThenElseVisitor.cs" />
<Compile Include="GPUVerifyBoogieDriver.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
</ItemGroup>
diff --git a/Source/GPUVerifyBoogieDriver/GetIfOfIfThenElseVisitor.cs b/Source/GPUVerifyBoogieDriver/GetIfOfIfThenElseVisitor.cs new file mode 100644 index 00000000..a7c6be8a --- /dev/null +++ b/Source/GPUVerifyBoogieDriver/GetIfOfIfThenElseVisitor.cs @@ -0,0 +1,61 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie
+{
+ class GetIfOfIfThenElseVisitor : StandardVisitor
+ {
+ IdentifierExpr result;
+
+ internal GetIfOfIfThenElseVisitor()
+ {
+ result = null;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is IfThenElse)
+ {
+ if (node.Args[0] is IdentifierExpr)
+ {
+ Debug.Assert(result == null);
+ result = node.Args[0] as IdentifierExpr;
+ }
+ else if (node.Args[0] is NAryExpr)
+ {
+ Debug.Assert(result == null);
+ result = ExtractEnabledArg((NAryExpr)node.Args[0]);
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ internal IdentifierExpr getResult()
+ {
+ Debug.Assert(result != null);
+ return result;
+ }
+
+ internal IdentifierExpr ExtractEnabledArg(NAryExpr ne)
+ {
+ if (ne.Args[0] is IdentifierExpr)
+ {
+ return (IdentifierExpr)ne.Args[0];
+ }
+ else if (ne.Args[0] is NAryExpr)
+ {
+ return ExtractEnabledArg((NAryExpr)ne.Args[0]);
+ }
+ else
+ {
+ Debug.Assert(false, "ExtractEnabledArg: not all cases covered");
+ return null;
+ }
+ }
+ }
+}
diff --git a/Source/GPUVerifyBoogieDriver/GetRHSOfEqualityVisitor.cs b/Source/GPUVerifyBoogieDriver/GetRHSOfEqualityVisitor.cs new file mode 100644 index 00000000..f13c28cf --- /dev/null +++ b/Source/GPUVerifyBoogieDriver/GetRHSOfEqualityVisitor.cs @@ -0,0 +1,43 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie
+{
+ class GetRHSOfEqualityVisitor : StandardVisitor
+ {
+
+ string LHSPattern;
+ Expr result;
+
+ internal GetRHSOfEqualityVisitor(string LHSPattern)
+ {
+ this.LHSPattern = LHSPattern;
+ result = null;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is BinaryOperator && ((BinaryOperator)node.Fun).Op == BinaryOperator.Opcode.Eq)
+ {
+ if (node.Args[0] is IdentifierExpr && Regex.IsMatch(((IdentifierExpr)node.Args[0]).Decl.Name, LHSPattern))
+ {
+ Debug.Assert(result == null);
+ result = node.Args[1];
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ internal Expr getResult()
+ {
+ Debug.Assert(result != null);
+ return result;
+ }
+
+ }
+}
diff --git a/Source/GPUVerifyBoogieDriver/GetThenOfIfThenElseVisitor.cs b/Source/GPUVerifyBoogieDriver/GetThenOfIfThenElseVisitor.cs new file mode 100644 index 00000000..dbecda97 --- /dev/null +++ b/Source/GPUVerifyBoogieDriver/GetThenOfIfThenElseVisitor.cs @@ -0,0 +1,39 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie
+{
+ class GetThenOfIfThenElseVisitor : StandardVisitor
+ {
+ LiteralExpr result;
+
+ internal GetThenOfIfThenElseVisitor()
+ {
+ result = null;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is IfThenElse)
+ {
+ if (node.Args[1] is LiteralExpr)
+ {
+ Debug.Assert(result == null);
+ result = (LiteralExpr)node.Args[1];
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ internal LiteralExpr getResult()
+ {
+ Debug.Assert(result != null);
+ return result;
+ }
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 19f98ff7..ec1514ae 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -227,6 +227,7 @@ namespace DafnyLanguage #region keywords
case "allocated":
case "array":
+ case "as":
case "assert":
case "assume":
case "bool":
@@ -250,7 +251,7 @@ namespace DafnyLanguage case "function":
case "ghost":
case "if":
- case "imports":
+ case "import":
case "in":
case "int":
case "invariant":
@@ -265,6 +266,7 @@ namespace DafnyLanguage case "null":
case "object":
case "old":
+ case "opened":
case "parallel":
case "predicate":
case "print":
|