{-# LANGUAGE PartialTypeSignatures , DeriveGeneric, BangPatterns, StrictData, ScopedTypeVariables, FunctionalDependencies, FlexibleInstances, UndecidableInstances, FlexibleContexts#-}

module WithAbstractPredicates.ContextSensitiveAnalysis where

import Base
import Config

import WithAbstractPredicates.Class
import WithAbstractPredicates.GenerateCFG
import WithAbstractPredicates.GenerateInvariants
import WithAbstractPredicates.ControlFlow

import Data.JumpTarget
import Data.Symbol
import Data.L0
import Data.CFG
import Data.Indirection
import Data.VerificationCondition
import Data.X86.Opcode
import Data.X86.Instruction

import Binary.Generic
import Binary.FunctionNames



import Algorithm.SCC



import Data.Word
import Data.List
import Data.List.Extra (firstJust)
import Data.Maybe
import Data.IORef
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 Control.Monad.State.Strict
import Control.Monad.Reader
import Control.Monad.Extra




import GHC.Generics
import Debug.Trace












type WithLifting bin pred finit v = StateT (L0 pred finit v) (ReaderT (bin,Config) IO)


-- A mapping of blockIDs to predicates
type Invariants pred = IM.IntMap pred




type Recursions = IM.IntMap IS.IntSet






data AnalysisResult pred finit v = FoundNewCalls (IM.IntMap finit) | AnalyzedWithResult (FResult pred v)





-- Lift the binary to the L0 representation
lift_to_L0 :: WithAbstractPredicates bin pred finit v => Config -> bin -> finit -> IO (L0 pred finit v)
lift_to_L0 :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Config -> bin -> finit -> IO (L0 pred finit v)
lift_to_L0 Config
config bin
bin finit
finit = do
  [Key]
entries <- IO [Key]
get_entries

  let empty_L0 :: L0 pred finit v
empty_L0 = IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
forall pred finit v.
IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
L0 IntMap (finit, Maybe (FResult pred v))
forall a. IntMap a
IM.empty IntMap Indirections
forall a. IntMap a
IM.empty String
""
  let init_L0 :: L0 pred finit v
init_L0 = (Key -> L0 pred finit v -> L0 pred finit v)
-> L0 pred finit v -> [Key] -> L0 pred finit v
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Key
entry -> Key -> finit -> L0 pred finit v -> L0 pred finit v
forall {finit} {pred} {v}.
Key -> finit -> L0 pred finit v -> L0 pred finit v
l0_insert_new_entry Key
entry finit
finit) L0 pred finit v
forall {pred} {finit} {v}. L0 pred finit v
empty_L0 [Key]
entries

  let recs :: IntMap a
recs = IntMap a
forall a. IntMap a
IM.empty
  let entry_graph :: Graph
entry_graph = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Key, IntSet)] -> IntMap IntSet
forall a. [(Key, a)] -> IntMap a
IM.fromList ([Key] -> [IntSet] -> [(Key, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key]
entries ([IntSet] -> [(Key, IntSet)]) -> [IntSet] -> [(Key, IntSet)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [IntSet]
forall a. a -> [a]
repeat IntSet
IS.empty)
  ReaderT (bin, Config) IO (L0 pred finit v)
-> (bin, Config) -> IO (L0 pred finit v)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
-> L0 pred finit v -> ReaderT (bin, Config) IO (L0 pred finit v)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Graph
-> IntMap IntSet
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entry_graph IntMap IntSet
forall a. IntMap a
recs) L0 pred finit v
forall {pred} {v}. L0 pred finit v
init_L0) (bin
bin,Config
config)
 where
  get_entries :: IO [Key]
get_entries = do
    let dirname :: String
dirname = bin -> String
forall a. BinaryClass a => a -> String
binary_dir_name bin
bin
    let name :: String
name    = bin -> String
forall a. BinaryClass a => a -> String
binary_file_name bin
bin
    let fname :: String
fname   = String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".entry" 
    IO [Key] -> IO [Key]
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Key] -> IO [Key]) -> IO [Key] -> IO [Key]
forall a b. (a -> b) -> a -> b
$ String -> IO [Key]
parse (String -> IO [Key]) -> String -> IO [Key]
forall a b. (a -> b) -> a -> b
$! String
fname
  parse :: String -> IO [Key]
parse String
filename = do
    String
ls <- String -> IO String
readFile String
filename
    [Key] -> IO [Key]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Key] -> IO [Key]) -> [Key] -> IO [Key]
forall a b. (a -> b) -> a -> b
$ (String -> Key) -> [String] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map String -> Key
read_line ([String] -> [Key]) -> [String] -> [Key]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
ls
  read_line :: String -> Key
read_line = String -> Key
forall a. (Eq a, Num a) => String -> a
readHex' (String -> Key) -> (String -> String) -> String -> Key
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. HasCallStack => [a] -> [a]
tail (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. HasCallStack => [a] -> [a]
tail



exploreFunctionEntries :: WithAbstractPredicates bin pred finit v => Graph -> Recursions -> WithLifting bin pred finit v ()
exploreFunctionEntries :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries IntMap IntSet
recursions = do
  -- Check if a (mutually) recursive function must be reconsidered as all its calls are done.
  Maybe (Key, IntSet)
rec <- IntMap IntSet -> WithLifting bin pred finit v (Maybe (Key, IntSet))
forall bin pred finit v.
IntMap IntSet -> WithLifting bin pred finit v (Maybe (Key, IntSet))
reconsider_mutual_recursive_call IntMap IntSet
recursions
  case Maybe (Key, IntSet)
rec of
    Just (Key
entry,IntSet
trgts) -> do
      -- If yes, then reinsert the function entry, remove the current known results and continue
      IO () -> WithLifting bin pred finit v ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> WithLifting bin pred finit v ())
-> IO () -> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Reconsidering (due to mutual recursion) entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall {a}. Integral a => a -> String
showHex Key
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as all entries " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IntSet -> String
showHex_set IntSet
trgts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" are now done."
      let entries' :: Graph
entries'    = Graph -> Key -> IntSet -> Graph
graph_add_edges Graph
entries Key
entry IntSet
IS.empty 
      let recursions' :: IntMap IntSet
recursions' = Key -> IntMap IntSet -> IntMap IntSet
forall a. Key -> IntMap a -> IntMap a
IM.delete Key
entry IntMap IntSet
recursions
      (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> WithLifting bin pred finit v ())
