{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Crux.Overrides
  ( mkFresh
  , mkFreshFloat
  , baseFreshOverride
  , baseFreshOverride'
  ) where

import qualified Data.Parameterized.Context as Ctx

import What4.BaseTypes (BaseTypeRepr)
import qualified What4.Interface as W4
import qualified What4.InterpretedFloatingPoint as W4

import qualified Lang.Crucible.Backend as C
import qualified Lang.Crucible.Simulator.RegValue as C
import qualified Lang.Crucible.Types as C
import qualified Lang.Crucible.Simulator.OverrideSim as C

import Crux.Types (OverM)
import Control.Monad.IO.Class (liftIO)

-- | Create a fresh constant ('W4.freshConstant') with the given base type
mkFresh ::
  C.IsSymInterface sym =>
  W4.SolverSymbol ->
  BaseTypeRepr ty ->
  OverM personality sym ext (C.RegValue sym (C.BaseToType ty))
mkFresh :: forall sym (ty :: BaseType) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr ty
-> OverM personality sym ext (RegValue sym (BaseToType ty))
mkFresh SolverSymbol
name BaseTypeRepr ty
ty =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (RegValue sym (BaseToType ty)))
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym (BaseToType ty))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       (personality sym)
       sym
       ext
       r
       args
       ret
       (RegValue sym (BaseToType ty)))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (RegValue sym (BaseToType ty)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         (personality sym)
         sym
         ext
         r
         args
         ret
         (RegValue sym (BaseToType ty)))
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym (BaseToType ty))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak
       SymExpr sym ty
elt <- IO (SymExpr sym ty)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym ty)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SolverSymbol -> BaseTypeRepr ty -> IO (SymExpr sym ty)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym SolverSymbol
name BaseTypeRepr ty
ty)
       ProgramLoc
loc <- IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> OverrideSim (personality sym) sym ext r args ret ProgramLoc)
-> IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
       let ev :: CrucibleEvent (SymExpr sym)
ev = ProgramLoc
-> String
-> BaseTypeRepr ty
-> SymExpr sym ty
-> CrucibleEvent (SymExpr sym)
forall (tp :: BaseType) (e :: BaseType -> *).
ProgramLoc -> String -> BaseTypeRepr tp -> e tp -> CrucibleEvent e
C.CreateVariableEvent ProgramLoc
loc (SolverSymbol -> String
forall a. Show a => a -> String
show SolverSymbol
name) BaseTypeRepr ty
ty SymExpr sym ty
elt
       IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ bak -> Assumptions sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumptions sym -> IO ()
C.addAssumptions bak
bak (CrucibleEvent (SymExpr sym) -> Assumptions sym
forall (e :: BaseType -> *).
CrucibleEvent e -> CrucibleAssumptions e
C.singleEvent CrucibleEvent (SymExpr sym)
ev)
       SymExpr sym ty
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym ty)
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym ty
elt

-- | Create a fresh float constant ('W4.freshFloatConstant')
mkFreshFloat ::
  C.IsSymInterface sym =>
  W4.SolverSymbol ->
  C.FloatInfoRepr fi ->
  OverM personality sym ext (C.RegValue sym (C.FloatType fi))
mkFreshFloat :: forall sym (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> FloatInfoRepr fi
-> OverM personality sym ext (RegValue sym (FloatType fi))
mkFreshFloat SolverSymbol
name FloatInfoRepr fi
fi =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      (personality sym) sym ext r args ret (RegValue sym (FloatType fi)))
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym (FloatType fi))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       (personality sym) sym ext r args ret (RegValue sym (FloatType fi)))
 -> OverrideSim
      (personality sym) sym ext r args ret (RegValue sym (FloatType fi)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         (personality sym) sym ext r args ret (RegValue sym (FloatType fi)))
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym (FloatType fi))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak
       SymExpr sym (SymInterpretedFloatType sym fi)
elt <- IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (SymInterpretedFloatType sym fi))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (fi :: FloatInfo).
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
W4.freshFloatConstant sym
sym SolverSymbol
name FloatInfoRepr fi
fi
       ProgramLoc
loc <- IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> OverrideSim (personality sym) sym ext r args ret ProgramLoc)
-> IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
       let ev :: CrucibleEvent (SymExpr sym)
ev = ProgramLoc
-> String
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
-> SymExpr sym (SymInterpretedFloatType sym fi)
-> CrucibleEvent (SymExpr sym)
forall (tp :: BaseType) (e :: BaseType -> *).
ProgramLoc -> String -> BaseTypeRepr tp -> e tp -> CrucibleEvent e
C.CreateVariableEvent ProgramLoc
loc (SolverSymbol -> String
forall a. Show a => a -> String
show SolverSymbol
name) (sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
W4.iFloatBaseTypeRepr sym
sym FloatInfoRepr fi
fi) SymExpr sym (SymInterpretedFloatType sym fi)
elt
       IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ bak -> Assumptions sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumptions sym -> IO ()
C.addAssumptions bak
bak (CrucibleEvent (SymExpr sym) -> Assumptions sym
forall (e :: BaseType -> *).
CrucibleEvent e -> CrucibleAssumptions e
C.singleEvent CrucibleEvent (SymExpr sym)
ev)
       SymExpr sym (SymInterpretedFloatType sym fi)
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym (SymInterpretedFloatType sym fi)
elt

-- | Build an override that takes a string and returns a fresh constant with
-- that string as its name.
baseFreshOverride :: 
  C.IsSymInterface sym =>
  W4.BaseTypeRepr bty ->
  -- | The language's string type (e.g., @LLVMPointerType@ for LLVM)
  C.TypeRepr stringTy ->
  -- | Get the variable name as a concrete string from the override arguments
  (C.RegValue' sym stringTy -> OverM p sym ext W4.SolverSymbol) ->
  C.TypedOverride (p sym) sym ext (C.EmptyCtx C.::> stringTy) (C.BaseToType bty)
baseFreshOverride :: forall sym (bty :: BaseType) (stringTy :: CrucibleType)
       (p :: * -> *) ext.
IsSymInterface sym =>
BaseTypeRepr bty
-> TypeRepr stringTy
-> (RegValue' sym stringTy -> OverM p sym ext SolverSymbol)
-> TypedOverride
     (p sym) sym ext (EmptyCtx ::> stringTy) (BaseToType bty)
baseFreshOverride BaseTypeRepr bty
bty TypeRepr stringTy
sty RegValue' sym stringTy -> OverM p sym ext SolverSymbol
getStr =
  C.TypedOverride
  { typedOverrideHandler :: forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
Assignment (RegValue' sym) (EmptyCtx ::> stringTy)
-> OverrideSim
     (p sym) sym ext rtp args' ret' (RegValue sym (BaseToType bty))
C.typedOverrideHandler = \(Assignment (RegValue' sym) ctx
Ctx.Empty Ctx.:> RegValue' sym tp
strVal) -> do
      SolverSymbol
str <- RegValue' sym stringTy -> OverM p sym ext SolverSymbol
getStr RegValue' sym stringTy
RegValue' sym tp
strVal
      SolverSymbol
-> BaseTypeRepr bty
-> OverM p sym ext (RegValue sym (BaseToType bty))
forall sym (ty :: BaseType) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr ty
-> OverM personality sym ext (RegValue sym (BaseToType ty))
mkFresh SolverSymbol
str BaseTypeRepr bty
bty
  , typedOverrideArgs :: CtxRepr (EmptyCtx ::> stringTy)
C.typedOverrideArgs = Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment TypeRepr EmptyCtx
-> TypeRepr stringTy -> CtxRepr (EmptyCtx ::> stringTy)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr stringTy
sty
  , typedOverrideRet :: TypeRepr (BaseToType bty)
C.typedOverrideRet = BaseTypeRepr bty -> TypeRepr (BaseToType bty)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
C.baseToType BaseTypeRepr bty
bty
  }

-- | Build an override that takes no arguments and returns a fresh
-- constant that uses the given name. Generally, frontends should prefer
-- 'baseFreshOverride', to allow users to specify variable names.
baseFreshOverride' :: 
  C.IsSymInterface sym =>
  -- | Variable name
  W4.SolverSymbol ->
  W4.BaseTypeRepr bty ->
  C.TypedOverride (p sym) sym ext C.EmptyCtx (C.BaseToType bty)
baseFreshOverride' :: forall sym (bty :: BaseType) (p :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr bty
-> TypedOverride (p sym) sym ext EmptyCtx (BaseToType bty)
baseFreshOverride' SolverSymbol
nm BaseTypeRepr bty
bty =
  C.TypedOverride
  { typedOverrideHandler :: forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
Assignment (RegValue' sym) EmptyCtx
-> OverrideSim
     (p sym) sym ext rtp args' ret' (RegValue sym (BaseToType bty))
C.typedOverrideHandler = \Assignment (RegValue' sym) EmptyCtx
Ctx.Empty -> SolverSymbol
-> BaseTypeRepr bty
-> OverM p sym ext (RegValue sym (BaseToType bty))
forall sym (ty :: BaseType) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr ty
-> OverM personality sym ext (RegValue sym (BaseToType ty))
mkFresh SolverSymbol
nm BaseTypeRepr bty
bty
  , typedOverrideArgs :: Assignment TypeRepr EmptyCtx
C.typedOverrideArgs = Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
  , typedOverrideRet :: TypeRepr (BaseToType bty)
C.typedOverrideRet = BaseTypeRepr bty -> TypeRepr (BaseToType bty)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
C.baseToType BaseTypeRepr bty
bty
  }