Skip to content

Commit 6f9e741

Browse files
leventeBajczileventeBajczi
authored
Merge pull request #391 from csanadtelbisz/xcfa-fall-2025-fixes
Various XCFA improvements
2 parents 2039958 + b307f61 commit 6f9e741

File tree

124 files changed

+8948
-2434
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

124 files changed

+8948
-2434
lines changed

‎.idea/codeStyles/Project.xml‎

Lines changed: 10 additions & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎build.gradle.kts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ buildscript {
2929

3030
allprojects {
3131
group = "hu.bme.mit.theta"
32-
version = "6.19.3"
32+
version = "6.20.1"
3333

3434

3535
apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))

‎scripts/complex.kts‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ var baseConfig = XcfaCegarConfig(
4848
maxEnum = 1,
4949
search = Search.ERR,
5050
initPrec = InitPrec.EMPTY,
51-
porLevel = POR.NOPOR,
51+
por = POR.NOPOR,
5252
refinementSolver = "Z3",
5353
validateRefinementSolver = false,
5454
refinement = Refinement.SEQ_ITP,
@@ -59,10 +59,10 @@ var baseConfig = XcfaCegarConfig(
5959
)
6060

6161
if (traitsTyped.multithreaded) {
62-
baseConfig = baseConfig.copy(search = Search.BFS, porLevel = POR.AASPOR, pruneStrategy = PruneStrategy.LAZY)
62+
baseConfig = baseConfig.copy(search = Search.BFS, por = POR.AASPOR, pruneStrategy = PruneStrategy.LAZY)
6363

6464
if (propertyTyped == ErrorDetection.DATA_RACE) {
65-
baseConfig = baseConfig.copy(porLevel = POR.SPOR)
65+
baseConfig = baseConfig.copy(por = POR.SPOR)
6666
}
6767
}
6868

‎scripts/simple.kts‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ var baseConfig = XcfaCegarConfig(
3636
maxEnum = 1,
3737
search = Search.ERR,
3838
initPrec = InitPrec.EMPTY,
39-
porLevel = POR.NOPOR,
39+
por = POR.NOPOR,
4040
refinementSolver = "Z3",
4141
validateRefinementSolver = false,
4242
refinement = Refinement.SEQ_ITP,
@@ -47,11 +47,11 @@ var baseConfig = XcfaCegarConfig(
4747
)
4848

4949
if (traitsTyped.multithreaded) {
50-
baseConfig = baseConfig.copy(search = Search.BFS, porLevel = POR.AAPOR,
50+
baseConfig = baseConfig.copy(search = Search.BFS, por = POR.AAPOR,
5151
pruneStrategy = PruneStrategy.LAZY)
5252

5353
if (propertyTyped == ErrorDetection.DATA_RACE) {
54-
baseConfig = baseConfig.copy(porLevel = POR.BASIC)
54+
baseConfig = baseConfig.copy(por = POR.BASIC)
5555
}
5656
}
5757

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -95,10 +95,12 @@ abstract class OcCheckerBase<E : Event> : OcChecker<E>() {
9595

9696
protected fun derive(rels: GlobalRelation, rf: Relation<E>, w: E): Reason? =
9797
when {
98-
!rf.from.sameMemory(w) -> null // different referenced memory locations
99-
rf.from.clkId == rf.to.clkId -> null // rf within an atomic block
100-
w.clkId == rf.from.clkId || w.clkId == rf.to.clkId ->
101-
null // w within an atomic block with one of the rf ends
98+
rf.from.clkId == rf.to.clkId -> null
99+
// rf within an atomic block
100+
w.clkId == rf.from.clkId || w.clkId == rf.to.clkId -> null
101+
// w within an atomic block with one of the rf ends
102+
!rf.to.sameMemory(w) -> null
103+
// different memory locations (checking with rf.to due to common memory garbage event)
102104

103105
rels[w.clkId, rf.to.clkId] != null -> { // WS derivation
104106
val reason = WriteSerializationReason(rf, w, rels[w.clkId, rf.to.clkId]!!)
@@ -159,7 +161,7 @@ abstract class OcCheckerBase<E : Event> : OcChecker<E>() {
159161
/**
160162
* Represents the known value of an important element for ordering consistency checking. Such an
161163
* important element is either a relation (being enabled) or an event (being enabled - having a
162-
* guard that evaluates to true). The fix (closed by theory axioms) relations and the solver
164+
* guard that evaluates to true). The fix relations (closed by theory axioms) and the solver
163165
* decision stack level are also stored.
164166
*/
165167
open class OcAssignment<E : Event>

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

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -745,10 +745,6 @@ public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
745745
@Override
746746
public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
747747
final var variable = getVar(ctx.Identifier().getText());
748-
if (atomicVars.contains(variable)) {
749-
preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext));
750-
postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext));
751-
}
752748
return variable.getRef();
753749
}
754750

@@ -1009,6 +1005,12 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionIncrement(
10091005
// no need to truncate here, as left and right side types are the same
10101006
CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
10111007
postStatements.add(0, cAssignment);
1008+
if (primary instanceof RefExpr
1009+
&& atomicVars.contains(((RefExpr<?>) primary).getDecl())) {
1010+
preStatements.add(
1011+
new CCall("__VERIFIER_atomic_begin", List.of(), parseContext));
1012+
postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext));
1013+
}
10121014
if (functionVisitor != null) functionVisitor.recordMetadata(ctx, cAssignment);
10131015
if (functionVisitor != null) functionVisitor.recordMetadata(ctx, cexpr);
10141016
return primary;
@@ -1030,6 +1032,12 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionDecrement(
10301032
// no need to truncate here, as left and right side types are the same
10311033
CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
10321034
postStatements.add(0, cAssignment);
1035+
if (primary instanceof RefExpr
1036+
&& atomicVars.contains(((RefExpr<?>) primary).getDecl())) {
1037+
preStatements.add(
1038+
new CCall("__VERIFIER_atomic_begin", List.of(), parseContext));
1039+
postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext));
1040+
}
10331041
if (functionVisitor != null) functionVisitor.recordMetadata(ctx, cAssignment);
10341042
if (functionVisitor != null) functionVisitor.recordMetadata(ctx, cexpr);
10351043
return expr;