-> (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ Key -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
forall {a} {pred} {v} {finit}.
Integral a =>
a -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
l0_adjust_result Key
entry Maybe (FResult pred v)
forall a. Maybe a
Nothing
      Graph -> IntMap IntSet -> Word64 -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> Word64 -> WithLifting bin pred finit v ()
exploreFunctionEntry Graph
entries' IntMap IntSet
recursions' (Word64 -> WithLifting bin pred finit v ())
-> Word64 -> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
entry
    Maybe (Key, IntSet)
Nothing -> do
      -- If not, find next entry to consider
      case Maybe Key
next_entry of
        Maybe Key
Nothing -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
exploreDanglingFunctionPointers
        Just Key
a  -> Graph -> IntMap IntSet -> Word64 -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> Word64 -> WithLifting bin pred finit v ()
exploreFunctionEntry Graph
entries IntMap IntSet
recursions (Word64 -> WithLifting bin pred finit v ())
-> Word64 -> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
a
 where
  next_entry :: Maybe Key
next_entry = Maybe Key
try_end_node_from_node_to_be_reconsidered Maybe Key -> Maybe Key -> Maybe Key
forall a. Eq a => Maybe a -> Maybe a -> Maybe a
`orTry` Graph -> Maybe Key
graph_find_next Graph
entries
  try_end_node_from_node_to_be_reconsidered :: Maybe Key
try_end_node_from_node_to_be_reconsidered = (Key -> Maybe Key) -> [Key] -> Maybe Key
forall a b. (a -> Maybe b) -> [a] -> Maybe b
firstJust (Graph -> Key -> Maybe Key
try_find_end_node_from_node Graph
entries) ([Key] -> Maybe Key) -> [Key] -> Maybe Key
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
IS.toList (IntSet -> [Key]) -> IntSet -> [Key]
forall a b. (a -> b) -> a -> b
$ [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [IntSet]
forall a. IntMap a -> [a]
IM.elems IntMap IntSet
recursions

exploreDanglingFunctionPointers :: WithAbstractPredicates bin pred finit v => WithLifting bin pred finit v ()
exploreDanglingFunctionPointers :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
exploreDanglingFunctionPointers = do
  L0 pred finit v
l0 <- StateT
  (L0 pred finit v) (ReaderT (bin, Config) IO) (L0 pred finit v)
forall s (m :: * -> *). MonadState s m => m s
get
  Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static

  let fptrs :: [Key]
fptrs = ((finit, Maybe (FResult pred v)) -> [Key])
-> [(finit, Maybe (FResult pred v))] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IntMap (finit, Maybe (FResult pred v))
-> (finit, Maybe (FResult pred v)) -> [Key]
forall {a} {a} {pred} {v}.
IntMap a -> (a, Maybe (FResult pred v)) -> [Key]
get_dangling_function_pointers (IntMap (finit, Maybe (FResult pred v))
 -> (finit, Maybe (FResult pred v)) -> [Key])
-> IntMap (finit, Maybe (FResult pred v))
-> (finit, Maybe (FResult pred v))
-> [Key]
forall a b. (a -> b) -> a -> b
$ L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit v
l0) ([(finit, Maybe (FResult pred v))] -> [Key])
-> [(finit, Maybe (FResult pred v))] -> [Key]
forall a b. (a -> b) -> a -> b
$ IntMap (finit, Maybe (FResult pred v))
-> [(finit, Maybe (FResult pred v))]
forall a. IntMap a -> [a]
IM.elems (IntMap (finit, Maybe (FResult pred v))
 -> [(finit, Maybe (FResult pred v))])
-> IntMap (finit, Maybe (FResult pred v))
-> [(finit, Maybe (FResult pred v))]
forall a b. (a -> b) -> a -> b
$ L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit v
l0

  case [Key]
fptrs of
    [] -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
exploreDanglingRelocations
    [Key]
_ -> do
      IO () -> WithLifting bin pred finit v ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> WithLifting bin pred finit v ())
-> IO () -> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Dangling function pointers found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IntSet -> String
showHex_set (IntSet -> String) -> IntSet -> String
forall a b. (a -> b) -> a -> b
$ [Key] -> IntSet
IS.fromList [Key]
fptrs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
      let entries' :: Graph
entries' = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Key, IntSet)] -> IntMap IntSet
forall a. [(Key, a)] -> IntMap a
IM.fromList ([Key] -> [IntSet] -> [(Key, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key]
fptrs ([IntSet] -> [(Key, IntSet)]) -> [IntSet] -> [(Key, IntSet)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [IntSet]
forall a. a -> [a]
repeat IntSet
IS.empty)
      let finit :: finit
finit = Lifting bin pred finit v -> finit
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> finit
new_finit Lifting bin pred finit v
static
      (Key -> WithLifting bin pred finit v ())
-> [Key] -> WithLifting bin pred finit v ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Key
a -> (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> WithLifting bin pred finit v ())
-> (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ Key -> finit -> L0 pred finit v -> L0 pred finit v
forall {finit} {pred} {v}.
Key -> finit -> L0 pred finit v -> L0 pred finit v
l0_insert_new_entry Key
a finit
finit) [Key]
fptrs
      Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
forall a. IntMap a
IM.empty
 where
  get_dangling_function_pointers :: IntMap a -> (a, Maybe (FResult pred v)) -> [Key]
get_dangling_function_pointers IntMap a
l0 (a
_,Maybe (FResult pred v)
Nothing) = []
  get_dangling_function_pointers IntMap a
l0 (a
_,Just FResult pred v
r)  = (VerificationCondition v -> [Key])
-> [VerificationCondition v] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IntMap a -> VerificationCondition v -> [Key]
forall {a} {v}. IntMap a -> VerificationCondition v -> [Key]
mkDanglingFunctionPointers IntMap a
l0) ([VerificationCondition v] -> [Key])
-> [VerificationCondition v] -> [Key]
forall a b. (a -> b) -> a -> b
$ Set (VerificationCondition v) -> [VerificationCondition v]
forall a. Set a -> [a]
S.toList (Set (VerificationCondition v) -> [VerificationCondition v])
-> Set (VerificationCondition v) -> [VerificationCondition v]
forall a b. (a -> b) -> a -> b
$ FResult pred v -> Set (VerificationCondition v)
forall pred v. FResult pred v -> Set (VerificationCondition v)
result_vcs FResult pred v
r

  mkDanglingFunctionPointers :: IntMap a -> VerificationCondition v -> [Key]
mkDanglingFunctionPointers IntMap a
l0 (FunctionPointers Word64
a IntSet
ptrs) = (Key -> [Key]) -> [Key] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IntMap a -> Key -> [Key]
forall {a}. IntMap a -> Key -> [Key]
isDangling IntMap a
l0) ([Key] -> [Key]) -> [Key] -> [Key]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
IS.toList IntSet
ptrs

  isDangling :: IntMap a -> Key -> [Key]
isDangling IntMap a
l0 Key
ptr = 
    case Key -> IntMap a -> Maybe a
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
ptr IntMap a
l0 of
      Maybe a
Nothing -> [Key
ptr] 
      Just a
_  -> []


exploreDanglingRelocations :: WithAbstractPredicates bin pred finit v => WithLifting bin pred finit v ()
exploreDanglingRelocations :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
exploreDanglingRelocations = do
  (bin
bin,Config
_)        <- StateT (L0 pred finit v) (ReaderT (bin, Config) IO) (bin, Config)
forall r (m :: * -> *). MonadReader r m => m r
ask
  [Relocation]
relocs <- (Relocation
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [Relocation]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Relocation]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Relocation
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall {a} {pred} {finit} {v}.
BinaryClass a =>
Relocation
-> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool
is_dangling ([Relocation]
 -> StateT
      (L0 pred finit v) (ReaderT (bin, Config) IO) [Relocation])
-> [Relocation]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Relocation]
forall a b. (a -> b) -> a -> b
$ Set Relocation -> [Relocation]
forall a. Set a -> [a]
S.toList (Set Relocation -> [Relocation]) -> Set Relocation -> [Relocation]
forall a b. (a -> b) -> a -> b
$ bin -> Set Relocation
forall a. BinaryClass a => a -> Set Relocation
binary_get_relocations bin
bin
  case [Relocation]
relocs of
    [] -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
finishExploration
    [Relocation]
_  -> do
      IO () -> WithLifting bin pred finit v ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> WithLifting bin pred finit v ())
-> IO () -> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Dangling relocations found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Relocation] -> String
forall a. Show a => a -> String
show [Relocation]
relocs
      let fptrs :: [Key]
fptrs = (Relocation -> Key) -> [Relocation] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Relocation -> Key
forall {b}. Num b => Relocation -> b
get_fptr [Relocation]
relocs

      let entries' :: Graph
entries' = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Key, IntSet)] -> IntMap IntSet
forall a. [(Key, a)] -> IntMap a
IM.fromList ([Key] -> [IntSet] -> [(Key, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key]
fptrs ([IntSet] -> [(Key, IntSet)]) -> [IntSet] -> [(Key, IntSet)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [IntSet]
forall a. a -> [a]
repeat IntSet
IS.empty)
      Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static
      let finit :: finit
finit = Lifting bin pred finit v -> finit
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> finit
new_finit Lifting bin pred finit v
static
      (Key -> WithLifting bin pred finit v ())
-> [Key] -> WithLifting bin pred finit v ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Key
a -> (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> WithLifting bin pred finit v ())
-> (L0 pred finit v -> L0 pred finit v)
-> WithLifting bin pred finit v ()
forall a b. (a -> b) -> a -> b
$ Key -> finit -> L0 pred finit v -> L0 pred finit v
forall {finit} {pred} {v}.
Key -> finit -> L0 pred finit v -> L0 pred finit v
l0_insert_new_entry Key
a finit
finit) [Key]
fptrs
      Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
forall a. IntMap a
IM.empty
 where
  get_fptr :: Relocation -> b
get_fptr (Relocation Word64
_ Word64
a1) = Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1
  is_dangling :: Relocation
-> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool
is_dangling (Relocation Word64
a0 Word64
a1) = do
    (a
bin,Config
_)        <- StateT (L0 pred finit v) (ReaderT (a, Config) IO) (a, Config)
forall r (m :: * -> *). MonadReader r m => m r
ask
    let valid_entry :: Bool
valid_entry = a -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
address_has_instruction a
bin Word64
a1 
    Bool
has_been_done  <- IntMap IntSet
-> Word64 -> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool
forall bin pred finit v.
IntMap IntSet -> Word64 -> WithLifting bin pred finit v Bool
entry_has_been_done IntMap IntSet
forall a. IntMap a
IM.empty Word64
a1 
    -- TODO a0 within data section?
    Bool -> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool
forall a. a -> StateT (L0 pred finit v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool)
-> Bool -> StateT (L0 pred finit v) (ReaderT (a, Config) IO) Bool
forall a b. (a -> b) -> a -> b
$ Bool
valid_entry Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
has_been_done



exploreFunctionEntry :: WithAbstractPredicates bin pred finit v => Graph -> Recursions -> Word64 ->  WithLifting bin pred finit v ()
exploreFunctionEntry :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> Word64 -> WithLifting bin pred finit v ()
exploreFunctionEntry Graph
entries IntMap IntSet
recursions Word64
entry = do
  (bin
bin,Config
_)        <- StateT (L0 pred finit v) (ReaderT (bin, Config) IO) (bin, Config)
forall r (m :: * -> *). MonadReader r m => m r
ask
  let valid_entry :: Bool
valid_entry = bin -> Word64 -> Bool
forall bin. BinaryClass bin => bin -> Word64 -> Bool
address_has_instruction bin
bin Word64
entry
  Bool
has_been_done  <- IntMap IntSet -> Word64 -> WithLifting bin pred finit v Bool
forall bin pred finit v.
IntMap IntSet -> Word64 -> WithLifting bin pred finit v Bool
entry_has_been_done IntMap IntSet
recursions Word64
entry
  Bool -> Bool -> WithLifting bin pred finit v ()
forall {bin} {pred} {finit} {v}.
WithAbstractPredicates bin pred finit v =>
Bool
-> Bool -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
explore Bool
has_been_done Bool
valid_entry 
 where 
  explore :: Bool
-> Bool -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
explore Bool
_ Bool
False = do
    -- Entry is not within a text section of the binary, delete it and continue
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n\nEntry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ignored."
    (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
forall {a} {pred} {v} {finit}.
Integral a =>
a -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
l0_adjust_result Word64
entry (FResult pred v -> Maybe (FResult pred v)
forall a. a -> Maybe a
Just FResult pred v
forall {pred} {v}. FResult pred v
empty_result) 

    let entries' :: Graph
entries' = Graph -> Key -> Graph
graph_delete Graph
entries (Key -> Graph) -> Key -> Graph
forall a b. (a -> b) -> a -> b
$ Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry
    Graph
-> IntMap IntSet
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
recursions    
  explore Bool
True Bool
_  = do
    -- Entry is already done, delete it and continue
    let entries' :: Graph
entries' = Graph -> Key -> Graph
graph_delete Graph
entries (Key -> Graph) -> Key -> Graph
forall a b. (a -> b) -> a -> b
$ Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry
    Graph
-> IntMap IntSet
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
recursions
  explore Bool
_ Bool
_     = do
    -- Entry is to be explored
    L0 pred finit v
l0 <- StateT
  (L0 pred finit v) (ReaderT (bin, Config) IO) (L0 pred finit v)
forall s (m :: * -> *). MonadState s m => m s
get
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n\nEntry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (#entries explored/to be explored: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (IntMap (finit, Maybe (FResult pred v)) -> Key
forall a. IntMap a -> Key
IM.size (IntMap (finit, Maybe (FResult pred v)) -> Key)
-> IntMap (finit, Maybe (FResult pred v)) -> Key
forall a b. (a -> b) -> a -> b
$ L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit v
l0) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (IntSet -> Key
IS.size (IntSet -> Key) -> IntSet -> Key
forall a b. (a -> b) -> a -> b
$ Graph -> IntSet
forall g. IntGraph g => g -> IntSet
intgraph_V Graph
entries) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    AnalysisResult pred finit v
result <- Word64
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Word64
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
analyze_entry Word64
entry 
    case AnalysisResult pred finit v
result of
      FoundNewCalls IntMap finit
m -> do
        -- Found calls to unexplored functions, or functions called with a new FInit
        let new_calls :: [(Key, finit)]
new_calls = IntMap finit -> [(Key, finit)]
forall a. IntMap a -> [(Key, a)]
IM.toList IntMap finit
m
        let entries' :: Graph
entries' = ((Key, finit) -> Graph -> Graph)
-> Graph -> [(Key, finit)] -> Graph
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Key
trgt,finit
finit) Graph
entries -> Graph -> Key -> IntSet -> Graph
graph_add_edges Graph
entries (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry) (Key -> IntSet
IS.singleton Key
trgt)) Graph
entries [(Key, finit)]
new_calls
        ((Key, finit)
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> [(Key, finit)]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Key
trgt,finit
finit) -> (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ Key -> finit -> L0 pred finit v -> L0 pred finit v
forall {finit} {pred} {v}.
Key -> finit -> L0 pred finit v -> L0 pred finit v
l0_insert_new_entry Key
trgt finit
finit) [(Key, finit)]
new_calls
        Graph
