{-# LANGUAGE DeriveGeneric, DefaultSignatures, StrictData #-}

{-|
Module      : SimplePred
Description : A datatype for symbolic expressions and symbolic predicates.

A datatype for symbolic predicates, tailored to storing information
on equalities between the current values stored in state parts (lhs) 
and constant expressions (rhs).
-}

module Data.SimplePred ( 
  Pred (..),
  StatePart (..),
  SimpleExpr (..),
  FlagStatus (..),
  BotTyp (..),
  BotSrc (..),
  Operator (..),
  PointerBase(..),
  is_immediate,
  is_mem_sp,
  is_reg_sp,
  contains_bot,
  contains_bot_sp,
  all_bot_satisfy,
  simp,
  rock_bottom,
  pp_expr,
  pp_pred,
  expr_size
 )
 where

import Base
import Config
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import Data.Word (Word64,Word32)
import Data.Traversable (for)
import Data.List
import Data.Maybe (mapMaybe,fromJust)
import Debug.Trace
import GHC.Generics
import Data.Bits (testBit, (.|.), (.&.))
import qualified Data.Serialize as Cereal hiding (get,put)
import X86.Register (Register)
import qualified X86.Operand as X86


-- | A pointerbase is a positive addend of a symbolic expression that may represent a pointer.
data PointerBase = 
    StackPointer String                  -- ^ The stack frame of the given function
  | Malloc (Maybe Word64) (Maybe String) -- ^ A malloc (at the /heap/) at a given address (hash is unused for now)
  | GlobalAddress Word64                 -- ^ A /global/ address in the range of the sections of the binary.
  | PointerToSymbol Word64 String        -- ^ An address with an associated symbol.
  deriving ((forall x. PointerBase -> Rep PointerBase x)
-> (forall x. Rep PointerBase x -> PointerBase)
-> Generic PointerBase
forall x. Rep PointerBase x -> PointerBase
forall x. PointerBase -> Rep PointerBase x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PointerBase x -> PointerBase
$cfrom :: forall x. PointerBase -> Rep PointerBase x
Generic,PointerBase -> PointerBase -> Bool
(PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> Bool) -> Eq PointerBase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PointerBase -> PointerBase -> Bool
$c/= :: PointerBase -> PointerBase -> Bool
== :: PointerBase -> PointerBase -> Bool
$c== :: PointerBase -> PointerBase -> Bool
Eq,Eq PointerBase
Eq PointerBase
-> (PointerBase -> PointerBase -> Ordering)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> PointerBase)
-> (PointerBase -> PointerBase -> PointerBase)
-> Ord PointerBase
PointerBase -> PointerBase -> Bool
PointerBase -> PointerBase -> Ordering
PointerBase -> PointerBase -> PointerBase
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PointerBase -> PointerBase -> PointerBase
$cmin :: PointerBase -> PointerBase -> PointerBase
max :: PointerBase -> PointerBase -> PointerBase
$cmax :: PointerBase -> PointerBase -> PointerBase
>= :: PointerBase -> PointerBase -> Bool
$c>= :: PointerBase -> PointerBase -> Bool
> :: PointerBase -> PointerBase -> Bool
$c> :: PointerBase -> PointerBase -> Bool
<= :: PointerBase -> PointerBase -> Bool
$c<= :: PointerBase -> PointerBase -> Bool
< :: PointerBase -> PointerBase -> Bool
$c< :: PointerBase -> PointerBase -> Bool
compare :: PointerBase -> PointerBase -> Ordering
$ccompare :: PointerBase -> PointerBase -> Ordering
$cp1Ord :: Eq PointerBase
Ord)



-- | Bot represents an unknown (bottom) value.
-- We annotate each occurence of Bot with a BotTyp.
-- This type indicates where the bottom value originates from.
-- The latter  six are all equal, we just use them for debugging and information.
-- They indicate that the  value is unknown, but was computed using the set of sources.
data BotTyp = 
    FromNonDeterminism (S.Set SimpleExpr)   -- ^ The expression evaluates to one of the expressions in the set
  | FromPointerBases (S.Set PointerBase)    -- ^ The expression is a pointer-computation with known base(s)
  | FromCall String                         -- ^ Return value of a function call
  | FromSources (S.Set BotSrc)              -- ^ The expression is some computation based on sources.
  | FromOverlap (S.Set BotSrc)              -- ^ A read from two possibly overlapping regions
  | FromMemWrite (S.Set BotSrc)             -- ^ A write to two possibly overlapping regions 
  | FromSemantics (S.Set BotSrc)            -- ^ An instruction with unknown semantics
  | FromBitMode (S.Set BotSrc)              -- ^ Should not happen, but if a register writes to a registeralias with unknown bit size
  | FromUninitializedMemory (S.Set BotSrc)  -- ^ Reading from memory not written to yet
 deriving (BotTyp -> BotTyp -> Bool
(BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> Bool) -> Eq BotTyp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BotTyp -> BotTyp -> Bool
$c/= :: BotTyp -> BotTyp -> Bool
== :: BotTyp -> BotTyp -> Bool
$c== :: BotTyp -> BotTyp -> Bool
Eq, Eq BotTyp
Eq BotTyp
-> (BotTyp -> BotTyp -> Ordering)
-> (BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> BotTyp)
-> (BotTyp -> BotTyp -> BotTyp)
-> Ord BotTyp
BotTyp -> BotTyp -> Bool
BotTyp -> BotTyp -> Ordering
BotTyp -> BotTyp -> BotTyp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BotTyp -> BotTyp -> BotTyp
$cmin :: BotTyp -> BotTyp -> BotTyp
max :: BotTyp -> BotTyp -> BotTyp
$cmax :: BotTyp -> BotTyp -> BotTyp
>= :: BotTyp -> BotTyp -> Bool
$c>= :: BotTyp -> BotTyp -> Bool
> :: BotTyp -> BotTyp -> Bool
$c> :: BotTyp -> BotTyp -> Bool
<= :: BotTyp -> BotTyp -> Bool
$c<= :: BotTyp -> BotTyp -> Bool
< :: BotTyp -> BotTyp -> Bool
$c< :: BotTyp -> BotTyp -> Bool
compare :: BotTyp -> BotTyp -> Ordering
$ccompare :: BotTyp -> BotTyp -> Ordering
$cp1Ord :: Eq BotTyp
Ord, (forall x. BotTyp -> Rep BotTyp x)
-> (forall x. Rep BotTyp x -> BotTyp) -> Generic BotTyp
forall x. Rep BotTyp x -> BotTyp
forall x. BotTyp -> Rep BotTyp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BotTyp x -> BotTyp
$cfrom :: forall x. BotTyp -> Rep BotTyp x
Generic)


-- | Sources that may be used to compute an expression. That is, the inputs to an expression.
data BotSrc = 
    Src_Var StatePart                        -- ^ An initial variable, i.e., a constant
  | Src_StackPointer String                  -- ^ The stack pointer of the given function
  | Src_Malloc (Maybe Word64) (Maybe String) -- ^ A malloced address
  | Src_ImmediateAddress Word64              -- ^ An immediate used in the computation of the pointer
  | Src_Function String                      -- ^ A return value from a function
 deriving (BotSrc -> BotSrc -> Bool
(BotSrc -> BotSrc -> Bool)
-> (BotSrc -> BotSrc -> Bool) -> Eq BotSrc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BotSrc -> BotSrc -> Bool
$c/= :: BotSrc -> BotSrc -> Bool
== :: BotSrc -> BotSrc -> Bool
$c== :: BotSrc -> BotSrc -> Bool
Eq, Eq BotSrc
Eq BotSrc
-> (BotSrc -> BotSrc -> Ordering)
-> (BotSrc -> BotSrc -> Bool)
-> (BotSrc -> BotSrc -> Bool)
-> (BotSrc -> BotSrc -> Bool)
-> (BotSrc -> BotSrc -> Bool)
-> (BotSrc -> BotSrc -> BotSrc)
-> (BotSrc -> BotSrc -> BotSrc)
-> Ord BotSrc
BotSrc -> BotSrc -> Bool
BotSrc -> BotSrc -> Ordering
BotSrc -> BotSrc -> BotSrc
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BotSrc -> BotSrc -> BotSrc
$cmin :: BotSrc -> BotSrc -> BotSrc
max :: BotSrc -> BotSrc -> BotSrc
$cmax :: BotSrc -> BotSrc -> BotSrc
>= :: BotSrc -> BotSrc -> Bool
$c>= :: BotSrc -> BotSrc -> Bool
> :: BotSrc -> BotSrc -> Bool
$c> :: BotSrc -> BotSrc -> Bool
<= :: BotSrc -> BotSrc -> Bool
$c<= :: BotSrc -> BotSrc -> Bool
< :: BotSrc -> BotSrc -> Bool
$c< :: BotSrc -> BotSrc -> Bool
compare :: BotSrc -> BotSrc -> Ordering
$ccompare :: BotSrc -> BotSrc -> Ordering
$cp1Ord :: Eq BotSrc
Ord, (forall x. BotSrc -> Rep BotSrc x)
-> (forall x. Rep BotSrc x -> BotSrc) -> Generic BotSrc
forall x. Rep BotSrc x -> BotSrc
forall x. BotSrc -> Rep BotSrc x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BotSrc x -> BotSrc
$cfrom :: forall x. BotSrc -> Rep BotSrc x
Generic)




-- | An operator is a pure operation over bit-vectors, annotated with the bit-size of its operands.
-- For example, @Plus 64@ denotes 64-bit addition.
-- @Udiv@ and @Times@ are operators op type @w -> w -> w@ with all words same length.
-- @Div@ and @Div_Rem@ are operators of type @w -> w -> w -> w@ performing concatenation of the first two words and then doing division/remainder.
data Operator = 
    Minus Int | Plus Int | Times Int | And Int | Or Int | Xor Int | Not Int | SetXX | Bsr Int 
  | Div_Rem Int | Div Int | Shl Int | Shr Int | Sar Int | Udiv Int | Ror Int | Rol Int
  | Bswap Int | Pextr Int
 deriving (Operator -> Operator -> Bool
(Operator -> Operator -> Bool)
-> (Operator -> Operator -> Bool) -> Eq Operator
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Operator -> Operator -> Bool
$c/= :: Operator -> Operator -> Bool
== :: Operator -> Operator -> Bool
$c== :: Operator -> Operator -> Bool
Eq, Eq Operator
Eq Operator
-> (Operator -> Operator -> Ordering)
-> (Operator -> Operator -> Bool)
-> (Operator -> Operator -> Bool)
-> (Operator -> Operator -> Bool)
-> (Operator -> Operator -> Bool)
-> (Operator -> Operator -> Operator)
-> (Operator -> Operator -> Operator)
-> Ord Operator
Operator -> Operator -> Bool
Operator -> Operator -> Ordering
Operator -> Operator -> Operator
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Operator -> Operator -> Operator
$cmin :: Operator -> Operator -> Operator
max :: Operator -> Operator -> Operator
$cmax :: Operator -> Operator -> Operator
>= :: Operator -> Operator -> Bool
$c>= :: Operator -> Operator -> Bool
> :: Operator -> Operator -> Bool
$c> :: Operator -> Operator -> Bool
<= :: Operator -> Operator -> Bool
$c<= :: Operator -> Operator -> Bool
< :: Operator -> Operator -> Bool
$c< :: Operator -> Operator -> Bool
compare :: Operator -> Operator -> Ordering
$ccompare :: Operator -> Operator -> Ordering
$cp1Ord :: Eq Operator
Ord, (forall x. Operator -> Rep Operator x)
-> (forall x. Rep Operator x -> Operator) -> Generic Operator
forall x. Rep Operator x -> Operator
forall x. Operator -> Rep Operator x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Operator x -> Operator
$cfrom :: forall x. Operator -> Rep Operator x
Generic)


instance Show Operator where
  show :: Operator -> String
