Xcfa phased procedure pass optimization + unsupported initializer

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

@@ -388,41 +388,43 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
 
     /**
      * Conversion from C (/) semantics to solver (div) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C division semantics with solver operations
      */
     private Expr<?> createIntDiv(Expr<?> a, Expr<?> b) {
         DivExpr<?> aDivB = Div(a, b);
         return Ite(Geq(a, Int(0)),          // if (a >= 0)
-            aDivB,                                //   a div b
-                                                  // else
-            Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
-                Ite(Geq(b, Int(0)),         //     if (b >= 0)
-                    Add(aDivB, Int(1)),     //       a div b + 1
-                                                  //     else
-                    Sub(aDivB, Int(1))      //       a div b - 1
-                ),                                //   else
-                aDivB                             //     a div b
-            )
+                aDivB,                                //   a div b
+                // else
+                Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
+                        Ite(Geq(b, Int(0)),         //     if (b >= 0)
+                                Add(aDivB, Int(1)),     //       a div b + 1
+                                //     else
+                                Sub(aDivB, Int(1))      //       a div b - 1
+                        ),                                //   else
+                        aDivB                             //     a div b
+                )
         );
     }
 
     /**
      * Conversion from C (%) semantics to solver (mod) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C modulo semantics with solver operations
      */
     private Expr<?> createIntMod(Expr<?> a, Expr<?> b) {
         ModExpr<?> aModB = Mod(a, b);
         return Ite(Geq(a, Int(0)),  // if (a >= 0)
-            aModB,                        //   a mod b
-                                          // else
-            Ite(Geq(b, Int(0)),     //   if (b >= 0)
-                Sub(aModB, b),            //     a mod b - b
-                Add(aModB, b)             //     a mod b + b
-            )
+                aModB,                        //   a mod b
+                // else
+                Ite(Geq(b, Int(0)),     //   if (b >= 0)
+                        Sub(aModB, b),            //     a mod b - b
+                        Add(aModB, b)             //     a mod b + b
+                )
         );
     }
 

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

@@ -0,0 +1,42 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.frontend.transformation.grammar.expression;
+
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.LitExpr;
+import hu.bme.mit.theta.core.type.NullaryExpr;
+import hu.bme.mit.theta.core.type.inttype.IntType;
+
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
+
+public class UnsupportedInitializer extends NullaryExpr<IntType> {
+
+    @Override
+    public IntType getType() {
+        return Int();
+    }
+
+    @Override
+    public LitExpr<IntType> eval(Valuation val) {
+        throw new UnsupportedOperationException("UnsupportedInitializer expressions are not supported.");
+    }
+
+    @Override
+    public String toString() {
+        return "UnsupportedInitializer";
+    }
+}

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

@@ -19,9 +19,11 @@
 import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor;
 import hu.bme.mit.theta.c.frontend.dsl.gen.CParser;
 import hu.bme.mit.theta.frontend.ParseContext;
+import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer;
 import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor;
 import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
 import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
+import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CInitializerList;
 import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
@@ -81,13 +83,17 @@ public List<CDeclaration> getDeclarations(CParser.DeclarationSpecifiersContext d
                                 "Initializer list designators not yet implemented!");
                         CInitializerList cInitializerList = new CInitializerList(
                                 cSimpleType.getActualType(), parseContext);
