{-|
Copyright  : (c) Galois, Inc 2017-2019
Maintainer : jhendrix@galois.com

This provides a rewriter for simplifying blocks by rewriting value
computations and performing other rearrangement and adjustments.

The main entry point is calling 'runRewriter' with a constructed
'RewriteContext' to control the rewrite operation and a Rewriter monad
computation that rewrites the statements for a particular block.

Note that while the common case is a single block, the Branch TermStmt
that can be part of a block may refer to other Blocks (by ID) and
therefore the rewriting operation may need to actually modify multiple
blocks or even add new blocks for new Branch TermStmt targets.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Macaw.CFG.Rewriter
  ( -- * Basic types
    RewriteContext
  , mkRewriteContext
  , Rewriter
  , runRewriter
  , rewriteStmt
  , rewriteValue
  , rewriteApp
  , evalRewrittenArchFn
  , appendRewrittenArchStmt
  ) where

import           Control.Lens
import           Control.Monad (when)
import           Control.Monad.ST
import           Control.Monad.State.Strict (StateT(..), gets)
import           Control.Monad.Trans (MonadTrans(..))
import           Data.BinarySymbols
import           Data.Bits
import           Data.List (find)
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.TraversableFC
import           Data.STRef

import           Data.Macaw.CFG.App
import           Data.Macaw.CFG.Core
import           Data.Macaw.Memory
import qualified Data.Macaw.Panic as P
import           Data.Macaw.Types
import           Data.Macaw.CFG.Block (TermStmt)

-- | Information needed for rewriting.
data RewriteContext arch s src tgt
   = RewriteContext { forall arch s src tgt.
RewriteContext arch s src tgt -> NonceGenerator (ST s) tgt
rwctxNonceGen  :: !(NonceGenerator (ST s) tgt)
                      -- ^ Generator for making new nonces in the target ST monad
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> forall (tp :: Type).
   ArchFn arch (Value arch src) tp
   -> Rewriter arch s src tgt (Value arch tgt tp)
rwctxArchFn
                      :: !(forall tp
                            .  ArchFn arch (Value arch src) tp
                            -> Rewriter arch s src tgt (Value arch tgt tp))
                      -- ^ Rewriter for architecture-specific functions
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()
rwctxArchStmt
                      :: !(ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
                      -- ^ Rewriter for architecture-specific statements
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> TermStmt arch tgt -> Rewriter arch s src tgt (TermStmt arch tgt)
rwctxTermStmt
                      :: (TermStmt arch tgt ->
                          Rewriter arch s src tgt (TermStmt arch tgt))
                         -- ^ Rewriter for block terminal statements
                         -- for block at specified address to make any
                         -- additional adjustments beyond normal
                         -- discovery.
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> forall a. (RegisterInfo (ArchReg arch) => a) -> a
rwctxConstraints
                      :: !(forall a . (RegisterInfo (ArchReg arch) => a) -> a)
                      -- ^ Constraints needed during rewriting.
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> Map SectionIndex (ArchSegmentOff arch)
rwctxSectionAddrMap
                      :: !(Map SectionIndex (ArchSegmentOff arch))
                      -- ^ Map from section indices to the address they are loaded at
                      -- if any.
                      -- This is used to replace section references with their address.
                    , forall arch s src tgt.
RewriteContext arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
rwctxCache :: !(STRef s (MapF (AssignId src) (Value arch tgt)))
                      -- ^ A reference to a  map from source assignment
                      -- identifiers to the updated value.
                      --
                      -- N.B. When using the rewriter, the user should
                      -- process each statement sequentially so that
                      -- every assign id is mapped to a value.  If some
                      -- of the assignments can be eliminated this
                      -- should be done via a dead code elimination step
                      -- rather than during rewriting.
                    }

mkRewriteContext :: RegisterInfo (ArchReg arch)
                 => NonceGenerator (ST s) tgt
                 -> (forall tp
                     .  ArchFn arch (Value arch src) tp
                     -> Rewriter arch s src tgt (Value arch tgt tp))
                 -> (ArchStmt arch (Value arch src)
                     -> Rewriter arch s src tgt ())
                 -> (TermStmt arch tgt ->
                     Rewriter arch s src tgt (TermStmt arch tgt))
                    -- ^ Optional internal terminal statement
                    -- rewriter; e.g. use is for block jump targets
                    -- discovered outside normal pattern-matching in
                    -- Discovery.hs.
                 -> Map SectionIndex (ArchSegmentOff arch)
                    -- ^ Map from loaded section indices to their address.
                 -> ST s (RewriteContext arch s src tgt)
mkRewriteContext :: forall arch s tgt src.
RegisterInfo (ArchReg arch) =>
NonceGenerator (ST s) tgt
-> (forall (tp :: Type).
    ArchFn arch (Value arch src) tp
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> (TermStmt arch tgt
    -> Rewriter arch s src tgt (TermStmt arch tgt))
-> Map SectionIndex (ArchSegmentOff arch)
-> ST s (RewriteContext arch s src tgt)
mkRewriteContext NonceGenerator (ST s) tgt
nonceGen forall (tp :: Type).
ArchFn arch (Value arch src) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
archFn ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()
archStmt TermStmt arch tgt -> Rewriter arch s src tgt (TermStmt arch tgt)
termStmt Map SectionIndex (ArchSegmentOff arch)
secAddrMap = do
  ref <- MapF (AssignId src) (Value arch tgt)
-> ST s (STRef s (MapF (AssignId src) (Value arch tgt)))
forall a s. a -> ST s (STRef s a)
newSTRef MapF (AssignId src) (Value arch tgt)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
  pure $! RewriteContext { rwctxNonceGen = nonceGen
                         , rwctxArchFn = archFn
                         , rwctxArchStmt = archStmt
                         , rwctxTermStmt = termStmt
                         , rwctxConstraints = \RegisterInfo (ArchReg arch) => a
a -> a
RegisterInfo (ArchReg arch) => a
a
                         , rwctxSectionAddrMap = secAddrMap
                         , rwctxCache = ref
                         }

-- | State used by rewriter for tracking states
data RewriteState arch s src tgt
   = RewriteState { -- | Access to the context for the rewriter
                    forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext        :: !(RewriteContext arch s src tgt)
                  , forall arch s src tgt.
RewriteState arch s src tgt -> [Stmt arch tgt]
_rwRevStmts      :: ![Stmt arch tgt]
                  }

-- | A list of statements in the current block in reverse order.
rwRevStmts :: Simple Lens (RewriteState arch s src tgt) [Stmt arch tgt]
rwRevStmts :: forall arch s src tgt (f :: Type -> Type).
Functor f =>
([Stmt arch tgt] -> f [Stmt arch tgt])
-> RewriteState arch s src tgt -> f (RewriteState arch s src tgt)
rwRevStmts = (RewriteState arch s src tgt -> [Stmt arch tgt])
-> (RewriteState arch s src tgt
    -> [Stmt arch tgt] -> RewriteState arch s src tgt)
-> Lens
     (RewriteState arch s src tgt)
     (RewriteState arch s src tgt)
     [Stmt arch tgt]
     [Stmt arch tgt]
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens RewriteState arch s src tgt -> [Stmt arch tgt]
forall arch s src tgt.
RewriteState arch s src tgt -> [Stmt arch tgt]
_rwRevStmts (\RewriteState arch s src tgt
s [Stmt arch tgt]
v -> RewriteState arch s src tgt
s { _rwRevStmts = v })

-- | Monad for constant propagation within a block.
newtype Rewriter arch s src tgt a = Rewriter { forall arch s src tgt a.
Rewriter arch s src tgt a
-> StateT (RewriteState arch s src tgt) (ST s) a
unRewriter :: StateT (RewriteState arch s src tgt) (ST s) a }
  deriving ((forall a b.
 (a -> b) -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b)
-> (forall a b.
    a -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a)
-> Functor (Rewriter arch s src tgt)
forall a b.
a -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
forall a b.
(a -> b) -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
forall arch s src tgt a b.
a -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
forall arch s src tgt a b.
(a -> b) -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall arch s src tgt a b.
(a -> b) -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
fmap :: forall a b.
(a -> b) -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
$c<$ :: forall arch s src tgt a b.
a -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
<$ :: forall a b.
a -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
Functor, Functor (Rewriter arch s src tgt)
Functor (Rewriter arch s src tgt) =>
(forall a. a -> Rewriter arch s src tgt a)
-> (forall a b.
    Rewriter arch s src tgt (a -> b)
    -> Rewriter arch s src tgt a -> Rewriter arch s src tgt b)
-> (forall a b c.
    (a -> b -> c)
    -> Rewriter arch s src tgt a
    -> Rewriter arch s src tgt b
    -> Rewriter arch s src tgt c)
-> (forall a b.
    Rewriter arch s src tgt a
    -> Rewriter arch s src tgt b -> Rewriter arch s src tgt b)
-> (forall a b.
    Rewriter arch s src tgt a
    -> Rewriter arch s src tgt b -> Rewriter arch s src tgt a)
-> Applicative (Rewriter arch s src tgt)
forall a. a -> Rewriter arch s src tgt a
forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
forall a b.
Rewriter arch s src tgt (a -> b)
-> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
forall a b c.
(a -> b -> c)
-> Rewriter arch s src tgt a
-> Rewriter arch s src tgt b
-> Rewriter arch s src tgt c
forall arch s src tgt. Functor (Rewriter arch s src tgt)
forall arch s src tgt a. a -> Rewriter arch s src tgt a
forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
forall arch s src tgt a b.
Rewriter arch s src tgt (a -> b)
-> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
forall arch s src tgt a b c.
(a -> b -> c)
-> Rewriter arch s src tgt a
-> Rewriter arch s src tgt b
-> Rewriter arch s src tgt c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall arch s src tgt a. a -> Rewriter arch s src tgt a
pure :: forall a. a -> Rewriter arch s src tgt a
$c<*> :: forall arch s src tgt a b.
Rewriter arch s src tgt (a -> b)
-> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
<*> :: forall a b.
Rewriter arch s src tgt (a -> b)
-> Rewriter arch s src tgt a -> Rewriter arch s src tgt b
$cliftA2 :: forall arch s src tgt a b c.
(a -> b -> c)
-> Rewriter arch s src tgt a
-> Rewriter arch s src tgt b
-> Rewriter arch s src tgt c
liftA2 :: forall a b c.
(a -> b -> c)
-> Rewriter arch s src tgt a
-> Rewriter arch s src tgt b
-> Rewriter arch s src tgt c
$c*> :: forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
*> :: forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
$c<* :: forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
<* :: forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt a
Applicative, Applicative (Rewriter arch s src tgt)
Applicative (Rewriter arch s src tgt) =>
(forall a b.
 Rewriter arch s src tgt a
 -> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b)
-> (forall a b.
    Rewriter arch s src tgt a
    -> Rewriter arch s src tgt b -> Rewriter arch s src tgt b)
-> (forall a. a -> Rewriter arch s src tgt a)
-> Monad (Rewriter arch s src tgt)
forall a. a -> Rewriter arch s src tgt a
forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall arch s src tgt. Applicative (Rewriter arch s src tgt)
forall arch s src tgt a. a -> Rewriter arch s src tgt a
forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
forall arch s src tgt a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall arch s src tgt a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
>>= :: forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
$c>> :: forall arch s src tgt a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
>> :: forall a b.
Rewriter arch s src tgt a
-> Rewriter arch s src tgt b -> Rewriter arch s src tgt b
$creturn :: forall arch s src tgt a. a -> Rewriter arch s src tgt a
return :: forall a. a -> Rewriter arch s src tgt a
Monad)

-- | Run the rewriter with the given context
-- and collect the statements.
runRewriter :: RewriteContext arch s src tgt
            -> Rewriter arch s src tgt (TermStmt arch tgt)
            -> ST s ( RewriteContext arch s src tgt
                    , [Stmt arch tgt]
                    , (TermStmt arch tgt))
runRewriter :: forall arch s src tgt.
RewriteContext arch s src tgt
-> Rewriter arch s src tgt (TermStmt arch tgt)
-> ST
     s
     (RewriteContext arch s src tgt, [Stmt arch tgt], TermStmt arch tgt)
runRewriter RewriteContext arch s src tgt
ctx Rewriter arch s src tgt (TermStmt arch tgt)
m = do
  let s :: RewriteState arch s src tgt
s = RewriteState { rwContext :: RewriteContext arch s src tgt
rwContext = RewriteContext arch s src tgt
ctx
                       , _rwRevStmts :: [Stmt arch tgt]
_rwRevStmts = []
                       }
      m' :: Rewriter arch s src tgt (TermStmt arch tgt)
m' = RewriteContext arch s src tgt
-> TermStmt arch tgt -> Rewriter arch s src tgt (TermStmt arch tgt)
forall arch s src tgt.
RewriteContext arch s src tgt
-> TermStmt arch tgt -> Rewriter arch s src tgt (TermStmt arch tgt)
rwctxTermStmt RewriteContext arch s src tgt
ctx (TermStmt arch tgt -> Rewriter arch s src tgt (TermStmt arch tgt))
-> Rewriter arch s src tgt (TermStmt arch tgt)
-> Rewriter arch s src tgt (TermStmt arch tgt)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewriter arch s src tgt (TermStmt arch tgt)
m
  (r, s') <- StateT (RewriteState arch s src tgt) (ST s) (TermStmt arch tgt)
-> RewriteState arch s src tgt
-> ST s (TermStmt arch tgt, RewriteState arch s src tgt)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (Rewriter arch s src tgt (TermStmt arch tgt)
-> StateT (RewriteState arch s src tgt) (ST s) (TermStmt arch tgt)
forall arch s src tgt a.
Rewriter arch s src tgt a
-> StateT (RewriteState arch s src tgt) (ST s) a
unRewriter Rewriter arch s src tgt (TermStmt arch tgt)
m') RewriteState arch s src tgt
s
  pure (rwContext s', reverse (_rwRevStmts s'), r)

-- | Add a statement to the list
appendRewrittenStmt :: Stmt arch tgt -> Rewriter arch s src tgt ()
appendRewrittenStmt :: forall arch tgt s src. Stmt arch tgt -> Rewriter arch s src tgt ()
appendRewrittenStmt Stmt arch tgt
stmt = StateT (RewriteState arch s src tgt) (ST s) ()
-> Rewriter arch s src tgt ()
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT (RewriteState arch s src tgt) (ST s) ()
 -> Rewriter arch s src tgt ())
-> StateT (RewriteState arch s src tgt) (ST s) ()
-> Rewriter arch s src tgt ()
forall a b. (a -> b) -> a -> b
$ do
  stmts <- Getting
  [Stmt arch tgt] (RewriteState arch s src tgt) [Stmt arch tgt]
-> StateT (RewriteState arch s src tgt) (ST s) [Stmt arch tgt]
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  [Stmt arch tgt] (RewriteState arch s src tgt) [Stmt arch tgt]
forall arch s src tgt (f :: Type -> Type).
Functor f =>
([Stmt arch tgt] -> f [Stmt arch tgt])
-> RewriteState arch s src tgt -> f (RewriteState arch s src tgt)
rwRevStmts
  let stmts' = Stmt arch tgt
stmt Stmt arch tgt -> [Stmt arch tgt] -> [Stmt arch tgt]
forall a. a -> [a] -> [a]
: [Stmt arch tgt]
stmts
  seq stmt $ seq stmts' $ do
    rwRevStmts .= stmts'

-- | Add a architecture-specific statement to the list
appendRewrittenArchStmt :: ArchStmt arch (Value arch tgt) -> Rewriter arch s src tgt ()
appendRewrittenArchStmt :: forall arch tgt s src.
ArchStmt arch (Value arch tgt) -> Rewriter arch s src tgt ()
appendRewrittenArchStmt = Stmt arch tgt -> Rewriter arch s src tgt ()
forall arch tgt s src. Stmt arch tgt -> Rewriter arch s src tgt ()
appendRewrittenStmt (Stmt arch tgt -> Rewriter arch s src tgt ())
-> (ArchStmt arch (Value arch tgt) -> Stmt arch tgt)
-> ArchStmt arch (Value arch tgt)
-> Rewriter arch s src tgt ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArchStmt arch (Value arch tgt) -> Stmt arch tgt
forall arch ids. ArchStmt arch (Value arch ids) -> Stmt arch ids
ExecArchStmt

-- | Add an assignment statement that evaluates the right hand side and return the resulting value.
evalRewrittenRhs :: AssignRhs arch (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs :: forall arch tgt (tp :: Type) s src.
AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs AssignRhs arch (Value arch tgt) tp
rhs = StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ do
  gen <- (RewriteState arch s src tgt -> NonceGenerator (ST s) tgt)
-> StateT
     (RewriteState arch s src tgt) (ST s) (NonceGenerator (ST s) tgt)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((RewriteState arch s src tgt -> NonceGenerator (ST s) tgt)
 -> StateT
      (RewriteState arch s src tgt) (ST s) (NonceGenerator (ST s) tgt))
-> (RewriteState arch s src tgt -> NonceGenerator (ST s) tgt)
-> StateT
     (RewriteState arch s src tgt) (ST s) (NonceGenerator (ST s) tgt)
forall a b. (a -> b) -> a -> b
$ RewriteContext arch s src tgt -> NonceGenerator (ST s) tgt
forall arch s src tgt.
RewriteContext arch s src tgt -> NonceGenerator (ST s) tgt
rwctxNonceGen (RewriteContext arch s src tgt -> NonceGenerator (ST s) tgt)
-> (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> RewriteState arch s src tgt
-> NonceGenerator (ST s) tgt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
  aid <- lift $ AssignId <$> freshNonce gen
  let a = AssignId tgt tp
-> AssignRhs arch (Value arch tgt) tp -> Assignment arch tgt tp
forall arch ids (tp :: Type).
AssignId ids tp
-> AssignRhs arch (Value arch ids) tp -> Assignment arch ids tp
Assignment AssignId tgt tp
aid AssignRhs arch (Value arch tgt) tp
rhs
  unRewriter $ appendRewrittenStmt $ AssignStmt a
  pure $! AssignedValue a

-- | Add an assignment statement that evaluates the architecture function.
evalRewrittenArchFn :: HasRepr (ArchFn arch (Value arch tgt)) TypeRepr
                    => ArchFn arch (Value arch tgt) tp
                    -> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenArchFn :: forall arch tgt (tp :: Type) s src.
HasRepr (ArchFn arch (Value arch tgt)) TypeRepr =>
ArchFn arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenArchFn ArchFn arch (Value arch tgt) tp
f = AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs (ArchFn arch (Value arch tgt) tp
-> TypeRepr tp -> AssignRhs arch (Value arch tgt) tp
forall arch (f :: Type -> Type) (tp :: Type).
ArchFn arch f tp -> TypeRepr tp -> AssignRhs arch f tp
EvalArchFn ArchFn arch (Value arch tgt) tp
f (ArchFn arch (Value arch tgt) tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). ArchFn arch (Value arch tgt) tp -> TypeRepr tp
typeRepr ArchFn arch (Value arch tgt) tp
f))

-- | Add a binding from the source assign id to the value.
addBinding :: AssignId src tp -> Value arch tgt tp -> Rewriter arch s src tgt ()
addBinding :: forall src (tp :: Type) arch tgt s.
AssignId src tp -> Value arch tgt tp -> Rewriter arch s src tgt ()
addBinding AssignId src tp
srcId Value arch tgt tp
val = StateT (RewriteState arch s src tgt) (ST s) ()
-> Rewriter arch s src tgt ()
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT (RewriteState arch s src tgt) (ST s) ()
 -> Rewriter arch s src tgt ())
-> StateT (RewriteState arch s src tgt) (ST s) ()
-> Rewriter arch s src tgt ()
forall a b. (a -> b) -> a -> b
$ do
  ref <- (RewriteState arch s src tgt
 -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (STRef s (MapF (AssignId src) (Value arch tgt)))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((RewriteState arch s src tgt
  -> STRef s (MapF (AssignId src) (Value arch tgt)))
 -> StateT
      (RewriteState arch s src tgt)
      (ST s)
      (STRef s (MapF (AssignId src) (Value arch tgt))))
-> (RewriteState arch s src tgt
    -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (STRef s (MapF (AssignId src) (Value arch tgt)))
forall a b. (a -> b) -> a -> b
$ RewriteContext arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
forall arch s src tgt.
RewriteContext arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
rwctxCache (RewriteContext arch s src tgt
 -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> RewriteState arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
  lift $ do
    m <- readSTRef ref
    when (MapF.member srcId m) $ do
      P.panic P.Base "addBinding"
        ["Assignment " ++ show srcId ++ " is already bound."]
    writeSTRef ref $! MapF.insert srcId val m

-- | Return true if values are identical
identValue :: TestEquality (ArchReg arch) => Value arch tgt tp -> Value arch tgt tp -> Bool
identValue :: forall arch tgt (tp :: Type).
TestEquality (ArchReg arch) =>
Value arch tgt tp -> Value arch tgt tp -> Bool
identValue (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
identValue (RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
x) (RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
y) = MemAddr (ArchAddrWidth arch)
x MemAddr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr (ArchAddrWidth arch)
y
identValue (AssignedValue Assignment arch tgt tp
x) (AssignedValue Assignment arch tgt tp
y) = Assignment arch tgt tp -> AssignId tgt tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch tgt tp
x AssignId tgt tp -> AssignId tgt tp -> Bool
forall a. Eq a => a -> a -> Bool
== Assignment arch tgt tp -> AssignId tgt tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch tgt tp
y
identValue (Initial ArchReg arch tp
x) (Initial ArchReg arch tp
y) | Just tp :~: tp
Refl <- ArchReg arch tp -> ArchReg arch tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
ArchReg arch a -> ArchReg arch b -> Maybe (a :~: b)
testEquality ArchReg arch tp
x ArchReg arch tp
y = Bool
True
identValue Value arch tgt tp
_ Value arch tgt tp
_ = Bool
False

boolLitValue :: Bool -> Value arch ids BoolType
boolLitValue :: forall arch ids. Bool -> Value arch ids BoolType
boolLitValue = Bool -> Value arch ids BoolType
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue

rewriteApp :: App (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp :: forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp App (Value arch tgt) tp
app = do
  ctx <- StateT
  (RewriteState arch s src tgt)
  (ST s)
  (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT
   (RewriteState arch s src tgt)
   (ST s)
   (RewriteContext arch s src tgt)
 -> Rewriter arch s src tgt (RewriteContext arch s src tgt))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall a b. (a -> b) -> a -> b
$ (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
  rwctxConstraints ctx $ do
   case app of

    Trunc (BVValue NatRepr n
_ Integer
x) NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer -> Value arch tgt tp) -> Integer -> Value arch tgt tp
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x

    Trunc (Value arch tgt (BVType m)
-> Maybe (App (Value arch tgt) (BVType m))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (Mux TypeRepr (BVType m)
_ Value arch tgt BoolType
c t :: Value arch tgt (BVType m)
t@BVValue{} f :: Value arch tgt (BVType m)
f@BVValue{})) NatRepr n
w -> do
      t' <- App (Value arch tgt) ('BVType n)
-> Rewriter arch s src tgt (Value arch tgt ('BVType n))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr n -> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (m :: Natural) (f :: Type -> Type).
(1 <= n, (n + 1) <= m) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
Trunc Value arch tgt (BVType m)
t NatRepr n
w)
      f' <- rewriteApp (Trunc f w)
      rewriteApp $ Mux (BVTypeRepr w) c t' f'

    Trunc (Value arch tgt (BVType m)
-> Maybe (App (Value arch tgt) (BVType m))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
v NatRepr n
_)) NatRepr n
w -> case NatRepr n -> NatRepr m -> NatComparison n m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr n
w (Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
v) of
      NatLT NatRepr y
_ -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt (BVType m)
-> NatRepr n -> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (m :: Natural) (f :: Type -> Type).
(1 <= n, (n + 1) <= m) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
Trunc Value arch tgt (BVType m)
v NatRepr n
w
      NatComparison n m
NatEQ   -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt (BVType m)
v
      NatGT NatRepr y
_ -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt (BVType m)
-> NatRepr n -> App (Value arch tgt) ('BVType n)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
UExt Value arch tgt (BVType m)
v NatRepr n
w
    Trunc (Value arch tgt (BVType m)
-> Maybe (App (Value arch tgt) (BVType m))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
v NatRepr n
_)) NatRepr n
w -> case NatRepr n -> NatRepr m -> NatComparison n m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr n
w (Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
v) of
      NatLT NatRepr y
_ -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt (BVType m)
-> NatRepr n -> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (m :: Natural) (f :: Type -> Type).
(1 <= n, (n + 1) <= m) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
Trunc Value arch tgt (BVType m)
v NatRepr n
w
      NatComparison n m
NatEQ   -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt (BVType m)
v
      NatGT NatRepr y
_ -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt (BVType m)
-> NatRepr n -> App (Value arch tgt) ('BVType n)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
v NatRepr n
w

    SExt (BVValue NatRepr n
u Integer
x) NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer -> Value arch tgt tp) -> Integer -> Value arch tgt tp
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
u Integer
x
    UExt (BVValue NatRepr n
_ Integer
x) NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
x

    Mux TypeRepr tp
_ (BoolValue Bool
c) Value arch tgt tp
t Value arch tgt tp
f -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ if Bool
c then Value arch tgt tp
t else Value arch tgt tp
f
    Mux TypeRepr tp
tp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (NotApp Value arch tgt BoolType
c)) Value arch tgt tp
t Value arch tgt tp
f -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (TypeRepr tp
-> Value arch tgt BoolType
-> Value arch tgt tp
-> Value arch tgt tp
-> App (Value arch tgt) tp
forall (tp :: Type) (f :: Type -> Type).
TypeRepr tp -> f BoolType -> f tp -> f tp -> App f tp
Mux TypeRepr tp
tp Value arch tgt BoolType
c Value arch tgt tp
f Value arch tgt tp
t)
    -- ite c T y = (~c | T) & (c | y)
    --           = c | y
    Mux TypeRepr tp
_ Value arch tgt BoolType
c (BoolValue Bool
True) Value arch tgt tp
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType
-> Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type).
f BoolType -> f BoolType -> App f BoolType
OrApp Value arch tgt BoolType
c Value arch tgt tp
Value arch tgt BoolType
y)
    -- ite c F y = (~c | F) & (c | y)
    --           = ~c & y
    Mux TypeRepr tp
BoolTypeRepr Value arch tgt BoolType
c (BoolValue Bool
False) Value arch tgt tp
y -> do
      cn <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt BoolType
c)
      rewriteApp (AndApp cn y)
    -- ite c x T = (~c | x) & (c | T)
    --           = ~c | x
    Mux TypeRepr tp
BoolTypeRepr Value arch tgt BoolType
c Value arch tgt tp
x (BoolValue Bool
True) -> do
      cn <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt BoolType
c)
      rewriteApp (OrApp cn x)
    -- ite c x F = (~c | x) & (c | F)
    --           = c & x
    Mux TypeRepr tp
BoolTypeRepr Value arch tgt BoolType
c Value arch tgt tp
x (BoolValue Bool
False) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType
-> Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type).
f BoolType -> f BoolType -> App f BoolType
AndApp Value arch tgt BoolType
c Value arch tgt tp
Value arch tgt BoolType
x)

    AndApp (BoolValue Bool
xc) Value arch tgt BoolType
y -> do
      if Bool
xc then
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
y
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
False)
    AndApp Value arch tgt BoolType
x (BoolValue Bool
yc) ->
      if Bool
yc then
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
x
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
False)
    -- x < y && x <= y   =   x < y
    AndApp   (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLe Value arch tgt (BVType n)
x  Value arch tgt (BVType n)
y ))
           v :: Value arch tgt BoolType
v@(Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLt Value arch tgt (BVType n)
x' Value arch tgt (BVType n)
y'))
      | Just n :~: n
Refl <- NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x) (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x')
      , (Value arch tgt (BVType n)
x,Value arch tgt (BVType n)
y) (Value arch tgt (BVType n), Value arch tgt (BVType n))
-> (Value arch tgt (BVType n), Value arch tgt (BVType n)) -> Bool
forall a. Eq a => a -> a -> Bool
== (Value arch tgt (BVType n)
Value arch tgt (BVType n)
x',Value arch tgt (BVType n)
Value arch tgt (BVType n)
y')
      -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
v
    AndApp v :: Value arch tgt BoolType
v@(Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLt Value arch tgt (BVType n)
x' Value arch tgt (BVType n)
y'))
             (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLe Value arch tgt (BVType n)
x  Value arch tgt (BVType n)
y ))
      | Just n :~: n
Refl <- NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x) (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x')
      , (Value arch tgt (BVType n)
x,Value arch tgt (BVType n)
y) (Value arch tgt (BVType n), Value arch tgt (BVType n))
-> (Value arch tgt (BVType n), Value arch tgt (BVType n)) -> Bool
forall a. Eq a => a -> a -> Bool
== (Value arch tgt (BVType n)
Value arch tgt (BVType n)
x',Value arch tgt (BVType n)
Value arch tgt (BVType n)
y')
      -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
v
    AndApp   (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLe Value arch tgt (BVType n)
x  Value arch tgt (BVType n)
y ))
           v :: Value arch tgt BoolType
v@(Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLt Value arch tgt (BVType n)
x' Value arch tgt (BVType n)
y'))
      | Just n :~: n
Refl <- NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x) (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x')
      , (Value arch tgt (BVType n)
x,Value arch tgt (BVType n)
y) (Value arch tgt (BVType n), Value arch tgt (BVType n))
-> (Value arch tgt (BVType n), Value arch tgt (BVType n)) -> Bool
forall a. Eq a => a -> a -> Bool
== (Value arch tgt (BVType n)
Value arch tgt (BVType n)
x',Value arch tgt (BVType n)
Value arch tgt (BVType n)
y')
      -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
v
    AndApp v :: Value arch tgt BoolType
v@(Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLt Value arch tgt (BVType n)
x' Value arch tgt (BVType n)
y'))
             (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLe Value arch tgt (BVType n)
x  Value arch tgt (BVType n)
y ))
      | Just n :~: n
Refl <- NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x) (Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x')
      , (Value arch tgt (BVType n)
x,Value arch tgt (BVType n)
y) (Value arch tgt (BVType n), Value arch tgt (BVType n))
-> (Value arch tgt (BVType n), Value arch tgt (BVType n)) -> Bool
forall a. Eq a => a -> a -> Bool
== (Value arch tgt (BVType n)
Value arch tgt (BVType n)
x',Value arch tgt (BVType n)
Value arch tgt (BVType n)
y')
      -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
v

    OrApp (BoolValue Bool
xc) Value arch tgt BoolType
y -> do
      if Bool
xc then
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
True)
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
y
    OrApp Value arch tgt BoolType
x y :: Value arch tgt BoolType
y@BoolValue{} -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType
-> Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type).
f BoolType -> f BoolType -> App f BoolType
OrApp Value arch tgt BoolType
y Value arch tgt BoolType
x)

    NotApp (BoolValue Bool
b) ->
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool -> Bool
not Bool
b)
    NotApp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (NotApp Value arch tgt BoolType
c)) ->
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Value arch tgt tp
Value arch tgt BoolType
c
    NotApp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLe Value arch tgt (BVType n)
