From dcb4ec1c6a6eb4a493e1547e4e7d392afdf9a7d4 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 20 Aug 2024 13:43:39 -0400
Subject: [PATCH] x86-cli: Test suite

---
 macaw-x86-cli/macaw-x86-cli.cabal        |  5 ++-
 macaw-x86-cli/test-data/byte-id.cbl      | 10 +++++
 macaw-x86-cli/test-data/byte-id.out.good |  4 ++
 macaw-x86-cli/test/Test.hs               | 49 +++++++++++++++++++++++-
 4 files changed, 65 insertions(+), 3 deletions(-)
 create mode 100644 macaw-x86-cli/test-data/byte-id.cbl
 create mode 100644 macaw-x86-cli/test-data/byte-id.out.good

diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal
index 900f53d1..6fc9c975 100644
--- a/macaw-x86-cli/macaw-x86-cli.cabal
+++ b/macaw-x86-cli/macaw-x86-cli.cabal
@@ -120,18 +120,19 @@ test-suite macaw-x86-syntax-tests
     base,
     containers,
     crucible >= 0.1,
-    crucible-syntax,
-    crucible-llvm-syntax,
+    crucible-cli,
     filepath,
     macaw-symbolic,
     macaw-symbolic-syntax,
     macaw-x86,
+    macaw-x86-cli,
     macaw-x86-symbolic,
     macaw-x86-syntax,
     parameterized-utils >= 0.1.7,
     tasty,
     tasty-golden,
     text,
+    what4,
 
 executable macaw-x86
   import: shared
diff --git a/macaw-x86-cli/test-data/byte-id.cbl b/macaw-x86-cli/test-data/byte-id.cbl
new file mode 100644
index 00000000..24d3d81a
--- /dev/null
+++ b/macaw-x86-cli/test-data/byte-id.cbl
@@ -0,0 +1,10 @@
+(defun @byte_id ((x (Bitvector 8))) (Bitvector 8)
+  (start start:
+    (return x)))
+
+(defun @main () Unit
+  (start start:
+    (let input (fresh (Bitvector 8)))
+    (let input_back (funcall @byte_id input))
+    (assert! (equal? input input_back) "byte_id test")
+    (return ())))
\ No newline at end of file
diff --git a/macaw-x86-cli/test-data/byte-id.out.good b/macaw-x86-cli/test-data/byte-id.out.good
new file mode 100644
index 00000000..a0dc0d91
--- /dev/null
+++ b/macaw-x86-cli/test-data/byte-id.out.good
@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====
diff --git a/macaw-x86-cli/test/Test.hs b/macaw-x86-cli/test/Test.hs
index a31c5a02..323604a4 100644
--- a/macaw-x86-cli/test/Test.hs
+++ b/macaw-x86-cli/test/Test.hs
@@ -1,4 +1,51 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+
 module Main (main) where
 
+import Data.List (sort)
+import Data.Text.IO qualified as T
+import System.FilePath
+import System.IO
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+
+import What4.Solver.Z3 (z3Options)
+
+import Lang.Crucible.CLI (simulateProgramWithExtension)
+
+import Data.Macaw.X86.Symbolic.CLI (withX86Hooks)
+
 main :: IO ()
-main = pure ()
+main = do
+  simTests <- findTests "x86 simulation" "test-data" testSimulator
+  defaultMain simTests
+
+findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
+findTests groupName testDir testAction =
+  do inputs <- findByExtension [".cbl"] testDir
+     return $ testGroup groupName
+       [ goldenFileTestCase input testAction
+       | input <- sort inputs
+       ]
+
+goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree
+goldenFileTestCase input testAction =
+  goldenVsFileDiff
+   (takeBaseName input) -- test name
+   (\x y -> ["diff", "-u", x, y])
+   goodFile -- golden file path
+   outFile
+   (testAction input outFile) -- action whose result is tested
+  where
+    outFile = replaceExtension input ".out"
+    goodFile = replaceExtension input ".out.good"
+
+testSimulator :: FilePath -> FilePath -> IO ()
+testSimulator inFile outFile =
+  do contents <- T.readFile inFile
+     withFile outFile WriteMode $ \outh ->
+       withX86Hooks $ \ext hooks ->
+         simulateProgramWithExtension ext inFile contents outh Nothing z3Options hooks