Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

macaw-x86-syntax: Syntactic sugar for macaw-x86-symbolic CFGs #422

Merged
merged 9 commits into from
Aug 16, 2024
Merged

macaw-x86-syntax: Syntactic sugar for macaw-x86-symbolic CFGs #422

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
284e1d8
macaw-x86-syntax: Syntactic sugar for macaw-x86-symbolic CFGs
langston-barrett Aug 15, 2024
1d38ffa
macaw-x86-syntax: `get-reg` operation, `rip` register
langston-barrett Aug 15, 2024
f7faf4e
x86-symbolic: Minor cleanup (alphabetization, typo fix)
langston-barrett Aug 15, 2024
4ad8a70
x86-symbolic: Add `Index`s into `MacawCrucibleRegTypes` for named reg…
langston-barrett Aug 15, 2024
d2a304f
x86-syntax: Use upstream register indices
langston-barrett Aug 15, 2024
85c8653
x86-{symbolic,syntax}: `Index`s and names for GP registers
langston-barrett Aug 16, 2024
d023170
x86-symbolic: Comment on register `Index` definitions
langston-barrett Aug 16, 2024
bcfbd90
x86-syntax: `set-reg`
langston-barrett Aug 16, 2024
c1ef172
x86-symbolic: Simplify definitions of `Index`s for named registers
langston-barrett Aug 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions macaw-x86-syntax/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,5 +15,21 @@ This `ParserHooks` supports the following types and operations:
- `get-reg :: X86Reg -> X86Regs -> t`: extract an x86 register
- Registers:
- `rip :: X86Reg`: instruction pointer
- `rax :: X86Reg`: SysV return value register
- `rbx :: X86Reg`: general-purpose register
- `rcx :: X86Reg`: general-purpose register
- `rdx :: X86Reg`: general-purpose register
- `rsp :: X86Reg`: stack pointer
- `rbp :: X86Reg`: base pointer
- `rsi :: X86Reg`: general-purpose register
- `rdi :: X86Reg`: general-purpose register
- `r8 :: X86Reg`: general-purpose register
- `r9 :: X86Reg`: general-purpose register
- `r10 :: X86Reg`: general-purpose register
- `r11 :: X86Reg`: general-purpose register
- `r12 :: X86Reg`: general-purpose register
- `r13 :: X86Reg`: general-purpose register
- `r14 :: X86Reg`: general-purpose register
- `r15 :: X86Reg`: general-purpose register

