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

module WithAbstractSymbolicValues.SymbolicExecution where

import Base

import WithAbstractSymbolicValues.Class
import WithAbstractSymbolicValues.FInit
import WithAbstractSymbolicValues.Sstate

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


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 qualified Data.IntMap as IM
import qualified Data.Set.NonEmpty as NES

import Data.List (intercalate,partition,intersectBy,find,nub)
import Data.Word 
import Data.Maybe

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

import GHC.Generics (Generic)
import Debug.Trace




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


add_pa_result :: Word64
-> PointerAnalysisResult v
-> (a, Set (VerificationCondition v))
-> (a, Set (VerificationCondition v))
add_pa_result Word64
a PointerAnalysisResult v
par (a
s,Set (VerificationCondition v)
vcs) = (a
s,VerificationCondition v
-> Set (VerificationCondition v) -> Set (VerificationCondition v)
forall a. Ord a => a -> Set a -> Set a
S.insert (Word64 -> PointerAnalysisResult v -> VerificationCondition v
forall v.
Word64 -> PointerAnalysisResult v -> VerificationCondition v
PointerAnalysis Word64
a PointerAnalysisResult v
par) Set (VerificationCondition v)
vcs)











-- | Given the address of an operand of an instruction, resolve it given the current state.
sresolve_address :: WithAbstractSymbolicValues ctxt v p => ctxt -> Operand -> State (Sstate v p,VCS v) v
sresolve_address :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt (Op_Mem BitSize
si BitSize
aSi Register
reg Register
idx Word8
scale Key
displ (Just SReg
seg)) =  do
  v
ra0 <- ctxt -> Operand -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt (BitSize
-> BitSize
-> Register
-> Register
-> Word8
-> Key
-> Maybe SReg
-> Operand
Op_Mem BitSize
si (Key -> BitSize
BitSize Key
64) Register
reg Register
idx Word8
scale Key
displ Maybe SReg
forall a. Maybe a
Nothing)
  v
ra1 <- ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt (Register -> State (Sstate v p, VCS v) v)
-> Register -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ SReg -> Register
RegSeg SReg
seg
  v -> State (Sstate v p, VCS v) v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, VCS v) v)
-> v -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues 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 (Op_Mem BitSize
si (BitSize Key
64) Register
reg Register
idx Word8
scale Key
displ Maybe SReg
Nothing)
  | Word8
scale Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word8
0 Bool -> Bool -> Bool
&& Register
idx Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
/= Register
RegNone = do
    v
idx_val <- ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt Register
idx
    let ra1 :: v
ra1 = ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues 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
idx_val (ctxt -> Word8 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Word8
scale)
    v
ra0 <- ctxt -> Register -> Key -> State (Sstate v p, VCS v) v
forall {a} {ctxt} {a} {p}.
(Integral a, WithAbstractSymbolicValues ctxt a p) =>
ctxt -> Register -> a -> StateT (Sstate a p, VCS a) Identity a
add_base_displ ctxt
ctxt Register
reg Key
displ
    v -> State (Sstate v p, VCS v) v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> State (Sstate v p, VCS v) v)
-> v -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues 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
  | Bool
otherwise = ctxt -> Register -> Key -> State (Sstate v p, VCS v) v
forall {a} {ctxt} {a} {p}.
(Integral a, WithAbstractSymbolicValues ctxt a p) =>
ctxt -> Register -> a -> StateT (Sstate a p, VCS a) Identity a
add_base_displ ctxt
ctxt Register
reg Key
displ

add_base_displ :: ctxt -> Register -> a -> StateT (Sstate a p, VCS a) Identity a
add_base_displ ctxt
ctxt Register
RegNone a
displ = a -> StateT (Sstate a p, VCS a) Identity a
forall a. a -> StateT (Sstate a p, VCS a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StateT (Sstate a p, VCS a) Identity a)
-> a -> StateT (Sstate a p, VCS a) Identity a
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> a
forall i. Integral i => ctxt -> i -> a
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
displ :: Word64)
add_base_displ ctxt
ctxt Register
reg a
displ = do
  a
ra0 <- ctxt -> Register -> StateT (Sstate a p, VCS a) Identity a
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt Register
reg
  a -> StateT (Sstate a p, VCS a) Identity a
forall a. a -> StateT (Sstate a p, VCS a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StateT (Sstate a p, VCS a) Identity a)
-> a -> StateT (Sstate a p, VCS a) Identity a
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation a -> a
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt String
"plus" (SymbolicOperation a -> a) -> SymbolicOperation a -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> SymbolicOperation a
forall v. v -> v -> SymbolicOperation v
SO_Plus a
ra0 (a -> SymbolicOperation a) -> a -> SymbolicOperation a
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> a
forall i. Integral i => ctxt -> i -> a
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
displ :: Word64) 



