{-# LANGUAGE DeriveGeneric, FlexibleContexts  #-}

module WithAbstractSymbolicValues.Sstate where

import Base


import WithAbstractSymbolicValues.Class

import Data.Size
import Data.X86.Register
import Data.X86.Instruction
import Data.VerificationCondition
import Data.SymbolicExpression (FlagStatus(..)) -- TODO


import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified Data.Set.NonEmpty as NES
import Data.List

import Control.Monad.State.Strict hiding (join)

import GHC.Generics (Generic)
import Control.DeepSeq
import qualified Data.Serialize as Cereal






execSstate :: State (Sstate v p, VCS v) b -> Sstate v p -> Sstate v p
execSstate :: forall v p b.
State (Sstate v p, VCS v) b -> Sstate v p -> Sstate v p
execSstate State (Sstate v p, VCS v) b
m Sstate v p
s = (Sstate v p, VCS v) -> Sstate v p
forall a b. (a, b) -> a
fst ((Sstate v p, VCS v) -> Sstate v p)
-> (Sstate v p, VCS v) -> Sstate v p
forall a b. (a -> b) -> a -> b
$ State (Sstate v p, VCS v) b
-> (Sstate v p, VCS v) -> (Sstate v p, VCS v)
forall s a. State s a -> s -> s
execState State (Sstate v p, VCS v) b
m (Sstate v p
s,VCS v
forall a. Set a
S.empty)

evalSstate :: State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate :: forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate State (Sstate v p, VCS v) a
m Sstate v p
s = State (Sstate v p, VCS v) a -> (Sstate v p, VCS v) -> a
forall s a. State s a -> s -> a
evalState State (Sstate v p, VCS v) a
m (Sstate v p
s,VCS v
forall a. Set a
S.empty)



-- | Read from a register
sread_rreg :: ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
r (Sstate v p
s,b
_) = 
  case Register -> Map Register v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Register
r (Sstate v p -> Map Register v
forall v p. Sstate v p -> Map Register v
sregs Sstate v p
s) of
    Maybe v
Nothing -> ctxt -> Register -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> v
smk_init_reg_value ctxt
ctxt Register
r
    Just v
v  -> v
v



sread_reg :: WithAbstractSymbolicValues ctxt v p => ctxt -> Register -> State (Sstate v p,VCS v) v
sread_reg :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt   (Reg8  GPR
r RegHalf
HalfL) = (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 8" (SymbolicOperation v -> v) -> (v -> SymbolicOperation v) -> v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
8) (v -> v)
-> StateT (Sstate v p, VCS v) Identity v
-> StateT (Sstate v p, VCS v) Identity v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt (Register -> (Sstate v p, VCS v) -> v)
-> Register -> (Sstate v p, VCS v) -> v
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
r)
sread_reg ctxt
ctxt   (Reg8  GPR
r RegHalf
HalfH) = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt String
"read_reg halfR"
sread_reg ctxt
ctxt   (Reg16 GPR
r)       = (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 16" (SymbolicOperation v -> v) -> (v -> SymbolicOperation v) -> v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
16) (v -> v)
-> StateT (Sstate v p, VCS v) Identity v
-> StateT (Sstate v p, VCS v) Identity v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt (Register -> (Sstate v p, VCS v) -> v)
-> Register -> (Sstate v p, VCS v) -> v
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
r)
sread_reg ctxt
ctxt   (Reg32 GPR
r)       = (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 32" (SymbolicOperation v -> v) -> (v -> SymbolicOperation v) -> v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
32) (v -> v)
-> StateT (Sstate v p, VCS v) Identity v
-> StateT (Sstate v p, VCS v) Identity v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt (Register -> (Sstate v p, VCS v) -> v)
-> Register -> (Sstate v p, VCS v) -> v
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
r)
sread_reg ctxt
ctxt r :: Register
r@(Reg64 GPR
_)       = ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
r
sread_reg ctxt
ctxt r :: Register
r@(Reg128 SSEReg
_)      = ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
r
sread_reg ctxt
ctxt r :: Register
r@(RegSeg SReg
_)      = ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
r
sread_reg ctxt
ctxt r :: Register
r@(Register
RegTemp)       = ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
r
sread_reg ctxt
ctxt r :: Register
r@(RegFPU FPUReg
_)      = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt String
"read_reg ST(_)"
sread_reg ctxt
ctxt Register
r                 = String -> StateT (Sstate v p, VCS v) Identity v
forall a. HasCallStack => String -> a
error (String -> StateT (Sstate v p, VCS v) Identity v)
-> String -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ String
"READING REG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Register -> String
forall a. Show a => a -> String
show Register
r






-- | Write to a register
swrite_rreg :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Register -> v -> State (Sstate v p,VCS v) () 
swrite_rreg :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i (RegFPU FPUReg
_) v
v = () -> StateT (Sstate v p, VCS v) Identity ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
swrite_rreg ctxt
ctxt String
i Register
r          v
v = do
  (Sstate v p
s,VCS v
vcs) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
  -- let tr = if (r == Reg64 RSP || r == Reg64 RBP) && v == top ctxt "" then traceShow (show r ++ "WRITE", v, i, s) else id
  (Sstate v p, VCS v) -> StateT (Sstate v p, VCS v) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> StateT (Sstate v p, VCS v) Identity ())
-> (Sstate v p, VCS v) -> StateT (Sstate v p, VCS v) Identity ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s {sregs = M.insert r v (sregs s), sflags = clean_flg (SSP_Reg r) (sflags s) }, VCS v
vcs)


soverwrite_reg :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Bool -> Register -> v -> State (Sstate v p,VCS v) ()
soverwrite_reg :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> Bool -> Register -> v -> State (Sstate v p, VCS v) ()
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg8 GPR
_ RegHalf
HalfL) v
v = do
  let rr :: Register
rr = Register -> Register
real_reg Register
r
  v
curr_v <- ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
rr
  let v' :: SymbolicOperation v
v' = if Bool
use_existing_value then Int -> v -> v -> SymbolicOperation v
forall v. Int -> v -> v -> SymbolicOperation v
SO_Overwrite Int
8 v
curr_v (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg 8" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
8 v
v) else Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
8 v
v
  ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
rr (v -> State (Sstate v p, VCS v) ())
-> v -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg' 8" SymbolicOperation v
v'
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg8 GPR
_ RegHalf
HalfH) v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i (Register -> Register
real_reg Register
r) (ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt String
"RegHalfH")
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg16 GPR
_)      v
v = do
  let rr :: Register
rr = Register -> Register
real_reg Register
r
  v
curr_v <- ((Sstate v p, VCS v) -> v) -> StateT (Sstate v p, VCS v) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> v)
 -> StateT (Sstate v p, VCS v) Identity v)
-> ((Sstate v p, VCS v) -> v)
-> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, VCS v) -> v
forall {ctxt} {v} {p} {p} {b}.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> (Sstate v p, b) -> v
sread_rreg ctxt
ctxt Register
rr
  let v' :: SymbolicOperation v
v' = if Bool
use_existing_value then Int -> v -> v -> SymbolicOperation v
forall v. Int -> v -> v -> SymbolicOperation v
SO_Overwrite Int
16 v
curr_v (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg 16" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
16 v
v) else Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
16 v
v
  ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
rr (v -> State (Sstate v p, VCS v) ())
-> v -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg' 16" SymbolicOperation v
v'
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg32 GPR
_)      v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i (Register -> Register
real_reg Register
r) (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg 32" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Int -> v -> SymbolicOperation v
forall v. Int -> v -> SymbolicOperation v
SO_Bit Int
32 v
v)
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg64 GPR
_)      v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
r v
v
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Reg128 SSEReg
_)     v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
r v
v
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(RegSeg SReg
_)     v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
r v
v
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(Register
RegTemp)      v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
i Register
r v
v
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value r :: Register
r@(RegFPU FPUReg
_)     v
v = () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
soverwrite_reg ctxt
ctxt String
i Bool
use_existing_value Register
r                v
v = String -> State (Sstate v p, VCS v) ()
forall a. HasCallStack => String -> a
error (String -> State (Sstate v p, VCS v) ())
-> String -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ Register -> String
forall a. Show a => a -> String
show Register
r


swrite_reg :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Register -> v -> State (Sstate v p,VCS v) ()
swrite_reg :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
i = ctxt
-> String -> Bool -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> Bool -> Register -> v -> State (Sstate v p, VCS v) ()
soverwrite_reg ctxt
ctxt String
i Bool
True


-- | Read from memory
sread_mem :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> v -> Maybe ByteSize -> State (Sstate v p,VCS v) v
--sread_mem ctxt msg a si | trace ("sread_mem: "++ show (a,si)) False = error "trace"
sread_mem :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> v -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem ctxt
ctxt String
msg v
a Maybe ByteSize
si = do
  (Sstate v p
p,VCS v
_) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
  let ptrs :: Set p
ptrs = ctxt -> String -> v -> Set p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt (String
"sread_mem" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, v, Maybe ByteSize, Sstate v p) -> String
forall a. Show a => a -> String
show (String
msg,v
a,Maybe ByteSize
si,Sstate v p
p)) v
a
  if Set p -> Bool
forall a. Set a -> Bool
S.null Set p
ptrs then
    v -> State (Sstate v p, VCS v) v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, VCS v) v)
-> v -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt (String -> v) -> String -> v
forall a b. (a -> b) -> a -> b
$ String
"read_mem from top"
  else do
    [v]
vs <- (p -> State (Sstate v p, VCS v) v)
-> [p] -> StateT (Sstate v p, VCS v) Identity [v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\p
ptr -> ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem_from_ptr ctxt
ctxt String
msg p
ptr Maybe ByteSize
si) ([p] -> StateT (Sstate v p, VCS v) Identity [v])
-> [p] -> StateT (Sstate v p, VCS v) Identity [v]
forall a b. (a -> b) -> a -> b
$ Set p -> [p]
forall a. Set a -> [a]
S.toList Set p
ptrs
    v -> State (Sstate v p, VCS v) v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, VCS v) v)
-> v -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nRead join:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Set p, [v]) -> String
forall a. Show a => a -> String
show (Set p
ptrs,[v]
vs)) [v]
vs

sread_mem_from_ptr :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> p -> Maybe ByteSize -> State (Sstate v p,VCS v) v
--sread_mem_from_ptr ctxt msg a si | trace ("sread_mem_from_ptr: "++ show (a,si)) False = error "trace"
sread_mem_from_ptr :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem_from_ptr ctxt
ctxt String
msg p
a Maybe ByteSize
si = Maybe v -> StateT (Sstate v p, VCS v) Identity (Maybe v)
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (ctxt -> p -> Maybe ByteSize -> Maybe v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> Maybe v
sread_from_ro_data ctxt
ctxt p
a Maybe ByteSize
si) StateT (Sstate v p, VCS v) Identity (Maybe v)
-> StateT (Sstate v p, VCS v) Identity v
-> StateT (Sstate v p, VCS v) Identity v
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m a -> m a
`orElseM` p -> StateT (Sstate v p, VCS v) Identity v
forall {m :: * -> *} {b}. MonadState (Sstate v p, b) m => p -> m v
sread_mem' p
a 
 where
  sread_mem' :: p -> m v
sread_mem' p
a = do
    (Sstate v p
s,b
vcs) <- m (Sstate v p, b)
forall s (m :: * -> *). MonadState s m => m s
get
    case (((p, Maybe ByteSize), v) -> Bool)
-> [((p, Maybe ByteSize), v)] -> Maybe ((p, Maybe ByteSize), v)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\((p
a0,Maybe ByteSize
si0),v
v0) -> (p
a0,Maybe ByteSize
si0) (p, Maybe ByteSize) -> (p, Maybe ByteSize) -> Bool
forall a. Eq a => a -> a -> Bool
== (p
a,Maybe ByteSize
si) Bool -> Bool -> Bool
&& ctxt -> p -> Maybe ByteSize -> v -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> v -> Bool
ssensitive ctxt
ctxt p
a0 Maybe ByteSize
si0 v
v0) ([((p, Maybe ByteSize), v)] -> Maybe ((p, Maybe ByteSize), v))
-> [((p, Maybe ByteSize), v)] -> Maybe ((p, Maybe ByteSize), v)
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)])
-> Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall a b. (a -> b) -> a -> b
$ Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s of
      Just ((p
a0,Maybe ByteSize
si0),v
v0) -> v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return v
v0
      Maybe ((p, Maybe ByteSize), v)
_ -> p -> m v
forall {b} {m :: * -> *}. MonadState (Sstate v p, b) m => p -> m v
sread_mem'' p
a
  sread_mem'' :: p -> m v
sread_mem'' p
a = do
    (Sstate v p
s,b
vcs) <- m (Sstate v p, b)
forall s (m :: * -> *). MonadState s m => m s
get
    let (Map (p, Maybe ByteSize) v
_,Map (p, Maybe ByteSize) v
overlap) = ((p, Maybe ByteSize) -> v -> Bool)
-> Map (p, Maybe ByteSize) v
-> (Map (p, Maybe ByteSize) v, Map (p, Maybe ByteSize) v)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partitionWithKey (p, Maybe ByteSize) -> v -> Bool
ssep (Map (p, Maybe ByteSize) v
 -> (Map (p, Maybe ByteSize) v, Map (p, Maybe ByteSize) v))
-> Map (p, Maybe ByteSize) v
-> (Map (p, Maybe ByteSize) v, Map (p, Maybe ByteSize) v)
forall a b. (a -> b) -> a -> b
$ Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s
    if Map (p, Maybe ByteSize) v -> Int
forall k a. Map k a -> Int
M.size Map (p, Maybe ByteSize) v
overlap Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
      let [((p
a0,Maybe ByteSize
si0),v
v0)] = Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (p, Maybe ByteSize) v
overlap in
        if ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
salias ctxt
ctxt p
a Maybe ByteSize
si p
a0 Maybe ByteSize
si0 then
          v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return v
v0
        else if ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
senclosed ctxt
ctxt p
a Maybe ByteSize
si p
a0 Maybe ByteSize
si0 then
          v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"read_mem (enclosure)" v
v0
        else
          v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ p -> Sstate v p -> Map (p, Maybe ByteSize) v -> v
forall {k} {a}. (Show k, Show a) => p -> a -> Map k v -> v
read_from_overlap p
a Sstate v p
s Map (p, Maybe ByteSize) v
overlap
    else
      v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ p -> Sstate v p -> Map (p, Maybe ByteSize) v -> v
forall {k} {a}. (Show k, Show a) => p -> a -> Map k v -> v
read_from_overlap p
a Sstate v p
s Map (p, Maybe ByteSize) v
overlap
 
  ssep :: (p, Maybe ByteSize) -> v -> Bool
ssep (p
a0,Maybe ByteSize
si0) v
v0 = ((p
a,Maybe ByteSize
si) (p, Maybe ByteSize) -> (p, Maybe ByteSize) -> Bool
forall a. Eq a => a -> a -> Bool
/= (p
a0,Maybe ByteSize
si0) Bool -> Bool -> Bool
&& ctxt -> p -> Maybe ByteSize -> v -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> v -> Bool
ssensitive ctxt
ctxt p
a0 Maybe ByteSize
si0 v
v0) Bool -> Bool -> Bool
|| ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
sseparate ctxt
ctxt String
"read" p
a0 Maybe ByteSize
si0 p
a Maybe ByteSize
si

  read_from_overlap :: p -> a -> Map k v -> v
read_from_overlap p
a a
s Map k v
overlap
    | Map k v -> Int
forall k a. Map k a -> Int
M.size Map k v
overlap Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = ctxt -> String -> p -> Maybe ByteSize -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> p -> Maybe ByteSize -> v
smk_init_mem_value ctxt
ctxt (String
"\nmaking init mem value:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (p, Maybe ByteSize) -> String
forall a. Show a => a -> String
show (p
a,Maybe ByteSize
si) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) p
a Maybe ByteSize
si
    | Bool
