{-# LANGUAGE DeriveGeneric, DefaultSignatures #-}

{-|
Module      : VerificationReportInterface
Description : The interface to the @.report@ generated after running FoxDec.

The interface to the @.report@ generated after running FoxDec.
After running FoxDec, a \"verification report\" (an object of type @"Context"@) can be retrieved from the generated .report file (see function @ctxt_read_report@).
Essentially, this module provides hooks into some of the information retrieved and derived from the binary,
including instructions, invariants, function entry points, etc.

A verification report is represented by the type @"Context"@, as internally it
is just the context passed around and maintained during verification.

The main flow is to read the .report file and use these functions to retrieve information.
The following example reads in a .report file provided as first command-line parameter and outputs the function entries:

>  main = do
>    args <- getArgs
>    ctxt <- ctxt_read_report (args !! 0) (args !! 1)
>    putStrLn $ show $ ctxt_get_function_entries ctxt

Some of the information is automatically also exported in plain-text format, for easy access.
-}


module VerificationReportInterface
  (
    Retrieve,FunctionEntry,InstructionAddress,
    ctxt_read_report,
    retrieve_io,
    ctxt_get_function_entries,
    ctxt_get_instruction_addresses,
    ctxt_get_indirections,
    ctxt_get_instruction,
    ctxt_get_invariant,
    ctxt_get_internal_function_calls,
    ctxt_get_cfg,
    ctxt_get_function_init,
    ctxt_get_postcondition
  )
where

import Analysis.Context
import Analysis.SymbolicExecution
import Base
import Data.CallGraph
import Data.Binary
import Data.ControlFlow
import Data.Pointers
import Data.SimplePred
import Pass.CFG_Gen

import Data.IORef
import qualified Data.Serialize as Cereal hiding (get,put)
import qualified Data.IntMap as IM
import qualified Data.Set as S
import qualified Data.IntSet as IS
import System.IO.Unsafe (unsafePerformIO)
import qualified Data.ByteString as BS (readFile,writeFile) 
import System.Exit (die)
import qualified X86.Instruction as X86







-- | The return type when retrieving information from a verification report: either an error message or a result.
type Retrieve a = Context -> Either String a
-- | Function Entries are simply integers
type FunctionEntry      = Int
-- | Instruction Addresses are simply integers
type InstructionAddress = Int



-- | Read in the .report file from a file with the given file name.
--   May produce an error if no report can be read from the file.
--   Returns the verification report stored in the .report file.
ctxt_read_report :: 
      String     -- ^ The directory name
   -> String     -- ^ The file name of the binary
   -> IO Context
ctxt_read_report :: String -> String -> IO Context
ctxt_read_report 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
".report")
  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 report 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
".report") 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_

-- | Retrieve information from a @"Context"@ read from a .report file, or die with an error message.
-- For example:
--
-- >   retrieve_io $ ctxt_get_instruction a ctxt
--
-- This code reads in a .report file with the given @filename@,  and reads the instruction at address @a@ if any.
retrieve_io :: Either String a -> IO a
retrieve_io :: Either String a -> IO a
retrieve_io Either String a
retrieve_result = do
  case Either String a
retrieve_result of
    Left String
err -> String -> IO a
forall a. String -> IO a
die String
err
    Right a
result -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

 




-- | Retrieve all function entries.
--
-- Returns a set of funtion entries.
ctxt_get_function_entries :: Retrieve (S.Set FunctionEntry) 
ctxt_get_function_entries :: Retrieve (Set FunctionEntry)
ctxt_get_function_entries = Set FunctionEntry -> Either String (Set FunctionEntry)
forall a b. b -> Either a b
Right (Set FunctionEntry -> Either String (Set FunctionEntry))
-> (Context -> Set FunctionEntry) -> Retrieve (Set FunctionEntry)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FunctionEntry] -> Set FunctionEntry
forall a. Ord a => [a] -> Set a
S.fromList ([FunctionEntry] -> Set FunctionEntry)
-> (Context -> [FunctionEntry]) -> Context -> Set FunctionEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap FReturnBehavior -> [FunctionEntry]
forall a. IntMap a -> [FunctionEntry]
IM.keys (IntMap FReturnBehavior -> [FunctionEntry])
-> (Context -> IntMap FReturnBehavior)
-> Context
-> [FunctionEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IntMap FReturnBehavior
ctxt_calls


-- | Retrieve all instruction addresses.
--
-- Returns a set of instruction addresses.
ctxt_get_instruction_addresses :: Retrieve (S.Set InstructionAddress)
ctxt_get_instruction_addresses :: Retrieve (Set FunctionEntry)
ctxt_get_instruction_addresses Context
ctxt =
  Set FunctionEntry -> Either String (Set FunctionEntry)
forall a b. b -> Either a b
Right (Set FunctionEntry -> Either String (Set FunctionEntry))
-> Set FunctionEntry -> Either String (Set FunctionEntry)
forall a b. (a -> b) -> a -> b
$ [Set FunctionEntry] -> Set FunctionEntry
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set FunctionEntry] -> Set FunctionEntry)
-> [Set FunctionEntry] -> Set FunctionEntry
forall a b. (a -> b) -> a -> b
$ (CFG -> Set FunctionEntry) -> [CFG] -> [Set FunctionEntry]
forall a b. (a -> b) -> [a] -> [b]
map CFG -> Set FunctionEntry
cfg_to_addresses ([CFG] -> [Set FunctionEntry]) -> [CFG] -> [Set FunctionEntry]
forall a b. (a -> b) -> a -> b
$ IntMap CFG -> [CFG]
forall a. IntMap a -> [a]
IM.elems (IntMap CFG -> [CFG]) -> IntMap CFG -> [CFG]
forall a b. (a -> b) -> a -> b
$ Context -> IntMap CFG
ctxt_cfgs Context
ctxt
 where
  cfg_to_addresses :: CFG -> Set FunctionEntry
cfg_to_addresses CFG
g = [FunctionEntry] -> Set FunctionEntry
forall a. Ord a => [a] -> Set a
S.fromList ([FunctionEntry] -> Set FunctionEntry)
-> [FunctionEntry] -> Set FunctionEntry
forall a b. (a -> b) -> a -> b
$ [[FunctionEntry]] -> [FunctionEntry]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FunctionEntry]] -> [FunctionEntry])
-> [[FunctionEntry]] -> [FunctionEntry]
forall a b. (a -> b) -> a -> b
$ IntMap [FunctionEntry] -> [[FunctionEntry]]
forall a. IntMap a -> [a]
IM.elems (IntMap [FunctionEntry] -> [[FunctionEntry]])
-> IntMap [FunctionEntry] -> [[FunctionEntry]]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [FunctionEntry]
cfg_blocks CFG
g

-- | Retrieve all indirections
--
-- Returns a mapping that provides for some instruction addresses a set of jump targets.
ctxt_get_indirections :: Retrieve Indirections
ctxt_get_indirections :: Retrieve Indirections
ctxt_get_indirections = Indirections -> Either String Indirections
forall a b. b -> Either a b
Right (Indirections -> Either String Indirections)
-> (Context -> Indirections) -> Retrieve Indirections
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Indirections
ctxt_inds


-- | Retrieve instruction for a given instruction address, both as datastructure and pretty-printed
ctxt_get_instruction :: InstructionAddress -> Retrieve (X86.Instruction,String)
ctxt_get_instruction :: FunctionEntry -> Retrieve (Instruction, String)
ctxt_get_instruction FunctionEntry
a Context
ctxt =
  case IO (Maybe Instruction) -> Maybe Instruction
forall a. IO a -> a
unsafePerformIO (IO (Maybe Instruction) -> Maybe Instruction)
-> IO (Maybe Instruction) -> Maybe Instruction
forall a b. (a -> b) -> a -> b
$ Context -> Word64 -> IO (Maybe Instruction)
fetch_instruction Context
ctxt (Word64 -> IO (Maybe Instruction))
-> Word64 -> IO (Maybe Instruction)
forall a b. (a -> b) -> a -> b
$ FunctionEntry -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral FunctionEntry
a of -- Should be safe as result is immutable.
    Maybe Instruction
Nothing -> String -> Either String (Instruction, String)
forall a b. a -> Either a b
Left (String -> Either String (Instruction, String))
-> String -> Either String (Instruction, String)
forall a b. (a -> b) -> a -> b
$ String
"Could not disassemble instruction at address: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FunctionEntry -> String
forall a. (Integral a, Show a) => a -> String
showHex FunctionEntry
a
    Just Instruction
i  -> (Instruction, String) -> Either String (Instruction, String)
forall a b. b -> Either a b
Right (Instruction
i,Context -> Instruction -> String
pp_instruction Context
ctxt Instruction
i)

-- | Retrieve invariant for a given function entry and instruction address
--
-- An invariant is a predicate provding information over registers, memory, flags, and verification conditions.
ctxt_get_invariant :: FunctionEntry -> InstructionAddress -> Retrieve Pred
ctxt_get_invariant :: FunctionEntry -> FunctionEntry -> Retrieve Pred
ctxt_get_invariant FunctionEntry
entry FunctionEntry
a Context
ctxt =
  let fctxt :: FContext
fctxt = Context -> FunctionEntry -> FContext
mk_fcontext Context
ctxt FunctionEntry
entry in
    case FContext -> FunctionEntry -> Maybe Pred
get_invariant FContext
fctxt FunctionEntry
a of
      Maybe Pred
Nothing -> String -> Either String Pred
forall a b. a -> Either a b
Left (String -> Either String Pred) -> String -> Either String Pred
forall a b. (a -> b) -> a -> b
$ String
"Cannot retrieve invariant for function entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FunctionEntry -> String
forall a. (Integral a, Show a) => a -> String
showHex FunctionEntry
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and instruction address " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FunctionEntry -> String
forall a. (Integral a, Show a) => a -> String
showHex FunctionEntry
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in verification report."
      Just Pred
