{-# LANGUAGE PartialTypeSignatures, MultiParamTypeClasses, DeriveGeneric, DefaultSignatures, FlexibleContexts, Strict #-}



{-|
Module      : MachineState
Description : Functions for resolving symbolic memory reads and writes.

These functions are defined using the @State (Pred,VCS)@ monad.
Both the read- and write function may update the current predicate, as well as introduce new verification conditions.
-}
module Data.MachineState (
  read_reg,
  write_reg,
  read_mem,
  write_mem,
  read_operand,
  write_operand,
  read_sp,
  write_sp,
  invalid_bottom_pointer,
  address_is_unwritable,
  resolve_address
 )
 where

import Analysis.Context
import Base
import Data.ControlFlow
import Data.Binary
import Data.Pointers
import Data.SimplePred
import X86.Conventions
import Config

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 Data.Word 
import Data.Traversable (for)
import Control.Monad.State.Strict hiding (join)
import Control.Monad.Extra (partitionM,mapMaybeM)
import Data.List
import Data.Maybe (mapMaybe,fromJust,catMaybes)
import Debug.Trace
import GHC.Generics
import qualified Data.Serialize as Cereal hiding (get,put)
import X86.Register (Register (..))
import qualified X86.Register as Reg
import Typeclasses.HasSize (sizeof)
import qualified X86.Address as X86
import qualified X86.Operand as X86
import Generic.Address (GenericAddress(..))
import Generic.Operand (GenericOperand(..))


-- *  Registers
read_rreg :: Register -> State (Pred,VCS) SimpleExpr
read_rreg :: Register -> State (Pred, VCS) SimpleExpr
read_rreg Register
r = do
  (Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg, VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
  case StatePart -> Map StatePart SimpleExpr -> Maybe SimpleExpr
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Register -> StatePart
SP_Reg Register
r) Map StatePart SimpleExpr
eqs of
    Maybe SimpleExpr
Nothing -> do
      let var :: SimpleExpr
var = StatePart -> SimpleExpr
SE_Var (Register -> StatePart
SP_Reg Register
r)
      (Pred, VCS) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Pred, VCS) -> StateT (Pred, VCS) Identity ())
-> (Pred, VCS) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ (Map StatePart SimpleExpr -> FlagStatus -> Pred
Predicate (StatePart
-> SimpleExpr
-> Map StatePart SimpleExpr
-> Map StatePart SimpleExpr
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Register -> StatePart
SP_Reg Register
r) SimpleExpr
var Map StatePart SimpleExpr
eqs) FlagStatus
flg, VCS
vcs)
      SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
var 
    Just SimpleExpr
e  -> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
e

-- | Read from a register
read_reg :: FContext -> Register -> State (Pred,VCS) SimpleExpr
read_reg :: FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
r = do
  let rr :: Register
rr = Register -> Register
Reg.real Register
r
  SimpleExpr
v <- Register -> State (Pred, VCS) SimpleExpr
read_rreg Register
rr
  if Register -> Int
forall a. HasSize a => a -> Int
sizeof Register
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 then -- 64 bit 
    SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
v
  else if Register -> Int
forall a. HasSize a => a -> Int
sizeof Register
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 then -- 32 bit
    SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
32 SimpleExpr
v
  else if Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Register]
Reg.reg16 then -- 16 bit
    SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
16 SimpleExpr
v
  else if Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Register]
Reg.reg8 then -- 8 bit low registers
    SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
8 SimpleExpr
v
  else
    case SimpleExpr
v of
      SE_Immediate Word64
imm -> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
imm
      SimpleExpr
e -> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromBitMode (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e)



write_rreg :: FContext -> MemWriteIdentifier -> Register -> SimpleExpr -> State (Pred,VCS) () 
write_rreg :: FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid Register
r SimpleExpr
e = 
  if Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
2 (Register -> [Char]
forall a. Show a => a -> [Char]
show Register
r) [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"ST" then
    () -> StateT (Pred, VCS) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  --else if r == RSP && not (is_valid_rsp_value e) then do
  --  (p,_) <- get
  --  error $ "Illegal value for RSP: " ++ show e ++ "\n" ++ show p
  else do
    ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Pred, VCS) -> (Pred, VCS)
forall b. (Pred, b) -> (Pred, b)
do_write
 where
  do_write :: (Pred, b) -> (Pred, b)
do_write (Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg,b
vcs) =
    let eqs' :: Map StatePart SimpleExpr
eqs' = StatePart
-> SimpleExpr
-> Map StatePart SimpleExpr
-> Map StatePart SimpleExpr
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Register -> StatePart
SP_Reg Register
r) (FContext -> SimpleExpr -> SimpleExpr
trim_expr FContext
ctxt SimpleExpr
e) Map StatePart SimpleExpr
eqs
        flg' :: FlagStatus
flg' = StatePart -> FlagStatus -> FlagStatus
clean_flg (Register -> StatePart
SP_Reg Register
r) FlagStatus
flg in
      (Map StatePart SimpleExpr -> FlagStatus -> Pred
Predicate Map StatePart SimpleExpr
eqs' FlagStatus
flg',b
vcs)


is_valid_rsp_value :: SimpleExpr -> Bool
is_valid_rsp_value (SE_Op (Minus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
_]) = Bool
True
is_valid_rsp_value (SE_Op (Plus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
_]) = Bool
True
is_valid_rsp_value (SE_Op (And Int
_) [SE_Op (Plus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
_],SE_Immediate Word64
_]) = Bool
True
is_valid_rsp_value (SE_Op (Minus Int
_) [SE_Op (And Int
_) [SE_Op (Plus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
_],SE_Immediate Word64
_],SE_Immediate Word64
_]) = Bool
True
is_valid_rsp_value (SE_Var (SP_StackPointer [Char]
_)) = Bool
True
is_valid_rsp_value SimpleExpr
v = Bool
False
 
-- | Write to a register
write_reg :: FContext -> Word64 -> Register -> SimpleExpr -> State (Pred,VCS) ()
write_reg :: FContext
-> Word64
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_reg FContext
ctxt Word64
i_a Register
r SimpleExpr
v = do
 let mid :: MemWriteIdentifier
mid = Word64 -> Register -> MemWriteIdentifier
mk_reg_write_identifier Word64
i_a Register
r 
     sz :: Int
sz  = Register -> Int
forall a. HasSize a => a -> Int
sizeof Register
r in
  if Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 then -- 64 bit
    FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid Register
r (SimpleExpr -> StateT (Pred, VCS) Identity ())
-> SimpleExpr -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp SimpleExpr
v
  else if Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 then -- 32 bit
    FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid (Register -> Register
Reg.real Register
r) (SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
32 SimpleExpr
v)
  else if Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 then do -- 16 bit 
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    SimpleExpr
curr_v <- Register -> State (Pred, VCS) SimpleExpr
read_rreg Register
rr
    FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid Register
rr (SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
16 SimpleExpr
curr_v (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
16 SimpleExpr
v))
  else if Register
r Register -> [Register] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Register]
Reg.reg8 then do -- 8 bit low registers
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    SimpleExpr
curr_v <- Register -> State (Pred, VCS) SimpleExpr
read_rreg Register
rr
    FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid Register
rr (SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Int -> SimpleExpr -> SimpleExpr -> SimpleExpr
SE_Overwrite Int
8 SimpleExpr
curr_v (Int -> SimpleExpr -> SimpleExpr
SE_Bit Int
8 SimpleExpr
v))
  else
    FContext
