Feedback implemented

Signed-off-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Sep 21, 2024 · 99182f5 · 99182f5
1 parent d37bbad
commit 99182f5
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 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
@@ -48,8 +48,6 @@ public class ProgramBuilder {
     private final Map<Integer, Map<String, Label>> fid2LabelsMap = new HashMap<>();
     private final Map<String, MemoryObject> 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<Expression> 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<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) {
@@ -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/...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/...gnan/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
@@ -19,8 +19,7 @@
 
 public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor<Object> {
 
-    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();
     }