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

module WithAbstractPredicates.GenerateInvariants where

import Base
import Config

import WithAbstractPredicates.ControlFlow

import Data.X86.Opcode
import Data.CFG
import Data.VerificationCondition
import Data.L0
import Data.Indirection
import Data.X86.Instruction

import WithAbstractPredicates.Class

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.Maybe
import Data.List
import Control.Monad.State.Strict

-- | Start propagation at the given entry address with the given initial predicate.
-- Returns a set of invariants, i.e., a mapping of instruction addresses to predicates.
--
-- Assumes blockID 0 is start of function
generate_invariants :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> finit -> (IM.IntMap pred,VCS v)
generate_invariants :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> finit -> (IntMap pred, VCS v)
generate_invariants LiftingEntry bin pred finit v
l CFG
cfg finit
finit =
  let p :: pred
p = LiftingEntry bin pred finit v -> finit -> pred
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> finit -> pred
finit_to_init_pred LiftingEntry bin pred finit v
l finit
finit
      (IntMap pred
invs,Set (Int, Int)
_,VCS v
vcs) = State (IntMap pred, Set (Int, Int), VCS v) ()
-> (IntMap pred, Set (Int, Int), VCS v)
-> (IntMap pred, Set (Int, Int), VCS v)
forall s a. State s a -> s -> s
execState (LiftingEntry bin pred finit v
-> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
propagate LiftingEntry bin pred finit v
l CFG
cfg) (Int -> pred -> IntMap pred
forall a. Int -> a -> IntMap a
IM.singleton Int
0 pred
p, CFG -> Int -> Set (Int, Int)
out_edges CFG
cfg Int
0, VCS v
forall a. Set a
S.empty)
      blocks :: [(Int, [Instruction])]
blocks = IntMap [Instruction] -> [(Int, [Instruction])]
forall a. IntMap a -> [(Int, a)]
IM.assocs (IntMap [Instruction] -> [(Int, [Instruction])])
-> IntMap [Instruction] -> [(Int, [Instruction])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg
      end_blocks :: [(Int, [Instruction])]
end_blocks = ((Int, [Instruction]) -> Bool)
-> [(Int, [Instruction])] -> [(Int, [Instruction])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
blockID,[Instruction]
_) -> CFG -> Int -> Bool
is_end_node CFG
cfg Int
blockID) [(Int, [Instruction])]
blocks
      vcs' :: [VCS v]
vcs' = ((Int, [Instruction]) -> VCS v)
-> [(Int, [Instruction])] -> [VCS v]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
blockID,[Instruction]
instrs) -> (pred, VCS v) -> VCS v
forall a b. (a, b) -> b
snd ((pred, VCS v) -> VCS v) -> (pred, VCS v) -> VCS v
forall a b. (a -> b) -> a -> b
$ LiftingEntry bin pred finit v
-> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
get_postcondition_for_block LiftingEntry bin pred finit v
l Int
blockID [Instruction]
instrs IntMap pred
invs) [(Int, [Instruction])]
end_blocks in
    (IntMap pred
invs,[VCS v] -> VCS v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([VCS v] -> VCS v) -> [VCS v] -> VCS v
forall a b. (a -> b) -> a -> b
$ VCS v
vcsVCS v -> [VCS v] -> [VCS v]
forall a. a -> [a] -> [a]
:[VCS v]
vcs')





invs_to_PA :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IM.IntMap pred -> IM.IntMap (PointerAnalysisResult v)
invs_to_PA :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> IntMap (PointerAnalysisResult v)
invs_to_PA l :: LiftingEntry bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
l0,Word64
_) CFG
cfg IntMap pred
invs =
  let blocks :: [(Int, [Instruction])]
blocks = IntMap [Instruction] -> [(Int, [Instruction])]
forall a. IntMap a -> [(Int, a)]
IM.assocs (IntMap [Instruction] -> [(Int, [Instruction])])
-> IntMap [Instruction] -> [(Int, [Instruction])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg
      pa :: IntMap (PointerAnalysisResult v)
pa     = [IntMap (PointerAnalysisResult v)]
-> IntMap (PointerAnalysisResult v)
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap (PointerAnalysisResult v)]
 -> IntMap (PointerAnalysisResult v))
