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

module WithAbstractSymbolicValues.Class where

import Data.SymbolicExpression (FlagStatus(..)) -- TODO

import Data.Indirection
import Data.JumpTarget
import Data.Size
import Data.VerificationCondition
import Data.X86.Opcode
import Data.X86.Instruction
import Data.X86.Register

import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified Data.Set.NonEmpty as NES
import Data.Word
import Data.List

import GHC.Generics (Generic)
import Control.Monad.State.Strict hiding (join)

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


data SymbolicOperation v = SO_Op Opcode Int (Maybe Int) [v] | SO_Bit Int v | SO_SExtend Int Int v | SO_Overwrite Int v v | SO_Plus v v | SO_Minus v v | SO_Times v v

-- | A statepart is either a register or a region in memory
data SStatePart p =
    SSP_Reg Register -- ^ A register
  | SSP_Mem p Int    -- ^ A region with a symbolic address and an immediate size.
 deriving (SStatePart p -> SStatePart p -> Bool
(SStatePart p -> SStatePart p -> Bool)
-> (SStatePart p -> SStatePart p -> Bool) -> Eq (SStatePart p)
forall p. Eq p => SStatePart p -> SStatePart p -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall p. Eq p => SStatePart p -> SStatePart p -> Bool
== :: SStatePart p -> SStatePart p -> Bool
$c/= :: forall p. Eq p => SStatePart p -> SStatePart p -> Bool
/= :: SStatePart p -> SStatePart p -> Bool
Eq, Eq (SStatePart p)
Eq (SStatePart p) =>
(SStatePart p -> SStatePart p -> Ordering)
-> (SStatePart p -> SStatePart p -> Bool)
-> (SStatePart p -> SStatePart p -> Bool)
-> (SStatePart p -> SStatePart p -> Bool)
-> (SStatePart p -> SStatePart p -> Bool)
-> (SStatePart p -> SStatePart p -> SStatePart p)
-> (SStatePart p -> SStatePart p -> SStatePart p)
-> Ord (SStatePart p)
SStatePart p -> SStatePart p -> Bool
SStatePart p -> SStatePart p -> Ordering
SStatePart p -> SStatePart p -> SStatePart p
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 p. Ord p => Eq (SStatePart p)
forall p. Ord p => SStatePart p -> SStatePart p -> Bool
forall p. Ord p => SStatePart p -> SStatePart p -> Ordering
forall p. Ord p => SStatePart p -> SStatePart p -> SStatePart p
$ccompare :: forall p. Ord p => SStatePart p -> SStatePart p -> Ordering
compare :: SStatePart p -> SStatePart p -> Ordering
$c< :: forall p. Ord p => SStatePart p -> SStatePart p -> Bool
< :: SStatePart p -> SStatePart p -> Bool
$c<= :: forall p. Ord p => SStatePart p -> SStatePart p -> Bool
<= :: SStatePart p -> SStatePart p -> Bool
$c> :: forall p. Ord p => SStatePart p -> SStatePart p -> Bool
> :: SStatePart p -> SStatePart p -> Bool
$c>= :: forall p. Ord p => SStatePart p -> SStatePart p -> Bool
>= :: SStatePart p -> SStatePart p -> Bool
$cmax :: forall p. Ord p => SStatePart p -> SStatePart p -> SStatePart p
max :: SStatePart p -> SStatePart p -> SStatePart p
$cmin :: forall p. Ord p => SStatePart p -> SStatePart p -> SStatePart p
min :: SStatePart p -> SStatePart p -> SStatePart p
Ord, (forall x. SStatePart p -> Rep (SStatePart p) x)
-> (forall x. Rep (SStatePart p) x -> SStatePart p)
-> Generic (SStatePart p)
forall x. Rep (SStatePart p) x -> SStatePart p
forall x. SStatePart p -> Rep (SStatePart p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p x. Rep (SStatePart p) x -> SStatePart p
forall p x. SStatePart p -> Rep (SStatePart p) x
$cfrom :: forall p x. SStatePart p -> Rep (SStatePart p) x
from :: forall x. SStatePart p -> Rep (SStatePart p) x
$cto :: forall p x. Rep (SStatePart p) x -> SStatePart p
to :: forall x. Rep (SStatePart p) x -> SStatePart p
Generic)


instance (Cereal.Serialize p) => Cereal.Serialize (SStatePart p)
instance (NFData p) => NFData (SStatePart p)

data Sstate v p = Sstate {
    forall v p. Sstate v p -> Map Register v
sregs  :: M.Map Register v,
    forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem   :: M.Map (p,Maybe ByteSize) v,
    forall v p. Sstate v p -> FlagStatus
sflags :: FlagStatus
  }
  deriving (Sstate v p -> Sstate v p -> Bool
(Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool) -> Eq (Sstate v p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
$c== :: forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
== :: Sstate v p -> Sstate v p -> Bool
$c/= :: forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
/= :: Sstate v p -> Sstate v p -> Bool
Eq,Eq (Sstate v p)
Eq (Sstate v p) =>
(Sstate v p -> Sstate v p -> Ordering)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Sstate v p)
-> (Sstate v p -> Sstate v p -> Sstate v p)
-> Ord (Sstate v p)
Sstate v p -> Sstate v p -> Bool
Sstate v p -> Sstate v p -> Ordering
Sstate v p -> Sstate v p -> Sstate v p
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 p. (Ord v, Ord p) => Eq (Sstate v p)
forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Ordering
forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
$ccompare :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Ordering
compare :: Sstate v p -> Sstate v p -> Ordering
$c< :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
< :: Sstate v p -> Sstate v p -> Bool
$c<= :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
<= :: Sstate v p -> Sstate v p -> Bool
$c> :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
> :: Sstate v p -> Sstate v p -> Bool
$c>= :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
>= :: Sstate v p -> Sstate v p -> Bool
$cmax :: forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
max :: Sstate v p -> Sstate v p -> Sstate v p
$cmin :: forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
min :: Sstate v p -> Sstate v p -> Sstate v p
Ord,(forall x. Sstate v p -> Rep (Sstate v p) x)
-> (forall x. Rep (Sstate v p) x -> Sstate v p)
-> Generic (Sstate v p)
forall x. Rep (Sstate v p) x -> Sstate v p
forall x. Sstate v p -> Rep (Sstate v p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v p x. Rep (Sstate v p) x -> Sstate v p
forall v p x. Sstate v p -> Rep (Sstate v p) x
$cfrom :: forall v p x. Sstate v p -> Rep (Sstate v p) x
from :: forall x. Sstate v p -> Rep (Sstate v p) x
$cto :: forall v p x. Rep (Sstate v p) x -> Sstate v p
to :: forall x. Rep (Sstate v p) x -> Sstate v p
Generic)

instance (Ord v, Cereal.Serialize v,Ord p, Cereal.Serialize p) => Cereal.Serialize (Sstate v p)
instance (NFData v,NFData p) => NFData (Sstate v p)

instance (Show v,Show p) => Show (Sstate v p) where
  show :: Sstate v p -> String
show (Sstate Map Register v
regs Map (p, Maybe ByteSize) v
mem FlagStatus
flags) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((Register, v) -> String) -> [(Register, v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Register, v) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
show_reg ([(Register, v)] -> [String]) -> [(Register, v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map Register v -> [(Register, v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Register v
regs) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((p, Maybe ByteSize), v) -> String)
-> [((p, Maybe ByteSize), v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((p, Maybe ByteSize), v) -> String
forall {a} {a}.
(Show a, Show a) =>
((a, Maybe ByteSize), a) -> String
show_mem ([((p, Maybe ByteSize), v)] -> [String])
-> [((p, Maybe ByteSize), v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (p, Maybe ByteSize) v
mem) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [FlagStatus -> String
show_flags FlagStatus
flags]
   where
    show_reg :: (a, a) -> String
show_reg (a
r,a
v)      = a -> String
forall a. Show a => a -> String
show a
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
    show_mem :: ((a, Maybe ByteSize), a) -> String
show_mem ((a
a,Maybe ByteSize
si),a
v) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe ByteSize -> String
show_size Maybe ByteSize
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v 
    show_flags :: FlagStatus -> String
show_flags          = FlagStatus -> String
forall a. Show a => a -> String
show
    show_size :: Maybe ByteSize -> String
show_size Maybe ByteSize
Nothing   = String
"unknown"
    show_size (Just (ByteSize Int
si)) = Int -> String
forall a. Show a => a -> String
show Int
si





-- | A function initialisation consists of a mapping of state parts to values, and memory relations
data MemRelation = Separate | Aliassing | Unknown
  deriving ((forall x. MemRelation -> Rep MemRelation x)
-> (forall x. Rep MemRelation x -> MemRelation)
-> Generic MemRelation
forall x. Rep MemRelation x -> MemRelation
forall x. MemRelation -> Rep MemRelation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MemRelation -> Rep MemRelation x
from :: forall x. MemRelation -> Rep MemRelation x
$cto :: forall x. Rep MemRelation x -> MemRelation
to :: forall x. Rep MemRelation x -> MemRelation
Generic,MemRelation -> MemRelation -> Bool
(MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool) -> Eq MemRelation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MemRelation -> MemRelation -> Bool
== :: MemRelation -> MemRelation -> Bool
$c/= :: MemRelation -> MemRelation -> Bool
/= :: MemRelation -> MemRelation -> Bool
Eq,Eq MemRelation
Eq MemRelation =>
(MemRelation -> MemRelation -> Ordering)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> MemRelation)
-> (MemRelation -> MemRelation -> MemRelation)
-> Ord MemRelation
MemRelation -> MemRelation -> Bool
MemRelation -> MemRelation -> Ordering
MemRelation -> MemRelation -> MemRelation
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
$ccompare :: MemRelation -> MemRelation -> Ordering
compare :: MemRelation -> MemRelation -> Ordering
$c< :: MemRelation -> MemRelation -> Bool
< :: MemRelation -> MemRelation -> Bool
$c<= :: MemRelation -> MemRelation -> Bool
<= :: MemRelation -> MemRelation -> Bool
$c> :: MemRelation -> MemRelation -> Bool
> :: MemRelation -> MemRelation -> Bool
$c>= :: MemRelation -> MemRelation -> Bool
>= :: MemRelation -> MemRelation -> Bool
$cmax :: MemRelation -> MemRelation -> MemRelation
max :: MemRelation -> MemRelation -> MemRelation
$cmin :: MemRelation -> MemRelation -> MemRelation
min :: MemRelation -> MemRelation -> MemRelation
Ord,Int -> MemRelation -> ShowS
[MemRelation] -> ShowS
MemRelation -> String
(Int -> MemRelation -> ShowS)
-> (MemRelation -> String)
-> ([MemRelation] -> ShowS)
-> Show MemRelation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MemRelation -> ShowS
showsPrec :: Int -> MemRelation -> ShowS
$cshow :: MemRelation -> String
show :: MemRelation -> String
$cshowList :: [MemRelation] -> ShowS
showList :: [MemRelation] -> ShowS
Show)



data FInit v p = FInit (S.Set (SStatePart p,v)) (M.Map (SStatePart p,SStatePart p) MemRelation)
  deriving ((forall x. FInit v p -> Rep (FInit v p) x)
-> (forall x. Rep (FInit v p) x -> FInit v p)
-> Generic (FInit v p)
forall x. Rep (FInit v p) x -> FInit v p
forall x. FInit v p -> Rep (FInit v p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v p x. Rep (FInit v p) x -> FInit v p
forall v p x. FInit v p -> Rep (FInit v p) x
$cfrom :: forall v p x. FInit v p -> Rep (FInit v p) x
from :: forall x. FInit v p -> Rep (FInit v p) x
$cto :: forall v p x. Rep (FInit v p) x -> FInit v p
to :: forall x. Rep (FInit v p) x -> FInit v p
Generic,FInit v p -> FInit v p -> Bool
(FInit v p -> FInit v p -> Bool)
-> (FInit v p -> FInit v p -> Bool) -> Eq (FInit v p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v p. (Eq p, Eq v) => FInit v p -> FInit v p -> Bool
$c== :: forall v p. (Eq p, Eq v) => FInit v p -> FInit v p -> Bool
== :: FInit v p -> FInit v p -> Bool
$c/= :: forall v p. (Eq p, Eq v) => FInit v p -> FInit v p -> Bool
/= :: FInit v p -> FInit v p -> Bool
Eq,Eq (FInit v p)
Eq (FInit v p) =>
(FInit v p -> FInit v p -> Ordering)
-> (FInit v p -> FInit v p -> Bool)
-> (FInit v p -> FInit v p -> Bool)
-> (FInit v p -> FInit v p -> Bool)
-> (FInit v p -> FInit v p -> Bool)
-> (FInit v p -> FInit v p -> FInit v p)
-> (FInit v p -> FInit v p -> FInit v p)
-> Ord (FInit v p)
FInit v p -> FInit v p -> Bool
FInit v p -> FInit v p -> Ordering
FInit v p -> FInit v p -> FInit v p
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 p. (Ord p, Ord v) => Eq (FInit v p)
forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Bool
forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Ordering
forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> FInit v p
$ccompare :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Ordering
compare :: FInit v p -> FInit v p -> Ordering
$c< :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Bool
< :: FInit v p -> FInit v p -> Bool
$c<= :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Bool
<= :: FInit v p -> FInit v p -> Bool
$c> :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Bool
> :: FInit v p -> FInit v p -> Bool
$c>= :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> Bool
>= :: FInit v p -> FInit v p -> Bool
$cmax :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> FInit v p
max :: FInit v p -> FInit v p -> FInit v p
$cmin :: forall v p. (Ord p, Ord v) => FInit v p -> FInit v p -> FInit v p
min :: FInit v p -> FInit v p -> FInit v p
Ord)


instance Cereal.Serialize MemRelation
instance (Cereal.Serialize v,Cereal.Serialize p, Ord p,Ord v) => Cereal.Serialize (FInit v p)

instance NFData MemRelation
instance (NFData p,NFData v) => NFData (FInit v p)


empty_finit :: FInit v p
empty_finit = Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
forall v p.
Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
FInit Set (SStatePart p, v)
forall a. Set a
S.empty Map (SStatePart p, SStatePart p) MemRelation
forall k a. Map k a
M.empty


unknownSize :: Maybe a
unknownSize = Maybe a
forall a. Maybe a
Nothing


class (Ord v,Eq v,Show v, Eq p,Ord p,Show p) => WithAbstractSymbolicValues ctxt v p | ctxt -> v p where 
  sseparate :: ctxt -> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
  senclosed :: ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
  salias :: ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
  ssensitive :: ctxt -> p -> Maybe ByteSize -> v -> Bool
  sread_from_ro_data :: ctxt -> p -> Maybe ByteSize -> Maybe v
  smk_mem_addresses :: ctxt -> String -> v -> S.Set p

  sjoin_values :: Foldable t => ctxt -> String -> t v -> v
  swiden_values :: ctxt -> String -> v -> v
  sjoin_pointers :: ctxt -> [p] -> [p]
  top :: ctxt -> String -> v


  ssemantics :: ctxt -> String -> SymbolicOperation v -> v
  sflg_semantics :: ctxt -> v -> Instruction -> FlagStatus -> FlagStatus
  simmediate :: Integral i => ctxt -> i -> v

  smk_init_reg_value :: ctxt -> Register -> v
  smk_init_mem_value :: ctxt -> String -> p -> Maybe ByteSize -> v

  scall :: ctxt -> Instruction -> State (Sstate v p,VCS v) ()
  sjump :: ctxt -> Instruction -> State (Sstate v p,VCS v) ()
  saddress_has_instruction :: ctxt -> Word64 -> Bool
  skeep_for_finit :: ctxt -> SStatePart p -> v -> Maybe (S.Set p)

  stry_jump_targets :: ctxt -> v -> Maybe (S.Set ResolvedJumpTarget)
  stry_resolve_error_call :: ctxt -> Instruction -> v -> Maybe Indirection

  stry_immediate :: ctxt -> v -> Maybe Word64
  sis_deterministic :: ctxt -> v -> Bool
  scheck_regs_in_postcondition :: ctxt -> v -> v -> Bool