{-# LANGUAGE MultiParamTypeClasses, DeriveGeneric, FlexibleInstances, StrictData #-}

{-|
Module      : SymbolicPropagation
Description : Provides an instantiation of all functions necessary to do symbolic propagation
-}
module WithNoAbstraction.SymbolicExecution where


import Base
import Config

import Data.L0
import Data.Size
import Data.SValue
import Data.SPointer
import Data.JumpTarget
import Data.SymbolicExpression
import Data.Symbol
import Data.VerificationCondition
import Data.Indirection
import Data.X86.Opcode 
import Data.X86.Instruction
import Data.X86.Register


import WithAbstractPredicates.ControlFlow
import Binary.FunctionNames
import WithNoAbstraction.Pointers

import WithAbstractSymbolicValues.Class
import WithAbstractSymbolicValues.SymbolicExecution
import WithAbstractSymbolicValues.Sstate

import Binary.Generic

import Conventions


import Control.Monad.State.Strict hiding (join)
import Control.Applicative ((<|>))
import Control.Monad.Extra 
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



type Static bin v = LiftingEntry bin (Sstate SValue SPointer) (FInit SValue SPointer) v


traceTop :: p -> a -> a
traceTop p
msg = a -> a
forall a. a -> a
id -- trace ("TOP: " ++ msg)

mk_top :: String -> SValue
mk_top String
""  = SValue
Top
mk_top String
msg = String -> SValue -> SValue
forall {p} {a}. p -> a -> a
traceTop String
msg SValue
Top

-- Try to get an immediate value from an SValue
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

-- Check whether the SValue is deterministic
cis_deterministic :: SValue -> Bool
cis_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 = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Bool
contains_bot (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
  | Bool
otherwise        = Bool
False
cis_deterministic SValue
_ = Bool
False





-- Construct an SValue from SExpressions
mk_concrete :: BinaryClass bin => Static bin v -> String -> NES.NESet SimpleExpr -> SValue
---mk_concrete fctxt msg | trace ("mk_concrete: "++ show msg) False = error "trace"
mk_concrete :: forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete l :: Static bin v
l@(bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
_) String
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 -- TODO simp should be unnecessary?
 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 Bool -> Bool -> Bool
|| (SimpleExpr -> Bool) -> NESet SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SimpleExpr -> Bool
too_large NESet SimpleExpr
es = Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
l (String
"mkconcrete_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) (SValue -> SValue) -> SValue -> SValue
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SValue
SConcrete NESet SimpleExpr
es
    | Bool
otherwise = NESet SimpleExpr -> SValue
SConcrete NESet SimpleExpr
es
  num_cases :: Int
num_cases = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Config -> Natural
max_num_of_cases Config
config

  too_large :: SimpleExpr -> Bool
too_large SimpleExpr
e = SimpleExpr -> Int
expr_size SimpleExpr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Config -> Natural
max_expr_size Config
config)

mk_concreteS :: Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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_saddends :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> SValue
mk_saddends l :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
l@(bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
_) = NESet SimpleExpr -> SValue
mk (NESet SimpleExpr -> SValue)
-> (NESet SimpleExpr -> NESet SimpleExpr)
-> NESet SimpleExpr
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> NESet SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> NESet SimpleExpr -> NESet SimpleExpr
group_immediates (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
l
 where
  mk :: NESet SimpleExpr -> SValue
mk NESet SimpleExpr
as
    | NESet SimpleExpr -> Int
forall a. NESet a -> Int
NES.size NESet SimpleExpr
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Config -> Natural
max_num_of_bases Config
config) = String -> SValue -> SValue
forall {p} {a}. p -> a -> a
traceTop String
"mk_saddends" SValue
Top
    | Bool
otherwise = NESet SimpleExpr -> SValue
SAddends NESet SimpleExpr
as


-- When doing abstraction, immediate values are grouped according to whether they are pointers into the same section.
-- Immediates within the same section are merged into one immediate (the lowest).
-- For example, if the values {0x2050, 0x2052, 0x2054} are abstracted and there is a data section starting at 0x2000 with size 0x100,
-- the value 0x2050 + Top is produced
group_immediates :: BinaryClass bin => Static bin v -> NES.NESet SimpleExpr -> NES.NESet SimpleExpr
group_immediates :: forall bin v.
BinaryClass bin =>
Static bin v -> NESet SimpleExpr -> NESet SimpleExpr
group_immediates l :: Static bin v
l@(bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
_) NESet SimpleExpr
addends =
  let (Set SimpleExpr
imms,Set SimpleExpr
remainder) = (SimpleExpr -> Bool)
-> Set SimpleExpr -> (Set SimpleExpr, Set SimpleExpr)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition SimpleExpr -> Bool
is_imm (Set SimpleExpr -> (Set SimpleExpr, Set SimpleExpr))
-> Set SimpleExpr -> (Set SimpleExpr, Set SimpleExpr)
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
addends in
    if Set SimpleExpr -> Bool
forall a. Set a -> Bool
S.null Set SimpleExpr
imms then
      NESet SimpleExpr
addends
    else
      Set SimpleExpr -> NESet SimpleExpr
forall a. Set a -> NESet a
NES.unsafeFromSet (Set SimpleExpr -> NESet SimpleExpr)
-> Set SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> Set SimpleExpr -> Set SimpleExpr
forall a. Ord a => Set a -> Set a -> Set a
S.union ((Set SimpleExpr -> SimpleExpr)
-> Set (Set SimpleExpr) -> Set SimpleExpr
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set SimpleExpr -> SimpleExpr
merge_imms (Set (Set SimpleExpr) -> Set SimpleExpr)
-> Set (Set SimpleExpr) -> Set SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> Set (Set SimpleExpr)
group_imms_by_section Set SimpleExpr
imms) Set SimpleExpr
remainder
 where
  is_imm :: SimpleExpr -> Bool
is_imm (SE_Immediate Word64
_) = Bool
True
  is_imm SimpleExpr
_ = Bool
False

  group_imms_by_section :: S.Set SimpleExpr -> S.Set (S.Set SimpleExpr)
  group_imms_by_section :: Set SimpleExpr -> Set (Set SimpleExpr)
group_imms_by_section = (SimpleExpr -> SimpleExpr -> Bool)
-> Set SimpleExpr -> Set (Set SimpleExpr)
forall a. Ord a => (a -> a -> Bool) -> Set a -> Set (Set a)
quotientBy SimpleExpr -> SimpleExpr -> Bool
same_section

  same_section :: SimpleExpr -> SimpleExpr -> Bool
same_section SimpleExpr
imm0 SimpleExpr
imm1 = Word64 -> Maybe (String, String, Word64, Word64, Word64)
get_section_for (SimpleExpr -> Word64
get_imm SimpleExpr
imm0) Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Maybe (String, String, Word64, Word64, Word64)
get_section_for (SimpleExpr -> Word64
get_imm SimpleExpr
imm1)

  get_section_for :: Word64 -> Maybe (String, String, Word64, Word64, Word64)
get_section_for Word64
a = bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address bin
bin Word64
a Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_ending_at bin
bin Word64
a

  merge_imms :: Set SimpleExpr -> SimpleExpr
merge_imms = Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr)
-> (Set SimpleExpr -> Word64) -> Set SimpleExpr -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Word64 -> Word64
forall a. Ord a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (Set Word64 -> Word64)
-> (Set SimpleExpr -> Set Word64) -> Set SimpleExpr -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> Word64) -> Set SimpleExpr -> Set Word64
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Word64
get_imm 
  get_imm :: SimpleExpr -> Word64
get_imm (SE_Immediate Word64
imm) = Word64
imm


cimmediate :: (Integral i, BinaryClass bin) => Static bin v -> i -> SValue
cimmediate :: forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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



-- JOINING / WIDENING
cwiden :: BinaryClass bin => Static bin v -> String -> SValue -> SValue
--cwiden fctxt msg v | trace ("cwiden: " ++ msg ++ "\n" ++ show v) False = error "trace"
cwiden :: forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
msg (SConcrete NESet SimpleExpr
es) = 
  let ass :: NESet (Maybe SimpleExpr)
ass = (SimpleExpr -> Maybe SimpleExpr)
-> NESet SimpleExpr -> NESet (Maybe SimpleExpr)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (Static bin v -> SimpleExpr -> Maybe SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base Static bin v
fctxt) NESet SimpleExpr
es in
    if Maybe SimpleExpr