-                        for (CParser.InitializerContext initializer : context.initializer()
-                                .initializerList().initializers) {
-                            CStatement expr = initializer.assignmentExpression()
-                                    .accept(functionVisitor);
-                            cInitializerList.addStatement(null /* TODO: add designator */, expr);
+                        try {
+                            for (CParser.InitializerContext initializer : context.initializer()
+                                    .initializerList().initializers) {
+                                CStatement expr = initializer.assignmentExpression().accept(functionVisitor);
+                                cInitializerList.addStatement(null /* TODO: add designator */, expr);
+                            }
+                            initializerExpression = cInitializerList;
+                        } catch (NullPointerException e) {
+                            initializerExpression = new CExpr(new UnsupportedInitializer(), parseContext);
+                            parseContext.getMetadata().create(initializerExpression.getExpression(), "cType", cSimpleType);
                         }
-                        initializerExpression = cInitializerList;
                     } else {
                         initializerExpression = context.initializer().assignmentExpression()
                                 .accept(functionVisitor);

subprojects/xcfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java

@@ -58,7 +58,7 @@ public class FunctionState {
     public FunctionState(GlobalState globalState, Tuple3<String, Optional<String>, List<Tuple2<String, String>>> function) {
         this.globalState = globalState;
         this.function = function;
-        procedureBuilder = new XcfaProcedureBuilder(function.get1(), new ProcedurePassManager(List.of()));
+        procedureBuilder = new XcfaProcedureBuilder(function.get1(), new ProcedurePassManager());
 //        procedureBuilder.setName(function.get1());
         localVars = new HashMap<>();
         params = new HashSet<>();

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

@@ -37,14 +37,12 @@ import hu.bme.mit.theta.core.stmt.Stmts
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.core.utils.TypeUtils
 import hu.bme.mit.theta.solver.Solver
+import hu.bme.mit.theta.xcfa.*
 import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup
 import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
-import hu.bme.mit.theta.xcfa.getFlatLabels
-import hu.bme.mit.theta.xcfa.getGlobalVars
 import hu.bme.mit.theta.xcfa.isWritten
 import hu.bme.mit.theta.xcfa.model.*
 import hu.bme.mit.theta.xcfa.passes.changeVars
-import hu.bme.mit.theta.xcfa.startsAtomic
 import java.util.*
 import java.util.function.Predicate
 
@@ -153,15 +151,16 @@ fun getXcfaErrorPredicate(
                     if (process1.key != process2.key)
                         for (edge1 in process1.value.locs.peek().outgoingEdges)
                             for (edge2 in process2.value.locs.peek().outgoingEdges) {
-                                val globalVars1 = edge1.getGlobalVars(xcfa)
-                                val globalVars2 = edge2.getGlobalVars(xcfa)
-                                val isAtomic1 = edge1.startsAtomic()
-                                val isAtomic2 = edge2.startsAtomic()
-                                if (!isAtomic1 || !isAtomic2) {
-                                    val intersection = globalVars1.keys intersect globalVars2.keys
-                                    if (intersection.any { globalVars1[it].isWritten || globalVars2[it].isWritten })
-                                        return@Predicate true
-                                }
+                                val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys
+                                val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys
+                                val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1)
+                                val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2)
+                                for (v1 in globalVars1)
+                                    for (v2 in globalVars2)
+                                        if (v1.varDecl == v2.varDecl)
+                                            if (v1.access.isWritten || v2.access.isWritten)
+                                                if ((v1.mutexes intersect v2.mutexes).isEmpty())
+                                                    return@Predicate true
                             }
             false
         }

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

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS
@@ -88,7 +104,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) {
 
     protected fun findDirectObservers(edge: XcfaEdge, prec: Prec) {
         val precVars = prec.usedVars
-        val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars }
+        val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars }
         if (writtenVars.isEmpty()) return
 
         val toVisit = mutableListOf(edge)
@@ -105,7 +121,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) {
         source: XcfaEdge, target: XcfaEdge, observableVars: Map<VarDecl<*>, AccessType>,
         precVars: Collection<VarDecl<*>>, relation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>>
     ) {
-        val vars = target.getVars()
+        val vars = target.collectVarsWithAccessType()
         var relevantAction = vars.any { it.value.isWritten && it.key in precVars }
         if (!relevantAction) {
             val assumeVars = target.label.collectAssumesVars()

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

@@ -1,9 +1,25 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS
 import hu.bme.mit.theta.analysis.Prec
 import hu.bme.mit.theta.xcfa.getFlatLabels
-import hu.bme.mit.theta.xcfa.getVars
+import hu.bme.mit.theta.xcfa.collectVarsWithAccessType
 import hu.bme.mit.theta.xcfa.isWritten
 import hu.bme.mit.theta.xcfa.model.StartLabel
 import hu.bme.mit.theta.xcfa.model.XCFA
@@ -125,7 +141,7 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) {
 
     private fun findInterProcessObservers(edge: XcfaEdge, prec: Prec) {
         val precVars = prec.usedVars
-        val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars }
+        val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars }
         if (writtenVars.isEmpty()) return
 
         xcfa.procedures.forEach { procedure ->

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

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS

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

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.por
 
 import hu.bme.mit.theta.analysis.LTS

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

@@ -23,8 +23,10 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.model.XCFA
 
-open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>) :
-    XcfaSporLts(xcfa) {
+open class XcfaAasporLts(
+    xcfa: XCFA,
+    private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>
+) : XcfaSporLts(xcfa) {
 
     override fun <P : Prec> getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection<XcfaAction>,
         prec: P): Set<XcfaAction> {

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

@@ -25,7 +25,7 @@ import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.analysis.getXcfaLts
-import hu.bme.mit.theta.xcfa.getGlobalVars
+import hu.bme.mit.theta.xcfa.collectIndirectGlobalVarAccesses
 import hu.bme.mit.theta.xcfa.isWritten
 import hu.bme.mit.theta.xcfa.model.XCFA
 import java.util.*
@@ -456,8 +456,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
     protected open fun dependent(a: A, b: A): Boolean {
         if (a.pid == b.pid) return true
 
-        val aGlobalVars = a.edge.getGlobalVars(xcfa)
-        val bGlobalVars = b.edge.getGlobalVars(xcfa)
+        val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa)
+        val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa)
         // dependent if they access the same variable (at least one write)
         return (aGlobalVars.keys intersect bGlobalVars.keys).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten }
     }
@@ -488,8 +488,8 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) {
         if (a.pid == b.pid) return true
 
         val precVars = prec?.usedVars?.toSet() ?: return super.dependent(a, b)
-        val aGlobalVars = a.edge.getGlobalVars(xcfa)
-        val bGlobalVars = b.edge.getGlobalVars(xcfa)
+        val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa)
+        val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa)
         // dependent if they access the same variable in the precision (at least one write)
         return (aGlobalVars.keys intersect bGlobalVars.keys intersect precVars).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten }
     }