CTSRD-CHERI / QuickCheckVEngine

A RISC-V TestRIG Verification Engine based on QuickCheck
BSD 2-Clause "Simplified" License
7 stars 10 forks source link

Trace is not saved if one implemention dies #24

Closed arichardson closed 1 year ago

arichardson commented 1 year ago

I feel like this used to work, now I just see Failure rerunning test without a file being written (in non-interactive mode)/being prompted to save the test.

arichardson commented 1 year ago

Example trace that currently asserts in QEMU:

#>QCVENGINE_TEST_V2.0
#>START_NO_SHRINK
.4byte 0x000020b7 # lui x1, 2
.4byte 0x3000a073 # csrrs x0, mstatus (0x300), x1
.4byte 0x00302073 # csrrs x0, fcsr (0x3), x0
.4byte 0xf0000053 # fmv.w.x f0, x0
.4byte 0xf00000d3 # fmv.w.x f1, x0
.4byte 0xf0000153 # fmv.w.x f2, x0
.4byte 0xf00001d3 # fmv.w.x f3, x0
.4byte 0xf0000253 # fmv.w.x f4, x0
.4byte 0xf2000853 # fmv.d.x f16, x0
.4byte 0xf20008d3 # fmv.d.x f17, x0
.4byte 0xf2000953 # fmv.d.x f18, x0
.4byte 0xf20009d3 # fmv.d.x f19, x0
.4byte 0xf2000a53 # fmv.d.x f20, x0
#>END_NO_SHRINK
.4byte 0x007a285b # csetboundsimmediate x16, x20, 7
.4byte 0x00200113 # addi x2, x0, 2
.4byte 0x00c11113 # slli x2, x2, 12
.4byte 0x1e28085b # csetoffset x16, x16, x2
.4byte 0x4168185b # cincoffsetimmediate x16, x16, 1046
.4byte 0xffd00193 # addi x3, x0, -3
.4byte 0x1a38085b # candperm x16, x16, x3
.4byte 0x171181db # cseal x3, x3, x17
.4byte 0xfd0180db # cinvoke x3, x16
.4byte 0xfea08fdb # cmove x31, x1
.4byte 0x0ff17113 # andi x2, x2, 255
.4byte 0x400040b7 # lui x1, 262148
.4byte 0x00109093 # slli x1, x1, 1
.4byte 0x00208133 # add x2, x1, x2
.4byte 0xfb7100db # lq.ddc x1, x2[0]
.4byte 0xfe4888db # cgettag x17, x17
.4byte 0x01082a5b # csetboundsimmediate x20, x16, 16
.4byte 0x00200993 # addi x19, x0, 2
.4byte 0x00c99993 # slli x19, x19, 12
.4byte 0x1f3a0a5b # csetoffset x20, x20, x19
.4byte 0x911a1a5b # cincoffsetimmediate x20, x20, 2321
# Test end
PeterRugg commented 1 year ago

Hmm, that trace seems to run fine in QEMU for me?

PeterRugg commented 1 year ago

Oh, it works for the qemu pointed to by testrig. I can't seem to build dev, if that's the version that asserts: ../target/cheri-common/op_helper_cheri_common.c:1547:39: error: initializer element is not constant static const uint32_t sizealign = ncaps * CHERI_CAP_SIZE; Any chance you could give me a pointer to the qemu version that fails and the exact test command you run?

arichardson commented 1 year ago

Yes it's the latest dev branch.

PeterRugg commented 1 year ago

Hopefully fixed by: https://github.com/CTSRD-CHERI/QuickCheckVEngine/commit/20f16cf6515fc7b137a1402b926ea065305cf75b

arichardson commented 1 year ago

Thanks, I can confirm it now prompts me to save the unreduced test case.