Skip to content

Develop workflow to support safe use of -infer-types-for-undefs by enforcing review of inferred declarations #698

Open
@mattmccutchen-cci

Description

@mattmccutchen-cci

Currently, -infer-types-for-undefs is useful for our experiments, but for it to be useful to a user who actually wants spatial memory safety, they need a workflow to ensure that all the inferred declarations of undefined functions actually get reviewed for soundness with respect to the external implementations. In a typical case, the user will have copied the external library headers into a subdirectory of the base directory, so that's the only subdirectory that should have undefined functions, and the user can focus on reviewing it. But if there's a declaration of an undefined function anywhere else in writable code (due to some special case in how the user's code is set up to interact with other external libraries?), 3C might infer a type for it and the user might not notice. I don't know how common this is in real-world programs, but it seems it could be a significant safety risk.

Some ideas for a solution:

  1. Have a flag that limits -infer-types-for-undefs to specified subdirectories under the base directory.
  2. Every time 3C infers types for an undefined function, have it insert some artificial code construct that isn't allowed in a checked scope adjacent to the declaration (maybe just an undefined global variable with an unchecked type, assuming we have a way to exclude that variable itself from -infer-types-for-undefs). The user would remove each of these constructs when they review the adjacent declaration. Then the user would be forced to review all the declarations before they could mark the file #pragma CHECKED_SCOPE on; effectively, they would be tracked like any other unchecked code.

While (1) at least helps contain the problem, it still relies on the user to follow some additional process to track what has been reviewed (possibly involving version control and/or their normal code review process). If a user is in a hurry to get to an approximation of what the Checked C code should ultimately be, they would be tempted to neglect that process. (2) is more foolproof, so I lean toward it. But even if we have (2), it could be useful to additionally have (1) to help stop 3C from making unexpected changes that would take more work for the user to revert later.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions