{-# LANGUAGE DeriveGeneric, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}

module Generic.SymbolicConstituents where

import qualified X86.Register as Reg
import qualified X86.Operand as X86
import qualified X86.Instruction as X86
import qualified X86.Address as X86
import qualified X86.Opcode as X86
import X86.Instruction (addressof)

import Data.JumpTarget
import Data.SymbolicExpression

import Generic.HasSize
import Generic.Address
import Generic.Operand (GenericOperand(..))
import Generic.Instruction (GenericInstruction(Instruction))


import qualified Data.Serialize as Cereal
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntSet as IS
import Data.List (intercalate,partition,intersectBy,find)
import Data.Word 

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

import GHC.Generics (Generic)
import Debug.Trace


-- |  A verification condition is either:
-- * A precondition of the form:
-- >    Precondition (a0,si0) (a1,si1)
-- This formulates that at the initial state the two regions must be separate.
-- * An assertion of the form:
-- >    Assertion a (a0,si0) (a1,si1)
-- This formulates that dynamically, whenever address a is executed, the two regions are asserted to be separate.
-- * A function constraint of the form:
-- >    FunctionConstraint foo [(RDI, v0), (RSI, v1), ...]   { sp0,sp1,... }
-- This formulates that a function call to function foo with values v0, v1, ... stored in the registers should not overwrite certain state parts.
data VerificationCondition =
    Precondition          SimpleExpr Int SimpleExpr Int                               -- ^ Precondition:           lhs SEP rhs
  | Assertion             SimpleExpr SimpleExpr Int SimpleExpr Int                    -- ^ Assertion:    @address, lhs SEP rhs
  | FunctionConstraint    String Word64 [(Reg.Register,SimpleExpr)] (S.Set StatePart) -- ^ Function name, address, of call, with param registers
  | FunctionPointers      Word64 IS.IntSet                                             -- ^ A set of function pointers passed to a function
  deriving ((forall x. VerificationCondition -> Rep VerificationCondition x)
-> (forall x. Rep VerificationCondition x -> VerificationCondition)
-> Generic VerificationCondition
forall x. Rep VerificationCondition x -> VerificationCondition
forall x. VerificationCondition -> Rep VerificationCondition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep VerificationCondition x -> VerificationCondition
$cfrom :: forall x. VerificationCondition -> Rep VerificationCondition x
Generic,VerificationCondition -> VerificationCondition -> Bool
(VerificationCondition -> VerificationCondition -> Bool)
-> (VerificationCondition -> VerificationCondition -> Bool)
-> Eq VerificationCondition
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VerificationCondition -> VerificationCondition -> Bool
$c/= :: VerificationCondition -> VerificationCondition -> Bool
== :: VerificationCondition -> VerificationCondition -> Bool
$c== :: VerificationCondition -> VerificationCondition -> Bool
Eq,Eq VerificationCondition
Eq VerificationCondition
-> (VerificationCondition -> VerificationCondition -> Ordering)
-> (VerificationCondition -> VerificationCondition -> Bool)
-> (VerificationCondition -> VerificationCondition -> Bool)
-> (VerificationCondition -> VerificationCondition -> Bool)
-> (VerificationCondition -> VerificationCondition -> Bool)
-> (VerificationCondition
    -> VerificationCondition -> VerificationCondition)
-> (VerificationCondition
    -> VerificationCondition -> VerificationCondition)
-> Ord VerificationCondition
VerificationCondition -> VerificationCondition -> Bool
VerificationCondition -> VerificationCondition -> Ordering
VerificationCondition
-> VerificationCondition -> VerificationCondition
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: VerificationCondition
-> VerificationCondition -> VerificationCondition
$cmin :: VerificationCondition
-> VerificationCondition -> VerificationCondition
max :: VerificationCondition
-> VerificationCondition -> VerificationCondition
$cmax :: VerificationCondition
-> VerificationCondition -> VerificationCondition
>= :: VerificationCondition -> VerificationCondition -> Bool
$c>= :: VerificationCondition -> VerificationCondition -> Bool
> :: VerificationCondition -> VerificationCondition -> Bool
$c> :: VerificationCondition -> VerificationCondition -> Bool
<= :: VerificationCondition -> VerificationCondition -> Bool
$c<= :: VerificationCondition -> VerificationCondition -> Bool
< :: VerificationCondition -> VerificationCondition -> Bool
$c< :: VerificationCondition -> VerificationCondition -> Bool
compare :: VerificationCondition -> VerificationCondition -> Ordering
$ccompare :: VerificationCondition -> VerificationCondition -> Ordering
$cp1Ord :: Eq VerificationCondition
Ord)

-- | An acornym for a set of verification conditions
type VCS = S.Set VerificationCondition



-- | Add a function_pointer_intro to the given symbolic predicate
add_function_pointer :: Word64
-> Key
-> (a, Set VerificationCondition)
-> (a, Set VerificationCondition)
add_function_pointer Word64
a Key
ptr (a
s,Set VerificationCondition
vcs) =
  let (Set VerificationCondition
match,Set VerificationCondition
remainder) = (VerificationCondition -> Bool)
-> Set VerificationCondition
-> (Set VerificationCondition, Set VerificationCondition)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
S.partition VerificationCondition -> Bool
belongs_to_a Set VerificationCondition
vcs in
    case Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
match of
      []                         -> (a
s,VerificationCondition
-> Set VerificationCondition -> Set VerificationCondition
forall a. Ord a => a -> Set a -> Set a
S.insert (Word64 -> IntSet -> VerificationCondition
FunctionPointers Word64
a (IntSet -> VerificationCondition)
-> IntSet -> VerificationCondition
forall a b. (a -> b) -> a -> b
$ Key -> IntSet
IS.singleton Key
ptr) Set VerificationCondition
remainder)
      [FunctionPointers Word64
_ IntSet
ptrs'] -> (a
s,VerificationCondition
-> Set VerificationCondition -> Set VerificationCondition
forall a. Ord a => a -> Set a -> Set a
S.insert (Word64 -> IntSet -> VerificationCondition
FunctionPointers Word64
a (IntSet -> VerificationCondition)
-> IntSet -> VerificationCondition
forall a b. (a -> b) -> a -> b
$ Key -> IntSet -> IntSet
IS.insert Key
ptr IntSet
ptrs') Set VerificationCondition
remainder)
 where
  belongs_to_a :: VerificationCondition -> Bool
belongs_to_a (FunctionPointers Word64
a' IntSet
_) = Word64
a Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a'
  belongs_to_a VerificationCondition
_                       = Bool
False










data SymbolicOperation v = SO_Op X86.Opcode Int (Maybe Int) [v] | SO_Bit Int v | SO_SExtend Int Int v | SO_Overwrite Int v v | SO_Plus v v | SO_Minus v v | SO_Times v v

data RegionSize = Nat Word64 | UnknownSize
 deriving (RegionSize -> RegionSize -> Bool
(RegionSize -> RegionSize -> Bool)
-> (RegionSize -> RegionSize -> Bool) -> Eq RegionSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RegionSize -> RegionSize -> Bool
$c/= :: RegionSize -> RegionSize -> Bool
== :: RegionSize -> RegionSize -> Bool
$c== :: RegionSize -> RegionSize -> Bool
Eq,Eq RegionSize
Eq RegionSize
-> (RegionSize -> RegionSize -> Ordering)
-> (RegionSize -> RegionSize -> Bool)
-> (RegionSize -> RegionSize -> Bool)
-> (RegionSize -> RegionSize -> Bool)
-> (RegionSize -> RegionSize -> Bool)
-> (RegionSize -> RegionSize -> RegionSize)
-> (RegionSize -> RegionSize -> RegionSize)
-> Ord RegionSize
RegionSize -> RegionSize -> Bool
RegionSize -> RegionSize -> Ordering
RegionSize -> RegionSize -> RegionSize
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RegionSize -> RegionSize -> RegionSize
$cmin :: RegionSize -> RegionSize -> RegionSize
max :: RegionSize -> RegionSize -> RegionSize
$cmax :: RegionSize -> RegionSize -> RegionSize
>= :: RegionSize -> RegionSize -> Bool
$c>= :: RegionSize -> RegionSize -> Bool
> :: RegionSize -> RegionSize -> Bool
$c> :: RegionSize -> RegionSize -> Bool
<= :: RegionSize -> RegionSize -> Bool
$c<= :: RegionSize -> RegionSize -> Bool
< :: RegionSize -> RegionSize -> Bool
$c< :: RegionSize -> RegionSize -> Bool
compare :: RegionSize -> RegionSize -> Ordering
$ccompare :: RegionSize -> RegionSize -> Ordering
$cp1Ord :: Eq RegionSize
Ord,(forall x. RegionSize -> Rep RegionSize x)
-> (forall x. Rep RegionSize x -> RegionSize) -> Generic RegionSize
forall x. Rep RegionSize x -> RegionSize
forall x. RegionSize -> Rep RegionSize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RegionSize x -> RegionSize
$cfrom :: forall x. RegionSize -> Rep RegionSize x
Generic)

class (Ord v,Eq v,Show v, Eq p,Ord p,Show p) => SymbolicExecutable ctxt v p | ctxt -> v p where 
  sseparate :: ctxt -> String -> p -> RegionSize -> p -> RegionSize -> Bool
  senclosed :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
  salias :: ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
  ssensitive :: ctxt -> p -> RegionSize -> v -> Bool
  sread_from_ro_data :: ctxt -> p -> RegionSize -> Maybe v
  smk_mem_addresses :: ctxt -> String -> v -> S.Set p

  sjoin_values :: Foldable t => ctxt -> String -> t v -> v
  swiden_values :: ctxt -> String -> v -> v
  sjoin_pointers :: ctxt -> [p] -> [p]
  top :: ctxt -> String -> v


  ssemantics :: ctxt -> String -> SymbolicOperation v -> v
  sflg_semantics :: ctxt -> v -> X86.Instruction -> FlagStatus -> FlagStatus
  simmediate :: Integral i => ctxt -> i -> v

  smk_init_reg_value :: ctxt -> Reg.Register -> v
  smk_init_mem_value :: ctxt -> String -> p -> RegionSize -> v

  scall :: ctxt -> Bool -> X86.Instruction -> State (Sstate v p,VCS) ()
  sjump :: ctxt -> X86.Instruction -> State (Sstate v p,VCS) ()

  stry_jump_targets :: ctxt -> v -> Maybe (S.Set ResolvedJumpTarget)

  stry_immediate :: ctxt -> v -> Maybe Word64
  stry_deterministic :: ctxt -> v -> Maybe SimpleExpr
  stry_relocation :: ctxt -> p -> RegionSize -> Maybe v
  saddress_has_instruction :: ctxt -> Word64 -> Bool

data Sstate v p = Sstate {
    Sstate v p -> Map Register v
sregs  :: M.Map Reg.Register v,
    Sstate v p -> Map (p, RegionSize) v
smem   :: M.Map (p,RegionSize) v,
    Sstate v p -> FlagStatus
sflags :: FlagStatus
  }
  deriving (Sstate v p -> Sstate v p -> Bool
(Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool) -> Eq (Sstate v p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
/= :: Sstate v p -> Sstate v p -> Bool
$c/= :: forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
== :: Sstate v p -> Sstate v p -> Bool
$c== :: forall v p. (Eq v, Eq p) => Sstate v p -> Sstate v p -> Bool
Eq,Eq (Sstate v p)
Eq (Sstate v p)
-> (Sstate v p -> Sstate v p -> Ordering)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Bool)
-> (Sstate v p -> Sstate v p -> Sstate v p)
-> (Sstate v p -> Sstate v p -> Sstate v p)
-> Ord (Sstate v p)
Sstate v p -> Sstate v p -> Bool
Sstate v p -> Sstate v p -> Ordering
Sstate v p -> Sstate v p -> Sstate v p
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v p. (Ord v, Ord p) => Eq (Sstate v p)
forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Ordering
forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
min :: Sstate v p -> Sstate v p -> Sstate v p
$cmin :: forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
max :: Sstate v p -> Sstate v p -> Sstate v p
$cmax :: forall v p.
(Ord v, Ord p) =>
Sstate v p -> Sstate v p -> Sstate v p
>= :: Sstate v p -> Sstate v p -> Bool
$c>= :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
> :: Sstate v p -> Sstate v p -> Bool
$c> :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
<= :: Sstate v p -> Sstate v p -> Bool
$c<= :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
< :: Sstate v p -> Sstate v p -> Bool
$c< :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Bool
compare :: Sstate v p -> Sstate v p -> Ordering
$ccompare :: forall v p. (Ord v, Ord p) => Sstate v p -> Sstate v p -> Ordering
$cp1Ord :: forall v p. (Ord v, Ord p) => Eq (Sstate v p)
Ord,(forall x. Sstate v p -> Rep (Sstate v p) x)
-> (forall x. Rep (Sstate v p) x -> Sstate v p)
-> Generic (Sstate v p)
forall x. Rep (Sstate v p) x -> Sstate v p
forall x. Sstate v p -> Rep (Sstate v p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v p x. Rep (Sstate v p) x -> Sstate v p
forall v p x. Sstate v p -> Rep (Sstate v p) x
$cto :: forall v p x. Rep (Sstate v p) x -> Sstate v p
$cfrom :: forall v p x. Sstate v p -> Rep (Sstate v p) x
Generic)


instance Show RegionSize where
  show :: RegionSize -> String
show (Nat Word64
imm)  = Word64 -> String
forall a. Show a => a -> String
show Word64
imm
  show RegionSize
UnknownSize = String
"u"

instance (Show v,Show p) => Show (Sstate v p) where
  show :: Sstate v p -> String
show (Sstate Map Register v
regs Map (p, RegionSize) v
mem FlagStatus
flags) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((Register, v) -> String) -> [(Register, v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Register, v) -> String
forall a a. (Show a, Show a) => (a, a) -> String
show_reg ([(Register, v)] -> [String]) -> [(Register, v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map Register v -> [(Register, v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Register v
regs) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((p, RegionSize), v) -> String)
-> [((p, RegionSize), v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((p, RegionSize), v) -> String
forall a a a. (Show a, Show a, Show a) => ((a, a), a) -> String
show_mem ([((p, RegionSize), v)] -> [String])
-> [((p, RegionSize), v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map (p, RegionSize) v -> [((p, RegionSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (p, RegionSize) v
mem) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [FlagStatus -> String
show_flags FlagStatus
flags]
   where
    show_reg :: (a, a) -> String
show_reg (a
r,a
v)      = a -> String
forall a. Show a => a -> String
show a
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
    show_mem :: ((a, a), a) -> String
show_mem ((a
a,a
si),a
v) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] := " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v 
    show_flags :: FlagStatus -> String
show_flags          = FlagStatus -> String
forall a. Show a => a -> String
show

instance Cereal.Serialize RegionSize
instance (Ord v, Cereal.Serialize v,Ord p, Cereal.Serialize p) => Cereal.Serialize (Sstate v p)
instance NFData RegionSize
instance (NFData v,NFData p) => NFData (Sstate v p)



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

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



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

sread_reg :: SymbolicExecutable ctxt v p => ctxt -> Reg.Register -> State (Sstate v p,VCS) v
sread_reg :: ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
sread_reg ctxt
ctxt Register
r = do
  let rr :: Register
rr = Register -> Register
Reg.real Register
r
  v
v <- ((Sstate v p, Set VerificationCondition) -> v)
-> State (Sstate v p, Set VerificationCondition) v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, Set VerificationCondition) -> v)
 -> State (Sstate v p, Set VerificationCondition) v)
-> ((Sstate v p, Set VerificationCondition) -> v)
-> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, Set VerificationCondition) -> v
forall ctxt p p p b.
SymbolicExecutable ctxt p p =>
ctxt -> Register -> (Sstate p p, b) -> p
sread_rreg ctxt
ctxt Register
rr
  if Register -> Key
forall a. HasSize a => a -> Key
sizeof Register
r Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
32 then -- 256 bits
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
  else if Register -> Key
forall a. HasSize a => a -> Key
sizeof Register
r Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
16 then -- 128 bit
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 128" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
128 v
v
  else if Register -> Key
forall a. HasSize a => a -> Key
sizeof Register
r Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
8 then -- 64 bit
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
  else if Register -> Key
forall a. HasSize a => a -> Key
sizeof Register
r Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
4 then do -- 32 bit
    v
rip <- ((Sstate v p, Set VerificationCondition) -> v)
-> State (Sstate v p, Set VerificationCondition) v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, Set VerificationCondition) -> v)
 -> State (Sstate v p, Set VerificationCondition) v)
-> ((Sstate v p, Set VerificationCondition) -> v)
-> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, Set VerificationCondition) -> v
forall ctxt p p p b.
SymbolicExecutable ctxt p p =>
ctxt -> Register -> (Sstate p p, b) -> p
sread_rreg ctxt
ctxt (Register -> (Sstate v p, Set VerificationCondition) -> v)
-> Register -> (Sstate v p, Set VerificationCondition) -> v
forall a b. (a -> b) -> a -> b
$ Register
Reg.RIP
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt (String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
rip String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": read_reg 32") (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
32 v
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
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 16" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
16 v
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
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"read_reg 8" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
8 v
v
  else -- 8 bit hi
    v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"read_reg" v
v


-- | Write to a register
swrite_rreg :: SymbolicExecutable ctxt v p => ctxt -> Reg.Register -> v -> State (Sstate v p,VCS) () 
swrite_rreg :: ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
r v
v = 
  if Key -> ShowS
forall a. Key -> [a] -> [a]
take Key
2 (Register -> String
forall a. Show a => a -> String
show Register
r) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"ST" then
    () -> State (Sstate v p, Set VerificationCondition) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  else do
    (Sstate v p
s,Set VerificationCondition
vcs) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
    (Sstate v p, Set VerificationCondition)
-> State (Sstate v p, Set VerificationCondition) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, Set VerificationCondition)
 -> State (Sstate v p, Set VerificationCondition) ())
-> (Sstate v p, Set VerificationCondition)
-> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s {sregs :: Map Register v
sregs = Register -> v -> Map Register v -> Map Register v
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Register
r v
v (Sstate v p -> Map Register v
forall v p. Sstate v p -> Map Register v
sregs Sstate v p
s), sflags :: FlagStatus
sflags = StatePart -> FlagStatus -> FlagStatus
clean_flg (Register -> StatePart
SP_Reg Register
r) (Sstate v p -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Sstate v p
s) }, Set VerificationCondition
vcs)

soverwrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Bool -> Reg.Register -> v -> State (Sstate v p,VCS) ()
soverwrite_reg :: ctxt
-> Bool
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
soverwrite_reg ctxt
ctxt Bool
use_existing_value Register
r v
v = do
 let sz :: Key
sz  = Register -> Key
forall a. HasSize a => a -> Key
sizeof Register
r in
  if Key
sz Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
32 then -- 256 bit
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
r v
v
  else if Key
sz Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
16 then do -- 128 bit
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
rr (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg 128" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
128 v
v)
  else if Key
sz Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
8 then -- 64 bit
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
r v
v
  else if Key
sz Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
4 then do -- 32 bit
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
rr (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable 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
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
32 v
v)
  else if Key
sz Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
2 then do -- 16 bit 
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    v
curr_v <- ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, Set VerificationCondition) -> v)
 -> StateT (Sstate v p, Set VerificationCondition) Identity v)
-> ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, Set VerificationCondition) -> v
forall ctxt p p p b.
SymbolicExecutable ctxt p p =>
ctxt -> Register -> (Sstate p p, b) -> p
sread_rreg ctxt
ctxt Register
rr
    let v' :: SymbolicOperation v
v' = if Bool
use_existing_value then Key -> v -> v -> SymbolicOperation v
forall v. Key -> v -> v -> SymbolicOperation v
SO_Overwrite Key
16 v
curr_v (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable 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
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
16 v
v) else Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
16 v
v
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
rr (v -> State (Sstate v p, Set VerificationCondition) ())
-> v -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg' 16" SymbolicOperation v
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
    v
curr_v <- ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, Set VerificationCondition) -> v)
 -> StateT (Sstate v p, Set VerificationCondition) Identity v)
-> ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, Set VerificationCondition) -> v
forall ctxt p p p b.
SymbolicExecutable ctxt p p =>
ctxt -> Register -> (Sstate p p, b) -> p
sread_rreg ctxt
ctxt Register
rr
    let v' :: SymbolicOperation v
v' = if Bool
use_existing_value then Key -> v -> v -> SymbolicOperation v
forall v. Key -> v -> v -> SymbolicOperation v
SO_Overwrite Key
8 v
curr_v (ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable 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
$ Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
8 v
v) else Key -> v -> SymbolicOperation v
forall v. Key -> v -> SymbolicOperation v
SO_Bit Key
8 v
v
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
rr (v -> State (Sstate v p, Set VerificationCondition) ())
-> v -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"overreg' 8" SymbolicOperation v
v'
  else do
    let rr :: Register