sread_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Operand -> State (Sstate v p,VCS v) v
--sread_operand ctxt msg op | trace ("sgeneric_cinstr: "++ show op) False = error "trace"
sread_operand :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
sread_operand ctxt
ctxt String
msg    (Op_Imm (Immediate (BitSize Key
64) Word64
a))  = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Word64
a
sread_operand ctxt
ctxt String
msg    (Op_Imm (Immediate (BitSize Key
32) Word64
a))  = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall {a}. (Bits a, Num a) => a -> a
sextend_32_64 Word64
a
sread_operand ctxt
ctxt String
msg    (Op_Imm (Immediate (BitSize Key
16) Word64
a))  = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall {a}. (Bits a, Num a) => a -> a
sextend_16_64 Word64
a
sread_operand ctxt
ctxt String
msg    (Op_Imm (Immediate (BitSize Key
8) Word64
a))   = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64
forall {a}. (Bits a, Num a) => a -> a
sextend_8_64 Word64
a
sread_operand ctxt
ctxt String
msg    (Op_Const Key
c)                         = v -> StateT (Sstate v p, VCS v) Identity v
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> StateT (Sstate v p, VCS v) Identity v)
-> v -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ ctxt -> Key -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Key -> v) -> Key -> v
forall a b. (a -> b) -> a -> b
$ Key
c
sread_operand ctxt
ctxt String
msg    (Op_Reg Register
r)                           = ctxt -> Register -> StateT (Sstate v p, VCS v) Identity v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt Register
r
sread_operand ctxt
ctxt String
msg    (Op_Near Operand
op)                         = ctxt -> String -> Operand -> StateT (Sstate v p, VCS v) Identity v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
sread_operand ctxt
ctxt String
msg Operand
op
sread_operand ctxt
ctxt String
msg op :: Operand
op@(Op_Mem (BitSize Key
si) BitSize
_ Register
_ Register
_ Word8
_ Key
_ Maybe SReg
_) = do
  v
resolved_address <- ctxt -> Operand -> StateT (Sstate v p, VCS v) Identity v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt Operand
op
  ctxt
-> String
-> v
-> Maybe ByteSize
-> StateT (Sstate v p, VCS v) Identity v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> v -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem ctxt
ctxt String
msg v
resolved_address (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Key -> ByteSize
ByteSize (Key
si Key -> Key -> Key
forall a. Integral a => a -> a -> a
`div` Key
8))

sread_operand ctxt
ctxt String
msg    Operand
op  = String -> StateT (Sstate v p, VCS v) Identity v
forall a. HasCallStack => String -> a
error (String -> StateT (Sstate v p, VCS v) Identity v)
-> String -> StateT (Sstate v p, VCS v) Identity v
forall a b. (a -> b) -> a -> b
$ (String, Operand) -> String
forall a. Show a => a -> String
show (String
msg,Operand
op)

swrite_operand :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Bool -> Operand -> v -> State (Sstate v p,VCS v) ()
swrite_operand :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
swrite_operand ctxt
ctxt Instruction
i Bool
use_existing_value    (Op_Reg Register
r)   v
v = ctxt
-> String -> Bool -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> Bool -> Register -> v -> State (Sstate v p, VCS v) ()
soverwrite_reg ctxt
ctxt (Instruction -> String
forall a. Show a => a -> String
show Instruction
i) Bool
use_existing_value Register
r v
v
swrite_operand ctxt
ctxt Instruction
i Bool
use_existing_value op :: Operand
op@(Op_Mem (BitSize Key
si) BitSize
_ Register
_ Register
_ Word8
_ Key
_ Maybe SReg
_) v
v = do
  v
resolved_address <- ctxt -> Operand -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt Operand
op
  ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem ctxt
ctxt Bool
use_existing_value v
resolved_address (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Key -> ByteSize
ByteSize (Key
si Key -> Key -> Key
forall a. Integral a => a -> a -> a
`div` Key
8)) v
v
swrite_operand ctxt
ctxt Instruction
i Bool
_ Operand
op v
v = String -> State (Sstate v p, VCS v) ()
forall a. HasCallStack => String -> a
error (String -> State (Sstate v p, VCS v) ())
-> String -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ (Instruction, Operand) -> String
forall a. Show a => a -> String
show (Instruction
i,Operand
op)





-- TODO JE, other JMP aboves and JUMP lesses
add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus
add_jump_to_pred :: Instruction -> Instruction -> FlagStatus -> FlagStatus
add_jump_to_pred i0 :: Instruction
i0@(Instruction Word64
_ [Prefix]
_ Opcode
JA Maybe Operand
_ [Op_Jmp (Immediate BitSize
_ Word64
trgt)] Key
_) Instruction
i1 FlagStatus
flg =
  case FlagStatus
flg of
    FS_CMP Maybe Bool
b Operand
o1 Operand
o2 -> if Instruction -> Word64
inAddress 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 Word64
_ [Prefix]
_ Opcode
JBE Maybe Operand
_ [Op_Jmp (Immediate BitSize
_ Word64
trgt)] Key
_) Instruction
i1 FlagStatus
flg =
  case FlagStatus
flg of
    FS_CMP Maybe Bool
