Extend and clean up public documentation

[mattmccutchen-cci]

This is a catch-all issue for documentation extensions and cleanups that didn't make the initial submission of the "October 2020" PR to Microsoft (checkedc#930). Some might still be added to that PR if they are done early enough in the review process of the PR, while others will miss it. We can file more specific issues as desired.

• Review the checklist in our main not-yet-public 3C document for more material to add to the public documentation. Some of the most important items:
  • convert_project.py method: is anything from here or clang/tools/3c/utils/{,port_tools/}README.md useful?
  • 3c flags
    • -alltypes: clarify that it means "enable all 3C features that are useful but may cause Checked C type checking failures" and it's just that array bounds inference is currently the only such feature
    • -addcr
    • -debug-solver: needs explanation of how to interpret the output
  • Links to 3C design information
• Workflow in clang/tools/3c/README.md:
  • Include "Actually run the Checked C type checker on your code"?
  • End with "enforce that all files are checked", referencing here? Is there a compiler flag that could be put into the build system rather than having to verify that every file contains this pragma? Research this and file an enhancement request if not.
• Make sure the link from clang/tools/3c/README.md to the tutorial ends up pointing where we want as we revise the tutorial.
• Integrate stuff we wrote that is not specific to 3C into the Checked C documentation (as appropriate)
  • Build instructions
  • Explanation of system headers (wait for Further improvements to installation of Checked C system headers #296 to avoid having to change it again?)
• Update the old reference to 3C on Microsoft's wiki
• As we file GitHub issues for problems mentioned in the new readmes, add links (where appropriate).
• Remove obsolete stuff from correctcomputation/checkedc-clang wiki
• Revise or retire clang/tools/3c/utils/{,port_tools/}README.md
• We've developed a new porting workflow that is much better than the one currently described in our public documentation; for now, we're keeping it private as a potential 5C value-add. Unless and until we document the new workflow publicly, it may be worth adding a mention to the public documentation of the old workflow that users interested in the new workflow should contact us, rather than just hoping users will see the mention of 5C in the general readme.

I hope I got everything...

Other things we have since decided we'd like to add:

• Clarification of the rules for conversions between checked and unchecked pointers in Checked C and 3C

[mwhicks1]

For the first bullet:

• Shilpa's text for Kyle's tutorial is probably the ideal of what to include for that conversion script. But we can/should update the script before we bother to add docs for it (and write the docs accordingly).
• As for -addcr you can say this is an experimental feature that aims to add _Checked annotations on code blocks that should be fully checked. The flag will also insert _Unchecked annotations in some cases, e.g., around variadic function calls, like to printf, which Checked C does not deem as safe.
• For -debug-solver -- this can just be an undocumented feature. It will be too much work to explain the constraint graph, and that graph is in flux anyway.

[mwhicks1]

For the second bullet:

• The sentence "Manually add annotations to help Checked C verify the safety of your existing code" implies that you'll be running Checked C's clang to compile your program, else it cannot verify its safety. Doing so will run its type checker. You could say that explicitly here.
• There's nothing we are going to provide to ensure that the pragma is included. That's a Checked C issue. I don't know the answer to what's the best way (you could ask them).

[mwhicks1]

For the third bullet: The tutorial link is fine as is. Won't change.

For the fourth bullet, on Checked C stuff that is not specific to us; this is low priority. You could file an issue suggesting they include these changes, or else file a PR to their main trunk with the changes, as you like.

For the fifth bullet: File a PR on this (perhaps with the stuff above) ?

For the rest: Nothing specific to add.

[mattmccutchen-cci]

• There's nothing we are going to provide to ensure that the pragma is included. That's a Checked C issue.

Right, I wasn't proposing that 3C do that; I just thought of mentioning it as part of the workflow.