{-# LANGUAGE DeriveGeneric #-}


{-|
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,
  addends
 )
 where

import Base
import Config

import Binary.Generic
import Data.Symbol
import Data.Size
import Data.X86.Register
import Data.X86.Instruction

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, shiftL,shiftR)
import qualified Data.Serialize as Cereal hiding (get,put)


import Control.DeepSeq


-- | A pointerbase is a positive addend of a symbolic expression that may represent a pointer.
data PointerBase = 
    StackPointer                         -- ^ 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.
  | ThreadLocalStorage                   -- ^ A pointer to the thread-local-storage (e.g., FS register)
  | BaseIsStatePart StatePart            -- ^ A statepart that is known to contain a pointer
  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
$cfrom :: forall x. PointerBase -> Rep PointerBase x
from :: forall x. PointerBase -> Rep PointerBase x
$cto :: forall x. Rep PointerBase x -> PointerBase
to :: forall x. Rep PointerBase x -> PointerBase
Generic,PointerBase -> PointerBase -> Bool
(PointerBase -> PointerBase -> Bool)
-> (PointerBase -> PointerBase -> Bool) -> Eq PointerBase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PointerBase -> PointerBase -> Bool
== :: PointerBase -> PointerBase -> Bool
$c/= :: PointerBase -> PointerBase -> Bool
/= :: 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
$ccompare :: PointerBase -> PointerBase -> Ordering
compare :: PointerBase -> PointerBase -> Ordering
$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
>= :: PointerBase -> PointerBase -> Bool
$cmax :: PointerBase -> PointerBase -> PointerBase
max :: PointerBase -> PointerBase -> PointerBase
$cmin :: PointerBase -> PointerBase -> PointerBase
min :: PointerBase -> PointerBase -> 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
  | RockBottom
 deriving (BotTyp -> BotTyp -> Bool
(BotTyp -> BotTyp -> Bool)
-> (BotTyp -> BotTyp -> Bool) -> Eq BotTyp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BotTyp -> BotTyp -> Bool
== :: BotTyp -> BotTyp -> Bool
$c/= :: BotTyp -> BotTyp -> Bool
/= :: 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
$ccompare :: BotTyp -> BotTyp -> Ordering
compare :: BotTyp -> BotTyp -> Ordering
$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
>= :: BotTyp -> BotTyp -> Bool
$cmax :: BotTyp -> BotTyp -> BotTyp
max :: BotTyp -> BotTyp -> BotTyp
$cmin :: BotTyp -> BotTyp -> BotTyp
min :: BotTyp -> BotTyp -> 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
$cfrom :: forall x. BotTyp -> Rep BotTyp x
from :: forall x. BotTyp -> Rep BotTyp x
$cto :: forall x. Rep BotTyp x -> BotTyp
to :: forall x. Rep BotTyp x -> BotTyp
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                         -- ^ 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
$c== :: BotSrc -> BotSrc -> Bool
== :: BotSrc -> BotSrc -> Bool
$c/= :: BotSrc -> BotSrc -> Bool
/= :: 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
$ccompare :: BotSrc -> BotSrc -> Ordering
compare :: BotSrc -> BotSrc -> Ordering
$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
>= :: BotSrc -> BotSrc -> Bool
$cmax :: BotSrc -> BotSrc -> BotSrc
max :: BotSrc -> BotSrc -> BotSrc
$cmin :: BotSrc -> BotSrc -> BotSrc
min :: BotSrc -> BotSrc -> 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
$cfrom :: forall x. BotSrc -> Rep BotSrc x
from :: forall x. BotSrc -> Rep BotSrc x
$cto :: forall x. Rep BotSrc x -> BotSrc
to :: forall x. Rep BotSrc x -> BotSrc
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.
data Operator = 
    Minus | Plus | Times | And | Or | Xor | Not | Bsr 
  | SExtHi Int -- ^ The high part after sign-extension from $n$ bits, thus producing $n$-bit value
  | IMulLo | IMulHi
  | UdivHi | UdivLo | Udiv
  | SdivHi | SdivLo | Sdiv
  | Shl | Shr | Sar | Ror | Rol 
  | Bswap | Pextr | Sbb | Adc | Cmov | ZeroOne
 deriving (Operator -> Operator -> Bool
(Operator -> Operator -> Bool)
-> (Operator -> Operator -> Bool) -> Eq Operator
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Operator -> Operator -> Bool
== :: Operator -> Operator -> Bool
$c/= :: Operator -> Operator -> Bool
/= :: 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
$ccompare :: Operator -> Operator -> Ordering
compare :: Operator -> Operator -> Ordering
$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
>= :: Operator -> Operator -> Bool
$cmax :: Operator -> Operator -> Operator
max :: Operator -> Operator -> Operator
$cmin :: Operator -> Operator -> Operator
min :: Operator -> Operator -> 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
$cfrom :: forall x. Operator -> Rep Operator x
from :: forall x. Operator -> Rep Operator x
$cto :: forall x. Rep Operator x -> Operator
to :: forall x. Rep Operator x -> Operator
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
Shl     ) = String
"shl"     
  show (Operator
Shr     ) = String
"shr"     
  show (Operator
Sar     ) = String
"sar"     
  show (Operator
Ror     ) = String
"ror"     
  show (Operator
Rol     ) = String
"rol"
  show (Operator
Sbb     ) = String
"sbb"
  show (Operator
Adc     ) = String
"adc"
  show (Operator
Bswap   ) = String
"bswap"
  show (Operator
Pextr   ) = String
"pextr"
  show (Operator
Cmov    ) = String
"cmov"

  show (Operator
ZeroOne ) = String
"setxx"
  show (SExtHi Int
b) = String
"sext_h"
  show (Operator
IMulLo  ) = String
"imul_l"    
  show (Operator
IMulHi  ) = String
"imul_h" 
  show (Operator
Udiv    ) = String
"udiv"    
  show (Operator
UdivLo  ) = String
"udiv_l"    
  show (Operator
UdivHi  ) = String
"udiv_h"    
  show (Operator
Sdiv    ) = String
"sdiv"
  show (Operator
SdivLo  ) = String
"sdiv_l" 
  show (Operator
SdivHi  ) = String
"sdiv_h"    

-- | 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 (Maybe String)      -- ^ 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
$c== :: SimpleExpr -> SimpleExpr -> Bool
== :: SimpleExpr -> SimpleExpr -> Bool
$c/= :: SimpleExpr -> SimpleExpr -> Bool
/= :: 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
$ccompare :: SimpleExpr -> SimpleExpr -> Ordering
compare :: SimpleExpr -> SimpleExpr -> Ordering
$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
>= :: SimpleExpr -> SimpleExpr -> Bool
$cmax :: SimpleExpr -> SimpleExpr -> SimpleExpr
max :: SimpleExpr -> SimpleExpr -> SimpleExpr
$cmin :: SimpleExpr -> SimpleExpr -> SimpleExpr
min :: SimpleExpr -> SimpleExpr -> 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
$cfrom :: forall x. SimpleExpr -> Rep SimpleExpr x
from :: forall x. SimpleExpr -> Rep SimpleExpr x
$cto :: forall x. Rep SimpleExpr x -> SimpleExpr
to :: forall x. Rep SimpleExpr x -> SimpleExpr
Generic)

