Use new what4 bitvector helpers, hlint in crux-{llvm,mir}

.github/workflows/lint.yml

@@ -32,3 +32,5 @@ jobs:
           (cd crucible-symio/; ../hlint-3.8/hlint src tests)
           (cd crucible-syntax/; ../hlint-3.8/hlint src test)
           (cd crucible-wasm/; ../hlint-3.8/hlint src test)
+          (cd crux-llvm/; ../hlint-3.8/hlint src test)
+          (cd crux-wasm/; ../hlint-3.8/hlint src test)

crux-llvm/src/Crux/LLVM/Overrides.hs

@@ -417,7 +417,7 @@ fresh_str arch mvar (Empty :> pName :> maxLen) =
 
     -- Compute the allocation length, which is the requested length plus one
     -- to hold the NUL terminator
-    one <- liftIO $ bvLit sym ?ptrWidth (BV.one ?ptrWidth)
+    one <- liftIO $ bvOne sym ?ptrWidth
     -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen)
     len <- liftIO $ bvAdd sym (regValue maxLen) one
     mem0 <- readGlobal mvar

crux-llvm/src/Crux/LLVM/Simulate.hs

@@ -339,7 +339,7 @@ checkFun llvmOpts trans memVar =
       mem <- case lookupGlobal memVar gs of
                Just mem -> pure mem
                Nothing  -> fail "checkFun.checkMainWithArguments: Memory missing from global vars"
-      argc <- liftIO $ LLVMPointer <$> natLit sym 0 <*> bvLit sym w (BV.zero w)
+      argc <- liftIO $ LLVMPointer <$> natLit sym 0 <*> bvZero sym w
       sz   <- liftIO $ bvLit sym PtrWidth $ bytesToBV PtrWidth tp_sz
       (argv, mem') <- liftIO $ doAlloca bak mem sz alignment loc
       stateTree.actFrame.gpGlobals %= insertGlobal memVar mem'

crux-mir/src/Mir/Overrides.hs

@@ -229,7 +229,7 @@ regEval bak baseEval tpr v = go tpr v
 
         let vec = MirVector_Vector $ V.fromList vals
         let vecRef = newConstMirRef sym (MirVectorRepr tpr') vec
-        ptr <- subindexMirRefSim tpr' vecRef =<< liftIO (bvLit sym knownRepr (BV.zero knownRepr))
+        ptr <- subindexMirRefSim tpr' vecRef =<< liftIO (bvZero sym knownRepr)
         return $ Empty :> RV ptr :> RV len'
 
     go (FloatRepr fi) v = pure v