From 4585748231967e09e46b6e4dafa94afc55d5d957 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 12 Nov 2023 21:36:16 +0100 Subject: [PATCH] Added better logging, and complex portfolio --- scripts/complex.kts | 271 ++++++++++++++++++ scripts/{portfolio.kts => simple.kts} | 0 .../grammar/expression/ExpressionVisitor.java | 8 +- .../grammar/function/FunctionVisitor.java | 2 +- .../grammar/type/DeclarationVisitor.java | 2 +- .../grammar/type/TypeVisitor.java | 6 +- .../model/types/simple/NamedType.java | 2 +- .../model/types/simple/Struct.java | 2 +- subprojects/xcfa/xcfa-cli/build.gradle.kts | 14 +- .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 17 +- .../mit/theta/xcfa/cli/XcfaCegarServer.java | 21 +- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 47 ++- .../mit/theta/xcfa/passes/UnusedVarPass.kt | 2 +- 13 files changed, 347 insertions(+), 47 deletions(-) create mode 100644 scripts/complex.kts rename scripts/{portfolio.kts => simple.kts} (100%) diff --git a/scripts/complex.kts b/scripts/complex.kts new file mode 100644 index 0000000000..e12d8f0b5a --- /dev/null +++ b/scripts/complex.kts @@ -0,0 +1,271 @@ +/* + * Copyright 2022 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. + */ + +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseOption +import hu.bme.mit.theta.frontend.ParseContext +import hu.bme.mit.theta.xcfa.analysis.ErrorDetection +import hu.bme.mit.theta.xcfa.cli.* +import hu.bme.mit.theta.xcfa.cli.portfolio.* +import hu.bme.mit.theta.xcfa.model.XCFA +import java.io.File +import java.util.concurrent.TimeoutException + +val xcfaTyped = xcfa as XCFA +val cFileNameTyped = cFileName as String +val loggerTyped = logger as Logger +val smtHomeTyped = smtHome as String +val traitsTyped = traits as VerificationTraits +val propertyTyped = property as ErrorDetection +val parseContextTyped = parseContext as ParseContext + +val checker = {p: Boolean, config: XcfaCegarConfig -> + if(p) + config.checkInProcess(xcfaTyped, smtHomeTyped, true, cFileNameTyped, loggerTyped, parseContextTyped)() + else config.check(xcfaTyped, loggerTyped) +} + +var baseConfig = XcfaCegarConfig( + errorDetectionType = propertyTyped, + abstractionSolver = "Z3", + validateAbstractionSolver = false, + domain = Domain.EXPL, + maxEnum = 1, + search = Search.ERR, + initPrec = InitPrec.EMPTY, + porLevel = POR.NOPOR, + refinementSolver = "Z3", + validateRefinementSolver = false, + refinement = Refinement.SEQ_ITP, + exprSplitter = ExprSplitterOptions.WHOLE, + pruneStrategy = PruneStrategy.FULL, + cexMonitor = CexMonitorOptions.CHECK, + timeoutMs = 0 +) + +if(traitsTyped.multithreaded) { + baseConfig = baseConfig.copy(search=Search.BFS, porLevel=POR.AASPOR, pruneStrategy = PruneStrategy.LAZY) + + if(propertyTyped == ErrorDetection.DATA_RACE) { + baseConfig = baseConfig.copy(porLevel=POR.SPOR) + } +} + +val timeoutTrigger = ExceptionTrigger( + ErrorCodeException(ExitCodes.TIMEOUT.code), + ErrorCodeException(ExitCodes.VERIFICATION_STUCK.code), + ErrorCodeException(ExitCodes.OUT_OF_MEMORY.code), + ErrorCodeException(ExitCodes.GENERIC_ERROR.code), + label="Timeout" +) + +val timeoutOrSolverError = ExceptionTrigger( + ErrorCodeException(ExitCodes.SOLVER_ERROR.code), + ErrorCodeException(ExitCodes.TIMEOUT.code), + ErrorCodeException(ExitCodes.VERIFICATION_STUCK.code), + ErrorCodeException(ExitCodes.OUT_OF_MEMORY.code), + ErrorCodeException(ExitCodes.GENERIC_ERROR.code), + label="TimeoutOrSolverError" +) + +val quickExplConfig = baseConfig.copy(initPrec=InitPrec.ALLVARS, timeoutMs = 90_000) +val emptyExplConfig = baseConfig.copy(timeoutMs = 210_000) +val predConfig = baseConfig.copy(domain=Domain.PRED_CART, refinement = Refinement.BW_BIN_ITP) + +fun integerStm(): STM { + fun getStm(inProcess: Boolean): STM { + val config_1_1 = ConfigNode("QuickFullExpl_z3_4.10.1_$inProcess", quickExplConfig.copy(abstractionSolver = "z3:4.10.1", refinementSolver = "z3:4.10.1", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_2_1 = ConfigNode("EmptyExpl_z3_4.10.1_$inProcess", emptyExplConfig.copy(abstractionSolver = "z3:4.10.1", refinementSolver = "z3:4.10.1", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_3_1 = ConfigNode("PredCart_z3_4.10.1_$inProcess", predConfig.copy(abstractionSolver = "z3:4.10.1", refinementSolver = "z3:4.10.1"), checker, inProcess) + + val config_1_2 = ConfigNode("QuickFullExpl_Z3_$inProcess", quickExplConfig.copy(), checker, inProcess) + val config_2_2 = ConfigNode("EmptyExpl_Z3_$inProcess", emptyExplConfig.copy(), checker, inProcess) + val config_3_2 = ConfigNode("PredCart_Z3_$inProcess", predConfig.copy(), checker, inProcess) + + val config_1_3 = ConfigNode("QuickFullExpl_princess_2022_07_01_$inProcess", quickExplConfig.copy(abstractionSolver = "princess:2022-07-01", refinementSolver = "princess:2022-07-01"), checker, inProcess) + val config_2_3 = ConfigNode("EmptyExpl_princess_2022_07_01_$inProcess", emptyExplConfig.copy(abstractionSolver = "princess:2022-07-01", refinementSolver = "princess:2022-07-01"), checker, inProcess) + val config_3_3 = ConfigNode("PredCart_mathsat_5.6.8_$inProcess", predConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8"), checker, inProcess) + + val config_1_4 = ConfigNode("QuickFullExpl_mathsat_5.6.8_$inProcess", quickExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8"), checker, inProcess) + val config_2_4 = ConfigNode("EmptyExpl_mathsat_5.6.8_$inProcess", emptyExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8"), checker, inProcess) + val config_3_4 = ConfigNode("PredCart_princess_2022_07_01_$inProcess", predConfig.copy(abstractionSolver = "princess:2022-07-01", refinementSolver = "princess:2022-07-01"), checker, inProcess) + + val timeouts = setOf( + Edge(config_1_1, config_2_1, timeoutTrigger), + Edge(config_2_1, config_3_1, timeoutTrigger), + + Edge(config_1_2, config_2_2, timeoutTrigger), + Edge(config_2_2, config_3_1, timeoutTrigger), + + Edge(config_1_3, config_2_3, timeoutTrigger), + Edge(config_2_3, config_3_1, timeoutTrigger), + + Edge(config_1_4, config_2_4, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + Edge(config_2_4, config_3_1, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + ) + + val notTimeout = if(inProcess) ExceptionTrigger(ErrorCodeException(ExitCodes.SOLVER_ERROR.code), label="SolverError") else ExceptionTrigger(fallthroughExceptions=timeoutTrigger.exceptions, label="AnythingButTimeout") + + val solverExceptions = setOf( + Edge(config_1_1, config_1_2, notTimeout), + Edge(config_1_2, config_1_3, notTimeout), + Edge(config_1_3, config_1_4, notTimeout), + + Edge(config_2_1, config_2_2, notTimeout), + Edge(config_2_2, config_2_3, notTimeout), + Edge(config_2_3, config_2_4, notTimeout), + + Edge(config_3_1, config_3_2, notTimeout), + Edge(config_3_2, config_3_3, notTimeout), + Edge(config_3_3, config_3_4, notTimeout), + ) + return STM(config_1_1, timeouts union solverExceptions) + } + + val inProcess = HierarchicalNode("InProcess", getStm(true)) + val notInProcess = HierarchicalNode("NotInprocess", getStm(false)) + + val fallbackEdge = Edge(inProcess, notInProcess, ExceptionTrigger(label="Anything")) + + return STM(inProcess, setOf(fallbackEdge)) +} + +fun bitwiseStm(): STM { + fun getStm(inProcess: Boolean): STM { + val config_1_1 = ConfigNode("QuickFullExpl_Z3_$inProcess", quickExplConfig.copy(refinement=Refinement.NWT_IT_WP), checker, inProcess) + val config_2_1 = ConfigNode("EmptyExpl_Z3_$inProcess", emptyExplConfig.copy(refinement=Refinement.NWT_IT_WP), checker, inProcess) + val config_3_1 = ConfigNode("PredCart_mathsat_5.6.8_$inProcess", predConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8"), checker, inProcess) + + val config_1_2 = ConfigNode("QuickFullExpl_cvc5_1.0.2_$inProcess", quickExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_2_2 = ConfigNode("EmptyExpl_cvc5_1.0.2_$inProcess", emptyExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_3_2 = ConfigNode("PredCart_z3_4.10.1_$inProcess", predConfig.copy(abstractionSolver = "z3:4.10.1", refinementSolver = "z3:4.10.1"), checker, inProcess) + + val config_1_3 = ConfigNode("QuickFullExpl_mathsat_5.6.8_$inProcess", quickExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8", refinement=Refinement.NWT_IT_WP), checker, inProcess) + val config_2_3 = ConfigNode("EmptyExpl_mathsat_5.6.8_$inProcess", emptyExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8", refinement = Refinement.SEQ_ITP), checker, inProcess) + val config_3_3 = ConfigNode("PredCart_cvc5_1.0.2_$inProcess", predConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + + val timeouts = setOf( + Edge(config_1_1, config_2_1, timeoutTrigger), + Edge(config_2_1, config_3_1, timeoutTrigger), + + Edge(config_1_2, config_2_2, timeoutTrigger), + Edge(config_2_2, config_3_1, timeoutTrigger), + + Edge(config_1_3, config_2_3, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + Edge(config_2_3, config_3_1, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + ) + + val notTimeout = if(inProcess) ExceptionTrigger(ErrorCodeException(ExitCodes.SOLVER_ERROR.code), label="SolverError") else ExceptionTrigger(fallthroughExceptions=timeoutTrigger.exceptions, label="AnythingButTimeout") + + val solverExceptions = setOf( + Edge(config_1_1, config_1_2, notTimeout), + Edge(config_1_2, config_1_3, notTimeout), + + Edge(config_2_1, config_2_2, notTimeout), + Edge(config_2_2, config_2_3, notTimeout), + + Edge(config_3_1, config_3_2, notTimeout), + Edge(config_3_2, config_3_3, notTimeout), + ) + return STM(config_1_1, timeouts union solverExceptions) + } + + val inProcess = HierarchicalNode("InProcess", getStm(true)) + val notInProcess = HierarchicalNode("NotInprocess", getStm(false)) + + val fallbackEdge = Edge(inProcess, notInProcess, ExceptionTrigger(label="Anything")) + + return STM(inProcess, setOf(fallbackEdge)) +} + +fun floatsStm(): STM { + fun getStm(inProcess: Boolean): STM { + val config_1_1 = ConfigNode("QuickFullExpl_cvc5_1.0.2_$inProcess", quickExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_2_1 = ConfigNode("EmptyExpl_cvc5_1.0.2_$inProcess", quickExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_3_1 = ConfigNode("PredCart_mathsat_5.6.8_$inProcess", predConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8"), checker, inProcess) + + val config_1_2 = ConfigNode("QuickFullExpl_cvc5_1.0.2_seq_$inProcess", quickExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.SEQ_ITP), checker, inProcess) + val config_2_2 = ConfigNode("EmptyExpl_cvc5_1.0.2_seq_$inProcess", emptyExplConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.SEQ_ITP), checker, inProcess) + val config_3_2 = ConfigNode("PredCart_bitwuzla_latest_$inProcess", predConfig.copy(abstractionSolver = "bitwuzla:latest", refinementSolver = "bitwuzla:latest", refinement=Refinement.NWT_IT_WP), checker, inProcess) + + val config_1_3 = ConfigNode("QuickFullExpl_mathsat_5.6.8_$inProcess", quickExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8", validateAbstractionSolver=true, validateRefinementSolver=true, refinement=Refinement.NWT_IT_WP), checker, inProcess) + val config_2_3 = ConfigNode("EmptyExpl_mathsat_5.6.8_$inProcess", emptyExplConfig.copy(abstractionSolver = "mathsat:5.6.8", refinementSolver = "mathsat:5.6.8", validateAbstractionSolver=true, validateRefinementSolver=true, refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_3_3 = ConfigNode("PredCart_cvc5_1.0.2_$inProcess", predConfig.copy(abstractionSolver = "cvc5:1.0.2", refinementSolver = "cvc5:1.0.2", refinement = Refinement.NWT_IT_WP), checker, inProcess) + + val config_1_4 = ConfigNode("QuickFullExpl_mathsat_fp_$inProcess", quickExplConfig.copy(abstractionSolver = "mathsat:fp", refinementSolver = "mathsat:fp", validateAbstractionSolver=true, validateRefinementSolver=true), checker, inProcess) + val config_2_4 = ConfigNode("EmptyExpl_mathsat_fp_$inProcess", emptyExplConfig.copy(abstractionSolver = "mathsat:fp", refinementSolver = "mathsat:fp", validateAbstractionSolver=true, validateRefinementSolver=true), checker, inProcess) + val config_3_4 = ConfigNode("PredCart_mathsat_fp_$inProcess", predConfig.copy(abstractionSolver = "mathsat:fp", refinementSolver = "mathsat:fp", validateAbstractionSolver=true, validateRefinementSolver=true), checker, inProcess) + + val config_1_5 = ConfigNode("QuickFullExpl_Z3_$inProcess", quickExplConfig.copy(abstractionSolver = "Z3", refinementSolver = "Z3", validateAbstractionSolver=true, validateRefinementSolver=true, refinement=Refinement.NWT_IT_WP), checker, inProcess) + val config_2_5 = ConfigNode("EmptyExpl_Z3_$inProcess", emptyExplConfig.copy(abstractionSolver = "Z3", refinementSolver = "Z3", validateAbstractionSolver=true, validateRefinementSolver=true, refinement = Refinement.NWT_IT_WP), checker, inProcess) + val config_3_5 = ConfigNode("PredCart_Z3_$inProcess", predConfig.copy(abstractionSolver = "Z3", refinementSolver = "Z3", refinement = Refinement.NWT_IT_WP), checker, inProcess) + + + val timeouts = setOf( + Edge(config_1_1, config_2_1, timeoutTrigger), + Edge(config_2_1, config_3_1, timeoutTrigger), + + Edge(config_1_2, config_2_2, timeoutTrigger), + Edge(config_2_2, config_3_1, timeoutTrigger), + + Edge(config_1_3, config_2_3, timeoutTrigger), + Edge(config_2_3, config_3_1, timeoutTrigger), + + Edge(config_1_4, config_2_4, timeoutTrigger), + Edge(config_2_4, config_3_1, timeoutTrigger), + + Edge(config_1_5, config_2_5, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + Edge(config_2_5, config_3_1, if(inProcess) timeoutOrSolverError else ExceptionTrigger(label="Anything")), + ) + + val notTimeout = if(inProcess) ExceptionTrigger(ErrorCodeException(ExitCodes.SOLVER_ERROR.code), label="SolverError") else ExceptionTrigger(fallthroughExceptions=timeoutTrigger.exceptions, label="AnythingButTimeout") + + val solverExceptions = setOf( + Edge(config_1_1, config_1_2, notTimeout), + Edge(config_1_2, config_1_3, notTimeout), + Edge(config_1_3, config_1_4, notTimeout), + Edge(config_1_4, config_1_5, notTimeout), + + Edge(config_2_1, config_2_2, notTimeout), + Edge(config_2_2, config_2_3, notTimeout), + Edge(config_2_3, config_2_4, notTimeout), + Edge(config_2_4, config_2_5, notTimeout), + + Edge(config_3_1, config_3_2, notTimeout), + Edge(config_3_2, config_3_3, notTimeout), + Edge(config_3_3, config_3_4, notTimeout), + Edge(config_3_4, config_3_5, notTimeout), + ) + return STM(config_1_1, timeouts union solverExceptions) + } + + val inProcess = HierarchicalNode("InProcess", getStm(true)) + val notInProcess = HierarchicalNode("NotInprocess", getStm(false)) + + val fallbackEdge = Edge(inProcess, notInProcess, ExceptionTrigger(label="Anything")) + + return STM(inProcess, setOf(fallbackEdge)) +} + +val stm = when(traitsTyped.arithmetic) { + BitwiseOption.INTEGER -> integerStm() + BitwiseOption.BITWISE -> bitwiseStm() + BitwiseOption.BITWISE_FLOAT -> floatsStm() +} + +stm.execute() diff --git a/scripts/portfolio.kts b/scripts/simple.kts similarity index 100% rename from scripts/portfolio.kts rename to scripts/simple.kts 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 5e9084855f..084dd96d50 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 @@ -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); @@ -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); @@ -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); @@ -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; } 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 0026f32e8a..aa34d7d263 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 @@ -130,7 +130,7 @@ private void createVars(String name, CDeclaration declaration, CComplexType type Tuple2>> 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); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java index aef372d29f..2eac00cd9b 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java @@ -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; } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java index fe913694e3..8bf0016648 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java @@ -85,7 +85,7 @@ private CSimpleType mergeCTypes(List cSimpleTypes) { List 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); } @@ -106,7 +106,7 @@ private CSimpleType mergeCTypes(List 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); } @@ -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); } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java index 2e9e295c67..6223532c58 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java @@ -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; } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java index d03541178f..24a31f96f1 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java @@ -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; diff --git a/subprojects/xcfa/xcfa-cli/build.gradle.kts b/subprojects/xcfa/xcfa-cli/build.gradle.kts index 35870a9554..054d1927e9 100644 --- a/subprojects/xcfa/xcfa-cli/build.gradle.kts +++ b/subprojects/xcfa/xcfa-cli/build.gradle.kts @@ -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) -// } -//} - 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 bb16d46173..1b8c862699 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 @@ -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 @@ -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) { @@ -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 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 c24d3138cc..e7654daf7e 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 @@ -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; @@ -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; @@ -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; @@ -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 check = xcfaCegarConfig.check(xcfa, logger); logger.write(Logger.Level.INFO, "Safety check done.\n"); if (returnSafetyResult) { 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 af20be3108..68cdcd9705 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 @@ -64,9 +64,9 @@ import java.nio.file.FileSystems import java.util.* import java.util.concurrent.TimeUnit import javax.script.Bindings +import javax.script.Compilable import javax.script.ScriptEngine import javax.script.ScriptEngineManager -import javax.script.SimpleBindings import kotlin.random.Random import kotlin.system.exitProcess @@ -204,7 +204,7 @@ class XcfaCli(private val args: Array) { } LoopUnrollPass.UNROLL_LIMIT = loopUnroll - logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") + logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType\n") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext, uniqueWarningLogger) ConeOfInfluence = if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) @@ -215,17 +215,23 @@ class XcfaCli(private val args: Array) { preVerificationLogging(logger, xcfa, gsonForOutput, parseContext) if (noAnalysis) { - logger.write(Logger.Level.RESULT, "ParsingResult Success") + logger.write(Logger.Level.RESULT, "ParsingResult Success\n") return } // verification stopwatch.reset().start() - logger.write(Logger.Level.INFO, "Starting verification of ${xcfa.name} using $backend") + logger.write(Logger.Level.INFO, + "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using $backend\n") registerAllSolverManagers(solverHome, logger) + logger.write(Logger.Level.INFO, + "Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + stopwatch.reset().start() val config = parseConfigFromCli() if (strategy != Strategy.PORTFOLIO && printConfigFile != null) { printConfigFile!!.writeText(gsonForOutput.toJson(config)) } + logger.write(Logger.Level.INFO, "Parsed config (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + stopwatch.reset().start() val safetyResult: SafetyResult<*, *> = when (strategy) { Strategy.DIRECT -> runDirect(xcfa, config, logger) @@ -268,7 +274,7 @@ class XcfaCli(private val args: Array) { val portfolioDescriptor = portfolio val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts") return try { - val bindings: Bindings = SimpleBindings() + val bindings: Bindings = kotlinEngine.createBindings() bindings["xcfa"] = xcfa bindings["parseContext"] = parseContext bindings["property"] = explicitProperty @@ -279,8 +285,21 @@ class XcfaCli(private val args: Array) { multithreaded = parseContext.multiThreading, arithmetic = parseContext.bitwiseOption, ) - val portfolioResult = kotlinEngine.eval(FileReader(portfolioDescriptor), - bindings) as Pair> + + kotlinEngine as Compilable + val stopwatch = Stopwatch.createStarted() + + kotlinEngine.eval("true") as Boolean + logger.write(Logger.Level.INFO, + "Loaded script engine (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + stopwatch.reset().start() + + kotlinEngine.context.setBindings(bindings, + 100) // 100 seems to be a safe default, based on AbstractScriptEngine + val compiled = kotlinEngine.compile(FileReader(portfolioDescriptor)) + logger.write(Logger.Level.INFO, "Compiled portfolio (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + + val portfolioResult = compiled.eval() as Pair> concretizerSolver = portfolioResult.first.refinementSolver validateConcretizerSolver = portfolioResult.first.validateRefinementSolver @@ -292,7 +311,7 @@ class XcfaCli(private val args: Array) { } catch (e: Exception) { if (debug) throw e logger.write(Logger.Level.RESULT, - "Portfolio from $portfolioDescriptor could not be executed.") + "Portfolio from $portfolioDescriptor could not be executed.\n") e.printStackTrace() exitProcess(ExitCodes.PORTFOLIO_ERROR.code) } @@ -304,7 +323,7 @@ class XcfaCli(private val args: Array) { resultFolder.mkdirs() logger.write(Logger.Level.INFO, - "Writing results to directory ${resultFolder.absolutePath}") + "Writing results to directory ${resultFolder.absolutePath}\n") val xcfaDotFile = File(resultFolder, "xcfa.dot") xcfaDotFile.writeText(xcfa.toDot()) @@ -313,7 +332,7 @@ class XcfaCli(private val args: Array) { val xcfaCFile = File(resultFolder, "xcfa.c") xcfaCFile.writeText(xcfa.toC(parseContext, useArr, useExArr, useRange)) } catch (e: Throwable) { - logger.write(Logger.Level.VERBOSE, "Could not emit C file") + logger.write(Logger.Level.VERBOSE, "Could not emit C file\n") } val xcfaJsonFile = File(resultFolder, "xcfa.json") @@ -398,7 +417,7 @@ class XcfaCli(private val args: Array) { chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)), ChcPasses(parseContext, uniqueWarningLogger)) } catch (e: UnsupportedOperationException) { - logger.write(Logger.Level.INFO, "Non-linear CHC found, retrying using backward transformation...") + logger.write(Logger.Level.INFO, "Non-linear CHC found, retrying using backward transformation...\n") chcFrontend = ChcFrontend(ChcFrontend.ChcTransformation.BACKWARD) chcFrontend.buildXcfa(CharStreams.fromStream(FileInputStream(input!!)), ChcPasses(parseContext, uniqueWarningLogger)) @@ -423,7 +442,7 @@ class XcfaCli(private val args: Array) { remainingFlags.add(ErrorDetection.DATA_RACE.toString()) if (lbeLevel != LbePass.LbeLevel.NO_LBE) { uniqueWarningLogger.write(Logger.Level.INFO, - "Changing LBE type to NO_LBE because the DATA_RACE property will be erroneous otherwise") + "Changing LBE type to NO_LBE because the DATA_RACE property will be erroneous otherwise\n") lbeLevel = LbePass.LbeLevel.NO_LBE } ErrorDetection.DATA_RACE @@ -433,7 +452,7 @@ class XcfaCli(private val args: Array) { remainingFlags.add(ErrorDetection.OVERFLOW.toString()) if (lbeLevel != LbePass.LbeLevel.NO_LBE) { uniqueWarningLogger.write(Logger.Level.INFO, - "Changing LBE type to NO_LBE because the OVERFLOW property will be erroneous otherwise") + "Changing LBE type to NO_LBE because the OVERFLOW property will be erroneous otherwise\n") lbeLevel = LbePass.LbeLevel.NO_LBE } ErrorDetection.OVERFLOW @@ -442,7 +461,7 @@ class XcfaCli(private val args: Array) { else -> { remainingFlags.add(ErrorDetection.NO_ERROR.toString()) uniqueWarningLogger.write(Logger.Level.INFO, - "Unknown property $property, using full state space exploration (no refinement)") + "Unknown property $property, using full state space exploration (no refinement)\n") ErrorDetection.NO_ERROR } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt index 3f0f9a4fc1..afc9234b12 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt @@ -40,7 +40,7 @@ class UnusedVarPass(val parseContext: ParseContext, val uniqueWarningLogger: Log val varsAndParams = Sets.union(allVars, builder.getParams().map { it.first }.toSet()) if (!varsAndParams.containsAll(usedVars)) { uniqueWarningLogger.write(Logger.Level.INFO, - "Warning: There are some used variables not present as declarations: \n${ + "WARNING: There are some used variables not present as declarations: \n${ usedVars.filter { !varsAndParams.contains(it) }