From d0db08386edd5218751bbff60b34c6f354c38cbf Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 18:08:42 +0100 Subject: [PATCH 01/22] Added support for memsafety and memcleanup --- .../mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 28 +++ .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 5 + .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 26 +- .../mit/theta/xcfa/cli/portfolio/complex25.kt | 40 +++ .../mit/theta/xcfa/cli/utils/PropertyUtils.kt | 8 + .../hu/bme/mit/theta/xcfa/model/PtrSize.kt | 56 +++++ .../theta/xcfa/passes/MallocFunctionPass.kt | 17 +- .../mit/theta/xcfa/passes/MemsafetyPass.kt | 232 ++++++++++++++++++ .../theta/xcfa/passes/ProcedurePassManager.kt | 1 + .../theta/xcfa/passes/ReferenceElimination.kt | 10 +- 10 files changed, 415 insertions(+), 8 deletions(-) create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index fe963cb479..45cdde8e73 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -21,13 +21,16 @@ import com.google.common.base.Preconditions import com.google.common.base.Preconditions.checkState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.decl.Decls.Var import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.stmt.AssignStmt import hu.bme.mit.theta.core.stmt.MemoryAssignStmt import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.stmt.Stmts.Assume import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.LitExpr import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs +import hu.bme.mit.theta.core.type.abstracttype.ModExpr import hu.bme.mit.theta.core.type.anytype.Dereference import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference import hu.bme.mit.theta.core.type.anytype.RefExpr @@ -40,6 +43,7 @@ import hu.bme.mit.theta.core.utils.BvUtils import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.TypeUtils.cast import hu.bme.mit.theta.frontend.ParseContext +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer import hu.bme.mit.theta.frontend.transformation.model.statements.* import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType @@ -52,6 +56,7 @@ import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFa import hu.bme.mit.theta.xcfa.AssignStmtLabel import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.passes.CPasses +import hu.bme.mit.theta.xcfa.passes.MemsafetyPass import java.math.BigInteger import java.util.stream.Collectors @@ -122,6 +127,14 @@ class FrontendXcfaBuilder( ) ) ) + if (MemsafetyPass.NEED_CHECK) { + val bounds = globalDeclaration.get1().arrayDimensions[0].expression + checkState( + bounds is IntLitExpr || bounds is BvLitExpr, + "Only IntLit and BvLit expression expected here.", + ) + initStmtList.add(builder.allocate(parseContext, globalDeclaration.get2().ref, bounds)) + } } else { if ( globalDeclaration.get1().initExpr != null && @@ -321,6 +334,13 @@ class FrontendXcfaBuilder( } is RefExpr<*> -> { + 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.") + } AssignStmtLabel( lValue, cast(CComplexType.getType(lValue, parseContext).castTo(rExpression), lValue.type), @@ -1058,3 +1078,11 @@ class FrontendXcfaBuilder( } } } + +private fun Expr<*>.hasArithmetic(): Boolean = + when (this) { + is ModExpr -> ops.any { it.hasArithmetic() } + is LitExpr -> false + is RefExpr -> false + else -> true + } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 115be3a907..5f65d7055f 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -204,6 +204,8 @@ enum class ErrorDetection { ERROR_LOCATION, DATA_RACE, OVERFLOW, + MEMSAFETY, + MEMCLEANUP, NO_ERROR, } @@ -211,6 +213,7 @@ fun getXcfaErrorPredicate( errorDetection: ErrorDetection ): Predicate>> = when (errorDetection) { + ErrorDetection.MEMSAFETY, ErrorDetection.ERROR_LOCATION -> Predicate>> { s -> s.processes.any { it.value.locs.peek().error } @@ -246,6 +249,8 @@ fun getXcfaErrorPredicate( ErrorDetection.NO_ERROR, ErrorDetection.OVERFLOW -> Predicate>> { false } + + ErrorDetection.MEMCLEANUP -> TODO() } fun getPartialOrder(partialOrd: PartialOrd>) = diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 3b06ebfd55..1a2aae35d2 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -56,10 +56,7 @@ import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.XcfaLabel import hu.bme.mit.theta.xcfa.model.toDot -import hu.bme.mit.theta.xcfa.passes.FetchExecuteWriteback -import hu.bme.mit.theta.xcfa.passes.LbePass -import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass -import hu.bme.mit.theta.xcfa.passes.StaticCoiPass +import hu.bme.mit.theta.xcfa.passes.* import hu.bme.mit.theta.xcfa.toC import hu.bme.mit.theta.xcfa2chc.toSMT2CHC import java.io.File @@ -100,6 +97,9 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq XcfaSporLts.random = random XcfaDporLts.random = random } + if (config.inputConfig.property == ErrorDetection.MEMSAFETY) { + MemsafetyPass.NEED_CHECK = true + } if (config.debugConfig.argToFile) { WebDebuggerLogger.enableWebDebuggerLogger() WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) @@ -251,6 +251,24 @@ private fun backend( else SafetyResult.unknown() } + result.isUnsafe && config.inputConfig.property == ErrorDetection.MEMSAFETY -> { + // need to determine what kind + val trace = result.asUnsafe().cex as? Trace, XcfaAction> + val namedState = + trace + ?.states + ?.asReversed() + ?.getOrNull(1) + ?.processes + ?.values + ?.firstOrNull() + ?.locs + ?.firstOrNull() + ?.name + println(namedState) + result + } + else -> result } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt index 7af6f13ee0..64fc73ff93 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt @@ -45,6 +45,7 @@ import hu.bme.mit.theta.xcfa.cli.params.Refinement.NWT_IT_WP import hu.bme.mit.theta.xcfa.cli.params.Refinement.SEQ_ITP import hu.bme.mit.theta.xcfa.cli.params.Search.* import hu.bme.mit.theta.xcfa.cli.runConfig +import hu.bme.mit.theta.xcfa.dereferences import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.optimizeFurther import hu.bme.mit.theta.xcfa.passes.* @@ -236,6 +237,45 @@ fun complexPortfolio25( ) } + if (xcfa.procedures.any { it.edges.any { it.label.dereferences.isNotEmpty() } }) { + val inProcEdges = LinkedHashSet() + val notInProcEdges = LinkedHashSet() + val edges = LinkedHashSet() + + val explTrue = + ConfigNode( + "PTR-expl-inproc", + baseConfig.adaptConfig(inProcess = true, domain = EXPL, timeoutMs = 100_000), + checker, + ) + val predTrue = + ConfigNode( + "PTR-pred-inproc", + baseConfig.adaptConfig(inProcess = true, domain = PRED_CART), + checker, + ) + inProcEdges.add(Edge(explTrue, predTrue, timeoutOrNotSolvableError)) + val inproc = HierarchicalNode("inProc", STM(explTrue, inProcEdges)) + + val explFalse = + ConfigNode( + "PTR-expl-notinproc", + baseConfig.adaptConfig(inProcess = false, domain = EXPL, timeoutMs = 100_000), + checker, + ) + val predFalse = + ConfigNode( + "PTR-pred-notinproc", + baseConfig.adaptConfig(inProcess = false, domain = PRED_CART), + checker, + ) + notInProcEdges.add(Edge(explFalse, predFalse, anyError)) + val notinproc = HierarchicalNode("notInProc", STM(explFalse, notInProcEdges)) + + edges.add(Edge(inproc, notinproc, anyError)) + return if (portfolioConfig.debugConfig.debug) notinproc.innerSTM else STM(inproc, edges) + } + fun getStm(trait: ArithmeticTrait, inProcess: Boolean): STM { val edges = LinkedHashSet() val config_BITWISE_EXPL_NWT_IT_WP_cvc5 = diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt index 967b38ed04..29d77fda52 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt @@ -35,6 +35,14 @@ fun determineProperty(config: XcfaConfig<*, *>, logger: Logger): ErrorDetection ErrorDetection.OVERFLOW } + propertyFile.name.endsWith("valid-memsafety.prp") -> { + ErrorDetection.MEMSAFETY + } + + propertyFile.name.endsWith("valid-memcleanup.prp") -> { + ErrorDetection.MEMCLEANUP + } + else -> { logger.write( Logger.Level.INFO, diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt new file mode 100644 index 0000000000..8decd5d933 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt @@ -0,0 +1,56 @@ +/* + * Copyright 2024 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.model + +import hu.bme.mit.theta.core.decl.Decls.Var +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr +import hu.bme.mit.theta.core.type.arraytype.ArrayType +import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.frontend.ParseContext +import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall +import hu.bme.mit.theta.xcfa.AssignStmtLabel + +fun XcfaBuilder.getPtrSizeVar(type: CComplexType): VarDecl> = + getPtrSizeVar(type.smtType, type.nullValue as Expr) + +fun XcfaBuilder.getPtrSizeVar(intType: Type, nullValue: Expr): VarDecl> = + (getVars().find { it.wrappedVar.name == "__theta_ptr_size" }?.wrappedVar + ?: XcfaGlobalVar( + Var("__theta_ptr_size", ArrayType.of(intType, intType)), + ArrayLitExpr.of(listOf(), nullValue, ArrayType.of(intType, intType)), + ) + .also { addVar(it) } + .wrappedVar) + as VarDecl> + +fun XcfaBuilder.allocate(parseContext: ParseContext, base: Expr<*>, size: Expr<*>): StmtLabel { + val type = Fitsall(null, parseContext) + val arr = getPtrSizeVar(type) + val baseCast = if (type.smtType is IntType) base else type.castTo(base) + val sizeCast = if (type.smtType is IntType) size else type.castTo(size) + val write = ArrayWriteExpr.create(arr.ref, baseCast, sizeCast) + return AssignStmtLabel(arr, write) +} + +fun XcfaBuilder.allocateUnit(parseContext: ParseContext, base: Expr<*>): StmtLabel { + val type = Fitsall(null, parseContext) + return allocate(parseContext, base, type.unitValue) +} diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt index 0cbacc5f94..97538816ff 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt @@ -54,10 +54,16 @@ class MallocFunctionPass(val parseContext: ParseContext) : ProcedurePass { if (predicate((e.label as SequenceLabel).labels[0])) { val invokeLabel = e.label.labels[0] as InvokeLabel val ret = invokeLabel.params[0] as RefExpr<*> + val arg = invokeLabel.params[1] if (builder.parent.getVars().none { it.wrappedVar == mallocVar }) { // initial creation builder.parent.addVar( XcfaGlobalVar(mallocVar, CComplexType.getType(ret, parseContext).nullValue) ) + if (MemsafetyPass.NEED_CHECK) { + builder.parent.addVar( + XcfaGlobalVar(mallocVar, CComplexType.getType(ret, parseContext).nullValue) + ) + } val initProc = builder.parent.getInitProcedures().map { it.first } check(initProc.size == 1) { "Multiple start procedure are not handled well" } initProc.forEach { proc -> @@ -89,9 +95,14 @@ class MallocFunctionPass(val parseContext: ParseContext) : ProcedurePass { invokeLabel.metadata, ) val assign2 = AssignStmtLabel(ret, cast(mallocVar.ref, ret.type)) - builder.addEdge( - XcfaEdge(e.source, e.target, SequenceLabel(listOf(assign1, assign2)), e.metadata) - ) + val labels = + if (MemsafetyPass.NEED_CHECK) { + val assign3 = builder.parent.allocate(parseContext, ret, arg) + listOf(assign1, assign2, assign3) + } else { + listOf(assign1, assign2) + } + builder.addEdge(XcfaEdge(e.source, e.target, SequenceLabel(labels), e.metadata)) } else { builder.addEdge(e) } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt new file mode 100644 index 0000000000..a313f858e5 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -0,0 +1,232 @@ +/* + * Copyright 2024 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.passes + +import hu.bme.mit.theta.core.decl.Decls.Var +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.Stmts.Assume +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.* +import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.Or +import hu.bme.mit.theta.frontend.ParseContext +import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall +import hu.bme.mit.theta.xcfa.dereferences +import hu.bme.mit.theta.xcfa.model.* + +/** + * Adds assumptions to the XCFA if memory safety needs to be checked. Rules based on: + * https://sv-comp.sosy-lab.org/2025/rules.php Summary: + * - valid-free: All memory deallocations are valid (counterexample: invalid free). More precisely: + * There exists no finite execution of the program on which an invalid memory deallocation occurs. + * - inserted check: at every free, we check if pointer is valid (no NULLPTR, no double free). + * - valid-deref: All pointer dereferences are valid (counterexample: invalid dereference). More + * precisely: There exists no finite execution of the program on which an invalid pointer + * dereference occurs. + * - inserted check: at every dereference, we check if pointer is valid (non-null, non-freed, + * in-size) + * - valid-memtrack: All allocated memory is tracked, i.e., pointed to or deallocated + * (counterexample: memory leak). More precisely: There exists no finite execution of the program + * on which the program lost track of some previously allocated memory. (Comparison to Valgrind: + * This property is violated if Valgrind reports 'definitely lost'.) + * - inserted check: we keep track of variables. + */ +class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { + + companion object { + var NEED_CHECK = false + } + + val variableUsedAsPtr = LinkedHashSet>() + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + if (!NEED_CHECK) return builder + + annotateFree(builder) + + annotateDeref(builder) + + annotateLost(builder) + + return builder + } + + private val pointerType = CPointer(null, null, parseContext) + val fitsall = Fitsall(null, parseContext) + + private fun annotateFree(builder: XcfaProcedureBuilder) { + val errorLoc = + builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } + + val invalidFree = XcfaLocation("__THETA_bad-free", metadata = EmptyMetaData) + builder.addLoc(invalidFree) + for (edge in ArrayList(builder.getEdges())) { + val edges = edge.splitIf(this::free) + if ( + edges.size > 1 || (edges.size == 1 && free((edges[0].label as SequenceLabel).labels[0])) + ) { + builder.removeEdge(edge) + edges.forEach { + if (free((it.label as SequenceLabel).labels[0])) { + val invokeLabel = it.label.labels[0] as InvokeLabel + val argument = (invokeLabel.params[1] as RefExpr<*>).decl as VarDecl<*> + val sizeVar = builder.parent.getPtrSizeVar(fitsall) + val derefAssume = + Assume( + Or( + Leq(argument.ref, pointerType.nullValue), // uninit ptr + // freed/not big enough ptr + Leq( + ArrayReadExpr.create(sizeVar.ref, argument.ref), + pointerType.nullValue, + ), // freed/not big enough ptr + ) + ) + + builder.addEdge( + XcfaEdge( + it.source, + it.target, + SequenceLabel( + listOf(builder.parent.allocate(parseContext, argument.ref, fitsall.nullValue)) + ), + it.metadata, + ) + ) + builder.addEdge( + XcfaEdge( + it.source, + invalidFree, + SequenceLabel(listOf(StmtLabel(derefAssume))), + it.metadata, + ) + ) + builder.addEdge( + XcfaEdge(invalidFree, errorLoc, SequenceLabel(listOf(NopLabel)), it.metadata) + ) + } else { + builder.addEdge(it) + } + } + } + } + } + + private fun annotateDeref(builder: XcfaProcedureBuilder) { + val errorLoc = + builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } + val badDeref = XcfaLocation("__THETA_bad-deref", metadata = EmptyMetaData) + builder.addLoc(badDeref) + for (edge in ArrayList(builder.getEdges())) { + val edges = edge.splitIf(this::deref) + if ( + edges.size > 1 || (edges.size == 1 && deref((edges[0].label as SequenceLabel).labels[0])) + ) { + builder.removeEdge(edge) + edges.forEach { + if (deref((it.label as SequenceLabel).labels[0])) { + val derefAssume = + Assume( + Or( + Or( + it.label.labels[0].dereferences.map { Leq(it.array, pointerType.nullValue) } + ), // uninit ptr + Or( + it.label.labels[0].dereferences.map { + val sizeVar = builder.parent.getPtrSizeVar(fitsall) + Leq( + ArrayReadExpr.create(sizeVar.ref, it.array), + it.offset, + ) // freed/not big enough ptr + } + ), + Or( + it.label.labels[0].dereferences.map { + Lt(it.offset, fitsall.nullValue) // negative index + } + ), + ) + ) + builder.addEdge(it) + builder.addEdge( + XcfaEdge( + it.source, + badDeref, + SequenceLabel( + listOf(StmtLabel(derefAssume)) + ), // deref(x a), x <= 0 || a >= sizeof(x) + it.metadata, + ) + ) + builder.addEdge( + XcfaEdge(badDeref, errorLoc, SequenceLabel(listOf(NopLabel)), it.metadata) + ) + } else { + builder.addEdge(it) + } + } + } + } + } + + fun annotateLost(builder: XcfaProcedureBuilder) { + val finalLoc = + builder.finalLoc.orElseGet { builder.createFinalLoc().let { builder.finalLoc.get() } } + val lostLoc = XcfaLocation("__THETA_lost", metadata = EmptyMetaData) + builder.addLoc(lostLoc) + + val sizeVar = builder.parent.getPtrSizeVar(fitsall) + val anyBase = + builder.parent.getVars().find { it.wrappedVar.name == "__ptr" }?.wrappedVar + ?: XcfaGlobalVar(Var("__ptr", sizeVar.type.indexType), pointerType.nullValue) + .also { builder.parent.addVar(it) } + .wrappedVar + val remained = Gt(ArrayReadExpr.create(sizeVar.ref, anyBase.ref), fitsall.nullValue) + + for (incomingEdge in finalLoc.incomingEdges) { + builder.removeEdge(incomingEdge) + val newLoc = XcfaLocation("pre-final", metadata = EmptyMetaData) + builder.addLoc(newLoc) + builder.addEdge(incomingEdge.withTarget(newLoc)) + builder.addEdge( + XcfaEdge( + newLoc, + lostLoc, + label = SequenceLabel(listOf(StmtLabel(Assume(remained)))), + metadata = EmptyMetaData, + ) + ) + builder.addEdge( + XcfaEdge( + lostLoc, + finalLoc, + label = SequenceLabel(listOf(NopLabel)), + metadata = EmptyMetaData, + ) + ) + } + } + + private fun free(it: XcfaLabel): Boolean { + return it is InvokeLabel && it.name == "free" + } + + private fun deref(it: XcfaLabel): Boolean { + return it.dereferences.isNotEmpty() + } +} diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index f9979b3aae..3b3cb24561 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -58,6 +58,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL listOf(StaticCoiPass()), listOf( // handling remaining function calls + MemsafetyPass(parseContext), NoSideEffectPass(parseContext), NondetFunctionPass(), LbePass(parseContext), diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index 9a10822fc4..fc14f52ea6 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -107,7 +107,15 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { builder.addVar(varDecl) parseContext.metadata.create(varDecl.ref, "cType", ptrType) val assign2 = AssignStmtLabel(varDecl, ptrVar.ref) - Pair(varDecl, SequenceLabel(listOf(assign1, assign2))) + val labels = + if (MemsafetyPass.NEED_CHECK) { + val assign3 = builder.parent.allocateUnit(parseContext, varDecl.ref) + + listOf(assign1, assign2, assign3) + } else { + listOf(assign1, assign2) + } + Pair(varDecl, SequenceLabel(labels)) } if (builder.parent.getInitProcedures().any { it.first == builder }) { From 56edf4a5d2491865edd1100e13f96d056998e037 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 18:10:43 +0100 Subject: [PATCH 02/22] Added memcleanup --- .../main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt | 3 +-- .../src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 5 ++++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 5f65d7055f..1b41de5b1d 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -214,6 +214,7 @@ fun getXcfaErrorPredicate( ): Predicate>> = when (errorDetection) { ErrorDetection.MEMSAFETY, + ErrorDetection.MEMCLEANUP, ErrorDetection.ERROR_LOCATION -> Predicate>> { s -> s.processes.any { it.value.locs.peek().error } @@ -249,8 +250,6 @@ fun getXcfaErrorPredicate( ErrorDetection.NO_ERROR, ErrorDetection.OVERFLOW -> Predicate>> { false } - - ErrorDetection.MEMCLEANUP -> TODO() } fun getPartialOrder(partialOrd: PartialOrd>) = diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 1a2aae35d2..87f78612fe 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -97,7 +97,10 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq XcfaSporLts.random = random XcfaDporLts.random = random } - if (config.inputConfig.property == ErrorDetection.MEMSAFETY) { + if ( + config.inputConfig.property == ErrorDetection.MEMSAFETY || + config.inputConfig.property == ErrorDetection.MEMCLEANUP + ) { MemsafetyPass.NEED_CHECK = true } if (config.debugConfig.argToFile) { From 12b16fd62242a4c0f58849416195edbcf4cc2dc6 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 18:11:41 +0100 Subject: [PATCH 03/22] version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index c3b28cbddc..19d6102585 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.8.2" + version = "6.8.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From 955f0de6817bcb75d5e598ba3c6528a5c00c60bb Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 18:41:04 +0100 Subject: [PATCH 04/22] fixed pointer arithmetic check --- .../bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 45cdde8e73..c6c5b2868a 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -28,9 +28,11 @@ import hu.bme.mit.theta.core.stmt.MemoryAssignStmt import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.stmt.Stmts.Assume import hu.bme.mit.theta.core.type.Expr -import hu.bme.mit.theta.core.type.LitExpr import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs -import hu.bme.mit.theta.core.type.abstracttype.ModExpr +import hu.bme.mit.theta.core.type.abstracttype.AddExpr +import hu.bme.mit.theta.core.type.abstracttype.DivExpr +import hu.bme.mit.theta.core.type.abstracttype.MulExpr +import hu.bme.mit.theta.core.type.abstracttype.SubExpr import hu.bme.mit.theta.core.type.anytype.Dereference import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference import hu.bme.mit.theta.core.type.anytype.RefExpr @@ -1081,8 +1083,9 @@ class FrontendXcfaBuilder( private fun Expr<*>.hasArithmetic(): Boolean = when (this) { - is ModExpr -> ops.any { it.hasArithmetic() } - is LitExpr -> false - is RefExpr -> false - else -> true + is AddExpr -> true + is SubExpr -> true + is DivExpr -> true + is MulExpr -> true + else -> ops.any { it.hasArithmetic() } } From 38c82353a57a9799c464fdbc69915b515693e304 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 20:47:33 +0100 Subject: [PATCH 05/22] Handling fix-sized arrays --- .../model/declaration/CDeclaration.java | 25 ++++++----- .../model/types/complex/compound/CArray.java | 19 +++++++-- .../mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 41 +++++++++++++++++++ .../hu/bme/mit/theta/xcfa/model/PtrSize.kt | 18 ++------ .../mit/theta/xcfa/passes/MemsafetyPass.kt | 12 +++--- 5 files changed, 80 insertions(+), 35 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java index 7242590d40..cd00c718f1 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java @@ -13,20 +13,18 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.frontend.transformation.model.declaration; +import static com.google.common.base.Preconditions.checkNotNull; + import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray; import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType; - import java.util.ArrayList; import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class CDeclaration { private CSimpleType type; @@ -87,13 +85,20 @@ public CComplexType getActualType() { for (CStatement arrayDimension : arrayDimensions) { CSimpleType simpleType = type.copyOf(); simpleType.incrementPointer(); - actualType = new CArray(simpleType, actualType, actualType.getParseContext()); // some day change this back to arrays, when simple & complex types are better synchronized... + actualType = + new CArray( + simpleType, + actualType, + actualType.getParseContext(), + arrayDimension); // some day change this back to arrays, when simple & + // complex types are better synchronized... } -// for (int i = 0; i < derefCounter; i++) { -// CSimpleType simpleType = type.copyOf(); -// simpleType.incrementPointer(); -// actualType = new CPointer(simpleType, actualType, actualType.getParseContext()); -// } + // for (int i = 0; i < derefCounter; i++) { + // CSimpleType simpleType = type.copyOf(); + // simpleType.incrementPointer(); + // actualType = new CPointer(simpleType, actualType, + // actualType.getParseContext()); + // } return actualType; } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CArray.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CArray.java index a746a13545..806bfa9a7d 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CArray.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CArray.java @@ -13,10 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.frontend.transformation.model.types.complex.compound; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger; import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.clong.CUnsignedLong; @@ -25,10 +25,22 @@ public class CArray extends CInteger { private final CComplexType embeddedType; + private final CStatement arrayDimension; // if null, infinite + + public CArray( + CSimpleType origin, + CComplexType embeddedType, + ParseContext parseContext, + CStatement arrayDimension) { + super(origin, parseContext); + this.embeddedType = embeddedType; + this.arrayDimension = arrayDimension; + } public CArray(CSimpleType origin, CComplexType embeddedType, ParseContext parseContext) { super(origin, parseContext); this.embeddedType = embeddedType; + this.arrayDimension = null; } public CComplexType getEmbeddedType() { @@ -39,7 +51,6 @@ public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } - @Override public CInteger getSignedVersion() { return this; @@ -50,10 +61,12 @@ public CInteger getUnsignedVersion() { return this; } - @Override public String getTypeName() { return new CUnsignedLong(null, parseContext).getTypeName(); } + public CStatement getArrayDimension() { + return arrayDimension; + } } diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index c6c5b2868a..225ad1c51f 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -28,6 +28,8 @@ import hu.bme.mit.theta.core.stmt.MemoryAssignStmt import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.stmt.Stmts.Assume 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.abstracttype.AbstractExprs import hu.bme.mit.theta.core.type.abstracttype.AddExpr import hu.bme.mit.theta.core.type.abstracttype.DivExpr @@ -36,10 +38,13 @@ import hu.bme.mit.theta.core.type.abstracttype.SubExpr import hu.bme.mit.theta.core.type.anytype.Dereference import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr +import hu.bme.mit.theta.core.type.arraytype.ArrayType import hu.bme.mit.theta.core.type.booltype.BoolExprs import hu.bme.mit.theta.core.type.booltype.BoolExprs.* import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.type.bvtype.BvLitExpr +import hu.bme.mit.theta.core.type.inttype.IntExprs.Int import hu.bme.mit.theta.core.type.inttype.IntLitExpr import hu.bme.mit.theta.core.utils.BvUtils import hu.bme.mit.theta.core.utils.ExprUtils @@ -54,6 +59,7 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CAr import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CStruct import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory import hu.bme.mit.theta.xcfa.AssignStmtLabel import hu.bme.mit.theta.xcfa.model.* @@ -102,6 +108,30 @@ class FrontendXcfaBuilder( fun buildXcfa(cProgram: CProgram): XcfaBuilder { val builder = XcfaBuilder(cProgram.id ?: "") val initStmtList: MutableList = ArrayList() + if (MemsafetyPass.NEED_CHECK) { + val fitsall = Fitsall.getFitsall(parseContext) + val ptrType = CPointer(null, null, parseContext) + val ptrSize = + XcfaGlobalVar( + Var("__theta_ptr_size", ArrayType.of(ptrType.smtType, fitsall.smtType)), + ArrayLitExpr.of( + listOf(), + fitsall.nullValue as Expr, + ArrayType.of(ptrType.smtType as Type, fitsall.smtType as Type), + ), + ) + builder.addVar(ptrSize) + initStmtList.add( + AssignStmtLabel( + ptrSize.wrappedVar, + ArrayLitExpr.of( + listOf(), + fitsall.nullValue as Expr, + ArrayType.of(ptrType.smtType as Type, fitsall.smtType as Type), + ), + ) + ) + } for (globalDeclaration in cProgram.globalDeclarations) { val type = CComplexType.getType(globalDeclaration.get2().ref, parseContext) if (type is CVoid) { @@ -285,6 +315,17 @@ class FrontendXcfaBuilder( if (type is CArray && type.embeddedType is CArray) { // some day this is where initialization will occur. But this is not today. error("Not handling init expression of high dimsension array $flatVariable") + } else if (type is CArray) { + if (MemsafetyPass.NEED_CHECK) { + type.arrayDimension?.expression?.also { + if (it is LitExpr<*>) { + initStmtList.add(builder.parent.allocate(parseContext, flatVariable.ref, it)) + } else + throw UnsupportedFrontendElementException( + "Arrays for memory safety must be literal-sized, or mallocd." + ) + } + } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt index 8decd5d933..54f24c12cb 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt @@ -15,35 +15,23 @@ */ package hu.bme.mit.theta.xcfa.model -import hu.bme.mit.theta.core.decl.Decls.Var import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.Type -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr import hu.bme.mit.theta.core.type.arraytype.ArrayType import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr import hu.bme.mit.theta.core.type.inttype.IntType import hu.bme.mit.theta.frontend.ParseContext -import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall import hu.bme.mit.theta.xcfa.AssignStmtLabel -fun XcfaBuilder.getPtrSizeVar(type: CComplexType): VarDecl> = - getPtrSizeVar(type.smtType, type.nullValue as Expr) - -fun XcfaBuilder.getPtrSizeVar(intType: Type, nullValue: Expr): VarDecl> = - (getVars().find { it.wrappedVar.name == "__theta_ptr_size" }?.wrappedVar - ?: XcfaGlobalVar( - Var("__theta_ptr_size", ArrayType.of(intType, intType)), - ArrayLitExpr.of(listOf(), nullValue, ArrayType.of(intType, intType)), - ) - .also { addVar(it) } - .wrappedVar) +fun XcfaBuilder.getPtrSizeVar(): VarDecl> = + getVars().find { it.wrappedVar.name == "__theta_ptr_size" }!!.wrappedVar as VarDecl> fun XcfaBuilder.allocate(parseContext: ParseContext, base: Expr<*>, size: Expr<*>): StmtLabel { val type = Fitsall(null, parseContext) - val arr = getPtrSizeVar(type) + val arr = getPtrSizeVar() val baseCast = if (type.smtType is IntType) base else type.castTo(base) val sizeCast = if (type.smtType is IntType) size else type.castTo(size) val write = ArrayWriteExpr.create(arr.ref, baseCast, sizeCast) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt index a313f858e5..6216c38fd9 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -52,8 +52,6 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { var NEED_CHECK = false } - val variableUsedAsPtr = LinkedHashSet>() - override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { if (!NEED_CHECK) return builder @@ -73,7 +71,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { val errorLoc = builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } - val invalidFree = XcfaLocation("__THETA_bad-free", metadata = EmptyMetaData) + val invalidFree = XcfaLocation("__THETA_bad_free", metadata = EmptyMetaData) builder.addLoc(invalidFree) for (edge in ArrayList(builder.getEdges())) { val edges = edge.splitIf(this::free) @@ -85,7 +83,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { if (free((it.label as SequenceLabel).labels[0])) { val invokeLabel = it.label.labels[0] as InvokeLabel val argument = (invokeLabel.params[1] as RefExpr<*>).decl as VarDecl<*> - val sizeVar = builder.parent.getPtrSizeVar(fitsall) + val sizeVar = builder.parent.getPtrSizeVar() val derefAssume = Assume( Or( @@ -130,7 +128,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { private fun annotateDeref(builder: XcfaProcedureBuilder) { val errorLoc = builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } - val badDeref = XcfaLocation("__THETA_bad-deref", metadata = EmptyMetaData) + val badDeref = XcfaLocation("__THETA_bad_deref", metadata = EmptyMetaData) builder.addLoc(badDeref) for (edge in ArrayList(builder.getEdges())) { val edges = edge.splitIf(this::deref) @@ -148,7 +146,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { ), // uninit ptr Or( it.label.labels[0].dereferences.map { - val sizeVar = builder.parent.getPtrSizeVar(fitsall) + val sizeVar = builder.parent.getPtrSizeVar() Leq( ArrayReadExpr.create(sizeVar.ref, it.array), it.offset, @@ -190,7 +188,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { val lostLoc = XcfaLocation("__THETA_lost", metadata = EmptyMetaData) builder.addLoc(lostLoc) - val sizeVar = builder.parent.getPtrSizeVar(fitsall) + val sizeVar = builder.parent.getPtrSizeVar() val anyBase = builder.parent.getVars().find { it.wrappedVar.name == "__ptr" }?.wrappedVar ?: XcfaGlobalVar(Var("__ptr", sizeVar.type.indexType), pointerType.nullValue) From 913b15b58f20ff6372de7a6cf0a0ba89f7028629 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 20:50:50 +0100 Subject: [PATCH 06/22] Disabled non-linux bounded portfolio test --- .../src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt | 1 + 1 file changed, 1 insertion(+) diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt index 0d767337e5..1bd6dcf752 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt @@ -371,6 +371,7 @@ class XcfaCliVerifyTest { @ParameterizedTest @MethodSource("singleThreadedCFiles") fun testCVerifyBoundedPortfolio(filePath: String, extraArgs: String?) { + Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) val params = arrayOf( "--backend", From d8838cfc23a5f2cfaa94b7da0182c8f3c907bca0 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 20:56:20 +0100 Subject: [PATCH 07/22] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 19d6102585..d097203cde 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.8.3" + version = "6.8.4" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From bef071b6c563018988034fe90776b372648601e3 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 21:51:18 +0100 Subject: [PATCH 08/22] Sigkill after Sigterm in test --- .github/actions/benchexec-test/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml index 6456d4de30..2c71062f5d 100644 --- a/.github/actions/benchexec-test/action.yml +++ b/.github/actions/benchexec-test/action.yml @@ -65,7 +65,7 @@ runs: do echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'" echo "timeout $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true" - timeout $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true + timeout $timeout --kill-after 15 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true done - name: Upload results uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2 From 3747bc503268b2fc376e601284cd6d7274db7f64 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 22:26:16 +0100 Subject: [PATCH 09/22] fix syntax --- .github/actions/benchexec-test/action.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml index 2c71062f5d..7a41f95dfe 100644 --- a/.github/actions/benchexec-test/action.yml +++ b/.github/actions/benchexec-test/action.yml @@ -64,8 +64,8 @@ runs: for task in ${tasks[@]} do echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'" - echo "timeout $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true" - timeout $timeout --kill-after 15 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true + echo "timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true" + timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true done - name: Upload results uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2 From 572efa65d49adb3b99c221479efca07bd8aa4d61 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 12 Nov 2024 23:32:36 +0100 Subject: [PATCH 10/22] More resilient --- .github/actions/benchexec-report/action.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/actions/benchexec-report/action.yml b/.github/actions/benchexec-report/action.yml index d97886a2cb..4529e2a4e9 100644 --- a/.github/actions/benchexec-report/action.yml +++ b/.github/actions/benchexec-report/action.yml @@ -40,11 +40,11 @@ runs: all=0 for txt in *.txt do - new_correct=$(tail -n9 $txt | grep ' correct:' | awk ' { print $2 } ') + new_correct=$(tail -n9 $txt | grep ' correct:' | awk ' { print $2 } ' || echo 0) correct=$((correct + new_correct)) - new_incorrect=$(tail -n9 $txt | grep ' incorrect:' | awk ' { print $2 } ') + new_incorrect=$(tail -n9 $txt | grep ' incorrect:' | awk ' { print $2 } ' || echo 0) incorrect=$((incorrect + new_incorrect)) - new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ') + new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ' || echo 0) all=$((all + new_all)) echo "Found $new_correct correct and $new_incorrect incorrect results out of $new_all tasks in $txt" done From e6d7a38336bcbda78b125c5cea2e776f31d59f79 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 00:39:11 +0100 Subject: [PATCH 11/22] fix order --- .../bme/mit/theta/xcfa/passes/ReferenceElimination.kt | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index fc14f52ea6..8ce6c2f606 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -26,6 +26,7 @@ import hu.bme.mit.theta.core.type.anytype.Dereference import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference import hu.bme.mit.theta.core.type.anytype.RefExpr import hu.bme.mit.theta.core.type.anytype.Reference +import hu.bme.mit.theta.core.type.arraytype.ArrayType import hu.bme.mit.theta.core.utils.TypeUtils.cast import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType @@ -147,7 +148,15 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { val initEdges = builder.initLoc.outgoingEdges val newInitEdges = initEdges.map { - it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) + val labels = it.label.getFlatLabels() + val sizeInit = + labels.find { + it is StmtLabel && + it.stmt is AssignStmt<*> && + it.stmt.varDecl.let { it.name == "__theta_ptr_size" && it.type is ArrayType<*, *> } + } + val newLabelOrder = listOfNotNull(sizeInit) + initLabels + labels.filter { it != sizeInit } + it.withLabel(SequenceLabel(newLabelOrder, it.label.metadata)) } initEdges.forEach(builder::removeEdge) newInitEdges.forEach(builder::addEdge) From abb6d06bb75a0186b2aeb799838c50701f5d498a Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 16:42:05 +0100 Subject: [PATCH 12/22] Portfolio is now better --- .../main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt index 64fc73ff93..0f60431494 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt @@ -121,6 +121,9 @@ fun complexPortfolio25( ), argConfig = ArgConfig(disable = true), enableOutput = portfolioConfig.outputConfig.enableOutput, + acceptUnreliableSafe = portfolioConfig.outputConfig.acceptUnreliableSafe, + xcfaOutputConfig = XcfaOutputConfig(disable = true), + chcOutputConfig = ChcOutputConfig(disable = true), ), debugConfig = portfolioConfig.debugConfig, ) From 8840a7ecd8d928276281e228fd7610d7a0bc4888 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 16:52:02 +0100 Subject: [PATCH 13/22] Removing normal errors --- .../bme/mit/theta/xcfa/passes/MemsafetyPass.kt | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt index 6216c38fd9..8756768f95 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -55,6 +55,8 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { if (!NEED_CHECK) return builder + breakUpErrors(builder) + annotateFree(builder) annotateDeref(builder) @@ -67,6 +69,18 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { private val pointerType = CPointer(null, null, parseContext) val fitsall = Fitsall(null, parseContext) + private fun breakUpErrors(builder: XcfaProcedureBuilder) { + val errorLoc = + builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } + val finalLoc = + builder.finalLoc.orElseGet { builder.createFinalLoc().let { builder.finalLoc.get() } } + + LinkedHashSet(errorLoc.incomingEdges).forEach { + builder.removeEdge(it) + builder.addEdge(it.withTarget(finalLoc)) + } + } + private fun annotateFree(builder: XcfaProcedureBuilder) { val errorLoc = builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } @@ -196,7 +210,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { .wrappedVar val remained = Gt(ArrayReadExpr.create(sizeVar.ref, anyBase.ref), fitsall.nullValue) - for (incomingEdge in finalLoc.incomingEdges) { + for (incomingEdge in LinkedHashSet(finalLoc.incomingEdges)) { builder.removeEdge(incomingEdge) val newLoc = XcfaLocation("pre-final", metadata = EmptyMetaData) builder.addLoc(newLoc) From 02fb1b93a76216e079573e5c2892f099b5069a0c Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 18:31:44 +0100 Subject: [PATCH 14/22] Fixed optimizing locations and scoped arrays --- .../grammar/function/FunctionVisitor.java | 58 +++++++++++++++---- .../mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 16 +---- .../theta/xcfa/passes/EmptyEdgeRemovalPass.kt | 3 +- .../hu/bme/mit/theta/xcfa/passes/LbePass.kt | 1 + .../theta/xcfa/passes/ProcedurePassManager.kt | 2 +- 5 files changed, 52 insertions(+), 28 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index a8ca280557..93ed299903 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -50,6 +50,7 @@ import hu.bme.mit.theta.frontend.transformation.model.statements.*; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CVoid; +import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray; import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType; import hu.bme.mit.theta.frontend.transformation.model.types.simple.Struct; import java.util.*; @@ -72,13 +73,15 @@ public class FunctionVisitor extends CBaseVisitor { private final TypedefVisitor typedefVisitor; private final Logger uniqueWarningLogger; - private ParserRuleContext currentStatementContext = null; + private final LinkedList>> + currentStatementContext = new LinkedList<>(); public void clear() { variables.clear(); atomicVariables.clear(); flatVariables.clear(); functions.clear(); + currentStatementContext.clear(); } private final Deque>>> variables; @@ -184,8 +187,11 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) { } public void recordMetadata(ParserRuleContext ctx, CStatement statement) { - if (currentStatementContext != null) { - ctx = currentStatementContext; // this will overwrite the current ASt element's ctx + if (!currentStatementContext.isEmpty()) { + ctx = + currentStatementContext + .peek() + .get1(); // this will overwrite the current ASt element's ctx // with the statement's ctx } Token start = ctx.getStart(); @@ -300,10 +306,9 @@ public CStatement visitBlockItemList(CParser.BlockItemListContext ctx) { if (ctx.parent.parent.parent.parent instanceof CParser.BlockItemListContext) variables.push(Tuple2.of("anonymous" + anonCnt++, new LinkedHashMap<>())); for (CParser.BlockItemContext blockItemContext : ctx.blockItem()) { - final var save = currentStatementContext; - currentStatementContext = blockItemContext; + currentStatementContext.push(Tuple2.of(blockItemContext, Optional.of(compound))); compound.getcStatementList().add(blockItemContext.accept(this)); - currentStatementContext = save; + currentStatementContext.pop(); } if (ctx.parent.parent.parent.parent instanceof CParser.BlockItemListContext) variables.pop(); @@ -482,10 +487,9 @@ public CStatement visitReturnStatement(CParser.ReturnStatementContext ctx) { @Override public CStatement visitStatement(CParser.StatementContext ctx) { - final var save = currentStatementContext; - currentStatementContext = ctx; + currentStatementContext.push(Tuple2.of(ctx, Optional.empty())); final var ret = ctx.children.get(0).accept(this); - currentStatementContext = save; + currentStatementContext.pop(); return ret; } @@ -501,8 +505,41 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { compound.setPreStatements(preCompound); compound.setPostStatements(postCompound); for (CDeclaration declaration : declarations) { + createVars(declaration); + if (declaration.getActualType() + instanceof CArray cArray) { // we transform it into a malloc + final var malloc = + new CCall("malloc", List.of(cArray.getArrayDimension()), parseContext); + preCompound.getcStatementList().add(malloc); + final var free = + new CCall( + "free", + List.of(new CExpr(malloc.getRet().getRef(), parseContext)), + parseContext); + preCompound.getcStatementList().add(malloc); + CAssignment cAssignment = + new CAssignment( + declaration.getVarDecls().get(0).getRef(), + new CExpr(malloc.getRet().getRef(), parseContext), + "=", + parseContext); + recordMetadata(ctx, cAssignment); + compound.getcStatementList().add(cAssignment); + if (currentStatementContext.isEmpty()) { + throw new RuntimeException( + "Scope for variable " + declaration.getName() + " not found."); + } + final var scope = currentStatementContext.peek().get2(); + if (scope.isEmpty() || scope.get().getPostStatements() instanceof CCompound) { + throw new RuntimeException( + "Scope for variable " + declaration.getName() + " not found."); + } + if (scope.get().getPostStatements() == null) { + scope.get().setPostStatements(new CCompound(parseContext)); + } + ((CCompound) scope.get().getPostStatements()).getcStatementList().add(free); + } if (declaration.getInitExpr() != null) { - createVars(declaration); if (declaration.getType() instanceof Struct) { checkState( declaration.getInitExpr() instanceof CInitializerList, @@ -575,7 +612,6 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { } } } else { - createVars(declaration); // if there is no initializer, then we'll add an assumption regarding min and max // values if (declaration.getType() instanceof Struct) { diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 225ad1c51f..708f6a8d60 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -28,7 +28,6 @@ import hu.bme.mit.theta.core.stmt.MemoryAssignStmt import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.stmt.Stmts.Assume 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.abstracttype.AbstractExprs import hu.bme.mit.theta.core.type.abstracttype.AddExpr @@ -294,9 +293,7 @@ class FrontendXcfaBuilder( builder.setAtomic(flatVariable) } val type = CComplexType.getType(flatVariable.ref, parseContext) - if ( - (type is CArray || type is CStruct) && builder.getParams().none { it.first == flatVariable } - ) { + if ((type is CStruct) && builder.getParams().none { it.first == flatVariable }) { initStmtList.add( StmtLabel( Stmts.Assign( @@ -315,17 +312,6 @@ class FrontendXcfaBuilder( if (type is CArray && type.embeddedType is CArray) { // some day this is where initialization will occur. But this is not today. error("Not handling init expression of high dimsension array $flatVariable") - } else if (type is CArray) { - if (MemsafetyPass.NEED_CHECK) { - type.arrayDimension?.expression?.also { - if (it is LitExpr<*>) { - initStmtList.add(builder.parent.allocate(parseContext, flatVariable.ref, it)) - } else - throw UnsupportedFrontendElementException( - "Arrays for memory safety must be literal-sized, or mallocd." - ) - } - } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt index dd9adf3563..72a4ac29cd 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt @@ -33,7 +33,8 @@ class EmptyEdgeRemovalPass : ProcedurePass { !it.target.error && !it.target.final && !it.source.initial && - (it.source.outgoingEdges.size == 1 || it.target.incomingEdges.size == 1) + ((it.source.outgoingEdges.size == 1 && !it.source.name.contains("__THETA_")) || + (it.target.incomingEdges.size == 1) && !it.target.name.contains("__THETA_")) } ?: return builder val collapseBefore = edge.source.outgoingEdges.size == 1 builder.removeEdge(edge) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt index 40e24ad50a..36e724e5dc 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt @@ -273,6 +273,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { */ private fun removeMiddleLocation(location: XcfaLocation): Boolean { if (location.outgoingEdges.size != 1) return false + if (location.name.contains("__THETA_")) return false // these must remain in the trace val outEdge = location.outgoingEdges.first() if ( location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } || diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index 3b3cb24561..ff621131ac 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -70,7 +70,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL EmptyEdgeRemovalPass(), UnusedLocRemovalPass(), ), - listOf(FetchExecuteWriteback(parseContext)), + // listOf(FetchExecuteWriteback(parseContext)), ) class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : From b7946fffa296143bfe58b1bc4643781f88f588ee Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 18:38:09 +0100 Subject: [PATCH 15/22] Added better logging of subproperty --- .../hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 87f78612fe..a38dc6f7a5 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -33,8 +33,7 @@ import hu.bme.mit.theta.analysis.utils.TraceVisualizer import hu.bme.mit.theta.c2xcfa.CMetaData import hu.bme.mit.theta.cat.dsl.CatDslManager import hu.bme.mit.theta.common.logging.Logger -import hu.bme.mit.theta.common.logging.Logger.Level.INFO -import hu.bme.mit.theta.common.logging.Logger.Level.RESULT +import hu.bme.mit.theta.common.logging.Logger.Level.* import hu.bme.mit.theta.common.visualization.Graph import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger @@ -268,7 +267,17 @@ private fun backend( ?.locs ?.firstOrNull() ?.name - println(namedState) + val subproperty = + when (namedState) { + "__THETA_bad_free" -> "valid-free" + "__THETA_bad_deref" -> "valid-deref" + "__THETA_lost" -> "valid-memtrack" + else -> + throw RuntimeException( + "Something went wrong; could not determine subproperty! Named location: $namedState" + ) + } + logger.write(MAINSTEP, "(Subproperty %s)\n", subproperty) result } From 38ba862017509d09843783fcb31e62e6e94a3a7d Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 18:56:56 +0100 Subject: [PATCH 16/22] Determining property now --- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 59 +++++++++++-------- 1 file changed, 35 insertions(+), 24 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index a38dc6f7a5..1d3fefc4eb 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -253,35 +253,46 @@ private fun backend( else SafetyResult.unknown() } - result.isUnsafe && config.inputConfig.property == ErrorDetection.MEMSAFETY -> { + result.isUnsafe -> { // need to determine what kind - val trace = result.asUnsafe().cex as? Trace, XcfaAction> - val namedState = - trace - ?.states - ?.asReversed() - ?.getOrNull(1) - ?.processes - ?.values - ?.firstOrNull() - ?.locs - ?.firstOrNull() - ?.name - val subproperty = - when (namedState) { - "__THETA_bad_free" -> "valid-free" - "__THETA_bad_deref" -> "valid-deref" - "__THETA_lost" -> "valid-memtrack" - else -> - throw RuntimeException( - "Something went wrong; could not determine subproperty! Named location: $namedState" - ) + val property = + when (config.inputConfig.property) { + ErrorDetection.MEMSAFETY, + ErrorDetection.MEMCLEANUP -> { + val trace = result.asUnsafe().cex as? Trace, XcfaAction> + val namedState = + trace + ?.states + ?.asReversed() + ?.getOrNull(1) + ?.processes + ?.values + ?.firstOrNull() + ?.locs + ?.firstOrNull() + ?.name + when (namedState) { + "__THETA_bad_free" -> "valid-free" + "__THETA_bad_deref" -> "valid-deref" + "__THETA_lost" -> "valid-memtrack" + else -> + throw RuntimeException( + "Something went wrong; could not determine subproperty! Named location: $namedState" + ) + } + } + ErrorDetection.DATA_RACE -> "no-data-race" + ErrorDetection.ERROR_LOCATION -> "unreach-call" + ErrorDetection.OVERFLOW -> "no-overflow" + ErrorDetection.NO_ERROR -> null } - logger.write(MAINSTEP, "(Subproperty %s)\n", subproperty) + property?.also { logger.write(MAINSTEP, "(Property %s)\n", it) } result } - else -> result + else -> { + result + } } } From 8a95eef88a34a8cc126e368f9daf523b1a7a0e6e Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 19:21:08 +0100 Subject: [PATCH 17/22] fix memtrack --- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 43 ++++++++++--------- .../mit/theta/xcfa/passes/MemsafetyPass.kt | 14 +++--- 2 files changed, 29 insertions(+), 28 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 1d3fefc4eb..6631b0ca2c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -260,33 +260,34 @@ private fun backend( ErrorDetection.MEMSAFETY, ErrorDetection.MEMCLEANUP -> { val trace = result.asUnsafe().cex as? Trace, XcfaAction> - val namedState = - trace - ?.states - ?.asReversed() - ?.getOrNull(1) - ?.processes - ?.values - ?.firstOrNull() - ?.locs - ?.firstOrNull() - ?.name - when (namedState) { - "__THETA_bad_free" -> "valid-free" - "__THETA_bad_deref" -> "valid-deref" - "__THETA_lost" -> "valid-memtrack" - else -> - throw RuntimeException( - "Something went wrong; could not determine subproperty! Named location: $namedState" - ) - } + trace + ?.states + ?.asReversed() + ?.getOrNull(1) + ?.processes + ?.values + ?.firstOrNull() + ?.locs + ?.firstOrNull() + ?.name + ?.let { + when (it) { + "__THETA_bad_free" -> "valid-free" + "__THETA_bad_deref" -> "valid-deref" + "__THETA_lost" -> "valid-memtrack" + else -> + throw RuntimeException( + "Something went wrong; could not determine subproperty! Named location: $it" + ) + } + } } ErrorDetection.DATA_RACE -> "no-data-race" ErrorDetection.ERROR_LOCATION -> "unreach-call" ErrorDetection.OVERFLOW -> "no-overflow" ErrorDetection.NO_ERROR -> null } - property?.also { logger.write(MAINSTEP, "(Property %s)\n", it) } + property?.also { logger.write(RESULT, "(Property %s)\n", it) } result } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt index 8756768f95..923dd78c56 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -16,11 +16,9 @@ package hu.bme.mit.theta.xcfa.passes import hu.bme.mit.theta.core.decl.Decls.Var -import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.stmt.Stmts.Assume import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.* -import hu.bme.mit.theta.core.type.anytype.RefExpr import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr import hu.bme.mit.theta.core.type.booltype.BoolExprs.Or import hu.bme.mit.theta.frontend.ParseContext @@ -96,15 +94,15 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { edges.forEach { if (free((it.label as SequenceLabel).labels[0])) { val invokeLabel = it.label.labels[0] as InvokeLabel - val argument = (invokeLabel.params[1] as RefExpr<*>).decl as VarDecl<*> + val argument = invokeLabel.params[1] val sizeVar = builder.parent.getPtrSizeVar() val derefAssume = Assume( Or( - Leq(argument.ref, pointerType.nullValue), // uninit ptr + Leq(argument, pointerType.nullValue), // uninit ptr // freed/not big enough ptr Leq( - ArrayReadExpr.create(sizeVar.ref, argument.ref), + ArrayReadExpr.create(sizeVar.ref, argument), pointerType.nullValue, ), // freed/not big enough ptr ) @@ -115,7 +113,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { it.source, it.target, SequenceLabel( - listOf(builder.parent.allocate(parseContext, argument.ref, fitsall.nullValue)) + listOf(builder.parent.allocate(parseContext, argument, fitsall.nullValue)) ), it.metadata, ) @@ -197,6 +195,8 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { } fun annotateLost(builder: XcfaProcedureBuilder) { + val errorLoc = + builder.errorLoc.orElseGet { builder.createErrorLoc().let { builder.errorLoc.get() } } val finalLoc = builder.finalLoc.orElseGet { builder.createFinalLoc().let { builder.finalLoc.get() } } val lostLoc = XcfaLocation("__THETA_lost", metadata = EmptyMetaData) @@ -226,7 +226,7 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { builder.addEdge( XcfaEdge( lostLoc, - finalLoc, + errorLoc, label = SequenceLabel(listOf(NopLabel)), metadata = EmptyMetaData, ) From 3165862b7ae2fee32729164e20d9facd6908e404 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 19:48:43 +0100 Subject: [PATCH 18/22] Fix bug and better memtrack --- .../java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt | 6 +++++- .../bme/mit/theta/xcfa/passes/ReferenceElimination.kt | 10 +++++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt index 923dd78c56..f05bdbedd3 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -208,7 +208,11 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { ?: XcfaGlobalVar(Var("__ptr", sizeVar.type.indexType), pointerType.nullValue) .also { builder.parent.addVar(it) } .wrappedVar - val remained = Gt(ArrayReadExpr.create(sizeVar.ref, anyBase.ref), fitsall.nullValue) + val remained = // 3k+0: malloc + Gt( + ArrayReadExpr.create(sizeVar.ref, Mul(anyBase.ref, pointerType.getValue("3"))), + fitsall.nullValue, + ) for (incomingEdge in LinkedHashSet(finalLoc.incomingEdges)) { builder.removeEdge(incomingEdge) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index 8ce6c2f606..5fc074d697 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -69,7 +69,15 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { builder.parent.addVar(XcfaGlobalVar(varDecl, lit)) parseContext.metadata.create(varDecl.ref, "cType", ptrType) val assign = AssignStmtLabel(varDecl, lit) - Pair(varDecl, SequenceLabel(listOf(assign))) + val labels = + if (MemsafetyPass.NEED_CHECK) { + val assign2 = builder.parent.allocateUnit(parseContext, varDecl.ref) + + listOf(assign, assign2) + } else { + listOf(assign) + } + Pair(varDecl, SequenceLabel(labels)) } } checkState(globalReferredVars is Map<*, *>, "ReferenceElimination needs info on references") From 82efcc269ad88d3486693072a52141047b3ad8e8 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 20:51:16 +0100 Subject: [PATCH 19/22] Added comment on assumptions and dereferences --- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 19 ++++++++++++++----- .../mit/theta/xcfa/passes/MemsafetyPass.kt | 4 +++- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 6631b0ca2c..db963f6bf9 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -243,7 +243,7 @@ private fun backend( exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { checker.check() } - .let { result -> + .let ResultMapper@{ result -> when { result.isSafe && xcfa.unsafeUnrollUsed -> { // cannot report safe if force unroll was used @@ -263,18 +263,27 @@ private fun backend( trace ?.states ?.asReversed() - ?.getOrNull(1) + ?.firstOrNull { + it.processes.values.any { it.locs.any { it.name.contains("__THETA_") } } + } ?.processes ?.values - ?.firstOrNull() + ?.firstOrNull { it.locs.any { it.name.contains("__THETA_") } } ?.locs - ?.firstOrNull() + ?.firstOrNull { it.name.contains("__THETA_") } ?.name ?.let { when (it) { "__THETA_bad_free" -> "valid-free" "__THETA_bad_deref" -> "valid-deref" - "__THETA_lost" -> "valid-memtrack" + "__THETA_lost" -> + if (config.inputConfig.property == ErrorDetection.MEMCLEANUP) + "valid-memcleanup" + else + "valid-memtrack" + .also { // this is not an exact check. + return@ResultMapper SafetyResult.unknown() + } else -> throw RuntimeException( "Something went wrong; could not determine subproperty! Named location: $it" diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt index f05bdbedd3..e29faf60c8 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -149,7 +149,9 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass { ) { builder.removeEdge(edge) edges.forEach { - if (deref((it.label as SequenceLabel).labels[0])) { + if ( + deref((it.label as SequenceLabel).labels[0]) + ) { // if dereference is in a short-circuiting path, add prior assumptions as well. val derefAssume = Assume( Or( From 62dd36577344f48a0bb16a4af0379c4d22982eda Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 12:52:38 +0100 Subject: [PATCH 20/22] Fixed reference elimination when params are dereffd --- .../theta/xcfa/passes/ReferenceElimination.kt | 43 ++++++++++++++++--- 1 file changed, 37 insertions(+), 6 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index 5fc074d697..8fa9614f0b 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -127,11 +127,6 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { Pair(varDecl, SequenceLabel(labels)) } - if (builder.parent.getInitProcedures().any { it.first == builder }) { - addRefInitializations(builder, globalReferredVars) // we only need this for main - } - addRefInitializations(builder, referredVars) - val allReferredVars = referredVars + globalReferredVars if (allReferredVars.isNotEmpty()) { val edges = LinkedHashSet(builder.getEdges()) @@ -141,6 +136,11 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { edge.withLabel(edge.label.changeReferredVars(allReferredVars, parseContext)) ) } + if (builder.parent.getInitProcedures().any { it.first == builder }) { + addRefInitializations(builder, globalReferredVars) // we only need this for main + } + addRefInitializations(builder, referredVars) + return DeterministicPass().run(NormalizePass().run(builder)) } @@ -163,7 +163,38 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { it.stmt is AssignStmt<*> && it.stmt.varDecl.let { it.name == "__theta_ptr_size" && it.type is ArrayType<*, *> } } - val newLabelOrder = listOfNotNull(sizeInit) + initLabels + labels.filter { it != sizeInit } + val spInit = + labels.find { + it is StmtLabel && + it.stmt is AssignStmt<*> && + it.stmt.varDecl == builder.parent.ptrVar(parseContext) + } + val touchedParams = + builder.getParams().filter { + it.second != ParamDirection.OUT && referredVars.containsKey(it.first) + } + val paramMapping = + if (touchedParams.isNotEmpty()) { + touchedParams.map { + val type = referredVars[it.first]!!.first.type + StmtLabel( + MemoryAssignStmt.create( + Dereference( + cast(referredVars[it.first]!!.first.ref, type), + cast(CComplexType.getSignedLong(parseContext).nullValue, type), + it.first.type, + ), + it.first.ref, + ) + ) + } + } else listOf() + val newLabelOrder = + listOfNotNull(spInit) + + listOfNotNull(sizeInit) + + initLabels + + paramMapping + + labels.filter { it != sizeInit && it != spInit } it.withLabel(SequenceLabel(newLabelOrder, it.label.metadata)) } initEdges.forEach(builder::removeEdge) From 99427b5c765f1c5a3e269f5af92e5b44ad31794c Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 13:01:44 +0100 Subject: [PATCH 21/22] Handling unknowns better --- .../hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt index 193a062499..4022efe510 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt @@ -150,6 +150,9 @@ class InProcessChecker( if (stdoutRemainder.contains("SafetyResult Unsafe")) { safetyResult = SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance()) } + if (stdoutRemainder.contains("SafetyResult Unknown")) { + safetyResult = SafetyResult.unknown() + } val newLines = stdoutRemainder.split("\n") // if ends with \n, last element will be "" newLines.subList(0, newLines.size - 1).forEach { From b36d87f8c8d5d9ab98801499477bad9a1e51c84e Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 13:34:13 +0100 Subject: [PATCH 22/22] Instead of exception, only working when scope is found --- build.gradle.kts | 2 +- .../grammar/function/FunctionVisitor.java | 20 ++++++++----------- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index d097203cde..642c9fde76 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.8.4" + version = "6.8.5" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index 93ed299903..a8325f792f 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -525,19 +525,15 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { parseContext); recordMetadata(ctx, cAssignment); compound.getcStatementList().add(cAssignment); - if (currentStatementContext.isEmpty()) { - throw new RuntimeException( - "Scope for variable " + declaration.getName() + " not found."); - } - final var scope = currentStatementContext.peek().get2(); - if (scope.isEmpty() || scope.get().getPostStatements() instanceof CCompound) { - throw new RuntimeException( - "Scope for variable " + declaration.getName() + " not found."); - } - if (scope.get().getPostStatements() == null) { - scope.get().setPostStatements(new CCompound(parseContext)); + if (!currentStatementContext.isEmpty()) { + final var scope = currentStatementContext.peek().get2(); + if (scope.isPresent() && scope.get().getPostStatements() instanceof CCompound) { + if (scope.get().getPostStatements() == null) { + scope.get().setPostStatements(new CCompound(parseContext)); + } + ((CCompound) scope.get().getPostStatements()).getcStatementList().add(free); + } } - ((CCompound) scope.get().getPostStatements()).getcStatementList().add(free); } if (declaration.getInitExpr() != null) { if (declaration.getType() instanceof Struct) {