forall a. Maybe a
Nothing Maybe SimpleExpr -> NESet (Maybe SimpleExpr) -> Bool
forall a. Eq a => a -> NESet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` NESet (Maybe SimpleExpr)
ass then
      String -> SValue -> SValue
forall {p} {a}. p -> a -> a
traceTop (String
"cwiden" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NESet SimpleExpr -> String
forall (t :: * -> *) a. (Foldable t, Show a) => t a -> String
show_set NESet SimpleExpr
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) SValue
Top
    else
      Static bin v -> NESet SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
(bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> SValue
mk_saddends Static bin v
fctxt (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ (Maybe SimpleExpr -> SimpleExpr)
-> NESet (Maybe SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map Maybe SimpleExpr -> SimpleExpr
forall a. HasCallStack => Maybe a -> a
fromJust NESet (Maybe SimpleExpr)
ass
  

cwiden Static bin v
fctxt String
msg SValue
v = SValue
v


expr_to_addends :: BinaryClass bin => Static bin v -> SimpleExpr -> [SimpleExpr]
expr_to_addends :: forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> [SimpleExpr]
expr_to_addends fctxt :: Static bin v
fctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
entry) SimpleExpr
e =
  let adds :: [SimpleExpr]
adds = Map SimpleExpr Word64 -> [SimpleExpr]
forall k a. Map k a -> [k]
M.keys (Map SimpleExpr Word64 -> [SimpleExpr])
-> Map SimpleExpr Word64 -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Bool) -> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
1) (Map SimpleExpr Word64 -> Map SimpleExpr Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Map SimpleExpr Word64
addends SimpleExpr
e in
    case (SimpleExpr -> Bool) -> [SimpleExpr] -> [SimpleExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter SimpleExpr -> Bool
is_addend [SimpleExpr]
adds of
      [] -> [] -- filter is_immediate adds
      [SimpleExpr]
as -> [SimpleExpr]
as 
 where
  is_addend :: SimpleExpr -> Bool
is_addend a :: SimpleExpr
a@(SE_Immediate Word64
_)    = bin -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_global_immediate bin
bin SimpleExpr
a
  is_addend (Bottom (FromCall String
f)) = Bool
True
  is_addend (SE_Var StatePart
_)            = Bool
True
  is_addend SimpleExpr
_                     = Bool
False


---cjoin fctxt msg v0 v1 | trace ("cjoin: " ++ msg ++ "\n" ++ show (v0,v1)) False = error "trace"
cjoin :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue -> SValue
cjoin (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt String
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) = 
    let j :: NESet SimpleExpr
j = NESet SimpleExpr -> NESet SimpleExpr -> NESet SimpleExpr
forall a. Ord a => NESet a -> NESet a -> NESet a
NES.union NESet SimpleExpr
es0 NESet SimpleExpr
es1 in
      (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt (String
"cjoin1_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) NESet SimpleExpr
j
  join v0 :: SValue
v0@(SAddends NESet SimpleExpr
as0) v1 :: SValue
v1@(SAddends NESet SimpleExpr
as1) = (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
(bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> SValue
mk_saddends (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt (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
as0 NESet SimpleExpr
as1
  join v0 :: SValue
v0@(SAddends NESet SimpleExpr
_)  v1 :: SValue
v1@(SConcrete NESet SimpleExpr
_) = SValue -> SValue -> SValue
join SValue
v0 ((bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt (String
"cjoin2" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) SValue
v1)
  join v0 :: SValue
v0@(SConcrete NESet SimpleExpr
_) v1 :: SValue
v1@(SAddends NESet SimpleExpr
_)  = SValue -> SValue -> SValue
join ((bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt (String
"cjoin3" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) SValue
v0) SValue
v1
  join SValue
Top SValue
_ = SValue
Top
  join SValue
_ SValue
Top = SValue
Top


cjoin_all :: Foldable t => BinaryClass bin => Static bin v -> String -> t SValue -> SValue
cjoin_all :: forall (t :: * -> *) bin v.
(Foldable t, BinaryClass bin) =>
Static bin v -> String -> t SValue -> SValue
cjoin_all Static bin v
fctxt String
msg t SValue
es
  | t SValue -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t SValue
es   = String -> SValue
forall a. HasCallStack => String -> a
error (String -> SValue) -> String -> SValue
forall a b. (a -> b) -> a -> b
$ String
"Cannot join [], msg = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
  | Bool
otherwise = (SValue -> SValue -> SValue) -> t SValue -> SValue
forall a. (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Static bin v -> String -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
(bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue -> SValue
cjoin Static bin v
fctxt String
msg) t SValue
es



cjoin_pointers :: BinaryClass bin => Static bin v -> [SPointer] -> [SPointer]
cjoin_pointers :: forall bin v.
BinaryClass bin =>
Static bin v -> [SPointer] -> [SPointer]
cjoin_pointers fctxt :: Static bin v
fctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
entry) [SPointer]
es =
  case [SPointer] -> [SPointer]
forall a. Eq a => [a] -> [a]
nub [SPointer]
es of
    []  -> String -> [SPointer]
forall a. HasCallStack => String -> a
error (String -> [SPointer]) -> String -> [SPointer]
forall a b. (a -> b) -> a -> b
$ String
"Cannot join []"
    [SPointer
e] -> [SPointer
e]
    [SPointer]
es  -> 
      let bs :: [Maybe SimpleExpr]
bs = [Maybe SimpleExpr] -> [Maybe SimpleExpr]
forall a. Eq a => [a] -> [a]
nub ([Maybe SimpleExpr] -> [Maybe SimpleExpr])
-> [Maybe SimpleExpr] -> [Maybe SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Maybe SimpleExpr)
-> [SimpleExpr] -> [Maybe SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Static bin v -> SimpleExpr -> Maybe SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base Static bin v
fctxt) ([SimpleExpr] -> [Maybe SimpleExpr])
-> [SimpleExpr] -> [Maybe SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (SPointer -> SimpleExpr) -> [SPointer] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map SPointer -> SimpleExpr
ptr_to_expr [SPointer]
es in
        if Maybe SimpleExpr
forall a. Maybe a
Nothing Maybe SimpleExpr -> [Maybe SimpleExpr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe SimpleExpr]
bs then
          String -> [SPointer]
forall a. HasCallStack => String -> a
error (String -> [SPointer]) -> String -> [SPointer]
forall a b. (a -> b) -> a -> b
$ [SPointer] -> String
forall a. Show a => a -> String
show [SPointer]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((SPointer, SPointer) -> String)
-> [(SPointer, SPointer)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SPointer, SPointer) -> String
forall a. Show a => a -> String
show ([(SPointer, SPointer)] -> [String])
-> [(SPointer, SPointer)] -> [String]
forall a b. (a -> b) -> a -> b
$ ((SPointer, SPointer) -> [(SPointer, SPointer)])
-> [(SPointer, SPointer)] -> [(SPointer, SPointer)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SPointer, SPointer) -> [(SPointer, SPointer)]
mk [(SPointer
e0,SPointer
e1) | SPointer
e0 <- [SPointer]
es, SPointer
e1 <- [SPointer]
es]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\nFinit:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe (FInit SValue SPointer) -> String
forall a. Show a => a -> String
show ((FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
-> FInit SValue SPointer
forall a b. (a, b) -> a
fst ((FInit SValue SPointer,
  Maybe (FResult (Sstate SValue SPointer) v))
 -> FInit SValue SPointer)
-> Maybe
     (FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
-> Maybe (FInit SValue SPointer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word64
-> L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
-> Maybe
     (FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0)
        else
          (SimpleExpr -> SPointer) -> [SimpleExpr] -> [SPointer]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> SPointer
Ptr_Base ([SimpleExpr] -> [SPointer]) -> [SimpleExpr] -> [SPointer]
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> [SimpleExpr]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NESet SimpleExpr -> [SimpleExpr])
-> NESet SimpleExpr -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ Static bin v -> NESet SimpleExpr -> NESet SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> NESet SimpleExpr -> NESet SimpleExpr
group_immediates Static bin v
fctxt (NESet SimpleExpr -> NESet SimpleExpr)
-> NESet SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList ([SimpleExpr] -> NESet SimpleExpr)
-> [SimpleExpr] -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ (Maybe SimpleExpr -> SimpleExpr)
-> [Maybe SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map Maybe SimpleExpr -> SimpleExpr
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe SimpleExpr]
bs
 where
  mk :: (SPointer, SPointer) -> [(SPointer, SPointer)]
mk (SPointer
e0,SPointer
e1)
    | SPointer
e0 SPointer -> SPointer -> Bool
forall a. Eq a => a -> a -> Bool
== SPointer
e1 Bool -> Bool -> Bool
|| Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
forall bin v.
BinaryClass bin =>
Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
cseparate Static bin v
fctxt String
"" SPointer
e0 (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
1) SPointer
e1 (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
1) = []
    | Bool
otherwise = [(SPointer
e0,SPointer
e1)]

  ptr_to_expr :: SPointer -> SimpleExpr
ptr_to_expr (Ptr_Concrete SimpleExpr
e) = SimpleExpr
e
  ptr_to_expr (Ptr_Base SimpleExpr
b) = SimpleExpr
b








-- SYMBOLIC COMPUTATIONS
mk_expr :: BinaryClass bin => Static bin v -> SimpleExpr -> SimpleExpr
mk_expr :: forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
fctxt SimpleExpr
e = SimpleExpr -> SimpleExpr
simp SimpleExpr
e


svalue_plus :: Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus Static bin v
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"plus" (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 (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
fctxt Int
si v0 :: SValue
v0@(SAddends NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet SimpleExpr
es1)  = Static bin v -> NESet SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
(bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> NESet SimpleExpr -> SValue
mk_saddends Static bin v
fctxt (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 
svalue_plus Static bin v
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
_) SValue
v1 = Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus Static bin v
fctxt Int
si (Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"plus" SValue
v0) SValue
v1
svalue_plus Static bin v
fctxt Int
si SValue
v0 v1 :: SValue
v1@(SConcrete NESet SimpleExpr
_) = Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus Static bin v
fctxt Int
si SValue
v0 (Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"plus" SValue
v1)
svalue_plus Static bin v
fctxt Int
si v0 :: SValue
v0@(SAddends NESet SimpleExpr
es0) SValue
Top = SValue
v0
svalue_plus Static bin v
fctxt Int
si SValue
Top v1 :: SValue
v1@(SAddends NESet SimpleExpr
es0) = SValue
v1
svalue_plus Static bin v
_ Int
_      SValue
Top SValue
Top = SValue
Top



svalue_minus :: Static bin v -> Int -> SValue -> SValue -> SValue
svalue_minus Static bin v
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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 (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
_) SValue
_ = Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"minus" SValue
v0
svalue_minus Static bin v
fctxt Int
si v0 :: SValue
v0@(SAddends NESet SimpleExpr
_) SValue
_  = SValue
v0 -- TODO what v1 = ( x- ptr )
svalue_minus Static bin v
_ Int
_ SValue
Top SValue
_ = SValue
Top

svalue_and :: Static bin v -> Int -> SValue -> SValue -> SValue
svalue_and Static bin v
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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 (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
_ Int
_ SValue
_ SValue
_ = SValue
Top

svalue_unop :: Static bin v
-> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop Static bin v
fctxt String
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) = Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
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 (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
fctxt String
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SAddends  NESet SimpleExpr
as0) = String -> SValue -> SValue
forall {p} {a}. p -> a -> a
traceTop String
"unop" SValue
Top
svalue_unop Static bin v
fctxt String
msg SimpleExpr -> SimpleExpr
f SValue
Top = SValue
Top


svalue_takebits :: Static bin v -> Int -> SValue -> SValue
svalue_takebits Static bin v
fctxt Int
h   = Static bin v
-> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v
-> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop Static bin v
fctxt String
"takebits" (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
h)
svalue_sextend :: Static bin v -> Int -> Int -> SValue -> SValue
svalue_sextend  Static bin v
fctxt Int
l Int
h = Static bin v
-> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v
-> String -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop Static bin v
fctxt String
"sextend"  (Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h)

svalue_apply :: BinaryClass bin => Static bin v -> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply :: forall bin v.
BinaryClass bin =>
Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply Static bin v
fctxt String
msg [SimpleExpr] -> SimpleExpr
f [SValue]
es
  | (SValue -> Bool) -> [SValue] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (SValue -> Bool) -> SValue -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SValue -> Bool
isConcrete) [SValue]
es = String -> SValue -> SValue
forall {p} {a}. p -> a -> a
traceTop String
"svalue_apply" SValue
Top
  -- | Top `elem` es = Top
  | Bool
otherwise =
  let args :: [[SimpleExpr]]
args = (SValue -> [SimpleExpr]) -> [SValue] -> [[SimpleExpr]]
forall a b. (a -> b) -> [a] -> [b]
map SValue -> [SimpleExpr]
mk_args [SValue]
es
      prod :: [[SimpleExpr]]
prod = [[SimpleExpr]] -> [[SimpleExpr]]
forall a. [[a]] -> [[a]]
crossProduct [[SimpleExpr]]
args
      app :: [SimpleExpr]
app  = ([SimpleExpr] -> SimpleExpr) -> [[SimpleExpr]] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleExpr] -> SimpleExpr
f) [[SimpleExpr]]
prod in
    Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"apply" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList [SimpleExpr]
app 
 where
  mk_args :: SValue -> [SimpleExpr]
mk_args (SConcrete NESet SimpleExpr
es) = Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList (Set SimpleExpr -> [SimpleExpr]) -> Set SimpleExpr -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es

  isConcrete :: SValue -> Bool
isConcrete (SConcrete NESet SimpleExpr
es) = Bool
True
  isConcrete SValue
_ = Bool
False
  

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 :: BinaryClass bin => Static bin v -> String -> SymbolicOperation SValue -> SValue
---csemantics fctxt msg _ | trace ("csemantics: "++ msg) False = error "trace"
csemantics :: forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
msg (SO_Plus  SValue
a SValue
b)         = Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus Static bin v
fctxt Int
64 SValue
a SValue
b
csemantics Static bin v
fctxt String
msg (SO_Minus SValue
a SValue
b)         = Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_minus Static bin v
fctxt Int
64 SValue
a SValue
b
csemantics Static bin v
fctxt String
msg (SO_Times SValue
a SValue
b)         = Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
forall bin v.
BinaryClass bin =>
Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply Static bin v
fctxt String
"times" (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
fctxt String
msg (SO_Overwrite Int
n SValue
a SValue
b)   = Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
forall bin v.
BinaryClass bin =>
Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply Static bin v
fctxt String
"overwrite" (\[SimpleExpr
e0,SimpleExpr
e1] -> Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 Static bin v
fctxt String
msg (SO_SExtend Int
l Int
h SValue
a)     = Static bin v -> Int -> Int -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> Int -> SValue -> SValue
svalue_sextend Static bin v
fctxt Int
l Int
h SValue
a
csemantics Static bin v
fctxt String
msg (SO_Bit Int
h SValue
a)           = Static bin v -> Int -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue
svalue_takebits Static bin v
fctxt Int
h SValue
a
csemantics Static bin v
fctxt String
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. HasCallStack => [a] -> Int -> a
!!Int
0
    CSemantics
ApplyCMov        -> Static bin v -> String -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
(bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue -> SValue
cjoin        Static bin v
fctxt String
"cmov" ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
1)
    ApplyPlus  Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus  Static bin v
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
1)
    ApplyInc   Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_plus  Static bin v
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) (Static bin v -> Integer -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt Integer
1)
    ApplyMinus Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_minus Static bin v
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
1)
    ApplyDec   Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_minus Static bin v
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) (Static bin v -> Integer -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt Integer
1)
    ApplyNeg   Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_minus Static bin v
fctxt Int
si (Static bin v -> Integer -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt Integer
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0)
    ApplyAnd   Int
si    -> Static bin v -> Int -> SValue -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> SValue -> SValue -> SValue
svalue_and   Static bin v
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
1)
    ApplySExtend Int
l Int
h -> Static bin v -> Int -> Int -> SValue -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> Int -> Int -> SValue -> SValue
svalue_sextend Static bin v
fctxt Int
l Int
h ([SValue]
es[SValue] -> Int -> SValue
forall a. HasCallStack => [a] -> Int -> a
!!Int
0)
    Apply [SimpleExpr] -> SimpleExpr
sop        -> Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
forall bin v.
BinaryClass bin =>
Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply Static bin v
fctxt (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", op = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Opcode -> String
forall a. Show a => a -> String
show Opcode
op) (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleExpr] -> SimpleExpr
sop) [SValue]
es
    CSemantics
SetXX            -> Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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    -> Static bin v -> String -> NESet SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> NESet SimpleExpr -> SValue
mk_concrete Static bin v
fctxt String
"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      -> String -> SValue
mk_top (String
"Widening due to operand: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Opcode -> String
forall a. Show a => a -> String
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'    = String -> CSemantics
forall a. HasCallStack => String -> a
error (String -> CSemantics) -> String -> CSemantics
forall a b. (a -> b) -> a -> b
$ String
"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'     = CSemantics
NoSemantics -- Apply $ shl
 where
  shl :: [SimpleExpr] -> CSemantics
shl [SimpleExpr
a,SE_Immediate Word64
i] = CSemantics
NoSemantics -- SE_Op Times si [a,SE_Immediate $ 2^i]
  shl [SimpleExpr
a,SimpleExpr
b]              = CSemantics
NoSemantics -- SE_Op Shl si [a,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
SdivLo Int
si
mnemonic_to_semantics Opcode
SAR Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ sar
 where
  sar :: [SimpleExpr] -> CSemantics
sar [SimpleExpr
a,SE_Immediate Word64
i] = CSemantics
NoSemantics -- SE_Op Sdiv si [a,SE_Immediate $ 2^i]
  sar [SimpleExpr
a,SimpleExpr
b]              = CSemantics
NoSemantics -- SE_Op Sar si [a,b]


mnemonic_to_semantics Opcode
DIV_LO Int
si Maybe Int
si'  = CSemantics
NoSemantics -- Apply $ SE_Op UdivLo si
mnemonic_to_semantics Opcode
SHR Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ shr
 where
  shr :: [SimpleExpr] -> CSemantics
shr [SimpleExpr
a,SE_Immediate Word64
i] = CSemantics
NoSemantics -- SE_Op Udiv si [a,SE_Immediate $ 2^i]
  shr [SimpleExpr
a,SimpleExpr
b]              = CSemantics
NoSemantics -- SE_Op Shr si [a,b]



mnemonic_to_semantics Opcode
BSR Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ (\[a] -> SE_Op Bsr si [SE_Immediate 0,a])
mnemonic_to_semantics Opcode
ROL Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ SE_Op Rol si
mnemonic_to_semantics Opcode
ROR Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ SE_Op Ror si
mnemonic_to_semantics Opcode
BSWAP Int
si Maybe Int
si'   = CSemantics
NoSemantics -- Apply $ SE_Op Bswap si

mnemonic_to_semantics Opcode
PEXTRB Int
si Maybe Int
si'  = CSemantics
NoSemantics -- Apply $ (\[a,b,c] -> SE_Op Pextr si [a,b,c])
mnemonic_to_semantics Opcode
PEXTRD Int
si Maybe Int
si'  = CSemantics
NoSemantics -- Apply $ (\[a,b,c] -> SE_Op Pextr si [a,b,c])
mnemonic_to_semantics Opcode
PEXTRQ Int
si Maybe Int
si'  = CSemantics
NoSemantics -- Apply $ (\[a,b,c] -> SE_Op Pextr si [a,b,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'     = CSemantics
NoSemantics -- Apply $ SE_Op Or si
mnemonic_to_semantics Opcode
NOT Int
si Maybe Int
si'     = CSemantics
NoSemantics -- Apply $ (\[a] -> SE_Op Not si [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 -- TODO only if string operation
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 -- TODO if prefix = Nothing?
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
--TODO TEST
--TODO other sign extension thingies
mnemonic_to_semantics Opcode
_      Int
_ Maybe Int
_  = CSemantics
NoSemantics




replace_rip_in_operand :: a -> Operand -> Operand
replace_rip_in_operand a
rip op :: Operand
op@(Op_Mem BitSize
si BitSize
aSi (Reg64 GPR
RIP) Register
RegNone Word8
0 Int
displ Maybe SReg
Nothing) = BitSize
-> BitSize
-> Register
-> Register
-> Word8
-> Int
-> Maybe SReg
-> Operand
Op_Mem BitSize
si BitSize
aSi Register
RegNone Register
RegNone Word8
0 (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
rip Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
displ) Maybe SReg
forall a. Maybe a
Nothing
replace_rip_in_operand a
rip op :: Operand
op@(Op_Mem BitSize
si BitSize
aSi (Reg64 GPR
RIP) Register
_ Word8
_ Int
displ Maybe SReg
Nothing) = String -> Operand
forall a. HasCallStack => String -> a
error (String -> Operand) -> String -> Operand
forall a b. (a -> b) -> a -> b
$ String
"TODO: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
op
replace_rip_in_operand a
rip Operand
op = Operand
op



cflg_semantics :: BinaryClass bin => Static bin v -> a -> Instruction -> FlagStatus -> FlagStatus
cflg_semantics :: forall bin v a.
BinaryClass bin =>
Static bin v -> a -> Instruction -> FlagStatus -> FlagStatus
cflg_semantics Static bin v
fctxt a
_ i :: Instruction
i@(Instruction Word64
label [Prefix]
prefix Opcode
mnemonic Maybe Operand
dst [Operand]
srcs Int
annot) FlagStatus
flgs = Opcode -> FlagStatus
flg Opcode
mnemonic
 where
  flg :: Opcode -> FlagStatus
flg Opcode
CMP      = Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP Maybe Bool
forall a. Maybe a
Nothing (Word64 -> Operand -> Operand
forall {a}. Integral a => a -> Operand -> Operand
replace_rip_in_operand (Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ Instruction -> Int
inSize Instruction
i)) (Operand -> Operand) -> Operand -> Operand
forall a b. (a -> b) -> a -> b
$ [Operand]
srcs[Operand] -> Int -> Operand
forall a. HasCallStack => [a] -> Int -> a
!!Int
0) (Word64 -> Operand -> Operand
forall {a}. Integral a => a -> Operand -> Operand
replace_rip_in_operand (Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ Instruction -> Int
inSize Instruction
i)) (Operand -> Operand) -> Operand -> Operand
forall a b. (a -> b) -> a -> b
$ [Operand]
srcs[Operand] -> Int -> Operand
forall a. HasCallStack => [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
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 -- TODO




-- MAKING POINTERS FROM EXPRESSIONS


try_get_base :: BinaryClass bin => Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base :: forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base (bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
entry) SimpleExpr
a = (Set PointerBase -> Maybe SimpleExpr
mk_base (Set PointerBase -> Maybe SimpleExpr)
-> Set PointerBase -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
get_finit SimpleExpr
a) Maybe SimpleExpr -> Maybe SimpleExpr -> Maybe SimpleExpr
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` ([SimpleExpr] -> Maybe SimpleExpr
try_mk_addition ([SimpleExpr] -> Maybe SimpleExpr)
-> [SimpleExpr] -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Bool) -> [SimpleExpr] -> [SimpleExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter SimpleExpr -> Bool
is_possible_base ([SimpleExpr] -> [SimpleExpr]) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ Map SimpleExpr Word64 -> [SimpleExpr]
forall k a. Map k a -> [k]
M.keys (Map SimpleExpr Word64 -> [SimpleExpr])
-> Map SimpleExpr Word64 -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Bool) -> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
1) (Map SimpleExpr Word64 -> Map SimpleExpr Word64)
-> Map SimpleExpr Word64 -> Map SimpleExpr Word64
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Map SimpleExpr Word64
addends SimpleExpr
a)  -- `orTry` null_pointer a
 where
  mk_base :: S.Set PointerBase -> Maybe SimpleExpr
  mk_base :: Set PointerBase -> Maybe SimpleExpr
