Skip to content
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

Jump to bottom

Some improvements to aarch64 pseudo-assembly #741

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

Some improvements to aarch64 pseudo-assembly #741

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
ced0faa
Some improvements to aarch64 pseudo-assembly
hernan-poncedeleon Sep 20, 2024
1315cc3
Move zero register replacement to ProgramBuilder
hernan-poncedeleon Sep 21, 2024
d37bbad
Replace zero registers in specifications
hernan-poncedeleon Sep 21, 2024
99182f5
Feedback implemented
hernan-poncedeleon Sep 21, 2024
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
32 changes: 30 additions & 2 deletions dartagnan/src/main/antlr4/LitmusAArch64.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,8 @@ instruction
| branchRegister
| branchLabel
| fence
| return
| nop
;

mov locals [String rD, int size]
Expand Down Expand Up @@ -131,6 +133,14 @@ branchLabel
: label Colon
;

return
: Ret
;

nop
: Nop
;

loadInstruction locals [String mo]
: LDR {$mo = MO_RX;}
| LDAR {$mo = MO_ACQ;}
Expand Down Expand Up @@ -244,15 +254,15 @@ register64 returns[String id]
;

register32 returns[String id]
: r = Register32 {$id = $r.text.replace("W","X");}
: r = Register32 {$id = $r.text.replace("W","X").replace("w","x");}
;

location
: Identifier
;

immediate
: Num constant
: Num Hexa? constant
;

label
Expand All @@ -265,6 +275,18 @@ assertionValue
| constant
;

Hexa
: '0x'
;

Ret
: 'ret'
;

Nop
: 'nop'
;

Locations
: 'locations'
;
Expand Down Expand Up @@ -371,10 +393,16 @@ BitfieldOperator

Register64
: 'X' DigitSequence
| 'x' DigitSequence
| 'XZR' // zero register
| 'xzr' // zero register
;

Register32
: 'W' DigitSequence
| 'w' DigitSequence
| 'WZR' // zero register
| 'wzr' // zero register
;

LitmusLanguage
Expand Down
24 changes: 24 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,18 @@
import com.dat3m.dartagnan.exception.MalformedProgramException;
import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
import com.dat3m.dartagnan.expression.ExpressionVisitor;
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.integers.IntLiteral;
import com.dat3m.dartagnan.expression.processing.ExprTransformer;
import com.dat3m.dartagnan.expression.type.FunctionType;
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.RegReader;
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;
Expand Down Expand Up @@ -78,6 +81,27 @@ public Program build() {
return program;
}

/*
The zero register plays a special role in some architectures:
1. Reading accesses always return the value 0.
2. Discards data when written.
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 the zero register,
its value is never read after the transformation so its value is effectively 0.
*/
public void replaceZeroRegister(String registerName) {
final ExpressionVisitor<Expression> zeroRegReplacer = new ExprTransformer() {
@Override
public Expression visitRegister(Register reg) {
return reg.getName().equals(registerName) ? expressions.makeGeneralZero(reg.getType()) : reg;
}
};
program.getThreadEvents(RegReader.class)
.forEach(e -> e.transformExpressions(zeroRegReplacer));
program.setSpecification(program.getSpecificationType(),
program.getSpecification().accept(zeroRegReplacer));
}

public static void processAfterParsing(Program program) {
program.getFunctions().forEach(Function::validate);
program.getThreads().forEach(Function::validate);
Expand Down
17 changes: 16 additions & 1 deletion ...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
import com.dat3m.dartagnan.program.event.core.Label;
import com.dat3m.dartagnan.program.event.core.Load;

import java.math.BigInteger;
import java.util.HashMap;
import java.util.Map;

Expand Down Expand Up @@ -53,10 +54,10 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) {
visitVariableDeclaratorList(ctx.variableDeclaratorList());
visitInstructionList(ctx.program().instructionList());
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
programBuilder.replaceZeroRegister("xzr");
return programBuilder.build();
}


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

Expand Down Expand Up @@ -211,6 +212,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);
Expand Down Expand Up @@ -255,4 +262,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);
}

}
30 changes: 2 additions & 28 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,7 @@
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;
Expand All @@ -16,7 +14,6 @@
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;

Expand All @@ -41,33 +38,10 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) {
visitVariableDeclaratorList(ctx.variableDeclaratorList());
visitInstructionList(ctx.program().instructionList());
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
Program prog = programBuilder.build();
replaceX0Register(prog);

return prog;
programBuilder.replaceZeroRegister("x0");
return programBuilder.build();
}

/*
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

Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
ComplexBlockSplitting.newInstance(),
BranchReordering.fromConfig(config),
Simplifier.fromConfig(config)
), Target.FUNCTIONS, true
), Target.ALL, true
ThomasHaas marked this conversation as resolved.
Show resolved Hide resolved
),
ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true),
RegisterDecomposition.newInstance(),
Expand Down
Loading