Skip to content

Commit 04f7250

Browse files
ThomasHaasThomasHaas
committed
Add STADD and variants (except for min/max)
1 parent c140f80 commit 04f7250

3 files changed

Lines changed: 153 additions & 43 deletions

File tree

‎dartagnan/src/main/antlr4/LitmusAArch64.g4‎

Lines changed: 62 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -63,9 +63,12 @@ instruction
6363
| store
6464
| storePair
6565
| storeExclusive
66+
// AMOs
6667
| loadOp
68+
| storeOp
6769
| swap
6870
| cas
71+
// -----
6972
| cmp
7073
| branch
7174
| branchRegister
@@ -125,6 +128,11 @@ loadOp
125128
| loadOpInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
126129
;
127130

131+
storeOp
132+
: storeOpInstruction rS32 = register32 Comma LBracket address RBracket
133+
| storeOpInstruction rS64 = register64 Comma LBracket address RBracket
134+
;
135+
128136
swap
129137
: swapInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket
130138
| swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
@@ -179,25 +187,44 @@ loadExclusiveInstruction locals [boolean acquire, boolean byteSize, boolean half
179187
| LDAXRH {$acquire = true; $halfWordSize = true;}
180188
;
181189

182-
loadOpInstruction locals [IntBinaryOp op, boolean acquire, boolean release, boolean byteSize, boolean halfWordSize]
190+
loadOpInstruction
183191
// ADD
184-
: LDADD | LDADDA | LDADDL | LDADDAL
192+
: LDADD | LDADDA | LDADDL | LDADDAL
185193
| LDADDH | LDADDAH | LDADDLH | LDADDALH
186194
| LDADDB | LDADDAB | LDADDLB | LDADDALB
187195
// EOR
188-
| LDEOR | LDEORA | LDEORL | LDEORAL
196+
| LDEOR | LDEORA | LDEORL | LDEORAL
189197
| LDEORH | LDEORAH | LDEORLH | LDEORALH
190198
| LDEORB | LDEORAB | LDEORLB | LDEORALB
191199
// SET
192-
| LDSET | LDSETA | LDSETL | LDSETAL
200+
| LDSET | LDSETA | LDSETL | LDSETAL
193201
| LDSETH | LDSETAH | LDSETLH | LDSETALH
194202
| LDSETB | LDSETAB | LDSETLB | LDSETALB
195203
// CLR
196-
| LDCLR | LDCLRA | LDCLRL | LDCLRAL
204+
| LDCLR | LDCLRA | LDCLRL | LDCLRAL
197205
| LDCLRH | LDCLRAH | LDCLRLH | LDCLRALH
198206
| LDCLRB | LDCLRAB | LDCLRLB | LDCLRALB
199207
;
200208

209+
storeOpInstruction
210+
// ADD
211+
: STADD | STADDL
212+
| STADDH | STADDLH
213+
| STADDB | STADDLB
214+
// EOR
215+
| STEOR | STEORL
216+
| STEORH | STEORLH
217+
| STEORB | STEORLB
218+
// SET
219+
| STSET | STSETL
220+
| STSETH | STSETLH
221+
| STSETB | STSETLB
222+
// CLR
223+
| STCLR | STCLRL
224+
| STCLRH | STCLRLH
225+
| STCLRB | STCLRLB
226+
;
227+
201228
storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize]
202229
: STR
203230
| STRB {$byteSize = true;}
@@ -441,7 +468,6 @@ LDADDB : 'LDADDB' ;
441468
LDADDAB : 'LDADDAB' ;
442469
LDADDLB : 'LDADDLB' ;
443470
LDADDALB : 'LDADDALB' ;
444-
445471
// EOR (XOR)
446472
LDEOR : 'LDEOR' ;
447473
LDEORA : 'LDEORA' ;
@@ -455,7 +481,6 @@ LDEORB : 'LDEORB' ;
455481
LDEORAB : 'LDEORAB' ;
456482
LDEORLB : 'LDEORLB' ;
457483
LDEORALB : 'LDEORALB' ;
458-
459484
// SET (OR)
460485
LDSET : 'LDSET' ;
461486
LDSETA : 'LDSETA' ;
@@ -469,7 +494,6 @@ LDSETB : 'LDSETB' ;
469494
LDSETAB : 'LDSETAB' ;
470495
LDSETLB : 'LDSETLB' ;
471496
LDSETALB : 'LDSETALB' ;
472-
473497
// CLR (AND with complement)
474498
LDCLR : 'LDCLR' ;
475499
LDCLRA : 'LDCLRA' ;
@@ -484,6 +508,36 @@ LDCLRAB : 'LDCLRAB' ;
484508
LDCLRLB : 'LDCLRLB' ;
485509
LDCLRALB : 'LDCLRALB' ;
486510

