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

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

import Base
import Config

import Data.SymbolicExpression

import Analysis.Context
import Analysis.FunctionNames

import X86.Register

import Generic.Binary

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.List
import Data.Word 
import Data.Maybe
import Debug.Trace



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


-- | Returns true if the expression has a local pointerbase
expr_is_highly_likely_local_pointer :: FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer FContext
ctxt SimpleExpr
e = FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall t. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` FContext -> Bool -> PointerDomain -> Bool
is_local_pointer_domain FContext
ctxt Bool
True
expr_is_maybe_local_pointer :: FContext -> SimpleExpr -> Bool
expr_is_maybe_local_pointer         FContext
ctxt SimpleExpr
e = FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall t. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` FContext -> Bool -> PointerDomain -> Bool
is_local_pointer_domain FContext
ctxt Bool
False

-- | Returns true iff the give domain is highly likelty local to the current function
is_local_pointer_domain :: FContext -> Bool -> PointerDomain -> Bool
is_local_pointer_domain FContext
ctxt 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 (StackPointer String
f)     = String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Context -> Int -> String
function_name_of_entry (FContext -> Context
f_ctxt FContext
ctxt) (FContext -> Int
f_entry FContext
ctxt)
  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 FContext
ctxt 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 (Src_StackPointer String
f)  = String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Context -> Int -> String
function_name_of_entry (FContext -> Context
f_ctxt FContext
ctxt) (FContext -> Int
f_entry FContext
ctxt)
  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 if the expression has known pointerbases.
expr_highly_likely_pointer :: FContext -> SimpleExpr -> Bool
expr_highly_likely_pointer FContext
fctxt SimpleExpr
e = FContext -> SimpleExpr -> Maybe (NESet PointerBase)
get_pointer_bases FContext
fctxt SimpleExpr
e Maybe (NESet PointerBase) -> Maybe (NESet PointerBase) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (NESet PointerBase)
forall a. Maybe a
Nothing


-- | Returns true if the expression has a heap pointerbase
expr_is_highly_likely_heap_pointer :: FContext -> SimpleExpr -> Bool
expr_is_highly_likely_heap_pointer FContext
ctxt SimpleExpr
e = FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e Maybe PointerDomain -> (PointerDomain -> Bool) -> Bool
forall t. Maybe t -> (t -> Bool) -> Bool
`existsAndSatisfies` FContext -> PointerDomain -> Bool
forall p. p -> PointerDomain -> Bool
is_heap_pointer_domain FContext
ctxt

is_heap_pointer_domain :: p -> PointerDomain -> Bool
is_heap_pointer_domain p
ctxt (Domain_Bases NESet PointerBase
bs) = (PointerBase -> Bool) -> NESet PointerBase -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PointerBase -> Bool
is_heap_base NESet PointerBase
bs
 where
  is_heap_base :: PointerBase -> Bool
is_heap_base (Malloc Maybe Word64
id Maybe String
hash)     = Bool
True
  is_heap_base PointerBase
_                    = Bool
False
is_heap_pointer_domain p
ctxt (Domain_Sources NESet BotSrc
srcs) = (BotSrc -> Bool) -> NESet BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all BotSrc -> Bool
is_heap_source NESet BotSrc
srcs
 where
  is_heap_source :: BotSrc -> Bool
is_heap_source (Src_Malloc Maybe Word64
id Maybe String
hash) = Bool
True
  is_heap_source BotSrc
_                    = Bool
False






-- | Returns true iff the given symbolic regions are necessarily separate.
-- TODO: add VCS, not necc
necessarily_separate :: FContext
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate FContext
fctxt 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 a.
(Ord a, Num a) =>
SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate_expressions SimpleExpr
a0 Word64
si0' SimpleExpr
a1 Word64
si1' Bool -> Bool -> Bool
|| FContext -> String -> SimpleExpr -> SimpleExpr -> Bool
necessarily_separate_no_size FContext
fctxt String
msg SimpleExpr
a0 SimpleExpr
a1 
    (SimpleExpr, SimpleExpr)
_ -> FContext -> String -> SimpleExpr -> SimpleExpr -> Bool
necessarily_separate_no_size FContext
fctxt String
msg SimpleExpr
a0 SimpleExpr
a1
necessarily_separate FContext
fctxt String
msg SimpleExpr
a0 Maybe SimpleExpr
_ SimpleExpr
a1 Maybe SimpleExpr
_ = FContext -> String -> SimpleExpr -> SimpleExpr -> Bool
necessarily_separate_no_size FContext
fctxt String
msg SimpleExpr
a0 SimpleExpr
a1 

necessarily_separate_no_size :: FContext -> String -> SimpleExpr -> SimpleExpr -> Bool
necessarily_separate_no_size FContext
fctxt 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
$ FContext -> SimpleExpr -> SimpleExpr -> (Bool, Bool)
separate_pointer_domains FContext
fctxt 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
a0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
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 -> a -> SimpleExpr -> a -> Bool
necessarily_separate_expressions SimpleExpr
a0 a
si0 SimpleExpr
a1 a
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,a
si0) (SimpleExpr, a) -> (SimpleExpr, a) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SimpleExpr
a1,a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 Bool -> Bool -> Bool
|| Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> a
forall a. Num a => a -> a -> a
- a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Bool -> Bool -> Bool
|| Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 a -> a -> a
forall a. Num a => a -> a -> a
- a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 Bool -> Bool -> Bool
|| Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
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 -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
a0 a
si0 SimpleExpr
a1 a
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
_ [SE_Var StatePart
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Minus Int
_ [SE_Var StatePart
v1, SE_Immediate Word64
i1]) = 
    StatePart
v0 StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== StatePart
v1 Bool -> Bool -> Bool
&& 
      if a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
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 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> a
forall a. Num a => a -> a -> a
- a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 a -> a -> a
forall a. Num a => a -> a -> a
- a
si1
      else if a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> a
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 a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 then
        Bool
False
      else if a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 Bool -> Bool -> Bool
&& a
si1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> Word64 -> a
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
&& a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
si0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
i0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
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
_ [SE_Var StatePart
v0, SE_Immediate Word64
i0])
      (SE_Op Operator
Plus Int
_ [SE_Var StatePart
v1, SE_Immediate Word64
i1]) = 
    StatePart
v0 StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== StatePart
v1 Bool -> Bool -> Bool
&& Word64
i0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
i1 Bool -> Bool -> Bool
&& Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si1
  -- v0 + i0 enc v0 <==> i0 + si0 <= si1
  enc (SE_Op Operator
Plus Int
_ [SE_Var StatePart
v0, SE_Immediate Word64
i0])
      (SE_Var StatePart
v1) =
    StatePart
v0 StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== StatePart
v1 Bool -> Bool -> Bool
&& Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
si1
  -- immediates
  enc (SE_Immediate Word64
a0) (SE_Immediate Word64
a1) = 
    Word64
a0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
a1 Bool -> Bool -> Bool
&& Word64
a0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
si0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
a1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
si1
  enc SimpleExpr
_ SimpleExpr
_ = 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.
--
-- Retrieves the pointer bases from a symbolic expression.
-- They are either 1.) all known, or 2.) all unknown.
get_pointer_domain ::
  FContext               -- ^ The current context
  -> SimpleExpr          -- ^ A symbolic expression 
  -> Maybe PointerDomain -- ^ A pointer domain
get_pointer_domain :: FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e =
  let bs :: Set PointerBase
bs  = SimpleExpr -> Set PointerBase
get_pointer_bases 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
      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 :: NESet BotSrc
srcs = FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e in
      --if NES.size srcs <= 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
srcs
      --else
      --  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_bases :: SimpleExpr -> S.Set PointerBase
  get_pointer_bases :: SimpleExpr -> Set PointerBase
get_pointer_bases (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 SimpleExpr -> Set PointerBase
get_pointer_bases (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_bases (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 SimpleExpr -> Set PointerBase
get_pointer_bases (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_bases (SE_Op Operator
Minus Int
_ (SimpleExpr
e:[SimpleExpr]
es))           = SimpleExpr -> Set PointerBase
get_pointer_bases SimpleExpr
e
  get_pointer_bases SimpleExpr
e                                = SimpleExpr -> Set PointerBase
get_pointer_base SimpleExpr
e


  get_pointer_base :: SimpleExpr -> S.Set PointerBase
  get_pointer_base :: SimpleExpr -> Set PointerBase
get_pointer_base (SE_Immediate Word64
a)                     = if Context -> SimpleExpr -> Bool
expr_is_global_immediate (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
e then 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 else Set PointerBase
forall a. Set a
S.empty
  get_pointer_base (SE_Var (SP_StackPointer String
f))         = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ String -> PointerBase
StackPointer String
f
  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) (Context -> IntMap Symbol
ctxt_symbol_table (Context -> IntMap Symbol) -> Context -> IntMap Symbol
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt) of
                                                            Just (Relocated_Function String
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 -> String -> PointerBase
PointerToSymbol Word64
a String
sym
                                                            Just (Relocated_Label String
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 -> String -> PointerBase
PointerToSymbol Word64
a String
sym
                                                            Maybe Symbol
_ -> Set PointerBase
forall a. Set a
S.empty
  statepart_to_pointerbase (SP_Reg Register
FS)                  = PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton PointerBase
ThreadLocalStorage
  statepart_to_pointerbase StatePart
_                            = Set PointerBase
forall a. Set a
S.empty




-- | Returns true iff the two given expressions can be shown to be separate based on their domains.
separate_pointer_domains :: FContext -> SimpleExpr -> SimpleExpr -> (Bool, Bool)
separate_pointer_domains FContext
ctxt SimpleExpr
a0 SimpleExpr
a1 =
  let dom0 :: Maybe PointerDomain
dom0 = FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
a0
      dom1 :: Maybe PointerDomain
dom1 = FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt 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
$ FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt 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
$ FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt 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 :: NESet BotSrc
srcs0 = Maybe PointerDomain -> SimpleExpr -> NESet BotSrc
sources_of_domain Maybe PointerDomain
dom0 SimpleExpr
a0
        srcs1 :: NESet BotSrc
srcs1 = Maybe PointerDomain -> SimpleExpr -> NESet 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
$ FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate FContext
ctxt Bool
necc) [(BotSrc
src0,BotSrc
src1) | BotSrc
src0 <- NESet BotSrc -> [BotSrc]
forall a. NESet a -> [a]
neSetToList NESet BotSrc
srcs0, BotSrc
src1 <- NESet BotSrc -> [BotSrc]
forall a. NESet a -> [a]
neSetToList NESet BotSrc
srcs1]
      else
        FContext -> Bool -> NESet BotSrc -> NESet BotSrc -> Bool
source_sets_separate FContext
ctxt Bool
necc NESet BotSrc
srcs0 NESet BotSrc
srcs1

  sources_of_domain :: Maybe PointerDomain -> SimpleExpr -> NESet BotSrc
sources_of_domain (Just (Domain_Sources NESet BotSrc
srcs)) SimpleExpr
_ = NESet BotSrc
srcs
  sources_of_domain Maybe PointerDomain
_ SimpleExpr
a                            = FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt 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 :: FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt Bool
necc (StackPointer String
f)           (StackPointer String
f')         = if Bool
necc then Bool
False else String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
f'
pointer_bases_separate FContext
ctxt Bool
necc (StackPointer String
f)           (GlobalAddress Word64
_)         = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (StackPointer String
f)           (PointerToSymbol Word64
_ String
_)     = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (StackPointer String
f)           (Malloc Maybe Word64
_ Maybe String
_)              = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (StackPointer String
f)           PointerBase
ThreadLocalStorage        = Bool
True

pointer_bases_separate FContext
ctxt Bool
necc (GlobalAddress Word64
_)          (StackPointer String
f)          = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (GlobalAddress Word64
_)          (PointerToSymbol Word64
_ String
_)     = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (GlobalAddress Word64
a0)         (GlobalAddress Word64
a1)        = if Bool
necc then Bool
False else Context -> Word64 -> Word64 -> Bool
forall a a. (Integral a, Integral a) => Context -> a -> a -> Bool
pointers_from_different_global_section (FContext -> Context
f_ctxt FContext
ctxt) Word64
a0 Word64
a1
pointer_bases_separate FContext
ctxt Bool
necc (GlobalAddress Word64
_)          (Malloc Maybe Word64
_ Maybe String
_)              = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (GlobalAddress Word64
_)          PointerBase
ThreadLocalStorage        = Bool
True

pointer_bases_separate FContext
ctxt Bool
necc (PointerToSymbol Word64
_ String
_)      (StackPointer String
f)          = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (PointerToSymbol Word64
_ String
_)      (GlobalAddress Word64
_)         = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (PointerToSymbol Word64
_ String
sym0)   (PointerToSymbol Word64
_ String
sym1)  = String
sym0 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
sym1
pointer_bases_separate FContext
ctxt Bool
necc (PointerToSymbol Word64
_ String
sym0)   (Malloc Maybe Word64
_ Maybe String
_)              = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc (PointerToSymbol Word64
_ String
sym0)   PointerBase
ThreadLocalStorage        = Bool
True

pointer_bases_separate FContext
ctxt Bool
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 FContext
ctxt Bool
necc (Malloc Maybe Word64
_ Maybe String
_)               PointerBase
_                         = Bool
True

pointer_bases_separate FContext
ctxt Bool
necc PointerBase
ThreadLocalStorage         (StackPointer String
f')         = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc PointerBase
ThreadLocalStorage         (GlobalAddress Word64
_)         = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc PointerBase
ThreadLocalStorage         (PointerToSymbol Word64
_ String
_)     = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc PointerBase
ThreadLocalStorage         (Malloc Maybe Word64
_ Maybe String
_)              = Bool
True
pointer_bases_separate FContext
ctxt Bool
necc PointerBase
ThreadLocalStorage         PointerBase
ThreadLocalStorage        = Bool
False

pointer_bases_separate_necessarily :: FContext -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_necessarily FContext
ctxt = FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt Bool
True
pointer_bases_separate_possibly :: FContext -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_possibly    FContext
ctxt = FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt 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 :: Context -> a -> a -> Bool
pointers_from_different_global_section Context
ctxt a
a0 a
a1 = Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_for_address Context
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a0) Maybe (String, String, Word64, Word64)
-> Maybe (String, String, Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_for_address Context
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a1)



-- | returns the set of bases of a domain, if any
bases_of_domain :: PointerDomain -> Maybe (NES.NESet PointerBase)
bases_of_domain :: PointerDomain -> Maybe (NESet PointerBase)
bases_of_domain (Domain_Bases NESet PointerBase
bs) = NESet PointerBase -> Maybe (NESet PointerBase)
forall a. a -> Maybe a
Just NESet PointerBase
bs
bases_of_domain PointerDomain
_                 = Maybe (NESet PointerBase)
forall a. Maybe a
Nothing

-- | Returns the set of pointer bases, if any
get_pointer_bases :: FContext -> SimpleExpr -> Maybe (NESet PointerBase)
get_pointer_bases FContext
ctxt SimpleExpr
e =
  case FContext -> SimpleExpr -> Maybe PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e of
    Maybe PointerDomain
Nothing -> Maybe (NESet PointerBase)
forall a. Maybe a
Nothing
    Just PointerDomain
d  -> PointerDomain -> Maybe (NESet PointerBase)
bases_of_domain PointerDomain
d




-- * Pointer sources
srcs_of_expr :: FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt (Bottom BotTyp
typ)                 = FContext -> BotTyp -> NESet BotSrc
srcs_of_bottyp FContext
ctxt BotTyp
typ
srcs_of_expr FContext
ctxt (SE_Malloc Maybe Word64
id Maybe String
h)             = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> BotSrc
Src_Malloc Maybe Word64
id Maybe String
h
srcs_of_expr FContext
ctxt (SE_Var (SP_StackPointer String
f)) = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ String -> BotSrc
Src_StackPointer String
f
srcs_of_expr FContext
ctxt (SE_Var StatePart
sp)                  = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ StatePart -> BotSrc
Src_Var StatePart
sp
--srcs_of_expr ctxt (SE_StatePart sp)            = S.empty 
srcs_of_expr FContext
ctxt (SE_Op Operator
_ Int
_ [SimpleExpr]
es)               = NESet (NESet BotSrc) -> NESet BotSrc
forall (f :: * -> *) a.
(Foldable1 f, Ord a) =>
f (NESet a) -> NESet a
NES.unions (NESet (NESet BotSrc) -> NESet BotSrc)
-> NESet (NESet BotSrc) -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> NESet BotSrc)
-> NESet SimpleExpr -> NESet (NESet BotSrc)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt) (NESet SimpleExpr -> NESet (NESet BotSrc))
-> NESet SimpleExpr -> NESet (NESet BotSrc)
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> NESet SimpleExpr
forall a. Set a -> NESet a
NES.unsafeFromSet (Set SimpleExpr -> NESet SimpleExpr)
-> Set SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr]
es
srcs_of_expr FContext
ctxt (SE_Bit Int
i SimpleExpr
e)                 = FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e
srcs_of_expr FContext
ctxt (SE_SExtend Int
_ Int
_ SimpleExpr
e)           = FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e
srcs_of_expr FContext
ctxt (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b)         = NESet (NESet BotSrc) -> NESet BotSrc
forall (f :: * -> *) a.
(Foldable1 f, Ord a) =>
f (NESet a) -> NESet a
NES.unions (NESet (NESet BotSrc) -> NESet BotSrc)
-> NESet (NESet BotSrc) -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> NESet BotSrc)
-> NESet SimpleExpr -> NESet (NESet BotSrc)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt) (NESet SimpleExpr -> NESet (NESet BotSrc))
-> NESet SimpleExpr -> NESet (NESet BotSrc)
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> NESet SimpleExpr
forall a. Set a -> NESet a
NES.unsafeFromSet (Set SimpleExpr -> NESet SimpleExpr)
-> Set SimpleExpr -> NESet SimpleExpr
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 FContext
ctxt e :: SimpleExpr
e@(SE_Immediate Word64
i)           = 
  if Context -> Integer -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_external_symbol (FContext -> Context
f_ctxt FContext
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 then
    BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> BotSrc
Src_ImmediateAddress Word64
i
  else case Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_for_address (FContext -> Context
f_ctxt FContext
ctxt) (Word64 -> Maybe (String, String, Word64, Word64))
-> Word64 -> Maybe (String, String, 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
_) -> BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> BotSrc
Src_ImmediateAddress Word64
a0
    Maybe (String, String, Word64, Word64)
Nothing  -> BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ BotSrc
Src_ImmediateConstants

-- | Returns the set of sources of the bottom type
srcs_of_bottyp :: FContext -> BotTyp -> NESet BotSrc
srcs_of_bottyp FContext
ctxt (FromNonDeterminism NESet SimpleExpr
es)        = NESet (NESet BotSrc) -> NESet BotSrc
forall (f :: * -> *) a.
(Foldable1 f, Ord a) =>
f (NESet a) -> NESet a
NES.unions (NESet (NESet BotSrc) -> NESet BotSrc)
-> NESet (NESet BotSrc) -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> NESet BotSrc)
-> NESet SimpleExpr -> NESet (NESet BotSrc)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt) NESet SimpleExpr
es
srcs_of_bottyp FContext
ctxt (FromPointerBases NESet PointerBase
bs)          = NESet (NESet BotSrc) -> NESet BotSrc
forall (f :: * -> *) a.
(Foldable1 f, Ord a) =>
f (NESet a) -> NESet a
NES.unions (NESet (NESet BotSrc) -> NESet BotSrc)
-> NESet (NESet BotSrc) -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ (PointerBase -> NESet BotSrc)
-> NESet PointerBase -> NESet (NESet BotSrc)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> PointerBase -> NESet BotSrc
srcs_of_base FContext
ctxt) NESet PointerBase
bs
srcs_of_bottyp FContext
ctxt (FromSources NESet BotSrc
srcs)             = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromBitMode NESet BotSrc
srcs)             = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromOverlap NESet BotSrc
srcs)             = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromSemantics NESet BotSrc
srcs)           = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromMemWrite NESet BotSrc
srcs)            = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromUninitializedMemory NESet BotSrc
srcs) = NESet BotSrc
srcs
srcs_of_bottyp FContext
ctxt (FromCall String
f)                   = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet 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 :: FContext -> PointerBase -> NESet BotSrc
srcs_of_base FContext
ctxt (StackPointer String
f)        = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ String -> BotSrc
Src_StackPointer String
f
srcs_of_base FContext
ctxt (Malloc Maybe Word64
id Maybe String
h)           = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> BotSrc
Src_Malloc Maybe Word64
id Maybe String
h
srcs_of_base FContext
ctxt (GlobalAddress Word64
a)       = FContext -> SimpleExpr -> NESet BotSrc
srcs_of_expr FContext
ctxt (SimpleExpr -> NESet BotSrc) -> SimpleExpr -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
a
srcs_of_base FContext
ctxt (PointerToSymbol Word64
a String
sym) = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet BotSrc
forall a b. (a -> b) -> a -> b
$ StatePart -> BotSrc
Src_Var (StatePart -> BotSrc) -> StatePart -> BotSrc
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8
srcs_of_base FContext
ctxt PointerBase
ThreadLocalStorage      = BotSrc -> NESet BotSrc
forall a. a -> NESet a
NES.singleton (BotSrc -> NESet BotSrc) -> BotSrc -> NESet 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 Register
FS




is_src_mem :: BotSrc -> Bool
is_src_mem (Src_Mem NESet BotSrc
srcs) = Bool
True
is_src_mem BotSrc
_              = Bool
False

source_sets_separate :: FContext -> Bool -> NESet BotSrc -> NESet BotSrc -> Bool
source_sets_separate FContext
ctxt Bool
necc NESet BotSrc
srcs0 NESet BotSrc
srcs1 = 
 let srcs0' :: Set BotSrc
srcs0' = BotSrc -> Set BotSrc -> Set BotSrc
forall a. Ord a => a -> Set a -> Set a
S.delete BotSrc
Src_ImmediateConstants (Set BotSrc -> Set BotSrc) -> Set BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet NESet BotSrc
srcs0
     srcs1' :: Set BotSrc
srcs1' = BotSrc -> Set BotSrc -> Set BotSrc
forall a. Ord a => a -> Set a -> Set a
S.delete BotSrc
Src_ImmediateConstants (Set BotSrc -> Set BotSrc) -> Set BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> Set BotSrc
forall a. NESet a -> Set a
NES.toSet NESet BotSrc
srcs1
     (Set BotSrc
ms0,Set BotSrc
srcs0'') = (BotSrc -> Bool) -> Set BotSrc -> (Set BotSrc, Set BotSrc)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition BotSrc -> Bool
is_src_mem Set BotSrc
srcs0'
     (Set BotSrc
ms1,Set BotSrc
srcs1'') = (BotSrc -> Bool) -> Set BotSrc -> (Set BotSrc, Set BotSrc)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition BotSrc -> Bool
is_src_mem Set BotSrc
srcs1' in
   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
$ FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate FContext
ctxt 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 :: FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate :: FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate FContext
ctxt Bool
necc (Src_Mem NESet BotSrc
a0s) (Src_Mem NESet BotSrc
a1s)         = FContext -> Bool -> NESet BotSrc -> NESet BotSrc -> Bool
source_sets_separate FContext
ctxt Bool
necc NESet BotSrc
a0s NESet BotSrc
a1s
sources_separate FContext
ctxt 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 FContext
ctxt Bool
necc (Src_Function String
f0) BotSrc
_                 = Bool -> Bool
not Bool
necc 
sources_separate FContext
ctxt Bool
necc BotSrc
_                 (Src_Function String
f1) = Bool -> Bool
not Bool
necc 
sources_separate FContext
ctxt Bool
necc BotSrc
src0 BotSrc
src1
  | BotSrc
src0 BotSrc -> BotSrc -> Bool
forall a. Eq a => a -> a -> Bool
== BotSrc
Src_ImmediateConstants Bool -> Bool -> Bool
|| BotSrc
src1 BotSrc -> BotSrc -> Bool
forall a. Eq a => a -> a -> Bool
== BotSrc
Src_ImmediateConstants = Bool
True
  | 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)           -> FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate FContext
ctxt Bool
necc PointerBase
b0 PointerBase
b1
        (Just (StackPointer String
_), Maybe PointerBase
_)  -> Bool -> Bool
not Bool
necc
        (Maybe PointerBase
_, Just (StackPointer String
_))  -> 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)
_                           -> Bool
False -- if necc then False else src0 /= src1 -- TODO
 where
  src_to_base :: BotSrc -> Maybe PointerBase
src_to_base (Src_StackPointer String
f)     = PointerBase -> Maybe PointerBase
forall a. a -> Maybe a
Just (PointerBase -> Maybe PointerBase)
-> PointerBase -> Maybe PointerBase
forall a b. (a -> b) -> a -> b
$ String -> PointerBase
StackPointer String
f
  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 Register
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 :: FContext -> BotSrc -> BotSrc -> Bool
sources_separate_necessarily FContext
ctxt = FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate FContext
ctxt Bool
True
sources_separate_possibly :: FContext -> BotSrc -> BotSrc -> Bool
sources_separate_possibly    FContext
ctxt = FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate FContext
ctxt Bool
False