Merge pull request #2338 from ucsd-progsys/fd/strengthen-inline-loop-…

…breaker

Strengthen the inlineLoopBreaker transformation

.circleci/config.yml

@@ -44,7 +44,7 @@ commands:
             chmod +x ./x86_64-linux-ghcup
             ./x86_64-linux-ghcup install ghc << parameters.ghc_version >>
             ./x86_64-linux-ghcup set ghc << parameters.ghc_version >>
-            ./x86_64-linux-ghcup install cabal 3.10.2.0
+            ./x86_64-linux-ghcup install cabal 3.12.1.0
             export PATH=~/.ghcup/bin:$PATH
             echo 'export PATH=~/.ghcup/bin:$PATH' >> $BASH_ENV
             cabal update

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -548,6 +548,7 @@ import GHC.Types.Basic                as Ghc
     , funPrec
     , InlinePragma(inl_act, inl_inline, inl_rule, inl_sat, inl_src)
     , isDeadOcc
+    , isNoInlinePragma
     , isStrongLoopBreaker
     , noOccInfo
     , topPrec
@@ -574,6 +575,7 @@ import GHC.Types.Id                   as Ghc
     , idInfo
     , idOccInfo
     , isConLikeId
+    , idInlinePragma
     , modifyIdInfo
     , mkExportedLocalId
     , mkUserLocal

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -56,11 +56,13 @@ module Language.Haskell.Liquid.Bare.Resolve
 
 import qualified Control.Exception                 as Ex
 import           Control.Monad (mplus)
+import           Data.Function (on)
 import qualified Data.List                         as L
 import qualified Data.HashSet                      as S
 import qualified Data.Maybe                        as Mb
 import qualified Data.HashMap.Strict               as M
 import qualified Data.Text                         as T
+import           Text.Megaparsec.Pos (sourceColumn, sourceLine)
 import qualified Text.PrettyPrint.HughesPJ         as PJ
 
 import qualified Language.Fixpoint.Types               as F
@@ -119,30 +121,37 @@ makeLocalVars :: GhcSrc -> LocalVars
 makeLocalVars = localVarMap . localBinds . _giCbs
 
 -- TODO: rewrite using CoreVisitor
-localBinds :: [Ghc.CoreBind] -> [Ghc.Var]
-localBinds                    = concatMap (bgo S.empty)
+localBinds :: [Ghc.CoreBind] -> [LocalVarDetails]
+localBinds                    = concatMap bgoT
   where
