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

Improve integration of maraboupy (Python interface to Marabou)

See merge request laiser/caisar!137

bin/dune

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

bin/marabou_eval.py → bin/runMarabou.py

 #!/usr/bin/env python3
 """
-Adapted for quick evaluation of Marabou for CAISAR
+Modified by the AISER team, Software Safety and Security Laboratory, CEA-List.
+
+This file is part of CAISAR.
+This file is used for integrating Marabou, via its Python interface, in CAISAR.
 
 Top contributors (to current version):
     - Andrew Wu
@@ -12,33 +15,46 @@ 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 importlib.metadata import version
+
+from maraboupy import Marabou, MarabouCore  # type: ignore
+
 
-from maraboupy import Marabou
-from maraboupy import MarabouCore
+class WrongNetFormat(Exception):
+    def __init__(self, networkPath):
+        self.message = (
+            f"Network {networkPath} has an unrecognized extension."
+            f"The network must be in .pb, .nnet or .onnx format."
+        )
+        super().__init__(self.message)
 
 
 sys.path.insert(0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../"))
 
 
+def maraboupy_version(marabou_binary: str):
+    result = subprocess.run([marabou_binary, "--version"], capture_output=True, text=True)
+    if result.returncode != 0:
+        print(f"Error running {marabou_binary} --version")
+        sys.exit(1)
+
+    maraboupy_version = version("maraboupy")
+    output = result.stdout.strip()
+    if maraboupy_version in output:
+        return f"maraboupy {maraboupy_version}"
+
+    return sys.exit(1)
+
+
 def arguments():
-    parser = argparse.ArgumentParser(
-        description="Thin wrapper around Maraboupy executable"
-    )
+    parser = argparse.ArgumentParser(description="Thin wrapper around Maraboupy executable")
     parser.add_argument(
         "network",
         type=str,
@@ -46,15 +62,9 @@ def arguments():
         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"
-    )
+    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",
@@ -74,15 +84,17 @@ def arguments():
 
 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')}")
+            print(f"{maraboupy_version(marabou_binary)}")
         else:
+            assert args.network is not None
+            assert args.prop is not None
 
-            assert args.prop != None
             networkPath = args.network
             suffix = networkPath.split(".")[-1]
             if suffix == "nnet":
@@ -93,18 +105,17 @@ def main():
                 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
+                [marabou_binary] + ["--input-query={}".format(name)] + ["--timeout={}".format(timeout)] + unknown
             )
             os.remove(name)
 

caisar.opam

@@ -3,10 +3,8 @@ opam-version: "2.0"
 version: "1.0"
 synopsis:
   "A platform for characterizing the safety and robustness of artificial intelligence based software"
-maintainer: [
-  "LAISER team, Software Safety and Security Laboratory, CEA-List"
-]
-authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+maintainer: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
+authors: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
 license: "LGPL-2.1-only"
 homepage: "https://git.frama-c.com/pub/caisar"
 doc: "https://git.frama-c.com/pub/caisar"

config/caisar-detection-data.conf

@@ -54,12 +54,12 @@ driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP maraboupy]
-name = "Maraboupy"
-exec = "marabou_eval.py"
+name = "maraboupy"
+exec = "runMarabou.py"
 version_switch = "--version"
-version_regexp = "Maraboupy version \\([0-9.]+\\)"
+version_regexp = "maraboupy \\([0-9.]+\\)"
 version_ok  = "2.0.0"
-command = "%e %{nnet-onnx} %f "
+command = "%e %{nnet-onnx} %f --timeout %t"
 driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 

dune-project

@@ -10,8 +10,8 @@
 (generate_opam_files true)
 
 (license LGPL-2.1-only)
-(authors "LAISER team, Software Safety and Security Laboratory, CEA-List")
-(maintainers "LAISER team, Software Safety and Security Laboratory, CEA-List")
+(authors "AISER team, Software Safety and Security Laboratory, CEA-List")
+(maintainers "AISER team, Software Safety and Security Laboratory, CEA-List")
 (source (uri "git+https://git.frama-c.com/pub/caisar.git"))
 (bug_reports https://git.frama-c.com/pub/caisar/issues)
 (homepage https://git.frama-c.com/pub/caisar)

src/prover.ml

@@ -22,7 +22,7 @@
 
 type t =
   | Marabou
-  | Maraboupy [@name "Maraboupy"]
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]
@@ -38,6 +38,7 @@ let of_string prover =
   let prover = String.lowercase_ascii prover in
   match prover with
   | "marabou" -> Some Marabou
+  | "maraboupy" -> Some Maraboupy
   | "pyrat" -> Some Pyrat
   | "saver" -> Some Saver
   | "aimos" -> Some Aimos
@@ -48,7 +49,7 @@ let of_string prover =
 
 let to_string = function
   | Marabou -> "Marabou"
-  | Maraboupy -> "Maraboupy"
+  | Maraboupy -> "maraboupy"
   | Pyrat -> "PyRAT"
   | Saver -> "SAVer"
   | Aimos -> "AIMOS"

src/prover.mli

@@ -22,7 +22,7 @@
 
 type t = private
   | Marabou
-  | Maraboupy [@name "Maraboupy"]
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]

src/verification.ml

@@ -237,7 +237,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
   in
   let dataset_answers =
     match prover with
-    | Prover.Marabou ->
+    | Prover.Marabou | Maraboupy ->
       (* We turn each task in [dataset_tasks] into a list (ie, conjunction) of
          disjunctions of tasks. *)
       let tasks = List.map ~f:(Trans.apply Split.split_all) dataset_tasks in
@@ -345,7 +345,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         (* Turn [task] into a list (ie, conjunction) of disjunctions of
            tasks. *)
         match prover with
-        | Prover.Marabou -> Trans.apply Split.split_all task
+        | Prover.Marabou | Maraboupy -> Trans.apply Split.split_all task
         | Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
         | _ -> [ task ]
       in
@@ -368,7 +368,8 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
       let proof_strategy = Proof_strategy.apply_svm_prover_strategy in
       answer_saver limit config env config_prover ~proof_strategy task
     | Aimos -> answer_aimos limit config env config_prover dataset task
-    | (Marabou | Pyrat | Nnenum | ABCrown) when Option.is_some dataset ->
+    | (Marabou | Maraboupy | Pyrat | Nnenum | ABCrown)
+      when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
     | Marabou | Maraboupy | Pyrat | Nnenum | ABCrown ->

tests/autodetect.t

@@ -30,15 +30,14 @@ Test autodetect
   $ bin/abcrown.sh --version
   dummy-version
 
-  $ bin/marabou_eval.py --version
-  Maraboupy version 2.0.0
+  $ bin/runMarabou.py --version
+  maraboupy 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)
@@ -47,4 +46,5 @@ Test autodetect
   SAVer v1.0
   alpha-beta-CROWN dummy-version
   alpha-beta-CROWN dummy-version (ACAS)
+  maraboupy 2.0.0
   nnenum dummy-version

tests/bin/marabou_eval.py → tests/bin/runMarabou.py

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

tests/marabou.t

@@ -4,7 +4,7 @@ Test verify
   $ bin/Marabou --version
   1.0.+
 
-  $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - <<EOF
+  $ cat > file.mlw <<EOF
   > theory T
   >   use ieee_float.Float64
   >   use caisar.types.Vector
@@ -38,6 +38,70 @@ Test verify
   >       (nn @@ i)[1] .< (nn @@ i)[0] \/ (nn @@ i)[0] .< (nn @@ i)[1]
   > end
   > EOF
+
+  $ caisar verify --prover=Marabou --ltag=ProverSpec file.mlw
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  y0 <= 0.0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  y0 >= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y0 <= 0.0
+  y0 <= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y1 <= 0.0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y1 >= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.75
+  x0 <= 1.0
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  Goal G: Unknown ()
+  Goal H: Unknown ()
+  Goal I: Unknown ()
+  Goal J: Unknown ()
+
+  $ caisar verify --prover=maraboupy --ltag=ProverSpec file.mlw
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
   x0 <= 0.5