[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax
18 changes: 17 additions & 1 deletion macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,23 @@ parseReg =
LCSM.describe "an x86_64 register" $ do
name <- LCSC.atomName
case name of
LCSA.AtomName "rip" -> pure (Some X86.ip)
LCSA.AtomName "rip" -> pure (Some X86.rip)
LCSA.AtomName "rax" -> pure (Some X86.rax)
LCSA.AtomName "rbx" -> pure (Some X86.rbx)
LCSA.AtomName "rcx" -> pure (Some X86.rcx)
LCSA.AtomName "rdx" -> pure (Some X86.rdx)
LCSA.AtomName "rsp" -> pure (Some X86.rsp)
LCSA.AtomName "rbp" -> pure (Some X86.rbp)
LCSA.AtomName "rsi" -> pure (Some X86.rsi)
LCSA.AtomName "rdi" -> pure (Some X86.rdi)
LCSA.AtomName "r8" -> pure (Some X86.r8)
LCSA.AtomName "r9" -> pure (Some X86.r9)
LCSA.AtomName "r10" -> pure (Some X86.r10)
LCSA.AtomName "r11" -> pure (Some X86.r11)
LCSA.AtomName "r12" -> pure (Some X86.r12)
LCSA.AtomName "r13" -> pure (Some X86.r13)
LCSA.AtomName "r14" -> pure (Some X86.r14)
LCSA.AtomName "r15" -> pure (Some X86.r15)
LCSA.AtomName _ -> empty

x86AtomParser ::
Expand Down
20 changes: 20 additions & 0 deletions macaw-x86-syntax/test-data/get-regs.cbl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
(defun @id ((regs X86Regs)) X86Regs
(start start:
(let rip (get-reg rip regs))
(let rax (get-reg rax regs))
(let rbx (get-reg rbx regs))
(let rcx (get-reg rcx regs))
(let rdx (get-reg rdx regs))
(let rsp (get-reg rsp regs))
(let rbp (get-reg rbp regs))
(let rsi (get-reg rsi regs))
(let rdi (get-reg rdi regs))
(let r8 (get-reg r8 regs))
(let r9 (get-reg r9 regs))
(let r10 (get-reg r10 regs))
(let r11 (get-reg r11 regs))
(let r12 (get-reg r12 regs))
(let r13 (get-reg r13 regs))
(let r14 (get-reg r14 regs))
(let r15 (get-reg r15 regs))
(return regs)))
60 changes: 60 additions & 0 deletions macaw-x86-syntax/test-data/get-regs.out.good
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
(defun @id ((regs X86Regs)) X86Regs
(start start:
(let rip (get-reg rip regs))
(let rax (get-reg rax regs))
(let rbx (get-reg rbx regs))
(let rcx (get-reg rcx regs))
(let rdx (get-reg rdx regs))
(let rsp (get-reg rsp regs))
(let rbp (get-reg rbp regs))
(let rsi (get-reg rsi regs))
(let rdi (get-reg rdi regs))
(let r8 (get-reg r8 regs))
(let r9 (get-reg r9 regs))
(let r10 (get-reg r10 regs))
(let r11 (get-reg r11 regs))
(let r12 (get-reg r12 regs))
(let r13 (get-reg r13 regs))
(let r14 (get-reg r14 regs))
(let r15 (get-reg r15 regs))
(return regs)))

id
%0
% 3:14
$1 = getStruct($0, 0, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 4:14
$2 = getStruct($0, 1, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 5:14
$3 = getStruct($0, 4, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 6:14
$4 = getStruct($0, 2, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 7:14
$5 = getStruct($0, 3, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 8:14
$6 = getStruct($0, 5, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 9:14
$7 = getStruct($0, 6, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 10:14
$8 = getStruct($0, 7, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 11:14
$9 = getStruct($0, 8, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 12:13
$10 = getStruct($0, 9, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 13:13
$11 = getStruct($0, 10, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 14:14
$12 = getStruct($0, 11, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 15:14
$13 = getStruct($0, 12, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 16:14
$14 = getStruct($0, 13, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 17:14
$15 = getStruct($0, 14, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 18:14
$16 = getStruct($0, 15, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 19:14
$17 = getStruct($0, 16, IntrinsicRepr LLVM_pointer [BVRepr 64])
% 20:5
return $0
% no postdom
58 changes: 55 additions & 3 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,23 @@ module Data.Macaw.X86.Symbolic
, freshX86Reg

, RegAssign
, ip
, rip
, rax
, rbx
, rcx
, rdx
, rsp
, rbp
, rsi
, rdi
, r8
, r9
, r10
, r11
, r12
, r13
, r14
, r15
, getReg
, IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
) where
Expand Down Expand Up @@ -109,8 +121,12 @@ 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)
-- The following definitions are tightly coupled to that of ArchRegContext for
-- X86_64. Unit tests in the test suite ensure that they are consistent with
-- x86RegAssignment (below).

rip :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rip = 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)))
Expand All @@ -124,6 +140,42 @@ rdx = Ctx.extendIndex (Ctx.nextIndex (Ctx.size3 @(MM.LLVMPointerType 64) @(MM.LL
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)))

rsp :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rsp = Ctx.extendIndex (Ctx.nextIndex (Ctx.size5 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))

rbp :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rbp = Ctx.extendIndex (Ctx.nextIndex (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))

rsi :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rsi = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64))))

rdi :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
rdi = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))))

r8 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r8 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64))))))

r9 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r9 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))))))

r10 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r10 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64))))))))

r11 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r11 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))))))))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

r12 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r12 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64))))))))))

r13 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r13 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64)))))))))))

r14 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r14 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64))))))))))))

r15 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
r15 = Ctx.extendIndex (Ctx.nextIndex (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.incSize @_ @(MM.LLVMPointerType 64) (Ctx.size6 @(MM.LLVMPointerType 64) @(MM.LLVMPointerType 64) @(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)
Expand Down
14 changes: 13 additions & 1 deletion x86_symbolic/tests/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,11 +97,23 @@ main = do
TT.defaultMainWithIngredients ingredients $
TT.testGroup "macaw-x86-symbolic tests"
[ TT.testGroup "Unit tests"
[ TTH.testCase "ip" $ getRegName MXS.ip TTH.@?= "r!ip"
[ TTH.testCase "ip" $ getRegName MXS.rip 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"
, TTH.testCase "rsp" $ getRegName MXS.rsp TTH.@?= "r!rsp"
, TTH.testCase "rbp" $ getRegName MXS.rbp TTH.@?= "r!rbp"
, TTH.testCase "rsi" $ getRegName MXS.rsi TTH.@?= "r!rsi"
, TTH.testCase "rdi" $ getRegName MXS.rdi TTH.@?= "r!rdi"
, TTH.testCase "r8" $ getRegName MXS.r8 TTH.@?= "r!r8"
, TTH.testCase "r9" $ getRegName MXS.r9 TTH.@?= "r!r9"
, TTH.testCase "r10" $ getRegName MXS.r10 TTH.@?= "r!r10"
, TTH.testCase "r11" $ getRegName MXS.r11 TTH.@?= "r!r11"
, TTH.testCase "r12" $ getRegName MXS.r12 TTH.@?= "r!r12"
, TTH.testCase "r13" $ getRegName MXS.r13 TTH.@?= "r!r13"
, TTH.testCase "r14" $ getRegName MXS.r14 TTH.@?= "r!r14"
, TTH.testCase "r15" $ getRegName MXS.r15 TTH.@?= "r!r15"
]
, TT.testGroup "Binary tests" $
map (\mmPreset ->
Expand Down