GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-25 21:54:51 +03:00
Code Issues Projects Releases Wiki Activity

support alignment ops when processing statements in RegisterUse

Browse Source 
For some reason we were very conservative in our support or abstract
operations over the processor state in the `RegisterUse` analysis.

In particular, we were failing to process code such as:

r23 := (bv_and r21 (0xfffffffffffffff0 :: [64]))

whose goal is to align the value in r21 at a 16-byte boundary.

This resulted in us failing to analyze some code that was realigning its
stack pointer.  With this change, the same code succeeds at propagating
the abstract stack pointer offset forward.
This commit is contained in:
Valentin Robert 2024-07-23 16:19:18 -07:00
parent 32244627f2
commit dc1591d168
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
base/src/Data/Macaw/Analysis/RegisterUse.hs
View File

@ -71,6 +71,7 @@ import Control.Monad (unless, when, zipWithM_)
import Control.Monad.Except (MonadError(..), Except)
import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks)
import Control.Monad.State.Strict (MonadState(..), State, StateT, execStateT, evalState, gets, modify)
import qualified Data.Bits as Bits
import qualified Data.ByteString.Char8 as BSC
import qualified Data.ByteString as BS
import Data.Foldable
@ -664,6 +665,9 @@ addMemAccessInfo :: StmtIndex -> MemAccessInfo arch ids -> StartInfer arch ids (
addMemAccessInfo idx i = seq idx $ seq i $ do
modify $ \s -> s { sisMemAccessStack = (idx,i) : sisMemAccessStack s }
-- | @processApp aid app@ computes the effect of a program assignment @aid <- app@. When `app` is
-- a computation over a stack offset expression (a `FrameExpr`), we attempt to simplify it, as we
-- require a concrete stack offset when computing `postCallConstraints`.
processApp :: (OrdF (ArchReg arch), MemWidth (ArchAddrWidth arch))
=> AssignId ids tp
-> App (Value arch ids) tp
@ -671,6 +675,11 @@ processApp :: (OrdF (ArchReg arch), MemWidth (ArchAddrWidth arch))
processApp aid app = do
ctx <- ask
am <- gets sisAssignMap
-- This inspects the `app` term to detect cases where the abstract expression can be simplified
-- down to a `FrameExpr` expression. In such cases, the simplified expression is registered as
-- the value for this assignment. Otherwise, the value for the assignment remains abstract.
-- This may not be exhaustive, so if you encounter the `CallStackHeightError` in
-- `postCallConstraints`, you may need to extend the patterns recognized here.
case fmapFC (valueToStartExpr ctx am) app of
BVAdd _ (FrameExpr o) (IVCValue (BVCValue _ c)) ->
setAssignVal aid (FrameExpr (o+fromInteger c))
@ -678,6 +687,10 @@ processApp aid app = do
setAssignVal aid (FrameExpr (o+fromInteger c))
BVSub _ (FrameExpr o) (IVCValue (BVCValue _ c)) ->
setAssignVal aid (FrameExpr (o-fromInteger c))
BVAnd _ (FrameExpr o) (IVCValue (BVCValue _ c)) ->
setAssignVal aid (FrameExpr (o Bits..&. fromInteger c))
BVAnd _ (IVCValue (BVCValue _ c)) (FrameExpr o) ->
setAssignVal aid (FrameExpr (o Bits..&. fromInteger c))
appExpr -> do
c <- gets sisAppCache
-- Check to see if we have seen an app equivalent to