{-# LANGUAGE DeriveGeneric, DefaultSignatures, Strict, StandaloneDeriving, BangPatterns #-}

{-|
Module      : Context
Description : A @"Context"@ stores all the information retrieved from the binary, as well as the command-line parameters passed to FoxDec.

The context stores, among others, information obtained during verification, such as CFGs, invariants, etc. (see @`Context`@).
Module "VerificationReportInterface" provides functions for obtaining and interfacing with a @Context@.
-}


module Analysis.Context where

import Base
import Config

import Analysis.Capstone

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

import Generic.Binary
import Generic.SymbolicConstituents

import Instantiation.BinaryElf
import Instantiation.BinaryMacho

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


import Data.List ( find, intercalate )
import Data.Word (Word8,Word64)
import Data.Maybe (mapMaybe,fromJust)
import qualified Data.ByteString as BS
import Data.IORef
import Data.Int (Int64)


import GHC.Generics
import qualified Data.Serialize as Cereal hiding (get,put)
import X86.Register (Register)
import X86.Opcode (isCall)
import X86.Conventions
import qualified X86.Instruction as X86
import qualified X86.Operand as X86
import X86.Operand (GenericOperand(..))
import Generic.Operand (GenericOperand(..)) -- TODO: why is this needed?
import qualified Generic.Instruction as Instr
import Generic.Instruction (GenericInstruction(Instruction))
import X86.Opcode (Opcode(JMP), isCall, isJump)

import System.Directory (doesFileExist)
import System.IO.Unsafe (unsafePerformIO)

import Control.DeepSeq


-- | The context augmented with information on the current function
data FContext = FContext {
  FContext -> Context
f_ctxt  :: Context,   -- ^ The context
  FContext -> Int
f_entry :: Int,       -- ^ The entry address of the current function
  FContext -> FInit
f_init  :: FInit      -- ^ The initialization of the current function
 }

mk_fcontext :: Context -> Int -> FContext
mk_fcontext :: Context -> Int -> FContext
mk_fcontext Context
ctxt Int
entry =
  let -- f     = function_name_of_entry ctxt entry
      finit :: Maybe FInit
finit = Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt
      fctxt :: FContext
fctxt = Context -> Int -> FInit -> FContext
FContext Context
ctxt Int
entry (Maybe FInit
finit Maybe FInit -> FInit -> FInit
forall a. Eq a => Maybe a -> a -> a
`orElse` FInit
init_finit) in
    FContext
fctxt

-- | Reading a binary given a filename (ELF or MachO)
read_binary :: String -> String -> IO (Maybe Binary)
read_binary :: String -> String -> IO (Maybe Binary)
read_binary String
dirname String
name = do
  let filename :: String
filename = String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
  Bool
exists <- String -> IO Bool
doesFileExist String
filename
  if Bool
exists then do
    -- if the original binary is given, we now assume it its an ELF
    ByteString
content <-  String -> IO ByteString
BS.readFile String
filename
    if (ByteString -> [Word8]
BS.unpack (ByteString -> [Word8]) -> ByteString -> [Word8]
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take Int
4 ByteString
content) [Word8] -> [Word8] -> Bool
forall a. Eq a => a -> a -> Bool
== [Word8
0x7f, Word8
0x45, Word8
0x4C, Word8
0x46] then
      Maybe Binary -> IO (Maybe Binary)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Binary -> IO (Maybe Binary))
-> Maybe Binary -> IO (Maybe Binary)
forall a b. (a -> b) -> a -> b
$ Binary -> Maybe Binary
forall a. a -> Maybe a
Just (Binary -> Maybe Binary) -> Binary -> Maybe Binary
forall a b. (a -> b) -> a -> b
$ Elf -> Binary
forall b. BinaryClass b => b -> Binary
Binary (Elf -> Binary) -> Elf -> Binary
forall a b. (a -> b) -> a -> b
$ ByteString -> Elf
elf_read_file ByteString
content
    else
      Maybe Binary -> IO (Maybe Binary)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Binary
forall a. Maybe a
Nothing
  else do
    -- otherwise, see if the binary is contained in the following files (MachO)
    Bool
exists1 <- String -> IO Bool
doesFileExist (String
filename String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".dump")
    Bool
exists2 <- String -> IO Bool
doesFileExist (String
filename String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".data")
    Bool
exists3 <- String -> IO Bool
doesFileExist (String
filename String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sections")
    Bool
exists4 <- String -> IO Bool
doesFileExist (String
filename String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".symbols")
    Bool
exists5 <- String -> IO Bool
doesFileExist (String
filename String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".entry")
    if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
exists1,Bool
exists2,Bool
exists3,Bool
exists4,Bool
exists5] then do
      Macho
macho <- String -> String -> IO Macho
macho_read_file String
dirname String
name
      Maybe Binary -> IO (Maybe Binary)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Binary -> IO (Maybe Binary))
-> Maybe Binary -> IO (Maybe Binary)
forall a b. (a -> b) -> a -> b
$ Binary -> Maybe Binary
forall a. a -> Maybe a
Just (Binary -> Maybe Binary) -> Binary -> Maybe Binary
forall a b. (a -> b) -> a -> b
$ Macho -> Binary
forall b. BinaryClass b => b -> Binary
Binary (Macho -> Binary) -> Macho -> Binary
forall a b. (a -> b) -> a -> b
$ Macho
macho
    else
      Maybe Binary -> IO (Maybe Binary)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Binary
forall a. Maybe a
Nothing



-- | A control flow graph with blocks and edges.
-- A blockID (represented as an @Int@) is a unique identifier of a basic block.
-- We store basic blocks twice: once as addresses, and once as instructions.
data CFG = CFG {
  CFG -> IntMap [Int]
cfg_blocks :: IM.IntMap [Int],            -- ^ A mapping of blockIDs to instruction addresses
  CFG -> IntMap IntSet
cfg_edges  :: IM.IntMap (IS.IntSet),      -- ^ A mapping of blockIDs to sets of blocKIDs
  CFG -> IntMap Int
cfg_addr_to_blockID :: IM.IntMap Int,     -- ^ A mapping of instruction addresses to blockIDs
  CFG -> Int
cfg_fresh :: Int,                         -- ^ A fresh blockID
  CFG -> IntMap [Instruction]
cfg_instrs :: IM.IntMap [X86.Instruction] -- ^ A mapping of blockIDs to lists of disassembled instructions.
 }
 deriving (Int -> CFG -> String -> String
[CFG] -> String -> String
CFG -> String
(Int -> CFG -> String -> String)
-> (CFG -> String) -> ([CFG] -> String -> String) -> Show CFG
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CFG] -> String -> String
$cshowList :: [CFG] -> String -> String
show :: CFG -> String
$cshow :: CFG -> String
showsPrec :: Int -> CFG -> String -> String
$cshowsPrec :: Int -> CFG -> String -> String
Show,(forall x. CFG -> Rep CFG x)
-> (forall x. Rep CFG x -> CFG) -> Generic CFG
forall x. Rep CFG x -> CFG
forall x. CFG -> Rep CFG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CFG x -> CFG
$cfrom :: forall x. CFG -> Rep CFG x
Generic,CFG -> CFG -> Bool
(CFG -> CFG -> Bool) -> (CFG -> CFG -> Bool) -> Eq CFG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CFG -> CFG -> Bool
$c/= :: CFG -> CFG -> Bool
== :: CFG -> CFG -> Bool
$c== :: CFG -> CFG -> Bool
Eq)


-- | A jump table with :
--   index: an operand containing a bounded index at the beginning of execution of the block
--   bound: the bound on idx
--   trgt: the operand containg the jump target at the end of execution of the block
--   tbl: a table from values of idx to resulting jump targets
data JumpTable = JumpTable {
  JumpTable -> Operand
jtbl_index  :: X86.Operand,
  JumpTable -> Int
jtbl_bound  :: Int,
  JumpTable -> Operand
jtbl_target :: X86.Operand,
  JumpTable -> IntMap Word64
jtbl_table  :: IM.IntMap Word64 
 }
 deriving ((forall x. JumpTable -> Rep JumpTable x)
-> (forall x. Rep JumpTable x -> JumpTable) -> Generic JumpTable
forall x. Rep JumpTable x -> JumpTable
forall x. JumpTable -> Rep JumpTable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep JumpTable x -> JumpTable
$cfrom :: forall x. JumpTable -> Rep JumpTable x
Generic, JumpTable -> JumpTable -> Bool
(JumpTable -> JumpTable -> Bool)
-> (JumpTable -> JumpTable -> Bool) -> Eq JumpTable
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: JumpTable -> JumpTable -> Bool
$c/= :: JumpTable -> JumpTable -> Bool
== :: JumpTable -> JumpTable -> Bool
$c== :: JumpTable -> JumpTable -> Bool
Eq)

