Safe Haskell	None
Language	Haskell2010

Generic.SymbolicConstituents

Synopsis

data VerificationCondition
- = Precondition SimpleExpr Int SimpleExpr Int
- | Assertion SimpleExpr SimpleExpr Int SimpleExpr Int
- | FunctionConstraint String Word64 [(Register, SimpleExpr)] (Set StatePart)
- | FunctionPointers Word64 IntSet
type VCS = Set VerificationCondition
add_function_pointer :: Word64 -> Key -> (a, Set VerificationCondition) -> (a, Set VerificationCondition)
data SymbolicOperation v
- = SO_Op Opcode Int (Maybe Int) [v]
- | SO_Bit Int v
- | SO_SExtend Int Int v
- | SO_Overwrite Int v v
- | SO_Plus v v
- | SO_Minus v v
- | SO_Times v v
data RegionSize
- = Nat Word64
- | UnknownSize
class (Ord v, Eq v, Show v, Eq p, Ord p, Show p) => SymbolicExecutable ctxt v p | ctxt -> v p where
- sseparate :: ctxt -> String -> p -> RegionSize -> p -> RegionSize -> Bool
- senclosed :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
- salias :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
- ssensitive :: ctxt -> p -> RegionSize -> v -> Bool
- sread_from_ro_data :: ctxt -> p -> RegionSize -> Maybe v
- smk_mem_addresses :: ctxt -> String -> v -> Set p
- sjoin_values :: Foldable t => ctxt -> String -> t v -> v
- swiden_values :: ctxt -> String -> v -> v
- sjoin_pointers :: ctxt -> [p] -> [p]
- top :: ctxt -> String -> v
- ssemantics :: ctxt -> String -> SymbolicOperation v -> v
- sflg_semantics :: ctxt -> v -> Instruction -> FlagStatus -> FlagStatus
- simmediate :: Integral i => ctxt -> i -> v
- smk_init_reg_value :: ctxt -> Register -> v
- smk_init_mem_value :: ctxt -> String -> p -> RegionSize -> v
- scall :: ctxt -> Bool -> Instruction -> State (Sstate v p, VCS) ()
- sjump :: ctxt -> Instruction -> State (Sstate v p, VCS) ()
- stry_jump_targets :: ctxt -> v -> Maybe (Set ResolvedJumpTarget)
- stry_immediate :: ctxt -> v -> Maybe Word64
- stry_deterministic :: ctxt -> v -> Maybe SimpleExpr
- stry_relocation :: ctxt -> p -> RegionSize -> Maybe v
- saddress_has_instruction :: ctxt -> Word64 -> Bool
data Sstate v p = Sstate {
- sregs :: Map Register v
- smem :: Map (p, RegionSize) v
- sflags :: FlagStatus
}
execSstate :: State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
evalSstate :: State (Sstate v p, VCS) a -> Sstate v p -> a
sread_rreg :: SymbolicExecutable ctxt p1 p2 => ctxt -> Register -> (Sstate p1 p3, b) -> p1
sread_reg :: SymbolicExecutable ctxt v p => ctxt -> Register -> State (Sstate v p, VCS) v
swrite_rreg :: SymbolicExecutable ctxt v p => ctxt -> Register -> v -> State (Sstate v p, VCS) ()
soverwrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Bool -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Register -> v -> State (Sstate v p, VCS) ()
sread_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> v -> RegionSize -> State (Sstate v p, VCS) v
sread_mem_from_ptr :: SymbolicExecutable ctxt v p => ctxt -> String -> p -> RegionSize -> State (Sstate v p, VCS) v
swrite_mem :: SymbolicExecutable ctxt v p => ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem_to_ptr :: SymbolicExecutable ctxt v p => ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) ()
sresolve_address :: SymbolicExecutable ctxt v p => ctxt -> Address -> State (Sstate v p, VCS) v
sread_operand :: SymbolicExecutable ctxt v p => ctxt -> String -> Operand -> State (Sstate v p, VCS) v
swrite_operand :: SymbolicExecutable ctxt v p => ctxt -> Bool -> Operand -> v -> State (Sstate v p, VCS) ()
swrite_flags :: SymbolicExecutable ctxt v p => ctxt -> v -> Instruction -> State (Sstate v p, VCS) ()
clean_flg :: StatePart -> FlagStatus -> FlagStatus
add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus
sreturn :: SymbolicExecutable ctxt v p => ctxt -> State (Sstate v p, VCS) ()
slea :: SymbolicExecutable ctxt v p => ctxt -> AddressWord64 -> Operand -> Operand -> State (Sstate v p, VCS) ()
smov :: SymbolicExecutable ctxt v p => ctxt -> a -> Instruction -> State (Sstate v p, VCS) ()
sgeneric_cinstr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) ()
operand_size :: HasSize a => GenericOperand a -> Int
maybe_operand_size :: HasSize storage => [GenericOperand storage] -> Maybe Int
sexec_cinstr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) ()
sset_rip :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_block :: SymbolicExecutable ctxt v p => ctxt -> [GenericInstruction AddressWord64 Register Prefix Opcode Int] -> Maybe [GenericInstruction AddressWord64 Register Prefix Opcode Int] -> Sstate v p -> (Sstate v p, Set VerificationCondition)
sjoin_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, RegionSize) v
sjoin_states :: forall v p1 ctxt p2. (SymbolicExecutable ctxt v p1, SymbolicExecutable ctxt v p2) => ctxt -> [Char] -> Sstate v p1 -> Sstate v p1 -> Sstate v p1
supremum :: SymbolicExecutable ctxt v p => ctxt -> [Sstate v p] -> Sstate v p
simplies :: SymbolicExecutable ctxt v p => ctxt -> Sstate v p -> Sstate v p -> Bool

Documentation

data VerificationCondition Source #

A verification condition is either: * A precondition of the form: > Precondition (a0,si0) (a1,si1) This formulates that at the initial state the two regions must be separate. * An assertion of the form: > Assertion a (a0,si0) (a1,si1) This formulates that dynamically, whenever address a is executed, the two regions are asserted to be separate. * A function constraint of the form: > FunctionConstraint foo [(RDI, v0), (RSI, v1), ...] { sp0,sp1,... } This formulates that a function call to function foo with values v0, v1, ... stored in the registers should not overwrite certain state parts.

Constructors

Precondition SimpleExpr Int SimpleExpr Int	Precondition: lhs SEP rhs
Assertion SimpleExpr SimpleExpr Int SimpleExpr Int	Assertion: @address, lhs SEP rhs
FunctionConstraint String Word64 [(Register, SimpleExpr)] (Set StatePart)	Function name, address, of call, with param registers
FunctionPointers Word64 IntSet	A set of function pointers passed to a function

Instances

Instances details

Eq VerificationCondition Source #
Instance details Defined in Generic.SymbolicConstituents Methods (==) :: VerificationCondition -> VerificationCondition -> Bool # (/=) :: VerificationCondition -> VerificationCondition -> Bool #
Ord VerificationCondition Source #
Instance details Defined in Generic.SymbolicConstituents Methods compare :: VerificationCondition -> VerificationCondition -> Ordering # (<) :: VerificationCondition -> VerificationCondition -> Bool # (<=) :: VerificationCondition -> VerificationCondition -> Bool # (>) :: VerificationCondition -> VerificationCondition -> Bool # (>=) :: VerificationCondition -> VerificationCondition -> Bool # max :: VerificationCondition -> VerificationCondition -> VerificationCondition # min :: VerificationCondition -> VerificationCondition -> VerificationCondition #
Show VerificationCondition Source #
Instance details Defined in Analysis.Context Methods showsPrec :: Int -> VerificationCondition -> ShowS # show :: VerificationCondition -> String # showList :: [VerificationCondition] -> ShowS #
Generic VerificationCondition Source #
Instance details Defined in Generic.SymbolicConstituents Associated Types type Rep VerificationCondition :: Type -> Type # Methods from :: VerificationCondition -> Rep VerificationCondition x # to :: Rep VerificationCondition x -> VerificationCondition #
Serialize VerificationCondition Source #
Instance details Defined in Analysis.Context Methods put :: Putter VerificationCondition # get :: Get VerificationCondition #
NFData VerificationCondition Source #
Instance details Defined in Analysis.Context Methods rnf :: VerificationCondition -> () #
type Rep VerificationCondition Source #
Instance details Defined in Generic.SymbolicConstituents type Rep VerificationCondition = D1 ('MetaData "VerificationCondition" "Generic.SymbolicConstituents" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) ((C1 ('MetaCons "Precondition" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SimpleExpr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SimpleExpr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: C1 ('MetaCons "Assertion" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SimpleExpr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SimpleExpr)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SimpleExpr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :+: (C1 ('MetaCons "FunctionConstraint" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Register, SimpleExpr)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set StatePart)))) :+: C1 ('MetaCons "FunctionPointers" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IntSet))))

type VCS = Set VerificationCondition Source #

An acornym for a set of verification conditions

add_function_pointer :: Word64 -> Key -> (a, Set VerificationCondition) -> (a, Set VerificationCondition) Source #

Add a function_pointer_intro to the given symbolic predicate

data SymbolicOperation v Source #

Constructors

SO_Op Opcode Int (Maybe Int) [v]
SO_Bit Int v
SO_SExtend Int Int v
SO_Overwrite Int v v
SO_Plus v v
SO_Minus v v
SO_Times v v

data RegionSize Source #

Constructors

Nat Word64
UnknownSize

Instances

Instances details

Eq RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Methods (==) :: RegionSize -> RegionSize -> Bool # (/=) :: RegionSize -> RegionSize -> Bool #
Ord RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Methods compare :: RegionSize -> RegionSize -> Ordering # (<) :: RegionSize -> RegionSize -> Bool # (<=) :: RegionSize -> RegionSize -> Bool # (>) :: RegionSize -> RegionSize -> Bool # (>=) :: RegionSize -> RegionSize -> Bool # max :: RegionSize -> RegionSize -> RegionSize # min :: RegionSize -> RegionSize -> RegionSize #
Show RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Methods showsPrec :: Int -> RegionSize -> ShowS # show :: RegionSize -> String # showList :: [RegionSize] -> ShowS #
Generic RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Associated Types type Rep RegionSize :: Type -> Type # Methods from :: RegionSize -> Rep RegionSize x # to :: Rep RegionSize x -> RegionSize #
Serialize RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Methods put :: Putter RegionSize # get :: Get RegionSize #
NFData RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents Methods rnf :: RegionSize -> () #
type Rep RegionSize Source #
Instance details Defined in Generic.SymbolicConstituents type Rep RegionSize = D1 ('MetaData "RegionSize" "Generic.SymbolicConstituents" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Nat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64)) :+: C1 ('MetaCons "UnknownSize" 'PrefixI 'False) (U1 :: Type -> Type))

class (Ord v, Eq v, Show v, Eq p, Ord p, Show p) => SymbolicExecutable ctxt v p | ctxt -> v p where Source #

Methods

sseparate :: ctxt -> String -> p -> RegionSize -> p -> RegionSize -> Bool Source #

senclosed :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool Source #

salias :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool Source #

ssensitive :: ctxt -> p -> RegionSize -> v -> Bool Source #

sread_from_ro_data :: ctxt -> p -> RegionSize -> Maybe v Source #

smk_mem_addresses :: ctxt -> String -> v -> Set p Source #

sjoin_values :: Foldable t => ctxt -> String -> t v -> v Source #

swiden_values :: ctxt -> String -> v -> v Source #

sjoin_pointers :: ctxt -> [p] -> [p] Source #

top :: ctxt -> String -> v Source #

ssemantics :: ctxt -> String -> SymbolicOperation v -> v Source #

sflg_semantics :: ctxt -> v -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => ctxt -> i -> v Source #

smk_init_reg_value :: ctxt -> Register -> v Source #

smk_init_mem_value :: ctxt -> String -> p -> RegionSize -> v Source #

scall :: ctxt -> Bool -> Instruction -> State (Sstate v p, VCS) () Source #

sjump :: ctxt -> Instruction -> State (Sstate v p, VCS) () Source #

