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

{-|
Module      : SymbolicPropagation
Description : Provides an instantiation of all functions necessary to do symbolic propagation
-}
module Instantiation.SymbolicPropagation (
 get_invariant,
 init_pred,
 invariant_to_finit,
 join_finit,
 gather_stateparts
 ) where


import Base
import Config

import Data.SValue
import Data.JumpTarget
import Data.SymbolicExpression

import Analysis.ControlFlow
import Analysis.Pointers
import Analysis.FunctionNames
import Analysis.Context

import Generic.SymbolicConstituents
import Generic.SymbolicPropagation
import Generic.Binary


import X86.Opcode (Opcode(..), isCondJump, isJump)
import X86.Register
import X86.Conventions
import X86.Instruction (addressof)
import Generic.HasSize (sizeof)
import qualified X86.Instruction as X86
import Generic.Instruction (GenericInstruction(Instruction))
import Generic.Address (AddressWord64(..))
import Generic.Operand


import Control.Monad.State.Strict hiding (join)
import Control.Applicative ((<|>))
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set.NonEmpty as NES
import Data.List
import Data.Word 
import Data.Maybe
import Data.Either
import Data.Foldable (toList)
import Data.Bits (testBit, (.|.), (.&.), xor, complement)
import Control.Applicative (liftA2)

import qualified Data.Serialize as Cereal hiding (get,put)
import Control.DeepSeq
import GHC.Generics

import Debug.Trace



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

mk_top :: [Char] -> SValue
mk_top [Char]
""  = SValue
Top
mk_top [Char]
msg = [Char] -> SValue -> SValue
forall p a. p -> a -> a
traceTop [Char]
msg SValue
Top

-- 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

ctry_deterministic :: SValue -> Maybe SimpleExpr
ctry_deterministic (SConcrete NESet SimpleExpr
es)
  | NESet SimpleExpr -> Int
forall a. NESet a -> Int
NES.size NESet SimpleExpr
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SimpleExpr -> Maybe SimpleExpr
try_det (SimpleExpr -> Maybe SimpleExpr) -> SimpleExpr -> Maybe SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> SimpleExpr
forall a. NESet a -> a
NES.findMin NESet SimpleExpr
es
  | Bool
otherwise        = Maybe SimpleExpr
forall a. Maybe a
Nothing
 where
  try_det :: SimpleExpr -> Maybe SimpleExpr
try_det SimpleExpr
e
    | SimpleExpr -> Bool
contains_bot SimpleExpr
e = Maybe SimpleExpr
forall a. Maybe a
Nothing
    | Bool
otherwise      = SimpleExpr -> Maybe SimpleExpr
forall a. a -> Maybe a
Just SimpleExpr
e
ctry_deterministic SValue
_ = Maybe SimpleExpr
forall a. Maybe a
Nothing




-- 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 :: FContext -> NES.NESet (S.Set SAddend) -> S.Set (S.Set SAddend)
group_immediates :: FContext -> NESet (Set SAddend) -> Set (Set SAddend)
group_immediates FContext
fctxt NESet (Set SAddend)
addends =
  let (Set (Set SAddend)
imms,Set (Set SAddend)
remainder) = (Set SAddend -> Bool)
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition Set SAddend -> Bool
is_imm (Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend)))
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a b. (a -> b) -> a -> b
$ NESet (Set SAddend) -> Set (Set SAddend)
forall a. NESet a -> Set a
NES.toSet NESet (Set SAddend)
addends in
    if Set (Set SAddend) -> Bool
forall a. Set a -> Bool
S.null Set (Set SAddend)
imms then
      Set (Set SAddend)
remainder
    else
      Set (Set SAddend) -> Set (Set SAddend) -> Set (Set SAddend)
forall a. Ord a => Set a -> Set a -> Set a
S.union ((Set (Set SAddend) -> Set SAddend)
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set (Set SAddend) -> Set SAddend
merge_imms (Set (Set (Set SAddend)) -> Set (Set SAddend))
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall a b. (a -> b) -> a -> b
$ Set (Set SAddend) -> Set (Set (Set SAddend))
group_imms_by_section Set (Set SAddend)
imms) Set (Set SAddend)
remainder
 where
  is_imm :: Set SAddend -> Bool
is_imm Set SAddend
bs = Set SAddend -> Int
forall a. Set a -> Int
S.size Set SAddend
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& (SAddend -> Bool) -> Set SAddend -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SAddend -> Bool
isImmediateBase Set SAddend
bs

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

  same_section :: Set SAddend -> Set SAddend -> Bool
same_section Set SAddend
imms0 Set SAddend
imms1 = Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for (SAddend -> Word64
get_imm (SAddend -> Word64) -> SAddend -> Word64
forall a b. (a -> b) -> a -> b
$ Set SAddend -> SAddend
forall a. Set a -> a
S.findMin Set SAddend
imms0) Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for (SAddend -> Word64
get_imm (SAddend -> Word64) -> SAddend -> Word64
forall a b. (a -> b) -> a -> b
$ Set SAddend -> SAddend
forall a. Set a -> a
S.findMin Set SAddend
imms1)

  get_section_for :: Word64 -> Maybe ([Char], [Char], Word64, Word64)
get_section_for Word64
a =
    let ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt in
      Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_for_address Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_ending_at Context
ctxt Word64
a

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


-- When doing abstraction, we cap the number of nested dereferences, group them if they have the some inner deref,
-- and abstract over them using Top
group_nested_dereferences :: S.Set (S.Set SAddend) -> S.Set (S.Set SAddend)
group_nested_dereferences :: Set (Set SAddend) -> Set (Set SAddend)
group_nested_dereferences Set (Set SAddend)
ptrs =
  let (Set (Set SAddend)
derefs,Set (Set SAddend)
remainder) = (Set SAddend -> Bool)
-> Set (Set SAddend) -> (Set (Set SAddend), Set (Set SAddend))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition Set SAddend -> Bool
is_deref Set (Set SAddend)
ptrs
      grouped_derefs :: Set (Set (Set SAddend))
grouped_derefs     = (Set SAddend -> Set SAddend -> Bool)
-> Set (Set SAddend) -> Set (Set (Set SAddend))
forall a. Ord a => (a -> a -> Bool) -> Set a -> Set (Set a)
quotientBy Set SAddend -> Set SAddend -> Bool
same_group Set (Set SAddend)
derefs
      groups :: Set (Set SAddend)
groups             = (Set (Set SAddend) -> Set SAddend)
-> Set (Set (Set SAddend)) -> Set (Set SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set (Set SAddend) -> Set SAddend
do_abstraction Set (Set (Set SAddend))
grouped_derefs in
    Set (Set SAddend) -> Set (Set SAddend) -> Set (Set SAddend)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Set SAddend)
groups Set (Set SAddend)
remainder
 where
  is_deref :: Set SAddend -> Bool
is_deref = (SAddend -> Bool) -> Set SAddend -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SAddend -> Bool
is_deref_base

  is_deref_base :: SAddend -> Bool
is_deref_base (SAddend_StatePart (SP_Mem SimpleExpr
_ Int
_)) = Bool
True
  is_deref_base SAddend
_                                = Bool
False

  same_group :: Set SAddend -> Set SAddend -> Bool
same_group Set SAddend
ptr0 Set SAddend
ptr1 = Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr0 Set StatePart -> Set StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr1

  do_abstraction :: Set (Set SAddend) -> Set SAddend
do_abstraction Set (Set SAddend)
ptrs =
    let ptr :: Set SAddend
ptr    = Set (Set SAddend) -> Set SAddend
forall a. Set a -> a
S.findMin Set (Set SAddend)
ptrs
        derefs :: Set StatePart
derefs = Set SAddend -> Set StatePart
get_inner_derefs Set SAddend
ptr in
      (StatePart -> SAddend) -> Set StatePart -> Set SAddend
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map StatePart -> SAddend
SAddend_StatePart Set StatePart
derefs

  get_inner_derefs :: Set SAddend -> Set StatePart
get_inner_derefs = Set (Set StatePart) -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set StatePart) -> Set StatePart)
-> (Set SAddend -> Set (Set StatePart))
-> Set SAddend
-> Set StatePart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SAddend -> Set StatePart) -> Set SAddend -> Set (Set StatePart)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SAddend -> Set StatePart
get_inner_derefs_base
  get_inner_derefs_base :: SAddend -> Set StatePart
get_inner_derefs_base b :: SAddend
b@(SAddend_StatePart StatePart
sp) = SimpleExpr -> Set StatePart
inner_derefs (SimpleExpr -> Set StatePart) -> SimpleExpr -> Set StatePart
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp

  inner_derefs :: SimpleExpr -> Set StatePart
inner_derefs (SE_Var (SP_Mem SimpleExpr
a Int
si))   =
    let ds :: Set StatePart
ds = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
a in
      if Set StatePart -> Bool
forall a. Set a -> Bool
S.null Set StatePart
ds then StatePart -> Set StatePart
forall a. a -> Set a
S.singleton (StatePart -> Set StatePart) -> StatePart -> Set StatePart
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a Int
si else Set StatePart
ds 
  inner_derefs e :: SimpleExpr
e@(SE_Op Operator
op Int
si [SimpleExpr]
es)       = [Set StatePart] -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set StatePart] -> Set StatePart)
-> [Set StatePart] -> Set StatePart
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set StatePart) -> [SimpleExpr] -> [Set StatePart]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Set StatePart
inner_derefs [SimpleExpr]
es
  inner_derefs e :: SimpleExpr
e@(SE_Bit Int
l SimpleExpr
e0)          = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
e0
  inner_derefs e :: SimpleExpr
e@(SE_SExtend Int
l Int
h SimpleExpr
e0)    = SimpleExpr -> Set StatePart
inner_derefs SimpleExpr
e0
  inner_derefs e :: SimpleExpr
e@(SE_Overwrite Int
h SimpleExpr
e0 SimpleExpr
e1) = [Set StatePart] -> Set StatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set StatePart] -> Set StatePart)
-> [Set StatePart] -> Set StatePart
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set StatePart) -> [SimpleExpr] -> [Set StatePart]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> Set StatePart
inner_derefs [SimpleExpr
e0,SimpleExpr
e1]
  inner_derefs SimpleExpr
e                        = Set StatePart
forall a. Set a
S.empty



-- Construct an SValue from SExpressions
mk_concrete :: FContext -> String -> NES.NESet SimpleExpr -> SValue
---mk_concrete fctxt msg | trace ("mk_concrete: "++ show msg) False = error "trace"
mk_concrete :: FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
msg = NESet SimpleExpr -> SValue
cap (NESet SimpleExpr -> SValue)
-> (NESet SimpleExpr -> NESet SimpleExpr)
-> NESet SimpleExpr
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr) -> NESet SimpleExpr -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SimpleExpr -> SimpleExpr
simp -- 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 = 
      let es' :: NESet (Set SAddend)
es' = FContext -> [Char] -> NESet SimpleExpr -> NESet (Set SAddend)
forall p. FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt ([Char]
"mk_concrete"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
msg) NESet SimpleExpr
es in
        FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt ([Char]
"mk_concrete"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
msg) NESet (Set SAddend)
es'
    | Bool
otherwise = NESet SimpleExpr -> SValue
SConcrete NESet SimpleExpr
es
  num_cases :: Int
num_cases = Context -> Int
ctxt_max_num_of_cases (FContext -> Context
f_ctxt FContext
fctxt)

mk_concreteS :: FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"mk_concreteS" (NESet SimpleExpr -> SValue)
-> (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton

mk_addends :: FContext -> String -> NES.NESet (S.Set SAddend) -> SValue
mk_addends :: FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt [Char]
msg = Set (Set SAddend) -> SValue
mk (Set (Set SAddend) -> SValue)
-> (NESet (Set SAddend) -> Set (Set SAddend))
-> NESet (Set SAddend)
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set SAddend) -> Set (Set SAddend)
group_nested_dereferences (Set (Set SAddend) -> Set (Set SAddend))
-> (NESet (Set SAddend) -> Set (Set SAddend))
-> NESet (Set SAddend)
-> Set (Set SAddend)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> NESet (Set SAddend) -> Set (Set SAddend)
group_immediates FContext
fctxt
 where
  mk :: Set (Set SAddend) -> SValue
mk Set (Set SAddend)
addends
    | (Set SAddend -> Bool) -> Set (Set SAddend) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Set SAddend -> Bool
forall a. Set a -> Bool
S.null Set (Set SAddend)
addends = [Char] -> SValue
mk_top ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"mk_addends: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Set (Set SAddend) -> [Char]
forall a. Show a => a -> [Char]
show Set (Set SAddend)
addends
    | Set (Set SAddend) -> Int
forall a. Set a -> Int
S.size Set (Set SAddend)
addends Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 = [Char] -> SValue
mk_top ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"mk_addends: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Set (Set SAddend) -> [Char]
forall a. Show a => a -> [Char]
show Set (Set SAddend)
addends -- TODO 5: num_of_addends
    | Bool
otherwise          = NESet (NESet SAddend) -> SValue
SAddends (NESet (NESet SAddend) -> SValue)
-> NESet (NESet SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ Set (NESet SAddend) -> NESet (NESet SAddend)
forall a. Set a -> NESet a
NES.unsafeFromSet (Set (NESet SAddend) -> NESet (NESet SAddend))
-> Set (NESet SAddend) -> NESet (NESet SAddend)
forall a b. (a -> b) -> a -> b
$ (Set SAddend -> NESet SAddend)
-> Set (Set SAddend) -> Set (NESet SAddend)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Set SAddend -> NESet SAddend
forall a. Set a -> NESet a
NES.unsafeFromSet Set (Set SAddend)
addends

cimmediate :: Integral i => FContext -> i -> SValue
cimmediate :: FContext -> i -> SValue
cimmediate FContext
fctxt = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"cimmediate" (NESet SimpleExpr -> SValue)
-> (i -> NESet SimpleExpr) -> i -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr)
-> (i -> SimpleExpr) -> i -> NESet SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> (i -> Word64) -> i -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral


-- WIDENING
set_unknown_offset :: p -> [Char] -> SPointer -> SPointer
set_unknown_offset p
fctxt [Char]
msg (Base_StackPointer [Char]
f   PtrOffset
offset) = [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f PtrOffset
UnknownOffset 
set_unknown_offset p
fctxt [Char]
msg (Base_Immediate Word64
a      PtrOffset
offset) = Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
a PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_Malloc Maybe Word64
id Maybe [Char]
h      PtrOffset
offset) = Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
h PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_FunctionPtr Word64
a [Char]
f  PtrOffset
offset) = Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_TLS              PtrOffset
offset) = PtrOffset -> SPointer
Base_TLS PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_StatePart StatePart
sp     PtrOffset
offset) = StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg (Base_FunctionReturn [Char]
f PtrOffset
offset) = [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f PtrOffset
UnknownOffset
set_unknown_offset p
fctxt [Char]
msg SPointer
b                              = [Char] -> SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> SPointer) -> [Char] -> SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"set_unknown_offset: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show SPointer
b



abstract_addends :: FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt (SE_Op Operator
Plus  Int
si [SimpleExpr
e0,SimpleExpr
e1])                = [Set SAddend] -> Set SAddend
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e0,FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e1]
abstract_addends FContext
fctxt (SE_Op Operator
Minus Int
si [SimpleExpr
e0,SimpleExpr
e1])                = FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e0
abstract_addends FContext
fctxt (SE_Var (SP_StackPointer [Char]
f))            = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_StackPointer [Char]
f
abstract_addends FContext
fctxt (SE_Immediate Word64
imm)
  | FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
imm                        = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Word64 -> SAddend
SAddend_Immediate Word64
imm
  | Bool
otherwise                                                  = Set SAddend
forall a. Set a
S.empty
abstract_addends FContext
fctxt (SE_Malloc Maybe Word64
id Maybe [Char]
h)                        = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SAddend
SAddend_Malloc Maybe Word64
id Maybe [Char]
h
abstract_addends FContext
fctxt (SE_Var sp :: StatePart
sp@(SP_Mem (SE_Immediate Word64
a) Int
8)) = 
  case FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a of
    Maybe [Char]
Nothing -> SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ StatePart -> SAddend
SAddend_StatePart StatePart
sp
    Just [Char]
f  -> SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ Word64 -> [Char] -> SAddend
SAddend_FunctionPtr Word64
a [Char]
f 
abstract_addends FContext
fctxt (SE_Var (SP_Mem (SE_Var (SP_StackPointer [Char]
f)) Int
8)) = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_ReturnAddr [Char]
f
abstract_addends FContext
fctxt (SE_Var (SP_Reg Register
FS))                    = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ SAddend
SAddend_TLS
abstract_addends FContext
fctxt (SE_Var StatePart
sp)                             = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ StatePart -> SAddend
SAddend_StatePart StatePart
sp
abstract_addends FContext
fctxt (Bottom (FromCall [Char]
f))
  | [Char]
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
""                                                    = Set SAddend
forall a. Set a
S.empty
  | Bool
otherwise                                                  = SAddend -> Set SAddend
forall a. a -> Set a
S.singleton (SAddend -> Set SAddend) -> SAddend -> Set SAddend
forall a b. (a -> b) -> a -> b
$ [Char] -> SAddend
SAddend_FunctionReturn [Char]
f
abstract_addends FContext
fctxt (SE_Bit Int
h SimpleExpr
e)                            = FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt SimpleExpr
e
abstract_addends FContext
fctxt SimpleExpr
_                                       = Set SAddend
forall a. Set a
S.empty



widen_exprs :: FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt p
msg NESet SimpleExpr
es = (SimpleExpr -> Set SAddend)
-> NESet SimpleExpr -> NESet (Set SAddend)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> Set SAddend
abstract_addends FContext
fctxt) NESet SimpleExpr
es