-> MemWriteIdentifier
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_rreg FContext
ctxt MemWriteIdentifier
mid (Register -> Register
Reg.real Register
r) (SimpleExpr -> StateT (Pred, VCS) Identity ())
-> SimpleExpr -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromBitMode (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
v)


-- * Flags 


-- If the given StatePart is overwritten, does that taint the current flag status?
-- If so, set flagstatus to None, otherwise keep it.
clean_flg :: StatePart -> FlagStatus -> FlagStatus
clean_flg :: StatePart -> FlagStatus -> FlagStatus
clean_flg StatePart
sp FlagStatus
None               = FlagStatus
None
clean_flg StatePart
sp (FS_CMP Maybe Bool
b Operand
op1 Operand
op2) = do
  if Operand -> Bool
is_tainted Operand
op1 Bool -> Bool -> Bool
|| Operand -> Bool
is_tainted Operand
op2 then
    FlagStatus
None
  else
    Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP Maybe Bool
b Operand
op1 Operand
op2
 where
  is_tainted :: Operand -> Bool
is_tainted (Storage Register
r)          = StatePart
sp StatePart -> StatePart -> Bool
forall a. Eq a => a -> a -> Bool
== Register -> StatePart
SP_Reg (Register -> Register
Reg.real Register
r)
  is_tainted (Immediate Word64
_)        = Bool
False
  is_tainted (EffectiveAddress GenericAddress Register
_) = Bool
True -- TODO
  is_tainted (Memory GenericAddress Register
a Int
si)        =
    case StatePart
sp of
      SP_Mem SimpleExpr
_ Int
_ -> Bool
True
      StatePart
_          -> Bool
False





-- * Memory 

-- | Given the address of an operand of an instruction, resolve it given the current state.
resolve_address :: FContext -> X86.Address -> State (Pred,VCS) SimpleExpr
resolve_address :: FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt (AddressStorage Register
r) = FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
r
resolve_address FContext
ctxt (AddressImm Word64
i)     = SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i
resolve_address FContext
ctxt (AddressMinus GenericAddress Register
a0 GenericAddress Register
a1) = do
  SimpleExpr
ra0 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a0 
  SimpleExpr
ra1 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a1
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
64) [SimpleExpr
ra0,SimpleExpr
ra1]
resolve_address FContext
ctxt (AddressPlus GenericAddress Register
a0 GenericAddress Register
a1) = do
  SimpleExpr
ra0 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a0 
  SimpleExpr
ra1 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a1
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
64) [SimpleExpr
ra0,SimpleExpr
ra1]
resolve_address FContext
ctxt (AddressTimes GenericAddress Register
a0 GenericAddress Register
a1) = do
  SimpleExpr
ra0 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a0 
  SimpleExpr
ra1 <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a1
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Times Int
64) [SimpleExpr
ra0,SimpleExpr
ra1]


-- | Can we assume that the two given symbolic addresses are separate, and add a precondition?
-- Returns true iff the expressions do not contain bottom.
-- This function is called only after other checks have alreayd been done.
is_preconditionable :: p -> SimpleExpr -> SimpleExpr -> Bool
is_preconditionable p
ctxt SimpleExpr
a0 SimpleExpr
a1 = Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a0) Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1)

-- | Add a precondition to the given symbolic predicate
add_precondition :: SimpleExpr -> Int -> SimpleExpr -> Int -> (a, VCS) -> (a, VCS)
add_precondition SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 (a
p,VCS
vcs)   = (a
p,VerificationCondition -> VCS -> VCS
forall a. Ord a => a -> Set a -> Set a
S.insert (SimpleExpr -> Int -> SimpleExpr -> Int -> VerificationCondition
Precondition SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1) VCS
vcs)


-- | Can we assume that the two given symbolic addresses are separate, and add a assertion?
-- Even if two pointers contain bottom, we might still just assume (assert) they are separate based on their sources.
--
-- 1. If we write to an unknown region at the stackframe, we have to assert separation between the write and some essential known parts of the current stackframe.
--    These assertions are interesting, these may point to a stack overflow.
-- 2. If one is local and the other not, we assert separation.
-- 3. If the two pointers are global immediates from different global section, we assert separation.
-- 4. If one pointer is the return value of a call, and the other is different, we assert separation.
--
--
is_assertable :: FContext -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
is_assertable FContext
ctxt SimpleExpr
a0 a1
si0 SimpleExpr
a1 a2
si1 =
  let srcs0 :: Set BotSrc
srcs0       = FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
a0
      srcs1 :: Set BotSrc
srcs1       = FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
a1
      is_local0 :: ((BotSrc -> Bool) -> Set BotSrc -> t) -> t
is_local0 (BotSrc -> Bool) -> Set BotSrc -> t
q = (BotSrc -> Bool) -> Set BotSrc -> t
q BotSrc -> Bool
is_stackpointer_src Set BotSrc
srcs0
      is_local1 :: ((BotSrc -> Bool) -> Set BotSrc -> t) -> t
is_local1 (BotSrc -> Bool) -> Set BotSrc -> t
q = (BotSrc -> Bool) -> Set BotSrc -> t
q BotSrc -> Bool
is_stackpointer_src Set BotSrc
srcs1 in
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [
      --any (uncurry $ sources_separate_possibly ctxt) [(s0,s1) | s0 <- S.toList srcs0, s1 <- S.toList srcs1],
      FContext -> Bool -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
forall a1 a2.
(Integral a1, Integral a2) =>
FContext -> Bool -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
separate_pointer_domains FContext
ctxt Bool
False SimpleExpr
a0 a1
si0 SimpleExpr
a1 a2
si1,
      --is_local0 all && not (S.null srcs1) && not (is_local1 any),
      -- is_local1 all && not (S.null srcs0) && not (is_local0 any),

      Set BotSrc -> Bool
is_call Set BotSrc
srcs0 Bool -> Bool -> Bool
&& SimpleExpr
a0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
/= SimpleExpr
a1,
      Set BotSrc -> Bool
is_call Set BotSrc
srcs1 Bool -> Bool -> Bool
&& SimpleExpr
a0 SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
/= SimpleExpr
a1,

      SimpleExpr -> Bool
contains_bot SimpleExpr
a0 Bool -> Bool -> Bool
&& ((BotSrc -> Bool) -> Set BotSrc -> Bool) -> Bool
forall t. ((BotSrc -> Bool) -> Set BotSrc -> t) -> t
is_local0 (BotSrc -> Bool) -> Set BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool -> Bool
&& Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a1) Bool -> Bool -> Bool
&& ((BotSrc -> Bool) -> Set BotSrc -> Bool) -> Bool
forall t. ((BotSrc -> Bool) -> Set BotSrc -> t) -> t
is_local1 (BotSrc -> Bool) -> Set BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all -- TODO make more precise, only certain parts of a1 
     ]
 where
  is_call :: Set BotSrc -> Bool
is_call Set BotSrc
srcs = Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& (BotSrc -> Bool) -> Set BotSrc -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all BotSrc -> Bool
is_src_call Set BotSrc
srcs

  is_src_call :: BotSrc -> Bool
is_src_call (Src_Function [Char]
_) = Bool
True
  is_src_call BotSrc
_                = Bool
False 

  is_stackpointer_src :: BotSrc -> Bool
is_stackpointer_src (Src_StackPointer [Char]
_) = Bool
True  -- TODO compare stackframes
  is_stackpointer_src BotSrc
_                    = Bool
False


  


-- | Add an assertion to the given symbolic predicate
add_assertion :: FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (a, VCS)
-> (a, VCS)
add_assertion FContext
ctxt SimpleExpr
rip SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 (a
p,VCS
vcs) =
  if Config -> Bool
store_assertions_in_report (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Config
ctxt_config (Context -> Config) -> Context -> Config
forall a b. (a -> b) -> a -> b
$ FContext -> Context
f_ctxt FContext
ctxt then
    (a
p,VerificationCondition -> VCS -> VCS
forall a. Ord a => a -> Set a -> Set a
S.insert (SimpleExpr
-> SimpleExpr -> Int -> SimpleExpr -> Int -> VerificationCondition
Assertion SimpleExpr
rip SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1) VCS
vcs)
  else
    (a
p,VCS
vcs)



generate_assertion :: FContext -> Maybe X86.Address -> SimpleExpr -> State (Pred,VCS) SimpleExpr
generate_assertion :: FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt Maybe (GenericAddress Register)
Nothing SimpleExpr
a0                    = SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
a0
generate_assertion FContext
ctxt (Just (AddressStorage Register
r)) SimpleExpr
_   = FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
r
generate_assertion FContext
ctxt (Just (AddressImm Word64
i))       SimpleExpr
_ = SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate (Word64 -> SimpleExpr) -> Word64 -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i
generate_assertion FContext
ctxt (Just (AddressMinus GenericAddress Register
a0 GenericAddress Register
a1)) SimpleExpr
x = do
  SimpleExpr
v0 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a0) SimpleExpr
x
  SimpleExpr
v1 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a1) SimpleExpr
x
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Minus Int
64) [SimpleExpr
v0,SimpleExpr
v1]
generate_assertion FContext
ctxt (Just (AddressPlus GenericAddress Register
a0 GenericAddress Register
a1) ) SimpleExpr
x = do
  SimpleExpr
v0 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a0) SimpleExpr
x
  SimpleExpr
v1 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a1) SimpleExpr
x
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Plus Int
64) [SimpleExpr
v0,SimpleExpr
v1]
generate_assertion FContext
ctxt (Just (AddressTimes GenericAddress Register
a0 GenericAddress Register
a1)) SimpleExpr
x = do
  SimpleExpr
v0 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a0) SimpleExpr
x
  SimpleExpr
v1 <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
a1) SimpleExpr
x
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> SimpleExpr
simp (SimpleExpr -> SimpleExpr) -> SimpleExpr -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Operator -> [SimpleExpr] -> SimpleExpr
SE_Op (Int -> Operator
Times Int
64) [SimpleExpr
v0,SimpleExpr
v1]
  



-- | An address is considered "unwritable" only if it is an immediate address that belongs to a section that is considered unwritable
-- according to Conventions (see 'section_is_unwritable')
address_is_unwritable :: Context -> SimpleExpr -> Bool
address_is_unwritable Context
ctxt (SE_Immediate Word64
a) =
  case Context -> Word64 -> Maybe ([Char], [Char], Word64, Word64)
find_section_for_address Context
ctxt (Word64 -> Maybe ([Char], [Char], Word64, Word64))
-> Word64 -> Maybe ([Char], [Char], Word64, Word64)
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a of
    Maybe ([Char], [Char], Word64, Word64)
Nothing -> Bool
False
    Just ([Char]
segname,[Char]
sectname,Word64
_,Word64
_) -> ([Char], [Char]) -> Bool
section_is_unwritable ([Char]
segname,[Char]
sectname)
address_is_unwritable Context
ctxt SimpleExpr
_ = Bool
False





-- | Returns true if a pointer is not suitable for writing to memory.
-- This may happen if the symbolic expression provides no information, i.e., it has @Bottom@ without known pointerbases,
-- and without any sources.
invalid_bottom_pointer :: FContext -> SimpleExpr -> Bool
invalid_bottom_pointer FContext
ctxt SimpleExpr
e = Bool -> Bool
not (SimpleExpr -> Bool
is_immediate SimpleExpr
e) Bool -> Bool -> Bool
&& Set BotSrc -> Bool
forall a. Set a -> Bool
S.null (FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e) 

-- | Assuming a valid pointer (see 'invalid_bottom_pointer'), produce a list of pointers that are to be written to in the memory.
expr_to_mem_addresses :: FContext -> SimpleExpr -> b -> [(SimpleExpr, b)]
expr_to_mem_addresses FContext
ctxt SimpleExpr
a b
si =
  if Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
a) then
    [(SimpleExpr
a,b
si)]
  else
    let addresses :: [(SimpleExpr, b)]
addresses = PointerDomain -> [(SimpleExpr, b)]
forall b. Num b => PointerDomain -> [(SimpleExpr, b)]
dom_to_mem_addresses (PointerDomain -> [(SimpleExpr, b)])
-> PointerDomain -> [(SimpleExpr, b)]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> PointerDomain
get_pointer_domain FContext
ctxt SimpleExpr
a in
      [(SimpleExpr, b)]
addresses
 where 
  is_global :: BotSrc -> Bool
is_global (Src_ImmediateAddress Word64
_) = Bool
True
  is_global BotSrc
_ = Bool
False

  dom_to_mem_addresses :: PointerDomain -> [(SimpleExpr, b)]
dom_to_mem_addresses (Domain_Bases Set PointerBase
bs)     = ([PointerBase] -> (SimpleExpr, b))
-> [[PointerBase]] -> [(SimpleExpr, b)]
forall a b. (a -> b) -> [a] -> [b]
map [PointerBase] -> (SimpleExpr, b)
forall b. Num b => [PointerBase] -> (SimpleExpr, b)
base_to_mem_address ([[PointerBase]] -> [(SimpleExpr, b)])
-> [[PointerBase]] -> [(SimpleExpr, b)]
forall a b. (a -> b) -> a -> b
$ [PointerBase] -> [[PointerBase]]
split_per_base ([PointerBase] -> [[PointerBase]])
-> [PointerBase] -> [[PointerBase]]
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs
  dom_to_mem_addresses (Domain_Sources Set BotSrc
srcs) = ([BotSrc] -> (SimpleExpr, b)) -> [[BotSrc]] -> [(SimpleExpr, b)]
forall a b. (a -> b) -> [a] -> [b]
map [BotSrc] -> (SimpleExpr, b)
forall b. Num b => [BotSrc] -> (SimpleExpr, b)
srcs_to_mem_address ([[BotSrc]] -> [(SimpleExpr, b)])
-> [[BotSrc]] -> [(SimpleExpr, b)]
forall a b. (a -> b) -> a -> b
$ [BotSrc] -> [[BotSrc]]
split_per_source ([BotSrc] -> [[BotSrc]]) -> [BotSrc] -> [[BotSrc]]
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs

  base_to_mem_address :: [PointerBase] -> (SimpleExpr, b)
base_to_mem_address [PointerBase]
bs = (BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> BotTyp
FromPointerBases (Set PointerBase -> BotTyp) -> Set PointerBase -> BotTyp
forall a b. (a -> b) -> a -> b
$ [PointerBase] -> Set PointerBase
forall a. Ord a => [a] -> Set a
S.fromList [PointerBase]
bs, b
1)

  srcs_to_mem_address :: [BotSrc] -> (SimpleExpr, b)
srcs_to_mem_address [Src_StackPointer [Char]
f] = (BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> BotTyp
FromPointerBases (Set PointerBase -> BotTyp) -> Set PointerBase -> BotTyp
forall a b. (a -> b) -> a -> b
$ PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ [Char] -> PointerBase
StackPointer [Char]
f,b
1)
  srcs_to_mem_address [Src_Malloc Maybe Word64
i Maybe [Char]
h]     = (BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> BotTyp
FromPointerBases (Set PointerBase -> BotTyp) -> Set PointerBase -> BotTyp
forall a b. (a -> b) -> a -> b
$ PointerBase -> Set PointerBase
forall a. a -> Set a
S.singleton (PointerBase -> Set PointerBase) -> PointerBase -> Set PointerBase
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> PointerBase
Malloc Maybe Word64
i Maybe [Char]
h,b
1)
  srcs_to_mem_address [BotSrc]
srcs                 = (BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> BotTyp
FromSources (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ [BotSrc] -> Set BotSrc
forall a. Ord a => [a] -> Set a
S.fromList [BotSrc]
srcs,b
1)
    
  split_per_base :: [PointerBase] -> [[PointerBase]]
split_per_base [] = []
  split_per_base (PointerBase
bs:[PointerBase]
bss) =
    let ([PointerBase]
separate,[PointerBase]
overlapping) = (PointerBase -> Bool)
-> [PointerBase] -> ([PointerBase], [PointerBase])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (FContext -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_possibly FContext
ctxt PointerBase
bs) [PointerBase]
bss in
      (PointerBase
bsPointerBase -> [PointerBase] -> [PointerBase]
forall a. a -> [a] -> [a]
:[PointerBase]
overlapping) [PointerBase] -> [[PointerBase]] -> [[PointerBase]]
forall a. a -> [a] -> [a]
: [PointerBase] -> [[PointerBase]]
split_per_base [PointerBase]
separate

  split_per_source :: [BotSrc] -> [[BotSrc]]
split_per_source [] = [] 
  split_per_source (BotSrc
src:[BotSrc]
srcs) =
    let ([BotSrc]
separate,[BotSrc]
overlapping) = (BotSrc -> Bool) -> [BotSrc] -> ([BotSrc], [BotSrc])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (FContext -> BotSrc -> BotSrc -> Bool
sources_separate_possibly FContext
ctxt BotSrc
src) [BotSrc]
srcs in
      (BotSrc
srcBotSrc -> [BotSrc] -> [BotSrc]
forall a. a -> [a] -> [a]
:[BotSrc]
overlapping) [BotSrc] -> [[BotSrc]] -> [[BotSrc]]
forall a. a -> [a] -> [a]
: [BotSrc] -> [[BotSrc]]
split_per_source [BotSrc]
separate






data SeparationStatus = Alias | Separated | Enclosed | Disclosed | Overlap
  deriving SeparationStatus -> SeparationStatus -> Bool
(SeparationStatus -> SeparationStatus -> Bool)
-> (SeparationStatus -> SeparationStatus -> Bool)
-> Eq SeparationStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SeparationStatus -> SeparationStatus -> Bool
$c/= :: SeparationStatus -> SeparationStatus -> Bool
== :: SeparationStatus -> SeparationStatus -> Bool
$c== :: SeparationStatus -> SeparationStatus -> Bool
Eq


is_rock_bottom :: SimpleExpr -> Bool
is_rock_bottom (Bottom (FromSources Set BotSrc
srcs)) = Set BotSrc -> Bool
forall a. Set a -> Bool
S.null Set BotSrc
srcs
is_rock_bottom SimpleExpr
_ = Bool
False

read_from_address :: FContext -> Maybe X86.Operand -> SimpleExpr -> Int -> State (Pred,VCS) SimpleExpr
read_from_address :: FContext
-> Maybe Operand
-> SimpleExpr
-> Int
-> State (Pred, VCS) SimpleExpr
read_from_address FContext
ctxt Maybe Operand
operand SimpleExpr
a Int
si0 = do
  let as :: [SimpleExpr]
as = (SimpleExpr -> SimpleExpr) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> SimpleExpr
simp ([SimpleExpr] -> [SimpleExpr]) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt SimpleExpr
a
  [SimpleExpr]
vs <- (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> [SimpleExpr] -> StateT (Pred, VCS) Identity [SimpleExpr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SimpleExpr -> State (Pred, VCS) SimpleExpr
read_from_address' [SimpleExpr]
as
  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs ([Char]
"Read") FContext
ctxt [SimpleExpr]
vs
 where
  read_from_address' :: SimpleExpr -> State (Pred, VCS) SimpleExpr
read_from_address' (SE_Immediate Word64
imm) = 
    case Context -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection (FContext -> Context
f_ctxt FContext
ctxt) Word64
imm Int
si0 of 
      Just Word64
imm -> -- trace ("Read immediate from datasection: " ++ show (a0,si0) ++ " := " ++ show imm) $ return $ SE_Immediate imm
                  SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
imm  
      Maybe Word64
Nothing  -> SimpleExpr -> State (Pred, VCS) SimpleExpr
read_from_state (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
imm
  read_from_address' SimpleExpr
a0 = SimpleExpr -> State (Pred, VCS) SimpleExpr
read_from_state SimpleExpr
a0


  read_from_state :: SimpleExpr -> State (Pred,VCS) SimpleExpr
  read_from_state :: SimpleExpr -> State (Pred, VCS) SimpleExpr
read_from_state SimpleExpr
a0 = do
    if SimpleExpr -> Bool
contains_bot SimpleExpr
a0 then
      if FContext -> SimpleExpr -> Bool
invalid_bottom_pointer FContext
ctxt SimpleExpr
a0 then do
        --rip <- read_reg ctxt RIP
        --trace ("READ FROM BASELESS POINTER @ " ++ show rip ++ ": " ++ show (a,si0)) $
        SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
rock_bottom
      else do
        (Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg,VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
        [(StatePart, SimpleExpr)]
overlapping <- ((StatePart, SimpleExpr) -> StateT (Pred, VCS) Identity Bool)
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Bool -> Bool)
-> StateT (Pred, VCS) Identity Bool
-> StateT (Pred, VCS) Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (StateT (Pred, VCS) Identity Bool
 -> StateT (Pred, VCS) Identity Bool)
-> ((StatePart, SimpleExpr) -> StateT (Pred, VCS) Identity Bool)
-> (StatePart, SimpleExpr)
-> StateT (Pred, VCS) Identity Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleExpr
-> (StatePart, SimpleExpr) -> StateT (Pred, VCS) Identity Bool
forall b.
SimpleExpr -> (StatePart, b) -> StateT (Pred, VCS) Identity Bool
has_separate_base SimpleExpr
a0) ([(StatePart, SimpleExpr)]
 -> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)])
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> a -> b
$ Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
eqs

        let sps' :: [StatePart]
sps'      = ((SimpleExpr, Int) -> StatePart)
-> [(SimpleExpr, Int)] -> [StatePart]
forall a b. (a -> b) -> [a] -> [b]
map ((SimpleExpr -> Int -> StatePart) -> (SimpleExpr, Int) -> StatePart
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> Int -> StatePart
SP_Mem) ([(SimpleExpr, Int)] -> [StatePart])
-> [(SimpleExpr, Int)] -> [StatePart]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Int -> [(SimpleExpr, Int)]
forall b. Num b => FContext -> SimpleExpr -> b -> [(SimpleExpr, b)]
expr_to_mem_addresses FContext
ctxt SimpleExpr
a0  Int
si0
        let new_eqs :: [(StatePart, SimpleExpr)]
