{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Strict     #-}
-- | 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.
module Tokstyle.C.Analysis.Interval
    ( IntTy (..)
    , intTy
    , Origin (..)
    , Range (..)
    , wrapSite
    , Linear (..)
    , atMost
    , exactSum
    , anySum
    , pathSum
    , constantSum
    , plus
    , scale
    , times
    , Term (..)
    , TermKind (..)
    , Facts (..)
    , Fact (..)
    , Program (..)
    , emptyProgram
    , Function
    , translate
    , solveFunction
    , dependsOn
    , canWrap
    , eval
    , assume
    , effects
    , subTerms
    , subTermsWith
    , normalise
    , convert
    , intType
    ) where

import           Control.Monad                    (foldM, forM, forM_, join)
import           Data.List                        (sortOn)
import           Data.Map.Strict                  (Map)
import qualified Data.Map.Strict                  as Map
import           Data.Maybe                       (fromMaybe, isJust, isNothing,
                                                   listToMaybe, mapMaybe)
import           Data.Set                         (Set)
import qualified Data.Set                         as Set
import           Language.C.Analysis.AstAnalysis  (defineParams)
import           Language.C.Analysis.ConstEval    (constEval, iSize, intValue)
import           Language.C.Analysis.DeclAnalysis (analyseTypeDecl)
import           Language.C.Analysis.DefTable     (defineScopedIdent)
import           Language.C.Analysis.MachineDescs (x86_64)
import           Language.C.Analysis.SemRep       (ArraySize (..),
                                                   Enumerator (..), FunDef (..),
                                                   FunType (..), IdentDecl (..),
                                                   IntType (..), ParamDecl (..),
                                                   Type (..), TypeName (..),
                                                   VarDecl (..), VarName (..),
                                                   declIdent, declType)
import           Language.C.Analysis.TravMonad    (MonadTrav, catchTravError,
                                                   enterBlockScope,
                                                   enterFunctionScope,
                                                   leaveBlockScope,
                                                   leaveFunctionScope,
                                                   lookupObject, withDefTable)
import           Language.C.Analysis.TypeUtils    (canonicalType)
import           Language.C.Data.Ident            (identToString)
import           Language.C.Data.Name             (Name)
import           Language.C.Data.Node             (NodeInfo, nameOfNode,
                                                   undefNode)
import           Language.C.Syntax.AST
import           Language.C.Syntax.Constants      (getCInteger)
import           Tokstyle.Analysis.AccessPath     (AccessPath (..),
                                                   isPathPrefixOf)
import           Tokstyle.Analysis.Dataflow       (Dataflow (..), solve)
import           Tokstyle.C.Analysis.CFG          (CFG, EdgeType (..),
                                                   Node (..), NodeKind (..),
                                                   endsPath, fromFunDef)
import           Tokstyle.C.Analysis.Known        (Reach (..))
import           Tokstyle.C.Analysis.Syntax       (exprChildren, initExprs,
                                                   localDecls, statExprs)
import           Tokstyle.C.Analysis.Types        (FieldKey, exprType, fieldKey,
                                                   funKey, funType)


data IntTy = IntTy
    { IntTy -> Bool
tySigned :: Bool
    , IntTy -> Integer
tyBits   :: Integer
    , IntTy -> Range
tyRange  :: Range
    -- ^ The values the type can hold.
    }
    deriving (IntTy -> IntTy -> Bool
(IntTy -> IntTy -> Bool) -> (IntTy -> IntTy -> Bool) -> Eq IntTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntTy -> IntTy -> Bool
== :: IntTy -> IntTy -> Bool
$c/= :: IntTy -> IntTy -> Bool
/= :: IntTy -> IntTy -> Bool
Eq, Int -> IntTy -> ShowS
[IntTy] -> ShowS
IntTy -> String
(Int -> IntTy -> ShowS)
-> (IntTy -> String) -> ([IntTy] -> ShowS) -> Show IntTy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntTy -> ShowS
showsPrec :: Int -> IntTy -> ShowS
$cshow :: IntTy -> String
show :: IntTy -> String
$cshowList :: [IntTy] -> ShowS
showList :: [IntTy] -> ShowS
Show)

-- | Where the values in a range come from.
data Origin
    = Plain
    -- ^ Any value of the type, or a constant.
    | Reduced
    -- ^ An index reduced with @%@ or @&@.
    | 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.
    deriving (Origin -> Origin -> Bool
(Origin -> Origin -> Bool)
-> (Origin -> Origin -> Bool) -> Eq Origin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Origin -> Origin -> Bool
== :: Origin -> Origin -> Bool
$c/= :: Origin -> Origin -> Bool
/= :: Origin -> Origin -> Bool
Eq, Int -> Origin -> ShowS
[Origin] -> ShowS
Origin -> String
(Int -> Origin -> ShowS)
-> (Origin -> String) -> ([Origin] -> ShowS) -> Show Origin
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Origin -> ShowS
showsPrec :: Int -> Origin -> ShowS
$cshow :: Origin -> String
show :: Origin -> String
$cshowList :: [Origin] -> ShowS
showList :: [Origin] -> ShowS
Show)

data Range = Range
    { Range -> Integer
lo     :: Integer
    , Range -> Integer
hi     :: Integer
    , Range -> Origin
origin :: Origin
    }
    deriving (Range -> Range -> Bool
(Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
/= :: Range -> Range -> Bool
Eq, Int -> Range -> ShowS
[Range] -> ShowS
Range -> String
(Int -> Range -> ShowS)
-> (Range -> String) -> ([Range] -> ShowS) -> Show Range
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Range -> ShowS
showsPrec :: Int -> Range -> ShowS
$cshow :: Range -> String
show :: Range -> String
$cshowList :: [Range] -> ShowS
showList :: [Range] -> ShowS
Show)

data Term = Term
    { Term -> CExpr
termExpr    :: CExpr
    , Term -> Maybe IntTy
termTy      :: Maybe IntTy
    , Term -> Maybe Fact
termFact    :: Maybe Fact
    , Term -> Maybe [Range]
termDefault :: Maybe [Range]
    -- ^ The values the term can have when nothing else is known about it.
    , Term -> TermKind
termKind    :: TermKind
    }

data TermKind
    = 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.
data Facts = Facts
    { Facts -> Int
factsChanges  :: Int
    , Facts -> Bool
factsBackEdge :: Bool
    -- ^ Whether the facts arrive at a loop head from the end of the loop.
    , Facts -> Map AccessPath (IntTy, [Range])
factsValues   :: Map AccessPath (IntTy, [Range])
    , Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs    :: Map (AccessPath, AccessPath) Integer
    -- ^ For paths @p@ and @q@, the most @p - q@ can be.
    }
    deriving (Facts -> Facts -> Bool
(Facts -> Facts -> Bool) -> (Facts -> Facts -> Bool) -> Eq Facts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Facts -> Facts -> Bool
== :: Facts -> Facts -> Bool
$c/= :: Facts -> Facts -> Bool
/= :: Facts -> Facts -> Bool
Eq)

-- | What a node of the control flow graph evaluates.
data NodeTerms
    = Evaluates [Term]
    | Declares [(AccessPath, IntTy, Maybe Term)] [Term] [Term]
    -- ^ The locals a declaration initialises, the initialisers it evaluates,
    -- and the terms to check, where an integer local's initialiser is an
    -- assignment to the local.
    | Opaque
    -- ^ A statement the graph doesn't model, which may change anything.

intType :: Type -> Maybe IntTy
intType :: Type -> Maybe IntTy
intType Type
ty = case Type -> Type
canonicalType Type
ty of
    DirectType (TyIntegral IntType
TyBool) TypeQuals
_ Attributes
_ -> IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (Bool -> Integer -> IntTy
intTy Bool
False Integer
1)
    DirectType (TyIntegral IntType
it) TypeQuals
_ Attributes
_     -> IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (Bool -> Integer -> IntTy
intTy (IntType -> Bool
isSigned IntType
it) (Integer
8 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* MachineDesc -> IntType -> Integer
iSize MachineDesc
x86_64 IntType
it))
    DirectType (TyEnum EnumTypeRef
_) TypeQuals
_ Attributes
_          -> IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (Bool -> Integer -> IntTy
intTy Bool
True Integer
32)
    Type
_                                  -> Maybe IntTy
forall a. Maybe a
Nothing
  where
    isSigned :: IntType -> Bool
isSigned = (IntType -> [IntType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [IntType
TyUChar, IntType
TyUShort, IntType
TyUInt, IntType
TyUInt128, IntType
TyULong, IntType
TyULLong])

intTy :: Bool -> Integer -> IntTy
intTy :: Bool -> Integer -> IntTy
intTy Bool
True Integer
bits  = Bool -> Integer -> Range -> IntTy
IntTy Bool
True Integer
bits (Integer -> Integer -> Origin -> Range
Range (-(Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
bits Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))) (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
bits Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Origin
Plain)
intTy Bool
False Integer
bits = Bool -> Integer -> Range -> IntTy
IntTy Bool
False Integer
bits (Integer -> Integer -> Origin -> Range
Range Integer
0 (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
bits Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Origin
Plain)

isWrapped :: Origin -> Bool
isWrapped :: Origin -> Bool
isWrapped = \case
    Wrapped NodeInfo
_ -> Bool
True
    Origin
_         -> Bool
False

-- | The values a conversion to an integer type at an expression turns a
-- range into.
convert :: NodeInfo -> IntTy -> Range -> [Range]
convert :: NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
_ t :: IntTy
t@IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
True} Range
r
    | Range -> Integer
lo Range
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Range -> Integer
lo Range
full Bool -> Bool -> Bool
&& Range -> Integer
hi Range
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi Range
full = [Range
r]
    | Bool
otherwise = [Range
full]
  where full :: Range
full = IntTy -> Range
tyRange IntTy
t
convert NodeInfo
site t :: IntTy
t@IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
False} (Range Integer
l Integer
h Origin
o)
    -- Unsigned values of 64 bits count things in memory, which stay below
    -- 2^63, so arithmetic on them doesn't go past the top of their range.
    | IntTy -> Integer
tyBits IntTy
t Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
64, Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
m, Integer
h Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m = NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
site IntTy
t (Integer -> Integer -> Origin -> Range
Range Integer
l (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Origin
o)
    | Integer
h Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m =
        [ Integer -> Integer -> Origin -> Range
Range (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
l (-Integer
m)) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (Integer -> Origin
moved (-Integer
1)) | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 ]
        [Range] -> [Range] -> [Range]
forall a. [a] -> [a] -> [a]
++ [ Integer -> Integer -> Origin -> Range
Range (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
l Integer
0) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
h (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) Origin
o | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
m, Integer
h Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 ]
        [Range] -> [Range] -> [Range]
forall a. [a] -> [a] -> [a]
++ [ Integer -> Integer -> Origin -> Range
Range Integer
0 (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
h Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) (Integer -> Origin
moved Integer
1) | Integer
h Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m ]
    | Integer
ql Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
qh = [Integer -> Integer -> Origin -> Range
Range (Integer
l Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) (Integer
h Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) (Integer -> Origin
moved Integer
ql)]
    | Bool
otherwise = [Integer -> Integer -> Origin -> Range
Range (Integer
l Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (Integer -> Origin
moved Integer
ql), Integer -> Integer -> Origin -> Range
Range Integer
0 (Integer
h Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) (Integer -> Origin
moved Integer
qh)]
  where
    m :: Integer
m = Range -> Integer
hi (IntTy -> Range
tyRange IntTy
t) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    ql :: Integer
ql = Integer
l Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
m
    qh :: Integer
qh = Integer
h Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
m
    moved :: Integer -> Origin
    moved :: Integer -> Origin
moved Integer
q
        | Integer
q Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
|| Origin -> Bool
isWrapped Origin
o = Origin
o
        | Origin
o Origin -> [Origin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Origin
Plain, Origin
Reduced] = Origin
Plain
        | Integer
q Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = NodeInfo -> Origin
Wrapped NodeInfo
site
        | Bool
otherwise = NodeInfo -> Origin
Overflowed NodeInfo
site

-- | Where arithmetic that produced values wrapped around, either way.
wrapSite :: Origin -> Maybe NodeInfo
wrapSite :: Origin -> Maybe NodeInfo
wrapSite = \case
    Wrapped NodeInfo
site    -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just NodeInfo
site
    Overflowed NodeInfo
site -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just NodeInfo
site
    Origin
_               -> Maybe NodeInfo
forall a. Maybe a
Nothing

joinOrigin :: Origin -> Origin -> Origin
joinOrigin :: Origin -> Origin -> Origin
joinOrigin Origin
a Origin
b
    | Origin
a Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
b = Origin
a
    | Origin -> Bool
isWrapped Origin
a = Origin
a
    | Origin -> Bool
isWrapped Origin
b = Origin
b
    | Just NodeInfo
_ <- Origin -> Maybe NodeInfo
wrapSite Origin
a = Origin
a
    | Just NodeInfo
_ <- Origin -> Maybe NodeInfo
wrapSite Origin
b = Origin
b
    | Origin
Arith Origin -> [Origin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Origin
a, Origin
b] = Origin
Arith
    | Bool
otherwise = Origin
Plain

-- | How many ranges from the same place a value keeps before they become one.
maxRanges :: Int
maxRanges :: Int
maxRanges = Int
3

-- | Sorts ranges and merges those that overlap and come from the same place.
-- Ranges that come from different places can overlap.
normalise :: [Range] -> [Range]
normalise :: [Range] -> [Range]
normalise [Range]
rs = ([Range] -> [Range]) -> [[Range]] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Range] -> [Range]
cap ([Range] -> [Range]) -> ([Range] -> [Range]) -> [Range] -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range] -> [Range]
mergeRuns ([Range] -> [Range]) -> ([Range] -> [Range]) -> [Range] -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> Integer) -> [Range] -> [Range]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn Range -> Integer
lo) ([Range] -> [[Range]]
groupByOrigin [Range]
rs)
  where
    groupByOrigin :: [Range] -> [[Range]]
groupByOrigin [Range]
xs = [ [ Range
x | Range
x <- [Range]
xs, Origin -> Maybe Origin
group (Range -> Origin
origin Range
x) Maybe Origin -> Maybe Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Origin
g ] | Maybe Origin
g <- [Maybe Origin] -> [Maybe Origin]
distinct ((Range -> Maybe Origin) -> [Range] -> [Maybe Origin]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> Maybe Origin
group (Origin -> Maybe Origin)
-> (Range -> Origin) -> Range -> Maybe Origin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Origin
origin) [Range]
xs) ]
    -- Values overflow in many places, so they merge whichever it was.
    group :: Origin -> Maybe Origin
group = \case
        Overflowed NodeInfo
_ -> Maybe Origin
forall a. Maybe a
Nothing
        Origin
o            -> Origin -> Maybe Origin
forall a. a -> Maybe a
Just Origin
o
    distinct :: [Maybe Origin] -> [Maybe Origin]
distinct = (Maybe Origin -> [Maybe Origin] -> [Maybe Origin])
-> [Maybe Origin] -> [Maybe Origin] -> [Maybe Origin]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Maybe Origin
x [Maybe Origin]
seen -> if Maybe Origin
x Maybe Origin -> [Maybe Origin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe Origin]
seen then [Maybe Origin]
seen else Maybe Origin
x Maybe Origin -> [Maybe Origin] -> [Maybe Origin]
forall a. a -> [a] -> [a]
: [Maybe Origin]
seen) []
    mergeRuns :: [Range] -> [Range]
mergeRuns (Range
a : Range
b : [Range]
rest)
        | Range -> Integer
lo Range
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi Range
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 = [Range] -> [Range]
mergeRuns (Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
a) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Range -> Integer
hi Range
a) (Range -> Integer
hi Range
b)) (Range -> Origin
origin Range
a) Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rest)
        | Bool
otherwise = Range
a Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range] -> [Range]
mergeRuns (Range
b Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rest)
    mergeRuns [Range]
short = [Range]
short
    cap :: [Range] -> [Range]
cap [Range]
xs
        | [Range] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Range]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxRanges = [[Range] -> Range
hull [Range]
xs]
        | Bool
otherwise = [Range]
xs

hull :: [Range] -> Range
hull :: [Range] -> Range
hull [Range]
xs = Integer -> Integer -> Origin -> Range
Range ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
lo [Range]
xs)) ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
hi [Range]
xs)) ((Origin -> Origin -> Origin) -> [Origin] -> Origin
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Origin -> Origin -> Origin
joinOrigin ((Range -> Origin) -> [Range] -> [Origin]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Origin
origin [Range]
xs))

------------------------------------------------------------------------------
-- Translating expressions

-- | 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.
data Fact = FieldFact FieldKey | CallFact String

-- | What is known about the program as a whole.
data Program = Program
    { Program -> Map FieldKey [Range]
progFields  :: Map FieldKey [Range]
    -- ^ The values each field can have, for the fields the program only
    -- changes in ways the analysis sees.
    , Program -> Map String [Range]
progReturns :: Map String [Range]
    -- ^ The values each function the program defines can return.
    , Program -> Map String [Maybe [Range]]
progParams  :: Map String [Maybe [Range]]
    -- ^ The values each parameter of a static function can have, for the
    -- functions the program only calls directly.
    , Program -> Map String [Reach]
progReaches :: Map String [Reach]
    -- ^ How far each function the program defines can reach into the memory
    -- its pointer parameters point to.
    }
    deriving (Program -> Program -> Bool
(Program -> Program -> Bool)
-> (Program -> Program -> Bool) -> Eq Program
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Program -> Program -> Bool
== :: Program -> Program -> Bool
$c/= :: Program -> Program -> Bool
/= :: Program -> Program -> Bool
Eq)

emptyProgram :: Program
emptyProgram :: Program
emptyProgram = Map FieldKey [Range]
-> Map String [Range]
-> Map String [Maybe [Range]]
-> Map String [Reach]
-> Program
Program Map FieldKey [Range]
forall k a. Map k a
Map.empty Map String [Range]
forall k a. Map k a
Map.empty Map String [Maybe [Range]]
forall k a. Map k a
Map.empty Map String [Reach]
forall k a. Map k a
Map.empty

-- | Where a function is analysed. The locals it can track are its parameters
-- and the locals it declares once, if it never takes their address. The
-- translation unit tells static functions apart.
data Scope = Scope
    { Scope -> Set String
trackable :: Set String
    , Scope -> String
scopeUnit :: FilePath
    }

pathOf :: Scope -> CExpr -> Maybe AccessPath
pathOf :: Scope -> CExpr -> Maybe AccessPath
pathOf Scope
scope = \case
    CVar Ident
i NodeInfo
_ | Ident -> String
identToString Ident
i String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Scope -> Set String
trackable Scope
scope -> AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just (String -> AccessPath
PathVar (Ident -> String
identToString Ident
i))
    CMember CExpr
