Skip to content

Commit

Permalink
initialize Reg after thread created
Browse files Browse the repository at this point in the history
  • Loading branch information
@tonghaining
tonghaining committed Sep 27, 2024
1 parent 0705298 commit 2ec066e
Show file tree
Hide file tree
Showing 2 changed files with 54 additions and 19 deletions.
53 changes: 45 additions & 8 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 @@ -7,6 +7,7 @@
import com.dat3m.dartagnan.expression.Type;
import com.dat3m.dartagnan.expression.integers.IntLiteral;
import com.dat3m.dartagnan.expression.type.FunctionType;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.*;
import com.dat3m.dartagnan.program.Thread;
Expand Down Expand Up @@ -45,6 +46,10 @@ public class ProgramBuilder {
private final Map<Integer, Map<String, Label>> fid2LabelsMap = new HashMap<>();
private final Map<String, MemoryObject> locations = new HashMap<>();
private final Map<Register, MemoryObject> reg2LocMap = new HashMap<>();
private final Map<Integer, Map<String, IntegerType>> id2RegTypeMap = new HashMap<>();
private final Map<Integer, Map<String, Expression>> id2RegConstMap = new HashMap<>();
private final Map<Integer, Map<String, String>> id2RegLocPtrMap = new HashMap<>();
private final Map<Integer, Map<String, String>> id2RegLocValMap = new HashMap<>();

private final Program program;

Expand Down Expand Up @@ -114,13 +119,19 @@ public void setAssertFilter(Expression ass) {

// This method creates a "default" thread that has no parameters, no return value, and runs unconditionally.
// It is only useful for creating threads of Litmus code.
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.newThreadStart(null));
public Thread newThread(int tid, Thread thread) {
id2FunctionsMap.put(tid, thread);
program.addThread(thread);
if (id2RegConstMap.containsKey(tid)) {
id2RegConstMap.get(tid).forEach((regName, value) ->
initRegEqConst(tid, regName, value));
} else if (id2RegLocPtrMap.containsKey(tid)) {
id2RegLocPtrMap.get(tid).forEach((regName, value) ->
initRegEqLocPtr(tid, regName, value, getRegType(tid, regName)));
} else if (id2RegLocValMap.containsKey(tid)) {
id2RegLocValMap.get(tid).forEach((regName, value) ->
initRegEqLocVal(tid, regName, value, getRegType(tid, regName)));
}
return thread;
}

Expand All @@ -135,8 +146,12 @@ public Function newFunction(String name, int fid, FunctionType type, List<String
}

public Thread newThread(int tid) {
if(id2FunctionsMap.containsKey(tid)) {
throw new MalformedProgramException("Function or thread with id " + tid + " already exists.");
}
final String threadName = (program.getFormat() == LITMUS ? "P" : "__thread_") + tid;
return newThread(threadName, tid);
final Thread thread = new Thread(threadName, DEFAULT_THREAD_TYPE, List.of(), tid, EventFactory.newThreadStart(null));
return newThread(tid, thread);
}

public Thread getOrNewThread(int tid) {
Expand Down Expand Up @@ -235,6 +250,29 @@ public void initRegEqConst(int regThread, String regName, Expression value){
addChild(regThread, EventFactory.newLocal(getOrNewRegister(regThread, regName, value.getType()), value));
}

public void addRegType(int tid, String regName, IntegerType type) {
id2RegTypeMap.computeIfAbsent(tid, k -> new HashMap<>()).put(regName, type);
}

public IntegerType getRegType(int tid, String regName) {
if (id2RegTypeMap.containsKey(tid) && id2RegTypeMap.get(tid).containsKey(regName)) {
return id2RegTypeMap.get(tid).get(regName);
}
throw new IllegalStateException("Register " + tid + ":" + regName + " is not initialised");
}

public void addRegToConstMap(int tid, String regName, Expression value) {
id2RegConstMap.computeIfAbsent(tid, k -> new HashMap<>()).put(regName, value);
}

public void addRegToLocPtrMap(int tid, String regName, String locName) {
id2RegLocPtrMap.computeIfAbsent(tid, k -> new HashMap<>()).put(regName, locName);
}

public void addRegToLocValMap(int tid, String regName, String locName) {
id2RegLocValMap.computeIfAbsent(tid, k -> new HashMap<>()).put(regName, locName);
}

private Expression getInitialValue(String name) {
return getOrNewMemoryObject(name).getInitialValue(0);
}
Expand Down Expand Up @@ -291,8 +329,7 @@ public void newScopedThread(Arch arch, String name, int id, int ...scopeIds) {
ScopeHierarchy.ScopeHierarchyForOpenCL(scopeIds[0], scopeIds[1]), new HashSet<>());
default -> throw new UnsupportedOperationException("Unsupported architecture: " + arch);
};
id2FunctionsMap.put(id, scopedThread);
program.addThread(scopedThread);
newThread(id, scopedThread);
}

