{-# LANGUAGE PartialTypeSignatures , FlexibleContexts, StrictData #-}


module Algorithm.L0_Lifting (
  lift_to_L0
 ) where




import Base
import Config

import Analysis.Context
import Analysis.FunctionNames
import Analysis.ControlFlow

import Generic.Binary
import Generic.SymbolicPropagation
import Generic.SymbolicConstituents
import Instantiation.SymbolicPropagation

import Data.JumpTarget
import Data.SymbolicExpression

import Parser.ParserIndirections

import OutputGeneration.Metrics
import OutputGeneration.JSON
import OutputGeneration.CallGraph

-- import Pass.ACode_Gen


import X86.Conventions
import X86.Register (Register(..))
import X86.Opcode
import X86.Instruction
import qualified Generic.Instruction as Instr
import Generic.Operand (GenericOperand(..))

import Numeric (readHex)
import Control.Monad.State.Strict
import Control.Monad (filterM)
import Control.Monad.Extra (whenM)
import qualified Data.Map as M
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set as S
import Data.Maybe (fromJust,catMaybes,mapMaybe)
import Data.List (intercalate,delete,isInfixOf,partition,nub)
import Data.Foldable
import qualified Data.Serialize as Cereal hiding (get,put)
import qualified Data.ByteString as BS (readFile,writeFile) 
import Data.IORef

import Debug.Trace
import System.IO
import System.Process (callCommand)
import System.Timeout (timeout)
import System.Directory (doesFileExist,createDirectoryIfMissing)
import System.Exit (die)
import Data.Functor.Identity

import System.IO.Unsafe (unsafePerformIO)










to_out_r :: String -> StateT Context IO ()
to_out_r = IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ())
-> (String -> IO ()) -> String -> StateT Context IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn
to_out :: String -> StateT Context IO ()
to_out   = StateT Context IO Bool
-> StateT Context IO () -> StateT Context IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Context -> Bool) -> StateT Context IO Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Bool
ctxt_verbose) (StateT Context IO () -> StateT Context IO ())
-> (String -> StateT Context IO ())
-> String
-> StateT Context IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> StateT Context IO ()
to_out_r
to_log :: String -> String -> m ()
to_log String
log String
s = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
appendFile String
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"


-- | The main algorithm for lifting a binary to an L0 representation (i.e., a Hoare Graph)
lift_to_L0 :: StateT Context IO ()
lift_to_L0 :: StateT Context IO ()
lift_to_L0 = do
  -- 1.) read entry points, clear .indirections file
  StateT Context IO ()
ctxt_read_and_set_entries
  StateT Context IO ()
ctxt_init_indirections

  -- 2.) repeatedly, do 2.1 -> 2.3
  StateT Context IO ()
repeat
 where
  -- 2.)
  repeat :: StateT Context IO ()
repeat = do
    Maybe (Int, IntSet)
reconsider <- StateT Context IO (Maybe (Int, IntSet))
ctxt_reconsider_mutual_recursive_call
    case Maybe (Int, IntSet)
reconsider of
      Just (Int
entry,IntSet
trgts) -> do
        String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n\nReconsidering (due to mutual recursion) entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
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."
        Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
        (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> Context -> Context
set_ctxt_recursions (Int -> IntMap IntSet -> IntMap IntSet
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
entry (IntMap IntSet -> IntMap IntSet) -> IntMap IntSet -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ Context -> IntMap IntSet
ctxt_recursions Context
ctxt)
        (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap FReturnBehavior -> Context -> Context
set_ctxt_calls (Int -> IntMap FReturnBehavior -> IntMap FReturnBehavior
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
entry (IntMap FReturnBehavior -> IntMap FReturnBehavior)
-> IntMap FReturnBehavior -> IntMap FReturnBehavior
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt)
        (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Graph -> Context -> Context
set_ctxt_entries (Graph -> Int -> IntSet -> Graph
graph_add_edges (Context -> Graph
ctxt_entries Context
ctxt) Int
entry IntSet
IS.empty)
        StateT Context IO ()
repeat
      Maybe (Int, IntSet)
Nothing -> do
        Graph
entries <- (Context -> Graph) -> StateT Context IO Graph
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Graph
ctxt_entries
        case Graph -> Maybe Int
graph_find_next Graph
entries of
          Maybe Int
Nothing -> StateT Context IO ()
ctxt_finish_repeat
          Just Int
a  -> Int -> StateT Context IO ()
ctxt_run_entry Int
a

  ctxt_finish_repeat :: StateT Context IO ()
ctxt_finish_repeat = do
    [(Int, Int)]
dangling_fptrs <- StateT Context IO [(Int, Int)]
ctxt_find_dangling_function_pointers
    String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Done!"
    Bool -> StateT Context IO () -> StateT Context IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Int, Int)]
dangling_fptrs [(Int, Int)] -> [(Int, Int)] -> Bool
forall a. Eq a => a -> a -> Bool
/= []) (StateT Context IO () -> StateT Context IO ())
-> StateT Context IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> StateT Context IO ()
to_out_r (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
""
      String -> StateT Context IO ()
to_out_r (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
""
      String -> StateT Context IO ()
to_out_r (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Dangling function pointers found, which may point to function entries currently not analyzed."
      String -> StateT Context IO ()
to_out_r (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"These require manual analysis: if they correspond to real function entries, add them to the .entry file"
      String -> StateT Context IO ()
to_out_r (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> String
forall b a.
(Integral b, Integral a, Show b, Show a) =>
[(a, b)] -> String
show_dangling_function_pointers [(Int, Int)]
dangling_fptrs




  -- 2.1) consider the current entry address $a$
  ctxt_run_entry :: Int -> StateT Context IO ()
ctxt_run_entry Int
a = do
    -- 2.2) Start analysis at entry-address $a$
    IntMap FReturnBehavior
calls <- (Context -> IntMap FReturnBehavior)
-> StateT Context IO (IntMap FReturnBehavior)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap FReturnBehavior
ctxt_calls
    Bool
has_instruction <- (Context -> Bool) -> StateT Context IO Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Context -> Int -> Bool) -> Int -> Context -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Context -> Int -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction (Int -> Context -> Bool) -> Int -> Context -> Bool
forall a b. (a -> b) -> a -> b
$ Int
a)
    case (Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
a IntMap FReturnBehavior
calls, Bool
has_instruction)  of
      (Just FReturnBehavior
_,Bool
_) -> do
        -- 2.2.1) Entry is already done, delete it and continue
        Int -> StateT Context IO ()
ctxt_del_entry Int
a
        StateT Context IO ()
repeat
      (Maybe FReturnBehavior
_,Bool
False)  -> do
        String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n\nEntry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ignored."
        Int -> StateT Context IO ()
ctxt_del_entry Int
a
        StateT Context IO ()
repeat
      (Maybe FReturnBehavior, Bool)
_ -> do
        String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n\nEntry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
a
        -- 2.2.3) Entry is new, generate a CFG
        Maybe CFG
curr_g <- (Context -> Maybe CFG) -> StateT Context IO (Maybe CFG)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap CFG -> Maybe CFG
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
a (IntMap CFG -> Maybe CFG)
-> (Context -> IntMap CFG) -> Context -> Maybe CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IntMap CFG
ctxt_cfgs)
        (FInit
curr_finit,Invariants
curr_invs,Set (NodeInfo, Predicate)
curr_posts,Set SStatePart
curr_sps) <- Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
a


        String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": starting CFG generation."
        Int -> StateT Context IO (Set (Instruction, Int))
ctxt_generate_cfg Int
a
        Int
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set SStatePart
-> StateT Context IO ()
ctxt_generate_invs Int
a Invariants
curr_invs Set (NodeInfo, Predicate)
curr_posts Set SStatePart
curr_sps

        Maybe CFG
g <- (Context -> Maybe CFG) -> StateT Context IO (Maybe CFG)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap CFG -> Maybe CFG
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
a (IntMap CFG -> Maybe CFG)
-> (Context -> IntMap CFG) -> Context -> Maybe CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IntMap CFG
ctxt_cfgs)
        (FInit
finit,Invariants
invs,Set (NodeInfo, Predicate)
posts,Set SStatePart
sps) <- Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
a
        let do_repeat :: Bool
do_repeat = Maybe CFG
curr_g Maybe CFG -> Maybe CFG -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe CFG
g Bool -> Bool -> Bool
|| Set SStatePart
curr_sps Set SStatePart -> Set SStatePart -> Bool
forall a. Eq a => a -> a -> Bool
/= Set SStatePart
sps -- TODO why sps, not posts?

        [(Int, FInit)]
new_calls <- Int -> StateT Context IO [(Int, FInit)]
forall a. (Eq a, Num a) => Int -> StateT Context IO [(a, FInit)]
ctxt_get_new_calls Int
a
        if [(Int, FInit)]
new_calls [(Int, FInit)] -> [(Int, FInit)] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then do
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": no new entries."
          Int -> Bool -> StateT Context IO ()
ctxt_after_invgen Int
a Bool
do_repeat 
        else do
          ((Int, FInit) -> StateT Context IO ())
-> [(Int, FInit)] -> StateT Context IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int -> (Int, FInit) -> StateT Context IO ()
ctxt_add_entry_edge Int
a) [(Int, FInit)]
new_calls
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Adding new internal functions at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. (Integral a, Show a) => [a] -> String
showHex_list (((Int, FInit) -> Int) -> [(Int, FInit)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, FInit) -> Int
forall a b. (a, b) -> a
fst [(Int, FInit)]
new_calls) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to graph of entries."
          StateT Context IO ()
repeat

  -- 2.3) Analyze a CFG, either needing a new round (in case of newly resolved indirections) are not.
  ctxt_after_invgen :: Int -> Bool -> StateT Context IO ()
ctxt_after_invgen Int
entry Bool
do_repeat = do
    -- analyze unresolved jumps
    Bool
continue <- Int -> StateT Context IO Bool
ctxt_analyze_unresolved_indirections Int
entry
    if Bool
continue then do
      -- if new jumps where resolved, repeat with current function
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Continuing to next round as there are newly resolved indirections."
      StateT Context IO ()
repeat
    else if Bool
do_repeat then do
      -- if new invariants were found, repeat with current function
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Continuing to next round as CFG or invariants where refined."
      StateT Context IO ()
repeat
    else do
      -- if no new jumps where resolved, this function is done: store entry address as an analyzed call and pop the entry-stack
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Terminating as no new indirections are resolved."
      VerificationResult
verified <- Int -> StateT Context IO VerificationResult
ctxt_verify_proper_return Int
entry
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Verified == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerificationResult -> String
forall a. Show a => a -> String
show VerificationResult
verified

      Int -> VerificationResult -> StateT Context IO ()
ctxt_add_call Int
entry VerificationResult
verified
      Int -> StateT Context IO ()
ctxt_del_entry Int
entry
      Int -> VerificationResult -> StateT Context IO ()
ctxt_add_to_results Int
entry VerificationResult
verified
      Int -> StateT Context IO ()
ctxt_get_recursive_calls Int
entry
      StateT Context IO ()
repeat



