Skip to content

Commit

Permalink
Moved to traits rather than classification
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Nov 15, 2023
1 parent 9ed1975 commit ab92574
Show file tree
Hide file tree
Showing 10 changed files with 111 additions and 64 deletions.
19 changes: 11 additions & 8 deletions subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/ParseContext.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,15 @@
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArchitectureType;
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType;
import hu.bme.mit.theta.frontend.transformation.CStmtCounter;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseOption;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait;

import java.util.LinkedHashSet;
import java.util.Set;

public class ParseContext {
private final FrontendMetadata metadata;
private final CStmtCounter cStmtCounter;
private BitwiseOption bitwiseOption;
private Set<ArithmeticTrait> arithmeticTraits = new LinkedHashSet<>();
private ArchitectureType architecture = ArchitectureType.ILP32;
private Boolean multiThreading = false;
private ArithmeticType arithmetic = ArithmeticType.efficient;
Expand All @@ -37,14 +40,14 @@ public ParseContext() {
public ParseContext(
final FrontendMetadata metadata,
final CStmtCounter cStmtCounter,
final BitwiseOption bitwiseOption,
final Set<ArithmeticTrait> arithmeticTraits,
final ArchitectureType architecture,
final Boolean multiThreading,
final ArithmeticType arithmetic
) {
this.metadata = metadata;
this.cStmtCounter = cStmtCounter;
this.bitwiseOption = bitwiseOption;
this.arithmeticTraits = arithmeticTraits;
this.architecture = architecture;
this.multiThreading = multiThreading;
this.arithmetic = arithmetic;
Expand All @@ -54,12 +57,12 @@ public FrontendMetadata getMetadata() {
return metadata;
}

public BitwiseOption getBitwiseOption() {
return bitwiseOption;
public Set<ArithmeticTrait> getArithmeticTraits() {
return Set.copyOf(arithmeticTraits);
}

public void setBitwiseOption(BitwiseOption bitwiseOption) {
this.bitwiseOption = bitwiseOption;
public void addArithmeticTrait(ArithmeticTrait arithmeticTrait) {
this.arithmeticTraits.add(arithmeticTrait);
}

public ArchitectureType getArchitecture() {
Expand Down
10 changes: 7 additions & 3 deletions .../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 @@ -28,9 +28,10 @@
import hu.bme.mit.theta.core.type.booltype.BoolType;
import hu.bme.mit.theta.frontend.ParseContext;
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig;
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType;
import hu.bme.mit.theta.frontend.transformation.grammar.expression.ExpressionVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseChecker;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseOption;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.GlobalDeclUsageVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.type.DeclarationVisitor;
Expand Down Expand Up @@ -72,6 +73,7 @@
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.StringJoiner;

import static com.google.common.base.Preconditions.checkState;
Expand Down Expand Up @@ -167,8 +169,10 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {

// if arithemetic is set on efficient, we change it to either bv or int arithmetic here
if (parseContext.getArithmetic() == ArchitectureConfig.ArithmeticType.efficient) { // if it wasn't on efficient, the check returns manual
BitwiseOption bitwiseOption = BitwiseChecker.checkIfBitwise(parseContext, globalUsages);
parseContext.setArithmetic((bitwiseOption == BitwiseOption.INTEGER) ? ArchitectureConfig.ArithmeticType.integer : ArchitectureConfig.ArithmeticType.bitvector);
Set<ArithmeticTrait> arithmeticTraits = BitwiseChecker.gatherArithmeticTraits(parseContext, globalUsages);
parseContext.setArithmetic(
arithmeticTraits.contains(ArithmeticTrait.BITWISE) || arithmeticTraits.contains(ArithmeticTrait.FLOAT) ?
ArithmeticType.bitvector : ArithmeticType.integer);
}

CProgram program = new CProgram(parseContext);
Expand Down
4 changes: 2 additions & 2 deletions ...on/grammar/preprocess/MainArithmetic.java → ...n/grammar/preprocess/ArithmeticTrait.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,6 @@

package hu.bme.mit.theta.frontend.transformation.grammar.preprocess;

public enum BitwiseOption {
INTEGER, BITWISE, BITWISE_FLOAT
public enum ArithmeticTrait {
LIN_INT, NONLIN_INT, BITWISE, FLOAT, ARR,
}
85 changes: 56 additions & 29 deletions ...main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/BitwiseChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,44 +18,72 @@

import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.DirectDeclaratorArray1Context;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.DirectDeclaratorArray2Context;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.DirectDeclaratorArray3Context;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.DirectDeclaratorArray4Context;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.MultiplicativeExpressionContext;
import hu.bme.mit.theta.frontend.ParseContext;

import java.util.List;

import static com.google.common.base.Preconditions.checkState;
import java.util.Set;

public class BitwiseChecker extends CBaseVisitor<Void> {
private BitwiseOption bitwiseOption = null;
private final ParseContext parseContext;

private BitwiseChecker(ParseContext parseContext) {
this.parseContext = parseContext;
}

// checks only once, returns the result of the first check after
public static BitwiseOption checkIfBitwise(ParseContext parseContext, List<CParser.ExternalDeclarationContext> contexts) {
BitwiseChecker instance = new BitwiseChecker();
instance.bitwiseOption = BitwiseOption.INTEGER;
public static Set<ArithmeticTrait> gatherArithmeticTraits(ParseContext parseContext, List<CParser.ExternalDeclarationContext> contexts) {
BitwiseChecker instance = new BitwiseChecker(parseContext);
for (CParser.ExternalDeclarationContext ctx : contexts) {
ctx.accept(instance);
}
checkState(instance.bitwiseOption != null);
parseContext.setBitwiseOption(instance.bitwiseOption);
return instance.bitwiseOption;
return instance.parseContext.getArithmeticTraits();
}

@Override
public Void visitTypeSpecifierDouble(CParser.TypeSpecifierDoubleContext ctx) {
bitwiseOption = BitwiseOption.BITWISE_FLOAT;
parseContext.addArithmeticTrait(ArithmeticTrait.FLOAT);
return null;
}

@Override
public Void visitTypeSpecifierFloat(CParser.TypeSpecifierFloatContext ctx) {
bitwiseOption = BitwiseOption.BITWISE_FLOAT;
parseContext.addArithmeticTrait(ArithmeticTrait.FLOAT);
return null;
}

@Override
public Void visitDirectDeclaratorArray1(DirectDeclaratorArray1Context ctx) {
parseContext.addArithmeticTrait(ArithmeticTrait.ARR);
return null;
}

@Override
public Void visitDirectDeclaratorArray2(DirectDeclaratorArray2Context ctx) {
parseContext.addArithmeticTrait(ArithmeticTrait.ARR);
return null;
}

@Override
public Void visitDirectDeclaratorArray3(DirectDeclaratorArray3Context ctx) {
parseContext.addArithmeticTrait(ArithmeticTrait.ARR);
return null;
}

@Override
public Void visitDirectDeclaratorArray4(DirectDeclaratorArray4Context ctx) {
parseContext.addArithmeticTrait(ArithmeticTrait.ARR);
return null;
}

@Override
public Void visitPrimaryExpressionConstant(CParser.PrimaryExpressionConstantContext ctx) {
String text = ctx.getText();
if (text.contains(".")) {
bitwiseOption = BitwiseOption.BITWISE_FLOAT;
parseContext.addArithmeticTrait(ArithmeticTrait.FLOAT);
return null;
}
return super.visitPrimaryExpressionConstant(ctx);
Expand All @@ -64,49 +92,48 @@ public Void visitPrimaryExpressionConstant(CParser.PrimaryExpressionConstantCont
@Override
public Void visitInclusiveOrExpression(CParser.InclusiveOrExpressionContext ctx) {
ctx.exclusiveOrExpression(0).accept(this);
Boolean b = ctx.exclusiveOrExpression().size() > 1;
boolean b = ctx.exclusiveOrExpression().size() > 1;
if (b) {
if (bitwiseOption == BitwiseOption.INTEGER) {
bitwiseOption = BitwiseOption.BITWISE;
}
parseContext.addArithmeticTrait(ArithmeticTrait.BITWISE);
}
return null;
}

@Override
public Void visitExclusiveOrExpression(CParser.ExclusiveOrExpressionContext ctx) {
ctx.andExpression(0).accept(this);
Boolean b = ctx.andExpression().size() > 1;
boolean b = ctx.andExpression().size() > 1;
if (b) {
if (bitwiseOption == BitwiseOption.INTEGER) {
bitwiseOption = BitwiseOption.BITWISE;
}
parseContext.addArithmeticTrait(ArithmeticTrait.BITWISE);
}
return null;
}

@Override
public Void visitAndExpression(CParser.AndExpressionContext ctx) {
ctx.equalityExpression(0).accept(this);
Boolean b = ctx.equalityExpression().size() > 1;
boolean b = ctx.equalityExpression().size() > 1;
if (b) {
if (bitwiseOption == BitwiseOption.INTEGER) {
bitwiseOption = BitwiseOption.BITWISE;
}
parseContext.addArithmeticTrait(ArithmeticTrait.BITWISE);
}
return null;
}

@Override
public Void visitShiftExpression(CParser.ShiftExpressionContext ctx) {
ctx.additiveExpression(0).accept(this);
Boolean b = ctx.additiveExpression().size() > 1;
boolean b = ctx.additiveExpression().size() > 1;
if (b) {
if (bitwiseOption == BitwiseOption.INTEGER) {
bitwiseOption = BitwiseOption.BITWISE;
}
parseContext.addArithmeticTrait(ArithmeticTrait.BITWISE);
}
return null;
}

@Override
public Void visitMultiplicativeExpression(MultiplicativeExpressionContext ctx) {
if (ctx.castExpression().size() > 1) {
parseContext.addArithmeticTrait(ArithmeticTrait.NONLIN_INT);
}
return super.visitMultiplicativeExpression(ctx);
}
}
2 changes: 1 addition & 1 deletion subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
val type = CComplexType.getType(globalDeclaration.get2().ref, parseContext)
if (type is CVoid || type is CStruct) {
uniqueWarningLogger.write(Level.INFO,
"WARNING: Not handling init expression of " + globalDeclaration.get1() + " as it is non initializable")
"WARNING: Not handling init expression of " + globalDeclaration.get1() + " as it is non initializable\n")
continue
}
builder.addVar(XcfaGlobalVar(globalDeclaration.get2(), type.nullValue))
Expand Down
4 changes: 2 additions & 2 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/VerificationTraits.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@

package hu.bme.mit.theta.xcfa.cli

import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseOption
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait

data class VerificationTraits(
val multithreaded: Boolean = false,
val arithmetic: BitwiseOption = BitwiseOption.INTEGER,
val arithmeticTraits: Set<ArithmeticTrait> = LinkedHashSet(),
)
13 changes: 8 additions & 5 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ class XcfaCli(private val args: Array<String>) {
logger.write(Logger.Level.INFO,
"Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
stopwatch.reset().start()
val config = parseConfigFromCli()
val config = parseConfigFromCli(parseContext)
if (strategy != Strategy.PORTFOLIO && printConfigFile != null) {
printConfigFile!!.writeText(gsonForOutput.toJson(config))
}
Expand Down Expand Up @@ -294,7 +294,7 @@ class XcfaCli(private val args: Array<String>) {
bindings["smtHome"] = solverHome
bindings["traits"] = VerificationTraits(
multithreaded = parseContext.multiThreading,
arithmetic = parseContext.bitwiseOption,
arithmeticTraits = parseContext.arithmeticTraits,
)
bindings["argdebug"] = argdebug

Expand All @@ -316,7 +316,7 @@ class XcfaCli(private val args: Array<String>) {
} else if (portfolio == "COMPLEX") {
complexPortfolio(xcfa, input!!.absolutePath, logger, solverHome, VerificationTraits(
multithreaded = parseContext.multiThreading,
arithmetic = parseContext.bitwiseOption,
arithmeticTraits = parseContext.arithmeticTraits,
), explicitProperty, parseContext, argdebug)
} else throw Exception("No known portfolio $portfolio")

Expand Down Expand Up @@ -417,7 +417,7 @@ class XcfaCli(private val args: Array<String>) {
}
}
logger.write(Logger.Level.RESULT,
"Arithmetic: ${parseContext.bitwiseOption}\n")
"Arithmetic: ${parseContext.arithmeticTraits}\n")
xcfaFromC
}

Expand Down Expand Up @@ -499,7 +499,7 @@ class XcfaCli(private val args: Array<String>) {
}
} else ErrorDetection.ERROR_LOCATION

private fun parseConfigFromCli(): XcfaCegarConfig {
private fun parseConfigFromCli(parseContext: ParseContext): XcfaCegarConfig {
val cegarConfig = XcfaCegarConfig()
try {
JCommander.newBuilder().addObject(cegarConfig).programName(JAR_NAME).build()
Expand All @@ -510,6 +510,9 @@ class XcfaCli(private val args: Array<String>) {
ex.usage()
exitProcess(ExitCodes.INVALID_PARAM.code)
}
if (parseContext.multiThreading && cegarConfig.search == Search.ERR) {
cegarConfig.search = Search.DFS;
}
return cegarConfig
}

Expand Down
11 changes: 5 additions & 6 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult
import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.BitwiseOption
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait
import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
import hu.bme.mit.theta.xcfa.cli.*
import hu.bme.mit.theta.xcfa.model.XCFA
Expand Down Expand Up @@ -341,11 +341,10 @@ fun complexPortfolio(xcfaTyped: XCFA, cFileNameTyped: String, loggerTyped: Logge
return STM(inProcess, setOf(fallbackEdge))
}

val stm = when (traitsTyped.arithmetic) {
BitwiseOption.INTEGER -> integerStm()
BitwiseOption.BITWISE -> bitwiseStm()
BitwiseOption.BITWISE_FLOAT -> floatsStm()
}
val stm =
if (traitsTyped.arithmeticTraits.contains(ArithmeticTrait.FLOAT)) floatsStm()
else if (traitsTyped.arithmeticTraits.contains(ArithmeticTrait.BITWISE)) bitwiseStm()
else integerStm()

return stm.execute() as Pair<XcfaCegarConfig, SafetyResult<*, *>>
}
Loading

0 comments on commit ab92574

Please sign in to comment.