{-# LANGUAGE PartialTypeSignatures, Strict #-}

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

module WithAbstractPredicates.ControlFlow 
 where

import Base

import Algorithm.SCC

import Binary.FunctionNames
import Data.X86.Opcode
import Data.X86.Instruction


import Data.L0
import Data.JumpTarget
import Data.Indirection
import Data.CFG
import Binary.Generic 

import Conventions


import Control.Monad.Extra


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 GHC.Float.RealFracMethods (floorDoubleInt,int2Double)


data NextRips = JustRips [Word64] | UnresolvedTarget | Terminal | UnvisitedFunctionCall Word64
  deriving (NextRips -> NextRips -> Bool
(NextRips -> NextRips -> Bool)
-> (NextRips -> NextRips -> Bool) -> Eq NextRips
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NextRips -> NextRips -> Bool
== :: NextRips -> NextRips -> Bool
$c/= :: NextRips -> NextRips -> Bool
/= :: NextRips -> NextRips -> Bool
Eq,Int -> NextRips -> ShowS
[NextRips] -> ShowS
NextRips -> String
(Int -> NextRips -> ShowS)
-> (NextRips -> String) -> ([NextRips] -> ShowS) -> Show NextRips
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NextRips -> ShowS
showsPrec :: Int -> NextRips -> ShowS
$cshow :: NextRips -> String
show :: NextRips -> String
$cshowList :: [NextRips] -> ShowS
showList :: [NextRips] -> ShowS
Show)

next_rips :: (BinaryClass bin, Eq pred) =>
     Lifting bin pred finit v
  -> Maybe Instruction
  -> NextRips
next_rips :: forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Maybe Instruction -> NextRips
next_rips l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
_) Maybe Instruction
Nothing  = [Word64] -> NextRips
JustRips []
next_rips l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
_) (Just Instruction
i) = Instruction -> Opcode -> NextRips
next_rip_based_on_opcode Instruction
i (Opcode -> NextRips) -> Opcode -> NextRips
forall a b. (a -> b) -> a -> b
$ Instruction -> Opcode
inOperation Instruction
i
 where
  next_rip_based_on_opcode :: Instruction -> Opcode -> NextRips
next_rip_based_on_opcode Instruction
i Opcode
op
    | Opcode -> Bool
isHalt Opcode
op = NextRips
Terminal
    | Opcode -> Bool
isJump Opcode
op =
      if Lifting bin pred finit v -> Instruction -> Bool
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> Bool
jump_is_actually_a_call Lifting bin pred finit v
l Instruction
i then
        case Lifting bin pred finit v -> Instruction -> NextRips
forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Instruction -> NextRips
resolve_call Lifting bin pred finit v
l Instruction
i of
          JustRips [Word64]
_       -> [Word64] -> NextRips
JustRips []
          NextRips
Terminal         -> NextRips
Terminal
          NextRips
UnresolvedTarget -> NextRips
UnresolvedTarget
      else let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
l Instruction
i in
        if (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ResolvedJumpTarget -> ResolvedJumpTarget -> Bool
forall a. Eq a => a -> a -> Bool
(==) ResolvedJumpTarget
Unresolved) [ResolvedJumpTarget]
trgts then
          NextRips
UnresolvedTarget
        else
          [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> [Word64])
-> [ResolvedJumpTarget] -> [Word64]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Word64]
mk_jmp_trgt [ResolvedJumpTarget]
trgts 
    | Opcode -> Bool
isCondJump Opcode
op =
      let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
l Instruction
i in
        if (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ResolvedJumpTarget -> ResolvedJumpTarget -> Bool
forall a. Eq a => a -> a -> Bool
(==) ResolvedJumpTarget
Unresolved) [ResolvedJumpTarget]
trgts then
          NextRips
