Add a testing framework for macaw-symbolic (#184)

The new test suites cover x86_64, PowerPC, and ARM. They test that the semantics are actually correct (rather than just seeing if symbolic execution produces any result). The `Data.Macaw.Symbolic.Testing` module in macaw-symbolic provides some common utilities for symbolic execution engine setup, while there are tailored test harnesses for each architecture. The semantics of the test harnesses are documented in each architecture test suite, but they: 1. Discover all of the test binaries (which are generated from the included makefiles) 2. Treat each function whose name begins with `test_` as a test entry point 3. Symbolically executes each test case with fully symbolic register states 4. Extracts the return value after symbolic execution, which is treated as the predicate to an assertion that must be proved - If the test case is in the `pass` subdirectory, it is proved and expected to hold - If the test case is in the `fail` subdirectory, it is proved and expected to not hold. Each test harness supports two options for debugging: - Dumping generated SMT queries - Dumping generated Macaw IR for inspection This testing uncovered a bug in the (previously untested) macaw-aarch32-symbolic code. It required a number of submodule updates to: - Adapt to some what4 changes - Fix a bug in the LLVM memory model that lets these tests pass - Adapt to changes to some crucible APIs This change also modifies the CI configuration to install SMT solvers earlier (which are now needed for all of the symbolic package tests).
2024-11-29 11:02:13 +03:00 · 2021-03-01 09:21:44 -08:00 · 2021-03-01 09:21:44 -08:00 · dbb4c83f08
commit dbb4c83f08
parent a58f1e25dd
55 changed files with 1333 additions and 149 deletions
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@ -1,3 +1,5 @@
+# Note: We build everything on all architectures, but we only test things
+# requiring SMT solvers on Linux
 name: CI
 on:
  push:
@ -42,19 +44,6 @@ jobs:
      run: |
        cabal build --only-dependencies macaw-base
        cabal build crucible-llvm
-    - name: macaw-x86 tests
-      run: |
-        cabal build pkg:macaw-x86 pkg:macaw-x86-symbolic
-        cabal test pkg:macaw-x86
-        cabal test pkg:macaw-x86-symbolic
-    - name: macaw-aarch32 tests
-      run: |
-        cabal build pkg:macaw-aarch32 pkg:macaw-aarch32-symbolic
-        cabal test pkg:macaw-aarch32
-    - name: macaw-ppc tests
-      run: |
-        cabal build pkg:macaw-ppc pkg:macaw-ppc-symbolic
-        cabal test pkg:macaw-ppc

    - name: Install Solvers
      if: runner.os == 'Linux'
@ -64,9 +53,40 @@ jobs:
        YICES_VERSION: "2.6.2"
        CVC4_VERSION: "4.1.8"

-    - name: macaw-refinement
-      run: |
-        cabal build pkg:macaw-refinement
-        cabal test pkg:macaw-refinement
-    - name: compare-dwarfdump
+    - name: Build macaw-x86
+      run: cabal build pkg:macaw-x86 pkg:macaw-x86-symbolic
+
+    - name: Test macaw-x86
+      run: cabal test pkg:macaw-x86
+
+    - name: Test macaw-x86-symbolic
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-x86-symbolic
+
+    - name: Build macaw-aarch32
+      run: cabal build pkg:macaw-aarch32 pkg:macaw-aarch32-symbolic
+    - name: Test macaw-aarch32
+      run: cabal test pkg:macaw-aarch32
+    - name: Test macaw-aarch32-symbolic
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-aarch32-symbolic
+
+    - name: Build macaw-ppc
+      run: cabal build pkg:macaw-ppc pkg:macaw-ppc-symbolic
+
+    - name: Test macaw-ppc
+      run: cabal test pkg:macaw-ppc
+
+    - name: Test macaw-ppc-symbolic
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-ppc-symbolic
+
+    - name: Build macaw-refinement
+      run: cabal build pkg:macaw-refinement
+
+    - name: Test macaw-refinement
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-refinement
+
+    - name: Build compare-dwarfdump
      run: cabal build compare-dwarfdump
--- a/deps/asl-translator
+++ b/deps/asl-translator
@ -1 +1 @@
-Subproject commit 69c4d62429015cedcb9c16a7f2d4f4210e84fd2c
+Subproject commit 8b90076a4381672d6691624e5d628e65da4b22b6
--- a/deps/crucible
+++ b/deps/crucible
@ -1 +1 @@
-Subproject commit e635f160a5c5ec713505e871da24cd9f39b35667
+Subproject commit dc5a5aee7ad9c0592b01e4372d2088cb515dcd70
--- a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal
+++ b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal
@ -40,3 +40,32 @@ library
  hs-source-dirs:      src
  default-language:    Haskell2010
  ghc-options: -Wall -Wcompat
+
+test-suite macaw-aarch32-symbolic-tests
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  ghc-options: -Wall -Wcompat
+  main-is: Main.hs
+  hs-source-dirs: tests
+  build-depends:
+    base >= 4,
+    bytestring,
+    containers,
+    crucible,
+    elf-edit,
+    filepath,
+    Glob >= 0.9 && < 0.11,
+    dismantle-arm-xml,
+    asl-translator,
+    semmc-aarch32,
+    macaw-aarch32,
+    macaw-aarch32-symbolic,
+    macaw-base,
+    macaw-symbolic,
+    parameterized-utils,
+    prettyprinter,
+    tasty,
+    tasty-hunit,
+    text,
+    what4,
+    vector
--- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
+++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
@ -63,7 +63,7 @@ aarch32MacawSymbolicFns =
  }

 aarch32RegName :: MAR.ARMReg tp -> WS.SolverSymbol
-aarch32RegName r = WS.systemSymbol ("r!" ++ show (MC.prettyF r))
+aarch32RegName r = WS.safeSymbol ("r!" ++ show (MC.prettyF r))

 aarch32MacawEvalFn :: (CB.IsSymInterface sym)
                   => AF.SymFuns sym
--- a/macaw-aarch32-symbolic/tests/Main.hs
+++ b/macaw-aarch32-symbolic/tests/Main.hs
@ -0,0 +1,180 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Main (main) where
+
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.ElfEdit as Elf
+import qualified Data.Foldable as F
+import           Data.Maybe ( mapMaybe )
+import qualified Data.Parameterized.Classes as PC
+import qualified Data.Parameterized.Nonce as PN
+import           Data.Parameterized.Some ( Some(..) )
+import           Data.Proxy ( Proxy(..) )
+import qualified Prettyprinter as PP
+import           System.FilePath ( (</>), (<.>) )
+import qualified System.FilePath.Glob as SFG
+import qualified System.IO as IO
+import qualified Test.Tasty as TT
+import qualified Test.Tasty.HUnit as TTH
+import qualified Test.Tasty.Options as TTO
+import qualified Test.Tasty.Runners as TTR
+
+import qualified Language.ASL.Globals as ASL
+import qualified Data.Macaw.Architecture.Info as MAI
+
+import           Data.Macaw.AArch32.Symbolic ()
+import qualified Data.Macaw.ARM as MA
+import qualified Data.Macaw.ARM.ARMReg as MAR
+import qualified Data.Macaw.CFG as MC
+import qualified Data.Macaw.Discovery as M
+import qualified Data.Macaw.Symbolic as MS
+import qualified Data.Macaw.Symbolic.Testing as MST
+import qualified What4.Config as WC
+import qualified What4.Interface as WI
+import qualified What4.ProblemFeatures as WPF
+import qualified What4.Solver as WS
+
+import qualified Lang.Crucible.Backend as CB
+import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.Simulator as CS
+
+-- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
+data SaveSMT = SaveSMT Bool
+  deriving (Eq, Show)
+
+instance TTO.IsOption SaveSMT where
+  defaultValue = SaveSMT False
+  parseValue v = SaveSMT <$> TTO.safeReadBool v
+  optionName = pure "save-smt"
+  optionHelp = pure "Save SMT sessions to files in /tmp for debugging"
+
+-- | A tasty option to have the test suite save the macaw IR for each test case to /tmp for debugging purposes
+data SaveMacaw = SaveMacaw Bool
+
+instance TTO.IsOption SaveMacaw where
+  defaultValue = SaveMacaw False
+  parseValue v = SaveMacaw <$> TTO.safeReadBool v
+  optionName = pure "save-macaw"
+  optionHelp = pure "Save Macaw IR for each test case to /tmp for debugging"
+
+ingredients :: [TTR.Ingredient]
+ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
+                                  , TTO.Option (Proxy @SaveMacaw)
+                                  ] : TT.defaultIngredients
+
+main :: IO ()
+main = do
+  -- These are pass/fail in that the assertions in the "pass" set are true (and
+  -- the solver returns Unsat), while the assertions in the "fail" set are false
+  -- (and the solver returns Sat).
+  passTestFilePaths <- SFG.glob "tests/pass/*.exe"
+  failTestFilePaths <- SFG.glob "tests/fail/*.exe"
+  let passRes = MST.SimulationResult MST.Unsat
+  let failRes = MST.SimulationResult MST.Sat
+  let passTests = TT.testGroup "True assertions" (map (mkSymExTest passRes) passTestFilePaths)
+  let failTests = TT.testGroup "False assertions" (map (mkSymExTest failRes) failTestFilePaths)
+  TT.defaultMainWithIngredients ingredients (TT.testGroup "Binary Tests" [passTests, failTests])
+
+hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
+hasTestPrefix (Some dfi) = do
+  bsname <- M.discoveredFunSymbol dfi
+  if BS8.pack "test_" `BS8.isPrefixOf` bsname
+    then return (bsname, Some dfi)
+    else Nothing
+
+-- | ARM functions with a single scalar return value return it in %r0
+--
+-- Since all test functions must return a value to assert as true, this is
+-- straightforward to extract
+armResultExtractor :: ( CB.IsSymInterface sym
+                      )
+                   => MS.ArchVals MA.ARM
+                   -> MST.ResultExtractor sym MA.ARM
+armResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+  let re = MS.lookupReg archVals regs (MAR.ARMGlobalBV (ASL.knownGlobalRef @"_R0"))
+  k PC.knownRepr (CS.regValue re)
+
+mkSymExTest :: MST.SimulationResult -> FilePath -> TT.TestTree
+mkSymExTest expected exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOption $ \saveMacaw@(SaveMacaw _) -> TTH.testCaseSteps exePath $ \step -> do
+  bytes <- BS.readFile exePath
+  case Elf.decodeElfHeaderInfo bytes of
+    Left (_, msg) -> TTH.assertFailure ("Error parsing ELF header from file '" ++ show exePath ++ "': " ++ msg)
+    Right (Elf.SomeElf ehi) -> do
+      case Elf.headerClass (Elf.header ehi) of
+        Elf.ELFCLASS32 ->
+          symExTestSized expected exePath saveSMT saveMacaw step ehi MA.arm_linux_info
+        Elf.ELFCLASS64 -> TTH.assertFailure "64 bit ARM is not supported"
+
+symExTestSized :: MST.SimulationResult
+               -> FilePath
+               -> SaveSMT
+               -> SaveMacaw
+               -> (String -> IO ())
+               -> Elf.ElfHeaderInfo 32
+               -> MAI.ArchitectureInfo MA.ARM
+               -> TTH.Assertion
+symExTestSized expected exePath saveSMT saveMacaw step ehi archInfo = do
+   (mem, funInfos) <- MST.runDiscovery ehi MST.toAddrSymMap archInfo
+   let testEntryPoints = mapMaybe hasTestPrefix funInfos
+   F.forM_ testEntryPoints $ \(name, Some dfi) -> do
+     step ("Testing " ++ BS8.unpack name ++ " at " ++ show (M.discoveredFunAddr dfi))
+     writeMacawIR saveMacaw (BS8.unpack name) dfi
+     Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator
+     CBO.withYicesOnlineBackend CBO.FloatRealRepr gen CBO.NoUnsatFeatures WPF.noFeatures $ \sym -> do
+       -- We are using the z3 backend to discharge proof obligations, so
+       -- we need to add its options to the backend configuration
+       let solver = WS.z3Adapter
+       let backendConf = WI.getConfiguration sym
+       WC.extendConfig (WS.solver_adapter_config_options solver) backendConf
+
+       execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend sym)
+       let Just archVals = MS.archVals (Proxy @MA.ARM)
+       let extract = armResultExtractor archVals
+       logger <- makeGoalLogger saveSMT solver name exePath
+       simRes <- MST.simulateAndVerify solver logger sym execFeatures archInfo archVals mem extract dfi
+       TTH.assertEqual "AssertionResult" expected simRes
+
+writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()
+writeMacawIR (SaveMacaw sm) name dfi
+  | not sm = return ()
+  | otherwise = writeFile (toSavedMacawPath name) (show (PP.pretty dfi))
+
+toSavedMacawPath :: String -> FilePath
+toSavedMacawPath testName = "/tmp" </> name <.> "macaw"
+  where
+    name = fmap escapeSlash testName
+
+-- | Construct a solver logger that saves the SMT session for the goal solving
+-- in /tmp (if requested by the save-smt option)
+--
+-- The adapter name is included so that, if the same test is solved with
+-- multiple solvers, we can differentiate them.
+makeGoalLogger :: SaveSMT -> WS.SolverAdapter st -> BS8.ByteString -> FilePath -> IO WS.LogData
+makeGoalLogger (SaveSMT saveSMT) adapter funName p
+  | not saveSMT = return WS.defaultLogData
+  | otherwise = do
+      hdl <- IO.openFile (toSavedSMTSessionPath adapter funName p) IO.WriteMode
+      return (WS.defaultLogData { WS.logHandle = Just hdl })
+
+-- | Construct a path in /tmp to save the SMT session to
+--
+-- Just take the original path name and turn all of the slashes into underscores to escape them
+toSavedSMTSessionPath :: WS.SolverAdapter st -> BS8.ByteString -> FilePath -> FilePath
+toSavedSMTSessionPath adapter funName p = "/tmp" </> filename <.> "smtlib2"
+  where
+    filename = concat [ fmap escapeSlash p
+                      , "_"
+                      , BS8.unpack funName
+                      , "_"
+                      , WS.solver_adapter_name adapter
+                      ]
+
+escapeSlash :: Char -> Char
+escapeSlash '/' = '_'
+escapeSlash c = c
--- a/macaw-aarch32-symbolic/tests/README.org
+++ b/macaw-aarch32-symbolic/tests/README.org
@ -0,0 +1,16 @@
+* Overview
+This test suite tests that symbolic execution of AArch32 programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
+
+* Usage
+
+The test runner has two command line options (beyond the defaults for tasty):
+
+- ~--save-macaw~: Saves the Macaw IR for each test case to /tmp for debugging purposes
+- ~--save-smt~: Saves the generated SMTLib for each test to /tmp for debugging purposes
+
+
+* Limitations
+- It currently tests both optimized an unoptimized binaries. It is intended that this set will expand and that a wide variety of compilers will be tested.
+- Only two solvers are involved in the test, rather than a whole matrix
+- Function calls are not supported in test cases
+- There are no facilities for generating symbolic data beyond the initial symbolic arguments to each function
--- a/macaw-aarch32-symbolic/tests/fail/Makefile
+++ b/macaw-aarch32-symbolic/tests/fail/Makefile
@ -0,0 +1,13 @@
+CC=arm-linux-gnueabi-gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt = $(patsubst %.c,%.unopt.exe,$(wildcard *.c))
+opt = $(patsubst %.c,%.opt.exe,$(wildcard *.c))
+
+all: $(unopt) $(opt)
+
+%.unopt.exe : %.c
+	$(CC) $(CFLAGS) -O0 $< -o $@
+
+%.opt.exe : %.c
+	$(CC) $(CFLAGS) -O2 $< -o $@
--- a/macaw-aarch32-symbolic/tests/fail/constant.c
+++ b/macaw-aarch32-symbolic/tests/fail/constant.c
@ -0,0 +1,16 @@
+// This test fails because x is not always 1
+int __attribute__((noinline)) test_constant(int x) {
+  return x == 1;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_constant(0);
+}
--- a/macaw-aarch32-symbolic/tests/fail/constant.opt.exe
+++ b/macaw-aarch32-symbolic/tests/fail/constant.opt.exe
--- a/macaw-aarch32-symbolic/tests/fail/constant.unopt.exe
+++ b/macaw-aarch32-symbolic/tests/fail/constant.unopt.exe
--- a/macaw-aarch32-symbolic/tests/pass/Makefile
+++ b/macaw-aarch32-symbolic/tests/pass/Makefile
@ -0,0 +1,13 @@
+CC=arm-linux-gnueabi-gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt = $(patsubst %.c,%.unopt.exe,$(wildcard *.c))
+opt = $(patsubst %.c,%.opt.exe,$(wildcard *.c))
+
+all: $(unopt) $(opt)
+
+%.unopt.exe : %.c
+	$(CC) $(CFLAGS) -O0 $< -o $@
+
+%.opt.exe : %.c
+	$(CC) $(CFLAGS) -O2 $< -o $@
--- a/macaw-aarch32-symbolic/tests/pass/identity.c
+++ b/macaw-aarch32-symbolic/tests/pass/identity.c
@ -0,0 +1,15 @@
+int __attribute__((noinline)) test_identity(int x) {
+  return x == x;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_identity(0);
+}
--- a/macaw-aarch32-symbolic/tests/pass/identity.opt.exe
+++ b/macaw-aarch32-symbolic/tests/pass/identity.opt.exe
--- a/macaw-aarch32-symbolic/tests/pass/identity.unopt.exe
+++ b/macaw-aarch32-symbolic/tests/pass/identity.unopt.exe
--- a/macaw-aarch32-symbolic/tests/pass/saturate-add.c
+++ b/macaw-aarch32-symbolic/tests/pass/saturate-add.c
@ -0,0 +1,13 @@
+#include <limits.h>
+
+int __attribute__((noinline)) test_saturate_add(int x, int y) {
+  int c = x + y;
+  if(c < x || c < y)
+    c = INT_MAX;
+
+  return c >= x && c >= y;
+}
+
+void _start() {
+  test_saturate_add(1, 2);
+}
--- a/macaw-aarch32-symbolic/tests/pass/saturate-add.opt.exe
+++ b/macaw-aarch32-symbolic/tests/pass/saturate-add.opt.exe
--- a/macaw-aarch32-symbolic/tests/pass/saturate-add.unopt.exe
+++ b/macaw-aarch32-symbolic/tests/pass/saturate-add.unopt.exe
--- a/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal
+++ b/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal
@ -38,4 +38,34 @@ library
                       what4
  hs-source-dirs:      src
  default-language:    Haskell2010
-  ghc-options:         -Wall
+  ghc-options:         -Wall -Wcompat
+
+test-suite macaw-ppc-symbolic-tests
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  ghc-options: -Wall -Wcompat
+  main-is: Main.hs
+  hs-source-dirs: tests
+  build-depends:
+    base >= 4,
+    bytestring,
+    containers,
+    crucible,
+    elf-edit,
+    filepath,
+    Glob >= 0.9 && < 0.11,
+    dismantle-ppc,
+    semmc-ppc,
+    macaw-base,
+    macaw-loader,
+    macaw-symbolic,
+    macaw-ppc,
+    macaw-loader-ppc,
+    macaw-ppc-symbolic,
+    parameterized-utils,
+    prettyprinter,
+    tasty,
+    tasty-hunit,
+    text,
+    what4,
+    vector
--- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
+++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
@ -43,6 +43,7 @@ import           Control.Monad ( void )
 import qualified Control.Monad.Catch as X
 import           Control.Monad.IO.Class ( liftIO )
 import qualified Data.Functor.Identity as I
