[gen] Rework on printing generated litmus tests

[ShaleXIONG]

This pull request replaces the diy manual test printing by lib/simpledumper.ml. It fixes two main problems for the initialisation list.

• Incorrect array initialisation, for example, changing int y[2]; y=5 to int y[2] = {5,5}.
• Using square bracket syntax for pte initialisation [PTE(x)].

A good example is diyone7 -arch AArch64 -variant kvm PodRW Pa Rfe PodRW PteV1 Rfe. The new result shows at the end of this message.

Separately, we made major rework to top_gen.ml and final.ml in the internal code of printing litmus test. It now use lib/SimpleDumper directly rather than manually print out all the information. This simplifies the code and ensure the formatting is consistent with other tools in this repo. The new formatting can be seen below. Notice that

• the "PodRWPPa RfePaP PodRWPPteV1 RfePteV1P" is now at the end of prelude,
• all the white space are the result of SimpleDumper,
• the code label, e.g. L00, now is on the same line as the instruction, and
• the fault in post-condition now is in lower case and logical negation is not rather than ~.

Last, we add automatic Variant= ... based on the diy* argument -variant .... This enables herd7 directly configure the expected variant.

AArch64 LB+popptev1+poppa
Com=Rf Rf
Generator=diyone7 (version 7.58+1)
Orig=PodRWPPa RfePaP PodRWPPteV1 RfePteV1P
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Variant=vmsa
"PodRWPPa RfePaP PodRWPPteV1 RfePteV1P"
{
 [x]=1;
 [PTE(x)]=(oa:PA(x), valid:0);
 int y[2]={5,5};
 0:X0=x; 0:X2=y;
 1:X2=y; 1:X3=PTE(x); 1:X4=(oa:PA(x));
}
 P0               | P1          ;
 L00: LDR W1,[X0] | LDR W1,[X2] ;
 MOV W3,#7        | STR X4,[X3] ;
 SUB W4,W3,#1     |             ;
 STP W4,W3,[X2]   |             ;

exists (1:X1=6 /\ not (fault(P0:L00,x)))

It now has the same syntax as the mprog7 -mode text tool.

[murzinv]

How automatic insert of variant deal with

-info add metadata to generated test(s)

?
The reason I'm asking is that another way to inject variant into litmus test is using -info, for instance -info "variant=memtag". Now if combined with automatic variant insertion is would add two variants into the test and upset herd7

Warning: File "T.litmus": Duplicated meta-data on key Variant
 (User error)

[ShaleXIONG]

How automatic insert of variant deal with

-info add metadata to generated test(s)

? The reason I'm asking is that another way to inject variant into litmus test is using -info, for instance -info "variant=memtag". Now if combined with automatic variant insertion is would add two variants into the test and upset herd7

Warning: File "T.litmus": Duplicated meta-data on key Variant
 (User error)

[update] I managed to merge -info with the internal prelude by concat all the value in string if the key is the same in both -info and in the internal.

[fsestini]

I will have a proper look at the code ASAP, but as a quick comment: I have a question about a change to the final conditions of generarted litmus tests introduced by this PR. For example, when running your example CLI command on current master:

$ dune exec diyone7 -- -arch AArch64 -variant kvm  PodRW Pa Rfe PodRW PteV1 Rfe -cond unicond
AArch64 LB+popptev1+poppa
"PodRWPPa RfePaP PodRWPPteV1 RfePteV1P"
Generator=diyone7 (version 7.58+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Rf
Orig=PodRWPPa RfePaP PodRWPPteV1 RfePteV1P
{
int y[2];
 int x=1; PTE(x)=(oa:PA(x), valid:0); y=5;
0:X0=x; 0:X2=y;
1:X2=y; 1:X3=PTE(x); 1:X4=(oa:PA(x));
}
 P0             | P1          ;
 L00:           | LDR W1,[X2] ;
 LDR W1,[X0]    | STR X4,[X3] ;
 MOV W3,#7      |             ;
 SUB W4,W3,#1   |             ;
 STP W4,W3,[X2] |             ;
forall (x=(oa:PA(x)) /\ (y=7 /\ (1:X1=7 \/ 1:X1=0))) /\ ~Fault(P0:L00,x)

But if I run the same command on top of this PR, I get:

$ dune exec diyone7 -- -arch AArch64 -variant kvm  PodRW Pa Rfe PodRW PteV1 Rfe -cond unicond
AArch64 LB+popptev1+poppa
Com=Rf Rf
Generator=diyone7 (version 7.58+1)
Orig=PodRWPPa RfePaP PodRWPPteV1 RfePteV1P
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Variant=vmsa
"PodRWPPa RfePaP PodRWPPteV1 RfePteV1P"
{
 [x]=1;
 [PTE(x)]=(oa:PA(x), valid:0);
 int y[2]={5,5};
 0:X0=x; 0:X2=y;
 1:X2=y; 1:X3=PTE(x); 1:X4=(oa:PA(x));
}
 P0               | P1          ;
 L00: LDR W1,[X0] | LDR W1,[X2] ;
 MOV W3,#7        | STR X4,[X3] ;
 SUB W4,W3,#1     |             ;
 STP W4,W3,[X2]   |             ;

forall (not (fault(P0:L00,x)) \/ [x]=(oa:PA(x)) /\ ([y]=7 /\ (1:X1=7 \/ 1:X1=0)))

You can see that the final condition in the second run relates the fault proposition and the values propositions disjunctively, but the first run relates them conjunctively, which is a stronger assertion logically speaking. Is this intended, and if so, what is the rationale?

[ShaleXIONG]

diyone7 -- -arch AArch64 -variant kvm PodRW Pa Rfe PodRW PteV1 Rfe -cond unicond

This is a mistake. I just patched.

=To help you review, if you think it is helpful, we can have a chat in person or zoom and just go through code together, since there are many structure changes.

[fsestini]

Similarly, why is this set to F.exist_true in all cases?

Prior to this change, the command dune exec diyone7 -- -arch C PodWW Rfe PodRR Fre -cond observe would generate locations in the final condition, but now only generates exists (true).

Actually, other architectures as well now seem to always include this exists (true) line:

$ dune exec diyone7 -- -arch AArch64 PodWW Rfe PodRR Fre -cond observe
AArch64 MP
Com=Rf Fr
...
STR W2,[X3] |             ;

locations [x; y; 1:X0; 1:X2;]
exists (true)

[ShaleXIONG]

One of the goal of this change is to line up with mprog7 -mode text. In the case where only exists locations [...], the tool mprog7 actually append a forall (true). I will match the behaviour there.

Regarding questions on when location[...] yields a different result in herd7, the example is diyone7 -variant vmsa -arch AArch64 PteV1 PodWW Rfe PodRR Fre -cond observe. The location contains fault(P1:L00,x). This requests herd7 to show the fault information in all stages.

[fsestini]

Here the variants are sorted by key, which means the following comment by @relokin is still not implemented:

The variant should appear before the metadata, if not after all the metadata.

For example, if I run:

$ dune exec diyone7 -- -oneloc -variant mixed,MixedDisjoint -arch AArch64 h2 PosWW h0 Rfe Fre -hexa -info 'Z=foo'
AArch64 WW+R+posh2h0+w0
Com=Rf Fr
Generator=diyone7 (version 7.58+1)
Orig=PosWWh2h0 Rfeh0w0 Frew0h2
Variant=mixed
Z=foo
"PosWWh2h0 Rfeh0w0 Frew0h2"
{
 uint32_t 0:X0=0; 0:X1=x; uint32_t 0:X2=0;
...

The Variant key/value pair appears in between other metadata.

Code-wise, I don't see why we couldn't sort the keys via List.sort or similar, rather than StringMap.

[ShaleXIONG]

I update it in a way that the rhs will be merged into the lhs. Also I realised if the key collides, for example internal and user-defined, or between two user-defined. The value will be concatenate.

In the case of Variant it is in fact ok to have Variant = memtag memtag for herd7.

[relokin]

One more request please. Can we make sure that the variant is always printed. That's even when I do -metadata false.

[relokin]

And similarly for TTHM, -metadata false shouldn't hide. Also TTHM should appear right after the Variant=....

[ShaleXIONG]

All good point ! I will update now.