You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have automated footprint generation in Isla for all instructions on RISC-V (I essentially provide the instruction listings from the RISC-V unprivileged spec in adoc format, parse those and encode the immediates as symbolic segments).
What I am trying to achieve now is to use the "d" option to pretty-print all the dependencies of each instruction.
By default, I get the error that it's a Symbolic Instruction.
I have been tinkering the code a bit to change that and capture the footprint already in footprint.rs (since that's similar to what is done in footprint_analysis.rs in the absence of a cache).
For this, I am basically creating the footprint_buckets before calling the executor::start_multi in footprint.rs and pushing all the events in the buckets (as done in footprint_analysis). The opcode_val is still symbolic in this case. This part is currently a WIP.
But I am wondering whether it will be fruitful eventually to generate output in the pretty format or am I missing something i.e. why is pretty printing not supported by default for Symbolic instructions?
The other option I can take is simply to parse the smtlib traces generated. But getting an output similar to what is generated with the "-d" option would help me save that effort.
Thanks in advance.
The text was updated successfully, but these errors were encountered:
Hello,
I have automated footprint generation in Isla for all instructions on RISC-V (I essentially provide the instruction listings from the RISC-V unprivileged spec in adoc format, parse those and encode the immediates as symbolic segments).
What I am trying to achieve now is to use the "d" option to pretty-print all the dependencies of each instruction.
By default, I get the error that it's a Symbolic Instruction.
I have been tinkering the code a bit to change that and capture the footprint already in footprint.rs (since that's similar to what is done in footprint_analysis.rs in the absence of a cache).
For this, I am basically creating the footprint_buckets before calling the executor::start_multi in footprint.rs and pushing all the events in the buckets (as done in footprint_analysis). The opcode_val is still symbolic in this case. This part is currently a WIP.
But I am wondering whether it will be fruitful eventually to generate output in the pretty format or am I missing something i.e. why is pretty printing not supported by default for Symbolic instructions?
The other option I can take is simply to parse the smtlib traces generated. But getting an output similar to what is generated with the "-d" option would help me save that effort.
Thanks in advance.
The text was updated successfully, but these errors were encountered: