{-# LANGUAGE PartialTypeSignatures , FlexibleContexts, DeriveGeneric, StandaloneDeriving, StrictData #-}


module OutputGeneration.Metrics where 

import Base

import Data.SValue
import Data.L0
import Data.CFG
import Data.Indirection
import Data.VerificationCondition
import Data.SymbolicExpression
import Data.X86.Instruction


import Binary.Generic
import WithNoAbstraction.Pointers

import qualified Data.Map as M
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set as S
import Data.Aeson
import Data.ByteString.Lazy.Char8 (unpack)

import Data.Maybe (fromJust,catMaybes,mapMaybe)
import Data.List 
import Data.Foldable
import Data.Word
import Data.Int (Int64)

import System.IO.Unsafe (unsafePerformIO)

import GHC.Generics
import Debug.Trace







mk_metrics :: p -> L0 pred finit SValue -> [Char]
mk_metrics p
bin L0 pred finit SValue
l0 =
  let (IntMap Indirections
rest,IntMap Indirections
unresolved) = (Indirections -> Bool)
-> IntMap Indirections
-> (IntMap Indirections, IntMap Indirections)
forall a. (a -> Bool) -> IntMap a -> (IntMap a, IntMap a)
IM.partition (Indirections -> Indirections -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Indirection -> Indirections
forall a. a -> Set a
S.singleton Indirection
Indirection_Unresolved)) (IntMap Indirections -> (IntMap Indirections, IntMap Indirections))
-> IntMap Indirections
-> (IntMap Indirections, IntMap Indirections)
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap Indirections
forall pred finit v. L0 pred finit v -> IntMap Indirections
l0_indirections L0 pred finit SValue
l0
      (IntMap Indirections
partially_resolved,IntMap Indirections
resolved) = (Indirections -> Bool)
-> IntMap Indirections
-> (IntMap Indirections, IntMap Indirections)
forall a. (a -> Bool) -> IntMap a -> (IntMap a, IntMap a)
IM.partition (Indirection -> Indirections -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Indirection
Indirection_Unresolved) (IntMap Indirections -> (IntMap Indirections, IntMap Indirections))
-> IntMap Indirections
-> (IntMap Indirections, IntMap Indirections)
forall a b. (a -> b) -> a -> b
$ IntMap Indirections
rest
      instrs :: [Instruction]
instrs = L0 pred finit SValue -> [Instruction]
forall {pred} {finit} {v}. L0 pred finit v -> [Instruction]
l0_get_all_instructions L0 pred finit SValue
l0
      num_intrs :: Int
num_intrs = [Instruction] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Instruction]
instrs
      avg_size :: Double
avg_size = [Int] -> Double
forall a b. (Real a, Fractional b) => [a] -> b
average ([Int] -> Double) -> [Int] -> Double
forall a b. (a -> b) -> a -> b
$ (Instruction -> Int) -> [Instruction] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Instruction -> Int
inSize [Instruction]
instrs
      num_expected_intrs :: Integer
num_expected_intrs = Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (p -> Int
forall a. BinaryClass a => a -> Int
binary_text_section_size p
bin) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
avg_size)
      pars :: IntMap (PointerAnalysisResult SValue)
pars = IntMap (IntMap (PointerAnalysisResult SValue))
-> IntMap (PointerAnalysisResult SValue)
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions (IntMap (IntMap (PointerAnalysisResult SValue))
 -> IntMap (PointerAnalysisResult SValue))
-> IntMap (IntMap (PointerAnalysisResult SValue))
-> IntMap (PointerAnalysisResult SValue)
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue
-> IntMap (IntMap (PointerAnalysisResult SValue))
forall pred finit v.
L0 pred finit v -> IntMap (IntMap (PointerAnalysisResult v))
l0_get_pars L0 pred finit SValue
l0
      pointerDesignations :: Map [Char] Int
pointerDesignations = p -> IntMap (PointerAnalysisResult SValue) -> Map [Char] Int
forall {p} {a}.
(BinaryClass p, Num a) =>
p -> IntMap (PointerAnalysisResult SValue) -> Map [Char] a
mk_metric_pointerDesignations p
bin IntMap (PointerAnalysisResult SValue)
pars in
   [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" [
       [Char]
"-------------"
     , [Char]
"INDIRECTIONS:"
     , [Char]
"-------------"
     , [Char]
"#indirections:                   " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap Indirections -> Int
forall a. IntMap a -> Int
IM.size (IntMap Indirections -> Int) -> IntMap Indirections -> Int
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap Indirections
forall pred finit v. L0 pred finit v -> IntMap Indirections
l0_indirections L0 pred finit SValue
l0) 
     , [Char]
"  (of which resolved):           " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap Indirections -> Int
forall a. IntMap a -> Int
IM.size IntMap Indirections
resolved) 
     , [Char]
"  (of which partially resolved): " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap Indirections -> Int
forall a. IntMap a -> Int
IM.size IntMap Indirections
partially_resolved)
     , [Char]
"  (of which unresolved):         " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap Indirections -> Int
forall a. IntMap a -> Int
IM.size IntMap Indirections
unresolved)
     ,IntMap Indirections -> [Char]
show_indirections (IntMap Indirections -> [Char]) -> IntMap Indirections -> [Char]
forall a b. (a -> b) -> a -> b
$ (Indirections -> Bool)
-> IntMap Indirections -> IntMap Indirections
forall a. (a -> Bool) -> IntMap a -> IntMap a
IM.filter (Indirections -> Indirections -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Indirection -> Indirections
forall a. a -> Set a
S.singleton Indirection
Indirection_Unresolved)) (IntMap Indirections -> IntMap Indirections)
-> IntMap Indirections -> IntMap Indirections
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap Indirections
forall pred finit v. L0 pred finit v -> IntMap Indirections
l0_indirections L0 pred finit SValue
l0 

     , [Char]
"\n"
     , [Char]
"-------------"
     , [Char]
"INSTRUCTIONS:"
     , [Char]
"-------------"
     , [Char]
"#instructions:                      " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
num_intrs
     , [Char]
"average instruction size:           " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show Double
avg_size
     , [Char]
"estimate of expected #instructions: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
num_expected_intrs
     , [Char]
"coverage:                           " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Double -> Double
round2dp (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
num_intrs Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
num_expected_intrs Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
100))
     , [Char]
"#instructions with memory access:   " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap (PointerAnalysisResult SValue) -> Int
forall a. IntMap a -> Int
IM.size IntMap (PointerAnalysisResult SValue)
pars)
     , [Char]
"  designations:                     " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [([Char], Double)] -> [Char]
forall a. Show a => a -> [Char]
show (Map [Char] Double -> [([Char], Double)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map [Char] Double -> [([Char], Double)])
-> Map [Char] Double -> [([Char], Double)]
forall a b. (a -> b) -> a -> b
$ Map [Char] Int -> Map [Char] Double
designations_to_percentages Map [Char] Int
pointerDesignations)

     , [Char]
"\n"
     , [Char]
"----------"
     , [Char]
"FUNCTIONS:"
     , [Char]
"----------"
     , [Char]
"#lifted functions:                              " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a. IntMap a -> Int
IM.size (IntMap (finit, Maybe (FResult pred SValue)) -> Int)
-> IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap (finit, Maybe (FResult pred SValue))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit SValue
l0)
     , [Char]
"  (of which ending in unresolved indirections): " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a. IntMap a -> Int
IM.size (IntMap (finit, Maybe (FResult pred SValue)) -> Int)
-> IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a b. (a -> b) -> a -> b
$ ((finit, Maybe (FResult pred SValue)) -> Bool)
-> IntMap (finit, Maybe (FResult pred SValue))
-> IntMap (finit, Maybe (FResult pred SValue))
forall a. (a -> Bool) -> IntMap a -> IntMap a
IM.filter (Postcondition pred -> Bool
forall {pred}. Postcondition pred -> Bool
is_unresolved (Postcondition pred -> Bool)
-> ((finit, Maybe (FResult pred SValue)) -> Postcondition pred)
-> (finit, Maybe (FResult pred SValue))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (finit, Maybe (FResult pred SValue)) -> Postcondition pred
forall {a} {pred} {v}.
(a, Maybe (FResult pred v)) -> Postcondition pred
get_post) (IntMap (finit, Maybe (FResult pred SValue))
 -> IntMap (finit, Maybe (FResult pred SValue)))
-> IntMap (finit, Maybe (FResult pred SValue))
-> IntMap (finit, Maybe (FResult pred SValue))
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap (finit, Maybe (FResult pred SValue))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit SValue
l0)
     , [Char]
"  (of which verification error):                " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a. IntMap a -> Int
IM.size (IntMap (finit, Maybe (FResult pred SValue)) -> Int)
-> IntMap (finit, Maybe (FResult pred SValue)) -> Int
forall a b. (a -> b) -> a -> b
$ ((finit, Maybe (FResult pred SValue)) -> Bool)
-> IntMap (finit, Maybe (FResult pred SValue))
-> IntMap (finit, Maybe (FResult pred SValue))
forall a. (a -> Bool) -> IntMap a -> IntMap a
IM.filter (Postcondition pred -> Bool
forall {pred}. Postcondition pred -> Bool
is_error (Postcondition pred -> Bool)
-> ((finit, Maybe (FResult pred SValue)) -> Postcondition pred)
-> (finit, Maybe (FResult pred SValue))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (finit, Maybe (FResult pred SValue)) -> Postcondition pred
forall {a} {pred} {v}.
(a, Maybe (FResult pred v)) -> Postcondition pred
get_post) (IntMap (finit, Maybe (FResult pred SValue))
 -> IntMap (finit, Maybe (FResult pred SValue)))
-> IntMap (finit, Maybe (FResult pred SValue))
-> IntMap (finit, Maybe (FResult pred SValue))
forall a b. (a -> b) -> a -> b
$ L0 pred finit SValue -> IntMap (finit, Maybe (FResult pred SValue))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions L0 pred finit SValue
l0)

     , [Char]
"\n"
     , [Char]
"----------"
     , [Char]
"OTHER:"
     , [Char]
"----------"     
     , [Char]
"verificaton time: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ L0 pred finit SValue -> [Char]
forall pred finit v. L0 pred finit v -> [Char]
l0_time L0 pred finit SValue
l0
     , [Char]
"\n"
   ]
  --putStrLn $ show $ IM.filter is_error $ IM.map get_post $ l0_functions l0
  --putStrLn $ show $ IM.map get_cfg $ IM.filter (is_error . get_post) $ l0_functions l0
 where
  get_post :: (a, Maybe (FResult pred v)) -> Postcondition pred
get_post (a
finit,Just (FResult CFG
_ Postcondition pred
post Set Word64
_ Set (VerificationCondition v)
_ IntMap (PointerAnalysisResult v)
_)) = Postcondition pred
post
  get_cfg :: (a, Maybe (FResult pred v)) -> CFG
get_cfg (a
finit,Just (FResult CFG
cfg Postcondition pred
post Set Word64
_ Set (VerificationCondition v)
_ IntMap (PointerAnalysisResult v)
_)) = CFG
cfg


  is_error :: Postcondition pred -> Bool
is_error (VerificationError [(Int, pred)]
_) = Bool
True
  is_error Postcondition pred
_ = Bool
False

  is_unresolved :: Postcondition pred -> Bool
is_unresolved (HasUnresolvedIndirections [Int]
_) = Bool
True
  is_unresolved Postcondition pred
_ = Bool
False

  l0_get_all_instructions :: L0 pred finit v -> [Instruction]