e Ident
f Bool
True NodeInfo
_ -> AccessPath -> String -> AccessPath
PathField (AccessPath -> String -> AccessPath)
-> (AccessPath -> AccessPath) -> AccessPath -> String -> AccessPath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AccessPath -> AccessPath
PathDeref (AccessPath -> String -> AccessPath)
-> Maybe AccessPath -> Maybe (String -> AccessPath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> Maybe AccessPath
basePath CExpr
e Maybe (String -> AccessPath) -> Maybe String -> Maybe AccessPath
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Maybe String
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> String
identToString Ident
f)
    CMember CExpr
e Ident
f Bool
False NodeInfo
_ -> AccessPath -> String -> AccessPath
PathField (AccessPath -> String -> AccessPath)
-> Maybe AccessPath -> Maybe (String -> AccessPath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope -> CExpr -> Maybe AccessPath
pathOf Scope
scope CExpr
e Maybe (String -> AccessPath) -> Maybe String -> Maybe AccessPath
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Maybe String
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> String
identToString Ident
f)
    CIndex CExpr
e (CConst (CIntConst CInteger
k NodeInfo
_)) NodeInfo
_ -> AccessPath -> String -> AccessPath
PathIndex (AccessPath -> String -> AccessPath)
-> Maybe AccessPath -> Maybe (String -> AccessPath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> Maybe AccessPath
basePath CExpr
e Maybe (String -> AccessPath) -> Maybe String -> Maybe AccessPath
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Maybe String
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> String
forall a. Show a => a -> String
show (CInteger -> Integer
getCInteger CInteger
k))
    CExpr
_ -> Maybe AccessPath
forall a. Maybe a
Nothing
  where
    basePath :: CExpr -> Maybe AccessPath
basePath = \case
        CVar Ident
i NodeInfo
_ -> AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just (String -> AccessPath
PathVar (Ident -> String
identToString Ident
i))
        CExpr
e        -> Scope -> CExpr -> Maybe AccessPath
pathOf Scope
scope CExpr
e

-- | Whether the memory a path names can change behind the function's back.
isMemory :: AccessPath -> Bool
isMemory :: AccessPath -> Bool
isMemory = \case
    PathVar String
_     -> Bool
False
    PathField AccessPath
p String
_ -> AccessPath -> Bool
isMemory AccessPath
p
    AccessPath
_             -> Bool
True

constValue :: MonadTrav m => CExpr -> m (Maybe Integer)
constValue :: forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e = (CExpr -> Maybe Integer
intValue (CExpr -> Maybe Integer) -> m CExpr -> m (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MachineDesc -> Map Ident CExpr -> CExpr -> m CExpr
forall (m :: * -> *).
MonadTrav m =>
MachineDesc -> Map Ident CExpr -> CExpr -> m CExpr
constEval MachineDesc
x86_64 Map Ident CExpr
forall k a. Map k a
Map.empty CExpr
e) m (Maybe Integer)
-> (CError -> m (Maybe Integer)) -> m (Maybe Integer)
forall a. m a -> (CError -> m a) -> m a
forall (m :: * -> *) a.
MonadCError m =>
m a -> (CError -> m a) -> m a
`catchTravError` m (Maybe Integer) -> CError -> m (Maybe Integer)
forall a b. a -> b -> a
const (Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing)

-- | The value of a constant expression, as far as it can be found without
-- evaluating every subexpression again.
literal :: MonadTrav m => CExpr -> m (Maybe Integer)
literal :: forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
literal = \case
    CConst (CIntConst CInteger
i NodeInfo
_) -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (CInteger -> Integer
getCInteger CInteger
i))
    e :: CExpr
e@(CConst CCharConst{}) -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e
    CUnary CUnaryOp
CMinOp CExpr
e NodeInfo
_ -> (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
forall a. Num a => a -> a
negate (Maybe Integer -> Maybe Integer)
-> m (Maybe Integer) -> m (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
literal CExpr
e
    CUnary CUnaryOp
CPlusOp CExpr
e NodeInfo
_ -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
literal CExpr
e
    e :: CExpr
e@CSizeofExpr{} -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e
    e :: CExpr
e@CSizeofType{} -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e
    e :: CExpr
e@CAlignofExpr{} -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e
    e :: CExpr
e@CAlignofType{} -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
e
    CVar Ident
i NodeInfo
_ -> (Ident -> m (Maybe IdentDecl)
forall (m :: * -> *).
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe IdentDecl)
lookupObject Ident
i m (Maybe IdentDecl)
-> (CError -> m (Maybe IdentDecl)) -> m (Maybe IdentDecl)
forall a. m a -> (CError -> m a) -> m a
forall (m :: * -> *) a.
MonadCError m =>
m a -> (CError -> m a) -> m a
`catchTravError` m (Maybe IdentDecl) -> CError -> m (Maybe IdentDecl)
forall a b. a -> b -> a
const (Maybe IdentDecl -> m (Maybe IdentDecl)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IdentDecl
forall a. Maybe a
Nothing)) m (Maybe IdentDecl)
-> (Maybe IdentDecl -> m (Maybe Integer)) -> m (Maybe Integer)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (EnumeratorDef (Enumerator Ident
_ CExpr
v EnumType
_ NodeInfo
_)) -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
v
        Just IdentDecl
d | Ident -> String
identToString Ident
i String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
limits -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> Integer
hi (Range -> Integer) -> (IntTy -> Range) -> IntTy -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntTy -> Range
tyRange (IntTy -> Integer) -> Maybe IntTy -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe IntTy
intType (IdentDecl -> Type
forall n. Declaration n => n -> Type
declType IdentDecl
d))
        Maybe IdentDecl
_ -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
    CExpr
_ -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
  where
    -- The maximum values of the integer types, which tokstyle's own headers
    -- declare as objects of those types.
    limits :: [String]
limits =
        [ String
"UINT8_MAX", String
"INT8_MAX", String
"UINT16_MAX", String
"INT16_MAX"
        , String
"UINT32_MAX", String
"INT32_MAX", String
"UINT64_MAX", String
"INT64_MAX" ]

term :: MonadTrav m => Scope -> CExpr -> m Term
term :: forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope CExpr
e = CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
literal CExpr
e m (Maybe Integer) -> (Maybe Integer -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
v -> do
        Maybe IntTy
ty <- (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> m (Maybe Type) -> m (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe Type)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Type)
exprType CExpr
e
        Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term CExpr
e Maybe IntTy
ty Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (Integer -> TermKind
TConst Integer
v))
    Maybe Integer
Nothing -> do
        TermKind
k <- m TermKind
kind
        Maybe IntTy
ty <- TermKind -> m (Maybe IntTy)
typeOf TermKind
k
        Maybe Fact
fact <- case (Maybe IntTy
ty, CExpr
e) of
            (Just IntTy
_, CMember{}) -> (FieldKey -> Fact) -> Maybe FieldKey -> Maybe Fact
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FieldKey -> Fact
FieldFact (Maybe FieldKey -> Maybe Fact)
-> m (Maybe FieldKey) -> m (Maybe Fact)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe FieldKey)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe FieldKey)
fieldKey CExpr
e
            (Maybe IntTy
_, CCall (CVar Ident
f NodeInfo
_) [CExpr]
_ NodeInfo
_) -> (String -> Fact) -> Maybe String -> Maybe Fact
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Fact
CallFact (Maybe String -> Maybe Fact) -> m (Maybe String) -> m (Maybe Fact)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Ident -> m (Maybe String)
forall (m :: * -> *).
MonadTrav m =>
String -> Ident -> m (Maybe String)
funKey (Scope -> String
scopeUnit Scope
scope) Ident
f
            (Maybe IntTy, CExpr)
_ -> Maybe Fact -> m (Maybe Fact)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Fact
forall a. Maybe a
Nothing
        Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> (TermKind -> Term) -> TermKind -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term CExpr
e Maybe IntTy
ty Maybe Fact
fact Maybe [Range]
forall a. Maybe a
Nothing (TermKind -> m Term) -> TermKind -> m Term
forall a b. (a -> b) -> a -> b
$ case (Scope -> CExpr -> Maybe AccessPath
pathOf Scope
scope CExpr
e, Maybe IntTy
ty) of
            (Just AccessPath
p, Just IntTy
_) -> AccessPath -> TermKind
TLoad AccessPath
p
            (Maybe AccessPath, Maybe IntTy)
_                -> TermKind
k
  where
    sub :: CExpr -> m Term
sub = Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope
    kind :: m TermKind
kind = case CExpr
e of
        CBinary CBinaryOp
op CExpr
a CExpr
b NodeInfo
_ -> CBinaryOp -> Term -> Term -> TermKind
TBin CBinaryOp
op (Term -> Term -> TermKind) -> m Term -> m (Term -> TermKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
a m (Term -> TermKind) -> m Term -> m TermKind
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CExpr -> m Term
sub CExpr
b
        CUnary CUnaryOp
op CExpr
a NodeInfo
_    -> CUnaryOp -> Term -> TermKind
TUnary CUnaryOp
op (Term -> TermKind) -> m Term -> m TermKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
a
        CCast CDeclaration NodeInfo
_ CExpr
a NodeInfo
_      -> Term -> TermKind
TCast (Term -> TermKind) -> m Term -> m TermKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
a
        CCond CExpr
c Maybe CExpr
t CExpr
f NodeInfo
_    -> Term -> Maybe Term -> Term -> TermKind
TCond (Term -> Maybe Term -> Term -> TermKind)
-> m Term -> m (Maybe Term -> Term -> TermKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
c m (Maybe Term -> Term -> TermKind)
-> m (Maybe Term) -> m (Term -> TermKind)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (CExpr -> m Term) -> Maybe CExpr -> m (Maybe Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse CExpr -> m Term
sub Maybe CExpr
t m (Term -> TermKind) -> m Term -> m TermKind
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CExpr -> m Term
sub CExpr
f
        CAssign CAssignOp
op CExpr
l CExpr
r NodeInfo
_ -> Maybe AccessPath -> CAssignOp -> Term -> Term -> TermKind
TAssign (Scope -> CExpr -> Maybe AccessPath
pathOf Scope
scope CExpr
l) CAssignOp
op (Term -> Term -> TermKind) -> m Term -> m (Term -> TermKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
l m (Term -> TermKind) -> m Term -> m TermKind
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CExpr -> m Term
sub CExpr
r
        CIndex CExpr
a CExpr
i NodeInfo
_     -> Term -> Term -> Maybe Integer -> TermKind
TIndex (Term -> Term -> Maybe Integer -> TermKind)
-> m Term -> m (Term -> Maybe Integer -> TermKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
a m (Term -> Maybe Integer -> TermKind)
-> m Term -> m (Maybe Integer -> TermKind)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CExpr -> m Term
sub CExpr
i m (Maybe Integer -> TermKind) -> m (Maybe Integer) -> m TermKind
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
arrayLength CExpr
a
        CCall CExpr
f [CExpr]
args NodeInfo
_   -> Term -> [Term] -> TermKind
TCall (Term -> [Term] -> TermKind) -> m Term -> m ([Term] -> TermKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
f m ([Term] -> TermKind) -> m [Term] -> m TermKind
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> m Term
sub [CExpr]
args
        CComma [CExpr]
es NodeInfo
_      -> [Term] -> TermKind
TOther ([Term] -> TermKind) -> m [Term] -> m TermKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> m Term
sub [CExpr]
es
        CMember CExpr
a Ident
_ Bool
_ NodeInfo
_  -> [Term] -> TermKind
TOther ([Term] -> TermKind) -> (Term -> [Term]) -> Term -> TermKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TermKind) -> m Term -> m TermKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m Term
sub CExpr
a
        CStatExpr{}      -> TermKind -> m TermKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return TermKind
TUnknown
        CExpr
_                -> TermKind -> m TermKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TermKind
TOther [])

    -- The integer type of the expression, from the types of its operands
    -- where C's conversions give it, and from its named declarations.
    typeOf :: TermKind -> m (Maybe IntTy)
typeOf TermKind
k = case (CExpr
e, TermKind
k) of
        (CBinary CBinaryOp
op CExpr
_ CExpr
_ NodeInfo
_, TBin CBinaryOp
_ Term
a Term
b)
            | Just IntTy
x <- Term -> Maybe IntTy
termTy Term
a, Just IntTy
y <- Term -> Maybe IntTy
termTy Term
b -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (CBinaryOp -> IntTy -> IntTy -> IntTy
binaryType CBinaryOp
op IntTy
x IntTy
y))
        (CUnary CUnaryOp
op CExpr
_ NodeInfo
_, TUnary CUnaryOp
_ Term
a)
            | CUnaryOp
op CUnaryOp -> [CUnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CUnaryOp
CMinOp, CUnaryOp
CPlusOp, CUnaryOp
CCompOp], Just IntTy
x <- Term -> Maybe IntTy
termTy Term
a -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (IntTy -> IntTy
promote IntTy
x))
            | CUnaryOp
op CUnaryOp -> [CUnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CUnaryOp
CPreIncOp, CUnaryOp
CPreDecOp, CUnaryOp
CPostIncOp, CUnaryOp
CPostDecOp] -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe IntTy
termTy Term
a)
            | CUnaryOp
op CUnaryOp -> CUnaryOp -> Bool
forall a. Eq a => a -> a -> Bool
== CUnaryOp
CNegOp -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just IntTy
int)
            | CUnaryOp
op CUnaryOp -> CUnaryOp -> Bool
forall a. Eq a => a -> a -> Bool
== CUnaryOp
CAdrOp -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntTy
forall a. Maybe a
Nothing
        (CCast CDeclaration NodeInfo
d CExpr
_ NodeInfo
_, TermKind
_) -> (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> m (Maybe Type) -> m (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CDeclaration NodeInfo -> m (Maybe Type)
forall {m :: * -> *}.
MonadTrav m =>
CDeclaration NodeInfo -> m (Maybe Type)
declaredType CDeclaration NodeInfo
d
        (CCond{}, TCond Term
_ (Just Term
t) Term
f)
            | Just IntTy
x <- Term -> Maybe IntTy
termTy Term
t, Just IntTy
y <- Term -> Maybe IntTy
termTy Term
f -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just (IntTy -> IntTy -> IntTy
usual (IntTy -> IntTy
promote IntTy
x) (IntTy -> IntTy
promote IntTy
y)))
        (CAssign{}, TAssign Maybe AccessPath
_ CAssignOp
_ Term
l Term
_) -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe IntTy
termTy Term
l)
        (CComma{}, TOther ts :: [Term]
ts@(Term
_ : [Term]
_)) -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe IntTy
termTy ([Term] -> Term
forall a. HasCallStack => [a] -> a
last [Term]
ts))
        (CVar Ident
i NodeInfo
_, TermKind
_) -> Ident -> m (Maybe IntTy)
forall {f :: * -> *}.
(MonadCError f, MonadSymtab f) =>
Ident -> f (Maybe IntTy)
objectType Ident
i
        (CCall (CVar Ident
f NodeInfo
_) [CExpr]
_ NodeInfo
_, TermKind
_) -> Ident -> m (Maybe Type)
forall {m :: * -> *}.
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe Type)
declTypeOf Ident
f m (Maybe Type)
-> (Maybe Type -> m (Maybe IntTy)) -> m (Maybe IntTy)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just Type
t | Just FunType
ft <- Type -> Maybe FunType
funType Type
t -> Maybe IntTy -> m (Maybe IntTy)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe IntTy
intType (FunType -> Type
resultType FunType
ft))
            Maybe Type
_                             -> m (Maybe IntTy)
fallback
        (CExpr, TermKind)
_ -> m (Maybe IntTy)
fallback

    fallback :: m (Maybe IntTy)
fallback = (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> m (Maybe Type) -> m (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe Type)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Type)
exprType CExpr
e

    objectType :: Ident -> f (Maybe IntTy)
objectType Ident
i = (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> f (Maybe Type) -> f (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> f (Maybe Type)
forall {m :: * -> *}.
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe Type)
declTypeOf Ident
i

    declTypeOf :: Ident -> m (Maybe Type)
declTypeOf Ident
i = ((IdentDecl -> Type) -> Maybe IdentDecl -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IdentDecl -> Type
forall n. Declaration n => n -> Type
declType (Maybe IdentDecl -> Maybe Type)
-> m (Maybe IdentDecl) -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> m (Maybe IdentDecl)
forall (m :: * -> *).
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe IdentDecl)
lookupObject Ident
i) m (Maybe Type) -> (CError -> m (Maybe Type)) -> m (Maybe Type)
forall a. m a -> (CError -> m a) -> m a
forall (m :: * -> *) a.
MonadCError m =>
m a -> (CError -> m a) -> m a
`catchTravError` m (Maybe Type) -> CError -> m (Maybe Type)
forall a b. a -> b -> a
const (Maybe Type -> m (Maybe Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing)

    resultType :: FunType -> Type
resultType = \case
        FunType Type
rt [ParamDecl]
_ Bool
_       -> Type
rt
        FunTypeIncomplete Type
rt -> Type
rt

    declaredType :: CDeclaration NodeInfo -> m (Maybe Type)
declaredType CDeclaration NodeInfo
d = (Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CDeclaration NodeInfo -> m Type
forall (m :: * -> *).
MonadTrav m =>
CDeclaration NodeInfo -> m Type
analyseTypeDecl CDeclaration NodeInfo
d) m (Maybe Type) -> (CError -> m (Maybe Type)) -> m (Maybe Type)
forall a. m a -> (CError -> m a) -> m a
forall (m :: * -> *) a.
MonadCError m =>
m a -> (CError -> m a) -> m a
`catchTravError` m (Maybe Type) -> CError -> m (Maybe Type)
forall a b. a -> b -> a
const (Maybe Type -> m (Maybe Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing)

    arrayLength :: CExpr -> m (Maybe Integer)
arrayLength CExpr
a = CExpr -> m (Maybe Type)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Type)
exprType CExpr
a m (Maybe Type)
-> (Maybe Type -> m (Maybe Integer)) -> m (Maybe Integer)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (ArrayType Type
_ (ArraySize Bool
_ CExpr
size) TypeQuals
_ Attributes
_) -> CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
size
        Maybe Type
_                                         -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing

int :: IntTy
int :: IntTy
int = Bool -> Integer -> IntTy
intTy Bool
True Integer
32

-- | Type integer promotion gives a value of a type.
promote :: IntTy -> IntTy
promote :: IntTy -> IntTy
promote IntTy
t
    | IntTy -> Integer
tyBits IntTy
t Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
32 = IntTy
int
    | Bool
otherwise = IntTy
t

-- | Type the usual arithmetic conversions give two promoted types.
usual :: IntTy -> IntTy -> IntTy
usual :: IntTy -> IntTy -> IntTy
usual IntTy
a IntTy
b
    | IntTy -> Bool
tySigned IntTy
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== IntTy -> Bool
tySigned IntTy
b = if IntTy -> Integer
tyBits IntTy
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= IntTy -> Integer
tyBits IntTy
b then IntTy
a else IntTy
b
    | Bool
otherwise =
        let (IntTy
u, IntTy
sg) = if IntTy -> Bool
tySigned IntTy
a then (IntTy
b, IntTy
a) else (IntTy
a, IntTy
b)
        in if IntTy -> Integer
tyBits IntTy
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= IntTy -> Integer
tyBits IntTy
sg then IntTy
u else IntTy
sg

binaryType :: CBinaryOp -> IntTy -> IntTy -> IntTy
binaryType :: CBinaryOp -> IntTy -> IntTy -> IntTy
binaryType CBinaryOp
op IntTy
a IntTy
b
    | CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp, CBinaryOp
CEqOp, CBinaryOp
CNeqOp, CBinaryOp
CLndOp, CBinaryOp
CLorOp] = IntTy
int
    | CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CShlOp, CBinaryOp
CShrOp] = IntTy -> IntTy
promote IntTy
a
    | Bool
otherwise = IntTy -> IntTy -> IntTy
usual (IntTy -> IntTy
promote IntTy
a) (IntTy -> IntTy
promote IntTy
b)

subTerms :: Term -> [Term]
subTerms :: Term -> [Term]
subTerms Term
t = Term
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (Term -> [Term]) -> [Term] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [Term]
subTerms (Term -> [Term]
children Term
t)

-- | 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.
subTermsWith :: Facts -> Term -> [(Facts, Term)]
subTermsWith :: Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts Term
t = (Facts
facts, Term
t) (Facts, Term) -> [(Facts, Term)] -> [(Facts, Term)]
forall a. a -> [a] -> [a]
: case Term -> TermKind
termKind Term
t of
    TBin CBinaryOp
CLndOp Term
a Term
b -> Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts Term
a [(Facts, Term)] -> [(Facts, Term)] -> [(Facts, Term)]
forall a. [a] -> [a] -> [a]
++ Bool -> Term -> Term -> [(Facts, Term)]
after Bool
True Term
a Term
b
    TBin CBinaryOp
CLorOp Term
a Term
b -> Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts Term
a [(Facts, Term)] -> [(Facts, Term)] -> [(Facts, Term)]
forall a. [a] -> [a] -> [a]
++ Bool -> Term -> Term -> [(Facts, Term)]
after Bool
False Term
a Term
b
    TCond Term
c Maybe Term
m Term
f     -> Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts Term
c [(Facts, Term)] -> [(Facts, Term)] -> [(Facts, Term)]
forall a. [a] -> [a] -> [a]
++ [(Facts, Term)]
-> (Term -> [(Facts, Term)]) -> Maybe Term -> [(Facts, Term)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Bool -> Term -> Term -> [(Facts, Term)]
after Bool
True Term
c) Maybe Term
m [(Facts, Term)] -> [(Facts, Term)] -> [(Facts, Term)]
forall a. [a] -> [a] -> [a]
++ Bool -> Term -> Term -> [(Facts, Term)]
after Bool
False Term
c Term
f
    TermKind
_               -> (Term -> [(Facts, Term)]) -> [Term] -> [(Facts, Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts) (Term -> [Term]
children Term
t)
  where
    after :: Bool -> Term -> Term -> [(Facts, Term)]
after Bool
truth Term
c Term
x = [(Facts, Term)]
-> (Facts -> [(Facts, Term)]) -> Maybe Facts -> [(Facts, Term)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Facts -> Term -> [(Facts, Term)]
`subTermsWith` Term
x) (Bool -> Term -> Facts -> Maybe Facts
assume Bool
truth Term
c Facts
facts)

------------------------------------------------------------------------------
-- Evaluating terms


-- | The values a term can have, if it is an integer.
eval :: Facts -> Term -> Maybe [Range]
eval :: Facts -> Term -> Maybe [Range]
eval Facts
facts Term
t = do
    IntTy
ty <- Term -> Maybe IntTy
termTy Term
t
    let unknown :: [Range]
unknown = [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [IntTy -> Range
tyRange IntTy
ty] (Term -> Maybe [Range]
termDefault Term
t)
    [Range] -> Maybe [Range]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range] -> Maybe [Range])
-> ([Range] -> [Range]) -> [Range] -> Maybe [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range] -> [Range]
normalise ([Range] -> [Range]) -> ([Range] -> [Range]) -> [Range] -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
site IntTy
ty) ([Range] -> Maybe [Range]) -> [Range] -> Maybe [Range]
forall a b. (a -> b) -> a -> b
$ case Term -> TermKind
termKind Term
t of
        TConst Integer
v -> [Integer -> Integer -> Origin -> Range
Range Integer
v Integer
v Origin
Plain]
        TLoad AccessPath
p -> [Range]
-> ((IntTy, [Range]) -> [Range])
-> Maybe (IntTy, [Range])
-> [Range]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Range]
unknown (IntTy, [Range]) -> [Range]
forall a b. (a, b) -> b
snd (AccessPath
-> Map AccessPath (IntTy, [Range]) -> Maybe (IntTy, [Range])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
p (Facts -> Map AccessPath (IntTy, [Range])
factsValues Facts
facts))
        TBin CBinaryOp
op Term
a Term
b -> [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [Range]
unknown (IntTy -> CBinaryOp -> Term -> Term -> Maybe [Range]
binary IntTy
ty CBinaryOp
op Term
a Term
b)
        TUnary CUnaryOp
op Term
a -> [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [Range]
unknown (CUnaryOp -> Term -> Maybe [Range]
unary CUnaryOp
op Term
a)
        TCast Term
a -> [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [Range]
unknown (Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a)
        TCond Term
_ Maybe Term
m Term
f -> [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [Range]
unknown ([Range] -> [Range] -> [Range]
forall a. [a] -> [a] -> [a]
(++) ([Range] -> [Range] -> [Range])
-> Maybe [Range] -> Maybe ([Range] -> [Range])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Range]
-> (Term -> Maybe [Range]) -> Maybe Term -> Maybe [Range]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Range] -> Maybe [Range]
forall a. a -> Maybe a
Just []) (Facts -> Term -> Maybe [Range]
eval Facts
facts) Maybe Term
m Maybe ([Range] -> [Range]) -> Maybe [Range] -> Maybe [Range]
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
f)
        TAssign Maybe AccessPath
_ CAssignOp
op Term
l Term
r -> [Range] -> Maybe [Range] -> [Range]
forall a. a -> Maybe a -> a
fromMaybe [Range]
unknown (Facts -> NodeInfo -> CAssignOp -> Term -> Term -> Maybe [Range]
assigned Facts
facts NodeInfo
site CAssignOp
op Term
l Term
r)
        TermKind
_ -> [Range]
unknown
  where
    site :: NodeInfo
site = CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation (Term -> CExpr
termExpr Term
t)

    binary :: IntTy -> CBinaryOp -> Term -> Term -> Maybe [Range]
binary IntTy
ty CBinaryOp
op Term
a Term
b
        | CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp, CBinaryOp
CEqOp, CBinaryOp
CNeqOp, CBinaryOp
CLndOp, CBinaryOp
CLorOp] = [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [Integer -> Integer -> Origin -> Range
Range Integer
0 Integer
1 Origin
Plain]
        | Bool
otherwise = do
            [Range]
ra <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a
            [Range]
rb <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
b
            Facts
-> NodeInfo
-> IntTy
-> CBinaryOp
-> [Range]
-> [Range]
-> Term
-> Term
-> Maybe [Range]
arith Facts
facts NodeInfo
site IntTy
ty CBinaryOp
op [Range]
ra [Range]
rb Term
a Term
b

    unary :: CUnaryOp -> Term -> Maybe [Range]
unary CUnaryOp
op Term
a = case CUnaryOp
op of
        CUnaryOp
CMinOp -> (Range -> Range) -> [Range] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\Range
r -> Integer -> Integer -> Origin -> Range
Range (Integer -> Integer
forall a. Num a => a -> a
negate (Range -> Integer
hi Range
r)) (Integer -> Integer
forall a. Num a => a -> a
negate (Range -> Integer
lo Range
r)) (Range -> Range -> Origin
arithOrigin Range
r Range
r)) ([Range] -> [Range]) -> Maybe [Range] -> Maybe [Range]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a
        CUnaryOp
CPlusOp -> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a
        CUnaryOp
CNegOp -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [Integer -> Integer -> Origin -> Range
Range Integer
0 Integer
1 Origin
Plain]
        CUnaryOp
CPreIncOp -> Integer -> Maybe [Range]
step Integer
1
        CUnaryOp
CPreDecOp -> Integer -> Maybe [Range]
step (-Integer
1)
        CUnaryOp
CPostIncOp -> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a
        CUnaryOp
CPostDecOp -> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a
        CUnaryOp
_ -> Maybe [Range]
forall a. Maybe a
Nothing
      where step :: Integer -> Maybe [Range]
step Integer
d = (Range -> Range) -> [Range] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\Range
r -> Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) (Range -> Integer
hi Range
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) (Range -> Range -> Origin
arithOrigin Range
r Range
r)) ([Range] -> [Range]) -> Maybe [Range] -> Maybe [Range]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a

arithOrigin :: Range -> Range -> Origin
arithOrigin :: Range -> Range -> Origin
arithOrigin Range
x Range
y
    | Origin -> Bool
isWrapped (Range -> Origin
origin Range
x) = Range -> Origin
origin Range
x
    | Origin -> Bool
isWrapped (Range -> Origin
origin Range
y) = Range -> Origin
origin Range
y
    | Just NodeInfo
_ <- Origin -> Maybe NodeInfo
wrapSite (Range -> Origin
origin Range
x) = Range -> Origin
origin Range
x
    | Just NodeInfo
_ <- Origin -> Maybe NodeInfo
wrapSite (Range -> Origin
origin Range
y) = Range -> Origin
origin Range
y
    | (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Range -> Bool
constant [Range
x, Range
y] = Origin
Plain
    | Bool
otherwise = Origin
Arith
  where
    constant :: Range -> Bool
constant Range
r = Range -> Integer
lo Range
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Range -> Integer
hi Range
r Bool -> Bool -> Bool
&& Range -> Origin
origin Range
r Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Plain

-- | The ranges arithmetic produces, before converting them to its type.
arith :: Facts -> NodeInfo -> IntTy -> CBinaryOp -> [Range] -> [Range] -> Term -> Term -> Maybe [Range]
arith :: Facts
-> NodeInfo
-> IntTy
-> CBinaryOp
-> [Range]
-> [Range]
-> Term
-> Term
-> Maybe [Range]
arith Facts
facts NodeInfo
site IntTy
ty CBinaryOp
op [Range]
ra [Range]
rb Term
a Term
b = case CBinaryOp
op of
    CBinaryOp
CAddOp -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [ Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Range -> Integer
lo Range
y) (Range -> Integer
hi Range
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Range -> Integer
hi Range
y) (Range -> Range -> Origin
arithOrigin Range
x Range
y) | Range
x <- [Range]
ra, Range
y <- [Range]
rb ]
    CBinaryOp
CSubOp -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just ([Range] -> [Range]
difference [ Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Range -> Integer
hi Range
y) (Range -> Integer
hi Range
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Range -> Integer
lo Range
y) (Range -> Range -> Origin
arithOrigin Range
x Range
y) | Range
x <- [Range]
ra, Range
y <- [Range]
rb ])
    CBinaryOp
CMulOp -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [ Range -> Range -> Range
products Range
x Range
y | Range
x <- [Range]
ra, Range
y <- [Range]
rb ]
    CBinaryOp
CRmdOp -> Maybe Integer
divisor Maybe Integer -> (Integer -> Maybe [Range]) -> Maybe [Range]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Integer
n ->
        if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Integer -> Bool) -> (Range -> Integer) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer
lo) [Range]
ra'
        then [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [Integer -> Integer -> Origin -> Range
Range Integer
0 (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
hi [Range]
ra'))) Origin
Reduced]
        else Maybe [Range]
forall a. Maybe a
Nothing
    CBinaryOp
CDivOp -> Maybe Integer
divisor Maybe Integer -> (Integer -> Maybe [Range]) -> Maybe [Range]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Integer
n ->
        if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
        then [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [ Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
n) (Range -> Integer
hi Range
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
n) (Range -> Origin
origin Range
x) | Range
x <- [Range]
ra' ]
        else Maybe [Range]
forall a. Maybe a
Nothing
    CBinaryOp
CShrOp -> Maybe Integer
divisor Maybe Integer -> (Integer -> Maybe [Range]) -> Maybe [Range]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Integer
n ->
        if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< IntTy -> Integer
tyBits IntTy
ty Bool -> Bool -> Bool
&& (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Integer -> Bool) -> (Range -> Integer) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer
lo) [Range]
ra'
        then [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [ Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n)) (Range -> Integer
hi Range
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n)) (Range -> Origin
origin Range
x) | Range
x <- [Range]
ra' ]
        else Maybe [Range]
forall a. Maybe a
Nothing
    CBinaryOp
CAndOp -> case [ Integer
v | [Range Integer
v Integer
v' Origin
_] <- [[Range]
ra, [Range]
rb], Integer
v Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
v', Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 ] of
        Integer
v : [Integer]
_ -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [Integer -> Integer -> Origin -> Range
Range Integer
0 Integer
v Origin
Reduced]
        []    -> Maybe [Range]
forall a. Maybe a
Nothing
    CBinaryOp
_ -> Maybe [Range]
forall a. Maybe a
Nothing
  where
    -- What is known about how the paths in the operands relate gives bounds
    -- on their difference.
    difference :: [Range] -> [Range]
difference [Range]
rs = case (Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
a, Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
b) of
        (Just (Just AccessPath
p, Integer
ka), Just (Just AccessPath
q, Integer
kb)) ->
            let lower :: Integer
lower = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Range -> Integer
lo ([Range] -> Range
hull [Range]
rs)) (\Integer
c -> Integer
ka Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
kb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c) ((AccessPath, AccessPath)
-> Map (AccessPath, AccessPath) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AccessPath
q, AccessPath
p) (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
facts))
                upper :: Integer
upper = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Range -> Integer
hi ([Range] -> Range
hull [Range]
rs)) (\Integer
c -> Integer
ka Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
kb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c) ((AccessPath, AccessPath)
-> Map (AccessPath, AccessPath) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AccessPath
p, AccessPath
q) (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
facts))
                clipped :: [Range]
clipped = Integer -> Integer -> [Range] -> [Range]
clipRanges Integer
lower Integer
upper [Range]
rs
            in if [Range] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Range]
clipped then [Range]
rs else [Range]
clipped
        (Maybe (Maybe AccessPath, Integer),
 Maybe (Maybe AccessPath, Integer))
_ -> [Range]
rs

    -- Division and shifts work on values converted to the result type.
    ra' :: [Range]
ra' = (Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
site IntTy
ty) [Range]
ra
    divisor :: Maybe Integer
divisor = case Term -> TermKind
termKind Term
b of
        TConst Integer
v -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v
        TermKind
_        -> case Facts -> Term -> Maybe [Range]
eval Facts
facts Term
b of
            Just [Range Integer
v Integer
v' Origin
_] | Integer
v Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
v' -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v
            Maybe [Range]
_                             -> Maybe Integer
forall a. Maybe a
Nothing
    products :: Range -> Range -> Range
products Range
x Range
y =
        let ps :: [Integer]
ps = [ Integer
p Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
q | Integer
p <- [Range -> Integer
lo Range
x, Range -> Integer
hi Range
x], Integer
q <- [Range -> Integer
lo Range
y, Range -> Integer
hi Range
y] ]
        in Integer -> Integer -> Origin -> Range
Range ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
ps) ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
ps) (Range -> Range -> Origin
arithOrigin Range
x Range
y)

-- | The value an assignment at an expression stores.
assigned :: Facts -> NodeInfo -> CAssignOp -> Term -> Term -> Maybe [Range]
assigned :: Facts -> NodeInfo -> CAssignOp -> Term -> Term -> Maybe [Range]
assigned Facts
facts NodeInfo
site CAssignOp
op Term
l Term
r = do
    IntTy
lt <- Term -> Maybe IntTy
termTy Term
l
    [Range]
rr <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
r
    [Range]
vals <- case CAssignOp -> Maybe CBinaryOp
compound CAssignOp
op of
        Maybe CBinaryOp
Nothing -> [Range] -> Maybe [Range]
forall a. a -> Maybe a
Just [Range]
rr
        Just CBinaryOp
bop -> do
            [Range]
rl <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
l
            Facts
-> NodeInfo
-> IntTy
-> CBinaryOp
-> [Range]
-> [Range]
-> Term
-> Term
-> Maybe [Range]
arith Facts
facts NodeInfo
site IntTy
lt CBinaryOp
bop [Range]
rl [Range]
rr Term
l Term
r
    [Range] -> Maybe [Range]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
site IntTy
lt) [Range]
vals)
  where
    compound :: CAssignOp -> Maybe CBinaryOp
compound = \case
        CAssignOp
CAssignOp -> Maybe CBinaryOp
forall a. Maybe a
Nothing
        CAssignOp
CMulAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CMulOp
        CAssignOp
CDivAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CDivOp
        CAssignOp
CRmdAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CRmdOp
        CAssignOp
CAddAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CAddOp
        CAssignOp
CSubAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CSubOp
        CAssignOp
CShlAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CShlOp
        CAssignOp
CShrAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CShrOp
        CAssignOp
CAndAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CAndOp
        CAssignOp
CXorAssOp -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
CXorOp
        CAssignOp
COrAssOp  -> CBinaryOp -> Maybe CBinaryOp
forall a. a -> Maybe a
Just CBinaryOp
COrOp

------------------------------------------------------------------------------
-- Effects

-- | Records the values of a path, keeping how it relates to other paths.
narrowPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts
narrowPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts
narrowPath AccessPath
p IntTy
ty [Range]
v Facts
facts = Facts
facts { factsValues = Map.insert p (ty, v) (factsValues facts) }

-- | Records a write of the values to a path.
setPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath AccessPath
p IntTy
ty [Range]
v Facts
facts = AccessPath -> IntTy -> [Range] -> Facts -> Facts
narrowPath AccessPath
p IntTy
ty [Range]
v (AccessPath -> Facts -> Facts
forget AccessPath
p Facts
facts)

-- | Records a write that adds a constant to a path, which keeps how it relates
-- to other paths.
shiftPath :: AccessPath -> IntTy -> [Range] -> Integer -> Facts -> Facts
shiftPath :: AccessPath -> IntTy -> [Range] -> Integer -> Facts -> Facts
shiftPath AccessPath
p IntTy
ty [Range]
v Integer
d Facts
facts = AccessPath -> IntTy -> [Range] -> Facts -> Facts
narrowPath AccessPath
p IntTy
ty [Range]
v Facts
shifted
  where
    others :: Facts
others = (AccessPath -> Bool) -> Facts -> Facts
forgetWhere (\AccessPath
q -> AccessPath
q AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
/= AccessPath
p Bool -> Bool -> Bool
&& AccessPath -> AccessPath -> Bool
overwrittenBy AccessPath
p AccessPath
q) Facts
facts
    shifted :: Facts
