Add post-install testing for ocaml binding. (#5617)

* Add path flags for cc loader (linux). * Fix os linking and loading problem (maybe on #4840). * Add post-install test of OCaml binding on ubuntu. * Minor. * Tentative CI for macos.
Z3Prover · Oct 25, 2021 · 0660765 · 0660765
1 parent 3a3cef8
commit 0660765
Show file tree

Hide file tree

Showing 2 changed files with 126 additions and 5 deletions.
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
@@ -44,28 +44,74 @@ jobs:
       - template: scripts/test-regressions.yml
 
 - job: "Ubuntu20OCaml"
-  displayName: "Ubuntu 20 with ocaml"
+  displayName: "Ubuntu 20 with OCaml"
   pool:
     vmImage: "Ubuntu-20.04"
   steps:
     - script: sudo apt-get install ocaml opam libgmp-dev
     - script: opam init -y
     - script: eval `opam config env`; opam install zarith ocamlfind -y
-    - script: eval `opam config env`; python scripts/mk_make.py --ml --staticlib
+    - script: eval `opam config env`; python scripts/mk_make.py --ml
     - script: |
         set -e
         cd build
-        eval `opam config env` 
+        eval `opam config env`
         make -j3
         make -j3 examples
         make -j3 test-z3
+        ./ml_example.byte
         ./ml_example
         cd ..
+    - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.*
+    - script: |
+        set -e
+        cd build
+        eval `opam config env`
+        make -j3
+        make -j3 _ex_ml_example_post_install
+        ./ml_example_shared.byte
+        ./ml_example_shared_custom.byte
+        ./ml_example_shared
+      cd ..
     - template: scripts/test-z3.yml
     - template: scripts/test-regressions.yml
     - template: scripts/generate-doc.yml
 
 
+- job: "Ubuntu20OCamlStatic"
+  displayName: "Ubuntu 20 with OCaml on z3-static"
+  pool:
+    vmImage: "Ubuntu-20.04"
+  steps:
+    - script: sudo apt-get install ocaml opam libgmp-dev
+    - script: opam init -y
+    - script: eval `opam config env`; opam install zarith ocamlfind -y
+    - script: eval `opam config env`; python scripts/mk_make.py --ml --staticlib
+    - script: |
+        set -e
+        cd build
+        eval `opam config env`
+        make -j3
+        make -j3 examples
+        make -j3 test-z3
+        ./ml_example.byte
+        ./ml_example
+        cd ..
+    - script: eval `opam config env`; ocamlfind install z3-static build/api/ml/* build/libz3-static.a
+    - script: |
+        set -e
+        cd build
+        eval `opam config env`
+        make -j3
+        make -j3 _ex_ml_example_post_install
+        ./ml_example_static.byte
+        ./ml_example_static_custom.byte
+        ./ml_example_static
+      cd ..
+    - template: scripts/test-z3.yml
+    - template: scripts/test-regressions.yml
+    - template: scripts/generate-doc.yml
+
 - job: "LinuxMSan"
   displayName: "Ubuntu build - cmake"
   condition: eq(0,1) 
@@ -252,3 +298,37 @@ jobs:
 #   - template: scripts/test-examples-cmake.yml
     - template: scripts/test-regressions.yml
 #   - template: scripts/test-java-cmake.yml
+
+
+- job: "MacOSOCaml"
+  displayName: "MacOS build with OCaml"
+  pool:
+    vmImage: "macOS-latest"
+  steps:
+    - script: brew install opam
+    - script: opam init -y
+    - script: eval `opam config env`; opam install zarith ocamlfind -y
+    - script: eval `opam config env`; python scripts/mk_make.py --ml
+    - script: |
+        set -e
+        cd build
+        make -j3
+        make -j3 examples
+        make -j3 test-z3
+        ./ml_example.byte
+        ./ml_example
+        cd ..
+    - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.*
+    - script: |
+        set -e
+        cd build
+        eval `opam config env`
+        make -j3
+        make -j3 _ex_ml_example_post_install
+        ./ml_example_shared.byte
+        ./ml_example_shared_custom.byte
+        ./ml_example_shared
+      cd ..
+# Skip as dead-slow in debug mode:
+#  - template: scripts/test-z3.yml
+    - template: scripts/test-regressions.yml
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
@@ -2013,9 +2013,12 @@ def mk_makefile(self, out):
                 LIBZ3 = z3linkdep
 
             LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))
+
+            stubs_install_path = '$$(%s printconf path)/stublibs' % OCAMLFIND
             if not STATIC_LIB:
-                dllpath = '-dllpath $$(%s printconf path)/stublibs' % OCAMLFIND
-                LIBZ3 = LIBZ3 + ' ' + dllpath
+                loadpath = '-ccopt -L' + stubs_install_path
+                dllpath = '-dllpath ' + stubs_install_path
+                LIBZ3 = LIBZ3 + ' ' + loadpath + ' ' + dllpath
 
             if DEBUG_MODE and not(is_cygwin()):
                 # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
@@ -2036,6 +2039,9 @@ def mk_makefile(self, out):
 
             out.write('\n')
             out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
+            if IS_OSX:
+                out.write('\tinstall_name_tool -id libz3.dylib %s/libz3.dylib libz3.dylib\n' % (stubs_install_path))
+                out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path))                
             out.write('\n')
 
             if IS_WINDOWS:
@@ -2294,6 +2300,41 @@ def mk_makefile(self, out):
             out.write('\n')
             out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
 
+        debug_opt = '-g ' if DEBUG_MODE else ''
+
+        if STATIC_LIB:
+            opam_z3_opts = '-thread -package z3-static -linkpkg'
+            ml_post_install_tests = [
+                (OCAMLC,              'ml_example_static.byte'),
+                (OCAMLC + ' -custom', 'ml_example_static_custom.byte'),
+                (OCAMLOPT,            'ml_example_static$(EXE_EXT)')
+            ]
+        else:
+            opam_z3_opts = '-thread -package z3 -linkpkg'
+            ml_post_install_tests = [
+                (OCAMLC,              'ml_example_shared.byte'),
+                (OCAMLC + ' -custom', 'ml_example_shared_custom.byte'),
+                (OCAMLOPT,            'ml_example_shared$(EXE_EXT)')
+            ]
+
+        for ocaml_compiler, testname in ml_post_install_tests:
+            out.write(testname + ':')
+            for mlfile in get_ml_files(self.ex_dir):
+                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
+            out.write('\n')
+            out.write('\tocamlfind %s -o %s %s %s ' % (ocaml_compiler, debug_opt, testname, opam_z3_opts))
+            for mlfile in get_ml_files(self.ex_dir):
+                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
+            out.write('\n')
+
+        if STATIC_LIB:
+            out.write('_ex_ml_example_post_install: ml_example_static.byte ml_example_static_custom.byte ml_example_static$(EXE_EXT)\n')
+        else:
+            out.write('_ex_ml_example_post_install: ml_example_shared.byte ml_example_shared_custom.byte ml_example_shared$(EXE_EXT)\n')
+
+        out.write('\n')
+
+
 class PythonExampleComponent(ExampleComponent):
     def __init__(self, name, path):
         ExampleComponent.__init__(self, name, path)