diff --git a/build.gradle.kts b/build.gradle.kts index 8da5a5b750..194a9d5eab 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "2.3.0" + version = "2.4.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java index dfafbfacfb..6b4da0808c 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java @@ -18,6 +18,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; @@ -43,4 +44,8 @@ public boolean isBottom() { return expr.equals(False()); } + @Override + public String toString() { + return Utils.lispStringBuilder(getClass().getSimpleName()).body().add(expr).toString(); + } } diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java index 5e43da9a8a..844a5f596c 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java @@ -33,7 +33,7 @@ public final class ExprTraceUtils { private ExprTraceUtils() { } - public static Trace traceFrom(final List actions) { + public static Trace traceFrom(final List actions) { checkNotNull(actions); final List states = new ArrayList<>(actions.size() + 1); for (int i = 0; i < actions.size() + 1; i++) { diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java new file mode 100644 index 0000000000..92b187b8c3 --- /dev/null +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java @@ -0,0 +1,669 @@ +package hu.bme.mit.theta.analysis.expr.refinement; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.Lists; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.ExprTraceUtils; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.BasicSubstitution; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.stmt.AssignStmt; +import hu.bme.mit.theta.core.stmt.AssumeStmt; +import hu.bme.mit.theta.core.stmt.HavocStmt; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.OrtStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; +import hu.bme.mit.theta.core.stmt.SkipStmt; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.stmt.StmtVisitor; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.ExprSimplifier; +import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.core.utils.PathUtils; +import hu.bme.mit.theta.core.utils.SpState; +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.VarIndexing; +import hu.bme.mit.theta.core.utils.WpState; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.utils.WithPushPop; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import java.util.stream.Stream; + +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static java.util.stream.Collectors.toList; +import static java.util.stream.Collectors.toUnmodifiableMap; + +/** + * An ExprTraceChecker that generates new predicates based on the Newton-style algorithms described in + * Daniel Dietsch, Matthias Heizmann, Betim Musa, Alexander Nutz, and Andreas Podelski. 2017. + * Craig vs. Newton in software model checking. In Proceedings of the 2017 11th Joint Meeting on Foundations + * of Software Engineering (ESEC/FSE 2017). Association for Computing Machinery, New York, NY, USA, + * 487–497. DOI:https://doi.org/10.1145/3106237.3106307 + */ +public class ExprTraceNewtonChecker implements ExprTraceChecker { + private enum AssertionGeneratorMethod { SP, WP } + + private final Solver solver; + private final Expr init; + private final Expr target; + + private final boolean IT; // Whether to abstract the trace or not + private final AssertionGeneratorMethod SPorWP; // Whether to use pre- or postconditions + private final boolean LV; // Whether to project the assertions to live variables + + private ExprTraceNewtonChecker( + final Expr init, final Expr target, final Solver solver, + boolean it, AssertionGeneratorMethod sPorWP, boolean lv + ) { + this.solver = checkNotNull(solver); + this.init = checkNotNull(init); + this.target = checkNotNull(target); + this.IT = it; + this.SPorWP = checkNotNull(sPorWP); + this.LV = lv; + } + + public static ExprTraceNewtonCheckerITBuilder create( + final Expr init, final Expr target, final Solver solver + ) { + return new ExprTraceNewtonCheckerITBuilder(solver, init, target); + } + + @SuppressWarnings("unchecked") + @Override + public ExprTraceStatus check(final Trace trace) { + checkNotNull(trace); + try { + return check2((Trace) trace); + } + catch(ClassCastException e) { + throw new UnsupportedOperationException("Actions must be of type StmtAction", e); + } + } + + private ExprTraceStatus check2(final Trace trace) { + var ftrace = flattenTrace(trace); // Moves the expressions in the states to the corresponting actions as assumptions + + final int stateCount = ftrace.getStates().size(); + final List indexings = new ArrayList<>(stateCount); + indexings.add(VarIndexing.all(0)); + + final Valuation model; + final Collection> unsatCore; + final boolean concretizable; + + try (WithPushPop wpp = new WithPushPop(solver)) { + for (int i = 1; i < stateCount; ++i) { + var curIndexing = indexings.get(i - 1); + for(var stmt : ftrace.getAction(i - 1).getStmts()) { + var stmtUnfoldResult = StmtUtils.toExpr(stmt, VarIndexing.all(0)); + solver.track(PathUtils.unfold(stmtUnfoldResult.getExprs().iterator().next(), curIndexing)); + curIndexing = curIndexing.add(stmtUnfoldResult.getIndexing()); + } + indexings.add(curIndexing); + } + + concretizable = solver.check().isSat(); + + if (concretizable) { + model = solver.getModel(); + unsatCore = null; + } else { + model = null; + unsatCore = solver.getUnsatCore(); + } + } + + if (concretizable) { + checkNotNull(model); + return createCounterexample(model, indexings, trace); + } else { + checkNotNull(unsatCore); + return createRefinement(unsatCore, indexings, ftrace); + } + } + + @Override + public String toString() { + return getClass().getSimpleName(); + } + + private Trace flattenTrace(final Trace trace) { + final var stateCount = trace.getStates().size(); + final var flattenedActions = new ArrayList(stateCount - 1); + + for(var i = 1; i < stateCount; i++) { + var initStream = + (i == 1) + ? ExprUtils.getConjuncts(init).stream().map(AssumeStmt::of) + : Stream.empty(); + + var stateStream = ExprUtils.getConjuncts(trace.getState(i - 1).toExpr()).stream().map(AssumeStmt::of); + + var actionStream = trace.getAction(i - 1).getStmts().stream(); + + var targetStream = + (i == stateCount - 1) + ? Stream.concat( + ExprUtils.getConjuncts(trace.getState(i).toExpr()).stream().map(AssumeStmt::of), + ExprUtils.getConjuncts(target).stream().map(AssumeStmt::of) + ) + : Stream.empty(); + + flattenedActions.add( + NewtonAction.of( + Stream.of(initStream, stateStream, actionStream, targetStream).flatMap(e -> e).collect(toList()) + ) + ); + } + + return ExprTraceUtils.traceFrom(flattenedActions); + } + + private ExprTraceStatus.Feasible createCounterexample( + final Valuation model, + final List indexings, + final Trace trace + ) { + final ImmutableList.Builder builder = ImmutableList.builder(); + for (final VarIndexing indexing : indexings) { + builder.add(PathUtils.extractValuation(model, indexing)); + } + return ExprTraceStatus.feasible(Trace.of(builder.build(), trace.getActions())); + } + + private ExprTraceStatus.Infeasible createRefinement( + final Collection> unsatCore, + final List indexings, + Trace trace + ) { + if(IT) { + trace = computeAbstractTrace(unsatCore, trace); + } + + final List> assertions; + if(SPorWP == AssertionGeneratorMethod.SP) { + assertions = computeAssertionsFromTraceWithStrongestPostcondition(trace); + } + else if(SPorWP == AssertionGeneratorMethod.WP) { + assertions = computeAssertionsFromTraceWithWeakestPrecondition(trace); + } + else { + throw new AssertionError("There should be no other option"); + } + + return ExprTraceStatus.infeasible(ItpRefutation.sequence(assertions)); + } + + /* + * State abstraction + */ + + private Trace computeAbstractTrace( + final Collection> unsatCore, + final Trace trace + ) { + final var stateCount = trace.getStates().size(); + var curIndexing = VarIndexing.all(0); + + final var actions = new ArrayList(); + + for (int i = 1; i < stateCount; ++i) { + final var stmts = new ArrayList(); + for(final var stmt : trace.getAction(i - 1).getStmts()) { + final var stmtUnfoldResult = StmtUtils.toExpr(stmt, VarIndexing.all(0)); + final var stmtExpr = PathUtils.unfold(stmtUnfoldResult.getExprs().iterator().next(), curIndexing); + + if(unsatCore.contains(stmtExpr)) { + stmts.add(stmt); + } + else { + stmts.add(computeAbstractStmt(stmt)); + } + + curIndexing = curIndexing.add(stmtUnfoldResult.getIndexing()); + } + actions.add(NewtonAction.of(stmts)); + } + + return Trace.of(trace.getStates(), actions); + } + + private Stmt computeAbstractStmt(Stmt stmt) { + return stmt.accept(new StmtVisitor() { + @Override + public Stmt visit(SkipStmt stmt, Void param) { + return SkipStmt.getInstance(); + } + + @Override + public Stmt visit(AssumeStmt stmt, Void param) { + return AssumeStmt.of(True()); + } + + @Override + public Stmt visit(AssignStmt stmt, Void param) { + return HavocStmt.of(stmt.getVarDecl()); + } + + @Override + public Stmt visit(HavocStmt stmt, Void param) { + return HavocStmt.of(stmt.getVarDecl()); + } + + @Override + public Stmt visit(SequenceStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Stmt visit(NonDetStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Stmt visit(OrtStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + }, null); + } + + /* + * Assertion computation + */ + + private List> computeAssertionsFromTraceWithStrongestPostcondition( + final Trace trace + ) { + final int stateCount = trace.getStates().size(); + final List> assertions = new ArrayList<>(stateCount); + + assertions.add(True()); + var constCount = 0; + for(var i = 1; i < stateCount; i++) { + var spState = SpState.of(assertions.get(i - 1), constCount); + for(var stmt : trace.getAction(i - 1).getStmts()) { + spState = spState.sp(stmt); + } + assertions.add(ExprSimplifier.simplify(spState.getExpr(), ImmutableValuation.empty())); + constCount = spState.getConstCount(); + } + + if(LV) { + var allVariables = collectVariablesInTrace(trace); + var futureLiveVariables = collectFutureLiveVariablesForTrace(trace); + return IntStream.range(0, assertions.size()) + .mapToObj(i -> existentialProjection(assertions.get(i), futureLiveVariables.get(i), allVariables)) + .collect(Collectors.toUnmodifiableList()); + } + else { + return assertions; + } + } + + private List> computeAssertionsFromTraceWithWeakestPrecondition( + final Trace trace + ) { + final int stateCount = trace.getStates().size(); + final List> assertions = new ArrayList<>(Collections.nCopies(stateCount, null)); + + assertions.set(stateCount - 1, True()); + var constCount = 0; + for(var i = stateCount - 2; i >= 0; i--) { + var wpState = WpState.of(assertions.get(i + 1), constCount); + for(var stmt : Lists.reverse(trace.getAction(i).getStmts())) { + wpState = wpState.wep(stmt); + } + assertions.set(i, ExprSimplifier.simplify(wpState.getExpr(), ImmutableValuation.empty())); + constCount = wpState.getConstCount(); + } + + if(LV) { + var allVariables = collectVariablesInTrace(trace); + var pastLiveVariables = collectPastLiveVariablesForTrace(trace); + return IntStream.range(0, assertions.size()) + .mapToObj(i -> universalProjection(assertions.get(i), pastLiveVariables.get(i), allVariables)) + .collect(Collectors.toUnmodifiableList()); + } + else { + return assertions; + } + } + + /* + * Live variable collection + */ + + private Collection> collectVariablesInTrace(final Trace trace) { + var variables = new HashSet>(); + + for(var state : trace.getStates()) { + ExprUtils.collectVars(state.toExpr(), variables); + } + for(var action : trace.getActions()) { + ExprUtils.collectVars(action.toExpr(), variables); + } + + return variables; + } + + private Collection> stmtReadsVariables(final Stmt stmt) { + return stmt.accept(new StmtVisitor>>() { + @Override + public Collection> visit(SkipStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(AssumeStmt stmt, Void param) { + return ExprUtils.getVars(stmt.getCond()); + } + + @Override + public Collection> visit(AssignStmt stmt, Void param) { + return ExprUtils.getVars(stmt.getExpr()); + } + + @Override + public Collection> visit(HavocStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(SequenceStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(NonDetStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(OrtStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + }, null); + } + + private Collection> stmtWritesVariables(final Stmt stmt) { + return stmt.accept(new StmtVisitor>>() { + @Override + public Collection> visit(SkipStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(AssumeStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(AssignStmt stmt, Void param) { + return Collections.singletonList(stmt.getVarDecl()); + } + + @Override + public Collection> visit(HavocStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(SequenceStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(NonDetStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(OrtStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + }, null); + } + + private Collection> stmtHavocsVariables(final Stmt stmt) { + return stmt.accept(new StmtVisitor>>() { + @Override + public Collection> visit(SkipStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(AssumeStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(AssignStmt stmt, Void param) { + return Collections.emptySet(); + } + + @Override + public Collection> visit(HavocStmt stmt, Void param) { + return Collections.singletonList(stmt.getVarDecl()); + } + + @Override + public Collection> visit(SequenceStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(NonDetStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public Collection> visit(OrtStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + }, null); + } + + private Collection> actionReadsVariables(final StmtAction action) { + return action.getStmts().stream().flatMap(stmt -> stmtReadsVariables(stmt).stream()).collect(Collectors.toUnmodifiableSet()); + } + + private Collection> actionWritesVariables(final StmtAction action) { + return action.getStmts().stream().flatMap(stmt -> stmtWritesVariables(stmt).stream()).collect(Collectors.toUnmodifiableSet()); + } + + private Collection> actionHavocsVariables(final StmtAction action) { + return action.getStmts().stream().flatMap(stmt -> stmtHavocsVariables(stmt).stream()).collect(Collectors.toUnmodifiableSet()); + } + + private List>> collectFutureLiveVariablesForTrace(final Trace trace) { + final var stateCount = trace.getStates().size(); + final var futureLiveVariables = new ArrayList>>(Collections.nCopies(stateCount, null)); + + futureLiveVariables.set(stateCount - 1, Collections.emptySet()); + for(var i = stateCount - 2; i >= 0; i--) { + var vars = new HashSet<>(futureLiveVariables.get(i + 1)); + vars.addAll(actionReadsVariables(trace.getAction(i))); + vars.removeAll(actionWritesVariables(trace.getAction(i))); + vars.removeAll(actionHavocsVariables(trace.getAction(i))); + futureLiveVariables.set(i, vars); + } + + return futureLiveVariables; + } + + private List>> collectPastLiveVariablesForTrace(final Trace trace) { + final var stateCount = trace.getStates().size(); + final var pastLiveVariables = new ArrayList>>(Collections.nCopies(stateCount, null)); + + pastLiveVariables.set(0, Collections.emptySet()); + for(var i = 1; i < stateCount; i++) { + var vars = new HashSet<>(pastLiveVariables.get(i - 1)); + vars.addAll(actionReadsVariables(trace.getAction(i - 1))); + vars.addAll(actionWritesVariables(trace.getAction(i - 1))); + vars.removeAll(actionHavocsVariables(trace.getAction(i - 1))); + pastLiveVariables.set(i, vars); + } + + return pastLiveVariables; + } + + /* + * Projection to live variables + */ + + private Expr existentialProjection( + final Expr expr, + final Collection> variables, + final Collection> allVariables + ) { + var params = allVariables.stream() + .filter(e -> !variables.contains(e)) + .map(e -> Tuple2.of(e, Param(e.getName(), e.getType()))) + .collect(Collectors.toUnmodifiableSet()); + + var substitution = BasicSubstitution.builder() + .putAll(params.stream().collect(toUnmodifiableMap(Tuple2::get1, e -> e.get2().getRef()))) + .build(); + + return params.size() > 0 + ? Exists(params.stream().map(Tuple2::get2).collect(toList()), substitution.apply(expr)) + : expr; + } + + private Expr universalProjection( + final Expr expr, + final Collection> variables, + final Collection> allVariables + ) { + var params = allVariables.stream() + .filter(e -> !variables.contains(e)) + .map(e -> Tuple2.of(e, Param(e.getName(), e.getType()))) + .collect(Collectors.toUnmodifiableSet()); + + var substitution = BasicSubstitution.builder() + .putAll(params.stream().collect(toUnmodifiableMap(Tuple2::get1, e -> e.get2().getRef()))) + .build(); + + return params.size() > 0 + ? Forall(params.stream().map(Tuple2::get2).collect(toList()), substitution.apply(expr)) + : expr; + } + + /* + * Builder for ExprTraceNewtonChecker + */ + + public static class ExprTraceNewtonCheckerITBuilder { + private final Solver solver; + private final Expr init; + private final Expr target; + + public ExprTraceNewtonCheckerITBuilder(Solver solver, Expr init, Expr target) { + this.solver = solver; + this.init = init; + this.target = target; + } + + public ExprTraceNewtonCheckerAssertBuilder withIT() { + return new ExprTraceNewtonCheckerAssertBuilder(solver, init, target, true); + } + + public ExprTraceNewtonCheckerAssertBuilder withoutIT() { + return new ExprTraceNewtonCheckerAssertBuilder(solver, init, target, false); + } + } + + public static class ExprTraceNewtonCheckerAssertBuilder { + private final Solver solver; + private final Expr init; + private final Expr target; + + private final boolean IT; + + public ExprTraceNewtonCheckerAssertBuilder(Solver solver, Expr init, Expr target, boolean it) { + this.solver = solver; + this.init = init; + this.target = target; + this.IT = it; + } + + public ExprTraceNewtonCheckerLVBuilder withSP() { + return new ExprTraceNewtonCheckerLVBuilder(solver, init, target, IT, AssertionGeneratorMethod.SP); + } + + public ExprTraceNewtonCheckerLVBuilder withWP() { + return new ExprTraceNewtonCheckerLVBuilder(solver, init, target, IT, AssertionGeneratorMethod.WP); + } + } + + public static class ExprTraceNewtonCheckerLVBuilder { + private final Solver solver; + private final Expr init; + private final Expr target; + + private final boolean IT; + private final AssertionGeneratorMethod SPorWP; + + public ExprTraceNewtonCheckerLVBuilder(Solver solver, Expr init, Expr target, boolean it, AssertionGeneratorMethod sPorWP) { + this.solver = solver; + this.init = init; + this.target = target; + this.IT = it; + this.SPorWP = sPorWP; + } + + public ExprTraceNewtonChecker withLV() { + return new ExprTraceNewtonChecker(init, target, solver, IT, SPorWP, true); + } + + public ExprTraceNewtonChecker withoutLV() { + return new ExprTraceNewtonChecker(init, target, solver, IT, SPorWP, false); + } + } + + /* + * Custom StmtAction to use when constructing helper traces + */ + + private static class NewtonAction extends StmtAction { + private final List stmts; + + private NewtonAction(List stmts) { + this.stmts = stmts; + } + + public static NewtonAction of(List stmts) { + return new NewtonAction(stmts); + } + + @Override + public List getStmts() { + return stmts; + } + + @Override + public String toString() { + return Utils.lispStringBuilder(getClass().getSimpleName()).body().addAll(stmts).toString(); + } + } +} diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java new file mode 100644 index 0000000000..7319d3b88e --- /dev/null +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java @@ -0,0 +1,277 @@ +package hu.bme.mit.theta.analysis.expr.refinement; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.Lists; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.ExprTraceUtils; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.stmt.AssumeStmt; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.ExprSimplifier; +import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.core.utils.PathUtils; +import hu.bme.mit.theta.core.utils.SpState; +import hu.bme.mit.theta.core.utils.VarIndexing; +import hu.bme.mit.theta.core.utils.WpState; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.utils.WithPushPop; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import java.util.stream.Stream; + +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; +import static java.util.stream.Collectors.toList; + +/** + * An ExprTraceChecker that generates new predicates based on the UCB algorithm by + * Leucker, Martin & Markin, Grigory & Neuhäußer, Martin. (2015). A New Refinement + * Strategy for CEGAR-Based Industrial Model Checking. 155-170. 10.1007/978-3-319-26287-1_10. + */ +public class ExprTraceUCBChecker implements ExprTraceChecker { + + private final Solver solver; + private final Expr init; + private final Expr target; + + private ExprTraceUCBChecker(final Expr init, final Expr target, final Solver solver) { + this.solver = checkNotNull(solver); + this.init = checkNotNull(init); + this.target = checkNotNull(target); + } + + public static ExprTraceUCBChecker create( + final Expr init, final Expr target, final Solver solver + ) { + return new ExprTraceUCBChecker(init, target, solver); + } + + @SuppressWarnings("unchecked") + @Override + public ExprTraceStatus check(final Trace trace) { + checkNotNull(trace); + try { + return check2((Trace) trace); + } + catch(ClassCastException e) { + throw new UnsupportedOperationException("Actions must be of type StmtAction", e); + } + } + +private ExprTraceStatus check2(final Trace trace) { + final var ftrace = flattenTrace(trace); + final int stateCount = trace.getStates().size(); + + final List indexings = new ArrayList<>(stateCount); + indexings.add(VarIndexing.all(0)); + + final Valuation model; + final Collection> unsatCore; + final boolean concretizable; + + try (WithPushPop wpp = new WithPushPop(solver)) { + for (int i = 1; i < stateCount; ++i) { + indexings.add(indexings.get(i - 1).add(trace.getAction(i - 1).nextIndexing())); + solver.track( + ExprUtils.getConjuncts( + PathUtils.unfold(trace.getAction(i - 1).toExpr(), indexings.get(i - 1)) + ) + ); + } + + concretizable = solver.check().isSat(); + + if (concretizable) { + model = solver.getModel(); + unsatCore = null; + } else { + model = null; + unsatCore = solver.getUnsatCore(); + } + } + + if (concretizable) { + checkNotNull(model); + return createCounterexample(model, indexings, trace); + } else { + checkNotNull(unsatCore); + return createRefinement(unsatCore, indexings, ftrace); + } + } + + @Override + public String toString() { + return getClass().getSimpleName(); + } + + private ExprTraceStatus.Feasible createCounterexample( + final Valuation model, + final List indexings, + final Trace trace + ) { + final ImmutableList.Builder builder = ImmutableList.builder(); + for (final VarIndexing indexing : indexings) { + builder.add(PathUtils.extractValuation(model, indexing)); + } + return ExprTraceStatus.feasible(Trace.of(builder.build(), trace.getActions())); + } + + private ExprTraceStatus.Infeasible createRefinement( + final Collection> unsatCore, + final List indexings, + final Trace trace + ) { + final int stateCount = trace.getStates().size(); + final List> wps = calculateWpStates(trace, indexings); + + final List> predicates = new ArrayList<>(); + + var constCount = 0; + for(var i = 0; i < stateCount; i++) { + try(final var wpp = new WithPushPop(solver)) { + final List> dataRegion = new ArrayList<>(); + + /* Calculate SP */ + if (i == 0) { + solver.track(True()); + dataRegion.add(True()); + } else /* i > 0 */ { + var spState = SpState.of(PathUtils.foldin(predicates.get(i - 1), indexings.get(i - 1)), constCount); + for(var stmt : trace.getAction(i - 1).getStmts()) { + spState = spState.sp(stmt); + } + + final var expr = PathUtils.unfold(spState.getExpr(), indexings.get(i)); + constCount = spState.getConstCount(); + solver.track(ExprUtils.getConjuncts(expr)); + dataRegion.addAll(ExprUtils.getConjuncts(expr)); + } + + /* Add wp */ + solver.track(ExprUtils.getConjuncts(wps.get(i))); + + solver.check(); + assert solver.check().isUnsat(); // It must be unsat + Collection> uc = solver.getUnsatCore(); + + /* Keep only those expressions from uc that are not in the data region */ + final Collection> predicate = new ArrayList<>(); + for (var ucExpr : uc) { + if (!dataRegion.contains(ucExpr)) { + predicate.add(ucExpr); + } + } + + /* Add the negated of the above expression as the new predicate */ + predicates.add( + ExprSimplifier.simplify( + Not(And(new HashSet<>(predicate))), + ImmutableValuation.empty() + ) + ); + } + } + return ExprTraceStatus.infeasible( + ItpRefutation.sequence( + IntStream.range(0, predicates.size()) + .mapToObj(i -> PathUtils.foldin(predicates.get(i), indexings.get(i))) + .collect(Collectors.toUnmodifiableList()) + ) + ); + } + + private List> calculateWpStates( + final Trace trace, + final List indexings + ) { + final int stateCount = trace.getStates().size(); + final List> wps = new ArrayList<>(Collections.nCopies(stateCount, null)); + + var wpstate = WpState.of(target); + wps.set(stateCount - 1, target); + for(var i = stateCount - 1; i > 0; i--) { + var action = trace.getAction(i - 1); + + for(var stmt : Lists.reverse(action.getStmts())) { + wpstate = wpstate.wep(stmt); + } + + wps.set(i - 1, PathUtils.unfold(wpstate.getExpr(), indexings.get(i - 1))); + } + + return wps; + } + + private Trace flattenTrace(final Trace trace) { + final var stateCount = trace.getStates().size(); + final var flattenedActions = new ArrayList(stateCount - 1); + + for(var i = 1; i < stateCount; i++) { + var initStream = + (i == 1) + ? ExprUtils.getConjuncts(init).stream().map(AssumeStmt::of) + : Stream.empty(); + + var stateStream = ExprUtils.getConjuncts(trace.getState(i - 1).toExpr()).stream().map(AssumeStmt::of); + + var actionStream = trace.getAction(i - 1).getStmts().stream(); + + var targetStream = + (i == stateCount - 1) + ? Stream.concat( + ExprUtils.getConjuncts(trace.getState(i).toExpr()).stream().map(AssumeStmt::of), + ExprUtils.getConjuncts(target).stream().map(AssumeStmt::of) + ) + : Stream.empty(); + + flattenedActions.add( + UCBAction.of( + Stream.of(initStream, stateStream, actionStream, targetStream).flatMap(e -> e).collect(toList()) + ) + ); + } + + return ExprTraceUtils.traceFrom(flattenedActions); + } + + /* + * Custom StmtAction to use when constructing helper traces + */ + + private static class UCBAction extends StmtAction { + private final List stmts; + + private UCBAction(List stmts) { + this.stmts = stmts; + } + + public static UCBAction of(List stmts) { + return new UCBAction(stmts); + } + + @Override + public List getStmts() { + return stmts; + } + + @Override + public String toString() { + return Utils.lispStringBuilder(getClass().getSimpleName()).body().addAll(stmts).toString(); + } + } +} diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index af559b8827..c86e2793a7 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -67,7 +67,8 @@ public enum Domain { } public enum Refinement { - FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE + FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE, UCB, + NWT_WP, NWT_SP, NWT_WP_LV, NWT_SP_LV, NWT_IT_WP, NWT_IT_SP, NWT_IT_WP_LV, NWT_IT_SP_LV } public enum Search { @@ -162,7 +163,7 @@ public CfaLts getLts() { } public enum InitPrec { - EMPTY, ALLVARS, ALLASSUMES; + EMPTY, ALLVARS, ALLASSUMES } private Logger logger = NullLogger.getInstance(); @@ -261,6 +262,74 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), solver), precGranularity.createRefiner(new VarsRefToExplPrec()), pruneStrategy, logger); break; + case UCB: + refiner = SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(True(), True(), solver), + precGranularity.createRefiner(new ItpRefToExplPrec()), pruneStrategy, logger); + break; + case NWT_SP: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withSP().withoutLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_WP: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withWP().withoutLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_SP_LV: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withSP().withLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_WP_LV: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withWP().withLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_IT_SP: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withSP().withoutLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_IT_WP: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withWP().withoutLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_IT_SP_LV: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withSP().withLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; + case NWT_IT_WP_LV: + refiner = SingleExprTraceRefiner.create( + ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withWP().withLV(), + precGranularity.createRefiner(new ItpRefToExplPrec()), + pruneStrategy, + logger + ); + break; default: throw new UnsupportedOperationException( domain + " domain does not support " + refinement + " refinement."); @@ -324,6 +393,33 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { case MULTI_SEQ: exprTraceChecker = ExprTraceSeqItpChecker.create(True(), True(), solver); break; + case UCB: + exprTraceChecker = ExprTraceUCBChecker.create(True(), True(), solver); + break; + case NWT_SP: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withSP().withoutLV(); + break; + case NWT_WP: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withWP().withoutLV(); + break; + case NWT_SP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withSP().withLV(); + break; + case NWT_WP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withoutIT().withWP().withLV(); + break; + case NWT_IT_SP: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withSP().withoutLV(); + break; + case NWT_IT_WP: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withWP().withoutLV(); + break; + case NWT_IT_SP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withSP().withLV(); + break; + case NWT_IT_WP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), solver).withIT().withWP().withLV(); + break; default: throw new UnsupportedOperationException( domain + " domain does not support " + refinement + " refinement."); diff --git a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java index e0c09c30a3..91c119306c 100644 --- a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java +++ b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java @@ -37,8 +37,7 @@ import java.util.Collection; import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain.*; -import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement.BW_BIN_ITP; -import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement.SEQ_ITP; +import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement.*; @RunWith(value = Parameterized.class) public class CfaTest { @@ -61,12 +60,6 @@ public class CfaTest { public static Collection data() { return Arrays.asList(new Object[][] { - { "src/test/resources/counter5_true.cfa", PRED_BOOL, SEQ_ITP, true, 0 }, - - { "src/test/resources/counter5_true.cfa", PRED_CART, BW_BIN_ITP, true, 0 }, - - { "src/test/resources/counter5_true.cfa", EXPL, SEQ_ITP, true, 0 }, - { "src/test/resources/arithmetic-bool00.cfa", PRED_CART, SEQ_ITP, false, 15 }, { "src/test/resources/arithmetic-bool00.cfa", PRED_BOOL, BW_BIN_ITP, false, 15 }, @@ -103,6 +96,20 @@ public static Collection data() { { "src/test/resources/arrays.cfa", EXPL, SEQ_ITP, false, 8 }, + { "src/test/resources/counter5_true.cfa", PRED_BOOL, SEQ_ITP, true, 0 }, + + { "src/test/resources/counter5_true.cfa", PRED_CART, BW_BIN_ITP, true, 0 }, + + { "src/test/resources/counter5_true.cfa", EXPL, SEQ_ITP, true, 0 }, + + { "src/test/resources/counter_bv_true.cfa", EXPL, NWT_IT_WP, true, 0 }, + + { "src/test/resources/counter_bv_false.cfa", EXPL, NWT_IT_WP, false, 13 }, + + { "src/test/resources/counter_bv_true.cfa", PRED_CART, NWT_IT_WP, true, 0 }, + + { "src/test/resources/counter_bv_false.cfa", PRED_CART, UCB, false, 13 }, + { "src/test/resources/ifelse.cfa", PRED_CART, SEQ_ITP, false, 3 }, { "src/test/resources/ifelse.cfa", PRED_BOOL, BW_BIN_ITP, false, 3 }, diff --git a/subprojects/cfa-analysis/src/test/resources/counter_bv_false.cfa b/subprojects/cfa-analysis/src/test/resources/counter_bv_false.cfa new file mode 100644 index 0000000000..ba19cb05c1 --- /dev/null +++ b/subprojects/cfa-analysis/src/test/resources/counter_bv_false.cfa @@ -0,0 +1,17 @@ +main process cfa { + var x : bv[4] + + init loc L0 + loc L1 + loc L2 + loc L3 + final loc END + error loc ERR + + L0 -> L1 { x := 4'd0 } + L1 -> L2 { assume x bvult 4'd5 } + L1 -> L3 { assume not (x bvult 4'd5) } + L2 -> L1 { x := (x bvadd 4'd1) } + L3 -> END { assume x bvult 4'd5 } + L3 -> ERR { assume not (x bvult 4'd5) } +} \ No newline at end of file diff --git a/subprojects/cfa-analysis/src/test/resources/counter_bv_true.cfa b/subprojects/cfa-analysis/src/test/resources/counter_bv_true.cfa new file mode 100644 index 0000000000..179939dae1 --- /dev/null +++ b/subprojects/cfa-analysis/src/test/resources/counter_bv_true.cfa @@ -0,0 +1,17 @@ +main process cfa { + var x : bv[4] + + init loc L0 + loc L1 + loc L2 + loc L3 + final loc END + error loc ERR + + L0 -> L1 { x := 4'd0 } + L1 -> L2 { assume x bvult 4'd5 } + L1 -> L3 { assume not (x bvult 4'd5) } + L2 -> L1 { x := (x bvadd 4'd1) } + L3 -> END { assume x = 4'd5 } + L3 -> ERR { assume not (x = 4'd5) } +} \ No newline at end of file diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md index 65a85a65a0..93020e67cb 100644 --- a/subprojects/cfa-cli/README.md +++ b/subprojects/cfa-cli/README.md @@ -82,8 +82,13 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J * `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). * `SEQ_ITP` (default): Sequence interpolation. * `MULTI_SEQ`: Sequence interpolation with multiple counterexamples (see Section 3.2.2 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). - * `UNSAT_CORE`: Unsat cores, only available if `--domain` is `EXPL`. - * _Remark: `BW_BIN_ITP` and `SEQ_ITP` has the best performance usually._ + * `UNSAT_CORE`: Simple unsat cores, only available if `--domain` is `EXPL`. This refinement strategy does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver). + * `UCB`: Unsat core based predicates ([see paper](https://link.springer.com/chapter/10.1007%2F978-3-319-26287-1_10) for more information). _Experimental feature._ Does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver). + * `NWT_*`: Newton-style refinement. _Experimental feature._ Does not rely on interpolation, so it can even work if interpolating is not possible (e.g. bitvectors with Z3 solver). The supported Newton-style variants can be found in the following list ([see paper](https://dl.acm.org/doi/10.1145/3106237.3106307) for more information): + * `NWT_SP` and `NWT_WP`: Only works for really simple inputs, + * `NWT_SP_LV`, `NWT_WP_LV`, `NWT_IT_SP`, `NWT_IT_WP_LV`, `NWT_IT_SP_LV`, + * `NWT_IT_WP`: Usually the most effective. + * _Remark: `BW_BIN_ITP` and `SEQ_ITP` has the best performance usually. For bitvectors, `NWT_IT_WP` is recommended._ * `--predsplit`: Splitting applied to predicates during refinement, possible values: * `WHOLE` (default): Keep predicates as a whole, no splitting is applied. Can perform well if the model has many Boolean variables. * `CONJUNCTS`: Split predicates into conjuncts. diff --git a/subprojects/cfa/README.md b/subprojects/cfa/README.md index 19a1451790..634be359a4 100644 --- a/subprojects/cfa/README.md +++ b/subprojects/cfa/README.md @@ -38,19 +38,19 @@ Variables of the CFA can have the following types. * `int`: Mathematical, unbounded SMT integers. * `rat`: Rational numbers (implemented as SMT reals). * `[K] -> V`: SMT arrays (associative maps) from a given key type `K` to a value type `V`. -* `bv[L]`: Bitvector of given length `L`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._ +* `bv[L]`: Bitvector of given length `L`. _This is an experimental feature. See the [details](doc/bitvectors.md) for more information._ Expressions of the CFA include the following. * Identifiers (variables). * Literals, e.g., `true`, `false` (Bool), `0`, `123` (integer), `4 % 5` (rational). * Array literals can be given by listing the key-value pairs and the (mandatory) default element, e.g., `[0 <- 182, 1 <- 41, default <- 75]`. If there are no elements, the key type has to be given before the default element, e.g., `[default <- 75]`. - * Bitvector literals can be given by stating the length and the exact value of the bitvector in binary, decimal or hexadecimal form. (E.g. `4'd5` is a 4-bit-long bitvector with the decimal value 5.) _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._ + * Bitvector literals can be given by stating the length and the exact value of the bitvector in binary, decimal or hexadecimal form. (E.g. `4'd5` is a 4-bit-long bitvector with the decimal value 5.) _This is an experimental feature. See the [details](doc/bitvectors.md) for more information._ * Comparison, e.g., `=`, `/=`, `<`, `>`, `<=`, `>=`. * Boolean operators, e.g., `and`, `or`, `xor`, `not`, `imply`, `iff`. * Arithmetic, e.g., `+`, `-`, `/`, `*`, `mod`, `rem`. * Conditional: `if . then . else .`. * Array read (`a[i]`) and write (`a[i <- v]`). -* Bitvector specific operators, e.g., `bvand`, `bvor`, `bvxor`, `bvshl`, `bvashr`, `bvlshr`, `bvrol`, `bvror`, `bvnot`, etc. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._ +* Bitvector specific operators, e.g., `bvand`, `bvor`, `bvxor`, `bvshl`, `bvashr`, `bvlshr`, `bvrol`, `bvror`, `bvnot`, etc. _This is an experimental feature. See the [details](doc/bitvectors.md) for more information._ ### Textual representation (DSL) diff --git a/subprojects/cfa/doc/bitvectors.md b/subprojects/cfa/doc/bitvectors.md index 76e73539aa..dbab527f46 100644 --- a/subprojects/cfa/doc/bitvectors.md +++ b/subprojects/cfa/doc/bitvectors.md @@ -97,6 +97,6 @@ These operations encode relational operations between bitvectors. These operatio ## Algorithmic support for verification with bitvectors -As of now, bitvectors are only partially supported due to the fact, that the underlying SMT solver, Z3 does not support interpolation when bitvectors are involved. - -As a result, CEGAR with predicate abstraction is not supported at all. However, CEGAR with explicit value abstraction, and with the UNSAT core refinement strategy is working preoperty, as it does not rely on the interpolation capabilities of the SMT solver. +The CEGAR algorithms use Z3 as an SMT solver, which does not support interpolation when bitvectors are involved. +Therefore, refinement algorithms involving interpolation (`--refinement *_ITP`) do not work. +However, there are other refinement algorithms (e.g., `UNSAT_CORE`, `UCB` or `NWT_*`) that do not rely on interpolation and work for bitvectors as well. diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/SmartBoolExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/SmartBoolExprs.java index ea55d214ed..8f565f315d 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/SmartBoolExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/SmartBoolExprs.java @@ -21,6 +21,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; import java.util.Collection; +import java.util.LinkedHashSet; import java.util.List; import com.google.common.collect.ImmutableList; @@ -72,7 +73,7 @@ public static Expr And(final Collection> ops) } else if (filteredOps.size() == 1) { return singleElementOf(filteredOps); } else { - return BoolExprs.And(filteredOps); + return BoolExprs.And(new LinkedHashSet<>(filteredOps)); } } @@ -91,7 +92,7 @@ public static Expr Or(final Collection> ops) } else if (filteredOps.size() == 1) { return singleElementOf(filteredOps); } else { - return BoolExprs.Or(filteredOps); + return BoolExprs.Or(new LinkedHashSet<>(filteredOps)); } } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index e6a2dca525..c94e2c4915 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -255,13 +255,13 @@ public final class ExprSimplifier { .addCase(BvULeqExpr.class, ExprSimplifier::simplifyBvULeq) .addCase(BvULtExpr.class, ExprSimplifier::simplifyBvULt) - + .addCase(BvSGeqExpr.class, ExprSimplifier::simplifyBvSGeq) - + .addCase(BvSGtExpr.class, ExprSimplifier::simplifyBvSGt) - + .addCase(BvSLeqExpr.class, ExprSimplifier::simplifyBvSLeq) - + .addCase(BvSLtExpr.class, ExprSimplifier::simplifyBvSLt) // General diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java new file mode 100644 index 0000000000..c85d400950 --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java @@ -0,0 +1,161 @@ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.BasicSubstitution; +import hu.bme.mit.theta.core.model.Substitution; +import hu.bme.mit.theta.core.stmt.AssignStmt; +import hu.bme.mit.theta.core.stmt.AssumeStmt; +import hu.bme.mit.theta.core.stmt.HavocStmt; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.OrtStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; +import hu.bme.mit.theta.core.stmt.SkipStmt; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.stmt.StmtVisitor; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; + +public class SpState { + private static final int HASH_SEED = 2029; + private volatile int hashCode = 0; + + private final Expr expr; + private final int constCount; + + private SpState(final Expr expr, final int constCount) { + checkNotNull(expr); + checkArgument(constCount >= 0); + this.expr = expr; + this.constCount = constCount; + } + + public static SpState of(final Expr expr) { + return new SpState(expr, 0); + } + + public static SpState of(final Expr expr, final int constCount) { + return new SpState(expr, constCount); + } + + public Expr getExpr() { + return expr; + } + + public int getConstCount() { + return constCount; + } + + /** + * Compute the strongest postcondition w.r.t. a statement + * + * @param stmt Statement + * @return + */ + public SpState sp(final Stmt stmt) { + return stmt.accept(SpState.SpVisitor.getInstance(), this); + } + + @Override + public int hashCode() { + int result = hashCode; + if (result == 0) { + result = HASH_SEED; + result = 31 * result + expr.hashCode(); + result = 31 * result + constCount; + hashCode = result; + } + return result; + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof SpState) { + final SpState that = (SpState) obj; + return this.constCount == that.constCount && this.expr.equals(that.expr); + } else { + return false; + } + } + + @Override + public String toString() { + return Utils.lispStringBuilder(getClass().getSimpleName()).add(expr).add(Integer.valueOf(constCount)) + .toString(); + } + + private static final class SpVisitor implements StmtVisitor { + + private SpVisitor() { + } + + private static class LazyHolder { + private static final SpState.SpVisitor INSTANCE = new SpState.SpVisitor(); + } + + public static SpState.SpVisitor getInstance() { + return SpState.SpVisitor.LazyHolder.INSTANCE; + } + + @Override + public SpState visit(final SkipStmt stmt, final SpState state) { + return state; + } + + @Override + public SpState visit(final AssignStmt stmt, final SpState state) { + final VarDecl varDecl = stmt.getVarDecl(); + final int constCount = state.constCount + 1; + final String valName = String.format("_sp_%d", constCount); + final Expr val = Const(valName, varDecl.getType()).getRef(); + final Substitution sub = BasicSubstitution.builder().put(varDecl, val).build(); + + final Expr stateExpr = sub.apply(state.getExpr()); + final Expr eqExpr = sub.apply(stmt.getExpr()); + final Expr expr = And(stateExpr, Eq(varDecl.getRef(), eqExpr)); + return new SpState(expr, constCount); + } + + @Override + public SpState visit(final HavocStmt stmt, final SpState state) { + final VarDecl varDecl = stmt.getVarDecl(); + final int constCount = state.constCount + 1; + final String valName = String.format("_sp_%d", constCount); + final Expr val = Const(valName, varDecl.getType()).getRef(); + final Substitution sub = BasicSubstitution.builder().put(varDecl, val).build(); + final Expr expr = sub.apply(state.getExpr()); + return new SpState(expr, constCount); + } + + @Override + public SpState visit(final AssumeStmt stmt, final SpState state) { + final Expr expr = And(state.getExpr(), stmt.getCond()); + final int constCount = state.constCount; + return new SpState(expr, constCount); + } + + @Override + public SpState visit(SequenceStmt stmt, SpState param) { + throw new UnsupportedOperationException(); + } + + @Override + public SpState visit(NonDetStmt stmt, SpState param) { + throw new UnsupportedOperationException(); + } + + @Override + public SpState visit(OrtStmt stmt, SpState param) { + throw new UnsupportedOperationException(); + } + } +} diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java index d0b24273e5..5d026737c6 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java @@ -48,10 +48,18 @@ public static WpState of(final Expr expr) { return new WpState(expr, 0); } + public static WpState of(final Expr expr, final int constCount) { + return new WpState(expr, constCount); + } + public Expr getExpr() { return expr; } + public int getConstCount() { + return constCount; + } + /** * Compute the weakest precondition w.r.t. a statement * @@ -133,7 +141,7 @@ public WpState visit(final AssignStmt stmt, fi public WpState visit(final HavocStmt stmt, final WpState state) { final VarDecl varDecl = stmt.getVarDecl(); final int constCount = state.constCount + 1; - final String valName = String.format("_val_%d", constCount); + final String valName = String.format("_wp_%d", constCount); final Expr val = Const(valName, varDecl.getType()).getRef(); final Substitution sub = BasicSubstitution.builder().put(varDecl, val).build(); final Expr expr = sub.apply(state.getExpr());