-- | An indirection is either a jump table or a set of resolved jump targets
data Indirection = Indirection_JumpTable JumpTable | Indirection_Resolved (S.Set ResolvedJumpTarget) | Indirection_Unresolved
 deriving ((forall x. Indirection -> Rep Indirection x)
-> (forall x. Rep Indirection x -> Indirection)
-> Generic Indirection
forall x. Rep Indirection x -> Indirection
forall x. Indirection -> Rep Indirection x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Indirection x -> Indirection
$cfrom :: forall x. Indirection -> Rep Indirection x
Generic, Indirection -> Indirection -> Bool
(Indirection -> Indirection -> Bool)
-> (Indirection -> Indirection -> Bool) -> Eq Indirection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Indirection -> Indirection -> Bool
$c/= :: Indirection -> Indirection -> Bool
== :: Indirection -> Indirection -> Bool
$c== :: Indirection -> Indirection -> Bool
Eq)

-- | Per instruction address, a set of possibly resolved jump targets
type Indirections = IM.IntMap Indirection




-- | An enumeration indicating the result of verification over a function
data VerificationResult =
     VerificationSuccess              -- ^ Function was succesfully verified
  | VerificationSuccesWithAssumptions -- ^ Function was succesfully verified, but required assertions
  | VerificationUnresolvedIndirection -- ^ Function contains an unresolved indirection
  | VerificationError String          -- ^ There was some verification error, e.g., return adresss overwrite
  | Unverified                        -- ^ The function has not been verified.
  deriving (VerificationResult -> VerificationResult -> Bool
(VerificationResult -> VerificationResult -> Bool)
-> (VerificationResult -> VerificationResult -> Bool)
-> Eq VerificationResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VerificationResult -> VerificationResult -> Bool
$c/= :: VerificationResult -> VerificationResult -> Bool
== :: VerificationResult -> VerificationResult -> Bool
$c== :: VerificationResult -> VerificationResult -> Bool
Eq, (forall x. VerificationResult -> Rep VerificationResult x)
-> (forall x. Rep VerificationResult x -> VerificationResult)
-> Generic VerificationResult
forall x. Rep VerificationResult x -> VerificationResult
forall x. VerificationResult -> Rep VerificationResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep VerificationResult x -> VerificationResult
$cfrom :: forall x. VerificationResult -> Rep VerificationResult x
Generic)


-- | Predicates: symbolic states
type Predicate = Sstate SValue SPointer


-- | Invariants: a mapping of blockIDs to predicates
type Invariants = IM.IntMap Predicate


-- | For each leaf-node in a CFG we store the following info. (TODO MOVE?)
data NodeInfo =
    Normal                -- ^ The basic block behaves normally, e.g., a ret
  | UnresolvedIndirection -- ^ The basic block ends in an unresolved indirection
  | Terminal              -- ^ The basic blocks ends with, e.g., a call to exit()
 deriving (Int -> NodeInfo -> String -> String
[NodeInfo] -> String -> String
NodeInfo -> String
(Int -> NodeInfo -> String -> String)
-> (NodeInfo -> String)
-> ([NodeInfo] -> String -> String)
-> Show NodeInfo
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [NodeInfo] -> String -> String
$cshowList :: [NodeInfo] -> String -> String
show :: NodeInfo -> String
$cshow :: NodeInfo -> String
showsPrec :: Int -> NodeInfo -> String -> String
$cshowsPrec :: Int -> NodeInfo -> String -> String
Show,(forall x. NodeInfo -> Rep NodeInfo x)
-> (forall x. Rep NodeInfo x -> NodeInfo) -> Generic NodeInfo
forall x. Rep NodeInfo x -> NodeInfo
forall x. NodeInfo -> Rep NodeInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NodeInfo x -> NodeInfo
$cfrom :: forall x. NodeInfo -> Rep NodeInfo x
Generic,NodeInfo -> NodeInfo -> Bool
(NodeInfo -> NodeInfo -> Bool)
-> (NodeInfo -> NodeInfo -> Bool) -> Eq NodeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeInfo -> NodeInfo -> Bool
$c/= :: NodeInfo -> NodeInfo -> Bool
== :: NodeInfo -> NodeInfo -> Bool
$c== :: NodeInfo -> NodeInfo -> Bool
Eq,Eq NodeInfo
Eq NodeInfo
-> (NodeInfo -> NodeInfo -> Ordering)
-> (NodeInfo -> NodeInfo -> Bool)
-> (NodeInfo -> NodeInfo -> Bool)
-> (NodeInfo -> NodeInfo -> Bool)
-> (NodeInfo -> NodeInfo -> Bool)
-> (NodeInfo -> NodeInfo -> NodeInfo)
-> (NodeInfo -> NodeInfo -> NodeInfo)
-> Ord NodeInfo
NodeInfo -> NodeInfo -> Bool
NodeInfo -> NodeInfo -> Ordering
NodeInfo -> NodeInfo -> NodeInfo
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 :: NodeInfo -> NodeInfo -> NodeInfo
$cmin :: NodeInfo -> NodeInfo -> NodeInfo
max :: NodeInfo -> NodeInfo -> NodeInfo
$cmax :: NodeInfo -> NodeInfo -> NodeInfo
>= :: NodeInfo -> NodeInfo -> Bool
$c>= :: NodeInfo -> NodeInfo -> Bool
> :: NodeInfo -> NodeInfo -> Bool
$c> :: NodeInfo -> NodeInfo -> Bool
<= :: NodeInfo -> NodeInfo -> Bool
$c<= :: NodeInfo -> NodeInfo -> Bool
< :: NodeInfo -> NodeInfo -> Bool
$c< :: NodeInfo -> NodeInfo -> Bool
compare :: NodeInfo -> NodeInfo -> Ordering
$ccompare :: NodeInfo -> NodeInfo -> Ordering
$cp1Ord :: Eq NodeInfo
Ord)

-- | Postconditions: for each final block the @NodeInfo@ and the final predicate after execution of the block
type Postconditions = S.Set (NodeInfo,Predicate)





-- | An abstract domain for pointers
data PointerDomain =
    Domain_Bases    (NES.NESet PointerBase)  -- a non-empty set of bases
  | Domain_Sources  (NES.NESet BotSrc)       -- a possibly empty set of sources
  deriving ((forall x. PointerDomain -> Rep PointerDomain x)
-> (forall x. Rep PointerDomain x -> PointerDomain)
-> Generic PointerDomain
forall x. Rep PointerDomain x -> PointerDomain
forall x. PointerDomain -> Rep PointerDomain x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PointerDomain x -> PointerDomain
$cfrom :: forall x. PointerDomain -> Rep PointerDomain x
Generic,PointerDomain -> PointerDomain -> Bool
(PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool) -> Eq PointerDomain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PointerDomain -> PointerDomain -> Bool
$c/= :: PointerDomain -> PointerDomain -> Bool
== :: PointerDomain -> PointerDomain -> Bool
$c== :: PointerDomain -> PointerDomain -> Bool
Eq,Eq PointerDomain
Eq PointerDomain
-> (PointerDomain -> PointerDomain -> Ordering)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> Bool)
-> (PointerDomain -> PointerDomain -> PointerDomain)
-> (PointerDomain -> PointerDomain -> PointerDomain)
-> Ord PointerDomain
PointerDomain -> PointerDomain -> Bool
PointerDomain -> PointerDomain -> Ordering
PointerDomain -> PointerDomain -> PointerDomain
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 :: PointerDomain -> PointerDomain -> PointerDomain
$cmin :: PointerDomain -> PointerDomain -> PointerDomain
max :: PointerDomain -> PointerDomain -> PointerDomain
$cmax :: PointerDomain -> PointerDomain -> PointerDomain
>= :: PointerDomain -> PointerDomain -> Bool
$c>= :: PointerDomain -> PointerDomain -> Bool
> :: PointerDomain -> PointerDomain -> Bool
$c> :: PointerDomain -> PointerDomain -> Bool
<= :: PointerDomain -> PointerDomain -> Bool
$c<= :: PointerDomain -> PointerDomain -> Bool
< :: PointerDomain -> PointerDomain -> Bool
$c< :: PointerDomain -> PointerDomain -> Bool
compare :: PointerDomain -> PointerDomain -> Ordering
$ccompare :: PointerDomain -> PointerDomain -> Ordering
$cp1Ord :: Eq PointerDomain
Ord)