rr = Register -> Register
Reg.real Register
r
    v
curr_v <- ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, Set VerificationCondition) -> v)
 -> StateT (Sstate v p, Set VerificationCondition) Identity v)
-> ((Sstate v p, Set VerificationCondition) -> v)
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Register -> (Sstate v p, Set VerificationCondition) -> v
forall ctxt p p p b.
SymbolicExecutable ctxt p p =>
ctxt -> Register -> (Sstate p p, b) -> p
sread_rreg ctxt
ctxt Register
rr
    let v' :: v
v' = ctxt -> String -> v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"write_reg (bitmode)" (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(SymbolicExecutable ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt String
"join write_reg (bitmode)" [v
v,v
curr_v]
    ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
rr (v -> State (Sstate v p, Set VerificationCondition) ())
-> v -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ v
v

swrite_reg :: SymbolicExecutable ctxt v p => ctxt -> Reg.Register -> v -> State (Sstate v p,VCS) ()
swrite_reg :: ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_reg ctxt
ctxt = ctxt
-> Bool
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
soverwrite_reg ctxt
ctxt Bool
True


-- | Read from memory
sread_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> v -> RegionSize -> State (Sstate v p,VCS) v
--sread_mem ctxt msg a si | trace ("sread_mem: "++ show (a,si)) False = error "trace"
sread_mem :: ctxt
-> String
-> v
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem ctxt
ctxt String
msg v
a RegionSize
si = do
  (Sstate v p
p,Set VerificationCondition
_) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
  let ptrs :: Set p
ptrs = ctxt -> String -> v -> Set p
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt (String
"sread_mem" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String, v, RegionSize, Sstate v p) -> String
forall a. Show a => a -> String
show (String
msg,v
a,RegionSize
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, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v
forall ctxt v p. SymbolicExecutable ctxt v p => ctxt -> String -> v
top ctxt
ctxt String
"read_mem from top"
  else do
    [v]
vs <- (p -> State (Sstate v p, Set VerificationCondition) v)
-> [p]
-> StateT (Sstate v p, Set VerificationCondition) Identity [v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\p
ptr -> ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem_from_ptr ctxt
ctxt String
msg p
ptr RegionSize
si) ([p]
 -> StateT (Sstate v p, Set VerificationCondition) Identity [v])
-> [p]
-> StateT (Sstate v p, Set VerificationCondition) 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, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(SymbolicExecutable ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nRead join:" String -> ShowS
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 :: SymbolicExecutable ctxt v p => ctxt -> String -> p -> RegionSize -> State (Sstate v p,VCS) v
--sread_mem_from_ptr ctxt msg a si | trace ("sread_mem_from_ptr: "++ show (a,si)) False = error "trace"
sread_mem_from_ptr :: ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem_from_ptr ctxt
ctxt String
msg p
a RegionSize
si =
  case ctxt -> p -> RegionSize -> Maybe v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> Maybe v
stry_relocation ctxt
ctxt p
a RegionSize
si of
    Just v
v -> v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
    Maybe v
_      -> 
      case ctxt -> p -> RegionSize -> Maybe v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> Maybe v
sread_from_ro_data ctxt
ctxt p
a RegionSize
si of
        Just v
v -> v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
        Maybe v
_      -> p -> State (Sstate v p, Set VerificationCondition) v
forall b b (m :: * -> *).
(MonadState (Sstate b p, b) m, SymbolicExecutable ctxt b p) =>
p -> m b
sread_mem' p
a
 where
  sread_mem' :: p -> m b
sread_mem' p
a = do
    (Sstate b p
s,b
vcs) <- m (Sstate b p, b)
forall s (m :: * -> *). MonadState s m => m s
get
    case (((p, RegionSize), b) -> Bool)
-> [((p, RegionSize), b)] -> Maybe ((p, RegionSize), b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\((p
a0,RegionSize
si0),b
v0) -> (p
a0,RegionSize
si0) (p, RegionSize) -> (p, RegionSize) -> Bool
forall a. Eq a => a -> a -> Bool
== (p
a,RegionSize
si) Bool -> Bool -> Bool
&& ctxt -> p -> RegionSize -> b -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> v -> Bool
ssensitive ctxt
ctxt p
a0 RegionSize
si0 b
v0) ([((p, RegionSize), b)] -> Maybe ((p, RegionSize), b))
-> [((p, RegionSize), b)] -> Maybe ((p, RegionSize), b)
forall a b. (a -> b) -> a -> b
$ Map (p, RegionSize) b -> [((p, RegionSize), b)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, RegionSize) b -> [((p, RegionSize), b)])
-> Map (p, RegionSize) b -> [((p, RegionSize), b)]
forall a b. (a -> b) -> a -> b
$ Sstate b p -> Map (p, RegionSize) b
forall v p. Sstate v p -> Map (p, RegionSize) v
smem Sstate b p
s of
      Just ((p
a0,RegionSize
si0),b
v0) -> b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
v0
      Maybe ((p, RegionSize), b)
_ -> p -> m b
forall b b (m :: * -> *).
(MonadState (Sstate b p, b) m, SymbolicExecutable ctxt b p) =>
p -> m b
sread_mem'' p
a
  sread_mem'' :: p -> m a
sread_mem'' p
a = do
    (Sstate a p
s,b
vcs) <- m (Sstate a p, b)
forall s (m :: * -> *). MonadState s m => m s
get
    let (Map (p, RegionSize) a
_,Map (p, RegionSize) a
overlap) = ((p, RegionSize) -> a -> Bool)
-> Map (p, RegionSize) a
-> (Map (p, RegionSize) a, Map (p, RegionSize) a)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partitionWithKey (p, RegionSize) -> a -> Bool
forall v.
SymbolicExecutable ctxt v p =>
(p, RegionSize) -> v -> Bool
ssep (Map (p, RegionSize) a
 -> (Map (p, RegionSize) a, Map (p, RegionSize) a))
-> Map (p, RegionSize) a
-> (Map (p, RegionSize) a, Map (p, RegionSize) a)
forall a b. (a -> b) -> a -> b
$ Sstate a p -> Map (p, RegionSize) a
forall v p. Sstate v p -> Map (p, RegionSize) v
smem Sstate a p
s
    if Map (p, RegionSize) a -> Key
forall k a. Map k a -> Key
M.size Map (p, RegionSize) a
overlap Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
1 then
      let [((p
a0,RegionSize
si0),a
v0)] = Map (p, RegionSize) a -> [((p, RegionSize), a)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (p, RegionSize) a
overlap in
        if ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
salias ctxt
ctxt p
a RegionSize
si p
a0 RegionSize
si0 then
          a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v0
        else if ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> p -> RegionSize -> Bool
senclosed ctxt
ctxt p
a RegionSize
si p
a0 RegionSize
si0 then
          a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> a -> a
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt String
"read_mem (enclosure)" a
v0
        else
          a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ p -> Sstate a p -> Map (p, RegionSize) a -> a
forall p p k a.
(SymbolicExecutable ctxt p p, Show k, Show a) =>
p -> a -> Map k p -> p
read_from_overlap p
a Sstate a p
s Map (p, RegionSize) a
overlap
    else
      a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ p -> Sstate a p -> Map (p, RegionSize) a -> a
forall p p k a.
(SymbolicExecutable ctxt p p, Show k, Show a) =>
p -> a -> Map k p -> p
read_from_overlap p
a Sstate a p
s Map (p, RegionSize) a
overlap
 
  ssep :: (p, RegionSize) -> v -> Bool
ssep (p
a0,RegionSize
si0) v
v0 = ((p
a,RegionSize
si) (p, RegionSize) -> (p, RegionSize) -> Bool
forall a. Eq a => a -> a -> Bool
/= (p
a0,RegionSize
si0) Bool -> Bool -> Bool
&& ctxt -> p -> RegionSize -> v -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> p -> RegionSize -> v -> Bool
ssensitive ctxt
ctxt p
a0 RegionSize
si0 v
v0) Bool -> Bool -> Bool
|| ctxt -> String -> p -> RegionSize -> p -> RegionSize -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> p -> RegionSize -> p -> RegionSize -> Bool
sseparate ctxt
ctxt String
"read" p
a0 RegionSize
si0 p
a RegionSize
si

  read_from_overlap :: p -> a -> Map k p -> p
read_from_overlap p
a a
s Map k p
overlap
    | Map k p -> Key
forall k a. Map k a -> Key
M.size Map k p
overlap Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
0 = ctxt -> String -> p -> RegionSize -> p
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> p -> RegionSize -> v
smk_init_mem_value ctxt
ctxt (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nmaking init mem value:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (p, RegionSize) -> String
forall a. Show a => a -> String
show (p
a,RegionSize
si)) p
a RegionSize
si
    | Bool
otherwise = -- error ("Overlapping read:\nReading from: " ++ show (a,si,S.map fst overlap) ++ "\nIn state:\n" ++ show s) 
                  ctxt -> String -> p -> p
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> v
swiden_values ctxt
ctxt (String -> p -> a -> Map k p -> 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 p
overlap) (p -> p) -> p -> p
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> [p] -> p
forall ctxt v p (t :: * -> *).
(SymbolicExecutable ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String -> p -> a -> Map k p -> 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 p
overlap) (Map k p -> [p]
forall k a. Map k a -> [a]
M.elems Map k p
overlap)

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



-- | Write to memory
swrite_mem :: SymbolicExecutable ctxt v p => ctxt -> Bool -> v -> RegionSize -> v -> State (Sstate v p,VCS) ()
swrite_mem :: ctxt
-> Bool
-> v
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_mem ctxt
ctxt Bool
use_existing_value v
a RegionSize
si v
v = do
  (Sstate v p
p,Set VerificationCondition
_) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
  let ptrs :: Set p
ptrs = ctxt -> String -> v -> Set p
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt (String
"swrite_mem\n"String -> ShowS
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
    --trace ("TOP: writing to " ++ show (a,si) ++ "\nIn state:\n" ++ show p) $
    () -> State (Sstate v p, Set VerificationCondition) ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO ADD VC
  else
    (p -> State (Sstate v p, Set VerificationCondition) ())
-> Set p -> State (Sstate v p, Set VerificationCondition) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\p
ptr -> ctxt
-> Bool
-> p
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> p
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_mem_to_ptr ctxt
ctxt Bool
use_existing_value p
ptr RegionSize
si v
v) Set p
ptrs

swrite_mem_to_ptr :: SymbolicExecutable ctxt v p => ctxt -> Bool -> p -> RegionSize -> v -> State (Sstate v p,VCS) ()
swrite_mem_to_ptr :: ctxt
-> Bool
-> p
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_mem_to_ptr ctxt
ctxt Bool
use_existing_value p
a RegionSize
si v
v = do
  ((Sstate v p, Set VerificationCondition)
 -> (Sstate v p, Set VerificationCondition))
-> State (Sstate v p, Set VerificationCondition) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, Set VerificationCondition)
  -> (Sstate v p, Set VerificationCondition))
 -> State (Sstate v p, Set VerificationCondition) ())
-> ((Sstate v p, Set VerificationCondition)
    -> (Sstate v p, Set VerificationCondition))
-> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ \(Sstate v p
s,Set VerificationCondition
vcs) -> (Sstate v p
s { sflags :: FlagStatus
sflags = StatePart -> FlagStatus -> FlagStatus
clean_flg (SimpleExpr -> Key -> StatePart
SP_Mem (Word64 -> SimpleExpr
SE_Immediate Word64
0) Key
0) (Sstate v p -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Sstate v p
s) }, Set VerificationCondition
vcs)
  (Sstate v p
s,Set VerificationCondition
vcs) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get

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

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

  merge ::  SymbolicExecutable ctxt v p => ctxt -> [((p, RegionSize), v)] -> [((p, RegionSize), v)]
  merge :: ctxt -> [((p, RegionSize), v)] -> [((p, RegionSize), v)]
merge ctxt
ctxt [((p, RegionSize), v)]
m =
    let ptrs :: [p]
ptrs = ctxt -> [p] -> [p]
forall ctxt v p. SymbolicExecutable ctxt v p => ctxt -> [p] -> [p]
sjoin_pointers ctxt
ctxt ([p] -> [p]) -> [p] -> [p]
forall a b. (a -> b) -> a -> b
$ (((p, RegionSize), v) -> p) -> [((p, RegionSize), v)] -> [p]
forall a b. (a -> b) -> [a] -> [b]
map ((p, RegionSize) -> p
forall a b. (a, b) -> a
fst ((p, RegionSize) -> p)
-> (((p, RegionSize), v) -> (p, RegionSize))
-> ((p, RegionSize), v)
-> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((p, RegionSize), v) -> (p, RegionSize)
forall a b. (a, b) -> a
fst) [((p, RegionSize), v)]
m
        v' :: v
v'   = ctxt -> String -> v -> v
forall ctxt v p.
SymbolicExecutable 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 :: * -> *).
(SymbolicExecutable ctxt v p, 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, RegionSize), v) -> v) -> [((p, RegionSize), v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map ((p, RegionSize), v) -> v
forall a b. (a, b) -> b
snd [((p, RegionSize), v)]
m in
      (p -> ((p, RegionSize), v)) -> [p] -> [((p, RegionSize), v)]
forall a b. (a -> b) -> [a] -> [b]
map (\p
ptr -> ((p
ptr,RegionSize
UnknownSize),v
v')) [p]
ptrs




-- | Given the address of an operand of an instruction, resolve it given the current state.
sresolve_address :: SymbolicExecutable ctxt v p => ctxt -> X86.Address -> State (Sstate v p,VCS) v
sresolve_address :: ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt (AddressStorage Register
r) = ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
sread_reg ctxt
ctxt Register
r
sresolve_address ctxt
ctxt (AddressImm Word64
i)     = v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Word64
i
sresolve_address ctxt
ctxt (AddressMinus Address
a0 Address
a1) = do
  v
ra0 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a0 
  v
ra1 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a1
  v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"min" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ v -> v -> SymbolicOperation v
forall v. v -> v -> SymbolicOperation v
SO_Minus v
ra0 v
ra1
sresolve_address ctxt
ctxt (AddressPlus Address
a0 Address
a1) = do
  v
ra0 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a0 
  v
ra1 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a1
  v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"plus" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ v -> v -> SymbolicOperation v
forall v. v -> v -> SymbolicOperation v
SO_Plus v
ra0 v
ra1
sresolve_address ctxt
ctxt (AddressTimes Address
a0 Address
a1) = do
  v
ra0 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a0 
  v
ra1 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a1
  v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"times" (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ v -> v -> SymbolicOperation v
forall v. v -> v -> SymbolicOperation v
SO_Times v
ra0 v
ra1


sread_operand :: SymbolicExecutable ctxt v p => ctxt -> String -> X86.Operand -> State (Sstate v p,VCS) v
--sread_operand ctxt msg op | trace ("sgeneric_cinstr: "++ show op) False = error "trace"
sread_operand :: ctxt
-> String
-> Operand
-> State (Sstate v p, Set VerificationCondition) v
sread_operand ctxt
ctxt String
msg (Storage Register
r)          = ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
sread_reg ctxt
ctxt Register
r
sread_operand ctxt
ctxt String
msg (EffectiveAddress Address
a) = ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a
sread_operand ctxt
ctxt String
msg (Immediate Word64
a)        = v -> State (Sstate v p, Set VerificationCondition) v
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, Set VerificationCondition) v)
-> v -> State (Sstate v p, Set VerificationCondition) v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Word64
a
sread_operand ctxt
ctxt String
msg (Memory Address
a Key
si)        = do
  v
resolved_address <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a 
  ctxt
-> String
-> v
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> v
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem ctxt
ctxt String
msg v
resolved_address (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
si)

swrite_operand :: SymbolicExecutable ctxt v p => ctxt -> Bool -> X86.Operand -> v -> State (Sstate v p,VCS) ()
swrite_operand :: ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand ctxt
ctxt Bool
use_existing_value (Storage Register
r)   v
v = ctxt
-> Bool
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
soverwrite_reg ctxt
ctxt Bool
use_existing_value Register
r v
v
swrite_operand ctxt
ctxt Bool
use_existing_value (Memory Address
a Key
si) v
v = do
  v
resolved_address <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a 
  ctxt
-> Bool
-> v
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> v
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_mem ctxt
ctxt Bool
use_existing_value v
resolved_address (Word64 -> RegionSize
Nat (Word64 -> RegionSize) -> Word64 -> RegionSize
forall a b. (a -> b) -> a -> b
$ Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
si) v
v


-- v is bogus, but needed for getting the type checker to accept this. Don't know why. 
swrite_flags :: SymbolicExecutable ctxt v p => ctxt -> v -> X86.Instruction -> State (Sstate v p,VCS) ()
swrite_flags :: ctxt
-> v
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
swrite_flags ctxt
ctxt v
v Instruction
i = do
  (Sstate v p
s,Set VerificationCondition
vcs) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
  (Sstate v p, Set VerificationCondition)
-> State (Sstate v p, Set VerificationCondition) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Sstate v p, Set VerificationCondition)
 -> State (Sstate v p, Set VerificationCondition) ())
-> (Sstate v p, Set VerificationCondition)
-> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ (Sstate v p
s {sflags :: FlagStatus
sflags = ctxt -> v -> Instruction -> FlagStatus -> FlagStatus
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Instruction -> FlagStatus -> FlagStatus
sflg_semantics ctxt
ctxt v
v Instruction
i (Sstate v p -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Sstate v p
s)}, Set VerificationCondition
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 :: 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 Address
_) = Bool
True -- TODO
  is_tainted (Memory Address
a Key
si)        =
    case StatePart
sp of
      SP_Mem SimpleExpr
_ Key
_ -> Bool
True
      StatePart
_          -> Bool
False


-- TODO JE, other JMP aboves and JUMP lesses
add_jump_to_pred :: X86.Instruction -> X86.Instruction -> FlagStatus -> FlagStatus
add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus
add_jump_to_pred i0 :: Instruction
i0@(Instruction AddressWord64
_ Maybe Prefix
_ Opcode
X86.JA Maybe Operand
_ [Immediate Word64
trgt] Maybe Key
_) Instruction
i1 FlagStatus
flg =
  case FlagStatus
flg of
    FS_CMP Maybe Bool
b Operand
o1 Operand
o2 -> if Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i1 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt then Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False) Operand
o1 Operand
o2 else Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) Operand
o1 Operand
o2
    FlagStatus
_ -> FlagStatus
flg
add_jump_to_pred i0 :: Instruction
i0@(Instruction AddressWord64
_ Maybe Prefix
_ Opcode
X86.JBE Maybe Operand
_ [Immediate Word64
trgt] Maybe Key
_) Instruction
i1 FlagStatus
flg =
  case FlagStatus
flg of
    FS_CMP Maybe Bool
b Operand
o1 Operand
o2 -> if Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i1 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt then Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) Operand
o1 Operand
o2 else Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False) Operand
o1 Operand
o2
    FlagStatus
_ -> FlagStatus
flg
add_jump_to_pred Instruction
i0 Instruction
i1 FlagStatus
flg = FlagStatus
flg



sreturn :: SymbolicExecutable ctxt v p => ctxt -> State (Sstate v p,VCS) ()
sreturn :: ctxt -> State (Sstate v p, Set VerificationCondition) ()
sreturn ctxt
ctxt = do
  v
e0 <- ctxt
-> String
-> Operand
-> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> Operand
-> State (Sstate v p, Set VerificationCondition) v
sread_operand ctxt
ctxt String
"return" (Address -> Key -> Operand
forall storage.
GenericAddress storage -> Key -> GenericOperand storage
Memory (Register -> Address
forall storage. storage -> GenericAddress storage
AddressStorage Register
Reg.RSP) Key
8)
  let address :: Address
address = Address -> Address -> Address
forall storage.
GenericAddress storage
-> GenericAddress storage -> GenericAddress storage
AddressPlus (Register -> Address
forall storage. storage -> GenericAddress storage
AddressStorage Register
Reg.RSP) (Word64 -> Address
forall storage. Word64 -> GenericAddress storage
AddressImm Word64
8)
  v
e1 <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
address
  ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_reg ctxt
ctxt Register
Reg.RSP v
e1
  ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand ctxt
ctxt Bool
True (Register -> Operand
forall storage. storage -> GenericOperand storage
Storage Register
Reg.RIP) v
e0


-- LEA
slea :: SymbolicExecutable ctxt v p => ctxt -> AddressWord64 -> X86.Operand -> X86.Operand -> State (Sstate v p,VCS) ()
slea :: ctxt
-> AddressWord64
-> Operand
-> Operand
-> State (Sstate v p, Set VerificationCondition) ()
slea ctxt
ctxt (AddressWord64 Word64
i_a) Operand
dst (EffectiveAddress Address
a) = do
  v
e <- ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Address -> State (Sstate v p, Set VerificationCondition) v
sresolve_address ctxt
ctxt Address
a
  ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand ctxt
ctxt Bool
True Operand
dst v
e
  case ctxt -> v -> Maybe Word64
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Maybe Word64
stry_immediate ctxt
ctxt v
e of
    Maybe Word64
