{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE NamedFieldPuns    #-}
{-# LANGUAGE OverloadedStrings #-}
module Tokstyle.Linter.PointsToAsserts (descr) where

import           Control.Monad                       (foldM, guard)
import           Control.Monad.State.Strict          (evalState, get, runState)
import           Data.Fix
import           Data.IntMap.Strict                  (IntMap)
import qualified Data.IntMap.Strict                  as IntMap
import           Data.IntSet                         (IntSet)
import qualified Data.IntSet                         as IntSet
import           Data.List                           (foldl')
import qualified Data.Map.Strict                     as Map
import           Data.Maybe                          (fromMaybe)
import           Data.Set                            (Set)
import qualified Data.Set                            as Set
import           Data.Text                           (Text)
import qualified Data.Text                           as Text
import qualified Debug.Trace                         as Debug
import qualified Language.Cimple                     as C
import qualified Language.Cimple.Diagnostics         as Diagnostics
import           Tokstyle.Analysis.DataFlow          (CFGNode (..), transfer)
import           Tokstyle.Analysis.PointsTo          (evalExpr)
import           Tokstyle.Analysis.PointsTo.Fixpoint (findEntryPointsAndFuncMap,
                                                      findVarTypes,
                                                      runGlobalFixpoint)
import           Tokstyle.Analysis.PointsTo.Types
import           Tokstyle.Analysis.Scope             (ScopedId (..),
                                                      runScopePass)
import           Tokstyle.Analysis.VTable            (resolveVTables)
import           Tokstyle.Common.TypeSystem          (collect)

debugging :: Bool
debugging :: Bool
debugging = Bool
False

dtrace :: String -> a -> a
dtrace :: String -> a -> a
dtrace String
msg a
x = if Bool
debugging then String -> a -> a
forall a. String -> a -> a
Debug.trace String
msg a
x else a
x

analyse :: [(FilePath, [C.Node (C.Lexeme Text)])] -> [Text]
analyse :: [(String, [Node (Lexeme Text)])] -> [Text]
analyse [(String, [Node (Lexeme Text)])]
sources =
    let
        flatAst :: [Node (Lexeme Text)]
flatAst = ((String, [Node (Lexeme Text)]) -> [Node (Lexeme Text)])
-> [(String, [Node (Lexeme Text)])] -> [Node (Lexeme Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, [Node (Lexeme Text)]) -> [Node (Lexeme Text)]
forall a b. (a, b) -> b
snd [(String, [Node (Lexeme Text)])]
sources
        ([Node (Lexeme ScopedId)]
scopedAsts, ScopeState
_) = [Node (Lexeme Text)] -> ([Node (Lexeme ScopedId)], ScopeState)
runScopePass [Node (Lexeme Text)]
flatAst
        typeSystem :: TypeSystem
typeSystem = [(String, [Node (Lexeme Text)])] -> TypeSystem
collect ((String
"test.c", [Node (Lexeme Text)]
flatAst) (String, [Node (Lexeme Text)])
-> [(String, [Node (Lexeme Text)])]
-> [(String, [Node (Lexeme Text)])]
forall a. a -> [a] -> [a]
: ((String, [Node (Lexeme Text)]) -> (String, [Node (Lexeme Text)]))
-> [(String, [Node (Lexeme Text)])]
-> [(String, [Node (Lexeme Text)])]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
fp, [Node (Lexeme Text)]
ast) -> (String
fp, [Node (Lexeme Text)]
ast)) [(String, [Node (Lexeme Text)])]
sources)
        vtableMap :: VTableMap
vtableMap = [Node (Lexeme ScopedId)] -> TypeSystem -> VTableMap
resolveVTables [Node (Lexeme ScopedId)]
scopedAsts TypeSystem
typeSystem
        ([ScopedId]
_, Map ScopedId [Node (Lexeme ScopedId)]
funcMap) = [Node (Lexeme ScopedId)]
-> ([ScopedId], Map ScopedId [Node (Lexeme ScopedId)])
findEntryPointsAndFuncMap [Node (Lexeme ScopedId)]
scopedAsts

        filePath :: String
filePath = (String, [Node (Lexeme Text)]) -> String
forall a b. (a, b) -> a
fst ([(String, [Node (Lexeme Text)])] -> (String, [Node (Lexeme Text)])
forall a. [a] -> a
head [(String, [Node (Lexeme Text)])]
sources)
        dummyId :: ScopedId
dummyId = Int -> Text -> Scope -> ScopedId
ScopedId Int
0 Text
"" Scope
C.Global
        ctx :: PointsToContext l
ctx = String
-> TypeSystem
-> VTableMap
-> GlobalEnv
-> Map ScopedId [Node (Lexeme ScopedId)]
-> ScopedId
-> Map ScopedId (Node (Lexeme ScopedId))
-> PointsToContext l
forall l.
String
-> TypeSystem
-> VTableMap
-> GlobalEnv
-> Map ScopedId [Node (Lexeme ScopedId)]
-> ScopedId
-> Map ScopedId (Node (Lexeme ScopedId))
-> PointsToContext l
PointsToContext String
filePath TypeSystem
typeSystem VTableMap
vtableMap (Map (ScopedId, RelevantInputState) (FunctionSummary, PointsToFact)
-> GlobalEnv
GlobalEnv Map (ScopedId, RelevantInputState) (FunctionSummary, PointsToFact)
forall k a. Map k a
Map.empty) Map ScopedId [Node (Lexeme ScopedId)]
funcMap ScopedId
dummyId Map ScopedId (Node (Lexeme ScopedId))
forall k a. Map k a
Map.empty
        (GlobalEnv
gEnv, CallGraph
_, CFGCache
cfgCache, MemLocPool
pool) = PointsToContext ScopedId
-> [Node (Lexeme ScopedId)]
-> (GlobalEnv, CallGraph, CFGCache, MemLocPool)
runGlobalFixpoint PointsToContext ScopedId
forall l. PointsToContext l
ctx [Node (Lexeme ScopedId)]
scopedAsts

        (GlobalEnv Map (ScopedId, RelevantInputState) (FunctionSummary, PointsToFact)
globalEnvMap) = GlobalEnv
gEnv
        allFuncContextPairs :: [(ScopedId, RelevantInputState)]
allFuncContextPairs = Map (ScopedId, RelevantInputState) (FunctionSummary, PointsToFact)
-> [(ScopedId, RelevantInputState)]
forall k a. Map k a -> [k]
Map.keys Map (ScopedId, RelevantInputState) (FunctionSummary, PointsToFact)
globalEnvMap

        lintFunction :: (ScopedId, RelevantInputState) -> [Text]
lintFunction (ScopedId
funcId, RelevantInputState
relevantState) =
            case (ScopedId, RelevantInputState)
-> CFGCache
-> Maybe ([CFG ScopedId PointsToFact], Map ScopedId Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (ScopedId
funcId, RelevantInputState
relevantState) CFGCache
cfgCache of
                Just ([CFG ScopedId PointsToFact]
cfgs, Map ScopedId Int
_) ->
                    let funcDef :: Node (Lexeme ScopedId)
funcDef = [Node (Lexeme ScopedId)] -> Node (Lexeme ScopedId)
forall a. [a] -> a
head ([Node (Lexeme ScopedId)]
-> Maybe [Node (Lexeme ScopedId)] -> [Node (Lexeme ScopedId)]
forall a. a -> Maybe a -> a
fromMaybe [] (ScopedId
-> Map ScopedId [Node (Lexeme ScopedId)]
-> Maybe [Node (Lexeme ScopedId)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScopedId
funcId Map ScopedId [Node (Lexeme ScopedId)]
funcMap))
                        varTypes :: Map ScopedId (Node (Lexeme ScopedId))
varTypes = Node (Lexeme ScopedId) -> Map ScopedId (Node (Lexeme ScopedId))
findVarTypes Node (Lexeme ScopedId)
funcDef
                        lintCtx :: PointsToContext l
lintCtx = PointsToContext Any
forall l. PointsToContext l
ctx { pcGlobalEnv :: GlobalEnv
pcGlobalEnv = GlobalEnv
gEnv, pcCurrentFunc :: ScopedId
pcCurrentFunc = ScopedId
funcId, pcVarTypes :: Map ScopedId (Node (Lexeme ScopedId))
pcVarTypes = Map ScopedId (Node (Lexeme ScopedId))
varTypes }
                    in (CFG ScopedId PointsToFact -> [Text])
-> [CFG ScopedId PointsToFact] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\CFG ScopedId PointsToFact
cfg -> (CFGNode ScopedId PointsToFact -> [Text])
-> [CFGNode ScopedId PointsToFact] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PointsToContext ScopedId
-> MemLocPool -> CFGNode ScopedId PointsToFact -> [Text]
checkNode PointsToContext ScopedId
forall l. PointsToContext l
lintCtx MemLocPool
pool) (CFG ScopedId PointsToFact -> [CFGNode ScopedId PointsToFact]
forall k a. Map k a -> [a]
Map.elems CFG ScopedId PointsToFact
cfg)) [CFG ScopedId PointsToFact]
cfgs
                Maybe ([CFG ScopedId PointsToFact], Map ScopedId Int)
Nothing -> []

        lintResults :: [Text]
lintResults = ((ScopedId, RelevantInputState) -> [Text])
-> [(ScopedId, RelevantInputState)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ScopedId, RelevantInputState) -> [Text]
lintFunction [(ScopedId, RelevantInputState)]
allFuncContextPairs
    in
        Set Text -> [Text]
forall a. Set a -> [a]
Set.toList ([Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList [Text]
lintResults)

checkNode :: PointsToContext ScopedId -> MemLocPool -> CFGNode ScopedId PointsToFact -> [Text]
checkNode :: PointsToContext ScopedId
-> MemLocPool -> CFGNode ScopedId PointsToFact -> [Text]
checkNode PointsToContext ScopedId
ctx MemLocPool
pool CFGNode ScopedId PointsToFact
node =
    let
        folder :: (PointsToFact, [Text])
-> Node (Lexeme ScopedId)
-> StateT MemLocPool Identity (PointsToFact, [Text])
folder (PointsToFact
facts, [Text]
diags) Node (Lexeme ScopedId)
stmt = do
            (PointsToFact
nextFacts, Set (ScopedId, RelevantInputState)
_) <- PointsToContext ScopedId
-> ScopedId
-> Int
-> PointsToFact
-> Node (Lexeme ScopedId)
-> StateT
     MemLocPool
     Identity
     (PointsToFact, Set (ScopedId, RelevantInputState))
forall (m :: * -> *) (c :: * -> *) l a callCtx.
DataFlow m c l a callCtx =>
c l -> l -> Int -> a -> Node (Lexeme l) -> m (a, Set (l, callCtx))
transfer PointsToContext ScopedId
ctx (PointsToContext ScopedId -> ScopedId
forall l. PointsToContext l -> ScopedId
pcCurrentFunc PointsToContext ScopedId
ctx) (CFGNode ScopedId PointsToFact -> Int
forall l a. CFGNode l a -> Int
cfgNodeId CFGNode ScopedId PointsToFact
node) PointsToFact
facts Node (Lexeme ScopedId)
stmt
            [Text]
newDiags <- PointsToContext ScopedId
-> Int
-> PointsToFact
-> Node (Lexeme ScopedId)
-> PointsToAnalysis [Text]
checkStmt PointsToContext ScopedId
ctx (CFGNode ScopedId PointsToFact -> Int
forall l a. CFGNode l a -> Int
cfgNodeId CFGNode ScopedId PointsToFact
node) PointsToFact
facts Node (Lexeme ScopedId)
stmt
            (PointsToFact, [Text])
-> StateT MemLocPool Identity (PointsToFact, [Text])
forall (m :: * -> *) a. Monad m => a -> m a
return (PointsToFact
nextFacts, [Text]
diags [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
newDiags)
        ((PointsToFact
_, [Text]
allDiags), MemLocPool
_) = StateT MemLocPool Identity (PointsToFact, [Text])
-> MemLocPool -> ((PointsToFact, [Text]), MemLocPool)
forall s a. State s a -> s -> (a, s)
runState (((PointsToFact, [Text])
 -> Node (Lexeme ScopedId)
 -> StateT MemLocPool Identity (PointsToFact, [Text]))
-> (PointsToFact, [Text])
-> [Node (Lexeme ScopedId)]
-> StateT MemLocPool Identity (PointsToFact, [Text])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (PointsToFact, [Text])
-> Node (Lexeme ScopedId)
-> StateT MemLocPool Identity (PointsToFact, [Text])
folder (CFGNode ScopedId PointsToFact -> PointsToFact
forall l a. CFGNode l a -> a
cfgInFacts CFGNode ScopedId PointsToFact
node, []) (CFGNode ScopedId PointsToFact -> [Node (Lexeme ScopedId)]
forall l a. CFGNode l a -> [Node (Lexeme l)]
cfgStmts CFGNode ScopedId PointsToFact
node)) MemLocPool
pool
    in
        [Text]
allDiags

checkStmt :: PointsToContext ScopedId -> Int -> PointsToFact -> C.Node (C.Lexeme ScopedId) -> PointsToAnalysis [Text]
checkStmt :: PointsToContext ScopedId
-> Int
-> PointsToFact
-> Node (Lexeme ScopedId)
-> PointsToAnalysis [Text]
checkStmt PointsToContext ScopedId
ctx Int
nodeId PointsToFact
facts Node (Lexeme ScopedId)
stmt =
    case Node (Lexeme ScopedId)
-> NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node (Lexeme ScopedId)
stmt of
        C.ExprStmt (Fix (C.FunctionCall (Fix (C.VarExpr lexeme :: Lexeme ScopedId
lexeme@(C.L AlexPosn
_ LexemeClass
_ ScopedId
sid))) [Node (Lexeme ScopedId)
arg])) | ScopedId -> Text
sidName ScopedId
sid Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"assert" ->
            PointsToContext ScopedId
-> Int
-> PointsToFact
-> Lexeme ScopedId
-> Node (Lexeme ScopedId)
-> PointsToAnalysis [Text]
checkAssert PointsToContext ScopedId
ctx Int
nodeId PointsToFact
facts Lexeme ScopedId
lexeme Node (Lexeme ScopedId)
arg
        NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
_ -> [Text] -> PointsToAnalysis [Text]
forall (m :: * -> *) a. Monad m => a -> m a
return []

checkAssert :: PointsToContext ScopedId -> Int -> PointsToFact -> C.Lexeme ScopedId -> C.Node (C.Lexeme ScopedId) -> PointsToAnalysis [Text]
checkAssert :: PointsToContext ScopedId
-> Int
-> PointsToFact
-> Lexeme ScopedId
-> Node (Lexeme ScopedId)
-> PointsToAnalysis [Text]
checkAssert PointsToContext ScopedId
ctx Int
nodeId PointsToFact
facts Lexeme ScopedId
assertLexeme Node (Lexeme ScopedId)
assertArg =
    case Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
assertArg of
        Just (Node (Lexeme ScopedId)
ptrArg, MemLoc -> Bool
predicate, Text
desc) ->
            let errMsg :: Text
errMsg = Text
"does not satisfy assertion: must be " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
desc
            in PointsToContext ScopedId
-> Int
-> PointsToFact
-> Lexeme ScopedId
-> Node (Lexeme ScopedId)
-> (MemLoc -> Bool)
-> Text
-> PointsToAnalysis [Text]
checkPredicate PointsToContext ScopedId
ctx Int
nodeId PointsToFact
facts Lexeme ScopedId
assertLexeme Node (Lexeme ScopedId)
ptrArg MemLoc -> Bool
predicate Text
errMsg
        Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
Nothing -> [Text] -> PointsToAnalysis [Text]
forall (m :: * -> *) a. Monad m => a -> m a
return []

checkPredicate :: PointsToContext ScopedId -> Int -> PointsToFact -> C.Lexeme ScopedId -> C.Node (C.Lexeme ScopedId) -> (MemLoc -> Bool) -> Text -> PointsToAnalysis [Text]
checkPredicate :: PointsToContext ScopedId
-> Int
-> PointsToFact
-> Lexeme ScopedId
-> Node (Lexeme ScopedId)
-> (MemLoc -> Bool)
-> Text
-> PointsToAnalysis [Text]
checkPredicate PointsToContext ScopedId
ctx Int
nodeId PointsToFact
facts Lexeme ScopedId
assertLexeme Node (Lexeme ScopedId)
ptrArg MemLoc -> Bool
predicate Text
errMsg = do
    IntSet
ptrLocsInt <- PointsToFact
-> PointsToContext ScopedId
-> Int
-> Node (Lexeme ScopedId)
-> PointsToAnalysis IntSet
evalExpr PointsToFact
facts PointsToContext ScopedId
ctx Int
nodeId Node (Lexeme ScopedId)
ptrArg
    MemLocPool
pool <- StateT MemLocPool Identity MemLocPool
forall s (m :: * -> *). MonadState s m => m s
get
    let ptrLocs :: [MemLoc]
ptrLocs = (Int -> MemLoc) -> [Int] -> [MemLoc]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> MemLoc -> Int -> IntMap MemLoc -> MemLoc
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault MemLoc
UnknownLoc Int
i (MemLocPool -> IntMap MemLoc
idToMemLoc MemLocPool
pool)) (IntSet -> [Int]
IntSet.toList IntSet
ptrLocsInt)
    let predicateResults :: [Bool]
predicateResults = (MemLoc -> Bool) -> [MemLoc] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map MemLoc -> Bool
predicate [MemLoc]
ptrLocs
    if Bool -> Bool
not ([MemLoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [MemLoc]
ptrLocs) Bool -> Bool -> Bool
&& (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
==Bool
True) [Bool]
predicateResults
       then [Text] -> PointsToAnalysis [Text]
forall (m :: * -> *) a. Monad m => a -> m a
return []
       else [Text] -> PointsToAnalysis [Text]
forall (m :: * -> *) a. Monad m => a -> m a
return
           [ String -> Lexeme ScopedId -> Text
forall a. HasLocation a => String -> a -> Text
Diagnostics.sloc (PointsToContext ScopedId -> String
forall l. PointsToContext l -> String
pcFilePath PointsToContext ScopedId
ctx) Lexeme ScopedId
assertLexeme Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
             Text
": Static analysis check failed: Pointer '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ScopedId -> Text
sidName (Lexeme ScopedId -> ScopedId
forall text. Lexeme text -> text
C.lexemeText (Lexeme ScopedId -> Maybe (Lexeme ScopedId) -> Lexeme ScopedId
forall a. a -> Maybe a -> a
fromMaybe (AlexPosn -> LexemeClass -> ScopedId -> Lexeme ScopedId
forall text. AlexPosn -> LexemeClass -> text -> Lexeme text
C.L (Int -> Int -> Int -> AlexPosn
C.AlexPn Int
0 Int
0 Int
0) LexemeClass
C.IdVar (Int -> Text -> Scope -> ScopedId
ScopedId Int
0 Text
"" Scope
C.Local)) (Node (Lexeme ScopedId) -> Maybe (Lexeme ScopedId)
forall l. Node (Lexeme l) -> Maybe (Lexeme l)
getLexeme Node (Lexeme ScopedId)
ptrArg))) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
             Text
"' " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
errMsg Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". It can point to " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Set MemLoc -> Text
summarizeMemLocs ([MemLoc] -> Set MemLoc
forall a. Ord a => [a] -> Set a
Set.fromList [MemLoc]
ptrLocs) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"."
           ]

stripParens :: C.Node a -> C.Node a
stripParens :: Node a -> Node a
stripParens (Fix (C.ParenExpr Node a
inner)) = Node a -> Node a
forall a. Node a -> Node a
stripParens Node a
inner
stripParens Node a
node                      = Node a
node

evalAssertExpr :: C.Node (C.Lexeme ScopedId) -> Maybe (C.Node (C.Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr :: Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
expr = String
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. String -> a -> a
dtrace (String
"[evalAssertExpr] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeF (Lexeme ScopedId) () -> String
forall a. Show a => a -> String
show ((Node (Lexeme ScopedId) -> ())
-> NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
-> NodeF (Lexeme ScopedId) ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> Node (Lexeme ScopedId) -> ()
forall a b. a -> b -> a
const ()) (Node (Lexeme ScopedId)
-> NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node (Lexeme ScopedId)
expr))) (Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
 -> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text))
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a b. (a -> b) -> a -> b
$
    case Node (Lexeme ScopedId)
-> NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node (Lexeme ScopedId)
expr of
    C.ParenExpr Node (Lexeme ScopedId)
inner -> Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
inner
    C.UnaryExpr UnaryOp
C.UopNot Node (Lexeme ScopedId)
inner -> do
        (Node (Lexeme ScopedId)
ptrArg, MemLoc -> Bool
p, Text
desc) <- Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
inner
        let newDesc :: Text
newDesc = case Node (Lexeme ScopedId)
-> NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Node (Lexeme ScopedId) -> Node (Lexeme ScopedId)
forall a. Node a -> Node a
stripParens Node (Lexeme ScopedId)
inner) of
                C.BinaryExpr {} -> Text
"not (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
desc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
_               -> Text
"not " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
desc
        (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg, Bool -> Bool
not (Bool -> Bool) -> (MemLoc -> Bool) -> MemLoc -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemLoc -> Bool
p, Text
newDesc)
    C.FunctionCall (Fix (C.VarExpr (C.L AlexPosn
_ LexemeClass
_ ScopedId{Text
sidName :: Text
sidName :: ScopedId -> Text
sidName}))) [Node (Lexeme ScopedId)
ptrArg] ->
        case Text
sidName of
            Text
"mem_is_heap"           -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg, \case { HeapLoc Text
_ -> Bool
True; MemLoc
_ -> Bool
False }, Text
"heap")
            Text
"mem_is_stack"          -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg, \case { StackLoc ScopedId
_ -> Bool
True; MemLoc
_ -> Bool
False }, Text
"stack")
            Text
"mem_is_not_null"       -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg, \case { MemLoc
NullLoc -> Bool
False; MemLoc
_ -> Bool
True }, Text
"not null")
            Text