-> IntMap IntSet
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
recursions
      AnalyzedWithResult FResult pred v
result -> do
        -- Finished analysis of the function entry
        (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v)
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> (L0 pred finit v -> L0 pred finit v)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
forall {a} {pred} {v} {finit}.
Integral a =>
a -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
l0_adjust_result Word64
entry (FResult pred v -> Maybe (FResult pred v)
forall a. a -> Maybe a
Just FResult pred v
result) 
        let entries' :: Graph
entries' = Graph -> Key -> Graph
graph_delete Graph
entries (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry)
        IntMap IntSet
recursions' <- Word64
-> FResult pred v
-> IntMap IntSet
-> WithLifting bin pred finit v (IntMap IntSet)
forall pred v bin finit.
Word64
-> FResult pred v
-> IntMap IntSet
-> WithLifting bin pred finit v (IntMap IntSet)
mark_mutual_recursive_calls Word64
entry FResult pred v
result IntMap IntSet
recursions
        FResult pred v
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall {bin} {pred} {finit} {v} {pred} {v}.
(WithAbstractPredicates bin pred finit v, Show pred, Show v) =>
FResult pred v
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
report_result FResult pred v
result
        Graph
-> IntMap IntSet
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Graph -> IntMap IntSet -> WithLifting bin pred finit v ()
exploreFunctionEntries Graph
entries' IntMap IntSet
recursions'
       
  report_result :: FResult pred v
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
report_result FResult pred v
result = do
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" lifted."
    Just (finit
finit,Maybe (FResult pred v)
_) <- (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
 -> StateT
      (L0 pred finit v)
      (ReaderT (bin, Config) IO)
      (Maybe (finit, Maybe (FResult pred v))))
-> (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry
    Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static
    let empty_finit :: finit
empty_finit = Lifting bin pred finit v -> finit
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> finit
new_finit Lifting bin pred finit v
static
    Bool
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (finit
finit finit -> finit -> Bool
forall a. Eq a => a -> a -> Bool
/= finit
empty_finit) (StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ do
      IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Function precondition:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lifting bin pred finit v -> finit -> String
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> finit -> String
pp_finit Lifting bin pred finit v
static finit
finit
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Function postcondition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Postcondition pred -> String
forall a. Show a => a -> String
show (Postcondition pred -> String) -> Postcondition pred -> String
forall a b. (a -> b) -> a -> b
$ FResult pred v -> Postcondition pred
forall pred v. FResult pred v -> Postcondition pred
result_post FResult pred v
result)
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (VerificationCondition v -> String)
-> [VerificationCondition v] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition v -> String
forall a. Show a => a -> String
show ([VerificationCondition v] -> [String])
-> [VerificationCondition v] -> [String]
forall a b. (a -> b) -> a -> b
$ Set (VerificationCondition v) -> [VerificationCondition v]
forall a. Set a -> [a]
S.toList (Set (VerificationCondition v) -> [VerificationCondition v])
-> Set (VerificationCondition v) -> [VerificationCondition v]
forall a b. (a -> b) -> a -> b
$ FResult pred v -> Set (VerificationCondition v)
forall pred v. FResult pred v -> Set (VerificationCondition v)
result_vcs FResult pred v
result)

entry_has_been_done :: Recursions -> Word64 -> WithLifting bin pred finit v Bool
entry_has_been_done :: forall bin pred finit v.
IntMap IntSet -> Word64 -> WithLifting bin pred finit v Bool
entry_has_been_done IntMap IntSet
recursions Word64
entry = do
  Maybe (finit, Maybe (FResult pred v))
result <- (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
 -> StateT
      (L0 pred finit v)
      (ReaderT (bin, Config) IO)
      (Maybe (finit, Maybe (FResult pred v))))
-> (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry
  case Maybe (finit, Maybe (FResult pred v))
result of
    Just (finit
_,Just FResult pred v
_) -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> WithLifting bin pred finit v Bool)
-> Bool -> WithLifting bin pred finit v Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry Key -> IntMap IntSet -> Bool
forall a. Key -> IntMap a -> Bool
`IM.member` IntMap IntSet
recursions
    Maybe (finit, Maybe (FResult pred v))
_               -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> WithLifting bin pred finit v Bool)
-> Bool -> WithLifting bin pred finit v Bool
forall a b. (a -> b) -> a -> b
$ Bool
False



reconsider_mutual_recursive_call :: Recursions -> WithLifting bin pred finit v (Maybe (Int,IS.IntSet))
reconsider_mutual_recursive_call :: forall bin pred finit v.
IntMap IntSet -> WithLifting bin pred finit v (Maybe (Key, IntSet))
reconsider_mutual_recursive_call IntMap IntSet
recursions = ((Key, IntSet)
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [(Key, IntSet)]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) (Maybe (Key, IntSet))
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (Key, IntSet)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall {a} {pred} {finit} {v} {bin}.
(a, IntSet)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
to_be_reconsidered ([(Key, IntSet)]
 -> StateT
      (L0 pred finit v) (ReaderT (bin, Config) IO) (Maybe (Key, IntSet)))
-> [(Key, IntSet)]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) (Maybe (Key, IntSet))
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Key, IntSet)]
forall a. IntMap a -> [(Key, a)]
IM.toList IntMap IntSet
recursions
 where
  to_be_reconsidered :: (a, IntSet)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
to_be_reconsidered (a
entry,IntSet
trgts) = (Word64
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM (IntMap IntSet
-> Word64
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall bin pred finit v.
IntMap IntSet -> Word64 -> WithLifting bin pred finit v Bool
entry_has_been_done IntMap IntSet
recursions) ([Word64]
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall a b. (a -> b) -> a -> b
$ (Key -> Word64) -> [Key] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Key] -> [Word64]) -> [Key] -> [Word64]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
IS.toList IntSet
trgts


-- If an entry has an FInit but no FResult, this means that it has been visited but not analyzed yet.
-- Calls to those functions indicate recursion. It is stored that the current entry did a recursive call to those functions,
-- so that it can be reconsidered later.
mark_mutual_recursive_calls :: Word64 -> FResult pred v -> Recursions -> WithLifting bin pred finit v Recursions
mark_mutual_recursive_calls :: forall pred v bin finit.
Word64
-> FResult pred v
-> IntMap IntSet
-> WithLifting bin pred finit v (IntMap IntSet)
mark_mutual_recursive_calls Word64
entry FResult pred v
result IntMap IntSet
recursions = do
  IntSet
