Skip to content

Commit

Permalink
support alignment ops when processing statements in RegisterUse
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Ptival committed Jul 24, 2024
1 parent 3224462 commit 0986922
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions base/src/Data/Macaw/Analysis/RegisterUse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -678,6 +679,8 @@ 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..&. memInt (fromInteger c)))
appExpr -> do
c <- gets sisAppCache
-- Check to see if we have seen an app equivalent to
Expand Down

0 comments on commit 0986922

Please sign in to comment.