Add support for FSBASE and GSBASE registers on x86_64

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs

@@ -68,7 +68,7 @@ aarch32RegName r = WS.safeSymbol ("r!" ++ show (MC.prettyF r))
 aarch32MacawEvalFn :: (CB.IsSymInterface sym)
                    => AF.SymFuns sym
                    -> MS.MacawArchEvalFn sym mem SA.AArch32
-aarch32MacawEvalFn fs = MSB.MacawArchEvalFn $ \_ _ xt s ->
+aarch32MacawEvalFn fs = MSB.MacawArchEvalFn $ \_ _ _ xt s ->
   case xt of
     AArch32PrimFn p -> AF.funcSemantics fs p s
     AArch32PrimStmt p -> AF.stmtSemantics fs p s

macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs

@@ -120,7 +120,7 @@ ppcMacawEvalFn :: ( C.IsSymInterface sym
                   )
                => F.SymFuns sym
                -> MS.MacawArchEvalFn sym mem (SP.AnyPPC v)
-ppcMacawEvalFn fs = MSB.MacawArchEvalFn $ \_ _ xt s -> case xt of
+ppcMacawEvalFn fs = MSB.MacawArchEvalFn $ \_ _ _ xt s -> case xt of
   PPCPrimFn fn -> F.funcSemantics fs fn s
   PPCPrimStmt stmt -> F.stmtSemantics fs stmt s
   PPCPrimTerm term -> F.termSemantics fs term s

refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs

@@ -490,8 +490,9 @@ initializeSimulator ctx sym archVals halloc cfg entryBlock = MS.withArchEval arc
   let globalMappingFn = MS.mapRegionPointers memPtrTable
   let lookupHdl = MS.unsupportedFunctionCalls "macaw-refinement"
   let lookupSyscall = MS.unsupportedSyscalls "macaw-refinement"
+  let lookupSegmentBase = MS.unsupportedSegmentBasePointers "macaw-refinement"
   let mkPtrPred = MS.mkGlobalPointerValidityPred memPtrTable
-  let ext = MS.macawExtensions archEvalFns memVar globalMappingFn lookupHdl lookupSyscall mkPtrPred
+  let ext = MS.macawExtensions archEvalFns memVar globalMappingFn lookupHdl lookupSyscall mkPtrPred lookupSegmentBase
   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

symbolic/src/Data/Macaw/Symbolic.hs

@@ -130,6 +130,8 @@ module Data.Macaw.Symbolic
   , MO.LookupFunctionHandle(..)
   , unsupportedSyscalls
   , MO.LookupSyscallHandle(..)
+  , unsupportedSegmentBasePointers
+  , MO.LookupSegmentBasePointer(..)
   , MO.MacawSimulatorState(..)
   , MkGlobalPointerValidityAssertion
   , PointerUse(..)
@@ -1141,6 +1143,19 @@ unsupportedSyscalls
 unsupportedSyscalls compName =
   MO.LookupSyscallHandle $ \_ _ _ _ -> error ("Symbolically executing system calls is not supported in " ++ compName)
 
+-- | A default 'MO.LookupSegmentBasePointer' that raises an error if it is
+-- invoked
+--
+-- Some applications may not need to support segment base pointers (e.g., if
+-- the arctecture doesn't support them).  This is a reasonable handler that
+-- raises an error if it encounters an access to a segment base pointer.
+unsupportedSegmentBasePointers
+  :: String
+  -- ^ The name of the component providing the handler
+  -> MO.LookupSegmentBasePointer sym arch
+unsupportedSegmentBasePointers compName =
+  MO.LookupSegmentBasePointer $ \_ -> error ("Symbolically accessing segment base pointers is not supported in " ++ compName)
+
 -- | This evaluates a Macaw statement extension in the simulator.
 execMacawStmtExtension
   :: forall sym arch
@@ -1159,8 +1174,10 @@ execMacawStmtExtension
   -- should be invoked; returns the function handle to invoke
   -> MkGlobalPointerValidityAssertion sym (M.ArchAddrWidth arch)
   -- ^ A function to make memory validity predicates (see 'MkGlobalPointerValidityAssertion' for details)
+  -> MO.LookupSegmentBasePointer sym arch
+  -- ^ A function to return the appropriate segment base pointer when a segment base register is read.
   -> SB.MacawEvalStmtFunc (MacawStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
-execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunctionHandle lookupH) (MO.LookupSyscallHandle lookupSyscall) toMemPred s0 st =
+execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunctionHandle lookupH) (MO.LookupSyscallHandle lookupSyscall) toMemPred lookupSegmentBase s0 st =
   case s0 of
     MacawReadMem addrWidth memRep ptr0 -> do
       let sym = st^.C.stateSymInterface
@@ -1227,7 +1244,7 @@ execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunc
       (hv, st') <- lookupSyscall argReprs retRepr st argStruct
       return (C.HandleFnVal hv, st')
 
-    MacawArchStmtExtension s    -> archStmtFn mvar globs s st
+    MacawArchStmtExtension s    -> archStmtFn mvar globs lookupSegmentBase s st
     MacawArchStateUpdate {}     -> return ((), st)
     MacawInstructionStart {}    -> return ((), st)
 
@@ -1259,10 +1276,12 @@ macawExtensions
   -- should be invoked; returns the function handle to invoke
   -> MkGlobalPointerValidityAssertion sym (M.ArchAddrWidth arch)
   -- ^ A function to make memory validity predicates (see 'MkGlobalPointerValidityAssertion' for details)
+  -> MO.LookupSegmentBasePointer sym arch
+  -- ^ A function to return the appropriate segment base pointer when a segment base register is read.
   -> C.ExtensionImpl (MacawSimulatorState sym) sym (MacawExt arch)
-macawExtensions f mvar globs lookupH lookupSyscall toMemPred =
+macawExtensions f mvar globs lookupH lookupSyscall toMemPred lookupSegmentBase =
   C.ExtensionImpl { C.extensionEval = evalMacawExprExtension
-                  , C.extensionExec = execMacawStmtExtension f mvar globs lookupH lookupSyscall toMemPred
+                  , C.extensionExec = execMacawStmtExtension f mvar globs lookupH lookupSyscall toMemPred lookupSegmentBase
                   }
 
 -- | Run the simulator over a contiguous set of code.
@@ -1282,13 +1301,14 @@ runCodeBlock
   -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
   -> Ctx.Assignment (C.RegValue' sym) (MacawCrucibleRegTypes arch)
   -- ^ Register assignment
+  -> MO.LookupSegmentBasePointer sym arch
   -> IO ( C.GlobalVar MM.Mem
         , C.ExecResult
           (MacawSimulatorState sym)
           sym
           (MacawExt arch)
           (C.RegEntry sym (ArchRegStruct arch)))
-runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH lookupSyscall toMemPred g regStruct = do
+runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH lookupSyscall toMemPred g regStruct lookupSegmentBase = do
   mvar <- MM.mkMemVar "macaw:codeblock_llvm_memory" halloc
   let crucRegTypes = crucArchRegTypes archFns
   let macawStructRepr = C.StructRepr crucRegTypes
@@ -1297,7 +1317,7 @@ runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH lookupSyscall t
       ctx = let fnBindings = C.insertHandleMap (C.cfgHandle g)
                              (C.UseCFG g (C.postdomInfo g)) $
                              C.emptyHandleMap
-                extImpl = macawExtensions archEval mvar globs lookupH lookupSyscall toMemPred
+                extImpl = macawExtensions archEval mvar globs lookupH lookupSyscall toMemPred lookupSegmentBase
             in C.initSimContext sym llvmIntrinsicTypes halloc stdout
                (C.FnBindings fnBindings) extImpl MacawSimulatorState
   -- Create the symbolic simulator state

symbolic/src/Data/Macaw/Symbolic/Backend.hs

@@ -74,6 +74,7 @@ type MacawEvalStmtFunc f p sym ext =
 newtype MacawArchEvalFn sym mem arch =
   MacawArchEvalFn (C.GlobalVar mem
                   -> MO.GlobalMap sym mem (M.ArchAddrWidth arch)
+                  -> MO.LookupSegmentBasePointer sym arch
                   -> MacawEvalStmtFunc (CG.MacawArchStmtExtension arch)
                                        (MO.MacawSimulatorState sym)
                                        sym

symbolic/src/Data/Macaw/Symbolic/MemOps.hs

@@ -35,6 +35,7 @@ module Data.Macaw.Symbolic.MemOps
   , MacawSimulatorState(..)
   , LookupFunctionHandle(..)
   , LookupSyscallHandle(..)
+  , LookupSegmentBasePointer(..)
   , ptrOp
   , isValidPtr
   , mkUndefinedBool
@@ -365,6 +366,17 @@ newtype LookupSyscallHandle sym arch =
                       -> IO (C.FnHandle atps (StructType rtps), CrucibleState (MacawSimulatorState sym) sym (MacawExt arch) rtp blocks r ctx)
                       )
 
+-- | A function to inspect an ArchFn fetching a segment base pointer and return
+-- the appropriate segment base pointer.
+--
+-- This can be used for architectures that emulate segmented memory through
+-- special registers containing pointers to memory regions in the flat address
+-- space (e.g., FSBASE and GSBASE in x86).
+newtype LookupSegmentBasePointer sym arch =
+  LookupSegmentBasePointer (  forall v tp
+                           .  M.ArchFn arch v tp
+                           -> LLVMPtr sym (M.ArchAddrWidth arch))
+
 --------------------------------------------------------------------------------
 doLookupFunctionHandle :: (IsSymInterface sym)
                        => (CrucibleState s sym ext trp blocks r ctx -> MemImpl sym -> regs -> IO (a, CrucibleState s sym ext trp blocks r ctx))

symbolic/src/Data/Macaw/Symbolic/Testing.hs

@@ -332,7 +332,7 @@ simulateFunction sym execFeatures archVals halloc initMem globalMap g = do
 
   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 lookupSyscall validityCheck
+    let extImpl = MS.macawExtensions archEvalFn memVar globalMap lookupFunction lookupSyscall validityCheck lookupSegmentBase
     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
@@ -397,6 +397,12 @@ lookupFunction = MS.unsupportedFunctionCalls "macaw-symbolic-tests"
 lookupSyscall :: MS.LookupSyscallHandle sym arch
 lookupSyscall = MS.unsupportedSyscalls "macaw-symbolic-tests"
 
+-- | The test harness does not currently support accesses to segment base registers from test cases.
+--
+-- It could be modified to do so.
+lookupSegmentBase :: MS.LookupSegmentBasePointer sym arch
+lookupSegmentBase = MS.unsupportedSegmentBasePointers "macaw-symbolic-tests"
+
 -- | 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.

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

@@ -93,13 +93,15 @@ funcSemantics
   => SymFuns sym
   -> M.X86PrimFn (AtomWrapper (RegEntry sym)) mt
   -> S sym rtp bs r ctx
+  -> LookupSegmentBasePointer sym M.X86_64
   -> IO (RegValue sym t, S sym rtp bs r ctx)
-funcSemantics fs x s = do let sym = Sym { symIface = s^.stateSymInterface
-                                        , symTys   = s^.stateIntrinsicTypes
-                                        , symFuns  = fs
-                                        }
-                          v <- pureSem sym x
-                          return (v,s)
+funcSemantics fs x s lookupSegmentBase = do
+  let sym = Sym { symIface = s^.stateSymInterface
+                , symTys   = s^.stateIntrinsicTypes
+                , symFuns  = fs
+                }
+  v <- pureSem sym x lookupSegmentBase
+  return (v,s)
 
 withConcreteCountAndDir
   :: (IsSymInterface sym, 1 <= w)
@@ -336,16 +338,18 @@ pureSem :: forall sym mt
         .  IsSymInterface sym
         => Sym sym   {- ^ Handle to the simulator -}
         -> M.X86PrimFn (AtomWrapper (RegEntry sym)) mt {- ^ Instruction -}
+        -> LookupSegmentBasePointer sym M.X86_64
+        -- ^ Handler for 'ReadFSBase' and 'ReadGSBase'
         -> IO (RegValue sym (ToCrucibleType mt)) -- ^ Resulting value
-pureSem sym fn = do
+pureSem sym fn (LookupSegmentBasePointer lookupSegmentBase) = do
   let symi = (symIface sym)
   case fn of
     M.EvenParity x0 ->
       do x <- getBitVal (symIface sym) x0
          evalE sym $ app $ Not $ foldr1 xor [ bvTestBit x i | i <- [ 0 .. 7 ] ]
       where xor a b = app (BoolXor a b)
-    M.ReadFSBase    -> error " ReadFSBase"
-    M.ReadGSBase    -> error "ReadGSBase"
+    M.ReadFSBase    -> return (lookupSegmentBase fn)
+    M.ReadGSBase    -> return (lookupSegmentBase fn)
     M.GetSegmentSelector _ -> error "GetSegmentSelector"
     M.CPUID{}       -> error "CPUID"
     M.CMPXCHG8B{} -> error "CMPXCHG8B"

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

@@ -342,9 +342,9 @@ x86_64MacawEvalFn
   => SymFuns sym
   -> MacawArchEvalFn sym MM.Mem M.X86_64
 x86_64MacawEvalFn fs =
-  MacawArchEvalFn $ \global_var_mem globals ext_stmt crux_state ->
+  MacawArchEvalFn $ \global_var_mem globals lookupSegmentBase ext_stmt crux_state ->
     case ext_stmt of
-      X86PrimFn x -> funcSemantics fs x crux_state
+      X86PrimFn x -> funcSemantics fs x crux_state lookupSegmentBase
       X86PrimStmt stmt -> stmtSemantics fs global_var_mem globals stmt crux_state
       X86PrimTerm term -> termSemantics fs term crux_state