Skip to content

Refactor EventFactory, Compilers and Parsers #1009

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
xeren wants to merge 9 commits into
base: development
Choose a base branch
from
Open

Refactor EventFactory, Compilers and Parsers #1009

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
595744e
Refactor
xeren Jan 12, 2026
62a9f58
fixup! Refactor
xeren Mar 16, 2026
5977ce6
Merge remote-tracking branch 'origin/development' into refactorEventF…
xeren Mar 25, 2026
952ad54
fixup! Refactor
xeren Mar 26, 2026
b6d6ab2
Move newRMWLoadExclusive from EventFactory to compilers
xeren Mar 26, 2026
0385200
fixup! Move newRMWLoadExclusive from EventFactory to compilers
xeren Mar 26, 2026
ebd62db
fixup! Move newRMWLoadExclusive from EventFactory to compilers
xeren Mar 26, 2026
c3acefb
Refactor VisitorLitmusAArch64
xeren Mar 26, 2026
b82a538
fixup! Refactor VisitorLitmusAArch64
xeren Mar 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 33 additions & 57 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorAsmArm.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
package com.dat3m.dartagnan.parsers.program.visitors;

import com.dat3m.dartagnan.exception.ParsingException;
import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.integers.IntCmpOp;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.parsers.AsmArmBaseVisitor;
import com.dat3m.dartagnan.parsers.AsmArmParser;
import com.dat3m.dartagnan.parsers.AsmArmParser.*;
import com.dat3m.dartagnan.parsers.program.utils.AsmUtils;
import com.dat3m.dartagnan.program.Function;
import com.dat3m.dartagnan.program.Register;
Expand Down Expand Up @@ -126,7 +125,7 @@ public VisitorAsmArm(Function llvmFunction, Register returnRegister, List<Expres
// The visitor will first visit the asm code (which will create the events and asm registers) and then the constraints.
// The latter will take care of creating input and output assignments.
@Override
public List<Event> visitAsm(AsmArmParser.AsmContext ctx) {
public List<Event> visitAsm(AsmContext ctx) {
visitChildren(ctx);
List<Event> events = new ArrayList<>();
events.addAll(inputAssignments);
Expand All @@ -136,59 +135,59 @@ public List<Event> visitAsm(AsmArmParser.AsmContext ctx) {
}

// Tells if a constraint is a numeric one, e.g. '3'
private boolean isConstraintNumeric(AsmArmParser.ConstraintContext constraint) {
private boolean isConstraintNumeric(ConstraintContext constraint) {
return constraint.overlapInOutRegister() != null;
}

// Tells if the constraint is a memory location '=*m'
private boolean isConstraintMemoryLocation(AsmArmParser.ConstraintContext constraint) {
private boolean isConstraintMemoryLocation(ConstraintContext constraint) {
return constraint.pointerToMemoryLocation() != null;
}

// Tells if the constraint is an output one, e.g. '=r' or '=&r'
private boolean isConstraintOutputConstraint(AsmArmParser.ConstraintContext constraint) {
private boolean isConstraintOutputConstraint(ConstraintContext constraint) {
return constraint.outputOpAssign() != null;
}

// Tells us if the constraint is an input one, e.g. 'Q' or '*Q' or 'r'
private boolean isConstraintInputConstraint(AsmArmParser.ConstraintContext constraint) {
private boolean isConstraintInputConstraint(ConstraintContext constraint) {
return constraint.memoryAddress() != null || constraint.inputOpGeneralReg() != null;
}

@Override
public Object visitLoad(AsmArmParser.LoadContext ctx) {
public Object visitLoad(LoadContext ctx) {
Register register = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newLoad(register, address));
return null;
}

@Override
public Object visitLoadAcquire(AsmArmParser.LoadAcquireContext ctx) {
public Object visitLoadAcquire(LoadAcquireContext ctx) {
Register register = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newLoadWithMo(register, address, Tag.ARMv8.MO_ACQ));
return null;
}

@Override
public Object visitLoadExclusive(AsmArmParser.LoadExclusiveContext ctx) {
public Object visitLoadExclusive(LoadExclusiveContext ctx) {
Register register = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newRMWLoadExclusive(register, address));
return null;
}

@Override
public Object visitLoadAcquireExclusive(AsmArmParser.LoadAcquireExclusiveContext ctx) {
public Object visitLoadAcquireExclusive(LoadAcquireExclusiveContext ctx) {
Register register = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newRMWLoadExclusiveWithMo(register, address, Tag.ARMv8.MO_ACQ));
return null;
}

@Override
public Object visitAdd(AsmArmParser.AddContext ctx) {
public Object visitAdd(AddContext ctx) {
Register resultRegister = (Register) ctx.register(0).accept(this);
Register lhs = (Register) ctx.register(1).accept(this);
expectedType = lhs.getType();
Expand All @@ -199,7 +198,7 @@ public Object visitAdd(AsmArmParser.AddContext ctx) {
}

@Override
public Object visitSub(AsmArmParser.SubContext ctx) {
public Object visitSub(SubContext ctx) {
Register resultRegister = (Register) ctx.register(0).accept(this);
Register lhs = (Register) ctx.register(1).accept(this);
expectedType = lhs.getType();
Expand All @@ -210,7 +209,7 @@ public Object visitSub(AsmArmParser.SubContext ctx) {
}

@Override
public Object visitOr(AsmArmParser.OrContext ctx) {
public Object visitOr(OrContext ctx) {
Register resultRegister = (Register) ctx.register(0).accept(this);
Register leftRegister = (Register) ctx.register(1).accept(this);
Register rightRegister = (Register) ctx.register(2).accept(this);
Expand All @@ -220,7 +219,7 @@ public Object visitOr(AsmArmParser.OrContext ctx) {
}

@Override
public Object visitAnd(AsmArmParser.AndContext ctx) {
public Object visitAnd(AndContext ctx) {
Register resultRegister = (Register) ctx.register(0).accept(this);
Register leftRegister = (Register) ctx.register(1).accept(this);
Register rightRegister = (Register) ctx.register(2).accept(this);
Expand All @@ -230,23 +229,23 @@ public Object visitAnd(AsmArmParser.AndContext ctx) {
}

@Override
public Object visitStore(AsmArmParser.StoreContext ctx) {
public Object visitStore(StoreContext ctx) {
Register value = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newStore(address, value));
return null;
}

@Override
public Object visitStoreRelease(AsmArmParser.StoreReleaseContext ctx) {
public Object visitStoreRelease(StoreReleaseContext ctx) {
Register value = (Register) ctx.register(0).accept(this);
Register address = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newStoreWithMo(address, value, Tag.ARMv8.MO_REL));
return null;
}

@Override
public Object visitStoreExclusive(AsmArmParser.StoreExclusiveContext ctx) {
public Object visitStoreExclusive(StoreExclusiveContext ctx) {
Register freshResultRegister = (Register) ctx.register(0).accept(this);
Register value = (Register) ctx.register(1).accept(this);
Register address = (Register) ctx.register(2).accept(this);
Expand All @@ -255,7 +254,7 @@ public Object visitStoreExclusive(AsmArmParser.StoreExclusiveContext ctx) {
}

@Override
public Object visitStoreReleaseExclusive(AsmArmParser.StoreReleaseExclusiveContext ctx) {
public Object visitStoreReleaseExclusive(StoreReleaseExclusiveContext ctx) {
Register freshResultRegister = (Register) ctx.register(0).accept(this);
Register value = (Register) ctx.register(1).accept(this);
Register address = (Register) ctx.register(2).accept(this);
Expand All @@ -264,7 +263,7 @@ public Object visitStoreReleaseExclusive(AsmArmParser.StoreReleaseExclusiveConte
}

@Override
public Object visitCompare(AsmArmParser.CompareContext ctx) {
public Object visitCompare(CompareContext ctx) {
Register firstRegister = (Register) ctx.register().accept(this);
expectedType = firstRegister.getType();
Expression secondRegister = (Expression) ctx.expr().accept(this);
Expand All @@ -273,7 +272,7 @@ public Object visitCompare(AsmArmParser.CompareContext ctx) {
}

@Override
public Object visitCompareBranchNonZero(AsmArmParser.CompareBranchNonZeroContext ctx) {
public Object visitCompareBranchNonZero(CompareBranchNonZeroContext ctx) {
Label label = AsmUtils.getOrNewLabel(labelsDefined, ctx.Numbers().getText());
Register firstRegister = (Register) ctx.register().accept(this);
Expression zero = expressions.makeZero((IntegerType) firstRegister.getType());
Expand All @@ -283,31 +282,31 @@ public Object visitCompareBranchNonZero(AsmArmParser.CompareBranchNonZeroContext
}

@Override
public Object visitMove(AsmArmParser.MoveContext ctx) {
public Object visitMove(MoveContext ctx) {
Register toRegister = (Register) ctx.register(0).accept(this);
Register fromRegister = (Register) ctx.register(1).accept(this);
asmInstructions.add(EventFactory.newLocal(toRegister, fromRegister));
return null;
}

@Override
public Object visitBranchEqual(AsmArmParser.BranchEqualContext ctx) {
public Object visitBranchEqual(BranchEqualContext ctx) {
Label label = AsmUtils.getOrNewLabel(labelsDefined, ctx.Numbers().getText());
Expression expr = expressions.makeIntCmp(comparator.left(), IntCmpOp.EQ, comparator.right());
asmInstructions.add(EventFactory.newJump(expr, label));
return null;
}

@Override
public Object visitBranchNotEqual(AsmArmParser.BranchNotEqualContext ctx) {
public Object visitBranchNotEqual(BranchNotEqualContext ctx) {
Label label = AsmUtils.getOrNewLabel(labelsDefined, ctx.Numbers().getText());
Expression expr = expressions.makeIntCmp(comparator.left(), IntCmpOp.NEQ, comparator.right());
asmInstructions.add(EventFactory.newJump(expr, label));
return null;
}

@Override
public Object visitLabelDefinition(AsmArmParser.LabelDefinitionContext ctx) {
public Object visitLabelDefinition(LabelDefinitionContext ctx) {
String labelID = ctx.Numbers().getText();
Label label = AsmUtils.getOrNewLabel(labelsDefined, labelID);
asmInstructions.add(label);
Expand All @@ -320,7 +319,7 @@ public Object visitLabelDefinition(AsmArmParser.LabelDefinitionContext ctx) {
// if we created a register which will be mapped to the return Register, we have to add to "pendingRegisters",
// as we are going to need it while visiting the metadata to create the output assignment
@Override
public Object visitRegister(AsmArmParser.RegisterContext ctx) {
public Object visitRegister(RegisterContext ctx) {
String registerNumber = ctx.Numbers().getText();
int registerID = Integer.parseInt(registerNumber);
if (asmRegisters.containsKey(registerID)) {
Expand All @@ -345,15 +344,15 @@ public Object visitRegister(AsmArmParser.RegisterContext ctx) {
// We just have to read the constraints, and based on their type, understand if they are going to be mapped
// to the args registers or to the return register.
@Override
public Object visitAsmMetadataEntries(AsmArmParser.AsmMetadataEntriesContext ctx) {
List<AsmArmParser.ConstraintContext> constraints = ctx.constraint();
public Object visitAsmMetadataEntries(AsmMetadataEntriesContext ctx) {
List<ConstraintContext> constraints = ctx.constraint();
boolean isOutputRegistersInitialized = returnRegister == null;
// We iterate until we find the first non-output constraint. Then we immediately initialize the return register
// (the right-hand side of the assignment will be either a single register or an aggregate type depending on how many output constraints we processed).
// We then map args registers to asm registers (we need to shift the register ID to find the corresponding args position of the matching register).
// Numeric constraint just map the registerID with the corresponding numeric position. (https://llvm.org/docs/LangRef.html#input-constraints)
for (int i = 0; i < constraints.size(); i++) {
AsmArmParser.ConstraintContext constraint = constraints.get(i);
ConstraintContext constraint = constraints.get(i);
if (isConstraintMemoryLocation(constraint)) {
isOutputRegistersInitialized = true;
continue;
Expand Down Expand Up @@ -388,42 +387,19 @@ public Object visitAsmMetadataEntries(AsmArmParser.AsmMetadataEntriesContext ctx
}

@Override
public Object visitValue(AsmArmParser.ValueContext ctx) {
public Object visitValue(ValueContext ctx) {
checkState(expectedType instanceof IntegerType, "Expected type is not an integer type");
String valueString = ctx.Numbers().getText();
BigInteger value = new BigInteger(valueString);
return expressions.makeValue(value, (IntegerType) expectedType);
}

@Override
public Object visitArmFence(AsmArmParser.ArmFenceContext ctx) {
public Object visitArmFence(ArmFenceContext ctx) {
// check which type of fence it is : DataMemoryBarrier or DataSynchronizationBarrier
String type = ctx.DataMemoryBarrier() == null ? ctx.DataSynchronizationBarrier().getText() : ctx.DataMemoryBarrier().getText();
String option = ctx.FenceArmOpt().getText();
String barrier = type + " " + option;
Event fence = switch (barrier) {
case "dmb ish" ->
EventFactory.AArch64.DMB.newISHBarrier();
case "dmb ishld" ->
EventFactory.AArch64.DMB.newISHLDBarrier();
case "dmb sy" ->
EventFactory.AArch64.DMB.newSYBarrier();
case "dmb st" ->
EventFactory.AArch64.DMB.newSTBarrier();
case "dmb ishst" ->
EventFactory.AArch64.DMB.newISHSTBarrier();
case "dsb ish" ->
EventFactory.AArch64.DSB.newISHBarrier();
case "dsb ishld" ->
EventFactory.AArch64.DSB.newISHLDBarrier();
case "dsb sy" ->
EventFactory.AArch64.DSB.newSYBarrier();
case "dsb ishst" ->
EventFactory.AArch64.DSB.newISHSTBarrier();
default ->
throw new ParsingException("Barrier not implemented");
};
asmInstructions.add(fence);
final String type = (ctx.DataMemoryBarrier() == null ? ctx.DataSynchronizationBarrier() : ctx.DataMemoryBarrier()).getText();
final String option = ctx.FenceArmOpt().getText();
asmInstructions.add(EventFactory.AArch64.newBarrier(type.toUpperCase(), option.toUpperCase()));
return null;
}
}
Loading
Loading