cwiden :: FContext -> String -> SValue -> SValue
---cwiden fctxt msg v | trace ("cwiden: " ++ msg ++ "\n" ++ show v) False = error "trace"
cwiden :: FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
msg (SConcrete NESet SimpleExpr
es) = FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends FContext
fctxt ([Char]
"cwiden " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet (Set SAddend) -> SValue) -> NESet (Set SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> NESet SimpleExpr -> NESet (Set SAddend)
forall p. FContext -> p -> NESet SimpleExpr -> NESet (Set SAddend)
widen_exprs FContext
fctxt [Char]
msg NESet SimpleExpr
es
cwiden FContext
fctxt [Char]
msg SValue
v = SValue
v



cwiden_all :: FContext -> String -> [SValue] -> SValue
cwiden_all :: FContext -> [Char] -> [SValue] -> SValue
cwiden_all FContext
fctxt [Char]
msg []     = [Char] -> SValue
mk_top ([Char]
"cwiden_all" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg)
cwiden_all FContext
fctxt [Char]
msg (SValue
v:[SValue]
vs) = (SValue -> SValue -> SValue) -> [SValue] -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg) ([SValue] -> SValue) -> [SValue] -> SValue
forall a b. (a -> b) -> a -> b
$ (SValue -> SValue) -> [SValue] -> [SValue]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
msg) (SValue
vSValue -> [SValue] -> [SValue]
forall a. a -> [a] -> [a]
:[SValue]
vs)


-- JOINING
---cjoin fctxt msg v0 v1 | trace ("cjoin: " ++ msg ++ "\n" ++ show (v0,v1)) False = error "trace"
cjoin :: FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg SValue
v0 SValue
v1 = SValue -> SValue -> SValue
join SValue
v0 SValue
v1
 where
  join :: SValue -> SValue -> SValue
join v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> NESet SimpleExpr -> NESet SimpleExpr
forall a. Ord a => NESet a -> NESet a -> NESet a
NES.union NESet SimpleExpr
es0 NESet SimpleExpr
es1
  join v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)  = FContext -> [Char] -> NESet (Set SAddend) -> SValue
mk_addends  FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (NESet (Set SAddend) -> SValue) -> NESet (Set SAddend) -> SValue
forall a b. (a -> b) -> a -> b
$ (NESet SAddend -> Set SAddend)
-> NESet (NESet SAddend) -> NESet (Set SAddend)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map NESet SAddend -> Set SAddend
forall a. NESet a -> Set a
NES.toSet (NESet (NESet SAddend) -> NESet (Set SAddend))
-> NESet (NESet SAddend) -> NESet (Set SAddend)
forall a b. (a -> b) -> a -> b
$ NESet (NESet SAddend)
-> NESet (NESet SAddend) -> NESet (NESet SAddend)
forall a. Ord a => NESet a -> NESet a -> NESet a
NES.union NESet (NESet SAddend)
es0 NESet (NESet SAddend)
es1
  join v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)  = SValue -> SValue -> SValue
join (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v0) SValue
v1
  join v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1) = SValue -> SValue -> SValue
join SValue
v0 (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cjoin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v1)

  join t :: SValue
t@SValue
Top SValue
_ = SValue
t
  join SValue
_ t :: SValue
t@SValue
Top = SValue
t

cjoin_all :: Foldable t => FContext -> String -> t SValue -> SValue
cjoin_all :: FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
msg t SValue
es
  | t SValue -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t SValue
es   = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot join [], msg = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg
  | Bool
otherwise = (SValue -> SValue -> SValue) -> t SValue -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
msg) t SValue
es



all_equal :: (Eq a) => [a] -> Bool
all_equal :: [a] -> Bool
all_equal [] = Bool
True
all_equal [a]
xs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> a
forall a. [a] -> a
head [a]
xs) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)


-- TODO joining global immediates can be prevented at the cost of scalability
cjoin_pointers :: p -> [SPointer] -> [SPointer]
cjoin_pointers p
fctxt []    = []
cjoin_pointers p
fctxt [SPointer
ptr] = [SPointer
ptr]
cjoin_pointers p
fctxt [SPointer]
ptrs
  | [SPointer] -> Bool
forall a. Eq a => [a] -> Bool
all_equal [SPointer]
ptrs = [[SPointer] -> SPointer
forall a. [a] -> a
head [SPointer]
ptrs]
  | Bool
otherwise      = 
    let ptrs' :: [SPointer]
ptrs'            = [SPointer] -> [SPointer]
forall a. Eq a => [a] -> [a]
nub ([SPointer] -> [SPointer]) -> [SPointer] -> [SPointer]
forall a b. (a -> b) -> a -> b
$ (SPointer -> SPointer) -> [SPointer] -> [SPointer]
forall a b. (a -> b) -> [a] -> [b]
map (p -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset p
fctxt [Char]
"cjoin_pointers") [SPointer]
ptrs
        ([SPointer]
imms,[SPointer]
remainder) = (SPointer -> Bool) -> [SPointer] -> ([SPointer], [SPointer])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition SPointer -> Bool
is_imm [SPointer]
ptrs' in
      [SPointer] -> [SPointer]
merge_imms [SPointer]
imms [SPointer] -> [SPointer] -> [SPointer]
forall a. [a] -> [a] -> [a]
++ [SPointer]
remainder
 where
  is_imm :: SPointer -> Bool
is_imm (Base_Immediate Word64
_ PtrOffset
_)  = Bool
True
  is_imm SPointer
_                     = Bool
False

  get_imm :: SPointer -> Word64
get_imm (Base_Immediate Word64
i PtrOffset
_) = Word64
i

  merge_imms :: [SPointer] -> [SPointer]
merge_imms []   = []
  merge_imms [SPointer]
imms = [(\Word64
i -> Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
i PtrOffset
UnknownOffset) (Word64 -> SPointer) -> Word64 -> SPointer
forall a b. (a -> b) -> a -> b
$ [Word64] -> Word64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Word64] -> Word64) -> [Word64] -> Word64
forall a b. (a -> b) -> a -> b
$ (SPointer -> Word64) -> [SPointer] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map SPointer -> Word64
get_imm [SPointer]
imms]






-- MAKING POINTERS FROM EXPRESSIONS
addends_of :: SimpleExpr -> Set SimpleExpr
addends_of (SE_Op Operator
Plus Int
_ [SimpleExpr]
es)      = Set (Set SimpleExpr) -> Set SimpleExpr
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set SimpleExpr) -> Set SimpleExpr)
-> Set (Set SimpleExpr) -> Set SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Set SimpleExpr)
-> Set SimpleExpr -> Set (Set SimpleExpr)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Set SimpleExpr
addends_of (Set SimpleExpr -> Set (Set SimpleExpr))
-> Set SimpleExpr -> Set (Set SimpleExpr)
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> Set SimpleExpr
forall a. Ord a => [a] -> Set a
S.fromList [SimpleExpr]
es
addends_of (SE_Op Operator
Minus Int
_ (SimpleExpr
e:[SimpleExpr]
es)) = SimpleExpr -> Set SimpleExpr
addends_of SimpleExpr
e
addends_of SimpleExpr
e                      = SimpleExpr -> Set SimpleExpr
forall a. a -> Set a
S.singleton SimpleExpr
e


is_local_expr :: SimpleExpr -> Maybe [Char]
is_local_expr (SE_Var (SP_StackPointer [Char]
f))        = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
f 
is_local_expr (SE_Op Operator
Plus Int
_ [SimpleExpr
e0,SimpleExpr
e1])              = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e0 Maybe [Char] -> Maybe [Char] -> Maybe [Char]
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e1
is_local_expr (SE_Op Operator
Minus Int
_ [SimpleExpr
e0,SimpleExpr
_])              = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e0
is_local_expr (SE_Op Operator
And Int
_ [SimpleExpr
e,SE_Immediate Word64
mask]) = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e
is_local_expr SimpleExpr
_                                   = Maybe [Char]
forall a. Maybe a
Nothing
-- Returns true if the immediate value is likely a pointer
immediate_maybe_a_pointer :: FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
a = Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_for_address Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe ([Char], [Char], Word64, Word64)
forall a. Maybe a
Nothing Bool -> Bool -> Bool
|| Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_ending_at Context
ctxt Word64
a Maybe ([Char], [Char], Word64, Word64)
-> Maybe ([Char], [Char], Word64, Word64) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe ([Char], [Char], Word64, Word64)
forall a. Maybe a
Nothing Bool -> Bool -> Bool
|| Word64 -> Bool
forall a. Integral a => a -> Bool
has_symbol Word64
a
 where
  ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
  has_symbol :: a -> Bool
has_symbol a
a = (Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt) Maybe Symbol -> Maybe Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Symbol
forall a. Maybe a
Nothing



-- Try to promote an expression to a pointer base
try_promote_expr :: FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr :: FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Plus Int
si [SE_Immediate Word64
imm,SimpleExpr
e0]) = FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
si [SimpleExpr
e0,Word64 -> SimpleExpr
SE_Immediate Word64
imm])
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Plus Int
si [SimpleExpr
e0,SE_Immediate Word64
imm]) = 
  case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e0 of
    Just b :: SPointer
b@(Base_Immediate Word64
i (PtrOffset Word64
i0)) -> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
imm) Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` (SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" SPointer
b)
    Just b :: SPointer
b@(Base_Immediate Word64
i PtrOffset
_)              -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
    Maybe SPointer
Nothing -> FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
imm)
    Maybe SPointer
x -> (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) Word64
imm) (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SPointer
x
try_promote_expr FContext
fctxt Bool
strict (SE_Op Operator
Minus Int
_ [SimpleExpr
e0,SE_Immediate Word64
imm]) =
  case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e0 of
    Just b :: SPointer
b@(Base_Immediate Word64
i (PtrOffset Word64
i0)) -> (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
strict (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
imm)  Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` (SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"try_promote_expr" SPointer
b)
    Just b :: SPointer
b@(Base_Immediate Word64
i PtrOffset
_)              -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
    Maybe SPointer
x -> (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (\Word64
v -> Word64
v Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
imm) (SPointer -> SPointer) -> Maybe SPointer -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SPointer
x
try_promote_expr FContext
fctxt Bool
strict SimpleExpr
e =
  let promotions :: [(SimpleExpr, Maybe SPointer)]
promotions = (SimpleExpr -> (SimpleExpr, Maybe SPointer))
-> [SimpleExpr] -> [(SimpleExpr, Maybe SPointer)]
forall a b. (a -> b) -> [a] -> [b]
map (\SimpleExpr
a -> (SimpleExpr
a,SimpleExpr -> Maybe SPointer
try_promote_addend SimpleExpr
a)) ([SimpleExpr] -> [(SimpleExpr, Maybe SPointer)])
-> [SimpleExpr] -> [(SimpleExpr, Maybe SPointer)]
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> [SimpleExpr]
forall a. Set a -> [a]
S.toList (Set SimpleExpr -> [SimpleExpr]) -> Set SimpleExpr -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Set SimpleExpr
addends_of SimpleExpr
e
      bases :: [(SimpleExpr, Maybe SPointer)]
bases      = ((SimpleExpr, Maybe SPointer) -> Bool)
-> [(SimpleExpr, Maybe SPointer)] -> [(SimpleExpr, Maybe SPointer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SimpleExpr
_,Maybe SPointer
p) -> Maybe SPointer
p Maybe SPointer -> Maybe SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe SPointer
forall a. Maybe a
Nothing) [(SimpleExpr, Maybe SPointer)]
promotions in
    case [(SimpleExpr, Maybe SPointer)]
bases of
      []            -> Maybe SPointer
forall a. Maybe a
Nothing
      [(SimpleExpr
e',Just SPointer
b)] -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool -> SPointer
mk_offset SPointer
b (SimpleExpr
e'SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
==SimpleExpr
e)
      [(SimpleExpr, Maybe SPointer)]
bases         -> case ((SimpleExpr, Maybe SPointer) -> Bool)
-> [(SimpleExpr, Maybe SPointer)] -> [(SimpleExpr, Maybe SPointer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe SPointer -> Bool
real_base (Maybe SPointer -> Bool)
-> ((SimpleExpr, Maybe SPointer) -> Maybe SPointer)
-> (SimpleExpr, Maybe SPointer)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr, Maybe SPointer) -> Maybe SPointer
forall a b. (a, b) -> b
snd) [(SimpleExpr, Maybe SPointer)]
bases of
                         [(SimpleExpr
_,Just SPointer
b)] -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool -> SPointer
mk_offset SPointer
b Bool
False
                         [(SimpleExpr, Maybe SPointer)]
_            -> Maybe SPointer
forall a. Maybe a
Nothing -- error $ "TODO: get initial values from addends" ++ show e
 where
  mk_offset :: SPointer -> Bool -> SPointer
mk_offset SPointer
b Bool
True  = SPointer
b
  mk_offset SPointer
b Bool
False = FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"mk_offset" SPointer
b

  try_promote_addend :: SimpleExpr -> Maybe SPointer
try_promote_addend (SE_Var (SP_StackPointer [Char]
f))         = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
  try_promote_addend (SE_Immediate Word64
imm)
    | FContext -> Word64 -> Bool
immediate_maybe_a_pointer FContext
fctxt Word64
imm                 = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
imm (Word64 -> PtrOffset
PtrOffset Word64
0)
    | Bool
otherwise                                           = Maybe SPointer
forall a. Maybe a
Nothing
  try_promote_addend (SE_Malloc Maybe Word64
id Maybe [Char]
hash)                  = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
hash (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
  try_promote_addend (SE_Var sp :: StatePart
sp@(SP_Mem (SE_Immediate Word64
a) Int
8)) =
    case (\[Char]
f -> Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0) ([Char] -> SPointer) -> Maybe [Char] -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a of
      Maybe SPointer
Nothing -> if Bool
strict then Maybe SPointer
forall a. Maybe a
Nothing else SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
      Just SPointer
p  -> SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
p
  -- TODO return address
  try_promote_addend (SE_Var (SP_Reg Register
FS))                 = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ PtrOffset -> SPointer
Base_TLS (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
  try_promote_addend e :: SimpleExpr
e@(SE_Var StatePart
sp)                        
    | Bool -> Bool
not Bool
strict                                          = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
    | FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt SimpleExpr
e                     = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
    | Bool
otherwise                                           = Maybe SPointer
forall a. Maybe a
Nothing
  try_promote_addend (Bottom (FromCall [Char]
f))
    | Bool -> Bool
not Bool
strict Bool -> Bool -> Bool
&& [Char]
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
""                               = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
    | Bool
otherwise                                           = Maybe SPointer
forall a. Maybe a
Nothing
  try_promote_addend SimpleExpr
e                                    = Maybe SPointer
forall a. Maybe a
Nothing


  real_base :: Maybe SPointer -> Bool
real_base (Just (Base_StatePart StatePart
_ PtrOffset
_)) = Bool
False
  real_base Maybe SPointer
_                           = Bool
True

possible_pointer_addend :: FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt (SE_Var StatePart
sp) = StatePart
sp StatePart -> Set StatePart -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` (((StatePart, Maybe SValue) -> StatePart)
-> Set (StatePart, Maybe SValue) -> Set StatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (StatePart, Maybe SValue) -> StatePart
forall a b. (a, b) -> a
fst Set (StatePart, Maybe SValue)
sps)
 where
  FInit Set (StatePart, Maybe SValue)
sps Map (SStatePart, SStatePart) MemRelation
_ = FContext -> FInit
f_init FContext
fctxt
possible_pointer_addend FContext
_ SimpleExpr
_               = Bool
False


cmk_mem_addresses :: FContext -> String -> SValue -> S.Set SPointer
cmk_mem_addresses :: FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt [Char]
msg v :: SValue
v@(SConcrete NESet SimpleExpr
es) = 
  let as :: Set (Maybe SPointer)
as = (SimpleExpr -> Maybe SPointer)
-> Set SimpleExpr -> Set (Maybe SPointer)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map SimpleExpr -> Maybe SPointer
mk (Set SimpleExpr -> Set (Maybe SPointer))
-> Set SimpleExpr -> Set (Maybe SPointer)
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr -> Set SimpleExpr
forall a. NESet a -> Set a
NES.toSet NESet SimpleExpr
es in
    if Maybe SPointer
forall a. Maybe a
Nothing Maybe SPointer -> Set (Maybe SPointer) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Maybe SPointer)
as then
      FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt [Char]
msg (SValue -> Set SPointer) -> SValue -> Set SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt ([Char]
"cmk_mem_addresses of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SValue
v
    else
      (Maybe SPointer -> SPointer)
-> Set (Maybe SPointer) -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe SPointer -> SPointer
forall a. HasCallStack => Maybe a -> a
fromJust Set (Maybe SPointer)
as
 where
  mk :: SimpleExpr -> Maybe SPointer
mk SimpleExpr
e = FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` SimpleExpr -> Maybe SPointer
try_local SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Maybe SPointer
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
e 
  try_local :: SimpleExpr -> Maybe SPointer
try_local SimpleExpr
e = (\[Char]
f -> [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f PtrOffset
UnknownOffset) ([Char] -> SPointer) -> Maybe [Char] -> Maybe SPointer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
e
cmk_mem_addresses FContext
fctxt [Char]
msg v :: SValue
v@(SAddends NESet (NESet SAddend)
adds) = (NESet SAddend -> Maybe SPointer)
-> Set (NESet SAddend) -> Set SPointer
forall b a. Ord b => (a -> Maybe b) -> Set a -> Set b
mapMaybeS NESet SAddend -> Maybe SPointer
mk (Set (NESet SAddend) -> Set SPointer)
-> Set (NESet SAddend) -> Set SPointer
forall a b. (a -> b) -> a -> b
$ NESet (NESet SAddend) -> Set (NESet SAddend)
forall a. NESet a -> Set a
NES.toSet NESet (NESet SAddend)
adds
 where
  mk :: NESet SAddend -> Maybe SPointer
mk NESet SAddend
adds =
    let ptrs :: NESet SPointer
ptrs = (SAddend -> SPointer) -> NESet SAddend -> NESet SPointer
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SAddend -> SPointer
saddend_to_spointer NESet SAddend
adds
        (Set SPointer
strict,Set SPointer
nonstrict) = (SPointer -> Bool) -> Set SPointer -> (Set SPointer, Set SPointer)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition SPointer -> Bool
is_strict (Set SPointer -> (Set SPointer, Set SPointer))
-> Set SPointer -> (Set SPointer, Set SPointer)
forall a b. (a -> b) -> a -> b
$ NESet SPointer -> Set SPointer
forall a. NESet a -> Set a
NES.toSet NESet SPointer
ptrs in
      if Set SPointer -> Bool
forall a. Set a -> Bool
S.null Set SPointer
strict Bool -> Bool -> Bool
&& Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
nonstrict Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
        SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt ([Char]
"cmk_mem_addresses (1) of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  [Char]
msg) (SPointer -> SPointer) -> SPointer -> SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
nonstrict
      else if Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
strict Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
        SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt ([Char]
"cmk_mem_addresses (2) of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  [Char]
msg) (SPointer -> SPointer) -> SPointer -> SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
strict
      else
        [Char] -> Maybe SPointer -> Maybe SPointer
forall p a. p -> a -> a
traceTop ([Char]
"cmk_mem_addresses of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show SValue
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Set SPointer, Set SPointer) -> [Char]
forall a. Show a => a -> [Char]
show (Set SPointer
strict,Set SPointer
nonstrict)) Maybe SPointer
forall a. Maybe a
Nothing

  is_strict :: SPointer -> Bool
is_strict (Base_StatePart StatePart
sp PtrOffset
_)     = FContext -> SimpleExpr -> Bool
possible_pointer_addend FContext
fctxt (StatePart -> SimpleExpr
SE_Var StatePart
sp)
  is_strict (Base_FunctionReturn [Char]
f PtrOffset
_) = Bool
False
  is_strict SPointer
_                         = Bool
True
cmk_mem_addresses FContext
fctxt [Char]
msg t :: SValue
t@SValue
Top = Set SPointer
forall a. Set a
S.empty


-- Concert SValues to SExpressions
-- TODO UnknownOffsets?
saddend_to_spointer :: SAddend -> SPointer
saddend_to_spointer (SAddend_StackPointer [Char]
f)   = [Char] -> PtrOffset -> SPointer
Base_StackPointer [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_Immediate Word64
i)      = Word64 -> PtrOffset -> SPointer
Base_Immediate Word64
i (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_Malloc Maybe Word64
id Maybe [Char]
h)      = Maybe Word64 -> Maybe [Char] -> PtrOffset -> SPointer
Base_Malloc Maybe Word64
id Maybe [Char]
h (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_FunctionPtr Word64
a [Char]
f)  = Word64 -> [Char] -> PtrOffset -> SPointer
Base_FunctionPtr Word64
a [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_ReturnAddr [Char]
f)     = [Char] -> SPointer
Base_ReturnAddr [Char]
f
saddend_to_spointer (SAddend
SAddend_TLS)              = PtrOffset -> SPointer
Base_TLS (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_StatePart StatePart
sp)     = StatePart -> PtrOffset -> SPointer
Base_StatePart StatePart
sp (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0
saddend_to_spointer (SAddend_FunctionReturn [Char]
f) = [Char] -> PtrOffset -> SPointer
Base_FunctionReturn [Char]
f (PtrOffset -> SPointer) -> PtrOffset -> SPointer
forall a b. (a -> b) -> a -> b
$ Word64 -> PtrOffset
PtrOffset Word64
0





-- SYMBOLIC COMPUTATIONS
mk_expr :: FContext -> SimpleExpr -> SimpleExpr
mk_expr :: FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt SimpleExpr
e = SimpleExpr -> SimpleExpr
trim_expr (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp SimpleExpr
e
 where
  trim_expr :: SimpleExpr -> SimpleExpr
trim_expr SimpleExpr
e
    | SimpleExpr -> Int
expr_size SimpleExpr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
get_max_expr_size = [Char] -> SimpleExpr
forall a. HasCallStack => [Char] -> a
error ([Char] -> SimpleExpr) -> [Char] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> [Char]
forall a. Show a => a -> [Char]
show SimpleExpr
e
    | Bool
otherwise = SimpleExpr
e
  get_max_expr_size :: Int
get_max_expr_size = Context -> Int
ctxt_max_expr_size (Context -> Int) -> Context -> Int
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt

svalue_plus :: FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"plus1" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
 where
  f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)   = FContext -> [Char] -> SValue -> SValue -> SValue
cjoin FContext
fctxt [Char]
"plus2" SValue
v0 SValue
v1
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)   = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si (FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"plus" SValue
v0) SValue
v1
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
v0
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) SValue
Top                 = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"plus5" SValue
v0
svalue_plus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  SValue
Top                 = SValue
v0
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)               = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
t
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)                = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
si SValue
v1 SValue
t
svalue_plus FContext
fctxt Int
si t :: SValue
t@SValue
Top SValue
Top                              = SValue
t


