Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/emergent-2025' into emergent-2025
Browse files Browse the repository at this point in the history
  • Loading branch information
@mondokm
mondokm committed Nov 7, 2024
2 parents deae12f + f155e8b commit 6b0aff3
Show file tree
Hide file tree
Showing 10 changed files with 213 additions and 129 deletions.
6 changes: 5 additions & 1 deletion ...cts/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,11 @@ fun CFA.toMonolithicExpr(): MonolithicExpr {
for ((i, x) in this.locs.withIndex()) {
map[x] = i
}
val locVar = Decls.Var("__loc__", Int())
val locVar =
Decls.Var(
"__loc__",
Int(),
) // TODO: add edge var as well, to avoid parallel edges causing problems
val tranList =
this.edges
.map { e ->
Expand Down
12 changes: 8 additions & 4 deletions ...lysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,23 +53,26 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
}

var indexingBuilder = VarIndexingFactory.indexingBuilder(1)
this.vars./*filter { it !in ctrlVars }.*/ forEach { decl ->
repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) }
}
this.vars
.filter { it !in ctrlVars }
.forEach { decl ->
repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) }
}

return MonolithicExpr(
initExpr = And(And(lambdaList), initExpr),
transExpr = And(And(lambdaList), And(lambdaPrimeList), transExpr),
propExpr = Not(And(And(lambdaList), Not(propExpr))),
transOffsetIndex = indexingBuilder.build(),
initOffsetIndex = VarIndexingFactory.indexing(0),
vars = activationLiterals /* + ctrlVars*/,
vars = activationLiterals + ctrlVars,
valToState = { valuation: Valuation ->
PredState.of(
valuation
.toMap()
.entries
.stream()
.filter { it.key !in ctrlVars }
.map {
when ((it.value as BoolLitExpr).value) {
true -> literalToPred[it.key]
Expand All @@ -80,5 +83,6 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
)
},
biValToAction = this.biValToAction,
ctrlVars = ctrlVars,
)
}
47 changes: 13 additions & 34 deletions ...src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
*/
package hu.bme.mit.theta.analysis.algorithm.bounded;

import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not;
import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;

import com.google.common.base.Preconditions;
import hu.bme.mit.theta.analysis.*;
Expand All @@ -31,16 +31,12 @@
import hu.bme.mit.theta.analysis.pred.PredPrec;
import hu.bme.mit.theta.analysis.unit.UnitPrec;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.core.model.Valuation;
import hu.bme.mit.theta.solver.SolverFactory;
import java.util.ArrayList;
import java.util.List;
import java.util.function.BiFunction;
import java.util.function.Function;

public class MonolithicExprCegarChecker<
W extends Proof, S extends ExprState, A extends ExprAction, P extends Prec>
implements SafetyChecker<W, Trace<S, A>, PredPrec> {
public class MonolithicExprCegarChecker<W extends Proof>
implements SafetyChecker<W, Trace<? extends ExprState, ? extends ExprAction>, PredPrec> {
private final MonolithicExpr model;
private final Function<
MonolithicExpr,
Expand All @@ -50,9 +46,6 @@ public class MonolithicExprCegarChecker<
UnitPrec>>
checkerFactory;

private final Function<Valuation, S> valToState;
private final BiFunction<Valuation, Valuation, A> biValToAction;

private final SolverFactory solverFactory;

private final Logger logger;
Expand All @@ -66,32 +59,31 @@ public MonolithicExprCegarChecker(
? extends Trace<? extends ExprState, ? extends ExprAction>,
UnitPrec>>
checkerFactory,
Function<Valuation, S> valToState,
BiFunction<Valuation, Valuation, A> biValToAction,
Logger logger,
SolverFactory solverFactory) {
this.model = model;
this.checkerFactory = checkerFactory;
this.valToState = valToState;
this.biValToAction = biValToAction;
this.logger = logger;
this.solverFactory = solverFactory;
}

public SafetyResult<W, Trace<S, A>> check(PredPrec initPrec) {
public SafetyResult<W, Trace<? extends ExprState, ? extends ExprAction>> check(
PredPrec initPrec) {
var predPrec =
initPrec == null
? PredPrec.of(List.of(model.getInitExpr(), model.getPropExpr()))
: initPrec;

while (true) {
logger.write(Logger.Level.SUBSTEP, "Current prec: %s\n", predPrec);

final var abstractMonolithicExpr =
AbstractMonolithicExprKt.createAbstract(model, predPrec);
final var checker = checkerFactory.apply(abstractMonolithicExpr);

final var result = checker.check();
if (result.isSafe()) {
logger.write(Logger.Level.INFO, "Model is safe, stopping CEGAR");
logger.write(Logger.Level.MAINSTEP, "Model is safe, stopping CEGAR");
return SafetyResult.safe(result.getProof());
} else {
Preconditions.checkState(result.isUnsafe());
Expand All @@ -100,35 +92,22 @@ public SafetyResult<W, Trace<S, A>> check(PredPrec initPrec) {

final ExprTraceChecker<ItpRefutation> exprTraceFwBinItpChecker =
ExprTraceFwBinItpChecker.create(
model.getInitExpr(),
Not(model.getPropExpr()),
solverFactory.createItpSolver());
True(), True(), solverFactory.createItpSolver());

if (trace != null) {
logger.write(Logger.Level.VERBOSE, "\tFound trace: %s\n", trace);
final ExprTraceStatus<ItpRefutation> concretizationResult =
exprTraceFwBinItpChecker.check(trace);
if (concretizationResult.isFeasible()) {
logger.write(Logger.Level.INFO, "Model is unsafe, stopping CEGAR");

final var valTrace = concretizationResult.asFeasible().getValuations();
Valuation lastValuation = null;
final ArrayList<S> states = new ArrayList<>();
final ArrayList<A> actions = new ArrayList<>();
for (var val : valTrace.getStates()) {
states.add(valToState.apply(val));
if (lastValuation != null) {
actions.add(biValToAction.apply(lastValuation, val));
}
lastValuation = val;
}
logger.write(Logger.Level.MAINSTEP, "Model is unsafe, stopping CEGAR\n");

return SafetyResult.unsafe(Trace.of(states, actions), result.getProof());
return SafetyResult.unsafe(trace, result.getProof());
} else {
final var ref = concretizationResult.asInfeasible().getRefutation();
final var newPred = ref.get(ref.getPruneIndex());
final var newPrec = PredPrec.of(newPred);
predPrec = predPrec.join(newPrec);
logger.write(Logger.Level.INFO, "Added new predicate " + newPrec);
logger.write(Logger.Level.INFO, "Added new predicate " + newPrec + "\n");
}
}
}
Expand Down
8 changes: 4 additions & 4 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 @@ -481,6 +481,10 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) {
ctx.declaration().declarationSpecifiers(),
ctx.declaration().initDeclaratorList());
CCompound compound = new CCompound(parseContext);
final var preCompound = new CCompound(parseContext);
final var postCompound = new CCompound(parseContext);
compound.setPreStatements(preCompound);
compound.setPostStatements(postCompound);
for (CDeclaration declaration : declarations) {
if (declaration.getInitExpr() != null) {
createVars(declaration);
Expand Down Expand Up @@ -546,16 +550,12 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) {
recordMetadata(ctx, cAssignment);
compound.getcStatementList().add(cAssignment);
if (declaration.getInitExpr() instanceof CCompound compoundInitExpr) {
final var preCompound = new CCompound(parseContext);
final var postCompound = new CCompound(parseContext);
final var preStatements = collectPreStatements(compoundInitExpr);
preCompound.getcStatementList().addAll(preStatements);
final var postStatements = collectPostStatements(compoundInitExpr);
postCompound.getcStatementList().addAll(postStatements);
resetPreStatements(compoundInitExpr);
resetPostStatements(compoundInitExpr);
compound.setPreStatements(preCompound);
compound.setPostStatements(postCompound);
}
}
}
Expand Down
12 changes: 12 additions & 0 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,18 @@ constructor(
val bottom: Boolean = false,
) : ExprState {

constructor(
xcfa: XCFA,
loc: XcfaLocation,
state: S,
) : this(
xcfa = xcfa,
processes =
mapOf(Pair(0, XcfaProcessState(locs = LinkedList(listOf(loc)), varLookup = LinkedList()))),
state,
mutexes = emptyMap(),
)

override fun isBottom(): Boolean {
return bottom || sGlobal.isBottom
}
Expand Down
Loading

0 comments on commit 6b0aff3

Please sign in to comment.