shifted = Facts
others { factsDiffs = Map.mapWithKey move (factsDiffs others) }
    move :: (AccessPath, AccessPath) -> Integer -> Integer
move (AccessPath
a, AccessPath
b) Integer
c
        | AccessPath
a AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
== AccessPath
p = Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d
        | AccessPath
b AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
== AccessPath
p = Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
d
        | Bool
otherwise = Integer
c

-- | Whether writing the first path can change what the second holds: its
-- parts, and memory that may be the same.
overwrittenBy :: AccessPath -> AccessPath -> Bool
overwrittenBy :: AccessPath -> AccessPath -> Bool
overwrittenBy AccessPath
p AccessPath
q = AccessPath
p AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
q Bool -> Bool -> Bool
|| AccessPath -> Bool
isMemory AccessPath
p Bool -> Bool -> Bool
&& AccessPath -> Bool
isMemory AccessPath
q Bool -> Bool -> Bool
&& AccessPath -> AccessPath -> Bool
mayAlias AccessPath
p AccessPath
q
  where
    mayAlias :: AccessPath -> AccessPath -> Bool
mayAlias (PathField AccessPath
_ String
f) (PathField AccessPath
_ String
g) = String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
g
    mayAlias AccessPath
_ AccessPath
_                             = Bool
True

-- | Forgets what is known about a path and what writing it can change.
forget :: AccessPath -> Facts -> Facts
forget :: AccessPath -> Facts -> Facts
forget AccessPath
p = (AccessPath -> Bool) -> Facts -> Facts
forgetWhere (AccessPath -> AccessPath -> Bool
overwrittenBy AccessPath
p)

forgetWhere :: (AccessPath -> Bool) -> Facts -> Facts
forgetWhere :: (AccessPath -> Bool) -> Facts -> Facts
forgetWhere AccessPath -> Bool
gone Facts
facts = Facts
facts
    { factsValues = Map.filterWithKey (\AccessPath
q (IntTy, [Range])
_ -> Bool -> Bool
not (AccessPath -> Bool
gone AccessPath
q)) (factsValues facts)
    , factsDiffs = Map.filterWithKey (\(AccessPath
a, AccessPath
b) Integer
_ -> Bool -> Bool
not (AccessPath -> Bool
gone AccessPath
a Bool -> Bool -> Bool
|| AccessPath -> Bool
gone AccessPath
b)) (factsDiffs facts)
    }

forgetMemory :: Facts -> Facts
forgetMemory :: Facts -> Facts
forgetMemory = (AccessPath -> Bool) -> Facts -> Facts
forgetWhere AccessPath -> Bool
isMemory

forgetAll :: Facts -> Facts
forgetAll :: Facts -> Facts
forgetAll = (AccessPath -> Bool) -> Facts -> Facts
forgetWhere (Bool -> AccessPath -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | Records that @p - q@ is at most a constant, or 'Nothing' if what is known
-- says it can't be.
relate :: AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate :: AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
p AccessPath
q Integer
c Facts
facts
    | AccessPath
p AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
== AccessPath
q = if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts else Maybe Facts
forall a. Maybe a
Nothing
    | Just Integer
c' <- (AccessPath, AccessPath)
-> Map (AccessPath, AccessPath) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AccessPath
q, AccessPath
p) (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
facts), Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Maybe Facts
forall a. Maybe a
Nothing
    | Bool
otherwise = Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts { factsDiffs = Map.insertWith min (p, q) c (factsDiffs facts) }

-- | A term whose value is a path plus a constant, or a constant, computed
-- without wrapping around. A path counts as itself even if its value wrapped.
linear :: Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear :: Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
t = Facts -> Term -> Maybe Linear
exactSum Facts
facts Term
t Maybe Linear
-> (Linear -> Maybe (Maybe AccessPath, Integer))
-> Maybe (Maybe AccessPath, Integer)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Linear Map AccessPath (Integer, Maybe (Integer, Integer))
ps Integer
c) -> case Map AccessPath (Integer, Maybe (Integer, Integer))
-> [(AccessPath, (Integer, Maybe (Integer, Integer)))]
forall k a. Map k a -> [(k, a)]
Map.toList Map AccessPath (Integer, Maybe (Integer, Integer))
ps of
    []            -> (Maybe AccessPath, Integer) -> Maybe (Maybe AccessPath, Integer)
forall a. a -> Maybe a
Just (Maybe AccessPath
forall a. Maybe a
Nothing, Integer
c)
    [(AccessPath
p, (Integer
1, Maybe (Integer, Integer)
_))] -> (Maybe AccessPath, Integer) -> Maybe (Maybe AccessPath, Integer)
forall a. a -> Maybe a
Just (AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just AccessPath
p, Integer
c)
    [(AccessPath, (Integer, Maybe (Integer, Integer)))]
_             -> Maybe (Maybe AccessPath, Integer)
forall a. Maybe a
Nothing

-- | A sum of paths, each times a coefficient, and a constant.
data Linear = Linear
    { Linear -> Map AccessPath (Integer, Maybe (Integer, Integer))
linPaths :: Map AccessPath (Integer, Maybe (Integer, Integer))
    -- ^ Each path's coefficient, and the least and most it can be.
    , Linear -> Integer
linConst :: Integer
    }

constantSum :: Integer -> Linear
constantSum :: Integer -> Linear
constantSum = Map AccessPath (Integer, Maybe (Integer, Integer))
-> Integer -> Linear
Linear Map AccessPath (Integer, Maybe (Integer, Integer))
forall k a. Map k a
Map.empty

-- | A path as a sum, with the values the facts know it has, or any of its
-- type's.
pathSum :: Facts -> AccessPath -> IntTy -> Linear
pathSum :: Facts -> AccessPath -> IntTy -> Linear
pathSum Facts
facts AccessPath
p IntTy
ty = Map AccessPath (Integer, Maybe (Integer, Integer))
-> Integer -> Linear
Linear (AccessPath
-> (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall k a. k -> a -> Map k a
Map.singleton AccessPath
p (Integer
1, [Range] -> Maybe (Integer, Integer)
valueSpan ([Range]
-> ((IntTy, [Range]) -> [Range])
-> Maybe (IntTy, [Range])
-> [Range]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [IntTy -> Range
tyRange IntTy
ty] (IntTy, [Range]) -> [Range]
forall a b. (a, b) -> b
snd (AccessPath
-> Map AccessPath (IntTy, [Range]) -> Maybe (IntTy, [Range])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
p (Facts -> Map AccessPath (IntTy, [Range])
factsValues Facts
facts))))) Integer
0

valueSpan :: [Range] -> Maybe (Integer, Integer)
valueSpan :: [Range] -> Maybe (Integer, Integer)
valueSpan = \case
    [] -> Maybe (Integer, Integer)
forall a. Maybe a
Nothing
    [Range]
rs -> (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
lo [Range]
rs), [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
hi [Range]
rs))

plus :: Linear -> Linear -> Linear
plus :: Linear -> Linear -> Linear
plus (Linear Map AccessPath (Integer, Maybe (Integer, Integer))
a Integer
c) (Linear Map AccessPath (Integer, Maybe (Integer, Integer))
b Integer
d) = Map AccessPath (Integer, Maybe (Integer, Integer))
-> Integer -> Linear
Linear (((Integer, Maybe (Integer, Integer)) -> Bool)
-> Map AccessPath (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) (Integer -> Bool)
-> ((Integer, Maybe (Integer, Integer)) -> Integer)
-> (Integer, Maybe (Integer, Integer))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Maybe (Integer, Integer)) -> Integer
forall a b. (a, b) -> a
fst) (((Integer, Maybe (Integer, Integer))
 -> (Integer, Maybe (Integer, Integer))
 -> (Integer, Maybe (Integer, Integer)))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (Integer, Maybe (Integer, Integer))
-> (Integer, Maybe (Integer, Integer))
-> (Integer, Maybe (Integer, Integer))
forall {a} {b} {b}. Num a => (a, b) -> (a, b) -> (a, b)
add Map AccessPath (Integer, Maybe (Integer, Integer))
a Map AccessPath (Integer, Maybe (Integer, Integer))
b)) (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d)
  where add :: (a, b) -> (a, b) -> (a, b)
add (a
x, b
r) (a
y, b
_) = (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y, b
r)

scale :: Integer -> Linear -> Linear
scale :: Integer -> Linear -> Linear
scale Integer
k (Linear Map AccessPath (Integer, Maybe (Integer, Integer))
ps Integer
c) = Map AccessPath (Integer, Maybe (Integer, Integer))
-> Integer -> Linear
Linear (((Integer, Maybe (Integer, Integer)) -> Bool)
-> Map AccessPath (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) (Integer -> Bool)
-> ((Integer, Maybe (Integer, Integer)) -> Integer)
-> (Integer, Maybe (Integer, Integer))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Maybe (Integer, Integer)) -> Integer
forall a b. (a, b) -> a
fst) (((Integer, Maybe (Integer, Integer))
 -> (Integer, Maybe (Integer, Integer)))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(Integer
x, Maybe (Integer, Integer)
r) -> (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
x, Maybe (Integer, Integer)
r)) Map AccessPath (Integer, Maybe (Integer, Integer))
ps)) (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
c)

-- | The product of two sums, if one of them is a constant.
times :: Linear -> Linear -> Maybe Linear
times :: Linear -> Linear -> Maybe Linear
times Linear
x Linear
y
    | Map AccessPath (Integer, Maybe (Integer, Integer)) -> Bool
forall k a. Map k a -> Bool
Map.null (Linear -> Map AccessPath (Integer, Maybe (Integer, Integer))
linPaths Linear
x) = Linear -> Maybe Linear
forall a. a -> Maybe a
Just (Integer -> Linear -> Linear
scale (Linear -> Integer
linConst Linear
x) Linear
y)
    | Map AccessPath (Integer, Maybe (Integer, Integer)) -> Bool
forall k a. Map k a -> Bool
Map.null (Linear -> Map AccessPath (Integer, Maybe (Integer, Integer))
linPaths Linear
y) = Linear -> Maybe Linear
forall a. a -> Maybe a
Just (Integer -> Linear -> Linear
scale (Linear -> Integer
linConst Linear
y) Linear
x)
    | Bool
otherwise = Maybe Linear
forall a. Maybe a
Nothing

-- | The least and most a sum can be.
extent :: Linear -> Maybe (Integer, Integer)
extent :: Linear -> Maybe (Integer, Integer)
extent (Linear Map AccessPath (Integer, Maybe (Integer, Integer))
ps Integer
c) = ((Integer, Integer)
 -> (Integer, Maybe (Integer, Integer)) -> Maybe (Integer, Integer))
-> (Integer, Integer)
-> [(Integer, Maybe (Integer, Integer))]
-> Maybe (Integer, Integer)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Integer, Integer)
-> (Integer, Maybe (Integer, Integer)) -> Maybe (Integer, Integer)
forall {f :: * -> *} {b}.
(Functor f, Num b, Ord b) =>
(b, b) -> (b, f (b, b)) -> f (b, b)
add (Integer
c, Integer
c) (Map AccessPath (Integer, Maybe (Integer, Integer))
-> [(Integer, Maybe (Integer, Integer))]
forall k a. Map k a -> [a]
Map.elems Map AccessPath (Integer, Maybe (Integer, Integer))
ps)
  where
    add :: (b, b) -> (b, f (b, b)) -> f (b, b)
add (b
l, b
h) (b
k, f (b, b)
r) = (\(b
pl, b
ph) -> (b
l b -> b -> b
forall a. Num a => a -> a -> a
+ b -> b -> b
forall a. Ord a => a -> a -> a
min (b
k b -> b -> b
forall a. Num a => a -> a -> a
* b
pl) (b
k b -> b -> b
forall a. Num a => a -> a -> a
* b
ph), b
h b -> b -> b
forall a. Num a => a -> a -> a
+ b -> b -> b
forall a. Ord a => a -> a -> a
max (b
k b -> b -> b
forall a. Num a => a -> a -> a
* b
pl) (b
k b -> b -> b
forall a. Num a => a -> a -> a
* b
ph))) ((b, b) -> (b, b)) -> f (b, b) -> f (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b, b)
r

-- | 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.
exactSum :: Facts -> Term -> Maybe Linear
exactSum :: Facts -> Term -> Maybe Linear
exactSum Facts
facts = Facts -> (Term -> Linear -> Bool) -> Term -> Maybe Linear
sumWith Facts
facts ((Term -> Linear -> Bool) -> Term -> Maybe Linear)
-> (Term -> Linear -> Bool) -> Term -> Maybe Linear
forall a b. (a -> b) -> a -> b
$ \Term
u Linear
s -> case (Term -> Maybe IntTy
termTy Term
u, Linear -> Maybe (Integer, Integer)
extent Linear
s) of
    (Just IntTy
ty, Just (Integer
l, Integer
h)) -> Range -> Integer
lo (IntTy -> Range
tyRange IntTy
ty) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
l Bool -> Bool -> Bool
&& Integer
h Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi (IntTy -> Range
tyRange IntTy
ty)
    (Maybe IntTy, Maybe (Integer, Integer))
_                      -> Bool
False

-- | A term as a sum, even where computing it can wrap around.
anySum :: Facts -> Term -> Maybe Linear
anySum :: Facts -> Term -> Maybe Linear
anySum Facts
facts = Facts -> (Term -> Linear -> Bool) -> Term -> Maybe Linear
sumWith Facts
facts (\Term
_ Linear
_ -> Bool
True)

-- | A term as a sum, where each part of it that is arithmetic is one that
-- the check accepts.
sumWith :: Facts -> (Term -> Linear -> Bool) -> Term -> Maybe Linear
sumWith :: Facts -> (Term -> Linear -> Bool) -> Term -> Maybe Linear
sumWith Facts
facts Term -> Linear -> Bool
accepts = Term -> Maybe Linear
go
  where
    go :: Term -> Maybe Linear
go Term
u = case Term -> TermKind
termKind (Term -> Term
stripCasts Term
u) of
        TConst Integer
k -> Linear -> Maybe Linear
forall a. a -> Maybe a
Just (Integer -> Linear
constantSum Integer
k)
        TLoad AccessPath
p -> Linear -> Maybe Linear
forall a. a -> Maybe a
Just (Map AccessPath (Integer, Maybe (Integer, Integer))
-> Integer -> Linear
Linear (AccessPath
-> (Integer, Maybe (Integer, Integer))
-> Map AccessPath (Integer, Maybe (Integer, Integer))
forall k a. k -> a -> Map k a
Map.singleton AccessPath
p (Integer
1, [Range] -> Maybe (Integer, Integer)
valueSpan ([Range] -> Maybe (Integer, Integer))
-> Maybe [Range] -> Maybe (Integer, Integer)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Facts -> Term -> Maybe [Range]
eval Facts
facts Term
u)) Integer
0)
        TBin CBinaryOp
CAddOp Term
a Term
b -> Term -> Linear -> Maybe Linear
checked Term
u (Linear -> Maybe Linear) -> Maybe Linear -> Maybe Linear
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Linear -> Linear -> Linear
plus (Linear -> Linear -> Linear)
-> Maybe Linear -> Maybe (Linear -> Linear)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Linear
go Term
a Maybe (Linear -> Linear) -> Maybe Linear -> Maybe Linear
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Linear
go Term
b
        TBin CBinaryOp
CSubOp Term
a Term
b -> Term -> Linear -> Maybe Linear
checked Term
u (Linear -> Maybe Linear) -> Maybe Linear -> Maybe Linear
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Linear -> Linear -> Linear
plus (Linear -> Linear -> Linear)
-> Maybe Linear -> Maybe (Linear -> Linear)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Linear
go Term
a Maybe (Linear -> Linear) -> Maybe Linear -> Maybe Linear
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Integer -> Linear -> Linear
scale (-Integer
1) (Linear -> Linear) -> Maybe Linear -> Maybe Linear
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Linear
go Term
b)
        TBin CBinaryOp
CMulOp Term
a Term
b -> Term -> Linear -> Maybe Linear
checked Term
u (Linear -> Maybe Linear) -> Maybe Linear -> Maybe Linear
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe (Maybe Linear) -> Maybe Linear
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Linear -> Linear -> Maybe Linear
times (Linear -> Linear -> Maybe Linear)
-> Maybe Linear -> Maybe (Linear -> Maybe Linear)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Linear
go Term
a Maybe (Linear -> Maybe Linear)
-> Maybe Linear -> Maybe (Maybe Linear)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Linear
go Term
b)
        TermKind
_ | Just [Range Integer
k Integer
k' Origin
Plain] <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
u, Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
k' -> Linear -> Maybe Linear
forall a. a -> Maybe a
Just (Integer -> Linear
constantSum Integer
k)
        TermKind
_ -> Maybe Linear
forall a. Maybe a
Nothing
    checked :: Term -> Linear -> Maybe Linear
checked Term
u Linear
s = if Term -> Linear -> Bool
accepts (Term -> Term
stripCasts Term
u) Linear
s then Linear -> Maybe Linear
forall a. a -> Maybe a
Just Linear
s else Maybe Linear
forall a. Maybe a
Nothing

-- | 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.
atMost :: Facts -> [(Integer, Term)] -> Integer -> Linear -> Bool
atMost :: Facts -> [(Integer, Term)] -> Integer -> Linear -> Bool
atMost Facts
facts [(Integer, Term)]
ts Integer
k Linear
bound = case (Linear -> Linear -> Linear) -> Linear -> [Linear] -> Linear
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Linear -> Linear -> Linear
plus (Integer -> Linear
constantSum Integer
k) ([Linear] -> Linear) -> Maybe [Linear] -> Maybe Linear
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Integer, Term) -> Maybe Linear)
-> [(Integer, Term)] -> Maybe [Linear]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Integer, Term) -> Maybe Linear
part [(Integer, Term)]
ts of
    Just Linear
total -> Linear -> Bool
nonPositive (Linear
total Linear -> Linear -> Linear
`plus` Integer -> Linear -> Linear
scale (-Integer
1) Linear
bound)
    Maybe Linear
Nothing    -> Bool
False
  where
    part :: (Integer, Term) -> Maybe Linear
part (Integer
c, Term
t) = Integer -> Linear -> Linear
scale Integer
c (Linear -> Linear) -> Maybe Linear -> Maybe Linear
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Facts -> Term -> Maybe Linear
exactSum Facts
facts Term
t
    nonPositive :: Linear -> Bool
nonPositive Linear
d = case Map AccessPath (Integer, Maybe (Integer, Integer))
-> [(AccessPath, (Integer, Maybe (Integer, Integer)))]
forall k a. Map k a -> [(k, a)]
Map.toList (Linear -> Map AccessPath (Integer, Maybe (Integer, Integer))
linPaths Linear
d) of
        [(AccessPath
p, (Integer
a, Maybe (Integer, Integer)
_)), (AccessPath
q, (Integer
b, Maybe (Integer, Integer)
_))]
            | Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
forall a. Num a => a -> a
negate Integer
b, Just Integer
c <- (AccessPath, AccessPath)
-> Map (AccessPath, AccessPath) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (if Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then (AccessPath
p, AccessPath
q) else (AccessPath
q, AccessPath
p)) (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
facts) ->
                Integer -> Integer
forall a. Num a => a -> a
abs Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Linear -> Integer
linConst Linear
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0
        [(AccessPath, (Integer, Maybe (Integer, Integer)))]
_ -> Bool
-> ((Integer, Integer) -> Bool) -> Maybe (Integer, Integer) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) (Integer -> Bool)
-> ((Integer, Integer) -> Integer) -> (Integer, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd) (Linear -> Maybe (Integer, Integer)
extent Linear
d)

-- | Records how an assigned path relates to the path it was assigned from.
relateAssigned :: Facts -> AccessPath -> IntTy -> Term -> Facts -> Facts
relateAssigned :: Facts -> AccessPath -> IntTy -> Term -> Facts -> Facts
relateAssigned Facts
before AccessPath
p IntTy
ty Term
r Facts
after = case (Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
before Term
r, Facts -> Term -> Maybe [Range]
eval Facts
before Term
r) of
    (Just (Just AccessPath
q, Integer
c), Just [Range]
v) | AccessPath
q AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
/= AccessPath
p, (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe IntTy -> Range -> Bool
fitsIn (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just IntTy
ty)) [Range]
v ->
        Facts -> Maybe Facts -> Facts
forall a. a -> Maybe a -> a
fromMaybe Facts
after (AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
p AccessPath
q Integer
c Facts
after Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
q AccessPath
p (Integer -> Integer
forall a. Num a => a -> a
negate Integer
c))
    (Maybe (Maybe AccessPath, Integer), Maybe [Range])
_ -> Facts
after

clipRanges :: Integer -> Integer -> [Range] -> [Range]
clipRanges :: Integer -> Integer -> [Range] -> [Range]
clipRanges Integer
a Integer
b = (Range -> Maybe Range) -> [Range] -> [Range]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Range -> Maybe Range) -> [Range] -> [Range])
-> (Range -> Maybe Range) -> [Range] -> [Range]
forall a b. (a -> b) -> a -> b
$ \Range
x ->
    let x' :: Range
x' = Integer -> Integer -> Origin -> Range
Range (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
a (Range -> Integer
lo Range
x)) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
b (Range -> Integer
hi Range
x)) (Range -> Origin
origin Range
x)
    in if Range -> Integer
lo Range
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi Range
x' then Range -> Maybe Range
forall a. a -> Maybe a
Just Range
x' else Maybe Range
forall a. Maybe a
Nothing

-- | What evaluating a term does to the facts. Writes that only happen on
-- some paths through the term forget the paths they write.
effects :: Bool -> Term -> Facts -> Facts
effects :: Bool -> Term -> Facts -> Facts
effects Bool
definite Term
t Facts
facts = case Term -> TermKind
termKind Term
t of
    TAssign Maybe AccessPath
mp CAssignOp
op Term
l Term
r ->
        let after :: Facts
after = Bool -> Term -> Facts -> Facts
effects Bool
definite Term
l (Bool -> Term -> Facts -> Facts
effects Bool
definite Term
r Facts
facts)
        in case (Maybe AccessPath
mp, Term -> Maybe IntTy
termTy Term
l) of
            (Just AccessPath
p, Just IntTy
ty) | Bool
definite, Just [Range]
v <- Facts -> NodeInfo -> CAssignOp -> Term -> Term -> Maybe [Range]
assigned Facts
facts NodeInfo
site CAssignOp
op Term
l Term
r ->
                let selfShift :: Maybe Integer
selfShift = case (CAssignOp
op, Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
r) of
                        (CAssignOp
CAssignOp, Just (Just AccessPath
q, Integer
c)) | AccessPath
q AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
== AccessPath
p -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
c
                        (CAssignOp
CAddAssOp, Just (Maybe AccessPath
Nothing, Integer
c))         -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
c
                        (CAssignOp
CSubAssOp, Just (Maybe AccessPath
Nothing, Integer
c))         -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer
forall a. Num a => a -> a
negate Integer
c)
                        (CAssignOp, Maybe (Maybe AccessPath, Integer))
_                                      -> Maybe Integer
forall a. Maybe a
Nothing
                in case Maybe Integer
selfShift of
                    Just Integer
c | Facts -> Term -> IntTy -> Integer -> Bool
shifts Facts
facts Term
l IntTy
ty Integer
c -> AccessPath -> IntTy -> [Range] -> Integer -> Facts -> Facts
shiftPath AccessPath
p IntTy
ty [Range]
v Integer
c Facts
after
                    Maybe Integer
_ | CAssignOp
op CAssignOp -> CAssignOp -> Bool
forall a. Eq a => a -> a -> Bool
== CAssignOp
CAssignOp -> Facts -> AccessPath -> IntTy -> Term -> Facts -> Facts
relateAssigned Facts
facts AccessPath
p IntTy
ty Term
r (AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath AccessPath
p IntTy
ty [Range]
v Facts
after)
                    Maybe Integer
_ -> AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath AccessPath
p IntTy
ty [Range]
v Facts
after
            (Just AccessPath
p, Maybe IntTy
_) -> AccessPath -> Facts -> Facts
forget AccessPath
p Facts
after
            (Maybe AccessPath
Nothing, Maybe IntTy
_) -> Term -> Facts -> Facts
forgetWrite Term
l Facts
after
    TUnary CUnaryOp
op Term
a | CUnaryOp
op CUnaryOp -> [CUnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CUnaryOp
CPreIncOp, CUnaryOp
CPreDecOp, CUnaryOp
CPostIncOp, CUnaryOp
CPostDecOp] ->
        let after :: Facts
after = Bool -> Term -> Facts -> Facts
effects Bool
definite Term
a Facts
facts
            d :: Integer
d = if CUnaryOp
op CUnaryOp -> [CUnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CUnaryOp
CPreIncOp, CUnaryOp
CPostIncOp] then Integer
1 else -Integer
1
        in case (Term -> TermKind
termKind Term
a, Term -> Maybe IntTy
termTy Term
a, Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a) of
            (TLoad AccessPath
p, Just IntTy
ty, Just [Range]
v) | Bool
definite ->
                let v' :: [Range]
v' = [Range] -> [Range]
normalise ((Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NodeInfo -> IntTy -> Range -> [Range]
convert NodeInfo
site IntTy
ty) [ Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) (Range -> Integer
hi Range
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) (Range -> Range -> Origin
arithOrigin Range
r Range
r) | Range
r <- [Range]
v ])
                in if Facts -> Term -> IntTy -> Integer -> Bool
shifts Facts
facts Term
a IntTy
ty Integer
d then AccessPath -> IntTy -> [Range] -> Integer -> Facts -> Facts
shiftPath AccessPath
p IntTy
ty [Range]
v' Integer
d Facts
after else AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath AccessPath
p IntTy
ty [Range]
v' Facts
after
            (TLoad AccessPath
p, Maybe IntTy
_, Maybe [Range]
_) -> AccessPath -> Facts -> Facts
forget AccessPath
p Facts
after
            (TermKind, Maybe IntTy, Maybe [Range])
_ -> Term -> Facts -> Facts
forgetWrite Term
a Facts
after
    TCall Term
f [Term]
args ->
        let passed :: [AccessPath]
passed = [ String -> AccessPath
PathVar String
n | Term
a <- [Term]
args, Just CExpr
e <- [CExpr -> Maybe CExpr
passedAddress (Term -> CExpr
termExpr Term
a)], String
n <- CExpr -> [String]
addressed CExpr
e ]
        in (AccessPath -> Facts -> Facts) -> Facts -> [AccessPath] -> Facts
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr AccessPath -> Facts -> Facts
forget (Facts -> Facts
forgetMemory ((Facts -> Term -> Facts) -> Facts -> [Term] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Term -> Facts -> Facts) -> Facts -> Term -> Facts
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Term -> Facts -> Facts
effects Bool
definite)) (Bool -> Term -> Facts -> Facts
effects Bool
definite Term
f Facts
facts) [Term]
args)) [AccessPath]
passed
    TBin CBinaryOp
op Term
a Term
b | CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLndOp, CBinaryOp
CLorOp] -> Bool -> Term -> Facts -> Facts
effects Bool
False Term
b (Bool -> Term -> Facts -> Facts
effects Bool
definite Term
a Facts
facts)
    TCond Term
c Maybe Term
m Term
f -> (Facts -> Term -> Facts) -> Facts -> [Term] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Term -> Facts -> Facts) -> Facts -> Term -> Facts
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Term -> Facts -> Facts
effects Bool
False)) (Bool -> Term -> Facts -> Facts
effects Bool
definite Term
c Facts
facts) ([Term] -> (Term -> [Term]) -> Maybe Term -> [Term]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Term
m [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
f])
    TermKind
TUnknown -> Facts -> Facts
forgetAll Facts
facts
    TermKind
_ -> (Facts -> Term -> Facts) -> Facts -> [Term] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Term -> Facts -> Facts) -> Facts -> Term -> Facts
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Term -> Facts -> Facts
effects Bool
definite)) Facts
facts (Term -> [Term]
children Term
t)
  where
    site :: NodeInfo
site = CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation (Term -> CExpr
termExpr Term
t)
    -- Adding a constant to a path shifts it if every value it has stays in
    -- its type.
    shifts :: Facts -> Term -> IntTy -> Integer -> Bool
shifts Facts
fs Term
l IntTy
ty Integer
c = Bool -> ([Range] -> Bool) -> Maybe [Range] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe IntTy -> Range -> Bool
fitsIn (IntTy -> Maybe IntTy
forall a. a -> Maybe a
Just IntTy
ty)) ([Range] -> Bool) -> ([Range] -> [Range]) -> [Range] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Range] -> [Range]
shift Integer
c) (Facts -> Term -> Maybe [Range]
eval Facts
fs Term
l)
    forgetWrite :: Term -> Facts -> Facts
forgetWrite Term
l = case Term -> CExpr
termExpr Term
l of
        CMember CExpr
_ Ident
f Bool
_ NodeInfo
_ -> String -> Facts -> Facts
forgetField (Ident -> String
identToString Ident
f)
        CExpr
_               -> Facts -> Facts
forgetMemory

-- | Forgets the field with this name of any object in memory, and memory it
-- may be part of.
forgetField :: String -> Facts -> Facts
forgetField :: String -> Facts -> Facts
forgetField String
f = (AccessPath -> Bool) -> Facts -> Facts
forgetWhere ((AccessPath -> Bool) -> Facts -> Facts)
-> (AccessPath -> Bool) -> Facts -> Facts
forall a b. (a -> b) -> a -> b
$ \AccessPath
q -> AccessPath -> Bool
isMemory AccessPath
q Bool -> Bool -> Bool
&& case AccessPath
q of
    PathField AccessPath
_ String
g -> String
g String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
f
    AccessPath
_             -> Bool
True

children :: Term -> [Term]
children :: Term -> [Term]
children Term
t = case Term -> TermKind
termKind Term
t of
    TBin CBinaryOp
_ Term
a Term
b      -> [Term
a, Term
b]
    TUnary CUnaryOp
_ Term
a      -> [Term
a]
    TCast Term
a         -> [Term
a]
    TCond Term
c Maybe Term
m Term
f     -> Term
c Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term] -> (Term -> [Term]) -> Maybe Term -> [Term]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Term
m [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
f]
    TAssign Maybe AccessPath
_ CAssignOp
_ Term
l Term
r -> [Term
l, Term
r]
    TIndex Term
a Term
i Maybe Integer
_    -> [Term
a, Term
i]
    TCall Term
f [Term]
args    -> Term
f Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args
    TOther [Term]
ts       -> [Term]
ts
    TermKind
_               -> []

------------------------------------------------------------------------------
-- Branch conditions

swapOp :: CBinaryOp -> CBinaryOp
swapOp :: CBinaryOp -> CBinaryOp
swapOp = \case
    CBinaryOp
CLeOp  -> CBinaryOp
CGrOp
    CBinaryOp
CGrOp  -> CBinaryOp
CLeOp
    CBinaryOp
CLeqOp -> CBinaryOp
CGeqOp
    CBinaryOp
CGeqOp -> CBinaryOp
CLeqOp
    CBinaryOp
op     -> CBinaryOp
op

-- | The comparison that holds when this one doesn't.
negateOp :: CBinaryOp -> CBinaryOp
negateOp :: CBinaryOp -> CBinaryOp
negateOp = \case
    CBinaryOp
CLeOp  -> CBinaryOp
CGeqOp
    CBinaryOp
CGrOp  -> CBinaryOp
CLeqOp
    CBinaryOp
CLeqOp -> CBinaryOp
CGrOp
    CBinaryOp
CGeqOp -> CBinaryOp
CLeOp
    CBinaryOp
CEqOp  -> CBinaryOp
CNeqOp
    CBinaryOp
_      -> CBinaryOp
CEqOp

joinFacts :: Facts -> Facts -> Facts
joinFacts :: Facts -> Facts -> Facts
joinFacts Facts
a Facts
b = Facts
    { factsChanges :: Int
factsChanges = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Facts -> Int
factsChanges Facts
a) (Facts -> Int
factsChanges Facts
b)
    , factsBackEdge :: Bool
factsBackEdge = Bool
False
    , factsValues :: Map AccessPath (IntTy, [Range])
factsValues = ((IntTy, [Range]) -> (IntTy, [Range]) -> (IntTy, [Range]))
-> Map AccessPath (IntTy, [Range])
-> Map AccessPath (IntTy, [Range])
-> Map AccessPath (IntTy, [Range])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (\(IntTy
ty, [Range]
x) (IntTy
_, [Range]
y) -> (IntTy
ty, [Range] -> [Range]
normalise ([Range]
x [Range] -> [Range] -> [Range]
forall a. [a] -> [a] -> [a]
++ [Range]
y))) (Facts -> Map AccessPath (IntTy, [Range])
factsValues Facts
a) (Facts -> Map AccessPath (IntTy, [Range])
factsValues Facts
b)
    , factsDiffs :: Map (AccessPath, AccessPath) Integer
factsDiffs = (Integer -> Integer -> Integer)
-> Map (AccessPath, AccessPath) Integer
-> Map (AccessPath, AccessPath) Integer
-> Map (AccessPath, AccessPath) Integer
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
a) (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
b)
    }

joinMaybe :: Maybe Facts -> Maybe Facts -> Maybe Facts
joinMaybe :: Maybe Facts -> Maybe Facts -> Maybe Facts
joinMaybe (Just Facts
a) (Just Facts
b) = Facts -> Maybe Facts
forall a. a -> Maybe a
Just (Facts -> Facts -> Facts
joinFacts Facts
a Facts
b)
joinMaybe Maybe Facts
a Maybe Facts
Nothing         = Maybe Facts
a
joinMaybe Maybe Facts
Nothing Maybe Facts
b         = Maybe Facts
b

-- | The facts on the paths where a condition has the given truth value, or
-- 'Nothing' if it can't have it.
assume :: Bool -> Term -> Facts -> Maybe Facts
assume :: Bool -> Term -> Facts -> Maybe Facts
assume Bool
truth Term
t Facts
facts = case Term -> TermKind
termKind Term
t of
    TUnary CUnaryOp
CNegOp Term
a -> Bool -> Term -> Facts -> Maybe Facts
assume (Bool -> Bool
not Bool
truth) Term
a Facts
facts
    TBin CBinaryOp
CLndOp Term
a Term
b
        | Bool
truth -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
a Facts
facts Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
b
        | Bool
otherwise -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
a Facts
facts Maybe Facts -> Maybe Facts -> Maybe Facts
`joinMaybe` (Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
a Facts
facts Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
b)
    TBin CBinaryOp
CLorOp Term
a Term
b
        | Bool
truth -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
a Facts
facts Maybe Facts -> Maybe Facts -> Maybe Facts
`joinMaybe` (Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
a Facts
facts Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
b)
        | Bool
otherwise -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
a Facts
facts Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
b
    TBin CBinaryOp
op Term
a Term
b | CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp, CBinaryOp
CEqOp, CBinaryOp
CNeqOp] ->
        let op' :: CBinaryOp
op' = if Bool
truth then CBinaryOp
op else CBinaryOp -> CBinaryOp
negateOp CBinaryOp
op
        in CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts CBinaryOp
op' Term
a Term
b Facts
facts
    TCast Term
a | Just [Range]
v <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a, (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe IntTy -> Range -> Bool
fitsIn (Term -> Maybe IntTy
termTy Term
t)) [Range]
v -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
truth Term
a Facts
facts
    TLoad AccessPath
_ -> CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts (if Bool
truth then CBinaryOp
CNeqOp else CBinaryOp
CEqOp) Term
t Term
zero Facts
facts
    TermKind
_ -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts
  where
    zero :: Term
zero = CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term (Term -> CExpr
termExpr Term
t) (Term -> Maybe IntTy
termTy Term
t) Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (Integer -> TermKind
TConst Integer
0)

-- | Narrows the paths each side of a comparison reads, given that it holds,
-- and records how the sides relate.
compareFacts :: CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts :: CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts CBinaryOp
op Term
l Term
r Facts
facts = case (Facts -> Term -> Maybe [Range]
eval Facts
facts Term
l, Facts -> Term -> Maybe [Range]
eval Facts
facts Term
r) of
    (Just lv :: [Range]
lv@(Range
_ : [Range]
_), Just rv :: [Range]
rv@(Range
_ : [Range]
_)) | [Range] -> [Range] -> Bool
forall {t :: * -> *} {t :: * -> *}.
(Foldable t, Foldable t) =>
t Range -> t Range -> Bool
exact [Range]
lv [Range]
rv ->
        CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide CBinaryOp
op Term
l [Range]
lv [Range]
rv Facts
facts Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide (CBinaryOp -> CBinaryOp
swapOp CBinaryOp
op) Term
r [Range]
rv [Range]
lv Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Facts -> Maybe Facts
relateSides
    (Maybe [Range], Maybe [Range])
_ -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts
  where
    -- The comparison is between the values themselves, rather than values
    -- converted to an unsigned type, if neither side can be negative or the
    -- conversions C makes before comparing give a signed type.
    exact :: t Range -> t Range -> Bool
exact t Range
lv t Range
rv = (Range -> Bool) -> t Range -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Integer -> Bool) -> (Range -> Integer) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer
lo) t Range
lv Bool -> Bool -> Bool
&& (Range -> Bool) -> t Range -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Integer -> Bool) -> (Range -> Integer) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer
lo) t Range
rv
        Bool -> Bool -> Bool