-- | A statepart is either a register or a region in memory
data StatePart =
    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
$c== :: StatePart -> StatePart -> Bool
== :: StatePart -> StatePart -> Bool
$c/= :: StatePart -> StatePart -> Bool
/= :: 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
$ccompare :: StatePart -> StatePart -> Ordering
compare :: StatePart -> StatePart -> Ordering
$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
>= :: StatePart -> StatePart -> Bool
$cmax :: StatePart -> StatePart -> StatePart
max :: StatePart -> StatePart -> StatePart
$cmin :: StatePart -> StatePart -> StatePart
min :: StatePart -> StatePart -> 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
$cfrom :: forall x. StatePart -> Rep StatePart x
from :: forall x. StatePart -> Rep StatePart x
$cto :: forall x. Rep StatePart x -> StatePart
to :: forall x. Rep StatePart x -> StatePart
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 (BotSrc
Src_StackPointer)         = String
"RSP"
  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 => 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
RockBottom)             = String
"TOP"
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
a) Maybe String
Nothing)    = String
"malloc@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"()" 
show_expr NESet BotSrc -> String
show_srcs (SE_Malloc (Just Word64
a) (Just String
id))  = String
id String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
a
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 => 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 Maybe String
Nothing)       = StatePart -> String
forall a. Show a => a -> String
show StatePart
sp
show_expr NESet BotSrc -> String
show_srcs (SE_StatePart StatePart
sp (Just String
id))     = (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]
++ String
id
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_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_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 Maybe String
_ ) = 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_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 Maybe String
_)  = (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_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 Maybe String
_)  = 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 a. Num a => [a] -> a
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_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 a. Num a => NESet a -> a
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




-- | 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 -> SimpleExpr
reorder_addends 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))      
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l    = SimpleExpr -> SimpleExpr
simp' SimpleExpr
e
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
h    = 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
  | Bool
otherwise = 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
Times Int
si0 [SE_Immediate Word64
1, SimpleExpr
e1]) = SimpleExpr
e1
simp' (SE_Op Operator
Times Int
si0 [SimpleExpr
e0, SE_Immediate Word64
1]) = SimpleExpr
e0
simp' (SE_Op Operator
Udiv  Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Sdiv  Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Shl   Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Shr   Int
si0 [SE_Immediate Word64
0, SimpleExpr
e1]) = Word64 -> SimpleExpr
SE_Immediate Word64
0
simp' (SE_Op Operator
Sar   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 -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
i SimpleExpr
e


simp' (SE_Op Operator
Shl Int
si0   [SimpleExpr
e,SE_Immediate Word64
i]) = SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si0 [SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
2Word64 -> Word64 -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Word64
i]

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
Sdiv  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
Sdiv  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_Op Operator
Shl   Int
si0 [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Int -> Word64
forall a. Bits a => a -> Int -> a
`shiftL` Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1)
simp' (SE_Op Operator
Shr   Int
si0 [SE_Immediate Word64
i0, SE_Immediate Word64
i1]) = Word64 -> SimpleExpr
SE_Immediate (Word64
i0 Word64 -> Int -> Word64
forall a. Bits a => a -> Int -> a
`shiftR` Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1)
simp' (SE_Op Operator
Sar   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 (Int64 -> Word64) -> Int64 -> Word64
forall a b. (a -> b) -> a -> b
$ (Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0::Int64) Int64 -> Int -> Int64
forall a. Bits a => a -> Int -> a
`shiftR` (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1))
simp' (SE_Op Operator
Sar   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 (Int32 -> Word64) -> Int32 -> Word64
forall a b. (a -> b) -> a -> b
$ (Word64 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i0::Int32) Int32 -> Int -> Int32
forall a. Bits a => a -> Int -> a
`shiftR` (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i1))



