Skip to content

Commit 95fe0c3

Browse files
hernanponcedeleonhernanponcedeleon
authored
Some improvements to aarch64 pseudo-assembly (#741)
Signed-off-by: Hernan Ponce de Leon <[email protected]>
1 parent 2d6ef05 commit 95fe0c3

File tree

7 files changed

+76
-51
lines changed

7 files changed

+76
-51
lines changed

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

Lines changed: 25 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,8 @@ instruction
7676
| branchRegister
7777
| branchLabel
7878
| fence
79+
| return
80+
| nop
7981
;
8082

8183
mov locals [String rD, int size]
@@ -131,6 +133,14 @@ branchLabel
131133
: label Colon
132134
;
133135

136+
return
137+
: Ret
138+
;
139+
140+
nop
141+
: Nop
142+
;
143+
134144
loadInstruction locals [String mo]
135145
: LDR {$mo = MO_RX;}
136146
| LDAR {$mo = MO_ACQ;}
@@ -252,7 +262,7 @@ location
252262
;
253263

254264
immediate
255-
: Num constant
265+
: Num Hexa? constant
256266
;
257267

258268
label
@@ -265,6 +275,18 @@ assertionValue
265275
| constant
266276
;
267277

278+
Hexa
279+
: '0x'
280+
;
281+
282+
Ret
283+
: 'ret'
284+
;
285+
286+
Nop
287+
: 'nop'
288+
;
289+
268290
Locations
269291
: 'locations'
270292
;
@@ -371,10 +393,12 @@ BitfieldOperator
371393

372394
Register64
373395
: 'X' DigitSequence
396+
| 'XZR' // zero register
374397
;
375398

376399
Register32
377400
: 'W' DigitSequence
401+
| 'WZR' // zero register
378402
;
379403

380404
LitmusLanguage

‎dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,14 @@
77
import com.dat3m.dartagnan.expression.Type;
88
import com.dat3m.dartagnan.expression.integers.IntLiteral;
99
import com.dat3m.dartagnan.expression.type.FunctionType;
10+
import com.dat3m.dartagnan.expression.type.IntegerType;
1011
import com.dat3m.dartagnan.expression.type.TypeFactory;
1112
import com.dat3m.dartagnan.program.*;
1213
import com.dat3m.dartagnan.program.Thread;
1314
import com.dat3m.dartagnan.program.Program.SourceLanguage;
1415
import com.dat3m.dartagnan.program.event.Event;
1516
import com.dat3m.dartagnan.program.event.EventFactory;
17+
import com.dat3m.dartagnan.program.event.RegWriter;
1618
import com.dat3m.dartagnan.program.event.core.Label;
1719
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
1820
import com.dat3m.dartagnan.program.event.metadata.OriginalId;
@@ -89,6 +91,27 @@ public static void processAfterParsing(Program program) {
8991
}
9092
}
9193

94+
public static void replaceZeroRegisters(Program program, List<String> zeroRegNames) {
95+
for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
96+
if (func.hasBody()) {
97+
for (String zeroRegName : zeroRegNames) {
98+
Register zr = func.getRegister(zeroRegName);
99+
if (zr != null) {
100+
for (RegWriter rw : func.getEvents(RegWriter.class)) {
101+
if (rw.getResultRegister().equals(zr)) {
102+
Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
103+
rw.setResultRegister(dummy);
104+
}
105+
}
106+
// This comes after the loop to avoid the renaming in the initialization event
107+
Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType()));
108+
func.getEntry().insertAfter(initToZero);
109+
}
110+
}
111+
}
112+
}
113+
}
114+
92115
// ----------------------------------------------------------------------------------------------------------------
93116
// Misc
94117

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

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,13 @@
1717
import com.dat3m.dartagnan.program.event.core.Label;
1818
import com.dat3m.dartagnan.program.event.core.Load;
1919

20+
import java.math.BigInteger;
21+
import java.util.Arrays;
2022
import java.util.HashMap;
2123
import java.util.Map;
2224

25+
import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
26+
2327
public class VisitorLitmusAArch64 extends LitmusAArch64BaseVisitor<Object> {
2428

2529
private static class CmpInstruction {
@@ -53,10 +57,11 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) {
5357
visitVariableDeclaratorList(ctx.variableDeclaratorList());
5458
visitInstructionList(ctx.program().instructionList());
5559
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
56-
return programBuilder.build();
60+
Program prog = programBuilder.build();
61+
replaceZeroRegisters(prog, Arrays.asList("XZR, WZR"));
62+
return prog;
5763
}
5864

59-
6065
// ----------------------------------------------------------------------------------------------------------------
6166
// Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; }
6267

@@ -211,6 +216,12 @@ public Object visitFence(LitmusAArch64Parser.FenceContext ctx) {
211216
return programBuilder.addChild(mainThread, EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt));
212217
}
213218

219+
@Override
220+
public Object visitReturn(LitmusAArch64Parser.ReturnContext ctx) {
221+
Label end = programBuilder.getEndOfThreadLabel(mainThread);
222+
return programBuilder.addChild(mainThread, EventFactory.newGoto(end));
223+
}
224+
214225
@Override
215226
public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) {
216227
Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType);
@@ -255,4 +266,12 @@ private Register visitOffset(LitmusAArch64Parser.OffsetContext ctx, Register reg
255266
programBuilder.addChild(mainThread, EventFactory.newLocal(result, expressions.makeAdd(register, expr)));
256267
return result;
257268
}
269+
270+
@Override
271+
public Expression visitImmediate(LitmusAArch64Parser.ImmediateContext ctx) {
272+
final int radix = ctx.Hexa() != null ? 16 : 10;
273+
BigInteger value = new BigInteger(ctx.constant().getText(), radix);
274+
return expressions.makeValue(value, archType);
275+
}
276+
258277
}

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

Lines changed: 4 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
11
package com.dat3m.dartagnan.parsers.program.visitors;
22

3+
import java.util.Arrays;
34
import com.dat3m.dartagnan.configuration.Arch;
45
import com.dat3m.dartagnan.exception.ParsingException;
56
import com.dat3m.dartagnan.expression.Expression;
67
import com.dat3m.dartagnan.expression.ExpressionFactory;
7-
import com.dat3m.dartagnan.expression.ExpressionVisitor;
88
import com.dat3m.dartagnan.expression.integers.IntLiteral;
9-
import com.dat3m.dartagnan.expression.processing.ExprTransformer;
109
import com.dat3m.dartagnan.expression.type.IntegerType;
1110
import com.dat3m.dartagnan.expression.type.TypeFactory;
1211
import com.dat3m.dartagnan.parsers.LitmusRISCVBaseVisitor;
@@ -16,10 +15,11 @@
1615
import com.dat3m.dartagnan.program.Register;
1716
import com.dat3m.dartagnan.program.event.Event;
1817
import com.dat3m.dartagnan.program.event.EventFactory;
19-
import com.dat3m.dartagnan.program.event.RegReader;
2018
import com.dat3m.dartagnan.program.event.Tag;
2119
import com.dat3m.dartagnan.program.event.core.Label;
2220

21+
import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
22+
2323
public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor<Object> {
2424

2525
private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.RISCV);
@@ -42,32 +42,10 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) {
4242
visitInstructionList(ctx.program().instructionList());
4343
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
4444
Program prog = programBuilder.build();
45-
replaceX0Register(prog);
46-
45+
replaceZeroRegisters(prog, Arrays.asList("x0"));
4746
return prog;
4847
}
4948

50-
/*
51-
The "x0" register plays a special role in RISCV:
52-
1. Reading accesses always return the value 0.
53-
2. Writing accesses are discarded.
54-
TODO: The below code is a simple fix to guarantee point 1. above.
55-
Point 2. might also be resolved: although we do not prevent writing to x0,
56-
the value of x0 is never read after the transformation so its value is effectively 0.
57-
However, the exists/forall clauses could still refer to that register and observe a non-zero value.
58-
*/
59-
private void replaceX0Register(Program program) {
60-
final ExpressionVisitor<Expression> x0Replacer = new ExprTransformer() {
61-
@Override
62-
public Expression visitRegister(Register reg) {
63-
return reg.getName().equals("x0") ? expressions.makeGeneralZero(reg.getType()) : reg;
64-
}
65-
};
66-
program.getThreadEvents(RegReader.class)
67-
.forEach(e -> e.transformExpressions(x0Replacer));
68-
}
69-
70-
7149
// ----------------------------------------------------------------------------------------------------------------
7250
// Variable declarator list
7351

‎dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
9696
ComplexBlockSplitting.newInstance(),
9797
BranchReordering.fromConfig(config),
9898
Simplifier.fromConfig(config)
99-
), Target.FUNCTIONS, true
99+
), Target.ALL, true
100100
),
101101
ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true),
102102
RegisterDecomposition.newInstance(),

‎dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -238,16 +238,8 @@ private EventGraph computeInternalDependencies(Set<Register.UsageType> usageType
238238
reader.getRegisterReads().forEach(read -> {
239239
if (usageTypes.contains(read.usageType())) {
240240
Register register = read.register();
241-
// TODO: Update after this is merged
242-
// https://github.com/hernanponcedeleon/Dat3M/pull/741
243-
// Register x0 is hardwired to the constant 0 in RISCV
244-
// https://en.wikichip.org/wiki/risc-v/registers,
245-
// and thus it generates no dependency, see
246-
// https://github.com/herd/herdtools7/issues/408
247-
if (!program.getArch().equals(RISCV) || !register.getName().equals("x0")) {
248-
state.ofRegister(register).getMayWriters().forEach(writer ->
249-
data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
250-
}
241+
state.ofRegister(register).getMayWriters()
242+
.forEach(writer -> data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
251243
}
252244
});
253245
});

‎dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,6 @@
4040
import java.util.stream.Collectors;
4141
import java.util.stream.Stream;
4242

43-
import static com.dat3m.dartagnan.configuration.Arch.RISCV;
4443
import static com.dat3m.dartagnan.program.Register.UsageType.*;
4544
import static com.dat3m.dartagnan.program.event.Tag.*;
4645
import static com.google.common.base.Preconditions.checkArgument;
@@ -915,16 +914,6 @@ private MutableKnowledge computeInternalDependencies(Set<UsageType> usageTypes)
915914
continue;
916915
}
917916
final Register register = regRead.register();
918-
// TODO: Update after this is merged
919-
// https://github.com/hernanponcedeleon/Dat3M/pull/741
920-
// Register x0 is hardwired to the constant 0 in RISCV
921-
// https://en.wikichip.org/wiki/risc-v/registers,
922-
// and thus it generates no dependency, see
923-
// https://github.com/herd/herdtools7/issues/408
924-
// TODO: Can't we just replace all reads of "x0" by 0 in RISC-specific preprocessing?
925-
if (program.getArch().equals(RISCV) && register.getName().equals("x0")) {
926-
continue;
927-
}
928917
final List<? extends Event> writers = state.ofRegister(register).getMayWriters();
929918
for (Event regWriter : writers) {
930919
may.add(regWriter, regReader);

0 commit comments

Comments
 (0)