diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 152c34d8e4..bae408b323 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -76,6 +76,8 @@ instruction
| branchRegister
| branchLabel
| fence
+ | return
+ | nop
;
mov locals [String rD, int size]
@@ -131,6 +133,14 @@ branchLabel
: label Colon
;
+return
+ : Ret
+ ;
+
+nop
+ : Nop
+ ;
+
loadInstruction locals [String mo]
: LDR {$mo = MO_RX;}
| LDAR {$mo = MO_ACQ;}
@@ -252,7 +262,7 @@ location
;
immediate
- : Num constant
+ : Num Hexa? constant
;
label
@@ -265,6 +275,18 @@ assertionValue
| constant
;
+Hexa
+ : '0x'
+ ;
+
+Ret
+ : 'ret'
+ ;
+
+Nop
+ : 'nop'
+ ;
+
Locations
: 'locations'
;
@@ -371,10 +393,12 @@ BitfieldOperator
Register64
: 'X' DigitSequence
+ | 'XZR' // zero register
;
Register32
: 'W' DigitSequence
+ | 'WZR' // zero register
;
LitmusLanguage
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
index b0bff0d508..1d1e773a9a 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
@@ -7,12 +7,14 @@
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.integers.IntLiteral;
import com.dat3m.dartagnan.expression.type.FunctionType;
+import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.*;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.Program.SourceLanguage;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.RegWriter;
import com.dat3m.dartagnan.program.event.core.Label;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
import com.dat3m.dartagnan.program.event.metadata.OriginalId;
@@ -89,6 +91,27 @@ public static void processAfterParsing(Program program) {
}
}
+ public static void replaceZeroRegisters(Program program, List<String> zeroRegNames) {
+ for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
+ if (func.hasBody()) {
+ for (String zeroRegName : zeroRegNames) {
+ Register zr = func.getRegister(zeroRegName);
+ if (zr != null) {
+ for (RegWriter rw : func.getEvents(RegWriter.class)) {
+ if (rw.getResultRegister().equals(zr)) {
+ Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
+ rw.setResultRegister(dummy);
+ }
+ }
+ // This comes after the loop to avoid the renaming in the initialization event
+ Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType()));
+ func.getEntry().insertAfter(initToZero);
+ }
+ }
+ }
+ }
+ }
+
// ----------------------------------------------------------------------------------------------------------------
// Misc
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index 4c0d1e5091..455c285ad0 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -17,9 +17,13 @@
import com.dat3m.dartagnan.program.event.core.Label;
import com.dat3m.dartagnan.program.event.core.Load;
+import java.math.BigInteger;
+import java.util.Arrays;
import java.util.HashMap;
import java.util.Map;
+import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
+
public class VisitorLitmusAArch64 extends LitmusAArch64BaseVisitor<Object> {
private static class CmpInstruction {
@@ -53,10 +57,11 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) {
visitVariableDeclaratorList(ctx.variableDeclaratorList());
visitInstructionList(ctx.program().instructionList());
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
- return programBuilder.build();
+ Program prog = programBuilder.build();
+ replaceZeroRegisters(prog, Arrays.asList("XZR, WZR"));
+ return prog;
}
-
// ----------------------------------------------------------------------------------------------------------------
// Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; }
@@ -211,6 +216,12 @@ public Object visitFence(LitmusAArch64Parser.FenceContext ctx) {
return programBuilder.addChild(mainThread, EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt));
}
+ @Override
+ public Object visitReturn(LitmusAArch64Parser.ReturnContext ctx) {
+ Label end = programBuilder.getEndOfThreadLabel(mainThread);
+ return programBuilder.addChild(mainThread, EventFactory.newGoto(end));
+ }
+
@Override
public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) {
Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType);
@@ -255,4 +266,12 @@ private Register visitOffset(LitmusAArch64Parser.OffsetContext ctx, Register reg
programBuilder.addChild(mainThread, EventFactory.newLocal(result, expressions.makeAdd(register, expr)));
return result;
}
+
+ @Override
+ public Expression visitImmediate(LitmusAArch64Parser.ImmediateContext ctx) {
+ final int radix = ctx.Hexa() != null ? 16 : 10;
+ BigInteger value = new BigInteger(ctx.constant().getText(), radix);
+ return expressions.makeValue(value, archType);
+ }
+
}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java
index 8959730977..92568decfd 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java
@@ -1,12 +1,11 @@
package com.dat3m.dartagnan.parsers.program.visitors;
+import java.util.Arrays;
import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.exception.ParsingException;
import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.ExpressionVisitor;
import com.dat3m.dartagnan.expression.integers.IntLiteral;
-import com.dat3m.dartagnan.expression.processing.ExprTransformer;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.parsers.LitmusRISCVBaseVisitor;
@@ -16,10 +15,11 @@
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.EventFactory;
-import com.dat3m.dartagnan.program.event.RegReader;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.event.core.Label;
+import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
+
public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor<Object> {
private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.RISCV);
@@ -42,32 +42,10 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) {
visitInstructionList(ctx.program().instructionList());
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
Program prog = programBuilder.build();
- replaceX0Register(prog);
-
+ replaceZeroRegisters(prog, Arrays.asList("x0"));
return prog;
}
- /*
- The "x0" register plays a special role in RISCV:
- 1. Reading accesses always return the value 0.
- 2. Writing accesses are discarded.
- TODO: The below code is a simple fix to guarantee point 1. above.
- Point 2. might also be resolved: although we do not prevent writing to x0,
- the value of x0 is never read after the transformation so its value is effectively 0.
- However, the exists/forall clauses could still refer to that register and observe a non-zero value.
- */
- private void replaceX0Register(Program program) {
- final ExpressionVisitor<Expression> x0Replacer = new ExprTransformer() {
- @Override
- public Expression visitRegister(Register reg) {
- return reg.getName().equals("x0") ? expressions.makeGeneralZero(reg.getType()) : reg;
- }
- };
- program.getThreadEvents(RegReader.class)
- .forEach(e -> e.transformExpressions(x0Replacer));
- }
-
-
// ----------------------------------------------------------------------------------------------------------------
// Variable declarator list
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index 60b209d087..451fc3678c 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
@@ -96,7 +96,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
ComplexBlockSplitting.newInstance(),
BranchReordering.fromConfig(config),
Simplifier.fromConfig(config)
- ), Target.FUNCTIONS, true
+ ), Target.ALL, true
),
ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true),
RegisterDecomposition.newInstance(),
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
index c02bd2aa9a..32db0c5cff 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
@@ -238,16 +238,8 @@ private EventGraph computeInternalDependencies(Set<Register.UsageType> usageType
reader.getRegisterReads().forEach(read -> {
if (usageTypes.contains(read.usageType())) {
Register register = read.register();
- // TODO: Update after this is merged
- // https://github.com/hernanponcedeleon/Dat3M/pull/741
- // Register x0 is hardwired to the constant 0 in RISCV
- // https://en.wikichip.org/wiki/risc-v/registers,
- // and thus it generates no dependency, see
- // https://github.com/herd/herdtools7/issues/408
- if (!program.getArch().equals(RISCV) || !register.getName().equals("x0")) {
- state.ofRegister(register).getMayWriters().forEach(writer ->
- data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
- }
+ state.ofRegister(register).getMayWriters()
+ .forEach(writer -> data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
}
});
});
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java
index dca921255b..e2cf68ff7b 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java
@@ -40,7 +40,6 @@
import java.util.stream.Collectors;
import java.util.stream.Stream;
-import static com.dat3m.dartagnan.configuration.Arch.RISCV;
import static com.dat3m.dartagnan.program.Register.UsageType.*;
import static com.dat3m.dartagnan.program.event.Tag.*;
import static com.google.common.base.Preconditions.checkArgument;
@@ -915,16 +914,6 @@ private MutableKnowledge computeInternalDependencies(Set<UsageType> usageTypes)
continue;
}
final Register register = regRead.register();
- // TODO: Update after this is merged
- // https://github.com/hernanponcedeleon/Dat3M/pull/741
- // Register x0 is hardwired to the constant 0 in RISCV
- // https://en.wikichip.org/wiki/risc-v/registers,
- // and thus it generates no dependency, see
- // https://github.com/herd/herdtools7/issues/408
- // TODO: Can't we just replace all reads of "x0" by 0 in RISC-specific preprocessing?
- if (program.getArch().equals(RISCV) && register.getName().equals("x0")) {
- continue;
- }
final List<? extends Event> writers = state.ofRegister(register).getMayWriters();
for (Event regWriter : writers) {
may.add(regWriter, regReader);