+import qualified Data.Kind as DK
 import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Some ( Some(..) )
@ -261,7 +262,7 @@ ppcGenTermStmt :: forall v ids s ppc
 ppcGenTermStmt ts _rs =
  void (MSB.evalArchStmt (PPCPrimTerm ts))

-data PPCStmtExtension ppc (f :: C.CrucibleType -> *) (ctp :: C.CrucibleType) where
+data PPCStmtExtension ppc (f :: C.CrucibleType -> DK.Type) (ctp :: C.CrucibleType) where
  -- | Wrappers around the arch-specific functions in PowerPC; these are
  -- interpreted in 'funcSemantics'.
  PPCPrimFn :: MP.PPCPrimFn ppc (A.AtomWrapper f) t
--- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/AtomWrapper.hs
+++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/AtomWrapper.hs
@ -8,11 +8,12 @@ module Data.Macaw.PPC.Symbolic.AtomWrapper (
  liftAtomIn
  ) where

+import qualified Data.Kind as DK
 import qualified Lang.Crucible.Types as C
 import qualified Data.Macaw.Types as MT
 import qualified Data.Macaw.Symbolic as MS

-newtype AtomWrapper (f :: C.CrucibleType -> *) (tp :: MT.Type)
+newtype AtomWrapper (f :: C.CrucibleType -> DK.Type) (tp :: MT.Type)
  = AtomWrapper (f (MS.ToCrucibleType tp))

 liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
--- a/macaw-ppc-symbolic/tests/Main.hs
+++ b/macaw-ppc-symbolic/tests/Main.hs
@ -0,0 +1,225 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Main (main) where
+
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.ElfEdit as Elf
+import qualified Data.Foldable as F
+import qualified Data.Map as Map
+import           Data.Maybe ( mapMaybe )
+import qualified Data.Parameterized.Classes as PC
+import qualified Data.Parameterized.Nonce as PN
+import           Data.Parameterized.Some ( Some(..) )
+import           Data.Proxy ( Proxy(..) )
+import           GHC.TypeNats ( KnownNat, type (<=) )
+import qualified Prettyprinter as PP
+import           System.FilePath ( (</>), (<.>) )
+import qualified System.FilePath.Glob as SFG
+import qualified System.IO as IO
+import qualified Test.Tasty as TT
+import qualified Test.Tasty.HUnit as TTH
+import qualified Test.Tasty.Options as TTO
+import qualified Test.Tasty.Runners as TTR
+
+import qualified Dismantle.PPC as DP
+import qualified Data.Macaw.Architecture.Info as MAI
+import qualified Data.Macaw.BinaryLoader as MBL
+import qualified Data.Macaw.BinaryLoader.PPC as MBLP
+import qualified Data.Macaw.BinaryLoader.PPC.TOC as MBLP
+import qualified Data.Macaw.CFG as MC
+import qualified Data.Macaw.Discovery as M
+import qualified Data.Macaw.Memory as MM
+import qualified Data.Macaw.Memory.ElfLoader as MMEL
+import qualified Data.Macaw.Symbolic as MS
+import qualified Data.Macaw.Symbolic.Testing as MST
+import qualified Data.Macaw.PPC as MP
+import           Data.Macaw.PPC.Symbolic ()
+import qualified SemMC.Architecture.PPC as SAP
+import qualified What4.Config as WC
+import qualified What4.Interface as WI
+import qualified What4.ProblemFeatures as WPF
+import qualified What4.Solver as WS
+
+import qualified Lang.Crucible.Backend as CB
+import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.Simulator as CS
+
+-- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
+data SaveSMT = SaveSMT Bool
+  deriving (Eq, Show)
+
+instance TTO.IsOption SaveSMT where
+  defaultValue = SaveSMT False
+  parseValue v = SaveSMT <$> TTO.safeReadBool v
+  optionName = pure "save-smt"
+  optionHelp = pure "Save SMT sessions to files in /tmp for debugging"
+
+-- | A tasty option to have the test suite save the macaw IR for each test case to /tmp for debugging purposes
+data SaveMacaw = SaveMacaw Bool
+
+instance TTO.IsOption SaveMacaw where
+  defaultValue = SaveMacaw False
+  parseValue v = SaveMacaw <$> TTO.safeReadBool v
+  optionName = pure "save-macaw"
+  optionHelp = pure "Save Macaw IR for each test case to /tmp for debugging"
+
+ingredients :: [TTR.Ingredient]
+ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
+                                  , TTO.Option (Proxy @SaveMacaw)
+                                  ] : TT.defaultIngredients
+
+main :: IO ()
+main = do
+  -- These are pass/fail in that the assertions in the "pass" set are true (and
+  -- the solver returns Unsat), while the assertions in the "fail" set are false
+  -- (and the solver returns Sat).
+  passTestFilePaths <- SFG.glob "tests/pass/*.exe"
+  failTestFilePaths <- SFG.glob "tests/fail/*.exe"
+  let passRes = MST.SimulationResult MST.Unsat
+  let failRes = MST.SimulationResult MST.Sat
+  let passTests = TT.testGroup "True assertions" (map (mkSymExTest passRes) passTestFilePaths)
+  let failTests = TT.testGroup "False assertions" (map (mkSymExTest failRes) failTestFilePaths)
+  TT.defaultMainWithIngredients ingredients (TT.testGroup "Binary Tests" [passTests, failTests])
+
+hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
+hasTestPrefix (Some dfi) = do
+  bsname <- M.discoveredFunSymbol dfi
+  if BS8.pack "test_" `BS8.isPrefixOf` bsname
+    then return (bsname, Some dfi)
+    else Nothing
+
+-- | PowerPC functions (at least in the common ABIs) with a single scalar return value return it in %r3
+--
+-- Since all test functions must return a value to assert as true, this is
+-- straightforward to extract
+ppcResultExtractor :: ( arch ~ MP.AnyPPC v
+                      , CB.IsSymInterface sym
+                      , MP.KnownVariant v
+                      , MM.MemWidth (SAP.AddrWidth v)
+                      , MC.ArchConstraints arch
+                      , MS.ArchInfo arch
+                      , KnownNat (SAP.AddrWidth v)
+                      )
+                   => MS.ArchVals arch
+                   -> MST.ResultExtractor sym arch
+ppcResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+  let re = MS.lookupReg archVals regs (MP.PPC_GP (DP.GPR 3))
+  k PC.knownRepr (CS.regValue re)
+
+-- | This helper is required because the mapping that comes back from the macaw
+-- ELF loader doesn't account for the TOC in PowerPC64.
+toPPCAddrNameMap :: ( w ~ SAP.AddrWidth v
+                    , MBLP.HasTOC (MP.AnyPPC v) (Elf.ElfHeaderInfo w)
+                    )
+                 => MBL.LoadedBinary (MP.AnyPPC v) (Elf.ElfHeaderInfo w)
+                 -> MM.Memory w
+                 -> [MMEL.MemSymbol w]
+                 -> Map.Map (MM.MemSegmentOff w) BS8.ByteString
+toPPCAddrNameMap loadedBinary mem elfSyms =
+  Map.fromList [ (realSegOff, name)
+               | (addr, name) <- Map.toList (MST.toAddrSymMap mem elfSyms)
+               , Just realAddr <- return (MBLP.mapTOCEntryAddress toc (MM.segoffAddr addr))
+               , Just realSegOff <- return (MM.asSegmentOff mem realAddr)
+               ]
+  where
+    toc = MBLP.getTOC loadedBinary
+
+mkSymExTest :: MST.SimulationResult -> FilePath -> TT.TestTree
+mkSymExTest expected exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOption $ \saveMacaw@(SaveMacaw _) -> TTH.testCaseSteps exePath $ \step -> do
+  bytes <- BS.readFile exePath
+  case Elf.decodeElfHeaderInfo bytes of
+    Left (_, msg) -> TTH.assertFailure ("Error parsing ELF header from file '" ++ show exePath ++ "': " ++ msg)
+    Right (Elf.SomeElf ehi) -> do
+      case Elf.headerClass (Elf.header ehi) of
+        Elf.ELFCLASS32 -> TTH.assertFailure "PPC32 is not supported yet due to ABI differences"
+        Elf.ELFCLASS64 -> do
+          loadedBinary <- MBL.loadBinary MMEL.defaultLoadOptions ehi
+          symExTestSized expected exePath saveSMT saveMacaw step ehi loadedBinary (MP.ppc64_linux_info loadedBinary)
+
+symExTestSized :: forall v w arch
+                . ( w ~ SAP.AddrWidth v
+                  , 16 <= w
+                  , 1 <= w
+                  , SAP.KnownVariant v
+                  , MM.MemWidth w
+                  , MC.ArchConstraints arch
+                  , arch ~ MP.AnyPPC v
+                  , KnownNat w
+                  , MS.ArchInfo arch
+                  , MBLP.HasTOC (MP.AnyPPC v) (Elf.ElfHeaderInfo w)
+                  )
+                => MST.SimulationResult
+               -> FilePath
+               -> SaveSMT
+               -> SaveMacaw
+               -> (String -> IO ())
+               -> Elf.ElfHeaderInfo w
+               -> MBL.LoadedBinary arch (Elf.ElfHeaderInfo w)
+               -> MAI.ArchitectureInfo arch
+               -> TTH.Assertion
+symExTestSized expected exePath saveSMT saveMacaw step ehi loadedBinary archInfo = do
+   (mem, funInfos) <- MST.runDiscovery ehi (toPPCAddrNameMap loadedBinary) archInfo
+   let testEntryPoints = mapMaybe hasTestPrefix funInfos
+   F.forM_ testEntryPoints $ \(name, Some dfi) -> do
+     step ("Testing " ++ BS8.unpack name ++ " at " ++ show (M.discoveredFunAddr dfi))
+     writeMacawIR saveMacaw (BS8.unpack name) dfi
+     Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator
+     CBO.withYicesOnlineBackend CBO.FloatRealRepr gen CBO.NoUnsatFeatures WPF.noFeatures $ \sym -> do
+       -- We are using the z3 backend to discharge proof obligations, so
+       -- we need to add its options to the backend configuration
+       let solver = WS.z3Adapter
+       let backendConf = WI.getConfiguration sym
+       WC.extendConfig (WS.solver_adapter_config_options solver) backendConf
+
+       execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend sym)
+       let Just archVals = MS.archVals (Proxy @(MP.AnyPPC v))
+       let extract = ppcResultExtractor archVals
+       logger <- makeGoalLogger saveSMT solver name exePath
+       simRes <- MST.simulateAndVerify solver logger sym execFeatures archInfo archVals mem extract dfi
+       TTH.assertEqual "AssertionResult" expected simRes
+
+writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()
+writeMacawIR (SaveMacaw sm) name dfi
+  | not sm = return ()
+  | otherwise = writeFile (toSavedMacawPath name) (show (PP.pretty dfi))
+
+toSavedMacawPath :: String -> FilePath
+toSavedMacawPath testName = "/tmp" </> name <.> "macaw"
+  where
+    name = fmap escapeSlash testName
+
+-- | Construct a solver logger that saves the SMT session for the goal solving
+-- in /tmp (if requested by the save-smt option)
+--
+-- The adapter name is included so that, if the same test is solved with
+-- multiple solvers, we can differentiate them.
+makeGoalLogger :: SaveSMT -> WS.SolverAdapter st -> BS8.ByteString -> FilePath -> IO WS.LogData
+makeGoalLogger (SaveSMT saveSMT) adapter funName p
+  | not saveSMT = return WS.defaultLogData
+  | otherwise = do
+      hdl <- IO.openFile (toSavedSMTSessionPath adapter funName p) IO.WriteMode
+      return (WS.defaultLogData { WS.logHandle = Just hdl })
+
+
+-- | Construct a path in /tmp to save the SMT session to
+--
+-- Just take the original path name and turn all of the slashes into underscores to escape them
+toSavedSMTSessionPath :: WS.SolverAdapter st -> BS8.ByteString -> FilePath -> FilePath
+toSavedSMTSessionPath adapter funName p = "/tmp" </> filename <.> "smtlib2"
+  where
+    filename = concat [ fmap escapeSlash p
+                      , "_"
+                      , BS8.unpack funName
+                      , "_"
+                      , WS.solver_adapter_name adapter
+                      ]
+
+escapeSlash :: Char -> Char
+escapeSlash '/' = '_'
+escapeSlash c = c
--- a/macaw-ppc-symbolic/tests/README.org
+++ b/macaw-ppc-symbolic/tests/README.org
@ -0,0 +1,16 @@
+* Overview
+This test suite tests that symbolic execution of PowerPC programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
+
+* Usage
+
+The test runner has two command line options (beyond the defaults for tasty):
+
+- ~--save-macaw~: Saves the Macaw IR for each test case to /tmp for debugging purposes
+- ~--save-smt~: Saves the generated SMTLib for each test to /tmp for debugging purposes
+
+
+* Limitations
+- It currently tests both optimized an unoptimized binaries. It is intended that this set will expand and that a wide variety of compilers will be tested.
+- Only two solvers are involved in the test, rather than a whole matrix
+- Function calls are not supported in test cases
+- There are no facilities for generating symbolic data beyond the initial symbolic arguments to each function
--- a/macaw-ppc-symbolic/tests/fail/Makefile
+++ b/macaw-ppc-symbolic/tests/fail/Makefile
@ -0,0 +1,22 @@
+CC64=powerpc64-linux-gnu-gcc
+CC32=powerpc-linux-gnu-gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt32 = $(patsubst %.c,%.unopt32.exe,$(wildcard *.c))
+unopt64 = $(patsubst %.c,%.unopt64.exe,$(wildcard *.c))
+opt32 = $(patsubst %.c,%.opt32.exe,$(wildcard *.c))
+opt64 = $(patsubst %.c,%.opt64.exe,$(wildcard *.c))
+
+all: $(unopt64) $(opt64)
+
+%.unopt32.exe : %.c
+	$(CC32) $(CFLAGS) -O0 $< -o $@
+
+%.opt32.exe : %.c
+	$(CC32) $(CFLAGS) -O2 $< -o $@
+
+%.unopt64.exe : %.c
+	$(CC64) $(CFLAGS) -O0 $< -o $@
+
+%.opt64.exe : %.c
+	$(CC64) $(CFLAGS) -O2 $< -o $@
--- a/macaw-ppc-symbolic/tests/fail/constant.c
+++ b/macaw-ppc-symbolic/tests/fail/constant.c
@ -0,0 +1,16 @@
+// This test fails because x is not always 1
+int __attribute__((noinline)) test_constant(int x) {
+  return x == 1;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_constant(0);
+}
--- a/macaw-ppc-symbolic/tests/fail/constant.opt64.exe
+++ b/macaw-ppc-symbolic/tests/fail/constant.opt64.exe
--- a/macaw-ppc-symbolic/tests/fail/constant.unopt64.exe
+++ b/macaw-ppc-symbolic/tests/fail/constant.unopt64.exe
--- a/macaw-ppc-symbolic/tests/pass/Makefile
+++ b/macaw-ppc-symbolic/tests/pass/Makefile
@ -0,0 +1,22 @@
+CC64=powerpc64-linux-gnu-gcc
+CC32=powerpc-linux-gnu-gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt32 = $(patsubst %.c,%.unopt32.exe,$(wildcard *.c))
+unopt64 = $(patsubst %.c,%.unopt64.exe,$(wildcard *.c))
+opt32 = $(patsubst %.c,%.opt32.exe,$(wildcard *.c))
+opt64 = $(patsubst %.c,%.opt64.exe,$(wildcard *.c))
+
+all: $(unopt64) $(opt64)
+
+%.unopt32.exe : %.c
+	$(CC32) $(CFLAGS) -O0 $< -o $@
+
+%.opt32.exe : %.c
+	$(CC32) $(CFLAGS) -O2 $< -o $@
+
+%.unopt64.exe : %.c
+	$(CC64) $(CFLAGS) -O0 $< -o $@
+
+%.opt64.exe : %.c
+	$(CC64) $(CFLAGS) -O2 $< -o $@
--- a/macaw-ppc-symbolic/tests/pass/identity.c
+++ b/macaw-ppc-symbolic/tests/pass/identity.c
@ -0,0 +1,15 @@
+int __attribute__((noinline)) test_identity(int x) {
+  return x == x;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_identity(0);
+}
--- a/macaw-ppc-symbolic/tests/pass/identity.opt64.exe
+++ b/macaw-ppc-symbolic/tests/pass/identity.opt64.exe
--- a/macaw-ppc-symbolic/tests/pass/identity.unopt64.exe
+++ b/macaw-ppc-symbolic/tests/pass/identity.unopt64.exe
--- a/macaw-ppc-symbolic/tests/pass/saturate-add.c
+++ b/macaw-ppc-symbolic/tests/pass/saturate-add.c
@ -0,0 +1,13 @@
+#include <limits.h>
+
+int __attribute__((noinline)) test_saturate_add(int x, int y) {
+  int c = x + y;
+  if(c < x || c < y)
+    c = INT_MAX;
+
+  return c >= x && c >= y;
+}
+
+void _start() {
+  test_saturate_add(1, 2);
+}
--- a/macaw-ppc-symbolic/tests/pass/saturate-add.opt64.exe
+++ b/macaw-ppc-symbolic/tests/pass/saturate-add.opt64.exe
--- a/macaw-ppc-symbolic/tests/pass/saturate-add.unopt64.exe
+++ b/macaw-ppc-symbolic/tests/pass/saturate-add.unopt64.exe
--- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
@ -490,7 +490,7 @@ initializeSimulator ctx sym archVals halloc cfg entryBlock = MS.withArchEval arc
  let lookupHdl = MS.LookupFunctionHandle $ \_ _ _ -> error "Function calls not supported"
  let mkPtrPred = MS.mkGlobalPointerValidityPred memPtrTable
  let ext = MS.macawExtensions archEvalFns memVar globalMappingFn lookupHdl mkPtrPred
