From 99182f511c38c7d7ff8ac6c4913753b5466556f2 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 21 Sep 2024 13:39:15 +0200 Subject: [PATCH] Feedback implemented Signed-off-by: Hernan Ponce de Leon --- .../parsers/program/utils/ProgramBuilder.java | 37 ++++++------------- .../visitors/VisitorLitmusAArch64.java | 4 +- .../program/visitors/VisitorLitmusRISCV.java | 4 +- 3 files changed, 15 insertions(+), 30 deletions(-) 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 0fde831ef1..ad2386caa1 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 @@ -48,8 +48,6 @@ public class ProgramBuilder { private final Map> fid2LabelsMap = new HashMap<>(); private final Map locations = new HashMap<>(); - private String zeroRegister = null; - private final Program program; // ---------------------------------------------------------------------------------------------------------------- @@ -68,12 +66,6 @@ public static ProgramBuilder forLanguage(SourceLanguage format) { return new ProgramBuilder(format); } - public static ProgramBuilder withZeroRegister(SourceLanguage format, Arch arch, String zeroRegister) { - final ProgramBuilder programBuilder = forArch(format, arch); - programBuilder.setZeroRegisterName(zeroRegister); - return programBuilder; - } - public Program build() { for (Thread thread : program.getThreads()) { final Label endOfThread = getEndOfThreadLabel(thread.getId()); @@ -86,7 +78,6 @@ public Program build() { thread.append(endOfThread); } processAfterParsing(program); - replaceZeroRegister(); return program; } @@ -98,19 +89,17 @@ public Program build() { 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. */ - private void replaceZeroRegister() { - if(zeroRegister != null) { - final ExpressionVisitor zeroRegReplacer = new ExprTransformer() { - @Override - public Expression visitRegister(Register reg) { - return reg.getName().equals(zeroRegister) ? expressions.makeGeneralZero(reg.getType()) : reg; - } - }; - program.getThreadEvents(RegReader.class) - .forEach(e -> e.transformExpressions(zeroRegReplacer)); - program.setSpecification(program.getSpecificationType(), - program.getSpecification().accept(zeroRegReplacer)); - } + public void replaceZeroRegister(String registerName) { + final ExpressionVisitor 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) { @@ -139,10 +128,6 @@ public void setAssert(Program.SpecificationType type, Expression ass) { program.setSpecification(type, ass); } - public void setZeroRegisterName(String zeroRegister) { - this.zeroRegister = zeroRegister; - } - public void setAssertFilter(Expression ass) { program.setFilterSpecification(ass); } 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 7ef5b5e654..915f546c2b 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 @@ -33,8 +33,7 @@ public CmpInstruction(Expression left, Expression right) { } } - private final ProgramBuilder programBuilder = ProgramBuilder.withZeroRegister(Program.SourceLanguage.LITMUS, - Arch.ARM8, "xzr"); + private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.ARM8); private final TypeFactory types = programBuilder.getTypeFactory(); private final IntegerType archType = types.getArchType(); private final ExpressionFactory expressions = programBuilder.getExpressionFactory(); @@ -55,6 +54,7 @@ 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(); } 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 9c1c88775c..a847260c51 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 @@ -19,8 +19,7 @@ public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor { - private final ProgramBuilder programBuilder = ProgramBuilder.withZeroRegister(Program.SourceLanguage.LITMUS, - Arch.RISCV, "x0"); + private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.RISCV); private final TypeFactory types = programBuilder.getTypeFactory(); private final ExpressionFactory expressions = programBuilder.getExpressionFactory(); private final IntegerType archType = types.getArchType(); @@ -39,6 +38,7 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) { visitVariableDeclaratorList(ctx.variableDeclaratorList()); visitInstructionList(ctx.program().instructionList()); VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter()); + programBuilder.replaceZeroRegister("x0"); return programBuilder.build(); }