511+
// Store Op instructions
512+
// Add
513+
STADD : 'STADD' ;
514+
STADDL : 'STADDL' ;
515+
STADDH : 'STADDH' ;
516+
STADDLH : 'STADDLH' ;
517+
STADDB : 'STADDB' ;
518+
STADDLB : 'STADDLB' ;
519+
// EOR (XOR)
520+
STEOR : 'STEOR' ;
521+
STEORL : 'STEORL' ;
522+
STEORH : 'STEORH' ;
523+
STEORLH : 'STEORLH' ;
524+
STEORB : 'STEORB' ;
525+
STEORLB : 'STEORLB' ;
526+
// SET (OR)
527+
STSET : 'STSET' ;
528+
STSETL : 'STSETL' ;
529+
STSETH : 'STSETH' ;
530+
STSETLH : 'STSETLH' ;
531+
STSETB : 'STSETB' ;
532+
STSETLB : 'STSETLB' ;
533+
// CLR (AND with complement)
534+
STCLR : 'STCLR' ;
535+
STCLRL : 'STCLRL' ;
536+
STCLRH : 'STCLRH' ;
537+
STCLRLH : 'STCLRLH' ;
538+
STCLRB : 'STCLRB' ;
539+
STCLRLB : 'STCLRLB' ;
540+
487541

488542
// Swap word instructions (~ Exchange)
489543

‎dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java‎

Lines changed: 89 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
import com.dat3m.dartagnan.exception.ParsingException;
55
import com.dat3m.dartagnan.expression.Expression;
66
import com.dat3m.dartagnan.expression.ExpressionFactory;
7+
import com.dat3m.dartagnan.expression.Type;
78
import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
89
import com.dat3m.dartagnan.expression.integers.IntLiteral;
910
import com.dat3m.dartagnan.expression.integers.IntUnaryExpr;
@@ -20,6 +21,7 @@
2021
import com.dat3m.dartagnan.program.event.RegWriter;
2122
import com.dat3m.dartagnan.program.event.arch.CAS;
2223
import com.dat3m.dartagnan.program.event.arch.RMWFetchOp;
24+
import com.dat3m.dartagnan.program.event.arch.RMWOp;
2325
import com.dat3m.dartagnan.program.event.arch.Xchg;
2426
import com.dat3m.dartagnan.program.event.core.Label;
2527
import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
@@ -351,35 +353,11 @@ public Object visitCas(CasContext ctx) {
351353
return null;
352354
}
353355