mk_base Set PointerBase
bs
    | Set PointerBase -> Bool
forall a. Set a -> Bool
S.null Set PointerBase
bs = Maybe SimpleExpr
forall a. Maybe a
Nothing
    | Bool
otherwise = SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just (SimpleExpr -> Maybe SimpleExpr) -> SimpleExpr -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> Set SimpleExpr -> SimpleExpr
forall a. (a -> a -> a) -> Set a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SimpleExpr -> SimpleExpr -> SimpleExpr
plus (Set SimpleExpr -> SimpleExpr) -> Set SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ (PointerBase -> SimpleExpr) -> Set PointerBase -> Set SimpleExpr
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map PointerBase -> SimpleExpr
base_to_expr Set PointerBase
bs

  try_mk_addition :: [SimpleExpr] -> Maybe SimpleExpr
  try_mk_addition :: [SimpleExpr] -> Maybe SimpleExpr
try_mk_addition [] = Maybe SimpleExpr
forall a. Maybe a
Nothing
  try_mk_addition [SimpleExpr]
as = SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just (SimpleExpr -> Maybe SimpleExpr) -> SimpleExpr -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> [SimpleExpr] -> SimpleExpr
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SimpleExpr -> SimpleExpr -> SimpleExpr
plus [SimpleExpr]
as
  plus :: SimpleExpr -> SimpleExpr -> SimpleExpr
plus SimpleExpr
a SimpleExpr
b = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
64 [SimpleExpr
a,SimpleExpr
b]

    
  is_possible_base :: SimpleExpr -> Bool
is_possible_base (SE_Var StatePart
sp) = Bool
True
  is_possible_base (Bottom (FromCall String
f)) = Bool
True
  is_possible_base SimpleExpr
_ = Bool
False

  get_finit :: FInit SValue SPointer
get_finit =
    case Word64
-> L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
-> Maybe
     (FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0 of
      Just (FInit SValue SPointer
finit,Maybe (FResult (Sstate SValue SPointer) v)
_) -> FInit SValue SPointer
finit

  null_pointer :: SimpleExpr -> Maybe SimpleExpr
null_pointer a :: SimpleExpr
a@(SE_Immediate Word64
imm) = if Word64
imm Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
100 then SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just SimpleExpr
a else Maybe SimpleExpr
forall a. Maybe a
Nothing
  null_pointer SimpleExpr
_ = Maybe SimpleExpr
forall a. Maybe a
Nothing


base_to_expr :: PointerBase -> SimpleExpr
base_to_expr (PointerBase
StackPointer)        = StatePart -> SimpleExpr
SE_Var(StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Register -> StatePart
SP_Reg (GPR -> Register
Reg64 GPR
RSP)
base_to_expr (Malloc Maybe Word64
id Maybe String
hash)      = Maybe Word64 -> Maybe String -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe String
hash
base_to_expr (GlobalAddress Word64
a)     = Word64 -> SimpleExpr
SE_Immediate Word64
a
base_to_expr PointerBase
ThreadLocalStorage    = StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg (Register -> StatePart) -> Register -> StatePart
forall a b. (a -> b) -> a -> b
$ SReg -> Register
RegSeg SReg
FS)
base_to_expr (BaseIsStatePart StatePart
sp)  = StatePart -> SimpleExpr
SE_Var StatePart
sp


cmk_mem_addresses :: BinaryClass bin => Static bin v -> String -> SValue -> S.Set SPointer
cmk_mem_addresses :: forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses l :: Static bin v
l@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
entry) String
msg v :: SValue
v@(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 -> Bool
could_be_pointer NESet SimpleExpr
es
      bs :: Set (Maybe SimpleExpr)
bs  = (SimpleExpr -> Maybe SimpleExpr)
-> Set SimpleExpr -> Set (Maybe SimpleExpr)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Static bin v -> SimpleExpr -> Maybe SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base Static bin v
l) Set SimpleExpr
es' in
    if (Maybe SimpleExpr -> Bool) -> Set (Maybe SimpleExpr) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe SimpleExpr -> Maybe SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
(==) Maybe SimpleExpr
forall a. Maybe a
Nothing) Set (Maybe SimpleExpr)
bs then -- TODO check if all is OK
      Set SPointer
forall a. Set a
S.empty
    else
      (SimpleExpr -> SPointer) -> Set SimpleExpr -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> SPointer
Ptr_Concrete Set SimpleExpr
es'
 where
  could_be_pointer :: SimpleExpr -> Bool
could_be_pointer (SE_Immediate Word64
imm) = bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
forall bin.
BinaryClass bin =>
bin -> Word64 -> Maybe (String, String, Word64, Word64, Word64)
find_section_for_address bin
bin Word64
imm Maybe (String, String, Word64, Word64, Word64)
-> Maybe (String, String, Word64, Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (String, String, Word64, Word64, Word64)
forall a. Maybe a
Nothing
  could_be_pointer SimpleExpr
_ = Bool
True
cmk_mem_addresses Static bin v
fctxt String
msg v :: SValue
v@(SAddends NESet SimpleExpr
as) = 
  let bs :: NESet (Maybe SimpleExpr)
bs = (SimpleExpr -> Maybe SimpleExpr)
-> NESet SimpleExpr -> NESet (Maybe SimpleExpr)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SimpleExpr -> Maybe SimpleExpr
try_get_base_from_addends NESet SimpleExpr
as in
    if (Maybe SimpleExpr -> Bool) -> NESet (Maybe SimpleExpr) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe SimpleExpr -> Maybe SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
(==) Maybe SimpleExpr
forall a. Maybe a
Nothing) NESet (Maybe SimpleExpr)
bs then
     Set SPointer
forall a. Set a
S.empty
    else
      (Maybe SimpleExpr -> SPointer)
