Merge branch 'feature/varasse/maraboupy' into 'master'

Add support for Maraboupy

See merge request laiser/caisar!135

.gitlab-ci.yml

@@ -45,7 +45,7 @@ test:
   stage: test
   script:
     - nix --extra-experimental-features "nix-command flakes" build
-    - nix --extra-experimental-features "nix-command flakes" flake check
+    - nix --extra-experimental-features "nix-command flakes" flake check -L
 
 ## Manual generation of the documentation
 

bin/dune

@@ -4,4 +4,5 @@
  (files
   (dummyversion.py as dummyversion.py)
   (nnenum.sh as nnenum.sh)
+  (marabou_eval.py as marabou_eval.py)
   (abcrown.sh as abcrown.sh)))

bin/marabou_eval.py

+#!/usr/bin/env python3
+"""
+Adapted for quick evaluation of Marabou for CAISAR
+
+Top contributors (to current version):
+    - Andrew Wu
+
+This file is part of the Marabou project.
+Copyright (c) 2017-2021 by the authors listed in the file AUTHORS
+in the top-level source directory) and their institutional affiliations.
+All rights reserved. See the file COPYING in the top-level source
+directory for licensing information.
+"""
+
+
+class WrongNetFormat(Exception):
+    def __init__(self, networkPath):
+        self.message = f"Network {networkPath} not in onnx, pb or nnet format!"
+        super().__init__(self.message)
+
+
+import argparse
+from importlib.metadata import version
+import os
+import pathlib
+import shutil
+import subprocess
+import sys
+import tempfile
+
+from maraboupy import Marabou
+from maraboupy import MarabouCore
+
+
+sys.path.insert(0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../"))
+
+
+def arguments():
+    parser = argparse.ArgumentParser(
+        description="Thin wrapper around Maraboupy executable"
+    )
+    parser.add_argument(
+        "network",
+        type=str,
+        nargs="?",
+        default=None,
+        help="The network file name, the extension can be only .pb, .nnet, and .onnx",
+    )
+    parser.add_argument(
+        "prop", type=str, nargs="?", default=None, help="The property file name"
+    )
+    parser.add_argument(
+        "-t", "--timeout", type=int, default=10, help="Timeout in seconds"
+    )
+    parser.add_argument(
+        "--temp-dir", type=str, default="/tmp/", help="Temporary directory"
+    )
+    marabou_path = shutil.which("Marabou")
+    parser.add_argument(
+        "--marabou-binary",
+        type=str,
+        default=marabou_path,
+        help="The path to Marabou binary",
+    )
+    parser.add_argument(
+        "--version",
+        action="store_true",
+        help="Output a version string if Maraboupy is present and exit",
+    )
+    parser.set_defaults(version=False)
+
+    return parser
+
+
+def main():
+    args, unknown = arguments().parse_known_args()
+    marabou_binary = args.marabou_binary
+    if not os.access(marabou_binary, os.X_OK):
+        sys.exit('"{}" does not exist or is not executable'.format(marabou_binary))
+    else:
+        if args.version:
+            print(f"Maraboupy version {version('maraboupy')}")
+        else:
+
+            assert args.prop != None
+            networkPath = args.network
+            suffix = networkPath.split(".")[-1]
+            if suffix == "nnet":
+                network = Marabou.read_nnet(networkPath)
+            elif suffix == "pb":
+                network = Marabou.read_tf(networkPath)
+            elif suffix == "onnx":
+                network = Marabou.read_onnx(networkPath)
+            else:
+                raise WrongNetFormat(networkPath)
+            query = network.getInputQuery()
+            MarabouCore.loadProperty(query, args.prop)
+            temp = tempfile.NamedTemporaryFile(dir=args.temp_dir, delete=False)
+            name = temp.name
+            timeout = args.timeout
+            MarabouCore.saveQuery(query, name)
+            print("Running Marabou with the following arguments: ", unknown)
+            subprocess.run(
+                [marabou_binary]
+                + ["--input-query={}".format(name)]
+                + ["--timeout={}".format(timeout)]
+                + unknown
+            )
+            os.remove(name)
+
+
+if __name__ == "__main__":
+    main()

config/caisar-detection-data.conf

@@ -53,6 +53,16 @@ command = "%e %{nnet-onnx} %f --timeout %t --snc --initial-divides=4 --num-onlin
 driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
+[ATP maraboupy]
+name = "Maraboupy"
+exec = "marabou_eval.py"
+version_switch = "--version"
+version_regexp = "Maraboupy version \\([0-9.]+\\)"
+version_ok  = "2.0.0"
+command = "%e %{nnet-onnx} %f "
+driver = "%{config}/drivers/marabou.drv"
+use_at_auto_level = 1
+
 [ATP pyrat]
 name = "PyRAT"
 exec = "pyrat.py"

tests/autodetect.t

@@ -30,11 +30,15 @@ Test autodetect
   $ bin/abcrown.sh --version
   dummy-version
 
+  $ bin/marabou_eval.py --version
+  Maraboupy version 2.0.0
+
   $ caisar config -d
   AIMOS 1.0
   Alt-Ergo 2.4.0
   CVC5 1.0.2
   Marabou 1.0.+
+  Maraboupy 2.0.0
   PyRAT 1.1
   PyRAT 1.1 (ACAS)
   PyRAT 1.1 (ACASd)

tests/bin/marabou_eval.py

+#!/bin/sh -e
+
+case $1 in
+    --version)
+        echo "Maraboupy version 2.0.0"
+        ;;
+    *)
+        echo "PWD: $(pwd)"
+        echo "NN: $2"
+        test -e $2 || (echo "Cannot find the NN file" && exit 1)
+        echo "Goal:"
+        cat $4
+        echo "Result = Unknown"
+esac