Skip to content

Commit

Permalink
Trace generation (#330)
Browse files Browse the repository at this point in the history 
* Added basic dfs trace generator; not tested yet

* tracgen half-done, but ran into some issues; refactor next

* no propert concretizer in progress

* Writing generated traces into files

* minor changes

* Generating maximal traces from xsts

* Deleted some commented code

* Fixed xsts based bug generating extra traces

* Added temporary ARG to file to cegarchecker

* Started adding advanced arg trace for trace generation

* iterative trace lengthening works on small example

* Added get full traces as an option

* Cleaning up tracegen code

* Refactored full trace generation

* Adding configurable initial precision

* Added some trace gen options

* Shortened tracegen algorithm code

* Fixed accidentally changed code

* Patched tracegen feasibility check

* Patched xsts specific superfluous node removal

* Patch superfluous node filtering

* minor fix

* Fixed typo in shortened trace containment check

* Added heuristics for incomplete abstract state coverages

* added correct check inbetween abstract states

* Fixed typo

* Added insecure delete to google recursive delete for windows

* Added basic dfs trace generator; not tested yet

* tracgen half-done, but ran into some issues; refactor next

* no propert concretizer in progress

* Writing generated traces into files

* minor changes

* Generating maximal traces from xsts

* Deleted some commented code

* Fixed xsts based bug generating extra traces

* Added temporary ARG to file to cegarchecker

* Started adding advanced arg trace for trace generation

* iterative trace lengthening works on small example

* Added get full traces as an option

* Cleaning up tracegen code

* Refactored full trace generation

* Adding configurable initial precision

* Added some trace gen options

* Shortened tracegen algorithm code

* Fixed accidentally changed code

* Patched tracegen feasibility check

* Patched xsts specific superfluous node removal

* Patch superfluous node filtering

* minor fix

* Fixed typo in shortened trace containment check

* Added heuristics for incomplete abstract state coverages

* added correct check inbetween abstract states

* Fixed typo

* Added insecure delete to google recursive delete for windows

* optimized imports after rebase

* added promela frontend project

* promela grammar can parse models now

* solve merge conflict

* some promela boilerplate

* adding grammar and model classes to promela frontend

* commented out some of promela grammar

* promela frontend update

* started refactoring trace generation

* refactored and minimized tracegen

* tracegen refactor wip

* adding predicates to tracegen

* readded full traces option and started developing trace metadata

* cleaning up before trace metadata

* added v0 trace metadata, wip refactor tracegen checker

* added basic trace metadata collection; tracegen refactored to clikt

* changing return value of trace generation

* refactor trace metadata to trace summary

* basic trace summary and visualization added

* trace generation checker is now a Checker

* summary concretization and least/most over approx arg node wip

* working on summary concretization

* added feasible concretization and concrete summary

* clean up some templates

* adding summary statuses

* basic summary concretization works

* .cexs can exported, but todos for tracegen with abstraction still present

* wip tracegen to xcfa

* tracegen added to xcfa execute config

* xcfa-cli trace generation can be built, but not tested

* fix config node result type

* added some post tracegen log

* added trace concretizations to xcfa tracegen

* reformatting after merge

* add _ in cexs node id

* added options to (not) get summary/trace set after tracegen for xsts

* added options to (not) get summary/trace set after tracegen for xsts

* fixed --traces and --summary in xsts cli

---------

Co-authored-by: AdamZsofi <[email protected]>
  • Loading branch information
@leventeBajczi @AdamZsofi
leventeBajczi and AdamZsofi authored Dec 2, 2024
1 parent 1bf5fdd commit 0fd5bbe
Show file tree
Hide file tree
Showing 52 changed files with 3,330 additions and 223 deletions.
67 changes: 29 additions & 38 deletions ...ojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<S extends State, A extends Action> {

final ARG<S, A> arg;
Expand All @@ -47,7 +46,12 @@ public final class ArgNode<S extends State, A extends Action> {

public boolean expanded; // Set by ArgBuilder

ArgNode(final ARG<S, A> arg, final S state, final int id, final int depth, final boolean target) {
ArgNode(
final ARG<S, A> arg,
final S state,
final int id,
final int depth,
final boolean target) {
this.arg = arg;
this.state = state;
this.id = id;
Expand All @@ -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;
Expand All @@ -83,6 +87,10 @@ public void setState(final S state) {
this.state = state;
}

public boolean inPartialOrder(final ArgNode<S, A> node) {
return arg.getPartialOrd().isLeq(node.getState(), this.getState());
}

public boolean mayCover(final ArgNode<S, A> node) {
if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed());
Expand Down Expand Up @@ -162,77 +170,59 @@ public Stream<S> 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();
}

////

public Stream<ArgNode<S, A>> 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<ArgNode<S, A>> ancestors() {
Expand Down Expand Up @@ -263,7 +253,8 @@ private Stream<ArgNode<S, A>> 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));
}
}

Expand Down
1 change: 0 additions & 1 deletion ...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,6 @@ public SafetyResult<Pr, C> 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);
Expand Down
166 changes: 166 additions & 0 deletions ...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java
View file
Original file line number Diff line number Diff line change
@@ -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<S extends State, A extends Action> implements Iterable<ArgNode<S, A>> {
private static final int HASH_SEED = 7453;
private volatile int hashCode = 0;

private final List<ArgNode<S, A>> nodes;
private final List<ArgEdge<S, A>> edges;
private final Collection<State> states;

private AdvancedArgTrace(final ArgNode<S, A> node) {
// adding items to first index will lead to O(N^2) performance
final List<ArgNode<S, A>> nodeList = new ArrayList<>();
final List<ArgEdge<S, A>> edgeList = new ArrayList<>();

ArgNode<S, A> running = node;
nodeList.add(running);

while (running.getInEdge().isPresent()) {
final ArgEdge<S, A> 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<ArgNode<S, A>> nodeList, List<ArgEdge<S, A>> edgeList) {
this.nodes = Collections.unmodifiableList(nodeList);
this.edges = Collections.unmodifiableList(edgeList);
states = nodes.stream().map(ArgNode::getState).collect(Collectors.toList());
}

////

public static <S extends State, A extends Action> AdvancedArgTrace<S, A> to(
final ArgNode<S, A> node) {
checkNotNull(node);
return new AdvancedArgTrace<>(node);
}

public static <S extends State, A extends Action> AdvancedArgTrace<S, A> fromTo(
final ArgNode<S, A> fromNode, final ArgNode<S, A> toNode) {
checkNotNull(fromNode);
checkNotNull(toNode);
AdvancedArgTrace<S, A> differenceTrace = new AdvancedArgTrace<>(fromNode);
AdvancedArgTrace<S, A> 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 <A extends Action, S extends State> AdvancedArgTrace<S, A> substituteTrace(
AdvancedArgTrace<S, A> fullTrace, AdvancedArgTrace<S, A> differenceTrace) {
List<ArgNode<S, A>> differenceNodes = differenceTrace.nodes;

List<ArgNode<S, A>> remainingNodes = new ArrayList<>(fullTrace.nodes);
remainingNodes.removeIf(
saArgNode ->
!(saArgNode.equals(differenceNodes.get(differenceNodes.size() - 1)))
&& differenceNodes.contains(saArgNode));

List<ArgEdge<S, A>> 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<S, A> node(final int index) {
return nodes.get(index);
}

public ArgEdge<S, A> edge(final int index) {
return edges.get(index);
}

public List<ArgNode<S, A>> nodes() {
return nodes;
}

public List<ArgEdge<S, A>> edges() {
return edges;
}

////

/**
* Converts the ArgTrace to a Trace by extracting states and actions from nodes and edges
* respectively.
*/
public Trace<S, A> toTrace() {
final List<S> states = nodes.stream().map(ArgNode::getState).collect(toList());
final List<A> actions = edges.stream().map(ArgEdge::getAction).collect(toList());
return Trace.of(states, actions);
}

////

@Override
public Iterator<ArgNode<S, A>> 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);
}
}
Loading

0 comments on commit 0fd5bbe

Please sign in to comment.