{- |
Copyright        : (c) Galois, Inc 2015-2017
Maintainer       : Joe Hendrix <jhendrix@galois.com>, Simon Winwood <sjw@galois.com>

This provides a set of functions for abstract evaluation of statements.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Macaw.Discovery.AbsEval
  ( absEvalStmt
--  , absEvalStmts
  , absEvalReadMem
  ) where

import           Control.Lens
import qualified Data.Map.Strict as Map
import           Data.Parameterized.Classes

import           Data.Macaw.AbsDomain.AbsState
import           Data.Macaw.Architecture.Info
import           Data.Macaw.CFG

-- | Get the abstract value associated with an address.
absEvalReadMem :: RegisterInfo (ArchReg a)
               => AbsProcessorState (ArchReg a) ids
               -> ArchAddrValue a ids
               -> MemRepr tp
                  -- ^ Information about the memory layout for the value.
               -> ArchAbsValue a tp
absEvalReadMem :: forall a ids (tp :: Type).
RegisterInfo (ArchReg a) =>
AbsProcessorState (ArchReg a) ids
-> ArchAddrValue a ids -> MemRepr tp -> ArchAbsValue a tp
absEvalReadMem AbsProcessorState (ArchReg a) ids
r ArchAddrValue a ids
a MemRepr tp
tp
    -- If the value is a stack entry, then see if there is a stack
    -- value associated with it.
  | StackOffsetAbsVal MemAddr (ArchAddrWidth a)
_ Int64
o <- AbsProcessorState (ArchReg a) ids
-> ArchAddrValue a ids
-> AbsValue (ArchAddrWidth a) (BVType (ArchAddrWidth a))
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg a) ids
r ArchAddrValue a ids
a
  , Just (StackEntry MemRepr tp
v_tp AbsValue (ArchAddrWidth a) tp
v) <- Int64
-> Map Int64 (StackEntry (ArchAddrWidth a))
-> Maybe (StackEntry (ArchAddrWidth a))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int64
o (AbsProcessorState (ArchReg a) ids
rAbsProcessorState (ArchReg a) ids
-> Getting
     (Map Int64 (StackEntry (ArchAddrWidth a)))
     (AbsProcessorState (ArchReg a) ids)
     (Map Int64 (StackEntry (ArchAddrWidth a)))
-> Map Int64 (StackEntry (ArchAddrWidth a))
forall s a. s -> Getting a s a -> a
^.Getting
  (Map Int64 (StackEntry (ArchAddrWidth a)))
  (AbsProcessorState (ArchReg a) ids)
  (Map Int64 (StackEntry (ArchAddrWidth a)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack)
  , Just tp :~: tp
Refl <- MemRepr tp -> MemRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality MemRepr tp
tp MemRepr tp
v_tp = AbsValue (ArchAddrWidth a) tp
AbsValue (ArchAddrWidth a) tp
v
  | Bool
otherwise = AbsValue (ArchAddrWidth a) tp
forall (w :: Nat) (tp :: Type). AbsValue w tp
TopV

-- | Get the abstract domain for the right-hand side of an assignment.
transferRHS :: ArchitectureInfo a
            -> AbsProcessorState (ArchReg a) ids
            -> AssignRhs a (Value a ids) tp
            -> ArchAbsValue a tp
transferRHS :: forall a ids (tp :: Type).
ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> AssignRhs a (Value a ids) tp
-> ArchAbsValue a tp
transferRHS ArchitectureInfo a
info AbsProcessorState (ArchReg a) ids
r AssignRhs a (Value a ids) tp
rhs =
  case AssignRhs a (Value a ids) tp
rhs of
    EvalApp App (Value a ids) tp
app    -> ArchitectureInfo a -> forall a. (ArchConstraints a => a) -> a
forall arch.
ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
withArchConstraints ArchitectureInfo a
info ((ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp)
-> (ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp
forall a b. (a -> b) -> a -> b
$ AbsProcessorState (ArchReg a) ids
-> App (Value a ids) tp -> ArchAbsValue a tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> App (Value a ids) tp -> ArchAbsValue a tp
transferApp AbsProcessorState (ArchReg a) ids
r App (Value a ids) tp
app
    SetUndefined TypeRepr tp
_ -> ArchAbsValue a tp
forall (w :: Nat) (tp :: Type). AbsValue w tp
TopV
    ReadMem Value a ids (BVType (ArchAddrWidth a))
a MemRepr tp
tp   -> ArchitectureInfo a -> forall a. (ArchConstraints a => a) -> a
forall arch.
ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
withArchConstraints ArchitectureInfo a
info ((ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp)
-> (ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp
forall a b. (a -> b) -> a -> b
$ AbsProcessorState (ArchReg a) ids
-> Value a ids (BVType (ArchAddrWidth a))
-> MemRepr tp
-> ArchAbsValue a tp
forall a ids (tp :: Type).
RegisterInfo (ArchReg a) =>
AbsProcessorState (ArchReg a) ids
-> ArchAddrValue a ids -> MemRepr tp -> ArchAbsValue a tp
absEvalReadMem AbsProcessorState (ArchReg a) ids
r Value a ids (BVType (ArchAddrWidth a))
a MemRepr tp
tp

    -- TODO: See if we should build a mux specific version
    CondReadMem MemRepr tp
tp Value a ids BoolType
_ Value a ids (BVType (ArchAddrWidth a))
a Value a ids tp
d ->
      ArchitectureInfo a -> forall a. (ArchConstraints a => a) -> a
forall arch.
ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
withArchConstraints ArchitectureInfo a
info ((ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp)
-> (ArchConstraints a => ArchAbsValue a tp) -> ArchAbsValue a tp
forall a b. (a -> b) -> a -> b
$ do
        ArchAbsValue a tp -> ArchAbsValue a tp -> ArchAbsValue a tp
forall d. AbsDomain d => d -> d -> d
lub (AbsProcessorState (ArchReg a) ids
-> Value a ids (BVType (ArchAddrWidth a))
-> MemRepr tp
-> ArchAbsValue a tp
forall a ids (tp :: Type).
RegisterInfo (ArchReg a) =>
AbsProcessorState (ArchReg a) ids
-> ArchAddrValue a ids -> MemRepr tp -> ArchAbsValue a tp
absEvalReadMem AbsProcessorState (ArchReg a) ids
r Value a ids (BVType (ArchAddrWidth a))
a MemRepr tp
tp)
            (AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg a) ids
r Value a ids tp
d)
    EvalArchFn ArchFn a (Value a ids) tp
f TypeRepr tp
_ -> ArchitectureInfo a
-> forall ids (tp :: Type).
   AbsProcessorState (ArchReg a) ids
   -> ArchFn a (Value a ids) tp -> AbsValue (ArchAddrWidth a) tp
forall arch.
ArchitectureInfo arch
-> forall ids (tp :: Type).
   AbsProcessorState (ArchReg arch) ids
   -> ArchFn arch (Value arch ids) tp
   -> AbsValue (ArchAddrWidth arch) tp
absEvalArchFn ArchitectureInfo a
info AbsProcessorState (ArchReg a) ids
r ArchFn a (Value a ids) tp
f

-- | Merge in the value of the assignment.
--
-- If we have already seen a value, this will combine with meet.
addAssignment :: ArchitectureInfo a
              -> AbsProcessorState (ArchReg a) ids
              -> Assignment a ids tp
              -> AbsProcessorState (ArchReg a) ids
addAssignment :: forall a ids (tp :: Type).
ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> Assignment a ids tp
-> AbsProcessorState (ArchReg a) ids
addAssignment ArchitectureInfo a
info AbsProcessorState (ArchReg a) ids
s Assignment a ids tp
a = ArchitectureInfo a -> forall a. (ArchConstraints a => a) -> a
forall arch.
ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
withArchConstraints ArchitectureInfo a
info ((ArchConstraints a => AbsProcessorState (ArchReg a) ids)
 -> AbsProcessorState (ArchReg a) ids)
-> (ArchConstraints a => AbsProcessorState (ArchReg a) ids)
-> AbsProcessorState (ArchReg a) ids
forall a b. (a -> b) -> a -> b
$
  AbsProcessorState (ArchReg a) ids
s AbsProcessorState (ArchReg a) ids
-> (AbsProcessorState (ArchReg a) ids
    -> AbsProcessorState (ArchReg a) ids)
-> AbsProcessorState (ArchReg a) ids
forall a b. a -> (a -> b) -> b
& ((MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))
 -> Identity
      (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))))
-> AbsProcessorState (ArchReg a) ids
-> Identity (AbsProcessorState (ArchReg a) ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(MapF (AssignId ids) (AbsValue (RegAddrWidth r))
 -> f (MapF (AssignId ids) (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absAssignments ((MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))
  -> Identity
       (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))))
 -> AbsProcessorState (ArchReg a) ids
 -> Identity (AbsProcessorState (ArchReg a) ids))
-> ((AbsValue (RegAddrWidth (ArchReg a)) tp
     -> Identity (AbsValue (RegAddrWidth (ArchReg a)) tp))
    -> MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))
    -> Identity
         (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))))
-> (AbsValue (RegAddrWidth (ArchReg a)) tp
    -> Identity (AbsValue (RegAddrWidth (ArchReg a)) tp))
-> AbsProcessorState (ArchReg a) ids
-> Identity (AbsProcessorState (ArchReg a) ids)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AssignId ids tp
-> Lens'
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a))))
     (AbsValue (RegAddrWidth (ArchReg a)) tp)
forall ids (tp :: Type) (w :: Nat).
AssignId ids tp
-> Lens' (MapF (AssignId ids) (AbsValue w)) (AbsValue w tp)
assignLens (Assignment a ids tp -> AssignId ids tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment a ids tp
a))
    ((AbsValue (RegAddrWidth (ArchReg a)) tp
  -> Identity (AbsValue (RegAddrWidth (ArchReg a)) tp))
 -> AbsProcessorState (ArchReg a) ids
 -> Identity (AbsProcessorState (ArchReg a) ids))
-> (AbsValue (RegAddrWidth (ArchReg a)) tp
    -> AbsValue (RegAddrWidth (ArchReg a)) tp)
-> AbsProcessorState (ArchReg a) ids
-> AbsProcessorState (ArchReg a) ids
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (AbsValue (RegAddrWidth (ArchReg a)) tp
-> AbsValue (RegAddrWidth (ArchReg a)) tp
-> AbsValue (RegAddrWidth (ArchReg a)) tp
forall (w :: Nat) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
`meet` ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> AssignRhs a (Value a ids) tp
-> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a ids (tp :: Type).
ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> AssignRhs a (Value a ids) tp
-> ArchAbsValue a tp
transferRHS ArchitectureInfo a
info AbsProcessorState (ArchReg a) ids
s (Assignment a ids tp -> AssignRhs a (Value a ids) tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs Assignment a ids tp
a))

-- | Given a statement this modifies the processor state based on the statement.
absEvalStmt :: ArchitectureInfo arch
            -> AbsProcessorState (ArchReg arch) ids
            -> Stmt arch ids
            -> AbsProcessorState (ArchReg arch) ids
absEvalStmt :: forall arch ids.
ArchitectureInfo arch
-> AbsProcessorState (ArchReg arch) ids
-> Stmt arch ids
-> AbsProcessorState (ArchReg arch) ids
absEvalStmt ArchitectureInfo arch
info AbsProcessorState (ArchReg arch) ids
s Stmt arch ids
stmt = ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
forall arch.
ArchitectureInfo arch -> forall a. (ArchConstraints arch => a) -> a
withArchConstraints ArchitectureInfo arch
info ((ArchConstraints arch => AbsProcessorState (ArchReg arch) ids)
 -> AbsProcessorState (ArchReg arch) ids)
-> (ArchConstraints arch => AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
forall a b. (a -> b) -> a -> b
$
  case Stmt arch ids
stmt of
    AssignStmt Assignment arch ids tp
a ->
      ArchitectureInfo arch
-> AbsProcessorState (ArchReg arch) ids
-> Assignment arch ids tp
-> AbsProcessorState (ArchReg arch) ids
forall a ids (tp :: Type).
ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> Assignment a ids tp
-> AbsProcessorState (ArchReg a) ids
addAssignment ArchitectureInfo arch
info AbsProcessorState (ArchReg arch) ids
s Assignment arch ids tp
a
    WriteMem ArchAddrValue arch ids
addr MemRepr tp
memRepr Value arch ids tp
v -> do
      AbsProcessorState (ArchReg arch) ids
-> ArchAddrValue arch ids
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
(RegisterInfo (ArchReg arch), MemWidth (ArchAddrWidth arch),
 HasCallStack) =>
AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType (ArchAddrWidth arch))
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState (ArchReg arch) ids
addMemWrite AbsProcessorState (ArchReg arch) ids
s ArchAddrValue arch ids
addr MemRepr tp
memRepr Value arch ids tp
v
    CondWriteMem Value arch ids BoolType
cond ArchAddrValue arch ids
addr MemRepr tp
memRepr Value arch ids tp
v ->
      AbsProcessorState (ArchReg arch) ids
-> Value arch ids BoolType
-> ArchAddrValue arch ids
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState (ArchReg arch) ids
forall (r :: Type -> Type) arch ids (tp :: Type).
(RegisterInfo r, MemWidth (RegAddrWidth r), HasCallStack,
 r ~ ArchReg arch) =>
AbsProcessorState r ids
-> Value arch ids BoolType
-> Value arch ids (BVType (RegAddrWidth r))
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState r ids
addCondMemWrite AbsProcessorState (ArchReg arch) ids
s Value arch ids BoolType
cond ArchAddrValue arch ids
addr MemRepr tp
memRepr Value arch ids tp
v
    InstructionStart ArchAddrWord arch
_ Text
_ ->
      AbsProcessorState (ArchReg arch) ids
s
    Comment{} ->
      AbsProcessorState (ArchReg arch) ids
s
    ExecArchStmt ArchStmt arch (Value arch ids)
astmt ->
      ArchitectureInfo arch
-> forall ids.
   AbsProcessorState (ArchReg arch) ids
   -> ArchStmt arch (Value arch ids)
   -> AbsProcessorState (ArchReg arch) ids
forall arch.
ArchitectureInfo arch
-> forall ids.
   AbsProcessorState (ArchReg arch) ids
   -> ArchStmt arch (Value arch ids)
   -> AbsProcessorState (ArchReg arch) ids
absEvalArchStmt ArchitectureInfo arch
info AbsProcessorState (ArchReg arch) ids
s ArchStmt arch (Value arch ids)
astmt
    ArchState{} ->
      AbsProcessorState (ArchReg arch) ids
s

{-
-- This takes a processor state and updates it based on executing each statement.
absEvalStmts :: Foldable t
             => ArchitectureInfo arch
             -> AbsProcessorState (ArchReg arch) ids
             -> t (Stmt arch ids)
             -> AbsProcessorState (ArchReg arch) ids
absEvalStmts info = foldl' (absEvalStmt info)
-}