-> [IntMap (PointerAnalysisResult v)]
-> IntMap (PointerAnalysisResult v)
forall a b. (a -> b) -> a -> b
$ ((Int, [Instruction]) -> IntMap (PointerAnalysisResult v))
-> [(Int, [Instruction])] -> [IntMap (PointerAnalysisResult v)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Instruction]) -> IntMap (PointerAnalysisResult v)
get_pa [(Int, [Instruction])]
blocks in
    IntMap (PointerAnalysisResult v)
pa
 where
  get_pa :: (Int, [Instruction]) -> IntMap (PointerAnalysisResult v)
get_pa (Int
blockID,[Instruction]
instrs) = 
    let inv :: pred
inv     = IntMap pred
invs IntMap pred -> Int -> pred
forall a. IntMap a -> Int -> a
IM.! Int
blockID
        (pred
_,VCS v
vcs) = State (pred, VCS v) () -> (pred, VCS v) -> (pred, VCS v)
forall s a. State s a -> s -> s
execState (LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
symbolically_execute LiftingEntry bin pred finit v
l Bool
True [Instruction]
instrs Maybe [Instruction]
forall a. Maybe a
Nothing) (pred
inv,VCS v
forall a. Set a
S.empty) in
      VCS v -> IntMap (PointerAnalysisResult v)
forall v. VCS v -> IntMap (PointerAnalysisResult v)
gather_pa_results VCS v
vcs



invs_to_post :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IM.IntMap pred -> Postcondition pred
invs_to_post :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> IntMap pred -> Postcondition pred
invs_to_post l :: LiftingEntry bin pred finit v
l@(bin
bin,Config
_,L0 pred finit v
l0,Word64
_) CFG
cfg IntMap pred
invs =
  let blocks :: [(Int, [Instruction])]
blocks = IntMap [Instruction] -> [(Int, [Instruction])]
forall a. IntMap a -> [(Int, a)]
IM.assocs (IntMap [Instruction] -> [(Int, [Instruction])])
-> IntMap [Instruction] -> [(Int, [Instruction])]
forall a b. (a -> b) -> a -> b
$ CFG -> IntMap [Instruction]
cfg_instrs CFG
cfg
      end_blocks :: [(Int, [Instruction])]
end_blocks = ((Int, [Instruction]) -> Bool)
-> [(Int, [Instruction])] -> [(Int, [Instruction])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
blockID,[Instruction]
_) -> CFG -> Int -> Bool
is_end_node CFG
cfg Int
blockID) [(Int, [Instruction])]
blocks
      posts :: [(Int, Postcondition pred)]
posts = ((Int, [Instruction]) -> (Int, Postcondition pred))
-> [(Int, [Instruction])] -> [(Int, Postcondition pred)]
forall a b. (a -> b) -> [a] -> [b]
map (LiftingEntry bin pred finit v
-> IntMap pred -> (Int, [Instruction]) -> (Int, Postcondition pred)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> IntMap pred -> (Int, [Instruction]) -> (Int, Postcondition pred)
get_post LiftingEntry bin pred finit v
l IntMap pred
invs) [(Int, [Instruction])]
end_blocks in
    [(Int, Postcondition pred)] -> Postcondition pred
join_postconditions [(Int, Postcondition pred)]
posts
 where
  join_postconditions :: [(Int, Postcondition pred)] -> Postcondition pred
join_postconditions [(Int, Postcondition pred)]
posts
    | ((Int, Postcondition pred) -> Bool)
-> [(Int, Postcondition pred)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Postcondition pred -> Postcondition pred -> Bool
forall a. Eq a => a -> a -> Bool
(==) Postcondition pred
forall pred. Postcondition pred
Terminates (Postcondition pred -> Bool)
-> ((Int, Postcondition pred) -> Postcondition pred)
-> (Int, Postcondition pred)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Postcondition pred) -> Postcondition pred
forall a b. (a, b) -> b
snd) [(Int, Postcondition pred)]
posts = Postcondition pred
forall pred. Postcondition pred
Terminates
    | ((Int, Postcondition pred) -> Bool)
-> [(Int, Postcondition pred)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Postcondition pred -> Postcondition pred -> Bool
forall a. Eq a => a -> a -> Bool
(==) Postcondition pred
forall pred. Postcondition pred
TimeOut (Postcondition pred -> Bool)
-> ((Int, Postcondition pred) -> Postcondition pred)
-> (Int, Postcondition pred)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Postcondition pred) -> Postcondition pred
forall a b. (a, b) -> b
snd) [(Int, Postcondition pred)]
posts = Postcondition pred
forall pred. Postcondition pred
TimeOut
    | ((Int, Postcondition pred) -> Bool)
-> [(Int, Postcondition pred)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Postcondition pred -> Bool
forall {pred}. Postcondition pred -> Bool
is_unresolved_indirection (Postcondition pred -> Bool)
-> ((Int, Postcondition pred) -> Postcondition pred)
-> (Int, Postcondition pred)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Postcondition pred) -> Postcondition pred
forall a b. (a, b) -> b
snd) [(Int, Postcondition pred)]
posts = [Postcondition pred] -> Postcondition pred
forall {t :: * -> *} {pred} {pred}.
Foldable t =>
t (Postcondition pred) -> Postcondition pred
join_unresolved_indirections ([Postcondition pred] -> Postcondition pred)
-> [Postcondition pred] -> Postcondition pred
forall a b. (a -> b) -> a -> b
$ ((Int, Postcondition pred) -> Postcondition pred)
-> [(Int, Postcondition pred)] -> [Postcondition pred]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Postcondition pred) -> Postcondition pred
forall a b. (a, b) -> b
snd [(Int, Postcondition pred)]
posts
    | Bool
otherwise =
      let errors :: [(Int, Postcondition pred)]
errors = ((Int, Postcondition pred) -> Bool)
-> [(Int, Postcondition pred)] -> [(Int, Postcondition pred)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, Postcondition pred) -> Bool
forall {a}. (a, Postcondition pred) -> Bool
is_error [(Int, Postcondition pred)]
posts in
        case [(Int, Postcondition pred)]
errors of
          [] -> pred -> Postcondition pred
forall pred. pred -> Postcondition pred
ReturnsWith (pred -> Postcondition pred) -> pred -> Postcondition pred
forall a b. (a -> b) -> a -> b
$ (pred -> pred -> pred) -> [pred] -> pred
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (LiftingEntry bin pred finit v -> pred -> pred -> pred
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> pred -> pred
join_preds LiftingEntry bin pred finit v
l) ([pred] -> pred) -> [pred] -> pred
forall a b. (a -> b) -> a -> b
$ (Postcondition pred -> Maybe pred)
-> [Postcondition pred] -> [pred]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Postcondition pred -> Maybe pred
forall {a}. Postcondition a -> Maybe a
get_return_pred ([Postcondition pred] -> [pred]) -> [Postcondition pred] -> [pred]
forall a b. (a -> b) -> a -> b
$ ((Int, Postcondition pred) -> Postcondition pred)
-> [(Int, Postcondition pred)] -> [Postcondition pred]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Postcondition pred) -> Postcondition pred
forall a b. (a, b) -> b
snd [(Int, Postcondition pred)]
posts
          [(Int, Postcondition pred)]
_  -> [(Int, pred)] -> Postcondition pred
forall pred. [(Int, pred)] -> Postcondition pred
VerificationError ([(Int, pred)] -> Postcondition pred)
-> [(Int, pred)] -> Postcondition pred
forall a b. (a -> b) -> a -> b
$ ((Int, Postcondition pred) -> (Int, pred))
-> [(Int, Postcondition pred)] -> [(Int, pred)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
blockID,ReturnsWith pred
pred) -> (Int
blockID,pred
pred)) [(Int, Postcondition pred)]
errors

  is_error :: (a, Postcondition pred) -> Bool
is_error (a
blockID, ReturnsWith pred
pred) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ LiftingEntry bin pred finit v -> pred -> Bool
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> Bool
verify_postcondition LiftingEntry bin pred finit v
l pred
pred
  is_error (a, Postcondition pred)
_ = Bool
False

  get_return_pred :: Postcondition a -> Maybe a
get_return_pred (ReturnsWith a
pred) = a -> Maybe a
forall a. a -> Maybe a
Just a
pred
  get_return_pred Postcondition a
_ = Maybe a
forall a. Maybe a
Nothing


  join_unresolved_indirections :: t (Postcondition pred) -> Postcondition pred
join_unresolved_indirections t (Postcondition pred)
posts = [Int] -> Postcondition pred
forall pred. [Int] -> Postcondition pred
HasUnresolvedIndirections ([Int] -> Postcondition pred) -> [Int] -> Postcondition pred
forall a b. (a -> b) -> a -> b
$ (Postcondition pred -> [Int]) -> t (Postcondition pred) -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Postcondition pred -> [Int]
forall {pred}. Postcondition pred -> [Int]
get_unresolved_indirections t (Postcondition pred)
posts
  get_unresolved_indirections :: Postcondition pred -> [Int]
get_unresolved_indirections (HasUnresolvedIndirections [Int]
blockIDs) = [Int]
blockIDs
  get_unresolved_indirections Postcondition pred
_ = []
  is_unresolved_indirection :: Postcondition pred -> Bool
is_unresolved_indirection (HasUnresolvedIndirections [Int]
_) = Bool
True
  is_unresolved_indirection Postcondition pred
_ = Bool
False


  has_unresolved_instruction :: L0 pred finit v -> (a, t Instruction) -> Bool
has_unresolved_instruction L0 pred finit v
l0 (a
blockID,t Instruction
instrs) = (Instruction -> Bool) -> t Instruction -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (L0 pred finit v -> Instruction -> Bool
forall {pred} {finit} {v}. L0 pred finit v -> Instruction -> Bool
is_unresolved_instruction L0 pred finit v
l0) t Instruction
instrs
  is_unresolved_instruction :: L0 pred finit v -> Instruction -> Bool
is_unresolved_instruction L0 pred finit v
l0 Instruction
i
    | Opcode -> Bool
isCall (Instruction -> Opcode
inOperation Instruction
i) Bool -> Bool -> Bool
|| Opcode -> Bool
isJump (Instruction -> Opcode
inOperation Instruction
i) = Maybe (Set Indirection) -> Bool
has_unresolved_indirections (Maybe (Set Indirection) -> Bool)
-> Maybe (Set Indirection) -> Bool
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (Set Indirection)
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (Set Indirection)
l0_lookup_indirection (Instruction -> Word64
inAddress Instruction
i) L0 pred finit v
l0
    | Bool
otherwise = Bool
False

  get_post :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> IM.IntMap pred -> (Int,[Instruction]) -> (Int,Postcondition pred)
  get_post :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> IntMap pred -> (Int, [Instruction]) -> (Int, Postcondition pred)
get_post l :: LiftingEntry bin pred finit v
l@(bin
_,Config
_,L0 pred finit v
l0,Word64
_) IntMap pred
invs (Int
blockID,[Instruction]
instrs) =
    if Maybe (Set Indirection) -> Bool
has_unresolved_indirections (Maybe (Set Indirection) -> Bool)
-> Maybe (Set Indirection) -> Bool
forall a b. (a -> b) -> a -> b
$ Word64 -> L0 pred finit v -> Maybe (Set Indirection)
forall {a} {pred} {finit} {v}.
Integral a =>
a -> L0 pred finit v -> Maybe (Set Indirection)
l0_lookup_indirection (Instruction -> Word64
inAddress (Instruction -> Word64) -> Instruction -> Word64
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) L0 pred finit v
l0 then
      (Int
blockID,[Int] -> Postcondition pred
forall pred. [Int] -> Postcondition pred
HasUnresolvedIndirections [Int
blockID])
    else case Lifting bin pred finit v -> Maybe Instruction -> NextRips
forall bin pred finit v.
(BinaryClass bin, Eq pred) =>
Lifting bin pred finit v -> Maybe Instruction -> NextRips
next_rips (LiftingEntry bin pred finit v -> Lifting bin pred finit v
forall {a} {b} {c} {d}. (a, b, c, d) -> (a, b, c)
withoutEntry LiftingEntry bin pred finit v
l) (Instruction -> Maybe Instruction
forall a. a -> Maybe a
Just (Instruction -> Maybe Instruction)
-> Instruction -> Maybe Instruction
forall a b. (a -> b) -> a -> b
$ [Instruction] -> Instruction
forall a. HasCallStack => [a] -> a
last [Instruction]
instrs) of
      NextRips
UnresolvedTarget -> [Char] -> (Int, Postcondition pred)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (Int, Postcondition pred))
-> [Char] -> (Int, Postcondition pred)
forall a b. (a -> b) -> a -> b
$ (Int, [Instruction]) -> [Char]
forall a. Show a => a -> [Char]
show (Int
blockID,[Instruction]
instrs)  -- HasUnresolvedIndirections
      NextRips
Terminal         -> (Int
blockID,Postcondition pred
forall pred. Postcondition pred
Terminates)
      JustRips []      -> (Int
blockID,pred -> Postcondition pred
forall pred. pred -> Postcondition pred
ReturnsWith (pred -> Postcondition pred) -> pred -> Postcondition pred
forall a b. (a -> b) -> a -> b
$ (pred, VCS v) -> pred
forall a b. (a, b) -> a
fst ((pred, VCS v) -> pred) -> (pred, VCS v) -> pred
forall a b. (a -> b) -> a -> b
$ LiftingEntry bin pred finit v
-> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
get_postcondition_for_block LiftingEntry bin pred finit v
l Int
blockID [Instruction]
instrs IntMap pred
invs)


  has_unresolved_indirections :: Maybe (Set Indirection) -> Bool
has_unresolved_indirections (Just Set Indirection
inds) = Indirection
Indirection_Unresolved Indirection -> Set Indirection -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Indirection
inds
  has_unresolved_indirections Maybe (Set Indirection)
Nothing = Bool
False

withEntry :: d -> (a, b, c) -> (a, b, c, d)
withEntry d
entry (a
a,b
b,c
c) = (a
a,b
b,c
c,d
entry) 
withoutEntry :: (a, b, c, d) -> (a, b, c)
withoutEntry (a
a,b
b,c
c,d
entry) = (a
a,b
b,c
c)

get_postcondition_for_block :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> Int -> [Instruction] -> IM.IntMap pred -> (pred,VCS v)
get_postcondition_for_block :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
get_postcondition_for_block LiftingEntry bin pred finit v
l Int
blockID [Instruction]
instrs IntMap pred
invs =
  let pre :: pred
pre = Maybe pred -> pred
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe pred -> pred) -> Maybe pred -> pred
forall a b. (a -> b) -> a -> b
$ Int -> IntMap pred -> Maybe pred
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
blockID IntMap pred
invs in
   State (pred, VCS v) () -> (pred, VCS v) -> (pred, VCS v)
forall s a. State s a -> s -> s
execState (LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
symbolically_execute LiftingEntry bin pred finit v
l Bool
False [Instruction]
instrs Maybe [Instruction]
forall a. Maybe a
Nothing) (pred
pre,VCS v
forall a. Set a
S.empty)







-- PROPAGATION
--
--
-- propagation
-- The state consists of 
-- 		1.) the current mapping of addresses to predicates 
-- 		2.) the current bag (a set of edges to be explored)
--


propagate :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> State (IM.IntMap pred, S.Set (Int,Int), VCS v) ()
propagate :: forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
propagate LiftingEntry bin pred finit v
l CFG
g = do
  Maybe ((Int, Int), Set (Int, Int))
pick <- StateT
  (IntMap pred, Set (Int, Int), VCS v)
  Identity
  (Maybe ((Int, Int), Set (Int, Int)))
pick_edge_from_bag
  case Maybe ((Int, Int), Set (Int, Int))
pick of
    Maybe ((Int, Int), Set (Int, Int))
