Detect unsound behavior

[jprider63]

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]

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

[ranjitjhala]

This would be amazing thanks James!!

…

On Mon, Dec 16, 2019 at 7:01 AM Niki Vazou ***@***.***> 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 <#1576?email_source=notifications&email_token=AAMS4OA4J67ZZ43SH3HO7GDQY6J2DA5CNFSM4J3LFXBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEG67ORA#issuecomment-566097732>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OHUGEUEC7JKWLL6CALQY6J2DANCNFSM4J3LFXBA> .

[jprider63]

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]

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 ***@***.***> 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 <#1576?email_source=notifications&email_token=AAMS4OE7H5PHHLEADV7MES3QY75FJA5CNFSM4J3LFXBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEHAJYOA#issuecomment-566271032>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMS4OBJZBQU7RVB5JRJJI3QY75FJANCNFSM4J3LFXBA> .

[jprider63]

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?