Page MenuHomeFreeBSD
Differential D14285

Added SAL annotatations to system calls
ClosedPublic
Actions

Authored by talg_cs.stanford.edu on Feb 9 2018, 7:36 PM.
Tags
None
Referenced Files
Unknown Object (File)
Sat, Dec 21, 1:28 AM
Unknown Object (File)
Mon, Dec 16, 5:51 PM
Unknown Object (File)
Wed, Dec 11, 6:39 AM
Unknown Object (File)
Fri, Dec 6, 10:08 PM
Unknown Object (File)
Fri, Dec 6, 10:08 PM
Unknown Object (File)
Fri, Dec 6, 10:06 PM
Unknown Object (File)
Mon, Dec 2, 7:16 AM
Unknown Object (File)
Mon, Nov 25, 12:58 PM
View All Files
Subscribers
ali_mashtizadeh.com
cem
emaste
imp
jhb
lwhsu

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
Repository 
rS FreeBSD src repository - subversion 
Lint 
Lint Not Applicable
 
Unit 
Tests Not Applicable
 
Event Timeline
There are a very large number of changes, so older changes are hidden. Show Older Changes
talg_cs.stanford.edu updated this revision to Diff 39890.Mar 2 2018, 6:35 PM
    

  • added missing annotations for send and recv.
    • 

cem accepted this revision.Mar 3 2018, 5:55 AM
cem added a subscriber: cem.
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
cem added a comment.Mar 3 2018, 5:56 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
jhb added a subscriber: jhb.Mar 5 2018, 6:24 PM
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.
emaste added a comment.Mar 5 2018, 6:47 PM


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.
talg_cs.stanford.edu updated this revision to Diff 39978.Mar 5 2018, 10:03 PM
    

  • added annotatations for gethostname, sethostname, revoke, pathconf.
    • 

This revision now requires review to proceed.Mar 5 2018, 10:03 PM
talg_cs.stanford.edu updated this revision to Diff 39979.Mar 5 2018, 10:25 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
brooks added a comment.Mar 5 2018, 10:53 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.
talg_cs.stanford.edu added a comment.Mar 5 2018, 11:28 PM


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


534 ↗(On Diff #39104)
drop this comment


946 ↗(On Diff #39104)
drop |STD


1080 ↗(On Diff #39104)
TMI?
ali_mashtizadeh.com added a subscriber: ali_mashtizadeh.com.Mar 7 2018, 6:40 PM
talg_cs.stanford.edu updated this revision to Diff 40046.Mar 7 2018, 7:43 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
talg_cs.stanford.edu updated this revision to Diff 40051.Mar 7 2018, 10:10 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
talg_cs.stanford.edu updated this revision to Diff 40052.Mar 7 2018, 10:20 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
talg_cs.stanford.edu updated this revision to Diff 40054.Mar 7 2018, 10:42 PM
    

  • tiny wording change in documentation.
    • 

Harbormaster completed remote builds in B15420: Diff 40054.Mar 7 2018, 10:42 PM
talg_cs.stanford.edu updated this revision to Diff 40055.Mar 7 2018, 10:43 PM
    

  • replaced tab with spaces for uniform formatting.
    • 

Harbormaster completed remote builds in B15421: Diff 40055.Mar 7 2018, 10:43 PM
talg_cs.stanford.edu updated this revision to Diff 40062.EditedMar 8 2018, 1:08 AM
-rebased against latest HEAD.
Harbormaster completed remote builds in B15428: Diff 40062.Mar 8 2018, 1:08 AM
talg_cs.stanford.edu added a comment.Mar 8 2018, 1:11 AM
If everyone is happy with the documentation and new annotations I think this is ready to land.
talg_cs.stanford.edu updated this revision to Diff 40092.Mar 9 2018, 12:09 AM
    

  • 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
brooks added a comment.Mar 15 2018, 12:14 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 ↗(On Diff #40092)
Don't make unrelated changes in this diff.


95 ↗(On Diff #40092)
I'd leave this comment in.


193 ↗(On Diff #40092)
I think we should infact go with _In_z_ here.  I now believe it's the correct usage.


609 ↗(On Diff #40092)
This comment was incorrectly restored.


623 ↗(On Diff #40092)
this one too.


1080 ↗(On Diff #39104)
We can remove this comment.
talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 16 2018, 7:28 PM
talg_cs.stanford.edu updated this revision to Diff 40356.EditedMar 16 2018, 8:08 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
brooks added a comment.Mar 22 2018, 10:44 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


141 ↗(On Diff #40356)
Wrong indention and several other places.  Continuing definitions should all be indented with <tab><tab><tab><tab><space><space><space><space>


242 ↗(On Diff #40356)
Looks like a NOPARSE slipped through from CheriBSD


243 ↗(On Diff #40356)
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?


276 ↗(On Diff #40356)
Not an issue with the change, but this isn't quite true to reality.  Some programs allocate truncated fd_sets and the kernel needs to cope with this.  Such programs shouldn't almost certainly use poll.


286 ↗(On Diff #40356)
missing space before \


322 ↗(On Diff #40356)
msg is a pointer and requires annotation.  Other unannotated caddr_ts exist (at least recvfrom at 125)


402 ↗(On Diff #40356)
extra space before comma


641 ↗(On Diff #40356)
missing annotation.


742 ↗(On Diff #40356)
no need to split this line.
talg_cs.stanford.edu updated this revision to Diff 40622.Mar 23 2018, 12:44 AM
    

  • formatting fixed a few missing annotations added.
    • 

Harbormaster completed remote builds in B15731: Diff 40622.Mar 23 2018, 12:44 AM
talg_cs.stanford.edu updated this revision to Diff 40623.Mar 23 2018, 12:46 AM
    

  • removed line break.
    • 

Harbormaster completed remote builds in B15732: Diff 40623.Mar 23 2018, 12:46 AM
talg_cs.stanford.edu updated this revision to Diff 40626.Mar 23 2018, 1:01 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
talg_cs.stanford.edu added a comment.Mar 23 2018, 1:04 AM
sorry about dribbling in the last set of fixes. that should address all the issues raised.
sys/kern/syscalls.master


243 ↗(On Diff #40356)
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.
brooks updated this revision to Diff 40649.Mar 23 2018, 9:03 PM
    

  • rebase
    • 

  • Whitespace fixes.
    • 

Harbormaster completed remote builds in B15743: Diff 40649.Mar 23 2018, 9:03 PM
brooks updated this revision to Diff 40650.Mar 23 2018, 9:04 PM
    

  • Fix getrandom annotation syntax.
    • 

Harbormaster completed remote builds in B15744: Diff 40650.Mar 23 2018, 9:04 PM
brooks updated this revision to Diff 40651.Mar 23 2018, 9:06 PM
    

  • Fix getrandom() whitespace.
    • 

Harbormaster completed remote builds in B15745: Diff 40651.Mar 23 2018, 9:06 PM
brooks added a comment.Mar 23 2018, 9:07 PM
This could probably use another review with fresh eyes for whitespace and missing annotations, but I think it's otherwise ready to land.
brooks added a reviewer: emaste.Mar 26 2018, 8:12 PM
brooks mentioned this in D14858: arm64 linuxulator syscalls.master style review.Mar 26 2018, 11:46 PM
brooks accepted this revision.Mar 30 2018, 8:35 PM
I'm sending out a final call for objections to freebsd-arch and plan to commit early next week.
This revision is now accepted and ready to land.Mar 30 2018, 8:35 PM
brooks edited the summary of this revision. (Show Details)Apr 5 2018, 8:28 PM
Closed by commit rS332086: Added SAL annotatations to system calls. (authored by brooks).  ·  Explain WhyApr 5 2018, 8:32 PM
This revision was automatically updated to reflect the committed changes.
Herald added a subscriber: imp.  ·  View Herald TranscriptApr 5 2018, 8:32 PM
Revision Contents
Changeset List
PathSize
head/
sys/
kern/
10 lines
1311 lines
Diff 41151
View Options
head/sys/kern/makesyscalls.sh
Loading...
View Options
head/sys/kern/syscalls.master
Loading...