Skip to content

Commit

Permalink
x86-symbolic: Remove terse register names from top-level exports
Browse files Browse the repository at this point in the history 
These names are so short that they might conflict with local names in
files that import this module. Instead, export them from `Regs` and
encourage qualified use of that module.
  • Loading branch information
Your Name committed Sep 24, 2024
1 parent a022c2b commit 896d35c
Show file tree
Hide file tree
Showing 5 changed files with 69 additions and 66 deletions.
35 changes: 18 additions & 17 deletions macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ import Data.Text qualified as Text
import Data.Macaw.Symbolic qualified as DMS
import Data.Macaw.X86 qualified as X86
import Data.Macaw.X86.Symbolic qualified as X86
import Data.Macaw.X86.Symbolic.Regs qualified as X86R
import Data.Parameterized.Context qualified as Ctx
import Data.Parameterized.Some (Some(..))
import Lang.Crucible.CFG.Expr as Expr
Expand Down Expand Up @@ -93,23 +94,23 @@ parseReg =
LCSM.describe "an x86_64 register" $ do
name <- LCSC.atomName
case name of
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 "rip" -> pure (Some X86R.rip)
LCSA.AtomName "rax" -> pure (Some X86R.rax)
LCSA.AtomName "rbx" -> pure (Some X86R.rbx)
LCSA.AtomName "rcx" -> pure (Some X86R.rcx)
LCSA.AtomName "rdx" -> pure (Some X86R.rdx)
LCSA.AtomName "rsp" -> pure (Some X86R.rsp)
LCSA.AtomName "rbp" -> pure (Some X86R.rbp)
LCSA.AtomName "rsi" -> pure (Some X86R.rsi)
LCSA.AtomName "rdi" -> pure (Some X86R.rdi)
LCSA.AtomName "r8" -> pure (Some X86R.r8)
LCSA.AtomName "r9" -> pure (Some X86R.r9)
LCSA.AtomName "r10" -> pure (Some X86R.r10)
LCSA.AtomName "r11" -> pure (Some X86R.r11)
LCSA.AtomName "r12" -> pure (Some X86R.r12)
LCSA.AtomName "r13" -> pure (Some X86R.r13)
LCSA.AtomName "r14" -> pure (Some X86R.r14)
LCSA.AtomName "r15" -> pure (Some X86R.r15)
LCSA.AtomName _ -> empty

x86AtomParser ::
Expand Down
8 changes: 0 additions & 8 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,14 +27,6 @@ module Data.Macaw.X86.Symbolic
, RegAssign
, getReg
, IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
, Rip, Rax, Rcx, Rdx, Rbx, Rsp, Rbp, Rsi, Rdi
, R8, R9, R10, R11, R12, R13, R14, R15
, CF, PF, AF, ZF, SF, TF, IF, DF, OF
, IE, DE, ZE, OE, UE, PE, EF, ES, C0, C1, C2, C3
, rip, rax, rbx, rcx, rdx, rsp, rbp, rsi, rdi
, r8, r9, r10, r11, r12, r13, r14, r15
, cf, pf, af, zf, sf, tf, if_, df, of_
, ie, de, ze, oe, ue, pe, ef, es, c0, c1, c2, c3
) where

