------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Partial
-- Description      : Operations on partial values in the LLVM memory model
-- Copyright        : (c) Galois, Inc 2015-2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.MemModel.Partial
  ( PartLLVMVal(..)
  , partErr
  , attachSideCondition
  , attachMemoryError
  , assertSafe
  , MemoryError(..)
  , totalLLVMVal
  , bvConcat
  , consArray
  , appendArray
  , mkArray
  , mkStruct
  , HasLLVMAnn
  , LLVMAnnMap
  , BoolAnn(..)
  , annotateME
  , annotateUB
  , projectLLVM_bv

  , floatToBV
  , doubleToBV
  , fp80ToBV
  , bvToDouble
  , bvToFloat
  , bvToX86_FP80
  , selectHighBv
  , selectLowBv
  , arrayElt
  , fieldVal
  , muxLLVMVal

  , CexExplanation(..)
  , explainCex
  ) where

import           Prelude hiding (pred)

import           Control.Lens ((^.), view)
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Except (ExceptT, MonadError(..), runExceptT)
import           Control.Monad.State.Strict (StateT, get, put, runStateT)
import qualified Data.ByteString as BS
import qualified Data.Foldable as Fold
import           Data.Maybe (isJust)
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Vector (Vector)
import qualified Data.Vector as V
import           Numeric.Natural

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Classes (toOrdering, OrdF(..))
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Some (Some(..))

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Simulator.RegValue (RegValue'(..))
import           Lang.Crucible.LLVM.Bytes (Bytes)
import qualified Lang.Crucible.LLVM.Bytes as Bytes
import           Lang.Crucible.LLVM.MemModel.MemLog (memState)
import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack)
import           Lang.Crucible.LLVM.MemModel.Pointer ( pattern LLVMPointer, LLVMPtr )
import           Lang.Crucible.LLVM.MemModel.Type (StorageType(..), StorageTypeF(..), Field(..))
import qualified Lang.Crucible.LLVM.MemModel.Type as Type
import           Lang.Crucible.LLVM.MemModel.Value (LLVMVal(..))
import qualified Lang.Crucible.LLVM.MemModel.Value as Value
import           Lang.Crucible.LLVM.Errors
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
import           Lang.Crucible.LLVM.Errors.MemoryError (MemoryError(..), MemoryErrorReason(..), MemoryOp(..), memOpMem)
import           Lang.Crucible.Panic (panic)

import           What4.Expr
import           What4.Expr.BoolMap
import           What4.Expr.Builder
import           What4.Interface hiding (bvConcat, mkStruct, floatToBV, bvToFloat)
import qualified What4.Interface as W4I
import qualified What4.InterpretedFloatingPoint as W4IFP


newtype BoolAnn sym = BoolAnn (SymAnnotation sym BaseBoolType)

instance IsSymInterface sym => Eq (BoolAnn sym) where
  BoolAnn SymAnnotation sym BaseBoolType
x == :: BoolAnn sym -> BoolAnn sym -> Bool
== BoolAnn SymAnnotation sym BaseBoolType
y = Maybe (BaseBoolType :~: BaseBoolType) -> Bool
forall a. Maybe a -> Bool
isJust (SymAnnotation sym BaseBoolType
-> SymAnnotation sym BaseBoolType
-> Maybe (BaseBoolType :~: BaseBoolType)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
SymAnnotation sym a -> SymAnnotation sym b -> Maybe (a :~: b)
testEquality SymAnnotation sym BaseBoolType
x SymAnnotation sym BaseBoolType
y)
instance IsSymInterface sym => Ord (BoolAnn sym) where
  compare :: BoolAnn sym -> BoolAnn sym -> Ordering
compare (BoolAnn SymAnnotation sym BaseBoolType
x) (BoolAnn SymAnnotation sym BaseBoolType
y) = OrderingF BaseBoolType BaseBoolType -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF BaseBoolType BaseBoolType -> Ordering)
-> OrderingF BaseBoolType BaseBoolType -> Ordering
forall a b. (a -> b) -> a -> b
$ SymAnnotation sym BaseBoolType
-> SymAnnotation sym BaseBoolType
-> OrderingF BaseBoolType BaseBoolType
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
SymAnnotation sym x -> SymAnnotation sym y -> OrderingF x y
compareF SymAnnotation sym BaseBoolType
x SymAnnotation sym BaseBoolType
y

type LLVMAnnMap sym = Map (BoolAnn sym) (CallStack, BadBehavior sym)
type HasLLVMAnn sym = (?recordLLVMAnnotation :: CallStack -> BoolAnn sym -> BadBehavior sym -> IO ())

data CexExplanation sym (tp :: BaseType) where
  NoExplanation  :: CexExplanation sym tp
  DisjOfFailures :: [ (CallStack, BadBehavior sym) ] -> CexExplanation sym BaseBoolType

instance Semigroup (CexExplanation sym BaseBoolType) where
  CexExplanation sym BaseBoolType
NoExplanation <> :: CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
<> CexExplanation sym BaseBoolType
y = CexExplanation sym BaseBoolType
y
  CexExplanation sym BaseBoolType
x <> CexExplanation sym BaseBoolType
NoExplanation = CexExplanation sym BaseBoolType
x
  DisjOfFailures [(CallStack, BadBehavior sym)]
xs <> DisjOfFailures [(CallStack, BadBehavior sym)]
ys = [(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType
forall sym.
[(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType
DisjOfFailures ([(CallStack, BadBehavior sym)]
xs [(CallStack, BadBehavior sym)]
-> [(CallStack, BadBehavior sym)] -> [(CallStack, BadBehavior sym)]
forall a. [a] -> [a] -> [a]
++ [(CallStack, BadBehavior sym)]
ys)

explainCex :: forall t st fs sym.
  (IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
  sym ->
  LLVMAnnMap sym ->
  Maybe (GroundEvalFn t) ->
  IO (Pred sym -> IO (CexExplanation sym BaseBoolType))
explainCex :: forall t (st :: Type -> Type) fs sym.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym
-> LLVMAnnMap sym
-> Maybe (GroundEvalFn t)
-> IO (Pred sym -> IO (CexExplanation sym BaseBoolType))
explainCex sym
sym LLVMAnnMap sym
bbMap Maybe (GroundEvalFn t)
evalFn =
  do IdxCache t (CexExplanation sym)
posCache <- IO (IdxCache t (CexExplanation sym))
forall (m :: Type -> Type) t (f :: BaseType -> Type).
MonadIO m =>
m (IdxCache t f)
newIdxCache
     IdxCache t (CexExplanation sym)
negCache <- IO (IdxCache t (CexExplanation sym))
forall (m :: Type -> Type) t (f :: BaseType -> Type).
MonadIO m =>
m (IdxCache t f)
newIdxCache
     (Expr t BaseBoolType -> IO (CexExplanation sym BaseBoolType))
-> IO (Expr t BaseBoolType -> IO (CexExplanation sym BaseBoolType))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache)

  where
  evalPos, evalNeg ::
    IdxCache t (CexExplanation sym) ->
    IdxCache t (CexExplanation sym) ->
    Expr t BaseBoolType ->
    IO (CexExplanation sym BaseBoolType)

  evalPos :: IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e = IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
idxCacheEval IdxCache t (CexExplanation sym)
posCache Expr t BaseBoolType
e (IO (CexExplanation sym BaseBoolType)
 -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$
    case Expr t BaseBoolType
e of
      (Expr t BaseBoolType -> Maybe (NonceApp t (Expr t) BaseBoolType)
forall t (tp :: BaseType).
Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp -> Just (Annotation BaseTypeRepr BaseBoolType
BaseBoolRepr Nonce t BaseBoolType
annId Expr t BaseBoolType
e')) ->
        case BoolAnn sym -> LLVMAnnMap sym -> Maybe (CallStack, BadBehavior sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn Nonce t BaseBoolType
SymAnnotation sym BaseBoolType
annId) LLVMAnnMap sym
bbMap of
          Maybe (CallStack, BadBehavior sym)
Nothing -> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e'
          Just (CallStack
callStack, BadBehavior sym
bb) ->
            do BadBehavior sym
bb' <- case Maybe (GroundEvalFn t)
evalFn of
                        Just GroundEvalFn t
f  -> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> BadBehavior sym
-> IO (BadBehavior sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> BadBehavior sym
-> IO (BadBehavior sym)
concBadBehavior sym
sym (GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
f) BadBehavior sym
bb
                        Maybe (GroundEvalFn t)
Nothing -> BadBehavior sym -> IO (BadBehavior sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BadBehavior sym
bb
               CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType
forall sym.
[(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType
DisjOfFailures [ (CallStack
callStack, BadBehavior sym
bb') ])

      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr BaseBoolType
BaseBoolRepr Integer
_ Expr t BaseBoolType
c Expr t BaseBoolType
x Expr t BaseBoolType
y))
         | Just GroundEvalFn t
f <- Maybe (GroundEvalFn t)
evalFn ->
              do Bool
c' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
f Expr t BaseBoolType
c
                 if Bool
c' then
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x
                 else
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
y
         | Bool
otherwise ->
              CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
forall a. Semigroup a => a -> a -> a
(<>) (CexExplanation sym BaseBoolType
 -> CexExplanation sym BaseBoolType
 -> CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
-> IO
     (CexExplanation sym BaseBoolType
      -> CexExplanation sym BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x IO
  (CexExplanation sym BaseBoolType
   -> CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
y

      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred Expr t BaseBoolType
e')) -> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e'

      -- We expect at least one of the contained predicates to be false, so choose one
      -- and explain that failure
      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (ConjPred (BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
viewBoolMap -> BoolMapTerms NonEmpty (Expr t BaseBoolType, Polarity)
tms))) -> [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go (NonEmpty (Expr t BaseBoolType, Polarity)
-> [(Expr t BaseBoolType, Polarity)]
forall a. NonEmpty a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (Expr t BaseBoolType, Polarity)
tms)
        where
        go :: [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [] = CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
forall sym (tp :: BaseType). CexExplanation sym tp
NoExplanation
        go ((Expr t BaseBoolType
x,Polarity
Positive):[(Expr t BaseBoolType, Polarity)]
xs)
          | Just GroundEvalFn t
f <- Maybe (GroundEvalFn t)
evalFn =
              do Bool
x' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
f Expr t BaseBoolType
x
                 if Bool
x' then
                   [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
                 else
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x IO (CexExplanation sym BaseBoolType)
-> (CexExplanation sym BaseBoolType
    -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                     CexExplanation sym BaseBoolType
NoExplanation -> [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
                     CexExplanation sym BaseBoolType
ex -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
ex
          | Bool
otherwise =
              -- no counterexample in hand, assume this might be the problem
              IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x  IO (CexExplanation sym BaseBoolType)
-> (CexExplanation sym BaseBoolType
    -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                     CexExplanation sym BaseBoolType
NoExplanation -> [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
                     CexExplanation sym BaseBoolType
ex -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
ex

        go ((Expr t BaseBoolType
x,Polarity
Negative):[(Expr t BaseBoolType, Polarity)]
xs)
          | Just GroundEvalFn t
f <- Maybe (GroundEvalFn t)
evalFn =
              do Bool
x' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
f Expr t BaseBoolType
x
                 if Bool
x' then
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x IO (CexExplanation sym BaseBoolType)
-> (CexExplanation sym BaseBoolType
    -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                     CexExplanation sym BaseBoolType
NoExplanation -> [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
                     CexExplanation sym BaseBoolType
ex -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
ex
                 else
                   [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
           | Bool
otherwise =
              -- no counterexample in hand, assume this might be the problem
              IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x IO (CexExplanation sym BaseBoolType)
-> (CexExplanation sym BaseBoolType
    -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                CexExplanation sym BaseBoolType
NoExplanation -> [(Expr t BaseBoolType, Polarity)]
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs
                CexExplanation sym BaseBoolType
ex -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
ex

      Expr t BaseBoolType
_ -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
forall sym (tp :: BaseType). CexExplanation sym tp
NoExplanation

  evalNeg :: IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e = IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
idxCacheEval IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e (IO (CexExplanation sym BaseBoolType)
 -> IO (CexExplanation sym BaseBoolType))
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$
    case Expr t BaseBoolType
e of
      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr BaseBoolType
BaseBoolRepr Integer
_ Expr t BaseBoolType
c Expr t BaseBoolType
x Expr t BaseBoolType
y))
         | Just GroundEvalFn t
f <- Maybe (GroundEvalFn t)
evalFn ->
              do Bool
c' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
f Expr t BaseBoolType
c
                 if Bool
c' then
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x
                 else
                   IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
y
         | Bool
otherwise ->
              CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
forall a. Semigroup a => a -> a -> a
(<>) (CexExplanation sym BaseBoolType
 -> CexExplanation sym BaseBoolType
 -> CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
-> IO
     (CexExplanation sym BaseBoolType
      -> CexExplanation sym BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x IO
  (CexExplanation sym BaseBoolType
   -> CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
-> IO (CexExplanation sym BaseBoolType)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
y

      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred Expr t BaseBoolType
e')) -> IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
e'

      -- under negative polarity, we expect all members of the disjunction to be false,
      -- and we must construct an explanation for all of them
      (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (ConjPred (BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
viewBoolMap -> BoolMapTerms NonEmpty (Expr t BaseBoolType, Polarity)
tms))) -> [(Expr t BaseBoolType, Polarity)]
-> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
go (NonEmpty (Expr t BaseBoolType, Polarity)
-> [(Expr t BaseBoolType, Polarity)]
forall a. NonEmpty a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (Expr t BaseBoolType, Polarity)
tms) CexExplanation sym BaseBoolType
forall sym (tp :: BaseType). CexExplanation sym tp
NoExplanation
        where
        go :: [(Expr t BaseBoolType, Polarity)]
-> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
go [] CexExplanation sym BaseBoolType
es = CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
es
        go ((Expr t BaseBoolType
x,Polarity
Positive):[(Expr t BaseBoolType, Polarity)]
xs) CexExplanation sym BaseBoolType
es =
          do CexExplanation sym BaseBoolType
ex <- IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalNeg IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x
             [(Expr t BaseBoolType, Polarity)]
-> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs (CexExplanation sym BaseBoolType
ex CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
forall a. Semigroup a => a -> a -> a
<> CexExplanation sym BaseBoolType
es)
        go ((Expr t BaseBoolType
x,Polarity
Negative):[(Expr t BaseBoolType, Polarity)]
xs) CexExplanation sym BaseBoolType
es =
          do CexExplanation sym BaseBoolType
ex <- IdxCache t (CexExplanation sym)
-> IdxCache t (CexExplanation sym)
-> Expr t BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
evalPos IdxCache t (CexExplanation sym)
posCache IdxCache t (CexExplanation sym)
negCache Expr t BaseBoolType
x
             [(Expr t BaseBoolType, Polarity)]
-> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
go [(Expr t BaseBoolType, Polarity)]
xs (CexExplanation sym BaseBoolType
ex CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
-> CexExplanation sym BaseBoolType
forall a. Semigroup a => a -> a -> a
<> CexExplanation sym BaseBoolType
es)

      Expr t BaseBoolType
_ -> CexExplanation sym BaseBoolType
-> IO (CexExplanation sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CexExplanation sym BaseBoolType
forall sym (tp :: BaseType). CexExplanation sym tp
NoExplanation

annotateUB :: (IsSymInterface sym, HasLLVMAnn sym) =>
  sym ->
  CallStack ->
  UB.UndefinedBehavior (RegValue' sym) ->
  Pred sym ->
  IO (Pred sym)
annotateUB :: forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym CallStack
callStack UndefinedBehavior (RegValue' sym)
ub Pred sym
p =
  do (SymAnnotation sym BaseBoolType
n, Pred sym
p') <- sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
p
     HasLLVMAnn sym
CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()
?recordLLVMAnnotation CallStack
callStack (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
n) (UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub)
     Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
p'

memOpCallStack :: MemoryOp sym w -> CallStack
memOpCallStack :: forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack = MemState sym -> CallStack
forall sym. MemState sym -> CallStack
getCallStack (MemState sym -> CallStack)
-> (MemoryOp sym w -> MemState sym) -> MemoryOp sym w -> CallStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (MemState sym) (Mem sym) (MemState sym)
-> Mem sym -> MemState sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState (Mem sym -> MemState sym)
-> (MemoryOp sym w -> Mem sym) -> MemoryOp sym w -> MemState sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemoryOp sym w -> Mem sym
forall sym (w :: Nat). MemoryOp sym w -> Mem sym
memOpMem

annotateME :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  MemoryErrorReason ->
  Pred sym ->
  IO (Pred sym)
annotateME :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym)
annotateME sym
sym MemoryOp sym w
mop MemoryErrorReason
rsn Pred sym
p =
  do (SymAnnotation sym BaseBoolType
n, Pred sym
p') <- sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
p
     HasLLVMAnn sym
CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()
?recordLLVMAnnotation
       (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
mop)
       (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
n)
       (MemoryError sym -> BadBehavior sym
forall sym. MemoryError sym -> BadBehavior sym
BBMemoryError (MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
forall (w :: Nat) sym.
(1 <= w) =>
MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
MemoryError MemoryOp sym w
mop MemoryErrorReason
rsn))
     Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
p'

-- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.
projectLLVM_bv ::
  IsSymBackend sym bak =>
  bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv :: forall sym bak (w :: Nat).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak (LLVMPointer SymNat sym
blk SymBV sym w
bv) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     SymExpr sym BaseBoolType
p <- sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (SymExpr sym BaseBoolType))
-> IO (SymNat sym) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
p (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError String
"Pointer value coerced to bitvector" String
""
     SymBV sym w -> IO (SymBV sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymBV sym w
bv

------------------------------------------------------------------------
-- ** PartLLVMVal

-- | Either an 'LLVMValue' paired with a tree of predicates explaining
-- just when it is actually valid, or a type mismatch.
data PartLLVMVal sym where
  Err :: Pred sym -> PartLLVMVal sym
  NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym

partErr ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  MemoryErrorReason ->
  IO (PartLLVMVal sym)
partErr :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx MemoryErrorReason
rsn =
  do SymExpr sym BaseBoolType
p <- sym
-> MemoryOp sym w
-> MemoryErrorReason
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym)
annotateME sym
sym MemoryOp sym w
errCtx MemoryErrorReason
rsn (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymExpr sym BaseBoolType -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err SymExpr sym BaseBoolType
p)

attachSideCondition ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  sym ->
  CallStack ->
  Pred sym ->
  UB.UndefinedBehavior (RegValue' sym) ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
attachSideCondition :: forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> Pred sym
-> UndefinedBehavior (RegValue' sym)
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
attachSideCondition sym
sym CallStack
callStack Pred sym
pnew UndefinedBehavior (RegValue' sym)
ub PartLLVMVal sym
pv =
  case PartLLVMVal sym
pv of
    Err Pred sym
p -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)
    NoErr Pred sym
p LLVMVal sym
v ->
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym CallStack
callStack UndefinedBehavior (RegValue' sym)
ub Pred sym
pnew
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' LLVMVal sym
v

attachMemoryError ::
  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
  sym ->
  Pred sym ->
  MemoryOp sym w ->
  MemoryErrorReason ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
attachMemoryError :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> Pred sym
-> MemoryOp sym w
-> MemoryErrorReason
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
attachMemoryError sym
sym Pred sym
pnew MemoryOp sym w
mop MemoryErrorReason
rsn PartLLVMVal sym
pv =
  case PartLLVMVal sym
pv of
    Err Pred sym
p -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)
    NoErr Pred sym
p LLVMVal sym
v ->
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym)
annotateME sym
sym MemoryOp sym w
mop MemoryErrorReason
rsn Pred sym
pnew
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' LLVMVal sym
v

typeOfBitvector :: IsExpr (SymExpr sym)
                => proxy sym -> SymBV sym w -> StorageType
typeOfBitvector :: forall sym (proxy :: Type -> Type) (w :: Nat).
IsExpr (SymExpr sym) =>
proxy sym -> SymBV sym w -> StorageType
typeOfBitvector proxy sym
_ =
  Bytes -> StorageType
Type.bitvectorType (Bytes -> StorageType)
-> (SymExpr sym ('BaseBVType w) -> Bytes)
-> SymExpr sym ('BaseBVType w)
-> StorageType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Bytes
forall a. Integral a => a -> Bytes
Bytes.toBytes (Nat -> Bytes)
-> (SymExpr sym ('BaseBVType w) -> Nat)
-> SymExpr sym ('BaseBVType w)
-> Bytes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue (NatRepr w -> Nat)
-> (SymExpr sym ('BaseBVType w) -> NatRepr w)
-> SymExpr sym ('BaseBVType w)
-> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymExpr sym ('BaseBVType w) -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth

-- | An 'LLVMVal' which is always valid.
totalLLVMVal :: (IsExprBuilder sym)
             => sym
             -> LLVMVal sym
             -> PartLLVMVal sym
totalLLVMVal :: forall sym.
IsExprBuilder sym =>
sym -> LLVMVal sym -> PartLLVMVal sym
totalLLVMVal sym
sym = Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)

-- | Take a partial value and assert its safety
assertSafe :: IsSymBackend sym bak
           => bak
           -> PartLLVMVal sym
           -> IO (LLVMVal sym)
assertSafe :: forall sym bak.
IsSymBackend sym bak =>
bak -> PartLLVMVal sym -> IO (LLVMVal sym)
assertSafe bak
bak (NoErr Pred sym
p LLVMVal sym
v) =
  do let rsn :: SimErrorReason
rsn = String -> String -> SimErrorReason
AssertFailureSimError String
"Error during memory load" String
""
     bak -> Pred sym -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak Pred sym
p SimErrorReason
rsn
     LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMVal sym
v

assertSafe bak
bak (Err Pred sym
p) = do
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     let rsn :: SimErrorReason
rsn = String -> String -> SimErrorReason
AssertFailureSimError String
"Error during memory load" String
""
     ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     let err :: SimError
err = ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
rsn
     bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
p SimError
err)
     AbortExecReason -> IO (LLVMVal sym)
forall a. AbortExecReason -> IO a
abortExecBecause (SimError -> AbortExecReason
AssertionFailure SimError
err)

------------------------------------------------------------------------
-- ** PartLLVMVal interface
--

floatToBV ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
floatToBV :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
floatToBV sym
_ MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValUndef (StorageType StorageTypeF StorageType
Float Bytes
_))) =
  PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValUndef (Bytes -> StorageType
Type.bitvectorType Bytes
4)))

floatToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType StorageTypeF StorageType
Float Bytes
_))) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
W4I.natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 32)
iz <- sym -> NatRepr 32 -> BV 32 -> IO (SymExpr sym (BaseBVType 32))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @32) (NatRepr 32 -> BV 32
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 32) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 32)
iz))

floatToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValFloat FloatSize fi
Value.SingleSize SymInterpretedFloat sym fi
v)) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 32)
i  <- sym
-> FloatInfoRepr 'SingleFloat
-> SymInterpretedFloat sym 'SingleFloat
-> IO (SymBV sym (FloatInfoToBitWidth 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
W4IFP.iFloatToBinary sym
sym FloatInfoRepr 'SingleFloat
W4IFP.SingleFloatRepr SymInterpretedFloat sym fi
SymInterpretedFloat sym 'SingleFloat
v
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 32) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 32)
i))

floatToBV sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

floatToBV sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a float to a bitvector"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$
       Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

doubleToBV ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
doubleToBV :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
doubleToBV sym
_ MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValUndef (StorageType StorageTypeF StorageType
Double Bytes
_))) =
  PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValUndef (Bytes -> StorageType
Type.bitvectorType Bytes
8)))

doubleToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType StorageTypeF StorageType
Double Bytes
_))) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
W4I.natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 64)
iz <- sym -> NatRepr 64 -> BV 64 -> IO (SymExpr sym (BaseBVType 64))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @64) (NatRepr 64 -> BV 64
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 64) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 64)
iz))

doubleToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValFloat FloatSize fi
Value.DoubleSize SymInterpretedFloat sym fi
v)) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 64)
i  <- sym
-> FloatInfoRepr 'DoubleFloat
-> SymInterpretedFloat sym 'DoubleFloat
-> IO (SymBV sym (FloatInfoToBitWidth 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
W4IFP.iFloatToBinary sym
sym FloatInfoRepr 'DoubleFloat
W4IFP.DoubleFloatRepr SymInterpretedFloat sym fi
SymInterpretedFloat sym 'DoubleFloat
v
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 64) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 64)
i))

doubleToBV sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

doubleToBV sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a double to a bitvector"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$
       Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

fp80ToBV ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
fp80ToBV :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
fp80ToBV sym
_ MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValUndef (StorageType StorageTypeF StorageType
X86_FP80 Bytes
_))) =
  PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValUndef (Bytes -> StorageType
Type.bitvectorType Bytes
10)))

fp80ToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType StorageTypeF StorageType
X86_FP80 Bytes
_))) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
W4I.natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 80)
iz <- sym -> NatRepr 80 -> BV 80 -> IO (SymExpr sym (BaseBVType 80))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @80) (NatRepr 80 -> BV 80
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 80
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 80) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 80)
iz))

fp80ToBV sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValFloat FloatSize fi
Value.X86_FP80Size SymInterpretedFloat sym fi
v)) =
  do SymNat sym
nz <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     SymExpr sym (BaseBVType 80)
i  <- sym
-> FloatInfoRepr 'X86_80Float
-> SymInterpretedFloat sym 'X86_80Float
-> IO (SymBV sym (FloatInfoToBitWidth 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
W4IFP.iFloatToBinary sym
sym FloatInfoRepr 'X86_80Float
W4IFP.X86_80FloatRepr SymInterpretedFloat sym fi
SymInterpretedFloat sym 'X86_80Float
v
     PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 80) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
nz SymExpr sym (BaseBVType 80)
i))

fp80ToBV sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

fp80ToBV sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a FP80 to a bitvector"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

-- | Convert a bitvector to a float, asserting that it is not a pointer
bvToFloat :: forall sym w.
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

bvToFloat :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToFloat sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType (Bitvector Bytes
4) Bytes
_))) =
  Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatSize 'SingleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'SingleFloat
Value.SingleSize (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (sym
-> FloatInfoRepr 'SingleFloat
-> SymBV sym (FloatInfoToBitWidth 'SingleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'SingleFloat
W4IFP.SingleFloatRepr (SymExpr sym (BaseBVType 32)
 -> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)))
-> IO (SymExpr sym (BaseBVType 32))
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<<
       sym -> NatRepr 32 -> BV 32 -> IO (SymExpr sym (BaseBVType 32))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @32) (NatRepr 32 -> BV 32
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat))

bvToFloat sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p (LLVMValInt SymNat sym
blk SymBV sym w
off))
  | Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Nat) (b :: Nat).
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 (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off) (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @32) = do
      Pred sym
pz <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
      let ub :: UndefinedBehavior (RegValue' sym)
ub = RegValue' sym (LLVMPointerType 32)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerFloatCast (RegValue sym (LLVMPointerType 32)
-> RegValue' sym (LLVMPointerType 32)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymExpr sym (BaseBVType 32) -> LLVMPointer sym 32
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
SymExpr sym (BaseBVType 32)
off)) StorageType
Type.floatType
      Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx) UndefinedBehavior (RegValue' sym)
ub Pred sym
pz
      Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatSize 'SingleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'SingleFloat
Value.SingleSize (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        sym
-> FloatInfoRepr 'SingleFloat
-> SymBV sym (FloatInfoToBitWidth 'SingleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'SingleFloat
W4IFP.SingleFloatRepr SymBV sym w
SymBV sym (FloatInfoToBitWidth 'SingleFloat)
off

bvToFloat sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

bvToFloat sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a bitvector to a float"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]


-- | Convert a bitvector to a double, asserting that it is not a pointer
bvToDouble ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

bvToDouble :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToDouble sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType (Bitvector Bytes
8) Bytes
_))) =
  Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatSize 'DoubleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'DoubleFloat
Value.DoubleSize (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (sym
-> FloatInfoRepr 'DoubleFloat
-> SymBV sym (FloatInfoToBitWidth 'DoubleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'DoubleFloat
W4IFP.DoubleFloatRepr (SymExpr sym (BaseBVType 64)
 -> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)))
-> IO (SymExpr sym (BaseBVType 64))
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<<
       sym -> NatRepr 64 -> BV 64 -> IO (SymExpr sym (BaseBVType 64))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @64) (NatRepr 64 -> BV 64
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat))

bvToDouble sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p (LLVMValInt SymNat sym
blk SymBV sym w
off))
  | Just w :~: 64
Refl <- NatRepr w -> NatRepr 64 -> Maybe (w :~: 64)
forall (a :: Nat) (b :: Nat).
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 (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off) (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @64) = do
      Pred sym
pz <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
      let ub :: UndefinedBehavior (RegValue' sym)
ub = RegValue' sym (LLVMPointerType 64)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerFloatCast (RegValue sym (LLVMPointerType 64)
-> RegValue' sym (LLVMPointerType 64)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymExpr sym (BaseBVType 64) -> LLVMPointer sym 64
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
SymExpr sym (BaseBVType 64)
off)) StorageType
Type.doubleType
      Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx) UndefinedBehavior (RegValue' sym)
ub Pred sym
pz
      Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        FloatSize 'DoubleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'DoubleFloat
Value.DoubleSize (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        sym
-> FloatInfoRepr 'DoubleFloat
-> SymBV sym (FloatInfoToBitWidth 'DoubleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'DoubleFloat
W4IFP.DoubleFloatRepr SymBV sym w
SymBV sym (FloatInfoToBitWidth 'DoubleFloat)
off

bvToDouble sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

bvToDouble sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a bitvector to a double"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]


-- | Convert a bitvector to an FP80 float, asserting that it is not a pointer
bvToX86_FP80 ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

bvToX86_FP80 :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToX86_FP80 sym
sym MemoryOp sym w
_ (NoErr Pred sym
p (LLVMValZero (StorageType (Bitvector Bytes
10) Bytes
_))) =
  Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatSize 'X86_80Float
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'X86_80Float
Value.X86_FP80Size (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (sym
-> FloatInfoRepr 'X86_80Float
-> SymBV sym (FloatInfoToBitWidth 'X86_80Float)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'X86_80Float
W4IFP.X86_80FloatRepr (SymExpr sym (BaseBVType 80)
 -> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)))
-> IO (SymExpr sym (BaseBVType 80))
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<<
       sym -> NatRepr 80 -> BV 80 -> IO (SymExpr sym (BaseBVType 80))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @80) (NatRepr 80 -> BV 80
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 80
forall (n :: Nat). KnownNat n => NatRepr n
knownNat))

bvToX86_FP80 sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p (LLVMValInt SymNat sym
blk SymBV sym w
off))
  | Just w :~: 80
Refl <- NatRepr w -> NatRepr 80 -> Maybe (w :~: 80)
forall (a :: Nat) (b :: Nat).
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 (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off) (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @80) =
      do Pred sym
pz <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
         let ub :: UndefinedBehavior (RegValue' sym)
ub = RegValue' sym (LLVMPointerType 80)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerFloatCast (RegValue sym (LLVMPointerType 80)
-> RegValue' sym (LLVMPointerType 80)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymExpr sym (BaseBVType 80) -> LLVMPointer sym 80
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
SymExpr sym (BaseBVType 80)
off)) StorageType
Type.x86_fp80Type
         Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx) UndefinedBehavior (RegValue' sym)
ub Pred sym
pz
         Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym)
-> (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
    -> LLVMVal sym)
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> PartLLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatSize 'X86_80Float
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'X86_80Float
Value.X86_FP80Size (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
 -> PartLLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
-> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
           sym
-> FloatInfoRepr 'X86_80Float
-> SymBV sym (FloatInfoToBitWidth 'X86_80Float)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr 'X86_80Float
W4IFP.X86_80FloatRepr SymBV sym w
SymBV sym (FloatInfoToBitWidth 'X86_80Float)
off

bvToX86_FP80 sym
_ MemoryOp sym w
_ (Err Pred sym
p) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
p)

bvToX86_FP80 sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While converting from a bitvector to a X86_FP80"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

-- | Concatenate partial LLVM bitvector values. The least-significant
-- (low) bytes are given first. The allocation block number of each
-- argument is asserted to equal 0, indicating non-pointers.
bvConcat :: forall sym w.
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

bvConcat :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
bvConcat sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p1 LLVMVal sym
v1) (NoErr Pred sym
p2 LLVMVal sym
v2) =
    case (LLVMVal sym
v1, LLVMVal sym
v2) of
      (LLVMValInt SymNat sym
blk_low SymBV sym w
low, LLVMValInt SymNat sym
blk_high SymBV sym w
high) ->
        do SymNat sym
-> SymBV sym w -> SymNat sym -> SymBV sym w -> IO (PartLLVMVal sym)
forall (l :: Nat) (h :: Nat).
(1 <= l, 1 <= h) =>
SymNat sym
-> SymBV sym l -> SymNat sym -> SymBV sym h -> IO (PartLLVMVal sym)
go SymNat sym
blk_low SymBV sym w
low SymNat sym
blk_high SymBV sym w
high
      (LLVMValInt SymNat sym
blk_low SymBV sym w
low, LLVMValZero t :: StorageType
t@(StorageType (Bitvector Bytes
high_bytes) Bytes
_)) ->
        sym
-> Bytes
-> (forall {w :: Nat}.
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall sym a.
IsSymInterface sym =>
sym
-> Bytes
-> (forall (w :: Nat).
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO a)
-> IO a
Value.zeroInt sym
sym Bytes
high_bytes ((forall {w :: Nat}.
  (1 <= w) =>
  Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
 -> IO (PartLLVMVal sym))
-> (forall {w :: Nat}.
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ \case
          Maybe (SymNat sym, SymBV sym w)
Nothing -> sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ StorageType -> StorageType -> MemoryErrorReason
TypeMismatch (Maybe sym -> SymBV sym w -> StorageType
forall sym (proxy :: Type -> Type) (w :: Nat).
IsExpr (SymExpr sym) =>
proxy sym -> SymBV sym w -> StorageType
typeOfBitvector (sym -> Maybe sym
forall a. a -> Maybe a
Just sym
sym) SymBV sym w
low) StorageType
t
          Just (SymNat sym
blk_high, SymBV sym w
high) ->
            SymNat sym
-> SymBV sym w -> SymNat sym -> SymBV sym w -> IO (PartLLVMVal sym)
forall (l :: Nat) (h :: Nat).
(1 <= l, 1 <= h) =>
SymNat sym
-> SymBV sym l -> SymNat sym -> SymBV sym h -> IO (PartLLVMVal sym)
go SymNat sym
blk_low SymBV sym w
low SymNat sym
blk_high SymBV sym w
high
      (LLVMValZero t :: StorageType
t@(StorageType (Bitvector Bytes
low_bytes) Bytes
_), LLVMValInt SymNat sym
blk_high SymBV sym w
high) ->
         sym
-> Bytes
-> (forall {w :: Nat}.
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall sym a.
IsSymInterface sym =>
sym
-> Bytes
-> (forall (w :: Nat).
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO a)
-> IO a
Value.zeroInt sym
sym Bytes
low_bytes ((forall {w :: Nat}.
  (1 <= w) =>
  Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
 -> IO (PartLLVMVal sym))
-> (forall {w :: Nat}.
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ \case
           Maybe (SymNat sym, SymBV sym w)
Nothing -> sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ StorageType -> StorageType -> MemoryErrorReason
TypeMismatch (Maybe sym -> SymBV sym w -> StorageType
forall sym (proxy :: Type -> Type) (w :: Nat).
IsExpr (SymExpr sym) =>
proxy sym -> SymBV sym w -> StorageType
typeOfBitvector (sym -> Maybe sym
forall a. a -> Maybe a
Just sym
sym) SymBV sym w
high) StorageType
t
           Just (SymNat sym
blk_low, SymBV sym w
low) ->
             SymNat sym
-> SymBV sym w -> SymNat sym -> SymBV sym w -> IO (PartLLVMVal sym)
forall (l :: Nat) (h :: Nat).
(1 <= l, 1 <= h) =>
SymNat sym
-> SymBV sym l -> SymNat sym -> SymBV sym h -> IO (PartLLVMVal sym)
go SymNat sym
blk_low SymBV sym w
low SymNat sym
blk_high SymBV sym w
high
      (LLVMValZero (StorageType (Bitvector Bytes
low_bytes) Bytes
_), LLVMValZero (StorageType (Bitvector Bytes
high_bytes) Bytes
_)) ->
        PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ sym -> LLVMVal sym -> PartLLVMVal sym
forall sym.
IsExprBuilder sym =>
sym -> LLVMVal sym -> PartLLVMVal sym
totalLLVMVal sym
sym (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (Bytes -> StorageType
Type.bitvectorType (Bytes
low_bytes Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
high_bytes)))
      (LLVMVal sym
a, LLVMVal sym
b) -> sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
"While concatenating bitvectors"
                  [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
a, LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
b]

 where
  go :: forall l h. (1 <= l, 1 <= h) =>
    SymNat sym -> SymBV sym l -> SymNat sym -> SymBV sym h -> IO (PartLLVMVal sym)
  go :: forall (l :: Nat) (h :: Nat).
(1 <= l, 1 <= h) =>
SymNat sym
-> SymBV sym l -> SymNat sym -> SymBV sym h -> IO (PartLLVMVal sym)
go SymNat sym
blk_low SymBV sym l
low SymNat sym
blk_high SymBV sym h
high
    -- NB we check that the things we are concatenating are each an integral number of
    -- bytes.  This prevents us from concatenating together the partial-byte writes that
    -- result from e.g. writing an i1 or an i20 into memory.  This is consistent with LLVM
    -- documentation, which says that non-integral number of bytes loads will only succeed
    -- if the value was written orignally with the same type.
    | Nat
low_nat  Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
8 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0
    , Nat
high_nat Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
8 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 =
      do SymNat sym
blk0   <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
         -- TODO: Why won't this pattern match fail?
         Just LeqProof 1 (h + l)
LeqProof <- Maybe (LeqProof 1 (h + l)) -> IO (Maybe (LeqProof 1 (h + l)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (LeqProof 1 (h + l)) -> IO (Maybe (LeqProof 1 (h + l))))
-> Maybe (LeqProof 1 (h + l)) -> IO (Maybe (LeqProof 1 (h + l)))
forall a b. (a -> b) -> a -> b
$ NatRepr (h + l) -> Maybe (LeqProof 1 (h + l))
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat (NatRepr h -> NatRepr l -> NatRepr (h + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr h
high_w' NatRepr l
low_w')
         let ub1 :: UndefinedBehavior (RegValue' sym)
ub1 = RegValue' sym (LLVMPointerType l)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerIntCast (RegValue sym (LLVMPointerType l)
-> RegValue' sym (LLVMPointerType l)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymBV sym l -> LLVMPointer sym l
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk_low SymBV sym l
low))   StorageType
low_tp
             ub2 :: UndefinedBehavior (RegValue' sym)
ub2 = RegValue' sym (LLVMPointerType h)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerIntCast (RegValue sym (LLVMPointerType h)
-> RegValue' sym (LLVMPointerType h)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymBV sym h -> LLVMPointer sym h
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk_high SymBV sym h
high)) StorageType
high_tp
             annUB :: UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym)
annUB = sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx)
         Pred sym
predLow       <- UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym)
annUB UndefinedBehavior (RegValue' sym)
ub1 (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk_low SymNat sym
blk0
         Pred sym
predHigh      <- UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym)
annUB UndefinedBehavior (RegValue' sym)
ub2 (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk_high SymNat sym
blk0
         SymExpr sym (BaseBVType (h + l))
bv            <- sym
-> SymBV sym h
-> SymBV sym l
-> IO (SymExpr sym (BaseBVType (h + l)))
forall (u :: Nat) (v :: Nat).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Nat) (v :: Nat).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
W4I.bvConcat sym
sym SymBV sym h
high SymBV sym l
low

         Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p2 (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
predLow Pred sym
predHigh
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (SymNat sym -> SymExpr sym (BaseBVType (h + l)) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
blk0 SymExpr sym (BaseBVType (h + l))
bv)

    | Bool
otherwise = sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$
        Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
"Non-byte-sized bitvectors"
          [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v1, LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v2]

    where low_w' :: NatRepr l
low_w'  = SymBV sym l -> NatRepr l
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym l
low
          low_nat :: Nat
low_nat = NatRepr l -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr l
low_w'
          low_tp :: StorageType
low_tp  = Bytes -> StorageType
Type.bitvectorType (Nat -> Bytes
forall a. Integral a => a -> Bytes
Bytes.bitsToBytes Nat
low_nat)

          high_w' :: NatRepr h
high_w'  = SymBV sym h -> NatRepr h
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym h
high
          high_nat :: Nat
high_nat = NatRepr h -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr h
high_w'
          high_tp :: StorageType
high_tp  = Bytes -> StorageType
Type.bitvectorType (Nat -> Bytes
forall a. Integral a => a -> Bytes
Bytes.bitsToBytes Nat
high_nat)

bvConcat sym
sym MemoryOp sym w
_ (Err Pred sym
e1) (Err Pred sym
e2) = Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err (Pred sym -> PartLLVMVal sym)
-> IO (Pred sym) -> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
e1 Pred sym
e2
bvConcat sym
_ MemoryOp sym w
_ PartLLVMVal sym
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)
bvConcat sym
_ MemoryOp sym w
_ (Err Pred sym
e) PartLLVMVal sym
_ = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

-- | Cons an element onto a partial LLVM array value.
consArray ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
consArray :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
consArray sym
sym MemoryOp sym w
_ (NoErr Pred sym
p1 (LLVMValZero StorageType
tp)) (NoErr Pred sym
p2 (LLVMValZero (StorageType (Array Nat
m StorageType
tp') Bytes
_)))
  | StorageType
tp StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp' =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (Nat -> StorageType -> StorageType
Type.arrayType (Nat
mNat -> Nat -> Nat
forall a. Num a => a -> a -> a
+Nat
1) StorageType
tp')

consArray sym
sym MemoryOp sym w
_ (NoErr Pred sym
p1 LLVMVal sym
hd) (NoErr Pred sym
p2 (LLVMValZero (StorageType (Array Nat
m StorageType
tp) Bytes
_)))
  | LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
hd StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$
           StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp (LLVMVal sym -> Vector (LLVMVal sym) -> Vector (LLVMVal sym)
forall a. a -> Vector a -> Vector a
V.cons LLVMVal sym
hd (Int -> LLVMVal sym -> Vector (LLVMVal sym)
forall a. Int -> a -> Vector a
V.replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
m) (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
tp)))

consArray sym
sym MemoryOp sym w
_ (NoErr Pred sym
p1 (LLVMValInt SymNat sym
blk SymBV sym w
off)) (NoErr Pred sym
p2 (LLVMValString ByteString
bs))
  | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Nat) (b :: Nat).
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 (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off) (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @8)
  , Just Nat
0    <- SymNat sym -> Maybe Nat
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Nat
asNat SymNat sym
blk
  , Just BV 8
bv   <- SymExpr sym (BaseBVType 8) -> Maybe (BV 8)
forall (w :: Nat). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
SymExpr sym (BaseBVType 8)
off
  = do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
       PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (ByteString -> LLVMVal sym
forall sym. ByteString -> LLVMVal sym
LLVMValString (Word8 -> ByteString -> ByteString
BS.cons (Integer -> Word8
forall a. Num a => Integer -> a
fromInteger (BV 8 -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV 8
bv)) ByteString
bs))

consArray sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p1 LLVMVal sym
v) (NoErr Pred sym
p2 (LLVMValString ByteString
bs))
  = sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
consArray sym
sym MemoryOp sym w
errCtx (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p1 LLVMVal sym
v) (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> (LLVMVal sym -> PartLLVMVal sym)
-> LLVMVal sym
-> IO (PartLLVMVal sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p2 (LLVMVal sym -> IO (PartLLVMVal sym))
-> IO (LLVMVal sym) -> IO (PartLLVMVal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs

consArray sym
sym MemoryOp sym w
_ (NoErr Pred sym
p1 LLVMVal sym
hd) (NoErr Pred sym
p2 (LLVMValArray StorageType
tp Vector (LLVMVal sym)
vec))
  | LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
hd StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp (LLVMVal sym -> Vector (LLVMVal sym) -> Vector (LLVMVal sym)
forall a. a -> Vector a -> Vector a
V.cons LLVMVal sym
hd Vector (LLVMVal sym)
vec)

consArray sym
sym MemoryOp sym w
_ (Err Pred sym
e1) (Err Pred sym
e2) = Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err (Pred sym -> PartLLVMVal sym)
-> IO (Pred sym) -> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
e1 Pred sym
e2
consArray sym
_ MemoryOp sym w
_ (Err Pred sym
e) PartLLVMVal sym
_ = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)
consArray sym
_ MemoryOp sym w
_ PartLLVMVal sym
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

consArray sym
sym MemoryOp sym w
errCtx PartLLVMVal sym
_ (NoErr Pred sym
_ LLVMVal sym
v) =
  sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
"Non-array value" [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

-- | Append two partial LLVM array values.
appendArray ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  PartLLVMVal sym ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
appendArray :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
appendArray sym
sym MemoryOp sym w
_
  (NoErr Pred sym
p1 (LLVMValZero (StorageType (Array Nat
n1 StorageType
tp1) Bytes
_)))
  (NoErr Pred sym
p2 (LLVMValZero (StorageType (Array Nat
n2 StorageType
tp2) Bytes
_)))
  | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (Nat -> StorageType -> StorageType
Type.arrayType (Nat
n1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+Nat
n2) StorageType
tp1)

appendArray sym
sym MemoryOp sym w
_
  (NoErr Pred sym
p1 (LLVMValString ByteString
bs1))
  (NoErr Pred sym
p2 (LLVMValString ByteString
bs2))
  = do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
       PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ ByteString -> LLVMVal sym
forall sym. ByteString -> LLVMVal sym
LLVMValString (ByteString
bs1 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
bs2)

appendArray sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p1 (LLVMValString ByteString
bs1)) (NoErr Pred sym
p2 LLVMVal sym
v2)
  = do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs1
       sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
appendArray sym
sym MemoryOp sym w
errCtx (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p1 LLVMVal sym
bsv) (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p2 LLVMVal sym
v2)

appendArray sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
p1 LLVMVal sym
v1) (NoErr Pred sym
p2 (LLVMValString ByteString
bs2))
  = do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs2
       sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
appendArray sym
sym MemoryOp sym w
errCtx (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p1 LLVMVal sym
v1) (Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p2 LLVMVal sym
bsv)

appendArray sym
sym MemoryOp sym w
_
  (NoErr Pred sym
p1 (LLVMValZero (StorageType (Array Nat
n1 StorageType
tp1) Bytes
_)))
  (NoErr Pred sym
p2 (LLVMValArray StorageType
tp2 Vector (LLVMVal sym)
v2))
  | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 =
      do let v1 :: Vector (LLVMVal sym)
v1 = Int -> LLVMVal sym -> Vector (LLVMVal sym)
forall a. Int -> a -> Vector a
V.replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n1) (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
tp1)
         Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp1 (Vector (LLVMVal sym)
v1 Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> Vector (LLVMVal sym)
forall a. Vector a -> Vector a -> Vector a
V.++ Vector (LLVMVal sym)
v2)

appendArray sym
sym MemoryOp sym w
_
  (NoErr Pred sym
p1 (LLVMValArray StorageType
tp1 Vector (LLVMVal sym)
v1))
  (NoErr Pred sym
p2 (LLVMValZero (StorageType (Array Nat
n2 StorageType
tp2) Bytes
_)))
  | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 =
      do let v2 :: Vector (LLVMVal sym)
v2 = Int -> LLVMVal sym -> Vector (LLVMVal sym)
forall a. Int -> a -> Vector a
V.replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n2) (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
tp1)
         Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp1 (Vector (LLVMVal sym)
v1 Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> Vector (LLVMVal sym)
forall a. Vector a -> Vector a -> Vector a
V.++ Vector (LLVMVal sym)
v2)

appendArray sym
sym MemoryOp sym w
_
  (NoErr Pred sym
p1 (LLVMValArray StorageType
tp1 Vector (LLVMVal sym)
v1))
  (NoErr Pred sym
p2 (LLVMValArray StorageType
tp2 Vector (LLVMVal sym)
v2))
  | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp1 (Vector (LLVMVal sym)
v1 Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> Vector (LLVMVal sym)
forall a. Vector a -> Vector a -> Vector a
V.++ Vector (LLVMVal sym)
v2)

appendArray sym
sym MemoryOp sym w
_ (Err Pred sym
e1) (Err Pred sym
e2) = Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err (Pred sym -> PartLLVMVal sym)
-> IO (Pred sym) -> IO (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
e1 Pred sym
e2
appendArray sym
_ MemoryOp sym w
_ (Err Pred sym
e) PartLLVMVal sym
_ = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)
appendArray sym
_ MemoryOp sym w
_ PartLLVMVal sym
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

appendArray sym
sym MemoryOp sym w
errCtx (NoErr Pred sym
_ LLVMVal sym
v1) (NoErr Pred sym
_ LLVMVal sym
v2) =
  sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
"Non-array value when appending arrays"
          [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v1, LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v2]

-- | Make a partial LLVM array value.
--
-- It returns 'Err' if any of the elements of the vector are
-- 'Err'. Otherwise, the 'Pred' on the returned 'NoErr' value
-- is the 'And' of all the assertions on the values.
mkArray :: forall sym. (IsExprBuilder sym, IsSymInterface sym) =>
  sym ->
  StorageType ->
  Vector (PartLLVMVal sym) ->
  IO (PartLLVMVal sym)
mkArray :: forall sym.
(IsExprBuilder sym, IsSymInterface sym) =>
sym
-> StorageType -> Vector (PartLLVMVal sym) -> IO (PartLLVMVal sym)
mkArray sym
sym StorageType
tp Vector (PartLLVMVal sym)
vec =
  do let f :: PartLLVMVal sym -> StateT (Pred sym) (ExceptT (Pred sym) IO) (LLVMVal sym)
         f :: PartLLVMVal sym
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (LLVMVal sym)
f (Err SymExpr sym BaseBoolType
e) = SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (LLVMVal sym)
forall a.
SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError SymExpr sym BaseBoolType
e
         f (NoErr SymExpr sym BaseBoolType
p LLVMVal sym
x) = do
           SymExpr sym BaseBoolType
pd <- StateT
  (SymExpr sym BaseBoolType)
  (ExceptT (SymExpr sym BaseBoolType) IO)
  (SymExpr sym BaseBoolType)
forall s (m :: Type -> Type). MonadState s m => m s
get     -- Current predicates
           SymExpr sym BaseBoolType
pd' <- IO (SymExpr sym BaseBoolType)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (SymExpr sym BaseBoolType)
forall a.
IO a
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> StateT
      (SymExpr sym BaseBoolType)
      (ExceptT (SymExpr sym BaseBoolType) IO)
      (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
pd SymExpr sym BaseBoolType
p
           SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put SymExpr sym BaseBoolType
pd'    -- Append this one
           LLVMVal sym
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (LLVMVal sym)
forall a.
a
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMVal sym
x
     (ExceptT
  (SymExpr sym BaseBoolType)
  IO
  (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
-> IO
     (Either
        (SymExpr sym BaseBoolType)
        (Vector (LLVMVal sym), SymExpr sym BaseBoolType))
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (SymExpr sym BaseBoolType)
   IO
   (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
 -> IO
      (Either
         (SymExpr sym BaseBoolType)
         (Vector (LLVMVal sym), SymExpr sym BaseBoolType)))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
-> IO
     (Either
        (SymExpr sym BaseBoolType)
        (Vector (LLVMVal sym), SymExpr sym BaseBoolType))
forall a b. (a -> b) -> a -> b
$ (StateT
   (SymExpr sym BaseBoolType)
   (ExceptT (SymExpr sym BaseBoolType) IO)
   (Vector (LLVMVal sym))
 -> SymExpr sym BaseBoolType
 -> ExceptT
      (SymExpr sym BaseBoolType)
      IO
      (Vector (LLVMVal sym), SymExpr sym BaseBoolType))
-> SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (LLVMVal sym))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (SymExpr sym BaseBoolType)
  (ExceptT (SymExpr sym BaseBoolType) IO)
  (Vector (LLVMVal sym))
-> SymExpr sym BaseBoolType
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) (StateT
   (SymExpr sym BaseBoolType)
   (ExceptT (SymExpr sym BaseBoolType) IO)
   (Vector (LLVMVal sym))
 -> ExceptT
      (SymExpr sym BaseBoolType)
      IO
      (Vector (LLVMVal sym), SymExpr sym BaseBoolType))
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (LLVMVal sym))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ (PartLLVMVal sym
 -> StateT
      (SymExpr sym BaseBoolType)
      (ExceptT (SymExpr sym BaseBoolType) IO)
      (LLVMVal sym))
-> Vector (PartLLVMVal sym)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (LLVMVal sym))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse PartLLVMVal sym
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (LLVMVal sym)
f Vector (PartLLVMVal sym)
vec) IO
  (Either
     (SymExpr sym BaseBoolType)
     (Vector (LLVMVal sym), SymExpr sym BaseBoolType))
-> (Either
      (SymExpr sym BaseBoolType)
      (Vector (LLVMVal sym), SymExpr sym BaseBoolType)
    -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left SymExpr sym BaseBoolType
e -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err SymExpr sym BaseBoolType
e
        Right (Vector (LLVMVal sym)
vec', SymExpr sym BaseBoolType
p) -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr SymExpr sym BaseBoolType
p (StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp Vector (LLVMVal sym)
vec')


-- | Make a partial LLVM struct value.
--
-- It returns 'Err' if any of the struct fields are 'Err'.
-- Otherwise, the 'Pred' on the returned 'NoErr' value is the 'And' of all the
-- assertions on the values.
mkStruct :: forall sym. IsExprBuilder sym =>
  sym ->
  Vector (Field StorageType, PartLLVMVal sym) ->
  IO (PartLLVMVal sym)
mkStruct :: forall sym.
IsExprBuilder sym =>
sym
-> Vector (Field StorageType, PartLLVMVal sym)
-> IO (PartLLVMVal sym)
mkStruct sym
sym Vector (Field StorageType, PartLLVMVal sym)
vec =
  do let f :: (Field StorageType, PartLLVMVal sym) ->
              StateT (Pred sym) (ExceptT (Pred sym) IO) (Field StorageType, LLVMVal sym)
         f :: (Field StorageType, PartLLVMVal sym)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Field StorageType, LLVMVal sym)
f (Field StorageType
_, Err SymExpr sym BaseBoolType
e)       = SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Field StorageType, LLVMVal sym)
forall a.
SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError SymExpr sym BaseBoolType
e
         f (Field StorageType
fld, NoErr SymExpr sym BaseBoolType
p LLVMVal sym
x) = do
           SymExpr sym BaseBoolType
pd <- StateT
  (SymExpr sym BaseBoolType)
  (ExceptT (SymExpr sym BaseBoolType) IO)
  (SymExpr sym BaseBoolType)
forall s (m :: Type -> Type). MonadState s m => m s
get
           SymExpr sym BaseBoolType
pd' <- IO (SymExpr sym BaseBoolType)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (SymExpr sym BaseBoolType)
forall a.
IO a
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> StateT
      (SymExpr sym BaseBoolType)
      (ExceptT (SymExpr sym BaseBoolType) IO)
      (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
pd SymExpr sym BaseBoolType
p
           SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put SymExpr sym BaseBoolType
pd'
           (Field StorageType, LLVMVal sym)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Field StorageType, LLVMVal sym)
forall a.
a
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Field StorageType
fld, LLVMVal sym
x)

     (ExceptT
  (SymExpr sym BaseBoolType)
  IO
  (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
-> IO
     (Either
        (SymExpr sym BaseBoolType)
        (Vector (Field StorageType, LLVMVal sym),
         SymExpr sym BaseBoolType))
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (SymExpr sym BaseBoolType)
   IO
   (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
 -> IO
      (Either
         (SymExpr sym BaseBoolType)
         (Vector (Field StorageType, LLVMVal sym),
          SymExpr sym BaseBoolType)))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
-> IO
     (Either
        (SymExpr sym BaseBoolType)
        (Vector (Field StorageType, LLVMVal sym),
         SymExpr sym BaseBoolType))
forall a b. (a -> b) -> a -> b
$ (StateT
   (SymExpr sym BaseBoolType)
   (ExceptT (SymExpr sym BaseBoolType) IO)
   (Vector (Field StorageType, LLVMVal sym))
 -> SymExpr sym BaseBoolType
 -> ExceptT
      (SymExpr sym BaseBoolType)
      IO
      (Vector (Field StorageType, LLVMVal sym),
       SymExpr sym BaseBoolType))
-> SymExpr sym BaseBoolType
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (Field StorageType, LLVMVal sym))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (SymExpr sym BaseBoolType)
  (ExceptT (SymExpr sym BaseBoolType) IO)
  (Vector (Field StorageType, LLVMVal sym))
-> SymExpr sym BaseBoolType
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) (StateT
   (SymExpr sym BaseBoolType)
   (ExceptT (SymExpr sym BaseBoolType) IO)
   (Vector (Field StorageType, LLVMVal sym))
 -> ExceptT
      (SymExpr sym BaseBoolType)
      IO
      (Vector (Field StorageType, LLVMVal sym),
       SymExpr sym BaseBoolType))
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (Field StorageType, LLVMVal sym))
-> ExceptT
     (SymExpr sym BaseBoolType)
     IO
     (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ((Field StorageType, PartLLVMVal sym)
 -> StateT
      (SymExpr sym BaseBoolType)
      (ExceptT (SymExpr sym BaseBoolType) IO)
      (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType, PartLLVMVal sym)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Vector (Field StorageType, LLVMVal sym))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (Field StorageType, PartLLVMVal sym)
-> StateT
     (SymExpr sym BaseBoolType)
     (ExceptT (SymExpr sym BaseBoolType) IO)
     (Field StorageType, LLVMVal sym)
f Vector (Field StorageType, PartLLVMVal sym)
vec) IO
  (Either
     (SymExpr sym BaseBoolType)
     (Vector (Field StorageType, LLVMVal sym),
      SymExpr sym BaseBoolType))