-> Set (Maybe SimpleExpr) -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (SimpleExpr -> SPointer
Ptr_Base (SimpleExpr -> SPointer)
-> (Maybe SimpleExpr -> SimpleExpr) -> Maybe SimpleExpr -> SPointer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SimpleExpr -> SimpleExpr
forall a. HasCallStack => Maybe a -> a
fromJust) (Set (Maybe SimpleExpr) -> Set SPointer)
-> Set (Maybe SimpleExpr) -> Set SPointer
forall a b. (a -> b) -> a -> b
$ NESet (Maybe SimpleExpr) -> Set (Maybe SimpleExpr)
forall a. NESet a -> Set a
NES.toSet NESet (Maybe SimpleExpr)
bs
 where
  try_get_base_from_addends :: SimpleExpr -> Maybe SimpleExpr
try_get_base_from_addends SimpleExpr
a = Static bin v -> SimpleExpr -> Maybe SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> Maybe SimpleExpr
try_get_base Static bin v
fctxt SimpleExpr
a



cmk_mem_addresses Static bin v
_ String
_ SValue
Top = Set SPointer
forall a. Set a
S.empty


-- MAKING INITIAL VALUES

cmk_init_reg_value :: BinaryClass bin => Static bin v  -> Register -> SValue
cmk_init_reg_value :: forall bin v. BinaryClass bin => Static bin v -> Register -> SValue
cmk_init_reg_value Static bin v
fctxt = Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
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


-- Concert SValues to SExpressions
cmk_init_mem_value :: BinaryClass bin => Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value :: forall bin v.
BinaryClass bin =>
Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value Static bin v
fctxt String
msg (Ptr_Concrete SimpleExpr
a) Maybe ByteSize
si = Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
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
a (Int -> StatePart) -> Int -> StatePart
forall a b. (a -> b) -> a -> b
$ Maybe ByteSize -> Int
mk_si Maybe ByteSize
si
 where
  mk_si :: Maybe ByteSize -> Int
mk_si (Just (ByteSize Int
imm)) = Int
imm
cmk_init_mem_value Static bin v
fctxt String
msg (Ptr_Base SimpleExpr
b) Maybe ByteSize
si = SValue
Top





-- MEMORY RELATIONS
cseparate :: BinaryClass bin => Static bin v -> String -> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
---cseparate fctxt msg v0 s0 v1 si1 | trace ("cseparate: "++ show (v0,v1)) False = error "trace"
cseparate :: forall bin v.
BinaryClass bin =>
Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
cseparate ctxt :: Static bin v
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) String
msg (Ptr_Concrete SimpleExpr
a0) Maybe ByteSize
si0 (Ptr_Concrete SimpleExpr
a1) Maybe ByteSize
si1 = bin
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate bin
bin (Static bin v -> FInit SValue SPointer
forall {a} {a} {b} {pred} {finit} {v}.
Integral a =>
(a, b, L0 pred finit v, a) -> finit
lookup_finit Static bin v
ctxt) String
msg SimpleExpr
a0 (Maybe ByteSize -> Maybe SimpleExpr
mk_si Maybe ByteSize
si0) SimpleExpr
a1 (Maybe ByteSize -> Maybe SimpleExpr
mk_si Maybe ByteSize
si1)
 where
  mk_si :: Maybe ByteSize -> Maybe SimpleExpr
mk_si (Just (ByteSize Int
si)) = SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just (SimpleExpr -> Maybe SimpleExpr) -> SimpleExpr -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si
  mk_si Maybe ByteSize
_                    = Maybe SimpleExpr
forall a. Maybe a
Nothing
cseparate ctxt :: Static bin v
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) String
msg (Ptr_Base SimpleExpr
a0)     Maybe ByteSize
si0 (Ptr_Base SimpleExpr
a1)     Maybe ByteSize
si1 = bin
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate bin
bin (Static bin v -> FInit SValue SPointer
forall {a} {a} {b} {pred} {finit} {v}.
Integral a =>
(a, b, L0 pred finit v, a) -> finit
lookup_finit Static bin v
ctxt) String
msg SimpleExpr
a0 Maybe SimpleExpr
forall a. Maybe a
Nothing SimpleExpr
a1 Maybe SimpleExpr
forall a. Maybe a
Nothing
cseparate ctxt :: Static bin v
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) String
msg (Ptr_Base SimpleExpr
a0)     Maybe ByteSize
si0 (Ptr_Concrete SimpleExpr
a1) Maybe ByteSize
si1 = bin
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate bin
bin (Static bin v -> FInit SValue SPointer
forall {a} {a} {b} {pred} {finit} {v}.
Integral a =>
(a, b, L0 pred finit v, a) -> finit
lookup_finit Static bin v
ctxt) String
msg SimpleExpr
a0 Maybe SimpleExpr
forall a. Maybe a
Nothing SimpleExpr
a1 Maybe SimpleExpr
forall a. Maybe a
Nothing
cseparate ctxt :: Static bin v
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) String
msg (Ptr_Concrete SimpleExpr
a0) Maybe ByteSize
si0 (Ptr_Base SimpleExpr
a1)     Maybe ByteSize
si1 = bin
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
forall {p}.
BinaryClass p =>
p
-> FInit SValue SPointer
-> String
-> SimpleExpr
-> Maybe SimpleExpr
-> SimpleExpr
-> Maybe SimpleExpr
-> Bool
necessarily_separate bin
bin (Static bin v -> FInit SValue SPointer
forall {a} {a} {b} {pred} {finit} {v}.
Integral a =>
(a, b, L0 pred finit v, a) -> finit
lookup_finit Static bin v
ctxt) String
msg SimpleExpr
a0 Maybe SimpleExpr
forall a. Maybe a
Nothing SimpleExpr
a1 Maybe SimpleExpr
forall a. Maybe a
Nothing
cseparate Static bin v
ctxt String
msg SPointer
Ptr_Top Maybe ByteSize
_ SPointer
_ Maybe ByteSize
_ = Bool
False
cseparate Static bin v
ctxt String
msg SPointer
_ Maybe ByteSize
_ SPointer
Ptr_Top Maybe ByteSize
_ = Bool
False

lookup_finit :: (a, b, L0 pred finit v, a) -> finit
lookup_finit (a
bin,b
_,L0 pred finit v
l0,a
entry) = 
  case a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry a
entry L0 pred finit v
l0 of
    Just (finit
finit,Maybe (FResult pred v)
_) -> finit
finit

calias :: p -> a -> a -> a -> a -> Bool
calias p
fctxt a
a0 a
si0 a
a1 a
si1 = a
si0a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==a
si1 Bool -> Bool -> Bool
&& a
a0a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==a
a1 -- necessarily_equal a0 a1


cnecessarily_enclosed :: p
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
cnecessarily_enclosed p
fctxt (Ptr_Concrete SimpleExpr
a0) (Just (ByteSize Int
si0)) (Ptr_Concrete SimpleExpr
a1) (Just (ByteSize Int
si1)) = SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall {p}.
Integral p =>
SimpleExpr -> p -> SimpleExpr -> p -> Bool
necessarily_enclosed SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
cnecessarily_enclosed p
_ SPointer
_ Maybe ByteSize
_ SPointer
_ Maybe ByteSize
_ = Bool
False


csensitive :: (p, b, c, d) -> SPointer -> Maybe ByteSize -> SValue -> Bool
csensitive (p
bin,b
_,c
_,d
_) (Ptr_Concrete SimpleExpr
a) (Just (ByteSize Int
si)) SValue
v = SimpleExpr -> Maybe ByteSize -> Bool
is_top_stackframe SimpleExpr
a (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (Int -> ByteSize
ByteSize Int
si)) Bool -> Bool -> Bool
|| SimpleExpr -> SValue -> Bool
is_pushed_reg SimpleExpr
a SValue
v Bool -> Bool -> Bool
|| p -> SValue -> Bool
forall {p}. BinaryClass p => p -> SValue -> Bool
is_function_pointer p
bin SValue
v
 where
  is_initial_reg :: SimpleExpr -> Bool
is_initial_reg (SE_Var (SP_Reg Register
_)) = Bool
True
  is_initial_reg SimpleExpr
_                   = Bool
False
  
  is_pushed_reg :: SimpleExpr -> SValue -> Bool
is_pushed_reg SimpleExpr
a' (SConcrete NESet SimpleExpr
vs) = (SimpleExpr -> Bool) -> NESet SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SimpleExpr -> Bool
is_initial_reg NESet SimpleExpr
vs Bool -> Bool -> Bool
&& p -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer p
bin SimpleExpr
a'
  is_pushed_reg SimpleExpr
a' SValue
_ = Bool
False

csensitive (p, b, c, d)
fctxt SPointer
_ Maybe ByteSize
_ SValue
_ = Bool
False


cread_from_ro_data :: BinaryClass bin => Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue
cread_from_ro_data :: forall bin v.
BinaryClass bin =>
Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue
cread_from_ro_data fctxt :: Static bin v
fctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) p :: SPointer
p@(Ptr_Concrete (SE_Immediate Word64
a)) (Just (ByteSize Int
si)) = Word64 -> Int -> Maybe SValue
try_read_reloc Word64
a Int
si Maybe SValue -> Maybe SValue -> Maybe SValue
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` Word64 -> Int -> Maybe SValue
forall {a}. Integral a => a -> Int -> Maybe SValue
try_read_symbol Word64
a Int
si Maybe SValue -> Maybe SValue -> Maybe SValue
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` Word64 -> Int -> Maybe SValue
forall {a}. Integral a => Word64 -> a -> Maybe SValue
try_read_ro_data Word64
a Int
si
 where
  try_read_ro_data :: Word64 -> a -> Maybe SValue
try_read_ro_data Word64
a a
si = Static bin v -> Word64 -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt (Word64 -> SValue) -> Maybe Word64 -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bin -> Word64 -> Int -> Maybe Word64
forall bin. BinaryClass bin => bin -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection bin
bin Word64
a (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
si)

  try_read_reloc :: Word64 -> Int -> Maybe SValue
try_read_reloc Word64
a Int
si =
    case (Relocation -> Bool) -> [Relocation] -> Maybe Relocation
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> Relocation -> Bool
is_reloc_for Word64
a) ([Relocation] -> Maybe Relocation)
-> [Relocation] -> Maybe Relocation
forall a b. (a -> b) -> a -> b
$ Set Relocation -> [Relocation]
forall a. Set a -> [a]
S.toList (Set Relocation -> [Relocation]) -> Set Relocation -> [Relocation]
forall a b. (a -> b) -> a -> b
$ bin -> Set Relocation
forall a. BinaryClass a => a -> Set Relocation
binary_get_relocations bin
bin of
      Just (Relocation Word64
_ Word64
a') -> SValue -> Maybe SValue
forall a. a -> Maybe a
Just (SValue -> Maybe SValue) -> SValue -> Maybe SValue
forall a b. (a -> b) -> a -> b
$ Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value Static bin v
fctxt String
"reloc" SPointer
p (Maybe ByteSize -> SValue) -> Maybe ByteSize -> SValue
forall a b. (a -> b) -> a -> b
$ ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si
      Maybe Relocation
Nothing -> Maybe SValue
forall a. Maybe a
Nothing

  is_reloc_for :: Word64 -> Relocation -> Bool
is_reloc_for Word64
a (Relocation Word64
a' Word64
_) = Word64
a Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a'


  try_read_symbol :: a -> Int -> Maybe SValue
try_read_symbol a
a Int
si = 
    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
$ bin -> IntMap Symbol
forall {a}. BinaryClass a => a -> IntMap Symbol
binary_get_symbol_table bin
bin of
      Just (PointerToLabel String
f Bool
True)  -> SValue -> Maybe SValue
forall a. a -> Maybe a
Just (SValue -> Maybe SValue) -> SValue -> Maybe SValue
forall a b. (a -> b) -> a -> b
$ Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value Static bin v
fctxt String
"reloc" SPointer
p (Maybe ByteSize -> SValue) -> Maybe ByteSize -> SValue
forall a b. (a -> b) -> a -> b
$ ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si
      Just (PointerToObject String
f Bool
True) -> SValue -> Maybe SValue
forall a. a -> Maybe a
Just (SValue -> Maybe SValue) -> SValue -> Maybe SValue
forall a b. (a -> b) -> a -> b
$ Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value Static bin v
fctxt String
"reloc" SPointer
p (Maybe ByteSize -> SValue) -> Maybe ByteSize -> SValue
forall a b. (a -> b) -> a -> b
$ ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si
      --Just s                        -> error $ show (a, s) -- Just $ External f
      Maybe Symbol
_                             -> Maybe SValue
forall a. Maybe a
Nothing


cread_from_ro_data Static bin v
_ SPointer
_ Maybe ByteSize
_ = Maybe SValue
forall a. Maybe a
Nothing


cis_local :: (bin, b, c, d) -> SPointer -> Bool
cis_local (bin
bin,b
_,c
_,d
_) (Ptr_Concrete SimpleExpr
a) = bin -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_local_pointer bin
bin SimpleExpr
a
cis_local (bin
bin,b
_,c
_,d
_) (Ptr_Base SimpleExpr
a) = bin -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_local_pointer bin
bin SimpleExpr
a
cis_local (bin, b, c, d)
_ SPointer
Ptr_Top = Bool
False

ckeep_for_finit :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> SStatePart SPointer -> SValue -> Maybe (Set SPointer)
ckeep_for_finit ctxt :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) (SSP_Reg Register
r) SValue
v 
  | Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [GPR -> Register
Reg64 GPR
RSP,GPR -> Register
Reg64 GPR
RIP,GPR -> Register
Reg64 GPR
RBP] Bool -> Bool -> Bool
&& bin -> SValue -> Bool
forall {p}. BinaryClass p => p -> SValue -> Bool
is_function_pointer bin
bin SValue
v = Set SPointer -> Maybe (Set SPointer)
forall a. a -> Maybe a
Just (Set SPointer -> Maybe (Set SPointer))
-> Set SPointer -> Maybe (Set SPointer)
forall a b. (a -> b) -> a -> b
$ (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
ctxt String
"finit" SValue
v 
  | Bool
otherwise = Maybe (Set SPointer)
forall a. Maybe a
Nothing
ckeep_for_finit ctxt :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
ctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) (SSP_Mem SPointer
a Int
si) SValue
v = 
  case SPointer
