Libvsync

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Reference.java

@@ -18,7 +18,6 @@
 import static com.google.common.base.Preconditions.checkState;
 
 import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.model.Valuation;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
@@ -69,10 +68,6 @@ public List<? extends Expr<?>> getOps() {
     @Override
     public Expr<A> withOps(List<? extends Expr<?>> ops) {
         checkState(ops.size() == 1);
-        checkState(
-                ops.get(0) instanceof RefExpr<?>
-                        && ((RefExpr) ops.get(0)).getDecl() instanceof VarDecl<?>,
-                "Don't transform references to constants.");
         return Reference.of((Expr<T>) ops.get(0), type);
     }
 

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java

@@ -29,10 +29,7 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.Type;
-import hu.bme.mit.theta.core.type.anytype.Dereference;
-import hu.bme.mit.theta.core.type.anytype.InvalidLitExpr;
-import hu.bme.mit.theta.core.type.anytype.IteExpr;
-import hu.bme.mit.theta.core.type.anytype.RefExpr;
+import hu.bme.mit.theta.core.type.anytype.*;
 import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
@@ -207,8 +204,7 @@ public <T extends Type> Expr<T> simplify(final Expr<T> expr, final Valuation val
                     // Reference
 
                     .addCase(Dereference.class, this::simplifyDereference)
-
-                    //            .addCase(Reference.class, this::simplifyReference)
+                    .addCase(Reference.class, this::simplifyReference)
 
                     // Default
 
@@ -268,6 +264,10 @@ private Expr<?> simplifyDereference(final Dereference<?, ?, ?> expr, final Valua
         return expr.map(it -> simplify(it, val));
     }
 
+    private Expr<?> simplifyReference(final Reference<?, ?> expr, final Valuation val) {
+        return expr.map(it -> simplify(it, val));
+    }
+
     private Expr<?> simplifyArrayRead(final ArrayReadExpr<?, ?> expr, final Valuation val) {
         return simplifyGenericArrayRead(expr, val);
     }

subprojects/frontends/c-frontend/src/main/antlr/C.g4

@@ -29,15 +29,58 @@
 /** C 2011 grammar built from the C11 Spec */
 grammar C;
 
-
+@parser::header {
+ import java.util.LinkedHashSet;
+ import java.util.Set;
+ }
+ @parser::members {
+ private final LinkedHashSet<String> typedefNames = new LinkedHashSet<>(Set.of(
+                                                                            "void",
+                                                                            "_Bool",
+                                                                            "char",
+                                                                            "signed",
+                                                                            "unsigned",
+                                                                            "short",
+                                                                            "int",
+                                                                            "long",
+                                                                            "float",
+                                                                            "double",
+                                                                            "struct",
+                                                                            "enum"
+                                                                        ));
+ private void saveTypedef(DeclarationContext ctx) {
+     if(ctx.initDeclaratorList() == null) return;
+     if(ctx.declarationSpecifiers().declarationSpecifier(0).getText().equals("typedef")) {
+       var dD = ctx.initDeclaratorList().initDeclarator(0).declarator().directDeclarator();
+       while(!(dD instanceof DirectDeclaratorIdContext idDd))
+         dD = (DirectDeclaratorContext) dD.getChild(0);
+       typedefNames.add(idDd.Identifier().getText());
+     }
+ }
+ private boolean isDefinedTypeCast(TokenStream ts) {
+    int i = 1;
+    while(ts.LA(i) == LeftParen) ++i;
+    int parens = 1;
+    while(parens > 0) {
+      int next = ts.LA(i);
+      if(next == RightParen) --parens;
+      else if(next == LeftParen) ++parens;
+      else if(typedefNames.contains(ts.LT(i).getText())) {
+        return true;
+      }
+      ++i;
+    }
+    return false;
+ }
+ }
 primaryExpression
     :   PRETTY_FUNC                                                         # gccPrettyFunc
-    |   Identifier                                                          # primaryExpressionId
+    |   {!typedefNames.contains(_input.LT(1).getText())}? Identifier        # primaryExpressionId
     |   Constant                                                            # primaryExpressionConstant
     |   StringLiteral+                                                      # primaryExpressionStrings
     |   '(' expression ')'                                                  # primaryExpressionBraceExpression
     |   '(' compoundStatement ')'                                           # primaryExpressionCompoundStatement // GNU C extension?
-    |   '(' castDeclarationSpecifierList ')' initializer                    # primaryExpressionTypeInitializer
+    |   '(' castDeclarationSpecifierList ')' initializer                      # primaryExpressionTypeInitializer
     //|   genericSelection                                                    # primaryExpressionGenericSelection
     |   '__extension__'? '(' compoundStatement ')'                          # primaryExpressionGccExtension
     //|   '__builtin_va_arg' '(' unaryExpression ',' typeName ')'             # primaryExpressionBuiltinVaArg
@@ -133,7 +176,7 @@ unaryOperator
     ;
 
 castExpression
-    :   '__extension__'? '(' castDeclarationSpecifierList ')' castExpression    #castExpressionCast
+    :   {isDefinedTypeCast(_input)}? '__extension__'? '(' castDeclarationSpecifierList ')' castExpression    #castExpressionCast
     |   unaryExpression                                     #castExpressionUnaryExpression
 //    |   DigitSequence                                       #castExpressionDigitSequence
     ;
@@ -201,7 +244,7 @@ constantExpression
     ;
 
 declaration
-    :   declarationSpecifiers initDeclaratorList? ';'
+    :   declarationSpecifiers initDeclaratorList? ';' {saveTypedef(_localctx); }
 //    |   staticAssertDeclaration                         # declarationStatic
     ;
 
@@ -575,11 +618,16 @@ translationUnit
 
 externalDeclaration
     :   functionDefinition  #externalFunctionDefinition
+    |   typeDefinition      #externalTypeDefinition
     |   declaration         #globalDeclaration
     |   IncludeDirective    #includeDirective
     |   ';'                 #externalNop
     ;
 
+typeDefinition
+    :   'typedef' declarationSpecifiers Identifier ';' {typedefNames.add($Identifier.text); }
+    ;
+
 functionDefinition
     :   declarationSpecifiers declarator /*declarationList?*/ compoundStatement
     ;

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -16,6 +16,7 @@
 package hu.bme.mit.theta.frontend.transformation.grammar.expression;
 
 import static com.google.common.base.Preconditions.checkState;
+import static hu.bme.mit.theta.core.decl.Decls.Var;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mod;
@@ -104,17 +105,17 @@ public ExpressionVisitor(
         postfixVisitor = new PostfixVisitor();
     }
 
-    protected VarDecl<?> getVar(String name) {
+    protected Optional<VarDecl<?>> getVar(String name) {
         for (Tuple2<String, Map<String, VarDecl<?>>> variableList : variables) {
             if (variableList.get2().containsKey(name)) {
                 VarDecl<?> varDecl = variableList.get2().get(name);
                 if (functions.containsKey(varDecl)) {
                     parseContext.getMetadata().create(name, "shouldInline", false);
                 }
-                return varDecl;
+                return Optional.of(varDecl);
             }
         }
-        return null;
+        return Optional.empty();
     }
 
     public List<CStatement> getPostStatements() {
@@ -575,11 +576,12 @@ public Expr<?> visitUnaryExpressionSizeOrAlignOf(
                                                     .map(it -> (CComplexType) it))
                             .or(
                                     () ->
-                                            Optional.ofNullable(
-                                                    CComplexType.getType(
-                                                            getVar(ctx.typeName().getText())
-                                                                    .getRef(),
-                                                            parseContext)));
+                                            getVar(ctx.typeName().getText())
+                                                    .map(
+                                                            it ->
+                                                                    CComplexType.getType(
+                                                                            it.getRef(),
+                                                                            parseContext)));
 
             if (type.isPresent()) {
                 LitExpr<?> value =
@@ -671,11 +673,7 @@ public Expr<?> visitUnaryExpressionCast(CParser.UnaryExpressionCastContext ctx)
                 parseContext.getMetadata().create(expr, "cType", type);
                 return expr;
             case "&":
-                checkState(
-                        originalOperand instanceof RefExpr<?>
-                                && ((RefExpr<?>) originalOperand).getDecl() instanceof VarDecl,
-                        "Referencing non-variable expressions is not allowed!");
-                return reference((RefExpr<?>) originalOperand);
+                return reference(originalOperand);
             case "*":
                 type = CComplexType.getType(originalOperand, parseContext);
                 if (type instanceof CPointer) type = ((CPointer) type).getEmbeddedType();
@@ -698,7 +696,7 @@ private <T extends Type> Expr<?> dereference(
         return of;
     }
 
-    private Expr<?> reference(RefExpr<?> accept) {
+    private Expr<?> reference(Expr<?> accept) {
         final var newType =
                 new CPointer(null, CComplexType.getType(accept, parseContext), parseContext);
         Reference<Type, ?> of = Reference(accept, newType.getSmtType());
@@ -739,15 +737,16 @@ public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
     public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
         final var name = ctx.Identifier().getText();
         final var variable = getVar(name);
-        if (variable == null) {
+        if (variable.isEmpty()) {
             // no variable found, we try some macros..
             final var ret = fromName(name, parseContext);
             if (ret != null) {
                 return ret;
             }
-            throw new RuntimeException("No such variable or macro: " + name);
+            //throw new RuntimeException("No such variable or macro: " + name);
+            return Var(name, BoolType.getInstance()).getRef();
         } else {
-            return variable.getRef();
+            return variable.get().getRef();
         }
     }
 

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/TypedefVisitor.java

@@ -132,4 +132,15 @@ public Set<CDeclaration> visitCompilationUnit(CParser.CompilationUnitContext ctx
         }
         return declarations;
     }
+
+    @Override
+    public Set<CDeclaration> visitTypeDefinition(CParser.TypeDefinitionContext ctx) {
+        CSimpleType cSimpleType =
+                ctx.declarationSpecifiers().accept(declarationVisitor.getTypeVisitor());
+        CDeclaration cDeclaration = new CDeclaration(ctx.Identifier.getText());
+        cDeclaration.setType(cSimpleType);
+        cDeclaration.incDerefCounter(cSimpleType.getPointerLevel());
+        this.declarations.add(cDeclaration);
+        return Set.of(cDeclaration);
+    }
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java

@@ -154,10 +154,17 @@ private CSimpleType createCType(
                 }
             }
             if (specifierQualifierListContext.typeSpecifierPointer() != null) {
-                CSimpleType qualifierSpecifier =
-                        specifierQualifierListContext.typeSpecifierPointer().accept(this);
-                if (qualifierSpecifier != null) {
-                    cSimpleTypes.add(qualifierSpecifier);
+                if (specifierQualifierListContext.typeSpecifierPointer().typeSpecifier() != null) {
+                    CSimpleType qualifierSpecifier =
+                            specifierQualifierListContext.typeSpecifierPointer().accept(this);
+                    if (qualifierSpecifier != null) {
+                        cSimpleTypes.add(qualifierSpecifier);
+                    }
+                } else {
+                    for (Token star :
+                            specifierQualifierListContext.typeSpecifierPointer().pointer().stars) {
+                        cSimpleTypes.get(cSimpleTypes.size() - 1).incrementPointer();
+                    }
                 }
             }
         }
@@ -320,7 +327,7 @@ public CSimpleType visitTypeSpecifierExtension(CParser.TypeSpecifierExtensionCon
     public CSimpleType visitTypeSpecifierPointer(CParser.TypeSpecifierPointerContext ctx) {
         CSimpleType subtype =
                 ctx.typeSpecifier() == null
-                        ? NamedType("", parseContext, uniqueWarningLogger)
+                        ? NamedType("void", parseContext, uniqueWarningLogger)
                         : ctx.typeSpecifier().accept(this);
         if (subtype == null) {
             return null;

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CCompound.java

@@ -43,8 +43,10 @@ public void insertCStatementsToFront(List<CStatement> cStatements) {
     }
 
     public void addCStatement(CStatement cStatement) {
-        cStatementList.add(cStatement);
-        cStatement.setParent(this);
+        if (cStatement != null) {
+            cStatementList.add(cStatement);
+            cStatement.setParent(this);
+        }
     }
 
     @Override

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java

@@ -173,7 +173,7 @@ public static CComplexType getType(Expr<?> expr, ParseContext parseContext) {
         }
     }
 
-    private static CComplexType getType(Type type, ParseContext parseContext) {
+    public static CComplexType getType(Type type, ParseContext parseContext) {
         if (type instanceof IntType) {
             return new CSignedInt(null, parseContext);
         } else if (type instanceof ArrayType<?, ?> aType) {
@@ -213,6 +213,10 @@ private static CComplexType getType(Type type, ParseContext parseContext) {
                     switch (s) {
                         case "bool":
                             return new CBool(null, parseContext);
+                        case "char":
+                            return ((BvType) type).getSigned()
+                                    ? new CSignedChar(null, parseContext)
+                                    : new CUnsignedChar(null, parseContext);
                         case "short":
                             return ((BvType) type).getSigned()
                                     ? new CSignedShort(null, parseContext)

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java

@@ -66,6 +66,8 @@ private Expr<? extends Type> handleSignedConversion(CInteger type, Expr<?> param
         CComplexType that = CComplexType.getType(param, parseContext);
         if (that instanceof CPointer) {
             that = CComplexType.getUnsignedLong(parseContext);
+        } else if (that instanceof CVoid) {
+            that = CComplexType.getType(param.getType(), parseContext);
         }
         if (that instanceof CReal) {
             //noinspection unchecked

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java

@@ -173,7 +173,10 @@ protected void patch(CSimpleType cSimpleType) {
             case "":
                 break;
             default:
-                if (!cSimpleType.isTypedef()) {
+                if (cSimpleType.getAssociatedName() == null
+                        || cSimpleType.getAssociatedName().isEmpty()) {
+                    cSimpleType.setAssociatedName(namedType);
+                } else if (!cSimpleType.isTypedef()) {
                     throw new UnsupportedFrontendElementException(
                             "namedType should be short or long or type specifier, instead it is "
                                     + namedType);

subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt

@@ -406,13 +406,13 @@ class FrontendXcfaBuilder(
         }
 
         is RefExpr<*> -> {
-          if (
+          /*if (
             (CComplexType.getType(lValue, parseContext) is CPointer ||
               CComplexType.getType(lValue, parseContext) is CArray ||
               CComplexType.getType(lValue, parseContext) is CStruct) && rExpression.hasArithmetic()
           ) {
             throw UnsupportedFrontendElementException("Pointer arithmetic not supported.")
-          }
+          }*/
           // TODO: check if assignment to structs, arrays (stack AND heap) are value- or
           // pointer-based
           AssignStmtLabel(

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt

@@ -42,7 +42,7 @@ constructor(
   val processes: Map<Int, XcfaProcessState>,
   val sGlobal: S,
   val mutexes: Map<String, Set<Int>> = mapOf(),
-  val threadLookup: Map<VarDecl<*>, Int> = emptyMap(),
+  val threadLookup: Map<Expr<*>, Int> = emptyMap(),
   val bottom: Boolean = false,
 ) : ExprState {
 
@@ -148,7 +148,7 @@ constructor(
           is StartLabel -> changes.add { state -> state.start(label, a.pid) }.let { null }
           is JoinLabel -> {
             changes.add { state ->
-              val joinedPid = state.threadLookup[label.pidVar] ?: error("No such thread.")
+              val joinedPid = state.threadLookup[label.handle] ?: error("No such thread.")
               if (joinedPid in state.processes) copy(bottom = true) else state
             }
             null
@@ -173,7 +173,7 @@ constructor(
 
   private fun start(startLabel: StartLabel, startingPid: Int): XcfaState<S> {
     val newProcesses: MutableMap<Int, XcfaProcessState> = LinkedHashMap(processes)
-    val newThreadLookup: MutableMap<VarDecl<*>, Int> = LinkedHashMap(threadLookup)
+    val newThreadLookup: MutableMap<Expr<*>, Int> = LinkedHashMap(threadLookup)
 
     val procedure = xcfa?.procedures?.find { it.name == startLabel.name }!!
     val paramList = procedure.params.toMap()
@@ -194,7 +194,7 @@ constructor(
 
     val pid = pidCnt++
     val lookup = procedure.createLookup("T$pid")
-    newThreadLookup[startLabel.pidVar] = pid
+    newThreadLookup[startLabel.handle] = pid
     newProcesses[pid] =
       XcfaProcessState(
         LinkedList(listOf(procedure.initLoc)),