Skip to content

Commit

Permalink
Refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
@ThomasHaas
ThomasHaas committed Jun 30, 2023
1 parent bab6927 commit 7975c5b
Show file tree
Hide file tree
Showing 12 changed files with 136 additions and 129 deletions.
144 changes: 76 additions & 68 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@
import java.util.*;

import static com.dat3m.dartagnan.program.Program.SourceLanguage.LITMUS;
import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkState;

public class ProgramBuilder {

Expand All @@ -47,6 +47,8 @@ public class ProgramBuilder {

private final Program program;

// ----------------------------------------------------------------------------------------------------------------
// Construction
private ProgramBuilder(SourceLanguage format) {
this.program = new Program(new Memory(), format);
}
Expand All @@ -61,14 +63,6 @@ public static ProgramBuilder forLanguage(SourceLanguage format) {
return new ProgramBuilder(format);
}

public TypeFactory getTypeFactory() {
return types;
}

public ExpressionFactory getExpressionFactory() {
return expressions;
}

public Program build() {
for (Thread thread : program.getThreads()) {
final Label endOfThread = getEndOfThreadLabel(thread.getId());
Expand All @@ -82,16 +76,39 @@ public Program build() {
return program;
}

public void initThread(String name, int tid) {
// ----------------------------------------------------------------------------------------------------------------
// Misc

public TypeFactory getTypeFactory() {
return types;
}

public ExpressionFactory getExpressionFactory() {
return expressions;
}

public void setAssert(AbstractAssert ass) {
program.setSpecification(ass);
}

public void setAssertFilter(AbstractAssert ass) {
program.setFilterSpecification(ass);
}

// ----------------------------------------------------------------------------------------------------------------
// Threads and Functions

public Thread newThread(String name, int tid) {
if(id2FunctionsMap.containsKey(tid)) {
throw new MalformedProgramException("Function or thread with id " + tid + " already exists.");
}
final Thread thread = new Thread(name, DEFAULT_THREAD_TYPE, List.of(), tid, EventFactory.newSkip());
id2FunctionsMap.put(tid, thread);
program.addThread(thread);
return thread;
}

public Function initFunction(String name, int fid, FunctionType type, List<String> parameterNames) {
public Function newFunction(String name, int fid, FunctionType type, List<String> parameterNames) {
if(id2FunctionsMap.containsKey(fid)) {
throw new MalformedProgramException("Function or thread with id " + fid + " already exists.");
}
Expand All @@ -101,22 +118,28 @@ public Function initFunction(String name, int fid, FunctionType type, List<Strin
return func;
}

public void initThread(int tid) {
initThread(String.valueOf(tid), tid);
public Thread newThread(int tid) {
return newThread(String.valueOf(tid), tid);
}

public Thread getOrNewThread(int tid) {
if (!id2FunctionsMap.containsKey(tid)) {
initThread(tid);
return (Thread)id2FunctionsMap.computeIfAbsent(tid, this::newThread);
}

public boolean functionExists(int fid) {
return id2FunctionsMap.containsKey(fid);
}

public Function getFunctionOrError(int fid) {
final Function function = id2FunctionsMap.get(fid);
if (function != null) {
return function;
}
return (Thread)id2FunctionsMap.get(tid);
throw new MalformedProgramException("Function or Thread with id " + fid + " does not exist");
}

public Event addChild(int fid, Event child) {
final Function func = id2FunctionsMap.get(fid);
if(func == null){
throw new MalformedProgramException("Function " + fid + " is not initialised");
}
final Function func = getFunctionOrError(fid);
func.append(child);
// Every event in litmus tests is non-optimisable
if(program.getFormat().equals(LITMUS)) {
Expand All @@ -125,85 +148,70 @@ public Event addChild(int fid, Event child) {
return child;
}

public void setAssert(AbstractAssert ass) {
program.setSpecification(ass);
// ----------------------------------------------------------------------------------------------------------------
// Memory & Constants

public MemoryObject getMemoryObject(String name) {
return locations.get(name);
}

public void setAssertFilter(AbstractAssert ass) {
program.setFilterSpecification(ass);
public MemoryObject getOrNewMemoryObject(String name) {
final MemoryObject mem = locations.computeIfAbsent(name, k -> program.getMemory().allocate(1, true));
mem.setCVar(name);
return mem;
}

public MemoryObject newMemoryObject(String name, int size) {
checkState(!locations.containsKey(name),
"Illegal allocation. Memory object %s is already defined", name);
final MemoryObject mem = program.getMemory().allocate(size, true);
mem.setCVar(name);
locations.put(name, mem);
return mem;
}

public INonDet newConstant(IntegerType type, boolean signed) {
var constant = new INonDet(program.getConstants().size(), type, signed);
program.addConstant(constant);
return constant;
}

// ----------------------------------------------------------------------------------------------------------------
// Declarators
public void initLocEqLocPtr(String leftName, String rightName){
initLocEqConst(leftName, getOrNewObject(rightName));
public void initLocEqLocPtr(String leftName, String rightName) {
initLocEqConst(leftName, getOrNewMemoryObject(rightName));
}

public void initLocEqLocVal(String leftName, String rightName){
initLocEqConst(leftName,getInitialValue(rightName));
}

public void initLocEqConst(String locName, IConst iValue){
getOrNewObject(locName).setInitialValue(0,iValue);
getOrNewMemoryObject(locName).setInitialValue(0,iValue);
}

public void initRegEqLocPtr(int regThread, String regName, String locName, Type type) {
MemoryObject object = getOrNewObject(locName);
MemoryObject object = getOrNewMemoryObject(locName);
Register reg = getOrNewRegister(regThread, regName, type);
addChild(regThread, EventFactory.newLocal(reg, object));
}

public void initRegEqLocVal(int regThread, String regName, String locName, Type type) {
Register reg = getOrNewRegister(regThread, regName, type);
addChild(regThread,EventFactory.newLocal(reg,getInitialValue(locName)));
addChild(regThread, EventFactory.newLocal(reg,getInitialValue(locName)));
}

public void initRegEqConst(int regThread, String regName, IConst iValue){
addChild(regThread, EventFactory.newLocal(getOrNewRegister(regThread, regName, iValue.getType()), iValue));
}

private IConst getInitialValue(String name) {
return getOrNewObject(name).getInitialValue(0);
return getOrNewMemoryObject(name).getInitialValue(0);
}

// ----------------------------------------------------------------------------------------------------------------
// Utility

public boolean functionExists(int fid) {
return id2FunctionsMap.containsKey(fid);
}

public Function getFunctionOrError(int fid) {
final Function function = id2FunctionsMap.get(fid);
if (function != null) {
return function;
}
throw new MalformedProgramException("Function or Thread with id " + fid + " does not exist");
}

public INonDet newConstant(IntegerType type, boolean signed) {
var constant = new INonDet(program.getConstants().size(), type, signed);
program.addConstant(constant);
return constant;
}

public MemoryObject getObject(String name) {
return locations.get(name);
}

public MemoryObject getOrNewObject(String name) {
MemoryObject object = locations.computeIfAbsent(name, k -> program.getMemory().allocate(1, true));
object.setCVar(name);
return object;
}

public MemoryObject newObject(String name, int size) {
checkArgument(!locations.containsKey(name), "Illegal malloc. Array " + name + " is already defined");
MemoryObject result = program.getMemory().allocate(size, true);
locations.put(name, result);
return result;
}

public Register getRegister(int fid, String name){
return getFunctionOrError(fid).getRegister(name);
}
Expand Down Expand Up @@ -289,7 +297,7 @@ public void initVirLocEqCon(String leftName, IConst iValue){
}

public void initVirLocEqLoc(String leftName, String rightName){
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getObject(rightName);
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getMemoryObject(rightName);
if (rightLocation == null) {
throw new MalformedProgramException("Alias to non-exist location: " + rightName);
}
Expand All @@ -300,7 +308,7 @@ public void initVirLocEqLoc(String leftName, String rightName){
}

public void initVirLocEqLocAliasGen(String leftName, String rightName){
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getObject(rightName);
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getMemoryObject(rightName);
if (rightLocation == null) {
throw new MalformedProgramException("Alias to non-exist location: " + rightName);
}
Expand All @@ -311,7 +319,7 @@ public void initVirLocEqLocAliasGen(String leftName, String rightName){
}

public void initVirLocEqLocAliasProxy(String leftName, String rightName){
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getObject(rightName);
VirtualMemoryObject rightLocation = (VirtualMemoryObject) getMemoryObject(rightName);
if (rightLocation == null) {
throw new MalformedProgramException("Alias to non-exist location: " + rightName);
}
Expand Down
2 changes: 1 addition & 1 deletion ...gnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ public Object visitVariableDeclaratorLocationLocation(LitmusAArch64Parser.Variab
@Override
public Object visitThreadDeclaratorList(LitmusAArch64Parser.ThreadDeclaratorListContext ctx) {
for(LitmusAArch64Parser.ThreadIdContext threadCtx : ctx.threadId()){
programBuilder.initThread(threadCtx.id);
programBuilder.newThread(threadCtx.id);
threadCount++;
}
return null;
Expand Down
2 changes: 1 addition & 1 deletion ...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueCon
if(ctx.threadId() != null) {
return programBuilder.getOrErrorRegister(ctx.threadId().id,name);
}
MemoryObject base = programBuilder.getObject(name);
MemoryObject base = programBuilder.getMemoryObject(name);
checkState(base != null, "uninitialized location %s", name);
TerminalNode offset = ctx.DigitSequence();
int o = offset == null ? 0 : Integer.parseInt(offset.getText());
Expand Down
18 changes: 9 additions & 9 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ public Object visitGlobalDeclaratorLocationLocation(LitmusCParser.GlobalDeclarat
programBuilder.initLocEqLocPtr(ctx.varName(0).getText(), ctx.varName(1).getText());
} else {
String rightName = ctx.varName(1).getText();
MemoryObject object = programBuilder.getObject(rightName);
MemoryObject object = programBuilder.getMemoryObject(rightName);
if(object != null){
programBuilder.initLocEqConst(ctx.varName(0).getText(), object);
} else {
Expand All @@ -113,7 +113,7 @@ public Object visitGlobalDeclaratorRegisterLocation(LitmusCParser.GlobalDeclarat
programBuilder.initRegEqLocPtr(ctx.threadId().id, ctx.varName(0).getText(), ctx.varName(1).getText(), archType);
} else {
String rightName = ctx.varName(1).getText();
MemoryObject object = programBuilder.getObject(rightName);
MemoryObject object = programBuilder.getMemoryObject(rightName);
if(object != null){
programBuilder.initRegEqConst(ctx.threadId().id, ctx.varName(0).getText(), object);
} else {
Expand All @@ -129,7 +129,7 @@ public Object visitGlobalDeclaratorArray(LitmusCParser.GlobalDeclaratorArrayCont
Integer size = ctx.DigitSequence() != null ? Integer.parseInt(ctx.DigitSequence().getText()) : null;

if(ctx.initArray() == null && size != null && size > 0){
programBuilder.newObject(name,size);
programBuilder.newMemoryObject(name,size);
return null;
}
if(ctx.initArray() != null){
Expand All @@ -141,16 +141,16 @@ public Object visitGlobalDeclaratorArray(LitmusCParser.GlobalDeclaratorArrayCont
} else {
String varName = elCtx.varName().getText();
//see test/resources/arrays/ok/C-array-ok-17.litmus
MemoryObject object = programBuilder.getObject(varName);
MemoryObject object = programBuilder.getMemoryObject(varName);
if(object != null){
values.add(object);
} else {
object = programBuilder.getOrNewObject(varName);
object = programBuilder.getOrNewMemoryObject(varName);
values.add(elCtx.Ast() == null ? object : object.getInitialValue(0));
}
}
}
MemoryObject object = programBuilder.newObject(name,values.size());
MemoryObject object = programBuilder.newMemoryObject(name,values.size());
for(int i = 0; i < values.size(); i++) {
object.setInitialValue(i,values.get(i));
}
Expand Down Expand Up @@ -184,7 +184,7 @@ public Object visitThreadArguments(LitmusCParser.ThreadArgumentsContext ctx){
int id = 0;
for(LitmusCParser.VarNameContext varName : ctx.varName()){
String name = varName.getText();
MemoryObject object = programBuilder.getOrNewObject(name);
MemoryObject object = programBuilder.getOrNewMemoryObject(name);
PointerTypeSpecifierContext pType = ctx.pointerTypeSpecifier(id);
if(pType != null) {
BasicTypeSpecifierContext bType = pType.basicTypeSpecifier();
Expand Down Expand Up @@ -526,15 +526,15 @@ public Expression visitVarName(LitmusCParser.VarNameContext ctx){
if(register != null){
return register;
}
MemoryObject object = programBuilder.getObject(ctx.getText());
MemoryObject object = programBuilder.getMemoryObject(ctx.getText());
if(object != null){
register = programBuilder.getOrNewRegister(scope, null, archType);
programBuilder.addChild(currentThread, EventFactory.newLoadWithMo(register, object, C11.NONATOMIC));
return register;
}
return programBuilder.getOrNewRegister(scope, ctx.getText(), archType);
}
MemoryObject object = programBuilder.getOrNewObject(ctx.getText());
MemoryObject object = programBuilder.newMemoryObject(ctx.getText(), 1);
Register register = programBuilder.getOrNewRegister(scope, null, archType);
programBuilder.addChild(currentThread, EventFactory.newLoadWithMo(register, object, C11.NONATOMIC));
return register;
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusLISA.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ public Object visitVariableDeclaratorLocationLocation(LitmusLISAParser.VariableD
@Override
public Object visitThreadDeclaratorList(LitmusLISAParser.ThreadDeclaratorListContext ctx) {
for (LitmusLISAParser.ThreadIdContext threadCtx : ctx.threadId()) {
programBuilder.initThread(threadCtx.id);
programBuilder.newThread(threadCtx.id);
threadCount++;
}
return null;
Expand Down Expand Up @@ -170,7 +170,7 @@ public Object visitJump(LitmusLISAParser.JumpContext ctx) {

@Override
public Object visitLocation(LitmusLISAParser.LocationContext ctx) {
return programBuilder.getOrNewObject(ctx.getText());
return programBuilder.getOrNewMemoryObject(ctx.getText());
}

@Override
Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ public Object visitVariableDeclaratorLocationLocation(LitmusPPCParser.VariableDe
@Override
public Object visitThreadDeclaratorList(LitmusPPCParser.ThreadDeclaratorListContext ctx) {
for(LitmusPPCParser.ThreadIdContext threadCtx : ctx.threadId()){
programBuilder.initThread(threadCtx.id);
programBuilder.newThread(threadCtx.id);
threadCount++;
}
return null;
Expand Down
Loading

0 comments on commit 7975c5b

Please sign in to comment.