a of
    Ptr_Concrete (SE_Immediate Word64
_) -> if bin -> SValue -> Bool
forall {p}. BinaryClass p => p -> SValue -> Bool
is_function_pointer bin
bin SValue
v then Set SPointer -> Maybe (Set SPointer)
forall a. a -> Maybe a
Just (Set SPointer -> Maybe (Set SPointer))
-> Set SPointer -> Maybe (Set SPointer)
forall a b. (a -> b) -> a -> b
$ (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
ctxt String
"finit" SValue
v else Maybe (Set SPointer)
forall a. Maybe a
Nothing
    SPointer
_ -> Maybe (Set SPointer)
forall a. Maybe a
Nothing


is_function_pointer :: p -> SValue -> Bool
is_function_pointer p
bin (SConcrete NESet SimpleExpr
vs) = (SimpleExpr -> Bool) -> NESet SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SimpleExpr -> Bool
is_function_pointer_expr NESet SimpleExpr
vs
 where
  is_function_pointer_expr :: SimpleExpr -> Bool
is_function_pointer_expr (SE_Immediate Word64
imm) = p -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
address_has_instruction p
bin Word64
imm
  is_function_pointer_expr SimpleExpr
_                  = Bool
False
is_function_pointer p
bin SValue
_              = Bool
False

check_regs_in_postcondition :: BinaryClass bin => Static bin v -> SValue -> SValue -> Bool
check_regs_in_postcondition :: forall bin v.
BinaryClass bin =>
Static bin v -> SValue -> SValue -> Bool
check_regs_in_postcondition Static bin v
ctxt SValue
rip SValue
rsp = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ SValue -> Bool
rsp_check SValue
rsp, SValue -> Bool
rip_check SValue
rip ]
 where
  -- check: is RSP restored to RSP_0 + 8 ?
  rsp_check :: SValue -> Bool
rsp_check rsp :: SValue
rsp@(SConcrete NESet SimpleExpr
es)
    | SValue -> Bool
cis_deterministic SValue
rsp = SimpleExpr -> Bool
rsp_check_value (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
    | Bool
otherwise = Bool
False
  rsp_check SValue
_ = Bool
False


  rsp_check_value :: SimpleExpr -> Bool
rsp_check_value (SE_Op Operator
Plus Int
_ [SE_Var (SP_Reg (Reg64 GPR
RSP)), SE_Immediate Word64
0x8]) = Bool
True 
  rsp_check_value (SE_Op Operator
Minus Int
_ [SE_Var (SP_Reg (Reg64 GPR
RSP)), SE_Immediate Word64
0xfffffffffffffff8]) = Bool
True 
  rsp_check_value SimpleExpr
_ = Bool
False


  -- check: is RIP set to the value originally stored at the top of the stack frame?
  rip_check :: SValue -> Bool
rip_check rip :: SValue
rip@(SConcrete NESet SimpleExpr
es)
    | SValue -> Bool
cis_deterministic SValue
rip = SimpleExpr -> Bool
rip_check_value (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
    | Bool
otherwise = Bool
False
  rip_check SValue
_ = Bool
False


  rip_check_value :: SimpleExpr -> Bool
rip_check_value (SE_Var (SP_Mem (SE_Var (SP_Reg (Reg64 GPR
RSP))) Int
8)) = Bool
True
  rip_check_value SimpleExpr
_ = Bool
False


ctry_resolve_error_call :: (bin, Config, L0 pred finit v, d)
-> Instruction -> SValue -> Maybe Indirection
ctry_resolve_error_call ctxt :: (bin, Config, L0 pred finit v, d)
ctxt@(bin
bin,Config
config,L0 pred finit v
l0,d
_) Instruction
i SValue
rdi
  | Opcode -> Bool
isCall (Instruction -> Opcode
inOperation Instruction
i) Bool -> Bool -> Bool
|| (Opcode -> Bool
isJump (Instruction -> Opcode
inOperation Instruction
i) Bool -> Bool -> Bool
&& Lifting bin pred finit v -> Instruction -> Bool
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> Bool
jump_is_actually_a_call (bin
bin,Config
config,L0 pred finit v
l0) Instruction
i) =
    case bin -> Instruction -> ResolvedJumpTarget
forall bin.
BinaryClass bin =>
bin -> Instruction -> ResolvedJumpTarget
jump_target_for_instruction bin
bin Instruction
i of
      External String
"error" ->
        case SValue -> Maybe Word64
ctry_immediate SValue
rdi of
          Just Word64
imm -> Indirection -> Maybe Indirection
forall a. a -> Maybe a
Just (Indirection -> Maybe Indirection)
-> Indirection -> Maybe Indirection
forall a b. (a -> b) -> a -> b
$ ResolvedJumpTarget -> Indirection
Indirection_Resolved (ResolvedJumpTarget -> Indirection)
-> ResolvedJumpTarget -> Indirection
forall a b. (a -> b) -> a -> b
$ Bool -> ResolvedJumpTarget
Returns (Word64
immWord64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
==Word64
0)
          Maybe Word64
Nothing  -> Indirection -> Maybe Indirection
forall a. a -> Maybe a
Just (Indirection -> Maybe Indirection)
-> Indirection -> Maybe Indirection
forall a b. (a -> b) -> a -> b
$ ResolvedJumpTarget -> Indirection
Indirection_Resolved (ResolvedJumpTarget -> Indirection)
-> ResolvedJumpTarget -> Indirection
forall a b. (a -> b) -> a -> b
$ Bool -> ResolvedJumpTarget
Returns Bool
True
      ResolvedJumpTarget
_ -> Maybe Indirection
forall a. Maybe a
Nothing
  | Bool
otherwise = Maybe Indirection
forall a. Maybe a
Nothing

instance BinaryClass bin => WithAbstractSymbolicValues (Static bin v) SValue SPointer where
  sseparate :: Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
sseparate                = Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
forall bin v.
BinaryClass bin =>
Static bin v
-> String
-> SPointer
-> Maybe ByteSize
-> SPointer
-> Maybe ByteSize
-> Bool
cseparate
  senclosed :: Static bin v
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
senclosed                = Static bin v
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
forall {p}.
p
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
cnecessarily_enclosed
  salias :: Static bin v
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
salias                   = Static bin v
-> SPointer -> Maybe ByteSize -> SPointer -> Maybe ByteSize -> Bool
forall {a} {a} {p}. (Eq a, Eq a) => p -> a -> a -> a -> a -> Bool
calias
  ssensitive :: Static bin v -> SPointer -> Maybe ByteSize -> SValue -> Bool
ssensitive               = Static bin v -> SPointer -> Maybe ByteSize -> SValue -> Bool
forall {p} {b} {c} {d}.
BinaryClass p =>
(p, b, c, d) -> SPointer -> Maybe ByteSize -> SValue -> Bool
csensitive
  sread_from_ro_data :: Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue
sread_from_ro_data       = Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue
forall bin v.
BinaryClass bin =>
Static bin v -> SPointer -> Maybe ByteSize -> Maybe SValue
cread_from_ro_data
  smk_mem_addresses :: Static bin v -> String -> SValue -> Set SPointer
smk_mem_addresses        = Static bin v -> String -> SValue -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses
  sjoin_values :: forall (t :: * -> *).
Foldable t =>
Static bin v -> String -> t SValue -> SValue
sjoin_values             = Static bin v -> String -> t SValue -> SValue
forall (t :: * -> *) bin v.
(Foldable t, BinaryClass bin) =>
Static bin v -> String -> t SValue -> SValue
cjoin_all
  swiden_values :: Static bin v -> String -> SValue -> SValue
swiden_values            = Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden
  sjoin_pointers :: Static bin v -> [SPointer] -> [SPointer]
sjoin_pointers           = Static bin v -> [SPointer] -> [SPointer]
forall bin v.
BinaryClass bin =>
Static bin v -> [SPointer] -> [SPointer]
cjoin_pointers
  ssemantics :: Static bin v -> String -> SymbolicOperation SValue -> SValue
ssemantics               = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics
  sflg_semantics :: Static bin v -> SValue -> Instruction -> FlagStatus -> FlagStatus
sflg_semantics           = Static bin v -> SValue -> Instruction -> FlagStatus -> FlagStatus
forall bin v a.
BinaryClass bin =>
Static bin v -> a -> Instruction -> FlagStatus -> FlagStatus
cflg_semantics
  simmediate :: forall i. Integral i => Static bin v -> i -> SValue
simmediate               = Static bin v -> i -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate
  top :: Static bin v -> String -> SValue
top                      = \Static bin v
_ -> String -> SValue
mk_top
  smk_init_reg_value :: Static bin v -> Register -> SValue
smk_init_reg_value       = Static bin v -> Register -> SValue
forall bin v. BinaryClass bin => Static bin v -> Register -> SValue
cmk_init_reg_value
  smk_init_mem_value :: Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
smk_init_mem_value       = Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SPointer -> Maybe ByteSize -> SValue
cmk_init_mem_value
  skeep_for_finit :: Static bin v
-> SStatePart SPointer -> SValue -> Maybe (Set SPointer)
skeep_for_finit          = Static bin v
-> SStatePart SPointer -> SValue -> Maybe (Set SPointer)
forall bin v.
BinaryClass bin =>
Static bin v
-> SStatePart SPointer -> SValue -> Maybe (Set SPointer)
ckeep_for_finit
  sjump :: Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
sjump                    = Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
forall bin v.
BinaryClass bin =>
Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
jump
  scall :: Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
scall                    = Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
forall bin v.
BinaryClass bin =>
Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
call
  stry_jump_targets :: Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget)
stry_jump_targets        = Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget)
forall bin v.
BinaryClass bin =>
Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets
  stry_immediate :: Static bin v -> SValue -> Maybe Word64
stry_immediate           = \Static bin v
_ -> SValue -> Maybe Word64
ctry_immediate 
  sis_deterministic :: Static bin v -> SValue -> Bool
sis_deterministic        = \Static bin v
_ -> SValue -> Bool
cis_deterministic 
  saddress_has_instruction :: Static bin v -> Word64 -> Bool
saddress_has_instruction = \(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_)-> bin -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
address_has_instruction bin
bin
  scheck_regs_in_postcondition :: Static bin v -> SValue -> SValue -> Bool
scheck_regs_in_postcondition = Static bin v -> SValue -> SValue -> Bool
forall bin v.
BinaryClass bin =>
Static bin v -> SValue -> SValue -> Bool
check_regs_in_postcondition
  stry_resolve_error_call :: Static bin v -> Instruction -> SValue -> Maybe Indirection
stry_resolve_error_call  = Static bin v -> Instruction -> SValue -> Maybe Indirection
forall {bin} {pred} {finit} {v} {d}.
BinaryClass bin =>
(bin, Config, L0 pred finit v, d)
-> Instruction -> SValue -> Maybe Indirection
ctry_resolve_error_call
  






mapMaybeS :: Ord b => (a -> Maybe b) -> S.Set a -> S.Set b
mapMaybeS :: forall b a. Ord b => (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 :: forall b a. Ord b => (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

























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 = GPR -> Register
Reg64 GPR
RDI 
param a
1 = GPR -> Register
Reg64 GPR
RSI
param a
2 = GPR -> Register
Reg64 GPR
RDX
param a
3 = GPR -> Register
Reg64 GPR
RCX
param a
4 = GPR -> Register
Reg64 GPR
R8
param a
5 = GPR -> Register
Reg64 GPR
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 :: String -> ExternalFunctionBehavior
-- | a list of some function that return a heap-pointer through RAX.
-- The pointer is assumed to  be fresh.
external_function_behavior :: String -> ExternalFunctionBehavior
external_function_behavior String
"_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_malloc_create_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_malloc_default_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_malloc_zone_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"isc__mem_allocate" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"isc_mem_allocate" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"PyType_GenericAlloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"PyType_GenericNew" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"PySys_GetObject" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"aligned_alloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_malloc_zone_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_mmap" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_av_mallocz" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"___error" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_strerror_r" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"__wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_EVP_CIPHER_CTX_new" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_open" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_fts_read$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_fts_open$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_opendir$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_fdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_wfdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_wsetlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"__ctype_b_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"dcgettext" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"nl_langinfo" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"__errno_location" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"_popen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"__ctype_tolower_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"__ctype_toupper_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"readdir" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"getmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"setmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior String
"hasmntopt" = ExternalFunctionBehavior
pure_and_fresh
-- | A list of some functions that are assumed not to change the state in any significant way, and that return an unknown bottom value through RAX
external_function_behavior String
"feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fnmatch" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"___maskrune" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_getbsize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"vprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"vfprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fwprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fwprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__fprintf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__printf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_putchar" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_puts" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"strlen" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_ilogb" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_atoi" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_getopt" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"getopt_long" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_warn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_warnx" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__errno_location" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__libc_start_main" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__cxa_finalize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"perror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"unlink" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"unlinkat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"strspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"utimensat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fdatasync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fsync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"isatty" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"strcspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"isprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"iswprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_isprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_iswprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"__cxa_atexit" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"towlower" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"towupper" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"iswalnum" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fseeko" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_fgets" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_ferror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_strtol" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_strtoul" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"_munmap" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior String
"fread_unlocked" = ExternalFunctionBehavior
pure_and_unknown



-- | A list of some functions that return bottom and write to pointers passed by parameters
--external_function_behavior "_sysctlbyname" = ExternalFunctionBehavior [param 2, param 4] UnknownReturnValue
--external_function_behavior "_fstat$INODE64" = ExternalFunctionBehavior [param 1] UnknownReturnValue
--external_function_behavior "_fstatfs$INODE64" = ExternalFunctionBehavior [param 1] UnknownReturnValue
--external_function_behavior "_statfs$INODE64" = ExternalFunctionBehavior [param 1] UnknownReturnValue
external_function_behavior String
"snprintf"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_snprintf"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_snprintf_l"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_snwprintf"           = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_snwprintf_l"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"__snprintf_chk"       = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_vsnprintf"           = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"sprintf"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"_sprintf"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"___bzero"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"sigprocmask"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"__strcat_chk"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"strcat"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"strlcpy"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"___strlcpy_chk"       = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"sigemptyset"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"sigaction"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior String
"localtime"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall {a}. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
FreshPointer
external_function_behavior String
"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 String
"_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 String
"__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 String
"___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 String
"_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 String
"_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

-- A list of functions that return a pointer given to them by a parameter
external_function_behavior String
"_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 String
"reallocarray"         = [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 String
"_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 String
"_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 String
"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 String
"mremap"               = [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 String
"_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 String
"__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 String
"_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 String
"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 String
"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 String
"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 String
"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 String
"_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 String
"__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 String
"___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 String
"__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 String
"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 String
"_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 String
"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 String
"_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 String
"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 String
"_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 String
"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 String
"_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 String
"_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 String
"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 String
"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 String
"_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 String
"_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 String
"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 String
"_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 String
"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 String
"_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 String
f
 | String -> Bool
is_exiting_function_call String
f = ExternalFunctionBehavior
pure_and_unknown
 | Bool
otherwise                  = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
UnknownReturnValue -- trace ("Unknown external function: " ++ f) $ 



{-- TODO
 - functions calling function pointers
 - __cxa_finalize
 - __libc_start_main
 - pthread_*
 --}






-- | Backward transposition
-- Let p be the current predicate and let the equality sp == v be from the predicate after execution of an internal function.
-- For example, p contains:
--   RSP == RSP0 - 64
--   RSI == 10
--
-- And after execution of the function, we have:
--   *[RSP0+16,8] == RSI0
--
-- Transposing this equality produces:
--   *[RSP0-40,8] == 10

transpose_bw_svalue :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue :: forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue Static bin v
fctxt Sstate SValue SPointer
p t :: SValue
t@SValue
Top           = SValue
t
transpose_bw_svalue Static bin v
fctxt Sstate SValue SPointer
p (SConcrete NESet SimpleExpr
es)  = Static bin v -> String -> NESet SValue -> SValue
forall (t :: * -> *) bin v.
(Foldable t, BinaryClass bin) =>
Static bin v -> String -> t SValue -> SValue
cjoin_all Static bin v
fctxt String
"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 (Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p) NESet SimpleExpr
es
transpose_bw_svalue Static bin v
fctxt Sstate SValue SPointer
p (SAddends NESet SimpleExpr
as)   = Static bin v -> String -> NESet SValue -> SValue
forall (t :: * -> *) bin v.
(Foldable t, BinaryClass bin) =>
Static bin v -> String -> t SValue -> SValue
cjoin_all Static bin v
fctxt String
"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 (Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_addends Static bin v
fctxt Sstate SValue SPointer
p) NESet SimpleExpr
as

transpose_bw_addends :: (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_addends (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt Sstate SValue SPointer
p SimpleExpr
a =
  let a' :: SValue
a' = (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt Sstate SValue SPointer
p SimpleExpr
a
      v' :: SValue
v' = (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
-> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden (bin, Config,
 L0 (Sstate SValue SPointer) (FInit SValue SPointer) v, Word64)
fctxt String
"transpose_bw" SValue
a' in
    SValue
v'



transpose_bw_spointer :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SPointer -> S.Set SPointer
transpose_bw_spointer :: forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SPointer -> Set SPointer
transpose_bw_spointer Static bin v
fctxt Sstate SValue SPointer
p (Ptr_Concrete SimpleExpr
a) =
  let a' :: SValue
a' = Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
a in
    Static bin v -> String -> SValue -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses Static bin v
fctxt String
"transpose_bw" SValue
a'
transpose_bw_spointer Static bin v
fctxt Sstate SValue SPointer
p (Ptr_Base SimpleExpr
b) =
  let b' :: SValue
b' = Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
b in
    Static bin v -> String -> SValue -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> Set SPointer
cmk_mem_addresses Static bin v
fctxt String
"transpose_bw" (SValue -> Set SPointer) -> SValue -> Set SPointer
forall a b. (a -> b) -> a -> b
$ Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"transpose_bw" SValue
b'
transpose_bw_spointer Static bin v
fctxt Sstate SValue SPointer
p SPointer
Ptr_Top = SPointer -> Set SPointer
forall a. a -> Set a
S.singleton SPointer
Ptr_Top



transpose_bw_reg :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> (Register, SValue) -> Maybe (Register, SValue)
transpose_bw_reg :: forall bin v.
BinaryClass bin =>
Static bin v
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg Static bin v
fctxt Sstate SValue SPointer
p (Register
r,SValue
v) =
  let v' :: SValue
v' = Static bin v -> Sstate SValue SPointer -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue Static bin v
fctxt Sstate SValue SPointer
p 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 :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> ((SPointer,Maybe ByteSize), SValue) -> [((SPointer,Maybe ByteSize), SValue)]
transpose_bw_mem :: forall bin v.
BinaryClass bin =>
Static bin v
-> Sstate SValue SPointer
-> ((SPointer, Maybe ByteSize), SValue)
-> [((SPointer, Maybe ByteSize), SValue)]
transpose_bw_mem Static bin v
fctxt Sstate SValue SPointer
p ((SPointer
a,Maybe ByteSize
si),SValue
v) =
  let as' :: Set SPointer
as' = Static bin v -> Sstate SValue SPointer -> SPointer -> Set SPointer
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SPointer -> Set SPointer
transpose_bw_spointer Static bin v
fctxt Sstate SValue SPointer
p SPointer
a
      v' :: SValue
v'  = if Maybe ByteSize
si Maybe ByteSize -> Maybe ByteSize -> Bool
forall a. Eq a => a -> a -> Bool
== ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (Int -> ByteSize
ByteSize Int
8) then Static bin v -> Sstate SValue SPointer -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue Static bin v
fctxt Sstate SValue SPointer
p SValue
v else String -> SValue
mk_top String
"transpose_bw_mem" in
    Set ((SPointer, Maybe ByteSize), SValue)
-> [((SPointer, Maybe ByteSize), SValue)]
forall a. Set a -> [a]
S.toList (Set ((SPointer, Maybe ByteSize), SValue)
 -> [((SPointer, Maybe ByteSize), SValue)])
-> Set ((SPointer, Maybe ByteSize), SValue)
-> [((SPointer, Maybe ByteSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (SPointer -> ((SPointer, Maybe ByteSize), SValue))
-> Set SPointer -> Set ((SPointer, Maybe ByteSize), SValue)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\SPointer
a' -> ((SPointer
a',Maybe ByteSize
si),SValue
v')) Set SPointer
as'



transpose_bw_e :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e :: forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (Bottom (FromCall String
f))            = Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (String -> BotTyp
FromCall String
f)
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Malloc Maybe Word64
id Maybe String
hash)              = Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe String
hash
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Immediate Word64
i)                 = Static bin v -> Word64 -> SValue
forall i bin v.
(Integral i, BinaryClass bin) =>
Static bin v -> i -> SValue
cimmediate Static bin v
fctxt Word64
i
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_StatePart StatePart
sp Maybe String
id)             = String -> SValue
forall a. HasCallStack => String -> a
error String
"Should not happen"
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Var StatePart
sp)                      = Static bin v -> Sstate SValue SPointer -> StatePart -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp Static bin v
fctxt Sstate SValue SPointer
p StatePart
sp
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Bit Int
i SimpleExpr
e)                     = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
"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
$ Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_SExtend Int
l Int
h SimpleExpr
e)               = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
"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
$ Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Op Operator
Plus Int
si [SimpleExpr
a,SimpleExpr
b])            = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
"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 [Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
a,Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Op Operator
Minus Int
si [SimpleExpr
a,SimpleExpr
b])           = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
"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 [Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
a,Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Op Operator
op Int
si [SimpleExpr]
es)                 = Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
forall bin v.
BinaryClass bin =>
Static bin v
-> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
svalue_apply Static bin v
fctxt String
"transpose_bw" (Static bin v -> SimpleExpr -> SimpleExpr
forall bin v.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SimpleExpr
mk_expr Static bin v
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 (Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p) [SimpleExpr]
es
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p (SE_Overwrite Int
i SimpleExpr
a SimpleExpr
b)             = Static bin v -> String -> SymbolicOperation SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SymbolicOperation SValue -> SValue
csemantics Static bin v
fctxt String
"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 (Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
a) (Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
b)

transpose_bw_sp :: BinaryClass bin => Static bin v -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp :: forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp Static bin v
fctxt Sstate SValue SPointer
p (SP_Reg Register
r)    = State (Sstate SValue SPointer, VCS SValue) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate (Static bin v
-> Register -> State (Sstate SValue SPointer, VCS SValue) SValue
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg Static bin v
fctxt Register
r) Sstate SValue SPointer
p
transpose_bw_sp Static bin v
fctxt Sstate SValue SPointer
p (SP_Mem SimpleExpr
a Int
si) = 
  let a' :: SValue
a' = Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e Static bin v
fctxt Sstate SValue SPointer
p SimpleExpr
a in
    State (Sstate SValue SPointer, VCS SValue) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate (Static bin v
-> String
-> SValue
-> Maybe ByteSize
-> State (Sstate SValue SPointer, VCS SValue) SValue
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> v -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem Static bin v
fctxt String
"transpose_bw_sp" SValue
a' (Maybe ByteSize
 -> State (Sstate SValue SPointer, VCS SValue) SValue)
-> Maybe ByteSize
-> State (Sstate SValue SPointer, VCS SValue) SValue
forall a b. (a -> b) -> a -> b
$ ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si) Sstate SValue SPointer
p





data FunctionType = AnalyzedInternalFunction (Sstate SValue SPointer) | ExternalFunction | AnalyzedInternalFunctionTerminates | AnalyzedInternalFunctionUnknown


-- TODO add VerificationError as Functiontype. If so, overwrite at least RAX/XMM0 with top
get_function_type :: BinaryClass bin => Static bin v -> Instruction -> String -> FunctionType
get_function_type :: forall bin v.
BinaryClass bin =>
Static bin v -> Instruction -> String -> FunctionType
get_function_type l :: Static bin v
l@(bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
_) Instruction
i String
f_callee =
  let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin (Sstate SValue SPointer) (FInit SValue SPointer) v
-> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets (bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0) Instruction
i in
    [Maybe (Postcondition (Sstate SValue SPointer))] -> FunctionType
ftype ([Maybe (Postcondition (Sstate SValue SPointer))] -> FunctionType)
-> [Maybe (Postcondition (Sstate SValue SPointer))] -> FunctionType
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget
 -> Maybe (Postcondition (Sstate SValue SPointer)))
-> [ResolvedJumpTarget]
-> [Maybe (Postcondition (Sstate SValue SPointer))]
forall a b. (a -> b) -> [a] -> [b]
map ResolvedJumpTarget
-> Maybe (Postcondition (Sstate SValue SPointer))
postcondition_of_jump_target [ResolvedJumpTarget]
trgts
 where
  ftype :: [Maybe (Postcondition (Sstate SValue SPointer))] -> FunctionType
ftype [Maybe (Postcondition (Sstate SValue SPointer))]
posts
    | (Maybe (Postcondition (Sstate SValue SPointer)) -> Bool)
-> [Maybe (Postcondition (Sstate SValue SPointer))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe (Postcondition (Sstate SValue SPointer))
-> Maybe (Postcondition (Sstate SValue SPointer)) -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Postcondition (Sstate SValue SPointer)
-> Maybe (Postcondition (Sstate SValue SPointer))
forall a. a -> Maybe a
Just Postcondition (Sstate SValue SPointer)
forall pred. Postcondition pred
Terminates)) [Maybe (Postcondition (Sstate SValue SPointer))]
posts                                 = FunctionType
AnalyzedInternalFunctionTerminates
    | (Maybe (Postcondition (Sstate SValue SPointer)) -> Bool)
-> [Maybe (Postcondition (Sstate SValue SPointer))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe (Postcondition (Sstate SValue SPointer)) -> Bool
forall {pred}. Maybe (Postcondition pred) -> Bool
is_returning [Maybe (Postcondition (Sstate SValue SPointer))]
posts                                             = Sstate SValue SPointer -> FunctionType
AnalyzedInternalFunction (Sstate SValue SPointer -> FunctionType)
-> Sstate SValue SPointer -> FunctionType
forall a b. (a -> b) -> a -> b
$ Static bin v -> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> [Sstate v p] -> Sstate v p
supremum Static bin v
l ([Sstate SValue SPointer] -> Sstate SValue SPointer)
-> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ (Maybe (Postcondition (Sstate SValue SPointer))
 -> Sstate SValue SPointer)
-> [Maybe (Postcondition (Sstate SValue SPointer))]
-> [Sstate SValue SPointer]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Postcondition (Sstate SValue SPointer))
-> Sstate SValue SPointer
forall {pred}. Maybe (Postcondition pred) -> pred
fromReturning [Maybe (Postcondition (Sstate SValue SPointer))]
posts
    | String
"0x" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
f_callee Bool -> Bool -> Bool
|| String
"indirection@" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
f_callee = FunctionType
AnalyzedInternalFunctionUnknown
    | Bool
otherwise                                                          = FunctionType
ExternalFunction

  fromReturning :: Maybe (Postcondition pred) -> pred
fromReturning (Just (ReturnsWith pred
q)) = pred
q
  is_returning :: Maybe (Postcondition pred) -> Bool
is_returning  (Just (ReturnsWith pred
q)) = Bool
True
  is_returning  Maybe (Postcondition pred)
_                      = Bool
False

  postcondition_of_jump_target :: ResolvedJumpTarget
-> Maybe (Postcondition (Sstate SValue SPointer))
postcondition_of_jump_target (ImmediateAddress Word64
a) = 
    case Word64
-> L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
-> Maybe
     (FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
a L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0 of 
      Just (FInit SValue SPointer
_,Just FResult (Sstate SValue SPointer) v
r) -> Postcondition (Sstate SValue SPointer)
-> Maybe (Postcondition (Sstate SValue SPointer))
forall a. a -> Maybe a
Just (Postcondition (Sstate SValue SPointer)
 -> Maybe (Postcondition (Sstate SValue SPointer)))
-> Postcondition (Sstate SValue SPointer)
-> Maybe (Postcondition (Sstate SValue SPointer))
forall a b. (a -> b) -> a -> b
$ FResult (Sstate SValue SPointer) v
-> Postcondition (Sstate SValue SPointer)
forall pred v. FResult pred v -> Postcondition pred
result_post FResult (Sstate SValue SPointer) v
r
      Maybe
  (FInit SValue SPointer, Maybe (FResult (Sstate SValue SPointer) v))
_ -> Maybe (Postcondition (Sstate SValue SPointer))
forall a. Maybe a
Nothing
  postcondition_of_jump_target ResolvedJumpTarget
_                    = Maybe (Postcondition (Sstate SValue SPointer))
forall a. Maybe a
Nothing






-- | Executes semantics for external functions.
call :: BinaryClass bin => Static bin v -> Instruction -> State (Sstate SValue SPointer,VCS SValue) ()
call :: forall bin v.
BinaryClass bin =>
Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
call fctxt :: Static bin v
fctxt@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
entry) Instruction
i = do
  let f_callee :: String
f_callee = bin -> Instruction -> String
forall bin. BinaryClass bin => bin -> Instruction -> String
function_name_of_instruction bin
bin Instruction
i
  let ty :: FunctionType
ty = Static bin v -> Instruction -> String -> FunctionType
forall bin v.
BinaryClass bin =>
Static bin v -> Instruction -> String -> FunctionType
get_function_type Static bin v
fctxt Instruction
i String
f_callee
  case FunctionType
ty of
    FunctionType
AnalyzedInternalFunctionUnknown    -> Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
forall {m :: * -> *} {p} {p}. Monad m => p -> p -> m ()
unknown_internal_function Static bin v
fctxt Instruction
i
    FunctionType
AnalyzedInternalFunctionTerminates -> () -> State (Sstate SValue SPointer, VCS SValue) ()
forall a.
a -> StateT (Sstate SValue SPointer, VCS SValue) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AnalyzedInternalFunction Sstate SValue SPointer
q         -> Sstate SValue SPointer
-> State (Sstate SValue SPointer, VCS SValue) ()
internal_function Sstate SValue SPointer
q
    FunctionType
ExternalFunction                   -> String -> State (Sstate SValue SPointer, VCS SValue) ()
external_function String
f_callee
 where
  external_function :: String -> State (Sstate SValue SPointer, VCS SValue) ()
external_function String
f_callee
    --   | f_callee == "error" = call_error fctxt
    | Bool
otherwise =
      case String -> ExternalFunctionBehavior
external_function_behavior String
f_callee of
        ExternalFunctionBehavior [Register]
params ExternalFunctionOutput
output -> {--mapM_ write_param params >> --} String
-> ExternalFunctionOutput
-> State (Sstate SValue SPointer, VCS SValue) ()
write_output String
f_callee ExternalFunctionOutput
output -- writing to params really roughly overapproximates

  write_output :: String -> ExternalFunctionOutput -> State (Sstate SValue SPointer,VCS SValue) ()
  write_output :: String
-> ExternalFunctionOutput
-> State (Sstate SValue SPointer, VCS SValue) ()
write_output String
f_callee ExternalFunctionOutput
FreshPointer       = Static bin v
-> String
-> Register
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg Static bin v
fctxt String
"wo1" (GPR -> Register
Reg64 GPR
RAX) (SValue -> State (Sstate SValue SPointer, VCS SValue) ())
-> SValue -> State (Sstate SValue SPointer, VCS SValue) ()
forall a b. (a -> b) -> a -> b
$ (Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> SimpleExpr
SE_Malloc (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Instruction -> Word64
inAddress Instruction
i)) (String -> Maybe String
forall a. a -> Maybe a
Just String
f_callee))
  write_output String
f_callee ExternalFunctionOutput
UnknownReturnValue = Static bin v
-> String
-> Register
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg Static bin v
fctxt String
"wo2" (GPR -> Register
Reg64 GPR
RAX) (SValue -> State (Sstate SValue SPointer, VCS SValue) ())
-> SValue -> State (Sstate SValue SPointer, VCS SValue) ()
forall a b. (a -> b) -> a -> b
$ (Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (String -> BotTyp
FromCall String
f_callee))
  write_output String
f_callee (Input Register
r)          = do
    --input <- sread_reg fctxt r
    --let ptrs = cmk_mem_addresses fctxt "write_output" input
    --if S.null ptrs then
      Static bin v
-> String
-> Register
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg Static bin v
fctxt String
"wo3" (GPR -> Register
Reg64 GPR
RAX) (SValue -> State (Sstate SValue SPointer, VCS SValue) ())
-> SValue -> State (Sstate SValue SPointer, VCS SValue) ()
forall a b. (a -> b) -> a -> b
$ Static bin v -> SimpleExpr -> SValue
forall {bin} {v}.
BinaryClass bin =>
Static bin v -> SimpleExpr -> SValue
mk_concreteS Static bin v
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe String -> SimpleExpr
SE_Malloc (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Instruction -> Word64
inAddress Instruction
i)) (String -> Maybe String
forall a. a -> Maybe a
Just String
f_callee)
    --else
    --  swrite_reg fctxt "wo4" (Reg64 RAX) input

  incr_rsp :: State (Sstate SValue SPointer, VCS SValue) ()
incr_rsp = Static bin v
-> Bool
-> Instruction
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) ()
sexec_instr Static bin v
fctxt Bool
False (Word64
-> [Prefix]
-> Opcode
-> Maybe Operand
-> [Operand]
-> Int
-> Instruction
Instruction Word64
0 [] Opcode
ADD Maybe Operand
forall a. Maybe a
Nothing [Register -> Operand
Op_Reg (Register -> Operand) -> Register -> Operand
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
RSP, Immediate -> Operand
Op_Imm (Immediate -> Operand) -> Immediate -> Operand
forall a b. (a -> b) -> a -> b
$ BitSize -> Word64 -> Immediate
Immediate (Int -> BitSize
BitSize Int
64) Word64
8] Int
1)

  decr_rsp :: State (Sstate SValue SPointer, VCS SValue) ()
decr_rsp = Static bin v
-> Bool
-> Instruction
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) ()
sexec_instr Static bin v
fctxt Bool
False (Word64
-> [Prefix]
-> Opcode
-> Maybe Operand
-> [Operand]
-> Int
-> Instruction
Instruction Word64
0 [] Opcode
SUB Maybe Operand
forall a. Maybe a
Nothing [Register -> Operand
Op_Reg (Register -> Operand) -> Register -> Operand
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
RSP, Immediate -> Operand
Op_Imm (Immediate -> Operand) -> Immediate -> Operand
forall a b. (a -> b) -> a -> b
$ BitSize -> Word64 -> Immediate
Immediate (Int -> BitSize
BitSize Int
64) Word64
8] Int
1)


  internal_function :: Sstate SValue SPointer -> State (Sstate SValue SPointer,VCS SValue) ()
  internal_function :: Sstate SValue SPointer
-> State (Sstate SValue SPointer, VCS SValue) ()
internal_function Sstate SValue SPointer
q = do
    -- push return address if is call
    State (Sstate SValue SPointer, VCS SValue) ()
decr_rsp

    (Sstate SValue SPointer
p,VCS SValue
vcs) <- StateT
  (Sstate SValue SPointer, VCS SValue)
  Identity
  (Sstate SValue SPointer, VCS SValue)