ctxt_find_dangling_function_pointers :: StateT Context IO [(Int,Int)]
ctxt_find_dangling_function_pointers :: StateT Context IO [(Int, Int)]
ctxt_find_dangling_function_pointers = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let ptrs :: [(Int, Int)]
ptrs = (VerificationCondition -> [(Int, Int)])
-> [VerificationCondition] -> [(Int, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VerificationCondition -> [(Int, Int)]
forall a. Num a => VerificationCondition -> [(a, Int)]
mk_function_pointer (Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList (Set VerificationCondition -> [VerificationCondition])
-> Set VerificationCondition -> [VerificationCondition]
forall a b. (a -> b) -> a -> b
$ IntMap (Set VerificationCondition) -> Set VerificationCondition
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (IntMap (Set VerificationCondition) -> Set VerificationCondition)
-> IntMap (Set VerificationCondition) -> Set VerificationCondition
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt)
  ((Int, Int) -> StateT Context IO Bool)
-> [(Int, Int)] -> StateT Context IO [(Int, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Int, Int) -> StateT Context IO Bool
forall (m :: * -> *) a. MonadState Context m => (a, Int) -> m Bool
is_dangling [(Int, Int)]
ptrs
 where
  mk_function_pointer :: VerificationCondition -> [(a, Int)]
mk_function_pointer (FunctionPointers Word64
a IntSet
ptrs) = (Int -> (a, Int)) -> [Int] -> [(a, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> (a, Int)
forall a b. a -> b -> (a, b)
pair (Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a)) ([Int] -> [(a, Int)]) -> [Int] -> [(a, Int)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList IntSet
ptrs
  mk_function_pointer VerificationCondition
_                         = []

  is_dangling :: (a, Int) -> m Bool
is_dangling (a
a,Int
ptr) = do
    IntMap FReturnBehavior
calls <- (Context -> IntMap FReturnBehavior) -> m (IntMap FReturnBehavior)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap FReturnBehavior
ctxt_calls
    Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
ptr IntMap FReturnBehavior
calls Maybe FReturnBehavior -> Maybe FReturnBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe FReturnBehavior
forall a. Maybe a
Nothing
    
    
show_dangling_function_pointers :: [(a, b)] -> String
show_dangling_function_pointers [] = String
""
show_dangling_function_pointers ((a
a,b
fptr):[(a, b)]
fptrs) = 
  let ([(a, b)]
match,[(a, b)]
remaining) = ((a, b) -> Bool) -> [(a, b)] -> ([(a, b)], [(a, b)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a, b) -> Bool
forall a. (a, b) -> Bool
does_match [(a, b)]
fptrs in
    String
"Function pointer " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. (Integral a, Show a) => a -> String
showHex b
fptr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" introduced at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. (Integral a, Show a) => [a] -> String
showHex_list (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst  [(a, b)]
match) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(a, b)] -> String
show_dangling_function_pointers [(a, b)]
remaining
 where
  does_match :: (a, b) -> Bool
does_match (a
_,b
fptr') = b
fptr b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
fptr'
  



ctxt_get_recursive_calls :: Int -> StateT Context IO ()
ctxt_get_recursive_calls :: Int -> StateT Context IO ()
ctxt_get_recursive_calls Int
entry = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let g :: CFG
g = Context -> IntMap CFG
ctxt_cfgs Context
ctxt IntMap CFG -> Int -> CFG
forall a. IntMap a -> Int -> a
IM.! Int
entry
  let recursions :: IntSet
recursions = [Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Int] -> [Int]) -> [Maybe Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [[Maybe Int]] -> [Maybe Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Maybe Int]] -> [Maybe Int]) -> [[Maybe Int]] -> [Maybe Int]
forall a b. (a -> b) -> a -> b
$ ([Instruction] -> [[Maybe Int]])
-> [[Instruction]] -> [[Maybe Int]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Context -> [Instruction] -> [[Maybe Int]]
forall a. Num a => Context -> [Instruction] -> [[Maybe a]]
get_new_calls Context
ctxt) ([[Instruction]] -> [[Maybe Int]])
-> [[Instruction]] -> [[Maybe Int]]
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
g
  Bool -> StateT Context IO () -> StateT Context IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
IS.null IntSet
recursions) (StateT Context IO () -> StateT Context IO ())
-> StateT Context IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ do
    (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> Context -> Context
set_ctxt_recursions ((IntSet -> IntSet -> IntSet)
-> Int -> IntSet -> IntMap IntSet -> IntMap IntSet
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith IntSet -> IntSet -> IntSet
IS.union Int
entry IntSet
recursions (Context -> IntMap IntSet
ctxt_recursions Context
ctxt))
    String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
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
recursions String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as external. It will be reconsidered after those entries have been done."
 where
  get_new_calls :: Context -> [Instruction] -> [[Maybe a]]
get_new_calls Context
ctxt [Instruction]
is = (Instruction -> [Maybe a]) -> [Instruction] -> [[Maybe a]]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> Instruction -> [Maybe a]
forall a. Num a => Context -> Instruction -> [Maybe a]
get_new_call Context
ctxt) [Instruction]
is
  get_new_call :: Context -> Instruction -> [Maybe a]
get_new_call  Context
ctxt Instruction
i =
    if Opcode -> Bool
isCall (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) then
      (ResolvedJumpTarget -> Maybe a)
-> [ResolvedJumpTarget] -> [Maybe a]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> ResolvedJumpTarget -> Maybe a
forall a. Num a => Context -> ResolvedJumpTarget -> Maybe a
when_trgt_is_not_done_yet Context
ctxt) ([ResolvedJumpTarget] -> [Maybe a])
-> [ResolvedJumpTarget] -> [Maybe a]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i
    else
      []

  when_trgt_is_not_done_yet :: Context -> ResolvedJumpTarget -> Maybe a
when_trgt_is_not_done_yet Context
ctxt (ImmediateAddress Word64
trgt) =
    case (Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt) (IntMap FReturnBehavior -> Maybe FReturnBehavior)
-> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt) of
      Maybe FReturnBehavior
Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt
      Just FReturnBehavior
_  -> Maybe a
forall a. Maybe a
Nothing
  when_trgt_is_not_done_yet Context
ctxt ResolvedJumpTarget
_ = Maybe a
forall a. Maybe a
Nothing


ctxt_reconsider_mutual_recursive_call :: StateT Context IO (Maybe (Int,IS.IntSet))
ctxt_reconsider_mutual_recursive_call :: StateT Context IO (Maybe (Int, IntSet))
ctxt_reconsider_mutual_recursive_call = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  IntMap IntSet
recursions <- (Context -> IntMap IntSet) -> StateT Context IO (IntMap IntSet)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap IntSet
ctxt_recursions
  Maybe (Int, IntSet) -> StateT Context IO (Maybe (Int, IntSet))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, IntSet) -> StateT Context IO (Maybe (Int, IntSet)))
-> Maybe (Int, IntSet) -> StateT Context IO (Maybe (Int, IntSet))
forall a b. (a -> b) -> a -> b
$ ((Int, IntSet) -> Bool) -> [(Int, IntSet)] -> Maybe (Int, IntSet)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Context -> (Int, IntSet) -> Bool
forall a. Context -> (a, IntSet) -> Bool
to_be_reconsidered Context
ctxt) ([(Int, IntSet)] -> Maybe (Int, IntSet))
-> [(Int, IntSet)] -> Maybe (Int, IntSet)
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap IntSet
recursions
 where
  to_be_reconsidered :: Context -> (a, IntSet) -> Bool
to_be_reconsidered Context
ctxt (a
entry,IntSet
trgts) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
trgt -> Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
trgt (Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt) Maybe FReturnBehavior -> Maybe FReturnBehavior -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe FReturnBehavior
forall a. Maybe a
Nothing) ([Int] -> Bool) -> [Int] -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList IntSet
trgts






ctxt_get_new_calls :: Int -> StateT Context IO [(a, FInit)]
ctxt_get_new_calls Int
entry = do
  Context
ctxt   <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  FContext
fctxt  <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
  let g :: CFG
g   = Context -> IntMap CFG
ctxt_cfgs Context
ctxt IntMap CFG -> Int -> CFG
forall a. IntMap a -> Int -> a
IM.! Int
entry

  [(a, FInit)] -> StateT Context IO [(a, FInit)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, FInit)] -> StateT Context IO [(a, FInit)])
-> [(a, FInit)] -> StateT Context IO [(a, FInit)]
forall a b. (a -> b) -> a -> b
$ FContext -> [(a, FInit)] -> [(a, FInit)]
forall a. Eq a => FContext -> [(a, FInit)] -> [(a, FInit)]
gather FContext
fctxt ([(a, FInit)] -> [(a, FInit)]) -> [(a, FInit)] -> [(a, FInit)]
forall a b. (a -> b) -> a -> b
$ [Maybe (a, FInit)] -> [(a, FInit)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (a, FInit)] -> [(a, FInit)])
-> [Maybe (a, FInit)] -> [(a, FInit)]
forall a b. (a -> b) -> a -> b
$ [[Maybe (a, FInit)]] -> [Maybe (a, FInit)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Maybe (a, FInit)]] -> [Maybe (a, FInit)])
-> [[Maybe (a, FInit)]] -> [Maybe (a, FInit)]
forall a b. (a -> b) -> a -> b
$ ([Instruction] -> [[Maybe (a, FInit)]])
-> [[Instruction]] -> [[Maybe (a, FInit)]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FContext -> [Instruction] -> [[Maybe (a, FInit)]]
forall a.
Num a =>
FContext -> [Instruction] -> [[Maybe (a, FInit)]]
get_new_calls FContext
fctxt) ([[Instruction]] -> [[Maybe (a, FInit)]])
-> [[Instruction]] -> [[Maybe (a, FInit)]]
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
g
 where
  get_new_calls :: FContext -> [Instruction] -> [[Maybe (a, FInit)]]
get_new_calls FContext
fctxt [Instruction]
is = (Instruction -> [Maybe (a, FInit)])
-> [Instruction] -> [[Maybe (a, FInit)]]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Instruction -> [Maybe (a, FInit)]
forall a. Num a => FContext -> Instruction -> [Maybe (a, FInit)]
get_new_call FContext
fctxt) [Instruction]
is
  get_new_call :: FContext -> Instruction -> [Maybe (a, FInit)]
get_new_call  FContext
fctxt Instruction
i =
    if Opcode -> Bool
isCall (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) Bool -> Bool -> Bool
|| (Opcode -> Bool
isJump (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) Bool -> Bool -> Bool
&& Context -> Instruction -> Bool
jump_is_actually_a_call (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i) then
       (ResolvedJumpTarget -> Maybe (a, FInit))
-> [ResolvedJumpTarget] -> [Maybe (a, FInit)]
forall a b. (a -> b) -> [a] -> [b]
map (FContext -> Instruction -> ResolvedJumpTarget -> Maybe (a, FInit)
forall a storage prefix opcode annotation.
Num a =>
FContext
-> GenericInstruction
     AddressWord64 storage prefix opcode annotation
-> ResolvedJumpTarget
-> Maybe (a, FInit)
trgt_to_finit FContext
fctxt Instruction
i) ([ResolvedJumpTarget] -> [Maybe (a, FInit)])
-> [ResolvedJumpTarget] -> [Maybe (a, FInit)]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target (FContext -> Context
f_ctxt FContext
fctxt) Instruction
i
    else
      []

  trgt_to_finit :: FContext
-> GenericInstruction
     AddressWord64 storage prefix opcode annotation
-> ResolvedJumpTarget
-> Maybe (a, FInit)
trgt_to_finit FContext
fctxt GenericInstruction AddressWord64 storage prefix opcode annotation
i (ImmediateAddress Word64
trgt) =
   let ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt in
    case (Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt) (IntMap FReturnBehavior -> Maybe FReturnBehavior)
-> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt, Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt) (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt, FContext -> Int -> Maybe Predicate
get_invariant FContext
fctxt (Int -> Maybe Predicate) -> Int -> Maybe Predicate
forall a b. (a -> b) -> a -> b
$ Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof GenericInstruction AddressWord64 storage prefix opcode annotation
i) of
      (Maybe FReturnBehavior
Nothing,Maybe FInit
Nothing,Just Predicate
inv) -> (a, FInit) -> Maybe (a, FInit)
forall a. a -> Maybe a
Just ((a, FInit) -> Maybe (a, FInit)) -> (a, FInit) -> Maybe (a, FInit)
forall a b. (a -> b) -> a -> b
$ (Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt,FContext -> Predicate -> FInit
invariant_to_finit FContext
fctxt Predicate
inv)
      (Maybe FReturnBehavior
_,Just FInit
finit,Just Predicate
inv)    -> do
        let finit' :: FInit