Nothing  -> () -> State (Sstate v p, Set VerificationCondition) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Word64
imm -> if ctxt -> Word64 -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Word64 -> Bool
saddress_has_instruction ctxt
ctxt Word64
imm then ((Sstate v p, Set VerificationCondition)
 -> (Sstate v p, Set VerificationCondition))
-> State (Sstate v p, Set VerificationCondition) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, Set VerificationCondition)
  -> (Sstate v p, Set VerificationCondition))
 -> State (Sstate v p, Set VerificationCondition) ())
-> ((Sstate v p, Set VerificationCondition)
    -> (Sstate v p, Set VerificationCondition))
-> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Key
-> (Sstate v p, Set VerificationCondition)
-> (Sstate v p, Set VerificationCondition)
forall a.
Word64
-> Key
-> (a, Set VerificationCondition)
-> (a, Set VerificationCondition)
add_function_pointer Word64
i_a (Key
 -> (Sstate v p, Set VerificationCondition)
 -> (Sstate v p, Set VerificationCondition))
-> Key
-> (Sstate v p, Set VerificationCondition)
-> (Sstate v p, Set VerificationCondition)
forall a b. (a -> b) -> a -> b
$ Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
imm else () -> State (Sstate v p, Set VerificationCondition) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- MOV
smov :: SymbolicExecutable ctxt v p => ctxt -> a -> X86.Instruction -> State (Sstate v p,VCS) ()
smov :: ctxt
-> a
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
smov ctxt
ctxt a
a i :: Instruction
i@(Instruction AddressWord64
label Maybe Prefix
prefix Opcode
X86.MOV (Just Operand
dst) [src :: Operand
src@(Immediate Word64
imm)] Maybe Key
annot)
  | ctxt -> Word64 -> Bool
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Word64 -> Bool
saddress_has_instruction ctxt
ctxt Word64
imm   = ctxt
-> AddressWord64
-> Operand
-> Operand
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> AddressWord64
-> Operand
-> Operand
-> State (Sstate v p, Set VerificationCondition) ()
slea ctxt
ctxt AddressWord64
label Operand
dst (Address -> Operand
forall storage. GenericAddress storage -> GenericOperand storage
EffectiveAddress (Word64 -> Address
forall storage. Word64 -> GenericAddress storage
AddressImm Word64
imm))
  | Bool
otherwise                           = ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sgeneric_cinstr ctxt
ctxt Instruction
i
smov ctxt
ctxt a
a Instruction
i                           = ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sgeneric_cinstr ctxt
ctxt Instruction
i


sgeneric_cinstr :: SymbolicExecutable ctxt v p => ctxt -> X86.Instruction -> State (Sstate v p,VCS) ()
--sgeneric_cinstr ctxt i | trace ("sgeneric_cinstr: "++ show i) False = error "trace"
sgeneric_cinstr :: ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sgeneric_cinstr ctxt
ctxt i :: Instruction
i@(Instruction AddressWord64
label Maybe Prefix
prefix Opcode
mnemonic (Just Operand
dst) [Operand]
srcs Maybe Key
annot) = do
  [v]
ops <- (Operand
 -> StateT (Sstate v p, Set VerificationCondition) Identity v)
-> [Operand]
-> StateT (Sstate v p, Set VerificationCondition) Identity [v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ctxt
-> String
-> Operand
-> StateT (Sstate v p, Set VerificationCondition) Identity v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> Operand
-> State (Sstate v p, Set VerificationCondition) v
sread_operand ctxt
ctxt (Instruction -> String
forall a. Show a => a -> String
show Instruction
i)) [Operand]
srcs
  ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand ctxt
ctxt Bool
True Operand
dst (v -> State (Sstate v p, Set VerificationCondition) ())
-> v -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt (Instruction -> String
forall a. Show a => a -> String
show Instruction
i) (SymbolicOperation v -> v) -> SymbolicOperation v -> v
forall a b. (a -> b) -> a -> b
$ Opcode -> Key -> Maybe Key -> [v] -> SymbolicOperation v
forall v. Opcode -> Key -> Maybe Key -> [v] -> SymbolicOperation v
SO_Op Opcode
mnemonic (Operand -> Key
forall a. HasSize a => GenericOperand a -> Key
operand_size Operand
dst) ([Operand] -> Maybe Key
forall storage.
HasSize storage =>
[GenericOperand storage] -> Maybe Key
maybe_operand_size [Operand]
srcs) [v]
ops

operand_size :: GenericOperand a -> Key
operand_size (Storage a
r)   = a -> Key
forall a. HasSize a => a -> Key
sizeof a
r
operand_size (Memory GenericAddress a
a Key
si) = Key
si
operand_size (EffectiveAddress GenericAddress a
_) = Key
8

maybe_operand_size :: [GenericOperand storage] -> Maybe Key
maybe_operand_size []   = Maybe Key
forall a. Maybe a
Nothing
maybe_operand_size [GenericOperand storage]
srcs
  | (GenericOperand storage -> Bool)
-> [GenericOperand storage] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any GenericOperand storage -> Bool
forall storage. GenericOperand storage -> Bool
is_immediate [GenericOperand storage]
srcs = Maybe Key
forall a. Maybe a
Nothing
  | Bool
otherwise =
    let sizes :: [Key]
sizes = (GenericOperand storage -> Key)
-> [GenericOperand storage] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map GenericOperand storage -> Key
forall a. HasSize a => GenericOperand a -> Key
operand_size [GenericOperand storage]
srcs in
      if (Key -> Bool) -> [Key] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Key] -> Key
forall a. [a] -> a
head [Key]
sizes)) ([Key] -> [Key]
forall a. [a] -> [a]
tail [Key]
sizes) then
        Key -> Maybe Key
forall a. a -> Maybe a
Just (Key -> Maybe Key) -> Key -> Maybe Key
forall a b. (a -> b) -> a -> b
$ [Key] -> Key
forall a. [a] -> a
head [Key]
sizes
      else
        Maybe Key
forall a. Maybe a
Nothing
 where
  is_immediate :: GenericOperand storage -> Bool
is_immediate (Immediate Word64
_) = Bool
True
  is_immediate GenericOperand storage
_             = Bool
False

sexec_cinstr :: SymbolicExecutable ctxt v p => ctxt -> X86.Instruction -> State (Sstate v p,VCS) ()
--sexec_cinstr ctxt i | trace ("sexec_cinstr: "++ show i) False = error "trace"
sexec_cinstr :: ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sexec_cinstr ctxt
ctxt i :: Instruction
i@(Instruction AddressWord64
label Maybe Prefix
prefix Opcode
mnemonic (Just Operand
dst) [Operand]
srcs Maybe Key
annot)
  | Opcode
mnemonic Opcode -> Opcode -> Bool
forall a. Eq a => a -> a -> Bool
== Opcode
X86.LEA                      = ctxt
-> AddressWord64
-> Operand
-> Operand
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> AddressWord64
-> Operand
-> Operand
-> State (Sstate v p, Set VerificationCondition) ()
slea ctxt
ctxt AddressWord64
label Operand
dst (Operand -> State (Sstate v p, Set VerificationCondition) ())
-> Operand -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ [Operand] -> Operand
forall a. [a] -> a
head [Operand]
srcs
  | Opcode
mnemonic Opcode -> Opcode -> Bool
forall a. Eq a => a -> a -> Bool
== Opcode
X86.MOV                      = ctxt
-> v
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p a.
SymbolicExecutable ctxt v p =>
ctxt
-> a
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
smov ctxt
ctxt (ctxt -> String -> v
forall ctxt v p. SymbolicExecutable ctxt v p => ctxt -> String -> v
top ctxt
ctxt String
"") Instruction
i
  | Opcode
mnemonic Opcode -> [Opcode] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opcode]
xors Bool -> Bool -> Bool
&& Operand
dst Operand -> Operand -> Bool
forall a. Eq a => a -> a -> Bool
== [Operand] -> Operand
forall a. [a] -> a
head [Operand]
srcs = ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Operand
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand ctxt
ctxt Bool
False Operand
dst (v -> State (Sstate v p, Set VerificationCondition) ())
-> v -> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> Integer -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Integer
0
  | Bool
otherwise                                = ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sgeneric_cinstr ctxt
ctxt Instruction
i
 where
  xors :: [Opcode]
xors = [Opcode
X86.XOR,Opcode
X86.PXOR]
sexec_cinstr ctxt
ctxt i :: Instruction
i@(Instruction AddressWord64
label Maybe Prefix
prefix Opcode
mnemonic Maybe Operand
Nothing [Operand]
_ Maybe Key
_)
  | Opcode -> Bool
X86.isRet Opcode
mnemonic        = ctxt -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> State (Sstate v p, Set VerificationCondition) ()
sreturn ctxt
ctxt
  | Opcode -> Bool
X86.isJump Opcode
mnemonic       = ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sjump ctxt
ctxt Instruction
i
  | Opcode -> Bool
X86.isCall Opcode
mnemonic       = ctxt
-> Bool
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
scall ctxt
ctxt Bool
False Instruction
i
  | Bool
otherwise                 = () -> State (Sstate v p, Set VerificationCondition) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()






sset_rip :: SymbolicExecutable ctxt v p => ctxt -> X86.Instruction -> State (Sstate v p,VCS) ()
sset_rip :: ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sset_rip ctxt
ctxt Instruction
i = ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_reg ctxt
ctxt Register
Reg.RIP (ctxt -> Word64 -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ (Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Key -> Word64) -> Key -> Word64
forall a b. (a -> b) -> a -> b
$ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i))

sexec_instr :: SymbolicExecutable ctxt v p => ctxt -> X86.Instruction -> State (Sstate v p,VCS) ()
--sexec_instr ctxt i | trace ("sexec_isntr: "++ show i) False = error "trace"
sexec_instr :: ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sexec_instr ctxt
ctxt Instruction
i = do
  (Sstate v p
p,Set VerificationCondition
_) <- StateT
  (Sstate v p, Set VerificationCondition)
  Identity
  (Sstate v p, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
  ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sset_rip ctxt
ctxt Instruction
i
  (Instruction -> State (Sstate v p, Set VerificationCondition) ())
-> [Instruction]
-> State (Sstate v p, Set VerificationCondition) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sexec_cinstr ctxt
ctxt) ([Instruction] -> State (Sstate v p, Set VerificationCondition) ())
-> [Instruction]
-> State (Sstate v p, Set VerificationCondition) ()
forall a b. (a -> b) -> a -> b
$ Instruction -> [Instruction]
X86.canonicalize Instruction
i
  ctxt
-> v
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> v
-> Instruction
-> State (Sstate v p, Set VerificationCondition) ()
swrite_flags ctxt
ctxt (ctxt -> String -> v
forall ctxt v p. SymbolicExecutable ctxt v p => ctxt -> String -> v
top ctxt
ctxt String
"") Instruction
i 



--sexec_block :: SymbolicExecutable ctxt v p => ctxt -> [X86.Instruction] -> Maybe [X86.Instruction] -> Sstate v p -> (Sstate v p,VCS)
sexec_block :: ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, Set VerificationCondition)
sexec_block ctxt
ctxt []    Maybe [Instruction]
_    Sstate v p
s = (Sstate v p
s,Set VerificationCondition
forall a. Set a
S.empty)
sexec_block ctxt
ctxt [Instruction]
block Maybe [Instruction]
next Sstate v p
s = 
  let  m :: StateT (Sstate v p, Set VerificationCondition) Identity ()
m = ctxt
-> Register
-> v
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_reg ctxt
ctxt Register
Reg.RIP (ctxt -> Word64 -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof ([Instruction] -> Instruction
forall a. [a] -> a
head [Instruction]
block)) StateT (Sstate v p, Set VerificationCondition) Identity ()
-> StateT (Sstate v p, Set VerificationCondition) Identity [()]
-> StateT (Sstate v p, Set VerificationCondition) Identity [()]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Instruction
 -> StateT (Sstate v p, Set VerificationCondition) Identity ())
-> [Instruction]
-> StateT (Sstate v p, Set VerificationCondition) Identity [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ctxt
-> Instruction
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sexec_instr ctxt
ctxt) [Instruction]
block StateT (Sstate v p, Set VerificationCondition) Identity [()]
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Maybe [Instruction]
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall v p p.
(SymbolicExecutable ctxt v p, SymbolicExecutable ctxt v p) =>
Maybe [Instruction]
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
set_flagstatus Maybe [Instruction]
next) in
    StateT (Sstate v p, Set VerificationCondition) Identity ()
-> (Sstate v p, Set VerificationCondition)
-> (Sstate v p, Set VerificationCondition)
forall s a. State s a -> s -> s
execState StateT (Sstate v p, Set VerificationCondition) Identity ()
m (Sstate v p
s,Set VerificationCondition
forall a. Set a
S.empty)
 where
  --set_flagstatus :: Maybe [X86.Instruction] -> State (Sstate v p,VCS) ()
  set_flagstatus :: Maybe [Instruction]
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
set_flagstatus Maybe [Instruction]
Nothing       = () -> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  set_flagstatus (Just (Instruction
i':[Instruction]
_)) = do
    ctxt
-> Register
-> v
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_reg ctxt
ctxt Register
Reg.RIP (ctxt -> Word64 -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i')
    ((Sstate v p, Set VerificationCondition)
 -> (Sstate v p, Set VerificationCondition))
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, Set VerificationCondition)
  -> (Sstate v p, Set VerificationCondition))
 -> StateT (Sstate v p, Set VerificationCondition) Identity ())
-> ((Sstate v p, Set VerificationCondition)
    -> (Sstate v p, Set VerificationCondition))
-> StateT (Sstate v p, Set VerificationCondition) Identity ()
forall a b. (a -> b) -> a -> b
$ \(Sstate v p
s,Set VerificationCondition
vcs) -> (Sstate v p
s { sflags :: FlagStatus
sflags = Instruction -> Instruction -> FlagStatus -> FlagStatus
add_jump_to_pred ([Instruction] -> Instruction
forall a. [a] -> a
last [Instruction]
block) Instruction
i' (Sstate v p -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Sstate v p
s) }, Set VerificationCondition
vcs)



sjoin_mem :: SymbolicExecutable ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> M.Map (p, RegionSize) v
sjoin_mem :: ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, RegionSize) v
sjoin_mem ctxt
ctxt String
msg Sstate v p
s0 Sstate v p
s1 =
  let m0 :: [((p, RegionSize), v)]