-- | A function initialisation consists of a mapping of registers to symbolic pointers TODO
data MemRelation = Separate | Aliassing | Unknown
  deriving ((forall x. MemRelation -> Rep MemRelation x)
-> (forall x. Rep MemRelation x -> MemRelation)
-> Generic MemRelation
forall x. Rep MemRelation x -> MemRelation
forall x. MemRelation -> Rep MemRelation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MemRelation x -> MemRelation
$cfrom :: forall x. MemRelation -> Rep MemRelation x
Generic,MemRelation -> MemRelation -> Bool
(MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool) -> Eq MemRelation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MemRelation -> MemRelation -> Bool
$c/= :: MemRelation -> MemRelation -> Bool
== :: MemRelation -> MemRelation -> Bool
$c== :: MemRelation -> MemRelation -> Bool
Eq,Eq MemRelation
Eq MemRelation
-> (MemRelation -> MemRelation -> Ordering)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> Bool)
-> (MemRelation -> MemRelation -> MemRelation)
-> (MemRelation -> MemRelation -> MemRelation)
-> Ord MemRelation
MemRelation -> MemRelation -> Bool
MemRelation -> MemRelation -> Ordering
MemRelation -> MemRelation -> MemRelation
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 :: MemRelation -> MemRelation -> MemRelation
$cmin :: MemRelation -> MemRelation -> MemRelation
max :: MemRelation -> MemRelation -> MemRelation
$cmax :: MemRelation -> MemRelation -> MemRelation
>= :: MemRelation -> MemRelation -> Bool
$c>= :: MemRelation -> MemRelation -> Bool
> :: MemRelation -> MemRelation -> Bool
$c> :: MemRelation -> MemRelation -> Bool
<= :: MemRelation -> MemRelation -> Bool
$c<= :: MemRelation -> MemRelation -> Bool
< :: MemRelation -> MemRelation -> Bool
$c< :: MemRelation -> MemRelation -> Bool
compare :: MemRelation -> MemRelation -> Ordering
$ccompare :: MemRelation -> MemRelation -> Ordering
$cp1Ord :: Eq MemRelation
Ord,Int -> MemRelation -> String -> String
[MemRelation] -> String -> String
MemRelation -> String
(Int -> MemRelation -> String -> String)
-> (MemRelation -> String)
-> ([MemRelation] -> String -> String)
-> Show MemRelation
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [MemRelation] -> String -> String
$cshowList :: [MemRelation] -> String -> String
show :: MemRelation -> String
$cshow :: MemRelation -> String
showsPrec :: Int -> MemRelation -> String -> String
$cshowsPrec :: Int -> MemRelation -> String -> String
Show)
data FInit = FInit (S.Set (StatePart,Maybe SValue)) (M.Map (SStatePart,SStatePart) MemRelation)
  deriving ((forall x. FInit -> Rep FInit x)
-> (forall x. Rep FInit x -> FInit) -> Generic FInit
forall x. Rep FInit x -> FInit
forall x. FInit -> Rep FInit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FInit x -> FInit
$cfrom :: forall x. FInit -> Rep FInit x
Generic,FInit -> FInit -> Bool
(FInit -> FInit -> Bool) -> (FInit -> FInit -> Bool) -> Eq FInit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FInit -> FInit -> Bool
$c/= :: FInit -> FInit -> Bool
== :: FInit -> FInit -> Bool
$c== :: FInit -> FInit -> Bool
Eq,Eq FInit
Eq FInit
-> (FInit -> FInit -> Ordering)
-> (FInit -> FInit -> Bool)
-> (FInit -> FInit -> Bool)
-> (FInit -> FInit -> Bool)
-> (FInit -> FInit -> Bool)
-> (FInit -> FInit -> FInit)
-> (FInit -> FInit -> FInit)
-> Ord FInit
FInit -> FInit -> Bool
FInit -> FInit -> Ordering
FInit -> FInit -> FInit
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 :: FInit -> FInit -> FInit
$cmin :: FInit -> FInit -> FInit
max :: FInit -> FInit -> FInit
$cmax :: FInit -> FInit -> FInit
>= :: FInit -> FInit -> Bool
$c>= :: FInit -> FInit -> Bool
> :: FInit -> FInit -> Bool
$c> :: FInit -> FInit -> Bool
<= :: FInit -> FInit -> Bool
$c<= :: FInit -> FInit -> Bool
< :: FInit -> FInit -> Bool
$c< :: FInit -> FInit -> Bool
compare :: FInit -> FInit -> Ordering
$ccompare :: FInit -> FInit -> Ordering
$cp1Ord :: Eq FInit
Ord)

-- | A function call 
data FReturnBehavior =
    Terminating              -- ^ The function does never return
  | ReturningWith Predicate  -- ^ The function returns withg the symbolic changes stored in the predicate
  | UnknownRetBehavior       -- ^  It is unknown whether the function returns or not
 deriving (Int -> FReturnBehavior -> String -> String
[FReturnBehavior] -> String -> String
FReturnBehavior -> String
(Int -> FReturnBehavior -> String -> String)
-> (FReturnBehavior -> String)
-> ([FReturnBehavior] -> String -> String)
-> Show FReturnBehavior
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FReturnBehavior] -> String -> String
$cshowList :: [FReturnBehavior] -> String -> String
show :: FReturnBehavior -> String
$cshow :: FReturnBehavior -> String
showsPrec :: Int -> FReturnBehavior -> String -> String
$cshowsPrec :: Int -> FReturnBehavior -> String -> String
Show,(forall x. FReturnBehavior -> Rep FReturnBehavior x)
-> (forall x. Rep FReturnBehavior x -> FReturnBehavior)
-> Generic FReturnBehavior
forall x. Rep FReturnBehavior x -> FReturnBehavior
forall x. FReturnBehavior -> Rep FReturnBehavior x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FReturnBehavior x -> FReturnBehavior
$cfrom :: forall x. FReturnBehavior -> Rep FReturnBehavior x
Generic,FReturnBehavior -> FReturnBehavior -> Bool
(FReturnBehavior -> FReturnBehavior -> Bool)
-> (FReturnBehavior -> FReturnBehavior -> Bool)
-> Eq FReturnBehavior
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FReturnBehavior -> FReturnBehavior -> Bool
$c/= :: FReturnBehavior -> FReturnBehavior -> Bool
== :: FReturnBehavior -> FReturnBehavior -> Bool
$c== :: FReturnBehavior -> FReturnBehavior -> Bool
Eq,Eq FReturnBehavior
Eq FReturnBehavior
-> (FReturnBehavior -> FReturnBehavior -> Ordering)
-> (FReturnBehavior -> FReturnBehavior -> Bool)
-> (FReturnBehavior -> FReturnBehavior -> Bool)
-> (FReturnBehavior -> FReturnBehavior -> Bool)
-> (FReturnBehavior -> FReturnBehavior -> Bool)
-> (FReturnBehavior -> FReturnBehavior -> FReturnBehavior)
-> (FReturnBehavior -> FReturnBehavior -> FReturnBehavior)
-> Ord FReturnBehavior
FReturnBehavior -> FReturnBehavior -> Bool
FReturnBehavior -> FReturnBehavior -> Ordering
FReturnBehavior -> FReturnBehavior -> FReturnBehavior
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 :: FReturnBehavior -> FReturnBehavior -> FReturnBehavior
$cmin :: FReturnBehavior -> FReturnBehavior -> FReturnBehavior
max :: FReturnBehavior -> FReturnBehavior -> FReturnBehavior
$cmax :: FReturnBehavior -> FReturnBehavior -> FReturnBehavior
>= :: FReturnBehavior -> FReturnBehavior -> Bool
$c>= :: FReturnBehavior -> FReturnBehavior -> Bool
> :: FReturnBehavior -> FReturnBehavior -> Bool
$c> :: FReturnBehavior -> FReturnBehavior -> Bool
<= :: FReturnBehavior -> FReturnBehavior -> Bool
$c<= :: FReturnBehavior -> FReturnBehavior -> Bool
< :: FReturnBehavior -> FReturnBehavior -> Bool
$c< :: FReturnBehavior -> FReturnBehavior -> Bool
compare :: FReturnBehavior -> FReturnBehavior -> Ordering
$ccompare :: FReturnBehavior -> FReturnBehavior -> Ordering
$cp1Ord :: Eq FReturnBehavior
Ord)


