qute-symex-0.1.0: A symbolic execution engine for the QBE intermediate language.
Safe HaskellNone
LanguageGHC2021

Language.QBE.Simulator.Concolic.Expression

Documentation

data Concolic v Source #

Constructors

Concolic 

Fields

Instances

Instances details
NFData1 Concolic Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Methods

liftRnf :: (a -> ()) -> Concolic a -> () #

Generic1 Concolic Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Associated Types

type Rep1 Concolic 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

type Rep1 Concolic = D1 ('MetaData "Concolic" "Language.QBE.Simulator.Concolic.Expression" "qute-symex-0.1.0-BpSHhgkMrEs8e4o3qeYGbi" 'False) (C1 ('MetaCons "Concolic" 'PrefixI 'True) (S1 ('MetaSel ('Just "concrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Just "symbolic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BitVector))))

Methods

from1 :: Concolic a -> Rep1 Concolic a #

to1 :: Rep1 Concolic a -> Concolic a #

Simulator SimState (Concolic RegVal) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.State

Methods

isTrue :: Concolic RegVal -> SimState Bool #

toAddress :: Concolic RegVal -> SimState Address #

lookupSymbol :: GlobalIdent -> SimState (Maybe Address) #

findFunc :: GlobalIdent -> SimState (Maybe (SomeFunc SimState (Concolic RegVal))) #

findFuncByAddr :: Address -> SimState (Maybe (SomeFunc SimState (Concolic RegVal))) #

activeFrame :: SimState (StackFrame (Concolic RegVal)) #

pushStackFrame :: StackFrame (Concolic RegVal) -> SimState () #

popStackFrame :: SimState (StackFrame (Concolic RegVal)) #

getSP :: SimState (Concolic RegVal) #

setSP :: Concolic RegVal -> SimState () #

writeMemory :: Address -> ExtType -> Concolic RegVal -> SimState () #

readMemory :: LoadType -> Address -> SimState (Concolic RegVal) #

Generic (Concolic v) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Associated Types

type Rep (Concolic v) 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

type Rep (Concolic v) = D1 ('MetaData "Concolic" "Language.QBE.Simulator.Concolic.Expression" "qute-symex-0.1.0-BpSHhgkMrEs8e4o3qeYGbi" 'False) (C1 ('MetaCons "Concolic" 'PrefixI 'True) (S1 ('MetaSel ('Just "concrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v) :*: S1 ('MetaSel ('Just "symbolic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BitVector))))

Methods

from :: Concolic v -> Rep (Concolic v) x #

to :: Rep (Concolic v) x -> Concolic v #

Show v => Show (Concolic v) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Methods

showsPrec :: Int -> Concolic v -> ShowS #

show :: Concolic v -> String #

showList :: [Concolic v] -> ShowS #

NFData a => NFData (Concolic a) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Methods

rnf :: Concolic a -> () #

ValueRepr (Concolic RegVal) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Methods

fromLit :: ExtType -> Word64 -> Concolic RegVal #

fromFloat :: Float -> Concolic RegVal #

fromDouble :: Double -> Concolic RegVal #

toWord64 :: Concolic RegVal -> Word64 #

getType :: Concolic RegVal -> ExtType #

floatToInt :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal) #

intToFloat :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal) #

extendFloat :: Concolic RegVal -> Maybe (Concolic RegVal) #

truncFloat :: Concolic RegVal -> Maybe (Concolic RegVal) #

extend :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal) #

extract :: ExtType -> Concolic RegVal -> Maybe (Concolic RegVal) #

add :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

sub :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

mul :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

div :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

urem :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

srem :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

udiv :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

or :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

xor :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

and :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

neg :: Concolic RegVal -> Maybe (Concolic RegVal) #

sar :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

shr :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

shl :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

eq :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

ne :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

sle :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

slt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

sge :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

sgt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

ule :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

ult :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

uge :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

ugt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

ord :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

unord :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal) #

Storable (Concolic RegVal) (Concolic Word8) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

Methods

toBytes :: Concolic RegVal -> [Concolic Word8] #

fromBytes :: LoadType -> [Concolic Word8] -> Maybe (Concolic RegVal) #

type Rep1 Concolic Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

type Rep1 Concolic = D1 ('MetaData "Concolic" "Language.QBE.Simulator.Concolic.Expression" "qute-symex-0.1.0-BpSHhgkMrEs8e4o3qeYGbi" 'False) (C1 ('MetaCons "Concolic" 'PrefixI 'True) (S1 ('MetaSel ('Just "concrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Just "symbolic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BitVector))))
type Rep (Concolic v) Source # 
Instance details

Defined in Language.QBE.Simulator.Concolic.Expression

type Rep (Concolic v) = D1 ('MetaData "Concolic" "Language.QBE.Simulator.Concolic.Expression" "qute-symex-0.1.0-BpSHhgkMrEs8e4o3qeYGbi" 'False) (C1 ('MetaCons "Concolic" 'PrefixI 'True) (S1 ('MetaSel ('Just "concrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v) :*: S1 ('MetaSel ('Just "symbolic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BitVector))))

hasSymbolic :: Concolic v -> Bool Source #