Skip to content

Commit

Permalink
Improve control flow splitting terminology
Browse files Browse the repository at this point in the history
  • Loading branch information
DoriCz committed Nov 20, 2024
1 parent 5564c0e commit f54c953
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 94 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -29,42 +29,43 @@ public class ControlFlowSplitUtil {
private ControlFlowSplitUtil() {
}

public static ControlFlowSplitResult splitCF(final Stmt stmt) {
public static ControlFlowSplitResult splitControlFlows(final Stmt stmt) {

final List<VarDecl<BoolType>> flags = new ArrayList<>();
final List<Expr<BoolType>> flagConstraints = new ArrayList<>();
final List<Expr<BoolType>> controlFlowConstraints = new ArrayList<>();

final ControlFlowFlagsHelper helper = new ControlFlowFlagsHelper(flags, flagConstraints);
final Stmt flaggedStmt = helper.flagStmt(stmt);
final ControlFlowEncodingHelper helper = new ControlFlowEncodingHelper(flags, controlFlowConstraints);
final Stmt flaggedStmt = helper.encodeControlFlows(stmt);

for (final VarDecl<BoolType> flag : Lists.reverse(flags)) {
VarPoolUtil.returnBool(flag);
}

return ControlFlowSplitResult.of(flaggedStmt, flags, flagConstraints);
return ControlFlowSplitResult.of(flaggedStmt, flags, controlFlowConstraints);
}

private static final class ControlFlowFlagsHelper implements StmtVisitor<VarDecl<BoolType>, Stmt> {
private static final class ControlFlowEncodingHelper implements StmtVisitor<VarDecl<BoolType>, Stmt> {

private final List<VarDecl<BoolType>> flags;
private final List<Expr<BoolType>> flagConstraints;
private final List<Expr<BoolType>> controlFlowConstraints;
private final AssumeTransformationHelper assumeHelper;

private ControlFlowFlagsHelper(final List<VarDecl<BoolType>> flags, final List<Expr<BoolType>> flagConstraints) {
private ControlFlowEncodingHelper(final List<VarDecl<BoolType>> flags,
final List<Expr<BoolType>> controlFlowConstraints) {
this.flags = flags;
this.flagConstraints = flagConstraints;
this.controlFlowConstraints = controlFlowConstraints;
assumeHelper = new AssumeTransformationHelper();
}

public Stmt flagStmt(final Stmt stmt) {
public Stmt encodeControlFlows(final Stmt stmt) {
final VarDecl<BoolType> root = VarPoolUtil.requestBool();
flags.add(root);
flagConstraints.add(root.getRef());
controlFlowConstraints.add(root.getRef());

final Stmt flaggedStmt = stmt.accept(this, root);
final AssumeStmt flagConstraintsAssume = Stmts.Assume(And(flagConstraints));
final Stmt transformedStmt = stmt.accept(this, root);
final AssumeStmt controlFlowAssumptions = Stmts.Assume(And(controlFlowConstraints));

return Stmts.SequenceStmt(List.of(flaggedStmt, flagConstraintsAssume));
return Stmts.SequenceStmt(List.of(transformedStmt, controlFlowAssumptions));
}

@Override
Expand Down Expand Up @@ -105,10 +106,10 @@ public <DeclType extends Type> Stmt visit(HavocStmt<DeclType> stmt, VarDecl<Bool

@Override
public Stmt visit(SequenceStmt stmt, VarDecl<BoolType> parent) {
final List<Stmt> flaggedSubStmts = stmt.getStmts().stream()
final List<Stmt> transformedSubStmts = stmt.getStmts().stream()
.map(subStmt -> subStmt.accept(this, parent))
.toList();
return SequenceStmt(flaggedSubStmts);
return SequenceStmt(transformedSubStmts);
}

@Override
Expand All @@ -125,17 +126,17 @@ public Stmt visit(NonDetStmt stmt, VarDecl<BoolType> parent) {
}

final List<VarDecl<BoolType>> localFlags = new ArrayList<>(branchCnt);
final List<Stmt> flaggedBranches = new ArrayList<>(branchCnt);
final List<Stmt> transformedBranches = new ArrayList<>(branchCnt);

for (final Stmt branch : branches) {
final VarDecl<BoolType> flag = VarPoolUtil.requestBool();
localFlags.add(flag);
flags.add(flag);
flagConstraints.add(Imply(Not(parent.getRef()), Not(flag.getRef())));
controlFlowConstraints.add(Imply(Not(parent.getRef()), Not(flag.getRef())));

final Stmt flaggedBranchBody = branch.accept(this, flag);
final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody);
flaggedBranches.add(flaggedBranch);
final Stmt transformedBranchBody = branch.accept(this, flag);
final IfStmt transformedBranch = IfStmt(flag.getRef(), transformedBranchBody);
transformedBranches.add(transformedBranch);
}

final List<Expr<BoolType>> branchExprs = new ArrayList<>();
Expand All @@ -147,9 +148,9 @@ public Stmt visit(NonDetStmt stmt, VarDecl<BoolType> parent) {
}
branchExprs.add(And(flagsForCurrentBranch));
}
flagConstraints.add(Imply(parent.getRef(), Or(branchExprs)));
controlFlowConstraints.add(Imply(parent.getRef(), Or(branchExprs)));

return SequenceStmt(flaggedBranches);
return SequenceStmt(transformedBranches);
}

@Override
Expand All @@ -173,7 +174,7 @@ public Stmt visit(IfStmt stmt, VarDecl<BoolType> parent) {
condToBranch.put(Not(stmt.getCond()), stmt.getElze());

final List<VarDecl<BoolType>> localFlags = new ArrayList<>(2);
final List<Stmt> flaggedBranches = new ArrayList<>(2);
final List<Stmt> transformedBranches = new ArrayList<>(2);

for (final Map.Entry<Expr<BoolType>, Stmt> branch : condToBranch.entrySet()) {
final VarDecl<BoolType> flag = VarPoolUtil.requestBool();
Expand All @@ -183,20 +184,20 @@ public Stmt visit(IfStmt stmt, VarDecl<BoolType> parent) {
final Expr<BoolType> cond = branch.getKey();
final Stmt branchBody = branch.getValue();
final Stmt newBranchBody = SequenceStmt(List.of(Assume(cond), branchBody));
final Stmt flaggedBranchBody = newBranchBody.accept(this, flag);
final Stmt transformedBranchBody = newBranchBody.accept(this, flag);

final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody);
flaggedBranches.add(flaggedBranch);
final IfStmt transformedBranch = IfStmt(flag.getRef(), transformedBranchBody);
transformedBranches.add(transformedBranch);
}

final Expr<BoolType> p = parent.getRef();
final Expr<BoolType> b1 = localFlags.get(0).getRef();
final Expr<BoolType> b2 = localFlags.get(1).getRef();
flagConstraints.add(Imply(p, Xor(b1, b2)));
flagConstraints.add(Imply(Not(p), Not(b1)));
flagConstraints.add(Imply(Not(p), Not(b2)));
controlFlowConstraints.add(Imply(p, Xor(b1, b2)));
controlFlowConstraints.add(Imply(Not(p), Not(b1)));
controlFlowConstraints.add(Imply(Not(p), Not(b2)));

return SequenceStmt(flaggedBranches);
return SequenceStmt(transformedBranches);
}

@Override
Expand Down Expand Up @@ -238,20 +239,20 @@ private Stmt transformAssume(final Expr<BoolType> cond, final VarDecl<BoolType>
private Stmt transformAnd(final AndExpr andExpr, final VarDecl<BoolType> parent) {
final List<Stmt> assumes = andExpr.getOps().stream().map(Stmts::Assume).collect(toList());
final Stmt transformed = SequenceStmt(assumes);
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformOr(final OrExpr orExpr, final VarDecl<BoolType> parent) {
final List<Stmt> assumes = orExpr.getOps().stream().map(Stmts::Assume).collect(toList());
final Stmt transformed = NonDetStmt(assumes);
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformImply(final ImplyExpr implyExpr, final VarDecl<BoolType> parent) {
final Expr<BoolType> a = implyExpr.getLeftOp();
final Expr<BoolType> b = implyExpr.getRightOp();
final Stmt transformed = Assume(Or(Not(a), b));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformIff(final IffExpr iffExpr, final VarDecl<BoolType> parent) {
Expand All @@ -260,7 +261,7 @@ private Stmt transformIff(final IffExpr iffExpr, final VarDecl<BoolType> parent)
final Expr<BoolType> imply1 = Or(Not(a), b);
final Expr<BoolType> imply2 = Or(Not(b), a);
final Stmt transformed = Assume(And(imply1, imply2));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformXor(final XorExpr xorExpr, final VarDecl<BoolType> parent) {
Expand All @@ -269,7 +270,7 @@ private Stmt transformXor(final XorExpr xorExpr, final VarDecl<BoolType> parent)
final Expr<BoolType> case1 = And(Not(a), b);
final Expr<BoolType> case2 = And(a, Not(b));
final Stmt transformed = Assume(Or(case1, case2));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNot(final NotExpr notExpr, final VarDecl<BoolType> parent) {
Expand Down Expand Up @@ -312,26 +313,26 @@ private Stmt transformNegatedClockConstraint(final ClockConstraintExpr negatedCl

private Stmt transformNegatedNot(final NotExpr negatedNotExpr, final VarDecl<BoolType> parent) {
final Stmt transformed = Assume(negatedNotExpr.getOp());
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedAnd(final AndExpr negatedAndExpr, final VarDecl<BoolType> parent) {
final List<NotExpr> negatedOps = negatedAndExpr.getOps().stream().map(BoolExprs::Not).toList();
final Stmt transformed = Assume(Or(negatedOps));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedOr(final OrExpr negatedOrExpr, final VarDecl<BoolType> parent) {
final List<NotExpr> negatedOps = negatedOrExpr.getOps().stream().map(BoolExprs::Not).toList();
final Stmt transformed = Assume(And(negatedOps));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedImply(final ImplyExpr negatedImplyExpr, final VarDecl<BoolType> parent) {
final Expr<BoolType> a = negatedImplyExpr.getLeftOp();
final Expr<BoolType> b = negatedImplyExpr.getRightOp();
final Stmt transformed = Assume(And(a, Not(b)));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedIff(final IffExpr negatedIffExpr, final VarDecl<BoolType> parent) {
Expand All @@ -340,7 +341,7 @@ private Stmt transformNegatedIff(final IffExpr negatedIffExpr, final VarDecl<Boo
final Expr<BoolType> notImply1 = And(a, Not(b));
final Expr<BoolType> notImply2 = And(b, Not(a));
final Stmt transformed = Assume(Or(notImply1, notImply2));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedXor(final XorExpr negatedXorExpr, final VarDecl<BoolType> parent) {
Expand All @@ -349,21 +350,21 @@ private Stmt transformNegatedXor(final XorExpr negatedXorExpr, final VarDecl<Boo
final Expr<BoolType> same1 = And(a, b);
final Expr<BoolType> same2 = And(Not(a), Not(b));
final Stmt transformed = Assume(Or(same1, same2));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedExists(final ExistsExpr negatedExistsExpr, final VarDecl<BoolType> parent) {
final List<ParamDecl<?>> params = negatedExistsExpr.getParamDecls();
final Expr<BoolType> op = negatedExistsExpr.getOp();
final Stmt transformed = Assume(Forall(params, Not(op)));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}

private Stmt transformNegatedForall(final ForallExpr negatedForallExpr, final VarDecl<BoolType> parent) {
final List<ParamDecl<?>> params = negatedForallExpr.getParamDecls();
final Expr<BoolType> op = negatedForallExpr.getOp();
final Stmt transformed = Assume(Exists(params, Not(op)));
return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent);
return transformed.accept(ControlFlowEncodingHelper.this, parent);
}
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ public class ControlFlowSplitXstsLts<S extends ExprState> implements LTS<XstsSta

private ControlFlowSplitResult cfSplitResult;
private ExprState lastState;
private boolean stmtInSolver;

private ControlFlowSplitXstsLts(final XSTS xsts, final Solver solver, final ValuationExtractor<S> valExtractor) {
this.solver = solver;
Expand Down Expand Up @@ -76,49 +75,46 @@ public static <S extends ExprState> ControlFlowSplitXstsLts<S> create(final XSTS
@Override
public Collection<XstsAction> getEnabledActionsFor(XstsState<S> state) {
reset();
splitCF(state);
return getEnabledActions();
}

public Collection<XstsAction> getEnabledActionsFor(XstsState<S> state, ExprState abstrState) {
reset();
splitCF(state);
filterCF(abstrState);
return getEnabledActions();
splitControlFlows(state, false);
final List<XstsAction> actions = new ArrayList<>();
Optional<XstsAction> action = getNextEnabledAction();
while (action.isPresent()) {
actions.add(action.get());
action = getNextEnabledAction();
}
return actions;
}

public void reset() {
if (!solver.getAssertions().isEmpty()) {
solver.pop();
}
lastState = null;
stmtInSolver = false;
}

public void splitCF(final XstsState<S> state) {
final Stmt xstsStep;
if (!state.isInitialized()) xstsStep = init;
else if (state.lastActionWasEnv()) xstsStep = tran;
else xstsStep = env;
public void splitControlFlows(final XstsState<S> state, final boolean feasibleOnly) {
final Stmt enabledSet;
if (!state.isInitialized()) enabledSet = init;
else if (state.lastActionWasEnv()) enabledSet = tran;
else enabledSet = env;

final Valuation ctrlVal = valExtractor.extractValuationForVars(state.getState(), ctrlVars);
final Stmt simplifiedStmt = StmtSimplifier.simplifyStmt(ctrlVal, xstsStep);
cfSplitResult = cfSplitCache.computeIfAbsent(simplifiedStmt, ControlFlowSplitUtil::splitCF);
final Stmt simplifiedStmt = StmtSimplifier.simplifyStmt(ctrlVal, enabledSet);
cfSplitResult = cfSplitCache.computeIfAbsent(simplifiedStmt, ControlFlowSplitUtil::splitControlFlows);

solver.push();
solver.add(cfSplitResult.getIndexedFlagConstraintExpr());
if (feasibleOnly) {
final Stmt stmtWithoutClocks = stmtClockTransformer.apply(cfSplitResult.getFlaggedStmt());
StmtUtils.toExpr(stmtWithoutClocks, VarIndexingFactory.indexing(0)).getExprs()
.forEach(expr -> solver.add(PathUtils.unfold(expr, 0)));
}
}

public void filterCF(final ExprState state) {
public void updateSourceAbstractState(final ExprState state) {
if (state != lastState) {
solver.add(PathUtils.unfold(state.toExpr(), 0));
}
if (!stmtInSolver) {
final Stmt stmtWithoutClocks = stmtClockTransformer.apply(cfSplitResult.getFlaggedStmt());
StmtUtils.toExpr(stmtWithoutClocks, VarIndexingFactory.indexing(0)).getExprs()
.forEach(expr -> solver.add(PathUtils.unfold(expr, 0)));
stmtInSolver = true;
}
}

public Optional<XstsAction> getNextEnabledAction() {
Expand Down Expand Up @@ -152,14 +148,4 @@ public Optional<XstsAction> getNextEnabledAction() {
return Optional.empty();
}
}

private Collection<XstsAction> getEnabledActions() {
final List<XstsAction> actions = new ArrayList<>();
Optional<XstsAction> action = getNextEnabledAction();
while (action.isPresent()) {
actions.add(action.get());
action = getNextEnabledAction();
}
return actions;
}
}
Loading

0 comments on commit f54c953

Please sign in to comment.