From 113f27446a7d5f11c9f15bcb26ceadf05f300800 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 12 Nov 2023 17:50:47 +0100 Subject: [PATCH] Added witness test, fixed witness printing --- .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 13 ++- .../mit/theta/xcfa/cli/XcfaCegarServer.java | 16 ++- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 8 +- .../theta/xcfa/cli/utils/XcfaWitnessWriter.kt | 10 +- .../xcfa/cli/witnesses/TraceToWitness.kt | 4 +- .../mit/theta/xcfa/cli/XcfaCliWitnessTest.kt | 99 +++++++++++++++++++ .../c/litmustest/singlethread/witness_test.c | 9 ++ 7 files changed, 141 insertions(+), 18 deletions(-) create mode 100644 subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt create mode 100644 subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/witness_test.c diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt index d7d17452d1..bb16d46173 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt @@ -42,7 +42,9 @@ import hu.bme.mit.theta.core.decl.Decl import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.solver.SolverFactory -import hu.bme.mit.theta.xcfa.analysis.* +import hu.bme.mit.theta.xcfa.analysis.ErrorDetection +import hu.bme.mit.theta.xcfa.analysis.XcfaAction +import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.model.XCFA import java.io.BufferedReader @@ -52,6 +54,7 @@ import java.io.PrintWriter import java.net.Socket import java.nio.ByteBuffer import java.util.concurrent.TimeUnit +import java.util.zip.GZIPOutputStream import kotlin.system.exitProcess @@ -221,15 +224,15 @@ data class XcfaCegarConfig( val pb = NuProcessBuilder(listOf( getJavaExecutable(), "-cp", - File( - XcfaCegarServer::class.java.protectionDomain.codeSource.location.toURI()).absolutePath, + File(XcfaCegarServer::class.java.protectionDomain.codeSource.location.toURI()).absolutePath, XcfaCegarServer::class.qualifiedName, "--smt-home", smtHome, "--return-safety-result", "" + !writeWitness, "--input", - sourceFileName + sourceFileName, + "--gzip" )) val processHandler = ProcessHandler(logger) pb.setProcessListener(processHandler) @@ -256,7 +259,7 @@ data class XcfaCegarConfig( val gson = getGson(xcfa, { domain }, { getSolver(abstractionSolver, validateAbstractionSolver).createSolver() }) clientSocket.use { - val writer = PrintWriter(clientSocket.getOutputStream(), true) + val writer = PrintWriter(GZIPOutputStream(clientSocket.getOutputStream()), true) val reader = BufferedReader(InputStreamReader(clientSocket.getInputStream())) writer.println(gson.toJson(this)) writer.println(gson.toJson(xcfa)) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java index 013657aadd..c24d3138cc 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java @@ -36,10 +36,13 @@ import java.io.FileNotFoundException; import java.io.FileWriter; import java.io.IOException; +import java.io.InputStream; import java.io.InputStreamReader; import java.io.PrintWriter; import java.net.ServerSocket; import java.net.Socket; +import java.nio.file.FileSystems; +import java.util.zip.GZIPInputStream; import static hu.bme.mit.theta.xcfa.cli.ExitCodesKt.exitOnError; import static hu.bme.mit.theta.xcfa.cli.GsonUtilsKt.getGson; @@ -73,6 +76,9 @@ class XcfaCegarServer { @Parameter(names = "--debug", description = "Debug mode (will not create a socket)") Boolean debug = false; + @Parameter(names = "--gzip", description = "Expect stdin to contain gzipped text") + Boolean gzip = false; + private void run(String[] args) { try { JCommander.newBuilder().addObject(this).build().parse(args); @@ -93,7 +99,11 @@ private void run(String[] args) { do { try (final Socket clientSocket = debug ? null : socket.accept()) { final PrintWriter out = new PrintWriter(debug ? System.out : clientSocket.getOutputStream(), true); - final BufferedReader in = new BufferedReader(new InputStreamReader(debug ? System.in : clientSocket.getInputStream())); + InputStream stream = debug ? System.in : clientSocket.getInputStream(); + if (gzip) { + stream = new GZIPInputStream(stream); + } + final BufferedReader in = new BufferedReader(new InputStreamReader(stream)); final String configStr = this.configStr == null ? in.readLine() : this.configStr; final String xcfaStr = this.xcfaStr == null ? in.readLine() : this.xcfaStr; @@ -146,7 +156,9 @@ private void run(String[] args) { String s = gson.toJson(check); out.println(s); } else { - new XcfaWitnessWriter().writeWitness(check, new File(inputFileName), getSolver(xcfaCegarConfig.getRefinementSolver(), xcfaCegarConfig.getValidateRefinementSolver()), parseContext); + var workdir = FileSystems.getDefault().getPath("").toAbsolutePath(); + var witnessfile = new File(workdir.toString() + File.separator + "witness.graphml"); + new XcfaWitnessWriter().writeWitness(check, new File(inputFileName), getSolver(xcfaCegarConfig.getRefinementSolver(), xcfaCegarConfig.getValidateRefinementSolver()), parseContext, witnessfile); } logger.write(Logger.Level.INFO, "Server exiting.\n"); } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index 88972a3264..af20be3108 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -60,6 +60,7 @@ import org.antlr.v4.runtime.CharStreams import java.io.File import java.io.FileInputStream import java.io.FileReader +import java.nio.file.FileSystems import java.util.* import java.util.concurrent.TimeUnit import javax.script.Bindings @@ -340,10 +341,15 @@ class XcfaCli(private val args: Array) { val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) } + val witnessFile = File(resultFolder, "witness.graphml") + XcfaWitnessWriter().writeWitness(safetyResult, input!!, + getSolver(concretizerSolver, validateConcretizerSolver), parseContext, witnessFile) } else { + val workdir = FileSystems.getDefault().getPath("").toAbsolutePath() + val witnessfile = File(workdir.toString() + File.separator + "witness.graphml") XcfaWitnessWriter().writeWitness(safetyResult, input!!, - getSolver(concretizerSolver, validateConcretizerSolver), parseContext) + getSolver(concretizerSolver, validateConcretizerSolver), parseContext, witnessfile) } } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt index 14dff34e99..748f86a0fa 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt @@ -29,8 +29,6 @@ import java.io.BufferedWriter import java.io.File import java.io.FileWriter import java.io.IOException -import java.nio.file.FileSystems -import java.nio.file.Path import java.text.DateFormat import java.text.SimpleDateFormat import java.util.* @@ -41,11 +39,10 @@ class XcfaWitnessWriter { safetyResult: SafetyResult<*, *>, inputFile: File, cexSolverFactory: SolverFactory, - parseContext: ParseContext + parseContext: ParseContext, + witnessfile: File, ) { if (safetyResult.isUnsafe) { - val workdir: Path = FileSystems.getDefault().getPath("").toAbsolutePath() - val witnessfile = File(workdir.toString() + File.separator + "witness.graphml") val concrTrace: Trace, XcfaAction> = XcfaTraceConcretizer.concretize( safetyResult.asUnsafe().trace as Trace, XcfaAction>?, cexSolverFactory) @@ -54,9 +51,6 @@ class XcfaWitnessWriter { val xml = witness.toPrettyXml() witnessfile.writeText(xml) } else if (safetyResult.isSafe) { - val workdir = FileSystems.getDefault().getPath("").toAbsolutePath() - val witnessfile = File(workdir.toString() + File.separator + "witness.graphml") - val taskHash = WitnessWriter.createTaskHash(inputFile.absolutePath) val dummyWitness = StringBuilder() dummyWitness.append( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt index 4cf9867c72..9284a39bd0 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt @@ -140,8 +140,8 @@ private fun labelToEdge(lastNode: WitnessNode, node: WitnessNode, xcfaLabel: Xcf startline = xcfaLabel.getCMetaData()?.lineNumberStart, endline = xcfaLabel.getCMetaData()?.lineNumberStop, - startoffset = xcfaLabel.getCMetaData()?.lineNumberStart, - endoffset = xcfaLabel.getCMetaData()?.lineNumberStart, + startoffset = xcfaLabel.getCMetaData()?.offsetStart, + endoffset = xcfaLabel.getCMetaData()?.offsetEnd, threadId = if (pid != null) "$pid" else null, diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt new file mode 100644 index 0000000000..b9c57c1a1a --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt @@ -0,0 +1,99 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xcfa.cli + +import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main +import org.junit.jupiter.api.Assertions +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.Arguments +import org.junit.jupiter.params.provider.MethodSource +import java.util.stream.Stream +import kotlin.io.path.absolutePathString +import kotlin.io.path.createTempDirectory +import kotlin.io.path.exists + +data class WitnessEdge( + val startlineRange: Pair?, + val endlineRange: Pair?, + val startoffsetRange: Pair?, + val endoffsetRange: Pair?, + val assumption: Regex?, + ) + +class XcfaCliWitnessTest { + companion object { + + @JvmStatic + fun cFiles(): Stream { + return Stream.of( + Arguments.of("/c/litmustest/singlethread/witness_test.c", listOf( + WitnessEdge( + startlineRange = Pair(5, 5), + endlineRange = Pair(5, 5), + startoffsetRange = Pair(79, 91), + endoffsetRange = Pair(110, 115), + assumption = Regex("i *== *-1"), + ), + )), + ) + } + + } + + @ParameterizedTest + @MethodSource("cFiles") + fun testCWitness(filePath: String, expectedWitnessEdges: List) { + val temp = createTempDirectory() + val params = arrayOf( + "--input-type", "C", + "--input", javaClass.getResource(filePath)!!.path, + "--stacktrace", + "--output-results", + "--output-directory", temp.absolutePathString(), + "--debug", + ) + main(params) + Assertions.assertTrue(temp.resolve("witness.graphml").exists()) + val witnessContents = temp.resolve("witness.graphml").toFile().readText() + val edges = mutableListOf>() + val edgeMatcher = Regex("(?s)(.*)") + val data = mutableMapOf() + for(dataMatch in dataMatcher.findAll(match.value)) { + val (key, value) = dataMatch.destructured + data.put(key, value) + } + edges.add(data) + } + for (expectedWitnessEdge in expectedWitnessEdges) { + Assertions.assertFalse( + edges.none { edge -> + val startline = expectedWitnessEdge.startlineRange?.let {edge["startline"]?.let{v -> Pair(it, Integer.parseInt(v)) } }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val endline = expectedWitnessEdge.endlineRange?.let {edge["endline"]?.let{v -> Pair(it, Integer.parseInt(v)) } }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val startoffset = expectedWitnessEdge.startoffsetRange?.let {edge["startoffset"]?.let{v -> Pair(it, Integer.parseInt(v)) } }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val endoffset = expectedWitnessEdge.endoffsetRange?.let {edge["endoffset"]?.let{v -> Pair(it, Integer.parseInt(v)) } }?.let { it.first.first <= it.second && it.second <= it.first.second } ?: false + val assumption = expectedWitnessEdge.assumption?.let {edge["assumption"]?.let{v -> Pair(it, v) } }?.let { it.first.matches(it.second) } ?: false + startline && endline && startoffset && endoffset && assumption + }, + "Expected witness edge not found: $expectedWitnessEdge" + ) + } + temp.toFile().deleteRecursively() + } + + +} diff --git a/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/witness_test.c b/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/witness_test.c new file mode 100644 index 0000000000..83276a8106 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/witness_test.c @@ -0,0 +1,9 @@ +extern void reach_error(); +extern int __VERIFIER_nondet_int(void); + +int main() { + int i = __VERIFIER_nondet_int(); + + if(i + 1 == 0) reach_error(); + +} \ No newline at end of file