{-# LANGUAGE PartialTypeSignatures, Strict #-}

{-|
Module      : CFG_Gen
Description : Contains functions pertaining to control flow graph generation.
-}

module Pass.CFG_Gen (
   cfg_gen,
   cfg_to_dot,
   is_end_node,
   node_info_of,
   stepA
 )
 where

import Algorithm.SCC
import Analysis.Context
import Analysis.Propagation
import Analysis.SymbolicExecution
import Base
import Data.ControlFlow
import Data.MachineState
import Data.SimplePred
import X86.Conventions
import Data.Binary


import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set as S
import qualified Data.Map as M
import Data.Either (fromRight,fromLeft,partitionEithers)
import Data.Maybe (fromJust)
import Data.List
import Data.List.Split (chunksOf)
import Data.Word (Word64)
import Control.Monad ((>=>))
import Debug.Trace
import Numeric (readHex)
import GHC.Float.RealFracMethods (floorDoubleInt,int2Double)
import X86.Opcode (isRet, isCall, isCondJump, isJump, isHalt)
import qualified X86.Instruction as X86
import Typeclasses.HasSize (sizeof)
import Typeclasses.HasAddress (addressof)
import qualified Generic.Instruction as Instr

-- the algorithm below has been formally proven correct in Isabelle/HOL
split_graph' :: Key -> CFG -> Maybe CFG
split_graph' Key
a CFG
g = 
  case Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g) of
    Maybe Key
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
    Just Key
blockID ->
      case Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID (CFG -> IntMap [Key]
cfg_blocks CFG
g) of
        Maybe [Key]
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
        Just [Key]
block ->
          if [Key] -> Key
forall a. [a] -> a
last [Key]
block Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
/= Key
a then do
            let ([Key]
begin,[Key]
end) = (Key -> Bool) -> [Key] -> ([Key], [Key])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
(==) Key
a) [Key]
block
            let f :: Key
f           = CFG -> Key
cfg_fresh CFG
g
            let blocks' :: IntMap [Key]
blocks'     = Key -> [Key] -> IntMap [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
blockID ([Key]
begin[Key] -> [Key] -> [Key]
forall a. [a] -> [a] -> [a]
++ [Key
a]) (IntMap [Key] -> IntMap [Key]) -> IntMap [Key] -> IntMap [Key]
forall a b. (a -> b) -> a -> b
$ Key -> [Key] -> IntMap [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
f ([Key] -> [Key]
forall a. [a] -> [a]
tail [Key]
end) (CFG -> IntMap [Key]
cfg_blocks CFG
g)
            let edges' :: IntMap IntSet
edges'      = Key -> IntSet -> IntMap IntSet -> IntMap IntSet
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
blockID (Key -> IntSet
IS.singleton Key
f) (IntMap IntSet -> IntMap IntSet) -> IntMap IntSet -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ (Key -> Key) -> IntMap IntSet -> IntMap IntSet
forall a. (Key -> Key) -> IntMap a -> IntMap a
IM.mapKeys (\Key
k -> if Key
k Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
blockID then Key
f else Key
k) (CFG -> IntMap IntSet
cfg_edges CFG
g)
            let a_to_b' :: IntMap Key
a_to_b'     = (Key -> Key -> Key) -> IntMap Key -> IntMap Key
forall a b. (Key -> a -> b) -> IntMap a -> IntMap b
IM.mapWithKey (\Key
addr Key
blockID -> if Key
addr Key -> [Key] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Key] -> [Key]
forall a. [a] -> [a]
tail [Key]
end then Key
f else Key
blockID) (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
            let fresh' :: Key
fresh'      = Key
f Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Key
1
            CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ IntMap [Key]
-> IntMap IntSet
-> IntMap Key
-> Key
-> IntMap [Instruction]
-> CFG
CFG IntMap [Key]
blocks' IntMap IntSet
edges' IntMap Key
a_to_b' Key
fresh' IntMap [Instruction]
forall a. IntMap a
IM.empty
          else
            CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return CFG
g

split_graph :: Key -> CFG -> Maybe CFG
split_graph Key
a CFG
g = do
  case Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g) of
    Maybe Key
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
    Just Key
blockID ->
      case Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID (CFG -> IntMap [Key]
cfg_blocks CFG
g) of
        Maybe [Key]
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
        Just [Key]
block ->
          if [Key] -> Key
forall a. [a] -> a
head [Key]
block Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
/= Key
a then do
            let ([Key]
begin,[Key]
end) = (Key -> Bool) -> [Key] -> ([Key], [Key])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
(==) Key
a) [Key]
block
            let f :: Key
f           = CFG -> Key
cfg_fresh CFG
g
            let blocks' :: IntMap [Key]