-- | A symbolic state part
data SStatePart =
    SSP_Reg Register -- ^ A register
  | SSP_Mem SPointer Int
 deriving (Int -> SStatePart -> String -> String
[SStatePart] -> String -> String
SStatePart -> String
(Int -> SStatePart -> String -> String)
-> (SStatePart -> String)
-> ([SStatePart] -> String -> String)
-> Show SStatePart
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SStatePart] -> String -> String
$cshowList :: [SStatePart] -> String -> String
show :: SStatePart -> String
$cshow :: SStatePart -> String
showsPrec :: Int -> SStatePart -> String -> String
$cshowsPrec :: Int -> SStatePart -> String -> String
Show,(forall x. SStatePart -> Rep SStatePart x)
-> (forall x. Rep SStatePart x -> SStatePart) -> Generic SStatePart
forall x. Rep SStatePart x -> SStatePart
forall x. SStatePart -> Rep SStatePart x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SStatePart x -> SStatePart
$cfrom :: forall x. SStatePart -> Rep SStatePart x
Generic,SStatePart -> SStatePart -> Bool
(SStatePart -> SStatePart -> Bool)
-> (SStatePart -> SStatePart -> Bool) -> Eq SStatePart
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SStatePart -> SStatePart -> Bool
$c/= :: SStatePart -> SStatePart -> Bool
== :: SStatePart -> SStatePart -> Bool
$c== :: SStatePart -> SStatePart -> Bool
Eq,Eq SStatePart
Eq SStatePart
-> (SStatePart -> SStatePart -> Ordering)
-> (SStatePart -> SStatePart -> Bool)
-> (SStatePart -> SStatePart -> Bool)
-> (SStatePart -> SStatePart -> Bool)
-> (SStatePart -> SStatePart -> Bool)
-> (SStatePart -> SStatePart -> SStatePart)
-> (SStatePart -> SStatePart -> SStatePart)
-> Ord SStatePart
SStatePart -> SStatePart -> Bool
SStatePart -> SStatePart -> Ordering
SStatePart -> SStatePart -> SStatePart
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 :: SStatePart -> SStatePart -> SStatePart
$cmin :: SStatePart -> SStatePart -> SStatePart
max :: SStatePart -> SStatePart -> SStatePart
$cmax :: SStatePart -> SStatePart -> SStatePart
>= :: SStatePart -> SStatePart -> Bool
$c>= :: SStatePart -> SStatePart -> Bool
> :: SStatePart -> SStatePart -> Bool
$c> :: SStatePart -> SStatePart -> Bool
<= :: SStatePart -> SStatePart -> Bool
$c<= :: SStatePart -> SStatePart -> Bool
< :: SStatePart -> SStatePart -> Bool
$c< :: SStatePart -> SStatePart -> Bool
compare :: SStatePart -> SStatePart -> Ordering
$ccompare :: SStatePart -> SStatePart -> Ordering
$cp1Ord :: Eq SStatePart
Ord)



-----------------------------------------------------------------------------
-- |
-- The context datastructure.
--
-- __S__: Information __S__tatically obtained by reading from the binary
--
-- __D__: Information __D__ynamically updated during verification
-------------------------------------------------------------------------------
data Context_ = Context_ {
   Context_ -> Config
ctxt__config        :: !Config,                         -- ^ __S__: the configuration file in ./config
   Context_ -> Bool
ctxt__verbose       :: !Bool,                           -- ^ __S__: is verbose output requested?
   Context_ -> SymbolTable
ctxt__syms          :: !SymbolTable,                    -- ^ __S__: the symbol table: a mapping of addresses to function names for external functions
   Context_ -> SectionsInfo
ctxt__sections      :: !SectionsInfo,                   -- ^ __S__: information on segments/section
   Context_ -> Set Relocation
ctxt__relocs        :: !(S.Set Relocation),             -- ^ __S__: relocation entries
   Context_ -> String
ctxt__dirname       :: !String,                         -- ^ __S__: the name of the directory where the .dump, .entry, .sections and .symbols files reside
   Context_ -> String
ctxt__name          :: !String,                         -- ^ __S__: the name of the binary
   Context_ -> Int
ctxt__start         :: !Int,                            -- ^ __S__: the address of the _start symbol

   Context_ -> Graph
ctxt__entries       :: !Graph,                          -- ^ __D__: a graph with an edge (e0,e1) if entry address e0 calls entry address e1, and e0 and e1 have not been verified yet
   Context_ -> IntMap CFG
ctxt__cfgs          :: !(IM.IntMap CFG),                -- ^ __D__: the currently known control flow graphs per function entry
   Context_ -> IntMap FReturnBehavior
ctxt__calls         :: !(IM.IntMap FReturnBehavior),    -- ^ __D__: the currently known and verified entry addresses of functions mapped to return-information
   Context_ -> IntMap Invariants
ctxt__invs          :: !(IM.IntMap Invariants),         -- ^ __D__: the currently known invariants
   Context_ -> IntMap Postconditions
ctxt__posts         :: !(IM.IntMap Postconditions),     -- ^ __D__: the currently known postconditions
   Context_ -> IntMap (Set SStatePart)
ctxt__stateparts    :: !(IM.IntMap (S.Set SStatePart)), -- ^ __D__: the state parts read from/written to be the function
   Context_ -> Indirections
ctxt__inds          :: !Indirections,                   -- ^ __D__: the currently known indirections
   Context_ -> IntMap FInit
ctxt__finits        :: !(IM.IntMap FInit),              -- ^ __D__: the currently known function initialisations
   Context_ -> IntMap VCS
ctxt__vcs           :: !(IM.IntMap VCS),                -- ^ __D__: the verification conditions
   Context_ -> IntMap VerificationResult
ctxt__results       :: !(IM.IntMap VerificationResult), -- ^ __D__: the verification result
   Context_ -> IntMap IntSet
ctxt__recursions    :: !(IM.IntMap IS.IntSet),          -- ^ __D__: a mapping from function entries to the set of mutually recursive functions entries they occur in
   Context_ -> Int64
ctxt__runningtime   :: !Int64                           -- ^ __D__: running time of lifting effort
 }
 deriving (forall x. Context_ -> Rep Context_ x)
-> (forall x. Rep Context_ x -> Context_) -> Generic Context_
forall x. Rep Context_ x -> Context_
forall x. Context_ -> Rep Context_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Context_ x -> Context_
$cfrom :: forall x. Context_ -> Rep Context_ x
Generic

data Context = Context {
  Context -> Binary
ctxt_binary :: !Binary,
  Context -> IORef (IntMap Instruction)
ctxt_ioref  :: IORef (IM.IntMap X86.Instruction),
  Context -> Context_
ctxt_ctxt_  :: !Context_
 }


ctxt_config :: Context -> Config
ctxt_config      = Context_ -> Config
ctxt__config      (Context_ -> Config) -> (Context -> Context_) -> Context -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_verbose :: Context -> Bool
ctxt_verbose     = Context_ -> Bool
ctxt__verbose     (Context_ -> Bool) -> (Context -> Context_) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_syms :: Context -> SymbolTable
ctxt_syms        = Context_ -> SymbolTable
ctxt__syms        (Context_ -> SymbolTable)
-> (Context -> Context_) -> Context -> SymbolTable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_sections :: Context -> SectionsInfo
ctxt_sections    = Context_ -> SectionsInfo
ctxt__sections    (Context_ -> SectionsInfo)
-> (Context -> Context_) -> Context -> SectionsInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_relocs :: Context -> Set Relocation
ctxt_relocs      = Context_ -> Set Relocation
ctxt__relocs      (Context_ -> Set Relocation)
-> (Context -> Context_) -> Context -> Set Relocation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_dirname :: Context -> String
ctxt_dirname     = Context_ -> String
ctxt__dirname     (Context_ -> String) -> (Context -> Context_) -> Context -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_name :: Context -> String
ctxt_name        = Context_ -> String
ctxt__name        (Context_ -> String) -> (Context -> Context_) -> Context -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_start :: Context -> Int
ctxt_start       = Context_ -> Int
ctxt__start       (Context_ -> Int) -> (Context -> Context_) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_entries :: Context -> Graph
ctxt_entries     = Context_ -> Graph
ctxt__entries     (Context_ -> Graph) -> (Context -> Context_) -> Context -> Graph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_cfgs :: Context -> IntMap CFG
ctxt_cfgs        = Context_ -> IntMap CFG
ctxt__cfgs        (Context_ -> IntMap CFG)
-> (Context -> Context_) -> Context -> IntMap CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_calls :: Context -> IntMap FReturnBehavior
ctxt_calls       = Context_ -> IntMap FReturnBehavior
ctxt__calls       (Context_ -> IntMap FReturnBehavior)
-> (Context -> Context_) -> Context -> IntMap FReturnBehavior
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_invs :: Context -> IntMap Invariants
ctxt_invs        = Context_ -> IntMap Invariants
ctxt__invs        (Context_ -> IntMap Invariants)
-> (Context -> Context_) -> Context -> IntMap Invariants
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_posts :: Context -> IntMap Postconditions
ctxt_posts       = Context_ -> IntMap Postconditions
ctxt__posts       (Context_ -> IntMap Postconditions)
-> (Context -> Context_) -> Context -> IntMap Postconditions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_stateparts :: Context -> IntMap (Set SStatePart)
ctxt_stateparts  = Context_ -> IntMap (Set SStatePart)
ctxt__stateparts  (Context_ -> IntMap (Set SStatePart))
-> (Context -> Context_) -> Context -> IntMap (Set SStatePart)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_inds :: Context -> Indirections
ctxt_inds        = Context_ -> Indirections
ctxt__inds        (Context_ -> Indirections)
-> (Context -> Context_) -> Context -> Indirections
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_finits :: Context -> IntMap FInit
ctxt_finits      = Context_ -> IntMap FInit
ctxt__finits      (Context_ -> IntMap FInit)
-> (Context -> Context_) -> Context -> IntMap FInit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_vcs :: Context -> IntMap VCS
ctxt_vcs         = Context_ -> IntMap VCS
ctxt__vcs         (Context_ -> IntMap VCS)
-> (Context -> Context_) -> Context -> IntMap VCS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_results :: Context -> IntMap VerificationResult
ctxt_results     = Context_ -> IntMap VerificationResult
ctxt__results     (Context_ -> IntMap VerificationResult)
-> (Context -> Context_) -> Context -> IntMap VerificationResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_recursions :: Context -> IntMap IntSet
ctxt_recursions  = Context_ -> IntMap IntSet
ctxt__recursions  (Context_ -> IntMap IntSet)
-> (Context -> Context_) -> Context -> IntMap IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_
ctxt_runningtime :: Context -> Int64
ctxt_runningtime = Context_ -> Int64
ctxt__runningtime (Context_ -> Int64) -> (Context -> Context_) -> Context -> Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context_
ctxt_ctxt_

set_ctxt_syms :: SymbolTable -> Context -> Context
set_ctxt_syms       SymbolTable
syms     (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__syms :: SymbolTable
ctxt__syms = SymbolTable
syms})
set_ctxt_sections :: SectionsInfo -> Context -> Context
set_ctxt_sections   SectionsInfo
sections (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__sections :: SectionsInfo
ctxt__sections = SectionsInfo
sections})
set_ctxt_relocs :: Set Relocation -> Context -> Context
set_ctxt_relocs     Set Relocation
relocs   (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__relocs :: Set Relocation
ctxt__relocs = Set Relocation
relocs})
set_ctxt_start :: Int -> Context -> Context
set_ctxt_start      Int
start    (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__start :: Int
ctxt__start = Int
start})
set_ctxt_entries :: Graph -> Context -> Context
set_ctxt_entries    Graph
entries  (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__entries :: Graph
ctxt__entries = Graph
entries})
set_ctxt_calls :: IntMap FReturnBehavior -> Context -> Context
set_ctxt_calls      IntMap FReturnBehavior
calls    (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__calls :: IntMap FReturnBehavior
ctxt__calls = IntMap FReturnBehavior
calls})
set_ctxt_inds :: Indirections -> Context -> Context
set_ctxt_inds       Indirections
inds     (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__inds :: Indirections
ctxt__inds = Indirections
inds})
set_ctxt_posts :: IntMap Postconditions -> Context -> Context
set_ctxt_posts      IntMap Postconditions
posts    (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__posts :: IntMap Postconditions
ctxt__posts = IntMap Postconditions
posts})
set_ctxt_stateparts :: IntMap (Set SStatePart) -> Context -> Context
set_ctxt_stateparts IntMap (Set SStatePart)
sps      (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__stateparts :: IntMap (Set SStatePart)
ctxt__stateparts = IntMap (Set SStatePart)
sps})
set_ctxt_vcs :: IntMap VCS -> Context -> Context
set_ctxt_vcs        IntMap VCS
vcs      (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__vcs :: IntMap VCS
ctxt__vcs = IntMap VCS
vcs})
set_ctxt_finits :: IntMap FInit -> Context -> Context
set_ctxt_finits     IntMap FInit
finits   (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__finits :: IntMap FInit
ctxt__finits = IntMap FInit
finits})
set_ctxt_invs :: IntMap Invariants -> Context -> Context
set_ctxt_invs       IntMap Invariants
invs     (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__invs :: IntMap Invariants
ctxt__invs = IntMap Invariants
invs})
set_ctxt_cfgs :: IntMap CFG -> Context -> Context
set_ctxt_cfgs       IntMap CFG
cfgs     (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__cfgs :: IntMap CFG
ctxt__cfgs = IntMap CFG
cfgs})
set_ctxt_results :: IntMap VerificationResult -> Context -> Context
set_ctxt_results    IntMap VerificationResult
results  (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__results :: IntMap VerificationResult
ctxt__results = IntMap VerificationResult
results})
set_ctxt_recursions :: IntMap IntSet -> Context -> Context
set_ctxt_recursions IntMap IntSet
recs     (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__recursions :: IntMap IntSet
ctxt__recursions = IntMap IntSet
recs})
set_ctxt_runningtime :: Int64 -> Context -> Context
set_ctxt_runningtime Int64
time    (Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_) = Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref (Context_
ctxt_ {ctxt__runningtime :: Int64
ctxt__runningtime = Int64
time})

instance Cereal.Serialize VerificationResult
instance Cereal.Serialize ResolvedJumpTarget
instance Cereal.Serialize JumpTable
instance Cereal.Serialize Symbol
instance Cereal.Serialize SymbolTable
instance Cereal.Serialize Indirection
instance Cereal.Serialize Relocation
instance Cereal.Serialize MemRelation 
instance Cereal.Serialize FInit
instance Cereal.Serialize CFG
instance Cereal.Serialize FReturnBehavior
instance Cereal.Serialize VerificationCondition
instance Cereal.Serialize PointerDomain
instance Cereal.Serialize SectionsInfo
instance Cereal.Serialize SStatePart
instance Cereal.Serialize NodeInfo
instance Cereal.Serialize Context_


instance NFData VerificationResult
instance NFData ResolvedJumpTarget
instance NFData JumpTable
instance NFData Symbol
instance NFData SymbolTable
instance NFData Indirection
instance NFData Relocation
instance NFData MemRelation 
instance NFData FInit
instance NFData CFG
instance NFData FReturnBehavior
instance NFData VerificationCondition
instance NFData PointerDomain
instance NFData SectionsInfo
instance NFData SStatePart
instance NFData NodeInfo
instance NFData Context_

-- | intialize an empty context based on the command-line parameters
init_finit :: FInit
init_finit = Set (StatePart, Maybe SValue)
-> Map (SStatePart, SStatePart) MemRelation -> FInit
FInit Set (StatePart, Maybe SValue)
forall a. Set a
S.empty Map (SStatePart, SStatePart) MemRelation
forall k a. Map k a
M.empty
init_context :: Binary
-> IORef (IntMap Instruction)
-> Config
-> Bool
-> String
-> String
-> Context
init_context Binary
binary IORef (IntMap Instruction)
ioref Config
config Bool
verbose String
dirname String
name =
  let !sections :: SectionsInfo
sections = Binary -> SectionsInfo
forall a. BinaryClass a => a -> SectionsInfo
binary_get_sections_info Binary
binary
      !symbols :: SymbolTable
symbols  = Binary -> SymbolTable
forall a. BinaryClass a => a -> SymbolTable
binary_get_symbols Binary
binary
      !relocs :: Set Relocation
relocs   = Binary -> Set Relocation
forall a. BinaryClass a => a -> Set Relocation
binary_get_relocations Binary
binary in
  Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
