-- | A simple domain for tracking even-ness and odd-ness of values
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
module EvenOdd (
  EvenOdd(..), EOExt,
  evenOddDom,
  evenOddInterp
  ) where

import qualified Data.Parameterized.Context as PU

import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.CFG.Expr as C
import Lang.Crucible.Analysis.Fixpoint

data EvenOdd (tp :: C.CrucibleType) where
  Even :: EvenOdd tp
  Odd :: EvenOdd tp

deriving instance Eq (EvenOdd tp)
deriving instance Show (EvenOdd tp)

instance C.ShowF EvenOdd

type EvenOdd' = Pointed EvenOdd

evenOddDom :: Domain EvenOdd'
evenOddDom = pointed j (==) WTO
  where
    j Even Odd = Top
    j Odd Even = Top
    j Even Even = Pointed Even
    j Odd Odd = Pointed Odd

type EOExt = ()

evenOddInterp :: Interpretation EOExt EvenOdd'
evenOddInterp = Interpretation { interpExpr = eoIExpr
                               , interpExt = undefined
                               , interpCall = eoICall
                               , interpReadGlobal = eoIRdGlobal
                               , interpWriteGlobal = eoIWrGlobal
                               , interpBr = eoIBr
                               , interpMaybe = eoIMaybe
                               }

eoIExpr :: ScopedReg
        -> C.TypeRepr tp
        -> C.Expr ext ctx tp
        -> PointAbstraction blocks EvenOdd' ctx
        -> (Maybe (PointAbstraction blocks EvenOdd' ctx), EvenOdd' tp)
eoIExpr _sr _tr (C.App e) abstr =
  case e of
    C.IntLit i -> (Nothing, if i `mod` 2 == 0 then Pointed Even else Pointed Odd)
    C.IntAdd r1 r2 ->
      let a1 = lookupAbstractRegValue abstr r1
          a2 = lookupAbstractRegValue abstr r2
      in case (a1, a2) of
        (Pointed Even, Pointed Even) -> (Nothing, Pointed Even)
        (Pointed Odd, Pointed Odd) -> (Nothing, Pointed Even)
        (Pointed Even, Pointed Odd) -> (Nothing, Pointed Odd)
        (Pointed Odd, Pointed Even) -> (Nothing, Pointed Odd)
        _ -> (Nothing, Top)
    _ -> (Nothing, Top)

eoICall :: C.CtxRepr args
        -> C.TypeRepr ret
        -> C.Reg ctx (C.FunctionHandleType args ret)
        -> EvenOdd' (C.FunctionHandleType args ret)
        -> PU.Assignment EvenOdd' args
        -> PointAbstraction blocks dom ctx
        -> (Maybe (PointAbstraction blocks EvenOdd' ctx), EvenOdd' ret)
eoICall _ _ _ _ _ _ = (Nothing, Top)

eoIBr :: C.Reg ctx C.BoolType
      -> EvenOdd' C.BoolType
      -> C.JumpTarget blocks ctx
      -> C.JumpTarget blocks ctx
      -> PointAbstraction blocks EvenOdd' ctx
      -> (Maybe (PointAbstraction blocks EvenOdd' ctx), Maybe (PointAbstraction blocks EvenOdd' ctx))
eoIBr _ _ _ _ _ = (Nothing, Nothing)

eoIMaybe :: C.TypeRepr tp
         -> C.Reg ctx (C.MaybeType tp)
         -> EvenOdd' (C.MaybeType tp)
         -> PointAbstraction blocks EvenOdd' ctx
         -> (Maybe (PointAbstraction blocks EvenOdd' ctx), EvenOdd' tp, Maybe (PointAbstraction blocks EvenOdd' ctx))
eoIMaybe _ _ _ _ = (Nothing, Top, Nothing)

eoIWrGlobal :: C.GlobalVar tp -> C.Reg ctx tp -> PointAbstraction blocks EvenOdd' ctx -> Maybe (PointAbstraction blocks EvenOdd' ctx)
eoIWrGlobal _ _ _ = Nothing

eoIRdGlobal :: C.GlobalVar tp -> PointAbstraction blocks EvenOdd' ctx -> (Maybe (PointAbstraction blocks EvenOdd' ctx), EvenOdd' tp)
eoIRdGlobal _ _ = (Nothing, Top)