-> (Either
      (SymExpr sym BaseBoolType)
      (Vector (Field StorageType, LLVMVal sym), SymExpr sym BaseBoolType)
    -> IO (PartLLVMVal sym))
-> IO (PartLLVMVal sym)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Left SymExpr sym BaseBoolType
e -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymExpr sym BaseBoolType -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err SymExpr sym BaseBoolType
e)
       Right (Vector (Field StorageType, LLVMVal sym)
vec',SymExpr sym BaseBoolType
p) -> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr SymExpr sym BaseBoolType
p (Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall sym. Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
LLVMValStruct Vector (Field StorageType, LLVMVal sym)
vec')

-- | Select some of the least significant bytes of a partial LLVM
-- bitvector value. The allocation block number of the argument is
-- asserted to equal 0, indicating a non-pointer.
selectLowBv ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  Bytes ->
  Bytes ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

selectLowBv :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> Bytes
-> Bytes
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
selectLowBv sym
_sym MemoryOp sym w
_ Bytes
low Bytes
hi (NoErr Pred sym
p (LLVMValZero (StorageType (Bitvector Bytes
bytes) Bytes
_)))
  | Bytes
low Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
hi Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
bytes =
      PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (Bytes -> StorageType
Type.bitvectorType Bytes
low)

selectLowBv sym
sym MemoryOp sym w
errCtx Bytes
low Bytes
hi (NoErr Pred sym
p (LLVMValInt SymNat sym
blk SymBV sym w
bv))
  | Just (Some (NatRepr x
low_w)) <- Nat -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Bytes -> Nat
Bytes.bytesToBits Bytes
low)
  , Just (Some (NatRepr x
hi_w))  <- Nat -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Bytes -> Nat
Bytes.bytesToBits Bytes
hi)
  , Just LeqProof 1 x
LeqProof       <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
low_w
  , Just (x + x) :~: w
Refl           <- NatRepr (x + x) -> NatRepr w -> Maybe ((x + x) :~: w)
forall (a :: Nat) (b :: Nat).
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 x -> NatRepr x -> NatRepr (x + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
low_w NatRepr x
hi_w) NatRepr w
w
  , Just LeqProof x w
LeqProof       <- NatRepr x -> NatRepr w -> Maybe (LeqProof x w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq NatRepr x
low_w NatRepr w
w =
      do Pred sym
pz  <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
         SymExpr sym (BaseBVType x)
bv' <- sym
-> NatRepr 0
-> NatRepr x
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType x))
forall (idx :: Nat) (n :: Nat) (w :: Nat).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect sym
sym (NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 0) NatRepr x
low_w SymBV sym w
bv
         let ub :: UndefinedBehavior (RegValue' sym)
ub = RegValue' sym (LLVMPointerType w)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerIntCast (RegValue sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
bv)) StorageType
tp
         Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx) UndefinedBehavior (RegValue' sym)
ub Pred sym
pz
         PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymExpr sym (BaseBVType x) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
blk SymExpr sym (BaseBVType x)
bv'
 where w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
bv
       tp :: StorageType
tp = Bytes -> StorageType
Type.bitvectorType (Nat -> Bytes
forall a. Integral a => a -> Bytes
Bytes.bitsToBytes (NatRepr w -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w))

selectLowBv sym
sym MemoryOp sym w
errCtx Bytes
_ Bytes
_ (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While selecting the low bits of a bitvector"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

selectLowBv sym
_ MemoryOp sym w
_ Bytes
_ Bytes
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

-- | Select some of the most significant bytes of a partial LLVM
-- bitvector value. The allocation block number of the argument is
-- asserted to equal 0, indicating a non-pointer.
selectHighBv ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  Bytes ->
  Bytes ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)

selectHighBv :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> Bytes
-> Bytes
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
selectHighBv sym
_sym MemoryOp sym w
_ Bytes
low Bytes
hi (NoErr Pred sym
p (LLVMValZero (StorageType (Bitvector Bytes
bytes) Bytes
_)))
  | Bytes
low Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
hi Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
bytes =
      PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (Bytes -> StorageType
Type.bitvectorType Bytes
hi)

selectHighBv sym
sym MemoryOp sym w
errCtx Bytes
low Bytes
hi (NoErr Pred sym
p (LLVMValInt SymNat sym
blk SymBV sym w
bv))
  | Just (Some (NatRepr x
low_w)) <- Nat -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Bytes -> Nat
Bytes.bytesToBits Bytes
low)
  , Just (Some (NatRepr x
hi_w))  <- Nat -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Bytes -> Nat
Bytes.bytesToBits Bytes
hi)
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
hi_w
  , Just (x + x) :~: w