binary IORef (IntMap Instruction)
ioref (Context_ -> Context) -> Context_ -> Context
forall a b. (a -> b) -> a -> b
$ Config
-> Bool
-> SymbolTable
-> SectionsInfo
-> Set Relocation
-> String
-> String
-> Int
-> Graph
-> IntMap CFG
-> IntMap FReturnBehavior
-> IntMap Invariants
-> IntMap Postconditions
-> IntMap (Set SStatePart)
-> Indirections
-> IntMap FInit
-> IntMap VCS
-> IntMap VerificationResult
-> IntMap IntSet
-> Int64
-> Context_
Context_ Config
config Bool
verbose SymbolTable
symbols SectionsInfo
sections Set Relocation
relocs String
dirname String
name Int
0 (IntMap IntSet -> Graph
Edges IntMap IntSet
forall a. IntMap a
IM.empty) IntMap CFG
forall a. IntMap a
IM.empty IntMap FReturnBehavior
forall a. IntMap a
IM.empty IntMap Invariants
forall a. IntMap a
IM.empty IntMap Postconditions
forall a. IntMap a
IM.empty IntMap (Set SStatePart)
forall a. IntMap a
IM.empty Indirections
forall a. IntMap a
IM.empty IntMap FInit
forall a. IntMap a
IM.empty IntMap VCS
forall a. IntMap a
IM.empty IntMap VerificationResult
forall a. IntMap a
IM.empty IntMap IntSet
forall a. IntMap a
IM.empty Int64
0


-- | purge the context before exporting it (may save a lot of disk space)
purge_context  :: Context -> Context_
purge_context :: Context -> Context_
purge_context (Context Binary
binary IORef (IntMap Instruction)
_ (Context_ Config
config Bool
verbose SymbolTable
syms SectionsInfo
sections Set Relocation
relocs String
dirname String
name Int
start Graph
entries IntMap CFG
cfgs IntMap FReturnBehavior
calls IntMap Invariants
invs IntMap Postconditions
posts IntMap (Set SStatePart)
stateparts Indirections
inds IntMap FInit
finits IntMap VCS
vcs IntMap VerificationResult
results IntMap IntSet
recursions Int64
runningTime)) =
  let keep_preconditions :: Bool
keep_preconditions = Config -> Bool
store_preconditions_in_L0 Config
config
      keep_assertions :: Bool
keep_assertions    = Config -> Bool
store_assertions_in_L0 Config
config
      vcs' :: IntMap VCS
vcs'               = (VCS -> Bool) -> IntMap VCS -> IntMap VCS
forall a. (a -> Bool) -> IntMap a -> IntMap a
IM.filter (Bool -> Bool
not (Bool -> Bool) -> (VCS -> Bool) -> VCS -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VCS -> Bool
forall a. Set a -> Bool
S.null) (IntMap VCS -> IntMap VCS) -> IntMap VCS -> IntMap VCS
forall a b. (a -> b) -> a -> b
$ (VCS -> VCS) -> IntMap VCS -> IntMap VCS
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (Bool -> Bool -> VCS -> VCS
purge Bool
keep_preconditions Bool
keep_assertions) IntMap VCS
vcs in
    Config
-> Bool
-> SymbolTable
-> SectionsInfo
-> Set Relocation
-> String
-> String
-> Int
-> Graph
-> IntMap CFG
-> IntMap FReturnBehavior
-> IntMap Invariants
-> IntMap Postconditions
-> IntMap (Set SStatePart)
-> Indirections
-> IntMap FInit
-> IntMap VCS
-> IntMap VerificationResult
-> IntMap IntSet
-> Int64
-> Context_
Context_ Config
config Bool
verbose SymbolTable
syms SectionsInfo
sections Set Relocation
relocs String
dirname String
name Int
start (IntMap IntSet -> Graph
Edges IntMap IntSet
forall a. IntMap a
IM.empty) IntMap CFG
cfgs IntMap FReturnBehavior
calls IntMap Invariants
invs IntMap Postconditions
forall a. IntMap a
IM.empty IntMap (Set SStatePart)
forall a. IntMap a
IM.empty Indirections
inds IntMap FInit
finits IntMap VCS
vcs' IntMap VerificationResult
results IntMap IntSet
forall a. IntMap a
IM.empty Int64
runningTime
 where
  purge :: Bool -> Bool -> VCS -> VCS
purge Bool
keep_preconditions Bool
keep_assertions VCS
vcs = (VerificationCondition -> Bool) -> VCS -> VCS
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Bool -> Bool -> VerificationCondition -> Bool
keep_vcs Bool
keep_preconditions Bool
keep_assertions) VCS
vcs

  keep_vcs :: Bool -> Bool -> VerificationCondition -> Bool
keep_vcs Bool
keep_preconditions Bool
keep_assertions (Precondition SimpleExpr
_ Int
_ SimpleExpr
_ Int
_)   = Bool
keep_preconditions
  keep_vcs Bool
keep_preconditions Bool
keep_assertions (Assertion    SimpleExpr
_ SimpleExpr
_ Int
_ SimpleExpr
_ Int
_) = Bool
keep_assertions
  keep_vcs Bool
keep_preconditions Bool
keep_assertions VerificationCondition
_                        = Bool
True



-- | Getting the symbol table
ctxt_symbol_table :: Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt =
  case Context -> SymbolTable
ctxt_syms Context
ctxt of
    SymbolTable IntMap Symbol
tbl -> IntMap Symbol
tbl



-- | Reading from a read-only data section.
--
-- Reads maximally up to 8 bytes. Returns @Nothing@ if the given address is out-of-range.
read_from_ro_datasection ::
     Context       -- ^ The context 
  -> Word64        -- ^ An address
  -> Int           -- ^ Size, i.e., the number of bytes to read
  -> Maybe Word64
read_from_ro_datasection :: Context -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection Context
ctxt Word64
a Int
si = [Word8] -> Word64
bytes_to_word ([Word8] -> Word64) -> Maybe [Word8] -> Maybe Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binary -> Word64 -> Int -> Maybe [Word8]
forall a. BinaryClass a => a -> Word64 -> Int -> Maybe [Word8]
binary_read_ro_data (Context -> Binary
ctxt_binary Context
ctxt) Word64
a Int
si

-- | Reading from a writable data section.
--
-- Reads maximally up to 8 bytes. Returns @Nothing@ if the given address is out-of-range.
read_from_datasection ::
     Context       -- ^ The context 
  -> Word64        -- ^ An address
  -> Int           -- ^ Size, i.e., the number of bytes to read
  -> Maybe Word64
read_from_datasection :: Context -> Word64 -> Int -> Maybe Word64
read_from_datasection Context
ctxt Word64
a Int
si = [Word8] -> Word64
bytes_to_word ([Word8] -> Word64) -> Maybe [Word8] -> Maybe Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binary -> Word64 -> Int -> Maybe [Word8]
forall a. BinaryClass a => a -> Word64 -> Int -> Maybe [Word8]
binary_read_data (Context -> Binary
ctxt_binary Context
ctxt) Word64
a Int
si



-- | Is the immediate roughly in range to be an address?
is_roughly_an_address ::
  Context                              -- ^ The context
  -> Word64                            -- ^ An address
  -> Bool
is_roughly_an_address :: Context -> Word64 -> Bool
is_roughly_an_address Context
ctxt Word64
a = 
  let si :: SectionsInfo
si = Context -> SectionsInfo
ctxt_sections Context
ctxt in
    Word64
a Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= SectionsInfo -> Word64
si_min_address SectionsInfo
si Bool -> Bool -> Bool
&& Word64
a Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= SectionsInfo -> Word64
si_max_address SectionsInfo
si

-- | Find a section for an address (see @`SectionsInfo`@)
find_section_for_address ::
   Context                              -- ^ The context
   -> Word64                            -- ^ An address
   -> Maybe (String, String, Word64, Word64)
find_section_for_address :: Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_for_address Context
ctxt Word64
a =
  if Context -> Word64 -> Bool
is_roughly_an_address Context
ctxt Word64
a then
    ((String, String, Word64, Word64) -> Bool)
-> [(String, String, Word64, Word64)]
-> Maybe (String, String, Word64, Word64)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> (String, String, Word64, Word64) -> Bool
forall a a b. (Ord a, Num a) => a -> (a, b, a, a) -> Bool
address_in_section Word64
a) (SectionsInfo -> [(String, String, Word64, Word64)]
si_sections (SectionsInfo -> [(String, String, Word64, Word64)])
-> SectionsInfo -> [(String, String, Word64, Word64)]
forall a b. (a -> b) -> a -> b
$ Context -> SectionsInfo
ctxt_sections Context
ctxt)
  else
    Maybe (String, String, Word64, Word64)
forall a. Maybe a
Nothing
 where
  address_in_section :: a -> (a, b, a, a) -> Bool
address_in_section a
a (a
_,b
_,a
a0,a
si) = a
a0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
a Bool -> Bool -> Bool
&& a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
a0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si


-- | Find a section ending at address (see @`SectionsInfo`@)
find_section_ending_at ::
   Context                              -- ^ The context
   -> Word64                            -- ^ An address
   -> Maybe (String, String, Word64, Word64)
