Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix unsafe data constructor refinements #2470

Merged
merged 9 commits into from
Jan 14, 2025
Merged

Fix unsafe data constructor refinements #2470

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
24b415d
Allow only safe refinements of data constructors
AlecsFerra Jan 10, 2025
31a8d59
Merge branch 'ucsd-progsys:develop' into develop
AlecsFerra Jan 10, 2025
d461ed3
Apply suggestions from code review
AlecsFerra Jan 10, 2025
4d69733
Make error in negative test explicit
AlecsFerra Jan 10, 2025
df43885
Add a flag to allow unsafe ctor refinement
AlecsFerra Jan 14, 2025
13fa421
Add documentation for allow-unsafe-constructors
AlecsFerra Jan 14, 2025
3b6ee53
typo
AlecsFerra Jan 14, 2025
4d70d12
Mention --allow-unsafe-constructors in the error message for usafe co…
AlecsFerra Jan 14, 2025
d61e399
Apply suggestions from code review
AlecsFerra Jan 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,9 @@ _ *** _ = ()
data QED = Admit | QED

{-@ measure isAdmit :: QED -> Bool @-}
{-@ Admit :: {v:QED | isAdmit v } @-}
isAdmit :: QED -> Bool
isAdmit Admit = True
isAdmit QED = False


-------------------------------------------------------------------------------
Expand Down
27 changes: 27 additions & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ checkTargetSpec specs src env cbs tsp
<> checkSizeFun emb env (gsTconsP (gsName tsp))
<> checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig tsp) ])
<> checkRewrites tsp
<> checkConstructorRefinement (gsTySigs $ gsSig tsp)

_rClasses = concatMap Ms.classes specs
_rInsts = concatMap Ms.rinstance specs
Expand All @@ -193,6 +194,32 @@ checkTargetSpec specs src env cbs tsp



checkConstructorRefinement :: [(Var, LocSpecType)] -> Diagnostics
checkConstructorRefinement = mconcat . map checkOne
where
checkOne (s, ty) | isCtorName s
, not $ validRef $ getRetTyRef $ val ty
= mkDiagnostics mempty [ ErrCtorRefinement (GM.sourcePosSrcSpan $ loc ty) (pprint s) ]
checkOne _ = mempty

getRetTyRef (RFun _ _ _ t _) = getRetTyRef t
getRetTyRef (RAllT _ t _) = getRetTyRef t
getRetTyRef t = ur_reft $ rt_reft t

-- True refinement
validRef (F.Reft (_, F.PTrue))
= True
-- Prop foo from ProofCombinators
validRef (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) _))
| n == "Language.Haskell.Liquid.ProofCombinators.prop"
, v == v'
= True
Comment on lines +222 to +225
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this need to be so strict? Maybe it is fine to allow both prop v = foo and foo = prop v.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No is fine also in the other direction, I just copied the way that is done in ProofCombinators

validRef _ = False

isCtorName x = case idDetails x of
DataConWorkId _ -> True
DataConWrapId _ -> True
_ -> False


checkPlugged :: PPrint v => [(v, LocSpecType)] -> Diagnostics
Expand Down
10 changes: 10 additions & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -483,6 +483,11 @@ data TError t =
, dc :: !Doc
}

| ErrCtorRefinement { pos :: !SrcSpan
, ctorName :: !Doc
} -- ^ The refinement of a doesn't admit
-- a refinement on the return type that
-- isn't deemd safe

| ErrOther { pos :: SrcSpan
, msg :: !Doc
Expand Down Expand Up @@ -1061,6 +1066,11 @@ ppError' _ dCtx (ErrPosTyCon _ tc dc)
, nest 2 "https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check"
]

ppError' _ dCtx (ErrCtorRefinement _ ctorName)
= text "Refinement of the constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type"
$+$ dCtx
$+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?")

ppError' _ dCtx (ErrParseAnn _ msg)
= text "Malformed annotation"
$+$ dCtx
Expand Down
4 changes: 3 additions & 1 deletion tests/benchmarks/cse230/src/Week10/ProofCombinators.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,9 @@ _ *** _ = ()
data QED = Admit | QED

{-@ measure isAdmit :: QED -> Bool @-}
{-@ Admit :: {v:QED | isAdmit v } @-}
isAdmit :: QED -> Bool
isAdmit Admit = True
isAdmit QED = False


-------------------------------------------------------------------------------
Expand Down
14 changes: 14 additions & 0 deletions tests/neg/RefCtor.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
{-# LANGUAGE GADTs #-}
{-@ LIQUID "--expect-any-error" @-}
module RefCtor where

import Language.Haskell.Liquid.ProofCombinators

{-@ type K X Y = { _:F | X = Y } @-}

data F where
{-@ MkF :: x:Int -> y:Int -> K x y @-}
MkF :: Int -> Int -> F

{-@ falseProof :: { false } @-}
falseProof = () ? MkF 0 2
2 changes: 0 additions & 2 deletions tests/pos/CountMonad.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ module CountMonad () where

{-@ measure count :: Count a -> Int @-}

{-@ Count :: x:a -> {v:Count a | v == Count x } @-}
data Count a = Count a

instance Functor Count where
Expand Down Expand Up @@ -36,7 +35,6 @@ assertCount _ x = x
getCount :: Count a -> Int
getCount _ = 0

{-@ makeCount :: x:a -> {v:Count a | v == Count x} @-}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this not true anymore? I would expect it to remain valid.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is still true bout you need --exact-data-cons or some other flag that triggers it

makeCount = Count

{-@ assume incr :: a -> {v:Count a | count v == 1 } @-}
Expand Down
1 change: 1 addition & 0 deletions tests/tests.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1297,6 +1297,7 @@ executable unit-neg
, Record0
, RecQSort
, RecSelector
, RefCtor
, RefinedProp
, Revshape
, ReWrite2
Expand Down
Loading