mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-27 12:52:52 +03:00
Fix a bad exponential behavior bug
The recursive simplifier could exhibit exponential behavior in cases where a nested tree of irreducable terms were accumulated. The recursive calls quickly exploded execution times. The fix was to remove the recursive calls from the simplifier, but to incrementally simplify expressions to constants as they are added (via the addExpr function). This simplifies as much as the recursive case, but more efficiently. This change required exporting the simplifyApp function.
This commit is contained in:
Tristan Ravitch
parent
9ce1ffa0c5
commit
80145a0161
@ -75,7 +75,7 @@ import qualified SemMC.Architecture.PPC.Location as APPC
|
||||
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Arch ( PPCArchConstraints )
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue )
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue, simplifyApp )
|
||||
|
||||
-- GenResult
|
||||
|
||||
@ -263,9 +263,11 @@ addExpr :: (ArchConstraints ppc) => Expr ppc ids tp -> PPCGenerator ppc ids s (V
|
||||
addExpr expr = do
|
||||
case expr of
|
||||
ValueExpr val -> return val
|
||||
AppExpr app -> do
|
||||
assignment <- addAssignment (EvalApp app)
|
||||
return $ AssignedValue assignment
|
||||
AppExpr app
|
||||
| Just val <- simplifyApp app -> return val
|
||||
| otherwise -> do
|
||||
assignment <- addAssignment (EvalApp app)
|
||||
return $ AssignedValue assignment
|
||||
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
||||
@ -2,8 +2,10 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
module Data.Macaw.PPC.Simplify ( simplifyValue ) where
|
||||
module Data.Macaw.PPC.Simplify (
|
||||
simplifyValue,
|
||||
simplifyApp
|
||||
) where
|
||||
|
||||
import Data.Bits
|
||||
import Data.Parameterized.Classes
|
||||
@ -33,35 +35,35 @@ simplifyApp :: forall arch ids tp
|
||||
-> Maybe (Value arch ids tp)
|
||||
simplifyApp a =
|
||||
case a of
|
||||
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
|
||||
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
|
||||
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 (simplifyValue -> Just (BVValue _ 0)) -> Just l
|
||||
BVAdd _ (simplifyValue -> Just (BVValue _ 0)) r -> Just r
|
||||
BVAdd rep (simplifyValue -> Just l@(BVValue {})) (simplifyValue -> Just r@(RelocatableValue {})) ->
|
||||
BVAdd _ l (BVValue _ 0) -> Just l
|
||||
BVAdd _ (BVValue _ 0) r -> Just r
|
||||
BVAdd rep l@(BVValue {}) r@(RelocatableValue {}) ->
|
||||
simplifyApp (BVAdd rep r l)
|
||||
BVAdd rep (simplifyValue -> Just (RelocatableValue _ addr)) (simplifyValue -> Just (BVValue _ off)) ->
|
||||
BVAdd rep (RelocatableValue _ addr) (BVValue _ off) ->
|
||||
Just (RelocatableValue rep (MM.incAddr off addr))
|
||||
BVAdd sz l r -> binopbv (+) sz l r
|
||||
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 _ 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 rep l r -> binopbv (*) rep l r
|
||||
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)
|
||||
SExt (BVValue u n) sz -> Just (BVValue sz (toUnsigned sz (toSigned u n)))
|
||||
UExt (BVValue _ n) sz -> Just (mkLit sz n)
|
||||
Trunc (BVValue _ x) sz -> Just (mkLit sz x)
|
||||
|
||||
Eq l r -> boolop (==) l r
|
||||
BVComplement sz x -> unop complement sz x
|
||||
@ -72,14 +74,14 @@ simplifyApp a =
|
||||
-> NatRepr n
|
||||
-> Value arch ids tp
|
||||
-> Maybe (Value arch ids tp)
|
||||
unop f sz (simplifyValue -> Just (BVValue _ l)) = Just (mkLit sz (f l))
|
||||
unop f sz (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 (simplifyValue -> Just (BVValue _ l)) (simplifyValue -> Just (BVValue _ r)) =
|
||||
boolop f (BVValue _ l) (BVValue _ r) =
|
||||
Just (BoolValue (f l r))
|
||||
boolop _ _ _ = Nothing
|
||||
|
||||
@ -89,6 +91,6 @@ simplifyApp a =
|
||||
-> Value arch ids tp
|
||||
-> Value arch ids tp
|
||||
-> Maybe (Value arch ids tp)
|
||||
binopbv f sz (simplifyValue -> Just (BVValue _ l)) (simplifyValue -> Just (BVValue _ r)) =
|
||||
binopbv f sz (BVValue _ l) (BVValue _ r) =
|
||||
Just (mkLit sz (f l r))
|
||||
binopbv _ _ _ _ = Nothing
|
||||
|
||||
Loading…
Reference in New Issue
Block a user