{-# LANGUAGE MultiParamTypeClasses, DeriveGeneric, FlexibleInstances, StrictData#-}
module Instantiation.SymbolicPropagation (
get_invariant,
init_pred,
invariant_to_finit,
join_finit,
gather_stateparts
) where
import Base
import Config
import Data.SValue
import Data.JumpTarget
import Data.SymbolicExpression
import Analysis.ControlFlow
import Analysis.Pointers
import Analysis.FunctionNames
import Analysis.Context
import Generic.SymbolicConstituents
import Generic.SymbolicPropagation
import Generic.Binary
import X86.Opcode (Opcode(..), isCondJump, isJump)
import X86.Register
import X86.Conventions
import X86.Instruction (addressof)
import Generic.HasSize (sizeof)
import qualified X86.Instruction as X86
import Generic.Instruction (GenericInstruction(Instruction))
import Generic.Address (AddressWord64(..))
import Generic.Operand
import Control.Monad.State.Strict hiding (join)
import Control.Applicative ((<|>))
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set.NonEmpty as NES
import Data.List
import Data.Word
import Data.Maybe
import Data.Either
import Data.Foldable (toList)
import Data.Bits (testBit, (.|.), (.&.), xor, complement)
import Control.Applicative (liftA2)
import qualified Data.Serialize as Cereal hiding (get,put)
import Control.DeepSeq
import GHC.Generics
import Debug.Trace
traceTop :: p -> a -> a
traceTop p
msg = a -> a
forall a. a -> a
id
mk_top :: [Char] -> SValue
mk_top [Char]
"" = SValue
Top
mk_top [Char]
msg = [Char] -> SValue -> SValue
forall p a. p -> a -> a
traceTop [Char]
msg SValue
Top
ctry_immediate :: SValue -> Maybe Word64
ctry_immediate (SConcrete NESet SimpleExpr
es)
| NESet SimpleExpr -> Int
forall a. NESet a -> Int
NES.size NESet SimpleExpr
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SimpleExpr -> Maybe Word64
try_imm (SimpleExpr -> Maybe Word64) -> SimpleExpr -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
| Bool
otherwise = Maybe Word64
forall a. Maybe a
Nothing
where
try_imm :: SimpleExpr -> Maybe Word64
try_imm (SE_Immediate Word64
i) = Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
i
try_imm SimpleExpr
_ = Maybe Word64
forall a. Maybe a
Nothing
ctry_immediate SValue
_ = Maybe Word64
forall a. Maybe a
Nothing
ctry_deterministic :: SValue -> Maybe SimpleExpr
ctry_deterministic (SConcrete NESet SimpleExpr
es)
| NESet SimpleExpr -> Int
forall a. NESet a -> Int
NES.size NESet SimpleExpr
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SimpleExpr -> Maybe SimpleExpr
try_det (SimpleExpr -> Maybe SimpleExpr) -> SimpleExpr -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
| Bool
otherwise = Maybe SimpleExpr
forall a. Maybe a
Nothing
where
try_det :: SimpleExpr -> Maybe SimpleExpr
try_det SimpleExpr
e
| SimpleExpr -> Bool
contains_bot SimpleExpr
e = Maybe SimpleExpr
forall a. Maybe a
Nothing
| Bool
otherwise = SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just SimpleExpr
e
ctry_deterministic SValue
_ = Maybe SimpleExpr
forall a. Maybe a
Nothing
group_immediates :: FContext -> NES.NESet (S.Set SAddend) -> S.Set (S.Set SAddend)
group_immediates :: FContext -> NESet (Set SAddend) -> Set (Set SAddend)
group_immediates FContext
fctxt NESet (Set SAddend)
addends =
let (Set (Set SAddend)
imms,Set (Set SAddend)
remainder) = (Set SAddend -> Bool)
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition Set SAddend -> Bool
is_imm (Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend)))
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a b. (a -> b) -> a -> b
$ NESet (Set SAddend) -> Set (Set SAddend)
forall a. NESet a -> Set a
NES.toSet NESet (Set SAddend)
addends in
if Set (Set SAddend) -> Bool
forall a. Set a -> Bool
S.null Set (Set SAddend)
imms then
Set (Set SAddend)
remainder
else
Set (Set SAddend) -> Set (Set SAddend) -> Set (Set SAddend)
forall a. Ord a => Set a -> Set a -> Set a
S.union ((Set (Set SAddend) -> Set SAddend)
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set (Set SAddend) -> Set SAddend
merge_imms (Set (Set (Set SAddend)) -> Set (Set SAddend))
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall a b. (a -> b) -> a -> b
$ Set (Set SAddend) -> Set (Set (Set SAddend))
group_imms_by_section Set (Set SAddend)
imms) Set (Set SAddend)
remainder
where
is_imm :: Set SAddend -> Bool
is_imm Set SAddend
bs = Set SAddend -> Int
forall a. Set a -> Int
S.size Set SAddend
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& (SAddend -> Bool) -> Set SAddend -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SAddend -> Bool
isImmediateBase Set SAddend
bs
group_imms_by_section :: S.Set (S.Set SAddend) -> S.Set (S.Set (S.Set SAddend))
group_imms_by_section :: Set (Set SAddend) -> Set (Set (Set SAddend))
group_imms_by_section = (Set SAddend -> Set SAddend -> Bool)
-> Set (Set SAddend) -> Set (Set (Set SAddend))
forall a. Ord a => (a -> a -> Bool) -> Set a -> Set (Set a)
quotientBy Set SAddend -> Set SAddend -> Bool
same_section
same_section :: Set SAddend -> Set SAddend -> Bool
same_section Set SAddend
imms0 Set SAddend
imms1 = Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for (SAddend -> Word64
get_imm (SAddend -> Word64) -> SAddend -> Word64
forall a b. (a -> b) -> a -> b
$ Set SAddend -> SAddend
forall a. Set a -> a
S.findMin Set SAddend
imms0) Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for (SAddend -> Word64
get_imm (SAddend -> Word64) -> SAddend -> Word64
forall a b. (a -> b) -> a -> b
$ Set SAddend -> SAddend
forall a. Set a -> a
S.findMin Set SAddend
imms1)
get_section_for :: Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for Word64
a =
let ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt in
Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_for_address Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_ending_at Context
ctxt Word64
a
merge_imms :: Set (Set SAddend) -> Set SAddend
merge_imms = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend)
-> (Set (Set SAddend) -> SAddend)
-> Set (Set SAddend)
-> Set SAddend
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> SAddend
SAddend_Immediate (Word64 -> SAddend)
-> (Set (Set SAddend) -> Word64) -> Set (Set SAddend) -> SAddend
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Word64 -> Word64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (Set Word64 -> Word64)
-> (Set (Set SAddend) -> Set Word64) -> Set (Set SAddend) -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set SAddend -> Word64) -> Set (Set SAddend) -> Set Word64
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (SAddend -> Word64
get_imm (SAddend -> Word64)
-> (Set SAddend -> SAddend) -> Set SAddend -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SAddend -> SAddend
forall a. Set a -> a
S.findMin)
get_imm :: SAddend -> Word64
get_imm (SAddend_Immediate Word64
imm) = Word64
imm
group_nested_dereferences :: S.Set (S.Set SAddend) -> S.Set (S.Set SAddend)
group_nested_dereferences :: Set (Set SAddend) -> Set (Set SAddend)
group_nested_dereferences Set (Set SAddend)
ptrs =
let (Set (Set SAddend)
derefs,Set (Set SAddend)
remainder) = (Set SAddend -> Bool)
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition Set SAddend -> Bool
is_deref Set (Set SAddend)
ptrs
grouped_derefs :: Set (Set (Set SAddend))
grouped_derefs = (Set SAddend -> Set SAddend -> Bool)
-> Set (Set SAddend) -> Set (Set (Set SAddend))
forall a. Ord a => (a -> a -> Bool) -> Set a -> Set (Set a)
quotientBy Set SAddend -> Set SAddend -> Bool
same_group Set (Set SAddend)
derefs
groups :: Set (Set SAddend)
groups = (Set (Set SAddend) -> Set SAddend)
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set (Set SAddend) -> Set SAddend
do_abstraction Set (Set (Set SAddend))
grouped_derefs in
Set (Set SAddend) -> Set (Set SAddend) -> Set (Set SAddend)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Set SAddend)
groups Set (Set SAddend)
remainder
where
is_deref :: Set SAddend -> Bool
is_deref = (SAddend -> Bool) -> Set SAddend -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SAddend -> Bool
is_deref_base
is_deref_base :: SAddend -> Bool
is_deref_base (SAddend_StatePart (SP_Mem SimpleExpr
_ Int
_)) = Bool
True
is_deref_base SAddend
_ = Bool
False
same_group :: Set SAddend -> Set SAddend -> Bool
same_group Set SAddend
ptr0 Set SAddend
ptr1 = Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr0 Set StatePart -> Set StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr1
do_abstraction :: Set (Set SAddend) -> Set SAddend
do_abstraction Set (Set SAddend)
ptrs =
let ptr :: Set SAddend
ptr = Set (Set SAddend) -> Set SAddend
forall a. Set a -> a
S.findMin Set (Set SAddend)
ptrs
derefs :: Set StatePart
derefs = Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr in
(StatePart -> SAddend) -> Set StatePart -> Set SAddend
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map StatePart -> SAddend
SAddend_StatePart Set StatePart
derefs
get_inner_derefs :: Set SAddend -> Set StatePart
get_inner_derefs = Set (Set StatePart) -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set StatePart) -> Set StatePart)
-> (Set SAddend -> Set (Set StatePart))
-> Set SAddend
-> Set StatePart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SAddend -> Set StatePart) -> Set SAddend -> Set (Set StatePart)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SAddend -> Set StatePart
get_inner_derefs_base
get_inner_derefs_base :: SAddend -> Set StatePart
get_inner_derefs_base b :: SAddend
b@(SAddend_StatePart StatePart
sp) = SimpleExpr -> Set StatePart
inner_derefs (SimpleExpr -> Set StatePart) -> SimpleExpr -> Set StatePart
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
inner_derefs :: SimpleExpr -> Set StatePart
inner_derefs (SE_Var (SP_Mem SimpleExpr
a Int
si)) =
let ds :: Set StatePart
ds = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
a in
if Set StatePart -> Bool
forall a. Set a -> Bool
S.null Set StatePart
ds then StatePart -> Set StatePart
forall a. a -> Set a
S.singleton (StatePart -> Set StatePart) -> StatePart -> Set StatePart
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a Int
si else Set StatePart
ds
inner_derefs e :: SimpleExpr
e@(SE_Op Operator
op Int
si [SimpleExpr]
es) = [Set StatePart] -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set StatePart] -> Set StatePart)
-> [Set StatePart] -> Set StatePart
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set StatePart) -> [SimpleExpr] -> [Set StatePart]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Set StatePart
inner_derefs [SimpleExpr]
es
inner_derefs e :: SimpleExpr
e@(SE_Bit Int
l SimpleExpr
e0) = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
e0
inner_derefs e :: SimpleExpr
e@(SE_SExtend Int
l Int
h SimpleExpr
e0) = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
e0
inner_derefs e :: SimpleExpr
e@(SE_Overwrite Int
h SimpleExpr
e0 SimpleExpr
e1) = [Set StatePart] -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set StatePart] -> Set StatePart)
-> [Set StatePart] -> Set StatePart
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set StatePart) -> [SimpleExpr] -> [Set StatePart]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Set StatePart
inner_derefs [SimpleExpr
e0,SimpleExpr
e1]
inner_derefs SimpleExpr
e = Set StatePart
forall a. Set a
S.empty
mk_concrete :: FContext -> String -> NES.NESet SimpleExpr -> SValue
mk_concrete :: FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
msg = NESet SimpleExpr -> SValue
cap (NESet SimpleExpr -> SValue)
-> (NESet SimpleExpr -> NESet SimpleExpr)
-> NESet SimpleExpr
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr) -> NESet SimpleExpr -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SimpleExpr -> SimpleExpr
simp
where
cap :: NESet SimpleExpr -> SValue
cap NESet SimpleExpr
es
| NESet SimpleExpr -> Int
forall a. NESet a -> Int
NES.size NESet SimpleExpr
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
num_cases =
let es' :: NESet (Set SAddend)
es' = FContext -> [Char] -> NESet SimpleExpr -> NESet (Set SAddend)
forall p. FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt ([Char]
"mk_concrete"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
msg) NESet SimpleExpr
es in
FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt ([Char]
"mk_concrete"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
msg) NESet (Set SAddend)
es'
| Bool
otherwise = NESet SimpleExpr -> SValue
SConcrete NESet SimpleExpr
es
num_cases :: Int
num_cases = Context -> Int
ctxt_max_num_of_cases (FContext -> Context
f_ctxt FContext
fctxt)
mk_concreteS :: FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"mk_concreteS" (NESet SimpleExpr -> SValue)
-> (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton
mk_addends :: FContext -> String -> NES.NESet (S.Set SAddend) -> SValue
mk_addends :: FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt [Char]
msg = Set (Set SAddend) -> SValue
mk (Set (Set SAddend) -> SValue)
-> (NESet (Set SAddend) -> Set (Set SAddend))
-> NESet (Set SAddend)
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set SAddend) -> Set (Set SAddend)
group_nested_dereferences (Set (Set SAddend) -> Set (Set SAddend))
-> (NESet (Set SAddend) -> Set (Set SAddend))
-> NESet (Set SAddend)
-> Set (Set SAddend)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> NESet (Set SAddend) -> Set (Set SAddend)
group_immediates FContext
fctxt
where
mk :: Set (Set SAddend) -> SValue
mk Set (Set SAddend)
addends
| (Set SAddend -> Bool) -> Set (Set SAddend) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Set SAddend -> Bool
forall a. Set a -> Bool
S.null Set (Set SAddend)
addends = [Char] -> SValue
mk_top ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"mk_addends: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Set (Set SAddend) -> [Char]
forall a. Show a => a -> [Char]
show Set (Set SAddend)
addends
| Set (Set SAddend) -> Int
forall a. Set a -> Int
S.size Set (Set SAddend)
addends Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 = [Char] -> SValue
mk_top ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"mk_addends: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Set (Set SAddend) -> [Char]
forall a. Show a => a -> [Char]
show Set (Set SAddend)
addends
| Bool
otherwise = NESet (NESet SAddend) -> SValue
SAddends (NESet (NESet SAddend) -> SValue)
-> NESet (NESet SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ Set (NESet SAddend) -> NESet (NESet SAddend)
forall a. Set a -> NESet a
NES.unsafeFromSet (Set (NESet SAddend) -> NESet (NESet SAddend))
-> Set (NESet SAddend) -> NESet (NESet SAddend)
forall a b. (a -> b) -> a -> b
$ (Set SAddend -> NESet SAddend)
-> Set (Set SAddend) -> Set (NESet SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set SAddend -> NESet SAddend
forall a. Set a -> NESet a
NES.unsafeFromSet Set (Set SAddend)
addends
cimmediate :: Integral i => FContext -> i -> SValue
cimmediate :: FContext -> i -> SValue
cimmediate FContext
fctxt = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"cimmediate" (NESet SimpleExpr -> SValue)
-> (i -> NESet SimpleExpr) -> i -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr)
-> (i -> SimpleExpr) -> i -> NESet SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> (i -> Word64) -> i -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
set_unknown_offset :: p -> [Char] -> SPointer -> SPointer
set_unknown_offset p
fctxt [Char]
msg (Base_StackPointer [Char]
f PtrOffset
offset) = [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_Immediate Word64
a PtrOffset
offset) = Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
a PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_Malloc Maybe Word64
id Maybe [Char]
h PtrOffset
offset) = Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
h PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_FunctionPtr Word64
a [Char]
f PtrOffset
offset) = Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_TLS PtrOffset
offset) = PtrOffset -> SPointer
Base_TLS PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_StatePart StatePart
sp PtrOffset
offset) = StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_FunctionReturn [Char]
f PtrOffset
offset) = [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg SPointer
b = [Char] -> SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> SPointer) -> [Char] -> SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"set_unknown_offset: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show SPointer
b
abstract_addends :: FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt (SE_Op Operator
Plus Int
si [SimpleExpr
e0,SimpleExpr
e1]) = [Set SAddend] -> Set SAddend
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e0,FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e1]
abstract_addends FContext
fctxt (SE_Op Operator
Minus Int
si [SimpleExpr
e0,SimpleExpr
e1]) = FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e0
abstract_addends FContext
fctxt (SE_Var (SP_StackPointer [Char]
f)) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_StackPointer [Char]
f
abstract_addends FContext
fctxt (SE_Immediate Word64
imm)
| FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
imm = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Word64 -> SAddend
SAddend_Immediate Word64
imm
| Bool
otherwise = Set SAddend
forall a. Set a
S.empty
abstract_addends FContext
fctxt (SE_Malloc Maybe Word64
id Maybe [Char]
h) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SAddend
SAddend_Malloc Maybe Word64
id Maybe [Char]
h
abstract_addends FContext
fctxt (SE_Var sp :: StatePart
sp@(SP_Mem (SE_Immediate Word64
a) Int
8)) =
case FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a of
Maybe [Char]
Nothing -> SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ StatePart -> SAddend
SAddend_StatePart StatePart
sp
Just [Char]
f -> SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Word64 -> [Char] -> SAddend
SAddend_FunctionPtr Word64
a [Char]
f
abstract_addends FContext
fctxt (SE_Var (SP_Mem (SE_Var (SP_StackPointer [Char]
f)) Int
8)) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_ReturnAddr [Char]
f
abstract_addends FContext
fctxt (SE_Var (SP_Reg Register
FS)) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ SAddend
SAddend_TLS
abstract_addends FContext
fctxt (SE_Var StatePart
sp) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ StatePart -> SAddend
SAddend_StatePart StatePart
sp
abstract_addends FContext
fctxt (Bottom (FromCall [Char]
f))
| [Char]
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"" = Set SAddend
forall a. Set a
S.empty
| Bool
otherwise = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_FunctionReturn [Char]
f
abstract_addends FContext
fctxt (SE_Bit Int
h SimpleExpr
e) = FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e
abstract_addends FContext
fctxt SimpleExpr
_ = Set SAddend
forall a. Set a
S.empty
widen_exprs :: FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt p
msg NESet SimpleExpr
es = (SimpleExpr -> Set SAddend)
-> NESet SimpleExpr -> NESet (Set SAddend)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt) NESet SimpleExpr
es
cwiden :: FContext -> String -> SValue -> SValue
cwiden :: FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
msg (SConcrete NESet SimpleExpr
es) = FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt ([Char]
"cwiden " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet (Set SAddend) -> SValue) -> NESet (Set SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> NESet SimpleExpr -> NESet (Set SAddend)
forall p. FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt [Char]
msg NESet SimpleExpr
es
cwiden FContext
fctxt [Char]
msg SValue
v = SValue
v
cwiden_all :: FContext -> String -> [SValue] -> SValue
cwiden_all :: FContext -> [Char] -> [SValue] -> SValue
cwiden_all FContext
fctxt [Char]
msg [] = [Char] -> SValue
mk_top ([Char]
"cwiden_all" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg)
cwiden_all FContext
fctxt [Char]
msg (SValue
v:[SValue]
vs) = (SValue -> SValue -> SValue) -> [SValue] -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg) ([SValue] -> SValue) -> [SValue] -> SValue
forall a b. (a -> b) -> a -> b
$ (SValue -> SValue) -> [SValue] -> [SValue]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
msg) (SValue
vSValue -> [SValue] -> [SValue]
forall a. a -> [a] -> [a]
:[SValue]
vs)
cjoin :: FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg SValue
v0 SValue
v1 = SValue -> SValue -> SValue
join SValue
v0 SValue
v1
where
join :: SValue -> SValue -> SValue
join v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> NESet SimpleExpr -> NESet SimpleExpr
forall a. Ord a => NESet a -> NESet a -> NESet a
NES.union NESet SimpleExpr
es0 NESet SimpleExpr
es1
join v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet (Set SAddend) -> SValue) -> NESet (Set SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ (NESet SAddend -> Set SAddend)
-> NESet (NESet SAddend) -> NESet (Set SAddend)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map NESet SAddend -> Set SAddend
forall a. NESet a -> Set a
NES.toSet (NESet (NESet SAddend) -> NESet (Set SAddend))
-> NESet (NESet SAddend) -> NESet (Set SAddend)
forall a b. (a -> b) -> a -> b
$ NESet (NESet SAddend)
-> NESet (NESet SAddend) -> NESet (NESet SAddend)
forall a. Ord a => NESet a -> NESet a -> NESet a
NES.union NESet (NESet SAddend)
es0 NESet (NESet SAddend)
es1
join v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = SValue -> SValue -> SValue
join (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v0) SValue
v1
join v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = SValue -> SValue -> SValue
join SValue
v0 (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v1)
join t :: SValue
t@SValue
Top SValue
_ = SValue
t
join SValue
_ t :: SValue
t@SValue
Top = SValue
t
cjoin_all :: Foldable t => FContext -> String -> t SValue -> SValue
cjoin_all :: FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
msg t SValue
es
| t SValue -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t SValue
es = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot join [], msg = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg
| Bool
otherwise = (SValue -> SValue -> SValue) -> t SValue -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg) t SValue
es
all_equal :: (Eq a) => [a] -> Bool
all_equal :: [a] -> Bool
all_equal [] = Bool
True
all_equal [a]
xs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> a
forall a. [a] -> a
head [a]
xs) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)
cjoin_pointers :: p -> [SPointer] -> [SPointer]
cjoin_pointers p
fctxt [] = []
cjoin_pointers p
fctxt [SPointer
ptr] = [SPointer
ptr]
cjoin_pointers p
fctxt [SPointer]
ptrs
| [SPointer] -> Bool
forall a. Eq a => [a] -> Bool
all_equal [SPointer]
ptrs = [[SPointer] -> SPointer
forall a. [a] -> a
head [SPointer]
ptrs]
| Bool
otherwise =
let ptrs' :: [SPointer]
ptrs' = [SPointer] -> [SPointer]
forall a. Eq a => [a] -> [a]
nub ([SPointer] -> [SPointer]) -> [SPointer] -> [SPointer]
forall a b. (a -> b) -> a -> b
$ (SPointer -> SPointer) -> [SPointer] -> [SPointer]
forall a b. (a -> b) -> [a] -> [b]
map (p -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset p
fctxt [Char]
"cjoin_pointers") [SPointer]
ptrs
([SPointer]
imms,[SPointer]
remainder) = (SPointer -> Bool) -> [SPointer] -> ([SPointer], [SPointer])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition SPointer -> Bool
is_imm [SPointer]
ptrs' in
[SPointer] -> [SPointer]
merge_imms [SPointer]
imms [SPointer] -> [SPointer] -> [SPointer]
forall a. [a] -> [a] -> [a]
++ [SPointer]
remainder
where
is_imm :: SPointer -> Bool
is_imm (Base_Immediate Word64
_ PtrOffset
_) = Bool
True
is_imm SPointer
_ = Bool
False
get_imm :: SPointer -> Word64
get_imm (Base_Immediate Word64
i PtrOffset
_) = Word64
i
merge_imms :: [SPointer] -> [SPointer]
merge_imms [] = []
merge_imms [SPointer]
imms = [(\Word64
i -> Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
i PtrOffset
UnknownOffset) (Word64 -> SPointer) -> Word64 -> SPointer
forall a b. (a -> b) -> a -> b
$ [Word64] -> Word64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Word64] -> Word64) -> [Word64] -> Word64
forall a b. (a -> b) -> a -> b
$ (SPointer -> Word64) -> [SPointer] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map SPointer -> Word64
get_imm [SPointer]
imms]
addends_of :: SimpleExpr -> Set SimpleExpr
addends_of (SE_Op Operator
Plus Int
_ [SimpleExpr]
es) = Set (Set SimpleExpr) -> Set SimpleExpr
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set SimpleExpr) -> Set SimpleExpr)
-> Set (Set SimpleExpr) -> Set SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set SimpleExpr)
-> Set SimpleExpr -> Set (Set SimpleExpr)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Set SimpleExpr
addends_of (Set SimpleExpr -> Set (Set SimpleExpr))
-> Set SimpleExpr -> Set (Set SimpleExpr)
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr]
es
addends_of (SE_Op Operator
Minus Int
_ (SimpleExpr
e:[SimpleExpr]
es)) = SimpleExpr -> Set SimpleExpr
addends_of SimpleExpr
e
addends_of SimpleExpr
e = SimpleExpr -> Set SimpleExpr
forall a. a -> Set a
S.singleton SimpleExpr
e
is_local_expr :: SimpleExpr -> Maybe [Char]
is_local_expr (SE_Var (SP_StackPointer [Char]
f)) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
f
is_local_expr (SE_Op Operator
Plus Int
_ [SimpleExpr
e0,SimpleExpr
e1]) = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e0 Maybe [Char] -> Maybe [Char] -> Maybe [Char]
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e1
is_local_expr (SE_Op Operator
Minus Int
_ [SimpleExpr
e0,SimpleExpr
_]) = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e0
is_local_expr (SE_Op Operator
And Int
_ [SimpleExpr
e,SE_Immediate Word64
mask]) = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e
is_local_expr SimpleExpr
_ = Maybe [Char]
forall a. Maybe a
Nothing
immediate_maybe_a_pointer :: FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
a = Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_for_address Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe ([Char], [Char], Word64, Word64)
forall a. Maybe a
Nothing Bool -> Bool -> Bool
|| Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_ending_at Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe ([Char], [Char], Word64, Word64)
forall a. Maybe a
Nothing Bool -> Bool -> Bool
|| Word64 -> Bool
forall a. Integral a => a -> Bool
has_symbol Word64
a
where
ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
has_symbol :: a -> Bool
has_symbol a
a = (Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt) Maybe Symbol -> Maybe Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Symbol
forall a. Maybe a
Nothing
try_promote_expr :: FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr :: FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Plus Int
si [SE_Immediate Word64
imm,SimpleExpr
e0]) = FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
si [SimpleExpr
e0,Word64 -> SimpleExpr
SE_Immediate Word64
imm])
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Plus Int
si [SimpleExpr
e0,SE_Immediate Word64
imm]) =
case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e0 of
Just b :: SPointer
b@(Base_Immediate Word64
i (PtrOffset Word64
i0)) -> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
imm) Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` (SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" SPointer
b)
Just b :: SPointer
b@(Base_Immediate Word64
i PtrOffset
_) -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
Maybe SPointer
Nothing -> FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
imm)
Maybe SPointer
x -> (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) Word64
imm) (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SPointer
x
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Minus Int
_ [SimpleExpr
e0,SE_Immediate Word64
imm]) =
case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e0 of
Just b :: SPointer
b@(Base_Immediate Word64
i (PtrOffset Word64
i0)) -> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
imm) Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` (SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" SPointer
b)
Just b :: SPointer
b@(Base_Immediate Word64
i PtrOffset
_) -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
Maybe SPointer
x -> (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (\Word64
v -> Word64
v Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
imm) (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SPointer
x
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e =
let promotions :: [(SimpleExpr, Maybe SPointer)]
promotions = (SimpleExpr -> (SimpleExpr, Maybe SPointer))
-> [SimpleExpr] -> [(SimpleExpr, Maybe SPointer)]
forall a b. (a -> b) -> [a] -> [b]
map (\SimpleExpr
a -> (SimpleExpr
a,SimpleExpr -> Maybe SPointer
try_promote_addend SimpleExpr
a)) ([SimpleExpr] -> [(SimpleExpr, Maybe SPointer)])
-> [SimpleExpr] -> [(SimpleExpr, Maybe SPointer)]
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
$ SimpleExpr -> Set SimpleExpr
addends_of SimpleExpr
e
bases :: [(SimpleExpr, Maybe SPointer)]
bases = ((SimpleExpr, Maybe SPointer) -> Bool)
-> [(SimpleExpr, Maybe SPointer)] -> [(SimpleExpr, Maybe SPointer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SimpleExpr
_,Maybe SPointer
p) -> Maybe SPointer
p Maybe SPointer -> Maybe SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe SPointer
forall a. Maybe a
Nothing) [(SimpleExpr, Maybe SPointer)]
promotions in
case [(SimpleExpr, Maybe SPointer)]
bases of
[] -> Maybe SPointer
forall a. Maybe a
Nothing
[(SimpleExpr
e',Just SPointer
b)] -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool -> SPointer
mk_offset SPointer
b (SimpleExpr
e'SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
==SimpleExpr
e)
[(SimpleExpr, Maybe SPointer)]
bases -> case ((SimpleExpr, Maybe SPointer) -> Bool)
-> [(SimpleExpr, Maybe SPointer)] -> [(SimpleExpr, Maybe SPointer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe SPointer -> Bool
real_base (Maybe SPointer -> Bool)
-> ((SimpleExpr, Maybe SPointer) -> Maybe SPointer)
-> (SimpleExpr, Maybe SPointer)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr, Maybe SPointer) -> Maybe SPointer
forall a b. (a, b) -> b
snd) [(SimpleExpr, Maybe SPointer)]
bases of
[(SimpleExpr
_,Just SPointer
b)] -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool -> SPointer
mk_offset SPointer
b Bool
False
[(SimpleExpr, Maybe SPointer)]
_ -> Maybe SPointer
forall a. Maybe a
Nothing
where
mk_offset :: SPointer -> Bool -> SPointer
mk_offset SPointer
b Bool
True = SPointer
b
mk_offset SPointer
b Bool
False = FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"mk_offset" SPointer
b
try_promote_addend :: SimpleExpr -> Maybe SPointer
try_promote_addend (SE_Var (SP_StackPointer [Char]
f)) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
try_promote_addend (SE_Immediate Word64
imm)
| FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
imm = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
imm (Word64 -> PtrOffset
PtrOffset Word64
0)
| Bool
otherwise = Maybe SPointer
forall a. Maybe a
Nothing
try_promote_addend (SE_Malloc Maybe Word64
id Maybe [Char]
hash) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
hash (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
try_promote_addend (SE_Var sp :: StatePart
sp@(SP_Mem (SE_Immediate Word64
a) Int
8)) =
case (\[Char]
f -> Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0) ([Char] -> SPointer) -> Maybe [Char] -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a of
Maybe SPointer
Nothing -> if Bool
strict then Maybe SPointer
forall a. Maybe a
Nothing else SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
Just SPointer
p -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
p
try_promote_addend (SE_Var (SP_Reg Register
FS)) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ PtrOffset -> SPointer
Base_TLS (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
try_promote_addend e :: SimpleExpr
e@(SE_Var StatePart
sp)
| Bool -> Bool
not Bool
strict = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
| FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt SimpleExpr
e = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
| Bool
otherwise = Maybe SPointer
forall a. Maybe a
Nothing
try_promote_addend (Bottom (FromCall [Char]
f))
| Bool -> Bool
not Bool
strict Bool -> Bool -> Bool
&& [Char]
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"" = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
| Bool
otherwise = Maybe SPointer
forall a. Maybe a
Nothing
try_promote_addend SimpleExpr
e = Maybe SPointer
forall a. Maybe a
Nothing
real_base :: Maybe SPointer -> Bool
real_base (Just (Base_StatePart StatePart
_ PtrOffset
_)) = Bool
False
real_base Maybe SPointer
_ = Bool
True
possible_pointer_addend :: FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt (SE_Var StatePart
sp) = StatePart
sp StatePart -> Set StatePart -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` (((StatePart, Maybe SValue) -> StatePart)
-> Set (StatePart, Maybe SValue) -> Set StatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (StatePart, Maybe SValue) -> StatePart
forall a b. (a, b) -> a
fst Set (StatePart, Maybe SValue)
sps)
where
FInit Set (StatePart, Maybe SValue)
sps Map (SStatePart, SStatePart) MemRelation
_ = FContext -> FInit
f_init FContext
fctxt
possible_pointer_addend FContext
_ SimpleExpr
_ = Bool
False
cmk_mem_addresses :: FContext -> String -> SValue -> S.Set SPointer
cmk_mem_addresses :: FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt [Char]
msg v :: SValue
v@(SConcrete NESet SimpleExpr
es) =
let as :: Set (Maybe SPointer)
as = (SimpleExpr -> Maybe SPointer)
-> Set SimpleExpr -> Set (Maybe SPointer)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Maybe SPointer
mk (Set SimpleExpr -> Set (Maybe SPointer))
-> Set SimpleExpr -> Set (Maybe SPointer)
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es in
if Maybe SPointer
forall a. Maybe a
Nothing Maybe SPointer -> Set (Maybe SPointer) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Maybe SPointer)
as then
FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt [Char]
msg (SValue -> Set SPointer) -> SValue -> Set SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cmk_mem_addresses of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v
else
(Maybe SPointer -> SPointer)
-> Set (Maybe SPointer) -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe SPointer -> SPointer
forall a. HasCallStack => Maybe a -> a
fromJust Set (Maybe SPointer)
as
where
mk :: SimpleExpr -> Maybe SPointer
mk SimpleExpr
e = FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` SimpleExpr -> Maybe SPointer
try_local SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
e
try_local :: SimpleExpr -> Maybe SPointer
try_local SimpleExpr
e = (\[Char]
f -> [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f PtrOffset
UnknownOffset) ([Char] -> SPointer) -> Maybe [Char] -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e
cmk_mem_addresses FContext
fctxt [Char]
msg v :: SValue
v@(SAddends NESet (NESet SAddend)
adds) = (NESet SAddend -> Maybe SPointer)
-> Set (NESet SAddend) -> Set SPointer
forall b a. Ord b => (a -> Maybe b) -> Set a -> Set b
mapMaybeS NESet SAddend -> Maybe SPointer
mk (Set (NESet SAddend) -> Set SPointer)
-> Set (NESet SAddend) -> Set SPointer
forall a b. (a -> b) -> a -> b
$ NESet (NESet SAddend) -> Set (NESet SAddend)
forall a. NESet a -> Set a
NES.toSet NESet (NESet SAddend)
adds
where
mk :: NESet SAddend -> Maybe SPointer
mk NESet SAddend
adds =
let ptrs :: NESet SPointer
ptrs = (SAddend -> SPointer) -> NESet SAddend -> NESet SPointer
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SAddend -> SPointer
saddend_to_spointer NESet SAddend
adds
(Set SPointer
strict,Set SPointer
nonstrict) = (SPointer -> Bool) -> Set SPointer -> (Set SPointer, Set SPointer)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition SPointer -> Bool
is_strict (Set SPointer -> (Set SPointer, Set SPointer))
-> Set SPointer -> (Set SPointer, Set SPointer)
forall a b. (a -> b) -> a -> b
$ NESet SPointer -> Set SPointer
forall a. NESet a -> Set a
NES.toSet NESet SPointer
ptrs in
if Set SPointer -> Bool
forall a. Set a -> Bool
S.null Set SPointer
strict Bool -> Bool -> Bool
&& Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
nonstrict Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt ([Char]
"cmk_mem_addresses (1) of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (SPointer -> SPointer) -> SPointer -> SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
nonstrict
else if Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
strict Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt ([Char]
"cmk_mem_addresses (2) of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (SPointer -> SPointer) -> SPointer -> SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
strict
else
[Char] -> Maybe SPointer -> Maybe SPointer
forall p a. p -> a -> a
traceTop ([Char]
"cmk_mem_addresses of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Set SPointer, Set SPointer) -> [Char]
forall a. Show a => a -> [Char]
show (Set SPointer
strict,Set SPointer
nonstrict)) Maybe SPointer
forall a. Maybe a
Nothing
is_strict :: SPointer -> Bool
is_strict (Base_StatePart StatePart
sp PtrOffset
_) = FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt (StatePart -> SimpleExpr
SE_Var StatePart
sp)
is_strict (Base_FunctionReturn [Char]
f PtrOffset
_) = Bool
False
is_strict SPointer
_ = Bool
True
cmk_mem_addresses FContext
fctxt [Char]
msg t :: SValue
t@SValue
Top = Set SPointer
forall a. Set a
S.empty
saddend_to_spointer :: SAddend -> SPointer
saddend_to_spointer (SAddend_StackPointer [Char]
f) = [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_Immediate Word64
i) = Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
i (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_Malloc Maybe Word64
id Maybe [Char]
h) = Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
h (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_FunctionPtr Word64
a [Char]
f) = Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_ReturnAddr [Char]
f) = [Char] -> SPointer
Base_ReturnAddr [Char]
f
saddend_to_spointer (SAddend
SAddend_TLS) = PtrOffset -> SPointer
Base_TLS (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_StatePart StatePart
sp) = StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_FunctionReturn [Char]
f) = [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
mk_expr :: FContext -> SimpleExpr -> SimpleExpr
mk_expr :: FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt SimpleExpr
e = SimpleExpr -> SimpleExpr
trim_expr (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp SimpleExpr
e
where
trim_expr :: SimpleExpr -> SimpleExpr
trim_expr SimpleExpr
e
| SimpleExpr -> Int
expr_size SimpleExpr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
get_max_expr_size = [Char] -> SimpleExpr
forall a. HasCallStack => [Char] -> a
error ([Char] -> SimpleExpr) -> [Char] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> [Char]
forall a. Show a => a -> [Char]
show SimpleExpr
e
| Bool
otherwise = SimpleExpr
e
get_max_expr_size :: Int
get_max_expr_size = Context -> Int
ctxt_max_expr_size (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt
svalue_plus :: FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"plus1" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
where
f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
"plus2" SValue
v0 SValue
v1
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"plus" SValue
v0) SValue
v1
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
v0
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) SValue
Top = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"plus5" SValue
v0
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) SValue
Top = SValue
v0
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
t
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
t
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top SValue
Top = SValue
t
svalue_minus :: FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"minus" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
where
f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1) = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"minus" SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) SValue
Top = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"minus" SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) SValue
Top = SValue
v0
svalue_minus FContext
fctxt Int
si t :: SValue
t@SValue
Top SValue
_ = SValue
t
svalue_and :: FContext -> Int -> SValue -> SValue -> SValue
svalue_and FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"and" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
where
f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
And Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_and FContext
fctxt Int
si SValue
v0 SValue
v1 = [Char] -> SValue
mk_top ([Char]
"svalue_and" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SValue, SValue) -> [Char]
forall a. Show a => a -> [Char]
show (SValue
v0,SValue
v1))
svalue_unop :: FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
msg (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
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 (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> SimpleExpr
f) NESet SimpleExpr
es0
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0) = [Char] -> SValue
mk_top ([Char]
"unop" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg)
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@SValue
Top = SValue
v0
svalue_takebits :: FContext -> Int -> SValue -> SValue
svalue_takebits FContext
fctxt Int
h = FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
"takebits" (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
h)
svalue_sextend :: FContext -> Int -> Int -> SValue -> SValue
svalue_sextend FContext
fctxt Int
l Int
h = FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
"sextend" (Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h)
apply_expr_op :: FContext -> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op :: FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
msg [SimpleExpr] -> SimpleExpr
f [SValue]
vs
| (SValue -> Bool) -> [SValue] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SValue -> Bool
isImmediate [SValue]
vs =
let es' :: SimpleExpr
es' = [SimpleExpr] -> SimpleExpr
f ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SValue -> SimpleExpr) -> [SValue] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr)
-> (SValue -> Word64) -> SValue -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Word64 -> Word64
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Word64 -> Word64)
-> (SValue -> Maybe Word64) -> SValue -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SValue -> Maybe Word64
ctry_immediate) [SValue]
vs in
FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt SimpleExpr
es'
| SValue
Top SValue -> [SValue] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SValue]
vs = [Char] -> SValue
mk_top [Char]
""
| Bool
otherwise = [Char] -> SValue
mk_top ([Char]
"Making top from: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SValue] -> [Char]
forall a. Show a => a -> [Char]
show [SValue]
vs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"(msg == " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")")
where
isImmediate :: SValue -> Bool
isImmediate SValue
v = SValue -> Maybe Word64
ctry_immediate SValue
v Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Word64
forall a. Maybe a
Nothing
data CSemantics = ApplyPlus Int | ApplyMinus Int | ApplyNeg Int | ApplyDec Int | ApplyInc Int | ApplyAnd Int |
ApplyMov | ApplyCMov | ApplySExtend Int Int |
Apply ([SimpleExpr] -> SimpleExpr) | SetXX | SExtension_HI | NoSemantics
csemantics :: FContext -> String -> SymbolicOperation SValue -> SValue
csemantics :: FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
msg (SO_Plus SValue
a SValue
b) = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
64 SValue
a SValue
b
csemantics FContext
fctxt [Char]
msg (SO_Minus SValue
a SValue
b) = FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
64 SValue
a SValue
b
csemantics FContext
fctxt [Char]
msg (SO_Times SValue
a SValue
b) = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"times" (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
64) [SValue
a,SValue
b]
csemantics FContext
fctxt [Char]
msg (SO_Overwrite Int
n SValue
a SValue
b) = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"overwrite" (\[SimpleExpr
e0,SimpleExpr
e1] -> FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
n SimpleExpr
e0 SimpleExpr
e1) [SValue
a,SValue
b]
csemantics FContext
fctxt [Char]
msg (SO_SExtend Int
l Int
h SValue
a) = FContext -> Int -> Int -> SValue -> SValue
svalue_sextend FContext
fctxt Int
l Int
h SValue
a
csemantics FContext
fctxt [Char]
msg (SO_Bit Int
h SValue
a) = FContext -> Int -> SValue -> SValue
svalue_takebits FContext
fctxt Int
h SValue
a
csemantics FContext
fctxt [Char]
msg (SO_Op Opcode
op Int
si Maybe Int
si' [SValue]
es) =
case Opcode -> Int -> Maybe Int -> CSemantics
mnemonic_to_semantics Opcode
op (Int
8Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
si) ((Int -> Int -> Int
forall a. Num a => a -> a -> a
(*) Int
8) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
si') of
CSemantics
ApplyMov -> [SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0
CSemantics
ApplyCMov -> FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
"cmov" ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
ApplyPlus Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
ApplyInc Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
1)
ApplyMinus Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
ApplyDec Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
1)
ApplyNeg Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0)
ApplyAnd Int
si -> FContext -> Int -> SValue -> SValue -> SValue
svalue_and FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
ApplySExtend Int
l Int
h -> FContext -> Int -> Int -> SValue -> SValue
svalue_sextend FContext
fctxt Int
l Int
h ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0)
Apply [SimpleExpr] -> SimpleExpr
sop -> FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", op = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Opcode -> [Char]
forall a. Show a => a -> [Char]
show Opcode
op) (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleExpr] -> SimpleExpr
sop) [SValue]
es
CSemantics
SetXX -> FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"setxx" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList [Word64 -> SimpleExpr
SE_Immediate Word64
0,Word64 -> SimpleExpr
SE_Immediate Word64
1]
CSemantics
SExtension_HI -> FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"sextend" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList [Word64 -> SimpleExpr
SE_Immediate Word64
0,Word64 -> SimpleExpr
SE_Immediate Word64
18446744073709551615]
CSemantics
NoSemantics -> [Char] -> SValue
mk_top ([Char]
"Widening due to operand: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Opcode -> [Char]
forall a. Show a => a -> [Char]
show Opcode
op)
mnemonic_to_semantics :: Opcode -> Int -> Maybe Int -> CSemantics
mnemonic_to_semantics Opcode
SUB Int
si Maybe Int
si' = Int -> CSemantics
ApplyMinus Int
si
mnemonic_to_semantics Opcode
NEG Int
si Maybe Int
si' = Int -> CSemantics
ApplyNeg Int
si
mnemonic_to_semantics Opcode
DEC Int
si Maybe Int
si' = Int -> CSemantics
ApplyDec Int
si
mnemonic_to_semantics Opcode
ADD Int
si Maybe Int
si' = Int -> CSemantics
ApplyPlus Int
si
mnemonic_to_semantics Opcode
INC Int
si Maybe Int
si' = Int -> CSemantics
ApplyInc Int
si
mnemonic_to_semantics Opcode
XADD Int
si Maybe Int
si' = [Char] -> CSemantics
forall a. HasCallStack => [Char] -> a
error ([Char] -> CSemantics) -> [Char] -> CSemantics
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: XADD"
mnemonic_to_semantics Opcode
IMUL_LO Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si
mnemonic_to_semantics Opcode
SHL Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
shl
where
shl :: [SimpleExpr] -> SimpleExpr
shl [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si [SimpleExpr
a,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]
shl [SimpleExpr
a,SimpleExpr
b] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Shl Int
si [SimpleExpr
a,SimpleExpr
b]
mnemonic_to_semantics Opcode
IDIV_LO Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Div Int
si
mnemonic_to_semantics Opcode
SAR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
sar
where
sar :: [SimpleExpr] -> SimpleExpr
sar [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Div Int
si [SimpleExpr
a,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]
sar [SimpleExpr
a,SimpleExpr
b] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Sar Int
si [SimpleExpr
a,SimpleExpr
b]
mnemonic_to_semantics Opcode
DIV_LO Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Udiv Int
si
mnemonic_to_semantics Opcode
SHR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
shr
where
shr :: [SimpleExpr] -> SimpleExpr
shr [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Udiv Int
si [SimpleExpr
a,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]
shr [SimpleExpr
a,SimpleExpr
b] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Shr Int
si [SimpleExpr
a,SimpleExpr
b]
mnemonic_to_semantics Opcode
BSR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Bsr Int
si [Word64 -> SimpleExpr
SE_Immediate Word64
0,SimpleExpr
a])
mnemonic_to_semantics Opcode
ROL Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Rol Int
si
mnemonic_to_semantics Opcode
ROR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Ror Int
si
mnemonic_to_semantics Opcode
BSWAP Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Bswap Int
si
mnemonic_to_semantics Opcode
PEXTRB Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])
mnemonic_to_semantics Opcode
PEXTRD Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])
mnemonic_to_semantics Opcode
PEXTRQ Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])
mnemonic_to_semantics Opcode
AND Int
si Maybe Int
si' = Int -> CSemantics
ApplyAnd Int
si
mnemonic_to_semantics Opcode
OR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Or Int
si
mnemonic_to_semantics Opcode
NOT Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Not Int
si [SimpleExpr
a])
mnemonic_to_semantics Opcode
XOR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
PXOR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
VPXOR Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
XORPS Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
XORPD Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
MOV Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVSD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVSS Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVAPS Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVAPD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVUPS Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVUPD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVABS Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVDQU Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVDQA Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVLPD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVQ Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
VMOVD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
VMOVAPD Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
VMOVAPS Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVZX Int
si Maybe Int
si' = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVSX Int
si (Just Int
si') = Int -> Int -> CSemantics
ApplySExtend Int
si' Int
si
mnemonic_to_semantics Opcode
MOVSXD Int
si (Just Int
si') = Int -> Int -> CSemantics
ApplySExtend Int
si' Int
si
mnemonic_to_semantics Opcode
CDQE Int
si (Just Int
si') = Int -> Int -> CSemantics
ApplySExtend Int
si' Int
si
mnemonic_to_semantics Opcode
CWDE Int
si (Just Int
si') = Int -> Int -> CSemantics
ApplySExtend Int
si' Int
si
mnemonic_to_semantics Opcode
CBW Int
si (Just Int
si') = Int -> Int -> CSemantics
ApplySExtend Int
si' Int
si
mnemonic_to_semantics Opcode
CWD Int
si (Just Int
si') = CSemantics
SExtension_HI
mnemonic_to_semantics Opcode
CDQ Int
si (Just Int
si') = CSemantics
SExtension_HI
mnemonic_to_semantics Opcode
CQO Int
si (Just Int
si') = CSemantics
SExtension_HI
mnemonic_to_semantics Opcode
SETO Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNO Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETS Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNS Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETZ Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNZ Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETB Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNAE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETC Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNB Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETAE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNC Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETBE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNA Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETA Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNBE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETL Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNGE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETG Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETGE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNL Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETLE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNG Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNLE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETP Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETPE Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETNP Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
SETPO Int
si Maybe Int
si' = CSemantics
SetXX
mnemonic_to_semantics Opcode
CMOVO Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNO Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVS Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNS Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVZ Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNZ Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVB Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNAE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVC Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNB Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVAE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNC Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVBE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNA Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVA Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNBE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVL Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNGE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVG Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVGE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNL Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVLE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNG Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNLE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVP Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVPE Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVNP Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
CMOVPO Int
si Maybe Int
si' = CSemantics
ApplyCMov
mnemonic_to_semantics Opcode
_ Int
_ Maybe Int
_ = CSemantics
NoSemantics
cflg_semantics :: p
-> p
-> GenericInstruction label Register prefix Opcode annotation
-> FlagStatus
-> FlagStatus
cflg_semantics p
fctxt p
_ i :: GenericInstruction label Register prefix Opcode annotation
i@(Instruction label
label Maybe prefix
prefix Opcode
mnemonic Maybe (GenericOperand Register)
dst [GenericOperand Register]
srcs Maybe annotation
annot) FlagStatus
flgs = Opcode -> FlagStatus
flg Opcode
mnemonic
where
flg :: Opcode -> FlagStatus
flg Opcode
CMP = Maybe Bool
-> GenericOperand Register -> GenericOperand Register -> FlagStatus
FS_CMP Maybe Bool
forall a. Maybe a
Nothing ([GenericOperand Register]
srcs[GenericOperand Register] -> Int -> GenericOperand Register
forall a. [a] -> Int -> a
!!Int
0) ([GenericOperand Register]
srcs[GenericOperand Register] -> Int -> GenericOperand Register
forall a. [a] -> Int -> a
!!Int
1)
flg Opcode
PUSH = FlagStatus
flgs
flg Opcode
POP = FlagStatus
flgs
flg Opcode
LEA = FlagStatus
flgs
flg Opcode
LEAVE = FlagStatus
flgs
flg Opcode
NOP = FlagStatus
flgs
flg Opcode
UD2 = FlagStatus
flgs
flg Opcode
ENDBR64 = FlagStatus
flgs
flg Opcode
HLT = FlagStatus
flgs
flg Opcode
WAIT = FlagStatus
flgs
flg Opcode
MFENCE = FlagStatus
flgs
flg Opcode
CLFLUSH = FlagStatus
flgs
flg Opcode
MOV = FlagStatus
flgs
flg Opcode
MOVSD = FlagStatus
flgs
flg Opcode
MOVSS = FlagStatus
flgs
flg Opcode
MOVAPS = FlagStatus
flgs
flg Opcode
MOVAPD = FlagStatus
flgs
flg Opcode
MOVUPS = FlagStatus
flgs
flg Opcode
MOVUPD = FlagStatus
flgs
flg Opcode
MOVABS = FlagStatus
flgs
flg Opcode
MOVDQU = FlagStatus
flgs
flg Opcode
MOVDQA = FlagStatus
flgs
flg Opcode
MOVLPD = FlagStatus
flgs
flg Opcode
MOVD = FlagStatus
flgs
flg Opcode
VMOVD = FlagStatus
flgs
flg Opcode
VMOVAPD = FlagStatus
flgs
flg Opcode
VMOVAPS = FlagStatus
flgs
flg Opcode
MOVZX = FlagStatus
flgs
flg Opcode
MOVSX = FlagStatus
flgs
flg Opcode
MOVSXD = FlagStatus
flgs
flg Opcode
CMOVO = FlagStatus
flgs
flg Opcode
CMOVNO = FlagStatus
flgs
flg Opcode
CMOVS = FlagStatus
flgs
flg Opcode
CMOVNS = FlagStatus
flgs
flg Opcode
CMOVE = FlagStatus
flgs
flg Opcode
CMOVZ = FlagStatus
flgs
flg Opcode
CMOVNE = FlagStatus
flgs
flg Opcode
CMOVNZ = FlagStatus
flgs
flg Opcode
CMOVB = FlagStatus
flgs
flg Opcode
CMOVNAE = FlagStatus
flgs
flg Opcode
CMOVC = FlagStatus
flgs
flg Opcode
CMOVNB = FlagStatus
flgs
flg Opcode
CMOVAE = FlagStatus
flgs
flg Opcode
CMOVNC = FlagStatus
flgs
flg Opcode
CMOVBE = FlagStatus
flgs
flg Opcode
CMOVNA = FlagStatus
flgs
flg Opcode
CMOVA = FlagStatus
flgs
flg Opcode
CMOVNBE = FlagStatus
flgs
flg Opcode
CMOVL = FlagStatus
flgs
flg Opcode
CMOVNGE = FlagStatus
flgs
flg Opcode
CMOVG = FlagStatus
flgs
flg Opcode
CMOVGE = FlagStatus
flgs
flg Opcode
CMOVNL = FlagStatus
flgs
flg Opcode
CMOVLE = FlagStatus
flgs
flg Opcode
CMOVNG = FlagStatus
flgs
flg Opcode
CMOVNLE = FlagStatus
flgs
flg Opcode
CMOVP = FlagStatus
flgs
flg Opcode
CMOVPE = FlagStatus
flgs
flg Opcode
CMOVNP = FlagStatus
flgs
flg Opcode
CMOVPO = FlagStatus
flgs
flg Opcode
SETO = FlagStatus
flgs
flg Opcode
SETNO = FlagStatus
flgs
flg Opcode
SETS = FlagStatus
flgs
flg Opcode
SETNS = FlagStatus
flgs
flg Opcode
SETE = FlagStatus
flgs
flg Opcode
SETZ = FlagStatus
flgs
flg Opcode
SETNE = FlagStatus
flgs
flg Opcode
SETNZ = FlagStatus
flgs
flg Opcode
SETB = FlagStatus
flgs
flg Opcode
SETNAE = FlagStatus
flgs
flg Opcode
SETC = FlagStatus
flgs
flg Opcode
SETNB = FlagStatus
flgs
flg Opcode
SETAE = FlagStatus
flgs
flg Opcode
SETNC = FlagStatus
flgs
flg Opcode
SETBE = FlagStatus
flgs
flg Opcode
SETNA = FlagStatus
flgs
flg Opcode
SETA = FlagStatus
flgs
flg Opcode
SETNBE = FlagStatus
flgs
flg Opcode
SETL = FlagStatus
flgs
flg Opcode
SETNGE = FlagStatus
flgs
flg Opcode
SETG = FlagStatus
flgs
flg Opcode
SETGE = FlagStatus
flgs
flg Opcode
SETNL = FlagStatus
flgs
flg Opcode
SETLE = FlagStatus
flgs
flg Opcode
SETNG = FlagStatus
flgs
flg Opcode
SETNLE = FlagStatus
flgs
flg Opcode
SETP = FlagStatus
flgs
flg Opcode
SETPE = FlagStatus
flgs
flg Opcode
SETNP = FlagStatus
flgs
flg Opcode
SETPO = FlagStatus
flgs
flg Opcode
CBW = FlagStatus
flgs
flg Opcode
CWDE = FlagStatus
flgs
flg Opcode
CDQE = FlagStatus
flgs
flg Opcode
CWD = FlagStatus
flgs
flg Opcode
CDQ = FlagStatus
flgs
flg Opcode
CQO = FlagStatus
flgs
flg Opcode
XCHG = FlagStatus
flgs
flg Opcode
mnemonic = if Opcode -> Bool
isJump Opcode
mnemonic Bool -> Bool -> Bool
|| Opcode -> Bool
isCondJump Opcode
mnemonic then FlagStatus
flgs else FlagStatus
None
cmk_init_reg_value :: FContext -> Register -> SValue
cmk_init_reg_value :: FContext -> Register -> SValue
cmk_init_reg_value FContext
fctxt = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue)
-> (Register -> SimpleExpr) -> Register -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr)
-> (Register -> StatePart) -> Register -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> StatePart
SP_Reg
offset_to_expr :: PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
UnknownOffset SimpleExpr
e = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
64 [SimpleExpr
e,BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
""]
offset_to_expr (PtrOffset Word64
0) SimpleExpr
e = SimpleExpr
e
offset_to_expr (PtrOffset Word64
i) SimpleExpr
e = SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
64 [SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]
spointer_to_expr :: SPointer -> SimpleExpr
spointer_to_expr (Base_StackPointer [Char]
f PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f
spointer_to_expr (Base_Immediate Word64
i PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
i
spointer_to_expr (Base_Malloc Maybe Word64
id Maybe [Char]
h PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
h
spointer_to_expr (Base_FunctionPtr Word64
a [Char]
f PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8
spointer_to_expr (Base_ReturnAddr [Char]
f) = StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f) Int
8
spointer_to_expr (Base_TLS PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg Register
FS)
spointer_to_expr (Base_StatePart StatePart
sp PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
spointer_to_expr (Base_FunctionReturn [Char]
f PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
f
cmk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue
cmk_init_mem_value :: FContext -> [Char] -> SPointer -> RegionSize -> SValue
cmk_init_mem_value FContext
fctxt [Char]
msg SPointer
a RegionSize
si = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
mk_a (Int -> StatePart) -> Int -> StatePart
forall a b. (a -> b) -> a -> b
$ RegionSize -> Int
forall p. Num p => RegionSize -> p
mk_si RegionSize
si
where
mk_a :: SimpleExpr
mk_a = SPointer -> SimpleExpr
spointer_to_expr SPointer
a
mk_si :: RegionSize -> p
mk_si (Nat Word64
imm) = Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
imm
mk_si RegionSize
_ = p
1
cseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
cseparate :: FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate FContext
fctxt [Char]
msg SPointer
a0 (Nat Word64
si0) SPointer
a1 (Nat Word64
si1) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
[ SPointer -> SPointer -> Bool
separation_based_on_necessity SPointer
a0 SPointer
a1
, FContext
-> [Char] -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
forall p.
FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt [Char]
msg SPointer
a0 Word64
si0 SPointer
a1 Word64
si1]
where
separation_based_on_necessity :: SPointer -> SPointer -> Bool
separation_based_on_necessity SPointer
a0 SPointer
a1 = SimpleExpr -> Word64 -> SimpleExpr -> Word64 -> Bool
forall a.
(Ord a, Num a) =>
SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate_expressions (SPointer -> SimpleExpr
spointer_to_expr SPointer
a0) Word64
si0 (SPointer -> SimpleExpr
spointer_to_expr SPointer
a1) Word64
si1
cseparate FContext
fctxt [Char]
msg SPointer
a0 RegionSize
_ SPointer
a1 RegionSize
_ = FContext
-> [Char] -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
forall p.
FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt [Char]
msg SPointer
a0 (Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
20) SPointer
a1 (Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
20)
mk_sstatepart :: FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt (SP_Reg Register
r) = Register -> SStatePart
SSP_Reg Register
r
mk_sstatepart FContext
fctxt (SP_Mem SimpleExpr
a Int
si) =
case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
a of
Just SPointer
ptr -> SPointer -> Int -> SStatePart
SSP_Mem SPointer
ptr Int
si
Maybe SPointer
Nothing -> [Char] -> SStatePart
forall a. HasCallStack => [Char] -> a
error ([Char] -> SStatePart) -> [Char] -> SStatePart
forall a b. (a -> b) -> a -> b
$ [Char]
"CANNOT PROMOTE: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SimpleExpr, Int) -> [Char]
forall a. Show a => a -> [Char]
show (SimpleExpr
a,Int
si)
separation_of_spointers :: FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt p
msg SPointer
v0 Word64
si0 SPointer
v1 Word64
si1 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ SPointer
v0 SPointer -> SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= SPointer
v1
, SPointer -> SPointer -> Bool
separate_bases SPointer
v0 SPointer
v1 ]
where
separate_bases :: SPointer -> SPointer -> Bool
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_StackPointer [Char]
f1 PtrOffset
_)
| [Char]
f0 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
f1 = Bool
False
| Bool
otherwise = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_Malloc Maybe Word64
_ Maybe [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_TLS PtrOffset
_) = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_StatePart StatePart
_ PtrOffset
_) = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_Immediate Word64
_ PtrOffset
_) = Bool
True
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_Malloc Maybe Word64
id1 Maybe [Char]
h1 PtrOffset
_) = Maybe Word64
id0 Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Word64
id1
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_TLS PtrOffset
_) = Bool
True
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_StatePart StatePart
_ PtrOffset
_) = Bool
True
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_Immediate Word64
_ PtrOffset
_) = Bool
True
separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_FunctionPtr Word64
a1 [Char]
_ PtrOffset
_) = Word64
a0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
a1
separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_TLS PtrOffset
_) = Bool
True
separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_StatePart StatePart
_ PtrOffset
_) = Bool
True
separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_Immediate Word64
i1 PtrOffset
_) = Bool
True
separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_TLS PtrOffset
_) (Base_TLS PtrOffset
_) = Bool
False
separate_bases (Base_TLS PtrOffset
_) (Base_StatePart StatePart
_ PtrOffset
_) = Bool
True
separate_bases (Base_TLS PtrOffset
_) (Base_Immediate Word64
_ PtrOffset
_) = Bool
True
separate_bases (Base_TLS PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_) (Base_StatePart StatePart
sp1 PtrOffset
_) =
case (SStatePart, SStatePart)
-> Map (SStatePart, SStatePart) MemRelation -> Maybe MemRelation
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp0,FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp1) Map (SStatePart, SStatePart) MemRelation
m of
Just MemRelation
Separate -> Bool
True
Maybe MemRelation
_ -> Bool
False
separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_) (Base_Immediate Word64
imm1 PtrOffset
_) =
case ((StatePart, Maybe SValue) -> Bool)
-> Set (StatePart, Maybe SValue) -> Maybe (StatePart, Maybe SValue)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(StatePart
sp',Maybe SValue
_) -> StatePart
sp0 StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== StatePart
sp') Set (StatePart, Maybe SValue)
sps of
Just (StatePart
_,Just SValue
imm) -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen?"
Maybe (StatePart, Maybe SValue)
_ -> Bool
True
separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_Immediate Word64
i0 (PtrOffset Word64
off0)) (Base_Immediate Word64
i1 PtrOffset
UnknownOffset) = Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
off0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
si0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
i1
separate_bases (Base_Immediate Word64
i0 PtrOffset
UnknownOffset) (Base_Immediate Word64
i1 (PtrOffset Word64
off1)) = Word64
i1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
off1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
si1 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
i0
separate_bases (Base_Immediate Word64
i0 PtrOffset
_) (Base_Immediate Word64
i1 PtrOffset
_)
| Context -> Word64 -> Word64 -> Bool
forall a1 a2.
(Integral a1, Integral a2) =>
Context -> a1 -> a2 -> Bool
pointers_from_different_global_section (FContext -> Context
f_ctxt FContext
fctxt) Word64
i0 Word64
i1 = Bool
True
| Word64
i0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
i1 = Bool
False
| Bool
otherwise = Bool
False
separate_bases (Base_Immediate Word64
i0 PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_) = Bool
True
separate_bases (Base_FunctionReturn [Char]
f0 PtrOffset
_ ) (Base_FunctionReturn [Char]
f1 PtrOffset
_) = [Char]
f0[Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/=[Char]
f1
separate_bases (Base_ReturnAddr [Char]
f0) (Base_ReturnAddr [Char]
f1) = [Char]
f0 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
f1
separate_bases (Base_ReturnAddr [Char]
f0) SPointer
_ = Bool
True
separate_bases SPointer
_ (Base_ReturnAddr [Char]
f0) = Bool
True
separate_bases SPointer
b0 SPointer
b1 = SPointer -> SPointer -> Bool
separate_bases SPointer
b1 SPointer
b0
FInit Set (StatePart, Maybe SValue)
sps Map (SStatePart, SStatePart) MemRelation
m = FContext -> FInit
f_init FContext
fctxt
calias :: p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias p
fctxt SPointer
a0 RegionSize
si0 SPointer
a1 RegionSize
si1 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ RegionSize
si0 RegionSize -> RegionSize -> Bool
forall a. Eq a => a -> a -> Bool
/= RegionSize
UnknownSize
, RegionSize
si1 RegionSize -> RegionSize -> Bool
forall a. Eq a => a -> a -> Bool
/= RegionSize
UnknownSize
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool
has_unknown_offset SPointer
a0
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool
has_unknown_offset SPointer
a1
, (SPointer
a0,RegionSize
si0) (SPointer, RegionSize) -> (SPointer, RegionSize) -> Bool
forall a. Eq a => a -> a -> Bool
== (SPointer
a1,RegionSize
si1) ]
cenclosed :: p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
cenclosed p
fctxt SPointer
a0 (Nat Word64
si0) SPointer
a1 (Nat Word64
si1) =
let v0 :: SimpleExpr
v0 = SPointer -> SimpleExpr
spointer_to_expr SPointer
a0
v1 :: SimpleExpr
v1 = SPointer -> SimpleExpr
spointer_to_expr SPointer
a1 in
SimpleExpr -> Word64 -> SimpleExpr -> Word64 -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
v0 Word64
si0 SimpleExpr
v1 Word64
si1
cenclosed p
fctxt SPointer
a0 RegionSize
_ SPointer
a1 RegionSize
_ = Bool
False
csensitive :: p -> SPointer -> RegionSize -> SValue -> Bool
csensitive p
fctxt SPointer
a (Nat Word64
si) SValue
v =
case SValue -> Maybe SimpleExpr
ctry_deterministic SValue
v of
(Just SimpleExpr
v') -> SPointer -> Word64 -> Bool
forall p. SPointer -> p -> Bool
is_top_stackframe SPointer
a Word64
si Bool -> Bool -> Bool
|| SPointer -> Word64 -> SimpleExpr -> Bool
forall p. SPointer -> p -> SimpleExpr -> Bool
is_pushed_reg SPointer
a Word64
si SimpleExpr
v'
Maybe SimpleExpr
_ -> Bool
False
where
is_initial_reg :: SimpleExpr -> Bool
is_initial_reg (SE_Var (SP_Reg Register
_)) = Bool
True
is_initial_reg SimpleExpr
_ = Bool
False
is_top_stackframe :: SPointer -> p -> Bool
is_top_stackframe (Base_StackPointer [Char]
_ (PtrOffset Word64
0)) p
_ = Bool
True
is_top_stackframe SPointer
_ p
_ = Bool
False
is_pushed_reg :: SPointer -> p -> SimpleExpr -> Bool
is_pushed_reg SPointer
a' p
si' SimpleExpr
v' = SimpleExpr -> Bool
is_initial_reg SimpleExpr
v' Bool -> Bool -> Bool
&& p -> SPointer -> Bool
forall p. p -> SPointer -> Bool
is_local_spointer p
fctxt SPointer
a'
csensitive p
fctxt SPointer
a RegionSize
UnknownSize SValue
v = Bool
False
cread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_ro_data FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt (Word64 -> SValue) -> Maybe Word64 -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection (FContext -> Context
f_ctxt FContext
fctxt) Word64
a (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si)
cread_from_ro_data FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing
cread_from_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_data FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt (Word64 -> SValue) -> Maybe Word64 -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Word64 -> Int -> Maybe Word64
read_from_datasection (FContext -> Context
f_ctxt FContext
fctxt) Word64
a (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si)
cread_from_data FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing
ctry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue
ctry_relocation FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = Word64 -> Maybe SValue
try_reloc Word64
a Maybe SValue -> Maybe SValue -> Maybe SValue
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((\[Char]
_ -> Word64 -> SValue
mk_value Word64
a) ([Char] -> SValue) -> Maybe [Char] -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a)
where
ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
try_reloc :: Word64 -> Maybe SValue
try_reloc Word64
a' = Relocation -> SValue
get_trgt (Relocation -> SValue) -> Maybe Relocation -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Relocation -> Bool) -> Set Relocation -> Maybe Relocation
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> Relocation -> Bool
is_reloc_for Word64
a') (Set Relocation -> Maybe Relocation)
-> Set Relocation -> Maybe Relocation
forall a b. (a -> b) -> a -> b
$ Context -> Set Relocation
ctxt_relocs (Context -> Set Relocation) -> Context -> Set Relocation
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt)
is_reloc_for :: Word64 -> Relocation -> Bool
is_reloc_for Word64
a' (Relocation Word64
a0 Word64
a1) = Word64
a0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a'
get_trgt :: Relocation -> SValue
get_trgt (Relocation Word64
a0 Word64
a1) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
a1
mk_value :: Word64 -> SValue
mk_value Word64
a' = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a') Int
8
ctry_relocation FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing
try_relocated_pointer :: FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt a
a =
case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt of
Just (Relocated_Function [Char]
f) -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
f
Maybe Symbol
_ -> Maybe [Char]
forall a. Maybe a
Nothing
where
ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
instance SymbolicExecutable FContext SValue SPointer where
sseparate :: FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
sseparate = FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate
senclosed :: FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
senclosed = FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
cenclosed
salias :: FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
salias = FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias
ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool
ssensitive = FContext -> SPointer -> RegionSize -> SValue -> Bool
forall p. p -> SPointer -> RegionSize -> SValue -> Bool
csensitive
sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
sread_from_ro_data = FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_ro_data
smk_mem_addresses :: FContext -> [Char] -> SValue -> Set SPointer
smk_mem_addresses = FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses
sjoin_values :: FContext -> [Char] -> t SValue -> SValue
sjoin_values = FContext -> [Char] -> t SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all
swiden_values :: FContext -> [Char] -> SValue -> SValue
swiden_values = FContext -> [Char] -> SValue -> SValue
cwiden
sjoin_pointers :: FContext -> [SPointer] -> [SPointer]
sjoin_pointers = FContext -> [SPointer] -> [SPointer]
forall p. p -> [SPointer] -> [SPointer]
cjoin_pointers
ssemantics :: FContext -> [Char] -> SymbolicOperation SValue -> SValue
ssemantics = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics
sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus
sflg_semantics = FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus
forall p p label prefix annotation.
p
-> p
-> GenericInstruction label Register prefix Opcode annotation
-> FlagStatus
-> FlagStatus
cflg_semantics
simmediate :: FContext -> i -> SValue
simmediate = FContext -> i -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate
top :: FContext -> [Char] -> SValue
top = \FContext
_ -> [Char] -> SValue
mk_top
smk_init_reg_value :: FContext -> Register -> SValue
smk_init_reg_value = FContext -> Register -> SValue
cmk_init_reg_value
smk_init_mem_value :: FContext -> [Char] -> SPointer -> RegionSize -> SValue
smk_init_mem_value = FContext -> [Char] -> SPointer -> RegionSize -> SValue
cmk_init_mem_value
sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
sjump = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
jump
scall :: FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
scall = FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call
stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
stry_jump_targets = FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets
stry_immediate :: FContext -> SValue -> Maybe Word64
stry_immediate = \FContext
_ -> SValue -> Maybe Word64
ctry_immediate
stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr
stry_deterministic = \FContext
_ -> SValue -> Maybe SimpleExpr
ctry_deterministic
stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue
stry_relocation = FContext -> SPointer -> RegionSize -> Maybe SValue
ctry_relocation
saddress_has_instruction :: FContext -> Word64 -> Bool
saddress_has_instruction = \FContext
ctxt -> Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction (FContext -> Context
f_ctxt FContext
ctxt)
instance Propagator FContext Predicate where
tau :: FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
tau = FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, VCS)
sexec_block
join :: FContext
-> [Char]
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> Sstate SValue SPointer
join = FContext
-> [Char]
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> Sstate SValue SPointer
forall v p1 ctxt p2.
(SymbolicExecutable ctxt v p1, SymbolicExecutable ctxt v p2) =>
ctxt -> [Char] -> Sstate v p1 -> Sstate v p1 -> Sstate v p1
sjoin_states
implies :: FContext
-> Sstate SValue SPointer -> Sstate SValue SPointer -> Bool
implies = FContext
-> Sstate SValue SPointer -> Sstate SValue SPointer -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Sstate v p -> Sstate v p -> Bool
simplies
get_invariant :: FContext -> Int -> Maybe Predicate
get_invariant :: FContext -> Int -> Maybe (Sstate SValue SPointer)
get_invariant FContext
fctxt Int
a = do
let ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
let entry :: Int
entry = FContext -> Int
f_entry FContext
fctxt
CFG
g <- Int -> IntMap CFG -> Maybe CFG
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap CFG -> Maybe CFG) -> IntMap CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ Context -> IntMap CFG
ctxt_cfgs Context
ctxt
Invariants
invs <- Int -> IntMap Invariants -> Maybe Invariants
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap Invariants -> Maybe Invariants)
-> IntMap Invariants -> Maybe Invariants
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Invariants
ctxt_invs Context
ctxt
Int
blockId <- Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
a (IntMap Int -> Maybe Int) -> IntMap Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap Int
cfg_addr_to_blockID CFG
g
Sstate SValue SPointer
p <- Int -> Invariants -> Maybe (Sstate SValue SPointer)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockId Invariants
invs
[Instruction]
instrs <- Int -> IntMap [Instruction] -> Maybe [Instruction]
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockId (IntMap [Instruction] -> Maybe [Instruction])
-> IntMap [Instruction] -> Maybe [Instruction]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
g
Sstate SValue SPointer -> Maybe (Sstate SValue SPointer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sstate SValue SPointer -> Maybe (Sstate SValue SPointer))
-> Sstate SValue SPointer -> Maybe (Sstate SValue SPointer)
forall a b. (a -> b) -> a -> b
$ (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a, b) -> a
fst ((Sstate SValue SPointer, VCS) -> Sstate SValue SPointer)
-> (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, VCS)
sexec_block FContext
fctxt ((Instruction -> Bool) -> [Instruction] -> [Instruction]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Instruction
i -> Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
a) [Instruction]
instrs) Maybe [Instruction]
forall a. Maybe a
Nothing Sstate SValue SPointer
p
init_pred ::
FContext
-> String
-> Invariants
-> S.Set (NodeInfo,Predicate)
-> S.Set SStatePart
-> Predicate
init_pred :: FContext
-> [Char]
-> Invariants
-> Set (NodeInfo, Sstate SValue SPointer)
-> Set SStatePart
-> Sstate SValue SPointer
init_pred FContext
fctxt [Char]
f Invariants
curr_invs Set (NodeInfo, Sstate SValue SPointer)
curr_posts Set SStatePart
curr_sps =
let FInit Set (StatePart, Maybe SValue)
finit Map (SStatePart, SStatePart) MemRelation
_ = FContext -> FInit
f_init FContext
fctxt
sps :: Set SStatePart
sps = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [Set SStatePart
curr_sps, (StatePart -> SStatePart) -> Set StatePart -> Set SStatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt) (Set StatePart -> Set SStatePart)
-> Set StatePart -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> StatePart)
-> Set (StatePart, Maybe SValue) -> Set StatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (StatePart, Maybe SValue) -> StatePart
forall a b. (a, b) -> a
fst Set (StatePart, Maybe SValue)
finit, (SStatePart -> Set SStatePart -> Set SStatePart
forall a. Ord a => a -> Set a -> Set a
S.delete (Register -> SStatePart
SSP_Reg Register
RIP) (Set SStatePart -> Set SStatePart)
-> Set SStatePart -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ Invariants
-> Set (NodeInfo, Sstate SValue SPointer) -> Set SStatePart
gather_stateparts Invariants
curr_invs Set (NodeInfo, Sstate SValue SPointer)
curr_posts)]
([Register]
regs,[(SPointer, Int)]
regions) = (SStatePart -> Either Register (SPointer, Int))
-> [SStatePart] -> ([Register], [(SPointer, Int)])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith SStatePart -> Either Register (SPointer, Int)
reg_or_mem ([SStatePart] -> ([Register], [(SPointer, Int)]))
-> [SStatePart] -> ([Register], [(SPointer, Int)])
forall a b. (a -> b) -> a -> b
$ Set SStatePart -> [SStatePart]
forall a. Set a -> [a]
S.toList Set SStatePart
sps
rsp0 :: SValue
rsp0 = NESet SimpleExpr -> SValue
SConcrete (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f
write_stack_pointer :: Sstate SValue SPointer -> Sstate SValue SPointer
write_stack_pointer = State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_rreg FContext
fctxt Register
RSP SValue
rsp0)
top_stack_frame :: SValue
top_stack_frame = NESet SimpleExpr -> SValue
SConcrete (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f) Int
8
write_return_address :: Sstate SValue SPointer -> Sstate SValue SPointer
write_return_address = State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> Bool
-> SValue
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem FContext
fctxt Bool
True SValue
rsp0 (Word64 -> RegionSize
Nat Word64
8) SValue
top_stack_frame)
sregs :: Map Register SValue
sregs = [(Register, SValue)] -> Map Register SValue
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Register, SValue)] -> Map Register SValue)
-> [(Register, SValue)] -> Map Register SValue
forall a b. (a -> b) -> a -> b
$ (Register -> (Register, SValue))
-> [Register] -> [(Register, SValue)]
forall a b. (a -> b) -> [a] -> [b]
map (\Register
r -> (Register
r,FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg Register
r))) [Register]
regs
smem :: Map k a
smem = Map k a
forall k a. Map k a
M.empty in
Sstate SValue SPointer -> Sstate SValue SPointer
write_stack_pointer (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> Sstate SValue SPointer
write_return_address (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit (Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a. Set a -> [a]
S.toList Set (StatePart, Maybe SValue)
finit) (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ (Map Register SValue
-> Map (SPointer, RegionSize) SValue
-> FlagStatus
-> Sstate SValue SPointer
forall v p.
Map Register v -> Map (p, RegionSize) v -> FlagStatus -> Sstate v p
Sstate Map Register SValue
sregs Map (SPointer, RegionSize) SValue
forall k a. Map k a
smem FlagStatus
None)
where
reg_or_mem :: SStatePart -> Either Register (SPointer, Int)
reg_or_mem (SSP_Reg Register
r) = Register -> Either Register (SPointer, Int)
forall a b. a -> Either a b
Left Register
r
reg_or_mem (SSP_Mem SPointer
a Int
si) = (SPointer, Int) -> Either Register (SPointer, Int)
forall a b. b -> Either a b
Right (SPointer
a,Int
si)
write_finit :: [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [] Sstate SValue SPointer
s = Sstate SValue SPointer
s
write_finit ((StatePart
sp,Maybe SValue
Nothing):[(StatePart, Maybe SValue)]
finit) Sstate SValue SPointer
s = [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [(StatePart, Maybe SValue)]
finit Sstate SValue SPointer
s
write_finit ((StatePart
sp,Just SValue
v):[(StatePart, Maybe SValue)]
finit) Sstate SValue SPointer
s = [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [(StatePart, Maybe SValue)]
finit (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp FContext
fctxt (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp) SValue
v) Sstate SValue SPointer
s
gather_stateparts ::
Invariants
-> S.Set (NodeInfo,Predicate)
-> S.Set SStatePart
gather_stateparts :: Invariants
-> Set (NodeInfo, Sstate SValue SPointer) -> Set SStatePart
gather_stateparts Invariants
invs Set (NodeInfo, Sstate SValue SPointer)
posts = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [(Sstate SValue SPointer -> Set SStatePart -> Set SStatePart)
-> Set SStatePart -> Invariants -> Set SStatePart
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IM.foldr Sstate SValue SPointer -> Set SStatePart -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart -> Set SStatePart
accumulate_stateparts Set SStatePart
forall a. Set a
S.empty Invariants
invs, Set (Sstate SValue SPointer) -> Set SStatePart
forall b. Set (Sstate b SPointer) -> Set SStatePart
get_stateparts_of_sstates (((NodeInfo, Sstate SValue SPointer) -> Sstate SValue SPointer)
-> Set (NodeInfo, Sstate SValue SPointer)
-> Set (Sstate SValue SPointer)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (NodeInfo, Sstate SValue SPointer) -> Sstate SValue SPointer
forall a b. (a, b) -> b
snd Set (NodeInfo, Sstate SValue SPointer)
posts)]
where
accumulate_stateparts :: Sstate b SPointer -> Set SStatePart -> Set SStatePart
accumulate_stateparts Sstate b SPointer
p = Set SStatePart -> Set SStatePart -> Set SStatePart
forall a. Ord a => Set a -> Set a -> Set a
S.union (Sstate b SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate Sstate b SPointer
p)
get_stateparts_of_sstates :: Set (Sstate b SPointer) -> Set SStatePart
get_stateparts_of_sstates Set (Sstate b SPointer)
ps = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set SStatePart] -> Set SStatePart)
-> [Set SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ (Sstate b SPointer -> Set SStatePart)
-> [Sstate b SPointer] -> [Set SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map Sstate b SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate ([Sstate b SPointer] -> [Set SStatePart])
-> [Sstate b SPointer] -> [Set SStatePart]
forall a b. (a -> b) -> a -> b
$ Set (Sstate b SPointer) -> [Sstate b SPointer]
forall a. Set a -> [a]
S.toList (Set (Sstate b SPointer) -> [Sstate b SPointer])
-> Set (Sstate b SPointer) -> [Sstate b SPointer]
forall a b. (a -> b) -> a -> b
$ Set (Sstate b SPointer)
ps
get_stateparts_of_sstate :: Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate (Sstate Map Register b
sregs Map (SPointer, RegionSize) b
smem FlagStatus
_) = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [Map Register b -> Set SStatePart
forall a. Map Register a -> Set SStatePart
gather_regs Map Register b
sregs, Map Register b -> Set SStatePart
forall p a. p -> Set a
gather_reg_values Map Register b
sregs, Map (SPointer, RegionSize) b -> Set SStatePart
forall b. Map (SPointer, RegionSize) b -> Set SStatePart
gather_regions Map (SPointer, RegionSize) b
smem, Map (SPointer, RegionSize) b -> Set SStatePart
forall p a. p -> Set a
gather_mem_values Map (SPointer, RegionSize) b
smem]
where
gather_regs :: Map Register a -> Set SStatePart
gather_regs Map Register a
regs = [SStatePart] -> Set SStatePart
forall a. Ord a => [a] -> Set a
S.fromList ([SStatePart] -> Set SStatePart) -> [SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ (Register -> SStatePart) -> [Register] -> [SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map Register -> SStatePart
SSP_Reg ([Register] -> [SStatePart]) -> [Register] -> [SStatePart]
forall a b. (a -> b) -> a -> b
$ Map Register a -> [Register]
forall k a. Map k a -> [k]
M.keys Map Register a
regs
gather_reg_values :: p -> Set a
gather_reg_values p
regs = Set a
forall a. Set a
S.empty
gather_regions :: Map (SPointer, RegionSize) b -> Set SStatePart
gather_regions Map (SPointer, RegionSize) b
mem = [SStatePart] -> Set SStatePart
forall a. Ord a => [a] -> Set a
S.fromList ([SStatePart] -> Set SStatePart) -> [SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ [Maybe SStatePart] -> [SStatePart]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SStatePart] -> [SStatePart])
-> [Maybe SStatePart] -> [SStatePart]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), b) -> Maybe SStatePart)
-> [((SPointer, RegionSize), b)] -> [Maybe SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map ((SPointer, RegionSize), b) -> Maybe SStatePart
forall b. ((SPointer, RegionSize), b) -> Maybe SStatePart
mk_mem_region ([((SPointer, RegionSize), b)] -> [Maybe SStatePart])
-> [((SPointer, RegionSize), b)] -> [Maybe SStatePart]
forall a b. (a -> b) -> a -> b
$ Map (SPointer, RegionSize) b -> [((SPointer, RegionSize), b)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (SPointer, RegionSize) b
mem
gather_mem_values :: p -> Set a
gather_mem_values p
mem = Set a
forall a. Set a
S.empty
mk_mem_region :: ((SPointer, RegionSize), b) -> Maybe SStatePart
mk_mem_region ((SPointer
a,Nat Word64
si),b
_)
| SPointer -> Bool
has_unknown_offset SPointer
a = Maybe SStatePart
forall a. Maybe a
Nothing
| Bool
otherwise = SStatePart -> Maybe SStatePart
forall a. a -> Maybe a
Just (SStatePart -> Maybe SStatePart) -> SStatePart -> Maybe SStatePart
forall a b. (a -> b) -> a -> b
$ SPointer -> Int -> SStatePart
SSP_Mem SPointer
a (Int -> SStatePart) -> Int -> SStatePart
forall a b. (a -> b) -> a -> b
$ Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si
mk_mem_region ((SPointer, RegionSize), b)
_ = Maybe SStatePart
forall a. Maybe a
Nothing
mapMaybeS :: Ord b => (a -> Maybe b) -> S.Set a -> S.Set b
mapMaybeS :: (a -> Maybe b) -> Set a -> Set b
mapMaybeS a -> Maybe b
f = (Maybe b -> b) -> Set (Maybe b) -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Set (Maybe b) -> Set b)
-> (Set a -> Set (Maybe b)) -> Set a -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe b -> Bool) -> Set (Maybe b) -> Set (Maybe b)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Maybe b -> Maybe b -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe b
forall a. Maybe a
Nothing) (Set (Maybe b) -> Set (Maybe b))
-> (Set a -> Set (Maybe b)) -> Set a -> Set (Maybe b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> Set a -> Set (Maybe b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map a -> Maybe b
f
mapMaybeNES :: Ord b => (a -> Maybe b) -> NES.NESet a -> S.Set b
mapMaybeNES :: (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES a -> Maybe b
f = (Maybe b -> b) -> Set (Maybe b) -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Set (Maybe b) -> Set b)
-> (NESet a -> Set (Maybe b)) -> NESet a -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe b -> Bool) -> NESet (Maybe b) -> Set (Maybe b)
forall a. (a -> Bool) -> NESet a -> Set a
NES.filter (Maybe b -> Maybe b -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe b
forall a. Maybe a
Nothing) (NESet (Maybe b) -> Set (Maybe b))
-> (NESet a -> NESet (Maybe b)) -> NESet a -> Set (Maybe b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> NESet a -> NESet (Maybe b)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map a -> Maybe b
f
invariant_to_finit :: FContext -> Predicate -> FInit
invariant_to_finit :: FContext -> Sstate SValue SPointer -> FInit
invariant_to_finit FContext
fctxt Sstate SValue SPointer
p =
let sps :: Set (SStatePart, SValue, Set SPointer)
sps = (SStatePart -> Maybe (SStatePart, SValue, Set SPointer))
-> Set SStatePart -> Set (SStatePart, SValue, Set SPointer)
forall b a. Ord b => (a -> Maybe b) -> Set a -> Set b
mapMaybeS SStatePart -> Maybe (SStatePart, SValue, Set SPointer)
maybe_read_sp (Set SStatePart -> Set (SStatePart, SValue, Set SPointer))
-> Set SStatePart -> Set (SStatePart, SValue, Set SPointer)
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate Sstate SValue SPointer
p
pairs :: [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))]
pairs = Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))]
forall a. Set a -> [a]
S.toList (Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))])
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))]
forall a b. (a -> b) -> a -> b
$ (((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> Bool)
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
forall a. (a -> Bool) -> Set a -> Set a
S.filter (\((SStatePart, SValue, Set SPointer)
x,(SStatePart, SValue, Set SPointer)
y) -> (SStatePart, SValue, Set SPointer)
x (SStatePart, SValue, Set SPointer)
-> (SStatePart, SValue, Set SPointer) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SStatePart, SValue, Set SPointer)
y) (Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer)))
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
forall a b. (a -> b) -> a -> b
$ Set (SStatePart, SValue, Set SPointer)
-> Set (SStatePart, SValue, Set SPointer)
-> Set
((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
forall a b. Set a -> Set b -> Set (a, b)
S.cartesianProduct Set (SStatePart, SValue, Set SPointer)
sps Set (SStatePart, SValue, Set SPointer)
sps
finit :: FInit
finit = Set (StatePart, Maybe SValue)
-> Map (SStatePart, SStatePart) MemRelation -> FInit
FInit (((SStatePart, SValue, Set SPointer) -> (StatePart, Maybe SValue))
-> Set (SStatePart, SValue, Set SPointer)
-> Set (StatePart, Maybe SValue)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (SStatePart, SValue, Set SPointer) -> (StatePart, Maybe SValue)
forall c. (SStatePart, SValue, c) -> (StatePart, Maybe SValue)
keep_globals Set (SStatePart, SValue, Set SPointer)
sps) ([((SStatePart, SStatePart), MemRelation)]
-> Map (SStatePart, SStatePart) MemRelation
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((SStatePart, SStatePart), MemRelation)]
-> Map (SStatePart, SStatePart) MemRelation)
-> [((SStatePart, SStatePart), MemRelation)]
-> Map (SStatePart, SStatePart) MemRelation
forall a b. (a -> b) -> a -> b
$ (((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> ((SStatePart, SStatePart), MemRelation))
-> [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))]
-> [((SStatePart, SStatePart), MemRelation)]
forall a b. (a -> b) -> [a] -> [b]
map ((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))
-> ((SStatePart, SStatePart), MemRelation)
forall (t :: * -> *) (t :: * -> *) a b b b.
(Foldable t, Foldable t) =>
((a, b, t SPointer), (b, b, t SPointer)) -> ((a, b), MemRelation)
mk_memrel [((SStatePart, SValue, Set SPointer),
(SStatePart, SValue, Set SPointer))]
pairs) in
FInit
finit
where
keep_globals :: (SStatePart, SValue, c) -> (StatePart, Maybe SValue)
keep_globals (SStatePart
sp,SValue
v,c
_)
| SValue -> Bool
is_global_value SValue
v = (SStatePart -> StatePart
mk_sp SStatePart
sp,SValue -> Maybe SValue
forall a. a -> Maybe a
Just SValue
v)
| Bool
otherwise = (SStatePart -> StatePart
mk_sp SStatePart
sp,Maybe SValue
forall a. Maybe a
Nothing)
maybe_read_sp :: SStatePart -> Maybe (SStatePart, SValue, Set SPointer)
maybe_read_sp SStatePart
sp
| SStatePart -> Bool
suitable_sp SStatePart
sp =
case State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt SStatePart
sp) Sstate SValue SPointer
p of
SValue
Top -> Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
SAddends NESet (NESet SAddend)
es -> Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
SConcrete NESet SimpleExpr
es ->
let es' :: Set SimpleExpr
es' = (SimpleExpr -> Bool) -> NESet SimpleExpr -> Set SimpleExpr
forall a. (a -> Bool) -> NESet a -> Set a
NES.filter (\SimpleExpr
e -> FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe SPointer
forall a. Maybe a
Nothing) NESet SimpleExpr
es
ptrs :: Set SPointer
ptrs = (SimpleExpr -> SPointer) -> Set SimpleExpr -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Maybe SPointer -> SPointer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SPointer -> SPointer)
-> (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> SPointer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True) Set SimpleExpr
es' in
if Set SPointer -> Bool
forall a. Set a -> Bool
S.null Set SPointer
ptrs then
Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
else
(SStatePart, SValue, Set SPointer)
-> Maybe (SStatePart, SValue, Set SPointer)
forall a. a -> Maybe a
Just (SStatePart
sp,FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"finit" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> NESet SimpleExpr
forall a. Set a -> NESet a
NES.unsafeFromSet Set SimpleExpr
es',Set SPointer
ptrs)
| Bool
otherwise = Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
suitable_sp :: SStatePart -> Bool
suitable_sp (SSP_Reg Register
r) = Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Register
RIP,Register
RSP,Register
RBP]
suitable_sp (SSP_Mem SPointer
a Int
si) = SPointer -> Bool
is_global_ptr SPointer
a Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> SimpleExpr
spointer_to_expr SPointer
a)
mk_memrel :: ((a, b, t SPointer), (b, b, t SPointer)) -> ((a, b), MemRelation)
mk_memrel ((a
sp0,b
v0,t SPointer
ptrs0),(b
sp1,b
v1,t SPointer
ptrs1))
| (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr0 -> (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr1 -> FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate FContext
fctxt [Char]
"invariant_to_finit" SPointer
ptr0 RegionSize
UnknownSize SPointer
ptr1 RegionSize
UnknownSize) t SPointer
ptrs1) t SPointer
ptrs0 = ((a
sp0,b
sp1),MemRelation
Separate)
| (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr0 -> (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr1 -> FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias FContext
fctxt SPointer
ptr0 RegionSize
UnknownSize SPointer
ptr1 RegionSize
UnknownSize) t SPointer
ptrs1) t SPointer
ptrs0 = ((a
sp0,b
sp1),MemRelation
Aliassing)
| Bool
otherwise = ((a
sp0,b
sp1),MemRelation
Unknown)
is_global_value :: SValue -> Bool
is_global_value (SConcrete NESet SimpleExpr
es) = (SPointer -> Bool) -> Set SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SPointer -> Bool
is_global_ptr (Set SPointer -> Bool) -> Set SPointer -> Bool
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Maybe SPointer) -> NESet SimpleExpr -> Set SPointer
forall b a. Ord b => (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True) NESet SimpleExpr
es
is_global_ptr :: SPointer -> Bool
is_global_ptr (Base_Immediate Word64
_ PtrOffset
_) = Bool
True
is_global_ptr SPointer
_ = Bool
False
mk_sp :: SStatePart -> StatePart
mk_sp (SSP_Reg Register
r) = Register -> StatePart
SP_Reg Register
r
mk_sp (SSP_Mem SPointer
a Int
si) = SimpleExpr -> Int -> StatePart
SP_Mem (SPointer -> SimpleExpr
spointer_to_expr SPointer
a) Int
si
join_finit :: FContext -> FInit -> FInit -> FInit
join_finit :: FContext -> FInit -> FInit -> FInit
join_finit FContext
fctxt f0 :: FInit
f0@(FInit Set (StatePart, Maybe SValue)
sps0 Map (SStatePart, SStatePart) MemRelation
m0) f1 :: FInit
f1@(FInit Set (StatePart, Maybe SValue)
sps1 Map (SStatePart, SStatePart) MemRelation
m1)
| FInit
f0 FInit -> FInit -> Bool
forall a. Eq a => a -> a -> Bool
== FInit
f1 = FInit
f0
| Bool
otherwise = Set (StatePart, Maybe SValue)
-> Map (SStatePart, SStatePart) MemRelation -> FInit
FInit (Set (StatePart, Maybe SValue)
-> Set (StatePart, Maybe SValue) -> Set (StatePart, Maybe SValue)
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set (StatePart, Maybe SValue)
sps0 Set (StatePart, Maybe SValue)
sps1) ((MemRelation -> MemRelation -> MemRelation)
-> Map (SStatePart, SStatePart) MemRelation
-> Map (SStatePart, SStatePart) MemRelation
-> Map (SStatePart, SStatePart) MemRelation
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith MemRelation -> MemRelation -> MemRelation
join_rel Map (SStatePart, SStatePart) MemRelation
m0 Map (SStatePart, SStatePart) MemRelation
m1)
where
join_rel :: MemRelation -> MemRelation -> MemRelation
join_rel MemRelation
r0 MemRelation
r1
| MemRelation
r0 MemRelation -> MemRelation -> Bool
forall a. Eq a => a -> a -> Bool
== MemRelation
r1 = MemRelation
r0
| Bool
otherwise = MemRelation
Unknown
data ExternalFunctionOutput = FreshPointer | UnknownReturnValue | Input Register
data ExternalFunctionBehavior = ExternalFunctionBehavior {
ExternalFunctionBehavior -> [Register]
f_inputs :: [Register],
ExternalFunctionBehavior -> ExternalFunctionOutput
f_output :: ExternalFunctionOutput
}
param :: a -> Register
param a
0 = Register
RDI
param a
1 = Register
RSI
param a
2 = Register
RDX
param a
3 = Register
RCX
param a
4 = Register
R8
param a
5 = Register
R9
pure_and_fresh :: ExternalFunctionBehavior
pure_and_fresh = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
FreshPointer
pure_and_unknown :: ExternalFunctionBehavior
pure_and_unknown = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior :: FContext -> String -> ExternalFunctionBehavior
external_function_behavior :: FContext -> [Char] -> ExternalFunctionBehavior
external_function_behavior FContext
_ [Char]
"_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_create_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_default_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_zone_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_zone_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_mmap" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_av_mallocz" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"___error" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strerror_r" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_EVP_CIPHER_CTX_new" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_open" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fts_read$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fts_open$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_opendir$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wfdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wsetlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_b_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"dcgettext" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"nl_langinfo" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__errno_location" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_popen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_tolower_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_toupper_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"readdir" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"getmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"setmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"hasmntopt" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fnmatch" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"___maskrune" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getbsize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"vprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"vfprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fwprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fwprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__fprintf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__printf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_putchar" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_puts" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strlen" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_ilogb" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_atoi" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getopt" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"getopt_long" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_warn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_warnx" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__errno_location" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__libc_start_main" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__cxa_finalize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"perror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"unlink" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"unlinkat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"utimensat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fdatasync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fsync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"isatty" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strcspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"isprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"iswprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_isprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_iswprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__cxa_atexit" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"towlower" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"towupper" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"iswalnum" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fseeko" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgets" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_ferror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strtol" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strtoul" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_munmap" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"snprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snprintf_l" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snwprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snwprintf_l" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"__snprintf_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_vsnprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_sprintf" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"___bzero" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigprocmask" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"__strcat_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"strcat" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"strlcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"___strlcpy_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigemptyset" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigaction" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"localtime" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
FreshPointer
external_function_behavior FContext
_ [Char]
"memset" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memset" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memset_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"___memset_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_index" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_rindex" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_realloc" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_malloc_zone_realloc" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_recallocarray" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"realloc" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__strcpy_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strncpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strncpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"stpcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memcpy" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memcpy_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"___memcpy_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memmove_chk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memmove" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memmove" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strcat" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strcat" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strrchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strrchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memchr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strstr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strstr" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strpbrk" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strtok" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strtok" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strlen" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
fctxt [Char]
f
| [Char] -> Bool
is_exiting_function_call [Char]
f = ExternalFunctionBehavior
pure_and_unknown
| Bool
otherwise = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
UnknownReturnValue
transpose_bw_offset :: FContext -> PtrOffset -> SPointer -> SPointer
transpose_bw_offset :: FContext -> PtrOffset -> SPointer -> SPointer
transpose_bw_offset FContext
fctxt (PtrOffset Word64
off) SPointer
v
| SPointer -> Bool
has_unknown_offset SPointer
v = SPointer
v
| Bool
otherwise = (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) Word64
off) SPointer
v
transpose_bw_offset FContext
fctxt PtrOffset
UnknownOffset SPointer
v = FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"transpose_bw_offset" SPointer
v
transpose_bw_spointer :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> SPointer -> Maybe SPointer
transpose_bw_spointer :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SPointer
-> Maybe SPointer
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_StackPointer [Char]
f PtrOffset
offset) = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show (SPointer
b)
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_Immediate Word64
a PtrOffset
offset) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_Malloc Maybe Word64
_ Maybe [Char]
_ PtrOffset
offset) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
offset) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_ReturnAddr [Char]
_) = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of return address"
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_TLS PtrOffset
offset) = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of TLS"
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_FunctionReturn [Char]
f PtrOffset
offset) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_StatePart StatePart
sp PtrOffset
offset) =
let ptrs :: Set SPointer
ptrs = FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt ([Char]
"transpose_bw_spointer\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sstate SValue SPointer -> [Char]
forall a. Show a => a -> [Char]
show Sstate SValue SPointer
p [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sstate SValue SPointer -> [Char]
forall a. Show a => a -> [Char]
show Sstate SValue SPointer
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\nb = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show SPointer
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\ne = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp))) (SValue -> Set SPointer) -> SValue -> Set SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp) in
if Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
ptrs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
ptrs
else
Maybe SPointer
forall a. Maybe a
Nothing
transpose_bw_addend :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> NES.NESet SAddend -> SValue
transpose_bw_addend :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> NESet SAddend
-> SValue
transpose_bw_addend FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q NESet SAddend
ptrs = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"transpose_bw_addend" (SValue -> SValue) -> SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SValue -> SValue -> SValue) -> NESet SValue -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
NES.foldr1 (FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
64) (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SAddend -> SValue) -> NESet SAddend -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SAddend -> SValue
transpose_bw_saddend NESet SAddend
ptrs
where
transpose_bw_saddend :: SAddend -> SValue
transpose_bw_saddend :: SAddend -> SValue
transpose_bw_saddend (SAddend_StackPointer [Char]
f) = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt (Register -> SStatePart
SSP_Reg Register
RSP)) Sstate SValue SPointer
p
transpose_bw_saddend (SAddend_Immediate Word64
a) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
a
transpose_bw_saddend (SAddend_Malloc Maybe Word64
id Maybe [Char]
hash) = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
hash
transpose_bw_saddend (SAddend_FunctionPtr Word64
a [Char]
_) = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8
transpose_bw_saddend (SAddend_ReturnAddr [Char]
_) = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of return address"
transpose_bw_saddend (SAddend
SAddend_TLS) = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of TLS"
transpose_bw_saddend (SAddend_StatePart StatePart
sp) = FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp)
transpose_bw_saddend (SAddend_FunctionReturn [Char]
f) = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
f
transpose_bw_svalue :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (SConcrete NESet SimpleExpr
es) = FContext -> [Char] -> NESet SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
"transpose_bw" (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SValue) -> NESet SimpleExpr -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p) NESet SimpleExpr
es
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (SAddends NESet (NESet SAddend)
adds) = FContext -> [Char] -> NESet SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
"transpose_bw" (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (NESet SAddend -> SValue) -> NESet (NESet SAddend) -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> NESet SAddend
-> SValue
transpose_bw_addend FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) NESet (NESet SAddend)
adds
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q t :: SValue
t@SValue
Top = SValue
t
transpose_bw_reg :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> (Register, SValue) -> Maybe (Register, SValue)
transpose_bw_reg :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (Register
r,SValue
v) =
let v' :: SValue
v' = FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SValue
v in
(Register, SValue) -> Maybe (Register, SValue)
forall a. a -> Maybe a
Just ((Register, SValue) -> Maybe (Register, SValue))
-> (Register, SValue) -> Maybe (Register, SValue)
forall a b. (a -> b) -> a -> b
$ (Register
r,SValue
v')
transpose_bw_mem :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> ((SPointer,RegionSize), SValue) -> Maybe ((SPointer,RegionSize), SValue)
transpose_bw_mem :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
transpose_bw_mem FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q ((SPointer
a,RegionSize
si),SValue
v) =
case FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SPointer
-> Maybe SPointer
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SPointer
a of
Just SPointer
a' -> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
forall a. a -> Maybe a
Just ((SPointer
a',RegionSize
si), FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SValue
v)
Maybe SPointer
Nothing -> Maybe ((SPointer, RegionSize), SValue)
forall a. Maybe a
Nothing
transpose_bw_e :: FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e :: FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (Bottom (FromCall [Char]
f)) = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom ([Char] -> BotTyp
FromCall [Char]
f)
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Malloc Maybe Word64
id Maybe [Char]
hash) = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
hash
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Immediate Word64
i) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
i
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_StatePart StatePart
sp) = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Var (SP_StackPointer [Char]
f)) = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
RSP) Sstate SValue SPointer
p
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Var StatePart
sp) = FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p StatePart
sp
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Bit Int
i SimpleExpr
e) = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> SValue -> SymbolicOperation SValue
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
i (SValue -> SymbolicOperation SValue)
-> SValue -> SymbolicOperation SValue
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_SExtend Int
l Int
h SimpleExpr
e) = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SValue -> SymbolicOperation SValue
forall v. Int -> Int -> v -> SymbolicOperation v
SO_SExtend Int
l Int
h (SValue -> SymbolicOperation SValue)
-> SValue -> SymbolicOperation SValue
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
Plus Int
si [SimpleExpr
a,SimpleExpr
b]) = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Opcode -> Int -> Maybe Int -> [SValue] -> SymbolicOperation SValue
forall v. Opcode -> Int -> Maybe Int -> [v] -> SymbolicOperation v
SO_Op Opcode
ADD (Int
si Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Maybe Int
forall a. Maybe a
Nothing [FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a,FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
Minus Int
si [SimpleExpr
a,SimpleExpr
b]) = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Opcode -> Int -> Maybe Int -> [SValue] -> SymbolicOperation SValue
forall v. Opcode -> Int -> Maybe Int -> [v] -> SymbolicOperation v
SO_Op Opcode
SUB (Int
si Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Maybe Int
forall a. Maybe a
Nothing [FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a,FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
op Int
si [SimpleExpr]
es) = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"transpose_bw" (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
op Int
si) ([SValue] -> SValue) -> [SValue] -> SValue
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SValue) -> [SimpleExpr] -> [SValue]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p) [SimpleExpr]
es
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Overwrite Int
i SimpleExpr
a SimpleExpr
b) = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> SValue -> SValue -> SymbolicOperation SValue
forall v. Int -> v -> v -> SymbolicOperation v
SO_Overwrite Int
i (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a) (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b)
transpose_bw_sp :: FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp :: FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p (SP_Reg Register
r) = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r) Sstate SValue SPointer
p
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p (SP_Mem SimpleExpr
a Int
si) =
let a' :: SValue
a' = FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a in
State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> [Char]
-> SValue
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> v -> RegionSize -> State (Sstate v p, VCS) v
sread_mem FContext
fctxt [Char]
"transpose_bw_sp" SValue
a' (RegionSize -> State (Sstate SValue SPointer, VCS) SValue)
-> RegionSize -> State (Sstate SValue SPointer, VCS) SValue
forall a b. (a -> b) -> a -> b
$ Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si) Sstate SValue SPointer
p
read_sp :: FContext -> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp :: FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt (SSP_Reg Register
r) = FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r
read_sp FContext
fctxt (SSP_Mem SPointer
a Int
si) = FContext
-> [Char]
-> SPointer
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> p -> RegionSize -> State (Sstate v p, VCS) v
sread_mem_from_ptr FContext
fctxt [Char]
"read_sp" SPointer
a (RegionSize -> State (Sstate SValue SPointer, VCS) SValue)
-> RegionSize -> State (Sstate SValue SPointer, VCS) SValue
forall a b. (a -> b) -> a -> b
$ (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si)
write_sp :: FContext -> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp :: FContext
-> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp FContext
fctxt (SSP_Reg Register
r) SValue
v = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
r SValue
v
write_sp FContext
fctxt (SSP_Mem SPointer
a Int
si) SValue
v = FContext
-> Bool
-> SPointer
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem_to_ptr FContext
fctxt Bool
True SPointer
a (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si) SValue
v
data FunctionType = AnalyzedInternalFunction (Sstate SValue SPointer) | ExternalFunction | AnalyzedInternalFunctionTerminates | AnalyzedInternalFunctionUnknown
get_function_type :: FContext -> Instruction -> [Char] -> FunctionType
get_function_type FContext
fctxt Instruction
i [Char]
f_callee =
[Maybe FReturnBehavior] -> FunctionType
ftype ([Maybe FReturnBehavior] -> FunctionType)
-> [Maybe FReturnBehavior] -> FunctionType
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> Maybe FReturnBehavior)
-> [ResolvedJumpTarget] -> [Maybe FReturnBehavior]
forall a b. (a -> b) -> [a] -> [b]
map ResolvedJumpTarget -> Maybe FReturnBehavior
postcondition_of_jump_target ([ResolvedJumpTarget] -> [Maybe FReturnBehavior])
-> [ResolvedJumpTarget] -> [Maybe FReturnBehavior]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i
where
ftype :: [Maybe FReturnBehavior] -> FunctionType
ftype [Maybe FReturnBehavior]
posts
| (Maybe FReturnBehavior -> Bool) -> [Maybe FReturnBehavior] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe FReturnBehavior -> Maybe FReturnBehavior -> Bool
forall a. Eq a => a -> a -> Bool
(==) (FReturnBehavior -> Maybe FReturnBehavior
forall a. a -> Maybe a
Just FReturnBehavior
Terminating)) [Maybe FReturnBehavior]
posts = FunctionType
AnalyzedInternalFunctionTerminates
| (Maybe FReturnBehavior -> Bool) -> [Maybe FReturnBehavior] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe FReturnBehavior -> Bool
is_returning [Maybe FReturnBehavior]
posts = Sstate SValue SPointer -> FunctionType
AnalyzedInternalFunction (Sstate SValue SPointer -> FunctionType)
-> Sstate SValue SPointer -> FunctionType
forall a b. (a -> b) -> a -> b
$ FContext -> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Sstate v p] -> Sstate v p
supremum FContext
fctxt ([Sstate SValue SPointer] -> Sstate SValue SPointer)
-> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ (Maybe FReturnBehavior -> Sstate SValue SPointer)
-> [Maybe FReturnBehavior] -> [Sstate SValue SPointer]
forall a b. (a -> b) -> [a] -> [b]
map Maybe FReturnBehavior -> Sstate SValue SPointer
fromReturning [Maybe FReturnBehavior]
posts
| [Char]
"0x" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
f_callee Bool -> Bool -> Bool
|| [Char]
"indirection@" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
f_callee = FunctionType
AnalyzedInternalFunctionUnknown
| Bool
otherwise = FunctionType
ExternalFunction
fromReturning :: Maybe FReturnBehavior -> Sstate SValue SPointer
fromReturning (Just (ReturningWith Sstate SValue SPointer
q)) = Sstate SValue SPointer
q
is_returning :: Maybe FReturnBehavior -> Bool
is_returning (Just (ReturningWith Sstate SValue SPointer
q)) = Bool
True
is_returning Maybe FReturnBehavior
_ = Bool
False
postcondition_of_jump_target :: ResolvedJumpTarget -> Maybe FReturnBehavior
postcondition_of_jump_target (ImmediateAddress Word64
a) = Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) (Context -> IntMap FReturnBehavior
ctxt_calls (Context -> IntMap FReturnBehavior)
-> Context -> IntMap FReturnBehavior
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt)
postcondition_of_jump_target ResolvedJumpTarget
_ = Maybe FReturnBehavior
forall a. Maybe a
Nothing
call :: FContext -> Bool -> X86.Instruction -> State (Sstate SValue SPointer,VCS) ()
call :: FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call FContext
fctxt Bool
is_jump Instruction
i = do
case FContext -> Instruction -> [Char] -> FunctionType
get_function_type FContext
fctxt Instruction
i [Char]
f_callee of
FunctionType
AnalyzedInternalFunctionUnknown -> FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall p p. p -> p -> State (Sstate SValue SPointer, VCS) ()
unknown_internal_function FContext
fctxt Instruction
i
FunctionType
AnalyzedInternalFunctionTerminates -> State (Sstate SValue SPointer, VCS) ()
incr_rsp
AnalyzedInternalFunction Sstate SValue SPointer
q -> Sstate SValue SPointer -> State (Sstate SValue SPointer, VCS) ()
internal_function Sstate SValue SPointer
q
FunctionType
ExternalFunction -> State (Sstate SValue SPointer, VCS) ()
external_function
where
external_function :: State (Sstate SValue SPointer, VCS) ()
external_function = case FContext -> [Char] -> ExternalFunctionBehavior
external_function_behavior FContext
fctxt [Char]
f_callee of
ExternalFunctionBehavior [Register]
params ExternalFunctionOutput
output -> ExternalFunctionOutput -> State (Sstate SValue SPointer, VCS) ()
write_output ExternalFunctionOutput
output State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State (Sstate SValue SPointer, VCS) ()
incr_rsp
write_output :: ExternalFunctionOutput -> State (Sstate SValue SPointer,VCS) ()
write_output :: ExternalFunctionOutput -> State (Sstate SValue SPointer, VCS) ()
write_output ExternalFunctionOutput
FreshPointer = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX (SValue -> State (Sstate SValue SPointer, VCS) ())
-> SValue -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i)) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
""))
write_output ExternalFunctionOutput
UnknownReturnValue = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX (SValue -> State (Sstate SValue SPointer, VCS) ())
-> SValue -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom ([Char] -> BotTyp
FromCall [Char]
f_callee))
write_output (Input Register
r) = FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r State (Sstate SValue SPointer, VCS) SValue
-> (SValue -> State (Sstate SValue SPointer, VCS) ())
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX
incr_rsp :: State (Sstate SValue SPointer, VCS) ()
incr_rsp
| Bool
is_jump = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
ADD Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing)
| Bool
otherwise = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
decr_rsp :: State (Sstate SValue SPointer, VCS) ()
decr_rsp
| Bool -> Bool
not Bool
is_jump = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
SUB Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing)
| Bool
otherwise = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
internal_function :: Sstate SValue SPointer -> State (Sstate SValue SPointer,VCS) ()
internal_function :: Sstate SValue SPointer -> State (Sstate SValue SPointer, VCS) ()
internal_function Sstate SValue SPointer
q = do
State (Sstate SValue SPointer, VCS) ()
decr_rsp
(Sstate SValue SPointer
p,VCS
vcs) <- StateT
(Sstate SValue SPointer, VCS)
Identity
(Sstate SValue SPointer, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
let q_eqs_transposed_regs :: [(Register, SValue)]
q_eqs_transposed_regs = [Maybe (Register, SValue)] -> [(Register, SValue)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Register, SValue)] -> [(Register, SValue)])
-> [Maybe (Register, SValue)] -> [(Register, SValue)]
forall a b. (a -> b) -> a -> b
$ ((Register, SValue) -> Maybe (Register, SValue))
-> [(Register, SValue)] -> [Maybe (Register, SValue)]
forall a b. (a -> b) -> [a] -> [b]
map (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) ([(Register, SValue)] -> [Maybe (Register, SValue)])
-> [(Register, SValue)] -> [Maybe (Register, SValue)]
forall a b. (a -> b) -> a -> b
$ ((Register, SValue) -> Bool)
-> [(Register, SValue)] -> [(Register, SValue)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Register
RIP (Register -> Bool)
-> ((Register, SValue) -> Register) -> (Register, SValue) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Register, SValue) -> Register
forall a b. (a, b) -> a
fst) ([(Register, SValue)] -> [(Register, SValue)])
-> [(Register, SValue)] -> [(Register, SValue)]
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> [(Register, SValue)]
forall a p. Sstate a p -> [(Register, a)]
sstate_to_reg_eqs Sstate SValue SPointer
q
let q_eqs_transposed_mem :: [((SPointer, RegionSize), SValue)]
q_eqs_transposed_mem = [Maybe ((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)])
-> [Maybe ((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue))
-> [((SPointer, RegionSize), SValue)]
-> [Maybe ((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> [a] -> [b]
map (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
transpose_bw_mem FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) ([((SPointer, RegionSize), SValue)]
-> [Maybe ((SPointer, RegionSize), SValue)])
-> [((SPointer, RegionSize), SValue)]
-> [Maybe ((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), SValue) -> Bool)
-> [((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SPointer, RegionSize), SValue) -> Bool
do_transfer ([((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)])
-> [((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> [((SPointer, RegionSize), SValue)]
forall a p. Sstate a p -> [((p, RegionSize), a)]
sstate_to_mem_eqs Sstate SValue SPointer
q
(((SPointer, RegionSize), SValue)
-> State (Sstate SValue SPointer, VCS) ())
-> [((SPointer, RegionSize), SValue)]
-> State (Sstate SValue SPointer, VCS) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\((SPointer
a,RegionSize
si),SValue
v) -> FContext
-> Bool
-> SPointer
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem_to_ptr FContext
fctxt Bool
True SPointer
a RegionSize
si SValue
v) ([((SPointer, RegionSize), SValue)]
-> State (Sstate SValue SPointer, VCS) ())
-> [((SPointer, RegionSize), SValue)]
-> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ [((SPointer, RegionSize), SValue)]
q_eqs_transposed_mem
((Register, SValue) -> State (Sstate SValue SPointer, VCS) ())
-> [(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Register
r,SValue
v) -> FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
r SValue
v) ([(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ())
-> [(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ [(Register, SValue)]
q_eqs_transposed_regs
write_param :: Register -> State (Sstate SValue SPointer,VCS) ()
write_param :: Register -> State (Sstate SValue SPointer, VCS) ()
write_param Register
r = do
SValue
a <- FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r
let a' :: SValue
a' = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"write_param" SValue
a
SValue
v' <- ((Sstate SValue SPointer, VCS) -> SValue)
-> State (Sstate SValue SPointer, VCS) SValue
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue)
-> State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer
-> SValue
forall a b. (a -> b) -> a -> b
$ FContext
-> [Char]
-> SValue
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> v -> RegionSize -> State (Sstate v p, VCS) v
sread_mem FContext
fctxt [Char]
"write_param" SValue
a RegionSize
UnknownSize) (Sstate SValue SPointer -> SValue)
-> ((Sstate SValue SPointer, VCS) -> Sstate SValue SPointer)
-> (Sstate SValue SPointer, VCS)
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a, b) -> a
fst)
let bot :: SValue
bot = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"write_param_v" SValue
v'
FContext
-> Bool
-> SValue
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem FContext
fctxt Bool
True SValue
a' RegionSize
UnknownSize SValue
bot
do_transfer :: ((SPointer, RegionSize), SValue) -> Bool
do_transfer ((SPointer
a,RegionSize
si),SValue
v) = Bool -> Bool
not ((SPointer, RegionSize) -> SValue -> Bool
is_initial (SPointer
a,RegionSize
si) SValue
v) Bool -> Bool -> Bool
&& Bool -> Bool
not (SPointer -> RegionSize -> Bool
is_top_stackframe SPointer
a RegionSize
si) Bool -> Bool -> Bool
&& Bool -> Bool
not (FContext -> SPointer -> Bool
forall p. p -> SPointer -> Bool
is_local_spointer FContext
fctxt SPointer
a)
is_initial :: (SPointer,RegionSize) -> SValue -> Bool
is_initial :: (SPointer, RegionSize) -> SValue -> Bool
is_initial (SPointer
a,RegionSize
si) SValue
v = Bool
False
is_top_stackframe :: SPointer -> RegionSize -> Bool
is_top_stackframe (Base_StackPointer [Char]
_ (PtrOffset Word64
0)) (Nat Word64
8) = Bool
True
is_top_stackframe SPointer
_ RegionSize
_ = Bool
False
f_name :: [Char]
f_name = Context -> Int -> [Char]
function_name_of_entry (FContext -> Context
f_ctxt FContext
fctxt) (FContext -> Int
f_entry FContext
fctxt)
f_callee :: [Char]
f_callee = Context -> Instruction -> [Char]
function_name_of_instruction (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i
sstate_to_reg_eqs :: Sstate a p -> [(Register, a)]
sstate_to_reg_eqs (Sstate Map Register a
regs Map (p, RegionSize) a
_ FlagStatus
_) = Map Register a -> [(Register, a)]
forall k a. Map k a -> [(k, a)]
M.toList Map Register a
regs
sstate_to_mem_eqs :: Sstate a p -> [((p, RegionSize), a)]
sstate_to_mem_eqs (Sstate Map Register a
_ Map (p, RegionSize) a
mem FlagStatus
_) = Map (p, RegionSize) a -> [((p, RegionSize), a)]
forall k a. Map k a -> [(k, a)]
M.toList Map (p, RegionSize) a
mem
unknown_internal_function :: p -> p -> State (Sstate SValue SPointer, VCS) ()
unknown_internal_function p
fctxt p
i = State (Sstate SValue SPointer, VCS) ()
incr_rsp
is_local_spointer :: p -> SPointer -> Bool
is_local_spointer p
fctxt (Base_StackPointer [Char]
_ PtrOffset
_) = Bool
True
is_local_spointer p
fctxt b :: SPointer
b@(Base_StatePart StatePart
sp PtrOffset
_ ) = p -> SimpleExpr -> Bool
forall p. p -> SimpleExpr -> Bool
is_local_var p
fctxt (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
is_local_spointer p
fctxt SPointer
_ = Bool
False
is_local_var :: p -> SimpleExpr -> Bool
is_local_var p
fctxt (SE_Var (SP_StackPointer [Char]
_)) = Bool
True
is_local_var p
fctxt (SE_Var (SP_Mem SimpleExpr
a Int
si)) = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
a Maybe [Char] -> Maybe [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe [Char]
forall a. Maybe a
Nothing
is_local_var p
fctxt SimpleExpr
_ = Bool
False
jump :: FContext -> X86.Instruction -> State (Sstate SValue SPointer,VCS) ()
jump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
jump FContext
fctxt Instruction
i
| Context -> Instruction -> Bool
jump_is_actually_a_call (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i = FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call FContext
fctxt Bool
True Instruction
i State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
SUB Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing) State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FContext -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> State (Sstate v p, VCS) ()
sreturn FContext
fctxt
| Bool
otherwise = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ctry_jump_targets :: FContext -> SValue -> Maybe (S.Set ResolvedJumpTarget)
ctry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets FContext
fctxt v :: SValue
v@(SConcrete NESet SimpleExpr
es) =
let tries :: Set ResolvedJumpTarget
tries = (SimpleExpr -> Maybe ResolvedJumpTarget)
-> NESet SimpleExpr -> Set ResolvedJumpTarget
forall b a. Ord b => (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES SimpleExpr -> Maybe ResolvedJumpTarget
try NESet SimpleExpr
es in
if Set ResolvedJumpTarget -> Bool
forall a. Set a -> Bool
S.null Set ResolvedJumpTarget
tries then
Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing
else
Set ResolvedJumpTarget -> Maybe (Set ResolvedJumpTarget)
forall a. a -> Maybe a
Just Set ResolvedJumpTarget
tries
where
try :: SimpleExpr -> Maybe ResolvedJumpTarget
try SimpleExpr
e =
case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
e of
Just SPointer
ptr -> SPointer -> Maybe ResolvedJumpTarget
try_pointer SPointer
ptr
Maybe SPointer
Nothing -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing
try_pointer :: SPointer -> Maybe ResolvedJumpTarget
try_pointer (Base_FunctionPtr Word64
a [Char]
f (PtrOffset Word64
0)) = ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
try_pointer (Base_Immediate Word64
imm (PtrOffset Word64
0)) = Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
imm
try_pointer b :: SPointer
b@(Base_StatePart (SP_Mem (SE_Immediate Word64
i) Int
_) PtrOffset
_) = Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing
try_pointer SPointer
_ = Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing
try_immediate_address :: Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
a
| Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction (FContext -> Context
f_ctxt FContext
fctxt) Word64
a = ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ Word64 -> ResolvedJumpTarget
ImmediateAddress Word64
a
| Bool
otherwise = Word64 -> Maybe ResolvedJumpTarget
forall a. Integral a => a -> Maybe ResolvedJumpTarget
try_symbol Word64
a
try_symbol :: a -> Maybe ResolvedJumpTarget
try_symbol a
a =
case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table (Context -> IntMap Symbol) -> Context -> IntMap Symbol
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt of
Just (Internal_Label [Char]
f) -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
Just (Relocated_Label [Char]
f) -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
Maybe Symbol
_ -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing
ctry_jump_targets FContext
fctxt SValue
_ = Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing