{-# LANGUAGE DeriveGeneric, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}

module Data.VerificationCondition where

import Base

import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import Data.Word
import Data.List

import qualified Data.Serialize as Cereal hiding (get,put)
import Control.DeepSeq
import GHC.Generics


data PointerAnalysisResult v = PointerAnalysisResult {
  forall v. PointerAnalysisResult v -> Maybe v
pa_mem_write :: Maybe v,
  forall v. PointerAnalysisResult v -> [Maybe v]
pa_mem_reads :: [Maybe v]
 }
  deriving ((forall x.
 PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x)
-> (forall x.
    Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v)
-> Generic (PointerAnalysisResult v)
forall x.
Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v
forall x.
PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x.
Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v
forall v x.
PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x
$cfrom :: forall v x.
PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x
from :: forall x.
PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x
$cto :: forall v x.
Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v
to :: forall x.
Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v
Generic,PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
(PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> (PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> Eq (PointerAnalysisResult v)
forall v.
Eq v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v.
Eq v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
== :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
$c/= :: forall v.
Eq v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
/= :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
Eq,Eq (PointerAnalysisResult v)
Eq (PointerAnalysisResult v) =>
(PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering)
-> (PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> (PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> (PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> (PointerAnalysisResult v -> PointerAnalysisResult v -> Bool)
-> (PointerAnalysisResult v
    -> PointerAnalysisResult v -> PointerAnalysisResult v)
-> (PointerAnalysisResult v
    -> PointerAnalysisResult v -> PointerAnalysisResult v)
-> Ord (PointerAnalysisResult v)
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering
PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (PointerAnalysisResult v)
forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering
forall v.
Ord v =>
PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
$ccompare :: forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering
compare :: PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering
$c< :: forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
< :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
$c<= :: forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
<= :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
$c> :: forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
> :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
$c>= :: forall v.
Ord v =>
PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
>= :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool
$cmax :: forall v.
Ord v =>
PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
max :: PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
$cmin :: forall v.
Ord v =>
PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
min :: PointerAnalysisResult v
-> PointerAnalysisResult v -> PointerAnalysisResult v
Ord)

instance Show v => Show (PointerAnalysisResult v) where
  show :: PointerAnalysisResult v -> String
show (PointerAnalysisResult Maybe v
Nothing  [Maybe v]
rs) = [Maybe v] -> String
forall {a}. Show a => [Maybe a] -> String
show_pars [Maybe v]
rs
  show (PointerAnalysisResult (Just v
w) [Maybe v]
rs) = v -> String
forall a. Show a => a -> String
show v
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <-- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Maybe v] -> String
forall {a}. Show a => [Maybe a] -> String
show_pars [Maybe v]
rs


show_pars :: [Maybe a] -> String
show_pars [Maybe a]
pars = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Maybe a -> String) -> [Maybe a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Maybe a -> String
forall {a}. Show a => Maybe a -> String
show_pa [Maybe a]
pars) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
 where
  show_pa :: Maybe a -> String
show_pa Maybe a
Nothing  = String
"_"
  show_pa (Just a
v) = a -> String
forall a. Show a => a -> String
show a
v

data VerificationCondition v =
    FunctionPointers      Word64 IS.IntSet -- ^ A set of function pointers passed to a function
  | PointerAnalysis       Word64 (PointerAnalysisResult v) -- ^ A pointer analysis result for the instruction at the address
  deriving ((forall x.
 VerificationCondition v -> Rep (VerificationCondition v) x)
-> (forall x.
    Rep (VerificationCondition v) x -> VerificationCondition v)
-> Generic (VerificationCondition v)
forall x.
Rep (VerificationCondition v) x -> VerificationCondition v
forall x.
VerificationCondition v -> Rep (VerificationCondition v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x.
Rep (VerificationCondition v) x -> VerificationCondition v
forall v x.
VerificationCondition v -> Rep (VerificationCondition v) x
$cfrom :: forall v x.
VerificationCondition v -> Rep (VerificationCondition v) x
from :: forall x.
VerificationCondition v -> Rep (VerificationCondition v) x
$cto :: forall v x.
Rep (VerificationCondition v) x -> VerificationCondition v
to :: forall x.
Rep (VerificationCondition v) x -> VerificationCondition v
Generic,VerificationCondition v -> VerificationCondition v -> Bool
(VerificationCondition v -> VerificationCondition v -> Bool)
-> (VerificationCondition v -> VerificationCondition v -> Bool)
-> Eq (VerificationCondition v)
forall v.
Eq v =>
VerificationCondition v -> VerificationCondition v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v.
Eq v =>
VerificationCondition v -> VerificationCondition v -> Bool
== :: VerificationCondition v -> VerificationCondition v -> Bool
$c/= :: forall v.
Eq v =>
VerificationCondition v -> VerificationCondition v -> Bool
/= :: VerificationCondition v -> VerificationCondition v -> Bool
Eq,Eq (VerificationCondition v)
Eq (VerificationCondition v) =>
(VerificationCondition v -> VerificationCondition v -> Ordering)
-> (VerificationCondition v -> VerificationCondition v -> Bool)
-> (VerificationCondition v -> VerificationCondition v -> Bool)
-> (VerificationCondition v -> VerificationCondition v -> Bool)
-> (VerificationCondition v -> VerificationCondition v -> Bool)
-> (VerificationCondition v
    -> VerificationCondition v -> VerificationCondition v)
-> (VerificationCondition v
    -> VerificationCondition v -> VerificationCondition v)
-> Ord (VerificationCondition v)
VerificationCondition v -> VerificationCondition v -> Bool
VerificationCondition v -> VerificationCondition v -> Ordering
VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (VerificationCondition v)
forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Bool
forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Ordering
forall v.
Ord v =>
VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
$ccompare :: forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Ordering
compare :: VerificationCondition v -> VerificationCondition v -> Ordering
$c< :: forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Bool
< :: VerificationCondition v -> VerificationCondition v -> Bool
$c<= :: forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Bool
<= :: VerificationCondition v -> VerificationCondition v -> Bool
$c> :: forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Bool
> :: VerificationCondition v -> VerificationCondition v -> Bool
$c>= :: forall v.
Ord v =>
VerificationCondition v -> VerificationCondition v -> Bool
>= :: VerificationCondition v -> VerificationCondition v -> Bool
$cmax :: forall v.
Ord v =>
VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
max :: VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
$cmin :: forall v.
Ord v =>
VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
min :: VerificationCondition v
-> VerificationCondition v -> VerificationCondition v
Ord)

instance Show v => Show (VerificationCondition v) where
  show :: VerificationCondition v -> String
show (FunctionPointers Word64
a IntSet
ptrs) = String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": function pointer loaded " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IntSet -> String
showHex_set IntSet
ptrs
  show (PointerAnalysis Word64
a PointerAnalysisResult v
r)     = String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PointerAnalysisResult v -> String
forall a. Show a => a -> String
show PointerAnalysisResult v
r



instance Cereal.Serialize v => Cereal.Serialize (PointerAnalysisResult v)
instance Cereal.Serialize v => Cereal.Serialize (VerificationCondition v)

instance NFData v => NFData (PointerAnalysisResult v)
instance NFData v => NFData (VerificationCondition v)

type VCS v = S.Set (VerificationCondition v)



gather_pa_results :: VCS v -> IM.IntMap (PointerAnalysisResult v)
gather_pa_results :: forall v. VCS v -> IntMap (PointerAnalysisResult v)
gather_pa_results = (VerificationCondition v
 -> IntMap (PointerAnalysisResult v)
 -> IntMap (PointerAnalysisResult v))
-> IntMap (PointerAnalysisResult v)
-> Set (VerificationCondition v)
-> IntMap (PointerAnalysisResult v)
forall a b. (a -> b -> b) -> b -> Set a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VerificationCondition v
-> IntMap (PointerAnalysisResult v)
-> IntMap (PointerAnalysisResult v)
forall {v}.
VerificationCondition v
-> IntMap (PointerAnalysisResult v)
-> IntMap (PointerAnalysisResult v)
gather IntMap (PointerAnalysisResult v)
forall a. IntMap a
IM.empty
 where
  gather :: VerificationCondition v
-> IntMap (PointerAnalysisResult v)
-> IntMap (PointerAnalysisResult v)
gather (PointerAnalysis Word64
a PointerAnalysisResult v
par) = Int
-> PointerAnalysisResult v
-> IntMap (PointerAnalysisResult v)
-> IntMap (PointerAnalysisResult v)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) PointerAnalysisResult v
par
  gather VerificationCondition v
_  = IntMap (PointerAnalysisResult v)
-> IntMap (PointerAnalysisResult v)
forall a. a -> a
id