give string literals a refined type with their length

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:String | len v == strLen x}

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/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
 
@@ -26,10 +30,18 @@ makeRTypeBase _              _
   = error "RefType : makeRTypeBase"
 
 literalFRefType tce l
-  = makeRTypeBase (literalType l) (literalFReft tce l)
+  = makeRTypeBase (literalType l) (addStrLen l $ literalFReft tce l)
 
-literalFReft tce = maybe mempty exprReft . snd . literalConst tce
+literalFReft tce = maybe mempty F.exprReft . snd . literalConst tce
 
+addStrLen l = F.meet r
+  where
+    r = case l of
+          MachStr str ->
+            F.reft "v" (F.PAtom F.Eq
+                        (F.EApp (name strLen) [F.EVar "v"])
+                        (F.ECon (F.I (fromIntegral (T.length $ T.decodeUtf8 str)))))
+          _ -> mempty
 
 -- | `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"