xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
170 stars 3 forks source link

Detect reliance on unspecified order of subexpression side effects #54

Open jorendorff opened 1 month ago

jorendorff commented 1 month ago

In Xr0, function arguments are evaluated in order.

The C standard allows compilers to evaluate arguments in any order. I think they often run in reverse order.

Here is an example that Xr0 allows, but according to standard C is undefined behavior, because f(use(p), free_ptr(p)); may call free_ptr before use, invalidating p.

#include <stdlib.h>

int
use(int *p) ~ [
    setup: { p = malloc(sizeof(int)); *p = $; }
    return *p;
] {
    return *p;
}

int
free_ptr(int *p) ~ [
    setup: p = malloc(sizeof(int));
    free(p);
    return 0;
] {
    free(p);
    return 0;
}

int
f(int x, int y)
{
    return 0;
}

int
main()
{
    int *p;

    p = malloc(sizeof(int));
    *p = 0;
    f(use(p), free_ptr(p)); // possible use after free

    return 0;
}

As it happens, GCC compiles this so that use is called after free. https://godbolt.org/z/bv8Y9ve6E

akiarie commented 1 month ago

Yes. Interestingly the Standard addresses this in two paragraphs within the same section (3.3):

Between the previous and next sequence point an object shall have its stored value modified at most once by the evaluation of an expression. Furthermore, the prior value shall be accessed only to determine the value to be stored.

Except as indicated by the syntax or otherwise specified later (for the function-call operator () , && , || , ?: , and comma operators), the order of evaluation of subexpressions and the order in which side effects take place are both unspecified.

So there are technically two rules in play here:

  1. The order of evaluation of subexpressions and their side effects are unspecified
  2. It is undefined behaviour to modify the value of an object twice within the span between two subsequent sequence points.

A first solution here may be to track in the state when an object has been modified, and to refresh this tracking with each sequence point. Then if a second modification occurs (in violation of (2.)) Xr0 should reject this as undefined behaviour. Also, if there is a modification there should be no "read" operation like in use above, which would constitute unspecified behaviour according to (1.).

I think this would address the issue — thoughts?

jorendorff commented 1 month ago

Note that the wording of the rule about unsequenced side effects has changed in more recent C standards. See paragraph 2 of section 6.5 of C23.

Anyway, I don't think that rule is in play here, because