finit' = FContext -> FInit -> FInit -> FInit
join_finit FContext
fctxt (FContext -> Predicate -> FInit
invariant_to_finit FContext
fctxt Predicate
inv) FInit
finit
        if FInit
finit FInit -> FInit -> Bool
forall a. Eq a => a -> a -> Bool
/= FInit
finit' Bool -> Bool -> Bool
|| (Graph -> Int -> Bool
graph_is_vertex (Context -> Graph
ctxt_entries Context
ctxt) (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt) Bool -> Bool -> Bool
&& Bool -> Bool
not (Graph -> Int -> Int -> Bool
graph_is_edge (Context -> Graph
ctxt_entries Context
ctxt) Int
entry (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt))) then
          (a, FInit) -> Maybe (a, FInit)
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
trgt,FInit
finit') -- trace ("new finit@" ++ showHex trgt ++ "\n" ++ show finit ++ "\n" ++ show (invariant_to_finit fctxt inv) ++ "\n" ++ show finit') 
        else
          Maybe (a, FInit)
forall a. Maybe a
Nothing
      (Maybe FReturnBehavior
_,Maybe FInit
_,Maybe Predicate
Nothing) -> Maybe (a, FInit)
forall a. Maybe a
Nothing -- time out
      (Maybe FReturnBehavior
x,Maybe FInit
y,Maybe Predicate
z) -> String -> Maybe (a, FInit)
forall a. HasCallStack => String -> a
error ((Maybe FReturnBehavior, Maybe FInit, Maybe Predicate) -> String
forall a. Show a => a -> String
show (Maybe FReturnBehavior
x,Maybe FInit
y,Maybe Predicate
z))
  trgt_to_finit FContext
ctxt GenericInstruction AddressWord64 storage prefix opcode annotation
i ResolvedJumpTarget
_ = Maybe (a, FInit)
forall a. Maybe a
Nothing

  gather :: FContext -> [(a, FInit)] -> [(a, FInit)]
gather FContext
fctxt []         = []
  gather FContext
fctxt [(a, FInit)
new_call] = [(a, FInit)
new_call]
  gather FContext
fctxt ((a
entry',FInit
finit):[(a, FInit)]
new_calls) =
    let ([(a, FInit)]
same,[(a, FInit)]
others) = ((a, FInit) -> Bool)
-> [(a, FInit)] -> ([(a, FInit)], [(a, FInit)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) a
entry' (a -> Bool) -> ((a, FInit) -> a) -> (a, FInit) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, FInit) -> a
forall a b. (a, b) -> a
fst) [(a, FInit)]
new_calls in
      (a
entry', (FInit -> FInit -> FInit) -> [FInit] -> FInit
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FContext -> FInit -> FInit -> FInit
join_finit FContext
fctxt) (FInit
finitFInit -> [FInit] -> [FInit]
forall a. a -> [a] -> [a]
:((a, FInit) -> FInit) -> [(a, FInit)] -> [FInit]
forall a b. (a -> b) -> [a] -> [b]
map (a, FInit) -> FInit
forall a b. (a, b) -> b
snd [(a, FInit)]
same)) (a, FInit) -> [(a, FInit)] -> [(a, FInit)]
forall a. a -> [a] -> [a]
: FContext -> [(a, FInit)] -> [(a, FInit)]
gather FContext
fctxt [(a, FInit)]
others
    



ctxt_add_entry_edge :: Int -> (Int,FInit) -> StateT Context IO ()
ctxt_add_entry_edge :: Int -> (Int, FInit) -> StateT Context IO ()
ctxt_add_entry_edge Int
a (Int
trgt,FInit
finit) = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Graph -> Context -> Context
set_ctxt_entries (Graph -> Int -> IntSet -> Graph
graph_add_edges (Context -> Graph
ctxt_entries Context
ctxt) Int
a (Int -> IntSet
IS.singleton Int
trgt))
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap FInit -> Context -> Context
set_ctxt_finits  (Int -> FInit -> IntMap FInit -> IntMap FInit
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
trgt FInit
finit (IntMap FInit -> IntMap FInit) -> IntMap FInit -> IntMap FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt)
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap FReturnBehavior -> Context -> Context
set_ctxt_calls   (Int -> IntMap FReturnBehavior -> IntMap FReturnBehavior
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
trgt (IntMap FReturnBehavior -> IntMap FReturnBehavior)
-> IntMap FReturnBehavior -> IntMap FReturnBehavior
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt)
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap Invariants -> Context -> Context
set_ctxt_invs    (Int -> IntMap Invariants -> IntMap Invariants
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
trgt (IntMap Invariants -> IntMap Invariants)
-> IntMap Invariants -> IntMap Invariants
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Invariants
ctxt_invs  Context
ctxt)
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap (Set (NodeInfo, Predicate)) -> Context -> Context
set_ctxt_posts   (Int
-> IntMap (Set (NodeInfo, Predicate))
-> IntMap (Set (NodeInfo, Predicate))
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
trgt (IntMap (Set (NodeInfo, Predicate))
 -> IntMap (Set (NodeInfo, Predicate)))
-> IntMap (Set (NodeInfo, Predicate))
-> IntMap (Set (NodeInfo, Predicate))
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Set (NodeInfo, Predicate))
ctxt_posts Context
ctxt)


ctxt_get_curr_posts :: Int -> StateT Context IO (FInit,Invariants,S.Set (NodeInfo,Predicate),S.Set SStatePart)
ctxt_get_curr_posts :: Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
entry = do
  IntMap FInit
finits <- (Context -> IntMap FInit) -> StateT Context IO (IntMap FInit)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap FInit
ctxt_finits
  IntMap Invariants
invs   <- (Context -> IntMap Invariants)
-> StateT Context IO (IntMap Invariants)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap Invariants
ctxt_invs
  IntMap (Set (NodeInfo, Predicate))
posts  <- (Context -> IntMap (Set (NodeInfo, Predicate)))
-> StateT Context IO (IntMap (Set (NodeInfo, Predicate)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap (Set (NodeInfo, Predicate))
ctxt_posts
  IntMap (Set SStatePart)
sps    <- (Context -> IntMap (Set SStatePart))
-> StateT Context IO (IntMap (Set SStatePart))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap (Set SStatePart)
ctxt_stateparts
  (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry IntMap FInit
finits Maybe FInit -> FInit -> FInit
forall a. Eq a => Maybe a -> a -> a
`orElse` FInit
init_finit, Int -> IntMap Invariants -> Maybe Invariants
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry IntMap Invariants
invs Maybe Invariants -> Invariants -> Invariants
forall a. Eq a => Maybe a -> a -> a
`orElse` Invariants
forall a. IntMap a
IM.empty, Int
-> IntMap (Set (NodeInfo, Predicate))
-> Maybe (Set (NodeInfo, Predicate))
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry IntMap (Set (NodeInfo, Predicate))
posts Maybe (Set (NodeInfo, Predicate))
-> Set (NodeInfo, Predicate) -> Set (NodeInfo, Predicate)
forall a. Eq a => Maybe a -> a -> a
`orElse` Set (NodeInfo, Predicate)
forall a. Set a
S.empty,Int -> IntMap (Set SStatePart) -> Maybe (Set SStatePart)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry IntMap (Set SStatePart)
sps Maybe (Set SStatePart) -> Set SStatePart -> Set SStatePart
forall a. Eq a => Maybe a -> a -> a
`orElse` Set SStatePart
forall a. Set a
S.empty)




-- Assuming a CFG and invariants are generated, verify for each block $b$ that is an end-node in the CFG whether:
-- if the end-node "returns normally", i.e., ends in a RET, then it returns correctly, i.e., the return address is 
-- not overwritten and callee-saved registers are preserved and RSP is set to RSP0+8
ctxt_verify_proper_return :: Int -> StateT Context IO VerificationResult
ctxt_verify_proper_return :: Int -> StateT Context IO VerificationResult
ctxt_verify_proper_return Int
entry = do
  Context
ctxt            <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  FContext
fctxt           <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
  let vcs :: Set VerificationCondition
vcs          = Int
-> IntMap (Set VerificationCondition)
-> Maybe (Set VerificationCondition)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt) Maybe (Set VerificationCondition)
-> Set VerificationCondition -> Set VerificationCondition
forall a. Eq a => Maybe a -> a -> a
`orElse` Set VerificationCondition
forall a. Set a
S.empty
  (FInit
_,Invariants
_,Set (NodeInfo, Predicate)
posts,Set SStatePart
_)   <- Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
entry
  [[Maybe String]]
all_checks      <- ((NodeInfo, Predicate) -> StateT Context IO [Maybe String])
-> [(NodeInfo, Predicate)] -> StateT Context IO [[Maybe String]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FContext
-> (NodeInfo, Predicate) -> StateT Context IO [Maybe String]
correct FContext
fctxt) ([(NodeInfo, Predicate)] -> StateT Context IO [[Maybe String]])
-> [(NodeInfo, Predicate)] -> StateT Context IO [[Maybe String]]
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate) -> Bool)
-> [(NodeInfo, Predicate)] -> [(NodeInfo, Predicate)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(NodeInfo
ni,Predicate
q) -> NodeInfo
ni NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= NodeInfo
Terminal) ([(NodeInfo, Predicate)] -> [(NodeInfo, Predicate)])
-> [(NodeInfo, Predicate)] -> [(NodeInfo, Predicate)]
forall a b. (a -> b) -> a -> b
$ Set (NodeInfo, Predicate) -> [(NodeInfo, Predicate)]
forall a. Set a -> [a]
S.toList Set (NodeInfo, Predicate)
posts

  if Set (NodeInfo, Predicate) -> Bool
forall a. Set a -> Bool
S.null Set (NodeInfo, Predicate)
posts then
    VerificationResult -> StateT Context IO VerificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> VerificationResult
VerificationError String
"time out reached")
  else if ((NodeInfo, Predicate) -> Bool)
-> Set (NodeInfo, Predicate) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(NodeInfo
ni,Predicate
q) -> NodeInfo
ni NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
== NodeInfo
UnresolvedIndirection) Set (NodeInfo, Predicate)
posts then do
    VerificationResult -> StateT Context IO VerificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return VerificationResult
VerificationUnresolvedIndirection
  else if (Maybe String -> Bool) -> [Maybe String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Maybe String
forall a. Maybe a
Nothing) ([Maybe String] -> Bool) -> [Maybe String] -> Bool
forall a b. (a -> b) -> a -> b
$ [[Maybe String]] -> [Maybe String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Maybe String]]
all_checks then do
    VerificationResult -> StateT Context IO VerificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> VerificationResult
VerificationError (String -> VerificationResult) -> String -> VerificationResult
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
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> [String]) -> [Maybe String] -> [String]
forall a b. (a -> b) -> a -> b
$ [[Maybe String]] -> [Maybe String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Maybe String]]
all_checks)
  else if (VerificationCondition -> Bool)
-> Set VerificationCondition -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool)
-> (VerificationCondition -> Bool) -> VerificationCondition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerificationCondition -> Bool
is_precondition) Set VerificationCondition
vcs then do
    VerificationResult -> StateT Context IO VerificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return VerificationResult
VerificationSuccesWithAssumptions
  else
    VerificationResult -> StateT Context IO VerificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return VerificationResult
VerificationSuccess
 where
  -- is the postcondition "correct"? 
  -- A succesfull check returns Nothing, a verification error produces a "Just err" with an error-message
  correct :: FContext -> (NodeInfo,Predicate) -> StateT Context IO [Maybe String]
  correct :: FContext
-> (NodeInfo, Predicate) -> StateT Context IO [Maybe String]
correct FContext
fctxt (NodeInfo
_,Predicate
q) = do
    [Maybe String] -> StateT Context IO [Maybe String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe String] -> StateT Context IO [Maybe String])
