[klee-dev] Dealing with missing intrinsics (Rust support)

2020-08-14 Thread Alastair Reid
Hi, I want to check what the best way is to deal with missing intrinsics when adapting KLEE for a new language and new standard libraries. In particular, what kind of changes should I make and submit as PRs? I am trying to use KLEE with a modest sized Rust application (about 20kloc) but that

Re: [klee-dev] Dealing with missing intrinsics (Rust support)

2020-08-14 Thread Cristian Cadar
+1 to this, we should only terminate those paths that hit unhandled intrinsics. This is what we do with unavailable external functions and inline assembly for instance, so we should adopt the same behaviour here. Best, Cristian On 14/08/2020 18:06, Nowack, Martin wrote: Hi Alastair, I

Re: [klee-dev] Dealing with missing intrinsics (Rust support)

2020-08-14 Thread Nowack, Martin
Hi Alastair, I would also rather use option 3. Normally, the `LowerIntrinsic` pass should try to replace appropriate calls if possible. It should not terminate it. Beside your attached code, I would suggest to change the following code line in `lib/Core/Executor.cpp`: