{-# 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.SymbolicExpression ( 
  StatePart (..),
  SimpleExpr (..),
  FlagStatus (..),
  BotTyp (..),
  BotSrc (..),
  Operator (..),
  PointerBase(..),
  is_immediate,
  is_mem_sp,
  is_reg_sp,
  contains_bot,
  contains_bot_sp,
  all_bot_satisfy,
  simp,
  pp_expr,
  expr_size,
  sextend_32_64,
  sextend_16_64,
  sextend_8_64
 )
 where

import Base
import Config
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import qualified Data.Set.NonEmpty as NES

import Data.Int (Int32,Int64)
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, (.|.), (.&.), xor)
import qualified Data.Serialize as Cereal hiding (get,put)
import X86.Register (Register)
import qualified X86.Operand as X86

import Control.DeepSeq


-- | 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.
  | ThreadLocalStorage                   -- ^ A pointer to the thread-local-storage (e.g., FS register)
  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 (NES.NESet SimpleExpr)   -- ^ The expression evaluates to one of the expressions in the set
  | FromPointerBases (NES.NESet PointerBase)    -- ^ The expression is a pointer-computation with known base(s)
  | FromCall String                             -- ^ Return value of a function call
  | FromSources (NES.NESet BotSrc)              -- ^ The expression is some computation based on sources.
  | FromOverlap (NES.NESet BotSrc)              -- ^ A read from two possibly overlapping regions
  | FromMemWrite (NES.NESet BotSrc)             -- ^ A write to two possibly overlapping regions 
  | FromSemantics (NES.NESet BotSrc)            -- ^ An instruction with unknown semantics
  | FromBitMode (NES.NESet BotSrc)              -- ^ Should not happen, but if a register writes to a registeralias with unknown bit size
  | FromUninitializedMemory (NES.NESet 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
  | Src_Mem (NES.NESet BotSrc)               -- ^ reading from memory
  | Src_ImmediateConstants                   -- ^ Some immediate value
 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 | Plus | Times | And | Or | Xor | Not | Bsr 
  | Div_Rem | Div | Shl | Shr | Sar | Udiv | Ror | Rol 
  | Bswap | Pextr
 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 (Operator
Plus    ) = String
"+"       
  show (Operator
Minus   ) = String
"-"       
  show (Operator
Times   ) = String
"*"       
  show (Operator
And     ) = String
"&"       
  show (Operator
Or      ) = String
"|"       
  show (Operator
Xor     ) = String
"xor"     
  show (Operator
Not     ) = String
"not"     
  show (Operator
Bsr     ) = String
"bsr"     
  show (Operator
Div_Rem ) = String
"div_rem" 
  show (Operator
Div     ) = String
"div"     
  show (Operator
Shl     ) = String
"shl"     
  show (Operator
Shr     ) = String
"shr"     
  show (Operator
Sar     ) = String
"sar"     
  show (Operator
Udiv    ) = String
"udiv"    
  show (Operator
Ror     ) = String
"ror"     
  show (Operator
Rol     ) = String
"rol"
  show (Operator
Bswap   ) = String
"bswap"
  show (Operator
Pextr   ) = String
"pextr"

-- | 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 Int [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 (Src_Mem NESet BotSrc
a)                = String
"*[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((BotSrc -> String) -> [BotSrc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map BotSrc -> String
forall a. Show a => a -> String
show ([BotSrc] -> [String]) -> [BotSrc] -> [String]
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> [BotSrc]
forall a. NESet a -> [a]
neSetToList NESet BotSrc
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
  show (BotSrc
Src_ImmediateConstants)   = String
"constant"

show_srcs :: NESet a -> String
show_srcs NESet 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 -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ NESet a -> Set a
forall a. NESet a -> Set a
NES.toSet NESet a
srcs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"

show_bottyp :: (NESet BotSrc -> String) -> BotTyp -> String
show_bottyp NESet BotSrc -> String
show_srcs (FromNonDeterminism NESet 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 -> [SimpleExpr]) -> Set SimpleExpr -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
show_bottyp NESet BotSrc -> String
show_srcs (FromPointerBases NESet 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 -> [PointerBase])
-> Set PointerBase -> [PointerBase]
forall a b. (a -> b) -> a -> b
$ NESet PointerBase -> Set PointerBase
forall a. NESet a -> Set a
NES.toSet NESet PointerBase
bs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
show_bottyp NESet BotSrc -> String
show_srcs (FromSources NESet BotSrc
srcs)             = String
"src" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet BotSrc -> String
show_srcs (FromBitMode NESet BotSrc
srcs)             = String
"b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet BotSrc -> String
show_srcs (FromOverlap NESet BotSrc
srcs)             = String
"o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet BotSrc -> String
show_srcs (FromSemantics NESet BotSrc
srcs)           = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet BotSrc -> String
show_srcs (FromMemWrite NESet BotSrc
srcs)            = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet BotSrc -> String
show_srcs (FromUninitializedMemory NESet BotSrc
srcs) = String
"m" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NESet BotSrc -> String
show_srcs NESet BotSrc
srcs
show_bottyp NESet 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 = (NESet BotSrc -> String) -> BotTyp -> String
show_bottyp NESet BotSrc -> String
forall a. Show a => NESet a -> String
show_srcs

show_expr :: (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs (Bottom BotTyp
typ)              = String
"Bot[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> BotTyp -> String
show_bottyp NESet BotSrc -> String
show_srcs BotTyp
typ String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
show_expr NESet BotSrc -> String
show_srcs (SE_Malloc Maybe Word64
Nothing Maybe String
_)     = String
"malloc()" 
show_expr NESet 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 NESet 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 NESet 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 NESet BotSrc -> String
show_srcs (SE_StatePart StatePart
sp)         = StatePart -> String
forall a. Show a => a -> String
show StatePart
sp
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
Plus ) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
Minus) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
Times) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
And  ) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" & "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
Or   ) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" | "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op (Operator
Xor  ) Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" xor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet BotSrc -> String
show_srcs (SE_Op Operator
op Int
si [SimpleExpr]
es)          = Operator -> String
forall a. Show a => a -> String
show Operator
op 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
"(" 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 ((NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs) [SimpleExpr]
es) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet 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]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet 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]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_expr NESet 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]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
show_srcs SimpleExpr
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"


