From 384e0502e2761a625e6798e87f53ff8ff4a74eb5 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Mar 2024 14:21:11 -0400 Subject: [PATCH] crucible-llvm: Don't pass around the symbolic backend explicitly `Lang.Crucible.Simulator.OverrideSim.{getSymInterface,ovrWithBackend}` can replace the explicit passing of `bak`. This should simplify some type signatures. --- .../src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs | 6 +- .../src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 111 +++++++++--------- 2 files changed, 57 insertions(+), 60 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs index 6c15f93ee..64d90b691 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs @@ -739,7 +739,7 @@ llvmBSwapOverride widthRepr = -- From the LLVM docs: -- declare i16 @llvm.bswap.i16(i16 ) [llvmOvr| #width8 $nm( #width8 ) |] - (\_ bak args -> Ctx.uncurryAssignment (Libc.callBSwap bak widthRepr) args) + (\_ _bak args -> Ctx.uncurryAssignment (Libc.callBSwap widthRepr) args) }}} llvmAbsOverride :: @@ -751,9 +751,9 @@ llvmAbsOverride :: llvmAbsOverride w = let nm = L.Symbol ("llvm.abs.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, i1 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (Libc.callLLVMAbs bak callStack w) args) + Ctx.uncurryAssignment (Libc.callLLVMAbs callStack w) args) llvmCopysignOverride_F32 :: IsSymInterface sym => diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index b93ba7421..aeeb4a88f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -1529,7 +1529,7 @@ llvmHtonlOverride :: (BVType 32) llvmHtonlOverride = [llvmOvr| i32 @htonl( i32 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmHtonsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1538,7 +1538,7 @@ llvmHtonsOverride :: (BVType 16) llvmHtonsOverride = [llvmOvr| i16 @htons( i16 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmNtohlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1547,7 +1547,7 @@ llvmNtohlOverride :: (BVType 32) llvmNtohlOverride = [llvmOvr| i32 @ntohl( i32 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmNtohsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1556,7 +1556,7 @@ llvmNtohsOverride :: (BVType 16) llvmNtohsOverride = [llvmOvr| i16 @ntohs( i16 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1565,9 +1565,9 @@ llvmAbsOverride :: (BVType 32) llvmAbsOverride = [llvmOvr| i32 @abs( i32 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @32)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) -- @labs@ uses `long` as its argument and result type, so we need two overrides -- for @labs@. See Note [Overrides involving (unsigned) long] in @@ -1579,9 +1579,9 @@ llvmLAbsOverride_32 :: (BVType 32) llvmLAbsOverride_32 = [llvmOvr| i32 @labs( i32 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @32)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) llvmLAbsOverride_64 :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1590,9 +1590,9 @@ llvmLAbsOverride_64 :: (BVType 64) llvmLAbsOverride_64 = [llvmOvr| i64 @labs( i64 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) llvmLLAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1601,18 +1601,18 @@ llvmLLAbsOverride :: (BVType 64) llvmLLAbsOverride = [llvmOvr| i64 @llabs( i64 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) callBSwap :: - (1 <= width, IsSymBackend sym bak) => - bak -> + (1 <= width, IsSymInterface sym) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) -callBSwap bak widthRepr (regValue -> vec) = - liftIO $ bvSwap (backendGetSym bak) widthRepr vec +callBSwap widthRepr (regValue -> vec) = do + sym <- getSymInterface + liftIO $ bvSwap sym widthRepr vec -- | This determines under what circumstances @callAbs@ should check if its -- argument is equal to the smallest signed integer of a particular size @@ -1631,60 +1631,58 @@ data CheckAbsIntMin -- | The workhorse for the @abs@, @labs@, and @llabs@ functions, as well as the -- @llvm.abs.*@ family of overloaded intrinsics. callAbs :: - forall w p sym bak ext r args ret. - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + forall w p sym ext r args ret. + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> CheckAbsIntMin -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callAbs bak callStack checkIntMin widthRepr (regValue -> src) = liftIO $ do - let sym = backendGetSym bak - bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr) - isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin - - when shouldCheckIntMin $ do - isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin - let err = AssertFailureSimError "Undefined behavior encountered" $ - show $ UB.explain ub - assert bak isNotIntMinUB err - - isSrcNegative <- bvIsNeg sym src - srcNegated <- bvNeg sym src - bvIte sym isSrcNegative srcNegated src - where - shouldCheckIntMin :: Bool - shouldCheckIntMin = - case checkIntMin of - LibcAbsIntMinUB -> True - LLVMAbsIntMinPoison shouldCheck -> shouldCheck - - ub :: UB.UndefinedBehavior (RegValue' sym) - ub = case checkIntMin of - LibcAbsIntMinUB -> - UB.AbsIntMin $ RV src - LLVMAbsIntMinPoison{} -> - UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src +callAbs callStack checkIntMin widthRepr (regValue -> src) = do + sym <- getSymInterface + ovrWithBackend $ \bak -> liftIO $ do + bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr) + isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin + + when shouldCheckIntMin $ do + isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin + let err = AssertFailureSimError "Undefined behavior encountered" $ + show $ UB.explain ub + assert bak isNotIntMinUB err + + isSrcNegative <- bvIsNeg sym src + srcNegated <- bvNeg sym src + bvIte sym isSrcNegative srcNegated src + where + shouldCheckIntMin :: Bool + shouldCheckIntMin = + case checkIntMin of + LibcAbsIntMinUB -> True + LLVMAbsIntMinPoison shouldCheck -> shouldCheck + + ub :: UB.UndefinedBehavior (RegValue' sym) + ub = case checkIntMin of + LibcAbsIntMinUB -> + UB.AbsIntMin $ RV src + LLVMAbsIntMinPoison{} -> + UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src callLibcAbs :: - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLibcAbs bak callStack = callAbs bak callStack LibcAbsIntMinUB +callLibcAbs callStack = callAbs callStack LibcAbsIntMinUB callLLVMAbs :: - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLLVMAbs bak callStack widthRepr src (regValue -> isIntMinPoison) = do +callLLVMAbs callStack widthRepr src (regValue -> isIntMinPoison) = do shouldCheckIntMin <- liftIO $ -- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second -- argument must be a constant. @@ -1693,21 +1691,20 @@ callLLVMAbs bak callStack widthRepr src (regValue -> isIntMinPoison) = do Nothing -> malformedLLVMModule "Call to llvm.abs.* with non-constant second argument" [printSymExpr isIntMinPoison] - callAbs bak callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src + callAbs callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src -- | If the data layout is little-endian, run 'callBSwap' on the input. -- Otherwise, return the input unchanged. This is the workhorse for the -- @hton{s,l}@ and @ntoh{s,l}@ overrides. callBSwapIfLittleEndian :: - (1 <= width, IsSymBackend sym bak, ?lc :: TypeContext) => - bak -> + (1 <= width, IsSymInterface sym, ?lc :: TypeContext) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) -callBSwapIfLittleEndian bak widthRepr vec = +callBSwapIfLittleEndian widthRepr vec = case (llvmDataLayout ?lc)^.intLayout of BigEndian -> pure (regValue vec) - LittleEndian -> callBSwap bak widthRepr vec + LittleEndian -> callBSwap widthRepr vec ---------------------------------------------------------------------------- -- atexit stuff