From a42de79292d9541db7865b54e93be2d0b6e6a094 Mon Sep 17 00:00:00 2001 From: "serena.spinoso" Date: Thu, 7 Sep 2017 10:22:39 +0200 Subject: update verigraph JIRA: PARSER-154 code optimizations about graph manipulation and formula generation. Change-Id: Idebef19b128281aa2bc40d1aeab6e208c7ddd93d Signed-off-by: serena.spinoso --- .../polito/escape/verify/service/GraphService.java | 129 --- .../verify/service/JsonValidationService.java | 136 --- .../escape/verify/service/NeighbourService.java | 182 --- .../polito/escape/verify/service/NodeService.java | 258 ----- .../escape/verify/service/ValidationUtils.java | 132 --- .../escape/verify/service/VerificationService.java | 1185 -------------------- 6 files changed, 2022 deletions(-) delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java delete mode 100644 verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java (limited to 'verigraph/src/main/java/it/polito/escape/verify/service') 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 deleted file mode 100644 index b34eb08..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/GraphService.java +++ /dev/null @@ -1,129 +0,0 @@ -/******************************************************************************* - * 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 graphs = DatabaseClass.getInstance().getGraphs(); - - public GraphService() { - - } - - public List getAllGraphs() { - return new ArrayList(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 nodeEntry : graph.getNodes().entrySet()){ - nodeEntry.getValue().setId(nodeEntry.getKey()); - - for (Map.Entry 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 nodeEntry : graph.getNodes().entrySet()){ - nodeEntry.getValue().setId(nodeEntry.getKey()); - - for (Map.Entry 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 deleted file mode 100644 index 1ac6c1f..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/JsonValidationService.java +++ /dev/null @@ -1,136 +0,0 @@ -/******************************************************************************* - * 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> iter = node.fields(); - - while (iter.hasNext()) { - Entry 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 deleted file mode 100644 index ecf4e69..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/NeighbourService.java +++ /dev/null @@ -1,182 +0,0 @@ -/******************************************************************************* - * 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 graphs = DatabaseClass.getInstance().getGraphs(); - - public List 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 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 neighbours = node.getNeighbours(); - return new ArrayList(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 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 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 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 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 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 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 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 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 deleted file mode 100644 index e6ad672..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/NodeService.java +++ /dev/null @@ -1,258 +0,0 @@ -/******************************************************************************* - * 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 graphs = DatabaseClass.getInstance().getGraphs(); - - public NodeService() { - - } - - public List 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 nodes = graph.getNodes(); - return new ArrayList(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 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 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(graph.getNodes())); - graphCopy.getNodes().remove(node.getId()); - - // int numberOfNeighbours = 0; - // for(Neighbour neighbour : node.getNeighbours().values()){ - // neighbour.setId(++numberOfNeighbours); - // } - - for (Map.Entry 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 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 nodes = graph.getNodes(); - - validateNode(graph, node); - - synchronized (this) { - node.setId(DatabaseClass.getInstance().getGraphNumberOfNodes(graphId) + 1); - } - - // int numberOfNeighbours = 0; - - for (Map.Entry 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 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 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 deleted file mode 100644 index 77ef4f7..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/ValidationUtils.java +++ /dev/null @@ -1,132 +0,0 @@ -/******************************************************************************* - * 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 deleted file mode 100644 index 1d31ae9..0000000 --- a/verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java +++ /dev/null @@ -1,1185 +0,0 @@ -/******************************************************************************* - * 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 endpoints = new ArrayList<>(); - List firewalls = new ArrayList<>(); - Map> 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()); - routingTable.put(node.getName() + "_" + node.getId() + "_out", new ArrayList()); - // 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()); - // 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 sanitizePath(String path) { - List newPath = new ArrayList(); - // 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> sanitizePaths(Paths paths) { - List> sanitizedPaths = new ArrayList>(); - for (String path : paths.getPath()) { - System.out.println("Original path: " + path); - List newPath = sanitizePath(path); - sanitizedPaths.add(newPath); - } - return sanitizedPaths; - } - - static private Map toMap(List lst) { - return lst.stream().collect(Collectors.groupingBy(s -> s, Collectors.counting())); - } - - private void eliminateLoopsInPaths(List> sanitizedPaths) { - List> pathsToBeRemoved = new ArrayList>(); - - for (List path : sanitizedPaths) { - Map occurrencesMap = toMap(path); - for (long occurrences : occurrencesMap.values()) { - if (occurrences > 1) { - pathsToBeRemoved.add(path); - break; - } - } - } - for (List path : pathsToBeRemoved) { - sanitizedPaths.remove(path); - } - } - - private void printListsOfStrings(String message, List> lists) { - System.out.println(message); - for (List 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> sanitizedPaths, String chainsFile) { - JSONObject root = new JSONObject(); - JSONArray chains = new JSONArray(); - - int chainCounter = 0; - - for (List path : sanitizedPaths) { - Iterator 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 scenarios = new ArrayList(); - List tests = new ArrayList(); - 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 sourceFiles, List 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 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 optionList = new ArrayList(); - // optionList.add("-classpath"); - // optionList.add(System.getProperty("java.class.path") + ":" + z3); - List optionList = new ArrayList(); - optionList.add("-d"); - optionList.add(folder); - DiagnosticCollector 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 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 runFiles(String folder, List> paths, Graph graph, List files) { - List tests = new ArrayList(); - 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 path = new ArrayList(); - 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> 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 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 sourceFiles = new ArrayList(); - List classFiles = new ArrayList(); - 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 extractTestsFromPaths(Graph graph, List> paths, String result) { - List tests = new ArrayList(); - for (List path : paths) { - List nodes = new ArrayList(); - for (String nodeName : path) { - nodes.add(graph.searchNodeByName(nodeName)); - } - tests.add(new Test(nodes, result)); - } - return tests; - } - - private Verification evaluateIsolationResults( List 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> sanitizedPaths, String middleboxName) { - List> pathsToBeRemoved = new ArrayList>(); - for (List path : sanitizedPaths) { - boolean middleboxFound = false; - for (String node : path) { - if (node.equals(middleboxName)) { - middleboxFound = true; - break; - } - } - if (!middleboxFound) { - pathsToBeRemoved.add(path); - } - } - - for (List path : pathsToBeRemoved) { - sanitizedPaths.remove(path); - } - - } - - private void extractPathsWithoutMiddlebox(List> sanitizedPaths, String middleboxName) { - List> pathsToBeRemoved = new ArrayList>(); - for (List path : sanitizedPaths) { - boolean middleboxFound = false; - for (String node : path) { - if (node.equals(middleboxName)) { - middleboxFound = true; - break; - } - } - if (middleboxFound) { - pathsToBeRemoved.add(path); - } - } - - for (List 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> 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 tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN"); - - List> pathsWithMiddlebox = new ArrayList>(); - for (List 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 sourceFiles = new ArrayList(); - List classFiles = new ArrayList(); - 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(); - classFiles = new ArrayList(); - 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 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> 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 sourceFiles = new ArrayList(); - List classFiles = new ArrayList(); - prepareForCompilationAndExecution( sanitizedPaths.size(), - reachabilityScenariosBasename, - reachabilityTestsBasename, - sourceFiles, - classFiles); - - compileFiles(sourceFiles, tempDir.getAbsolutePath()); - - List tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles); - - return evaluateReachabilityResult(tests, sourceNode.getName(), destinationNode.getName()); - } - - private Verification evaluateReachabilityResult(List 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; - } - -} -- cgit 1.2.3-korg