connect everything together so that litmus tests can be compiled and …

…run in one go

package.yaml

@@ -63,6 +63,7 @@ executables:
       - Utility.ListMemory
       - Utility.MapMemory
       - Utility.Utility
+      - Utility.LitmusToRiscv
 
 
   riscv-semantics:
@@ -205,6 +206,3 @@ executables:
       - Utility.ListMemory
       - Utility.MapMemory
       - Utility.Utility
-
-  litmus-to-riscv:
-    main:             src/Utility/LitmusToRiscv.hs

src/Platform/MemoryModelTracking.hs

@@ -29,6 +29,7 @@ import System.Process
 
 import Spec.ExecuteI as I
 import Utility.Elf
+import Utility.LitmusToRiscv as LTR
 import Debug.Trace as T
 import Numeric (showHex)
 
@@ -291,8 +292,6 @@ updateDepsI inst d =
 
 type IORead= ReaderT Ptrs IO
 
-data Condition = RegCond (Int64, Register, Int64) | MemCond (Int, Word8) deriving Show
-
 data Ptrs = Ptrs {
   r_threads :: IORef Minimal64,
   r_currentExecution :: IORef Execution,
@@ -697,16 +696,9 @@ readLitmusProgram f = do
     mem <- readElf f
 --    T.trace (show $ mem) $ return()
     threads <- getThreads f 0
-    T.trace (show threads) $ return ()
+--    T.trace (show threads) $ return ()
     return (mem, threads)
 
-readLitmusPost :: String -> IO [Condition]
-readLitmusPost postfile = do
-  T.trace "HARDCODED POSTCONDITION TODO FIX" $ return ()
-  -- return [RegCond (0, 5, 0), RegCond (1, 5, 0)]
-  -- return [MemCond (0x100d8, 2), MemCond (0x100dc, 2)]
-  return [RegCond (0, 9, 2), RegCond (0, 10, 2), RegCond (1, 9, 2), RegCond (1, 10, 2)]
-
 runFile :: String -> [(Int64, Int64)] -> ReaderT Ptrs IO [Execution]
 runFile f threads = do
   (_maybeToHostAddress, program) <- lift $ readProgram f
@@ -727,10 +719,11 @@ runFile f threads = do
   runTime c threads
   where initList = [(i,Set.empty) | i <- [0..31]]:: [(Register,Events)]
 
-runLitmusFile :: String -> String -> ReaderT Ptrs IO [Execution]
-runLitmusFile asmfile postfile = do
-  (program, threads) <- lift $ readLitmusProgram asmfile
-  postcond <- lift $ readLitmusPost postfile
+runLitmusFile :: String -> ReaderT Ptrs IO [Execution]
+runLitmusFile litmusFile = do
+  (asmFile, postcond) <- lift $ litmusToRiscv litmusFile
+  (program, threads) <- lift $ readLitmusProgram asmFile 
+--  T.trace (show postcond) $ return ()
 --  T.trace (show $ program) $ return()
   let mem = S.fromList program
   let c = Minimal64 { registers = S.empty,
@@ -750,33 +743,36 @@ runLitmusFile asmfile postfile = do
   where initList = [(i,Set.empty) | i <- [0..31]]:: [(Register,Events)]
 
 checkLitmusPosts :: [(Int64, Minimal64)] -> MapMemory Int -> [Condition] -> IO Bool
-checkLitmusPosts endStates endMem (RegCond (tid, reg, val) : tl) = do
-  case L.find (\(t,_) -> t == tid) endStates of
-    Just (_, endState) -> do
-      case S.lookup reg (registers endState) of
-        Just regVal -> 
-          if regVal == val then
-            checkLitmusPosts endStates endMem tl
-          else do
-            putStrLn "\n\"exists\" postconditions pass\n"
-            return True
-        Nothing -> do
-          putStrLn $ "condition supplied for register " ++ show reg ++ " which was not set"
-          checkLitmusPosts endStates endMem tl
-    Nothing -> do
-      putStrLn $ "condition supplied for tid " ++ show tid ++ " which does not exist"
-      checkLitmusPosts endStates endMem tl
-checkLitmusPosts endStates endMem (MemCond (addr, val) : tl) = do
-  let memVal = M.loadByte endMem addr
-  T.trace ("\t\t\t addr = " ++ showHex addr "" ++ " val = " ++ show memVal) $ return ()
-  if memVal == val then
-    checkLitmusPosts endStates endMem tl
-  else do
-    putStrLn "\n\"exists\" postconditions pass\n"
-    return True  
-checkLitmusPosts endStates endMem [] = do
-  putStrLn "\n\n\nFAILURE: all \"exists\" postconditions were met, indicating failure\n\n\n"
-  return False
+checkLitmusPosts endStates endMem [] = return True -- empty condition always holds
+checkLitmusPosts endStates endMem conds = helper endStates endMem conds where
+  helper :: [(Int64, Minimal64)] -> MapMemory Int -> [Condition] -> IO Bool
+  helper endStates endMem (RegCond (tid, reg, val) : tl) = do
+    case L.find (\(t,_) -> t == tid) endStates of
+      Just (_, endState) -> do
+        case S.lookup reg (registers endState) of
+          Just regVal -> 
+            if regVal == val then
+              helper endStates endMem tl
+            else do
+              putStrLn "\n\"exists\" postconditions pass\n"
+              return True
+          Nothing -> do
+            putStrLn $ "condition supplied for register " ++ show reg ++ " which was not set"
+            helper endStates endMem tl
+      Nothing -> do
+        putStrLn $ "condition supplied for tid " ++ show tid ++ " which does not exist"
+        helper endStates endMem tl
+{-   helper endStates endMem (MemCond (addr, val) : tl) = do
+    let memVal = M.loadByte endMem addr
+    T.trace ("\t\t\t addr = " ++ showHex addr "" ++ " val = " ++ show memVal) $ return ()
+    if memVal == val then
+      helper endStates endMem tl
+    else do
+      putStrLn "\n\"exists\" postconditions pass\n"
+      return True   -}
+  helper endStates endMem [] = do
+    putStrLn "\nCase found where all \"exists\" postconditions were met, could indicate a bug or an interesting execution\n"
+    return False
 
 runTime :: Minimal64 -> [(Int64, Int64)] -> ReaderT Ptrs IO [Execution]
 runTime init threads = do
@@ -802,9 +798,9 @@ runTime init threads = do
         endMem <- lift $ readIORef (r_mem refs)
         condsOk <- lift $ checkLitmusPosts endStates endMem postExists
         unless condsOk $ do
-          lift $ print postExists
+{-        lift $ print postExists
           lift $ print endStates
-          lift $ print endMem
+          lift $ print endMem -}
           lift $ T.putStrLn alloyFile
           return ()
         nextRound
@@ -872,10 +868,10 @@ sbDataRev = Platform.MemoryModelTracking.runFile
  $ L.reverse [(0x10078,0x10098),(0x1009c,0x100b4)]
 
 sbLitmus = Platform.MemoryModelTracking.runLitmusFile
- "./test/litmus/SB.litmus.exe" "./test/litmus/SB.litmus.post"
+ "./test/litmus/SB.litmus"
 
 litmus22W = Platform.MemoryModelTracking.runLitmusFile
- "./test/litmus/2+2W.litmus.exe" "./test/litmus/2+2W.litmus.post"
+ "./test/litmus/2+2W.litmus"
 
 
 emptyEx = Execution {

src/Platform/RunMM.hs

@@ -85,10 +85,19 @@ import Numeric (showHex, readHex)
 --
 main :: IO ()
 main = do
-  putStrLn "\n\n\nSB.litmus.exe:\n"
-  readerRead sbLitmus
-  putStrLn "\n\n\n2+2W.litmus.exe:\n"
-  readerRead litmus22W
+  args <- getArgs
+  retval <- case args of
+    [filename] -> do 
+      putStrLn $ "\n\n\n" ++ filename ++ "\n\n"
+      readerRead $ runLitmusFile filename
+      return 0
+    _ -> do
+      putStr "ERROR: this program expects exactly one litmus file as command-line argument\n"
+      return 1
+  exitWith (if retval == 0 then ExitSuccess else ExitFailure $ (fromIntegral:: Int64 -> Int) retval)
+
+  -- putStrLn "\n\n\n2+2W.litmus.exe:\n"
+  -- readerRead litmus22W
   -- putStrLn "\n\n\n\n\n\n\n\n\nmp"
   -- readerRead mp 
   {- putStrLn "\n\n\n\n\n\n\n\n\nmpRev"
@@ -99,7 +108,6 @@ main = do
   readerRead sbData 
   putStrLn "\n\n\n\n\n\n\n\n\nsbDataRev"
   readerRead sbDataRev -}
-  return ()
   --  do
   --args <- getArgs
   --retval <- case args of

src/Utility/LitmusToRiscv.hs

@@ -1,6 +1,6 @@
+module Utility.LitmusToRiscv where
 import System.IO
 import Text.ParserCombinators.Parsec
-import System.Environment
 import System.Process
 import qualified Data.Set as Set
 import Debug.Trace as T
@@ -19,7 +19,8 @@ instance Show LitmusInit where
 newtype LitmusThread = LThread String -- just the list of instructions separated by \n
 instance Show LitmusThread where
   show (LThread s) = "LT " ++ show s
-data SymCondition = RegCond (Int64, Register, Int64) | MemCond (String, Word8) deriving Show
+data SymCondition = SRegCond (Int64, Register, Int64) | SMemCond (String, Word8) deriving Show
+newtype Condition = RegCond (Int64, Register, Int64) deriving Show
 newtype LitmusFile = LFile ([LitmusInit], (LitmusThread, LitmusThread), [SymCondition])
 instance Show LitmusFile where
   show (LFile (inits, (t0, t1), conds)) = "L (" ++ show inits ++ ", (" ++ show t0 ++ ", " ++ show t1++ ")," ++ show conds ++ ")"
@@ -67,21 +68,21 @@ parseThreads = do
 
 parseCond :: Parser SymCondition
 parseCond = do
-  parseRegCond <|> parseMemCond
+  parseSRegCond <|> parseSMemCond
   where
-    parseRegCond = do
+    parseSRegCond = do
       thread <- read <$> many1 digit
       char ':'
       char 'x'
       regNum <- read <$> many1 digit
       char '='
       regVal <- read <$> many1 digit
-      return $ RegCond (thread, regNum, regVal)
-    parseMemCond = do
+      return $ SRegCond (thread, regNum, regVal)
+    parseSMemCond = do
       ptrName <- many1 lower
       char '='
       regVal <- read <$> many1 digit
-      return $ MemCond (ptrName, regVal)
+      return $ SMemCond (ptrName, regVal)
 
 parseConds :: Parser [SymCondition]
 parseConds = do
@@ -139,8 +140,8 @@ preamble = "\
   \  .globl _endTh1\n\
   \"
 
-compileMemConds :: [SymCondition] -> (String, String, [SymCondition])
-compileMemConds conds = 
+compileSMemConds :: [SymCondition] -> (String, String, [Condition])
+compileSMemConds conds = 
   -- This function uses registers x18 and up to read values in memory locations
   -- For the basic 2-thread tests, only registers x5-x10 are used, so no conflicts occur
   -- More complex litmus tests may require a more sophisticated register choice strategy
@@ -149,18 +150,18 @@ compileMemConds conds =
      if t1checks == "" then "" else "  fence\n" ++ t1checks,
      newConds)
   where
-    helper (RegCond r) (t0acc, t1acc, condacc, n) = (t0acc, t1acc, RegCond r : condacc, n)
-    helper (MemCond (ptr, val)) (t0acc, t1acc, condacc, n) = 
+    helper (SRegCond r) (t0acc, t1acc, condacc, n) = (t0acc, t1acc, RegCond r : condacc, n)
+    helper (SMemCond (ptr, val)) (t0acc, t1acc, condacc, n) = 
       (t0acc ++ "  lw x" ++ show n ++ "," ++ ptr ++ "\n",
        t0acc ++ "  lw x" ++ show n ++ "," ++ ptr ++ "\n",
        RegCond (0, n, fromIntegral val) : RegCond (1, n, fromIntegral val) : condacc,
        n + 1
       )
 
-compileLitmusFile :: LitmusFile -> ([SymCondition], String)
+compileLitmusFile :: LitmusFile -> ([Condition], String)
 compileLitmusFile (LFile (inits, (LThread t0, LThread t1), conds)) =
   let (t0inits, t1inits, symptrs) = compileInits inits in
-  let (t0memChecks, t1memChecks, newConds) = compileMemConds conds in
+  let (t0memChecks, t1memChecks, newConds) = compileSMemConds conds in
     (newConds, preamble
                 ++ "_start:\n"
                 ++ "_startTh0:\n"
@@ -177,37 +178,39 @@ compileLitmusFile (LFile (inits, (LThread t0, LThread t1), conds)) =
                 ++ symptrs
     )
 
-litmusToRiscv :: IO [SymCondition]
-litmusToRiscv = do
+litmusToRiscv :: String -> IO (String, [Condition])
+litmusToRiscv filename = do
   -- TODO fix hardcoding of filename
-  args <- getArgs
-  let filename = head args
   litmusFile <- openFile filename ReadMode
   litmusStr <- hGetContents litmusFile
   --putStrLn litmusStr
-  putStrLn filename
+  --putStrLn filename
   case parse parseLitmusFile "blah" litmusStr of
     Left _ -> do
       putStrLn "Parse error"
       hClose litmusFile
-      return []
+      return ("", [])
     Right lfile -> do
-      print lfile
+      -- print lfile
       let (newConds, asmStr) = compileLitmusFile lfile
       putStrLn asmStr
-      print newConds
+      -- print newConds
       writeFile (filename ++ ".S") asmStr
       let callGccO = proc "riscv-none-embed-gcc" ["-march=rv64im", "-mabi=lp64", "-static", "-nostdlib", "-nostartfiles", "-mcmodel=medany", "-c", filename ++ ".S", "-o", filename ++ ".o"]
       let callGccExe = proc "riscv-none-embed-gcc" ["-march=rv64im", "-mabi=lp64", "-static", "-nostdlib", "-nostartfiles", "-mcmodel=medany", "-o", filename ++ ".exe", filename ++ ".o"]
       (exitCodeO, stdoutO, stderrO) <- readCreateProcessWithExitCode callGccO "stdin"
-      putStrLn $ "first gcc call returned:\n" ++ show exitCodeO ++ "\n stdOut: " ++ stdoutO ++ "\n stderr:" ++ stderrO
+      -- putStrLn $ "first gcc call returned:\n" ++ show exitCodeO ++ "\n stdOut: " ++ stdoutO ++ "\n stderr:" ++ stderrO
       (exitCodeExe, stdoutExe, stderrExe) <- readCreateProcessWithExitCode callGccExe "stdin"
-      putStrLn $ "second gcc call returned:\n" ++ show exitCodeExe ++ "\n stdOut: " ++ stdoutExe ++ "\n stderr:" ++ stderrExe
+      -- putStrLn $ "second gcc call returned:\n" ++ show exitCodeExe ++ "\n stdOut: " ++ stdoutExe ++ "\n stderr:" ++ stderrExe
       hClose litmusFile
-      return newConds
+      return (filename ++ ".exe", newConds)
 
-main :: IO ()
-main = litmusToRiscv >> return ()
+{- main :: IO ()
+main = do
+  args <- getArgs
+  let filename = head args
+  litmusToRiscv filename 
+  return () -}
 
 -- TODOS:
 -- - parse postconditions