Does not compile with Z3 v4.4.2

[dgenin]

Which version of Z3 is SLAayer known to work with? I have been trying to compile against Z3 v4.4.2 but the OCaml interface appears to have changed substantially.

[jberdine]

Which version of Z3 is SLAayer known to work with? I have been trying to compile against Z3 v4.4.2 but the OCaml interface appears to have changed substantially.

Yes, SLAyer uses a significantly different OCaml interface to Z3. The version of Z3 that the submodule references, commit d4314d4e3c9722ca10b27250dd2dec822174e4d1 of https://git.codeplex.com/forks/jjb/z3 was tested quite thoroughly. I don't know if later versions of Z3 can be easily merged into that fork, in order to use the OCaml api. Also, in the past, significant changes to the version of Z3 have entailed some work in SLAyer, hence the submodule pointing at a specific commit. Cheers, Josh

[dgenin]

Are you certain the above commit number is correct? I just cloned the z3 git repo in your reply but "git checkout d4314d4e3c9722ca10b27250dd2dec822174e4d1" produced no results (fatal: reference is not a tree: d4314d4e3c9722ca10b27250dd2dec822174e4d1).

Thank you for your help,
Dan

[jberdine]

Hmm... I just tried cloning a fresh copy, and the referenced Z3 commit is found:

$ git clone git+ssh://git@github.com/Microsoft/SLAyer.git                  /tmp
Cloning into 'SLAyer'...
remote: Counting objects: 549, done.
remote: Total 549 (delta 0), reused 0 (delta 0), pack-reused 549
Receiving objects: 100% (549/549), 448.82 KiB | 681.00 KiB/s, done.
Resolving deltas: 100% (87/87), done.
Checking connectivity... done.
$ cd SLAyer                                                                /tmp
$ git submodule init                                         /tmp/SLAyer:master
Submodule 'tools/Z3' (https://git.codeplex.com/forks/jjb/z3) registered for path 'tools/Z3'
$ git submodule update                                       /tmp/SLAyer:master
Cloning into 'tools/Z3'...
remote: Counting objects: 15416, done.
remote: Compressing objects: 100% (3850/3850), done.
remote: Total 15416 (delta 11541), reused 15380 (delta 11505)
Receiving objects: 100% (15416/15416), 7.28 MiB | 3.33 MiB/s, done.
Resolving deltas: 100% (11541/11541), done.
Checking connectivity... done.
Submodule path 'tools/Z3': checked out 'd4314d4e3c9722ca10b27250dd2dec822174e4d1'

Do you get different results?

[dgenin]

My bad, I was cloning from the official Z3 repo. So Z3 appears to compile fine now but I still get
$ make
/Library/Developer/CommandLineTools/usr/bin/make -j 8 -C /Users/genindi1/tools/SLAyer/src/../tools/Z3/src/../build api_dll
make[1]: Nothing to be done for api_dll'. /Library/Developer/CommandLineTools/usr/bin/make DEPS='/Users/genindi1/tools/SLAyer/src/_build*/{Slayer,CounterExample,Pure}.cm{i,o,x}' ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS' -C /Users/genindi1/tools/SLAyer/src/../tools/Z3/src/../build/api/ml z3.cma z3.cmxa make[1]:z3.cma' is up to date.
make[1]: `z3.cmxa' is up to date.
fatal: No names found, cannot describe anything.
echo "let version = """ > Version.ml
======== building SLAyer debug (byte & native) code ========
ocamlbuild -j 8 -no-links -build-dir _build/Darwin/x86_64 -tag bin_annot -cflags "-short-paths -w +6+7+27+29+32..39+41+44+45" -cflags -I,/Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -lflags -I,/Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -cflags -I,/Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -lflags -I,/Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -cflags -annot -Is Library,contaminated,UnitTests,UnitTests/StandAlone -libs str,unix,z3 -tag debug
slayer.byte slayer.native

• /usr/local/bin/ocamlc.opt -c -short-paths -w +6+7+27+29+32..39+41+44+45 -I /Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -I /Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -annot -g -bin-annot -I UnitTests -I Library -I contaminated -o slayer.cmo slayer.ml
  File "slayer.ml", line 88, characters 30-44:
  Error: Unbound value Z3.get_version
  Command exited with code 2.
  Compilation unsuccessful after building 108 targets (107 cached) in 00:00:00.
  make: *** [dbg] Error 10

[jberdine]

On Fri, Apr 22 2016, dgenin wrote:

My bad, I was cloning from the official Z3 repo. So Z3 appears to compile fine now but I still get
$ make
/Library/Developer/CommandLineTools/usr/bin/make -j 8 -C
/Users/genindi1/tools/SLAyer/src/../tools/Z3/src/../build api_dll
make[1]: Nothing to be done for api_dll'.
/Library/Developer/CommandLineTools/usr/bin/make DEPS='/Users/genindi1/tools/SLAyer/src/_build*/
{Slayer,CounterExample,Pure}.cm{i,o,x}' ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS' -C
/Users/genindi1/tools/SLAyer/src/../tools/Z3/src/../build/api/ml z3.cma z3.cmxa
make[1]:z3.cma' is up to date.
make[1]: `z3.cmxa' is up to date.
fatal: No names found, cannot describe anything.
echo "let version = """ > Version.ml
======== building SLAyer debug (byte & native) code ========
ocamlbuild -j 8 -no-links -build-dir _build/Darwin/x86_64 -tag bin_annot -cflags "-short-paths -w
+6+7+27+29+32..39+41+44+45" -cflags -I,/Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -lflags
-I,/Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -cflags
-I,/Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -lflags
-I,/Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -cflags -annot -Is
Library,contaminated,UnitTests,UnitTests/StandAlone -libs str,unix,z3 -tag debug
slayer.byte slayer.native

• /usr/local/bin/ocamlc.opt -c -short-paths -w +6+7+27+29+32..39+41+44+45 -I
  /Users/genindi1/tools/SLAyer/src/../tools/esp/ocaml -I
  /Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml -annot -g -bin-annot -I UnitTests -I Library -I
  contaminated -o slayer.cmo slayer.ml File "slayer.ml", line 88, characters 30-44: Error: Unbound value
  Z3.get_version Command exited with code 2. Compilation unsuccessful after building 108 targets (107
  cached) in 00:00:00. make: *** [dbg] Error 10

This is indicating that the OCaml bindings for Z3 have not been built successfully. Do you have z3.cmi and z3.cma in the /Users/genindi1/tools/SLAyer/src/../tools/Z3/build/api/ml directory? Perhaps things got into an inconsistent state due to the difficulty cloning Z3? Does make clean clean_mlz3 and retrying help?

[dgenin]

z3.cma and z3.cmi are both there

$ ls ../tools/Z3/build/api/ml/z3.cm*
../tools/Z3/build/api/ml/z3.cma ../tools/Z3/build/api/ml/z3.cmi ../tools/Z3/build/api/ml/z3.cmxa

Just tried starting over from scratch and ran into the same problem

~/Code/SLAyer/src $ make
make -j 8 -C /home/genin/Code/SLAyer/src/../tools/Z3/src/../build api_dll
make[1]: Entering directory /home/genin/Code/SLAyer/tools/Z3/build' make[1]: Nothing to be done forapi_dll'.
make[1]: Leaving directory /home/genin/Code/SLAyer/tools/Z3/build' make DEPS='/home/genin/Code/SLAyer/src/_build*/{Slayer,CounterExample,Pure}.cm{i,o,x}' ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS' -C /home/genin/Code/SLAyer/src/../tools/Z3/src/../build/api/ml z3.cma z3.cmxa make[1]: Entering directory/home/genin/Code/SLAyer/tools/Z3/build/api/ml'
make[1]: z3.cma' is up to date. make[1]:z3.cmxa' is up to date.
make[1]: Leaving directory `/home/genin/Code/SLAyer/tools/Z3/build/api/ml'
fatal: No names found, cannot describe anything.
echo "let version = """ > Version.ml
======== building SLAyer debug (byte & native) code ========
ocamlbuild -j 8 -no-links -build-dir _build/Linux/x86_64 -tag bin_annot -cflags "-short-paths -w +6+7+27+29+32..39+41+44+45" -cflags -I,/home/genin/Code/SLAyer/src/../tools/esp/ocaml -lflags -I,/home/genin/Code/SLAyer/src/../tools/esp/ocaml -cflags -I,/home/genin/Code/SLAyer/src/../tools/Z3/build/api/ml -lflags -I,/home/genin/Code/SLAyer/src/../tools/Z3/build/api/ml -cflags -annot -Is Library,contaminated,UnitTests,UnitTests/StandAlone -libs str,unix,z3 -tag debug
slayer.byte slayer.native

• /home/genin/.opam/4.02.1/bin/ocamlc.opt -c -short-paths -w +6+7+27+29+32..39+41+44+45 -I /home/genin/Code/SLAyer/src/../tools/esp/ocaml -I /home/genin/Code/SLAyer/src/../tools/Z3/build/api/ml -annot -g -bin-annot -I UnitTests -I Library -I contaminated -o slayer.cmo slayer.ml
  File "slayer.ml", line 88, characters 30-44:
  Error: Unbound value Z3.get_version
  Command exited with code 2.
  Compilation unsuccessful after building 108 targets (107 cached) in 00:00:00.
  make: *** [dbg] Error 10

[jberdine]

Ok, thanks. I think that to debug I will need the full transcript from building at least the z3 ocaml bindings and slayer. Could you add the transcript of running: `opam info camlidl`, `make clean clean_mlz3`, and `make`? At the moment I suspect something related to camlidl is not as expected on your system.

[dgenin]

OK, that helped! Turns out camlidl was not installed. Once I installed it, I was able to compile slayer. BTW, was this in the documentation somewhere? Might be a good idea to add a check for camlidl in config.sh.

Thank you for your help, Josh.

[jberdine]

Excellent, that's good to hear. You are right, there seems to be no mention of the camlidl dependency anywhere. Will fix, thanks.

[sishtiaq]

Hi DiG (@dgenin),
If you want to change the README, we'd be happy to take your change.

[dgenin]

I would love to help but sadly my employer's IP rules are so expansive that I can't contribute even if I do it in my own free time:( This probably means I had no right to pull your code either, right?

[sishtiaq]

DiG (@dgenin): I understand! (At MSFT, we can contribute as many bug-fixes and sample code as we like. Much better than nothing.)

[dgenin]

For sure. I am actually quite impressed with Microsoft's recent open sourcing of a number of projects like Z3 and SLayer. Hopefully, my employer too will decide to join the 21st century in the not too distant future.