| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Tokstyle.C.Analysis.Interval
Description
Interval analysis of the integer values in a function.
Each value is a set of ranges, and each range remembers whether arithmetic that wrapped around its type produced it. Branch conditions narrow the ranges of the locals and fields they test.
The analysis assumes that unsigned values of 64 bits stay below 2^63, and that a function a local's address is passed to doesn't keep the address.
Synopsis
- data IntTy = IntTy {}
- intTy :: Bool -> Integer -> IntTy
- data Origin
- data Range = Range {}
- wrapSite :: Origin -> Maybe NodeInfo
- data Linear = Linear {}
- atMost :: Facts -> [(Integer, Term)] -> Integer -> Linear -> Bool
- exactSum :: Facts -> Term -> Maybe Linear
- anySum :: Facts -> Term -> Maybe Linear
- pathSum :: Facts -> AccessPath -> IntTy -> Linear
- constantSum :: Integer -> Linear
- plus :: Linear -> Linear -> Linear
- scale :: Integer -> Linear -> Linear
- times :: Linear -> Linear -> Maybe Linear
- data Term = Term {}
- data TermKind
- data Facts = Facts {
- factsChanges :: Int
- factsBackEdge :: Bool
- factsValues :: Map AccessPath (IntTy, [Range])
- factsDiffs :: Map (AccessPath, AccessPath) Integer
- data Fact
- data Program = Program {
- progFields :: Map FieldKey [Range]
- progReturns :: Map String [Range]
- progParams :: Map String [Maybe [Range]]
- progReaches :: Map String [Reach]
- emptyProgram :: Program
- data Function
- translate :: MonadTrav m => FilePath -> [IdentDecl] -> FunDef -> m Function
- solveFunction :: Program -> Function -> [(Node, Facts, [Term])]
- dependsOn :: Program -> Function -> Bool
- canWrap :: FunDef -> Bool
- eval :: Facts -> Term -> Maybe [Range]
- assume :: Bool -> Term -> Facts -> Maybe Facts
- effects :: Bool -> Term -> Facts -> Facts
- subTerms :: Term -> [Term]
- subTermsWith :: Facts -> Term -> [(Facts, Term)]
- normalise :: [Range] -> [Range]
- convert :: NodeInfo -> IntTy -> Range -> [Range]
- intType :: Type -> Maybe IntTy
Documentation
Constructors
| IntTy | |
Where the values in a range come from.
Constructors
| Plain | Any value of the type, or a constant. |
| Reduced | An index reduced with |
| Arith | Arithmetic, which may leave the type's range. |
| Wrapped NodeInfo | Arithmetic that went below zero and wrapped around to the top of an unsigned type's range, at the given expression. |
| Overflowed NodeInfo | Arithmetic that went past the top of an unsigned type's range and wrapped around to zero, at the given expression. |
Instances
wrapSite :: Origin -> Maybe NodeInfo Source #
Where arithmetic that produced values wrapped around, either way.
A sum of paths, each times a coefficient, and a constant.
atMost :: Facts -> [(Integer, Term)] -> Integer -> Linear -> Bool Source #
Whether the sum of some terms, each times a coefficient, and a constant is always at most a sum, by how the paths they read relate, or by the values of those paths.
exactSum :: Facts -> Term -> Maybe Linear Source #
A term as a sum, where computing each part doesn't wrap around, as its type holds all the values the paths in it give it.
anySum :: Facts -> Term -> Maybe Linear Source #
A term as a sum, even where computing it can wrap around.
pathSum :: Facts -> AccessPath -> IntTy -> Linear Source #
A path as a sum, with the values the facts know it has, or any of its type's.
constantSum :: Integer -> Linear Source #
times :: Linear -> Linear -> Maybe Linear Source #
The product of two sums, if one of them is a constant.
Constructors
| TConst Integer | |
| TLoad AccessPath | |
| TBin CBinaryOp Term Term | |
| TUnary CUnaryOp Term | |
| TCast Term | |
| TCond Term (Maybe Term) Term | |
| TAssign (Maybe AccessPath) CAssignOp Term Term | |
| TIndex Term Term (Maybe Integer) | An array access, with the array's length if it is known. |
| TCall Term [Term] | |
| TOther [Term] | |
| TUnknown | An expression the analysis doesn't model, which may change anything. |
The values of the locals and fields known at a point in a function. A path that isn't in the map can have any value of its type.
Constructors
| Facts | |
Fields
| |
What the program as a whole knows about a term: the values of the field it reads, or what the function it calls returns and how far it reaches into its arguments.
What is known about the program as a whole.
Constructors
| Program | |
Fields
| |
A function as the analysis sees it: its control flow graph and the terms each node evaluates.
translate :: MonadTrav m => FilePath -> [IdentDecl] -> FunDef -> m Function Source #
A function in a translation unit, given the declarations of its locals.
solveFunction :: Program -> Function -> [(Node, Facts, [Term])] Source #
The facts before each reachable node of a function, with the terms the node evaluates, given what is known about the program.
dependsOn :: Program -> Function -> Bool Source #
Whether what is known about the program says more about a function than knowing nothing about it.
canWrap :: FunDef -> Bool Source #
Whether a function does anything that can make a value wrap around below zero: subtract, decrement or negate. Values from the rest of the program never come wrapped, so only these can.
assume :: Bool -> Term -> Facts -> Maybe Facts Source #
The facts on the paths where a condition has the given truth value, or
Nothing if it can't have it.
effects :: Bool -> Term -> Facts -> Facts Source #
What evaluating a term does to the facts. Writes that only happen on some paths through the term forget the paths they write.
subTermsWith :: Facts -> Term -> [(Facts, Term)] Source #
Each term within a term, with the facts where it is evaluated. The right
operand of && or || and the branches of ?: are only evaluated where
what comes before them has the value that leads to them.
normalise :: [Range] -> [Range] Source #
Sorts ranges and merges those that overlap and come from the same place. Ranges that come from different places can overlap.