Skip to content

Commit

Permalink
Added reversed and abstract checkers
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Nov 7, 2024
1 parent c6039f8 commit f155e8b
Show file tree
Hide file tree
Showing 8 changed files with 195 additions and 124 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
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
124 changes: 60 additions & 64 deletions ...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,7 @@ import hu.bme.mit.theta.core.type.Expr
import hu.bme.mit.theta.core.type.LitExpr
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq
import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.core.type.bvtype.BvLitExpr
import hu.bme.mit.theta.core.type.bvtype.BvType
Expand All @@ -48,10 +47,7 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CInt
import hu.bme.mit.theta.xcfa.getFlatLabels
import hu.bme.mit.theta.xcfa.model.StmtLabel
import hu.bme.mit.theta.xcfa.model.XCFA
import hu.bme.mit.theta.xcfa.model.XcfaEdge
import hu.bme.mit.theta.xcfa.model.XcfaLocation
import hu.bme.mit.theta.xcfa.model.*
import java.math.BigInteger
import java.util.*
import org.kframework.mpfr.BigFloat
Expand All @@ -64,7 +60,7 @@ private val LitExpr<*>.value: Int
else -> error("Unknown integer type: $type")
}

fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr {
fun XCFA.toMonolithicExpr(parseContext: ParseContext, initValues: Boolean = false): MonolithicExpr {
val intType = CInt.getUnsignedInt(parseContext).smtType

fun int(value: Int): Expr<*> =
Expand All @@ -83,19 +79,26 @@ fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr {
)
Preconditions.checkArgument(proc.errorLoc.isPresent)

val map = mutableMapOf<XcfaLocation, Int>()
val locMap = mutableMapOf<XcfaLocation, Int>()
for ((i, x) in proc.locs.withIndex()) {
map[x] = i
locMap[x] = i
}
val edgeMap = mutableMapOf<XcfaEdge, Int>()
for ((i, x) in proc.edges.withIndex()) {
edgeMap[x] = i
}
val locVar = Decls.Var("__loc_", intType)
val edgeVar = Decls.Var("__edge_", intType)
val tranList =
proc.edges
.map { (source, target, label): XcfaEdge ->
.map { edge: XcfaEdge ->
val (source, target, label) = edge
SequenceStmt.of(
listOf(
AssumeStmt.of(Eq(locVar.ref, int(map[source]!!))),
AssumeStmt.of(Eq(locVar.ref, int(locMap[source]!!))),
label.toStmt(),
AssignStmt.of(locVar, cast(int(map[target]!!), locVar.type)),
AssignStmt.of(locVar, cast(int(locMap[target]!!), locVar.type)),
AssignStmt.of(edgeVar, cast(int(edgeMap[edge]!!), edgeVar.type)),
)
)
}
Expand All @@ -104,46 +107,55 @@ fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr {
val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0))

val defaultValues =
StmtUtils.getVars(trans)
.map {
when (it.type) {
is IntType -> Eq(it.ref, int(0))
is BoolType -> Eq(it.ref, Bool(false))
is BvType ->
Eq(
it.ref,
BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size),
)
is FpType ->
FpAssign(
it.ref as Expr<FpType>,
FpUtils.bigFloatToFpLitExpr(
BigFloat.zero((it.type as FpType).significand),
it.type as FpType,
),
)
else -> throw IllegalArgumentException("Unsupported type")
if (initValues)
StmtUtils.getVars(trans)
.map {
when (it.type) {
is IntType -> Eq(it.ref, int(0))
is BoolType -> Eq(it.ref, Bool(false))
is BvType ->
Eq(
it.ref,
BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size),
)
is FpType ->
FpAssign(
it.ref as Expr<FpType>,
FpUtils.bigFloatToFpLitExpr(
BigFloat.zero((it.type as FpType).significand),
it.type as FpType,
),
)
else -> throw IllegalArgumentException("Unsupported type")
}
}
}
.toList()
.let { And(it) }
.toList()
.let { And(it) }
else True()

return MonolithicExpr(
initExpr = And(Eq(locVar.ref, int(map[proc.initLoc]!!)), defaultValues),
initExpr =
And(Eq(locVar.ref, int(locMap[proc.initLoc]!!)), Eq(edgeVar.ref, int(-1)), defaultValues),
transExpr = And(transUnfold.exprs),
propExpr = Neq(locVar.ref, int(map[proc.errorLoc.get()]!!)),
propExpr = Neq(locVar.ref, int(locMap[proc.errorLoc.get()]!!)),
transOffsetIndex = transUnfold.indexing,
vars = (StmtUtils.getVars(trans) + listOf(locVar)).toList(),
valToState = { valToState(it) },
biValToAction = { val1, val2 -> valToAction(val1, val2) },
ctrlVars = listOf(locVar, edgeVar),
)
}

fun XCFA.valToAction(val1: Valuation, val2: Valuation): XcfaAction {
val val1Map = val1.toMap()
val val2Map = val2.toMap()
var i = 0
val map: MutableMap<XcfaLocation, Int> = HashMap()
for (x in this.procedures.first { it.name == "main" }.locs) {
map[x] = i++
val proc = this.procedures.first { it.name == "main" }
val locMap = mutableMapOf<XcfaLocation, Int>()
for ((i, x) in proc.locs.withIndex()) {
locMap[x] = i
}
val edgeMap = mutableMapOf<XcfaEdge, Int>()
for ((i, x) in proc.edges.withIndex()) {
edgeMap[x] = i
}
return XcfaAction(
pid = 0,
Expand All @@ -152,34 +164,21 @@ fun XCFA.valToAction(val1: Valuation, val2: Valuation): XcfaAction {
.first { it.name == "main" }
.edges
.first { edge ->
map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }])?.value ?: -1 &&
map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }])?.value ?: -1
edgeMap[edge] == (val2Map[val2Map.keys.first { it.name == "__edge_" }]?.value ?: -1)
},
)
}

fun XCFA.valToState(val1: Valuation): XcfaState<PtrState<ExplState>> {
val valMap = val1.toMap()
var i = 0
val map: MutableMap<Int, XcfaLocation> = HashMap()
for (x in this.procedures.first { it.name == "main" }.locs) {
map[i++] = x
val proc = this.procedures.first { it.name == "main" }
val locMap = mutableMapOf<Int, XcfaLocation>()
for ((i, x) in proc.locs.withIndex()) {
locMap[i] = x
}
return XcfaState(
xcfa = this,
processes =
mapOf(
Pair(
0,
XcfaProcessState(
locs =
LinkedList(
listOf(map[(valMap[valMap.keys.first { it.name == "__loc_" }])?.value ?: -1])
),
varLookup = LinkedList(),
),
)
),
this,
locMap[(valMap[valMap.keys.first { it.name == "__loc_" }])?.value ?: -1]!!,
PtrState(
ExplState.of(
ImmutableValuation.from(
Expand All @@ -191,8 +190,5 @@ fun XCFA.valToState(val1: Valuation): XcfaState<PtrState<ExplState>> {
)
)
),
mutexes = emptyMap(),
threadLookup = emptyMap(),
bottom = false,
)
}
Loading

0 comments on commit f155e8b

Please sign in to comment.