UnresolvedTarget
        else
          [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ ((ResolvedJumpTarget -> [Word64])
-> [ResolvedJumpTarget] -> [Word64]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Word64]
mk_jmp_trgt [ResolvedJumpTarget]
trgts) [Word64] -> [Word64] -> [Word64]
forall a. [a] -> [a] -> [a]
++ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
    | Opcode -> Bool
isCall Opcode
op = Lifting bin pred finit v -> Instruction -> NextRips
forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Instruction -> NextRips
resolve_call Lifting bin pred finit v
l Instruction
i
    | Opcode -> Bool
isRet Opcode
op  = [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ []
    | Bool
otherwise = [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]

  mk_jmp_trgt :: ResolvedJumpTarget -> [Word64]
mk_jmp_trgt (ImmediateAddress Word64
a) = [Word64
a]
  mk_jmp_trgt (ResolvedJumpTarget
Unresolved) = []


resolve_call :: (BinaryClass bin, Eq pred) => Lifting bin pred finit v -> Instruction -> NextRips
resolve_call :: forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Instruction -> NextRips
resolve_call l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
l0) Instruction
i =
  let resolved_addresses :: [ResolvedJumpTarget]
resolved_addresses = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
l Instruction
i in
    if (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ResolvedJumpTarget -> ResolvedJumpTarget -> Bool
forall a. Eq a => a -> a -> Bool
(==) ResolvedJumpTarget
Unresolved) [ResolvedJumpTarget]
resolved_addresses then
      case Word64 -> L0 pred finit v -> Maybe Indirections
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe Indirections
l0_lookup_indirection (Instruction -> Word64
inAddress Instruction
i) L0 pred finit v
l0 of
        Just Indirections
