| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
WithAbstractSymbolicValues.SymbolicExecution
Synopsis
- add_function_pointer :: Ord v => Word64 -> Key -> (a, Set (VerificationCondition v)) -> (a, Set (VerificationCondition v))
- add_pa_result :: Ord v => Word64 -> PointerAnalysisResult v -> (a, Set (VerificationCondition v)) -> (a, Set (VerificationCondition v))
- sresolve_address :: WithAbstractSymbolicValues ctxt v p => ctxt -> Operand -> State (Sstate v p, VCS v) v
- add_base_displ :: (Integral a, WithAbstractSymbolicValues ctxt a p) => ctxt -> Register -> a -> StateT (Sstate a p, VCS a) Identity a
- sread_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
- swrite_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Bool -> Operand -> v -> State (Sstate v p, VCS v) ()
- add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus
- sreturn :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- slea :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Operand -> Operand -> State (Sstate v p, VCS v) ()
- smov :: WithAbstractSymbolicValues ctxt v p => ctxt -> a -> Instruction -> State (Sstate v p, VCS v) ()
- sgeneric_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- maybe_operand_size :: [Operand] -> Maybe ByteSize
- sexec_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- sset_rip :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) ()
- sexec_instr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) ()
- sexec_block :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p, VCS v) ()
- sjoin_mem :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, Maybe ByteSize) v
- sjoin_regs :: WithAbstractSymbolicValues ctxt v p => ctxt -> Map Register v -> Map Register v -> Map Register v
- sjoin_states :: WithAbstractSymbolicValues p v p => p -> [Char] -> Sstate v p -> Sstate v p -> Sstate v p
- supremum :: WithAbstractSymbolicValues ctxt v p => ctxt -> [Sstate v p] -> Sstate v p
- simplies :: WithAbstractSymbolicValues p v p => p -> Sstate v p -> Sstate v p -> Bool
- sverify_postcondition :: WithAbstractSymbolicValues ctxt v p => ctxt -> Sstate v p -> Bool
Documentation
add_function_pointer :: Ord v => Word64 -> Key -> (a, Set (VerificationCondition v)) -> (a, Set (VerificationCondition v)) Source #
Add a function_pointer_intro to the given symbolic predicate
add_pa_result :: Ord v => Word64 -> PointerAnalysisResult v -> (a, Set (VerificationCondition v)) -> (a, Set (VerificationCondition v)) Source #
sresolve_address :: WithAbstractSymbolicValues ctxt v p => ctxt -> Operand -> State (Sstate v p, VCS v) v Source #
Given the address of an operand of an instruction, resolve it given the current state.
add_base_displ :: (Integral a, WithAbstractSymbolicValues ctxt a p) => ctxt -> Register -> a -> StateT (Sstate a p, VCS a) Identity a Source #
sread_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Operand -> State (Sstate v p, VCS v) v Source #
swrite_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Bool -> Operand -> v -> State (Sstate v p, VCS v) () Source #
add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus Source #
sreturn :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) () Source #
slea :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Operand -> Operand -> State (Sstate v p, VCS v) () Source #
smov :: WithAbstractSymbolicValues ctxt v p => ctxt -> a -> Instruction -> State (Sstate v p, VCS v) () Source #
sgeneric_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) () Source #
sexec_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) () Source #
sset_rip :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p, VCS v) () Source #
sexec_instr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) () Source #
sexec_block :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p, VCS v) () Source #
sjoin_mem :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, Maybe ByteSize) v Source #
sjoin_regs :: WithAbstractSymbolicValues ctxt v p => ctxt -> Map Register v -> Map Register v -> Map Register v Source #
sjoin_states :: WithAbstractSymbolicValues p v p => p -> [Char] -> Sstate v p -> Sstate v p -> Sstate v p Source #
supremum :: WithAbstractSymbolicValues ctxt v p => ctxt -> [Sstate v p] -> Sstate v p Source #
The supremum of a list of predicates
sverify_postcondition :: WithAbstractSymbolicValues ctxt v p => ctxt -> Sstate v p -> Bool Source #