forall s (m :: * -> *). MonadState s m => m s
get
    -- obtain the postcondition of the function, and do backwards transposition
    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 (Static bin v
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
forall bin v.
BinaryClass bin =>
Static bin v
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg Static bin v
fctxt Sstate SValue SPointer
p) ([(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
r,SValue
_) -> Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [GPR -> Register
Reg64 GPR
RIP,GPR -> Register
Reg64 GPR
RSP]) ([(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, Maybe ByteSize), SValue)]
q_eqs_transposed_mem   = (((SPointer, Maybe ByteSize), SValue)
 -> [((SPointer, Maybe ByteSize), SValue)])
-> [((SPointer, Maybe ByteSize), SValue)]
-> [((SPointer, Maybe ByteSize), SValue)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Static bin v
-> Sstate SValue SPointer
-> ((SPointer, Maybe ByteSize), SValue)
-> [((SPointer, Maybe ByteSize), SValue)]
forall bin v.
BinaryClass bin =>
Static bin v
-> Sstate SValue SPointer
-> ((SPointer, Maybe ByteSize), SValue)
-> [((SPointer, Maybe ByteSize), SValue)]
transpose_bw_mem Static bin v
fctxt Sstate SValue SPointer
p) ([((SPointer, Maybe ByteSize), SValue)]
 -> [((SPointer, Maybe ByteSize), SValue)])
-> [((SPointer, Maybe ByteSize), SValue)]
-> [((SPointer, Maybe ByteSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (((SPointer, Maybe ByteSize), SValue) -> Bool)
-> [((SPointer, Maybe ByteSize), SValue)]
-> [((SPointer, Maybe ByteSize), SValue)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SPointer, Maybe ByteSize), SValue) -> Bool
forall {b} {b}. ((SPointer, b), b) -> Bool
do_transfer ([((SPointer, Maybe ByteSize), SValue)]
 -> [((SPointer, Maybe ByteSize), SValue)])
-> [((SPointer, Maybe ByteSize), SValue)]
-> [((SPointer, Maybe ByteSize), SValue)]
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> [((SPointer, Maybe ByteSize), SValue)]
forall {a} {p}. Sstate a p -> [((p, Maybe ByteSize), a)]
sstate_to_mem_eqs Sstate SValue SPointer
q
    -- write transposed postcondition to current state
    ((Register, SValue)
 -> State (Sstate SValue SPointer, VCS SValue) ())
-> [(Register, SValue)]
-> State (Sstate SValue SPointer, VCS SValue) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Register
r,SValue
v) -> Static bin v
-> String
-> Register
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg Static bin v
fctxt (String
"call: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Instruction -> String
forall a. Show a => a -> String
show Instruction
i) Register
r SValue
v) ([(Register, SValue)]
 -> State (Sstate SValue SPointer, VCS SValue) ())
-> [(Register, SValue)]
-> State (Sstate SValue SPointer, VCS SValue) ()
forall a b. (a -> b) -> a -> b
$ [(Register, SValue)]
q_eqs_transposed_regs
    (((SPointer, Maybe ByteSize), SValue)
 -> State (Sstate SValue SPointer, VCS SValue) ())
-> [((SPointer, Maybe ByteSize), SValue)]
-> State (Sstate SValue SPointer, VCS SValue) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\((SPointer
a,Maybe ByteSize
si),SValue
v) -> Static bin v
-> Bool
-> SPointer
-> Maybe ByteSize
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem_to_ptr Static bin v
fctxt Bool
True SPointer
a Maybe ByteSize
si SValue
v) ([((SPointer, Maybe ByteSize), SValue)]
 -> State (Sstate SValue SPointer, VCS SValue) ())
-> [((SPointer, Maybe ByteSize), SValue)]
-> State (Sstate SValue SPointer, VCS SValue) ()
forall a b. (a -> b) -> a -> b
$ [((SPointer, Maybe ByteSize), SValue)]
q_eqs_transposed_mem 

    State (Sstate SValue SPointer, VCS SValue) ()
incr_rsp 

  -- in case of an external function, which is passed a parameter $r$ 
  -- do a write to region [r+bot,1] to muddle the state. The value written to that region is an abstraction of what is already there.
  write_param :: Register -> State (Sstate SValue SPointer,VCS SValue) ()
  write_param :: Register -> State (Sstate SValue SPointer, VCS SValue) ()
write_param Register
r = do
    SValue
a      <- Static bin v
-> Register -> State (Sstate SValue SPointer, VCS SValue) SValue
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg Static bin v
fctxt Register
r
    let a' :: SValue
a'  = Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"write_param" SValue
a
    SValue
v'     <- ((Sstate SValue SPointer, VCS SValue) -> SValue)
-> State (Sstate SValue SPointer, VCS SValue) SValue
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((State (Sstate SValue SPointer, VCS SValue) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate (State (Sstate SValue SPointer, VCS SValue) SValue
 -> Sstate SValue SPointer -> SValue)
-> State (Sstate SValue SPointer, VCS SValue) SValue
-> Sstate SValue SPointer
-> SValue
forall a b. (a -> b) -> a -> b
$ Static bin v
-> String
-> SValue
-> Maybe ByteSize
-> State (Sstate SValue SPointer, VCS SValue) SValue
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> v -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem Static bin v
fctxt String
"write_param" SValue
a Maybe ByteSize
forall a. Maybe a
unknownSize) (Sstate SValue SPointer -> SValue)
-> ((Sstate SValue SPointer, VCS SValue) -> Sstate SValue SPointer)
-> (Sstate SValue SPointer, VCS SValue)
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sstate SValue SPointer, VCS SValue) -> Sstate SValue SPointer
forall a b. (a, b) -> a
fst)
    let bot :: SValue
bot = Static bin v -> String -> SValue -> SValue
forall bin v.
BinaryClass bin =>
Static bin v -> String -> SValue -> SValue
cwiden Static bin v
fctxt String
"write_param_v" SValue
v'
    Static bin v
-> Bool
-> SValue
-> Maybe ByteSize
-> SValue
-> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem Static bin v
fctxt Bool
True SValue
a' Maybe ByteSize
forall a. Maybe a
unknownSize SValue
bot


  -- TODO
  do_transfer :: ((SPointer, b), b) -> Bool
do_transfer ((p :: SPointer
p@(Ptr_Concrete SimpleExpr
a),b
si),b
v) = SimpleExpr -> Bool
is_global SimpleExpr
a -- not (is_top_stackframe a si) && not (cis_local fctxt p)
  do_transfer ((p :: SPointer
p@(Ptr_Base SimpleExpr
b),b
si),b
v) = SimpleExpr -> Bool
is_global SimpleExpr
b -- not (cis_local fctxt p)
  
  is_global :: SimpleExpr -> Bool
is_global = (PointerBase -> Bool) -> Set PointerBase -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PointerBase -> Bool
is_global_base (Set PointerBase -> Bool)
-> (SimpleExpr -> Set PointerBase) -> SimpleExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
forall bin.
BinaryClass bin =>
bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
get_pointer_base_set bin
bin FInit SValue SPointer
forall {v} {p}. FInit v p
empty_finit)
  is_global_base :: PointerBase -> Bool
is_global_base (GlobalAddress Word64
_) = Bool
True
  is_global_base (BaseIsStatePart StatePart
_) = Bool
True
  is_global_base PointerBase
_ = Bool
False
  

  sstate_to_reg_eqs :: Sstate a p -> [(Register, a)]
sstate_to_reg_eqs (Sstate Map Register a
regs Map (p, Maybe ByteSize) 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, Maybe ByteSize), a)]
sstate_to_mem_eqs (Sstate Map Register a
_ Map (p, Maybe ByteSize) a
mem FlagStatus
_)  = Map (p, Maybe ByteSize) a -> [((p, Maybe ByteSize), a)]
forall k a. Map k a -> [(k, a)]
M.toList Map (p, Maybe ByteSize) a
mem

  unknown_internal_function :: p -> p -> m ()
unknown_internal_function p
fctxt p
i = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()-- TODO try as external



is_top_stackframe :: SimpleExpr -> Maybe ByteSize -> Bool
is_top_stackframe (SE_Var (SP_Reg (Reg64 GPR
RSP))) (Just (ByteSize Int
8)) = Bool
True
is_top_stackframe SimpleExpr
_ Maybe ByteSize
_ = Bool
False




jump :: BinaryClass bin => Static bin v -> Instruction -> State (Sstate SValue SPointer,VCS SValue) ()
jump :: forall bin v.
BinaryClass bin =>
Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
jump l :: Static bin v
l@(bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0,Word64
_) Instruction
i = do
  if Lifting bin (Sstate SValue SPointer) (FInit SValue SPointer) v
-> Instruction -> Bool
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> Bool
jump_is_actually_a_call (bin
bin,Config
config,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
l0) Instruction
i then do
    Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
forall bin v.
BinaryClass bin =>
Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
call Static bin v
l Instruction
i
    Static bin v
-> Instruction -> State (Sstate SValue SPointer, VCS SValue) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sreturn Static bin v
l Instruction
i
  else
    () -> State (Sstate SValue SPointer, VCS SValue) ()
forall a.
a -> StateT (Sstate SValue SPointer, VCS SValue) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()



ctry_jump_targets :: BinaryClass bin => Static bin v -> SValue -> Maybe (S.Set ResolvedJumpTarget)
ctry_jump_targets :: forall bin v.
BinaryClass bin =>
Static bin v -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets l :: Static bin v
l@(bin
bin,Config
_,L0 (Sstate SValue SPointer) (FInit SValue SPointer) v
_,Word64
_) v :: SValue
v@(SConcrete NESet SimpleExpr
es) =
  let tries :: [ResolvedJumpTarget]
tries = (SimpleExpr -> Maybe ResolvedJumpTarget)
-> [SimpleExpr] -> [ResolvedJumpTarget]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SimpleExpr -> Maybe ResolvedJumpTarget
try ([SimpleExpr] -> [ResolvedJumpTarget])
-> [SimpleExpr] -> [ResolvedJumpTarget]
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList (Set SimpleExpr -> [SimpleExpr]) -> Set SimpleExpr -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es in
    case [ResolvedJumpTarget]
tries of
      [] -> Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing -- trace ("Cannot resolve indirection: " ++ show v) Nothing      
      [ResolvedJumpTarget]
_  -> Set ResolvedJumpTarget -> Maybe (Set ResolvedJumpTarget)
forall a. a -> Maybe a
Just (Set ResolvedJumpTarget -> Maybe (Set ResolvedJumpTarget))
-> Set ResolvedJumpTarget -> Maybe (Set ResolvedJumpTarget)
forall a b. (a -> b) -> a -> b
$ [ResolvedJumpTarget] -> Set ResolvedJumpTarget
forall a. Ord a => [a] -> Set a
S.fromList [ResolvedJumpTarget]
tries
 where
  try :: SimpleExpr -> Maybe ResolvedJumpTarget
try (SE_Immediate Word64
imm)                     = Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
imm 
  try (SE_Var (SP_Mem (SE_Immediate Word64
imm) Int
_)) = Word64 -> Maybe ResolvedJumpTarget
try_reloc Word64
imm Maybe ResolvedJumpTarget
-> Maybe ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` Word64 -> Maybe ResolvedJumpTarget
forall {a}. (Integral a, Show a) => a -> Maybe ResolvedJumpTarget
try_symbol Word64
imm 
  try SimpleExpr
_ = Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing


  try_immediate_address :: Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
a =
    if bin -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
address_has_instruction bin
bin Word64
a then
      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
    else case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ bin -> IntMap Symbol
forall {a}. BinaryClass a => a -> IntMap Symbol
binary_get_symbol_table bin
bin of
      Just (AddressOfLabel String
f Bool
True)  -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ String -> ResolvedJumpTarget
External String
f
      Just Symbol
s                        -> String -> Maybe ResolvedJumpTarget
forall a. HasCallStack => String -> a
error (String -> Maybe ResolvedJumpTarget)
-> String -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ (Word64, Symbol) -> String
forall a. Show a => a -> String
show (Word64
a, Symbol
s) -- Just $ External f
      Maybe Symbol
_                             -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing

  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
$ bin -> IntMap Symbol
forall {a}. BinaryClass a => a -> IntMap Symbol
binary_get_symbol_table bin
bin of
      Just (PointerToLabel String
f Bool
True)  -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ String -> ResolvedJumpTarget
External String
f
      Just (AddressOfLabel String
f Bool
True)  -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ String -> ResolvedJumpTarget
ExternalDeref String
f -- an external variable contains a pointer to a function
      Just (AddressOfObject String
f Bool
True) -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ String -> ResolvedJumpTarget
ExternalDeref String
f      -- an external variable contains a pointer to a function
      Just Symbol
s                        -> String -> Maybe ResolvedJumpTarget
forall a. HasCallStack => String -> a
error (String -> Maybe ResolvedJumpTarget)
-> String -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ (a, Symbol) -> String
forall a. Show a => a -> String
show (a
a, Symbol
s) -- Just $ External f
      Maybe Symbol
_                             -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing


  try_reloc :: Word64 -> Maybe ResolvedJumpTarget
try_reloc Word64
a =
    case (Relocation -> Bool) -> [Relocation] -> Maybe Relocation
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> Relocation -> Bool
is_reloc_for Word64
a) ([Relocation] -> Maybe Relocation)
-> [Relocation] -> Maybe Relocation
forall a b. (a -> b) -> a -> b
$ Set Relocation -> [Relocation]
forall a. Set a -> [a]
S.toList (Set Relocation -> [Relocation]) -> Set Relocation -> [Relocation]
forall a b. (a -> b) -> a -> b
$ bin -> Set Relocation
forall a. BinaryClass a => a -> Set Relocation
binary_get_relocations bin
bin of
      Just (Relocation Word64
_ Word64
a') -> Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
a'
      Maybe Relocation
Nothing -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing

  is_reloc_for :: Word64 -> Relocation -> Bool
is_reloc_for Word64
a (Relocation Word64
a' Word64
_) = Word64
a Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a'

ctry_jump_targets Static bin v
fctxt SValue
_ = Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing