{-# LANGUAGE DeriveGeneric, StrictData #-}

module WithAbstractPredicates.GenerateCFG where

import Base
import Config

import WithAbstractPredicates.Class
import WithAbstractPredicates.ControlFlow


import Binary.Generic
import Data.JumpTarget
import Data.Symbol
import Data.L0
import Data.CFG
import Data.X86.Opcode
import Data.X86.Instruction


import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.Word
import Data.Maybe
import Control.Monad.Extra



-- CONTROL FLOW

-- | Produce a CFG
generate_cfg ::
  WithAbstractPredicates bin pred finit v =>
     Lifting bin pred finit v
  -> Word64 -- ^ The entry point of the function
  -> CFG
generate_cfg :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> Word64 -> CFG
generate_cfg l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
_) Word64
entry =
  let g :: CFG
g           = Word64 -> CFG
forall {a}. Integral a => a -> CFG
init_cfg Word64
entry
      i :: Maybe Instruction
i           = bin -> Word64 -> Maybe Instruction
forall bin. BinaryClass bin => bin -> Word64 -> Maybe Instruction
fetch_instruction bin
bin Word64
entry
      nxt :: NextRips
nxt         = Lifting bin pred finit v -> Maybe Instruction -> NextRips
forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Maybe Instruction -> NextRips
next_rips Lifting bin pred finit v
l Maybe Instruction
i
      bag :: Set (Word64, Word64)
bag         = [(Word64, Word64)] -> Set (Word64, Word64)
forall a. Ord a => [a] -> Set a
S.fromList ([(Word64, Word64)] -> Set (Word64, Word64))
-> [(Word64, Word64)] -> Set (Word64, Word64)
forall a b. (a -> b) -> a -> b
$ (\(JustRips [Word64]
as) -> (Word64 -> (Word64, Word64)) -> [Word64] -> [(Word64, Word64)]
forall a b. (a -> b) -> [a] -> [b]
map (\Word64
a -> (Word64
entry,Word64
a)) [Word64]
as) NextRips
nxt 
      g' :: CFG
g'          = Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
mk_graph Lifting bin pred finit v
l Word64
entry Set (Word64, Word64)
bag CFG
g 
      g'' :: CFG
g''         = Lifting bin pred finit v -> CFG -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> CFG -> CFG
cfg_add_instrs Lifting bin pred finit v
l CFG
g' in
    CFG
g''


mk_graph :: WithAbstractPredicates bin pred finit v => Lifting bin pred finit v -> Word64 -> S.Set (Word64, Word64) -> CFG -> CFG
mk_graph :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
mk_graph l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
_) Word64
entry Set (Word64, Word64)
bag CFG
g =
  case Set (Word64, Word64)
-> Maybe ((Word64, Word64), Set (Word64, Word64))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (Word64, Word64)
bag of
    Maybe ((Word64, Word64), Set (Word64, Word64))
Nothing -> CFG
g
    Just ((Word64
a0,Word64
a1),Set (Word64, Word64)
bag) ->
      if CFG -> Int -> Int -> Bool
is_edge CFG
g (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0) (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1) then 
        Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
mk_graph Lifting bin pred finit v
l Word64
entry Set (Word64, Word64)
bag CFG
g
      else
        let g' :: CFG
g' = Int -> Int -> Bool -> CFG -> CFG
add_edge (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a0) (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a1) (Word64 -> Bool
is_call Word64
a0) CFG
g in
          case Lifting bin pred finit v -> Maybe Instruction -> NextRips
forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Maybe Instruction -> NextRips
next_rips Lifting bin pred finit v
l (bin -> Word64 -> Maybe Instruction
forall bin. BinaryClass bin => bin -> Word64 -> Maybe Instruction
fetch_instruction bin
bin Word64
a1) of
            JustRips [Word64]
as -> let bag' :: Set (Word64, Word64)
bag' = Set (Word64, Word64)
-> Set (Word64, Word64) -> Set (Word64, Word64)
forall a. Ord a => Set a -> Set a -> Set a
S.union ([(Word64, Word64)] -> Set (Word64, Word64)
forall a. Ord a => [a] -> Set a
S.fromList ([(Word64, Word64)] -> Set (Word64, Word64))
-> [(Word64, Word64)] -> Set (Word64, Word64)
forall a b. (a -> b) -> a -> b
$ (Word64 -> (Word64, Word64)) -> [Word64] -> [(Word64, Word64)]
forall a b. (a -> b) -> [a] -> [b]
map (\Word64
a2 -> (Word64
a1,Word64
a2)) [Word64]
as) Set (Word64, Word64)
bag in
                             Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
mk_graph Lifting bin pred finit v
l Word64
entry Set (Word64, Word64)
bag' CFG
g' 
            NextRips
_           -> Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v
-> Word64 -> Set (Word64, Word64) -> CFG -> CFG
mk_graph Lifting bin pred finit v
l Word64
entry Set (Word64, Word64)
bag CFG
g'
 where
  is_call :: Word64 -> Bool
is_call Word64
a =
    let i :: Maybe Instruction
i = bin -> Word64 -> Maybe Instruction
forall bin. BinaryClass bin => bin -> Word64 -> Maybe Instruction
fetch_instruction bin
bin Word64
a in
      Opcode -> Bool
isCall (Opcode -> Bool) -> Opcode -> Bool
forall a b. (a -> b) -> a -> b
$ Instruction -> Opcode
inOperation (Instruction -> Opcode) -> Instruction -> Opcode
forall a b. (a -> b) -> a -> b
$ Maybe Instruction -> Instruction
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Instruction
i






-- CONTROL FLOW GRAPH

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

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

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



add_to_intset :: Int -> Maybe IntSet -> Maybe IntSet
add_to_intset Int
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
$ Int -> IntSet
IS.singleton Int
a
add_to_intset Int
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
$ Int -> IntSet -> IntSet
IS.insert Int
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 :: Int -> Int -> Bool -> CFG -> CFG
add_edge Int
a0 Int
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 = Int -> CFG -> Maybe CFG
split_graph' Int
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
>=> Int -> CFG -> Maybe CFG
split_graph Int
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
>=> Int -> Int -> CFG -> Maybe CFG
add_edge_to_graph Int
a0 Int
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
>=> Int -> Bool -> CFG -> Maybe CFG
split_calls Int
a0 Bool
is_call_a0
  split_calls :: Int -> Bool -> CFG -> Maybe CFG
split_calls Int
a Bool
True  = Int -> CFG -> Maybe CFG
split_graph' Int
a
  split_calls Int
a Bool
False = CFG -> Maybe CFG
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return

fromJust' :: a -> [a] -> Maybe a -> a
fromJust' a
instrs [a]
as Maybe a
Nothing = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [a] -> [Char]
forall {a}. Integral a => [a] -> [Char]
showHex_list [a]
as [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
instrs
fromJust' a
_ [a]
_ (Just a
a) = a
a

cfg_add_instrs ::
  WithAbstractPredicates bin pred finit v =>
     Lifting bin pred finit v
  -> CFG
  -> CFG
cfg_add_instrs :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
Lifting bin pred finit v -> CFG -> CFG
cfg_add_instrs l :: Lifting bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
_) CFG
g =
  let instrs :: [(Int, [Instruction])]
instrs = ((Int, [Int]) -> (Int, [Instruction]))
-> [(Int, [Int])] -> [(Int, [Instruction])]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Int]) -> (Int, [Instruction])
forall {a} {a}. Integral a => (a, [a]) -> (a, [Instruction])
block_to_instrs (IntMap [Int] -> [(Int, [Int])]
forall a. IntMap a -> [(Int, a)]
IM.toList (IntMap [Int] -> [(Int, [Int])]) -> IntMap [Int] -> [(Int, [Int])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Int]
cfg_blocks CFG
g) in
    CFG
g { cfg_instrs = IM.fromList instrs }
 where
  block_to_instrs :: (a, [a]) -> (a, [Instruction])
block_to_instrs (a
a,[a]
as) =
    let instrs :: [Maybe Instruction]
instrs = (a -> Maybe Instruction) -> [a] -> [Maybe Instruction]
forall a b. (a -> b) -> [a] -> [b]
map (bin -> Word64 -> Maybe Instruction
forall bin. BinaryClass bin => bin -> Word64 -> Maybe Instruction
fetch_instruction bin
bin (Word64 -> Maybe Instruction)
-> (a -> Word64) -> a -> 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 in
      (a
a, (Maybe Instruction -> Instruction)
-> [Maybe Instruction] -> [Instruction]
forall a b. (a -> b) -> [a] -> [b]
map ([Maybe Instruction] -> [a] -> Maybe Instruction -> Instruction
forall {a} {a} {a}.
(Integral a, Show a) =>
a -> [a] -> Maybe a -> a
fromJust' [Maybe Instruction]
instrs [a]
as) [Maybe Instruction]
instrs)



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