GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-29 11:02:13 +03:00
Code Issues Projects Releases Wiki Activity

x86-symbolic: Add Indexs into MacawCrucibleRegTypes for named registers

Browse Source
This commit is contained in:
Langston Barrett 2024-08-15 16:11:46 -04:00
parent d017106154
commit 97751b0895
2 changed files with 49 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View File

@ -19,11 +19,17 @@ module Data.Macaw.X86.Symbolic
, SymFuns(..), newSymFuns
, X86StmtExtension(..)
, x86RegAssignment
, lookupX86Reg
, updateX86Reg
, freshX86Reg
, RegAssign
, ip
, rax
, rbx
, rcx
, rdx
, getReg
, IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
) where
@ -103,13 +109,28 @@ type X87Tag n = 39 + n -- 8
type FPReg n = 47 + n -- 8
type YMM n = 55 + n -- 16
ip :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
ip = Ctx.extendIndex (Ctx.nextIndex zeroSize)
rax :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rax = Ctx.extendIndex (Ctx.nextIndex (Ctx.size1 @(MM.LLVMPointerType 64)))
rcx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rcx = Ctx.extendIndex (Ctx.nextIndex (Ctx.size2 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))
rdx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rdx = Ctx.extendIndex (Ctx.nextIndex (Ctx.size3 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))
rbx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rbx = Ctx.extendIndex (Ctx.nextIndex (Ctx.size4 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))
getReg ::
forall n t f. (Idx n (ArchRegContext M.X86_64) t) => RegAssign f -> f t
getReg x = x ^. (field @n)
x86RegName' :: M.X86Reg tp -> String
x86RegName' M.X86_IP = "ip"
x86RegName' (M.X86_GP r) = show $ F.reg64No r
x86RegName' (M.X86_GP r) = show r
x86RegName' (M.X86_FlagReg r) = show r
x86RegName' (M.X87_StatusReg r) = show r
x86RegName' M.X87_TopReg = "x87Top"

32
x86_symbolic/tests/Main.hs
View File

@ -33,6 +33,7 @@ import qualified Data.Macaw.Symbolic as MS
import qualified Data.Macaw.Symbolic.Testing as MST
import qualified Data.Macaw.X86 as MX
import Data.Macaw.X86.Symbolic ()
import qualified Data.Macaw.X86.Symbolic as MXS
import qualified What4.Config as WC
import qualified What4.Interface as WI
import qualified What4.ProblemFeatures as WPF
@ -45,6 +46,7 @@ import qualified Lang.Crucible.LLVM.MemModel as LLVM
import qualified What4.FloatMode as W4
import qualified What4.Expr.Builder as W4
import qualified Data.Parameterized.Context as Ctx
-- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
data SaveSMT = SaveSMT Bool
@ -70,6 +72,17 @@ ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
, TTO.Option (Proxy @SaveMacaw)
] : TT.defaultIngredients
getRegName ::
Ctx.Index (MS.MacawCrucibleRegTypes MX.X86_64) t ->
String
getRegName reg =
case Ctx.intIndex (Ctx.indexVal reg) (Ctx.size MXS.x86RegAssignment) of
Just (Some i) ->
let r = MXS.x86RegAssignment Ctx.! i
rName = MS.crucGenArchRegName MXS.x86_64MacawSymbolicFns r
in show rName
Nothing -> error "impossible"
main :: IO ()
main = do
-- These are pass/fail in that the assertions in the "pass" set are true (and
@ -82,11 +95,20 @@ main = do
let passTests mmPreset = TT.testGroup "True assertions" (map (mkSymExTest passRes mmPreset) passTestFilePaths)
let failTests mmPreset = TT.testGroup "False assertions" (map (mkSymExTest failRes mmPreset) failTestFilePaths)
TT.defaultMainWithIngredients ingredients $
TT.testGroup "Binary Tests" $
map (\mmPreset ->
TT.testGroup (MST.describeMemModelPreset mmPreset)
[passTests mmPreset, failTests mmPreset])
[MST.DefaultMemModel, MST.LazyMemModel]
TT.testGroup "macaw-x86-symbolic tests"
[ TT.testGroup "Unit tests"
[ TTH.testCase "ip" $ getRegName MXS.ip TTH.@?= "r!ip"
, TTH.testCase "rax" $ getRegName MXS.rax TTH.@?= "r!rax"
, TTH.testCase "rbx" $ getRegName MXS.rbx TTH.@?= "r!rbx"
, TTH.testCase "rcx" $ getRegName MXS.rcx TTH.@?= "r!rcx"
, TTH.testCase "rdx" $ getRegName MXS.rdx TTH.@?= "r!rdx"
]
, TT.testGroup "Binary tests" $
map (\mmPreset ->
TT.testGroup (MST.describeMemModelPreset mmPreset)
[passTests mmPreset, failTests mmPreset])
[MST.DefaultMemModel, MST.LazyMemModel]
]
hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
hasTestPrefix (Some dfi) = do