Details

Reviewers

theraven
brooks
cem
emaste

Commits

rS332086: Added SAL annotatations to system calls.

Summary

Add SAL annotatations to most system calls declarations (STD, NOSTD, COMPAT*) in
syscalls.master.

Modify makesyscalls.sh to strip out SAL annotations.

This is based on work I started in CheriBSD and use to validate fat
pointers at the syscall boundary. Tal Garfinkel reviewed the changes,
added annotations to COMPAT* syscalls and is using them in a record and
playback framework. One can envision other uses such as a WITNESS-like
validator for copyin/out as speculated on in the review.

As this time we are only annotating sys/kern/syscalls.master as that is
sufficient for userspace work. If kernel use cases materialize, we can
annotate other syscalls.master as needed.

Submitted by: Tal Garfinkel <talg@cs.stanford.edu>
Sponsored by: DARPA, AFRL (in part)

Test Plan

Running make sysent and looking at git status to ensure that the changes
have not impacted output of makesyscalls.sh.

Diff Detail

Lint

Lint Passed

Unit

No Test Coverage

Build Status

Buildable 15419
Build 15468: arc lint + arc unit

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes

added missing annotations for send and recv.

Seems fine in principle. I haven't audited the entire table for correctness. It would be good to document the available annotations and what they mean somewhere (a manual page?).

This revision is now accepted and ready to land.Mar 3 2018, 5:55 AM

Keep in mind the compat32 and Linux syscall tables could benefit from a very similar treatment.

emaste added a subscriber: emaste.Mar 4 2018, 2:01 AM

I think some sort of reference to what SAL annotations are and where they are defined would be useful, probably in the commit message, but possibly also in the leading comment block of syscalls.master itself.

In D14285#306247, @jhb wrote:

I think some sort of reference to what SAL annotations are and where they are defined would be useful, probably in the commit message, but possibly also in the leading comment block of syscalls.master itself.

I'd argue for having the reference in the comment block.

added annotatations for gethostname, sethostname, revoke, pathconf.

This revision now requires review to proceed.Mar 5 2018, 10:03 PM

Added a note about SAL annotations to header comments re: emaste and jhb's comments.

Harbormaster completed remote builds in B15383: Diff 39979.Mar 5 2018, 10:25 PM

I think it would be good to describe at least _In_, _Inout_, _Out_, and _opt_ annotation components not just that they are SAL 2.0 annotations since SAL doesn't google very well.

In D14285#306357, @brooks wrote:

I think it would be good to describe at least _In_, _Inout_, _Out_, and _opt_ annotation components not just that they are SAL 2.0 annotations since SAL doesn't google very well.

I might as well describe them all. Given that we use such a small subset of SAL it will probably be much easier for future readers.

sys/kern/syscalls.master
565	drop this comment
972	drop \|STD
1107	TMI?

ali_mashtizadeh.com added a subscriber: ali_mashtizadeh.com.Mar 7 2018, 6:40 PM

Added documentation for annotations to header comment block.

Harbormaster completed remote builds in B15414: Diff 40046.Mar 7 2018, 7:43 PM

talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 7 2018, 7:44 PM

-added annotations for remaining calls of type COMPAT and STD for consistency/completeness.

Harbormaster completed remote builds in B15418: Diff 40051.Mar 7 2018, 10:10 PM

fixed incorrect annotation for cpuset_getdomain.

Harbormaster completed remote builds in B15419: Diff 40052.Mar 7 2018, 10:20 PM

talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 7 2018, 10:23 PM

tiny wording change in documentation.

Harbormaster completed remote builds in B15420: Diff 40054.Mar 7 2018, 10:42 PM

replaced tab with spaces for uniform formatting.

Harbormaster completed remote builds in B15421: Diff 40055.Mar 7 2018, 10:43 PM

-rebased against latest HEAD.

Harbormaster completed remote builds in B15428: Diff 40062.Mar 8 2018, 1:08 AM

If everyone is happy with the documentation and new annotations I think this is ready to land.

Added SAL annotations for COMPAT11 syscalls.

Harbormaster completed remote builds in B15445: Diff 40092.Mar 9 2018, 12:09 AM

talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 9 2018, 12:10 AM

Some general comments:

NOSTD syscalls should definitely be annotated as they are current.
I think it would be best if the remaining COMPAT* ones were annotated as well.
When I look at the patched file in an editor, I see quite a few lines that extend beyond 80 columns. That should be fixed for lines that are newly too long. I know some of those are my fault...

sys/kern/syscalls.master
25	Don't make unrelated changes in this diff.
95	I'd leave this comment in.
193	I think we should infact go with `_In_z_` here. I now believe it's the correct usage.
611–617	This comment was incorrectly restored.
624	this one too.
1107	We can remove this comment.

talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 16 2018, 7:28 PM

addresses brook's comments.
adds annotations for COMPAT* i.e. COMPAT10,7,...
adds annotations for NOSTD calls
reformats everything to not exceed 80 columns.
adds/removes some comments.
also fixes annotation for pwrite

Harbormaster completed remote builds in B15601: Diff 40356.Mar 16 2018, 8:08 PM

This is getting close. In addition to (hopefully small) issues I've noted, another rebase is needed because getrandom has been added and needs annotation.

sys/kern/syscalls.master
134	Wrong indention and several other places. Continuing definitions should all be indented with <tab><tab><tab><tab><space><space><space><space>
230	Looks like a NOPARSE slipped through from CheriBSD
231	missing annotation on `addr`. That being said, there doesn't really seem to be a valid SAL annotation for the `addr` arguments of the `mmap` family. I'm not sure if we should use `_In_` somewhat misleadingly or use something else like I did in CheriBSD. What does your framework need to know about these addresses?
258	Not an issue with the change, but this isn't quite true to reality. Some programs allocate truncated `fd_set`s and the kernel needs to cope with this. Such programs shouldn't almost certainly use poll.
268–269	missing space before `\`
302	`msg` is a pointer and requires annotation. Other unannotated `caddr_t`s exist (at least recvfrom at 125)
376	extra space before comma
597	missing annotation.
689	no need to split this line.

formatting fixed a few missing annotations added.

Harbormaster completed remote builds in B15731: Diff 40622.Mar 23 2018, 12:44 AM

removed line break.

Harbormaster completed remote builds in B15732: Diff 40623.Mar 23 2018, 12:46 AM

-rebased against master to pull in getrandom and added annotation.

Harbormaster completed remote builds in B15735: Diff 40626.Mar 23 2018, 1:01 AM

sorry about dribbling in the last set of fixes. that should address all the issues raised.

sys/kern/syscalls.master
231	We only care about _Out_* and _Inout_* parameters since we are only recording the results of system calls, not their inputs. So I'm neutral on the topic.