Skip to content

Commit af0ce42

Browse files
mondokmmondokm
committed
Add EXPL_PRED_COMBINED to xcfa cli
1 parent 9f9683b commit af0ce42

File tree

4 files changed

+119
-14
lines changed

4 files changed

+119
-14
lines changed

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/autoexpl/NewOperandsAutoExpl.java‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@
1515
*/
1616
package hu.bme.mit.theta.analysis.expr.refinement.autoexpl;
1717

18+
import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
19+
1820
import hu.bme.mit.theta.common.container.Containers;
1921
import hu.bme.mit.theta.core.decl.Decl;
2022
import hu.bme.mit.theta.core.decl.VarDecl;
@@ -99,15 +101,20 @@ public void update(Expr<BoolType> itp) {
99101
}));
100102
});
101103

104+
explVars.addAll(
105+
ExprUtils.getVars(itp).stream()
106+
.filter(
107+
decl ->
108+
newOperands
109+
.computeIfAbsent(
110+
decl,
111+
d -> Containers.createSet())
112+
.size()
113+
> newOperandsLimit
114+
|| decl.getType() == Bool())
115+
.collect(Collectors.toSet()));
102116
// explVars.addAll(
103-
// ExprUtils.getVars(itp).stream()
104-
// .filter(
105-
// decl ->
106-
// newOperands.computeIfAbsent(decl, d ->
107-
// Containers.createSet()).size()
108-
// > newOperandsLimit
109-
// || decl.getType() == Bool())
110-
// .collect(Collectors.toSet()));
117+
// ExprUtils.getVars(itp));
111118

112119
cache.add(itp);
113120
}

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredAbstractors.java‎

Lines changed: 88 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -40,12 +40,7 @@
4040
import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
4141
import hu.bme.mit.theta.solver.Solver;
4242
import hu.bme.mit.theta.solver.utils.WithPushPop;
43-
import java.util.ArrayList;
44-
import java.util.Collection;
45-
import java.util.LinkedList;
46-
import java.util.List;
47-
import java.util.Optional;
48-
import java.util.Set;
43+
import java.util.*;
4944
import java.util.function.Function;
5045
import java.util.stream.Collectors;
5146

@@ -68,6 +63,9 @@ public static BooleanAbstractor booleanAbstractor(final Solver solver) {
6863
return new BooleanAbstractor(solver, false);
6964
}
7065

66+
/*
67+
* PRED_SPLIT-like combined abstractor, which returns a separate state for each satisfying assignment
68+
*/
7169
private static final class BooleanAbstractor implements Prod2ExplPredAbstractor {
7270

7371
private final Solver solver;
@@ -160,4 +158,88 @@ private void generateActivationLiterals(final int n) {
160158
}
161159
}
162160
}
161+
162+
/*
163+
* PRED_CART-like combined abstractor, which returns a single abstract state and behaves similarly to maxenum=1 for explicitly tracked values
164+
*/
165+
private static final class CartesianAbstractor implements Prod2ExplPredAbstractor {
166+
167+
private final Solver solver;
168+
169+
public CartesianAbstractor(final Solver solver) {
170+
this.solver = solver;
171+
}
172+
173+
@Override
174+
public Collection<Prod2State<ExplState, PredState>> createStatesForExpr(
175+
final Expr<BoolType> expr,
176+
final VarIndexing exprIndexing,
177+
final Prod2Prec<ExplPrec, PredPrec> prec,
178+
final VarIndexing precIndexing,
179+
final Function<? super Valuation, ? extends ExplState> valuationToState,
180+
final int limit) {
181+
final List<Expr<BoolType>> newStatePreds = new ArrayList<>();
182+
183+
try (WithPushPop wp = new WithPushPop(solver)) {
184+
solver.add(PathUtils.unfold(expr, exprIndexing));
185+
solver.check();
186+
if (solver.getStatus().isUnsat()) {
187+
return Collections.emptySet();
188+
}
189+
190+
final var predPrec = prec.getPrec2();
191+
192+
for (final Expr<BoolType> pred : predPrec.getPreds()) {
193+
final boolean ponEntailed;
194+
final boolean negEntailed;
195+
try (WithPushPop wp1 = new WithPushPop(solver)) {
196+
solver.add(PathUtils.unfold(predPrec.negate(pred), precIndexing));
197+
ponEntailed = solver.check().isUnsat();
198+
}
199+
try (WithPushPop wp2 = new WithPushPop(solver)) {
200+
solver.add(PathUtils.unfold(pred, precIndexing));
201+
negEntailed = solver.check().isUnsat();
202+
}
203+
204+
assert !(ponEntailed && negEntailed)
205+
: "Ponated and negated predicates are both entailed.";
206+
207+
if (ponEntailed) {
208+
newStatePreds.add(pred);
209+
}
210+
if (negEntailed) {
211+
newStatePreds.add(predPrec.negate(pred));
212+
}
213+
}
214+
}
215+
216+
return Collections.singleton(
217+
Prod2State.of(ExplState.top(), PredState.of(newStatePreds)));
218+
}
219+
220+
// @Override
221+
// public Collection<Prod2State<ExplState, PredState>> createStatesForExpr(
222+
// final Expr<BoolType> expr,
223+
// final VarIndexing exprIndexing,
224+
// final PredPrec prec,
225+
// final VarIndexing precIndexing,
226+
// final Prod2State<ExplState, PredState> state,
227+
// final ExprAction action) {
228+
// var actionExpr = action.toExpr();
229+
// if (actionExpr.equals(True())) {
230+
// var filteredPreds =
231+
// state.getPreds().stream()
232+
// .filter(
233+
// p -> {
234+
// var vars = ExprUtils.getVars(p);
235+
// var indexing = action.nextIndexing();
236+
// return vars.stream()
237+
// .allMatch(v -> indexing.get(v) == 0);
238+
// })
239+
// .collect(Collectors.toList());
240+
// return Collections.singleton(PredState.of(filteredPreds));
241+
// }
242+
// return createStatesForExpr(expr, exprIndexing, prec, precIndexing);
243+
// }
244+
}
163245
}

‎subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.analysis
1818
import hu.bme.mit.theta.analysis.expl.ExplState
1919
import hu.bme.mit.theta.analysis.expr.ExprState
2020
import hu.bme.mit.theta.analysis.pred.PredState
21+
import hu.bme.mit.theta.analysis.prod2.Prod2State
2122
import hu.bme.mit.theta.analysis.ptr.PtrState
2223
import hu.bme.mit.theta.core.decl.Decl
2324
import hu.bme.mit.theta.core.decl.VarDecl
@@ -53,6 +54,8 @@ private fun <S : ExprState> S.getState(varLookup: Map<VarDecl<*>, VarDecl<*>>):
5354
when (this) {
5455
is ExplState -> ExplState.of(getVal().changeVars(varLookup))
5556
is PredState -> PredState.of(preds.map { p -> p.changeVars(varLookup) })
57+
is Prod2State<*, *> ->
58+
Prod2State.of((this.state1 as S).getState(varLookup), (this.state2 as S).getState(varLookup))
5659
is PtrState<*> -> PtrState(innerState.getState(varLookup))
5760
else ->
5861
throw NotImplementedError(

‎subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ import hu.bme.mit.theta.analysis.expr.ExprAction
2929
import hu.bme.mit.theta.analysis.expr.ExprState
3030
import hu.bme.mit.theta.analysis.expr.refinement.*
3131
import hu.bme.mit.theta.analysis.pred.PredState
32+
import hu.bme.mit.theta.analysis.prod2.Prod2State
3233
import hu.bme.mit.theta.analysis.ptr.PtrState
3334
import hu.bme.mit.theta.analysis.runtimemonitor.CexMonitor
3435
import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint
@@ -203,6 +204,18 @@ fun getCegarChecker(
203204
is PredState -> {
204205
PredState.of(s.preds.map { ExprUtils.changeDecls(it, declMap) })
205206
}
207+
is Prod2State<*, *> -> {
208+
if (s.state1.isBottom) ExplState.bottom()
209+
else
210+
Prod2State.of(
211+
ExplState.of((s.state1 as ExplState).`val`.changeVars(declMap)),
212+
PredState.of(
213+
(s.state2 as PredState).preds.map {
214+
ExprUtils.changeDecls(it, declMap)
215+
}
216+
),
217+
)
218+
}
206219
else -> {
207220
error("Unknown state: ${s}")
208221
}

0 commit comments

Comments
 (0)