{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Strict     #-}
-- | Accesses to memory through variables, and how far into it they reach.
module Tokstyle.C.Analysis.Access
    ( Access (..)
    , AccessBy (..)
    , accesses
    , changedNames
    ) where

import qualified Data.Map.Strict              as Map
import           Data.Maybe                   (isJust)
import           Data.Set                     (Set)
import qualified Data.Set                     as Set
import           Language.C.Data.Ident        (identToString)
import           Language.C.Syntax.AST
import           Language.C.Syntax.Constants  (getCInteger)
import           Tokstyle.C.Analysis.Interval (Fact (..), Program (..),
                                               Term (..), TermKind (..))
import           Tokstyle.C.Analysis.Known    (Reach (..), libraryReaches)
import           Tokstyle.C.Analysis.Syntax   (exprChildren, statExprs)

data AccessBy
    = ByElement CExpr
    | ByCall String

-- | An access through a variable: the variable, the terms, each times a
-- coefficient, and the constant whose sum is how far the access reaches, and
-- what makes it.
data Access = Access
    { Access -> String
accBuffer :: String
    , Access -> [(Integer, Term)]
accTerms  :: [(Integer, Term)]
    , Access -> Integer
accConst  :: Integer
    , Access -> AccessBy
accBy     :: AccessBy
    }

-- | The accesses a term makes, in calls to the functions in 'progReaches'
-- and the library's.
accesses :: Program -> Term -> [Access]
accesses :: Program -> Term -> [Access]
accesses Program
prog Term
t = case Term -> TermKind
termKind Term
t of
    TCall Term
f [Term]
args | CVar Ident
g NodeInfo
_ <- Term -> CExpression NodeInfo
termExpr Term
f, String
fn <- Ident -> String
identToString Ident
g, Just [Reach]
rs <- String -> Maybe [Reach]
reaches String
fn ->
        [ Access
acc
        | Reach Int
p Maybe (Int, Integer)
l Integer
c <- [Reach]
rs, Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args, ((Int, Integer) -> Bool) -> Maybe (Int, Integer) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) (Int -> Bool) -> ((Int, Integer) -> Int) -> (Int, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Integer) -> Int
forall a b. (a, b) -> a
fst) Maybe (Int, Integer)
l
        , Just Access
acc <- [String -> [(Integer, Term)] -> Integer -> Term -> Maybe Access
call String
fn [ (Integer
k, [Term]
args [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) | Just (Int
i, Integer
k) <- [Maybe (Int, Integer)
l] ] Integer
c ([Term]
args [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
p)] ]
    TermKind
_ | Just (String
b, [(Integer, Term)]
ts, Integer
k) <- Term -> Maybe (String, [(Integer, Term)], Integer)
element Term
t -> [String -> [(Integer, Term)] -> Integer -> AccessBy -> Access
Access String
b [(Integer, Term)]
ts (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (CExpression NodeInfo -> AccessBy
ByElement (Term -> CExpression NodeInfo
termExpr Term
t))]
    TermKind
_ -> []
  where
    reaches :: String -> Maybe [Reach]
reaches String
fn = case Term -> Maybe Fact
termFact Term
t of
        Just (CallFact String
k) | Just [Reach]
rs <- String -> Map String [Reach] -> Maybe [Reach]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
k (Program -> Map String [Reach]
progReaches Program
prog) -> [Reach] -> Maybe [Reach]
forall a. a -> Maybe a
Just [Reach]
rs
        Maybe Fact
_                                                             -> String -> Map String [Reach] -> Maybe [Reach]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
fn Map String [Reach]
libraryReaches
    call :: String -> [(Integer, Term)] -> Integer -> Term -> Maybe Access
call String
fn [(Integer, Term)]
ns Integer
c Term
p = case Term -> TermKind
termKind Term
p of
        TCast Term
a -> String -> [(Integer, Term)] -> Integer -> Term -> Maybe Access
call String
fn [(Integer, Term)]
ns Integer
c Term
a
        TermKind
_       -> (\(String
b, [(Integer, Term)]
ts, Integer
k) -> String -> [(Integer, Term)] -> Integer -> AccessBy -> Access
Access String
b ([(Integer, Term)]
ts [(Integer, Term)] -> [(Integer, Term)] -> [(Integer, Term)]
forall a. [a] -> [a] -> [a]
++ [(Integer, Term)]
ns) (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c) (String -> AccessBy
ByCall String
fn)) ((String, [(Integer, Term)], Integer) -> Access)
-> Maybe (String, [(Integer, Term)], Integer) -> Maybe Access
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe (String, [(Integer, Term)], Integer)
pointsInto Term
p

-- | The variable a pointer points into, and the terms and constant it adds.
pointsInto :: Term -> Maybe (String, [(Integer, Term)], Integer)
pointsInto :: Term -> Maybe (String, [(Integer, Term)], Integer)
pointsInto Term
t = case Term -> TermKind
termKind Term
t of
    TBin CBinaryOp
CAddOp Term
a Term
k | Maybe IntTy -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe IntTy
termTy Term
k) -> (\(String
b, [(Integer, Term)]
ts, Integer
c) -> (String
b, [(Integer, Term)]
ts [(Integer, Term)] -> [(Integer, Term)] -> [(Integer, Term)]
forall a. [a] -> [a] -> [a]
++ [(Integer
1, Term
k)], Integer
c)) ((String, [(Integer, Term)], Integer)
 -> (String, [(Integer, Term)], Integer))
-> Maybe (String, [(Integer, Term)], Integer)
-> Maybe (String, [(Integer, Term)], Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe (String, [(Integer, Term)], Integer)
pointsInto Term
a
    TUnary CUnaryOp
CAdrOp Term
x -> Term -> Maybe (String, [(Integer, Term)], Integer)
element Term
x
    TermKind
_ | CVar Ident
i NodeInfo
_ <- Term -> CExpression NodeInfo
termExpr Term
t -> (String, [(Integer, Term)], Integer)
-> Maybe (String, [(Integer, Term)], Integer)
forall a. a -> Maybe a
Just (Ident -> String
identToString Ident
i, [], Integer
0)
    TermKind
_ -> Maybe (String, [(Integer, Term)], Integer)
forall a. Maybe a
Nothing

-- | The variable an element is in, and the terms and constant that index it.
-- An element at a constant index is a path the analysis tracks.
element :: Term -> Maybe (String, [(Integer, Term)], Integer)
element :: Term -> Maybe (String, [(Integer, Term)], Integer)
element Term
t = case (Term -> TermKind
termKind Term
t, Term -> CExpression NodeInfo
termExpr Term
t) of
    (TIndex Term
a Term
i Maybe Integer
_, CExpression NodeInfo
_) -> (\(String
b, [(Integer, Term)]
ts, Integer
c) -> (String
b, [(Integer, Term)]
ts [(Integer, Term)] -> [(Integer, Term)] -> [(Integer, Term)]
forall a. [a] -> [a] -> [a]
++ [(Integer
1, Term
i)], Integer
c)) ((String, [(Integer, Term)], Integer)
 -> (String, [(Integer, Term)], Integer))
-> Maybe (String, [(Integer, Term)], Integer)
-> Maybe (String, [(Integer, Term)], Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe (String, [(Integer, Term)], Integer)
pointsInto Term
a
    (TLoad AccessPath
_, CIndex (CVar Ident
b NodeInfo
_) (CConst (CIntConst CInteger
k NodeInfo
_)) NodeInfo
_) -> (String, [(Integer, Term)], Integer)
-> Maybe (String, [(Integer, Term)], Integer)
forall a. a -> Maybe a
Just (Ident -> String
identToString Ident
b, [], CInteger -> Integer
getCInteger CInteger
k)
    (TermKind, CExpression NodeInfo)
_ -> Maybe (String, [(Integer, Term)], Integer)
forall a. Maybe a
Nothing

-- | The variables a function body changes or takes the address of.
changedNames :: CStat -> Set String
changedNames :: CStat -> Set String
changedNames CStat
body = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [ Ident -> String
identToString Ident
i | CExpression NodeInfo
e <- (CExpression NodeInfo -> [CExpression NodeInfo])
-> [CExpression NodeInfo] -> [CExpression NodeInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpression NodeInfo -> [CExpression NodeInfo]
everyExpr (CStat -> [CExpression NodeInfo]
statExprs CStat
body), CVar Ident
i NodeInfo
_ <- CExpression NodeInfo -> [CExpression NodeInfo]
forall {a}. CExpression a -> [CExpression a]
written CExpression NodeInfo
e ]
  where
    everyExpr :: CExpression NodeInfo -> [CExpression NodeInfo]
everyExpr CExpression NodeInfo
e = CExpression NodeInfo
e CExpression NodeInfo
-> [CExpression NodeInfo] -> [CExpression NodeInfo]
forall a. a -> [a] -> [a]
: (CExpression NodeInfo -> [CExpression NodeInfo])
-> [CExpression NodeInfo] -> [CExpression NodeInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpression NodeInfo -> [CExpression NodeInfo]
everyExpr (CExpression NodeInfo -> [CExpression NodeInfo]
exprChildren CExpression NodeInfo
e)
    written :: CExpression a -> [CExpression a]
written = \case
        CAssign CAssignOp
_ CExpression a
l CExpression a
_ a
_ -> [CExpression a
l]
        CUnary CUnaryOp
op CExpression a
l 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, CUnaryOp
CAdrOp] -> [CExpression a
l]
        CExpression a
_ -> []