diff options
Diffstat (limited to 'verigraph/src/main/java/it/polito/escape/verify/service')
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; + } + +} |