public void newScopedThread(Arch arch, int id, int ...ids) {
Expand Down
20 changes: 9 additions & 11 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 @@ -13,7 +13,6 @@
import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.ScopeHierarchy;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.EventFactory;
import com.dat3m.dartagnan.program.event.Tag;
Expand Down Expand Up @@ -47,8 +46,6 @@ public VisitorLitmusC(){

@Override
public Program visitMain(LitmusCParser.MainContext ctx) {
//FIXME: We should visit thread declarations before variable declarations
// because variable declaration refer to threads.
visitVariableDeclaratorList(ctx.variableDeclaratorList());
visitProgram(ctx.program());
VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
Expand All @@ -71,10 +68,9 @@ public Object visitGlobalDeclaratorLocation(LitmusCParser.GlobalDeclaratorLocati
@Override
public Object visitGlobalDeclaratorRegister(LitmusCParser.GlobalDeclaratorRegisterContext ctx) {
if (ctx.initConstantValue() != null) {
// FIXME: We visit declarators before threads, so we need to create threads early
programBuilder.getOrNewThread(ctx.threadId().id);
IntLiteral value = expressions.parseValue(ctx.initConstantValue().constant().getText(), archType);
programBuilder.initRegEqConst(ctx.threadId().id,ctx.varName().getText(), value);
programBuilder.addRegType(ctx.threadId().id, ctx.varName().getText(), archType);
programBuilder.addRegToConstMap(ctx.threadId().id, ctx.varName().getText(), value);
}
return null;
}
Expand All @@ -97,17 +93,19 @@ public Object visitGlobalDeclaratorLocationLocation(LitmusCParser.GlobalDeclarat

@Override
public Object visitGlobalDeclaratorRegisterLocation(LitmusCParser.GlobalDeclaratorRegisterLocationContext ctx) {
// FIXME: We visit declarators before threads, so we need to create threads early
programBuilder.getOrNewThread(ctx.threadId().id);
int threadId = ctx.threadId().id;
String regName = ctx.varName(0).getText();
String locName = ctx.varName(1).getText();
programBuilder.addRegType(threadId, regName, archType);
if(ctx.Ast() == null){
programBuilder.initRegEqLocPtr(ctx.threadId().id, ctx.varName(0).getText(), ctx.varName(1).getText(), archType);
programBuilder.addRegToLocPtrMap(threadId, regName, locName);
} else {
String rightName = ctx.varName(1).getText();
MemoryObject object = programBuilder.getMemoryObject(rightName);
if(object != null){
programBuilder.initRegEqConst(ctx.threadId().id, ctx.varName(0).getText(), object);
programBuilder.addRegToConstMap(threadId, regName, object);
} else {
programBuilder.initRegEqLocVal(ctx.threadId().id, ctx.varName(0).getText(), ctx.varName(1).getText(), archType);
programBuilder.addRegToLocValMap(threadId, regName, locName);
}
}
return null;
Expand Down

0 comments on commit 2ec066e

Please sign in to comment.