Isla-footprint RISC-V

[neeluk7]

Hello,

I am trying to use the Isla-footprint tool to generate traces for RISC-V instructions but so far I have not been successful. I get an error for sail_barrier being an unknown event. (See image attached)

I assumed that it is because of outdated Isla IR snapshots, so I tried to regenerate them using Isla-sail. If that is not the case, please let me know if you have any idea why I am getting this error.

For regenerating the snapshots, I followed the following advice from the README of this repo:

"To generate this IR in the correct format a tool is available in the isla-sail directory. Building this requires various arcane OCaml incantations, but mostly one can follow the Sail install guide here, followed by the instructions here. It will only work with the latest HEAD of the sail2branch in the Sail repository."

So the sail I use is from the sail2 branch. But running the Isla-sail tool for all the sail files in the RISC-V model throws the following error:

If you could point me to where I might be going wrong, I will highly appreciate that.

Thanks in advance.
Regards,
Neelu

[bacam]

I think you've just put the source files in the wrong order. I can build it with the following change to the Makefile in sail-riscv:

--- a/Makefile
+++ b/Makefile
@@ -193,6 +193,8 @@ endif
 RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
 RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
 
+ISLA_SAIL=isla-sail
+
 .PHONY:
 
 all: c_emulator/riscv_sim_$(ARCH)
@@ -214,6 +216,9 @@ sail_doc/riscv_$(ARCH).json: $(SAIL_SRCS) model/main.sail
 riscv.smt_model: $(SAIL_SRCS)
        $(SAIL) -smt_serialize $(SAIL_FLAGS) $(SAIL_SRCS) -o riscv
 
+riscv64.ir: $(SAIL_SRCS) model/main.sail
+       $(ISLA_SAIL) $(ISLA_SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -o riscv64
+
 cgen: $(SAIL_SRCS) model/main.sail
        $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail

[neeluk7]

Hello,

Thanks for your response. Indeed the order of the source files needed to be fixed. I am able to build the IR now.

But even then, generating instruction traces with Isla-footprint does not work and I get the following error:

Even though val sys_pmp_count is defined in the sail source (and it's not really a function as Isla-footprint seems to be expecting).

Can you please confirm if you see the same output or not?
And if not, is it because of something missing in the command or should I be using a particular branch/commit from sail-riscv?

I appreciate the help!

[bacam]

This is one of the configuration options for the RISC-V model, which they occasionally add to. You can provide a value for it by adding a sys_pmp_count entry to the const_primops section at the bottom of the configuration file. If you need some reasonable default values, look at those used for the C emulation in c_emulator/riscv_platform_impl.c in the sail-riscv repository.

[neeluk7]

Hello Brian, thanks for your reply.

I tried adding it to the const_primops, and I get some type error now instead.

It might be very trivial,
but I just specified sys_pmp_count = 0 under the const_primops. It's similar to what I saw in the riscv_platform_impl.c.

Is there a version of the config you could share that already has the necessary configurations specified?

[bacam]

There were a couple of issues preventing that from working which I've fixed and pushed, along with an updated configuration file. In particular, the integer needs to have the right size, so I've added the ability to specify which size it has in the config file. Ideally it would be automatically inferred, but this should be sufficient for now.

[neeluk7]

Hello Brian,

Thanks a lot for the help and prompt responses. The trace generation works now. 👍