find_section_ending_at :: Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_ending_at Context
ctxt Word64
a = ((String, String, Word64, Word64) -> Bool)
-> [(String, String, Word64, Word64)]
-> Maybe (String, String, Word64, Word64)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Word64 -> (String, String, Word64, Word64) -> Bool
forall a a b. (Eq a, Num a) => a -> (a, b, a, a) -> Bool
address_ends_at_section Word64
a) (SectionsInfo -> [(String, String, Word64, Word64)]
si_sections (SectionsInfo -> [(String, String, Word64, Word64)])
-> SectionsInfo -> [(String, String, Word64, Word64)]
forall a b. (a -> b) -> a -> b
$ Context -> SectionsInfo
ctxt_sections Context
ctxt)
 where
  address_ends_at_section :: a -> (a, b, a, a) -> Bool
address_ends_at_section a
a (a
_,b
_,a
a0,a
si) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
si



-- | Fetching an instruction
--
-- Returns @Nothing@ if the given address is out-of-range.
fetch_instruction ::
  Context              -- ^ The context
  -> Word64            -- ^ An address
  -> IO (Maybe X86.Instruction)
fetch_instruction :: Context -> Word64 -> IO (Maybe Instruction)
fetch_instruction Context
ctxt Word64
a =
  case Binary -> Word64 -> Int -> Maybe [Word8]
forall a. BinaryClass a => a -> Word64 -> Int -> Maybe [Word8]
binary_read_ro_data (Context -> Binary
ctxt_binary Context
ctxt) Word64
a Int
20 of -- maximum instruction length == 15
    Maybe [Word8]
Nothing -> Maybe Instruction -> IO (Maybe Instruction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Instruction
forall a. Maybe a
Nothing
    Just [Word8]
bytes -> IORef (IntMap Instruction)
-> [Word8] -> Word64 -> IO (Maybe Instruction)
disassemble (Context -> IORef (IntMap Instruction)
ctxt_ioref Context
ctxt) [Word8]
bytes Word64
a


-- | Pretty printing an instruction
pp_instruction ::
  Context             -- ^ The context
  -> X86.Instruction  -- ^ An instruction
  -> String
pp_instruction :: Context -> Instruction -> String
pp_instruction Context
ctxt Instruction
i =
  if Opcode -> Bool
isCall (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) then
    Instruction -> String
forall a. Show a => a -> String
show Instruction
i String -> String -> String
forall a. [a] -> [a] -> [a]
++
      case Instruction -> [Operand]
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation
-> [GenericOperand storage]
Instr.srcs Instruction
i of
        [Immediate Word64
imm] ->
          case Int -> IntMap Symbol -> Maybe Symbol
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
imm) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt of
            Just (Relocated_Function String
sym) -> String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
sym String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
            Just (Internal_Label String
sym)     -> String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
sym String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
            Maybe Symbol
Nothing  -> String
" (0x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
imm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        [Operand]
_ -> String
""
  else
    Instruction -> String
forall a. Show a => a -> String
show Instruction
i



instance Show PointerDomain where
  show :: PointerDomain -> String
show (Domain_Bases NESet PointerBase
bs)     = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((PointerBase -> String) -> [PointerBase] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PointerBase -> String
forall a. Show a => a -> String
show ([PointerBase] -> [String]) -> [PointerBase] -> [String]
forall a b. (a -> b) -> a -> b
$ NESet PointerBase -> [PointerBase]
forall a. NESet a -> [a]
neSetToList NESet PointerBase
bs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]_B"
  show (Domain_Sources NESet BotSrc
srcs) = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((BotSrc -> String) -> [BotSrc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map BotSrc -> String
forall a. Show a => a -> String
show ([BotSrc] -> [String]) -> [BotSrc] -> [String]
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> [BotSrc]
forall a. NESet a -> [a]
neSetToList NESet BotSrc
srcs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]_S"


-- | Show function initialisation
instance Show FInit where
 show :: FInit -> String
show (FInit Set (StatePart, Maybe SValue)
sps Map (SStatePart, SStatePart) MemRelation
m) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(/=) []) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ 
  [ String
"Stateparts:" 
  , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> String)
-> [(StatePart, Maybe SValue)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart -> String
forall a. Show a => a -> String
show (StatePart -> String)
-> ((StatePart, Maybe SValue) -> StatePart)
-> (StatePart, Maybe SValue)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StatePart, Maybe SValue) -> StatePart
forall a b. (a, b) -> a
fst) ([(StatePart, Maybe SValue)] -> [String])
-> [(StatePart, Maybe SValue)] -> [String]
forall a b. (a -> b) -> a -> b
$ Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a. Set a -> [a]
S.toList (Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)])
-> Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> Bool)
-> Set (StatePart, Maybe SValue) -> Set (StatePart, Maybe SValue)
forall a. (a -> Bool) -> Set a -> Set a
S.filter ((Maybe SValue -> Maybe SValue -> Bool
forall a. Eq a => a -> a -> Bool
(==) Maybe SValue
forall a. Maybe a
Nothing) (Maybe SValue -> Bool)
-> ((StatePart, Maybe SValue) -> Maybe SValue)
-> (StatePart, Maybe SValue)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StatePart, Maybe SValue) -> Maybe SValue
forall a b. (a, b) -> b
snd) Set (StatePart, Maybe SValue)
sps
  , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> String)
-> [(StatePart, Maybe SValue)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart, Maybe SValue) -> String
forall a a. (Show a, Show a) => (a, Maybe a) -> String
show_sp ([(StatePart, Maybe SValue)] -> [String])
-> [(StatePart, Maybe SValue)] -> [String]
forall a b. (a -> b) -> a -> b
$ Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a. Set a -> [a]
S.toList (Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)])
-> Set (StatePart, Maybe SValue) -> [(StatePart, Maybe SValue)]
forall a b. (a -> b) -> a -> b
$ ((StatePart, Maybe SValue) -> Bool)
-> Set (StatePart, Maybe SValue) -> Set (StatePart, Maybe SValue)
forall a. (a -> Bool) -> Set a -> Set a
S.filter ((Maybe SValue -> Maybe SValue -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe SValue
forall a. Maybe a
Nothing) (Maybe SValue -> Bool)
-> ((StatePart, Maybe SValue) -> Maybe SValue)
-> (StatePart, Maybe SValue)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StatePart, Maybe SValue) -> Maybe SValue
forall a b. (a, b) -> b
snd) Set (StatePart, Maybe SValue)
sps
  , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((SStatePart, SStatePart), MemRelation) -> String)
-> [((SStatePart, SStatePart), MemRelation)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((SStatePart, SStatePart), MemRelation) -> String
forall a b a. (Show a, Show b, Show a) => ((a, b), a) -> String
show_entry ([((SStatePart, SStatePart), MemRelation)] -> [String])
-> [((SStatePart, SStatePart), MemRelation)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map (SStatePart, SStatePart) MemRelation
-> [((SStatePart, SStatePart), MemRelation)]
forall k a. Map k a -> [(k, a)]
M.toList Map (SStatePart, SStatePart) MemRelation
m ]
  where
    show_sp :: (a, Maybe a) -> String
show_sp (a
sp,Just a
v)    = a -> String
forall a. Show a => a -> String
show a
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
    show_entry :: ((a, b), a) -> String
show_entry ((a
sp0,b
sp1),a
r) = (a, b) -> String
forall a. Show a => a -> String
show (a
sp0,b
sp1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
r




instance Show VerificationResult where
 show :: VerificationResult -> String
show VerificationResult
VerificationSuccess               = String
"VerificationSuccess"
 show VerificationResult
VerificationSuccesWithAssumptions = String
"VerificationSuccesWithAssumptions"
 show VerificationResult
VerificationUnresolvedIndirection = String
"VerificationUnresolvedIndirection"
 show (VerificationError String
msg)           = String
"VerificationError: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg


instance Show JumpTable where
  show :: JumpTable -> String
show (JumpTable Operand
idx Int
bnd Operand
trgt IntMap Word64
tbl) = String
"JumpTable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
idx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" < " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
bnd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" --> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Operand -> String
forall a. Show a => a -> String
show Operand
trgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IntSet -> String
showHex_set ([Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Word64 -> Int) -> [Word64] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Word64] -> [Int]) -> [Word64] -> [Int]
forall a b. (a -> b) -> a -> b
$ IntMap Word64 -> [Word64]
forall a. IntMap a -> [a]
IM.elems IntMap Word64
tbl)

instance Show Indirection where
  show :: Indirection -> String
