-- | Go through the program and use algebraic simplification and range
-- analysis to try to figure out which assertions are statically true.
--
-- Currently implemented by running the simplifier with a special rule
-- that is too expensive to run all the time.

module Futhark.Pass.ResolveAssertions
  ( resolveAssertions
  )
  where

import Data.Maybe
import Data.Monoid

import qualified Futhark.Analysis.SymbolTable as ST
import Futhark.Optimise.Simplify.Rule
import qualified Futhark.Analysis.AlgSimplify as AS
import qualified Futhark.Analysis.ScalExp as SE
import Futhark.Analysis.PrimExp.Convert
import Futhark.Representation.AST.Syntax
import Futhark.Construct
import Futhark.Pass
import Futhark.Representation.SOACS (SOACS)
import qualified Futhark.Representation.SOACS.Simplify as Simplify
import qualified Futhark.Optimise.Simplify as Simplify

import Prelude

-- | The assertion-resolver pass.
resolveAssertions :: Pass SOACS SOACS
resolveAssertions :: Pass SOACS SOACS
resolveAssertions = String
-> String -> (Prog SOACS -> PassM (Prog SOACS)) -> Pass SOACS SOACS
forall fromlore tolore.
String
-> String
-> (Prog fromlore -> PassM (Prog tolore))
-> Pass fromlore tolore
Pass
  String
"resolve assertions"
  String
"Try to statically resolve bounds checks and similar." ((Prog SOACS -> PassM (Prog SOACS)) -> Pass SOACS SOACS)
-> (Prog SOACS -> PassM (Prog SOACS)) -> Pass SOACS SOACS
forall a b. (a -> b) -> a -> b
$
  SimpleOps SOACS
-> RuleBook (Wise SOACS)
-> HoistBlockers SOACS
-> Prog SOACS
-> PassM (Prog SOACS)
forall lore.
SimplifiableLore lore =>
SimpleOps lore
-> RuleBook (Wise lore)
-> HoistBlockers lore
-> Prog lore
-> PassM (Prog lore)
Simplify.simplifyProg SimpleOps SOACS
Simplify.simpleSOACS RuleBook (Wise SOACS)
rulebook HoistBlockers SOACS
forall lore. HoistBlockers lore
Simplify.noExtraHoistBlockers
  where rulebook :: RuleBook (Wise SOACS)
rulebook = RuleBook (Wise SOACS)
Simplify.soacRules RuleBook (Wise SOACS)
-> RuleBook (Wise SOACS) -> RuleBook (Wise SOACS)
forall a. Semigroup a => a -> a -> a
<> [TopDownRule (Wise SOACS)]
-> [BottomUpRule (Wise SOACS)] -> RuleBook (Wise SOACS)
forall m. [TopDownRule m] -> [BottomUpRule m] -> RuleBook m
ruleBook [ RuleBasicOp (Wise SOACS) (TopDown (Wise SOACS))
-> TopDownRule (Wise SOACS)
forall lore a. RuleBasicOp lore a -> SimplificationRule lore a
RuleBasicOp RuleBasicOp (Wise SOACS) (TopDown (Wise SOACS))
forall lore. BinderOps lore => TopDownRuleBasicOp lore
simplifyScalExp ] []

simplifyScalExp :: BinderOps lore => TopDownRuleBasicOp lore
simplifyScalExp :: TopDownRuleBasicOp lore
simplifyScalExp TopDown lore
vtable Pattern lore
pat StmAux (ExpAttr lore)
_ BasicOp
e = RuleM lore () -> Rule lore
forall lore. RuleM lore () -> Rule lore
Simplify (RuleM lore () -> Rule lore) -> RuleM lore () -> Rule lore
forall a b. (a -> b) -> a -> b
$ do
  Maybe ScalExp
res <- LookupVar -> Exp Any -> RuleM lore (Maybe ScalExp)
forall t (f :: * -> *) lore.
(HasScope t f, Monad f) =>
LookupVar -> Exp lore -> f (Maybe ScalExp)
SE.toScalExp (VName -> TopDown lore -> Maybe ScalExp
forall lore.
Attributes lore =>
VName -> SymbolTable lore -> Maybe ScalExp
`ST.lookupScalExp` TopDown lore
vtable) (Exp Any -> RuleM lore (Maybe ScalExp))
-> Exp Any -> RuleM lore (Maybe ScalExp)
forall a b. (a -> b) -> a -> b
$ BasicOp -> Exp Any
forall lore. BasicOp -> ExpT lore
BasicOp BasicOp
e
  case Maybe ScalExp
res of
    -- If the sufficient condition is 'True', then it statically succeeds.
    Just ScalExp
se
      | BasicOp -> Bool
interesting BasicOp
e,
        Maybe SubExp -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe SubExp -> Bool) -> Maybe SubExp -> Bool
forall a b. (a -> b) -> a -> b
$ ScalExp -> Maybe SubExp
valOrVar ScalExp
se,
        ScalExp -> Int
SE.scalExpSize ScalExp
se Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size_bound,
        Just SubExp
se' <- ScalExp -> Maybe SubExp
valOrVar (ScalExp -> Maybe SubExp) -> ScalExp -> Maybe SubExp
forall a b. (a -> b) -> a -> b
$ ScalExp -> RangesRep -> ScalExp
AS.simplify ScalExp
se RangesRep
ranges ->
        Pattern (Lore (RuleM lore))
-> Exp (Lore (RuleM lore)) -> RuleM lore ()
forall (m :: * -> *).
MonadBinder m =>
Pattern (Lore m) -> Exp (Lore m) -> m ()
letBind_ Pattern lore
Pattern (Lore (RuleM lore))
pat (Exp (Lore (RuleM lore)) -> RuleM lore ())
-> Exp (Lore (RuleM lore)) -> RuleM lore ()
forall a b. (a -> b) -> a -> b
$ BasicOp -> ExpT lore
forall lore. BasicOp -> ExpT lore
BasicOp (BasicOp -> ExpT lore) -> BasicOp -> ExpT lore
forall a b. (a -> b) -> a -> b
$ SubExp -> BasicOp
SubExp SubExp
se'
    Maybe ScalExp
_ -> RuleM lore ()
forall lore a. RuleM lore a
cannotSimplify
  where ranges :: RangesRep
ranges = TopDown lore -> RangesRep
forall lore. SymbolTable lore -> RangesRep
ST.rangesRep TopDown lore
vtable
        size_bound :: Int
size_bound = Int
10 -- don't touch scalexps bigger than this.

        valOrVar :: ScalExp -> Maybe SubExp
valOrVar (SE.Val PrimValue
v)  = SubExp -> Maybe SubExp
forall a. a -> Maybe a
Just (SubExp -> Maybe SubExp) -> SubExp -> Maybe SubExp
forall a b. (a -> b) -> a -> b
$ PrimValue -> SubExp
Constant PrimValue
v
        valOrVar (SE.Id VName
v PrimType
_) = SubExp -> Maybe SubExp
forall a. a -> Maybe a
Just (SubExp -> Maybe SubExp) -> SubExp -> Maybe SubExp
forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
v
        valOrVar ScalExp
_           = Maybe SubExp
forall a. Maybe a
Nothing

        interesting :: BasicOp -> Bool
interesting CmpOp{} = Bool
True
        interesting (BinOp BinOp
LogAnd SubExp
_ SubExp
_) = Bool
True
        interesting (BinOp BinOp
LogOr SubExp
_ SubExp
_) = Bool
True
        interesting (BinOp BinOp
_ SubExp
x SubExp
y) = SubExp -> Bool
isConst SubExp
x Bool -> Bool -> Bool
|| SubExp -> Bool
isConst SubExp
y
        interesting BasicOp
_ = Bool
False

        isConst :: SubExp -> Bool
isConst Constant{} = Bool
True
        isConst Var{} = Bool
False