Skip to content

Commit

Permalink
Added code from CHC2C implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi committed Nov 2, 2023
1 parent 7fd3216 commit 5e0e9de
Show file tree
Hide file tree
Showing 14 changed files with 552 additions and 34 deletions.
3 changes: 2 additions & 1 deletion subprojects/frontends/c-frontend/src/main/antlr/C.g4
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,8 @@ grammar C;


primaryExpression
: Identifier # primaryExpressionId
: '__PRETTY_FUNC__' # gccPrettyFunc
| Identifier # primaryExpressionId
| Constant # primaryExpressionConstant
| StringLiteral+ # primaryExpressionStrings
| '(' expression ')' # primaryExpressionBraceExpression
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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() {
Expand All @@ -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);
}


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,4 +28,9 @@ public CVoid(CSimpleType origin, ParseContext parseContext) {
public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
return visitor.visit(this, param);
}

@Override
public String getTypeName() {
return "void";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,9 @@ public CDouble(CSimpleType origin, ParseContext parseContext) {
public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
return visitor.visit(this, param);
}

@Override
public String getTypeName() {
return "double";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,9 @@ public CFloat(CSimpleType origin, ParseContext parseContext) {
public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
return visitor.visit(this, param);
}

@Override
public String getTypeName() {
return "float";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,9 @@ public CLongDouble(CSimpleType origin, ParseContext parseContext) {
public <T, R> R accept(CComplexTypeVisitor<T, R> visitor, T param) {
return visitor.visit(this, param);
}

@Override
public String getTypeName() {
return "long double";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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<Object> implements ChcXcfaBuilder {
private final Map<String, XcfaProcedureBuilder> 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");
Expand Down Expand Up @@ -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);

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<Object> implements ChcXcfaBuilder {
private final ProcedurePassManager procedurePassManager;
private XcfaProcedureBuilder builder;
private XcfaLocation initLocation;
private XcfaLocation errorLocation;
private final Map<String, UPred> 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();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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.");
};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -142,6 +144,15 @@ class XcfaCli(private val args: Array<String>) {
@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
Expand Down Expand Up @@ -198,7 +209,7 @@ class XcfaCli(private val args: Array<String>) {
stopwatch.elapsed(TimeUnit.MILLISECONDS)
} ms)\n")

preVerificationLogging(logger, xcfa, gsonForOutput)
preVerificationLogging(logger, xcfa, gsonForOutput, parseContext)

if (noAnalysis) {
logger.write(Logger.Level.RESULT, "ParsingResult Success")
Expand Down Expand Up @@ -284,7 +295,8 @@ class XcfaCli(private val args: Array<String>) {
}
}

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()

Expand All @@ -294,6 +306,9 @@ class XcfaCli(private val args: Array<String>) {
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()
Expand Down Expand Up @@ -331,7 +346,7 @@ class XcfaCli(private val args: Array<String>) {
try {
when (inputType) {
InputType.CHC -> {
parseChc(logger)
parseChc(logger, parseContext)
}

InputType.C -> {
Expand Down Expand Up @@ -362,20 +377,20 @@ class XcfaCli(private val args: Array<String>) {
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()
}
Expand Down
Original file line number Diff line number Diff line change
@@ -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<Arguments> {
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<Arguments> {
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)
}

}
Loading

0 comments on commit 5e0e9de

Please sign in to comment.