simp' e :: SimpleExpr
e@(SE_Bit Int
64  e1 :: SimpleExpr
e1@(SE_Malloc Maybe Word64
_ Maybe String
_))                = SimpleExpr
e1
simp' e :: SimpleExpr
e@(SE_Bit Int
si0 e1 :: SimpleExpr
e1@(SE_StatePart (SP_Reg Register
r) Maybe String
_))    = if ByteSize -> Int
byteSize (Register -> ByteSize
regSize Register
r) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si0 then SimpleExpr
e1 else SimpleExpr
e
simp' e :: SimpleExpr
e@(SE_Bit Int
si0 e1 :: SimpleExpr
e1@(SE_StatePart (SP_Mem SimpleExpr
_ Int
si) Maybe String
_)) = if Int
siInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si0 then SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1 else Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
si0 (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1
simp' e :: SimpleExpr
e@(SE_Bit Int
si0 e1 :: SimpleExpr
e1@(SE_Var (SP_Reg Register
r)))            = if ByteSize -> Int
byteSize (Register -> ByteSize
regSize Register
r) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si0 then SimpleExpr
e1 else SimpleExpr
e
simp' e :: SimpleExpr
e@(SE_Bit Int
si0 e1 :: SimpleExpr
e1@(SE_Var (SP_Mem SimpleExpr
_ Int
si)))         = if Int
siInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si0 then SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1 else Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
si0 (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1
simp' e :: SimpleExpr
e@(SE_Bit Int
si0 e1 :: SimpleExpr
e1@(SE_Op (SExtHi Int
b) Int
_ [SimpleExpr
_]))       = if Int
bInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
si0 then SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1 else Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
si0 (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp' SimpleExpr
e1


simp' (SE_Op Operator
SdivLo Int
si0 es :: [SimpleExpr]
es@[SE_Op (SExtHi Int
b) Int
_ [SimpleExpr
e0], SimpleExpr
e1,SimpleExpr
e2]) = if SimpleExpr
e0SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
==SimpleExpr
e1 then SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Sdiv Int
si0 [SimpleExpr
e0,SimpleExpr
e2] else Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
SdivLo 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_Bit Int
128 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate Word64
i
simp' (SE_Bit Int
64  (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64
i Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
0xFFFFFFFFFFFFFFFF)
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 {a}. (Bits a, Num a) => a -> a
sextend_32_64 Word64
i)
simp' (SE_SExtend Int
16 Int
64 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64 -> Word64
forall {a}. (Bits a, Num a) => a -> a
sextend_16_64 Word64
i)
simp' (SE_SExtend Int
8  Int
64 (SE_Immediate Word64
i)) = Word64 -> SimpleExpr
SE_Immediate (Word64 -> Word64
forall {a}. (Bits a, Num a) => a -> a
sextend_8_64 Word64
i)

--simp' (SE_Op Minus si0 [SE_Immediate i0, SE_Op Minus _ [e1, SE_Immediate i1]]) = simp' $ SE_Op Minus si0 [SE_Immediate (i0+i1), e1] -- i0-(e1-i1) ==> (i0+i1)-e1
--simp' (SE_Op Minus si0 [SE_Immediate i0, SE_Op Plus  _ [e1, SE_Immediate i1]]) = simp' $ SE_Op Minus si0 [SE_Immediate (i0-i1), e1] -- i0-(e1+i1) ==> (i0-i1)-e1
--simp' (SE_Op Minus si0 [SE_Immediate i0, SE_Op Plus  _ [SE_Immediate i1, e1]]) = simp' $ SE_Op Minus si0 [SE_Immediate (i0-i1), e1] -- i0-(i1+e1) ==> (i0-i1)-e1
--simp' (SE_Op Plus  si0 [SE_Immediate i0, SE_Op Minus _ [e1, SE_Immediate i1]]) = simp' $ SE_Op Plus  si0 [e1, SE_Immediate (i0-i1)] -- i0+(e1-i1) ==> e1+(i0-i1)
--simp' (SE_Op Plus  si0 [SE_Immediate i0, SE_Op Plus  _ [e1, SE_Immediate i1]]) = simp' $ SE_Op Plus  si0 [e1, SE_Immediate (i0+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
Times Int
si0 [SE_Op Operator
Times Int
si1 [SimpleExpr
e1, SE_Immediate Word64
i1],SE_Immediate Word64
i0]) = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si0 [SimpleExpr
e1,Word64 -> SimpleExpr
SE_Immediate (Word64
i0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
*Word64
i1)]    -- (e1*i1)*i0 = e1*(i0*i1)



--simp' (SE_Op Plus  si0 es@[SE_Op Times _ [e0, SE_Immediate i0], SE_Op Times _ [e1, SE_Immediate i1]])
--  | e0 == e1  = SE_Op Times si0 [simp' e0, SE_Immediate (i0+i1)]                                                                        -- a*i0+a*i1 = a*(i0+i1)
--  | otherwise = SE_Op Plus si0 $ map simp' es
--simp' (SE_Op Minus si0 es@[e0,SE_Op Minus _ [e1, e2]])
--  | e0 == e1  = simp' e2                                                                                                                -- a-(a-b) = b
--  | otherwise = SE_Op Minus si0 $ map simp' es
--simp' (SE_Op Minus si0 es@[e0,SE_Op Plus _ [e1, e2]])
--  | e0 == e1  = simp' $ SE_Op Minus si0 [SE_Immediate 0,e2]                                                                             -- a-(a+b) = -b
--  | otherwise = SE_Op Minus si0 $ map simp' es


--simp' (SE_Op Plus  si0 [e0,e1]) = if e0 == e1 then simp' $ SE_Op Times si0 [e0,SE_Immediate 2] else SE_Op Plus si0 $ map simp' [e0,e1]  -- a + a   = a*2
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 Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
e0) 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]                                -- a xor a = 0
--simp' (SE_Op Minus si0 [e0,e1]) = if e0 == e1 then SE_Immediate 0 else SE_Op Minus si0 $ map simp' [e0,e1]                              -- a - a   = 0




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 Maybe String
id)             = StatePart -> Maybe String -> SimpleExpr
SE_StatePart (StatePart -> StatePart
simp'_sp StatePart
sp) Maybe String
id
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




