{-# LANGUAGE OverloadedStrings #-}
module Tokstyle.Analysis.SecurityRank.Lattice
    ( SecurityRank(..)
    , mergeRank
    , TaintState
    ) where

import           Data.Map.Strict         (Map)
import           Data.Text               (Text)
import           Tokstyle.Analysis.Types (AbstractLocation)

-- | Represents the security level of data.
-- The Ord instance defines the lattice structure, where the minimum element
-- is the most restrictive/tainted.
-- Bottom < Safe < Rank 0 < Rank 1 < ...
data SecurityRank
    = Bottom   -- ^ Uninitialized or unreachable code path.
    | Safe     -- ^ A value known to be safe (e.g., a literal).
    | Rank Int -- ^ A tainted value with a specific integer rank.
    deriving (SecurityRank -> SecurityRank -> Bool
(SecurityRank -> SecurityRank -> Bool)
-> (SecurityRank -> SecurityRank -> Bool) -> Eq SecurityRank
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SecurityRank -> SecurityRank -> Bool
$c/= :: SecurityRank -> SecurityRank -> Bool
== :: SecurityRank -> SecurityRank -> Bool
$c== :: SecurityRank -> SecurityRank -> Bool
Eq, Int -> SecurityRank -> ShowS
[SecurityRank] -> ShowS
SecurityRank -> String
(Int -> SecurityRank -> ShowS)
-> (SecurityRank -> String)
-> ([SecurityRank] -> ShowS)
-> Show SecurityRank
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SecurityRank] -> ShowS
$cshowList :: [SecurityRank] -> ShowS
show :: SecurityRank -> String
$cshow :: SecurityRank -> String
showsPrec :: Int -> SecurityRank -> ShowS
$cshowsPrec :: Int -> SecurityRank -> ShowS
Show)

-- | The ordering defines the lattice. A lower value is "more tainted".
instance Ord SecurityRank where
    compare :: SecurityRank -> SecurityRank -> Ordering
compare SecurityRank
Bottom      SecurityRank
Bottom   = Ordering
EQ
    compare SecurityRank
Bottom      SecurityRank
_        = Ordering
LT
    compare SecurityRank
_           SecurityRank
Bottom   = Ordering
GT
    compare SecurityRank
Safe        SecurityRank
Safe     = Ordering
EQ
    compare SecurityRank
Safe        SecurityRank
_        = Ordering
GT
    compare SecurityRank
_           SecurityRank
Safe     = Ordering
LT
    compare (Rank Int
a)    (Rank Int
b) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
a Int
b

-- | The merge operation for the lattice. When control paths join,
-- we take the most restrictive (i.e., minimum) rank.
mergeRank :: SecurityRank -> SecurityRank -> SecurityRank
mergeRank :: SecurityRank -> SecurityRank -> SecurityRank
mergeRank = SecurityRank -> SecurityRank -> SecurityRank
forall a. Ord a => a -> a -> a
min

-- | The TaintState is the fact that flows through the analysis. It maps every
-- abstract location currently in scope to its security rank.
type TaintState = Map AbstractLocation SecurityRank