"mem_is_external_param" -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg, \case { ExternalParamLoc {} -> Bool
True; MemLoc
_ -> Bool
False }, Text
"external param")
            Text
_                       -> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. Maybe a
Nothing
    C.BinaryExpr Node (Lexeme ScopedId)
lhs BinaryOp
op Node (Lexeme ScopedId)
rhs -> do
        (Node (Lexeme ScopedId)
ptrArg1, MemLoc -> Bool
p1, Text
desc1) <- Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
lhs
        (Node (Lexeme ScopedId)
ptrArg2, MemLoc -> Bool
p2, Text
desc2) <- Node (Lexeme ScopedId)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
evalAssertExpr Node (Lexeme ScopedId)
rhs
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((Lexeme ScopedId -> ScopedId)
-> Maybe (Lexeme ScopedId) -> Maybe ScopedId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Lexeme ScopedId -> ScopedId
forall text. Lexeme text -> text
C.lexemeText (Node (Lexeme ScopedId) -> Maybe (Lexeme ScopedId)
forall l. Node (Lexeme l) -> Maybe (Lexeme l)
getLexeme Node (Lexeme ScopedId)
ptrArg1) Maybe ScopedId -> Maybe ScopedId -> Bool
forall a. Eq a => a -> a -> Bool
== (Lexeme ScopedId -> ScopedId)
-> Maybe (Lexeme ScopedId) -> Maybe ScopedId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Lexeme ScopedId -> ScopedId
forall text. Lexeme text -> text
C.lexemeText (Node (Lexeme ScopedId) -> Maybe (Lexeme ScopedId)
forall l. Node (Lexeme l) -> Maybe (Lexeme l)
getLexeme Node (Lexeme ScopedId)
ptrArg2))
        let pDesc1 :: Text
