search

rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
61 stars 10 forks source link

isla-preprocess: linearization breaks serialization #79

Closed mmcloughlin closed 8 months ago

mmcloughlin commented 8 months ago

I'm not sure if this is expected to work, but it appears that linearization breaks serialization.

So for example, I see that the following works:

> cargo run --release --bin isla-preprocess -- --verbose --arch path/to/armv9.ir --config isla/configs/armv9p4.toml --output /tmp/armv9

But with --linearize AddWithCarry I get 

Failed to write output file '/tmp/armv9.irx' error: Failed to serialize architecture

To avoid the XY Problem: my use case is that I'm currently using isla-lib in another binary and not currently using your opts.rs options parsing (which does the linearization logic). I can port my code to invoke your options parser before my own, but I had thought I might be able to do the required linearization in preprocess and ingest the serialized architecture in my tool instead.

Alternatively, I had wondered about whether opts.rs is actually the right place to be doing surgery on the architecture definitions? Perhaps instead we could add a list of functions to be linearized to the ISAConfig and do linearization in init.rs? This would be easier for external tools to specify linearized functions without needing to use the same options parser.

Alasdair commented 8 months ago

I think the serialization code relies on some preprocessing steps not having occurred. Instructions that call primitive functions are updated to include a function pointer to the primitive they reference, so a primitive call is just a pointer dereference. Those function pointers can't be serialised. On the other hand, the linearization step probably expects to happen after that.

The serialization thing is mostly there to speed up the web interface. I think in any other use-case it would be better to just treat loading the IR as a one time cost, then keep it around in memory for subsequent queries.

The opts.rs file is probably the wrong place to be doing some of what it does. I think the overall API for isla-lib is not very friendly right now. I've been thinking it might be good to have some kind of high-level builder API for constructing queries that wouldn't have so many moving pieces.

mmcloughlin commented 8 months ago

Thanks for the explanation. Happy to close this out.