l0_get_all_instructions = Set Instruction -> [Instruction]
forall a. Set a -> [a]
S.toList (Set Instruction -> [Instruction])
-> (L0 pred finit v -> Set Instruction)
-> L0 pred finit v
-> [Instruction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Instruction] -> Set Instruction
forall a. Ord a => [a] -> Set a
S.fromList ([Instruction] -> Set Instruction)
-> (L0 pred finit v -> [Instruction])
-> L0 pred finit v
-> Set Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Instruction]] -> [Instruction]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Instruction]] -> [Instruction])
-> (L0 pred finit v -> [[Instruction]])
-> L0 pred finit v
-> [Instruction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CFG -> [[Instruction]]) -> [CFG] -> [[Instruction]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (IntMap [Instruction] -> [[Instruction]]
forall a. IntMap a -> [a]
IM.elems (IntMap [Instruction] -> [[Instruction]])
-> (CFG -> IntMap [Instruction]) -> CFG -> [[Instruction]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG -> IntMap [Instruction]
cfg_instrs) ([CFG] -> [[Instruction]])
-> (L0 pred finit v -> [CFG]) -> L0 pred finit v -> [[Instruction]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap CFG -> [CFG]
forall a. IntMap a -> [a]
IM.elems (IntMap CFG -> [CFG])
-> (L0 pred finit v -> IntMap CFG) -> L0 pred finit v -> [CFG]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L0 pred finit v -> IntMap CFG
forall pred finit v. L0 pred finit v -> IntMap CFG
l0_get_cfgs

  

mk_metric_pointerDesignations :: p -> IntMap (PointerAnalysisResult SValue) -> Map [Char] a
mk_metric_pointerDesignations p
bin = ([Char] -> Map [Char] a -> Map [Char] a)
-> Map [Char] a -> [[Char]] -> Map [Char] a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((a -> a) -> [Char] -> Map [Char] a -> Map [Char] a
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust (a -> a -> a
forall a. Num a => a -> a -> a
(+) a
1)) Map [Char] a
init_m ([[Char]] -> Map [Char] a)
-> (IntMap (PointerAnalysisResult SValue) -> [[Char]])
-> IntMap (PointerAnalysisResult SValue)
-> Map [Char] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, PointerAnalysisResult SValue) -> [[Char]])
-> [(Int, PointerAnalysisResult SValue)] -> [[Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, PointerAnalysisResult SValue) -> [[Char]]
forall {p}. (p, PointerAnalysisResult SValue) -> [[Char]]
get_specifity_per_instruction ([(Int, PointerAnalysisResult SValue)] -> [[Char]])
-> (IntMap (PointerAnalysisResult SValue)
    -> [(Int, PointerAnalysisResult SValue)])
-> IntMap (PointerAnalysisResult SValue)
-> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap (PointerAnalysisResult SValue)
-> [(Int, PointerAnalysisResult SValue)]
forall a. IntMap a -> [(Int, a)]
IM.assocs
 where
  init_m :: Map [Char] a
init_m = [([Char], a)] -> Map [Char] a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [([Char]
"U",a
0), ([Char]
"CL",a
0),([Char]
"CG",a
0),([Char]
"CH",a
0),([Char]
"CLG",a
0),([Char]
"CLH",a
0),([Char]
"CGH",a
0),([Char]
"CLHG",a
0), ([Char]
"AL",a
0),([Char]
"AG",a
0),([Char]
"AH",a
0),([Char]
"ALG",a
0),([Char]
"ALH",a
0),([Char]
"AGH",a
0),([Char]
"ALHG",a
0)]

  get_specifity_per_instruction :: (p, PointerAnalysisResult SValue) -> [[Char]]
get_specifity_per_instruction (p
entry,PointerAnalysisResult Maybe SValue
w [Maybe SValue]
rs) = (Maybe SValue -> [Char]) -> [Maybe SValue] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (p -> Maybe SValue -> [Char]
forall {p}. p -> Maybe SValue -> [Char]
get_domains p
entry) [Maybe SValue
w] -- (w:rs) IF ALSO PRODUCING DATA OVER READS

  get_domains :: p -> Maybe SValue -> [Char]
get_domains p
entry Maybe SValue
Nothing  = [Char]
"Nothing"
  get_domains p
entry (Just SValue
e) = p -> SValue -> [Char]
forall {p}. BinaryClass p => p -> SValue -> [Char]
get_pointer_specifity_cpointer p
bin SValue
e


-- "C"     = Concrete
-- "C+U"   = Concrete plus unknown offset
-- "U"     = Unknown
-- "A"     = Addends
get_pointer_specifity_cpointer :: p -> SValue -> [Char]
get_pointer_specifity_cpointer p
bin SValue
Top = [Char]
"U"
get_pointer_specifity_cpointer p
bin (SAddends NESet SimpleExpr
es)  = [Char]
"A" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ p -> NESet SimpleExpr -> [Char]
forall {t :: * -> *} {p}.
(Foldable t, BinaryClass p) =>
p -> t SimpleExpr -> [Char]
get_types p
bin NESet SimpleExpr
es
get_pointer_specifity_cpointer p
bin (SConcrete NESet SimpleExpr
es) = [Char]
"C" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ p -> NESet SimpleExpr -> [Char]
forall {t :: * -> *} {p}.
(Foldable t, BinaryClass p) =>
p -> t SimpleExpr -> [Char]
get_types p
bin NESet SimpleExpr
es

get_types :: p -> t SimpleExpr -> [Char]
get_types p
bin t SimpleExpr
es = [Char]
local [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
global [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
heap
 where
  local :: [Char]
local
    | (SimpleExpr -> Bool) -> t SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (p -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_local_pointer p
bin) t SimpleExpr
es = [Char]
"L"
    | Bool
otherwise = [Char]
""
  global :: [Char]
global
    | (SimpleExpr -> Bool) -> t SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (p -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_global_pointer p
bin) t SimpleExpr
es = [Char]
"G"
    | Bool
otherwise = [Char]
""
  heap :: [Char]
heap 
    | (SimpleExpr -> Bool) -> t SimpleExpr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\SimpleExpr
e -> Bool -> Bool
not (p -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_global_pointer p
bin SimpleExpr
e) Bool -> Bool -> Bool
&& Bool -> Bool
not (p -> SimpleExpr -> Bool
forall {bin}. BinaryClass bin => bin -> SimpleExpr -> Bool
expr_is_maybe_local_pointer p
bin SimpleExpr
e)) t SimpleExpr
es = [Char]
"H"
    | Bool
otherwise = [Char]
""


designations_to_percentages :: M.Map String Int -> M.Map String Double
designations_to_percentages :: Map [Char] Int -> Map [Char] Double
designations_to_percentages Map [Char] Int
m = (Int -> Double) -> Map [Char] Int -> Map [Char] Double
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\Int
v -> Int -> Int -> Double
forall {a} {b}. (Integral a, Integral b) => a -> b -> Double
mk_percentage Int
v (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Map [Char] Int -> [Int]
forall k a. Map k a -> [a]
M.elems Map [Char] Int
m) Map [Char] Int
m
 where
  mk_percentage :: a -> b -> Double
mk_percentage a
x b
y = Double -> Double
round2dp (a
x a -> b -> Double
forall {a} {b}. (Integral a, Integral b) => a -> b -> Double
`intDiv` b
y Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
100)

intDiv :: (Integral a,Integral b) => a -> b -> Double
a
x intDiv :: forall {a} {b}. (Integral a, Integral b) => a -> b -> Double
`intDiv` b
y = a -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ b -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
y


{--

metrics = M.fromList [
  ("#instructions",          "number of covered instructions"),
  ("avgInstructionSize",     "average instruction size"),
  ("#expectedInstructions",  "expected number of instructions"),
  ("%instructionCoverage",   "estimate of percentage of covered instructions"),
  ("#memWrites",             "total number of instructions writing to memory"),
  ("pointerDesignations",    "A, C, C+U, U"),
  ("%resolvedMemWrites",     "percentage of pointers that are assigned a non-trivial domain"),
  ("specifityMetric",        "weighted mean of pointer designations"),

  ("#functions",             "total number of functions"),
  ("#functions_verified",    "total number of verified functions"),
  ("#functions_unresolved",  "total number of functions with unresolved indirections"),
  ("#functions_verif_error", "total number of functions with verification error"),

  ("#resolved_jumps",        "total number of resolved jumps"),
  ("#resolved_calls",        "total number of resolved calls"),
  ("#unresolved_jumps",      "total number of unresolved jumps"),
  ("#unresolved_calls",      "total number of unresolved calls"),

  ("runningTime",            "Running time in HH:MM:SS")
 ]


-- | Returns all generated metrics in JSON and pretty-printed
mk_metrics :: Context -> (String,String)
mk_metrics ctxt =
  let instrs                          = S.toList $ ctxt_get_instructions ctxt
      avg_size                        = average $ map sizeof instrs
      text_section_size               = binary_text_section_size $ ctxt_binary ctxt
      num_expected_intrs              = floor (fromIntegral text_section_size / avg_size)
      num_intrs                       = length instrs
      instructionCoverage             = round2dp (fromIntegral num_intrs / fromIntegral num_expected_intrs * 100)
      mem_ops                         = ctxt_resolve_mem_operands ctxt
      pointerDesignations             = mk_metric_pointerDesignations ctxt mem_ops 
      pointerDesignationsPercentages  = designations_to_percentages pointerDesignations
      memWrites                       = sum $ M.elems pointerDesignations
      specifityMetric                 = specifityMetricOf pointerDesignationsPercentages
      resolvedMemWrites               = percentageResolvedMemWrites pointerDesignationsPercentages

      num_functions                   = IM.size $ ctxt_results ctxt
      num_verif_success               = num_of_verif_success ctxt
      num_verif_unresolved            = num_of_verif_unresolved ctxt
      num_verif_error                 = num_of_verif_error ctxt

      resolved_jumps                  = num_of_resolved_indirection_jumps ctxt
      resolved_calls                  = num_of_resolved_indirection_calls ctxt
      unresolved_jumps                = num_of_unres_inds ctxt isJump
      unresolved_calls                = num_of_unres_inds ctxt isCall

      runningTimeRepr                 = show_runningtime $ ctxt_runningtime ctxt

      metrics = map mk_metric [
                 ("#instructions",            show num_intrs),
                 ("avgInstructionSize",       show avg_size),
                 ("#expectedInstructions",    show num_expected_intrs),
                 ("%instructionCoverage",     show instructionCoverage),
                 ("#memWrites",               show memWrites),
                 ("pointerDesignations",      show $ M.toList pointerDesignationsPercentages),
                 ("%resolvedMemWrites",       show resolvedMemWrites),
                 ("specifityMetric",          show specifityMetric),
                 ("#functions",               show num_functions),
                 ("#functions_verified",      show num_verif_success),
                 ("#functions_unresolved",    show num_verif_unresolved),
                 ("#functions_verif_error",   show num_verif_error),
                 ("#resolved_jumps",          show resolved_jumps),
                 ("#resolved_calls",          show resolved_calls),
                 ("#unresolved_jumps",        show unresolved_jumps),
                 ("#unresolved_calls",        show unresolved_calls),
                 ("runningTime",              runningTimeRepr)
                ] in
  (unpack $ encode metrics,intercalate "\n" $ map show_metric metrics)
 where
  mk_metric (name,value) = Metric name (metrics M.! name) value


  show_metric (Metric name desc value) =
    let str0 = name ++ replicate (metrics_metric_size - length name + 3) ' '
        str1 = str0 ++ " (" ++ desc ++ ")" in
      str1 ++ replicate (metrics_descr_size - length desc) ' ' ++ " = " ++ value

  designations_to_percentages :: M.Map String Int -> M.Map String Double
  designations_to_percentages m = M.map (\v -> mk_percentage v $ sum $ M.elems m) m
  
  mk_percentage x y = round2dp (x `intDiv` y * 100)


-- | Show time in HH:MM:SS
show_runningtime :: Int64 -> String
show_runningtime secs = show hours ++ ":" ++ show minutes ++ ":" ++ show seconds
 where
  (hours,rem_hour)  = secs `divMod` 3600
  (minutes,seconds) = rem_hour `divMod` 60

-- | Number of functions successfully verified
num_of_verif_success = IM.size . IM.filter isVerificationSuccess . ctxt_results
 where
  isVerificationSuccess VerificationSuccess               = True
  isVerificationSuccess VerificationSuccesWithAssumptions = True
  isVerificationSuccess _                                 = False

-- | Number of functions with unresolved indirections
num_of_verif_unresolved = IM.size . IM.filter ((==) VerificationUnresolvedIndirection) . ctxt_results

-- | Number of functions with a verification error
num_of_verif_error = IM.size . IM.filter isVerificationError . ctxt_results
 where
  isVerificationError (VerificationError _) = True
  isVerificationError _                     = False

-- | Number of unresolved indirections
num_of_unres_inds ctxt chkKind = sum (map (num_of_unres_inds_in_cfg ctxt chkKind) $ IM.elems $ ctxt_cfgs ctxt)

-- | Number of unresolved indirections in the given CFG
num_of_unres_inds_in_cfg ctxt chkKind g = 
  let blocks  = IM.keys $ cfg_blocks g in
    length (filter (\b -> node_info_of ctxt g b == UnresolvedIndirection && ends_in_kind b) blocks)
 where
  ends_in_kind b = chkKind $ opcode $ last (fetch_block g b)

-- | Number of resolved indirections
num_of_resolved_indirection_calls ctxt = IM.size $ IM.filterWithKey (indirectionIsCall ctxt) $ ctxt_inds ctxt
 where
  indirectionIsCall ctxt a _ =
    case unsafePerformIO $ Analysis.Context.fetch_instruction ctxt $ fromIntegral a of -- Should be safe as result is immutable.
      Nothing -> False
      Just i  -> isCall $ opcode i
num_of_resolved_indirection_jumps ctxt = IM.size $ IM.filterWithKey (indirectionIsJump ctxt) $ ctxt_inds ctxt
 where
  indirectionIsJump ctxt a _ =
    case unsafePerformIO $ Analysis.Context.fetch_instruction ctxt $ fromIntegral a of -- Should be safe as result is immutable.
      Nothing -> False
      Just i  -> not $ isCall $ opcode i


-- | Number of instructions in CFG
num_of_instructions g = sum (map length $ IM.elems $ cfg_blocks g)

-- | Number of basic blocks in CFG
num_of_blocks g = IM.size $ cfg_blocks g

-- | Number of edges in CFG
num_of_edges g = sum (map IS.size $ IM.elems $ cfg_edges g)



percentageResolvedMemWrites :: M.Map String Double -> Double
percentageResolvedMemWrites m = 100 - m M.! "U"


specifityMetricOf :: M.Map String Double -> Double
specifityMetricOf m = m M.! "C" + 0.8*(m M.! "A") + 0.6*(m M.! "A")



metrics_metric_size = maximum $ map length $ M.keys metrics
metrics_descr_size  = maximum $ map length $ M.elems metrics


round2dp :: Double -> Double
round2dp x = fromIntegral (round $ x * 1e2) / 1e2



intDiv :: (Integral a,Integral b) => a -> b -> Double
x `intDiv` y = fromIntegral x / fromIntegral y

data Metric = Metric {
  metrics_name  :: String, -- ^ Name of the metric
  metrics_desc  :: String, -- ^ Description of the metric
  metrics_value :: String  -- ^ Serialized value of the metric
 }
 deriving Generic

instance ToJSON Metric where
  toJSON = genericToJSON defaultOptions { sumEncoding = ObjectWithSingleField }

--}