first pass to barriernet

NNet/.coveragerc

@@ -0,0 +1,3 @@
+[report]
+exclude_lines =
+    if __name__ == '__main__':

NNet/.gitignore

@@ -0,0 +1,2 @@
+*.ipynb
+*pyc

NNet/.travis.yml

@@ -0,0 +1,11 @@
+language: python
+python:
+  - "3.6"
+install:
+  - pip install -r test_requirements.txt
+script:
+  - python -m pytest --cov=utils --cov=python --cov=converters test 
+after_success:
+  - coveralls
+notifications:
+  email: false

NNet/LICENSE

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2018 Stanford Intelligent Systems Laboratory
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

NNet/README.md

@@ -0,0 +1,36 @@
+## NNet Repository
+
+[![Build Status](https://travis-ci.org/sisl/NNet.svg?branch=master)](https://travis-ci.org/sisl/NNet)
+[![Coverage Status](https://coveralls.io/repos/github/sisl/NNet/badge.svg?branch=master&service=github)](https://coveralls.io/github/sisl/NNet?branch=master)
+
+### Introduction
+The .nnet file format for fully connected ReLU networks was originially created in 2016 to define aircraft collision avoidance neural networks in a human-readable text document. Since then it was incorporated into the Reluplex repository and used to define benchmark neural networks. This format is a simple text-based format for feed-forward, fully-connected, ReLU-activated neural networks. It is not affiliated with Neuroph or other frameworks that produce files with the .nnet extension.
+
+This repository contains documentation for the .nnet format as well as useful functions for working with the networks. The nnet folder contains example neural network files. The converters folder contains functions to convert the .nnet files to Tensorflow, ONNX, and Keras formats and vice-versa. The python, julia, and cpp folders contain python, julia, and C++ functions for reading and evaluating .nnet networks. The examples folder provides python examples for using the available functions.
+
+This repository is set up as a python package. To run the examples, make sure that the folder in which this repository resides (the parent directory of NNet) is added to the PYTHONPATH environment variable.
+
+### File format of .nnet
+The file begins with header lines, some information about the network architecture, normalization information, and then model parameters. Line by line:<br/><br/>
+    **1**: Header text. This can be any number of lines so long as they begin with "//"<br/>
+    **2**: Four values: Number of layers, number of inputs, number of outputs, and maximum layer size<br/>
+    **3**: A sequence of values describing the network layer sizes. Begin with the input size, then the size of the first layer, second layer, and so on until the output layer size<br/>
+    **4**: A flag that is no longer used, can be ignored<br/>
+    **5**: Minimum values of inputs (used to keep inputs within expected range)<br/>
+    **6**: Maximum values of inputs (used to keep inputs within expected range)<br/>
+    **7**: Mean values of inputs and one value for all outputs (used for normalization)<br/>
+    **8**: Range values of inputs and one value for all outputs (used for normalization)<br/>
+    **9+**: Begin defining the weight matrix for the first layer, followed by the bias vector. The weights and biases for the second layer follow after, until the weights and biases for the output layer are defined.<br/>
+
+The minimum/maximum input values are used to define the range of input values seen during training, which can be used to ensure input values remain in the training range. Each input has its own value.
+
+The mean/range values are the values used to normalize the network training data before training the network. The normalization substracts the mean and divides by the range, giving a distribution that is zero mean and unit range. Therefore, new inputs to the network should be normalized as well, so there is a mean/range value for every input to the network. There is also an additional mean/range value for the network outputs, but just one value for all outputs. The raw network outputs can be re-scaled by multiplying by the range and adding the mean.
+
+### Writing .nnet files
+In the utils folder, the file writeNNet.py contains a python method for writing neural network data to a .nnet file. The main method, writeNNet, requires a list of weights, biases, minimum input values, maximum input values, mean of inputs/ouput, and range of inputs/output, and a filename to write the neural network.
+
+### Loading and evaluating .nnet files
+There are three folders for C++, Julia, and Python examples. Each subfolder contains a nnet.* file that contains functions for loading the network from a .nnet file and then evaluating a set of inputs given the loaded model. There are examples in each folder to demonstrate how the functions can be used.
+
+## License
+This code is licensed under the MIT license. See LICENSE for details.

NNet/converters/nnet2onnx.py

@@ -0,0 +1,86 @@
+import numpy as np 
+import sys
+import onnx
+from onnx import helper, numpy_helper, TensorProto
+from NNet.utils.readNNet import readNNet
+from NNet.utils.normalizeNNet import normalizeNNet
+
+def nnet2onnx(nnetFile, onnxFile="", outputVar = "y_out", inputVar="X", normalizeNetwork=False):
+    '''
+    Convert a .nnet file to onnx format
+    Args:
+        nnetFile: (string) .nnet file to convert to onnx
+        onnxFile: (string) Optional, name for the created .onnx file
+        outputName: (string) Optional, name of the output variable in onnx
+        normalizeNetwork: (bool) If true, adapt the network weights and biases so that 
+                                 networks and inputs do not need to be normalized. Default is False.
+    '''
+    if normalizeNetwork:
+        weights, biases = normalizeNNet(nnetFile)
+    else:
+        weights, biases = readNNet(nnetFile)
+
+    inputSize = weights[0].shape[1]
+    outputSize = weights[-1].shape[0]
+    numLayers = len(weights)
+
+    # Default onnx filename if none specified
+    if onnxFile=="":
+        onnxFile = nnetFile[:-4]+'onnx'
+
+    # Initialize graph
+    inputs = [helper.make_tensor_value_info(inputVar,   TensorProto.FLOAT, [inputSize])]
+    outputs = [helper.make_tensor_value_info(outputVar, TensorProto.FLOAT, [outputSize])]
+    operations = []
+    initializers = []
+
+    # Loop through each layer of the network and add operations and initializers
+    for i in range(numLayers):
+
+        # Use outputVar for the last layer
+        outputName = "H%d"%i
+        if i==numLayers-1: 
+            outputName = outputVar
+
+        # Weight matrix multiplication
+        operations.append(helper.make_node("MatMul",["W%d"%i,inputVar],["M%d"%i]))
+        initializers.append(numpy_helper.from_array(weights[i].astype(np.float32),name="W%d"%i))
+
+        # Bias add 
+        operations.append(helper.make_node("Add",["M%d"%i,"B%d"%i],[outputName]))
+        initializers.append(numpy_helper.from_array(biases[i].astype(np.float32),name="B%d"%i))
+
+        # Use Relu activation for all layers except the last layer
+        if i<numLayers-1: 
+            operations.append(helper.make_node("Relu",["H%d"%i],["R%d"%i]))
+            inputVar = "R%d"%i
+
+    # Create the graph and model in onnx
+    graph_proto = helper.make_graph(operations,"nnet2onnx_Model",inputs, outputs,initializers)
+    model_def = helper.make_model(graph_proto)
+
+    # Print statements
+    print("Converted NNet model at %s"%nnetFile)
+    print("    to an ONNX model at %s"%onnxFile)
+
+    # Additional print statements if desired
+    #print("\nReadable GraphProto:\n")
+    #print(helper.printable_graph(graph_proto))
+
+    # Save the ONNX model
+    onnx.save(model_def, onnxFile)
+
+
+if __name__ == '__main__':
+    # Read user inputs and run nnet2onnx function for different numbers of inputs
+    if len(sys.argv)>1:
+        nnetFile = sys.argv[1]
+        if len(sys.argv)>2:
+            onnxFile = sys.argv[2]
+            if len(sys.argv)>3:
+                outputName = argv[3]
+                nnet2onnx(nnetFile,onnxFile,outputName)
+            else: nnet2onnx(nnetFile,onnxFile)
+        else: nnet2onnx(nnetFile)
+    else:
+        print("Need to specify which .nnet file to convert to ONNX!")

NNet/converters/nnet2pb.py

@@ -0,0 +1,85 @@
+import tensorflow as tf
+import numpy as np 
+import sys
+from tensorflow.python.framework import graph_util
+import os
+os.environ["CUDA_VISIBLE_DEVICES"] = "-1"
+from NNet.utils.readNNet import readNNet
+from NNet.utils.normalizeNNet import normalizeNNet
+
+def nnet2pb(nnetFile, pbFile="", output_node_names = "y_out", normalizeNetwork=False):
+    '''
+    Read a .nnet file and create a frozen Tensorflow graph and save to a .pb file
+    
+    Args:
+        nnetFile (str): A .nnet file to convert to Tensorflow format
+        pbFile (str, optional): Name for the created .pb file. Default: ""
+        output_node_names (str, optional): Name of the final operation in the Tensorflow graph. Default: "y_out"
+    '''
+    if normalizeNetwork:
+        weights, biases = normalizeNNet(nnetFile)
+    else:
+        weights, biases = readNNet(nnetFile)
+    inputSize = weights[0].shape[1]
+
+    # Default pb filename if none are specified
+    if pbFile=="":
+        pbFile = nnetFile[:-4]+'pb'
+
+    # Reset tensorflow and load a session using only CPUs
+    tf.reset_default_graph()
+    sess = tf.Session()
+
+    # Define model and assign values to tensors
+    currentTensor = tf.placeholder(tf.float32, [None, inputSize],name='input')
+    for i in range(len(weights)):
+        W = tf.get_variable("W%d"%i, shape=weights[i].T.shape)
+        b = tf.get_variable("b%d"%i, shape=biases[i].shape)
+
+        # Use ReLU for all but last operation, and name last operation to desired name
+        if i!=len(weights)-1:
+            currentTensor = tf.nn.relu(tf.matmul(currentTensor ,W) + b)
+        else:
+            currentTensor =  tf.add(tf.matmul(currentTensor ,W), b,name=output_node_names)
+
+        # Assign values to tensors
+        sess.run(tf.assign(W,weights[i].T))
+        sess.run(tf.assign(b,biases[i]))
+
+    # Freeze the graph to write the pb file
+    freeze_graph(sess,pbFile,output_node_names)
+
+def freeze_graph(sess, output_graph_name, output_node_names):
+    '''
+    Given a session with a graph loaded, save only the variables needed for evaluation to a .pb file
+    
+    Args:
+        sess (tf.session): Tensorflow session where graph is defined
+        output_graph_name (str): Name of file for writing frozen graph
+        output_node_names (str): Name of the output operation in the graph, comma separated if there are multiple output operations
+    '''
+
+    input_graph_def = tf.get_default_graph().as_graph_def()
+    output_graph_def = graph_util.convert_variables_to_constants(
+        sess,                        # The session is used to retrieve the weights
+        input_graph_def,             # The graph_def is used to retrieve the nodes 
+        output_node_names.split(",") # The output node names are used to select the useful nodes
+    ) 
+
+    # Finally we serialize and dump the output graph to the file
+    with tf.gfile.GFile(output_graph_name, "w") as f:
+        f.write(output_graph_def.SerializeToString())
+
+if __name__ == '__main__':
+    # Read user inputs and run writePB function
+    if len(sys.argv)>1:
+        nnetFile = sys.argv[1]
+        pbFile = ""
+        output_node_names = "y_out"
+        if len(sys.argv)>2:
+            pbFile = sys.argv[2]
+        if len(sys.argv)>3:
+            output_node_names = argv[3]
+        nnet2pb(nnetFile,pbFile,output_node_names)
+    else:
+        print("Need to specify which .nnet file to convert to Tensorflow frozen graph!")

NNet/converters/onnx2nnet.py

@@ -0,0 +1,129 @@
+import numpy as np
+import sys
+import onnx
+from onnx import numpy_helper
+from NNet.utils.writeNNet import writeNNet
+
+def onnx2nnet(onnxFile, inputMins=None, inputMaxes=None, means=None, ranges=None, nnetFile="", inputName="", outputName=""):
+    '''
+    Write a .nnet file from an onnx file
+    Args:
+        onnxFile: (string) Path to onnx file
+        inputMins: (list) optional, Minimum values for each neural network input.
+        inputMaxes: (list) optional, Maximum values for each neural network output.
+        means: (list) optional, Mean value for each input and value for mean of all outputs, used for normalization
+        ranges: (list) optional, Range value for each input and value for range of all outputs, used for normalization
+        inputName: (string) optional, Name of operation corresponding to input.
+        outputName: (string) optional, Name of operation corresponding to output.
+    '''
+
+    if nnetFile=="":
+        nnetFile = onnxFile[:-4] + 'nnet'
+
+    model = onnx.load(onnxFile)
+    graph = model.graph
+
+    if not inputName:
+        assert len(graph.input)==1
+        inputName = graph.input[0].name
+    if not outputName:
+        assert len(graph.output)==1
+        outputName = graph.output[0].name
+
+    # Search through nodes until we find the inputName.
+    # Accumulate the weight matrices and bias vectors into lists.
+    # Continue through the network until we reach outputName.
+    # This assumes that the network is "frozen", and the model uses initializers to set weight and bias array values.
+    weights = []
+    biases = []
+
+    # Loop through nodes in graph
+    for node in graph.node:
+
+        # Ignore nodes that do not use inputName as an input to the node
+        if inputName in node.input:
+
+            # This supports three types of nodes: MatMul, Add, and Relu
+            # The .nnet file format specifies only feedforward fully-connected Relu networks, so
+            # these operations are sufficient to specify nnet networks. If the onnx model uses other 
+            # operations, this will break.
+            if node.op_type=="MatMul":
+                assert len(node.input)==2
+
+                # Find the name of the weight matrix, which should be the other input to the node
+                weightIndex=0
+                if node.input[0]==inputName:
+                    weightIndex=1
+                weightName = node.input[weightIndex]
+
+                # Extract the value of the weight matrix from the initializers
+                weights+= [numpy_helper.to_array(inits) for inits in graph.initializer if inits.name==weightName]
+
+                # Update inputName to be the output of this node
+                inputName = node.output[0]
+
+            elif node.op_type=="Add":
+                assert len(node.input)==2
+
+                # Find the name of the bias vector, which should be the other input to the node
+                biasIndex=0
+                if node.input[0]==inputName:
+                    biasIndex=1
+                biasName = node.input[biasIndex]
+
+                # Extract the value of the bias vector from the initializers
+                biases+= [numpy_helper.to_array(inits) for inits in graph.initializer if inits.name==biasName]
+
+                # Update inputName to be the output of this node
+                inputName = node.output[0]
+
+            # For the .nnet file format, the Relu's are implicit, so we just need to update the input
+            elif node.op_type=="Relu":
+                inputName = node.output[0]
+
+            # If there is a different node in the model that is not supported, through an error and break out of the loop
+            else:
+                print("Node operation type %s not supported!"%node.op_type)
+                weights = []
+                biases=[]
+                break
+
+            # Terminate once we find the outputName in the graph
+            if outputName == inputName:
+                break
+
+    # Check if the weights and biases were extracted correctly from the graph
+    if outputName==inputName and len(weights)>0 and len(weights)==len(biases):
+
+        inputSize = weights[0].shape[0]
+
+        # Default values for input bounds and normalization constants
+        if inputMins is None: inputMins = inputSize*[np.finfo(np.float32).min]
+        if inputMaxes is None: inputMaxes = inputSize*[np.finfo(np.float32).max]
+        if means is None: means = (inputSize+1)*[0.0]
+        if ranges is None: ranges = (inputSize+1)*[1.0]
+
+        # Print statements
+        print("Converted ONNX model at %s"%onnxFile)
+        print("    to an NNet model at %s"%nnetFile)
+
+        # Write NNet file
+        writeNNet(weights,biases,inputMins,inputMaxes,means,ranges,nnetFile)
+
+    # Something went wrong, so don't write the NNet file
+    else:
+        print("Could not write NNet file!")
+
+if __name__ == '__main__':
+    # Read user inputs and run onnx2nnet function
+    # If non-default values of input bounds and normalization constants are needed, 
+    # this function should be run from a script instead of the command line
+    if len(sys.argv)>1:
+        print("WARNING: Using the default values of input bounds and normalization constants")
+        onnxFile = sys.argv[1]
+        if len(sys.argv)>2:
+            nnetFile = sys.argv[2]
+            onnx2nnet(onnxFile,nnetFile=nnetFile)
+        else: onnx2nnet(onnxFile)
+    else:
+        print("Need to specify which ONNX file to convert to .nnet!")