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 diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml index 6456d4de30..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 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 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 a8ca280557..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 @@ -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,37 @@ 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()) { + 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); + } + } + } if (declaration.getInitExpr() != null) { - createVars(declaration); if (declaration.getType() instanceof Struct) { checkState( declaration.getInitExpr() instanceof CInitializerList, @@ -575,7 +608,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/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 d573eae8d0..1f4e49b62f 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,25 +21,35 @@ 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.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 +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 +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 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 @@ -48,10 +58,12 @@ 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.* 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 @@ -95,6 +107,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) { @@ -122,6 +158,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 && @@ -249,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( @@ -321,6 +363,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), @@ -1060,3 +1109,12 @@ class FrontendXcfaBuilder( } } } + +private fun Expr<*>.hasArithmetic(): Boolean = + when (this) { + is AddExpr -> true + is SubExpr -> true + is DivExpr -> true + is MulExpr -> true + else -> ops.any { it.hasArithmetic() } + } 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..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 @@ -204,6 +204,8 @@ enum class ErrorDetection { ERROR_LOCATION, DATA_RACE, OVERFLOW, + MEMSAFETY, + MEMCLEANUP, NO_ERROR, } @@ -211,6 +213,8 @@ fun getXcfaErrorPredicate( errorDetection: ErrorDetection ): Predicate>> = when (errorDetection) { + ErrorDetection.MEMSAFETY, + ErrorDetection.MEMCLEANUP, ErrorDetection.ERROR_LOCATION -> Predicate>> { s -> s.processes.any { it.value.locs.peek().error } 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..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 @@ -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 @@ -56,10 +55,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 +96,12 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq XcfaSporLts.random = random XcfaDporLts.random = random } + if ( + config.inputConfig.property == ErrorDetection.MEMSAFETY || + config.inputConfig.property == ErrorDetection.MEMCLEANUP + ) { + MemsafetyPass.NEED_CHECK = true + } if (config.debugConfig.argToFile) { WebDebuggerLogger.enableWebDebuggerLogger() WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) @@ -241,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 @@ -251,7 +253,56 @@ private fun backend( else SafetyResult.unknown() } - else -> result + result.isUnsafe -> { + // need to determine what kind + val property = + when (config.inputConfig.property) { + ErrorDetection.MEMSAFETY, + ErrorDetection.MEMCLEANUP -> { + val trace = result.asUnsafe().cex as? Trace, XcfaAction> + trace + ?.states + ?.asReversed() + ?.firstOrNull { + it.processes.values.any { it.locs.any { it.name.contains("__THETA_") } } + } + ?.processes + ?.values + ?.firstOrNull { it.locs.any { it.name.contains("__THETA_") } } + ?.locs + ?.firstOrNull { it.name.contains("__THETA_") } + ?.name + ?.let { + when (it) { + "__THETA_bad_free" -> "valid-free" + "__THETA_bad_deref" -> "valid-deref" + "__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" + ) + } + } + } + ErrorDetection.DATA_RACE -> "no-data-race" + ErrorDetection.ERROR_LOCATION -> "unreach-call" + ErrorDetection.OVERFLOW -> "no-overflow" + ErrorDetection.NO_ERROR -> null + } + property?.also { logger.write(RESULT, "(Property %s)\n", it) } + result + } + + else -> { + result + } } } 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 { 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 53cce44448..03cff34e47 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.passes.* import java.nio.file.Paths @@ -119,6 +120,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, ) @@ -224,6 +228,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-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", 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..54f24c12cb --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/PtrSize.kt @@ -0,0 +1,44 @@ +/* + * 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.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.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.integer.Fitsall +import hu.bme.mit.theta.xcfa.AssignStmtLabel + +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() + 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/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/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..e29faf60c8 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt @@ -0,0 +1,250 @@ +/* + * 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.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.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 + } + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + if (!NEED_CHECK) return builder + + breakUpErrors(builder) + + annotateFree(builder) + + annotateDeref(builder) + + annotateLost(builder) + + return builder + } + + 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() } } + + 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] + val sizeVar = builder.parent.getPtrSizeVar() + val derefAssume = + Assume( + Or( + Leq(argument, pointerType.nullValue), // uninit ptr + // freed/not big enough ptr + Leq( + ArrayReadExpr.create(sizeVar.ref, argument), + pointerType.nullValue, + ), // freed/not big enough ptr + ) + ) + + builder.addEdge( + XcfaEdge( + it.source, + it.target, + SequenceLabel( + listOf(builder.parent.allocate(parseContext, argument, 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]) + ) { // if dereference is in a short-circuiting path, add prior assumptions as well. + 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() + 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 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) + builder.addLoc(lostLoc) + + val sizeVar = builder.parent.getPtrSizeVar() + 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 = // 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) + 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, + errorLoc, + 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 0e624b12d3..ac8a7e4650 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), @@ -69,7 +70,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL EmptyEdgeRemovalPass(), UnusedLocRemovalPass(), ), - listOf(FetchExecuteWriteback(parseContext)), + // listOf(FetchExecuteWriteback(parseContext)), ) class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : 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..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 @@ -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 @@ -68,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") @@ -107,13 +116,16 @@ 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) - if (builder.parent.getInitProcedures().any { it.first == builder }) { - addRefInitializations(builder, globalReferredVars) // we only need this for main - } - addRefInitializations(builder, referredVars) + listOf(assign1, assign2, assign3) + } else { + listOf(assign1, assign2) + } + Pair(varDecl, SequenceLabel(labels)) + } val allReferredVars = referredVars + globalReferredVars if (allReferredVars.isNotEmpty()) { @@ -124,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)) } @@ -139,7 +156,46 @@ 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 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) newInitEdges.forEach(builder::addEdge)