-> [Maybe String] -> StateT Context IO [Maybe String]
forall a b. (a -> b) -> a -> b
$ Identity [Maybe String] -> [Maybe String]
forall a. Identity a -> a
runIdentity (Identity [Maybe String] -> [Maybe String])
-> Identity [Maybe String] -> [Maybe String]
forall a b. (a -> b) -> a -> b
$ StateT
  (Predicate, Set VerificationCondition) Identity [Maybe String]
-> (Predicate, Set VerificationCondition)
-> Identity [Maybe String]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (FContext
-> StateT
     (Predicate, Set VerificationCondition) Identity [Maybe String]
do_post_check FContext
fctxt) (Predicate
q,Set VerificationCondition
forall a. Set a
S.empty) 


  -- do one more tau-transformation on the node, as the stored invariant is a 
  -- precondition (not a postcondition) of the node.
  do_post_check :: FContext -> State (Predicate,VCS) [Maybe String]
  do_post_check :: FContext
-> StateT
     (Predicate, Set VerificationCondition) Identity [Maybe String]
do_post_check FContext
fctxt = do
    let f :: String
f   = Context -> Int -> String
function_name_of_entry (FContext -> Context
f_ctxt FContext
fctxt) (FContext -> Int
f_entry FContext
fctxt)
    SValue
rsp    <- FContext
-> Register -> State (Predicate, Set VerificationCondition) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
sread_reg FContext
fctxt Register
RSP
    SValue
rip    <- FContext
-> Register -> State (Predicate, Set VerificationCondition) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> Register -> State (Sstate v p, Set VerificationCondition) v
sread_reg FContext
fctxt Register
RIP
    [Maybe String]
checks <- [Maybe String]
-> StateT
     (Predicate, Set VerificationCondition) Identity [Maybe String]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- forM (delete RSP callee_saved_registers) (\r -> read_reg ctxt r >>= return . reg_check r) 
    (Predicate
s,Set VerificationCondition
_)  <- StateT
  (Predicate, Set VerificationCondition)
  Identity
  (Predicate, Set VerificationCondition)
forall s (m :: * -> *). MonadState s m => m s
get
    [Maybe String]
-> StateT
     (Predicate, Set VerificationCondition) Identity [Maybe String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe String]
 -> StateT
      (Predicate, Set VerificationCondition) Identity [Maybe String])
-> [Maybe String]
-> StateT
     (Predicate, Set VerificationCondition) Identity [Maybe String]
forall a b. (a -> b) -> a -> b
$ [FContext -> String -> SValue -> Maybe String
forall ctxt a p.
SymbolicExecutable ctxt a p =>
ctxt -> String -> a -> Maybe String
rsp_check FContext
fctxt String
f SValue
rsp, FContext -> Predicate -> String -> SValue -> Maybe String
forall ctxt a p a p.
(SymbolicExecutable ctxt a p, Show a) =>
ctxt -> a -> p -> a -> Maybe String
rip_check FContext
fctxt Predicate
s String
f SValue
rip] [Maybe String] -> [Maybe String] -> [Maybe String]
forall a. [a] -> [a] -> [a]
++ [Maybe String]
checks

  -- check: are all caller-saved-registers restored to their initial values?
  reg_check :: ctxt -> a -> a -> Maybe String
reg_check ctxt
fctxt a
reg a
v =
    case ctxt -> a -> Maybe SimpleExpr
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Maybe SimpleExpr
stry_deterministic ctxt
fctxt a
v of
      -- REG == REG_0
      Just (SE_Var (SP_Reg Register
reg)) -> Maybe String
forall a. Maybe a
Nothing
      Maybe SimpleExpr
_ -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Verification error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
reg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v

  -- check: is RSP restored to RSP_0 + 8 ?
  rsp_check :: ctxt -> String -> a -> Maybe String
rsp_check ctxt
fctxt  String
f a
rsp = 
    case ctxt -> a -> Maybe SimpleExpr
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Maybe SimpleExpr
stry_deterministic ctxt
fctxt a
rsp of
      -- RSP == RSP_0 + 8
      Just (SE_Op Operator
Plus Int
_ [SE_Var (SP_StackPointer String
f'), SE_Immediate Word64
0x8]) -> if String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
f' then Maybe String
forall a. Maybe a
Nothing else a -> Maybe String
forall a. Show a => a -> Maybe String
v_error a
rsp
      -- RSP == RSP_0 - 0xfffffffffffffff8
      Just (SE_Op Operator
Minus Int
_ [SE_Var (SP_StackPointer String
f'), SE_Immediate Word64
0xfffffffffffffff8]) -> if String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
f' then Maybe String
forall a. Maybe a
Nothing else a -> Maybe String
forall a. Show a => a -> Maybe String
v_error a
rsp
      Maybe SimpleExpr
_ -> a -> Maybe String
forall a. Show a => a -> Maybe String
v_error a
rsp
  v_error :: a -> Maybe String
v_error a
rsp = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Verification error: RSP == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
rsp

  -- check: is RIP set to the value originally stored at the top of the stack frame?
  rip_check :: ctxt -> a -> p -> a -> Maybe String
rip_check ctxt
fctxt  a
s p
f a
rip = 
    case ctxt -> a -> Maybe SimpleExpr
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Maybe SimpleExpr
stry_deterministic ctxt
fctxt a
rip of
      -- RIP == *[RSP_0,8]
      Just (SE_Var (SP_Mem (SE_Var (SP_StackPointer String
f)) Int
8)) -> Maybe String
forall a. Maybe a
Nothing
      Maybe SimpleExpr
e -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Verification error: RIP == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
rip String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nState: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s 



-- After a succesfull effort, store the current CFG, the invariants,...,  in the "report"-field of the context
ctxt_add_to_results :: Int -> VerificationResult -> StateT Context IO ()
ctxt_add_to_results Int
entry VerificationResult
verified = do
  IntMap VerificationResult
results <- (Context -> IntMap VerificationResult)
-> StateT Context IO (IntMap VerificationResult)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap VerificationResult
ctxt_results
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap VerificationResult -> Context -> Context
set_ctxt_results (Int
-> VerificationResult
-> IntMap VerificationResult
-> IntMap VerificationResult
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry VerificationResult
verified IntMap VerificationResult
results)

  Context
ctxt     <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  String
base     <- Int -> StateT Context IO String
ctxt_base_name Int
entry
  let invs :: Invariants
invs  = Context -> IntMap Invariants
ctxt_invs Context
ctxt IntMap Invariants -> Int -> Invariants
forall a. IntMap a -> Int -> a
IM.! Int
entry
  let g :: CFG
g     = Context -> IntMap CFG
ctxt_cfgs Context
ctxt IntMap CFG -> Int -> CFG
forall a. IntMap a -> Int -> a
IM.! Int
entry
  let ret :: FReturnBehavior
ret   = Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt IntMap FReturnBehavior -> Int -> FReturnBehavior
forall a. IntMap a -> Int -> a
IM.! Int
entry
  let finit :: Maybe FInit
finit = Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt
  let vcs :: Set VerificationCondition
vcs   = Int
-> IntMap (Set VerificationCondition)
-> Maybe (Set VerificationCondition)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt) Maybe (Set VerificationCondition)
-> Set VerificationCondition -> Set VerificationCondition
forall a. Eq a => Maybe a -> a -> a
`orElse` Set VerificationCondition
forall a. Set a
S.empty
  let log :: String
log   = String
base String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".log"

  IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
log String
""

  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Function entry:             " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Verification result:        " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerificationResult -> String
show_verification_result VerificationResult
verified
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#instructions:              " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (CFG -> Int
num_of_instructions CFG
g)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#assertions:                " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set VerificationCondition -> Int
count_instructions_with_assertions Set VerificationCondition
vcs)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#unresolved indirect jumps: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Context -> (Opcode -> Bool) -> CFG -> Int
num_of_unres_inds_in_cfg Context
ctxt Opcode -> Bool
isJump CFG
g)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#unresolved indirect calls: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Context -> (Opcode -> Bool) -> CFG -> Int
num_of_unres_inds_in_cfg Context
ctxt Opcode -> Bool
isCall CFG
g)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#blocks:                    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (CFG -> Int
num_of_blocks       CFG
g)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"#edges:                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (CFG -> Int
num_of_edges        CFG
g)
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
""

  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Maybe FInit -> String
summarize_finit Maybe FInit
finit
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
""

  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Return behavior: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FReturnBehavior -> String
show_return_behavior FReturnBehavior
ret  

  --to_log log $ summarize_preconditions_long ctxt vcs -- TODO make configurable
  --to_log log $ summarize_assertions_long ctxt vcs
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Set VerificationCondition -> String
summarize_function_constraints_long Context
ctxt Set VerificationCondition
vcs
  String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Set VerificationCondition -> String
forall p. p -> Set VerificationCondition -> String
summarize_function_pointers Context
ctxt Set VerificationCondition
vcs


  Bool -> StateT Context IO () -> StateT Context IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxt_verbose_logs Context
ctxt) (StateT Context IO () -> StateT Context IO ())
-> StateT Context IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> StateT Context IO ()
forall (m :: * -> *). MonadIO m => String -> String -> m ()
to_log String
log (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ CFG -> Invariants -> String
show_invariants CFG
g Invariants
invs
 where
  show_return_behavior :: FReturnBehavior -> String
show_return_behavior (ReturningWith Predicate
p)  = String
"returning with\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Predicate -> String
forall a. Show a => a -> String
show Predicate
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
  show_return_behavior FReturnBehavior
Terminating        = String
"terminating"
  show_return_behavior FReturnBehavior
UnknownRetBehavior = String
"unknown"

  show_verification_result :: VerificationResult -> String
show_verification_result (VerificationError String
msg)           = String
"\n\n\n---------------------\nVerification error!!!\n---------------------\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
  show_verification_result VerificationResult
VerificationSuccesWithAssumptions = String
"Verified (with assumptions)"
  show_verification_result VerificationResult
VerificationSuccess               = String
"Verified"
  show_verification_result VerificationResult
VerificationUnresolvedIndirection = String
"Unresolved indirections"
  show_verification_result VerificationResult
Unverified                        = String
"UNVERIFIED"

















-- Read entry from file producing entries :: [Int]
ctxt_read_entries :: StateT Context IO [Int]
ctxt_read_entries :: StateT Context IO [Int]
ctxt_read_entries = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let dirname :: String
dirname = Context -> String
ctxt_dirname Context
ctxt
  let name :: String
name    = Context -> String
ctxt_name Context
ctxt
  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 [Int] -> StateT Context IO [Int]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Int] -> StateT Context IO [Int])
-> IO [Int] -> StateT Context IO [Int]
forall a b. (a -> b) -> a -> b
$ String -> IO [Int]
parse (String -> IO [Int]) -> String -> IO [Int]
forall a b. (a -> b) -> a -> b
$! String
fname
 where
  parse :: String -> IO [Int]
parse String
filename = do
    String
ls <- String -> IO String
readFile String
filename
    [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> IO [Int]) -> [Int] -> IO [Int]
forall a b. (a -> b) -> a -> b
$ (String -> Int) -> [String] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map String -> Int
read_line ([String] -> [Int]) -> [String] -> [Int]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
ls
  read_line :: String -> Int
