{-|
Module     : Data.Macaw.AbsDomain.Refine
Copyright  : (c) Galois, Inc 2016
Maintainer : jhendrix@galois.com

This defines operations that use assertions to refine state.
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Macaw.AbsDomain.Refine
  ( RefineConstraints
  , refineProcState
  ) where


import           Control.Lens
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr

import           Data.Macaw.AbsDomain.AbsState
import           Data.Macaw.CFG
import           Data.Macaw.Types

-- | Constraints needed for refinement on abstract states.
type RefineConstraints arch
   = ( RegisterInfo (ArchReg arch)
--     , ShowF (ArchReg arch)
--     , HasRepr (ArchReg arch) TypeRepr
--     , MemWidth (ArchAddrWidth arch)
     )

-- | @refineValue v av s@ records an assertion that the value @v@ must
-- be in the domain @av@, and updates abstract domain information in
-- the processor state @s@ accordingly.
refineValue :: RefineConstraints arch
                => Value arch ids tp -- ^ Value in processor state
                -> AbsValue (ArchAddrWidth arch) tp -- ^ Abstract value to assign value.
                -> AbsProcessorState (ArchReg arch) ids
                -> AbsProcessorState (ArchReg arch) ids
refineValue :: forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue (BoolValue Bool
_) AbsValue (RegAddrWidth (ArchReg arch)) tp
_av AbsProcessorState (ArchReg arch) ids
regs          = AbsProcessorState (ArchReg arch) ids
regs -- Skip refinement for literal values
refineValue (BVValue NatRepr n
_n Integer
_val) AbsValue (RegAddrWidth (ArchReg arch)) tp
_av AbsProcessorState (ArchReg arch) ids
regs      = AbsProcessorState (ArchReg arch) ids
regs -- Skip refinement for literal values
refineValue (RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
_ MemAddr (RegAddrWidth (ArchReg arch))
_) AbsValue (RegAddrWidth (ArchReg arch)) tp
_av AbsProcessorState (ArchReg arch) ids
regs = AbsProcessorState (ArchReg arch) ids
regs -- Skip refinement for relocatable values
refineValue (SymbolValue AddrWidthRepr (RegAddrWidth (ArchReg arch))
_ SymbolIdentifier
_)      AbsValue (RegAddrWidth (ArchReg arch)) tp
_av AbsProcessorState (ArchReg arch) ids
regs = AbsProcessorState (ArchReg arch) ids
regs -- Skip refinement for this case.
refineValue (Initial ArchReg arch tp
r) AbsValue (RegAddrWidth (ArchReg arch)) tp
av AbsProcessorState (ArchReg arch) ids
regs =
  AbsProcessorState (ArchReg arch) ids
regs AbsProcessorState (ArchReg arch) ids
-> (AbsProcessorState (ArchReg arch) ids
    -> AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
forall a b. a -> (a -> b) -> b
& ((RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))
 -> Identity
      (RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegs ((RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))
  -> Identity
       (RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> ((AbsValue (RegAddrWidth (ArchReg arch)) tp
     -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
    -> RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))
    -> Identity
         (RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))))
-> (AbsValue (RegAddrWidth (ArchReg arch)) tp
    -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) ids)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArchReg arch tp
