Faial checks for absence of #dataraces in #CUDA kernels. New since our #CAV21 version is:
- a new frontend all written in OCaml (no more Python+Rust) we also have a new UI (sshot below)
- a new backend (invoke #Z3 as a library, as a process)
- support for partial inputs (eg, missing includes)

My intent to have a bit of a codebase written in Python was to attract students. Turns out interested students are excited to learn #OCaml.

@AssertionError how much of C++ does this support? I had a miserable time doing CUDA tooling for an academic project (@shriramk likely remembers 😅) because of having to deal with parsing all the bizarre C++ corner cases.

@elfprince13 @shriramk

We use libclang to parse. Luckily most kernels we've seen use a small number of C++ features. We do support things like templated kernels and we have limited support for classes --- insofar as we only support arrays of opaque data.

@AssertionError @shriramk I did a clang plugin but there are an absurd number of weird corner cases even in the AST representation. Ignoring classes probably helps with a lot

@elfprince13 @shriramk

Ah, exactly. Libclang/C++ overwhelmed me very quickly. Instead we just serialize the ast into JSON and then handle everything in OCaml here:

https://gitlab.com/umb-svl/faial/-/blob/main/inference/lib/c_lang.ml

@elfprince13 @shriramk

The C++ plug-in we have to maintain is pretty trivial, since it's one of the hello world examples of libtooling. I mostly keep it in sync whenever I want to do an API bump. The OCaml part becomes manageable because it was written to support only the application we're interested in --- it's a restriction of the the whole API surface of libclang.

C++ code:

https://gitlab.com/umb-svl/c-to-json/-/blob/master/src/JSONNodeDumper.cpp