From 82dcf7dd2e46f3cc154ccd8f09af2b732c88fe61 Mon Sep 17 00:00:00 2001
From: Eric Seidel <gridaphobe@gmail.com>
Date: Fri, 10 Jul 2015 13:10:56 -0700
Subject: [PATCH] give string literals a refined type with their length

---
 include/GHC/Base.spec                       |  1 +
 include/GHC/CString.spec                    |  4 +++-
 src/Language/Haskell/Liquid/Bare/GhcSpec.hs |  2 +-
 src/Language/Haskell/Liquid/Literals.hs     | 18 +++++++++++++++---
 src/Language/Haskell/Liquid/Measure.hs      | 17 +++++++++++++++++
 tests/pos/StringLit.hs                      |  4 ++++
 6 files changed, 41 insertions(+), 5 deletions(-)
 create mode 100644 tests/pos/StringLit.hs

diff --git a/include/GHC/Base.spec b/include/GHC/Base.spec
index 5302c9bceb..4adc7db598 100644
--- a/include/GHC/Base.spec
+++ b/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
diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec
index c62541f48f..e308167fe3 100644
--- a/include/GHC/CString.spec
+++ b/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}
diff --git a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs b/src/Language/Haskell/Liquid/Bare/GhcSpec.hs
index 9674f92514..1483bf704a 100644
--- a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs
+++ b/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 ]
diff --git a/src/Language/Haskell/Liquid/Literals.hs b/src/Language/Haskell/Liquid/Literals.hs
index dd8b89987f..5da831204a 100644
--- a/src/Language/Haskell/Liquid/Literals.hs
+++ b/src/Language/Haskell/Liquid/Literals.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE OverloadedStrings #-}
 module Language.Haskell.Liquid.Literals (
         literalFRefType, literalFReft, literalConst
         ) where
@@ -5,12 +6,15 @@ module Language.Haskell.Liquid.Literals (
 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
diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs
index 762280a85f..8692cab0f6 100644
--- a/src/Language/Haskell/Liquid/Measure.hs
+++ b/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]
diff --git a/tests/pos/StringLit.hs b/tests/pos/StringLit.hs
new file mode 100644
index 0000000000..06dc738ed3
--- /dev/null
+++ b/tests/pos/StringLit.hs
@@ -0,0 +1,4 @@
+module StringLit where
+
+{-@ foo :: {v:String | len v = 3} @-}
+foo = "foo"