show (Plus    Int
b) = String
"+"       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Minus   Int
b) = String
"-"       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Times   Int
b) = String
"*"       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (And     Int
b) = String
"&"       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Or      Int
b) = String
"|"       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Xor     Int
b) = String
"xor"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Not     Int
b) = String
"not"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Bsr     Int
b) = String
"bsr"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Div_Rem Int
b) = String
"div_rem" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Div     Int
b) = String
"div"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Shl     Int
b) = String
"shl"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Shr     Int
b) = String
"shr"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Sar     Int
b) = String
"sar"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Udiv    Int
b) = String
"udiv"    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Ror     Int
b) = String
"ror"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Rol     Int
b) = String
"rol"     String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Bswap   Int
b) = String
"bswap"   String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  show (Pextr   Int
b) = String
"pextr"   String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b

-- | A symbolic expression with as leafs either immediates, variables, live values of stateparts, or malloced addresses.
-- A variable is a constant representing some initial value, e.g., RDI_0, or [RSP_0,8]_0.
-- A statepart evaluates to its current value, e.g., RDI or [RSP,8].
data SimpleExpr =
    SE_Immediate Word64                        -- ^ An immediate word
  | SE_Var       StatePart                     -- ^ A variable representing the initial value stored in the statepart (e.g., RSP0)
  | SE_StatePart StatePart                     -- ^ The value stored currently in the statepart
  | SE_Malloc    (Maybe Word64) (Maybe String) -- ^ A malloc return value with possibly an ID
  | SE_Op        Operator [SimpleExpr]         -- ^ Application of an @`Operator`@ to the list of arguments
  | SE_Bit       Int SimpleExpr                -- ^ Taking the lower bits of a value
  | SE_SExtend   Int Int SimpleExpr            -- ^ Sign extension
  | SE_Overwrite Int SimpleExpr SimpleExpr     -- ^ Overwriting certain bits of a value with bits from another value
  | Bottom       BotTyp                        -- ^ Bottom (unknown value)
 deriving (SimpleExpr -> SimpleExpr -> Bool
(SimpleExpr -> SimpleExpr -> Bool)
-> (SimpleExpr -> SimpleExpr -> Bool) -> Eq SimpleExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimpleExpr -> SimpleExpr -> Bool
$c/= :: SimpleExpr -> SimpleExpr -> Bool
== :: SimpleExpr -> SimpleExpr -> Bool
$c== :: SimpleExpr -> SimpleExpr -> Bool
Eq, Eq SimpleExpr
Eq SimpleExpr
-> (SimpleExpr -> SimpleExpr -> Ordering)
-> (SimpleExpr -> SimpleExpr -> Bool)
-> (SimpleExpr -> SimpleExpr -> Bool)
-> (SimpleExpr -> SimpleExpr -> Bool)
-> (SimpleExpr -> SimpleExpr -> Bool)
-> (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> Ord SimpleExpr
SimpleExpr -> SimpleExpr -> Bool
SimpleExpr -> SimpleExpr -> Ordering
SimpleExpr -> SimpleExpr -> SimpleExpr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SimpleExpr -> SimpleExpr -> SimpleExpr
$cmin :: SimpleExpr -> SimpleExpr -> SimpleExpr
max :: SimpleExpr -> SimpleExpr -> SimpleExpr
$cmax :: SimpleExpr -> SimpleExpr -> SimpleExpr
>= :: SimpleExpr -> SimpleExpr -> Bool
$c>= :: SimpleExpr -> SimpleExpr -> Bool
> :: SimpleExpr -> SimpleExpr -> Bool
$c> :: SimpleExpr -> SimpleExpr -> Bool
<= :: SimpleExpr -> SimpleExpr -> Bool
$c<= :: SimpleExpr -> SimpleExpr -> Bool
< :: SimpleExpr -> SimpleExpr -> Bool
$c< :: SimpleExpr -> SimpleExpr -> Bool
compare :: SimpleExpr -> SimpleExpr -> Ordering
$ccompare :: SimpleExpr -> SimpleExpr -> Ordering
$cp1Ord :: Eq SimpleExpr
Ord, (forall x. SimpleExpr -> Rep SimpleExpr x)
-> (forall x. Rep SimpleExpr x -> SimpleExpr) -> Generic SimpleExpr
forall x. Rep SimpleExpr x -> SimpleExpr
forall x. SimpleExpr -> Rep SimpleExpr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SimpleExpr x -> SimpleExpr
$cfrom :: forall x. SimpleExpr -> Rep SimpleExpr x
Generic)

-- | A statepart is either a register or a region in memory
data StatePart =
    SP_StackPointer String   -- ^ The stack pointer of the given function
  | SP_Reg Register          -- ^ A register
  | SP_Mem SimpleExpr Int    -- ^ A region with a symbolic address and an immediate size.
 deriving (StatePart -> StatePart -> Bool
(StatePart -> StatePart -> Bool)
-> (StatePart -> StatePart -> Bool) -> Eq StatePart
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StatePart -> StatePart -> Bool
$c/= :: StatePart -> StatePart -> Bool
== :: StatePart -> StatePart -> Bool
$c== :: StatePart -> StatePart -> Bool
Eq, Eq StatePart
Eq StatePart
-> (StatePart -> StatePart -> Ordering)
-> (StatePart -> StatePart -> Bool)
-> (StatePart -> StatePart -> Bool)
-> (StatePart -> StatePart -> Bool)
-> (StatePart -> StatePart -> Bool)
-> (StatePart -> StatePart -> StatePart)
-> (StatePart -> StatePart -> StatePart)
-> Ord StatePart
StatePart -> StatePart -> Bool
StatePart -> StatePart -> Ordering
StatePart -> StatePart -> StatePart
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: StatePart -> StatePart -> StatePart
$cmin :: StatePart -> StatePart -> StatePart
max :: StatePart -> StatePart -> StatePart
$cmax :: StatePart -> StatePart -> StatePart
>= :: StatePart -> StatePart -> Bool
$c>= :: StatePart -> StatePart -> Bool
> :: StatePart -> StatePart -> Bool
$c> :: StatePart -> StatePart -> Bool
<= :: StatePart -> StatePart -> Bool
$c<= :: StatePart -> StatePart -> Bool
< :: StatePart -> StatePart -> Bool
$c< :: StatePart -> StatePart -> Bool
compare :: StatePart -> StatePart -> Ordering
$ccompare :: StatePart -> StatePart -> Ordering
$cp1Ord :: Eq StatePart
Ord, (forall x. StatePart -> Rep StatePart x)
-> (forall x. Rep StatePart x -> StatePart) -> Generic StatePart
forall x. Rep StatePart x -> StatePart
forall x. StatePart -> Rep StatePart x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep StatePart x -> StatePart
$cfrom :: forall x. StatePart -> Rep StatePart x
Generic)


instance Show BotSrc where
  show :: BotSrc -> String
show (Src_Var StatePart
sp)             = SimpleExpr -> String
forall a. Show a => a -> String
show (SimpleExpr -> String) -> SimpleExpr -> String
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
  show (Src_StackPointer String
f)     = String
"RSP_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f
  show (Src_Malloc Maybe Word64
id Maybe String
h)        = SimpleExpr -> String
forall a. Show a => a -> String
show (SimpleExpr -> String) -> SimpleExpr -> String
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe String
h
  show (Src_ImmediateAddress Word64
a) = Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
a
  show (Src_Function String
f)         = String
f

show_srcs :: Set a -> String
show_srcs Set a
srcs = String
"|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show ([a] -> [String]) -> [a] -> [String]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
srcs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"

show_bottyp :: (Set BotSrc -> String) -> BotTyp -> String
show_bottyp Set BotSrc -> String
show_srcs (FromNonDeterminism Set SimpleExpr
es)        = String
"nd|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((SimpleExpr -> String) -> [SimpleExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> String
forall a. Show a => a -> String
show ([SimpleExpr] -> [String]) -> [SimpleExpr] -> [String]
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList Set SimpleExpr
es) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
show_bottyp Set BotSrc -> String
show_srcs (FromPointerBases Set PointerBase
bs)          = String
"pbs|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((PointerBase -> String) -> [PointerBase] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PointerBase -> String
forall a. Show a => a -> String
show ([PointerBase] -> [String]) -> [PointerBase] -> [String]
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
show_bottyp Set BotSrc -> String
show_srcs (FromSources Set BotSrc
srcs)             = String
"src" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromBitMode Set BotSrc
srcs)             = String
"b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromOverlap Set BotSrc
srcs)             = String
"o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromSemantics Set BotSrc
srcs)           = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromMemWrite Set BotSrc
srcs)            = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromUninitializedMemory Set BotSrc
srcs) = String
"m" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set BotSrc -> String
show_srcs Set BotSrc
srcs
show_bottyp Set BotSrc -> String
show_srcs (FromCall String
f)                   = String
"c|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"