b Operand
o1 Operand
o2 -> if Instruction -> Word64
inAddress 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 :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p,VCS v) ()
sreturn :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sreturn ctxt
ctxt Instruction
i = do
  v
rsp_value <- ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt (GPR -> Register
Reg64 GPR
RSP)
  v
ret_addr <- ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
sread_operand ctxt
ctxt String
"return" (Operand -> State (Sstate v p, VCS v) v)
-> Operand -> State (Sstate v p, VCS v) v
forall a b. (a -> b) -> a -> b
$ ByteSize -> Operand
mk_RSP_mem_operand (Key -> ByteSize
ByteSize Key
8)
  let rsp8 :: v
rsp8 = ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues 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
rsp_value (v -> SymbolicOperation v) -> v -> SymbolicOperation v
forall a b. (a -> b) -> a -> b
$ ctxt -> Integer -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Integer
8
  ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
"sret1" (GPR -> Register
Reg64 GPR
RSP) v
rsp8
  ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
"sret2" (GPR -> Register
Reg64 GPR
RIP) v
ret_addr


-- LEA
slea :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> Operand -> Operand -> State (Sstate v p,VCS v) ()
slea :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Operand
-> Operand
-> State (Sstate v p, VCS v) ()
slea ctxt
ctxt Instruction
i Operand
dst Operand
op = do
  v
e <- ctxt -> Operand -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt Operand
op
  ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
swrite_operand ctxt
ctxt Instruction
i Bool
True Operand
dst v
e
  if Operand -> Bool
rip_relative Operand
op then
    case ctxt -> v -> Maybe Word64
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> v -> Maybe Word64
stry_immediate ctxt
ctxt v
e of
      Maybe Word64
Nothing  -> () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just Word64
imm -> if (ctxt -> Word64 -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Word64 -> Bool
saddress_has_instruction ctxt
ctxt Word64
imm) then ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> State (Sstate v p, VCS v) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, VCS v) -> (Sstate v p, VCS v))
 -> State (Sstate v p, VCS v) ())
-> ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ Word64 -> Key -> (Sstate v p, VCS v) -> (Sstate v p, VCS v)
forall {v} {a}.
Ord v =>
Word64
-> Key
-> (a, Set (VerificationCondition v))
-> (a, Set (VerificationCondition v))
add_function_pointer (Instruction -> Word64
inAddress Instruction
i) (Key -> (Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> Key -> (Sstate v p, VCS v) -> (Sstate v p, VCS v)
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, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  else
    () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  rip_relative :: Operand -> Bool
rip_relative (Op_Mem BitSize
_ BitSize
_ Register
r0 Register
r1 Word8
_ Key
_ Maybe SReg
_) = GPR -> Register
Reg64 GPR
RIP Register -> [Register] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Register
r0,Register
r1]

-- MOV
smov :: WithAbstractSymbolicValues ctxt v p => ctxt -> a -> Instruction -> State (Sstate v p,VCS v) ()
smov :: forall ctxt v p a.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> a -> Instruction -> State (Sstate v p, VCS v) ()
smov ctxt
ctxt a
a i :: Instruction
i@(Instruction Word64
label [Prefix]
prefix Opcode
MOV (Just Operand
dst) [src :: Operand
src@(Op_Imm Immediate
_)] Key
annot)
  -- | saddress_has_instruction ctxt imm   = slea ctxt label dst (EffectiveAddress (AddressImm imm))
  | Bool
otherwise                           = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sgeneric_cinstr ctxt
ctxt Instruction
i
smov ctxt
ctxt a
a Instruction
i                           = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sgeneric_cinstr ctxt
ctxt Instruction
i


sgeneric_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p,VCS v) ()
--sgeneric_cinstr ctxt i | trace ("sgeneric_cinstr: "++ show i) False = error "trace"
sgeneric_cinstr :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sgeneric_cinstr ctxt
ctxt i :: Instruction
i@(Instruction Word64
label [Prefix]
prefix Opcode
mnemonic (Just Operand
dst) [Operand]
srcs Key
annot) = do
  [v]
ops <- (Operand -> StateT (Sstate v p, VCS v) Identity v)
-> [Operand] -> StateT (Sstate v p, VCS v) Identity [v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ctxt -> String -> Operand -> StateT (Sstate v p, VCS v) Identity v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Operand -> State (Sstate v p, VCS v) v
sread_operand ctxt
ctxt (Instruction -> String
forall a. Show a => a -> String
show Instruction
i)) [Operand]
srcs
  ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
swrite_operand ctxt
ctxt Instruction
i Bool
True Operand
dst (v -> State (Sstate v p, VCS v) ())
-> v -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> SymbolicOperation v -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> SymbolicOperation v -> v
ssemantics ctxt
ctxt (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 (ByteSize -> Key
byteSize (ByteSize -> Key) -> ByteSize -> Key
forall a b. (a -> b) -> a -> b
$ Operand -> ByteSize
operand_size Operand
dst) (ByteSize -> Key
byteSize (ByteSize -> Key) -> Maybe ByteSize -> Maybe Key
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Operand] -> Maybe ByteSize
maybe_operand_size [Operand]
srcs) [v]
ops


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