‎subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -685,10 +685,10 @@ public CStatement visitAssignmentExpressionAssignmentExpression(
685685
CAssignment cAssignment =
686686
new CAssignment(ret, rhs, ctx.assignmentOperator().getText(), parseContext);
687687
compound.addCStatement(cAssignment);
688-
expressionVisitor.getPreStatements().forEach(compound::addCStatement);
688+
expressionVisitor.getPreStatements().forEach(preStatements::addCStatement);
689689
compound.setPreStatements(preStatements);
690690
recordMetadata(ctx, compound);
691-
expressionVisitor.getPostStatements().forEach(compound::addCStatement);
691+
expressionVisitor.getPostStatements().forEach(postStatements::addCStatement);
692692
compound.setPostStatements(postStatements);
693693
recordMetadata(ctx, compound);
694694
return compound;

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,5 @@ public enum ArithmeticTrait {
2020
NONLIN_INT,
2121
BITWISE,
2222
FLOAT,
23-
ARR,
24-
MULTITHREAD
23+
ARR
2524
}

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -59,19 +59,26 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CSt
5959
import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger
6060
import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall
6161
import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory
62-
import hu.bme.mit.theta.xcfa.AssignStmtLabel
62+
import hu.bme.mit.theta.xcfa.ErrorDetection
63+
import hu.bme.mit.theta.xcfa.XcfaProperty
6364
import hu.bme.mit.theta.xcfa.model.*
6465
import hu.bme.mit.theta.xcfa.passes.CPasses
6566
import hu.bme.mit.theta.xcfa.passes.MemsafetyPass
67+
import hu.bme.mit.theta.xcfa.utils.AssignStmtLabel
6668
import java.math.BigInteger
6769
import java.util.stream.Collectors
6870

6971
class FrontendXcfaBuilder(
7072
val parseContext: ParseContext,
71-
val checkOverflow: Boolean = false,
73+
val property: XcfaProperty,
7274
val uniqueWarningLogger: Logger,
7375
) : CStatementVisitorBase<FrontendXcfaBuilder.ParamPack, XcfaLocation>() {
7476

77+
private val checkOverflow: Boolean =
78+
(property.inputProperty == ErrorDetection.OVERFLOW).also {
79+
if (it) property.transformSpecification(ErrorDetection.NO_ERROR)
80+
}
81+
7582
private val locationLut: MutableMap<String, XcfaLocation> = LinkedHashMap()
7683
private var ptrCnt = 1 // counts up, uses 3k+1
7784
get() = field.also { field += 3 }
@@ -107,7 +114,7 @@ class FrontendXcfaBuilder(
107114
fun buildXcfa(cProgram: CProgram): XcfaBuilder {
108115
val builder = XcfaBuilder(cProgram.id ?: "")
109116
val initStmtList: MutableList<XcfaLabel> = ArrayList()
110-
if (MemsafetyPass.NEED_CHECK) {
117+
if (MemsafetyPass.enabled) {
111118
val fitsall = Fitsall.getFitsall(parseContext)
112119
val ptrType = CPointer(null, null, parseContext)
113120
val ptrSize =
@@ -158,7 +165,7 @@ class FrontendXcfaBuilder(
158165
)
159166
)
160167
)
161-
if (MemsafetyPass.NEED_CHECK) {
168+
if (MemsafetyPass.enabled) {
162169
val bounds = globalDeclaration.get1().arrayDimensions[0].expression
163170
checkState(
164171
bounds is IntLitExpr || bounds is BvLitExpr,
@@ -257,7 +264,7 @@ class FrontendXcfaBuilder(
257264
val funcDecl = function.funcDecl
258265
val compound = function.compound
259266
val builder =
260-
XcfaProcedureBuilder(funcDecl.name, CPasses(checkOverflow, parseContext, uniqueWarningLogger))
267+
XcfaProcedureBuilder(funcDecl.name, CPasses(property, parseContext, uniqueWarningLogger))
261268
xcfaBuilder.addProcedure(builder)
262269
val initStmtList = ArrayList<XcfaLabel>()
263270
if (param.size > 0 && builder.name.equals("main")) {

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ import hu.bme.mit.theta.frontend.transformation.grammar.expression.ExpressionVis
3131
import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor
3232
import hu.bme.mit.theta.frontend.transformation.model.statements.CProgram
3333
import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
34+
import hu.bme.mit.theta.xcfa.XcfaProperty
3435
import hu.bme.mit.theta.xcfa.model.XCFA
3536
import java.io.InputStream
3637
import java.util.ArrayDeque
@@ -43,7 +44,7 @@ fun getXcfaFromC(
4344
stream: InputStream,
4445
parseContext: ParseContext,
4546
collectStatistics: Boolean,
46-
checkOverflow: Boolean,
47+
property: XcfaProperty,
4748
warningLogger: Logger,
4849
): Triple<XCFA, CStatistics?, Pair<XcfaStatistics, XcfaStatistics>?> {
4950
val input = CharStreams.fromStream(stream)
@@ -56,7 +57,7 @@ fun getXcfaFromC(
5657
val program = context.accept(FunctionVisitor(parseContext, warningLogger))
5758
check(program is CProgram)
5859

59-
val frontendXcfaBuilder = FrontendXcfaBuilder(parseContext, checkOverflow, warningLogger)
60+
val frontendXcfaBuilder = FrontendXcfaBuilder(parseContext, property, warningLogger)
6061
val builder = frontendXcfaBuilder.buildXcfa(program)
6162
val xcfa = builder.build()
6263

0 commit comments

Comments
 (0)