From b0bab8b12a4a0c311d9c6bfbe1d1ca07c82900a1 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 13 Nov 2023 17:39:42 +0100 Subject: [PATCH] Replace GEP in initial values of MemoryObjects Support subtraction in AliasAnalysis --- .../program/analysis/alias/FieldSensitiveAndersen.java | 4 ++-- .../dat3m/dartagnan/program/processing/GEPToAddition.java | 7 +++++++ 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java index accc274154..acc0f3c6a8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java @@ -320,12 +320,12 @@ public Result visit(IExprBin x) { } return new Result(null, null, l.offset.multiply(r.offset), min(min(l.alignment,l.register)*r.offset.intValue(), min(r.alignment,r.register)*l.offset.intValue())); } - if(x.getOp() == ADD) { + if(x.getOp() == ADD || x.getOp() == SUB) { if(l.address!=null && r.address!=null) { return null; } MemoryObject base = l.address!=null ? l.address : r.address; - BigInteger offset = l.offset.add(r.offset); + BigInteger offset = x.getOp() == ADD ? l.offset.add(r.offset) : l.offset.subtract(r.offset); if(base!=null) { return new Result(base,null,offset,min(min(l.alignment,l.register), min(r.alignment,r.register))); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java index ad0cdff9a1..67393cbea0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java @@ -10,6 +10,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.memory.MemoryObject; import java.math.BigInteger; import java.util.List; @@ -30,6 +31,12 @@ public void run(Program program) { reader.transformExpressions(transformer); } } + + for (MemoryObject memoryObject : program.getMemory().getObjects()) { + for (int field : memoryObject.getStaticallyInitializedFields()) { + memoryObject.setInitialValue(field, memoryObject.getInitialValue(field).accept(transformer)); + } + } } private static final class GEPToAdditionTransformer extends ExprTransformer {