diff --git a/deps/crucible b/deps/crucible index 313441c194..03aa61dfed 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 313441c194509d4a84045b2973d22eecd88d9df9 +Subproject commit 03aa61dfed7322c997ecc7d6fb4f252b6f36e224 diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index be5d5221ec..60cd5b5913 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -44,6 +44,7 @@ module SAWScript.Crucible.LLVM.Builtins , crucible_llvm_unsafe_assume_spec , crucible_fresh_var , crucible_alloc + , crucible_alloc_aligned , crucible_alloc_readonly , crucible_alloc_with_size , crucible_alloc_global @@ -676,15 +677,13 @@ assertEqualVals cc v1 v2 = -- TODO(langston): combine with/move to executeAllocation doAlloc :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> LLVMAllocSpec -> StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch)) -doAlloc cc (LLVMAllocSpec mut _memTy sz loc) = StateT $ \mem -> +doAlloc cc (LLVMAllocSpec mut _memTy alignment sz loc) = StateT $ \mem -> do let sym = cc^.ccBackend - let dl = Crucible.llvmDataLayout ?lc sz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToInteger sz - let alignment = Crucible.maxAlignment dl -- Use the maximum alignment required for any primitive type (FIXME?) let l = show (W4.plSourceLoc loc) liftIO $ Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment @@ -1452,37 +1451,53 @@ crucible_alloc_internal _bic _opt lty spec = do crucible_alloc_with_mutability_and_size :: Crucible.Mutability -> Maybe (Crucible.Bytes) -> + Maybe Crucible.Alignment -> BuiltinContext -> Options -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_alloc_with_mutability_and_size mut sz bic opts lty = LLVMCrucibleSetupM $ do - cctx <- getLLVMCrucibleContext - loc <- getW4Position "crucible_alloc" - memTy <- memTypeForLLVMType bic lty - - let memTySize = - let ?lc = ccTypeCtx cctx - ?dl = Crucible.llvmDataLayout ?lc - in Crucible.memTypeSize ?dl memTy - - sz' <- - case sz of - Just sz_ -> do - when (sz_ < memTySize) $ fail $ unlines - [ "User error: manually-specified allocation size was less than needed" - , "Needed for this type: " ++ show memTySize - , "Specified: " ++ show sz_ - ] - pure sz_ - Nothing -> pure (Crucible.toBytes memTySize) - - crucible_alloc_internal bic opts lty $ - LLVMAllocSpec { _allocSpecMut = mut - , _allocSpecType = memTy - , _allocSpecBytes = sz' - , _allocSpecLoc = loc - } +crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty = + LLVMCrucibleSetupM $ + do cctx <- getLLVMCrucibleContext + loc <- getW4Position "crucible_alloc" + memTy <- memTypeForLLVMType bic lty + + let lc = ccTypeCtx cctx + let dl = Crucible.llvmDataLayout lc + let memTySize = Crucible.memTypeSize dl memTy + let memTyAlign = Crucible.memTypeAlign dl memTy + + sz' <- + case sz of + Just sz_ -> do + when (sz_ < memTySize) $ fail $ unlines + [ "User error: manually-specified allocation size was less than needed" + , "Needed for this type: " ++ show memTySize + , "Specified: " ++ show sz_ + ] + pure sz_ + Nothing -> pure (Crucible.toBytes memTySize) + + alignment' <- + case alignment of + Just a -> do + when (a < memTyAlign) $ fail $ unlines + [ "User error: manually-specified alignment was less than needed" + , "Allocation type: " ++ show memTy + , "Minimum alignment for type: " ++ show (Crucible.fromAlignment memTyAlign) ++ "-byte" + , "Specified alignment: " ++ show (Crucible.fromAlignment a) ++ "-byte" + ] + pure a + Nothing -> pure memTyAlign + + crucible_alloc_internal bic opts lty $ + LLVMAllocSpec + { _allocSpecMut = mut + , _allocSpecType = memTy + , _allocSpecAlign = alignment' + , _allocSpecBytes = sz' + , _allocSpecLoc = loc + } crucible_alloc :: BuiltinContext -> @@ -1490,7 +1505,27 @@ crucible_alloc :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) crucible_alloc = - crucible_alloc_with_mutability_and_size Crucible.Mutable Nothing + crucible_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing + +crucible_alloc_aligned :: + BuiltinContext -> + Options -> + Int -> + L.Type -> + LLVMCrucibleSetupM (AllLLVM SetupValue) +crucible_alloc_aligned bic opts n lty = + case Crucible.toAlignment (Crucible.toBytes n) of + Nothing -> + LLVMCrucibleSetupM $ fail $ + "crucible_alloc_aligned: invalid non-power-of-2 alignment: " ++ show n + Just alignment -> + crucible_alloc_with_mutability_and_size + Crucible.Mutable + Nothing + (Just alignment) + bic + opts + lty crucible_alloc_readonly :: BuiltinContext -> @@ -1498,7 +1533,7 @@ crucible_alloc_readonly :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) crucible_alloc_readonly = - crucible_alloc_with_mutability_and_size Crucible.Immutable Nothing + crucible_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing crucible_alloc_with_size :: BuiltinContext -> @@ -1510,6 +1545,7 @@ crucible_alloc_with_size bic opts sz lty = crucible_alloc_with_mutability_and_size Crucible.Mutable (Just (Crucible.toBytes sz)) + Nothing bic opts lty @@ -1538,23 +1574,25 @@ constructFreshPointer :: W4.ProgramLoc -> Crucible.MemType -> CrucibleSetup (LLVM arch) (AllLLVM SetupValue) -constructFreshPointer mid loc memTy = do - cctx <- getLLVMCrucibleContext - let ?lc = ccTypeCtx cctx - let ?dl = Crucible.llvmDataLayout ?lc - n <- Setup.csVarCounter <<%= nextAllocIndex - let sz = Crucible.memTypeSize ?dl memTy - Setup.currentState . MS.csFreshPointers . at n ?= - LLVMAllocSpec { _allocSpecMut = Crucible.Mutable - , _allocSpecType = memTy - , _allocSpecBytes = sz - , _allocSpecLoc = loc - } - -- TODO: refactor - case mid of - Just i -> Setup.currentState . MS.csVarTypeNames.at n ?= i - Nothing -> return () - return (mkAllLLVM (SetupVar n)) +constructFreshPointer mid loc memTy = + do cctx <- getLLVMCrucibleContext + let ?lc = ccTypeCtx cctx + let ?dl = Crucible.llvmDataLayout ?lc + n <- Setup.csVarCounter <<%= nextAllocIndex + let sz = Crucible.memTypeSize ?dl memTy + let alignment = Crucible.memTypeAlign ?dl memTy + Setup.currentState . MS.csFreshPointers . at n ?= + LLVMAllocSpec { _allocSpecMut = Crucible.Mutable + , _allocSpecType = memTy + , _allocSpecAlign = alignment + , _allocSpecBytes = sz + , _allocSpecLoc = loc + } + -- TODO: refactor + case mid of + Just i -> Setup.currentState . MS.csVarTypeNames.at n ?= i + Nothing -> return () + return (mkAllLLVM (SetupVar n)) crucible_points_to :: Bool {- ^ whether to check type compatibility -} -> diff --git a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs index 763a0b625a..ab10a77f6f 100644 --- a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs +++ b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs @@ -31,6 +31,7 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM , ptrBitwidth , integerAlignment , floatAlignment + , fromAlignment , EndianForm(..) -- * Re-exports from "Lang.Crucible.LLVM.Extension" , ArchWidth @@ -137,7 +138,7 @@ import Lang.Crucible.LLVM.Bytes import Lang.Crucible.LLVM.DataLayout (Alignment, noAlignment, padToAlignment, DataLayout, EndianForm(..), - integerAlignment, floatAlignment, intWidthSize, ptrBitwidth) + integerAlignment, floatAlignment, fromAlignment, intWidthSize, ptrBitwidth) import Lang.Crucible.LLVM.Extension (ArchWidth) diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index d5619558c0..2a60c6a546 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -39,6 +39,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR -- * LLVMAllocSpec , LLVMAllocSpec(..) , allocSpecType + , allocSpecAlign , allocSpecMut , allocSpecLoc , allocSpecBytes @@ -183,6 +184,7 @@ data LLVMAllocSpec = LLVMAllocSpec { _allocSpecMut :: CL.Mutability , _allocSpecType :: CL.MemType + , _allocSpecAlign :: CL.Alignment , _allocSpecBytes :: CL.Bytes , _allocSpecLoc :: ProgramLoc } diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 08f8deba12..cba427a0d8 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -612,12 +612,13 @@ learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWi -> PrePost -> MS.StateSpec (LLVM arch) -> OverrideMatcher (LLVM arch) md () -learnCond opts sc cc cs prepost ss = do - let loc = cs ^. MS.csLoc - matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) - traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) - enforceDisjointness loc ss - enforceCompleteSubstitution loc ss +learnCond opts sc cc cs prepost ss = + do let loc = cs ^. MS.csLoc + matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) + traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + enforcePointerValidity cc loc ss + enforceDisjointness loc ss + enforceCompleteSubstitution loc ss -- | Verify that all of the fresh variables for the given @@ -688,6 +689,44 @@ refreshTerms sc ss = ------------------------------------------------------------------------ +-- | Generate assertions that all of the memory regions matched by an +-- override's precondition are allocated, and meet the appropriate +-- requirements for alignment and mutability. +enforcePointerValidity :: + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + LLVMCrucibleContext arch -> + W4.ProgramLoc -> + MS.StateSpec (LLVM arch) -> + OverrideMatcher (LLVM arch) md () +enforcePointerValidity cc loc ss = + do sym <- Ov.getSymInterface + sub <- OM (use setupValueSub) -- Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) + let allocs = view MS.csAllocs ss -- Map AllocIndex LLVMAllocSpec + let mems = Map.elems $ Map.intersectionWith (,) allocs sub + let w = Crucible.PtrWidth + let memVar = Crucible.llvmMemVar (ccLLVMContext cc) + mem <- readGlobal memVar + + sequence_ + [ do psz' <- + liftIO $ W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToInteger psz + c <- + liftIO $ + Crucible.isAllocatedAlignedPointer sym w alignment mut ptr (Just psz') mem + let msg = + "Pointer not valid:" + ++ "\n base = " ++ show (Crucible.ppPtr ptr) + ++ "\n size = " ++ show psz + ++ "\n required alignment = " ++ show (Crucible.fromAlignment alignment) ++ "-byte" + ++ "\n required mutability = " ++ show mut + addAssert c $ Crucible.SimError loc $ + Crucible.AssertFailureSimError msg "" + + | (LLVMAllocSpec mut _pty alignment psz _ploc, ptr) <- mems + ] + +------------------------------------------------------------------------ + -- | Generate assertions that all of the memory allocations matched by -- an override's precondition are disjoint. Read-only allocations are -- allowed to alias other read-only allocations, however. @@ -724,8 +763,8 @@ enforceDisjointness loc ss = addAssert c $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - | (LLVMAllocSpec _mut _pty psz ploc, p) : ps <- tails memsRW - , (LLVMAllocSpec _mut _qty qsz qloc, q) <- ps ++ memsRO + | (LLVMAllocSpec _mut _pty _align psz ploc, p) : ps <- tails memsRW + , (LLVMAllocSpec _mut _qty _align qsz qloc, q) <- ps ++ memsRO ] ------------------------------------------------------------------------ @@ -1078,9 +1117,11 @@ learnSetupCondition :: PrePost -> MS.SetupCondition (LLVM arch) -> OverrideMatcher (LLVM arch) md () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal loc val1 val2) = learnEqual opts sc cc spec loc prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred loc tm) = learnPred sc cc loc prepost (ttTerm tm) -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Ghost () loc var val) = learnGhost sc cc loc prepost var val +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal loc val1 val2 -> learnEqual opts sc cc spec loc prepost val1 val2 + MS.SetupCond_Pred loc tm -> learnPred sc cc loc prepost (ttTerm tm) + MS.SetupCond_Ghost () loc var val -> learnGhost sc cc loc prepost var val ------------------------------------------------------------------------ @@ -1306,7 +1347,7 @@ executeAllocation :: LLVMCrucibleContext arch -> (AllocIndex, LLVMAllocSpec) -> OverrideMatcher (LLVM arch) RW () -executeAllocation opts cc (var, LLVMAllocSpec mut memTy sz loc) = +executeAllocation opts cc (var, LLVMAllocSpec mut memTy alignment sz loc) = do let sym = cc^.ccBackend {- memTy <- case Crucible.asMemType symTy of @@ -1317,7 +1358,6 @@ executeAllocation opts cc (var, LLVMAllocSpec mut memTy sz loc) = let memVar = Crucible.llvmMemVar (ccLLVMContext cc) mem <- readGlobal memVar sz' <- liftIO $ W4.bvLit sym Crucible.PtrWidth (Crucible.bytesToInteger sz) - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) let l = show (W4.plSourceLoc loc) ++ " (Poststate)" (ptr, mem') <- liftIO $ Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index f8e1420288..edd7813b7a 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1807,6 +1807,16 @@ primitives = Map.fromList , "verified is expected to perform the allocation." ] + , prim "crucible_alloc_aligned" "Int -> LLVMType -> CrucibleSetup SetupValue" + (bicVal crucible_alloc_aligned) + Current + [ "Declare that a memory region of the given type should be allocated in" + , "a Crucible specification, and also specify that the start of the region" + , "should be aligned to a multiple of the specified number of bytes (which" + , "must be a power of 2). The specified alignment must be no less than the" + , "minimum required by the LLVM type." + ] + , prim "crucible_alloc_readonly" "LLVMType -> CrucibleSetup SetupValue" (bicVal crucible_alloc_readonly) Current