{-# LANGUAGE PartialTypeSignatures, MultiParamTypeClasses, DeriveGeneric, DefaultSignatures, FlexibleContexts, StrictData #-}


{-# OPTIONS_HADDOCK hide #-}


module Data.CallGraph where

import Analysis.Context
import Data.Binary
import Base
import Data.ControlFlow
import Data.MachineState
import Data.Pointers
import Data.SimplePred

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.List
import Data.List.Split (chunksOf)
import Data.List.Extra (groupSort)
import Data.Maybe (fromJust)
import Debug.Trace
import X86.Opcode (isCall)
import qualified Generic.Instruction as Instr
import Typeclasses.HasAddress (addressof)

pp_bot :: SimpleExpr -> [Char]
pp_bot (Bottom (FromSources Set BotSrc
srcs))    = if Set BotSrc -> Int
forall a. Set a -> Int
S.size Set BotSrc
srcs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 then [Char]
"Bot" else [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ((BotSrc -> [Char]) -> [BotSrc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map BotSrc -> [Char]
pp_source ([BotSrc] -> [[Char]]) -> [BotSrc] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs)
pp_bot (Bottom (FromPointerBases Set PointerBase
bs)) = if Set PointerBase -> Int
forall a. Set a -> Int
S.size Set PointerBase
bs   Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 then [Char]
"Bot" else [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ((PointerBase -> [Char]) -> [PointerBase] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map PointerBase -> [Char]
pp_base ([PointerBase] -> [[Char]]) -> [PointerBase] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs)
pp_bot SimpleExpr
e                              = SimpleExpr -> [Char]
pp_expr SimpleExpr
e

pp_base :: PointerBase -> [Char]
pp_base (StackPointer [Char]
f)        = [Char]
"StackPointer of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f
pp_base (Malloc Maybe Word64
id Maybe [Char]
h)           = SimpleExpr -> [Char]
pp_expr (SimpleExpr -> [Char]) -> SimpleExpr -> [Char]
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
h
pp_base (GlobalAddress Word64
a)       = Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
a
pp_base (PointerToSymbol Word64
a [Char]
sym) = [Char]
"&" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
sym

pp_source :: BotSrc -> [Char]
pp_source (Src_Var StatePart
v)              = SimpleExpr -> [Char]
pp_expr (SimpleExpr -> [Char]) -> SimpleExpr -> [Char]
forall a b. (a -> b) -> a -> b
$ StatePart -> SimpleExpr
SE_Var StatePart
v
pp_source (Src_StackPointer [Char]
f)     = [Char]
"StackPointer of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f
pp_source (Src_Malloc Maybe Word64
id Maybe [Char]
h)        = SimpleExpr -> [Char]
pp_expr (SimpleExpr -> [Char]) -> SimpleExpr -> [Char]
forall a b. (a -> b) -> a -> b
$ Maybe Word64 -> Maybe [Char] -> SimpleExpr
SE_Malloc Maybe Word64
id Maybe [Char]
h
pp_source (Src_Function [Char]
f)         = [Char]
f
pp_source (Src_ImmediateAddress Word64
a) = Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
a


pp_statepart :: StatePart -> [Char]
pp_statepart (SP_Mem SimpleExpr
a Int
si)       = [Char]
"[" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> [Char]
pp_bot SimpleExpr
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"," [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
si [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"
pp_statepart (SP_StackPointer [Char]
f) = [Char]
"StackPointer of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f
pp_statepart (SP_Reg Register
r)          = Register -> [Char]
forall a. Show a => a -> [Char]
show Register
r

pp_dom :: PointerDomain -> [Char]
pp_dom (Domain_Bases Set PointerBase
bs)     = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ((PointerBase -> [Char]) -> [PointerBase] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map PointerBase -> [Char]
pp_base ([PointerBase] -> [[Char]]) -> [PointerBase] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set PointerBase -> [PointerBase]
forall a. Set a -> [a]
S.toList Set PointerBase
bs)
pp_dom (Domain_Sources Set BotSrc
srcs) = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ((BotSrc -> [Char]) -> [BotSrc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map BotSrc -> [Char]
pp_source ([BotSrc] -> [[Char]]) -> [BotSrc] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set BotSrc -> [BotSrc]
forall a. Set a -> [a]
S.toList Set BotSrc
srcs)

-- | Summarize preconditions
summarize_preconditions :: (SimpleExpr -> a)
-> (a -> [Char]) -> Set VerificationCondition -> [Char]
summarize_preconditions SimpleExpr -> a
get_info a -> [Char]
show_e Set VerificationCondition
vcs =
  let pointer_pairs :: [(a, a)]
pointer_pairs = (VerificationCondition -> (a, a))
-> [VerificationCondition] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> (a, a)
get_pointer_pair ([VerificationCondition] -> [(a, a)])
-> [VerificationCondition] -> [(a, a)]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList (Set VerificationCondition -> [VerificationCondition])
-> Set VerificationCondition -> [VerificationCondition]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_precondition Set VerificationCondition
vcs
      groups :: [(a, [a])]
groups        = [(a, a)] -> [(a, [a])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort [(a, a)]
pointer_pairs in
    if [(a, [a])]
groups [(a, [a])] -> [(a, [a])] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
      [Char]
""
    else
      [Char]
"PRECONDITIONS:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((a, [a]) -> [Char]) -> [(a, [a])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (a, [a]) -> [Char]
show_group [(a, [a])]
groups) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where
  get_pointer_pair :: VerificationCondition -> (a, a)
get_pointer_pair (Precondition SimpleExpr
a0 Int
_ SimpleExpr
a1 Int
_) = (SimpleExpr -> a
get_info SimpleExpr
a0, SimpleExpr -> a
get_info SimpleExpr
a1)
  show_group :: (a, [a]) -> [Char]
show_group (a
a,[a]
as) = a -> [Char]
show_e a
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" SEP " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
nub ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (a -> [Char]) -> [a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map a -> [Char]
show_e [a]
as)

summarize_preconditions_short :: FContext -> Set VerificationCondition -> [Char]
summarize_preconditions_short FContext
ctxt = (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> [Char]) -> Set VerificationCondition -> [Char]
forall a.
Ord a =>
(SimpleExpr -> a)
-> (a -> [Char]) -> Set VerificationCondition -> [Char]
summarize_preconditions (FContext -> SimpleExpr -> SimpleExpr
join_single FContext
ctxt) SimpleExpr -> [Char]
pp_bot
summarize_preconditions_long :: p -> Set VerificationCondition -> [Char]
summarize_preconditions_long  p
ctxt = (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> [Char]) -> Set VerificationCondition -> [Char]
forall a.
Ord a =>
(SimpleExpr -> a)
-> (a -> [Char]) -> Set VerificationCondition -> [Char]
summarize_preconditions SimpleExpr -> SimpleExpr
forall a. a -> a
id SimpleExpr -> [Char]
forall a. Show a => a -> [Char]
show




-- | Summarize assertions
summarize_assertions :: (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> [Char]) -> Set VerificationCondition -> [Char]
summarize_assertions SimpleExpr -> SimpleExpr
get_info SimpleExpr -> [Char]
show_e Set VerificationCondition
vcs =
  let instr_assert_pairs :: [(SimpleExpr, (SimpleExpr, SimpleExpr))]
instr_assert_pairs      = (VerificationCondition -> (SimpleExpr, (SimpleExpr, SimpleExpr)))
-> [VerificationCondition]
-> [(SimpleExpr, (SimpleExpr, SimpleExpr))]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> (SimpleExpr, (SimpleExpr, SimpleExpr))
get_instr_assert_pair ([VerificationCondition]
 -> [(SimpleExpr, (SimpleExpr, SimpleExpr))])
-> [VerificationCondition]
-> [(SimpleExpr, (SimpleExpr, SimpleExpr))]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList (Set VerificationCondition -> [VerificationCondition])
-> Set VerificationCondition -> [VerificationCondition]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_assertion Set VerificationCondition
vcs
      per_instruction :: [(SimpleExpr, [(SimpleExpr, SimpleExpr)])]
per_instruction         = [(SimpleExpr, (SimpleExpr, SimpleExpr))]
-> [(SimpleExpr, [(SimpleExpr, SimpleExpr)])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort [(SimpleExpr, (SimpleExpr, SimpleExpr))]
instr_assert_pairs
      per_instruction_grouped :: [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
per_instruction_grouped = ((SimpleExpr, [(SimpleExpr, SimpleExpr)])
 -> (SimpleExpr, [(SimpleExpr, [SimpleExpr])]))
-> [(SimpleExpr, [(SimpleExpr, SimpleExpr)])]
-> [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
forall a b. (a -> b) -> [a] -> [b]
map (\(SimpleExpr
rip,[(SimpleExpr, SimpleExpr)]
pairs) -> (SimpleExpr
rip, [(SimpleExpr, SimpleExpr)] -> [(SimpleExpr, [SimpleExpr])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort [(SimpleExpr, SimpleExpr)]
pairs)) [(SimpleExpr, [(SimpleExpr, SimpleExpr)])]
per_instruction in
    if [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
per_instruction_grouped [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
-> [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
      [Char]
""
    else
      [Char]
"ASSERTIONS:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, [(SimpleExpr, [SimpleExpr])]) -> [Char])
-> [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleExpr, [(SimpleExpr, [SimpleExpr])]) -> [Char]
show_instr_group [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
per_instruction_grouped) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where
  get_instr_assert_pair :: VerificationCondition -> (SimpleExpr, (SimpleExpr, SimpleExpr))
get_instr_assert_pair (Assertion SimpleExpr
rip SimpleExpr
a0 Int
_ SimpleExpr
a1 Int
_) = (SimpleExpr
rip, (SimpleExpr
a0, SimpleExpr -> SimpleExpr
get_info SimpleExpr
a1))
  show_instr_group :: (SimpleExpr, [(SimpleExpr, [SimpleExpr])]) -> [Char]
show_instr_group (SimpleExpr
rip,[(SimpleExpr, [SimpleExpr])]
groups) = [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> [Char]
show_e SimpleExpr
rip [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate[Char]
" && " (((SimpleExpr, [SimpleExpr]) -> [Char])
-> [(SimpleExpr, [SimpleExpr])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleExpr, [SimpleExpr]) -> [Char]
show_group [(SimpleExpr, [SimpleExpr])]
groups)
  show_group :: (SimpleExpr, [SimpleExpr]) -> [Char]
show_group (SimpleExpr
a,[SimpleExpr]
as) = SimpleExpr -> [Char]
show_e SimpleExpr
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" SEP " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
nub ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> [Char]) -> [SimpleExpr] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> [Char]
show_e [SimpleExpr]
as)

summarize_assertions_short :: FContext -> Set VerificationCondition -> [Char]
summarize_assertions_short FContext
ctxt = (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> [Char]) -> Set VerificationCondition -> [Char]
summarize_assertions (FContext -> SimpleExpr -> SimpleExpr
join_single FContext
ctxt) SimpleExpr -> [Char]
pp_bot
summarize_assertions_long :: p -> Set VerificationCondition -> [Char]
summarize_assertions_long  p
ctxt = (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> [Char]) -> Set VerificationCondition -> [Char]
summarize_assertions SimpleExpr -> SimpleExpr
forall a. a -> a
id SimpleExpr -> [Char]
forall a. Show a => a -> [Char]
show


-- | Summarize function constraints
summarize_function_constraints_short :: FContext -> Set VerificationCondition -> [Char]
summarize_function_constraints_short FContext
ctxt Set VerificationCondition
vcs =
  let fcs :: Set VerificationCondition
fcs = (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_func_constraint Set VerificationCondition
vcs in
    if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
fcs then
      [Char]
""
    else
      [Char]
"FUNCTION CONSTRAINTS:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> [Char])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> [Char]
summarize_fcs ([VerificationCondition] -> [[Char]])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fcs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where
  summarize_fcs :: VerificationCondition -> [Char]
summarize_fcs (FunctionConstraint [Char]
f Word64
i_a [(Register, SimpleExpr)]
params Set StatePart
sps) = [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
i_a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
parens ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((Register, SimpleExpr) -> [Char])
-> [(Register, SimpleExpr)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Register, SimpleExpr) -> [Char]
forall a. Show a => (a, SimpleExpr) -> [Char]
show_param [(Register, SimpleExpr)]
params) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" PRESERVES " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Set StatePart -> [Char]
show_sps Set StatePart
sps

  show_param :: (a, SimpleExpr) -> [Char]
show_param (a
r,SimpleExpr
e) = a -> [Char]
forall a. Show a => a -> [Char]
show a
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> [Char]
show_param_eq_sign SimpleExpr
e [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
strip_parentheses (SimpleExpr -> [Char]
show_param_value SimpleExpr
e)
  show_param_value :: SimpleExpr -> [Char]
show_param_value SimpleExpr
e = if Bool -> Bool
not (SimpleExpr -> Bool
contains_bot SimpleExpr
e) then SimpleExpr -> [Char]
pp_bot SimpleExpr
e else SimpleExpr -> [Char]
pp_bot (SimpleExpr -> [Char]) -> SimpleExpr -> [Char]
forall a b. (a -> b) -> a -> b
$ FContext -> SimpleExpr -> SimpleExpr
join_single FContext
ctxt SimpleExpr
e
  show_param_eq_sign :: SimpleExpr -> [Char]
show_param_eq_sign SimpleExpr
e = if SimpleExpr -> Bool
contains_bot SimpleExpr
e then [Char]
"~=" else [Char]
":="

  show_sps :: Set StatePart -> [Char]
show_sps Set StatePart
sps =
    let ([StatePart]
stackframe,[StatePart]
others) = (StatePart -> Bool) -> [StatePart] -> ([StatePart], [StatePart])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition StatePart -> Bool
is_stack_frame ([StatePart] -> ([StatePart], [StatePart]))
-> [StatePart] -> ([StatePart], [StatePart])
forall a b. (a -> b) -> a -> b
$ Set StatePart -> [StatePart]
forall a. Set a -> [a]
S.toList Set StatePart
sps
        showed_stack_frame :: [Char]
showed_stack_frame  = [StatePart] -> [Char]
show_stack_frame [StatePart]
stackframe in
      [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
(/=) []) ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char]
showed_stack_frame [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (StatePart -> [Char]) -> [StatePart] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map StatePart -> [Char]
pp_statepart [StatePart]
others

  is_stack_frame :: StatePart -> Bool
is_stack_frame (SP_Mem (SE_Op (Minus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
_]) Int
_) = Bool
True
  is_stack_frame (SP_Mem (SE_Var (SP_StackPointer [Char]
_)) Int
_)                                   = Bool
True
  is_stack_frame StatePart
sp                                                                        = Bool
False


  show_stack_frame :: [StatePart] -> [Char]
show_stack_frame [StatePart]
sps =
    if [StatePart]
sps  [StatePart] -> [StatePart] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
      [Char]
""
    else let offset :: Word64
offset = [Word64] -> Word64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Word64] -> Word64) -> [Word64] -> Word64
forall a b. (a -> b) -> a -> b
$ (StatePart -> Word64) -> [StatePart] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map StatePart -> Word64
get_offset [StatePart]
sps
             top :: Int
top    = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (StatePart -> Int) -> [StatePart] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map StatePart -> Int
get_top [StatePart]
sps in
      [Char]
"[ RSP_0 - " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. Show a => a -> [Char]
show Word64
offset [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" TO RSP_0" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (if Int
top Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then [Char]
"" else [Char]
" + " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
top) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ]"

  get_offset :: StatePart -> Word64
get_offset (SP_Mem (SE_Op (Minus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
offset]) Int
_) = Word64
offset
  get_offset (SP_Mem (SE_Var (SP_StackPointer [Char]
_)) Int
_)                                        = Word64
0

  get_top :: StatePart -> Int
get_top (SP_Mem (SE_Op (Minus Int
_) [SE_Var (SP_StackPointer [Char]
_), SE_Immediate Word64
offset]) Int
si) = Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
offset
  get_top (SP_Mem (SE_Var (SP_StackPointer [Char]
_)) Int
si)                                        = Int
si

summarize_function_constraints_long :: Context -> S.Set VerificationCondition -> String
summarize_function_constraints_long :: Context -> Set VerificationCondition -> [Char]
summarize_function_constraints_long Context
ctxt Set VerificationCondition
vcs =
  let fcs :: Set VerificationCondition
fcs = (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_func_constraint Set VerificationCondition
vcs in
    if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
fcs then
      [Char]
""
    else
      [Char]
"FUNCTION CONSTRAINTS:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> [Char])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> [Char]
forall a. Show a => a -> [Char]
show ([VerificationCondition] -> [[Char]])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fcs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"


-- | Summarize sourceless memwrites
summarize_sourceless_memwrites_short :: p -> Set VerificationCondition -> [Char]
summarize_sourceless_memwrites_short p
ctxt Set VerificationCondition
vcs =
  let mws :: Set VerificationCondition
mws = (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_sourceless_memwrite Set VerificationCondition
vcs in
    if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
mws then
      [Char]
""
    else
      [Char]
"SOURCELESS MEM WRITES:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" (([[Char]] -> [Char]) -> [[[Char]]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
",") ([[[Char]]] -> [[Char]]) -> [[[Char]]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Int -> [[Char]] -> [[[Char]]]
forall e. Int -> [e] -> [[e]]
chunksOf Int
5 ([[Char]] -> [[[Char]]]) -> [[Char]] -> [[[Char]]]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
nub ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> [Char])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> [Char]
get_location ([VerificationCondition] -> [[Char]])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
mws) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where
   get_location :: VerificationCondition -> [Char]
get_location (SourcelessMemWrite (MemWriteFunction [Char]
f Word64
a StatePart
sp))       = [Char]
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
a
   get_location (SourcelessMemWrite (MemWriteInstruction Word64
a Operand
addr SimpleExpr
a')) = [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
showHex Word64
a

summarize_sourceless_memwrites_long :: p -> Set VerificationCondition -> [Char]
summarize_sourceless_memwrites_long p
ctxt Set VerificationCondition
vcs =
  let mws :: Set VerificationCondition
mws = (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_sourceless_memwrite Set VerificationCondition
vcs in
    if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
mws then
      [Char]
""
    else
      [Char]
"SOURCELESS MEM WRITES:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> [Char])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> [Char]
forall a. Show a => a -> [Char]
show ([VerificationCondition] -> [[Char]])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
mws) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"



summarize_function_pointers :: p -> Set VerificationCondition -> [Char]
summarize_function_pointers p
ctxt Set VerificationCondition
vcs =
  let fptrs :: Set VerificationCondition
fptrs = (VerificationCondition -> Bool)
-> Set VerificationCondition -> Set VerificationCondition
forall a. (a -> Bool) -> Set a -> Set a
S.filter VerificationCondition -> Bool
is_functionpointers Set VerificationCondition
vcs in
    if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
fptrs then
      [Char]
""
    else
      [Char]
"FUNCTION POINTERS USED:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> [Char])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> [Char]
forall a. Show a => a -> [Char]
show ([VerificationCondition] -> [[Char]])
-> [VerificationCondition] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fptrs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"

-- | Summarize function initialization
summarize_finit :: Maybe (Map StatePart SimpleExpr) -> [Char]
summarize_finit Maybe (Map StatePart SimpleExpr)
Nothing      = [Char]
""
summarize_finit (Just Map StatePart SimpleExpr
finit) = if Map StatePart SimpleExpr -> Bool
forall k a. Map k a -> Bool
M.null Map StatePart SimpleExpr
finit then [Char]
"" else [Char]
"INITIAL:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((StatePart, SimpleExpr) -> [Char])
-> [(StatePart, SimpleExpr)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (StatePart, SimpleExpr) -> [Char]
show_finit_entry ([(StatePart, SimpleExpr)] -> [[Char]])
-> [(StatePart, SimpleExpr)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Map StatePart SimpleExpr -> [(StatePart, SimpleExpr)]
forall k a. Map k a -> [(k, a)]
M.toList Map StatePart SimpleExpr
finit) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where
  show_finit_entry :: (StatePart, SimpleExpr) -> [Char]
show_finit_entry (StatePart
sp,bot :: SimpleExpr
bot@(Bottom BotTyp
_)) = StatePart -> [Char]
pp_statepart StatePart
sp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ~= " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> [Char]
pp_bot SimpleExpr
bot
  show_finit_entry (StatePart
sp,SimpleExpr
v)              = StatePart -> [Char]
pp_statepart StatePart
sp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> [Char]
pp_expr SimpleExpr
v



-- TODO move
parens :: [Char] -> [Char]
parens [Char]
str = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
str [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

summarize_verification_conditions :: Context -> Int -> [Char]
summarize_verification_conditions Context
ctxt Int
entry =
  let vcs :: Set VerificationCondition
vcs        = Int
-> IntMap (Set VerificationCondition)
-> Maybe (Set VerificationCondition)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt) Maybe (Set VerificationCondition)
-> Set VerificationCondition -> Set VerificationCondition
forall p. Maybe p -> p -> p
`orElse` Set VerificationCondition
forall a. Set a
S.empty
      finit :: Maybe (Map StatePart SimpleExpr)
finit      = Int
-> IntMap (Map StatePart SimpleExpr)
-> Maybe (Map StatePart SimpleExpr)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap (Map StatePart SimpleExpr)
 -> Maybe (Map StatePart SimpleExpr))
-> IntMap (Map StatePart SimpleExpr)
-> Maybe (Map StatePart SimpleExpr)
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Map StatePart SimpleExpr)
ctxt_finits Context
ctxt
      fctxt :: FContext
fctxt      = Context -> Int -> FContext
mk_fcontext Context
ctxt Int
entry
      summary :: [Char]
summary    = Maybe (Map StatePart SimpleExpr) -> [Char]
summarize_finit Maybe (Map StatePart SimpleExpr)
finit
                   -- ++ summarize_preconditions_short fctxt vcs
                   -- ++ summarize_assertions_short ctxt vcs
                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FContext -> Set VerificationCondition -> [Char]
summarize_function_constraints_short FContext
fctxt Set VerificationCondition
vcs
                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Context -> Set VerificationCondition -> [Char]
forall p. p -> Set VerificationCondition -> [Char]
summarize_sourceless_memwrites_short Context
ctxt Set VerificationCondition
vcs
                   -- ++ summarize_function_pointer_intros ctxt vcs
                   in
    [Char] -> [Char]
butlast [Char]
summary
 where
  butlast :: [Char] -> [Char]
butlast [Char]
""  = [Char]
""
  butlast [Char]
str = [Char] -> [Char]
forall a. [a] -> [a]
init [Char]
str




calls_of_cfg :: Context -> CFG -> IntSet
calls_of_cfg Context
ctxt CFG
cfg = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ (GenericInstruction AddressWord64 Register Prefix Opcode Int
 -> IntSet)
-> [GenericInstruction AddressWord64 Register Prefix Opcode Int]
-> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map GenericInstruction AddressWord64 Register Prefix Opcode Int
-> IntSet
get_call_target ([GenericInstruction AddressWord64 Register Prefix Opcode Int]
 -> [IntSet])
-> [GenericInstruction AddressWord64 Register Prefix Opcode Int]
-> [IntSet]
forall a b. (a -> b) -> a -> b
$ [[GenericInstruction AddressWord64 Register Prefix Opcode Int]]
-> [GenericInstruction AddressWord64 Register Prefix Opcode Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[GenericInstruction AddressWord64 Register Prefix Opcode Int]]
 -> [GenericInstruction AddressWord64 Register Prefix Opcode Int])
-> [[GenericInstruction AddressWord64 Register Prefix Opcode Int]]
-> [GenericInstruction AddressWord64 Register Prefix Opcode Int]
forall a b. (a -> b) -> a -> b
$ IntMap
  [GenericInstruction AddressWord64 Register Prefix Opcode Int]
-> [[GenericInstruction AddressWord64 Register Prefix Opcode Int]]
forall a. IntMap a -> [a]
IM.elems (IntMap
   [GenericInstruction AddressWord64 Register Prefix Opcode Int]
 -> [[GenericInstruction AddressWord64 Register Prefix Opcode Int]])
-> IntMap
     [GenericInstruction AddressWord64 Register Prefix Opcode Int]
-> [[GenericInstruction AddressWord64 Register Prefix Opcode Int]]
forall a b. (a -> b) -> a -> b
$ CFG
-> IntMap
     [GenericInstruction AddressWord64 Register Prefix Opcode Int]
cfg_instrs CFG
cfg
 where
  get_call_target :: GenericInstruction AddressWord64 Register Prefix Opcode Int
-> IntSet
get_call_target GenericInstruction AddressWord64 Register Prefix Opcode Int
i =
    if Opcode -> Bool
isCall (GenericInstruction AddressWord64 Register Prefix Opcode Int
-> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode GenericInstruction AddressWord64 Register Prefix Opcode Int
i) then
      [Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (ResolvedJumpTarget -> [Int]) -> [ResolvedJumpTarget] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ResolvedJumpTarget -> [Int]
get_internal_addresses ([ResolvedJumpTarget] -> [Int]) -> [ResolvedJumpTarget] -> [Int]
forall a b. (a -> b) -> a -> b
$ Context
-> GenericInstruction AddressWord64 Register Prefix Opcode Int
-> [ResolvedJumpTarget]
resolve_jump_target Context
ctxt GenericInstruction AddressWord64 Register Prefix Opcode Int
i
    else
      IntSet
IS.empty


function_pointer_intros :: Context -> p -> IntSet
function_pointer_intros Context
ctxt p
cfg = IntSet
IS.empty -- IS.unions $ map get_function_pointers_of_call $ concat $ IM.elems $ cfg_instrs cfg
 where
  get_function_pointers_of_call :: GenericInstruction label storage prefix Opcode annotation -> IntSet
get_function_pointers_of_call GenericInstruction label storage prefix Opcode annotation
i =
    if Opcode -> Bool
isCall (GenericInstruction label storage prefix Opcode annotation -> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode GenericInstruction label storage prefix Opcode annotation
i) then -- TODO or jump?
      Set IntSet -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions (Set IntSet -> IntSet) -> Set IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> IntSet)
-> Set VerificationCondition -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Word64 -> VerificationCondition -> IntSet
get_function_pointers (Word64 -> VerificationCondition -> IntSet)
-> Word64 -> VerificationCondition -> IntSet
forall a b. (a -> b) -> a -> b
$ GenericInstruction label storage prefix Opcode annotation -> Word64
forall a. HasAddress a => a -> Word64
addressof GenericInstruction label storage prefix Opcode annotation
i) (Set VerificationCondition -> Set IntSet)
-> Set VerificationCondition -> Set IntSet
forall a b. (a -> b) -> a -> b
$ (IntMap (Set VerificationCondition) -> Set VerificationCondition
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (IntMap (Set VerificationCondition) -> Set VerificationCondition)
-> IntMap (Set VerificationCondition) -> Set VerificationCondition
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt)
    else
      IntSet
IS.empty

  get_function_pointers :: Word64 -> VerificationCondition -> IntSet
get_function_pointers Word64
a (FunctionPointers Word64
a' IntSet
ptrs) = if Word64
a Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
a' then (Int -> Bool) -> IntSet -> IntSet
IS.filter Int -> Bool
has_been_analyzed IntSet
ptrs else IntSet
IS.empty
  get_function_pointers Word64
_ VerificationCondition
_                          = IntSet
IS.empty

  has_been_analyzed :: Int -> Bool
has_been_analyzed Int
entry = Int -> IntMap FReturnBehavior -> Maybe FReturnBehavior
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (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


callgraph_to_dot :: Context -> Graph -> Graph -> String
callgraph_to_dot :: Context -> Graph -> Graph -> [Char]
callgraph_to_dot Context
ctxt (Edges IntMap IntSet
es) (Edges IntMap IntSet
fptrs) =
 let name :: [Char]
name  = Context -> [Char]
ctxt_name Context
ctxt 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" ((Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [Char]
node_to_dot ([Int] -> [[Char]]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [Int]
forall a. IntMap a -> [Int]
IM.keys IntMap IntSet
es)
  [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" (((Int, IntSet) -> [Char]) -> [(Int, IntSet)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> (Int, IntSet) -> [Char]
forall a. (Integral a, Show a) => [Char] -> (a, IntSet) -> [Char]
edge_to_dot' [Char]
"") ([(Int, IntSet)] -> [[Char]]) -> [(Int, IntSet)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.assocs IntMap IntSet
es)
  [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" (((Int, IntSet) -> [Char]) -> [(Int, IntSet)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> (Int, IntSet) -> [Char]
forall a. (Integral a, Show a) => [Char] -> (a, IntSet) -> [Char]
edge_to_dot' [Char]
"[style=dotted]") ([(Int, IntSet)] -> [[Char]]) -> [(Int, IntSet)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.assocs IntMap IntSet
fptrs)
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n}"
 where
  node_to_dot :: Int -> [Char]
node_to_dot Int
v =
    let bgcolor :: [Char]
bgcolor = Int -> [Char]
node_color Int
v
        fgcolor :: [Char]
fgcolor = [Char] -> [Char]
hex_color_of_text [Char]
bgcolor in
       [Char]
"\t"
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
mk_node Int
v
    [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]
++ Int -> [Char]
node_shape Int
v [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]
++ Int -> [Char]
node_label Int
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"

  edge_to_dot' :: [Char] -> (a, IntSet) -> [Char]
edge_to_dot'  [Char]
style (a
v,IntSet
vs) = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> a -> Int -> [Char]
forall a a.
(Integral a, Integral a, Show a, Show a) =>
[Char] -> a -> a -> [Char]
edge_to_dot'' [Char]
style a
v) ([Int] -> [[Char]]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList IntSet
vs
  edge_to_dot'' :: [Char] -> a -> a -> [Char]
edge_to_dot'' [Char]
style a
v a
v'   = [Char]
"\t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. (Integral a, Show a) => a -> [Char]
mk_node a
v [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
v'  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
style

  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 :: Int -> [Char]
node_shape Int
v =
    case Int -> IntMap VerificationResult -> Maybe VerificationResult
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap VerificationResult -> Maybe VerificationResult)
-> IntMap VerificationResult -> Maybe VerificationResult
forall a b. (a -> b) -> a -> b
$ Context -> IntMap VerificationResult
ctxt_results Context
ctxt of
      Just VerificationResult
VerificationSuccess               -> [Char]
"Mrecord"
      Just VerificationResult
VerificationSuccesWithAssumptions -> [Char]
"Mrecord"
      Maybe VerificationResult
_                                      -> [Char]
"record"

  node_label :: Int -> [Char]
node_label Int
v =
    let finit :: Maybe (Map StatePart SimpleExpr)
finit = Int
-> IntMap (Map StatePart SimpleExpr)
-> Maybe (Map StatePart SimpleExpr)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap (Map StatePart SimpleExpr)
 -> Maybe (Map StatePart SimpleExpr))
-> IntMap (Map StatePart SimpleExpr)
-> Maybe (Map StatePart SimpleExpr)
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Map StatePart SimpleExpr)
ctxt_finits Context
ctxt in
      case Int
-> IntMap (Set VerificationCondition)
-> Maybe (Set VerificationCondition)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap (Set VerificationCondition)
 -> Maybe (Set VerificationCondition))
-> IntMap (Set VerificationCondition)
-> Maybe (Set VerificationCondition)
forall a b. (a -> b) -> a -> b
$ Context -> IntMap (Set VerificationCondition)
ctxt_vcs Context
ctxt of
        Maybe (Set VerificationCondition)
Nothing  -> Context -> Int -> [Char]
function_name_of_entry Context
ctxt Int
v
        Just Set VerificationCondition
vcs ->
          if Set VerificationCondition -> Bool
forall a. Set a -> Bool
S.null Set VerificationCondition
vcs Bool -> Bool -> Bool
&& Maybe (Map StatePart SimpleExpr)
finit Maybe (Map StatePart SimpleExpr)
-> [Maybe (Map StatePart SimpleExpr)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Map StatePart SimpleExpr -> Maybe (Map StatePart SimpleExpr)
forall a. a -> Maybe a
Just Map StatePart SimpleExpr
forall k a. Map k a
M.empty,Maybe (Map StatePart SimpleExpr)
forall a. Maybe a
Nothing] then
            Context -> Int -> [Char]
function_name_of_entry Context
ctxt Int
v
          else
            [Char]
"{" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Context -> Int -> [Char]
function_name_of_entry Context
ctxt Int
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"|" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
markup (Context -> Int -> [Char]
summarize_verification_conditions Context
ctxt Int
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"}"

  node_color :: Int -> [Char]
node_color Int
v =
    let verified :: VerificationResult
verified = case Int -> IntMap VerificationResult -> Maybe VerificationResult
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (Context -> IntMap VerificationResult
ctxt_results Context
ctxt) of
                     Maybe VerificationResult
Nothing -> [Char] -> VerificationResult
VerificationError [Char]
"Verification error"
                     Just VerificationResult
v  -> VerificationResult
v
     in
      case VerificationResult
verified of
        VerificationResult
VerificationSuccess               -> [Char]
"#90EE90" -- light green
        VerificationResult
VerificationSuccesWithAssumptions -> [Char]
"#89CFF0" -- light blue
        VerificationError [Char]
_               -> [Char]
"#FF7F7F" -- light red
        VerificationResult
VerificationUnresolvedIndirection -> [Char]
"#CBC3E3" -- light purple





  markup :: [Char] -> [Char]
markup [Char]
vcs = Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
max_limit_node_text_size_as_indicated_by_graphviz ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replace [Char
c | Char
c <- [Char]
vcs, Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'|']

  replace :: Char -> Char
replace Char
'\n' = Char
'|'
  replace Char
c    = Char
c

  max_limit_node_text_size_as_indicated_by_graphviz :: Int
max_limit_node_text_size_as_indicated_by_graphviz = Int
15000