hlint: Add a hint, also lint crucible-llvm in CI (#1221)

.github/workflows/lint.yml

@@ -25,6 +25,7 @@ jobs:
           (cd crucible-concurrency/; ../hlint-3.8/hlint src test)
           (cd crucible-go/; ../hlint-3.8/hlint src tests)
           (cd crucible-jvm/; ../hlint-3.8/hlint src tests)
+          (cd crucible-llvm/; ../hlint-3.8/hlint src test)
           (cd crucible-llvm-cli/; ../hlint-3.8/hlint src test)
           (cd crucible-llvm-syntax/; ../hlint-3.8/hlint src test)
           (cd crucible-mir/; ../hlint-3.8/hlint src)

.hlint.yaml

@@ -3,6 +3,11 @@
 
 - ignore: {}  # ignore all
 
+- error:
+    name: Use llvmPointer_bv
+    lhs: "LLVMPointer <$> What4.Interface.natLit sym 0 <*> offset"
+    rhs: 'Lang.Crucible.LLVM.MemModel.Pointer.llvmPointer_bv sym =<< offset'
+
 - error:
     name: Use bvZero
     lhs: "What4.Interface.bvLit sym w (Data.BitVector.Sized.zero w)"

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -1255,7 +1255,7 @@ loadArrayConcreteSizeRaw ::
   IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8)))
 loadArrayConcreteSizeRaw sym mem ptr sz alignment
   | sz == 0 = do
-    zero_bv <- bvLit sym knownNat $ BV.zero knownNat
+    zero_bv <- bvZero sym knownNat
     zero_arr <- constantArray sym (Ctx.singleton $ BaseBVRepr PtrWidth) zero_bv
     return $ Right (truePred sym, zero_arr)
   | otherwise = do
@@ -1271,7 +1271,7 @@ loadArrayConcreteSizeRaw sym mem ptr sz alignment
                       (Ctx.singleton $ BVIndexLit PtrWidth $ BV.mkBV PtrWidth $ fromIntegral i, byte)
                     _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValInt"])
                   llvm_vals
-            zero_bv <- bvLit sym knownNat $ BV.zero knownNat
+            zero_bv <- bvZero sym knownNat
             arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv
             return $ Right (ok, arr)
           _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"]

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -383,7 +383,7 @@ floatToBV _ _ (NoErr p (LLVMValUndef (StorageType Float _))) =
 
 floatToBV sym _ (NoErr p (LLVMValZero (StorageType Float _))) =
   do nz <- W4I.natLit sym 0
-     iz <- W4I.bvLit sym (knownNat @32) (BV.zero knownNat)
+     iz <- W4I.bvZero sym (knownNat @32)
      return (NoErr p (LLVMValInt nz iz))
 
 floatToBV sym _ (NoErr p (LLVMValFloat Value.SingleSize v)) =
@@ -409,7 +409,7 @@ doubleToBV _ _ (NoErr p (LLVMValUndef (StorageType Double _))) =
 
 doubleToBV sym _ (NoErr p (LLVMValZero (StorageType Double _))) =
   do nz <- W4I.natLit sym 0
-     iz <- W4I.bvLit sym (knownNat @64) (BV.zero knownNat)
+     iz <- W4I.bvZero sym (knownNat @64)
      return (NoErr p (LLVMValInt nz iz))
 
 doubleToBV sym _ (NoErr p (LLVMValFloat Value.DoubleSize v)) =
@@ -941,7 +941,7 @@ muxLLVMVal sym = merge sym muxval
 
       LLVMValInt base off ->
         do zbase <- W4I.natLit sym 0
-           zoff  <- W4I.bvLit sym (W4I.bvWidth off) (BV.zero (W4I.bvWidth off))
+           zoff  <- W4I.bvZero sym (W4I.bvWidth off)
            base' <- W4I.natIte sym cond zbase base
            off'  <- W4I.bvIte sym cond zoff off
            return $ LLVMValInt base' off'

crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs

@@ -1093,8 +1093,8 @@ advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id
             -- try to unify widening variables that have the same values
             (normal_substitution', equality_substitution') <- uninterpretedConstantEqualitySubstitution sym union_substitution
 
-            zero_bv <- W4.bvLit sym knownNat $ BV.zero knownNat
-            one_bv <- W4.bvLit sym knownNat $ BV.one knownNat
+            zero_bv <- W4.bvZero sym knownNat
+            one_bv <- W4.bvOne sym knownNat
             add_index_one <- W4.bvAdd sym (fixpointIndex fixpoint_record) one_bv
             let normal_substitution = MapF.insert
                   (fixpointIndex fixpoint_record)

crucible-llvm/test/TestMemory.hs

@@ -329,7 +329,7 @@ testMemArrayCopy = testCase "smt array copy memory model" $ withMem LLVMD.Little
   assume bak =<< What4.bvUlt sym len =<< What4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth 1024)
   mem3 <- LLVMMem.doMemcpy bak ?ptrWidth mem2 False dst_ptr src_base_ptr len
 
-  zero_bv <- What4.bvLit sym ?ptrWidth $ BV.zero ?ptrWidth
+  zero_bv <- What4.bvZero sym ?ptrWidth
   expected_arr <- What4.arrayCopy sym dst_arr i src_arr zero_bv len
   expected_val <- What4.arrayLookup sym expected_arr $ Ctx.singleton i
 

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

@@ -36,7 +36,7 @@ import Prettyprinter
 
 -- what4
 import qualified What4.Expr.Builder as WEB
-import What4.Interface (bvLit, natLit, bvZero)
+import What4.Interface (bvLit, bvZero)
 
 -- crucible
 import Lang.Crucible.Backend
@@ -65,8 +65,8 @@ import Lang.Crucible.LLVM.MemModel
         ( Mem, MemImpl, mkMemVar, withPtrWidth, memAllocCount, memWriteCount
         , MemOptions(..), HasLLVMAnn, LLVMAnnMap
         , explainCex, CexExplanation(..), doAlloca
-        , pattern LLVMPointer, pattern LLVMPointerRepr, LLVMPointerType
-        , pattern PtrRepr, pattern PtrWidth
+        , pattern LLVMPointerRepr, LLVMPointerType
+        , pattern PtrRepr, pattern PtrWidth, llvmPointer_bv
         )
 import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack)
 import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize)
@@ -338,7 +338,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 <*> bvZero sym w
+      argc <- liftIO $ llvmPointer_bv sym =<< 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'