Skip to content

Commit

Permalink
pthread library intrinsics (#582)
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren authored Dec 23, 2023
1 parent e5c25c1 commit 024bd43
Show file tree
Hide file tree
Showing 14 changed files with 3,462 additions and 74 deletions.
421 changes: 421 additions & 0 deletions benchmarks/c/miscellaneous/pthread.c
View file

Large diffs are not rendered by default.

4 changes: 4 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,10 @@ public IValue parseValue(String text, IntegerType type) {
return makeValue(new BigInteger(text), type);
}

public IValue makeValue(long value, IntegerType type) {
return makeValue(BigInteger.valueOf(value), type);
}

public IValue makeValue(BigInteger value, IntegerType type) {
return new IValue(value, type);
}
Expand Down
73 changes: 52 additions & 21 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ public Expression visitCompilationUnit(CompilationUnitContext ctx) {
// Parse global definitions after declarations.
for (final TopLevelEntityContext entity : ctx.topLevelEntity()) {
if (entity.globalDef() != null) {
entity.accept(this);
visitGlobalDef(entity.globalDef());
}
}

Expand Down Expand Up @@ -364,16 +364,7 @@ public Expression visitSwitchTerm(SwitchTermContext ctx) {

@Override
public Expression visitCallInst(CallInstContext ctx) {
if (ctx.inlineAsm() != null) {
// FIXME: We ignore all inline assembly.
return null;
}
final Expression callTarget = checkPointerExpression(ctx.value());
if (callTarget == null) {
//FIXME ignores metadata functions, but also undeclared functions
return null;
}
//checkSupport(callTarget instanceof Function, "Indirect call in %s.", ctx);
// see https://llvm.org/docs/LangRef.html#call-instruction
final Type type = parseType(ctx.type());
// Calls can either list the full function type or just the return type.
final Type returnType = type instanceof FunctionType funcType ? funcType.getReturnType() : type;
Expand All @@ -389,16 +380,29 @@ public Expression visitCallInst(CallInstContext ctx) {
arguments.add(checkExpression(argumentType, argument.value()));
}

final FunctionType funcType;
if (type instanceof FunctionType) {
funcType = (FunctionType) type;
} else {
// Build FunctionType from return type and argument types
funcType = types.getFunctionType(returnType, Lists.transform(arguments, Expression::getType));
}

final Register resultRegister = currentRegisterName == null ? null :
getOrNewRegister(currentRegisterName, returnType);

if (ctx.inlineAsm() != null) {
// see https://llvm.org/docs/LangRef.html#inline-assembler-expressions
//TODO add support form inline assembly
//FIXME ignore side effects of inline assembly
if (resultRegister != null) {
block.events.add(newLocal(resultRegister, makeNonDetOfType(returnType)));
}
return resultRegister;
}

final Expression callTarget = checkPointerExpression(ctx.value());
if (callTarget == null) {
//FIXME ignores metadata functions, but also undeclared functions
return null;
}

// Build FunctionType from return type and argument types
final FunctionType funcType = type instanceof FunctionType t ? t :
types.getFunctionType(returnType, Lists.transform(arguments, Expression::getType));

final Event call = currentRegisterName == null ?
newVoidFunctionCall(funcType, callTarget, arguments) :
newValueFunctionCall(resultRegister, funcType, callTarget, arguments);
Expand Down Expand Up @@ -1361,15 +1365,42 @@ private static String parseMemoryOrder(AtomicOrderingContext ctx) {
}

private static String globalIdent(TerminalNode node) {
//see https://llvm.org/docs/LangRef.html#identifiers
// Names can be quoted, to allow escaping and other characters than .
// This should not bother us after parsing: @fun and @"fun" should be identical.
final String ident = node.getText();
assert ident.startsWith("@");
return ident.substring(1).replace(".loop", ".\\loop");
final String unescapedIdent = unescape(ident.substring(1));
// LLVM prepends \01 to a global, if subsequent name mangling should be disabled.
// Clang produces this flag, when a C declaration contains an explicit __asm alias.
// We ignore this flag.
final String trimmedIdent = unescapedIdent.startsWith("\1") ? unescapedIdent.substring(1) : unescapedIdent;
return trimmedIdent.replace(".loop", ".\\loop");
}

private static String localIdent(TerminalNode node) {
final String ident = node.getText();
assert ident.startsWith("%");
return ident.substring(1).replace(".loop", ".\\loop");
return unescape(ident.substring(1)).replace(".loop", ".\\loop");
}

private static String unescape(String original) {
final boolean quoted = original.startsWith("\"");
assert quoted == (original.endsWith("\""));
final String unquoted = quoted ? original.substring(1, original.length() - 1) : original;
int escape = unquoted.indexOf('\\');
if (escape == -1) {
return unquoted;
}
final StringBuilder sb = new StringBuilder(unquoted.length());
int progress = 0;
do {
sb.append(unquoted, progress, escape);
progress = escape + 3;
sb.append((char) Integer.parseInt(unquoted.substring(escape + 1, progress), 16));
escape = unquoted.indexOf('\\', progress);
} while (escape != -1);
return sb.append(unquoted, progress, unquoted.length()).toString();
}

private Register getOrNewRegister(String name, Type type) {
Expand Down
9 changes: 5 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.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.FunctionType;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.Type;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.Function;
import com.dat3m.dartagnan.program.Register;
import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
Expand Down Expand Up @@ -42,7 +43,6 @@
import com.dat3m.dartagnan.program.event.lang.svcomp.*;
import com.dat3m.dartagnan.program.memory.MemoryObject;

import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;

Expand Down Expand Up @@ -134,7 +134,7 @@ public static Init newInit(MemoryObject base, int offset) {
//TODO: We simplify here because virtual aliasing currently fails when pointer arithmetic is involved
// meaning that <addr> and <addr + 0> are treated differently.
final Expression address = offset == 0 ? base :
expressions.makeADD(base, expressions.makeValue(BigInteger.valueOf(offset), base.getType()));
expressions.makeADD(base, expressions.makeValue(offset, base.getType()));
return new Init(base, offset, address);
}

Expand Down Expand Up @@ -317,8 +317,9 @@ public static class Pthread {
private Pthread() {
}

public static InitLock newInitLock(String name, Expression address, Expression value) {
return new InitLock(name, address, value);
public static InitLock newInitLock(String name, Expression address, Expression ignoreAttributes) {
//TODO store attributes inside mutex object
return new InitLock(name, address, expressions.makeZero(TypeFactory.getInstance().getArchType()));
}

public static Lock newLock(String name, Expression address) {
Expand Down
4 changes: 3 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,9 @@ public Expression getAllocationSize() {
);
} else {
allocationSize = expressions.makeMUL(
expressions.makeValue(BigInteger.valueOf(types.getMemorySizeInBytes(allocationType)), types.getArchType()),
expressions.makeValue(
BigInteger.valueOf(types.getMemorySizeInBytes(allocationType)),
(IntegerType) arraySize.getType()),
arraySize
);
}
Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ public class MemoryObject extends IConst {

// Should only be called for statically allocated objects.
public Set<Integer> getStaticallyInitializedFields() {
checkState(this.isStaticallyAllocated());
checkState(this.isStaticallyAllocated(), "Unexpected dynamic object %s", this);
return initialValues.keySet();
}

Expand Down
7 changes: 3 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@
import com.dat3m.dartagnan.program.event.core.utils.RegReader;
import com.dat3m.dartagnan.program.memory.MemoryObject;

import java.math.BigInteger;
import java.util.List;

public class GEPToAddition implements ProgramProcessor {
Expand Down Expand Up @@ -53,15 +52,15 @@ public Expression visit(GEPExpression getElementPointer) {
assert offsets.size() > 0;
result = expressions.makeADD(result,
expressions.makeMUL(
expressions.makeValue(BigInteger.valueOf(types.getMemorySizeInBytes(type)), archType),
expressions.makeValue(types.getMemorySizeInBytes(type), archType),
expressions.makeIntegerCast(offsets.get(0).accept(this), archType, true)));
for (final Expression oldOffset : offsets.subList(1, offsets.size())) {
final Expression offset = oldOffset.accept(this);
if (type instanceof ArrayType arrayType) {
type = arrayType.getElementType();
result = expressions.makeADD(result,
expressions.makeMUL(
expressions.makeValue(BigInteger.valueOf(types.getMemorySizeInBytes(arrayType.getElementType())), archType),
expressions.makeValue(types.getMemorySizeInBytes(arrayType.getElementType()), archType),
expressions.makeIntegerCast(offset, archType, true)));
continue;
}
Expand All @@ -78,7 +77,7 @@ public Expression visit(GEPExpression getElementPointer) {
for (final Type elementType : aggregateType.getDirectFields().subList(0, value)) {
o += types.getMemorySizeInBytes(elementType);
}
result = expressions.makeADD(result, expressions.makeValue(BigInteger.valueOf(o), archType));
result = expressions.makeADD(result, expressions.makeValue(o, archType));
}
return result;
}
Expand Down
13 changes: 9 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
import static com.dat3m.dartagnan.configuration.OptionNames.RECURSION_BOUND;
import static com.dat3m.dartagnan.program.event.EventFactory.*;
import static com.google.common.base.Preconditions.checkNotNull;
import static com.google.common.base.Verify.verify;

@Options
public class Inlining implements ProgramProcessor {
Expand All @@ -56,7 +57,8 @@ public void run(Program program) {
function.getName(),
function.getParameterRegisters(),
function.getEvents(),
List.copyOf(function.getRegisters())));
List.copyOf(function.getRegisters()),
function.getFunctionType().isVarArgs()));
}
for (final Function function : program.getFunctions()) {
inlineAllCalls(function, snapshots);
Expand All @@ -66,7 +68,8 @@ public void run(Program program) {
}
}

private record Snapshot(String name, List<Register> parameters, List<Event> events, List<Register> registers) {}
private record Snapshot(String name, List<Register> parameters, List<Event> events, List<Register> registers,
boolean isVarArgs) {}

private boolean canInline(FunctionCall call) {
return call.isDirectCall() && call.getCalledFunction().hasBody();
Expand Down Expand Up @@ -126,15 +129,17 @@ private static Event inlineBody(FunctionCall call, Snapshot callTarget, int scop
var replacementMap = new HashMap<Event, Event>();
var registerMap = new HashMap<Register, Register>();
final List<Expression> arguments = call.getArguments();
assert arguments.size() == callTarget.parameters.size();
//TODO add support for __VA_INIT
verify(callTarget.isVarArgs ? arguments.size() >= callTarget.parameters.size() :
arguments.size() == callTarget.parameters.size(), "Parameter mismatch at %s", call);
// All registers have to be replaced
for (final Register register : callTarget.registers) {
final String newName = scope + ":" + register.getName();
registerMap.put(register, call.getFunction().newRegister(newName, register.getType()));
}
var parameterAssignments = new ArrayList<Event>();
var returnEvents = new HashSet<Event>();
for (int j = 0; j < arguments.size(); j++) {
for (int j = 0; j < callTarget.parameters.size(); j++) {
Register register = registerMap.get(callTarget.parameters.get(j));
parameterAssignments.add(newLocal(register, arguments.get(j)));
}
Expand Down
Loading

0 comments on commit 024bd43

Please sign in to comment.