x Value arch tgt (BVType n)
y)) ->
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType n)
y Value arch tgt (BVType n)
x)
    NotApp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVUnsignedLt Value arch tgt (BVType n)
x Value arch tgt (BVType n)
y)) ->
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType n)
y Value arch tgt (BVType n)
x)
    NotApp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLe Value arch tgt (BVType n)
x Value arch tgt (BVType n)
y)) ->
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLt Value arch tgt (BVType n)
y Value arch tgt (BVType n)
x)
    NotApp (Value arch tgt BoolType -> Maybe (App (Value arch tgt) BoolType)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSignedLt Value arch tgt (BVType n)
x Value arch tgt (BVType n)
y)) ->
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLe Value arch tgt (BVType n)
y Value arch tgt (BVType n)
x)

    XorApp (BoolValue Bool
b) Value arch tgt BoolType
x ->
      if Bool
b then
        App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt BoolType
x)
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
x
    XorApp Value arch tgt BoolType
x (BoolValue Bool
b) ->
      if Bool
b then
        App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt BoolType
x)
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt BoolType
x

    BVAdd NatRepr n
_ Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
0) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x
    BVAdd NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)))
    -- If first argument is constant and second is not, then commute.
    BVAdd NatRepr n
w (BVValue NatRepr n
_ Integer
x) Value arch tgt ('BVType n)
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
y (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
x)
    -- (x + yc) + zc -> x + (yc + zc)
    BVAdd NatRepr n
w (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVAdd NatRepr n
_ Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
yc))) (BVValue NatRepr n
_ Integer
zc) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
yc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
zc)))
    -- (x - yc) + zc -> x + (zc - yc)
    BVAdd NatRepr n
w (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSub NatRepr n
_ Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
yc))) (BVValue NatRepr n
_ Integer
zc) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
zc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
yc)))
    -- (xc - y) + zc => (xc + zc) - y
    BVAdd NatRepr n
w (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSub NatRepr n
_ (BVValue NatRepr n
_ Integer
xc) Value arch tgt ('BVType n)
y)) (BVValue NatRepr n
_ Integer
zc) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVSub NatRepr n
w (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
xc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
zc))) Value arch tgt ('BVType n)
Value arch tgt ('BVType n)
y
    -- Increment address by a constant.
    BVAdd NatRepr n
_ (RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
r MemAddr (RegAddrWidth (ArchReg arch))
a) (BVValue NatRepr n
_ Integer
c) ->
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ AddrWidthRepr (RegAddrWidth (ArchReg arch))
-> MemAddr (RegAddrWidth (ArchReg arch)) -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch ids tp
RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
r (Integer -> MemAddr n -> MemAddr n
forall (w :: Natural).
MemWidth w =>
Integer -> MemAddr w -> MemAddr w
incAddr Integer
c MemAddr n
MemAddr (RegAddrWidth (ArchReg arch))
a)

    -- addr a + (c - addr b) => c + (addr a - addr b)
    BVAdd NatRepr n
w (RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
_ MemAddr (RegAddrWidth (ArchReg arch))
a) (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSub NatRepr n
_ Value arch tgt ('BVType n)
c (RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
_ MemAddr (RegAddrWidth (ArchReg arch))
b)))
      | Just Integer
d <- MemAddr n -> MemAddr n -> Maybe Integer
forall (w :: Natural).
MemWidth w =>
MemAddr w -> MemAddr w -> Maybe Integer
diffAddr MemAddr n
MemAddr (RegAddrWidth (ArchReg arch))
a MemAddr n
MemAddr (RegAddrWidth (ArchReg arch))
b ->
        App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
Value arch tgt ('BVType n)
c (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
d))

    -- x - yc = x + (negate yc)
    BVSub NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
yc) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer -> Integer
forall a. Num a => a -> a
negate Integer
yc))))

    BVUnsignedLe (BVValue NatRepr n
w Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool -> Value arch tgt BoolType)
-> Bool -> Value arch tgt BoolType
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
y
    BVUnsignedLe (BVValue NatRepr n
w Integer
x) Value arch tgt (BVType n)
_ | NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
minUnsigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    BVUnsignedLe Value arch tgt (BVType n)
_ (BVValue NatRepr n
w Integer
y) | NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    -- in uext(x) <= uext(y) we can eliminate one or both uext's.
    -- same for sext's, even with unsigned comparisons!
    -- uext(x) <= yc = true    if yc >= 2^width(x)-1
    -- uext(x) <= yc = x <= yc if yc <  2^width(x)-1
    -- similar shortcuts exist for the other inequalities
    BVUnsignedLe (BVValue NatRepr n
_ Integer
x) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr m
wShort
        then App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