_ -> [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
        Maybe Indirections
_ -> NextRips
UnresolvedTarget
    else let nexts :: [NextRips]
nexts = (ResolvedJumpTarget -> NextRips)
-> [ResolvedJumpTarget] -> [NextRips]
forall a b. (a -> b) -> [a] -> [b]
map ResolvedJumpTarget -> NextRips
next [ResolvedJumpTarget]
resolved_addresses in
      (NextRips -> NextRips -> NextRips) -> [NextRips] -> NextRips
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 NextRips -> NextRips -> NextRips
gather [NextRips]
nexts
 where
  gather :: NextRips -> NextRips -> NextRips
gather n :: NextRips
n@(UnvisitedFunctionCall Word64
i) NextRips
_  = NextRips
n
  gather (JustRips [Word64]
as) (JustRips [Word64]
as')   = [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Word64]
as[Word64] -> [Word64] -> [Word64]
forall a. [a] -> [a] -> [a]
++[Word64]
as'
  gather NextRips
_ n :: NextRips
n@(UnvisitedFunctionCall Word64
i)  = NextRips
n
  gather NextRips
Terminal NextRips
Terminal              = NextRips
Terminal
  gather (JustRips [Word64]
as) NextRips
Terminal         = [Word64] -> NextRips
JustRips [Word64]
as
  gather NextRips
Terminal (JustRips [Word64]
as)         = [Word64] -> NextRips
JustRips [Word64]
as
  gather NextRips
UnresolvedTarget (JustRips [Word64]
as) = [Word64] -> NextRips
JustRips [Word64]
as
  gather (JustRips [Word64]
as) NextRips
UnresolvedTarget = [Word64] -> NextRips
JustRips [Word64]
as
  gather NextRips
x NextRips
y = String -> NextRips
forall a. HasCallStack => String -> a
error (String -> NextRips) -> String -> NextRips
forall a b. (a -> b) -> a -> b
$ (NextRips, NextRips) -> String
forall a. Show a => a -> String
show (NextRips
x,NextRips
y)


  next :: ResolvedJumpTarget -> NextRips
next (External String
sym)
    -- external function call
    | String -> Bool
is_exiting_function_call String
sym = NextRips
Terminal
    | String
sym String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"error" = NextRips
UnresolvedTarget
    | Bool
otherwise = [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
  next (ExternalDeref String
sym)
    -- external function call
    | String -> Bool
is_exiting_function_call String
sym = NextRips
Terminal
    | Bool
otherwise = [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
  next (ImmediateAddress Word64
a') =
    case Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
a' L0 pred finit v
l0 of
      Maybe (finit, Maybe (FResult pred v))
Nothing          -> -- Unvisited, stop CFG generation here
                          Word64 -> NextRips
UnvisitedFunctionCall Word64
a'
      Just (finit
_,Maybe (FResult pred v)
Nothing) -> -- Recursive unanalyzed call
                          [Word64] -> NextRips
JustRips ([Word64] -> NextRips) -> [Word64] -> NextRips
forall a b. (a -> b) -> a -> b
$ [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)] 
      Just (finit
_,Just FResult pred v
r)  -> -- Already analyzed call
                          if FResult pred v -> Postcondition pred
forall pred v. FResult pred v -> Postcondition pred
result_post FResult pred v
r Postcondition pred -> Postcondition pred -> Bool
forall a. Eq a => a -> a -> Bool
== Postcondition pred
forall pred. Postcondition pred
Terminates then NextRips
Terminal else [Word64] -> NextRips
JustRips [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
  next (Returns Bool
True) = [Word64] -> NextRips
JustRips [Instruction -> Word64
inAddress Instruction
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Instruction -> Int
inSize Instruction
i)]
  next (Returns Bool
False) = NextRips
Terminal
  next (ResolvedJumpTarget
Unresolved)    = NextRips
UnresolvedTarget


-- | Returns true iff the JUMP instruction is actually a CALL followed by implicit RET
jump_is_actually_a_call ::
  BinaryClass bin =>
     Lifting bin pred finit v
  -> Instruction       -- ^ The instruction
  -> Bool
jump_is_actually_a_call :: forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> Bool
jump_is_actually_a_call l :: Lifting bin pred finit v
l@(bin
_,Config
_,L0 pred finit v
l0) Instruction
i =
  let trgts :: [ResolvedJumpTarget]
trgts = Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets Lifting bin pred finit v
l Instruction
i in
    (ResolvedJumpTarget -> Bool) -> [ResolvedJumpTarget] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ResolvedJumpTarget -> Bool
resolves_to_function_entry [ResolvedJumpTarget]
trgts
 where
  resolves_to_function_entry :: ResolvedJumpTarget -> Bool
resolves_to_function_entry ResolvedJumpTarget
Unresolved           = Bool
False
  resolves_to_function_entry (External String
sym)       = Bool
True
  resolves_to_function_entry (ExternalDeref String
sym)  = Bool
True
  resolves_to_function_entry (Returns Bool
_)          = Bool
True
  resolves_to_function_entry (ImmediateAddress Word64
a) = 
    case Word64 -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry Word64
a L0 pred finit v
l0 of
      Maybe (finit, Maybe (FResult pred v))
Nothing -> Bool
False
      Just (finit, Maybe (FResult pred v))
_  -> Bool
True


get_known_jump_targets ::
  BinaryClass bin =>
     Lifting bin pred finit v
  -> Instruction       -- ^ The instruction
  -> [ResolvedJumpTarget]
get_known_jump_targets :: forall bin pred finit v.
BinaryClass bin =>
Lifting bin pred finit v -> Instruction -> [ResolvedJumpTarget]
get_known_jump_targets l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
l0) Instruction
i =
  case Word64 -> L0 pred finit v -> Maybe Indirections
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe Indirections
l0_lookup_indirection (Instruction -> Word64
inAddress Instruction
i) L0 pred finit v
l0 of
    Just Indirections
r -> Set ResolvedJumpTarget -> [ResolvedJumpTarget]
forall a. Set a -> [a]
S.toList (Set ResolvedJumpTarget -> [ResolvedJumpTarget])
-> Set ResolvedJumpTarget -> [ResolvedJumpTarget]
forall a b. (a -> b) -> a -> b
$ Set (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (Set (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget)
-> Set (Set ResolvedJumpTarget) -> Set ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ (Indirection -> Set ResolvedJumpTarget)
-> Indirections -> Set (Set ResolvedJumpTarget)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Indirection -> Set ResolvedJumpTarget
indirection_to_jump_target Indirections
r
    Maybe Indirections
_      -> ResolvedJumpTarget -> [ResolvedJumpTarget]
forall a. a -> [a]
singleton (ResolvedJumpTarget -> [ResolvedJumpTarget])
-> ResolvedJumpTarget -> [ResolvedJumpTarget]
forall a b. (a -> b) -> a -> b
$ bin -> Instruction -> ResolvedJumpTarget
forall bin.
BinaryClass bin =>
bin -> Instruction -> ResolvedJumpTarget
jump_target_for_instruction bin
bin Instruction
i
 where
  indirection_to_jump_target :: Indirection -> Set ResolvedJumpTarget
indirection_to_jump_target (Indirection_JumpTable (JumpTable Operand
_ Int
_ Operand
_ IntMap Word64
tbl)) = [ResolvedJumpTarget] -> Set ResolvedJumpTarget
forall a. Ord a => [a] -> Set a
S.fromList ([ResolvedJumpTarget] -> Set ResolvedJumpTarget)
-> [ResolvedJumpTarget] -> Set ResolvedJumpTarget
forall a b. (a -> b) -> a -> b
$ (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
  indirection_to_jump_target (Indirection_Resolved ResolvedJumpTarget
trgt) = ResolvedJumpTarget -> Set ResolvedJumpTarget
forall a. a -> Set a
S.singleton ResolvedJumpTarget
trgt
  indirection_to_jump_target (Indirection
Indirection_Unresolved) = ResolvedJumpTarget -> Set ResolvedJumpTarget
forall a. a -> Set a
S.singleton ResolvedJumpTarget
Unresolved








instance IntGraph CFG where
  intgraph_V :: CFG -> IntSet
intgraph_V    = IntMap [Int] -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet (IntMap [Int] -> IntSet) -> (CFG -> IntMap [Int]) -> CFG -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG -> IntMap [Int]
cfg_blocks
  intgraph_post :: CFG -> Int -> IntSet
intgraph_post = CFG -> Int -> IntSet
post
   where
    post :: CFG -> IS.Key -> IS.IntSet
    post :: CFG -> Int -> IntSet
post CFG
g Int
blockId = IntSet -> Maybe IntSet -> IntSet
forall a. a -> Maybe a -> a
fromMaybe IntSet
IS.empty (Int -> IntMap IntSet -> Maybe IntSet
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockId (CFG -> IntMap IntSet
cfg_edges CFG
g))
-- | Export a CFG to .dot file
--
-- Strongly connected components get the same color.
cfg_to_dot ::
  BinaryClass bin =>
     bin
  -> FResult pred v
  -> String
cfg_to_dot :: forall bin pred v.
BinaryClass bin =>
bin -> FResult pred v -> String
cfg_to_dot bin
bin (FResult CFG
g Postcondition pred
post Set Word64
_ Set (VerificationCondition v)
_ IntMap (PointerAnalysisResult v)
_) =
 let name :: String
name = bin -> String
forall a. BinaryClass a => a -> String
binary_file_name bin
bin
     sccs :: [IntSet]
sccs = CFG -> Int -> IntSet -> [IntSet]
forall g. IntGraph g => g -> Int -> IntSet -> [IntSet]
scc_of CFG
g Int
0 IntSet
IS.empty in
  String
"diGraph " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"{\n"
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (CFG -> Postcondition pred -> [IntSet] -> Int -> String
forall {b}. CFG -> Postcondition b -> [IntSet] -> Int -> String
node_to_dot CFG
g Postcondition pred
post [IntSet]
sccs) ([Int] -> [String]) -> [Int] -> [String]
forall a b. (a -> b) -> a -> b
$ IntMap [Int] -> [Int]
forall a. IntMap a -> [Int]
IM.keys (IntMap [Int] -> [Int]) -> IntMap [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Int]
cfg_blocks CFG
g)
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (((Int, IntSet) -> String) -> [(Int, IntSet)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, IntSet) -> String
forall {a}. Integral a => (a, IntSet) -> String
edge_to_dot' ([(Int, IntSet)] -> [String]) -> [(Int, IntSet)] -> [String]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.toList (IntMap IntSet -> [(Int, IntSet)])
-> IntMap IntSet -> [(Int, IntSet)]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap IntSet
cfg_edges CFG
g)
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n}"
 where
  node_to_dot :: CFG -> Postcondition b -> [IntSet] -> Int -> String
node_to_dot CFG
g Postcondition b
post [IntSet]
sccs Int
blockId =
    let bgcolor :: String
bgcolor = Int -> [IntSet] -> String
hex_color_of Int
blockId [IntSet]
sccs
        fgcolor :: String
fgcolor = ShowS
hex_color_of_text String
bgcolor in
       String
"\t" 
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Integral a => a -> String
mk_node Int
blockId
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  ["
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"style=filled fillcolor=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
bgcolor String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" fontcolor=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fgcolor String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" shape=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Postcondition b -> Int -> String
forall {b}. Postcondition b -> Int -> String
node_shape Postcondition b
post Int
blockId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"label=\""
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ CFG -> Int -> String
show_block CFG
g Int
blockId
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"]"

  edge_to_dot' :: (a, IntSet) -> String
edge_to_dot' (a
blockId, IntSet
blockIds) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> String
forall {a} {a}. (Integral a, Integral a) => a -> a -> String
edge_to_dot'' a
blockId) ([Int] -> [String]) -> [Int] -> [String]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList IntSet
blockIds

  edge_to_dot'' :: a -> a -> String
edge_to_dot'' a
blockId a
blockId' = String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Integral a => a -> String
mk_node a
blockId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Integral a => a -> String
mk_node a
blockId'

  mk_node :: a -> String
mk_node a
v = bin -> String
forall a. BinaryClass a => a -> String
binary_file_name bin
bin String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Integral a => a -> String
showHex a
v

  node_shape :: Postcondition b -> Int -> String
node_shape (ReturnsWith b
_) Int
blockId = String
"oval"
  node_shape (Postcondition b
Terminates) Int
blockId = String
"terminator"
  node_shape (Postcondition b
TimeOut) Int
blockId = String
"invtriangle"
  node_shape (HasUnresolvedIndirections [Int]
blockIDs) Int
blockId 
    | Int
blockId Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
blockIDs = String
"box3d"
    | Bool
otherwise = String
"oval"
  node_shape (VerificationError [(Int, b)]
errors) Int
blockId 
    | Int
blockId Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Int, b) -> Int) -> [(Int, b)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, b) -> Int
forall a b. (a, b) -> a
fst [(Int, b)]
errors = String
"invtriangle"
    | Bool
otherwise = String
"oval"
    


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



-- | Shows the block associated to the givern blockID.
show_block ::
  CFG    -- ^ The CFG
  -> Int -- ^ The blockID
  -> String
show_block :: CFG -> Int -> String
show_block CFG
g Int
b =
  let instrs :: [Int]
instrs = CFG -> IntMap [Int]
cfg_blocks CFG
g IntMap [Int] -> Int -> [Int]
forall a. IntMap a -> Int -> a
IM.! Int
b in
       Int -> String
forall a. Show a => a -> String
show Int
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ["
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Integral a => a -> String
showHex ([Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int]
instrs)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Integral a => a -> String
showHex ([Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
instrs)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"