instance Show SimpleExpr where
  show :: SimpleExpr -> String
show = (NESet BotSrc -> String) -> SimpleExpr -> String
show_expr NESet BotSrc -> String
forall a. Show a => NESet 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
_ Int
_ [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  
all_bot_satisfy :: (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy :: (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p (Bottom BotTyp
typ)         = BotTyp -> Bool
p BotTyp
typ
all_bot_satisfy BotTyp -> Bool
p (SE_Malloc Maybe Word64
_ Maybe String
_)      = Bool
True
all_bot_satisfy BotTyp -> Bool
p (SE_Var StatePart
sp)          = (BotTyp -> Bool) -> StatePart -> Bool
all_bot_satisfy_sp BotTyp -> Bool
p StatePart
sp
all_bot_satisfy BotTyp -> Bool
p (SE_Immediate Word64
_)     = Bool
True
all_bot_satisfy BotTyp -> Bool
p (SE_StatePart StatePart
sp)    = (BotTyp -> Bool) -> StatePart -> Bool
all_bot_satisfy_sp BotTyp -> Bool
p StatePart
sp
all_bot_satisfy BotTyp -> Bool
p (SE_Op Operator
_ Int
_ [SimpleExpr]
es)       = (SimpleExpr -> Bool) -> [SimpleExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p) [SimpleExpr]
es
all_bot_satisfy BotTyp -> Bool
p (SE_Bit Int
i SimpleExpr
e)         = (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p SimpleExpr
e
all_bot_satisfy BotTyp -> Bool
p (SE_SExtend Int
_ Int
_ SimpleExpr
e)   = (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p SimpleExpr
e
all_bot_satisfy BotTyp -> Bool
p (SE_Overwrite Int
_ SimpleExpr
a SimpleExpr
b) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [(BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p SimpleExpr
a, (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p SimpleExpr
b]

all_bot_satisfy_sp :: (BotTyp -> Bool) -> StatePart -> Bool
all_bot_satisfy_sp BotTyp -> Bool
p (SP_StackPointer String
r) = Bool
True
all_bot_satisfy_sp BotTyp -> Bool
p (SP_Reg Register
r)          = Bool
True
all_bot_satisfy_sp BotTyp -> Bool
p (SP_Mem SimpleExpr
a Int
si)       = (BotTyp -> Bool) -> SimpleExpr -> Bool
all_bot_satisfy BotTyp -> Bool
p SimpleExpr
a





-- | 
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
_ Int
_ [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 NESet SimpleExpr
es)        = NESet Int -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (NESet Int -> Int) -> NESet Int -> Int
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Int) -> NESet SimpleExpr -> NESet Int
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SimpleExpr -> Int
expr_size NESet SimpleExpr
es
expr_size_bottyp (FromPointerBases NESet PointerBase
bs)          = NESet PointerBase -> Int
forall a. NESet a -> Int
NES.size NESet PointerBase
bs
expr_size_bottyp (FromSources NESet BotSrc
srcs)             = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromBitMode NESet BotSrc
srcs)             = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromOverlap NESet BotSrc
srcs)             = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromSemantics NESet BotSrc
srcs)           = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromMemWrite NESet BotSrc
srcs)            = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromUninitializedMemory NESet BotSrc
srcs) = NESet BotSrc -> Int
forall a. NESet a -> Int
NES.size NESet BotSrc
srcs
expr_size_bottyp (FromCall String
_)                   = Int
1



-- | Sign-extension from 32 to 64 bits
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
-- | Sign-extension from 16 to 64 bits
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
-- | Sign-extension from 8 to 64 bits
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.
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_Bit Int
i (SE_SExtend Int
l Int
h SimpleExpr
e))      = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l then SimpleExpr -> SimpleExpr
simp' SimpleExpr
e else Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ 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 (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 Operator
Minus Int
si0 [SE_Op Operator
Minus Int
_ [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr
a0, Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr
a1, SimpleExpr
a2]] -- (a0-a1)-a2 ==> a0 - (a1 + a2)
simp' (SE_Op Operator
Plus  Int
si0 [SE_Op Operator
Minus Int
_ [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr
a0, Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr
a1, SimpleExpr
a2]] -- (a0-a1)+a2 ==> a0 - (a1 - a2)
simp' (SE_Op Operator
Minus Int
si0 [SE_Op Operator
Plus  Int
_ [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr
a0, Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr
a1, SimpleExpr
a2]] -- (a0+a1)-a2 ==> a0 + (a1 - a2)
simp' (SE_Op Operator
Plus  Int
si0 [SE_Op Operator
Plus  Int
_ [SimpleExpr
a0,SimpleExpr
a1], SimpleExpr
a2]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr
a0, Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr
a1, SimpleExpr
a2]] -- (a0+a1)+a2 ==> a0 + (a1 + a2)

