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

{-|
Module      : Pointers
Description : Functions for dealing with symbolic pointers and abstraction.
-}
module Data.Pointers (
   FContext (..),
   mk_fcontext,
   get_pointer_domain,
   expr_highly_likely_pointer,
   expr_is_global_pointer,
   expr_is_highly_likely_local_pointer,
   expr_is_global_immediate,
   srcs_of_expr,
   srcs_of_exprs,
   is_known_source,
   join_exprs,
   join_single,
   separate_pointer_domains,
   pointer_bases_separate_necessarily,
   pointer_bases_separate_possibly,
   sources_separate_necessarily,
   sources_separate_possibly,
   necessarily_equal,
   necessarily_equal_stateparts,
   necessarily_separate,
   necessarily_separate_stateparts,
   necessarily_enclosed,
   unfold_non_determinism,
   trim_expr
  )
  where

import Analysis.Context
import Data.Binary
import Base
import Config
import Data.ControlFlow
import Data.SimplePred

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


-- | The context augmented with information on the current function
data FContext = FContext {
  FContext -> Context
f_ctxt  :: Context,   -- ^ The context
  FContext -> Int
f_entry :: Int,       -- ^ The entry address of the current function
  FContext -> String
f_name  :: String,    -- ^ The name of the current function
  FContext -> FInit
f_init  :: FInit      -- ^ The initialization of the current function
 }

mk_fcontext :: Context -> Int -> FContext
mk_fcontext :: Context -> Int -> FContext
mk_fcontext Context
ctxt Int
entry =
  let f :: String
f     = Context -> Int -> String
function_name_of_entry Context
ctxt Int
entry
      finit :: Maybe FInit
finit = Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt
      fctxt :: FContext
fctxt = Context -> Int -> String -> FInit -> FContext
FContext Context
ctxt Int
entry String
f (Maybe FInit
finit Maybe FInit -> FInit -> FInit
forall p. Maybe p -> p -> p
`orElse` FInit
forall k a. Map k a
M.empty) in
    FContext
fctxt



statepart_to_finit_expr :: FContext -> StatePart -> Maybe SimpleExpr
statepart_to_finit_expr :: FContext -> StatePart -> Maybe SimpleExpr
statepart_to_finit_expr FContext
ctxt StatePart
sp = StatePart -> FInit -> Maybe SimpleExpr
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup StatePart
sp (FInit -> Maybe SimpleExpr) -> FInit -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ FContext -> FInit
f_init FContext
ctxt

 
-- * 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 
  -> PointerDomain     -- ^ A pointer domain
get_pointer_domain :: FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e =
  let bs :: Set PointerBase
bs  = Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
True (SimpleExpr -> Set PointerBase) -> SimpleExpr -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp SimpleExpr
e in
    if Bool -> Bool
not (Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs) Bool -> Bool -> Bool
&& Set PointerBase -> Int
forall a. Set a -> Int
S.size Set PointerBase
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_bases then
      Set PointerBase -> PointerDomain
Domain_Bases Set PointerBase
bs
    else let srcs :: Set BotSrc
srcs = FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt 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
get_max_num_of_sources then
        Set BotSrc -> PointerDomain
Domain_Sources Set BotSrc
srcs
      else
        Set BotSrc -> PointerDomain
Domain_Sources (Set BotSrc -> PointerDomain) -> Set BotSrc -> PointerDomain
forall a b. (a -> b) -> a -> b
$ Set BotSrc
forall a. Set a
S.empty

 where
  get_max_num_of_bases :: Int
get_max_num_of_bases   = Context -> Int
ctxt_max_num_of_bases (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt
  get_max_num_of_sources :: Int
get_max_num_of_sources = Context -> Int
ctxt_max_num_of_sources (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt


  get_pointer_bases' :: Bool -> SimpleExpr -> S.Set PointerBase
  get_pointer_bases' :: Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
use_finit (Bottom (FromNonDeterminism Set 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 (Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
use_finit) Set SimpleExpr
es -- TODO non-empty union?
  get_pointer_bases' Bool
use_finit (SE_Op (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 (Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
use_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_bases' Bool
use_finit (SE_Op (Minus Int
_) (SimpleExpr
e:[SimpleExpr]
es))         = Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
use_finit SimpleExpr
e
  get_pointer_bases' Bool
use_finit SimpleExpr
e                                = Bool -> SimpleExpr -> Set PointerBase
get_pointer_base Bool
use_finit SimpleExpr
e


  get_pointer_base :: Bool -> SimpleExpr -> S.Set PointerBase
  get_pointer_base :: Bool -> SimpleExpr -> Set PointerBase
get_pointer_base Bool
use_finit (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 Bool
use_finit (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 Bool
True      (SE_Var StatePart
sp)                          = (Bool -> SimpleExpr -> Set PointerBase
get_pointer_bases' Bool
False (SimpleExpr -> Set PointerBase)
-> Maybe SimpleExpr -> Maybe (Set PointerBase)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> StatePart -> Maybe SimpleExpr
statepart_to_finit_expr FContext
ctxt StatePart
sp) Maybe (Set PointerBase) -> Set PointerBase -> Set PointerBase
forall p. Maybe p -> p -> p
`orElse` (StatePart -> Set PointerBase
statepart_to_pointerbase StatePart
sp)
  get_pointer_base Bool
False     (SE_Var StatePart
sp)                          = (StatePart -> Set PointerBase
statepart_to_pointerbase StatePart
sp)
  get_pointer_base Bool
use_finit (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 Bool
use_finit (Bottom (FromPointerBases Set PointerBase
bs))       = if Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs then Set PointerBase
forall a. Set a
S.empty else Set PointerBase
bs
  get_pointer_base Bool
use_finit 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 String -> Maybe String
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 String
ctxt_syms (Context -> IntMap String) -> Context -> IntMap String
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt) of
                                                            Maybe String
Nothing  -> Set PointerBase
forall a. Set a
S.empty
                                                            Just 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
  statepart_to_pointerbase StatePart
_                            = Set PointerBase
forall a. Set a
S.empty


-- | returns the set of bases of a domain, if any
bases_of_domain :: PointerDomain -> Maybe (S.Set PointerBase)
bases_of_domain :: PointerDomain -> Maybe (Set PointerBase)
bases_of_domain (Domain_Bases Set PointerBase
bs) = if 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
bs then Set PointerBase -> Maybe (Set PointerBase)
forall a. a -> Maybe a
Just Set PointerBase
bs else Maybe (Set PointerBase)
forall a. Maybe a
Nothing
bases_of_domain PointerDomain
_                 = Maybe (Set PointerBase)
forall a. Maybe a
Nothing

-- | Returns the set of pointer bases, if any
get_pointer_bases :: FContext -> SimpleExpr -> Maybe (Set PointerBase)
get_pointer_bases FContext
ctxt SimpleExpr
e = PointerDomain -> Maybe (Set PointerBase)
bases_of_domain (PointerDomain -> Maybe (Set PointerBase))
-> PointerDomain -> Maybe (Set PointerBase)
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e

-- | Returns true if the expression has known pointerbases.
expr_highly_likely_pointer :: FContext -> SimpleExpr -> Bool
expr_highly_likely_pointer FContext
ctxt SimpleExpr
e = FContext -> SimpleExpr -> Maybe (Set PointerBase)
get_pointer_bases FContext
ctxt SimpleExpr
e Maybe (Set PointerBase) -> Maybe (Set PointerBase) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (Set PointerBase)
forall a. Maybe a
Nothing

-- | Returns the set of global pointerbases, or the empty set if none.
get_global_pointer_bases :: FContext -> SimpleExpr -> Set PointerBase
get_global_pointer_bases FContext
ctxt SimpleExpr
e = ((PointerBase -> Bool) -> Set PointerBase -> Set PointerBase
forall a. (a -> Bool) -> Set a -> Set a
S.filter PointerBase -> Bool
is_global_ptr_base (Set PointerBase -> Set PointerBase)
-> Maybe (Set PointerBase) -> Maybe (Set PointerBase)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> SimpleExpr -> Maybe (Set PointerBase)
get_pointer_bases FContext
ctxt SimpleExpr
e) Maybe (Set PointerBase) -> Set PointerBase -> Set PointerBase
forall p. Maybe p -> p -> p
`orElse` Set PointerBase
forall a. Set a
S.empty

-- | Returns true if the expression has a global pointerbase.
expr_is_global_pointer :: FContext -> SimpleExpr -> Bool
expr_is_global_pointer FContext
ctxt 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
$ FContext -> SimpleExpr -> Set PointerBase
get_global_pointer_bases FContext
ctxt SimpleExpr
e

-- | 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) = if Context -> Word64 -> Bool
is_roughly_an_address Context
ctxt (Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) then Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_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 else Bool
False
expr_is_global_immediate Context
ctxt SimpleExpr
_                = Bool
False

-- | Returns true if the expression has a local pointerbase, and no others.
expr_is_highly_likely_local_pointer :: FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer FContext
ctxt SimpleExpr
e = FContext -> PointerDomain -> Bool
is_highly_likely_local_pointer_domain FContext
ctxt (PointerDomain -> Bool) -> PointerDomain -> Bool
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
e

-- | Returns true iff the give domain is highly likelty local to the current function
is_highly_likely_local_pointer_domain :: FContext -> PointerDomain -> Bool
is_highly_likely_local_pointer_domain FContext
ctxt (Domain_Bases Set PointerBase
bs)     = Bool -> Bool
not (Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs) Bool -> Bool -> Bool
&& (PointerBase -> Bool) -> Set PointerBase -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PointerBase -> Bool
is_local_base Set 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
== FContext -> String
f_name FContext
ctxt
  is_local_base PointerBase
_                    = Bool
False
is_highly_likely_local_pointer_domain FContext
ctxt (Domain_Sources Set BotSrc
srcs) = Bool -> Bool
not (Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs) Bool -> Bool -> Bool
&& (BotSrc -> Bool) -> Set BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all BotSrc -> Bool
is_local_src Set 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
== FContext -> String
f_name FContext
ctxt
  is_local_src BotSrc
_                     = Bool
False





is_global_ptr_base :: PointerBase -> Bool
is_global_ptr_base (GlobalAddress Word64
_) = Bool
True
is_global_ptr_base PointerBase
_                 = Bool
False

is_malloc :: PointerBase -> Bool
is_malloc (Malloc Maybe Word64
_ Maybe String
_) = Bool
True
is_malloc PointerBase
_            = Bool
False




-- * Sources

-- | Returns the set of sources (inputs used to compute the expression) of an expression.
srcs_of_expr :: FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e = FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
True SimpleExpr
e {--
  let srcs       = srcs_of_expr' ctxt True e
      known_srcs = S.filter is_known_source srcs in
   if S.null known_srcs then srcs else known_srcs
--}

is_known_source :: BotSrc -> Bool
is_known_source (Src_StackPointer String
_)     = Bool
True
is_known_source (Src_Malloc Maybe Word64
_ Maybe String
_)         = Bool
True
is_known_source (Src_ImmediateAddress Word64
_) = Bool
True
is_known_source BotSrc
_                        = Bool
False

-- | Returns the set of sources (state parts used to compute the expression) of two expressions.
srcs_of_exprs :: FContext -> [SimpleExpr] -> Set BotSrc
srcs_of_exprs FContext
ctxt [SimpleExpr]
es = [Set BotSrc] -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set BotSrc] -> Set BotSrc) -> [Set BotSrc] -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> [SimpleExpr] -> [Set BotSrc]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
True) [SimpleExpr]
es 
-- | returns the set of sources of a domain, if any
sources_of_domain :: FContext -> PointerDomain -> S.Set BotSrc 
sources_of_domain :: FContext -> PointerDomain -> Set BotSrc
sources_of_domain FContext
ctxt (Domain_Bases Set 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 (FContext -> Bool -> PointerBase -> Set BotSrc
forall p p. p -> p -> PointerBase -> Set BotSrc
srcs_of_base FContext
ctxt Bool
True) Set PointerBase
bs
sources_of_domain FContext
ctxt (Domain_Sources Set BotSrc
srcs) = Set BotSrc
srcs





srcs_of_expr' :: FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit (Bottom BotTyp
typ)                 = FContext -> Bool -> BotTyp -> Set BotSrc
srcs_of_bottyp FContext
ctxt Bool
use_finit BotTyp
typ
srcs_of_expr' FContext
ctxt Bool
use_finit (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' FContext
ctxt Bool
use_finit (SE_Var (SP_StackPointer 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_StackPointer String
f
srcs_of_expr' FContext
ctxt Bool
True      (SE_Var StatePart
sp)                  = (FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
False (SimpleExpr -> Set BotSrc)
-> Maybe SimpleExpr -> Maybe (Set BotSrc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> StatePart -> Maybe SimpleExpr
statepart_to_finit_expr FContext
ctxt StatePart
sp) Maybe (Set BotSrc) -> Set BotSrc -> Set BotSrc
forall p. Maybe p -> p -> p
`orElse` (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' FContext
ctxt Bool
False     (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' FContext
ctxt Bool
use_finit e :: SimpleExpr
e@(SE_Immediate Word64
i)           = if Context -> SimpleExpr -> Bool
expr_is_global_immediate (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
e then 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 else Set BotSrc
forall a. Set a
S.empty
srcs_of_expr' FContext
ctxt Bool
use_finit (SE_StatePart StatePart
sp)            = Set BotSrc
forall a. Set a
S.empty 
srcs_of_expr' FContext
ctxt Bool
use_finit (SE_Op Operator
_ [SimpleExpr]
es)                 = [Set BotSrc] -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set BotSrc] -> Set BotSrc) -> [Set BotSrc] -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> [SimpleExpr] -> [Set BotSrc]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit) [SimpleExpr]
es
srcs_of_expr' FContext
ctxt Bool
use_finit (SE_Bit Int
i SimpleExpr
e)                 = FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit SimpleExpr
e
srcs_of_expr' FContext
ctxt Bool
use_finit (SE_SExtend Int
_ Int
_ SimpleExpr
e)           = FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit SimpleExpr
e
srcs_of_expr' FContext
ctxt Bool
use_finit (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b)         = [Set BotSrc] -> Set BotSrc
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set BotSrc] -> Set BotSrc) -> [Set BotSrc] -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set BotSrc) -> [SimpleExpr] -> [Set BotSrc]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit) [SimpleExpr
a,SimpleExpr
b]


-- | Returns the set of sources of the bottom type
srcs_of_bottyp :: FContext -> Bool -> BotTyp -> Set BotSrc
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromNonDeterminism Set 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 (FContext -> Bool -> SimpleExpr -> Set BotSrc
srcs_of_expr' FContext
ctxt Bool
use_finit) Set SimpleExpr
es
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromPointerBases Set 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 (FContext -> Bool -> PointerBase -> Set BotSrc
forall p p. p -> p -> PointerBase -> Set BotSrc
srcs_of_base FContext
ctxt Bool
use_finit) Set PointerBase
bs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromSources Set BotSrc
srcs)             = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromBitMode Set BotSrc
srcs)             = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromOverlap Set BotSrc
srcs)             = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromSemantics Set BotSrc
srcs)           = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromMemWrite Set BotSrc
srcs)            = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (FromUninitializedMemory Set BotSrc
srcs) = Set BotSrc
srcs
srcs_of_bottyp FContext
ctxt Bool
use_finit (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 :: p -> p -> PointerBase -> Set BotSrc
srcs_of_base p
ctxt p
use_finit (StackPointer 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_StackPointer String
f
srcs_of_base p
ctxt p
use_finit (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 p
ctxt p
use_finit (GlobalAddress Word64
a)       = 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
a
srcs_of_base p
ctxt p
use_finit (PointerToSymbol Word64
a String
sym) = 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
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8





-- * Joining


-- | Given a set of expressions, produce an expression that resembles the join of the entire set.
-- That is, the produced expression should be coarser than the disjunction of all input-expressions.
--
--   (1) First, just use non-determinism, i.e., @a join b@ becomes @{a,b}@. This is precise, but doesn't guarantee termination.
--   (2) If step 1 produces too many cases, join based on known pointerbases. This requires all given expressions to have known pointerbases.
--   (3) If step 2 produces too many bases, or the given expressions have no known pointerbases, join bsed on sources.
--   (4) If step 3 produces too many sources, just produces 'rock_bottom'.
--
--
-- TODO: joining immediates
join_exprs' :: String -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs' :: String -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs' String
msg FContext
ctxt [SimpleExpr]
es = 
  let es' :: Set SimpleExpr
es' = (SimpleExpr -> SimpleExpr) -> Set SimpleExpr -> Set SimpleExpr
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> SimpleExpr
simp (Set SimpleExpr -> Set SimpleExpr)
-> Set SimpleExpr -> Set SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Set SimpleExpr] -> Set SimpleExpr
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set SimpleExpr] -> Set SimpleExpr)
-> [Set SimpleExpr] -> Set SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set SimpleExpr) -> [SimpleExpr] -> [Set SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList ([SimpleExpr] -> Set SimpleExpr)
-> (SimpleExpr -> [SimpleExpr]) -> SimpleExpr -> Set SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt) [SimpleExpr]
es in
    if Set SimpleExpr -> Int
forall a. Set a -> Int
S.size Set SimpleExpr
es' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
      SimpleExpr
rock_bottom
    else if Set SimpleExpr -> Int
forall a. Set a -> Int
S.size Set SimpleExpr
es' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
      [SimpleExpr] -> SimpleExpr
forall a. [a] -> a
head ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList Set SimpleExpr
es'  
    else if Set SimpleExpr -> Int
forall a. Set a -> Int
S.size Set SimpleExpr
es' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_cases Bool -> Bool -> Bool
&& (SimpleExpr -> Bool) -> Set SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> Bool
contains_bot) Set SimpleExpr
es' then
      BotTyp -> SimpleExpr
Bottom (Set SimpleExpr -> BotTyp
FromNonDeterminism Set SimpleExpr
es')
    else if SimpleExpr
rock_bottom SimpleExpr -> Set SimpleExpr -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set SimpleExpr
es' then
      SimpleExpr
rock_bottom
    else let bss :: Set (Set PointerBase)
bss = (SimpleExpr -> Set PointerBase)
-> Set SimpleExpr -> Set (Set PointerBase)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Maybe (Set PointerBase) -> Set PointerBase
forall a. Maybe (Set a) -> Set a
nothing_to_empty (Maybe (Set PointerBase) -> Set PointerBase)
-> (SimpleExpr -> Maybe (Set PointerBase))
-> SimpleExpr
-> Set PointerBase
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> SimpleExpr -> Maybe (Set PointerBase)
get_pointer_bases FContext
ctxt) Set SimpleExpr
es'
             bs :: Set PointerBase
bs  = Set (Set PointerBase) -> Set PointerBase
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions Set (Set PointerBase)
bss in
      if Set PointerBase -> Int
forall a. Set a -> Int
S.size Set PointerBase
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_bases Bool -> Bool -> Bool
&& (Set PointerBase -> Bool) -> Set (Set PointerBase) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool)
-> (Set PointerBase -> Bool) -> Set PointerBase -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set PointerBase -> Bool
forall a. Set a -> Bool
S.null) Set (Set PointerBase)
bss then
        BotTyp -> SimpleExpr
Bottom (Set PointerBase -> BotTyp
FromPointerBases Set PointerBase
bs)
      else
        let srcs :: Set BotSrc
srcs = 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 (FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt) Set SimpleExpr
es' in
          if Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_sources then
            BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromSources Set BotSrc
srcs)
          else
            {--trace ("Hitting max num of sources: " ++ show get_max_num_of_sources)--} SimpleExpr
rock_bottom
 where
  get_max_num_of_cases :: Int
get_max_num_of_cases   = Context -> Int
ctxt_max_num_of_cases (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt
  get_max_num_of_bases :: Int
get_max_num_of_bases   = Context -> Int
ctxt_max_num_of_bases (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt
  get_max_num_of_sources :: Int
get_max_num_of_sources = Context -> Int
ctxt_max_num_of_sources (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt

  nothing_to_empty :: Maybe (Set a) -> Set a
nothing_to_empty Maybe (Set a)
Nothing   = Set a
forall a. Set a
S.empty
  nothing_to_empty (Just Set a
bs) = Set a
bs

join_exprs :: String -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs String
msg FContext
ctxt [SimpleExpr]
es = 
  let e :: SimpleExpr
e = String -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs' String
msg FContext
ctxt [SimpleExpr]
es in
    SimpleExpr
e
--    if expr_is_possibly_local_pointer ctxt e && any (not . expr_is_possibly_local_pointer ctxt) es then traceShow ("joining: ",msg,es,e) e else e
--    if S.size (srcs_of_expr e) == 0 && all (\e -> S.size (srcs_of_expr e) > 0) es && es /= [] then traceShow ("joining: ",es,e, S.size $ srcs_of_exprs es) e else e 
--    if all (\e' -> S.size (srcs_of_expr ctxt e') < S.size (srcs_of_expr ctxt e)) es && es /= [] then traceShow ("joining: ",msg,es,e, S.size $ srcs_of_exprs ctxt es) e else e 


-- | Abstraction for a single expression, even if the expression is concrete.
join_single :: FContext -> SimpleExpr -> SimpleExpr
join_single :: FContext -> SimpleExpr -> SimpleExpr
join_single FContext
ctxt SimpleExpr
e =
  case FContext -> SimpleExpr -> Maybe (Set PointerBase)
get_pointer_bases FContext
ctxt SimpleExpr
e of
    Maybe (Set PointerBase)
Nothing -> SimpleExpr
join_sources
    Just Set PointerBase
bs -> if Bool -> Bool
not (Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs) Bool -> Bool -> Bool
&& Set PointerBase -> Int
forall a. Set a -> Int
S.size Set PointerBase
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_bases then BotTyp -> SimpleExpr
Bottom (Set PointerBase -> BotTyp
FromPointerBases Set PointerBase
bs) else SimpleExpr
join_sources
 where
  get_max_num_of_bases :: Int
get_max_num_of_bases   = Context -> Int
ctxt_max_num_of_bases (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt
  get_max_num_of_sources :: Int
get_max_num_of_sources = Context -> Int
ctxt_max_num_of_sources (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt

  join_sources :: SimpleExpr
join_sources =
    let srcs :: Set BotSrc
srcs = FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e in 
      if Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
get_max_num_of_sources then
        BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromSources Set BotSrc
srcs)
      else
        {--trace ("Hitting max num of sources: " ++ show get_max_num_of_sources) --} SimpleExpr
rock_bottom



-- * Separation


-- | 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)



domains_separate :: FContext -> Bool -> PointerDomain -> PointerDomain -> Bool
domains_separate FContext
ctxt Bool
necc (Domain_Bases Set PointerBase
bs0) (Domain_Bases Set PointerBase
bs1) = 
  if Bool
necc then
    ((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
necc) [(PointerBase
b0,PointerBase
b1) | PointerBase
b0 <- Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs0, PointerBase
b1 <- Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs1]
  else
    Set PointerBase -> Set PointerBase -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.disjoint Set PointerBase
bs0 Set 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
necc) [(PointerBase
b0,PointerBase
b1) | PointerBase
b0 <- Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs0, PointerBase
b1 <- Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs1]
domains_separate FContext
ctxt Bool
necc PointerDomain
dom0 PointerDomain
dom1 =
  let srcs0 :: Set BotSrc
srcs0 = FContext -> PointerDomain -> Set BotSrc
sources_of_domain FContext
ctxt PointerDomain
dom0
      srcs1 :: Set BotSrc
srcs1 = FContext -> PointerDomain -> Set BotSrc
sources_of_domain FContext
ctxt PointerDomain
dom1 in
    if Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs0 Bool -> Bool -> Bool
|| Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs1 then
      Bool
False
    else 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 <- 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
      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]




-- | 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 (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 (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 (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_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

-- | 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 BotSrc
src0 BotSrc
src1 =
  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
    (Maybe PointerBase, Maybe PointerBase)
_                          -> Bool
False
 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 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



-- | Returns true iff the two given expressions can be shown to be separate.
separate_pointer_domains :: FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
necc SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1 =
  if Bool -> Bool
not Bool
necc Bool -> Bool -> Bool
&& Bool
possibly_separate_globals then
    Bool
True
  else
    let dom0 :: PointerDomain
dom0 = FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
a0
        dom1 :: PointerDomain
dom1 = FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
a1 in
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [
        FContext -> Bool -> PointerDomain -> PointerDomain -> Bool
domains_separate FContext
ctxt Bool
necc PointerDomain
dom0 PointerDomain
dom1,
        SimpleExpr -> Bool
is_immediate SimpleExpr
a0 Bool -> Bool -> Bool
&& FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer FContext
ctxt SimpleExpr
a1,
        SimpleExpr -> Bool
is_immediate SimpleExpr
a1 Bool -> Bool -> Bool
&& FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer FContext
ctxt SimpleExpr
a0
       ]
 where
  possibly_separate_globals :: Bool
possibly_separate_globals =
    case (SimpleExpr
a0,SimpleExpr
a1) of
      (SE_Immediate Word64
imm0,SimpleExpr
_) -> if Context -> SimpleExpr -> Bool
expr_is_global_immediate (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
a0 then Word64 -> a -> Set BotSrc -> Bool
forall a. Integral a => Word64 -> a -> Set BotSrc -> Bool
below Word64
imm0 a
si0 ((BotSrc -> Bool) -> Set BotSrc -> Set BotSrc
forall a. (a -> Bool) -> Set a -> Set a
S.filter BotSrc -> Bool
is_global_src (Set BotSrc -> Set BotSrc) -> Set BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
a1) else Bool
False
      (SimpleExpr
_,SE_Immediate Word64
imm1) -> if Context -> SimpleExpr -> Bool
expr_is_global_immediate (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
a1 then Word64 -> a -> Set BotSrc -> Bool
forall a. Integral a => Word64 -> a -> Set BotSrc -> Bool
below Word64
imm1 a
si1 ((BotSrc -> Bool) -> Set BotSrc -> Set BotSrc
forall a. (a -> Bool) -> Set a -> Set a
S.filter BotSrc -> Bool
is_global_src (Set BotSrc -> Set BotSrc) -> Set BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
a0) else Bool
False
      (SimpleExpr, SimpleExpr)
_                     -> Bool
False

  below :: Word64 -> a -> Set BotSrc -> Bool
below Word64
imm a
si Set BotSrc
srcs = (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs) Bool -> Bool -> Bool
&& (BotSrc -> Bool) -> Set BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Src_ImmediateAddress Word64
imm') -> Word64
imm Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
si Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
imm') Set BotSrc
srcs

  is_global_src :: BotSrc -> Bool
is_global_src (Src_ImmediateAddress Word64
_) = Bool
True
  is_global_src BotSrc
_                        = 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 (Minus Int
_) [SE_Var StatePart
v0, SE_Immediate Word64
i0])
      (SE_Op (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 (Plus Int
_) [SE_Var StatePart
v0, SE_Immediate Word64
i0])
      (SE_Op (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 (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


-- | 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 :: FContext -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate FContext
ctxt SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1 =
  if Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1) then
    (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
  else
    FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1
 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 || v0 - i1 + si1 <= v0 - i0 <==> i0-si0 >= i1 || i1-si1 >= i0
  sep (SE_Op (Minus Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op (Minus Int
_) [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1


  -- v0 - i0 |x| v0 + i1 <==> True
  sep (SE_Op (Minus Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op (Plus  Int
_) [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      Bool
True
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1
  sep (SE_Op (Plus  Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op (Minus Int
_) [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      Bool
True
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1


  -- v0 - i0 |x| v0 <==> i0 >= si0
  sep (SE_Op (Minus Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
       SimpleExpr
v1 = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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 
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1
  sep SimpleExpr
v0
      (SE_Op (Minus Int
_) [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 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 (Plus Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
      (SE_Op (Plus Int
_) [SimpleExpr
v1, SE_Immediate Word64
i1]) = 
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1 


  -- v0 + i0 |x| v0 <==> i0 >= si1
  sep (SE_Op (Plus Int
_) [SimpleExpr
v0, SE_Immediate Word64
i0])
      SimpleExpr
v1 =
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1 
  sep SimpleExpr
v1
      (SE_Op (Plus Int
_) [SimpleExpr
v0,SE_Immediate Word64
i0]) =
    if SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
v0 SimpleExpr
v1 then
      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
    else
      FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1 

  -- remainder
  sep SimpleExpr
a0 SimpleExpr
a1 = FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
forall a a.
(Integral a, Integral a) =>
FContext -> Bool -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
separate_pointer_domains FContext
ctxt Bool
True SimpleExpr
a0 a
si0 SimpleExpr
a1 a
si1


-- | Returns true iff the given symbolic stateparts are necessarily separate.
necessarily_separate_stateparts :: FContext -> StatePart -> StatePart -> Bool
necessarily_separate_stateparts FContext
ctxt (SP_Reg Register
r0)     (SP_Reg Register
r1)     = Register
r0 Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
/= Register
r1
necessarily_separate_stateparts FContext
ctxt (SP_Mem SimpleExpr
a0 Int
si0) (SP_Mem SimpleExpr
a1 Int
si1) = FContext -> SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a.
Integral a =>
FContext -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate FContext
ctxt SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
necessarily_separate_stateparts FContext
_    StatePart
_               StatePart
_               = Bool
True




-- | Returns true iff the given symbolic regions are necessarily equal.
-- For example:
--    @[RSP-16,4]@ is enclosed in @[RSP-16,4]@
--
-- Will return @False@ if the expressions contain bottom.
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 stateparts are necessarily equal.
necessarily_equal_stateparts :: StatePart -> StatePart -> Bool
necessarily_equal_stateparts (SP_Reg Register
r0) (SP_Reg Register
r1) = Register
r0 Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
== Register
r1
necessarily_equal_stateparts (SP_Mem SimpleExpr
a0 Int
si0) (SP_Mem SimpleExpr
a1 Int
si1) = Int
si0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si1 Bool -> Bool -> Bool
&& SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
a0 SimpleExpr
a1
necessarily_equal_stateparts StatePart
_ StatePart
_ = Bool
False







-- crossProduct [[1], [2,3,4], [5,6]] == [[1,2,5],[1,3,5],[1,4,5],[1,2,6],[1,3,6],[1,4,6]]
-- The size of a crossProduct [x_0,x_1,x_i] is the number of produced lists |x_0|*|x_1|*...*|x_i| times the size of each list i.
crossProduct :: [[a]] -> [[a]]
crossProduct :: [[a]] -> [[a]]
crossProduct []       = [[]]
crossProduct ([a]
as:[[a]]
ass) = [ a
ba -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
bs | a
b <- [a]
as, [a]
bs <- [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
crossProduct [[a]]
ass ]

crossProduct_size :: [t a] -> Int
crossProduct_size [t a]
x = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([t a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t a]
x Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (t a -> Int) -> [t a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t a]
x) 

-- | Unfold an expression with non-determinisism to a list of expressions.
-- Keep an eye on the produced size, as this may cause blow-up.
unfold_non_determinism :: FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism :: FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt (Bottom (FromNonDeterminism Set SimpleExpr
es)) = Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList Set SimpleExpr
es
unfold_non_determinism FContext
ctxt (SE_Op Operator
op [SimpleExpr]
es)                    = 
  let es' :: [[SimpleExpr]]
es' = (SimpleExpr -> [SimpleExpr]) -> [SimpleExpr] -> [[SimpleExpr]]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt) [SimpleExpr]
es in
    if [[SimpleExpr]] -> Int
forall (t :: * -> *) a. Foldable t => [t a] -> Int
crossProduct_size [[SimpleExpr]]
es' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Context -> Int
ctxt_max_expr_size (FContext -> Context
f_ctxt FContext
ctxt) then [SimpleExpr
rock_bottom] else ([SimpleExpr] -> SimpleExpr) -> [[SimpleExpr]] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Operator -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
op) ([[SimpleExpr]] -> [SimpleExpr]) -> [[SimpleExpr]] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ [[SimpleExpr]] -> [[SimpleExpr]]
forall a. [[a]] -> [[a]]
crossProduct [[SimpleExpr]]
es'
unfold_non_determinism FContext
ctxt (SE_Bit Int
b SimpleExpr
e)                     = (SimpleExpr -> SimpleExpr) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
b) ([SimpleExpr] -> [SimpleExpr]) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt) SimpleExpr
e
unfold_non_determinism FContext
ctxt (SE_SExtend Int
l Int
h SimpleExpr
e)               = (SimpleExpr -> SimpleExpr) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h) ([SimpleExpr] -> [SimpleExpr]) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt) SimpleExpr
e
unfold_non_determinism FContext
ctxt (SE_Overwrite Int
l SimpleExpr
a SimpleExpr
b)             = 
  let as :: [SimpleExpr]
as = FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt SimpleExpr
a
      bs :: [SimpleExpr]
bs = FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt SimpleExpr
b in
    if [[SimpleExpr]] -> Int
forall (t :: * -> *) a. Foldable t => [t a] -> Int
crossProduct_size [[SimpleExpr]
as,[SimpleExpr]
bs] Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Context -> Int
ctxt_max_expr_size (FContext -> Context
f_ctxt FContext
ctxt) then [SimpleExpr
rock_bottom] else [ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
l SimpleExpr
a' SimpleExpr
b' | SimpleExpr
a' <- [SimpleExpr]
as, SimpleExpr
b' <- [SimpleExpr]
bs ]
unfold_non_determinism FContext
ctxt SimpleExpr
e                                = [SimpleExpr
e]



-- | If the size of an expression becomes too large, we simply turn it into Bottom.
trim_expr :: FContext -> SimpleExpr -> SimpleExpr
trim_expr FContext
ctxt SimpleExpr
e =
  if SimpleExpr -> Int
expr_size SimpleExpr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
get_max_expr_size then 
    {--trace ("Hitting expr_size limit of " ++ show get_max_expr_size ++ ".")--} SimpleExpr
rock_bottom -- Bottom (FromSources $ srcs_of_expr e)
  else
    SimpleExpr
e
 where
  get_max_expr_size :: Int
get_max_expr_size = Context -> Int
ctxt_max_expr_size (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt