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


{-# OPTIONS_HADDOCK hide #-}


module OutputGeneration.CallGraph where

import Base

import Analysis.Context
import Analysis.ControlFlow
import Analysis.FunctionNames
import Analysis.Pointers

import Generic.SymbolicConstituents 

import Data.SymbolicExpression

import X86.Opcode (isCall)
import X86.Instruction (addressof)
import qualified Generic.Instruction as Instr


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 qualified Data.Set.NonEmpty as NES
import Data.List
import Data.List.Split (chunksOf)
import Data.List.Extra (groupSort)
import Data.Maybe (fromJust)
import Debug.Trace


mk_callgraph :: Context -> String
mk_callgraph Context
ctxt =
  let cfgs :: IntMap CFG
cfgs  = Context -> IntMap CFG
ctxt_cfgs Context
ctxt
      g :: Graph
g     = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ (CFG -> IntSet) -> IntMap CFG -> IntMap IntSet
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (Context -> CFG -> IntSet
calls_of_cfg Context
ctxt) IntMap CFG
cfgs
      fptrs :: Graph
fptrs = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ (CFG -> IntSet) -> IntMap CFG -> IntMap IntSet
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (Context -> CFG -> IntSet
forall p. Context -> p -> IntSet
function_pointer_intros Context
ctxt) IntMap CFG
cfgs in
    Context -> Graph -> Graph -> String
callgraph_to_dot Context
ctxt Graph
g Graph
fptrs


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

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

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


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

pp_dom :: PointerDomain -> String
pp_dom (Domain_Bases NESet PointerBase
bs)     = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((PointerBase -> String) -> [PointerBase] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PointerBase -> String
pp_base ([PointerBase] -> [String]) -> [PointerBase] -> [String]
forall a b. (a -> b) -> a -> b
$ NESet PointerBase -> [PointerBase]
forall a. NESet a -> [a]
neSetToList NESet PointerBase
bs)
pp_dom (Domain_Sources NESet BotSrc
srcs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((BotSrc -> String) -> [BotSrc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map BotSrc -> String
pp_source ([BotSrc] -> [String]) -> [BotSrc] -> [String]
forall a b. (a -> b) -> a -> b
$ NESet BotSrc -> [BotSrc]
forall a. NESet a -> [a]
neSetToList NESet BotSrc
srcs)

-- | Summarize preconditions
summarize_preconditions :: (SimpleExpr -> a)
-> (a -> String) -> Set VerificationCondition -> String
summarize_preconditions SimpleExpr -> a
get_info a -> String
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
      String
""
    else
      String
"PRECONDITIONS:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((a, [a]) -> String) -> [(a, [a])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (a, [a]) -> String
show_group [(a, [a])]
groups) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\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]) -> String
show_group (a
a,[a]
as) = a -> String
show_e a
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" SEP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
show_e [a]
as)

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



-- | Summarize assertions
summarize_assertions :: (SimpleExpr -> SimpleExpr)
-> (SimpleExpr -> String) -> Set VerificationCondition -> String
summarize_assertions SimpleExpr -> SimpleExpr
get_info SimpleExpr -> String
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
      String
""
    else
      String
"ASSERTIONS:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((SimpleExpr, [(SimpleExpr, [SimpleExpr])]) -> String)
-> [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleExpr, [(SimpleExpr, [SimpleExpr])]) -> String
show_instr_group [(SimpleExpr, [(SimpleExpr, [SimpleExpr])])]
per_instruction_grouped) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\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])]) -> String
show_instr_group (SimpleExpr
rip,[(SimpleExpr, [SimpleExpr])]
groups) = String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
show_e SimpleExpr
rip String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalateString
" && " (((SimpleExpr, [SimpleExpr]) -> String)
-> [(SimpleExpr, [SimpleExpr])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleExpr, [SimpleExpr]) -> String
show_group [(SimpleExpr, [SimpleExpr])]
groups)
  show_group :: (SimpleExpr, [SimpleExpr]) -> String
show_group (SimpleExpr
a,[SimpleExpr]
as) = SimpleExpr -> String
show_e SimpleExpr
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" SEP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (SimpleExpr -> String) -> [SimpleExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SimpleExpr -> String
show_e [SimpleExpr]
as)

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


-- | Summarize function constraints
summarize_function_constraints_short :: FContext -> S.Set VerificationCondition -> String 
summarize_function_constraints_short :: FContext -> Set VerificationCondition -> String
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
      String
""
    else
      String
"FUNCTION CONSTRAINTS:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> String)
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> String
summarize_fcs ([VerificationCondition] -> [String])
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fcs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
 where
  summarize_fcs :: VerificationCondition -> String
summarize_fcs (FunctionConstraint String
f Word64
i_a [(Register, SimpleExpr)]
params Set StatePart
sps) = String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. (Integral a, Show a) => a -> String
showHex Word64
i_a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((Register, SimpleExpr) -> String)
-> [(Register, SimpleExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Register, SimpleExpr) -> String
forall a. Show a => (a, SimpleExpr) -> String
show_param [(Register, SimpleExpr)]
params) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" PRESERVES " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set StatePart -> String
show_sps Set StatePart
sps

  show_param :: (a, SimpleExpr) -> String
show_param (a
r,SimpleExpr
e) = a -> String
forall a. Show a => a -> String
show a
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleExpr -> String
show_param_eq_sign SimpleExpr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
strip_parentheses (SimpleExpr -> String
show_param_value SimpleExpr
e)
  show_param_value :: SimpleExpr -> String
show_param_value SimpleExpr
e = SimpleExpr -> String
pp_bot SimpleExpr
e
  show_param_eq_sign :: SimpleExpr -> String
show_param_eq_sign SimpleExpr
e = if SimpleExpr -> Bool
contains_bot SimpleExpr
e then String
"~=" else String
":="

  show_sps :: Set StatePart -> String
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 :: String
showed_stack_frame  = [StatePart] -> String
show_stack_frame [StatePart]
stackframe in
      String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(/=) []) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String
showed_stack_frame String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (StatePart -> String) -> [StatePart] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map StatePart -> String
pp_statepart [StatePart]
others

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


  show_stack_frame :: [StatePart] -> String
show_stack_frame [StatePart]
sps =
    if [StatePart]
sps  [StatePart] -> [StatePart] -> Bool
forall a. Eq a => a -> a -> Bool
== [] then
      String
""
    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
      String
"[ RSP_0 - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
offset String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" TO RSP_0" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Int
top Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String
"" else String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
top) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"

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

  get_top :: StatePart -> Int
get_top (SP_Mem (SE_Op Operator
Minus Int
_ [SE_Var (SP_StackPointer String
_), 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 String
_)) Int
si)                                        = Int
si

summarize_function_constraints_long :: Context -> S.Set VerificationCondition -> String
summarize_function_constraints_long :: Context -> Set VerificationCondition -> String
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
      String
""
    else
      String
"FUNCTION CONSTRAINTS:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> String)
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> String
forall a. Show a => a -> String
show ([VerificationCondition] -> [String])
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fcs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"



summarize_function_pointers :: p -> Set VerificationCondition -> String
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
      String
""
    else
      String
"FUNCTION POINTERS USED:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (VerificationCondition -> String)
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VerificationCondition -> String
forall a. Show a => a -> String
show ([VerificationCondition] -> [String])
-> [VerificationCondition] -> [String]
forall a b. (a -> b) -> a -> b
$ Set VerificationCondition -> [VerificationCondition]
forall a. Set a -> [a]
S.toList Set VerificationCondition
fptrs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

-- | Summarize function initialization
summarize_finit :: Maybe FInit -> String
summarize_finit Maybe FInit
Nothing      = String
""
summarize_finit (Just FInit
finit) = if FInit
finit FInit -> FInit -> Bool
forall a. Eq a => a -> a -> Bool
== FInit
init_finit then String
"" else String
"INITIAL:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FInit -> String
forall a. Show a => a -> String
show FInit
finit -- TODO 



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

summarize_verification_conditions :: Context -> Int -> String
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 a. Eq a => Maybe a -> a -> a
`orElse` Set VerificationCondition
forall a. Set a
S.empty
      finit :: Maybe FInit
finit      = Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
entry (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
ctxt_finits Context
ctxt
      fctxt :: FContext
fctxt      = Context -> Int -> FContext
mk_fcontext Context
ctxt Int
entry
      summary :: String
summary    = Maybe FInit -> String
summarize_finit Maybe FInit
finit
                   -- ++ summarize_preconditions_short fctxt vcs
                   -- ++ summarize_assertions_short ctxt vcs
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ FContext -> Set VerificationCondition -> String
summarize_function_constraints_short FContext
fctxt Set VerificationCondition
vcs
                   -- ++ summarize_function_pointer_intros ctxt vcs
                   in
    String -> String
butlast String
summary
 where
  butlast :: String -> String
butlast String
""  = String
""
  butlast String
str = String -> String
forall a. [a] -> [a]
init String
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 AddressWord64 storage prefix Opcode annotation
-> IntSet
get_function_pointers_of_call GenericInstruction AddressWord64 storage prefix Opcode annotation
i =
    if Opcode -> Bool
isCall (GenericInstruction AddressWord64 storage prefix Opcode annotation
-> Opcode
forall label storage prefix opcode annotation.
GenericInstruction label storage prefix opcode annotation -> opcode
Instr.opcode GenericInstruction AddressWord64 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 AddressWord64 storage prefix Opcode annotation
-> Word64
forall storage prefix opcode annotation.
GenericInstruction AddressWord64 storage prefix opcode annotation
-> Word64
addressof GenericInstruction AddressWord64 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 -> String
callgraph_to_dot Context
ctxt (Edges IntMap IntSet
es) (Edges IntMap IntSet
fptrs) =
 let name :: String
name  = Context -> String
ctxt_name Context
ctxt in
  String
"diGraph " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"{\n"
  String -> String -> String
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 Int -> String
node_to_dot ([Int] -> [String]) -> [Int] -> [String]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [Int]
forall a. IntMap a -> [Int]
IM.keys IntMap IntSet
es)
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
  String -> String -> String
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 (String -> (Int, IntSet) -> String
forall a. (Integral a, Show a) => String -> (a, IntSet) -> String
edge_to_dot' String
"") ([(Int, IntSet)] -> [String]) -> [(Int, IntSet)] -> [String]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.assocs IntMap IntSet
es)
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
  String -> String -> String
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 (String -> (Int, IntSet) -> String
forall a. (Integral a, Show a) => String -> (a, IntSet) -> String
edge_to_dot' String
"[style=dotted]") ([(Int, IntSet)] -> [String]) -> [(Int, IntSet)] -> [String]
forall a b. (a -> b) -> a -> b
$ IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IM.assocs IntMap IntSet
fptrs)
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n}"
 where
  node_to_dot :: Int -> String
node_to_dot Int
v =
    let bgcolor :: String
bgcolor = Int -> String
node_color Int
v
        fgcolor :: String
fgcolor = String -> String
hex_color_of_text String
bgcolor in
       String
"\t"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Integral a, Show a) => a -> String
mk_node Int
v
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  ["
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"style=filled fillcolor=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bgcolor String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" fontcolor=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fgcolor String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" shape=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
node_shape Int
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"label=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
node_label Int
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

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

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

  node_shape :: Int -> String
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               -> String
"Mrecord"
      Just VerificationResult
VerificationSuccesWithAssumptions -> String
"Mrecord"
      Maybe VerificationResult
_                                      -> String
"record"

  node_label :: Int -> String
node_label Int
v =
    let finit :: Maybe FInit
finit = Int -> IntMap FInit -> Maybe FInit
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap FInit -> Maybe FInit) -> IntMap FInit -> Maybe FInit
forall a b. (a -> b) -> a -> b
$ Context -> IntMap FInit
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 -> String
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 FInit
finit Maybe FInit -> [Maybe FInit] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FInit -> Maybe FInit
forall a. a -> Maybe a
Just FInit
init_finit,Maybe FInit
forall a. Maybe a
Nothing] then
            Context -> Int -> String
function_name_of_entry Context
ctxt Int
v
          else
            String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Context -> Int -> String
function_name_of_entry Context
ctxt Int
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
markup (Context -> Int -> String
summarize_verification_conditions Context
ctxt Int
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

  node_color :: Int -> String
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 -> String -> VerificationResult
VerificationError String
"Verification error"
                     Just VerificationResult
v  -> VerificationResult
v
     in
      case VerificationResult
verified of
        VerificationResult
VerificationSuccess               -> String
"#90EE90" -- light green
        VerificationResult
VerificationSuccesWithAssumptions -> String
"#89CFF0" -- light blue
        VerificationError String
_               -> String
"#FF7F7F" -- light red
        VerificationResult
VerificationUnresolvedIndirection -> String
"#CBC3E3" -- light purple





  markup :: String -> String
markup String
vcs = Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
max_limit_node_text_size_as_indicated_by_graphviz (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replace [Char
c | Char
c <- String
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