|| Bool -> (IntTy -> Bool) -> Maybe IntTy -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False IntTy -> Bool
tySigned (IntTy -> IntTy -> IntTy
usual (IntTy -> IntTy -> IntTy) -> Maybe IntTy -> Maybe (IntTy -> IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IntTy -> IntTy
promote (IntTy -> IntTy) -> Maybe IntTy -> Maybe IntTy
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe IntTy
termTy Term
l) Maybe (IntTy -> IntTy) -> Maybe IntTy -> Maybe IntTy
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (IntTy -> IntTy
promote (IntTy -> IntTy) -> Maybe IntTy -> Maybe IntTy
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe IntTy
termTy Term
r))

    relateSides :: Facts -> Maybe Facts
relateSides Facts
f = case (Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
l, Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
r) of
        (Just (Just AccessPath
p, Integer
a), Just (Just AccessPath
q, Integer
b)) -> case CBinaryOp
op of
            CBinaryOp
CLeOp  -> AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
p AccessPath
q (Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Facts
f
            CBinaryOp
CLeqOp -> AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
p AccessPath
q (Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
a) Facts
f
            CBinaryOp
CGrOp  -> AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
q AccessPath
p (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Facts
f
            CBinaryOp
CGeqOp -> AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
q AccessPath
p (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b) Facts
f
            CBinaryOp
CEqOp  -> AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
p AccessPath
q (Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
a) Facts
f Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts
relate AccessPath
q AccessPath
p (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b)
            CBinaryOp
_      -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
f
        (Maybe (Maybe AccessPath, Integer),
 Maybe (Maybe AccessPath, Integer))
_ -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
f

-- | Narrows the path one side of a comparison reads, given that the
-- comparison holds and the values of both sides, or 'Nothing' if it can't
-- hold.
narrowSide :: CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide :: CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide CBinaryOp
op Term
t [Range]
tv [Range]
ov Facts
facts = case (Term -> TermKind
termKind (Term -> Term
stripCasts Term
t), Term -> Maybe IntTy
termTy (Term -> Term
stripCasts Term
t)) of
    (TLoad AccessPath
p, Just IntTy
ty) | Bool -> Bool
not ([Range] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Range]
narrowed) -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just (AccessPath -> IntTy -> [Range] -> Facts -> Facts
narrowPath AccessPath
p IntTy
ty [Range]
narrowed Facts
facts)
                       | Bool
otherwise -> Maybe Facts
forall a. Maybe a
Nothing
      where narrowed :: [Range]
narrowed = IntTy -> [Range]
narrow IntTy
ty
    (TermKind, Maybe IntTy)
_ | Just (Term
l, Integer
k) <- Facts -> Term -> Maybe (Term, Integer)
offsetLoad Facts
facts Term
t, Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 ->
        CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide CBinaryOp
op Term
l (Integer -> [Range] -> [Range]
shift (-Integer
k) [Range]
tv) (Integer -> [Range] -> [Range]
shift (-Integer
k) [Range]
ov) Facts
facts
    (TermKind, Maybe IntTy)
_ | TCast Term
a <- Term -> TermKind
termKind Term
t, Just [Range]
av <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
a, (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe IntTy -> Range -> Bool
fitsIn (Term -> Maybe IntTy
termTy Term
t)) [Range]
av ->
        CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts
narrowSide CBinaryOp
op Term
a [Range]
tv [Range]
ov Facts
facts
    (TermKind, Maybe IntTy)
_ | CBinaryOp
op CBinaryOp -> CBinaryOp -> Bool
forall a. Eq a => a -> a -> Bool
== CBinaryOp
CEqOp, [Range] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Integer -> Integer -> [Range] -> [Range]
clipRanges Integer
ol Integer
oh [Range]
tv) -> Maybe Facts
forall a. Maybe a
Nothing
      | Bool
otherwise -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts
  where
    Range Integer
ol Integer
oh Origin
_ = [Range] -> Range
hull [Range]
ov
    narrow :: IntTy -> [Range]
narrow IntTy
ty = case CBinaryOp
op of
        CBinaryOp
CLeOp  -> Integer -> Integer -> [Range] -> [Range]
clipRanges (Range -> Integer
lo (IntTy -> Range
tyRange IntTy
ty)) (Integer
oh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) [Range]
tv
        CBinaryOp
CLeqOp -> Integer -> Integer -> [Range] -> [Range]
clipRanges (Range -> Integer
lo (IntTy -> Range
tyRange IntTy
ty)) Integer
oh [Range]
tv
        CBinaryOp
CGrOp  -> Integer -> Integer -> [Range] -> [Range]
clipRanges (Integer
ol Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Range -> Integer
hi (IntTy -> Range
tyRange IntTy
ty)) [Range]
tv
        CBinaryOp
CGeqOp -> Integer -> Integer -> [Range] -> [Range]
clipRanges Integer
ol (Range -> Integer
hi (IntTy -> Range
tyRange IntTy
ty)) [Range]
tv
        CBinaryOp
CEqOp  -> Integer -> Integer -> [Range] -> [Range]
clipRanges Integer
ol Integer
oh [Range]
tv
        CBinaryOp
_ | Integer
ol Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
oh -> (Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Integer -> Range -> [Range]
remove Integer
ol) [Range]
tv
          | Bool
otherwise -> [Range]
tv
    remove :: Integer -> Range -> [Range]
remove Integer
v Range
x
        | Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Integer
lo Range
x Bool -> Bool -> Bool
|| Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Range -> Integer
hi Range
x = [Range
x]
        | Bool
otherwise = [ Range
y | Range
y <- [Integer -> Integer -> Origin -> Range
Range (Range -> Integer
lo Range
x) (Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (Range -> Origin
origin Range
x), Integer -> Integer -> Origin -> Range
Range (Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Range -> Integer
hi Range
x) (Range -> Origin
origin Range
x)], Range -> Integer
lo Range
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi Range
y ]

fitsIn :: Maybe IntTy -> Range -> Bool
fitsIn :: Maybe IntTy -> Range -> Bool
fitsIn Maybe IntTy
ty Range
r = Bool -> (IntTy -> Bool) -> Maybe IntTy -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\IntTy
t -> Range -> Integer
lo Range
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Range -> Integer
lo (IntTy -> Range
tyRange IntTy
t) Bool -> Bool -> Bool
&& Range -> Integer
hi Range
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi (IntTy -> Range
tyRange IntTy
t)) Maybe IntTy
ty

-- | The path a term loads and the constant it adds to it, if its value is
-- that sum, computed without wrapping around.
offsetLoad :: Facts -> Term -> Maybe (Term, Integer)
offsetLoad :: Facts -> Term -> Maybe (Term, Integer)
offsetLoad Facts
facts Term
t = case Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
facts Term
t of
    Just (Just AccessPath
p, Integer
k) -> (\Term
l -> (Term
l, Integer
k)) (Term -> (Term, Integer)) -> Maybe Term -> Maybe (Term, Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> Maybe Term
forall a. [a] -> Maybe a
listToMaybe [ Term
u | Term
u <- Term -> [Term]
subTerms Term
t, TLoad AccessPath
q <- [Term -> TermKind
termKind Term
u], AccessPath
q AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
== AccessPath
p ]
    Maybe (Maybe AccessPath, Integer)
_                -> Maybe (Term, Integer)
forall a. Maybe a
Nothing

shift :: Integer -> [Range] -> [Range]
shift :: Integer -> [Range] -> [Range]
shift Integer
d = (Range -> Range) -> [Range] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\Range
r -> Range
r { lo = lo r + d, hi = hi r + d })

-- | The term a value-preserving cast converts: one to a type that can hold
-- every value of the type it converts from.
stripCasts :: Term -> Term
stripCasts :: Term -> Term
stripCasts Term
t = case Term -> TermKind
termKind Term
t of
    TCast Term
a | Just IntTy
from <- Term -> Maybe IntTy
termTy Term
a, Just IntTy
to <- Term -> Maybe IntTy
termTy Term
t
            , Range -> Integer
lo (IntTy -> Range
tyRange IntTy
to) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
lo (IntTy -> Range
tyRange IntTy
from), Range -> Integer
hi (IntTy -> Range
tyRange IntTy
from) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Integer
hi (IntTy -> Range
tyRange IntTy
to) -> Term -> Term
stripCasts Term
a
    TermKind
_ -> Term
t

------------------------------------------------------------------------------
-- The analysis

-- | How many times the facts at a loop head can change before ranges that keep
-- growing widen to the next bound the function compares them against, or to
-- their type's range.
roundsBeforeWidening :: Int
roundsBeforeWidening :: Int
roundsBeforeWidening = Int
3

-- | Joins the facts from two paths, widening at loop heads to the bounds each
-- path is compared against.
mergeFacts :: Map AccessPath (Set Integer) -> Maybe Facts -> Maybe Facts -> Maybe Facts
mergeFacts :: Map AccessPath (Set Integer)
-> Maybe Facts -> Maybe Facts -> Maybe Facts
mergeFacts Map AccessPath (Set Integer)
bounds (Just Facts
old) (Just Facts
new)
    | Facts
joined Facts -> Facts -> Bool
forall a. Eq a => a -> a -> Bool
== Facts
old = Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
old
    | Facts -> Bool
factsBackEdge Facts
new Bool -> Bool -> Bool
&& Facts -> Int
factsChanges Facts
old Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
roundsBeforeWidening = Facts -> Maybe Facts
forall a. a -> Maybe a
Just (Map AccessPath (Set Integer) -> Facts -> Facts -> Facts
widen Map AccessPath (Set Integer)
bounds Facts
old Facts
joined)
    | Bool
otherwise = Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
joined { factsChanges = factsChanges old + 1 }
  where
    joined :: Facts
joined = (Facts -> Facts -> Facts
joinFacts Facts
old Facts
new) { factsChanges = factsChanges old }
mergeFacts Map AccessPath (Set Integer)
_ Maybe Facts
a Maybe Facts
b = Maybe Facts -> Maybe Facts -> Maybe Facts
joinMaybe Maybe Facts
a Maybe Facts
b

widen :: Map AccessPath (Set Integer) -> Facts -> Facts -> Facts
widen :: Map AccessPath (Set Integer) -> Facts -> Facts -> Facts
widen Map AccessPath (Set Integer)
bounds Facts
old Facts
joined = Facts
joined
    { factsChanges = factsChanges old + 1
    , factsValues = Map.mapWithKey grow (factsValues joined)
    , factsDiffs = Map.filterWithKey steady (factsDiffs joined)
    }
  where
    steady :: (AccessPath, AccessPath) -> Integer -> Bool
steady (AccessPath, AccessPath)
k Integer
c = Bool -> (Integer -> Bool) -> Maybe Integer -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
c) ((AccessPath, AccessPath)
-> Map (AccessPath, AccessPath) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AccessPath, AccessPath)
k (Facts -> Map (AccessPath, AccessPath) Integer
factsDiffs Facts
old))
    grow :: AccessPath -> (IntTy, [Range]) -> (IntTy, [Range])
grow AccessPath
p (IntTy
ty, [Range]
v) = case AccessPath
-> Map AccessPath (IntTy, [Range]) -> Maybe (IntTy, [Range])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
p (Facts -> Map AccessPath (IntTy, [Range])
factsValues Facts
old) of
        Just (IntTy
_, [Range]
ov) | [Range]
v [Range] -> [Range] -> Bool
forall a. Eq a => a -> a -> Bool
== [Range]
ov -> (IntTy
ty, [Range]
v)
        Just (IntTy
_, [Range]
ov) ->
            let Range Integer
nl Integer
nh Origin
o = [Range] -> Range
hull [Range]
v
                Range Integer
ol Integer
oh Origin
_ = [Range] -> Range
hull [Range]
ov
                ks :: Set Integer
ks = Set Integer
-> AccessPath -> Map AccessPath (Set Integer) -> Set Integer
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set Integer
forall a. Set a
Set.empty AccessPath
p Map AccessPath (Set Integer)
bounds
                l :: Integer
l | Integer
nl Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
ol = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Range -> Integer
lo (IntTy -> Range
tyRange IntTy
ty)) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Range -> Integer
lo (IntTy -> Range
tyRange IntTy
ty))) (Integer -> Set Integer -> Maybe Integer
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLE Integer
nl Set Integer
ks)
                  | Bool
otherwise = Integer
nl
                h :: Integer
h | Integer
nh Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
oh = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Range -> Integer
hi (IntTy -> Range
tyRange IntTy
ty)) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Range -> Integer
hi (IntTy -> Range
tyRange IntTy
ty))) (Integer -> Set Integer -> Maybe Integer
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupGE Integer
nh Set Integer
ks)
                  | Bool
otherwise = Integer
nh
            in (IntTy
ty, [Integer -> Integer -> Origin -> Range
Range Integer
l Integer
h Origin
o])
        Maybe (IntTy, [Range])
Nothing -> (IntTy
ty, [Range]
v)

paramNames :: FunDef -> [String]
paramNames :: FunDef -> [String]
paramNames (FunDef (VarDecl VarName
_ DeclAttrs
_ Type
ty) Stmt
_ NodeInfo
_) = case Type
ty of
    FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_ ->
        [ Ident -> String
identToString Ident
i | ParamDecl
p <- [ParamDecl]
params, VarName Ident
i Maybe AsmName
_ <- [ParamDecl -> VarName
paramVarName ParamDecl
p] ]
    Type
_ -> []

paramVarName :: ParamDecl -> VarName
paramVarName :: ParamDecl -> VarName
paramVarName = \case
    ParamDecl (VarDecl VarName
n DeclAttrs
_ Type
_) NodeInfo
_         -> VarName
n
    AbstractParamDecl (VarDecl VarName
n DeclAttrs
_ Type
_) NodeInfo
_ -> VarName
n

-- | The locals a function declares, once for each declaration.
declaredNames :: CStat -> [String]
declaredNames :: Stmt -> [String]
declaredNames Stmt
body =
    [ Ident -> String
identToString Ident
i | CDecl [CDeclarationSpecifier NodeInfo]
_ [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds NodeInfo
_ <- Stmt -> [CDeclaration NodeInfo]
localDecls Stmt
body, (Just (CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
_ Maybe AsmName
_ [CAttribute NodeInfo]
_ NodeInfo
_), Maybe (CInitializer NodeInfo)
_, Maybe CExpr
_) <- [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds ]

-- | The locals a function declares @static@ or @extern@, whose values outlive
-- a call.
storedElsewhere :: CStat -> Set String
storedElsewhere :: Stmt -> Set String
storedElsewhere Stmt
body = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList
    [ Ident -> String
identToString Ident
i
    | CDecl [CDeclarationSpecifier NodeInfo]
specs [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds NodeInfo
_ <- Stmt -> [CDeclaration NodeInfo]
localDecls Stmt
body, (CDeclarationSpecifier NodeInfo -> Bool)
-> [CDeclarationSpecifier NodeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDeclarationSpecifier NodeInfo -> Bool
forall {a}. CDeclarationSpecifier a -> Bool
isStorage [CDeclarationSpecifier NodeInfo]
specs
    , (Just (CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
_ Maybe AsmName
_ [CAttribute NodeInfo]
_ NodeInfo
_), Maybe (CInitializer NodeInfo)
_, Maybe CExpr
_) <- [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds ]
  where
    isStorage :: CDeclarationSpecifier a -> Bool
isStorage = \case
        CStorageSpec CStatic{} -> Bool
True
        CStorageSpec CExtern{} -> Bool
True
        CDeclarationSpecifier a
_                      -> Bool
False

-- | The names whose address a statement takes, other than to pass it straight
-- to a call, which only changes them in the call.
addressTaken :: CStat -> Set String
addressTaken :: Stmt -> Set String
addressTaken = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String)
-> (Stmt -> [String]) -> Stmt -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stmt -> [String]
everything
  where
    everything :: Stmt -> [String]
everything Stmt
s = (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
exprAddrs (Stmt -> [CExpr]
statExprs Stmt
s)
    exprAddrs :: CExpr -> [String]
exprAddrs = \case
        CUnary CUnaryOp
CAdrOp CExpr
e NodeInfo
_ -> CExpr -> [String]
addressed CExpr
e [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CExpr -> [String]
exprAddrs CExpr
e
        CVar{}            -> []
        CCall CExpr
f [CExpr]
args NodeInfo
_    -> CExpr -> [String]
exprAddrs CExpr
f [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
argAddrs [CExpr]
args
        CExpr
e                 -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
exprAddrs (CExpr -> [CExpr]
exprChildren CExpr
e)
    argAddrs :: CExpr -> [String]
argAddrs CExpr
a = case CExpr -> Maybe CExpr
passedAddress CExpr
a of
        Just CExpr
e  -> CExpr -> [String]
exprAddrs CExpr
e
        Maybe CExpr
Nothing -> CExpr -> [String]
exprAddrs CExpr
a

-- | The expression whose address an argument passes.
passedAddress :: CExpr -> Maybe CExpr
passedAddress :: CExpr -> Maybe CExpr
passedAddress = \case
    CCast CDeclaration NodeInfo
_ CExpr
e NodeInfo
_       -> CExpr -> Maybe CExpr
passedAddress CExpr
e
    CUnary CUnaryOp
CAdrOp CExpr
e NodeInfo
_ -> CExpr -> Maybe CExpr
forall a. a -> Maybe a
Just CExpr
e
    CExpr
_                 -> Maybe CExpr
forall a. Maybe a
Nothing

-- | The variable whose memory an expression is in, if any.
addressed :: CExpr -> [String]
addressed :: CExpr -> [String]
addressed = \case
    CVar Ident
i NodeInfo
_        -> [Ident -> String
identToString Ident
i]
    CMember CExpr
e Ident
_ Bool
_ NodeInfo
_ -> CExpr -> [String]
addressed CExpr
e
    CIndex CExpr
e CExpr
_ NodeInfo
_    -> CExpr -> [String]
addressed CExpr
e
    CExpr
_               -> []

-- | 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.
canWrap :: FunDef -> Bool
canWrap :: FunDef -> Bool
canWrap (FunDef VarDecl
_ Stmt
body NodeInfo
_) = (CExpr -> Bool) -> [CExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((CExpr -> Bool) -> [CExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CExpr -> Bool
forall {a}. CExpression a -> Bool
wraps ([CExpr] -> Bool) -> (CExpr -> [CExpr]) -> CExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CExpr -> [CExpr]
everyExpr) (Stmt -> [CExpr]
statExprs Stmt
body)
  where
    everyExpr :: CExpr -> [CExpr]
everyExpr CExpr
e = CExpr
e CExpr -> [CExpr] -> [CExpr]
forall a. a -> [a] -> [a]
: (CExpr -> [CExpr]) -> [CExpr] -> [CExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [CExpr]
everyExpr (CExpr -> [CExpr]
exprChildren CExpr
e)
    wraps :: CExpression a -> Bool
wraps = \case
        CBinary CBinaryOp
CSubOp CExpression a
_ CExpression a
_ a
_    -> Bool
True
        CAssign CAssignOp
CSubAssOp CExpression a
_ CExpression a
_ a
_ -> Bool
True
        CUnary CUnaryOp
CPreDecOp CExpression a
_ a
_    -> Bool
True
        CUnary CUnaryOp
CPostDecOp CExpression a
_ a
_   -> Bool
True
        CUnary CUnaryOp
CMinOp CExpression a
_ a
_       -> Bool
True
        CExpression a
_                       -> Bool
False

nodeTermsOf :: MonadTrav m => Scope -> Node -> m NodeTerms
nodeTermsOf :: forall (m :: * -> *). MonadTrav m => Scope -> Node -> m NodeTerms
nodeTermsOf Scope
scope (Node Int
_ NodeKind
kind) = case NodeKind
kind of
    StatNode (CExpr Maybe CExpr
e NodeInfo
_) -> [Term] -> NodeTerms
Evaluates ([Term] -> NodeTerms) -> m [Term] -> m NodeTerms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope) ([CExpr] -> (CExpr -> [CExpr]) -> Maybe CExpr -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CExpr -> [CExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe CExpr
e)
    StatNode (CReturn Maybe CExpr
e NodeInfo
_) -> [Term] -> NodeTerms
Evaluates ([Term] -> NodeTerms) -> m [Term] -> m NodeTerms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope) ([CExpr] -> (CExpr -> [CExpr]) -> Maybe CExpr -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CExpr -> [CExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe CExpr
e)
    StatNode CBreak{} -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
    StatNode CCont{} -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
    StatNode CGoto{} -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
    StatNode CFor{} -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
    StatNode Stmt
_ -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NodeTerms
Opaque
    ExprNode CExpr
e -> [Term] -> NodeTerms
Evaluates ([Term] -> NodeTerms) -> (Term -> [Term]) -> Term -> NodeTerms
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> NodeTerms) -> m Term -> m NodeTerms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope CExpr
e
    BranchNode CExpr
e -> [Term] -> NodeTerms
Evaluates ([Term] -> NodeTerms) -> (Term -> [Term]) -> Term -> NodeTerms
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> NodeTerms) -> m Term -> m NodeTerms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope CExpr
e
    DeclNode (CDecl [CDeclarationSpecifier NodeInfo]
_ [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds NodeInfo
_) -> do
        [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
items <- [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
-> ((Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
     Maybe CExpr)
    -> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term]))
-> m [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
  Maybe CExpr)]
ds (((Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
   Maybe CExpr)
  -> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term]))
 -> m [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])])
-> ((Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
     Maybe CExpr)
    -> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term]))
-> m [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
forall a b. (a -> b) -> a -> b
$ \case
            (Just (CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
derived Maybe AsmName
_ [CAttribute NodeInfo]
_ NodeInfo
ni), Just (CInitExpr CExpr
e NodeInfo
_), Maybe CExpr
_) -> do
                Maybe IntTy
ty <- (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> m (Maybe Type) -> m (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe Type)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Type)
exprType (Ident -> NodeInfo -> CExpr
forall a. Ident -> a -> CExpression a
CVar Ident
i NodeInfo
ni)
                [Term]
sizes <- [CDerivedDeclarator NodeInfo] -> m [Term]
forall {m :: * -> *}.
MonadTrav m =>
[CDerivedDeclarator NodeInfo] -> m [Term]
arraySizes [CDerivedDeclarator NodeInfo]
derived
                Term
t <- Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope CExpr
e
                let path :: Maybe AccessPath
path = if Ident -> String
identToString Ident
i String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Scope -> Set String
trackable Scope
scope then AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just (String -> AccessPath
PathVar (Ident -> String
identToString Ident
i)) else Maybe AccessPath
forall a. Maybe a
Nothing
                    var :: Term
var = CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term (Ident -> NodeInfo -> CExpr
forall a. Ident -> a -> CExpression a
CVar Ident
i NodeInfo
ni) Maybe IntTy
ty Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (TermKind
-> (AccessPath -> TermKind) -> Maybe AccessPath -> TermKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Term] -> TermKind
TOther []) AccessPath -> TermKind
TLoad Maybe AccessPath
path)
                    assign :: Term
assign = CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term (CAssignOp -> CExpr -> CExpr -> NodeInfo -> CExpr
forall a.
CAssignOp -> CExpression a -> CExpression a -> a -> CExpression a
CAssign CAssignOp
CAssignOp (Ident -> NodeInfo -> CExpr
forall a. Ident -> a -> CExpression a
CVar Ident
i NodeInfo
ni) CExpr
e NodeInfo
ni) Maybe IntTy
ty Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (Maybe AccessPath -> CAssignOp -> Term -> Term -> TermKind
TAssign Maybe AccessPath
path CAssignOp
CAssignOp Term
var Term
t)
                ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
-> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [ (AccessPath
p, IntTy
vt, Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t) | Just AccessPath
p <- [Maybe AccessPath
path], Just IntTy
vt <- [Maybe IntTy
ty] ], [Term]
sizes [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
t]
                       , [Term]
sizes [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term -> (IntTy -> Term) -> Maybe IntTy -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
t (Term -> IntTy -> Term
forall a b. a -> b -> a
const Term
assign) Maybe IntTy
ty] )
            (Just (CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
derived Maybe AsmName
_ [CAttribute NodeInfo]
_ NodeInfo
ni), Maybe (CInitializer NodeInfo)
ini, Maybe CExpr
_) -> do
                Maybe IntTy