simp' (SE_Op Operator
Plus  Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1 -- 0 + e1 = e1
simp' (SE_Op Operator
Plus  Int
si0 [SimpleExpr
e0, SE_Immediate Word64
0]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0 -- e0 + 0 = e0
simp' (SE_Op Operator
Minus Int
si0 [SimpleExpr
e0, SE_Immediate Word64
0]) = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e0 -- e0 - 0 = e0
simp' (SE_Op Operator
Times Int
si0 [SimpleExpr
e0, SE_Immediate Word64
0]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Times Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Udiv  Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Div   Int
si0 [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 Operator
Minus Int
si0 [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 Operator
Plus  Int
si0 [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 Operator
Times Int
si0 [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 Operator
Or    Int
si0 [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 Operator
And   Int
si0 [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 Operator
Xor   Int
si0 [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
`xor` Word64
i1) -- Immediate: i0 xor i1
simp' (SE_Op Operator
Udiv  Int
64  [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0  Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
i1) 
simp' (SE_Op Operator
Udiv  Int
32  [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Word64 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0::Word32) Word32 -> Word32 -> Word32
forall a. Integral a => a -> a -> a
`div` (Word64 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1::Word32)))
simp' (SE_Op Operator
Div   Int
64  [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Int64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0::Int64)  Int64 -> Int64 -> Int64
forall a. Integral a => a -> a -> a
`div` (Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1::Int64))) 
simp' (SE_Op Operator
Div   Int
32  [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Int32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Word64 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0::Int32)  Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
`div` (Word64 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1::Int32)))