-  let simCtx = C.initSimContext sym LLVM.llvmIntrinsicTypes halloc IO.stderr C.emptyHandleMap ext MS.MacawSimulatorState
+  let simCtx = C.initSimContext sym LLVM.llvmIntrinsicTypes halloc IO.stderr (C.FnBindings C.emptyHandleMap) ext MS.MacawSimulatorState
  let globalState = C.insertGlobal memVar memory1 C.emptyGlobals
  initRegs <- initialRegisterState sym archVals globalMappingFn memory1 entryBlock initSPVal
  let simulation = C.regValue <$> C.callCFG cfg initRegs
--- a/symbolic/macaw-symbolic.cabal
+++ b/symbolic/macaw-symbolic.cabal
@ -12,6 +12,7 @@ library
    base >= 4,
    bv-sized >= 1.0.0,
    containers,
+    elf-edit,
    IntervalMap >= 0.6 && < 0.7,
    crucible >= 0.4,
    crucible-llvm,
@ -32,6 +33,7 @@ library
    Data.Macaw.Symbolic.Backend
    Data.Macaw.Symbolic.Memory
    Data.Macaw.Symbolic.MemOps
+    Data.Macaw.Symbolic.Testing
  other-modules:
    Data.Macaw.Symbolic.Bitcast
    Data.Macaw.Symbolic.CrucGen
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@ -1250,7 +1250,7 @@ runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH toMemPred g reg
                             C.emptyHandleMap
                extImpl = macawExtensions archEval mvar globs lookupH toMemPred
            in C.initSimContext sym llvmIntrinsicTypes halloc stdout
-               fnBindings extImpl MacawSimulatorState
+               (C.FnBindings fnBindings) extImpl MacawSimulatorState
  -- Create the symbolic simulator state
  let initGlobals = C.insertGlobal mvar initMem C.emptyGlobals
  let retType = macawStructRepr
--- a/symbolic/src/Data/Macaw/Symbolic/Testing.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Testing.hs
@ -0,0 +1,407 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+-- | This module defines common test harness code that can be used in each of the
+-- architecture-specific backends
+--
+-- The model is:
+--
+-- 1. Load an ELF file and run code discovery on it (returning the ELF and a DiscoveryFunInfo)
+--
+-- 2. Provide the harness a list of discovered functions to simulate and try to
+--    prove the result of (there is a helper for selecting tests whose name
+--    begins with test_)
+--
+-- Note that tests invoked by this harness must not call other functions, as
+-- function resolution is not set up.
+module Data.Macaw.Symbolic.Testing (
+  runDiscovery,
+  ResultExtractor(..),
+  simulateAndVerify,
+  SimulationResult(..),
+  SATResult(..),
+  toAddrSymMap,
+  -- * Execution features
+  SomeBackend(..),
+  defaultExecFeatures
+  ) where
+
+import qualified Control.Exception as X
+import qualified Control.Lens as L
+import qualified Control.Monad.ST as ST
+import qualified Data.BitVector.Sized as BVS
+import qualified Data.ByteString as BS
+import qualified Data.ElfEdit as EE
+import qualified Data.Foldable as F
+import qualified Data.Macaw.Architecture.Info as MAI
+import qualified Data.Macaw.CFG as MC
+import qualified Data.Macaw.Discovery as MD
+import qualified Data.Macaw.Memory as MM
+import qualified Data.Macaw.Memory.ElfLoader as MEL
+import qualified Data.Macaw.Symbolic as MS
+import qualified Data.Macaw.Symbolic.Memory as MSM
+import qualified Data.Macaw.Types as MT
+import qualified Data.Map as Map
+import qualified Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.List as PL
+import qualified Data.Parameterized.NatRepr as PN
+import           Data.Parameterized.Some ( Some(..) )
+import           Data.Proxy ( Proxy(..) )
+import qualified Data.Text as Text
+import qualified Data.Text.Encoding as Text
+import qualified Data.Text.Encoding.Error as Text
+import qualified Data.Traversable as T
+import           GHC.TypeNats ( type (<=) )
+import qualified Lang.Crucible.Analysis.Postdom as CAP
+import qualified Lang.Crucible.Backend as CB
+import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.CFG.Core as CCC
+import qualified Lang.Crucible.CFG.Extension as CCE
+import qualified Lang.Crucible.FunctionHandle as CFH
+import qualified Lang.Crucible.LLVM.DataLayout as CLD
+import qualified Lang.Crucible.LLVM.Intrinsics as CLI
+import qualified Lang.Crucible.LLVM.MemModel as CLM
+import qualified Lang.Crucible.Simulator as CS
+import qualified Lang.Crucible.Simulator.GlobalState as CSG
+import qualified Lang.Crucible.Simulator.PathSatisfiability as CSP
+import qualified Lang.Crucible.Types as CT
+import qualified System.IO as IO
+import qualified What4.BaseTypes as WT
+import qualified What4.Expr as WE
+import qualified What4.FunctionName as WF
+import qualified What4.Interface as WI
+import qualified What4.ProgramLoc as WPL
+import qualified What4.Protocol.Online as WPO
+import qualified What4.SatResult as WSR
+import qualified What4.Solver as WS
+import qualified What4.Symbol as WSym
+
+data TestingException = ELFResolutionError String
+  deriving (Show)
+
+instance X.Exception TestingException
+
+nullDiscoveryLogger :: (Monad m) => a -> m ()
+nullDiscoveryLogger _ = return ()
+
+posFn :: (MM.MemWidth w) => MM.MemSegmentOff w -> WPL.Position
+posFn = WPL.OtherPos . Text.pack . show
+
+-- | Load an ELF file into a macaw 'MM.Memory' (and symbols)
+loadELF :: EE.ElfHeaderInfo w
+        -> IO (MM.Memory w, [MEL.MemSymbol w])
+loadELF ehi = do
+  let loadOpts = MEL.defaultLoadOptions
+  case MEL.resolveElfContents loadOpts ehi of
+    Left err -> X.throwIO (ELFResolutionError err)
+    Right (warnings, mem, _mentry, nameAddrList) -> do
+      F.forM_ warnings $ \w -> do
+        IO.hPutStrLn IO.stderr w
+      return (mem, nameAddrList)
+
+-- | Convert a list of symbols into a mapping from entry point addresses to function names
+--
+-- Meant to be passed to 'runDiscovery' to compute (named) entry points
+--
+-- NOTE that the 'MM.Memory' is unused, but provided to make the API cleaner
+-- (since some clients do need a 'MM.Memory', and 'runDiscovery' passes that as
+-- an extra argument).
+toAddrSymMap :: MM.Memory w
+             -> [MEL.MemSymbol w]
+             -> Map.Map (MEL.MemSegmentOff w) BS.ByteString
+toAddrSymMap _mem nameAddrList =
+  Map.fromList [ (MEL.memSymbolStart msym, MEL.memSymbolName msym)
+               | msym <- nameAddrList
+               ]
+
+-- | Run code discovery over every function entry point (i.e., a function with a
+-- symbol attached to it, plus the program entry point) and return the resulting
+-- 'MD.DiscoveryFunInfo' for each.
+runDiscovery :: (MC.ArchAddrWidth arch ~ w)
+             => EE.ElfHeaderInfo w
+             -> (MM.Memory w -> [MEL.MemSymbol w] -> Map.Map (MM.MemSegmentOff w) BS.ByteString)
+             -- ^ A function to turn discovered symbols into (address, name)
+             -- mappings; the addresses are used as test entry points
+             --
+             -- A good default is 'toAddrySymMap'
+             -> MAI.ArchitectureInfo arch
+             -> IO (MM.Memory w, [Some (MD.DiscoveryFunInfo arch)])
+runDiscovery ehi toEntryPoints archInfo = do
+  (mem, nameAddrList) <- loadELF ehi
+  let addrSymMap = toEntryPoints mem nameAddrList
+  let ds0 = MD.emptyDiscoveryState mem addrSymMap archInfo
+  fns <- T.forM (Map.keys addrSymMap) $ \entryPoint -> do
+    -- We are discovering each function in isolation for now, so we can throw
+    -- away the updated discovery state.
+    --
+    -- NOTE: If we extend this to support function calls, we will probably want
+    -- to just turn this into a fold/use the main discovery entry point.
+    (_ds1, dfi) <- ST.stToIO (MD.analyzeFunction nullDiscoveryLogger entryPoint MD.UserRequest ds0)
+    return dfi
+  return (mem, fns)
+
+data SATResult = Unsat | Sat | Unknown
+  deriving (Eq, Show)
+
+data SimulationResult = SimulationAborted
+                      | SimulationTimeout
+                      | SimulationPartial
+                      | SimulationResult SATResult
+                      deriving (Eq, Show)
+
+-- | Allocate a fresh symbolic value for initial register states
+mkInitialRegVal :: (CB.IsSymInterface sym, MT.HasRepr (MC.ArchReg arch) MT.TypeRepr)
+                => MS.MacawSymbolicArchFunctions arch
+                -> sym
+                -> MC.ArchReg arch tp
+                -> IO (CS.RegValue' sym (MS.ToCrucibleType tp))
+mkInitialRegVal archFns sym r = do
+  let regName = MS.crucGenArchRegName archFns r
+  case MT.typeRepr r of
+    MT.BoolTypeRepr ->
+      CS.RV <$> WI.freshConstant sym regName WT.BaseBoolRepr
+    MT.BVTypeRepr w -> do
+      c <- WI.freshConstant sym regName (WT.BaseBVRepr w)
+      ptr <- CLM.llvmPointer_bv sym c
+      return (CS.RV ptr)
+    MT.TupleTypeRepr PL.Nil -> return (CS.RV Ctx.Empty)
+    MT.TupleTypeRepr {} -> error ("Tuple-typed registers are not supported in the macaw-symbolic test harness: " ++ show regName)
+    MT.FloatTypeRepr {} -> error ("Float-typed registers are not supported in the macaw-symbolic test harness: " ++ show regName)
+    MT.VecTypeRepr {} -> error ("Vector-typed registers are not supported in the macaw-symbolic test harness: " ++ show regName)
+
+-- | Create a name for the given 'MD.DiscoveryFunInfo'
+--
+-- If the function has no name, just use its address
+functionName :: (MM.MemWidth (MC.ArchAddrWidth arch)) => MD.DiscoveryFunInfo arch ids -> WF.FunctionName
+functionName dfi = maybe addrName fromByteString (MD.discoveredFunSymbol dfi)
+  where
+    addrName = WF.functionNameFromText (Text.pack (show (MD.discoveredFunAddr dfi)))
+    fromByteString = WF.functionNameFromText . Text.decodeUtf8With Text.lenientDecode
+
+-- | Convert the given function into a Crucible CFG, symbolically execute it,
+-- and treat the return value as an assertion to be verified.
+--
+-- The initial environment of the symbolic execution populates global memory
+-- with the (concrete) contents of the data segment.  It provides fully symbolic
+-- inputs in all registers (except as directed by architecture-specific code).
+--
+-- An initial stack will be allocated and the stack pointer location will be
+-- populated with an appropriate pointer into that storage.  The initial stack
+-- will have completely symbolic contents.
+--
+-- One of the arguments to this function selects the return value from the
+-- simulator state.
+--
+-- In the API, recall that 'MS.MacawSymbolicArchFunctions' are used during
+-- *translation* of programs into Crucible, while 'MS.MacawArchEvalFn' is used
+-- during symbolic execution (to provide interpretations to
+-- architecture-specific primitives).
+simulateAndVerify :: forall arch sym ids w t st fs
+                   . ( CB.IsSymInterface sym
+                     , CCE.IsSyntaxExtension (MS.MacawExt arch)
+                     , MM.MemWidth (MC.ArchAddrWidth arch)
+                     , w ~ MC.ArchAddrWidth arch
+                     , 16 <= w
+                     , MT.KnownNat w
+                     , sym ~ WE.ExprBuilder t st fs
+                     )
+                  => WS.SolverAdapter st
+                  -- ^ The solver adapter to use to discharge assertions
+                  -> WS.LogData
+                  -- ^ A logger to (optionally) record solver interaction (for the goal solver)
+                  -> sym
+                  -- ^ The symbolic backend
+                  -> [CS.GenericExecutionFeature sym]
+                  -- ^ Crucible execution features, see 'defaultExecFeatures' for a good initial selection
+                  -> MAI.ArchitectureInfo arch
+                  -- ^ The architecture info (only really used for endianness in this context)
+                  -> MS.ArchVals arch
+                  -- ^ Architecture-specific register state inspection and manipulation
+                  -> MM.Memory w
+                  -- ^ The initial contents of static memory
+                  -> ResultExtractor sym arch
+                  -- ^ A function to extract the return value of a function from its post-state
+                  -> MD.DiscoveryFunInfo arch ids
+                  -- ^ The function to simulate and verify
+                  -> IO SimulationResult
+simulateAndVerify goalSolver logger sym execFeatures archInfo archVals mem (ResultExtractor withResult) dfi =
+  MS.withArchConstraints archVals $ do
+    let funName = functionName dfi
+    halloc <- CFH.newHandleAllocator
+    CCC.SomeCFG g <- MS.mkFunCFG (MS.archFunctions archVals) halloc funName posFn dfi
+
+    let endianness = toCrucibleEndian (MAI.archEndianness archInfo)
+    let ?recordLLVMAnnotation = \_ _ -> return ()
+    (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @arch) sym endianness MSM.ConcreteMutable mem
+    let globalMap = MSM.mapRegionPointers memPtrTbl
+    (memVar, stackPointer, execResult) <- simulateFunction sym execFeatures archVals halloc initMem globalMap g
+    case execResult of
+      CS.TimeoutResult {} -> return SimulationTimeout
+      CS.AbortedResult {} -> return SimulationAborted
+      CS.FinishedResult _simCtx partialRes ->
+        case partialRes of
+          CS.PartialRes {} -> return SimulationPartial
+          CS.TotalRes gp -> do
+            let Just postMem = CSG.lookupGlobal memVar (gp L.^. CS.gpGlobals)
+            withResult (gp L.^. CS.gpValue) stackPointer postMem $ \resRepr val -> do
+              -- The function is assumed to return a value that is intended to be
+              -- True.  Try to prove that (by checking the negation for unsat)
+              --
+              -- The result is treated as true if it is not equal to zero
+              zero <- WI.bvLit sym resRepr (BVS.mkBV resRepr 0)
+              bv_val <- CLM.projectLLVM_bv sym val
+              notZero <- WI.bvNe sym bv_val zero
+              goal <- WI.notPred sym notZero
+              WS.solver_adapter_check_sat goalSolver sym logger [goal] $ \satRes ->
+                case satRes of
+                  WSR.Sat {} -> return (SimulationResult Sat)
+                  WSR.Unsat {} -> return (SimulationResult Unsat)
+                  WSR.Unknown -> return (SimulationResult Unknown)
+
+-- | Set up the symbolic execution engine with initial states and execute
+--
+-- It returns:
+--
+-- 1. The global variable that holds the memory state (allowing for
+--    inspecting the post-state, which is extracted from the 'CS.ExecResult')
+--
+-- 2. The stack pointer for the function
+--
+-- 3. The result of symbolic execution
+--
+-- Note that the provided 'CLM.MemImpl' is expected to have its global state
+-- populated as desired.  The default loader populates it with concrete (and
+-- mutable) values taken from the data segment of the binary (as well as the
+-- immutable contents of the text segment).
+simulateFunction :: ( ext ~ MS.MacawExt arch
+                    , CCE.IsSyntaxExtension ext
+                    , CB.IsSymInterface sym
+                    , CLM.HasLLVMAnn sym
+                    , MS.SymArchConstraints arch
+                    , w ~ MC.ArchAddrWidth arch
+                    , 16 <= w
+                    )
+                 => sym
+                 -> [CS.GenericExecutionFeature sym]
+                 -> MS.ArchVals arch
+                 -> CFH.HandleAllocator
+                 -> CLM.MemImpl sym
+                 -> MS.GlobalMap sym CLM.Mem w
+                 -> CCC.CFG ext blocks (Ctx.EmptyCtx Ctx.::> MS.ArchRegStruct arch) (MS.ArchRegStruct arch)
+                 -> IO ( CS.GlobalVar CLM.Mem
+                       , CLM.LLVMPtr sym w
+                       , CS.ExecResult (MS.MacawSimulatorState sym) sym ext (CS.RegEntry sym (MS.ArchRegStruct arch))
+                       )
+simulateFunction sym execFeatures archVals halloc initMem globalMap g = do
+  let symArchFns = MS.archFunctions archVals
+  let crucRegTypes = MS.crucArchRegTypes symArchFns
+  let regsRepr = CT.StructRepr crucRegTypes
+
+  -- Initialize memory
+  --
+  -- This includes both global static memory (taken from the data segment
+  -- initial contents) and a totally symbolic stack
+
+  -- Allocate a stack and insert it into memory
+  --
+  -- The stack allocation uses the SMT array backed memory model (rather than
+  -- the Haskell-level memory model)
+  stackArrayStorage <- WI.freshConstant sym (WSym.safeSymbol "stack_array") WI.knownRepr
+  stackSize <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (2 * 1024 * 1024))
+  let ?ptrWidth = WI.knownRepr
+  (stackBasePtr, mem1) <- CLM.doMalloc sym CLM.StackAlloc CLM.Mutable "stack_alloc" initMem stackSize CLD.noAlignment
+  mem2 <- CLM.doArrayStore sym mem1 stackBasePtr CLD.noAlignment stackArrayStorage stackSize
+
+  -- Make initial registers, including setting up a stack pointer (which points
+  -- into the middle of the stack allocation, to allow accesses into the caller
+  -- frame if needed (though it generally should not be)
+  initialRegs <- MS.macawAssignToCrucM (mkInitialRegVal symArchFns sym) (MS.crucGenRegAssignment symArchFns)
+  stackInitialOffset <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (1024 * 1024))
+  sp <- CLM.ptrAdd sym WI.knownRepr stackBasePtr stackInitialOffset
+  let initialRegsEntry = CS.RegEntry regsRepr initialRegs
+  let regsWithStack = MS.updateReg archVals initialRegsEntry MC.sp_reg sp
+
+  memVar <- CLM.mkMemVar halloc
+  let initGlobals = CSG.insertGlobal memVar mem2 CS.emptyGlobals
+  let arguments = CS.RegMap (Ctx.singleton regsWithStack)
+  let simAction = CS.runOverrideSim regsRepr (CS.regValue <$> CS.callCFG g arguments)
+
+  let fnBindings = CFH.insertHandleMap (CCC.cfgHandle g) (CS.UseCFG g (CAP.postdomInfo g)) CFH.emptyHandleMap
+  MS.withArchEval archVals sym $ \archEvalFn -> do
+    let extImpl = MS.macawExtensions archEvalFn memVar globalMap lookupFunction validityCheck
+    let ctx = CS.initSimContext sym CLI.llvmIntrinsicTypes halloc IO.stdout (CS.FnBindings fnBindings) extImpl MS.MacawSimulatorState
+    let s0 = CS.InitialState ctx initGlobals CS.defaultAbortHandler regsRepr simAction
+    res <- CS.executeCrucible (fmap CS.genericToExecutionFeature execFeatures) s0
+    return (memVar, sp, res)
+
+-- | A wrapper around the symbolic backend that allows us to recover the online
+-- constraints when they are available
+--
+-- The online constraints allow us to turn on path satisfiability checking
+data SomeBackend sym where
+  SomeOnlineBackend :: ( sym ~ CBO.OnlineBackend scope solver fs
+                       , WPO.OnlineSolver solver
+                       , CB.IsSymInterface sym
+                       ) => sym -> SomeBackend sym
+  SomeOfflineBackend :: sym -> SomeBackend sym
+
+-- | A default set of execution features that are flexible enough to support a
+-- wide range of tests.  If the backend provided supports online solving, the
+-- execution features will include path satisfiability checking to allow simple
+-- loops in test cases.
+defaultExecFeatures :: SomeBackend sym -> IO [CS.GenericExecutionFeature sym]
+defaultExecFeatures backend =
+  case backend of
+    SomeOfflineBackend {} -> return []
+    SomeOnlineBackend sym -> do
+      pathSat <- CSP.pathSatisfiabilityFeature sym (CBO.considerSatisfiability sym)
+      return [pathSat]
+
+-- | This type wraps up a function that takes the post-state of a symbolic
+-- execution and extracts the return value from executing that function
+--
+-- The details are architecture specific.  Some architectures return values via
+-- dedicated registers, while others return values on the stack.
+--
+-- This function takes the final register state and the post-state of memory,
+-- allowing arbitrary access.
+--
+-- Note that the function that clients provide could return any arbitrary
+-- post-state value (e.g., a distinguished memory location) - the rest of this
+-- test harness is agnostic.
+--
+-- The function parameter is a continuation under which the caller (i.e., the
+-- test harness) has access to the value provided by the user of the test harness.
+data ResultExtractor sym arch where
+  ResultExtractor :: (forall a
+                       . CS.RegEntry sym (MS.ArchRegStruct arch)
+                      -> CLM.LLVMPtr sym (MC.ArchAddrWidth arch)
+                      -> CLM.MemImpl sym
+                      -> (forall n . (1 <= n) => PN.NatRepr n -> CLM.LLVMPtr sym n -> IO a)
+                      -> IO a)
+                  -> ResultExtractor sym arch
+
+-- | The test harness does not currently support calling functions from test cases.
+--
+-- It could be modified to do so.
+lookupFunction :: MS.LookupFunctionHandle sym arch
+lookupFunction = MS.LookupFunctionHandle $ \_s _mem _regs -> do
+  error "Function calls are not supported in the macaw-symbolic test harness"
+
+-- | The test suite does not currently generate global pointer well-formedness
+-- conditions (though it could be changed to do so).  This could become a
+-- parameter.
+validityCheck :: MS.MkGlobalPointerValidityAssertion sym w
+validityCheck _ _ _ _ = return Nothing
+
+-- | Convert from macaw endianness to the LLVM memory model endianness
+toCrucibleEndian :: MEL.Endianness -> CLD.EndianForm
+toCrucibleEndian e =
+  case e of
+    MM.LittleEndian -> CLD.LittleEndian
+    MM.BigEndian -> CLD.BigEndian
--- a/x86_symbolic/macaw-x86-symbolic.cabal
+++ b/x86_symbolic/macaw-x86-symbolic.cabal
@ -47,11 +47,16 @@ test-suite macaw-x86-symbolic-tests
    crucible,
    crucible-llvm,
    elf-edit,
+    filepath,
+    Glob >= 0.9 && < 0.11,
    macaw-base,
    macaw-symbolic,
    macaw-x86,
    macaw-x86-symbolic,
    parameterized-utils,
+    prettyprinter,
+    tasty,
+    tasty-hunit,
    text,
    what4,
    vector
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@ -1,136 +1,162 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 module Main (main) where

-import           Control.Monad
-import           Control.Monad.ST
 import qualified Data.ByteString as BS
+import qualified Data.ByteString.Char8 as BS8
 import qualified Data.ElfEdit as Elf
-import qualified Data.Map.Strict as Map
-import           Data.Parameterized.Nonce
-import           Data.Parameterized.Some
+import qualified Data.Foldable as F
+import           Data.Maybe ( mapMaybe )
+import qualified Data.Parameterized.Classes as PC
+import qualified Data.Parameterized.Nonce as PN
+import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
-import qualified Data.Text as Text
-import           GHC.IO (ioToST)
-import           System.IO
+import qualified Prettyprinter as PP
+import           System.FilePath ( (</>), (<.>) )
+import qualified System.FilePath.Glob as SFG
+import qualified System.IO as IO
+import qualified Test.Tasty as TT
+import qualified Test.Tasty.HUnit as TTH
+import qualified Test.Tasty.Options as TTO
+import qualified Test.Tasty.Runners as TTR