ty <- (Maybe Type -> (Type -> Maybe IntTy) -> Maybe IntTy
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe IntTy
intType) (Maybe Type -> Maybe IntTy) -> m (Maybe Type) -> m (Maybe IntTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpr -> m (Maybe Type)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Type)
exprType (Ident -> NodeInfo -> CExpr
forall a. Ident -> a -> CExpression a
CVar Ident
i NodeInfo
ni)
                [Term]
sizes <- [CDerivedDeclarator NodeInfo] -> m [Term]
forall {m :: * -> *}.
MonadTrav m =>
[CDerivedDeclarator NodeInfo] -> m [Term]
arraySizes [CDerivedDeclarator NodeInfo]
derived
                [Term]
ts <- (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope) ([CExpr]
-> (CInitializer NodeInfo -> [CExpr])
-> Maybe (CInitializer NodeInfo)
-> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CInitializer NodeInfo -> [CExpr]
initExprs Maybe (CInitializer NodeInfo)
ini)
                ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
-> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [ (String -> AccessPath
PathVar (Ident -> String
identToString Ident
i), IntTy
vt, Maybe Term
forall a. Maybe a
Nothing) | Just IntTy
vt <- [Maybe IntTy
ty], Ident -> String
identToString Ident
i String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Scope -> Set String
trackable Scope
scope ]
                       , [Term]
sizes [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
ts, [Term]
sizes [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
ts )
            (Maybe (CDeclarator NodeInfo)
_, Maybe (CInitializer NodeInfo)
ini, Maybe CExpr
_) -> do
                [Term]
ts <- (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope) ([CExpr]
-> (CInitializer NodeInfo -> [CExpr])
-> Maybe (CInitializer NodeInfo)
-> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CInitializer NodeInfo -> [CExpr]
initExprs Maybe (CInitializer NodeInfo)
ini)
                ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
-> m ([(AccessPath, IntTy, Maybe Term)], [Term], [Term])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Term]
ts, [Term]
ts)
        NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeTerms -> m NodeTerms) -> NodeTerms -> m NodeTerms
forall a b. (a -> b) -> a -> b
$ [(AccessPath, IntTy, Maybe Term)] -> [Term] -> [Term] -> NodeTerms
Declares ([[(AccessPath, IntTy, Maybe Term)]]
-> [(AccessPath, IntTy, Maybe Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(AccessPath, IntTy, Maybe Term)]
v | ([(AccessPath, IntTy, Maybe Term)]
v, [Term]
_, [Term]
_) <- [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
items ]) ([[Term]] -> [Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Term]
e | ([(AccessPath, IntTy, Maybe Term)]
_, [Term]
e, [Term]
_) <- [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
items ])
            ([[Term]] -> [Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Term]
c | ([(AccessPath, IntTy, Maybe Term)]
_, [Term]
_, [Term]
c) <- [([(AccessPath, IntTy, Maybe Term)], [Term], [Term])]
items ])
    DeclNode CDeclaration NodeInfo
_ -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NodeTerms
Opaque
    NodeKind
EntryNode -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
    NodeKind
ExitNode -> NodeTerms -> m NodeTerms
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> NodeTerms
Evaluates [])
  where
    -- A variable length array's declaration evaluates its size.
    arraySizes :: [CDerivedDeclarator NodeInfo] -> m [Term]
arraySizes [CDerivedDeclarator NodeInfo]
derived = (CExpr -> m Term) -> [CExpr] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Scope -> CExpr -> m Term
forall (m :: * -> *). MonadTrav m => Scope -> CExpr -> m Term
term Scope
scope) [ CExpr
e | CArrDeclr [CTypeQualifier NodeInfo]
_ (CArrSize Bool
_ CExpr
e) NodeInfo
_ <- [CDerivedDeclarator NodeInfo]
derived ]

mapTerms :: (Term -> Term) -> NodeTerms -> NodeTerms
mapTerms :: (Term -> Term) -> NodeTerms -> NodeTerms
mapTerms Term -> Term
f = \case
    Evaluates [Term]
ts           -> [Term] -> NodeTerms
Evaluates ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
f [Term]
ts)
    Declares [(AccessPath, IntTy, Maybe Term)]
vars [Term]
inits [Term]
ts -> [(AccessPath, IntTy, Maybe Term)] -> [Term] -> [Term] -> NodeTerms
Declares [ (AccessPath
p, IntTy
ty, Term -> Term
f (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Term
t) | (AccessPath
p, IntTy
ty, Maybe Term
t) <- [(AccessPath, IntTy, Maybe Term)]
vars ] ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
f [Term]
inits) ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
f [Term]
ts)
    NodeTerms
Opaque                 -> NodeTerms
Opaque

termsOf :: NodeTerms -> [Term]
termsOf :: NodeTerms -> [Term]
termsOf = \case
    Evaluates [Term]
ts    -> [Term]
ts
    Declares [(AccessPath, IntTy, Maybe Term)]
_ [Term]
_ [Term]
ts -> [Term]
ts
    NodeTerms
Opaque          -> []

transferTerms :: NodeTerms -> Facts -> Facts
transferTerms :: NodeTerms -> Facts -> Facts
transferTerms NodeTerms
nt Facts
facts = case NodeTerms
nt of
    Evaluates [Term]
ts -> (Facts -> Term -> Facts) -> Facts -> [Term] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Term -> Facts -> Facts) -> Facts -> Term -> Facts
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Term -> Facts -> Facts
effects Bool
True)) Facts
facts [Term]
ts
    Declares [(AccessPath, IntTy, Maybe Term)]
vars [Term]
inits [Term]
_ ->
        let after :: Facts
after = (Facts -> Term -> Facts) -> Facts -> [Term] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Term -> Facts -> Facts) -> Facts -> Term -> Facts
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Term -> Facts -> Facts
effects Bool
True)) Facts
facts [Term]
inits
        in (Facts -> (AccessPath, IntTy, Maybe Term) -> Facts)
-> Facts -> [(AccessPath, IntTy, Maybe Term)] -> Facts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Facts
f (AccessPath
p, IntTy
ty, Maybe Term
ini) -> case Maybe Term
ini Maybe Term -> (Term -> Maybe [Range]) -> Maybe [Range]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Facts -> Term -> Maybe [Range]
eval Facts
facts of
                     Just [Range]
v  -> AccessPath -> IntTy -> [Range] -> Facts -> Facts
setPath AccessPath
p IntTy
ty ([Range] -> [Range]
normalise ((Range -> [Range]) -> [Range] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NodeInfo -> IntTy -> Range -> [Range]
convert (Maybe Term -> NodeInfo
initSite Maybe Term
ini) IntTy
ty) [Range]
v)) Facts
f
                     Maybe [Range]
Nothing -> AccessPath -> Facts -> Facts
forget AccessPath
p Facts
f) Facts
after [(AccessPath, IntTy, Maybe Term)]
vars
    NodeTerms
Opaque -> Facts -> Facts
forgetAll Facts
facts
  where
    initSite :: Maybe Term -> NodeInfo
initSite = NodeInfo -> (Term -> NodeInfo) -> Maybe Term -> NodeInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe NodeInfo
undefNode (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation (CExpr -> NodeInfo) -> (Term -> CExpr) -> Term -> NodeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> CExpr
termExpr)

-- | A function as the analysis sees it: its control flow graph and the terms
-- each node evaluates.
data Function = Function
    { Function -> Node
fnEntry  :: Node
    , Function -> CFG
fnCfg    :: CFG
    , Function -> Map Node NodeTerms
fnTerms  :: Map Node NodeTerms
    , Function -> Map Name Integer
fnCases  :: Map Name Integer
    -- ^ The value of each case label.
    , Function -> [Maybe (AccessPath, IntTy)]
fnParams :: [Maybe (AccessPath, IntTy)]
    -- ^ The paths of the parameters the analysis tracks.
    , Function -> Maybe String
fnSelf   :: Maybe String
    }

-- | A function in a translation unit, given the declarations of its locals.
translate :: MonadTrav m => FilePath -> [IdentDecl] -> FunDef -> m Function
translate :: forall (m :: * -> *).
MonadTrav m =>
String -> [IdentDecl] -> FunDef -> m Function
translate String
unit [IdentDecl]
locals fd :: FunDef
fd@(FunDef VarDecl
decl Stmt
_ NodeInfo
ni) = do
    m ()
forall (m :: * -> *). MonadSymtab m => m ()
enterFunctionScope
    NodeInfo -> VarDecl -> m ()
forall (m :: * -> *). MonadTrav m => NodeInfo -> VarDecl -> m ()
defineParams NodeInfo
ni VarDecl
decl
    m ()
forall (m :: * -> *). MonadSymtab m => m ()
enterBlockScope
    [IdentDecl] -> (IdentDecl -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [IdentDecl]
locals ((IdentDecl -> m ()) -> m ()) -> (IdentDecl -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \IdentDecl
d -> (DefTable -> ((), DefTable)) -> m ()
forall a. (DefTable -> (a, DefTable)) -> m a
forall (m :: * -> *) a.
MonadSymtab m =>
(DefTable -> (a, DefTable)) -> m a
withDefTable ((DefTable -> ((), DefTable)) -> m ())
-> (DefTable -> ((), DefTable)) -> m ()
forall a b. (a -> b) -> a -> b
$ \DefTable
dt -> ((), (DeclarationStatus IdentEntry, DefTable) -> DefTable
forall a b. (a, b) -> b
snd (Ident
-> IdentDecl
-> DefTable
-> (DeclarationStatus IdentEntry, DefTable)
defineScopedIdent (IdentDecl -> Ident
forall n. Declaration n => n -> Ident
declIdent IdentDecl
d) IdentDecl
d DefTable
dt))
    Function
result <- String -> FunDef -> m Function
forall (m :: * -> *). MonadTrav m => String -> FunDef -> m Function
translateBody String
unit FunDef
fd
    m ()
forall (m :: * -> *). MonadSymtab m => m ()
leaveBlockScope
    m ()
forall (m :: * -> *). MonadSymtab m => m ()
leaveFunctionScope
    Function -> m Function
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Function
result

translateBody :: MonadTrav m => FilePath -> FunDef -> m Function
translateBody :: forall (m :: * -> *). MonadTrav m => String -> FunDef -> m Function
translateBody String
unit fd :: FunDef
fd@(FunDef (VarDecl VarName
self DeclAttrs
_ Type
ty) Stmt
body NodeInfo
_) = do
    let (Node
entry, CFG
cfg) = FunDef -> (Node, CFG)
fromFunDef FunDef
fd
        nodes :: [Node]
nodes = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> ([Node] -> Set Node) -> [Node] -> [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ CFG -> [Node]
forall k a. Map k a -> [k]
Map.keys CFG
cfg [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [ Node
n | [Edge]
es <- CFG -> [[Edge]]
forall k a. Map k a -> [a]
Map.elems CFG
cfg, (EdgeType
_, Node
n) <- [Edge]
es ]
        declared :: [String]
declared = FunDef -> [String]
paramNames FunDef
fd [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Stmt -> [String]
declaredNames Stmt
body
        counts :: Map String Int
counts = (Int -> Int -> Int) -> [(String, Int)] -> Map String Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) [ (String
n, Int
1 :: Int) | String
n <- [String]
declared ]
        scope :: Scope
scope = Scope
            { trackable :: Set String
trackable = Map String Int -> Set String
forall k a. Map k a -> Set k
Map.keysSet ((Int -> Bool) -> Map String Int -> Map String Int
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) Map String Int
counts)
                Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` (Stmt -> Set String
addressTaken Stmt
body Set String -> Set String -> Set String
forall a. Semigroup a => a -> a -> a
<> Stmt -> Set String
storedElsewhere Stmt
body)
            , scopeUnit :: String
scopeUnit = String
unit
            }
    Map Node NodeTerms
terms <- [(Node, NodeTerms)] -> Map Node NodeTerms
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Node, NodeTerms)] -> Map Node NodeTerms)
-> m [(Node, NodeTerms)] -> m (Map Node NodeTerms)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Node] -> (Node -> m (Node, NodeTerms)) -> m [(Node, NodeTerms)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Node]
nodes (\Node
n -> (,) Node
n (NodeTerms -> (Node, NodeTerms))
-> m NodeTerms -> m (Node, NodeTerms)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope -> Node -> m NodeTerms
forall (m :: * -> *). MonadTrav m => Scope -> Node -> m NodeTerms
nodeTermsOf Scope
scope Node
n)
    Maybe String
selfKey <- case VarName
self of
        VarName Ident
i Maybe AsmName
_ -> String -> Ident -> m (Maybe String)
forall (m :: * -> *).
MonadTrav m =>
String -> Ident -> m (Maybe String)
funKey String
unit Ident
i
        VarName
NoName      -> Maybe String -> m (Maybe String)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
    Map Name Integer
caseValues <- CFG -> m (Map Name Integer)
forall (m :: * -> *). MonadTrav m => CFG -> m (Map Name Integer)
caseConstants CFG
cfg
    Function -> m Function
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Function
        { fnEntry :: Node
fnEntry = Node
entry
        , fnCfg :: CFG
fnCfg = CFG
cfg
        , fnTerms :: Map Node NodeTerms
fnTerms = Map Node NodeTerms
terms
        , fnCases :: Map Name Integer
fnCases = Map Name Integer
caseValues
        , fnParams :: [Maybe (AccessPath, IntTy)]
fnParams =
            [ case (ParamDecl -> VarName
paramVarName ParamDecl
p, Type -> Maybe IntTy
intType (ParamDecl -> Type
forall n. Declaration n => n -> Type
declType ParamDecl
p)) of
                (VarName Ident
i Maybe AsmName
_, Just IntTy
t) | Ident -> String
identToString Ident
i String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Scope -> Set String
trackable Scope
scope -> (AccessPath, IntTy) -> Maybe (AccessPath, IntTy)
forall a. a -> Maybe a
Just (String -> AccessPath
PathVar (Ident -> String
identToString Ident
i), IntTy
t)
                (VarName, Maybe IntTy)
_ -> Maybe (AccessPath, IntTy)
forall a. Maybe a
Nothing
            | FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_ <- [Type
ty], ParamDecl
p <- [ParamDecl]
params ]
        , fnSelf :: Maybe String
fnSelf = Maybe String
selfKey
        }
  where
    caseConstants :: MonadTrav m => CFG -> m (Map Name Integer)
    caseConstants :: forall (m :: * -> *). MonadTrav m => CFG -> m (Map Name Integer)
caseConstants CFG
cfg = ([[(Name, Integer)]] -> Map Name Integer)
-> m [[(Name, Integer)]] -> m (Map Name Integer)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Integer)] -> Map Name Integer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Integer)] -> Map Name Integer)
-> ([[(Name, Integer)]] -> [(Name, Integer)])
-> [[(Name, Integer)]]
-> Map Name Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Name, Integer)]] -> [(Name, Integer)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (m [[(Name, Integer)]] -> m (Map Name Integer))
-> ((CExpr -> m [(Name, Integer)]) -> m [[(Name, Integer)]])
-> (CExpr -> m [(Name, Integer)])
-> m (Map Name Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CExpr] -> (CExpr -> m [(Name, Integer)]) -> m [[(Name, Integer)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ CExpr
v | [Edge]
es <- CFG -> [[Edge]]
forall k a. Map k a -> [a]
Map.elems CFG
cfg, (CaseBranch CExpr
v, Node
_) <- [Edge]
es ] ((CExpr -> m [(Name, Integer)]) -> m (Map Name Integer))
-> (CExpr -> m [(Name, Integer)]) -> m (Map Name Integer)
forall a b. (a -> b) -> a -> b
$ \CExpr
v ->
        CExpr -> m (Maybe Integer)
forall (m :: * -> *). MonadTrav m => CExpr -> m (Maybe Integer)
constValue CExpr
v m (Maybe Integer)
-> (Maybe Integer -> m [(Name, Integer)]) -> m [(Name, Integer)]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe Integer
k -> [(Name, Integer)] -> m [(Name, Integer)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Name
n, Integer
x) | Just Name
n <- [NodeInfo -> Maybe Name
nameOfNode (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CExpr
v)], Just Integer
x <- [Maybe Integer
k] ]

-- | Whether what is known about the program says more about a function than
-- knowing nothing about it.
dependsOn :: Program -> Function -> Bool
dependsOn :: Program -> Function -> Bool
dependsOn Program
prog Function
fn = Bool -> (String -> Bool) -> Maybe String -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (String -> Map String [Maybe [Range]] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Program -> Map String [Maybe [Range]]
progParams Program
prog) (Function -> Maybe String
fnSelf Function
fn)
    Bool -> Bool -> Bool
|| (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> (Fact -> Bool) -> Maybe Fact -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Fact -> Bool
known (Maybe Fact -> Bool) -> (Term -> Maybe Fact) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Fact
termFact) ((NodeTerms -> [Term]) -> [NodeTerms] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Term -> [Term]) -> [Term] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [Term]
subTerms ([Term] -> [Term]) -> (NodeTerms -> [Term]) -> NodeTerms -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeTerms -> [Term]
termsOf) (Map Node NodeTerms -> [NodeTerms]
forall k a. Map k a -> [a]
Map.elems (Function -> Map Node NodeTerms
fnTerms Function
fn)))
  where
    known :: Fact -> Bool
known = \case
        FieldFact FieldKey
k -> FieldKey
k FieldKey -> Map FieldKey [Range] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Program -> Map FieldKey [Range]
progFields Program
prog
        CallFact String
k  -> String
k String -> Map String [Range] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Program -> Map String [Range]
progReturns Program
prog

-- | A term with its defaults from what is known about the program.
withProgram :: Program -> Term -> Term
withProgram :: Program -> Term -> Term
withProgram Program
prog = Term -> Term
go
  where
    go :: Term -> Term
go Term
t = Term
t { termDefault = termFact t >>= known, termKind = kind (termKind t) }
    kind :: TermKind -> TermKind
kind = \case
        TBin CBinaryOp
op Term
a Term
b      -> CBinaryOp -> Term -> Term -> TermKind
TBin CBinaryOp
op (Term -> Term
go Term
a) (Term -> Term
go Term
b)
        TUnary CUnaryOp
op Term
a      -> CUnaryOp -> Term -> TermKind
TUnary CUnaryOp
op (Term -> Term
go Term
a)
        TCast Term
a          -> Term -> TermKind
TCast (Term -> Term
go Term
a)
        TCond Term
c Maybe Term
m Term
f      -> Term -> Maybe Term -> Term -> TermKind
TCond (Term -> Term
go Term
c) (Term -> Term
go (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Term
m) (Term -> Term
go Term
f)
        TAssign Maybe AccessPath
p CAssignOp
op Term
l Term
r -> Maybe AccessPath -> CAssignOp -> Term -> Term -> TermKind
TAssign Maybe AccessPath
p CAssignOp
op (Term -> Term
go Term
l) (Term -> Term
go Term
r)
        TIndex Term
a Term
i Maybe Integer
n     -> Term -> Term -> Maybe Integer -> TermKind
TIndex (Term -> Term
go Term
a) (Term -> Term
go Term
i) Maybe Integer
n
        TCall Term
f [Term]
args     -> Term -> [Term] -> TermKind
TCall (Term -> Term
go Term
f) ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
go [Term]
args)
        TOther [Term]
ts        -> [Term] -> TermKind
TOther ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
go [Term]
ts)
        TermKind
k                -> TermKind
k
    known :: Fact -> Maybe [Range]
known = \case
        FieldFact FieldKey
k -> FieldKey -> Map FieldKey [Range] -> Maybe [Range]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FieldKey
k (Program -> Map FieldKey [Range]
progFields Program
prog)
        CallFact String
k  -> String -> Map String [Range] -> Maybe [Range]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
k (Program -> Map String [Range]
progReturns Program
prog)

-- | The facts before each reachable node of a function, with the terms the
-- node evaluates, given what is known about the program.
solveFunction :: Program -> Function -> [(Node, Facts, [Term])]
solveFunction :: Program -> Function -> [(Node, Facts, [Term])]
solveFunction Program
prog Function
fn = [ (Node
n, Facts
facts, NodeTerms -> [Term]
termsOf (Node -> NodeTerms
termsAt Node
n)) | (Node
n, Just Facts
facts) <- Map Node (Maybe Facts) -> [(Node, Maybe Facts)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node (Maybe Facts)
result ]
  where
    entry :: Node
entry = Function -> Node
fnEntry Function
fn
    cfg :: CFG
cfg = Function -> CFG
fnCfg Function
fn
    terms :: Map Node NodeTerms
terms = (NodeTerms -> NodeTerms)
-> Map Node NodeTerms -> Map Node NodeTerms
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Term -> Term) -> NodeTerms -> NodeTerms
mapTerms (Program -> Term -> Term
withProgram Program
prog)) (Function -> Map Node NodeTerms
fnTerms Function
fn)
    entryFacts :: Facts
entryFacts = [Maybe (AccessPath, IntTy)] -> Maybe [Maybe [Range]] -> Facts
paramFacts (Function -> [Maybe (AccessPath, IntTy)]
fnParams Function
fn) (Function -> Maybe String
fnSelf Function
fn Maybe String
-> (String -> Maybe [Maybe [Range]]) -> Maybe [Maybe [Range]]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (String -> Map String [Maybe [Range]] -> Maybe [Maybe [Range]]
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Program -> Map String [Maybe [Range]]
progParams Program
prog))
    termsAt :: Node -> NodeTerms
termsAt Node
n = NodeTerms -> Node -> Map Node NodeTerms -> NodeTerms
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Term] -> NodeTerms
Evaluates []) Node
n Map Node NodeTerms
terms
    -- The constants branch conditions compare paths against, shifted by what
    -- they add to the paths, and their neighbours.
    bounds :: Map AccessPath (Set Integer)
bounds = (Set Integer -> Set Integer -> Set Integer)
-> [(AccessPath, Set Integer)] -> Map AccessPath (Set Integer)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.union
        [ (AccessPath
p, [Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [ Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d | Integer
d <- [-Integer
1, Integer
0, Integer
1] ])
        | (Node Int
_ BranchNode{}, NodeTerms
nt) <- Map Node NodeTerms -> [(Node, NodeTerms)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node NodeTerms
terms, Term
t <- (Term -> [Term]) -> [Term] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [Term]
subTerms (NodeTerms -> [Term]
termsOf NodeTerms
nt)
        , TBin CBinaryOp
op Term
a Term
b <- [Term -> TermKind
termKind Term
t], CBinaryOp
op CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp, CBinaryOp
CEqOp, CBinaryOp
CNeqOp]
        , (Term
x, Term
y) <- [(Term
a, Term
b), (Term
b, Term
a)]
        , Just (Just AccessPath
p, Integer
c) <- [Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
nothingKnown Term
x]
        , Just (Maybe AccessPath
Nothing, Integer
k) <- [Facts -> Term -> Maybe (Maybe AccessPath, Integer)
linear Facts
nothingKnown Term
y] ]
    nothingKnown :: Facts
nothingKnown = Int
-> Bool
-> Map AccessPath (IntTy, [Range])
-> Map (AccessPath, AccessPath) Integer
-> Facts
Facts Int
0 Bool
False Map AccessPath (IntTy, [Range])
forall k a. Map k a
Map.empty Map (AccessPath, AccessPath) Integer
forall k a. Map k a
Map.empty
    condOf :: Node -> Maybe Term
condOf Node
n = case Node -> NodeTerms
termsAt Node
n of
        Evaluates [Term
c] | Node Int
_ BranchNode{} <- Node
n -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
c
        NodeTerms
_                                        -> Maybe Term
forall a. Maybe a
Nothing
    back :: Set (Node, Node)
back = Node -> CFG -> Set (Node, Node)
backEdges Node
entry CFG
cfg
    isBack :: Node -> EdgeType -> Bool
isBack Node
n EdgeType
e = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ (Node
n, Node
v) (Node, Node) -> Set (Node, Node) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Node, Node)
back | (EdgeType
e', Node
v) <- [Edge] -> Node -> CFG -> [Edge]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg, EdgeType -> EdgeType -> Bool
sameEdge EdgeType
e EdgeType
e' ]
    edgeTransferNode :: Node -> EdgeType -> Maybe Facts -> Maybe Facts
edgeTransferNode Node
n EdgeType
e Maybe Facts
s = (\Facts
f -> Facts
f { factsBackEdge = isBack n e }) (Facts -> Facts) -> Maybe Facts -> Maybe Facts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe Facts
s Maybe Facts -> (Facts -> Maybe Facts) -> Maybe Facts
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Facts
facts -> case (Node -> Maybe Term
condOf Node
n, EdgeType
e) of
        (Just Term
c, EdgeType
TrueBranch) -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
True Term
c Facts
facts
        (Just Term
c, EdgeType
FalseBranch) -> Bool -> Term -> Facts -> Maybe Facts
assume Bool
False Term
c Facts
facts
        (Just Term
c, CaseBranch CExpr
v) | Just Integer
k <- CExpr -> Maybe Integer
forall {ast :: * -> *}.
Annotated ast =>
ast NodeInfo -> Maybe Integer
caseValue CExpr
v ->
            CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts CBinaryOp
CEqOp Term
c (CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term CExpr
v (Term -> Maybe IntTy
termTy Term
c) Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (Integer -> TermKind
TConst Integer
k)) Facts
facts
        (Just Term
c, EdgeType
DefaultBranch) ->
            (Facts -> (CExpr, Integer) -> Maybe Facts)
-> Facts -> [(CExpr, Integer)] -> Maybe Facts
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Facts
f (CExpr
v, Integer
k) -> CBinaryOp -> Term -> Term -> Facts -> Maybe Facts
compareFacts CBinaryOp
CNeqOp Term
c (CExpr
-> Maybe IntTy -> Maybe Fact -> Maybe [Range] -> TermKind -> Term
Term CExpr
v (Term -> Maybe IntTy
termTy Term
c) Maybe Fact
forall a. Maybe a
Nothing Maybe [Range]
forall a. Maybe a
Nothing (Integer -> TermKind
TConst Integer
k)) Facts
f) Facts
facts
                [ (CExpr
v, Integer
k) | (CaseBranch CExpr
v, Node
_) <- [Edge] -> Node -> CFG -> [Edge]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg, Just Integer
k <- [CExpr -> Maybe Integer
forall {ast :: * -> *}.
Annotated ast =>
ast NodeInfo -> Maybe Integer
caseValue CExpr
v] ]
        (Maybe Term, EdgeType)
_ -> Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
facts)
      where caseValue :: ast NodeInfo -> Maybe Integer
caseValue ast NodeInfo
v = NodeInfo -> Maybe Name
nameOfNode (ast NodeInfo -> NodeInfo
forall a. ast a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation ast NodeInfo
v) Maybe Name -> (Name -> Maybe Integer) -> Maybe Integer
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Name -> Map Name Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Function -> Map Name Integer
fnCases Function
fn)
    problem :: Dataflow Node EdgeType (Maybe Facts)
problem = Dataflow
        { transfer :: Node -> Maybe Facts -> Maybe Facts
transfer     = \Node
n Maybe Facts
s -> if Node -> Bool
endsPath Node
n then Maybe Facts
forall a. Maybe a
Nothing else (\Facts
f -> (NodeTerms -> Facts -> Facts
transferTerms (Node -> NodeTerms
termsAt Node
n) Facts
f) { factsBackEdge = False }) (Facts -> Facts) -> Maybe Facts -> Maybe Facts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Facts
s
        , edgeTransfer :: Node -> EdgeType -> Maybe Facts -> Maybe Facts
edgeTransfer = Node -> EdgeType -> Maybe Facts -> Maybe Facts
edgeTransferNode
        , merge :: Maybe Facts -> Maybe Facts -> Maybe Facts
merge        = Map AccessPath (Set Integer)
-> Maybe Facts -> Maybe Facts -> Maybe Facts
mergeFacts Map AccessPath (Set Integer)
bounds
        , initial :: Maybe Facts
initial      = Facts -> Maybe Facts
forall a. a -> Maybe a
Just Facts
entryFacts
        }
    result :: Map Node (Maybe Facts)
result = Node
-> CFG
-> Dataflow Node EdgeType (Maybe Facts)
-> Map Node (Maybe Facts)
forall node state edge.
(Ord node, Eq state) =>
node
-> Map node [(edge, node)]
-> Dataflow node edge state
-> Map node state
solve Node
entry CFG
cfg Dataflow Node EdgeType (Maybe Facts)
problem

sameEdge :: EdgeType -> EdgeType -> Bool
sameEdge :: EdgeType -> EdgeType -> Bool
sameEdge (CaseBranch CExpr
a) (CaseBranch CExpr
b) = NodeInfo -> Maybe Name
nameOfNode (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CExpr
a) Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== NodeInfo -> Maybe Name
nameOfNode (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CExpr
b)
sameEdge EdgeType
a EdgeType
b                           = EdgeType
a EdgeType -> EdgeType -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeType
b

-- | The edges that go back to a node the depth-first search from the entry is
-- still inside. Every cycle in the graph has one.
backEdges :: Node -> CFG -> Set (Node, Node)
backEdges :: Node -> CFG -> Set (Node, Node)
backEdges Node
entry CFG
cfg = (Set Node, Set (Node, Node)) -> Set (Node, Node)
forall a b. (a, b) -> b
snd (Set Node
-> Node
-> (Set Node, Set (Node, Node))
-> (Set Node, Set (Node, Node))
visit Set Node
forall a. Set a
Set.empty Node
entry (Set Node
forall a. Set a
Set.empty, Set (Node, Node)
forall a. Set a
Set.empty))
  where
    visit :: Set Node
-> Node
-> (Set Node, Set (Node, Node))
-> (Set Node, Set (Node, Node))
visit Set Node
stack Node
n acc :: (Set Node, Set (Node, Node))
acc@(Set Node
done, Set (Node, Node)
back)
        | Node
n Node -> Set Node -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Node
done = (Set Node, Set (Node, Node))
acc
        | Bool
otherwise =
            let stack' :: Set Node
stack' = Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert Node
n Set Node
stack
                step :: (Set Node, Set (Node, Node))
-> (a, Node) -> (Set Node, Set (Node, Node))
step acc' :: (Set Node, Set (Node, Node))
acc'@(Set Node
d, Set (Node, Node)
b) (a
_, Node
m)
                    | Node
m Node -> Set Node -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Node
stack' = (Set Node
d, (Node, Node) -> Set (Node, Node) -> Set (Node, Node)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Node
n, Node
m) Set (Node, Node)
b)
                    | Bool
otherwise = Set Node
-> Node
-> (Set Node, Set (Node, Node))
-> (Set Node, Set (Node, Node))
visit Set Node
stack' Node
m (Set Node, Set (Node, Node))
acc'
                (Set Node
done', Set (Node, Node)
back') = ((Set Node, Set (Node, Node))
 -> Edge -> (Set Node, Set (Node, Node)))
-> (Set Node, Set (Node, Node))
-> [Edge]
-> (Set Node, Set (Node, Node))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Set Node, Set (Node, Node))
-> Edge -> (Set Node, Set (Node, Node))
forall {a}.
(Set Node, Set (Node, Node))
-> (a, Node) -> (Set Node, Set (Node, Node))
step (Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert Node
n Set Node
done, Set (Node, Node)
back) ([Edge] -> Node -> CFG -> [Edge]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg)
            in (Set Node
done', Set (Node, Node)
back')

-- | The facts at the entry of a function whose parameters are known to have
-- the given values.
paramFacts :: [Maybe (AccessPath, IntTy)] -> Maybe [Maybe [Range]] -> Facts
paramFacts :: [Maybe (AccessPath, IntTy)] -> Maybe [Maybe [Range]] -> Facts
paramFacts [Maybe (AccessPath, IntTy)]
params Maybe [Maybe [Range]]
known = Int
-> Bool
-> Map AccessPath (IntTy, [Range])
-> Map (AccessPath, AccessPath) Integer
-> Facts
Facts Int
0 Bool
False Map AccessPath (IntTy, [Range])
values Map (AccessPath, AccessPath) Integer
forall k a. Map k a
Map.empty
  where
    values :: Map AccessPath (IntTy, [Range])
values = [(AccessPath, (IntTy, [Range]))] -> Map AccessPath (IntTy, [Range])
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (AccessPath
p, (IntTy
t, [Range]
v)) | (Just (AccessPath
p, IntTy
t), Just [Range]
v) <- [Maybe (AccessPath, IntTy)]
-> [Maybe [Range]] -> [(Maybe (AccessPath, IntTy), Maybe [Range])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe (AccessPath, IntTy)]
params ([Maybe [Range]] -> Maybe [Maybe [Range]] -> [Maybe [Range]]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Maybe [Range]]
known) ]