Merge pull request #55 from GaloisInc/macaw-T374

Bump `macaw` submodule to bring in GaloisInc/macaw#465 changes
GaloisInc · Feb 18, 2025 · 2aadaaf · 2aadaaf
2 parents 37d2159 + c1fcd2f
commit 2aadaaf
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 35 deletions.
diff --git a/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs b/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs
@@ -35,7 +35,6 @@ import qualified Data.Macaw.ARM.ARMReg as ARMReg
 import qualified Data.Macaw.Memory as DMM
 import qualified Data.Macaw.Symbolic as DMS
 import qualified Data.Macaw.Types as DMT
-import qualified Language.ASL.Globals as ASL
 import qualified Lang.Crucible.Backend as LCB
 import qualified Lang.Crucible.Backend.Online as LCBO
 import qualified Lang.Crucible.CFG.Common as LCCC
@@ -97,10 +96,10 @@ aarch32LinuxIntegerArguments bak archVals argTypes regFile mem = do
 
 aarch32LinuxIntegerArgumentRegisters :: [ARMReg.ARMReg (DMT.BVType 32)]
 aarch32LinuxIntegerArgumentRegisters =
-  [ ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R0")
-  , ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R1")
-  , ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R2")
-  , ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R3")
+  [ ARMReg.r0
+  , ARMReg.r1
+  , ARMReg.r2
+  , ARMReg.r3
   ]
 
 -- | Inject override return values back into the register state
@@ -125,16 +124,14 @@ aarch32LinuxIntegerReturnRegisters bak _archVals ovTy result initRegs =
     -- though we are computing two return values, one in R0 and the other in R1.
     LCT.StructRepr (Ctx.Empty Ctx.:> fstTpr Ctx.:> sndTpr) -> do
       Ctx.Empty Ctx.:> LCS.RV fstVal Ctx.:> LCS.RV sndVal <- pure (AF.result result)
-      regs0 <- injectIntoReg fstTpr fstVal r0 initRegs
-      regs1 <- injectIntoReg sndTpr sndVal r1 regs0
+      regs0 <- injectIntoReg fstTpr fstVal ARMReg.r0 initRegs
+      regs1 <- injectIntoReg sndTpr sndVal ARMReg.r1 regs0
       pure $ updateRegs regs1 (AF.regUpdates result)
     _ -> do
-      regs' <- injectIntoReg ovTy (AF.result result) r0 initRegs
+      regs' <- injectIntoReg ovTy (AF.result result) ARMReg.r0 initRegs
       pure $ updateRegs regs' (AF.regUpdates result)
   where
     sym = LCB.backendGetSym bak
-    r0 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R0")
-    r1 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R1")
 
     -- Inject a return value of the given TypeRepr into the supplied ARMReg.
     -- Depending on the type of the value, this may require zero extension.
@@ -196,7 +193,7 @@ aarch32LinuxReturnAddr ::
   -> IO (Maybe (DMM.MemWord 32))
 aarch32LinuxReturnAddr bak archVals regs _mem = do
   let addrSymBV = LCLMP.llvmPointerOffset $ LCS.regValue
-                                          $ DMS.lookupReg archVals regsEntry ARMReg.arm_LR
+                                          $ DMS.lookupReg archVals regsEntry ARMReg.lr
   res <- AVC.resolveSymBVAs bak WT.knownNat addrSymBV
   case res of
     Left AVC.UnsatInitialAssumptions -> do

diff --git a/stubs-common/src/Stubs/Syscall/AArch32/Linux.hs b/stubs-common/src/Stubs/Syscall/AArch32/Linux.hs
@@ -25,7 +25,6 @@ import qualified Data.Macaw.ARM as DMA
 import qualified Data.Macaw.ARM.ARMReg as ARMReg
 import qualified Data.Macaw.CFG as DMC
 import qualified Data.Macaw.Types as DMT
-import qualified Language.ASL.Globals as ASL
 import qualified Lang.Crucible.Backend as LCB
 import qualified Lang.Crucible.LLVM.MemModel as LCLM
 import qualified Lang.Crucible.Simulator as LCS
@@ -76,18 +75,16 @@ aarch32LinuxGetReg
 aarch32LinuxGetReg tps regs reg
   | Just PC.Refl <- PC.testEquality tps syscallABIRepr =
       case LCS.regValue regs of
-        Ctx.Empty Ctx.:> r0 Ctx.:> r1 Ctx.:> r2 Ctx.:> r3 Ctx.:> r4 Ctx.:> r5 Ctx.:> r6 Ctx.:> r7 ->
-          case reg of
-            ARMReg.ARMGlobalBV ref
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R0") -> r0
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R1") -> r1
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R2") -> r2
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R3") -> r3
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R4") -> r4
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R5") -> r5
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R6") -> r6
-              | Just PC.Refl <- PC.testEquality ref (ASL.knownGlobalRef @"_R7") -> r7
-            _ -> AP.panic AP.Syscall "aarch32LinuxGetReg" ["Unexpected syscall register: " ++ show reg]
+        Ctx.Empty Ctx.:> r0 Ctx.:> r1 Ctx.:> r2 Ctx.:> r3 Ctx.:> r4 Ctx.:> r5 Ctx.:> r6 Ctx.:> r7
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r0 -> r0
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r1 -> r1
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r2 -> r2
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r3 -> r3
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r4 -> r4
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r5 -> r5
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r6 -> r6
+          | Just PC.Refl <- PC.testEquality reg ARMReg.r7 -> r7
+        _ -> AP.panic AP.Syscall "aarch32LinuxGetReg" ["Unexpected syscall register: " ++ show reg]
   | otherwise = AP.panic AP.Syscall "aarch32LinuxGetReg" [ "Unexpected syscall args shape"
                                                          , " Expected: " ++ show syscallABIRepr
                                                          , " But got: " ++ show tps
@@ -105,12 +102,10 @@ aarch32LinuxSyscallNumberRegister
   -> LCS.RegEntry sym (LCT.StructType atps)
   -> IO (LCS.RegEntry sym (LCT.BVType w))
 aarch32LinuxSyscallNumberRegister bak repr regs = do
-  bv <- LCLM.projectLLVM_bv bak (LCS.unRV (aarch32LinuxGetReg repr regs r7))
+  bv <- LCLM.projectLLVM_bv bak (LCS.unRV (aarch32LinuxGetReg repr regs ARMReg.r7))
   return LCS.RegEntry { LCS.regType = LCT.BVRepr PN.knownNat
                       , LCS.regValue = bv
                       }
-  where
-    r7 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R7")
 
 -- | Syscall arguments are passed in (in order): r0, r1, r2, r3, r4, r5, r6
 --
@@ -158,13 +153,13 @@ aarch32LinuxSyscallReturnRegisters ovTy ovSim argsRepr args retRepr
       case ovTy of
         LCT.UnitRepr -> do
           ovSim
-          let r0Val = aarch32LinuxGetReg argsRepr args r0
-          let r1Val = aarch32LinuxGetReg argsRepr args r1
+          let r0Val = aarch32LinuxGetReg argsRepr args ARMReg.r0
+          let r1Val = aarch32LinuxGetReg argsRepr args ARMReg.r1
           return (Ctx.Empty Ctx.:> r0Val Ctx.:> r1Val)
         LCLM.LLVMPointerRepr w
           | Just PC.Refl <- PC.testEquality w ptrWidth -> do
               result <- ovSim
-              let r1Val = aarch32LinuxGetReg argsRepr args r1
+              let r1Val = aarch32LinuxGetReg argsRepr args ARMReg.r1
               return (Ctx.Empty Ctx.:> LCS.RV result Ctx.:> r1Val)
         _ -> AP.panic AP.Syscall "aarch32LinuxSyscallReturnRegisters" [ "Unexpected override return type: " ++ show ovTy ]
   | otherwise = AP.panic AP.Syscall "aarch32LinuxSyscallReturnRegisters" [ "Unexpected return shape"
@@ -173,8 +168,6 @@ aarch32LinuxSyscallReturnRegisters ovTy ovSim argsRepr args retRepr
                                                                          ]
   where
     ptrWidth = PN.knownNat @32
-    r0 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R0")
-    r1 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R1")
 
 aarch32LinuxSyscallABI :: SM.BuildSyscallABI DMA.ARM sym (AE.AmbientSimulatorState sym DMA.ARM) mem
 aarch32LinuxSyscallABI = SM.BuildSyscallABI $ \ initialMem unsupportedRelocs ->

diff --git a/stubs-loader/src/Stubs/Loader.hs b/stubs-loader/src/Stubs/Loader.hs
@@ -75,7 +75,6 @@ import Stubs.Arch.PPC32 ()
 import Stubs.Arch.PPC64 ()
 import qualified Data.Macaw.ARM.ARMReg as ARMReg
 import qualified Dismantle.PPC as DP
-import qualified Language.ASL.Globals as ASL
 import qualified Stubs.Translate.Core as STC
 import qualified Stubs.Memory as SM
 import qualified Stubs.Translate.Intrinsic as STI
@@ -214,7 +213,7 @@ withBinary name bytes mbSharedObjectDir hdlAlloc _sym k = do
                                             AFAL.aarch32LinuxTypes)
                 (elfBinarySizeTotal bins)
                 binConf
-                (Just (FunABIExt (ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R0"))))
+                (Just (FunABIExt ARMReg.r0))
                 ovs
             Nothing -> CMC.throwM (AE.UnsupportedELFArchitecture name DE.EM_ARM DE.ELFCLASS32)
         (DE.EM_PPC, DE.ELFCLASS32) -> do

diff --git a/submodules/macaw b/submodules/macaw
+1 −1		macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
+1 −1		macaw-aarch32-symbolic/tests/Main.hs
+2 −0		macaw-aarch32/ChangeLog.md
+1 −1		macaw-aarch32/src/Data/Macaw/ARM.hs
+131 −32		macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
+24 −30		macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
+1 −1		macaw-aarch32/src/Data/Macaw/ARM/Eval.hs
+2 −2		macaw-aarch32/src/Data/Macaw/ARM/Identify.hs