import Control.Monad ( void )
Expand Down
6 changes: 3 additions & 3 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ import Data.Coerce (coerce)
import Data.Macaw.Symbolic qualified as MS
import Data.Macaw.Symbolic.Stack qualified as MSS
import Data.Macaw.X86 qualified as X86
import Data.Macaw.X86.Symbolic qualified as X86S
import Data.Macaw.X86.Symbolic.Regs qualified as X86SR
import Data.Parameterized.Classes (ixF')
import Data.Parameterized.Context qualified as Ctx
import Data.Sequence qualified as Seq
Expand Down Expand Up @@ -109,8 +109,8 @@ stackPointerReg ::
(StackPointer sym)
stackPointerReg =
Lens.lens
(\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86S.rsp)))
(\regs v -> regs Lens.& ixF' X86S.rsp Lens..~ C.RV (getStackPointer v))
(\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86SR.rsp)))
(\regs v -> regs Lens.& ixF' X86SR.rsp Lens..~ C.RV (getStackPointer v))

-- | A return address
newtype RetAddr sym = RetAddr { getRetAddr :: MM.LLVMPtr sym 64 }
Expand Down
9 changes: 9 additions & 0 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic/Regs.hs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,12 @@
{-|
Copyright : (c) Galois, Inc 2024
Maintainer : Langston Barrett <[email protected]>
x86_64 registers.
This module is meant to be imported qualified, as it exports many terse names.
-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
Expand Down
77 changes: 39 additions & 38 deletions x86_symbolic/tests/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ 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 Data.Macaw.X86.Symbolic.Regs as MXSR
import qualified Data.Macaw.X86.Symbolic.ABI.SysV as SysV
import qualified What4.Config as WC
import qualified What4.Expr.Builder as W4
Expand Down Expand Up @@ -103,44 +104,44 @@ main = do
TT.defaultMainWithIngredients ingredients $
TT.testGroup "macaw-x86-symbolic tests"
[ TT.testGroup "Unit tests"
[ 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"
, TTH.testCase "cf" $ getRegName MXS.cf TTH.@?= "r!cf"
, TTH.testCase "pf" $ getRegName MXS.pf TTH.@?= "r!pf"
, TTH.testCase "af" $ getRegName MXS.af TTH.@?= "r!af"
, TTH.testCase "zf" $ getRegName MXS.zf TTH.@?= "r!zf"
, TTH.testCase "sf" $ getRegName MXS.sf TTH.@?= "r!sf"
, TTH.testCase "tf" $ getRegName MXS.tf TTH.@?= "r!tf"
, TTH.testCase "if" $ getRegName MXS.if_ TTH.@?= "r!if"
, TTH.testCase "df" $ getRegName MXS.df TTH.@?= "r!df"
, TTH.testCase "of" $ getRegName MXS.of_ TTH.@?= "r!of"
, TTH.testCase "ie" $ getRegName MXS.ie TTH.@?= "r!ie"
, TTH.testCase "de" $ getRegName MXS.de TTH.@?= "r!de"
, TTH.testCase "ze" $ getRegName MXS.ze TTH.@?= "r!ze"
, TTH.testCase "oe" $ getRegName MXS.oe TTH.@?= "r!oe"
, TTH.testCase "ue" $ getRegName MXS.ue TTH.@?= "r!ue"
, TTH.testCase "pe" $ getRegName MXS.pe TTH.@?= "r!pe"
, TTH.testCase "ef" $ getRegName MXS.ef TTH.@?= "r!ef"
, TTH.testCase "es" $ getRegName MXS.es TTH.@?= "r!es"
, TTH.testCase "c0" $ getRegName MXS.c0 TTH.@?= "r!c0"
, TTH.testCase "c1" $ getRegName MXS.c1 TTH.@?= "r!c1"
, TTH.testCase "c2" $ getRegName MXS.c2 TTH.@?= "r!c2"
, TTH.testCase "c3" $ getRegName MXS.c3 TTH.@?= "r!c3"
[ TTH.testCase "ip" $ getRegName MXSR.rip TTH.@?= "r!ip"
, TTH.testCase "rax" $ getRegName MXSR.rax TTH.@?= "r!rax"
, TTH.testCase "rbx" $ getRegName MXSR.rbx TTH.@?= "r!rbx"
, TTH.testCase "rcx" $ getRegName MXSR.rcx TTH.@?= "r!rcx"
, TTH.testCase "rdx" $ getRegName MXSR.rdx TTH.@?= "r!rdx"
, TTH.testCase "rsp" $ getRegName MXSR.rsp TTH.@?= "r!rsp"
, TTH.testCase "rbp" $ getRegName MXSR.rbp TTH.@?= "r!rbp"
, TTH.testCase "rsi" $ getRegName MXSR.rsi TTH.@?= "r!rsi"
, TTH.testCase "rdi" $ getRegName MXSR.rdi TTH.@?= "r!rdi"
, TTH.testCase "r8" $ getRegName MXSR.r8 TTH.@?= "r!r8"
, TTH.testCase "r9" $ getRegName MXSR.r9 TTH.@?= "r!r9"
, TTH.testCase "r10" $ getRegName MXSR.r10 TTH.@?= "r!r10"
, TTH.testCase "r11" $ getRegName MXSR.r11 TTH.@?= "r!r11"
, TTH.testCase "r12" $ getRegName MXSR.r12 TTH.@?= "r!r12"
, TTH.testCase "r13" $ getRegName MXSR.r13 TTH.@?= "r!r13"
, TTH.testCase "r14" $ getRegName MXSR.r14 TTH.@?= "r!r14"
, TTH.testCase "r15" $ getRegName MXSR.r15 TTH.@?= "r!r15"
, TTH.testCase "cf" $ getRegName MXSR.cf TTH.@?= "r!cf"
, TTH.testCase "pf" $ getRegName MXSR.pf TTH.@?= "r!pf"
, TTH.testCase "af" $ getRegName MXSR.af TTH.@?= "r!af"
, TTH.testCase "zf" $ getRegName MXSR.zf TTH.@?= "r!zf"
, TTH.testCase "sf" $ getRegName MXSR.sf TTH.@?= "r!sf"
, TTH.testCase "tf" $ getRegName MXSR.tf TTH.@?= "r!tf"
, TTH.testCase "if" $ getRegName MXSR.if_ TTH.@?= "r!if"
, TTH.testCase "df" $ getRegName MXSR.df TTH.@?= "r!df"
, TTH.testCase "of" $ getRegName MXSR.of_ TTH.@?= "r!of"
, TTH.testCase "ie" $ getRegName MXSR.ie TTH.@?= "r!ie"
, TTH.testCase "de" $ getRegName MXSR.de TTH.@?= "r!de"
, TTH.testCase "ze" $ getRegName MXSR.ze TTH.@?= "r!ze"
, TTH.testCase "oe" $ getRegName MXSR.oe TTH.@?= "r!oe"
, TTH.testCase "ue" $ getRegName MXSR.ue TTH.@?= "r!ue"
, TTH.testCase "pe" $ getRegName MXSR.pe TTH.@?= "r!pe"
, TTH.testCase "ef" $ getRegName MXSR.ef TTH.@?= "r!ef"
, TTH.testCase "es" $ getRegName MXSR.es TTH.@?= "r!es"
, TTH.testCase "c0" $ getRegName MXSR.c0 TTH.@?= "r!c0"
, TTH.testCase "c1" $ getRegName MXSR.c1 TTH.@?= "r!c1"
, TTH.testCase "c2" $ getRegName MXSR.c2 TTH.@?= "r!c2"
, TTH.testCase "c3" $ getRegName MXSR.c3 TTH.@?= "r!c3"
]
, TT.testGroup "Binary tests" $
map (\mmPreset ->
Expand Down

0 comments on commit 896d35c

Please sign in to comment.