read_line = String -> Int
forall a. (Eq a, Num a) => String -> a
readHex' (String -> Int) -> (String -> String) -> String -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
tail (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
tail





-- Read entry from file producing entry :: Int
ctxt_read_and_set_entries :: StateT Context IO ()
ctxt_read_and_set_entries :: StateT Context IO ()
ctxt_read_and_set_entries = do
  [Int]
entries <- StateT Context IO [Int]
ctxt_read_entries
  [[Word64]]
read_arrays <- StateT Context IO [[Word64]]
ctxt_read_init_fini_arrays
  let extra_ptrs :: [Int]
extra_ptrs = (Word64 -> Int) -> [Word64] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Word64] -> [Int]) -> [Word64] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Bool) -> [Word64] -> [Word64]
forall a. (a -> Bool) -> [a] -> [a]
filter (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Word64
0) ([Word64] -> [Word64]) -> [Word64] -> [Word64]
forall a b. (a -> b) -> a -> b
$ (Word64 -> Bool) -> [Word64] -> [Word64]
forall a. (a -> Bool) -> [a] -> [a]
filter (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Word64
0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
1)) ([Word64] -> [Word64]) -> [Word64] -> [Word64]
forall a b. (a -> b) -> a -> b
$ [[Word64]] -> [Word64]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Word64]]
read_arrays
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Graph -> Context -> Context
set_ctxt_entries (IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Int, IntSet)] -> IntMap IntSet
forall a. [(Int, a)] -> IntMap a
IM.fromList ([Int] -> [IntSet] -> [(Int, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Int]
entries [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
extra_ptrs) ([IntSet] -> [(Int, IntSet)]) -> [IntSet] -> [(Int, IntSet)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [IntSet]
forall a. a -> [a]
repeat IntSet
IS.empty))
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Context -> Context
set_ctxt_start ([Int] -> Int
forall a. [a] -> a
head [Int]
entries)
 where
  ctxt_read_init_fini_arrays :: StateT Context IO [[Word64]]
ctxt_read_init_fini_arrays = (Context -> [(String, String, Word64, Word64)])
-> StateT Context IO [(String, String, Word64, Word64)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SectionsInfo -> [(String, String, Word64, Word64)]
si_sections (SectionsInfo -> [(String, String, Word64, Word64)])
-> (Context -> SectionsInfo)
-> Context
-> [(String, String, Word64, Word64)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> SectionsInfo
ctxt_sections) StateT Context IO [(String, String, Word64, Word64)]
-> ([(String, String, Word64, Word64)]
    -> StateT Context IO [[Word64]])
-> StateT Context IO [[Word64]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((String, String, Word64, Word64) -> StateT Context IO [Word64])
-> [(String, String, Word64, Word64)]
-> StateT Context IO [[Word64]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String, String, Word64, Word64) -> StateT Context IO [Word64]
forall (m :: * -> *) t.
(MonadState Context m, Integral t) =>
(String, String, Word64, t) -> m [Word64]
ctxt_read_init_fini_array 

  ctxt_read_init_fini_array :: (String, String, Word64, t) -> m [Word64]
ctxt_read_init_fini_array (String
"", String
".init_array",Word64
a0,t
si) = Word64 -> t -> m [Word64]
forall t (m :: * -> *).
(MonadState Context m, Integral t) =>
Word64 -> t -> m [Word64]
read_pointers_from_ro_data_section Word64
a0 t
si
  ctxt_read_init_fini_array (String
"", String
".fini_array",Word64
a0,t
si) = Word64 -> t -> m [Word64]
forall t (m :: * -> *).
(MonadState Context m, Integral t) =>
Word64 -> t -> m [Word64]
read_pointers_from_ro_data_section Word64
a0 t
si
  ctxt_read_init_fini_array (String, String, Word64, t)
_                         = [Word64] -> m [Word64]
forall (m :: * -> *) a. Monad m => a -> m a
return []

  read_pointers_from_ro_data_section :: Word64 -> t -> m [Word64]
read_pointers_from_ro_data_section Word64
a0 t
si =
    if t
si t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
8 then
      [Word64] -> m [Word64]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    else do
      Context
ctxt <- m Context
forall s (m :: * -> *). MonadState s m => m s
get
      let ptr :: Maybe Word64
ptr = Context -> Word64 -> Int -> Maybe Word64
read_from_ro_datasection Context
ctxt Word64
a0 (t -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral t
si)
      [Word64]
ptrs <- Word64 -> t -> m [Word64]
read_pointers_from_ro_data_section (Word64
a0Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
8) (t
sit -> t -> t
forall a. Num a => a -> a -> a
-t
8)
      [Word64] -> m [Word64]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Word64] -> m [Word64]) -> [Word64] -> m [Word64]
forall a b. (a -> b) -> a -> b
$ (Maybe Word64 -> Word64
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Word64
ptr)Word64 -> [Word64] -> [Word64]
forall a. a -> [a] -> [a]
:[Word64]
ptrs
      




-- Produce a base file name (without .extension) based on the current entry under consideration
-- If necessary, make the directory
ctxt_base_name :: Int -> StateT Context IO String
ctxt_base_name :: Int -> StateT Context IO String
ctxt_base_name Int
entry = do
  String
dirname  <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_dirname
  String
name     <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_name

  let functions_dirname :: String
functions_dirname = String
dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"functions/"
  IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
False String
functions_dirname      
  let entry_dirname :: String
entry_dirname = String
functions_dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/"
  IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
False String
entry_dirname      
  String -> StateT Context IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> StateT Context IO String)
-> String -> StateT Context IO String
forall a b. (a -> b) -> a -> b
$ String
entry_dirname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name

-- For the current entry under consideration, read indirections producing inds :: IM.IntMap IS.IntSet
-- Per address a set of next addresses (jump targets).
ctxt_init_indirections :: StateT Context IO ()
ctxt_init_indirections :: StateT Context IO ()
ctxt_init_indirections = do
  String
dirname   <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_dirname
  String
name      <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_name
  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
".indirections" 

  --exists <- liftIO $ doesFileExist fname
  --if exists then do
  --  inds <- liftIO $ parse fname
  --  ctxt <- get
  --  put $ ctxt { ctxt_inds = inds }
  --else do
  IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
fname String
""
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Indirections -> Context -> Context
set_ctxt_inds Indirections
forall a. IntMap a
IM.empty
 where
  parse :: String -> IO (IntMap IntSet)
parse String
fname = do
    Either ParseError (IntMap IntSet)
ret0 <- String -> IO (Either ParseError (IntMap IntSet))
parse_indirections String
fname
    case Either ParseError (IntMap IntSet)
ret0 of
      Left ParseError
err   -> String -> IO (IntMap IntSet)
forall a. HasCallStack => String -> a
error (String -> IO (IntMap IntSet)) -> String -> IO (IntMap IntSet)
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
      Right IntMap IntSet
inds -> IntMap IntSet -> IO (IntMap IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap IntSet
inds





-- TODO generate dot only once
ctxt_generate_cfg :: Int -> StateT Context IO (S.Set (Instruction,Int))
ctxt_generate_cfg :: Int -> StateT Context IO (Set (Instruction, Int))
ctxt_generate_cfg Int
entry = do
  -- Generate a CFG, write dot file if no new calls discovered
  Context
ctxt          <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  String
base          <- Int -> StateT Context IO String
ctxt_base_name Int
entry
  let log :: String
log        = String
base String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".log"
  let fname :: String
fname      = String
base String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".dot"
  let pdf :: String
pdf        = String
base String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".pdf"
  let do_pdfs :: Bool
do_pdfs    = Context -> Bool
ctxt_generate_pdfs Context
ctxt
  (Set (Instruction, Int)
new_calls,CFG
g) <- IO (Set (Instruction, Int), CFG)
-> StateT Context IO (Set (Instruction, Int), CFG)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Set (Instruction, Int), CFG)
 -> StateT Context IO (Set (Instruction, Int), CFG))
-> IO (Set (Instruction, Int), CFG)
-> StateT Context IO (Set (Instruction, Int), CFG)
forall a b. (a -> b) -> a -> b
$ Context -> Int -> IO (Set (Instruction, Int), CFG)
cfg_gen Context
ctxt Int
entry

  IntMap CFG
cfgs <- (Context -> IntMap CFG) -> StateT Context IO (IntMap CFG)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap CFG
ctxt_cfgs
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap CFG -> Context -> Context
set_ctxt_cfgs (IntMap CFG -> Context -> Context)
-> IntMap CFG -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int -> CFG -> IntMap CFG -> IntMap CFG
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry CFG
g IntMap CFG
cfgs)

  if Set (Instruction, Int) -> Bool
forall a. Set a -> Bool
S.null Set (Instruction, Int)
new_calls then do
    IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
fname (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> CFG -> String
cfg_to_dot Context
ctxt CFG
g
    if Bool
do_pdfs then do
      IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
callCommand (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"dot -Tpdf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -o " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pdf
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Generated CFG, exported to files: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pdf
    else do
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Generated CFG, exported to file: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname 
    Set (Instruction, Int)
-> StateT Context IO (Set (Instruction, Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Set (Instruction, Int)
new_calls
  else
    Set (Instruction, Int)
-> StateT Context IO (Set (Instruction, Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Set (Instruction, Int)
new_calls

     


ctxt_add_invariants :: Int
-> FInit
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set VerificationCondition
-> Set SStatePart
-> m ()
ctxt_add_invariants Int
entry FInit
finit Invariants
invs Set (NodeInfo, Predicate)
posts Set VerificationCondition
vcs Set SStatePart
sps = do
  IntMap Invariants
all_invs   <- (Context -> IntMap Invariants) -> m (IntMap Invariants)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap Invariants
ctxt_invs
  IntMap (Set (NodeInfo, Predicate))
all_posts  <- (Context -> IntMap (Set (NodeInfo, Predicate)))
-> m (IntMap (Set (NodeInfo, Predicate)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap (Set (NodeInfo, Predicate))
ctxt_posts
  IntMap (Set VerificationCondition)
all_vcs    <- (Context -> IntMap (Set VerificationCondition))
-> m (IntMap (Set VerificationCondition))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap (Set VerificationCondition)
ctxt_vcs
  IntMap FInit
all_finits <- (Context -> IntMap FInit) -> m (IntMap FInit)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap FInit
ctxt_finits
  IntMap (Set SStatePart)
all_sps    <- (Context -> IntMap (Set SStatePart)) -> m (IntMap (Set SStatePart))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> IntMap (Set SStatePart)
ctxt_stateparts

  (Context -> Context) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap Invariants -> Context -> Context
set_ctxt_invs       (IntMap Invariants -> Context -> Context)
-> IntMap Invariants -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int -> Invariants -> IntMap Invariants -> IntMap Invariants
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry Invariants
invs IntMap Invariants
all_invs)
  (Context -> Context) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap (Set (NodeInfo, Predicate)) -> Context -> Context
set_ctxt_posts      (IntMap (Set (NodeInfo, Predicate)) -> Context -> Context)
-> IntMap (Set (NodeInfo, Predicate)) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int
-> Set (NodeInfo, Predicate)
-> IntMap (Set (NodeInfo, Predicate))
-> IntMap (Set (NodeInfo, Predicate))
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry Set (NodeInfo, Predicate)
posts IntMap (Set (NodeInfo, Predicate))
all_posts)
  (Context -> Context) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap (Set VerificationCondition) -> Context -> Context
set_ctxt_vcs        (IntMap (Set VerificationCondition) -> Context -> Context)
-> IntMap (Set VerificationCondition) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int
-> Set VerificationCondition
-> IntMap (Set VerificationCondition)
-> IntMap (Set VerificationCondition)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry Set VerificationCondition
vcs IntMap (Set VerificationCondition)
all_vcs)
  (Context -> Context) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap FInit -> Context -> Context
set_ctxt_finits     (IntMap FInit -> Context -> Context)
-> IntMap FInit -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int -> FInit -> IntMap FInit -> IntMap FInit
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry FInit
finit IntMap FInit
all_finits)
  (Context -> Context) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (IntMap (Set SStatePart) -> Context -> Context
set_ctxt_stateparts (IntMap (Set SStatePart) -> Context -> Context)
-> IntMap (Set SStatePart) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Int
-> Set SStatePart
-> IntMap (Set SStatePart)
-> IntMap (Set SStatePart)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry Set SStatePart
sps IntMap (Set SStatePart)
all_sps)




ctxt_mk_fcontext :: Int -> StateT Context IO FContext
ctxt_mk_fcontext :: Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  FContext -> StateT Context IO FContext
forall (m :: * -> *) a. Monad m => a -> m a
return (FContext -> StateT Context IO FContext)
-> FContext -> StateT Context IO FContext
forall a b. (a -> b) -> a -> b
$ Context -> Int -> FContext
mk_fcontext Context
ctxt Int
entry

ctxt_generate_invs :: Int -> Invariants -> S.Set (NodeInfo,Predicate) -> S.Set SStatePart -> StateT Context IO ()
ctxt_generate_invs :: Int
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set SStatePart
-> StateT Context IO ()
ctxt_generate_invs Int
entry Invariants
curr_invs Set (NodeInfo, Predicate)
curr_posts Set SStatePart
curr_sps = do
  -- Generate invariants
  Context
ctxt  <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let get_max_time :: Int
get_max_time         = Context -> Int
ctxt_max_time Context
ctxt
  let get_max_time_minutes :: Int
get_max_time_minutes = Int
get_max_time Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
60000000

  FContext
fctxt    <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
  let finit :: FInit
finit = FContext -> FInit
f_init FContext
fctxt
  let f :: String
f     = Context -> Int -> String
function_name_of_entry (FContext -> Context
f_ctxt FContext
fctxt) (FContext -> Int
f_entry FContext
fctxt)

  
  -- when (finit /= init_finit) $ to_out $ "Function initialisation: " ++ show finit

  -- let a       = acode_simp $ cfg_to_acode g 0 IS.empty
  CFG
g          <- (Context -> CFG) -> StateT Context IO CFG
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Maybe CFG -> CFG
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe CFG -> CFG) -> (Context -> Maybe CFG) -> Context -> CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntMap CFG -> Maybe CFG
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap CFG -> Maybe CFG)
-> (Context -> IntMap CFG) -> Context -> Maybe CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> IntMap CFG
ctxt_cfgs)
  let p :: Predicate
p       = FContext
-> String
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set SStatePart
-> Predicate
init_pred FContext
fctxt String
f Invariants
curr_invs Set (NodeInfo, Predicate)
curr_posts Set SStatePart
curr_sps

  Maybe (Invariants, Set VerificationCondition)
result  <- IO (Maybe (Invariants, Set VerificationCondition))
-> StateT
     Context IO (Maybe (Invariants, Set VerificationCondition))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Int
-> IO (Invariants, Set VerificationCondition)
-> IO (Maybe (Invariants, Set VerificationCondition))
forall a. Int -> IO a -> IO (Maybe a)
timeout Int
get_max_time (IO (Invariants, Set VerificationCondition)
 -> IO (Maybe (Invariants, Set VerificationCondition)))
-> IO (Invariants, Set VerificationCondition)
-> IO (Maybe (Invariants, Set VerificationCondition))
forall a b. (a -> b) -> a -> b
$ (Invariants, Set VerificationCondition)
-> IO (Invariants, Set VerificationCondition)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Invariants, Set VerificationCondition)
 -> IO (Invariants, Set VerificationCondition))
-> (Invariants, Set VerificationCondition)
-> IO (Invariants, Set VerificationCondition)
forall a b. (a -> b) -> a -> b
$! FContext
-> CFG
-> Int
-> Predicate
-> (Invariants, Set VerificationCondition)
forall ctxt pred.
Propagator ctxt pred =>
ctxt
-> CFG -> Int -> pred -> (IntMap pred, Set VerificationCondition)
do_prop FContext
fctxt CFG
g Int
0 Predicate
p) -- TODO always 0?

  case Maybe (Invariants, Set VerificationCondition)
result of
    Maybe (Invariants, Set VerificationCondition)
Nothing         -> do
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": time out of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
get_max_time_minutes String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" minutes reached."
      Int
-> FInit
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set VerificationCondition
-> Set SStatePart
-> StateT Context IO ()
forall (m :: * -> *).
MonadState Context m =>
Int
-> FInit
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set VerificationCondition
-> Set SStatePart
-> m ()
ctxt_add_invariants Int
entry FInit
finit Invariants
forall a. IntMap a
IM.empty Set (NodeInfo, Predicate)
forall a. Set a
S.empty Set VerificationCondition
forall a. Set a
S.empty Set SStatePart
forall a. Set a
S.empty
    Just (Invariants
invs,Set VerificationCondition
vcs) -> do
      let blocks :: [Int]
blocks  = IntMap [Int] -> [Int]
forall a. IntMap a -> [Int]
IM.keys (IntMap [Int] -> [Int]) -> IntMap [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Int]
cfg_blocks CFG
g
      [((NodeInfo, Predicate), Set VerificationCondition)]
postss     <- [Maybe ((NodeInfo, Predicate), Set VerificationCondition)]
-> [((NodeInfo, Predicate), Set VerificationCondition)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ((NodeInfo, Predicate), Set VerificationCondition)]
 -> [((NodeInfo, Predicate), Set VerificationCondition)])
-> StateT
     Context
     IO
     [Maybe ((NodeInfo, Predicate), Set VerificationCondition)]
-> StateT
     Context IO [((NodeInfo, Predicate), Set VerificationCondition)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int
 -> StateT
      Context
      IO
      (Maybe ((NodeInfo, Predicate), Set VerificationCondition)))
-> [Int]
-> StateT
     Context
     IO
     [Maybe ((NodeInfo, Predicate), Set VerificationCondition)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FContext
-> CFG
-> Invariants
-> Int
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
get_post FContext
fctxt CFG
g Invariants
invs) [Int]
blocks
      let posts :: Set (NodeInfo, Predicate)
posts   = [(NodeInfo, Predicate)] -> Set (NodeInfo, Predicate)
forall a. Ord a => [a] -> Set a
S.fromList ([(NodeInfo, Predicate)] -> Set (NodeInfo, Predicate))
-> [(NodeInfo, Predicate)] -> Set (NodeInfo, Predicate)
forall a b. (a -> b) -> a -> b
$ (((NodeInfo, Predicate), Set VerificationCondition)
 -> (NodeInfo, Predicate))
-> [((NodeInfo, Predicate), Set VerificationCondition)]
-> [(NodeInfo, Predicate)]
forall a b. (a -> b) -> [a] -> [b]
map ((NodeInfo, Predicate), Set VerificationCondition)
-> (NodeInfo, Predicate)
forall a b. (a, b) -> a
fst [((NodeInfo, Predicate), Set VerificationCondition)]
postss
      let vcs' :: Set VerificationCondition
vcs'    = [Set VerificationCondition] -> Set VerificationCondition
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set VerificationCondition] -> Set VerificationCondition)
-> [Set VerificationCondition] -> Set VerificationCondition
forall a b. (a -> b) -> a -> b
$ (((NodeInfo, Predicate), Set VerificationCondition)
 -> Set VerificationCondition)
-> [((NodeInfo, Predicate), Set VerificationCondition)]
-> [Set VerificationCondition]
forall a b. (a -> b) -> [a] -> [b]
map ((NodeInfo, Predicate), Set VerificationCondition)
-> Set VerificationCondition
forall a b. (a, b) -> b
snd [((NodeInfo, Predicate), Set VerificationCondition)]
postss 
      Int
-> FInit
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set VerificationCondition
-> Set SStatePart
-> StateT Context IO ()
forall (m :: * -> *).
MonadState Context m =>
Int
-> FInit
-> Invariants
-> Set (NodeInfo, Predicate)
-> Set VerificationCondition
-> Set SStatePart
-> m ()
ctxt_add_invariants Int
entry FInit
finit Invariants
invs Set (NodeInfo, Predicate)
posts (Set VerificationCondition
-> Set VerificationCondition -> Set VerificationCondition
forall a. Ord a => Set a -> Set a -> Set a
S.union Set VerificationCondition
vcs Set VerificationCondition
vcs') (Set SStatePart -> Set SStatePart -> Set SStatePart
forall a. Ord a => Set a -> Set a -> Set a
S.union Set SStatePart
curr_sps (Set SStatePart -> Set SStatePart)
-> Set SStatePart -> Set SStatePart
forall a b. (a -> b) -> a -> b
$ Invariants -> Set (NodeInfo, Predicate) -> Set SStatePart
gather_stateparts Invariants
invs Set (NodeInfo, Predicate)
posts)
 where
  get_post :: FContext -> CFG -> Invariants -> Int -> StateT Context IO (Maybe ((NodeInfo,Predicate),VCS))
  get_post :: FContext
-> CFG
-> Invariants
-> Int
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
get_post FContext
fctxt CFG
g Invariants
invs Int
b = do
    let ctxt :: Context
ctxt = FContext -> Context
f_ctxt FContext
fctxt
    if CFG -> Int -> Bool
is_end_node CFG
g Int
b then do
      let (Predicate
q,Set VerificationCondition
vcs') = Identity (Predicate, Set VerificationCondition)
-> (Predicate, Set VerificationCondition)
forall a. Identity a -> a
runIdentity (Identity (Predicate, Set VerificationCondition)
 -> (Predicate, Set VerificationCondition))
-> Identity (Predicate, Set VerificationCondition)
-> (Predicate, Set VerificationCondition)
forall a b. (a -> b) -> a -> b
$ StateT (Predicate, Set VerificationCondition) Identity ()
-> (Predicate, Set VerificationCondition)
-> Identity (Predicate, Set VerificationCondition)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (FContext
-> CFG
-> Int
-> StateT (Predicate, Set VerificationCondition) Identity ()
do_tau FContext
fctxt CFG
g Int
b) (String -> Invariants -> Int -> Predicate
forall p. String -> IntMap p -> Int -> p
im_lookup (String
"B.) Block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in invs") Invariants
invs Int
b, Set VerificationCondition
forall a. Set a
S.empty)
      Maybe ((NodeInfo, Predicate), Set VerificationCondition)
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ((NodeInfo, Predicate), Set VerificationCondition)
 -> StateT
      Context
      IO
      (Maybe ((NodeInfo, Predicate), Set VerificationCondition)))
-> Maybe ((NodeInfo, Predicate), Set VerificationCondition)
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate), Set VerificationCondition)
-> Maybe ((NodeInfo, Predicate), Set VerificationCondition)
forall a. a -> Maybe a
Just ((Context -> CFG -> Int -> NodeInfo
node_info_of Context
ctxt CFG
g Int
b,Predicate
q),Set VerificationCondition
vcs')
    else
      Maybe ((NodeInfo, Predicate), Set VerificationCondition)
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ((NodeInfo, Predicate), Set VerificationCondition)
 -> StateT
      Context
      IO
      (Maybe ((NodeInfo, Predicate), Set VerificationCondition)))
-> Maybe ((NodeInfo, Predicate), Set VerificationCondition)
-> StateT
     Context
     IO
     (Maybe ((NodeInfo, Predicate), Set VerificationCondition))
forall a b. (a -> b) -> a -> b
$ Maybe ((NodeInfo, Predicate), Set VerificationCondition)
forall a. Maybe a
Nothing

  -- do one more tau-transformation on the node, as the stored invariant is a 
  -- precondition (not a postcondition) of the node.
  do_tau :: FContext -> CFG -> Int -> State (Predicate,VCS) ()
  do_tau :: FContext
-> CFG
-> Int
-> StateT (Predicate, Set VerificationCondition) Identity ()
do_tau FContext
fctxt CFG
g Int
b = ((Predicate, Set VerificationCondition)
 -> (Predicate, Set VerificationCondition))
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Predicate, Set VerificationCondition)
  -> (Predicate, Set VerificationCondition))
 -> StateT (Predicate, Set VerificationCondition) Identity ())
-> ((Predicate, Set VerificationCondition)
    -> (Predicate, Set VerificationCondition))
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall a b. (a -> b) -> a -> b
$ (FContext
-> [Instruction]
-> Maybe [Instruction]
-> Predicate
-> (Predicate, Set VerificationCondition)
forall ctxt pred.
Propagator ctxt pred =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> pred
-> (pred, Set VerificationCondition)
tau FContext
fctxt (CFG -> Int -> [Instruction]
fetch_block CFG
g Int
b) Maybe [Instruction]
forall a. Maybe a
Nothing (Predicate -> (Predicate, Set VerificationCondition))
-> ((Predicate, Set VerificationCondition) -> Predicate)
-> (Predicate, Set VerificationCondition)
-> (Predicate, Set VerificationCondition)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Predicate, Set VerificationCondition) -> Predicate
forall a b. (a, b) -> a
fst)







