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.
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.