Nothing -> () -> State (IntMap pred, Set (Int, Int), VCS v) ()
forall a.
a -> StateT (IntMap pred, Set (Int, Int), VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ((Int
v0,Int
v1),Set (Int, Int)
bag') -> do
      ((IntMap pred, Set (Int, Int), VCS v)
 -> (IntMap pred, Set (Int, Int), VCS v))
-> State (IntMap pred, Set (Int, Int), VCS v) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((IntMap pred, Set (Int, Int), VCS v)
  -> (IntMap pred, Set (Int, Int), VCS v))
 -> State (IntMap pred, Set (Int, Int), VCS v) ())
-> ((IntMap pred, Set (Int, Int), VCS v)
    -> (IntMap pred, Set (Int, Int), VCS v))
-> State (IntMap pred, Set (Int, Int), VCS v) ()
forall a b. (a -> b) -> a -> b
$ Set (Int, Int)
-> (IntMap pred, Set (Int, Int), VCS v)
-> (IntMap pred, Set (Int, Int), VCS v)
forall {b} {a} {b} {c}. b -> (a, b, c) -> (a, b, c)
put_bag Set (Int, Int)
bag'
      -- take an edge (v0,v1) out of the bag
      (IntMap pred
m,Set (Int, Int)
_,VCS v
_) <- StateT
  (IntMap pred, Set (Int, Int), VCS v)
  Identity
  (IntMap pred, Set (Int, Int), VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
      -- do predicate transformation on the currently available precondition of v0
      let p :: pred
p = IntMap pred
m IntMap pred -> Int -> pred
forall a. IntMap a -> Int -> a
IM.! Int
v0
      -- this produces q: the precondition for v1
      let (pred
q,VCS v
vcs') = State (pred, VCS v) () -> (pred, VCS v) -> (pred, VCS v)
forall s a. State s a -> s -> s
execState (LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (pred, VCS v) ()
symbolically_execute LiftingEntry bin pred finit v
l Bool
False (CFG -> Int -> [Instruction]
fetch_block CFG
g Int
v0) ([Instruction] -> Maybe [Instruction]
forall a. a -> Maybe a
Just ([Instruction] -> Maybe [Instruction])
-> [Instruction] -> Maybe [Instruction]
forall a b. (a -> b) -> a -> b
$ CFG -> Int -> [Instruction]
fetch_block CFG
g Int
v1)) (pred
p,VCS v
forall a. Set a
S.empty)
      ((IntMap pred, Set (Int, Int), VCS v)
 -> (IntMap pred, Set (Int, Int), VCS v))
-> State (IntMap pred, Set (Int, Int), VCS v) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((IntMap pred, Set (Int, Int), VCS v)
  -> (IntMap pred, Set (Int, Int), VCS v))
 -> State (IntMap pred, Set (Int, Int), VCS v) ())
-> ((IntMap pred, Set (Int, Int), VCS v)
    -> (IntMap pred, Set (Int, Int), VCS v))
-> State (IntMap pred, Set (Int, Int), VCS v) ()
forall a b. (a -> b) -> a -> b
$ VCS v
-> (IntMap pred, Set (Int, Int), VCS v)
-> (IntMap pred, Set (Int, Int), VCS v)
forall {a} {a} {b}.
Ord a =>
Set a -> (a, b, Set a) -> (a, b, Set a)
add_vcs VCS v
vcs'
      -- store q
      LiftingEntry bin pred finit v
-> pred -> Int -> State (IntMap pred, Set (Int, Int), VCS v) ()
forall {m :: * -> *} {a} {c} {bin} {finit} {v}.
(MonadState (IntMap a, Set (Int, Int), c) m,
 WithAbstractPredicates bin a finit v) =>
LiftingEntry bin a finit v -> a -> Int -> m ()
add_predicate LiftingEntry bin pred finit v
l pred
q Int
v1
      -- continue
      LiftingEntry bin pred finit v
-> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v
-> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
propagate LiftingEntry bin pred finit v
l CFG
g
 where
  pick_edge_from_bag :: StateT
  (IntMap pred, Set (Int, Int), VCS v)
  Identity
  (Maybe ((Int, Int), Set (Int, Int)))
pick_edge_from_bag = do
    (IntMap pred
m,Set (Int, Int)
bag,VCS v
vcs) <- StateT
  (IntMap pred, Set (Int, Int), VCS v)
  Identity
  (IntMap pred, Set (Int, Int), VCS v)
forall s (m :: * -> *). MonadState s m => m s
get
    case ((Int, Int) -> Bool) -> Set (Int, Int) -> Maybe (Int, Int)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(Int
v0,Int
v1) -> Int -> IntMap pred -> Bool
forall a. Int -> IntMap a -> Bool
IM.member Int
v1 IntMap pred
m) Set (Int, Int)
bag of
      Just (Int, Int)
edge -> Maybe ((Int, Int), Set (Int, Int))
-> StateT
     (IntMap pred, Set (Int, Int), VCS v)
     Identity
     (Maybe ((Int, Int), Set (Int, Int)))
forall a.
a -> StateT (IntMap pred, Set (Int, Int), VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ((Int, Int), Set (Int, Int))
 -> StateT
      (IntMap pred, Set (Int, Int), VCS v)
      Identity
      (Maybe ((Int, Int), Set (Int, Int))))
-> Maybe ((Int, Int), Set (Int, Int))
-> StateT
     (IntMap pred, Set (Int, Int), VCS v)
     Identity
     (Maybe ((Int, Int), Set (Int, Int)))
forall a b. (a -> b) -> a -> b
$ ((Int, Int), Set (Int, Int)) -> Maybe ((Int, Int), Set (Int, Int))
forall a. a -> Maybe a
Just ((Int, Int)
edge, (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => a -> Set a -> Set a
S.delete (Int, Int)
edge Set (Int, Int)
bag)
      Maybe (Int, Int)
Nothing   -> Maybe ((Int, Int), Set (Int, Int))
-> StateT
     (IntMap pred, Set (Int, Int), VCS v)
     Identity
     (Maybe ((Int, Int), Set (Int, Int)))
forall a.
a -> StateT (IntMap pred, Set (Int, Int), VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ((Int, Int), Set (Int, Int))
 -> StateT
      (IntMap pred, Set (Int, Int), VCS v)
      Identity
      (Maybe ((Int, Int), Set (Int, Int))))
-> Maybe ((Int, Int), Set (Int, Int))
-> StateT
     (IntMap pred, Set (Int, Int), VCS v)
     Identity
     (Maybe ((Int, Int), Set (Int, Int)))
forall a b. (a -> b) -> a -> b
$ Set (Int, Int) -> Maybe ((Int, Int), Set (Int, Int))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (Int, Int)
bag

  put_bag :: b -> (a, b, c) -> (a, b, c)
put_bag b
bag (a
m,b
_,c
vcs) = (a
m,b
bag,c
vcs)

  add_vcs :: Set a -> (a, b, Set a) -> (a, b, Set a)
add_vcs Set a
vcs' (a
m,b
bag,Set a
vcs) = (a
m,b
bag,Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.union Set a
vcs Set a
vcs')

  add_predicate :: LiftingEntry bin a finit v -> a -> Int -> m ()
add_predicate LiftingEntry bin a finit v
l a
q Int
v1 = do
   (IntMap a
m,Set (Int, Int)
bag,c
vcs) <- m (IntMap a, Set (Int, Int), c)
forall s (m :: * -> *). MonadState s m => m s
get
   case Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v1 IntMap a
m of
     Maybe a
Nothing -> do
       -- first time visit, store q and explore all outgoing edges
       (IntMap a, Set (Int, Int), c) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> a -> IntMap a -> IntMap a
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v1 a
q IntMap a
m, Set (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Int, Int)
bag (Set (Int, Int) -> Set (Int, Int))
-> Set (Int, Int) -> Set (Int, Int)
forall a b. (a -> b) -> a -> b
$ CFG -> Int -> Set (Int, Int)
out_edges CFG
g Int
v1,c
vcs)
     Just a
p -> do
       if LiftingEntry bin a finit v -> a -> a -> Bool
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> pred -> Bool
is_weaker_than LiftingEntry bin a finit v
l a
p a
q then
         -- previously visited, no need for further exploration
         () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- put (IM.insert v1 j m, bag, vcs)
       else do
         let j :: a
j = LiftingEntry bin a finit v -> a -> a -> a
forall bin pred finit v.
WithAbstractPredicates bin pred finit v =>
LiftingEntry bin pred finit v -> pred -> pred -> pred
join_preds LiftingEntry bin a finit v
l a
p a
q
         -- previously visited, need to weaken invariant by joining
         (IntMap a, Set (Int, Int), c) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> a -> IntMap a -> IntMap a
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v1 a
j IntMap a
m,Set (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Int, Int)
bag (Set (Int, Int) -> Set (Int, Int))
-> Set (Int, Int) -> Set (Int, Int)
forall a b. (a -> b) -> a -> b
$ CFG -> Int -> Set (Int, Int)
out_edges CFG
g Int
v1,c
vcs)

out_edges :: CFG -> Int -> Set (Int, Int)
out_edges CFG
g Int
v = [(Int, Int)] -> Set (Int, Int)
forall a. Ord a => [a] -> Set a
S.fromList ([(Int, Int)] -> Set (Int, Int)) -> [(Int, Int)] -> Set (Int, Int)
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. a -> [a]
repeat Int
v) ([Int] -> [(Int, Int)]) -> [Int] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ CFG -> Int -> IntSet
post CFG
g Int
v