-> Lens'
     (RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch))))
     (AbsValue (RegAddrWidth (ArchReg arch)) tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue ArchReg arch tp
r) ((AbsValue (RegAddrWidth (ArchReg arch)) tp
  -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> (AbsValue (RegAddrWidth (ArchReg arch)) tp
    -> AbsValue (RegAddrWidth (ArchReg arch)) tp)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (AbsValue (RegAddrWidth (ArchReg arch)) tp
 -> AbsValue (RegAddrWidth (ArchReg arch)) tp
 -> AbsValue (RegAddrWidth (ArchReg arch)) tp)
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall a b c. (a -> b -> c) -> b -> a -> c
flip AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue (RegAddrWidth (ArchReg arch)) tp
av
refineValue (AssignedValue (Assignment AssignId ids tp
a_id AssignRhs arch (Value arch ids) tp
rhs)) AbsValue (RegAddrWidth (ArchReg arch)) tp
av AbsProcessorState (ArchReg arch) ids
regs
  -- av is not a subset.
  | Maybe (AbsValue (RegAddrWidth (ArchReg arch)) tp)
Nothing <- AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> Maybe (AbsValue (RegAddrWidth (ArchReg arch)) tp)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> Maybe (AbsValue w tp)
joinAbsValue AbsValue (RegAddrWidth (ArchReg arch)) tp
av AbsValue (RegAddrWidth (ArchReg arch)) tp
av_old = AbsProcessorState (ArchReg arch) ids
regs
  | Bool
otherwise = do
    -- Get joined abstract value.
    let av' :: AbsValue (RegAddrWidth (ArchReg arch)) tp
av'    = AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue (RegAddrWidth (ArchReg arch)) tp
av_old AbsValue (RegAddrWidth (ArchReg arch)) tp
av
    -- Get registers after updating assignment value to av'
    let  regs' :: AbsProcessorState (ArchReg arch) ids
regs'  = AbsProcessorState (ArchReg arch) ids
regs AbsProcessorState (ArchReg arch) ids
-> (AbsProcessorState (ArchReg arch) ids
    -> AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
forall a b. a -> (a -> b) -> b
& ((MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))
 -> Identity
      (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) 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 arch)))
  -> Identity
       (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> ((AbsValue (RegAddrWidth (ArchReg arch)) tp
     -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
    -> MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))
    -> Identity
         (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))))
-> (AbsValue (RegAddrWidth (ArchReg arch)) tp
    -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) ids)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AssignId ids tp
-> Lens'
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
     (AbsValue (RegAddrWidth (ArchReg arch)) tp)
forall ids (tp :: Type) (w :: Natural).
AssignId ids tp
-> Lens' (MapF (AssignId ids) (AbsValue w)) (AbsValue w tp)
assignLens AssignId ids tp
a_id) ((AbsValue (RegAddrWidth (ArchReg arch)) tp
  -> Identity (AbsValue (RegAddrWidth (ArchReg arch)) tp))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AbsValue (RegAddrWidth (ArchReg arch)) tp
av'
    case AssignRhs arch (Value arch ids) tp
rhs of
      -- av adds new information, we need to refine any parents
      EvalApp App (Value arch ids) tp
app -> App (Value arch ids) tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
App (Value arch ids) tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineApp App (Value arch ids) tp
app AbsValue (RegAddrWidth (ArchReg arch)) tp
av' AbsProcessorState (ArchReg arch) ids
regs'
      -- no parents, but update ass
      AssignRhs arch (Value arch ids) tp
_ -> AbsProcessorState (ArchReg arch) ids
regs'
  where
    av_old :: AbsValue (RegAddrWidth (ArchReg arch)) tp
av_old = AbsProcessorState (ArchReg arch) ids
regs AbsProcessorState (ArchReg arch) ids
-> Getting
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
     (AbsProcessorState (ArchReg arch) ids)
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
-> MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch)))
forall s a. s -> Getting a s a -> a
^. Getting
  (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
  (AbsProcessorState (ArchReg arch) ids)
  (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
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 arch)))
-> Getting
     (AbsValue (RegAddrWidth (ArchReg arch)) tp)
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
     (AbsValue (RegAddrWidth (ArchReg arch)) tp)
-> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall s a. s -> Getting a s a -> a
^. AssignId ids tp
-> Lens'
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg arch))))
     (AbsValue (RegAddrWidth (ArchReg arch)) tp)
forall ids (tp :: Type) (w :: Natural).
AssignId ids tp
-> Lens' (MapF (AssignId ids) (AbsValue w)) (AbsValue w tp)
assignLens AssignId ids tp
a_id

refineApp :: RefineConstraints arch
          => App (Value arch ids) tp
          -> AbsValue (ArchAddrWidth arch) tp
          -> AbsProcessorState (ArchReg arch) ids
          -> AbsProcessorState (ArchReg arch) ids
refineApp :: forall arch ids (tp :: Type).
RefineConstraints arch =>
App (Value arch ids) tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineApp App (Value arch ids) tp
app AbsValue (RegAddrWidth (ArchReg arch)) tp
av AbsProcessorState (ArchReg arch) ids
regs =
  case App (Value arch ids) tp
app of

   -- If we know something about the result of a trunc, we can
   -- propagate back a subvalue.
   Trunc Value arch ids (BVType m)
x NatRepr n
sz -> Value arch ids (BVType m)
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg arch)) ('BVType n)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall (n :: Natural) (n' :: Natural) arch ids.
((n + 1) <= n', RefineConstraints arch) =>
BVValue arch ids n'
-> NatRepr n
-> AbsValue (ArchAddrWidth arch) (BVType n)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineTrunc Value arch ids (BVType m)
x NatRepr n
sz AbsValue (RegAddrWidth (ArchReg arch)) tp
AbsValue (RegAddrWidth (ArchReg arch)) ('BVType n)
av AbsProcessorState (ArchReg arch) ids
regs

   -- Assertion "r <= x"
   BVUnsignedLt Value arch ids (BVType n)
l Value arch ids (BVType n)
r
     | Just Integer
b    <- AbsValue (RegAddrWidth (ArchReg arch)) tp -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton AbsValue (RegAddrWidth (ArchReg arch)) tp
av -> Value arch ids (BVType n)
-> Value arch ids (BVType n)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLt Value arch ids (BVType n)
l Value arch ids (BVType n)
r Integer
b AbsProcessorState (ArchReg arch) ids
regs

   BVUnsignedLe Value arch ids (BVType n)
l Value arch ids (BVType n)
r
     | Just Integer
b    <- AbsValue (RegAddrWidth (ArchReg arch)) tp -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton AbsValue (RegAddrWidth (ArchReg arch)) tp
av -> Value arch ids (BVType n)
-> Value arch ids (BVType n)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLeq Value arch ids (BVType n)
l Value arch ids (BVType n)
r Integer
b AbsProcessorState (ArchReg arch) ids
regs

   -- FIXME: HACK
   -- This detects r - x < 0 || r - x == 0, i.e. r <= x
   OrApp (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (UsbbOverflows Value arch ids (BVType n)
r xv :: Value arch ids (BVType n)
xv@(BVValue NatRepr n
sz Integer
x) (BoolValue Bool
False)))
         (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (Eq (Value arch ids tp1 -> Maybe (App (Value arch ids) tp1)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (BVAdd NatRepr n
_ Value arch ids ('BVType n)
r' Value arch ids ('BVType n)
y)) (BVValue NatRepr n
_ Integer
0)))
     | Just BVType n :~: 'BVType n
Refl <- Value arch ids (BVType n)
-> Value arch ids ('BVType n) -> Maybe (BVType n :~: 'BVType n)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids (BVType n)
r Value arch ids ('BVType n)
r'
     , Just 'BVType n :~: BVType n
Refl <- Value arch ids ('BVType n)
-> Value arch ids (BVType n) -> Maybe ('BVType n :~: BVType n)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids ('BVType n)
y (NatRepr n -> Integer -> Value arch ids (BVType n)
forall (n :: Natural) arch ids.
(1 <= n) =>
NatRepr n -> Integer -> Value arch ids (BVType n)
mkLit NatRepr n
sz (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x))
     , Just Integer
b    <- AbsValue (RegAddrWidth (ArchReg arch)) tp -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton AbsValue (RegAddrWidth (ArchReg arch)) tp
av ->
       Value arch ids (BVType n)
-> Value arch ids (BVType n)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLeq Value arch ids (BVType n)
r Value arch ids (BVType n)
xv Integer
b AbsProcessorState (ArchReg arch) ids
regs

   -- FIXME: HACK
   -- This detects not (r - x < 0) && not (r - x == 0), i.e. x < r
   AndApp (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just
             (NotApp (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (UsbbOverflows Value arch ids (BVType n)
r xv :: Value arch ids (BVType n)
xv@(BVValue NatRepr n
sz Integer
x) (BoolValue Bool
False)))))
          (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just
             (NotApp (Value arch ids BoolType -> Maybe (App (Value arch ids) BoolType)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (Eq (Value arch ids tp1 -> Maybe (App (Value arch ids) tp1)
forall {arch} {ids} {tp :: Type}.
Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp -> Just (BVAdd NatRepr n
_ Value arch ids ('BVType n)
r' Value arch ids ('BVType n)
y)) (BVValue NatRepr n
_ Integer
0)))))
     | Just BVType n :~: 'BVType n
Refl <- Value arch ids (BVType n)
-> Value arch ids ('BVType n) -> Maybe (BVType n :~: 'BVType n)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids (BVType n)
r Value arch ids ('BVType n)
r'
     , Just 'BVType n :~: BVType n
Refl <- Value arch ids ('BVType n)
-> Value arch ids (BVType n) -> Maybe ('BVType n :~: BVType n)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids ('BVType n)
y (NatRepr n -> Integer -> Value arch ids (BVType n)
forall (n :: Natural) arch ids.
(1 <= n) =>
NatRepr n -> Integer -> Value arch ids (BVType n)
mkLit NatRepr n
sz (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x))
     , Just Integer
b    <- AbsValue (RegAddrWidth (ArchReg arch)) tp -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton AbsValue (RegAddrWidth (ArchReg arch)) tp
av ->
       Value arch ids (BVType n)
-> Value arch ids (BVType n)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLt Value arch ids (BVType n)
xv Value arch ids (BVType n)
r Integer
b AbsProcessorState (ArchReg arch) ids
regs

  -- Mux can let us infer the condition?
   App (Value arch ids) tp
_ -> AbsProcessorState (ArchReg arch) ids
regs
  where
    getAssignApp :: Value arch ids tp -> Maybe (App (Value arch ids) tp)
getAssignApp (AssignedValue (Assignment AssignId ids tp
_ (EvalApp App (Value arch ids) tp
a))) = App (Value arch ids) tp -> Maybe (App (Value arch ids) tp)
forall a. a -> Maybe a
Just App (Value arch ids) tp
a
    getAssignApp Value arch ids tp
_ = Maybe (App (Value arch ids) tp)
forall a. Maybe a
Nothing

refineTrunc :: ( (n + 1) <= n'
               , RefineConstraints arch
               )
            => BVValue arch ids n'
            -> NatRepr n
            -> AbsValue (ArchAddrWidth arch) (BVType n)
            -> AbsProcessorState (ArchReg arch) ids
            -> AbsProcessorState (ArchReg arch) ids
refineTrunc :: forall (n :: Natural) (n' :: Natural) arch ids.
((n + 1) <= n', RefineConstraints arch) =>
BVValue arch ids n'
-> NatRepr n
-> AbsValue (ArchAddrWidth arch) (BVType n)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineTrunc BVValue arch ids n'
v NatRepr n
sz AbsValue (ArchAddrWidth arch) (BVType n)
av AbsProcessorState (ArchReg arch) ids
regs = BVValue arch ids n'
-> AbsValue (ArchAddrWidth arch) (BVType n')
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue BVValue arch ids n'
v (NatRepr n
-> AbsValue (ArchAddrWidth arch) (BVType n)
-> AbsValue (ArchAddrWidth arch) (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
sz AbsValue (ArchAddrWidth arch) (BVType n)
av) AbsProcessorState (ArchReg arch) ids
regs

refineLt :: RefineConstraints arch
         => Value arch ids (BVType u)
         -> Value arch ids (BVType u)
         -> Integer
         -> AbsProcessorState (ArchReg arch) ids
         -> AbsProcessorState (ArchReg arch) ids
refineLt :: forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLt Value arch ids (BVType u)
x Value arch ids (BVType u)
y Integer
b AbsProcessorState (ArchReg arch) ids
regs
  -- y <= x
  | Integer
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0     = Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULeqTrue Value arch ids (BVType u)
y Value arch ids (BVType u)
x AbsProcessorState (ArchReg arch) ids
regs
  -- x < y case
  | Bool
otherwise  = Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULtTrue  Value arch ids (BVType u)
x Value arch ids (BVType u)
y AbsProcessorState (ArchReg arch) ids
regs

refineLeq :: RefineConstraints arch
          => Value arch ids (BVType u)
          -> Value arch ids (BVType u)
          -> Integer
          -> AbsProcessorState (ArchReg arch) ids
          -> AbsProcessorState (ArchReg arch) ids
refineLeq :: forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> Integer
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineLeq Value arch ids (BVType u)
x Value arch ids (BVType u)
y Integer
b AbsProcessorState (ArchReg arch) ids
regs
     -- y < x
    | Integer
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0     = Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULtTrue Value arch ids (BVType u)
y Value arch ids (BVType u)
x AbsProcessorState (ArchReg arch) ids
regs
    -- x <= y
    | Bool
otherwise  = Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULeqTrue Value arch ids (BVType u)
x Value arch ids (BVType u)
y AbsProcessorState (ArchReg arch) ids
regs

refineULeqTrue :: RefineConstraints arch
               => Value arch ids (BVType u)
               -> Value arch ids (BVType u)
               -> AbsProcessorState (ArchReg arch) ids
               -> AbsProcessorState (ArchReg arch) ids
refineULeqTrue :: forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULeqTrue Value arch ids (BVType u)
x Value arch ids (BVType u)
y AbsProcessorState (ArchReg arch) ids
regs = Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue Value arch ids (BVType u)
x AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
x_leq (Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue Value arch ids (BVType u)
y AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
y_leq AbsProcessorState (ArchReg arch) ids
regs)
  where
    (AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
x_leq, AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
y_leq) = NatRepr u
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> (AbsValue (RegAddrWidth (ArchReg arch)) (BVType u),
    AbsValue (RegAddrWidth (ArchReg arch)) (BVType u))
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULeq (Value arch ids (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch ids (BVType u)
x) (AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
regs Value arch ids (BVType u)
x) (AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
regs Value arch ids (BVType u)
y)
    -- check r@(a, b)
    --   | isBottom a = flip trace r $ "Bottom in refineLeq: "
    --                  ++ show (pretty regs)
    --   | isBottom b = flip trace r $ "Bottom in refineLeq: "
    --                  ++ show (pretty regs)
    --   | otherwise  = r

-- | Refine using the observation that x < y when treated as unsigned values.
refineULtTrue :: RefineConstraints arch
              => Value arch ids (BVType u)
              -> Value arch ids (BVType u)
              -> AbsProcessorState (ArchReg arch) ids
              -> AbsProcessorState (ArchReg arch) ids
refineULtTrue :: forall arch ids (u :: Natural).
RefineConstraints arch =>
Value arch ids (BVType u)
-> Value arch ids (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineULtTrue Value arch ids (BVType u)
x Value arch ids (BVType u)
y AbsProcessorState (ArchReg arch) ids
regs = Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue Value arch ids (BVType u)
x AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
x_lt (Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue Value arch ids (BVType u)
y AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
y_lt AbsProcessorState (ArchReg arch) ids
regs)
  where
    (AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
x_lt, AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
y_lt) = NatRepr u
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
-> (AbsValue (RegAddrWidth (ArchReg arch)) (BVType u),
    AbsValue (RegAddrWidth (ArchReg arch)) (BVType u))
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULt (Value arch ids (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch ids (BVType u)
x) (AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
regs Value arch ids (BVType u)
x) (AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType u)
-> AbsValue (RegAddrWidth (ArchReg arch)) (BVType u)
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
regs Value arch ids (BVType u)
y)

-- | This uses an assertion about a given value being true or false to
-- refine the information in an abstract processor state.
refineProcState :: ( RegisterInfo (ArchReg arch)
                   , OrdF (ArchReg arch)
                   , HasRepr (ArchReg arch) TypeRepr
                   )
                => Value arch ids BoolType
                   -- ^ Condition known to be true/false.
                -> Bool
                -- ^ Indicates whether the Boolean above is true/false.
                -> AbsProcessorState (ArchReg arch) ids
                -> AbsProcessorState (ArchReg arch) ids
refineProcState :: forall arch ids.
(RegisterInfo (ArchReg arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
Value arch ids BoolType
-> Bool
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineProcState Value arch ids BoolType
v Bool
isTrue AbsProcessorState (ArchReg arch) ids
ps0 = Value arch ids BoolType
-> AbsValue (ArchAddrWidth arch) BoolType
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall arch ids (tp :: Type).
RefineConstraints arch =>
Value arch ids tp
-> AbsValue (ArchAddrWidth arch) tp
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
refineValue Value arch ids BoolType
v (if Bool
isTrue then AbsValue (ArchAddrWidth arch) BoolType
forall (w :: Natural). AbsValue w BoolType
absTrue else AbsValue (ArchAddrWidth arch) BoolType
forall (w :: Natural). AbsValue w BoolType
absFalse) AbsProcessorState (ArchReg arch) ids
ps0