new_eqs   = (StatePart -> (StatePart, SimpleExpr))
-> [StatePart] -> [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\StatePart
sp' -> (StatePart
sp',StatePart -> SimpleExpr
mk_uninitialized_value StatePart
sp')) [StatePart]
sps'
        if [(StatePart, SimpleExpr)]
overlapping [(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then do
          let eqs' :: Map StatePart SimpleExpr
eqs'    = Map StatePart SimpleExpr
-> Map StatePart SimpleExpr -> Map StatePart SimpleExpr
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union ([(StatePart, SimpleExpr)] -> Map StatePart SimpleExpr
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(StatePart, SimpleExpr)]
new_eqs) Map StatePart SimpleExpr
eqs
          (Pred, VCS) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map StatePart SimpleExpr -> FlagStatus -> Pred
Predicate Map StatePart SimpleExpr
eqs' FlagStatus
flg,VCS
vcs)
          let srcs :: Set BotSrc
srcs      = FContext -> [SimpleExpr] -> Set BotSrc
srcs_of_exprs FContext
ctxt ([SimpleExpr] -> Set BotSrc) -> [SimpleExpr] -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ ((StatePart, SimpleExpr) -> SimpleExpr)
-> [(StatePart, SimpleExpr)] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart, SimpleExpr) -> SimpleExpr
forall a b. (a, b) -> b
snd [(StatePart, SimpleExpr)]
new_eqs
          let bot :: SimpleExpr
bot       = BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromUninitializedMemory Set BotSrc
srcs)
          SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
bot 
        else do
          let srcs :: Set BotSrc
srcs      = if (SimpleExpr -> Bool) -> [SimpleExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SimpleExpr -> Bool
is_rock_bottom (((StatePart, SimpleExpr) -> SimpleExpr)
-> [(StatePart, SimpleExpr)] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart, SimpleExpr) -> SimpleExpr
forall a b. (a, b) -> b
snd [(StatePart, SimpleExpr)]
overlapping) then Set BotSrc
forall a. Set a
S.empty else FContext -> [SimpleExpr] -> Set BotSrc
srcs_of_exprs FContext
ctxt ([SimpleExpr] -> Set BotSrc) -> [SimpleExpr] -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ ((StatePart, SimpleExpr) -> SimpleExpr)
-> [(StatePart, SimpleExpr)] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart, SimpleExpr) -> SimpleExpr
forall a b. (a, b) -> b
snd ([(StatePart, SimpleExpr)]
new_eqs [(StatePart, SimpleExpr)]
-> [(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)]
forall a. [a] -> [a] -> [a]
++ [(StatePart, SimpleExpr)]
overlapping)
          let bot :: SimpleExpr
bot       = BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromOverlap Set BotSrc
srcs)
          SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
bot 
    else if Context -> SimpleExpr -> Bool
