Skip to content

Commit

Permalink
Added better logging, and complex portfolio
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Nov 12, 2023
1 parent 217f2f1 commit 4585748
Show file tree
Hide file tree
Showing 13 changed files with 347 additions and 47 deletions.
271 changes: 271 additions & 0 deletions scripts/complex.kts
View file

Large diffs are not rendered by default.

0 scripts/portfolio.kts → scripts/simple.kts
View file
File renamed without changes.
8 changes: 4 additions & 4 deletions ...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -469,7 +469,7 @@ public Expr<?> visitCastExpressionCast(CParser.CastExpressionCastContext ctx) {
@Override
public Expr<?> visitUnaryExpressionSizeOrAlignOf(CParser.UnaryExpressionSizeOrAlignOfContext ctx) {
if (ctx.Alignof() != null) {
uniqueWarningLogger.write(Level.INFO, "WARNING: alignof is not yet implemented, using a literal 0 instead.");
uniqueWarningLogger.write(Level.INFO, "WARNING: alignof is not yet implemented, using a literal 0 instead.\n");
CComplexType signedInt = CComplexType.getSignedInt(parseContext);
LitExpr<?> zero = signedInt.getNullValue();
parseContext.getMetadata().create(zero, "cType", signedInt);
Expand All @@ -480,7 +480,7 @@ public Expr<?> visitUnaryExpressionSizeOrAlignOf(CParser.UnaryExpressionSizeOrAl
LitExpr<?> value = CComplexType.getSignedInt(parseContext).getValue("" + parseContext.getArchitecture().getBitWidth(type.get().getTypeName()) / 8);
return value;
} else {
uniqueWarningLogger.write(Level.INFO, "WARNING: sizeof got unknown type, using a literal 0 instead.");
uniqueWarningLogger.write(Level.INFO, "WARNING: sizeof got unknown type, using a literal 0 instead.\n");
CComplexType signedInt = CComplexType.getSignedInt(parseContext);
LitExpr<?> zero = signedInt.getNullValue();
parseContext.getMetadata().create(zero, "cType", signedInt);
Expand Down Expand Up @@ -652,7 +652,7 @@ public Expr<?> visitPostfixExpressionBrackets(CParser.PostfixExpressionBracketsC

@Override
public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
uniqueWarningLogger.write(Level.INFO, "WARNING: gcc intrinsic encountered in place of an expression, using a literal 0 instead.");
uniqueWarningLogger.write(Level.INFO, "WARNING: gcc intrinsic encountered in place of an expression, using a literal 0 instead.\n");
CComplexType signedInt = CComplexType.getSignedInt(parseContext);
LitExpr<?> zero = signedInt.getNullValue();
parseContext.getMetadata().create(zero, "cType", signedInt);
Expand Down Expand Up @@ -755,7 +755,7 @@ public Expr<?> visitPrimaryExpressionGccExtension(CParser.PrimaryExpressionGccEx
public Expr<?> visitPrimaryExpressionStrings(CParser.PrimaryExpressionStringsContext ctx) {
CComplexType signedInt = CComplexType.getSignedInt(parseContext);
Expr<?> ret = signedInt.getUnitValue();
uniqueWarningLogger.write(Level.INFO, "Warning: using int(1) as a string constant");
uniqueWarningLogger.write(Level.INFO, "WARNING: using int(1) as a string constant\n");
parseContext.getMetadata().create(ret, "cType", signedInt);
return ret;
}
Expand Down
2 changes: 1 addition & 1 deletion .../main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ private void createVars(String name, CDeclaration declaration, CComplexType type
Tuple2<String, Map<String, VarDecl<?>>> peek = variables.peek();
VarDecl<?> varDecl = Var(getName(name), type.getSmtType());
if (peek.get2().containsKey(name)) {
uniqueWarningLogger.write(Level.INFO, "WARNING: Variable already exists: " + name);
uniqueWarningLogger.write(Level.INFO, "WARNING: Variable already exists: " + name + "\n");
varDecl = peek.get2().get(name);
}
peek.get2().put(name, varDecl);
Expand Down
2 changes: 1 addition & 1 deletion ...c/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ public CDeclaration visitDirectDeclaratorFunctionDecl(
CParser.DirectDeclaratorFunctionDeclContext ctx) {
CDeclaration decl = ctx.directDeclarator().accept(this);
if (!(ctx.parameterTypeList() == null || ctx.parameterTypeList().ellipses == null)) {
uniqueWarningLogger.write(Level.INFO, "WARNING: variable args are not supported!");
uniqueWarningLogger.write(Level.INFO, "WARNING: variable args are not supported!\n");
decl.setFunc(true);
return decl;
}
Expand Down
6 changes: 3 additions & 3 deletions ...tend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ private CSimpleType mergeCTypes(List<CSimpleType> cSimpleTypes) {
List<CSimpleType> enums = cSimpleTypes.stream().filter(cType -> cType instanceof Enum)
.collect(Collectors.toList());
if (enums.size() > 0) {
uniqueWarningLogger.write(Level.INFO, "WARNING: enums are not yet supported! Using int instead.");
uniqueWarningLogger.write(Level.INFO, "WARNING: enums are not yet supported! Using int instead.\n");
cSimpleTypes.add(NamedType("int", parseContext, uniqueWarningLogger));
cSimpleTypes.removeAll(enums);
}
Expand All @@ -106,7 +106,7 @@ private CSimpleType mergeCTypes(List<CSimpleType> cSimpleTypes) {
if (type.isSigned() == null) {
if (type instanceof NamedType && ((NamedType) type).getNamedType().contains("char")) {
uniqueWarningLogger.write(Level.INFO,
"WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char.");
"WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char.\n");
}
type.setSigned(true);
}
Expand Down Expand Up @@ -213,7 +213,7 @@ public CSimpleType visitCompoundDefinition(CParser.CompoundDefinitionContext ctx
}
return struct;
} else {
uniqueWarningLogger.write(Level.INFO, "Warning: CompoundDefinitions are not yet implemented!");
uniqueWarningLogger.write(Level.INFO, "WARNING: CompoundDefinitions are not yet implemented!\n");
return NamedType("int", parseContext, uniqueWarningLogger);
}
}
Expand Down
2 changes: 1 addition & 1 deletion .../src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ public CComplexType getActualType() {
type = new CVoid(this, parseContext);
break;
default: {
uniqueWarningLogger.write(Level.INFO, "WARNING: Unknown simple type " + namedType);
uniqueWarningLogger.write(Level.INFO, "WARNING: Unknown simple type " + namedType + "\n");
type = new CVoid(this, parseContext);
break;
}
Expand Down
2 changes: 1 addition & 1 deletion ...end/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ public void addField(String name, CSimpleType type) {
@Override
public CComplexType getActualType() {
if (currentlyBeingBuilt) {
uniqueWarningLogger.write(Level.INFO, "WARNING: self-embedded structs! Using long as a placeholder");
uniqueWarningLogger.write(Level.INFO, "WARNING: self-embedded structs! Using long as a placeholder\n");
return CComplexType.getSignedInt(parseContext);
}
currentlyBeingBuilt = true;
Expand Down
14 changes: 1 addition & 13 deletions subprojects/xcfa/xcfa-cli/build.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,22 +36,10 @@ dependencies {
implementation(project(":theta-grammar"))
implementation(project(":theta-llvm2xcfa"))
implementation("com.zaxxer:nuprocess:2.0.5")
runtimeOnly("org.jetbrains.kotlin:kotlin-scripting-jsr223:1.7.10")
implementation("org.jetbrains.kotlin:kotlin-scripting-jsr223:${Versions.kotlin}")
}

application {
mainClassName = "hu.bme.mit.theta.xcfa.cli.XcfaCli"
}

//tasks.test {
// if (OperatingSystem.current().isLinux) {
// val nativeLibTasks = project(":theta-llvm").tasks
// dependsOn(nativeLibTasks.build)
//
// val linkTask = nativeLibTasks.withType(LinkSharedLibrary::class).first()
// val existingLibraryPath = systemProperties["java.library.path"]
// val newLibraryPath = "${existingLibraryPath}:${linkTask.linkedFile.get().asFile.parent}"
// systemProperty("java.library.path", newLibraryPath)
// }
//}

17 changes: 12 additions & 5 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
package hu.bme.mit.theta.xcfa.cli

import com.beust.jcommander.Parameter
import com.google.common.base.Stopwatch
import com.google.gson.reflect.TypeToken
import com.zaxxer.nuprocess.NuAbstractProcessHandler
import com.zaxxer.nuprocess.NuProcess
Expand Down Expand Up @@ -259,11 +260,17 @@ data class XcfaCegarConfig(
val gson = getGson(xcfa, { domain },
{ getSolver(abstractionSolver, validateAbstractionSolver).createSolver() })
clientSocket.use {
val writer = PrintWriter(GZIPOutputStream(clientSocket.getOutputStream()), true)
val reader = BufferedReader(InputStreamReader(clientSocket.getInputStream()))
writer.println(gson.toJson(this))
writer.println(gson.toJson(xcfa))
writer.println(gson.toJson(parseContext))
run {
val writer = PrintWriter(GZIPOutputStream(clientSocket.getOutputStream(), 65536, true), true)
val sw = Stopwatch.createStarted()
writer.println(gson.toJson(this))
writer.println(gson.toJson(xcfa))
writer.println(gson.toJson(parseContext))
logger.write(Logger.Level.RESULT,
"Serialized Config, XCFA and ParseContext in ${sw.elapsed(TimeUnit.MILLISECONDS)}ms\n")
writer.close()
}
val retCode = process.waitFor(timeoutMs, TimeUnit.MILLISECONDS)
if (retCode == Int.MIN_VALUE) {
if (!processHandler.writingSafetyResult) {
Expand Down Expand Up @@ -330,7 +337,7 @@ private class ProcessHandler(
}
}
stdoutBuffer += str
val matchResults = Regex("([a-zA-Z]*)\t\\{([^}]*)}").findAll(stdoutBuffer)
val matchResults = Regex("(?s)([a-zA-Z]*)\t\\{([^}]*)}").findAll(stdoutBuffer)
var length = 0
for (matchResult in matchResults) {
val (level, message) = matchResult.destructured
Expand Down
21 changes: 18 additions & 3 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,14 @@
import com.beust.jcommander.JCommander;
import com.beust.jcommander.Parameter;
import com.beust.jcommander.ParameterException;
import com.google.common.base.Stopwatch;
import com.google.gson.Gson;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
import hu.bme.mit.theta.analysis.expr.ExprAction;
import hu.bme.mit.theta.analysis.expr.ExprState;
import hu.bme.mit.theta.common.logging.ConsoleLabelledLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.Logger.Level;
import hu.bme.mit.theta.frontend.ParseContext;
import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter;
Expand All @@ -42,6 +44,7 @@
import java.net.ServerSocket;
import java.net.Socket;
import java.nio.file.FileSystems;
import java.util.concurrent.TimeUnit;
import java.util.zip.GZIPInputStream;

import static hu.bme.mit.theta.xcfa.cli.ExitCodesKt.exitOnError;
Expand Down Expand Up @@ -90,24 +93,33 @@ private void run(String[] args) {
}

final Logger logger = new ConsoleLabelledLogger();
logger.write(Logger.Level.INFO, "Server started on port " + port + ".\n");

exitOnError(false, debug, () -> {
exitOnError(true, debug, () -> {
SolverRegistrationKt.registerAllSolverManagers(solverHome, logger);
try (final ServerSocket socket = new ServerSocket(port)) {
logger.write(Logger.Level.INFO, "Server started on port " + socket.getLocalPort() + ".\n");
System.out.println("Port=(" + socket.getLocalPort() + ")");
do {
try (final Socket clientSocket = debug ? null : socket.accept()) {
final PrintWriter out = new PrintWriter(debug ? System.out : clientSocket.getOutputStream(), true);
InputStream stream = debug ? System.in : clientSocket.getInputStream();
if (gzip) {
stream = new GZIPInputStream(stream);
stream = new GZIPInputStream(stream, 65536);
logger.write(Level.INFO, "Using GZIP compression\n");
}
final BufferedReader in = new BufferedReader(new InputStreamReader(stream));

final Stopwatch sw = Stopwatch.createStarted();

final String configStr = this.configStr == null ? in.readLine() : this.configStr;
logger.write(Level.INFO, "Read config in " + sw.elapsed(TimeUnit.MILLISECONDS) + "ms\n");
sw.reset().start();
final String xcfaStr = this.xcfaStr == null ? in.readLine() : this.xcfaStr;
logger.write(Level.INFO, "Read XCFA in " + sw.elapsed(TimeUnit.MILLISECONDS) + "ms\n");
sw.reset().start();
final String parseStr = this.parseContext == null ? in.readLine() : this.parseContext;
logger.write(Level.INFO, "Read ParseContext in " + sw.elapsed(TimeUnit.MILLISECONDS) + "ms\n");
sw.reset().start();
final Gson gson = getGson();

XCFA xcfa;
Expand Down Expand Up @@ -150,6 +162,9 @@ private void run(String[] args) {

logger.write(Logger.Level.INFO, "Parsed parsecontext.\n");

logger.write(Level.INFO, "Parsed config, XCFA and ParseContext in " + sw.elapsed(TimeUnit.MILLISECONDS) + "ms\n");
sw.reset();

SafetyResult<ExprState, ExprAction> check = xcfaCegarConfig.check(xcfa, logger);
logger.write(Logger.Level.INFO, "Safety check done.\n");
if (returnSafetyResult) {
Expand Down
Loading

0 comments on commit 4585748

Please sign in to comment.