diff options
28 files changed, 727 insertions, 605 deletions
diff --git a/Chalice/tests/examples/list-reverse.chalice b/Chalice/tests/examples/list-reverse.chalice new file mode 100644 index 00000000..c694b4c9 --- /dev/null +++ b/Chalice/tests/examples/list-reverse.chalice @@ -0,0 +1,44 @@ +class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures r != null && r.list;
+ ensures r.vals() == old(this.reverse_vals());
+ {
+ var l : Node := this;
+ r := null;
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ unfold l.list;
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt index d8e19122..d8e19122 100644 --- a/Chalice/tests/predicates/list-reverse.output.txt +++ b/Chalice/tests/examples/list-reverse.output.txt diff --git a/Chalice/tests/predicates/list-reverse.chalice b/Chalice/tests/predicates/list-reverse.chalice deleted file mode 100644 index 5a596409..00000000 --- a/Chalice/tests/predicates/list-reverse.chalice +++ /dev/null @@ -1,158 +0,0 @@ -// this would be nice in the "examples" folder (at least, the version without the commented blocks), once the problem with old(..) is fixed
-
-class Node {
- var next : Node;
- var val : int;
-
- predicate list {
- acc(next) && acc(val) && (next!=null ==> next.list)
- }
-
- function vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : [val] ++ next.vals())
- }
-
- function reverse_vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
- }
-
- method reverse_in_place() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
- method reverse_in_place_01() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
- method reverse_in_place_10() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
-
- method reverse_in_place_11() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-}
\ No newline at end of file diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 61943cf0..0911cbd3 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -404,7 +404,7 @@ namespace Microsoft.Boogie { inline = true;
}
}
- if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ if (inline) {
foreach (var d in TopLevelDeclarations) {
var impl = d as Implementation;
if (impl != null) {
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 704c5973..90cfd6d8 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2482,6 +2482,10 @@ namespace Microsoft.Boogie { }
}
+ if (CommandLineOptions.Clo.StratifiedInlining > 0) {
+ return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint");
+ }
+
return false;
}
}
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs new file mode 100644 index 00000000..15ad2432 --- /dev/null +++ b/Source/GPUVerify/BlockPredicator.cs @@ -0,0 +1,191 @@ +using Microsoft.Boogie; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace GPUVerify { + +class BlockPredicator { + + Program prog; + Implementation impl; + + Expr returnBlockId; + + LocalVariable curVar, pVar; + IdentifierExpr cur, p; + Expr pExpr; + Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = + new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); + Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); + + BlockPredicator(Program p, Implementation i) { + prog = p; + impl = i; + } + + void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) { + if (cmd is AssignCmd) { + var aCmd = (AssignCmd)cmd; + cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss, + new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) => + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(p, rhs, lhs.AsExpr)))))); + } else if (cmd is AssertCmd) { + var aCmd = (AssertCmd)cmd; + if (cmdSeq.Last() is AssignCmd && + cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) { + // This may be a loop invariant. Make sure it continues to appear as + // the first statement in the block. + var assign = cmdSeq.Last(); + cmdSeq.Truncate(cmdSeq.Length-1); + cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr))); + cmdSeq.Add(assign); + } else { + cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); + } + } else if (cmd is AssumeCmd) { + var aCmd = (AssumeCmd)cmd; + cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); + } else if (cmd is HavocCmd) { + var hCmd = (HavocCmd)cmd; + foreach (IdentifierExpr v in hCmd.Vars) { + Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type; + Contract.Assert(type != null); + + IdentifierExpr havocTempExpr; + if (havocVars.ContainsKey(type)) { + havocTempExpr = havocVars[type]; + } else { + var havocVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, + "_HAVOC_" + type.ToString(), type)); + impl.LocVars.Add(havocVar); + havocVars[type] = havocTempExpr = + new IdentifierExpr(Token.NoToken, havocVar); + } + cmdSeq.Add(new HavocCmd(Token.NoToken, + new IdentifierExprSeq(havocTempExpr))); + cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v, + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(p, havocTempExpr, v)))); + } + } else if (cmd is CallCmd) { + var cCmd = (CallCmd)cmd; + cCmd.Ins.Insert(0, p); + cmdSeq.Add(cCmd); + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) { + if (cmd is GotoCmd) { + var gCmd = (GotoCmd)cmd; + var targets = new List<Expr>( + gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b])); + if (targets.Count == 1) { + PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0])); + } else { + PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken, + new IdentifierExprSeq(cur))); + PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken, + targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or))); + } + } else if (cmd is ReturnCmd) { + PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId)); + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateImplementation() { + var g = prog.ProcessLoops(impl); + var sortedBlocks = g.LoopyTopSort(); + + int blockId = 0; + foreach (var block in impl.Blocks) + blockIds[block] = Expr.Literal(blockId++); + returnBlockId = Expr.Literal(blockId++); + + curVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "cur", + Microsoft.Boogie.Type.Int)); + impl.LocVars.Add(curVar); + cur = Expr.Ident(curVar); + + pVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "p", + Microsoft.Boogie.Type.Bool)); + impl.LocVars.Add(pVar); + p = Expr.Ident(pVar); + + var newBlocks = new List<Block>(); + + var fp = Expr.Ident(impl.InParams[0]); + Block entryBlock = new Block(); + entryBlock.Label = "entry"; + entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, blockIds[sortedBlocks[0].Item1], + returnBlockId)))); + newBlocks.Add(entryBlock); + + var prevBlock = entryBlock; + foreach (var n in sortedBlocks) { + if (n.Item2) { + var tailBlock = new Block(); + newBlocks.Add(tailBlock); + + tailBlock.Label = n.Item1.Label + ".tail"; + tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, + Expr.Neq(cur, blockIds[n.Item1]))); + + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(tailBlock, n.Item1)); + prevBlock = tailBlock; + } else { + var runBlock = n.Item1; + newBlocks.Add(runBlock); + + pExpr = Expr.Eq(cur, blockIds[runBlock]); + CmdSeq newCmdSeq = new CmdSeq(); + newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); + foreach (Cmd cmd in runBlock.Cmds) + PredicateCmd(newCmdSeq, cmd); + PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd); + runBlock.Cmds = newCmdSeq; + + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(runBlock)); + prevBlock = runBlock; + } + } + + prevBlock.TransferCmd = new ReturnCmd(Token.NoToken); + impl.Blocks = newBlocks; + } + + public static void Predicate(Program p) { + foreach (var decl in p.TopLevelDeclarations) { + if (decl is DeclWithFormals && !(decl is Function)) { + var dwf = (DeclWithFormals)decl; + var fpVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "fp", + Microsoft.Boogie.Type.Bool)); + dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar)) + .Cast<Variable>().ToArray()); + } + var impl = decl as Implementation; + if (impl != null) + new BlockPredicator(p, impl).PredicateImplementation(); + } + } + +} + +} diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 502844b2..7e6324b2 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -40,6 +40,8 @@ namespace GPUVerify public static bool NoLoopPredicateInvariants = false;
+ public static bool Unstructured = false;
+
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -177,6 +179,11 @@ namespace GPUVerify NoLoopPredicateInvariants = true;
break;
+ case "-unstructured":
+ case "/unstructured":
+ Unstructured = true;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
@@ -216,6 +223,7 @@ namespace GPUVerify /divided : check individual pairs of possibly racing statements separately
/dividedArray : check races on arrays one at a time
/dividedElement : ???
+ /unstructured : operate on the unstructured form of the program
");
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index f6ba390b..5d5bd4d6 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -102,19 +102,35 @@ namespace GPUVerify private Procedure CheckExactlyOneKernelProcedure()
{
- return CheckSingleInstanceOfAttributedProcedure(Program, "kernel");
+ var p = CheckSingleInstanceOfAttributedProcedure("kernel");
+ if (p == null)
+ {
+ Error(Program, "\"kernel\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute");
+ }
+
+ return p;
}
- private Procedure CheckExactlyOneBarrierProcedure()
+ private Procedure FindOrCreateBarrierProcedure()
{
- return CheckSingleInstanceOfAttributedProcedure(Program, "barrier");
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier");
+ if (p == null)
+ {
+ p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),
+ new VariableSeq(), new VariableSeq(),
+ new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ }
+ return p;
}
- private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)
+ private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)
{
Procedure attributedProcedure = null;
- foreach (Declaration decl in program.TopLevelDeclarations)
+ foreach (Declaration decl in Program.TopLevelDeclarations)
{
if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))
{
@@ -144,11 +160,6 @@ namespace GPUVerify }
}
- if (attributedProcedure == null)
- {
- Error(program, "\"{0}\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute", attribute);
- }
-
return attributedProcedure;
}
@@ -189,10 +200,20 @@ namespace GPUVerify return true;
}
- private bool FindNonLocalVariables(Program program)
+ private void MaybeCreateAttributedConst(string attr, ref Constant constFieldRef)
+ {
+ if (constFieldRef == null)
+ {
+ constFieldRef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, attr, Microsoft.Boogie.Type.GetBvType(32)));
+ constFieldRef.AddAttribute(attr);
+ Program.TopLevelDeclarations.Add(constFieldRef);
+ }
+ }
+
+ private bool FindNonLocalVariables()
{
bool success = true;
- foreach (Declaration D in program.TopLevelDeclarations)
+ foreach (Declaration D in Program.TopLevelDeclarations)
{
if (D is Variable && (D as Variable).IsMutable)
{
@@ -232,6 +253,22 @@ namespace GPUVerify }
}
+ MaybeCreateAttributedConst(LOCAL_ID_X_STRING, ref _X);
+ MaybeCreateAttributedConst(LOCAL_ID_Y_STRING, ref _Y);
+ MaybeCreateAttributedConst(LOCAL_ID_Z_STRING, ref _Z);
+
+ MaybeCreateAttributedConst(GROUP_SIZE_X_STRING, ref _GROUP_SIZE_X);
+ MaybeCreateAttributedConst(GROUP_SIZE_Y_STRING, ref _GROUP_SIZE_Y);
+ MaybeCreateAttributedConst(GROUP_SIZE_Z_STRING, ref _GROUP_SIZE_Z);
+
+ MaybeCreateAttributedConst(GROUP_ID_X_STRING, ref _GROUP_X);
+ MaybeCreateAttributedConst(GROUP_ID_Y_STRING, ref _GROUP_Y);
+ MaybeCreateAttributedConst(GROUP_ID_Z_STRING, ref _GROUP_Z);
+
+ MaybeCreateAttributedConst(NUM_GROUPS_X_STRING, ref _NUM_GROUPS_X);
+ MaybeCreateAttributedConst(NUM_GROUPS_Y_STRING, ref _NUM_GROUPS_Y);
+ MaybeCreateAttributedConst(NUM_GROUPS_Z_STRING, ref _NUM_GROUPS_Z);
+
return success;
}
@@ -307,6 +344,10 @@ namespace GPUVerify internal void doit()
{
+ if (CommandLineOptions.Unstructured)
+ {
+ Microsoft.Boogie.CommandLineOptions.Clo.PrintUnstructured = 2;
+ }
if (CommandLineOptions.ShowStages)
{
@@ -1920,7 +1961,7 @@ namespace GPUVerify if (d is Implementation)
{
- new KernelDualiser(this).DualiseImplementation(d as Implementation);
+ new KernelDualiser(this).DualiseImplementation(d as Implementation, CommandLineOptions.Unstructured);
NewTopLevelDeclarations.Add(d as Implementation);
@@ -1946,6 +1987,12 @@ namespace GPUVerify private void MakeKernelPredicated()
{
+ if (CommandLineOptions.Unstructured)
+ {
+ BlockPredicator.Predicate(Program);
+ return;
+ }
+
foreach (Declaration d in Program.TopLevelDeclarations)
{
if (d is Procedure)
@@ -2007,7 +2054,7 @@ namespace GPUVerify private int Check()
{
- BarrierProcedure = CheckExactlyOneBarrierProcedure();
+ BarrierProcedure = FindOrCreateBarrierProcedure();
KernelProcedure = CheckExactlyOneKernelProcedure();
if (ErrorCount > 0)
@@ -2025,101 +2072,15 @@ namespace GPUVerify Error(BarrierProcedure, "Barrier procedure must not return any results");
}
- if (!FindNonLocalVariables(Program))
+ if (!FindNonLocalVariables())
{
return ErrorCount;
}
CheckKernelImplementation();
-
- if (!KernelHasIdX())
- {
- MissingKernelAttributeError(LOCAL_ID_X_STRING);
- }
-
- if (!KernelHasGroupSizeX())
- {
- MissingKernelAttributeError(GROUP_SIZE_X_STRING);
- }
-
- if (!KernelHasNumGroupsX())
- {
- MissingKernelAttributeError(NUM_GROUPS_X_STRING);
- }
-
- if (!KernelHasGroupIdX())
- {
- MissingKernelAttributeError(GROUP_ID_X_STRING);
- }
-
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError(LOCAL_ID_Y_STRING);
- }
-
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
- }
-
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
- }
-
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError(GROUP_ID_Y_STRING);
- }
-
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError(LOCAL_ID_Y_STRING);
- }
-
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
- }
-
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
- }
-
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError(GROUP_ID_Y_STRING);
- }
-
- if (!KernelHasIdZ())
- {
- MissingKernelAttributeError(LOCAL_ID_Z_STRING);
- }
-
- if (!KernelHasGroupSizeZ())
- {
- MissingKernelAttributeError(GROUP_SIZE_Z_STRING);
- }
-
- if (!KernelHasNumGroupsZ())
- {
- MissingKernelAttributeError(NUM_GROUPS_Z_STRING);
- }
-
- if (!KernelHasGroupIdZ())
- {
- MissingKernelAttributeError(GROUP_ID_Z_STRING);
- }
-
return ErrorCount;
}
- private void MissingKernelAttributeError(string attribute)
- {
- Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");
- }
-
public static bool IsThreadLocalIdConstant(Variable variable)
{
return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index b375efd9..27b9abe5 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,6 +108,8 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="BlockPredicator.cs" />
+ <Compile Include="GraphAlgorithms.cs" />
<Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
<Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
@@ -158,6 +160,10 @@ <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>
diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs new file mode 100644 index 00000000..3442a64d --- /dev/null +++ b/Source/GPUVerify/GraphAlgorithms.cs @@ -0,0 +1,84 @@ +using Graphing; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace GPUVerify { + +public static class GraphAlgorithms { + + public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) { + Contract.Assert(g.Reducible); + + int n = g.Nodes.Count; + var nodeToNumber = new Dictionary<Node, int>(n); + var numberToNode = new Node[n]; + var allNodes = new List<int>(); + int counter = 0; + foreach (Node node in g.Nodes) { + numberToNode[counter] = node; + nodeToNumber[node] = counter; + allNodes.Add(counter); + counter++; + } + + var loops = new List<int>[n]; + foreach (var h in g.Headers) { + var loopNodes = new HashSet<Node>(); + foreach (var b in g.BackEdgeNodes(h)) + loopNodes.UnionWith(g.NaturalLoops(h, b)); + loops[nodeToNumber[h]] = + new List<int>(loopNodes.Select(node => nodeToNumber[node])); + } + + var successors = new List<int>[n]; + int[] incomingEdges = new int[n]; + + foreach (var e in g.Edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2]; + if (loops[target] == null || !loops[target].Contains(source)) { + if (successors[source] == null) + successors[source] = new List<int>(); + successors[source].Add(target); + incomingEdges[target]++; + } + } + + var sortedNodes = new List<Tuple<Node, bool>>(); + + var regionStack = new Stack<Tuple<Node, List<int>>>(); + regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes)); + + while (regionStack.Count != 0) { + int rootIndex = -1; + foreach (var i in regionStack.Peek().Item2) { + if (incomingEdges[i] == 0) { + rootIndex = i; + break; + } + } + if (rootIndex == -1) { + var region = regionStack.Pop(); + if (regionStack.Count != 0) + sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true)); + continue; + } + incomingEdges[rootIndex] = -1; + sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false)); + if (successors[rootIndex] != null) + foreach (int s in successors[rootIndex]) + incomingEdges[s]--; + if (loops[rootIndex] != null) + regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex], + loops[rootIndex])); + } + + return sortedNodes; + } + +} + +} diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 0496a4e0..8d51e74e 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -82,145 +82,150 @@ namespace GPUVerify return result;
}
- private BigBlock MakeDual(BigBlock bb)
+ private void MakeDual(CmdSeq cs, Cmd c)
{
- // Not sure what to do about the transfer command
-
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- foreach (Cmd c in bb.simpleCmds)
+ if (c is CallCmd)
{
- if (c is CallCmd)
- {
- CallCmd Call = c as CallCmd;
+ CallCmd Call = c as CallCmd;
- List<Expr> uniformNewIns = new List<Expr>();
- List<Expr> nonUniformNewIns = new List<Expr>();
- for (int i = 0; i < Call.Ins.Count; i++)
+ List<Expr> uniformNewIns = new List<Expr>();
+ List<Expr> nonUniformNewIns = new List<Expr>();
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))
{
- if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))
- {
- uniformNewIns.Add(Call.Ins[i]);
- }
- else
- {
- nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
- }
+ uniformNewIns.Add(Call.Ins[i]);
}
- for (int i = 0; i < Call.Ins.Count; i++)
+ else
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
- {
- nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
- }
+ nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
}
+ }
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
+ {
+ nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
+ }
+ }
- List<Expr> newIns = uniformNewIns;
- newIns.AddRange(nonUniformNewIns);
+ List<Expr> newIns = uniformNewIns;
+ newIns.AddRange(nonUniformNewIns);
- List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();
- List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();
- for (int i = 0; i < Call.Outs.Count; i++)
+ List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();
+ List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();
+ for (int i = 0; i < Call.Outs.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))
{
- if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))
- {
- uniformNewOuts.Add(Call.Outs[i]);
- }
- else
- {
- nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
- }
-
+ uniformNewOuts.Add(Call.Outs[i]);
}
- for (int i = 0; i < Call.Outs.Count; i++)
+ else
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
- {
- nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
- }
+ nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
}
- List<IdentifierExpr> newOuts = uniformNewOuts;
- newOuts.AddRange(nonUniformNewOuts);
-
- CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
-
- NewCallCmd.Proc = Call.Proc;
-
- result.simpleCmds.Add(NewCallCmd);
}
- else if (c is AssignCmd)
+ for (int i = 0; i < Call.Outs.Count; i++)
{
- AssignCmd assign = c as AssignCmd;
-
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- if (assign.Lhss[0] is SimpleAssignLhs &&
- verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
{
- result.simpleCmds.Add(assign);
+ nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
}
- else
- {
- List<AssignLhs> newLhss = new List<AssignLhs>();
- List<Expr> newRhss = new List<Expr>();
+ }
- newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ List<IdentifierExpr> newOuts = uniformNewOuts;
+ newOuts.AddRange(nonUniformNewOuts);
- newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
- AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
+ NewCallCmd.Proc = Call.Proc;
- result.simpleCmds.Add(newAssign);
- }
+ cs.Add(NewCallCmd);
+ }
+ else if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+
+ if (assign.Lhss[0] is SimpleAssignLhs &&
+ verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ {
+ cs.Add(assign);
}
- else if (c is HavocCmd)
+ else
{
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
+ List<AssignLhs> newLhss = new List<AssignLhs>();
+ List<Expr> newRhss = new List<Expr>();
+
+ newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+
+ newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+
+ AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
+
+ cs.Add(newAssign);
+ }
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
- HavocCmd newHavoc;
+ HavocCmd newHavoc;
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
- (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
+ (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
- result.simpleCmds.Add(newHavoc);
+ cs.Add(newHavoc);
+ }
+ else if (c is AssertCmd)
+ {
+ AssertCmd ass = c as AssertCmd;
+ if (ContainsAsymmetricExpression(ass.Expr))
+ {
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
- else if (c is AssertCmd)
+ else
{
- AssertCmd ass = c as AssertCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
- }
+ cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
- else if (c is AssumeCmd)
+ }
+ else if (c is AssumeCmd)
+ {
+ AssumeCmd ass = c as AssumeCmd;
+ if (ContainsAsymmetricExpression(ass.Expr))
{
- AssumeCmd ass = c as AssumeCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
- }
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
else
{
- Debug.Assert(false);
+ cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
}
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+
+ private BigBlock MakeDual(BigBlock bb)
+ {
+ // Not sure what to do about the transfer command
+
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ MakeDual(result.simpleCmds, c);
+ }
if (bb.ec is WhileCmd)
{
@@ -262,6 +267,16 @@ namespace GPUVerify }
+ private Block MakeDual(Block b)
+ {
+ Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);
+ foreach (Cmd c in b.Cmds)
+ {
+ MakeDual(result.Cmds, c);
+ }
+ return result;
+ }
+
private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
{
List<PredicateCmd> result = new List<PredicateCmd>();
@@ -345,14 +360,17 @@ namespace GPUVerify }
- internal void DualiseImplementation(Implementation impl)
+ internal void DualiseImplementation(Implementation impl, bool unstructured)
{
procName = impl.Name;
impl.InParams = DualiseVariableSequence(impl.InParams);
impl.OutParams = DualiseVariableSequence(impl.OutParams);
MakeDualLocalVariables(impl);
- impl.StructuredStmts = MakeDual(impl.StructuredStmts);
+ if (unstructured)
+ impl.Blocks = new List<Block>(impl.Blocks.Select(MakeDual));
+ else
+ impl.StructuredStmts = MakeDual(impl.StructuredStmts);
procName = null;
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 8f9f7498..e69c38b1 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -52,9 +52,7 @@ namespace VC Implementation impl = decl as Implementation;
if (impl == null) continue;
Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
- if (impl.Proc.FindExprAttribute("inline") != null) {
- implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
- }
+ implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
}
this.GenerateRecordFunctions();
PersistCallTree = false;
@@ -136,58 +134,63 @@ namespace VC return node;
}
}
-
- public class StratifiedVC {
- private static int newVarCount = 0;
- private static VCExprVar CreateNewVar(ProverInterface prover, Microsoft.Boogie.Type type) {
- string newName = "StratifiedInlining@" + newVarCnt.ToString();
- newVarCount++;
- Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
- prover.Context.DeclareConstant(newVar, false, null);
- return prover.VCExprGen.Variable(newVar.Name, type);
- }
- private static int idCount = 0;
+ private int newVarCount = 0;
+ public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
+ string newName = "StratifiedInlining@" + newVarCnt.ToString();
+ newVarCount++;
+ Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
+ prover.Context.DeclareConstant(newVar, false, null);
+ return prover.VCExprGen.Variable(newVar.Name, type);
+ }
+ private int idCount = 1; // 0 is reserved for the VC of main
+ public int CreateNewId() {
+ return idCount++;
+ }
+
+ public class StratifiedVC {
+ StratifiedInliningInfo info;
int id;
- Implementation impl;
List<VCExprVar> interfaceExprVars;
List<StratifiedCallSite> callSites;
VCExpr vcexpr;
public Dictionary<Block, VCExprVar> reachVars;
- public StratifiedVC(StratifiedInliningInfo info, StratifiedVCGen vcgen) {
+ public StratifiedVC(StratifiedInliningInfo siInfo) {
+ info = siInfo;
if (!info.initialized) {
- info.GenerateVC(vcgen);
+ info.GenerateVC();
}
- impl = info.impl;
- interfaceExprVars = new List<VCExprVar>();
VCExpr expansion = info.vcexpr;
+ var vcgen = info.vcgen;
var prover = vcgen.prover;
VCExpressionGenerator gen = prover.VCExprGen;
var bet = prover.Context.BoogieExprTranslator;
VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);
- id = idCount++;
+ id = vcgen.CreateNewId();
VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
expansion = gen.And(eqExpr, expansion);
+ interfaceExprVars = new List<VCExprVar>();
Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
foreach (VCExprVar v in info.interfaceExprVars) {
- VCExprVar newVar = CreateNewVar(prover, v.Type);
+ VCExprVar newVar = vcgen.CreateNewVar(v.Type);
interfaceExprVars.Add(newVar);
substDict.Add(v, newVar);
}
foreach (VCExprVar v in info.privateExprVars) {
- substDict.Add(v, CreateNewVar(prover, v.Type));
+ substDict.Add(v, vcgen.CreateNewVar(v.Type));
}
VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
expansion = substVisitor.Mutate(expansion, subst);
-
+
+ var impl = info.impl;
reachVars = new Dictionary<Block, VCExprVar>();
Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();
foreach (Block b in impl.Blocks) {
- reachVars[b] = CreateNewVar(prover, Bpl.Type.Bool);
+ reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);
reachExprs[b] = VCExpressionGenerator.False;
}
foreach (Block b in impl.Blocks) {
@@ -209,7 +212,16 @@ namespace VC foreach (CallSite cs in info.callSites) {
callSites.Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
}
+ }
+ public VCExpr Attach(StratifiedCallSite stratifiedCallSite) {
+ Contract.Assert(interfaceExprVars.Count == stratifiedCallSite.interfaceExprVars.Count);
+ VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;
+ VCExpr ret = gen.Eq(stratifiedCallSite.reachVar, reachVars[info.impl.Blocks[0]]);
+ for (int i = 0; i < stratifiedCallSite.interfaceExprVars.Count; i++) {
+ ret = gen.And(ret, gen.Eq(stratifiedCallSite.interfaceExprVars[i], interfaceExprVars[i]));
+ }
+ return ret;
}
}
@@ -225,9 +237,9 @@ namespace VC }
public class StratifiedCallSite {
- CallSite callSite;
- List<VCExpr> interfaceExprVars;
- VCExprVar reachVar;
+ public CallSite callSite;
+ public List<VCExpr> interfaceExprVars;
+ public VCExprVar reachVar;
public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {
callSite = cs;
@@ -240,6 +252,7 @@ namespace VC }
public class StratifiedInliningInfo {
+ public StratifiedVCGen vcgen;
public Implementation impl;
public Function function;
public Variable controlFlowVariable;
@@ -252,7 +265,8 @@ namespace VC public List<CallSite> callSites;
public bool initialized;
- public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen vcgen) {
+ public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen stratifiedVcGen) {
+ vcgen = stratifiedVcGen;
impl = implementation;
VariableSeq functionInterfaceVars = new VariableSeq();
@@ -298,7 +312,7 @@ namespace VC initialized = false;
}
- public void GenerateVC(StratifiedVCGen vcgen) {
+ public void GenerateVC() {
List<Variable> outputVariables = new List<Variable>();
assertExpr = new LiteralExpr(Token.NoToken, true);
foreach (Variable v in impl.OutParams) {
@@ -1054,7 +1068,7 @@ namespace VC public ApiChecker checker2;
public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {
- prover.Assert(vcMain, false);
+ prover.Assert(vcMain, true);
this.calls = calls;
this.checker = new ApiChecker(prover, reporter);
vcSize = 0;
@@ -1087,7 +1101,7 @@ namespace VC foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
{
Contract.Assert(info != null);
- info.GenerateVC(this);
+ info.GenerateVC();
}
// Get the VC of the current procedure
@@ -1285,8 +1299,10 @@ namespace VC public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)
{
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+ return Outcome.Correct;
Debug.Assert(this.program == program);
+
var computeUnderBound = true;
#region stratified inlining options
@@ -1320,11 +1336,12 @@ namespace VC }
// Get the VC of the current procedure
- VCExpr vc;
- Hashtable/*<int, Absy!>*/ mainLabel2absy;
- StratifiedInliningErrorReporter reporter;
- GetVC(impl, program, prover, callback, out vc, out mainLabel2absy, out reporter);
-
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
+ info.GenerateVC();
+ VCExpr vc = info.vcexpr;
+ Hashtable mainLabel2absy = info.label2absy;
+ var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info.mvInfo, prover.Context, program, impl);
+
// Find all procedure calls in vc and put labels on them
FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
calls.setCurrProcAsMain();
@@ -1773,7 +1790,7 @@ namespace VC StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
if (!info.initialized)
{
- info.GenerateVC(this);
+ info.GenerateVC();
}
//Console.WriteLine("Inlining {0}", procName);
VCExpr expansion = cce.NonNull(info.vcexpr);
@@ -1883,7 +1900,7 @@ namespace VC }
reporter = new StratifiedInliningErrorReporter(
- cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, gotoCmdOrigins, program, impl);
+ cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, program, impl);
}
@@ -2467,7 +2484,6 @@ namespace VC Program/*!*/ program;
Implementation/*!*/ mainImpl;
ProverContext/*!*/ context;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
public bool underapproximationMode;
public List<int>/*!*/ candidatesToExpand;
@@ -2487,7 +2503,6 @@ namespace VC public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,
Program/*!*/ program, Implementation/*!*/ mainImpl)
{
Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
@@ -2505,7 +2520,6 @@ namespace VC this.underapproximationMode = false;
this.calls = null;
this.candidatesToExpand = new List<int>();
- this.gotoCmdOrigins = gotoCmdOrigins;
}
public void SetCandidateHandler(FCallHandler calls)
@@ -2637,21 +2651,14 @@ namespace VC Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);
candidatesToExpand = new List<int>();
+ var cex = GenerateTraceMain(labels, model, mvInfo);
- if (underapproximationMode) {
- var cex = GenerateTraceMain(labels, model, mvInfo);
+ if (underapproximationMode && cex != null) {
Debug.Assert(candidatesToExpand.All(calls.isSkipped));
- if (cex != null) {
- GetModelWithStates(model);
- callback.OnCounterexample(cex, null);
- this.PrintModel(model);
- }
- return;
+ GetModelWithStates(model);
+ callback.OnCounterexample(cex, null);
+ this.PrintModel(model);
}
-
- Contract.Assert(calls != null);
-
- GenerateTraceMain(labels, model, mvInfo);
}
// Construct the interprocedural trace
@@ -2663,28 +2670,7 @@ namespace VC }
orderedStateIds = new List<Tuple<int, int>>();
- Counterexample newCounterexample =
- GenerateTrace(labels, errModel, 0, mainImpl);
-
- if (newCounterexample == null)
- return null;
-
- #region Map passive program errors back to original program errors
- ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;
- if (returnExample != null && gotoCmdOrigins != null) {
- foreach (Block b in returnExample.Trace) {
- Contract.Assert(b != null);
- Contract.Assume(b.TransferCmd != null);
- ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];
- if (cmd != null) {
- returnExample.FailingReturn = cmd;
- break;
- }
- }
- }
- #endregion
-
- return newCounterexample;
+ return GenerateTrace(labels, errModel, 0, mainImpl);
}
private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index bf30d427..08b1fffc 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -1,58 +1,58 @@ ----- Running regression test t1.bpl
-t1.bpl(38,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(19,3): anon0
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(17,3): anon0
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(27,3): anon3_LoopBody
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(26,3): anon3_LoopBody
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(27,3): anon3_LoopBody
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(26,3): anon3_LoopBody
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(33,3): anon3_LoopDone
- t1.bpl(37,3): anon2
+ t1.bpl(32,3): anon3_LoopDone
+ t1.bpl(36,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test t2.bpl
-t2.bpl(51,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t2.bpl(19,3): anon0
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(16,3): anon0
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(27,3): anon3_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(42,3): lab1_LoopDone
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(25,3): anon3_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(40,3): lab1_LoopDone
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(27,3): anon3_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(42,3): lab1_LoopDone
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(25,3): anon3_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(40,3): lab1_LoopDone
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(46,3): anon3_LoopDone
- t2.bpl(50,3): anon2
+ t2.bpl(44,3): anon3_LoopDone
+ t2.bpl(48,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -61,30 +61,25 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-----
----- Running regression test t3.bpl with recursion bound 4
-t3.bpl(38,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t3.bpl(19,3): anon0
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(15,3): anon0
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(27,3): anon3_LoopBody
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(24,3): anon3_LoopBody
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(27,3): anon3_LoopBody
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(24,3): anon3_LoopBody
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(33,3): anon3_LoopDone
- t3.bpl(37,3): anon2
+ t3.bpl(30,3): anon3_LoopDone
+ t3.bpl(34,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
------ Running regression test detLoopExtract.bpl with deterministicExtractLoops
-Stratified Inlining: Reached recursion bound of 4
-
-Boogie program verifier finished with 2 verified, 0 errors
------
diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl index 58b89e6b..00df45e9 100644 --- a/Test/extractloops/t1.bpl +++ b/Test/extractloops/t1.bpl @@ -1,22 +1,21 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-procedure {:inline 1} {:verify false} foo();
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead;
@@ -35,7 +34,7 @@ implementation A() goto anon2;
anon2:
- assert x == 1;
+ assume x != 1;
return;
}
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl index d0011929..93f80f20 100644 --- a/Test/extractloops/t2.bpl +++ b/Test/extractloops/t2.bpl @@ -1,22 +1,20 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-procedure {:inline 1} {:verify false} foo();
-
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead;
@@ -48,8 +46,6 @@ implementation A() goto anon2;
anon2:
- assert false;
- assert x == 1;
return;
}
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl index e5fad6d1..d14767ab 100644 --- a/Test/extractloops/t3.bpl +++ b/Test/extractloops/t3.bpl @@ -1,22 +1,19 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-
-procedure {:inline 1} {:verify false} foo();
-
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead, anon3_LoopBody;
@@ -35,7 +32,7 @@ implementation A() goto anon2;
anon2:
- assert x == 1;
+ assume x != 1;
return;
}
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index 77b00b19..dd5344e8 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,8 +1,7 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar1.bpl(24,3): anon0
+ bar1.bpl(22,3): anon0
Inlined call to procedure foo begins
bar1.bpl(13,5): anon0
Inlined call to procedure bar begins
@@ -16,25 +15,24 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar2.bpl
-bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(19,3): anon0
+ bar2.bpl(18,3): anon0
Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
+ bar2.bpl(4,3): anon0
+ bar2.bpl(5,7): anon3_Then
Inlined call to procedure foo ends
Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
+ bar2.bpl(4,3): anon0
+ bar2.bpl(8,7): anon3_Else
Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar3.bpl(38,3): anon0
+ bar3.bpl(35,3): anon0
Inlined call to procedure foo begins
bar3.bpl(18,3): anon0
bar3.bpl(19,7): anon3_Then
@@ -63,7 +61,7 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-----
----- Running regression test bar7.bpl
-bar7.bpl(42,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar7.bpl(35,5): anon0
bar7.bpl(37,5): anon4_Then
@@ -156,7 +154,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar8.bpl
-bar8.bpl(41,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar8.bpl(34,5): anon0
bar8.bpl(36,5): anon4_Then
@@ -249,7 +247,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar9.bpl
-bar9.bpl(44,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar9.bpl(35,5): anon0
bar9.bpl(41,5): anon4_Else
@@ -386,7 +384,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar10.bpl
-bar10.bpl(40,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar10.bpl(35,5): anon0
Inlined call to procedure bar1 begins
@@ -485,10 +483,9 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar11.bpl
-bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.
-bar11.bpl(26,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar11.bpl(30,3): anon0
+ bar11.bpl(26,3): anon0
Inlined call to procedure foo begins
bar11.bpl(15,3): anon0
value = 0
diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl index 845954d5..bd210f70 100644 --- a/Test/stratifiedinline/bar1.bpl +++ b/Test/stratifiedinline/bar1.bpl @@ -1,13 +1,13 @@ var x: int;
var y: int;
-procedure {:inline 1} bar()
+procedure bar()
modifies y;
{
y := y + 1;
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
x := x + 1;
@@ -16,11 +16,11 @@ modifies x, y; x := x + 1;
}
-procedure main()
-requires x == y;
-ensures x != y;
+procedure {:entrypoint} main()
modifies x, y;
{
+ assume x == y;
call foo();
+ assume x == y;
}
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl index 8cfcfc13..ab1e4748 100644 --- a/Test/stratifiedinline/bar10.bpl +++ b/Test/stratifiedinline/bar10.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -37,5 +37,5 @@ modifies i; call bar2(0);
i := 0;
call foo();
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl index baad27a1..67e21ba6 100644 --- a/Test/stratifiedinline/bar11.bpl +++ b/Test/stratifiedinline/bar11.bpl @@ -2,14 +2,14 @@ var x: int; var y: int;
procedure boogie_si_record_int(x:int);
-procedure {:inline 1} bar()
+procedure bar()
modifies y;
{
y := y + 1;
call boogie_si_record_int(y);
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
call boogie_si_record_int(x);
@@ -20,13 +20,12 @@ modifies x, y; call boogie_si_record_int(x);
}
-procedure main()
-requires x == 0;
-requires x == y;
-ensures x != y;
+procedure {:entrypoint} main()
modifies x, y;
{
-
+ assume x == 0;
+ assume x == y;
call foo();
+ assume x == y;
}
diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl index 76991a8f..6c383591 100644 --- a/Test/stratifiedinline/bar2.bpl +++ b/Test/stratifiedinline/bar2.bpl @@ -1,5 +1,4 @@ -
-procedure {:inline 1} foo() returns (x: bool)
+procedure foo() returns (x: bool)
{
var b: bool;
if (b) {
@@ -11,14 +10,14 @@ procedure {:inline 1} foo() returns (x: bool) }
}
-procedure main()
+procedure {:entrypoint} main()
{
var b1: bool;
var b2: bool;
call b1 := foo();
call b2 := foo();
- assert b1 == b2;
+ assume b1 != b2;
}
diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl index 7bd91184..a1f0bea3 100644 --- a/Test/stratifiedinline/bar3.bpl +++ b/Test/stratifiedinline/bar3.bpl @@ -1,7 +1,7 @@ var y: int;
var x: int;
-procedure {:inline 1} bar(b: bool)
+procedure bar(b: bool)
modifies y;
{
if (b) {
@@ -11,7 +11,7 @@ modifies y; }
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
var b: bool;
@@ -29,13 +29,11 @@ modifies x, y; }
-procedure main()
-requires x == y;
-ensures x == y;
+procedure {:entrypoint} main()
modifies x, y;
-modifies y;
{
+ assume x == y;
call foo();
- assert x == y;
call bar(false);
+ assume x != y;
}
diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl index 84640811..4b3a6ee2 100644 --- a/Test/stratifiedinline/bar4.bpl +++ b/Test/stratifiedinline/bar4.bpl @@ -1,7 +1,7 @@ var y: int;
var x: int;
-procedure {:inline 1} bar() returns (b: bool)
+procedure bar() returns (b: bool)
modifies y;
{
if (b) {
@@ -11,7 +11,7 @@ modifies y; }
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
var b: bool;
@@ -25,14 +25,13 @@ modifies x, y; }
-procedure main() returns (b: bool)
-requires x == y;
-ensures !b ==> x == y+1;
-ensures b ==> x+1 == y;
+procedure {:entrypoint} main() returns (b: bool)
modifies x, y;
-modifies y;
{
+ assume x == y;
call foo();
- assert x == y;
- call b := bar();
+ if (x == y) {
+ call b := bar();
+ assume (if b then x+1 != y else x != y+1);
+ }
}
diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index e133aef7..dd528f6f 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,6 +1,6 @@ var M: [int]int;
-procedure {:inline 1} bar(y: int) returns (b: bool)
+procedure bar(y: int) returns (b: bool)
modifies M;
{
if (b) {
@@ -10,7 +10,7 @@ modifies M; }
}
-procedure {:inline 1} foo(x: int, y: int)
+procedure foo(x: int, y: int)
modifies M;
{
var b: bool;
@@ -23,14 +23,14 @@ modifies M; }
}
-procedure main(x: int, y: int) returns (b: bool)
-requires x != y;
-requires M[x] == M[y];
-ensures !b ==> M[x] == M[y]+1;
-ensures b ==> M[x]+1 == M[y];
+procedure {:entrypoint} main(x: int, y: int) returns (b: bool)
modifies M;
{
+ assume x != y;
+ assume M[x] == M[y];
call foo(x, y);
- assert M[x] == M[y];
- call b := bar(y);
+ if (M[x] == M[y]) {
+ call b := bar(y);
+ assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);
+ }
}
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index b28777bd..41cf612e 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -39,5 +39,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index e96655f3..356645e6 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m) {
@@ -19,7 +19,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -28,7 +28,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -38,5 +38,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl index 12de78ad..d1eacb18 100644 --- a/Test/stratifiedinline/bar9.bpl +++ b/Test/stratifiedinline/bar9.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo(x: int)
+procedure foo(x: int)
modifies i;
{
if (i < x) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -41,5 +41,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/_admin/Chalice/aste/summary.log b/_admin/Chalice/aste/summary.log index e676ecd8..ade80273 100644 --- a/_admin/Chalice/aste/summary.log +++ b/_admin/Chalice/aste/summary.log @@ -1,9 +1,9 @@ -# Aste started: 2012-05-22 09:04:38
+# Aste started: 2012-05-25 09:05:16
# Host id: Boogiebox
# Configuration: chalice.cfg
# Task: aste.tasks.chalice.FullBuild
-# [2012-05-22 09:05:24] Chalice revision: 5b532a1a7343
-[2012-05-22 09:06:48] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"
+# [2012-05-25 09:06:05] Chalice revision: 8d9c6d63a543
+[2012-05-25 09:07:29] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:77: case class `class SeqClass' has case class ancestor `class Class'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:111: case class `class TokenClass' has case class ancestor `class Class'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
@@ -11,6 +11,5 @@ [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:141: case class `class TokenType' has case class ancestor `class Type'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:168: case class `class SpecialField' has case class ancestor `class Field'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:227: case class `class SpecialVariable' has case class ancestor `class Variable'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
-[2012-05-22 10:22:41] 1 out of 83 test(s) failed
-['list-reverse.chalice\r']
-# [2012-05-22 10:23:44] Released nightly of Chalice
+[2012-05-25 10:22:31] 0 out of 83 test(s) failed
+# [2012-05-25 10:23:12] Released nightly of Chalice
|