{-# LANGUAGE PartialTypeSignatures, Strict #-}

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

module Analysis.ControlFlow (
   cfg_gen,
   cfg_to_dot,
   is_end_node,
   node_info_of,
   stepA,
   post,
   fetch_block,
   resolve_jump_target,
   get_internal_addresses,
   jump_is_actually_a_call,
   show_block,
   show_invariants,
   isTerminal
 )
 where

import Base

import Algorithm.SCC

import Analysis.Context
import Analysis.FunctionNames

import Data.JumpTarget
import Generic.Binary

import X86.Conventions
import X86.Instruction (addressof)
import X86.Opcode (isRet, isCall, isCondJump, isJump, isHalt)
import qualified X86.Instruction as X86
import Generic.HasSize (sizeof)
import qualified Generic.Instruction as Instr

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,fromMaybe,isNothing)
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)


-- 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









-- | The set of next blocks from the given block in a CFG
post :: CFG -> IS.Key -> IS.IntSet
post :: CFG -> Key -> IntSet
post CFG
g Key
blockId = IntSet -> Maybe IntSet -> IntSet
forall a. a -> Maybe a -> a
fromMaybe IntSet
IS.empty (Key -> IntMap IntSet -> Maybe IntSet
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockId (CFG -> IntMap IntSet
cfg_edges CFG
g))



-- | Fetching an instruction list given a block ID
fetch_block ::
  CFG    -- ^ The CFG
  -> Int -- ^ The blockID
  -> [X86.Instruction]
fetch_block :: CFG -> Key -> [Instruction]
fetch_block CFG
g Key
blockId =
  case Key -> IntMap [Instruction] -> Maybe [Instruction]
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
blockId (IntMap [Instruction] -> Maybe [Instruction])
-> IntMap [Instruction] -> Maybe [Instruction]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs (CFG -> IntMap [Instruction]) -> CFG -> IntMap [Instruction]
forall a b. (a -> b) -> a -> b
$ CFG
g of
    Maybe [Instruction]
Nothing -> [Char] -> [Instruction]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [Instruction]) -> [Char] -> [Instruction]
forall a b. (a -> b) -> a -> b
$ [Char]
"Block with ID" [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]
" not found in cfg."
    Just [Instruction]
b -> [Instruction]
b

isTerminal :: CFG -> IS.Key -> Bool
isTerminal :: CFG -> Key -> Bool
isTerminal CFG
cfg Key
b = Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe IntSet -> Bool) -> Maybe IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ Key -> IntMap IntSet -> Maybe IntSet
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
b (CFG -> IntMap IntSet
cfg_edges CFG
cfg)

-- | Resolves the first operand of a call or jump instruction.
-- First tries to see if the instruction is an indirection, that has already been resolved.
-- If not, try to statically resolve the first operand using @`operand_static_resolve`@.
-- If that resolves to an immediate value, see if that immediate value corresponds to an external function or an internal function.
--
-- Returns a list of @`ResolvedJumpTarget`@, since an indirection may be resolved to multiple targets.
resolve_jump_target ::
  Context        -- ^ The context
  -> X86.Instruction       -- ^ The instruction
  -> [ResolvedJumpTarget]
resolve_jump_target :: Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i =
  case (Key -> IntMap Indirection -> Maybe Indirection
forall a. Key -> IntMap a -> Maybe a
IM.lookup (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Key) -> Word64 -> Key
forall a b. (a -> b) -> a -> b
$ Instruction -> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof Instruction
i) (IntMap Indirection -> Maybe Indirection)
-> IntMap Indirection -> Maybe Indirection
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Indirection
ctxt_inds Context
ctxt, Instruction -> [GenericOperand Register]
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation
-> [GenericOperand storage]
Instr.srcs Instruction
i) of
    (Just Indirection
ind,[GenericOperand Register]
_)    -> Indirection -> [ResolvedJumpTarget]
indirection_to_jump_target Indirection
ind -- already resolved indirection
    (Maybe Indirection
Nothing,[GenericOperand Register
op1]) ->
      case Context
-> Instruction -> GenericOperand Register -> ResolvedJumpTarget
operand_static_resolve Context
ctxt Instruction
i GenericOperand Register
op1 of
        ResolvedJumpTarget
Unresolved         -> [ResolvedJumpTarget
Unresolved] -- unresolved indirection
        External [Char]
sym       -> [[Char] -> ResolvedJumpTarget
External [Char]
sym]
        ImmediateAddress Word64
a ->
          case Key -> IntMap Symbol -> Maybe Symbol
forall a. Key -> IntMap a -> Maybe a
IM.lookup (Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a) (IntMap Symbol -> Maybe Symbol) -> IntMap Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Context -> IntMap Symbol
ctxt_symbol_table Context
ctxt of
            Just (Relocated_Function [Char]
sym) -> [[Char] -> ResolvedJumpTarget
External [Char]
sym]
            Maybe Symbol
_ -> if Bool -> Bool
not (Context -> Word64 -> Bool
forall a. Integral a => Context -> a -> Bool
address_has_instruction Context
ctxt Word64
a) then [[Char] -> ResolvedJumpTarget
External ([Char] -> ResolvedJumpTarget) -> [Char] -> ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
a] else [Word64 -> ResolvedJumpTarget
ImmediateAddress Word64
a]

 where
  indirection_to_jump_target :: Indirection -> [ResolvedJumpTarget]
indirection_to_jump_target (Indirection_Resolved Set ResolvedJumpTarget
trgts) = Set ResolvedJumpTarget -> [ResolvedJumpTarget]
forall a. Set a -> [a]
S.toList Set ResolvedJumpTarget
trgts
  indirection_to_jump_target (Indirection_JumpTable (JumpTable GenericOperand Register
_ Key
_ GenericOperand Register
_ IntMap Word64
tbl)) = (Word64 -> ResolvedJumpTarget) -> [Word64] -> [ResolvedJumpTarget]
forall a b. (a -> b) -> [a] -> [b]
map Word64 -> ResolvedJumpTarget
ImmediateAddress ([Word64] -> [ResolvedJumpTarget])
-> [Word64] -> [ResolvedJumpTarget]
forall a b. (a -> b) -> a -> b
$ IntMap Word64 -> [Word64]
forall a. IntMap a -> [a]
IM.elems IntMap Word64
tbl

-- | Returns true iff the JUMP instruction is actually a CALL followed by implicit RET
jump_is_actually_a_call ::
  Context        -- ^ The context
  -> X86.Instruction       -- ^ The instruction
  -> Bool
jump_is_actually_a_call :: Context -> Instruction -> Bool
jump_is_actually_a_call Context
ctxt Instruction
i =
  (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ResolvedJumpTarget -> Bool
resolves_to_function_entry ([ResolvedJumpTarget] -> Bool) -> [ResolvedJumpTarget] -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Instruction -> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt Instruction
i
 where
  resolves_to_function_entry :: ResolvedJumpTarget -> Bool
resolves_to_function_entry ResolvedJumpTarget
Unresolved           = Bool
False
  resolves_to_function_entry (External [Char]
sym)       = Bool
True
  resolves_to_function_entry (ImmediateAddress Word64
a) = 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) (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




-- | Given a resolved jump target, get a possibly empty list of internal addresses to which the jump target can jump.
get_internal_addresses ::
  ResolvedJumpTarget -- ^ A resolved jump target
  -> [Int]
get_internal_addresses :: ResolvedJumpTarget -> [Key]
get_internal_addresses (External [Char]
_)         = []
get_internal_addresses ResolvedJumpTarget
Unresolved           = []
get_internal_addresses (ImmediateAddress Word64
a) = [Word64 -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a]







-- | Shows the block associated to the givern blockID.
show_block ::
  CFG    -- ^ The CFG
  -> Int -- ^ The blockID
  -> String
show_block :: CFG -> Key -> [Char]
show_block CFG
g Key
b =
  let instrs :: [Key]
instrs = [Char] -> IntMap [Key] -> Key -> [Key]
forall p. [Char] -> IntMap p -> Key -> p
im_lookup ([Char]
"show_block: Block " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. Show a => a -> [Char]
show Key
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"in cfg.") (CFG -> IntMap [Key]
cfg_blocks CFG
g) Key
b in
       Key -> [Char]
forall a. Show a => a -> [Char]
show Key
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ["
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex ([Key] -> Key
forall a. [a] -> a
head [Key]
instrs)
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
","
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Key -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex ([Key] -> Key
forall a. [a] -> a
last [Key]
instrs)
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"

-- | Shows invariants.
show_invariants
  :: CFG        -- ^ The CFG
  -> Invariants -- ^ The invariants
  -> String
show_invariants :: CFG -> Invariants -> [Char]
show_invariants CFG
g Invariants
invs = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((Key, Predicate) -> [Char]) -> [(Key, Predicate)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Key, Predicate) -> [Char]
forall a. Show a => (Key, a) -> [Char]
show_entry ([(Key, Predicate)] -> [[Char]]) -> [(Key, Predicate)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Invariants -> [(Key, Predicate)]
forall a. IntMap a -> [(Key, a)]
IM.toList (Invariants -> [(Key, Predicate)])
-> Invariants -> [(Key, Predicate)]
forall a b. (a -> b) -> a -> b
$ Invariants
invs
 where
  show_entry :: (Key, a) -> [Char]
show_entry (Key
blockId, a
p) =  [Char]
"Block " [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]
":\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
p







instance IntGraph CFG where
  intgraph_post :: CFG -> Key -> IntSet
intgraph_post = CFG -> Key -> IntSet
post
  intgraph_V :: CFG -> IntSet
intgraph_V    = IntMap [Key] -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet (IntMap [Key] -> IntSet) -> (CFG -> IntMap [Key]) -> CFG -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG -> IntMap [Key]
cfg_blocks





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 storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> 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 storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> 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 storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> 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 storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> 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]
forall a. Num a => ResolvedJumpTarget -> [a]
mk_jmp_trgt ([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)]
 where
  mk_jmp_trgt :: ResolvedJumpTarget -> [a]
mk_jmp_trgt ResolvedJumpTarget
Unresolved           = []
  mk_jmp_trgt (External [Char]
sym)       = []
  mk_jmp_trgt (ImmediateAddress Word64
a)
    | 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) (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
otherwise = [Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a]


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"