See paragraph 2 of [section 6.5.2.2](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3096.pdf#subsubsection.6.5.2.2 of C23). "Indeterminately sequenced" is defined in paragraph 3 of section 5.1.2.3.

Rather, the problem is just that this code can do a use-after-free, which is UB by other rules.

jorendorff commented 1 month ago

A first solution here may be to track in the state when an object has been modified, and to refresh this tracking with each sequence point. Then if a second modification occurs (in violation of (2.)) Xr0 should reject this as undefined behaviour. Also, if there is a modification there should be no "read" operation like in use above, which would constitute unspecified behaviour according to (1.).

It might be too strict. A function like total = f1() + f2() + f3() is allowed in C, even if the functions have side effects to the same global variable. The actions of f1() are sequenced relative to the other two functions, but in an unspecified order.

akiarie commented 1 month ago

So the situation is indeed more subtle than I realised. We've been working off the C89 Standard exclusively as a first step, but it's worth recognising such changes as you've noted, to give us foresight for when we begin to support the newer (and more complicated) standards.

The C11 Standard (I assume due to multithreading support) seems to be the one where the wordings were changed the most substantially with respect to the sequencing rules. The paragraph which appears to be the most significant addition is this one 6.5.2.2p10:

There is a sequence point after the evaluations of the function designator and the actual arguments but before the actual call. Every evaluation in the calling function (including other function calls) that is not otherwise specifically sequenced before or after the execution of the body of the called function is indeterminately sequenced with respect to the execution of the called function.

Taken together with the definition of "indeterminately sequenced", this is a marked change to the semantics of the call expression, because previously (in light of 6.5p3) the operating assumption would've been that there is no defined sequencing between the subexpressions of a call expression, whereas with this amendment there is a guarantee of sequencing, albeit of the indeterminate kind. In other words, if my interpretation is correct, previously

f1(f2(), f3())

would've been UB if f2() and f3() both modify the same object, but with the amendment this is now unspecified behaviour with the potential of UB only if something like a use-after-free occurs as a consequence.

That notwithstanding, it seems to me that

f1() + f2()

is still UB if the functions have side effects for the same object because, crucially, this is only an additive expression, and there is no sequencing defined for its operands, so the default rule 6.5p3 should apply. (The same seems to hold for C23.)

akiarie commented 1 month ago

A strictly conforming program shall use only those features of the language and library specified in this Standard. It shall not produce output dependent on any unspecified, undefined, or implementation-defined behavior, and shall not exceed any minimum implementation limit.

Returning to the question of solutions, it does seem reasonable to disallow multi-modification[^1] to the same object within the span of a single expression (apart from with the exceptional expressions like &&, ||, etc. that have some defined sequencing from C89 going forward) because it could only be used to produce a program that is not "strictly conforming". Even for C11 going forward, although an expression like

f(++a, a)

is not technically UB, it's impossible to say with certainty what value will be given as the second argument — and it seems risky to allow this.

[^1]: Multi-modification and also simultaneous modification and read.

jorendorff commented 1 month ago

if my interpretation is correct, previously f1(f2(), f3()) would've been UB if f2() and f3() both modify the same object, but with the amendment this is now unspecified behaviour with the potential of UB only if something like a use-after-free occurs as a consequence.

That sounds right. At least, I won't dig into C89 to try and prove you wrong!

I'm sure C programs have "always" used expressions like this, though, so I think of the new wording as more of a correction of the standard (to align with what compilers and users were already doing) than an actual language change.

That notwithstanding, it seems to me that f1() + f2() is still UB if the functions have side effects for the same object [...]

I don't think so, because of this rule:

Every evaluation in the calling function (including other function calls) [...] is indeterminately sequenced with respect to the execution of the called function.

So everything else in the calling function, the one that says f1() + f2(), is indeterminately sequenced with respect to the execution of the called function f1. That explicitly includes the other function call, f2().

jorendorff commented 1 month ago

Even for C11 going forward, although an expression like f(++a, a) is not technically UB [...]

I believe it is UB. In C23 (emphasis mine):

If a side effect on a scalar object is unsequenced relative to either a different side effect on the same scalar object or a value computation using the value of the same scalar object, the behavior is undefined.

The write in ++a is unsequenced relative to the other a "using the value of" the same object.

It was also UB in C89: "the prior value shall be accessed only to determine the value to be stored." But the second a accesses this value, and not to determine the value to be stored in the first ++a.

jorendorff commented 1 month ago

All this took me forever to get straight. The standard is not super clear.

akiarie commented 1 month ago

I don't think so, because of this rule:

Every evaluation in the calling function (including other function calls) [...] is indeterminately sequenced with respect to the execution of the called function.

Hmmmm. I think you're right, but it is definitely poorly worded. I was reasoning about it as though this rule applies only to call expressions, but it is universal, "every". So the fact that f1() + f2() is an additive expression whereas f1(f2(), f3()) is a call one seemed to indicate that the rule only applied to the latter one.

akiarie commented 1 month ago

I agree also that

f(++a, a)

is UB. I was misreading the rule

Every evaluation in the calling function (including other function calls) that is not otherwise specifically sequenced before or after the execution of the body of the called function is indeterminately sequenced with respect to the execution of the called function.

and thinking that it meant that all subexpressions of a call are indeterminately sequenced, but it only says that expressions in the calling function are indeterminately sequenced wrt to the execution of the called function. So the evaluation of ++a and a is indeterminately sequenced wrt to the call to f, but that of ++a is unsequenced wrt to that of a.

akiarie commented 1 month ago

Returning to this:

It might be too strict. A function like total = f1() + f2() + f3() is allowed in C, even if the functions have side effects to the same global variable.

I'm thinking also that we could disallow multi-modification and modification-plus-read within a single expression for certain classes of pointer-related operations alone, and this would prevent UB at least in the example you provided.

It would take some effort to enumerate these cases carefully, but it's very much finite. Anything that makes a pointer valid (dereference-able), like assigning an address to it; or anything that makes it invalid, like freeing an address it's pointed at or assigning a different value to it — anything in one of these two classes will lead to UB if it occurs with another operation.

Restricting these cases seems to me to deal with the UB without curtailing the abilities that a programmer has under the Standard.

Thoughts?

akiarie commented 1 month ago

To be a bit more concrete, expanding on the theme of your example:

#include <stdlib.h>

int
assign_addr(int **p, int *q) ~ [
    setup: p = .clump(sizeof(int *));
    *p = q;
    return 0;
]{
    *p = q;
    return 0;
}

int
assign_alloc(int **p) ~ [
    setup: p = .clump(sizeof(int *));
    *p = malloc(sizeof(int));
    *p = 1;
    return 0;
]{
    *p = malloc(sizeof(int));
    *p = 1;
    return 0;
}

int
free_ptr(int *p) ~ [
    setup: p = malloc(sizeof(int));
    free(p);
    return 0;
]{
    free(p);
    return 0;
}

void
side_effect(int *p, int k) ~ [
    setup: p = .clump(sizeof(int));
    *p = k;
]{
    *p = k;
}

int
f(int x, int y)
{
    return 0;
}

void
main1()
{
    int *p;

    f(use(p), free_ptr(p)); /* possible use after free */
}

void
main2()
{
    int k;
    int *p;

    k = 0;
    f(assign_addr(&p, &k), *p); /* possible use of uninitialised value */
}

void
main3()
{
    int *p;

    f(assign_alloc(&p), *p); /* possible use of uninitialised value */
}

void
main4()
{
    int k;
    int *p;
    p = &k;
    f(side_effect(p, 1), side_effect(p, 2)); /* safe (albeit unpredictable) */
}

So disallowing what occurs in main1, main2 and main3 seems to be all that is required. main4 is weird but technically permissible.

The algorithm to do this can be fairly simple — track when an object undergoes one of these constructive/destructive operations in an expression and require that it remain untouched by the rest of the subexpressions.

jorendorff commented 1 month ago

That approach would catch many problems, but the unpredictable cases are still trouble. Xr0 must check every state that can be reached in actual execution. Even if the expression is safe, if it leaves Xr0 in one state, but compiled code in a different state, subsequent code can do things Xr0 didn't check.

For example:

void g(int x, int y) {}

void
f()
{
    int k;
    int *p;

    g(k = 1, k = 0); /* UB: unsequenced writes */
    if (k)
        *p = 0; /* possible use of uninitialized variable p */
}

Xr0 currently allows this. I think it skips the body of the if-statement because it thinks k is definitely zero.

jorendorff commented 1 month ago

In the above test case, I guess Xr0 could simply detect that the unsequenced writes are UB. But those assignments could happen in other functions:

int set(int *p) ~ [ setup: *p = .clump(1); *p = 1; ] { *p = 1; }
int clear(int *p) ~ [ setup: *p = .clump(1); *p = 0; ] { *p = 0; }

void
f()
{
    int k;
    int *p;

    g(set(&k), clear(&k)); /* OK: indeterminately sequenced writes */
    if (k)
        *p = 0; /* possible use of uninitialized variable p */
}

To detect this bug correctly, Xr0 needs to determine that k might be nonzero.

akiarie commented 1 month ago

I think (esp. with the last example) the bug is Xr0's failure to detect that there are two possible values for k after the call. If it recognises this and has its value in the state as either 0 or 1 then it would split on the if-condition, and throw an error.

So another way it can be solved is simply by detecting the possible range of values that results from the unpredictability.

Edit: This is really a variant of

Xr0 must check every state that can be reached in actual execution.

akiarie commented 1 month ago

To avoid the O(n!) which would result from examining every possible path, all that Xr0 needs to do is to represent the multi-assignments as expanding the range of values. So as it loops through the arguments instead of overwriting k's value above it should augment it. That would be O(n) and I think we can do this soon.

claude-betz commented 1 month ago

Renaming since this is more general than the order of arguments. As an example we should also handle cases like:

a[i++] = i - 1;