llvm_load_module: FUNC_CODE_INST_ATOMICRMW not implemented

[ctz]

I'm just getting started with saw/crucible. I can't seem to load my bitcode:

✓ jbp@debian ⎇ master= ~/rustls$ export PATH=$PATH:~jbp/saw-0.2-2017-09-15-Ubuntu14.04-64/bin

✓ jbp@debian ⎇ master= ~/rustls$ cat basics.saw
llvm <- llvm_load_module "rustls.bc";

✓ jbp@debian ⎇ master= ~/rustls$ saw basics.saw
Loading module Cryptol
Loading file "/home/jbp/rustls/basics.saw"
saw: user error ("llvm_load_module" (/home/jbp/rustls/basics.saw:1:9):
not implemented
from:
	FUNC_CODE_INST_ATOMICRMW
	_ZN4core4sync6atomic10atomic_add17hcb98728e357b46d4E
	FUNCTION_BLOCK
	FUNCTION_BLOCK_ID
	MODULE_BLOCK
	Bitstream
)

This bitcode is generated by rustc 1.20.0, which AIUI is based on LLVM 4.0.

[atomb]

Ah, yeah, it looks like the atomicrmw instruction isn't being parsed yet. Thanks for pointing it out!

[robdockins]

We should now be able to parse atomicrmw given some recent work on improving our bitcode parser. Unfortunately, the attached bitcode file is produced by a rather old clang, before they changed the meaning of the type argument to stores and loads, and currently fails with a "Invalid argument type on store" message.

More importantly, we have not yet provided semantics for the atomicrmw instruction. I believe the current situation is that we can load a BC file containing this instruction (provided it's build with a reasonably recent LLVM), but translation will fail if we actually try to execute a function containing the instruction.

[langston-barrett]

That's my understanding as well. It's a very recent PR that implemented this in the parser: GaloisInc/llvm-pretty-bc-parser#111

[atomb]

With the latest parser, it's possible to load the module, but the translation to Crucible fails.

sawscript> m <- llvm_load_module "rustls.bc"
saw: Failure encountered while generating a Crucible CFG: at :370:0: Invalid argument type on store Typed {typedType = PtrTo (Alias (Ident "str_slice")), typedValue = ValIdent (Ident "_0")}

[atomb]

Even if the error produced above is inevitable (i.e., a well-typed Crucible program can't feasibly be generated), it might be nice to delay the error until runtime, so that it'll only get in the way if we try to symbolically execute the function in question.

[robdockins]

I believe that there are now translations for the atomicrmw instructions, so it seems like we just have to navigate the type question. If we produce a bitcode file with more recent rust/clang, this might just work...

[robdockins]

I've attempted to reproduce this error by building rustls and loading it... however, recent rustc is based on LLVM version 8.0, which our bitcode parser cannot yet handle.

So, we seem to be blocked on GaloisInc/llvm-pretty-bc-parser#127

[ctz]

I've attempted to reproduce this error by building rustls and loading it... however, recent rustc is based on LLVM version 8.0, which our bitcode parser cannot yet handle.

I've just come back to looking at this and am finding the same thing :( Worse, the last rustc which used LLVM 7 (1.29.2) does not support the 2018 edition of rust.

[atomb]

We now support the atomicrmw instruction and LLVM 8 and 9 (and therefore the output of the latest Rust compiler). For the store type error listed above, I think it's an instance of GaloisInc/llvm-pretty-bc-parser#135 (even though that specific example is about vector instructions --- I think the overall problem is broader). So I'm going to close this issue now.

[ctz]

Took me a while to get back to this, but I'm pleased to say that I just tried this again with 0.4 and it worked fine. Thanks!