{-# LANGUAGE DeriveGeneric #-}


module Data.L0 where


import Config
import Base

import Data.Indirection
import Data.CFG
import Data.VerificationCondition

import Binary.Generic


import qualified Data.Set as S
import qualified Data.IntMap as IM
import Data.Word
import Data.List

import qualified Data.Serialize as Cereal hiding (get,put)
import Control.DeepSeq
import GHC.Generics


data Postcondition pred = ReturnsWith pred | HasUnresolvedIndirections [Int] | Terminates | TimeOut | VerificationError [(Int,pred)]
  deriving ((forall x. Postcondition pred -> Rep (Postcondition pred) x)
-> (forall x. Rep (Postcondition pred) x -> Postcondition pred)
-> Generic (Postcondition pred)
forall x. Rep (Postcondition pred) x -> Postcondition pred
forall x. Postcondition pred -> Rep (Postcondition pred) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall pred x. Rep (Postcondition pred) x -> Postcondition pred
forall pred x. Postcondition pred -> Rep (Postcondition pred) x
$cfrom :: forall pred x. Postcondition pred -> Rep (Postcondition pred) x
from :: forall x. Postcondition pred -> Rep (Postcondition pred) x
$cto :: forall pred x. Rep (Postcondition pred) x -> Postcondition pred
to :: forall x. Rep (Postcondition pred) x -> Postcondition pred
Generic,Postcondition pred -> Postcondition pred -> Bool
(Postcondition pred -> Postcondition pred -> Bool)
-> (Postcondition pred -> Postcondition pred -> Bool)
-> Eq (Postcondition pred)
forall pred.
Eq pred =>
Postcondition pred -> Postcondition pred -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall pred.
Eq pred =>
Postcondition pred -> Postcondition pred -> Bool
== :: Postcondition pred -> Postcondition pred -> Bool
$c/= :: forall pred.
Eq pred =>
Postcondition pred -> Postcondition pred -> Bool
/= :: Postcondition pred -> Postcondition pred -> Bool
Eq)

instance Show pred => Show (Postcondition pred) where
  show :: Postcondition pred -> String
show (ReturnsWith pred
p) = String
"returns with postcondition\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ pred -> String
forall a. Show a => a -> String
show pred
p
  show (HasUnresolvedIndirections [Key]
blockIDs) = String
"has unresolved indirections at blocks " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Key] -> String
forall a. Show a => a -> String
show [Key]
blockIDs
  show (Postcondition pred
Terminates) = String
"terminates"
  show (Postcondition pred
TimeOut) = String
"TimeOut"
  show (VerificationError [(Key, pred)]
bs) = String
" returns with a verification error:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (((Key, pred) -> String) -> [(Key, pred)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Key, pred) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
show_error [(Key, pred)]
bs)
   where
    show_error :: (a, a) -> String
show_error (a
blockID,a
p) = String
"BlockID: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
blockID String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p 


data FResult pred v = FResult {
  forall pred v. FResult pred v -> CFG
result_cfg   :: CFG,
  forall pred v. FResult pred v -> Postcondition pred
result_post  :: Postcondition pred,
  forall pred v. FResult pred v -> Set Word64
result_calls :: S.Set Word64,
  forall pred v. FResult pred v -> Set (VerificationCondition v)
result_vcs   :: S.Set (VerificationCondition v),
  forall pred v. FResult pred v -> IntMap (PointerAnalysisResult v)
result_pa    :: IM.IntMap (PointerAnalysisResult v)
 }
 deriving (forall x. FResult pred v -> Rep (FResult pred v) x)