instance Show BotTyp where
  show :: BotTyp -> String
show = (Set BotSrc -> String) -> BotTyp -> String
show_bottyp Set BotSrc -> String
forall a. Show a => Set a -> String
show_srcs

show_expr :: (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs (Bottom BotTyp
typ)              = String
"Bot[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> BotTyp -> String
show_bottyp Set BotSrc -> String
show_srcs BotTyp
typ String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
show_expr Set BotSrc -> String
show_srcs (SE_Malloc Maybe Word64
Nothing Maybe String
_)     = String
"malloc()" 
show_expr Set BotSrc -> String
show_srcs (SE_Malloc (Just Word64
id) Maybe String
_)   = String
"malloc@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
id String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"()" 
show_expr Set BotSrc -> String
show_srcs (SE_Var StatePart
sp)               = StatePart -> String
forall a. Show a => a -> String
show StatePart
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_0"
show_expr Set BotSrc -> String
show_srcs (SE_Immediate Word64
i)          = if Word64
i Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
2000 then String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
i else Word64 -> String
forall a. Show a => a -> String
show Word64
i
show_expr Set BotSrc -> String
show_srcs (SE_StatePart StatePart
sp)         = StatePart -> String
forall a. Show a => a -> String
show StatePart
sp
show_expr Set BotSrc -> String
show_srcs (SE_Op (Plus  Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op (Minus Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op (Times Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op (And   Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" & "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op (Or    Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" | "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op (Xor   Int
_) [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" xor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Op Operator
op [SimpleExpr]
es)             = Operator -> String
forall a. Show a => a -> String
show Operator
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((SimpleExpr -> String) -> [SimpleExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs) [SimpleExpr]
es) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Bit Int
i SimpleExpr
a)              = String
"b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_SExtend Int
l Int
h SimpleExpr
a)        = String
"signextend(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr Set BotSrc -> String
show_srcs (SE_Overwrite Int
i SimpleExpr
a SimpleExpr
b)      = String
"overwrite(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
show_srcs SimpleExpr
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"


instance Show SimpleExpr where
  show :: SimpleExpr -> String
show = (Set BotSrc -> String) -> SimpleExpr -> String
show_expr Set BotSrc -> String
forall a. Show a => Set a -> String
show_srcs





-- | Returns true iff the expression is an immediate value
is_immediate :: SimpleExpr -> Bool
is_immediate (SE_Immediate Word64
_) = Bool
True
is_immediate SimpleExpr
_                = Bool
False


-- | Is the statepart memory?
is_mem_sp :: StatePart -> Bool
is_mem_sp (SP_StackPointer String
_) = Bool
False
is_mem_sp (SP_Reg Register
_)          = Bool
False
is_mem_sp (SP_Mem SimpleExpr
a Int
si)       = Bool
True

-- | Is the statepart a register?
is_reg_sp :: StatePart -> Bool
is_reg_sp (SP_StackPointer String
_) = Bool
True
is_reg_sp (SP_Reg Register
_)          = Bool
True
is_reg_sp (SP_Mem SimpleExpr
a Int
si)       = Bool
False


-- | Returns true iff the expression contains Bot
contains_bot :: SimpleExpr -> Bool
contains_bot (Bottom BotTyp
typ)         = Bool
True
contains_bot (SE_Malloc Maybe Word64
_ Maybe String
_)      = Bool
False
contains_bot (SE_Var StatePart
sp)          = StatePart -> Bool
contains_bot_sp StatePart
sp
contains_bot (SE_Immediate Word64
_)     = Bool
False
contains_bot (SE_StatePart StatePart
sp)    = StatePart -> Bool
contains_bot_sp StatePart
sp
contains_bot (SE_Op Operator
_ [SimpleExpr]
es)         = (SimpleExpr -> Bool) -> [SimpleExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SimpleExpr -> Bool
contains_bot [SimpleExpr]
es
contains_bot (SE_Bit Int
i SimpleExpr
e)         = SimpleExpr -> Bool
contains_bot SimpleExpr
e
contains_bot (SE_SExtend Int
_ Int
_ SimpleExpr
e)   = SimpleExpr -> Bool
contains_bot SimpleExpr
e
contains_bot (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b) = SimpleExpr -> Bool
contains_bot SimpleExpr
a Bool -> Bool -> Bool
|| SimpleExpr -> Bool
contains_bot SimpleExpr
b

-- | Returns true iff the statepart contains Bot
contains_bot_sp :: StatePart -> Bool
contains_bot_sp (SP_StackPointer String
_) = Bool
False
contains_bot_sp (SP_Reg Register
r)          = Bool
False
contains_bot_sp (SP_Mem SimpleExpr
a Int
si)       = SimpleExpr -> Bool
contains_bot SimpleExpr
a






-- | concatMap function p over all bottom values in the expression  
map_all_bot :: Ord a => (BotTyp -> S.Set a) -> SimpleExpr -> S.Set a
map_all_bot :: (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p (Bottom BotTyp
typ)         = BotTyp -> Set a
p BotTyp
typ
map_all_bot BotTyp -> Set a
p (SE_Malloc Maybe Word64
_ Maybe String
_)      = Set a
forall a. Set a
S.empty
map_all_bot BotTyp -> Set a
p (SE_Var StatePart
sp)          = (BotTyp -> Set a) -> StatePart -> Set a
forall a. Ord a => (BotTyp -> Set a) -> StatePart -> Set a
map_all_bot_sp BotTyp -> Set a
p StatePart
sp
map_all_bot BotTyp -> Set a
p (SE_Immediate Word64
_)     = Set a
forall a. Set a
S.empty
map_all_bot BotTyp -> Set a
p (SE_StatePart StatePart
sp)    = (BotTyp -> Set a) -> StatePart -> Set a
forall a. Ord a => (BotTyp -> Set a) -> StatePart -> Set a
map_all_bot_sp BotTyp -> Set a
p StatePart
sp
map_all_bot BotTyp -> Set a
p (SE_Op Operator
_ [SimpleExpr]
es)         = [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set a] -> Set a) -> [Set a] -> Set a
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set a) -> [SimpleExpr] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map ((BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p) [SimpleExpr]
es
map_all_bot BotTyp -> Set a
p (SE_Bit Int
i SimpleExpr
e)         = (BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p SimpleExpr
e
map_all_bot BotTyp -> Set a
p (SE_SExtend Int
_ Int
_ SimpleExpr
e)   = (BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p SimpleExpr
e
map_all_bot BotTyp -> Set a
p (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b) = [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [(BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p SimpleExpr
a, (BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p SimpleExpr
b]

map_all_bot_sp :: (BotTyp -> Set a) -> StatePart -> Set a
map_all_bot_sp BotTyp -> Set a
p (SP_StackPointer String
r) = Set a
forall a. Set a
S.empty
map_all_bot_sp BotTyp -> Set a
p (SP_Reg Register
r)          = Set a
forall a. Set a
S.empty
map_all_bot_sp BotTyp -> Set a
p (SP_Mem SimpleExpr
a Int
si)       = (BotTyp -> Set a) -> SimpleExpr -> Set a
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot BotTyp -> Set a
p SimpleExpr
a


-- | Do all occurences of Bottom satisfy the given predicate?
all_bot_satisfy :: (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p = Set Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Set Bool -> Bool)
-> (SimpleExpr -> Set Bool) -> SimpleExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BotTyp -> Set Bool) -> SimpleExpr -> Set Bool
forall a. Ord a => (BotTyp -> Set a) -> SimpleExpr -> Set a
map_all_bot (Bool -> Set Bool
forall a. a -> Set a
S.singleton (Bool -> Set Bool) -> (BotTyp -> Bool) -> BotTyp -> Set Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BotTyp -> Bool
p)




-- | 
expr_size :: SimpleExpr -> Int
expr_size (Bottom BotTyp
typ)         = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ BotTyp -> Int
expr_size_bottyp BotTyp
typ
expr_size (SE_Malloc Maybe Word64
id Maybe String
_)     = Int
1
expr_size (SE_Var StatePart
sp)          = StatePart -> Int
expr_size_sp StatePart
sp
expr_size (SE_Immediate Word64
_)     = Int
1
expr_size (SE_StatePart StatePart
sp)    = StatePart -> Int
expr_size_sp StatePart
sp
expr_size (SE_Op Operator
_ [SimpleExpr]
es)         = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ([Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Int) -> [SimpleExpr] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Int
expr_size [SimpleExpr]
es)
expr_size (SE_Bit Int
i SimpleExpr
e)         = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SimpleExpr -> Int
expr_size SimpleExpr
e
expr_size (SE_SExtend Int
l Int
h SimpleExpr
e)   = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SimpleExpr -> Int
expr_size SimpleExpr
e
expr_size (SE_Overwrite Int
_ SimpleExpr
_ SimpleExpr
e) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SimpleExpr -> Int
expr_size SimpleExpr
e

expr_size_sp :: StatePart -> Int
expr_size_sp (SP_StackPointer String
_) = Int
1
expr_size_sp (SP_Reg Register
r)          = Int
1
expr_size_sp (SP_Mem SimpleExpr
a Int
si)       = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SimpleExpr -> Int
expr_size SimpleExpr
a 

expr_size_bottyp :: BotTyp -> Int
expr_size_bottyp (FromNonDeterminism Set SimpleExpr
es)        = Set Int -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Set Int -> Int) -> Set Int -> Int
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Int) -> Set SimpleExpr -> Set Int
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Int
expr_size Set SimpleExpr
es
expr_size_bottyp (FromPointerBases Set PointerBase
bs)          = Set PointerBase -> Int
forall a. Set a -> Int
S.size Set PointerBase
bs
expr_size_bottyp (FromSources Set BotSrc
srcs)             = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromBitMode Set BotSrc
srcs)             = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromOverlap Set BotSrc
srcs)             = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromSemantics Set BotSrc
srcs)           = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromMemWrite Set BotSrc
srcs)            = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromUninitializedMemory Set BotSrc
srcs) = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs
expr_size_bottyp (FromCall String
_)                   = Int
1





-- | The lowest botom element
rock_bottom :: SimpleExpr
rock_bottom = BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromSources Set BotSrc
forall a. Set a
S.empty)



sextend_32_64 :: p -> p
sextend_32_64 p
w = if p -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit p
w Int
31 then p
w p -> p -> p
forall a. Bits a => a -> a -> a
.|. p
0xFFFFFFFF00000000 else p
w
sextend_16_64 :: p -> p
sextend_16_64 p
w = if p -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit p
w Int
15 then p
w p -> p -> p
forall a. Bits a => a -> a -> a
.|. p
0xFFFFFFFFFFFF0000 else p
w
sextend_8_64 :: p -> p
sextend_8_64  p
w = if p -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit p
w Int
7  then p
w p -> p -> p
forall a. Bits a => a -> a -> a
.|. p
0xFFFFFFFFFFFFFF00 else p
w


-- | Simplification of symbolic expressions. 
--
-- Must always produce an expression logically equivalent to the original.
-- TODO: overwrite(8,Bot[src|RSP_0x1000070ec,malloc@100007204()|],b8(Bot[m|RSP_0x1000070ec,malloc@100007204()|]))
simp :: SimpleExpr -> SimpleExpr
simp :: SimpleExpr -> SimpleExpr
simp SimpleExpr
e = 
  let e' :: SimpleExpr
e' = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e in
    if SimpleExpr
e SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
e' then SimpleExpr
e' else SimpleExpr -> SimpleExpr
simp SimpleExpr
e'

simp' :: SimpleExpr -> SimpleExpr
simp' (SE_Bit Int
i (SE_Bit Int
i' SimpleExpr
e))   = Int -> SimpleExpr -> SimpleExpr
SE_Bit (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
i Int
i') (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e
simp' (SE_Bit Int
i (SE_Overwrite Int
i' SimpleExpr
e0 SimpleExpr
e1)) = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i' then Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1) else Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
i' (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0) (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1)

simp' (SE_Overwrite Int
i (SE_Overwrite Int
i' SimpleExpr
e0 SimpleExpr
e1) SimpleExpr
e2) = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i' then Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
i (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0) (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e2) else Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
i (Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
i' (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0) (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1)) (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e2)

simp' (SE_SExtend Int
l Int
h (SE_Bit Int
i SimpleExpr
e))  = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l then Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e) else Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e)