new_recursions <- [Key] -> IntSet
IS.fromList ([Key] -> IntSet) -> ([Word64] -> [Key]) -> [Word64] -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Key) -> [Word64] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Word64] -> IntSet)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Word64
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Word64 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall bin pred finit v.
Word64 -> WithLifting bin pred finit v Bool
is_recursive ([Word64]
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64])
-> [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall a b. (a -> b) -> a -> b
$ Set Word64 -> [Word64]
forall a. Set a -> [a]
S.toList (Set Word64 -> [Word64]) -> Set Word64 -> [Word64]
forall a b. (a -> b) -> a -> b
$ FResult pred v -> Set Word64
forall pred v. FResult pred v -> Set Word64
result_calls FResult pred v
result)
  if IntSet -> Bool
IS.null IntSet
new_recursions then
    IntMap IntSet -> WithLifting bin pred finit v (IntMap IntSet)
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap IntSet
recursions
  else do
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is part of mutual recursion and treated entries " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IntSet -> String
showHex_set IntSet
new_recursions String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as external. It will be reconsidered after those entries have been done."
    IntMap IntSet -> WithLifting bin pred finit v (IntMap IntSet)
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap IntSet -> WithLifting bin pred finit v (IntMap IntSet))
-> IntMap IntSet -> WithLifting bin pred finit v (IntMap IntSet)
forall a b. (a -> b) -> a -> b
$ (IntSet -> IntSet -> IntSet)
-> Key -> IntSet -> IntMap IntSet -> IntMap IntSet
forall a. (a -> a -> a) -> Key -> a -> IntMap a -> IntMap a
IM.insertWith IntSet -> IntSet -> IntSet
IS.union (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry) IntSet
new_recursions IntMap IntSet
recursions
 where
  is_recursive :: Word64 -> WithLifting bin pred finit v Bool
  is_recursive :: forall bin pred finit v.
Word64 -> WithLifting bin pred finit v Bool
is_recursive Word64
entry = do
    Maybe (finit, Maybe (FResult pred v))
result <- (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
 -> StateT
      (L0 pred finit v)
      (ReaderT (bin, Config) IO)
      (Maybe (finit, Maybe (FResult pred v))))
-> (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry
    case Maybe (finit, Maybe (FResult pred v))
result of
      Just (finit
_,Maybe (FResult pred v)
Nothing) -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> WithLifting bin pred finit v Bool)
-> Bool -> WithLifting bin pred finit v Bool
forall a b. (a -> b) -> a -> b
$ Bool
True
      Maybe (finit, Maybe (FResult pred v))
_                -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> WithLifting bin pred finit v Bool)
-> Bool -> WithLifting bin pred finit v Bool
forall a b. (a -> b) -> a -> b
$ Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
entry Key -> IntMap IntSet -> Bool
forall a. Key -> IntMap a -> Bool
`IM.member` IntMap IntSet
recursions -- False



mk_static :: WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static :: forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static = do
  L0 pred finit v
l <- StateT
  (L0 pred finit v) (ReaderT (bin, Config) IO) (L0 pred finit v)
forall s (m :: * -> *). MonadState s m => m s
get
  (bin
bin,Config
config) <- StateT (L0 pred finit v) (ReaderT (bin, Config) IO) (bin, Config)
forall r (m :: * -> *). MonadReader r m => m r
ask
  Lifting bin pred finit v
-> WithLifting bin pred finit v (Lifting bin pred finit v)
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (bin
bin,Config
config,L0 pred finit v
l)

analyze_entry :: WithAbstractPredicates bin pred finit v => Word64 -> WithLifting bin pred finit v (AnalysisResult pred finit v)
analyze_entry :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Word64
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
analyze_entry Word64
entry = do
  (Just (finit
finit,Maybe (FResult pred v)
_)) <- (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
 -> StateT
      (L0 pred finit v)
      (ReaderT (bin, Config) IO)
      (Maybe (finit, Maybe (FResult pred v))))
-> (L0 pred finit v -> Maybe (finit, Maybe (FResult pred v)))
-> StateT
     (L0 pred finit v)
     (ReaderT (bin, Config) IO)
     (Maybe (finit, Maybe (FResult pred v)))
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
entry

  Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static 
  IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": starting CFG generation."
  let !cfg :: CFG
cfg = Lifting bin pred finit v -> Word64 -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> Word64 -> CFG
generate_cfg Lifting bin pred finit v
static Word64
entry
  IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": CFG generation done: #basic blocks = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (IntMap [Instruction] -> Key
forall a. IntMap a -> Key
IM.size (IntMap [Instruction] -> Key) -> IntMap [Instruction] -> Key
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", #instructions = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (CFG -> Key
num_of_instructions CFG
cfg)

  IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": starting invariant generation."
  let !(IntMap pred
invs,VCS v
vcs)  = LiftingEntry bin pred finit v
-> CFG -> finit -> (IntMap pred, VCS v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> finit -> (IntMap pred, VCS v)
generate_invariants (Word64 -> Lifting bin pred finit v -> LiftingEntry bin pred finit v
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry Lifting bin pred finit v
static) CFG
cfg finit
finit

  [(Key, finit)]
new_calls <- (Lifting bin pred finit v -> [(Key, finit)] -> [(Key, finit)]
forall {bin} {pred} {b} {v} {a}.
(WithAbstractPredicates bin pred b v, Integral a) =>
(bin, Config, L0 pred b v) -> [(a, b)] -> [(a, b)]
join_duplicate_new_calls Lifting bin pred finit v
static ([(Key, finit)] -> [(Key, finit)])
-> ([Maybe (Key, finit)] -> [(Key, finit)])
-> [Maybe (Key, finit)]
-> [(Key, finit)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Key, finit)] -> [(Key, finit)]
forall a. [Maybe a] -> [a]
catMaybes) ([Maybe (Key, finit)] -> [(Key, finit)])
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [(Key, finit)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Key, [Instruction])
 -> StateT
      (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)])
-> [(Key, [Instruction])]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (IntMap pred
-> (Key, [Instruction])
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)]
forall {a} {bin} {pred} {finit} {v}.
(Num a, WithAbstractPredicates bin pred finit v) =>
IntMap pred
-> (Key, [Instruction])
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (a, finit)]
get_new_calls IntMap pred
invs) ([(Key, [Instruction])]
 -> StateT
      (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)])
-> [(Key, [Instruction])]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (Key, finit)]
forall a b. (a -> b) -> a -> b
$ IntMap [Instruction] -> [(Key, [Instruction])]
forall a. IntMap a -> [(Key, a)]
IM.assocs (IntMap [Instruction] -> [(Key, [Instruction])])
-> IntMap [Instruction] -> [(Key, [Instruction])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg)

  if [(Key, finit)]
new_calls [(Key, finit)] -> [(Key, finit)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then do
    IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Adding new internal functions at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Key] -> String
forall {a}. Integral a => [a] -> String
showHex_list (((Key, finit) -> Key) -> [(Key, finit)] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map (Key, finit) -> Key
forall a b. (a, b) -> a
fst [(Key, finit)]
new_calls) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to entries to be explored."
    AnalysisResult pred finit v
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AnalysisResult pred finit v
 -> WithLifting bin pred finit v (AnalysisResult pred finit v))
-> AnalysisResult pred finit v
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall a b. (a -> b) -> a -> b
$ IntMap finit -> AnalysisResult pred finit v
forall pred finit v. IntMap finit -> AnalysisResult pred finit v
FoundNewCalls (IntMap finit -> AnalysisResult pred finit v)
-> IntMap finit -> AnalysisResult pred finit v
forall a b. (a -> b) -> a -> b
$ [(Key, finit)] -> IntMap finit
forall a. [(Key, a)] -> IntMap a
IM.fromList [(Key, finit)]
new_calls
  else do
    [(Key, [Instruction])]
to_be_resolved_blocks <- ((Key, [Instruction])
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [(Key, [Instruction])]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [(Key, [Instruction])]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Key, [Instruction])
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
(Key, [Instruction]) -> WithLifting bin pred finit v Bool
is_to_be_resolved_block) ([(Key, [Instruction])]
 -> StateT
      (L0 pred finit v)
      (ReaderT (bin, Config) IO)
      [(Key, [Instruction])])
-> [(Key, [Instruction])]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [(Key, [Instruction])]
forall a b. (a -> b) -> a -> b
$ IntMap [Instruction] -> [(Key, [Instruction])]
forall a. IntMap a -> [(Key, a)]
IM.assocs (IntMap [Instruction] -> [(Key, [Instruction])])
-> IntMap [Instruction] -> [(Key, [Instruction])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg
    [Bool]
is_newly_resolved <- ((Key, [Instruction])
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool)
-> [(Key, [Instruction])]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (IntMap pred
-> (Key, [Instruction])
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) Bool
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
IntMap pred
-> (Key, [Instruction]) -> WithLifting bin pred finit v Bool
try_resolve_indirection IntMap pred
invs) [(Key, [Instruction])]
to_be_resolved_blocks
    if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
is_newly_resolved then do
      IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Continuing to next round as there are newly resolved indirections."
      Word64
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Word64
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
analyze_entry Word64
entry 
    else do
      IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall {a}. Integral a => a -> String
showHex Word64
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Terminating as no new indirections are resolved."

      -- liftIO $ putStrLn $ "Invariants:\n" ++ intercalate "\n" (map show $ IM.assocs invs)

      let posts :: Postcondition pred
posts = LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> Postcondition pred
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> Postcondition pred
invs_to_post (Word64 -> Lifting bin pred finit v -> LiftingEntry bin pred finit v
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry Lifting bin pred finit v
static) CFG
cfg IntMap pred
invs
      let pars :: IntMap (PointerAnalysisResult v)
pars  = LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> IntMap (PointerAnalysisResult v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> IntMap (PointerAnalysisResult v)
invs_to_PA (Word64 -> Lifting bin pred finit v -> LiftingEntry bin pred finit v
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry Lifting bin pred finit v
static) CFG
cfg IntMap pred
invs
      Set Word64
calls <- [Word64] -> Set Word64
forall a. Ord a => [a] -> Set a
S.fromList ([Word64] -> Set Word64)
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) (Set Word64)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Instruction
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64])
-> [Instruction]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM Instruction
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall {bin} {pred} {finit} {v}.
BinaryClass bin =>
Instruction
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
get_internal_calls ([Instruction]
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64])
-> [Instruction]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall a b. (a -> b) -> a -> b
$ [[Instruction]] -> [Instruction]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Instruction]] -> [Instruction])
-> [[Instruction]] -> [Instruction]
forall a b. (a -> b) -> a -> b
$ IntMap [Instruction] -> [[Instruction]]
forall a. IntMap a -> [a]
IM.elems (IntMap [Instruction] -> [[Instruction]])
-> IntMap [Instruction] -> [[Instruction]]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg)
      AnalysisResult pred finit v
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AnalysisResult pred finit v
 -> WithLifting bin pred finit v (AnalysisResult pred finit v))
-> AnalysisResult pred finit v
-> WithLifting bin pred finit v (AnalysisResult pred finit v)
forall a b. (a -> b) -> a -> b
$ FResult pred v -> AnalysisResult pred finit v
forall pred finit v. FResult pred v -> AnalysisResult pred finit v
AnalyzedWithResult (FResult pred v -> AnalysisResult pred finit v)
-> FResult pred v -> AnalysisResult pred finit v
forall a b. (a -> b) -> a -> b
$ CFG
-> Postcondition pred
-> Set Word64
-> VCS v
-> IntMap (PointerAnalysisResult v)
-> FResult pred v
forall pred v.
CFG
-> Postcondition pred
-> Set Word64
-> Set (VerificationCondition v)
-> IntMap (PointerAnalysisResult v)
-> FResult pred v
FResult CFG
cfg Postcondition pred
posts Set Word64
calls VCS v
vcs IntMap (PointerAnalysisResult v)
pars
 where
  join_duplicate_new_calls :: (bin, Config, L0 pred b v) -> [(a, b)] -> [(a, b)]
join_duplicate_new_calls (bin, Config, L0 pred b v)
static [] = []
  join_duplicate_new_calls (bin, Config, L0 pred b v)