address_is_unwritable (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
a0 then do
      let sp :: StatePart
sp  = SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a0 Int
si0
      let var :: SimpleExpr
var = StatePart -> SimpleExpr
SE_Var StatePart
sp
      SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
var   
    else do
      (Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg,VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
      SimpleExpr
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
do_read SimpleExpr
a0 ([(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr)
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
eqs


  has_separate_base :: SimpleExpr -> (StatePart, b) -> StateT (Pred, VCS) Identity Bool
has_separate_base SimpleExpr
a0 (SP_Reg Register
_,b
_)      = Bool -> StateT (Pred, VCS) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  has_separate_base SimpleExpr
a0 (SP_Mem SimpleExpr
a1 Int
si1,b
_) = do
    SeparationStatus
sep <- SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> StateT (Pred, VCS) Identity SeparationStatus
is_separate SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
    Bool -> StateT (Pred, VCS) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT (Pred, VCS) Identity Bool)
-> Bool -> StateT (Pred, VCS) Identity Bool
forall a b. (a -> b) -> a -> b
$ SeparationStatus
sep SeparationStatus -> SeparationStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SeparationStatus
Separated


  mk_uninitialized_value :: StatePart -> SimpleExpr
mk_uninitialized_value sp :: StatePart
sp@(SP_Mem SimpleExpr
a Int
si) = 
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SimpleExpr -> Bool
contains_bot SimpleExpr
a then
      BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromUninitializedMemory (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (BotSrc -> Set BotSrc) -> BotSrc -> Set BotSrc
forall a b. (a -> b) -> a -> b
$ StatePart -> BotSrc
Src_Var StatePart
sp)
    else
      BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromUninitializedMemory (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
a) -- rock_bottom 

  is_separate :: SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> StateT (Pred, VCS) Identity SeparationStatus
is_separate SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 = do
    if Int
si0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si1 Bool -> Bool -> Bool
&& SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
a0 SimpleExpr
a1 then
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Alias
    else if FContext -> SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a.
Integral a =>
FContext -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate FContext
ctxt SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else if SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then
      --trace ("PRECONDITION (READ): ENCLOSURE BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1))
       SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Enclosed
    else if SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
a1 Int
si1 SimpleExpr
a0 Int
si0 then
      --trace ("PRECONDITION (READ): DISCLOSURE BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1))
       SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Disclosed
    else if FContext -> SimpleExpr -> SimpleExpr -> Bool
forall p. p -> SimpleExpr -> SimpleExpr -> Bool
is_preconditionable FContext
ctxt SimpleExpr
a0 SimpleExpr
a1 then do
      --trace ("PRECONDITION (READ): SEPARATION BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1))
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ SimpleExpr
-> Int -> SimpleExpr -> Int -> (Pred, VCS) -> (Pred, VCS)
forall a.
SimpleExpr -> Int -> SimpleExpr -> Int -> (a, VCS) -> (a, VCS)
add_precondition SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else if FContext -> SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a1 a2.
(Integral a1, Integral a2) =>
FContext -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
is_assertable FContext
ctxt SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then do
      SimpleExpr
rip <- FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
RIP
      SimpleExpr
assertion <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (Maybe Operand -> Maybe (GenericAddress Register)
forall storage.
Maybe (GenericOperand storage) -> Maybe (GenericAddress storage)
mk_address Maybe Operand
operand) SimpleExpr
a0
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (Pred, VCS)
-> (Pred, VCS)
forall a.
FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (a, VCS)
-> (a, VCS)
add_assertion FContext
ctxt SimpleExpr
rip SimpleExpr
assertion Int
si0 SimpleExpr
a1 Int
si1
      --trace ("ASSERTION (READ@" ++ show rip ++ "): SEPARATION BETWEEN " ++ show (assertion,si0,a0) ++ " and " ++ show (a1,si1)) $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else do
     --if do_trace a0 a1 then trace ("PRECONDITION (READ): OVERLAP BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1)) $ return Overlap else
     SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Overlap

  mk_address :: Maybe (GenericOperand storage) -> Maybe (GenericAddress storage)
mk_address (Just (Memory GenericAddress storage
a Int
si)) = GenericAddress storage -> Maybe (GenericAddress storage)
forall a. a -> Maybe a
Just GenericAddress storage
a
  mk_address Maybe (GenericOperand storage)
_                    = Maybe (GenericAddress storage)
forall a. Maybe a
Nothing

  do_trace :: p -> p -> Bool
do_trace p
a0 p
a1 = Bool
True--srcs_of_expr ctxt a0 /= srcs_of_expr ctxt a1 


  do_read :: SimpleExpr -> [(StatePart, SimpleExpr)] -> State (Pred,VCS) SimpleExpr
  do_read :: SimpleExpr
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
do_read SimpleExpr
a0 [] = do
    (Pred
p,VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
    let Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg = Pred
p
    let sp :: StatePart
sp  = SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a0 Int
si0
    let var :: SimpleExpr
var = BotTyp -> SimpleExpr
Bottom (BotTyp -> SimpleExpr) -> BotTyp -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> BotTyp
FromUninitializedMemory (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ BotSrc -> Set BotSrc
forall a. a -> Set a
S.singleton (StatePart -> BotSrc
Src_Var StatePart
sp)
    (Pred, VCS) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map StatePart SimpleExpr -> FlagStatus -> Pred
Predicate (StatePart
-> SimpleExpr
-> Map StatePart SimpleExpr
-> Map StatePart SimpleExpr
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert StatePart
sp SimpleExpr
var Map StatePart SimpleExpr
eqs) FlagStatus
flg,VCS
vcs)
    SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SimpleExpr
var
  do_read SimpleExpr
a0 ((SP_Reg Register
_,SimpleExpr
_):[(StatePart, SimpleExpr)]
mem)       = SimpleExpr
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
do_read SimpleExpr
a0 [(StatePart, SimpleExpr)]
mem
  do_read SimpleExpr
a0 ((SP_Mem SimpleExpr
a1 Int
si1,SimpleExpr
e1):[(StatePart, SimpleExpr)]
mem) = do
      SeparationStatus
sep <- SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> StateT (Pred, VCS) Identity SeparationStatus
is_separate SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
      case SeparationStatus
sep of
        SeparationStatus
Alias     -> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr
e1
        SeparationStatus
Separated -> SimpleExpr
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
do_read SimpleExpr
a0 [(StatePart, SimpleExpr)]
mem
        SeparationStatus
Enclosed  -> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ BotTyp -> SimpleExpr
Bottom (Set BotSrc -> BotTyp
FromOverlap (Set BotSrc -> BotTyp) -> Set BotSrc -> BotTyp
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Set BotSrc
srcs_of_expr FContext
ctxt SimpleExpr
e1)
        SeparationStatus
_         -> do
          SimpleExpr
e0 <- SimpleExpr
-> [(StatePart, SimpleExpr)] -> State (Pred, VCS) SimpleExpr
do_read SimpleExpr
a0 [(StatePart, SimpleExpr)]
mem
          let bot :: SimpleExpr
bot  = [Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs ([Char]
"read merge overlapping values2" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SimpleExpr, Int, SimpleExpr, Int) -> [Char]
forall a. Show a => a -> [Char]
show (SimpleExpr
a0,Int
si0,SimpleExpr
a1,Int
si1)) FContext
ctxt ([SimpleExpr] -> SimpleExpr) -> [SimpleExpr] -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Bool) -> [SimpleExpr] -> [SimpleExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter (SimpleExpr -> SimpleExpr -> Bool
forall a. Eq a => a -> a -> Bool
(/=) SimpleExpr
rock_bottom) [SimpleExpr
e0,SimpleExpr
e1]
          SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ SimpleExpr
bot 



-- | Read from memory
read_mem :: 
     FContext     -- ^ The context
  -> X86.Operand  -- ^ The address of an operand of an instruction
  -> State (Pred,VCS) SimpleExpr
read_mem :: FContext -> Operand -> State (Pred, VCS) SimpleExpr
read_mem FContext
ctxt (Memory GenericAddress Register
a Int
si) = do
  SimpleExpr
resolved_address <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a
  FContext
-> Maybe Operand
-> SimpleExpr
-> Int
-> State (Pred, VCS) SimpleExpr
read_from_address FContext
ctxt (Operand -> Maybe Operand
forall a. a -> Maybe a
Just (Operand -> Maybe Operand) -> Operand -> Maybe Operand
forall a b. (a -> b) -> a -> b
$ GenericAddress Register -> Int -> Operand
forall storage.
GenericAddress storage -> Int -> GenericOperand storage
Memory GenericAddress Register
a Int
si) SimpleExpr
resolved_address Int
si



add_unknown_mem_write :: MemWriteIdentifier -> (a, VCS) -> (a, VCS)
add_unknown_mem_write MemWriteIdentifier
mid (a
p,VCS
vcs) = (a
p,VerificationCondition -> VCS -> VCS
forall a. Ord a => a -> Set a -> Set a
S.insert (MemWriteIdentifier -> VerificationCondition
SourcelessMemWrite MemWriteIdentifier
mid) VCS
vcs)

-- | Write to memory
-- Each memory write is accomponied with a `MemWriteIdentifier` so that we can log memory writes to unknown locations.
--
write_mem :: 
  FContext               -- ^ The context
  -> MemWriteIdentifier  -- ^ An identifier where the write occurs
  -> SimpleExpr          -- ^ The symbolic address
  -> Int                 -- ^ The size (in bytes)
  -> SimpleExpr          -- ^ The value to be written
  -> State (Pred,VCS) ()
write_mem :: FContext
-> MemWriteIdentifier
-> SimpleExpr
-> Int
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_mem FContext
ctxt MemWriteIdentifier
mid SimpleExpr
a Int
si0 SimpleExpr
v = do
  let as :: [SimpleExpr]
as = (SimpleExpr -> SimpleExpr) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> SimpleExpr
simp ([SimpleExpr] -> [SimpleExpr]) -> [SimpleExpr] -> [SimpleExpr]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> [SimpleExpr]
unfold_non_determinism FContext
ctxt SimpleExpr
a
  (SimpleExpr -> StateT (Pred, VCS) Identity ())
-> [SimpleExpr] -> StateT (Pred, VCS) Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\SimpleExpr
a -> SimpleExpr -> SimpleExpr -> StateT (Pred, VCS) Identity ()
write_mem' SimpleExpr
a SimpleExpr
v) [SimpleExpr]
as -- TODO v should be bot?
 where
  write_mem' :: SimpleExpr -> SimpleExpr -> StateT (Pred, VCS) Identity ()
write_mem' SimpleExpr
a0 SimpleExpr
v = do
    p :: (Pred, VCS)
p@(Predicate Map StatePart SimpleExpr
eqs FlagStatus
flg,VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get

    if Context -> SimpleExpr -> Bool
address_is_unwritable (FContext -> Context
f_ctxt FContext
ctxt) SimpleExpr
a0 then do
      [Char]
-> StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ()
forall a. [Char] -> a -> a
trace ([Char]
"Writing to unwritable section: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (SimpleExpr, Int) -> [Char]
forall a. Show a => a -> [Char]
show (SimpleExpr
a0,Int
si0)) (StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ())
-> StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ () -> StateT (Pred, VCS) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else if FContext -> SimpleExpr -> Bool
invalid_bottom_pointer FContext
ctxt SimpleExpr
a0 Bool -> Bool -> Bool
&& FContext -> SimpleExpr -> Bool
invalid_bottom_pointer FContext
ctxt SimpleExpr
a then do -- FORALL PATHS VS EXISTS PATH
      --error (show (a0,a,get_known_pointer_bases ctxt a0, srcs_of_expr ctxt a0, get_known_pointer_bases ctxt a, srcs_of_expr ctxt a))
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ MemWriteIdentifier -> (Pred, VCS) -> (Pred, VCS)
forall a. MemWriteIdentifier -> (a, VCS) -> (a, VCS)
add_unknown_mem_write MemWriteIdentifier
mid
    else do
      (Pred, VCS)
p <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
      (Predicate Map StatePart SimpleExpr
eqs FlagStatus
_ ,VCS
_) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
      Map StatePart SimpleExpr
eqs' <- [(StatePart, SimpleExpr)] -> Map StatePart SimpleExpr
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(StatePart, SimpleExpr)] -> Map StatePart SimpleExpr)
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity (Map StatePart SimpleExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write SimpleExpr
a0 Int
si0 SimpleExpr
v (Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
eqs)
      (Predicate Map StatePart SimpleExpr
_ FlagStatus
flg,VCS
vcs) <- StateT (Pred, VCS) Identity (Pred, VCS)
forall s (m :: * -> *). MonadState s m => m s
get
      let flg' :: FlagStatus
flg' = StatePart -> FlagStatus -> FlagStatus
clean_flg (SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a0 Int
si0) FlagStatus
flg
      (Pred, VCS) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map StatePart SimpleExpr -> FlagStatus -> Pred
Predicate Map StatePart SimpleExpr
eqs' FlagStatus
flg',VCS
vcs)


  is_separate :: SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> StateT (Pred, VCS) Identity SeparationStatus
is_separate SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 = do
    if Int
si0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si1 Bool -> Bool -> Bool
&& SimpleExpr -> SimpleExpr -> Bool
necessarily_equal SimpleExpr
a0 SimpleExpr
a1 then
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Alias
    else if FContext -> SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a.
Integral a =>
FContext -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate FContext
ctxt SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then
      --trace ("SEPARATION (WRITE) BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1) ++ "\n") $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else if SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then do
      --trace ("ENCLOSURE1 (WRITE) BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1)) $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Enclosed
    else if SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a. Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed SimpleExpr
a1 Int
si1 SimpleExpr
a0 Int
si0 then do
      --trace ("ENCLOSURE2 (WRITE) BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1)) $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Disclosed
    else if FContext -> SimpleExpr -> SimpleExpr -> Bool
forall p. p -> SimpleExpr -> SimpleExpr -> Bool
is_preconditionable FContext
ctxt SimpleExpr
a0 SimpleExpr
a1 then do
      --trace ("PRECONDITION (WRITE): SEPARATION BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1))
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ SimpleExpr
-> Int -> SimpleExpr -> Int -> (Pred, VCS) -> (Pred, VCS)
forall a.
SimpleExpr -> Int -> SimpleExpr -> Int -> (a, VCS) -> (a, VCS)
add_precondition SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else if FContext -> SimpleExpr -> Int -> SimpleExpr -> Int -> Bool
forall a1 a2.
(Integral a1, Integral a2) =>
FContext -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
is_assertable FContext
ctxt SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1 then do
      SimpleExpr
assertion <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (MemWriteIdentifier -> Maybe (GenericAddress Register)
address MemWriteIdentifier
mid) SimpleExpr
a0
      SimpleExpr
rip <- FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
RIP
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (Pred, VCS)
-> (Pred, VCS)
forall a.
FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (a, VCS)
-> (a, VCS)
add_assertion FContext
ctxt SimpleExpr
rip SimpleExpr
assertion Int
si0 SimpleExpr
a1 Int
si1
      --trace ("ASSERTION (WRITE@" ++ show rip ++ "): SEPARATION BETWEEN " ++ show (assertion,si0,a0) ++ " and " ++ show (a1,si1)) $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else if FContext -> SimpleExpr -> Bool
invalid_bottom_pointer FContext
ctxt SimpleExpr
a0 Bool -> Bool -> Bool
&& FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer FContext
ctxt SimpleExpr
a1 then do
      SimpleExpr
assertion <- FContext
-> Maybe (GenericAddress Register)
-> SimpleExpr
-> State (Pred, VCS) SimpleExpr
generate_assertion FContext
ctxt (MemWriteIdentifier -> Maybe (GenericAddress Register)
address MemWriteIdentifier
mid) SimpleExpr
a0
      SimpleExpr
rip <- FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
RIP
      ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ())
-> ((Pred, VCS) -> (Pred, VCS)) -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (Pred, VCS)
-> (Pred, VCS)
forall a.
FContext
-> SimpleExpr
-> SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> (a, VCS)
-> (a, VCS)
add_assertion FContext
ctxt SimpleExpr
rip SimpleExpr
assertion Int
si0 SimpleExpr
a1 Int
si1
      --trace ("ASSERTION (WRITE@" ++ show rip ++ "): SEPARATION BETWEEN " ++ show (assertion,si0,a0) ++ " and " ++ show (a1,si1)) $
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Separated
    else
      --if do_trace a0 a1 then trace ("PRECONDITION (WRITE): OVERLAP BETWEEN " ++ show (a0,si0) ++ " and " ++ show (a1,si1)) $ return Overlap else
      SeparationStatus -> StateT (Pred, VCS) Identity SeparationStatus
forall (m :: * -> *) a. Monad m => a -> m a
return SeparationStatus
Overlap

  address :: MemWriteIdentifier -> Maybe (GenericAddress Register)
address (MemWriteInstruction Word64
_ (Memory GenericAddress Register
addr Int
si) SimpleExpr
_) = GenericAddress Register -> Maybe (GenericAddress Register)
forall a. a -> Maybe a
Just GenericAddress Register
addr
  address MemWriteIdentifier
_                                          = Maybe (GenericAddress Register)
forall a. Maybe a
Nothing



  do_trace :: p -> p -> Bool
do_trace p
a0 p
a1 = Bool
True -- srcs_of_expr ctxt a0 /= srcs_of_expr ctxt a1 


  do_write :: SimpleExpr -> Int -> SimpleExpr -> [(StatePart, SimpleExpr)] -> State (Pred,VCS) [(StatePart, SimpleExpr)]
  do_write :: SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write SimpleExpr
a0 Int
si0 SimpleExpr
v []                      =  do
    let sps' :: [StatePart]
sps'  = ((SimpleExpr, Int) -> StatePart)
-> [(SimpleExpr, Int)] -> [StatePart]
forall a b. (a -> b) -> [a] -> [b]
map ((SimpleExpr -> Int -> StatePart) -> (SimpleExpr, Int) -> StatePart
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SimpleExpr -> Int -> StatePart
SP_Mem) ([(SimpleExpr, Int)] -> [StatePart])
-> [(SimpleExpr, Int)] -> [StatePart]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> Int -> [(SimpleExpr, Int)]
forall b. Num b => FContext -> SimpleExpr -> b -> [(SimpleExpr, b)]
expr_to_mem_addresses FContext
ctxt SimpleExpr
a0 Int
si0
    [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(StatePart, SimpleExpr)]
 -> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)])
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> a -> b
$ (StatePart -> (StatePart, SimpleExpr))
-> [StatePart] -> [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\StatePart
sp' -> (StatePart
sp', FContext -> SimpleExpr -> SimpleExpr
trim_expr FContext
ctxt SimpleExpr
v)) [StatePart]
sps'
  do_write SimpleExpr
a0 Int
si0 SimpleExpr
v (eq :: (StatePart, SimpleExpr)
eq@(SP_Reg Register
_,SimpleExpr
_):[(StatePart, SimpleExpr)]
mem)   = ((:) (StatePart, SimpleExpr)
eq) ([(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)])
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write SimpleExpr
a0 Int
si0 SimpleExpr
v [(StatePart, SimpleExpr)]
mem
  do_write SimpleExpr
a0 Int
si0 SimpleExpr
v (eq :: (StatePart, SimpleExpr)
eq@(SP_Mem SimpleExpr
a1 Int
si1,SimpleExpr
e):[(StatePart, SimpleExpr)]
mem) = do
    SeparationStatus
sep <- SimpleExpr
-> Int
-> SimpleExpr
-> Int
-> StateT (Pred, VCS) Identity SeparationStatus
is_separate SimpleExpr
a0 Int
si0 SimpleExpr
a1 Int
si1
    case SeparationStatus
sep of
      SeparationStatus
Alias     -> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(StatePart, SimpleExpr)]
 -> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)])
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a0 Int
si0,FContext -> SimpleExpr -> SimpleExpr
trim_expr FContext
ctxt SimpleExpr
v) (StatePart, SimpleExpr)
-> [(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)]
forall a. a -> [a] -> [a]
: [(StatePart, SimpleExpr)]
mem
      SeparationStatus
Separated -> ((:) ((StatePart, SimpleExpr)
 -> [(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)])
-> (StatePart, SimpleExpr)
-> [(StatePart, SimpleExpr)]
-> [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> a -> b
$ (StatePart, SimpleExpr)
eq) ([(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)])
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write SimpleExpr
a0 Int
si0 SimpleExpr
v [(StatePart, SimpleExpr)]
mem
      SeparationStatus
Enclosed  -> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(StatePart, SimpleExpr)]
 -> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)])
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> Int -> StatePart
SP_Mem SimpleExpr
a1 Int
si1,[Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs ([Char]
"write enclosure") FContext
ctxt [SimpleExpr
e,SimpleExpr
v]) (StatePart, SimpleExpr)
-> [(StatePart, SimpleExpr)] -> [(StatePart, SimpleExpr)]
forall a. a -> [a] -> [a]
: [(StatePart, SimpleExpr)]
mem
      SeparationStatus
Disclosed -> SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write SimpleExpr
a0 Int
si0 SimpleExpr
v [(StatePart, SimpleExpr)]
mem
      SeparationStatus
Overlap   -> SimpleExpr
-> Int
-> SimpleExpr
-> [(StatePart, SimpleExpr)]
-> StateT (Pred, VCS) Identity [(StatePart, SimpleExpr)]
do_write ([Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs ([Char]
"write overlap adddres") FContext
ctxt [SimpleExpr
a0,SimpleExpr
a1]) Int
si0 ([Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_exprs ([Char]
"write overlap value") FContext
ctxt [SimpleExpr
e,SimpleExpr
v]) [(StatePart, SimpleExpr)]
mem





-- * Operands  
-- | Read from an operand of an instruction
read_operand :: FContext -> X86.Operand -> State (Pred,VCS) SimpleExpr
read_operand :: FContext -> Operand -> State (Pred, VCS) SimpleExpr
read_operand FContext
ctxt (Storage Register
r)          = FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
r
read_operand FContext
ctxt (Immediate Word64
w)        = SimpleExpr -> State (Pred, VCS) SimpleExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleExpr -> State (Pred, VCS) SimpleExpr)
-> SimpleExpr -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> SimpleExpr
SE_Immediate Word64
w
read_operand FContext
ctxt (EffectiveAddress GenericAddress Register
a) = FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a
read_operand FContext
ctxt (Memory GenericAddress Register
a Int
si)        = FContext -> Operand -> State (Pred, VCS) SimpleExpr
read_mem FContext
ctxt (Operand -> State (Pred, VCS) SimpleExpr)
-> Operand -> State (Pred, VCS) SimpleExpr
forall a b. (a -> b) -> a -> b
$ GenericAddress Register -> Int -> Operand
forall storage.
GenericAddress storage -> Int -> GenericOperand storage
Memory GenericAddress Register
a Int
si

-- | Write to an operand of an instruction 
write_operand ::
 FContext                -- ^ The context
 -> Word64               -- ^ The address of the instruction, used to build a `MemWriteIdentifier`
 -> X86.Operand          -- ^ The operand
 -> SimpleExpr           -- ^ The value to be written
 -> State (Pred,VCS) ()
write_operand :: FContext
-> Word64
-> Operand
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_operand FContext
ctxt Word64
instr_a (Storage Register
r)   SimpleExpr
v = FContext
-> Word64
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_reg FContext
ctxt Word64
instr_a Register
r SimpleExpr
v
write_operand FContext
ctxt Word64
instr_a (Memory GenericAddress Register
a Int
si) SimpleExpr
v = do
  SimpleExpr
resolved_address <- FContext -> GenericAddress Register -> State (Pred, VCS) SimpleExpr
resolve_address FContext
ctxt GenericAddress Register
a
  FContext
-> MemWriteIdentifier
-> SimpleExpr
-> Int
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_mem FContext
ctxt (Word64 -> Operand -> SimpleExpr -> MemWriteIdentifier
MemWriteInstruction Word64
instr_a (GenericAddress Register -> Int -> Operand
forall storage.
GenericAddress storage -> Int -> GenericOperand storage
Memory GenericAddress Register
a Int
si) SimpleExpr
resolved_address) SimpleExpr
resolved_address Int
si SimpleExpr
v
write_operand FContext
ctxt Word64
instr_a Operand
op1 SimpleExpr
e           = [Char]
-> StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ()
forall a. [Char] -> a -> a
trace ([Char]
"Writing to immediate operand: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Operand, SimpleExpr) -> [Char]
forall a. Show a => a -> [Char]
show (Operand
op1,SimpleExpr
e)) (StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ())
-> StateT (Pred, VCS) Identity () -> StateT (Pred, VCS) Identity ()
forall a b. (a -> b) -> a -> b
$ () -> StateT (Pred, VCS) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()-- Should not happen
 

mk_reg_write_identifier :: Word64 -> Register -> MemWriteIdentifier
mk_reg_write_identifier Word64
instr_a Register
r = Word64 -> Operand -> SimpleExpr -> MemWriteIdentifier
MemWriteInstruction Word64
instr_a (Register -> Operand
forall storage. storage -> GenericOperand storage
Storage Register
r) (StatePart -> SimpleExpr
SE_StatePart (StatePart -> SimpleExpr) -> StatePart -> SimpleExpr
forall a b. (a -> b) -> a -> b
$ Register -> StatePart
SP_Reg Register
r)


-- * Stateparts 
-- | Read from an statepart
read_sp :: FContext -> StatePart -> State (Pred,VCS) SimpleExpr
read_sp :: FContext -> StatePart -> State (Pred, VCS) SimpleExpr
read_sp FContext
ctxt (SP_Reg Register
r)          = FContext -> Register -> State (Pred, VCS) SimpleExpr
read_reg FContext
ctxt Register
r
read_sp FContext
ctxt (SP_Mem SimpleExpr
a Int
si)       = FContext
-> Maybe Operand
-> SimpleExpr
-> Int
-> State (Pred, VCS) SimpleExpr
read_from_address FContext
ctxt Maybe Operand
forall a. Maybe a
Nothing SimpleExpr
a Int
si

-- | Write to a statepart
write_sp :: 
  FContext                                        -- ^ The context
  -> Word64                                       -- ^ The address of the instruction
  -> (Word64 -> StatePart -> MemWriteIdentifier)  -- ^ Given a statepart, build a memwrite identifier
  -> (StatePart,SimpleExpr)                       -- ^ The statepart and the value to be written
  -> State (Pred,VCS) ()
write_sp :: FContext
-> Word64
-> (Word64 -> StatePart -> MemWriteIdentifier)
-> (StatePart, SimpleExpr)
-> StateT (Pred, VCS) Identity ()
write_sp FContext
ctxt Word64
i_a Word64 -> StatePart -> MemWriteIdentifier
mk_mid (sp :: StatePart
sp @(SP_Reg Register
r),SimpleExpr
v)   = FContext
-> Word64
-> Register
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_reg FContext
ctxt Word64
i_a Register
r SimpleExpr
v
write_sp FContext
ctxt Word64
i_a Word64 -> StatePart -> MemWriteIdentifier
mk_mid (sp :: StatePart
sp@(SP_Mem SimpleExpr
a Int
si),SimpleExpr
v) = FContext
-> MemWriteIdentifier
-> SimpleExpr
-> Int
-> SimpleExpr
-> StateT (Pred, VCS) Identity ()
write_mem FContext
ctxt (Word64 -> StatePart -> MemWriteIdentifier
mk_mid Word64
i_a StatePart
sp) SimpleExpr
a Int
si SimpleExpr
v