{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Strict            #-}
module Tokstyle.Linter.PointsTo (descr) where

import           Control.Monad.State.Strict  (State)
import qualified Control.Monad.State.Strict  as State
import           Data.Fix                    (Fix (..))
import qualified Data.Map.Strict             as Map
import           Data.Maybe                  (fromMaybe, mapMaybe)
import           Data.Set                    (Set)
import qualified Data.Set                    as Set
import           Data.Text                   (Text)
import qualified Data.Text                   as Text
import           Language.Cimple             (Lexeme (..), Node,
                                              NodeF (FunctionPrototype, MemberDecl, TyFunc, TyPointer, VarDecl))
import qualified Language.Cimple.Diagnostics as Diagnostics
import           Language.Cimple.TraverseAst (AstActions, astActions, doNode,
                                              traverseAst)
import           Text.Groom                  (groom)

import           Tokstyle.Analysis.CallGraph (buildCallGraph)
import           Tokstyle.Analysis.DataFlow  (cfgOutFacts)
import           Tokstyle.Analysis.PointsTo  (PointsToContext (..),
                                              PointsToState (..),
                                              buildPointsToContext)
import           Tokstyle.Analysis.Types     (AbstractLocation (..),
                                              PointsToMap)


findPointerDecls :: [(FilePath, [Node (Lexeme Text)])] -> Map.Map Text (FilePath, Lexeme Text)
findPointerDecls :: [(FilePath, [Node (Lexeme Text)])]
-> Map Text (FilePath, Lexeme Text)
findPointerDecls [(FilePath, [Node (Lexeme Text)])]
tus = State (Map Text (FilePath, Lexeme Text)) ()
-> Map Text (FilePath, Lexeme Text)
-> Map Text (FilePath, Lexeme Text)
forall s a. State s a -> s -> s
State.execState (AstActions (State (Map Text (FilePath, Lexeme Text))) Text
-> [(FilePath, [Node (Lexeme Text)])]
-> State (Map Text (FilePath, Lexeme Text)) ()
forall text a (f :: * -> *).
(TraverseAst text a, Applicative f) =>
AstActions f text -> a -> f ()
traverseAst AstActions (State (Map Text (FilePath, Lexeme Text))) Text
collector [(FilePath, [Node (Lexeme Text)])]
tus) Map Text (FilePath, Lexeme Text)
forall k a. Map k a
Map.empty
  where
    collector :: AstActions (State (Map.Map Text (FilePath, Lexeme Text))) Text
    collector :: AstActions (State (Map Text (FilePath, Lexeme Text))) Text
collector = AstActions (State (Map Text (FilePath, Lexeme Text))) Text
forall (f :: * -> *) text. Applicative f => AstActions f text
astActions
        { doNode :: FilePath
-> Node (Lexeme Text)
-> State (Map Text (FilePath, Lexeme Text)) ()
-> State (Map Text (FilePath, Lexeme Text)) ()
doNode = \FilePath
file Node (Lexeme Text)
node State (Map Text (FilePath, Lexeme Text)) ()
act -> do
            case Node (Lexeme Text) -> NodeF (Lexeme Text) (Node (Lexeme Text))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node (Lexeme Text)
node of
                VarDecl (Fix (TyPointer Node (Lexeme Text)
_)) l :: Lexeme Text
l@(L AlexPosn
_ LexemeClass
_ Text
name) [Node (Lexeme Text)]
_ -> (Map Text (FilePath, Lexeme Text)
 -> Map Text (FilePath, Lexeme Text))
-> State (Map Text (FilePath, Lexeme Text)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (Text
-> (FilePath, Lexeme Text)
-> Map Text (FilePath, Lexeme Text)
-> Map Text (FilePath, Lexeme Text)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (FilePath
file, Lexeme Text
l))
                MemberDecl (Fix (VarDecl (Fix (TyPointer Node (Lexeme Text)
_)) l :: Lexeme Text
l@(L AlexPosn
_ LexemeClass
_ Text
name) [Node (Lexeme Text)]
_)) Maybe (Lexeme Text)
_ -> (Map Text (FilePath, Lexeme Text)
 -> Map Text (FilePath, Lexeme Text))
-> State (Map Text (FilePath, Lexeme Text)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (Text
-> (FilePath, Lexeme Text)
-> Map Text (FilePath, Lexeme Text)
-> Map Text (FilePath, Lexeme Text)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (FilePath
file, Lexeme Text
l))
                NodeF (Lexeme Text) (Node (Lexeme Text))
_                                             -> () -> State (Map Text (FilePath, Lexeme Text)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            State (Map Text (FilePath, Lexeme Text)) ()
act
        }

isFunctionParameter :: Text -> [(FilePath, [Node (Lexeme Text)])] -> Bool
isFunctionParameter :: Text -> [(FilePath, [Node (Lexeme Text)])] -> Bool
isFunctionParameter Text
name [(FilePath, [Node (Lexeme Text)])]
tus = State Bool () -> Bool -> Bool
forall s a. State s a -> s -> s
State.execState (AstActions (State Bool) Text
-> [(FilePath, [Node (Lexeme Text)])] -> State Bool ()
forall text a (f :: * -> *).
(TraverseAst text a, Applicative f) =>
AstActions f text -> a -> f ()
traverseAst AstActions (State Bool) Text
collector [(FilePath, [Node (Lexeme Text)])]
tus) Bool
False
  where
    collector :: AstActions (State Bool) Text
    collector :: AstActions (State Bool) Text
collector = AstActions (State Bool) Text
forall (f :: * -> *) text. Applicative f => AstActions f text
astActions
        { doNode :: FilePath -> Node (Lexeme Text) -> State Bool () -> State Bool ()
doNode = \FilePath
_ Node (Lexeme Text)
node State Bool ()
act -> do
            case Node (Lexeme Text) -> NodeF (Lexeme Text) (Node (Lexeme Text))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node (Lexeme Text)
node of
                FunctionPrototype Node (Lexeme Text)
_ Lexeme Text
_ [Node (Lexeme Text)]
params ->
                    let paramNames :: Set Text
paramNames = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList ([Text] -> Set Text) -> [Text] -> Set Text
forall a b. (a -> b) -> a -> b
$ (Node (Lexeme Text) -> Maybe Text)
-> [Node (Lexeme Text)] -> [Text]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case
                            Fix (VarDecl Node (Lexeme Text)
_ (L AlexPosn
_ LexemeClass
_ Text
pname) [Node (Lexeme Text)]
_) -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
pname
                            Node (Lexeme Text)
_                               -> Maybe Text
forall a. Maybe a
Nothing
                            ) [Node (Lexeme Text)]
params
                    in if Text -> Set Text -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Text
name Set Text
paramNames
                       then Bool -> State Bool ()
forall s (m :: * -> *). MonadState s m => s -> m ()
State.put Bool
True
                       else State Bool ()
act
                NodeF (Lexeme Text) (Node (Lexeme Text))
_ -> State Bool ()
act
        }

prettyAbstractLocation :: AbstractLocation -> Text
prettyAbstractLocation :: AbstractLocation -> Text
prettyAbstractLocation (VarLocation Text
name) = Text
name
prettyAbstractLocation (FieldLocation AbstractLocation
base Text
field) = AbstractLocation -> Text
prettyAbstractLocation AbstractLocation
base Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
field
prettyAbstractLocation (DerefLocation AbstractLocation
ptr) = Text
"(*" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> AbstractLocation -> Text
prettyAbstractLocation AbstractLocation
ptr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
prettyAbstractLocation (GlobalVarLocation Text
name) = Text
name
prettyAbstractLocation (ReturnLocation Text
name) = Text
"ret:" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
name
prettyAbstractLocation (HeapLocation Int
_) = Text
"heap"
prettyAbstractLocation (FunctionLocation Text
name) = Text
"&" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
name

formatPointsToSet :: Set AbstractLocation -> Text
formatPointsToSet :: Set AbstractLocation -> Text
formatPointsToSet Set AbstractLocation
set =
    let locations :: [Text]
locations = Set Text -> [Text]
forall a. Set a -> [a]
Set.toList (Set Text -> [Text]) -> Set Text -> [Text]
forall a b. (a -> b) -> a -> b
$ (AbstractLocation -> Text) -> Set AbstractLocation -> Set Text
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\case
            FunctionLocation Text
name -> Text
name
            VarLocation Text
name      -> Text
name
            AbstractLocation
_                     -> Text
""
            ) Set AbstractLocation
set
    in Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
Text.intercalate Text
", " ((Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Text -> Bool) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
Text.null) [Text]
locations) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"

analyse :: [(FilePath, [Node (Lexeme Text)])] -> [Text]
analyse :: [(FilePath, [Node (Lexeme Text)])] -> [Text]
analyse [(FilePath, [Node (Lexeme Text)])]
tus =
    let initialCallGraph :: CallGraph
initialCallGraph = [(FilePath, [Node (Lexeme Text)])] -> PointsToMap -> CallGraph
buildCallGraph [(FilePath, [Node (Lexeme Text)])]
tus PointsToMap
forall k a. Map k a
Map.empty
        pointsToCtx :: PointsToContext Text
pointsToCtx = [(FilePath, [Node (Lexeme Text)])]
-> CallGraph -> Map Text PointsToSummary -> PointsToContext Text
buildPointsToContext [(FilePath, [Node (Lexeme Text)])]
tus CallGraph
initialCallGraph Map Text PointsToSummary
forall k a. Map k a
Map.empty
        allOutFacts :: [PointsToMap]
allOutFacts = (PointsToState -> PointsToMap) -> [PointsToState] -> [PointsToMap]
forall a b. (a -> b) -> [a] -> [b]
map PointsToState -> PointsToMap
ptsMap ([PointsToState] -> [PointsToMap])
-> [PointsToState] -> [PointsToMap]
forall a b. (a -> b) -> a -> b
$ (Map Int (CFGNode Text PointsToState) -> [PointsToState])
-> [Map Int (CFGNode Text PointsToState)] -> [PointsToState]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CFGNode Text PointsToState -> PointsToState)
-> [CFGNode Text PointsToState] -> [PointsToState]
forall a b. (a -> b) -> [a] -> [b]
map CFGNode Text PointsToState -> PointsToState
forall l a. CFGNode l a -> a
cfgOutFacts ([CFGNode Text PointsToState] -> [PointsToState])
-> (Map Int (CFGNode Text PointsToState)
    -> [CFGNode Text PointsToState])
-> Map Int (CFGNode Text PointsToState)
-> [PointsToState]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Int (CFGNode Text PointsToState)
-> [CFGNode Text PointsToState]
forall k a. Map k a -> [a]
Map.elems) (Map (Text, Context) (Map Int (CFGNode Text PointsToState))
-> [Map Int (CFGNode Text PointsToState)]
forall k a. Map k a -> [a]
Map.elems (PointsToContext Text
-> Map (Text, Context) (Map Int (CFGNode Text PointsToState))
forall l.
PointsToContext l
-> Map (Text, Context) (Map Int (CFGNode Text PointsToState))
ptcAnalyzedCfgs PointsToContext Text
pointsToCtx))
        finalPointsToMap :: PointsToMap
finalPointsToMap = (Set AbstractLocation
 -> Set AbstractLocation -> Set AbstractLocation)
-> [PointsToMap] -> PointsToMap
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Set AbstractLocation
-> Set AbstractLocation -> Set AbstractLocation
forall a. Ord a => Set a -> Set a -> Set a
Set.union [PointsToMap]
allOutFacts
        ptrDecls :: Map Text (FilePath, Lexeme Text)
ptrDecls = [(FilePath, [Node (Lexeme Text)])]
-> Map Text (FilePath, Lexeme Text)
findPointerDecls [(FilePath, [Node (Lexeme Text)])]
tus

        warnings :: [Text]
warnings = ((AbstractLocation, Set AbstractLocation) -> Maybe Text)
-> [(AbstractLocation, Set AbstractLocation)] -> [Text]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(AbstractLocation
loc, Set AbstractLocation
pointsToSet) ->
            let mname :: Maybe Text
mname = case AbstractLocation
loc of
                    VarLocation n -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
n
                    FieldLocation base n -> case AbstractLocation
base of
                        DerefLocation AbstractLocation
_ -> Maybe Text
forall a. Maybe a
Nothing
                        AbstractLocation
_               -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
n
                    ReturnLocation n  -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
n
                    AbstractLocation
_                 -> Maybe Text
forall a. Maybe a
Nothing
            in case Maybe Text
mname of
                Just Text
name ->
                   if Bool -> Bool
not (Set AbstractLocation -> Bool
forall a. Set a -> Bool
Set.null Set AbstractLocation
pointsToSet) Bool -> Bool -> Bool
&& Bool -> Bool
not (Text -> [(FilePath, [Node (Lexeme Text)])] -> Bool
isFunctionParameter Text
name [(FilePath, [Node (Lexeme Text)])]
tus)
                   then let (FilePath
file, Lexeme Text
lexeme) = (FilePath, Lexeme Text)
-> Maybe (FilePath, Lexeme Text) -> (FilePath, Lexeme Text)
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> (FilePath, Lexeme Text)
forall a. HasCallStack => FilePath -> a
error (FilePath -> (FilePath, Lexeme Text))
-> FilePath -> (FilePath, Lexeme Text)
forall a b. (a -> b) -> a -> b
$ FilePath
"impossible: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Text -> FilePath
forall a. Show a => a -> FilePath
show Text
name) (Text
-> Map Text (FilePath, Lexeme Text)
-> Maybe (FilePath, Lexeme Text)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text (FilePath, Lexeme Text)
ptrDecls)
                        in Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ FilePath -> Lexeme Text -> Text
forall a. HasLocation a => FilePath -> a -> Text
Diagnostics.sloc FilePath
file Lexeme Text
lexeme Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": `" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> AbstractLocation -> Text
prettyAbstractLocation AbstractLocation
loc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"` points to: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Set AbstractLocation -> Text
formatPointsToSet Set AbstractLocation
pointsToSet
                   else Maybe Text
forall a. Maybe a
Nothing
                Maybe Text
Nothing -> Maybe Text
forall a. Maybe a
Nothing
            ) (PointsToMap -> [(AbstractLocation, Set AbstractLocation)]
forall k a. Map k a -> [(k, a)]
Map.toList PointsToMap
finalPointsToMap)

    in if [Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
warnings
       then []
       else [Text]
warnings

descr :: ([(FilePath, [Node (Lexeme Text)])] -> [Text], (Text, Text))
descr :: ([(FilePath, [Node (Lexeme Text)])] -> [Text], (Text, Text))
descr = ([(FilePath, [Node (Lexeme Text)])] -> [Text]
analyse, (Text
"points-to", [Text] -> Text
Text.unlines
    [ Text
"Reports the set of functions that each function pointer can point to."
    , Text
""
    , Text
"**Reason:** To statically verify the possible targets of indirect calls."
    ]))