addends :: SimpleExpr -> M.Map SimpleExpr Word64
addends :: SimpleExpr -> Map SimpleExpr Word64
addends = Map SimpleExpr Word64 -> Map SimpleExpr Word64
gather_immediates (Map SimpleExpr Word64 -> Map SimpleExpr Word64)
-> (SimpleExpr -> Map SimpleExpr Word64)
-> SimpleExpr
-> Map SimpleExpr Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> Map SimpleExpr Word64
addends'
 where
  addends' :: SimpleExpr -> Map SimpleExpr Word64
addends' (SE_Op Operator
Plus  Int
_ [SimpleExpr]
es)                   = (Word64 -> Word64 -> Word64)
-> [Map SimpleExpr Word64] -> Map SimpleExpr Word64
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) ([Map SimpleExpr Word64] -> Map SimpleExpr Word64)
-> [Map SimpleExpr Word64] -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Map SimpleExpr Word64)
-> [SimpleExpr] -> [Map SimpleExpr Word64]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Map SimpleExpr Word64
addends' [SimpleExpr]
es
  addends' (SE_Op Operator
Minus Int
_ (SimpleExpr
e0:[SimpleExpr]
es))              = (Word64 -> Word64 -> Word64)
-> [Map SimpleExpr Word64] -> Map SimpleExpr Word64
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) [SimpleExpr -> Map SimpleExpr Word64
addends' SimpleExpr
e0,  (Word64 -> Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\Word64
i -> Word64
0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i) (Map SimpleExpr Word64 -> Map SimpleExpr Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ (Word64 -> Word64 -> Word64)
-> [Map SimpleExpr Word64] -> Map SimpleExpr Word64
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) ([Map SimpleExpr Word64] -> Map SimpleExpr Word64)
-> [Map SimpleExpr Word64] -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Map SimpleExpr Word64)
-> [SimpleExpr] -> [Map SimpleExpr Word64]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Map SimpleExpr Word64
addends' [SimpleExpr]
es]
  addends' (SE_Op Operator
Times Int
_ [SimpleExpr
e,SE_Immediate Word64
imm]) = SimpleExpr -> Word64 -> Map SimpleExpr Word64
forall k a. k -> a -> Map k a
M.singleton SimpleExpr
e Word64
imm
  addends' (SE_Op Operator
