From 30eb41a37812c21edbdefc3f58c2f6416f33c60f Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Tue, 15 Nov 2022 05:09:04 +0000 Subject: [PATCH 01/35] Code refactoring. --- .../Lang/Crucible/LLVM/MemModel/Generic.hs | 135 ++++++++++-------- 1 file changed, 74 insertions(+), 61 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index c2439fdc4..8fa558dfb 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -90,6 +90,7 @@ import Numeric.Natural import Prettyprinter import Lang.Crucible.Panic (panic) +import Data.BitVector.Sized (BV) import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx @@ -1651,73 +1652,85 @@ asMemAllocationArrayStore sym w ptr mem | Just blk_no <- asNat (llvmPointerBlock ptr) , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = - do result <- findArrayStore blk_no sz $ memWritesAtConstant blk_no $ memWrites mem + do result <- findArrayStore sym w blk_no (BV.zero w) sz $ memWritesAtConstant blk_no $ memWrites mem return $ case result of Just (ok, arr) -> Just (ok, arr, sz) Nothing -> Nothing | otherwise = return Nothing - where - findArrayStore :: - Natural -> - SymBV sym w -> - [MemWrite sym] -> - IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) - - findArrayStore _ _ [] = return Nothing - - findArrayStore blk_no sz (head_mem_write : tail_mem_writes) = - case head_mem_write of - MemWrite write_ptr write_source - | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) - , blk_no == write_blk_no - , Just (BV.BV 0) <- asBV (llvmPointerOffset write_ptr) - , MemArrayStore arr (Just arr_store_sz) <- write_source - , Just Refl <- testEquality w (ptrWidth write_ptr) -> do - ok <- bvEq sym sz arr_store_sz - return (Just (ok, arr)) - - | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) - , blk_no /= write_blk_no -> - findArrayStore blk_no sz tail_mem_writes - - | otherwise -> return Nothing - - WriteMerge cond lhs_mem_writes rhs_mem_writes -> do - lhs_result <- findArrayStore blk_no sz (memWritesAtConstant blk_no lhs_mem_writes) - rhs_result <- findArrayStore blk_no sz (memWritesAtConstant blk_no rhs_mem_writes) - - -- Only traverse the tail if necessary, and be careful - -- only to traverse it once - case (lhs_result, rhs_result) of - (Just _, Just _) -> combineResults cond lhs_result rhs_result - - (Just _, Nothing) -> - do rhs' <- findArrayStore blk_no sz tail_mem_writes - combineResults cond lhs_result rhs' - - (Nothing, Just _) -> - do lhs' <- findArrayStore blk_no sz tail_mem_writes - combineResults cond lhs' rhs_result - - (Nothing, Nothing) -> findArrayStore blk_no sz tail_mem_writes - - combineResults cond (Just (lhs_ok, lhs_arr)) (Just (rhs_ok, rhs_arr)) = - do ok <- itePred sym cond lhs_ok rhs_ok - arr <- arrayIte sym cond lhs_arr rhs_arr - pure (Just (ok,arr)) - - combineResults cond (Just (lhs_ok, lhs_arr)) Nothing = - do ok <- andPred sym cond lhs_ok - pure (Just (ok, lhs_arr)) - - combineResults cond Nothing (Just (rhs_ok, rhs_arr)) = - do cond' <- notPred sym cond - ok <- andPred sym cond' rhs_ok - pure (Just (ok, rhs_arr)) - - combineResults _cond Nothing Nothing = pure Nothing +findArrayStore :: + (IsSymInterface sym, 1 <= w) => + sym -> + NatRepr w -> + Natural -> + BV w -> + SymBV sym w -> + [MemWrite sym] -> + IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) + +findArrayStore _ _ _ _ _ [] = return Nothing + +findArrayStore sym w blk_no off sz (head_mem_write : tail_mem_writes) = + case head_mem_write of + MemWrite write_ptr write_source + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , off == write_off + , MemArrayStore arr (Just arr_store_sz) <- write_source -> do + ok <- bvEq sym sz arr_store_sz + return (Just (ok, arr)) + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no /= write_blk_no -> + findArrayStore sym w blk_no off sz tail_mem_writes + + | otherwise -> return Nothing + + WriteMerge cond lhs_mem_writes rhs_mem_writes -> do + lhs_result <- findArrayStore sym w blk_no off sz (memWritesAtConstant blk_no lhs_mem_writes) + rhs_result <- findArrayStore sym w blk_no off sz (memWritesAtConstant blk_no rhs_mem_writes) + + -- Only traverse the tail if necessary, and be careful + -- only to traverse it once + case (lhs_result, rhs_result) of + (Just _, Just _) -> combineResults sym cond lhs_result rhs_result + + (Just _, Nothing) -> + do rhs' <- findArrayStore sym w blk_no off sz tail_mem_writes + combineResults sym cond lhs_result rhs' + + (Nothing, Just _) -> + do lhs' <- findArrayStore sym w blk_no off sz tail_mem_writes + combineResults sym cond lhs' rhs_result + + (Nothing, Nothing) -> findArrayStore sym w blk_no off sz tail_mem_writes + +combineResults :: + IsSymInterface sym => + sym -> + Pred sym -> + Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) -> + Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) -> + IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) + +combineResults sym cond (Just (lhs_ok, lhs_arr)) (Just (rhs_ok, rhs_arr)) = + do ok <- itePred sym cond lhs_ok rhs_ok + arr <- arrayIte sym cond lhs_arr rhs_arr + pure (Just (ok,arr)) + +combineResults sym cond (Just (lhs_ok, lhs_arr)) Nothing = + do ok <- andPred sym cond lhs_ok + pure (Just (ok, lhs_arr)) + +combineResults sym cond Nothing (Just (rhs_ok, rhs_arr)) = + do cond' <- notPred sym cond + ok <- andPred sym cond' rhs_ok + pure (Just (ok, rhs_arr)) + +combineResults _cond _sym Nothing Nothing = pure Nothing {- Note [Memory Model Design] From a00340e7ae1c41ce920735fd27df75eaf8b46d0c Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Tue, 15 Nov 2022 05:12:49 +0000 Subject: [PATCH 02/35] Find SMT array write of a fixed size. --- .../src/Lang/Crucible/LLVM/MemModel.hs | 1 + .../Lang/Crucible/LLVM/MemModel/Generic.hs | 56 +++++++++++++++++++ .../src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 10 ++-- 3 files changed, 63 insertions(+), 4 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 786102d43..ef61d864b 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -163,6 +163,7 @@ module Lang.Crucible.LLVM.MemModel , G.pushStackFrameMem , G.popStackFrameMem , G.asMemAllocationArrayStore + , G.asMemMatchingArrayStore , SomeFnHandle(..) , G.SomeAlloc(..) , G.possibleAllocs diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 8fa558dfb..947382c0f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -58,6 +58,7 @@ module Lang.Crucible.LLVM.MemModel.Generic , branchAbortMem , mergeMem , asMemAllocationArrayStore + , asMemMatchingArrayStore , isAligned , SomeAlloc(..) @@ -78,6 +79,7 @@ import Prelude hiding (pred) import Control.Lens import Control.Monad import Control.Monad.State.Strict +import Control.Monad.Trans.Maybe import Data.IORef import Data.Maybe import qualified Data.List as List @@ -1659,6 +1661,20 @@ asMemAllocationArrayStore sym w ptr mem | otherwise = return Nothing +asMemMatchingArrayStore :: + (IsSymInterface sym, 1 <= w) => + sym -> + NatRepr w -> + LLVMPtr sym w -> + SymBV sym w -> + Mem sym -> + IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) +asMemMatchingArrayStore sym w ptr sz mem + | Just blk_no <- asNat (llvmPointerBlock ptr) + , Just off <- asBV (llvmPointerOffset ptr) = + findArrayStore sym w blk_no off sz $ memWritesAtConstant blk_no $ memWrites mem + | otherwise = return Nothing + findArrayStore :: (IsSymInterface sym, 1 <= w) => sym -> @@ -1683,6 +1699,46 @@ findArrayStore sym w blk_no off sz (head_mem_write : tail_mem_writes) = ok <- bvEq sym sz arr_store_sz return (Just (ok, arr)) + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , Just sz_bv <- asBV sz + , MemCopy src_ptr mem_copy_sz <- write_source + , Just mem_copy_sz_bv <- asBV mem_copy_sz + , BV.ule write_off off + , BV.ule (BV.add w off sz_bv) (BV.add w write_off mem_copy_sz_bv) + , Just src_blk_no <- asNat (llvmPointerBlock src_ptr) + , Just src_off <- asBV (llvmPointerOffset src_ptr) -> + findArrayStore sym w src_blk_no (BV.add w src_off $ BV.sub w off write_off) sz tail_mem_writes + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , Just sz_bv <- asBV sz + , MemSet val mem_set_sz <- write_source + , Just mem_set_sz_bv <- asBV mem_set_sz + , BV.ule write_off off + , BV.ule (BV.add w off sz_bv) (BV.add w write_off mem_set_sz_bv) -> do + arr <- constantArray sym (Ctx.singleton $ BaseBVRepr w) val + return $ Just (truePred sym, arr) + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) -> do + maybe_write_sz <- runMaybeT $ writeSourceSize sym w write_source + case maybe_write_sz of + Just write_sz + | Just sz_bv <- asBV sz + , Just write_sz_bv <- asBV write_sz + , end <- BV.add w off sz_bv + , write_end <- BV.add w write_off write_sz_bv + , BV.ule end write_off || BV.ule write_end off -> + findArrayStore sym w blk_no off sz tail_mem_writes + _ -> return Nothing + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) , blk_no /= write_blk_no -> findArrayStore sym w blk_no off sz tail_mem_writes diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index c004e26ea..f2eb2de35 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -44,6 +44,7 @@ module Lang.Crucible.LLVM.MemModel.MemLog , isAllocatedGeneric -- * Write logs , WriteSource(..) + , writeSourceSize , MemWrite(..) , MemWrites(..) , MemWritesChunk(..) @@ -527,15 +528,16 @@ multiUnion :: (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a multiUnion = Map.unionWith (<>) writeSourceSize :: - (IsExprBuilder sym, HasPtrWidth w) => + (IsExprBuilder sym, 1 <= w) => sym -> + NatRepr w -> WriteSource sym w -> MaybeT IO (SymBV sym w) -writeSourceSize sym = \case +writeSourceSize sym w = \case MemCopy _src sz -> pure sz MemSet _val sz -> pure sz MemStore _val st _align -> - liftIO $ bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth $ toInteger $ typeEnd 0 st + liftIO $ bvLit sym w $ BV.mkBV w $ toInteger $ typeEnd 0 st MemArrayStore _arr Nothing -> MaybeT $ pure Nothing MemArrayStore _arr (Just sz) -> pure sz MemInvalidate _nm sz -> pure sz @@ -550,7 +552,7 @@ writeRangesMemWrite sym = \case | Just Refl <- testEquality ?ptrWidth (ptrWidth ptr) -> case asNat (llvmPointerBlock ptr) of Just blk -> do - sz <- writeSourceSize sym wsrc + sz <- writeSourceSize sym ?ptrWidth wsrc pure $ Map.singleton blk [(llvmPointerOffset ptr, sz)] Nothing -> MaybeT $ pure Nothing | otherwise -> fail "foo" From c749b38f449a9402737a654fa2d5d500f55f5f1e Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 04:49:15 +0000 Subject: [PATCH 03/35] Cache tail traversal in findArrayStore. --- .../Lang/Crucible/LLVM/MemModel/Generic.hs | 88 +++++++++---------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 947382c0f..d5282b3cc 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -1632,6 +1632,21 @@ possibleAllocs n mem = Just (AllocInfo atp sz mut alignment loc) -> [SomeAlloc atp n sz mut alignment loc] + +newtype MemoIO m a = MemoIO (IORef (Either (m a) a)) + +putMemoIO :: MonadIO m => m a -> m (MemoIO m a) +putMemoIO comp = MemoIO <$> (liftIO $ newIORef $ Left comp) + +getMemoIO :: MonadIO m => MemoIO m a -> m a +getMemoIO (MemoIO ref) = (liftIO $ readIORef ref) >>= \case + Left comp -> do + res <- comp + liftIO $ writeIORef ref $ Right res + return res + Right res -> return res + + -- | Check if @LLVMPtr sym w@ points inside an allocation that is backed -- by an SMT array store. If true, return a predicate that indicates -- when the given array backs the given pointer, the SMT array, @@ -1654,7 +1669,9 @@ asMemAllocationArrayStore sym w ptr mem | Just blk_no <- asNat (llvmPointerBlock ptr) , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = - do result <- findArrayStore sym w blk_no (BV.zero w) sz $ memWritesAtConstant blk_no $ memWrites mem + do memo_nothing <- putMemoIO $ return Nothing + result <- findArrayStore sym w blk_no (BV.zero w) sz memo_nothing $ + memWritesAtConstant blk_no $ memWrites mem return $ case result of Just (ok, arr) -> Just (ok, arr, sz) Nothing -> Nothing @@ -1671,8 +1688,9 @@ asMemMatchingArrayStore :: IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) asMemMatchingArrayStore sym w ptr sz mem | Just blk_no <- asNat (llvmPointerBlock ptr) - , Just off <- asBV (llvmPointerOffset ptr) = - findArrayStore sym w blk_no off sz $ memWritesAtConstant blk_no $ memWrites mem + , Just off <- asBV (llvmPointerOffset ptr) = do + memo_nothing <- putMemoIO $ return Nothing + findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem | otherwise = return Nothing findArrayStore :: @@ -1682,13 +1700,12 @@ findArrayStore :: Natural -> BV w -> SymBV sym w -> + MemoIO IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) -> [MemWrite sym] -> IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) - -findArrayStore _ _ _ _ _ [] = return Nothing - -findArrayStore sym w blk_no off sz (head_mem_write : tail_mem_writes) = - case head_mem_write of +findArrayStore sym w blk_no off sz memo_cont = \case + [] -> getMemoIO memo_cont + head_mem_write : tail_mem_writes -> case head_mem_write of MemWrite write_ptr write_source | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) , blk_no == write_blk_no @@ -1710,7 +1727,7 @@ findArrayStore sym w blk_no off sz (head_mem_write : tail_mem_writes) = , BV.ule (BV.add w off sz_bv) (BV.add w write_off mem_copy_sz_bv) , Just src_blk_no <- asNat (llvmPointerBlock src_ptr) , Just src_off <- asBV (llvmPointerOffset src_ptr) -> - findArrayStore sym w src_blk_no (BV.add w src_off $ BV.sub w off write_off) sz tail_mem_writes + findArrayStore sym w src_blk_no (BV.add w src_off $ BV.sub w off write_off) sz memo_cont tail_mem_writes | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) , blk_no == write_blk_no @@ -1736,57 +1753,40 @@ findArrayStore sym w blk_no off sz (head_mem_write : tail_mem_writes) = , end <- BV.add w off sz_bv , write_end <- BV.add w write_off write_sz_bv , BV.ule end write_off || BV.ule write_end off -> - findArrayStore sym w blk_no off sz tail_mem_writes + findArrayStore sym w blk_no off sz memo_cont tail_mem_writes _ -> return Nothing | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) , blk_no /= write_blk_no -> - findArrayStore sym w blk_no off sz tail_mem_writes + findArrayStore sym w blk_no off sz memo_cont tail_mem_writes | otherwise -> return Nothing WriteMerge cond lhs_mem_writes rhs_mem_writes -> do - lhs_result <- findArrayStore sym w blk_no off sz (memWritesAtConstant blk_no lhs_mem_writes) - rhs_result <- findArrayStore sym w blk_no off sz (memWritesAtConstant blk_no rhs_mem_writes) - -- Only traverse the tail if necessary, and be careful -- only to traverse it once - case (lhs_result, rhs_result) of - (Just _, Just _) -> combineResults sym cond lhs_result rhs_result - - (Just _, Nothing) -> - do rhs' <- findArrayStore sym w blk_no off sz tail_mem_writes - combineResults sym cond lhs_result rhs' - - (Nothing, Just _) -> - do lhs' <- findArrayStore sym w blk_no off sz tail_mem_writes - combineResults sym cond lhs' rhs_result + memo_tail <- putMemoIO $ findArrayStore sym w blk_no off sz memo_cont tail_mem_writes - (Nothing, Nothing) -> findArrayStore sym w blk_no off sz tail_mem_writes + lhs_result <- findArrayStore sym w blk_no off sz memo_tail (memWritesAtConstant blk_no lhs_mem_writes) + rhs_result <- findArrayStore sym w blk_no off sz memo_tail (memWritesAtConstant blk_no rhs_mem_writes) -combineResults :: - IsSymInterface sym => - sym -> - Pred sym -> - Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) -> - Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) -> - IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) + case (lhs_result, rhs_result) of + (Just (lhs_ok, lhs_arr), Just (rhs_ok, rhs_arr)) -> + do ok <- itePred sym cond lhs_ok rhs_ok + arr <- arrayIte sym cond lhs_arr rhs_arr + pure (Just (ok,arr)) -combineResults sym cond (Just (lhs_ok, lhs_arr)) (Just (rhs_ok, rhs_arr)) = - do ok <- itePred sym cond lhs_ok rhs_ok - arr <- arrayIte sym cond lhs_arr rhs_arr - pure (Just (ok,arr)) + (Just (lhs_ok, lhs_arr), Nothing) -> + do ok <- andPred sym cond lhs_ok + pure (Just (ok, lhs_arr)) -combineResults sym cond (Just (lhs_ok, lhs_arr)) Nothing = - do ok <- andPred sym cond lhs_ok - pure (Just (ok, lhs_arr)) + (Nothing, Just (rhs_ok, rhs_arr)) -> + do cond' <- notPred sym cond + ok <- andPred sym cond' rhs_ok + pure (Just (ok, rhs_arr)) -combineResults sym cond Nothing (Just (rhs_ok, rhs_arr)) = - do cond' <- notPred sym cond - ok <- andPred sym cond' rhs_ok - pure (Just (ok, rhs_arr)) + (Nothing, Nothing) -> pure Nothing -combineResults _cond _sym Nothing Nothing = pure Nothing {- Note [Memory Model Design] From 523a230992d2f2e5a9087774f37d06c35d2a7daa Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 13:26:51 +0000 Subject: [PATCH 04/35] Load SMT array with concrete size. --- .../src/Lang/Crucible/LLVM/MemModel.hs | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index ef61d864b..90f053e64 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -96,6 +96,7 @@ module Lang.Crucible.LLVM.MemModel , unpackMemValue , packMemValue , loadRaw + , loadArrayConcreteSizeRaw , storeRaw , condStoreRaw , storeConstRaw @@ -215,6 +216,7 @@ import qualified Text.LLVM.AST as L import What4.Interface import What4.Expr( GroundValue ) +import qualified What4.Expr.ArrayUpdateMap as AUM import What4.InterpretedFloatingPoint import What4.ProgramLoc @@ -1289,6 +1291,34 @@ loadRaw sym mem ptr valType alignment = do let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr G.readMem sym PtrWidth gsym ptr valType alignment (memImplHeap mem) +-- | Load an array with concrete size from memory. +loadArrayConcreteSizeRaw :: + forall sym wptr . + (IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym, ?memOpts :: MemOptions) => + sym -> + MemImpl sym -> + LLVMPtr sym wptr -> + Natural -> + Alignment -> + IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8))) +loadArrayConcreteSizeRaw sym mem ptr sz alignment = do + let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr + res <- G.readMem sym PtrWidth gsym ptr (arrayType sz $ bitvectorType 1) alignment (memImplHeap mem) + case res of + Partial.NoErr ok llvm_val_arr -> case llvm_val_arr of + LLVMValArray _ llvm_vals -> do + let aum = AUM.fromAscList knownRepr $ V.toList $ V.imap + (\i -> \case + LLVMValInt _ byte | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> + (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 + arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv + return $ Right (ok, arr) + _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"] + Partial.Err err -> return $ Left err + -- | Store an LLVM value in memory. Asserts that the pointer is valid and points -- to a mutable memory region. storeRaw :: From 0a50a597bbba503183a9da378ac1fad90f1ef3a1 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 14:19:09 +0000 Subject: [PATCH 05/35] Load SMT array with 0 size. --- .../src/Lang/Crucible/LLVM/MemModel.hs | 40 +++++++++++-------- 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 90f053e64..26dab947e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -1301,23 +1301,29 @@ loadArrayConcreteSizeRaw :: Natural -> Alignment -> IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8))) -loadArrayConcreteSizeRaw sym mem ptr sz alignment = do - let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr - res <- G.readMem sym PtrWidth gsym ptr (arrayType sz $ bitvectorType 1) alignment (memImplHeap mem) - case res of - Partial.NoErr ok llvm_val_arr -> case llvm_val_arr of - LLVMValArray _ llvm_vals -> do - let aum = AUM.fromAscList knownRepr $ V.toList $ V.imap - (\i -> \case - LLVMValInt _ byte | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> - (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 - arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv - return $ Right (ok, arr) - _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"] - Partial.Err err -> return $ Left err +loadArrayConcreteSizeRaw sym mem ptr sz alignment + | sz == 0 = do + zero_bv <- bvLit sym knownNat $ BV.zero knownNat + zero_arr <- constantArray sym (Ctx.singleton $ BaseBVRepr PtrWidth) zero_bv + return $ Right (truePred sym, zero_arr) + | otherwise = do + let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr + res <- G.readMem sym PtrWidth gsym ptr (arrayType sz $ bitvectorType 1) alignment (memImplHeap mem) + case res of + Partial.NoErr ok llvm_val_arr -> do + case llvm_val_arr of + LLVMValArray _ llvm_vals -> do + let aum = AUM.fromAscList knownRepr $ V.toList $ V.imap + (\i -> \case + LLVMValInt _ byte | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> + (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 + arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv + return $ Right (ok, arr) + _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"] + Partial.Err err -> return $ Left err -- | Store an LLVM value in memory. Asserts that the pointer is valid and points -- to a mutable memory region. From d414f3e3b7a16aa2c68c033238efaf49a9d221ec Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 27 Jun 2023 03:16:48 +0000 Subject: [PATCH 06/35] Add cache for base pointers with array stores. --- .../Lang/Crucible/LLVM/MemModel/Generic.hs | 4 +++- .../src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 23 +++++++++++++++---- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index d5282b3cc..d938db130 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -1452,7 +1452,7 @@ writeArrayMemWithAllocationCheck is_allocated sym w ptr alignment arr sz m = _ -> return default_m - return (m', p1, p2) + return (memInsertArrayBlock (llvmPointerBlock ptr) m', p1, p2) -- | Write an array to memory. -- @@ -1667,6 +1667,7 @@ asMemAllocationArrayStore :: IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8), (SymBV sym w))) asMemAllocationArrayStore sym w ptr mem | Just blk_no <- asNat (llvmPointerBlock ptr) + , memMemberArrayBlock (llvmPointerBlock ptr) mem , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = do memo_nothing <- putMemoIO $ return Nothing @@ -1688,6 +1689,7 @@ asMemMatchingArrayStore :: IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) asMemMatchingArrayStore sym w ptr sz mem | Just blk_no <- asNat (llvmPointerBlock ptr) + , memMemberArrayBlock (llvmPointerBlock ptr) mem , Just off <- asBV (llvmPointerOffset ptr) = do memo_nothing <- putMemoIO $ return Nothing findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index f2eb2de35..58abe131f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -57,6 +57,8 @@ module Lang.Crucible.LLVM.MemModel.MemLog , emptyChanges , emptyMem , memEndian + , memInsertArrayBlock + , memMemberArrayBlock -- * Pretty printing , ppType @@ -87,6 +89,8 @@ import qualified Data.List.Extra as List import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (mapMaybe) +import Data.Set (Set) +import qualified Data.Set as Set import Data.Text (Text) import Numeric.Natural import Prettyprinter @@ -326,7 +330,7 @@ data MemWrite sym -- implementation is able to efficiently merge memories, but requires -- that one only merge memories that were identical prior to the last -- branch. -data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym } +data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym, memArrayBlocks :: Set Natural } memState :: Lens' (Mem sym) (MemState sym) memState = lens _memState (\s v -> s { _memState = v }) @@ -417,11 +421,21 @@ emptyChanges :: MemChanges sym emptyChanges = (mempty, mempty) emptyMem :: EndianForm -> Mem sym -emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges } +emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges, memArrayBlocks = Set.empty } memEndian :: Mem sym -> EndianForm memEndian = memEndianForm +memInsertArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Mem sym +memInsertArrayBlock blk mem = case asNat blk of + Just blk_no -> mem { memArrayBlocks = Set.insert blk_no (memArrayBlocks mem) } + Nothing -> mem { memArrayBlocks = Set.empty } + +memMemberArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Bool +memMemberArrayBlock blk mem = case asNat blk of + Just blk_no -> Set.member blk_no (memArrayBlocks mem) + Nothing -> False + -------------------------------------------------------------------------------- -- Pretty printing @@ -744,5 +758,6 @@ concMem :: sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> Mem sym -> IO (Mem sym) -concMem sym conc (Mem endian st) = - Mem endian <$> concMemState sym conc st +concMem sym conc mem = do + conc_st <- concMemState sym conc $ mem ^. memState + return $ mem & memState .~ conc_st From 5f0efd1cf94c2b24fb673649d09a0585c0ac73c9 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 28 Jun 2023 00:00:16 +0000 Subject: [PATCH 07/35] Add noSatisfyingWriteFreshConstant option. --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs | 4 +++- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs | 8 ++++++++ crux-llvm/src/Crux/LLVM/Config.hs | 3 +++ 3 files changed, 14 insertions(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index d938db130..5f47489db 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -793,7 +793,9 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) = else do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be -- sure it always fails. But, because it's a variable, it won't be constant-folded away -- and we can be relatively sure the annotation will survive. - b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr + b <- if noSatisfyingWriteFreshConstant ?memOpts + then freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr + else return $ falsePred sym Partial.Err <$> Partial.annotateME sym mop (NoSatisfyingWrite tp) b diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs index c6fd1bf0f..7e1181a7e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs @@ -67,6 +67,13 @@ data MemOptions -- semantics. -- -- If 'laxLoadsAndStores' is disabled, this option has no effect. + + , noSatisfyingWriteFreshConstant :: !Bool + -- ^ If 'True', for the 'NoSatisfyingWrite' annotation, make a fresh + -- constant as a proof obligation, which ensures it always fails. But, + -- because it's a variable, it won't be constant-folded away and it's + -- relatively sure the annotation will survive. If 'False', annotate + -- 'false'. } @@ -115,6 +122,7 @@ defaultMemOptions = -- The choice of StableSymbolic here doesn't matter too much, since it -- won't have any effect when laxLoadsAndStores is disabled. , indeterminateLoadBehavior = StableSymbolic + , noSatisfyingWriteFreshConstant = True } diff --git a/crux-llvm/src/Crux/LLVM/Config.hs b/crux-llvm/src/Crux/LLVM/Config.hs index c3c015ab4..10424ce05 100644 --- a/crux-llvm/src/Crux/LLVM/Config.hs +++ b/crux-llvm/src/Crux/LLVM/Config.hs @@ -208,6 +208,9 @@ llvmCruxConfig = do , "'unstable-symbolic', which causes each read from uninitialized" , "memory to return a fresh symbolic value." ]) + noSatisfyingWriteFreshConstant <- + Crux.section "no-satisfying-write-fresh-constant" Crux.yesOrNoSpec True + "Make a fresh constant for the NoSatisfyingWrite annotation." return MemOptions{..} transOpts <- do laxArith <- From 98428da33b1840e7adb37a74470d9a9246c3c03b Mon Sep 17 00:00:00 2001 From: Andrei Date: Mon, 17 Jul 2023 22:47:26 +0000 Subject: [PATCH 08/35] wip --- .../src/Lang/Crucible/LLVM/MemModel/Generic.hs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 5f47489db..757420006 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -1638,10 +1638,10 @@ possibleAllocs n mem = newtype MemoIO m a = MemoIO (IORef (Either (m a) a)) putMemoIO :: MonadIO m => m a -> m (MemoIO m a) -putMemoIO comp = MemoIO <$> (liftIO $ newIORef $ Left comp) +putMemoIO comp = MemoIO <$> liftIO (newIORef $ Left comp) getMemoIO :: MonadIO m => MemoIO m a -> m a -getMemoIO (MemoIO ref) = (liftIO $ readIORef ref) >>= \case +getMemoIO (MemoIO ref) = liftIO (readIORef ref) >>= \case Left comp -> do res <- comp liftIO $ writeIORef ref $ Right res @@ -1673,6 +1673,7 @@ asMemAllocationArrayStore sym w ptr mem , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = do memo_nothing <- putMemoIO $ return Nothing + putStrLn $ "asMemAllocationArrayStore: base=" ++ show blk_no ++ " sz=" ++ show (printSymExpr sz) result <- findArrayStore sym w blk_no (BV.zero w) sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem return $ case result of @@ -1693,6 +1694,7 @@ asMemMatchingArrayStore sym w ptr sz mem | Just blk_no <- asNat (llvmPointerBlock ptr) , memMemberArrayBlock (llvmPointerBlock ptr) mem , Just off <- asBV (llvmPointerOffset ptr) = do + putStrLn $ "asMemMatchingArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) memo_nothing <- putMemoIO $ return Nothing findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem | otherwise = return Nothing @@ -1709,7 +1711,11 @@ findArrayStore :: IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) findArrayStore sym w blk_no off sz memo_cont = \case [] -> getMemoIO memo_cont - head_mem_write : tail_mem_writes -> case head_mem_write of + head_mem_write : tail_mem_writes -> do + putStrLn $ " findArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) + putStrLn $ " findArrayStore: write=" ++ (case head_mem_write of MemWrite{} -> "write"; WriteMerge{} -> "merge") + + case head_mem_write of MemWrite write_ptr write_source | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) , blk_no == write_blk_no From ebbcd4ee0bd80d1d9291c0731c89cd60c99ab521 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:02:01 +0000 Subject: [PATCH 09/35] Cleanup. --- .../src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 1 - .../src/Lang/Crucible/LLVM/Translation/Expr.hs | 1 - crucible/src/Lang/Crucible/CFG/Expr.hs | 1 - crucible/src/Lang/Crucible/Simulator/EvalStmt.hs | 1 - crucible/src/Lang/Crucible/Types.hs | 11 +---------- 5 files changed, 1 insertion(+), 14 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 5396c371f..7c632091d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -43,7 +43,6 @@ import Data.Parameterized.Context ( pattern (:>), pattern Empty ) import qualified Data.Parameterized.Context as Ctx import What4.Interface -import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder(..)) import What4.ProgramLoc (plSourceLoc) import qualified What4.SpecialFunctions as W4 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs index 6af46020d..6962a94e3 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs @@ -101,7 +101,6 @@ import Lang.Crucible.LLVM.TypeContext import Lang.Crucible.Syntax import Lang.Crucible.Types -import What4.InterpretedFloatingPoint (X86_80Val(..)) ------------------------------------------------------------------------- -- LLVMExpr diff --git a/crucible/src/Lang/Crucible/CFG/Expr.hs b/crucible/src/Lang/Crucible/CFG/Expr.hs index 5455f9e15..e823bdbbc 100644 --- a/crucible/src/Lang/Crucible/CFG/Expr.hs +++ b/crucible/src/Lang/Crucible/CFG/Expr.hs @@ -75,7 +75,6 @@ import qualified Data.Parameterized.TH.GADT as U import Data.Parameterized.TraversableFC import What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo) -import What4.InterpretedFloatingPoint (X86_80Val(..)) import Lang.Crucible.CFG.Extension import Lang.Crucible.FunctionHandle diff --git a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs index c3cb1dd10..c155f4f91 100644 --- a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs +++ b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs @@ -60,7 +60,6 @@ import Prettyprinter import What4.Config import What4.Interface -import What4.InterpretedFloatingPoint (freshFloatConstant) import What4.Partial import What4.ProgramLoc diff --git a/crucible/src/Lang/Crucible/Types.hs b/crucible/src/Lang/Crucible/Types.hs index 1b01ffd04..156745756 100644 --- a/crucible/src/Lang/Crucible/Types.hs +++ b/crucible/src/Lang/Crucible/Types.hs @@ -95,16 +95,7 @@ module Lang.Crucible.Types , module Data.Parameterized.NatRepr , module Data.Parameterized.SymbolRepr , module What4.BaseTypes - , FloatInfo - , HalfFloat - , SingleFloat - , DoubleFloat - , QuadFloat - , X86_80Float - , DoubleDoubleFloat - , FloatInfoRepr(..) - , FloatInfoToBitWidth - , floatInfoToBVTypeRepr + , module What4.InterpretedFloatingPoint ) where import Data.Hashable From 39e9c1e794d8890c4046da25aa91688034112e37 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:02:40 +0000 Subject: [PATCH 10/35] Derive Show. --- crucible/src/Lang/Crucible/Backend/ProofGoals.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index dada74071..38ea32b42 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -166,7 +166,7 @@ traverseGoalsWithAssumptions f gls = -- primarily a debugging aid, to ensure that stack management -- remains well-bracketed. newtype FrameIdentifier = FrameIdentifier Word64 - deriving(Eq,Ord) + deriving(Eq,Ord,Show) -- | A data-strucutre that can incrementally collect goals in context. From 63f2c2a665a8a79f4caa193ec845e41ca3973a02 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:14:28 +0000 Subject: [PATCH 11/35] Add updateHandleMap. --- crucible/src/Lang/Crucible/FunctionHandle.hs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/crucible/src/Lang/Crucible/FunctionHandle.hs b/crucible/src/Lang/Crucible/FunctionHandle.hs index 269d086bd..6bb84138c 100644 --- a/crucible/src/Lang/Crucible/FunctionHandle.hs +++ b/crucible/src/Lang/Crucible/FunctionHandle.hs @@ -34,6 +34,7 @@ module Lang.Crucible.FunctionHandle , emptyHandleMap , insertHandleMap , lookupHandleMap + , updateHandleMap , searchHandleMap , handleMapToHandles -- * Reference cells @@ -44,6 +45,7 @@ module Lang.Crucible.FunctionHandle import Data.Hashable import Data.Kind +import Data.Functor.Identity import qualified Data.List as List import Data.Ord (comparing) @@ -217,6 +219,19 @@ lookupHandleMap hdl (FnHandleMap m) = Just (HandleElt _ x) -> Just x Nothing -> Nothing +-- | Update the entry of the function handle in the map. +updateHandleMap :: (f args ret -> f args ret) + -> FnHandle args ret + -> FnHandleMap f + -> FnHandleMap f +updateHandleMap f hdl (FnHandleMap m) = + FnHandleMap $ MapF.updatedValue $ runIdentity $ + MapF.updateAtKey + (handleID hdl) + (Identity Nothing) + (\(HandleElt hdl' x) -> Identity $ MapF.Set $ HandleElt hdl' $ f x) + m + -- | Lookup the function name in the map by a linear scan of all -- entries. This will be much slower than using 'lookupHandleMap' to -- find the function by ID, so the latter should be used if possible. From f5422da589b5b5124e99047b5be1a6edde71d39a Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:27:43 +0000 Subject: [PATCH 12/35] Add parentWTOComponent. --- .../Crucible/Analysis/Fixpoint/Components.hs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs index db296717b..a834f9d5c 100644 --- a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs +++ b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs @@ -21,6 +21,7 @@ module Lang.Crucible.Analysis.Fixpoint.Components ( weakTopologicalOrdering, WTOComponent(..), SCC(..), + parentWTOComponent, -- * Special cases cfgWeakTopologicalOrdering, cfgSuccessors, @@ -239,6 +240,23 @@ unlabeled = Label 0 maxLabel :: Label maxLabel = Label maxBound +-- | Construct a map from each vertex to the head of its parent WTO component. +-- In particular, the head of a component is mapped to itself. The top vertices +-- are not in the map. +parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n +parentWTOComponent = F.foldMap' $ \case + SCC scc' -> parentWTOComponent' scc' + Vertex{} -> M.empty + +parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n +parentWTOComponent' scc = M.singleton (wtoHead scc) (wtoHead scc) <> + F.foldMap' + (\case + SCC scc' -> parentWTOComponent' scc' + Vertex v -> M.singleton v $ wtoHead scc) + (wtoComps scc) + + {- Note [Bourdoncle Components] Bourdoncle components are a weak topological ordering of graph From 8813bd4ae3674734389fcadc452c045f86fdd903 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 04:56:58 +0000 Subject: [PATCH 13/35] Export writeSourceSize. --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index c004e26ea..735575e85 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -68,6 +68,7 @@ module Lang.Crucible.LLVM.MemModel.MemLog -- * Write ranges , writeRangesMem + , writeSourceSize -- * Concretization , concPtr From 72d90c0df7069a0359d83ad710b9b5481299de2b Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 05:16:26 +0000 Subject: [PATCH 14/35] Add runCHC and helpers. --- crucible/src/Lang/Crucible/Backend.hs | 66 +++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 69aa1f43c..f8adec788 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -95,6 +95,11 @@ module Lang.Crucible.Backend , addFailedAssertion , assertIsInteger , readPartExpr + , runCHC + , proofObligationsAsImplications + , convertProofObligationsAsImplications + , proofObligationsUninterpConstants + , pathConditionUninterpConstants , ppProofObligation , backendOptions , assertThenAssumeConfigOption @@ -110,17 +115,25 @@ import Data.Functor.Identity import Data.Functor.Const import qualified Data.Sequence as Seq import Data.Sequence (Seq) +import Data.Set (Set) import qualified Prettyprinter as PP import GHC.Stack +import System.IO + +import Data.Parameterized.Map (MapF) import What4.Concrete import What4.Config +import What4.Expr.Builder import What4.Interface import What4.InterpretedFloatingPoint import What4.LabeledPred import What4.Partial import What4.ProgramLoc import What4.Expr (GroundValue, GroundValueWrapper(..)) +import What4.Solver +import qualified What4.Solver.CVC5 as CVC5 +import qualified What4.Solver.Z3 as Z3 import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG @@ -613,6 +626,59 @@ readPartExpr bak (PE p v) msg = do addAssertion bak (LabeledPred p (SimError loc msg)) return v + +-- | Run the CHC solver on the current proof obligations, and return the +-- solution as a substitution from the uninterpreted functions to their +-- definitions. +runCHC :: + (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) => + bak -> + [SomeSymFn sym] -> + m (MapF (SymFnWrapper sym) (SymFnWrapper sym)) +runCHC bak uninterp_inv_fns = liftIO $ do + let sym = backendGetSym bak + + implications <- proofObligationsAsImplications bak + clearProofObligations bak + + -- log to stdout + let logData = defaultLogData + { logCallbackVerbose = \_ -> putStrLn + , logReason = "SAW inv" + } + Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case + Sat sub -> return sub + Unsat{} -> fail "Prover returned Infeasible" + Unknown -> fail "Prover returned Fail" + + +-- | Get proof obligations as What4 implications. +proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym] +proofObligationsAsImplications bak = do + let sym = backendGetSym bak + convertProofObligationsAsImplications sym =<< getProofObligations bak + +-- | Convert proof obligations to What4 implications. +convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym] +convertProofObligationsAsImplications sym goals = do + let obligations = maybe [] PG.goalsToList goals + forM obligations $ \(AS.ProofGoal hyps (LabeledPred concl _err)) -> do + hyp <- assumptionsPred sym hyps + impliesPred sym hyp concl + +-- | Get the set of uninterpreted constants that appear in the path condition. +pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym))) +pathConditionUninterpConstants bak = do + let sym = backendGetSym bak + exprUninterpConstants sym <$> getPathCondition bak + +-- | Get the set of uninterpreted constants that appear in the proof obligations. +proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym))) +proofObligationsUninterpConstants bak = do + let sym = backendGetSym bak + foldMap (exprUninterpConstants sym) <$> proofObligationsAsImplications bak + + ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann) ppProofObligation sym (AS.ProofGoal asmps gl) = do as <- flattenAssumptions sym asmps From 34651c6b1b977b83dfebae8a17365c5e18dc15df Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 08:24:45 +0000 Subject: [PATCH 15/35] Bump what4. --- dependencies/what4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dependencies/what4 b/dependencies/what4 index 28744e48e..670c8aca5 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 28744e48e01dc9c35d5aeebb914a9bb425cfe0f1 +Subproject commit 670c8aca552e8b748b20d127d1310430880a45e8 From 803a8bef50f9b39039d3d4520c7ded9734191f60 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 19 Jan 2024 05:17:14 +0000 Subject: [PATCH 16/35] wip --- .../Lang/Crucible/LLVM/MemModel/Generic.hs | 7 +- .../Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 1339 ++++++++++++----- .../Lang/Crucible/LLVM/SimpleLoopInvariant.hs | 6 + .../Crucible/Analysis/Fixpoint/Components.hs | 2 +- crucible/src/Lang/Crucible/Backend.hs | 9 + 5 files changed, 954 insertions(+), 409 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index c2439fdc4..8803c54fe 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -790,9 +790,10 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) = else do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be -- sure it always fails. But, because it's a variable, it won't be constant-folded away -- and we can be relatively sure the annotation will survive. - b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr - Partial.Err <$> - Partial.annotateME sym mop (NoSatisfyingWrite tp) b + -- b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr + -- Partial.Err <$> + -- Partial.annotateME sym mop (NoSatisfyingWrite tp) b + Partial.partErr sym mop (NoSatisfyingWrite tp) go :: (StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) -> LLVMPtr sym w -> diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs index af22ea5f1..5c356f881 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -11,40 +11,53 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TupleSections #-} module Lang.Crucible.LLVM.SimpleLoopFixpoint ( FixpointEntry(..) + , FixpointState(..) + , CallFrameContext(..) + , SomeCallFrameContext(..) + , ExecutionFeatureContext(..) , simpleLoopFixpoint ) where import Control.Lens -import Control.Monad (when) -import Control.Monad.IO.Class (MonadIO(..)) -import Control.Monad.Reader (ReaderT(..)) -import Control.Monad.State (MonadState(..), StateT(..)) +import Control.Monad +import Control.Monad.IO.Class +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.State import Control.Monad.Trans.Maybe -import Data.Either import Data.Foldable import qualified Data.IntMap as IntMap import Data.IORef +import Data.Kind import qualified Data.List as List import Data.Maybe import qualified Data.Map as Map import Data.Map (Map) +import qualified Data.Sequence as Seq import qualified Data.Set as Set +import Data.Set (Set) +import GHC.TypeLits import qualified System.IO -import Numeric.Natural import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes @@ -52,15 +65,19 @@ import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Map (MapF) import Data.Parameterized.NatRepr +import Data.Parameterized.Some import Data.Parameterized.TraversableF import Data.Parameterized.TraversableFC import qualified What4.Config as W4 +import qualified What4.Expr.Builder as W4 import qualified What4.Interface as W4 +import qualified What4.Solver as W4 import qualified Lang.Crucible.Analysis.Fixpoint.Components as C import qualified Lang.Crucible.Backend as C import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.FunctionHandle as C import qualified Lang.Crucible.Panic as C import qualified Lang.Crucible.Simulator.CallFrame as C import qualified Lang.Crucible.Simulator.EvalStmt as C @@ -76,6 +93,7 @@ import qualified Lang.Crucible.LLVM.MemModel as C import qualified Lang.Crucible.LLVM.MemModel.MemLog as C hiding (Mem) import qualified Lang.Crucible.LLVM.MemModel.Pointer as C import qualified Lang.Crucible.LLVM.MemModel.Type as C +-- import qualified Lang.Crucible.LLVM.MemModel.Generic as C (writeArrayMem) -- | When live loop-carried dependencies are discovered as we traverse @@ -96,53 +114,70 @@ data FixpointEntry sym tp = FixpointEntry } instance OrdF (W4.SymExpr sym) => OrdF (FixpointEntry sym) where - compareF x y = case compareF (headerValue x) (headerValue y) of - LTF -> LTF - EQF -> compareF (bodyValue x) (bodyValue y) - GTF -> GTF - + compareF x y = joinOrderingF + (compareF (headerValue x) (headerValue y)) + (compareF (bodyValue x) (bodyValue y)) instance OrdF (FixpointEntry sym) => W4.TestEquality (FixpointEntry sym) where - testEquality x y = case compareF x y of - EQF -> Just Refl - _ -> Nothing + testEquality x y = orderingF_refl $ compareF x y -data MemFixpointEntry sym = forall w . (1 <= w) => MemFixpointEntry - { memFixpointEntrySym :: sym - , memFixpointEntryJoinVariable :: W4.SymBV sym w +data MemLocation sym w = MemLocation + { memLocationBlock :: Natural + , memLocationOffset :: W4.SymBV sym w + , memLocationSize :: W4.SymBV sym w } +instance OrdF (W4.SymExpr sym) => Ord (MemLocation sym w) where + compare x y = + compare (memLocationBlock x) (memLocationBlock y) + <> toOrdering (compareF (memLocationOffset x) (memLocationOffset y)) + <> toOrdering (compareF (memLocationSize x) (memLocationSize y)) +instance OrdF (W4.SymExpr sym) => Eq (MemLocation sym w) where + x == y = EQ == compare x y + +data MemFixpointEntry sym wptr where + MemStoreFixpointEntry :: + (1 <= w) => + W4.SymBV sym w {- ^ bitvector join variable -} -> + C.StorageType -> + MemFixpointEntry sym wptr + MemArrayFixpointEntry :: + W4.SymArray sym (C.SingleCtx (W4.BaseBVType wptr)) (W4.BaseBVType 8) {- ^ array join variable -} -> + W4.SymBV sym wptr {- ^ length of the allocation -} -> + MemFixpointEntry sym wptr + + -- | This datatype captures the state machine that progresses as we -- attempt to compute a loop invariant for a simple structured loop. -data FixpointState sym blocks +data FixpointState sym wptr blocks args -- | We have not yet encoundered the loop head = BeforeFixpoint -- | We have encountered the loop head at least once, and are in the process -- of converging to an inductive representation of the live variables -- in the loop. - | ComputeFixpoint (FixpointRecord sym blocks) + | ComputeFixpoint (FixpointRecord sym wptr blocks args) -- | We have found an inductively-strong representation of the live variables -- of the loop, and have discovered the loop index structure controling the -- execution of the loop. We are now executing the loop once more to compute -- verification conditions for executions that reamain in the loop. | CheckFixpoint - (FixpointRecord sym blocks) - (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find + (FixpointRecord sym wptr blocks args) + (W4.SomeSymFn sym) -- ^ function that represents the loop invariant + (Some (Ctx.Assignment (W4.SymExpr sym))) -- ^ arguments to the loop invariant + (W4.Pred sym) -- ^ predicate that represents the loop condition -- | Finally, we stitch everything we have found together into the rest of the program. -- Starting from the loop header one final time, we now force execution to exit the loop -- and continue into the rest of the program. | AfterFixpoint - (FixpointRecord sym blocks) - (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find + (FixpointRecord sym wptr blocks args) -- | Data about the loop that we incrementally compute as we approach fixpoint. -data FixpointRecord sym blocks = forall args. - FixpointRecord +data FixpointRecord sym wptr blocks args = FixpointRecord { -- | Block identifier of the head of the loop - fixpointBlockId :: C.Some (C.BlockID blocks) + fixpointBlockId :: C.BlockID blocks args -- | identifier for the currently-active assumption frame related to this fixpoint computation , fixpointAssumptionFrameIdentifier :: C.FrameIdentifier @@ -156,23 +191,159 @@ data FixpointRecord sym blocks = forall args. , fixpointRegMap :: C.RegMap sym args -- | Triples are (blockId, offset, size) to bitvector-typed entries ( bitvector only/not pointers ) - , fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) + , fixpointMemSubstitution :: Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) + + , fixpointEqualitySubstitution :: MapF (W4.SymExpr sym) (W4.SymExpr sym) + + -- | The loop index variable + , fixpointIndex :: W4.SymBV sym wptr + } + + +data CallFrameContext sym wptr ext init ret blocks = CallFrameContext + { callFrameContextFixpointStates :: MapF (C.BlockID blocks) (FixpointState sym wptr blocks) + , callFrameContextLoopHeaders :: [C.Some (C.BlockID blocks)] + , callFrameContextCFG :: C.CFG ext blocks init ret + , callFrameContextParentLoop :: Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks)) + , callFrameContextLoopHeaderBlockIds :: Set (C.Some (C.BlockID blocks)) + } - -- | Condition which, when true, stays in the loop. This is captured when the (unique, by assumption) - -- symbolic branch that exits the loop is encountered. This condition is updated on each iteration - -- as we widen the invariant. - , fixpointLoopCondition :: Maybe (W4.Pred sym) +data CallFrameHandle init ret blocks = CallFrameHandle (C.FnHandle init ret) (Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks) + deriving (Eq, Ord, Show) + +data SomeCallFrameContext sym wptr ext init ret = + forall blocks . SomeCallFrameContext (CallFrameContext sym wptr ext init ret blocks) + +unwrapSomeCallFrameContext :: + Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks -> + SomeCallFrameContext sym wptr ext init ret -> + CallFrameContext sym wptr ext init ret blocks +unwrapSomeCallFrameContext blocks_repr (SomeCallFrameContext ctx) = + case W4.testEquality blocks_repr (fmapFC C.blockInputs $ C.cfgBlockMap $ callFrameContextCFG ctx) of + Just Refl -> ctx + Nothing -> C.panic "SimpleLoopFixpoint.unwrapSomeCallFrameContext" ["type mismatch"] + +data ExecutionFeatureContext sym wptr ext = ExecutionFeatureContext + { executionFeatureContextFixpointStates :: C.FnHandleMap (SomeCallFrameContext sym wptr ext) + , executionFeatureContextInvPreds :: [W4.SomeSymFn sym] + , executionFeatureContextLoopFunEquivConds :: [W4.Pred sym] } +callFrameContextLookup :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + CallFrameContext sym wptr ext init ret blocks +callFrameContextLookup (CallFrameHandle hdl blocks_repr) ctx = + unwrapSomeCallFrameContext blocks_repr $ + fromMaybe (C.panic "SimpleLoopFixpoint.callFrameContextLookup" ["missing call frame context", show hdl]) $ + C.lookupHandleMap hdl (executionFeatureContextFixpointStates ctx) + +callFrameContextUpdate :: + CallFrameHandle init ret blocks -> + (CallFrameContext sym wptr ext init ret blocks -> CallFrameContext sym wptr ext init ret blocks) -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextUpdate (CallFrameHandle hdl blocks_repr) f ctx = + ctx + { executionFeatureContextFixpointStates = C.updateHandleMap + (SomeCallFrameContext . f . unwrapSomeCallFrameContext blocks_repr) + hdl + (executionFeatureContextFixpointStates ctx) + } + +callFrameContextLookup' :: + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + ExecutionFeatureContext sym wptr ext -> + Maybe (FixpointState sym wptr blocks args) +callFrameContextLookup' hdl bid ctx = + MapF.lookup bid $ callFrameContextFixpointStates $ callFrameContextLookup hdl ctx + +callFrameContextInsert :: + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + FixpointState sym wptr blocks args -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextInsert hdl bid fs = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextFixpointStates = MapF.insert bid fs (callFrameContextFixpointStates ctx) } + +callFrameContextPush :: + CallFrameHandle init ret blocks -> + C.Some (C.BlockID blocks) -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextPush hdl bid = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextLoopHeaders = bid : callFrameContextLoopHeaders ctx } + +callFrameContextPop :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextPop hdl = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextLoopHeaders = tail $ callFrameContextLoopHeaders ctx } + +callFrameContextPeek :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Maybe (C.Some (C.BlockID blocks)) +callFrameContextPeek hdl ctx = + listToMaybe $ callFrameContextLoopHeaders $ callFrameContextLookup hdl ctx + +callFrameContextLoopHeaderBlockIds' :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Set (C.Some (C.BlockID blocks)) +callFrameContextLoopHeaderBlockIds' hdl = + callFrameContextLoopHeaderBlockIds . callFrameContextLookup hdl + +callFrameContextParentLoop' :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks)) +callFrameContextParentLoop' hdl = + callFrameContextParentLoop . callFrameContextLookup hdl + +executionFeatureContextAddCallFrameContext :: + CallFrameHandle init ret blocks -> + CallFrameContext sym wptr ext init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddCallFrameContext (CallFrameHandle hdl _blocks_repr) ctx context = + context + { executionFeatureContextFixpointStates = + C.insertHandleMap hdl (SomeCallFrameContext ctx) (executionFeatureContextFixpointStates context) + } + +executionFeatureContextAddInvPred :: + W4.SomeSymFn sym -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddInvPred inv_pred context = + context { executionFeatureContextInvPreds = inv_pred : executionFeatureContextInvPreds context } + +executionFeatureContextAddLoopFunEquivCond :: + W4.Pred sym -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddLoopFunEquivCond cond context = + context { executionFeatureContextLoopFunEquivConds = cond : executionFeatureContextLoopFunEquivConds context } -fixpointRecord :: FixpointState sym blocks -> Maybe (FixpointRecord sym blocks) -fixpointRecord BeforeFixpoint = Nothing -fixpointRecord (ComputeFixpoint r) = Just r -fixpointRecord (CheckFixpoint r _) = Just r -fixpointRecord (AfterFixpoint r _) = Just r +newtype FixpointMonad sym a = + FixpointMonad (StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO a) + deriving (Functor, Applicative, Monad, MonadIO, MonadFail) -type FixpointMonad sym = StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO +deriving instance s ~ MapF (W4.SymExpr sym) (FixpointEntry sym) => MonadState s (FixpointMonad sym) + +runFixpointMonad :: + FixpointMonad sym a -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + IO (a, MapF (W4.SymExpr sym) (FixpointEntry sym)) +runFixpointMonad (FixpointMonad m) = runStateT m joinRegEntries :: @@ -219,13 +390,15 @@ joinRegEntry sym left right = case C.regType left of return left Nothing -> do liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Nothing" - join_varaible <- liftIO $ W4.freshConstant sym (userSymbol' "reg_join_var") (W4.BaseBVRepr w) + join_variable <- liftIO $ W4.freshConstant sym (W4.safeSymbol "reg_join_var") (W4.BaseBVRepr w) let join_entry = FixpointEntry { headerValue = C.llvmPointerOffset (C.regValue left) , bodyValue = C.llvmPointerOffset (C.regValue right) } - put $ MapF.insert join_varaible join_entry subst - return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) join_varaible + put $ MapF.insert join_variable join_entry subst + return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) join_variable + | Just{} <- W4.asConcrete (C.llvmPointerOffset (C.regValue left)) -> do + return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) (C.llvmPointerOffset (C.regValue left)) | otherwise -> fail $ "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: unsupported pointer base join: " @@ -243,7 +416,7 @@ joinRegEntry sym left right = case C.regType left of ++ show (W4.printSymExpr $ C.regValue left) ++ " \\/ " ++ show (W4.printSymExpr $ C.regValue right) - join_varaible <- liftIO $ W4.freshConstant sym (userSymbol' "macaw_reg") W4.BaseBoolRepr + join_varaible <- liftIO $ W4.freshConstant sym (W4.safeSymbol "macaw_reg") W4.BaseBoolRepr return $ C.RegEntry C.BoolRepr join_varaible C.StructRepr field_types -> do @@ -292,127 +465,200 @@ applySubstitutionRegEntry sym substitution entry = case C.regType entry of _ -> C.panic "SimpleLoopFixpoint.applySubstitutionRegEntry" ["unsupported type: " ++ show (C.regType entry)] -findLoopIndex :: - (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) => - sym -> - MapF (W4.SymExpr sym) (FixpointEntry sym) -> - IO (W4.SymBV sym wptr, Natural, Natural) -findLoopIndex sym substitution = do - candidates <- catMaybes <$> mapM - (\(MapF.Pair variable FixpointEntry{..}) -> case W4.testEquality (W4.BaseBVRepr ?ptrWidth) (W4.exprType variable) of - Just Refl -> do - diff <- liftIO $ W4.bvSub sym bodyValue variable - case (BV.asNatural <$> W4.asBV headerValue, BV.asNatural <$> W4.asBV diff) of - (Just start, Just step) -> do - liftIO $ ?logMessage $ - "SimpleLoopFixpoint.findLoopIndex: " ++ show (W4.printSymExpr variable) ++ "=" ++ show (start, step) - return $ Just (variable, start, step) - _ -> return Nothing - Nothing -> return Nothing) - (MapF.toList substitution) - case candidates of - [candidate] -> return candidate - _ -> fail "SimpleLoopFixpoint.findLoopIndex: loop index identification failure." - -findLoopBound :: +joinMem :: + forall sym wptr . (C.IsSymInterface sym, C.HasPtrWidth wptr) => sym -> - W4.Pred sym -> - Natural -> - Natural -> - IO (W4.SymBV sym wptr) -findLoopBound sym condition _start step = - case Set.toList $ W4.exprUninterpConstants sym condition of - - -- this is a grungy hack, we are expecting exactly three variables and take the first - [C.Some loop_stop, _, _] - | Just Refl <- W4.testEquality (W4.BaseBVRepr ?ptrWidth) (W4.exprType $ W4.varExpr sym loop_stop) -> - W4.bvMul sym (W4.varExpr sym loop_stop) =<< W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral step) - _ -> fail "SimpleLoopFixpoint.findLoopBound: loop bound identification failure." - - --- index variable information for fixed stride, bounded loops -data LoopIndexBound sym = forall w . 1 <= w => LoopIndexBound - { index :: W4.SymBV sym w - , start :: Natural - , stop :: W4.SymBV sym w - , step :: Natural - } + C.MemImpl sym -> + C.MemWrites sym -> + IO (Map (MemLocation sym wptr) (MemFixpointEntry sym wptr)) +joinMem sym mem_impl mem_writes = do + ranges <- maybe (fail "SimpleLoopFixpoint: unsupported symbolic pointers") return =<< + runMaybeT (C.writeRangesMem @_ @wptr sym $ C.memImplHeap mem_impl) + + mem_subst <- case mem_writes of + C.MemWrites [C.MemWritesChunkIndexed indexed_writes] -> Map.fromList . catMaybes <$> mapM + (\case + C.MemWrite ptr mem_source + | Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr) + , Just blk <- W4.asNat (C.llvmPointerBlock ptr) -> do + sz <- maybe (fail "SimpleLoopFixpoint: unsupported MemSource") return =<< + runMaybeT (C.writeSourceSize sym mem_source) + let mem_loc = MemLocation + { memLocationBlock = blk + , memLocationOffset = C.llvmPointerOffset ptr + , memLocationSize = sz + } + + is_loop_local <- and <$> mapM + (\(prev_off, prev_sz) -> do + disjoint_pred <- C.buildDisjointRegionsAssertionWithSub + sym + ptr + sz + (C.LLVMPointer (C.llvmPointerBlock ptr) prev_off) + prev_sz + return $ W4.asConstantPred disjoint_pred == Just True) + (Map.findWithDefault [] blk ranges) + + if not is_loop_local then do + mem_entry <- case mem_source of + C.MemStore _ storage_type _ -> + case W4.mkNatRepr $ C.bytesToBits (C.typeEnd 0 storage_type) of + C.Some bv_width + | Just C.LeqProof <- W4.testLeq (W4.knownNat @1) bv_width -> do + join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.BaseBVRepr bv_width) + return $ MemStoreFixpointEntry join_variable storage_type + | otherwise -> + C.panic + "SimpleLoopFixpoint.simpleLoopFixpoint" + ["unexpected storage type " ++ show storage_type] -findLoopIndexBound :: - (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) => - sym -> - MapF (W4.SymExpr sym) (FixpointEntry sym) -> - Maybe (W4.Pred sym) -> - IO (LoopIndexBound sym) -findLoopIndexBound _sym _substitition Nothing = - fail "findLoopIndexBound: no loop condition recorded!" - -findLoopIndexBound sym substitution (Just condition) = do - (loop_index, start, step) <- findLoopIndex sym substitution - stop <- findLoopBound sym condition start step - return $ LoopIndexBound - { index = loop_index - , start = start - , stop = stop - , step = step - } + C.MemArrayStore arr _ -> do + join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.exprType arr) + return $ MemArrayFixpointEntry join_variable sz + + _ -> fail "SimpleLoopFixpoint.joinMem: unsupported MemSource" + + return $ Just (mem_loc, mem_entry) + + else + return Nothing + + _ -> fail $ "SimpleLoopFixpoint: not MemWrite: " ++ show (C.ppMemWrites mem_writes)) + (List.concat $ IntMap.elems indexed_writes) --- hard-coded here that we are always looking for a loop condition delimited by an unsigned comparison -loopIndexBoundCondition :: - (C.IsSymInterface sym, 1 <= w) => + C.MemWrites [] -> return Map.empty + + _ -> fail $ "SimpleLoopFixpoint: not MemWritesChunkIndexed: " ++ show (C.ppMemWrites mem_writes) + + checkDisjointRegions sym $ Map.keys mem_subst + + return mem_subst + +checkDisjointRegions :: + (C.IsSymInterface sym, C.HasPtrWidth wptr) => sym -> - W4.SymBV sym w -> - W4.SymBV sym w -> - IO (W4.Pred sym) -loopIndexBoundCondition = W4.bvUlt - --- | Describes an assumed invariant on the loop index variable, which is that it is an offset --- from the initial value that is a multiple of a discoveded stride value. -loopIndexStartStepCondition :: - C.IsSymInterface sym => + [MemLocation sym wptr] -> + IO () +checkDisjointRegions sym = \case + hd_mem_loc : tail_mem_locs -> do + mapM_ (checkDisjointRegions' sym hd_mem_loc) tail_mem_locs + checkDisjointRegions sym tail_mem_locs + [] -> return () + +checkDisjointRegions' :: + (C.IsSymInterface sym, C.HasPtrWidth wptr) => sym -> - LoopIndexBound sym -> - IO (W4.Pred sym) -loopIndexStartStepCondition sym LoopIndexBound{ index = loop_index, start = start, step = step } = do - start_bv <- W4.bvLit sym (W4.bvWidth loop_index) (BV.mkBV (W4.bvWidth loop_index) $ fromIntegral start) - step_bv <- W4.bvLit sym (W4.bvWidth loop_index) (BV.mkBV (W4.bvWidth loop_index) $ fromIntegral step) - W4.bvEq sym start_bv =<< W4.bvUrem sym loop_index step_bv + MemLocation sym wptr -> + MemLocation sym wptr -> + IO () +checkDisjointRegions' sym mem_loc1 mem_loc2 = do + ptr1 <- memLocationPtr sym mem_loc1 + ptr2 <- memLocationPtr sym mem_loc2 + disjoint_pred <- C.buildDisjointRegionsAssertionWithSub + sym + ptr1 + (memLocationSize mem_loc1) + ptr2 + (memLocationSize mem_loc2) + when (W4.asConstantPred disjoint_pred /= Just True) $ + fail $ + "SimpleLoopFixpoint: non-disjoint ranges: off1=" + ++ show (W4.printSymExpr $ C.llvmPointerOffset ptr1) + ++ ", sz1=" + ++ show (W4.printSymExpr $ memLocationSize mem_loc1) + ++ ", off2=" + ++ show (W4.printSymExpr $ C.llvmPointerOffset ptr2) + ++ ", sz2=" + ++ show (W4.printSymExpr $ memLocationSize mem_loc2) loadMemJoinVariables :: (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => bak -> C.MemImpl sym -> - Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) -> + Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym)) loadMemJoinVariables bak mem subst = let sym = C.backendGetSym bak in - MapF.fromList <$> mapM - (\((blk, off, _sz), (MemFixpointEntry { memFixpointEntryJoinVariable = join_varaible }, storeage_type)) -> do - ptr <- C.LLVMPointer <$> W4.natLit sym blk <*> W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral off) - val <- C.doLoad bak mem ptr storeage_type (C.LLVMPointerRepr $ W4.bvWidth join_varaible) C.noAlignment - case W4.asNat (C.llvmPointerBlock val) of - Just 0 -> return $ MapF.Pair join_varaible $ C.llvmPointerOffset val - _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val)) + MapF.fromList . catMaybes <$> mapM + (\(mem_loc, mem_entry) -> do + ptr <- memLocationPtr sym mem_loc + case mem_entry of + MemStoreFixpointEntry join_variable storage_type -> do + val <- C.doLoad bak mem ptr storage_type (C.LLVMPointerRepr $ W4.bvWidth join_variable) C.noAlignment + case W4.asNat (C.llvmPointerBlock val) of + Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val + _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val) + -- foo <- C.loadRaw sym mem ptr storage_type C.noAlignment + -- case foo of + -- C.NoErr _p val' -> do + -- val <- C.unpackMemValue sym (C.LLVMPointerRepr $ W4.bvWidth join_variable) val' + -- case W4.asNat (C.llvmPointerBlock val) of + -- Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val + -- _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val) + -- C.Err{} -> -- return Nothing + -- fail $ "SimpleLoopFixpoint.loadMemJoinVariables: loadRaw failed" + MemArrayFixpointEntry join_variable size -> do + -- TODO: handle arrays + maybe_allocation_array <- C.asMemAllocationArrayStore sym ?ptrWidth ptr (C.memImplHeap mem) + case maybe_allocation_array of + Just (ok, arr, arr_sz) | Just True <- W4.asConstantPred ok -> do + return $ Just $ MapF.Pair join_variable arr + _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables") (Map.toAscList subst) storeMemJoinVariables :: (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => bak -> C.MemImpl sym -> - Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) -> + Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) -> MapF (W4.SymExpr sym) (W4.SymExpr sym) -> IO (C.MemImpl sym) -storeMemJoinVariables bak mem mem_subst eq_subst = - let sym = C.backendGetSym bak in +storeMemJoinVariables bak mem mem_subst eq_subst = do + let sym = C.backendGetSym bak foldlM - (\mem_acc ((blk, off, _sz), (MemFixpointEntry { memFixpointEntryJoinVariable = join_varaible }, storeage_type)) -> do - ptr <- C.LLVMPointer <$> W4.natLit sym blk <*> W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral off) - C.doStore bak mem_acc ptr (C.LLVMPointerRepr $ W4.bvWidth join_varaible) storeage_type C.noAlignment =<< - C.llvmPointer_bv sym (MapF.findWithDefault join_varaible join_varaible eq_subst)) - mem - (Map.toAscList mem_subst) + (\mem_acc (mem_loc, mem_entry) -> do + ptr <- memLocationPtr sym mem_loc + case mem_entry of + MemStoreFixpointEntry join_variable storage_type -> do + C.doStore bak mem_acc ptr (C.LLVMPointerRepr $ W4.bvWidth join_variable) storage_type C.noAlignment =<< + C.llvmPointer_bv sym (findWithDefaultKey eq_subst join_variable) + MemArrayFixpointEntry join_variable size -> do + C.doArrayStore bak mem_acc ptr C.noAlignment (findWithDefaultKey eq_subst join_variable) size) + -- (heap, p1, p2) <- C.writeArrayMem + -- sym + -- ?ptrWidth + -- ptr + -- C.noAlignment + -- (findWithDefaultKey eq_subst join_variable) + -- (Just size) + -- (C.memImplHeap mem_acc) + -- return $ mem_acc { C.memImplHeap = heap }) + mem + (Map.toAscList mem_subst) + +memLocationPtr :: + C.IsSymInterface sym => + sym -> + MemLocation sym wptr -> + IO (C.LLVMPtr sym wptr) +memLocationPtr sym (MemLocation { memLocationBlock = blk, memLocationOffset = off }) = + C.LLVMPointer <$> W4.natLit sym blk <*> return off + + +applySubstitutionMemFixpointEntries :: + (C.IsSymInterface sym, Functor f) => + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + f (MemFixpointEntry sym wptr) -> + f (MemFixpointEntry sym wptr) +applySubstitutionMemFixpointEntries substitution = fmap $ \case + MemStoreFixpointEntry join_variable storage_type -> + MemStoreFixpointEntry (findWithDefaultKey substitution join_variable) storage_type + MemArrayFixpointEntry join_variable size -> + MemArrayFixpointEntry (findWithDefaultKey substitution join_variable) size + dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym) dropMemStackFrame mem = case (C.memImplHeap mem) ^. C.memState of @@ -433,47 +679,144 @@ filterSubstitution sym substitution = in MapF.filterWithKey (\variable _entry -> Set.member (C.Some variable) uninterp_constants) substitution +loopIndexLinearSubstitution :: + (C.IsSymInterface sym, C.HasPtrWidth wptr, MonadIO m) => + sym -> + W4.SymBV sym wptr -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + m (MapF (W4.SymExpr sym) (W4.SymExpr sym)) +loopIndexLinearSubstitution sym index_variable = + MapF.traverseMaybeWithKey + (\variable entry -> case W4.testEquality (W4.exprType variable) (W4.exprType index_variable) of + Just Refl -> do + diff <- liftIO $ W4.bvSub sym (bodyValue entry) variable + case W4.asBV diff of + Just{} -> liftIO $ Just <$> (W4.bvAdd sym (headerValue entry) =<< W4.bvMul sym index_variable diff) + Nothing -> return Nothing + Nothing -> return Nothing) + -- find widening variables that are actually the same (up to syntactic equality) -- and can be substituted for each other uninterpretedConstantEqualitySubstitution :: - forall sym . - C.IsSymInterface sym => + (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m) => sym -> MapF (W4.SymExpr sym) (FixpointEntry sym) -> - (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym)) -uninterpretedConstantEqualitySubstitution _sym substitution = + m (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym)) +uninterpretedConstantEqualitySubstitution sym substitution = do let reverse_substitution = MapF.foldlWithKey' (\accumulator variable entry -> MapF.insert entry variable accumulator) MapF.empty substitution - uninterpreted_constant_substitution = fmapF - (\entry -> fromJust $ MapF.lookup entry reverse_substitution) + let uninterpreted_constant_substitution = + MapF.filterWithKey (\variable entry -> isNothing $ W4.testEquality variable entry) $ + fmapF (\entry -> fromJust $ MapF.lookup entry reverse_substitution) substitution - normal_substitution = MapF.filterWithKey - (\variable _entry -> - Just Refl == W4.testEquality variable (fromJust $ MapF.lookup variable uninterpreted_constant_substitution)) + let normal_substitution = MapF.filterWithKey + (\variable _entry -> isNothing $ MapF.lookup variable uninterpreted_constant_substitution) substitution - in - (normal_substitution, uninterpreted_constant_substitution) - -userSymbol' :: String -> W4.SolverSymbol -userSymbol' = fromRight (C.panic "SimpleLoopFixpoint.userSymbol'" []) . W4.userSymbol + liftIO $ putStrLn $ "vars:" + mapM_ + (\(MapF.Pair variable entry) -> do + let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + liftIO $ putStrLn $ show (W4.printSymExpr variable) ++ " :: "++ show (W4.exprType variable) ++ " -> " ++ (show $ Set.map (C.viewSome $ show . W4.printSymExpr) $ body_vars)) + (MapF.toList normal_substitution) + + foo <- MapF.fromList <$> filterM + (\(MapF.Pair variable entry) -> do + let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + if Set.notMember (C.Some variable) body_vars then do + let lalala = runIdentity $ MapF.fromKeysM (return . W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + let foobar = fmapF headerValue $ MapF.mapMaybe (\v -> MapF.lookup v normal_substitution) lalala + bar <- liftIO $ W4.isEq sym (headerValue entry) =<< W4.substituteBoundVars sym foobar (bodyValue entry) + liftIO $ putStrLn $ "la: " ++ (show $ W4.printSymExpr variable) + liftIO $ putStrLn $ "headerValue entry: " ++ (show $ W4.printSymExpr $ headerValue entry) + liftIO $ putStrLn $ "bodyValue entry:" ++ (show $ W4.printSymExpr $ bodyValue entry) + liftIO $ putStrLn $ "bar: " ++ (show $ W4.printSymExpr $ bar) + if Just True == W4.asConstantPred bar then do + liftIO $ putStrLn "lala" + return True + else do + notbar <- liftIO $ W4.notPred sym bar + lala <- liftIO $ W4.runZ3InOverride sym (W4.defaultLogData { W4.logVerbosity = 2 }) [notbar] $ return . W4.isUnsat + when lala $ do + liftIO $ putStrLn "lalala" + return lala + else + return False) + (MapF.toList normal_substitution) + + unless (Set.disjoint (Set.fromList $ MapF.keys foo) (foldMapF (Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) $ fmapF bodyValue foo)) $ + fail "SimpleLoopFixpoint: uninterpretedConstantEqualitySubstitution: not disjoint" + + return + ( MapF.mergeWithKey (\_ _ _ -> Nothing) id (const MapF.empty) normal_substitution foo -- difference + , MapF.mergeWithKey (\_ _ -> Just) id id uninterpreted_constant_substitution $ fmapF bodyValue foo -- union + ) + + +-- -- | Given the WTO analysis results, find the nth loop. +-- -- Return the identifier of the loop header, and a list of all the blocks +-- -- that are part of the loop body. It is at this point that we check +-- -- that the loop has the necessary properties; there must be a single +-- -- entry point to the loop, and it must have a single back-edge. Otherwise, +-- -- the analysis will not work correctly. +-- computeLoopBlocks :: forall ext blocks init ret k . +-- (k ~ C.Some (C.BlockID blocks)) => +-- C.CFG ext blocks init ret -> +-- Integer -> +-- IO (k, [k]) +-- computeLoopBlocks cfg loopNum = +-- case List.genericDrop loopNum (Map.toList loop_map) of +-- [] -> fail ("Did not find " ++ show loopNum ++ " loop headers") +-- (p:_) -> do checkSingleEntry p +-- checkSingleBackedge p +-- return p + +-- where +-- -- There should be exactly one block which is not part of the loop body that +-- -- can jump to @hd@. +-- checkSingleEntry :: (k,[k]) -> IO () +-- checkSingleEntry (hd, body) = +-- case filter (\x -> not (elem x body) && elem hd (C.cfgSuccessors cfg x)) allReachable of +-- [_] -> return () +-- _ -> fail "SimpleLoopInvariant feature requires a single-entry loop!" + +-- -- There should be exactly on block in the loop body which can jump to @hd@. +-- checkSingleBackedge :: (k,[k]) -> IO () +-- checkSingleBackedge (hd, body) = +-- case filter (\x -> elem hd (C.cfgSuccessors cfg x)) body of +-- [_] -> return () +-- _ -> fail "SimpleLoopInvariant feature requires a loop with a single backedge!" + +-- flattenWTOComponent = \case +-- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps +-- C.Vertex v -> [v] + +-- loop_map = Map.fromList $ mapMaybe +-- (\case +-- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) +-- C.Vertex{} -> Nothing) +-- wto + +-- allReachable = concatMap flattenWTOComponent wto + +-- wto = C.cfgWeakTopologicalOrdering cfg -- | This execution feature is designed to allow a limited form of -- verification for programs with unbounded looping structures. -- --- It is currently highly experimental and has many limititations. --- Most notibly, it only really works properly for functions --- consiting of a single, non-nested loop with a single exit point. +-- It is currently highly experimental and has many limitations. +-- Most notably, it only really works properly for functions +-- consisting of a single, non-nested loop with a single exit point. -- Moreover, the loop must have an indexing variable that counts up -- from a starting point by a fixed stride amount. -- --- Currently, these assumptions about the loop strucutre are not +-- Currently, these assumptions about the loop structure are not -- checked. -- --- The basic use case here is for verifiying functions that loop +-- The basic use case here is for verifying functions that loop -- through an array of data of symbolic length. This is done by -- providing a \""fixpoint function\" which describes how the live -- values in the loop at an arbitrary iteration are used to compute @@ -481,159 +824,220 @@ userSymbol' = fromRight (C.panic "SimpleLoopFixpoint.userSymbol'" []) . W4.userS -- loop. The number and order of these variables depends on -- internal details of the representation, so is relatively fragile. simpleLoopFixpoint :: - forall sym ext p rtp blocks init ret . - (C.IsSymInterface sym, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => sym -> C.CFG ext blocks init ret {- ^ The function we want to verify -} -> C.GlobalVar C.Mem {- ^ global variable representing memory -} -> - (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) -> - IO (C.ExecutionFeature p sym ext rtp) -simpleLoopFixpoint sym cfg@C.CFG{..} mem_var fixpoint_func = do - let ?ptrWidth = knownNat @64 - + Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) -> + IO (C.ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext)) +simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do verbSetting <- W4.getOptionSetting W4.verbosity $ W4.getConfiguration sym verb <- fromInteger <$> W4.getOpt verbSetting + -- let loop_map = Map.fromList $ mapMaybe + -- (\case + -- scc@(C.SCC _) -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) + -- C.Vertex{} -> Nothing) + -- (C.cfgWeakTopologicalOrdering cfg) + -- Doesn't really work if there are nested loops: looop datastructures will -- overwrite each other. Currently no error message. -- Really only works for single-exit loops; need a message for that too. - let flattenWTOComponent = \case - C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps - C.Vertex v -> [v] - let loop_map = Map.fromList $ mapMaybe - (\case - C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) - C.Vertex{} -> Nothing) - (C.cfgWeakTopologicalOrdering cfg) + -- let flattenWTOComponent = \case + -- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps + -- C.Vertex v -> [v] + -- let loop_map = Map.fromList $ mapMaybe + -- (\case + -- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) + -- C.Vertex{} -> Nothing) + -- (C.cfgWeakTopologicalOrdering cfg) + + + -- let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg + -- fixpoint_state_ref <- newIORef $ + -- FrameContext + -- { frameContextFixpointStates = MapF.empty + -- , frameContextLoopHeaders = [] + -- , frameContextCFG = cfg + -- , frameContextParentLoop = parent_wto_component + -- , frameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component + -- } + + fixpoint_state_ref <- newIORef $ + ExecutionFeatureContext + { executionFeatureContextFixpointStates = C.emptyHandleMap + , executionFeatureContextInvPreds = [] + , executionFeatureContextLoopFunEquivConds = [] + } - fixpoint_state_ref <- newIORef @(FixpointState sym blocks) BeforeFixpoint + -- initializeCallFrameContext cfg fixpoint_state_ref - return $ C.ExecutionFeature $ \exec_state -> do - let ?logMessage = \msg -> when (verb >= (3 :: Natural)) $ do + return $ (, fixpoint_state_ref) $ C.ExecutionFeature $ \exec_state -> do + -- let ?logMessage = \msg -> when (verb >= (3 :: Natural)) $ do + let ?logMessage = \msg -> do let h = C.printHandle $ C.execStateContext exec_state System.IO.hPutStrLn h msg System.IO.hFlush h - fixpoint_state <- readIORef fixpoint_state_ref - C.withBackend (C.execStateContext exec_state) $ \bak -> - case exec_state of - C.RunningState (C.RunBlockStart block_id) sim_state - | C.SomeHandle cfgHandle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) - - -- make sure the types match - , Just Refl <- W4.testEquality - (fmapFC C.blockInputs cfgBlockMap) - (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) - -- loop map is what we computed above, is this state at a loop header - , Map.member (C.Some block_id) loop_map -> - - advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state fixpoint_state_ref - - | otherwise -> do + -- cfg_handle <- C.cfgHandle . callFrameContextCFG <$> readIORef fixpoint_state_ref + -- cfg_block_map <- C.cfgBlockMap . callFrameContextCFG <$> readIORef fixpoint_state_ref + -- parent_loop_map <- callFrameContextParentLoop <$> readIORef fixpoint_state_ref + -- loop_header_block_ids <- callFrameContextLoopHeaderBlockIds <$> readIORef fixpoint_state_ref + -- maybe_some_loop_block_id <- callFrameContextPeek <$> readIORef fixpoint_state_ref + C.withBackend (C.execStateContext exec_state) $ \bak -> case exec_state of + C.RunningState (C.RunBlockStart block_id) sim_state + | SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do + loop_header_block_ids <- callFrameContextLoopHeaderBlockIds' call_frame_handle <$> readIORef fixpoint_state_ref + if Set.member (C.Some block_id) loop_header_block_ids then do + putStrLn $ "!!!SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref + else do ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id return C.ExecutionFeatureNoChange + -- | C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + -- -- make sure the types match + -- , Just Refl <- W4.testEquality + -- (fmapFC C.blockInputs cfg_block_map) + -- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + -- -- loop map is what we computed above, is this state at a loop header + -- , Set.member (C.Some block_id) loop_header_block_ids -> + -- advanceFixpointState bak mem_var maybe_fixpoint_func cfg_handle block_id sim_state fixpoint_state_ref + + -- | otherwise -> do + -- ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + -- return C.ExecutionFeatureNoChange -- TODO: maybe need to rework this, so that we are sure to capture even concrete exits from the loop. C.SymbolicBranchState branch_condition true_frame false_frame _target sim_state - | Just fixpoint_record <- fixpointRecord fixpoint_state - , Just loop_body_some_block_ids <- Map.lookup (fixpointBlockId fixpoint_record) loop_map - , JustPausedFrameTgtId true_frame_some_block_id <- pausedFrameTgtId true_frame - , JustPausedFrameTgtId false_frame_some_block_id <- pausedFrameTgtId false_frame - , C.SomeHandle cfgHandle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) - , Just Refl <- W4.testEquality - (fmapFC C.blockInputs cfgBlockMap) - (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) - , elem true_frame_some_block_id loop_body_some_block_ids /= elem false_frame_some_block_id loop_body_some_block_ids -> do - - (loop_condition, inside_loop_frame, outside_loop_frame) <- - if elem true_frame_some_block_id loop_body_some_block_ids - then - return (branch_condition, true_frame, false_frame) - else do - not_branch_condition <- W4.notPred sym branch_condition - return (not_branch_condition, false_frame, true_frame) - - (condition, frame) <- case fixpoint_state of - BeforeFixpoint -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint:" ["BeforeFixpoint"] - - ComputeFixpoint _fixpoint_record -> do - -- continue in the loop - ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint" - writeIORef fixpoint_state_ref $ - ComputeFixpoint fixpoint_record { fixpointLoopCondition = Just loop_condition } - return (loop_condition, inside_loop_frame) - - CheckFixpoint _fixpoint_record _loop_bound -> do - -- continue in the loop - ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint" - return (loop_condition, inside_loop_frame) - - AfterFixpoint _fixpoint_record _loop_bound -> do - -- break out of the loop - ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint" - not_loop_condition <- W4.notPred sym loop_condition - return (not_loop_condition, outside_loop_frame) - - loc <- W4.getCurrentProgramLoc sym - C.addAssumption bak $ C.BranchCondition loc (C.pausedLoc frame) condition - C.ExecutionFeatureNewState <$> - runReaderT - (C.resumeFrame (C.forgetPostdomFrame frame) $ sim_state ^. (C.stateTree . C.actContext)) + | JustPausedFrameTgtId true_frame_some_block_id <- pausedFrameTgtId true_frame + , JustPausedFrameTgtId false_frame_some_block_id <- pausedFrameTgtId false_frame + , SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do + maybe_some_loop_block_id <- callFrameContextPeek call_frame_handle <$> readIORef fixpoint_state_ref + parent_loop_map <- callFrameContextParentLoop' call_frame_handle <$> readIORef fixpoint_state_ref + -- , C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + -- , Just Refl <- W4.testEquality + -- (fmapFC C.blockInputs cfg_block_map) + -- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + -- , Just (Some loop_block_id) <- maybe_some_loop_block_id + -- , true_frame_parent_loop_id <- Map.lookup true_frame_some_block_id parent_loop_map + -- , false_frame_parent_loop_id <- Map.lookup false_frame_some_block_id parent_loop_map + -- , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do + if| Just (Some loop_block_id) <- maybe_some_loop_block_id + , true_frame_parent_loop_id <- if true_frame_some_block_id /= C.Some loop_block_id then Map.lookup true_frame_some_block_id parent_loop_map else maybe_some_loop_block_id + , false_frame_parent_loop_id <- if false_frame_some_block_id /= C.Some loop_block_id then Map.lookup false_frame_some_block_id parent_loop_map else maybe_some_loop_block_id + , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do + putStrLn $ "!!!SimpleLoopFixpoint: SymbolicBranchState: " ++ show (true_frame_some_block_id, false_frame_some_block_id) + handleSymbolicBranch + bak + call_frame_handle + loop_block_id + branch_condition + true_frame + false_frame + true_frame_parent_loop_id + false_frame_parent_loop_id sim_state + fixpoint_state_ref + | otherwise -> do + ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: " ++ show (W4.printSymExpr branch_condition, true_frame_some_block_id, false_frame_some_block_id) + return C.ExecutionFeatureNoChange + + C.CallState _return_handler (C.CrucibleCall _block_id call_frame) _sim_state + | C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do + initializeCallFrameContext callee_cfg fixpoint_state_ref + return C.ExecutionFeatureNoChange + C.TailCallState _value_from_value (C.CrucibleCall _block_id call_frame) _sim_state + | C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do + initializeCallFrameContext callee_cfg fixpoint_state_ref + return C.ExecutionFeatureNoChange _ -> return C.ExecutionFeatureNoChange +initializeCallFrameContext :: + C.CFG ext blocks init ret -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO () +initializeCallFrameContext cfg context_ref = do + putStrLn $ "SimpleLoopFixpoint: cfgHandle: " ++ show (C.cfgHandle cfg) + putStrLn $ "SimpleLoopFixpoint: cfg: " ++ show (toListFC (\b -> (C.Some (C.blockID b), C.nextBlocks b)) $ C.cfgBlockMap cfg) + putStrLn $ "SimpleLoopFixpoint: cfgWeakTopologicalOrdering: " ++ show (C.cfgWeakTopologicalOrdering cfg) + let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg + let call_frame_handle = CallFrameHandle (C.cfgHandle cfg) $ fmapFC C.blockInputs $ C.cfgBlockMap cfg + modifyIORef' context_ref $ executionFeatureContextAddCallFrameContext call_frame_handle $ + CallFrameContext + { callFrameContextFixpointStates = MapF.empty + , callFrameContextLoopHeaders = [] + , callFrameContextCFG = cfg + , callFrameContextParentLoop = parent_wto_component + , callFrameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component + } + + +initializeFixpointState :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + C.GlobalVar C.Mem -> + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO (C.ExecutionFeatureResult p sym ext rtp) +initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + assumption_frame_identifier <- C.pushAssumptionFrame bak + putStrLn $ "!!!SimpleLoopFixpoint: initializeFixpointState: block_id=" ++ show block_id ++ ", assumption_frame_identifier=" ++ show assumption_frame_identifier + index_var <- W4.freshConstant sym (W4.safeSymbol "index_var") W4.knownRepr + let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl } + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint $ + FixpointRecord + { fixpointBlockId = block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = MapF.empty + , fixpointRegMap = sim_state ^. (C.stateCrucibleFrame . C.frameRegs) + , fixpointMemSubstitution = Map.empty + , fixpointEqualitySubstitution = MapF.empty + , fixpointIndex = index_var + } + modifyIORef' fixpoint_state_ref $ callFrameContextPush call_frame_handle $ Some block_id + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + advanceFixpointState :: - forall sym bak ext p rtp blocks r args . - (C.IsSymBackend sym bak, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + (C.IsSymBackend sym bak, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => bak -> C.GlobalVar C.Mem -> - (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) -> + Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) -> + CallFrameHandle init ret blocks -> C.BlockID blocks args -> C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> - FixpointState sym blocks -> - IORef (FixpointState sym blocks) -> + IORef (ExecutionFeatureContext sym wptr ext) -> IO (C.ExecutionFeatureResult p sym ext rtp) -advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state fixpoint_state_ref = - let ?ptrWidth = knownNat @64 in - let sym = C.backendGetSym bak in +advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + fixpoint_state <- fromMaybe BeforeFixpoint <$> callFrameContextLookup' call_frame_handle block_id <$> readIORef fixpoint_state_ref case fixpoint_state of BeforeFixpoint -> do ?logMessage $ "SimpleLoopFixpoint: RunningState: BeforeFixpoint -> ComputeFixpoint" - assumption_frame_identifier <- C.pushAssumptionFrame bak - let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) - let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl } - writeIORef fixpoint_state_ref $ ComputeFixpoint $ - FixpointRecord - { fixpointBlockId = C.Some block_id - , fixpointAssumptionFrameIdentifier = assumption_frame_identifier - , fixpointSubstitution = MapF.empty - , fixpointRegMap = sim_state ^. (C.stateCrucibleFrame . C.frameRegs) - , fixpointMemSubstitution = Map.empty - , fixpointLoopCondition = Nothing -- we don't know the loop condition yet - } - return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ - sim_state & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl - - ComputeFixpoint fixpoint_record - | FixpointRecord { fixpointRegMap = reg_map } <- fixpoint_record - , Just Refl <- W4.testEquality - (fmapFC C.regType $ C.regMap reg_map) - (fmapFC C.regType $ C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs)) -> do - + mapM_ (\g -> print =<< C.ppProofObligation sym g) =<< (maybe [] C.goalsToList <$> C.getProofObligations bak) + initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref + ComputeFixpoint fixpoint_record -> do ?logMessage $ "SimpleLoopFixpoint: RunningState: ComputeFixpoint: " ++ show block_id - _ <- C.popAssumptionFrameAndObligations bak $ fixpointAssumptionFrameIdentifier fixpoint_record + proof_goals_and_assumptions_vars <- Set.map (mapSome $ W4.varExpr sym) <$> + (Set.union <$> C.proofObligationsUninterpConstants bak <*> C.pathConditionUninterpConstants bak) + (frame_assumptions, _) <- C.popAssumptionFrameAndObligations bak $ fixpointAssumptionFrameIdentifier fixpoint_record + loop_condition <- C.assumptionsPred sym frame_assumptions -- widen the inductive condition - (join_reg_map, join_substitution) <- runStateT + (join_reg_map, join_substitution) <- runFixpointMonad (joinRegEntries sym - (C.regMap reg_map) + (C.regMap $ fixpointRegMap fixpoint_record) (C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs))) $ fixpointSubstitution fixpoint_record @@ -643,57 +1047,7 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state fail "SimpleLoopFixpoint: unsupported memory allocation in loop body." -- widen the memory - mem_substitution_candidate <- Map.fromList <$> catMaybes <$> case mem_writes of - C.MemWrites [C.MemWritesChunkIndexed mmm] -> mapM - (\case - (C.MemWrite ptr (C.MemStore _ storeage_type _)) - | Just blk <- W4.asNat (C.llvmPointerBlock ptr) - , Just off <- BV.asNatural <$> W4.asBV (C.llvmPointerOffset ptr) -> do - let sz = C.typeEnd 0 storeage_type - some_join_varaible <- liftIO $ case W4.mkNatRepr $ C.bytesToBits sz of - C.Some bv_width - | Just C.LeqProof <- W4.testLeq (W4.knownNat @1) bv_width -> do - join_varaible <- W4.freshConstant sym - (userSymbol' "mem_join_var") - (W4.BaseBVRepr bv_width) - return $ MemFixpointEntry - { memFixpointEntrySym = sym - , memFixpointEntryJoinVariable = join_varaible - } - | otherwise -> - C.panic - "SimpleLoopFixpoint.simpleLoopFixpoint" - ["unexpected storage type " ++ show storeage_type ++ " of size " ++ show sz] - return $ Just ((blk, off, fromIntegral sz), (some_join_varaible, storeage_type)) - | Just blk <- W4.asNat (C.llvmPointerBlock ptr) - , Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr) -> do - maybe_ranges <- runMaybeT $ - C.writeRangesMem @_ @64 sym $ C.memImplHeap header_mem_impl - case maybe_ranges of - Just ranges -> do - sz <- W4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth $ toInteger $ C.typeEnd 0 storeage_type - forM_ (Map.findWithDefault [] blk ranges) $ \(prev_off, prev_sz) -> do - disjoint_pred <- C.buildDisjointRegionsAssertionWithSub - sym - ptr - sz - (C.LLVMPointer (C.llvmPointerBlock ptr) prev_off) - prev_sz - when (W4.asConstantPred disjoint_pred /= Just True) $ - fail $ - "SimpleLoopFixpoint: non-disjoint ranges: off1=" - ++ show (W4.printSymExpr (C.llvmPointerOffset ptr)) - ++ ", sz1=" - ++ show (W4.printSymExpr sz) - ++ ", off2=" - ++ show (W4.printSymExpr prev_off) - ++ ", sz2=" - ++ show (W4.printSymExpr prev_sz) - return Nothing - Nothing -> fail $ "SimpleLoopFixpoint: unsupported symbolic pointers" - _ -> fail $ "SimpleLoopFixpoint: not MemWrite: " ++ show (C.ppMemWrites mem_writes)) - (List.concat $ IntMap.elems mmm) - _ -> fail $ "SimpleLoopFixpoint: not MemWritesChunkIndexed: " ++ show (C.ppMemWrites mem_writes) + mem_substitution_candidate <- joinMem sym header_mem_impl mem_writes -- check that the mem substitution always computes the same footprint on every iteration (!?!) mem_substitution <- if Map.null (fixpointMemSubstitution fixpoint_record) @@ -705,17 +1059,14 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state assumption_frame_identifier <- C.pushAssumptionFrame bak -- check if we are done; if we did not introduce any new variables, we don't have to widen any more - if MapF.keys join_substitution == MapF.keys (fixpointSubstitution fixpoint_record) + if MapF.keys join_substitution == MapF.keys (fixpointSubstitution fixpoint_record) && Map.keys mem_substitution == Map.keys (fixpointMemSubstitution fixpoint_record) -- we found the fixpoint, get ready to wrap up then do ?logMessage $ "SimpleLoopFixpoint: RunningState: ComputeFixpoint -> CheckFixpoint" - ?logMessage $ - "SimpleLoopFixpoint: cond: " ++ - show (maybe "Nothing" W4.printSymExpr $ fixpointLoopCondition fixpoint_record) - -- we have delayed populating the main substituation map with + -- we have delayed populating the main substitution map with -- memory variables, so we have to do that now header_mem_substitution <- loadMemJoinVariables bak header_mem_impl $ @@ -723,18 +1074,37 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record - -- try to unify widening variables that have the same values - let (normal_substitution, equality_substitution) = uninterpretedConstantEqualitySubstitution sym $ - -- drop variables that don't appear along some back edge (? understand this better) - filterSubstitution sym $ + -- drop variables that don't appear along some back edge + let union_substitution' = filterSubstitution sym $ MapF.union join_substitution $ -- this implements zip, because the two maps have the same keys MapF.intersectWithKeyMaybe (\_k x y -> Just $ FixpointEntry{ headerValue = x, bodyValue = y }) header_mem_substitution body_mem_substitution - -- ?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList normal_substitution) - -- ?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution) + loop_index_linear_substitution <- loopIndexLinearSubstitution sym (fixpointIndex fixpoint_record) union_substitution' + + let union_substitution = MapF.filterWithKey + (\variable _entry -> MapF.notMember variable loop_index_linear_substitution) + union_substitution' + -- 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 + add_index_one <- W4.bvAdd sym (fixpointIndex fixpoint_record) one_bv + let normal_substitution = MapF.insert + (fixpointIndex fixpoint_record) + FixpointEntry + { headerValue = zero_bv + , bodyValue = add_index_one + } + normal_substitution' + let equality_substitution = MapF.union equality_substitution' loop_index_linear_substitution + + ?logMessage $ "loop_index_linear_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList loop_index_linear_substitution) + ?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList normal_substitution) + ?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution) -- unify widening variables in the register subst let res_reg_map = applySubstitutionRegEntries sym equality_substitution join_reg_map @@ -746,28 +1116,77 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state mem_substitution equality_substitution - -- finally we can determine the loop bounds - loop_index_bound <- findLoopIndexBound sym normal_substitution $ fixpointLoopCondition fixpoint_record + let body_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue) $ + MapF.elems normal_substitution + let header_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . headerValue) $ + MapF.elems normal_substitution + -- let all_vars = Set.union proof_goals_and_assumptions_vars $ Set.union body_values_vars header_values_vars + let all_vars' = Set.insert (Some $ fixpointIndex fixpoint_record) proof_goals_and_assumptions_vars + let all_vars = Set.filter + (\(Some variable) -> MapF.notMember variable equality_substitution) + all_vars' + -- let some_uninterpreted_constants = Ctx.fromList $ Set.toList all_vars + let filtered_vars = Set.filter + (\(Some variable) -> + not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable)) + all_vars + let some_uninterpreted_constants = Ctx.fromList $ Set.toList filtered_vars + -- let implicit_vars = Set.filter + -- (\(Some variable) -> + -- not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable)) + -- all_vars + some_inv_pred <- case some_uninterpreted_constants of + Some uninterpreted_constants -> do + inv_pred <- W4.freshTotalUninterpFn + sym + (W4.safeSymbol "inv") + (fmapFC W4.exprType uninterpreted_constants) + W4.BaseBoolRepr - (_ :: ()) <- case loop_index_bound of - LoopIndexBound{ index = loop_index, stop = loop_stop } -> do loc <- W4.getCurrentProgramLoc sym - index_bound_condition <- loopIndexBoundCondition sym loop_index loop_stop - C.addAssumption bak $ C.GenericAssumption loc "" index_bound_condition - index_start_step_condition <- loopIndexStartStepCondition sym loop_index_bound - C.addAssumption bak $ C.GenericAssumption loc "" index_start_step_condition - writeIORef fixpoint_state_ref $ + header_inv <- W4.applySymFn sym inv_pred $ + applySubstitutionFC (fmapF headerValue normal_substitution) uninterpreted_constants + C.addProofObligation bak $ C.LabeledPred header_inv $ C.SimError loc "" + + inv <- W4.applySymFn sym inv_pred uninterpreted_constants + C.addAssumption bak $ C.GenericAssumption loc "inv" inv + + return $ W4.SomeSymFn inv_pred + + modifyIORef' fixpoint_state_ref $ executionFeatureContextAddInvPred some_inv_pred + + ?logMessage $ + "proof_goals_and_assumptions_vars: " + ++ show (map (viewSome W4.printSymExpr) $ Set.toList proof_goals_and_assumptions_vars) + ?logMessage $ + "body_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList body_values_vars) + ?logMessage $ + "header_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList header_values_vars) + ?logMessage $ + "uninterpreted_constants: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList filtered_vars) + + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ CheckFixpoint FixpointRecord - { fixpointBlockId = C.Some block_id + { fixpointBlockId = block_id , fixpointAssumptionFrameIdentifier = assumption_frame_identifier , fixpointSubstitution = normal_substitution - , fixpointRegMap = C.RegMap res_reg_map + , fixpointRegMap = fixpointRegMap fixpoint_record , fixpointMemSubstitution = mem_substitution - , fixpointLoopCondition = fixpointLoopCondition fixpoint_record + , fixpointEqualitySubstitution = equality_substitution + , fixpointIndex = fixpointIndex fixpoint_record } - loop_index_bound + some_inv_pred + -- implicit_vars + some_uninterpreted_constants + loop_condition return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap res_reg_map @@ -783,26 +1202,21 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state mem_substitution MapF.empty - writeIORef fixpoint_state_ref $ ComputeFixpoint + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint FixpointRecord - { fixpointBlockId = C.Some block_id + { fixpointBlockId = block_id , fixpointAssumptionFrameIdentifier = assumption_frame_identifier , fixpointSubstitution = join_substitution , fixpointRegMap = C.RegMap join_reg_map , fixpointMemSubstitution = mem_substitution - , fixpointLoopCondition = Nothing + , fixpointEqualitySubstitution = MapF.empty + , fixpointIndex = fixpointIndex fixpoint_record } return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap join_reg_map & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl - | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: ComputeFixpoint"] - - CheckFixpoint fixpoint_record loop_bound - | FixpointRecord { fixpointRegMap = reg_map } <- fixpoint_record - , Just Refl <- W4.testEquality - (fmapFC C.regType $ C.regMap reg_map) - (fmapFC C.regType $ C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs)) -> do + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition -> do ?logMessage $ "SimpleLoopFixpoint: RunningState: " ++ "CheckFixpoint" @@ -814,72 +1228,160 @@ advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state loc <- W4.getCurrentProgramLoc sym -- assert that the hypothesis we made about the loop termination condition is true - (_ :: ()) <- case loop_bound of - LoopIndexBound{ index = loop_index, stop = loop_stop } -> do - -- check the loop index bound condition - index_bound_condition <- loopIndexBoundCondition - sym - (bodyValue $ fromJust $ MapF.lookup loop_index $ fixpointSubstitution fixpoint_record) - loop_stop - C.addProofObligation bak $ C.LabeledPred index_bound_condition $ C.SimError loc "" - - _ <- C.popAssumptionFrame bak $ fixpointAssumptionFrameIdentifier fixpoint_record - - let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) - let (header_mem_impl, _mem_allocs, _mem_writes) = dropMemStackFrame body_mem_impl + (_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of + (W4.SomeSymFn inv_pred, Some uninterpreted_constants) + | Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants) + , Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do + inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC + (fmapF bodyValue $ fixpointSubstitution fixpoint_record) + uninterpreted_constants + C.addProofObligation bak $ C.LabeledPred inv $ C.SimError loc "" + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + + frame_assumptions <- C.popAssumptionFrame bak $ fixpointAssumptionFrameIdentifier fixpoint_record + + -- body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record + -- let res_substitution = MapF.mapWithKey + -- (\variable fixpoint_entry -> + -- fixpoint_entry + -- { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution + -- }) + -- (fixpointSubstitution fixpoint_record) + -- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution) - body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record - let res_substitution = MapF.mapWithKey - (\variable fixpoint_entry -> - fixpoint_entry - { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution + -- match things up with the input function that describes the loop body behavior + fixpoint_substitution <- case maybe_fixpoint_func of + Just fixpoint_func -> do + -- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func res_substitution loop_condition + + correct_substitution <- traverseF + (\fixpoint_entry -> do + correct_body_value <- W4.substituteBoundVars sym (asBoundVarSubstitution sym $ fixpointEqualitySubstitution fixpoint_record) $ bodyValue fixpoint_entry + return $ fixpoint_entry + { bodyValue = correct_body_value }) (fixpointSubstitution fixpoint_record) - -- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution) + (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func correct_substitution loop_condition + -- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func (fixpointSubstitution fixpoint_record) loop_condition + + _ <- case maybe_fixpoint_func_condition of + Just fixpoint_func_condition -> do + bak_assumptions <- liftIO $ C.assumptionsPred sym =<< C.collectAssumptions bak + inv_assumption <- C.assumptionPred <$> headAssumption sym frame_assumptions + all_assumptions <- liftIO $ W4.andPred sym bak_assumptions inv_assumption + implication <- liftIO $ W4.impliesPred sym all_assumptions fixpoint_func_condition + modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication + -- tmp_frame_id <- C.pushAssumptionFrame bak + -- C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc "" + -- (_, obligations) <- C.popAssumptionFrameAndObligations bak tmp_frame_id + -- putStrLn $ "before convertProofObligationsAsImplications" + -- implications <- C.convertProofObligationsAsImplications sym obligations + -- putStrLn $ "after convertProofObligationsAsImplications" + -- forM_ implications $ \implication -> + -- modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication + Nothing -> return () + + ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution) + + return fixpoint_func_substitution + + Nothing -> return MapF.empty - -- match things up with the input function that describes the loop body behavior - (fixpoint_func_substitution, fixpoint_func_condition) <- liftIO $ - case fixpointLoopCondition fixpoint_record of - Nothing -> fail "When checking the result of a fixpoint, no loop condition was found!" - Just c -> fixpoint_func res_substitution c - - C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc "" - -- ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution) - - let res_reg_map = C.RegMap $ - applySubstitutionRegEntries sym fixpoint_func_substitution (C.regMap reg_map) - - res_mem_impl <- storeMemJoinVariables bak - header_mem_impl - (fixpointMemSubstitution fixpoint_record) - fixpoint_func_substitution - - (_ :: ()) <- case loop_bound of - LoopIndexBound{ index = loop_index, stop = loop_stop } -> do - let loop_index' = MapF.findWithDefault loop_index loop_index fixpoint_func_substitution - index_bound_condition <- loopIndexBoundCondition sym loop_index' loop_stop - C.addAssumption bak $ C.GenericAssumption loc "" index_bound_condition - index_start_step_condition <- loopIndexStartStepCondition sym $ LoopIndexBound - { index = loop_index' - , start = start loop_bound - , stop = loop_stop - , step = step loop_bound - } - C.addAssumption bak $ C.GenericAssumption loc "" index_start_step_condition + let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let (header_mem_impl, _mem_allocs, _mem_writes) = dropMemStackFrame body_mem_impl - writeIORef fixpoint_state_ref $ + fixpoint_equality_substitution <- traverseF + (W4.substituteBoundVars sym $ asBoundVarSubstitution sym fixpoint_substitution) $ + fixpointEqualitySubstitution fixpoint_record + let fixpoint_equality_substitution' = MapF.union fixpoint_substitution fixpoint_equality_substitution + let res_reg_map = C.RegMap $ applySubstitutionRegEntries sym fixpoint_equality_substitution' (C.regMap $ fixpointRegMap fixpoint_record) + res_mem_impl <- storeMemJoinVariables bak header_mem_impl (fixpointMemSubstitution fixpoint_record) fixpoint_equality_substitution' + + (_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of + (W4.SomeSymFn inv_pred, Some uninterpreted_constants) + | Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants) + , Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do + inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC fixpoint_substitution uninterpreted_constants + C.addAssumption bak $ C.GenericAssumption loc "" inv + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ AfterFixpoint - fixpoint_record{ fixpointSubstitution = res_substitution } - loop_bound + -- fixpoint_record{ fixpointSubstitution = res_substitution } + fixpoint_record return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ res_reg_map & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl - | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + AfterFixpoint{} -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: AfterFixpoint -> ComputeFixpoint" + initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref - AfterFixpoint{} -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["AfterFixpoint"] +handleSymbolicBranch :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + CallFrameHandle init ret blocks -> + C.BlockID blocks tp -> + W4.Pred sym -> + C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) -> + C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) -> + Maybe (C.Some (C.BlockID blocks)) -> + Maybe (C.Some (C.BlockID blocks)) -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO (C.ExecutionFeatureResult p sym ext rtp) +handleSymbolicBranch bak call_frame_handle loop_block_id branch_condition true_frame false_frame true_frame_parent_loop_id false_frame_parent_loop_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + + (loop_condition, inside_loop_frame, outside_loop_frame) <- + if true_frame_parent_loop_id == Just (C.Some loop_block_id) + then + return (branch_condition, true_frame, false_frame) + else if false_frame_parent_loop_id == Just (C.Some loop_block_id) + then do + not_branch_condition <- W4.notPred sym branch_condition + return (not_branch_condition, false_frame, true_frame) + else + fail $ "unsupported loop: loop header block id " ++ show loop_block_id ++ " true frame parent loop id " ++ show true_frame_parent_loop_id ++ " false frame parent loop id " ++ show false_frame_parent_loop_id + + Just fixpoint_state <- callFrameContextLookup' call_frame_handle loop_block_id <$> readIORef fixpoint_state_ref + (condition, frame) <- case fixpoint_state of + BeforeFixpoint -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint:" ["BeforeFixpoint"] + + ComputeFixpoint{} -> do + -- continue in the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint" + return (loop_condition, inside_loop_frame) + + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants _ -> do + -- continue in the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint" + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle loop_block_id $ + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition + return (loop_condition, inside_loop_frame) + + AfterFixpoint{} -> do + -- break out of the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint" + modifyIORef' fixpoint_state_ref $ callFrameContextPop call_frame_handle + not_loop_condition <- W4.notPred sym loop_condition + return (not_loop_condition, outside_loop_frame) + + loc <- W4.getCurrentProgramLoc sym + C.addAssumption bak $ C.BranchCondition loc (C.pausedLoc frame) condition + C.ExecutionFeatureNewState <$> + runReaderT + (C.resumeFrame (C.forgetPostdomFrame frame) $ sim_state ^. (C.stateTree . C.actContext)) + sim_state + + +data SomeCallFrameHandle ret blocks = forall init . SomeCallFrameHandle (CallFrameHandle init ret blocks) + +callFrameHandle :: C.CallFrame sym ext blocks ret ctx -> SomeCallFrameHandle ret blocks +callFrameHandle C.CallFrame { _frameCFG = g } = + SomeCallFrameHandle $ CallFrameHandle (C.cfgHandle g) $ fmapFC C.blockInputs $ C.cfgBlockMap g data MaybePausedFrameTgtId f where JustPausedFrameTgtId :: C.Some (C.BlockID b) -> MaybePausedFrameTgtId (C.CrucibleLang b r) @@ -890,3 +1392,30 @@ pausedFrameTgtId C.PausedFrame{ resume = resume } = case resume of C.ContinueResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id C.CheckMergeResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id _ -> NothingPausedFrameTgtId + + +applySubstitutionF :: (OrdF k, FunctorF f) => MapF k k -> f k -> f k +applySubstitutionF substitution = fmapF $ findWithDefaultKey substitution + +applySubstitutionFC :: (OrdF k, FunctorFC f) => MapF k k -> f k l -> f k l +applySubstitutionFC substitution = fmapFC $ findWithDefaultKey substitution + +findWithDefaultKey :: forall a (k :: a -> Type) tp . OrdF k => MapF k k -> k tp -> k tp +findWithDefaultKey substitution key = MapF.findWithDefault key key substitution + +asBoundVarSubstitution :: W4.IsSymExprBuilder sym => sym -> MapF (W4.SymExpr sym) a -> MapF (W4.BoundVar sym) a +asBoundVarSubstitution sym = + MapF.fromList . mapMaybe (\(MapF.Pair k_expr v) -> fmap (\k_var -> MapF.Pair k_var v) $ asBoundVar sym k_expr) . MapF.toList + +asBoundVar :: W4.IsSymExprBuilder sym => sym -> W4.SymExpr sym tp -> Maybe (W4.BoundVar sym tp) +asBoundVar sym expr = case Set.toList (W4.exprUninterpConstants sym expr) of + [Some var] + | Just Refl <- testEquality expr (W4.varExpr sym var) -> + Just var + _ -> Nothing + +headAssumption :: sym -> C.Assumptions sym -> IO (C.CrucibleAssumption (W4.SymExpr sym)) +headAssumption sym = \case + C.SingleAssumption a -> return a + C.ManyAssumptions (x Seq.:<| _) -> headAssumption sym x + _ -> fail "SimpleLoopFixpoint.headAssumption: empty assumptions" diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs index 32c175076..4aaa10ed7 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs @@ -95,6 +95,12 @@ module Lang.Crucible.LLVM.SimpleLoopInvariant ( InvariantEntry(..) , InvariantPhase(..) , simpleLoopInvariant + -- , MemorySubstitution(..) + -- , computeMemSubstitution + -- , constructMemSubstitutionCandidate + -- , checkMemSubst + -- , loadMemJoinVariables + -- , storeMemJoinVariables ) where import Control.Lens diff --git a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs index a834f9d5c..70130b813 100644 --- a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs +++ b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs @@ -249,7 +249,7 @@ parentWTOComponent = F.foldMap' $ \case Vertex{} -> M.empty parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n -parentWTOComponent' scc = M.singleton (wtoHead scc) (wtoHead scc) <> +parentWTOComponent' scc = -- M.singleton (wtoHead scc) (wtoHead scc) <> F.foldMap' (\case SCC scc' -> parentWTOComponent' scc' diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index f8adec788..1aa3d4767 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -641,6 +641,11 @@ runCHC bak uninterp_inv_fns = liftIO $ do implications <- proofObligationsAsImplications bak clearProofObligations bak + withFile "foo.smt2" WriteMode $ \handle -> + Z3.writeZ3HornSMT2File sym True handle uninterp_inv_fns implications + withFile "foo.sy" WriteMode $ \handle -> + CVC5.writeCVC5SyFile sym handle uninterp_inv_fns implications + -- log to stdout let logData = defaultLogData { logCallbackVerbose = \_ -> putStrLn @@ -650,6 +655,10 @@ runCHC bak uninterp_inv_fns = liftIO $ do Sat sub -> return sub Unsat{} -> fail "Prover returned Infeasible" Unknown -> fail "Prover returned Fail" + -- CVC5.runCVC5SyGuS sym logData uninterp_inv_fns implications >>= \case + -- Sat sub -> return sub + -- Unsat{} -> fail "Prover returned Infeasible" + -- Unknown -> fail "Prover returned Fail" -- | Get proof obligations as What4 implications. From 08b51b64260e39c4052f746ae851d7d5ec76a7aa Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 17 Feb 2024 22:11:13 -0500 Subject: [PATCH 17/35] Fix build error with GHC 8.10 --- crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs index 5c356f881..87e0ab7f9 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -56,7 +56,8 @@ import Data.Map (Map) import qualified Data.Sequence as Seq import qualified Data.Set as Set import Data.Set (Set) -import GHC.TypeLits +import GHC.TypeLits (KnownNat) +import Numeric.Natural (Natural) import qualified System.IO import qualified Data.BitVector.Sized as BV From a4300a4d5bb008bead1c42bdde7797c3483e234d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:32:34 -0500 Subject: [PATCH 18/35] Bump what4 submodule to incorporate GaloisInc/what4#256 This also reverts the test output changes from commit 23cc439654abbc0c3714a7035d026453c234d9c4, as the option which caused the change is no longer enabled by default. --- crux-llvm/test-data/golden/golden/float-cast2.z3.good | 2 +- dependencies/what4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/crux-llvm/test-data/golden/golden/float-cast2.z3.good b/crux-llvm/test-data/golden/golden/float-cast2.z3.good index 63af98236..4334bf91d 100644 --- a/crux-llvm/test-data/golden/golden/float-cast2.z3.good +++ b/crux-llvm/test-data/golden/golden/float-cast2.z3.good @@ -1,2 +1,2 @@ -ite (floatIsNaN cX@3:f) 0x0:[32] 0x1:[32] +bvZext 32 (ite (floatIsNaN cX@3:f) 0x0:[1] 0x1:[1]) [Crux] Overall status: Valid. diff --git a/dependencies/what4 b/dependencies/what4 index 670c8aca5..72dd5ff57 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 670c8aca552e8b748b20d127d1310430880a45e8 +Subproject commit 72dd5ff5741caee5a40ca5f5791201a54f6064b7 From 82574be4556f1c28b4fdc3385b8a5b7b41b63f11 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:39:19 -0500 Subject: [PATCH 19/35] Fix build warnings introduced in #1165 --- crucible/src/Lang/Crucible/Backend.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index f8adec788..0438285b8 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -36,6 +36,7 @@ obligations with a solver backend. {-# LANGUAGE RankNTypes #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} module Lang.Crucible.Backend ( IsSymBackend(..) @@ -118,7 +119,6 @@ import Data.Sequence (Seq) import Data.Set (Set) import qualified Prettyprinter as PP import GHC.Stack -import System.IO import Data.Parameterized.Map (MapF) @@ -132,7 +132,6 @@ import What4.Partial import What4.ProgramLoc import What4.Expr (GroundValue, GroundValueWrapper(..)) import What4.Solver -import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3 import qualified Lang.Crucible.Backend.AssumptionStack as AS From 0d1cd5bcb393bcd01e0ab2ecbda149e833aa593a Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:39:56 -0500 Subject: [PATCH 20/35] crucible: Clearer error messages for runCHC --- crucible/src/Lang/Crucible/Backend.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 0438285b8..df60b7c78 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -647,8 +647,8 @@ runCHC bak uninterp_inv_fns = liftIO $ do } Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case Sat sub -> return sub - Unsat{} -> fail "Prover returned Infeasible" - Unknown -> fail "Prover returned Fail" + Unsat{} -> fail "Prover returned Unsat" + Unknown -> fail "Prover returned Unknown" -- | Get proof obligations as What4 implications. From cb2f709343f194e016c949c1b688fcd793c003a4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:55:08 -0500 Subject: [PATCH 21/35] Additional documentation --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs | 3 ++- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 757420006..919a5e7df 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -1634,7 +1634,8 @@ possibleAllocs n mem = Just (AllocInfo atp sz mut alignment loc) -> [SomeAlloc atp n sz mut alignment loc] - +-- | 'IO' plus memoization. The 'IORef' stores suspended computations with +-- 'Left' and evaluated results with 'Right'. newtype MemoIO m a = MemoIO (IORef (Either (m a) a)) putMemoIO :: MonadIO m => m a -> m (MemoIO m a) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index 58abe131f..c033e3567 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -541,6 +541,8 @@ ppMem m = ppMemState ppMemChanges (m^.memState) multiUnion :: (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a multiUnion = Map.unionWith (<>) +-- | This will return 'Just' if the size of the write is bounded and 'Nothing' +-- is the size of the write is unbounded. writeSourceSize :: (IsExprBuilder sym, 1 <= w) => sym -> From 80a9a3333ed5dab8f28ae36480089ca4394336e2 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:56:21 -0500 Subject: [PATCH 22/35] Comment out putStrLns --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 919a5e7df..cdf784d16 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -1674,7 +1674,7 @@ asMemAllocationArrayStore sym w ptr mem , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = do memo_nothing <- putMemoIO $ return Nothing - putStrLn $ "asMemAllocationArrayStore: base=" ++ show blk_no ++ " sz=" ++ show (printSymExpr sz) + --putStrLn $ "asMemAllocationArrayStore: base=" ++ show blk_no ++ " sz=" ++ show (printSymExpr sz) result <- findArrayStore sym w blk_no (BV.zero w) sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem return $ case result of @@ -1695,7 +1695,7 @@ asMemMatchingArrayStore sym w ptr sz mem | Just blk_no <- asNat (llvmPointerBlock ptr) , memMemberArrayBlock (llvmPointerBlock ptr) mem , Just off <- asBV (llvmPointerOffset ptr) = do - putStrLn $ "asMemMatchingArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) + --putStrLn $ "asMemMatchingArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) memo_nothing <- putMemoIO $ return Nothing findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem | otherwise = return Nothing @@ -1713,8 +1713,8 @@ findArrayStore :: findArrayStore sym w blk_no off sz memo_cont = \case [] -> getMemoIO memo_cont head_mem_write : tail_mem_writes -> do - putStrLn $ " findArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) - putStrLn $ " findArrayStore: write=" ++ (case head_mem_write of MemWrite{} -> "write"; WriteMerge{} -> "merge") + --putStrLn $ " findArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) + --putStrLn $ " findArrayStore: write=" ++ (case head_mem_write of MemWrite{} -> "write"; WriteMerge{} -> "merge") case head_mem_write of MemWrite write_ptr write_source From 0a3a21ee3c0a8bf302c4258bac35dd04fdbbcc53 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 11:57:42 -0500 Subject: [PATCH 23/35] Remove redundant export --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index 23ecef1cb..5317528b5 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -44,7 +44,6 @@ module Lang.Crucible.LLVM.MemModel.MemLog , isAllocatedGeneric -- * Write logs , WriteSource(..) - , writeSourceSize , MemWrite(..) , MemWrites(..) , MemWritesChunk(..) From 9475dce2af6e7c6441eb5579f9c58e9f1b14bc22 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 12:01:49 -0500 Subject: [PATCH 24/35] More accurate logReason --- crucible/src/Lang/Crucible/Backend.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index df60b7c78..130173396 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -643,7 +643,7 @@ runCHC bak uninterp_inv_fns = liftIO $ do -- log to stdout let logData = defaultLogData { logCallbackVerbose = \_ -> putStrLn - , logReason = "SAW inv" + , logReason = "Crucible inv" } Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case Sat sub -> return sub From 3b25fa0de3af1d94cd92e92b2d2f5ffc7f7c2e40 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:04:49 -0500 Subject: [PATCH 25/35] Remove redundant import --- crux/src/Crux.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index 709bd66c2..b5bb8fab8 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -74,7 +74,6 @@ import What4.Config (setOpt, getOptionSetting, verbosity, extendConfig import qualified What4.Expr as WE import What4.FunctionName (FunctionName) import What4.Interface (IsExprBuilder, getConfiguration) -import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder) import What4.Protocol.Online (OnlineSolver) import qualified What4.Solver as WS import What4.Solver.CVC4 (cvc4Timeout) From a743903d7b4d18ab1a91553a6c6cb1cf858e6c87 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:05:04 -0500 Subject: [PATCH 26/35] Don't log everything to foo.* files --- crucible/src/Lang/Crucible/Backend.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 809953f61..130173396 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -640,11 +640,6 @@ runCHC bak uninterp_inv_fns = liftIO $ do implications <- proofObligationsAsImplications bak clearProofObligations bak - withFile "foo.smt2" WriteMode $ \handle -> - Z3.writeZ3HornSMT2File sym True handle uninterp_inv_fns implications - withFile "foo.sy" WriteMode $ \handle -> - CVC5.writeCVC5SyFile sym handle uninterp_inv_fns implications - -- log to stdout let logData = defaultLogData { logCallbackVerbose = \_ -> putStrLn From 704a1279b9cc6483f9f8ef9bcfa31f25d4e2de69 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:08:50 -0500 Subject: [PATCH 27/35] Pass pointer size to writeSouceSize --- crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs index 87e0ab7f9..7eea3357f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -484,7 +484,7 @@ joinMem sym mem_impl mem_writes = do | Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr) , Just blk <- W4.asNat (C.llvmPointerBlock ptr) -> do sz <- maybe (fail "SimpleLoopFixpoint: unsupported MemSource") return =<< - runMaybeT (C.writeSourceSize sym mem_source) + runMaybeT (C.writeSourceSize sym (C.ptrWidth ptr) mem_source) let mem_loc = MemLocation { memLocationBlock = blk , memLocationOffset = C.llvmPointerOffset ptr From a6a062ad93283f9e0e682dfe0a2265d65dd7d671 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:16:00 -0500 Subject: [PATCH 28/35] Replace putStrLn's with ?logMessage's --- .../Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 35 ++++++++++--------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs index 7eea3357f..193c96b93 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -699,7 +699,7 @@ loopIndexLinearSubstitution sym index_variable = -- find widening variables that are actually the same (up to syntactic equality) -- and can be substituted for each other uninterpretedConstantEqualitySubstitution :: - (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m) => + (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m, ?logMessage :: String -> IO ()) => sym -> MapF (W4.SymExpr sym) (FixpointEntry sym) -> m (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym)) @@ -716,11 +716,11 @@ uninterpretedConstantEqualitySubstitution sym substitution = do (\variable _entry -> isNothing $ MapF.lookup variable uninterpreted_constant_substitution) substitution - liftIO $ putStrLn $ "vars:" + liftIO $ ?logMessage "vars:" mapM_ (\(MapF.Pair variable entry) -> do let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry - liftIO $ putStrLn $ show (W4.printSymExpr variable) ++ " :: "++ show (W4.exprType variable) ++ " -> " ++ (show $ Set.map (C.viewSome $ show . W4.printSymExpr) $ body_vars)) + liftIO $ ?logMessage $ show (W4.printSymExpr variable) ++ " :: "++ show (W4.exprType variable) ++ " -> " ++ (show $ Set.map (C.viewSome $ show . W4.printSymExpr) $ body_vars)) (MapF.toList normal_substitution) foo <- MapF.fromList <$> filterM @@ -730,18 +730,18 @@ uninterpretedConstantEqualitySubstitution sym substitution = do let lalala = runIdentity $ MapF.fromKeysM (return . W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry let foobar = fmapF headerValue $ MapF.mapMaybe (\v -> MapF.lookup v normal_substitution) lalala bar <- liftIO $ W4.isEq sym (headerValue entry) =<< W4.substituteBoundVars sym foobar (bodyValue entry) - liftIO $ putStrLn $ "la: " ++ (show $ W4.printSymExpr variable) - liftIO $ putStrLn $ "headerValue entry: " ++ (show $ W4.printSymExpr $ headerValue entry) - liftIO $ putStrLn $ "bodyValue entry:" ++ (show $ W4.printSymExpr $ bodyValue entry) - liftIO $ putStrLn $ "bar: " ++ (show $ W4.printSymExpr $ bar) + liftIO $ ?logMessage $ "la: " ++ (show $ W4.printSymExpr variable) + liftIO $ ?logMessage $ "headerValue entry: " ++ (show $ W4.printSymExpr $ headerValue entry) + liftIO $ ?logMessage $ "bodyValue entry:" ++ (show $ W4.printSymExpr $ bodyValue entry) + liftIO $ ?logMessage $ "bar: " ++ (show $ W4.printSymExpr $ bar) if Just True == W4.asConstantPred bar then do - liftIO $ putStrLn "lala" + liftIO $ ?logMessage "lala" return True else do notbar <- liftIO $ W4.notPred sym bar lala <- liftIO $ W4.runZ3InOverride sym (W4.defaultLogData { W4.logVerbosity = 2 }) [notbar] $ return . W4.isUnsat when lala $ do - liftIO $ putStrLn "lalala" + liftIO $ ?logMessage "lalala" return lala else return False) @@ -892,7 +892,7 @@ simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do | SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do loop_header_block_ids <- callFrameContextLoopHeaderBlockIds' call_frame_handle <$> readIORef fixpoint_state_ref if Set.member (C.Some block_id) loop_header_block_ids then do - putStrLn $ "!!!SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + ?logMessage $ "!!!SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref else do ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id @@ -930,7 +930,7 @@ simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do , true_frame_parent_loop_id <- if true_frame_some_block_id /= C.Some loop_block_id then Map.lookup true_frame_some_block_id parent_loop_map else maybe_some_loop_block_id , false_frame_parent_loop_id <- if false_frame_some_block_id /= C.Some loop_block_id then Map.lookup false_frame_some_block_id parent_loop_map else maybe_some_loop_block_id , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do - putStrLn $ "!!!SimpleLoopFixpoint: SymbolicBranchState: " ++ show (true_frame_some_block_id, false_frame_some_block_id) + ?logMessage $ "!!!SimpleLoopFixpoint: SymbolicBranchState: " ++ show (true_frame_some_block_id, false_frame_some_block_id) handleSymbolicBranch bak call_frame_handle @@ -959,13 +959,14 @@ simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do initializeCallFrameContext :: + (?logMessage :: String -> IO ()) => C.CFG ext blocks init ret -> IORef (ExecutionFeatureContext sym wptr ext) -> IO () initializeCallFrameContext cfg context_ref = do - putStrLn $ "SimpleLoopFixpoint: cfgHandle: " ++ show (C.cfgHandle cfg) - putStrLn $ "SimpleLoopFixpoint: cfg: " ++ show (toListFC (\b -> (C.Some (C.blockID b), C.nextBlocks b)) $ C.cfgBlockMap cfg) - putStrLn $ "SimpleLoopFixpoint: cfgWeakTopologicalOrdering: " ++ show (C.cfgWeakTopologicalOrdering cfg) + ?logMessage $ "SimpleLoopFixpoint: cfgHandle: " ++ show (C.cfgHandle cfg) + ?logMessage $ "SimpleLoopFixpoint: cfg: " ++ show (toListFC (\b -> (C.Some (C.blockID b), C.nextBlocks b)) $ C.cfgBlockMap cfg) + ?logMessage $ "SimpleLoopFixpoint: cfgWeakTopologicalOrdering: " ++ show (C.cfgWeakTopologicalOrdering cfg) let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg let call_frame_handle = CallFrameHandle (C.cfgHandle cfg) $ fmapFC C.blockInputs $ C.cfgBlockMap cfg modifyIORef' context_ref $ executionFeatureContextAddCallFrameContext call_frame_handle $ @@ -990,7 +991,7 @@ initializeFixpointState :: initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref = do let sym = C.backendGetSym bak assumption_frame_identifier <- C.pushAssumptionFrame bak - putStrLn $ "!!!SimpleLoopFixpoint: initializeFixpointState: block_id=" ++ show block_id ++ ", assumption_frame_identifier=" ++ show assumption_frame_identifier + ?logMessage $ "!!!SimpleLoopFixpoint: initializeFixpointState: block_id=" ++ show block_id ++ ", assumption_frame_identifier=" ++ show assumption_frame_identifier index_var <- W4.freshConstant sym (W4.safeSymbol "index_var") W4.knownRepr let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl } @@ -1275,9 +1276,9 @@ advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id -- tmp_frame_id <- C.pushAssumptionFrame bak -- C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc "" -- (_, obligations) <- C.popAssumptionFrameAndObligations bak tmp_frame_id - -- putStrLn $ "before convertProofObligationsAsImplications" + -- ?logMessage "before convertProofObligationsAsImplications" -- implications <- C.convertProofObligationsAsImplications sym obligations - -- putStrLn $ "after convertProofObligationsAsImplications" + -- ?logMessage "after convertProofObligationsAsImplications" -- forM_ implications $ \implication -> -- modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication Nothing -> return () From b938c6eebb3c0c0dda0fb3913d69a45a50058995 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 13:18:11 -0500 Subject: [PATCH 29/35] Fix build warnings --- .../Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 24 ++++--------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs index 193c96b93..66dc03e2c 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -41,7 +41,6 @@ module Lang.Crucible.LLVM.SimpleLoopFixpoint import Control.Lens import Control.Monad import Control.Monad.IO.Class -import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State import Control.Monad.Trans.Maybe @@ -601,11 +600,11 @@ loadMemJoinVariables bak mem subst = -- _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val) -- C.Err{} -> -- return Nothing -- fail $ "SimpleLoopFixpoint.loadMemJoinVariables: loadRaw failed" - MemArrayFixpointEntry join_variable size -> do + MemArrayFixpointEntry join_variable _size -> do -- TODO: handle arrays maybe_allocation_array <- C.asMemAllocationArrayStore sym ?ptrWidth ptr (C.memImplHeap mem) case maybe_allocation_array of - Just (ok, arr, arr_sz) | Just True <- W4.asConstantPred ok -> do + Just (ok, arr, _arr_sz) | Just True <- W4.asConstantPred ok -> do return $ Just $ MapF.Pair join_variable arr _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables") (Map.toAscList subst) @@ -649,18 +648,6 @@ memLocationPtr sym (MemLocation { memLocationBlock = blk, memLocationOffset = of C.LLVMPointer <$> W4.natLit sym blk <*> return off -applySubstitutionMemFixpointEntries :: - (C.IsSymInterface sym, Functor f) => - MapF (W4.SymExpr sym) (W4.SymExpr sym) -> - f (MemFixpointEntry sym wptr) -> - f (MemFixpointEntry sym wptr) -applySubstitutionMemFixpointEntries substitution = fmap $ \case - MemStoreFixpointEntry join_variable storage_type -> - MemStoreFixpointEntry (findWithDefaultKey substitution join_variable) storage_type - MemArrayFixpointEntry join_variable size -> - MemArrayFixpointEntry (findWithDefaultKey substitution join_variable) size - - dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym) dropMemStackFrame mem = case (C.memImplHeap mem) ^. C.memState of (C.StackFrame _ _ _ (a, w) s) -> ((mem { C.memImplHeap = (C.memImplHeap mem) & C.memState .~ s }), a, w) @@ -833,7 +820,7 @@ simpleLoopFixpoint :: IO (C.ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext)) simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do verbSetting <- W4.getOptionSetting W4.verbosity $ W4.getConfiguration sym - verb <- fromInteger <$> W4.getOpt verbSetting + _verb <- fromInteger @Natural <$> W4.getOpt verbSetting -- let loop_map = Map.fromList $ mapMaybe -- (\case @@ -876,7 +863,7 @@ simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do -- initializeCallFrameContext cfg fixpoint_state_ref return $ (, fixpoint_state_ref) $ C.ExecutionFeature $ \exec_state -> do - -- let ?logMessage = \msg -> when (verb >= (3 :: Natural)) $ do + -- let ?logMessage = \msg -> when (_verb >= 3) $ do let ?logMessage = \msg -> do let h = C.printHandle $ C.execStateContext exec_state System.IO.hPutStrLn h msg @@ -1396,9 +1383,6 @@ pausedFrameTgtId C.PausedFrame{ resume = resume } = case resume of _ -> NothingPausedFrameTgtId -applySubstitutionF :: (OrdF k, FunctorF f) => MapF k k -> f k -> f k -applySubstitutionF substitution = fmapF $ findWithDefaultKey substitution - applySubstitutionFC :: (OrdF k, FunctorFC f) => MapF k k -> f k l -> f k l applySubstitutionFC substitution = fmapFC $ findWithDefaultKey substitution From e356be1a7b9f9d76a0d15b7cb35c4438ff277fd6 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 7 Mar 2024 11:42:51 -0500 Subject: [PATCH 30/35] Rename SimpleLoopFixpoint to SimpleLoopFixpointCHC SimpleLoopFixpointCHC is not quite suitable for being a full replacement for SimpleLoopFixpoint as of yet. For now, we will offer the CHC functionality in a separate module, and we will restore the old SimpleLoopFixpoint functionality in a subsequent commit. --- crucible-llvm/crucible-llvm.cabal | 2 +- ...pleLoopFixpoint.hs => SimpleLoopFixpointCHC.hs} | 14 +++++++++++--- 2 files changed, 12 insertions(+), 4 deletions(-) rename crucible-llvm/src/Lang/Crucible/LLVM/{SimpleLoopFixpoint.hs => SimpleLoopFixpointCHC.hs} (99%) diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 6b3c24b5f..70e483f10 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -88,7 +88,7 @@ library Lang.Crucible.LLVM.Printf Lang.Crucible.LLVM.QQ Lang.Crucible.LLVM.SymIO - Lang.Crucible.LLVM.SimpleLoopFixpoint + Lang.Crucible.LLVM.SimpleLoopFixpointCHC Lang.Crucible.LLVM.SimpleLoopInvariant Lang.Crucible.LLVM.Translation Lang.Crucible.LLVM.Translation.Aliases diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs similarity index 99% rename from crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs rename to crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs index 66dc03e2c..da1afa3cf 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs @@ -1,10 +1,18 @@ ------------------------------------------------------------------------ -- | --- Module : Lang.Crucible.LLVM.SimpleLoopFixpoint --- Description : Execution feature to compute loop fixpoint +-- Module : Lang.Crucible.LLVM.SimpleLoopFixpointCHC +-- Description : Execution feature to compute loop fixpoint in +-- conjunction with CHC -- Copyright : (c) Galois, Inc 2021 -- License : BSD3 -- Stability : provisional +-- +-- This offers a similar API to what is offered in +-- "Lang.Crucible.LLVM.SimpleLoopFixpoint", but this generates proof obligations +-- involving a predicate function (named @inv@). The intent is that a user will +-- leverage Z3's constrained horn-clause (CHC) functionality to synthesize an +-- implementation of @inv@ and then substitute it back into the proof +-- obligations. ------------------------------------------------------------------------ {-# LANGUAGE DataKinds #-} @@ -29,7 +37,7 @@ {-# LANGUAGE TupleSections #-} -module Lang.Crucible.LLVM.SimpleLoopFixpoint +module Lang.Crucible.LLVM.SimpleLoopFixpointCHC ( FixpointEntry(..) , FixpointState(..) , CallFrameContext(..) From 6b7d94c61fca303f2ee155e2f3ee6a36ebb804cc Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 7 Mar 2024 11:44:25 -0500 Subject: [PATCH 31/35] Restore previous SimpleLoopFixpoint functionality --- crucible-llvm/crucible-llvm.cabal | 1 + .../Lang/Crucible/LLVM/SimpleLoopFixpoint.hs | 892 ++++++++++++++++++ 2 files changed, 893 insertions(+) create mode 100644 crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 70e483f10..f30c61336 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -88,6 +88,7 @@ library Lang.Crucible.LLVM.Printf Lang.Crucible.LLVM.QQ Lang.Crucible.LLVM.SymIO + Lang.Crucible.LLVM.SimpleLoopFixpoint Lang.Crucible.LLVM.SimpleLoopFixpointCHC Lang.Crucible.LLVM.SimpleLoopInvariant Lang.Crucible.LLVM.Translation diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs new file mode 100644 index 000000000..af22ea5f1 --- /dev/null +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs @@ -0,0 +1,892 @@ +------------------------------------------------------------------------ +-- | +-- Module : Lang.Crucible.LLVM.SimpleLoopFixpoint +-- Description : Execution feature to compute loop fixpoint +-- Copyright : (c) Galois, Inc 2021 +-- License : BSD3 +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + + +module Lang.Crucible.LLVM.SimpleLoopFixpoint + ( FixpointEntry(..) + , simpleLoopFixpoint + ) where + +import Control.Lens +import Control.Monad (when) +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Reader (ReaderT(..)) +import Control.Monad.State (MonadState(..), StateT(..)) +import Control.Monad.Trans.Maybe +import Data.Either +import Data.Foldable +import qualified Data.IntMap as IntMap +import Data.IORef +import qualified Data.List as List +import Data.Maybe +import qualified Data.Map as Map +import Data.Map (Map) +import qualified Data.Set as Set +import qualified System.IO +import Numeric.Natural + +import qualified Data.BitVector.Sized as BV +import Data.Parameterized.Classes +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Map (MapF) +import Data.Parameterized.NatRepr +import Data.Parameterized.TraversableF +import Data.Parameterized.TraversableFC + +import qualified What4.Config as W4 +import qualified What4.Interface as W4 + +import qualified Lang.Crucible.Analysis.Fixpoint.Components as C +import qualified Lang.Crucible.Backend as C +import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.Panic as C +import qualified Lang.Crucible.Simulator.CallFrame as C +import qualified Lang.Crucible.Simulator.EvalStmt as C +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.GlobalState as C +import qualified Lang.Crucible.Simulator.Operations as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Simulator as C + +import qualified Lang.Crucible.LLVM.Bytes as C +import qualified Lang.Crucible.LLVM.DataLayout as C +import qualified Lang.Crucible.LLVM.MemModel as C +import qualified Lang.Crucible.LLVM.MemModel.MemLog as C hiding (Mem) +import qualified Lang.Crucible.LLVM.MemModel.Pointer as C +import qualified Lang.Crucible.LLVM.MemModel.Type as C + + +-- | When live loop-carried dependencies are discovered as we traverse +-- a loop body, new "widening" variables are introduced to stand in +-- for those locations. When we introduce such a varible, we +-- capture what value the variable had when we entered the loop (the +-- \"header\" value); this is essentially the initial value of the +-- variable. We also compute what value the variable should take on +-- its next iteration assuming the loop doesn't exit and executes +-- along its backedge. This \"body\" value will be computed in +-- terms of the the set of all discovered live variables so far. +-- We know we have reached fixpoint when we don't need to introduce +-- and more fresh widening variables, and the body values for each +-- variable are stable across iterations. +data FixpointEntry sym tp = FixpointEntry + { headerValue :: W4.SymExpr sym tp + , bodyValue :: W4.SymExpr sym tp + } + +instance OrdF (W4.SymExpr sym) => OrdF (FixpointEntry sym) where + compareF x y = case compareF (headerValue x) (headerValue y) of + LTF -> LTF + EQF -> compareF (bodyValue x) (bodyValue y) + GTF -> GTF + +instance OrdF (FixpointEntry sym) => W4.TestEquality (FixpointEntry sym) where + testEquality x y = case compareF x y of + EQF -> Just Refl + _ -> Nothing + +data MemFixpointEntry sym = forall w . (1 <= w) => MemFixpointEntry + { memFixpointEntrySym :: sym + , memFixpointEntryJoinVariable :: W4.SymBV sym w + } + +-- | This datatype captures the state machine that progresses as we +-- attempt to compute a loop invariant for a simple structured loop. +data FixpointState sym blocks + -- | We have not yet encoundered the loop head + = BeforeFixpoint + + -- | We have encountered the loop head at least once, and are in the process + -- of converging to an inductive representation of the live variables + -- in the loop. + | ComputeFixpoint (FixpointRecord sym blocks) + + -- | We have found an inductively-strong representation of the live variables + -- of the loop, and have discovered the loop index structure controling the + -- execution of the loop. We are now executing the loop once more to compute + -- verification conditions for executions that reamain in the loop. + | CheckFixpoint + (FixpointRecord sym blocks) + (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find + + -- | Finally, we stitch everything we have found together into the rest of the program. + -- Starting from the loop header one final time, we now force execution to exit the loop + -- and continue into the rest of the program. + | AfterFixpoint + (FixpointRecord sym blocks) + (LoopIndexBound sym) -- ^ data about the fixed sort of loop index values we are trying to find + +-- | Data about the loop that we incrementally compute as we approach fixpoint. +data FixpointRecord sym blocks = forall args. + FixpointRecord + { + -- | Block identifier of the head of the loop + fixpointBlockId :: C.Some (C.BlockID blocks) + + -- | identifier for the currently-active assumption frame related to this fixpoint computation + , fixpointAssumptionFrameIdentifier :: C.FrameIdentifier + + -- | Map from introduced widening variables to prestate value before the loop starts, + -- and to the value computed in a single loop iteration, assuming we return to the + -- loop header. These variables may appear only in either registers or memory. + , fixpointSubstitution :: MapF (W4.SymExpr sym) (FixpointEntry sym) + + -- | Prestate values of the Crucible registers when the loop header is first encountered. + , fixpointRegMap :: C.RegMap sym args + + -- | Triples are (blockId, offset, size) to bitvector-typed entries ( bitvector only/not pointers ) + , fixpointMemSubstitution :: Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) + + -- | Condition which, when true, stays in the loop. This is captured when the (unique, by assumption) + -- symbolic branch that exits the loop is encountered. This condition is updated on each iteration + -- as we widen the invariant. + , fixpointLoopCondition :: Maybe (W4.Pred sym) + } + + +fixpointRecord :: FixpointState sym blocks -> Maybe (FixpointRecord sym blocks) +fixpointRecord BeforeFixpoint = Nothing +fixpointRecord (ComputeFixpoint r) = Just r +fixpointRecord (CheckFixpoint r _) = Just r +fixpointRecord (AfterFixpoint r _) = Just r + + +type FixpointMonad sym = StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO + + +joinRegEntries :: + (?logMessage :: String -> IO (), C.IsSymInterface sym) => + sym -> + Ctx.Assignment (C.RegEntry sym) ctx -> + Ctx.Assignment (C.RegEntry sym) ctx -> + FixpointMonad sym (Ctx.Assignment (C.RegEntry sym) ctx) +joinRegEntries sym = Ctx.zipWithM (joinRegEntry sym) + +joinRegEntry :: + (?logMessage :: String -> IO (), C.IsSymInterface sym) => + sym -> + C.RegEntry sym tp -> + C.RegEntry sym tp -> + FixpointMonad sym (C.RegEntry sym tp) +joinRegEntry sym left right = case C.regType left of + C.LLVMPointerRepr w + + -- special handling for "don't care" registers coming from Macaw + | List.isPrefixOf "cmacaw_reg" (show $ W4.printSymNat $ C.llvmPointerBlock (C.regValue left)) + , List.isPrefixOf "cmacaw_reg" (show $ W4.printSymExpr $ C.llvmPointerOffset (C.regValue left)) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg" + return left + + | C.llvmPointerBlock (C.regValue left) == C.llvmPointerBlock (C.regValue right) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr" + subst <- get + if isJust (W4.testEquality (C.llvmPointerOffset (C.regValue left)) (C.llvmPointerOffset (C.regValue right))) + then do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: left == right" + return left + else case MapF.lookup (C.llvmPointerOffset (C.regValue left)) subst of + Just join_entry -> do + liftIO $ ?logMessage $ + "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Just: " + ++ show (W4.printSymExpr $ bodyValue join_entry) + ++ " -> " + ++ show (W4.printSymExpr $ C.llvmPointerOffset (C.regValue right)) + put $ MapF.insert + (C.llvmPointerOffset (C.regValue left)) + (join_entry { bodyValue = C.llvmPointerOffset (C.regValue right) }) + subst + return left + Nothing -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Nothing" + join_varaible <- liftIO $ W4.freshConstant sym (userSymbol' "reg_join_var") (W4.BaseBVRepr w) + let join_entry = FixpointEntry + { headerValue = C.llvmPointerOffset (C.regValue left) + , bodyValue = C.llvmPointerOffset (C.regValue right) + } + put $ MapF.insert join_varaible join_entry subst + return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) join_varaible + | otherwise -> + fail $ + "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: unsupported pointer base join: " + ++ show (C.ppPtr $ C.regValue left) + ++ " \\/ " + ++ show (C.ppPtr $ C.regValue right) + + C.BoolRepr + | List.isPrefixOf "cmacaw" (show $ W4.printSymExpr $ C.regValue left) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg" + return left + | otherwise -> do + liftIO $ ?logMessage $ + "SimpleLoopFixpoint.joinRegEntry: BoolRepr:" + ++ show (W4.printSymExpr $ C.regValue left) + ++ " \\/ " + ++ show (W4.printSymExpr $ C.regValue right) + join_varaible <- liftIO $ W4.freshConstant sym (userSymbol' "macaw_reg") W4.BaseBoolRepr + return $ C.RegEntry C.BoolRepr join_varaible + + C.StructRepr field_types -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: StructRepr" + C.RegEntry (C.regType left) <$> fmapFC (C.RV . C.regValue) <$> joinRegEntries sym + (Ctx.generate (Ctx.size field_types) $ \i -> + C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue left) Ctx.! i) + (Ctx.generate (Ctx.size field_types) $ \i -> + C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue right) Ctx.! i) + _ -> fail $ "SimpleLoopFixpoint.joinRegEntry: unsupported type: " ++ show (C.regType left) + + +applySubstitutionRegEntries :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + Ctx.Assignment (C.RegEntry sym) ctx -> + Ctx.Assignment (C.RegEntry sym) ctx +applySubstitutionRegEntries sym substitution = fmapFC (applySubstitutionRegEntry sym substitution) + +applySubstitutionRegEntry :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + C.RegEntry sym tp -> + C.RegEntry sym tp +applySubstitutionRegEntry sym substitution entry = case C.regType entry of + C.LLVMPointerRepr{} -> + entry + { C.regValue = C.LLVMPointer + (C.llvmPointerBlock (C.regValue entry)) + (MapF.findWithDefault + (C.llvmPointerOffset (C.regValue entry)) + (C.llvmPointerOffset (C.regValue entry)) + substitution) + } + C.BoolRepr -> + entry + C.StructRepr field_types -> + entry + { C.regValue = fmapFC (C.RV . C.regValue) $ + applySubstitutionRegEntries sym substitution $ + Ctx.generate (Ctx.size field_types) $ + \i -> C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue entry) Ctx.! i + } + _ -> C.panic "SimpleLoopFixpoint.applySubstitutionRegEntry" ["unsupported type: " ++ show (C.regType entry)] + + +findLoopIndex :: + (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + IO (W4.SymBV sym wptr, Natural, Natural) +findLoopIndex sym substitution = do + candidates <- catMaybes <$> mapM + (\(MapF.Pair variable FixpointEntry{..}) -> case W4.testEquality (W4.BaseBVRepr ?ptrWidth) (W4.exprType variable) of + Just Refl -> do + diff <- liftIO $ W4.bvSub sym bodyValue variable + case (BV.asNatural <$> W4.asBV headerValue, BV.asNatural <$> W4.asBV diff) of + (Just start, Just step) -> do + liftIO $ ?logMessage $ + "SimpleLoopFixpoint.findLoopIndex: " ++ show (W4.printSymExpr variable) ++ "=" ++ show (start, step) + return $ Just (variable, start, step) + _ -> return Nothing + Nothing -> return Nothing) + (MapF.toList substitution) + case candidates of + [candidate] -> return candidate + _ -> fail "SimpleLoopFixpoint.findLoopIndex: loop index identification failure." + +findLoopBound :: + (C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + W4.Pred sym -> + Natural -> + Natural -> + IO (W4.SymBV sym wptr) +findLoopBound sym condition _start step = + case Set.toList $ W4.exprUninterpConstants sym condition of + + -- this is a grungy hack, we are expecting exactly three variables and take the first + [C.Some loop_stop, _, _] + | Just Refl <- W4.testEquality (W4.BaseBVRepr ?ptrWidth) (W4.exprType $ W4.varExpr sym loop_stop) -> + W4.bvMul sym (W4.varExpr sym loop_stop) =<< W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral step) + _ -> fail "SimpleLoopFixpoint.findLoopBound: loop bound identification failure." + + +-- index variable information for fixed stride, bounded loops +data LoopIndexBound sym = forall w . 1 <= w => LoopIndexBound + { index :: W4.SymBV sym w + , start :: Natural + , stop :: W4.SymBV sym w + , step :: Natural + } + +findLoopIndexBound :: + (?logMessage :: String -> IO (), C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + Maybe (W4.Pred sym) -> + IO (LoopIndexBound sym) +findLoopIndexBound _sym _substitition Nothing = + fail "findLoopIndexBound: no loop condition recorded!" + +findLoopIndexBound sym substitution (Just condition) = do + (loop_index, start, step) <- findLoopIndex sym substitution + stop <- findLoopBound sym condition start step + return $ LoopIndexBound + { index = loop_index + , start = start + , stop = stop + , step = step + } + +-- hard-coded here that we are always looking for a loop condition delimited by an unsigned comparison +loopIndexBoundCondition :: + (C.IsSymInterface sym, 1 <= w) => + sym -> + W4.SymBV sym w -> + W4.SymBV sym w -> + IO (W4.Pred sym) +loopIndexBoundCondition = W4.bvUlt + +-- | Describes an assumed invariant on the loop index variable, which is that it is an offset +-- from the initial value that is a multiple of a discoveded stride value. +loopIndexStartStepCondition :: + C.IsSymInterface sym => + sym -> + LoopIndexBound sym -> + IO (W4.Pred sym) +loopIndexStartStepCondition sym LoopIndexBound{ index = loop_index, start = start, step = step } = do + start_bv <- W4.bvLit sym (W4.bvWidth loop_index) (BV.mkBV (W4.bvWidth loop_index) $ fromIntegral start) + step_bv <- W4.bvLit sym (W4.bvWidth loop_index) (BV.mkBV (W4.bvWidth loop_index) $ fromIntegral step) + W4.bvEq sym start_bv =<< W4.bvUrem sym loop_index step_bv + + +loadMemJoinVariables :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + bak -> + C.MemImpl sym -> + Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) -> + IO (MapF (W4.SymExpr sym) (W4.SymExpr sym)) +loadMemJoinVariables bak mem subst = + let sym = C.backendGetSym bak in + MapF.fromList <$> mapM + (\((blk, off, _sz), (MemFixpointEntry { memFixpointEntryJoinVariable = join_varaible }, storeage_type)) -> do + ptr <- C.LLVMPointer <$> W4.natLit sym blk <*> W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral off) + val <- C.doLoad bak mem ptr storeage_type (C.LLVMPointerRepr $ W4.bvWidth join_varaible) C.noAlignment + case W4.asNat (C.llvmPointerBlock val) of + Just 0 -> return $ MapF.Pair join_varaible $ C.llvmPointerOffset val + _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val)) + (Map.toAscList subst) + +storeMemJoinVariables :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + bak -> + C.MemImpl sym -> + Map (Natural, Natural, Natural) (MemFixpointEntry sym, C.StorageType) -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + IO (C.MemImpl sym) +storeMemJoinVariables bak mem mem_subst eq_subst = + let sym = C.backendGetSym bak in + foldlM + (\mem_acc ((blk, off, _sz), (MemFixpointEntry { memFixpointEntryJoinVariable = join_varaible }, storeage_type)) -> do + ptr <- C.LLVMPointer <$> W4.natLit sym blk <*> W4.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth $ fromIntegral off) + C.doStore bak mem_acc ptr (C.LLVMPointerRepr $ W4.bvWidth join_varaible) storeage_type C.noAlignment =<< + C.llvmPointer_bv sym (MapF.findWithDefault join_varaible join_varaible eq_subst)) + mem + (Map.toAscList mem_subst) + +dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym) +dropMemStackFrame mem = case (C.memImplHeap mem) ^. C.memState of + (C.StackFrame _ _ _ (a, w) s) -> ((mem { C.memImplHeap = (C.memImplHeap mem) & C.memState .~ s }), a, w) + _ -> C.panic "SimpleLoopFixpoint.dropMemStackFrame" ["not a stack frame:", show (C.ppMem $ C.memImplHeap mem)] + + +filterSubstitution :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + MapF (W4.SymExpr sym) (FixpointEntry sym) +filterSubstitution sym substitution = + -- TODO: fixpoint + let uninterp_constants = foldMapF + (Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue) + substitution + in + MapF.filterWithKey (\variable _entry -> Set.member (C.Some variable) uninterp_constants) substitution + +-- find widening variables that are actually the same (up to syntactic equality) +-- and can be substituted for each other +uninterpretedConstantEqualitySubstitution :: + forall sym . + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym)) +uninterpretedConstantEqualitySubstitution _sym substitution = + let reverse_substitution = MapF.foldlWithKey' + (\accumulator variable entry -> MapF.insert entry variable accumulator) + MapF.empty + substitution + uninterpreted_constant_substitution = fmapF + (\entry -> fromJust $ MapF.lookup entry reverse_substitution) + substitution + normal_substitution = MapF.filterWithKey + (\variable _entry -> + Just Refl == W4.testEquality variable (fromJust $ MapF.lookup variable uninterpreted_constant_substitution)) + substitution + in + (normal_substitution, uninterpreted_constant_substitution) + + +userSymbol' :: String -> W4.SolverSymbol +userSymbol' = fromRight (C.panic "SimpleLoopFixpoint.userSymbol'" []) . W4.userSymbol + + +-- | This execution feature is designed to allow a limited form of +-- verification for programs with unbounded looping structures. +-- +-- It is currently highly experimental and has many limititations. +-- Most notibly, it only really works properly for functions +-- consiting of a single, non-nested loop with a single exit point. +-- Moreover, the loop must have an indexing variable that counts up +-- from a starting point by a fixed stride amount. +-- +-- Currently, these assumptions about the loop strucutre are not +-- checked. +-- +-- The basic use case here is for verifiying functions that loop +-- through an array of data of symbolic length. This is done by +-- providing a \""fixpoint function\" which describes how the live +-- values in the loop at an arbitrary iteration are used to compute +-- the final values of those variables before execution leaves the +-- loop. The number and order of these variables depends on +-- internal details of the representation, so is relatively fragile. +simpleLoopFixpoint :: + forall sym ext p rtp blocks init ret . + (C.IsSymInterface sym, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + sym -> + C.CFG ext blocks init ret {- ^ The function we want to verify -} -> + C.GlobalVar C.Mem {- ^ global variable representing memory -} -> + (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) -> + IO (C.ExecutionFeature p sym ext rtp) +simpleLoopFixpoint sym cfg@C.CFG{..} mem_var fixpoint_func = do + let ?ptrWidth = knownNat @64 + + verbSetting <- W4.getOptionSetting W4.verbosity $ W4.getConfiguration sym + verb <- fromInteger <$> W4.getOpt verbSetting + + -- Doesn't really work if there are nested loops: looop datastructures will + -- overwrite each other. Currently no error message. + + -- Really only works for single-exit loops; need a message for that too. + + let flattenWTOComponent = \case + C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps + C.Vertex v -> [v] + let loop_map = Map.fromList $ mapMaybe + (\case + C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) + C.Vertex{} -> Nothing) + (C.cfgWeakTopologicalOrdering cfg) + + fixpoint_state_ref <- newIORef @(FixpointState sym blocks) BeforeFixpoint + + return $ C.ExecutionFeature $ \exec_state -> do + let ?logMessage = \msg -> when (verb >= (3 :: Natural)) $ do + let h = C.printHandle $ C.execStateContext exec_state + System.IO.hPutStrLn h msg + System.IO.hFlush h + fixpoint_state <- readIORef fixpoint_state_ref + C.withBackend (C.execStateContext exec_state) $ \bak -> + case exec_state of + C.RunningState (C.RunBlockStart block_id) sim_state + | C.SomeHandle cfgHandle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + + -- make sure the types match + , Just Refl <- W4.testEquality + (fmapFC C.blockInputs cfgBlockMap) + (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + + -- loop map is what we computed above, is this state at a loop header + , Map.member (C.Some block_id) loop_map -> + + advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state fixpoint_state_ref + + | otherwise -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + return C.ExecutionFeatureNoChange + + + -- TODO: maybe need to rework this, so that we are sure to capture even concrete exits from the loop. + C.SymbolicBranchState branch_condition true_frame false_frame _target sim_state + | Just fixpoint_record <- fixpointRecord fixpoint_state + , Just loop_body_some_block_ids <- Map.lookup (fixpointBlockId fixpoint_record) loop_map + , JustPausedFrameTgtId true_frame_some_block_id <- pausedFrameTgtId true_frame + , JustPausedFrameTgtId false_frame_some_block_id <- pausedFrameTgtId false_frame + , C.SomeHandle cfgHandle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + , Just Refl <- W4.testEquality + (fmapFC C.blockInputs cfgBlockMap) + (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + , elem true_frame_some_block_id loop_body_some_block_ids /= elem false_frame_some_block_id loop_body_some_block_ids -> do + + (loop_condition, inside_loop_frame, outside_loop_frame) <- + if elem true_frame_some_block_id loop_body_some_block_ids + then + return (branch_condition, true_frame, false_frame) + else do + not_branch_condition <- W4.notPred sym branch_condition + return (not_branch_condition, false_frame, true_frame) + + (condition, frame) <- case fixpoint_state of + BeforeFixpoint -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint:" ["BeforeFixpoint"] + + ComputeFixpoint _fixpoint_record -> do + -- continue in the loop + ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint" + writeIORef fixpoint_state_ref $ + ComputeFixpoint fixpoint_record { fixpointLoopCondition = Just loop_condition } + return (loop_condition, inside_loop_frame) + + CheckFixpoint _fixpoint_record _loop_bound -> do + -- continue in the loop + ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint" + return (loop_condition, inside_loop_frame) + + AfterFixpoint _fixpoint_record _loop_bound -> do + -- break out of the loop + ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint" + not_loop_condition <- W4.notPred sym loop_condition + return (not_loop_condition, outside_loop_frame) + + loc <- W4.getCurrentProgramLoc sym + C.addAssumption bak $ C.BranchCondition loc (C.pausedLoc frame) condition + C.ExecutionFeatureNewState <$> + runReaderT + (C.resumeFrame (C.forgetPostdomFrame frame) $ sim_state ^. (C.stateTree . C.actContext)) + sim_state + + _ -> return C.ExecutionFeatureNoChange + + +advanceFixpointState :: + forall sym bak ext p rtp blocks r args . + (C.IsSymBackend sym bak, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + C.GlobalVar C.Mem -> + (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), W4.Pred sym)) -> + C.BlockID blocks args -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + FixpointState sym blocks -> + IORef (FixpointState sym blocks) -> + IO (C.ExecutionFeatureResult p sym ext rtp) + +advanceFixpointState bak mem_var fixpoint_func block_id sim_state fixpoint_state fixpoint_state_ref = + let ?ptrWidth = knownNat @64 in + let sym = C.backendGetSym bak in + case fixpoint_state of + BeforeFixpoint -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: BeforeFixpoint -> ComputeFixpoint" + assumption_frame_identifier <- C.pushAssumptionFrame bak + let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl } + writeIORef fixpoint_state_ref $ ComputeFixpoint $ + FixpointRecord + { fixpointBlockId = C.Some block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = MapF.empty + , fixpointRegMap = sim_state ^. (C.stateCrucibleFrame . C.frameRegs) + , fixpointMemSubstitution = Map.empty + , fixpointLoopCondition = Nothing -- we don't know the loop condition yet + } + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + ComputeFixpoint fixpoint_record + | FixpointRecord { fixpointRegMap = reg_map } <- fixpoint_record + , Just Refl <- W4.testEquality + (fmapFC C.regType $ C.regMap reg_map) + (fmapFC C.regType $ C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs)) -> do + + + ?logMessage $ "SimpleLoopFixpoint: RunningState: ComputeFixpoint: " ++ show block_id + _ <- C.popAssumptionFrameAndObligations bak $ fixpointAssumptionFrameIdentifier fixpoint_record + + -- widen the inductive condition + (join_reg_map, join_substitution) <- runStateT + (joinRegEntries sym + (C.regMap reg_map) + (C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs))) $ + fixpointSubstitution fixpoint_record + + let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let (header_mem_impl, mem_allocs, mem_writes) = dropMemStackFrame body_mem_impl + when (C.sizeMemAllocs mem_allocs /= 0) $ + fail "SimpleLoopFixpoint: unsupported memory allocation in loop body." + + -- widen the memory + mem_substitution_candidate <- Map.fromList <$> catMaybes <$> case mem_writes of + C.MemWrites [C.MemWritesChunkIndexed mmm] -> mapM + (\case + (C.MemWrite ptr (C.MemStore _ storeage_type _)) + | Just blk <- W4.asNat (C.llvmPointerBlock ptr) + , Just off <- BV.asNatural <$> W4.asBV (C.llvmPointerOffset ptr) -> do + let sz = C.typeEnd 0 storeage_type + some_join_varaible <- liftIO $ case W4.mkNatRepr $ C.bytesToBits sz of + C.Some bv_width + | Just C.LeqProof <- W4.testLeq (W4.knownNat @1) bv_width -> do + join_varaible <- W4.freshConstant sym + (userSymbol' "mem_join_var") + (W4.BaseBVRepr bv_width) + return $ MemFixpointEntry + { memFixpointEntrySym = sym + , memFixpointEntryJoinVariable = join_varaible + } + | otherwise -> + C.panic + "SimpleLoopFixpoint.simpleLoopFixpoint" + ["unexpected storage type " ++ show storeage_type ++ " of size " ++ show sz] + return $ Just ((blk, off, fromIntegral sz), (some_join_varaible, storeage_type)) + | Just blk <- W4.asNat (C.llvmPointerBlock ptr) + , Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr) -> do + maybe_ranges <- runMaybeT $ + C.writeRangesMem @_ @64 sym $ C.memImplHeap header_mem_impl + case maybe_ranges of + Just ranges -> do + sz <- W4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth $ toInteger $ C.typeEnd 0 storeage_type + forM_ (Map.findWithDefault [] blk ranges) $ \(prev_off, prev_sz) -> do + disjoint_pred <- C.buildDisjointRegionsAssertionWithSub + sym + ptr + sz + (C.LLVMPointer (C.llvmPointerBlock ptr) prev_off) + prev_sz + when (W4.asConstantPred disjoint_pred /= Just True) $ + fail $ + "SimpleLoopFixpoint: non-disjoint ranges: off1=" + ++ show (W4.printSymExpr (C.llvmPointerOffset ptr)) + ++ ", sz1=" + ++ show (W4.printSymExpr sz) + ++ ", off2=" + ++ show (W4.printSymExpr prev_off) + ++ ", sz2=" + ++ show (W4.printSymExpr prev_sz) + return Nothing + Nothing -> fail $ "SimpleLoopFixpoint: unsupported symbolic pointers" + _ -> fail $ "SimpleLoopFixpoint: not MemWrite: " ++ show (C.ppMemWrites mem_writes)) + (List.concat $ IntMap.elems mmm) + _ -> fail $ "SimpleLoopFixpoint: not MemWritesChunkIndexed: " ++ show (C.ppMemWrites mem_writes) + + -- check that the mem substitution always computes the same footprint on every iteration (!?!) + mem_substitution <- if Map.null (fixpointMemSubstitution fixpoint_record) + then return mem_substitution_candidate + else if Map.keys mem_substitution_candidate == Map.keys (fixpointMemSubstitution fixpoint_record) + then return $ fixpointMemSubstitution fixpoint_record + else fail "SimpleLoopFixpoint: unsupported memory writes change" + + assumption_frame_identifier <- C.pushAssumptionFrame bak + + -- check if we are done; if we did not introduce any new variables, we don't have to widen any more + if MapF.keys join_substitution == MapF.keys (fixpointSubstitution fixpoint_record) + + -- we found the fixpoint, get ready to wrap up + then do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: ComputeFixpoint -> CheckFixpoint" + ?logMessage $ + "SimpleLoopFixpoint: cond: " ++ + show (maybe "Nothing" W4.printSymExpr $ fixpointLoopCondition fixpoint_record) + + -- we have delayed populating the main substituation map with + -- memory variables, so we have to do that now + + header_mem_substitution <- loadMemJoinVariables bak header_mem_impl $ + fixpointMemSubstitution fixpoint_record + body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ + fixpointMemSubstitution fixpoint_record + + -- try to unify widening variables that have the same values + let (normal_substitution, equality_substitution) = uninterpretedConstantEqualitySubstitution sym $ + -- drop variables that don't appear along some back edge (? understand this better) + filterSubstitution sym $ + MapF.union join_substitution $ + -- this implements zip, because the two maps have the same keys + MapF.intersectWithKeyMaybe + (\_k x y -> Just $ FixpointEntry{ headerValue = x, bodyValue = y }) + header_mem_substitution + body_mem_substitution + -- ?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList normal_substitution) + -- ?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution) + + -- unify widening variables in the register subst + let res_reg_map = applySubstitutionRegEntries sym equality_substitution join_reg_map + + -- unify widening varialbes in the memory subst + res_mem_impl <- storeMemJoinVariables + bak + (header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) }) + mem_substitution + equality_substitution + + -- finally we can determine the loop bounds + loop_index_bound <- findLoopIndexBound sym normal_substitution $ fixpointLoopCondition fixpoint_record + + (_ :: ()) <- case loop_index_bound of + LoopIndexBound{ index = loop_index, stop = loop_stop } -> do + loc <- W4.getCurrentProgramLoc sym + index_bound_condition <- loopIndexBoundCondition sym loop_index loop_stop + C.addAssumption bak $ C.GenericAssumption loc "" index_bound_condition + index_start_step_condition <- loopIndexStartStepCondition sym loop_index_bound + C.addAssumption bak $ C.GenericAssumption loc "" index_start_step_condition + + writeIORef fixpoint_state_ref $ + CheckFixpoint + FixpointRecord + { fixpointBlockId = C.Some block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = normal_substitution + , fixpointRegMap = C.RegMap res_reg_map + , fixpointMemSubstitution = mem_substitution + , fixpointLoopCondition = fixpointLoopCondition fixpoint_record + } + loop_index_bound + + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap res_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + else do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: ComputeFixpoint: -> ComputeFixpoint" + + -- write any new widening variables into memory state + res_mem_impl <- storeMemJoinVariables bak + (header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) }) + mem_substitution + MapF.empty + + writeIORef fixpoint_state_ref $ ComputeFixpoint + FixpointRecord + { fixpointBlockId = C.Some block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = join_substitution + , fixpointRegMap = C.RegMap join_reg_map + , fixpointMemSubstitution = mem_substitution + , fixpointLoopCondition = Nothing + } + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap join_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: ComputeFixpoint"] + + CheckFixpoint fixpoint_record loop_bound + | FixpointRecord { fixpointRegMap = reg_map } <- fixpoint_record + , Just Refl <- W4.testEquality + (fmapFC C.regType $ C.regMap reg_map) + (fmapFC C.regType $ C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs)) -> do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: " + ++ "CheckFixpoint" + ++ " -> " + ++ "AfterFixpoint" + ++ ": " + ++ show block_id + + loc <- W4.getCurrentProgramLoc sym + + -- assert that the hypothesis we made about the loop termination condition is true + (_ :: ()) <- case loop_bound of + LoopIndexBound{ index = loop_index, stop = loop_stop } -> do + -- check the loop index bound condition + index_bound_condition <- loopIndexBoundCondition + sym + (bodyValue $ fromJust $ MapF.lookup loop_index $ fixpointSubstitution fixpoint_record) + loop_stop + C.addProofObligation bak $ C.LabeledPred index_bound_condition $ C.SimError loc "" + + _ <- C.popAssumptionFrame bak $ fixpointAssumptionFrameIdentifier fixpoint_record + + let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let (header_mem_impl, _mem_allocs, _mem_writes) = dropMemStackFrame body_mem_impl + + body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record + let res_substitution = MapF.mapWithKey + (\variable fixpoint_entry -> + fixpoint_entry + { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution + }) + (fixpointSubstitution fixpoint_record) + -- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution) + + -- match things up with the input function that describes the loop body behavior + (fixpoint_func_substitution, fixpoint_func_condition) <- liftIO $ + case fixpointLoopCondition fixpoint_record of + Nothing -> fail "When checking the result of a fixpoint, no loop condition was found!" + Just c -> fixpoint_func res_substitution c + + C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc "" + -- ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution) + + let res_reg_map = C.RegMap $ + applySubstitutionRegEntries sym fixpoint_func_substitution (C.regMap reg_map) + + res_mem_impl <- storeMemJoinVariables bak + header_mem_impl + (fixpointMemSubstitution fixpoint_record) + fixpoint_func_substitution + + (_ :: ()) <- case loop_bound of + LoopIndexBound{ index = loop_index, stop = loop_stop } -> do + let loop_index' = MapF.findWithDefault loop_index loop_index fixpoint_func_substitution + index_bound_condition <- loopIndexBoundCondition sym loop_index' loop_stop + C.addAssumption bak $ C.GenericAssumption loc "" index_bound_condition + index_start_step_condition <- loopIndexStartStepCondition sym $ LoopIndexBound + { index = loop_index' + , start = start loop_bound + , stop = loop_stop + , step = step loop_bound + } + C.addAssumption bak $ C.GenericAssumption loc "" index_start_step_condition + + writeIORef fixpoint_state_ref $ + AfterFixpoint + fixpoint_record{ fixpointSubstitution = res_substitution } + loop_bound + + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ res_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + + AfterFixpoint{} -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["AfterFixpoint"] + + +data MaybePausedFrameTgtId f where + JustPausedFrameTgtId :: C.Some (C.BlockID b) -> MaybePausedFrameTgtId (C.CrucibleLang b r) + NothingPausedFrameTgtId :: MaybePausedFrameTgtId f + +pausedFrameTgtId :: C.PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f +pausedFrameTgtId C.PausedFrame{ resume = resume } = case resume of + C.ContinueResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id + C.CheckMergeResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id + _ -> NothingPausedFrameTgtId From 5040e5709ed839241ce6e1042a635141f22ac6ea Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 May 2024 16:56:44 -0400 Subject: [PATCH 32/35] Fix -Wunused-do-bind warning --- crux-llvm/src/Crux/LLVM/Simulate.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index e15b0971d..027d70e1e 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/crux-llvm/src/Crux/LLVM/Simulate.hs @@ -139,13 +139,13 @@ registerFunctions llvmOpts llvm_module mtrans fs0 = ?memOpts = memOpts llvmOpts -- register the callable override functions - register_llvm_overrides llvm_module [] - (concat [ cruxLLVMOverrides proxy# - , svCompOverrides - , cbmcOverrides proxy# - , maybe [] symio_overrides fs0 - ]) - llvm_ctx + _ <- register_llvm_overrides llvm_module [] + (concat [ cruxLLVMOverrides proxy# + , svCompOverrides + , cbmcOverrides proxy# + , maybe [] symio_overrides fs0 + ]) + llvm_ctx -- register all the functions defined in the LLVM module registerLazyModule sayTranslationWarning mtrans From 867a7ed131ca29673dd011573bf65a047eaaaa05 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 11:09:41 -0400 Subject: [PATCH 33/35] Bump what4 to bring in latest changes from GaloisInc/what4#256 --- dependencies/what4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dependencies/what4 b/dependencies/what4 index 512eca663..8c9401b5d 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 512eca66373a900be1175c1e06aed4041bcf6f54 +Subproject commit 8c9401b5d21d20451d224d4834bd611fc83b850b From 1f39b6b6a773bb2a1e48f6eaedcbd59dff197a7f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 11:13:11 -0400 Subject: [PATCH 34/35] Remove commented-out exports --- crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs index 4aaa10ed7..32c175076 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs @@ -95,12 +95,6 @@ module Lang.Crucible.LLVM.SimpleLoopInvariant ( InvariantEntry(..) , InvariantPhase(..) , simpleLoopInvariant - -- , MemorySubstitution(..) - -- , computeMemSubstitution - -- , constructMemSubstitutionCandidate - -- , checkMemSubst - -- , loadMemJoinVariables - -- , storeMemJoinVariables ) where import Control.Lens From c2c11dc1fedf870d73a1d788d8711a3d019e535b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 12:43:01 -0400 Subject: [PATCH 35/35] Review comments --- .../src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs index da1afa3cf..7765c57ab 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs @@ -106,7 +106,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Type as C -- | When live loop-carried dependencies are discovered as we traverse -- a loop body, new "widening" variables are introduced to stand in --- for those locations. When we introduce such a varible, we +-- for those locations. When we introduce such a variable, we -- capture what value the variable had when we entered the loop (the -- \"header\" value); this is essentially the initial value of the -- variable. We also compute what value the variable should take on @@ -286,13 +286,19 @@ callFrameContextPush hdl bid = callFrameContextUpdate hdl $ \ctx -> ctx { callFrameContextLoopHeaders = bid : callFrameContextLoopHeaders ctx } +-- | Precondition: the context's 'callFrameContextLoopHeaders' should be +-- non-empty. callFrameContextPop :: CallFrameHandle init ret blocks -> ExecutionFeatureContext sym wptr ext -> ExecutionFeatureContext sym wptr ext callFrameContextPop hdl = callFrameContextUpdate hdl $ - \ctx -> ctx { callFrameContextLoopHeaders = tail $ callFrameContextLoopHeaders ctx } + \ctx -> ctx { callFrameContextLoopHeaders = + case callFrameContextLoopHeaders ctx of + _:hdrs -> hdrs + [] -> C.panic "callFrameContextPop" + ["Empty callFrameContextLoopHeaders"] } callFrameContextPeek :: CallFrameHandle init ret blocks ->