-> (forall x. Rep (FResult pred v) x -> FResult pred v)
-> Generic (FResult pred v)
forall x. Rep (FResult pred v) x -> FResult pred v
forall x. FResult pred v -> Rep (FResult pred v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall pred v x. Rep (FResult pred v) x -> FResult pred v
forall pred v x. FResult pred v -> Rep (FResult pred v) x
$cfrom :: forall pred v x. FResult pred v -> Rep (FResult pred v) x
from :: forall x. FResult pred v -> Rep (FResult pred v) x
$cto :: forall pred v x. Rep (FResult pred v) x -> FResult pred v
to :: forall x. Rep (FResult pred v) x -> FResult pred v
Generic


data L0 pred finit v = L0 {
  forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions :: IM.IntMap (finit,Maybe (FResult pred v)),
  forall pred finit v. L0 pred finit v -> IntMap Indirections
l0_indirections :: IM.IntMap Indirections,
  forall pred finit v. L0 pred finit v -> String
l0_time :: String
 }
 deriving (forall x. L0 pred finit v -> Rep (L0 pred finit v) x)
-> (forall x. Rep (L0 pred finit v) x -> L0 pred finit v)
-> Generic (L0 pred finit v)
forall x. Rep (L0 pred finit v) x -> L0 pred finit v
forall x. L0 pred finit v -> Rep (L0 pred finit v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall pred finit v x. Rep (L0 pred finit v) x -> L0 pred finit v
forall pred finit v x. L0 pred finit v -> Rep (L0 pred finit v) x
$cfrom :: forall pred finit v x. L0 pred finit v -> Rep (L0 pred finit v) x
from :: forall x. L0 pred finit v -> Rep (L0 pred finit v) x
$cto :: forall pred finit v x. Rep (L0 pred finit v) x -> L0 pred finit v
to :: forall x. Rep (L0 pred finit v) x -> L0 pred finit v
Generic

l0_insert_new_entry :: Key -> finit -> L0 pred finit v -> L0 pred finit v
l0_insert_new_entry Key
entry finit
finit (L0 IntMap (finit, Maybe (FResult pred v))
fs IntMap Indirections
inds String
time) = IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
forall pred finit v.
IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
L0 (Key
-> (finit, Maybe (FResult pred v))
-> IntMap (finit, Maybe (FResult pred v))
-> IntMap (finit, Maybe (FResult pred v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
entry (finit
finit,Maybe (FResult pred v)
forall a. Maybe a
Nothing) IntMap (finit, Maybe (FResult pred v))
fs) IntMap Indirections
inds String
time

l0_adjust_result :: a -> Maybe (FResult pred v) -> L0 pred finit v -> L0 pred finit v
l0_adjust_result a
entry Maybe (FResult pred v)
result (L0 IntMap (finit, Maybe (FResult pred v))
fs IntMap Indirections
inds String
time) = IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
forall pred finit v.
IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
L0 (((finit, Maybe (FResult pred v))
 -> (finit, Maybe (FResult pred v)))
-> Key
-> IntMap (finit, Maybe (FResult pred v))
-> IntMap (finit, Maybe (FResult pred v))
forall a. (a -> a) -> Key -> IntMap a -> IntMap a
IM.adjust (\(finit
finit,Maybe (FResult pred v)
_) -> (finit
finit,Maybe (FResult pred v)
result)) (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
entry) IntMap (finit, Maybe (FResult pred v))
fs) IntMap Indirections
inds String
time

l0_lookup_entry :: a -> L0 pred finit v -> Maybe (finit, Maybe (FResult pred v))
l0_lookup_entry a
entry (L0 IntMap (finit, Maybe (FResult pred v))
fs IntMap Indirections
inds String
time) = Key
-> IntMap (finit, Maybe (FResult pred v))
-> Maybe (finit, Maybe (FResult pred v))
forall a. Key -> IntMap a -> Maybe a
IM.lookup (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
entry) IntMap (finit, Maybe (FResult pred v))
fs

l0_lookup_indirection :: a -> L0 pred finit v -> Maybe Indirections
l0_lookup_indirection a
a (L0 IntMap (finit, Maybe (FResult pred v))
fs IntMap Indirections
inds String
time) = Key -> IntMap Indirections -> Maybe Indirections
forall a. Key -> IntMap a -> Maybe a
IM.lookup (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) IntMap Indirections
inds

l0_insert_indirection :: a -> Indirections -> L0 pred finit v -> L0 pred finit v
l0_insert_indirection a
a Indirections
ind (L0 IntMap (finit, Maybe (FResult pred v))
fs IntMap Indirections
inds String
time) = IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
forall pred finit v.
IntMap (finit, Maybe (FResult pred v))
-> IntMap Indirections -> String -> L0 pred finit v
L0 IntMap (finit, Maybe (FResult pred v))
fs (Key -> Indirections -> IntMap Indirections -> IntMap Indirections
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert (a -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) Indirections
ind IntMap Indirections
inds) String
time

empty_result :: FResult pred v
empty_result = CFG
-> Postcondition pred
-> Set Word64
-> Set (VerificationCondition v)
-> IntMap (PointerAnalysisResult v)
-> FResult pred v
forall pred v.
CFG
-> Postcondition pred
-> Set Word64
-> Set (VerificationCondition v)
-> IntMap (PointerAnalysisResult v)
-> FResult pred v
FResult (Integer -> CFG
forall {a}. Integral a => a -> CFG
init_cfg Integer
0) Postcondition pred
forall pred. Postcondition pred
TimeOut Set Word64
forall a. Set a
S.empty Set (VerificationCondition v)
forall a. Set a
S.empty IntMap (PointerAnalysisResult v)
forall a. IntMap a
IM.empty





l0_get_cfgs :: L0 pred finit v -> IM.IntMap CFG
l0_get_cfgs :: forall pred finit v. L0 pred finit v -> IntMap CFG
l0_get_cfgs = ((finit, Maybe (FResult pred v)) -> CFG)
-> IntMap (finit, Maybe (FResult pred v)) -> IntMap CFG
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (finit, Maybe (FResult pred v)) -> CFG
forall {a} {pred} {v}. (a, Maybe (FResult pred v)) -> CFG
get_cfg (IntMap (finit, Maybe (FResult pred v)) -> IntMap CFG)
-> (L0 pred finit v -> IntMap (finit, Maybe (FResult pred v)))
-> L0 pred finit v
-> IntMap CFG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions
 where
  get_cfg :: (a, Maybe (FResult pred v)) -> CFG
get_cfg (a
_,Just (FResult CFG
cfg Postcondition pred
_ Set Word64
_ Set (VerificationCondition v)
_ IntMap (PointerAnalysisResult v)
_)) = CFG
cfg

l0_get_function_entries :: L0 pred finit v -> S.Set Int
l0_get_function_entries :: forall pred finit v. L0 pred finit v -> Set Key
l0_get_function_entries = [Key] -> Set Key
forall a. Ord a => [a] -> Set a
S.fromList ([Key] -> Set Key)
-> (L0 pred finit v -> [Key]) -> L0 pred finit v -> Set Key
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap (finit, Maybe (FResult pred v)) -> [Key]
forall a. IntMap a -> [Key]
IM.keys (IntMap (finit, Maybe (FResult pred v)) -> [Key])
-> (L0 pred finit v -> IntMap (finit, Maybe (FResult pred v)))
-> L0 pred finit v
-> [Key]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions

l0_get_pars :: L0 pred finit v -> IM.IntMap (IM.IntMap (PointerAnalysisResult v))
l0_get_pars :: forall pred finit v.
L0 pred finit v -> IntMap (IntMap (PointerAnalysisResult v))
l0_get_pars = ((finit, Maybe (FResult pred v))
 -> IntMap (PointerAnalysisResult v))
-> IntMap (finit, Maybe (FResult pred v))
-> IntMap (IntMap (PointerAnalysisResult v))
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (finit, Maybe (FResult pred v)) -> IntMap (PointerAnalysisResult v)
forall {a} {pred} {v}.
(a, Maybe (FResult pred v)) -> IntMap (PointerAnalysisResult v)
get_par (IntMap (finit, Maybe (FResult pred v))
 -> IntMap (IntMap (PointerAnalysisResult v)))
-> (L0 pred finit v -> IntMap (finit, Maybe (FResult pred v)))
-> L0 pred finit v
-> IntMap (IntMap (PointerAnalysisResult v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
forall pred finit v.
L0 pred finit v -> IntMap (finit, Maybe (FResult pred v))
l0_functions
 where
  get_par :: (a, Maybe (FResult pred v)) -> IntMap (PointerAnalysisResult v)
get_par (a
_,Just (FResult CFG
_ Postcondition pred
_ Set Word64
_ Set (VerificationCondition v)
_ IntMap (PointerAnalysisResult v)
pa)) = IntMap (PointerAnalysisResult v)
pa



type Lifting bin pred finit v = (bin, Config, L0 pred finit v)
type LiftingEntry bin pred finit v = (bin, Config, L0 pred finit v,Word64)

instance (Cereal.Serialize pred) => Cereal.Serialize (Postcondition pred)
instance (Cereal.Serialize v,Cereal.Serialize pred,Ord v) => Cereal.Serialize (FResult pred v)
instance (Cereal.Serialize pred, Cereal.Serialize finit,Cereal.Serialize v, Ord v) => Cereal.Serialize (L0 pred finit v)

instance (NFData pred) => NFData (Postcondition pred)
instance (NFData v, NFData pred) => NFData (FResult pred v)
instance (NFData pred,NFData finit,NFData v) => NFData (L0 pred finit v)

show_indirections :: IM.IntMap Indirections -> String
show_indirections :: IntMap Indirections -> String
show_indirections = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> (IntMap Indirections -> [String])
-> IntMap Indirections
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Key, Indirections) -> String)
-> [(Key, Indirections)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Key, Indirections) -> String
forall {a} {a}. (Integral a, Show a) => (a, Set a) -> String
show_entry ([(Key, Indirections)] -> [String])
-> (IntMap Indirections -> [(Key, Indirections)])
-> IntMap Indirections
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap Indirections -> [(Key, Indirections)]
forall a. IntMap a -> [(Key, a)]
IM.assocs
 where
  show_entry :: (a, Set a) -> String
show_entry (a
a,Set a
inds) 
    | Set a -> Key
forall a. Set a -> Key
S.size Set a
inds Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
1 = a -> String
forall {a}. Integral a => a -> String
showHex a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (a -> String
forall a. Show a => a -> String
show (a -> String) -> a -> String
forall a b. (a -> b) -> a -> b
$ Set a -> a
forall a. Set a -> a
S.findMin Set a
inds)
    | Bool
otherwise        = a -> String
forall {a}. Integral a => a -> String
showHex a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([a] -> String
forall a. Show a => a -> String
show ([a] -> String) -> [a] -> String
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
inds)