svalue_minus :: FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"minus" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
 where
  f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Minus Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)   = SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SAddends NESet (NESet SAddend)
es1)   = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"minus" SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) SValue
Top                 = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"minus" SValue
v0
svalue_minus FContext
fctxt Int
si v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  SValue
Top                 = SValue
v0
svalue_minus FContext
fctxt Int
si t :: SValue
t@SValue
Top              SValue
_                   = SValue
t


svalue_and :: FContext -> Int -> SValue -> SValue -> SValue
svalue_and FContext
fctxt Int
si v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) v1 :: SValue
v1@(SConcrete NESet SimpleExpr
es1)  = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"and" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ((SimpleExpr, SimpleExpr) -> SimpleExpr)
-> (SimpleExpr, SimpleExpr)
-> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleExpr -> SimpleExpr -> SimpleExpr)
-> (SimpleExpr, SimpleExpr) -> SimpleExpr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> SimpleExpr -> SimpleExpr
f) (NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr)
-> NESet (SimpleExpr, SimpleExpr) -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ NESet SimpleExpr
-> NESet SimpleExpr -> NESet (SimpleExpr, SimpleExpr)
forall a b. NESet a -> NESet b -> NESet (a, b)
NES.cartesianProduct NESet SimpleExpr
es0 NESet SimpleExpr
es1
 where
  f :: SimpleExpr -> SimpleExpr -> SimpleExpr
f SimpleExpr
e0 SimpleExpr
e1 = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
And Int
si [SimpleExpr
e0,SimpleExpr
e1]
svalue_and FContext
fctxt Int
si SValue
v0                 SValue
v1                  = [Char] -> SValue
mk_top ([Char]
"svalue_and" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SValue, SValue) -> [Char]
forall a. Show a => a -> [Char]
show (SValue
v0,SValue
v1))


svalue_unop :: FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SConcrete NESet SimpleExpr
es0) = FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
msg (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SimpleExpr) -> NESet SimpleExpr -> NESet SimpleExpr
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr -> SimpleExpr
f) NESet SimpleExpr
es0
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@(SAddends NESet (NESet SAddend)
es0)  = [Char] -> SValue
mk_top ([Char]
"unop" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg)
svalue_unop FContext
fctxt [Char]
msg SimpleExpr -> SimpleExpr
f v0 :: SValue
v0@SValue
Top             = SValue
v0

svalue_takebits :: FContext -> Int -> SValue -> SValue
svalue_takebits FContext
fctxt Int
h   = FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
"takebits" (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
h)
svalue_sextend :: FContext -> Int -> Int -> SValue -> SValue
svalue_sextend  FContext
fctxt Int
l Int
h = FContext
-> [Char] -> (SimpleExpr -> SimpleExpr) -> SValue -> SValue
svalue_unop FContext
fctxt [Char]
"sextend"  (Int -> Int -> SimpleExpr -> SimpleExpr
SE_SExtend Int
l Int
h)

apply_expr_op :: FContext -> String -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op :: FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
msg [SimpleExpr] -> SimpleExpr
f [SValue]
vs
  | (SValue -> Bool) -> [SValue] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SValue -> Bool
isImmediate [SValue]
vs = 
    let es' :: SimpleExpr
es' = [SimpleExpr] -> SimpleExpr
f ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SValue -> SimpleExpr) -> [SValue] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr)
-> (SValue -> Word64) -> SValue -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Word64 -> Word64
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Word64 -> Word64)
-> (SValue -> Maybe Word64) -> SValue -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SValue -> Maybe Word64
ctry_immediate) [SValue]
vs in
      FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt SimpleExpr
es'
  | SValue
Top SValue -> [SValue] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SValue]
vs      = [Char] -> SValue
mk_top [Char]
""
  | Bool
otherwise          = [Char] -> SValue
mk_top ([Char]
"Making top from: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SValue] -> [Char]
forall a. Show a => a -> [Char]
show [SValue]
vs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"(msg == " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")")
 where
  isImmediate :: SValue -> Bool
isImmediate SValue
v = SValue -> Maybe Word64
ctry_immediate SValue
v Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Word64
forall a. Maybe a
Nothing

  

data CSemantics = ApplyPlus Int | ApplyMinus Int | ApplyNeg Int | ApplyDec Int | ApplyInc Int | ApplyAnd Int |
                  ApplyMov | ApplyCMov | ApplySExtend Int Int |
                  Apply ([SimpleExpr] -> SimpleExpr) | SetXX | SExtension_HI | NoSemantics



csemantics :: FContext -> String -> SymbolicOperation SValue -> SValue
---csemantics fctxt msg _ | trace ("csemantics: "++ msg) False = error "trace"
csemantics :: FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
msg (SO_Plus  SValue
a SValue
b)         = FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
64 SValue
a SValue
b
csemantics FContext
fctxt [Char]
msg (SO_Minus SValue
a SValue
b)         = FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
64 SValue
a SValue
b
csemantics FContext
fctxt [Char]
msg (SO_Times SValue
a SValue
b)         = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"times" (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
64) [SValue
a,SValue
b]
csemantics FContext
fctxt [Char]
msg (SO_Overwrite Int
n SValue
a SValue
b)   = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"overwrite" (\[SimpleExpr
e0,SimpleExpr
e1] -> FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
n SimpleExpr
e0 SimpleExpr
e1) [SValue
a,SValue
b]
csemantics FContext
fctxt [Char]
msg (SO_SExtend Int
l Int
h SValue
a)     = FContext -> Int -> Int -> SValue -> SValue
svalue_sextend FContext
fctxt Int
l Int
h SValue
a
csemantics FContext
fctxt [Char]
msg (SO_Bit Int
h SValue
a)           = FContext -> Int -> SValue -> SValue
svalue_takebits FContext
fctxt Int
h SValue
a
csemantics FContext
fctxt [Char]
msg (SO_Op Opcode
op Int
si Maybe Int
si' [SValue]
es)   = 
  case Opcode -> Int -> Maybe Int -> CSemantics
mnemonic_to_semantics Opcode
op (Int
8Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
si) ((Int -> Int -> Int
forall a. Num a => a -> a -> a
(*) Int
8) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
si') of
    CSemantics
ApplyMov         -> [SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0
    CSemantics
ApplyCMov        -> FContext -> [Char] -> SValue -> SValue -> SValue
cjoin        FContext
fctxt [Char]
"cmov" ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
    ApplyPlus  Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_plus  FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
    ApplyInc   Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_plus  FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
1)
    ApplyMinus Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
    ApplyDec   Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
1)
    ApplyNeg   Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_minus FContext
fctxt Int
si (FContext -> Integer -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Integer
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0)
    ApplyAnd   Int
si    -> FContext -> Int -> SValue -> SValue -> SValue
svalue_and   FContext
fctxt Int
si ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0) ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
1)
    ApplySExtend Int
l Int
h -> FContext -> Int -> Int -> SValue -> SValue
svalue_sextend FContext
fctxt Int
l Int
h ([SValue]
es[SValue] -> Int -> SValue
forall a. [a] -> Int -> a
!!Int
0)
    Apply [SimpleExpr] -> SimpleExpr
sop        -> FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", op = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Opcode -> [Char]
forall a. Show a => a -> [Char]
show Opcode
op) (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleExpr] -> SimpleExpr
sop) [SValue]
es
    CSemantics
SetXX            -> FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"setxx"   (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList [Word64 -> SimpleExpr
SE_Immediate Word64
0,Word64 -> SimpleExpr
SE_Immediate Word64
1]
    CSemantics
SExtension_HI    -> FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"sextend" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> NESet SimpleExpr
forall a. Ord a => [a] -> NESet a
neFromList [Word64 -> SimpleExpr
SE_Immediate Word64
0,Word64 -> SimpleExpr
SE_Immediate Word64
18446744073709551615]
    CSemantics
NoSemantics      -> [Char] -> SValue
mk_top ([Char]
"Widening due to operand: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Opcode -> [Char]
forall a. Show a => a -> [Char]
show Opcode
op)
  






mnemonic_to_semantics :: Opcode -> Int -> Maybe Int -> CSemantics
mnemonic_to_semantics Opcode
SUB Int
si Maybe Int
si'     = Int -> CSemantics
ApplyMinus Int
si
mnemonic_to_semantics Opcode
NEG Int
si Maybe Int
si'     = Int -> CSemantics
ApplyNeg Int
si
mnemonic_to_semantics Opcode
DEC Int
si Maybe Int
si'     = Int -> CSemantics
ApplyDec Int
si

mnemonic_to_semantics Opcode
ADD Int
si Maybe Int
si'     = Int -> CSemantics
ApplyPlus Int
si
mnemonic_to_semantics Opcode
INC Int
si Maybe Int
si'     = Int -> CSemantics
ApplyInc Int
si
mnemonic_to_semantics Opcode
XADD Int
si Maybe Int
si'    = [Char] -> CSemantics
forall a. HasCallStack => [Char] -> a
error ([Char] -> CSemantics) -> [Char] -> CSemantics
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: XADD"

mnemonic_to_semantics Opcode
IMUL_LO Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si
mnemonic_to_semantics Opcode
SHL Int
si Maybe Int
si'     = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
shl
 where
  shl :: [SimpleExpr] -> SimpleExpr
shl [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Times Int
si [SimpleExpr
a,Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
2Word64 -> Word64 -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Word64
i]
  shl [SimpleExpr
a,SimpleExpr
b]              = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Shl Int
si [SimpleExpr
a,SimpleExpr
b]

mnemonic_to_semantics Opcode
IDIV_LO Int
si Maybe Int
si' = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Div Int
si
mnemonic_to_semantics Opcode
SAR Int
si Maybe Int
si'     = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
sar
 where
  sar :: [SimpleExpr] -> SimpleExpr
sar [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Div Int
si [SimpleExpr
a,Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
2Word64 -> Word64 -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Word64
i]
  sar [SimpleExpr
a,SimpleExpr
b]              = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Sar Int
si [SimpleExpr
a,SimpleExpr
b]

mnemonic_to_semantics Opcode
DIV_LO Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Udiv Int
si
mnemonic_to_semantics Opcode
SHR Int
si Maybe Int
si'     = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ [SimpleExpr] -> SimpleExpr
shr
 where
  shr :: [SimpleExpr] -> SimpleExpr
shr [SimpleExpr
a,SE_Immediate Word64
i] = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Udiv Int
si [SimpleExpr
a,Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64
2Word64 -> Word64 -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Word64
i]
  shr [SimpleExpr
a,SimpleExpr
b]              = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Shr Int
si [SimpleExpr
a,SimpleExpr
b]


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

mnemonic_to_semantics Opcode
PEXTRB Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])
mnemonic_to_semantics Opcode
PEXTRD Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])
mnemonic_to_semantics Opcode
PEXTRQ Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a,SimpleExpr
b,SimpleExpr
c] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Pextr Int
si [SimpleExpr
a,SimpleExpr
b,SimpleExpr
c])

mnemonic_to_semantics Opcode
AND Int
si Maybe Int
si'     = Int -> CSemantics
ApplyAnd Int
si
mnemonic_to_semantics Opcode
OR  Int
si Maybe Int
si'     = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Or Int
si
mnemonic_to_semantics Opcode
NOT Int
si Maybe Int
si'     = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ (\[SimpleExpr
a] -> Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Not Int
si [SimpleExpr
a])

mnemonic_to_semantics Opcode
XOR    Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
PXOR   Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
VPXOR  Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
XORPS  Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si
mnemonic_to_semantics Opcode
XORPD  Int
si Maybe Int
si'  = ([SimpleExpr] -> SimpleExpr) -> CSemantics
Apply (([SimpleExpr] -> SimpleExpr) -> CSemantics)
-> ([SimpleExpr] -> SimpleExpr) -> CSemantics
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Xor Int
si

mnemonic_to_semantics Opcode
MOV     Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVSD   Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVSS   Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVAPS  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVAPD  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVUPS  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVUPD  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVABS  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVDQU  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVDQA  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVLPD  Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVD    Int
si Maybe Int
si'  = CSemantics
ApplyMov
mnemonic_to_semantics Opcode
MOVQ    Int
si Maybe Int
si'  = CSemantics
ApplyMov -- 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


cflg_semantics :: p
-> p
-> GenericInstruction label Register prefix Opcode annotation
-> FlagStatus
-> FlagStatus
cflg_semantics p
fctxt p
_ i :: GenericInstruction label Register prefix Opcode annotation
i@(Instruction label
label Maybe prefix
prefix Opcode
mnemonic Maybe (GenericOperand Register)
dst [GenericOperand Register]
srcs Maybe annotation
annot) FlagStatus
flgs = Opcode -> FlagStatus
flg Opcode
mnemonic
 where
  flg :: Opcode -> FlagStatus
flg Opcode
CMP      = Maybe Bool
-> GenericOperand Register -> GenericOperand Register -> FlagStatus
FS_CMP Maybe Bool
forall a. Maybe a
Nothing ([GenericOperand Register]
srcs[GenericOperand Register] -> Int -> GenericOperand Register
forall a. [a] -> Int -> a
!!Int
0) ([GenericOperand Register]
srcs[GenericOperand Register] -> Int -> GenericOperand Register
forall a. [a] -> Int -> a
!!Int
1)

  flg Opcode
PUSH     = FlagStatus
flgs
  flg Opcode
POP      = FlagStatus
flgs
  flg Opcode
LEA      = FlagStatus
flgs
  flg Opcode
LEAVE    = FlagStatus
flgs
  flg Opcode
NOP      = FlagStatus
flgs
  flg Opcode
UD2      = FlagStatus
flgs
  flg Opcode
ENDBR64  = FlagStatus
flgs
  flg Opcode
HLT      = FlagStatus
flgs
  flg Opcode
WAIT     = FlagStatus
flgs
  flg Opcode
MFENCE   = FlagStatus
flgs
  flg Opcode
CLFLUSH  = FlagStatus
flgs
  flg Opcode
MOV      = FlagStatus
flgs
  flg Opcode
MOVSD    = FlagStatus
flgs
  flg Opcode
MOVSS    = FlagStatus
flgs
  flg Opcode
MOVAPS   = FlagStatus
flgs
  flg Opcode
MOVAPD   = FlagStatus
flgs
  flg Opcode
MOVUPS   = FlagStatus
flgs
  flg Opcode
MOVUPD   = FlagStatus
flgs
  flg Opcode
MOVABS   = FlagStatus
flgs
  flg Opcode
MOVDQU   = FlagStatus
flgs
  flg Opcode
MOVDQA   = FlagStatus
flgs
  flg Opcode
MOVLPD   = FlagStatus
flgs
  flg Opcode
MOVD     = FlagStatus
flgs
  flg Opcode
VMOVD    = FlagStatus
flgs
  flg Opcode
VMOVAPD  = FlagStatus
flgs
  flg Opcode
VMOVAPS  = FlagStatus
flgs
  flg Opcode
MOVZX    = FlagStatus
flgs
  flg Opcode
MOVSX    = FlagStatus
flgs
  flg Opcode
MOVSXD   = FlagStatus
flgs
  flg Opcode
CMOVO    = FlagStatus
flgs
  flg Opcode
CMOVNO   = FlagStatus
flgs
  flg Opcode
CMOVS    = FlagStatus
flgs
  flg Opcode
CMOVNS   = FlagStatus
flgs
  flg Opcode
CMOVE    = FlagStatus
flgs
  flg Opcode
CMOVZ    = FlagStatus
flgs
  flg Opcode
CMOVNE   = FlagStatus
flgs
  flg Opcode
CMOVNZ   = FlagStatus
flgs
  flg Opcode
CMOVB    = FlagStatus
flgs
  flg Opcode
CMOVNAE  = FlagStatus
flgs
  flg Opcode
CMOVC    = FlagStatus
flgs
  flg Opcode
CMOVNB   = FlagStatus
flgs
  flg Opcode
CMOVAE   = FlagStatus
flgs
  flg Opcode
CMOVNC   = FlagStatus
flgs
  flg Opcode
CMOVBE   = FlagStatus
flgs
  flg Opcode
CMOVNA   = FlagStatus
flgs
  flg Opcode
CMOVA    = FlagStatus
flgs
  flg Opcode
CMOVNBE  = FlagStatus
flgs
  flg Opcode
CMOVL    = FlagStatus
flgs
  flg Opcode
CMOVNGE  = FlagStatus
flgs
  flg Opcode
CMOVG    = FlagStatus
flgs
  flg Opcode
CMOVGE   = FlagStatus
flgs
  flg Opcode
CMOVNL   = FlagStatus
flgs
  flg Opcode
CMOVLE   = FlagStatus
flgs
  flg Opcode
CMOVNG   = FlagStatus
flgs
  flg Opcode
CMOVNLE  = FlagStatus
flgs
  flg Opcode
CMOVP    = FlagStatus
flgs
  flg Opcode
CMOVPE   = FlagStatus
flgs
  flg Opcode
CMOVNP   = FlagStatus
flgs
  flg Opcode
CMOVPO   = FlagStatus
flgs
  flg Opcode
SETO     = FlagStatus
flgs
  flg Opcode
SETNO    = FlagStatus
flgs
  flg Opcode
SETS     = FlagStatus
flgs
  flg Opcode
SETNS    = FlagStatus
flgs
  flg Opcode
SETE     = FlagStatus
flgs
  flg Opcode
SETZ     = FlagStatus
flgs
  flg Opcode
SETNE    = FlagStatus
flgs
  flg Opcode
SETNZ    = FlagStatus
flgs
  flg Opcode
SETB     = FlagStatus
flgs
  flg Opcode
SETNAE   = FlagStatus
flgs
  flg Opcode
SETC     = FlagStatus
flgs
  flg Opcode
SETNB    = FlagStatus
flgs
  flg Opcode
SETAE    = FlagStatus
flgs
  flg Opcode
SETNC    = FlagStatus
flgs
  flg Opcode
SETBE    = FlagStatus
flgs
  flg Opcode
SETNA    = FlagStatus
flgs
  flg Opcode
SETA     = FlagStatus
flgs
  flg Opcode
SETNBE   = FlagStatus
flgs
  flg Opcode
SETL     = FlagStatus
flgs
  flg Opcode
SETNGE   = FlagStatus
flgs
  flg Opcode
SETG     = FlagStatus
flgs
  flg Opcode
SETGE    = FlagStatus
flgs
  flg Opcode
SETNL    = FlagStatus
flgs
  flg Opcode
SETLE    = FlagStatus
flgs
  flg Opcode
SETNG    = FlagStatus
flgs
  flg Opcode
SETNLE   = FlagStatus
flgs
  flg Opcode
SETP     = FlagStatus
flgs
  flg Opcode
SETPE    = FlagStatus
flgs
  flg Opcode
SETNP    = FlagStatus
flgs
  flg Opcode
SETPO    = FlagStatus
flgs
  flg Opcode
CBW      = FlagStatus
flgs
  flg Opcode
CWDE     = FlagStatus
flgs
  flg Opcode
CDQE     = FlagStatus
flgs
  flg Opcode
CWD      = FlagStatus
flgs
  flg Opcode
CDQ      = FlagStatus
flgs
  flg Opcode
CQO      = FlagStatus
flgs
  flg Opcode
XCHG     = FlagStatus
flgs
  flg Opcode
mnemonic = if Opcode -> Bool
isJump Opcode
mnemonic Bool -> Bool -> Bool
|| Opcode -> Bool
isCondJump Opcode
mnemonic then FlagStatus
flgs else FlagStatus
None -- TODO



-- MAKING INITIAL VALUES

cmk_init_reg_value :: FContext  -> Register -> SValue
cmk_init_reg_value :: FContext -> Register -> SValue
cmk_init_reg_value FContext
fctxt = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue)
-> (Register -> SimpleExpr) -> Register -> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr)
-> (Register -> StatePart) -> Register -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> StatePart
SP_Reg

offset_to_expr :: PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
UnknownOffset SimpleExpr
e = Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
64 [SimpleExpr
e,BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
""]
offset_to_expr (PtrOffset Word64
0) SimpleExpr
e = SimpleExpr
e
offset_to_expr (PtrOffset Word64
i) SimpleExpr
e = SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
Plus Int
64 [SimpleExpr
e,Word64 -> SimpleExpr
SE_Immediate Word64
i]

-- Concert SValues to SExpressions
spointer_to_expr :: SPointer -> SimpleExpr
spointer_to_expr (Base_StackPointer [Char]
f  PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f
spointer_to_expr (Base_Immediate Word64
i     PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
i
spointer_to_expr (Base_Malloc Maybe Word64
id Maybe [Char]
h     PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
h
spointer_to_expr (Base_FunctionPtr Word64
a [Char]
f PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8
spointer_to_expr (Base_ReturnAddr [Char]
f)            = StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f) Int
8
spointer_to_expr (Base_TLS             PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg Register
FS)
spointer_to_expr (Base_StatePart StatePart
sp    PtrOffset
offset)  = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
spointer_to_expr (Base_FunctionReturn [Char]
f PtrOffset
offset) = PtrOffset -> SimpleExpr -> SimpleExpr
offset_to_expr PtrOffset
offset (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
f

cmk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue
cmk_init_mem_value :: FContext -> [Char] -> SPointer -> RegionSize -> SValue
cmk_init_mem_value FContext
fctxt [Char]
msg SPointer
a RegionSize
si = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
mk_a (Int -> StatePart) -> Int -> StatePart
forall a b. (a -> b) -> a -> b
$ RegionSize -> Int
forall p. Num p => RegionSize -> p
mk_si RegionSize
si
 where
  mk_a :: SimpleExpr
mk_a            = SPointer -> SimpleExpr
spointer_to_expr SPointer
a
  mk_si :: RegionSize -> p
mk_si (Nat Word64
imm) = Word64 -> p
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
imm
  mk_si RegionSize
_         = p
1




-- MEMORY RELATIONS
cseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
---cseparate fctxt msg v0 s0 v1 si1 | trace ("cseparate: "++ show (v0,v1)) False = error "trace"
cseparate :: FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate FContext
fctxt [Char]
msg SPointer
a0 (Nat Word64
si0) SPointer
a1 (Nat Word64
si1) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
  [ SPointer -> SPointer -> Bool
separation_based_on_necessity SPointer
a0 SPointer
a1 
  , FContext
-> [Char] -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
forall p.
FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt [Char]
msg SPointer
a0 Word64
si0 SPointer
a1 Word64
si1]
 where
  separation_based_on_necessity :: SPointer -> SPointer -> Bool
separation_based_on_necessity SPointer
a0 SPointer
a1 = SimpleExpr -> Word64 -> SimpleExpr -> Word64 -> Bool
forall a.
(Ord a, Num a) =>
SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate_expressions (SPointer -> SimpleExpr
spointer_to_expr SPointer
a0) Word64
si0 (SPointer -> SimpleExpr
spointer_to_expr SPointer
a1) Word64
si1
cseparate FContext
fctxt [Char]
msg SPointer
a0 RegionSize
_ SPointer
a1 RegionSize
_ = FContext
-> [Char] -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
forall p.
FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt [Char]
msg SPointer
a0 (Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
20) SPointer
a1 (Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
20)


mk_sstatepart :: FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt (SP_Reg Register
r)    = Register -> SStatePart
SSP_Reg Register
r
mk_sstatepart FContext
fctxt (SP_Mem SimpleExpr
a Int
si) =
  case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
a of
    Just SPointer
ptr -> SPointer -> Int -> SStatePart
SSP_Mem SPointer
ptr Int
si
    Maybe SPointer
Nothing  -> [Char] -> SStatePart
forall a. HasCallStack => [Char] -> a
error ([Char] -> SStatePart) -> [Char] -> SStatePart
forall a b. (a -> b) -> a -> b
$ [Char]
"CANNOT PROMOTE: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SimpleExpr, Int) -> [Char]
forall a. Show a => a -> [Char]
show (SimpleExpr
a,Int
si)

separation_of_spointers :: FContext -> p -> SPointer -> Word64 -> SPointer -> Word64 -> Bool
separation_of_spointers FContext
fctxt p
msg SPointer
v0 Word64
si0 SPointer
v1 Word64
si1 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ SPointer
v0 SPointer -> SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= SPointer
v1
  , SPointer -> SPointer -> Bool
separate_bases SPointer
v0 SPointer
v1 ]
 where
  -- Separation using pointer bases 
  separate_bases :: SPointer -> SPointer -> Bool
separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_StackPointer [Char]
f1 PtrOffset
_)
    | [Char]
f0 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
f1  = Bool
False -- if (a0,si0) == (a1,si1) then False else trace ("SEP: " ++ show (a0,si0,a1,si1)) False
    | Bool
otherwise = Bool
True -- TODO ADD VC
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_Malloc Maybe Word64
_ Maybe [Char]
_ PtrOffset
_)           = Bool
True
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
_)      = Bool
True
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_TLS PtrOffset
_)                  = Bool
True
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_StatePart StatePart
_ PtrOffset
_)          = Bool
True -- TODO add vc
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_Immediate Word64
_ PtrOffset
_)          = Bool
True
  separate_bases (Base_StackPointer [Char]
f0 PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_)     = Bool
True-- TODO add vc

  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_Malloc Maybe Word64
id1 Maybe [Char]
h1 PtrOffset
_)        = Maybe Word64
id0 Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Word64
id1
  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
_)      = Bool
True
  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_TLS PtrOffset
_)                  = Bool
True
  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_StatePart StatePart
_ PtrOffset
_)          = Bool
True
  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_Immediate Word64
_ PtrOffset
_)          = Bool
True
  separate_bases (Base_Malloc Maybe Word64
id0 Maybe [Char]
h0 PtrOffset
_)   (Base_FunctionReturn [Char]
_ PtrOffset
_)     = Bool
True


  separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_FunctionPtr Word64
a1 [Char]
_ PtrOffset
_)    = Word64
a0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
a1
  separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_TLS PtrOffset
_)                 = Bool
True
  separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_StatePart StatePart
_  PtrOffset
_)        = Bool
True
  separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_Immediate Word64
i1 PtrOffset
_)        = Bool
True -- TODO???
  separate_bases (Base_FunctionPtr Word64
a0 [Char]
_ PtrOffset
_) (Base_FunctionReturn [Char]
_ PtrOffset
_)    = Bool
True-- TODO add vc

  separate_bases (Base_TLS PtrOffset
_)              (Base_TLS PtrOffset
_)                 = Bool
False
  separate_bases (Base_TLS PtrOffset
_)              (Base_StatePart StatePart
_ PtrOffset
_)         = Bool
True
  separate_bases (Base_TLS PtrOffset
_)              (Base_Immediate Word64
_ PtrOffset
_)         = Bool
True
  separate_bases (Base_TLS PtrOffset
_)              (Base_FunctionReturn [Char]
_ PtrOffset
_)    = Bool
True-- TODO add vc


  separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_)    (Base_StatePart StatePart
sp1 PtrOffset
_)       = 
    case (SStatePart, SStatePart)
-> Map (SStatePart, SStatePart) MemRelation -> Maybe MemRelation
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp0,FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp1) Map (SStatePart, SStatePart) MemRelation
m of
      Just MemRelation
Separate -> Bool
True
      Maybe MemRelation
_             -> Bool
False
  separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_)    (Base_Immediate Word64
imm1 PtrOffset
_)      =
    case ((StatePart, Maybe SValue) -> Bool)
-> Set (StatePart, Maybe SValue) -> Maybe (StatePart, Maybe SValue)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(StatePart
sp',Maybe SValue
_) -> StatePart
sp0 StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== StatePart
sp') Set (StatePart, Maybe SValue)
sps of
      Just (StatePart
_,Just SValue
imm) -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen?" -- cseparate fctxt msg a0 si0 imm si1
      Maybe (StatePart, Maybe SValue)
_ -> Bool
True 
  separate_bases (Base_StatePart StatePart
sp0 PtrOffset
_)    (Base_FunctionReturn [Char]
_ PtrOffset
_)    = Bool
True-- TODO add vc



  separate_bases (Base_Immediate Word64
i0 (PtrOffset Word64
off0)) (Base_Immediate Word64
i1 PtrOffset
UnknownOffset)  = Word64
i0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
off0 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
si0 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
i1 -- TODO add VC
  separate_bases (Base_Immediate Word64
i0 PtrOffset
UnknownOffset) (Base_Immediate Word64
i1  (PtrOffset Word64
off1)) = Word64
i1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
off1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
si1 Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
i0 -- TODO add VC
  separate_bases (Base_Immediate Word64
i0 PtrOffset
_)     (Base_Immediate Word64
i1 PtrOffset
_)
    | Context -> Word64 -> Word64 -> Bool
forall a1 a2.
(Integral a1, Integral a2) =>
Context -> a1 -> a2 -> Bool
pointers_from_different_global_section (FContext -> Context
f_ctxt FContext
fctxt) Word64
i0 Word64
i1      = Bool
True -- TODO ADD VC
    | Word64
i0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
i1                                                         = Bool
False -- REMOVE TODO ADD VC error $ "Separation of " ++ show (a0, si0, a1, si1) ++ "\nFINIT ==\n" ++ show (f_init fctxt) ++ "\nmsg = " ++ msg
    | Bool
otherwise                                                        = Bool
False
  separate_bases (Base_Immediate Word64
i0 PtrOffset
_)     (Base_FunctionReturn [Char]
_ PtrOffset
_)   = Bool
True-- TODO add vc



  separate_bases (Base_FunctionReturn [Char]
f0 PtrOffset
_ ) (Base_FunctionReturn [Char]
f1 PtrOffset
_) = [Char]
f0[Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/=[Char]
f1-- TODO add vc


  separate_bases (Base_ReturnAddr [Char]
f0)      (Base_ReturnAddr [Char]
f1)        = [Char]
f0 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
f1
  separate_bases (Base_ReturnAddr [Char]
f0)      SPointer
_                           = Bool
True
  separate_bases SPointer
_                         (Base_ReturnAddr [Char]
f0)        = Bool
True

  separate_bases SPointer
b0 SPointer
b1 = SPointer -> SPointer -> Bool
separate_bases SPointer
b1 SPointer
b0

  FInit Set (StatePart, Maybe SValue)
sps Map (SStatePart, SStatePart) MemRelation
m = FContext -> FInit
f_init FContext
fctxt 



calias :: p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias p
fctxt SPointer
a0 RegionSize
si0 SPointer
a1 RegionSize
si1 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ RegionSize
si0 RegionSize -> RegionSize -> Bool
forall a. Eq a => a -> a -> Bool
/= RegionSize
UnknownSize
  , RegionSize
si1 RegionSize -> RegionSize -> Bool
forall a. Eq a => a -> a -> Bool
/= RegionSize
UnknownSize
  , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool
has_unknown_offset SPointer
a0
  , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> Bool
has_unknown_offset SPointer
a1
  , (SPointer
a0,RegionSize
si0) (SPointer, RegionSize) -> (SPointer, RegionSize) -> Bool
forall a. Eq a => a -> a -> Bool
== (SPointer
a1,RegionSize
si1) ]

{--
  -- TODO experiment with this
  aliassing_ptrvalues si0' si1' (Base_StatePart sp0 (PtrOffset off0)) (Base_StatePart sp1 (PtrOffset off1)) = off0 == off1 && or
    [ sp0 == sp1
    , M.lookup (mk_sstatepart fctxt sp0,mk_sstatepart fctxt sp1) m == Just Aliassing ]
  aliassing_ptrvalues si0' si1' ptr0 ptr1 = and
    [ ptr0 == ptr1
    , not $ has_unknown_offset ptr0
    , not $ has_unknown_offset ptr1 ]

  FInit _ m = f_init fctxt
--}

cenclosed :: p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
cenclosed p
fctxt SPointer
a0 (Nat Word64
si0) SPointer
a1 (Nat Word64
si1) = 
  let v0 :: SimpleExpr
v0 = SPointer -> SimpleExpr
spointer_to_expr SPointer
a0
      v1 :: SimpleExpr
v1 = SPointer -> SimpleExpr
spointer_to_expr SPointer
a1 in
    SimpleExpr -> Word64 -> SimpleExpr -> Word64 -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
v0 Word64
si0 SimpleExpr
v1 Word64
si1
cenclosed p
fctxt SPointer
a0 RegionSize
_ SPointer
a1 RegionSize
_ = Bool
False




csensitive :: p -> SPointer -> RegionSize -> SValue -> Bool
csensitive p
fctxt SPointer
a (Nat Word64
si) SValue
v =
  case SValue -> Maybe SimpleExpr
ctry_deterministic SValue
v of
    (Just SimpleExpr
v') -> SPointer -> Word64 -> Bool
forall p. SPointer -> p -> Bool
is_top_stackframe SPointer
a Word64
si Bool -> Bool -> Bool
|| SPointer -> Word64 -> SimpleExpr -> Bool
forall p. SPointer -> p -> SimpleExpr -> Bool
is_pushed_reg SPointer
a Word64
si SimpleExpr
v' 
    Maybe SimpleExpr
_         -> Bool
False
 where
  is_initial_reg :: SimpleExpr -> Bool
is_initial_reg (SE_Var (SP_Reg Register
_)) = Bool
True
  is_initial_reg SimpleExpr
_                   = Bool
False
  
  is_top_stackframe :: SPointer -> p -> Bool
is_top_stackframe (Base_StackPointer [Char]
_ (PtrOffset Word64
0)) p
_ = Bool
True
  is_top_stackframe SPointer
_ p
_ = Bool
False
  is_pushed_reg :: SPointer -> p -> SimpleExpr -> Bool
is_pushed_reg SPointer
a' p
si' SimpleExpr
v' = SimpleExpr -> Bool
is_initial_reg SimpleExpr
v' Bool -> Bool -> Bool
&& p -> SPointer -> Bool
forall p. p -> SPointer -> Bool
is_local_spointer p
fctxt SPointer
a'
csensitive p
fctxt SPointer
a RegionSize
UnknownSize SValue
v = Bool
False


cread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_ro_data FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt (Word64 -> SValue) -> Maybe Word64 -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection (FContext -> Context
f_ctxt FContext
fctxt) Word64
a (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si)
cread_from_ro_data FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing

cread_from_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_data FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt (Word64 -> SValue) -> Maybe Word64 -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Word64 -> Int -> Maybe Word64
read_from_datasection (FContext -> Context
f_ctxt FContext
fctxt) Word64
a (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si)
cread_from_data FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing

ctry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue
ctry_relocation FContext
fctxt (Base_Immediate Word64
a (PtrOffset Word64
0)) (Nat Word64
si) = Word64 -> Maybe SValue
try_reloc Word64
a Maybe SValue -> Maybe SValue -> Maybe SValue
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((\[Char]
_ -> Word64 -> SValue
mk_value Word64
a) ([Char] -> SValue) -> Maybe [Char] -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FContext -> Word64 -> Maybe [Char]
forall a. Integral a => FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt Word64
a)
 where
  ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt

  try_reloc :: Word64 -> Maybe SValue
try_reloc Word64
a' = Relocation -> SValue
get_trgt (Relocation -> SValue) -> Maybe Relocation -> Maybe SValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Relocation -> Bool) -> Set Relocation -> Maybe Relocation
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> Relocation -> Bool
is_reloc_for Word64
a') (Set Relocation -> Maybe Relocation)
-> Set Relocation -> Maybe Relocation
forall a b. (a -> b) -> a -> b
$ Context -> Set Relocation
ctxt_relocs (Context -> Set Relocation) -> Context -> Set Relocation
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt)
  is_reloc_for :: Word64 -> Relocation -> Bool
is_reloc_for Word64
a' (Relocation Word64
a0 Word64
a1) = Word64
a0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a'
  get_trgt :: Relocation -> SValue
get_trgt (Relocation Word64
a0 Word64
a1) = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
a1

  mk_value :: Word64 -> SValue
mk_value Word64
a' = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a') Int
8

ctry_relocation FContext
fctxt SPointer
_ RegionSize
_ = Maybe SValue
forall a. Maybe a
Nothing


-- If *[a,8] contains a relocated value to some function f, return that function
try_relocated_pointer :: FContext -> a -> Maybe [Char]
try_relocated_pointer FContext
fctxt a
a =
  case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt of
    Just (Relocated_Function [Char]
f) -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
f
    Maybe Symbol
_ -> Maybe [Char]
forall a. Maybe a
Nothing
 where
  ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt




instance SymbolicExecutable FContext SValue SPointer where
  sseparate :: FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
sseparate                = FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate
  senclosed :: FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
senclosed                = FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
cenclosed
  salias :: FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
salias                   = FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias
  ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool
ssensitive               = FContext -> SPointer -> RegionSize -> SValue -> Bool
forall p. p -> SPointer -> RegionSize -> SValue -> Bool
csensitive
  sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue
sread_from_ro_data       = FContext -> SPointer -> RegionSize -> Maybe SValue
cread_from_ro_data
  smk_mem_addresses :: FContext -> [Char] -> SValue -> Set SPointer
smk_mem_addresses        = FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses
  sjoin_values :: FContext -> [Char] -> t SValue -> SValue
sjoin_values             = FContext -> [Char] -> t SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all
  swiden_values :: FContext -> [Char] -> SValue -> SValue
swiden_values            = FContext -> [Char] -> SValue -> SValue
cwiden
  sjoin_pointers :: FContext -> [SPointer] -> [SPointer]
sjoin_pointers           = FContext -> [SPointer] -> [SPointer]
forall p. p -> [SPointer] -> [SPointer]
cjoin_pointers
  ssemantics :: FContext -> [Char] -> SymbolicOperation SValue -> SValue
ssemantics               = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics
  sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus
sflg_semantics           = FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus
forall p p label prefix annotation.
p
-> p
-> GenericInstruction label Register prefix Opcode annotation
-> FlagStatus
-> FlagStatus
cflg_semantics
  simmediate :: FContext -> i -> SValue
simmediate               = FContext -> i -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate
  top :: FContext -> [Char] -> SValue
top                      = \FContext
_ -> [Char] -> SValue
mk_top
  smk_init_reg_value :: FContext -> Register -> SValue
smk_init_reg_value       = FContext -> Register -> SValue
cmk_init_reg_value
  smk_init_mem_value :: FContext -> [Char] -> SPointer -> RegionSize -> SValue
smk_init_mem_value       = FContext -> [Char] -> SPointer -> RegionSize -> SValue
cmk_init_mem_value
  sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
sjump                    = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
jump
  scall :: FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
scall                    = FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call
  stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
stry_jump_targets        = FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets
  stry_immediate :: FContext -> SValue -> Maybe Word64
stry_immediate           = \FContext
_ -> SValue -> Maybe Word64
ctry_immediate 
  stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr
stry_deterministic       = \FContext
_ -> SValue -> Maybe SimpleExpr
ctry_deterministic 
  stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue
stry_relocation          = FContext -> SPointer -> RegionSize -> Maybe SValue
ctry_relocation
  saddress_has_instruction :: FContext -> Word64 -> Bool
saddress_has_instruction = \FContext
ctxt -> Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction (FContext -> Context
f_ctxt FContext
ctxt)


instance Propagator FContext Predicate where
  tau :: FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
tau     = FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, VCS)
sexec_block
  join :: FContext
-> [Char]
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> Sstate SValue SPointer
join    = FContext
-> [Char]
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> Sstate SValue SPointer
forall v p1 ctxt p2.
(SymbolicExecutable ctxt v p1, SymbolicExecutable ctxt v p2) =>
ctxt -> [Char] -> Sstate v p1 -> Sstate v p1 -> Sstate v p1
sjoin_states
  implies :: FContext
-> Sstate SValue SPointer -> Sstate SValue SPointer -> Bool
implies = FContext
-> Sstate SValue SPointer -> Sstate SValue SPointer -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Sstate v p -> Sstate v p -> Bool
simplies






-- | Get the currently known invariant for the given instruction address
get_invariant :: FContext -> Int -> Maybe Predicate
get_invariant :: FContext -> Int -> Maybe (Sstate SValue SPointer)
get_invariant FContext
fctxt Int
a = do
  let ctxt :: Context
ctxt   = FContext -> Context
f_ctxt FContext
fctxt
  let entry :: Int
entry  = FContext -> Int
f_entry FContext
fctxt
  CFG
g         <- Int -> IntMap CFG -> Maybe CFG
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap CFG -> Maybe CFG) -> IntMap CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ Context -> IntMap CFG
ctxt_cfgs   Context
ctxt
  Invariants
invs      <- Int -> IntMap Invariants -> Maybe Invariants
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap Invariants -> Maybe Invariants)
-> IntMap Invariants -> Maybe Invariants
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Invariants
ctxt_invs   Context
ctxt
  Int
blockId   <- Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
a (IntMap Int -> Maybe Int) -> IntMap Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap Int
cfg_addr_to_blockID CFG
g
  Sstate SValue SPointer
p         <- Int -> Invariants -> Maybe (Sstate SValue SPointer)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockId Invariants
invs
  [Instruction]
instrs    <- Int -> IntMap [Instruction] -> Maybe [Instruction]
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockId (IntMap [Instruction] -> Maybe [Instruction])
-> IntMap [Instruction] -> Maybe [Instruction]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
g

  Sstate SValue SPointer -> Maybe (Sstate SValue SPointer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sstate SValue SPointer -> Maybe (Sstate SValue SPointer))
-> Sstate SValue SPointer -> Maybe (Sstate SValue SPointer)
forall a b. (a -> b) -> a -> b
$ (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a, b) -> a
fst ((Sstate SValue SPointer, VCS) -> Sstate SValue SPointer)
-> (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ FContext
-> [Instruction]
-> Maybe [Instruction]
-> Sstate SValue SPointer
-> (Sstate SValue SPointer, VCS)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, VCS)
sexec_block FContext
fctxt ((Instruction -> Bool) -> [Instruction] -> [Instruction]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Instruction
i -> Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
a) [Instruction]
instrs) Maybe [Instruction]
forall a. Maybe a
Nothing Sstate SValue SPointer
p



-- | The initial predicate.
init_pred ::
  FContext                      -- ^ The current context
  -> String                     -- ^ The current function
  -> Invariants                 -- ^ The currently available invariants
  -> S.Set (NodeInfo,Predicate) -- ^ The currently known postconditions
  -> S.Set SStatePart            -- ^ The currently known stateparts of the function
  -> Predicate
init_pred :: FContext
-> [Char]
-> Invariants
-> Set (NodeInfo, Sstate SValue SPointer)
-> Set SStatePart
-> Sstate SValue SPointer
init_pred FContext
fctxt [Char]
f Invariants
curr_invs Set (NodeInfo, Sstate SValue SPointer)
curr_posts Set SStatePart
curr_sps =
  let FInit Set (StatePart, Maybe SValue)
finit Map (SStatePart, SStatePart) MemRelation
_        = FContext -> FInit
f_init FContext
fctxt -- M.filter (not . contains_bot) $ 

      sps :: Set SStatePart
sps                  = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [Set SStatePart
curr_sps, (StatePart -> SStatePart) -> Set StatePart -> Set SStatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt) (Set StatePart -> Set SStatePart)
-> Set StatePart -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> StatePart)
-> Set (StatePart, Maybe SValue) -> Set StatePart
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (StatePart, Maybe SValue) -> StatePart
forall a b. (a, b) -> a
fst Set (StatePart, Maybe SValue)
finit, (SStatePart -> Set SStatePart -> Set SStatePart
forall a. Ord a => a -> Set a -> Set a
S.delete (Register -> SStatePart
SSP_Reg Register
RIP) (Set SStatePart -> Set SStatePart)
-> Set SStatePart -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ Invariants
-> Set (NodeInfo, Sstate SValue SPointer) -> Set SStatePart
gather_stateparts Invariants
curr_invs Set (NodeInfo, Sstate SValue SPointer)
curr_posts)]
      ([Register]
regs,[(SPointer, Int)]
regions)       = (SStatePart -> Either Register (SPointer, Int))
-> [SStatePart] -> ([Register], [(SPointer, Int)])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith SStatePart -> Either Register (SPointer, Int)
reg_or_mem ([SStatePart] -> ([Register], [(SPointer, Int)]))
-> [SStatePart] -> ([Register], [(SPointer, Int)])
forall a b. (a -> b) -> a -> b
$ Set SStatePart -> [SStatePart]
forall a. Set a -> [a]
S.toList Set SStatePart
sps

      rsp0 :: SValue
rsp0                 = NESet SimpleExpr -> SValue
SConcrete (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f
      write_stack_pointer :: Sstate SValue SPointer -> Sstate SValue SPointer
write_stack_pointer  = State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_rreg FContext
fctxt Register
RSP SValue
rsp0)
      top_stack_frame :: SValue
top_stack_frame      = NESet SimpleExpr -> SValue
SConcrete (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> NESet SimpleExpr
forall a. a -> NESet a
NES.singleton (SimpleExpr -> NESet SimpleExpr) -> SimpleExpr -> NESet SimpleExpr
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> StatePart
SP_StackPointer [Char]
f) Int
8
      write_return_address :: Sstate SValue SPointer -> Sstate SValue SPointer
write_return_address = State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> Bool
-> SValue
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem FContext
fctxt Bool
True SValue
rsp0 (Word64 -> RegionSize
Nat Word64
8) SValue
top_stack_frame)

      sregs :: Map Register SValue
sregs                = [(Register, SValue)] -> Map Register SValue
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Register, SValue)] -> Map Register SValue)
-> [(Register, SValue)] -> Map Register SValue
forall a b. (a -> b) -> a -> b
$ (Register -> (Register, SValue))
-> [Register] -> [(Register, SValue)]
forall a b. (a -> b) -> [a] -> [b]
map (\Register
r -> (Register
r,FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg Register
r))) [Register]
regs
      smem :: Map k a
smem                 = Map k a
forall k a. Map k a
M.empty in
    Sstate SValue SPointer -> Sstate SValue SPointer