Refl <- NatRepr (x + x) -> NatRepr w -> Maybe ((x + x) :~: w)
forall (a :: Nat) (b :: Nat).
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 x -> NatRepr x -> NatRepr (x + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
low_w NatRepr x
hi_w) NatRepr w
w =
    do Pred sym
pz <-  sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
       SymExpr sym (BaseBVType x)
bv' <- sym
-> NatRepr x
-> NatRepr x
-> SymBV sym w
-> IO (SymExpr sym (BaseBVType x))
forall (idx :: Nat) (n :: Nat) (w :: Nat).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect sym
sym NatRepr x
low_w NatRepr x
hi_w SymBV sym w
bv
       let ub :: UndefinedBehavior (RegValue' sym)
ub = RegValue' sym (LLVMPointerType w)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Nat) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
UB.PointerIntCast (RegValue sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
bv)) StorageType
tp
       Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym (MemoryOp sym w -> CallStack
forall sym (w :: Nat). MemoryOp sym w -> CallStack
memOpCallStack MemoryOp sym w
errCtx) UndefinedBehavior (RegValue' sym)
ub Pred sym
pz
       PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymExpr sym (BaseBVType x) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
blk SymExpr sym (BaseBVType x)
bv'
  where w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
bv
        tp :: StorageType
tp = Bytes -> StorageType
Type.bitvectorType (Nat -> Bytes
forall a. Integral a => a -> Bytes
Bytes.bitsToBytes (NatRepr w -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w))
selectHighBv sym
_ MemoryOp sym w
_ Bytes
_ Bytes
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

selectHighBv sym
sym MemoryOp sym w
errCtx Bytes
_ Bytes
_ (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While selecting the high bits of a bitvector"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]


-- | Look up an element in a partial LLVM array value.
arrayElt ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  Natural ->
  StorageType ->
  Natural ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
arrayElt :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> Nat
-> StorageType
-> Nat
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
arrayElt sym
_ MemoryOp sym w
_ Nat
sz StorageType
tp Nat
idx (NoErr Pred sym
p (LLVMValZero StorageType
_)) -- TODO(langston) typecheck
  | Nat
0 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
idx
  , Nat
idx Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
sz =
    PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
tp)

arrayElt sym
sym MemoryOp sym w
_ Nat
sz StorageType
tp Nat
idx (NoErr Pred sym
p (LLVMValString ByteString
bs))
  | Nat
sz Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)
  , Nat
0 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
idx
  , Nat
idx Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
sz
  , StorageType
tp StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes -> StorageType
Type.bitvectorType (Integer -> Bytes
Bytes.Bytes Integer
1)
  = do SymNat sym
blk <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
       SymExpr sym (BaseBVType 8)
off <- sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @8) (Word8 -> BV 8
BV.word8 (HasCallStack => ByteString -> Int -> Word8
ByteString -> Int -> Word8
BS.index ByteString
bs (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
idx)))
       PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (SymNat sym -> SymExpr sym (BaseBVType 8) -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
blk SymExpr sym (BaseBVType 8)
off)

arrayElt sym
_ MemoryOp sym w
_ Nat
sz StorageType
tp Nat
idx (NoErr Pred sym
p (LLVMValArray StorageType
tp' Vector (LLVMVal sym)
vec))
  | Nat
sz Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
vec)
  , Nat
0 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
idx
  , Nat
idx Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
sz
  , StorageType
tp StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp' =
    PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (Vector (LLVMVal sym)
vec Vector (LLVMVal sym) -> Int -> LLVMVal sym
forall a. Vector a -> Int -> a
V.! Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
idx)

arrayElt sym
_ MemoryOp sym w
_ Nat
_ StorageType
_ Nat
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

arrayElt sym
sym MemoryOp sym w
errCtx Nat
_ StorageType
_ Nat
_ (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While selecting and element of an array"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

-- | Look up a field in a partial LLVM struct value.
fieldVal ::
  (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
  sym ->
  MemoryOp sym w ->
  (Vector (Field StorageType)) ->
  Int ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
fieldVal :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym
-> MemoryOp sym w
-> Vector (Field StorageType)
-> Int
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
fieldVal sym
_ MemoryOp sym w
_ Vector (Field StorageType)
flds Int
idx (NoErr Pred sym
p (LLVMValZero StorageType
_)) -- TODO(langston) typecheck
  | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
idx
  , Int
idx Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Vector (Field StorageType) -> Int
forall a. Vector a -> Int
V.length Vector (Field StorageType)
flds =
      PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero (StorageType -> LLVMVal sym) -> StorageType -> LLVMVal sym
forall a b. (a -> b) -> a -> b
$ Getting StorageType (Field StorageType) StorageType
-> Field StorageType -> StorageType
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
Type.fieldVal (Field StorageType -> StorageType)
-> Field StorageType -> StorageType
forall a b. (a -> b) -> a -> b
$ Vector (Field StorageType)
flds Vector (Field StorageType) -> Int -> Field StorageType
forall a. Vector a -> Int -> a
V.! Int
idx

fieldVal sym
_ MemoryOp sym w
_ Vector (Field StorageType)
flds Int
idx (NoErr Pred sym
p (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
vec))
  | Vector (Field StorageType)
flds Vector (Field StorageType) -> Vector (Field StorageType) -> Bool
forall a. Eq a => a -> a -> Bool
== ((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
vec
  , Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
idx
  , Int
idx Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Vector (Field StorageType, LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (Field StorageType, LLVMVal sym)
vec =
    PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> IO (PartLLVMVal sym))
-> PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p (LLVMVal sym -> PartLLVMVal sym) -> LLVMVal sym -> PartLLVMVal sym
forall a b. (a -> b) -> a -> b
$ (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd ((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a -> b) -> a -> b
$ (Vector (Field StorageType, LLVMVal sym)
vec Vector (Field StorageType, LLVMVal sym)
-> Int -> (Field StorageType, LLVMVal sym)
forall a. Vector a -> Int -> a
V.! Int
idx)

fieldVal sym
_ MemoryOp sym w
_ Vector (Field StorageType)
_ Int
_ (Err Pred sym
e) = PartLLVMVal sym -> IO (PartLLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err Pred sym
e)

fieldVal sym
sym MemoryOp sym w
errCtx Vector (Field StorageType)
_ Int
_ (NoErr Pred sym
_ LLVMVal sym
v) =
  do let msg :: Text
msg = Text
"While getting a struct field"
     sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
partErr sym
sym MemoryOp sym w
errCtx (MemoryErrorReason -> IO (PartLLVMVal sym))
-> MemoryErrorReason -> IO (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Text -> [StorageType] -> MemoryErrorReason
UnexpectedArgumentType Text
msg [LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
Value.llvmValStorableType LLVMVal sym
v]

------------------------------------------------------------------------
-- ** Merging and muxing
--

-- | If-then-else on partial expressions.
merge :: forall sym m. (IsSymInterface sym, HasLLVMAnn sym, MonadIO m) =>
  sym ->
  (Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym))
    {- ^ Operation to combine inner values. The 'Pred' parameter is the
         if/then/else condition -} ->
  Pred sym {- ^ condition to merge on -} ->
  PartLLVMVal sym {- ^ 'then' value -}  ->
  PartLLVMVal sym {- ^ 'else' value -} ->
  m (PartLLVMVal sym)
merge :: forall sym (m :: Type -> Type).
(IsSymInterface sym, HasLLVMAnn sym, MonadIO m) =>
sym
-> (Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym))
-> Pred sym
-> PartLLVMVal sym
-> PartLLVMVal sym
-> m (PartLLVMVal sym)
merge sym
sym Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym)
_ Pred sym
c (Err Pred sym
e1) (Err Pred sym
e2) = Pred sym -> PartLLVMVal sym
forall sym. Pred sym -> PartLLVMVal sym
Err (Pred sym -> PartLLVMVal sym)
-> m (Pred sym) -> m (PartLLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c Pred sym
e1 Pred sym
e2)

merge sym
sym Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym)
_ Pred sym
cond (NoErr Pred sym
p LLVMVal sym
v) (Err Pred sym
pe) =
  do Pred sym
p' <- IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
cond Pred sym
p Pred sym
pe)
     PartLLVMVal sym -> m (PartLLVMVal sym)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartLLVMVal sym -> m (PartLLVMVal sym))
-> PartLLVMVal sym -> m (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' LLVMVal sym
v
merge sym
sym Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym)
_ Pred sym
cond (Err Pred sym
pe) (NoErr Pred sym
p LLVMVal sym
v) = do
  do Pred sym
p' <- IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
cond Pred sym
pe Pred sym
p)
     PartLLVMVal sym -> m (PartLLVMVal sym)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartLLVMVal sym -> m (PartLLVMVal sym))
-> PartLLVMVal sym -> m (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' LLVMVal sym
v
merge sym
sym Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym)
f Pred sym
cond (NoErr Pred sym
px LLVMVal sym
x) (NoErr Pred sym
py LLVMVal sym
y) = do
  LLVMVal sym
v <- Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym)
f Pred sym
cond LLVMVal sym
x LLVMVal sym
y
  Pred sym
p' <- IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
cond Pred sym
px Pred sym
py)
  PartLLVMVal sym -> m (PartLLVMVal sym)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartLLVMVal sym -> m (PartLLVMVal sym))
-> PartLLVMVal sym -> m (PartLLVMVal sym)
forall a b. (a -> b) -> a -> b
$ Pred sym -> LLVMVal sym -> PartLLVMVal sym
forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
NoErr Pred sym
p' LLVMVal sym
v

-- | Mux partial LLVM values.
--
--   Will @panic@ if the values are not structurally related.
--   This should never happen, as we only call @muxLLVMVal@
--   from inside the memory model as we read values, and the
--   shape of values is determined by the memory type
--   at which we read values.
muxLLVMVal :: forall sym.
  (IsSymInterface sym, HasLLVMAnn sym) =>
  sym ->
  Pred sym ->
  PartLLVMVal sym ->
  PartLLVMVal sym ->
  IO (PartLLVMVal sym)
muxLLVMVal :: forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> Pred sym
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
muxLLVMVal sym
sym = sym
-> (SymExpr sym BaseBoolType
    -> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym))
-> SymExpr sym BaseBoolType
-> PartLLVMVal sym
-> PartLLVMVal sym
-> IO (PartLLVMVal sym)
forall sym (m :: Type -> Type).
(IsSymInterface sym, HasLLVMAnn sym, MonadIO m) =>
sym
-> (Pred sym -> LLVMVal sym -> LLVMVal sym -> m (LLVMVal sym))
-> Pred sym
-> PartLLVMVal sym
-> PartLLVMVal sym
-> m (PartLLVMVal sym)
merge sym
sym SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval
  where

    muxzero :: Pred sym -> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
    muxzero :: SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond StorageType
tpz LLVMVal sym
val = case LLVMVal sym
val of
      LLVMValZero StorageType
tp -> LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
tp
      LLVMValUndef StorageType
tpu ->
        -- TODO: Is this the right behavior?
        String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cannot mux zero and undef" [ String
"Zero type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
tpz
                                          , String
"Undef type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
tpu
                                          ]

      LLVMValString ByteString
bs -> SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond StorageType
tpz (LLVMVal sym -> IO (LLVMVal sym))
-> IO (LLVMVal sym) -> IO (LLVMVal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs

      LLVMValInt SymNat sym
base SymBV sym w
off ->
        do SymNat sym
zbase <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
W4I.natLit sym
sym Nat
0
           SymBV sym w
zoff  <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4I.bvLit sym
sym (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4I.bvWidth SymBV sym w
off) (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4I.bvWidth SymBV sym w
off))
           SymNat sym
base' <- sym
-> SymExpr sym BaseBoolType
-> SymNat sym
-> SymNat sym
-> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
W4I.natIte sym
sym SymExpr sym BaseBoolType
cond SymNat sym
zbase SymNat sym
base
           SymBV sym w
off'  <- sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4I.bvIte sym
sym SymExpr sym BaseBoolType
cond SymBV sym w
zoff SymBV sym w
off
           LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymBV sym w -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
base' SymBV sym w
off'
      LLVMValFloat FloatSize fi
Value.SingleSize SymInterpretedFloat sym fi
x ->
        do SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
zerof <- (sym
-> FloatInfoRepr 'SingleFloat
-> Rational
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatLitRational sym
sym FloatInfoRepr 'SingleFloat
W4IFP.SingleFloatRepr Rational
0)
           SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
x'    <- (forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatIte @_ @W4IFP.SingleFloat sym
sym SymExpr sym BaseBoolType
cond SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
zerof SymInterpretedFloat sym fi
SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
x)
           LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ FloatSize 'SingleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'SingleFloat
Value.SingleSize SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
x'
      LLVMValFloat FloatSize fi
Value.DoubleSize SymInterpretedFloat sym fi
x ->
        do SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
zerof <- (sym
-> FloatInfoRepr 'DoubleFloat
-> Rational
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatLitRational sym
sym FloatInfoRepr 'DoubleFloat
W4IFP.DoubleFloatRepr Rational
0)
           SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
x'    <- (forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatIte @_ @W4IFP.DoubleFloat sym
sym SymExpr sym BaseBoolType
cond SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
zerof SymInterpretedFloat sym fi
SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
x)
           LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ FloatSize 'DoubleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'DoubleFloat
Value.DoubleSize SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
x'
      LLVMValFloat FloatSize fi
Value.X86_FP80Size SymInterpretedFloat sym fi
x ->
        do SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
zerof <- (sym
-> FloatInfoRepr 'X86_80Float
-> Rational
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatLitRational sym
sym FloatInfoRepr 'X86_80Float
W4IFP.X86_80FloatRepr Rational
0)
           SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
x'    <- (forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatIte @_ @W4IFP.X86_80Float sym
sym SymExpr sym BaseBoolType
cond SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
zerof SymInterpretedFloat sym fi
SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
x)
           LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ FloatSize 'X86_80Float
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'X86_80Float
Value.X86_FP80Size SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
x'

      LLVMValArray StorageType
tp Vector (LLVMVal sym)
vec -> StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp (Vector (LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (LLVMVal sym -> IO (LLVMVal sym))
-> Vector (LLVMVal sym) -> IO (Vector (LLVMVal sym))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond StorageType
tp) Vector (LLVMVal sym)
vec

      LLVMValStruct Vector (Field StorageType, LLVMVal sym)
flds -> Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall sym. Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
LLVMValStruct (Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((Field StorageType, LLVMVal sym)
 -> IO (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType, LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (\(Field StorageType
fld, LLVMVal sym
v) -> (Field StorageType
fld,) (LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (LLVMVal sym) -> IO (Field StorageType, LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
                     SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond (Field StorageType
fldField StorageType
-> Getting StorageType (Field StorageType) StorageType
-> StorageType
forall s a. s -> Getting a s a -> a
^.Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
Type.fieldVal) LLVMVal sym
v) Vector (Field StorageType, LLVMVal sym)
flds


    muxval :: Pred sym -> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
    muxval :: SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond (LLVMValZero StorageType
tp) LLVMVal sym
v = SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond StorageType
tp LLVMVal sym
v
    muxval SymExpr sym BaseBoolType
cond LLVMVal sym
v (LLVMValZero StorageType
tp) = do SymExpr sym BaseBoolType
cond' <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym SymExpr sym BaseBoolType
cond
                                        SymExpr sym BaseBoolType
-> StorageType -> LLVMVal sym -> IO (LLVMVal sym)
muxzero SymExpr sym BaseBoolType
cond' StorageType
tp LLVMVal sym
v

    muxval SymExpr sym BaseBoolType
cond (LLVMValInt SymNat sym
base1 SymBV sym w
off1) (LLVMValInt SymNat sym
base2 SymBV sym w
off2)
      | Just w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Nat) (b :: Nat).
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 (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off1) (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off2)
      = do SymNat sym
base <- IO (SymNat sym) -> IO (SymNat sym)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym) -> IO (SymNat sym))
-> IO (SymNat sym) -> IO (SymNat sym)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymNat sym
-> SymNat sym
-> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym SymExpr sym BaseBoolType
cond SymNat sym
base1 SymNat sym
base2
           SymBV sym w
off  <- IO (SymBV sym w) -> IO (SymBV sym w)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym w) -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
cond SymBV sym w
off1 SymBV sym w
SymBV sym w
off2
           LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (LLVMVal sym -> IO (LLVMVal sym))
-> LLVMVal sym -> IO (LLVMVal sym)
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymBV sym w -> LLVMVal sym
forall (w :: Nat) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
base SymBV sym w
off

    muxval SymExpr sym BaseBoolType
cond (LLVMValFloat (FloatSize fi
xsz :: Value.FloatSize fi) SymInterpretedFloat sym fi
x) (LLVMValFloat FloatSize fi
ysz SymInterpretedFloat sym fi
y)
      | Just fi :~: fi
Refl <- FloatSize fi -> FloatSize fi -> Maybe (fi :~: fi)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: FloatInfo) (b :: FloatInfo).
FloatSize a -> FloatSize b -> Maybe (a :~: b)
testEquality FloatSize fi
xsz FloatSize fi
ysz
      = FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize fi
xsz (SymInterpretedFloat sym fi -> LLVMVal sym)
-> IO (SymInterpretedFloat sym fi) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
          (IO (SymInterpretedFloat sym fi) -> IO (SymInterpretedFloat sym fi)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymInterpretedFloat sym fi)
 -> IO (SymInterpretedFloat sym fi))
-> IO (SymInterpretedFloat sym fi)
-> IO (SymInterpretedFloat sym fi)
forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatIte @_ @fi sym
sym SymExpr sym BaseBoolType
cond SymInterpretedFloat sym fi
x SymInterpretedFloat sym fi
SymInterpretedFloat sym fi
y)

    muxval SymExpr sym BaseBoolType
cond (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
fls1) (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
fls2)
      | ((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
fls1 Vector (Field StorageType) -> Vector (Field StorageType) -> Bool
forall a. Eq a => a -> a -> Bool
== ((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
fls2 =
          Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall sym. Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
LLVMValStruct (Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
            ((Field StorageType, LLVMVal sym)
 -> (Field StorageType, LLVMVal sym)
 -> IO (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType, LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym))
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM (\(Field StorageType
f, LLVMVal sym
x) (Field StorageType
_, LLVMVal sym
y) -> (Field StorageType
f,) (LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (LLVMVal sym) -> IO (Field StorageType, LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond LLVMVal sym
x LLVMVal sym
y) Vector (Field StorageType, LLVMVal sym)
fls1 Vector (Field StorageType, LLVMVal sym)
fls2

    muxval SymExpr sym BaseBoolType
cond (LLVMValString ByteString
bs1) (LLVMValString ByteString
bs2)
      | ByteString
bs1 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
bs2 = LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ByteString -> LLVMVal sym
forall sym. ByteString -> LLVMVal sym
LLVMValString ByteString
bs1)
      | ByteString -> Int
BS.length ByteString
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString -> Int
BS.length ByteString
bs2
      =  do LLVMVal sym
v1 <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs1
            LLVMVal sym
v2 <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs2
            SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond LLVMVal sym
v1 LLVMVal sym
v2

    muxval SymExpr sym BaseBoolType
cond (LLVMValString ByteString
bs) v :: LLVMVal sym
v@LLVMValArray{}
      = do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs
           SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond LLVMVal sym
bsv LLVMVal sym
v

    muxval SymExpr sym BaseBoolType
cond v :: LLVMVal sym
v@LLVMValArray{} (LLVMValString ByteString
bs)
      = do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
Value.explodeStringValue sym
sym ByteString
bs
           SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond LLVMVal sym
v LLVMVal sym
bsv

    muxval SymExpr sym BaseBoolType
cond (LLVMValArray StorageType
tp1 Vector (LLVMVal sym)
v1) (LLVMValArray StorageType
tp2 Vector (LLVMVal sym)
v2)
      | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 Bool -> Bool -> Bool
&& Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
v2 = do
          StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
tp1 (Vector (LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym))
-> Vector (LLVMVal sym)
-> Vector (LLVMVal sym)
-> IO (Vector (LLVMVal sym))
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM (SymExpr sym BaseBoolType
-> LLVMVal sym -> LLVMVal sym -> IO (LLVMVal sym)
muxval SymExpr sym BaseBoolType
cond) Vector (LLVMVal sym)
v1 Vector (LLVMVal sym)
v2

    muxval SymExpr sym BaseBoolType
_ v1 :: LLVMVal sym
v1@(LLVMValUndef StorageType
tp1) (LLVMValUndef StorageType
tp2)
      | StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 = LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure LLVMVal sym
v1

    muxval SymExpr sym BaseBoolType
_ LLVMVal sym
v1 LLVMVal sym
v2 =
      String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cannot mux LLVM values"
        [ String
"v1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LLVMVal sym -> String
forall a. Show a => a -> String
show LLVMVal sym
v1
        , String
"v2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LLVMVal sym -> String
forall a. Show a => a -> String
show LLVMVal sym
v2
        ]