diff --git a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 index e6ea2c984e..e8cb557d48 100644 --- a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 +++ b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 @@ -31,7 +31,8 @@ grammar C; primaryExpression - : Identifier # primaryExpressionId + : '__PRETTY_FUNC__' # gccPrettyFunc + | Identifier # primaryExpressionId | Constant # primaryExpressionConstant | StringLiteral+ # primaryExpressionStrings | '(' expression ')' # primaryExpressionBraceExpression diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index d898745256..4fcd245c6a 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -627,6 +627,15 @@ public Expr visitPostfixExpressionBrackets(CParser.PostfixExpressionBracketsC return ctx.expression().accept(this); } + @Override + public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { + System.err.println("WARNING: gcc intrinsic encountered in place of an expression, using a literal 0 instead."); + CComplexType signedInt = CComplexType.getSignedInt(parseContext); + LitExpr zero = signedInt.getNullValue(); + parseContext.getMetadata().create(zero, "cType", signedInt); + return zero; + } + @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { return getVar(ctx.Identifier().getText()).getRef(); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java index c9ddba7eaf..3887001ff6 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java @@ -20,6 +20,9 @@ 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.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.booltype.BoolType; +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.compound.CArray; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CCompound; @@ -117,7 +120,7 @@ public CComplexType getSmallestCommonType(CComplexType type) { } public String getTypeName() { - throw new RuntimeException("Type name could not be queried from this type!"); + throw new RuntimeException("Type name could not be queried from this type: " + this); } public int width() { @@ -138,7 +141,20 @@ public static CComplexType getType(Expr expr, ParseContext parseContext) { return (CComplexType) cTypeOptional.get(); } else if (cTypeOptional.isPresent() && cTypeOptional.get() instanceof CSimpleType) { return ((CSimpleType) cTypeOptional.get()).getActualType(); - } else throw new RuntimeException("Type not known for expression: " + expr); + } else { + return getType(expr.getType(), parseContext); +// throw new RuntimeException("Type not known for expression: " + expr); + } + } + + private static CComplexType getType(Type type, ParseContext parseContext) { + if (type instanceof IntType) { + return new CSignedInt(null, parseContext); + } else if (type instanceof ArrayType aType) { + return new CArray(null, getType(aType.getElemType(), parseContext), parseContext); + } else if (type instanceof BoolType) { + return new CBool(null, parseContext); + } else throw new RuntimeException("Not yet implemented for type: " + type); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java index 9b28e816f3..1d9e69f09f 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java @@ -28,4 +28,9 @@ public CVoid(CSimpleType origin, ParseContext parseContext) { public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + + @Override + public String getTypeName() { + return "void"; + } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CDouble.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CDouble.java index ab3693376f..08187a9f15 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CDouble.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CDouble.java @@ -31,4 +31,9 @@ public CDouble(CSimpleType origin, ParseContext parseContext) { public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + + @Override + public String getTypeName() { + return "double"; + } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CFloat.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CFloat.java index b71acbf65e..58612af384 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CFloat.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CFloat.java @@ -31,4 +31,9 @@ public CFloat(CSimpleType origin, ParseContext parseContext) { public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + + @Override + public String getTypeName() { + return "float"; + } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CLongDouble.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CLongDouble.java index ed12111dbe..963beb80a6 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CLongDouble.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CLongDouble.java @@ -31,4 +31,9 @@ public CLongDouble(CSimpleType origin, ParseContext parseContext) { public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + + @Override + public String getTypeName() { + return "long double"; + } } diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java index 6721326fff..0bd2d0d290 100644 --- a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java +++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcBackwardXcfaBuilder.java @@ -26,21 +26,41 @@ import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.xcfa.model.*; -import hu.bme.mit.theta.xcfa.passes.ChcPasses; +import hu.bme.mit.theta.xcfa.model.EmptyMetaData; +import hu.bme.mit.theta.xcfa.model.InvokeLabel; +import hu.bme.mit.theta.xcfa.model.ParamDirection; +import hu.bme.mit.theta.xcfa.model.SequenceLabel; +import hu.bme.mit.theta.xcfa.model.StmtLabel; +import hu.bme.mit.theta.xcfa.model.XcfaBuilder; +import hu.bme.mit.theta.xcfa.model.XcfaEdge; +import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder; +import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager; import kotlin.Pair; import org.antlr.v4.runtime.RuleContext; -import java.util.*; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.frontend.chc.ChcUtils.*; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.createVars; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.getTailConditionLabels; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformConst; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformSort; public class ChcBackwardXcfaBuilder extends CHCBaseVisitor implements ChcXcfaBuilder { private final Map procedures = new HashMap<>(); + private final ProcedurePassManager procedurePassManager; private XcfaBuilder xcfaBuilder; private int callCount = 0; + public ChcBackwardXcfaBuilder(final ProcedurePassManager procedurePassManager) { + this.procedurePassManager = procedurePassManager; + } + @Override public XcfaBuilder buildXcfa(CHCParser parser) { xcfaBuilder = new XcfaBuilder("chc"); @@ -123,7 +143,7 @@ private XcfaLocation createLocation(XcfaProcedureBuilder builder) { } private XcfaProcedureBuilder createProcedure(String procName) { - XcfaProcedureBuilder builder = new XcfaProcedureBuilder(procName, new ChcPasses()); + XcfaProcedureBuilder builder = new XcfaProcedureBuilder(procName, procedurePassManager); builder.setName(procName); builder.addParam(Decls.Var(procName + "_ret", Bool()), ParamDirection.OUT); diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java index ffd2119d62..71b06b1aa7 100644 --- a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java +++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcForwardXcfaBuilder.java @@ -22,27 +22,41 @@ import hu.bme.mit.theta.core.stmt.AssignStmt; import hu.bme.mit.theta.core.stmt.HavocStmt; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.xcfa.model.*; -import hu.bme.mit.theta.xcfa.passes.ChcPasses; +import hu.bme.mit.theta.xcfa.model.EmptyMetaData; +import hu.bme.mit.theta.xcfa.model.SequenceLabel; +import hu.bme.mit.theta.xcfa.model.StmtLabel; +import hu.bme.mit.theta.xcfa.model.XcfaBuilder; +import hu.bme.mit.theta.xcfa.model.XcfaEdge; +import hu.bme.mit.theta.xcfa.model.XcfaLabel; +import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder; +import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager; import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.frontend.chc.ChcUtils.*; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.createVars; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.getTailConditionLabels; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformConst; +import static hu.bme.mit.theta.frontend.chc.ChcUtils.transformSort; public class ChcForwardXcfaBuilder extends CHCBaseVisitor implements ChcXcfaBuilder { + private final ProcedurePassManager procedurePassManager; private XcfaProcedureBuilder builder; private XcfaLocation initLocation; private XcfaLocation errorLocation; private final Map locations = new HashMap<>(); + public ChcForwardXcfaBuilder(final ProcedurePassManager procedurePassManager) { + this.procedurePassManager = procedurePassManager; + } + @Override public XcfaBuilder buildXcfa(CHCParser parser) { XcfaBuilder xcfaBuilder = new XcfaBuilder("chc"); - builder = new XcfaProcedureBuilder("main", new ChcPasses()); + builder = new XcfaProcedureBuilder("main", procedurePassManager); builder.createInitLoc(); builder.createErrorLoc(); builder.createFinalLoc(); diff --git a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java index afbfbf24c5..58e992a895 100644 --- a/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java +++ b/subprojects/frontends/chc-frontend/src/main/java/hu/bme/mit/theta/frontend/chc/ChcFrontend.java @@ -18,6 +18,8 @@ import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCLexer; import hu.bme.mit.theta.chc.frontend.dsl.gen.CHCParser; import hu.bme.mit.theta.xcfa.model.XcfaBuilder; +import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager; +import org.antlr.v4.runtime.BailErrorStrategy; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CommonTokenStream; @@ -35,12 +37,13 @@ public ChcFrontend(ChcTransformation transformation) { chcTransformation = transformation; } - public XcfaBuilder buildXcfa(CharStream charStream) { + public XcfaBuilder buildXcfa(CharStream charStream, ProcedurePassManager procedurePassManager) { ChcUtils.init(charStream); CHCParser parser = new CHCParser(new CommonTokenStream(new CHCLexer(charStream))); + parser.setErrorHandler(new BailErrorStrategy()); ChcXcfaBuilder chcXcfaBuilder = switch (chcTransformation) { - case FORWARD -> new ChcForwardXcfaBuilder(); - case BACKWARD -> new ChcBackwardXcfaBuilder(); + case FORWARD -> new ChcForwardXcfaBuilder(procedurePassManager); + case BACKWARD -> new ChcBackwardXcfaBuilder(procedurePassManager); default -> throw new RuntimeException("Should not be here; adapt PORTFOLIO to FW/BW beforehand."); }; 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 119ec83fe9..5ef76b82ea 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 @@ -51,8 +51,10 @@ import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.toDot +import hu.bme.mit.theta.xcfa.passes.ChcPasses import hu.bme.mit.theta.xcfa.passes.LbePass import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass +import hu.bme.mit.theta.xcfa.toC import org.antlr.v4.runtime.CharStreams import java.io.File import java.io.FileInputStream @@ -142,6 +144,15 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--cex-solver"], description = "Concretizer solver name") var concretizerSolver: String = "Z3" + @Parameter(names = ["--to-c-use-arrays"]) + var useArr: Boolean = false + + @Parameter(names = ["--to-c-use-exact-arrays"]) + var useExArr: Boolean = false + + @Parameter(names = ["--to-c-use-ranges"]) + var useRange: Boolean = false + @Parameter(names = ["--validate-cex-solver"], description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") var validateConcretizerSolver: Boolean = false @@ -198,7 +209,7 @@ class XcfaCli(private val args: Array) { stopwatch.elapsed(TimeUnit.MILLISECONDS) } ms)\n") - preVerificationLogging(logger, xcfa, gsonForOutput) + preVerificationLogging(logger, xcfa, gsonForOutput, parseContext) if (noAnalysis) { logger.write(Logger.Level.RESULT, "ParsingResult Success") @@ -284,7 +295,8 @@ class XcfaCli(private val args: Array) { } } - private fun preVerificationLogging(logger: ConsoleLogger, xcfa: XCFA, gsonForOutput: Gson) { + private fun preVerificationLogging(logger: ConsoleLogger, xcfa: XCFA, gsonForOutput: Gson, + parseContext: ParseContext) { if (outputResults && !svcomp) { resultFolder.mkdirs() @@ -294,6 +306,9 @@ class XcfaCli(private val args: Array) { val xcfaDotFile = File(resultFolder, "xcfa.dot") xcfaDotFile.writeText(xcfa.toDot()) + val xcfaCFile = File(resultFolder, "xcfa.c") + xcfaCFile.writeText(xcfa.toC(parseContext, useArr, useExArr, useRange)) + val xcfaJsonFile = File(resultFolder, "xcfa.json") val uglyJson = gsonForOutput.toJson(xcfa) val create = GsonBuilder().setPrettyPrinting().create() @@ -331,7 +346,7 @@ class XcfaCli(private val args: Array) { try { when (inputType) { InputType.CHC -> { - parseChc(logger) + parseChc(logger, parseContext) } InputType.C -> { @@ -362,20 +377,20 @@ class XcfaCli(private val args: Array) { exitProcess(ExitCodes.FRONTEND_FAILED.code) } - private fun parseChc(logger: ConsoleLogger): XCFA { + private fun parseChc(logger: ConsoleLogger, parseContext: ParseContext): XCFA { var chcFrontend: ChcFrontend val xcfaBuilder = if (chcTransformation == ChcFrontend.ChcTransformation.PORTFOLIO) { // try forward, fallback to backward chcFrontend = ChcFrontend(ChcFrontend.ChcTransformation.FORWARD) try { - chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!))) + chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)), ChcPasses(parseContext)) } catch (e: UnsupportedOperationException) { logger.write(Logger.Level.INFO, "Non-linear CHC found, retrying using backward transformation...") chcFrontend = ChcFrontend(ChcFrontend.ChcTransformation.BACKWARD) - chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!))) + chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)), ChcPasses(parseContext)) } } else { chcFrontend = ChcFrontend(chcTransformation) - chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!))) + chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)), ChcPasses(parseContext)) } return xcfaBuilder.build() } diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt new file mode 100644 index 0000000000..47518b1742 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaToCTest.kt @@ -0,0 +1,65 @@ +/* + * 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.frontend.ParseContext +import hu.bme.mit.theta.frontend.chc.ChcFrontend +import hu.bme.mit.theta.frontend.chc.ChcFrontend.ChcTransformation +import hu.bme.mit.theta.xcfa.passes.ChcPasses +import hu.bme.mit.theta.xcfa.toC +import org.antlr.v4.runtime.CharStreams +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.Arguments +import org.junit.jupiter.params.provider.MethodSource +import java.io.FileInputStream +import java.util.* +import java.util.stream.Stream +import kotlin.io.path.createTempDirectory + +class XcfaToCTest { + companion object { + + @JvmStatic + fun chcFiles(): Stream { + return Stream.of( + Arguments.of("/chc/chc-LIA-Lin-Arrays_000.smt2", ChcFrontend.ChcTransformation.FORWARD), + Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.BACKWARD), + ) + } + + @JvmStatic + fun dslFiles(): Stream { + return Stream.of( + Arguments.of("/dsl/async.xcfa.kts"), + Arguments.of("/dsl/sync.xcfa.kts"), + ) + } + } + + + @ParameterizedTest + @MethodSource("chcFiles") + fun testRoundTrip(filePath: String, chcTransformation: ChcTransformation) { + val chcFrontend = ChcFrontend(chcTransformation) + val xcfa = chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(javaClass.getResource(filePath)!!.path)), ChcPasses( + ParseContext())).build() + val temp = createTempDirectory() + val file = temp.resolve("${filePath.split("/").last()}.c").also { it.toFile().writeText(xcfa.toC(ParseContext(), + useArr, useExArr, useRange))} + System.err.println(file) + } + +} diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt new file mode 100644 index 0000000000..610e7978c0 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt @@ -0,0 +1,355 @@ +/* + * 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 + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.AssignStmt +import hu.bme.mit.theta.core.stmt.AssumeStmt +import hu.bme.mit.theta.core.stmt.HavocStmt +import hu.bme.mit.theta.core.type.* +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Leq +import hu.bme.mit.theta.core.type.abstracttype.DivExpr +import hu.bme.mit.theta.core.type.abstracttype.EqExpr +import hu.bme.mit.theta.core.type.abstracttype.ModExpr +import hu.bme.mit.theta.core.type.abstracttype.NeqExpr +import hu.bme.mit.theta.core.type.anytype.IteExpr +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.arraytype.ArrayType +import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr +import hu.bme.mit.theta.core.type.booltype.* +import hu.bme.mit.theta.core.type.booltype.BoolExprs.Or +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr +import hu.bme.mit.theta.core.type.fptype.FpLitExpr +import hu.bme.mit.theta.core.type.fptype.FpRoundingMode +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.type.rattype.RatLitExpr +import hu.bme.mit.theta.core.utils.BvUtils +import hu.bme.mit.theta.core.utils.FpUtils +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.CComplexType.CComplexTypeVisitor +import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cbool.CBool +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cchar.CChar +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CSignedInt +import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CUnsignedInt +import hu.bme.mit.theta.xcfa.model.* + +private const val arraySize = 10; + +fun XCFA.toC(parseContext: ParseContext, arraySupport: Boolean, exactArraySupport: Boolean, intRangeConstraint: Boolean): String = """ + extern void abort(); + extern int __VERIFIER_nondet_int(); + extern _Bool __VERIFIER_nondet__Bool(); + extern void reach_error(); + + ${if(procedures.any { it.vars.any { it.type is ArrayType<*, *> } } ) if(arraySupport) if(exactArraySupport) """ + // "exact" array support + typedef long unsigned int size_t; + + void * __attribute__((__cdecl__)) malloc (size_t __size) ; + void __attribute__((__cdecl__)) free (void *) ; + + + typedef struct + { + int *arr; + int size; + int def; + } int_arr; + + int_arr array_write(int_arr arr, int idx, int val) { + int_arr ret; + ret.size = arr.size > idx + 1 ? arr.size : idx + 1; + ret.arr = malloc(ret.size * sizeof(int)); + ret.def = arr.def; + for(int i = 0; i < ret.size; ++i) { + ret.arr[i] = i < arr.size ? arr.arr[i] : ret.def; + } + ret.arr[idx] = val; + return ret; + } + + int array_read(int_arr arr, int idx) { + return idx < arr.size ? arr.arr[idx] : arr.def; + } + + int array_equals(int_arr arr1, int_arr arr2) { + int i = 0; + if(arr1.def != arr2.def) return 0; + for(; i < arr1.size; i++) { + if(arr1.arr[i] != (i < arr2.size ? arr2.arr[i] : arr2.def)) return 0; + } + for(; i < arr2.size; i++) { + if(arr2.arr[i] != arr1.def) return 0; + } + + return 1; + } + """.trimIndent() else """ + // non-exact array support + + typedef struct + { + int arr[$arraySize]; + } int_arr; + + int_arr array_write(int_arr arr, int idx, int val) { + arr.arr[idx] = val; + return arr; + } + + int array_read(int_arr arr, int idx) { + return arr.arr[idx]; + } + + int array_equals(int_arr arr1, int_arr arr2) { + for(int i = 0; i < $arraySize; i++) { + if(arr1.arr[i] != arr2.arr[i]) return 0; + } + return 1; + } + """.trimIndent() else error("Array support not enabled") else ""} + + ${procedures.joinToString("\n\n") { it.decl(parseContext) + ";" }} + + ${procedures.joinToString("\n\n") { it.def(parseContext, intRangeConstraint) }} + + ${ if(initProcedures.size != 1) error("Exactly one initial procedure is supported.") else + { + val proc = initProcedures[0] + val procName = proc.first.name.toC() + if (procName != "main") + "int main() { $procName(${proc.second.joinToString(", ") { it.toC(parseContext) } }); }" + else "" + } + } + +""".trimIndent() + + +fun XcfaProcedure.decl(parseContext: ParseContext): String = + if (params.isNotEmpty()) { + "${CComplexType.getType(params[0].first.ref, parseContext).toC()} ${name.toC()}(${ + params.subList(1, params.size).joinToString(", ") { it.decl(parseContext) } + })" + } else { + "void ${name.toC()}()" + } + +private fun VarDecl<*>.unsafeBounds(parseContext: ParseContext) = + CComplexType.getType(ref, parseContext).accept(object: CComplexTypeVisitor?>() { + override fun visit(type: CInteger, param: Unit): Expr? { + return Or(Leq(ref, Int(-1_000_000_000)), Geq(ref, Int(1_000_000_000))) + } + + override fun visit(type: CBool?, param: Unit?): Expr? { + return null + } + }, Unit) + +private fun Set>.unsafeBounds(parseContext: ParseContext, intRangeConstraint: Boolean): String { + if(!intRangeConstraint) return "" + + val conditions = this.map { (it.unsafeBounds(parseContext))?.toC(parseContext) }.filterNotNull() + return if (conditions.isNotEmpty()) + "if (" + conditions.joinToString(" || ") + ") abort();" + else + "" +} + +fun XcfaProcedure.def(parseContext: ParseContext, intRangeConstraint: Boolean): String = """ + ${decl(parseContext)} { + // return parameter + ${if(params.isNotEmpty()) params[0].decl(parseContext) + ";" else ""} + + // variables + ${(vars - params.map { it.first }.toSet()).joinToString("\n") { it.decl(parseContext) + ";" }} + + ${vars.unsafeBounds(parseContext, intRangeConstraint)} + + // main logic + goto ${initLoc.name.toC()}; + + ${locs.joinToString("\n") { + """ + ${it.name.toC()}: + ${it.toC(parseContext, intRangeConstraint)} + """.trimIndent() + } + } + + // return expression + ${if (params.isNotEmpty()) "return " + params[0].first.name.toC() + ";" else ""} + } +""".trimIndent() + +private fun XcfaLocation.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = + if(this.error) { + "reach_error();" + } else when (outgoingEdges.size) { + 0 -> "goto ${name.toC()};" + 1 -> outgoingEdges.first().getFlatLabels().joinToString("\n") + { it.toC(parseContext, intRangeConstraint) } + " goto ${outgoingEdges.first().target.name.toC()};" + + 2 -> + """ + switch(__VERIFIER_nondet__Bool()) { + ${outgoingEdges.mapIndexed { index, xcfaEdge -> + "case $index: \n" + + xcfaEdge.getFlatLabels().joinToString("\n", postfix="\n") { it.toC(parseContext, intRangeConstraint) } + + "goto ${xcfaEdge.target.name.toC()};\n" + }.joinToString("\n") + } + default: abort(); + } + """.trimIndent() + + else -> + """ + switch(__VERIFIER_nondet_int()) { + ${outgoingEdges.mapIndexed { index, xcfaEdge -> + "case $index: \n" + + xcfaEdge.getFlatLabels().joinToString("\n", postfix="\n") { it.toC(parseContext, intRangeConstraint) } + + "goto ${xcfaEdge.target.name.toC()};\n" + }.joinToString("\n") + } + default: abort(); + } + """.trimIndent() + } + +private fun XcfaLabel.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = + when(this) { + is StmtLabel -> this.toC(parseContext, intRangeConstraint) + is SequenceLabel -> labels.joinToString("\n") { it.toC(parseContext, intRangeConstraint) } + is InvokeLabel -> "${params[0].toC(parseContext)} = ${name.toC()}(${params.subList(1, params.size).map { it.toC(parseContext) }.joinToString(", ")});" + else -> TODO("Not yet supported: $this") + } + +private fun StmtLabel.toC(parseContext: ParseContext, intRangeConstraint: Boolean): String = + when(stmt) { + is HavocStmt<*> -> "${stmt.varDecl.name.toC()} = __VERIFIER_nondet_${CComplexType.getType(stmt.varDecl.ref, parseContext).toC()}(); ${setOf(stmt.varDecl).unsafeBounds(parseContext, intRangeConstraint)}" + is AssignStmt<*> -> "${stmt.varDecl.name.toC()} = ${stmt.expr.toC(parseContext)};" + is AssumeStmt -> "if(!${stmt.cond.toC(parseContext)}) abort();" + else -> TODO("Not yet supported: $stmt") + } + +fun Pair, ParamDirection>.decl(parseContext: ParseContext): String = +// if(second == ParamDirection.IN) { + first.decl(parseContext) +// } else error("Only IN params are supported right now") + +fun VarDecl<*>.decl(parseContext: ParseContext): String = + "${CComplexType.getType(ref, parseContext).toC()} ${name.toC()}" + +private fun CComplexType.toC(): String = + when(this) { + is CArray -> "${this.embeddedType.toC()}_arr" + is CSignedInt -> "int" + is CUnsignedInt -> "unsigned int" + is CChar -> "char" + is CBool -> "_Bool" + else -> this.typeName + } + +// below functions implement the serialization of expressions to C-style expressions +fun Expr<*>.toC(parseContext: ParseContext) = + when(this) { + is NullaryExpr<*> -> this.toC(parseContext) + is UnaryExpr<*, *> -> this.toC(parseContext) + is BinaryExpr<*, *> -> this.toC(parseContext) + is MultiaryExpr<*, *> -> this.toC(parseContext) + is ArrayWriteExpr<*, *> -> this.toC(parseContext) + is ArrayReadExpr<*, *> -> this.toC(parseContext) + is IteExpr<*> -> this.toC(parseContext) + else -> TODO("Not yet supported: $this") + } + +fun ArrayWriteExpr<*, *>.toC(parseContext: ParseContext): String = + "array_write(${this.array.toC(parseContext)}, ${this.index.toC(parseContext)}, ${this.elem.toC(parseContext)})" + +fun ArrayReadExpr<*, *>.toC(parseContext: ParseContext): String = + "array_read(${this.array.toC(parseContext)}, ${this.index.toC(parseContext)})" + +fun IteExpr<*>.toC(parseContext: ParseContext): String = + "(${this.cond.toC(parseContext)} ? ${this.then.toC(parseContext)} : ${this.`else`.toC(parseContext)})" + +// nullary: ref + lit +fun NullaryExpr<*>.toC(parseContext: ParseContext): String = + when(this) { + is RefExpr<*> -> this.decl.name.toC() + is LitExpr<*> -> (this as LitExpr<*>).toC(parseContext) + else -> TODO("Not yet supported: $this") + } + +fun LitExpr<*>.toC(parseContext: ParseContext): String = + when(this) { + is FalseExpr -> "0" + is TrueExpr -> "1" + is IntLitExpr -> this.value.toString() + is RatLitExpr -> "(${this.num}.0/${this.denom}.0)" + is FpLitExpr -> FpUtils.fpLitExprToBigFloat(FpRoundingMode.RNE, this).toString() + is BvLitExpr -> BvUtils.neutralBvLitExprToBigInteger(this).toString() + else -> error("Not supported: $this") + } + + +fun UnaryExpr<*, *>.toC(parseContext: ParseContext): String = + "(${this.cOperator()} ${op.toC(parseContext)})" + +fun BinaryExpr<*, *>.toC(parseContext: ParseContext): String = + if(leftOp.type is ArrayType<*, *>) { + "${this.arrayCOperator()}(${leftOp.toC(parseContext)}, ${rightOp.toC(parseContext)})" + } else if(this is ModExpr<*>) { + "( (${leftOp.toC(parseContext)} % ${rightOp.toC(parseContext)} + ${rightOp.toC(parseContext)}) % ${rightOp.toC(parseContext)} )" + } else { + "(${leftOp.toC(parseContext)} ${this.cOperator()} ${rightOp.toC(parseContext)})" + } + +fun MultiaryExpr<*, *>.toC(parseContext: ParseContext): String = + ops.joinToString(separator = " ${this.cOperator()} ", prefix = "(", postfix = ")") { it.toC(parseContext) } + +fun Expr<*>.cOperator() = + when(this) { + is EqExpr<*> -> "==" + is NeqExpr<*> -> "!=" + is OrExpr -> "||" + is AndExpr -> "&&" + is NotExpr -> "!" + // is ModExpr<*> -> "%" // handled above + is DivExpr<*> -> "/" + + is UnaryExpr<*, *> -> operatorLabel + is BinaryExpr<*, *> -> operatorLabel + is MultiaryExpr<*, *> -> operatorLabel + else -> TODO("Not yet implemented operator label for expr: $this") + } + +fun Expr<*>.arrayCOperator() = + when(this) { + is EqExpr<*> -> "array_equals" + is NeqExpr<*> -> "!array_equals" + else -> TODO("Not yet implemented array operator label for expr: $this") + } + +fun String.toC() = + this.replace(Regex("[^A-Za-z_0-9]"), "_") \ No newline at end of file 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 50017bf05d..0c49556c13 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 @@ -76,18 +76,18 @@ class ChcPasses : ProcedurePassManager(/*listOf( // SvCompIntrinsicsPass(), // FpFunctionsToExprsPass(), // PthreadFunctionsPass(), - // trying to inline procedures - InlineProceduresPass(), - RemoveDeadEnds(), - EliminateSelfLoops(), - // handling remaining function calls + // trying to inline procedures + InlineProceduresPass(parseContext), + RemoveDeadEnds(parseContext), + EliminateSelfLoops(parseContext), + // handling remaining function calls // NondetFunctionPass(), - LbePass(), - NormalizePass(), // needed after lbe, TODO - DeterministicPass(), // needed after lbe, TODO + LbePass(parseContext), + NormalizePass(parseContext), // needed after lbe, TODO + DeterministicPass(parseContext), // needed after lbe, TODO // HavocPromotionAndRange(), - // Final cleanup - UnusedVarPass(), -)*/) + // Final cleanup + UnusedVarPass(parseContext), +)) class LitmusPasses : ProcedurePassManager() \ No newline at end of file