ctxt_del_entry :: Int -> StateT Context IO ()
ctxt_del_entry :: Int -> StateT Context IO ()
ctxt_del_entry Int
entry = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Graph -> Context -> Context
set_ctxt_entries (Graph -> Context -> Context) -> Graph -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Graph -> Int -> Graph
graph_delete (Context -> Graph
ctxt_entries Context
ctxt) Int
entry

ctxt_add_call :: Int -> VerificationResult -> StateT Context IO ()
ctxt_add_call Int
entry VerificationResult
verified = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  FContext
fctxt <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
  let calls :: IntMap FReturnBehavior
calls       = Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt
  let dirname :: String
dirname     = Context -> String
ctxt_dirname Context
ctxt
  let name :: String
name        = Context -> String
ctxt_name Context
ctxt
  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
".calls"

  (FInit
_,Invariants
invs,Set (NodeInfo, Predicate)
posts,Set SStatePart
_) <- Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
entry
  
  (FReturnBehavior
ret,String
msg) <-
    if ((NodeInfo -> Bool) -> Set NodeInfo -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
(==) NodeInfo
UnresolvedIndirection) (Set NodeInfo -> Bool) -> Set NodeInfo -> Bool
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate) -> NodeInfo)
-> Set (NodeInfo, Predicate) -> Set NodeInfo
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (NodeInfo, Predicate) -> NodeInfo
forall a b. (a, b) -> a
fst Set (NodeInfo, Predicate)
posts) Bool -> Bool -> Bool
|| VerificationResult
verified VerificationResult -> [VerificationResult] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VerificationResult
VerificationSuccesWithAssumptions,VerificationResult
VerificationSuccess] then
      (FReturnBehavior, String)
-> StateT Context IO (FReturnBehavior, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (FReturnBehavior
UnknownRetBehavior, String
"unknown.")
    else if (NodeInfo -> Bool) -> Set NodeInfo -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
(==) NodeInfo
Terminal) (Set NodeInfo -> Bool) -> Set NodeInfo -> Bool
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate) -> NodeInfo)
-> Set (NodeInfo, Predicate) -> Set NodeInfo
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (NodeInfo, Predicate) -> NodeInfo
forall a b. (a, b) -> a
fst Set (NodeInfo, Predicate)
posts then
      (FReturnBehavior, String)
-> StateT Context IO (FReturnBehavior, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (FReturnBehavior
Terminating, String
"always terminating.")
    else let q :: Predicate
q = FContext -> [Predicate] -> Predicate
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> [Sstate v p] -> Sstate v p
supremum FContext
fctxt ([Predicate] -> Predicate) -> [Predicate] -> Predicate
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate) -> Predicate)
-> [(NodeInfo, Predicate)] -> [Predicate]
forall a b. (a -> b) -> [a] -> [b]
map (NodeInfo, Predicate) -> Predicate
forall a b. (a, b) -> b
snd ([(NodeInfo, Predicate)] -> [Predicate])
-> [(NodeInfo, Predicate)] -> [Predicate]
forall a b. (a -> b) -> a -> b
$ Set (NodeInfo, Predicate) -> [(NodeInfo, Predicate)]
forall a. Set a -> [a]
S.toList (Set (NodeInfo, Predicate) -> [(NodeInfo, Predicate)])
-> Set (NodeInfo, Predicate) -> [(NodeInfo, Predicate)]
forall a b. (a -> b) -> a -> b
$ ((NodeInfo, Predicate) -> Bool)
-> Set (NodeInfo, Predicate) -> Set (NodeInfo, Predicate)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
(==) NodeInfo
Normal (NodeInfo -> Bool)
-> ((NodeInfo, Predicate) -> NodeInfo)
-> (NodeInfo, Predicate)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NodeInfo, Predicate) -> NodeInfo
forall a b. (a, b) -> a
fst) (Set (NodeInfo, Predicate) -> Set (NodeInfo, Predicate))
-> Set (NodeInfo, Predicate) -> Set (NodeInfo, Predicate)
forall a b. (a -> b) -> a -> b
$ Set (NodeInfo, Predicate)
posts in
      (FReturnBehavior, String)
-> StateT Context IO (FReturnBehavior, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Predicate -> FReturnBehavior
ReturningWith Predicate
q, String
"normally returning.")

  (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IntMap FReturnBehavior -> Context -> Context
set_ctxt_calls (Int
-> FReturnBehavior
-> IntMap FReturnBehavior
-> IntMap FReturnBehavior
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
entry FReturnBehavior
ret (IntMap FReturnBehavior -> IntMap FReturnBehavior)
-> IntMap FReturnBehavior -> IntMap FReturnBehavior
forall a b. (a -> b) -> a -> b
$ IntMap FReturnBehavior
calls)
  String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Function at entry: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
showHex Int
entry String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" analyzed, return behavior is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg






ctxt_analyze_unresolved_indirections :: Int -> StateT Context IO Bool
ctxt_analyze_unresolved_indirections :: Int -> StateT Context IO Bool
ctxt_analyze_unresolved_indirections Int
entry = do
  Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get

  (FInit
finit,Invariants
invs,Set (NodeInfo, Predicate)
posts,Set SStatePart
_) <- Int
-> StateT
     Context
     IO
     (FInit, Invariants, Set (NodeInfo, Predicate), Set SStatePart)
ctxt_get_curr_posts Int
entry
  let f :: String
f        = Context -> Int -> String
function_name_of_entry Context
ctxt Int
entry
  let g :: CFG
g        =  Context -> IntMap CFG
ctxt_cfgs Context
ctxt IntMap CFG -> Int -> CFG
forall a. IntMap a -> Int -> a
IM.! Int
entry

  let bs :: [Int]
bs = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Int
b -> Context -> CFG -> Int -> NodeInfo
node_info_of Context
ctxt CFG
g Int
b NodeInfo -> NodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
== NodeInfo
UnresolvedIndirection) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ IntMap [Int] -> [Int]
forall a. IntMap a -> [Int]
IM.keys (IntMap [Int] -> [Int]) -> IntMap [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Int]
cfg_blocks CFG
g
  if [Int]
bs [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then do
    String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"No unresolved indirections."
    Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  else if Invariants -> Bool
forall a. IntMap a -> Bool
IM.null Invariants
invs then do
    -- time out
    Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  else do
    [Bool]
results <- [Int]
-> (Int -> StateT Context IO Bool) -> StateT Context IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
bs ((Int -> StateT Context IO Bool) -> StateT Context IO [Bool])
-> (Int -> StateT Context IO Bool) -> StateT Context IO [Bool]
forall a b. (a -> b) -> a -> b
$ String -> CFG -> Invariants -> Int -> StateT Context IO Bool
forall p. p -> CFG -> Invariants -> Int -> StateT Context IO Bool
try_to_resolve_indirection String
f CFG
g Invariants
invs
    Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT Context IO Bool) -> Bool -> StateT Context IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
not [Bool]
results -- prevent lazy execution
 where
  try_to_resolve_indirection :: p -> CFG -> Invariants -> Int -> StateT Context IO Bool
try_to_resolve_indirection p
f CFG
g Invariants
invs Int
b = do
    Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
    FContext
fctxt <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
    Int
max_tries <- (Context -> Int) -> StateT Context IO Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Int
ctxt_max_jump_table_size

    String
dirname   <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_dirname
    String
name      <- (Context -> String) -> StateT Context IO String
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> String
ctxt_name
    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
".indirections" 

    let i :: Instruction
i                 = [Instruction] -> Instruction
forall a. [a] -> a
last (CFG -> Int -> [Instruction]
fetch_block CFG
g Int
b)
    let [GenericOperand Register
trgt]            = Instruction -> [GenericOperand Register]
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation
-> [GenericOperand storage]
Instr.srcs Instruction
i
    let p :: Predicate
p                 = String -> Invariants -> Int -> Predicate
forall p. String -> IntMap p -> Int -> p
im_lookup (String
"A.) Block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in invs") Invariants
invs Int
b


    case Int -> FlagStatus -> Maybe (GenericOperand Register, Word64)
forall a.
Integral a =>
a -> FlagStatus -> Maybe (GenericOperand Register, Word64)
flagstatus_to_tries Int
max_tries (Predicate -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Predicate
p) of
      Maybe (GenericOperand Register, Word64)
Nothing -> String
-> p
-> CFG
-> Int
-> Predicate
-> Instruction
-> GenericOperand Register
-> StateT Context IO Bool
forall storage prefix opcode annotation p.
(Show storage, Show prefix, Show opcode, Show annotation) =>
String
-> p
-> CFG
-> Int
-> Predicate
-> GenericInstruction
     AddressWord64 storage prefix opcode annotation
-> GenericOperand Register
-> StateT Context IO Bool
try_to_resolve_from_invariant String
fname p
f CFG
g Int
b Predicate
p Instruction
i GenericOperand Register
trgt
      Just (GenericOperand Register
op1,Word64
n) -> do
        let values1 :: [Maybe (Set ResolvedJumpTarget)]
values1 = (Word64 -> Maybe (Set ResolvedJumpTarget))
-> [Word64] -> [Maybe (Set ResolvedJumpTarget)]
forall a b. (a -> b) -> [a] -> [b]
map (\Word64
n -> State
  (Predicate, Set VerificationCondition)
  (Maybe (Set ResolvedJumpTarget))
-> Predicate -> Maybe (Set ResolvedJumpTarget)
forall v p a.
State (Sstate v p, Set VerificationCondition) a -> Sstate v p -> a
evalSstate (FContext
-> p
-> Word64
-> CFG
-> Int
-> GenericOperand Register
-> GenericOperand Register
-> Word64
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
forall i p p.
Integral i =>
FContext
-> p
-> p
-> CFG
-> Int
-> GenericOperand Register
-> GenericOperand Register
-> i
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
try FContext
fctxt p
f (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) CFG
g Int
b GenericOperand Register
op1 GenericOperand Register
trgt Word64
n) Predicate
p) [Word64
0..Word64
n]
        if [Maybe (Set ResolvedJumpTarget)]
values1 [Maybe (Set ResolvedJumpTarget)]
-> [Maybe (Set ResolvedJumpTarget)] -> Bool
forall a. Eq a => a -> a -> Bool
== [] Bool -> Bool -> Bool
|| (Maybe (Set ResolvedJumpTarget) -> Bool)
-> [Maybe (Set ResolvedJumpTarget)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (Set ResolvedJumpTarget)
-> Maybe (Set ResolvedJumpTarget) -> Bool
forall a. Eq a => a -> a -> Bool
(==) Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing) [Maybe (Set ResolvedJumpTarget)]
values1 then
          String
-> p
-> CFG
-> Int
-> Predicate
-> Instruction
-> GenericOperand Register
-> StateT Context IO Bool
forall storage prefix opcode annotation p.
(Show storage, Show prefix, Show opcode, Show annotation) =>
String
-> p
-> CFG
-> Int
-> Predicate
-> GenericInstruction
     AddressWord64 storage prefix opcode annotation
-> GenericOperand Register
-> StateT Context IO Bool
try_to_resolve_from_invariant String
fname p
f CFG
g Int
b Predicate
p Instruction
i GenericOperand Register
trgt
        else if (Maybe (Set ResolvedJumpTarget) -> Bool)