x) Value arch tgt (BVType m)
y)
        else Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVUnsignedLe (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
_ Integer
y) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
      if Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr m
wShort
        then App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
y))
        else Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    BVUnsignedLe (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
UExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
UExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')
    BVUnsignedLe (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')

    BVUnsignedLt (BVValue NatRepr n
w Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool -> Value arch tgt BoolType)
-> Bool -> Value arch tgt BoolType
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
y
    BVUnsignedLt (BVValue NatRepr n
w Integer
x) Value arch tgt (BVType n)
_ | NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVUnsignedLt Value arch tgt (BVType n)
_ (BVValue NatRepr n
w Integer
x) | NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
minUnsigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVUnsignedLt (BVValue NatRepr n
_ Integer
x) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr m
wShort
        then App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
x) Value arch tgt (BVType m)
y)
        else Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVUnsignedLt (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
_ Integer
y) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
      if Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr m
wShort
        then App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
y))
        else Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    BVUnsignedLt (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
UExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
UExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')
    BVUnsignedLt (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')

    BVSignedLe (BVValue NatRepr n
w Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool -> Value arch tgt BoolType)
-> Bool -> Value arch tgt BoolType
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y
    BVSignedLe (BVValue NatRepr n
w Integer
x) Value arch tgt (BVType n)
_ | NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    BVSignedLe Value arch tgt (BVType n)
_ (BVValue NatRepr n
w Integer
y) | NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
    BVSignedLe (BVValue NatRepr n
w Integer
x) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
          xv :: Integer
xv = NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x
      if Integer
xv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr m
wShort
        then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
        else if Integer
xv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr m
wShort
          then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
          else App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLe (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
x) Value arch tgt (BVType m)
y)
    BVSignedLe (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
w Integer
y) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          yv :: Integer
yv = NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y
      if Integer
yv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr m
wShort
        then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
        else if Integer
yv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr m
wShort
          then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
          else App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLe Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
y))
    BVSignedLe (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLe Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')
    -- for signed comparisons, uext(x) <= uext(y) is not necessarily equivalent
    -- to either x <= uext(y) or uext(x) <= y, so no rewrite for that!

    BVSignedLt (BVValue NatRepr n
w Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool -> Value arch tgt BoolType)
-> Bool -> Value arch tgt BoolType
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y
    BVSignedLt (BVValue NatRepr n
w Integer
x) Value arch tgt (BVType n)
_ | NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVSignedLt Value arch tgt (BVType n)
_ (BVValue NatRepr n
w Integer
y) | NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
    BVSignedLt (BVValue NatRepr n
w Integer
x) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
          xv :: Integer
xv = NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x
      if Integer
xv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr m
wShort
        then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
        else if Integer
xv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr m
wShort
          then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
          else App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLt (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
x) Value arch tgt (BVType m)
y)
    BVSignedLt (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
w Integer
y) -> do
      let wShort :: NatRepr m
wShort = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          yv :: Integer
yv = NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
y
      if Integer
yv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned NatRepr m
wShort
        then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False
        else if Integer
yv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr m -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr m
wShort
          then Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
True
          else App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLt Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
wShort Integer
y))
    BVSignedLt (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
x NatRepr n
_)) (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (SExt Value arch tgt (BVType m)
y NatRepr n
_)) -> do
      let wx :: NatRepr m
wx = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
          wy :: NatRepr m
wy = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
y
      case NatRepr m -> NatRepr m -> NatComparison m m
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
wx NatRepr m
wy of
        NatLT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
x NatRepr m
wy) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
x' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x' Value arch tgt (BVType m)
y)
        NatComparison m m
NatEQ   -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
Value arch tgt (BVType m)
y)
        NatGT NatRepr y
_ -> App (Value arch tgt) (BVType m)
-> Rewriter arch s src tgt (Value arch tgt (BVType m))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> NatRepr m -> App (Value arch tgt) (BVType m)
forall (m :: Natural) (n :: Natural) (f :: Type -> Type).
(1 <= m, (m + 1) <= n, 1 <= n) =>
f (BVType m) -> NatRepr n -> App f ('BVType n)
SExt Value arch tgt (BVType m)
y NatRepr m
wx) Rewriter arch s src tgt (Value arch tgt (BVType m))
-> (Value arch tgt (BVType m)
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b.
Rewriter arch s src tgt a
-> (a -> Rewriter arch s src tgt b) -> Rewriter arch s src tgt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value arch tgt (BVType m)
y' -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVUnsignedLt Value arch tgt (BVType m)
x Value arch tgt (BVType m)
y')

    BVTestBit (BVValue NatRepr n
xw Integer
xc) (BVValue NatRepr n
_ Integer
ic) | Integer
ic Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
xw) (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int))  -> do
      let v :: Bool
v = Integer
xc Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
ic
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
v
    -- If we test the greatest bit turn this to a signed equality
    BVTestBit Value arch tgt (BVType n)
x (BVValue NatRepr n
_ Integer
ic)
      | NatRepr n
w <- Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x
      , Integer
ic Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVSignedLt Value arch tgt (BVType n)
x (NatRepr n -> Integer -> Value arch tgt (BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
0))
      | NatRepr n
w <- Value arch tgt (BVType n) -> NatRepr n
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType n)
x
      , Integer
ic Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
_ Integer
ic) -> do
      let xw :: NatRepr m
xw = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
      if Integer
ic Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr m
xw then
        App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
xw Integer
ic))
       else
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
False)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVAnd NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y)) i :: Value arch tgt (BVType n)
i@BVValue{} -> do
      xb <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x Value arch tgt (BVType n)
Value arch tgt ('BVType n)
i)
      yb <- rewriteApp (BVTestBit y i)
      rewriteApp (AndApp xb yb)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVOr NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y)) i :: Value arch tgt (BVType n)
i@BVValue{} -> do
      xb <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x Value arch tgt (BVType n)
Value arch tgt ('BVType n)
i)
      yb <- rewriteApp (BVTestBit y i)
      rewriteApp (OrApp xb yb)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVXor NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y)) Value arch tgt (BVType n)
i -> do
      xb <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x Value arch tgt (BVType n)
Value arch tgt ('BVType n)
i)
      yb <- rewriteApp (BVTestBit y i)
      rewriteApp (XorApp xb yb)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVComplement NatRepr n
_ Value arch tgt ('BVType n)
x)) Value arch tgt (BVType n)
i -> do
      xb <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x Value arch tgt (BVType n)
Value arch tgt ('BVType n)
i)
      rewriteApp (NotApp xb)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (Mux TypeRepr (BVType n)
_ Value arch tgt BoolType
c Value arch tgt (BVType n)
x Value arch tgt (BVType n)
y)) Value arch tgt (BVType n)
i -> do
      xb <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType n)
-> Value arch tgt (BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt (BVType n)
x Value arch tgt (BVType n)
i)
      yb <- rewriteApp (BVTestBit y i)
      rewriteApp (Mux BoolTypeRepr c xb yb)

    -- (x >> j) testBit i ~> x testBit (i+j)
    -- (x << j) testBit i ~> x testBit (i-j)
    -- plus a couple special cases for when the tested bit falls outside the shifted value
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVShr NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
j))) (BVValue NatRepr n
_ Integer
i)
      | Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w ->
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i)))
      | Bool
otherwise -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False)
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSar NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
j))) (BVValue NatRepr n
_ Integer
i)
      | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i) (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))))
    BVTestBit (Value arch tgt (BVType n)
-> Maybe (App (Value arch tgt) (BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVShl NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
j))) (BVValue NatRepr n
_ Integer
i)
      | Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
f (BVType n) -> f (BVType n) -> App f BoolType
BVTestBit Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j)))
      | Bool
otherwise -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue Bool
False)

    BVComplement NatRepr n
w (BVValue NatRepr n
_ Integer
x) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
x)))

    BVAnd NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
