diff options
| author |  stefanheule <unknown> | 2012-03-09 02:33:36 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-09 02:33:36 -0800 |
| commit | 1edc06c71b783d4a70d3e0e8a011fc47e78d3c3a (patch) | |
| tree | c0cd27c346d06c7111f6ae6e127cfae8e7fadac2 /Source/GPUVerify/StructuredProgramVisitor.cs | |
| parent | 55b69a7c7d029c9fbd607f563ecd23087141b298 (diff) | |
| parent | 68f2b9caf8b5d64399eb8e74daf75788bec74e4f (diff) | |
Automatic merge.
Diffstat (limited to 'Source/GPUVerify/StructuredProgramVisitor.cs')
| -rw-r--r-- | Source/GPUVerify/StructuredProgramVisitor.cs | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/Source/GPUVerify/StructuredProgramVisitor.cs b/Source/GPUVerify/StructuredProgramVisitor.cs new file mode 100644 index 00000000..4b2d1c47 --- /dev/null +++ b/Source/GPUVerify/StructuredProgramVisitor.cs @@ -0,0 +1,152 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class StructuredProgramVisitor
+ {
+
+ public virtual StmtList VisitStmtList(StmtList stmtList)
+ {
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ result.BigBlocks.AddRange(VisitBigBlock(bb));
+ }
+
+ return result;
+
+ }
+
+ public virtual List<BigBlock> VisitBigBlock(BigBlock bb)
+ {
+ BigBlock firstBigBlock = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ firstBigBlock.simpleCmds = VisitCmdSeq(bb.simpleCmds);
+
+ if (bb.ec is WhileCmd)
+ {
+ firstBigBlock.ec = VisitWhileCmd(bb.ec as WhileCmd);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ firstBigBlock.ec = VisitIfCmd(bb.ec as IfCmd);
+ }
+ else if (bb.ec is BreakCmd)
+ {
+ firstBigBlock.ec = VisitBreakCmd(bb.ec as BreakCmd);
+ }
+ else if (bb.ec != null)
+ {
+ throw new InvalidOperationException();
+ }
+
+ return new List<BigBlock>(new BigBlock[] { firstBigBlock });
+
+ }
+
+ public virtual IfCmd VisitIfCmd(IfCmd ifCmd)
+ {
+ if(ifCmd.elseIf != null)
+ {
+ throw new InvalidOperationException();
+ }
+
+ return new IfCmd(ifCmd.tok, VisitIfGuard(ifCmd.Guard), VisitStmtList(ifCmd.thn), ifCmd.elseIf,
+ (ifCmd.elseBlock == null ? ifCmd.elseBlock : VisitStmtList(ifCmd.elseBlock)));
+
+ throw new NotImplementedException();
+ }
+
+ public virtual Expr VisitIfGuard(Expr expr)
+ {
+ return expr;
+ }
+
+ public virtual WhileCmd VisitWhileCmd(WhileCmd whileCmd)
+ {
+ return new WhileCmd(whileCmd.tok, VisitWhileGuard(whileCmd.Guard), VisitWhileInvariants(whileCmd.Invariants), VisitStmtList(whileCmd.Body));
+ }
+
+ public virtual BreakCmd VisitBreakCmd(BreakCmd breakCmd)
+ {
+ return breakCmd;
+ }
+
+
+ public virtual List<PredicateCmd> VisitWhileInvariants(List<PredicateCmd> invariants)
+ {
+ return invariants;
+ }
+
+ public virtual Expr VisitWhileGuard(Expr expr)
+ {
+ return expr;
+ }
+
+ public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq)
+ {
+ CmdSeq result = new CmdSeq();
+ foreach (Cmd c in cmdSeq)
+ {
+ result.AddRange(VisitCmd(c));
+ }
+ return result;
+ }
+
+ public virtual CmdSeq VisitCmd(Cmd c)
+ {
+ if (c is CallCmd)
+ {
+ return VisitCallCmd(c as CallCmd);
+ }
+ if (c is AssignCmd)
+ {
+ return VisitAssignCmd(c as AssignCmd);
+ }
+ if (c is HavocCmd)
+ {
+ return VisitHavocCmd(c as HavocCmd);
+ }
+ if (c is AssertCmd)
+ {
+ return VisitAssertCmd(c as AssertCmd);
+ }
+ if (c is AssumeCmd)
+ {
+ return VisitAssumeCmd(c as AssumeCmd);
+ }
+ throw new InvalidOperationException();
+ }
+
+ public virtual CmdSeq VisitAssumeCmd(AssumeCmd assumeCmd)
+ {
+ return new CmdSeq(new Cmd[] { assumeCmd });
+ }
+
+ public virtual CmdSeq VisitAssertCmd(AssertCmd assertCmd)
+ {
+ return new CmdSeq(new Cmd[] { assertCmd });
+ }
+
+ public virtual CmdSeq VisitHavocCmd(HavocCmd havocCmd)
+ {
+ return new CmdSeq(new Cmd[] { havocCmd });
+ }
+
+ public virtual CmdSeq VisitAssignCmd(AssignCmd assignCmd)
+ {
+ return new CmdSeq(new Cmd[] { assignCmd });
+ }
+
+ public virtual CmdSeq VisitCallCmd(CallCmd callCmd)
+ {
+ return new CmdSeq(new Cmd[] { callCmd });
+ }
+
+ }
+}
|