blocks'     = Key -> [Key] -> IntMap [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
blockID [Key]
begin (IntMap [Key] -> IntMap [Key]) -> IntMap [Key] -> IntMap [Key]
forall a b. (a -> b) -> a -> b
$ Key -> [Key] -> IntMap [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
f [Key]
end  (CFG -> IntMap [Key]
cfg_blocks CFG
g)
            let edges' :: IntMap IntSet
edges'      = Key -> IntSet -> IntMap IntSet -> IntMap IntSet
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
blockID (Key -> IntSet
IS.singleton Key
f) (IntMap IntSet -> IntMap IntSet) -> IntMap IntSet -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ (Key -> Key) -> IntMap IntSet -> IntMap IntSet
forall a. (Key -> Key) -> IntMap a -> IntMap a
IM.mapKeys (\Key
k -> if Key
k Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
blockID then Key
f else Key
k) (CFG -> IntMap IntSet
cfg_edges CFG
g)
            let a_to_b' :: IntMap Key
a_to_b'     = (Key -> Key -> Key) -> IntMap Key -> IntMap Key
forall a b. (Key -> a -> b) -> IntMap a -> IntMap b
IM.mapWithKey (\Key
addr Key
blockID -> if Key
addr Key -> [Key] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Key]
end then Key
f else Key
blockID) (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
            let fresh' :: Key
fresh'      = Key
f Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Key
1
            CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ IntMap [Key]
-> IntMap IntSet
-> IntMap Key
-> Key
-> IntMap [Instruction]
-> CFG
CFG IntMap [Key]
blocks' IntMap IntSet
edges' IntMap Key
a_to_b' Key
fresh' IntMap [Instruction]
forall a. IntMap a
IM.empty
          else
            CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return CFG
g

add_edge_to_graph :: Key -> Key -> CFG -> Maybe CFG
add_edge_to_graph Key
a0 Key
a1 CFG
g = do
  case Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a0 (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g) of
    Maybe Key
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
    Just Key
blockID ->
      case Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID (CFG -> IntMap [Key]
cfg_blocks CFG
g) of
        Maybe [Key]
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
        Just [Key]
block ->
          case Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a1 (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g) of
            Just Key
blockID' -> do
              case Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID' (CFG -> IntMap [Key]
cfg_blocks CFG
g) of
                Maybe [Key]
Nothing -> CFG -> Maybe CFG
forall a. a -> Maybe a
Just CFG
g
                Just [Key]
block' -> do
                  let edges' :: IntMap IntSet
edges' = (Maybe IntSet -> Maybe IntSet)
-> Key -> IntMap IntSet -> IntMap IntSet
forall a. (Maybe a -> Maybe a) -> Key -> IntMap a -> IntMap a
IM.alter (Key -> Maybe IntSet -> Maybe IntSet
add_to_intset Key
blockID') Key
blockID (CFG -> IntMap IntSet
cfg_edges CFG
g)
                  CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ CFG
g { cfg_edges :: IntMap IntSet
cfg_edges = IntMap IntSet
edges' }
            Maybe Key
Nothing -> do
              case Key -> IntMap IntSet -> Maybe IntSet
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockID (CFG -> IntMap IntSet
cfg_edges CFG
g) of
                Maybe IntSet
Nothing -> do
                  let blocks' :: IntMap [Key]
blocks' = (Maybe [Key] -> Maybe [Key]) -> Key -> IntMap [Key] -> IntMap [Key]
forall a. (Maybe a -> Maybe a) -> Key -> IntMap a -> IntMap a
IM.alter (Key -> Maybe [Key] -> Maybe [Key]
forall a. a -> Maybe [a] -> Maybe [a]
append_to_list Key
a1) Key
blockID (CFG -> IntMap [Key]
cfg_blocks CFG
g)
                  let a_to_b' :: IntMap Key
a_to_b' = Key -> Key -> IntMap Key -> IntMap Key
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
a1 Key
blockID (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
                  CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ CFG
g { cfg_blocks :: IntMap [Key]
cfg_blocks = IntMap [Key]
blocks', cfg_addr_to_blockID :: IntMap Key
cfg_addr_to_blockID = IntMap Key
a_to_b' }
                Maybe IntSet
_ -> do
                  let f :: Key
f       = CFG -> Key
cfg_fresh CFG
g
                  let blocks' :: IntMap [Key]
blocks' = Key -> [Key] -> IntMap [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
f [Key
a1] (CFG -> IntMap [Key]
cfg_blocks CFG
g)
                  let edges' :: IntMap IntSet
edges'  = (Maybe IntSet -> Maybe IntSet)
-> Key -> IntMap IntSet -> IntMap IntSet
forall a. (Maybe a -> Maybe a) -> Key -> IntMap a -> IntMap a
IM.alter (Key -> Maybe IntSet -> Maybe IntSet
add_to_intset Key
f) Key
blockID (CFG -> IntMap IntSet
cfg_edges CFG
g)
                  let a_to_b' :: IntMap Key
a_to_b' = Key -> Key -> IntMap Key -> IntMap Key
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
a1 Key
f (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
                  let fresh' :: Key
fresh'  = Key
f Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Key
1
                  CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall a b. (a -> b) -> a -> b
$ IntMap [Key]
-> IntMap IntSet
-> IntMap Key
-> Key
-> IntMap [Instruction]
-> CFG
CFG IntMap [Key]
blocks' IntMap IntSet
edges' IntMap Key
a_to_b' Key
fresh' IntMap [Instruction]
forall a. IntMap a
IM.empty



add_to_intset :: Key -> Maybe IntSet -> Maybe IntSet
add_to_intset Key
a Maybe IntSet
Nothing  = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ Key -> IntSet
IS.singleton Key
a
add_to_intset Key
a (Just IntSet
x) = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ Key -> IntSet -> IntSet
IS.insert Key
a IntSet
x 

append_to_list :: a -> Maybe [a] -> Maybe [a]
append_to_list a
a Maybe [a]
Nothing = [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
a]
append_to_list a
a (Just [a]
x) = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a]
x[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a
a]) 

add_edge :: Key -> Key -> Bool -> CFG -> CFG
add_edge Key
a0 Key
a1 Bool
is_call_a0 CFG
g =
  case CFG -> Maybe CFG
add_to CFG
g of 
    Maybe CFG
Nothing -> [Char] -> CFG
forall a. HasCallStack => [Char] -> a
error [Char]
"Could not add edge"
    Just CFG
g  -> CFG
g
 where
  add_to :: CFG -> Maybe CFG
add_to = Key -> CFG -> Maybe CFG
split_graph' Key
a0 (CFG -> Maybe CFG) -> (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Key -> CFG -> Maybe CFG
split_graph Key
a1 (CFG -> Maybe CFG) -> (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Key -> Key -> CFG -> Maybe CFG
add_edge_to_graph Key
a0 Key
a1 (CFG -> Maybe CFG) -> (CFG -> Maybe CFG) -> CFG -> Maybe CFG
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Key -> Bool -> CFG -> Maybe CFG
split_calls Key
a0 Bool
is_call_a0
  split_calls :: Key -> Bool -> CFG -> Maybe CFG
split_calls Key
a Bool
True  = Key -> CFG -> Maybe CFG
split_graph' Key
a
  split_calls Key
a Bool
False = CFG -> Maybe CFG
forall (m :: * -> *) a. Monad m => a -> m a
return



init_cfg :: a -> CFG
init_cfg a
a = CFG :: IntMap [Key]
-> IntMap IntSet
-> IntMap Key
-> Key
-> IntMap [Instruction]
-> CFG
CFG { cfg_blocks :: IntMap [Key]
cfg_blocks = Key -> [Key] -> IntMap [Key]
forall a. Key -> a -> IntMap a
IM.singleton Key
0 [a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a], cfg_edges :: IntMap IntSet
cfg_edges = IntMap IntSet
forall a. IntMap a
IM.empty, cfg_addr_to_blockID :: IntMap Key
cfg_addr_to_blockID = Key -> Key -> IntMap Key
forall a. Key -> a -> IntMap a
IM.singleton (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) Key
0, cfg_fresh :: Key
cfg_fresh = Key
1, cfg_instrs :: IntMap [Instruction]
cfg_instrs = IntMap [Instruction]
forall a. IntMap a
IM.empty }


is_consecutive :: a -> a -> [a] -> Bool
is_consecutive a
a a
b []      = Bool
False
is_consecutive a
a a
b [a
_]     = Bool
False
is_consecutive a
a a
b (a
c:a
d:[a]
x) = (a
a,a
b) (a, a) -> (a, a) -> Bool
forall a. Eq a => a -> a -> Bool
== (a
c,a
d) Bool -> Bool -> Bool
|| a -> a -> [a] -> Bool
is_consecutive a
a a
b (a
da -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
x)

is_edge :: CFG -> Key -> Key -> Bool
is_edge CFG
g Key
a0 Key
a1 =
 case Maybe Bool
lookup of
  Maybe Bool
Nothing -> Bool
False
  Just Bool
b -> Bool
b
 where
  lookup :: Maybe Bool
lookup = do
    Key
blockId  <- Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a0 (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
    Key
blockId' <- Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
a1 (CFG -> IntMap Key
cfg_addr_to_blockID CFG
g)
    [Key]
b  <- Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockId  (CFG -> IntMap [Key]
cfg_blocks CFG
g)
    [Key]
b' <- Key -> IntMap [Key] -> Maybe [Key]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockId' (CFG -> IntMap [Key]
cfg_blocks CFG
g)
    if [Key] -> Key
forall a. [a] -> a
last [Key]
b Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
a0 then do
      IntSet
edges <- Key -> IntMap IntSet -> Maybe IntSet
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockId (CFG -> IntMap IntSet
cfg_edges CFG
g)
      Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ [Key] -> Key
forall a. [a] -> a
head [Key]
b' Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
a1 Bool -> Bool -> Bool
&& Key
blockId' Key -> IntSet -> Bool
`IS.member` IntSet
edges
    else
      Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Key
blockId Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
blockId' Bool -> Bool -> Bool
&& Key -> Key -> [Key] -> Bool
forall a. Eq a => a -> a -> [a] -> Bool
is_consecutive Key
a0 Key
a1 [Key]
b












is_new_function_call_to_be_analyzed :: Context -> Key -> Bool
is_new_function_call_to_be_analyzed Context
ctxt Key
trgt = (Key -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
trgt (IntMap FReturnBehavior -> Maybe FReturnBehavior)
-> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a b. (a -> b) -> a -> b
$ 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 Bool -> Bool -> Bool
|| (Key -> IntMap FInit -> Maybe FInit
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
trgt (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt) Maybe FInit -> Maybe FInit -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe FInit
forall a. Maybe a
Nothing


resolve_call :: Context
-> Key
-> Instruction
-> Either (Set (Instruction, b)) [(Key, Bool)]
resolve_call Context
ctxt Key
entry Instruction
i =
  let resolved_addresses :: [ResolvedJumpTarget]
resolved_addresses = Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i in
    if (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ResolvedJumpTarget -> ResolvedJumpTarget -> Bool
forall a. Eq a => a -> a -> Bool
(==) ResolvedJumpTarget
Unresolved) [ResolvedJumpTarget]
resolved_addresses then
      [(Key, Bool)] -> Either (Set (Instruction, b)) [(Key, Bool)]
forall a b. b -> Either a b
Right [(Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall a. HasAddress a => a -> Word64
addressof Instruction
i) Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i,Bool
True)] -- Right []
    else 
      let nexts :: [Either [b] [(Key, Bool)]]
nexts          = (ResolvedJumpTarget -> Either [b] [(Key, Bool)])
-> [ResolvedJumpTarget] -> [Either [b] [(Key, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map ResolvedJumpTarget -> Either [b] [(Key, Bool)]
forall a. Num a => ResolvedJumpTarget -> Either [a] [(Key, Bool)]
next [ResolvedJumpTarget]
resolved_addresses
          ([[b]]
lefts,[[(Key, Bool)]]
rights) = [Either [b] [(Key, Bool)]] -> ([[b]], [[(Key, Bool)]])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either [b] [(Key, Bool)]]
nexts in
        if [[b]]
lefts [[b]] -> [[b]] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
          [(Key, Bool)] -> Either (Set (Instruction, b)) [(Key, Bool)]
forall a b. b -> Either a b
Right ([(Key, Bool)] -> Either (Set (Instruction, b)) [(Key, Bool)])
-> [(Key, Bool)] -> Either (Set (Instruction, b)) [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ [[(Key, Bool)]] -> [(Key, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Key, Bool)]]
rights
        else
          Set (Instruction, b) -> Either (Set (Instruction, b)) [(Key, Bool)]
forall a b. a -> Either a b
Left (Set (Instruction, b)
 -> Either (Set (Instruction, b)) [(Key, Bool)])
-> Set (Instruction, b)
-> Either (Set (Instruction, b)) [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ [(Instruction, b)] -> Set (Instruction, b)
forall a. Ord a => [a] -> Set a
S.fromList ([(Instruction, b)] -> Set (Instruction, b))
-> [(Instruction, b)] -> Set (Instruction, b)
forall a b. (a -> b) -> a -> b
$ (b -> (Instruction, b)) -> [b] -> [(Instruction, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\b
a -> (Instruction
i,b
a)) ([b] -> [(Instruction, b)]) -> [b] -> [(Instruction, b)]
forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
lefts
 where
  next :: ResolvedJumpTarget -> Either [a] [(Key, Bool)]
next (External [Char]
sym) =
    -- external function call 
    if [Char] -> Bool
is_exiting_function_call [Char]
sym then
      [(Key, Bool)] -> Either [a] [(Key, Bool)]
forall a b. b -> Either a b
Right []
    else
      [(Key, Bool)] -> Either [a] [(Key, Bool)]
forall a b. b -> Either a b
Right [(Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall a. HasAddress a => a -> Word64
addressof Instruction
i) Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i,Bool
True)]
  next (ImmediateAddress Word64
a') =
    -- call to an immediate address
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Key -> Bool
is_new_function_call_to_be_analyzed Context
ctxt (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a') then
      -- internal function call already analyzed
      if (Key -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Key -> IntMap a -> Maybe a
IM.lookup (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a') (IntMap FReturnBehavior -> Maybe FReturnBehavior)
-> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FReturnBehavior
ctxt_calls Context
ctxt) Maybe FReturnBehavior -> Maybe FReturnBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== FReturnBehavior -> Maybe FReturnBehavior
forall a. a -> Maybe a
Just FReturnBehavior
Terminating then
        -- verified and terminating
        [(Key, Bool)] -> Either [a] [(Key, Bool)]
forall a b. b -> Either a b
Right []
      else
        -- verified and returning
        [(Key, Bool)] -> Either [a] [(Key, Bool)]
forall a b. b -> Either a b
Right [(Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall a. HasAddress a => a -> Word64
addressof Instruction
i) Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i,Bool
True)]
    else if Graph -> Key -> Key -> Bool
graph_is_edge (Context -> Graph
ctxt_entries Context
ctxt) Key
entry (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a') then
      -- recursion
      [(Key, Bool)] -> Either [a] [(Key, Bool)]
forall a b. b -> Either a b
Right [(Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Word64
forall a. HasAddress a => a -> Word64
addressof Instruction
i) Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i,Bool
True)]
    else
      -- new function, stop CFG generation here
      [a] -> Either [a] [(Key, Bool)]
forall a b. a -> Either a b
Left [Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a']


-- | An abstract step function
--
-- Given the entry address of the function currently under investigation, and the instruction address of the current instruction,
-- try to get the set of next instruction addresses.
-- 
-- This returns either:
--   * a set of tuples @(i,a)@ where @i@ is an instruction and @a@ its address. All these instructions are function calls that need to be analyzed before this current function entry can continue.
--   * a list of tuples @(a,b)@ where @a@ is an instruction address that may follow the current instruction, and @b@ is a Bool indicating whether that address belongs to a @call@
--
--   TODO the Lefts are ignored so need no to return them
stepA :: 
     Context   -- ^ The context
  -> Int       -- ^ The entry address
  -> Int       -- ^ The instruction address
  -> IO (Either (S.Set (X86.Instruction,Int)) [(Int,Bool)])
stepA :: Context
-> Key -> Key -> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
stepA Context
ctxt Key
entry Key
a = do
  Maybe Instruction
instr <- Context -> Word64 -> IO (Maybe Instruction)
fetch_instruction Context
ctxt (Word64 -> IO (Maybe Instruction))
-> Word64 -> IO (Maybe Instruction)
forall a b. (a -> b) -> a -> b
$ Key -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
a
  case Maybe Instruction
instr of
    Maybe Instruction
Nothing -> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right [] -- error $ "Cannot find instruction at addres: " ++ showHex a
    Just Instruction
i -> 
      if Opcode -> Bool
isHalt (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) then
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right []
      else if Opcode -> Bool
isJump (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) then
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right ([(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)])
-> [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ (Key -> (Key, Bool)) -> [Key] -> [(Key, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\Key
a -> (Key
a,Bool
False)) ([Key] -> [(Key, Bool)]) -> [Key] -> [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> [Key]) -> [ResolvedJumpTarget] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Key]
get_internal_addresses ([ResolvedJumpTarget] -> [Key]) -> [ResolvedJumpTarget] -> [Key]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i 
      else if Opcode -> Bool
isCondJump (Opcode -> Bool) -> Opcode -> Bool
forall a b. (a -> b) -> a -> b
$ Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i then
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right ([(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)])
-> [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ (Key -> (Key, Bool)) -> [Key] -> [(Key, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\Key
a -> (Key
a,Bool
False)) ([Key] -> [(Key, Bool)]) -> [Key] -> [(Key, Bool)]
forall a b. (a -> b) -> a -> b
$ ((ResolvedJumpTarget -> [Key]) -> [ResolvedJumpTarget] -> [Key]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Key]
get_internal_addresses ([ResolvedJumpTarget] -> [Key]) -> [ResolvedJumpTarget] -> [Key]
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i) [Key] -> [Key] -> [Key]
forall a. [a] -> [a] -> [a]
++ [Key
a Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i]
      else if Opcode -> Bool
isCall (Opcode -> Bool) -> Opcode -> Bool
forall a b. (a -> b) -> a -> b
$ Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i then
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ Context
-> Key
-> Instruction
-> Either (Set (Instruction, Key)) [(Key, Bool)]
forall b.
(Ord b, Num b) =>
Context
-> Key
-> Instruction
-> Either (Set (Instruction, b)) [(Key, Bool)]
resolve_call Context
ctxt Key
entry Instruction
i
      else if Opcode -> Bool
isRet (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i) then
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right []
      else
        Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Set (Instruction, Key)) [(Key, Bool)]
 -> IO (Either (Set (Instruction, Key)) [(Key, Bool)]))
-> Either (Set (Instruction, Key)) [(Key, Bool)]
-> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
forall a b. (a -> b) -> a -> b
$ [(Key, Bool)] -> Either (Set (Instruction, Key)) [(Key, Bool)]
forall a b. b -> Either a b
Right [(Key
a Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Instruction -> Key
forall a. HasSize a => a -> Key
sizeof Instruction
i,Bool
False)]




mk_graph :: Context -> Int -> S.Set ((Int,Bool), Int) -> CFG -> S.Set (X86.Instruction,Int) -> IO (S.Set (X86.Instruction,Int),CFG) 
mk_graph :: Context
-> Key
-> Set ((Key, Bool), Key)
-> CFG
-> Set (Instruction, Key)
-> IO (Set (Instruction, Key), CFG)
mk_graph Context
ctxt Key
entry Set ((Key, Bool), Key)
bag CFG
g Set (Instruction, Key)
new_calls =
  case Set ((Key, Bool), Key)
-> Maybe (((Key, Bool), Key), Set ((Key, Bool), Key))
forall a. Set a -> Maybe (a, Set a)
S.minView Set ((Key, Bool), Key)
bag of
    Maybe (((Key, Bool), Key), Set ((Key, Bool), Key))
Nothing -> (Set (Instruction, Key), CFG) -> IO (Set (Instruction, Key), CFG)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Set (Instruction, Key), CFG) -> IO (Set (Instruction, Key), CFG))
-> (Set (Instruction, Key), CFG)
-> IO (Set (Instruction, Key), CFG)
forall a b. (a -> b) -> a -> b
$ (Set (Instruction, Key)
new_calls,CFG
g)
    Just (((Key
a0,Bool
is_call_a0),Key
a1),Set ((Key, Bool), Key)
bag) -> do
      if CFG -> Key -> Key -> Bool
is_edge CFG
g Key
a0 Key
a1 then 
        Context
-> Key
-> Set ((Key, Bool), Key)
-> CFG
-> Set (Instruction, Key)
-> IO (Set (Instruction, Key), CFG)
mk_graph Context
ctxt Key
entry Set ((Key, Bool), Key)
bag CFG
g Set (Instruction, Key)
new_calls
      else do
        let g' :: CFG
g' = Key -> Key -> Bool -> CFG -> CFG
add_edge (Key -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
a0) (Key -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Key
a1) Bool
is_call_a0 CFG
g
        Either (Set (Instruction, Key)) [(Key, Bool)]
nxt <- Context
-> Key -> Key -> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
stepA Context
ctxt Key
entry Key
a1
        case Either (Set (Instruction, Key)) [(Key, Bool)]
nxt of
          Left Set (Instruction, Key)
new_calls' -> do
            Context
-> Key
-> Set ((Key, Bool), Key)
-> CFG
-> Set (Instruction, Key)
-> IO (Set (Instruction, Key), CFG)
mk_graph Context
ctxt Key
entry Set ((Key, Bool), Key)
bag CFG
g' (Set (Instruction, Key)
-> Set (Instruction, Key) -> Set (Instruction, Key)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Instruction, Key)
new_calls' Set (Instruction, Key)
new_calls)
          Right [(Key, Bool)]
as -> do
            let bag' :: Set ((Key, Bool), Key)
bag' = Set ((Key, Bool), Key)
-> Set ((Key, Bool), Key) -> Set ((Key, Bool), Key)
forall a. Ord a => Set a -> Set a -> Set a
S.union ([((Key, Bool), Key)] -> Set ((Key, Bool), Key)
forall a. Ord a => [a] -> Set a
S.fromList ([((Key, Bool), Key)] -> Set ((Key, Bool), Key))
-> [((Key, Bool), Key)] -> Set ((Key, Bool), Key)
forall a b. (a -> b) -> a -> b
$ ((Key, Bool) -> ((Key, Bool), Key))
-> [(Key, Bool)] -> [((Key, Bool), Key)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Key
a2,Bool
is_call_a1) -> ((Key
a1,Bool
is_call_a1),Key
a2)) [(Key, Bool)]
as) Set ((Key, Bool), Key)
bag
            Context
-> Key
-> Set ((Key, Bool), Key)
-> CFG
-> Set (Instruction, Key)
-> IO (Set (Instruction, Key), CFG)
mk_graph Context
ctxt Key
entry Set ((Key, Bool), Key)
bag' CFG
g' Set (Instruction, Key)
new_calls
    

fromJust' :: [a] -> Maybe p -> p
fromJust' [a]
as Maybe p
Nothing = [Char] -> p
forall a. HasCallStack => [Char] -> a
error ([Char] -> p) -> [Char] -> p
forall a b. (a -> b) -> a -> b
$ [a] -> [Char]
forall a. (Integral a, Show a) => [a] -> [Char]
showHex_list [a]
as
fromJust' [a]
_ (Just p
a) = p
a

cfg_add_instrs :: Context -> CFG -> IO CFG
cfg_add_instrs Context
ctxt CFG
g = do
  [(Key, [Instruction])]
instrs <- ((Key, [Key]) -> IO (Key, [Instruction]))
-> [(Key, [Key])] -> IO [(Key, [Instruction])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Key, [Key]) -> IO (Key, [Instruction])
forall a a.
(Integral a, Show a) =>
(a, [a]) -> IO (a, [Instruction])
block_to_instrs ([(Key, [Key])] -> IO [(Key, [Instruction])])
-> [(Key, [Key])] -> IO [(Key, [Instruction])]
forall a b. (a -> b) -> a -> b
$ IntMap [Key] -> [(Key, [Key])]
forall a. IntMap a -> [(Key, a)]
IM.toList (IntMap [Key] -> [(Key, [Key])]) -> IntMap [Key] -> [(Key, [Key])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Key]
cfg_blocks CFG
g
  CFG -> IO CFG
forall (m :: * -> *) a. Monad m => a -> m a
return (CFG -> IO CFG) -> CFG -> IO CFG
forall a b. (a -> b) -> a -> b
$ CFG
g { cfg_instrs :: IntMap [Instruction]
cfg_instrs = [(Key, [Instruction])] -> IntMap [Instruction]
forall a. [(Key, a)] -> IntMap a
IM.fromList [(Key, [Instruction])]
instrs }
 where
    block_to_instrs :: (a, [a]) -> IO (a, [Instruction])
block_to_instrs (a
a,[a]
as) = do 
      [Maybe Instruction]
instrs <- (a -> IO (Maybe Instruction)) -> [a] -> IO [Maybe Instruction]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Context -> Word64 -> IO (Maybe Instruction)
fetch_instruction Context
ctxt (Word64 -> IO (Maybe Instruction))
-> (a -> Word64) -> a -> IO (Maybe Instruction)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral) [a]
as
      (a, [Instruction]) -> IO (a, [Instruction])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, [Instruction]) -> IO (a, [Instruction]))
-> (a, [Instruction]) -> IO (a, [Instruction])
forall a b. (a -> b) -> a -> b
$ (a
a, (Maybe Instruction -> Instruction)
-> [Maybe Instruction] -> [Instruction]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> Maybe Instruction -> Instruction
forall a p. (Integral a, Show a) => [a] -> Maybe p -> p
fromJust' [a]
as) [Maybe Instruction]
instrs)

-- | Produce a CFG
--
-- Given the entry point of the function, generate either a CFG, or a set of new entry points to be analyzed first.
-- The set of new entry points are function entries called by the current function, but for which we do not know yet whether they terminate or not.
-- If a CFG is returned, then all function calls in that CFG have already been analyzed.
cfg_gen ::
     Context -- ^ The context
  -> Int     -- ^ The entry point of the function
  -> IO (S.Set (X86.Instruction,Int),CFG)
cfg_gen :: Context -> Key -> IO (Set (Instruction, Key), CFG)
cfg_gen Context
ctxt Key
entry = do
 let g :: CFG
g           = Key -> CFG
forall a. Integral a => a -> CFG
init_cfg Key
entry
 Either (Set (Instruction, Key)) [(Key, Bool)]
nxt            <- Context
-> Key -> Key -> IO (Either (Set (Instruction, Key)) [(Key, Bool)])
stepA Context
ctxt Key
entry Key
entry
 let bag :: Set ((Key, Bool), Key)
bag         = [((Key, Bool), Key)] -> Set ((Key, Bool), Key)
forall a. Ord a => [a] -> Set a
S.fromList ([((Key, Bool), Key)] -> Set ((Key, Bool), Key))
-> [((Key, Bool), Key)] -> Set ((Key, Bool), Key)
forall a b. (a -> b) -> a -> b
$ ((Key, Bool) -> ((Key, Bool), Key))
-> [(Key, Bool)] -> [((Key, Bool), Key)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Key
a,Bool
is_call_a) -> ((Key
entry,Bool
False),Key
a)) ([(Key, Bool)]
-> Either (Set (Instruction, Key)) [(Key, Bool)] -> [(Key, Bool)]
forall b a. b -> Either a b -> b
fromRight [] Either (Set (Instruction, Key)) [(Key, Bool)]
nxt) -- assumes entry is not a call
 (Set (Instruction, Key)
new_calls,CFG
g') <- Context
-> Key
-> Set ((Key, Bool), Key)
-> CFG
-> Set (Instruction, Key)
-> IO (Set (Instruction, Key), CFG)
mk_graph Context
ctxt Key
entry Set ((Key, Bool), Key)
bag CFG
g Set (Instruction, Key)
forall a. Set a
S.empty
 CFG
g''            <- Context -> CFG -> IO CFG
cfg_add_instrs Context
ctxt CFG
g'
 (Set (Instruction, Key), CFG) -> IO (Set (Instruction, Key), CFG)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Instruction, Key)
new_calls, CFG
g'')




        
-- | Returns true if the given blockID is a leaf-node in the given CFG.
is_end_node ::
  CFG     -- ^ The CFG
  -> Int  -- ^ The blockID
  -> Bool
is_end_node :: CFG -> Key -> Bool
is_end_node CFG
g Key
b = IntSet -> Bool
IS.null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ CFG -> Key -> IntSet
post CFG
g Key
b

is_unresolved_indirection :: Context -> Instruction -> Bool
is_unresolved_indirection Context
ctxt Instruction
i = (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
|| Opcode -> Bool
isCondJump (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i))
                   Bool -> Bool -> Bool
&& ((ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ResolvedJumpTarget -> ResolvedJumpTarget -> Bool
forall a. Eq a => a -> a -> Bool
(==) ResolvedJumpTarget
Unresolved) ([ResolvedJumpTarget] -> Bool) -> [ResolvedJumpTarget] -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i)


-- | Returns the @`NodeInfo`@ of a given blockID.
--
-- Assumes the given blockID corresponds to a leaf-node.
node_info_of ::
     Context -- ^ The context
  -> CFG
  -> Int
  -> NodeInfo 
node_info_of :: Context -> CFG -> Key -> NodeInfo
node_info_of Context
ctxt CFG
g Key
blockId =
  let a :: Key
a    = [Key] -> Key
forall a. [a] -> a
last ([Char] -> IntMap [Key] -> Key -> [Key]
forall p. [Char] -> IntMap p -> Key -> p
im_lookup ([Char]
"C.) Block " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. Show a => a -> [Char]
show Key
blockId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in cfg.") (CFG -> IntMap [Key]
cfg_blocks CFG
g) Key
blockId)
      i :: Instruction
i    = [Instruction] -> Instruction
forall a. [a] -> a
last ([Char] -> IntMap [Instruction] -> Key -> [Instruction]
forall p. [Char] -> IntMap p -> Key -> p
im_lookup ([Char]
"D.) Block " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. Show a => a -> [Char]
show Key
blockId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in instrs.") (CFG -> IntMap [Instruction]
cfg_instrs CFG
g) Key
blockId) in
    if Context -> Instruction -> Bool
is_unresolved_indirection Context
ctxt Instruction
i then
      NodeInfo
UnresolvedIndirection
    else if IntSet -> Bool
IS.null (CFG -> Key -> IntSet
post CFG
g Key
blockId) Bool -> Bool -> Bool
&& (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
isHalt (Instruction -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode Instruction
i)) Bool -> Bool -> Bool
|| Instruction -> Bool
is_terminating_jump Instruction
i then
        NodeInfo
Terminal
    else
      NodeInfo
Normal

 where
  is_terminating_jump :: Instruction -> Bool
is_terminating_jump Instruction
i = 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
&&
    case Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i of
      [External [Char]
sym] -> [Char] -> Bool
is_exiting_function_call [Char]
sym
      [ResolvedJumpTarget]
_              -> Bool
False






-- | Export a CFG to .dot file
--
-- Strongly connected components get the same color.
cfg_to_dot ::
     Context -- ^ The context
  -> CFG     -- ^ The CFG
  -> String
cfg_to_dot :: Context -> CFG -> [Char]
cfg_to_dot Context
ctxt CFG
g =
 let name :: [Char]
name  = Context -> [Char]
ctxt_name Context
ctxt
     frontier :: IntSet
frontier = IntSet
IS.empty
     sccs :: [IntSet]
sccs     = CFG -> Key -> IntSet -> [IntSet]
forall g. IntGraph g => g -> Key -> IntSet -> [IntSet]
scc_of CFG
g Key
0 IntSet
frontier in
  [Char]
"diGraph " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"{\n"
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((Key -> [Char]) -> [Key] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([IntSet] -> Key -> [Char]
node_to_dot [IntSet]
sccs) ([Key] -> [[Char]]) -> [Key] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntMap [Key] -> [Key]
forall a. IntMap a -> [Key]
IM.keys (IntMap [Key] -> [Key]) -> IntMap [Key] -> [Key]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Key]
cfg_blocks CFG
g)
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" (((Key, IntSet) -> [Char]) -> [(Key, IntSet)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Key, IntSet) -> [Char]
forall a. (Integral a, Show a) => (a, IntSet) -> [Char]
edge_to_dot' ([(Key, IntSet)] -> [[Char]]) -> [(Key, IntSet)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Key, IntSet)]
forall a. IntMap a -> [(Key, a)]
IM.toList (IntMap IntSet -> [(Key, IntSet)])
-> IntMap IntSet -> [(Key, IntSet)]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap IntSet
cfg_edges CFG
g)
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n}"
 where
  node_to_dot :: [IntSet] -> Key -> [Char]
node_to_dot [IntSet]
sccs Key
blockId =
    let bgcolor :: [Char]
bgcolor = Key -> [IntSet] -> [Char]
hex_color_of Key
blockId [IntSet]
sccs
        fgcolor :: [Char]
fgcolor = [Char] -> [Char]
hex_color_of_text [Char]
bgcolor in
       [Char]
"\t" 
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
mk_node Key
blockId
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  ["
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"style=filled fillcolor=\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
bgcolor [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\" fontcolor=\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fgcolor [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\" shape=" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
node_shape Key
blockId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"label=\""
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CFG -> Key -> [Char]
show_block CFG
g Key
blockId
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\"]"

  edge_to_dot' :: (a, IntSet) -> [Char]
edge_to_dot' (a
blockId, IntSet
blockIds) = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Key -> [Char]) -> [Key] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Key -> [Char]
forall a a.
(Integral a, Integral a, Show a, Show a) =>
a -> a -> [Char]
edge_to_dot'' a
blockId) ([Key] -> [[Char]]) -> [Key] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Key]
IS.toList IntSet
blockIds

  edge_to_dot'' :: a -> a -> [Char]
edge_to_dot'' a
blockId a
blockId' = [Char]
"\t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
mk_node a
blockId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
mk_node a
blockId'

  mk_node :: a -> [Char]
mk_node a
v = Context -> [Char]
ctxt_name Context
ctxt [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex a
v

  node_shape :: Key -> [Char]
node_shape Key
blockId =
    case Context -> CFG -> Key -> NodeInfo
node_info_of Context
ctxt CFG
g Key
blockId of
      NodeInfo
Normal -> [Char]
"oval"
      NodeInfo
Terminal -> [Char]
"invhouse"
      NodeInfo
UnresolvedIndirection -> [Char]
"box3d"

hex_color_of :: Key -> [IntSet] -> [Char]
hex_color_of Key
vertex [IntSet]
sccs =
  case (IntSet -> Bool) -> [IntSet] -> Maybe Key
forall a. (a -> Bool) -> [a] -> Maybe Key
findIndex (Key -> IntSet -> Bool
IS.member Key
vertex) [IntSet]
sccs of
    Just Key
n -> [[Char]]
hex_colors [[Char]] -> Key -> [Char]
forall a. [a] -> Key -> a
!! (Key
126 Key -> Key -> Key
forall a. Num a => a -> a -> a
- (Double -> Key
floorDoubleInt (Double -> Key) -> Double -> Key
forall a b. (a -> b) -> a -> b
$ Double
127 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Key -> Double
int2Double Key
n Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Key -> Double
int2Double ([IntSet] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [IntSet]
sccs)))
    Maybe Key
Nothing -> [Char]
"#FFFFFF"