From cd3951f9e6ae5c4b1929d4816f56c798f539e923 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 15:59:42 -0400 Subject: [PATCH] hlint: Add a hint, also lint crucible-llvm in CI --- .github/workflows/lint.yml | 1 + .hlint.yaml | 5 +++++ crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs | 4 ++-- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs | 6 +++--- .../src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs | 4 ++-- crucible-llvm/test/TestMemory.hs | 2 +- crux-llvm/src/Crux/LLVM/Simulate.hs | 8 ++++---- 7 files changed, 18 insertions(+), 12 deletions(-) diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index af7a7c604..7396dc3e6 100644 --- a/.github/workflows/lint.yml +++ b/.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) diff --git a/.hlint.yaml b/.hlint.yaml index db24bf8bb..a555d52c0 100644 --- a/.hlint.yaml +++ b/.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)" diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 226fa93e9..e81aa1fcd 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/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"] diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs index 0a39fda2f..d8b5ba596 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs +++ b/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' diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs index 7765c57ab..5d3d61497 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs +++ b/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) diff --git a/crucible-llvm/test/TestMemory.hs b/crucible-llvm/test/TestMemory.hs index c242582e1..d811c1e08 100644 --- a/crucible-llvm/test/TestMemory.hs +++ b/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 diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index 027d70e1e..4bdfa00e9 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/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'