{-# LANGUAGE DeriveGeneric, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances #-}

module WithAbstractSymbolicValues.InstanceOfAbstractPredicates where

import Config

import WithAbstractPredicates.Class

import WithAbstractSymbolicValues.SymbolicExecution
import WithAbstractSymbolicValues.ResolveIndirections
import WithAbstractSymbolicValues.Class
import WithAbstractSymbolicValues.FInit

import Binary.Generic

import Data.L0

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.Word

instance (Show v,Ord v,BinaryClass bin, WithAbstractSymbolicValues (bin, Config, L0 (Sstate v p) (FInit v p) v, Word64) v p) => WithAbstractPredicates bin (Sstate v p) (FInit v p) v where
  symbolically_execute :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (Sstate v p, VCS v) ()
symbolically_execute = LiftingEntry bin (Sstate v p) (FInit v p) v
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (Sstate v p, VCS v) ()
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt
-> Bool
-> [Instruction]
-> Maybe [Instruction]
-> State (Sstate v p, VCS v) ()
sexec_block
  verify_postcondition :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Bool
verify_postcondition = LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Bool
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Sstate v p -> Bool
sverify_postcondition
  finit_to_init_pred :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> FInit v p -> Sstate v p
finit_to_init_pred = LiftingEntry bin (Sstate v p) (FInit v p) v
-> FInit v p -> Sstate v p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> FInit v p -> Sstate v p
finit_to_init_sstate
  pred_to_finit :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> FInit v p
pred_to_finit = LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> FInit v p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Sstate v p -> FInit v p
sstate_to_finit
  resolve_indirection :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> [Instruction] -> Indirections
resolve_indirection = LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> [Instruction] -> Indirections
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> Sstate v p -> [Instruction] -> Indirections
stry_resolve_indirection
  is_weaker_than :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> Sstate v p -> Bool
is_weaker_than = LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> Sstate v p -> Bool
forall {p1} {v} {p2}.
WithAbstractSymbolicValues p1 v p2 =>
p1 -> Sstate v p2 -> Sstate v p2 -> Bool
simplies
  join_preds :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> Sstate v p -> Sstate v p -> Sstate v p
join_preds LiftingEntry bin (Sstate v p) (FInit v p) v
static = LiftingEntry bin (Sstate v p) (FInit v p) v
-> String -> Sstate v p -> Sstate v p -> Sstate v p
forall {p1} {v} {p2}.
WithAbstractSymbolicValues p1 v p2 =>
p1 -> String -> Sstate v p2 -> Sstate v p2 -> Sstate v p2
sjoin_states LiftingEntry bin (Sstate v p) (FInit v p) v
static String
""
  join_finits :: LiftingEntry bin (Sstate v p) (FInit v p) v
-> FInit v p -> FInit v p -> FInit v p
join_finits LiftingEntry bin (Sstate v p) (FInit v p) v
static = LiftingEntry bin (Sstate v p) (FInit v p) v
-> FInit v p -> FInit v p -> FInit v p
forall ctxt v p.
WithAbstractSymbolicValues ctxt v p =>
ctxt -> FInit v p -> FInit v p -> FInit v p
join_finit LiftingEntry bin (Sstate v p) (FInit v p) v
static
  new_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p
new_finit = \Lifting bin (Sstate v p) (FInit v p) v
_ -> 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)
forall a. Set a
S.empty Map (SStatePart p, SStatePart p) MemRelation
forall k a. Map k a
M.empty
  pp_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p -> String
pp_finit = \Lifting bin (Sstate v p) (FInit v p) v
_ -> FInit v p -> String
forall p v. (Show p, Show v, Ord p) => FInit v p -> String
pp_finitC