p  -> Pred -> Either String Pred
forall a b. b -> Either a b
Right Pred
p

-- | Retrieve all internal function calls for a given function entry
--
-- Returns a set of function entries.
ctxt_get_internal_function_calls :: FunctionEntry -> Retrieve (S.Set FunctionEntry)
ctxt_get_internal_function_calls :: FunctionEntry -> Retrieve (Set FunctionEntry)
ctxt_get_internal_function_calls FunctionEntry
entry Context
ctxt = 
  FunctionEntry -> Retrieve CFG
ctxt_get_cfg FunctionEntry
entry Context
ctxt Either String CFG
-> (CFG -> Either String (Set FunctionEntry))
-> Either String (Set FunctionEntry)
forall a b c. Either a b -> (b -> Either a c) -> Either a c
>>> (Set FunctionEntry -> Either String (Set FunctionEntry)
forall a b. b -> Either a b
Right (Set FunctionEntry -> Either String (Set FunctionEntry))
-> (CFG -> Set FunctionEntry)
-> CFG
-> Either String (Set FunctionEntry)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Set FunctionEntry
toSet (IntSet -> Set FunctionEntry)
-> (CFG -> IntSet) -> CFG -> Set FunctionEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> CFG -> IntSet
calls_of_cfg Context
ctxt)


-- | Retrieve a CFG for a given function entry
ctxt_get_cfg :: FunctionEntry -> Retrieve CFG
ctxt_get_cfg :: FunctionEntry -> Retrieve CFG
ctxt_get_cfg = (Context -> IntMap CFG) -> FunctionEntry -> Retrieve CFG
forall a. (Context -> IntMap a) -> FunctionEntry -> Retrieve a
ctxt_get Context -> IntMap CFG
ctxt_cfgs


-- | Retrieve a function initialization for a given function entry
ctxt_get_function_init :: FunctionEntry -> Retrieve FInit
ctxt_get_function_init :: FunctionEntry -> Retrieve FInit
ctxt_get_function_init = (Context -> IntMap FInit) -> FunctionEntry -> Retrieve FInit
forall a. (Context -> IntMap a) -> FunctionEntry -> Retrieve a
ctxt_get Context -> IntMap FInit
ctxt_finits


-- | Retrieve a function initialization for a given function entry
ctxt_get_postcondition :: FunctionEntry -> Retrieve FReturnBehavior
ctxt_get_postcondition :: FunctionEntry -> Retrieve FReturnBehavior
ctxt_get_postcondition = (Context -> IntMap FReturnBehavior)
-> FunctionEntry -> Retrieve FReturnBehavior
forall a. (Context -> IntMap a) -> FunctionEntry -> Retrieve a
ctxt_get Context -> IntMap FReturnBehavior
ctxt_calls


-- | Retrieve verification conditions for a given function entry, both as a datastructure and pretty-printed
--ctxt_get_vcs :: FunctionEntry -> Retrieve (S.Set VerificationCondition, String)
--ctxt_get_vcs entry ctxt = 
--  ctxt_get ctxt_vcs entry ctxt >>> (\vcs -> Right (vcs, summarize_verification_conditions ctxt entry))









(>>>) :: Either a b -> (b -> Either a c) -> Either a c
>>> :: Either a b -> (b -> Either a c) -> Either a c
(>>>) (Left a
a) b -> Either a c
_  = a -> Either a c
forall a b. a -> Either a b
Left a
a
(>>>) (Right b
b) b -> Either a c
e = b -> Either a c
e b
b

ctxt_get :: (Context -> IM.IntMap a) -> FunctionEntry -> Retrieve a
ctxt_get :: (Context -> IntMap a) -> FunctionEntry -> Retrieve a
ctxt_get Context -> IntMap a
lens FunctionEntry
entry Context
ctxt =
  case FunctionEntry -> IntMap a -> Maybe a
forall a. FunctionEntry -> IntMap a -> Maybe a
IM.lookup FunctionEntry
entry (IntMap a -> Maybe a) -> IntMap a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Context -> IntMap a
lens Context
ctxt of
    Maybe a
Nothing -> String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ String
"Cannot find function entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FunctionEntry -> String
forall a. (Integral a, Show a) => a -> String
showHex FunctionEntry
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in verification report."
    Just a
r  -> a -> Either String a
forall a b. b -> Either a b
Right a
r



toSet :: IS.IntSet -> S.Set Int
toSet :: IntSet -> Set FunctionEntry
toSet = [FunctionEntry] -> Set FunctionEntry
forall a. Ord a => [a] -> Set a
S.fromList ([FunctionEntry] -> Set FunctionEntry)
-> (IntSet -> [FunctionEntry]) -> IntSet -> Set FunctionEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [FunctionEntry]
IS.toList