simp' (SE_Op (Minus Int
b0) [SE_Op (Minus Int
b1) [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [SimpleExpr
a0, Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
a1, SimpleExpr
a2]] -- (a0-a1)-a2 ==> a0 - (a1 + a2)
simp' (SE_Op (Plus Int
b0)  [SE_Op (Minus Int
b1) [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [SimpleExpr
a0, Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [SimpleExpr
a1, SimpleExpr
a2]] -- (a0-a1)+a2 ==> a0 - (a1 - a2)
simp' (SE_Op (Minus Int
b0) [SE_Op (Plus Int
b1)  [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
a0, Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [SimpleExpr
a1, SimpleExpr
a2]] -- (a0+a1)-a2 ==> a0 + (a1 - a2)
simp' (SE_Op (Plus Int
b0)  [SE_Op (Plus Int
b1)  [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
a0, Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
a1, SimpleExpr
a2]] -- (a0+a1)+a2 ==> a0 + (a1 + a2)

simp' (SE_Op (Plus Int
b0)  [SE_Immediate Word64
0, SimpleExpr
e1]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1 -- 0 + e1 = e1
simp' (SE_Op (Plus Int
b0)  [SimpleExpr
e0, SE_Immediate Word64
0]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0 -- e0 + 0 = e0
simp' (SE_Op (Minus Int
b0) [SimpleExpr
e0, SE_Immediate Word64
0]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0 -- e0 - 0 = e0
simp' (SE_Op (Times Int
b0) [SimpleExpr
e0, SE_Immediate Word64
0]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op (Times Int
b0) [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0

simp' (SE_Overwrite Int
i (SE_Immediate Word64
0) SimpleExpr
e) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e

