Define the tag "decidability"

[darkwisebear]

Goal

Add a section to https://github.com/rustfoundation/safety-critical-rust-coding-guidelines/blob/main/src/process/style-guideline.rst that defines what the guidelines mean with "decidability", how a writer shall determine what to put there and when, and how a reader can interpret the tag.

Suggested direction

"Decidability" shall be derived from whether a static code analysis tool could determine within the given scope of the guideline.

[darkwisebear]

@felix91gr Here's the issue stub for the definition of decidability.

[felix91gr]

I like this direction. It fits what is usually understood as decidability in Computer Science.

I'd like to expand on it:

Decidability

A guideline is said to be decidable if and only if there is a general algorithm or procedure, which if given an arbitrary piece of code, can always determine if it complies with the guideline or not.

This is equivalent to any and all of the following:

• It is possible to write a static analysis tool which checks that this rule is being held, with no false positives nor false negatives.

• Note to issue readers: add more equivalent definitions here

What to do when rules are not decidable

In general, static analysis is known to not be decidable.

Note to issue readers: this is a laborious proof, which I haven't touched upon in 4 and a half years, but it is true. Most definitions of "what static analysis is" entail deducing program properties with a procedure that, if it existed, could also be used to solve undecidable problems like the Halting Problem.

This doesn't mean, however, that we can't do anything about a non-decidable rule.

In the worst case scenario, non-decidable rules could only be addressed with manual checking / vetting of the code. But there are two ways in which this manual load can be reduced (or bypassed entirely) for most cases.

Case 1: incomplete (yet still quite helpful) tools

Undecidability only means that a tool cannot do a complete (ie no-false-positives-nor-false-negatives) analysis. But a tool can still be useful, if it is configured properly.

If a rule is undecidable, then an incomplete tool can be made, but tuned in the following way:

• If the tool can prove the rule is being held, then it doesn't trigger (true negative).
• If the tool can prove the rule is not being held, then it triggers (true positive).
• In all other cases, the tool triggers (might be a true positive or a false positive).

In table form, it looks like this:

Code is...	Can prove	Cannot prove
Compliant	Doesn't trigger	Triggers
Not Compliant	Triggers (shows proof)	Triggers

So as to avoid repeated triggering in known false positives, the tool should also include a way to annotate code so as to skip triggering. That way, human vetting of compliance can be documented and used to streamline work.

The table would then look like this:

Code is...	Can prove compliance / not compliance	Cannot prove compliance / not compliance
Annotated to be Compliant	Doesn't trigger	Doesn't trigger
Compliant	Doesn't trigger	Triggers
Not Compliant	Triggers (shows proof)	Triggers

In this way, a workflow can be set up to address undecidable rules:

1. Always run this incomplete tool.
2. If it doesn't trigger, exit this workflow.
3. If it triggers, see why.
   1. If it includes a proof, then the code is not compliant and must be fixed.
   2. If it doesn't, check the code.
      1. If the code is determined to not comply, it must be fixed.
      2. Otherwise, it is annotated as compliant.

Such a workflow can be added to any local static analysis loop, and such a tool can be added to CI as well.

If the tool doesn't trigger, we know the code is compliant.

Case 2: bypass the cause of the problem, and comply by default

An alternative way, and I would say complementary to the case described above, is to bypass the problem. This can sometimes be achieved, by using constructs that achieve the same goal as the guideline in all cases (and are therefore compliant "by construction").

An example of this is how the idea of nullability is handled in Rust, by using Option<T> types. A function that may or may not return the desired result (say, a reference &T) doesn't return a pointer that might be null: it instead returns an Option<&T>. There are two cases here:

• The result is None. We handle this in our program, and we know we will handle it because the compiler won't accept that we ignore it.
• The result is Some(&T). When we open this, we know that the reference is valid.

And this is basically how all dereferences to null are bypassed in Rust.

Instead of "not dereferencing null pointers", which is an undecidable property, references cannot be null in Rust, and the way in which we give and receive fallible references is via Option<T>.

We can use the same approach.

Note to issue readers: I can't think of a general way to find ways to hold a rule by default, so these examples are more like case studies.

Let's take Dividing by Zero and Avoiding Arithmetic Overflow. Both are things we don't want to happen in Safety Critical contexts:

• Dividing by zero will most certainly panic, which in SC tends to be undesirable.
• Arithmetic Overflow will give unreliable results.

Note to issue readers: I mean Arithmetic Overflow and Arithmetic Underflow. They are the same kind of problem, and are addressed in the same ways, but it's a pain to write A. Underflow next to A. Overflow so I'm just writing Arithmetic Overflow instead :)

Determining whether any of them happen is undecidable. However, we can avoid the issue entirely if instead of asking the programmer to "not divide by zero" or "not incur arithmetic overflow", we require them to use checked arithmetic.

In this way, division by zero is statically known to be handled due to the usage of checked_div, and the behavior of other arithmetic operations (such as addition past the maximum value) can be made explicit and handled directly by the usage of methods such as carrying_add.

And thus, we took an undecidable guideline and fulfilled its objectives by replacing it with a decidable one.

[darkwisebear]

@felix91gr Great writeup so far! I really like how we can, for some tasks, improve decidability by imposing restrictions that reduces the amount of undecidable rules by using constructs that make a certain rule decidable. Then the developer actually has two options:

• Either they suppress by stating why the code is fine in this particular case, making the decision on behalf of the static analyzer who cannot proof the correctness or the definitive brokenness of a piece of code
• Or they follow hints in the rule how to turn the piece of code into something decidable.

This means we should actually have more than the binary decidable/non-decidable statement

• Decidable: Code can be analyzed as-is, no false positives or false negatives possible.
• Undecidable: The static analyzer cannot always prove the presence or absence of a certain unwanted state; a human being needs to assess and approve that piece of code.
• Possibly(?) decidable (not sure whether the wording makes sense): Code can/should be adapted, e.g. by adding asserts or other runtime properties, using other constructs or higher level APIs that help the compiler or static analyzer to verify static properties. The rule shall then contain hints and examples how to reshape the code so that it becomes decidable.

We also must not forget to always judge on decidability with the given scope the rule has. I could imagine that some rules will only be checked with a scope that make them undecidable, but on a larger scope (even system) the will become decidable, but it's just impractical or technically impossible to verify a given rule on that scope. So the categories above should still be applied in the given scope.

[PLeVasseur]

Some great discussion here.

I really like the concept of suggesting

adding asserts or other runtime properties, using other constructs or higher level APIs that help the compiler or static analyzer to verify static properties

With regard to a possible new option for decidability:

Possibly(?) decidable (not sure whether the wording makes sense)

My 2c is that the decidability would still be undecidable, however, we could make use of the Exception field and highlight if certain asserts etc. were used this coding guideline is not applicable.

Tagging @AlexCeleste, @rcseacord for their thoughts on this mechanism / concept.