On Sat, Nov 18, 2017 at 05:14:28PM +0100, Stefan Esser wrote: > Am 18.11.17 um 16:01 schrieb Pedro Giffuni: > > Hi; > > > > On 11/18/17 09:15, Stefan Esser wrote: > >> Am 18.11.17 um 03:31 schrieb Pedro Giffuni: > >>>> On Nov 17, 2017, at 20:34, Rodney W. Grimes > >>>> <free...@pdx.rh.cn85.dnsmgr.net> wrote: > >>>> > >>>> [ Charset UTF-8 unsupported, converting... ] > >>>>> Kib@ posted to arch that we were removing it, nobody objected, we > >>>>> removed > >>>>> it. If it was a working feature that might have a few users, that's one > >>>>> thing. But I don't think make lint has actually worked in at least a > >>>>> decade. > >>>> Thats a sad state of affairs. > >>>> > >>> t?s not sad, just the way things are, modern compilers are doing much of > >>> the checking older tools like lint used to do.. OpenBSD and DragonflyBSD > >>> both killed lint ages ago. > >>> > >>> OTOH, we should probably consider other tools, like sparse: > >>> > >>> https://sparse.wiki.kernel.org/index.php/Main_Page > >>> ? The license is fine and it plays nice with the compiler. > >> It builds on -CURRENT, but the Makefile needs some tweaks (it does > >> not find LLVM or Gtk+-2.0, even though they are present on my system). > >> > >> I'll work on a port over the weekend ... > > > > Thanks! > > I've got a port that builds all of sparse except sparse-llvm. The sources > use GNU extensions, and I do not think it is worth the effort to provide > standard compliant replacements for them at this time. > > Building sparc?se-llvm will take some more effort and require the LLVM port > to be installed, since it references headers not installed by our system > compiler. It is an optional component, but one we definitely should have. > > I'm not sure how to proceed, but the easiest path forward is to make the > LLVM support optional and depend on one particular LLVM version (i.e. 4.0 > for now) built from a port if the option is enabled. > > > For it to be really useful we still would have to add annotations to the > > kernel headers. > > Well, those could be added over time ... > > > I just resurrected a recent proposal from brooks@ into the IdeasPage: > > > > https://wiki.freebsd.org/IdeasPage#Userspace_Address_Space_Annotation > > > > It is actually a fun project but my hands are full! > > The port was easy, so far, I'll commit it without sparse-llvm for now. > LLVM support will follow when I've got the remaining build issues resolved.
I wrote up a port a month or so ago, but I didn't commit it because I belive they authors of sparse failed to understand how C qualifiers work and the __user annotations used in linux are harmful as a result. The problem is that they annotate the data not the pointer. You can make a case for this for the address space annotations, but I believe it's completely wrong for the anti-derefernce guards. I'd hoped that that the linux style __user annotations would be a good match for the __capability annotations we use in CHERI to denote pointers that are capabilities (fat pointers), but they aren't usable. This makes me sad, but I will object to adding these annotations to our tree. (Some of the other annotations look ok, but I've not tested further after this disappointment.) -- Brooks
signature.asc
Description: PGP signature