write_stack_pointer (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> Sstate SValue SPointer
write_return_address (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit (Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a. Set a -> [a]
S.toList Set (StatePart, Maybe SValue)
finit) (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ (Map Register SValue
-> Map (SPointer, RegionSize) SValue
-> FlagStatus
-> Sstate SValue SPointer
forall v p.
Map Register v -> Map (p, RegionSize) v -> FlagStatus -> Sstate v p
Sstate Map Register SValue
sregs Map (SPointer, RegionSize) SValue
forall k a. Map k a
smem FlagStatus
None) 
 where
  reg_or_mem :: SStatePart -> Either Register (SPointer, Int)
reg_or_mem (SSP_Reg Register
r) = Register -> Either Register (SPointer, Int)
forall a b. a -> Either a b
Left Register
r
  reg_or_mem (SSP_Mem SPointer
a Int
si) = (SPointer, Int) -> Either Register (SPointer, Int)
forall a b. b -> Either a b
Right (SPointer
a,Int
si)

  write_finit :: [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [] Sstate SValue SPointer
s                   = Sstate SValue SPointer
s
  write_finit ((StatePart
sp,Maybe SValue
Nothing):[(StatePart, Maybe SValue)]
finit) Sstate SValue SPointer
s = [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [(StatePart, Maybe SValue)]
finit Sstate SValue SPointer
s
  write_finit ((StatePart
sp,Just SValue
v):[(StatePart, Maybe SValue)]
finit)  Sstate SValue SPointer
s = [(StatePart, Maybe SValue)]
-> Sstate SValue SPointer -> Sstate SValue SPointer
write_finit [(StatePart, Maybe SValue)]
finit (Sstate SValue SPointer -> Sstate SValue SPointer)
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ State (Sstate SValue SPointer, VCS) ()
-> Sstate SValue SPointer -> Sstate SValue SPointer
forall v p b. State (Sstate v p, VCS) b -> Sstate v p -> Sstate v p
execSstate (FContext
-> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp FContext
fctxt (FContext -> StatePart -> SStatePart
mk_sstatepart FContext
fctxt StatePart
sp) SValue
v) Sstate SValue SPointer
s

  


-- | Given the currently known invariants and postconditions, gather all stateparts occurring in the current function.
gather_stateparts ::
     Invariants                 -- ^ The currently available invariants
  -> S.Set (NodeInfo,Predicate) -- ^ The currently known postconditions
  -> S.Set SStatePart
gather_stateparts :: Invariants
-> Set (NodeInfo, Sstate SValue SPointer) -> Set SStatePart
gather_stateparts Invariants
invs Set (NodeInfo, Sstate SValue SPointer)
posts = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [(Sstate SValue SPointer -> Set SStatePart -> Set SStatePart)
-> Set SStatePart -> Invariants -> Set SStatePart
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IM.foldr Sstate SValue SPointer -> Set SStatePart -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart -> Set SStatePart
accumulate_stateparts Set SStatePart
forall a. Set a
S.empty Invariants
invs, Set (Sstate SValue SPointer) -> Set SStatePart
forall b. Set (Sstate b SPointer) -> Set SStatePart
get_stateparts_of_sstates (((NodeInfo, Sstate SValue SPointer) -> Sstate SValue SPointer)
-> Set (NodeInfo, Sstate SValue SPointer)
-> Set (Sstate SValue SPointer)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (NodeInfo, Sstate SValue SPointer) -> Sstate SValue SPointer
forall a b. (a, b) -> b
snd Set (NodeInfo, Sstate SValue SPointer)
posts)]
 where
  accumulate_stateparts :: Sstate b SPointer -> Set SStatePart -> Set SStatePart
accumulate_stateparts Sstate b SPointer
p = Set SStatePart -> Set SStatePart -> Set SStatePart
forall a. Ord a => Set a -> Set a -> Set a
S.union (Sstate b SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate Sstate b SPointer
p)

  get_stateparts_of_sstates :: Set (Sstate b SPointer) -> Set SStatePart
get_stateparts_of_sstates Set (Sstate b SPointer)
ps = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set SStatePart] -> Set SStatePart)
-> [Set SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ (Sstate b SPointer -> Set SStatePart)
-> [Sstate b SPointer] -> [Set SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map Sstate b SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate ([Sstate b SPointer] -> [Set SStatePart])
-> [Sstate b SPointer] -> [Set SStatePart]
forall a b. (a -> b) -> a -> b
$ Set (Sstate b SPointer) -> [Sstate b SPointer]
forall a. Set a -> [a]
S.toList (Set (Sstate b SPointer) -> [Sstate b SPointer])
-> Set (Sstate b SPointer) -> [Sstate b SPointer]
forall a b. (a -> b) -> a -> b
$ Set (Sstate b SPointer)
ps

get_stateparts_of_sstate :: Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate (Sstate Map Register b
sregs Map (SPointer, RegionSize) b
smem FlagStatus
_) = [Set SStatePart] -> Set SStatePart
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [Map Register b -> Set SStatePart
forall a. Map Register a -> Set SStatePart
gather_regs Map Register b
sregs, Map Register b -> Set SStatePart
forall p a. p -> Set a
gather_reg_values Map Register b
sregs, Map (SPointer, RegionSize) b -> Set SStatePart
forall b. Map (SPointer, RegionSize) b -> Set SStatePart
gather_regions Map (SPointer, RegionSize) b
smem, Map (SPointer, RegionSize) b -> Set SStatePart
forall p a. p -> Set a
gather_mem_values Map (SPointer, RegionSize) b
smem]
 where
  gather_regs :: Map Register a -> Set SStatePart
gather_regs       Map Register a
regs = [SStatePart] -> Set SStatePart
forall a. Ord a => [a] -> Set a
S.fromList ([SStatePart] -> Set SStatePart) -> [SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ (Register -> SStatePart) -> [Register] -> [SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map Register -> SStatePart
SSP_Reg ([Register] -> [SStatePart]) -> [Register] -> [SStatePart]
forall a b. (a -> b) -> a -> b
$ Map Register a -> [Register]
forall k a. Map k a -> [k]
M.keys Map Register a
regs 
  gather_reg_values :: p -> Set a
gather_reg_values p
regs = Set a
forall a. Set a
S.empty -- TODO
  gather_regions :: Map (SPointer, RegionSize) b -> Set SStatePart
gather_regions    Map (SPointer, RegionSize) b
mem  = [SStatePart] -> Set SStatePart
forall a. Ord a => [a] -> Set a
S.fromList ([SStatePart] -> Set SStatePart) -> [SStatePart] -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ [Maybe SStatePart] -> [SStatePart]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SStatePart] -> [SStatePart])
-> [Maybe SStatePart] -> [SStatePart]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), b) -> Maybe SStatePart)
-> [((SPointer, RegionSize), b)] -> [Maybe SStatePart]
forall a b. (a -> b) -> [a] -> [b]
map ((SPointer, RegionSize), b) -> Maybe SStatePart
forall b. ((SPointer, RegionSize), b) -> Maybe SStatePart
mk_mem_region ([((SPointer, RegionSize), b)] -> [Maybe SStatePart])
-> [((SPointer, RegionSize), b)] -> [Maybe SStatePart]
forall a b. (a -> b) -> a -> b
$ Map (SPointer, RegionSize) b -> [((SPointer, RegionSize), b)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (SPointer, RegionSize) b
mem
  gather_mem_values :: p -> Set a
gather_mem_values p
mem  = Set a
forall a. Set a
S.empty -- TODO

  mk_mem_region :: ((SPointer, RegionSize), b) -> Maybe SStatePart
mk_mem_region ((SPointer
a,Nat Word64
si),b
_)
    | SPointer -> Bool
has_unknown_offset SPointer
a = Maybe SStatePart
forall a. Maybe a
Nothing
    | Bool
otherwise            = SStatePart -> Maybe SStatePart
forall a. a -> Maybe a
Just (SStatePart -> Maybe SStatePart) -> SStatePart -> Maybe SStatePart
forall a b. (a -> b) -> a -> b
$ SPointer -> Int -> SStatePart
SSP_Mem SPointer
a (Int -> SStatePart) -> Int -> SStatePart
forall a b. (a -> b) -> a -> b
$ Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
si
  mk_mem_region ((SPointer, RegionSize), b)
_ = Maybe SStatePart
forall a. Maybe a
Nothing





mapMaybeS :: Ord b => (a -> Maybe b) -> S.Set a -> S.Set b
mapMaybeS :: (a -> Maybe b) -> Set a -> Set b
mapMaybeS a -> Maybe b
f = (Maybe b -> b) -> Set (Maybe b) -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Set (Maybe b) -> Set b)
-> (Set a -> Set (Maybe b)) -> Set a -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe b -> Bool) -> Set (Maybe b) -> Set (Maybe b)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Maybe b -> Maybe b -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe b
forall a. Maybe a
Nothing) (Set (Maybe b) -> Set (Maybe b))
-> (Set a -> Set (Maybe b)) -> Set a -> Set (Maybe b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> Set a -> Set (Maybe b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map a -> Maybe b
f

mapMaybeNES :: Ord b => (a -> Maybe b) -> NES.NESet a -> S.Set b
mapMaybeNES :: (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES a -> Maybe b
f = (Maybe b -> b) -> Set (Maybe b) -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Set (Maybe b) -> Set b)
-> (NESet a -> Set (Maybe b)) -> NESet a -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe b -> Bool) -> NESet (Maybe b) -> Set (Maybe b)
forall a. (a -> Bool) -> NESet a -> Set a
NES.filter (Maybe b -> Maybe b -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe b
forall a. Maybe a
Nothing) (NESet (Maybe b) -> Set (Maybe b))
-> (NESet a -> NESet (Maybe b)) -> NESet a -> Set (Maybe b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> NESet a -> NESet (Maybe b)
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map a -> Maybe b
f

-- | Convert the current invariant into a function initialisation
invariant_to_finit :: FContext -> Predicate -> FInit
---invariant_to_finit fctxt p | trace ("invariant_to_finit: "++ show p) False = error "trace"
invariant_to_finit :: FContext -> Sstate SValue SPointer -> FInit
invariant_to_finit FContext
fctxt Sstate SValue SPointer
p = 
  let sps :: Set (SStatePart, SValue, Set SPointer)
sps   = (SStatePart -> Maybe (SStatePart, SValue, Set SPointer))
-> Set SStatePart -> Set (SStatePart, SValue, Set SPointer)
forall b a. Ord b => (a -> Maybe b) -> Set a -> Set b
mapMaybeS SStatePart -> Maybe (SStatePart, SValue, Set SPointer)
maybe_read_sp (Set SStatePart -> Set (SStatePart, SValue, Set SPointer))
-> Set SStatePart -> Set (SStatePart, SValue, Set SPointer)
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> Set SStatePart
forall b. Sstate b SPointer -> Set SStatePart
get_stateparts_of_sstate Sstate SValue SPointer
p
      pairs :: [((SStatePart, SValue, Set SPointer),
  (SStatePart, SValue, Set SPointer))]
pairs = Set
  ((SStatePart, SValue, Set SPointer),
   (SStatePart, SValue, Set SPointer))
-> [((SStatePart, SValue, Set SPointer),
     (SStatePart, SValue, Set SPointer))]
forall a. Set a -> [a]
S.toList (Set
   ((SStatePart, SValue, Set SPointer),
    (SStatePart, SValue, Set SPointer))
 -> [((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))])
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
-> [((SStatePart, SValue, Set SPointer),
     (SStatePart, SValue, Set SPointer))]
forall a b. (a -> b) -> a -> b
$ (((SStatePart, SValue, Set SPointer),
  (SStatePart, SValue, Set SPointer))
 -> Bool)
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
forall a. (a -> Bool) -> Set a -> Set a
S.filter (\((SStatePart, SValue, Set SPointer)
x,(SStatePart, SValue, Set SPointer)
y) -> (SStatePart, SValue, Set SPointer)
x (SStatePart, SValue, Set SPointer)
-> (SStatePart, SValue, Set SPointer) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SStatePart, SValue, Set SPointer)
y) (Set
   ((SStatePart, SValue, Set SPointer),
    (SStatePart, SValue, Set SPointer))
 -> Set
      ((SStatePart, SValue, Set SPointer),
       (SStatePart, SValue, Set SPointer)))
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
forall a b. (a -> b) -> a -> b
$ Set (SStatePart, SValue, Set SPointer)
-> Set (SStatePart, SValue, Set SPointer)
-> Set
     ((SStatePart, SValue, Set SPointer),
      (SStatePart, SValue, Set SPointer))
forall a b. Set a -> Set b -> Set (a, b)
S.cartesianProduct Set (SStatePart, SValue, Set SPointer)
sps Set (SStatePart, SValue, Set SPointer)
sps
      finit :: FInit
finit = Set (StatePart, Maybe SValue)
-> Map (SStatePart, SStatePart) MemRelation -> FInit
FInit (((SStatePart, SValue, Set SPointer) -> (StatePart, Maybe SValue))
-> Set (SStatePart, SValue, Set SPointer)
-> Set (StatePart, Maybe SValue)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (SStatePart, SValue, Set SPointer) -> (StatePart, Maybe SValue)
forall c. (SStatePart, SValue, c) -> (StatePart, Maybe SValue)
keep_globals Set (SStatePart, SValue, Set SPointer)
sps) ([((SStatePart, SStatePart), MemRelation)]
-> Map (SStatePart, SStatePart) MemRelation
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((SStatePart, SStatePart), MemRelation)]
 -> Map (SStatePart, SStatePart) MemRelation)
-> [((SStatePart, SStatePart), MemRelation)]
-> Map (SStatePart, SStatePart) MemRelation
forall a b. (a -> b) -> a -> b
$ (((SStatePart, SValue, Set SPointer),
  (SStatePart, SValue, Set SPointer))
 -> ((SStatePart, SStatePart), MemRelation))
-> [((SStatePart, SValue, Set SPointer),
     (SStatePart, SValue, Set SPointer))]
-> [((SStatePart, SStatePart), MemRelation)]
forall a b. (a -> b) -> [a] -> [b]
map ((SStatePart, SValue, Set SPointer),
 (SStatePart, SValue, Set SPointer))
-> ((SStatePart, SStatePart), MemRelation)
forall (t :: * -> *) (t :: * -> *) a b b b.
(Foldable t, Foldable t) =>
((a, b, t SPointer), (b, b, t SPointer)) -> ((a, b), MemRelation)
mk_memrel [((SStatePart, SValue, Set SPointer),
  (SStatePart, SValue, Set SPointer))]
pairs) in
    FInit
finit -- trace ("Turning into finit, precondition: \n" ++ show p ++ "\n-->\n" ++ show finit) finit 
 where
  keep_globals :: (SStatePart, SValue, c) -> (StatePart, Maybe SValue)
keep_globals (SStatePart
sp,SValue
v,c
_) 
    | SValue -> Bool
is_global_value SValue
v = (SStatePart -> StatePart
mk_sp SStatePart
sp,SValue -> Maybe SValue
forall a. a -> Maybe a
Just SValue
v)
    | Bool
otherwise         = (SStatePart -> StatePart
mk_sp SStatePart
sp,Maybe SValue
forall a. Maybe a
Nothing)

  maybe_read_sp :: SStatePart -> Maybe (SStatePart, SValue, Set SPointer)
maybe_read_sp SStatePart
sp
    | SStatePart -> Bool
suitable_sp SStatePart
sp =
      case State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt SStatePart
sp) Sstate SValue SPointer
p of
        SValue
Top -> Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
        SAddends NESet (NESet SAddend)
es -> Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing -- TODO!!!
        SConcrete NESet SimpleExpr
es -> 
          let es' :: Set SimpleExpr
es'  = (SimpleExpr -> Bool) -> NESet SimpleExpr -> Set SimpleExpr
forall a. (a -> Bool) -> NESet a -> Set a
NES.filter (\SimpleExpr
e -> FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True SimpleExpr
e Maybe SPointer -> Maybe SPointer -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe SPointer
forall a. Maybe a
Nothing) NESet SimpleExpr
es
              ptrs :: Set SPointer
ptrs = (SimpleExpr -> SPointer) -> Set SimpleExpr -> Set SPointer
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Maybe SPointer -> SPointer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SPointer -> SPointer)
-> (SimpleExpr -> Maybe SPointer) -> SimpleExpr -> SPointer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True) Set SimpleExpr
es' in
            if Set SPointer -> Bool
forall a. Set a -> Bool
S.null Set SPointer
ptrs then
              Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing
            else
              (SStatePart, SValue, Set SPointer)
-> Maybe (SStatePart, SValue, Set SPointer)
forall a. a -> Maybe a
Just (SStatePart
sp,FContext -> [Char] -> NESet SimpleExpr -> SValue
mk_concrete FContext
fctxt [Char]
"finit" (NESet SimpleExpr -> SValue) -> NESet SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Set SimpleExpr -> NESet SimpleExpr
forall a. Set a -> NESet a
NES.unsafeFromSet Set SimpleExpr
es',Set SPointer
ptrs)
    | Bool
otherwise = Maybe (SStatePart, SValue, Set SPointer)
forall a. Maybe a
Nothing

  suitable_sp :: SStatePart -> Bool
suitable_sp (SSP_Reg Register
r)    = Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Register
RIP,Register
RSP,Register
RBP]
  suitable_sp (SSP_Mem SPointer
a Int
si) = SPointer -> Bool
is_global_ptr SPointer
a Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ SPointer -> SimpleExpr
spointer_to_expr SPointer
a)


  mk_memrel :: ((a, b, t SPointer), (b, b, t SPointer)) -> ((a, b), MemRelation)
mk_memrel ((a
sp0,b
v0,t SPointer
ptrs0),(b
sp1,b
v1,t SPointer
ptrs1))
    | (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr0 -> (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr1 -> FContext
-> [Char]
-> SPointer
-> RegionSize
-> SPointer
-> RegionSize
-> Bool
cseparate FContext
fctxt [Char]
"invariant_to_finit" SPointer
ptr0 RegionSize
UnknownSize SPointer
ptr1 RegionSize
UnknownSize) t SPointer
ptrs1) t SPointer
ptrs0 = ((a
sp0,b
sp1),MemRelation
Separate)
    | (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr0 -> (SPointer -> Bool) -> t SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SPointer
ptr1 -> FContext
-> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
forall p.
p -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool
calias FContext
fctxt SPointer
ptr0 RegionSize
UnknownSize SPointer
ptr1 RegionSize
UnknownSize) t SPointer
ptrs1) t SPointer
ptrs0 = ((a
sp0,b
sp1),MemRelation
Aliassing)
    | Bool
otherwise = ((a
sp0,b
sp1),MemRelation
Unknown) -- TODO

  is_global_value :: SValue -> Bool
is_global_value (SConcrete NESet SimpleExpr
es) = (SPointer -> Bool) -> Set SPointer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SPointer -> Bool
is_global_ptr (Set SPointer -> Bool) -> Set SPointer -> Bool
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Maybe SPointer) -> NESet SimpleExpr -> Set SPointer
forall b a. Ord b => (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES (FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
True) NESet SimpleExpr
es

  is_global_ptr :: SPointer -> Bool
is_global_ptr (Base_Immediate Word64
_ PtrOffset
_)   = Bool
True
  is_global_ptr SPointer
_                    = Bool
False

  mk_sp :: SStatePart -> StatePart
mk_sp (SSP_Reg Register
r)    = Register -> StatePart
SP_Reg Register
r
  mk_sp (SSP_Mem SPointer
a Int
si) = SimpleExpr -> Int -> StatePart
SP_Mem (SPointer -> SimpleExpr
spointer_to_expr SPointer
a) Int
si





-- | The join between two function initialisations
join_finit :: FContext -> FInit -> FInit -> FInit
join_finit :: FContext -> FInit -> FInit -> FInit
join_finit FContext
fctxt f0 :: FInit
f0@(FInit Set (StatePart, Maybe SValue)
sps0 Map (SStatePart, SStatePart) MemRelation
m0) f1 :: FInit
f1@(FInit Set (StatePart, Maybe SValue)
sps1 Map (SStatePart, SStatePart) MemRelation
m1)
  | FInit
f0 FInit -> FInit -> Bool
forall a. Eq a => a -> a -> Bool
== FInit
f1 = FInit
f0
  | Bool
otherwise = Set (StatePart, Maybe SValue)
-> Map (SStatePart, SStatePart) MemRelation -> FInit
FInit (Set (StatePart, Maybe SValue)
-> Set (StatePart, Maybe SValue) -> Set (StatePart, Maybe SValue)
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set (StatePart, Maybe SValue)
sps0 Set (StatePart, Maybe SValue)
sps1) ((MemRelation -> MemRelation -> MemRelation)
-> Map (SStatePart, SStatePart) MemRelation
-> Map (SStatePart, SStatePart) MemRelation
-> Map (SStatePart, SStatePart) MemRelation
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith MemRelation -> MemRelation -> MemRelation
join_rel Map (SStatePart, SStatePart) MemRelation
m0 Map (SStatePart, SStatePart) MemRelation
m1)
 where
  join_rel :: MemRelation -> MemRelation -> MemRelation
join_rel MemRelation
r0 MemRelation
r1
    | MemRelation
r0 MemRelation -> MemRelation -> Bool
forall a. Eq a => a -> a -> Bool
== MemRelation
r1  = MemRelation
r0
    | Bool
otherwise = MemRelation
Unknown





















data ExternalFunctionOutput = FreshPointer | UnknownReturnValue | Input Register

data ExternalFunctionBehavior = ExternalFunctionBehavior {
  ExternalFunctionBehavior -> [Register]
f_inputs :: [Register],
  ExternalFunctionBehavior -> ExternalFunctionOutput
f_output :: ExternalFunctionOutput
 }


param :: a -> Register
param a
0 = Register
RDI 
param a
1 = Register
RSI
param a
2 = Register
RDX
param a
3 = Register
RCX
param a
4 = Register
R8
param a
5 = Register
R9


pure_and_fresh :: ExternalFunctionBehavior
pure_and_fresh = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
FreshPointer
pure_and_unknown :: ExternalFunctionBehavior
pure_and_unknown = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
UnknownReturnValue

external_function_behavior :: FContext -> String -> ExternalFunctionBehavior
-- | a list of some function that return a heap-pointer through RAX.
-- The pointer is assumed to  be fresh.
external_function_behavior :: FContext -> [Char] -> ExternalFunctionBehavior
external_function_behavior FContext
_ [Char]
"_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_create_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_default_zone" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_zone_malloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_malloc_zone_calloc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_mmap" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_av_mallocz" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"___error" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"localeconv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strerror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strerror_r" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__wcserror" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_EVP_CIPHER_CTX_new" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_strdup" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"getenv" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_open" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fts_read$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fts_open$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_opendir$INODE64" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wfdopen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"fgetln" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_wsetlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_b_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"dcgettext" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"nl_langinfo" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"setlocale" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__errno_location" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"_popen" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_tolower_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"__ctype_toupper_loc" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"readdir" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"getmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"setmntent" = ExternalFunctionBehavior
pure_and_fresh
external_function_behavior FContext
_ [Char]
"hasmntopt" = ExternalFunctionBehavior
pure_and_fresh
-- | 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 FContext
_ [Char]
"feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_feof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"getc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgetc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fgetwc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fnmatch" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fputc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"close" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fwrite" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"___maskrune" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getbsize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"printf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"vprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"vfprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fwprintf" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fwprintf_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__fprintf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__printf_chk" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_putchar" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_puts" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fputs" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"btowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_mbtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"mbrtowc" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"atof" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strncmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strlen" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_ilogb" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_atoi" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_getopt" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"getopt_long" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_warn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_warnx" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__errno_location" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__libc_start_main" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__cxa_finalize" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"perror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"free" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"unlink" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"unlinkat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"utimensat" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fdatasync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fsync" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"isatty" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"strcspn" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_memcmp" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"isprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"iswprint" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_isprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_iswprint_l" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"__cxa_atexit" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"towlower" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"towupper" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"iswalnum" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fseeko" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"fflush" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fclose" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_fgets" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_ferror" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strtol" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_strtoul" = ExternalFunctionBehavior
pure_and_unknown
external_function_behavior FContext
_ [Char]
"_munmap" = ExternalFunctionBehavior
pure_and_unknown



-- | 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 FContext
_ [Char]
"snprintf"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snprintf"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snprintf_l"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snwprintf"           = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_snwprintf_l"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"__snprintf_chk"       = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_vsnprintf"           = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sprintf"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"_sprintf"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"___bzero"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigprocmask"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"__strcat_chk"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"strcat"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"strlcpy"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"___strlcpy_chk"       = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigemptyset"          = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"sigaction"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
2] ExternalFunctionOutput
UnknownReturnValue
external_function_behavior FContext
_ [Char]
"localtime"            = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] ExternalFunctionOutput
FreshPointer
external_function_behavior FContext
_ [Char]
"memset"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memset"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memset_chk"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"___memset_chk"        = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_index"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_rindex"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0

-- A list of functions that return a pointer given to them by a parameter
external_function_behavior FContext
_ [Char]
"_realloc"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_malloc_zone_realloc" = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_recallocarray"       = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"realloc"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strcpy"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__strcpy_chk"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strncpy"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strcpy"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strncpy"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"stpcpy"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memcpy"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memcpy"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memcpy_chk"         = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"___memcpy_chk"        = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"__memmove_chk"        = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memmove"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memmove"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strcat"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strcat"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strchr"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strchr"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strrchr"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strrchr"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_memchr"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"memchr"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strstr"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strstr"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strpbrk"             = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strtok"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"strtok"               = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0
external_function_behavior FContext
_ [Char]
"_strlen"              = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] (ExternalFunctionOutput -> ExternalFunctionBehavior)
-> ExternalFunctionOutput -> ExternalFunctionBehavior
forall a b. (a -> b) -> a -> b
$ Register -> ExternalFunctionOutput
Input (Register -> ExternalFunctionOutput)
-> Register -> ExternalFunctionOutput
forall a b. (a -> b) -> a -> b
$ Integer -> Register
forall a. (Eq a, Num a) => a -> Register
param Integer
0


external_function_behavior FContext
fctxt [Char]
f
 | [Char] -> Bool
is_exiting_function_call [Char]
f = ExternalFunctionBehavior
pure_and_unknown
 | Bool
otherwise                  = [Register] -> ExternalFunctionOutput -> ExternalFunctionBehavior
ExternalFunctionBehavior [] ExternalFunctionOutput
UnknownReturnValue -- 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_offset :: FContext -> PtrOffset -> SPointer -> SPointer
transpose_bw_offset :: FContext -> PtrOffset -> SPointer -> SPointer
transpose_bw_offset FContext
fctxt (PtrOffset Word64
off) SPointer
v
  | SPointer -> Bool
has_unknown_offset SPointer
v = SPointer
v
  | Bool
otherwise            = (Word64 -> Word64) -> SPointer -> SPointer
mod_offset (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) Word64
off) SPointer
v
transpose_bw_offset FContext
fctxt PtrOffset
UnknownOffset SPointer
v   = FContext -> [Char] -> SPointer -> SPointer
forall p. p -> [Char] -> SPointer -> SPointer
set_unknown_offset FContext
fctxt [Char]
"transpose_bw_offset" SPointer
v

transpose_bw_spointer :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> SPointer -> Maybe SPointer
transpose_bw_spointer :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SPointer
-> Maybe SPointer
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_StackPointer [Char]
f PtrOffset
offset)   = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show (SPointer
b)-- transpose_bw_offset fctxt offset $ evalSstate (read_sp fctxt (SSP_Reg RSP)) p
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_Immediate Word64
a PtrOffset
offset)      = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_Malloc Maybe Word64
_ Maybe [Char]
_ PtrOffset
offset)       = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_FunctionPtr Word64
_ [Char]
_ PtrOffset
offset)  = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_ReturnAddr [Char]
_)            = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of return address"
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_TLS PtrOffset
offset)              = [Char] -> Maybe SPointer
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe SPointer) -> [Char] -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of TLS"
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_FunctionReturn [Char]
f PtrOffset
offset) = SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just SPointer
b
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q b :: SPointer
b@(Base_StatePart StatePart
sp PtrOffset
offset)     =
  let ptrs :: Set SPointer
ptrs = FContext -> [Char] -> SValue -> Set SPointer
cmk_mem_addresses FContext
fctxt ([Char]
"transpose_bw_spointer\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sstate SValue SPointer -> [Char]
forall a. Show a => a -> [Char]
show Sstate SValue SPointer
p [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sstate SValue SPointer -> [Char]
forall a. Show a => a -> [Char]
show Sstate SValue SPointer
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\nb = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SPointer -> [Char]
forall a. Show a => a -> [Char]
show SPointer
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\ne = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SValue -> [Char]
forall a. Show a => a -> [Char]
show (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp))) (SValue -> Set SPointer) -> SValue -> Set SPointer
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp) in
     if Set SPointer -> Int
forall a. Set a -> Int
S.size Set SPointer
ptrs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
      SPointer -> Maybe SPointer
forall a. a -> Maybe a
Just (SPointer -> Maybe SPointer) -> SPointer -> Maybe SPointer
forall a b. (a -> b) -> a -> b
$ Set SPointer -> SPointer
forall a. Set a -> a
S.findMin Set SPointer
ptrs
    else
      Maybe SPointer
forall a. Maybe a
Nothing 

transpose_bw_addend :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> NES.NESet SAddend -> SValue
transpose_bw_addend :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> NESet SAddend
-> SValue
transpose_bw_addend FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q NESet SAddend
ptrs = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"transpose_bw_addend" (SValue -> SValue) -> SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SValue -> SValue -> SValue) -> NESet SValue -> SValue
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
NES.foldr1 (FContext -> Int -> SValue -> SValue -> SValue
svalue_plus FContext
fctxt Int
64) (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SAddend -> SValue) -> NESet SAddend -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map SAddend -> SValue
transpose_bw_saddend NESet SAddend
ptrs
 where
  transpose_bw_saddend :: SAddend -> SValue
  transpose_bw_saddend :: SAddend -> SValue
transpose_bw_saddend (SAddend_StackPointer [Char]
f)    = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt (Register -> SStatePart
SSP_Reg Register
RSP)) Sstate SValue SPointer
p
  transpose_bw_saddend (SAddend_Immediate Word64
a)       = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
a
  transpose_bw_saddend (SAddend_Malloc Maybe Word64
id Maybe [Char]
hash)    = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
hash
  transpose_bw_saddend (SAddend_FunctionPtr Word64
a [Char]
_)   = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Int -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
a) Int
8
  transpose_bw_saddend (SAddend_ReturnAddr [Char]
_)      = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of return address"
  transpose_bw_saddend (SAddend
SAddend_TLS)               = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> SValue) -> [Char] -> SValue
forall a b. (a -> b) -> a -> b
$ [Char]
"Transposition of TLS"
  transpose_bw_saddend (SAddend_StatePart StatePart
sp)      = FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (StatePart -> SimpleExpr
SE_Var StatePart
sp) 
  transpose_bw_saddend (SAddend_FunctionReturn [Char]
f)  = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> BotTyp
FromCall [Char]
f


transpose_bw_svalue :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> SValue -> SValue
transpose_bw_svalue :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (SConcrete NESet SimpleExpr
es)  = FContext -> [Char] -> NESet SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
"transpose_bw" (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SValue) -> NESet SimpleExpr -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p) NESet SimpleExpr
es
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (SAddends NESet (NESet SAddend)
adds) = FContext -> [Char] -> NESet SValue -> SValue
forall (t :: * -> *).
Foldable t =>
FContext -> [Char] -> t SValue -> SValue
cjoin_all FContext
fctxt [Char]
"transpose_bw" (NESet SValue -> SValue) -> NESet SValue -> SValue
forall a b. (a -> b) -> a -> b
$ (NESet SAddend -> SValue) -> NESet (NESet SAddend) -> NESet SValue
forall b a. Ord b => (a -> b) -> NESet a -> NESet b
NES.map (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> NESet SAddend
-> SValue
transpose_bw_addend FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) NESet (NESet SAddend)
adds
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q t :: SValue
t@SValue
Top           = SValue
t


    
transpose_bw_reg :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> (Register, SValue) -> Maybe (Register, SValue)
transpose_bw_reg :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q (Register
r,SValue
v) =
  let v' :: SValue
v' = FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SValue
v in
    (Register, SValue) -> Maybe (Register, SValue)
forall a. a -> Maybe a
Just ((Register, SValue) -> Maybe (Register, SValue))
-> (Register, SValue) -> Maybe (Register, SValue)
forall a b. (a -> b) -> a -> b
$ (Register
r,SValue
v')

transpose_bw_mem :: FContext -> Sstate SValue SPointer -> Sstate SValue SPointer -> ((SPointer,RegionSize), SValue) -> Maybe ((SPointer,RegionSize), SValue)
transpose_bw_mem :: FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
transpose_bw_mem FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q ((SPointer
a,RegionSize
si),SValue
v) =
  case FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SPointer
-> Maybe SPointer
transpose_bw_spointer FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SPointer
a of
    Just SPointer
a' -> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
forall a. a -> Maybe a
Just ((SPointer
a',RegionSize
si), FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> SValue
-> SValue
transpose_bw_svalue FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q SValue
v)
    Maybe SPointer
Nothing -> Maybe ((SPointer, RegionSize), SValue)
forall a. Maybe a
Nothing




transpose_bw_e :: FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e :: FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (Bottom (FromCall [Char]
f))            = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom ([Char] -> BotTyp
FromCall [Char]
f)
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Malloc Maybe Word64
id Maybe [Char]
hash)              = FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
hash
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Immediate Word64
i)                 = FContext -> Word64 -> SValue
forall i. Integral i => FContext -> i -> SValue
cimmediate FContext
fctxt Word64
i
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_StatePart StatePart
sp)                = [Char] -> SValue
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Var (SP_StackPointer [Char]
f))     = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
RSP) Sstate SValue SPointer
p
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Var StatePart
sp)                      = FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p StatePart
sp
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Bit Int
i SimpleExpr
e)                     = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> SValue -> SymbolicOperation SValue
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
i (SValue -> SymbolicOperation SValue)
-> SValue -> SymbolicOperation SValue
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_SExtend Int
l Int
h SimpleExpr
e)               = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SValue -> SymbolicOperation SValue
forall v. Int -> Int -> v -> SymbolicOperation v
SO_SExtend Int
l Int
h (SValue -> SymbolicOperation SValue)
-> SValue -> SymbolicOperation SValue
forall a b. (a -> b) -> a -> b
$ FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
e
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
Plus Int
si [SimpleExpr
a,SimpleExpr
b])            = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Opcode -> Int -> Maybe Int -> [SValue] -> SymbolicOperation SValue
forall v. Opcode -> Int -> Maybe Int -> [v] -> SymbolicOperation v
SO_Op Opcode
ADD (Int
si Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Maybe Int
forall a. Maybe a
Nothing [FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a,FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
Minus Int
si [SimpleExpr
a,SimpleExpr
b])           = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Opcode -> Int -> Maybe Int -> [SValue] -> SymbolicOperation SValue
forall v. Opcode -> Int -> Maybe Int -> [v] -> SymbolicOperation v
SO_Op Opcode
SUB (Int
si Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Maybe Int
forall a. Maybe a
Nothing [FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a,FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b]
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Op Operator
op Int
si [SimpleExpr]
es)                 = FContext
-> [Char] -> ([SimpleExpr] -> SimpleExpr) -> [SValue] -> SValue
apply_expr_op FContext
fctxt [Char]
"transpose_bw" (FContext -> SimpleExpr -> SimpleExpr
mk_expr FContext
fctxt (SimpleExpr -> SimpleExpr)
-> ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Operator -> Int -> [SimpleExpr] -> SimpleExpr
SE_Op Operator
op Int
si) ([SValue] -> SValue) -> [SValue] -> SValue
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> SValue) -> [SimpleExpr] -> [SValue]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p) [SimpleExpr]
es
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p (SE_Overwrite Int
i SimpleExpr
a SimpleExpr
b)             = FContext -> [Char] -> SymbolicOperation SValue -> SValue
csemantics FContext
fctxt [Char]
"transpose_bw" (SymbolicOperation SValue -> SValue)
-> SymbolicOperation SValue -> SValue
forall a b. (a -> b) -> a -> b
$ Int -> SValue -> SValue -> SymbolicOperation SValue
forall v. Int -> v -> v -> SymbolicOperation v
SO_Overwrite Int
i (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a) (FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
b)

transpose_bw_sp :: FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp :: FContext -> Sstate SValue SPointer -> StatePart -> SValue
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p (SP_Reg Register
r)    = State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r) Sstate SValue SPointer
p
transpose_bw_sp FContext
fctxt Sstate SValue SPointer
p (SP_Mem SimpleExpr
a Int
si) = 
  let a' :: SValue
a' = FContext -> Sstate SValue SPointer -> SimpleExpr -> SValue
transpose_bw_e FContext
fctxt Sstate SValue SPointer
p SimpleExpr
a in
    State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (FContext
-> [Char]
-> SValue
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> v -> RegionSize -> State (Sstate v p, VCS) v
sread_mem FContext
fctxt [Char]
"transpose_bw_sp" SValue
a' (RegionSize -> State (Sstate SValue SPointer, VCS) SValue)
-> RegionSize -> State (Sstate SValue SPointer, VCS) SValue
forall a b. (a -> b) -> a -> b
$ Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si) Sstate SValue SPointer
p


read_sp :: FContext -> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp :: FContext
-> SStatePart -> State (Sstate SValue SPointer, VCS) SValue
read_sp FContext
fctxt (SSP_Reg Register
r)    = FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r
read_sp FContext
fctxt (SSP_Mem SPointer
a Int
si) = FContext
-> [Char]
-> SPointer
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> p -> RegionSize -> State (Sstate v p, VCS) v
sread_mem_from_ptr FContext
fctxt [Char]
"read_sp" SPointer
a (RegionSize -> State (Sstate SValue SPointer, VCS) SValue)
-> RegionSize -> State (Sstate SValue SPointer, VCS) SValue
forall a b. (a -> b) -> a -> b
$ (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si)

write_sp :: FContext -> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp :: FContext
-> SStatePart -> SValue -> State (Sstate SValue SPointer, VCS) ()
write_sp FContext
fctxt (SSP_Reg Register
r)    SValue
v = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
r SValue
v
write_sp FContext
fctxt (SSP_Mem SPointer
a Int
si) SValue
v = FContext
-> Bool
-> SPointer
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem_to_ptr FContext
fctxt Bool
True SPointer
a (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si) SValue
v


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

get_function_type :: FContext -> Instruction -> [Char] -> FunctionType
get_function_type FContext
fctxt Instruction
i [Char]
f_callee =
  [Maybe FReturnBehavior] -> FunctionType
ftype ([Maybe FReturnBehavior] -> FunctionType)
-> [Maybe FReturnBehavior] -> FunctionType
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> Maybe FReturnBehavior)
-> [ResolvedJumpTarget] -> [Maybe FReturnBehavior]
forall a b. (a -> b) -> [a] -> [b]
map ResolvedJumpTarget -> Maybe FReturnBehavior
postcondition_of_jump_target ([ResolvedJumpTarget] -> [Maybe FReturnBehavior])
-> [ResolvedJumpTarget] -> [Maybe FReturnBehavior]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i
 where
  ftype :: [Maybe FReturnBehavior] -> FunctionType
ftype [Maybe FReturnBehavior]
posts
    | (Maybe FReturnBehavior -> Bool) -> [Maybe FReturnBehavior] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe FReturnBehavior -> Maybe FReturnBehavior -> Bool
forall a. Eq a => a -> a -> Bool
(==) (FReturnBehavior -> Maybe FReturnBehavior
forall a. a -> Maybe a
Just FReturnBehavior
Terminating)) [Maybe FReturnBehavior]
posts                                = FunctionType
AnalyzedInternalFunctionTerminates
    | (Maybe FReturnBehavior -> Bool) -> [Maybe FReturnBehavior] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe FReturnBehavior -> Bool
is_returning [Maybe FReturnBehavior]
posts                                             = Sstate SValue SPointer -> FunctionType
AnalyzedInternalFunction (Sstate SValue SPointer -> FunctionType)
-> Sstate SValue SPointer -> FunctionType
forall a b. (a -> b) -> a -> b
$ FContext -> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Sstate v p] -> Sstate v p
supremum FContext
fctxt ([Sstate SValue SPointer] -> Sstate SValue SPointer)
-> [Sstate SValue SPointer] -> Sstate SValue SPointer
forall a b. (a -> b) -> a -> b
$ (Maybe FReturnBehavior -> Sstate SValue SPointer)
-> [Maybe FReturnBehavior] -> [Sstate SValue SPointer]
forall a b. (a -> b) -> [a] -> [b]
map Maybe FReturnBehavior -> Sstate SValue SPointer
fromReturning [Maybe FReturnBehavior]
posts
    | [Char]
"0x" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
f_callee Bool -> Bool -> Bool
|| [Char]
"indirection@" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
f_callee = FunctionType
AnalyzedInternalFunctionUnknown
    | Bool
otherwise                                                          = FunctionType
ExternalFunction

  fromReturning :: Maybe FReturnBehavior -> Sstate SValue SPointer
fromReturning (Just (ReturningWith Sstate SValue SPointer
q)) = Sstate SValue SPointer
q
  is_returning :: Maybe FReturnBehavior -> Bool
is_returning  (Just (ReturningWith Sstate SValue SPointer
q)) = Bool
True
  is_returning  Maybe FReturnBehavior
_                        = Bool
False

  postcondition_of_jump_target :: ResolvedJumpTarget -> Maybe FReturnBehavior
postcondition_of_jump_target (ImmediateAddress Word64
a) = Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) (Context -> IntMap FReturnBehavior
ctxt_calls (Context -> IntMap FReturnBehavior)
-> Context -> IntMap FReturnBehavior
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt)
  postcondition_of_jump_target ResolvedJumpTarget
_                    = Maybe FReturnBehavior
forall a. Maybe a
Nothing



-- | Executes semantics for external functions.
call :: FContext -> Bool -> X86.Instruction -> State (Sstate SValue SPointer,VCS) ()
call :: FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call FContext
fctxt Bool
is_jump Instruction
i = do
  case FContext -> Instruction -> [Char] -> FunctionType
get_function_type FContext
fctxt Instruction
i [Char]
f_callee of
    FunctionType
AnalyzedInternalFunctionUnknown    -> FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall p p. p -> p -> State (Sstate SValue SPointer, VCS) ()
unknown_internal_function FContext
fctxt Instruction
i
    FunctionType
AnalyzedInternalFunctionTerminates -> State (Sstate SValue SPointer, VCS) ()
incr_rsp
    AnalyzedInternalFunction Sstate SValue SPointer
q         -> Sstate SValue SPointer -> State (Sstate SValue SPointer, VCS) ()
internal_function Sstate SValue SPointer
q
    FunctionType
ExternalFunction                   -> State (Sstate SValue SPointer, VCS) ()
external_function 
 where
  external_function :: State (Sstate SValue SPointer, VCS) ()
external_function = case FContext -> [Char] -> ExternalFunctionBehavior
external_function_behavior FContext
fctxt [Char]
f_callee of
    ExternalFunctionBehavior [Register]
params ExternalFunctionOutput
output -> {--mapM_ write_param params >> --} ExternalFunctionOutput -> State (Sstate SValue SPointer, VCS) ()
write_output ExternalFunctionOutput
output State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State (Sstate SValue SPointer, VCS) ()
incr_rsp-- writing to params really roughly overapproximates

  write_output :: ExternalFunctionOutput -> State (Sstate SValue SPointer,VCS) ()
  write_output :: ExternalFunctionOutput -> State (Sstate SValue SPointer, VCS) ()
write_output ExternalFunctionOutput
FreshPointer       = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX (SValue -> State (Sstate SValue SPointer, VCS) ())
-> SValue -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i)) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
""))
  write_output ExternalFunctionOutput
UnknownReturnValue = FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX (SValue -> State (Sstate SValue SPointer, VCS) ())
-> SValue -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ (FContext -> SimpleExpr -> SValue
mk_concreteS FContext
fctxt (SimpleExpr -> SValue) -> SimpleExpr -> SValue
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom ([Char] -> BotTyp
FromCall [Char]
f_callee))
  write_output (Input Register
r)          = FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r State (Sstate SValue SPointer, VCS) SValue
-> (SValue -> State (Sstate SValue SPointer, VCS) ())
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
RAX

  incr_rsp :: State (Sstate SValue SPointer, VCS) ()
incr_rsp
    | Bool
is_jump   = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
ADD Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing)
    | Bool
otherwise = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  decr_rsp :: State (Sstate SValue SPointer, VCS) ()
decr_rsp
    | Bool -> Bool
not Bool
is_jump  = FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
SUB Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing)
    | Bool
otherwise    = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

    (Sstate SValue SPointer
p,VCS
vcs) <- StateT
  (Sstate SValue SPointer, VCS)
  Identity
  (Sstate SValue SPointer, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
    -- 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 (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> (Register, SValue)
-> Maybe (Register, SValue)
transpose_bw_reg FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) ([(Register, SValue)] -> [Maybe (Register, SValue)])
-> [(Register, SValue)] -> [Maybe (Register, SValue)]
forall a b. (a -> b) -> a -> b
$ ((Register, SValue) -> Bool)
-> [(Register, SValue)] -> [(Register, SValue)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Register
RIP (Register -> Bool)
-> ((Register, SValue) -> Register) -> (Register, SValue) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Register, SValue) -> Register
forall a b. (a, b) -> a
fst) ([(Register, SValue)] -> [(Register, SValue)])
-> [(Register, SValue)] -> [(Register, SValue)]
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> [(Register, SValue)]
forall a p. Sstate a p -> [(Register, a)]
sstate_to_reg_eqs Sstate SValue SPointer
q
    let q_eqs_transposed_mem :: [((SPointer, RegionSize), SValue)]
q_eqs_transposed_mem   = [Maybe ((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ((SPointer, RegionSize), SValue)]
 -> [((SPointer, RegionSize), SValue)])
-> [Maybe ((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), SValue)
 -> Maybe ((SPointer, RegionSize), SValue))
-> [((SPointer, RegionSize), SValue)]
-> [Maybe ((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> [a] -> [b]
map (FContext
-> Sstate SValue SPointer
-> Sstate SValue SPointer
-> ((SPointer, RegionSize), SValue)
-> Maybe ((SPointer, RegionSize), SValue)
transpose_bw_mem FContext
fctxt Sstate SValue SPointer
p Sstate SValue SPointer
q) ([((SPointer, RegionSize), SValue)]
 -> [Maybe ((SPointer, RegionSize), SValue)])
-> [((SPointer, RegionSize), SValue)]
-> [Maybe ((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ (((SPointer, RegionSize), SValue) -> Bool)
-> [((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SPointer, RegionSize), SValue) -> Bool
do_transfer ([((SPointer, RegionSize), SValue)]
 -> [((SPointer, RegionSize), SValue)])
-> [((SPointer, RegionSize), SValue)]
-> [((SPointer, RegionSize), SValue)]
forall a b. (a -> b) -> a -> b
$ Sstate SValue SPointer -> [((SPointer, RegionSize), SValue)]
forall a p. Sstate a p -> [((p, RegionSize), a)]
sstate_to_mem_eqs Sstate SValue SPointer
q
    -- write transposed postcondition to current state
    (((SPointer, RegionSize), SValue)
 -> State (Sstate SValue SPointer, VCS) ())
-> [((SPointer, RegionSize), SValue)]
-> State (Sstate SValue SPointer, VCS) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\((SPointer
a,RegionSize
si),SValue
v) -> FContext
-> Bool
-> SPointer
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem_to_ptr FContext
fctxt Bool
True SPointer
a RegionSize
si SValue
v) ([((SPointer, RegionSize), SValue)]
 -> State (Sstate SValue SPointer, VCS) ())
-> [((SPointer, RegionSize), SValue)]
-> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ [((SPointer, RegionSize), SValue)]
q_eqs_transposed_mem 
    ((Register, SValue) -> State (Sstate SValue SPointer, VCS) ())
-> [(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Register
r,SValue
v) -> FContext
-> Register -> SValue -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> v -> State (Sstate v p, VCS) ()
swrite_reg FContext
fctxt Register
r SValue
v) ([(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ())
-> [(Register, SValue)] -> State (Sstate SValue SPointer, VCS) ()
forall a b. (a -> b) -> a -> b
$ [(Register, SValue)]
q_eqs_transposed_regs


  -- 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) ()
  write_param :: Register -> State (Sstate SValue SPointer, VCS) ()
write_param Register
r = do
    SValue
a      <- FContext -> Register -> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS) v
sread_reg FContext
fctxt Register
r
    let a' :: SValue
a'  = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"write_param" SValue
a
    SValue
v'     <- ((Sstate SValue SPointer, VCS) -> SValue)
-> State (Sstate SValue SPointer, VCS) SValue
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer -> SValue
forall v p a. State (Sstate v p, VCS) a -> Sstate v p -> a
evalSstate (State (Sstate SValue SPointer, VCS) SValue
 -> Sstate SValue SPointer -> SValue)
-> State (Sstate SValue SPointer, VCS) SValue
-> Sstate SValue SPointer
-> SValue
forall a b. (a -> b) -> a -> b
$ FContext
-> [Char]
-> SValue
-> RegionSize
-> State (Sstate SValue SPointer, VCS) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Char] -> v -> RegionSize -> State (Sstate v p, VCS) v
sread_mem FContext
fctxt [Char]
"write_param" SValue
a RegionSize
UnknownSize) (Sstate SValue SPointer -> SValue)
-> ((Sstate SValue SPointer, VCS) -> Sstate SValue SPointer)
-> (Sstate SValue SPointer, VCS)
-> SValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sstate SValue SPointer, VCS) -> Sstate SValue SPointer
forall a b. (a, b) -> a
fst)
    let bot :: SValue
bot = FContext -> [Char] -> SValue -> SValue
cwiden FContext
fctxt [Char]
"write_param_v" SValue
v'
    FContext
-> Bool
-> SValue
-> RegionSize
-> SValue
-> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p, VCS) ()
swrite_mem FContext
fctxt Bool
True SValue
a' RegionSize
UnknownSize SValue
bot


  do_transfer :: ((SPointer, RegionSize), SValue) -> Bool
do_transfer ((SPointer
a,RegionSize
si),SValue
v) = Bool -> Bool
not ((SPointer, RegionSize) -> SValue -> Bool
is_initial (SPointer
a,RegionSize
si) SValue
v) Bool -> Bool -> Bool
&& Bool -> Bool
not (SPointer -> RegionSize -> Bool
is_top_stackframe SPointer
a RegionSize
si) Bool -> Bool -> Bool
&& Bool -> Bool
not (FContext -> SPointer -> Bool
forall p. p -> SPointer -> Bool
is_local_spointer FContext
fctxt SPointer
a)
  
  is_initial :: (SPointer,RegionSize) -> SValue -> Bool
  is_initial :: (SPointer, RegionSize) -> SValue -> Bool
is_initial (SPointer
a,RegionSize
si) SValue
v = Bool
False {-- "TODO: " ++ show (a,si,v) 
    case (ctry_deterministic a, ctry_immediate si) of
      (Just a', Just si') -> v == cmk_init_mem_value fctxt "is_initial" a si
      _                   -> False--}

  is_top_stackframe :: SPointer -> RegionSize -> Bool
is_top_stackframe (Base_StackPointer [Char]
_ (PtrOffset Word64
0)) (Nat Word64
8) = Bool
True  
  is_top_stackframe SPointer
_ RegionSize
_ = Bool
False

  f_name :: [Char]
f_name  = Context -> Int -> [Char]
function_name_of_entry (FContext -> Context
f_ctxt FContext
fctxt) (FContext -> Int
f_entry FContext
fctxt)
  f_callee :: [Char]
f_callee = Context -> Instruction -> [Char]
function_name_of_instruction (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i

  sstate_to_reg_eqs :: Sstate a p -> [(Register, a)]
sstate_to_reg_eqs (Sstate Map Register a
regs Map (p, RegionSize) a
_ FlagStatus
_) = Map Register a -> [(Register, a)]
forall k a. Map k a -> [(k, a)]
M.toList Map Register a
regs
  sstate_to_mem_eqs :: Sstate a p -> [((p, RegionSize), a)]
sstate_to_mem_eqs (Sstate Map Register a
_ Map (p, RegionSize) a
mem FlagStatus
_)  = Map (p, RegionSize) a -> [((p, RegionSize), a)]
forall k a. Map k a -> [(k, a)]
M.toList Map (p, RegionSize) a
mem



  unknown_internal_function :: p -> p -> State (Sstate SValue SPointer, VCS) ()
unknown_internal_function p
fctxt p
i = State (Sstate SValue SPointer, VCS) ()
incr_rsp -- TODO try as external

is_local_spointer :: p -> SPointer -> Bool
is_local_spointer p
fctxt (Base_StackPointer [Char]
_ PtrOffset
_)  = Bool
True
is_local_spointer p
fctxt b :: SPointer
b@(Base_StatePart StatePart
sp PtrOffset
_ ) = p -> SimpleExpr -> Bool
forall p. p -> SimpleExpr -> Bool
is_local_var p
fctxt (SimpleExpr -> Bool) -> SimpleExpr -> Bool
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
sp
is_local_spointer p
fctxt SPointer
_                        = Bool
False

is_local_var :: p -> SimpleExpr -> Bool
is_local_var p
fctxt (SE_Var (SP_StackPointer [Char]
_)) = Bool
True
is_local_var p
fctxt (SE_Var (SP_Mem SimpleExpr
a Int
si))       = SimpleExpr -> Maybe [Char]
is_local_expr SimpleExpr
a Maybe [Char] -> Maybe [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe [Char]
forall a. Maybe a
Nothing
is_local_var p
fctxt SimpleExpr
_                            = Bool
False


jump :: FContext -> X86.Instruction -> State (Sstate SValue SPointer,VCS) ()
jump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
jump FContext
fctxt Instruction
i
  | Context -> Instruction -> Bool
jump_is_actually_a_call (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i = FContext
-> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) ()
call FContext
fctxt Bool
True Instruction
i State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FContext -> Instruction -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS) ()
sexec_instr FContext
fctxt (AddressWord64
-> Maybe Prefix
-> Opcode
-> Maybe (GenericOperand Register)
-> [GenericOperand Register]
-> Maybe Int
-> Instruction
forall label storage prefix opcode annotation.
label
-> Maybe prefix
-> opcode
-> Maybe (GenericOperand storage)
-> [GenericOperand storage]
-> Maybe annotation
-> GenericInstruction label storage prefix opcode annotation
Instruction (Word64 -> AddressWord64
AddressWord64 Word64
0) Maybe Prefix
forall a. Maybe a
Nothing Opcode
SUB Maybe (GenericOperand Register)
forall a. Maybe a
Nothing [Register -> GenericOperand Register
forall storage. storage -> GenericOperand storage
Storage Register
RSP, Word64 -> GenericOperand Register
forall storage. Word64 -> GenericOperand storage
Immediate Word64
8] Maybe Int
forall a. Maybe a
Nothing) State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
-> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FContext -> State (Sstate SValue SPointer, VCS) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> State (Sstate v p, VCS) ()
sreturn FContext
fctxt
  | Bool
otherwise                                = () -> State (Sstate SValue SPointer, VCS) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


ctry_jump_targets :: FContext -> SValue -> Maybe (S.Set ResolvedJumpTarget)
ctry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
ctry_jump_targets FContext
fctxt v :: SValue
v@(SConcrete NESet SimpleExpr
es) = 
  let tries :: Set ResolvedJumpTarget
tries = (SimpleExpr -> Maybe ResolvedJumpTarget)
-> NESet SimpleExpr -> Set ResolvedJumpTarget
forall b a. Ord b => (a -> Maybe b) -> NESet a -> Set b
mapMaybeNES SimpleExpr -> Maybe ResolvedJumpTarget
try NESet SimpleExpr
es in
    if Set ResolvedJumpTarget -> Bool
forall a. Set a -> Bool
S.null Set ResolvedJumpTarget
tries then
      Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing -- trace ("Cannot resolve indirection: " ++ show v) Nothing      
    else
      Set ResolvedJumpTarget -> Maybe (Set ResolvedJumpTarget)
forall a. a -> Maybe a
Just Set ResolvedJumpTarget
tries
 where
  try :: SimpleExpr -> Maybe ResolvedJumpTarget
try SimpleExpr
e =
    case FContext -> Bool -> SimpleExpr -> Maybe SPointer
try_promote_expr FContext
fctxt Bool
False SimpleExpr
e of
      Just SPointer
ptr -> SPointer -> Maybe ResolvedJumpTarget
try_pointer SPointer
ptr
      Maybe SPointer
Nothing  -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing


  try_pointer :: SPointer -> Maybe ResolvedJumpTarget
try_pointer (Base_FunctionPtr Word64
a [Char]
f (PtrOffset Word64
0))  = ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
  try_pointer (Base_Immediate Word64
imm (PtrOffset Word64
0))    = Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
imm
  try_pointer b :: SPointer
b@(Base_StatePart (SP_Mem (SE_Immediate Word64
i) Int
_) PtrOffset
_) = Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing -- TODO do not report as unresolved if known symbol
  try_pointer SPointer
_ = Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing


  try_immediate_address :: Word64 -> Maybe ResolvedJumpTarget
try_immediate_address Word64
a
    | Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction (FContext -> Context
f_ctxt FContext
fctxt) Word64
a = ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ Word64 -> ResolvedJumpTarget
ImmediateAddress Word64
a 
    | Bool
otherwise = Word64 -> Maybe ResolvedJumpTarget
forall a. Integral a => a -> Maybe ResolvedJumpTarget
try_symbol Word64
a

  try_symbol :: a -> Maybe ResolvedJumpTarget
try_symbol a
a =
    case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table (Context -> IntMap Symbol) -> Context -> IntMap Symbol
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
fctxt of
      Just (Internal_Label [Char]
f)  -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
      Just (Relocated_Label [Char]
f) -> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a. a -> Maybe a
Just (ResolvedJumpTarget -> Maybe ResolvedJumpTarget)
-> ResolvedJumpTarget -> Maybe ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ [Char] -> ResolvedJumpTarget
External [Char]
f
      Maybe Symbol
_                        -> Maybe ResolvedJumpTarget
forall a. Maybe a
Nothing
ctry_jump_targets FContext
fctxt SValue
_ = Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing