From 6029a149a7cbc012121430cfd50ef433f130da09 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Tue, 29 May 2012 17:03:51 +0100
Subject: GPUVerify: factor the race instrumenter to handle unstructured blocks

---
 Source/GPUVerify/RaceInstrumenterBase.cs | 39 ++++++++++++++++++++------------
 1 file changed, 24 insertions(+), 15 deletions(-)

(limited to 'Source/GPUVerify')

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 7ae7ca44..11feb017 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -798,9 +798,17 @@ namespace GPUVerify
             return result;
         }
 
+        private Block AddRaceCheckCalls(Block b)
+        {
+            return new Block(Token.NoToken, b.Label, AddRaceCheckCalls(b.Cmds), b.TransferCmd);
+        }
+
         private void AddRaceCheckCalls(Implementation impl)
         {
-            impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
+            if (CommandLineOptions.Unstructured)
+                impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
+            else
+                impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
         }
 
         private bool shouldAddLogCallAndIncr()
@@ -828,13 +836,12 @@ namespace GPUVerify
             return false;
         }
 
-        private BigBlock AddRaceCheckCalls(BigBlock bb)
+        private CmdSeq AddRaceCheckCalls(CmdSeq cs)
         {
-            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
-            foreach (Cmd c in bb.simpleCmds)
+            var result = new CmdSeq();
+            foreach (Cmd c in cs)
             {
-                result.simpleCmds.Add(c);
+                result.Add(c);
                 if (c is AssignCmd)
                 {
                     AssignCmd assign = c as AssignCmd;
@@ -873,8 +880,8 @@ namespace GPUVerify
 
                             logAccessCallCmd.Proc = logProcedure;
 
-                            result.simpleCmds.Add(logAccessCallCmd);
-                            
+                            cs.Add(logAccessCallCmd);
+
                         }
                     }
 
@@ -907,17 +914,20 @@ namespace GPUVerify
 
                             logAccessCallCmd.Proc = logProcedure;
 
-                            result.simpleCmds.Add(logAccessCallCmd);
-                            
+                            cs.Add(logAccessCallCmd);
+
                             addedLogWrite = true;
-                            
+
                         }
                     }
-
-
-
                 }
             }
+            return result;
+        }
+
+        private BigBlock AddRaceCheckCalls(BigBlock bb)
+        {
+            BigBlock result = new BigBlock(bb.tok, bb.LabelName, AddRaceCheckCalls(bb.simpleCmds), null, bb.tc);
 
             if (bb.ec is WhileCmd)
             {
@@ -941,7 +951,6 @@ namespace GPUVerify
             }
 
             return result;
-
         }
 
         private Procedure GetLogAccessProcedure(IToken tok, string name)
-- 
cgit v1.2.3