summaryrefslogtreecommitdiffstats
path: root/verigraph/src/main/java/it/polito/escape/verify/service
diff options
context:
space:
mode:
Diffstat (limited to 'verigraph/src/main/java/it/polito/escape/verify/service')
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java129
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java136
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java182
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java258
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java132
-rw-r--r--verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java1185
6 files changed, 2022 insertions, 0 deletions
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java b/verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java
new file mode 100644
index 0000000..b34eb08
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java
@@ -0,0 +1,129 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+import it.polito.escape.verify.database.DatabaseClass;
+import it.polito.escape.verify.exception.DataNotFoundException;
+import it.polito.escape.verify.exception.ForbiddenException;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Neighbour;
+import it.polito.escape.verify.model.Node;
+
+public class GraphService {
+
+ private Map<Long, Graph> graphs = DatabaseClass.getInstance().getGraphs();
+
+ public GraphService() {
+
+ }
+
+ public List<Graph> getAllGraphs() {
+ return new ArrayList<Graph>(graphs.values());
+ }
+
+ public Graph getGraph(long id) {
+ if (id <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + id);
+ }
+ Graph graph = graphs.get(id);
+ if (graph == null) {
+ throw new DataNotFoundException("Graph with id " + id + " not found");
+ }
+ return graph;
+ }
+
+ public Graph updateGraph(Graph graph) {
+ if (graph.getId() <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graph.getId());
+ }
+ Graph localGraph = graphs.get(graph.getId());
+ if (localGraph == null) {
+ throw new DataNotFoundException("Graph with id " + graph.getId() + " not found");
+ }
+
+ validateGraph(graph);
+
+// int numberOfNodes = 0;
+// for (Node node : graph.getNodes().values()) {
+//
+// node.setId(++numberOfNodes);
+//
+// int numberOfNodeNeighbours = 0;
+// for (Neighbour neighbour : node.getNeighbours().values()) {
+// neighbour.setId(++numberOfNodeNeighbours);
+// }
+// }
+
+ for (Map.Entry<Long, Node> nodeEntry : graph.getNodes().entrySet()){
+ nodeEntry.getValue().setId(nodeEntry.getKey());
+
+ for (Map.Entry<Long, Neighbour> neighbourEntry : nodeEntry.getValue().getNeighbours().entrySet()){
+ neighbourEntry.getValue().setId(neighbourEntry.getKey());
+ }
+ }
+
+ synchronized(this){
+ graphs.put(graph.getId(), graph);
+ DatabaseClass.persistDatabase();
+ return graph;
+ }
+ }
+
+ public Graph removeGraph(long id) {
+ if (id <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + id);
+ }
+ synchronized(this){
+ return graphs.remove(id);
+ }
+ }
+
+ public Graph addGraph(Graph graph) {
+ validateGraph(graph);
+
+ synchronized (this) {
+ graph.setId(DatabaseClass.getInstance().getNumberOfGraphs() + 1);
+ }
+// int numberOfNodes = 0;
+// for (Node node : graph.getNodes().values()) {
+//
+// node.setId(++numberOfNodes);
+//
+// int numberOfNodeNeighbours = 0;
+// for (Neighbour neighbour : node.getNeighbours().values()) {
+// neighbour.setId(++numberOfNodeNeighbours);
+// }
+// }
+
+ for (Map.Entry<Long, Node> nodeEntry : graph.getNodes().entrySet()){
+ nodeEntry.getValue().setId(nodeEntry.getKey());
+
+ for (Map.Entry<Long, Neighbour> neighbourEntry : nodeEntry.getValue().getNeighbours().entrySet()){
+ neighbourEntry.getValue().setId(neighbourEntry.getKey());
+ }
+ }
+
+ synchronized(this){
+ graphs.put(graph.getId(), graph);
+ DatabaseClass.persistDatabase();
+ return graph;
+ }
+ }
+
+ public static void validateGraph(Graph graph) {
+ for (Node node : graph.getNodes().values()) {
+ NodeService.validateNode(graph, node);
+ }
+ }
+}
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java b/verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java
new file mode 100644
index 0000000..1ac6c1f
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java
@@ -0,0 +1,136 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.util.Iterator;
+import java.util.Map.Entry;
+
+import org.apache.commons.lang3.text.WordUtils;
+
+import com.fasterxml.jackson.databind.JsonNode;
+
+import it.polito.escape.verify.exception.BadRequestException;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Node;
+
+public class JsonValidationService {
+
+ private Graph graph = new Graph();
+
+ private Node node = new Node();
+
+ public JsonValidationService() {
+
+ }
+
+ public JsonValidationService(Graph graph, Node node) {
+ this.graph = graph;
+ this.node = node;
+ }
+
+ public boolean validateFieldAgainstNodeNames(String value) {
+ for (Node node : this.graph.getNodes().values()) {
+ if (node.getName().equals(value))
+ return true;
+ }
+ return false;
+ }
+
+ public void validateFieldsAgainstNodeNames(JsonNode node) {
+ if (node.isTextual()) {
+ boolean isValid = validateFieldAgainstNodeNames(node.asText());
+ if (!isValid) {
+ System.out.println(node.asText() + " is not a valid string!");
+ throw new BadRequestException("String '" + node.asText()
+ + "' is not valid for the configuration of node '" + this.node.getName()
+ + "'");
+ }
+ }
+ if (node.isArray()) {
+ for (JsonNode object : node) {
+ validateFieldsAgainstNodeNames(object);
+ }
+ }
+ if (node.isObject()) {
+ Iterator<Entry<String, JsonNode>> iter = node.fields();
+
+ while (iter.hasNext()) {
+ Entry<String, JsonNode> item = iter.next();
+ validateFieldsAgainstNodeNames(item.getValue());
+ }
+ }
+
+ }
+
+ public boolean validateNodeConfiguration() {
+ String className = WordUtils.capitalize(node.getFunctional_type()) + "Validator";
+
+ Class<?> validator;
+ try {
+ validator = Class.forName("it.polito.escape.verify.validation." + className);
+ }
+ catch (ClassNotFoundException e) {
+ System.out.println(className + " not found, configuration properties of node '" + node.getName()
+ + "' will be validated against node names");
+ return false;
+ }
+
+ Class<?> graphClass;
+ Class<?> nodeClass;
+ Class<?> configurationClass;
+ try {
+ graphClass = Class.forName("it.polito.escape.verify.model.Graph");
+ nodeClass = Class.forName("it.polito.escape.verify.model.Node");
+ configurationClass = Class.forName("it.polito.escape.verify.model.Configuration");
+ }
+ catch (ClassNotFoundException e) {
+ throw new RuntimeException("Model classes not found");
+ }
+
+ Class<?>[] paramTypes = new Class[3];
+ paramTypes[0] = graphClass;
+ paramTypes[1] = nodeClass;
+ paramTypes[2] = configurationClass;
+
+ String methodName = "validate";
+
+ Object instance;
+ try {
+ instance = validator.newInstance();
+ }
+ catch (InstantiationException e) {
+ throw new RuntimeException("'" + className + "' cannot be instantiated");
+ }
+ catch (IllegalAccessException e) {
+ throw new RuntimeException("Illegal access to '" + className + "' instantiation");
+ }
+
+ Method myMethod;
+ try {
+ myMethod = validator.getDeclaredMethod(methodName, paramTypes);
+ }
+ catch (NoSuchMethodException e) {
+ throw new RuntimeException("'" + methodName + "' method has to be implemented in " + className + " class");
+ }
+ try {
+ myMethod.invoke(instance, graph, node, node.getConfiguration());
+ }
+ catch (IllegalAccessException e) {
+ throw new RuntimeException("Illegal access to '" + methodName + "' method in " + className + " instance");
+ }
+ catch (InvocationTargetException e) {
+ throw new BadRequestException("Validation failed for node '" + node.getName() + "': "
+ + e.getTargetException().getMessage());
+ }
+ return true;
+ }
+}
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java b/verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java
new file mode 100644
index 0000000..ecf4e69
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java
@@ -0,0 +1,182 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+import it.polito.escape.verify.database.DatabaseClass;
+import it.polito.escape.verify.exception.BadRequestException;
+import it.polito.escape.verify.exception.DataNotFoundException;
+import it.polito.escape.verify.exception.ForbiddenException;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Neighbour;
+import it.polito.escape.verify.model.Node;
+
+public class NeighbourService {
+
+ private Map<Long, Graph> graphs = DatabaseClass.getInstance().getGraphs();
+
+ public List<Neighbour> getAllNeighbours(long graphId, long nodeId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null)
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ Map<Long, Neighbour> neighbours = node.getNeighbours();
+ return new ArrayList<Neighbour>(neighbours.values());
+ }
+
+ public Neighbour getNeighbour(long graphId, long nodeId, long neighbourId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ if (neighbourId <= 0) {
+ throw new ForbiddenException("Illegal neighbour id: " + neighbourId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null) {
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ }
+ Map<Long, Neighbour> neighbours = node.getNeighbours();
+ Neighbour neighbour = neighbours.get(neighbourId);
+ if (neighbour == null) {
+ throw new DataNotFoundException("Neighbour with id " + neighbourId + " not found for node with id " + nodeId
+ + " in graph with id " + graphId);
+ }
+ return neighbour;
+ }
+
+ public Neighbour addNeighbour(long graphId, long nodeId, Neighbour neighbour) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null) {
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ }
+ Map<Long, Neighbour> neighbours = node.getNeighbours();
+
+ validateNeighbour(graph, node, neighbour);
+
+ synchronized (this) {
+ neighbour.setId(neighbours.size() + 1);
+ neighbours.put(neighbour.getId(), neighbour);
+ DatabaseClass.persistDatabase();
+ return neighbour;
+ }
+ }
+
+ public Neighbour updateNeighbour(long graphId, long nodeId, Neighbour neighbour) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ if (neighbour.getId() <= 0) {
+ throw new ForbiddenException("Illegal neighbour id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null) {
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ }
+ Map<Long, Neighbour> neighbours = node.getNeighbours();
+ Neighbour currentNeighbour = neighbours.get(neighbour.getId());
+ if (currentNeighbour == null) {
+ throw new DataNotFoundException("Neighbour with id " + neighbour.getId() + " not found for node with id "
+ + nodeId + " in graph with id " + graphId);
+ }
+
+ validateNeighbour(graph, node, neighbour);
+
+ synchronized (this) {
+ neighbours.put(neighbour.getId(), neighbour);
+ DatabaseClass.persistDatabase();
+ return neighbour;
+ }
+ }
+
+ public Neighbour removeNeighbour(long graphId, long nodeId, long neighbourId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ if (neighbourId <= 0) {
+ throw new ForbiddenException("Illegal neighbour id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null) {
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ }
+ Map<Long, Neighbour> neighbours = node.getNeighbours();
+
+ synchronized(this){
+ return neighbours.remove(neighbourId);
+ }
+ }
+
+ public static void validateNeighbour(Graph graph, Node node, Neighbour neighbour) {
+ if (graph == null)
+ throw new BadRequestException("Neighbour validation failed: cannot validate null graph");
+ if (node == null)
+ throw new BadRequestException("Neighbour validation failed: cannot validate null node");
+ if (neighbour == null)
+ throw new BadRequestException("Neighbour validation failed: cannot validate null neighbour");
+
+ if (neighbour.getName() == null)
+ throw new BadRequestException("Neighbour validation failed: neighbour 'name' field cannot be null");
+ if (neighbour.getName().equals(""))
+ throw new BadRequestException("Neighbour validation failed: neighbour 'name' field cannot be an empty string");
+
+ Node nodeFound = graph.searchNodeByName(neighbour.getName());
+ if ((nodeFound == null) || (nodeFound.getName().equals(node.getName())))
+ throw new BadRequestException("Neighbour validation failed: '" + neighbour.getName()
+ + "' is not a valid name for a neighbour of node '" + node.getName() + "'");
+
+ Neighbour neighbourFound = node.searchNeighbourByName(neighbour.getName());
+ if ((neighbourFound != null) && (neighbourFound.equals(neighbour) == false))
+ throw new BadRequestException("Neighbour validation failed: node '" + node.getName()
+ + "' already has a neighbour named '" + neighbour.getName() + "'");
+ }
+}
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java b/verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java
new file mode 100644
index 0000000..e6ad672
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java
@@ -0,0 +1,258 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.io.File;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Scanner;
+
+import javax.ws.rs.InternalServerErrorException;
+
+import com.fasterxml.jackson.databind.JsonNode;
+import com.github.fge.jsonschema.core.exceptions.ProcessingException;
+import com.github.fge.jsonschema.main.JsonSchema;
+
+import it.polito.escape.verify.database.DatabaseClass;
+import it.polito.escape.verify.exception.BadRequestException;
+import it.polito.escape.verify.exception.DataNotFoundException;
+import it.polito.escape.verify.exception.ForbiddenException;
+import it.polito.escape.verify.model.Configuration;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Neighbour;
+import it.polito.escape.verify.model.Node;
+
+public class NodeService {
+
+ private Map<Long, Graph> graphs = DatabaseClass.getInstance().getGraphs();
+
+ public NodeService() {
+
+ }
+
+ public List<Node> getAllNodes(long graphId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ return new ArrayList<Node>(nodes.values());
+ }
+
+ public Node getNode(long graphId, long nodeId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node node = nodes.get(nodeId);
+ if (node == null) {
+ throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId);
+ }
+ return node;
+ }
+
+ public Node updateNode(long graphId, Node node) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (node.getId() <= 0) {
+ throw new ForbiddenException("Illegal node id: " + node.getId());
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+ Node localNode = nodes.get(node.getId());
+ if (localNode == null) {
+ throw new DataNotFoundException("Node with id " + node.getId() + " not found in graph with id " + graphId);
+ }
+
+ Graph graphCopy = new Graph();
+ graphCopy.setId(graph.getId());
+ graphCopy.setNodes(new HashMap<Long, Node>(graph.getNodes()));
+ graphCopy.getNodes().remove(node.getId());
+
+ // int numberOfNeighbours = 0;
+ // for(Neighbour neighbour : node.getNeighbours().values()){
+ // neighbour.setId(++numberOfNeighbours);
+ // }
+
+ for (Map.Entry<Long, Neighbour> neighbourEntry : node.getNeighbours().entrySet()) {
+ neighbourEntry.getValue().setId(neighbourEntry.getKey());
+ }
+
+ validateNode(graphCopy, node);
+
+ synchronized (this) {
+ nodes.put(node.getId(), node);
+ DatabaseClass.persistDatabase();
+ return node;
+ }
+ }
+
+ public Node removeNode(long graphId, long nodeId) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ if (nodeId <= 0) {
+ throw new ForbiddenException("Illegal node id: " + nodeId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+
+ synchronized (this) {
+ return nodes.remove(nodeId);
+ }
+ }
+
+ public Node addNode(long graphId, Node node) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+
+ validateNode(graph, node);
+
+ synchronized (this) {
+ node.setId(DatabaseClass.getInstance().getGraphNumberOfNodes(graphId) + 1);
+ }
+
+ // int numberOfNeighbours = 0;
+
+ for (Map.Entry<Long, Neighbour> neighbourEntry : node.getNeighbours().entrySet()) {
+ neighbourEntry.getValue().setId(neighbourEntry.getKey());
+ }
+
+ // for (Neighbour neighbour : node.getNeighbours().values()) {
+ // neighbour.setId(++numberOfNeighbours);
+ // }
+
+ synchronized (this) {
+ nodes.put(node.getId(), node);
+ DatabaseClass.persistDatabase();
+ return node;
+ }
+ }
+
+ public Node searchByName(long graphId, String nodeName) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ Graph graph = graphs.get(graphId);
+ if (graph == null)
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ Map<Long, Node> nodes = graph.getNodes();
+
+ for (Node node : nodes.values()) {
+ if (node.getName().equals(nodeName))
+ return node;
+ }
+ return null;
+ }
+
+ public static void validateNode(Graph graph, Node node) {
+ if (graph == null)
+ throw new BadRequestException("Node validation failed: cannot validate null graph");
+ if (node == null)
+ throw new BadRequestException("Node validation failed: cannot validate null node");
+
+ if (node.getName() == null)
+ throw new BadRequestException("Node validation failed: node 'name' field cannot be null");
+ if (node.getFunctional_type() == null)
+ throw new BadRequestException("Node validation failed: node 'functional_type' field cannot be null");
+
+ if (node.getName().equals(""))
+ throw new BadRequestException("Node validation failed: node 'name' field cannot be an empty string");
+ if (node.getFunctional_type().equals(""))
+ throw new BadRequestException("Node validation failed: node 'functional_type' field cannot be an empty string");
+
+ Node nodeFound = graph.searchNodeByName(node.getName());
+ if ((nodeFound != null) && (nodeFound.equals(node) == false))
+ throw new BadRequestException("Node validation failed: graph already has a node named '" + node.getName()
+ + "'");
+ Configuration configuration = node.getConfiguration();
+ if (configuration != null) {
+ JsonNode configurationJsonNode = configuration.getConfiguration();
+ // validate configuration against schema file
+ validateNodeConfigurationAgainstSchemaFile(node, configurationJsonNode);
+ JsonValidationService jsonValidator = new JsonValidationService(graph, node);
+ boolean hasCustomValidator = jsonValidator.validateNodeConfiguration();
+ if (!hasCustomValidator) {
+ jsonValidator.validateFieldsAgainstNodeNames(configurationJsonNode);
+ }
+ }
+
+ // validate neighbours
+ Map<Long, Neighbour> nodeNeighboursMap = node.getNeighbours();
+ if (nodeNeighboursMap == null)
+ throw new BadRequestException("Node validation failed: node 'neighbours' cannot be null");
+ for (Neighbour neighbour : nodeNeighboursMap.values()) {
+ NeighbourService.validateNeighbour(graph, node, neighbour);
+ }
+ }
+
+ public static void validateNodeConfigurationAgainstSchemaFile(Node node, JsonNode configurationJson) {
+ String schemaFileName = node.getFunctional_type() + ".json";
+
+ File schemaFile = new File(System.getProperty("catalina.base") + "/webapps/verify/json/" + schemaFileName);
+
+ if (!schemaFile.exists()) {
+ //if no REST client, try gRPC application
+ schemaFile = new File("src/main/webapp/json/" + schemaFileName);
+
+ if (!schemaFile.exists()) {
+ throw new ForbiddenException("Functional type '" + node.getFunctional_type()
+ + "' is not supported! Please edit 'functional_type' field of node '"
+ + node.getName() + "'");
+ }
+ }
+
+ JsonSchema schemaNode = null;
+ try {
+ schemaNode = ValidationUtils.getSchemaNode(schemaFile);
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to load '" + schemaFileName + "' schema file");
+ }
+ catch (ProcessingException e) {
+ throw new InternalServerErrorException("Unable to resolve '" + schemaFileName
+ + "' schema file as a schema node");
+ }
+
+ try {
+ ValidationUtils.validateJson(schemaNode, configurationJson);
+ }
+ catch (ProcessingException e) {
+ throw new BadRequestException("Something went wrong trying to validate node '" + node.getName()
+ + "' with the following configuration: '" + configurationJson.toString()
+ + "' against the json schema '" + schemaFile.getName() + "': "
+ + e.getMessage());
+
+ }
+
+ }
+}
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java b/verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java
new file mode 100644
index 0000000..77ef4f7
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java
@@ -0,0 +1,132 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.URL;
+
+import com.fasterxml.jackson.databind.JsonNode;
+import com.fasterxml.jackson.databind.node.ObjectNode;
+import com.github.fge.jackson.JsonLoader;
+import com.github.fge.jsonschema.core.exceptions.ProcessingException;
+import com.github.fge.jsonschema.core.report.ProcessingMessage;
+import com.github.fge.jsonschema.core.report.ProcessingReport;
+import com.github.fge.jsonschema.main.JsonSchema;
+import com.github.fge.jsonschema.main.JsonSchemaFactory;
+
+public class ValidationUtils {
+
+ public static final String JSON_V4_SCHEMA_IDENTIFIER = "http://json-schema.org/draft-04/schema#";
+ public static final String JSON_SCHEMA_IDENTIFIER_ELEMENT = "$schema";
+
+ public static JsonNode getJsonNode(String jsonText) throws IOException {
+ return JsonLoader.fromString(jsonText);
+ } // getJsonNode(text) ends
+
+ public static JsonNode getJsonNode(File jsonFile) throws IOException {
+ return JsonLoader.fromFile(jsonFile);
+ } // getJsonNode(File) ends
+
+ public static JsonNode getJsonNode(URL url) throws IOException {
+ return JsonLoader.fromURL(url);
+ } // getJsonNode(URL) ends
+
+ public static JsonNode getJsonNodeFromResource(String resource) throws IOException {
+ return JsonLoader.fromResource(resource);
+ } // getJsonNode(Resource) ends
+
+ public static JsonSchema getSchemaNode(String schemaText) throws IOException, ProcessingException {
+ final JsonNode schemaNode = getJsonNode(schemaText);
+ return _getSchemaNode(schemaNode);
+ } // getSchemaNode(text) ends
+
+ public static JsonSchema getSchemaNode(File schemaFile) throws IOException, ProcessingException {
+ final JsonNode schemaNode = getJsonNode(schemaFile);
+ return _getSchemaNode(schemaNode);
+ } // getSchemaNode(File) ends
+
+ public static JsonSchema getSchemaNode(URL schemaFile) throws IOException, ProcessingException {
+ final JsonNode schemaNode = getJsonNode(schemaFile);
+ return _getSchemaNode(schemaNode);
+ } // getSchemaNode(URL) ends
+
+ public static JsonSchema getSchemaNodeFromResource(String resource) throws IOException, ProcessingException {
+ final JsonNode schemaNode = getJsonNodeFromResource(resource);
+ return _getSchemaNode(schemaNode);
+ } // getSchemaNode() ends
+
+ public static void validateJson(JsonSchema jsonSchemaNode, JsonNode jsonNode) throws ProcessingException {
+ ProcessingReport report = jsonSchemaNode.validate(jsonNode);
+ if (!report.isSuccess()) {
+ for (ProcessingMessage processingMessage : report) {
+ throw new ProcessingException(processingMessage);
+ }
+ }
+ } // validateJson(Node) ends
+
+ public static boolean isJsonValid(JsonSchema jsonSchemaNode, JsonNode jsonNode) throws ProcessingException {
+ ProcessingReport report = jsonSchemaNode.validate(jsonNode);
+ return report.isSuccess();
+ } // validateJson(Node) ends
+
+ public static boolean isJsonValid(String schemaText, String jsonText) throws ProcessingException, IOException {
+ final JsonSchema schemaNode = getSchemaNode(schemaText);
+ final JsonNode jsonNode = getJsonNode(jsonText);
+ return isJsonValid(schemaNode, jsonNode);
+ } // validateJson(Node) ends
+
+ public static boolean isJsonValid(File schemaFile, File jsonFile) throws ProcessingException, IOException {
+ final JsonSchema schemaNode = getSchemaNode(schemaFile);
+ final JsonNode jsonNode = getJsonNode(jsonFile);
+ return isJsonValid(schemaNode, jsonNode);
+ } // validateJson(Node) ends
+
+ public static boolean isJsonValid(URL schemaURL, URL jsonURL) throws ProcessingException, IOException {
+ final JsonSchema schemaNode = getSchemaNode(schemaURL);
+ final JsonNode jsonNode = getJsonNode(jsonURL);
+ return isJsonValid(schemaNode, jsonNode);
+ } // validateJson(Node) ends
+
+ public static void validateJson(String schemaText, String jsonText) throws IOException, ProcessingException {
+ final JsonSchema schemaNode = getSchemaNode(schemaText);
+ final JsonNode jsonNode = getJsonNode(jsonText);
+ validateJson(schemaNode, jsonNode);
+ } // validateJson(text) ends
+
+ public static void validateJson(File schemaFile, File jsonFile) throws IOException, ProcessingException {
+ final JsonSchema schemaNode = getSchemaNode(schemaFile);
+ final JsonNode jsonNode = getJsonNode(jsonFile);
+ validateJson(schemaNode, jsonNode);
+ } // validateJson(File) ends
+
+ public static void validateJson(URL schemaDocument, URL jsonDocument) throws IOException, ProcessingException {
+ final JsonSchema schemaNode = getSchemaNode(schemaDocument);
+ final JsonNode jsonNode = getJsonNode(jsonDocument);
+ validateJson(schemaNode, jsonNode);
+ } // validateJson(URL) ends
+
+ public static void validateJsonResource(String schemaResource, String jsonResource) throws IOException,
+ ProcessingException {
+ final JsonSchema schemaNode = getSchemaNode(schemaResource);
+ final JsonNode jsonNode = getJsonNodeFromResource(jsonResource);
+ validateJson(schemaNode, jsonNode);
+ } // validateJsonResource() ends
+
+ private static JsonSchema _getSchemaNode(JsonNode jsonNode) throws ProcessingException {
+ final JsonNode schemaIdentifier = jsonNode.get(JSON_SCHEMA_IDENTIFIER_ELEMENT);
+ if (null == schemaIdentifier) {
+ ((ObjectNode) jsonNode).put(JSON_SCHEMA_IDENTIFIER_ELEMENT, JSON_V4_SCHEMA_IDENTIFIER);
+ }
+
+ final JsonSchemaFactory factory = JsonSchemaFactory.byDefault();
+ return factory.getJsonSchema(jsonNode);
+ } // _getSchemaNode() ends
+}
diff --git a/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java b/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
new file mode 100644
index 0000000..1d31ae9
--- /dev/null
+++ b/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java
@@ -0,0 +1,1185 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Politecnico di Torino and others.
+ *
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Apache License, Version 2.0
+ * which accompanies this distribution, and is available at
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *******************************************************************************/
+
+package it.polito.escape.verify.service;
+
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.FilenameFilter;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import java.util.stream.Collectors;
+
+import javax.tools.Diagnostic;
+import javax.tools.DiagnosticCollector;
+import javax.tools.JavaCompiler;
+import javax.tools.JavaFileObject;
+import javax.tools.StandardJavaFileManager;
+import javax.tools.ToolProvider;
+import javax.ws.rs.ProcessingException;
+import javax.xml.bind.JAXBException;
+
+import org.json.simple.JSONArray;
+import org.json.simple.JSONObject;
+
+import com.fasterxml.jackson.databind.JsonNode;
+
+import it.polito.escape.verify.client.Neo4jManagerClient;
+import it.polito.escape.verify.exception.BadRequestException;
+import it.polito.escape.verify.exception.DataNotFoundException;
+import it.polito.escape.verify.exception.ForbiddenException;
+import it.polito.escape.verify.exception.InternalServerErrorException;
+import it.polito.escape.verify.model.Configuration;
+import it.polito.escape.verify.model.Entry;
+import it.polito.escape.verify.model.Graph;
+import it.polito.escape.verify.model.Neighbour;
+import it.polito.escape.verify.model.Node;
+import it.polito.escape.verify.model.Test;
+import it.polito.escape.verify.model.Verification;
+import it.polito.escape.verify.resources.beans.VerificationBean;
+import it.polito.nffg.neo4j.jaxb.Paths;
+import qj.util.ReflectUtil;
+import qj.util.lang.DynamicClassLoader;
+
+public class VerificationService {
+
+ private static final String generatorFolder = System.getProperty("catalina.base")
+ + "/webapps/verify/WEB-INF/classes/tests/j-verigraph-generator";
+
+ private static final String generatorFolderForGrpc = "service/src/tests/j-verigraph-generator";
+
+ private String testClassGenerator = generatorFolder + "/test_class_generator.py";
+
+ private String testGenerator = generatorFolder + "/test_generator.py";
+
+ public VerificationService() {
+
+ }
+
+ private Paths getPaths(Graph graph, Node sourceNode, Node destinationNode) {
+
+ String source = sourceNode.getName() + "_" + sourceNode.getId();
+ String destination = destinationNode.getName() + "_" + destinationNode.getId();
+
+ List<String> endpoints = new ArrayList<>();
+ List<String> firewalls = new ArrayList<>();
+ Map<String, List<Entry>> routingTable = new HashMap<>();
+
+ for (Node node : graph.getNodes().values()) {
+ // if firewall
+ if (node.getFunctional_type().equals("NF")) {
+ // add 2 connection points to RT
+ routingTable.put(node.getName() + "_" + node.getId() + "_in", new ArrayList<Entry>());
+ routingTable.put(node.getName() + "_" + node.getId() + "_out", new ArrayList<Entry>());
+ // add node to firewalls
+ firewalls.add(node.getName() + "_" + node.getId());
+ // scan neighbours
+ for (Neighbour neighbour : node.getNeighbours().values()) {
+ // check if neighbour is a firewall
+ Node hop = graph.searchNodeByName(neighbour.getName());
+ // if neighbour is a firewall connect to its input port
+ if (hop.getFunctional_type().equals("NF"))
+ routingTable.get(node.getName() + "_" + node.getId() + "_out")
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
+ else
+ // connect
+ // normally to
+ // node
+ routingTable.get(node.getName() + "_" + node.getId()
+ + "_out")
+ .add(new Entry( "output",
+ neighbour.getName() + "_"
+ + hop.getId()));
+ }
+ }
+ // if endpoint
+ else {
+ // add endpoint to RT
+ routingTable.put(node.getName() + "_" + node.getId(), new ArrayList<Entry>());
+ // add to endpoints
+ endpoints.add(node.getName() + "_" + node.getId());
+ // scan neighbours
+ for (Neighbour neighbour : node.getNeighbours().values()) {
+ // check if neighbour is a firewall
+ Node hop = graph.searchNodeByName(neighbour.getName());
+ // if neighbour is a firewall connect to its input port
+ if (hop.getFunctional_type().equals("NF"))
+ routingTable.get(node.getName() + "_" + node.getId())
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
+ else {
+ // connect
+ // normally to
+ // node
+ routingTable.get(node.getName() + "_" + node.getId())
+ .add(new Entry("output", neighbour.getName() + "_" + hop.getId()));
+ }
+ }
+ }
+
+ // end node scan
+ }
+ // debug print
+ System.out.println("Endpoints:");
+ for (String endpoint : endpoints) {
+ System.out.println(endpoint);
+ }
+ System.out.println("Firewalls:");
+ for (String firewall : firewalls) {
+ System.out.println(firewall);
+ }
+ System.out.println("Source: " + source);
+ System.out.println("Destination: " + destination);
+ for (String key : routingTable.keySet()) {
+ System.out.println("RT for node " + key);
+ for (Entry entry : routingTable.get(key)) {
+ System.out.println("\t" + entry.getDirection() + "->" + entry.getDestination());
+ }
+ }
+ // end debug print
+
+ Neo4jManagerClient client = new Neo4jManagerClient( "http://localhost:8080/neo4jmanager/rest/",
+ source,
+ destination,
+ endpoints,
+ firewalls,
+ routingTable);
+
+ Paths paths = null;
+ try {
+ paths = client.getPaths();
+ }
+ catch (JAXBException e) {
+ throw new InternalServerErrorException("Error generating input for neo4jmanager: " + e.getMessage());
+ }
+ catch (ProcessingException e) {
+ throw new InternalServerErrorException("Response of neo4jmanager doesn't contain any path: "
+ + e.getMessage());
+ }
+ catch (IllegalStateException e) {
+ throw new InternalServerErrorException("Error getting a response from neo4jmanager, no input stream for paths or input stream already consumed: "
+ + e.getMessage());
+ }
+ catch (Exception e) {
+ throw new InternalServerErrorException("Unable to continue due to a neo4jmanager error: " + e.getMessage());
+ }
+
+ return paths;
+
+ }
+
+ private List<String> sanitizePath(String path) {
+ List<String> newPath = new ArrayList<String>();
+ // find all nodes, i.e. all names between parentheses
+ Matcher m = Pattern.compile("\\(([^)]+)\\)").matcher(path);
+ while (m.find()) {
+ String node = m.group(1);
+
+ int spaceIndex = node.lastIndexOf("_");
+ if (spaceIndex != -1) {
+ node = node.substring(0, spaceIndex);
+ newPath.add(node);
+ }
+ }
+ return newPath;
+
+ }
+
+ private List<List<String>> sanitizePaths(Paths paths) {
+ List<List<String>> sanitizedPaths = new ArrayList<List<String>>();
+ for (String path : paths.getPath()) {
+ System.out.println("Original path: " + path);
+ List<String> newPath = sanitizePath(path);
+ sanitizedPaths.add(newPath);
+ }
+ return sanitizedPaths;
+ }
+
+ static private Map<String, Long> toMap(List<String> lst) {
+ return lst.stream().collect(Collectors.groupingBy(s -> s, Collectors.counting()));
+ }
+
+ private void eliminateLoopsInPaths(List<List<String>> sanitizedPaths) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+
+ for (List<String> path : sanitizedPaths) {
+ Map<String, Long> occurrencesMap = toMap(path);
+ for (long occurrences : occurrencesMap.values()) {
+ if (occurrences > 1) {
+ pathsToBeRemoved.add(path);
+ break;
+ }
+ }
+ }
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+ }
+
+ private void printListsOfStrings(String message, List<List<String>> lists) {
+ System.out.println(message);
+ for (List<String> element : lists) {
+ System.out.println(element);
+ }
+ }
+
+ private static File createTempDir(String prefix) throws IOException {
+ String tmpDirStr = System.getProperty("java.io.tmpdir");
+ if (tmpDirStr == null) {
+ throw new IOException("System property 'java.io.tmpdir' does not specify a tmp dir");
+ }
+
+ File tmpDir = new File(tmpDirStr);
+ if (!tmpDir.exists()) {
+ boolean created = tmpDir.mkdirs();
+ if (!created) {
+ throw new IOException("Unable to create tmp dir " + tmpDir);
+ }
+ }
+
+ File resultDir = null;
+ int suffix = (int) System.currentTimeMillis();
+ int failureCount = 0;
+ do {
+ resultDir = new File(tmpDir, prefix + suffix % 10000);
+ suffix++;
+ failureCount++;
+ } while (resultDir.exists() && failureCount < 50);
+
+ if (resultDir.exists()) {
+ throw new IOException(failureCount
+ + " attempts to generate a non-existent directory name failed, giving up");
+ }
+ boolean created = resultDir.mkdir();
+ if (!created) {
+ throw new IOException("Failed to create tmp directory");
+ }
+
+ return resultDir;
+ }
+
+ @SuppressWarnings("unchecked")
+ private void generateChainsFile(Graph graph, List<List<String>> sanitizedPaths, String chainsFile) {
+ JSONObject root = new JSONObject();
+ JSONArray chains = new JSONArray();
+
+ int chainCounter = 0;
+
+ for (List<String> path : sanitizedPaths) {
+ Iterator<String> pathsIterator = path.iterator();
+ JSONObject chain = new JSONObject();
+ chain.put("id", ++chainCounter);
+ chain.put("flowspace", "tcp=80");
+ JSONArray nodes = new JSONArray();
+ while (pathsIterator.hasNext()) {
+ String nodeName = (String) pathsIterator.next();
+ Node currentNode = graph.searchNodeByName(nodeName);
+ if (currentNode == null) {
+ throw new InternalServerErrorException("Unable to generate 'chains.json' for neo4jmanager: node "
+ + nodeName + " not found");
+ }
+ JSONObject node = new JSONObject();
+ node.put("name", currentNode.getName());
+ // if(currentNode.getFunctional_type().equals("firewall"))
+ // node.put("address", "ip_nat");
+ // else
+ node.put("address", "ip_" + currentNode.getName());
+ node.put("functional_type", currentNode.getFunctional_type());
+ nodes.add(node);
+ chain.put("nodes", nodes);
+ }
+ chains.add(chain);
+ }
+ root.put("chains", chains);
+
+ try (FileWriter file = new FileWriter(chainsFile)) {
+ file.write(root.toJSONString());
+ System.out.println("Successfully created 'chains.json' with the following content:");
+ System.out.println(root);
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error saving 'chains.json' for neo4jmanager");
+ }
+
+ }
+
+ @SuppressWarnings("unchecked")
+ private void generateConfigFile(Graph graph, String configFile) {
+ JSONObject root = new JSONObject();
+ JSONArray nodes = new JSONArray();
+
+ for (Node n : graph.getNodes().values()) {
+ JSONObject node = new JSONObject();
+ // JSONArray configuration = new JSONArray();
+ Configuration nodeConfig = n.getConfiguration();
+ JsonNode configuration = nodeConfig.getConfiguration();
+
+ node.put("configuration", configuration);
+ node.put("id", nodeConfig.getId());
+ node.put("description", nodeConfig.getDescription());
+
+ nodes.add(node);
+
+ }
+ root.put("nodes", nodes);
+
+ try (FileWriter file = new FileWriter(configFile)) {
+ file.write(root.toJSONString());
+ System.out.println("Successfully created 'config.json' with the following content:");
+ System.out.println(root);
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error saving 'config.json' for neo4jmanager");
+ }
+
+ }
+
+ private void printCommand(String[] cmd) {
+ for (String c : cmd) {
+ System.out.printf(c + " ");
+ }
+ System.out.println("");
+ }
+
+ private String platfromIndependentPath(String path) {
+ path = path.replaceAll("/", Matcher.quoteReplacement(Character.toString(File.separatorChar)));
+ return path;
+ }
+
+ private void generateTestScenarios(String chainsFile, String configFile, String scenarioFile) {
+
+ String[] cmd = { "python", platfromIndependentPath(testClassGenerator), "-c",
+ platfromIndependentPath(chainsFile), "-f", platfromIndependentPath(configFile), "-o",
+ platfromIndependentPath(scenarioFile) };
+ printCommand(cmd);
+
+ ProcessBuilder pb = new ProcessBuilder(cmd);
+ pb.redirectErrorStream(true);
+ Process process;
+ try {
+ process = pb.start();
+
+ BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+ String line;
+ while ((line = reader.readLine()) != null)
+ System.out.println("test_class_generator.py: " + line);
+ process.waitFor();
+ if (process.exitValue() != 0) {
+ throw new InternalServerErrorException("Unable to generate test scenario file for the verification request: test_class_generator returned "
+ + process.exitValue());
+ }
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
+ }
+ catch (InterruptedException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
+ }
+
+ }
+
+ private void generateTests( int scenariosCounter, String scenariosBasename, String source, String destination,
+ String testsBasename) {
+
+ List<String> scenarios = new ArrayList<String>();
+ List<String> tests = new ArrayList<String>();
+ for (int i = 0; i < scenariosCounter; i++) {
+ scenarios.add(scenariosBasename + "_" + (i + 1) + ".java");
+ tests.add(testsBasename + "_" + (i + 1) + ".java");
+ }
+
+ for (int i = 0; i < scenariosCounter; i++) {
+ String[] cmd = { "python", platfromIndependentPath(testGenerator), "-i",
+ platfromIndependentPath(scenarios.get(i)), "-o", platfromIndependentPath(tests.get(i)),
+ "-s", source, "-d", destination };
+ printCommand(cmd);
+
+ ProcessBuilder pb = new ProcessBuilder(cmd);
+ pb.redirectErrorStream(true);
+ Process process;
+ try {
+ process = pb.start();
+
+ BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+ String line;
+ while ((line = reader.readLine()) != null)
+ System.out.println("test_generator.py: " + line);
+ process.waitFor();
+ if (process.exitValue() != 0) {
+ throw new InternalServerErrorException("Unable to generate test file for the verification request: test_generator returned "
+ + process.exitValue());
+ }
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
+ }
+ catch (InterruptedException e) {
+ throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
+ }
+
+ }
+
+ }
+
+ private void prepareForCompilationAndExecution( int scenariosCounter, String scenarioBasename, String testBasename,
+ List<File> sourceFiles, List<File> classFiles) {
+ for (int i = 0; i < scenariosCounter; i++) {
+ String scenario = scenarioBasename + "_" + (i + 1) + ".java";
+ sourceFiles.add(new File(scenario));
+ System.out.println("Scenario file " + scenario + " added to compilation");
+
+ String testSource = testBasename + "_" + (i + 1) + ".java";
+ String testClass = testBasename + "_" + (i + 1);
+
+ sourceFiles.add(new File(testSource));
+ System.out.println("Test file " + testSource + " added to copilation");
+ classFiles.add(new File(testClass));
+ System.out.println("Test file " + testClass + " added to execution");
+ }
+ }
+
+ private void compileFiles(List<File> files, String folder) {
+
+ JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
+ if (compiler == null) {
+ throw new InternalServerErrorException("Error getting the Java compiler: JDK >= 1.8 required");
+ }
+ StandardJavaFileManager fileManager = compiler.getStandardFileManager(null, null, null);
+
+ try {
+ // fileManager.setLocation(StandardLocation.CLASS_OUTPUT,
+ // Arrays.asList(new File(projectFolder)));
+
+ // String z3 = "/usr/lib/com.microsoft.z3.jar";
+ // List<String> optionList = new ArrayList<String>();
+ // optionList.add("-classpath");
+ // optionList.add(System.getProperty("java.class.path") + ":" + z3);
+ List<String> optionList = new ArrayList<String>();
+ optionList.add("-d");
+ optionList.add(folder);
+ DiagnosticCollector<JavaFileObject> diagnostics = new DiagnosticCollector<>();
+
+ boolean success = compiler
+ .getTask( null,
+ fileManager,
+ diagnostics,
+ optionList,
+ null,
+ fileManager.getJavaFileObjectsFromFiles(files))
+ .call();
+ if (!success) {
+ Locale myLocale = Locale.getDefault();
+ StringBuilder msg = new StringBuilder();
+ msg.append("Error compiling Z3 test files: ");
+ for (Diagnostic<? extends JavaFileObject> err : diagnostics.getDiagnostics()) {
+ msg.append('\n');
+ msg.append(err.getKind());
+ msg.append(": ");
+ if (err.getSource() != null) {
+ msg.append(err.getSource().getName());
+ }
+ msg.append(':');
+ msg.append(err.getLineNumber());
+ msg.append(": ");
+ msg.append(err.getMessage(myLocale));
+ }
+ throw new InternalServerErrorException(msg.toString());
+ }
+ fileManager.close();
+
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to set the location of the Z3 test files to be compiled");
+ }
+
+ }
+
+ private int runIt(File filename, String folder) {
+ int endIndex = filename.getName().lastIndexOf(".");
+ String filenameNoExtension;
+ if (endIndex == -1) {
+ filenameNoExtension = filename.getName();
+ }
+ else {
+ filenameNoExtension = filename.getName().substring(0, endIndex);
+ if (!filenameNoExtension.matches("\\w+")) {
+ filenameNoExtension = filename.getName();
+ }
+ }
+
+ System.out.println("Filename is: " + filenameNoExtension);
+ try {
+ Class<?> userClass = new DynamicClassLoader(folder).load("tests." + filenameNoExtension);
+ Object context = ReflectUtil.newInstance(userClass);
+ Object result = ReflectUtil.invoke("run", context);
+ return (int) result;
+ }
+ catch (Exception e) {
+ StringWriter errors = new StringWriter();
+ e.printStackTrace(new PrintWriter(errors));
+ throw new InternalServerErrorException("Error executing Z3 tests: " + e.getMessage()
+ + ". There are errors in the Z3 model.");
+ }
+ }
+
+ private List<Test> runFiles(String folder, List<List<String>> paths, Graph graph, List<File> files) {
+ List<Test> tests = new ArrayList<Test>();
+ for (int i = 0; i < files.size(); i++) {
+ System.out.println("Running test file \"" + files.get(i).getAbsolutePath() + "\"");
+ int result = runIt(files.get(i), folder);
+ System.out.println("Execution returned: " + result);
+
+ List<Node> path = new ArrayList<Node>();
+ for (String nodeString : paths.get(i)) {
+ Node node = graph.searchNodeByName(nodeString);
+ path.add(node);
+ }
+ Test t = new Test(path, result);
+ tests.add(t);
+ }
+
+ return tests;
+ }
+
+ @SuppressWarnings("unused")
+ private static boolean deleteDir(File dir) {
+ if (dir.isDirectory()) {
+ String[] children = dir.list();
+ for (int i = 0; i < children.length; i++) {
+ boolean success = deleteDir(new File(dir, children[i]));
+ if (!success) {
+ return false;
+ }
+ }
+ }
+
+ return dir.delete();
+
+ }
+
+ @SuppressWarnings("unused")
+ private void deleteFilesWithPrefix(String directory, String prefix, String extension) {
+ final File scenarioFolder = new File(directory);
+ final File[] scenarioFiles = scenarioFolder.listFiles(new FilenameFilter() {
+
+ @Override
+ public boolean accept(final File dir, final String name) {
+ return name.matches(prefix + ".*\\." + extension);
+ }
+ });
+ for (final File file : scenarioFiles) {
+ if (!file.delete()) {
+ System.err.println("Can't remove " + file.getAbsolutePath());
+ }
+ else {
+ System.out.println("Removed file " + file.getAbsolutePath());
+ }
+ }
+ }
+
+ public Verification verify(long graphId, VerificationBean verificationBean) {
+ if (graphId <= 0) {
+ throw new ForbiddenException("Illegal graph id: " + graphId);
+ }
+ GraphService graphService = new GraphService();
+ Graph graph = graphService.getGraph(graphId);
+ if (graph == null) {
+ throw new DataNotFoundException("Graph with id " + graphId + " not found");
+ }
+ String source = verificationBean.getSource();
+ String destination = verificationBean.getDestination();
+ String type = verificationBean.getType();
+ if (source == null || source.equals("")) {
+ throw new BadRequestException("Please specify the 'source' parameter in your request");
+ }
+ if (destination == null || destination.equals("")) {
+ throw new BadRequestException("Please specify the 'destination' parameter in your request");
+ }
+ if (type == null || type.equals("")) {
+ throw new BadRequestException("Please specify the 'type' parameter in your request");
+ }
+
+ Node sourceNode = graph.searchNodeByName(verificationBean.getSource());
+ Node destinationNode = graph.searchNodeByName(verificationBean.getDestination());
+
+ if (sourceNode == null) {
+ throw new BadRequestException("The 'source' parameter '" + source + "' is not valid, please insert the name of an existing node");
+ }
+ if (destinationNode == null) {
+ throw new BadRequestException("The 'destination' parameter '" + destination + "' is not valid, please insert the name of an existing node");
+ }
+ if ((!type.equals("reachability")) && (!type.equals("isolation")) && (!type.equals("traversal"))) {
+ throw new BadRequestException("The 'type' parameter '" + type
+ + "' is not valid: valid types are: 'reachability', 'isolation' and 'traversal'");
+ }
+
+ Verification v = null;
+ String middlebox;
+ Node middleboxNode;
+ switch (type) {
+ case "reachability":
+ v = reachabilityVerification(graph, sourceNode, destinationNode);
+ break;
+ case "isolation":
+ middlebox = verificationBean.getMiddlebox();
+ if (middlebox == null || middlebox.equals("")) {
+ throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
+ }
+
+ middleboxNode = graph.searchNodeByName(middlebox);
+ if (middleboxNode == null) {
+ throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
+ }
+ if (middleboxNode.getFunctional_type().equals("endpoint")) {
+ throw new BadRequestException("'" + middlebox
+ + "' is of type 'endpoint', please choose a valid middlebox");
+ }
+ v = isolationVerification(graph, sourceNode, destinationNode, middleboxNode);
+ break;
+ case "traversal":
+ middlebox = verificationBean.getMiddlebox();
+ if (middlebox == null || middlebox.equals("")) {
+ throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
+ }
+
+ middleboxNode = graph.searchNodeByName(middlebox);
+ if (middleboxNode == null) {
+ throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
+ }
+ if (middleboxNode.getFunctional_type().equals("endpoint")) {
+ throw new BadRequestException("'" + middlebox
+ + "' is of type 'endpoint', please choose a valid middlebox");
+ }
+ v = traversalVerification(graph, sourceNode, destinationNode, middleboxNode);
+ break;
+ default:
+ break;
+ }
+
+ return v;
+ }
+
+ private Verification isolationVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
+
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> sanitizedPaths = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", sanitizedPaths);
+
+ eliminateLoopsInPaths(sanitizedPaths);
+
+ printListsOfStrings("After loops removal", sanitizedPaths);
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<Test> tests = extractTestsFromPaths(graph, sanitizedPaths, "UNKNWON");
+
+ extractPathsWithMiddlebox(sanitizedPaths, middleboxNode.getName());
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ tests,
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' which traverse middlebox '"
+ + middleboxNode.getName() + "'. See below all the available paths.");
+ }
+
+ printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", sanitizedPaths);
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("isolation");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, sanitizedPaths, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String isolationScenariosBasename = tempDir.getAbsolutePath() + "/IsolationScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
+ }catch(Exception ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
+ }
+
+ String isolationTestsBasename = tempDir.getAbsolutePath() + "/IsolationTest";
+ try{
+ generateTests( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ sourceNode.getName(),
+ middleboxNode.getName(),
+ isolationTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ sourceNode.getName(),
+ middleboxNode.getName(),
+ isolationTestsBasename);
+ }
+
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( sanitizedPaths.size(),
+ isolationScenariosBasename,
+ isolationTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
+
+ return evaluateIsolationResults(tests,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ middleboxNode.getName());
+
+ }
+
+ private List<Test> extractTestsFromPaths(Graph graph, List<List<String>> paths, String result) {
+ List<Test> tests = new ArrayList<Test>();
+ for (List<String> path : paths) {
+ List<Node> nodes = new ArrayList<Node>();
+ for (String nodeName : path) {
+ nodes.add(graph.searchNodeByName(nodeName));
+ }
+ tests.add(new Test(nodes, result));
+ }
+ return tests;
+ }
+
+ private Verification evaluateIsolationResults( List<Test> tests, String source, String destination,
+ String middlebox) {
+ Verification v = new Verification();
+ boolean isSat = false;
+ int unsatCounter = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ isSat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is UNKNOWN because although '" + source
+ + "' cannot reach '" + middlebox + "' in any path from '" + source + "' to '"
+ + destination + "' which traverses middlebox '" + middlebox
+ + "' at least one reachability test between '" + source + "' and '" + middlebox
+ + "' returned UNKNOWN (see below all the paths that have been checked)");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsatCounter++;
+ }
+ }
+ if (isSat) {
+ v.setResult("UNSAT");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is UNSATISFIED because reachability between '"
+ + source + "' and '" + middlebox + "' is SATISFIED in at least one path between '" + source
+ + "' and '" + destination + "' which traverses middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (unsatCounter == tests.size()) {
+ v.setResult("SAT");
+ v.setComment("Isolation property with source '" + source + "', destination '" + destination
+ + "' and middlebox '" + middlebox + "' is SATISFIED because reachability between '" + source
+ + "' and '" + middlebox + "' is UNSATISFIED in all paths between '" + source + "' and '"
+ + destination + "' which traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ return v;
+
+ }
+
+ private void extractPathsWithMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (!middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+
+ }
+
+ private void extractPathsWithoutMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+
+ }
+
+ private Verification traversalVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
+
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> pathsBetweenSourceAndDestination = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", pathsBetweenSourceAndDestination);
+
+ eliminateLoopsInPaths(pathsBetweenSourceAndDestination);
+
+ printListsOfStrings("After loops removal", pathsBetweenSourceAndDestination);
+
+ if (pathsBetweenSourceAndDestination.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<Test> tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN");
+
+ List<List<String>> pathsWithMiddlebox = new ArrayList<List<String>>();
+ for (List<String> path : pathsBetweenSourceAndDestination) {
+ pathsWithMiddlebox.add(path);
+ }
+
+ extractPathsWithMiddlebox(pathsWithMiddlebox, middleboxNode.getName());
+
+ if (pathsWithMiddlebox.isEmpty()) {
+ return new Verification("UNSAT",
+ tests,
+ "There are no paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' which traverse middlebox '"
+ + middleboxNode.getName() + "'. See below all the available paths");
+ }
+
+ printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", pathsWithMiddlebox);
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("traversal");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, pathsWithMiddlebox, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+ }catch(Exception ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+ }
+
+ String traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
+ try{
+ generateTests( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+ }
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( pathsWithMiddlebox.size(),
+ traversalScenariosBasename,
+ traversalTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), pathsWithMiddlebox, graph, classFiles);
+
+ for (Test t : tests) {
+ if (t.getResult().equals("UNSAT")) {
+ return new Verification("UNSAT",
+ tests,
+ "There is at least a path between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traversing middlebox '"
+ + middleboxNode.getName() + "' where '" + sourceNode.getName()
+ + "' cannot reach '" + destinationNode.getName()
+ + "'. See below the paths that have been checked");
+ }
+ if (t.getResult().equals("UNKNOWN")) {
+ return new Verification("UNKNOWN",
+ tests,
+ "There is at least a path between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traversing middlebox '"
+ + middleboxNode.getName() + "' where it is not guaranteed that '"
+ + sourceNode.getName() + "' can effectively reach '"
+ + destinationNode.getName()
+ + "'. See below the paths that have been checked");
+ }
+ }
+
+ extractPathsWithoutMiddlebox(pathsBetweenSourceAndDestination, middleboxNode.getName());
+ printListsOfStrings("Paths without middlebox '" + middleboxNode.getName() + "'", pathsBetweenSourceAndDestination);
+
+ if (pathsBetweenSourceAndDestination.isEmpty()) {
+ return new Verification("SAT",
+ tests,
+ "All the paths between node '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "' traverse middlebox '"
+ + middleboxNode.getName() + "'");
+ }
+
+ tempDir = null;
+
+ try {
+ tempDir = createTempDir("traversal");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, pathsBetweenSourceAndDestination, chainsFile);
+
+ configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
+ generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
+
+ traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
+ generateTests( pathsBetweenSourceAndDestination.size(),
+ traversalScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ traversalTestsBasename);
+
+ sourceFiles = new ArrayList<File>();
+ classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( pathsBetweenSourceAndDestination.size(),
+ traversalScenariosBasename,
+ traversalTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ tests = runFiles(tempDir.getAbsolutePath(), pathsBetweenSourceAndDestination, graph, classFiles);
+
+ return evaluateTraversalResults(tests,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ middleboxNode.getName());
+
+ }
+
+ private Verification evaluateTraversalResults( List<Test> tests, String source, String destination,
+ String middlebox) {
+ Verification v = new Verification();
+ boolean isSat = false;
+ int unsatCounter = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ isSat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("There is at least one path from '" + source + "' to '" + destination
+ + "' that doesn't traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsatCounter++;
+ }
+ }
+ if (isSat) {
+ v.setResult("UNSAT");
+ v.setComment("There is at least one path from '" + source + "' to '" + destination
+ + "' that doesn't traverse middlebox '" + middlebox
+ + "' (see below all the paths that have been checked)");
+ }
+ else if (unsatCounter == tests.size()) {
+ v.setResult("SAT");
+ v.setComment("The only available paths from '" + source + "' to '" + destination
+ + "' are those that traverse middlebox '" + middlebox
+ + "' (see below the alternative paths that have been checked and are unusable)");
+ }
+ return v;
+ }
+
+ private Verification reachabilityVerification(Graph graph, Node sourceNode, Node destinationNode) {
+ Paths paths = getPaths(graph, sourceNode, destinationNode);
+
+ if (paths.getPath().size() == 0) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ List<List<String>> sanitizedPaths = sanitizePaths(paths);
+
+ printListsOfStrings("Before loops removal", sanitizedPaths);
+
+ eliminateLoopsInPaths(sanitizedPaths);
+
+ printListsOfStrings("After loops removal", sanitizedPaths);
+
+ if (sanitizedPaths.isEmpty()) {
+ return new Verification("UNSAT",
+ "There are no available paths between '" + sourceNode.getName() + "' and '"
+ + destinationNode.getName() + "'");
+ }
+
+ File tempDir = null;
+
+ try {
+ tempDir = createTempDir("reachability");
+ }
+ catch (IOException e) {
+ throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
+ }
+
+ String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
+ generateChainsFile(graph, sanitizedPaths, chainsFile);
+
+ String configFile = tempDir.getAbsolutePath() + "/config.json";
+ generateConfigFile(graph, configFile);
+
+ String reachabilityScenariosBasename = tempDir.getAbsolutePath() + "/ReachabilityScenario";
+ try{
+ generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
+ }catch(InternalServerErrorException ex){
+ testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
+ generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
+ }
+
+
+ String reachabilityTestsBasename = tempDir.getAbsolutePath() + "/ReachabilityTest";
+ try{
+ generateTests( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ reachabilityTestsBasename);
+ }catch(InternalServerErrorException ex){
+ testGenerator = generatorFolderForGrpc + "/test_generator.py";
+ generateTests( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ sourceNode.getName(),
+ destinationNode.getName(),
+ reachabilityTestsBasename);
+ }
+ List<File> sourceFiles = new ArrayList<File>();
+ List<File> classFiles = new ArrayList<File>();
+ prepareForCompilationAndExecution( sanitizedPaths.size(),
+ reachabilityScenariosBasename,
+ reachabilityTestsBasename,
+ sourceFiles,
+ classFiles);
+
+ compileFiles(sourceFiles, tempDir.getAbsolutePath());
+
+ List<Test> tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
+
+ return evaluateReachabilityResult(tests, sourceNode.getName(), destinationNode.getName());
+ }
+
+ private Verification evaluateReachabilityResult(List<Test> tests, String source, String destination) {
+ Verification v = new Verification();
+ boolean sat = false;
+ int unsat = 0;
+ for (Test t : tests) {
+ v.getTests().add(t);
+
+ if (t.getResult().equals("SAT")) {
+ sat = true;
+ }
+ else if (t.getResult().equals("UNKNOWN")) {
+ v.setResult("UNKNWON");
+ v.setComment("Reachability from '" + source + "' to '" + destination
+ + "' is unknown. See all the checked paths below");
+ }
+ else if (t.getResult().equals("UNSAT")) {
+ unsat++;
+ }
+ }
+ if (sat) {
+ v.setResult("SAT");
+ v.setComment("There is at least one path '" + source + "' can use to reach '" + destination
+ + "'. See all the available paths below");
+ }
+ else if (unsat == tests.size()) {
+ v.setResult("UNSAT");
+ v.setComment("There isn't any path '" + source + "' can use to reach '" + destination
+ + "'. See all the checked paths below");
+ }
+ return v;
+ }
+
+}