jprider63 commented 4 years ago

I have a bit of time, so I plan to work on this. My plan is to:

Generate a warning when unsafe behavior is encountered. This will happen when:
- Functions in a black list (including undefined) appear in an expression
- Refinements are declared with lazy or assume
This warning will be enabled by default and will have the flags -Wdetect-unsafe and -Wno-detect-unsafe.
I might add a -Werror flag.
I might add an unsafe field to spec files.

Are there other sources of unsoundness I'm not thinking of?

I thought we had an ongoing list of potential improvements, but I couldn't find an existing issue. Perhaps it was only over email/in the proposal.

1339

nikivazou commented 4 years ago

You can also break termination checking when you have negative data type definitions, but this looks more complicated to deted

ranjitjhala commented 4 years ago

This would be amazing thanks James!!

On Mon, Dec 16, 2019 at 7:01 AM Niki Vazou notifications@github.com wrote:

You can also break termination checking when you have negative data type definitions, but this looks more complicated to deted

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1576?email_source=notifications&email_token=AAMS4OA4J67ZZ43SH3HO7GDQY6J2DA5CNFSM4J3LFXBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEG67ORA#issuecomment-566097732, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OHUGEUEC7JKWLL6CALQY6J2DANCNFSM4J3LFXBA .

jprider63 commented 4 years ago

I have some code that works toward checking a blacklist. I'm not sure how to check whether a Var is in the list though. It appears that the name and unique identifier of undefined is being modified. For example, this code generates the following trace output. Do you have any suggestions?

g :: ()
g = undefined

h :: ()
h = let x = undefined in x

[02v]
d2p6: lq_anf$##7205759403792802844
[02v]
d2p8: lq_anf$##7205759403792802846
[02v]
d2pa: lq_anf$##7205759403792802848
[02v]
d2pc: lq_anf$##7205759403792802850
[02v]
d2pe: lq_anf$##7205759403792802852
[02v]
d2pg: lq_anf$##7205759403792802854
[02v]
d2pi: lq_anf$##7205759403792802856
[02v]
d2pk: lq_anf$##7205759403792802858
[02v]
d2pl: lq_anf$##7205759403792802859
[02v]
d2pj: lq_anf$##7205759403792802857
[02v]
d2ph: lq_anf$##7205759403792802855
[02v]
d2pf: lq_anf$##7205759403792802853
[02v]
d2pd: lq_anf$##7205759403792802851
[02v]
d2pb: lq_anf$##7205759403792802849
[02v]
d2p9: lq_anf$##7205759403792802847
[02v]
d2pm: lq_anf$##7205759403792802860
[02v]
d2p7: lq_anf$##7205759403792802845
[02v]
090: GHC.Stack.Types.emptyCallStack
[02v]
d2pp: lq_anf$##7205759403792802863
[02v]
d2pn: lq_anf$##7205759403792802861
[02v]
d2pq: lq_anf$##7205759403792802864
[02v]
a2dv: $dIP_a2dv
[02v]
d2pr: lq_anf$##7205759403792802865
[02v]
d2pt: lq_anf$##7205759403792802867
[02v]
d2pv: lq_anf$##7205759403792802869
[02v]
d2px: lq_anf$##7205759403792802871
[02v]
d2pz: lq_anf$##7205759403792802873
[02v]
d2pB: lq_anf$##7205759403792802875
[02v]
d2pD: lq_anf$##7205759403792802877
[02v]
d2pF: lq_anf$##7205759403792802879
[02v]
d2pG: lq_anf$##7205759403792802880
[02v]
d2pE: lq_anf$##7205759403792802878
[02v]
d2pC: lq_anf$##7205759403792802876
[02v]
d2pA: lq_anf$##7205759403792802874
[02v]
d2py: lq_anf$##7205759403792802872
[02v]
d2pw: lq_anf$##7205759403792802870
[02v]
d2pu: lq_anf$##7205759403792802868
[02v]
d2pH: lq_anf$##7205759403792802881
[02v]
d2ps: lq_anf$##7205759403792802866
[02v]
090: GHC.Stack.Types.emptyCallStack
[02v]
d2pK: lq_anf$##7205759403792802884
[02v]
d2pI: lq_anf$##7205759403792802882
[02v]
d2pL: lq_anf$##7205759403792802885
[02v]
a2cR: $dIP_a2cR
[02v]
d2pM: lq_anf$##7205759403792802886
[02v]
d2pO: lq_anf$##7205759403792802888
[02v]
d2pP: lq_anf$##7205759403792802889
[02v]
d2pN: lq_anf$##7205759403792802887

ranjitjhala commented 4 years ago

Why don't you run with -v and see what the generated core is? It should suffice to check if undefined is in the set of readVars e.g. see uses of this function:

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/src/Language/Haskell/Liquid/Types/Visitors.hs#L43-L44

On Mon, Dec 16, 2019 at 2:19 PM JP notifications@github.com wrote:

I have some code https://github.com/jprider63/liquidhaskell/tree/unsound.jp that works toward checking a blacklist. I'm not sure how to check whether a Var is in the list though. It appears that the name and unique identifier of undefined is being modified. For example, this code generates the following trace output. Do you have any suggestions?

g :: () g = undefined

h :: () h = let x = undefined in x

[02v] d2p6: lq_anf$##7205759403792802844 [02v] d2p8: lq_anf$##7205759403792802846 [02v] d2pa: lq_anf$##7205759403792802848 [02v] d2pc: lq_anf$##7205759403792802850 [02v] d2pe: lq_anf$##7205759403792802852 [02v] d2pg: lq_anf$##7205759403792802854 [02v] d2pi: lq_anf$##7205759403792802856 [02v] d2pk: lq_anf$##7205759403792802858 [02v] d2pl: lq_anf$##7205759403792802859 [02v] d2pj: lq_anf$##7205759403792802857 [02v] d2ph: lq_anf$##7205759403792802855 [02v] d2pf: lq_anf$##7205759403792802853 [02v] d2pd: lq_anf$##7205759403792802851 [02v] d2pb: lq_anf$##7205759403792802849 [02v] d2p9: lq_anf$##7205759403792802847 [02v] d2pm: lq_anf$##7205759403792802860 [02v] d2p7: lq_anf$##7205759403792802845 [02v] 090: GHC.Stack.Types.emptyCallStack [02v] d2pp: lq_anf$##7205759403792802863 [02v] d2pn: lq_anf$##7205759403792802861 [02v] d2pq: lq_anf$##7205759403792802864 [02v] a2dv: $dIP_a2dv [02v] d2pr: lq_anf$##7205759403792802865 [02v] d2pt: lq_anf$##7205759403792802867 [02v] d2pv: lq_anf$##7205759403792802869 [02v] d2px: lq_anf$##7205759403792802871 [02v] d2pz: lq_anf$##7205759403792802873 [02v] d2pB: lq_anf$##7205759403792802875 [02v] d2pD: lq_anf$##7205759403792802877 [02v] d2pF: lq_anf$##7205759403792802879 [02v] d2pG: lq_anf$##7205759403792802880 [02v] d2pE: lq_anf$##7205759403792802878 [02v] d2pC: lq_anf$##7205759403792802876 [02v] d2pA: lq_anf$##7205759403792802874 [02v] d2py: lq_anf$##7205759403792802872 [02v] d2pw: lq_anf$##7205759403792802870 [02v] d2pu: lq_anf$##7205759403792802868 [02v] d2pH: lq_anf$##7205759403792802881 [02v] d2ps: lq_anf$##7205759403792802866 [02v] 090: GHC.Stack.Types.emptyCallStack [02v] d2pK: lq_anf$##7205759403792802884 [02v] d2pI: lq_anf$##7205759403792802882 [02v] d2pL: lq_anf$##7205759403792802885 [02v] a2cR: $dIP_a2cR [02v] d2pM: lq_anf$##7205759403792802886 [02v] d2pO: lq_anf$##7205759403792802888 [02v] d2pP: lq_anf$##7205759403792802889 [02v] d2pN: lq_anf$##7205759403792802887

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1576?email_source=notifications&email_token=AAMS4OE7H5PHHLEADV7MES3QY75FJA5CNFSM4J3LFXBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEHAJYOA#issuecomment-566271032, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OBJZBQU7RVB5JRJJI3QY75FJANCNFSM4J3LFXBA .

jprider63 commented 4 years ago

undefined is in the generated core. For some reason, its Unique doesn't match what is in PrelNames.undefinedKey though. We see rt instead of 02v. For now, I've switched to a string comparison hack, but I'll keep investigating.

Besides this hack, most of the functionality is working in my branch. This is what needs to be improved:

Don't use strings comparison for blacklist check
Figure out how to use single dash arguments with cmdargs (so that it mimics GHC more closely)
Improve formatting of warning printing
Improve contents of warning messages.
- How do I get source spans?
- I'm currently generating the warnings in Language.Haskell.Liquid.GHC.Interface.processTargetModule. Is this the best place to do so?

ucsd-progsys / liquidhaskell

Detect unsound behavior #1576

1339