otherwise = -- error ("Overlapping read:\nReading from: " ++ show (a,si,S.map fst overlap) ++ "\nIn state:\n" ++ show s) 
                  ctxt -> String -> v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt (String -> p -> a -> Map k v -> String
forall {a} {a} {a}.
(Show a, Show a, Show a) =>
String -> a -> a -> a -> String
msg' String
"widen" p
a a
s Map k v
overlap) (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String -> p -> a -> Map k v -> String
forall {a} {a} {a}.
(Show a, Show a, Show a) =>
String -> a -> a -> a -> String
msg' String
"joining" p
a a
s Map k v
overlap) (Map k v -> [v]
forall k a. Map k a -> [a]
M.elems Map k v
overlap)

  msg' :: String -> a -> a -> a -> String
msg' String
name a
a a
s a
overlap = String
"Read " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, Maybe ByteSize) -> String
forall a. Show a => a -> String
show (a
a,Maybe ByteSize
si) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
overlap String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
msg



-- | Write to memory
swrite_mem :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p,VCS v) ()
swrite_mem :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem ctxt
ctxt Bool
use_existing_value v
a Maybe ByteSize
si v
v = do
  (Sstate v p
p,VCS v
_) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
  let ptrs :: Set p
ptrs = ctxt -> String -> v -> Set p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt (String
"swrite_mem\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++Sstate v p -> String
forall a. Show a => a -> String
show Sstate v p
p) v
a
  if Set p -> Bool
forall a. Set a -> Bool
S.null Set p
ptrs then
    --error ("TOP: writing to " ++ show (a,si) ++ "\nIn state:\n" ++ show p)
    --trace ("TOP: writing to " ++ show (a,si) ++ "\nIn state:\n" ++ show p) $
    () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO ADD VC
  else
    (p -> State (Sstate v p, VCS v) ())
-> Set p -> State (Sstate v p, VCS v) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\p
ptr -> ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem_to_ptr ctxt
ctxt Bool
use_existing_value p
ptr Maybe ByteSize
si v
v) Set p
ptrs

swrite_mem_to_ptr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p,VCS v) ()
swrite_mem_to_ptr :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem_to_ptr ctxt
ctxt Bool
use_existing_value p
a Maybe ByteSize
si v
v = do
  ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, VCS v) -> (Sstate v p, VCS v))
 -> State (Sstate v p, VCS v) ())
-> ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ \(Sstate v p
s,VCS v
vcs) -> (Sstate v p
s { sflags = clean_flg (SSP_Mem (simmediate ctxt 0) 0) (sflags s) }, VCS v
vcs)
  (Sstate v p
s,VCS v
vcs) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get

  let ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosed_by,[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) = Map (p, Maybe ByteSize) v
-> p
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
do_partitioning (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s) p
a
  if [((p, Maybe ByteSize), v)]
equal [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then
    (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s { smem = combine [ [((a,si),v)], enclosed_by, encloses, separate, overlap] }, VCS v
vcs)
  else if [((p, Maybe ByteSize), v)]
enclosed_by [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then do
    (Sstate v p
p,VCS v
_) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
    let v' :: v
v' = ctxt -> String -> v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"write_mem (enclosure)" (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
"MemWrite (enclosure)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (p, Maybe ByteSize, [((p, Maybe ByteSize), v)]) -> String
forall a. Show a => a -> String
show (p
a,Maybe ByteSize
si,[((p, Maybe ByteSize), v)]
enclosed_by) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sstate v p -> String
forall a. Show a => a -> String
show Sstate v p
p) (v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: (((p, Maybe ByteSize), v) -> v)
-> [((p, Maybe ByteSize), v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map ((p, Maybe ByteSize), v) -> v
forall a b. (a, b) -> b
snd [((p, Maybe ByteSize), v)]
enclosed_by)
    (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s { smem = combine [ [(fst $ head enclosed_by,v')], encloses, separate, overlap] }, VCS v
vcs)
  else if [((p, Maybe ByteSize), v)]
encloses [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then do
    let v' :: v
v' = ctxt -> String -> v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"write_mem (encloses)" (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt String
"MemWrite (encloses)" (v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: (((p, Maybe ByteSize), v) -> v)
-> [((p, Maybe ByteSize), v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map ((p, Maybe ByteSize), v) -> v
forall a b. (a, b) -> b
snd [((p, Maybe ByteSize), v)]
encloses)
    (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s { smem = combine [ [((a,si),v')], separate, overlap] }, VCS v
vcs)
  else if [((p, Maybe ByteSize), v)]
overlap [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
    (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s { smem = combine [ [((a,si),v)],  separate ] }, VCS v
vcs)
  else let m' :: [((p, Maybe ByteSize), v)]
m' = ctxt -> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
merge ctxt
ctxt ([((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)])
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a b. (a -> b) -> a -> b
$ ((p
a,Maybe ByteSize
si),v
v)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
overlap in
    --trace ("Overlapping write:\nWriting to: " ++ show (a,si,map fst overlap) ++ "\nm = " ++ show m' ++ "\nIn state:\n" ++ show s) $
    (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s { smem = combine [ m',  separate ] }, VCS v
vcs)
 where
  combine :: [[((p, Maybe ByteSize), a)]] -> Map (p, Maybe ByteSize) a
combine = [((p, Maybe ByteSize), a)] -> Map (p, Maybe ByteSize) a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((p, Maybe ByteSize), a)] -> Map (p, Maybe ByteSize) a)
-> ([[((p, Maybe ByteSize), a)]] -> [((p, Maybe ByteSize), a)])
-> [[((p, Maybe ByteSize), a)]]
-> Map (p, Maybe ByteSize) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[((p, Maybe ByteSize), a)]] -> [((p, Maybe ByteSize), a)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

  do_partitioning :: Map (p, Maybe ByteSize) v
-> p
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
do_partitioning Map (p, Maybe ByteSize) v
m p
a = ((p, Maybe ByteSize)
 -> v
 -> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
     [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
     [((p, Maybe ByteSize), v)])
 -> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
     [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
     [((p, Maybe ByteSize), v)]))
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
-> Map (p, Maybe ByteSize) v
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey (p
-> (p, Maybe ByteSize)
-> v
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
do_partition p
a) ([],[],[],[],[]) Map (p, Maybe ByteSize) v
m
  do_partition :: p
-> (p, Maybe ByteSize)
-> v
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
-> ([((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)], [((p, Maybe ByteSize), v)],
    [((p, Maybe ByteSize), v)])
do_partition p
a (p
a0,Maybe ByteSize
si0) v
v0 ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) 
    | ctxt -> p -> Maybe ByteSize -> v -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> v -> Bool
ssensitive ctxt
ctxt          p
a0 Maybe ByteSize
si0 v
v0   = ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) -- TODO: VCS v, especially when local pointer
    | ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
salias     ctxt
ctxt          p
a0 Maybe ByteSize
si0 p
a Maybe ByteSize
si = (((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) 
    | ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
senclosed  ctxt
ctxt          p
a Maybe ByteSize
si p
a0 Maybe ByteSize
si0 = ([((p, Maybe ByteSize), v)]
equal,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) 
    | ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
senclosed  ctxt
ctxt          p
a0 Maybe ByteSize
si0 p
a Maybe ByteSize
si = ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap)
    | ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
sseparate  ctxt
ctxt String
"wwrite" p
a Maybe ByteSize
si p
a0 Maybe ByteSize
si0 = ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap) 
    | Bool -> Bool
not Bool
use_existing_value               = ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
separate,[((p, Maybe ByteSize), v)]
overlap)
    | Bool
otherwise                            = ([((p, Maybe ByteSize), v)]
equal,[((p, Maybe ByteSize), v)]
enclosing,[((p, Maybe ByteSize), v)]
encloses,[((p, Maybe ByteSize), v)]
separate,((p
a0,Maybe ByteSize
si0),v
v0)((p, Maybe ByteSize), v)
-> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
forall a. a -> [a] -> [a]
:[((p, Maybe ByteSize), v)]
overlap) 

  merge ::  WithAbstractSymbolicValues ctxt v p => ctxt -> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
  merge :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> [((p, Maybe ByteSize), v)] -> [((p, Maybe ByteSize), v)]
merge ctxt
ctxt [((p, Maybe ByteSize), v)]
m =
    let ptrs :: [p]
ptrs = ctxt -> [p] -> [p]
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> [p] -> [p]
sjoin_pointers ctxt
ctxt ([p] -> [p]) -> [p] -> [p]
forall a b. (a -> b) -> a -> b
$ (((p, Maybe ByteSize), v) -> p)
-> [((p, Maybe ByteSize), v)] -> [p]
forall a b. (a -> b) -> [a] -> [b]
map ((p, Maybe ByteSize) -> p
forall a b. (a, b) -> a
fst ((p, Maybe ByteSize) -> p)
-> (((p, Maybe ByteSize), v) -> (p, Maybe ByteSize))
-> ((p, Maybe ByteSize), v)
-> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((p, Maybe ByteSize), v) -> (p, Maybe ByteSize)
forall a b. (a, b) -> a
fst) [((p, Maybe ByteSize), v)]
m
        v' :: v
v'   = ctxt -> String -> v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"write_mem (overlap)" (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt String
"MemWrite (values)" ([v] -> v) -> [v] -> v
forall a b. (a -> b) -> a -> b
$ (((p, Maybe ByteSize), v) -> v)
-> [((p, Maybe ByteSize), v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map ((p, Maybe ByteSize), v) -> v
forall a b. (a, b) -> b
snd [((p, Maybe ByteSize), v)]
m in
      (p -> ((p, Maybe ByteSize), v))
-> [p] -> [((p, Maybe ByteSize), v)]
forall a b. (a -> b) -> [a] -> [b]
map (\p
ptr -> ((p
ptr,Maybe ByteSize
forall {a}. Maybe a
unknownSize),v
v')) [p]
ptrs



-- v is bogus, but needed for getting the type checker to accept this. Don't know why. 
swrite_flags :: WithAbstractSymbolicValues ctxt v p => ctxt -> v -> Instruction -> State (Sstate v p,VCS v) ()
swrite_flags :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> v -> Instruction -> State (Sstate v p, VCS v) ()
swrite_flags ctxt
ctxt v
v Instruction
i = do
  (Sstate v p
s,VCS v
vcs) <- StateT (Sstate v p, VCS v) Identity (Sstate v p, VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
  (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, VCS v) -> State (Sstate v p, VCS v) ())
-> (Sstate v p, VCS v) -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s {sflags = sflg_semantics ctxt v i (sflags s)}, VCS v
vcs)


-- If the given StatePart is overwritten, does that taint the current flag status?
-- If so, set flagstatus to None, otherwise keep it.
clean_flg :: SStatePart p -> FlagStatus -> FlagStatus
clean_flg :: forall p. SStatePart p -> FlagStatus -> FlagStatus
clean_flg SStatePart p
sp FlagStatus
None               = FlagStatus
None
clean_flg SStatePart p
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 (Op_Reg Register
r)             = 
    case SStatePart p
sp of
      SSP_Reg Register
r' -> Register -> Register
real_reg Register
r' Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
== Register -> Register
real_reg Register
r
      SStatePart p
_          -> Bool
False
      
  is_tainted (Op_Imm Immediate
_)             = Bool
False
  is_tainted (Op_Mem BitSize
_ BitSize
_ Register
_ Register
_ Word8
_ Int
_ Maybe SReg
_) =
    case SStatePart p
sp of
      SSP_Mem p
_ Int
_ -> Bool
True
      SStatePart p
_          -> Bool
False





write_sp :: WithAbstractSymbolicValues ctxt v p => ctxt -> SStatePart p -> v -> State (Sstate v p, VCS v) ()
write_sp :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> SStatePart p -> v -> State (Sstate v p, VCS v) ()
write_sp ctxt
ctxt (SSP_Reg Register
r)    v
v = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
"write_sp" Register
r v
v
write_sp ctxt
ctxt (SSP_Mem p
a Int
si) v
v = ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem_to_ptr ctxt
ctxt Bool
True p
a (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si) v
v

read_sp :: WithAbstractSymbolicValues ctxt v p => ctxt -> SStatePart p -> State (Sstate v p, VCS v) v
read_sp :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> SStatePart p -> State (Sstate v p, VCS v) v
read_sp ctxt
ctxt (SSP_Reg Register
r)    = ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt Register
r
read_sp ctxt
ctxt (SSP_Mem p
a Int
si) = ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem_from_ptr ctxt
ctxt String
"read_sp" p
a (Maybe ByteSize -> State (Sstate v p, VCS v) v)
-> Maybe ByteSize -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
si)