Treatment of local uninitialised variables in AutoCorres and C Parser

[AntanasKal]

While experimenting with AutoCorres we noticed something unexpected in the way the C Parser treats local uninitialised variables when translating to SIMPL. The concrete examples in AutoCorres and AutoCorres2 are bellow.

Example in AutoCorres 1.12

In this example we are using AutoCorres 1.12 with Isabelle2025 and L4V_ARCH=ARM environment variable. Consider the following function:

int bogus(void) {
    int x;
    if (x < 100) {
        return 0;
    } else {
        return 1;
    }
}

If we import this using AutoCorres, we see by inspecting bogus'_def that the abstracted definition of bogus function becomes:

bogus' ≡ do x___int <- unknown;
             return (if x___int < 100 then 0 else 1)
          od

Where unknown is a nondeterministic selector from all integers. As far as we understand, the function in C has undefined behaviour as the local variable x is not initialised and it is accessed in the if statement. Because of this, we would expect that we should not be able to reason about this program. However, with the abstracted definition above we can prove that the function returns 0 or 1:

theory Bogus
imports
  "AutoCorres.AutoCorres"
begin

external_file  "bogus.c"

install_C_file  "bogus.c"

thm Bogus.bogus_global_addresses.bogus_body_def

autocorres "bogus.c"

context bogus begin

thm bogus'_def

lemma bogus_res:
       "⦃ λs. True ⦄
           bogus'
        ⦃ λr _. r = 0 ∨ r = 1 ⦄!"
  apply (unfold bogus'_def)
  apply wp
  by meson

end

end

We can see that the result of translating C to SIMPL is this:

bogus_global_addresses.bogus_body ≡
TRY
  lvar_nondet_init x_' x_'_update;;
  IF ´x <s 0x64 THEN
    creturn global_exn_var_'_update ret__int_'_update (λs. 0)
  ELSE
    creturn global_exn_var_'_update ret__int_'_update (λs. 1)
  FI;;
  Guard DontReach {} SKIP
CATCH SKIP
END

x seems to be initialised as a nondeterministic variable. We would expect there to be some guards before IF statement that prevent branching on an uninitialised value.

Same example in AutoCorres2

We originally spotted this using AutoCorres2 as provided in AFP 2025-12-27 version and Isabelle 2025-1.

Abstracted definition of the function bogus:

bogus' ≡ do {
  x ← unknown;
  return (if x < 100 then 0 else 1)
}

Proof that it returns 0 or 1:

theory Bogus
imports
  "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file  "bogus.c"

thm bogus_body_def

autocorres "bogus.c"

thm bogus'_def

lemma bogus_res:
  "bogus' ∙ s ⦃ λRes r _. r = 0 ∨ r = 1 ⦄"
  unfolding bogus'_def
  by runs_to_vcg

end

Result of the translation to SIMPL:

