diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts index c89e90bd86..f8ef04551d 100644 --- a/buildSrc/build.gradle.kts +++ b/buildSrc/build.gradle.kts @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -import java.io.FileOutputStream import org.jetbrains.kotlin.gradle.plugin.KotlinSourceSet import org.jetbrains.kotlin.gradle.tasks.KotlinCompile @@ -90,6 +89,11 @@ fun generateVersionsSource(): String { } tasks { + withType() { + kotlinOptions { + jvmTarget = "17" + } + } val generateVersions by creating { description = "Updates Versions.kt from project properties." group = "build" diff --git a/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts b/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts index 0f389f77d9..e2f92f2090 100644 --- a/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts +++ b/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -import java.nio.file.Files apply() diff --git a/buildSrc/src/main/kotlin/kotlin-common.gradle.kts b/buildSrc/src/main/kotlin/kotlin-common.gradle.kts index 7db603aca9..30449c1784 100644 --- a/buildSrc/src/main/kotlin/kotlin-common.gradle.kts +++ b/buildSrc/src/main/kotlin/kotlin-common.gradle.kts @@ -29,4 +29,21 @@ tasks { jvmTarget = "17" } } +} + +// Check if "antlr-common" plugin is applied and if the "generateGrammarSource" task is available +// If yes, add a task dependency from "compileKotlin" to "generateGrammarSource" +project.plugins.withType { + val generateGrammarTask = tasks.findByName("generateGrammarSource") + if (generateGrammarTask != null) { + project.tasks.named("compileKotlin").configure { + dependsOn(generateGrammarTask) + } + } + val generateTestGrammarTask = tasks.findByName("generateTestGrammarSource") + if (generateTestGrammarTask != null) { + project.tasks.named("compileTestKotlin").configure { + dependsOn(generateTestGrammarTask) + } + } } \ No newline at end of file diff --git a/settings.gradle.kts b/settings.gradle.kts index 239c40e12f..1a5e96db2d 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -34,6 +34,7 @@ include( "xcfa/xcfa", "xcfa/cat", + "xcfa/exec-graph-cli", "xcfa/c2xcfa", "xcfa/litmus2xcfa", "xcfa/xcfa-analysis", @@ -51,7 +52,8 @@ include( "solver/solver", "solver/solver-z3", "solver/solver-smtlib", - "solver/solver-smtlib-cli" + "solver/solver-smtlib-cli", + "solver/graph-solver", ) for (project in rootProject.children) { diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index c892d00818..dae61a15a5 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/subprojects/common/analysis/build.gradle.kts @@ -22,5 +22,6 @@ dependencies { implementation(project(":theta-common")) implementation(project(":theta-core")) implementation(project(":theta-solver")) + implementation(project(":theta-graph-solver")) testImplementation(project(":theta-solver-z3")) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraph.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraph.java deleted file mode 100644 index 9b89c96519..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraph.java +++ /dev/null @@ -1,466 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import com.google.common.collect.Sets; -import hu.bme.mit.theta.common.TupleN; -import hu.bme.mit.theta.common.datalog.DatalogArgument; -import hu.bme.mit.theta.common.datalog.GenericDatalogArgument; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.solver.Solver; -import tools.refinery.store.map.Cursor; -import tools.refinery.store.model.Model; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.model.ModelStoreImpl; -import tools.refinery.store.model.Tuple; -import tools.refinery.store.model.representation.Relation; -import tools.refinery.store.model.representation.TruthValue; - -import java.util.*; -import java.util.stream.Collectors; - -import static hu.bme.mit.theta.core.decl.Decls.Const; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; - -public class ExecutionGraph { - private final MCM mcm; - private final EncodedRelationWrapper encodedRelationWrapper; - private final ModelStore store; - private Model model; - private final Relation po, _int, ext, addr, ctrl, rmw, amo, loc, id, data, R, W, F, U; - private final Map> tags; - private final Relation rf, co; - private final long staticOnlyCommit; - - public ExecutionGraph(final ExecutionGraphBuilder builder, final MCM mcm, final Solver solver) { - this.mcm = mcm; - encodedRelationWrapper = new EncodedRelationWrapper(solver); - po = new Relation<>("po-raw", 2, false); - _int = new Relation<>("_int", 2, false); - ext = new Relation<>("ext", 2, false); - addr = new Relation<>("addr", 2, false); - ctrl = new Relation<>("ctrl", 2, false); - rmw = new Relation<>("rmw", 2, false); - amo = new Relation<>("amo", 2, false); - loc = new Relation<>("loc", 2, false); - id = new Relation<>("id", 2, false); - data = new Relation<>("data", 2, false); - R = new Relation<>("R", 1, false); - W = new Relation<>("W", 1, false); - F = new Relation<>("F", 1, false); - U = new Relation<>("U", 1, false); - rf = new Relation<>("rf", 2, TruthValue.UNKNOWN); - co = new Relation<>("co", 2, TruthValue.UNKNOWN); - this.tags = new LinkedHashMap<>(); - builder.getTags().forEach((key, value) -> { - final Relation rel = new Relation<>(key, 1, false); - this.tags.put(key, rel); - }); - store = new ModelStoreImpl(Sets.union(Set.copyOf(this.tags.values()), Set.of(po, _int, ext, addr, ctrl, rmw, amo, loc, id, data, R, W, F, U, rf, co))); - model = store.createModel(); - - builder.getPoRaw().getElements().forEach(elem -> model.put(po, datalog2tup(elem), true)); - builder.getLocCalculated().getElements().forEach(elem -> model.put(loc, datalog2tup(elem), true)); - builder.getIntCalculated().getElements().forEach(elem -> model.put(_int, datalog2tup(elem), true)); - builder.getData().getElements().forEach(elem -> model.put(data, datalog2tup(elem), true)); - builder.getAddr().getElements().forEach(elem -> model.put(addr, datalog2tup(elem), true)); - builder.getCtrl().getElements().forEach(elem -> model.put(ctrl, datalog2tup(elem), true)); - builder.getRmw().getElements().forEach(elem -> model.put(rmw, datalog2tup(elem), true)); - builder.getAmo().getElements().forEach(elem -> model.put(amo, datalog2tup(elem), true)); - builder.getR().getElements().forEach(elem -> model.put(R, datalog2tup(elem), true)); - builder.getW().getElements().forEach(elem -> model.put(W, datalog2tup(elem), true)); - builder.getF().getElements().forEach(elem -> model.put(F, datalog2tup(elem), true)); - Collection> intElements = builder.getIntCalculated().getElements(); - builder.getU().getElements().forEach(elem -> { - model.put(U, datalog2tup(elem), true); - model.put(id, Tuple.of(datalog2tup(elem).get(0), datalog2tup(elem).get(0)), true); - builder.getU().getElements().forEach(elem2 -> { - TupleN tuple = tupleN(elem.get(0), elem2.get(0)); - TupleN tupleDA = TupleN.of(GenericDatalogArgument.createArgument(elem.get(0)), GenericDatalogArgument.createArgument(elem2.get(0))); - if (!intElements.contains(tupleDA)) { - model.put(ext, tup(tuple), true); - } - }); - }); - - builder.getTags().forEach((key, value) -> { - value.getElements().forEach(elem -> model.put(this.tags.get(key), datalog2tup(elem), true)); - }); - - - encode(); - - staticOnlyCommit = model.commit(); - encodedRelationWrapper.getSolver().push(); - } - - public void reset() { - model = store.createModel(staticOnlyCommit); - encodedRelationWrapper.getSolver().pop(); - } - - public boolean nextSolution(final Collection, LitExpr>> solutions) { - model = store.createModel(staticOnlyCommit); - if (encodedRelationWrapper.getSolver().check().isSat()) { - solutions.add(Map.copyOf(encodedRelationWrapper.getSolver().getModel().toMap())); - final EventConstantLookup rf = encodedRelationWrapper.getEventLookup("rf"); - final EventConstantLookup co = encodedRelationWrapper.getEventLookup("co"); - - final Map, LitExpr> lut = encodedRelationWrapper.getSolver().getModel().toMap(); - final List> subexprs = new ArrayList<>(); - - rf.getAll().forEach((tuple, constDecl) -> { - if (lut.get(constDecl).equals(True())) { - model.put(this.rf, tup(tuple), TruthValue.TRUE); - subexprs.add(constDecl.getRef()); - } else subexprs.add(Not(constDecl.getRef())); - }); - co.getAll().forEach((tuple, constDecl) -> { - if (lut.get(constDecl).equals(True())) - model.put(this.co, tup(tuple), TruthValue.TRUE); - }); - - encodedRelationWrapper.getSolver().add(Not(And(subexprs))); - - return true; - } - return false; - } - - private TupleN tupleN(final DatalogArgument a, final DatalogArgument b) { - final int i = ((GenericDatalogArgument) a).getContent(); - final int j = ((GenericDatalogArgument) b).getContent(); - return TupleN.of(i, j); - } - - private Tuple datalog2tup(final TupleN from) { - final int i = ((GenericDatalogArgument) from.get(0)).getContent(); - if (from.arity() == 1) return Tuple.of(i); - final int j = ((GenericDatalogArgument) from.get(1)).getContent(); - return Tuple.of(i, j); - } - - private Tuple tup(final TupleN from) { - final int i = from.get(0); - if (from.arity() == 1) return Tuple.of(i); - final int j = from.get(1); - return Tuple.of(i, j); - } - - private void encode() { - final Cursor allEvents = model.getAll(U); - final List idList = new ArrayList<>(); - for (allEvents.move(); !allEvents.isTerminated(); allEvents.move()) { - if (allEvents.getValue()) idList.add(allEvents.getKey().get(0)); - } - - for (final MCMConstraint constraint : mcm.getConstraints()) { - constraint.encodeEvents(idList, encodedRelationWrapper); - } - - EventConstantLookup po = getOrCreate(encodedRelationWrapper, idList, "po-raw", false); - EventConstantLookup _int = getOrCreate(encodedRelationWrapper, idList, "int", false); - EventConstantLookup loc = getOrCreate(encodedRelationWrapper, idList, "loc", false); - EventConstantLookup data = getOrCreate(encodedRelationWrapper, idList, "data", false); - EventConstantLookup rmw = getOrCreate(encodedRelationWrapper, idList, "rmw", false); - EventConstantLookup amo = getOrCreate(encodedRelationWrapper, idList, "amo", false); - EventConstantLookup ctrl = getOrCreate(encodedRelationWrapper, idList, "ctrl", false); - EventConstantLookup ext = getOrCreate(encodedRelationWrapper, idList, "ext", false); - EventConstantLookup addr = getOrCreate(encodedRelationWrapper, idList, "addr", false); - EventConstantLookup id = getOrCreate(encodedRelationWrapper, idList, "id", false); - EventConstantLookup rf = getOrCreate(encodedRelationWrapper, idList, "rf", false); - EventConstantLookup co = getOrCreate(encodedRelationWrapper, idList, "co", false); - EventConstantLookup R = getOrCreate(encodedRelationWrapper, idList, "R", true); - EventConstantLookup W = getOrCreate(encodedRelationWrapper, idList, "W", true); - EventConstantLookup F = getOrCreate(encodedRelationWrapper, idList, "F", true); - EventConstantLookup U = getOrCreate(encodedRelationWrapper, idList, "U", true); - - for (final int i : idList) { - encodeUnaryRelation(this.R, encodedRelationWrapper, R, i); - encodeUnaryRelation(this.W, encodedRelationWrapper, W, i); - encodeUnaryRelation(this.F, encodedRelationWrapper, F, i); - encodeUnaryRelation(this.U, encodedRelationWrapper, U, i); - } - this.tags.forEach((s, rel) -> { - EventConstantLookup ecl = getOrCreate(encodedRelationWrapper, idList, s, true); - for (int i : idList) { - encodeUnaryRelation(rel, encodedRelationWrapper, ecl, i); - } - }); - - - encodeRelation(encodedRelationWrapper, idList, this._int, _int); - encodePo(encodedRelationWrapper, idList, this.po, this._int, po); - encodeRelation(encodedRelationWrapper, idList, this.loc, loc); - encodeRelation(encodedRelationWrapper, idList, this.id, id); - encodeRelation(encodedRelationWrapper, idList, this.data, data); - encodeRelation(encodedRelationWrapper, idList, this.rmw, rmw); - encodeRelation(encodedRelationWrapper, idList, this.amo, amo); - encodeRelation(encodedRelationWrapper, idList, this.ctrl, ctrl); - encodeRelation(encodedRelationWrapper, idList, this.ext, ext); - encodeRelation(encodedRelationWrapper, idList, this.addr, addr); - - for (final int i : idList) { - addRfConstraints(encodedRelationWrapper, idList, rf, i); - addCoConstraints(encodedRelationWrapper, idList, co, i); - } - - // encode missing relations - encodedRelationWrapper.getNonEncoded().forEach((key, value) -> { - final MCMRelation mcmRelation = mcm.getRelations().get(key); - if (mcmRelation != null && mcmRelation.getRule() == null) { - final int arity = mcmRelation.getArity(); - EventConstantLookup ecl = getOrCreate(encodedRelationWrapper, idList, key, arity == 1); - encodedRelationWrapper.setEncoded(ecl); - for (final int i : idList) { - if (arity == 1) { - encodedRelationWrapper.getSolver().add(Not(ecl.get(TupleN.of(i)).getRef())); - } else { - for (final int j : idList) { - encodedRelationWrapper.getSolver().add(Not(ecl.get(TupleN.of(i, j)).getRef())); - } - } - } - } - - }); - } - - private void encodePo(EncodedRelationWrapper encodedRelationWrapper, List idList, Relation rel, Relation _int, EventConstantLookup enc) { - encodedRelationWrapper.setEncoded(enc); - for (final int i : idList) { - List> collectors = new ArrayList<>(); - for (final int j : idList) { - if (model.get(rel, Tuple.of(i, j))) { - boolean foundSet = false; - for (Set integers : collectors) { - if (model.get(_int, Tuple.of(j, integers.stream().findAny().get()))) { - integers.add(j); - foundSet = true; - break; - } - } - if (!foundSet) { - Set set = new LinkedHashSet<>(); - set.add(j); - collectors.add(set); - } - } else { - encodedRelationWrapper.getSolver().add(Not(enc.get(TupleN.of(i, j)).getRef())); - } - } - for (Set collector : collectors) { - if (collector.size() > 1) { - encodedRelationWrapper.getSolver().add(Or(collector.stream().map(j -> enc.get(TupleN.of(i, j)).getRef()).collect(Collectors.toList()))); - } else if (collector.size() > 0) { - encodedRelationWrapper.getSolver().add(enc.get(TupleN.of(i, collector.stream().findAny().get())).getRef()); - } - } - } - } - - private EventConstantLookup getOrCreate( - final EncodedRelationWrapper encodedRelationWrapper, - final List idList, - final String name, - final boolean isUnary) { - EventConstantLookup lookup = encodedRelationWrapper.getEventLookup(name); - if (lookup == null) { - lookup = createDummyRelation(idList, name, isUnary); - encodedRelationWrapper.addEvent(name, lookup); - } - return lookup; - } - - private void encodeUnaryRelation(Relation rel, EncodedRelationWrapper encodedRelationWrapper, EventConstantLookup enc, int i) { - encodedRelationWrapper.setEncoded(enc); - if (model.get(rel, Tuple.of(i))) { - encodedRelationWrapper.getSolver().add(enc.get(TupleN.of(i)).getRef()); - } else { - encodedRelationWrapper.getSolver().add(Not(enc.get(TupleN.of(i)).getRef())); - } - } - - private void encodeRelation(EncodedRelationWrapper encodedRelationWrapper, List idList, Relation rel, EventConstantLookup enc) { - encodedRelationWrapper.setEncoded(enc); - for (final int i : idList) { - for (final int j : idList) { - if (model.get(rel, Tuple.of(i, j))) { - encodedRelationWrapper.getSolver().add(enc.get(TupleN.of(i, j)).getRef()); - } else { - encodedRelationWrapper.getSolver().add(Not(enc.get(TupleN.of(i, j)).getRef())); - } - } - } - } - - private EventConstantLookup createDummyRelation(List idList, String name, boolean isUnary) { - EventConstantLookup eventConstantLookup = new EventConstantLookup(); - for (final int i : idList) { - if (isUnary) { - eventConstantLookup.add(TupleN.of(i), Const(name + "_" + i, Bool())); - } else { - for (final int j : idList) { - eventConstantLookup.add(TupleN.of(i, j), Const(name + "_" + i + "_" + j, Bool())); - } - } - } - return eventConstantLookup; - } - - private void addCoConstraints(EncodedRelationWrapper encodedRelationWrapper, List idList, EventConstantLookup co, int i) { - encodedRelationWrapper.setEncoded(co); - if (model.get(W, Tuple.of(i))) { - final List> subexprs = new ArrayList<>(); - for (final int j : idList) { - if (model.get(W, Tuple.of(j)) && model.get(loc, Tuple.of(i, j))) { - if (i == j) subexprs.add(Not(co.get(TupleN.of(i, j)).getRef())); - else { - subexprs.add(Xor(co.get(TupleN.of(i, j)).getRef(), co.get(TupleN.of(j, i)).getRef())); - for (final int k : idList) { - if (model.get(W, Tuple.of(k)) && model.get(loc, Tuple.of(i, k)) && i != k && j != k) { - final RefExpr a = co.get(TupleN.of(i, k)).getRef(); - final RefExpr b = co.get(TupleN.of(k, j)).getRef(); - final RefExpr c = co.get(TupleN.of(i, j)).getRef(); - subexprs.add(Imply(And(a, b), c)); - } - } - } - } else { - encodedRelationWrapper.getSolver().add(Not(co.get(TupleN.of(i, j)).getRef())); // not W->W [samevar] - } - } - encodedRelationWrapper.getSolver().add(And(subexprs)); - } else { - for (final int j : idList) { - encodedRelationWrapper.getSolver().add(Not(co.get(TupleN.of(i, j)).getRef())); // not W->W [samevar] - } - } - } - - private void addRfConstraints(EncodedRelationWrapper encodedRelationWrapper, List idList, EventConstantLookup rf, int i) { - encodedRelationWrapper.setEncoded(rf); - if (model.get(R, Tuple.of(i))) { - final List> subexprs = new ArrayList<>(); - for (final int j : idList) { - if (model.get(W, Tuple.of(j)) && model.get(loc, Tuple.of(i, j))) { - final List> innerSubexprs = new ArrayList<>(); - for (final int k : idList) { - if (model.get(W, Tuple.of(k)) && j != k) { - innerSubexprs.add(Not(rf.get(TupleN.of(k, i)).getRef())); - } - } - innerSubexprs.add(rf.get(TupleN.of(j, i)).getRef()); - subexprs.add(And(innerSubexprs)); - } else { - encodedRelationWrapper.getSolver().add(Not(rf.get(TupleN.of(j, i)).getRef())); // not W->R [samevar] - } - } - encodedRelationWrapper.getSolver().add(Or(subexprs)); - } else { - for (final int j : idList) { - encodedRelationWrapper.getSolver().add(Not(rf.get(TupleN.of(j, i)).getRef())); // not W->R [samevar] - } - } - } - - - public void print(Map> vars) { - System.out.println("digraph G{"); - printEvents(vars); - printBinaryRelation(po, true); -// printBinaryRelation(loc, false); - printBinaryCalculatedRelation(rf, "red"); - printBinaryCalculatedRelation(co, "purple"); - System.out.println("}"); - } - - private void printEvents(Map> vars) { - Cursor all = model.getAll(U); - all.move(); - while (!all.isTerminated()) { - if (all.getValue()) { - final int key = all.getKey().get(0); - final String name = whichEvent(all.getKey()); - final String tags = collectTags(all.getKey()); - final VarDecl var = vars.get(key); - System.out.println(key + "[label=\"" + name + (var == null ? "" : "(" + var.getName() + ")") + tags + "\"];"); - } - all.move(); - } - } - - private String collectTags(Tuple key) { - final List ret = new ArrayList<>(); - tags.forEach((s, booleanRelation) -> { - if (model.get(booleanRelation, key)) ret.add(s); - }); - final StringJoiner sj = new StringJoiner(", ", "[", "]"); - return sj.toString(); - } - - private String whichEvent(Tuple key) { - if (model.get(R, key)) return "R"; - if (model.get(W, key)) return "W"; - if (model.get(F, key)) return "F"; - throw new RuntimeException("Unsupported event type"); - } - - private void printBinaryRelation(Relation r, boolean constraint) { - Cursor all = model.getAll(r); - all.move(); - while (!all.isTerminated()) { - if (all.getValue()) { - int source = all.getKey().get(0); - int target = all.getKey().get(1); - System.out.println(source + " -> " + target + "[label=\"" + r.getName() + "\"" + (constraint ? "" : ",constraint=false") + "];"); - } - all.move(); - } - } - - private void printBinaryCalculatedRelation(Relation r, String color) { - Cursor all = model.getAll(r); - all.move(); - while (!all.isTerminated()) { - int source = all.getKey().get(0); - int target = all.getKey().get(1); - String name = "\"" + r.getName() + "\""; - if (all.getValue() == TruthValue.FALSE) name = "\"" + r.getName() + "\""; - System.out.println(source + " -> " + target + "[label=" + name + ",constraint=false,color=" + color + "];"); - all.move(); - } - } - - public Collection getRf() { - final Cursor cursor = model.getAll(rf); - cursor.move(); - final Collection ret = new ArrayList<>(); - while (!cursor.isTerminated()) { - if (cursor.getValue().must()) { - ret.add(cursor.getKey()); - } - cursor.move(); - } - return ret; - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphBuilder.java deleted file mode 100644 index e970ec6178..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphBuilder.java +++ /dev/null @@ -1,183 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.common.TupleN; -import hu.bme.mit.theta.common.datalog.Datalog; -import hu.bme.mit.theta.common.datalog.DatalogArgument; -import hu.bme.mit.theta.common.datalog.GenericDatalogArgument; - -import java.util.Collection; -import java.util.LinkedHashMap; -import java.util.Map; - -public class ExecutionGraphBuilder { - private final Datalog program; - private final Datalog.Relation initWrite, poRaw, /*TODO: remove */ - poCalculated, intRaw, intCalculated, locRaw, locCalculated, R, W, F, U, data, addr, ctrl, rmw, amo; - private final Map tags; - private int lastCnt = 1; - - public ExecutionGraphBuilder() { - program = Datalog.createProgram(); - initWrite = program.createRelation("IW", 1); - poRaw = program.createRelation("po_raw", 2); - intRaw = program.createRelation("int_raw", 2); - locRaw = program.createRelation("loc_raw", 2); - R = program.createRelation("R", 1); - W = program.createRelation("W", 1); - F = program.createRelation("F", 1); - U = program.createRelation("U", 1); - data = program.createRelation("data", 2); - addr = program.createRelation("addr", 2); - ctrl = program.createRelation("ctrl", 2); - rmw = program.createRelation("rmw", 2); - amo = program.createRelation("amo", 2); - this.tags = new LinkedHashMap<>(); - - poCalculated = program.createRelation("po", 2); - intCalculated = program.createCommonSource("int", intRaw); - locCalculated = program.createCommonSource("loc", locRaw); - } - - private static TupleN arg(int i, int j) { - return TupleN.of(GenericDatalogArgument.createArgument(i), GenericDatalogArgument.createArgument(j)); - } - - private static TupleN arg(int i) { - return TupleN.of(GenericDatalogArgument.createArgument(i)); - } - - private int addEvent(int processId, int lastNode, final Collection tags) { - final int id = lastCnt++; - if (lastNode > 0) { - poRaw.addFact(arg(lastNode, id)); - } else { - for (TupleN element : initWrite.getElements()) { - int iw = ((GenericDatalogArgument) element.get(0)).getContent(); - poRaw.addFact(arg(iw, id)); - } - } - for (final String tag : tags) { - this.tags.putIfAbsent(tag, program.createRelation(tag, 1)); - final Datalog.Relation relation = this.tags.get(tag); - relation.addFact(arg(id)); - } - intRaw.addFact(arg(processId, id)); - U.addFact(arg(id)); - return id; - } - - private int addMemoryEvent(int processId, int varId, int lastNode, Datalog.Relation rel, final Collection tags) { - final int id = addEvent(processId, lastNode, tags); - locRaw.addFact(arg(varId, id)); - rel.addFact(arg(id)); - return id; - } - - public int addRead(final int processId, final int varId, final int lastNode, final Collection tags) { - return addMemoryEvent(processId, varId, lastNode, R, tags); - } - - public int addWrite(final int processId, final int varId, final int lastNode, final Collection tags) { - return addMemoryEvent(processId, varId, lastNode, W, tags); - } - - public void addDependency(int read, int write) { - data.addFact(arg(read, write)); - } - - public int addInitialWrite(final int varId) { - final int id = lastCnt++; - locRaw.addFact(arg(varId, id)); - initWrite.addFact(arg(id)); - W.addFact(arg(id)); - U.addFact(arg(id)); - return id; - } - - public int addFence(final int processId, final int lastNode, final Collection tags) { - final int id = addEvent(processId, lastNode, tags); - F.addFact(arg(id)); - return id; - } - - public Datalog.Relation getPoRaw() { - return poRaw; - } - - public Datalog.Relation getPoCalculated() { - return poCalculated; - } - - public Datalog.Relation getIntRaw() { - return intRaw; - } - - public Datalog.Relation getIntCalculated() { - return intCalculated; - } - - public Datalog.Relation getLocRaw() { - return locRaw; - } - - public Datalog.Relation getLocCalculated() { - return locCalculated; - } - - public Datalog.Relation getData() { - return data; - } - - public Datalog.Relation getR() { - return R; - } - - public Datalog.Relation getW() { - return W; - } - - public Datalog.Relation getF() { - return F; - } - - public Datalog.Relation getU() { - return U; - } - - - public Datalog.Relation getAddr() { - return addr; - } - - public Datalog.Relation getCtrl() { - return ctrl; - } - - public Datalog.Relation getRmw() { - return rmw; - } - - public Datalog.Relation getAmo() { - return amo; - } - - public Map getTags() { - return tags; - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphVisualizer.java deleted file mode 100644 index 0e49e51583..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphVisualizer.java +++ /dev/null @@ -1,285 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.type.LitExpr; - -import javax.swing.*; -import java.awt.*; -import java.awt.geom.Path2D; -import java.util.List; -import java.util.*; - -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - -public class ExecutionGraphVisualizer implements Runnable { - private final List, LitExpr>> solutions; - private int currentSolution = 0; - private final Map> events; - private final Map> eventLabels; - private final Map varLookup; - private final double eventWidth, eventHeight, separatorY; - private final Map relations; - private final Map possibleRelations; - private static final Set alwaysShow = Set.of("rf", "R", "W", "F"); - private final List initialWrites; - - public ExecutionGraphVisualizer( - final Collection, LitExpr>> solutions, - final List> threadEvents, - Map varLookup, final List initialWrites) { - this.solutions = List.copyOf(solutions); - this.varLookup = varLookup; - this.events = new LinkedHashMap<>(); - int threadNum = Integer.max(threadEvents.size(), initialWrites.size()); - int instructionNum = threadEvents.stream().map(List::size).max(Integer::compareTo).get() + 1; - double dX = 90.0 / (threadNum + 1); - double dY = 90.0 / (instructionNum + 1); - eventWidth = dX * 0.45; - eventHeight = dY * 0.45; - separatorY = dY + 5.0 + eventHeight; - for (int i = 1; i <= threadEvents.size(); i++) { - double x = i * dX + 5.0; - for (int j = 1; j <= threadEvents.get(i - 1).size(); j++) { - double y = (j + 1) * dY + 5.0; - events.put(threadEvents.get(i - 1).get(j - 1), Tuple2.of(x, y)); - } - } - for (int i = 1; i <= initialWrites.size(); i++) { - double x = i * dX + 5.0; - double y = 1 * dY + 5.0; - events.put(initialWrites.get(i - 1), Tuple2.of(x, y)); - } - possibleRelations = new LinkedHashMap<>(); - for (Map, LitExpr> solution : solutions) { - for (Decl decl : solution.keySet()) { - String[] s = decl.getName().split("_"); - possibleRelations.put(s[0], s.length - 1); - } - } - relations = new LinkedHashMap<>(); - eventLabels = new LinkedHashMap<>(); - this.initialWrites = initialWrites; - } - - - @Override - public void run() { - final JFrame frame = new JFrame("Execution Graph Visualizer - Theta"); - frame.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); - frame.setSize(1024, 768); - final JPanel mainPanel = new JPanel(new BorderLayout()); - frame.setContentPane(mainPanel); - - JComboBox solutionChooser = new JComboBox<>(); - for (int i = 0; i < solutions.size(); i++) { - solutionChooser.addItem(i); - } - solutionChooser.addActionListener(actionEvent -> { - currentSolution = solutionChooser.getSelectedIndex(); - frame.invalidate(); - frame.repaint(); - }); - mainPanel.add(solutionChooser, BorderLayout.NORTH); - final JPanel relationPanel = new JPanel(new BorderLayout()); - relationPanel.setLayout(new BoxLayout(relationPanel, BoxLayout.PAGE_AXIS)); - JScrollPane scrollpanel = new JScrollPane(relationPanel, - JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, - JScrollPane.HORIZONTAL_SCROLLBAR_NEVER); - scrollpanel.getVerticalScrollBar().setUnitIncrement(16); - final JPanel drawingPanel = new ExecutionGraphPanel(); - mainPanel.add(drawingPanel, BorderLayout.CENTER); - possibleRelations.entrySet().stream().sorted(Map.Entry.comparingByKey()).forEach(entry -> { - int arity = entry.getValue(); - String s = entry.getKey(); - JCheckBox jCheckBox = new JCheckBox(s); - if (alwaysShow.contains(s)) { - jCheckBox.setSelected(true); - relations.put(s, getColor(s)); - } - jCheckBox.addActionListener(actionEvent -> { - if (jCheckBox.isSelected()) { - relations.put(s, getColor(s)); - } else { - relations.remove(s); - } - frame.invalidate(); - frame.repaint(); - }); - relationPanel.add(jCheckBox); - }); - mainPanel.add(scrollpanel, BorderLayout.WEST); - frame.setVisible(true); - } - - private Color getColor(String relation) { - Random random = new Random(relation.hashCode()); - return switch (relation) { - case "po" -> Color.BLACK; - case "rf" -> Color.RED; - case "co" -> Color.MAGENTA; - default -> getRandomColor(random); - }; - } - - private Color getRandomColor(Random random) { - while (true) { - int r = random.nextInt(256); - int g = random.nextInt(256); - int b = random.nextInt(256); - if (r + g + b <= 256 * 2) { - return new Color(r, g, b); - } - } - } - - private class ExecutionGraphPanel extends JPanel { - @Override - protected void paintComponent(Graphics g) { - float strokeSize = Float.min(getWidth() / 100.0f / 4, getHeight() / 100.0f / 4); - ((Graphics2D) g).setStroke(new BasicStroke(strokeSize)); - ((Graphics2D) g).setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - ((Graphics2D) g).setRenderingHint(RenderingHints.KEY_STROKE_CONTROL, RenderingHints.VALUE_STROKE_PURE); - - double separatorY = ExecutionGraphVisualizer.this.separatorY * getHeight() / 100.0f; - int width = getWidth(); - Path2D.Double myPath = new Path2D.Double(); - boolean drawing = false; - for (int i = 0; i < width; i += width / 50) { - if (drawing) { - myPath.lineTo(i, separatorY); - } else { - myPath.moveTo(i, separatorY); - } - drawing = !drawing; - } - ((Graphics2D) g).draw(myPath); - - double eventWidth = ExecutionGraphVisualizer.this.eventWidth * getWidth() / 100.0f; - double eventHeight = ExecutionGraphVisualizer.this.eventHeight * getHeight() / 100.0f; - solutions.get(currentSolution).forEach((decl, lit) -> { - if (lit.equals(True())) { - String[] s = decl.getName().split("_"); - if (relations.containsKey(s[0]) && s.length == 3 && isChosen(Integer.valueOf(s[1])) && isChosen(Integer.valueOf(s[2]))) { - Tuple2 a = events.get(Integer.valueOf(s[1])); - Tuple2 b = events.get(Integer.valueOf(s[2])); - a = Tuple2.of(getWidth() / 100.0f * a.get1(), getHeight() / 100.0f * a.get2()); - b = Tuple2.of(getWidth() / 100.0f * b.get1(), getHeight() / 100.0f * b.get2()); - Color color = g.getColor(); - g.setColor(relations.get(s[0])); - Path2D.Double path = new Path2D.Double(); - double offset = 25 * (0.8 + 0.4 * new Random(decl.hashCode()).nextDouble()); -// double offset = Double.min(Math.abs(a.get1() - b.get1()), Math.abs(a.get2() - b.get2())) * 0.1 * (0.8 + 0.4 * new Random(decl.hashCode()).nextDouble()); - Tuple2 normal = Tuple2.of(a.get2() - b.get2(), b.get1() - a.get1()); - double norm = Math.sqrt(normal.get1() * normal.get1() + normal.get2() * normal.get2()); - normal = Tuple2.of(normal.get1() / norm, normal.get2() / norm); - Tuple2 dir = Tuple2.of(b.get1() - a.get1(), b.get2() - a.get2()); - double dirnorm = Math.sqrt(dir.get1() * dir.get1() + dir.get2() * dir.get2()); - dir = Tuple2.of(dir.get1() / dirnorm, dir.get2() / dirnorm); - - - a = Tuple2.of(a.get1() + dir.get1() * eventWidth / 1.8, a.get2() + dir.get2() * eventHeight / 1.8); - b = Tuple2.of(b.get1() - dir.get1() * eventWidth / 1.8, b.get2() - dir.get2() * eventHeight / 1.8); - Tuple2 midpoint = Tuple2.of( - (b.get1() + a.get1()) / 2 + offset * normal.get1(), - (b.get2() + a.get2()) / 2 + offset * normal.get2()); - - path.moveTo(a.get1(), a.get2()); - path.curveTo( - a.get1(), a.get2(), - midpoint.get1(), midpoint.get2(), - b.get1(), b.get2() - ); - Tuple2 derivative = Tuple2.of(2 * b.get1() - 2 * midpoint.get1(), 2 * b.get2() - 2 * midpoint.get2()); - double derivativenorm = Math.sqrt(derivative.get1() * derivative.get1() + derivative.get2() * derivative.get2()); - double arrowSize = strokeSize * 4; - derivative = Tuple2.of(derivative.get1() / derivativenorm * arrowSize, derivative.get2() / derivativenorm * arrowSize); - - Tuple2 arrow1vec = vecRotated(derivative, Math.PI / 4); - Tuple2 arrow2vec = vecRotated(derivative, -Math.PI / 4); - path.moveTo(b.get1(), b.get2()); - path.lineTo((b.get1() - arrow1vec.get1()), (b.get2() - arrow1vec.get2())); - path.moveTo(b.get1(), b.get2()); - path.lineTo((b.get1() - arrow2vec.get1()), (b.get2() - arrow2vec.get2())); - - - ((Graphics2D) g).draw(path); - g.setColor(color); - } - } - }); - eventLabels.clear(); - solutions.get(currentSolution).forEach((decl, lit) -> { - if (lit.equals(True())) { - String[] s = decl.getName().split("_"); - if (relations.containsKey(s[0]) && s.length == 2) { - eventLabels.putIfAbsent(Integer.valueOf(s[1]), new ArrayList<>()); - eventLabels.get(Integer.valueOf(s[1])).add(s[0]); - Collections.sort(eventLabels.get(Integer.valueOf(s[1]))); - } - } - }); - events.forEach((integer, tuple) -> { - boolean chosen = isChosen(integer); - if (chosen) { - drawEvent((int) (getWidth() / 100.0f * tuple.get1()), (int) (getHeight() / 100.0f * tuple.get2()), g); - StringJoiner stringJoiner = new StringJoiner(", ", "{", "}"); - if (eventLabels.containsKey(integer)) - eventLabels.get(integer).forEach(i -> stringJoiner.add(i)); - stringJoiner.add("" + integer); - if (varLookup.containsKey(integer)) stringJoiner.add(varLookup.get(integer)); - drawLabelForEvent(stringJoiner.toString(), (int) (getWidth() / 100.0f * tuple.get1()), (int) (getHeight() / 100.0f * tuple.get2()), g); - } - }); - } - - private boolean isChosen(Integer j) { - for (Map.Entry, LitExpr> entry : solutions.get(currentSolution).entrySet()) { - Decl decl = entry.getKey(); - LitExpr litExpr = entry.getValue(); - if (decl.getName().equals("T_" + j) && litExpr.equals(True())) return true; - } - return false; - } - - private Tuple2 vecRotated(Tuple2 dir, double v) { - return Tuple2.of( - dir.get1() * Math.cos(v) - dir.get2() * Math.sin(v), - dir.get1() * Math.sin(v) + dir.get2() * Math.cos(v)); - } - - private void drawLabelForEvent(String s, int x, int y, Graphics g) { - g.setColor(Color.BLACK); - g.setFont(g.getFont().deriveFont((float) (0.25 * Double.min(eventHeight * getWidth() / 100.0f, eventWidth * getWidth() / 100.0f)))); - FontMetrics fontMetrics = g.getFontMetrics(); - ((Graphics2D) g).setStroke(new BasicStroke(getWidth() / 100.0f / 4)); - g.drawString(s, x - fontMetrics.stringWidth(s) / 2, y + fontMetrics.getHeight() / 4); - } - - private void drawEvent(int x, int y, Graphics g) { - double eventWidth = ExecutionGraphVisualizer.this.eventWidth * getWidth() / 100.0f; - double eventHeight = ExecutionGraphVisualizer.this.eventHeight * getHeight() / 100.0f; - g.setColor(Color.WHITE); - ((Graphics2D) g).setStroke(new BasicStroke(Float.min(getWidth() / 100.0f / 2, getHeight() / 100.0f / 2))); - g.fillOval((int) (x - eventWidth / 2), (int) (y - eventHeight / 2), (int) eventWidth, (int) eventHeight); - g.setColor(Color.BLACK); - g.drawOval((int) (x - eventWidth / 2), (int) (y - eventHeight / 2), (int) eventWidth, (int) eventHeight); - } - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCM.java deleted file mode 100644 index 7a25740f02..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCM.java +++ /dev/null @@ -1,60 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import java.util.Collection; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.Map; - -public class MCM { - private final String name; - private final Collection constraints; - private final Map relations; - - public MCM(String name) { - this.name = name; - constraints = new LinkedHashSet<>(); - relations = new LinkedHashMap<>(); - } - - public Collection getConstraints() { - return constraints; - } - - public String getName() { - return name; - } - - public Map getRelations() { - return relations; - } - - public void addConstraint(final MCMConstraint constraint) { - constraints.add(constraint); - constraint.getRelation().collectRelations(relations); - } - - - @Override - public String toString() { - return "MCM{" + - "name='" + name + '\'' + - ", constraints=" + constraints + - '}'; - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMChecker.java deleted file mode 100644 index 3fdc06933b..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMChecker.java +++ /dev/null @@ -1,355 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.analysis.PartialOrd; -import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.algorithm.mcm.cegar.AbstractExecutionGraph; -import hu.bme.mit.theta.analysis.expr.ExprState; -import hu.bme.mit.theta.analysis.expr.StmtAction; -import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.solver.Solver; - -import java.util.*; - -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.analysis.algorithm.mcm.MemoryEvent.MemoryEventType.*; -import static hu.bme.mit.theta.core.stmt.Stmts.Assume; - -public class MCMChecker { - private final MemoryEventProvider memoryEventProvider; - private final MultiprocLTS multiprocLTS; - private final MultiprocInitFunc multiprocInitFunc; - private final MultiprocTransFunc multiprocTransFunc; - private final Collection pids; - private final Collection initialWrites; - private final PartialOrd partialOrd; - private final ExprState globalInitState; - private final Solver solver; - private final MCM mcm; - private final Logger logger; - - public MCMChecker( - final MemoryEventProvider memoryEventProvider, - final MultiprocLTS multiprocLTS, - final MultiprocInitFunc multiprocInitFunc, - final MultiprocTransFunc multiprocTransFunc, - final Collection pids, - final Collection initialWrites, - final PartialOrd partialOrd, - final ExprState globalInitState, - final Solver solver, - final MCM mcm, - final Logger logger) { - this.initialWrites = initialWrites; - this.partialOrd = partialOrd; - this.globalInitState = globalInitState; - checkArgument(pids.stream().noneMatch(i -> i >= 0), "Meta event IDs must be negative!"); - - this.memoryEventProvider = memoryEventProvider; - this.multiprocLTS = multiprocLTS; - this.multiprocInitFunc = multiprocInitFunc; - this.multiprocTransFunc = multiprocTransFunc; - this.pids = pids; - this.solver = solver; - this.mcm = mcm; - this.logger = logger; - } - - public MCMSafetyResult check(final P prec) { - logger.write(Logger.Level.MAINSTEP, "Starting verification\n"); - logger.write(Logger.Level.INFO, "Current precision: " + prec + "\n"); - final Collection> usedVars = prec.getUsedVars(); - logger.write(Logger.Level.INFO, "Variables in precision: " + usedVars + "\n"); - final AbstractExecutionGraph executionGraph = new AbstractExecutionGraph(List.of("RX", "A", "DMB.SY", "thread-end", "meta"), solver, this.mcm, partialOrd); - - final List initialWriteEvents = new ArrayList<>(); - - final List> events = new ArrayList<>(); - final Map eventVarLookup = new LinkedHashMap<>(); - final Collection delayedEvents = new LinkedHashSet<>(); - final Map> delayedReads = new LinkedHashMap<>(); - final Map>>> writes = new LinkedHashMap<>(); - - for (MemoryEvent.Write initialWrite : initialWrites) { - int i = executionGraph.addInitialWrite(initialWrite.varId(), Set.of()); - initialWriteEvents.add(i); - writes.putIfAbsent(initialWrite.varId(), new LinkedHashSet<>()); - writes.get(initialWrite.varId()).add(Tuple2.of(i, globalInitState.toExpr())); - eventVarLookup.put(i, initialWrite.var().getName()); - } - logger.write(Logger.Level.SUBSTEP, "|-- Added initial writes: " + initialWriteEvents.size() + "\n"); - - - final Map> readsMap = new LinkedHashMap<>(); - final Map> eventListMap = new LinkedHashMap<>(); - - - for (final int pid : pids) { - logger.write(Logger.Level.SUBSTEP, "|-- Starting exploration of pid " + pid + "\n"); - final Map reads = new LinkedHashMap<>(); - readsMap.put(pid, reads); - final List eventList = new ArrayList<>(); - eventListMap.put(pid, eventList); - events.add(eventList); - - final Collection initStates = multiprocInitFunc.getInitStates(pid, prec); - - for (final S initState : initStates) { - int id = executionGraph.addInitialState(pid, initState, false); - logger.write(Logger.Level.SUBSTEP, "|------ Adding init state #" + id + "(pid #" + pid + ")\n"); - delayedEvents.add(new DelayedEvent(pid, id, initState)); - } - } - - - while (true) { - Optional delayedEvent = delayedEvents.stream().findAny(); - if (delayedEvent.isEmpty()) break; - delayedEvents.remove(delayedEvent.get()); - - final int lastId = delayedEvent.get().getId(); - final S state = delayedEvent.get().getS(); - final int pid = delayedEvent.get().getPid(); - final Map reads = readsMap.get(pid); - final List eventList = eventListMap.get(pid); - - if (delayedEvent.get() instanceof final DelayedRead delayedRead) { - handleDelayedRead(prec, usedVars, executionGraph, delayedEvents, delayedReads, writes, lastId, state, pid, reads, eventList, delayedRead, eventVarLookup); - } else { - handleEvent(prec, usedVars, executionGraph, delayedEvents, delayedReads, writes, lastId, state, pid, reads, eventList, eventVarLookup); - } - } - - final Collection, LitExpr>> solutions = new ArrayList<>(); - EventConstantLookup rf = executionGraph.encode(); - - logger.write(Logger.Level.SUBSTEP, "|-- Successfully built execution graph\n"); - while (executionGraph.nextSolution(solutions)) { - logger.write(Logger.Level.SUBSTEP, "|-- Found new solution: " + executionGraph.getRf() + "\n"); - } - - logger.write(Logger.Level.RESULT, "Number of executions: " + solutions.size() + "\n"); - logger.write(Logger.Level.MAINSTEP, "Verification ended\n"); - return new MCMSafetyResult(solutions, events, initialWriteEvents, eventVarLookup); - } - - private void handleEvent(P prec, Collection> usedVars, AbstractExecutionGraph executionGraph, Collection delayedEvents, Map> delayedReads, Map>>> writes, int lastId, S state, int pid, Map reads, List eventList, Map eventVarLookup) { - final Collection enabledActionsFor = multiprocLTS.getEnabledActionsFor(pid, state); - for (final A a : enabledActionsFor) { - final List> piecesOf = List.copyOf(memoryEventProvider.getPiecewiseAction(state, a)); - Collection states = new ArrayList<>(List.of(new DelayedEvent(pid, lastId, state))); - Collection nextStates = new ArrayList<>(); - - for (int i = 0; i < piecesOf.size(); i++) { - MemoryEventProvider.ResultElement piece = piecesOf.get(i); - if (exploreActionPiece(prec, usedVars, executionGraph, delayedEvents, delayedReads, writes, pid, reads, eventList, a, states, nextStates, i, piece, i == piecesOf.size() - 1, eventVarLookup)) { - states = nextStates; - break; - } - states = nextStates; - nextStates = new ArrayList<>(); - } - for (DelayedEvent delayedEvent : states) { - if (!executionGraph.tryCover(delayedEvent.getPid(), delayedEvent.getId())) { - delayedEvents.add(delayedEvent); - } - } - } - } - - private void handleDelayedRead(P prec, Collection> usedVars, AbstractExecutionGraph executionGraph, Collection delayedEvents, Map> delayedReads, Map>>> writes, int lastId, S state, int pid, Map reads, List eventList, DelayedRead delayedRead, Map eventVarLookup) { - final A a = delayedRead.getA(); - final int pieceNo = delayedRead.getPieceNo(); - - final List> piecesOf = List.copyOf(memoryEventProvider.getPiecewiseAction(state, a)); - final MemoryEventProvider.ResultElement read = piecesOf.get(pieceNo); - checkState(read.isMemoryEvent() && read.getMemoryEvent().type() == READ, "Delayed read should actually be a read!"); - - int id = executionGraph.addMustRf(pid, delayedRead.getId(), memoryEventProvider.createAction(state, List.of()), state, delayedRead.getReadsFrom()); - eventList.add(id); - logger.write(Logger.Level.INFO, "|------ Adding rf " + delayedRead.getReadsFrom() + " -> " + delayedRead.getId() + "\n"); - - Collection states = new ArrayList<>(List.of(new DelayedEvent(pid, id, state))); - Collection nextStates = new ArrayList<>(); - for (int i = pieceNo + 1; i < piecesOf.size(); i++) { - MemoryEventProvider.ResultElement piece = piecesOf.get(i); - if (exploreActionPiece(prec, usedVars, executionGraph, delayedEvents, delayedReads, writes, pid, reads, eventList, a, states, nextStates, i, piece, i == piecesOf.size() - 1, eventVarLookup)) { - states = nextStates; - break; - } - states = nextStates; - nextStates = new ArrayList<>(); - } - for (DelayedEvent delayedEvent : states) { - if (!executionGraph.tryCover(delayedEvent.getPid(), delayedEvent.getId())) { - delayedEvents.add(delayedEvent); - } - } - } - - private boolean exploreActionPiece(P prec, Collection> usedVars, AbstractExecutionGraph executionGraph, Collection delayedEvents, Map> delayedReads, Map>>> writes, int pid, Map reads, List eventList, A a, Collection states, Collection nextStates, int i, MemoryEventProvider.ResultElement piece, boolean isLastPiece, Map eventVarLookup) { - for (DelayedEvent s : states) { - if (piece.isMemoryEvent()) { - MemoryEvent memoryEvent = piece.getMemoryEvent(); - int nextId = executionGraph.addMemoryEvent(memoryEvent, pid, s.getId()); - logger.write(Logger.Level.SUBSTEP, "|------ Adding memory event #" + nextId + ": " + piece + "\n"); - - if (memoryEvent.type == READ || memoryEvent.type == WRITE) { - MemoryEvent.MemoryIO memoryIO = memoryEvent.asMemoryIO(); - eventVarLookup.put(nextId, memoryIO.var().getName()); - } - - if (memoryEvent.type() == READ) reads.put(memoryEvent.asRead(), nextId); - else if (memoryEvent.type() == WRITE) { - writes.putIfAbsent(memoryEvent.asWrite().varId(), new LinkedHashSet<>()); - writes.get(memoryEvent.asWrite().varId()).add(Tuple2.of(nextId, s.getS().toExpr())); - for (MemoryEvent.Read read : reads.keySet()) { - if (memoryEvent.asWrite().dependencies().contains(read.localVar())) { - executionGraph.addDataDependency(reads.get(read), nextId); - } - } - - for (final DelayedRead delayedRead : delayedReads.getOrDefault(memoryEvent.asWrite().varId(), List.of())) { - for (S succState : multiprocTransFunc.getSuccStates(pid, delayedRead.getS(), memoryEventProvider.createAction(delayedRead.getS(), List.of(Assume(s.getS().toExpr()))), prec)) { - delayedEvents.add(delayedRead.withS(succState).withRf(nextId)); - } - } - } - eventList.add(nextId); - - if (memoryEvent.type() == READ && usedVars.contains(memoryEvent.asRead().var())) { - delayedReads.putIfAbsent(memoryEvent.asRead().varId(), new LinkedHashSet<>()); - DelayedRead delayedRead = new DelayedRead(pid, nextId, a, i, s.getS(), -1); - delayedReads.get(memoryEvent.asRead().varId()).add(delayedRead); - logger.write(Logger.Level.SUBSTEP, "|------ Delaying read #" + nextId + ": " + piece + "\n"); - - for (final Tuple2> write : writes.getOrDefault(memoryEvent.asRead().varId(), List.of())) { - for (S succState : multiprocTransFunc.getSuccStates(pid, s.getS(), memoryEventProvider.createAction(s.getS(), List.of(Assume(write.get2()))), prec)) { - delayedEvents.add(delayedRead.withS(succState).withRf(write.get1())); - } - } - return true; - } else { - nextStates.add(new DelayedEvent(pid, nextId, s.getS())); - } - } else { - final Collection succStates = multiprocTransFunc.getSuccStates(pid, s.getS(), piece.getAction(), prec); - for (final S succState : succStates) { - int id = executionGraph.addState(s.getId(), pid, piece.getAction(), succState, false, isLastPiece); - logger.write(Logger.Level.SUBSTEP, "|------ Adding action #" + id + ": " + piece.getAction() + "\n"); - nextStates.add(new DelayedEvent(pid, id, succState)); - } - } - } - return false; - } - - private class DelayedEvent { - protected final int pid; - protected final int id; - protected final S s; - - public DelayedEvent(int pid, int id, S state) { - this.pid = pid; - this.id = id; - this.s = state; - } - - public int getPid() { - return pid; - } - - public int getId() { - return id; - } - - public S getS() { - return s; - } - } - - private class DelayedRead extends DelayedEvent { - private final A a; - private final int pieceNo; - private final int readsFrom; - - private DelayedRead(int pid, int id, A a, int pieceNo, S s, int readsFrom) { - super(pid, id, s); - this.a = a; - this.pieceNo = pieceNo; - this.readsFrom = readsFrom; - } - - public A getA() { - return a; - } - - public int getPieceNo() { - return pieceNo; - } - - public int getReadsFrom() { - return readsFrom; - } - - public DelayedRead withS(final S s) { - return new DelayedRead(pid, id, a, pieceNo, s, readsFrom); - } - - public DelayedEvent withRf(int write) { - return new DelayedRead(pid, id, a, pieceNo, s, write); - } - } - - public static class MCMSafetyResult { - private final Collection, LitExpr>> solutions; - private final List> events; - private final List initialWriteEvents; - private final Map eventVarLookup; - - public MCMSafetyResult(Collection, LitExpr>> solutions, List> events, List initialWriteEvents, Map eventVarLookup) { - this.solutions = solutions; - this.events = events; - this.initialWriteEvents = initialWriteEvents; - this.eventVarLookup = eventVarLookup; - } - - public Collection, LitExpr>> getSolutions() { - return solutions; - } - - public List> getEvents() { - return events; - } - - public List getInitialWriteEvents() { - return initialWriteEvents; - } - - public void visualize() { - new Thread(new ExecutionGraphVisualizer(solutions, events, eventVarLookup, initialWriteEvents)).start(); - } - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEventProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEventProvider.java deleted file mode 100644 index 80072959a9..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEventProvider.java +++ /dev/null @@ -1,82 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.stmt.Stmt; - -import java.util.Collection; -import java.util.List; -import java.util.Optional; - -import static com.google.common.base.Preconditions.checkNotNull; - -public interface MemoryEventProvider { - - /** - * Gets a piecewise representation of an action, separating memory events from independent parts of the action. - * It is required that the original action's effect stays the same when the piecewise representation is applied. - * - * @param action - * @return - */ - Collection> getPiecewiseAction(S state, A action); - - int getVarId(VarDecl var); - - A createAction(S s, List stmt); - - class ResultElement { - private final Optional memoryEvent; - private final Optional action; - - public ResultElement(final MemoryEvent memoryEvent) { - this.memoryEvent = Optional.of(checkNotNull(memoryEvent)); - this.action = Optional.empty(); - } - - public ResultElement(final A action) { - this.memoryEvent = Optional.empty(); - this.action = Optional.of(checkNotNull(action)); - } - - public MemoryEvent getMemoryEvent() { - return memoryEvent.orElseThrow(); - } - - public A getAction() { - return action.orElseThrow(); - } - - public boolean isMemoryEvent() { - return memoryEvent.isPresent(); - } - - public boolean isAction() { - return action.isPresent(); - } - - @Override - public String toString() { - if (memoryEvent.isPresent()) return memoryEvent.get().toString(); - else return action.toString(); - } - } - -} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocInitFunc.java deleted file mode 100644 index f548005f03..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocInitFunc.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.analysis.InitFunc; -import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; - -import java.util.Collection; -import java.util.Map; - -public class MultiprocInitFunc { - private final Map> initFuncMap; - - public MultiprocInitFunc(final Map> initFuncMap) { - this.initFuncMap = initFuncMap; - } - - public Collection getInitStates(final int pid, final P prec) { - if (initFuncMap.containsKey(pid)) return initFuncMap.get(pid).getInitStates(prec); - else - throw new RuntimeException("No such process: " + pid + ". Known processes: " + initFuncMap.keySet()); - } - -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocLTS.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocLTS.java deleted file mode 100644 index 51ca84faee..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocLTS.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.State; - -import java.util.Collection; -import java.util.Map; - -public class MultiprocLTS { - private final Map> ltsMap; - - public MultiprocLTS(final Map> ltsMap) { - this.ltsMap = ltsMap; - } - - public Collection getEnabledActionsFor(final int pid, S state) { - if (ltsMap.containsKey(pid)) return ltsMap.get(pid).getEnabledActionsFor(state); - else - throw new RuntimeException("No such process: " + pid + ". Known processes: " + ltsMap.keySet()); - } - -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocTransFunc.java deleted file mode 100644 index 417590a142..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MultiprocTransFunc.java +++ /dev/null @@ -1,37 +0,0 @@ -/* - * Copyright 2023 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.mcm; - -import hu.bme.mit.theta.analysis.*; - -import java.util.Collection; -import java.util.Map; - -public class MultiprocTransFunc { - private final Map> transFuncMap; - - public MultiprocTransFunc(final Map> transFuncMap) { - this.transFuncMap = transFuncMap; - } - - public Collection getSuccStates(final int pid, final S state, final A action, final P prec) { - if (transFuncMap.containsKey(pid)) - return transFuncMap.get(pid).getSuccStates(state, action, prec); - else - throw new RuntimeException("No such process: " + pid + ". Known processes: " + transFuncMap.keySet()); - } - -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/ExecutionGraph.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/ExecutionGraph.kt new file mode 100644 index 0000000000..07a97172b4 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/ExecutionGraph.kt @@ -0,0 +1,101 @@ +/* + * Copyright 2023 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.mcm.analysis + +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCM +import hu.bme.mit.theta.common.TupleN +import hu.bme.mit.theta.core.model.MutableValuation +import hu.bme.mit.theta.core.model.Valuation +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.BoolExprs.And +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.SolverStatus + +class ExecutionGraph { + + private val events = ArrayList() + private val relations = LinkedHashMap>, TVL>() + + fun addEvent(event: Int) { + events.add(event) + } + + fun getEvents(): List = events + + operator fun set(name: String, tuple: TupleN, value: TVL) { + relations[Pair(name, tuple)] = value + } + + operator fun get(name: String, tuple: TupleN): TVL? { + return relations[Pair(name, tuple)] + } + + fun toExpr(mcm: MCM): Expr { + val expressionCollector = object : Solver { + private val expressions = ArrayList>() + override fun close() = Unit + override fun check(): SolverStatus = error("Unsupported") + override fun push() = Unit + override fun pop(n: Int) = Unit + override fun reset() = expressions.clear() + override fun getStatus(): SolverStatus = error("Unsupported") + override fun getModel(): Valuation = error("Unsupported") + override fun getAssertions(): MutableCollection> = expressions + override fun add(assertion: Expr) { + expressions.add(assertion) + } + } + val encodedRelationWrapper = EncodedRelationWrapper(expressionCollector) + val valuation = MutableValuation() + + mcm.constraints.forEach { + it.encodeEvents(events, encodedRelationWrapper) + } + + for (relation in mcm.relations) { + val eventSet = encodedRelationWrapper[relation.key] + val recordValue = { tuple: TupleN -> + val valueToEncode = relations.getOrDefault(Pair(relation.key, tuple), TVL.UNKNOWN) + if (valueToEncode != TVL.UNKNOWN) + valuation.put(eventSet[tuple], BoolExprs.Bool(valueToEncode == TVL.TRUE)) + } + for (event1 in events) { + if (relation.value.arity == 1) { + val tuple = TupleN.of(event1) + recordValue(tuple) + } else { + for (event2 in events) { + val tuple = TupleN.of(event1, event2) + recordValue(tuple) + } + } + } + } + + expressionCollector.add(valuation.toExpr()) + return And(expressionCollector.assertions) + } +} + +enum class TVL { + FALSE, + UNKNOWN, + TRUE +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt new file mode 100644 index 0000000000..76cde6ac78 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt @@ -0,0 +1,81 @@ +/* + * Copyright 2023 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.mcm.analysis + +import hu.bme.mit.theta.analysis.InitFunc +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.TransFunc +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.mcm.interpreter.MemoryEventProvider +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.common.Tuple1 +import hu.bme.mit.theta.common.Tuple2 +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint +import hu.bme.mit.theta.graphsolver.solvers.GraphSolver +import java.util.* + +class FiniteStateChecker( + private val mcm: Collection, + private val initFunc: InitFunc, + private val actionFunc: LTS, + private val transFunc: TransFunc, + private val memoryEventProvider: MemoryEventProvider, + private val graphPatternCompiler: GraphPatternCompiler, + private val graphPatternSolver: GraphSolver +) : SafetyChecker { + + override fun check(prec: ExplPrec): SafetyResult { + val eventIds = LinkedList() + val rels = LinkedList>() + val lastIds = LinkedHashMap() + val initId = nextId(eventIds) + val initStates = LinkedList(initFunc.getInitStates(prec)) + initStates.forEach { lastIds[it] = initId } + while (initStates.isNotEmpty()) { + val state = initStates.pop() + val lastId = checkNotNull(lastIds[state]) + val actions = actionFunc.getEnabledActionsFor(state) + + val nextStates = actions.map { a -> + val memEvent = memoryEventProvider[a, prec] + transFunc.getSuccStates(state, a, prec).onEach { s -> + memEvent?.also { + val id = nextId(eventIds) + rels.add(Pair(memEvent.type().label, Tuple1.of(id))) + rels.add(Pair("po", Tuple2.of(lastId, id))) + lastIds[s] = id + } + } + }.flatten() + initStates.addAll(nextStates) + } +// PartialSolver(mcm, CandidateExecutionGraph(eventIds, rels)) + return SafetyResult.unsafe(null, null) + + } + + private fun nextId(list: MutableList): Int { + val ret = list.size + list.add(list.size) + return ret + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/PartialSolver.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/PartialSolver.kt new file mode 100644 index 0000000000..0ac91921ff --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/PartialSolver.kt @@ -0,0 +1,55 @@ +/* + * Copyright 2023 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.mcm.analysis + +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.graphsolver.ThreeVL +import hu.bme.mit.theta.graphsolver.collectSubRelations +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint +import hu.bme.mit.theta.graphsolver.solvers.GraphSolver + +class PartialSolver( + private val mcm: Collection, + private val partialGraph: CandidateExecutionGraph, + private val graphPatternCompiler: GraphPatternCompiler, + private val graphPatternSolver: GraphSolver +) { + + fun getSolution(): CandidateExecutionGraph? { + graphPatternCompiler.addEvents(partialGraph.nodes) + graphPatternCompiler.addFacts(partialGraph.knownEvents) + + val exprs = mcm.map { it.accept(graphPatternCompiler) } + exprs.forEach { graphPatternSolver.add(it) } + + val namedPatterns = mcm.map { it.collectSubRelations() }.flatten().toSet() + + val status = graphPatternSolver.check() + + return if (status.isSat) { + val (nodes, events) = graphPatternCompiler.getCompleteGraph(namedPatterns, graphPatternSolver.getModel()) + CandidateExecutionGraph(nodes, events) + } else null + } + +} + +data class CandidateExecutionGraph( + val nodes: List, + val knownEvents: Map, ThreeVL>) { +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/AbstractExecutionGraph.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/AbstractExecutionGraph.java deleted file mode 100644 index 086650069f..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/AbstractExecutionGraph.java +++ /dev/null @@ -1,658 +0,0 @@ -/* - * Copyright 2023 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.mcm.cegar; - -import com.google.common.collect.Sets; -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.PartialOrd; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.algorithm.ARG; -import hu.bme.mit.theta.analysis.algorithm.ArgEdge; -import hu.bme.mit.theta.analysis.algorithm.ArgNode; -import hu.bme.mit.theta.analysis.algorithm.mcm.*; -import hu.bme.mit.theta.analysis.expr.StmtAction; -import hu.bme.mit.theta.analysis.utils.ArgVisualizer; -import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.common.Tuple3; -import hu.bme.mit.theta.common.TupleN; -import hu.bme.mit.theta.common.datalog.Datalog; -import hu.bme.mit.theta.common.datalog.DatalogArgument; -import hu.bme.mit.theta.common.datalog.GenericDatalogArgument; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -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.Solver; -import hu.bme.mit.theta.solver.SolverManager; -import hu.bme.mit.theta.solver.UCSolver; -import tools.refinery.store.map.Cursor; -import tools.refinery.store.model.Model; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.model.ModelStoreImpl; -import tools.refinery.store.model.Tuple; -import tools.refinery.store.model.representation.DataRepresentation; -import tools.refinery.store.model.representation.Relation; -import tools.refinery.store.model.representation.TruthValue; - -import java.util.*; -import java.util.stream.Collectors; - -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.core.decl.Decls.Const; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; - -public class AbstractExecutionGraph { - private final Map> preDefinedRelations = Map.ofEntries( - Map.entry("emptyset", new Relation<>("emptyset", 1, TruthValue.FALSE)), - Map.entry("W", new Relation<>("W", 1, TruthValue.FALSE)), - Map.entry("R", new Relation<>("R", 1, TruthValue.FALSE)), - Map.entry("M", new Relation<>("M", 1, TruthValue.FALSE)), - Map.entry("IW", new Relation<>("IW", 1, TruthValue.FALSE)), - Map.entry("FW", new Relation<>("FW", 1, TruthValue.FALSE)), - Map.entry("B", new Relation<>("B", 1, TruthValue.FALSE)), - Map.entry("RMW", new Relation<>("RMW", 1, TruthValue.FALSE)), - Map.entry("F", new Relation<>("F", 1, TruthValue.FALSE)), - - Map.entry("U", new Relation<>("U", 1, TruthValue.FALSE)), - Map.entry("T", new Relation<>("T", 1, TruthValue.UNKNOWN)), - - Map.entry("po", new Relation<>("po", 2, TruthValue.FALSE)), - Map.entry("po-raw", new Relation<>("po-raw", 2, TruthValue.FALSE)), - Map.entry("addr", new Relation<>("addr", 2, TruthValue.FALSE)), - Map.entry("data", new Relation<>("data", 2, TruthValue.FALSE)), - Map.entry("ctrl", new Relation<>("ctrl", 2, TruthValue.FALSE)), - Map.entry("rmw", new Relation<>("rmw", 2, TruthValue.FALSE)), - Map.entry("amo", new Relation<>("amo", 2, TruthValue.FALSE)), - - Map.entry("id", new Relation<>("id", 2, TruthValue.FALSE)), - Map.entry("loc-raw", new Relation<>("loc-raw", 2, TruthValue.FALSE)), - Map.entry("loc", new Relation<>("loc", 2, TruthValue.FALSE)), -// Map.entry("ext", new Relation<>("ext", 2, TruthValue.FALSE)), - Map.entry("int-raw", new Relation<>("int-raw", 2, TruthValue.FALSE)), - Map.entry("int", new Relation<>("int", 2, TruthValue.FALSE)), - - Map.entry("rf", new Relation<>("rf", 2, TruthValue.UNKNOWN)), - Map.entry("co", new Relation<>("co", 2, TruthValue.UNKNOWN)) - ); - private final Map> tags; - private final MCM mcm; - private final ModelStore modelStore; - private Model currentModel; - private final EncodedRelationWrapper encodedRelationWrapper; - private int lastCnt = 1; - private final Map>> threadArgs; - private final Map>> argNodeLookup; - private final PartialOrd partialOrd; - private final Map lastMemEventLookup; - private final Map memoryEventLookup; - private final Collection> fixedRf; - private final Map>>> potentialCoveringNodes; - - public AbstractExecutionGraph(final Collection tags, final Solver solver, final MCM mcm, final PartialOrd partialOrd) { - this.mcm = mcm; - this.partialOrd = partialOrd; - this.tags = new LinkedHashMap<>(); - tags.forEach(t -> this.tags.put(t, new Relation<>(t, 1, TruthValue.FALSE))); - modelStore = new ModelStoreImpl(Sets.union(Set.copyOf(this.tags.values()), Set.copyOf(preDefinedRelations.values()))); - currentModel = modelStore.createModel(); - encodedRelationWrapper = new EncodedRelationWrapper(solver); - threadArgs = new LinkedHashMap<>(); - argNodeLookup = new LinkedHashMap<>(); - lastMemEventLookup = new LinkedHashMap<>(); - memoryEventLookup = new LinkedHashMap<>(); - fixedRf = new LinkedHashSet<>(); - potentialCoveringNodes = new LinkedHashMap<>(); - } - - // Encoder method - - public EventConstantLookup encode() { - updateCalculatedRelations(); // this won't be necessary when Refinery will support derivation rules - - final List idList = getMustValues(rel("U")).stream().map(this::unbox).collect(Collectors.toList()); - - for (final MCMConstraint constraint : mcm.getConstraints()) { - constraint.encodeEvents(idList, encodedRelationWrapper); - } - Solver solver = encodedRelationWrapper.getSolver(); - - final Collection> binaryRelations = preDefinedRelations.values().stream().filter(r -> r.getArity() == 2).toList(); - final Collection> unaryRelations = Sets.union(Set.copyOf(tags.values()), preDefinedRelations.values().stream().filter(r -> r.getArity() == 1).collect(Collectors.toSet())); - - for (final int i : idList) { - for (final Relation unaryRelation : unaryRelations) { - TruthValue truthValue = currentModel.get(unaryRelation, Tuple.of(i)); - if (truthValue.must()) { - solver.add(getOrCreate(encodedRelationWrapper, idList, unaryRelation.getName(), true).get(TupleN.of(i)).getRef()); - } else if (!truthValue.may()) { - solver.add(Not(getOrCreate(encodedRelationWrapper, idList, unaryRelation.getName(), true).get(TupleN.of(i)).getRef())); - } - } - for (final int j : idList) { - for (final Relation binaryRelation : binaryRelations) { - TruthValue truthValue = currentModel.get(binaryRelation, Tuple.of(i, j)); - if (truthValue.must()) { - solver.add(getOrCreate(encodedRelationWrapper, idList, binaryRelation.getName(), false).get(TupleN.of(i, j)).getRef()); - } else if (!truthValue.may()) { - solver.add(Not(getOrCreate(encodedRelationWrapper, idList, binaryRelation.getName(), false).get(TupleN.of(i, j)).getRef())); - } - } - } - } - - // special encoding is necessary to ensure a maximal set of events are in-trace: - EventConstantLookup t = getOrCreate(encodedRelationWrapper, idList, "T", true); - for (final int i : idList) { - List> partitions = new ArrayList<>(); - if (currentModel.get(rel("IW"), Tuple.of(i)).must()) - solver.add(t.get(TupleN.of(i)).getRef()); - - for (final int j : idList) { - if (currentModel.get(rel("po-raw"), Tuple.of(i, j)).must()) { - boolean found = false; - for (List partition : partitions) { - if (currentModel.get(rel("int"), Tuple.of(partition.get(0), j)).must()) { - found = true; - partition.add(j); - break; - } - } - if (!found) { - List list = new ArrayList<>(); - list.add(j); - partitions.add(list); - } - } - } - for (List partition : partitions) { - solver.add(Imply(t.get(TupleN.of(i)).getRef(), Or(partition.stream().map(j -> t.get(TupleN.of(j)).getRef()).collect(Collectors.toList())))); - for (final int j : partition) { - solver.add(Imply(t.get(TupleN.of(j)).getRef(), t.get(TupleN.of(i)).getRef())); - solver.add(Imply(t.get(TupleN.of(j)).getRef(), Not(Or(partition.stream().filter(k -> k != j).map(k -> t.get(TupleN.of(k)).getRef()).collect(Collectors.toList()))))); - } - } - } - final EventConstantLookup rf = getOrCreate(encodedRelationWrapper, idList, "rf", false); - - final Map> writeVarIndexingMap = new LinkedHashMap<>(); - final Map> readVarIndexingMap = new LinkedHashMap<>(); - - - threadArgs.forEach((pid, arg) -> { - encodeArg(solver, t, writeVarIndexingMap, readVarIndexingMap, arg); - }); - - for (Tuple3 tuple : fixedRf) { -// final ArgEdge> inEdge = argNodeLookup.get(tuple.get1()).getInEdge().get(); -// final Expr inTrace = Or(collectImmediateSuccessors(inEdge).stream().map(i -> t.get(TupleN.of(i)).getRef()).toList()); - final Expr inTrace = t.get(TupleN.of(tuple.get1())).getRef(); - final Expr fixedRf = rf.get(TupleN.of(tuple.get2(), tuple.get3())).getRef(); - solver.add(Imply(inTrace, fixedRf)); - } - - writeVarIndexingMap.forEach((i, writeConst) -> readVarIndexingMap.forEach((j, readConst) -> - solver.add(Imply(rf.get(TupleN.of(i, j)).getRef(), Eq(writeConst, readConst))))); - - - printUC(solver); - - - return rf; - } - - Long commit = null; - - public boolean nextSolution(Collection, LitExpr>> solutions) { - if (commit != null) currentModel = modelStore.createModel(commit); - else commit = currentModel.commit(); - if (encodedRelationWrapper.getSolver().check().isSat()) { - solutions.add(Map.copyOf(encodedRelationWrapper.getSolver().getModel().toMap())); - final EventConstantLookup rf = encodedRelationWrapper.getEventLookup("rf"); - - final Map, LitExpr> lut = encodedRelationWrapper.getSolver().getModel().toMap(); - final List> subexprs = new ArrayList<>(); - - rf.getAll().forEach((tuple, constDecl) -> { - if (lut.get(constDecl).equals(True())) { - subexprs.add(constDecl.getRef()); - setTrue("rf", tuple.get(0), tuple.get(1)); - } else subexprs.add(Not(constDecl.getRef())); - }); - - - encodedRelationWrapper.getSolver().add(Not(And(subexprs))); - - return true; - } - return false; - } - - public Collection getRf() { - return getMustValues(rel("rf")); - } - - // Builder methods - - - public boolean tryCover(int pid, int id) { - checkState(threadArgs.containsKey(pid)); - final ArgNode> node = argNodeLookup.get(id); - final Optional>> covering = potentialCoveringNodes.get(pid).stream().filter(argNode -> argNode.mayCover(node)).findFirst(); - if (covering.isEmpty()) return false; - else { - node.cover(covering.get()); - return true; - } - } - - public void addDataDependency(final int i, final int j) { - setTrue("data", i, j); - } - - - public int addMustRf(int pid, int read, A action, S state, int readsFrom) { - int i = addMemoryEvent(new MemoryEvent(MemoryEvent.MemoryEventType.META, "meta"), pid, read, state); - fixedRf.add(Tuple3.of(i, readsFrom, read)); - return i; - } - - public int addMemoryEvent(final MemoryEvent memoryEvent, final int pid, final int lastId) { - final ArgNode> lastArgNode = argNodeLookup.get(lastId); - return addMemoryEvent(memoryEvent, pid, lastId, lastArgNode.getState()); - } - - public int addMemoryEvent(final MemoryEvent memoryEvent, final int pid, final int lastId, final S nextState) { - checkState(threadArgs.containsKey(pid)); - final int actualLastId = getActualLastId(lastId); - int id = switch (memoryEvent.type()) { - case READ -> - addRead(pid, memoryEvent.asRead().varId(), actualLastId, Set.of(memoryEvent.tag())); - case WRITE -> - addWrite(pid, memoryEvent.asWrite().varId(), actualLastId, Set.of(memoryEvent.tag())); - case FENCE -> addFence(pid, actualLastId, Set.of(memoryEvent.tag())); - case META -> addNormalEvent(pid, actualLastId, Set.of(memoryEvent.tag())); - }; - final ArgNode> lastArgNode = argNodeLookup.get(lastId); - final ArgNode> succNode = threadArgs.get(pid).createSuccNode(lastArgNode, new ActionUnion.MemoryEventAction<>(memoryEvent, id), nextState, false); - argNodeLookup.put(id, succNode); - memoryEventLookup.put(id, memoryEvent); - return id; - } - - private int getActualLastId(int lastId) { - if (lastMemEventLookup.containsKey(lastId)) { - return getActualLastId(lastMemEventLookup.get(lastId)); - } else return lastId; - } - - private int addWrite(final int processId, final int varId, final int lastNode, final Collection tags) { - check(processId, varId, lastNode, tags); - final int id = addMemoryEvent(processId, varId, lastNode, tags); - setTrue("W", id); - return id; - } - - private int addRead(final int processId, final int varId, final int lastNode, final Collection tags) { - check(processId, varId, lastNode, tags); - final int id = addMemoryEvent(processId, varId, lastNode, tags); - setTrue("R", id); - return id; - } - - private int addFence(final int processId, final int lastNode, final Collection tags) { - check(processId, -1, lastNode, tags); - final int id = addNormalEvent(processId, lastNode, tags); - setTrue("F", id); - return id; - } - - public int addInitialWrite(final int varId, final Collection tags) { - check(-1, varId, 0, tags); - final int id = addAnyEvent(tags); - setTrue("W", id); - setTrue("IW", id); - setTrue("M", id); - setTrue("loc-raw", varId, id); - return id; - } - - public int addInitialState(final int pid, final S state, final boolean target) { - if (!threadArgs.containsKey(pid)) { - threadArgs.put(pid, ARG.create(partialOrd)); - } - final int id = lastCnt++; - lastMemEventLookup.put(id, 0); - ArgNode> initNode = threadArgs.get(pid).createInitNode(state, target); - argNodeLookup.put(id, initNode); - return id; - } - - public int addState(final int lastNode, final int pid, final A action, final S state, final boolean target, final boolean isLastPiece) { - checkState(threadArgs.containsKey(pid)); - final int id = lastCnt++; - lastMemEventLookup.put(id, lastNode); - ArgNode> succNode = threadArgs.get(pid).createSuccNode(argNodeLookup.get(lastNode), new ActionUnion.ActionWrapper<>(action), state, target); - if (isLastPiece) { - potentialCoveringNodes.putIfAbsent(pid, new LinkedHashSet<>()); - potentialCoveringNodes.get(pid).add(succNode); - } - argNodeLookup.put(id, succNode); - return id; - } - // support methods for builders - - private int addMemoryEvent(int processId, int varId, int lastNode, Collection tags) { - final int id = addNormalEvent(processId, lastNode, tags); - setTrue("M", id); - setTrue("loc-raw", varId, id); - return id; - } - - private int addNormalEvent(int processId, int lastNode, Collection tags) { - final int id = addAnyEvent(tags); - if (lastNode == 0) { - for (final Tuple iw : getMustValues(rel("IW"))) { - setTrue("po-raw", unbox(iw), id); - } - } else { - setTrue("po-raw", lastNode, id); - } - setTrue("int-raw", processId, id); - return id; - } - - private int addAnyEvent(Collection tags) { - final int id = lastCnt++; - setTrue("id", id, id); - setTrue("U", id); - tags.forEach(s -> setTrue(s, id)); - return id; - } - - // HELPER METHODS - - public Relation rel(final String s) { - if (tags.containsKey(s)) return tags.get(s); - return preDefinedRelations.get(s); - } - - public void setTrue(final String s, final int... i) { - final Tuple t = Tuple.of(i); - currentModel.put(rel(s), t, TruthValue.TRUE); - } - - private Collection getMustValues(final DataRepresentation rel) { - final Cursor cursor = currentModel.getAll(rel); - cursor.move(); - final Collection ret = new LinkedHashSet<>(); - while (!cursor.isTerminated()) { - if (cursor.getValue().must()) ret.add(cursor.getKey()); - cursor.move(); - } - return ret; - } - - private int unbox(final Tuple unaryTuple) { - checkArgument(unaryTuple.getSize() == 1); - return unaryTuple.get(0); - } - - - private void check(int processId, int varId, int lastNode, Collection tags) { - checkArgument(processId < 0, "Meta IDs should be negative!"); - checkArgument(varId < 0, "Meta IDs should be negative!"); - checkArgument(lastNode >= 0, "Only meta IDs should be negative!"); - checkArgument(tags.stream().allMatch(this.tags::containsKey), "All tags should have been initialized!"); - } - - private EventConstantLookup getOrCreate( - final EncodedRelationWrapper encodedRelationWrapper, - final List idList, - final String name, - final boolean isUnary) { - EventConstantLookup lookup = encodedRelationWrapper.getEventLookup(name); - if (lookup == null) { - lookup = createDummyRelation(idList, name, isUnary); - encodedRelationWrapper.addEvent(name, lookup); - } - return lookup; - } - - private EventConstantLookup createDummyRelation(List idList, String name, boolean isUnary) { - EventConstantLookup eventConstantLookup = new EventConstantLookup(); - for (final int i : idList) { - if (isUnary) { - eventConstantLookup.add(TupleN.of(i), Const(name + "_" + i, Bool())); - } else { - for (final int j : idList) { - eventConstantLookup.add(TupleN.of(i, j), Const(name + "_" + i + "_" + j, Bool())); - } - } - } - return eventConstantLookup; - } - - - private void updateCalculatedRelations() { - final Collection poRawValues = getMustValues(rel("po-raw")); - final Relation po = rel("po"); - - final Collection intRawValues = getMustValues(rel("int-raw")); - final Relation _int = rel("int"); - - final Collection locRawValues = getMustValues(rel("loc-raw")); - final Relation loc = rel("loc"); - - final Datalog program = Datalog.createProgram(); - final Datalog.Relation poRaw = program.createRelation("po-raw", 2); - final Datalog.Relation intRaw = program.createRelation("int-raw", 2); - final Datalog.Relation locRaw = program.createRelation("loc-raw", 2); - final Datalog.Relation poRel = program.createTransitive("po", poRaw); - final Datalog.Relation intRel = program.createCommonSource("int", intRaw); - final Datalog.Relation locRel = program.createCommonSource("loc", locRaw); - - poRawValues.forEach(v -> poRaw.addFact(tup(v))); - intRawValues.forEach(v -> intRaw.addFact(tup(v))); - locRawValues.forEach(v -> locRaw.addFact(tup(v))); - - poRel.getElements().forEach(t -> currentModel.put(po, tup(t), TruthValue.TRUE)); - intRel.getElements().forEach(t -> currentModel.put(_int, tup(t), TruthValue.TRUE)); - locRel.getElements().forEach(t -> currentModel.put(loc, tup(t), TruthValue.TRUE)); - } - - private Tuple tup(TupleN t) { - if (t.arity() == 1) - return Tuple.of(((GenericDatalogArgument) t.get(0)).getContent()); - if (t.arity() == 2) - return Tuple.of(((GenericDatalogArgument) t.get(0)).getContent(), ((GenericDatalogArgument) t.get(1)).getContent()); - throw new UnsupportedOperationException("Relations with higher arities not supported"); - } - - private Tuple itup(TupleN t) { - if (t.arity() == 1) return Tuple.of(t.get(0)); - if (t.arity() == 2) return Tuple.of(t.get(0), t.get(1)); - throw new UnsupportedOperationException("Relations with higher arities not supported"); - } - - private TupleN tup(Tuple t) { - if (t.getSize() == 1) return TupleN.of(GenericDatalogArgument.createArgument(t.get(0))); - if (t.getSize() == 2) - return TupleN.of(GenericDatalogArgument.createArgument(t.get(0)), GenericDatalogArgument.createArgument(t.get(1))); - throw new UnsupportedOperationException("Relations with higher arities not supported"); - } - - private void printUC(Solver solver) { - if (solver.check().isUnsat()) { - try (final UCSolver ucSolver = SolverManager.resolveSolverFactory("Z3").createUCSolver()) { - ucSolver.track(solver.getAssertions()); - ucSolver.check(); - for (Expr boolTypeExpr : ucSolver.getUnsatCore()) { - System.err.println(boolTypeExpr); - } - } catch (Exception e) { - throw new RuntimeException(e); - } - } - } - - private void encodeArg(Solver solver, EventConstantLookup t, Map> writeVarIndexingMap, Map> readVarIndexingMap, ARG> arg) { - final Collection>, VarIndexing>> waitSet = new LinkedHashSet<>(); - arg.getInitNodes().forEach(node -> waitSet.add(Tuple2.of(node, VarIndexingFactory.indexing(0)))); - VarIndexing lhsIndexing = VarIndexingFactory.indexing(0); - while (!waitSet.isEmpty()) { - final Tuple2>, VarIndexing> nextElement = waitSet.stream().findAny().get(); - waitSet.remove(nextElement); - final ArgNode> node = nextElement.get1(); - final VarIndexing rhsIndexing = nextElement.get2(); - - for (ArgEdge> argEdge : node.getOutEdges().toList()) { - final ActionUnion actionOrMemEvent = argEdge.getAction(); - if (actionOrMemEvent.isMemoryEvent()) { - VarIndexing localIndexing = rhsIndexing; - MemoryEvent memoryEvent = actionOrMemEvent.asMemoryEventAction().getMemoryEvent(); - switch (memoryEvent.type()) { - case READ -> { - lhsIndexing = lhsIndexing.inc(memoryEvent.asRead().localVar()); - localIndexing = localIndexing.inc(memoryEvent.asRead().localVar(), lhsIndexing.get(memoryEvent.asRead().localVar()) - localIndexing.get(memoryEvent.asRead().localVar())); - readVarIndexingMap.put(actionOrMemEvent.asMemoryEventAction().getId(), PathUtils.unfold(memoryEvent.asRead().localVar().getRef(), localIndexing)); - } - case WRITE -> - writeVarIndexingMap.put(actionOrMemEvent.asMemoryEventAction().getId(), PathUtils.unfold(memoryEvent.asWrite().localVar().getRef(), localIndexing)); - default -> { - } - } - waitSet.add(Tuple2.of(argEdge.getTarget(), localIndexing)); - } - if (!actionOrMemEvent.isMemoryEvent()) { - final A action = actionOrMemEvent.asActionWrapper().getAction(); - VarIndexing localIndexing = rhsIndexing; - for (Stmt stmt : action.getStmts()) { - Tuple3>, VarIndexing, VarIndexing> unfoldResult = StmtTreeUnfolder.unfold(stmt, lhsIndexing, localIndexing); - Expr base = Or(collectImmediateSuccessors(argEdge).stream().map(i -> t.get(TupleN.of(i)).getRef()).toList()); - solver.add(Imply(base, And(unfoldResult.get1()))); - lhsIndexing = unfoldResult.get2(); - localIndexing = unfoldResult.get3(); - } - waitSet.add(Tuple2.of(argEdge.getTarget(), localIndexing)); - } - } - } - } - - private Set collectImmediateSuccessors(final ArgEdge> edge) { - if (edge.getAction().isMemoryEvent) { - return Set.of(edge.getAction().asMemoryEventAction().getId()); - } else { - final Set ret = new LinkedHashSet<>(); - for (ArgEdge> outEdge : edge.getTarget().getOutEdges().toList()) { - ret.addAll(collectImmediateSuccessors(outEdge)); - } - return ret; - } - } - - private static abstract class ActionUnion implements Action { - private final boolean isMemoryEvent; - - protected ActionWrapper asActionWrapper() { - throw new ClassCastException("Cannot be cast to ActionWrapper"); - } - - protected MemoryEventAction asMemoryEventAction() { - throw new ClassCastException("Cannot be cast to MemoryEventAction"); - } - - protected ActionUnion(boolean isMemoryEvent) { - this.isMemoryEvent = isMemoryEvent; - } - - public boolean isMemoryEvent() { - return isMemoryEvent; - } - - private static final class MemoryEventAction extends ActionUnion { - private final MemoryEvent memoryEvent; - private final int id; - - private MemoryEventAction(MemoryEvent memoryEvent, int id) { - super(true); - this.memoryEvent = memoryEvent; - this.id = id; - } - - public MemoryEvent getMemoryEvent() { - return memoryEvent; - } - - @Override - protected MemoryEventAction asMemoryEventAction() { - return this; - } - - public int getId() { - return id; - } - - @Override - public String toString() { - return "MemoryEventAction{" + - "memoryEvent=" + memoryEvent + - ", id=" + id + - '}'; - } - } - - private static final class ActionWrapper extends ActionUnion { - private final A action; - - private ActionWrapper(A action) { - super(false); - this.action = action; - } - - public A getAction() { - return action; - } - - @Override - protected ActionWrapper asActionWrapper() { - return this; - } - - @Override - public String toString() { - return "ActionWrapper{" + - "action=" + action + - '}'; - } - } - } - - public String toDot(int pid) { - ARG> arg = threadArgs.get(pid); - Graph g = ArgVisualizer.getDefault().visualize(arg); - return GraphvizWriter.getInstance().writeString(g); - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/StmtTreeUnfolder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/StmtTreeUnfolder.java deleted file mode 100644 index 93d9b09710..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/StmtTreeUnfolder.java +++ /dev/null @@ -1,110 +0,0 @@ -/* - * Copyright 2023 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.mcm.cegar; - -import hu.bme.mit.theta.common.Tuple3; -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.booltype.BoolType; -import hu.bme.mit.theta.core.utils.PathUtils; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; - -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; - -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; - -public class StmtTreeUnfolder { - public static Tuple3>, VarIndexing, VarIndexing> unfold(final Stmt stmt, final VarIndexing lhs, final VarIndexing rhs) { - Visitor visitor = new Visitor(lhs, rhs); - return Tuple3.of(stmt.accept(visitor, rhs), visitor.getLhsIndexing(), visitor.getRhsIndexing()); - } - - private static class Visitor implements StmtVisitor>> { - private VarIndexing lhsIndexing; - private VarIndexing rhsIndexing; - - public Visitor(final VarIndexing lhsIndexing, final VarIndexing rhsIndexing) { - this.lhsIndexing = lhsIndexing; - this.rhsIndexing = rhsIndexing; - } - - @Override - public Collection> visit(SkipStmt stmt, VarIndexing rhsIndexing) { - return List.of(); - } - - @Override - public Collection> visit(AssumeStmt stmt, VarIndexing rhsIndexing) { - return List.of(PathUtils.unfold(stmt.getCond(), rhsIndexing)); - } - - @Override - public Collection> visit(AssignStmt stmt, VarIndexing rhsIndexing) { - lhsIndexing = lhsIndexing.inc(stmt.getVarDecl()); - List> eq = List.of(Eq(stmt.getVarDecl().getConstDecl(lhsIndexing.get(stmt.getVarDecl())).getRef(), PathUtils.unfold(stmt.getExpr(), rhsIndexing))); - this.rhsIndexing = rhsIndexing.inc(stmt.getVarDecl(), lhsIndexing.get(stmt.getVarDecl()) - rhsIndexing.get(stmt.getVarDecl())); - return eq; - } - - @Override - public Collection> visit(HavocStmt stmt, VarIndexing rhsIndexing) { - lhsIndexing = lhsIndexing.inc(stmt.getVarDecl()); - this.rhsIndexing = rhsIndexing.inc(stmt.getVarDecl(), lhsIndexing.get(stmt.getVarDecl()) - rhsIndexing.get(stmt.getVarDecl())); - return List.of(); - } - - @Override - public Collection> visit(SequenceStmt stmt, VarIndexing rhsIndexing) { - Collection> ret = new ArrayList<>(); - for (Stmt stmtStmt : stmt.getStmts()) { - ret.addAll(stmtStmt.accept(this, rhsIndexing)); - } - return ret; - } - - @Override - public Collection> visit(NonDetStmt stmt, VarIndexing rhsIndexing) { - throw new UnsupportedOperationException("Not yet implemented"); - } - - @Override - public Collection> visit(OrtStmt stmt, VarIndexing rhsIndexing) { - throw new UnsupportedOperationException("Not yet implemented"); - } - - @Override - public Collection> visit(LoopStmt stmt, VarIndexing rhsIndexing) { - throw new UnsupportedOperationException("Not yet implemented"); - } - - @Override - public Collection> visit(IfStmt stmt, VarIndexing rhsIndexing) { - throw new UnsupportedOperationException("Not yet implemented"); - } - - public VarIndexing getRhsIndexing() { - return rhsIndexing; - } - - public VarIndexing getLhsIndexing() { - return lhsIndexing; - } - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/interpreter/MemoryEventProvider.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/interpreter/MemoryEventProvider.kt new file mode 100644 index 0000000000..10f5af7b09 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/interpreter/MemoryEventProvider.kt @@ -0,0 +1,26 @@ +/* + * Copyright 2023 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.mcm.interpreter + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MemoryEvent + +interface MemoryEventProvider { + + operator fun get(a: A, p: P): MemoryEvent? +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EncodedRelationWrapper.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EncodedRelationWrapper.java similarity index 94% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EncodedRelationWrapper.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EncodedRelationWrapper.java index 4d302398f9..b56e789645 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EncodedRelationWrapper.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EncodedRelationWrapper.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import hu.bme.mit.theta.solver.Solver; @@ -41,7 +41,7 @@ public void addEvent(final String name, final EventConstantLookup lookup) { encodedStatus.put(lookup, false); } - public EventConstantLookup getEventLookup(final String name) { + public EventConstantLookup get(final String name) { return eventLookup.get(name); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EventConstantLookup.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EventConstantLookup.java similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EventConstantLookup.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EventConstantLookup.java index d6d8b5aa2c..b426faba52 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/EventConstantLookup.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/EventConstantLookup.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; @@ -33,7 +33,7 @@ public EventConstantLookup() { forward = new LinkedHashMap<>(); } - public void add(final TupleN key, final ConstDecl value) { + public void set(final TupleN key, final ConstDecl value) { forward.put(key, value); reverse.put(value, key); } diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCM.java similarity index 96% rename from subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCM.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCM.java index 5c41cbe347..4695ad5f93 100644 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCM.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCM.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.cat.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import java.util.Collection; import java.util.LinkedHashMap; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMConstraint.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMConstraint.java similarity index 98% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMConstraint.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMConstraint.java index ac11a30563..a44750f5e0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMConstraint.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMConstraint.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import hu.bme.mit.theta.analysis.algorithm.mcm.rules.TransitiveClosure; import hu.bme.mit.theta.core.type.Expr; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRelation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRelation.java similarity index 91% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRelation.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRelation.java index 3ee7b294be..2dd07db526 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRelation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRelation.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import hu.bme.mit.theta.common.TupleN; @@ -78,8 +78,7 @@ public String toString() { } public EventConstantLookup encodeEvents(final List idList, final EncodedRelationWrapper encodedRelationWrapper) { - if (encodedRelationWrapper.getEventLookup(name) != null) - return encodedRelationWrapper.getEventLookup(name); + if (encodedRelationWrapper.get(name) != null) return encodedRelationWrapper.get(name); final EventConstantLookup eventConstantLookup = new EventConstantLookup(); encodedRelationWrapper.addEvent(name, eventConstantLookup); @@ -92,12 +91,12 @@ public EventConstantLookup encodeEvents(final List idList, final Encode private void createConstants(List idList, EventConstantLookup eventConstantLookup) { if (arity == 1) { for (final int i : idList) { - eventConstantLookup.add(TupleN.of(i), Const(name + "_" + i, Bool())); + eventConstantLookup.set(TupleN.of(i), Const(name + "_" + i, Bool())); } } else if (arity == 2) { for (final int i : idList) { for (final int j : idList) { - eventConstantLookup.add(TupleN.of(i, j), Const(name + "_" + i + "_" + j, Bool())); + eventConstantLookup.set(TupleN.of(i, j), Const(name + "_" + i + "_" + j, Bool())); } } } else diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRule.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRule.java similarity index 94% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRule.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRule.java index a7fe3fcb94..4330eabb29 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MCMRule.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MCMRule.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import java.util.List; import java.util.Map; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEvent.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MemoryEvent.java similarity index 75% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEvent.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MemoryEvent.java index b5320e42ee..ba456eafb6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/MemoryEvent.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/mcm/MemoryEvent.java @@ -14,21 +14,21 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.mcm; +package hu.bme.mit.theta.analysis.algorithm.mcm.mcm; import hu.bme.mit.theta.core.decl.VarDecl; import java.util.Set; -import static com.google.common.base.Preconditions.checkArgument; - public class MemoryEvent { protected final MemoryEventType type; protected final String tag; + protected final int id; - public MemoryEvent(MemoryEventType type, String tag) { + public MemoryEvent(MemoryEventType type, String tag, int id) { this.type = type; this.tag = tag; + this.id = id; } public String tag() { @@ -36,10 +36,16 @@ public String tag() { } public enum MemoryEventType { - READ, - WRITE, - FENCE, - META + READ("R"), + WRITE("W"), + FENCE("F"), + META("M"); + + public final String label; + + private MemoryEventType(String label) { + this.label = label; + } } public MemoryEventType type() { @@ -63,16 +69,13 @@ public MemoryIO asMemoryIO() { } public static abstract class MemoryIO extends MemoryEvent { - private final int varId; private final VarDecl var; private final VarDecl localVar; - public MemoryIO(int varId, VarDecl var, VarDecl localVar, MemoryEventType type, String tag) { - super(type, tag); - checkArgument(varId <= 0, "Meta event IDs must be negative!"); + public MemoryIO(int id, VarDecl var, VarDecl localVar, MemoryEventType type, String tag) { + super(type, tag, id); this.var = var; this.localVar = localVar; - this.varId = varId; } @Override @@ -86,13 +89,10 @@ public String toString() { "var=" + var + ", localVar=" + localVar + ", tag=" + tag + + ", id=" + id + '}'; } - public int varId() { - return varId; - } - public VarDecl var() { return var; } @@ -104,8 +104,8 @@ public VarDecl localVar() { } public static final class Read extends MemoryIO { - public Read(int varId, VarDecl var, VarDecl localVar, String tag) { - super(varId, var, localVar, MemoryEventType.READ, tag); + public Read(int id, VarDecl var, VarDecl localVar, String tag) { + super(id, var, localVar, MemoryEventType.READ, tag); } @Override @@ -117,8 +117,8 @@ public Read asRead() { public static final class Write extends MemoryIO { private final Set> dependencies; - public Write(int varId, VarDecl var, VarDecl localVar, Set> dependencies, String tag) { - super(varId, var, localVar, MemoryEventType.WRITE, tag); + public Write(int id, VarDecl var, VarDecl localVar, Set> dependencies, String tag) { + super(id, var, localVar, MemoryEventType.WRITE, tag); this.dependencies = dependencies; } @@ -133,8 +133,8 @@ public Set> dependencies() { } public static final class Fence extends MemoryEvent { - public Fence(String tag) { - super(MemoryEventType.FENCE, tag); + public Fence(int id, String tag) { + super(MemoryEventType.FENCE, tag, id); } @Override diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/BinaryMCMRule.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/BinaryMCMRule.java index 84df1906ec..1e9a9988bd 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/BinaryMCMRule.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/BinaryMCMRule.java @@ -16,10 +16,10 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRule; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRule; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/CartesianProduct.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/CartesianProduct.java index 4e138f9237..f75a7ae029 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/CartesianProduct.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/CartesianProduct.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Complement.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Complement.java index 2bb4a274b6..09afbf557a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Complement.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Complement.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import java.util.List; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Difference.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Difference.java index a794b11a70..da41cf1305 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Difference.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Difference.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Domain.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Domain.java index 11ce7ceb2e..421aa36538 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Domain.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Domain.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/EmptyRelation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/EmptyRelation.java index 2fa5cc989d..463f7dd04c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/EmptyRelation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/EmptyRelation.java @@ -16,10 +16,10 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRule; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRule; import java.util.List; import java.util.Map; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/IdentityClosure.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/IdentityClosure.java index 0bf3dbaa9a..3ae1e0a2f2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/IdentityClosure.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/IdentityClosure.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Intersection.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Intersection.java index 21c9737755..a61df18045 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Intersection.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Intersection.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Inverse.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Inverse.java index 4e4e283369..e032912a5d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Inverse.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Inverse.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import java.util.List; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Range.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Range.java index e3c81647a3..a19a013b35 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Range.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Range.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/ReflexiveTransitiveClosure.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/ReflexiveTransitiveClosure.java index 9f80a6a2bb..b2a3092005 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/ReflexiveTransitiveClosure.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/ReflexiveTransitiveClosure.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.Expr; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Self.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Self.java index cb4dd0bb32..95e304330a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Self.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Self.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import java.util.List; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Sequence.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Sequence.java index ee3c7a4da6..56e248ec44 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Sequence.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Sequence.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.Expr; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Toid.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Toid.java index 776d395b60..6acd998cf2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Toid.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Toid.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import java.util.List; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/TransitiveClosure.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/TransitiveClosure.java index d3a1da7757..f88c8d5710 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/TransitiveClosure.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/TransitiveClosure.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/UnaryMCMRule.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/UnaryMCMRule.java index 968a4e8aa4..d22eb2835c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/UnaryMCMRule.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/UnaryMCMRule.java @@ -16,8 +16,8 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRule; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRule; import java.util.Map; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Union.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Union.java index f2af77c1a4..facd5d89d6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Union.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/rules/Union.java @@ -16,9 +16,9 @@ package hu.bme.mit.theta.analysis.algorithm.mcm.rules; -import hu.bme.mit.theta.analysis.algorithm.mcm.EncodedRelationWrapper; -import hu.bme.mit.theta.analysis.algorithm.mcm.EventConstantLookup; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EncodedRelationWrapper; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.EventConstantLookup; +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation; import hu.bme.mit.theta.common.TupleN; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MCMTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MCMTest.java deleted file mode 100644 index 88dc583fdd..0000000000 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MCMTest.java +++ /dev/null @@ -1,174 +0,0 @@ -/* - * Copyright 2023 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; - -import hu.bme.mit.theta.analysis.*; -import hu.bme.mit.theta.analysis.algorithm.mcm.*; -import hu.bme.mit.theta.analysis.algorithm.mcm.rules.Inverse; -import hu.bme.mit.theta.analysis.algorithm.mcm.rules.Sequence; -import hu.bme.mit.theta.analysis.algorithm.mcm.rules.Union; -import hu.bme.mit.theta.analysis.expl.ExplState; -import hu.bme.mit.theta.analysis.expr.ExprState; -import hu.bme.mit.theta.analysis.expr.StmtAction; -import hu.bme.mit.theta.common.logging.NullLogger; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; -import org.junit.Test; - -import java.util.Collection; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import static hu.bme.mit.theta.core.decl.Decls.Var; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; - -public class MCMTest { - @Test - public void test() { - final VarDecl var = Var("x", Int()); - final TestState thrd1_loc3 = new TestState(List.of()); - final TestState thrd1_loc2 = new TestState(List.of(new TestAction(new MemoryEvent.Write(-3, var, null, Set.of(), "meta"), thrd1_loc3))); - final TestState thrd1_loc1 = new TestState(List.of(new TestAction(new MemoryEvent.Write(-3, var, null, Set.of(), "meta"), thrd1_loc2))); - - final TestState thrd2_loc3 = new TestState(List.of()); - final TestState thrd2_loc2 = new TestState(List.of(new TestAction(new MemoryEvent.Read(-3, var, null, "meta"), thrd2_loc3))); - final TestState thrd2_loc1 = new TestState(List.of(new TestAction(new MemoryEvent.Read(-3, var, null, "meta"), thrd2_loc2))); - - MCM mcm = new MCM("example"); - MCMRelation sc = new MCMRelation(2, "sc"); - MCMRelation po = new MCMRelation(2, "po"); - MCMRelation rf = new MCMRelation(2, "rf"); - MCMRelation fr = new MCMRelation(2, "fr"); - MCMRelation fr1 = new MCMRelation(2, "fr1"); - MCMRelation co = new MCMRelation(2, "co"); - MCMRelation com = new MCMRelation(2, "com"); - MCMRelation com1 = new MCMRelation(2, "com1"); - sc.addRule(new Union(po, com)); - com1.addRule(new Union(rf, fr)); - com.addRule(new Union(com1, co)); - fr1.addRule(new Inverse(rf)); - fr.addRule(new Sequence(fr1, co)); - mcm.addConstraint(new MCMConstraint(sc, MCMConstraint.ConstraintType.ACYCLIC)); - - - MCMChecker mcmChecker = new MCMChecker<>( - new TestMemoryEventProvider(), - new MultiprocLTS<>(Map.of(-1, new TestLTS(), -2, new TestLTS())), - new MultiprocInitFunc<>(Map.of(-1, new TestInitFunc(thrd1_loc1), -2, new TestInitFunc(thrd2_loc1))), - new MultiprocTransFunc<>(Map.of(-1, new TestTransFunc(), -2, new TestTransFunc())), - List.of(-1, -2), List.of(), new TestPartialOrder(), ExplState.top(), Z3SolverFactory.getInstance().createSolver(), mcm, NullLogger.getInstance()); - -// mcmChecker.check(new TestPrec()); - } - - private class TestMemoryEventProvider implements MemoryEventProvider { - @Override - public Collection> getPiecewiseAction(TestState state, TestAction action) { - return List.of(new ResultElement<>(action.event)); - } - - @Override - public int getVarId(VarDecl var) { - return -3; - } - - @Override - public TestAction createAction(TestState s, List stmt) { - return null; - } - } - - private class TestLTS implements LTS { - - @Override - public Collection getEnabledActionsFor(TestState state) { - return state.outgoingActions; - } - } - - private class TestInitFunc implements InitFunc { - private final TestState initState; - - private TestInitFunc(TestState initState) { - this.initState = initState; - } - - @Override - public Collection getInitStates(TestPrec prec) { - return List.of(initState); - } - } - - private class TestTransFunc implements TransFunc { - - @Override - public Collection getSuccStates(TestState state, TestAction action, TestPrec prec) { - return List.of(action.target); - } - } - - private class TestState implements ExprState { - private final Collection outgoingActions; - - private TestState(Collection outgoingActions) { - this.outgoingActions = outgoingActions; - } - - @Override - public boolean isBottom() { - return false; - } - - @Override - public Expr toExpr() { - return True(); - } - } - - private class TestAction extends StmtAction { - private final MemoryEvent event; - private final TestState target; - - private TestAction(MemoryEvent event, TestState target) { - this.event = event; - this.target = target; - } - - @Override - public List getStmts() { - return List.of(); - } - } - - private class TestPrec implements Prec { - @Override - public Collection> getUsedVars() { - return null; - } - } - - private class TestPartialOrder implements PartialOrd { - @Override - public boolean isLeq(TestState state1, TestState state2) { - return false; - } - } -} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphTest.kt new file mode 100644 index 0000000000..87078eefe3 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mcm/ExecutionGraphTest.kt @@ -0,0 +1,63 @@ +/* + * Copyright 2023 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.mcm + +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.ExecutionGraph +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.TVL +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCM +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMConstraint +import hu.bme.mit.theta.analysis.algorithm.mcm.mcm.MCMRelation +import hu.bme.mit.theta.common.TupleN +import hu.bme.mit.theta.solver.z3.Z3SolverFactory +import org.junit.Assert +import org.junit.Test + +class ExecutionGraphTest { + + @Test + fun test() { + val mcm: MCM = MCM("test-mcm") + mcm.addConstraint( + MCMConstraint( + MCMRelation(2, "po"), + MCMConstraint.ConstraintType.ACYCLIC + )) + val solver = Z3SolverFactory.getInstance().createSolver() + + val executionGraph = ExecutionGraph() + executionGraph.addEvent(0) + executionGraph.addEvent(1) + executionGraph.addEvent(2) + + executionGraph["po", TupleN.of(0, 1)] = TVL.TRUE + executionGraph["po", TupleN.of(0, 2)] = TVL.TRUE + executionGraph["po", TupleN.of(1, 2)] = TVL.TRUE + + solver.push() + solver.add(executionGraph.toExpr(mcm)) + val safeResult = solver.check() + Assert.assertTrue(safeResult.isSat) + solver.pop() + + executionGraph["po", TupleN.of(2, 0)] = TVL.TRUE + + solver.push() + solver.add(executionGraph.toExpr(mcm)) + val unsafeResult = solver.check() + Assert.assertTrue(unsafeResult.isUnsat) + solver.pop() + } +} \ No newline at end of file diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/Tuple1.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/Tuple1.java new file mode 100644 index 0000000000..889326594b --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/Tuple1.java @@ -0,0 +1,44 @@ +/* + * Copyright 2023 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.common; + +import com.google.common.collect.ImmutableList; + +import java.util.function.Function; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class Tuple1 extends Tuple { + + private Tuple1(final T1 e1) { + super(ImmutableList.of(e1)); + } + + public static Tuple1 of(final T1 e1) { + return new Tuple1<>(e1); + } + + public T1 get1() { + @SuppressWarnings("unchecked") final T1 result = (T1) elem(0); + return result; + } + + public R unpackTo(final Function function) { + checkNotNull(function); + return function.apply(get1()); + } + +} diff --git a/subprojects/frontends/c-frontend/build.gradle.kts b/subprojects/frontends/c-frontend/build.gradle.kts index 2fedd4ac78..8277abb3f6 100644 --- a/subprojects/frontends/c-frontend/build.gradle.kts +++ b/subprojects/frontends/c-frontend/build.gradle.kts @@ -14,7 +14,7 @@ * limitations under the License. */ plugins { - id("java-common") + id("kotlin-common") id("antlr-grammar") } dependencies { diff --git a/subprojects/frontends/c-frontend/src/main/antlr/Boogie.g4 b/subprojects/frontends/c-frontend/src/main/antlr/Boogie.g4 new file mode 100644 index 0000000000..19d416cfeb --- /dev/null +++ b/subprojects/frontends/c-frontend/src/main/antlr/Boogie.g4 @@ -0,0 +1,87 @@ +grammar Boogie; + +prog: decl+; + +decl: proc | global | impl | constDecl | axiom | func | typeparam | varDecl | typeDef; + +typeDef: 'type' ID (typeparam)* ('=' type)? ';'; + +varDecl: VAR (var (',' var)*)? ';'; + +proc: PROC ID (typeparam)* '(' (var (',' var)*)? ')' (':' type)? ';' + 'modifies' '(' (ID (',' ID)*)? ')' ';' + ( 'ensures' exp)? ';' + ( 'requires' exp)? ';' + '{' stmt* '}'; + +global: VAR (var ':=' exp)? (',' var ':=' exp)* ';'; + +impl: IMPL ID (typeparam)* '(' (var (',' var)*)? ')' (':' type)? ';' + 'modifies' '(' (ID (',' ID)*)? ')' ';' + ( 'ensures' exp)? ';' + ( 'requires' exp)? ';' + '{' stmt* '}'; + +var: ID (':' type)?; + +constDecl: CONST ID (':' type)? (':=' exp)? ';'; + +axiom: AXIOM exp ';'; + +func: FUNC ID (typeparam)* '(' (var (',' var)*)? ')' (':' type)? ';' + '{' stmt* '}'; + +type: INT_TYPE | BOOL | '[' 'int' ']' type | 'map' '[' type ']' 'to' type | BV | ID; + +typeparam: '$' ID (':' type)?; + +stmt: ID ':=' exp ';' + | ID '[' exp ']:=' exp ';' + | WHILE '(' exp ')' '{' stmt* '}' + | IF '(' exp ')' '{' stmt* '}' (ELSE '{' stmt* '}')? + | CALL ID '(' (exp (',' exp)*)? ')' ';' + | ASSERT exp ';' + | ASSUME exp ';' + | RETURN (exp)? ';' + | HAVOC ID (',' ID)* ';' + | FORALL '(' var (',' var)* ')' '{' stmt* '}' + | GHOST ID ':=' exp ';'; + +exp: ID + | ID '(' (exp (',' exp)*)? ')' + | ID '[' exp ']' + | exp op exp + | '(' exp ')' + | '!' exp + | OLD '(' exp ')' + | 'true' | 'false' + | INT | BV; + +op: '&&' | '||' | '==' | '!=' | '<' | '<=' | '>' | '>=' | '+' | '-' | '*' | '/' | 'bvand' | 'bvor' | 'bvxor' | 'bvnot' | 'bvshl' | 'bvlshr' | 'bvashr'; + +VAR: 'var'; +PROC: 'procedure'; +IMPL: 'implementation'; +CONST: 'constDecl'; +AXIOM: 'axiom'; +FUNC: 'function'; +CALL: 'call'; +WHILE: 'while'; +IF: 'if'; +ELSE: 'else'; +ASSERT: 'assert'; +ASSUME: 'assume'; +RETURN: 'return'; +HAVOC: 'havoc'; +OLD: 'old'; +FORALL: 'forall'; +BV: 'bv' [0-9]+; +BOOL: 'bool'; +INT_TYPE: 'int'; +GHOST: 'ghost'; + +INT: [0-9]+; +ID: [a-zA-Z_$.][a-zA-Z0-9_.]*; + + +WS: [ \t\r\n] -> skip; \ No newline at end of file diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/CStatistics.kt b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/CStatistics.kt new file mode 100644 index 0000000000..976cbd7756 --- /dev/null +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/CStatistics.kt @@ -0,0 +1,175 @@ +/* + * Copyright 2023 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.frontend + +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.abstracttype.DivExpr +import hu.bme.mit.theta.core.type.abstracttype.MulExpr +import hu.bme.mit.theta.frontend.transformation.model.statements.* + +data class CStatistics( + val globalDeclarations: Int, + val functions: Collection, +) + +data class CFunctionStatistics( + val variables: Int, + val loopNumber: Int, + val deepestLoop: Int, + val linear: Boolean, +) + +fun CProgram.getStatistics(): CStatistics { + return CStatistics( + globalDeclarations = globalDeclarations.size, + functions = functions.map { + val (loopNumber, deepestLoop, linear) = it.collectStatistics() + CFunctionStatistics( + variables = it.flatVariables.size, + loopNumber = loopNumber, + deepestLoop = deepestLoop, + linear = linear + ) + } + ) +} + +fun CFunction.collectStatistics(): Triple { + val statisticsCollectorVisitor = StatisticsCollectorVisitor() + this.compound?.accept(statisticsCollectorVisitor, Unit) + return Triple(statisticsCollectorVisitor.loopNumber, statisticsCollectorVisitor.deepestLoop, + statisticsCollectorVisitor.linear) +} + +fun Expr<*>.isNonLinear(): Boolean { + if (this is MulExpr<*> || this is DivExpr<*>) { + return true; + } else if (this.ops.size > 0) { + return this.ops.any { it.isNonLinear() } + } else return false; +} + +class StatisticsCollectorVisitor : CStatementVisitor { + + var loopNumber = 0 + private set + var deepestLoop = 0 + private set + var linear = true + private set + + private var currentDepth = 0 + + override fun visit(statement: CAssignment, param: Unit) { + val lval = statement.getlValue() + if (linear && lval.isNonLinear()) linear = false + statement.getrValue()?.accept(this, param) + } + + override fun visit(statement: CAssume, param: Unit) { + if (linear && statement.assumeStmt.cond.isNonLinear()) linear = false + } + + override fun visit(statement: CBreak, param: Unit) { + } + + override fun visit(statement: CCall, param: Unit) { + statement.params.forEach { it?.accept(this, param) } + } + + override fun visit(statement: CCase, param: Unit) { + statement.expr?.accept(this, param) + statement.statement?.accept(this, param) + } + + override fun visit(statement: CCompound, param: Unit) { + statement.getcStatementList().forEach { it?.accept(this, param) } + } + + override fun visit(statement: CContinue, param: Unit) { + } + + override fun visit(statement: CDecls, param: Unit) { + statement.getcDeclarations().map { it.get1().initExpr?.accept(this, param) } + } + + override fun visit(statement: CDefault, param: Unit) { + statement.statement?.accept(this, param) + } + + override fun visit(statement: CDoWhile, param: Unit) { + loopNumber++ + statement.guard?.accept(this, param) + currentDepth++ + if (deepestLoop < currentDepth) deepestLoop = currentDepth + statement.body?.accept(this, param) + currentDepth-- + } + + override fun visit(statement: CExpr, param: Unit) { + if (linear && statement.expr?.isNonLinear() == true) linear = false + } + + override fun visit(statement: CFor, param: Unit) { + loopNumber++ + statement.init?.accept(this, param) + statement.guard?.accept(this, param) + statement.increment?.accept(this, param) + currentDepth++ + if (deepestLoop < currentDepth) deepestLoop = currentDepth + statement.body?.accept(this, param) + currentDepth-- + } + + override fun visit(statement: CFunction, param: Unit) { + System.err.println("WARNING: Should not be here (CFUnction embedding not supported)") + } + + override fun visit(statement: CGoto, param: Unit) { + } + + override fun visit(statement: CIf, param: Unit) { + statement.guard?.accept(this, param) + statement.body?.accept(this, param) + } + + override fun visit(statement: CInitializerList, param: Unit) { + statement.statements.forEach { it.get1().map { it?.accept(this, param) }; it.get2()?.accept(this, param) } + } + + override fun visit(statement: CProgram, param: Unit) { + System.err.println("WARNING: Should not be here (CProgram embedding not supported)") + } + + override fun visit(statement: CRet, param: Unit) { + statement.expr?.accept(this, param); + } + + override fun visit(statement: CSwitch, param: Unit) { + statement.testValue?.accept(this, param) + statement.body?.accept(this, param) + } + + override fun visit(statement: CWhile, param: Unit) { + loopNumber++ + statement.guard?.accept(this, param) + currentDepth++ + if (deepestLoop < currentDepth) deepestLoop = currentDepth + statement.body?.accept(this, param) + currentDepth-- + } +} + diff --git a/subprojects/solver/graph-solver/README.md b/subprojects/solver/graph-solver/README.md new file mode 100644 index 0000000000..30404ce4c5 --- /dev/null +++ b/subprojects/solver/graph-solver/README.md @@ -0,0 +1 @@ +TODO \ No newline at end of file diff --git a/subprojects/solver/graph-solver/build.gradle.kts b/subprojects/solver/graph-solver/build.gradle.kts new file mode 100644 index 0000000000..4df6331291 --- /dev/null +++ b/subprojects/solver/graph-solver/build.gradle.kts @@ -0,0 +1,26 @@ +/* + * Copyright 2023 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("java-common") +} + +dependencies { + implementation(project(":theta-common")) + implementation(project(":theta-core")) + implementation(project(":theta-solver")) + testImplementation(project(":theta-solver-z3")) +} diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRule.java b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/3VL.kt similarity index 78% rename from subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRule.java rename to subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/3VL.kt index 5cd19e0d0b..4e18d1bc18 100644 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRule.java +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/3VL.kt @@ -14,10 +14,10 @@ * limitations under the License. */ -package hu.bme.mit.theta.cat.mcm; +package hu.bme.mit.theta.graphsolver -import java.util.Map; - -public abstract class MCMRule { - public abstract void collectRelations(final Map relations); -} +enum class ThreeVL { + TRUE, + UNKNOWN, + FALSE +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/Utils.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/Utils.kt new file mode 100644 index 0000000000..dd3c676e0b --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/Utils.kt @@ -0,0 +1,55 @@ +/* + * Copyright 2023 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.graphsolver + +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.* + +fun GraphConstraint.collectSubRelations(): Set = when (this) { + is Acyclic -> this.constrainedRule.collectSubRelations() + is Cyclic -> this.constrainedRule.collectSubRelations() + is Empty -> this.constrainedRule.collectSubRelations() + is Irreflexive -> this.constrainedRule.collectSubRelations() + is Nonempty -> this.constrainedRule.collectSubRelations() + is Reflexive -> this.constrainedRule.collectSubRelations() +} + +fun GraphPattern.collectSubRelations(): Set = when (this) { + is BasicRelation -> emptySet() + is CartesianProduct -> op1.collectSubRelations() union op2.collectSubRelations() + is Complement -> op.collectSubRelations() + is Difference -> op1.collectSubRelations() union op2.collectSubRelations() + EmptyRel -> emptySet() + EmptyRelation -> emptySet() + is IdentityClosure -> op.collectSubRelations() + is Intersection -> op1.collectSubRelations() union op2.collectSubRelations() + is Inverse -> op.collectSubRelations() + is ReflexiveTransitiveClosure -> op.collectSubRelations() + is Self -> op.collectSubRelations() + is Sequence -> op1.collectSubRelations() union op2.collectSubRelations() + is Toid -> op.collectSubRelations() + is TransitiveClosure -> op.collectSubRelations() + is Union -> op1.collectSubRelations() union op2.collectSubRelations() + is BasicEventSet -> emptySet() + is ComplementNode -> op.collectSubRelations() + is DifferenceNode -> op1.collectSubRelations() union op2.collectSubRelations() + is Domain -> op.collectSubRelations() + is IntersectionNode -> op1.collectSubRelations() union op2.collectSubRelations() + is Range -> op.collectSubRelations() + is UnionNode -> op1.collectSubRelations() union op2.collectSubRelations() + else -> error("Should not be here") +} union if (patternName != null) setOf(this) else emptySet() \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/DefaultGraphPatternCompiler.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/DefaultGraphPatternCompiler.kt new file mode 100644 index 0000000000..eaf9ef751a --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/DefaultGraphPatternCompiler.kt @@ -0,0 +1,117 @@ +/* + * Copyright 2023 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.graphsolver.compilers + +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.graphsolver.ThreeVL +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.* + +abstract class DefaultGraphPatternCompiler : GraphPatternCompiler { + + override fun addEvents(events: List) {} + override fun addFacts(edges: Map, ThreeVL>) {} + override fun compile(acyclic: Acyclic): T? = acyclic.constrainedRule.accept(this) + override fun compile(cyclic: Cyclic): T? = cyclic.constrainedRule.accept(this) + override fun compile(empty: Empty): T? = empty.constrainedRule.accept(this) + override fun compile(nonempty: Nonempty): T? = nonempty.constrainedRule.accept(this) + override fun compile(reflexive: Reflexive): T? = reflexive.constrainedRule.accept(this) + override fun compile(irreflexive: Irreflexive): T? = irreflexive.constrainedRule.accept(this) + + override fun compile(pattern: CartesianProduct): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: Complement): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: ComplementNode): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Difference): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: DifferenceNode): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: Domain): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: EmptyRelation): T? = null + override fun compile(pattern: EmptyRel): T? = null + override fun compile(pattern: IdentityClosure): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Intersection): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: IntersectionNode): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: Inverse): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Range): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: ReflexiveTransitiveClosure): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Self): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Sequence): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: Toid): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: TransitiveClosure): T? { + pattern.op.accept(this); return null + } + + override fun compile(pattern: Union): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: UnionNode): T? { + pattern.op1.accept(this); pattern.op2.accept(this); return null + } + + override fun compile(pattern: BasicEventSet): T? = null + override fun compile(pattern: BasicRelation): T? = null + + override fun getCompleteGraph(mcm: Set, + model: Valuation): Pair, Map, ThreeVL>> { + error("Not implemented") + } +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/GraphPatternCompiler.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/GraphPatternCompiler.kt new file mode 100644 index 0000000000..b64b7ee73e --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/GraphPatternCompiler.kt @@ -0,0 +1,64 @@ +/* + * Copyright 2023 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.graphsolver.compilers + +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.graphsolver.ThreeVL +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.* + +/** + * @param T1 Compiled constraint type + * @param T2 Compiled pattern type + */ +interface GraphPatternCompiler { + + fun addEvents(events: List) + fun addFacts(edges: Map, ThreeVL>) + fun compile(acyclic: Acyclic): T1 + fun compile(cyclic: Cyclic): T1 + fun compile(empty: Empty): T1 + fun compile(nonempty: Nonempty): T1 + fun compile(reflexive: Reflexive): T1 + fun compile(irreflexive: Irreflexive): T1 + + fun compile(pattern: CartesianProduct): T2 + fun compile(pattern: Complement): T2 + fun compile(pattern: ComplementNode): T2 + fun compile(pattern: Difference): T2 + fun compile(pattern: DifferenceNode): T2 + fun compile(pattern: Domain): T2 + fun compile(pattern: EmptyRelation): T2 + fun compile(pattern: EmptyRel): T2 + fun compile(pattern: IdentityClosure): T2 + fun compile(pattern: Intersection): T2 + fun compile(pattern: IntersectionNode): T2 + fun compile(pattern: Inverse): T2 + fun compile(pattern: Range): T2 + fun compile(pattern: ReflexiveTransitiveClosure): T2 + fun compile(pattern: Self): T2 + fun compile(pattern: Sequence): T2 + fun compile(pattern: Toid): T2 + fun compile(pattern: TransitiveClosure): T2 + fun compile(pattern: Union): T2 + fun compile(pattern: UnionNode): T2 + fun compile(pattern: BasicEventSet): T2 + fun compile(pattern: BasicRelation): T2 + fun getCompleteGraph(namedPatterns: Set, + model: Valuation): Pair, Map, ThreeVL>> +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt new file mode 100644 index 0000000000..ab0360fbad --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt @@ -0,0 +1,346 @@ +/* + * Copyright 2023 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.graphsolver.compilers.pattern2expr + +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.common.Tuple1 +import hu.bme.mit.theta.common.Tuple2 +import hu.bme.mit.theta.core.decl.ConstDecl +import hu.bme.mit.theta.core.decl.Decls.Const +import hu.bme.mit.theta.core.model.Valuation +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.graphsolver.ThreeVL +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.* +import java.util.* +import kotlin.jvm.optionals.getOrNull + +class Pattern2ExprCompiler : GraphPatternCompiler, Map>> { + + private val events = ArrayList() + private val facts = LinkedHashMap, ThreeVL>() + private val namedLookup = LinkedHashMap, ConstDecl>() + + private val transitiveConstraints = ArrayList>() + override fun addEvents(events: List) { + this.events.addAll(events) + } + + override fun addFacts(edges: Map, ThreeVL>) { + this.facts.putAll(edges) + } + + @OptIn(ExperimentalStdlibApi::class) + override fun getCompleteGraph(namedPatterns: Set, + model: Valuation): Pair, Map, ThreeVL>> { + val ret = LinkedHashMap, ThreeVL>() + ret.putAll(facts) + ret.putAll(namedLookup.map { n -> + model.eval(n.value).map { Pair(n.key, if (it == True()) ThreeVL.TRUE else ThreeVL.FALSE) }.getOrNull() + }.filterNotNull().toMap()) + ret.putAll(namedPatterns.map { pattern -> + pattern.accept(this).map { (tup, expr) -> + Pair(Pair(pattern.patternName!!, tup), if (expr.eval(model) == True()) ThreeVL.TRUE else ThreeVL.FALSE) + } + }.flatten().toMap()) + return Pair(events, ret) + } + + override fun compile(acyclic: Acyclic): Expr = + Irreflexive(TransitiveClosure(acyclic.constrainedRule)).accept(this) + + override fun compile(cyclic: Cyclic): Expr = + Reflexive(TransitiveClosure(cyclic.constrainedRule)).accept(this) + + override fun compile(empty: Empty): Expr { + val compiledRule = empty.constrainedRule.accept(this) + val ret = And(Not(Or(compiledRule.values)), And(transitiveConstraints)) + transitiveConstraints.clear() + return ret + } + + override fun compile(nonempty: Nonempty): Expr { + val compiledRule = nonempty.constrainedRule.accept(this) + val ret = And(Or(compiledRule.values), And(transitiveConstraints)) + transitiveConstraints.clear() + return ret + } + + override fun compile(reflexive: Reflexive): Expr { + val compiled = reflexive.constrainedRule.accept(this) + val ret = And(Or(events.map { compiled[Tuple2.of(it, it)] }), And(transitiveConstraints)) + transitiveConstraints.clear() + return ret + } + + override fun compile(irreflexive: Irreflexive): Expr { + val compiled = irreflexive.constrainedRule.accept(this) + val ret = And(Not(Or(events.map { compiled[Tuple2.of(it, it)] })), And(transitiveConstraints)) + transitiveConstraints.clear() + return ret + } + + override fun compile(pattern: CartesianProduct): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), And(op1Compiled[Tuple1.of(a)], op2Compiled[Tuple1.of(b)])) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: Complement): Map> = + pattern.op.accept(this).map { Pair(it.key, Not(it.value)) }.toMap() + + override fun compile(pattern: ComplementNode): Map> = + pattern.op.accept(this).map { Pair(it.key, Not(it.value)) }.toMap() + + override fun compile(pattern: Difference): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), And(op1Compiled[Tuple2.of(a, b)], Not(op2Compiled[Tuple2.of(a, b)]))) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: DifferenceNode): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> Pair(Tuple1.of(a), And(op1Compiled[Tuple1.of(a)], Not(op2Compiled[Tuple1.of(a)]))) } + return ret.toMap() + } + + override fun compile(pattern: Domain): Map> { + val opCompiled = pattern.op.accept(this) + + val ret = events.map { a -> Pair(Tuple1.of(a), Or(events.map { b -> opCompiled[Tuple2.of(a, b)] })) } + return ret.toMap() + } + + override fun compile(pattern: EmptyRelation): Map> { + return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), False()) } }.flatten().toMap() + } + + override fun compile(pattern: EmptyRel): Map> { + return events.associate { a -> Pair(Tuple1.of(a), False()) } + } + + override fun compile(pattern: IdentityClosure): Map> { + val opCompiled = pattern.op.accept(this) + return events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(opCompiled[Tuple2.of(a, b)])) + } + }.flatten().toMap() + } + + override fun compile(pattern: Intersection): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), And(op1Compiled[Tuple2.of(a, b)], op2Compiled[Tuple2.of(a, b)])) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: IntersectionNode): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> Pair(Tuple1.of(a), And(op1Compiled[Tuple1.of(a)], op2Compiled[Tuple1.of(a)])) } + return ret.toMap() + } + + override fun compile(pattern: Inverse): Map> { + val opCompiled = pattern.op.accept(this) + return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), checkNotNull(opCompiled[Tuple2.of(b, a)])) } } + .flatten() + .toMap() + } + + override fun compile(pattern: Range): Map> { + val opCompiled = pattern.op.accept(this) + + val ret = events.map { a -> Pair(Tuple1.of(a), Or(events.map { b -> opCompiled[Tuple2.of(a, b)] })) } + return ret.toMap() + } + + override fun compile(pattern: ReflexiveTransitiveClosure): Map> { + val opCompiled = pattern.op.accept(this) + val uuid = Random().nextInt() + val consts = events.map { a -> + events.map { b -> + val const = if (pattern.patternName != null) { + val const = namedLookup[Pair(pattern.patternName!!, Tuple2.of(a, b))] ?: Const( + "RTC_" + uuid + "_" + a + "_" + b, Bool()) + namedLookup[Pair(pattern.patternName!!, Tuple2.of(a, b))] = const + const + } else { + Const("RTC_" + uuid + "_" + a + "_" + b, Bool()) + } + Pair(Tuple2.of(a, b), const) + } + }.flatten().toMap() + + val constraints = And(events.map { a -> + events.map { b -> + Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.map { c -> + Or( + And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref), + And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)]) + ) + })), checkNotNull(consts[Tuple2.of(a, b)]).ref) + } + }.flatten()) + transitiveConstraints.add(constraints) + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(consts[Tuple2.of(a, b)]).ref) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: Self): Map> = + pattern.op.accept(this) + + override fun compile(pattern: Sequence): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), Or(events.filter { c -> a != c && b != c }.map { c -> + And(op1Compiled[Tuple2.of(a, c)], op2Compiled[Tuple2.of(c, b)]) + })) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: Toid): Map> { + val opCompiled = pattern.op.accept(this) + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), if (a == b) checkNotNull(opCompiled[Tuple1.of(a)]) else False()) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: TransitiveClosure): Map> { + val uuid = Random().nextInt() + val opCompiled = pattern.op.accept(this) + val consts = events.map { a -> + events.map { b -> + val const = if (pattern.patternName != null) { + val const = namedLookup[Pair(pattern.patternName!!, Tuple2.of(a, b))] ?: Const( + "TC_" + uuid + "_" + a + "_" + b, Bool()) + namedLookup[Pair(pattern.patternName!!, Tuple2.of(a, b))] = const + const + } else { + Const("TC_" + uuid + "_" + a + "_" + b, Bool()) + } + Pair(Tuple2.of(a, b), const) + } + }.flatten().toMap() + + val constraints = And(events.map { a -> + events.map { b -> + Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.filter { c -> a != c && b != c }.map { c -> + Or( + And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref), + And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)]) + ) + })), checkNotNull(consts[Tuple2.of(a, b)]).ref) + } + }.flatten()) + transitiveConstraints.add(constraints) + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), checkNotNull(consts[Tuple2.of(a, b)]).ref) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: Union): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), Or(op1Compiled[Tuple2.of(a, b)], op2Compiled[Tuple2.of(a, b)])) + } + } + return ret.flatten().toMap() + } + + override fun compile(pattern: UnionNode): Map> { + val op1Compiled = pattern.op1.accept(this) + val op2Compiled = pattern.op2.accept(this) + + val ret = events.map { a -> Pair(Tuple1.of(a), And(op1Compiled[Tuple1.of(a)], op2Compiled[Tuple1.of(a)])) } + return ret.toMap() + } + + override fun compile(pattern: BasicEventSet): Map> { + return events.associate { a -> + Pair(Tuple1.of(a), + when (facts[Pair(pattern.name, Tuple1.of(a))]) { + ThreeVL.FALSE -> False() + ThreeVL.TRUE -> True() + ThreeVL.UNKNOWN, null -> namedLookup.getOrElse(Pair(pattern.name, Tuple1.of(a))) { + val cnst = Const(pattern.name + "_" + a, Bool()) + namedLookup[Pair(pattern.name, Tuple1.of(a))] = cnst + cnst + }.ref + }) + } + } + + override fun compile(pattern: BasicRelation): Map> { + return events.map { a -> + events.map { b -> + Pair(Tuple2.of(a, b), + when (facts[Pair(pattern.name, Tuple2.of(a, b))]) { + ThreeVL.FALSE -> False() + ThreeVL.TRUE -> True() + ThreeVL.UNKNOWN, null -> namedLookup.getOrElse(Pair(pattern.name, Tuple2.of(a, b))) { + val cnst = Const(pattern.name + "_" + a + "-" + b, Bool()) + namedLookup[Pair(pattern.name, Tuple2.of(a, b))] = cnst + cnst + }.ref + }) + } + }.flatten().toMap() + } +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Acyclic.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Acyclic.kt new file mode 100644 index 0000000000..550759e14e --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Acyclic.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.EdgePattern + +class Acyclic(val constrainedRule: EdgePattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Cyclic.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Cyclic.kt new file mode 100644 index 0000000000..96c78f1885 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Cyclic.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.EdgePattern + +class Cyclic(val constrainedRule: EdgePattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Empty.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Empty.kt new file mode 100644 index 0000000000..c1a6b05610 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Empty.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.GraphPattern + +class Empty(val constrainedRule: GraphPattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt new file mode 100644 index 0000000000..f8b067fefc --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt @@ -0,0 +1,24 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +sealed interface GraphConstraint { + + fun accept(compiler: GraphPatternCompiler): T +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Irreflexive.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Irreflexive.kt new file mode 100644 index 0000000000..7a2bd1ca44 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Irreflexive.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.EdgePattern + +class Irreflexive(val constrainedRule: EdgePattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Nonempty.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Nonempty.kt new file mode 100644 index 0000000000..6c4f1b5302 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Nonempty.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.GraphPattern + +class Nonempty(val constrainedRule: GraphPattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Reflexive.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Reflexive.kt new file mode 100644 index 0000000000..019789ddd5 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/Reflexive.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.constraints + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.patterns.patterns.EdgePattern + +class Reflexive(val constrainedRule: EdgePattern) : GraphConstraint { + + override fun accept(compiler: GraphPatternCompiler): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicEventSet.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicEventSet.kt new file mode 100644 index 0000000000..a21d75fafa --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicEventSet.kt @@ -0,0 +1,27 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class BasicEventSet(val name: String) : NodePattern() { + + init { + patternName = name + } + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicRelation.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicRelation.kt new file mode 100644 index 0000000000..730aad40db --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/BasicRelation.kt @@ -0,0 +1,27 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class BasicRelation(val name: String) : EdgePattern() { + + init { + patternName = name + } + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/CartesianProduct.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/CartesianProduct.kt new file mode 100644 index 0000000000..8bd967e774 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/CartesianProduct.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class CartesianProduct(val op1: NodePattern, val op2: NodePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Complement.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Complement.kt new file mode 100644 index 0000000000..d1ddf15ad3 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Complement.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Complement(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ComplementNode.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ComplementNode.kt new file mode 100644 index 0000000000..62e142249b --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ComplementNode.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class ComplementNode(val op: NodePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Difference.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Difference.kt new file mode 100644 index 0000000000..aa9dde30fc --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Difference.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Difference(val op1: EdgePattern, val op2: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/DifferenceNode.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/DifferenceNode.kt new file mode 100644 index 0000000000..f582b744d4 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/DifferenceNode.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class DifferenceNode(val op1: NodePattern, val op2: NodePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Domain.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Domain.kt new file mode 100644 index 0000000000..540918cdd5 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Domain.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Domain(val op: EdgePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EdgePattern.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EdgePattern.kt new file mode 100644 index 0000000000..5af80d0bf1 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EdgePattern.kt @@ -0,0 +1,19 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +sealed class EdgePattern : GraphPattern() \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRel.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRel.kt new file mode 100644 index 0000000000..39ecf69484 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRel.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +object EmptyRel : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRelation.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRelation.kt new file mode 100644 index 0000000000..8b0f5748cf --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/EmptyRelation.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +object EmptyRelation : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/GraphPattern.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/GraphPattern.kt new file mode 100644 index 0000000000..30259c7862 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/GraphPattern.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +sealed class GraphPattern { + + var patternName: String? = null + abstract fun accept(compiler: GraphPatternCompiler<*, T>): T +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IdentityClosure.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IdentityClosure.kt new file mode 100644 index 0000000000..79f66a0098 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IdentityClosure.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class IdentityClosure(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Intersection.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Intersection.kt new file mode 100644 index 0000000000..aa8ffc7154 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Intersection.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Intersection(val op1: EdgePattern, val op2: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IntersectionNode.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IntersectionNode.kt new file mode 100644 index 0000000000..97e3f953e7 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/IntersectionNode.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class IntersectionNode(val op1: NodePattern, val op2: NodePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Inverse.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Inverse.kt new file mode 100644 index 0000000000..09210a03f1 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Inverse.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Inverse(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/NodePattern.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/NodePattern.kt new file mode 100644 index 0000000000..848be1ef23 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/NodePattern.kt @@ -0,0 +1,19 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +sealed class NodePattern : GraphPattern() \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Range.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Range.kt new file mode 100644 index 0000000000..cde945c8a1 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Range.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Range(val op: EdgePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ReflexiveTransitiveClosure.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ReflexiveTransitiveClosure.kt new file mode 100644 index 0000000000..67bc1a8241 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/ReflexiveTransitiveClosure.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class ReflexiveTransitiveClosure(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Self.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Self.kt new file mode 100644 index 0000000000..7436c63ecd --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Self.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Self(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Sequence.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Sequence.kt new file mode 100644 index 0000000000..a6c88bac63 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Sequence.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Sequence(val op1: EdgePattern, val op2: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Toid.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Toid.kt new file mode 100644 index 0000000000..cc0798a04a --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Toid.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Toid(val op: NodePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/TransitiveClosure.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/TransitiveClosure.kt new file mode 100644 index 0000000000..23f04e086b --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/TransitiveClosure.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class TransitiveClosure(val op: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Union.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Union.kt new file mode 100644 index 0000000000..5027019e2a --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/Union.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class Union(val op1: EdgePattern, val op2: EdgePattern) : EdgePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/UnionNode.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/UnionNode.kt new file mode 100644 index 0000000000..d3a8d151cc --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/patterns/UnionNode.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2023 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.graphsolver.patterns.patterns + +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler + +class UnionNode(val op1: NodePattern, val op2: NodePattern) : NodePattern() { + + override fun accept(compiler: GraphPatternCompiler<*, T>): T = compiler.compile(this) +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/GraphSolver.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/GraphSolver.kt new file mode 100644 index 0000000000..22f51386ef --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/GraphSolver.kt @@ -0,0 +1,32 @@ +/* + * Copyright 2023 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.graphsolver.solvers + +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.solver.SolverStatus + +interface GraphSolver { + + fun add(t: T) + + fun getAll(): Collection + + fun check(): SolverStatus + + fun getModel(): Valuation + +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/SATGraphSolver.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/SATGraphSolver.kt new file mode 100644 index 0000000000..fd7642a3e4 --- /dev/null +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/solvers/SATGraphSolver.kt @@ -0,0 +1,33 @@ +/* + * Copyright 2023 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.graphsolver.solvers + +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.solver.Solver +import hu.bme.mit.theta.solver.SolverStatus + +class SATGraphSolver(val solver: Solver) : GraphSolver> { + + override fun add(t: Expr) = solver.add(t) + + override fun getAll(): Collection> = solver.assertions + + override fun check(): SolverStatus = solver.check() + override fun getModel(): Valuation = solver.model +} \ No newline at end of file diff --git a/subprojects/solver/graph-solver/src/test/java/hu/bme/mit/theta/graphsolver/GraphSolverTest.kt b/subprojects/solver/graph-solver/src/test/java/hu/bme/mit/theta/graphsolver/GraphSolverTest.kt new file mode 100644 index 0000000000..b1e2997d88 --- /dev/null +++ b/subprojects/solver/graph-solver/src/test/java/hu/bme/mit/theta/graphsolver/GraphSolverTest.kt @@ -0,0 +1,214 @@ +/* + * Copyright 2023 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.graphsolver + +import hu.bme.mit.theta.common.Tuple +import hu.bme.mit.theta.common.Tuple2 +import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler +import hu.bme.mit.theta.graphsolver.compilers.pattern2expr.Pattern2ExprCompiler +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.BasicRelation +import hu.bme.mit.theta.graphsolver.solvers.GraphSolver +import hu.bme.mit.theta.graphsolver.solvers.SATGraphSolver +import hu.bme.mit.theta.solver.z3.Z3SolverFactory +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import org.junit.runners.Parameterized.Parameter +import java.io.IOException +import java.util.* + +@RunWith(Parameterized::class) +class GraphSolverTest { + + @Parameter(0) + @JvmField + var constraint: GraphConstraint? = null + + @Parameter(1) + @JvmField + var compiler: GraphPatternCompiler? = null + + @Parameter(2) + @JvmField + var graphEvents: List? = null + + @Parameter(3) + @JvmField + var graphEdges: Map, ThreeVL>? = null + + @Parameter(4) + @JvmField + var solver: GraphSolver? = null + + @Parameter(5) + @JvmField + var allowed: Boolean = false + + @Test + @Throws(IOException::class) + fun test() { + compiler!!.addEvents(graphEvents!!) + compiler!!.addFacts(graphEdges!!) + val compiledConstraint = constraint!!.accept(compiler!!) + solver!!.add(compiledConstraint) + val status = solver!!.check() + Assert.assertEquals(allowed, status.isSat) + } + + companion object { + + private val smallLine: Pair, Map, ThreeVL>> = Pair(listOf(1, 2, 3), mapOf( + Pair(Pair("po", Tuple2.of(1, 1)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(1, 2)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(1, 3)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 1)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 2)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 3)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 1)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(3, 2)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(3, 3)), ThreeVL.FALSE), + )) + + private val smallCycle: Pair, Map, ThreeVL>> = Pair(listOf(1, 2, 3), mapOf( + Pair(Pair("po", Tuple2.of(1, 1)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(1, 2)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(1, 3)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 1)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 2)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(2, 3)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 1)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 2)), ThreeVL.FALSE), + Pair(Pair("po", Tuple2.of(3, 3)), ThreeVL.FALSE), + )) + + private val smallFull: Pair, Map, ThreeVL>> = Pair(listOf(1, 2, 3), mapOf( + Pair(Pair("po", Tuple2.of(1, 1)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(1, 2)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(1, 3)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(2, 1)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(2, 2)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(2, 3)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 1)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 2)), ThreeVL.TRUE), + Pair(Pair("po", Tuple2.of(3, 3)), ThreeVL.TRUE), + )) + + @Parameterized.Parameters + @JvmStatic + fun data(): Collection> { + return Arrays.asList( + arrayOf( + Acyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallLine.first, + smallLine.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Acyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallCycle.first, + smallCycle.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + arrayOf( + Acyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallFull.first, + smallFull.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + arrayOf( + Cyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallLine.first, + smallLine.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + arrayOf( + Cyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallCycle.first, + smallCycle.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Cyclic(BasicRelation("po")), + Pattern2ExprCompiler(), + smallFull.first, + smallFull.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Reflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallLine.first, + smallLine.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + arrayOf( + Reflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallCycle.first, + smallCycle.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + arrayOf( + Reflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallFull.first, + smallFull.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Irreflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallLine.first, + smallLine.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Irreflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallCycle.first, + smallCycle.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + true + ), + arrayOf( + Irreflexive(BasicRelation("po")), + Pattern2ExprCompiler(), + smallFull.first, + smallFull.second, + SATGraphSolver(Z3SolverFactory.getInstance().createSolver()), + false + ), + ) + } + } +} \ No newline at end of file diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/Utils.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/Utils.kt index aecfc59710..fe9948f0ff 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/Utils.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/Utils.kt @@ -18,7 +18,9 @@ package hu.bme.mit.theta.c2xcfa import hu.bme.mit.theta.c.frontend.dsl.gen.CLexer import hu.bme.mit.theta.c.frontend.dsl.gen.CParser +import hu.bme.mit.theta.frontend.CStatistics import hu.bme.mit.theta.frontend.ParseContext +import hu.bme.mit.theta.frontend.getStatistics import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor import hu.bme.mit.theta.frontend.transformation.model.statements.CProgram import hu.bme.mit.theta.xcfa.model.XCFA @@ -27,7 +29,8 @@ import org.antlr.v4.runtime.CharStreams import org.antlr.v4.runtime.CommonTokenStream import java.io.InputStream -fun getXcfaFromC(stream: InputStream, parseContext: ParseContext, checkOverflow: Boolean): XCFA { +fun getXcfaFromC(stream: InputStream, parseContext: ParseContext, collectStatistics: Boolean, + checkOverflow: Boolean): Triple?> { val input = CharStreams.fromStream(stream) val lexer = CLexer(input) val tokens = CommonTokenStream(lexer) @@ -40,5 +43,26 @@ fun getXcfaFromC(stream: InputStream, parseContext: ParseContext, checkOverflow: val frontendXcfaBuilder = FrontendXcfaBuilder(parseContext, checkOverflow) val builder = frontendXcfaBuilder.buildXcfa(program) - return builder.build() + val xcfa = builder.build() + + if (collectStatistics) { + val programStatistics = try { + program.getStatistics() + } catch (_: Exception) { + CStatistics(0, emptyList()) + } + val unoptimizedXcfaStatistics = try { + builder.getStatistics() + } catch (_: Exception) { + XcfaStatistics(0, emptyList()) + } + val optimizedXcfaStatistics = try { + xcfa.getStatistics() + } catch (_: Exception) { + XcfaStatistics(0, emptyList()) + } + return Triple(xcfa, programStatistics, Pair(unoptimizedXcfaStatistics, optimizedXcfaStatistics)) + } + + return Triple(xcfa, null, null) } \ No newline at end of file diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/XcfaStatistics.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/XcfaStatistics.kt new file mode 100644 index 0000000000..46ace221b6 --- /dev/null +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/XcfaStatistics.kt @@ -0,0 +1,66 @@ +/* + * Copyright 2023 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.c2xcfa + +import hu.bme.mit.theta.xcfa.collectHavocs +import hu.bme.mit.theta.xcfa.model.XCFA +import hu.bme.mit.theta.xcfa.model.XcfaBuilder + +data class XcfaStatistics( + val globalVars: Int, + val procedures: Collection +) + +data class XcfaProcedureStatistics( + val localVariables: Int, + val locations: Int, + val edges: Int, + val havocs: Int, + val cyclComplexity: Int, + val hasFinalLoc: Boolean, +) + +fun XCFA.getStatistics(): XcfaStatistics { + return XcfaStatistics( + globalVars = vars.size, + procedures = procedures.map { + XcfaProcedureStatistics( + localVariables = it.vars.size, + locations = it.locs.size, + edges = it.edges.size, + havocs = it.edges.map { it.label.collectHavocs().size }.reduce(Int::plus), + cyclComplexity = it.edges.size - it.locs.size + 2, + hasFinalLoc = it.finalLoc.isPresent + ) + } + ) +} + +fun XcfaBuilder.getStatistics(): XcfaStatistics { + return XcfaStatistics( + globalVars = this.getVars().size, + procedures = getProcedures().map { + XcfaProcedureStatistics( + localVariables = it.getVars().size, + locations = it.getLocs().size, + edges = it.getEdges().size, + havocs = it.getEdges().map { it.label.collectHavocs().size }.reduce(Int::plus), + cyclComplexity = it.getEdges().size - it.getLocs().size + 2, + hasFinalLoc = it.finalLoc.isPresent + ) + } + ) +} \ No newline at end of file diff --git a/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt index 6848584572..975edddde5 100644 --- a/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt @@ -67,6 +67,6 @@ class TestFrontendXcfaBuilder { val stream = javaClass.getResourceAsStream(filepath) - getXcfaFromC(stream!!, ParseContext(), false) + getXcfaFromC(stream!!, ParseContext(), false, false) } } \ No newline at end of file diff --git a/subprojects/xcfa/cat/build.gradle.kts b/subprojects/xcfa/cat/build.gradle.kts index d92b00bf82..9077cc19ac 100644 --- a/subprojects/xcfa/cat/build.gradle.kts +++ b/subprojects/xcfa/cat/build.gradle.kts @@ -14,8 +14,9 @@ * limitations under the License. */ plugins { - id("java-common") id("antlr-grammar") + id("java-common") + id("kotlin-common") id("jacoco-common") } @@ -26,4 +27,12 @@ dependencies { implementation(project(":theta-core")) implementation(project(":theta-solver")) implementation(project(":theta-solver-z3")) + implementation(project(":theta-graph-solver")) +} +tasks.named("compileKotlin") { + dependsOn("generateGrammarSource") } +tasks.named("compileTestKotlin") { + dependsOn("generateTestGrammarSource") +} + diff --git a/subprojects/xcfa/cat/src/main/antlr/Cat.g4 b/subprojects/xcfa/cat/src/main/antlr/Cat.g4 index 5e5303af0f..e47e3515c4 100644 --- a/subprojects/xcfa/cat/src/main/antlr/Cat.g4 +++ b/subprojects/xcfa/cat/src/main/antlr/Cat.g4 @@ -8,7 +8,7 @@ name: (QUOT? NAME+ QUOT?) ; scopeBody - : (procCall | functionDef | procDef | definition | includeFile)+ + : (procCall | functionDef | procDef | definition | includeFile)* ; procCall diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatDslManager.java b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatDslManager.java index ef2c06cd5f..c17f2f3153 100644 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatDslManager.java +++ b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatDslManager.java @@ -18,7 +18,7 @@ import hu.bme.mit.theta.cat.dsl.gen.CatLexer; import hu.bme.mit.theta.cat.dsl.gen.CatParser; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCM; +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CommonTokenStream; @@ -26,10 +26,11 @@ import java.io.File; import java.io.FileInputStream; import java.io.IOException; +import java.util.Collection; public class CatDslManager { - public static MCM createMCM(final File file) throws IOException { + public static Collection createMCM(final File file) throws IOException { final CatParser.McmContext context = setupCatAntlr(file); final hu.bme.mit.theta.cat.dsl.CatVisitor visitor = new hu.bme.mit.theta.cat.dsl.CatVisitor(file); context.accept(visitor); diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.java b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.java deleted file mode 100644 index 5bb22af6d4..0000000000 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.java +++ /dev/null @@ -1,332 +0,0 @@ -/* - * Copyright 2023 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.cat.dsl; - -import hu.bme.mit.theta.analysis.algorithm.mcm.MCM; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMConstraint; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; -import hu.bme.mit.theta.analysis.algorithm.mcm.rules.*; -import hu.bme.mit.theta.cat.dsl.gen.CatBaseVisitor; -import hu.bme.mit.theta.cat.dsl.gen.CatParser; - -import java.io.File; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; - -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.cat.dsl.CatDslManager.setupCatAntlr; -import static java.lang.Character.isUpperCase; - -public class CatVisitor extends CatBaseVisitor { - private MCM mcm; - private int ruleNameCnt = 0; - private final File file; - private final Map relations; - private final Map functions; - private final Map procedures; - private final Map paramAssignment; - - public CatVisitor(final File file) { - this.relations = new LinkedHashMap<>(); - this.procedures = new LinkedHashMap<>(); - this.functions = new LinkedHashMap<>(); - this.paramAssignment = new LinkedHashMap<>(); - this.file = file; - } - - public MCM getMcm() { - return mcm; - } - - private MCMRelation getOrCreateRelation(final String name, final int arity) { - if (paramAssignment.containsKey(name)) { - final MCMRelation mcmRelation = paramAssignment.get(name); - return mcmRelation; - } - if (relations.containsKey(name)) { - final MCMRelation mcmRelation = relations.get(name); - return mcmRelation; - } - final MCMRelation relation = new MCMRelation(arity, name); - relations.put(name, relation); - return relation; - } - - @Override - public MCMRelation visitMcm(CatParser.McmContext ctx) { - this.mcm = new MCM(ctx.name() == null ? "Unnamed" : ctx.name().getText()); - - final File file = new File(this.file.getParent() + File.separator + "stdlib.cat"); - visitIncludedFile(file); - - return super.visitMcm(ctx); - } - - private void visitIncludedFile(File file) { - if (file.exists() && file.isFile()) { - try { - final CatParser.McmContext context = setupCatAntlr(file); - context.scopeBody().accept(this); - } catch (IOException e) { - e.printStackTrace(); - } - } else throw new RuntimeException(new FileNotFoundException(file.getAbsolutePath())); - } - - @Override - public MCMRelation visitIncludeFile(CatParser.IncludeFileContext ctx) { - final File file = new File(this.file.getParent() + File.separator + ctx.file.getText()); - visitIncludedFile(file); - return null; - } - - @Override - public MCMRelation visitAcyclicDefinition(CatParser.AcyclicDefinitionContext ctx) { - final MCMRelation rule = ctx.e.accept(this); - mcm.addConstraint(new MCMConstraint(rule, ctx.negate == null ? MCMConstraint.ConstraintType.ACYCLIC : MCMConstraint.ConstraintType.CYCLIC)); - return null; - } - - @Override - public MCMRelation visitIrreflexiveDefinition(CatParser.IrreflexiveDefinitionContext ctx) { - final MCMRelation rule = ctx.e.accept(this); - mcm.addConstraint(new MCMConstraint(rule, ctx.negate == null ? MCMConstraint.ConstraintType.IRREFLEXIVE : MCMConstraint.ConstraintType.REFLEXIVE)); - return null; - } - - @Override - public MCMRelation visitEmptyDefinition(CatParser.EmptyDefinitionContext ctx) { - final MCMRelation rule = ctx.e.accept(this); - mcm.addConstraint(new MCMConstraint(rule, ctx.negate == null ? MCMConstraint.ConstraintType.EMPTY : MCMConstraint.ConstraintType.NOTEMPTY)); - return null; - } - - @Override - public MCMRelation visitFunctionDef(CatParser.FunctionDefContext ctx) { - functions.put(ctx.n.getText(), ctx); - return null; - } - - @Override - public MCMRelation visitProcDef(CatParser.ProcDefContext ctx) { - procedures.put(ctx.n.getText(), ctx); - return null; - } - - @Override - public MCMRelation visitExprToid(CatParser.ExprToidContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("toid" + ruleNameCnt++, 2); - relation.addRule(new Toid(rel)); - return relation; - } - - @Override - public MCMRelation visitExprRange(CatParser.ExprRangeContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("range" + ruleNameCnt++, 1); - relation.addRule(new Range(rel)); - return relation; - } - - @Override - public MCMRelation visitExprDomain(CatParser.ExprDomainContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("domain" + ruleNameCnt++, 1); - relation.addRule(new Domain(rel)); - return relation; - } - - @Override - public MCMRelation visitProcCall(CatParser.ProcCallContext ctx) { - final CatParser.ProcDefContext procDefContext = procedures.get(ctx.NAME().getText()); - checkNotNull(procDefContext, "Procedure with name " + ctx.NAME().getText() + " does not exist."); - final List e = ctx.params; - final Map toReset = new LinkedHashMap<>(); - for (int i = 0; i < e.size(); i++) { - final String text = procDefContext.params.get(i).getText(); - CatParser.ExpressionContext expressionContext = e.get(i); - toReset.put(text, paramAssignment.get(text)); - paramAssignment.put( - text, - expressionContext.accept(this)); - } - final MCMRelation accept = procDefContext.body.accept(this); - toReset.forEach((s, mcmRelation) -> { - if (mcmRelation == null) paramAssignment.remove(s); - else paramAssignment.put(s, mcmRelation); - }); - return accept; - } - - @Override - public MCMRelation visitExprTryWith(CatParser.ExprTryWithContext ctx) { - return ctx.e.accept(this); - } - - @Override - public MCMRelation visitExprFunctionCall(CatParser.ExprFunctionCallContext ctx) { - final CatParser.FunctionDefContext functionDefContext = functions.get(ctx.NAME().getText()); - checkNotNull(functionDefContext, "Function with name " + ctx.NAME().getText() + " does not exist."); - List e = ctx.e; - final Map toReset = new LinkedHashMap<>(); - for (int i = 0; i < e.size(); i++) { - final String text = functionDefContext.params.get(i).getText(); - CatParser.ExpressionContext expressionContext = e.get(i); - toReset.put(text, paramAssignment.get(text)); - paramAssignment.put( - text, - expressionContext.accept(this)); - } - final MCMRelation accept = functionDefContext.e.accept(this); - toReset.forEach((s, mcmRelation) -> { - if (mcmRelation == null) paramAssignment.remove(s); - else paramAssignment.put(s, mcmRelation); - }); - return accept; - } - - @Override - public MCMRelation visitLetDefinition(CatParser.LetDefinitionContext ctx) { - String name = ctx.NAME().getText(); - CatParser.ExpressionContext eCtx = ctx.e; - - relations.remove(name); - for (CatParser.LetAndDefinitionContext letAndDefinitionContext : ctx.letAndDefinition()) { - name = letAndDefinitionContext.NAME().getText(); - relations.remove(name); - } - MCMRelation rel = eCtx.accept(this); - final MCMRelation relation = getOrCreateRelation(ctx.NAME().getText(), rel.getArity()); - relation.addRule(new Self(rel)); - for (CatParser.LetAndDefinitionContext letAndDefinitionContext : ctx.letAndDefinition()) { - name = letAndDefinitionContext.NAME().getText(); - eCtx = letAndDefinitionContext.e; - rel = eCtx.accept(this); - - final MCMRelation relationAnd = getOrCreateRelation(name, rel.getArity()); - relationAnd.addRule(new Self(rel)); - } - - return relation; - } - - @Override - public MCMRelation visitExprCartesian(CatParser.ExprCartesianContext ctx) { - MCMRelation rel = ctx.e1.accept(this); - final MCMRelation relation = getOrCreateRelation("cartesian" + ruleNameCnt++, 2); - relation.addRule(new CartesianProduct(rel, ctx.e2.accept(this))); - return relation; - } - - @Override - public MCMRelation visitExprBasic(CatParser.ExprBasicContext ctx) { - return getOrCreateRelation(ctx.NAME().getText(), isUpperCase(ctx.NAME().getText().charAt(0)) ? 1 : 2); - } - - @Override - public MCMRelation visitExprMinus(CatParser.ExprMinusContext ctx) { - MCMRelation rel = ctx.e1.accept(this); - final MCMRelation relation = getOrCreateRelation("minus" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Difference(rel, ctx.e2.accept(this))); - return relation; - } - - @Override - public MCMRelation visitExprUnion(CatParser.ExprUnionContext ctx) { - MCMRelation rel = ctx.e1.accept(this); - final MCMRelation relation = getOrCreateRelation("union" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Union(rel, ctx.e2.accept(this))); - return relation; - } - - @Override - public MCMRelation visitExprComposition(CatParser.ExprCompositionContext ctx) { - MCMRelation rel = ctx.e1.accept(this); - final MCMRelation relation = getOrCreateRelation("composition" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Sequence(rel, ctx.e2.accept(this))); - return relation; - } - - @Override - public MCMRelation visitExprIntersection(CatParser.ExprIntersectionContext ctx) { - MCMRelation rel = ctx.e1.accept(this); - final MCMRelation relation = getOrCreateRelation("intersection" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Intersection(rel, ctx.e2.accept(this))); - return relation; - } - - @Override - public MCMRelation visitExprTransitive(CatParser.ExprTransitiveContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("transitive" + ruleNameCnt++, rel.getArity()); - relation.addRule(new TransitiveClosure(rel)); - return relation; - } - - @Override - public MCMRelation visitExprComplement(CatParser.ExprComplementContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("complement" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Complement(rel)); - return relation; - } - - @Override - public MCMRelation visitExprInverse(CatParser.ExprInverseContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("inverse" + ruleNameCnt++, rel.getArity()); - relation.addRule(new Inverse(rel)); - return relation; - } - - @Override - public MCMRelation visitExprTransRef(CatParser.ExprTransRefContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("transref" + ruleNameCnt++, rel.getArity()); - relation.addRule(new ReflexiveTransitiveClosure(rel)); - return relation; - } - - @Override - public MCMRelation visitExpr(CatParser.ExprContext ctx) { - return ctx.e.accept(this); - } - - @Override - public MCMRelation visitExprOptional(CatParser.ExprOptionalContext ctx) { - MCMRelation rel = ctx.e.accept(this); - final MCMRelation relation = getOrCreateRelation("optional" + ruleNameCnt++, rel.getArity()); - relation.addRule(new IdentityClosure(rel)); - return relation; - } - - @Override - public MCMRelation visitExprNull(CatParser.ExprNullContext ctx) { - final MCMRelation relation = getOrCreateRelation("null" + ruleNameCnt++, 1); - relation.addRule(new EmptyRelation()); - return relation; - } - - @Override - public String toString() { - return mcm.toString(); - } -} diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.kt b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.kt new file mode 100644 index 0000000000..d5b3ea26df --- /dev/null +++ b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/dsl/CatVisitor.kt @@ -0,0 +1,270 @@ +/* + * Copyright 2023 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.cat.dsl + +import com.google.common.base.Preconditions +import hu.bme.mit.theta.cat.dsl.gen.CatBaseVisitor +import hu.bme.mit.theta.cat.dsl.gen.CatParser +import hu.bme.mit.theta.cat.dsl.gen.CatParser.* +import hu.bme.mit.theta.graphsolver.patterns.constraints.* +import hu.bme.mit.theta.graphsolver.patterns.patterns.* +import java.io.File +import java.io.FileNotFoundException +import java.io.IOException + +class CatVisitor(file: File) : CatBaseVisitor() { + + private var mcm: MutableList? = null + private val ruleNameCnt = 0 + private val file: File + private val relations: MutableMap + private val functions: MutableMap + private val procedures: MutableMap + private val paramAssignment: MutableMap + + init { + relations = LinkedHashMap() + procedures = LinkedHashMap() + functions = LinkedHashMap() + paramAssignment = LinkedHashMap() + this.file = file + } + + fun getMcm(): Collection? { + return mcm + } + + private fun getOrCreateRelation(name: String, arity: Int): GraphPattern? { + if (paramAssignment.containsKey(name)) { + return paramAssignment[name] + } + if (relations.containsKey(name)) { + return relations[name] + } + return if (arity == 1) BasicEventSet(name) else BasicRelation(name) + } + + override fun visitMcm(ctx: McmContext): GraphPattern { + mcm = ArrayList() + val file = File(file.parent + File.separator + "stdlib.cat") + visitIncludedFile(file) + return super.visitMcm(ctx) ?: EmptyRel + } + + private fun visitIncludedFile(file: File) { + if (file.exists() && file.isFile) { + try { + val context = CatDslManager.setupCatAntlr(file) + context.scopeBody().accept(this) + } catch (e: IOException) { + e.printStackTrace() + } + } else throw RuntimeException(FileNotFoundException(file.absolutePath)) + } + + override fun visitIncludeFile(ctx: IncludeFileContext): GraphPattern { + val file = File(file.parent + File.separator + ctx.file.text) + visitIncludedFile(file) + return EmptyRel + } + + override fun visitAcyclicDefinition(ctx: AcyclicDefinitionContext): GraphPattern { + val rule = ctx.e.accept(this) as EdgePattern + mcm!!.add(if (ctx.negate == null) Acyclic(rule) else Cyclic(rule)) + return EmptyRel + } + + override fun visitIrreflexiveDefinition(ctx: IrreflexiveDefinitionContext): GraphPattern { + val rule = ctx.e.accept(this) as EdgePattern + mcm!!.add(if (ctx.negate == null) Irreflexive(rule) else Reflexive(rule)) + return EmptyRel + } + + override fun visitEmptyDefinition(ctx: EmptyDefinitionContext): GraphPattern { + val rule = ctx.e.accept(this) + mcm!!.add(if (ctx.negate == null) Empty(rule) else Nonempty(rule)) + return EmptyRel + } + + override fun visitFunctionDef(ctx: FunctionDefContext): GraphPattern { + functions[ctx.n.text] = ctx + return EmptyRel + } + + override fun visitProcDef(ctx: ProcDefContext): GraphPattern { + procedures[ctx.n.text] = ctx + return EmptyRel + } + + override fun visitExprToid(ctx: ExprToidContext): GraphPattern { + val rel = ctx.e.accept(this) as NodePattern + return Toid(rel) + } + + override fun visitExprRange(ctx: ExprRangeContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return Range(rel) + } + + override fun visitExprDomain(ctx: ExprDomainContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return Domain(rel) + } + + override fun visitProcCall(ctx: ProcCallContext): GraphPattern { + val procDefContext = procedures[ctx.NAME().text] + Preconditions.checkNotNull(procDefContext, "Procedure with name " + ctx.NAME().text + " does not exist.") + val e = ctx.params + val toReset: MutableMap = LinkedHashMap() + for (i in e.indices) { + val text = procDefContext!!.params[i].text + val expressionContext = e[i] + toReset[text] = paramAssignment[text] + paramAssignment[text] = expressionContext.accept(this) + } + val accept = procDefContext!!.body.accept(this) + toReset.forEach { (s: String, graphPattern: GraphPattern?) -> + if (graphPattern == null) paramAssignment.remove(s) else paramAssignment[s] = graphPattern + } + return accept + } + + override fun visitExprTryWith(ctx: ExprTryWithContext): GraphPattern { + return ctx.e.accept(this) + } + + override fun visitExprFunctionCall(ctx: ExprFunctionCallContext): GraphPattern { + val functionDefContext = functions[ctx.NAME().text] + Preconditions.checkNotNull(functionDefContext, "Function with name " + ctx.NAME().text + " does not exist.") + val e = ctx.e + val toReset: MutableMap = LinkedHashMap() + for (i in e.indices) { + val text = functionDefContext!!.params[i].text + val expressionContext = e[i] + toReset[text] = paramAssignment[text] + paramAssignment[text] = expressionContext.accept(this) + } + val accept = functionDefContext!!.e.accept(this) + toReset.forEach { (s: String, graphPattern: GraphPattern?) -> + if (graphPattern == null) paramAssignment.remove(s) else paramAssignment[s] = graphPattern + } + return accept + } + + override fun visitLetDefinition(ctx: LetDefinitionContext): GraphPattern { + var name = ctx.NAME().text + var eCtx = ctx.e + relations.remove(name) + for (letAndDefinitionContext in ctx.letAndDefinition()) { + name = letAndDefinitionContext.NAME().text + relations.remove(name) + } + var rel = eCtx.accept(this) + rel.patternName = ctx.NAME().text + relations[ctx.NAME().text] = rel + for (letAndDefinitionContext in ctx.letAndDefinition()) { + name = letAndDefinitionContext.NAME().text + eCtx = letAndDefinitionContext.e + rel = eCtx.accept(this) + relations[name] = rel + } + return rel + } + + override fun visitExprCartesian(ctx: ExprCartesianContext): GraphPattern { + val rel1 = ctx.e1.accept(this) as NodePattern + val rel2 = ctx.e2.accept(this) as NodePattern + return CartesianProduct(rel1, rel2) + } + + override fun visitExprBasic(ctx: ExprBasicContext): GraphPattern { + return getOrCreateRelation(ctx.NAME().text, if (Character.isLowerCase(ctx.NAME().text[0])) 2 else 1)!! + } + + override fun visitExprMinus(ctx: ExprMinusContext): GraphPattern { + val rel1 = ctx.e1.accept(this) + val rel2 = ctx.e2.accept(this) + return if (rel1 is EdgePattern && rel2 is EdgePattern) + Difference(rel1, rel2) + else if (rel1 is NodePattern && rel2 is NodePattern) + DifferenceNode(rel1, rel2) + else error("Mismatched types") + } + + override fun visitExprUnion(ctx: ExprUnionContext): GraphPattern { + val rel1 = ctx.e1.accept(this) + val rel2 = ctx.e2.accept(this) + return if (rel1 is EdgePattern && rel2 is EdgePattern) + Union(rel1, rel2) + else if (rel1 is NodePattern && rel2 is NodePattern) + UnionNode(rel1, rel2) + else error("Mismatched types") + } + + override fun visitExprComposition(ctx: ExprCompositionContext): GraphPattern { + val rel1 = ctx.e1.accept(this) as EdgePattern + val rel2 = ctx.e2.accept(this) as EdgePattern + return Sequence(rel1, rel2) + } + + override fun visitExprIntersection(ctx: ExprIntersectionContext): GraphPattern { + val rel1 = ctx.e1.accept(this) + val rel2 = ctx.e2.accept(this) + return if (rel1 is EdgePattern && rel2 is EdgePattern) + Intersection(rel1, rel2) + else if (rel1 is NodePattern && rel2 is NodePattern) + IntersectionNode(rel1, rel2) + else error("Mismatched types") + } + + override fun visitExprTransitive(ctx: ExprTransitiveContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return TransitiveClosure(rel) + } + + override fun visitExprComplement(ctx: ExprComplementContext): GraphPattern { + val rel = ctx.e.accept(this) + return if (rel is EdgePattern) Complement(rel) else if (rel is NodePattern) ComplementNode(rel) else error( + "Mismatched types") + } + + override fun visitExprInverse(ctx: ExprInverseContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return Inverse(rel) + } + + override fun visitExprTransRef(ctx: ExprTransRefContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return ReflexiveTransitiveClosure(rel) + } + + override fun visitExpr(ctx: CatParser.ExprContext): GraphPattern { + return ctx.e.accept(this) + } + + override fun visitExprOptional(ctx: ExprOptionalContext): GraphPattern { + val rel = ctx.e.accept(this) as EdgePattern + return IdentityClosure(rel) + } + + override fun visitExprNull(ctx: ExprNullContext): GraphPattern { + return EmptyRel + } + + override fun toString(): String { + return mcm.toString() + } +} \ No newline at end of file diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMConstraint.java b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMConstraint.java deleted file mode 100644 index 4f800f9d39..0000000000 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMConstraint.java +++ /dev/null @@ -1,49 +0,0 @@ -/* - * Copyright 2023 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.cat.mcm; - -public class MCMConstraint { - private final MCMRelation relation; - private final ConstraintType constraintType; - - public MCMConstraint(MCMRelation relation, ConstraintType constraintType) { - this.relation = relation; - this.constraintType = constraintType; - } - - public MCMRelation getRelation() { - return relation; - } - - public ConstraintType getConstraintType() { - return constraintType; - } - - public enum ConstraintType { - EMPTY, NOTEMPTY, - ACYCLIC, CYCLIC, - IRREFLEXIVE, REFLEXIVE - } - - @Override - public String toString() { - return "MCMConstraint{" + - "relation=" + relation + - ", constraintType=" + constraintType + - '}'; - } -} diff --git a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRelation.java b/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRelation.java deleted file mode 100644 index b7b84b8813..0000000000 --- a/subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/mcm/MCMRelation.java +++ /dev/null @@ -1,84 +0,0 @@ -/* - * Copyright 2023 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.cat.mcm; - -import hu.bme.mit.theta.common.TupleN; - -import java.util.Collection; -import java.util.LinkedHashSet; -import java.util.Map; - -public class MCMRelation { - private final int arity; - private final String name; - - private final Collection> facts; - private final Collection rules; - - public MCMRelation(int arity, String name) { - this.arity = arity; - this.name = name; - this.facts = new LinkedHashSet<>(); - this.rules = new LinkedHashSet<>(); - } - - public int getArity() { - return arity; - } - - public String getName() { - return name; - } - - public Collection> getFacts() { - return facts; - } - - public Collection getRules() { - return rules; - } - - public void addFact(final TupleN fact) { - facts.add(fact); - } - - public void addRule(final MCMRule rule) { - rules.add(rule); - } - - public void collectRelations(final Map relations) { - if (!relations.containsKey(name)) { - relations.put(name, this); - for (MCMRule rule : getRules()) { - rule.collectRelations(relations); - } - } else { - if (!relations.get(name).equals(this)) - throw new RuntimeException("Different definitions for the relation " + name); - } - } - - @Override - public String toString() { - return "MCMRelation{" + - "arity=" + arity + - ", name='" + name + '\'' + - ", facts=" + facts + - ", rules=" + rules + - '}'; - } -} diff --git a/subprojects/xcfa/cat/src/test/java/hu/bme/mit/theta/xcfa/cat/ParseTest.java b/subprojects/xcfa/cat/src/test/java/hu/bme/mit/theta/xcfa/cat/ParseTest.java index 84d0916a3e..c63b64b4bc 100644 --- a/subprojects/xcfa/cat/src/test/java/hu/bme/mit/theta/xcfa/cat/ParseTest.java +++ b/subprojects/xcfa/cat/src/test/java/hu/bme/mit/theta/xcfa/cat/ParseTest.java @@ -16,20 +16,19 @@ package hu.bme.mit.theta.xcfa.cat; import hu.bme.mit.theta.cat.dsl.CatDslManager; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCM; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCMRelation; +import hu.bme.mit.theta.graphsolver.compilers.DefaultGraphPatternCompiler; +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint; +import hu.bme.mit.theta.graphsolver.patterns.patterns.BasicEventSet; +import hu.bme.mit.theta.graphsolver.patterns.patterns.BasicRelation; +import hu.bme.mit.theta.graphsolver.patterns.patterns.GraphPattern; +import org.jetbrains.annotations.NotNull; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; import java.io.File; import java.io.IOException; -import java.util.Arrays; -import java.util.Collection; -import java.util.LinkedHashMap; -import java.util.Map; -import java.util.Set; -import java.util.stream.Collectors; +import java.util.*; import static org.junit.Assert.assertEquals; @@ -62,13 +61,24 @@ public static Collection data() { @Test public void test() throws IOException { try { - final MCM mcm = CatDslManager.createMCM(new File(getClass().getResource(filepath).getFile())); - assertEquals(constraintNumber, mcm.getConstraints().size()); - Map relations = new LinkedHashMap<>(); - mcm.getRelations().forEach((s, mcmRelation) -> mcmRelation.collectRelations(relations)); + final Collection mcm = CatDslManager.createMCM(new File(getClass().getResource(filepath).getFile())); + assertEquals(constraintNumber, mcm.size()); if (allowedPrimitives != null) { - final Map primitives = relations.entrySet().stream().filter(mcmRelation -> mcmRelation.getValue().getRule() == null).collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue)); - assertEquals(allowedPrimitives, primitives.keySet()); + Map basicElements = new LinkedHashMap<>(); + mcm.forEach(c -> c.accept(new DefaultGraphPatternCompiler() { + @Override + public Void compile(@NotNull BasicEventSet pattern) { + basicElements.put(pattern.getName(), pattern); + return super.compile(pattern); + } + + @Override + public Void compile(@NotNull BasicRelation pattern) { + basicElements.put(pattern.getPatternName(), pattern); + return super.compile(pattern); + } + })); + assertEquals(allowedPrimitives, basicElements.keySet()); } } catch (IOException e) { throw new IOException(filepath, e); diff --git a/subprojects/xcfa/exec-graph-cli/README.md b/subprojects/xcfa/exec-graph-cli/README.md new file mode 100644 index 0000000000..f87f5c14cb --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/README.md @@ -0,0 +1 @@ +# TODO \ No newline at end of file diff --git a/subprojects/xcfa/exec-graph-cli/build.gradle.kts b/subprojects/xcfa/exec-graph-cli/build.gradle.kts new file mode 100644 index 0000000000..ef6623886e --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/build.gradle.kts @@ -0,0 +1,36 @@ +/* + * Copyright 2023 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("java-common") + id("antlr-grammar") + id("cli-tool") +} + +dependencies { + implementation(project(":theta-core")) + implementation(project(":theta-common")) + implementation(project(":theta-cat")) + implementation(project(":theta-analysis")) + implementation(project(":theta-solver")) + implementation(project(":theta-solver-z3")) + implementation(project(":theta-solver-smtlib")) + implementation(project(":theta-graph-solver")) +} + + +application { + mainClassName = "hu.bme.mit.theta.xcfa.execgraph.cli.ExecutionGraphCli" +} diff --git a/subprojects/xcfa/exec-graph-cli/src/main/antlr/Graph.g4 b/subprojects/xcfa/exec-graph-cli/src/main/antlr/Graph.g4 new file mode 100644 index 0000000000..24f05bb9ce --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/main/antlr/Graph.g4 @@ -0,0 +1,66 @@ +grammar Graph; + +graph + : 'digraph' 'G' '{' nodes relations '}' + ; + +nodes + : node* + ; + +relations + : relation* + ; + +node: name=ID '[' .*? 'label="' eventID (';' labels)? '"' .*? '];' + ; + +eventID + : DigitSequence + ; + +labels + : label? (';' label)* + ; + +label + : ID + ; + +relation + : source=ID '->' target=ID '[' .*? 'label="' label '"' .*? '];' + ; + +ID : Letter+ (Letter | Digit)* + ; + +DigitSequence + : Digit+ + ; + +fragment +Digit + : [0-9] + ; + +fragment +Letter + : [A-Za-z] + ; + +Whitespace + : [ \t]+ + -> skip + ; + +Newline + : ( '\r' '\n'? + | '\n' + ) + -> skip + ; + +BlockComment + : '(*' .*? '*)' + -> skip + ; diff --git a/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/ExecutionGraphCli.java b/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/ExecutionGraphCli.java new file mode 100644 index 0000000000..c0b7bd01dc --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/ExecutionGraphCli.java @@ -0,0 +1,145 @@ +/* + * Copyright 2023 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.execgraph.cli; + +import com.beust.jcommander.JCommander; +import com.beust.jcommander.Parameter; +import com.beust.jcommander.ParameterException; +import com.google.common.base.Stopwatch; +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.CandidateExecutionGraph; +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.PartialSolver; +import hu.bme.mit.theta.cat.dsl.CatDslManager; +import hu.bme.mit.theta.common.CliUtils; +import hu.bme.mit.theta.common.OsHelper; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.graphsolver.compilers.pattern2expr.Pattern2ExprCompiler; +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint; +import hu.bme.mit.theta.graphsolver.solvers.SATGraphSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverManager; +import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; +import hu.bme.mit.theta.solver.z3.Z3SolverManager; + +import java.io.File; +import java.nio.file.Path; +import java.util.Collection; +import java.util.concurrent.TimeUnit; + +public class ExecutionGraphCli { + private static final String JAR_NAME = "theta-exec-graph-cli.jar"; + private final String[] args; + + //////////// CONFIGURATION OPTIONS BEGIN //////////// + + //////////// input task //////////// + + @Parameter(names = "--graph", description = "Path of the partial graph (graphviz)", required = true) + File graph; + + @Parameter(names = "--cat", description = "Path of the cat model", required = true) + File cat; + + //////////// output data and statistics //////////// + + @Parameter(names = "--version", description = "Display version", help = true) + boolean versionInfo = false; + + @Parameter(names = "--loglevel", description = "Detailedness of logging") + Logger.Level logLevel = Logger.Level.MAINSTEP; + + //////////// SMTLib options //////////// + + @Parameter(names = "--smt-home", description = "The path of the solver registry") + String home = SmtLibSolverManager.HOME.toAbsolutePath().toString(); + + @Parameter(names = "--solver", description = "Sets the underlying SMT solver to use. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.") + String solver = "Z3"; + + //////////// CONFIGURATION OPTIONS END //////////// + + public ExecutionGraphCli(final String[] args) { + this.args = args; + } + + public static void main(final String[] args) { + final ExecutionGraphCli mainApp = new ExecutionGraphCli(args); + mainApp.run(); + } + + private void run() { + /// Checking flags + try { + JCommander.newBuilder().addObject(this).programName(JAR_NAME).build().parse(args); + } catch (final ParameterException ex) { + System.out.println("Invalid parameters, details:"); + System.out.println(ex.getMessage()); + ex.usage(); + return; + } + + Logger logger = new ConsoleLogger(logLevel); + + /// version + if (versionInfo) { + CliUtils.printVersion(System.out); + return; + } + + try { + registerAllSolverManagers(home, logger); + } catch (Exception e) { + e.printStackTrace(); + return; + } + + + final Stopwatch sw = Stopwatch.createStarted(); + try (Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver()) { + final Collection mcm = CatDslManager.createMCM(cat); + logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n"); + + final CandidateExecutionGraph partialGraph = PartialGraphVisitor.getPartialGraph(this.graph); + logger.write(Logger.Level.MAINSTEP, "Partial graph parsed successfully\n"); + + var partialSolver = new PartialSolver<>(mcm, partialGraph, new Pattern2ExprCompiler(), new SATGraphSolver(solver)); + var solution = partialSolver.getSolution(); + logger.write(Logger.Level.MAINSTEP, "Solution ready:\n"); + if (solution != null) { + logger.write(Logger.Level.RESULT, "Solution: " + solution + "\n"); + } else { + logger.write(Logger.Level.RESULT, "No such solution exists.\n"); + } + } catch (final Throwable t) { + t.printStackTrace(); + System.exit(-1); + } + long elapsed = sw.elapsed(TimeUnit.MILLISECONDS); + sw.stop(); + System.out.println("walltime: " + elapsed + " ms"); + } + + public static void registerAllSolverManagers(String home, Logger logger) throws Exception { + SolverManager.closeAll(); + SolverManager.registerSolverManager(Z3SolverManager.create()); + if (OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) { + final var homePath = Path.of(home); + final var smtLibSolverManager = SmtLibSolverManager.create(homePath, logger); + SolverManager.registerSolverManager(smtLibSolverManager); + } + } + +} \ No newline at end of file diff --git a/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/PartialGraphVisitor.java b/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/PartialGraphVisitor.java new file mode 100644 index 0000000000..86caeb5d5b --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/main/java/hu/bme/mit/theta/xcfa/execgraph/cli/PartialGraphVisitor.java @@ -0,0 +1,110 @@ +/* + * Copyright 2023 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.execgraph.cli; + +import com.google.common.base.Preconditions; +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.CandidateExecutionGraph; +import hu.bme.mit.theta.common.Tuple; +import hu.bme.mit.theta.common.Tuple1; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.exec.graph.cli.dsl.gen.GraphBaseVisitor; +import hu.bme.mit.theta.exec.graph.cli.dsl.gen.GraphLexer; +import hu.bme.mit.theta.exec.graph.cli.dsl.gen.GraphParser; +import hu.bme.mit.theta.graphsolver.ThreeVL; +import kotlin.Pair; +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; + +import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.Map; +import java.util.Set; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class PartialGraphVisitor extends GraphBaseVisitor { + private final Map events = new LinkedHashMap<>(); + private final Set relations = new LinkedHashSet<>(); + private final Set sets = new LinkedHashSet<>(); + private final Set> positiveFacts = new LinkedHashSet<>(); + + @Override + public Void visitNode(GraphParser.NodeContext ctx) { + var id = Integer.parseInt(ctx.eventID().getText()); + Preconditions.checkState(!events.containsValue(id), "Already existing event IDs cannot be added."); + events.put(ctx.name.getText(), id); + if (ctx.labels() != null) { + for (GraphParser.LabelContext labelContext : ctx.labels().label()) { + var label = labelContext.ID().getText(); + sets.add(label); + positiveFacts.add(new Pair<>(label, Tuple1.of(id))); + } + } + return null; + } + + @Override + public Void visitRelation(GraphParser.RelationContext ctx) { + var fromId = events.get(ctx.source.getText()); + checkNotNull(fromId, "Source event not known for " + ctx.getText()); + var toId = events.get(ctx.target.getText()); + checkNotNull(toId, "Taret event not known for " + ctx.getText()); + + var label = ctx.label().getText(); + relations.add(label); + positiveFacts.add(new Pair<>(label, Tuple2.of(fromId, toId))); + return null; + } + + public static CandidateExecutionGraph getPartialGraph(final File file) throws IOException { + FileInputStream inputStream = new FileInputStream(file); + final CharStream input = CharStreams.fromStream(inputStream); + + final GraphLexer lexer = new GraphLexer(input); + final CommonTokenStream tokens = new CommonTokenStream(lexer); + final GraphParser parser = new GraphParser(tokens); + inputStream.close(); + + var partialGraphVisitor = new PartialGraphVisitor(); + parser.graph().accept(partialGraphVisitor); + Map, ThreeVL> facts = new LinkedHashMap<>(); + var eventList = partialGraphVisitor.events.values().stream().toList(); + for (Integer a : eventList) { + for (String set : partialGraphVisitor.sets) { + if (partialGraphVisitor.positiveFacts.contains(new Pair<>(set, Tuple1.of(a)))) { + facts.put(new Pair<>(set, Tuple1.of(a)), ThreeVL.TRUE); + } else { + facts.put(new Pair<>(set, Tuple1.of(a)), ThreeVL.FALSE); + } + } + for (Integer b : eventList) { + for (String relation : partialGraphVisitor.relations) { + if (partialGraphVisitor.positiveFacts.contains(new Pair<>(relation, Tuple2.of(a, b)))) { + facts.put(new Pair<>(relation, Tuple2.of(a, b)), ThreeVL.TRUE); + } else { + facts.put(new Pair<>(relation, Tuple2.of(a, b)), ThreeVL.FALSE); + } + } + } + } + return new CandidateExecutionGraph(partialGraphVisitor.events.values().stream().toList(), facts); + } +} diff --git a/subprojects/xcfa/exec-graph-cli/src/test/java/hu/bme/mit/theta/xcfa/execgraph/cli/ParseTest.java b/subprojects/xcfa/exec-graph-cli/src/test/java/hu/bme/mit/theta/xcfa/execgraph/cli/ParseTest.java new file mode 100644 index 0000000000..e7c3cba71a --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/test/java/hu/bme/mit/theta/xcfa/execgraph/cli/ParseTest.java @@ -0,0 +1,61 @@ +/* + * Copyright 2023 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.execgraph.cli; + +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.CandidateExecutionGraph; +import hu.bme.mit.theta.analysis.algorithm.mcm.analysis.PartialSolver; +import hu.bme.mit.theta.cat.dsl.CatDslManager; +import hu.bme.mit.theta.graphsolver.compilers.pattern2expr.Pattern2ExprCompiler; +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint; +import hu.bme.mit.theta.graphsolver.solvers.SATGraphSolver; +import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.File; +import java.io.IOException; +import java.util.Arrays; +import java.util.Collection; + +@RunWith(Parameterized.class) +public class ParseTest { + @Parameterized.Parameter(0) + public String modelPath; + + @Parameterized.Parameter(1) + public String catPath; + + @Parameterized.Parameters() + public static Collection data() { + return Arrays.asList(new Object[][]{ + {"/simple.dot", "/postar.cat"}, + }); + } + + @Test + public void test() throws IOException { + final File model = new File(getClass().getResource(modelPath).getFile()); + final File cat = new File(getClass().getResource(catPath).getFile()); + + final Collection mcm = CatDslManager.createMCM(cat); + + final CandidateExecutionGraph partialGraph = PartialGraphVisitor.getPartialGraph(model); + + var partialSolver = new PartialSolver<>(mcm, partialGraph, new Pattern2ExprCompiler(), new SATGraphSolver(Z3SolverFactory.getInstance().createSolver())); + var solution = partialSolver.getSolution(); + } +} diff --git a/subprojects/xcfa/exec-graph-cli/src/test/resources/postar.cat b/subprojects/xcfa/exec-graph-cli/src/test/resources/postar.cat new file mode 100644 index 0000000000..c7edc6b44c --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/test/resources/postar.cat @@ -0,0 +1,2 @@ +let po-star = co* +~empty po-star \ No newline at end of file diff --git a/subprojects/xcfa/exec-graph-cli/src/test/resources/simple.dot b/subprojects/xcfa/exec-graph-cli/src/test/resources/simple.dot new file mode 100644 index 0000000000..6df41a0a23 --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/test/resources/simple.dot @@ -0,0 +1,10 @@ +digraph G { + + a[label="1"]; + b[label="2"]; + c[label="3"]; + + a -> b [label="po"]; + b -> c [label="po"]; + +} \ No newline at end of file diff --git a/subprojects/xcfa/exec-graph-cli/src/test/resources/stdlib.cat b/subprojects/xcfa/exec-graph-cli/src/test/resources/stdlib.cat new file mode 100644 index 0000000000..a5a3fc01b3 --- /dev/null +++ b/subprojects/xcfa/exec-graph-cli/src/test/resources/stdlib.cat @@ -0,0 +1,9 @@ +STDLIB + +let po-loc = po & loc +let rfe = rf & ext +let rfi = rf & int + +let fencerel(B) = (po & (_ * B)) ; po + +let ctrlcfence(ctrl,CFENCE) = (ctrl & (_ * CFENCE)) ; po diff --git a/subprojects/xcfa/litmus-cli/build.gradle.kts b/subprojects/xcfa/litmus-cli/build.gradle.kts index 6960582bff..91315f2b04 100644 --- a/subprojects/xcfa/litmus-cli/build.gradle.kts +++ b/subprojects/xcfa/litmus-cli/build.gradle.kts @@ -30,6 +30,7 @@ dependencies { implementation(project(":theta-solver")) implementation(project(":theta-solver-z3")) implementation(project(":theta-solver-smtlib")) + implementation(project(":theta-graph-solver")) } application { diff --git a/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java b/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java index f8dff80b2b..9edc0eaf09 100644 --- a/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java +++ b/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java @@ -19,7 +19,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParameterException; import com.google.common.base.Stopwatch; -import hu.bme.mit.theta.analysis.algorithm.mcm.MCM; +import hu.bme.mit.theta.graphsolver.patterns.constraints.GraphConstraint; import hu.bme.mit.theta.cat.dsl.CatDslManager; import hu.bme.mit.theta.common.CliUtils; import hu.bme.mit.theta.common.OsHelper; @@ -35,6 +35,7 @@ import java.io.File; import java.nio.file.Path; import java.util.ArrayList; +import java.util.Collection; import java.util.List; import java.util.concurrent.TimeUnit; @@ -119,13 +120,15 @@ private void run() { try { try (Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver()) { - final MCM mcm = CatDslManager.createMCM(cat); + final Collection mcm = CatDslManager.createMCM(cat); logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n"); final XCFA xcfa = LitmusInterpreter.getXcfa(litmus); logger.write(Logger.Level.MAINSTEP, "Litmus test parsed successfully\n"); if (printxcfa) { - System.out.println(toDot(xcfa)); + System.out.println("digraph G{"); + //TODO visualize + System.out.println("}"); } // final List processIds = listToRange(processes, -1, -1); @@ -136,6 +139,14 @@ private void run() { // final MultiprocTransFunc, XcfaProcessAction, ExplPrec> multiprocTransFunc = new MultiprocTransFunc<>(processIds.stream().map(id -> Map.entry(id, new XcfaProcessTransFunc<>(ExplStmtTransFunc.create(solver, 10)))).collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); // final List initialWrites = xcfa.getvars().stream().filter(it -> xcfa.getInitValue(it).isPresent()).map(it -> new MemoryEvent.Write(memEventProvider.getVarId(it), it, null, Set.of(), null)).collect(Collectors.toList()); // final XcfaProcessPartialOrd partialOrd = new XcfaProcessPartialOrd<>(ExplOrd.getInstance()); + + +// final XcfaProcessMemEventProvider memEventProvider = new XcfaProcessMemEventProvider<>(processes.size()); +// final MultiprocLTS, XcfaProcessAction> multiprocLTS = new MultiprocLTS<>(processIds.stream().map(id -> Map.entry(id, new XcfaProcessLTS())).collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); +// final MultiprocInitFunc, ExplPrec> multiprocInitFunc = new MultiprocInitFunc<>(processIds.stream().map(id -> Map.entry(id, new XcfaProcessInitFunc<>(processes.get(id*-1-1), ExplInitFunc.create(solver, True())))).collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); +// final MultiprocTransFunc, XcfaProcessAction, ExplPrec> multiprocTransFunc = new MultiprocTransFunc<>(processIds.stream().map(id -> Map.entry(id, new XcfaProcessTransFunc<>(ExplStmtTransFunc.create(solver, 10)))).collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue))); +// final List initialWrites = xcfa.getvars().stream().filter(it -> xcfa.getInitValue(it).isPresent()).map(it -> new MemoryEvent.Write(memEventProvider.getVarId(it), it, null, Set.of(), null)).collect(Collectors.toList()); +// final XcfaProcessPartialOrd partialOrd = new XcfaProcessPartialOrd<>(ExplOrd.getInstance()); // // final MutableValuation val = new MutableValuation(); // for (VarDecl var : xcfa.getvars()) { diff --git a/subprojects/xcfa/litmus2xcfa/src/main/antlr/BaseLexer.tokens b/subprojects/xcfa/litmus2xcfa/src/main/antlr/BaseLexer.tokens new file mode 100644 index 0000000000..7e1844c6f1 --- /dev/null +++ b/subprojects/xcfa/litmus2xcfa/src/main/antlr/BaseLexer.tokens @@ -0,0 +1,62 @@ +Excl=1 +Quot=2 +Num=3 +Dollar=4 +Percent=5 +Amp=6 +Apos=7 +LPar=8 +RPar=9 +Ast=10 +Plus=11 +Comma=12 +Minus=13 +Period=14 +Slash=15 +Colon=16 +Semi=17 +Less=18 +Equals=19 +Greater=20 +Question=21 +At=22 +LBracket=23 +RBracket=24 +BSlash=25 +LBrace=26 +RBrace=27 +Circ=28 +Tilde=29 +Bar=30 +Underscore=31 +'!'=1 +'"'=2 +'#'=3 +'$'=4 +'%'=5 +'&'=6 +'\''=7 +'('=8 +')'=9 +'*'=10 +'+'=11 +','=12 +'-'=13 +'.'=14 +'/'=15 +':'=16 +';'=17 +'<'=18 +'='=19 +'>'=20 +'?'=21 +'@'=22 +'['=23 +']'=24 +'\\'=25 +'{'=26 +'}'=27 +'^'=28 +'~'=29 +'|'=30 +'_'=31 diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysisTest.kt index 8e080c4900..df1c7c475d 100644 --- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysisTest.kt +++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysisTest.kt @@ -60,7 +60,7 @@ class XcfaAnalysisTest { @MethodSource("data") fun testNoporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first val analysis = ExplXcfaAnalysis( xcfa, @@ -102,7 +102,7 @@ class XcfaAnalysisTest { @MethodSource("data") fun testSporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first val analysis = ExplXcfaAnalysis( xcfa, @@ -144,7 +144,7 @@ class XcfaAnalysisTest { @MethodSource("data") fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first val analysis = ExplXcfaAnalysis( xcfa, @@ -185,7 +185,7 @@ class XcfaAnalysisTest { @MethodSource("data") fun testAasporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first val analysis = ExplXcfaAnalysis( xcfa, @@ -229,7 +229,7 @@ class XcfaAnalysisTest { fun testAadporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) { if (filepath.contains("multithread")) return // TODO: why does it fail to verify? val stream = javaClass.getResourceAsStream(filepath) - val xcfa = getXcfaFromC(stream!!, ParseContext(), false) + val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first val analysis = ExplXcfaAnalysis( xcfa, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/MCMCegar.java b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaCegarTest.kt similarity index 88% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/MCMCegar.java rename to subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaCegarTest.kt index 0fc78b179e..abb015ddcf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/cegar/MCMCegar.java +++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaCegarTest.kt @@ -13,9 +13,3 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - -package hu.bme.mit.theta.analysis.algorithm.mcm.cegar; - -public class MCMCegar { - -} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index 27fe74f7d7..6b3a12c7e9 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -314,8 +314,8 @@ class XcfaCli(private val args: Array) { InputType.C -> { val stream = FileInputStream(input!!) - val xcfaFromC = getXcfaFromC(stream, parseContext, - explicitProperty == ErrorDetection.OVERFLOW) + val xcfaFromC = getXcfaFromC(stream, parseContext, false, + explicitProperty == ErrorDetection.OVERFLOW).first logger.write(Logger.Level.RESULT, "Arithmetic: ${parseContext.arithmetic}\n") xcfaFromC diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt index f9a9432086..b3db63ef51 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt @@ -49,6 +49,17 @@ fun XcfaLabel.collectAssumes(): Iterable> = when (this) { else -> setOf() } +fun XcfaLabel.collectHavocs(): Set> = when (this) { + is StmtLabel -> when (stmt) { + is HavocStmt<*> -> setOf(stmt) + else -> setOf() + } + + is NondetLabel -> labels.map { it.collectHavocs() }.flatten().toSet() + is SequenceLabel -> labels.map { it.collectHavocs() }.flatten().toSet() + else -> setOf() +} + fun XcfaLabel.collectVars(): Iterable> = when (this) { is StmtLabel -> StmtUtils.getVars(stmt) is NondetLabel -> labels.map { it.collectVars() }.flatten() @@ -230,10 +241,10 @@ private fun getAtomicBlockInnerLocations(initialLocation: XcfaLocation): List label is FenceLabel && label.labels.contains("ATOMIC_BEGIN") }) { diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CallGraphPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CallGraphPass.kt new file mode 100644 index 0000000000..ec7098d90a --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CallGraphPass.kt @@ -0,0 +1,44 @@ +/* + * Copyright 2023 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.passes + +import hu.bme.mit.theta.xcfa.getFlatLabels +import hu.bme.mit.theta.xcfa.model.InvokeLabel +import hu.bme.mit.theta.xcfa.model.StartLabel +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder + +/** + * Mark procedure builders with reachability info. + * Marks the called ProcedureBuilders `reachable-from-`. + */ +class CallGraphPass : ProcedurePass { + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + val calledProcedures = LinkedHashSet() + builder.getEdges().map { it.getFlatLabels().filter { it is InvokeLabel || it is StartLabel } }.flatten() + .forEach { + when (it) { + is InvokeLabel -> calledProcedures.add(it.name) + is StartLabel -> calledProcedures.add(it.name) + else -> error("Will never be here (due to filter above)") + } + } + builder.parent.getProcedures().filter { calledProcedures.contains(it.name) } + .forEach { it.metaData["reachable-from-${builder.name}"] = Unit } + return builder + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index ac9d3e8d41..65370c72e6 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -49,7 +49,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePas UnusedVarPass(parseContext), )) -class ChcPasses : ProcedurePassManager(/*listOf( +class ChcPasses : ProcedurePassManager(listOf(/* // formatting NormalizePass(), DeterministicPass(), @@ -76,6 +76,6 @@ class ChcPasses : ProcedurePassManager(/*listOf( // HavocPromotionAndRange(), // Final cleanup UnusedVarPass(), -))*/emptyList()) +*/)) class LitmusPasses : ProcedurePassManager(emptyList()) \ No newline at end of file