Times Int
_ [SE_Immediate Word64
imm,SimpleExpr
e]) = SimpleExpr -> Word64 -> Map SimpleExpr Word64
forall k a. k -> a -> Map k a
M.singleton SimpleExpr
e Word64
imm
  addends' SimpleExpr
e                                    = SimpleExpr -> Word64 -> Map SimpleExpr Word64
forall k a. k -> a -> Map k a
M.singleton SimpleExpr
e Word64
1

  gather_immediates :: M.Map SimpleExpr Word64 -> M.Map SimpleExpr Word64
  gather_immediates :: Map SimpleExpr Word64 -> Map SimpleExpr Word64
gather_immediates Map SimpleExpr Word64
m =
    let (Map SimpleExpr Word64
imms,Map SimpleExpr Word64
rem) = (SimpleExpr -> Word64 -> Bool)
-> Map SimpleExpr Word64
-> (Map SimpleExpr Word64, Map SimpleExpr Word64)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partitionWithKey SimpleExpr -> Word64 -> Bool
forall {p}. SimpleExpr -> p -> Bool
entry_is_immediate Map SimpleExpr Word64
m in
      if Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
imms then Map SimpleExpr Word64
rem else SimpleExpr
-> Word64 -> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> Word64
gather_imms Map SimpleExpr Word64
imms) Word64
1 Map SimpleExpr Word64
rem

  gather_imms :: M.Map SimpleExpr Word64 -> Word64
  gather_imms :: Map SimpleExpr Word64 -> Word64
gather_imms = (SimpleExpr -> Word64 -> Word64 -> Word64)
-> Word64 -> Map SimpleExpr Word64 -> Word64
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey (\(SE_Immediate Word64
i) Word64
q -> (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) (Word64
iWord64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
*Word64
q))) Word64
0

  entry_is_immediate :: SimpleExpr -> p -> Bool
entry_is_immediate (SE_Immediate Word64
_) p
_ = Bool
True
  entry_is_immediate SimpleExpr
_ p
_ = Bool
False


reorder_addends :: SimpleExpr -> SimpleExpr
reorder_addends :: SimpleExpr -> SimpleExpr
reorder_addends SimpleExpr
e
  | SimpleExpr -> Bool
contains_bot SimpleExpr
e = SimpleExpr
e
  | Bool
otherwise      = 
  let si :: Maybe Int
si        = SimpleExpr -> Maybe Int
get_size SimpleExpr
e
      m :: Map SimpleExpr Word64
m         = (Word64 -> Bool) -> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter    (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Word64
0) (Map SimpleExpr Word64 -> Map SimpleExpr Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Map SimpleExpr Word64
addends SimpleExpr
e
      (Map SimpleExpr Word64
pos,Map SimpleExpr Word64
neg) = (Word64 -> Bool)
-> Map SimpleExpr Word64
-> (Map SimpleExpr Word64, Map SimpleExpr Word64)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition (Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
(<) Word64
0)  (Map SimpleExpr Word64
 -> (Map SimpleExpr Word64, Map SimpleExpr Word64))
-> Map SimpleExpr Word64
-> (Map SimpleExpr Word64, Map SimpleExpr Word64)
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64
m in
    if Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
pos Bool -> Bool -> Bool
&& Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
neg then
      Word64 -> SimpleExpr
SE_Immediate Word64
0
    else if Bool -> Bool
not (Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
pos) Bool -> Bool -> Bool
&& Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
neg then
      SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si ([(SimpleExpr, Word64)] -> SimpleExpr)
-> [(SimpleExpr, Word64)] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall k a. Map k a -> [(k, a)]
M.toList Map SimpleExpr Word64
pos
    else if Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
pos Bool -> Bool -> Bool
&& Bool -> Bool
not (Map SimpleExpr Word64 -> Bool
forall k a. Map k a -> Bool
M.null Map SimpleExpr Word64
neg) then
      SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
si) [Word64 -> SimpleExpr
SE_Immediate Word64
0, Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si ([(SimpleExpr, Word64)] -> SimpleExpr)
-> [(SimpleExpr, Word64)] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall k a. Map k a -> [(k, a)]
M.toList (Map SimpleExpr Word64 -> [(SimpleExpr, Word64)])
-> Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((\Word64
i -> Word64
0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i)) Map SimpleExpr Word64
neg]
    else
      SimpleExpr -> SimpleExpr