y))
    -- Ensure constant with and is second argument.
    BVAnd NatRepr n
w x :: Value arch tgt ('BVType n)
x@BVValue{} Value arch tgt ('BVType n)
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAnd NatRepr n
w Value arch tgt ('BVType n)
y Value arch tgt ('BVType n)
x)
    BVAnd NatRepr n
_ Value arch tgt ('BVType n)
_ y :: Value arch tgt ('BVType n)
y@(BVValue NatRepr n
_ Integer
0) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
y
    BVAnd NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
yc) | Integer
yc Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
w -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x
    BVAnd NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y | Value arch tgt ('BVType n)
x Value arch tgt ('BVType n) -> Value arch tgt ('BVType n) -> Bool
forall a. Eq a => a -> a -> Bool
== Value arch tgt ('BVType n)
y -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x

    BVOr NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y))
    BVOr NatRepr n
w x :: Value arch tgt ('BVType n)
x@BVValue{} Value arch tgt ('BVType n)
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVOr NatRepr n
w Value arch tgt ('BVType n)
y Value arch tgt ('BVType n)
x)
    BVOr NatRepr n
_ Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
0) -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x
    BVOr NatRepr n
w Value arch tgt ('BVType n)
_ y :: Value arch tgt ('BVType n)
y@(BVValue NatRepr n
_ Integer
yc) | Integer
yc Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
w -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
y
    BVOr NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y | Value arch tgt ('BVType n)
x Value arch tgt ('BVType n) -> Value arch tgt ('BVType n) -> Bool
forall a. Eq a => a -> a -> Bool
== Value arch tgt ('BVType n)
y -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x

    BVXor NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
y))
    BVXor NatRepr n
w x :: Value arch tgt ('BVType n)
x@BVValue{} Value arch tgt ('BVType n)
y -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVXor NatRepr n
w Value arch tgt ('BVType n)
y Value arch tgt ('BVType n)
x)
    BVXor NatRepr n
_ Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
0) -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
x
    BVXor NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
yc) | Integer
yc Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
w -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n) -> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> App f (BVType n)
BVComplement NatRepr n
w Value arch tgt ('BVType n)
x)
    -- x `xor` y -> 0
    BVXor NatRepr n
w Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y | Value arch tgt ('BVType n) -> Value arch tgt ('BVType n) -> Bool
forall arch tgt (tp :: Type).
TestEquality (ArchReg arch) =>
Value arch tgt tp -> Value arch tgt tp -> Bool
identValue Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
0)


    BVShl NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) -> do
      let s :: Integer
s = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w)
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
s)))
    BVShr NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) -> do
      let s :: Integer
s = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w)
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
s)))
    BVSar NatRepr n
w (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) -> do
      let s :: Integer
s = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
y (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w)
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
w Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
s)))

    BVShl NatRepr n
