GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
637 stars 42 forks source link

Could not resolve function/option [crucible-server] #204

Closed WeeknightMVP closed 2 years ago

WeeknightMVP commented 5 years ago

Following up on Issue #180, my client no longer reports failure to find the Prelude or Prelude.and_True, but for various scenarios now reports that crucible-server Could not resolve function: {function}:

...and Option not found: {option}:

WeeknightMVP commented 5 years ago

Now for multipart*_64_8_* I'm seeing pairs of error messages, where the first is null and the second is Expected simulator ACK response (suggesting a client/server handshake issue); the second message has code: AbortedReadBeforeWrite, message: WordMap: read an undefined index: 0x7 or likewise, with functionName: multipart*_64_8_* appearing in a backtrace.

robdockins commented 5 years ago

The setting name for saw.check_path_sat has changed and is now checkPathSat. I updated this in the Java API for the SAWSimulator, so you may need to recompile that library if you are using a stale version (for which you might have to downgrade your protoc, as we discussed before). I have not yet had a chance to chase down what I need to do to handle more recent protobuf compilers.

I'm not sure what's causing the multipart* errors, but if you have version drift with the Java library, that could well be it. I'll see if I can reproduce that problem here.

WeeknightMVP commented 5 years ago

After downgrading protoc (3.4.0) and updating crucible (nightly), I have successfully built java_api (during which tests fail as previously observed) and see that the saw.check_path_sat error has gone away. Thank you.

I've tracked down the client's calls to multiPart*, where it asks for a handle to a multipartLoad or multipartStore instruction with the appropriate address width (64), cell size (8), and number of cells (1 or 4). I generated these errors by trying to verify Salsa20 s20_littleendian and s20_rev_littleendian for a 64-bit little endian architecture.

RyanGlScott commented 2 years ago

Closing as crucible-server is no longer being maintained. See #952.