simp' (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
si) [Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si ([(SimpleExpr, Word64)] -> SimpleExpr)
-> [(SimpleExpr, Word64)] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall k a. Map k a -> [(k, a)]
M.toList Map SimpleExpr Word64
pos, Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si ([(SimpleExpr, Word64)] -> SimpleExpr)
-> [(SimpleExpr, Word64)] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall k a. Map k a -> [(k, a)]
M.toList (Map SimpleExpr Word64 -> [(SimpleExpr, Word64)])
-> Map SimpleExpr Word64 -> [(SimpleExpr, Word64)]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((\Word64
i -> Word64
0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
i)) Map SimpleExpr Word64
neg]
 where
  mk_expr :: Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si [(SimpleExpr
e,Word64
occ)]     = Maybe Int -> SimpleExpr -> Word64 -> SimpleExpr
mk_addend Maybe Int
si SimpleExpr
e Word64
occ
  mk_expr Maybe Int
si ((SimpleExpr
e,Word64
occ):[(SimpleExpr, Word64)]
rem) = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
si) [Maybe Int -> SimpleExpr -> Word64 -> SimpleExpr
mk_addend Maybe Int
si SimpleExpr
e Word64
occ, Maybe Int -> [(SimpleExpr, Word64)] -> SimpleExpr
mk_expr Maybe Int
si [(SimpleExpr, Word64)]
rem] 

  mk_addend :: Maybe Int -> SimpleExpr -> Word64 -> SimpleExpr
mk_addend Maybe Int
si SimpleExpr
e Word64
occ
    | Word64
occ Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
1 = SimpleExpr
e
    | Word64
occ  Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
si) [SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
occ]

  get_size :: SimpleExpr -> Maybe Int
get_size (SE_Op Operator
Plus Int
si [SimpleExpr]
es)  = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
si
  get_size (SE_Op Operator
Minus Int
si [SimpleExpr]
es) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
si
  get_size (SE_Op Operator
Times Int
si [SimpleExpr]
es) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
si
  get_size SimpleExpr
_                   = Maybe Int
forall a. Maybe a
Nothing



instance Show StatePart where
  show :: StatePart -> String
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) Operand 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
$cfrom :: forall x. FlagStatus -> Rep FlagStatus x
from :: forall x. FlagStatus -> Rep FlagStatus x
$cto :: forall x. Rep FlagStatus x -> FlagStatus
to :: forall x. Rep FlagStatus x -> FlagStatus
Generic,FlagStatus -> FlagStatus -> Bool
(FlagStatus -> FlagStatus -> Bool)
-> (FlagStatus -> FlagStatus -> Bool) -> Eq FlagStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FlagStatus -> FlagStatus -> Bool
== :: FlagStatus -> FlagStatus -> Bool
$c/= :: FlagStatus -> FlagStatus -> Bool
/= :: 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
$ccompare :: FlagStatus -> FlagStatus -> Ordering
compare :: FlagStatus -> FlagStatus -> Ordering
$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
>= :: FlagStatus -> FlagStatus -> Bool
$cmax :: FlagStatus -> FlagStatus -> FlagStatus
max :: FlagStatus -> FlagStatus -> FlagStatus
$cmin :: FlagStatus -> FlagStatus -> FlagStatus
min :: FlagStatus -> FlagStatus -> 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 (PointerBase
StackPointer)        = String
"StackPointer"
  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 => 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 => a -> String
showHex Word64
a
  show PointerBase
ThreadLocalStorage    = String
"ThreadLocalStorage"
  show (BaseIsStatePart StatePart
sp)  = StatePart -> String
forall a. Show a => a -> String
show StatePart
sp




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