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.
GaloisInc · Mar 21, 2024 · 384e050 · 384e050
1 parent af9c127
commit 384e050
Show file tree

Hide file tree

Showing 2 changed files with 57 additions and 60 deletions.
diff --git 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 <id>)
         [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
@@ -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