-> [Maybe (Set ResolvedJumpTarget)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe (Set ResolvedJumpTarget) -> Bool
is_jump_table_entry [Maybe (Set ResolvedJumpTarget)]
values1 then do
          let trgts :: [Word64]
trgts = (Maybe (Set ResolvedJumpTarget) -> Word64)
-> [Maybe (Set ResolvedJumpTarget)] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map (Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Word64)
-> (Maybe (Set ResolvedJumpTarget) -> Word64)
-> Maybe (Set ResolvedJumpTarget)
-> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResolvedJumpTarget -> Word64
get_immediate (ResolvedJumpTarget -> Word64)
-> (Maybe (Set ResolvedJumpTarget) -> ResolvedJumpTarget)
-> Maybe (Set ResolvedJumpTarget)
-> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ResolvedJumpTarget -> ResolvedJumpTarget
forall a. Set a -> a
S.findMin (Set ResolvedJumpTarget -> ResolvedJumpTarget)
-> (Maybe (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget)
-> Maybe (Set ResolvedJumpTarget)
-> ResolvedJumpTarget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget
forall a. HasCallStack => Maybe a -> a
fromJust) [Maybe (Set ResolvedJumpTarget)]
values1
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Resolved indirection at block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Instruction = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Instruction -> String
forall a. Show a => a -> String
show Instruction
i
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Operand " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GenericOperand Register -> String
forall a. Show a => a -> String
show GenericOperand Register
trgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" evaluates to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Word64] -> String
forall a. (Integral a, Show a) => [a] -> String
showHex_list ([Word64] -> [Word64]
forall a. Eq a => [a] -> [a]
nub [Word64]
trgts)
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Because of bounded jump table access: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FlagStatus -> String
forall a. Show a => a -> String
show (Predicate -> FlagStatus
forall v p. Sstate v p -> FlagStatus
sflags Predicate
p)
          String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Updated file: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname

          Indirections
inds <- (Context -> Indirections) -> StateT Context IO Indirections
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Indirections
ctxt_inds

          let tbl :: JumpTable
tbl = GenericOperand Register
-> Int -> GenericOperand Register -> IntMap Word64 -> JumpTable
JumpTable GenericOperand Register
op1 (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n) GenericOperand Register
trgt ([(Int, Word64)] -> IntMap Word64
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, Word64)] -> IntMap Word64)
-> [(Int, Word64)] -> IntMap Word64
forall a b. (a -> b) -> a -> b
$ [Int] -> [Word64] -> [(Int, Word64)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n] [Word64]
trgts)
          IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
appendFile String
fname (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex (Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ JumpTable -> String
forall a. Show a => a -> String
show JumpTable
tbl String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

          let inds' :: Indirections
inds' = Int -> Indirection -> Indirections -> Indirections
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) (JumpTable -> Indirection
Indirection_JumpTable JumpTable
tbl) Indirections
inds -- TODO check if already exists
          (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Indirections -> Context -> Context
set_ctxt_inds Indirections
inds'

          Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else
          String -> StateT Context IO Bool
forall a. HasCallStack => String -> a
error (String -> StateT Context IO Bool)
-> String -> StateT Context IO Bool
forall a b. (a -> b) -> a -> b
$ (String, [Maybe (Set ResolvedJumpTarget)]) -> String
forall a. Show a => a -> String
show (String
"resolving:",[Maybe (Set ResolvedJumpTarget)]
values1)


  try_to_resolve_from_invariant :: String
-> p
-> CFG
-> Int
-> Predicate
-> GenericInstruction
     AddressWord64 storage prefix opcode annotation
-> GenericOperand Register
-> StateT Context IO Bool
try_to_resolve_from_invariant String
fname p
f CFG
g Int
b Predicate
p GenericInstruction AddressWord64 storage prefix opcode annotation
i GenericOperand Register
trgt = do
    Context
ctxt <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
    FContext
fctxt <- Int -> StateT Context IO FContext
ctxt_mk_fcontext Int
entry
    let values0 :: Maybe (Set ResolvedJumpTarget)
values0 = State
  (Predicate, Set VerificationCondition)
  (Maybe (Set ResolvedJumpTarget))
-> Predicate -> Maybe (Set ResolvedJumpTarget)
forall v p a.
State (Sstate v p, Set VerificationCondition) a -> Sstate v p -> a
evalSstate (FContext
-> p
-> CFG
-> Int
-> GenericOperand Register
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
forall p.
FContext
-> p
-> CFG
-> Int
-> GenericOperand Register
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
try' FContext
fctxt p
f CFG
g Int
b GenericOperand Register
trgt) Predicate
p
    if Maybe (Set ResolvedJumpTarget)
values0 Maybe (Set ResolvedJumpTarget)
-> Maybe (Set ResolvedJumpTarget) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (Set ResolvedJumpTarget)
forall a. Maybe a
Nothing then do
      let value :: Set ResolvedJumpTarget
value = Maybe (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Set ResolvedJumpTarget)
values0
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Resolved indirection at block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Instruction = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GenericInstruction AddressWord64 storage prefix opcode annotation
-> String
forall a. Show a => a -> String
show GenericInstruction AddressWord64 storage prefix opcode annotation
i
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Operand " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GenericOperand Register -> String
forall a. Show a => a -> String
show GenericOperand Register
trgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" evaluates to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set ResolvedJumpTarget -> String
forall a. Show a => a -> String
show Set ResolvedJumpTarget
value
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"State:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Predicate -> String
forall a. Show a => a -> String
show Predicate
p
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Updated file: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname
      IO () -> StateT Context IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
appendFile String
fname (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex (GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof GenericInstruction AddressWord64 storage prefix opcode annotation
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Indirection -> String
forall a. Show a => a -> String
show (Set ResolvedJumpTarget -> Indirection
Indirection_Resolved Set ResolvedJumpTarget
value) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

      Indirections
inds <- (Context -> Indirections) -> StateT Context IO Indirections
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Indirections
ctxt_inds
      let inds' :: Indirections
inds' = Int -> Indirection -> Indirections -> Indirections
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof GenericInstruction AddressWord64 storage prefix opcode annotation
i) (Set ResolvedJumpTarget -> Indirection
Indirection_Resolved Set ResolvedJumpTarget
value) Indirections
inds -- TODO check if already exists
      (Context -> Context) -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context IO ())
-> (Context -> Context) -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Indirections -> Context -> Context
set_ctxt_inds Indirections
inds'
      Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    else do
      String -> StateT Context IO ()
to_out (String -> StateT Context IO ()) -> String -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unresolved block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ GenericInstruction AddressWord64 storage prefix opcode annotation
-> String
forall a. Show a => a -> String
show GenericInstruction AddressWord64 storage prefix opcode annotation
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Predicate -> String
forall a. Show a => a -> String
show Predicate
p
      Bool -> StateT Context IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False


  flagstatus_to_tries :: a -> FlagStatus -> Maybe (GenericOperand Register, Word64)
flagstatus_to_tries a
max_tries (FS_CMP (Just Bool
True) GenericOperand Register
op1 (Immediate Word64
n)) = if Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
max_tries then (GenericOperand Register, Word64)
-> Maybe (GenericOperand Register, Word64)
forall a. a -> Maybe a
Just (GenericOperand Register
op1,Word64
n) else Maybe (GenericOperand Register, Word64)
forall a. Maybe a
Nothing
  flagstatus_to_tries a
max_tries FlagStatus
_ = Maybe (GenericOperand Register, Word64)
forall a. Maybe a
Nothing


  is_jump_table_entry :: Maybe (Set ResolvedJumpTarget) -> Bool
is_jump_table_entry Maybe (Set ResolvedJumpTarget)
Nothing      = Bool
False
  is_jump_table_entry (Just Set ResolvedJumpTarget
trgts) = Set ResolvedJumpTarget -> Int
forall a. Set a -> Int
S.size Set ResolvedJumpTarget
trgts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& (ResolvedJumpTarget -> Bool) -> Set ResolvedJumpTarget -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ResolvedJumpTarget -> Bool
is_immediate Set ResolvedJumpTarget
trgts
  is_immediate :: ResolvedJumpTarget -> Bool
is_immediate (ImmediateAddress Word64
_) = Bool
True
  is_immediate ResolvedJumpTarget
_                    = Bool
False
  get_immediate :: ResolvedJumpTarget -> Word64
get_immediate (ImmediateAddress Word64
a) = Word64
a

  -- write an immediate value to operand op1, then run symbolic exection to see if
  -- after executing a block the target-operand is an immediate value as well.
  try :: FContext
-> p
-> p
-> CFG
-> Int
-> GenericOperand Register
-> GenericOperand Register
-> i
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
try FContext
fctxt p
f p
i_a CFG
g Int
blockId GenericOperand Register
op1 GenericOperand Register
trgt i
n = do
    FContext
-> Bool
-> GenericOperand Register
-> SValue
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Bool
-> GenericOperand Register
-> v
-> State (Sstate v p, Set VerificationCondition) ()
swrite_operand FContext
fctxt Bool
False GenericOperand Register
op1 (FContext -> i -> SValue
forall ctxt v p i.
(SymbolicExecutable ctxt v p, Integral i) =>
ctxt -> i -> v
simmediate FContext
fctxt i
n)
    FContext
-> p
-> CFG
-> Int
-> GenericOperand Register
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
forall p.
FContext
-> p
-> CFG
-> Int
-> GenericOperand Register
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
try' FContext
fctxt p
f CFG
g Int
blockId GenericOperand Register
trgt

  try' :: FContext
-> p
-> CFG
-> Int
-> GenericOperand Register
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
try' FContext
fctxt p
f CFG
g Int
blockId GenericOperand Register
trgt = do
    let ctxt :: Context
ctxt   = FContext -> Context
f_ctxt FContext
fctxt
    let instrs :: [Instruction]
instrs = CFG -> Int -> [Instruction]
fetch_block CFG
g Int
blockId
    ((Predicate, Set VerificationCondition)
 -> (Predicate, Set VerificationCondition))
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Predicate, Set VerificationCondition)
  -> (Predicate, Set VerificationCondition))
 -> StateT (Predicate, Set VerificationCondition) Identity ())
-> ((Predicate, Set VerificationCondition)
    -> (Predicate, Set VerificationCondition))
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall a b. (a -> b) -> a -> b
$ (FContext
-> [Instruction]
-> Maybe [Instruction]
-> Predicate
-> (Predicate, Set VerificationCondition)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> [Instruction]
-> Maybe [Instruction]
-> Sstate v p
-> (Sstate v p, Set VerificationCondition)
sexec_block FContext
fctxt ([Instruction] -> [Instruction]
forall a. [a] -> [a]
init [Instruction]
instrs) Maybe [Instruction]
forall a. Maybe a
Nothing (Predicate -> (Predicate, Set VerificationCondition))
-> ((Predicate, Set VerificationCondition) -> Predicate)
-> (Predicate, Set VerificationCondition)
-> (Predicate, Set VerificationCondition)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Predicate, Set VerificationCondition) -> Predicate
forall a b. (a, b) -> a
fst)
    FContext
-> Instruction
-> StateT (Predicate, Set VerificationCondition) Identity ()
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> Instruction -> State (Sstate v p, Set VerificationCondition) ()
sset_rip FContext
fctxt ([Instruction] -> Instruction
forall a. [a] -> a
last [Instruction]
instrs)
    SValue
val <- FContext
-> String
-> GenericOperand Register
-> State (Predicate, Set VerificationCondition) SValue
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt
-> String
-> GenericOperand Register
-> State (Sstate v p, Set VerificationCondition) v
sread_operand FContext
fctxt String
"indirection resolving" GenericOperand Register
trgt
    Maybe (Set ResolvedJumpTarget)
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Set ResolvedJumpTarget)
 -> State
      (Predicate, Set VerificationCondition)
      (Maybe (Set ResolvedJumpTarget)))
-> Maybe (Set ResolvedJumpTarget)
-> State
     (Predicate, Set VerificationCondition)
     (Maybe (Set ResolvedJumpTarget))
forall a b. (a -> b) -> a -> b
$ FContext -> SValue -> Maybe (Set ResolvedJumpTarget)
forall ctxt v p.
SymbolicExecutable ctxt v p =>
ctxt -> v -> Maybe (Set ResolvedJumpTarget)
stry_jump_targets FContext
fctxt SValue
val