[litmus] Print fault occurrences as generated

[maranget]

This PR is the litmus7 equivalent of the PR #1984 that fixes fault printing in herd7. The objective is the same: printing faults that have occurred in complete format and negated fault specifications from the final condition when they match no fault that has occurred.

In the case of litmus7 the situation was made more complex by the semantics of prefixless fault types in specifications. In short, they were viewed as differing from prefixed fault types. For instance fault(P0,x,MMU:AccessFlag) was considered to differ from Fault(P0,x,D-MMU:AccessFlag) and Fault(P0,x,I-MMU:AccessFlag) and not as a partial specification of those. As an example, consider the simple test:

AArch64 TST
Variant=vmsa
{
int x=1;
[TTD(x)]=(af:0);
0:X1=x;
1:X0=(oa:PA(x),af:1); 1:X1=TTD(x);
}
  P0        |  P1         ;
LDR W0,[X1] | STR X0,[X1] ;

forall 0:X0=0 => Fault(P0,x,MMU:AccessFlag);

Before this PR, running TST on some AArch64 machine yielded:

Test TST Required
Histogram (2 states)
32901 :>0:X0=1; ~fault(P0,x,MMU:AccessFlag);
1967099*>0:X0=0; ~fault(P0,x,MMU:AccessFlag);
No
Witnesses
Positive: 32901, Negative: 1967099
Condition forall (0:X0=0 => fault(P0,x,MMU:AccessFlag)) is NOT validated
Hash=0402bea6baacf20eca40414cc190ce26
Variant=vmsa
Observation TST Sometimes 32901 1967099
Faults TST 1967099 P0:1967099
Time TST 2.44

Observe that Fault(P0,x,MMU:AccessFlag) does not appear in the histogram. Moreover the count of faults 1967099 reveals that some faults did occur and suggests that the faults should appear in the second histogram line.

With this PR, running the test with litmus yields:

Test TST Required
Histogram (2 states)
61174 :>0:X0=1; ~fault(P0,x,MMU:AccessFlag);
1938826:>0:X0=0; fault(P0,x,D-MMU:AccessFlag);
Ok
Witnesses
Positive: 2000000, Negative: 0
Condition forall (0:X0=0 => fault(P0,x,MMU:AccessFlag)) is validated
Hash=0402bea6baacf20eca40414cc190ce26
Variant=vmsa
Observation TST Always 2000000 0
Faults TST 1938826 P0:1938826

Observe that the fault occurrences are now displayed and that the final condition is validated,

Additionally, we changed litmus7 implementation of fault recording and matching, following what herd7 does: fauts are recorded in sorted arrays (herd7 uses OCaml sets), matching follows the same rules and printing is performed in the same way: first scan the recorded faults to print them and then, for each specification, scan all recorded faults again to print non-matched specifications negated.

[maranget]

Hi @relokin and @psafont. This PR follows PR #1984. PR #1984 was cleaning fault matching for herd7, while this PR #1988 does the same for litmus7. I have attempted to synchronise both processes as much as possible. I'd appreciate your reviews.

[psafont]

I've validated that the output is as expected, manually:

$ mkdir ../kvm-unit-tests/litmus-m1-A009/
$ dune exec litmus/litmus.exe -- -set-libdir litmus/libdir -mach kvm-m1 \
                                                     -o ../kvm-unit-tests/litmus-m1-A009 \
                                                     herd/tests/instructions/AArch64.kvm/A009.litmus
$ sh -c "cd ../kvm-unit-tests/litmus-m1-A009 && \
             make CC=/opt/homebrew/bin/aarch64-elf-gcc \
                       AR=/opt/homebrew/bin/aarch64-elf-ar \
                       LD=/opt/homebrew/bin/aarch64-elf-ld \
                       OBJCOPY=/opt/homebrew/bin/aarch64-elf-objcopy"
[...]
$ sh -c "cd ../kvm-unit-tests && \
              QEMU=/opt/homebrew/bin/qemu-system-aarch64 \
              ./arm/run litmus-m1-A009/A009.flat -smp 4"
/opt/homebrew/bin/qemu-system-aarch64 -nodefaults -machine virt -accel hvf -cpu host -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel litmus-m1-A009/A009.flat -smp 4 # -initrd /var/folders/db/9808frkx4yv4kq0hkkd5f_vc0000gn/T/tmp.B9UAOX2oNz
Test A009 Required
Histogram (1 states)
4000000:> fault(P0:L0,x,D-MMU:Translation);
Ok

Witnesses
Positive: 4000000, Negative: 0
Condition forall (fault(P0:L0,x,MMU:Translation)) is validated
Hash=abfed1dff47d259c77dbd4bc5cef0cc5
Variant=fatal
Observation A009 Always 4000000 0
Faults A009 4000000 P0:4000000
Time A009 1.13

EXIT: STATUS=1

There's an example transcript of litmus logs with faults in doc/litmus.tex, it should be updated. I have to say they fail on my system, do these need to be changed?

...
Test MP-TTD+DMB.ST+DMB.LD Allowed
Histogram (3 states)
399200:>1:X7=0; ~fault(P1:L0,x,MMU:Translation);
84    :>1:X7=1; ~fault(P1:L0,x,MMU:Translation);
1600716:>1:X7=0; fault(P1:L0,x,D-MMU:Translation);
No

Witnesses
Positive: 0, Negative: 2000000
Condition exists (1:X7=1 /\ fault(P1:L0,x,MMU:Translation)) is NOT validated
Hash=e6d0396aa32c40b307db5f6921404c07
EL0=P1
Observation MP-TTD+DMB.ST+DMB.LD Never 0 2000000
Faults MP-TTD+DMB.ST+DMB.LD 1600716 P1:1600716
Time MP-TTD+DMB.ST+DMB.LD 2.20

...

Test MP-TTD+DMB.ST+DSB-ISB Allowed
Histogram (3 states)
1991148:>1:X7=0; ~fault(P1:L0,x,MMU:Translation);
69    :>1:X7=1; ~fault(P1:L0,x,MMU:Translation);
8783  :>1:X7=0; fault(P1:L0,x,D-MMU:Translation);
No

Witnesses
Positive: 0, Negative: 2000000
Condition exists (1:X7=1 /\ fault(P1:L0,x,MMU:Translation)) is NOT validated
Hash=18e9682c0e7ed43f7f059cbfc47d781d
EL0=P1
Observation MP-TTD+DMB.ST+DSB-ISB Never 0 2000000
Faults MP-TTD+DMB.ST+DSB-ISB 8783 P1:8783
Time MP-TTD+DMB.ST+DSB-ISB 2.13

EXIT: STATUS=1

...

[maranget]

There's an example transcript of litmus logs with faults in doc/litmus.tex, it should be updated. I have to say they fail on my system, do these need to be changed?

I do not understand. Do you mean that we should perform some experiment again?

[psafont]

I do not understand. Do you mean that we should perform some experiment again?

I was wondering why it fails when running in my system, and whether the experiment needed to be changed. I see that you regenerated the output, which is what I meant.

[maranget]

Merged, thanks @psafont.