sexec_cinstr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p,VCS v) ()
--sexec_cinstr ctxt i | trace ("sexec_cinstr: "++ show i) False = error "trace"
sexec_cinstr :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sexec_cinstr ctxt
ctxt i :: Instruction
i@(Instruction Word64
label [Prefix]
prefix Opcode
mnemonic (Just Operand
dst) [Operand]
srcs Key
annot)
  | Opcode
mnemonic Opcode -> Opcode -> Bool
forall a. Eq a => a -> a -> Bool
== Opcode
LEA                      = ctxt
-> Instruction
-> Operand
-> Operand
-> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Operand
-> Operand
-> State (Sstate v p, VCS v) ()
slea ctxt
ctxt Instruction
i Operand
dst (Operand -> State (Sstate v p, VCS v) ())
-> Operand -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ [Operand] -> Operand
forall a. HasCallStack => [a] -> a
head [Operand]
srcs
  | Opcode
mnemonic Opcode -> Opcode -> Bool
forall a. Eq a => a -> a -> Bool
== Opcode
MOV                      = ctxt -> v -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p a.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> a -> Instruction -> State (Sstate v p, VCS v) ()
smov ctxt
ctxt (ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt String
"") Instruction
i
  | Opcode
mnemonic Opcode -> [Opcode] -> Bool
forall a. Eq a => a -> [a] -> 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. HasCallStack => [a] -> a
head [Operand]
srcs = ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Instruction
-> Bool
-> Operand
-> v
-> State (Sstate v p, VCS v) ()
swrite_operand ctxt
ctxt Instruction
i Bool
False Operand
dst (v -> State (Sstate v p, VCS v) ())
-> v -> State (Sstate v p, VCS v) ()
forall a b. (a -> b) -> a -> b
$ ctxt -> Integer -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt Integer
0
  | Bool
otherwise                                = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sgeneric_cinstr ctxt
ctxt Instruction
i
 where
  xors :: [Opcode]
xors = [Opcode
XOR,Opcode
PXOR]
sexec_cinstr ctxt
ctxt i :: Instruction
i@(Instruction Word64
label [Prefix]
prefix Opcode
mnemonic Maybe Operand
Nothing [Operand]
_ Key
_)
  | Opcode -> Bool
isRet Opcode
mnemonic        = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sreturn ctxt
ctxt Instruction
i
  | Opcode -> Bool
isJump Opcode
mnemonic       = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sjump ctxt
ctxt Instruction
i
  | Opcode -> Bool
isCall Opcode
mnemonic       = ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
scall ctxt
ctxt Instruction
i
  | Bool
otherwise             = () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()






sset_rip :: WithAbstractSymbolicValues ctxt v p => ctxt -> Instruction -> State (Sstate v p,VCS v) ()
sset_rip :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sset_rip ctxt
ctxt Instruction
i = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
"sset_rip" (GPR -> Register
Reg64 GPR
RIP) (ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
inAddress 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
inSize Instruction
i))

sexec_instr :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> Instruction -> State (Sstate v p,VCS v) ()
--sexec_instr ctxt i | trace ("sexec_isntr: "++ show i) False = error "trace"
sexec_instr :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) ()
sexec_instr ctxt
ctxt Bool
store_pointer_analysis Instruction
i = do
  ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sset_rip ctxt
ctxt Instruction
i

  let i_c :: [Instruction]
i_c = Instruction -> [Instruction]
canonicalize Instruction
i
  [Instruction] -> State (Sstate v p, VCS v) ()
forall {m :: * -> *}.
MonadState (Sstate v p, VCS v) m =>
[Instruction] -> m ()
maybe_store_pointer_analysis_result [Instruction]
i_c
  (Instruction -> State (Sstate v p, VCS v) ())
-> [Instruction] -> State (Sstate v p, VCS v) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ctxt -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Instruction -> State (Sstate v p, VCS v) ()
sexec_cinstr ctxt
ctxt) [Instruction]
i_c
  ctxt -> v -> Instruction -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> v -> Instruction -> State (Sstate v p, VCS v) ()
swrite_flags ctxt
ctxt (ctxt -> String -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v
top ctxt
ctxt String
"") Instruction
i 
 where
  maybe_store_pointer_analysis_result :: [Instruction] -> m ()
maybe_store_pointer_analysis_result [Instruction]
i_c
    | Instruction -> Opcode
inOperation Instruction
i Opcode -> Opcode -> Bool
forall a. Eq a => a -> a -> Bool
== Opcode
LEA = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
store_pointer_analysis = do
      Maybe (PointerAnalysisResult v)
par <- ((Sstate v p, VCS v) -> Maybe (PointerAnalysisResult v))
-> m (Maybe (PointerAnalysisResult v))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (((Sstate v p, VCS v) -> Maybe (PointerAnalysisResult v))
 -> m (Maybe (PointerAnalysisResult v)))