354-
private static final CustomPrinting LDOP_PRINTER = e -> {
355-
if (!(e instanceof RMWFetchOp ldop)) {
356-
return Optional.empty();
357-
}
358-
final String acq = e.hasTag(MO_ACQ) ? "A" : "";
359-
final String rel = e.hasTag(MO_REL) ? "L" : "";
360-
final String op = switch (ldop.getOperator()) {
361-
case ADD -> "ADD";
362-
case XOR -> "EOR";
363-
case OR -> "SET";
364-
case AND -> "CLR";
365-
default -> throw new RuntimeException("Invalid load op: " + ldop.getOperator());
366-
};
367-
final String size = switch (((IntegerType)ldop.getResultRegister().getType()).getBitWidth()) {
368-
case 16 -> "H";
369-
case 8 -> "B";
370-
default -> "";
371-
};
372-
final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ? expr.getOperand() : ldop.getOperand();
373-
final Register loadReg = ldop.getResultRegister();
374-
final Expression address = ldop.getAddress();
356+
record RMWInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {}
375357

376-
return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
377-
};
378-
379-
@Override
380-
public Object visitLoadOp(LoadOpContext ctx) {
381-
String instr = ctx.loadOpInstruction().getText();
382-
instr = instr.substring(2); // Skip LD
358+
// Used for LDXXX and STXXX instructions
359+
private RMWInfo getInfoFromInstructionName(String instrName) {
360+
String instr = instrName.substring(2); // Skip LD/ST
383361

384362
// TODO: Maybe the following logic can be implemented in the grammar without
385363
// an explicit case distinction over all 48 (or more?) variants of LD
@@ -389,8 +367,8 @@ public Object visitLoadOp(LoadOpContext ctx) {
389367
case "ADD" -> IntBinaryOp.ADD;
390368
case "EOR" -> IntBinaryOp.XOR;
391369
case "SET" -> IntBinaryOp.OR;
392-
case "CLR" -> IntBinaryOp.AND;
393-
default -> throw new ParsingException("Invalid load op: " + instr);
370+
case "CLR" -> IntBinaryOp.AND; // Actually & with complement!!!
371+
default -> throw new ParsingException("Invalid op " + opCode + " found in " + instrName);
394372
};
395373
instr = instr.substring(3);
396374

@@ -409,25 +387,84 @@ public Object visitLoadOp(LoadOpContext ctx) {
409387
final boolean isHalfSize = instr.startsWith("H");
410388
final boolean isByteSize = instr.startsWith("B");
411389

390+
return new RMWInfo(op, isHalfSize, isByteSize, acquire, release);
391+
}
392+
393+
private static final CustomPrinting LDOP_PRINTER = e -> {
394+
if (!(e instanceof RMWFetchOp ldop)) {
395+
return Optional.empty();
396+
}
397+
final String acq = e.hasTag(MO_ACQ) ? "A" : "";
398+
final String rel = e.hasTag(MO_REL) ? "L" : "";
399+
final String op = OpToArmOpCode(ldop.getOperator());
400+
final String size = getArmSizeSuffix(ldop.getAccessType());
401+
final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ? expr.getOperand() : ldop.getOperand();
402+
final Register loadReg = ldop.getResultRegister();
403+
final Expression address = ldop.getAddress();
404+
405+
return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
406+
};
407+
408+
@Override
409+
public Object visitLoadOp(LoadOpContext ctx) {
410+
final String instr = ctx.loadOpInstruction().getText();
411+
final RMWInfo info = getInfoFromInstructionName(instr);
412412

413413
final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
414414
final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
415-
final Register rt = shrinkRegister(rt64, ctx.rD32, isHalfSize, isByteSize);
415+
final Register rt = shrinkRegister(rt64, ctx.rD32, info.isHalfSize, info.isByteSize);
416416
Expression operand = expressions.makeCast(rs64, rt.getType(), false);
417-
if (opCode.equals("CLR")) {
417+
if (info.op == IntBinaryOp.AND) {
418+
// This was a CLR instruction
418419
operand = expressions.makeIntNot(operand);
419420
}
420421

421422
final Expression address = parseAddress(ctx.address());
422-
final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, op, operand);
423-
ldOp.addTags(release ? MO_REL : null, acquire ? MO_ACQ : null);
423+
final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, info.op, operand);
424+
ldOp.addTags(info.release ? MO_REL : null, info.acquire ? MO_ACQ : null);
424425
ldOp.setMetadata(LDOP_PRINTER);
425426

426427
add(ldOp);
427428
addRegister64Update(rt64, rt);
428429
return null;
429430
}
430431

432+
private static final CustomPrinting STOP_PRINTER = e -> {
433+
if (!(e instanceof RMWOp stop)) {
434+
return Optional.empty();
435+
}
436+
final String rel = e.hasTag(MO_REL) ? "L" : "";
437+
final String op = OpToArmOpCode(stop.getOperator());
438+
final String size = getArmSizeSuffix(stop.getAccessType());
439+
final Expression operand = stop.getOperand() instanceof IntUnaryExpr expr ? expr.getOperand() : stop.getOperand();
440+
final Expression address = stop.getAddress();
441+
442+
return Optional.of(String.format("ST%s%s%s %s, [%s]", op, rel, size, operand, address));
443+
};
444+
445+
@Override
446+
public Object visitStoreOp(StoreOpContext ctx) {
447+
final String instr = ctx.storeOpInstruction().getText();
448+
final RMWInfo info = getInfoFromInstructionName(instr);
449+
450+
final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
451+
// TODO: We don't actually care about the smaller register, but only its type!
452+
final Register rs = shrinkRegister(rs64, ctx.rS32, info.isHalfSize, info.isByteSize);
453+
Expression operand = expressions.makeCast(rs64, rs.getType(), false);
454+
if (info.op == IntBinaryOp.AND) {
455+
// This was a CLR instruction
456+
operand = expressions.makeIntNot(operand);
457+
}
458+
459+
final Expression address = parseAddress(ctx.address());
460+
final RMWOp stOp = EventFactory.Common.newRmwOp(address, info.op, operand);
461+
stOp.addTags(info.release ? MO_REL : null);
462+
stOp.setMetadata(STOP_PRINTER);
463+
464+
add(stOp);
465+
return null;
466+
}
467+
431468
@Override
432469
public Object visitBranch(BranchContext ctx) {
433470
Label label = programBuilder.getOrCreateLabel(mainThread, ctx.label().getText());
@@ -587,4 +624,22 @@ private Void add(Event event) {
587624
programBuilder.addChild(mainThread, event);
588625
return null;
589626
}
627+
628+
private static String OpToArmOpCode(IntBinaryOp op) {
629+
return switch (op) {
630+
case ADD -> "ADD";
631+
case XOR -> "EOR";
632+
case OR -> "SET";
633+
case AND -> "CLR";
634+
default -> throw new RuntimeException("Invalid op: " + op);
635+
};
636+
}
637+
638+
private static String getArmSizeSuffix(Type type) {
639+
return switch (((IntegerType) type).getBitWidth()) {
640+
case 16 -> "H";
641+
case 8 -> "B";
642+
default -> "";
643+
};
644+
}
590645
}

‎dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,10 +105,11 @@ public List<Event> visitRMWOp(RMWOp rmwOp) {
105105
final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
106106

107107
final Load load = propagateNoRet(rmwOp, newRMWLoad(dummy, address));
108+
load.addTags(Tag.ARMv8.NO_RET);
108109
final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
109110

110111
return eventSequence(
111-
propagateNoRet(rmwOp, load),
112+
load,
112113
newRMWStoreWithMo(load, address, value, storeMo)
113114
);
114115
}

0 commit comments

Comments
 (0)