show (Indirection_JumpTable JumpTable
tbl)   = JumpTable -> String
forall a. Show a => a -> String
show JumpTable
tbl
  show (Indirection_Resolved  Set ResolvedJumpTarget
trgts) = Set ResolvedJumpTarget -> String
forall a. Show a => a -> String
show Set ResolvedJumpTarget
trgts





instance Show VerificationCondition where
  show :: VerificationCondition -> String
show (Precondition SimpleExpr
lhs Int
_ SimpleExpr
rhs Int
_)      = SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" SEP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
rhs
  show (Assertion SimpleExpr
a  SimpleExpr
lhs Int
_ SimpleExpr
rhs Int
_)      = String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" SEP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
forall a. Show a => a -> String
show SimpleExpr
rhs
  show (FunctionPointers Word64
a IntSet
ptrs)       = String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": function pointers " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IntSet -> String
showHex_set IntSet
ptrs
  show (FunctionConstraint String
f Word64
a [(Register, SimpleExpr)]
ps Set StatePart
sps) = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (((Register, SimpleExpr) -> String)
-> [(Register, SimpleExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Register, SimpleExpr) -> String
forall a a. (Show a, Show a) => (a, a) -> String
show_param [(Register, SimpleExpr)]
ps) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") PRESERVES " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((StatePart -> String) -> [StatePart] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map StatePart -> String
forall a. Show a => a -> String
show ([StatePart] -> [String]) -> [StatePart] -> [String]
forall a b. (a -> b) -> a -> b
$ Set StatePart -> [StatePart]
forall a. Set a -> [a]
S.toList Set StatePart
sps))
   where
    show_param :: (a, a) -> String
show_param (a
r,a
e) = a -> String
forall a. Show a => a -> String
show a
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
strip_parentheses (a -> String
forall a. Show a => a -> String
show a
e)

-- | Is the given verification condition an assertion?
is_assertion :: VerificationCondition -> Bool
is_assertion (Assertion SimpleExpr
_ SimpleExpr
_ Int
_ SimpleExpr
_ Int
_) = Bool
True
is_assertion VerificationCondition
_                     = Bool
False

-- | Is the given verification condition a precondition?
is_precondition :: VerificationCondition -> Bool
is_precondition (Precondition SimpleExpr
_ Int
_ SimpleExpr
_ Int
_) = Bool
True
is_precondition VerificationCondition
_                      = Bool
False

-- | Is the given verification condition a function constraint?
is_func_constraint :: VerificationCondition -> Bool
is_func_constraint (FunctionConstraint String
_ Word64
_ [(Register, SimpleExpr)]
_ Set StatePart
_) = Bool
True
is_func_constraint VerificationCondition
_                            = Bool
False


-- | Is the given verification condition a function pointer introduction?
is_functionpointers :: VerificationCondition -> Bool
is_functionpointers (FunctionPointers Word64
_ IntSet
_) = Bool
True
is_functionpointers VerificationCondition
_                      = Bool
False

-- | Count the number of assertions in the set of verification conditions.
count_instructions_with_assertions :: VCS -> Int
count_instructions_with_assertions = Set SimpleExpr -> Int
forall a. Set a -> Int
S.size (Set SimpleExpr -> Int) -> (VCS -> Set SimpleExpr) -> VCS -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerificationCondition -> SimpleExpr) -> VCS -> Set SimpleExpr
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\(Assertion SimpleExpr
rip SimpleExpr
_ Int
_ SimpleExpr
_ Int
_) -> SimpleExpr
rip) (VCS -> Set SimpleExpr) -> (VCS -> VCS) -> VCS -> Set SimpleExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerificationCondition -> Bool) -> VCS -> VCS
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_assertion





ctxt_continue_on_unknown_instruction :: Context -> Bool
ctxt_continue_on_unknown_instruction = Config -> Bool
continue_on_unknown_instruction (Config -> Bool) -> (Context -> Config) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config
ctxt_generate_pdfs :: Context -> Bool
ctxt_generate_pdfs = Config -> Bool
generate_pdfs (Config -> Bool) -> (Context -> Config) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config
ctxt_verbose_logs :: Context -> Bool
ctxt_verbose_logs = Config -> Bool
verbose_logs (Config -> Bool) -> (Context -> Config) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config
ctxt_store_preconditions_in_L0 :: Context -> Bool
ctxt_store_preconditions_in_L0 = Config -> Bool
store_preconditions_in_L0 (Config -> Bool) -> (Context -> Config) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config
ctxt_store_assertions_in_L0 :: Context -> Bool
ctxt_store_assertions_in_L0 = Config -> Bool
store_assertions_in_L0 (Config -> Bool) -> (Context -> Config) -> Context -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_time :: Context -> Int
ctxt_max_time :: Context -> Int
ctxt_max_time = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_time (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_num_of_cases :: Context -> Int
ctxt_max_num_of_cases :: Context -> Int
ctxt_max_num_of_cases = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_num_of_cases (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_num_of_bases :: Context -> Int
ctxt_max_num_of_bases :: Context -> Int
ctxt_max_num_of_bases = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_num_of_bases (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_num_of_sources :: Context -> Int
ctxt_max_num_of_sources :: Context -> Int
ctxt_max_num_of_sources = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_num_of_sources (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_jump_table_size :: Context -> Int
ctxt_max_jump_table_size :: Context -> Int
ctxt_max_jump_table_size = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_jump_table_size (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config

ctxt_max_expr_size :: Context -> Int
ctxt_max_expr_size :: Context -> Int
ctxt_max_expr_size = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (Context -> Natural) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Natural
max_expr_size (Config -> Natural) -> (Context -> Config) -> Context -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxt_config



-- | Read in the .L0 file from a file with the given file name.
--   May produce an error if no L0 can be read from the file.
--   Returns the L0 stored in the .L0 file.
ctxt_read_L0 :: 
   String        -- ^ The directory name
   -> String     -- ^ The file name of the binary
   -> IO Context
ctxt_read_L0 :: String -> String -> IO Context
ctxt_read_L0 String
dirname String
name = do
  ByteString
rcontents <- String -> IO ByteString
BS.readFile (String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".L0")
  IORef (IntMap Instruction)
ioref     <- IntMap Instruction -> IO (IORef (IntMap Instruction))
forall a. a -> IO (IORef a)
newIORef IntMap Instruction
forall a. IntMap a
IM.empty
  Maybe Binary
bcontents <- String -> String -> IO (Maybe Binary)
read_binary String
dirname String
name
  case (ByteString -> Either String Context_
forall a. Serialize a => ByteString -> Either String a
Cereal.decode ByteString
rcontents, Maybe Binary
bcontents) of
    (Left String
err,Maybe Binary
_)           -> String -> IO Context
forall a. HasCallStack => String -> a
error (String -> IO Context) -> String -> IO Context
forall a b. (a -> b) -> a -> b
$ String
"Could not read verification L0 in file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".L0") String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
err
    (Either String Context_
_,Maybe Binary
Nothing)            -> String -> IO Context
forall a. HasCallStack => String -> a
error (String -> IO Context) -> String -> IO Context
forall a b. (a -> b) -> a -> b
$ String
"Cannot read binary file: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
    (Right Context_
ctxt_,Just Binary
bin) -> Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> IO Context) -> Context -> IO Context
forall a b. (a -> b) -> a -> b
$ Binary -> IORef (IntMap Instruction) -> Context_ -> Context
Context Binary
bin IORef (IntMap Instruction)
ioref Context_
ctxt_





-- | Returns true iff an instruction can be fetched from the address.
address_has_instruction :: Context -> a -> Bool
address_has_instruction Context
ctxt a
a =
  case Context -> Word64 -> Maybe (String, String, Word64, Word64)
find_section_for_address Context
ctxt (Word64 -> Maybe (String, String, Word64, Word64))
-> Word64 -> Maybe (String, String, Word64, Word64)
forall a b. (a -> b) -> a -> b
$ a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a of
    Maybe (String, String, Word64, Word64)
Nothing                    -> Bool
False
    Just (String
segment,String
section,Word64
_,Word64
_) -> (String
segment,String
section) (String, String) -> [(String, String)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(String, String)]
sections_with_instructions Bool -> Bool -> Bool
&& IO (Maybe Instruction) -> Maybe Instruction
forall a. IO a -> a
unsafePerformIO (Context -> Word64 -> IO (Maybe Instruction)
fetch_instruction Context
ctxt (Word64 -> IO (Maybe Instruction))
-> Word64 -> IO (Maybe Instruction)
forall a b. (a -> b) -> a -> b
$ a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) Maybe Instruction -> Maybe Instruction -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Instruction
forall a. Maybe a
Nothing