| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Tokstyle.Analysis.Symbolic
Synopsis
- data SVal
- data Constraint
- data SState = SState {}
- emptyState :: SState
- assign :: AccessPath -> SVal -> SState -> SState
- addConstraint :: Constraint -> SState -> SState
- canBeNull :: (SVal -> Bool) -> SVal -> SState -> Bool
- merge :: (SVal -> Bool) -> Maybe SVal -> SState -> SState -> SState
- negateConstraint :: Constraint -> Constraint
- sIte :: SVal -> SVal -> SVal -> SVal
- sBinOp :: BinaryOp -> SVal -> SVal -> SVal
- sUnaryOp :: UnaryOp -> SVal -> SVal
- sVar :: AccessPath -> SVal
- sAddr :: AccessPath -> SVal
- valDepth :: SVal -> Int
- lookupStore :: AccessPath -> SState -> Maybe SVal
Documentation
A Symbolic Value represents the result of an expression.
Constructors
| STop | Unknown value |
| SVar AccessPath | Initial value of a path |
| SAddr AccessPath | The address of a memory location (e.g. &a, or a literal string) |
| SNull | Literal NULL 0 nullptr |
| SBinOp BinaryOp SVal SVal | |
| SUnaryOp UnaryOp SVal | |
| SIte SVal SVal SVal | If-Then-Else (Phi node) |
data Constraint Source #
A constraint on symbolic values.
Instances
| Eq Constraint Source # | |
Defined in Tokstyle.Analysis.Symbolic | |
| Ord Constraint Source # | |
Defined in Tokstyle.Analysis.Symbolic Methods compare :: Constraint -> Constraint -> Ordering # (<) :: Constraint -> Constraint -> Bool # (<=) :: Constraint -> Constraint -> Bool # (>) :: Constraint -> Constraint -> Bool # (>=) :: Constraint -> Constraint -> Bool # max :: Constraint -> Constraint -> Constraint # min :: Constraint -> Constraint -> Constraint # | |
| Show Constraint Source # | |
Defined in Tokstyle.Analysis.Symbolic Methods showsPrec :: Int -> Constraint -> ShowS # show :: Constraint -> String # showList :: [Constraint] -> ShowS # | |
The symbolic state at a point in the program.
Constructors
| SState | |
Fields
| |
emptyState :: SState Source #
assign :: AccessPath -> SVal -> SState -> SState Source #
Assign a value to a path, and handle invalidation of dependent paths.
addConstraint :: Constraint -> SState -> SState Source #
Add a new constraint to the state, with basic simplification.
canBeNull :: (SVal -> Bool) -> SVal -> SState -> Bool Source #
Solver: check if a value is known to be non-null. Takes a predicate to check if an initial SVar is known to be non-null (e.g. from declarations).
merge :: (SVal -> Bool) -> Maybe SVal -> SState -> SState -> SState Source #
Merge two symbolic states. If a condition is provided, differing values are merged into an SIte (Phi node). Otherwise, they are merged into an SIte with an inferred condition if possible, or STop (unknown) if no condition can be inferred. We also preserve non-nullness: if a path is non-null in both branches, the merged value is constrained to be non-null.
sVar :: AccessPath -> SVal Source #
sAddr :: AccessPath -> SVal Source #
lookupStore :: AccessPath -> SState -> Maybe SVal Source #