Merge pull request #415 from gridaphobe/master

add special rule for string literals

fixes #414

include/GHC/Base.spec

@@ -1,5 +1,6 @@
 module spec GHC.Base where
 
+import GHC.CString
 import GHC.Prim
 import GHC.Classes
 import GHC.Types

include/GHC/CString.spec

@@ -2,4 +2,6 @@ module spec GHC.CString where
 
 import GHC.Prim 
 
-GHC.CString.unpackCString# :: x:GHC.Prim.Addr# -> {v:String | v ~~ x}
+GHC.CString.unpackCString#
+  :: x:GHC.Prim.Addr#
+  -> {v:[Char] | v ~~ x && len v == strLen x}

src/Language/Haskell/Liquid/ANFTransform.hs

@@ -125,21 +125,18 @@ normalizeName :: VarEnv Id -> CoreExpr -> DsMW CoreExpr
 -- normalizeNameDebug γ e 
 --   = liftM (tracePpr ("normalizeName" ++ showPpr e)) $ normalizeName γ e
 
-normalizeName _ e@(Lit (LitInteger _ _))
-  = normalizeLiteral e
-
-normalizeName _ e@(Tick _ (Lit (LitInteger _ _)))
+normalizeName _ e@(Lit l)
+  | shouldNormalize l
   = normalizeLiteral e
+  | otherwise
+  = return e
 
 normalizeName γ (Var x)
   = return $ Var (lookupWithDefaultVarEnv γ x x)
 
 normalizeName _ e@(Type _)
   = return e
 
-normalizeName _ e@(Lit _)
-  = return e
-
 normalizeName _ e@(Coercion _)
   = do x     <- lift $ freshNormalVar $ exprType e
        add  [NonRec x e]
@@ -155,6 +152,10 @@ normalizeName γ e
        add [NonRec x e']
        return $ Var x
 
+shouldNormalize l = case l of
+  LitInteger _ _ -> True
+  MachStr _ -> True
+  _ -> False
 
 add :: [CoreBind] -> DsMW ()
 add w = modify $ \s -> s{st_binds = st_binds s++w}

src/Language/Haskell/Liquid/Bare/GhcSpec.hs

@@ -227,7 +227,7 @@ makeGhcSpecCHOP2 cbs specs dcSelectors datacons cls embs
        name            <- gets modName
        mapM_ (makeHaskellInlines  cbs name) specs
        hmeans          <- mapM (makeHaskellMeasures cbs name) specs
-       let measures     = mconcat (measures':Ms.mkMSpec' dcSelectors:hmeans)
+       let measures     = mconcat (Ms.wiredInMeasures:measures':Ms.mkMSpec' dcSelectors:hmeans)
        let (cs, ms)     = makeMeasureSpec' measures
        let cms          = makeClassMeasureSpec measures
        let cms'         = [ (x, Loc l l' $ cSort t) | (Loc l l' x, t) <- cms ]

src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -1453,8 +1453,8 @@ consE γ (Var x)
        addLocA (Just x) (loc γ) (varAnn γ x t)
        return t
 
-consE γ (Lit c)
-  = refreshVV $ uRType $ literalFRefType (emb γ) c
+consE _ (Lit c)
+  = refreshVV $ uRType $ literalFRefType c
 
 consE γ e'@(App e (Type τ))
   = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e
@@ -1686,7 +1686,7 @@ caseEnv γ x acs a _
        cγ     <- addBinders γ x' [(x', xt')]
        return cγ
 
-altReft γ _ (LitAlt l)   = literalFReft (emb γ) l
+altReft _ _ (LitAlt l)   = literalFReft l
 altReft γ acs DEFAULT    = mconcat [notLiteralReft l | LitAlt l <- acs]
   where notLiteralReft   = maybe mempty F.notExprReft . snd . literalConst (emb γ)
 altReft _ _ _            = error "Constraint : altReft"

src/Language/Haskell/Liquid/CoreToLogic.hs

@@ -388,6 +388,7 @@ isUndefined (_, _, e) = isUndefinedExpr e
   where 
    -- auto generated undefined case: (\_ -> (patError @type "error message")) void
    isUndefinedExpr (C.App (C.Var x) _) | (show x) `elem` perrors = True
+   isUndefinedExpr (C.Let _ e) = isUndefinedExpr e
    -- otherwise 
    isUndefinedExpr _ = False 
 

src/Language/Haskell/Liquid/Literals.hs

@@ -1,16 +1,20 @@
+{-# LANGUAGE OverloadedStrings #-}
 module Language.Haskell.Liquid.Literals (
         literalFRefType, literalFReft, literalConst
         ) where
 
 import TypeRep
 import Literal 
 
+import Language.Haskell.Liquid.Measure
 import Language.Haskell.Liquid.Types
 import Language.Haskell.Liquid.RefType
 import Language.Haskell.Liquid.CoreToLogic (mkLit)
 
-import Language.Fixpoint.Types (exprReft)
+import qualified Language.Fixpoint.Types as F
 
+import qualified Data.Text as T
+import qualified Data.Text.Encoding as T
 import Data.Monoid
 import Control.Applicative
 
@@ -25,11 +29,19 @@ makeRTypeBase (TyConApp c ts) x
 makeRTypeBase _              _
   = error "RefType : makeRTypeBase"
 
-literalFRefType tce l
-  = makeRTypeBase (literalType l) (literalFReft tce l)
+literalFRefType l
+  = makeRTypeBase (literalType l) (literalFReft l)
 
-literalFReft tce = maybe mempty exprReft . snd . literalConst tce
+literalFReft l = maybe mempty mkReft $ mkLit l
 
+mkReft e = case e of
+            F.ESym (F.SL str) ->
+              -- FIXME: unsorted equality is shady, better to not embed Add# as int..
+              F.meet (F.uexprReft e)
+                     (F.reft "v" (F.PAtom F.Eq
+                                  (F.EApp (name strLen) [F.EVar "v"])
+                                  (F.ECon (F.I (fromIntegral (T.length str))))))
+            _ -> F.exprReft e
 
 -- | `literalConst` returns `Nothing` for unhandled lits because
 --    otherwise string-literals show up as global int-constants

src/Language/Haskell/Liquid/Measure.hs

@@ -12,10 +12,15 @@ module Language.Haskell.Liquid.Measure (
   , mapTy
   , dataConTypes
   , defRefType
+  , strLen
+  , wiredInMeasures
   ) where
 
 import GHC hiding (Located)
 import Var
+import Type
+import TysPrim
+import TysWiredIn
 import Text.PrettyPrint.HughesPJ hiding (first)
 import Text.Printf (printf)
 import DataCon
@@ -347,3 +352,15 @@ bodyPred ::  Expr -> Body -> Pred
 bodyPred fv (E e)    = PAtom Eq fv e
 bodyPred fv (P p)    = PIff  (PBexp fv) p
 bodyPred fv (R v' p) = subst1 p (v', fv)
+
+
+-- | A wired-in measure @strLen@ that describes the length of a string
+-- literal, with type @Addr#@.
+strLen :: Measure SpecType ctor
+strLen = M { name = dummyLoc "strLen"
+           , sort = ofType (mkFunTy addrPrimTy intTy)
+           , eqns = []
+           }
+
+wiredInMeasures :: MSpec SpecType DataCon
+wiredInMeasures = mkMSpec' [strLen]

tests/pos/StringLit.hs

@@ -0,0 +1,4 @@
+module StringLit where
+
+{-@ foo :: {v:String | len v = 3} @-}
+foo = "foo"