Skip to content

Commit

Permalink
Final fixups
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Nov 16, 2023
1 parent 757c652 commit 9db1fda
Show file tree
Hide file tree
Showing 9 changed files with 93 additions and 25 deletions.
2 changes: 1 addition & 1 deletion subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ private void run() {
sw.stop();
} else if (algorithm == Algorithm.IMC) {
var transFunc = CfaToMonoliticTransFunc.create(cfa);
var checker = new ImcChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), ExplState::of, cfa.getVars(), true);
var checker = new ImcChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), ExplState::of, cfa.getVars());
status = checker.check(null);
logger.write(Logger.Level.RESULT, "%s%n", status);
sw.stop();
Expand Down
57 changes: 40 additions & 17 deletions ...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,12 @@
*/
package hu.bme.mit.theta.analysis.algorithm.imc;

import com.google.common.base.Stopwatch;
import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.ARG;
import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc;
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
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.analysis.expr.StmtAction;
import hu.bme.mit.theta.analysis.unit.UnitPrec;
Expand All @@ -31,36 +31,48 @@
import hu.bme.mit.theta.core.utils.PathUtils;
import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
import hu.bme.mit.theta.solver.*;
import hu.bme.mit.theta.solver.ItpMarker;
import hu.bme.mit.theta.solver.ItpPattern;
import hu.bme.mit.theta.solver.ItpSolver;
import hu.bme.mit.theta.solver.utils.WithPushPop;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.concurrent.TimeUnit;
import java.util.function.Function;


import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*;
import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And;
import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not;
import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Or;


public class ImcChecker<S extends ExprState, A extends StmtAction> implements SafetyChecker<S, A, UnitPrec> {
final Expr<BoolType> trans;
final Expr<BoolType> init;
final Expr<BoolType> prop;
final int upperBound;
ItpSolver solver;
final VarIndexing firstIndexing;
final VarIndexing offset;
final Function<Valuation, S> valToState;
final Collection<VarDecl<?>> vars;
final boolean interpolateForward;
private final Expr<BoolType> trans;
private final Expr<BoolType> init;
private final Expr<BoolType> prop;
private final int upperBound;
private ItpSolver solver;
private final VarIndexing firstIndexing;
private final VarIndexing offset;
private final Function<Valuation, S> valToState;
private final Collection<VarDecl<?>> vars;
private final int timeout;

public ImcChecker(MonolithicTransFunc transFunc,
int upperBound,
ItpSolver solver,
Function<Valuation, S> valToState,
Collection<VarDecl<?>> vars) {
this(transFunc, upperBound, solver, valToState, vars, 0);
}

public ImcChecker(MonolithicTransFunc transFunc,
int upperBound,
ItpSolver solver,
Function<Valuation, S> valToState,
Collection<VarDecl<?>> vars,
boolean interpolateForward1) {
int timeout) {
this.trans = transFunc.getTransExpr();
this.init = transFunc.getInitExpr();
this.prop = transFunc.getPropExpr();
Expand All @@ -70,12 +82,14 @@ public ImcChecker(MonolithicTransFunc transFunc,
this.offset = transFunc.getOffsetIndexing();
this.valToState = valToState;
this.vars = vars;
interpolateForward = interpolateForward1;
this.timeout = timeout;
}


@Override
public SafetyResult<S, A> check(UnitPrec prec) {
final Stopwatch sw = Stopwatch.createStarted();

int i = 0;
var exprsFromStart = new ArrayList<>(List.of(PathUtils.unfold(init, VarIndexingFactory.indexing(0))));
var listOfIndexes = new ArrayList<>(List.of(firstIndexing));
Expand All @@ -84,7 +98,7 @@ public SafetyResult<S, A> check(UnitPrec prec) {
final ItpMarker b = solver.createMarker();
final ItpPattern pattern = solver.createBinPattern(a, b);

while (i < upperBound) {
while (i < upperBound && (timeout == 0 || sw.elapsed(TimeUnit.SECONDS) < timeout)) {
i++;
var newIndex = listOfIndexes.get(i - 1).add(offset);
var expression = PathUtils.unfold(trans, listOfIndexes.get(i - 1));
Expand All @@ -102,6 +116,10 @@ public SafetyResult<S, A> check(UnitPrec prec) {
var img = exprsFromStart.get(0);

var status = solver.check();
if (!(timeout == 0 || sw.elapsed(TimeUnit.SECONDS) < timeout)) {
return null;
}

if (status.isSat()) {
S initial = null;
for (int j = 0; j < listOfIndexes.size(); j++) {
Expand All @@ -123,6 +141,8 @@ public SafetyResult<S, A> check(UnitPrec prec) {
solver.add(a, And(itpFormula, Not(img)));
if (solver.check().isUnsat()) {
return SafetyResult.safe(ARG.create((state1, state2) -> false));
} else if (!(timeout == 0 || sw.elapsed(TimeUnit.SECONDS) < timeout)) {
return null;
}
}
img = Or(img, itpFormula);
Expand All @@ -132,6 +152,9 @@ public SafetyResult<S, A> check(UnitPrec prec) {
solver.add(b, And(And(exprsFromStart.subList(2, exprsFromStart.size())), unfoldedProp));

status = solver.check();
if (!(timeout == 0 || sw.elapsed(TimeUnit.SECONDS) < timeout)) {
return null;
}
}
solver.pop();

Expand Down
2 changes: 1 addition & 1 deletion subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ private void run() {
status = checker.check(null);
} else if (algorithm.equals(Algorithm.IMC)) {
var transFunc = StsToMonoliticTransFunc.create(sts);
var checker = new ImcChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), ExplState::of, sts.getVars(), true);
var checker = new ImcChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), ExplState::of, sts.getVars());
status = checker.check(null);
}
sw.stop();
Expand Down
1 change: 1 addition & 0 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ enum class Backend {
CEGAR,
KIND,
IMC,
IMC_THEN_KIND,
LAZY
}

Expand Down
31 changes: 29 additions & 2 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 @@ -22,10 +22,14 @@ import com.google.common.base.Stopwatch
import com.google.gson.Gson
import com.google.gson.GsonBuilder
import com.google.gson.JsonParser
import hu.bme.mit.theta.analysis.Prec
import hu.bme.mit.theta.analysis.Trace
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
import hu.bme.mit.theta.analysis.algorithm.SafetyResult
import hu.bme.mit.theta.analysis.algorithm.debug.ARGWebDebugger
import hu.bme.mit.theta.analysis.expl.ExplState
import hu.bme.mit.theta.analysis.expr.ExprAction
import hu.bme.mit.theta.analysis.expr.ExprState
import hu.bme.mit.theta.analysis.utils.ArgVisualizer
import hu.bme.mit.theta.analysis.utils.TraceVisualizer
import hu.bme.mit.theta.c2xcfa.getXcfaFromC
Expand Down Expand Up @@ -258,8 +262,31 @@ class XcfaCli(private val args: Array<String>) {
val kindConfig = parseKindConfigFromCli()
kindConfig.getKindChecker(xcfa)
} else if (backend == Backend.IMC) {
val kindConfig = parseIMCConfigFromCli()
kindConfig.getIMCChecker(xcfa)
val imcConfig = parseIMCConfigFromCli()
imcConfig.getIMCChecker(xcfa)
} else if (backend == Backend.IMC_THEN_KIND) {
SafetyChecker<ExprState, ExprAction, Prec> {
val safetyResult = try {
val imcConfig = parseIMCConfigFromCli()
logger.write(Logger.Level.SUBSTEP, "Starting IMC with config $imcConfig...\n")
val ret = imcConfig.getIMCChecker(xcfa, 60).check(null)
logger.write(Logger.Level.SUBSTEP, "IMC ended\n")
ret
} catch (e: Throwable) {
logger.write(Logger.Level.SUBSTEP, "IMC threw exception: $e\n")
null
// do not do anything, kind will run
}
if (safetyResult == null) {
val kindConfig = parseKindConfigFromCli()
logger.write(Logger.Level.SUBSTEP, "Starting KIND with config $kindConfig\n")
val ret = kindConfig.getKindChecker(xcfa).check(null) as SafetyResult<ExprState, ExprAction>
logger.write(Logger.Level.SUBSTEP, "KIND ended\n")
ret
} else {
safetyResult as SafetyResult<ExprState, ExprAction>
}
}
} else {
error("Backend $backend not supported")
}
Expand Down
6 changes: 4 additions & 2 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaImcConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,17 +34,19 @@ data class XcfaImcConfig(
@Parameter(names = ["--max-bound"],
description = "How many successors to enumerate in a transition. Only relevant to the explicit domain. Use 0 for no limit.")
var maxBound: Int = Int.MAX_VALUE,
@Parameter
var remainingFlags: MutableList<String> = ArrayList()
) {

fun getIMCChecker(xcfa: XCFA): ImcChecker<ExprState, StmtAction> {
fun getIMCChecker(xcfa: XCFA, timeout: Int = 0): ImcChecker<ExprState, StmtAction> {
val transFunc = XcfaMonolithicTransFunc.create(xcfa)
return ImcChecker<ExprState, StmtAction>(
transFunc,
maxBound,
getSolver(imcSolver, validateIMCSolver).createItpSolver(),
ExplState::of,
ExprUtils.getVars(transFunc.transExpr),
true)
timeout)
}

}
4 changes: 3 additions & 1 deletion subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaKindConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ data class XcfaKindConfig(
@Parameter(names = ["--validate-bmc-solver"],
description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.")
var validateBMCSolver: Boolean = false,
@Parameter(names = ["--induction-solver"], description = "Induction solver name")
@Parameter(names = ["--induction-solver", "--ind-solver"], description = "Induction solver name")
var indSolver: String = "Z3",
@Parameter(names = ["--validate-induction-solver"],
description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.")
Expand All @@ -45,6 +45,8 @@ data class XcfaKindConfig(
@Parameter(names = ["--ind-frequency"],
description = "Frequency of induction check")
var indFreq: Int = 1,
@Parameter
var remainingFlags: MutableList<String> = ArrayList()
) {

fun getKindChecker(xcfa: XCFA): KIndChecker<ExprState, ExprAction> {
Expand Down
13 changes: 13 additions & 0 deletions subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,4 +198,17 @@ class XcfaCliVerifyTest {
main(params)
}

@ParameterizedTest
@MethodSource("singleThreadedCFiles")
fun testCVerifyIMC(filePath: String, extraArgs: String?) {
val params = arrayOf(
"--backend", "IMC",
"--input-type", "C",
"--input", javaClass.getResource(filePath)!!.path,
"--stacktrace",
"--debug"
)
main(params)
}

}
2 changes: 1 addition & 1 deletion subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ private void run() {
sw.stop();
} else if (algorithm.equals(Algorithm.IMC)) {
var transFunc = XstsToMonoliticTransFunc.create(xsts);
var checker = new ImcChecker<XstsState<ExplState>, XstsAction>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars(), true);
var checker = new ImcChecker<XstsState<ExplState>, XstsAction>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars());
status = checker.check(null);
logger.write(Logger.Level.RESULT, "%s%n", status);
sw.stop();
Expand Down

0 comments on commit 9db1fda

Please sign in to comment.