bundled version of l3 riscv model and step

[palmskog]

@didriklundberg is this what you had in mind? I took the latest files from the dev_riscv_l3_t1_2 branch.

[didriklundberg]

@didriklundberg is this what you had in mind? I took the latest files from the dev_riscv_l3_t1_2 branch.

No, take the files from trindemossen-1 as I wrote on Zulip. Then I will contribute my changes on top of those files. Also, I see you did not add the copyright notice of the "HOL4 CONTRIBUTORS".

[palmskog]

@didriklundberg OK now?

[didriklundberg]

@didriklundberg OK now?

You forgot to remove riscv_stepSimps.sig and riscv_stepSimps.sml.

[didriklundberg]

Okay, I added the changes now. Here's a PR into l3-riscv with the additions on the HolBA side, which I suggest we handle before merging this PR.

[palmskog]

@didriklundberg apparently an ARM(!) self test is failing, could you take a look?

 Failed tests: (1 total)
- src/tools/lifter/selftest_arm.exe

[didriklundberg]

@didriklundberg apparently an ARM(!) self test is failing, could you take a look?

 Failed tests: (1 total)
- src/tools/lifter/selftest_arm.exe

Looks like two failing instructions switching order: benign, but unexpected. Let me take a look at what could have caused this.

[didriklundberg]

@didriklundberg apparently an ARM(!) self test is failing, could you take a look?

 Failed tests: (1 total)
- src/tools/lifter/selftest_arm.exe

The reason for failure is the change to src/tools/lifter/selftestLib.sml which now lists lifter failures in order of occurrence, rather than reverse order of occurrence. I suggest pushing the updated arm8 selftest log: if you think this is solution is OK, I can fix it.

[palmskog]

I suggest pushing the updated arm8 selftest log: if you think this is solution is OK, I can fix it.

Please go ahead and fix, also feel free to merge this into riscv-symbexec when it makes CI green.