-import qualified Data.Macaw.Architecture.Info as M
-import qualified Data.Macaw.CFG.Core as M
+import qualified Data.Macaw.CFG as MC
 import qualified Data.Macaw.Discovery as M
-import qualified Data.Macaw.Memory as M
-import qualified Data.Macaw.Memory.ElfLoader as Elf
 import qualified Data.Macaw.Symbolic as MS
-import qualified Data.Macaw.Symbolic.Memory as MSM
-import qualified Data.Macaw.Types as M
+import qualified Data.Macaw.Symbolic.Testing as MST
 import qualified Data.Macaw.X86 as MX
-import qualified Data.Macaw.X86.Symbolic as MX
+import           Data.Macaw.X86.Symbolic ()
+import qualified What4.Config as WC
+import qualified What4.Interface as WI
+import qualified What4.ProblemFeatures as WPF
+import qualified What4.Solver as WS

-import qualified What4.ProgramLoc as C
-import qualified What4.Interface as C
+import qualified Lang.Crucible.Backend as CB
+import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.Simulator as CS

-import qualified Lang.Crucible.Backend as C
-import qualified Lang.Crucible.Backend.Simple as C
-import qualified Lang.Crucible.CFG.Core as C
-import qualified Lang.Crucible.FunctionHandle as C
-import           Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian))
-import qualified Lang.Crucible.LLVM.MemModel as C
-import qualified Lang.Crucible.Simulator.ExecutionTree as C
-import qualified Lang.Crucible.Simulator.RegValue as C
+-- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
+data SaveSMT = SaveSMT Bool
+  deriving (Eq, Show)

-mkReg :: (C.IsSymInterface sym, M.HasRepr (M.ArchReg arch) M.TypeRepr)
-      => MS.MacawSymbolicArchFunctions arch
-      -> sym
-      -> M.ArchReg arch tp
-      -> IO (C.RegValue' sym (MS.ToCrucibleType tp))
-mkReg archFns sym r =
-  case M.typeRepr r of
-    M.BoolTypeRepr ->
-      C.RV <$> C.freshConstant sym (MS.crucGenArchRegName archFns r) C.BaseBoolRepr
-    M.BVTypeRepr w ->
-      C.RV <$> (C.llvmPointer_bv sym =<< C.freshConstant sym (MS.crucGenArchRegName archFns r) (C.BaseBVRepr w))
-    M.TupleTypeRepr{}  ->
-      error "macaw-symbolic do not support tuple types."
-    M.FloatTypeRepr{}  ->
-      error "macaw-symbolic do not support float types."
-    M.VecTypeRepr{}  ->
-      error "macaw-symbolic do not support vector types."
+instance TTO.IsOption SaveSMT where
+  defaultValue = SaveSMT False
+  parseValue v = SaveSMT <$> TTO.safeReadBool v
+  optionName = pure "save-smt"
+  optionHelp = pure "Save SMT sessions to files in /tmp for debugging"
+
+-- | A tasty option to have the test suite save the macaw IR for each test case to /tmp for debugging purposes
+data SaveMacaw = SaveMacaw Bool
+
+instance TTO.IsOption SaveMacaw where
+  defaultValue = SaveMacaw False
+  parseValue v = SaveMacaw <$> TTO.safeReadBool v
+  optionName = pure "save-macaw"
+  optionHelp = pure "Save Macaw IR for each test case to /tmp for debugging"
+
+ingredients :: [TTR.Ingredient]
+ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
+                                  , TTO.Option (Proxy @SaveMacaw)
+                                  ] : TT.defaultIngredients

 main :: IO ()
 main = do
-  Some (gen :: NonceGenerator IO t) <- newIONonceGenerator
-  halloc <- C.newHandleAllocator
-  sym <- C.newSimpleBackend C.FloatRealRepr gen
+  -- These are pass/fail in that the assertions in the "pass" set are true (and
+  -- the solver returns Unsat), while the assertions in the "fail" set are false
+  -- (and the solver returns Sat).
+  passTestFilePaths <- SFG.glob "tests/pass/*.exe"
+  failTestFilePaths <- SFG.glob "tests/fail/*.exe"
+  let passRes = MST.SimulationResult MST.Unsat
+  let failRes = MST.SimulationResult MST.Sat
+  let passTests = TT.testGroup "True assertions" (map (mkSymExTest passRes) passTestFilePaths)
+  let failTests = TT.testGroup "False assertions" (map (mkSymExTest failRes) failTestFilePaths)
+  TT.defaultMainWithIngredients ingredients (TT.testGroup "Binary Tests" [passTests, failTests])

-  let x86ArchFns :: MS.MacawSymbolicArchFunctions MX.X86_64
-      x86ArchFns = MX.x86_64MacawSymbolicFns
+hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
+hasTestPrefix (Some dfi) = do
+  bsname <- M.discoveredFunSymbol dfi
+  if BS8.pack "test_" `BS8.isPrefixOf` bsname
+    then return (bsname, Some dfi)
+    else Nothing

-  let posFn :: M.MemSegmentOff 64 -> C.Position
-      posFn = C.OtherPos . Text.pack . show
+-- | X86_64 functions with a single scalar return value return it in %rax
+--
+-- Since all test functions must return a value to assert as true, this is
+-- straightforward to extract
+x86ResultExtractor :: (CB.IsSymInterface sym) => MS.ArchVals MX.X86_64 -> MST.ResultExtractor sym MX.X86_64
+x86ResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do
+  let re = MS.lookupReg archVals regs MX.RAX
+  k PC.knownRepr (CS.regValue re)

-  elfContents <- BS.readFile "tests/add_ubuntu64"
-  elf <-
-    case Elf.decodeElfHeaderInfo elfContents of
-      Left (_, msg) -> fail $ "Error parsing Elf file: " <> msg
-      Right (Elf.SomeElf e) ->
-        case Elf.headerClass (Elf.header e) of
-          Elf.ELFCLASS64 -> pure e
-          Elf.ELFCLASS32 -> fail "Expected 64-bit elf file"
+mkSymExTest :: MST.SimulationResult -> FilePath -> TT.TestTree
+mkSymExTest expected exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOption $ \saveMacaw@(SaveMacaw _) -> TTH.testCaseSteps exePath $ \step -> do
+  bytes <- BS.readFile exePath
+  case Elf.decodeElfHeaderInfo bytes of
+    Left (_, msg) -> TTH.assertFailure ("Error parsing ELF header from file '" ++ show exePath ++ "': " ++ msg)
+    Right (Elf.SomeElf ehi) -> do
+      case Elf.headerClass (Elf.header ehi) of
+        Elf.ELFCLASS32 -> TTH.assertFailure "32 bit x86 binaries are not supported"
+        Elf.ELFCLASS64 -> do
+          (mem, funInfos) <- MST.runDiscovery ehi MST.toAddrSymMap MX.x86_64_linux_info
+          let testEntryPoints = mapMaybe hasTestPrefix funInfos
+          F.forM_ testEntryPoints $ \(name, Some dfi) -> do
+            step ("Testing " ++ BS8.unpack name)
+            writeMacawIR saveMacaw (BS8.unpack name) dfi
+            Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator
+            CBO.withYicesOnlineBackend CBO.FloatRealRepr gen CBO.NoUnsatFeatures WPF.noFeatures $ \sym -> do
+              -- We are using the z3 backend to discharge proof obligations, so
+              -- we need to add its options to the backend configuration
+              let solver = WS.z3Adapter
+              let backendConf = WI.getConfiguration sym
+              WC.extendConfig (WS.solver_adapter_config_options solver) backendConf

