crucible-llvm-0.7: src/Lang/Crucible/LLVM/Utils.hs

{-# 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 b f x = if b then pure x else f 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 sym w w' x
  | Just Refl <- testEquality w w' = return x
  | Just LeqProof <- testLeq (incNat w) w' = bvSext sym w' x
  | Just LeqProof <- testLeq (incNat w') w = bvTrunc sym w' x
  | otherwise = panic "sextendBVTo"
                  [ "Impossible widths!"
                  , show w
                  , show w'
                  ]