GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 00:42:28 +03:00
Code Issues Projects Releases Wiki Activity

Make the simplifier more powerful

Browse Source 
It now recursively traverses its arguments.  This isn't great from an efficiency
perspective, but we need it to be able to simplify instruction pointers computed
from relative jumps (which involve some sign extensions and shifts).
This commit is contained in:
Tristan Ravitch 2017-11-07 13:44:41 -08:00
parent 0b43f5672e
commit a4cbd3a9d0
1 changed files with 30 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
macaw-ppc/src/Data/Macaw/PPC/Simplify.hs
View File

@ -1,11 +1,13 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Macaw.PPC.Simplify ( simplifyValue ) where
import Data.Bits
import Data.Parameterized.Classes
import Data.Parameterized.NatRepr ( NatRepr )
import Data.Parameterized.NatRepr ( NatRepr, toSigned, toUnsigned )
import Data.Macaw.CFG
import qualified Data.Macaw.Memory as MM
import Data.Macaw.Types ( BVType, BoolType )
@ -31,59 +33,62 @@ simplifyApp :: forall arch ids tp
-> Maybe (Value arch ids tp)
simplifyApp a =
case a of
AndApp (BoolValue True) r -> Just r
AndApp l (BoolValue True) -> Just l
AndApp f@(BoolValue False) _ -> Just f
AndApp _ f@(BoolValue False) -> Just f
OrApp t@(BoolValue True) _ -> Just t
OrApp _ t@(BoolValue True) -> Just t
OrApp (BoolValue False) r -> Just r
OrApp l (BoolValue False) -> Just l
Mux _ (BoolValue c) t e -> if c then Just t else Just e
AndApp (simplifyValue -> Just (BoolValue True)) r -> Just r
AndApp l (simplifyValue -> Just (BoolValue True)) -> Just l
AndApp f@(simplifyValue -> Just (BoolValue False)) _ -> Just f
AndApp _ f@(simplifyValue -> Just (BoolValue False)) -> Just f
OrApp t@(simplifyValue -> Just (BoolValue True)) _ -> Just t
OrApp _ t@(simplifyValue -> Just (BoolValue True)) -> Just t
OrApp (simplifyValue -> Just (BoolValue False)) r -> Just r
OrApp l (simplifyValue -> Just (BoolValue False)) -> Just l
Mux _ (simplifyValue -> Just (BoolValue c)) t e -> if c then Just t else Just e
BVAnd _ l r
| Just Refl <- testEquality l r -> Just l
BVAnd sz l r -> binopbv (.&.) sz l r
BVOr sz l r -> binopbv (.|.) sz l r
BVShl sz l r -> binopbv (\l' r' -> shiftL l' (fromIntegral r')) sz l r
BVAdd _ l (BVValue _ 0) -> Just l
BVAdd _ (BVValue _ 0) r -> Just r
BVAdd rep l@(BVValue {}) r@(RelocatableValue {}) ->
BVAdd _ l (simplifyValue -> Just (BVValue _ 0)) -> Just l
BVAdd _ (simplifyValue -> Just (BVValue _ 0)) r -> Just r
BVAdd rep (simplifyValue -> Just l@(BVValue {})) (simplifyValue -> Just r@(RelocatableValue {})) ->
simplifyApp (BVAdd rep r l)
BVAdd rep (RelocatableValue _ addr) (BVValue _ off) ->
BVAdd rep (simplifyValue -> Just (RelocatableValue _ addr)) (simplifyValue -> Just (BVValue _ off)) ->
Just (RelocatableValue rep (MM.incAddr off addr))
BVAdd sz l r -> binopbv (+) sz l r
BVMul _ l (BVValue _ 1) -> Just l
BVMul _ (BVValue _ 1) r -> Just r
BVMul rep _ (BVValue _ 0) -> Just (BVValue rep 0)
BVMul rep (BVValue _ 0) _ -> Just (BVValue rep 0)
BVMul _ l (simplifyValue -> Just (BVValue _ 1)) -> Just l
BVMul _ (simplifyValue -> Just (BVValue _ 1)) r -> Just r
BVMul rep _ (simplifyValue -> Just (BVValue _ 0)) -> Just (BVValue rep 0)
BVMul rep (simplifyValue -> Just (BVValue _ 0)) _ -> Just (BVValue rep 0)
BVMul rep l r -> binopbv (*) rep l r
UExt (BVValue _ n) sz -> Just (mkLit sz n)
Trunc (BVValue _ x) sz -> Just (mkLit sz x)
SExt (simplifyValue -> Just (BVValue u n)) sz -> Just (BVValue sz (toUnsigned sz (toSigned u n)))
UExt (simplifyValue -> Just (BVValue _ n)) sz -> Just (mkLit sz n)
Trunc (simplifyValue -> Just (BVValue _ x)) sz -> Just (mkLit sz x)
Eq l r -> boolop (==) l r
BVComplement sz x -> unop complement sz x
_ -> Nothing
where
unop :: (tp ~ BVType n)
unop :: forall n . (tp ~ BVType n)
=> (Integer -> Integer)
-> NatRepr n
-> Value arch ids tp
-> Maybe (Value arch ids tp)
unop f sz (BVValue _ l) = Just (mkLit sz (f l))
unop f sz (simplifyValue -> Just (BVValue _ l)) = Just (mkLit sz (f l))
unop _ _ _ = Nothing
boolop :: (Integer -> Integer -> Bool)
-> Value arch ids utp
-> Value arch ids utp
-> Maybe (Value arch ids BoolType)
boolop f (BVValue _ l) (BVValue _ r) = Just (BoolValue (f l r))
boolop f (simplifyValue -> Just (BVValue _ l)) (simplifyValue -> Just (BVValue _ r)) =
Just (BoolValue (f l r))
boolop _ _ _ = Nothing
binopbv :: (tp ~ BVType n)
binopbv :: forall n . (tp ~ BVType n)
=> (Integer -> Integer -> Integer)
-> NatRepr n
-> Value arch ids tp
-> Value arch ids tp
-> Maybe (Value arch ids tp)
binopbv f sz (BVValue _ l) (BVValue _ r) = Just (mkLit sz (f l r))
binopbv f sz (simplifyValue -> Just (BVValue _ l)) (simplifyValue -> Just (BVValue _ r)) =
Just (mkLit sz (f l r))
binopbv _ _ _ _ = Nothing