m0     = Map (p, RegionSize) v -> [((p, RegionSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, RegionSize) v -> [((p, RegionSize), v)])
-> Map (p, RegionSize) v -> [((p, RegionSize), v)]
forall a b. (a -> b) -> a -> b
$ Sstate v p -> Map (p, RegionSize) v
forall v p. Sstate v p -> Map (p, RegionSize) v
smem Sstate v p
s0
      m1 :: [((p, RegionSize), v)]
m1     = Map (p, RegionSize) v -> [((p, RegionSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, RegionSize) v -> [((p, RegionSize), v)])
-> Map (p, RegionSize) v -> [((p, RegionSize), v)]
forall a b. (a -> b) -> a -> b
$ Sstate v p -> Map (p, RegionSize) v
forall v p. Sstate v p -> Map (p, RegionSize) v
smem Sstate v p
s1
      shared :: Map (p, RegionSize) v
shared = (v -> v -> v)
-> Map (p, RegionSize) v
-> Map (p, RegionSize) v
-> Map (p, RegionSize) v
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith v -> v -> v
forall v p. SymbolicExecutable ctxt v p => v -> v -> v
join_values ([((p, RegionSize), v)] -> Map (p, RegionSize) v
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [((p, RegionSize), v)]
m0) ([((p, RegionSize), v)] -> Map (p, RegionSize) v
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [((p, RegionSize), v)]
m1)
      diff :: [((p, RegionSize), v)]
diff   = (((p, RegionSize), v) -> Bool)
-> [((p, RegionSize), v)] -> [((p, RegionSize), v)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\((p, RegionSize)
r,v
_) -> (p, RegionSize)
r (p, RegionSize) -> Map (p, RegionSize) v -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.notMember` Map (p, RegionSize) v
shared) ([((p, RegionSize), v)]
m0 [((p, RegionSize), v)]
-> [((p, RegionSize), v)] -> [((p, RegionSize), v)]
forall a. [a] -> [a] -> [a]
++ [((p, RegionSize), v)]
m1) in
    Map (p, RegionSize) v
-> [((p, RegionSize), v)] -> Map (p, RegionSize) v
forall p b.
SymbolicExecutable ctxt v p =>
Map (p, RegionSize) v
-> [((p, RegionSize), b)] -> Map (p, RegionSize) v
sjoin_mem' Map (p, RegionSize) v
shared [((p, RegionSize), v)]
diff
 where
  sjoin_mem' :: Map (p, RegionSize) v
-> [((p, RegionSize), b)] -> Map (p, RegionSize) v
sjoin_mem' Map (p, RegionSize) v
m [] = Map (p, RegionSize) v
m 
  sjoin_mem' Map (p, RegionSize) v
m (((p
a,RegionSize
si),b
v):[((p, RegionSize), b)]
regions)
    | Bool
otherwise =
      let v0 :: v
v0 = State (Sstate v p, Set VerificationCondition) v -> Sstate v p -> v
forall v p a.
State (Sstate v p, Set VerificationCondition) a -> Sstate v p -> a
evalSstate (ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem_from_ptr ctxt
ctxt (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"join0" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (p, RegionSize, Sstate v p, Sstate v p) -> String
forall a. Show a => a -> String
show (p
a,RegionSize
si,Sstate v p
s0,Sstate v p
s1)) p
a RegionSize
si) Sstate v p
s0
          v1 :: v
v1 = State (Sstate v p, Set VerificationCondition) v -> Sstate v p -> v
forall v p a.
State (Sstate v p, Set VerificationCondition) a -> Sstate v p -> a
evalSstate (ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> p
-> RegionSize
-> State (Sstate v p, Set VerificationCondition) v
sread_mem_from_ptr ctxt
ctxt (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"join0" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (p, RegionSize, Sstate v p, Sstate v p) -> String
forall a. Show a => a -> String
show (p
a,RegionSize
si,Sstate v p
s0,Sstate v p
s1)) p
a RegionSize
si) Sstate v p
s1
          v' :: v
v' = v -> v -> v
forall v p. SymbolicExecutable ctxt v p => v -> v -> v
join_values v
v0 v
v1
          m' :: Map (p, RegionSize) v
m' = Sstate v p -> Map (p, RegionSize) v
forall v p. Sstate v p -> Map (p, RegionSize) v
smem (Sstate v p -> Map (p, RegionSize) v)
-> Sstate v p -> Map (p, RegionSize) v
forall a b. (a -> b) -> a -> b
$ State (Sstate v p, Set VerificationCondition) ()
-> Sstate v p -> Sstate v p
forall v p b.
State (Sstate v p, Set VerificationCondition) b
-> Sstate v p -> Sstate v p
execSstate (ctxt
-> Bool
-> p
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> p
-> RegionSize
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_mem_to_ptr ctxt
ctxt Bool
True p
a RegionSize
si v
v') (Sstate v p -> Sstate v p) -> Sstate v p -> Sstate v p
forall a b. (a -> b) -> a -> b
$ Sstate :: forall v p.
Map Register v -> Map (p, RegionSize) v -> FlagStatus -> Sstate v p
Sstate {sregs :: Map Register v
sregs = Map Register v
forall k a. Map k a
M.empty, smem :: Map (p, RegionSize) v
smem = Map (p, RegionSize) v
m, sflags :: FlagStatus
sflags = FlagStatus
None} in
        Map (p, RegionSize) v
-> [((p, RegionSize), b)] -> Map (p, RegionSize) v
sjoin_mem' Map (p, RegionSize) v
m' [((p, RegionSize), b)]
regions

  join_values :: v -> v -> v
join_values v
a v
b = ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(SymbolicExecutable ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"States (mem value) " String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" joined with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
b) [v
a,v
b]




--sjoin_states ctxt msg s0 s1 | trace ("sjoin_states") False = error "trace"
sjoin_states :: ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states ctxt
ctxt String
msg s0 :: Sstate v p
s0@(Sstate Map Register v
regs0 Map (p, RegionSize) v
mem0 FlagStatus
flg0) s1 :: Sstate v p
s1@(Sstate Map Register v
regs1 Map (p, RegionSize) v
mem1 FlagStatus
flg1) =
  let flg :: FlagStatus
flg  = FlagStatus -> FlagStatus -> FlagStatus
join_flags FlagStatus
flg0 FlagStatus
flg1
      regs :: Map Register v
regs = (v -> v -> v) -> Map Register v -> Map Register v -> Map Register v
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith v -> v -> v
forall v p. SymbolicExecutable ctxt v p => v -> v -> v
join_reg Map Register v
regs0 Map Register v
regs1
      mem :: Map (p, RegionSize) v
mem  = ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, RegionSize) v
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> String -> Sstate v p -> Sstate v p -> Map (p, RegionSize) v
sjoin_mem ctxt
ctxt String
msg Sstate v p
s0 Sstate v p
s1
      s' :: Sstate v p
s'   = Map Register v -> Map (p, RegionSize) v -> FlagStatus -> Sstate v p
forall v p.
Map Register v -> Map (p, RegionSize) v -> FlagStatus -> Sstate v p
Sstate Map Register v
regs Map (p, RegionSize) v
mem FlagStatus
flg in
     Sstate v p
s'
 where
  join_reg :: v -> v -> v
join_reg v
a v
b 
    | v
a v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
b    = v
a
    | Bool
otherwise = ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(SymbolicExecutable ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
"States (regs)" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sstate v p -> String
forall a. Show a => a -> String
show Sstate v p
s0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sstate v p -> String
forall a. Show a => a -> String
show Sstate v p
s1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (v, v) -> String
forall a. Show a => a -> String
show(v
a,v
b)) [v
a,v
b]
  join_flags :: FlagStatus -> FlagStatus -> FlagStatus
join_flags (FS_CMP (Just Bool
True) Operand
o0 Operand
v0) (FS_CMP (Just Bool
True) Operand
o0' Operand
v0')
    | FlagStatus
flg0 FlagStatus -> FlagStatus -> Bool
forall a. Eq a => a -> a -> Bool
== FlagStatus
flg1 = FlagStatus
flg0
    | Operand
o0 Operand -> Operand -> Bool
forall a. Eq a => a -> a -> Bool
/= Operand
o0'    = FlagStatus
None
    | Bool
otherwise    = 
      case (Operand
v0,Operand
v0') of
        (Immediate Word64
n0,Immediate Word64
n1) -> Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) Operand
o0 (Word64 -> Operand
forall storage. Word64 -> GenericOperand storage
Immediate (Word64 -> Operand) -> Word64 -> Operand
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
max Word64
n0 Word64
n1)
        (Operand, Operand)
_ -> FlagStatus
None
  join_flags FlagStatus
_ FlagStatus
_ 
    | FlagStatus
flg0 FlagStatus -> FlagStatus -> Bool
forall a. Eq a => a -> a -> Bool
== FlagStatus
flg1 = FlagStatus
flg0
    | Bool
otherwise    = FlagStatus
None


-- | The supremum of a list of predicates
supremum :: SymbolicExecutable ctxt v p => ctxt -> [Sstate v p] -> Sstate v p
supremum :: ctxt -> [Sstate v p] -> Sstate v p
supremum ctxt
ctxt [] = String -> Sstate v p
forall a. HasCallStack => String -> a
error (String -> Sstate v p) -> String -> Sstate v p
forall a b. (a -> b) -> a -> b
$ String
"Cannot compute supremum of []"
supremum ctxt
ctxt [Sstate v p]
ss = (Sstate v p -> Sstate v p -> Sstate v p)
-> [Sstate v p] -> Sstate v p
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
forall v p ctxt p.
(SymbolicExecutable ctxt v p, SymbolicExecutable ctxt v p) =>
ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states ctxt
ctxt String
"supremum") [Sstate v p]
ss

simplies :: ctxt -> Sstate v p -> Sstate v p -> Bool
simplies ctxt
ctxt Sstate v p
s0 Sstate v p
s1 = (Sstate v p -> Sstate v p
set_rip (Sstate v p -> Sstate v p) -> Sstate v p -> Sstate v p
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
forall v p ctxt p.
(SymbolicExecutable ctxt v p, SymbolicExecutable ctxt v p) =>
ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states ctxt
ctxt String
"simplies" Sstate v p
s0 Sstate v p
s1) Sstate v p -> Sstate v p -> Bool
forall a. Eq a => a -> a -> Bool
== (Sstate v p -> Sstate v p
set_rip Sstate v p
s0)
 where
  set_rip :: Sstate v p -> Sstate v p
set_rip = State (Sstate v p, Set VerificationCondition) ()
-> Sstate v p -> Sstate v p
forall v p b.
State (Sstate v p, Set VerificationCondition) b
-> Sstate v p -> Sstate v p
execSstate (ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_rreg ctxt
ctxt Register
Reg.RIP (ctxt -> Integer -> v
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Integer
0))