diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java index 435193fa23..acc0e3af13 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java @@ -15,19 +15,18 @@ */ package hu.bme.mit.theta.analysis.algorithm.arg; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.container.Containers; - import java.util.ArrayList; import java.util.Collection; import java.util.Optional; import java.util.stream.Stream; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; - public final class ArgNode { final ARG arg; @@ -47,7 +46,12 @@ public final class ArgNode { public boolean expanded; // Set by ArgBuilder - ArgNode(final ARG arg, final S state, final int id, final int depth, final boolean target) { + ArgNode( + final ARG arg, + final S state, + final int id, + final int depth, + final boolean target) { this.arg = arg; this.state = state; this.id = id; @@ -67,8 +71,8 @@ public int getId() { } /** - * Gets the depth of the node, which is 0 if the node has no parent, and - * depth(parent) + 1 otherwise. + * Gets the depth of the node, which is 0 if the node has no parent, and depth(parent) + 1 + * otherwise. */ public int getDepth() { return depth; @@ -83,6 +87,10 @@ public void setState(final S state) { this.state = state; } + public boolean inPartialOrder(final ArgNode node) { + return arg.getPartialOrd().isLeq(node.getState(), this.getState()); + } + public boolean mayCover(final ArgNode node) { if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) { return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed()); @@ -162,69 +170,49 @@ public Stream getSuccStates() { //// - /** - * Checks if the node is covered, i.e., there is a covering edge for the - * node. - */ + /** Checks if the node is covered, i.e., there is a covering edge for the node. */ public boolean isCovered() { return coveringNode.isPresent(); } - /** - * Checks if the node is not a bottom state. - */ + /** Checks if the node is not a bottom state. */ public boolean isFeasible() { return !state.isBottom(); } - /** - * Checks if the node is subsumed, i.e., the node is covered or not - * feasible. - */ + /** Checks if the node is subsumed, i.e., the node is covered or not feasible. */ public boolean isSubsumed() { return isCovered() || !isFeasible(); } - /** - * Checks if the node is excluded, i.e., the node is subsumed or has an - * excluded parent. - */ + /** Checks if the node is excluded, i.e., the node is subsumed or has an excluded parent. */ public boolean isExcluded() { return ancestors().anyMatch(ArgNode::isSubsumed); } /** - * Checks if the node is target, i.e., the target predicate holds (e.g., it - * is an error state). + * Checks if the node is target, i.e., the target predicate holds (e.g., it is an error state). */ public boolean isTarget() { return target; } - /** - * Checks if the node is expanded, i.e., all of its successors are present. - */ + /** Checks if the node is expanded, i.e., all of its successors are present. */ public boolean isExpanded() { return expanded; } - /** - * Checks if the node is leaf, i.e., it has no successors. - */ + /** Checks if the node is leaf, i.e., it has no successors. */ public boolean isLeaf() { return outEdges.isEmpty(); } - /** - * Checks if the node is safe, i.e., not target or excluded. - */ + /** Checks if the node is safe, i.e., not target or excluded. */ public boolean isSafe() { return !isTarget() || isExcluded(); } - /** - * Checks if the node is complete, i.e., expanded or excluded. - */ + /** Checks if the node is complete, i.e., expanded or excluded. */ public boolean isComplete() { return isExpanded() || isExcluded(); } @@ -232,7 +220,9 @@ public boolean isComplete() { //// public Stream> properAncestors() { - return getParent().map(p -> Stream.concat(Stream.of(p), p.properAncestors())).orElse(Stream.empty()); + return getParent() + .map(p -> Stream.concat(Stream.of(p), p.properAncestors())) + .orElse(Stream.empty()); } public Stream> ancestors() { @@ -263,7 +253,8 @@ private Stream> unexcludedDescendantsOfNode() { if (this.isSubsumed()) { return Stream.empty(); } else { - return Stream.concat(Stream.of(this), this.children().flatMap(ArgNode::unexcludedDescendantsOfNode)); + return Stream.concat( + Stream.of(this), this.children().flatMap(ArgNode::unexcludedDescendantsOfNode)); } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index dac497e043..6596eb7cbb 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -91,7 +91,6 @@ public SafetyResult check(final P initPrec) { WebDebuggerLogger wdl = WebDebuggerLogger.getInstance(); do { ++iteration; - logger.write(Level.MAINSTEP, "Iteration %d%n", iteration); logger.write(Level.MAINSTEP, "| Checking abstraction...%n"); final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java new file mode 100644 index 0000000000..90511f840e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java @@ -0,0 +1,166 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration; + +import static com.google.common.base.Preconditions.checkNotNull; +import static java.util.stream.Collectors.toList; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge; +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; +import java.util.*; +import java.util.stream.Collectors; + +class AdvancedArgTrace implements Iterable> { + private static final int HASH_SEED = 7453; + private volatile int hashCode = 0; + + private final List> nodes; + private final List> edges; + private final Collection states; + + private AdvancedArgTrace(final ArgNode node) { + // adding items to first index will lead to O(N^2) performance + final List> nodeList = new ArrayList<>(); + final List> edgeList = new ArrayList<>(); + + ArgNode running = node; + nodeList.add(running); + + while (running.getInEdge().isPresent()) { + final ArgEdge inEdge = running.getInEdge().get(); + running = inEdge.getSource(); + edgeList.add(inEdge); + nodeList.add(running); + } + + // create the correct order by reversing O(N) + Collections.reverse(nodeList); + Collections.reverse(edgeList); + + this.nodes = Collections.unmodifiableList(nodeList); + this.edges = Collections.unmodifiableList(edgeList); + states = nodes.stream().map(ArgNode::getState).collect(Collectors.toList()); + } + + private AdvancedArgTrace(List> nodeList, List> edgeList) { + this.nodes = Collections.unmodifiableList(nodeList); + this.edges = Collections.unmodifiableList(edgeList); + states = nodes.stream().map(ArgNode::getState).collect(Collectors.toList()); + } + + //// + + public static AdvancedArgTrace to( + final ArgNode node) { + checkNotNull(node); + return new AdvancedArgTrace<>(node); + } + + public static AdvancedArgTrace fromTo( + final ArgNode fromNode, final ArgNode toNode) { + checkNotNull(fromNode); + checkNotNull(toNode); + AdvancedArgTrace differenceTrace = new AdvancedArgTrace<>(fromNode); + AdvancedArgTrace fullTrace = new AdvancedArgTrace<>(toNode); + return substituteTrace(fullTrace, differenceTrace); + } + + /** + * Substitutes the differenceTrace from the fullTrace, where the differenceTrace should be the + * beginning of the full trace + */ + private static AdvancedArgTrace substituteTrace( + AdvancedArgTrace fullTrace, AdvancedArgTrace differenceTrace) { + List> differenceNodes = differenceTrace.nodes; + + List> remainingNodes = new ArrayList<>(fullTrace.nodes); + remainingNodes.removeIf( + saArgNode -> + !(saArgNode.equals(differenceNodes.get(differenceNodes.size() - 1))) + && differenceNodes.contains(saArgNode)); + + List> remainingEdges = new ArrayList<>(fullTrace.edges); + remainingEdges.removeIf(differenceTrace.edges::contains); + + return new AdvancedArgTrace<>(remainingNodes, remainingEdges); + } + + //// + + /** Gets the length of the trace, i.e., the number of edges. */ + public int length() { + return edges.size(); + } + + public ArgNode node(final int index) { + return nodes.get(index); + } + + public ArgEdge edge(final int index) { + return edges.get(index); + } + + public List> nodes() { + return nodes; + } + + public List> edges() { + return edges; + } + + //// + + /** + * Converts the ArgTrace to a Trace by extracting states and actions from nodes and edges + * respectively. + */ + public Trace toTrace() { + final List states = nodes.stream().map(ArgNode::getState).collect(toList()); + final List actions = edges.stream().map(ArgEdge::getAction).collect(toList()); + return Trace.of(states, actions); + } + + //// + + @Override + public Iterator> iterator() { + return nodes.iterator(); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + AdvancedArgTrace argTrace = (AdvancedArgTrace) o; + return states.equals(argTrace.states); // && edges.equals(argTrace.edges); + } + + @Override + public int hashCode() { + int result = hashCode; + if (result == 0) { + result = HASH_SEED; + result = 31 * result + states.hashCode(); + result = 31 * result + edges.hashCode(); + hashCode = result; + } + return result; + // return Objects.hash(states, edges); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt new file mode 100644 index 0000000000..968e76a42f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt @@ -0,0 +1,125 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.expr.StmtAction +import java.io.BufferedReader +import java.io.IOException +import java.io.StringReader + +class DoubleEndNodeRemover { + + private fun isLastInternal(node: ArgNode): Boolean { + return node.state.toString().contains("last_internal") + } + + private fun isBadLeaf(node: ArgNode): Boolean { + if (isLastInternal(node)) { + if (node.parent.isEmpty) return false + val parent = node.parent.get() + if (parent.parent.isEmpty) return false + val grandParent = node.parent.get().parent.get() + return if ( + node.isCovered && parent.parent.get() == node.coveringNode.get() + ) { // node is covered and parent is checked above + // bad node + true + } else { + false + } + } else { + var transitionFired = false + if (node.parent.isPresent && node.parent.get().parent.isPresent) { + val grandParent = node.parent.get().parent.get() + if (!(node.isCovered && node.coveringNode.get() == grandParent)) return false + + val state = node.parent.get().state.toString() + val bufReader = BufferedReader(StringReader(state)) + var line: String? = null + try { + while ((bufReader.readLine().also { line = it }) != null) { + if (line!!.trim { it <= ' ' }.matches("^.*\\(__id_.*__.*\\strue\\).*$".toRegex())) + transitionFired = true + } + } catch (e: IOException) { + e.printStackTrace() + } + return !transitionFired // if no transition was fired (and state not changed), this is a + // superfluous node + } else { + return false + } + } + } + + companion object { + + /** + * Mainly of use for XSTS! Collecting nodes that look like there should be traces to it, but + * shouldn't ("not firing anything" nodes) This should most likely note come up with other + * formalisms. This removal is executed on them anyways. + */ + fun collectBadLeaves(arg: ARG): List> { + val instance = DoubleEndNodeRemover() + val badNodes: MutableList> = ArrayList() + arg.nodes + .filter { obj: ArgNode -> obj.isLeaf } + .forEach { node: ArgNode -> + if (instance.isBadLeaf(node)) { + badNodes.add(node) + } + } + return badNodes + } + + fun filterSuperfluousEndNode(trace: Trace): Trace { + if (trace.states.size > 3) { + var transitionFired = false + val size = trace.states.size + if (trace.getState(size - 1).toString() == trace.getState(size - 3).toString()) { + val bufReader = BufferedReader(StringReader(trace.getState(size - 2).toString())) + var line: String? = null + try { + while ((bufReader.readLine().also { line = it }) != null) { + if (line!!.trim { it <= ' ' }.matches("^\\(__id_.*__.*\\strue\\)*$".toRegex())) + transitionFired = true + } + } catch (e: IOException) { + e.printStackTrace() + } + } + if (!transitionFired) { + val newStates = ArrayList(trace.states) + newStates.removeAt(newStates.size - 1) + newStates.removeAt(newStates.size - 1) + val newActions = ArrayList(trace.actions) + newActions.removeAt(newActions.size - 1) + newActions.removeAt(newActions.size - 1) + return Trace.of(newStates, newActions) + } else { + return trace + } + } else { + return trace + } + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt new file mode 100644 index 0000000000..f511e11437 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt @@ -0,0 +1,38 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace + +/** Traces built on ArgTraces, but capable of handling traces going through covered nodes */ +class PatchArgTrace private constructor(val traces: List>) : + Iterable?> { + private val nodes: List> = traces.flatten() + + override fun iterator(): Iterator?> { + return nodes.iterator() + } + + companion object { + fun create(traces: List>): PatchArgTrace { + + return PatchArgTrace(traces) + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt new file mode 100644 index 0000000000..d0dbb7dc17 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt @@ -0,0 +1,258 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration + +import com.google.common.base.Preconditions +import hu.bme.mit.theta.analysis.* +import hu.bme.mit.theta.analysis.algorithm.* +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractSummaryBuilder +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult +import hu.bme.mit.theta.common.logging.Logger +import java.util.function.Consumer +import kotlin.collections.ArrayList + +class TraceGenerationChecker( + private val logger: Logger, + private val abstractor: BasicArgAbstractor, + private val getFullTraces: Boolean, +) : Checker, P> { + private var traces: List> = ArrayList() + + companion object { + fun create( + logger: Logger, + abstractor: BasicArgAbstractor, + getFullTraces: Boolean, + ): TraceGenerationChecker { + return TraceGenerationChecker(logger, abstractor, getFullTraces) + } + } + + override fun check(prec: P): TraceGenerationResult, S, A> { + logger.write( + Logger.Level.SUBSTEP, + "Printing prec for trace generation...\n" + System.lineSeparator(), + ) + logger.write(Logger.Level.SUBSTEP, prec.toString()) + + val arg = abstractor.createProof() + abstractor.check(arg, prec) + logger.write(Logger.Level.SUBSTEP, "ARG done, fetching traces...\n") + + // bad node: mostly XSTS specific thing, that the last state (last_env nodes) doubles up and the + // leaf is covered by the + // last_env before which is superfluous. + // Possible side effect if not handled: possibly a "non-existing leaf" and superfluous traces or + // just traces that are 1 longer than they should be + val badNodes = DoubleEndNodeRemover.collectBadLeaves(arg) + logger.write(Logger.Level.INFO, "Number of bad nodes filtered out: ${badNodes.size}") + + // leaves + val endNodes = arg.nodes.filter { obj: ArgNode -> obj.isLeaf }.toList() + // leaves, but bad nodes are properly filtered, see bad nodes above + val filteredEndNodes = filterEndNodes(endNodes, badNodes) + + val argTraces: List> = + ArrayList( + filteredEndNodes.stream().map { node: ArgNode? -> ArgTrace.to(node) }.toList() + ) + + assert(!getFullTraces) + val summaryBuilder = AbstractSummaryBuilder() + argTraces.forEach { trace -> summaryBuilder.addTrace(trace) } + val traceSetSummary = summaryBuilder.build() + + // filter 2, optional, to get full traces even where there is coverage + // why?: otherwise we stop at the leaf, which is covered in many traces by other nodes + traces = ArrayList(argTraces.stream().map { obj: ArgTrace -> obj.toTrace() }.toList()) + + Preconditions.checkState( + traces.isNotEmpty(), + "Generated 0 traces, configuration should probably be adjusted", + ) + logger.write(Logger.Level.SUBSTEP, "-- Trace generation done --\n") + + return TraceGenerationResult(traceSetSummary) + } + + private fun filterEndNodes( + endNodes: List>, + badNodes: List>, + ): List> { + val filteredEndNodes: MutableList> = + ArrayList() // leaves that are not "bad nodes" or bad nodes' grandparents + endNodes.forEach( + Consumer { endNode: ArgNode -> + if (badNodes.contains(endNode)) { + if (endNode.parent.isPresent && endNode.parent.get().parent.isPresent) { + val parent = endNode.parent.get() + val grandParent = endNode.parent.get().parent.get() + // If the parent & grandparent (same state as the bad node) has no other successors, + // the grandparent is the "new leaf" + // if there are successors, there is no real leaf here + if (grandParent.outEdges.count() == 1L && parent.outEdges.count() == 1L) { + filteredEndNodes.add(grandParent) + } + } else { + throw RuntimeException( + "Unexpected error: bad nodes should always have parents and grandparents" + ) + } + } else { + filteredEndNodes.add(endNode) + } + } + ) + + return filteredEndNodes + } + + private fun computeCrossCoveredEndNodes( + filteredEndNodes: List> + ): List> { + val coveredEndNodes: MutableList> = ArrayList() + for (node in filteredEndNodes) { + if (node.isCovered) { + // and covered-by edge is a cross-edge: + val coveringNode = node.coveringNode.get() // check above with isCovered() + var parentNode = node.parent + var crossEdge = true + while (parentNode.isPresent) { + if (parentNode.get() == coveringNode) { + // not a cross edge + crossEdge = false + break + } + parentNode = parentNode.get().parent + } + + if (crossEdge) { + coveredEndNodes.add(node) + } + } + } + return coveredEndNodes + } + + /* + private fun modifyToFullTraces( + filteredEndNodes: List>, + argTraces: List> + ): List> { + val crossCoveredEndNodes = computeCrossCoveredEndNodes(filteredEndNodes) + // new traces + var newTraces: MutableList>> = ArrayList() // T' + for (argTrace in argTraces) { + newTraces.add(java.util.List.of(AdvancedArgTrace.to(argTrace.node(argTrace.nodes().size - 1)))) + } + + // now we iterate over the new traces until all of them are maximal + // TODO - lengthening the traces this way is far from being the most efficient, it can easily blow up + // some kind of smart collecting of partial traces "globally", instead of iteratively and then pairing all of + // them properly might be faster (not sure) + // but however we do this, the number of full traces in the result can easily blow up anyways, so I am not sure + // it would matter much + var tracesChanged = true + while (tracesChanged) { + tracesChanged = false + val changedTraces: MutableList>> = ArrayList() // T'' + for (newTrace in newTraces) { + val lastNode = getLastNode(newTrace) + if (crossCoveredEndNodes.contains(lastNode)) { // isCovered() check present + val coveringNode = lastNode.coveringNode.get() + // we can lengthen the new trace more + // and it can even branch, so we might add several new traces actually + // for (ArgTrace existingTrace : argTraces) { + for (existingTrace in argTraces) { + if (existingTrace.nodes().contains(coveringNode)) { + // getting a new part for the trace + val newPart = AdvancedArgTrace.fromTo( + coveringNode, + existingTrace.node(existingTrace.nodes().size - 1) + ) + val newPartLastNode = newPart.node(newPart.nodes().size - 1) + if (newPartLastNode.isCovered && !crossCoveredEndNodes.contains( + newPartLastNode + ) + ) { + tracesChanged = false + } else { + tracesChanged = true + val changedTrace = ArrayList(newTrace) + changedTrace.add(newPart) + changedTraces.add(changedTrace) + } + } + } + } else { + changedTraces.add(newTrace) + } + } + + if (tracesChanged) { + newTraces = changedTraces + } + } + + val result: MutableList> = ArrayList() // TODO should be a Set(?) + // concatenating lengthened maximal traces and converting them to state-action traces to add them to the result list + for (newTrace in newTraces) { + result.add(concatenateTraces(newTrace)) + } + + // adding traces that did not have to be lengthened to the resulting state-action trace list + */ + /* + for (ArgTrace argTrace : argTraces) { + if(!crossCoveredEndNodes.contains(argTrace.node(argTrace.nodes().size()-1))) { + result.add(argTrace.toTrace()); + } + } + */ + /* + + return result + } + */ + + // created for traces that are stored as a list (they are not concatenated yet) + private fun getLastNode(traceList: List>): ArgNode { + val traces = traceList[traceList.size - 1] + return traces.node(traces.nodes().size - 1) + } + + private fun concatenateTraces(parts: List>): Trace { + Preconditions.checkState(parts.size > 0) + val newTraceStates = ArrayList() + val newTraceActions = ArrayList() + for (part in parts) { + // Concatenating states + if (newTraceStates.size > 0) { + newTraceStates.removeAt(newTraceStates.size - 1) + } + newTraceStates.addAll(part.toTrace().states) + + // Concatenating actions + newTraceActions.addAll(part.toTrace().actions) + } + + return Trace.of(newTraceStates, newTraceActions) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt new file mode 100644 index 0000000000..977fd8b0e6 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt @@ -0,0 +1,255 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary + +import com.google.common.base.Preconditions.checkState +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.Proof +import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace + +class AbstractSummaryBuilder { + val argTraces: MutableList> = mutableListOf() + + fun addTrace(trace: ArgTrace) { + if (argTraces.isNotEmpty()) { + checkState( + argTraces.get(0).node(0) == trace.node(0), + "All traces in summary must start with the same node!", + ) + } + argTraces.add(trace) + } + + fun build(): AbstractTraceSummary { + checkState(argTraces.isNotEmpty(), "Summary must have at least one trace in it!") + + val argNodes: Set> = argTraces.map { trace -> trace.nodes() }.flatten().toSet() + + // grouping nodes covering each other for state summaries + val nodeGroups: MutableList>> = mutableListOf() + for (node in argNodes) { + if (nodeGroups.isEmpty()) { + nodeGroups.add(mutableSetOf(node)) + } else { + val inCoverRelationWithNode: MutableList> = mutableListOf() + inCoverRelationWithNode.addAll(node.coveredNodes.toList()) + if (node.coveringNode.isPresent) inCoverRelationWithNode.add(node.coveringNode.get()) + + val nodeGroup = + nodeGroups + .filter( + fun(group: MutableSet>): Boolean { + for (coverNode in inCoverRelationWithNode) { + if (group.contains(coverNode)) { + return true + } + } + return false + } + ) + .toList() + + checkState( + nodeGroup.size <= 1 + ) // either found one where node would fit OR found none and will create new one + if (nodeGroup.size > 0) { + nodeGroup[0].add(node) + } else { + nodeGroups.add(mutableSetOf(node)) + } + } + } + + // create summary nodes + + val argNodeSummaryNodeMap = mutableMapOf, AbstractSummaryNode>() + for (nodeGroup in nodeGroups) { + val summaryNode = AbstractSummaryNode.create(nodeGroup) + for (node in nodeGroup) { + argNodeSummaryNodeMap[node] = summaryNode + } + } + val summaryNodes = argNodeSummaryNodeMap.values.toSet() + val initSummaryNodes = + summaryNodes.filter { summaryNode -> argTraces.get(0).node(0) in summaryNode.argNodes } + checkState(initSummaryNodes.size == 1, "Initial arg node must be in exactly 1 summary node!") + val initNode = initSummaryNodes.get(0) + + val abstractSummaryEdges = mutableSetOf>() + // save edges as well, so we can easily connect edge sources and targets + for (summaryNode in summaryNodes) { + for (argNode in summaryNode.argNodes) { + for (edge in argNode.outEdges) { + if (edge.target in argNodes) { + // summary edge adds itself to source and target as well + abstractSummaryEdges.add( + AbstractSummaryEdge.create(edge, summaryNode, argNodeSummaryNodeMap[edge.target]!!) + ) + } + } + } + } + + return AbstractTraceSummary(argTraces, abstractSummaryEdges, summaryNodes, initNode) + } +} + +/** + * This class represents an automata, similar to an ARG, where covered and covering nodes are merged + * into a single node (which we thus call a summary node). In some sense this class represents a + * wrapper level over a set of arg traces. + */ +data class AbstractTraceSummary( + val sourceTraces: Collection>, + val abstractSummaryEdges: Collection>, + val summaryNodes: Collection>, + val initNode: AbstractSummaryNode, +) : Proof {} + +/** + * Groups arg nodes based on coverages, but also stores the traces they appear in, coverage + * relations and arg nodes + */ +class AbstractSummaryNode +private constructor( + val id: Long, + val argNodes: Set>, + val leastOverApproximatedNode: ArgNode, + val mostOverApproximatedNode: ArgNode, +) { + // not immutable for edges, as both source and target has to exist when creating edge :c + var inEdges: MutableSet> = mutableSetOf() + var outEdges: MutableSet> = mutableSetOf() + + companion object { + var counter: Long = 0 + + fun create( + argNodes: MutableSet> + ): AbstractSummaryNode { + // all of the nodes should be in some kind of coverage relationship with each other, + // otherwise, split this summary node + for (node in argNodes) { + for (node2 in argNodes) { + if (node != node2) { + // ancestors & subsumed irrelevant here + if (!node.inPartialOrder(node2) && !node2.inPartialOrder(node)) { + TODO("split summary node") + } + } + } + } + + val notCoveredNodes = argNodes.filter { argNode -> argNode.coveringNode.isEmpty } + var leastOverApproximatedNode = + notCoveredNodes[0] // just get one of them, does not matter, which + + for (node in notCoveredNodes) { + if (leastOverApproximatedNode != node) { + // ancestors irrelevant here, subsumed should not be checked + if (node.inPartialOrder(leastOverApproximatedNode)) { + // node can cover the so far "least over approximated" node - node is more "abstract" + leastOverApproximatedNode = node + } else if (!leastOverApproximatedNode.inPartialOrder(node)) { + throw RuntimeException("All nodes in summary node should be in some partial ordering!") + } + } + } + + val notCoveringNodes = + argNodes.filter { argNode -> + argNode.coveredNodes.filter { node -> node in argNodes }.count() == 0L + } + var mostOverApproximatedNode = notCoveringNodes[0] + + for (node in notCoveringNodes) { + if (mostOverApproximatedNode != node) { + // ancestors irrelevant here, subsumed should not be checked + if (mostOverApproximatedNode.inPartialOrder(node)) { + // so far "most over approximated" node can cover this node - this node is more abstract + mostOverApproximatedNode = node + } else if (!node.inPartialOrder(mostOverApproximatedNode)) { + throw RuntimeException("All nodes in summary node should be in some partial ordering!") + } + } + } + + return AbstractSummaryNode( + counter++, + argNodes, + leastOverApproximatedNode, + mostOverApproximatedNode, + ) + } + } + + fun getStates(): Set { + return argNodes.map { argNode -> argNode.state }.toSet() + } + + fun getLabel(): String { + val sb = StringBuilder() + + for (node in argNodes) { + val label = node.state.toString() + if (label !in sb) { + sb.append(label) + } + } + + return sb.toString() + } + + override fun toString(): String { + return getLabel() + } + + fun addOutEdge(abstractSummaryEdge: AbstractSummaryEdge) { + outEdges.add(abstractSummaryEdge) + } + + fun addInEdge(abstractSummaryEdge: AbstractSummaryEdge) { + inEdges.add(abstractSummaryEdge) + } +} + +class AbstractSummaryEdge +private constructor( + val argEdge: ArgEdge, + val source: AbstractSummaryNode, + val target: AbstractSummaryNode, + val action: A = argEdge.action, +) { + companion object { + fun create( + argEdge: ArgEdge, + source: AbstractSummaryNode, + target: AbstractSummaryNode, + ): AbstractSummaryEdge { + val abstractSummaryEdge = AbstractSummaryEdge(argEdge, source, target) + source.addOutEdge(abstractSummaryEdge) + target.addInEdge(abstractSummaryEdge) + return abstractSummaryEdge + } + } + + fun getLabel(): String { + return argEdge.action.toString() + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt new file mode 100644 index 0000000000..3a2117ea3f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt @@ -0,0 +1,31 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.core.model.Valuation + +class ConcreteSummary( + val valuationMap: MutableMap, Valuation>, + val summary: AbstractTraceSummary, +) { + // TODO check that every node has a valuation? + + fun getValuation(node: AbstractSummaryNode): Valuation { + return valuationMap[node]!! + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt new file mode 100644 index 0000000000..a40f289070 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt @@ -0,0 +1,185 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.expr.refinement + +import com.google.common.base.Preconditions +import com.google.common.base.Preconditions.checkState +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.* +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.solver.ItpMarker +import hu.bme.mit.theta.solver.ItpSolver +import java.util.* + +/** + * ExprTraceChecker modified to concretize summaries (interconnected traces) instead of a single + * trace. It generates a binary interpolant by incrementally checking the traces forward. + */ +class ExprSummaryFwBinItpChecker private constructor(init: Expr, solver: ItpSolver) { + private val solver: ItpSolver = Preconditions.checkNotNull(solver) + private val init: Expr = Preconditions.checkNotNull(init) + private var nPush: Int = 0 + + // TODO what presumptions do we have about state and trace feasibility? Does it matter? + // TODO will binitp work? see notes + /** + * @return a summary edge, which, if present, represents the step where we start to have + * infeasibility, and map of the updated indexings + */ + fun addNodeToSolver( + currentNode: AbstractSummaryNode, + A: ItpMarker, + indexingMap: Map, VarIndexing>, + ): Pair< + Optional>, + MutableMap, VarIndexing>, + > { + var currentIndexingMap: + MutableMap, VarIndexing> = + indexingMap.toMutableMap() + + for (edge in currentNode.outEdges) { + solver.push() + nPush++ + + // if target is already in the indexings, then we just ran into a loop + val loopClosing = edge.target in currentIndexingMap.keys + + if (!loopClosing) { + currentIndexingMap[edge.target] = + currentIndexingMap[edge.source]!!.add(edge.action.nextIndexing()) + } + solver.add( + A, + PathUtils.unfold( + edge.target.leastOverApproximatedNode.state.toExpr(), + currentIndexingMap[edge.target], + ), + ) + solver.add(A, PathUtils.unfold(edge.action.toExpr(), currentIndexingMap[edge.source])) + if (solver.check().isSat) { + if (!loopClosing) { + val result = addNodeToSolver(edge.target, A, currentIndexingMap) + currentIndexingMap = result.second + + if (result.first.isPresent) { // reached unsat + // in one of the recursive calls, reached unsat step (see else branch below) + return Pair(result.first, currentIndexingMap) + } + } + } else { + solver.pop() + nPush-- + return Pair(Optional.of(edge), currentIndexingMap) + } + } + + // we recursively went down on this branch, time to go one up + return Pair(Optional.empty(), currentIndexingMap) + } + + fun check(summary: AbstractTraceSummary): ExprSummaryStatus { + Preconditions.checkNotNull(summary) + val summaryNodeCount = summary.summaryNodes.size + + val indexingMap: MutableMap, VarIndexing> = + mutableMapOf() + indexingMap[summary.initNode] = VarIndexingFactory.indexing(0) + + solver.push() + nPush++ + + val A = solver.createMarker() + val B = solver.createMarker() + val pattern = solver.createBinPattern(A, B) + + solver.add(A, PathUtils.unfold(init, indexingMap[summary.initNode])) + solver.add( + A, + PathUtils.unfold( + summary.initNode.leastOverApproximatedNode.state!!.toExpr(), + indexingMap[summary.initNode], + ), + ) + assert(solver.check().isSat) { "Initial state of the trace is not feasible" } + + // iterate through summary - take care of branchings + val result = addNodeToSolver(summary.initNode, A, indexingMap) + val updatedIndexingMap = result.second + val concretizable = result.first.isEmpty + + // concretizable case: we don't have a target, thus we don't even need B in this case + val status = + if (concretizable) { + val model = solver.model + val valuations = + mutableMapOf, Valuation>() + for ((node, indexing) in updatedIndexingMap.entries) { + valuations[node] = PathUtils.extractValuation(model, indexing) + } + + val concreteSummary = ConcreteSummary(valuations, summary) + FeasibleExprSummaryStatus(concreteSummary) + } else { + checkState( + result.first.isPresent, + "If summary not concretizable, border edge must be present!", + ) + val borderEdge = result.first.get() + + solver.add( + B, + PathUtils.unfold( + borderEdge.target.leastOverApproximatedNode.state.toExpr(), + updatedIndexingMap[borderEdge.target], + ), + ) + solver.add( + B, + PathUtils.unfold(borderEdge.action.toExpr(), updatedIndexingMap[borderEdge.source]), + ) + solver.check() + checkState(solver.status.isUnsat, "Trying to interpolate a feasible formula") + + val interpolant = solver.getInterpolant(pattern) + val itpFolded: Expr = + PathUtils.foldin(interpolant.eval(A), updatedIndexingMap[borderEdge.source]) + + InfeasibleExprSummaryStatus(itpFolded) + } + + solver.pop(nPush) + + return status + } + + override fun toString(): String { + return javaClass.simpleName + } + + companion object { + + fun create(init: Expr, solver: ItpSolver): ExprSummaryFwBinItpChecker { + return ExprSummaryFwBinItpChecker(init, solver) + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt new file mode 100644 index 0000000000..442638f3d2 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt @@ -0,0 +1,28 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolType + +abstract class ExprSummaryStatus(val feasible: Boolean) + +class FeasibleExprSummaryStatus(val summary: ConcreteSummary) : + ExprSummaryStatus(true) + +class InfeasibleExprSummaryStatus(val itp: Expr) : ExprSummaryStatus(false) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt new file mode 100644 index 0000000000..5f70fc08fb --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt @@ -0,0 +1,35 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.Result +import hu.bme.mit.theta.analysis.algorithm.Statistics +import java.util.* + +class TraceGenerationResult, S : State, A : Action>( + val summary: Pr +) : Result { + + override fun getProof(): Pr { + return summary + } + + override fun getStats(): Optional { + return Optional.empty() + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt new file mode 100644 index 0000000000..3c3e28f96b --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt @@ -0,0 +1,73 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.utils + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.common.visualization.EdgeAttributes +import hu.bme.mit.theta.common.visualization.Graph +import hu.bme.mit.theta.common.visualization.LineStyle +import hu.bme.mit.theta.common.visualization.NodeAttributes +import java.awt.Color + +/** + * This class visualizes not single traces, but a group of traces, connected by trace metadata. The + * result is an automata-like summary of executions. + */ +object AbstractTraceSummaryVisualizer { + val lineStyle: LineStyle = LineStyle.NORMAL + val fillColor: Color = Color.WHITE + val lineColor: Color = Color.BLACK + + // TODO TraceVisualizer has an unused, similar part (visualizeMerged) + // it does not use metadata, but visualizes a collection of traces + // (ie, it is not completely the same as TraceSummaryVisualizer::visualize) + fun visualize( + abstractTraceSummary: AbstractTraceSummary, + traceSummaryId: String = "trace_summary", + traceSummaryLabel: String = "Trace Summary", + ): Graph { + val graph: Graph = Graph(traceSummaryId, traceSummaryLabel) + + // add nodes + val stateNodeSummaries = abstractTraceSummary.summaryNodes + for (stateNodeSummary in stateNodeSummaries) { + val nAttribute = + NodeAttributes.builder() + .label(stateNodeSummary.getLabel()) + .fillColor(fillColor) + .lineColor(lineColor) + .lineStyle(lineStyle) + .build() + + graph.addNode(stateNodeSummary.id.toString(), nAttribute) + } + + for (summaryEdge in abstractTraceSummary.abstractSummaryEdges) { + val eAttribute = + EdgeAttributes.builder() + .label(summaryEdge.getLabel()) + .color(lineColor) + .lineStyle(lineStyle) + .build() + + graph.addEdge(summaryEdge.source.id.toString(), summaryEdge.target.id.toString(), eAttribute) + } + + return graph + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarChangerUtils.kt b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarChangerUtils.kt new file mode 100644 index 0000000000..52c2ada913 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarChangerUtils.kt @@ -0,0 +1,70 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.utils + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.utils.TypeUtils.cast + +fun Stmt.changeVars(variableMapping: Map>): Stmt { + return when (this) { + is AssignStmt<*> -> + AssignStmt.of( + cast(varDecl.changeVars(variableMapping), varDecl.type), + cast(expr.changeVars(variableMapping), varDecl.type), + ) + + is HavocStmt<*> -> HavocStmt.of(varDecl.changeVars(variableMapping)) + is AssumeStmt -> AssumeStmt.of(cond.changeVars(variableMapping)) + is SequenceStmt -> SequenceStmt.of(stmts.map { it.changeVars(variableMapping) }) + is SkipStmt -> this + is NonDetStmt -> NonDetStmt.of(stmts.map { it.changeVars(variableMapping) }) + is LoopStmt -> + LoopStmt.of( + stmt.changeVars(variableMapping), + loopVariable.changeVars(variableMapping), + from.changeVars(variableMapping), + to.changeVars(variableMapping), + ) + + is IfStmt -> + IfStmt.of( + cond.changeVars(variableMapping), + then.changeVars(variableMapping), + elze.changeVars(variableMapping), + ) + + else -> TODO("Not yet implemented") + } +} + +fun Expr.changeVars(variableMapping: Map>): Expr = + if (this is RefExpr) { + when (this.decl) { + is VarDecl -> (this.decl as VarDecl).changeVars(variableMapping).ref + else -> this + } + } else this.withOps(this.ops.map { it.changeVars(variableMapping) }) + +@SuppressWarnings("kotlin:S6530") +fun VarDecl.changeVars(variableMapping: Map>): VarDecl { + val swap = variableMapping[this.name] ?: return this + if (swap.type != this.type) throw RuntimeException("Can't change variable to different type") + return swap as VarDecl +} diff --git a/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt b/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt deleted file mode 100644 index 31838601b9..0000000000 --- a/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt +++ /dev/null @@ -1,66 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.core.utils - -import hu.bme.mit.theta.core.decl.VarDecl -import hu.bme.mit.theta.core.stmt.* -import hu.bme.mit.theta.core.type.Expr -import hu.bme.mit.theta.core.type.Type -import hu.bme.mit.theta.core.type.anytype.RefExpr -import hu.bme.mit.theta.core.utils.TypeUtils.cast - -fun Stmt.changeVars(variableMapping: Map>): Stmt { - return when (this) { - is AssignStmt<*> -> AssignStmt.of( - cast(varDecl.changeVars(variableMapping), varDecl.type), - cast(expr.changeVars(variableMapping), varDecl.type) - ) - - is HavocStmt<*> -> HavocStmt.of(varDecl.changeVars(variableMapping)) - is AssumeStmt -> AssumeStmt.of(cond.changeVars(variableMapping)) - is SequenceStmt -> SequenceStmt.of(stmts.map { it.changeVars(variableMapping) }) - is SkipStmt -> this - is NonDetStmt -> NonDetStmt.of(stmts.map { it.changeVars(variableMapping) }) - is LoopStmt -> LoopStmt.of( - stmt.changeVars(variableMapping), loopVariable.changeVars(variableMapping), - from.changeVars(variableMapping), to.changeVars(variableMapping) - ) - - is IfStmt -> IfStmt.of( - cond.changeVars(variableMapping), then.changeVars(variableMapping), - elze.changeVars(variableMapping) - ) - - else -> TODO("Not yet implemented") - } -} - -fun Expr.changeVars(variableMapping: Map>): Expr = - if (this is RefExpr) { - when (this.decl) { - is VarDecl -> (this.decl as VarDecl).changeVars(variableMapping).ref - else -> this - } - } else this.withOps(this.ops.map { it.changeVars(variableMapping) }) - -@SuppressWarnings("kotlin:S6530") -fun VarDecl.changeVars(variableMapping: Map>): VarDecl { - val swap = variableMapping[this.name] ?: return this - if (swap.type != this.type) - throw RuntimeException("Can't change variable to different type") - return swap as VarDecl -} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/README.md b/subprojects/frontends/promela-frontend/README.md new file mode 100644 index 0000000000..25a9f7dfbe --- /dev/null +++ b/subprojects/frontends/promela-frontend/README.md @@ -0,0 +1,3 @@ +# ANTLR-Based Promela Frontend for Verification + +This subproject adds an ANTLR-grammar based Promela frontend to Theta. This is independent of any formalism, and aims to be as widely applicable as possible. \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/build.gradle.kts b/subprojects/frontends/promela-frontend/build.gradle.kts new file mode 100644 index 0000000000..13604673bb --- /dev/null +++ b/subprojects/frontends/promela-frontend/build.gradle.kts @@ -0,0 +1,24 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +plugins { + id("kotlin-common") + id("antlr-grammar") +} +dependencies { + implementation(project(":theta-core")) + implementation(project(":theta-common")) + implementation(project(":theta-grammar")) +} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/antlr/promela.g4 b/subprojects/frontends/promela-frontend/src/main/antlr/promela.g4 new file mode 100644 index 0000000000..b05bee2d81 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/antlr/promela.g4 @@ -0,0 +1,229 @@ +grammar promela; +/** + source: https://spinroot.com/spin/Man/grammar.html + + WARNING only works on PREPROCESSSED promela files (no #define), + use cpp -p to preprocess promela file with macros + + the implementation is only partial, + thus unsupported language elements are commented out +*/ + +spec: (module(Separator)*)+; + +module: proctype + | init + //| never + //| trace + | utype + | mtype + | decl_lst; + +proctype +// : (active)? 'proctype' Name '(' (decl_lst)? ')' (priority)? (enabler)? '{' sequence '}'; + : 'proctype' Name '(' (decl_lst)? ')' '{' sequence '}'; + +//init : 'init' (priority)? '{' sequence '}'; +init: 'init' '{' sequence '}'; + +//never : 'never' '{' sequence '}'; + +//trace : 'trace' '{' sequence '}'; + +utype: 'typedef' Name '{' decl_lst '}'; + +mtype: 'mtype' '='? '{' Name (',' Name)* '}'; + +decl_lst: one_decl (Separator one_decl)*; + +one_decl +// : (visible)? typename ivar (',' ivar)* +// | (visible)? unsigned_decl; + : typename ivar (',' ivar)* + | unsigned_decl; + +unsigned_decl + : 'unsigned' Name ':' Const('=' any_expr)?; + +typename +// : 'bit' | 'bool' | 'byte' | 'short' | 'int' | 'mtype' | 'chan' | Name; + : 'bit' | 'bool' | 'byte' | 'int' | 'chan' | Name; + +//active: 'active' '['Const']'; + +//priority: 'priority' Const; + +//enabler : 'provided' '(' expr ')'; + +//visible : 'hidden' | 'show'; + +sequence: step Separator? (step Separator?)*; // after e.g., atomic {} no separator, after decl separator + +step : stmnt ('unless' stmnt)? # stmnts + | decl_lst # declLst + | ('xr') varref (',' varref)* # xr + //| ('xs') varref (',' varref)* # xs + ; + +ivar : Name ('['Const']')? (('=' any_expr)|('=' ch_init))?; + +ch_init : '['Const']' 'of' '{' typename (',' typename)* '}'; + +varref : Name ('[' any_expr ']')? ('.' varref)?; + +send : varref '!' send_args + | varref '!!' send_args; + +receive : varref '?' recv_args + | varref '??' recv_args + | varref '?' '<' recv_args '>' + | varref '??' '<' recv_args '>'; + +poll : varref '?' '[' recv_args ']' + | varref '??' '[' recv_args ']'; + +send_args: arg_lst | any_expr '(' arg_lst ')'; + +arg_lst : any_expr (',' any_expr)*; + +recv_args: recv_arg (',' recv_arg)* | recv_arg '(' recv_args ')'; + +recv_arg: varref | 'eval' '(' varref ')' | ('-')? Const; + +assign : varref '=' any_expr + | varref '++' + | varref '--'; + +stmnt : 'if' promela_options 'fi' # ifStmnt + | 'do' promela_options 'od' # doStmnt + | 'for' '(' range ')' '{' sequence '}' # forStmnt + | 'atomic' '{' sequence '}' # atomicStmnt + //| 'd_step' '{' sequence '}' # dstepStmnt + | 'select' '(' range ')' # selectStmnt + | '{' sequence '}' # sequenceStmnt + | send # sendStmnt + | receive # receiveStmnt + | assign # assignStmnt + | 'else' # elseStmnt + | 'break' # breakStmnt + | 'goto' Name # gotoStmnt + | Name ':' stmnt # nameStmnt + //| 'print' '(' String (',' arg_lst)? ')' # printStmnt + | 'assert' expr # assertStmnt + | expr # exprStmnt + ; + +range : Name ':' any_expr '..' any_expr + | Name 'in' Name; + +promela_options : ('::' sequence)+; + +binarop : '+' | '-' | '*' | '/' | '%' + | '&' | '^' | '|' + | '>' | '<' | '>=' | '<=' | '==' | '!=' + | '<<' | '>>' | AndAnd | OrOr; + +unarop : '~' | '-' | '!'; + +any_expr: '(' any_expr ')' # ParenthesesAnyExpr + | any_expr binarop any_expr # BinaryAnyExpr + | unarop any_expr # UnaryAnyExpr + | '(' any_expr '->' any_expr ':' any_expr ')' # ImplAnyExpr + | 'len' '(' varref ')' # LenAnyExpr + | poll # PollAnyExpr + | varref # VarrefAnyExpr + | Const # ConstAnyExpr + | 'run' Name '(' (arg_lst)? ')' # RunAnyExpr + // | 'timeout' + // | 'np_' + //| 'enabled' '(' any_expr ')' + //| 'pc_value' '(' any_expr ')' + //| Name '[' any_expr ']' '@' Name + //| 'run' Name '(' (arg_lst)? ')' (priority)? + //| 'get_priority' '(' expr ')' + //| 'set_priority' '(' expr ',' expr ')' + ; + +expr : any_expr # Any_exprExpr + | '(' expr ')' # ParenthesesExpr + | expr (AndAnd|OrOr) expr # AndorExpr + ; +// | chanpoll '(' varref ')'; + +//chanpoll: 'full' | 'empty' | 'nfull' | 'nempty'; + +String : '"' ~["]* '"'; + +Name : Alpha (Alpha|Number)*; + +Const : 'true' | 'false' | 'skip' | (Number)+; // seems like it's always signed based on the grammar..? + +Alpha : [a-zA-Z_]; // grammar is case insensitive, A-Z is superfluous + +Number : [0-9]; + +LeftParen : '('; +RightParen : ')'; +LeftBracket : '['; +RightBracket : ']'; +LeftBrace : '{'; +RightBrace : '}'; + +Less : '<'; +LessEqual : '<='; +Greater : '>'; +GreaterEqual : '>='; +LeftShift : '<<'; +RightShift : '>>'; + +Plus : '+'; +PlusPlus : '++'; +Minus : '-'; +MinusMinus : '--'; +Star : '*'; +Div : '/'; +Mod : '%'; + +And : '&'; +Or : '|'; +AndAnd : '&&'; +OrOr : '||'; +Caret : '^'; +Not : '!'; +Tilde : '~'; + +Separator: Semi | Arrow; + +Question : '?'; +Colon : ':'; +DoubleColon : Colon Colon; +Semi : ';'; +Comma : ','; + +Assign : '='; +StarAssign : '*='; +DivAssign : '/='; +ModAssign : '%='; +PlusAssign : '+='; +MinusAssign : '-='; +LeftShiftAssign : '<<='; +RightShiftAssign : '>>='; +AndAssign : '&='; +XorAssign : '^='; +OrAssign : '|='; + +Equal : '=='; +NotEqual : '!='; + +Arrow : '->'; +Dot : '.'; +Underscore : '_'; + +COMMENT + : '#' ~[\r\n]* -> skip // Match and skip comments starting with '#' + ; + +WS + : [ \t\n]+ + -> skip + ; \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/config/PromelaConfiguration.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/config/PromelaConfiguration.kt new file mode 100644 index 0000000000..0651ec3e14 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/config/PromelaConfiguration.kt @@ -0,0 +1,10 @@ +package hu.bme.mit.theta.frontend.promela.config + +import java.math.BigInteger + +sealed class PromelaConfiguration ( + // bit widths of types + val UCHAR_BIT : Int, // unsigned + val SHRT_BIT : Int, // signed + val INT_BIT : Int, // signed +) \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/ExpressionVisitors.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/ExpressionVisitors.kt new file mode 100644 index 0000000000..25e692825e --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/ExpressionVisitors.kt @@ -0,0 +1,86 @@ +package hu.bme.mit.theta.frontend.promela.grammar + +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs +import hu.bme.mit.theta.core.type.bvtype.BvExprs +import hu.bme.mit.theta.core.type.bvtype.BvType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.frontend.promela.config.PromelaConfiguration +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaBaseVisitor +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaParser +import java.math.BigInteger +import java.util.* + +// Used both for rules expr and any_expr +class ExprVisitor(val config : PromelaConfiguration) : promelaBaseVisitor>() { + override fun visitAny_exprExpr(ctx: promelaParser.Any_exprExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitParenthesesExpr(ctx: promelaParser.ParenthesesExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitAndorExpr(ctx: promelaParser.AndorExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitBinaryAnyExpr(ctx: promelaParser.BinaryAnyExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitUnaryAnyExpr(ctx: promelaParser.UnaryAnyExprContext?): Expr<*> { + val expr = ctx!!.any_expr().accept(this) + when (ctx.unarop().text) { + "~" -> { + @Suppress("UNCHECKED_CAST") + val negExpr: Expr<*> = BvExprs.Not(expr as Expr?) + } + "-" -> { + val negExpr: Expr<*> = AbstractExprs.Neg(expr) + } + "!" -> { + val negExpr = AbstractExprs.Ite( + AbstractExprs.Eq( + expr, + CComplexType.getType(expr, parseContext).getNullValue() + ), signedInt.getUnitValue(), signedInt.getNullValue() + ) + } + else -> { + throw RuntimeException("Unary operator does not exist") + } + } + } + + override fun visitImplAnyExpr(ctx: promelaParser.ImplAnyExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitLenAnyExpr(ctx: promelaParser.LenAnyExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitPollAnyExpr(ctx: promelaParser.PollAnyExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitVarrefAnyExpr(ctx: promelaParser.VarrefAnyExprContext?): Expr<*> { + throw NotImplementedError() + } + + override fun visitConstAnyExpr(ctx: promelaParser.ConstAnyExprContext?): Expr<*> { + val text = ctx!!.text.lowercase(Locale.getDefault()) + when (text) { + "false" -> { throw NotImplementedError() } + "true" -> { throw NotImplementedError() } + "skip" -> { throw NotImplementedError() } + else -> { + val value = BigInteger(text, 10) + // TODO we do not support Bv arithmetics - disable it on an upper level + return IntExprs.Int(value) + } + } + } +} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/SequenceVisitors.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/SequenceVisitors.kt new file mode 100644 index 0000000000..6e6b571460 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/SequenceVisitors.kt @@ -0,0 +1,33 @@ +package hu.bme.mit.theta.frontend.promela.grammar + +import hu.bme.mit.theta.frontend.promela.model.* +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaBaseVisitor +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaParser + +class SequenceVisitor : promelaBaseVisitor() { + val stepVisitor = StepVisitor() + + override fun visitSequence(ctx: promelaParser.SequenceContext?): Sequence { + val steps = ctx!!.step().map { it.accept(stepVisitor) }.toList() + } +} + +class StepVisitor(val decl_lstVisitor : Decl_lstVisitor) : promelaBaseVisitor() { + val statementVisitor = StatementVisitor() + + override fun visitStmnts(ctx: promelaParser.StmntsContext?): Step { + return StmntsStep(ctx!!.stmnt().map { it.accept(statementVisitor) }.toList()) + } + + override fun visitDeclLst(ctx: promelaParser.DeclLstContext?): Step { + return DeclListStep(ctx!!.decl_lst().accept(decl_lstVisitor)) + } + + override fun visitXr(ctx: promelaParser.XrContext?): Step { + throw NotImplementedError() + } + + override fun visitXs(ctx: promelaParser.XsContext?): Step { + throw NotImplementedError() + } +} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/StatementVisitor.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/StatementVisitor.kt new file mode 100644 index 0000000000..648f75cf4f --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/StatementVisitor.kt @@ -0,0 +1,75 @@ +package hu.bme.mit.theta.frontend.promela.grammar + +import hu.bme.mit.theta.frontend.promela.model.Statement +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaBaseVisitor +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaParser + +class StatementVisitor : promelaBaseVisitor() { + override fun visitIfStmnt(ctx: promelaParser.IfStmntContext?): Statement { + return super.visitIfStmnt(ctx) + } + + override fun visitDoStmnt(ctx: promelaParser.DoStmntContext?): Statement { + return super.visitDoStmnt(ctx) + } + + override fun visitForStmnt(ctx: promelaParser.ForStmntContext?): Statement { + return super.visitForStmnt(ctx) + } + + override fun visitAtomicStmnt(ctx: promelaParser.AtomicStmntContext?): Statement { + return super.visitAtomicStmnt(ctx) + } + + override fun visitDstepStmnt(ctx: promelaParser.DstepStmntContext?): Statement { + return super.visitDstepStmnt(ctx) + } + + override fun visitSelectStmnt(ctx: promelaParser.SelectStmntContext?): Statement { + return super.visitSelectStmnt(ctx) + } + + override fun visitSequenceStmnt(ctx: promelaParser.SequenceStmntContext?): Statement { + return super.visitSequenceStmnt(ctx) + } + + override fun visitSendStmnt(ctx: promelaParser.SendStmntContext?): Statement { + return super.visitSendStmnt(ctx) + } + + override fun visitReceiveStmnt(ctx: promelaParser.ReceiveStmntContext?): Statement { + return super.visitReceiveStmnt(ctx) + } + + override fun visitAssignStmnt(ctx: promelaParser.AssignStmntContext?): Statement { + return super.visitAssignStmnt(ctx) + } + + override fun visitElseStmnt(ctx: promelaParser.ElseStmntContext?): Statement { + return super.visitElseStmnt(ctx) + } + + override fun visitBreakStmnt(ctx: promelaParser.BreakStmntContext?): Statement { + return super.visitBreakStmnt(ctx) + } + + override fun visitGotoStmnt(ctx: promelaParser.GotoStmntContext?): Statement { + return super.visitGotoStmnt(ctx) + } + + override fun visitNameStmnt(ctx: promelaParser.NameStmntContext?): Statement { + return super.visitNameStmnt(ctx) + } + + override fun visitPrintStmnt(ctx: promelaParser.PrintStmntContext?): Statement { + return super.visitPrintStmnt(ctx) + } + + override fun visitAssertStmnt(ctx: promelaParser.AssertStmntContext?): Statement { + return super.visitAssertStmnt(ctx) + } + + override fun visitExprStmnt(ctx: promelaParser.ExprStmntContext?): Statement { + return super.visitExprStmnt(ctx) + } +} diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/TopVisitors.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/TopVisitors.kt new file mode 100644 index 0000000000..5601dd7a9f --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/TopVisitors.kt @@ -0,0 +1,92 @@ +package hu.bme.mit.theta.frontend.promela.grammar + +import hu.bme.mit.theta.frontend.promela.model.* +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaBaseVisitor +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaParser + +class SpecVisitor : promelaBaseVisitor() { + override fun visitSpec(ctx: promelaParser.SpecContext): Spec { + return Spec(ctx.module().map { ModuleVisitor().visitModule(it) }) + } +} + +// TODO add fixed single visitors for each visitor class used +class ModuleVisitor : promelaBaseVisitor() { + override fun visitModule(ctx: promelaParser.ModuleContext): Module { + return when { + ctx.proctype() != null -> ctx.proctype().accept(ProctypeVisitor()) + ctx.init() != null -> InitVisitor().visitInit(ctx.init()) + ctx.never() != null -> visitNever(ctx.never()) // TODO add accept and classes + ctx.trace() != null -> visitTrace(ctx.trace()) + ctx.utype() != null -> visitUtype(ctx.utype()) + ctx.mtype() != null -> visitMtype(ctx.mtype()) + ctx.decl_lst() != null -> visitDecl_lst(ctx.decl_lst()) + else -> throw RuntimeException("Module should not have any other subclasses") + } + } +} + +class ProctypeVisitor : promelaBaseVisitor() { + override fun visitProctype(ctx: promelaParser.ProctypeContext): Proctype { + val active = ctx.active()?.Const()?.text + val name = ctx.Name().text + val declList = ctx.decl_lst()?.accept(Decl_lstVisitor()) + val priority = ctx.priority()?.Const()?.text + val enabler = ctx.enabler()?.expr()?.text + val sequence = ctx.sequence().step().map { it.accept() } + return Proctype(active, name, declList, priority, enabler, sequence) + } +} + +class InitVisitor : promelaBaseVisitor() { + override fun visitInit(ctx: promelaParser.InitContext): Init { + val priority = ctx.priority()?.Const()?.text + val sequence = ctx.sequence().step().map { it.accept(this) } + return Init(priority, sequence) + } +} + +class NeverVisitor : promelaBaseVisitor() { + override fun visitNever(ctx: promelaParser.NeverContext): Never { + val sequence = ctx.sequence().step().map { it.accept(this) } + return Never(sequence) + } +} + +class TraceVisitor : promelaBaseVisitor() { + override fun visitTrace(ctx: promelaParser.TraceContext): Trace { + val sequence = ctx.sequence().step().map { it.accept(this) } + return Trace(sequence) + } +} + +class UtypeVisitor : promelaBaseVisitor() { + override fun visitUtype(ctx: promelaParser.UtypeContext): Utype { + val name = ctx.Name().text + val declList = ctx.decl_lst().accept(this) as DeclList + return Utype(name, declList) + } +} + +class MtypeVisitor : promelaBaseVisitor() { + override fun visitMtype(ctx: promelaParser.MtypeContext): Mtype { + val names = ctx.Name().map { it.text } + return Mtype(names) + } +} + +class Decl_lstVisitor : promelaBaseVisitor() { + val oneDeclVisitor = OneDeclVisitor() + override fun visitDecl_lst(ctx: promelaParser.Decl_lstContext): DeclList { + val declarations = ctx.one_decl().map { it.accept(oneDeclVisitor) } + + } +} + +class OneDeclVisitor(val exprVisitor : ExprVisitor) : promelaBaseVisitor() { + val variableInitVisitor = VariableInitVisitor(exprVisitor) + override fun visitOne_decl(ctx: promelaParser.One_declContext?): OneDecl { + ctx!!.typename() + ctx.ivar().map { it.accept(variableInitVisitor) } + } +} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/VariableVisitor.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/VariableVisitor.kt new file mode 100644 index 0000000000..28289298ee --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/grammar/VariableVisitor.kt @@ -0,0 +1,24 @@ +package hu.bme.mit.theta.frontend.promela.grammar + +import hu.bme.mit.theta.frontend.promela.model.PromelaExpression +import hu.bme.mit.theta.frontend.promela.model.Variable +import hu.bme.mit.theta.frontend.promela.model.VariableInitialization +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaBaseVisitor +import hu.bme.mit.theta.promela.frontend.dsl.gen.promelaParser + +class VariableInitVisitor(val exprVisitor : ExprVisitor) : promelaBaseVisitor() { + override fun visitIvar(ctx: promelaParser.IvarContext?): VariableInitialization { + val name = ctx!!.Name().text + if (ctx.Const() != null) { + // TODO array init + throw NotImplementedError() + } + if (ctx.ch_init() != null) { + // TODO ch init + throw NotImplementedError() + } else { + val promelaExpression : PromelaExpression = ctx.any_expr().accept(exprVisitor) + return VariableInitialization(Variable(name), promelaExpression) + } + } +} \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Declarations.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Declarations.kt new file mode 100644 index 0000000000..e546c2bad0 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Declarations.kt @@ -0,0 +1,19 @@ +package hu.bme.mit.theta.frontend.promela.model + +data class DeclList(val declarations: List) + +sealed class Declaration + +data class TypedDeclaration( + val visible: String?, + val typeName: String, + val variables: List +) : Declaration() + +data class UnsignedDeclaration( + val name: String, + val const: String, + val initialValue: Any? // This can be modified based on your specific logic +) : Declaration() + +class OneDecl \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Module.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Module.kt new file mode 100644 index 0000000000..afa2931646 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Module.kt @@ -0,0 +1,35 @@ +package hu.bme.mit.theta.frontend.promela.model + +sealed class Module { +} + +data class Proctype( + val active: String?, + val name: String, + val declList: DeclList?, + val priority: String?, + val enabler: String?, + val sequence: List +) : Module() + +data class Init( + val priority: String?, + val sequence: List +) : Module() + +data class Never( + val sequence: List +) : Module() + +data class Trace( + val sequence: List +) : Module() + +data class Utype( + val name: String, + val declList: DeclList +) : Module() + +data class Mtype( + val names: List +) : Module() \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Spec.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Spec.kt new file mode 100644 index 0000000000..9df270142f --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Spec.kt @@ -0,0 +1,3 @@ +package hu.bme.mit.theta.frontend.promela.model + +data class Spec(val modules : List) \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Statement.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Statement.kt new file mode 100644 index 0000000000..54965203a7 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Statement.kt @@ -0,0 +1,44 @@ +package hu.bme.mit.theta.frontend.promela.model + +sealed class Statement + +data class IfStatement( + val options: PromelaOptions, + val sequence: List +) : Statement() + +data class DoStatement( + val options: PromelaOptions, + val sequence: List +) : Statement() + +data class ForStatement( + val range: Range, + val sequence: List +) : Statement() + +data class AtomicStatement( + val sequence: List +) : Statement() + +data class DStepStatement( + val sequence: List +) : Statement() + +data class SelectStatement( + val range: Range +) : Statement() + +data class Sequence( + val steps: List +) + +data class Range( + val name: String, + val start: String, + val end: String +) + +data class PromelaOptions( + val sequences: List +) diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Step.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Step.kt new file mode 100644 index 0000000000..1aa3c415ba --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Step.kt @@ -0,0 +1,11 @@ +package hu.bme.mit.theta.frontend.promela.model + +sealed class Step() + +data class StmntsStep(val stmnts : List) : Step() + +data class DeclListStep(val declLst : DeclList) : Step() + +data class xrStep(val varrefs : List) : Step() + +data class xsStep(val varrefs : List) : Step() \ No newline at end of file diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Types.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Types.kt new file mode 100644 index 0000000000..a79ef2df20 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Types.kt @@ -0,0 +1,4 @@ +package hu.bme.mit.theta.frontend.promela.model + +class PromelaType + diff --git a/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Variables.kt b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Variables.kt new file mode 100644 index 0000000000..110cfebbc3 --- /dev/null +++ b/subprojects/frontends/promela-frontend/src/main/java/hu/bme/mit/theta/frontend/promela/model/Variables.kt @@ -0,0 +1,10 @@ +package hu.bme.mit.theta.frontend.promela.model + +// TODO static var list? +data class Variable(val name : String) { + lateinit var type : String +} + +data class VariableInitialization(val variable: Variable, val initExpr : PromelaExpression) { + +} // TODO ch_init \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingleExprTraceRefiner.kt similarity index 100% rename from subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt rename to subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingleExprTraceRefiner.kt diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 679c249977..04a7c3e5ed 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -22,12 +22,16 @@ import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyProof -import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.* import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult +import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.ptr.PtrPrec import hu.bme.mit.theta.analysis.ptr.PtrState +import hu.bme.mit.theta.analysis.utils.AbstractTraceSummaryVisualizer import hu.bme.mit.theta.analysis.utils.ArgVisualizer import hu.bme.mit.theta.analysis.utils.TraceVisualizer import hu.bme.mit.theta.c2xcfa.CMetaData @@ -41,6 +45,7 @@ import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.xcfa.analysis.ErrorDetection import hu.bme.mit.theta.xcfa.analysis.XcfaAction +import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread @@ -48,9 +53,11 @@ import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiSingleThread import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts import hu.bme.mit.theta.xcfa.cli.checkers.getChecker +import hu.bme.mit.theta.xcfa.cli.checkers.getSafetyChecker import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.cli.utils.* import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer +import hu.bme.mit.theta.xcfa.collectVars import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.XcfaLabel @@ -59,6 +66,7 @@ import hu.bme.mit.theta.xcfa.passes.* import hu.bme.mit.theta.xcfa.toC import hu.bme.mit.theta.xcfa2chc.toSMT2CHC import java.io.File +import java.io.PrintWriter import java.util.concurrent.TimeUnit import kotlin.random.Random @@ -67,7 +75,7 @@ fun runConfig( logger: Logger, uniqueLogger: Logger, throwDontExit: Boolean, -): SafetyResult<*, *> { +): Result<*> { propagateInputOptions(config, logger, uniqueLogger) registerAllSolverManagers(config.backendConfig.solverHome, logger) @@ -76,11 +84,11 @@ fun runConfig( val (xcfa, mcm, parseContext) = frontend(config, logger, uniqueLogger) - preVerificationLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) + preAnalysisLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) val result = backend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) - postVerificationLogging(result, mcm, parseContext, config, logger, uniqueLogger) + postAnalysisLogging(result, mcm, parseContext, config, logger, uniqueLogger) return result } @@ -195,8 +203,8 @@ fun frontend( logger.write( Logger.Level.INFO, "Frontend finished: ${xcfa.name} (in ${ - stopwatch.elapsed(TimeUnit.MILLISECONDS) - } ms)\n", + stopwatch.elapsed(TimeUnit.MILLISECONDS) + } ms)\n", ) logger.write(RESULT, "ParsingResult Success\n") @@ -216,8 +224,10 @@ private fun backend( logger: Logger, uniqueLogger: Logger, throwDontExit: Boolean, -): SafetyResult<*, *> = - if (config.backendConfig.backend == Backend.NONE) { +): Result<*> = + if (config.backendConfig.backend == Backend.TRACEGEN) { + tracegenBackend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) + } else if (config.backendConfig.backend == Backend.NONE) { SafetyResult.unknown() } else { if ( @@ -238,12 +248,13 @@ private fun backend( "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n", ) - val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) + val checker = getSafetyChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { checker.check() } .let ResultMapper@{ result -> + result as SafetyResult<*, *> when { result.isSafe && xcfa.unsafeUnrollUsed -> { // cannot report safe if force unroll was used @@ -319,7 +330,34 @@ private fun backend( } } -private fun preVerificationLogging( +private fun tracegenBackend( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, +): Result<*> { + val stopwatch = Stopwatch.createStarted() + val checker = + getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) + as Checker, XcfaAction>, XcfaPrec<*>> + val result = + exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { + checker.check(XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet()))) + } + logger.write( + Logger.Level.INFO, + "Backend finished (in ${ + stopwatch.elapsed(TimeUnit.MILLISECONDS) + } ms)\n", + ) + + return result +} + +private fun preAnalysisLogging( xcfa: XCFA, mcm: MCM, parseContext: ParseContext, @@ -379,6 +417,41 @@ private fun preVerificationLogging( } } +private fun postAnalysisLogging( + result: Result<*>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, +) = + when (config.backendConfig.backend) { + Backend.TRACEGEN -> + postTraceGenerationLogging( + result + as + TraceGenerationResult< + AbstractTraceSummary, XcfaAction>, + XcfaState<*>, + XcfaAction, + >, + mcm, + parseContext, + config, + logger, + uniqueLogger, + ) + else -> + postVerificationLogging( + result as SafetyResult<*, *>, + mcm, + parseContext, + config, + logger, + uniqueLogger, + ) // safety analysis (or none) + } + private fun postVerificationLogging( safetyResult: SafetyResult<*, *>, mcm: MCM, @@ -512,3 +585,76 @@ private fun writeSequenceTrace( } sequenceFile.appendText("@enduml\n") } + +private fun postTraceGenerationLogging( + result: + TraceGenerationResult, XcfaAction>, XcfaState<*>, XcfaAction>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, +) { + val abstractSummary = result.summary + logger.write( + Logger.Level.MAINSTEP, + "Successfully generated a summary of ${abstractSummary.sourceTraces.size} abstract traces.\n", + ) + + val resultFolder = config.outputConfig.resultFolder + resultFolder.mkdirs() + + if (config.outputConfig.enableOutput) { + logger.write( + Logger.Level.MAINSTEP, + "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n", + ) + + val modelName = config.inputConfig.input?.name ?: "anonymous" + val graph = AbstractTraceSummaryVisualizer.visualize(abstractSummary) + val visFile = + resultFolder.absolutePath + File.separator + modelName + ".abstract-trace-summary.png" + GraphvizWriter.getInstance().writeFileAutoConvert(graph, visFile) + logger.write(Logger.Level.SUBSTEP, "Abstract trace summary was visualized in ${visFile}\n") + + var concreteTraces = 0 + for (abstractTrace in abstractSummary.sourceTraces) { + try { + // TODO no concrete summary implemented for XCFA yet, only traces + val concrTrace: Trace, XcfaAction> = + XcfaTraceConcretizer.concretize( + abstractTrace.toTrace() as Trace>, XcfaAction>, + getSolver( + config.outputConfig.witnessConfig.concretizerSolver, + config.outputConfig.witnessConfig.validateConcretizerSolver, + ), + parseContext, + ) + + val concreteTraceFile = + resultFolder.absolutePath + File.separator + modelName + "_${concreteTraces}.cex" + + PrintWriter(File(concreteTraceFile)).use { printWriter -> + printWriter.write(concrTrace.toString()) + } + + val concreteDotFile = + File(resultFolder.absolutePath + File.separator + modelName + "_${concreteTraces}.dot") + val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) + concreteDotFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) + + logger.write( + Logger.Level.MAINSTEP, + "Concrete trace exported to ${concreteTraceFile} and ${concreteDotFile}", + ) + concreteTraces++ + } catch (e: IllegalArgumentException) { + logger.write(Logger.Level.SUBSTEP, e.toString()) + logger.write(Logger.Level.SUBSTEP, "Continuing concretization with next trace...") + } + } + logger.write(Logger.Level.RESULT, "Successfully generated ${concreteTraces} concrete traces.\n") + } + + // TODO print coverage (full or not)? +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt index c6bc1153fe..5087d378cb 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.Checker import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG @@ -30,7 +31,7 @@ import hu.bme.mit.theta.xcfa.cli.params.Backend import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.model.XCFA -fun getChecker( +fun getSafetyChecker( xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, @@ -58,5 +59,62 @@ fun getChecker( SafetyResult.unknown() } Backend.CHC -> getHornChecker(xcfa, mcm, config, logger) + Backend.TRACEGEN -> + throw RuntimeException( + "Trace generation is NOT safety analysis, can not return safety checker for trace generation" + ) + } + } + +fun getChecker( + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + parseContext: ParseContext, + logger: Logger, + uniqueLogger: Logger, +): Checker<*, XcfaPrec<*>> = + if (config.backendConfig.inProcess) { + InProcessChecker(xcfa, config, parseContext, logger) + } else { + when (config.backendConfig.backend) { + Backend.TRACEGEN -> getTracegenChecker(xcfa, mcm, config, logger) + Backend.CEGAR -> + throw RuntimeException( + "Use getSafetyChecker method for safety analysis instead of getChecker" + ) + Backend.BOUNDED -> + throw RuntimeException( + "Use getSafetyChecker method for safety analysis instead of getChecker" + ) + Backend.OC -> + throw RuntimeException( + "Use getSafetyChecker method for safety analysis instead of getChecker" + ) + Backend.LAZY -> + throw RuntimeException( + "Use getSafetyChecker method for portfolio safety analysis instead of getChecker" + ) + Backend.PORTFOLIO -> + throw RuntimeException( + "Use getSafetyChecker method for portfolio safety analysis instead of getChecker" + ) + Backend.NONE -> + SafetyChecker< + ARG>, XcfaAction>, + Trace>, XcfaAction>, + XcfaPrec<*>, + > { _ -> + SafetyResult.unknown() + } + Backend.CHC -> + throw RuntimeException( + "Use getSafetyChecker method for safety analysis instead of getChecker" + ) + + Backend.MDD -> + throw RuntimeException( + "Use getSafetyChecker method for portfolio safety analysis instead of getChecker" + ) } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt new file mode 100644 index 0000000000..ff661f78a9 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt @@ -0,0 +1,89 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xcfa.cli.checkers + +import hu.bme.mit.theta.analysis.PartialOrd +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.Checker +import hu.bme.mit.theta.analysis.algorithm.Result +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.refinement.* +import hu.bme.mit.theta.analysis.ptr.PtrState +import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.xcfa.analysis.* +import hu.bme.mit.theta.xcfa.cli.params.* +import hu.bme.mit.theta.xcfa.cli.utils.getSolver +import hu.bme.mit.theta.xcfa.model.XCFA + +fun getTracegenChecker( + xcfa: XCFA, + mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger, +): Checker, XcfaAction>, XcfaPrec<*>> { + val tracegenConfig = config.backendConfig.specConfig as TracegenConfig + val ignoredVarRegistry = mutableMapOf, MutableSet>() + + val lts = ConeOfInfluenceMode.NO_COI.getLts(xcfa, ignoredVarRegistry, POR.NOPOR) + + val abstractionSolverFactory: SolverFactory = + getSolver( + tracegenConfig.abstractorConfig.abstractionSolver, + tracegenConfig.abstractorConfig.validateAbstractionSolver, + ) + + val waitlist = + PriorityWaitlist.create>, XcfaAction>>( + tracegenConfig.abstractorConfig.search.getComp(xcfa) + ) + + val abstractionSolverInstance = abstractionSolverFactory.createSolver() + val globalStatePartialOrd: PartialOrd> = + tracegenConfig.abstractorConfig.domain.partialOrd(abstractionSolverInstance) + as PartialOrd> + val corePartialOrd: PartialOrd>> = + if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) + else getStackPartialOrder(globalStatePartialOrd) + val abstractor: BasicArgAbstractor = + tracegenConfig.abstractorConfig.domain.abstractor( + xcfa, + abstractionSolverInstance, + tracegenConfig.abstractorConfig.maxEnum, + waitlist, + StopCriterions.fullExploration(), + logger, + lts, + config.inputConfig.property, + corePartialOrd, + tracegenConfig.abstractorConfig.havocMemory, + ) as BasicArgAbstractor + + val tracegenChecker = TraceGenerationChecker.create(logger, abstractor, false) + + return Checker, XcfaAction>, XcfaPrec<*>> { prec -> + tracegenChecker.check(prec) as Result, XcfaAction>> + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt index c2d46bd504..5c8c4e9039 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt @@ -69,6 +69,7 @@ enum class Backend { OC, LAZY, PORTFOLIO, + TRACEGEN, MDD, NONE, } @@ -377,6 +378,11 @@ enum class Search { abstract fun getComp(cfa: XCFA): ArgNodeComparator } +enum class TracegenAbstraction { + NONE + // TODO add EXPL +} + enum class InitPrec( val explPrec: (xcfa: XCFA) -> XcfaPrec>, val predPrec: (xcfa: XCFA) -> XcfaPrec>, diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 1675afa4a6..57a6371644 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -196,6 +196,7 @@ data class BackendConfig( Backend.OC -> OcConfig() as T Backend.LAZY -> null Backend.PORTFOLIO -> PortfolioConfig() as T + Backend.TRACEGEN -> TracegenConfig() as T Backend.MDD -> MddConfig() as T Backend.NONE -> null } @@ -228,6 +229,12 @@ data class CegarConfig( listOf(abstractorConfig, refinerConfig).map { it.update() }.any { it } } +data class TracegenConfig( + @Parameter(names = ["--abstraction"], description = "Abstraction to be used for trace generation") + var abstraction: TracegenAbstraction = TracegenAbstraction.NONE, + val abstractorConfig: CegarAbstractorConfig = CegarAbstractorConfig(), +) : SpecBackendConfig + data class CegarAbstractorConfig( @Parameter(names = ["--abstraction-solver"], description = "Abstraction solver name") var abstractionSolver: String = "Z3", diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt index 2e54ec3fe8..1856d0d615 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -37,7 +38,9 @@ fun complexPortfolio23( uniqueLogger: Logger, ): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> + runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> + } var baseConfig = XcfaConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt index 7547273b57..eb108915ad 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -39,7 +40,9 @@ fun complexPortfolio24( uniqueLogger: Logger, ): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> + runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> + } var baseConfig = XcfaConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt index 749a43d6da..18c46807b0 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xcfa.cli.portfolio +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig @@ -36,7 +37,9 @@ fun hornPortfolio25( uniqueLogger: Logger, ): STM { - val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) } + val checker = { config: XcfaConfig<*, *> -> + runConfig(config, logger, uniqueLogger, true) as SafetyResult<*, *> + } var baseConfig = XcfaConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt index b8b33c9c21..8e9e4af373 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.xcfa.cli.portfolio -import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.Result import hu.bme.mit.theta.xcfa.cli.params.Backend import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig @@ -62,7 +62,7 @@ fun XcfaConfig<*, *>.visualize(): String = class ConfigNode( name: String, private val config: XcfaConfig<*, *>, - private val check: (config: XcfaConfig<*, *>) -> SafetyResult<*, *>, + private val check: (config: XcfaConfig<*, *>) -> Result<*>, ) : Node(name) { override fun execute(): Pair { diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt index 89c11bb249..fd88c5398c 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt @@ -20,7 +20,7 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager -import hu.bme.mit.theta.xcfa.cli.checkers.getChecker +import hu.bme.mit.theta.xcfa.cli.checkers.getSafetyChecker import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.model.ParamDirection.IN import hu.bme.mit.theta.xcfa.model.ParamDirection.OUT @@ -88,7 +88,7 @@ class XcfaDslTest { run { val xcfa = getSyncXcfa() val checker = - getChecker( + getSafetyChecker( xcfa, emptySet(), config, @@ -102,7 +102,7 @@ class XcfaDslTest { run { val xcfa = getAsyncXcfa() val checker = - getChecker( + getSafetyChecker( xcfa, emptySet(), config, diff --git a/subprojects/xsts/xsts-analysis/build.gradle.kts b/subprojects/xsts/xsts-analysis/build.gradle.kts index 2f3d02e007..bcbf3c1f3e 100644 --- a/subprojects/xsts/xsts-analysis/build.gradle.kts +++ b/subprojects/xsts/xsts-analysis/build.gradle.kts @@ -1,3 +1,5 @@ +import org.jetbrains.kotlin.gradle.tasks.KotlinCompile + /* * Copyright 2024 Budapest University of Technology and Economics * @@ -26,6 +28,18 @@ dependencies { implementation(project(":theta-xsts")) testImplementation(project(":theta-solver-z3")) testImplementation(project(":theta-solver-z3-legacy")) + implementation(kotlin("stdlib-jdk8")) testImplementation(project(":theta-solver-smtlib")) testImplementation(project(":theta-solver-javasmt")) } +repositories { + mavenCentral() +} +val compileKotlin: KotlinCompile by tasks +compileKotlin.kotlinOptions { + jvmTarget = "17" +} +val compileTestKotlin: KotlinCompile by tasks +compileTestKotlin.kotlinOptions { + jvmTarget = "17" +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsTraceGenerationConcretizerUtil.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsTraceGenerationConcretizerUtil.kt new file mode 100644 index 0000000000..655eb1dae5 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsTraceGenerationConcretizerUtil.kt @@ -0,0 +1,303 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.concretizer + +import com.google.common.base.Preconditions.checkState +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.* +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.refinement.ExprSummaryFwBinItpChecker +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceFwBinItpChecker +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.Tuple2 +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState +import java.util.* +import java.util.stream.Collectors + +object XstsTraceGenerationConcretizerUtil { + fun concretizeSummary( + summary: AbstractTraceSummary, XstsAction>, + solverFactory: SolverFactory, + xsts: XSTS, + ): Map, out XstsAction>, XstsState> { + val varFilter = VarFilter.of(xsts) + val checker: ExprSummaryFwBinItpChecker = + ExprSummaryFwBinItpChecker.create(xsts.initFormula, solverFactory.createItpSolver()) + val status = checker.check(summary) + + checkState(status.feasible, "Summary could not be concretized") + + val concreteSummary = (status as FeasibleExprSummaryStatus, XstsAction>).summary + + val xstsStateMap: + MutableMap, out XstsAction>, XstsState> = + mutableMapOf() + for ((abstractNode, valuation) in concreteSummary.valuationMap) { + xstsStateMap[abstractNode] = + XstsState.of( + ExplState.of(varFilter.filter(valuation)), + abstractNode.getStates().iterator().next().lastActionWasEnv(), + abstractNode.getStates().iterator().next().isInitialized(), + ) + } + + return xstsStateMap + } + + fun concretizeTraceList( + abstractTraces: List, XstsAction>>, + solverFactory: SolverFactory, + xsts: XSTS, + ): Tuple2, String> { + val infeasibles: MutableList>, ItpRefutation>> = ArrayList() + var foundInfeasible = false + + val varFilter = VarFilter.of(xsts) + val checker: ExprTraceChecker = + ExprTraceFwBinItpChecker.create( + xsts.initFormula, + BoolExprs.True(), + solverFactory.createItpSolver(), + ) + val tracePairs = HashMap, XstsAction>, XstsStateSequence>() + + for (abstractTrace in abstractTraces) { + var resultingTrace = abstractTrace + // another xsts specific thing - if the env is more complicated, trace might end in env + // sending something, which might seem weird + val lastState = abstractTrace.states[abstractTrace.states.size - 1] + if (lastState.toString().contains("last_env")) { + resultingTrace = shortenTrace(abstractTrace, abstractTrace.states.size - 2) + } + + var status = checker.check(abstractTrace) + if (status.isInfeasible) { + foundInfeasible = true + addToReport(infeasibles, status.asInfeasible().refutation, abstractTrace) + val pruneIndex = status.asInfeasible().refutation.pruneIndex + if (pruneIndex > 0) { + resultingTrace = shortenTrace(abstractTrace, pruneIndex) + status = checker.check(abstractTrace) + } + } + + if (status.isFeasible) { + val valuations: Trace = status.asFeasible().valuations + assert(valuations.states.size == abstractTrace.states.size) + val xstsStates: MutableList> = ArrayList() + for (i in abstractTrace.states.indices) { + xstsStates.add( + XstsState.of( + ExplState.of(varFilter.filter(valuations.getState(i))), + abstractTrace.getState(i).lastActionWasEnv(), + abstractTrace.getState(i).isInitialized, + ) + ) + } + + val concretizedTrace = XstsStateSequence.of(xstsStates, xsts) + + tracePairs[abstractTrace] = concretizedTrace + } + } + + // if trace was shortened, it might match with another one, in this case, do not add it again + val filteredTracePairs = HashMap, XstsAction>, XstsStateSequence>() + tracePairs.keys + .stream() + .filter { trace: Trace, XstsAction> -> + for (otherTrace in tracePairs.keys) { + if (trace.states.size < otherTrace.states.size) { + val traceString = trace.toString() + val traceStringWithoutClosingParentheses = + traceString.substring(0, traceString.length - 1) + if (otherTrace.toString().contains(traceStringWithoutClosingParentheses)) { + return@filter false + } + } + } + true + } + .forEach { key: Trace, XstsAction> -> + filteredTracePairs[key] = tracePairs[key]!! + } + + val report = createReport(filteredTracePairs.keys, infeasibles, foundInfeasible) + return Tuple2.of(HashSet(filteredTracePairs.values), report) + } + + private fun addToReport( + infeasibles: MutableList>, ItpRefutation>>, + refutation: ItpRefutation, + abstractTrace: Trace, XstsAction>, + ) { + val prunedStates = ArrayList>() + for (i in refutation.pruneIndex + 1 until abstractTrace.states.size) { + if ( + abstractTrace.getState(i).toString().contains("last_internal") + ) { // xsts specific condition + prunedStates.add(abstractTrace.getState(i)) + } + } + infeasibles.add(Tuple2.of(prunedStates, refutation)) + } + + private fun createReport( + traces: Collection, XstsAction>>, + infeasibles: MutableList>, ItpRefutation>>, + foundInfeasible: Boolean, + ): String { + var statesVisited = + traces + .stream() + .map { obj: Trace, XstsAction> -> obj.states } + .flatMap { obj: List> -> obj.stream() } + .collect(Collectors.toSet()) + // xsts specific part + statesVisited = + statesVisited + .stream() + .filter { state: XstsState -> state.toString().contains("last_internal") } + .collect(Collectors.toSet()) + + val missingStates: MutableList> = ArrayList() + val stateRefutations: MutableList = ArrayList() + for (infeasible in infeasibles) { + var missingState = false + for (xstsState in infeasible.get1()) { + if (!stateContains(statesVisited, xstsState)) { + missingState = true + missingStates.add(xstsState) + } + } + if (missingState) { + stateRefutations.add(infeasible.get2()) + } + } + + val problematicVariables = + stateRefutations + .stream() + .map { refutation: ItpRefutation -> ExprUtils.getVars(refutation[refutation.pruneIndex]) } + .flatMap { obj: Set> -> obj.stream() } + .collect(Collectors.toSet()) + + val reportBuilder = StringBuilder() + + // allapot fedest pontosan nezzuk, transition fedest csak annyira, hogy serulhetett-e + if (foundInfeasible) { + reportBuilder.append( + "There were infeasible traces found; transition coverage might be incomplete\n" + ) + } else { + reportBuilder.append("Trace coverage is complete\n") + } + + if (stateRefutations.isEmpty()) { + reportBuilder.append("State coverage (including variables in variable list) is complete\n") + } else { + reportBuilder.append( + "State coverage (including variables in variable list) is incomplete.\n\n" + ) + + reportBuilder.append( + "The following abstract states are not covered (they might or might not be possible):\n" + ) + + for (missingState in missingStates) { + reportBuilder.append(missingState.toString()) + reportBuilder.append("\n------------------------------\n") + } + + reportBuilder.append("\n") + // TODO ez NAGYON heurisztika, pl ha prioritas miatt maradt ki valami, akkor hulyesegeket is + // mondhat + reportBuilder.append( + "Maybe adding some of the following variables to the variable list can help:\n" + ) + reportBuilder.append( + problematicVariables + .stream() + .map { obj: VarDecl<*> -> obj.name } + .collect(Collectors.toSet()) + ) + reportBuilder.append("\n") + } + + return reportBuilder.toString() + } + + private fun stateContains( + statesVisited: Set>, + xstsState: XstsState, + ): Boolean { + val sb1 = StringBuilder() + val stateLineList = + Arrays.asList( + *xstsState.toString().split("\n".toRegex()).dropLastWhile { it.isEmpty() }.toTypedArray() + ) + for (line in stateLineList) { + if (!line.contains("__id_")) { + sb1.append(line) + sb1.append("\n") + } + } + val xstsStateNoTransitions = sb1.toString() + + val statesVisitedNoTransitions = + statesVisited + .stream() + .map { state: XstsState -> + val sb = StringBuilder() + val lineList = + Arrays.asList( + *state.toString().split("\n".toRegex()).dropLastWhile { it.isEmpty() }.toTypedArray() + ) + for (line in lineList) { + if (!line.contains("__id_")) { + sb.append(line) + sb.append("\n") + } + } + sb.toString() + } + .toList() + + return statesVisitedNoTransitions.contains(xstsStateNoTransitions) + } + + private fun shortenTrace( + abstractTrace: Trace, XstsAction>, + pruneIndex: Int, + ): Trace, XstsAction> { + var abstractTrace = abstractTrace + var newStates: List> = ArrayList(abstractTrace.states) + newStates = newStates.subList(0, pruneIndex + 1) + var newActions: List = ArrayList(abstractTrace.actions) + newActions = newActions.subList(0, pruneIndex) + abstractTrace = Trace.of(newStates, newActions) // remove last state + return abstractTrace + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt new file mode 100644 index 0000000000..7ff3f0590d --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt @@ -0,0 +1,41 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.initprec + +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.pred.PredPrec +import hu.bme.mit.theta.analysis.prod2.Prod2Prec +import hu.bme.mit.theta.core.utils.StmtAtomCollector +import hu.bme.mit.theta.xsts.XSTS + +class XstsTracegenPredInitPrec : XstsInitPrec { + override fun createExpl(xsts: XSTS?): ExplPrec { + throw RuntimeException("Explicit precision is not supported with guard init precision") + } + + override fun createPred(xsts: XSTS): PredPrec { + val tran = xsts.tran + val ctrlVars = xsts.ctrlVars // TODO add to pred + + val assumes = StmtAtomCollector.collectAtoms(tran) + // val assumes = StmtAssumeCollector.collectAssumes(tran) + return PredPrec.of(assumes) + } + + override fun createProd2ExplPred(xsts: XSTS): Prod2Prec { + throw RuntimeException("Prod2ExplPred precision is not supported with variable list precision") + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsVarListInitPrec.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsVarListInitPrec.java new file mode 100644 index 0000000000..3ba8355739 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsVarListInitPrec.java @@ -0,0 +1,62 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.initprec; + +import hu.bme.mit.theta.analysis.expl.ExplPrec; +import hu.bme.mit.theta.analysis.pred.PredPrec; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.xsts.XSTS; +import java.util.Set; + +public class XstsVarListInitPrec implements XstsInitPrec { + Set> vars; + boolean transitionCoverage = true; + + public XstsVarListInitPrec(Set> vars) { + this.vars = vars; + } + + public XstsVarListInitPrec setTransitionCoverage(boolean transitionCoverage) { + this.transitionCoverage = transitionCoverage; + return this; + } + + @Override + public ExplPrec createExpl(XSTS xsts) { + vars.addAll(xsts.getCtrlVars()); + if (transitionCoverage) { + for (VarDecl var : xsts.getVars()) { + if (var.getName().startsWith("__id_")) { + vars.add(var); + } + } + } + return ExplPrec.of(vars); + } + + @Override + public PredPrec createPred(XSTS xsts) { + throw new RuntimeException( + "Predicate precision is not supported with variable list precision"); + } + + @Override + public Prod2Prec createProd2ExplPred(XSTS xsts) { + throw new RuntimeException( + "Prod2ExplPred precision is not supported with variable list precision"); + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/TracegenerationAbstraction.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/TracegenerationAbstraction.kt new file mode 100644 index 0000000000..19bb8b5058 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/TracegenerationAbstraction.kt @@ -0,0 +1,22 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.tracegeneration + +enum class TracegenerationAbstraction { + NONE, + VARLIST, // explicit + // AUTOPRED // Cartesian predicates based on guards +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt new file mode 100644 index 0000000000..3d763d349a --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt @@ -0,0 +1,191 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.tracegeneration + +import com.google.common.base.Preconditions +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker.Companion.create +import hu.bme.mit.theta.analysis.expl.* +import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.* +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec +import hu.bme.mit.theta.xsts.analysis.initprec.XstsVarListInitPrec +import java.io.File +import java.io.IOException +import java.util.* +import java.util.function.Predicate + +class XstsTracegenBuilder( + private val solverFactory: SolverFactory, + private val transitionCoverage: Boolean, +) { + private var logger: Logger = NullLogger.getInstance() + private var varFile: File? = null + private var abstraction = TracegenerationAbstraction.NONE + private var getFullTraces = false + + fun logger(logger: Logger): XstsTracegenBuilder { + this.logger = logger + return this + } + + fun setVarFile(filename: String?): XstsTracegenBuilder { + if (filename != null) { + this.varFile = File(filename) + } + return this + } + + fun setAbstraction(abstraction: TracegenerationAbstraction): XstsTracegenBuilder { + this.abstraction = abstraction + return this + } + + private fun buildExpl(xsts: XSTS): XstsTracegenConfig { + val solver2 = + solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way + + val analysis = XstsAnalysis.create(ExplAnalysis.create(solver2, BoolExprs.True())) + val lts = XstsLts.create(xsts, XstsStmtOptimizer.create(ExplStmtOptimizer.getInstance())) + + val negProp: Expr = BoolExprs.Not(xsts.prop) + val target: Predicate?> = + XstsStatePredicate(ExplStatePredicate(negProp, solver2)) + val argBuilder = ArgBuilder.create(lts, analysis, target, true) + + if (abstraction == TracegenerationAbstraction.VARLIST) { + val abstractor: BasicArgAbstractor, XstsAction, ExplPrec> = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) + .stopCriterion(StopCriterions.fullExploration()) + .logger(logger) + .build() + + val tracegenChecker = create(logger, abstractor, getFullTraces) + + assert(varFile != null) + try { + Scanner(varFile).use { scanner -> + val varNamesToAdd: MutableSet = HashSet() + val varsToAdd: MutableSet> = HashSet() + while (scanner.hasNext()) { + varNamesToAdd.add(scanner.nextLine().trim { it <= ' ' }) + } + val vars = xsts.vars + for (`var` in vars) { + if (varNamesToAdd.contains(`var`.name)) { + varsToAdd.add(`var`) + } + } + Preconditions.checkState(varNamesToAdd.size == varsToAdd.size) + return XstsTracegenConfig.create( + tracegenChecker, + XstsVarListInitPrec(varsToAdd) + .setTransitionCoverage(transitionCoverage) + .createExpl(xsts), + ) + } + } catch (e: IOException) { + throw RuntimeException(e) + } + } else { + assert(abstraction == TracegenerationAbstraction.NONE) + val abstractor: BasicArgAbstractor, XstsAction, ExplPrec> = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) + .stopCriterion(StopCriterions.fullExploration()) + .logger(logger) + .build() + + val tracegenChecker = create(logger, abstractor, getFullTraces) + return XstsTracegenConfig.create(tracegenChecker, XstsAllVarsInitPrec().createExpl(xsts)) + } + } + + /* + private fun buildPred(xsts: XSTS) : XstsTracegenConfig { + assert(abstraction==TracegenerationAbstraction.AUTOPRED) + val lts = XstsLts.create(xsts, XstsStmtOptimizer.create(PredStmtOptimizer.getInstance())) + val negProp: Expr = BoolExprs.Not(xsts.prop) + val solver2 = + solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way + val target: Predicate?> = + XstsStatePredicate( + ExprStatePredicate(negProp, solver2) + ) + + val analysis = XstsAnalysis.create( + PredAnalysis.create( + solver2, PredAbstractors.booleanAbstractor(solver2), + xsts.initFormula + ) + ) + val argBuilder = ArgBuilder.create(lts, analysis, target, true) + + val abstractor: Abstractor?, XstsAction?, PredPrec?> = + BasicArgAbstractor.builder(argBuilder) + .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) + .stopCriterion(StopCriterions.fullExploration()) + .logger(logger).build() + val tracegenChecker = create(logger, abstractor) + return XstsTracegenConfig.create( + tracegenChecker, + XstsTracegenPredInitPrec().createPred(xsts) + ) + } + */ + + fun build(xsts: XSTS): XstsTracegenConfig { + val solver2 = + solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way + + val analysis = XstsAnalysis.create(ExplAnalysis.create(solver2, BoolExprs.True())) + val lts = XstsLts.create(xsts, XstsStmtOptimizer.create(ExplStmtOptimizer.getInstance())) + + val negProp: Expr = BoolExprs.Not(xsts.prop) + val target: Predicate?> = + XstsStatePredicate(ExplStatePredicate(negProp, solver2)) + val argBuilder = ArgBuilder.create(lts, analysis, target, true) + + if (abstraction == TracegenerationAbstraction.VARLIST) { + return buildExpl(xsts) + } /*else if (abstraction==TracegenerationAbstraction.AUTOPRED) { + return buildPred(xsts) + } */ else { + assert(abstraction == TracegenerationAbstraction.NONE) + return buildExpl(xsts) + } + } + + fun setGetFullTraces(getFullTraces: Boolean): XstsTracegenBuilder { + this.getFullTraces = getFullTraces + return this + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt new file mode 100644 index 0000000000..c2cc01ddeb --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt @@ -0,0 +1,39 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.analysis.tracegeneration + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult + +class XstsTracegenConfig +private constructor(private val checker: TraceGenerationChecker, private val prec: P) { + fun check(): TraceGenerationResult, S, A> { + return checker.check(prec) + } + + companion object { + fun create( + checker: TraceGenerationChecker, + initPrec: P, + ): XstsTracegenConfig { + return XstsTracegenConfig(checker, initPrec) + } + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt index 90c2af692e..87eed34b40 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.core.CliktCommand @@ -25,8 +24,6 @@ import com.github.ajalt.clikt.parameters.options.versionOption import com.github.ajalt.clikt.parameters.types.file import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.arg.ARG -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics import hu.bme.mit.theta.common.logging.ConsoleLogger import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.NullLogger @@ -44,62 +41,64 @@ import java.io.File import java.io.PrintWriter abstract class XstsCliBaseCommand(name: String? = null, help: String = "") : - CliktCommand(name = name, help = help, printHelpOnEmptyArgs = true) { + CliktCommand(name = name, help = help, printHelpOnEmptyArgs = true) { - init { - versionOption(javaClass.`package`.implementationVersion ?: "unknown") - } + init { + versionOption(javaClass.`package`.implementationVersion ?: "unknown") + } - protected val inputOptions by InputOptions() - protected val outputOptions by OutputOptions() - protected open val defaultSolver: String = "Z3" - protected val solver: String by option(help = "The solver to use for the check").defaultLazy { defaultSolver } - private val smtHome: File by option().file().default(SmtLibSolverManager.HOME.toFile()) - protected val logger: Logger by lazy { - if (outputOptions.benchmarkMode) NullLogger.getInstance() else ConsoleLogger(outputOptions.logLevel) - } - protected val writer = BasicTableWriter(System.out, ",", "\"", "\"") + protected val inputOptions by InputOptions() + protected val outputOptions by OutputOptions() + protected open val defaultSolver: String = "Z3" + protected val solver: String by + option(help = "The solver to use for the check").defaultLazy { defaultSolver } + private val smtHome: File by option().file().default(SmtLibSolverManager.HOME.toFile()) + protected val logger: Logger by lazy { + if (outputOptions.benchmarkMode) NullLogger.getInstance() + else ConsoleLogger(outputOptions.logLevel) + } + protected val writer = + BasicTableWriter(System.out, ",", "\"", "\"") // TODO shouldn't this be done through logger?? - fun printError(exception: Exception) { - val message = exception.message ?: "" - val exceptionName = exception.javaClass.simpleName - if (outputOptions.benchmarkMode) { - writer.cell("[EX] $exceptionName: $message") - writer.newRow() - return - } - logger.write(Logger.Level.RESULT, "%s occurred, message: %s%n", exceptionName, message) - if (outputOptions.stacktrace) { - logger.write(Logger.Level.RESULT, "Trace:%n%s%n", exception.stackTraceToString()) - } else { - logger.write(Logger.Level.RESULT, "Use --stacktrace for stack trace%n") - } + fun printError(exception: Exception) { + val message = exception.message ?: "" + val exceptionName = exception.javaClass.simpleName + if (outputOptions.benchmarkMode) { + writer.cell("[EX] $exceptionName: $message") + writer.newRow() + return } - - fun printCommonResult(status: SafetyResult<*, *>, xsts: XSTS, totalTimeMs: Long) { - listOf( - status.isSafe, - totalTimeMs, - if (status.isUnsafe) "${status.asUnsafe().cex?.length() ?: "N/A"}" else "", - xsts.vars.size, - ).forEach(writer::cell) + logger.write(Logger.Level.RESULT, "%s occurred, message: %s%n", exceptionName, message) + if (outputOptions.stacktrace) { + logger.write(Logger.Level.RESULT, "Trace:%n%s%n", exception.stackTraceToString()) + } else { + logger.write(Logger.Level.RESULT, "Use --stacktrace for stack trace%n") } + } - fun registerSolverManagers() { - SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create()) - SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create()) - SolverManager.registerSolverManager(SmtLibSolverManager.create(smtHome.toPath(), logger)) - SolverManager.registerSolverManager(JavaSMTSolverManager.create()) - } + fun printCommonResult(status: SafetyResult<*, *>, xsts: XSTS, totalTimeMs: Long) { + listOf( + status.isSafe, + totalTimeMs, + if (status.isUnsafe) "${status.asUnsafe().cex?.length() ?: "N/A"}" else "", + xsts.vars.size, + ) + .forEach(writer::cell) + } - protected fun writeCex(status: SafetyResult<*, *>, xsts: XSTS) { - if (outputOptions.cexfile == null || status.isSafe) return - val trace = status.asUnsafe().cex as Trace, XstsAction> - val concreteTrace = - XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts) - val file: File = outputOptions.cexfile!! - PrintWriter(file).use { printWriter -> - printWriter.write(concreteTrace.toString()) - } - } + fun registerSolverManagers() { + SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create()) + SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create()) + SolverManager.registerSolverManager(SmtLibSolverManager.create(smtHome.toPath(), logger)) + SolverManager.registerSolverManager(JavaSMTSolverManager.create()) + } + + protected fun writeCex(status: SafetyResult<*, *>, xsts: XSTS) { + if (outputOptions.cexfile == null || status.isSafe) return + val trace = status.asUnsafe().cex as Trace, XstsAction> + val concreteTrace = + XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts) + val file: File = outputOptions.cexfile!! + PrintWriter(file).use { printWriter -> printWriter.write(concreteTrace.toString()) } + } } diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt index 73b01a8568..9804ea0725 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.core.CliktCommand @@ -23,23 +22,32 @@ import com.github.ajalt.clikt.parameters.options.option class XstsCliMainCommand : CliktCommand() { - val algorithm by option(eager = true).deprecated( - "--algorithm switch is now deprecated, use the respective subcommands", error = true - ) - val metrics by option(eager = true).deprecated( - "--metrics switch is now deprecated, use the `metrics` subcommand", error = true - ) - val header by option(eager = true).deprecated( - "--header switch is now deprecated, use the `header` subcommand", error = true - ) - - override fun run() = Unit + val algorithm by + option(eager = true) + .deprecated( + "--algorithm switch is now deprecated, use the respective subcommands", + error = true, + ) + val metrics by + option(eager = true) + .deprecated("--metrics switch is now deprecated, use the `metrics` subcommand", error = true) + val header by + option(eager = true) + .deprecated("--header switch is now deprecated, use the `header` subcommand", error = true) + override fun run() = Unit } fun main(args: Array) = - XstsCliMainCommand().subcommands( - XstsCliCegar(), XstsCliBounded(), XstsCliMdd(), XstsCliPetrinetMdd(), XstsCliChc(), XstsCliHeader(), - XstsCliMetrics() + XstsCliMainCommand() + .subcommands( + XstsCliCegar(), + XstsCliBounded(), + XstsCliMdd(), + XstsCliPetrinetMdd(), + XstsCliChc(), + XstsCliHeader(), + XstsCliMetrics(), + XstsCliTracegen(), ) - .main(args) \ No newline at end of file + .main(args) diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt new file mode 100644 index 0000000000..439907c997 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt @@ -0,0 +1,220 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.cli + +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.flag +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.file +import com.google.common.base.Stopwatch +import com.google.common.io.Files +import com.google.common.io.MoreFiles +import com.google.common.io.RecursiveDeleteOption +import hu.bme.mit.theta.analysis.* +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.* +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.utils.AbstractTraceSummaryVisualizer +import hu.bme.mit.theta.common.Utils +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.z3.Z3SolverFactory +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState +import hu.bme.mit.theta.xsts.analysis.concretizer.XstsStateSequence +import hu.bme.mit.theta.xsts.analysis.concretizer.XstsTraceGenerationConcretizerUtil +import hu.bme.mit.theta.xsts.analysis.tracegeneration.XstsTracegenBuilder +import hu.bme.mit.theta.xsts.analysis.tracegeneration.XstsTracegenConfig +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import java.io.* +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +class XstsCliTracegen : + XstsCliBaseCommand( + name = "TRACEGEN", + help = "Trace generation (instead of verification). Property and input options will be ignored", + ) { + val traceDir: File? by + option( + help = + "Directory the traces should be written into. If not specified, output is written into model-directory/traces." + ) + .file(mustExist = true, canBeFile = false) // use the non-null value in traceDirPath! + val summary: Boolean by + option(help = "If this flag is present, a concretized summary is generated.") + .flag(default = false) + val traces: Boolean by + option(help = "If this flag is present, concretized traces are generated.") + .flag(default = false) + + private fun toCexs( + summaryStateMap: + Map, out XstsAction>, XstsState> + ): String { + val sb = Utils.lispStringBuilder(javaClass.simpleName).body() + + for ((node, state) in summaryStateMap) { + sb.add( + Utils.lispStringBuilder( + "_${node.id}: ${XstsState::class.java.simpleName}" + ) // TODO number env separately + .add(if (state.isInitialized) "post_init" else "pre_init") + .add(if (state.lastActionWasEnv()) "last_env" else "last_internal") + .body() + .add(state.state.toString()) + ) + } + + for (node in summaryStateMap.keys) { + for (outEdge in node.outEdges) { + sb.add("${node.id} -> ${outEdge.target.id}") + } + } + + return sb.toString() + } + + private fun printResult( + concretizationResult: + Map, out XstsAction>, XstsState>, + abstractSummary: AbstractTraceSummary, + totalTimeMs: Long, + traceDirPath: File, + xsts: XSTS, + ) { + logger.write( + Logger.Level.RESULT, + "Successfully generated a summary of ${abstractSummary.sourceTraces.size} traces in ${totalTimeMs}ms\n", + ) + + // TODO print coverage (full or not)? + val graph = AbstractTraceSummaryVisualizer.visualize(abstractSummary) + val visFile = + traceDirPath.absolutePath + + File.separator + + inputOptions.model.name + + ".abstract-trace-summary.png" + GraphvizWriter.getInstance().writeFileAutoConvert(graph, visFile) + logger.write(Logger.Level.SUBSTEP, "Abstract trace summary was visualized in ${visFile}\n") + + // trace concretization + if (traces) { + var traceCount = 0 + + val concretizationResultTuple = + XstsTraceGenerationConcretizerUtil.concretizeTraceList( + abstractSummary.sourceTraces.map { + it.toTrace() as Trace, XstsAction> + }, + Z3LegacySolverFactory.getInstance(), + xsts, + ) + val concretizedTraces: Set = concretizationResultTuple.get1() + val report: String = concretizationResultTuple.get2() + + for (trace in concretizedTraces) { + val traceFile = + File( + traceDirPath.absolutePath + + File.separator + + Files.getNameWithoutExtension(inputOptions.model.name) + + "-" + + traceCount + + ".trace" + ) + logger.write(Logger.Level.SUBSTEP, "Writing trace into file: %s%n", traceFile.path) + PrintWriter(traceFile).use { printWriter -> printWriter.write(trace.toString()) } + traceCount++ + + logger.write(Logger.Level.SUBSTEP, "---------------------------%n") + } + val reportFile = File(traceDirPath.absolutePath + File.separator + "report.txt") + logger.write(Logger.Level.MAINSTEP, "Writing report into file: %s%n", reportFile.path) + + PrintWriter(reportFile).use { printWriter -> printWriter.write(report) } + } + + // summary concretization + if (summary) { + val concreteSummaryFile = + traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".cexs" + val cexsString = toCexs(concretizationResult) + PrintWriter(File(concreteSummaryFile)).use { printWriter -> printWriter.write(cexsString) } + logger.write( + Logger.Level.SUBSTEP, + "Concrete trace summary exported to ${concreteSummaryFile}\n", + ) + } + } + + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun doRun() { + val traceDirPath: File = + if (traceDir == null) { + File(inputOptions.model.parent + File.separator + "traces") + } else { + traceDir!! + } + + registerSolverManagers() + val solverFactory = SolverManager.resolveSolverFactory(solver) + + val modelFile = inputOptions.model + if (traceDirPath.exists()) { + MoreFiles.deleteRecursively(traceDirPath.toPath(), RecursiveDeleteOption.ALLOW_INSECURE) + } + traceDirPath.mkdir() + + val propStream = ByteArrayInputStream(("prop {\n" + "\ttrue\n" + "}\n").toByteArray()) + val xsts = + XstsDslManager.createXsts(SequenceInputStream(FileInputStream(modelFile), propStream)) + val sw = Stopwatch.createStarted() + val checker: XstsTracegenConfig = + XstsTracegenBuilder(Z3SolverFactory.getInstance(), true) + .logger(logger) + .setGetFullTraces(false) + .build(xsts) + val result = checker.check() + val summary = result.summary as AbstractTraceSummary, XstsAction> + + val concretizationResult = + XstsTraceGenerationConcretizerUtil.concretizeSummary( + summary, + Z3LegacySolverFactory.getInstance(), + xsts, + ) + + sw.stop() + printResult( + concretizationResult, + result.summary, + sw.elapsed(TimeUnit.MILLISECONDS), + traceDirPath, + xsts, + ) + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt index 24c474808f..39a694a4b2 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli.optiongroup import com.github.ajalt.clikt.parameters.groups.OptionGroup @@ -30,34 +29,38 @@ import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.dsl.XstsDslManager import java.io.* -class InputOptions : OptionGroup( - name = "Input options", - help = "Options related to model and property input" -) { - - val model: File by option( - help = "Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input" - ).file(mustExist = true, canBeDir = false).required() - private val property: InputStream? by option( - help = "Path of the property file. Has priority over --inlineProperty" - ).inputStream() - private val inlineProperty: String? by option(help = "Input property as a string. Ignored if --property is defined") - private val initialmarking: String by option(help = "Initial marking of the pnml model").default("") +class InputOptions : + OptionGroup(name = "Input options", help = "Options related to model and property input") { + val model: File by + option( + help = + "Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input" + ) + .file(mustExist = true, canBeDir = false) + .required() + private val property: InputStream? by + option(help = "Path of the property file. Has priority over --inlineProperty").inputStream() + private val inlineProperty: String? by + option(help = "Input property as a string. Ignored if --property is defined") + private val initialmarking: String by + option(help = "Initial marking of the pnml model").default("") - fun isPnml() = model.path.endsWith("pnml") + fun isPnml() = model.path.endsWith("pnml") - fun loadXsts(): XSTS { - val propertyStream = if (property != null) property else (if (inlineProperty != null) ByteArrayInputStream( - "prop { $inlineProperty }".toByteArray() - ) else null) - if (isPnml()) { - val petriNet = XMLPnmlToPetrinet.parse(model.absolutePath, initialmarking) - return PetriNetToXSTS.createXSTS(petriNet, propertyStream) - } - return XstsDslManager.createXsts( - SequenceInputStream(FileInputStream(model), propertyStream ?: InputStream.nullInputStream()) - ) + fun loadXsts(): XSTS { + val propertyStream = + if (property != null) property + else + (if (inlineProperty != null) ByteArrayInputStream("prop { $inlineProperty }".toByteArray()) + else null) + if (isPnml()) { + val petriNet = XMLPnmlToPetrinet.parse(model.absolutePath, initialmarking) + return PetriNetToXSTS.createXSTS(petriNet, propertyStream) } + return XstsDslManager.createXsts( + SequenceInputStream(FileInputStream(model), propertyStream ?: InputStream.nullInputStream()) + ) + } - fun loadPetriNet(): MutableList = PetriNetParser.loadPnml(model).parsePTNet() -} \ No newline at end of file + fun loadPetriNet(): MutableList = PetriNetParser.loadPnml(model).parsePTNet() +}