{-# LANGUAGE PartialTypeSignatures, MultiParamTypeClasses, DeriveGeneric, DefaultSignatures, FlexibleContexts, StrictData #-}

{-|
Module      : Pointers
Description : Functions for dealing with symbolic pointers and abstraction.
-}
module WithNoAbstraction.Pointers where

import Base
import Config

import Data.SymbolicExpression
import Data.Symbol
import Data.L0
import Data.SValue
import Data.SPointer
import Data.X86.Register

import WithAbstractSymbolicValues.Class
import WithAbstractSymbolicValues.FInit

import Binary.Generic


import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set.NonEmpty as NES
import Data.Int (Int64)

import Data.List
import Data.Word 
import Data.Maybe
import Debug.Trace

import GHC.Generics


-- | An abstract domain for pointers
data PointerDomain =
    Domain_Bases    (NES.NESet PointerBase)  -- a non-empty set of bases
  | Domain_Sources  (NES.NESet BotSrc)       -- a possibly empty set of sources
  deriving ((forall x. PointerDomain -> Rep PointerDomain x)
-> (forall x. Rep PointerDomain x -> PointerDomain)
-> Generic PointerDomain
forall x. Rep PointerDomain x -> PointerDomain
forall x. PointerDomain -> Rep PointerDomain x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PointerDomain -> Rep PointerDomain x
from :: forall x. PointerDomain -> Rep PointerDomain x
$cto :: forall x. Rep PointerDomain x -> PointerDomain
to :: forall x. Rep PointerDomain x -> PointerDomain
Generic,PointerDomain -> PointerDomain -> Bool
(PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool) -> Eq PointerDomain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PointerDomain -> PointerDomain -> Bool
== :: PointerDomain -> PointerDomain -> Bool
$c/= :: PointerDomain -> PointerDomain -> Bool
/= :: PointerDomain -> PointerDomain -> Bool
Eq,Eq PointerDomain
Eq PointerDomain =>
(PointerDomain -> PointerDomain -> Ordering)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> PointerDomain)
-> (PointerDomain -> PointerDomain -> PointerDomain)
-> Ord PointerDomain
PointerDomain -> PointerDomain -> Bool
PointerDomain -> PointerDomain -> Ordering
PointerDomain -> PointerDomain -> PointerDomain
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 :: PointerDomain -> PointerDomain -> Ordering
compare :: PointerDomain -> PointerDomain -> Ordering
$c< :: PointerDomain -> PointerDomain -> Bool
< :: PointerDomain -> PointerDomain -> Bool
$c<= :: PointerDomain -> PointerDomain -> Bool
<= :: PointerDomain -> PointerDomain -> Bool
$c> :: PointerDomain -> PointerDomain -> Bool
> :: PointerDomain -> PointerDomain -> Bool
$c>= :: PointerDomain -> PointerDomain -> Bool
>= :: PointerDomain -> PointerDomain -> Bool
$cmax :: PointerDomain -> PointerDomain -> PointerDomain
max :: PointerDomain -> PointerDomain -> PointerDomain
$cmin :: PointerDomain -> PointerDomain -> PointerDomain
min :: PointerDomain -> PointerDomain -> PointerDomain
Ord,Int -> PointerDomain -> ShowS
[PointerDomain] -> ShowS
PointerDomain -> String
(Int -> PointerDomain -> ShowS)
-> (PointerDomain -> String)
-> ([PointerDomain] -> ShowS)
-> Show PointerDomain
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PointerDomain -> ShowS
showsPrec :: Int -> PointerDomain -> ShowS
$cshow :: PointerDomain -> String
show :: PointerDomain -> String
$cshowList :: [PointerDomain] -> ShowS
showList :: [PointerDomain] -> ShowS
Show)



-- | Returns true iff a symbol is associated with the address.
address_has_external_symbol :: a -> a -> Bool
address_has_external_symbol a
bin a
a =
  case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ a -> IntMap Symbol
forall {a}. BinaryClass a => a -> IntMap Symbol
binary_get_symbol_table a
bin of
    Just (PointerToLabel String
_ Bool
ex)  -> Bool
ex
    Just (PointerToObject String
_ Bool
ex) -> Bool
ex
    Just (AddressOfObject String
_ Bool
ex) -> Bool
ex
    Just (AddressOfLabel String
_ Bool
ex)  -> Bool
ex
    Maybe Symbol
_ -> Bool
False





-- | Returns true iff the expression is an immediate address falling into the range of sections of the binary
expr_is_global_immediate :: bin -> SimpleExpr -> Bool
expr_is_global_immediate bin
bin (SE_Immediate Word64
a)
  | bin -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