static ((a
a,b
finit):[(a, b)]
new_calls) =
    let ([(a, b)]
same,[(a, b)]
rest) = ((a, b) -> Bool) -> [(a, b)] -> ([(a, b)], [(a, b)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(a
a',b
_) -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a') [(a, b)]
new_calls
        finit' :: b
finit'      = (b -> b -> b) -> [b] -> b
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (LiftingEntry bin pred b v -> b -> b -> b
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> finit -> finit -> finit
join_finits (LiftingEntry bin pred b v -> b -> b -> b)
-> LiftingEntry bin pred b v -> b -> b -> b
forall a b. (a -> b) -> a -> b
$ Word64 -> (bin, Config, L0 pred b v) -> LiftingEntry bin pred b v
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (bin, Config, L0 pred b v)
static) (b
finitb -> [b] -> [b]
forall a. a -> [a] -> [a]
:((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
same) in
      (a
a,b
finit') (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: (bin, Config, L0 pred b v) -> [(a, b)] -> [(a, b)]
join_duplicate_new_calls (bin, Config, L0 pred b v)
static [(a, b)]
rest

  get_new_calls :: IntMap pred
-> (Key, [Instruction])
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (a, finit)]
get_new_calls IntMap pred
invs (Key
blockID,[Instruction]
instrs)
    -- Assumes calls are always last intruction in block (TODO jumps that are actually calls)
    | Opcode -> Bool
isCall (Instruction -> Opcode
inOperation (Instruction -> Opcode) -> Instruction -> Opcode
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) = do
      Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static
      let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
static (Instruction -> [ResolvedJumpTarget])
-> Instruction -> [ResolvedJumpTarget]
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs
      (ResolvedJumpTarget
 -> StateT
      (L0 pred finit v) (ReaderT (bin, Config) IO) (Maybe (a, finit)))
-> [ResolvedJumpTarget]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (a, finit)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (IntMap pred
-> Key
-> [Instruction]
-> ResolvedJumpTarget
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) (Maybe (a, finit))
forall {a} {a} {pred} {a} {v}.
(Num a, WithAbstractPredicates a pred a v) =>
IntMap pred
-> Key
-> [Instruction]
-> ResolvedJumpTarget
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
get_new_calls_from_trgt IntMap pred
invs Key
blockID [Instruction]
instrs) [ResolvedJumpTarget]
trgts
    | Bool
otherwise = [Maybe (a, finit)]
-> StateT
     (L0 pred finit v) (ReaderT (bin, Config) IO) [Maybe (a, finit)]
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Maybe (a, finit)
forall a. Maybe a
Nothing]

  get_new_calls_from_trgt :: IntMap pred
-> Key
-> [Instruction]
-> ResolvedJumpTarget
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
get_new_calls_from_trgt IntMap pred
invs Key
blockID [Instruction]
instrs (ImmediateAddress Word64
a') = do
    Maybe (a, Maybe (FResult pred v))
result <- (L0 pred a v -> Maybe (a, Maybe (FResult pred v)))
-> StateT
     (L0 pred a v)
     (ReaderT (a, Config) IO)
     (Maybe (a, Maybe (FResult pred v)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred a v -> Maybe (a, Maybe (FResult pred v)))
 -> StateT
      (L0 pred a v)
      (ReaderT (a, Config) IO)
      (Maybe (a, Maybe (FResult pred v))))
-> (L0 pred a v -> Maybe (a, Maybe (FResult pred v)))
-> StateT
     (L0 pred a v)
     (ReaderT (a, Config) IO)
     (Maybe (a, Maybe (FResult pred v)))
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred a v -> Maybe (a, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
a'
    case Maybe (a, Maybe (FResult pred v))
result of
      Maybe (a, Maybe (FResult pred v))
Nothing             -> do -- Unvisited
                               (a, Config, L0 pred a v, Word64)
static <- Word64
-> (a, Config, L0 pred a v) -> (a, Config, L0 pred a v, Word64)
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry ((a, Config, L0 pred a v) -> (a, Config, L0 pred a v, Word64))
-> StateT
     (L0 pred a v) (ReaderT (a, Config) IO) (a, Config, L0 pred a v)
-> StateT
     (L0 pred a v)
     (ReaderT (a, Config) IO)
     (a, Config, L0 pred a v, Word64)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
  (L0 pred a v) (ReaderT (a, Config) IO) (a, Config, L0 pred a v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static
                               let (pred
post,VCS v
_) = (a, Config, L0 pred a v, Word64)
-> Key -> [Instruction] -> IntMap pred -> (pred, VCS v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Key -> [Instruction] -> IntMap pred -> (pred, VCS v)
get_postcondition_for_block (a, Config, L0 pred a v, Word64)
static Key
blockID ([Instruction] -> [Instruction]
forall a. HasCallStack => [a] -> [a]
init [Instruction]
instrs) IntMap pred
invs
                               let new_finit :: a
new_finit = (a, Config, L0 pred a v, Word64) -> pred -> a
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> finit
pred_to_finit (a, Config, L0 pred a v, Word64)
static pred
post
                               Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a. a -> StateT (L0 pred a v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, a)
 -> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a)))
-> Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a b. (a -> b) -> a -> b
$ (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a',a
new_finit)
      Just (a
_,Maybe (FResult pred v)
Nothing)    -> do -- Recursive unanalyzed call
                               Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a. a -> StateT (L0 pred a v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, a)
forall a. Maybe a
Nothing
      Just (a
finit,Just FResult pred v
r) -> do -- Already analyzed call
                               (a, Config, L0 pred a v, Word64)
static <- Word64
-> (a, Config, L0 pred a v) -> (a, Config, L0 pred a v, Word64)
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry ((a, Config, L0 pred a v) -> (a, Config, L0 pred a v, Word64))
-> StateT
     (L0 pred a v) (ReaderT (a, Config) IO) (a, Config, L0 pred a v)
-> StateT
     (L0 pred a v)
     (ReaderT (a, Config) IO)
     (a, Config, L0 pred a v, Word64)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
  (L0 pred a v) (ReaderT (a, Config) IO) (a, Config, L0 pred a v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static 
                               let (pred
post,VCS v
_) = (a, Config, L0 pred a v, Word64)
-> Key -> [Instruction] -> IntMap pred -> (pred, VCS v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Key -> [Instruction] -> IntMap pred -> (pred, VCS v)
get_postcondition_for_block (a, Config, L0 pred a v, Word64)
static Key
blockID ([Instruction] -> [Instruction]
forall a. HasCallStack => [a] -> [a]
init [Instruction]
instrs) IntMap pred
invs
                               let new_finit :: a
new_finit = (a, Config, L0 pred a v, Word64) -> pred -> a
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> finit
pred_to_finit (a, Config, L0 pred a v, Word64)
static pred
post
                               let join :: a
join = (a, Config, L0 pred a v, Word64) -> a -> a -> a
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> finit -> finit -> finit
join_finits (a, Config, L0 pred a v, Word64)
static a
new_finit a
finit
                               if a
finit a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
join then do
                                  Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a. a -> StateT (L0 pred a v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, a)
 -> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a)))
-> Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a b. (a -> b) -> a -> b
$ (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a',a
join)
                               else
                                  Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a. a -> StateT (L0 pred a v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, a)
forall a. Maybe a
Nothing
  get_new_calls_from_trgt IntMap pred
_ Key
_ [Instruction]
_ ResolvedJumpTarget
_ = Maybe (a, a)
-> StateT (L0 pred a v) (ReaderT (a, Config) IO) (Maybe (a, a))
forall a. a -> StateT (L0 pred a v) (ReaderT (a, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, a)
forall a. Maybe a
Nothing


  get_internal_calls :: Instruction
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
get_internal_calls Instruction
i
    | Opcode -> Bool
isCall (Instruction -> Opcode
inOperation Instruction
i) = do
      Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static 
      let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
static Instruction
i
      [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Word64]
 -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64])
-> [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> [Word64])
-> [ResolvedJumpTarget] -> [Word64]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Word64]
get_internal_call_from_trgt [ResolvedJumpTarget]
trgts
    -- TODO jump
    | Bool
otherwise = [Word64]
-> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) [Word64]
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

  get_internal_call_from_trgt :: ResolvedJumpTarget -> [Word64]
