pthread library intrinsics

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java

@@ -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);
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java

@@ -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());
             }
         }
 
@@ -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;
@@ -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);
@@ -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) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -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;
@@ -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;
 
@@ -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);
     }
 
@@ -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) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java

@@ -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
             );
         }

dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java

@@ -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();
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java

@@ -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 {
@@ -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;
                 }
@@ -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;
         }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java

@@ -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 {
@@ -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);
@@ -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();
@@ -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)));
         }