simp' (SE_Bit Int
128 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate Word64
i
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 Operator
Minus Int
si0 [SE_Immediate Word64
i0, SE_Op Operator
Minus Int
_ [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [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 Operator
Minus Int
si0 [SE_Immediate Word64
i0, SE_Op Operator
Plus  Int
_ [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [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 Operator
Minus Int
si0 [SE_Immediate Word64
i0, SE_Op Operator
Plus  Int
_ [SE_Immediate Word64
i1, SimpleExpr
e1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [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 Operator
Plus  Int
si0 [SE_Immediate Word64
i0, SE_Op Operator
Minus Int
_ [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [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 Operator
Plus  Int
si0 [SE_Immediate Word64
i0, SE_Op Operator
Plus  Int
_ [SimpleExpr
e1, SE_Immediate Word64
i1]]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [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 Operator
Minus Int
si0 [SimpleExpr
e,SE_Immediate Word64
i]) = if Word64 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word64
i Int
63 then Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (-Word64
i)] else Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]
simp' (SE_Op Operator
Plus  Int
si0 [SimpleExpr
e,SE_Immediate Word64
i]) = if Word64 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word64
i Int
63 Bool -> Bool -> Bool
&& Word64
i Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
0x8000000000000000 then Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (-Word64
i)] else Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]
simp' (SE_Op Operator
Plus  Int
si0 [SE_Immediate Word64
i,SimpleExpr
e]) = if Word64 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word64
i Int
63  Bool -> Bool -> Bool
&& Word64
i Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
0x8000000000000000 then Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (-Word64
i)] else Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [SimpleExpr -> SimpleExpr
simp' SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]


simp' (SE_Bit Int
i (SE_Op Operator
Plus  Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus  Int
si0 [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 Operator
Minus Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si0 [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 Operator
Times Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si0 [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 Operator
And   Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
And   Int
si0 [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 Operator
Or    Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Or    Int
si0 [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 Operator
Xor   Int
si0 [SimpleExpr
e0, SimpleExpr
e1])) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor   Int
si0 [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 Operator
Not   Int
si0 [SimpleExpr
e0]))     = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Not   Int
si0 [Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e0]              -- b(not e0) = b(not e0)

simp' (SE_Op Operator
Xor Int
si0 [SimpleExpr
e0,SimpleExpr
e1]) = if SimpleExpr
e0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleExpr
e1 then Word64 -> SimpleExpr
SE_Immediate Word64
0 else Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si0 ([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
e0,SimpleExpr
e1]

simp' (Bottom (FromNonDeterminism NESet SimpleExpr
es)) = BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> BotTyp
FromNonDeterminism (NESet SimpleExpr -> BotTyp) -> NESet SimpleExpr -> BotTyp
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr) -> NESet SimpleExpr -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SimpleExpr -> SimpleExpr
simp' NESet SimpleExpr
es
simp' (SE_Op Operator
op Int
si0 [SimpleExpr]
es)                = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
op Int
si0 ([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 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 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
  show PointerBase
ThreadLocalStorage      = String
"ThreadLocalStorage"




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



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 NFData PointerBase
instance NFData BotTyp
instance NFData BotSrc
instance NFData StatePart
instance NFData Operator
instance NFData SimpleExpr
instance NFData FlagStatus