bogus_body ≡
TRY
  lvar_nondet_init (λupd. bogus.ret':=⇩ℒ upd);;
  (lvar_nondet_init (λupd. bogus.x:=⇩ℒ upd);;
   IF ´bogus.x <s 0x64 THEN
     creturn global_exn_var'_'_update (λupd. bogus.ret':=⇩ℒ upd) (λs. 0)
   ELSE
     creturn global_exn_var'_'_update (λupd. bogus.ret':=⇩ℒ upd) (λs. 1)
   FI);;
  Guard DontReach {} SKIP
CATCH ccatchreturn global_exn_var'_'
END

Questions

We would like to ask:

• Is this a known issue?
• Are there some additional assumptions about the C semantics, target compilers, or architectures where such treatment of locals is valid?
• Is there a way that the C Parser could be configured to add guards to disallow such UB?
• Do you have a strategy for dealing with such programs?

One naive patch maybe could be to disallow declarations of locals without assigning value. E.g. forbidding statements like int x; but allowing int x = 0; in function bodies in the C subset of C Parser. Though we don't know if this could have some larger implications, e.g. while dealing with structs that are locals or regarding efficiency. For our use case we could perhaps circumvent this in a way by using some linter on the C source to detect such patterns.

[zilinc]

A follow-up question is that, does it in a similar way affect the trustworthiness of the binary verification work?

[lsf37]

Good questions (and hi Zilin :-), it been a while!).

• Is this a known issue?
• Are there some additional assumptions about the C semantics, target compilers, or architectures where such treatment of locals is valid?

It is known, but in our stack it is not an issue, it is this way by design. I think the fundamental expectation mismatch is that we do not model the C standard -- we model the behaviour of specific GCC versions for specific platforms.

We do try to mostly conform to the C99 standard, just for general sanity, and we prove absence of most UB instances (null pointer dereferences, array bounds, signed under/overflow etc), but dynamic memory handling in a kernel like seL4 is fundamentally technically UB (it is implementing the allocator, so it cannot only use allocated memory). The memory model also allows proof of type punning that is strictly speaking UB in C (does not have to go via byte etc). While all of that is technically true, kernels do routinely rely on the compiler to not be aggressive about these types of UB, which is different for optimisation assumptions it would for instance make about signed overflow and underflow. Of course relying on "reasonable" compiler behaviour in the face of UB is a bit risky, and it does need to be checked for each new compiler version and platform.

For the case of local variable initialisation, we do make the assumption that it will hold some valid value. That is the case for the types we support on the platforms we support (e.g. specifically no floats). While we would generally try to avoid the case you have above (it is hard to get that result without noticing what you're doing in the proofs), it would in fact be true that gcc on aarch32 will return either 0 or 1 for this program. I'm not actually sure what the binary verification tool chain would do -- it might reject the dependency on nondeterminism, just because it can't deal with it. (Like I said, we avoid this case, even though the C-level tool chain does not force us to.)

The thing that allows us to be sure that we correctly model the behaviour GCC implements when we make these broader assumptions is the binary verification pass (for AArch32 only at the moment) and test/manual inspection of critical parts of the output (i.e. it would become obvious immediately in tests if the memory representation assumptions are violated or basic memory allocation would not work).

As a side remark, this is one of the main reasons we do not pair the C verification tool chain with CompCert (apart from being in a different logic). CompCert does model the C standard much more closely, and I don't think our code would satisfy the assumptions of its correctness theorem. That is no failure of CompCert -- this is the right thing to do for a verified compiler. It probably would generate the expected code anyway (it did in the past when we tried it out), but chaining the theorems does fundamentally not work because of that mismatch.

Is there a way that the C Parser could be configured to add guards to disallow such UB?

In the current implementation there is not, but an option could probably be added, yes. Your idea to disallow declarations without initialisation would work, for instance. A more general option would be tricky -- it would mean you need an additional value in the value space to indicate that the variable has not been initialised yet and trigger the guard on that. That additional value could maybe be provided with a separate boolean for each variable in the local variable record (or maybe an additional record for that). All of these would be a bit of a project, but they would be possible.

Do you have a strategy for dealing with such programs?

The short version is that we validate that the compiler does the "reasonable" thing even though it is allowed to set the machine on fire if it wants to. For one platform, this validation is formal, for the other ones it is informal.

[zilinc]

Thank you Gerwin for the detailed explanation. My following comments and questions may be beyond the scope of l4v. I think the mismatch of expectations possibly came from the fact that the AutoCorres toolchain is not only a dedicated l4v tool but also has an AFP community fork, which I perceived (possibly wrongly) as a more general-purpose tool that is not tied to kernel-level C code verification (some of the impression was from the discussion #Mirror: Isabelle Users Mailing List > [isabelle] New in the AFP: AutoCorres2). But I think it's still not a universally applicable tool.

Of course relying on "reasonable" compiler behaviour in the face of UB is a bit risky, and it does need to be checked for each new compiler version and platform.

That is totally understandable. If we were to use it, what is the best way to do this check in engineering, so that we can be sure that all the UB are modelled in a way that agrees with the specific arch and compiler of our choice? Is it done generically, in the sense that we can conclude that the AutoCorres toolchain is compatible with X-arch and Y-compiler, or is it done per target C program, that for one certain piece of C program in question, it doesn't contain any code that AutoCorres and the compiler/arch would disagree.

The thing that allows us to be sure that we correctly model the behaviour GCC implements when we make these broader assumptions is the binary verification pass (for AArch32 only at the moment) and test/manual inspection of critical parts of the output (i.e. it would become obvious immediately in tests if the memory representation assumptions are violated or basic memory allocation would not work).

Just to clarify, as you've argued in the paper https://sel4.systems/Research/pdfs/comprehensive-formal-verification-os-microkernel.pdf, once you chain the spec->C and C->binary proofs, the correctness of the extracted C semantics is no longer critical. In l4v's case, do you ever take advantage of this liberty of using an "incorrect" C semantic representation?

[midnightveil]

For the case of local variable initialisation, we do make the assumption that it will hold some valid value. That is the case for the types we support on the platforms we support (e.g. specifically no floats). While we would generally try to avoid the case you have above (it is hard to get that result without noticing what you're doing in the proofs), it would in fact be true that gcc on aarch32 will return either 0 or 1 for this program. I'm not actually sure what the binary verification tool chain would do -- it might reject the dependency on nondeterminism, just because it can't deal with it. (Like I said, we avoid this case, even though the C-level tool chain does not force us to.)

To be fair, afaik there's nothing explicit in C99 so this is easily missed, but whilst unitialised variables of automatic storage duration have "indeterminate or trap representation", and indeterminate just means any valid value of the type; there's a note in Appendix J that actually it's undefined behaviour.

Not sure about GCC's internal representation, but LLVM's is definitely incompatible: uninitialised is poison and so comparisons will not be internally consistent.