is_roughly_an_address bin
bin (Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) = bin -> Word64 -> Bool
forall {a} {a}. (BinaryClass a, Integral a) => a -> a -> Bool
address_has_external_symbol bin
bin Word64
a Bool -> Bool -> Bool
|| bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address bin
bin (Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (String, String, Word64, Word64, Word64)
forall a. Maybe a
Nothing
  | Bool
otherwise = Bool
False
expr_is_global_immediate bin
ctxt SimpleExpr
_ = Bool
False


-- | Returns true if the expression has a local pointerbase
expr_is_highly_likely_local_pointer :: bin -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer bin
bin SimpleExpr
e = bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain bin
bin FInit SValue SPointer
forall {v} {p}. FInit v p
no_finit SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall {t}. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` Bool -> PointerDomain -> Bool
is_local_pointer_domain Bool
True
expr_is_maybe_local_pointer :: bin -> SimpleExpr -> Bool
expr_is_maybe_local_pointer         bin
bin SimpleExpr
e = bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain bin
bin FInit SValue SPointer
forall {v} {p}. FInit v p
no_finit SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall {t}. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` Bool -> PointerDomain -> Bool
is_local_pointer_domain Bool
False


expr_is_highly_likely_global_pointer :: bin -> SimpleExpr -> Bool
expr_is_highly_likely_global_pointer bin
bin SimpleExpr
e = bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain bin
bin FInit SValue SPointer
forall {v} {p}. FInit v p
no_finit SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall {t}. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` Bool -> PointerDomain -> Bool
is_global_pointer_domain Bool
True
expr_is_maybe_global_pointer :: bin -> SimpleExpr -> Bool
expr_is_maybe_global_pointer         bin
bin SimpleExpr
e = bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain bin
bin FInit SValue SPointer
forall {v} {p}. FInit v p
no_finit SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall {t}. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` Bool -> PointerDomain -> Bool
is_global_pointer_domain Bool
False


no_finit :: FInit v p
no_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

-- | Returns true iff the give domain is highly likely local to the current function
is_local_pointer_domain :: Bool -> PointerDomain -> Bool
is_local_pointer_domain Bool
necc (Domain_Bases NESet PointerBase
bs) = (PointerBase -> Bool) -> NESet PointerBase -> Bool
forall {a}. (a -> Bool) -> NESet a -> Bool
quant PointerBase -> Bool
is_local_base NESet PointerBase
bs
 where
  is_local_base :: PointerBase -> Bool
is_local_base PointerBase
StackPointer     = Bool
True
  is_local_base PointerBase
_                = Bool
False
  quant :: (a -> Bool) -> NESet a -> Bool
quant                          = if Bool
necc then (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all else (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
is_local_pointer_domain Bool
necc (Domain_Sources NESet BotSrc
srcs) = (BotSrc -> Bool) -> NESet BotSrc -> Bool
forall {a}. (a -> Bool) -> NESet a -> Bool
quant BotSrc -> Bool
is_local_src NESet BotSrc
srcs
 where
  is_local_src :: BotSrc -> Bool
is_local_src (BotSrc
Src_StackPointer)  = Bool
True
  is_local_src BotSrc
_                   = Bool
False
  quant :: (a -> Bool) -> NESet a -> Bool
quant                            = if Bool
necc then (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all else (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any

-- | Returns true iff the give domain is highly likely global
is_global_pointer_domain :: Bool -> PointerDomain -> Bool
is_global_pointer_domain Bool
necc (Domain_Bases NESet PointerBase
bs) = (PointerBase -> Bool) -> NESet PointerBase -> Bool
forall {a}. (a -> Bool) -> NESet a -> Bool
quant PointerBase -> Bool
is_global_base NESet PointerBase
bs
 where
  is_global_base :: PointerBase -> Bool
is_global_base (GlobalAddress Word64
_) = Bool
True
  is_global_base PointerBase
_                 = Bool
False
  quant :: (a -> Bool) -> NESet a -> Bool
quant                            = if Bool
necc then (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all else (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
is_global_pointer_domain Bool
necc (Domain_Sources NESet BotSrc
srcs) = (BotSrc -> Bool) -> NESet BotSrc -> Bool
forall {a}. (a -> Bool) -> NESet a -> Bool
quant BotSrc -> Bool
is_global_src NESet BotSrc
srcs
 where
  is_global_src :: BotSrc -> Bool
is_global_src (Src_ImmediateAddress Word64
_) = Bool
True
  is_global_src BotSrc
_                        = Bool
False
  quant :: (a -> Bool) -> NESet a -> Bool
quant                                  = if Bool
necc then (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all else (a -> Bool) -> NESet a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any


-- | Returns true if the expression has known pointerbases.
expr_highly_likely_pointer :: bin -> FInit SValue SPointer -> SimpleExpr -> Bool
expr_highly_likely_pointer bin
bin FInit SValue SPointer
finit SimpleExpr
e = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> Bool
forall a. Set a -> Bool
S.null (Set PointerBase -> Bool) -> Set PointerBase -> Bool
forall a b. (a -> b) -> a -> b
$ bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit SimpleExpr
e

{--
-- | Returns true if the expression has a heap pointerbase
expr_is_highly_likely_heap_pointer ctxt e = get_pointer_domain ctxt e `existsAndSatisfies` is_heap_pointer_domain ctxt

is_heap_pointer_domain ctxt (Domain_Bases bs) = all is_heap_base bs
 where
  is_heap_base (Malloc id hash)     = True
  is_heap_base _                    = False
is_heap_pointer_domain ctxt (Domain_Sources srcs) = all is_heap_source srcs
 where
  is_heap_source (Src_Malloc id hash) = True
  is_heap_source _                    = False

--}



-- | Returns true iff the given symbolic regions are necessarily separate.
-- TODO: add VCS, not necc
necessarily_separate :: p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 (Just SimpleExpr
si0) SimpleExpr
a1 (Just SimpleExpr
si1) = 
  case (SimpleExpr
si0,SimpleExpr
si1) of
    (SE_Immediate Word64
si0', SE_Immediate Word64
si1') -> SimpleExpr -> Word64 -> SimpleExpr -> Word64 -> Bool
forall {b}.
(Ord b, Num b) =>
SimpleExpr -> b -> SimpleExpr -> b -> Bool
necessarily_separate_expressions SimpleExpr
a0 Word64
si0' SimpleExpr
a1 Word64
si1' Bool -> Bool -> Bool
|| p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
necessarily_separate_no_size p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 SimpleExpr
a1 
    (SimpleExpr, SimpleExpr)
_ -> p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
necessarily_separate_no_size p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 SimpleExpr
a1
necessarily_separate p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 Maybe SimpleExpr
_ SimpleExpr
a1 Maybe SimpleExpr
_ = p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
necessarily_separate_no_size p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 SimpleExpr
a1 

necessarily_separate_no_size :: p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> SimpleExpr
-> Bool
necessarily_separate_no_size p
bin FInit SValue SPointer
finit String
msg SimpleExpr
a0 SimpleExpr
a1 = SimpleExpr
a0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
/= SimpleExpr
a1 Bool -> Bool -> Bool
&& ((Bool, Bool) -> Bool
use_domains ((Bool, Bool) -> Bool) -> (Bool, Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ p
-> FInit SValue SPointer
-> SimpleExpr
-> SimpleExpr
-> (Bool, Bool)
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> SimpleExpr
-> SimpleExpr
-> (Bool, Bool)
separate_pointer_domains p
bin FInit SValue SPointer
finit SimpleExpr
a0 SimpleExpr
a1)
 where
  use_domains :: (Bool, Bool) -> Bool
use_domains (Bool
necc,Bool
poss)
    | Bool
necc                    = Bool
True
    | Bool
poss                    = Bool
True
    | SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
a0 SimpleExpr
a1 = Bool
False
    | String
msg String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"write" Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1) = String -> Bool -> Bool
forall a. String -> a -> a
trace (String
"Don't know separation of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
a0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
a1) Bool
False
    | Bool
otherwise               = Bool
False

-- | Returns true iff the given symbolic regions are necessarily equal.
necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
a0 SimpleExpr
a1 = SimpleExpr
a0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
a1 Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1)









-- | Returns true iff the given symbolic regions are ncessarily separate.
-- For example:
--    @[RSP-16,4]@ is separate from @[RSP-12,8]@
--    @[RSP+8,4]@ is separate from @[RSP,8]@
--
-- If none of the cases apply where it can be shjown arithmetically that the expressions are separate,
-- we check whether the expressions can be proven separate based on their domains (see 'separate_pointer_domains').
necessarily_separate_expressions :: SimpleExpr -> b -> SimpleExpr -> b -> Bool
necessarily_separate_expressions SimpleExpr
a0 b
si0 SimpleExpr
a1 b
si1 = Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1) Bool -> Bool -> Bool
&& (SimpleExpr
a0,b
si0) (SimpleExpr, b) -> (SimpleExpr, b) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SimpleExpr
a1,b
si1) Bool -> Bool -> Bool
&& SimpleExpr -> SimpleExpr -> Bool
sep SimpleExpr
a0 SimpleExpr
a1
 where
  -- two immediate addresses
  sep :: SimpleExpr -> SimpleExpr -> Bool
sep (SE_Immediate Word64
a0)
      (SE_Immediate Word64
a1) =
    Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0 b -> b -> b
forall a. Num a => a -> a -> a
+ b
si0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 Bool -> Bool -> Bool
|| Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 b -> b -> b
forall a. Num a => a -> a -> a
+ b
si1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0
  -- v0 - i0 |x| v0 - i1 <==> v0 - i0 + si0 <= v0 - i1 || v1 - i1 + si1 <= v0 - i0 <==> i0-si0 >= i1 || i1-si1 >= i0
  sep (SE_Op Operator
Minus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Minus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& (Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 b -> b -> b
forall a. Num a => a -> a -> a
- b
si0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Bool -> Bool -> Bool
|| Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 b -> b -> b
forall a. Num a => a -> a -> a
- b
si1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0)
  -- v0 - i0 |x| v0 + i1 <==> True
  sep (SE_Op Operator
Minus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Plus  Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1
  sep (SE_Op Operator
Plus  Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Minus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1
  -- v0 - i0 |x| v0 <==> i0 >= si0
  sep (SE_Op Operator
Minus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
       SimpleExpr
v1 = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= b
si0
  sep SimpleExpr
v0
      (SE_Op Operator
Minus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= b
si1
  -- v0 + i0 |x| v0 + i1 <==> v0 + i0 + si0 <= v0 + i1 || v0 + i1 + si1 <= v0 + i0 <==> i0+si0 <= i1 || i1+si1 <= i0
  sep (SE_Op Operator
Plus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Plus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) =  SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& (Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 b -> b -> b
forall a. Num a => a -> a -> a
+ b
si0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Bool -> Bool -> Bool
|| Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 b -> b -> b
forall a. Num a => a -> a -> a
+ b
si1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0)
  -- v0 + i0 |x| v0 <==> i0 >= si1
  sep (SE_Op Operator
Plus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      SimpleExpr
v1 = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= b
si1
  sep SimpleExpr
v1
      (SE_Op Operator
Plus Int
_ [SimpleExpr
v0,SE_Immediate Word64
i0]) = SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= b
si1
  -- remainder
  sep SimpleExpr
a0 SimpleExpr
a1 = Bool
False




-- | Returns true iff the given symbolic region is necessarily enclosed in the other.
-- For example:
--    @[RSP-16,4]@ is enclosed in @[RSP-18,8]@
--    @[RSP+4,4]@ is enclosed in @[RSP,8]@
--
-- Will return @False@ if the expressions contain bottom.
necessarily_enclosed :: SimpleExpr -> p -> SimpleExpr -> p -> Bool
necessarily_enclosed SimpleExpr
a0 p
si0 SimpleExpr
a1 p
si1 =
  Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1) Bool -> Bool -> Bool
&& SimpleExpr -> SimpleExpr -> Bool
enc SimpleExpr
a0 SimpleExpr
a1
 where
  -- v0 - i0 enc v0 - i1 <==> i1 >= i0  && si0 - i0 <= si1 - i1     (WHEN si0 >= i0 && si1 >= i1)
  enc :: SimpleExpr -> SimpleExpr -> Bool
enc (SE_Op Operator
Minus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Minus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& 
      if p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& p
si1 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 then
        Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 p -> p -> p
forall a. Num a => a -> a -> a
- p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 p -> p -> p
forall a. Num a => a -> a -> a
- p
si1
      else if p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& p
si1 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 then
        Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0
      else if p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& p
si1 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 then
        Bool
False
      else if p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& p
si1 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 then
        Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& p -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
si0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
i0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= p -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
si1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
i1
      else
        Bool
False
  -- v0 + i0 enc v0 + i1 <==> i0 >= i1 && i0 + si0 <= i1 + si1
  enc (SE_Op Operator
Plus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Plus Int
_ [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64
i0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
i1 Bool -> Bool -> Bool
&& Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 p -> p -> p
forall a. Num a => a -> a -> a
+ p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 p -> p -> p
forall a. Num a => a -> a -> a
+ p
si1
  -- v0 + i0 enc v0 <==> i0 + si0 <= si1
  enc (SE_Op Operator
Plus Int
_ [SimpleExpr
v0, SE_Immediate Word64
i0])
      SimpleExpr
v1 =
    SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1 Bool -> Bool -> Bool
&& Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 p -> p -> p
forall a. Num a => a -> a -> a
+ p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= p
si1
  -- immediates
  enc (SE_Immediate Word64
a0) (SE_Immediate Word64
a1) = 
    (Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0::Int64) Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 Bool -> Bool -> Bool
&& (Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0::Int64) Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ p -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
si0 Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ p -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
si1
  -- v0 enc v0 <==> si0 <= si1
  enc SimpleExpr
v0 SimpleExpr
v1
    | SimpleExpr
v0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
v1  = p
si0 p -> p -> Bool
forall a. Ord a => a -> a -> Bool
<= p
si1
    | Bool
otherwise = Bool
False




-- * Pointer Domains
--
-- Turn a symbolic expression into a pointer domain: either a pointer base, or a set of sources.
--
-- * A 'PointerBase' is a positive addend of a symbolic expression that likely represents a pointer. It can be a stack pointer, an immediate pointer into a section, or a pointer to a known symbol.
-- * A source is some statepart whose initial value affects the value of the pointer.
--
get_pointer_domain ::
  BinaryClass bin =>
     bin                     -- ^ The binary
  -> FInit SValue SPointer   -- ^ The current context
  -> SimpleExpr              -- ^ A symbolic expression 
  -> Maybe PointerDomain     -- ^ A pointer domain
get_pointer_domain :: forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain bin
bin FInit SValue SPointer
finit SimpleExpr
e =
  let bs :: Set PointerBase
bs = bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit SimpleExpr
e in
    if Bool -> Bool
not (Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs) then --  && S.size bs <= get_max_num_of_bases then TODO
      PointerDomain -> Maybe PointerDomain
forall a. a -> Maybe a
Just (PointerDomain -> Maybe PointerDomain)
-> PointerDomain -> Maybe PointerDomain
forall a b. (a -> b) -> a -> b
$ NESet PointerBase -> PointerDomain
Domain_Bases (NESet PointerBase -> PointerDomain)
-> NESet PointerBase -> PointerDomain
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> NESet PointerBase
forall a. Set a -> NESet a
NES.unsafeFromSet Set PointerBase
bs
    else let srcs :: Set BotSrc
srcs = bin -> SimpleExpr -> Set BotSrc
forall {t}. BinaryClass t => t -> SimpleExpr -> Set BotSrc
srcs_of_expr bin
bin SimpleExpr
e in
      if Bool -> Bool
not (Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs) Bool -> Bool -> Bool
&& Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
100 then -- TODO get_max_num_of_sources then
        PointerDomain -> Maybe PointerDomain
forall a. a -> Maybe a
Just (PointerDomain -> Maybe PointerDomain)
-> PointerDomain -> Maybe PointerDomain
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> PointerDomain
Domain_Sources (NESet BotSrc -> PointerDomain) -> NESet BotSrc -> PointerDomain
forall a b. (a -> b) -> a -> b
$  Set BotSrc -> NESet BotSrc
forall a. Set a -> NESet a
NES.unsafeFromSet Set BotSrc
srcs
      else
        Maybe PointerDomain
forall a. Maybe a
Nothing

 where
  --get_max_num_of_bases   = ctxt_max_num_of_bases $ f_ctxt ctxt
  --get_max_num_of_sources = ctxt_max_num_of_sources $ f_ctxt ctxt


get_pointer_base_set ::
  BinaryClass bin =>
     bin                     -- ^ The binary
  -> FInit SValue SPointer   -- ^ The current context
  -> SimpleExpr
  -> S.Set PointerBase
get_pointer_base_set :: forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit (Bottom (FromNonDeterminism NESet SimpleExpr
es)) = Set (Set PointerBase) -> Set PointerBase
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set PointerBase) -> Set PointerBase)
-> Set (Set PointerBase) -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set PointerBase)
-> Set SimpleExpr -> Set (Set PointerBase)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit) (Set SimpleExpr -> Set (Set PointerBase))
-> Set SimpleExpr -> Set (Set PointerBase)
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es -- TODO non-empty union?
get_pointer_base_set bin
bin FInit SValue SPointer
finit (SE_Op Operator
Plus Int
_ [SimpleExpr]
es)                = Set (Set PointerBase) -> Set PointerBase
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set PointerBase) -> Set PointerBase)
-> Set (Set PointerBase) -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set PointerBase)
-> Set SimpleExpr -> Set (Set PointerBase)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit) (Set SimpleExpr -> Set (Set PointerBase))
-> Set SimpleExpr -> Set (Set PointerBase)
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr]
es
get_pointer_base_set bin
bin FInit SValue SPointer
finit (SE_Op Operator
Minus Int
_ (SimpleExpr
e:[SimpleExpr]
es))           = bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit SimpleExpr
e
get_pointer_base_set bin
bin FInit SValue SPointer
finit (SE_Op Operator
And Int
_ [SimpleExpr
e,SE_Immediate Word64
_]) = bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit SimpleExpr
e
get_pointer_base_set bin
bin FInit SValue SPointer
finit (SE_Op Operator
And Int
_ [SE_Immediate Word64
_,SimpleExpr
e]) = bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
finit SimpleExpr
e
get_pointer_base_set bin
bin (FInit Set (SStatePart SPointer, SValue)
sps Map (SStatePart SPointer, SStatePart SPointer) MemRelation
m) SimpleExpr
e                        = SimpleExpr -> Set PointerBase
get_pointer_base SimpleExpr
e

 where
  get_pointer_base :: SimpleExpr -> S.Set PointerBase
  get_pointer_base :: SimpleExpr -> Set PointerBase
get_pointer_base (SE_Immediate Word64
a)
    | bin -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_global_immediate bin
bin SimpleExpr
e = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ Word64 -> PointerBase
GlobalAddress Word64
a 
    | Bool
otherwise = Set PointerBase
forall a. Set a
S.empty
  get_pointer_base (SE_Var StatePart
sp)                        = StatePart -> Set PointerBase
statepart_to_pointerbase StatePart
sp
  get_pointer_base (SE_Malloc Maybe Word64
id Maybe String
hash)                = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> PointerBase
Malloc Maybe Word64
id Maybe String
hash
  get_pointer_base (Bottom (FromPointerBases NESet PointerBase
bs))     = NESet PointerBase -> Set PointerBase
forall a. NESet a -> Set a
NES.toSet NESet PointerBase
bs
  get_pointer_base SimpleExpr
e                                  = Set PointerBase
forall a. Set a
S.empty


  statepart_to_pointerbase :: StatePart -> S.Set PointerBase
  statepart_to_pointerbase :: StatePart -> Set PointerBase
statepart_to_pointerbase (SP_Mem (SE_Immediate Word64
a) Int
8)  = case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) (bin -> IntMap Symbol
forall {a}. BinaryClass a => a -> IntMap Symbol
binary_get_symbol_table bin
bin) of
                                                            Just Symbol
sym -> PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ Word64 -> PointerBase
GlobalAddress Word64
a
                                                            Maybe Symbol
Nothing -> Set PointerBase
forall a. Set a
S.empty
  statepart_to_pointerbase (SP_Reg (RegSeg SReg
FS))         = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton PointerBase
ThreadLocalStorage
  statepart_to_pointerbase (SP_Reg (Reg64 GPR
RSP))         = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ PointerBase
StackPointer
  statepart_to_pointerbase StatePart
sp
    | ((SStatePart SPointer, SStatePart SPointer) -> Bool)
-> [(SStatePart SPointer, SStatePart SPointer)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (StatePart -> (SStatePart SPointer, SStatePart SPointer) -> Bool
has_mem_rel StatePart
sp) ([(SStatePart SPointer, SStatePart SPointer)] -> Bool)
-> [(SStatePart SPointer, SStatePart SPointer)] -> Bool
forall a b. (a -> b) -> a -> b
$ Map (SStatePart SPointer, SStatePart SPointer) MemRelation
-> [(SStatePart SPointer, SStatePart SPointer)]
forall k a. Map k a -> [k]
M.keys Map (SStatePart SPointer, SStatePart SPointer) MemRelation
m                   = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ StatePart -> PointerBase
BaseIsStatePart StatePart
sp
  statepart_to_pointerbase StatePart
_                            = Set PointerBase
forall a. Set a
S.empty


  has_mem_rel :: StatePart -> (SStatePart SPointer, SStatePart SPointer) -> Bool
has_mem_rel (SP_Reg Register
r)    (SStatePart SPointer
sp0,SStatePart SPointer
sp1) = Register -> SStatePart SPointer
forall p. Register -> SStatePart p
SSP_Reg Register
r SStatePart SPointer -> [SStatePart SPointer] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SStatePart SPointer
sp0,SStatePart SPointer
sp1]
  has_mem_rel (SP_Mem SimpleExpr
a Int
si) (SStatePart SPointer
sp0,SStatePart SPointer
sp1) = SPointer -> Int -> SStatePart SPointer
forall p. p -> Int -> SStatePart p
SSP_Mem (SimpleExpr -> SPointer
Ptr_Concrete SimpleExpr
a) Int
si  SStatePart SPointer -> [SStatePart SPointer] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SStatePart SPointer
sp0,SStatePart SPointer
sp1]




-- | Returns true iff the two given expressions can be shown to be separate based on their domains.
separate_pointer_domains :: p
-> FInit SValue SPointer
-> SimpleExpr
-> SimpleExpr
-> (Bool, Bool)
separate_pointer_domains p
bin FInit SValue SPointer
finit SimpleExpr
a0 SimpleExpr
a1 =
  let dom0 :: Maybe PointerDomain
dom0 = p -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain p
bin FInit SValue SPointer
finit SimpleExpr
a0
      dom1 :: Maybe PointerDomain
dom1 = p -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain p
bin FInit SValue SPointer
finit SimpleExpr
a1 in
    (Bool -> Maybe PointerDomain -> Maybe PointerDomain -> Bool
separate_domains Bool
True Maybe PointerDomain
dom0 Maybe PointerDomain
dom1, Bool -> Maybe PointerDomain -> Maybe PointerDomain -> Bool
separate_domains Bool
False Maybe PointerDomain
dom0 Maybe PointerDomain
dom1)
 where
  separate_domains :: Bool -> Maybe PointerDomain -> Maybe PointerDomain -> Bool
separate_domains Bool
True (Just (Domain_Bases NESet PointerBase
bs0)) (Just (Domain_Bases NESet PointerBase
bs1)) = 
    ((PointerBase, PointerBase) -> Bool)
-> [(PointerBase, PointerBase)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((PointerBase -> PointerBase -> Bool)
-> (PointerBase, PointerBase) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((PointerBase -> PointerBase -> Bool)
 -> (PointerBase, PointerBase) -> Bool)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase, PointerBase)
-> Bool
forall a b. (a -> b) -> a -> b
$ p
-> FInit SValue SPointer
-> Bool
-> PointerBase
-> PointerBase
-> Bool
forall {p} {v} {p}.
p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit SValue SPointer
finit Bool
True) [(PointerBase
b0,PointerBase
b1) | PointerBase
b0 <- NESet PointerBase -> [PointerBase]
forall {a}. NESet a -> [a]
neSetToList NESet PointerBase
bs0, PointerBase
b1 <- NESet PointerBase -> [PointerBase]
forall {a}. NESet a -> [a]
neSetToList NESet PointerBase
bs1]
  separate_domains Bool
False (Just (Domain_Bases NESet PointerBase
bs0)) (Just (Domain_Bases NESet PointerBase
bs1)) = 
    NESet PointerBase -> NESet PointerBase -> Bool
forall a. Ord a => NESet a -> NESet a -> Bool
NES.disjoint NESet PointerBase
bs0 NESet PointerBase
bs1 Bool -> Bool -> Bool
&& ((PointerBase, PointerBase) -> Bool)
-> [(PointerBase, PointerBase)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((PointerBase -> PointerBase -> Bool)
-> (PointerBase, PointerBase) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((PointerBase -> PointerBase -> Bool)
 -> (PointerBase, PointerBase) -> Bool)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase, PointerBase)
-> Bool
forall a b. (a -> b) -> a -> b
$ p
-> FInit SValue SPointer
-> Bool
-> PointerBase
-> PointerBase
-> Bool
forall {p} {v} {p}.
p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit SValue SPointer
finit Bool
False) [(PointerBase
b0,PointerBase
b1) | PointerBase
b0 <- NESet PointerBase -> [PointerBase]
forall {a}. NESet a -> [a]
neSetToList NESet PointerBase
bs0, PointerBase
b1 <- NESet PointerBase -> [PointerBase]
forall {a}. NESet a -> [a]
neSetToList NESet PointerBase
bs1]

  separate_domains Bool
necc Maybe PointerDomain
dom0 Maybe PointerDomain
dom1 =
    let srcs0 :: Set BotSrc
srcs0 = Maybe PointerDomain -> SimpleExpr -> Set BotSrc
sources_of_domain Maybe PointerDomain
dom0 SimpleExpr
a0
        srcs1 :: Set BotSrc
srcs1 = Maybe PointerDomain -> SimpleExpr -> Set BotSrc
sources_of_domain Maybe PointerDomain
dom1 SimpleExpr
a1 in
      if Bool
necc then
        ((BotSrc, BotSrc) -> Bool) -> [(BotSrc, BotSrc)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool)
-> (BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool
forall a b. (a -> b) -> a -> b
$ p -> FInit SValue SPointer -> Bool -> BotSrc -> BotSrc -> Bool
forall {p} {v}.
p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate p
bin FInit SValue SPointer
finit Bool
necc) [(BotSrc
src0,BotSrc
src1) | BotSrc
src0 <- Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs0, BotSrc
src1 <- Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs1]
      else
        p
-> FInit SValue SPointer
-> Bool
-> Set BotSrc
-> Set BotSrc
-> Bool
forall {p} {v}.
p -> FInit v SPointer -> Bool -> Set BotSrc -> Set BotSrc -> Bool
source_sets_separate p
bin FInit SValue SPointer
finit Bool
necc Set BotSrc
srcs0 Set BotSrc
srcs1

  sources_of_domain :: Maybe PointerDomain -> SimpleExpr -> Set BotSrc
sources_of_domain (Just (Domain_Sources NESet BotSrc
srcs)) SimpleExpr
_ = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet NESet BotSrc
srcs
  sources_of_domain Maybe PointerDomain
_ SimpleExpr
a                            = p -> SimpleExpr -> Set BotSrc
forall {t}. BinaryClass t => t -> SimpleExpr -> Set BotSrc
srcs_of_expr p
bin SimpleExpr
a




-- * Pointer bases
--
-- | Two pointerbases are separate if they refer to completely different parts of the memory.
-- We assume Stackframe, Global address space, and Heap are separate.
-- Two different @malloc@'s point to different regions.
pointer_bases_separate :: p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
StackPointer           PointerBase
StackPointer            = Bool
False
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
StackPointer           (GlobalAddress Word64
_)       = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
StackPointer           (Malloc Maybe Word64
_ Maybe String
_)            = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
StackPointer           PointerBase
ThreadLocalStorage      = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
StackPointer           (BaseIsStatePart StatePart
_)     = Bool
True

pointer_bases_separate p
bin FInit v SPointer
finit p
necc (GlobalAddress Word64
_)      PointerBase
StackPointer        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (GlobalAddress Word64
a0)     (GlobalAddress Word64
a1)  = if Word64
a1 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
a0 then Word64
a1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
a0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
8 else Word64
a0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
a1 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
8 -- if necc then False else pointers_from_different_global_section bin a0 a1
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (GlobalAddress Word64
_)      (Malloc Maybe Word64
_ Maybe String
_)        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (GlobalAddress Word64
_)      PointerBase
ThreadLocalStorage  = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (GlobalAddress Word64
_)      (BaseIsStatePart StatePart
_) = Bool
True -- TODO add to finit whether pointer is global

pointer_bases_separate p
bin FInit v SPointer
finit p
necc (Malloc Maybe Word64
id0 Maybe String
hash0)     (Malloc Maybe Word64
id1 Maybe String
hash1)  = Maybe Word64
forall a. Maybe a
Nothing Maybe Word64 -> [Maybe Word64] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Maybe Word64
id0,Maybe Word64
id1] Bool -> Bool -> Bool
&& Maybe String
forall a. Maybe a
Nothing Maybe String -> [Maybe String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Maybe String
hash0,Maybe String
hash1] Bool -> Bool -> Bool
&& (Maybe Word64
id0,Maybe String
hash0) (Maybe Word64, Maybe String)
-> (Maybe Word64, Maybe String) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Maybe Word64
id1,Maybe String
hash1)
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (Malloc Maybe Word64
_ Maybe String
_)           PointerBase
_                   = Bool
True

pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
ThreadLocalStorage     PointerBase
StackPointer        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
ThreadLocalStorage     (GlobalAddress Word64
_)   = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
ThreadLocalStorage     (Malloc Maybe Word64
_ Maybe String
_)        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
ThreadLocalStorage     PointerBase
ThreadLocalStorage  = Bool
False
pointer_bases_separate p
bin FInit v SPointer
finit p
necc PointerBase
ThreadLocalStorage     (BaseIsStatePart StatePart
_) = Bool
True

pointer_bases_separate p
bin FInit v SPointer
finit p
necc (BaseIsStatePart StatePart
sp0)  PointerBase
StackPointer        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (BaseIsStatePart StatePart
sp0)  (GlobalAddress Word64
_)   = Bool
True -- TODO add to finit whether pointer is global
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (BaseIsStatePart StatePart
sp0)  (Malloc Maybe Word64
_ Maybe String
_)        = Bool
True
pointer_bases_separate p
bin FInit v SPointer
finit p
necc (BaseIsStatePart StatePart
sp0)  PointerBase
ThreadLocalStorage  = Bool
True
pointer_bases_separate p
bin (FInit Set (SStatePart SPointer, v)
sps Map (SStatePart SPointer, SStatePart SPointer) MemRelation
m) p
necc (BaseIsStatePart StatePart
sp0)  (BaseIsStatePart StatePart
sp1) = StatePart -> StatePart -> Bool
lookup_mem_rel StatePart
sp0 StatePart
sp1
 where
  lookup_mem_rel :: StatePart -> StatePart -> Bool
lookup_mem_rel StatePart
sp0 StatePart
sp1 =
    case (((SStatePart SPointer, SStatePart SPointer), MemRelation) -> Bool)
-> [((SStatePart SPointer, SStatePart SPointer), MemRelation)]
-> Maybe ((SStatePart SPointer, SStatePart SPointer), MemRelation)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\((SStatePart SPointer
sp0',SStatePart SPointer
sp1'),MemRelation
mem_rel) -> (StatePart -> SStatePart SPointer -> Bool
sp_eq_ssp StatePart
sp0 SStatePart SPointer
sp0' Bool -> Bool -> Bool
&& StatePart -> SStatePart SPointer -> Bool
sp_eq_ssp StatePart
sp1 SStatePart SPointer
sp1') Bool -> Bool -> Bool
|| StatePart -> SStatePart SPointer -> Bool
sp_eq_ssp StatePart
sp0 SStatePart SPointer
sp1' Bool -> Bool -> Bool
&& StatePart -> SStatePart SPointer -> Bool
sp_eq_ssp StatePart
sp1 SStatePart SPointer
sp0') ([((SStatePart SPointer, SStatePart SPointer), MemRelation)]
 -> Maybe ((SStatePart SPointer, SStatePart SPointer), MemRelation))
-> [((SStatePart SPointer, SStatePart SPointer), MemRelation)]
-> Maybe ((SStatePart SPointer, SStatePart SPointer), MemRelation)
forall a b. (a -> b) -> a -> b
$ Map (SStatePart SPointer, SStatePart SPointer) MemRelation
-> [((SStatePart SPointer, SStatePart SPointer), MemRelation)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (SStatePart SPointer, SStatePart SPointer) MemRelation
m of
      Just ((SStatePart SPointer, SStatePart SPointer)
_, MemRelation
Separate) -> Bool
True
      Maybe ((SStatePart SPointer, SStatePart SPointer), MemRelation)
_ -> Bool
False

  sp_eq_ssp :: StatePart -> SStatePart SPointer -> Bool
sp_eq_ssp (SP_Reg Register
r0) (SSP_Reg Register
r1) = Register
r0 Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
== Register
r1
  sp_eq_ssp (SP_Mem SimpleExpr
a0 Int
si0) (SSP_Mem (Ptr_Concrete SimpleExpr
a1) Int
si1) = SimpleExpr
a0SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
==SimpleExpr
a1 Bool -> Bool -> Bool
&& Int
si0Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
si1
  sp_eq_ssp StatePart
_ SStatePart SPointer
_ = Bool
False


pointer_bases_separate_necessarily :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_necessarily p
bin FInit v SPointer
finit = p -> FInit v SPointer -> Bool -> PointerBase -> PointerBase -> Bool
forall {p} {v} {p}.
p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit v SPointer
finit Bool
True
pointer_bases_separate_possibly :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_possibly    p
bin FInit v SPointer
finit = p -> FInit v SPointer -> Bool -> PointerBase -> PointerBase -> Bool
forall {p} {v} {p}.
p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit v SPointer
finit Bool
False




-- | Returns true iff the two given expressions have global pointerbases in different segments/sections of the binary.
-- We do not assume that such pointers are separate, but do assert it.
pointers_from_different_global_section :: bin -> a -> a -> Bool
pointers_from_different_global_section bin
ctxt a
a0 a
a1 = bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address bin
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a0) Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address bin
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a1)



-- * Pointer sources
srcs_of_expr :: t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt (Bottom BotTyp
typ)                 = t -> BotTyp -> Set BotSrc
srcs_of_bottyp t
ctxt BotTyp
typ
srcs_of_expr t
ctxt (SE_Malloc Maybe Word64
id Maybe String
h)             = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> BotSrc
Src_Malloc Maybe Word64
id Maybe String
h
srcs_of_expr t
ctxt (SE_Var StatePart
sp)                  = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ StatePart -> BotSrc
Src_Var StatePart
sp
srcs_of_expr t
ctxt (SE_Op Operator
_ Int
_ [SimpleExpr]
es)               = Set (Set BotSrc) -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set BotSrc) -> Set BotSrc) -> Set (Set BotSrc) -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> Set SimpleExpr -> Set (Set BotSrc)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt) (Set SimpleExpr -> Set (Set BotSrc))
-> Set SimpleExpr -> Set (Set BotSrc)
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr]
es
srcs_of_expr t
ctxt (SE_Bit Int
i SimpleExpr
e)                 = t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt SimpleExpr
e
srcs_of_expr t
ctxt (SE_SExtend Int
_ Int
_ SimpleExpr
e)           = t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt SimpleExpr
e
srcs_of_expr t
ctxt (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b)         = Set (Set BotSrc) -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set BotSrc) -> Set BotSrc) -> Set (Set BotSrc) -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> Set SimpleExpr -> Set (Set BotSrc)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt) (Set SimpleExpr -> Set (Set BotSrc))
-> Set SimpleExpr -> Set (Set BotSrc)
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr
a,SimpleExpr
b]
srcs_of_expr t
ctxt e :: SimpleExpr
e@(SE_Immediate Word64
i)           
  | t -> Integer -> Bool
forall {a} {a}. (BinaryClass a, Integral a) => a -> a -> Bool
address_has_external_symbol t
ctxt (Integer -> Bool) -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i =
    BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> BotSrc
Src_ImmediateAddress Word64
i
  | Bool
otherwise =
    case t -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address t
ctxt (Word64 -> Maybe (String, String, Word64, Word64, Word64))
-> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i of
      Just (String
_,String
_,Word64
a0,Word64
_,Word64
_) -> BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> BotSrc
Src_ImmediateAddress Word64
a0
      Maybe (String, String, Word64, Word64, Word64)
Nothing  -> Set BotSrc
forall a. Set a
S.empty

-- | Returns the set of sources of the bottom type
srcs_of_bottyp :: t -> BotTyp -> Set BotSrc
srcs_of_bottyp t
ctxt (FromNonDeterminism NESet SimpleExpr
es)        = Set (Set BotSrc) -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set BotSrc) -> Set BotSrc) -> Set (Set BotSrc) -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> Set SimpleExpr -> Set (Set BotSrc)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt) (Set SimpleExpr -> Set (Set BotSrc))
-> Set SimpleExpr -> Set (Set BotSrc)
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es
srcs_of_bottyp t
ctxt (FromPointerBases NESet PointerBase
bs)          = Set (Set BotSrc) -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set BotSrc) -> Set BotSrc) -> Set (Set BotSrc) -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (PointerBase -> Set BotSrc) -> Set PointerBase -> Set (Set BotSrc)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (t -> PointerBase -> Set BotSrc
srcs_of_base t
ctxt) (Set PointerBase -> Set (Set BotSrc))
-> Set PointerBase -> Set (Set BotSrc)
forall a b. (a -> b) -> a -> b
$ NESet PointerBase -> Set PointerBase
forall a. NESet a -> Set a
NES.toSet NESet PointerBase
bs
srcs_of_bottyp t
ctxt (FromSources NESet BotSrc
srcs)             = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromBitMode NESet BotSrc
srcs)             = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromOverlap NESet BotSrc
srcs)             = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromSemantics NESet BotSrc
srcs)           = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromMemWrite NESet BotSrc
srcs)            = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromUninitializedMemory NESet BotSrc
srcs) = NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet (NESet BotSrc -> Set BotSrc) -> NESet BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc
srcs
srcs_of_bottyp t
ctxt (FromCall String
f)                   = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ String -> BotSrc
Src_Function String
f


-- | Returns the set of sources of the pointerbase
srcs_of_base :: t -> PointerBase -> Set BotSrc
srcs_of_base t
ctxt PointerBase
StackPointer            = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ BotSrc
Src_StackPointer
srcs_of_base t
ctxt (Malloc Maybe Word64
id Maybe String
h)           = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> BotSrc
Src_Malloc Maybe Word64
id Maybe String
h
srcs_of_base t
ctxt (GlobalAddress Word64
a)       = t -> SimpleExpr -> Set BotSrc
srcs_of_expr t
ctxt (SimpleExpr -> Set BotSrc) -> SimpleExpr -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
a
srcs_of_base t
ctxt PointerBase
ThreadLocalStorage      = BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ StatePart -> BotSrc
Src_Var (StatePart -> BotSrc) -> StatePart -> BotSrc
forall a b. (a -> b) -> a -> b
$ Register -> StatePart
SP_Reg (SReg -> Register
RegSeg SReg
FS)







source_sets_separate :: p -> FInit v SPointer -> Bool -> Set BotSrc -> Set BotSrc -> Bool
source_sets_separate p
bin FInit v SPointer
finit Bool
necc Set BotSrc
srcs0 Set BotSrc
srcs1 = 
 Bool -> Bool
not (Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs0)
 Bool -> Bool -> Bool