-> ((Sstate v p, VCS v) -> Maybe (PointerAnalysisResult v))
-> m (Maybe (PointerAnalysisResult v))
forall a b. (a -> b) -> a -> b
$ [Instruction]
-> (Sstate v p, VCS v) -> Maybe (PointerAnalysisResult v)
forall {b}.
[Instruction] -> (Sstate v p, b) -> Maybe (PointerAnalysisResult v)
mk_pointer_analysis_result [Instruction]
i_c
      case Maybe (PointerAnalysisResult v)
par of
        Maybe (PointerAnalysisResult v)
Nothing  -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just PointerAnalysisResult v
par -> ((Sstate v p, VCS v) -> (Sstate v p, VCS v)) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, VCS v) -> (Sstate v p, VCS v)) -> m ())
-> ((Sstate v p, VCS v) -> (Sstate v p, VCS v)) -> m ()
forall a b. (a -> b) -> a -> b
$ Word64
-> PointerAnalysisResult v
-> (Sstate v p, VCS v)
-> (Sstate v p, VCS v)
forall {v} {a}.
Ord v =>
Word64
-> PointerAnalysisResult v
-> (a, Set (VerificationCondition v))
-> (a, Set (VerificationCondition v))
add_pa_result (Instruction -> Word64
inAddress Instruction
i) PointerAnalysisResult v
par
    | Bool
otherwise = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  mk_pointer_analysis_result :: [Instruction] -> (Sstate v p, b) -> Maybe (PointerAnalysisResult v)
mk_pointer_analysis_result [Instruction]
i_c (Sstate v p
p,b
_) = 
    let (Maybe Operand
dst,[Operand]
srcs)   = (Instruction -> Maybe Operand
inDest (Instruction -> Maybe Operand) -> Instruction -> Maybe Operand
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
head [Instruction]
i_c, Instruction -> [Operand]
inOperands (Instruction -> [Operand]) -> Instruction -> [Operand]
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
head [Instruction]
i_c)
        resolved_w :: Maybe v
resolved_w   = Maybe Operand
dst Maybe Operand -> (Operand -> Maybe v) -> Maybe v
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sstate v p -> Operand -> Maybe v
resolve_mem_operand Sstate v p
p 
        resolved_rs :: [Maybe v]
resolved_rs  = (Operand -> Maybe v) -> [Operand] -> [Maybe v]
forall a b. (a -> b) -> [a] -> [b]
map (Sstate v p -> Operand -> Maybe v
resolve_mem_operand Sstate v p
p) [Operand]
srcs in
      --if any ((==) (Just $ top ctxt "")) (resolved_w:resolved_rs) then
      --  traceShow ("TOP PTR: " ++ show i_c ++ "\n" ++ show p) $ Just $ PointerAnalysisResult resolved_w resolved_rs
      --else
      if (Maybe v -> Bool) -> [Maybe v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe v -> Maybe v -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe v
forall a. Maybe a
Nothing) (Maybe v
resolved_wMaybe v -> [Maybe v] -> [Maybe v]
forall a. a -> [a] -> [a]
:[Maybe v]
resolved_rs) then
        PointerAnalysisResult v -> Maybe (PointerAnalysisResult v)
forall a. a -> Maybe a
Just (PointerAnalysisResult v -> Maybe (PointerAnalysisResult v))
-> PointerAnalysisResult v -> Maybe (PointerAnalysisResult v)
forall a b. (a -> b) -> a -> b
$ Maybe v -> [Maybe v] -> PointerAnalysisResult v
forall v. Maybe v -> [Maybe v] -> PointerAnalysisResult v
PointerAnalysisResult Maybe v
resolved_w [Maybe v]
resolved_rs
      else
        Maybe (PointerAnalysisResult v)
forall a. Maybe a
Nothing


  resolve_mem_operand :: Sstate v p -> Operand -> Maybe v
resolve_mem_operand Sstate v p
p op :: Operand
op@(Op_Mem BitSize
si BitSize
_ Register
base Register
idx Word8
scale Key
displ Maybe SReg
seg) = v -> Maybe v
forall a. a -> Maybe a
Just (v -> Maybe v) -> v -> Maybe v
forall a b. (a -> b) -> a -> b
$ State (Sstate v p, VCS v) v -> Sstate v p -> v
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate (ctxt -> Operand -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Operand -> State (Sstate v p, VCS v) v
sresolve_address ctxt
ctxt Operand
op) Sstate v p
p
  resolve_mem_operand Sstate v p
p Operand
_ = Maybe v
forall a. Maybe a
Nothing 



sexec_block :: WithAbstractSymbolicValues ctxt v p => ctxt -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p,VCS v) ()
sexec_block :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (Sstate v p, VCS v) ()
sexec_block ctxt
ctxt Bool
store_pointer_analysis []    Maybe [Instruction]
_    = () -> StateT (Sstate v p, VCS v) Identity ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--sexec_block ctxt block next | trace ("sexec_block: "++ show (head block)) False = error "trace"
sexec_block ctxt
ctxt Bool
store_pointer_analysis [Instruction]
block Maybe [Instruction]
next = StateT (Sstate v p, VCS v) Identity ()
run
 where 
  run :: StateT (Sstate v p, VCS v) Identity ()