-    add  x g                  = maybe g (`S.insert` g) (localKey x)
-    adds b g                  = foldr add g (Ghc.bindersOf b)
-    take' x g                 = maybe [] (\k -> [x | not (S.member k g)]) (localKey x)
-    pgo g (x, e)              = take' x g ++ go (add x g) e
-    bgo g (Ghc.NonRec x e)    = pgo g (x, e)
-    bgo g (Ghc.Rec xes)       = concatMap (pgo g) xes
-    go  g (Ghc.App e a)       = concatMap (go  g) [e, a]
-    go  g (Ghc.Lam _ e)       = go g e
-    go  g (Ghc.Let b e)       = bgo g b ++ go (adds b g) e
-    go  g (Ghc.Tick _ e)      = go g e
-    go  g (Ghc.Cast e _)      = go g e
-    go  g (Ghc.Case e _ _ cs) = go g e ++ concatMap (go g . (\(Ghc.Alt _ _ e') -> e')) cs
-    go  _ (Ghc.Var _)         = []
-    go  _ _                   = []
-
-localVarMap :: [Ghc.Var] -> LocalVars
-localVarMap vs =
-  Misc.group [ (x, (i, v)) | v <- vs
-                           , let i = F.unPos (F.srcLine v)
-                           , x <- Mb.maybeToList (localKey v)
-             ]
+    bgoT (Ghc.NonRec _ e)   = go e
+    bgoT (Ghc.Rec xes)      = concatMap (go . snd) xes
+    pgo isRec (x, e)        = mkLocalVarDetails isRec x : go e
+    bgo (Ghc.NonRec x e)    = pgo False (x, e)
+    bgo (Ghc.Rec xes)       = concatMap (pgo True) xes
+    go  (Ghc.App e a)       = concatMap go [e, a]
+    go  (Ghc.Lam _ e)       = go e
+    go  (Ghc.Let b e)       = bgo b ++ go e
+    go  (Ghc.Tick _ e)      = go e
+    go  (Ghc.Cast e _)      = go e
+    go  (Ghc.Case e _ _ cs) = go e ++ concatMap (go . (\(Ghc.Alt _ _ e') -> e')) cs
+    go  (Ghc.Var _)         = []
+    go  _                   = []
+
+    mkLocalVarDetails isRec v = LocalVarDetails
+      { lvdSourcePos = F.sp_start $ F.srcSpan v
+      , lvdVar = v
+      , lvdIsRec = isRec
+      }
+
+localVarMap :: [LocalVarDetails] -> LocalVars
+localVarMap lvds =
+    Misc.group
+      [ (x, lvd)
+      | lvd <- lvds
+      , let v = lvdVar lvd
+            x = F.symbol $ Ghc.occNameString $ Ghc.nameOccName $ Ghc.varName v
+      ]
 
 localKey   :: Ghc.Var -> Maybe F.Symbol
 localKey v
@@ -480,14 +489,37 @@ lookupGhcVar env name kind lx = case resolveLocSym env name kind lx of
 --   See tests/names/LocalSpec.hs for a motivating example.
 
 lookupLocalVar :: Env -> LocSymbol -> [Ghc.Var] -> Maybe Ghc.Var
-lookupLocalVar env lx gvs = Misc.findNearest lxn kvs
+lookupLocalVar env lx gvs = findNearest lxn kvs
   where
     _msg                  = "LOOKUP-LOCAL: " ++ F.showpp (F.val lx, lxn, kvs)
-    kvs                   = gs ++ M.lookupDefault [] x (reLocalVars env)
-    gs                    = [(F.unPos (F.srcLine v), v) | v <- gvs]
-    lxn                   = F.unPos (F.srcLine lx)
+    kvs                   = prioritizeRecBinds (M.lookupDefault [] x $ reLocalVars env) ++ gs
+    gs                    = [(F.sp_start $ F.srcSpan v, v) | v <- gvs]
+    lxn                   = F.sp_start $ F.srcSpan lx
     (_, x)                = unQualifySymbol (F.val lx)
 
+    -- Sometimes GHC produces multiple bindings that have the same source
+    -- location. To select among these, we give preference to the recursive
+    -- bindings which might need termination metrics.
+    prioritizeRecBinds lvds =
+      let (recs, nrecs) = L.partition lvdIsRec lvds
+       in map lvdToPair (recs ++ nrecs)
+    lvdToPair lvd = (lvdSourcePos lvd, lvdVar lvd)
+
+    findNearest :: F.SourcePos -> [(F.SourcePos, Ghc.Var)] -> Maybe Ghc.Var
+    findNearest key kvs = argMin [ (posDistance key k, v) | (k, v) <- kvs ]
+
+    -- We prefer the var with the smaller distance, or equal distance
+    -- but left of the spec, or not left of the spec but below it.
+    posDistance a b =
+      ( abs (F.unPos (sourceLine a) - F.unPos (sourceLine b))
+      , sourceColumn a < sourceColumn b -- Note: False is prefered/smaller to True
+      , sourceLine a > sourceLine b
+      )
+
+    argMin :: (Ord k) => [(k, v)] -> Maybe v
+    argMin = Mb.listToMaybe . map snd . L.sortBy (compare `on` fst)
+
+
 lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.DataCon
 lookupGhcDataCon = resolveLocSym -- strictResolveSym
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs

@@ -8,6 +8,7 @@ module Language.Haskell.Liquid.Bare.Types
   , TyThingMap 
   , ModSpecs
   , LocalVars 
+  , LocalVarDetails (..)
 
     -- * Tycon and Datacon processing environment
   , TycEnv (..) 
@@ -83,7 +84,13 @@ instance HasConfig Env where
 
 -- | @LocalVars@ is a map from names to lists of pairs of @Ghc.Var@ and 
 --   the lines at which they were defined. 
-type LocalVars = M.HashMap F.Symbol [(Int, Ghc.Var)]
+type LocalVars = M.HashMap F.Symbol [LocalVarDetails]
+
+data LocalVarDetails = LocalVarDetails
+  { lvdSourcePos :: F.SourcePos
+  , lvdVar :: Ghc.Var
+  , lvdIsRec :: Bool  -- ^ Is the variable defined in a letrec?
+  } deriving Show
 
 -------------------------------------------------------------------------------
 -- | A @TyThingMap@ is used to resolve symbols into GHC @TyThing@ and, 

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs

@@ -30,7 +30,6 @@ import           Language.Haskell.Liquid.Constraint.Types (CG, CGInfo (..), CGEn
 import           Language.Haskell.Liquid.Constraint.Monad (addWarning)
 import           Language.Haskell.Liquid.Constraint.Env (setTRec)
 import           Language.Haskell.Liquid.Constraint.Template ( Template(..), unTemplate, varTemplate, safeFromAsserted, extender )
-import           Language.Haskell.Liquid.Transforms.Rec (isIdTRecBound)
 import           Language.Haskell.Liquid.Types (refreshArgs, HasConfig (..), toRSort)
 import           Language.Haskell.Liquid.Types.Types
   (SpecType, TError (..), RType (..), RTypeRep (..), Oblig (..), Error, Config (..), RReft,
@@ -91,21 +90,21 @@ addObligation o t r  = mkArrow αs πs xts $ RRTy [] r o t2
 -- | TERMINATION TYPE ----------------------------------------------------------
 --------------------------------------------------------------------------------
 
-makeDecrIndex :: (GHC.Var, Template SpecType, [GHC.Var]) -> CG (Maybe Int)
-makeDecrIndex (x, Assumed t, args)
-  = do dindex <- makeDecrIndexTy x t args
+makeDecrIndex :: (GHC.Var, Template SpecType) -> CG (Maybe Int)
+makeDecrIndex (x, Assumed t)
+  = do dindex <- makeDecrIndexTy x t
        case dindex of
          Left msg -> addWarning msg >> return Nothing
          Right i -> return $ Just i
-makeDecrIndex (x, Asserted t, args)
-  = do dindex <- makeDecrIndexTy x t args
+makeDecrIndex (x, Asserted t)
+  = do dindex <- makeDecrIndexTy x t
        case dindex of
          Left msg -> addWarning msg >> return Nothing
          Right i  -> return $ Just i
 makeDecrIndex _ = return Nothing
 
-makeDecrIndexTy :: GHC.Var -> SpecType -> [GHC.Var] -> CG (Either (TError t) Int)
-makeDecrIndexTy x st args
+makeDecrIndexTy :: GHC.Var -> SpecType -> CG (Either (TError t) Int)
+makeDecrIndexTy x st
   = do autosz <- gets autoSize
        return $ case dindex autosz of
          Nothing -> Left msg
@@ -114,11 +113,10 @@ makeDecrIndexTy x st args
        msg  = ErrTermin (GHC.getSrcSpan x) [F.pprint x] (text "No decreasing parameter")
        trep = toRTypeRep $ unOCons st
        ts   = ty_args trep
-       tvs  = zip ts args
        cenv = makeNumEnv ts
 
-       p autosz (t, v)   = isDecreasing autosz cenv t && not (isIdTRecBound v)
-       dindex     autosz = L.findIndex (p autosz) tvs
+       p autosz t = isDecreasing autosz cenv t
+       dindex     autosz = L.findIndex (p autosz) ts
 
 recType :: F.Symbolic a
         => S.HashSet GHC.TyCon
@@ -186,7 +184,7 @@ consCBSizedTys consBind γ xes
        autoenv  <- gets autoSize
        ts       <- forM ts' $ T.mapM refreshArgs
        let vs    = zipWith collectArgs' ts es
-       is       <- mapM makeDecrIndex (zip3 vars ts vs) >>= checkSameLens
+       is       <- mapM makeDecrIndex (zip vars ts) >>= checkSameLens
        let xeets = zipWith (\v i -> [((v,i), x) | x <- zip3 vars is $ map unTemplate ts]) vs is
        _        <- mapM checkIndex (zip4 vars vs ts is) >>= checkEqTypes
        let rts   = (recType autoenv <$>) <$> xeets

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs

@@ -26,7 +26,6 @@ module Language.Haskell.Liquid.GHC.Interface (
 
   -- * Internal exports (provisional)
   , extractSpecComments
-  , extractSpecQuotes'
   , makeLogicMap
   , classCons
   , derivedVars
@@ -62,13 +61,9 @@ import Control.Exception
 import Control.Monad
 import Control.Monad.Trans.Maybe
 
-import Data.Data
 import Data.List hiding (intersperse)
 import Data.Maybe
 
-import Data.Generics.Aliases (mkT)
-import Data.Generics.Schemes (everywhere)
-
 import qualified Data.HashSet        as S
 
 import System.IO
@@ -85,9 +80,6 @@ import qualified Language.Haskell.Liquid.Measure  as Ms
 import qualified Language.Haskell.Liquid.Misc     as Misc
 import Language.Haskell.Liquid.Parse
 import Language.Haskell.Liquid.Types hiding (Spec)
--- import Language.Haskell.Liquid.Types.PrettyPrint
--- import Language.Haskell.Liquid.Types.Visitors
-import Language.Haskell.Liquid.UX.QuasiQuoter
 import Language.Haskell.Liquid.UX.Tidy
 
 import qualified Debug.Trace as Debug
@@ -304,28 +296,6 @@ extractSpecComment (Ghc.L sp (ApiBlockComment txt))
 
 extractSpecComment _ = Nothing
 
-extractSpecQuotes' :: (a -> Module) -> (a -> [Annotation]) -> a -> [BPspec]
-extractSpecQuotes' thisModule getAnns a = mapMaybe extractSpecQuote anns
-  where
-    anns = map ann_value $
-           filter (isOurModTarget . ann_target) $
-           getAnns a
-
-    isOurModTarget (ModuleTarget mod1) = mod1 == thisModule a
-    isOurModTarget _ = False
-
-extractSpecQuote :: AnnPayload -> Maybe BPspec
-extractSpecQuote payload =
-  case Ghc.fromSerialized Ghc.deserializeWithData payload of
-    Nothing -> Nothing
-    Just qt -> Just $ refreshSymbols $ liquidQuoteSpec qt
-
-refreshSymbols :: Data a => a -> a
-refreshSymbols = everywhere (mkT refreshSymbol)
-
-refreshSymbol :: Symbol -> Symbol
-refreshSymbol = symbol . symbolText
-
 --------------------------------------------------------------------------------
 -- | Finding & Parsing Files ---------------------------------------------------
 --------------------------------------------------------------------------------