{-# LANGUAGE DeriveGeneric #-}

module WithAbstractSymbolicValues.FInit where

import Base

import WithAbstractSymbolicValues.Class
import WithAbstractSymbolicValues.Sstate

import Data.SymbolicExpression (FlagStatus(..)) -- TODO
import Data.X86.Instruction
import Data.X86.Register
import Data.Size


import Algorithm.SCC


import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified Data.Set.NonEmpty as NES
import Data.List
import Data.Maybe

import GHC.Generics (Generic)
import Control.DeepSeq
import qualified Data.Serialize as Cereal





-- | Show function initialisation
instance (Eq v, Show v, Show p) => Show (FInit v p) where
 show :: FInit v p -> String
show (FInit Set (SStatePart p, v)
sps Map (SStatePart p, SStatePart p) MemRelation
m) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([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 -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((SStatePart p, v) -> String) -> [(SStatePart p, v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SStatePart p, v) -> String
forall {a} {a}. (Show a, Show a) => (SStatePart a, a) -> String
show_sp_v ([(SStatePart p, v)] -> [String])
-> [(SStatePart p, v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Set (SStatePart p, v) -> [(SStatePart p, v)]
forall a. Set a -> [a]
S.toList Set (SStatePart p, v)
sps
  , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((SStatePart p, SStatePart p), MemRelation) -> String)
-> [((SStatePart p, SStatePart p), MemRelation)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((SStatePart p, SStatePart p), MemRelation) -> String
forall {a} {b} {a}.
(Show a, Show b, Show a) =>
((a, b), a) -> String
show_entry ([((SStatePart p, SStatePart p), MemRelation)] -> [String])
-> [((SStatePart p, SStatePart p), MemRelation)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map (SStatePart p, SStatePart p) MemRelation
-> [((SStatePart p, SStatePart p), MemRelation)]
forall k a. Map k a -> [(k, a)]
M.toList Map (SStatePart p, SStatePart p) MemRelation
m ]
  where
    show_sp_v :: (SStatePart a, a) -> String
show_sp_v (SStatePart a
sp,a
v) = SStatePart a -> String
forall {a}. Show a => SStatePart a -> String
show_sp SStatePart a
sp 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
v
    show_sp :: SStatePart a -> String
show_sp (SSP_Reg Register
r) = Register -> String
forall a. Show a => a -> String
show Register
r
    show_sp (SSP_Mem a
a Int
si) = String
"*[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
    show_entry :: ((a, b), a) -> String
show_entry ((a
sp0,b
sp1),a
r) = (a, b) -> String
forall a. Show a => a -> String
show (a
sp0,b
sp1) 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
r

instance Show p => Show (SStatePart p) where
  show :: SStatePart p -> String
show (SSP_Reg Register
r)        = Register -> String
forall a. Show a => a -> String
show Register
r
  show (SSP_Mem p
a Int
si)     = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ p -> String
forall a. Show a => a -> String
show p
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"


-- | The initial predicate.
finit_to_init_sstate :: WithAbstractSymbolicValues ctxt v p => ctxt -> FInit v p -> Sstate v p
finit_to_init_sstate :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> FInit v p -> Sstate v p
finit_to_init_sstate ctxt
ctxt finit :: FInit v p
finit@(FInit Set (SStatePart p, v)
sps Map (SStatePart p, SStatePart p) MemRelation
init_mem) =
  let rsp0 :: v
rsp0                 = ctxt -> Register -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Register -> v
smk_init_reg_value ctxt
ctxt (Register -> v) -> Register -> v
forall a b. (a -> b) -> a -> b
$ GPR -> Register
Reg64 GPR
RSP
      write_stack_pointer :: State (Sstate v p, VCS v) ()
write_stack_pointer  = ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> Register -> v -> State (Sstate v p, VCS v) ()
swrite_rreg ctxt
ctxt String
"finit_to_init" (GPR -> Register
Reg64 GPR
RSP) v
rsp0

      [p
rsp0_pointer]       = Set p -> [p]
forall a. Set a -> [a]
S.toList (Set p -> [p]) -> Set p -> [p]
forall a b. (a -> b) -> a -> b
$ ctxt -> String -> v -> Set p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt String
"RSP0" v
rsp0
      top_stack_frame :: v
top_stack_frame      = ctxt -> String -> p -> Maybe ByteSize -> v
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> p -> Maybe ByteSize -> v
smk_init_mem_value ctxt
ctxt String
"[RSP0,8]" p
rsp0_pointer (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
8)
      write_return_address :: State (Sstate v p, VCS v) ()
write_return_address = ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool -> v -> Maybe ByteSize -> v -> State (Sstate v p, VCS v) ()
swrite_mem ctxt
ctxt Bool
False v
rsp0 (ByteSize -> Maybe ByteSize
forall a. a -> Maybe a
Just (ByteSize -> Maybe ByteSize) -> ByteSize -> Maybe ByteSize
forall a b. (a -> b) -> a -> b
$ Int -> ByteSize
ByteSize Int
8) v
top_stack_frame

      sregs :: Map k a
sregs                = Map k a
forall k a. Map k a
M.empty
      smem :: Map k a
smem                 = Map k a
forall k a. Map k a
M.empty in
    State (Sstate v p, VCS v) () -> Sstate v p -> Sstate v p
forall v p b.
State (Sstate v p, VCS v) b -> Sstate v p -> Sstate v p
execSstate (State (Sstate v p, VCS v) ()
write_stack_pointer State (Sstate v p, VCS v) ()
-> State (Sstate v p, VCS v) () -> State (Sstate v p, VCS v) ()
forall a b.
StateT (Sstate v p, VCS v) Identity a
-> StateT (Sstate v p, VCS v) Identity b
-> StateT (Sstate v p, VCS v) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State (Sstate v p, VCS v) ()
write_return_address State (Sstate v p, VCS v) ()
-> State (Sstate v p, VCS v) () -> State (Sstate v p, VCS v) ()
forall a b.
StateT (Sstate v p, VCS v) Identity a
-> StateT (Sstate v p, VCS v) Identity b
-> StateT (Sstate v p, VCS v) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [(SStatePart p, v)] -> State (Sstate v p, VCS v) ()
write_finit (Set (SStatePart p, v) -> [(SStatePart p, v)]
forall a. Set a -> [a]
S.toList Set (SStatePart p, v)
sps)) (Map Register v
-> Map (p, Maybe ByteSize) v -> FlagStatus -> Sstate v p
forall v p.
Map Register v
-> Map (p, Maybe ByteSize) v -> FlagStatus -> Sstate v p
Sstate Map Register v
forall k a. Map k a
sregs Map (p, Maybe ByteSize) v
forall k a. Map k a
smem FlagStatus
None)
 where
  write_finit :: [(SStatePart p, v)] -> State (Sstate v p, VCS v) ()
write_finit []             = () -> State (Sstate v p, VCS v) ()
forall a. a -> StateT (Sstate v p, VCS v) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  write_finit ((SStatePart p
sp,v
v):[(SStatePart p, v)]
finit) = ctxt -> SStatePart p -> v -> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> SStatePart p -> v -> State (Sstate v p, VCS v) ()
write_sp ctxt
ctxt SStatePart p
sp v
v State (Sstate v p, VCS v) ()
-> State (Sstate v p, VCS v) () -> State (Sstate v p, VCS v) ()
forall a b.
StateT (Sstate v p, VCS v) Identity a
-> StateT (Sstate v p, VCS v) Identity b
-> StateT (Sstate v p, VCS v) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [(SStatePart p, v)] -> State (Sstate v p, VCS v) ()
write_finit [(SStatePart p, v)]
finit 



-- | Convert the current invariant into a function initialisation
sstate_to_finit :: WithAbstractSymbolicValues ctxt v p => ctxt -> Sstate v p -> FInit v p
---invariant_to_finit ctxt p | trace ("invariant_to_finit: "++ show p) False = error "trace"
sstate_to_finit :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Sstate v p -> FInit v p
sstate_to_finit ctxt
ctxt Sstate v p
p = 
  let sps :: Set (SStatePart p, v, Set p)
sps      = [(SStatePart p, v, Set p)] -> Set (SStatePart p, v, Set p)
forall a. Ord a => [a] -> Set a
S.fromList ([(SStatePart p, v, Set p)] -> Set (SStatePart p, v, Set p))
-> [(SStatePart p, v, Set p)] -> Set (SStatePart p, v, Set p)
forall a b. (a -> b) -> a -> b
$ Map Register v -> [(SStatePart p, v, Set p)]
forall {p}. Map Register v -> [(SStatePart p, v, Set p)]
regs_to_sps (Sstate v p -> Map Register v
forall v p. Sstate v p -> Map Register v
sregs Sstate v p
p) [(SStatePart p, v, Set p)]
-> [(SStatePart p, v, Set p)] -> [(SStatePart p, v, Set p)]
forall a. [a] -> [a] -> [a]
++ Map (p, Maybe ByteSize) v -> [(SStatePart p, v, Set p)]
mem_to_sps (Sstate v p -> Map (p, Maybe ByteSize) v
forall v p. Sstate v p -> Map (p, Maybe ByteSize) v
smem Sstate v p
p)
      pairs :: [((SStatePart p, v, Set p), (SStatePart p, v, Set p))]
pairs    = Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
-> [((SStatePart p, v, Set p), (SStatePart p, v, Set p))]
forall a. Set a -> [a]
S.toList (Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
 -> [((SStatePart p, v, Set p), (SStatePart p, v, Set p))])
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
-> [((SStatePart p, v, Set p), (SStatePart p, v, Set p))]
forall a b. (a -> b) -> a -> b
$ (((SStatePart p, v, Set p), (SStatePart p, v, Set p)) -> Bool)
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
forall a. (a -> Bool) -> Set a -> Set a
S.filter (\((SStatePart p, v, Set p)
x,(SStatePart p, v, Set p)
y) -> (SStatePart p, v, Set p)
x (SStatePart p, v, Set p) -> (SStatePart p, v, Set p) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SStatePart p, v, Set p)
y) (Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
 -> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p)))
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
forall a b. (a -> b) -> a -> b
$ Set (SStatePart p, v, Set p)
-> Set (SStatePart p, v, Set p)
-> Set ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
forall a b. Set a -> Set b -> Set (a, b)
S.cartesianProduct Set (SStatePart p, v, Set p)
sps Set (SStatePart p, v, Set p)
sps
      mem_rels :: Map (SStatePart p, SStatePart p) MemRelation
mem_rels = [((SStatePart p, SStatePart p), MemRelation)]
-> Map (SStatePart p, SStatePart p) MemRelation
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((SStatePart p, SStatePart p), MemRelation)]
 -> Map (SStatePart p, SStatePart p) MemRelation)
-> [((SStatePart p, SStatePart p), MemRelation)]
-> Map (SStatePart p, SStatePart p) MemRelation
forall a b. (a -> b) -> a -> b
$ (((SStatePart p, v, Set p), (SStatePart p, v, Set p))
 -> Maybe ((SStatePart p, SStatePart p), MemRelation))
-> [((SStatePart p, v, Set p), (SStatePart p, v, Set p))]
-> [((SStatePart p, SStatePart p), MemRelation)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (ctxt
-> ((SStatePart p, v, Set p), (SStatePart p, v, Set p))
-> Maybe ((SStatePart p, SStatePart p), MemRelation)
forall {t :: * -> *} {t :: * -> *} {ctxt} {v} {p} {a} {b} {b} {b}.
(Foldable t, Foldable t, WithAbstractSymbolicValues ctxt v p) =>
ctxt -> ((a, b, t p), (b, b, t p)) -> Maybe ((a, b), MemRelation)
mk_memrel ctxt
ctxt) [((SStatePart p, v, Set p), (SStatePart p, v, Set p))]
pairs in
    Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
forall v p.
Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
FInit (((SStatePart p, v) -> Bool)
-> Set (SStatePart p, v) -> Set (SStatePart p, v)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (SStatePart p, v) -> Bool
keep_sp (Set (SStatePart p, v) -> Set (SStatePart p, v))
-> Set (SStatePart p, v) -> Set (SStatePart p, v)
forall a b. (a -> b) -> a -> b
$ ((SStatePart p, v, Set p) -> (SStatePart p, v))
-> Set (SStatePart p, v, Set p) -> Set (SStatePart p, v)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\(SStatePart p
sp,v
v,Set p
p) -> (SStatePart p
sp,v
v)) (Set (SStatePart p, v, Set p) -> Set (SStatePart p, v))
-> Set (SStatePart p, v, Set p) -> Set (SStatePart p, v)
forall a b. (a -> b) -> a -> b
$ Set (SStatePart p, v, Set p)
sps) Map (SStatePart p, SStatePart p) MemRelation
mem_rels
 where
    regs_to_sps :: Map Register v -> [(SStatePart p, v, Set p)]
regs_to_sps Map Register v
regs = ((Register, v) -> Maybe (SStatePart p, v, Set p))
-> [(Register, v)] -> [(SStatePart p, v, Set p)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Register, v) -> Maybe (SStatePart p, v, Set p)
forall {p}. (Register, v) -> Maybe (SStatePart p, v, Set p)
mk_reg ([(Register, v)] -> [(SStatePart p, v, Set p)])
-> [(Register, v)] -> [(SStatePart p, v, Set p)]
forall a b. (a -> b) -> a -> b
$ ((Register, v) -> Bool) -> [(Register, v)] -> [(Register, v)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Register, v) -> Bool
forall {b}. (Register, b) -> Bool
suitable_reg ([(Register, v)] -> [(Register, v)])
-> [(Register, v)] -> [(Register, v)]
forall a b. (a -> b) -> a -> b
$ Map Register v -> [(Register, v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Register v
regs
    mem_to_sps :: Map (p, Maybe ByteSize) v -> [(SStatePart p, v, Set p)]
mem_to_sps  Map (p, Maybe ByteSize) v
mem  = (((p, Maybe ByteSize), v) -> Maybe (SStatePart p, v, Set p))
-> [((p, Maybe ByteSize), v)] -> [(SStatePart p, v, Set p)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((p, Maybe ByteSize), v) -> Maybe (SStatePart p, v, Set p)
mk_mem ([((p, Maybe ByteSize), v)] -> [(SStatePart p, v, Set p)])
-> [((p, Maybe ByteSize), v)] -> [(SStatePart p, v, Set p)]
forall a b. (a -> b) -> a -> b
$ Map (p, Maybe ByteSize) v -> [((p, Maybe ByteSize), v)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (p, Maybe ByteSize) v
mem

    suitable_reg :: (Register, b) -> Bool
suitable_reg (Reg64 GPR
RIP,b
_) = Bool
False
    suitable_reg (Reg64 GPR
RSP,b
_) = Bool
False
    suitable_reg (Reg64 GPR
RBP,b
_) = Bool
False
    suitable_reg (Register, b)
_           = Bool
True

    mk_reg :: (Register, v) -> Maybe (SStatePart p, v, Set p)
mk_reg (Register
r,v
v)
     | Register -> ByteSize
regSize Register
r ByteSize -> ByteSize -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> ByteSize
ByteSize Int
8 Bool -> Bool -> Bool
&& Register
r Register -> Register -> Bool
forall a. Eq a => a -> a -> Bool
/= Register
RegTemp = 
        let ptrs :: Set p
ptrs = ctxt -> String -> v -> Set p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> String -> v -> Set p
smk_mem_addresses ctxt
ctxt String
"finit" v
v in
          if Set p -> Bool
forall a. Set a -> Bool
S.null Set p
ptrs then Maybe (SStatePart p, v, Set p)
forall a. Maybe a
Nothing else (SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p)
forall a. a -> Maybe a
Just ((SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p))
-> (SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p)
forall a b. (a -> b) -> a -> b
$ (Register -> SStatePart p
forall p. Register -> SStatePart p
SSP_Reg Register
r,v
v,Set p
ptrs)
     | Bool
otherwise = Maybe (SStatePart p, v, Set p)
forall a. Maybe a
Nothing

    mk_mem :: ((p, Maybe ByteSize), v) -> Maybe (SStatePart p, v, Set p)
mk_mem ((p
a,Just (ByteSize Int
si)),v
v) =
      case ctxt -> SStatePart p -> v -> Maybe (Set p)
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> SStatePart p -> v -> Maybe (Set p)
skeep_for_finit ctxt
ctxt (p -> Int -> SStatePart p
forall p. p -> Int -> SStatePart p
SSP_Mem p
a Int
si) v
v of
        Maybe (Set p)
Nothing   -> Maybe (SStatePart p, v, Set p)
forall a. Maybe a
Nothing
        Just Set p
ptrs -> (SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p)
forall a. a -> Maybe a
Just ((SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p))
-> (SStatePart p, v, Set p) -> Maybe (SStatePart p, v, Set p)
forall a b. (a -> b) -> a -> b
$ (p -> Int -> SStatePart p
forall p. p -> Int -> SStatePart p
SSP_Mem p
a (Int -> SStatePart p) -> Int -> SStatePart p
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
si,v
v,Set p
ptrs)
    mk_mem ((p, Maybe ByteSize), v)
_ = Maybe (SStatePart p, v, Set p)
forall a. Maybe a
Nothing

    mk_memrel :: ctxt -> ((a, b, t p), (b, b, t p)) -> Maybe ((a, b), MemRelation)
mk_memrel ctxt
ctxt ((a
sp0,b
v0,t p
ptrs0),(b
sp1,b
v1,t p
ptrs1))
    -- TODO separation should be necc here
      | (p -> Bool) -> t p -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\p
ptr0 -> (p -> Bool) -> t p -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\p
ptr1 -> ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> String -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
sseparate ctxt
ctxt String
"invariant_to_finit" p
ptr0 Maybe ByteSize
forall a. Maybe a
unknownSize p
ptr1 Maybe ByteSize
forall a. Maybe a
unknownSize) t p
ptrs1) t p
ptrs0 = ((a, b), MemRelation) -> Maybe ((a, b), MemRelation)
forall a. a -> Maybe a
Just ((a
sp0,b
sp1),MemRelation
Separate)
      | (p -> Bool) -> t p -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\p
ptr0 -> (p -> Bool) -> t p -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\p
ptr1 -> ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> p -> Maybe ByteSize -> p -> Maybe ByteSize -> Bool
salias ctxt
ctxt p
ptr0 Maybe ByteSize
forall a. Maybe a
unknownSize p
ptr1 Maybe ByteSize
forall a. Maybe a
unknownSize) t p
ptrs1) t p
ptrs0 = ((a, b), MemRelation) -> Maybe ((a, b), MemRelation)
forall a. a -> Maybe a
Just ((a
sp0,b
sp1),MemRelation
Aliassing)
      | Bool
otherwise = Maybe ((a, b), MemRelation)
forall a. Maybe a
Nothing

    
    keep_sp :: (SStatePart p, v) -> Bool
keep_sp (sp :: SStatePart p
sp@(SSP_Reg Register
_),v
v)   = ctxt -> SStatePart p -> v -> Maybe (Set p)
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> SStatePart p -> v -> Maybe (Set p)
skeep_for_finit ctxt
ctxt SStatePart p
sp v
v Maybe (Set p) -> Maybe (Set p) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (Set p)
forall a. Maybe a
Nothing
    keep_sp (SSP_Mem p
_ Int
_,v
v)      = Bool
True



-- | The join between two function initialisations
join_finit :: WithAbstractSymbolicValues ctxt v p => ctxt -> (FInit v p) -> (FInit v p) -> (FInit v p)
join_finit :: forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> FInit v p -> FInit v p -> FInit v p
join_finit ctxt
ctxt f0 :: FInit v p
f0@(FInit Set (SStatePart p, v)
sps0 Map (SStatePart p, SStatePart p) MemRelation
m0) f1 :: FInit v p
f1@(FInit Set (SStatePart p, v)
sps1 Map (SStatePart p, SStatePart p) MemRelation
m1)
  | FInit v p
f0 FInit v p -> FInit v p -> Bool
forall a. Eq a => a -> a -> Bool
== FInit v p
f1 = FInit v p
f0
  | Bool
otherwise = Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
forall v p.
Set (SStatePart p, v)
-> Map (SStatePart p, SStatePart p) MemRelation -> FInit v p
FInit (Set (SStatePart p, v)
-> Set (SStatePart p, v) -> Set (SStatePart p, v)
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set (SStatePart p, v)
sps0 Set (SStatePart p, v)
sps1) ((MemRelation -> MemRelation -> MemRelation)
-> Map (SStatePart p, SStatePart p) MemRelation
-> Map (SStatePart p, SStatePart p) MemRelation
-> Map (SStatePart p, SStatePart p) MemRelation
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith MemRelation -> MemRelation -> MemRelation
join_rel Map (SStatePart p, SStatePart p) MemRelation
m0 Map (SStatePart p, SStatePart p) MemRelation
m1)
 where
  join_rel :: MemRelation -> MemRelation -> MemRelation
join_rel MemRelation
r0 MemRelation
r1
    | MemRelation
r0 MemRelation -> MemRelation -> Bool
forall a. Eq a => a -> a -> Bool
== MemRelation
r1  = MemRelation
r0
    | Bool
otherwise = MemRelation
Unknown


pp_finitC :: (Show p, Show v, Ord p) => (FInit v p) -> String
pp_finitC :: forall p v. (Show p, Show v, Ord p) => FInit v p -> String
pp_finitC (FInit Set (SStatePart p, v)
sps Map (SStatePart p, SStatePart p) MemRelation
m) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ([Set (SStatePart p)] -> String)
-> [[Set (SStatePart p)]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map [Set (SStatePart p)] -> String
forall {a}. Show a => [Set a] -> String
show_group ([[SStatePart p]] -> [[Set (SStatePart p)]]
group_separations ([[SStatePart p]] -> [[Set (SStatePart p)]])
-> [[SStatePart p]] -> [[Set (SStatePart p)]]
forall a b. (a -> b) -> a -> b
$ Map (SStatePart p, SStatePart p) MemRelation -> [[SStatePart p]]
forall {a}. Map (SStatePart p, SStatePart p) a -> [[SStatePart p]]
group_aliasses Map (SStatePart p, SStatePart p) MemRelation
m) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (((SStatePart p, v) -> String) -> [(SStatePart p, v)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SStatePart p, v) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
show_sp ([(SStatePart p, v)] -> [String])
-> [(SStatePart p, v)] -> [String]
forall a b. (a -> b) -> a -> b
$ Set (SStatePart p, v) -> [(SStatePart p, v)]
forall a. Set a -> [a]
S.toList Set (SStatePart p, v)
sps)
 where
  group_aliasses :: Map (SStatePart p, SStatePart p) a -> [[SStatePart p]]
group_aliasses Map (SStatePart p, SStatePart p) a
m =
    let sps :: [SStatePart p]
sps          = Set (SStatePart p) -> [SStatePart p]
forall a. Set a -> [a]
S.toList (Set (SStatePart p) -> [SStatePart p])
-> Set (SStatePart p) -> [SStatePart p]
forall a b. (a -> b) -> a -> b
$ [SStatePart p] -> Set (SStatePart p)
forall a. Ord a => [a] -> Set a
S.fromList ([SStatePart p] -> Set (SStatePart p))
-> [SStatePart p] -> Set (SStatePart p)
forall a b. (a -> b) -> a -> b
$ ((SStatePart p, SStatePart p) -> [SStatePart p])
-> [(SStatePart p, SStatePart p)] -> [SStatePart p]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(SStatePart p
sp0,SStatePart p
sp1) -> [SStatePart p
sp0,SStatePart p
sp1]) ([(SStatePart p, SStatePart p)] -> [SStatePart p])
-> [(SStatePart p, SStatePart p)] -> [SStatePart p]
forall a b. (a -> b) -> a -> b
$ Map (SStatePart p, SStatePart p) a
-> [(SStatePart p, SStatePart p)]
forall k a. Map k a -> [k]
M.keys Map (SStatePart p, SStatePart p) a
m
        numbered_sps :: [(Int, SStatePart p)]
numbered_sps = [Int] -> [SStatePart p] -> [(Int, SStatePart p)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [SStatePart p]
sps
        g :: Graph
g            = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Int, IntSet)] -> IntMap IntSet
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, IntSet)] -> IntMap IntSet)
-> [(Int, IntSet)] -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ ((Int, SStatePart p) -> (Int, IntSet))
-> [(Int, SStatePart p)] -> [(Int, IntSet)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
idx,SStatePart p
sp) -> (Int
idx,[Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ MemRelation
-> (Int, SStatePart p) -> [(Int, SStatePart p)] -> [Int]
forall {a}.
Eq a =>
MemRelation -> (a, SStatePart p) -> [(a, SStatePart p)] -> [a]
related_to MemRelation
Aliassing (Int
idx,SStatePart p
sp) [(Int, SStatePart p)]
numbered_sps)) [(Int, SStatePart p)]
numbered_sps
        sccs :: [IntSet]
sccs         = Graph -> IntSet -> [IntSet]
forall g. IntGraph g => g -> IntSet -> [IntSet]
all_sccs Graph
g IntSet
IS.empty
        groups :: [[SStatePart p]]
groups       = (IntSet -> [SStatePart p]) -> [IntSet] -> [[SStatePart p]]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> SStatePart p) -> [Int] -> [SStatePart p]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
idx -> Maybe (SStatePart p) -> SStatePart p
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SStatePart p) -> SStatePart p)
-> Maybe (SStatePart p) -> SStatePart p
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (SStatePart p) -> Maybe (SStatePart p)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
idx (IntMap (SStatePart p) -> Maybe (SStatePart p))
-> IntMap (SStatePart p) -> Maybe (SStatePart p)
forall a b. (a -> b) -> a -> b
$ [(Int, SStatePart p)] -> IntMap (SStatePart p)
forall a. [(Int, a)] -> IntMap a
IM.fromList [(Int, SStatePart p)]
numbered_sps) ([Int] -> [SStatePart p])
-> (IntSet -> [Int]) -> IntSet -> [SStatePart p]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList) [IntSet]
sccs in
      [[SStatePart p]]
groups

  group_separations :: [[SStatePart p]] -> [[Set (SStatePart p)]]
group_separations [[SStatePart p]]
groups =
    let numbered_groups :: [(Int, Set (SStatePart p))]
numbered_groups = [Int] -> [Set (SStatePart p)] -> [(Int, Set (SStatePart p))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Set (SStatePart p)] -> [(Int, Set (SStatePart p))])
-> [Set (SStatePart p)] -> [(Int, Set (SStatePart p))]
forall a b. (a -> b) -> a -> b
$ ([SStatePart p] -> Set (SStatePart p))
-> [[SStatePart p]] -> [Set (SStatePart p)]
forall a b. (a -> b) -> [a] -> [b]
map [SStatePart p] -> Set (SStatePart p)
forall a. Ord a => [a] -> Set a
S.fromList [[SStatePart p]]
groups
        g :: Graph
g               = IntMap IntSet -> Graph
Edges (IntMap IntSet -> Graph) -> IntMap IntSet -> Graph
forall a b. (a -> b) -> a -> b
$ [(Int, IntSet)] -> IntMap IntSet
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, IntSet)] -> IntMap IntSet)
-> [(Int, IntSet)] -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ ((Int, Set (SStatePart p)) -> (Int, IntSet))
-> [(Int, Set (SStatePart p))] -> [(Int, IntSet)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
idx,Set (SStatePart p)
sps) -> (Int
idx,[Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Int, Set (SStatePart p)) -> [(Int, Set (SStatePart p))] -> [Int]
forall {a}.
Eq a =>
(a, Set (SStatePart p)) -> [(a, Set (SStatePart p))] -> [a]
related_to_group (Int
idx,Set (SStatePart p)
sps) [(Int, Set (SStatePart p))]
numbered_groups)) [(Int, Set (SStatePart p))]
numbered_groups
        sccs :: [IntSet]
sccs            = Graph -> IntSet -> [IntSet]
forall g. IntGraph g => g -> IntSet -> [IntSet]
all_sccs Graph
g IntSet
IS.empty
        groups' :: [[Set (SStatePart p)]]
groups'         = (IntSet -> [Set (SStatePart p)])
-> [IntSet] -> [[Set (SStatePart p)]]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Set (SStatePart p)) -> [Int] -> [Set (SStatePart p)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
idx -> Maybe (Set (SStatePart p)) -> Set (SStatePart p)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Set (SStatePart p)) -> Set (SStatePart p))
-> Maybe (Set (SStatePart p)) -> Set (SStatePart p)
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Set (SStatePart p)) -> Maybe (Set (SStatePart p))
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
idx (IntMap (Set (SStatePart p)) -> Maybe (Set (SStatePart p)))
-> IntMap (Set (SStatePart p)) -> Maybe (Set (SStatePart p))
forall a b. (a -> b) -> a -> b
$ [(Int, Set (SStatePart p))] -> IntMap (Set (SStatePart p))
forall a. [(Int, a)] -> IntMap a
IM.fromList [(Int, Set (SStatePart p))]
numbered_groups) ([Int] -> [Set (SStatePart p)])
-> (IntSet -> [Int]) -> IntSet -> [Set (SStatePart p)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList) [IntSet]
sccs in
      [[Set (SStatePart p)]]
groups'

  show_group :: [Set a] -> String
show_group [Set a]
group = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" | " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Set a -> String) -> [Set a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Set a -> String
forall {a}. Show a => Set a -> String
show_aliassing_group [Set a]
group 
  show_aliassing_group :: Set a -> String
show_aliassing_group Set a
group
    | Set a -> Int
forall a. Set a -> Int
S.size Set a
group Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = 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
group
    | Bool
otherwise         = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" aliasses " ([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
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
group) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

  related_to :: MemRelation -> (a, SStatePart p) -> [(a, SStatePart p)] -> [a]
related_to MemRelation
rel (a
idx,SStatePart p
sp) [(a, SStatePart p)]
numbered_sps = ((a, SStatePart p) -> a) -> [(a, SStatePart p)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, SStatePart p) -> a
forall a b. (a, b) -> a
fst ([(a, SStatePart p)] -> [a]) -> [(a, SStatePart p)] -> [a]
forall a b. (a -> b) -> a -> b
$ ((a, SStatePart p) -> Bool)
-> [(a, SStatePart p)] -> [(a, SStatePart p)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
idx',SStatePart p
sp') -> a
idx a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
idx' Bool -> Bool -> Bool
&& MemRelation -> (SStatePart p, SStatePart p) -> Bool
hasRelation MemRelation
rel (SStatePart p
sp,SStatePart p
sp')) [(a, SStatePart p)]
numbered_sps

  related_to_group :: (a, Set (SStatePart p)) -> [(a, Set (SStatePart p))] -> [a]
related_to_group (a
idx,Set (SStatePart p)
sps) [(a, Set (SStatePart p))]
numbered_groups = ((a, Set (SStatePart p)) -> a) -> [(a, Set (SStatePart p))] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Set (SStatePart p)) -> a
forall a b. (a, b) -> a
fst ([(a, Set (SStatePart p))] -> [a])
-> [(a, Set (SStatePart p))] -> [a]
forall a b. (a -> b) -> a -> b
$ ((a, Set (SStatePart p)) -> Bool)
-> [(a, Set (SStatePart p))] -> [(a, Set (SStatePart p))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
idx',Set (SStatePart p)
sps') -> a
idx a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
idx' Bool -> Bool -> Bool
&& ((SStatePart p, SStatePart p) -> Bool)
-> Set (SStatePart p, SStatePart p) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MemRelation -> (SStatePart p, SStatePart p) -> Bool
hasRelation MemRelation
Separate) (Set (SStatePart p)
-> Set (SStatePart p) -> Set (SStatePart p, SStatePart p)
forall a b. Set a -> Set b -> Set (a, b)
S.cartesianProduct Set (SStatePart p)
sps Set (SStatePart p)
sps')) [(a, Set (SStatePart p))]
numbered_groups

  hasRelation :: MemRelation -> (SStatePart p, SStatePart p) -> Bool
hasRelation MemRelation
rel (SStatePart p
sp,SStatePart p
sp') = (SStatePart p, SStatePart p)
-> Map (SStatePart p, SStatePart p) MemRelation
-> Maybe MemRelation
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (SStatePart p
sp,SStatePart p
sp') Map (SStatePart p, SStatePart p) MemRelation
m Maybe MemRelation -> Maybe MemRelation -> Bool
forall a. Eq a => a -> a -> Bool
== MemRelation -> Maybe MemRelation
forall a. a -> Maybe a
Just MemRelation
rel Bool -> Bool -> Bool
|| (SStatePart p, SStatePart p)
-> Map (SStatePart p, SStatePart p) MemRelation
-> Maybe MemRelation
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (SStatePart p
sp',SStatePart p
sp) Map (SStatePart p, SStatePart p) MemRelation
m Maybe MemRelation -> Maybe MemRelation -> Bool
forall a. Eq a => a -> a -> Bool
== MemRelation -> Maybe MemRelation
forall a. a -> Maybe a
Just MemRelation
rel

  show_sp :: (a, a) -> String
show_sp (a
sp,a
v) = a -> String
forall a. Show a => a -> String
show a
sp 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
v