_ Value arch tgt ('BVType n)
v (BVValue NatRepr n
_ Integer
0) -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
v
    BVShr NatRepr n
_ Value arch tgt ('BVType n)
v (BVValue NatRepr n
_ Integer
0) -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
v
    BVSar NatRepr n
_ Value arch tgt ('BVType n)
v (BVValue NatRepr n
_ Integer
0) -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
Value arch tgt ('BVType n)
v

    BVShl NatRepr n
w Value arch tgt ('BVType n)
_ (BVValue NatRepr n
_ Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w ->
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
0)
    BVShr NatRepr n
w Value arch tgt ('BVType n)
_ (BVValue NatRepr n
_ Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w ->
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
0)

    PopCount NatRepr n
w (BVValue NatRepr n
_ Integer
x) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer -> Value arch tgt tp) -> Integer -> Value arch tgt tp
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x
    Bsr NatRepr n
w (BVValue NatRepr n
_ Integer
x) -> do
      let i :: Integer
i = Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer) -> Maybe Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> [Integer] -> Maybe Integer
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find
                (\Integer
j -> NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                [Integer
0 .. NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w]
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (Integer -> Value arch tgt tp) -> Integer -> Value arch tgt tp
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i

    Eq (BoolValue Bool
x) (BoolValue Bool
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y)

    Eq (BoolValue Bool
True) Value arch tgt tp1
y -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Value arch tgt tp
Value arch tgt tp1
y
    Eq (BoolValue Bool
False) Value arch tgt tp1
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt tp1
Value arch tgt BoolType
y

    Eq Value arch tgt tp1
x (BoolValue Bool
True) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Value arch tgt tp
Value arch tgt tp1
x
    Eq Value arch tgt tp1
x (BoolValue Bool
False) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ Value arch tgt BoolType -> App (Value arch tgt) BoolType
forall (f :: Type -> Type). f BoolType -> App f BoolType
NotApp Value arch tgt tp1
Value arch tgt BoolType
x

    Eq (BVValue NatRepr n
_ Integer
x) (BVValue NatRepr n
_ Integer
y) -> do
      Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! Bool -> Value arch tgt BoolType
forall arch ids. Bool -> Value arch ids BoolType
boolLitValue (Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y)

    -- Move constant to right hand side.
    Eq x :: Value arch tgt tp1
x@BVValue{} Value arch tgt tp1
y -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt tp1
-> Value arch tgt tp1 -> App (Value arch tgt) BoolType
forall (f :: Type -> Type) (tp1 :: Type).
f tp1 -> f tp1 -> App f BoolType
Eq Value arch tgt tp1
y Value arch tgt tp1
x)

    Eq (Value arch tgt tp1 -> Maybe (App (Value arch tgt) tp1)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (Mux TypeRepr tp1
_ Value arch tgt BoolType
c t :: Value arch tgt tp1
t@BVValue{} f :: Value arch tgt tp1
f@BVValue{})) z :: Value arch tgt tp1
z@BVValue{} -> do
      t' <- App (Value arch tgt) BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt tp1
-> Value arch tgt tp1 -> App (Value arch tgt) BoolType
forall (f :: Type -> Type) (tp1 :: Type).
f tp1 -> f tp1 -> App f BoolType
Eq Value arch tgt tp1
t Value arch tgt tp1
z)
      f' <- rewriteApp (Eq f z)
      rewriteApp $ Mux BoolTypeRepr c t' f'

    -- x + o = y ~> x = (y - o)
    Eq (Value arch tgt tp1 -> Maybe (App (Value arch tgt) tp1)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVAdd NatRepr n
w Value arch tgt ('BVType n)
x (BVValue NatRepr n
_ Integer
o))) (BVValue NatRepr n
_ Integer
yc) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (f :: Type -> Type) (tp1 :: Type).
f tp1 -> f tp1 -> App f BoolType
Eq Value arch tgt ('BVType n)
x (NatRepr n -> Integer -> Value arch tgt ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (Integer
yc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
o))))

    Eq (Value arch tgt tp1 -> Maybe (App (Value arch tgt) tp1)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (BVSub NatRepr n
_ Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y)) (BVValue NatRepr n
_ Integer
0) -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n) -> App (Value arch tgt) BoolType
forall (f :: Type -> Type) (tp1 :: Type).
f tp1 -> f tp1 -> App f BoolType
Eq Value arch tgt ('BVType n)
x Value arch tgt ('BVType n)
y)

    Eq (Value arch tgt tp1 -> Maybe (App (Value arch tgt) tp1)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (UExt Value arch tgt (BVType m)
x NatRepr n
_)) (BVValue NatRepr n
_ Integer
yc) -> do
      let u :: NatRepr m
u = Value arch tgt (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch tgt (BVType m)
x
      if Integer
yc Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr m -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr m
u then
        Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
False)
       else
        App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (Value arch tgt (BVType m)
-> Value arch tgt (BVType m) -> App (Value arch tgt) BoolType
forall (f :: Type -> Type) (tp1 :: Type).
f tp1 -> f tp1 -> App f BoolType
Eq Value arch tgt (BVType m)
x (NatRepr m -> Integer -> Value arch tgt (BVType m)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr m
u (NatRepr m -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr m
u Integer
yc)))

    -- no normal rewrites available, now try mhnf for enabling Discovery
    App (Value arch tgt) tp
_ -> App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteMhnf App (Value arch tgt) tp
app


-- | Performs rewrites for "Mux Head Normal Form", which attempts to
-- raise Mux operations upwards to make them more likely to appear as
-- the last statement in a Block.  This is needed because
-- parseFetchAndExecute in Discovery will attempt to recognize branch
-- statements by pattern matching the value of the IP register as a
-- Mux.
--
-- For example, the following:
--
--     r32 := Mux r31 (0x4 :: [64]) (0x28 :: [64])
--     r33 := Add r32 (0x100a3e50)
--     { ip => r33, ... }
--
-- should be rewritten to:
--
--     r34 := Mux r31 (0x100a3e54) (0x100a3e78)
--     { ip => r34, ... }
--
-- so that the Mux itself is the ip register's valueAsApp.  (Note that
-- the BVAdd of the two r32 branch values and the r33 second argument
-- are reduced to simple values by the rewriter here as well.
--
-- This rewrite is performed after other rewrites to increase the
-- chances of it raising the Mux past previously rewrite-simplified
-- statements, although it still recurses into the main rewriter.
rewriteMhnf :: App (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteMhnf :: forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteMhnf App (Value arch tgt) tp
app = do
  ctx <- StateT
  (RewriteState arch s src tgt)
  (ST s)
  (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT
   (RewriteState arch s src tgt)
   (ST s)
   (RewriteContext arch s src tgt)
 -> Rewriter arch s src tgt (RewriteContext arch s src tgt))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall a b. (a -> b) -> a -> b
$ (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
  rwctxConstraints ctx $ do
   case app of

     BVAdd NatRepr n
w (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (Mux TypeRepr ('BVType n)
p Value arch tgt BoolType
c Value arch tgt ('BVType n)
t Value arch tgt ('BVType n)
f)) v :: Value arch tgt ('BVType n)
v@(BVValue NatRepr n
_ Integer
_) -> do
       t' <- App (Value arch tgt) ('BVType n)
-> Rewriter arch s src tgt (Value arch tgt ('BVType n))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
t Value arch tgt ('BVType n)
v)
       f' <- rewriteApp (BVAdd w f v)
       rewriteApp $ Mux p c t' f'

     BVAdd NatRepr n
w (Value arch tgt ('BVType n)
-> Maybe (App (Value arch tgt) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp -> Just (Mux TypeRepr ('BVType n)
p Value arch tgt BoolType
c Value arch tgt ('BVType n)
t Value arch tgt ('BVType n)
f)) v :: Value arch tgt ('BVType n)
v@(RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
_ MemAddr (RegAddrWidth (ArchReg arch))
_) -> do
       t' <- App (Value arch tgt) ('BVType n)
-> Rewriter arch s src tgt (Value arch tgt ('BVType n))
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (NatRepr n
-> Value arch tgt ('BVType n)
-> Value arch tgt ('BVType n)
-> App (Value arch tgt) ('BVType n)
forall (n :: Natural) (f :: Type -> Type).
(1 <= n) =>
NatRepr n -> f (BVType n) -> f (BVType n) -> App f (BVType n)
BVAdd NatRepr n
w Value arch tgt ('BVType n)
t Value arch tgt ('BVType n)
v)
       f' <- rewriteApp (BVAdd w f v)
       rewriteApp $ Mux p c t' f'

     -- no more rewrites applicable, so return the final result
     App (Value arch tgt) tp
_ -> AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs (App (Value arch tgt) tp -> AssignRhs arch (Value arch tgt) tp
forall (f :: Type -> Type) (tp :: Type) arch.
App f tp -> AssignRhs arch f tp
EvalApp App (Value arch tgt) tp
app)


rewriteAssignRhs :: AssignRhs arch (Value arch src) tp
                 -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteAssignRhs :: forall arch src (tp :: Type) s tgt.
AssignRhs arch (Value arch src) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteAssignRhs AssignRhs arch (Value arch src) tp
rhs =
  case AssignRhs arch (Value arch src) tp
rhs of
    EvalApp App (Value arch src) tp
app -> do
      App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
App (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteApp (App (Value arch tgt) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter arch s src tgt (App (Value arch tgt) tp)
-> Rewriter arch s src tgt (Value arch tgt tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: Type).
 Value arch src x -> Rewriter arch s src tgt (Value arch tgt x))
-> forall (x :: Type).
   App (Value arch src) x
   -> Rewriter arch s src tgt (App (Value arch tgt) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type).
Applicative m =>
(forall (x :: Type). f x -> m (g x))
-> forall (x :: Type). App f x -> m (App g x)
traverseFC Value arch src x -> Rewriter arch s src tgt (Value arch tgt x)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall (x :: Type).
Value arch src x -> Rewriter arch s src tgt (Value arch tgt x)
rewriteValue App (Value arch src) tp
app
    SetUndefined TypeRepr tp
w -> AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs (TypeRepr tp -> AssignRhs arch (Value arch tgt) tp
forall (tp :: Type) arch (f :: Type -> Type).
TypeRepr tp -> AssignRhs arch f tp
SetUndefined TypeRepr tp
w)
    ReadMem Value arch src (BVType (ArchAddrWidth arch))
addr MemRepr tp
repr -> do
      tgtAddr <- Value arch src (BVType (ArchAddrWidth arch))
-> Rewriter
     arch s src tgt (Value arch tgt (BVType (ArchAddrWidth arch)))
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src (BVType (ArchAddrWidth arch))
addr
      evalRewrittenRhs (ReadMem tgtAddr repr)
    CondReadMem MemRepr tp
repr Value arch src BoolType
cond0 Value arch src (BVType (ArchAddrWidth arch))
addr0 Value arch src tp
def0 -> do
      cond <- Value arch src BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src BoolType
cond0
      addr <- rewriteValue addr0
      case () of
        ()
_ | BoolValue Bool
b <- Value arch tgt BoolType
cond ->
            if Bool
b then
              AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch tgt (tp :: Type) s src.
AssignRhs arch (Value arch tgt) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs (Value arch tgt (BVType (ArchAddrWidth arch))
-> MemRepr tp -> AssignRhs arch (Value arch tgt) tp
forall (f :: Type -> Type) arch (tp :: Type).
f (BVType (ArchAddrWidth arch))
-> MemRepr tp -> AssignRhs arch f tp
ReadMem Value arch tgt (BVType (ArchAddrWidth arch))
addr MemRepr tp
repr)
             else
              Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src tp
def0
        ()
_ -> do
          def  <- Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src tp
def0
          evalRewrittenRhs (CondReadMem repr cond addr def)
    EvalArchFn ArchFn arch (Value arch src) tp
archFn TypeRepr tp
_repr -> do
      f <- StateT
  (RewriteState arch s src tgt)
  (ST s)
  (ArchFn arch (Value arch src) tp
   -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter
     arch
     s
     src
     tgt
     (ArchFn arch (Value arch src) tp
      -> Rewriter arch s src tgt (Value arch tgt tp))
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT
   (RewriteState arch s src tgt)
   (ST s)
   (ArchFn arch (Value arch src) tp
    -> Rewriter arch s src tgt (Value arch tgt tp))
 -> Rewriter
      arch
      s
      src
      tgt
      (ArchFn arch (Value arch src) tp
       -> Rewriter arch s src tgt (Value arch tgt tp)))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchFn arch (Value arch src) tp
      -> Rewriter arch s src tgt (Value arch tgt tp))
-> Rewriter
     arch
     s
     src
     tgt
     (ArchFn arch (Value arch src) tp
      -> Rewriter arch s src tgt (Value arch tgt tp))
forall a b. (a -> b) -> a -> b
$ (RewriteState arch s src tgt
 -> ArchFn arch (Value arch src) tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchFn arch (Value arch src) tp
      -> Rewriter arch s src tgt (Value arch tgt tp))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((RewriteState arch s src tgt
  -> ArchFn arch (Value arch src) tp
  -> Rewriter arch s src tgt (Value arch tgt tp))
 -> StateT
      (RewriteState arch s src tgt)
      (ST s)
      (ArchFn arch (Value arch src) tp
       -> Rewriter arch s src tgt (Value arch tgt tp)))
-> (RewriteState arch s src tgt
    -> ArchFn arch (Value arch src) tp
    -> Rewriter arch s src tgt (Value arch tgt tp))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchFn arch (Value arch src) tp
      -> Rewriter arch s src tgt (Value arch tgt tp))
forall a b. (a -> b) -> a -> b
$ \RewriteState arch s src tgt
x -> RewriteContext arch s src tgt
-> forall (tp :: Type).
   ArchFn arch (Value arch src) tp
   -> Rewriter arch s src tgt (Value arch tgt tp)
forall arch s src tgt.
RewriteContext arch s src tgt
-> forall (tp :: Type).
   ArchFn arch (Value arch src) tp
   -> Rewriter arch s src tgt (Value arch tgt tp)
rwctxArchFn (RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext RewriteState arch s src tgt
x)
      f archFn

rewriteValue :: Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue :: forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src tp
v =
  case Value arch src tp
v of
    BoolValue Bool
b -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue Bool
b)
    BVValue NatRepr n
w Integer
i -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NatRepr n -> Integer -> Value arch tgt tp
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
i)
    RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
w MemAddr (ArchAddrWidth arch)
a -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch ids tp
RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
w MemAddr (ArchAddrWidth arch)
a)
    SymbolValue AddrWidthRepr (ArchAddrWidth arch)
repr SymbolIdentifier
sym -> do
      ctx <- StateT
  (RewriteState arch s src tgt)
  (ST s)
  (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT
   (RewriteState arch s src tgt)
   (ST s)
   (RewriteContext arch s src tgt)
 -> Rewriter arch s src tgt (RewriteContext arch s src tgt))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
-> Rewriter arch s src tgt (RewriteContext arch s src tgt)
forall a b. (a -> b) -> a -> b
$ (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (RewriteContext arch s src tgt)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
      rwctxConstraints ctx $ do
        let secIdxAddrMap = RewriteContext arch s src tgt
-> Map SectionIndex (ArchSegmentOff arch)
forall arch s src tgt.
RewriteContext arch s src tgt
-> Map SectionIndex (ArchSegmentOff arch)
rwctxSectionAddrMap RewriteContext arch s src tgt
ctx
        case sym of
          SectionIdentifier SectionIndex
secIdx
            | Just ArchSegmentOff arch
val <- SectionIndex
-> Map SectionIndex (ArchSegmentOff arch)
-> Maybe (ArchSegmentOff arch)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SectionIndex
secIdx Map SectionIndex (ArchSegmentOff arch)
secIdxAddrMap -> do
                Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch ids tp
RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
repr (ArchSegmentOff arch -> MemAddr (ArchAddrWidth arch)
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr ArchSegmentOff arch
val)
          SymbolIdentifier
_ -> do
            Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$! AddrWidthRepr (ArchAddrWidth arch)
-> SymbolIdentifier -> Value arch tgt tp
forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> SymbolIdentifier -> Value arch ids tp
SymbolValue AddrWidthRepr (ArchAddrWidth arch)
repr SymbolIdentifier
sym
    AssignedValue (Assignment AssignId src tp
aid AssignRhs arch (Value arch src) tp
_) -> StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. (a -> b) -> a -> b
$ do
      ref <- (RewriteState arch s src tgt
 -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (STRef s (MapF (AssignId src) (Value arch tgt)))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((RewriteState arch s src tgt
  -> STRef s (MapF (AssignId src) (Value arch tgt)))
 -> StateT
      (RewriteState arch s src tgt)
      (ST s)
      (STRef s (MapF (AssignId src) (Value arch tgt))))
-> (RewriteState arch s src tgt
    -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (STRef s (MapF (AssignId src) (Value arch tgt)))
forall a b. (a -> b) -> a -> b
$ RewriteContext arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
forall arch s src tgt.
RewriteContext arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
rwctxCache (RewriteContext arch s src tgt
 -> STRef s (MapF (AssignId src) (Value arch tgt)))
-> (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> RewriteState arch s src tgt
-> STRef s (MapF (AssignId src) (Value arch tgt))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
      srcMap <- lift $ readSTRef ref
      case MapF.lookup aid srcMap of
        Just Value arch tgt tp
tgtVal -> Value arch tgt tp
-> StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
forall a. a -> StateT (RewriteState arch s src tgt) (ST s) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Value arch tgt tp
tgtVal
        Maybe (Value arch tgt tp)
Nothing -> Component
-> String
-> [String]
-> StateT (RewriteState arch s src tgt) (ST s) (Value arch tgt tp)
forall a b.
(PanicComponent a, HasCallStack) =>
a -> String -> [String] -> b
P.panic Component
P.Base String
"rewriteValue"
                     [String
"Could not resolve source assignment " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AssignId src tp -> String
forall a. Show a => a -> String
show AssignId src tp
aid String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."]
    Initial ArchReg arch tp
r -> Value arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall a. a -> Rewriter arch s src tgt a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ArchReg arch tp -> Value arch tgt tp
forall arch (tp :: Type) ids. ArchReg arch tp -> Value arch ids tp
Initial ArchReg arch tp
r)

-- | Apply optimizations to a statement.
--
-- Since statements may be introduced/deleted during optimization,
-- this should add new statements to the list of target statements
-- rather than return the optimized statement.
rewriteStmt :: Stmt arch src -> Rewriter arch s src tgt ()
rewriteStmt :: forall arch src s tgt. Stmt arch src -> Rewriter arch s src tgt ()
rewriteStmt Stmt arch src
s =
  case Stmt arch src
s of
    AssignStmt Assignment arch src tp
a -> do
      v <- AssignRhs arch (Value arch src) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall arch src (tp :: Type) s tgt.
AssignRhs arch (Value arch src) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteAssignRhs (Assignment arch src tp -> AssignRhs arch (Value arch src) tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs Assignment arch src tp
a)
      addBinding (assignId a) v
    WriteMem ArchAddrValue arch src
addr MemRepr tp
repr Value arch src tp
val -> do
      tgtAddr <- ArchAddrValue arch src
-> Rewriter
     arch
     s
     src
     tgt
     (Value arch tgt (BVType (RegAddrWidth (ArchReg arch))))
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue ArchAddrValue arch src
addr
      tgtVal  <- rewriteValue val
      appendRewrittenStmt $ WriteMem tgtAddr repr tgtVal
    CondWriteMem Value arch src BoolType
cond ArchAddrValue arch src
addr MemRepr tp
repr Value arch src tp
val -> do
      tgtCond <- Value arch src BoolType
-> Rewriter arch s src tgt (Value arch tgt BoolType)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue Value arch src BoolType
cond
      tgtAddr <- rewriteValue addr
      tgtVal  <- rewriteValue val
      appendRewrittenStmt $ CondWriteMem tgtCond tgtAddr repr tgtVal
    Comment Text
cmt ->
      Stmt arch tgt -> Rewriter arch s src tgt ()
forall arch tgt s src. Stmt arch tgt -> Rewriter arch s src tgt ()
appendRewrittenStmt (Stmt arch tgt -> Rewriter arch s src tgt ())
-> Stmt arch tgt -> Rewriter arch s src tgt ()
forall a b. (a -> b) -> a -> b
$ Text -> Stmt arch tgt
forall arch ids. Text -> Stmt arch ids
Comment Text
cmt
    InstructionStart ArchAddrWord arch
off Text
mnem ->
      Stmt arch tgt -> Rewriter arch s src tgt ()
forall arch tgt s src. Stmt arch tgt -> Rewriter arch s src tgt ()
appendRewrittenStmt (Stmt arch tgt -> Rewriter arch s src tgt ())
-> Stmt arch tgt -> Rewriter arch s src tgt ()
forall a b. (a -> b) -> a -> b
$ ArchAddrWord arch -> Text -> Stmt arch tgt
forall arch ids. ArchAddrWord arch -> Text -> Stmt arch ids
InstructionStart ArchAddrWord arch
off Text
mnem
    ExecArchStmt ArchStmt arch (Value arch src)
astmt -> do
      f <- StateT
  (RewriteState arch s src tgt)
  (ST s)
  (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> Rewriter
     arch
     s
     src
     tgt
     (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
forall arch s src tgt a.
StateT (RewriteState arch s src tgt) (ST s) a
-> Rewriter arch s src tgt a
Rewriter (StateT
   (RewriteState arch s src tgt)
   (ST s)
   (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
 -> Rewriter
      arch
      s
      src
      tgt
      (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()))
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> Rewriter
     arch
     s
     src
     tgt
     (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
forall a b. (a -> b) -> a -> b
$ (RewriteState arch s src tgt
 -> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((RewriteState arch s src tgt
  -> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
 -> StateT
      (RewriteState arch s src tgt)
      (ST s)
      (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()))
-> (RewriteState arch s src tgt
    -> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> StateT
     (RewriteState arch s src tgt)
     (ST s)
     (ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
forall a b. (a -> b) -> a -> b
$ RewriteContext arch s src tgt
-> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()
forall arch s src tgt.
RewriteContext arch s src tgt
-> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ()
rwctxArchStmt (RewriteContext arch s src tgt
 -> ArchStmt arch (Value arch src) -> Rewriter arch s src tgt ())
-> (RewriteState arch s src tgt -> RewriteContext arch s src tgt)
-> RewriteState arch s src tgt
-> ArchStmt arch (Value arch src)
-> Rewriter arch s src tgt ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteState arch s src tgt -> RewriteContext arch s src tgt
forall arch s src tgt.
RewriteState arch s src tgt -> RewriteContext arch s src tgt
rwContext
      f astmt
    ArchState ArchMemAddr arch
addr MapF (ArchReg arch) (Value arch src)
updates -> do
      tgtUpdates <- (forall (tp :: Type).
 ArchReg arch tp
 -> Value arch src tp
 -> Rewriter arch s src tgt (Value arch tgt tp))
-> MapF (ArchReg arch) (Value arch src)
-> Rewriter arch s src tgt (MapF (ArchReg arch) (Value arch tgt))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey ((Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp))
-> ArchReg arch tp
-> Value arch src tp
-> Rewriter arch s src tgt (Value arch tgt tp)
forall a b. a -> b -> a
const Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
forall arch src (tp :: Type) s tgt.
Value arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteValue) MapF (ArchReg arch) (Value arch src)
updates
      appendRewrittenStmt $ ArchState addr tgtUpdates