get_internal_call_from_trgt (ImmediateAddress Word64
a') = [Word64
a']
  get_internal_call_from_trgt ResolvedJumpTarget
_ = []


  is_to_be_resolved_block :: WithAbstractPredicates bin pred finit v => (Int,[Instruction]) -> WithLifting bin pred finit v Bool
  is_to_be_resolved_block :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
(Key, [Instruction]) -> WithLifting bin pred finit v Bool
is_to_be_resolved_block (Key
blockID,[Instruction]
instrs)
    | Opcode -> Bool
isJump (Instruction -> Opcode
inOperation (Instruction -> Opcode) -> Instruction -> Opcode
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) Bool -> Bool -> Bool
|| Opcode -> Bool
isCall (Instruction -> Opcode
inOperation (Instruction -> Opcode) -> Instruction -> Opcode
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) = Instruction -> WithLifting bin pred finit v Bool
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Instruction -> WithLifting bin pred finit v Bool
is_to_be_resolved_indirection ([Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs)
    | Bool
otherwise = Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  is_to_be_resolved_indirection :: WithAbstractPredicates bin pred finit v => Instruction -> WithLifting bin pred finit v Bool
  is_to_be_resolved_indirection :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Instruction -> WithLifting bin pred finit v Bool
is_to_be_resolved_indirection Instruction
i = do
   L0 pred finit v
l0 <- StateT
  (L0 pred finit v) (ReaderT (bin, Config) IO) (L0 pred finit v)
forall s (m :: * -> *). MonadState s m => m s
get
   (bin
bin,Config
config) <- StateT (L0 pred finit v) (ReaderT (bin, Config) IO) (bin, Config)
forall r (m :: * -> *). MonadReader r m => m r
ask
   case bin -> Instruction -> ResolvedJumpTarget
forall bin.
BinaryClass bin =>
bin -> Instruction -> ResolvedJumpTarget
jump_target_for_instruction bin
bin Instruction
i of
     ResolvedJumpTarget
Unresolved -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
     External String
"error" -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
     ResolvedJumpTarget
_ -> Bool -> WithLifting bin pred finit v Bool
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  try_resolve_indirection :: WithAbstractPredicates bin pred finit v => IM.IntMap pred -> (Int,[Instruction]) -> WithLifting bin pred finit v Bool
  try_resolve_indirection :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
IntMap pred
-> (Key, [Instruction]) -> WithLifting bin pred finit v Bool
try_resolve_indirection IntMap pred
invs (Key
blockID,[Instruction]
instrs) = do
    let pre :: pred
pre = Maybe pred -> pred
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe pred -> pred) -> Maybe pred -> pred
forall a b. (a -> b) -> a -> b
$ Key -> IntMap pred -> Maybe pred
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID IntMap pred
invs
    Lifting bin pred finit v
static <- WithLifting bin pred finit v (Lifting bin pred finit v)
forall bin pred finit v.
WithLifting bin pred finit v (Lifting bin pred finit v)
mk_static
    let inds :: Indirections
inds = LiftingEntry bin pred finit v
-> pred -> [Instruction] -> Indirections
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> pred -> [Instruction] -> Indirections
resolve_indirection (Word64 -> Lifting bin pred finit v -> LiftingEntry bin pred finit v
forall {d} {a} {b} {c}. d -> (a, b, c) -> (a, b, c, d)
withEntry Word64
entry Lifting bin pred finit v
static) pred
pre [Instruction]
instrs
    case Indirection
Indirection_Unresolved Indirection -> Indirections -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Indirections
inds of
      Bool
True -> do
        IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unresolved indirection: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Instruction -> String
forall a. Show a => a -> String
show ([Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs)
        IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ pred -> String
forall a. Show a => a -> String
show pred
pre
        Indirections -> Word64 -> WithLifting bin pred finit v Bool
forall {m :: * -> *} {a} {pred} {finit} {v}.
(MonadIO m, Integral a, MonadState (L0 pred finit v) m) =>
Indirections -> a -> m Bool
add_newly_resolved_indirection Indirections
inds (Instruction -> Word64
inAddress (Instruction -> Word64) -> Instruction -> Word64
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs)
      Bool
_ -> do
        IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Resolved indirection: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Instruction -> String
forall a. Show a => a -> String
show ([Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs)
        IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
IO a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ())
-> IO () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Indirection -> String) -> [Indirection] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Indirection -> String
forall a. Show a => a -> String
show ([Indirection] -> [String]) -> [Indirection] -> [String]
forall a b. (a -> b) -> a -> b
$ Indirections -> [Indirection]
forall a. Set a -> [a]
S.toList Indirections
inds
        Indirections -> Word64 -> WithLifting bin pred finit v Bool
forall {m :: * -> *} {a} {pred} {finit} {v}.
(MonadIO m, Integral a, MonadState (L0 pred finit v) m) =>
Indirections -> a -> m Bool
add_newly_resolved_indirection Indirections
inds (Instruction -> Word64
inAddress (Instruction -> Word64) -> Instruction -> Word64
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) 

  add_newly_resolved_indirection :: Indirections -> a -> m Bool
add_newly_resolved_indirection Indirections
inds a
a' = do
    Maybe Indirections
curr_inds <- (L0 pred finit v -> Maybe Indirections) -> m (Maybe Indirections)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((L0 pred finit v -> Maybe Indirections) -> m (Maybe Indirections))
-> (L0 pred finit v -> Maybe Indirections)
-> m (Maybe Indirections)
forall a b. (a -> b) -> a -> b
$ a -> L0 pred finit v -> Maybe Indirections
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe Indirections
l0_lookup_indirection a
a'
    case Maybe Indirections
curr_inds of
      Maybe Indirections
Nothing -> (L0 pred finit v -> L0 pred finit v) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (a -> Indirections -> L0 pred finit v -> L0 pred finit v
forall {a} {pred} {finit} {v}.
Integral a =>
a -> Indirections -> L0 pred finit v -> L0 pred finit v
l0_insert_indirection a
a' Indirections
inds) m () -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Just Indirections
inds' -> if Indirections
inds Indirections -> Indirections -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Indirections
inds' then 
                      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    else do
                      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Extending previous indirection resolving @ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Integral a => a -> String
showHex a
a' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Indirections -> String
forall a. Show a => a -> String
show Indirections
inds' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with new resolving: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Indirections -> String
forall a. Show a => a -> String
show Indirections
inds
                      (L0 pred finit v -> L0 pred finit v) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((L0 pred finit v -> L0 pred finit v) -> m ())
-> (L0 pred finit v -> L0 pred finit v) -> m ()
forall a b. (a -> b) -> a -> b
$ a -> Indirections -> L0 pred finit v -> L0 pred finit v
forall {a} {pred} {finit} {v}.
Integral a =>
a -> Indirections -> L0 pred finit v -> L0 pred finit v
l0_insert_indirection a
a' (Indirections -> Indirections -> Indirections
forall a. Ord a => Set a -> Set a -> Set a
S.union Indirections
inds Indirections
inds')
                      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True









finishExploration :: WithAbstractPredicates bin pred finit v => WithLifting bin pred finit v ()
finishExploration :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
WithLifting bin pred finit v ()
finishExploration = () -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) ()
forall a.
a -> StateT (L0 pred finit v) (ReaderT (bin, Config) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()