Initial code release

._dummy_.py

@@ -0,0 +1,2 @@
+# This file exists because the py_library rule in BUILD (that acts as a dummy
+# target for the pip imports) needs a src.

.bazelignore

@@ -0,0 +1 @@
+.docker_bazel

.bazelrc

@@ -0,0 +1,11 @@
+# Depset rule is for gRPC and Bazel 0.28.1
+build --incompatible_depset_is_not_iterable=false \
+--linkopt="-fopenmp" --linkopt="-lpthread" --linkopt="-m64" \
+--linkopt="-march=native" --linkopt="-O3" \
+--cxxopt="-fopenmp" --cxxopt="-lpthread" --cxxopt="-m64" \
+--cxxopt="-march=native" --cxxopt="-O3" \
+--copt="-fopenmp" --copt="-lpthread" \
+--copt="-march=native" --copt="-O3"  --copt="-m64" \
+--incompatible_disallow_dict_plus=false \
+--incompatible_string_join_requires_strings=false
+# run --run_under="runexec --no-container --walltimelimit 172800 --cores 0-15 --memlimit 17179869184 --output /dev/stdout --input - --"

.gitignore

@@ -0,0 +1,12 @@
+**/experiment_*
+*.csv
+*.log
+analysis_output
+ig_results
+**/bazel-*
+experiments/results/*
+.docker_bazel
+*.swp
+htmlcov
+*.coverage
+__pycache__

BUILD

@@ -0,0 +1,164 @@
+sh_library(
+    name = "pywrapper",
+    srcs = ["pywrapper.sh"],
+    visibility = ["//:__subpackages__"],
+)
+
+# https://stackoverflow.com/questions/47036855
+py_runtime(
+    name = "python-3",
+    files = ["@python_3//:installdir"],
+    interpreter = "pywrapper.sh",
+    python_version = "PY3",
+)
+
+# https://github.com/bazelbuild/rules_python/blob/master/proposals/2019-02-12-design-for-a-python-toolchain.md
+load("@bazel_tools//tools/python:toolchain.bzl", "py_runtime_pair")
+
+constraint_value(
+    name = "python3_constraint",
+    constraint_setting = "@bazel_tools//tools/python:py3_interpreter_path",
+)
+
+platform(
+    name = "python3_platform",
+    constraint_values = [
+        ":python3_constraint",
+    ],
+)
+
+py_runtime_pair(
+    name = "python3_runtime_pair",
+    py3_runtime = ":python-3",
+)
+
+toolchain(
+    name = "python3-toolchain",
+    # Since the Python interpreter is invoked at runtime on the target
+    # platform, there's no need to specify execution platform constraints here.
+    target_compatible_with = [
+        # Make sure this toolchain is only selected for a target platform that
+        # advertises that it has interpreters available under /usr/weirdpath.
+        # ":python3_constraint",
+    ],
+    toolchain = "//:python3_runtime_pair",
+    toolchain_type = "@bazel_tools//tools/python:toolchain_type",
+)
+
+# This seems to be the way Google is doing it now:
+# https://github.com/bazelbuild/rules_python/issues/119
+# See https://github.com/pypa/pip/issues/3826 for why we need the --system flag
+# on the pip call. For newer versions of pip, you may have to add
+# --no-build-isolation.
+genrule(
+    name = "install-pip-packages",
+    srcs = ["requirements.txt"],
+    cmd = """
+    PYTHON=$(location pywrapper.sh)
+    PIP="$$PYTHON -m pip"
+
+    DUMMY_HOME=/tmp/$$(head /dev/urandom | tr -dc A-Za-z0-9 | head -c 8)
+    rm -rf $$DUMMY_HOME
+    export HOME=$$DUMMY_HOME
+
+    PIP_INSTALL="$$PIP \
+        install --no-cache-dir --disable-pip-version-check \
+        --target=$@"
+
+    # Install the correct version of Torch
+    mkdir -p $$DUMMY_HOME
+    $$PIP_INSTALL torch==1.2.0+cpu -f https://download.pytorch.org/whl/torch_stable.html
+
+    # Install the other requirements.
+    mkdir -p $$DUMMY_HOME
+    $$PIP_INSTALL -r requirements.txt
+
+    # The custom typing package installed as a dependency doesn't seem to work
+    # well.
+    rm -rf $@/typing-*
+    rm -rf $@/typing.py
+
+    rm -rf $$DUMMY_HOME
+    """,
+    outs = ["pip_packages"],
+    tools = ["@python_3//:installdir", ":pywrapper.sh"],
+    visibility = ["//:__subpackages__"],
+)
+
+py_library(
+    name = "pip-packages",
+    data = [":install-pip-packages"],
+    srcs = ["._dummy_.py"],
+    imports = ["pip_packages"],
+    visibility = ["//:__subpackages__"],
+)
+
+# Make the thicker-bordered plane SVG.
+genrule(
+    name = "thicker-plane",
+    srcs = ["@plane_svg//file", "pywrapper.sh"],
+    outs = ["plane.png"],
+    cmd = """
+    PLANESVG=$(location @plane_svg//file)
+    PYTHON=$(location pywrapper.sh)
+    export PYTHONPATH=$(location //:pip_packages)
+
+    sed -i -e \
+        's/id="path5724" /id="path5724" stroke="white" fill="black" stroke-width="10" /' \
+        $$PLANESVG
+
+    $$PYTHON -m cairosvg $$PLANESVG -o plane.png --output-width 4965
+    cp plane.png $@
+    """,
+    tools = [
+        "@python_3//:installdir",
+        "//:pip_packages",
+    ],
+    visibility = ["//:__subpackages__"],
+)
+
+# For generating the coverage report.
+sh_binary(
+    name = "coverage_report",
+    srcs = ["coverage_report.sh"],
+    data = [
+        "@python_3//:installdir",
+        "//:pip_packages",
+        "//:pywrapper"
+    ],
+)
+
+# For wheel-ifying the Python code.
+# Thanks!
+# https://hynek.me/articles/sharing-your-labor-of-love-pypi-quick-and-dirty/
+genrule(
+    name = "wheel",
+    srcs = [
+        "pysyrenn",
+        "requirements.txt",
+        "LICENSE",
+        "pip_info/__metadata__.py",
+        "pip_info/README.md",
+        "pip_info/setup.cfg",
+        "pip_info/setup.py",
+    ],
+    outs = ["pysyrenn.dist"],
+    cmd = """
+    PYTHON=$(location pywrapper)
+    export PYTHONPATH=$$PWD:$(location //:pip_packages)
+
+    mkdir -p syrenn_proto
+    cp -Lr $(locations //syrenn_proto:syrenn_py_proto) syrenn_proto
+    touch syrenn_proto/__init__.py
+    cp pip_info/* .
+    $$PYTHON setup.py sdist bdist_wheel
+
+    cp -r dist $@
+    """,
+    tools = [
+        "@python_3//:installdir",
+        "pywrapper",
+        "//:pip_packages",
+        "//syrenn_proto:syrenn_py_proto",
+    ],
+)

Dockerfile

@@ -0,0 +1,46 @@
+FROM ubuntu:18.04
+
+LABEL maintainer="[email protected]"
+LABEL autodelete="True"
+
+# https://stackoverflow.com/questions/24288616#answer-48536224
+ARG UID=1000
+
+# Bazel, build dependencies, benchexec dependencies, and docker-in-docker
+# dependencies.
+RUN apt-get update && apt-get install -y \
+    pkg-config zip g++ zlib1g-dev unzip python2.7 python-pip python3 \
+    build-essential curl git cmake libcairo2 libffi-dev libgmp3-dev \
+    zlib1g-dev zip \
+    apt-transport-https ca-certificates gnupg-agent software-properties-common
+
+# Install Docker.
+RUN curl -fsSL https://download.docker.com/linux/ubuntu/gpg | apt-key add -
+RUN add-apt-repository \
+        "deb [arch=amd64] https://download.docker.com/linux/ubuntu \
+        $(lsb_release -cs) \
+        stable"
+RUN apt-get update && apt-get install -y docker-ce docker-ce-cli containerd.io
+
+# Install Bazel.
+WORKDIR /
+RUN curl -OL https://github.com/bazelbuild/bazel/releases/download/0.28.1/bazel-0.28.1-installer-linux-x86_64.sh
+RUN chmod +x bazel-0.28.1-installer-linux-x86_64.sh
+RUN ./bazel-0.28.1-installer-linux-x86_64.sh
+
+# Install benchexec.
+RUN curl -OL https://github.com/sosy-lab/benchexec/releases/download/2.0/benchexec_2.0-1_all.deb
+RUN apt install -y --install-recommends ./benchexec_2.0-1_all.deb
+
+RUN rm -rf /var/lib/apt/lists/*
+
+# Store Bazel outputs on /iovol/.docker_bazel, which will be loaded at runtime.
+# This allows us to cache Bazel build artifacts across Docker invocations.
+RUN echo "startup --output_user_root=/iovol/.docker_bazel" > /etc/bazel.bazelrc
+
+RUN useradd -u $UID -ms /bin/bash docker_user
+RUN adduser docker_user benchexec
+RUN adduser docker_user docker
+
+EXPOSE 50051
+USER docker_user

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2019 Matthew A. Sotoudeh and Aditya V. Thakur
+
+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.

Makefile

@@ -0,0 +1,51 @@
+.PHONY: pysyrenn_coverage start_server acas_lines_experiment \
+        integrated_gradients_experiment linearity_hypothesis_experiment \
+        exactline_experiments toy_examples_experiment acas_planes_experiment \
+	model_checking_experiment netpatch_experiment plane_experiments \
+	all_experiments
+
+pysyrenn_coverage:
+	bazel test //pysyrenn/...
+	bazel run coverage_report
+
+start_server:
+	bazel run syrenn_server:server
+
+# Experiments from [1]
+acas_lines_experiment:
+	@echo "Running the ACAS Xu Lines experiment"
+	bazel run experiments:acas_lines
+
+integrated_gradients_experiment:
+	@echo "Running the Integrated Gradinets experiment"
+	bazel run experiments:integrated_gradients
+
+linearity_hypothesis_experiment:
+	@echo "Running the Linearity Hypothesis experiment"
+	bazel run experiments:linearity_hypothesis
+
+exactline_experiments: acas_lines_experiment integrated_gradients_experiment \
+		       linearity_hypothesis_experiment
+
+# Experiments from [2]
+toy_examples_experiment:
+	@echo "Running the Toy Examples experiment"
+	bazel run experiments:toy_examples
+
+acas_planes_experiment:
+	@echo "Running the ACAS Xu Planes experiment"
+	bazel run experiments:acas_planes
+
+model_checking_experiment:
+	@echo "Running the Bounded Model Checking experiment"
+	bazel run experiments:model_checking
+
+netpatch_experiment:
+	@echo "Running the Network Patching experiment"
+	bazel run experiments:netpatch
+
+plane_experiments: toy_examples_experiment acas_planes_experiment \
+		   model_checking_experiment netpatch_experiment
+
+# Run experiments from [1] and [2]
+all_experiments: exactline_experiments plane_experiments