diff options
author | Unknown <afd@afd-THINK.home> | 2012-06-21 08:11:32 +0100 |
---|---|---|
committer | Unknown <afd@afd-THINK.home> | 2012-06-21 08:11:32 +0100 |
commit | 2ab8ab15f429542148c4d87613447948e3764923 (patch) | |
tree | 4ab20daf5b0c41c316a4a3d10454c3e252d9511c /Source/VCGeneration | |
parent | d8d1b432e117d8cce68f9735cad14177816c53b6 (diff) | |
parent | bfa96e990bd3d318cce8b10a230f74e3244c062e (diff) |
Merge
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/BlockPredicator.cs | 310 | ||||
-rw-r--r-- | Source/VCGeneration/GraphAlgorithms.cs | 84 | ||||
-rw-r--r-- | Source/VCGeneration/VCGeneration.csproj | 2 |
3 files changed, 396 insertions, 0 deletions
diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs new file mode 100644 index 00000000..987574be --- /dev/null +++ b/Source/VCGeneration/BlockPredicator.cs @@ -0,0 +1,310 @@ +using Graphing; +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie { + +public class BlockPredicator { + + Program prog; + Implementation impl; + Graph<Block> blockGraph; + + bool createCandidateInvariants = true; + bool useProcedurePredicates = true; + + Expr returnBlockId; + + LocalVariable curVar, pVar; + IdentifierExpr cur, p, fp; + Expr pExpr; + Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = + new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); + Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); + HashSet<Block> doneBlocks = new HashSet<Block>(); + + BlockPredicator(Program p, Implementation i, bool cci, bool upp) { + prog = p; + impl = i; + createCandidateInvariants = cci; + useProcedurePredicates = upp; + } + + void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) { + if (!useProcedurePredicates && cmd is CallCmd) { + var trueBlock = new Block(); + blocks.Add(trueBlock); + trueBlock.Label = block.Label + ".call.true"; + trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p)); + trueBlock.Cmds.Add(cmd); + + var falseBlock = new Block(); + blocks.Add(falseBlock); + falseBlock.Label = block.Label + ".call.false"; + falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p))); + + var contBlock = new Block(); + blocks.Add(contBlock); + contBlock.Label = block.Label + ".call.cont"; + + block.TransferCmd = + new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock)); + trueBlock.TransferCmd = falseBlock.TransferCmd = + new GotoCmd(Token.NoToken, new BlockSeq(contBlock)); + nextBlock = contBlock; + } else { + PredicateCmd(block.Cmds, cmd); + nextBlock = block; + } + } + + 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) { + Debug.Assert(useProcedurePredicates); + var cCmd = (CallCmd)cmd; + cCmd.Ins.Insert(0, p); + cmdSeq.Add(cCmd); + } else if (cmd is StateCmd) { + var sCmd = (StateCmd)cmd; + var newCmdSeq = new CmdSeq(); + foreach (Cmd c in sCmd.Cmds) + PredicateCmd(newCmdSeq, c); + sCmd.Cmds = newCmdSeq; + cmdSeq.Add(sCmd); + } 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))); + } + + foreach (Block b in gCmd.labelTargets) { + if (blockGraph.Predecessors(b).Count() == 1) { + if (!doneBlocks.Contains(b)) { + var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd); + if (assumes.Count() > 0) { + foreach (AssumeCmd aCmd in assumes) { + cmdSeq.Add(new AssumeCmd(Token.NoToken, + Expr.Imp(Expr.Eq(cur, blockIds[b]), + aCmd.Expr))); + } + b.Cmds = + new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray()); + } + } + } + } + } else if (cmd is ReturnCmd) { + PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId)); + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateImplementation() { + blockGraph = prog.ProcessLoops(impl); + var sortedBlocks = blockGraph.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); + + if (useProcedurePredicates) + fp = Expr.Ident(impl.InParams[0]); + + var newBlocks = new List<Block>(); + + Block entryBlock = new Block(); + entryBlock.Label = "entry"; + entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, + CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1], + returnBlockId))); + newBlocks.Add(entryBlock); + + var prevBlock = entryBlock; + foreach (var n in sortedBlocks) { + if (n.Item2) { + var backedgeBlock = new Block(); + newBlocks.Add(backedgeBlock); + + backedgeBlock.Label = n.Item1.Label + ".backedge"; + backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, + Expr.Eq(cur, blockIds[n.Item1]), + new QKeyValue(Token.NoToken, "backedge", new List<object>(), null))); + backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(n.Item1)); + + 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(backedgeBlock, tailBlock)); + prevBlock = tailBlock; + } else { + var runBlock = n.Item1; + var oldCmdSeq = runBlock.Cmds; + runBlock.Cmds = new CmdSeq(); + newBlocks.Add(runBlock); + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(runBlock)); + + pExpr = Expr.Eq(cur, blockIds[runBlock]); + if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) { + AddUniformCandidateInvariant(runBlock.Cmds, runBlock); + AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock); + } + runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); + var transferCmd = runBlock.TransferCmd; + foreach (Cmd cmd in oldCmdSeq) + PredicateCmd(newBlocks, runBlock, cmd, out runBlock); + PredicateTransferCmd(runBlock.Cmds, transferCmd); + + prevBlock = runBlock; + doneBlocks.Add(runBlock); + } + } + + prevBlock.TransferCmd = new ReturnCmd(Token.NoToken); + impl.Blocks = newBlocks; + } + + private Expr CreateIfFPThenElse(Expr then, Expr eElse) { + if (useProcedurePredicates) { + return new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, then, eElse)); + } else { + return then; + } + } + + private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { + cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur, + CreateIfFPThenElse(blockIds[header], returnBlockId)), + "uniform loop")); + } + + private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) { + var loopNodes = new HashSet<Block>(); + foreach (var b in blockGraph.BackEdgeNodes(header)) + loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); + var exits = new HashSet<Expr>(); + foreach (var ln in loopNodes) { + if (ln.TransferCmd is GotoCmd) { + var gCmd = (GotoCmd) ln.TransferCmd; + foreach (var exit in gCmd.labelTargets.Cast<Block>() + .Where(b => !loopNodes.Contains(b))) + exits.Add(blockIds[exit]); + } + if (ln.TransferCmd is ReturnCmd) + exits.Add(returnBlockId); + } + var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]), + (e, exit) => Expr.Or(e, Expr.Eq(cur, exit))); + cs.Add(prog.CreateCandidateInvariant( + CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)), + "non-uniform loop")); + } + + public static void Predicate(Program p, + bool createCandidateInvariants = true, + bool useProcedurePredicates = true) { + foreach (var decl in p.TopLevelDeclarations.ToList()) { + if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) { + var dwf = (DeclWithFormals)decl; + var fpVar = new Formal(Token.NoToken, + new TypedIdent(Token.NoToken, "_P", + Microsoft.Boogie.Type.Bool), + /*incoming=*/true); + dwf.InParams = new VariableSeq( + (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>())) + .ToArray()); + } + var impl = decl as Implementation; + if (impl != null) + new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation(); + } + } + +} + +} diff --git a/Source/VCGeneration/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs new file mode 100644 index 00000000..def77485 --- /dev/null +++ b/Source/VCGeneration/GraphAlgorithms.cs @@ -0,0 +1,84 @@ +using Graphing; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie { + +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/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 5b2541a9..39da0be6 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -144,6 +144,7 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="BlockPredicator.cs" />
<Compile Include="Check.cs" />
<Compile Include="ConditionGeneration.cs" />
<Compile Include="Context.cs" />
@@ -151,6 +152,7 @@ <Compile Include="DoomedLoopUnrolling.cs" />
<Compile Include="DoomedStrategy.cs" />
<Compile Include="DoomErrorHandler.cs" />
+ <Compile Include="GraphAlgorithms.cs" />
<Compile Include="HasseDiagram.cs" />
<Compile Include="OrderingAxioms.cs" />
<Compile Include="StratifiedVC.cs" />
|