&&
 Bool -> Bool
not (Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs1)
 Bool -> Bool -> Bool
&&
   (
     (Set BotSrc -> Set BotSrc -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.disjoint Set BotSrc
srcs0 Set BotSrc
srcs1 Bool -> Bool -> Bool
&& ((BotSrc, BotSrc) -> Bool) -> [(BotSrc, BotSrc)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool)
-> (BotSrc -> BotSrc -> Bool) -> (BotSrc, BotSrc) -> Bool
forall a b. (a -> b) -> a -> b
$ p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
forall {p} {v}.
p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate p
bin FInit v SPointer
finit Bool
necc) [(BotSrc
src0,BotSrc
src1) | BotSrc
src0 <- Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs0, BotSrc
src1 <- Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs1])
 --  ||
 --    (not (S.null ms0) && not (S.null ms1) && all (\src0 -> all (\src1 -> sources_separate ctxt necc src0 src1) ms1) ms0)
   )


-- | Two sources are inputs for separate pointers if, e.g., one of them is the stackpointer and the other a malloc-return-value.
sources_separate :: p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate p
bin FInit v SPointer
finit Bool
necc (Src_Function String
f0) (Src_Function String
f1) = Bool -> Bool
not Bool
necc Bool -> Bool -> Bool
&& String
f0 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
f1
sources_separate p
bin FInit v SPointer
finit Bool
necc (Src_Function String
f0) BotSrc
_                 = Bool -> Bool
not Bool
necc 
sources_separate p
bin FInit v SPointer
finit Bool
necc BotSrc
_                 (Src_Function String
f1) = Bool -> Bool
not Bool
necc 
sources_separate p
bin FInit v SPointer
finit Bool
necc BotSrc
src0 BotSrc
src1
  | Bool
