Track and check alignment for memory regions in llvm overrides

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,53 +1451,89 @@ 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 ->
   Options        ->
   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 ->
   Options        ->
   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 -} ->

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)

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
     }

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

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