{-# LANGUAGE Strict #-}
-- | What the analysis knows about functions whose bodies it doesn't see.
module Tokstyle.C.Analysis.Known
    ( Reach (..)
    , libraryReaches
    , allocators
    , noReturn
    , harmless
    ) where

import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map


-- | How far a function can reach into the memory one of its pointer
-- parameters points to: another parameter times a coefficient, if any, plus
-- a constant.
data Reach = Reach
    { Reach -> Int
reachParam  :: Int
    , Reach -> Maybe (Int, Integer)
reachLength :: Maybe (Int, Integer)
    , Reach -> Integer
reachConst  :: Integer
    }
    deriving (Reach -> Reach -> Bool
(Reach -> Reach -> Bool) -> (Reach -> Reach -> Bool) -> Eq Reach
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Reach -> Reach -> Bool
== :: Reach -> Reach -> Bool
$c/= :: Reach -> Reach -> Bool
/= :: Reach -> Reach -> Bool
Eq, Int -> Reach -> ShowS
[Reach] -> ShowS
Reach -> String
(Int -> Reach -> ShowS)
-> (Reach -> String) -> ([Reach] -> ShowS) -> Show Reach
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Reach -> ShowS
showsPrec :: Int -> Reach -> ShowS
$cshow :: Reach -> String
show :: Reach -> String
$cshowList :: [Reach] -> ShowS
showList :: [Reach] -> ShowS
Show)

-- | How far the library functions the program calls reach into the memory
-- their pointer arguments point to.
libraryReaches :: Map String [Reach]
libraryReaches :: Map String [Reach]
libraryReaches = [(String, [Reach])] -> Map String [Reach]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (String
"memcpy", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"memmove", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"memcmp", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"memset", [Int -> Int -> Reach
upTo Int
0 Int
2])
    , (String
"snprintf", [Int -> Int -> Reach
upTo Int
0 Int
1])
    , (String
"sodium_memzero", [Int -> Int -> Reach
upTo Int
0 Int
1])
    , (String
"sodium_memcmp", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"randombytes_buf", [Int -> Int -> Reach
upTo Int
0 Int
1])
    , (String
"crypto_hash_sha256", [Int -> Maybe (Int, Integer) -> Integer -> Reach
Reach Int
0 Maybe (Int, Integer)
forall a. Maybe a
Nothing Integer
32, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_hash_sha512", [Int -> Maybe (Int, Integer) -> Integer -> Reach
Reach Int
0 Maybe (Int, Integer)
forall a. Maybe a
Nothing Integer
64, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_auth", [Int -> Maybe (Int, Integer) -> Integer -> Reach
Reach Int
0 Maybe (Int, Integer)
forall a. Maybe a
Nothing Integer
32, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_auth_verify", [Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_sign_detached", [Int -> Maybe (Int, Integer) -> Integer -> Reach
Reach Int
0 Maybe (Int, Integer)
forall a. Maybe a
Nothing Integer
64, Int -> Int -> Reach
upTo Int
2 Int
3])
    , (String
"crypto_sign_verify_detached", [Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_box_afternm", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    , (String
"crypto_box_open_afternm", [Int -> Int -> Reach
upTo Int
0 Int
2, Int -> Int -> Reach
upTo Int
1 Int
2])
    ]
  where
    upTo :: Int -> Int -> Reach
upTo Int
p Int
n = Int -> Maybe (Int, Integer) -> Integer -> Reach
Reach Int
p ((Int, Integer) -> Maybe (Int, Integer)
forall a. a -> Maybe a
Just (Int
n, Integer
1)) Integer
0

-- | The functions that allocate memory: how many arguments they take, and
-- which of them multiply to the size in bytes.
allocators :: Map String (Int, [Int])
allocators :: Map String (Int, [Int])
allocators = [(String, (Int, [Int]))] -> Map String (Int, [Int])
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (String
"alloca", (Int
1, [Int
0]))
    , (String
"malloc", (Int
1, [Int
0]))
    , (String
"calloc", (Int
2, [Int
0, Int
1]))
    , (String
"realloc", (Int
2, [Int
1]))
    , (String
"mem_balloc", (Int
2, [Int
1]))
    , (String
"mem_alloc", (Int
2, [Int
1]))
    , (String
"mem_valloc", (Int
3, [Int
1, Int
2]))
    , (String
"mem_brealloc", (Int
3, [Int
2]))
    , (String
"mem_vrealloc", (Int
4, [Int
2, Int
3]))
    ]

noReturn :: [String]
noReturn :: [String]
noReturn = [String
"__assert_fail", String
"abort", String
"exit", String
"_Exit", String
"logger_abort"]

-- | External functions that don't change the objects their pointers point to
-- in ways the analysis needs to see.
harmless :: [String]
harmless :: [String]
harmless = [String
"free", String
"memset", String
"memcpy", String
"memmove", String
"crypto_memzero", String
"sodium_memzero"]