Additional code for macaw-symbolic.

symbolic/src/Data/Macaw/Symbolic.hs

@@ -29,6 +29,8 @@ module Data.Macaw.Symbolic
     -- * Architecture-specific extensions
   , Data.Macaw.Symbolic.CrucGen.MacawArchStmtExtension
   , Data.Macaw.Symbolic.CrucGen.MacawArchConstraints
+  , MacawArchEvalFn
+  , EvalStmtFunc
   ) where
 
 import           Control.Lens ((^.))
@@ -230,25 +232,33 @@ macawExecApp sym f e0 =
         _ -> undefined sym xv yv cv
 
 
-macawExecStmt :: MacawStmtExtension arch (C.RegEntry sym) tp'
-              -> C.CrucibleState MacawSimulatorState sym (MacawExt arch) rtp blocks r ctx
-              -> IO (C.RegValue sym tp'
-                    , C.CrucibleState MacawSimulatorState sym (MacawExt arch) rtp blocks r ctx
-                    )
-macawExecStmt s0 _st =
+type EvalStmtFunc f p sym ext =
+  forall rtp blocks r ctx tp'.
+    f (C.RegEntry sym) tp'
+    -> C.CrucibleState p sym ext rtp blocks r ctx
+    -> IO (C.RegValue sym tp', C.CrucibleState p sym ext rtp blocks r ctx)
+
+-- | Function for evaluating an architecture-specific statement
+type MacawArchEvalFn sym arch =
+  EvalStmtFunc (MacawArchStmtExtension arch) MacawSimulatorState sym (MacawExt arch)
+
+macawExecStmt :: MacawArchEvalFn sym arch
+              -> EvalStmtFunc (MacawStmtExtension arch) MacawSimulatorState sym (MacawExt arch)
+macawExecStmt archStmtFn s0 st =
   case s0 of
     MacawReadMem{} -> undefined
     MacawCondReadMem{} -> undefined
     MacawWriteMem{} -> undefined
     MacawFreshSymbolic{} -> undefined
     MacawCall{} -> undefined
-    MacawArchStmtExtension{} -> undefined
+    MacawArchStmtExtension s -> archStmtFn s st
 
 -- | Return macaw extension evaluation functions.
-macawExtensions :: C.ExtensionImpl MacawSimulatorState sym (MacawExt arch)
-macawExtensions =
+macawExtensions :: MacawArchEvalFn sym arch
+                -> C.ExtensionImpl MacawSimulatorState sym (MacawExt arch)
+macawExtensions f =
   C.ExtensionImpl { C.extensionEval = macawExecApp
-                  , C.extensionExec = macawExecStmt
+                  , C.extensionExec = macawExecStmt f
                   }
 
 -- | Run the simulator over a contiguous set of code.
@@ -256,6 +266,8 @@ runCodeBlock :: forall sym arch blocks
            .  IsSymInterface sym
            => sym
            -> MacawSymbolicArchFunctions arch
+              -- ^ Translation functions
+           -> MacawArchEvalFn sym arch
            -> C.HandleAllocator RealWorld
            -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
            -> Ctx.Assignment (C.RegValue' sym) (MacawCrucibleRegTypes arch)
@@ -265,7 +277,7 @@ runCodeBlock :: forall sym arch blocks
                    sym
                    (MacawExt arch)
                    (C.RegEntry sym (ArchRegStruct arch)))
-runCodeBlock sym archFns halloc g regStruct = do
+runCodeBlock sym archFns archEval halloc g regStruct = do
   let crucRegTypes = crucArchRegTypes archFns
   let macawStructRepr = C.StructRepr crucRegTypes
   -- Run the symbolic simulator.
@@ -277,7 +289,7 @@ runCodeBlock sym archFns halloc g regStruct = do
                          , C.simConfig = cfg
                          , C.simHandleAllocator = halloc
                          , C.printHandle = stdout
-                         , C.extensionImpl = macawExtensions
+                         , C.extensionImpl = macawExtensions archEval
                          , C._functionBindings =
                               C.insertHandleMap (C.cfgHandle g) (C.UseCFG g (C.postdomInfo g)) $
                               C.emptyHandleMap
@@ -297,6 +309,7 @@ runBlocks :: forall sym arch ids
            => sym
            -> MacawSymbolicArchFunctions arch
               -- ^ Crucible specific functions.
+           -> MacawArchEvalFn sym arch
            -> M.Memory (M.ArchAddrWidth arch)
               -- ^ Memory image for executable
            -> C.FunctionName
@@ -312,9 +325,9 @@ runBlocks :: forall sym arch ids
                    sym
                    (MacawExt arch)
                    (C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
-runBlocks sym archFns mem nm posFn macawBlocks regStruct = do
+runBlocks sym archFns archEval mem nm posFn macawBlocks regStruct = do
   halloc <- C.newHandleAllocator
   memBaseVarMap <- stToIO $ mkMemBaseVarMap halloc mem
   C.SomeCFG g <- stToIO $ mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks
   -- Run the symbolic simulator.
-  runCodeBlock sym archFns halloc g regStruct
+  runCodeBlock sym archFns archEval halloc g regStruct

x86_symbolic/macaw-x86-symbolic.cabal

@@ -21,7 +21,7 @@ library
   exposed-modules:
     Data.Macaw.X86.Symbolic
 
-  ghc-options: -Wall -Werror
+  ghc-options: -Wall
   ghc-prof-options: -O2 -fprof-auto-top
 
 test-suite macaw-x86-symbolic-tests

x86_symbolic/src/Data/Macaw/X86/Symbolic.hs

@@ -9,6 +9,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 module Data.Macaw.X86.Symbolic
   ( x86_64MacawSymbolicFns
+  , x86_64MacawEvalFn
   ) where
 
 import           Data.Parameterized.Context as Ctx
@@ -22,9 +23,11 @@ import qualified Data.Macaw.X86 as M
 import qualified Data.Macaw.X86.X86Reg as M
 import qualified Flexdis86.Register as F
 
+import qualified Lang.Crucible.CFG.Extension as C
 import qualified Lang.Crucible.CFG.Reg as C
 import qualified Lang.Crucible.Types as C
 import qualified Lang.Crucible.Solver.Symbol as C
+import qualified Lang.Crucible.Solver.Interface as C
 
 ------------------------------------------------------------------------
 -- Utilities for generating a type-level context with repeated elements.
@@ -102,6 +105,12 @@ data X86StmtExtension (f :: C.CrucibleType -> *) (tp :: C.CrucibleType) where
   X86PrimFn :: !(M.X86PrimFn (AtomWrapper f) tp) ->  X86StmtExtension f (ToCrucibleType tp)
 
 
+instance C.PrettyApp X86StmtExtension where
+instance C.TypeApp X86StmtExtension where
+instance FunctorFC X86StmtExtension where
+instance FoldableFC X86StmtExtension where
+instance TraversableFC X86StmtExtension where
+
 type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension
 
 
@@ -126,7 +135,7 @@ crucGenX86TermStmt tstmt regs =
   case tstmt of
     _ -> undefined regs
 
--- | The symbolic tra
+-- | X86_64 specific functions for translation Macaw into Crucible.
 x86_64MacawSymbolicFns :: MacawSymbolicArchFunctions M.X86_64
 x86_64MacawSymbolicFns =
   MacawSymbolicArchFunctions
@@ -137,3 +146,8 @@ x86_64MacawSymbolicFns =
   , crucGenArchStmt = crucGenX86Stmt
   , crucGenArchTermStmt = crucGenX86TermStmt
   }
+
+
+-- | X86_64 specific function for evaluating a Macaw X86_64 program in Crucible.
+x86_64MacawEvalFn :: C.IsSymInterface sym => MacawArchEvalFn sym M.X86_64
+x86_64MacawEvalFn = undefined

x86_symbolic/tests/Main.hs

@@ -114,7 +114,7 @@ main = do
 
   regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)
   putStrLn "Run code block"
-  execResult <- MS.runCodeBlock sym x86ArchFns halloc g regs
+  execResult <- MS.runCodeBlock sym x86ArchFns MX.x86_64MacawEvalFn halloc g regs
   case execResult of
     C.FinishedExecution _ (C.TotalRes _pair) -> do
       putStrLn "Done"