simp' (SE_Op (Minus Int
b0) [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
i1)   -- Immediate: i0 - i1
simp' (SE_Op (Plus  Int
b0) [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
i1)   -- Immediate: i0 + i1
simp' (SE_Op (Times Int
b0) [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
i1)   -- Immediate: i0 * i1
simp' (SE_Op (Or    Int
b0) [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.|. Word64
i1) -- Immediate: i0 | i1
simp' (SE_Op (And   Int
b0) [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
i1) -- Immediate: i0 & i1



simp' (SE_Bit Int
32 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64
i Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
0x00000000FFFFFFFF)
simp' (SE_Bit Int
16 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64
i Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
0x000000000000FFFF)
simp' (SE_Bit Int
8  (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64
i Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
0x00000000000000FF)

simp' (SE_SExtend Int
32 Int
64 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64 -> Word64
forall p. (Bits p, Num p) => p -> p
sextend_32_64 Word64
i)
simp' (SE_SExtend Int
16 Int
64 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64 -> Word64
forall p. (Bits p, Num p) => p -> p
sextend_16_64 Word64
i)
simp' (SE_SExtend Int
8  Int
64 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64 -> Word64
forall p. (Bits p, Num p) => p -> p
sextend_8_64 Word64
i)

simp' (SE_Op (Minus Int
b0) [SE_Immediate Word64
i0, SE_Op (Minus Int
b1) [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
i1), SimpleExpr
e1] -- i0-(e1-i1) ==> (i0+i1)-e1
simp' (SE_Op (Minus Int
b0) [SE_Immediate Word64
i0, SE_Op (Plus Int
b1)  [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i1), SimpleExpr
e1] -- i0-(e1+i1) ==> (i0-i1)-e1
simp' (SE_Op (Minus Int
b0) [SE_Immediate Word64
i0, SE_Op (Plus Int
b1)  [SE_Immediate Word64
i1, SimpleExpr
e1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b0) [Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i1), SimpleExpr
e1] -- i0-(i1+e1) ==> (i0-i1)-e1
simp' (SE_Op (Plus Int
b0)  [SE_Immediate Word64
i0, SE_Op (Minus Int
b1) [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
e1, Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i1)] -- i0+(e1-i1) ==> e1+(i0-i1)
simp' (SE_Op (Plus Int
b0)  [SE_Immediate Word64
i0, SE_Op (Plus  Int
b1) [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b0)  [SimpleExpr
e1, Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
i1)] -- i0+(e1+i1) ==> e1+(i0+i1)

simp' (SE_Op (Minus Int
b) [SimpleExpr
e,SE_Immediate Word64
i]) = if Word64 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word64
i Int
63 then Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
b)  [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (-Word64
i)] else Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b) [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]
simp' (SE_Op (Plus  Int
b) [SimpleExpr
e,SE_Immediate Word64
i]) = if Word64 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word64
i Int
63 then Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
b) [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (-Word64
i)] else Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus  Int
b) [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]


simp' (SE_Bit Int
i (SE_Op (Plus  Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
i)  [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0+e1) = b(e0) + b(e1)
simp' (SE_Bit Int
i (SE_Op (Minus Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
i) [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0-e1) = b(e0) - b(e1)
simp' (SE_Bit Int
i (SE_Op (Times Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Times Int
i) [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0*e1) = b(e0) * b(e1)
simp' (SE_Bit Int
i (SE_Op (And   Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
And Int
i)   [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0&e1) = b(e0) & b(e1)
simp' (SE_Bit Int
i (SE_Op (Or    Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Or Int
i)    [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0|e1) = b(e0) | b(e1)
simp' (SE_Bit Int
i (SE_Op (Xor   Int
b0) [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Xor Int
i)   [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0, Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e1] -- b(e0 xor e1) = b(e0) xor b(e1)
simp' (SE_Bit Int
i (SE_Op (Not   Int
b0) [SimpleExpr
e0]))     = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Not Int
i)   [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0]              -- b(not e0) = b(not e0)


simp' (Bottom (FromNonDeterminism Set SimpleExpr
es)) = BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> BotTyp
FromNonDeterminism (Set SimpleExpr -> BotTyp) -> Set SimpleExpr -> BotTyp
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr) -> Set SimpleExpr -> Set SimpleExpr
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> SimpleExpr
simp' Set SimpleExpr
es
simp' (SE_Op Operator
op [SimpleExpr]
es)          = Operator -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
op ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> SimpleExpr
simp' [SimpleExpr]
es
simp' (SE_StatePart StatePart
sp)      = StatePart -> SimpleExpr
SE_StatePart (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> StatePart
simp'_sp StatePart
sp
simp' (SE_Bit Int
i SimpleExpr
e)           = Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e
simp' (SE_SExtend Int
l Int
h SimpleExpr
e)     = Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e
simp' (SE_Overwrite Int
i SimpleExpr
e0 SimpleExpr
e1) = Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
i (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0) (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1)
simp' (SE_Var StatePart
sp)            = StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> StatePart
simp'_sp StatePart
sp
simp' SimpleExpr
e                      = SimpleExpr
e

simp'_sp :: StatePart -> StatePart
simp'_sp (SP_Mem SimpleExpr
e Int
si)    = SimpleExpr -> Int -> StatePart
SP_Mem (SimpleExpr -> SimpleExpr
simp' SimpleExpr
e) Int
si
simp'_sp StatePart
sp               = StatePart
sp




instance Show StatePart where
  show :: StatePart -> String
show (SP_StackPointer String
f) = String
"RSP_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f
  show (SP_Reg Register
r)          = Register -> String
forall a. Show a => a -> String
show Register
r
  show (SP_Mem SimpleExpr
a Int
si)       = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

-- | Symbolically represent the status of all flags in the current state
data FlagStatus = 
    None                                         -- ^ No information known, flags could have any value
  | FS_CMP (Maybe Bool) X86.Operand X86.Operand  -- ^ The flags are set by the x86 CMP instruction applied to the given operands.
  deriving ((forall x. FlagStatus -> Rep FlagStatus x)
-> (forall x. Rep FlagStatus x -> FlagStatus) -> Generic FlagStatus
forall x. Rep FlagStatus x -> FlagStatus
forall x. FlagStatus -> Rep FlagStatus x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FlagStatus x -> FlagStatus
$cfrom :: forall x. FlagStatus -> Rep FlagStatus x
Generic,FlagStatus -> FlagStatus -> Bool
(FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> Bool) -> Eq FlagStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlagStatus -> FlagStatus -> Bool
$c/= :: FlagStatus -> FlagStatus -> Bool
== :: FlagStatus -> FlagStatus -> Bool
$c== :: FlagStatus -> FlagStatus -> Bool
Eq,Eq FlagStatus
Eq FlagStatus
-> (FlagStatus -> FlagStatus -> Ordering)
-> (FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> FlagStatus)
-> (FlagStatus -> FlagStatus -> FlagStatus)
-> Ord FlagStatus
FlagStatus -> FlagStatus -> Bool
FlagStatus -> FlagStatus -> Ordering
FlagStatus -> FlagStatus -> FlagStatus
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FlagStatus -> FlagStatus -> FlagStatus
$cmin :: FlagStatus -> FlagStatus -> FlagStatus
max :: FlagStatus -> FlagStatus -> FlagStatus
$cmax :: FlagStatus -> FlagStatus -> FlagStatus
>= :: FlagStatus -> FlagStatus -> Bool
$c>= :: FlagStatus -> FlagStatus -> Bool
> :: FlagStatus -> FlagStatus -> Bool
$c> :: FlagStatus -> FlagStatus -> Bool
<= :: FlagStatus -> FlagStatus -> Bool
$c<= :: FlagStatus -> FlagStatus -> Bool
< :: FlagStatus -> FlagStatus -> Bool
$c< :: FlagStatus -> FlagStatus -> Bool
compare :: FlagStatus -> FlagStatus -> Ordering
$ccompare :: FlagStatus -> FlagStatus -> Ordering
$cp1Ord :: Eq FlagStatus
Ord)


instance Show PointerBase where
  show :: PointerBase -> String
show (StackPointer String
f)        = String
"StackPointer_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f
  show (Malloc Maybe Word64
Nothing  Maybe String
_)     = String
"malloc()"
  show (Malloc (Just Word64
a) Maybe String
_)     = String
"malloc@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"()"
  show (GlobalAddress Word64
a)       = String
"GlobalAddress@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
a
  show (PointerToSymbol Word64
a String
sym) = String
"PointerToSymbol_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sym





-- | A symbolic predicate consists of:
--
--   * A mapping from stateparts to symbolic expressions.
--   * The status of the flags.
--   * A set of verification conditions.
data Pred = Predicate (M.Map StatePart SimpleExpr) FlagStatus
  deriving ((forall x. Pred -> Rep Pred x)
-> (forall x. Rep Pred x -> Pred) -> Generic Pred
forall x. Rep Pred x -> Pred
forall x. Pred -> Rep Pred x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Pred x -> Pred
$cfrom :: forall x. Pred -> Rep Pred x
Generic,Pred -> Pred -> Bool
(Pred -> Pred -> Bool) -> (Pred -> Pred -> Bool) -> Eq Pred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pred -> Pred -> Bool
$c/= :: Pred -> Pred -> Bool
== :: Pred -> Pred -> Bool
$c== :: Pred -> Pred -> Bool
Eq,Eq Pred
Eq Pred
-> (Pred -> Pred -> Ordering)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Pred)
-> (Pred -> Pred -> Pred)
-> Ord Pred
Pred -> Pred -> Bool
Pred -> Pred -> Ordering
Pred -> Pred -> Pred
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Pred -> Pred -> Pred
$cmin :: Pred -> Pred -> Pred
max :: Pred -> Pred -> Pred
$cmax :: Pred -> Pred -> Pred
>= :: Pred -> Pred -> Bool
$c>= :: Pred -> Pred -> Bool
> :: Pred -> Pred -> Bool
$c> :: Pred -> Pred -> Bool
<= :: Pred -> Pred -> Bool
$c<= :: Pred -> Pred -> Bool
< :: Pred -> Pred -> Bool
$c< :: Pred -> Pred -> Bool
compare :: Pred -> Pred -> Ordering
$ccompare :: Pred -> Pred -> Ordering
$cp1Ord :: Eq Pred
Ord)

instance Cereal.Serialize PointerBase
instance Cereal.Serialize BotTyp
instance Cereal.Serialize BotSrc
instance Cereal.Serialize StatePart
instance Cereal.Serialize Operator
instance Cereal.Serialize SimpleExpr
instance Cereal.Serialize FlagStatus
instance Cereal.Serialize Pred

instance Show FlagStatus where
 show :: FlagStatus -> String
show FlagStatus
None = String
""
 show (FS_CMP Maybe Bool
Nothing      Operand
op1 Operand
op2) = String
"flags set by CMP(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
op1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
op2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
 show (FS_CMP (Just Bool
True)  Operand
op1 Operand
op2) = Operand -> String
forall a. Show a => a -> String
show Operand
op1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" < " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
op2
 show (FS_CMP (Just Bool
False) Operand
op1 Operand
op2) = Operand -> String
forall a. Show a => a -> String
show Operand
op1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
op2


instance Show Pred where
  show :: Pred -> String
show (Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg) =
       (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((StatePart, SimpleExpr) -> String)
-> [(StatePart, SimpleExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(StatePart
sp,SimpleExpr
e) -> StatePart -> String
forall a. Show a => a -> String
show StatePart
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
e) ([(StatePart, SimpleExpr)] -> [String])
-> [(StatePart, SimpleExpr)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
eqs))
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if FlagStatus -> String
forall a. Show a => a -> String
show FlagStatus
flg String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"" then String
"" else String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ FlagStatus -> String
forall a. Show a => a -> String
show FlagStatus
flg)



-- | Pretty print expression, showing Bottom expressions only as Bot
pp_expr :: SimpleExpr -> String
pp_expr = (Set BotSrc -> String) -> SimpleExpr -> String
show_expr (\Set BotSrc
_ -> String
"")

-- | Pretty print predicate, showing Bottom expressions only as Bot
pp_pred :: Pred -> String
pp_pred :: Pred -> String
pp_pred (Predicate Map StatePart SimpleExpr
eqs FlagStatus
_) = (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((StatePart, SimpleExpr) -> Maybe String)
-> [(StatePart, SimpleExpr)] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (StatePart, SimpleExpr) -> Maybe String
forall a. Show a => (a, SimpleExpr) -> Maybe String
pp_pred_entry ([(StatePart, SimpleExpr)] -> [String])
-> [(StatePart, SimpleExpr)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
eqs)
 where
  pp_pred_entry :: (a, SimpleExpr) -> Maybe String
pp_pred_entry (a
sp,SimpleExpr
v) =
    --if sp == SP_Reg RIP || contains_bot_sp sp then
    --  Nothing
    --else
      String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
pp_expr SimpleExpr
v