-  let loadOpt :: Elf.LoadOptions
-      loadOpt = Elf.defaultLoadOptions
-  (mem, nameAddrList) <-
-    case Elf.resolveElfContents loadOpt elf of
-      Left err -> fail err
-      Right (warn, mem, _mentry, nameAddrList)  -> do
-        forM_ warn $ \err -> do
-          hPutStrLn stderr err
-        pure (mem, nameAddrList)
+              execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend sym)
+              let Just archVals = MS.archVals (Proxy @MX.X86_64)
+              let extract = x86ResultExtractor archVals
+              logger <- makeGoalLogger saveSMT solver name exePath
+              simRes <- MST.simulateAndVerify solver logger sym execFeatures MX.x86_64_linux_info archVals mem extract dfi
+              TTH.assertEqual "AssertionResult" expected simRes

-  addAddr <-
-    case [ Elf.memSymbolStart msym | msym <- nameAddrList, Elf.memSymbolName msym == "add" ] of
-      [addr] -> pure $! addr
-      [] -> fail "Could not find add function"
-      _ -> fail "Found multiple add functions"
+writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()
+writeMacawIR (SaveMacaw sm) name dfi
+  | not sm = return ()
+  | otherwise = writeFile (toSavedMacawPath name) (show (PP.pretty dfi))

-  let addrSymMap :: M.AddrSymMap 64
-      addrSymMap = Map.fromList [ (Elf.memSymbolStart msym, Elf.memSymbolName msym)
-                                | msym <- nameAddrList ]
-  let archInfo :: M.ArchitectureInfo MX.X86_64
-      archInfo =  MX.x86_64_linux_info
+toSavedMacawPath :: String -> FilePath
+toSavedMacawPath testName = "/tmp" </> name <.> "macaw"
+  where
+    name = fmap escapeSlash testName

-  let ds0 :: M.DiscoveryState MX.X86_64
-      ds0 = M.emptyDiscoveryState mem addrSymMap archInfo
+-- | Construct a solver logger that saves the SMT session for the goal solving
+-- in /tmp (if requested by the save-smt option)
+--
+-- The adapter name is included so that, if the same test is solved with
+-- multiple solvers, we can differentiate them.
+makeGoalLogger :: SaveSMT -> WS.SolverAdapter st -> BS8.ByteString -> FilePath -> IO WS.LogData
+makeGoalLogger (SaveSMT saveSMT) adapter funName p
+  | not saveSMT = return WS.defaultLogData
+  | otherwise = do
+      hdl <- IO.openFile (toSavedSMTSessionPath adapter funName p) IO.WriteMode
+      return (WS.defaultLogData { WS.logHandle = Just hdl })

-  let logFn addr = ioToST $ do
-        putStrLn $ "Analyzing " ++ show addr

-  (_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0
-  C.SomeCFG g <- MS.mkFunCFG x86ArchFns halloc "add" posFn funInfo
+-- | Construct a path in /tmp to save the SMT session to
+--
+-- Just take the original path name and turn all of the slashes into underscores to escape them
+toSavedSMTSessionPath :: WS.SolverAdapter st -> BS8.ByteString -> FilePath -> FilePath
+toSavedSMTSessionPath adapter funName p = "/tmp" </> filename <.> "smtlib2"
+  where
+    filename = concat [ fmap escapeSlash p
+                      , "_"
+                      , BS8.unpack funName
+                      , "_"
+                      , WS.solver_adapter_name adapter
+                      ]

-  regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)
-
-  symFuns <- MX.newSymFuns sym
-
-  let ?recordLLVMAnnotation = \_ _ -> pure ()
-
-  (initMem, memPtrTbl) <-  MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem
-  let globalMap = MSM.mapRegionPointers memPtrTbl
-
-  let lookupFn :: MS.LookupFunctionHandle sym MX.X86_64
-      lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> do
-        fail "Could not find function handle."
-  let validityCheck :: MS.MkGlobalPointerValidityAssertion sym 64
-      validityCheck _ _ _ _ = return Nothing
-  execResult <-
-     MS.runCodeBlock sym x86ArchFns (MX.x86_64MacawEvalFn symFuns)
-        halloc (initMem, globalMap) lookupFn validityCheck g regs
-  case execResult of
-    (_,C.FinishedResult _ (C.TotalRes _pair))-> do
-      pure ()
-    _ -> do
-      pure () -- For now, we are ok with this.
+escapeSlash :: Char -> Char
+escapeSlash '/' = '_'
+escapeSlash c = c
--- a/x86_symbolic/tests/README.org
+++ b/x86_symbolic/tests/README.org
@ -0,0 +1,16 @@
+* Overview
+This test suite tests that symbolic execution of x86_64 programs works. It is also a convenient place to test the semantics.  The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories.  In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states.  It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion).  Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected).  The test harness uses yices for path satisfiability checking and z3 to prove goals.  Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
+
+* Usage
+
+The test runner has two command line options (beyond the defaults for tasty):
+
+- ~--save-macaw~: Saves the Macaw IR for each test case to /tmp for debugging purposes
+- ~--save-smt~: Saves the generated SMTLib for each test to /tmp for debugging purposes
+
+
+* Limitations
+- It currently tests both optimized an unoptimized binaries. It is intended that this set will expand and that a wide variety of compilers will be tested.
+- Only two solvers are involved in the test, rather than a whole matrix
+- Function calls are not supported in test cases
+- There are no facilities for generating symbolic data beyond the initial symbolic arguments to each function
--- a/x86_symbolic/tests/add.c
+++ b/x86_symbolic/tests/add.c
@ -1,18 +0,0 @@
-/*
-
-This is a small file designed to create a minimal test of the symbolic simulator.
-
-It can be compiled with:
-
-  clang -o test_add.o -O2 -c -momit-leaf-frame-pointer test_add.c
-*/
-
-#include <stdint.h>
-
-uint64_t __attribute__((noinline)) add(uint64_t x, uint64_t y) {
-    return x + y;
-}
-
-int main() {
-  return add(1, 2);
-}
--- a/x86_symbolic/tests/add_ubuntu64
+++ b/x86_symbolic/tests/add_ubuntu64
--- a/x86_symbolic/tests/add_ubuntu64.o
+++ b/x86_symbolic/tests/add_ubuntu64.o
--- a/x86_symbolic/tests/fail/Makefile
+++ b/x86_symbolic/tests/fail/Makefile
@ -0,0 +1,13 @@
+CC=gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt = $(patsubst %.c,%.unopt.exe,$(wildcard *.c))
+opt = $(patsubst %.c,%.opt.exe,$(wildcard *.c))
+
+all: $(unopt) $(opt)
+
+%.unopt.exe : %.c
+	$(CC) $(CFLAGS) -O0 $< -o $@
+
+%.opt.exe : %.c
+	$(CC) $(CFLAGS) -O2 $< -o $@
--- a/x86_symbolic/tests/fail/constant.c
+++ b/x86_symbolic/tests/fail/constant.c
@ -0,0 +1,16 @@
+// This test fails because x is not always 1
+int __attribute__((noinline)) test_constant(int x) {
+  return x == 1;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_constant(0);
+}
--- a/x86_symbolic/tests/fail/constant.opt.exe
+++ b/x86_symbolic/tests/fail/constant.opt.exe
--- a/x86_symbolic/tests/fail/constant.unopt.exe
+++ b/x86_symbolic/tests/fail/constant.unopt.exe
--- a/x86_symbolic/tests/pass/Makefile
+++ b/x86_symbolic/tests/pass/Makefile
@ -0,0 +1,13 @@
+CC=gcc
+CFLAGS=-nostdlib -static -fno-stack-protector
+
+unopt = $(patsubst %.c,%.unopt.exe,$(wildcard *.c))
+opt = $(patsubst %.c,%.opt.exe,$(wildcard *.c))
+
+all: $(unopt) $(opt)
+
+%.unopt.exe : %.c
+	$(CC) $(CFLAGS) -O0 $< -o $@
+
+%.opt.exe : %.c
+	$(CC) $(CFLAGS) -O2 $< -o $@
--- a/x86_symbolic/tests/pass/identity.c
+++ b/x86_symbolic/tests/pass/identity.c
@ -0,0 +1,15 @@
+int __attribute__((noinline)) test_identity(int x) {
+  return x == x;
+}
+
+// Notes:
+//
+// - The entry point is required by the compiler to make an executable
+//
+// - We can't put the test directly in _start because macaw-symbolic (and macaw
+//   in general) don't deal well with system calls
+//
+// - The test harness only looks for function symbols starting with test_
+void _start() {
+  test_identity(0);
+}
--- a/x86_symbolic/tests/pass/identity.opt.exe
+++ b/x86_symbolic/tests/pass/identity.opt.exe
--- a/x86_symbolic/tests/pass/identity.unopt.exe
+++ b/x86_symbolic/tests/pass/identity.unopt.exe
--- a/x86_symbolic/tests/pass/saturate-add.c
+++ b/x86_symbolic/tests/pass/saturate-add.c
@ -0,0 +1,13 @@
+#include <limits.h>
+
+int __attribute__((noinline)) test_saturate_add(int x, int y) {
+  int c = x + y;
+  if(c < x || c < y)
+    c = INT_MAX;
+
+  return c >= x && c >= y;
+}
+
+void _start() {
+  test_saturate_add(1, 2);
+}
--- a/x86_symbolic/tests/pass/saturate-add.opt.exe
+++ b/x86_symbolic/tests/pass/saturate-add.opt.exe
--- a/x86_symbolic/tests/pass/saturate-add.unopt.exe
+++ b/x86_symbolic/tests/pass/saturate-add.unopt.exe