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