run = do
    (Instruction -> StateT (Sstate v p, VCS v) Identity ())
-> [Instruction] -> StateT (Sstate v p, VCS v) Identity [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ctxt
-> Bool -> Instruction -> StateT (Sstate v p, VCS v) Identity ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Bool -> Instruction -> State (Sstate v p, VCS v) ()
sexec_instr ctxt
ctxt Bool
store_pointer_analysis) [Instruction]
block
    Maybe [Instruction] -> StateT (Sstate v p, VCS v) Identity ()
set_flagstatus Maybe [Instruction]
next

  set_flagstatus :: Maybe [Instruction] -> StateT (Sstate v p, VCS v) Identity ()
set_flagstatus Maybe [Instruction]
Nothing       = () -> StateT (Sstate v p, VCS v) Identity ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  set_flagstatus (Just (Instruction
i':[Instruction]
_)) = do
    ctxt
-> String
-> Register
-> v
-> StateT (Sstate v p, VCS v) Identity ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_reg ctxt
ctxt String
"set_rip" (GPR -> Register
Reg64 GPR
RIP) (ctxt -> Word64 -> v
forall i. Integral i => ctxt -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate ctxt
ctxt (Word64 -> v) -> Word64 -> v
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
inAddress Instruction
i')
    ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> StateT (Sstate v p, VCS v) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Sstate v p, VCS v) -> (Sstate v p, VCS v))
 -> StateT (Sstate v p, VCS v) Identity ())
-> ((Sstate v p, VCS v) -> (Sstate v p, VCS v))
-> StateT (Sstate v p, VCS v) Identity ()
forall a b. (a -> b) -> a -> b
$ \(Sstate v p
s,VCS v
vcs) -> (Sstate v p
s { sflags = add_jump_to_pred (last block) i' (sflags s) }, VCS v
vcs)



sjoin_mem :: WithAbstractSymbolicValues ctxt v p => ctxt -> String -> Sstate v p -> Sstate v p -> M.Map (p, Maybe ByteSize) v
sjoin_mem :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> Sstate v p -> Sstate v p -> Map (p, Maybe ByteSize) v
sjoin_mem ctxt
ctxt String
msg Sstate v p
s0 Sstate v p
s1 =
  let shared :: Map (p, Maybe ByteSize) v
shared  = (v -> v -> v)
-> Map (p, Maybe ByteSize) v
-> Map (p, Maybe ByteSize) v
-> Map (p, Maybe ByteSize) 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
join_values (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s0) (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s1)
      from_s1 :: [(((p, Maybe ByteSize), v), Sstate v p)]
from_s1 = (((p, Maybe ByteSize), v)
 -> (((p, Maybe ByteSize), v), Sstate v p))
-> [((p, Maybe ByteSize), v)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
forall a b. (a -> b) -> [a] -> [b]
map (\((p, Maybe ByteSize), v)
r -> (((p, Maybe ByteSize), v)
r,Sstate v p
s0)) ([((p, Maybe ByteSize), v)]
 -> [(((p, Maybe ByteSize), v), Sstate v p)])
-> [((p, Maybe ByteSize), v)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)])
-> Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v
-> Map (p, Maybe ByteSize) v -> Map (p, Maybe ByteSize) v
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s1) (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s0)
      from_s0 :: [(((p, Maybe ByteSize), v), Sstate v p)]
from_s0 = (((p, Maybe ByteSize), v)
 -> (((p, Maybe ByteSize), v), Sstate v p))
-> [((p, Maybe ByteSize), v)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
forall a b. (a -> b) -> [a] -> [b]
map (\((p, Maybe ByteSize), v)
r -> (((p, Maybe ByteSize), v)
r,Sstate v p
s1)) ([((p, Maybe ByteSize), v)]
 -> [(((p, Maybe ByteSize), v), Sstate v p)])
-> [((p, Maybe ByteSize), v)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)])
-> Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v
-> Map (p, Maybe ByteSize) v -> Map (p, Maybe ByteSize) v
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s0) (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
s1) in
    Map (p, Maybe ByteSize) v
-> [(((p, Maybe ByteSize), v), Sstate v p)]
-> Map (p, Maybe ByteSize) v
sjoin_mem' Map (p, Maybe ByteSize) v
shared ([(((p, Maybe ByteSize), v), Sstate v p)]
 -> Map (p, Maybe ByteSize) v)
-> [(((p, Maybe ByteSize), v), Sstate v p)]
-> Map (p, Maybe ByteSize) v
forall a b. (a -> b) -> a -> b
$ [(((p, Maybe ByteSize), v), Sstate v p)]
from_s1 [(((p, Maybe ByteSize), v), Sstate v p)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
-> [(((p, Maybe ByteSize), v), Sstate v p)]
forall a. [a] -> [a] -> [a]
++ [(((p, Maybe ByteSize), v), Sstate v p)]
from_s0
 where
  sjoin_mem' :: Map (p, Maybe ByteSize) v
-> [(((p, Maybe ByteSize), v), Sstate v p)]
-> Map (p, Maybe ByteSize) v
sjoin_mem' Map (p, Maybe ByteSize) v
m [] = Map (p, Maybe ByteSize) v
m 
  sjoin_mem' Map (p, Maybe ByteSize) v
m ((((p
a,Maybe ByteSize
si),v
v),Sstate v p
s'):[(((p, Maybe ByteSize), v), Sstate v p)]
rest) =
    let v' :: v
v' = State (Sstate v p, VCS v) v -> Sstate v p -> v
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate (ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> State (Sstate v p, VCS v) v
sread_mem_from_ptr ctxt
ctxt (String
"joinmem" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (p, Maybe ByteSize, Sstate v p, Sstate v p) -> String
forall a. Show a => a -> String
show (p
a,Maybe ByteSize
si,Sstate v p
s0,Sstate v p
s1)String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++String
msg) p
a Maybe ByteSize
si) Sstate v p
s'
        j :: v
j  = v -> v -> v
join_values v
v v
v'
        m' :: Map (p, Maybe ByteSize) v
m' = Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem (Sstate v p -> Map (p, Maybe ByteSize) v)
-> Sstate v p -> Map (p, Maybe ByteSize) v
forall a b. (a -> b) -> a -> b
$ State (Sstate v p, VCS v) () -> Sstate v p -> Sstate v p
forall v p b.
State (Sstate v p, VCS v) b -> Sstate v p -> Sstate v p
execSstate (ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> p -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem_to_ptr ctxt
ctxt Bool
True p
a Maybe ByteSize
si v
j) (Sstate v p -> Sstate v p) -> Sstate v p -> Sstate v p
forall a b. (a -> b) -> a -> b
$ Sstate {sregs :: Map Register v
sregs = Map Register v
forall k a. Map k a
M.empty, smem :: Map (p, Maybe ByteSize) v
smem = Map (p, Maybe ByteSize) v
m, sflags :: FlagStatus
sflags = FlagStatus
None} in
      Map (p, Maybe ByteSize) v
-> [(((p, Maybe ByteSize), v), Sstate v p)]
-> Map (p, Maybe ByteSize) v
sjoin_mem' Map (p, Maybe ByteSize) v
m' [(((p, Maybe ByteSize), v), Sstate v p)]
rest

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

sjoin_regs :: WithAbstractSymbolicValues ctxt v p => ctxt -> M.Map Register v -> M.Map Register v -> M.Map Register v
sjoin_regs :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Map Register v -> Map Register v -> Map Register v
sjoin_regs ctxt
ctxt Map Register v
r0 Map Register v
r1 = 
  let regs :: Map Register v
regs  = (Register -> v -> v -> v)
-> Map Register v -> Map Register v -> Map Register v
forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWithKey Register -> v -> v -> v
forall {a}. Show a => a -> v -> v -> v
join_reg Map Register v
r0 Map Register v
r1
      from0 :: Map Register v
from0 = (Register -> v -> v) -> Map Register v -> Map Register v
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\Register
r v
v0 -> v -> Register -> v
join_with_init_value v
v0 Register
r) (Map Register v -> Map Register v)
-> Map Register v -> Map Register v
forall a b. (a -> b) -> a -> b
$ Map Register v -> Map Register v -> Map Register v
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map Register v
r0 Map Register v
r1
      from1 :: Map Register v
from1 = (Register -> v -> v) -> Map Register v -> Map Register v
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\Register
r v
v1 -> v -> Register -> v
join_with_init_value v
v1 Register
r) (Map Register v -> Map Register v)
-> Map Register v -> Map Register v
forall a b. (a -> b) -> a -> b
$ Map Register v -> Map Register v -> Map Register v
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map Register v
r1 Map Register v
r0 in
    [Map Register v] -> Map Register v
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions [Map Register v
regs,Map Register v
from0,Map Register v
from1]
 where
  join_reg :: a -> v -> v -> v
join_reg a
r 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 :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
"joinregs"String -> String -> String
forall a. [a] -> [a] -> [a]
++a -> String
forall a. Show a => a -> String
show a
r) [v
a,v
b]

  join_with_init_value :: v -> Register -> v
join_with_init_value v
v Register
r = ctxt -> String -> [v] -> v
forall ctxt v p (t :: * -> *).
(WithAbstractSymbolicValues ctxt v p, Foldable t) =>
ctxt -> String -> t v -> v
forall (t :: * -> *). Foldable t => ctxt -> String -> t v -> v
sjoin_values ctxt
ctxt (String
"joinregs2"String -> String -> String
forall a. [a] -> [a] -> [a]
++Register -> String
forall a. Show a => a -> String
show Register
r) [v
v, ctxt -> Register -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> v
smk_init_reg_value ctxt
ctxt Register
r]
  

--sjoin_states ctxt msg s0 s1 | trace ("sjoin_states") False = error "trace"
sjoin_states :: p -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states p
ctxt String
msg s0 :: Sstate v p
s0@(Sstate Map Register v
regs0 Map (p, Maybe ByteSize) v
mem0 FlagStatus
flg0) s1 :: Sstate v p
s1@(Sstate Map Register v
regs1 Map (p, Maybe ByteSize) v
mem1 FlagStatus
flg1) =
  let flg :: FlagStatus
flg  = FlagStatus -> FlagStatus -> FlagStatus
join_flags FlagStatus
flg0 FlagStatus
flg1
      regs :: Map Register v
regs = p -> Map Register v -> Map Register v -> Map Register v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Map Register v -> Map Register v -> Map Register v
sjoin_regs p
ctxt Map Register v
regs0 Map Register v
regs1
      mem :: Map (p, Maybe ByteSize) v
mem  = p
-> String -> Sstate v p -> Sstate v p -> Map (p, Maybe ByteSize) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> Sstate v p -> Sstate v p -> Map (p, Maybe ByteSize) v
sjoin_mem p
ctxt String
msg Sstate v p
s0 Sstate v p
s1
      s' :: Sstate v p
s'   = Map Register v
-> Map (p, Maybe ByteSize) v -> FlagStatus -> Sstate v p
forall v p.
Map Register v
-> Map (p, Maybe ByteSize) v -> FlagStatus -> Sstate v p
Sstate Map Register v
regs Map (p, Maybe ByteSize) v
mem FlagStatus
flg in
     Sstate v p
s'
 where
  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
        (Op_Imm (Immediate BitSize
si0 Word64
n0),Op_Imm (Immediate BitSize
si1 Word64
n1)) -> Maybe Bool -> Operand -> Operand -> FlagStatus
FS_CMP (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) Operand
o0 (Immediate -> Operand
Op_Imm (Immediate -> Operand) -> Immediate -> Operand
forall a b. (a -> b) -> a -> b
$ BitSize -> Word64 -> Immediate
Immediate (BitSize -> BitSize -> BitSize
forall a. Ord a => a -> a -> a
max BitSize
si0 BitSize
si1) (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 :: WithAbstractSymbolicValues ctxt v p => ctxt -> [Sstate v p] -> Sstate v p
supremum :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
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 a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (ctxt -> String -> Sstate v p -> Sstate v p -> Sstate v p
forall {p} {v} {p}.
WithAbstractSymbolicValues p v p =>
p -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states ctxt
ctxt String
"supremum") [Sstate v p]
ss

simplies :: p -> Sstate v p -> Sstate v p -> Bool
simplies p
ctxt Sstate v p
s0 Sstate v p
s1 = 
  let j :: Sstate v p
j = 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
$ p -> String -> Sstate v p -> Sstate v p -> Sstate v p
forall {p} {v} {p}.
WithAbstractSymbolicValues p v p =>
p -> String -> Sstate v p -> Sstate v p -> Sstate v p
sjoin_states p
ctxt String
"simplies" (Sstate v p
s0 {sflags = None}) (Sstate v p
s1 {sflags = None}) in
    if Sstate v p
j 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 {sflags = None}) then
      Bool
True
    else
      Bool
False -- trace ("s0:\n" ++ show s0 ++ "\ns1:\n" ++ show s1 ++ "\nj:\n" ++ show j) False
 where
  set_rip :: Sstate v p -> Sstate v p
set_rip = State (Sstate v p, VCS v) () -> Sstate v p -> Sstate v p
forall v p b.
State (Sstate v p, VCS v) b -> Sstate v p -> Sstate v p
execSstate (p -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg p
ctxt String
"simplies" (GPR -> Register
Reg64 GPR
RIP) (p -> Integer -> v
forall i. Integral i => p -> i -> v
forall ctxt v p i.
(WithAbstractSymbolicValues ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate p
ctxt Integer
0))



sverify_postcondition :: WithAbstractSymbolicValues ctxt v p => ctxt -> Sstate v p -> Bool
sverify_postcondition :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Sstate v p -> Bool
sverify_postcondition ctxt
ctxt = State (Sstate v p, VCS v) Bool -> Sstate v p -> Bool
forall v p a. State (Sstate v p, VCS v) a -> Sstate v p -> a
evalSstate State (Sstate v p, VCS v) Bool
check
 where
  check :: State (Sstate v p, VCS v) Bool
check = do
    v
rsp <- ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt (GPR -> Register
Reg64 GPR
RSP)
    v
rip <- ctxt -> Register -> State (Sstate v p, VCS v) v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> State (Sstate v p, VCS v) v
sread_reg ctxt
ctxt (GPR -> Register
Reg64 GPR
RIP)
    Bool -> State (Sstate v p, VCS v) Bool
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> State (Sstate v p, VCS v) Bool)
-> Bool -> State (Sstate v p, VCS v) Bool
forall a b. (a -> b) -> a -> b
$ ctxt -> v -> v -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> v -> v -> Bool
scheck_regs_in_postcondition ctxt
ctxt v
rip v
rsp