{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Utils
-- Description      : Miscellaneous utility functions.
-- Copyright        : (c) Galois, Inc 2021
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
module Lang.Crucible.LLVM.Utils
  ( applyUnless
  , sextendBVTo
  ) where

import What4.Interface

import Lang.Crucible.Backend
import Lang.Crucible.Panic (panic)

-- | If the first argument is 'False', apply the second argument to the third.
-- Otherwise, simply return the third argument.
applyUnless :: Applicative f => Bool -> (a -> f a) -> a -> f a
applyUnless :: forall (f :: Type -> Type) a.
Applicative f =>
Bool -> (a -> f a) -> a -> f a
applyUnless Bool
b a -> f a
f a
x = if Bool
b then a -> f a
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
x else a -> f a
f a
x

-- | Convert a 'SymBV' value of width @w@ to width @w'@, performing sign
-- extension or truncation as needed.
sextendBVTo :: (1 <= w, 1 <= w', IsSymInterface sym)
            => sym
            -> NatRepr w
            -> NatRepr w'
            -> SymExpr sym (BaseBVType w)
            -> IO (SymExpr sym (BaseBVType w'))
sextendBVTo :: forall (w :: Natural) (w' :: Natural) sym.
(1 <= w, 1 <= w', IsSymInterface sym) =>
sym
-> NatRepr w
-> NatRepr w'
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w'))
sextendBVTo sym
sym NatRepr w
w NatRepr w'
w' SymExpr sym (BaseBVType w)
x
  | Just w :~: w'
Refl <- NatRepr w -> NatRepr w' -> Maybe (w :~: w')
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 NatRepr w
w NatRepr w'
w' = SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym (BaseBVType w)
x
  | Just LeqProof (w + 1) w'
LeqProof <- NatRepr (w + 1) -> NatRepr w' -> Maybe (LeqProof (w + 1) w')
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr w -> NatRepr (w + 1)
forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr w
w) NatRepr w'
w' = sym
-> NatRepr w'
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w'))
forall (u :: Natural) (r :: Natural).
(1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr w'
w' SymExpr sym (BaseBVType w)
x
  | Just LeqProof (w' + 1) w
LeqProof <- NatRepr (w' + 1) -> NatRepr w -> Maybe (LeqProof (w' + 1) w)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr w' -> NatRepr (w' + 1)
forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr w'
w') NatRepr w
w = sym
-> NatRepr w'
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w'))
forall (r :: Natural) (w :: Natural).
(1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w'
w' SymExpr sym (BaseBVType w)
x
  | Bool
otherwise = String -> [String] -> IO (SymExpr sym ('BaseBVType w'))
forall a. HasCallStack => String -> [String] -> a
panic String
"sextendBVTo"
                  [ String
"Impossible widths!"
                  , NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
w
                  , NatRepr w' -> String
forall a. Show a => a -> String
show NatRepr w'
w'
                  ]