pDesc1 = BinaryOp -> Node (Lexeme ScopedId) -> Text -> Text
forall a. BinaryOp -> Node a -> Text -> Text
paren BinaryOp
op Node (Lexeme ScopedId)
lhs Text
desc1
        let pDesc2 :: Text
pDesc2 = BinaryOp -> Node (Lexeme ScopedId) -> Text -> Text
forall a. BinaryOp -> Node a -> Text -> Text
paren BinaryOp
op Node (Lexeme ScopedId)
rhs Text
desc2
        case BinaryOp
op of
            BinaryOp
C.BopOr  -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg1, \MemLoc
loc -> MemLoc -> Bool
p1 MemLoc
loc Bool -> Bool -> Bool
|| MemLoc -> Bool
p2 MemLoc
loc, Text
pDesc1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" or " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
pDesc2)
            BinaryOp
C.BopAnd -> (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
-> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. a -> Maybe a
Just (Node (Lexeme ScopedId)
ptrArg1, \MemLoc
loc -> MemLoc -> Bool
p1 MemLoc
loc Bool -> Bool -> Bool
&& MemLoc -> Bool
p2 MemLoc
loc, Text
pDesc1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
pDesc2)
            BinaryOp
_        -> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. Maybe a
Nothing
    NodeF (Lexeme ScopedId) (Node (Lexeme ScopedId))
_ -> Maybe (Node (Lexeme ScopedId), MemLoc -> Bool, Text)
forall a. Maybe a
Nothing

opPrec :: C.BinaryOp -> Int
opPrec :: BinaryOp -> Int
opPrec BinaryOp
C.BopOr  = Int
1
opPrec BinaryOp
C.BopAnd = Int
2
opPrec BinaryOp
_        = Int
99

paren :: C.BinaryOp -> C.Node a -> Text -> Text
paren :: BinaryOp -> Node a -> Text -> Text
paren BinaryOp
outerOp Node a
node Text
txt = case Node a -> NodeF a (Node a)
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Node a
node of
    C.ParenExpr Node a
inner        -> BinaryOp -> Node a -> Text -> Text
forall a. BinaryOp -> Node a -> Text -> Text
paren BinaryOp
outerOp Node a
inner Text
txt
    C.BinaryExpr Node a
_ BinaryOp
innerOp Node a
_ -> if BinaryOp -> Int
opPrec BinaryOp
innerOp Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BinaryOp -> Int
opPrec BinaryOp
outerOp
        then Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
txt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        else Text
txt
    NodeF a (Node a)
_ -> Text
txt

summarizeMemLocs :: Set MemLoc -> Text
summarizeMemLocs :: Set MemLoc -> Text
summarizeMemLocs Set MemLoc
locs =
    let simplifiedNames :: Set Text
simplifiedNames = (MemLoc -> Text) -> Set MemLoc -> Set Text
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (String -> Text
Text.pack (String -> Text) -> (MemLoc -> String) -> MemLoc -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') (String -> String) -> (MemLoc -> String) -> MemLoc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemLoc -> String
forall a. Show a => a -> String
show) Set MemLoc
locs
    in Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
Text.intercalate Text
", " (Set Text -> [Text]
forall a. Set a -> [a]
Set.toList Set Text
simplifiedNames) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"

getLexeme :: C.Node (C.Lexeme l) -> Maybe (C.Lexeme l)
getLexeme :: Node (Lexeme l) -> Maybe (Lexeme l)
getLexeme (Fix (C.VarExpr Lexeme l
l))          = Lexeme l -> Maybe (Lexeme l)
forall a. a -> Maybe a
Just Lexeme l
l
getLexeme (Fix (C.MemberAccess Node (Lexeme l)
_ Lexeme l
l))   = Lexeme l -> Maybe (Lexeme l)
forall a. a -> Maybe a
Just Lexeme l
l
getLexeme (Fix (C.PointerAccess Node (Lexeme l)
_ Lexeme l
l))  = Lexeme l -> Maybe (Lexeme l)
forall a. a -> Maybe a
Just Lexeme l
l
getLexeme (Fix (C.ArrayAccess Node (Lexeme l)
base Node (Lexeme l)
_)) = Node (Lexeme l) -> Maybe (Lexeme l)
forall l. Node (Lexeme l) -> Maybe (Lexeme l)
getLexeme Node (Lexeme l)
base
getLexeme Node (Lexeme l)
_                            = Maybe (Lexeme l)
forall a. Maybe a
Nothing

descr :: ([(FilePath, [C.Node (C.Lexeme Text)])] -> [Text], (Text, Text))
descr :: ([(String, [Node (Lexeme Text)])] -> [Text], (Text, Text))
descr = ([(String, [Node (Lexeme Text)])] -> [Text]
analyse, (Text
"points-to-asserts", [Text] -> Text
Text.unlines
    [ Text
"Checks for static analysis assertions in the code."
    , Text
""
    , Text
"**Reason:** Allows developers to enforce invariants about pointer properties"
    , Text
"(e.g., whether a pointer refers to heap or stack memory) that are"
    , Text
"verified at compile time by the points-to analysis."
    , Text
""
    , Text
"Supported checks:"
    , Text
"  - `mem_is_heap(p)`: asserts that `p` points to a heap location."
    , Text
"  - `mem_is_stack(p)`: asserts that `p` points to a stack location."
    , Text
"  - `mem_is_not_null(p)`: asserts that `p` is not null."
    , Text
"  - `mem_is_external_param(p)`: asserts that `p` points to an external parameter."
    , Text
""
    , Text
"Checks can be combined with `&&` and `||`, and negated with `!`."
    , Text
"For example: `assert(!(mem_is_heap(p) || mem_is_stack(p)))`"
    ]))