stry_jump_targets :: ctxt -> v -> Maybe (Set ResolvedJumpTarget) Source #

stry_immediate :: ctxt -> v -> Maybe Word64 Source #

stry_deterministic :: ctxt -> v -> Maybe SimpleExpr Source #

stry_relocation :: ctxt -> p -> RegionSize -> Maybe v Source #

saddress_has_instruction :: ctxt -> Word64 -> Bool Source #

Instances

Instances details

SymbolicExecutable FContext SValue SPointer Source #

Instance details

Defined in Instantiation.SymbolicPropagation

Methods

sseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

senclosed :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

salias :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool Source #

sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

smk_mem_addresses :: FContext -> String -> SValue -> Set SPointer Source #

sjoin_values :: Foldable t => FContext -> String -> t SValue -> SValue Source #

swiden_values :: FContext -> String -> SValue -> SValue Source #

sjoin_pointers :: FContext -> [SPointer] -> [SPointer] Source #

top :: FContext -> String -> SValue Source #

ssemantics :: FContext -> String -> SymbolicOperation SValue -> SValue Source #

sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => FContext -> i -> SValue Source #

smk_init_reg_value :: FContext -> Register -> SValue Source #

smk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue Source #

scall :: FContext -> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

stry_immediate :: FContext -> SValue -> Maybe Word64 Source #

stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr Source #

stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

saddress_has_instruction :: FContext -> Word64 -> Bool Source #

data Sstate v p Source #

Constructors

Sstate
Fields sregs :: Map Register v smem :: Map (p, RegionSize) v sflags :: FlagStatus

Instances

Instances details

Propagator FContext Predicate Source #
Instance details Defined in Instantiation.SymbolicPropagation Methods tau :: FContext -> [Instruction] -> Maybe [Instruction] -> Predicate -> (Predicate, Set VerificationCondition) Source # join :: FContext -> String -> Predicate -> Predicate -> Predicate Source # implies :: FContext -> Predicate -> Predicate -> Bool Source #
(Eq v, Eq p) => Eq (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Methods (==) :: Sstate v p -> Sstate v p -> Bool # (/=) :: Sstate v p -> Sstate v p -> Bool #
(Ord v, Ord p) => Ord (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Methods compare :: Sstate v p -> Sstate v p -> Ordering # (<) :: Sstate v p -> Sstate v p -> Bool # (<=) :: Sstate v p -> Sstate v p -> Bool # (>) :: Sstate v p -> Sstate v p -> Bool # (>=) :: Sstate v p -> Sstate v p -> Bool # max :: Sstate v p -> Sstate v p -> Sstate v p # min :: Sstate v p -> Sstate v p -> Sstate v p #
(Show v, Show p) => Show (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Methods showsPrec :: Int -> Sstate v p -> ShowS # show :: Sstate v p -> String # showList :: [Sstate v p] -> ShowS #
Generic (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Associated Types type Rep (Sstate v p) :: Type -> Type # Methods from :: Sstate v p -> Rep (Sstate v p) x # to :: Rep (Sstate v p) x -> Sstate v p #
(Ord v, Serialize v, Ord p, Serialize p) => Serialize (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Methods put :: Putter (Sstate v p) # get :: Get (Sstate v p) #
(NFData v, NFData p) => NFData (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents Methods rnf :: Sstate v p -> () #
type Rep (Sstate v p) Source #
Instance details Defined in Generic.SymbolicConstituents type Rep (Sstate v p) = D1 ('MetaData "Sstate" "Generic.SymbolicConstituents" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Sstate" 'PrefixI 'True) (S1 ('MetaSel ('Just "sregs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Register v)) :: (S1 ('MetaSel ('Just "smem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (p, RegionSize) v)) :: S1 ('MetaSel ('Just "sflags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FlagStatus))))

execSstate :: State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p Source #

evalSstate :: State (Sstate v p, VCS) a -> Sstate v p -> a Source #

sread_rreg :: SymbolicExecutable ctxt p1 p2 => ctxt -> Register -> (Sstate p1 p3, b) -> p1 Source #

Read from a register

sread_reg :: SymbolicExecutable ctxt v p => ctxt -> Register -> State (Sstate v p, VCS) v Source #

swrite_rreg :: SymbolicExecutable ctxt v p => ctxt -> Register -> v -> State (Sstate v p, VCS) () Source #

Write to a register

soverwrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Bool -> Register -> v -> State (Sstate v p, VCS) () Source #

swrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Register -> v -> State (Sstate v p, VCS) () Source #

sread_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> v -> RegionSize -> State (Sstate v p, VCS) v Source #

Read from memory

sread_mem_from_ptr :: SymbolicExecutable ctxt v p => ctxt -> String -> p -> RegionSize -> State (Sstate v p, VCS) v Source #

swrite_mem :: SymbolicExecutable ctxt v p => ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) () Source #

Write to memory

swrite_mem_to_ptr :: SymbolicExecutable ctxt v p => ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) () Source #

sresolve_address :: SymbolicExecutable ctxt v p => ctxt -> Address -> State (Sstate v p, VCS) v Source #

Given the address of an operand of an instruction, resolve it given the current state.

sread_operand :: SymbolicExecutable ctxt v p => ctxt -> String -> Operand -> State (Sstate v p, VCS) v Source #

swrite_operand :: SymbolicExecutable ctxt v p => ctxt -> Bool -> Operand -> v -> State (Sstate v p, VCS) () Source #

swrite_flags :: SymbolicExecutable ctxt v p => ctxt -> v -> Instruction -> State (Sstate v p, VCS) () Source #

clean_flg :: StatePart -> FlagStatus -> FlagStatus Source #

add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus Source #

sreturn :: SymbolicExecutable ctxt v p => ctxt -> State (Sstate v p, VCS) () Source #

slea :: SymbolicExecutable ctxt v p => ctxt -> AddressWord64 -> Operand -> Operand -> State (Sstate v p, VCS) () Source #

smov :: SymbolicExecutable ctxt v p => ctxt -> a -> Instruction -> State (Sstate v p, VCS) () Source #

sgeneric_cinstr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) () Source #

operand_size :: HasSize a => GenericOperand a -> Int Source #

maybe_operand_size :: HasSize storage => [GenericOperand storage] -> Maybe Int Source #

sexec_cinstr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) () Source #

sset_rip :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) () Source #

sexec_instr :: SymbolicExecutable ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS) () Source #

sexec_block :: SymbolicExecutable ctxt v p => ctxt -> [GenericInstruction AddressWord64 Register Prefix Opcode Int] -> Maybe [GenericInstruction AddressWord64 Register Prefix Opcode Int] -> Sstate v p -> (Sstate v p, Set VerificationCondition) Source #

sjoin_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, RegionSize) v Source #

sjoin_states :: forall v p1 ctxt p2. (SymbolicExecutable ctxt v p1, SymbolicExecutable ctxt v p2) => ctxt -> [Char] -> Sstate v p1 -> Sstate v p1 -> Sstate v p1 Source #

supremum :: SymbolicExecutable ctxt v p => ctxt -> [Sstate v p] -> Sstate v p Source #

The supremum of a list of predicates

simplies :: SymbolicExecutable ctxt v p => ctxt -> Sstate v p -> Sstate v p -> Bool Source #