otherwise =
      case (BotSrc -> Maybe PointerBase
src_to_base BotSrc
src0, BotSrc -> Maybe PointerBase
src_to_base BotSrc
src1) of
        (Just PointerBase
b0,Just PointerBase
b1)           -> p -> FInit v SPointer -> Bool -> PointerBase -> PointerBase -> Bool
forall {p} {v} {p}.
p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
pointer_bases_separate p
bin FInit v SPointer
finit Bool
necc PointerBase
b0 PointerBase
b1
        (Just PointerBase
StackPointer, Maybe PointerBase
_)      -> Bool -> Bool
not Bool
necc
        (Maybe PointerBase
_, Just PointerBase
StackPointer)      -> Bool -> Bool
not Bool
necc
        (Just (Malloc Maybe Word64
_ Maybe String
_), Maybe PointerBase
_)      -> Bool
True
        (Maybe PointerBase
_, Just (Malloc Maybe Word64
_ Maybe String
_))      -> Bool
True
        (Just PointerBase
ThreadLocalStorage,Maybe PointerBase
_) -> Bool -> Bool
not Bool
necc
        (Maybe PointerBase
_,Just PointerBase
ThreadLocalStorage) -> Bool -> Bool
not Bool
necc
        (Maybe PointerBase, Maybe PointerBase)
_                           -> if Bool
necc then Bool
False else BotSrc
src0 BotSrc -> BotSrc -> Bool
forall a. Eq a => a -> a -> Bool
/= BotSrc
src1 -- TODO use finit
 where
  src_to_base :: BotSrc -> Maybe PointerBase
src_to_base (BotSrc
Src_StackPointer)       = PointerBase -> Maybe PointerBase
forall a. a -> Maybe a
Just (PointerBase -> Maybe PointerBase)
-> PointerBase -> Maybe PointerBase
forall a b. (a -> b) -> a -> b
$ PointerBase
StackPointer
  src_to_base (Src_Malloc Maybe Word64
i Maybe String
h)         = PointerBase -> Maybe PointerBase
forall a. a -> Maybe a
Just (PointerBase -> Maybe PointerBase)
-> PointerBase -> Maybe PointerBase
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> PointerBase
Malloc Maybe Word64
i Maybe String
h
  src_to_base (Src_ImmediateAddress Word64
a) = PointerBase -> Maybe PointerBase
forall a. a -> Maybe a
Just (PointerBase -> Maybe PointerBase)
-> PointerBase -> Maybe PointerBase
forall a b. (a -> b) -> a -> b
$ Word64 -> PointerBase
GlobalAddress Word64
a
  src_to_base (Src_Var (SP_Reg (RegSeg SReg
FS)))    = PointerBase -> Maybe PointerBase
forall a. a -> Maybe a
Just (PointerBase -> Maybe PointerBase)
-> PointerBase -> Maybe PointerBase
forall a b. (a -> b) -> a -> b
$ PointerBase
ThreadLocalStorage
  src_to_base BotSrc
_                        = Maybe PointerBase
forall a. Maybe a
Nothing

sources_separate_necessarily :: p -> FInit v SPointer -> BotSrc -> BotSrc -> Bool
sources_separate_necessarily p
bin FInit v SPointer
finit = p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
forall {p} {v}.
p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate p
bin FInit v SPointer
finit Bool
True
sources_separate_possibly :: p -> FInit v SPointer -> BotSrc -> BotSrc -> Bool
sources_separate_possibly    p
bin FInit v SPointer
finit = p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
forall {p} {v}.
p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate p
bin FInit v SPointer
finit Bool
False