Exception analyzing program with CAS operation

[aaronbembenek]

Hi there,

I got an exception when running this program (cas.c) through BASIL:

#include <stdatomic.h>

atomic_int z;

int main() {
    int expected = 0;
    atomic_compare_exchange_weak(&z, &expected, 1);
}

I used the ghcr.io/uq-pac/basil-dev:latest podman container to compile the program and lift the binary, with these commands:

aarch64-linux-gnu-gcc -O0 -fno-stack-protector -fno-plt -fno-pic -march=armv8.1-a cas.c -o cas.out
bap cas.out -d adt > cas.adt
readelf -r -s -W cas.out > cas.relf

I then ran BASIL (commit 686ee8e) like so:

./mill run --analyse --input cas.adt --relf cas.relf --spec cas.spec --output cas.bpl --memory-regions mra 

where cas.spec is:

Globals: 
z: bv32

L: z -> true

I got this exception:

Exception in thread "main" java.util.NoSuchElementException: None.get
        at scala.None$.get(Option.scala:627)
        at scala.None$.get(Option.scala:626)
        at translating.BAPToIR.translate$$anonfun$1(BAPToIR.scala:40)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at translating.BAPToIR.translate(BAPToIR.scala:45)
        at util.IRLoading$.load(RunUtils.scala:95)
        at util.RunUtils$.loadAndTranslate(RunUtils.scala:532)
        at util.RunUtils$.run(RunUtils.scala:517)
        at Main$.main(Main.scala:117)
        at Main.main(Main.scala)

Thanks! Let me know if you need more info.

[l-kent]

This is not the cause of the bug here but --memory-regions mra is not going to do anything useful until #270 is merged in.

[l-kent]

The issue is just that the AtomicStart and AtomicLoad intrinsics that our lifters produce for atomic operations are not yet supported in BASIL. If that's needed for something now then I can prioritise finishing that as it has been on the backburner for a long time.

[ailrst]

Bap emits procedures for these intrinsics fine, but it is an issue with the gtirb frontend. There are more issues with the gtirb frontend.

[l-kent]

The atomic intrinsics are not currently supported in BASIL with either lifter. The idea has never been to represent them in the Boogie output as procedure calls.

[ailrst]

Ok sorry I don't recall our previous discussion of this but Nick clarified for me we just want to remove the relies for the simple cas case. I will get the frontend to the point it can insert the intrinsics, so they can be cleaned up in an analysis as handling them properly will likely be the responsibility of the backend.

[l-kent]

I was working on this months ago but it was put on the backburner to get the memory regions working. It isn't something that requires an analysis to clean up but does require substantial new functionality. If getting the atomics working is now a priority, I can move back to working on that since memory regions are mostly fine now, but a version that just parses the intrinsics as procedure calls without crashing but without handling them properly is likely not going to be very useful to anyone.

[ailrst]

Fixing the frontend so it emits intrinsics may be enough for Aaron to manually tweak the output so he at least has something to test, if that is useful on its own. This should work for at least BAP now.

There was a lifter bug (fixed yesterday) which put loads in the branch condition so ensure you update the lifter and flush the bap lifter cache:

nix profile upgrade packages.x86_64-linux.bap-aslp
bap cache --clean

• The gtirb frontend still a) crashes on seeing the intrinsic, and b) doesn't replace the TempIf with control-flow.

If you would prefer to fix the whole thing at once I will leave that to you liam.

[l-kent]

Yes, it would be useful to know what @aaronbembenek is trying to do with this example - that would make it easier to know how to handle it for the time being.

[aaronbembenek]

Hi there - thanks for the help!

I am hoping to show that our invariant inference tool works on the example programs from the CSF'21 paper "Backwards-directed information flow analysis for concurrent programs." This is the actual program I'm trying to run BASIL on:

#include <stdatomic.h>

int x = 0;
atomic_int z;
int secret;

int main() {
    int expected = 0;
    while (!atomic_compare_exchange_weak(&z, &expected, 1)) {
        while (z != 0) {}
        expected = 0;
    }
    x = secret;
    x = 0;
    z = 0;
}

In terms of the translation of the CAS operation, I don't think I would need anything especially accurate; something like the conversion in the paper would be sufficient (which rewrites it to non-atomic code, but omits a rely() between when z is tested and when it is updated).

[aaronbembenek]

By the way, this isn't a huge blocker for me right now, if it's not the right time to fix it. I can always simulate the CAS operation by rewriting the source and deleting rely()s from the generated Boogie.

[l-kent]

something like the conversion in the paper would be sufficient (which rewrites it to non-atomic code, but omits a rely() between when z is tested and when it is updated).

Yeah, that's what we plan to implement but it isn't yet finished.

By the way, this isn't a huge blocker for me right now, if it's not the right time to fix it. I can always simulate the CAS operation by rewriting the source and deleting rely()s from the generated Boogie.

I'd suggest this is the best approach for you for now, it should be equivalent enough to what is produced when the atomics support is finished. I'm not sure how long that will take at this stage but I'll let you know when it is ready.

You may be able to get this example as-is to go through BASIL now thanks to @ailrst's minor fix but that won't be what you're after.