1############################################
2# Copyright (c) 2012 Microsoft Corporation
3#
4# Auxiliary scripts for generating Makefiles
5# and Visual Studio project files.
6#
7# Author: Leonardo de Moura (leonardo)
8############################################
9import io
10import sys
11import os
12import re
13import getopt
14import shutil
15from mk_exception import *
16import mk_genfile_common
17from fnmatch import fnmatch
18import distutils.sysconfig
19import compileall
20import subprocess
21
22def getenv(name, default):
23    try:
24        return os.environ[name].strip(' "\'')
25    except:
26        return default
27
28CXX=getenv("CXX", None)
29CC=getenv("CC", None)
30CPPFLAGS=getenv("CPPFLAGS", "")
31CXXFLAGS=getenv("CXXFLAGS", "")
32AR=getenv("AR", "ar")
33EXAMP_DEBUG_FLAG=''
34LDFLAGS=getenv("LDFLAGS", "")
35JNI_HOME=getenv("JNI_HOME", None)
36OCAMLC=getenv("OCAMLC", "ocamlc")
37OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
38OCAML_LIB=getenv("OCAML_LIB", None)
39OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
40DOTNET="dotnet"
41# Standard install directories relative to PREFIX
42INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
43INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
44INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
45INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig'))
46
47CXX_COMPILERS=['g++', 'clang++']
48C_COMPILERS=['gcc', 'clang']
49JAVAC=None
50JAR=None
51PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
52BUILD_DIR='build'
53REV_BUILD_DIR='..'
54SRC_DIR='src'
55EXAMPLE_DIR='examples'
56# Required Components
57Z3_DLL_COMPONENT='api_dll'
58PATTERN_COMPONENT='pattern'
59UTIL_COMPONENT='util'
60API_COMPONENT='api'
61DOTNET_COMPONENT='dotnet'
62DOTNET_CORE_COMPONENT='dotnet'
63JAVA_COMPONENT='java'
64ML_COMPONENT='ml'
65CPP_COMPONENT='cpp'
66PYTHON_COMPONENT='python'
67#####################
68IS_WINDOWS=False
69IS_LINUX=False
70IS_HURD=False
71IS_OSX=False
72IS_FREEBSD=False
73IS_NETBSD=False
74IS_OPENBSD=False
75IS_SUNOS=False
76IS_CYGWIN=False
77IS_CYGWIN_MINGW=False
78IS_MSYS2=False
79VERBOSE=True
80DEBUG_MODE=False
81SHOW_CPPS = True
82VS_X64 = False
83VS_ARM = False
84LINUX_X64 = True
85ONLY_MAKEFILES = False
86Z3PY_SRC_DIR=None
87Z3JS_SRC_DIR=None
88VS_PROJ = False
89TRACE = False
90PYTHON_ENABLED=False
91DOTNET_CORE_ENABLED=False
92DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
93JAVA_ENABLED=False
94ML_ENABLED=False
95JS_ENABLED=False
96PYTHON_INSTALL_ENABLED=False
97STATIC_LIB=False
98STATIC_BIN=False
99VER_MAJOR=None
100VER_MINOR=None
101VER_BUILD=None
102VER_TWEAK=None
103PREFIX=sys.prefix
104GMP=False
105VS_PAR=False
106VS_PAR_NUM=8
107GPROF=False
108GIT_HASH=False
109GIT_DESCRIBE=False
110SLOW_OPTIMIZE=False
111LOG_SYNC=False
112SINGLE_THREADED=False
113GUARD_CF=False
114ALWAYS_DYNAMIC_BASE=False
115
116FPMATH="Default"
117FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
118
119
120def check_output(cmd):
121    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
122    if out != None:
123        enc = sys.stdout.encoding
124        if enc != None: return out.decode(enc).rstrip('\r\n')
125        else: return out.rstrip('\r\n')
126    else:
127        return ""
128
129def git_hash():
130    try:
131        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
132        r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
133    except:
134        raise MKException("Failed to retrieve git hash")
135    ls = r.split(' ')
136    if len(ls) != 2:
137        raise MKException("Unexpected git output " + r)
138    return ls[0]
139
140def is_windows():
141    return IS_WINDOWS
142
143def is_linux():
144    return IS_LINUX
145
146def is_hurd():
147    return IS_HURD
148
149def is_freebsd():
150    return IS_FREEBSD
151
152def is_netbsd():
153    return IS_NETBSD
154
155def is_openbsd():
156    return IS_OPENBSD
157
158def is_sunos():
159    return IS_SUNOS
160
161def is_osx():
162    return IS_OSX
163
164def is_cygwin():
165    return IS_CYGWIN
166
167def is_cygwin_mingw():
168    return IS_CYGWIN_MINGW
169
170def is_msys2():
171    return IS_MSYS2
172
173def norm_path(p):
174    return os.path.expanduser(os.path.normpath(p))
175
176def which(program):
177    import os
178    def is_exe(fpath):
179        return os.path.isfile(fpath) and os.access(fpath, os.X_OK)
180
181    fpath, fname = os.path.split(program)
182    if fpath:
183        if is_exe(program):
184            return program
185    else:
186        for path in getenv("PATH", "").split(os.pathsep):
187            exe_file = os.path.join(path, program)
188            if is_exe(exe_file):
189                return exe_file
190    return None
191
192class TempFile:
193    def __init__(self, name):
194        try:
195            self.name  = name
196            self.fname = open(name, 'w')
197        except:
198            raise MKException("Failed to create temporary file '%s'" % self.name)
199
200    def add(self, s):
201        self.fname.write(s)
202
203    def commit(self):
204        self.fname.close()
205
206    def __del__(self):
207        self.fname.close()
208        try:
209            os.remove(self.name)
210        except:
211            pass
212
213def exec_cmd(cmd):
214    if isinstance(cmd, str):
215        cmd = cmd.split(' ')
216    new_cmd = []
217    first = True
218    for e in cmd:
219        if first:
220            first = False
221            new_cmd.append(e)
222        else:
223            if e != "":
224                se = e.split(' ')
225                if len(se) > 1:
226                    for e2 in se:
227                        if e2 != "":
228                            new_cmd.append(e2)
229                else:
230                    new_cmd.append(e)
231    cmd = new_cmd
232    null = open(os.devnull, 'wb')
233    try:
234        return subprocess.call(cmd, stdout=null, stderr=null)
235    except:
236        # Failed to create process
237        return 1
238    finally:
239        null.close()
240
241# rm -f fname
242def rmf(fname):
243    if os.path.exists(fname):
244        os.remove(fname)
245
246def exec_compiler_cmd(cmd):
247    r = exec_cmd(cmd)
248    if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
249        rmf('a.exe')
250    else:
251        rmf('a.out')
252    return r
253
254def test_cxx_compiler(cc):
255    if is_verbose():
256        print("Testing %s..." % cc)
257    t = TempFile('tst.cpp')
258    t.add('#include<iostream>\nint main() { return 0; }\n')
259    t.commit()
260    return exec_compiler_cmd([cc, CPPFLAGS, CXXFLAGS, 'tst.cpp', LDFLAGS]) == 0
261
262def test_c_compiler(cc):
263    if is_verbose():
264        print("Testing %s..." % cc)
265    t = TempFile('tst.c')
266    t.add('#include<stdio.h>\nint main() { return 0; }\n')
267    t.commit()
268    return exec_compiler_cmd([cc, CPPFLAGS, 'tst.c', LDFLAGS]) == 0
269
270def test_gmp(cc):
271    if is_verbose():
272        print("Testing GMP...")
273    t = TempFile('tstgmp.cpp')
274    t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
275    t.commit()
276    return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
277
278
279
280def test_fpmath(cc):
281    global FPMATH_FLAGS
282    if is_verbose():
283        print("Testing floating point support...")
284    t = TempFile('tstsse.cpp')
285    t.add('int main() { return 42; }\n')
286    t.commit()
287    # -Werror is needed because some versions of clang warn about unrecognized
288    # -m flags.
289    if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
290        FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
291        return "SSE2-GCC"
292    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
293        FPMATH_FLAGS="-msse -msse2"
294        return "SSE2-CLANG"
295    elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
296        FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
297        return "ARM-VFP"
298    else:
299        FPMATH_FLAGS=""
300        return "UNKNOWN"
301
302
303def find_jni_h(path):
304    for root, dirs, files in os.walk(path):
305        for f in files:
306            if f == 'jni.h':
307                return root
308    return False
309
310def check_java():
311    global JNI_HOME
312    global JAVAC
313    global JAR
314
315    JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.
316
317    if is_verbose():
318        print("Finding javac ...")
319
320    if JDK_HOME is not None:
321        if IS_WINDOWS:
322            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe')
323        else:
324            JAVAC = os.path.join(JDK_HOME, 'bin', 'javac')
325
326        if not os.path.exists(JAVAC):
327            raise MKException("Failed to detect javac at '%s/bin'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME))
328    else:
329        # Search for javac in the path.
330        ind = 'javac'
331        if IS_WINDOWS:
332            ind = ind + '.exe'
333        paths = os.getenv('PATH', None)
334        if paths:
335            spaths = paths.split(os.pathsep)
336            for i in range(0, len(spaths)):
337                cmb = os.path.join(spaths[i], ind)
338                if os.path.exists(cmb):
339                    JAVAC = cmb
340                    break
341
342    if JAVAC is None:
343        raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.')
344
345    if is_verbose():
346        print("Finding jar ...")
347
348    if IS_WINDOWS:
349        JAR = os.path.join(os.path.dirname(JAVAC), 'jar.exe')
350    else:
351        JAR = os.path.join(os.path.dirname(JAVAC), 'jar')
352
353    if not os.path.exists(JAR):
354        raise MKException("Failed to detect jar at '%s'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME))
355
356    if is_verbose():
357        print("Testing %s..." % JAVAC)
358
359    t = TempFile('Hello.java')
360    t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
361    t.commit()
362
363    oo = TempFile('output')
364    eo = TempFile('errout')
365    try:
366        subprocess.call([JAVAC, 'Hello.java', '-verbose', '-source', '1.8', '-target', '1.8' ], stdout=oo.fname, stderr=eo.fname)
367        oo.commit()
368        eo.commit()
369    except:
370        raise MKException('Found, but failed to run Java compiler at %s' % (JAVAC))
371
372    os.remove('Hello.class')
373
374    if is_verbose():
375        print("Finding jni.h...")
376
377    if JNI_HOME is not None:
378        if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
379            raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME))
380    else:
381        # Search for jni.h in the library directories...
382        t = open('errout', 'r')
383        open_pat = re.compile("\[search path for class files: (.*)\]")
384        cdirs = []
385        for line in t:
386            m = open_pat.match(line)
387            if m:
388                libdirs = m.group(1).split(',')
389                for libdir in libdirs:
390                    q = os.path.dirname(libdir)
391                    if cdirs.count(q) == 0 and len(q) > 0:
392                        cdirs.append(q)
393        t.close()
394
395        # ... plus some heuristic ones.
396        extra_dirs = []
397
398        # For the libraries, even the JDK usually uses a JRE that comes with it. To find the
399        # headers we have to go a little bit higher up.
400        for dir in cdirs:
401            extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))
402
403        if IS_OSX: # Apparently Apple knows best where to put stuff...
404            extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')
405
406        cdirs[len(cdirs):] = extra_dirs
407
408        for dir in cdirs:
409            q = find_jni_h(dir)
410            if q is not False:
411                JNI_HOME = q
412
413        if JNI_HOME is None:
414            raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
415
416def test_csc_compiler(c):
417    t = TempFile('hello.cs')
418    t.add('public class hello { public static void Main() {} }')
419    t.commit()
420    if is_verbose():
421        print ('Testing %s...' % c)
422    r = exec_cmd([c, 'hello.cs'])
423    try:
424        rmf('hello.cs')
425        rmf('hello.exe')
426    except:
427        pass
428    return r == 0
429
430def check_dotnet_core():
431    if not IS_WINDOWS:
432        return
433    r = exec_cmd([DOTNET, '--help'])
434    if r != 0:
435        raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities')
436
437def check_ml():
438    t = TempFile('hello.ml')
439    t.add('print_string "Hello world!\n";;')
440    t.commit()
441    if is_verbose():
442        print ('Testing %s...' % OCAMLC)
443    r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
444    if r != 0:
445        raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
446    if is_verbose():
447        print ('Testing %s...' % OCAMLOPT)
448    r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
449    if r != 0:
450        raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
451    try:
452        rmf('hello.cmi')
453        rmf('hello.cmo')
454        rmf('hello.cmx')
455        rmf('a.out')
456        rmf('hello.o')
457    except:
458        pass
459    find_ml_lib()
460    find_ocaml_find()
461
462def find_ocaml_find():
463    global OCAMLFIND
464    if is_verbose():
465        print ("Testing %s..." % OCAMLFIND)
466    r = exec_cmd([OCAMLFIND, 'printconf'])
467    if r != 0:
468        OCAMLFIND = ''
469
470def find_ml_lib():
471    global OCAML_LIB
472    if is_verbose():
473        print ('Finding OCAML_LIB...')
474    t = TempFile('output')
475    null = open(os.devnull, 'wb')
476    try:
477        subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
478        t.commit()
479    except:
480        raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
481    finally:
482        null.close()
483
484    t = open('output', 'r')
485    for line in t:
486        OCAML_LIB = line[:-1]
487    if is_verbose():
488        print ('OCAML_LIB=%s' % OCAML_LIB)
489    t.close()
490    rmf('output')
491    return
492
493def is64():
494    global LINUX_X64
495    if is_sunos() and sys.version_info.major < 3:
496        return LINUX_X64
497    else:
498        return LINUX_X64 and sys.maxsize >= 2**32
499
500def check_ar():
501    if is_verbose():
502        print("Testing ar...")
503    if which(AR) is None:
504        raise MKException('%s (archive tool) was not found' % AR)
505
506def find_cxx_compiler():
507    global CXX, CXX_COMPILERS
508    if CXX is not None:
509        if test_cxx_compiler(CXX):
510            return CXX
511    for cxx in CXX_COMPILERS:
512        if test_cxx_compiler(cxx):
513            CXX = cxx
514            return CXX
515    raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
516
517def find_c_compiler():
518    global CC, C_COMPILERS
519    if CC is not None:
520        if test_c_compiler(CC):
521            return CC
522    for c in C_COMPILERS:
523        if test_c_compiler(c):
524            CC = c
525            return CC
526    raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
527
528def set_version(major, minor, build, revision):
529    global VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK, GIT_DESCRIBE
530    VER_MAJOR = major
531    VER_MINOR = minor
532    VER_BUILD = build
533    VER_TWEAK = revision
534    if GIT_DESCRIBE:
535        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
536        VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
537
538def get_version():
539    return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
540
541def get_version_string(n):
542    if n == 3:
543        return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD)
544    return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_TWEAK)
545
546def build_static_lib():
547    return STATIC_LIB
548
549def build_static_bin():
550    return STATIC_BIN
551
552def is_cr_lf(fname):
553    # Check whether text files use cr/lf
554    f = open(fname, 'r')
555    line = f.readline()
556    f.close()
557    sz = len(line)
558    return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n'
559
560# dos2unix in python
561#    cr/lf --> lf
562def dos2unix(fname):
563    if is_cr_lf(fname):
564        fin  = open(fname, 'r')
565        fname_new = '%s.new' % fname
566        fout = open(fname_new, 'w')
567        for line in fin:
568            line = line.rstrip('\r\n')
569            fout.write(line)
570            fout.write('\n')
571        fin.close()
572        fout.close()
573        shutil.move(fname_new, fname)
574        if is_verbose():
575            print("dos2unix '%s'" % fname)
576
577def dos2unix_tree():
578    for root, dirs, files in os.walk('src'):
579        for f in files:
580            dos2unix(os.path.join(root, f))
581
582
583def check_eol():
584    if not IS_WINDOWS:
585        # Linux/OSX/BSD check if the end-of-line is cr/lf
586        if is_cr_lf('LICENSE.txt'):
587            if is_verbose():
588                print("Fixing end of line...")
589            dos2unix_tree()
590
591if os.name == 'nt':
592    IS_WINDOWS=True
593    # Visual Studio already displays the files being compiled
594    SHOW_CPPS=False
595elif os.name == 'posix':
596    if os.uname()[0] == 'Darwin':
597        IS_OSX=True
598    elif os.uname()[0] == 'Linux':
599        IS_LINUX=True
600    elif os.uname()[0] == 'GNU':
601        IS_HURD=True
602    elif os.uname()[0] == 'FreeBSD' or os.uname()[0] == 'DragonFly':
603        IS_FREEBSD=True
604    elif os.uname()[0] == 'NetBSD':
605        IS_NETBSD=True
606    elif os.uname()[0] == 'OpenBSD':
607        IS_OPENBSD=True
608    elif os.uname()[0] == 'SunOS':
609        IS_SUNOS=True
610    elif os.uname()[0][:6] == 'CYGWIN':
611        IS_CYGWIN=True
612        if (CC != None and "mingw" in CC):
613            IS_CYGWIN_MINGW=True
614    elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
615        IS_MSYS2=True
616        if os.uname()[4] == 'x86_64':
617            LINUX_X64=True
618        else:
619            LINUX_X64=False
620
621
622def display_help(exit_code):
623    print("mk_make.py: Z3 Makefile generator\n")
624    print("This script generates the Makefile for the Z3 theorem prover.")
625    print("It must be executed from the Z3 root directory.")
626    print("\nOptions:")
627    print("  -h, --help                    display this message.")
628    print("  -s, --silent                  do not print verbose messages.")
629    if not IS_WINDOWS:
630        print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
631    else:
632        print("  --parallel=num                use cl option /MP with 'num' parallel processes")
633    print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
634    print("  -b <subdir>, --build=<subdir>  subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
635    print("  --githash=hash                include the given hash in the binaries.")
636    print("  --git-describe                include the output of 'git describe' in the version information.")
637    print("  -d, --debug                   compile Z3 in debug mode.")
638    print("  -t, --trace                   enable tracing in release mode.")
639    if IS_WINDOWS:
640        print("  --guardcf                     enable Control Flow Guard runtime checks.")
641        print("  -x, --x64                     create 64 binary when using Visual Studio.")
642    else:
643        print("  --x86                         force 32-bit x86 build on x64 systems.")
644    print("  -m, --makefiles               generate only makefiles.")
645    if IS_WINDOWS:
646        print("  -v, --vsproj                  generate Visual Studio Project Files.")
647        print("  --optimize                    generate optimized code during linking.")
648    print("  --dotnet                      generate .NET platform bindings.")
649    print("  --dotnet-key=<file>           sign the .NET assembly using the private key in <file>.")
650    print("  --java                        generate Java bindings.")
651    print("  --ml                          generate OCaml bindings.")
652    print("  --js                          generate JScript bindings.")
653    print("  --python                      generate Python bindings.")
654    print("  --staticlib                   build Z3 static library.")
655    print("  --staticbin                   build a statically linked Z3 binary.")
656    if not IS_WINDOWS:
657        print("  -g, --gmp                     use GMP.")
658        print("  --gprof                       enable gprof")
659    print("  --log-sync                    synchronize access to API log files to enable multi-thread API logging.")
660    print("  --single-threaded             non-thread-safe build")
661    print("")
662    print("Some influential environment variables:")
663    if not IS_WINDOWS:
664        print("  CXX        C++ compiler")
665        print("  CC         C compiler")
666        print("  LDFLAGS    Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
667        print("  CPPFLAGS   Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
668        print("  CXXFLAGS   C++ compiler flags")
669    print("  JDK_HOME   JDK installation directory (only relevant if -j or --java option is provided)")
670    print("  JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)")
671    print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
672    print("  OCAMLFIND  Ocaml find tool (only relevant with --ml)")
673    print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
674    print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
675    print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
676    print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
677    print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
678    print("  Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
679    exit(exit_code)
680
681# Parse configuration option for mk_make script
682def parse_options():
683    global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
684    global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
685    global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
686    global GUARD_CF, ALWAYS_DYNAMIC_BASE
687    try:
688        options, remainder = getopt.gnu_getopt(sys.argv[1:],
689                                               'b:df:sxhmcvtnp:gj',
690                                               ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
691                                                'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
692                                                'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
693    except:
694        print("ERROR: Invalid command line option")
695        display_help(1)
696
697    for opt, arg in options:
698        print('opt = %s, arg = %s' % (opt, arg))
699        if opt in ('-b', '--build'):
700            if arg == 'src':
701                raise MKException('The src directory should not be used to host the Makefile')
702            set_build_dir(arg)
703        elif opt in ('-s', '--silent'):
704            VERBOSE = False
705        elif opt in ('-d', '--debug'):
706            DEBUG_MODE = True
707        elif opt in ('-x', '--x64'):
708            if not IS_WINDOWS:
709                raise MKException('x64 compilation mode can only be specified when using Visual Studio')
710            VS_X64 = True
711        elif opt in ('--x86'):
712            LINUX_X64=False
713        elif opt in ('-h', '--help'):
714            display_help(0)
715        elif opt in ('-m', '--makefiles'):
716            ONLY_MAKEFILES = True
717        elif opt in ('-c', '--showcpp'):
718            SHOW_CPPS = True
719        elif opt in ('-v', '--vsproj'):
720            VS_PROJ = True
721        elif opt in ('-t', '--trace'):
722            TRACE = True
723        elif opt in ('--dotnet',):
724            DOTNET_CORE_ENABLED = True
725        elif opt in ('--dotnet-key'):
726            DOTNET_KEY_FILE = arg
727        elif opt in ('--staticlib'):
728            STATIC_LIB = True
729        elif opt in ('--staticbin'):
730            STATIC_BIN = True
731        elif opt in ('--optimize'):
732            SLOW_OPTIMIZE = True
733        elif not IS_WINDOWS and opt in ('-p', '--prefix'):
734            PREFIX = arg
735        elif opt in ('--pypkgdir'):
736            PYTHON_PACKAGE_DIR = arg
737        elif IS_WINDOWS and opt == '--parallel':
738            VS_PAR = True
739            VS_PAR_NUM = int(arg)
740        elif opt in ('-g', '--gmp'):
741            GMP = True
742        elif opt in ('-j', '--java'):
743            JAVA_ENABLED = True
744        elif opt == '--gprof':
745            GPROF = True
746        elif opt == '--githash':
747            GIT_HASH=arg
748        elif opt == '--git-describe':
749            GIT_DESCRIBE = True
750        elif opt in ('', '--ml'):
751            ML_ENABLED = True
752        elif opt == "--js":
753            JS_ENABLED = True
754        elif opt in ('', '--log-sync'):
755            LOG_SYNC = True
756        elif opt == '--single-threaded':
757            SINGLE_THREADED = True
758        elif opt in ('--python'):
759            PYTHON_ENABLED = True
760            PYTHON_INSTALL_ENABLED = True
761        elif opt == '--guardcf':
762            GUARD_CF = True
763            ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE
764        else:
765            print("ERROR: Invalid command line option '%s'" % opt)
766            display_help(1)
767
768
769# Return a list containing a file names included using '#include' in
770# the given C/C++ file named fname.
771def extract_c_includes(fname):
772    result = {}
773    # We look for well behaved #include directives
774    std_inc_pat     = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
775    system_inc_pat  = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
776    # We should generate and error for any occurrence of #include that does not match the previous pattern.
777    non_std_inc_pat = re.compile(".*#include.*")
778
779    f = io.open(fname, encoding='utf-8', mode='r')
780    linenum = 1
781    for line in f:
782        m1 = std_inc_pat.match(line)
783        if m1:
784            root_file_name = m1.group(1)
785            slash_pos =  root_file_name.rfind('/')
786            if slash_pos >= 0  and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src"
787                # print(root_file_name)
788                root_file_name = root_file_name[slash_pos+1:]
789            result[root_file_name] = m1.group(1)
790        elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
791            raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
792        linenum = linenum + 1
793    f.close()
794    return result
795
796
797# Given a path dir1/subdir2/subdir3 returns ../../..
798def reverse_path(p):
799    # Filter out empty components (e.g. will have one if path ends in a slash)
800    l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
801    n = len(l)
802    r = '..'
803    for i in range(1, n):
804        r = os.path.join(r, '..')
805    return r
806
807def mk_dir(d):
808    if not os.path.exists(d):
809        os.makedirs(d)
810
811def set_build_dir(d):
812    global BUILD_DIR, REV_BUILD_DIR
813    BUILD_DIR = norm_path(d)
814    REV_BUILD_DIR = reverse_path(d)
815
816def set_z3js_dir(p):
817    global SRC_DIR, Z3JS_SRC_DIR
818    p = norm_path(p)
819    full = os.path.join(SRC_DIR, p)
820    if not os.path.exists(full):
821        raise MKException("Python bindings directory '%s' does not exist" % full)
822    Z3JS_SRC_DIR = full
823    if VERBOSE:
824        print("Js bindings directory was detected.")
825
826def set_z3py_dir(p):
827    global SRC_DIR, Z3PY_SRC_DIR
828    p = norm_path(p)
829    full = os.path.join(SRC_DIR, p)
830    if not os.path.exists(full):
831        raise MKException("Python bindings directory '%s' does not exist" % full)
832    Z3PY_SRC_DIR = full
833    if VERBOSE:
834        print("Python bindings directory was detected.")
835
836_UNIQ_ID = 0
837
838def mk_fresh_name(prefix):
839    global _UNIQ_ID
840    r = '%s_%s' % (prefix, _UNIQ_ID)
841    _UNIQ_ID = _UNIQ_ID + 1
842    return r
843
844_Id = 0
845_Components = []
846_ComponentNames = set()
847_Name2Component = {}
848_Processed_Headers = set()
849
850# Return the Component object named name
851def get_component(name):
852    return _Name2Component[name]
853
854def get_components():
855    return _Components
856
857# Return the directory where the python bindings are located.
858def get_z3py_dir():
859    return Z3PY_SRC_DIR
860
861# Return directory where the js bindings are located
862def get_z3js_dir():
863    return Z3JS_SRC_DIR
864
865# Return true if in verbose mode
866def is_verbose():
867    return VERBOSE
868
869def is_java_enabled():
870    return JAVA_ENABLED
871
872def is_ml_enabled():
873    return ML_ENABLED
874
875def is_js_enabled():
876    return JS_ENABLED
877
878def is_dotnet_core_enabled():
879    return DOTNET_CORE_ENABLED
880
881def is_python_enabled():
882    return PYTHON_ENABLED
883
884def is_python_install_enabled():
885    return PYTHON_INSTALL_ENABLED
886
887def is_compiler(given, expected):
888    """
889    Return True if the 'given' compiler is the expected one.
890    >>> is_compiler('g++', 'g++')
891    True
892    >>> is_compiler('/home/g++', 'g++')
893    True
894    >>> is_compiler(os.path.join('home', 'g++'), 'g++')
895    True
896    >>> is_compiler('clang++', 'g++')
897    False
898    >>> is_compiler(os.path.join('home', 'clang++'), 'clang++')
899    True
900    """
901    if given == expected:
902        return True
903    if len(expected) < len(given):
904        return given[len(given) - len(expected) - 1] == os.sep and given[len(given) - len(expected):] == expected
905    return False
906
907def is_CXX_gpp():
908    return is_compiler(CXX, 'g++')
909
910def is_clang_in_gpp_form(cc):
911    str = check_output([cc, '--version'])
912    try:
913       version_string = str.encode('utf-8')
914    except:
915       version_string = str
916    clang = 'clang'.encode('utf-8')
917    return version_string.find(clang) != -1
918
919def is_CXX_clangpp():
920    if is_compiler(CXX, 'g++'):
921        return is_clang_in_gpp_form(CXX)
922    return is_compiler(CXX, 'clang++')
923
924def get_files_with_ext(path, ext):
925    return filter(lambda f: f.endswith(ext), os.listdir(path))
926
927def get_cpp_files(path):
928    return get_files_with_ext(path,'.cpp')
929
930def get_c_files(path):
931    return get_files_with_ext(path,'.c')
932
933def get_cs_files(path):
934    return get_files_with_ext(path,'.cs')
935
936def get_java_files(path):
937    return get_files_with_ext(path,'.java')
938
939def get_ml_files(path):
940    return get_files_with_ext(path,'.ml')
941
942def find_all_deps(name, deps):
943    new_deps = []
944    for dep in deps:
945        if dep in _ComponentNames:
946            if not (dep in new_deps):
947                new_deps.append(dep)
948            for dep_dep in get_component(dep).deps:
949                if not (dep_dep in new_deps):
950                    new_deps.append(dep_dep)
951        else:
952            raise MKException("Unknown component '%s' at '%s'." % (dep, name))
953    return new_deps
954
955class Component:
956    def __init__(self, name, path, deps):
957        global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
958        if name in _ComponentNames:
959            raise MKException("Component '%s' was already defined." % name)
960        if path is None:
961            path = name
962        self.name = name
963        path = norm_path(path)
964        self.path = path
965        self.deps = find_all_deps(name, deps)
966        self.build_dir = path
967        self.src_dir   = os.path.join(SRC_DIR, path)
968        self.to_src_dir = os.path.join(REV_BUILD_DIR, self.src_dir)
969
970    def get_link_name(self):
971        return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
972
973
974    # Find fname in the include paths for the given component.
975    # ownerfile is only used for creating error messages.
976    # That is, we were looking for fname when processing ownerfile
977    def find_file(self, fname, ownerfile, orig_include=None):
978        full_fname = os.path.join(self.src_dir, fname)
979
980        # Store all our possible locations
981        possibilities = set()
982
983        # If the our file exists in the current directory, then we store it
984        if os.path.exists(full_fname):
985
986            # We cannot return here, as we might have files with the same
987            # basename, but different include paths
988            possibilities.add(self)
989
990        for dep in self.deps:
991            c_dep = get_component(dep)
992            full_fname = os.path.join(c_dep.src_dir, fname)
993            if os.path.exists(full_fname):
994                possibilities.add(c_dep)
995
996        if possibilities:
997
998            # We have ambiguity
999            if len(possibilities) > 1:
1000
1001                # We expect orig_path to be non-None here, so we can disambiguate
1002                assert orig_include is not None
1003
1004                # Get the original directory name
1005                orig_dir = os.path.dirname(orig_include)
1006
1007                # Iterate through all of the possibilities
1008                for possibility in possibilities:
1009
1010                    path = possibility.path.replace("\\","/")
1011                    # If we match the suffix of the path ...
1012                    if path.endswith(orig_dir):
1013
1014                        # ... use our new match
1015                        return possibility
1016
1017            # This means we didn't make an exact match ...
1018            #
1019            # We return any one possibility, just to ensure we don't break Z3's
1020            # builds
1021            return possibilities.pop()
1022
1023        raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name))
1024
1025    # Display all dependencies of file basename located in the given component directory.
1026    # The result is displayed at out
1027    def add_cpp_h_deps(self, out, basename):
1028        includes = extract_c_includes(os.path.join(self.src_dir, basename))
1029        out.write(os.path.join(self.to_src_dir, basename))
1030        for include, orig_include in includes.items():
1031            owner = self.find_file(include, basename, orig_include)
1032            out.write(' %s.node' % os.path.join(owner.build_dir, include))
1033
1034    # Add a rule for each #include directive in the file basename located at the current component.
1035    def add_rule_for_each_include(self, out, basename):
1036        fullname = os.path.join(self.src_dir, basename)
1037        includes = extract_c_includes(fullname)
1038        for include, orig_include in includes.items():
1039            owner = self.find_file(include, fullname, orig_include)
1040            owner.add_h_rule(out, include)
1041
1042    # Display a Makefile rule for an include file located in the given component directory.
1043    # 'include' is something of the form: ast.h, polynomial.h
1044    # The rule displayed at out is of the form
1045    #     ast/ast_pp.h.node : ../src/util/ast_pp.h util/util.h.node ast/ast.h.node
1046    #       @echo "done" > ast/ast_pp.h.node
1047    def add_h_rule(self, out, include):
1048        include_src_path   = os.path.join(self.to_src_dir, include)
1049        if include_src_path in _Processed_Headers:
1050            return
1051        _Processed_Headers.add(include_src_path)
1052        self.add_rule_for_each_include(out, include)
1053        include_node = '%s.node' % os.path.join(self.build_dir, include)
1054        out.write('%s: ' % include_node)
1055        self.add_cpp_h_deps(out, include)
1056        out.write('\n')
1057        out.write('\t@echo done > %s\n' % include_node)
1058
1059    def add_cpp_rules(self, out, include_defs, cppfile):
1060        self.add_rule_for_each_include(out, cppfile)
1061        objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1062        srcfile = os.path.join(self.to_src_dir, cppfile)
1063        out.write('%s: ' % objfile)
1064        self.add_cpp_h_deps(out, cppfile)
1065        out.write('\n')
1066        if SHOW_CPPS:
1067            out.write('\t@echo %s\n' % os.path.join(self.src_dir, cppfile))
1068        out.write('\t@$(CXX) $(CXXFLAGS) $(%s) $(CXX_OUT_FLAG)%s %s\n' % (include_defs, objfile, srcfile))
1069
1070    def mk_makefile(self, out):
1071        include_defs = mk_fresh_name('includes')
1072        out.write('%s =' % include_defs)
1073        for dep in self.deps:
1074            out.write(' -I%s' % get_component(dep).to_src_dir)
1075        out.write(' -I%s' % os.path.join(REV_BUILD_DIR,"src"))
1076        out.write('\n')
1077        mk_dir(os.path.join(BUILD_DIR, self.build_dir))
1078        if VS_PAR and IS_WINDOWS:
1079            cppfiles = list(get_cpp_files(self.src_dir))
1080            dependencies = set()
1081            for cppfile in cppfiles:
1082                dependencies.add(os.path.join(self.to_src_dir, cppfile))
1083                self.add_rule_for_each_include(out, cppfile)
1084                includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
1085                for include, orig_include in includes.items():
1086                    owner = self.find_file(include, cppfile, orig_include)
1087                    dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
1088            for cppfile in cppfiles:
1089                out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
1090            out.write(': ')
1091            for dep in dependencies:
1092                out.write(dep)
1093                out.write(' ')
1094            out.write('\n')
1095            out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
1096            for cppfile in cppfiles:
1097                out.write(' ')
1098                out.write(os.path.join(self.to_src_dir, cppfile))
1099            out.write('\n')
1100            out.write('\tmove *.obj %s\n' % self.build_dir)
1101        else:
1102            for cppfile in get_cpp_files(self.src_dir):
1103                self.add_cpp_rules(out, include_defs, cppfile)
1104
1105    # Return true if the component should be included in the all: rule
1106    def main_component(self):
1107        return False
1108
1109    # Return true if the component contains an AssemblyInfo.cs file that needs to be updated.
1110    def has_assembly_info(self):
1111        return False
1112
1113    # Return true if the component needs builder to generate an install_tactics.cpp file
1114    def require_install_tactics(self):
1115        return False
1116
1117    # Return true if the component needs a def file
1118    def require_def_file(self):
1119        return False
1120
1121    # Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
1122    def require_mem_initializer(self):
1123        return False
1124
1125    def mk_install_deps(self, out):
1126        return
1127
1128    def mk_install(self, out):
1129        return
1130
1131    def mk_uninstall(self, out):
1132        return
1133
1134    def is_example(self):
1135        return False
1136
1137    # Invoked when creating a (windows) distribution package using components at build_path, and
1138    # storing them at dist_path
1139    def mk_win_dist(self, build_path, dist_path):
1140        return
1141
1142    def mk_unix_dist(self, build_path, dist_path):
1143        return
1144
1145    # Used to print warnings or errors after mk_make.py is done, so that they
1146    # are not quite as easy to miss.
1147    def final_info(self):
1148        pass
1149
1150class LibComponent(Component):
1151    def __init__(self, name, path, deps, includes2install):
1152        Component.__init__(self, name, path, deps)
1153        self.includes2install = includes2install
1154
1155    def mk_makefile(self, out):
1156        Component.mk_makefile(self, out)
1157        # generate rule for lib
1158        objs = []
1159        for cppfile in get_cpp_files(self.src_dir):
1160            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1161            objs.append(objfile)
1162
1163        libfile = '%s$(LIB_EXT)' % os.path.join(self.build_dir, self.name)
1164        out.write('%s:' % libfile)
1165        for obj in objs:
1166            out.write(' ')
1167            out.write(obj)
1168        out.write('\n')
1169        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
1170        for obj in objs:
1171            out.write(' ')
1172            out.write(obj)
1173        out.write('\n')
1174        out.write('%s: %s\n\n' % (self.name, libfile))
1175
1176    def mk_install_deps(self, out):
1177        return
1178
1179    def mk_install(self, out):
1180        for include in self.includes2install:
1181            MakeRuleCmd.install_files(
1182                out,
1183                os.path.join(self.to_src_dir, include),
1184                os.path.join(INSTALL_INCLUDE_DIR, include)
1185            )
1186
1187    def mk_uninstall(self, out):
1188        for include in self.includes2install:
1189            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include))
1190
1191    def mk_win_dist(self, build_path, dist_path):
1192        mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR))
1193        for include in self.includes2install:
1194            shutil.copy(os.path.join(self.src_dir, include),
1195                        os.path.join(dist_path, INSTALL_INCLUDE_DIR, include))
1196
1197    def mk_unix_dist(self, build_path, dist_path):
1198        self.mk_win_dist(build_path, dist_path)
1199
1200# "Library" containing only .h files. This is just a placeholder for includes files to be installed.
1201class HLibComponent(LibComponent):
1202    def __init__(self, name, path, includes2install):
1203        LibComponent.__init__(self, name, path, [], includes2install)
1204
1205    def mk_makefile(self, out):
1206        return
1207
1208# Auxiliary function for sort_components
1209def comp_components(c1, c2):
1210    id1 = get_component(c1).id
1211    id2 = get_component(c2).id
1212    return id2 - id1
1213
1214# Sort components based on (reverse) definition time
1215def sort_components(cnames):
1216    return sorted(cnames, key=lambda c: get_component(c).id, reverse=True)
1217
1218class ExeComponent(Component):
1219    def __init__(self, name, exe_name, path, deps, install):
1220        Component.__init__(self, name, path, deps)
1221        if exe_name is None:
1222            exe_name = name
1223        self.exe_name = exe_name
1224        self.install = install
1225
1226    def mk_makefile(self, out):
1227        Component.mk_makefile(self, out)
1228        # generate rule for exe
1229
1230        exefile = '%s$(EXE_EXT)' % self.exe_name
1231        out.write('%s:' % exefile)
1232        deps = sort_components(self.deps)
1233        objs = []
1234        for cppfile in get_cpp_files(self.src_dir):
1235            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1236            objs.append(objfile)
1237        for obj in objs:
1238            out.write(' ')
1239            out.write(obj)
1240        for dep in deps:
1241            c_dep = get_component(dep)
1242            out.write(' ' + c_dep.get_link_name())
1243        out.write('\n')
1244        extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else ''
1245        out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile))
1246        for obj in objs:
1247            out.write(' ')
1248            out.write(obj)
1249        for dep in deps:
1250            c_dep = get_component(dep)
1251            out.write(' ' + c_dep.get_link_name())
1252        out.write(' $(LINK_EXTRA_FLAGS)\n')
1253        out.write('%s: %s\n\n' % (self.name, exefile))
1254
1255    def require_install_tactics(self):
1256        return ('tactic' in self.deps) and ('cmd_context' in self.deps)
1257
1258    def require_mem_initializer(self):
1259        return True
1260
1261    # All executables (to be installed) are included in the all: rule
1262    def main_component(self):
1263        return self.install
1264
1265    def mk_install_deps(self, out):
1266        if self.install:
1267            exefile = '%s$(EXE_EXT)' % self.exe_name
1268            out.write('%s' % exefile)
1269
1270    def mk_install(self, out):
1271        if self.install:
1272            exefile = '%s$(EXE_EXT)' % self.exe_name
1273            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile))
1274
1275    def mk_uninstall(self, out):
1276        if self.install:
1277            exefile = '%s$(EXE_EXT)' % self.exe_name
1278            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile))
1279
1280    def mk_win_dist(self, build_path, dist_path):
1281        if self.install:
1282            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1283            shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name),
1284                        '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
1285
1286    def mk_unix_dist(self, build_path, dist_path):
1287        if self.install:
1288            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1289            shutil.copy(os.path.join(build_path, self.exe_name),
1290                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
1291
1292
1293class ExtraExeComponent(ExeComponent):
1294    def __init__(self, name, exe_name, path, deps, install):
1295        ExeComponent.__init__(self, name, exe_name, path, deps, install)
1296
1297    def main_component(self):
1298        return False
1299
1300    def require_mem_initializer(self):
1301        return False
1302
1303def get_so_ext():
1304    sysname = os.uname()[0]
1305    if sysname == 'Darwin':
1306        return 'dylib'
1307    elif sysname == 'Linux' or sysname == 'GNU' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD' or sysname == 'DragonFly':
1308        return 'so'
1309    elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
1310        return 'dll'
1311    else:
1312        assert(False)
1313        return 'dll'
1314
1315class DLLComponent(Component):
1316    def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None):
1317        Component.__init__(self, name, path, deps)
1318        if dll_name is None:
1319            dll_name = name
1320        self.dll_name = dll_name
1321        self.export_files = export_files
1322        self.reexports = reexports
1323        self.install = install
1324        self.static = static
1325        self.staging_link = staging_link    # link a copy of the shared object into this directory on build
1326
1327    def get_link_name(self):
1328        if self.static:
1329            return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
1330        else:
1331            return self.name + '$(SO_EXT)'
1332
1333    def dll_file(self):
1334        """
1335            Return file name of component suitable for use in a Makefile
1336        """
1337        return '%s$(SO_EXT)' % self.dll_name
1338
1339    def install_path(self):
1340        """
1341            Return install location of component (relative to prefix)
1342            suitable for use in a Makefile
1343        """
1344        return os.path.join(INSTALL_LIB_DIR, self.dll_file())
1345
1346    def mk_makefile(self, out):
1347        Component.mk_makefile(self, out)
1348        # generate rule for (SO_EXT)
1349        out.write('%s:' % self.dll_file())
1350        deps = sort_components(self.deps)
1351        objs = []
1352        for cppfile in get_cpp_files(self.src_dir):
1353            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1354            objs.append(objfile)
1355        # Explicitly include obj files of reexport. This fixes problems with exported symbols on Linux and OSX.
1356        for reexport in self.reexports:
1357            reexport = get_component(reexport)
1358            for cppfile in get_cpp_files(reexport.src_dir):
1359                objfile = '%s$(OBJ_EXT)' % os.path.join(reexport.build_dir, os.path.splitext(cppfile)[0])
1360                objs.append(objfile)
1361        for obj in objs:
1362            out.write(' ')
1363            out.write(obj)
1364        for dep in deps:
1365            if dep not in self.reexports:
1366                c_dep = get_component(dep)
1367                out.write(' ' + c_dep.get_link_name())
1368        out.write('\n')
1369        out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file())
1370        for obj in objs:
1371            out.write(' ')
1372            out.write(obj)
1373        for dep in deps:
1374            if dep not in self.reexports:
1375                c_dep = get_component(dep)
1376                out.write(' ' + c_dep.get_link_name())
1377        out.write(' $(SLINK_EXTRA_FLAGS)')
1378        if IS_WINDOWS:
1379            out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name))
1380        if self.staging_link:
1381            if IS_WINDOWS:
1382                out.write('\n\tcopy %s %s' % (self.dll_file(), self.staging_link))
1383            elif IS_OSX:
1384                out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link))
1385            else:
1386                out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link))
1387        out.write('\n')
1388        if self.static:
1389            if IS_WINDOWS:
1390                libfile = '%s-static$(LIB_EXT)' % self.dll_name
1391            else:
1392                libfile = '%s$(LIB_EXT)' % self.dll_name
1393            self.mk_static(out, libfile)
1394            out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile))
1395        else:
1396            out.write('%s: %s\n\n' % (self.name, self.dll_file()))
1397
1398    def mk_static(self, out, libfile):
1399        # generate rule for lib
1400        objs = []
1401        for cppfile in get_cpp_files(self.src_dir):
1402            objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])
1403            objs.append(objfile)
1404        # we have to "reexport" all object files
1405        for dep in self.deps:
1406            dep = get_component(dep)
1407            for cppfile in get_cpp_files(dep.src_dir):
1408                objfile = '%s$(OBJ_EXT)' % os.path.join(dep.build_dir, os.path.splitext(cppfile)[0])
1409                objs.append(objfile)
1410        out.write('%s:' % libfile)
1411        for obj in objs:
1412            out.write(' ')
1413            out.write(obj)
1414        out.write('\n')
1415        out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
1416        for obj in objs:
1417            out.write(' ')
1418            out.write(obj)
1419        out.write('\n')
1420
1421    def main_component(self):
1422        return self.install
1423
1424    def require_install_tactics(self):
1425        return ('tactic' in self.deps) and ('cmd_context' in self.deps)
1426
1427    def require_mem_initializer(self):
1428        return True
1429
1430    def require_def_file(self):
1431        return IS_WINDOWS and self.export_files
1432
1433    def mk_install_deps(self, out):
1434        out.write('%s$(SO_EXT)' % self.dll_name)
1435        if self.static:
1436            out.write(' %s$(LIB_EXT)' % self.dll_name)
1437
1438    def mk_install(self, out):
1439        if self.install:
1440            MakeRuleCmd.install_files(out, self.dll_file(), self.install_path())
1441            if self.static:
1442                libfile = '%s$(LIB_EXT)' % self.dll_name
1443                MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile))
1444
1445    def mk_uninstall(self, out):
1446        MakeRuleCmd.remove_installed_files(out, self.install_path())
1447        libfile = '%s$(LIB_EXT)' % self.dll_name
1448        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
1449
1450    def mk_win_dist(self, build_path, dist_path):
1451        if self.install:
1452            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1453            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1454                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1455            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1456                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1457            shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
1458                        '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1459
1460    def mk_unix_dist(self, build_path, dist_path):
1461        if self.install:
1462            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1463            so = get_so_ext()
1464            shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
1465                        '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
1466            shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
1467                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1468
1469class JsComponent(Component):
1470    def __init__(self):
1471         Component.__init__(self, "js", None, [])
1472
1473    def main_component(self):
1474        return False
1475
1476    def mk_win_dist(self, build_path, dist_path):
1477        return
1478
1479    def mk_unix_dist(self, build_path, dist_path):
1480        return
1481
1482    def mk_makefile(self, out):
1483        return
1484
1485class PythonComponent(Component):
1486    def __init__(self, name, libz3Component):
1487        assert isinstance(libz3Component, DLLComponent)
1488        global PYTHON_ENABLED
1489        Component.__init__(self, name, None, [])
1490        self.libz3Component = libz3Component
1491
1492    def main_component(self):
1493        return False
1494
1495    def mk_win_dist(self, build_path, dist_path):
1496        if not is_python_enabled():
1497            return
1498
1499        src = os.path.join(build_path, 'python', 'z3')
1500        dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
1501        if os.path.exists(dst):
1502            shutil.rmtree(dst)
1503        shutil.copytree(src, dst)
1504
1505    def mk_unix_dist(self, build_path, dist_path):
1506        self.mk_win_dist(build_path, dist_path)
1507
1508    def mk_makefile(self, out):
1509        return
1510
1511class PythonInstallComponent(Component):
1512    def __init__(self, name, libz3Component):
1513        assert isinstance(libz3Component, DLLComponent)
1514        global PYTHON_INSTALL_ENABLED
1515        Component.__init__(self, name, None, [])
1516        self.pythonPkgDir = None
1517        self.in_prefix_install = True
1518        self.libz3Component = libz3Component
1519
1520        if not PYTHON_INSTALL_ENABLED:
1521            return
1522
1523        if IS_WINDOWS:
1524            # Installing under Windows doesn't make sense as the install prefix is used
1525            # but that doesn't make sense under Windows
1526            # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix,
1527            # i.e., something along the lines of C:\Python\... At the moment we are not
1528            # sure whether we would want to install libz3.dll into that directory though.
1529            PYTHON_INSTALL_ENABLED = False
1530            return
1531        else:
1532            PYTHON_INSTALL_ENABLED = True
1533
1534        if IS_WINDOWS or IS_OSX:
1535            # Use full path that is possibly outside of install prefix
1536            self.in_prefix_install = PYTHON_PACKAGE_DIR.startswith(PREFIX)
1537            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
1538        else:
1539            # Use path inside the prefix (should be the normal case on Linux)
1540            # CMW: Also normal on *BSD?
1541            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
1542                raise MKException(('The python package directory ({}) must live ' +
1543                    'under the install prefix ({}) to install the python bindings.' +
1544                    'Use --pypkgdir and --prefix to set the python package directory ' +
1545                    'and install prefix respectively. Note that the python package ' +
1546                    'directory does not need to exist and will be created if ' +
1547                    'necessary during install.').format(
1548                        PYTHON_PACKAGE_DIR,
1549                        PREFIX))
1550            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
1551            self.in_prefix_install = True
1552
1553        if self.in_prefix_install:
1554            assert not os.path.isabs(self.pythonPkgDir)
1555
1556    def final_info(self):
1557        if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED:
1558            print("Warning: The detected Python package directory (%s) is not "
1559                  "in the installation prefix (%s). This can lead to a broken "
1560                  "Python API installation. Use --pypkgdir= to change the "
1561                  "Python package directory." % (PYTHON_PACKAGE_DIR, PREFIX))
1562
1563    def main_component(self):
1564        return False
1565
1566    def mk_install(self, out):
1567        if not is_python_install_enabled():
1568            return
1569        MakeRuleCmd.make_install_directory(out,
1570                                           os.path.join(self.pythonPkgDir, 'z3'),
1571                                           in_prefix=self.in_prefix_install)
1572        MakeRuleCmd.make_install_directory(out,
1573                                           os.path.join(self.pythonPkgDir, 'z3', 'lib'),
1574                                           in_prefix=self.in_prefix_install)
1575
1576        # Sym-link or copy libz3 into python package directory
1577        if IS_WINDOWS or IS_OSX:
1578            MakeRuleCmd.install_files(out,
1579                                      self.libz3Component.dll_file(),
1580                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
1581                                                   self.libz3Component.dll_file()),
1582                                      in_prefix=self.in_prefix_install
1583                                     )
1584        else:
1585            # Create symbolic link to save space.
1586            # It's important that this symbolic link be relative (rather
1587            # than absolute) so that the install is relocatable (needed for
1588            # staged installs that use DESTDIR).
1589            MakeRuleCmd.create_relative_symbolic_link(out,
1590                                                      self.libz3Component.install_path(),
1591                                                      os.path.join(self.pythonPkgDir, 'z3', 'lib',
1592                                                                   self.libz3Component.dll_file()
1593                                                                  ),
1594                                                     )
1595
1596        MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'),
1597                                  os.path.join(self.pythonPkgDir, 'z3'),
1598                                  in_prefix=self.in_prefix_install)
1599        if sys.version >= "3":
1600            pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__')
1601            MakeRuleCmd.make_install_directory(out,
1602                                               pythonPycacheDir,
1603                                               in_prefix=self.in_prefix_install)
1604            MakeRuleCmd.install_files(out,
1605                                      os.path.join('python', 'z3', '__pycache__', '*.pyc'),
1606                                      pythonPycacheDir,
1607                                      in_prefix=self.in_prefix_install)
1608        else:
1609            MakeRuleCmd.install_files(out,
1610                                      os.path.join('python', 'z3', '*.pyc'),
1611                                      os.path.join(self.pythonPkgDir,'z3'),
1612                                      in_prefix=self.in_prefix_install)
1613
1614        if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
1615            out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
1616
1617    def mk_uninstall(self, out):
1618        if not is_python_install_enabled():
1619            return
1620        MakeRuleCmd.remove_installed_files(out,
1621                                           os.path.join(self.pythonPkgDir,
1622                                                        self.libz3Component.dll_file()),
1623                                           in_prefix=self.in_prefix_install
1624                                          )
1625        MakeRuleCmd.remove_installed_files(out,
1626                                           os.path.join(self.pythonPkgDir, 'z3', '*.py'),
1627                                           in_prefix=self.in_prefix_install)
1628        MakeRuleCmd.remove_installed_files(out,
1629                                           os.path.join(self.pythonPkgDir, 'z3', '*.pyc'),
1630                                           in_prefix=self.in_prefix_install)
1631        MakeRuleCmd.remove_installed_files(out,
1632                                           os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
1633                                           in_prefix=self.in_prefix_install
1634                                          )
1635        MakeRuleCmd.remove_installed_files(out,
1636                                           os.path.join(self.pythonPkgDir, 'z3', 'lib',
1637                                                        self.libz3Component.dll_file()))
1638
1639    def mk_makefile(self, out):
1640        return
1641
1642def set_key_file(self):
1643    global DOTNET_KEY_FILE
1644    # We need to give the assembly a strong name so that it
1645    # can be installed into the GAC with ``make install``
1646    if not DOTNET_KEY_FILE is None:
1647       self.key_file = DOTNET_KEY_FILE
1648
1649    if not self.key_file is None:
1650       if os.path.isfile(self.key_file):
1651           self.key_file = os.path.abspath(self.key_file)
1652       elif os.path.isfile(os.path.join(self.src_dir, self.key_file)):
1653           self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file))
1654       else:
1655           print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
1656           self.key_file = None
1657
1658
1659# build for dotnet core
1660class DotNetDLLComponent(Component):
1661    def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file):
1662        Component.__init__(self, name, path, deps)
1663        if dll_name is None:
1664            dll_name = name
1665        if assembly_info_dir is None:
1666            assembly_info_dir = "."
1667        self.dll_name          = dll_name
1668        self.assembly_info_dir = assembly_info_dir
1669        self.key_file = default_key_file
1670
1671
1672    def mk_makefile(self, out):
1673        if not is_dotnet_core_enabled():
1674            return
1675        cs_fp_files = []
1676        for cs_file in get_cs_files(self.src_dir):
1677            cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
1678        if self.assembly_info_dir != '.':
1679            for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
1680                cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
1681        dllfile = '%s.dll' % self.dll_name
1682        out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
1683        for cs_file in cs_fp_files:
1684            out.write(' ')
1685            out.write(cs_file)
1686        out.write('\n')
1687
1688        set_key_file(self)
1689        key = ""
1690        if not self.key_file is None:
1691            key = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
1692            key += "\n<SignAssembly>true</SignAssembly>"
1693
1694        version = get_version_string(3)
1695
1696        core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
1697
1698  <PropertyGroup>
1699    <TargetFramework>netstandard1.4</TargetFramework>
1700    <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
1701    <DebugType>portable</DebugType>
1702    <AssemblyName>Microsoft.Z3</AssemblyName>
1703    <OutputType>Library</OutputType>
1704    <PackageId>Microsoft.Z3</PackageId>
1705    <GenerateDocumentationFile>true</GenerateDocumentationFile>
1706    <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
1707    <Version>%s</Version>
1708    <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
1709    <Authors>Microsoft</Authors>
1710    <Company>Microsoft</Company>
1711    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
1712    <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
1713    <Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
1714    <PackageTags>smt constraint solver theorem prover</PackageTags>
1715    %s
1716  </PropertyGroup>
1717
1718  <ItemGroup>
1719    <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
1720  </ItemGroup>
1721
1722</Project>""" % (version, key, self.to_src_dir)
1723
1724        mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
1725        csproj = os.path.join('dotnet', 'z3.csproj')
1726        with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
1727            ous.write(core_csproj_str)
1728
1729        dotnetCmdLine = [DOTNET, "build", csproj]
1730
1731        dotnetCmdLine.extend(['-c'])
1732        if DEBUG_MODE:
1733            dotnetCmdLine.extend(['Debug'])
1734        else:
1735            dotnetCmdLine.extend(['Release'])
1736
1737        path = os.path.join(os.path.abspath(BUILD_DIR), ".")
1738        dotnetCmdLine.extend(['-o', "\"%s\"" % path])
1739
1740        MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
1741        out.write('\n')
1742        out.write('%s: %s\n\n' % (self.name, dllfile))
1743
1744    def main_component(self):
1745        return is_dotnet_core_enabled()
1746
1747    def has_assembly_info(self):
1748        # TBD: is this required for dotnet core given that version numbers are in z3.csproj file?
1749        return False
1750
1751
1752    def mk_win_dist(self, build_path, dist_path):
1753        if is_dotnet_core_enabled():
1754            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1755            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1756                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1757            shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1758                        '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1759            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
1760                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1761            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
1762                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1763            if DEBUG_MODE:
1764                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
1765                            '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1766
1767    def mk_unix_dist(self, build_path, dist_path):
1768        if is_dotnet_core_enabled():
1769            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1770            shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
1771                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1772            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
1773                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1774            shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name),
1775                        '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
1776
1777    def mk_install_deps(self, out):
1778        pass
1779
1780    def mk_install(self, out):
1781        pass
1782
1783    def mk_uninstall(self, out):
1784        pass
1785
1786class JavaDLLComponent(Component):
1787    def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
1788        Component.__init__(self, name, path, deps)
1789        if dll_name is None:
1790            dll_name = name
1791        self.dll_name     = dll_name
1792        self.package_name = package_name
1793        self.manifest_file = manifest_file
1794        self.install = not is_windows()
1795
1796    def mk_makefile(self, out):
1797        global JAVAC
1798        global JAR
1799
1800        if is_java_enabled():
1801            mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
1802            dllfile = '%s$(SO_EXT)' % self.dll_name
1803            out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
1804            t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s" -I"%s/PLATFORM" -I%s %s/Native.cpp\n' % (JNI_HOME, JNI_HOME, get_component('api').to_src_dir, self.to_src_dir)
1805            if IS_OSX:
1806                t = t.replace('PLATFORM', 'darwin')
1807            elif is_linux():
1808                t = t.replace('PLATFORM', 'linux')
1809            elif is_hurd():
1810                t = t.replace('PLATFORM', 'hurd')
1811            elif IS_FREEBSD:
1812                t = t.replace('PLATFORM', 'freebsd')
1813            elif IS_NETBSD:
1814                t = t.replace('PLATFORM', 'netbsd')
1815            elif IS_OPENBSD:
1816                t = t.replace('PLATFORM', 'openbsd')
1817            elif IS_SUNOS:
1818                t = t.replace('PLATFORM', 'SunOS')
1819            elif IS_CYGWIN:
1820                t = t.replace('PLATFORM', 'cygwin')
1821            elif IS_MSYS2:
1822                t = t.replace('PLATFORM', 'win32')
1823            else:
1824                t = t.replace('PLATFORM', 'win32')
1825            out.write(t)
1826            if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
1827                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
1828                          os.path.join('api', 'java', 'Native'))
1829            else:
1830                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
1831                          os.path.join('api', 'java', 'Native'))
1832            out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
1833            deps = ''
1834            for jfile in get_java_files(self.src_dir):
1835                deps += ('%s ' % os.path.join(self.to_src_dir, jfile))
1836            for jfile in get_java_files(os.path.join(self.src_dir, "enumerations")):
1837                deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile)
1838            out.write(deps)
1839            out.write('\n')
1840            #if IS_WINDOWS:
1841            JAVAC = '"%s"' % JAVAC
1842            JAR = '"%s"' % JAR
1843            t = ('\t%s -source 1.8 -target 1.8 %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
1844            out.write(t)
1845            t = ('\t%s -source 1.8 -target 1.8 -cp %s %s.java -d %s\n' % (JAVAC,
1846                                                  os.path.join('api', 'java', 'classes'),
1847                                                  os.path.join(self.to_src_dir, '*'),
1848                                                  os.path.join('api', 'java', 'classes')))
1849            out.write(t)
1850            out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
1851                                                         os.path.join(self.to_src_dir, 'manifest'),
1852                                                         os.path.join('api', 'java', 'classes')))
1853            out.write('java: %s.jar\n\n' % self.package_name)
1854
1855    def main_component(self):
1856        return is_java_enabled()
1857
1858    def mk_win_dist(self, build_path, dist_path):
1859        if JAVA_ENABLED:
1860            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1861            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
1862                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
1863            shutil.copy(os.path.join(build_path, 'libz3java.dll'),
1864                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll'))
1865            shutil.copy(os.path.join(build_path, 'libz3java.lib'),
1866                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib'))
1867
1868    def mk_unix_dist(self, build_path, dist_path):
1869        if JAVA_ENABLED:
1870            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
1871            shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
1872                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
1873            so = get_so_ext()
1874            shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
1875                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
1876
1877    def mk_install(self, out):
1878        if is_java_enabled() and self.install:
1879            dllfile = '%s$(SO_EXT)' % self.dll_name
1880            MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile))
1881            jarfile = '{}.jar'.format(self.package_name)
1882            MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile))
1883
1884    def mk_uninstall(self, out):
1885        if is_java_enabled() and self.install:
1886            dllfile = '%s$(SO_EXT)' % self.dll_name
1887            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
1888            jarfile = '{}.jar'.format(self.package_name)
1889            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))
1890
1891class MLComponent(Component):
1892
1893    def __init__(self, name, lib_name, path, deps):
1894        Component.__init__(self, name, path, deps)
1895        if lib_name is None:
1896            lib_name = name
1897        self.lib_name = lib_name
1898        self.modules = ["z3enums", "z3native", "z3"]  # dependencies in this order!
1899        self.stubs = "z3native_stubs"
1900        self.sub_dir = os.path.join('api', 'ml')
1901
1902        self.destdir = ""
1903        self.ldconf = ""
1904        # Calling _init_ocamlfind_paths() is postponed to later because
1905        # OCAMLFIND hasn't been checked yet.
1906
1907    def _install_bindings(self):
1908        # FIXME: Depending on global state is gross.  We can't pre-compute this
1909        # in the constructor because we haven't tested for ocamlfind yet
1910        return OCAMLFIND != ''
1911
1912    def _init_ocamlfind_paths(self):
1913        """
1914            Initialises self.destdir and self.ldconf
1915            Do not call this from the MLComponent constructor because OCAMLFIND
1916            has not been checked at that point
1917        """
1918        if self.destdir != "" and self.ldconf != "":
1919            # Initialisation already done
1920            return
1921        # Use Ocamlfind to get the default destdir and ldconf path
1922        self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir'])
1923        if self.destdir == "":
1924            raise MKException('Failed to get OCaml destdir')
1925
1926        if not os.path.isdir(self.destdir):
1927            raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir))
1928
1929        self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf'])
1930        if self.ldconf == "":
1931            raise MKException('Failed to get OCaml ldconf path')
1932
1933    def final_info(self):
1934        if not self._install_bindings():
1935            print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed")
1936
1937    def mk_makefile(self, out):
1938        if is_ml_enabled():
1939            CP_CMD = 'cp'
1940            if IS_WINDOWS:
1941                CP_CMD='copy'
1942
1943            OCAML_FLAGS = ''
1944            if DEBUG_MODE:
1945                OCAML_FLAGS += '-g'
1946
1947            if OCAMLFIND:
1948                OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package zarith' + ' ' + OCAML_FLAGS
1949                OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package zarith' + ' ' + OCAML_FLAGS
1950            else:
1951                OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
1952                OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
1953
1954            src_dir = self.to_src_dir
1955            mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
1956            api_src = get_component(API_COMPONENT).to_src_dir
1957            # remove /GL and -std=c++17; the ocaml tools don't like them.
1958            if IS_WINDOWS:
1959                out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n')
1960            else:
1961                out.write('CXXFLAGS_OCAML=$(subst -std=c++17,,$(CXXFLAGS))\n')
1962
1963            substitutions = { 'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) }
1964
1965            configure_file(os.path.join(self.src_dir, 'META.in'),
1966                           os.path.join(BUILD_DIR, self.sub_dir, 'META'),
1967                           substitutions)
1968
1969            stubsc = os.path.join(src_dir, self.stubs + '.c')
1970            stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
1971            base_dll_name = get_component(Z3_DLL_COMPONENT).dll_name
1972            if STATIC_LIB:
1973                z3link = 'z3-static'
1974                z3linkdep = base_dll_name + '-static$(LIB_EXT)'
1975                out.write('%s: %s\n' % (z3linkdep, base_dll_name + '$(LIB_EXT)'))
1976                out.write('\tcp $< $@\n')
1977            else:
1978                z3link = 'z3'
1979                z3linkdep = base_dll_name + '$(SO_EXT)'
1980            out.write('%s: %s %s\n' % (stubso, stubsc, z3linkdep))
1981            out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
1982                      (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))
1983
1984            cmos = ''
1985            for m in self.modules:
1986                ml = os.path.join(src_dir, m + '.ml')
1987                cmo = os.path.join(self.sub_dir, m + '.cmo')
1988                existing_mli = os.path.join(src_dir, m + '.mli')
1989                mli = os.path.join(self.sub_dir, m + '.mli')
1990                cmi = os.path.join(self.sub_dir, m + '.cmi')
1991                out.write('%s: %s %s\n' % (cmo, ml, cmos))
1992                if (os.path.exists(existing_mli[3:])):
1993                    out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
1994                else:
1995                    out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli))
1996                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
1997                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml))
1998                cmos = cmos + cmo + ' '
1999
2000            cmxs = ''
2001            for m in self.modules:
2002                ff = os.path.join(src_dir, m + '.ml')
2003                ft = os.path.join(self.sub_dir, m + '.cmx')
2004                out.write('%s: %s %s %s\n' % (ft, ff, cmos, cmxs))
2005                out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
2006                cmxs = cmxs + ' ' + ft
2007
2008
2009            OCAMLMKLIB = 'ocamlmklib'
2010
2011            LIBZ3 = '-l' + z3link + ' -lstdc++'
2012            if is_cygwin() and not(is_cygwin_mingw()):
2013                LIBZ3 = z3linkdep
2014
2015            LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))
2016
2017            stubs_install_path = '$$(%s printconf path)/stublibs' % OCAMLFIND
2018            if not STATIC_LIB:
2019                loadpath = '-ccopt -L' + stubs_install_path
2020                dllpath = '-dllpath ' + stubs_install_path
2021                LIBZ3 = LIBZ3 + ' ' + loadpath + ' ' + dllpath
2022
2023            if DEBUG_MODE and not(is_cygwin()):
2024                # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
2025                OCAMLMKLIB += ' -g'
2026
2027            z3mls = os.path.join(self.sub_dir, 'z3ml')
2028
2029            LIBZ3ML = ''
2030            if STATIC_LIB:
2031                LIBZ3ML = '-oc ' + os.path.join(self.sub_dir, 'z3ml-static')
2032
2033            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))
2034            out.write('\t%s -o %s %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, LIBZ3ML, self.sub_dir, stubso, cmos, LIBZ3))
2035            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))
2036            out.write('\t%s -o %s %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, LIBZ3ML, self.sub_dir, stubso, cmxs, LIBZ3))
2037            out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
2038            out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
2039
2040            out.write('\n')
2041            out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
2042            if IS_OSX:
2043                out.write('\tinstall_name_tool -id %s/libz3.dylib libz3.dylib\n' % (stubs_install_path))
2044                out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path))
2045            out.write('\n')
2046
2047            if IS_WINDOWS:
2048                out.write('ocamlfind_install: ')
2049                self.mk_install_deps(out)
2050                out.write('\n')
2051                self.mk_install(out)
2052                out.write('\n')
2053                out.write('ocamlfind_uninstall:\n')
2054                self.mk_uninstall(out)
2055                out.write('\n')
2056
2057    # The following three functions may be out of date.
2058    def mk_install_deps(self, out):
2059        if is_ml_enabled() and self._install_bindings():
2060            out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
2061            out.write(os.path.join(self.sub_dir, 'META '))
2062            out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
2063            out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
2064            out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))
2065
2066    def mk_install(self, out):
2067        if is_ml_enabled() and self._install_bindings():
2068            self._init_ocamlfind_paths()
2069            in_prefix = self.destdir.startswith(PREFIX)
2070            maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX)
2071            # Note that when doing a staged install with DESTDIR that modifying
2072            # OCaml's ``ld.conf`` may fail. Therefore packagers will need to
2073            # make their packages modify it manually at package install time
2074            # as opposed to ``make install`` time.
2075            MakeRuleCmd.make_install_directory(out,
2076                                               maybe_stripped_destdir,
2077                                               in_prefix=in_prefix)
2078            out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format(
2079                ldconf=self.ldconf,
2080                ocamlfind=OCAMLFIND,
2081                ocaml_destdir=self.destdir,
2082                metafile=os.path.join(self.sub_dir, 'META')))
2083
2084            for m in self.modules:
2085                mli = os.path.join(self.src_dir, m) + '.mli'
2086                if os.path.exists(mli):
2087                    out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
2088                else:
2089                    out.write(' ' + os.path.join(self.sub_dir, m) + '.mli')
2090                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
2091                out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx')
2092            out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
2093            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
2094            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma'))))
2095            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa'))))
2096            out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs'))))
2097            out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
2098            if is_windows() or is_cygwin_mingw():
2099                out.write('.dll')
2100            else:
2101                out.write('.so') # .so also on OSX!
2102            out.write('\n')
2103
2104    def mk_uninstall(self, out):
2105        if is_ml_enabled() and self._install_bindings():
2106            self._init_ocamlfind_paths()
2107            out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format(
2108                ldconf=self.ldconf,
2109                ocamlfind=OCAMLFIND,
2110                ocaml_destdir=self.destdir))
2111
2112    def main_component(self):
2113        return is_ml_enabled()
2114
2115class ExampleComponent(Component):
2116    def __init__(self, name, path):
2117        Component.__init__(self, name, path, [])
2118        self.ex_dir   = os.path.join(EXAMPLE_DIR, self.path)
2119        self.to_ex_dir = os.path.join(REV_BUILD_DIR, self.ex_dir)
2120
2121    def is_example(self):
2122        return True
2123
2124class CppExampleComponent(ExampleComponent):
2125    def __init__(self, name, path):
2126        ExampleComponent.__init__(self, name, path)
2127
2128    def compiler(self):
2129        return "$(CXX)"
2130
2131    def src_files(self):
2132        return get_cpp_files(self.ex_dir)
2133
2134    def mk_makefile(self, out):
2135        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
2136        dll = '%s$(SO_EXT)' % dll_name
2137
2138        objfiles = ''
2139        for cppfile in self.src_files():
2140            objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')])
2141            objfiles = objfiles + ('%s ' % objfile)
2142            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile)));
2143            out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
2144            # Add include dir components
2145            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
2146            out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
2147            out.write(' %s' % os.path.join(self.to_ex_dir, cppfile))
2148            out.write('\n')
2149
2150        exefile = '%s$(EXE_EXT)' % self.name
2151        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
2152        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
2153        if IS_WINDOWS:
2154            out.write('%s.lib' % dll_name)
2155        else:
2156            out.write(dll)
2157        out.write(' $(LINK_EXTRA_FLAGS)\n')
2158        out.write('_ex_%s: %s\n\n' % (self.name, exefile))
2159
2160class CExampleComponent(CppExampleComponent):
2161    def __init__(self, name, path):
2162        CppExampleComponent.__init__(self, name, path)
2163
2164    def compiler(self):
2165        return "$(CC)"
2166
2167    def src_files(self):
2168        return get_c_files(self.ex_dir)
2169
2170    def mk_makefile(self, out):
2171        dll_name = get_component(Z3_DLL_COMPONENT).dll_name
2172        dll = '%s$(SO_EXT)' % dll_name
2173
2174        objfiles = ''
2175        for cfile in self.src_files():
2176            objfile = '%s$(OBJ_EXT)' % (cfile[:cfile.rfind('.')])
2177            objfiles = objfiles + ('%s ' % objfile)
2178            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cfile)));
2179            out.write('\t%s $(CFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(C_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
2180            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
2181            out.write(' %s' % os.path.join(self.to_ex_dir, cfile))
2182            out.write('\n')
2183
2184        exefile = '%s$(EXE_EXT)' % self.name
2185        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
2186        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
2187        if IS_WINDOWS:
2188            out.write('%s.lib' % dll_name)
2189        else:
2190            out.write(dll)
2191        out.write(' $(LINK_EXTRA_FLAGS)\n')
2192        out.write('_ex_%s: %s\n\n' % (self.name, exefile))
2193
2194class DotNetExampleComponent(ExampleComponent):
2195    def __init__(self, name, path):
2196        ExampleComponent.__init__(self, name, path)
2197
2198    def is_example(self):
2199        return is_dotnet_core_enabled()
2200
2201    def mk_makefile(self, out):
2202        if is_dotnet_core_enabled():
2203            proj_name = 'dotnet_example.csproj'
2204            out.write('_ex_%s:' % self.name)
2205            for csfile in get_cs_files(self.ex_dir):
2206                out.write(' ')
2207                out.write(os.path.join(self.to_ex_dir, csfile))
2208
2209            mk_dir(os.path.join(BUILD_DIR, 'dotnet_example'))
2210            csproj = os.path.join('dotnet_example', proj_name)
2211            if VS_X64:
2212                platform = 'x64'
2213            elif VS_ARM:
2214                platform = 'ARM'
2215            else:
2216                platform = 'x86'
2217
2218            dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk">
2219  <PropertyGroup>
2220    <OutputType>Exe</OutputType>
2221    <TargetFramework>netcoreapp2.0</TargetFramework>
2222    <PlatformTarget>%s</PlatformTarget>
2223  </PropertyGroup>
2224  <ItemGroup>
2225    <Compile Include="..\%s/*.cs" />
2226    <Reference Include="Microsoft.Z3">
2227      <HintPath>..\Microsoft.Z3.dll</HintPath>
2228    </Reference>
2229  </ItemGroup>
2230</Project>""" % (platform, self.to_ex_dir)
2231
2232            with open(os.path.join(BUILD_DIR, csproj), 'w') as ous:
2233                ous.write(dotnet_proj_str)
2234
2235            out.write('\n')
2236            dotnetCmdLine = [DOTNET, "build", csproj]
2237            dotnetCmdLine.extend(['-c'])
2238            if DEBUG_MODE:
2239                dotnetCmdLine.extend(['Debug'])
2240            else:
2241                dotnetCmdLine.extend(['Release'])
2242            MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
2243            out.write('\n')
2244
2245class JavaExampleComponent(ExampleComponent):
2246    def __init__(self, name, path):
2247        ExampleComponent.__init__(self, name, path)
2248
2249    def is_example(self):
2250        return JAVA_ENABLED
2251
2252    def mk_makefile(self, out):
2253        if JAVA_ENABLED:
2254            pkg = get_component(JAVA_COMPONENT).package_name + '.jar'
2255            out.write('JavaExample.class: %s' % (pkg))
2256            deps = ''
2257            for jfile in get_java_files(self.ex_dir):
2258                out.write(' %s' % os.path.join(self.to_ex_dir, jfile))
2259            if IS_WINDOWS:
2260                deps = deps.replace('/', '\\')
2261            out.write('%s\n' % deps)
2262            out.write('\t%s -cp %s ' % (JAVAC, pkg))
2263            win_ex_dir = self.to_ex_dir
2264            for javafile in get_java_files(self.ex_dir):
2265                out.write(' ')
2266                out.write(os.path.join(win_ex_dir, javafile))
2267            out.write(' -d .\n')
2268            out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
2269
2270class MLExampleComponent(ExampleComponent):
2271    def __init__(self, name, path):
2272        ExampleComponent.__init__(self, name, path)
2273
2274    def is_example(self):
2275        return ML_ENABLED
2276
2277    def mk_makefile(self, out):
2278        if ML_ENABLED:
2279            out.write('ml_example.byte: api/ml/z3ml.cma')
2280            for mlfile in get_ml_files(self.ex_dir):
2281                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
2282            out.write('\n')
2283            out.write('\tocamlfind %s ' % OCAMLC)
2284            if DEBUG_MODE:
2285                out.write('-g ')
2286            out.write('-custom -o ml_example.byte -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cma')
2287            for mlfile in get_ml_files(self.ex_dir):
2288                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
2289            out.write('\n')
2290            out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa')
2291            for mlfile in get_ml_files(self.ex_dir):
2292                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
2293            out.write('\n')
2294            out.write('\tocamlfind %s ' % OCAMLOPT)
2295            if DEBUG_MODE:
2296                out.write('-g ')
2297            out.write('-o ml_example$(EXE_EXT) -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cmxa')
2298            for mlfile in get_ml_files(self.ex_dir):
2299                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
2300            out.write('\n')
2301            out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
2302
2303        debug_opt = '-g ' if DEBUG_MODE else ''
2304
2305        if STATIC_LIB:
2306            opam_z3_opts = '-thread -package z3-static -linkpkg'
2307            ml_post_install_tests = [
2308                (OCAMLC,              'ml_example_static.byte'),
2309                (OCAMLC + ' -custom', 'ml_example_static_custom.byte'),
2310                (OCAMLOPT,            'ml_example_static$(EXE_EXT)')
2311            ]
2312        else:
2313            opam_z3_opts = '-thread -package z3 -linkpkg'
2314            ml_post_install_tests = [
2315                (OCAMLC,              'ml_example_shared.byte'),
2316                (OCAMLC + ' -custom', 'ml_example_shared_custom.byte'),
2317                (OCAMLOPT,            'ml_example_shared$(EXE_EXT)')
2318            ]
2319
2320        for ocaml_compiler, testname in ml_post_install_tests:
2321            out.write(testname + ':')
2322            for mlfile in get_ml_files(self.ex_dir):
2323                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
2324            out.write('\n')
2325            out.write('\tocamlfind %s -o %s %s %s ' % (ocaml_compiler, debug_opt, testname, opam_z3_opts))
2326            for mlfile in get_ml_files(self.ex_dir):
2327                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
2328            out.write('\n')
2329
2330        if STATIC_LIB:
2331            out.write('_ex_ml_example_post_install: ml_example_static.byte ml_example_static_custom.byte ml_example_static$(EXE_EXT)\n')
2332        else:
2333            out.write('_ex_ml_example_post_install: ml_example_shared.byte ml_example_shared_custom.byte ml_example_shared$(EXE_EXT)\n')
2334
2335        out.write('\n')
2336
2337
2338class PythonExampleComponent(ExampleComponent):
2339    def __init__(self, name, path):
2340        ExampleComponent.__init__(self, name, path)
2341
2342    # Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked.
2343    # We don't need to include them in the :examples rule
2344    def mk_makefile(self, out):
2345        full = os.path.join(EXAMPLE_DIR, self.path)
2346        for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
2347            shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py))
2348            if is_verbose():
2349                print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python')))
2350        out.write('_ex_%s: \n\n' % self.name)
2351
2352    def mk_win_dist(self, build_path, dist_path):
2353        full = os.path.join(EXAMPLE_DIR, self.path)
2354        py = 'example.py'
2355        shutil.copyfile(os.path.join(full, py),
2356                        os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))
2357
2358    def mk_unix_dist(self, build_path, dist_path):
2359        self.mk_win_dist(build_path, dist_path)
2360
2361
2362def reg_component(name, c):
2363    global _Id, _Components, _ComponentNames, _Name2Component
2364    c.id = _Id
2365    _Id = _Id + 1
2366    _Components.append(c)
2367    _ComponentNames.add(name)
2368    _Name2Component[name] = c
2369    if VERBOSE:
2370        print("New component: '%s'" % name)
2371
2372def add_lib(name, deps=[], path=None, includes2install=[]):
2373    c = LibComponent(name, path, deps, includes2install)
2374    reg_component(name, c)
2375
2376def add_clib(name, deps=[], path=None, includes2install=[]):
2377    c = CLibComponent(name, path, deps, includes2install)
2378    reg_component(name, c)
2379
2380def add_hlib(name, path=None, includes2install=[]):
2381    c = HLibComponent(name, path, includes2install)
2382    reg_component(name, c)
2383
2384def add_exe(name, deps=[], path=None, exe_name=None, install=True):
2385    c = ExeComponent(name, exe_name, path, deps, install)
2386    reg_component(name, c)
2387
2388def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
2389    c = ExtraExeComponent(name, exe_name, path, deps, install)
2390    reg_component(name, c)
2391
2392def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None):
2393    c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link)
2394    reg_component(name, c)
2395    return c
2396
2397def add_dot_net_core_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None):
2398    c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
2399    reg_component(name, c)
2400
2401def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None):
2402    c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
2403    reg_component(name, c)
2404
2405def add_python(libz3Component):
2406    name = 'python'
2407    reg_component(name, PythonComponent(name, libz3Component))
2408
2409def add_js():
2410    reg_component('js', JsComponent())
2411
2412def add_python_install(libz3Component):
2413    name = 'python_install'
2414    reg_component(name, PythonInstallComponent(name, libz3Component))
2415
2416def add_ml_lib(name, deps=[], path=None, lib_name=None):
2417    c = MLComponent(name, lib_name, path, deps)
2418    reg_component(name, c)
2419
2420def add_cpp_example(name, path=None):
2421    c = CppExampleComponent(name, path)
2422    reg_component(name, c)
2423
2424def add_c_example(name, path=None):
2425    c = CExampleComponent(name, path)
2426    reg_component(name, c)
2427
2428def add_dotnet_example(name, path=None):
2429    c = DotNetExampleComponent(name, path)
2430    reg_component(name, c)
2431
2432def add_java_example(name, path=None):
2433    c = JavaExampleComponent(name, path)
2434    reg_component(name, c)
2435
2436def add_ml_example(name, path=None):
2437    c = MLExampleComponent(name, path)
2438    reg_component(name, c)
2439
2440def add_z3py_example(name, path=None):
2441    c = PythonExampleComponent(name, path)
2442    reg_component(name, c)
2443
2444def mk_config():
2445    if ONLY_MAKEFILES:
2446        return
2447    config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
2448    global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED
2449    if IS_WINDOWS:
2450        CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++17'
2451        config.write(
2452            'CC=cl\n'
2453            'CXX=cl\n'
2454            'CXX_OUT_FLAG=/Fo\n'
2455            'C_OUT_FLAG=/Fo\n'
2456            'OBJ_EXT=.obj\n'
2457            'LIB_EXT=.lib\n'
2458            'AR=lib\n'
2459            'AR_OUTFLAG=/OUT:\n'
2460            'EXE_EXT=.exe\n'
2461            'LINK=cl\n'
2462            'LINK_OUT_FLAG=/Fe\n'
2463            'SO_EXT=.dll\n'
2464            'SLINK=cl\n'
2465            'SLINK_OUT_FLAG=/Fe\n'
2466            'OS_DEFINES=/D _WINDOWS\n')
2467        extra_opt = ''
2468        link_extra_opt = ''
2469        if LOG_SYNC:
2470            extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt
2471        if SINGLE_THREADED:
2472            extra_opt = '%s /DSINGLE_THREAD' % extra_opt
2473        if GIT_HASH:
2474            extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
2475        if GUARD_CF:
2476            extra_opt = ' %s /guard:cf' % extra_opt
2477            link_extra_opt = ' %s /GUARD:CF' % link_extra_opt
2478        if STATIC_BIN:
2479            static_opt = '/MT'
2480        else:
2481            static_opt = '/MD'
2482        maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO'
2483        if DEBUG_MODE:
2484            static_opt = static_opt + 'd'
2485            config.write(
2486                'AR_FLAGS=/nologo\n'
2487                'LINK_FLAGS=/nologo %s\n'
2488                'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
2489            if VS_X64:
2490                config.write(
2491                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
2492                config.write(
2493                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2494                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
2495            elif VS_ARM:
2496                print("ARM on VS is unsupported")
2497                exit(1)
2498            else:
2499                config.write(
2500                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
2501                config.write(
2502                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2503                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
2504        else:
2505            # Windows Release mode
2506            LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
2507            GL = ' /GL' if SLOW_OPTIMIZE else ''
2508            config.write(
2509                'AR_FLAGS=/nologo %s\n'
2510                'LINK_FLAGS=/nologo %s\n'
2511                'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt))
2512            if TRACE:
2513                extra_opt = '%s /D _TRACE ' % extra_opt
2514            if VS_X64:
2515                config.write(
2516                    'CXXFLAGS=/c%s %s /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
2517                config.write(
2518                    'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
2519                    'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
2520            elif VS_ARM:
2521                print("ARM on VS is unsupported")
2522                exit(1)
2523            else:
2524                config.write(
2525                    'CXXFLAGS=/c%s %s /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
2526                config.write(
2527                    'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
2528                    'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
2529
2530        config.write('CFLAGS=$(CXXFLAGS)\n')
2531
2532        # End of Windows VS config.mk
2533        if is_verbose():
2534            print('64-bit:         %s' % is64())
2535            if is_java_enabled():
2536                print('JNI Bindings:   %s' % JNI_HOME)
2537                print('Java Compiler:  %s' % JAVAC)
2538            if is_ml_enabled():
2539                print('OCaml Compiler: %s' % OCAMLC)
2540                print('OCaml Find tool: %s' % OCAMLFIND)
2541                print('OCaml Native:   %s' % OCAMLOPT)
2542                print('OCaml Library:  %s' % OCAML_LIB)
2543    else:
2544        OS_DEFINES = ""
2545        ARITH = "internal"
2546        check_ar()
2547        CXX = find_cxx_compiler()
2548        CC  = find_c_compiler()
2549#       SLIBEXTRAFLAGS = ''
2550        SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
2551        EXE_EXT = ''
2552        LIB_EXT = '.a'
2553        if GPROF:
2554            CXXFLAGS = '%s -pg' % CXXFLAGS
2555            LDFLAGS  = '%s -pg' % LDFLAGS
2556        if GMP:
2557            test_gmp(CXX)
2558            ARITH = "gmp"
2559            CPPFLAGS = '%s -D_MP_GMP' % CPPFLAGS
2560            LDFLAGS  = '%s -lgmp' % LDFLAGS
2561            SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
2562        else:
2563            CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
2564        if GIT_HASH:
2565            CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
2566        CXXFLAGS = '%s -std=c++17' % CXXFLAGS
2567        CXXFLAGS = '%s -fvisibility=hidden -fvisibility-inlines-hidden -c' % CXXFLAGS
2568        FPMATH = test_fpmath(CXX)
2569        CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
2570        if LOG_SYNC:
2571            CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
2572        if SINGLE_THREADED:
2573            CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS
2574        if DEBUG_MODE:
2575            CXXFLAGS     = '%s -g -Wall' % CXXFLAGS
2576            EXAMP_DEBUG_FLAG = '-g'
2577            CPPFLAGS     = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
2578        else:
2579            CXXFLAGS     = '%s -O3' % CXXFLAGS
2580            if GPROF:
2581                CXXFLAGS     += '-fomit-frame-pointer'
2582            CPPFLAGS     = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
2583        if is_CXX_clangpp():
2584            CXXFLAGS   = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
2585        sysname, _, _, _, machine = os.uname()
2586        if sysname == 'Darwin':
2587            SO_EXT         = '.dylib'
2588            SLIBFLAGS      = '-dynamiclib'
2589        elif sysname == 'Linux':
2590            CXXFLAGS       = '%s -D_LINUX_' % CXXFLAGS
2591            OS_DEFINES     = '-D_LINUX_'
2592            SO_EXT         = '.so'
2593            SLIBFLAGS      = '-shared'
2594            SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
2595        elif sysname == 'GNU':
2596            CXXFLAGS       = '%s -D_HURD_' % CXXFLAGS
2597            OS_DEFINES     = '-D_HURD_'
2598            SO_EXT         = '.so'
2599            SLIBFLAGS      = '-shared'
2600        elif sysname == 'FreeBSD' or sysname == 'DragonFly':
2601            CXXFLAGS       = '%s -D_FREEBSD_' % CXXFLAGS
2602            OS_DEFINES     = '-D_FREEBSD_'
2603            SO_EXT         = '.so'
2604            SLIBFLAGS      = '-shared'
2605        elif sysname == 'NetBSD':
2606            CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
2607            OS_DEFINES     = '-D_NETBSD_'
2608            SO_EXT         = '.so'
2609            SLIBFLAGS      = '-shared'
2610        elif sysname == 'OpenBSD':
2611            CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
2612            OS_DEFINES     = '-D_OPENBSD_'
2613            SO_EXT         = '.so'
2614            SLIBFLAGS      = '-shared'
2615        elif sysname  == 'SunOS':
2616            CXXFLAGS       = '%s -D_SUNOS_' % CXXFLAGS
2617            OS_DEFINES     = '-D_SUNOS_'
2618            SO_EXT         = '.so'
2619            SLIBFLAGS      = '-shared'
2620            SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
2621        elif sysname.startswith('CYGWIN'):
2622            CXXFLAGS       = '%s -D_CYGWIN' % CXXFLAGS
2623            OS_DEFINES     = '-D_CYGWIN'
2624            SO_EXT         = '.dll'
2625            SLIBFLAGS      = '-shared'
2626        elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
2627            CXXFLAGS       = '%s -D_MINGW' % CXXFLAGS
2628            OS_DEFINES     = '-D_MINGW'
2629            SO_EXT         = '.dll'
2630            SLIBFLAGS      = '-shared'
2631            EXE_EXT        = '.exe'
2632            LIB_EXT        = '.lib'
2633        else:
2634            raise MKException('Unsupported platform: %s' % sysname)
2635        if is64():
2636            if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
2637                CXXFLAGS     = '%s -fPIC' % CXXFLAGS
2638            if sysname == 'Linux':
2639                CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
2640        elif not LINUX_X64:
2641            CXXFLAGS     = '%s -m32' % CXXFLAGS
2642            LDFLAGS      = '%s -m32' % LDFLAGS
2643            SLIBFLAGS    = '%s -m32' % SLIBFLAGS
2644        if TRACE or DEBUG_MODE:
2645            CPPFLAGS     = '%s -D_TRACE' % CPPFLAGS
2646        if is_cygwin_mingw():
2647            # when cross-compiling with MinGW, we need to statically link its standard libraries
2648            # and to make it create an import library.
2649            SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS
2650            LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
2651        if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
2652            CXXFLAGS = '%s -fpic' % CXXFLAGS
2653
2654        config.write('PREFIX=%s\n' % PREFIX)
2655        config.write('CC=%s\n' % CC)
2656        config.write('CXX=%s\n' % CXX)
2657        config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
2658        config.write('CFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS.replace('-std=c++17', '')))
2659        config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
2660        config.write('CXX_OUT_FLAG=-o \n')
2661        config.write('C_OUT_FLAG=-o \n')
2662        config.write('OBJ_EXT=.o\n')
2663        config.write('LIB_EXT=%s\n' % LIB_EXT)
2664        config.write('AR=%s\n' % AR)
2665        config.write('AR_FLAGS=rcs\n')
2666        config.write('AR_OUTFLAG=\n')
2667        config.write('EXE_EXT=%s\n' % EXE_EXT)
2668        config.write('LINK=%s\n' % CXX)
2669        config.write('LINK_FLAGS=\n')
2670        config.write('LINK_OUT_FLAG=-o \n')
2671        if is_linux() and (build_static_lib() or build_static_bin()):
2672            config.write('LINK_EXTRA_FLAGS=-Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive %s\n' % LDFLAGS)
2673        else:
2674            config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
2675        config.write('SO_EXT=%s\n' % SO_EXT)
2676        config.write('SLINK=%s\n' % CXX)
2677        config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
2678        config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
2679        config.write('SLINK_OUT_FLAG=-o \n')
2680        config.write('OS_DEFINES=%s\n' % OS_DEFINES)
2681        if is_verbose():
2682            print('Host platform:  %s' % sysname)
2683            print('C++ Compiler:   %s' % CXX)
2684            print('C Compiler  :   %s' % CC)
2685            if is_cygwin_mingw():
2686                print('MinGW32 cross:  %s' % (is_cygwin_mingw()))
2687            print('Archive Tool:   %s' % AR)
2688            print('Arithmetic:     %s' % ARITH)
2689            print('Prefix:         %s' % PREFIX)
2690            print('64-bit:         %s' % is64())
2691            print('FP math:        %s' % FPMATH)
2692            print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
2693            if GPROF:
2694                print('gprof:          enabled')
2695            print('Python version: %s' % distutils.sysconfig.get_python_version())
2696            if is_java_enabled():
2697                print('JNI Bindings:   %s' % JNI_HOME)
2698                print('Java Compiler:  %s' % JAVAC)
2699            if is_ml_enabled():
2700                print('OCaml Compiler: %s' % OCAMLC)
2701                print('OCaml Find tool: %s' % OCAMLFIND)
2702                print('OCaml Native:   %s' % OCAMLOPT)
2703                print('OCaml Library:  %s' % OCAML_LIB)
2704            if is_dotnet_core_enabled():
2705                print('C# Compiler:    %s' % DOTNET)
2706
2707    config.close()
2708
2709def mk_install(out):
2710    out.write('install: ')
2711    for c in get_components():
2712        c.mk_install_deps(out)
2713        out.write(' ')
2714    out.write('\n')
2715    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
2716    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
2717    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
2718    for c in get_components():
2719        c.mk_install(out)
2720    out.write('\t@echo Z3 was successfully installed.\n')
2721    out.write('\n')
2722
2723def mk_uninstall(out):
2724    out.write('uninstall:\n')
2725    for c in get_components():
2726        c.mk_uninstall(out)
2727    out.write('\t@echo Z3 was successfully uninstalled.\n')
2728    out.write('\n')
2729
2730# Generate the Z3 makefile
2731def mk_makefile():
2732    mk_dir(BUILD_DIR)
2733    mk_config()
2734    if VERBOSE:
2735        print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile'))
2736    out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w')
2737    out.write('# Automatically generated file.\n')
2738    out.write('include config.mk\n')
2739    # Generate :all rule
2740    out.write('all:')
2741    for c in get_components():
2742        if c.main_component():
2743            out.write(' %s' % c.name)
2744    out.write('\n\t@echo Z3 was successfully built.\n')
2745    out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python'))
2746    pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
2747    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable and the \'%s\' directory is added to the %s environment variable.\"\n" % (os.path.join(BUILD_DIR, 'python'), BUILD_DIR, pathvar))
2748    if not IS_WINDOWS:
2749        out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
2750        out.write('\t@echo "    sudo make install"\n\n')
2751        # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
2752        # out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
2753    # Generate :examples rule
2754    out.write('examples:')
2755    for c in get_components():
2756        if c.is_example():
2757            out.write(' _ex_%s' % c.name)
2758    out.write('\n\t@echo Z3 examples were successfully built.\n')
2759    # Generate components
2760    for c in get_components():
2761        c.mk_makefile(out)
2762    # Generate install/uninstall rules if not WINDOWS
2763    if not IS_WINDOWS:
2764        mk_install(out)
2765        mk_uninstall(out)
2766    for c in get_components():
2767        c.final_info()
2768    out.close()
2769    # Finalize
2770    if VERBOSE:
2771        print("Makefile was successfully generated.")
2772        if DEBUG_MODE:
2773            print("  compilation mode: Debug")
2774        else:
2775            print("  compilation mode: Release")
2776        if IS_WINDOWS:
2777            if VS_X64:
2778                print("  platform: x64\n")
2779                print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
2780            elif VS_ARM:
2781                print("  platform: ARM\n")
2782                print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
2783            else:
2784                print("  platform: x86")
2785                print("To build Z3, open a [Visual Studio Command Prompt], then")
2786            print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR))
2787            print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
2788        else:
2789            print("Type 'cd %s; make' to build Z3" % BUILD_DIR)
2790
2791# Generate automatically generated source code
2792def mk_auto_src():
2793    if not ONLY_MAKEFILES:
2794        exec_pyg_scripts()
2795        mk_pat_db()
2796        mk_all_install_tactic_cpps()
2797        mk_all_mem_initializer_cpps()
2798        mk_all_gparams_register_modules()
2799
2800
2801def _execfile(file, globals=globals(), locals=locals()):
2802    if sys.version < "2.7":
2803        execfile(file, globals, locals)
2804    else:
2805        with open(file, "r") as fh:
2806            exec(fh.read()+"\n", globals, locals)
2807
2808# Execute python auxiliary scripts that generate extra code for Z3.
2809def exec_pyg_scripts():
2810    for root, dirs, files in os.walk('src'):
2811        for f in files:
2812            if f.endswith('.pyg'):
2813                script = os.path.join(root, f)
2814                generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root)
2815                if is_verbose():
2816                    print("Generated '{}'".format(generated_file))
2817
2818# TODO: delete after src/ast/pattern/expr_pattern_match
2819# database.smt ==> database.h
2820def mk_pat_db():
2821    c = get_component(PATTERN_COMPONENT)
2822    fin  = os.path.join(c.src_dir, 'database.smt2')
2823    fout = os.path.join(c.src_dir, 'database.h')
2824    mk_genfile_common.mk_pat_db_internal(fin, fout)
2825    if VERBOSE:
2826        print("Generated '{}'".format(fout))
2827
2828# Update version numbers
2829def update_version():
2830    major = VER_MAJOR
2831    minor = VER_MINOR
2832    build = VER_BUILD
2833    revision = VER_TWEAK
2834    if major is None or minor is None or build is None or revision is None:
2835        raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
2836    if not ONLY_MAKEFILES:
2837        mk_version_dot_h(major, minor, build, revision)
2838        mk_all_assembly_infos(major, minor, build, revision)
2839        mk_def_files()
2840
2841def get_full_version_string(major, minor, build, revision):
2842    global GIT_HASH, GIT_DESCRIBE
2843    res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
2844    if GIT_HASH:
2845        res += " " + GIT_HASH
2846    if GIT_DESCRIBE:
2847        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
2848        res += " " + branch + " " + check_output(['git', 'describe'])
2849    return '"' + res + '"'
2850
2851# Update files with the version number
2852def mk_version_dot_h(major, minor, build, revision):
2853    c = get_component(UTIL_COMPONENT)
2854    version_template = os.path.join(c.src_dir, 'z3_version.h.in')
2855    version_header_output = os.path.join(c.src_dir, 'z3_version.h')
2856    # Note the substitution names are what is used by the CMake
2857    # builds system. If you change these you should change them
2858    # in the CMake build too
2859    configure_file(version_template, version_header_output,
2860        { 'Z3_VERSION_MAJOR': str(major),
2861          'Z3_VERSION_MINOR': str(minor),
2862          'Z3_VERSION_PATCH': str(build),
2863          'Z3_VERSION_TWEAK': str(revision),
2864          'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision)
2865        }
2866    )
2867    if VERBOSE:
2868        print("Generated '%s'" % version_header_output)
2869
2870# Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template
2871def mk_all_assembly_infos(major, minor, build, revision):
2872    for c in get_components():
2873        if c.has_assembly_info():
2874            c.make_assembly_info(major, minor, build, revision)
2875
2876def get_header_files_for_components(component_src_dirs):
2877    assert isinstance(component_src_dirs, list)
2878    h_files_full_path = []
2879    for component_src_dir in sorted(component_src_dirs):
2880        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
2881        h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
2882        h_files_full_path.extend(h_files)
2883    return h_files_full_path
2884
2885def mk_install_tactic_cpp(cnames, path):
2886    component_src_dirs = []
2887    for cname in cnames:
2888        print("Component %s" % cname)
2889        c = get_component(cname)
2890        component_src_dirs.append(c.src_dir)
2891    h_files_full_path = get_header_files_for_components(component_src_dirs)
2892    generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(h_files_full_path, path)
2893    if VERBOSE:
2894        print("Generated '{}'".format(generated_file))
2895
2896def mk_all_install_tactic_cpps():
2897    if not ONLY_MAKEFILES:
2898        for c in get_components():
2899            if c.require_install_tactics():
2900                cnames = []
2901                cnames.extend(c.deps)
2902                cnames.append(c.name)
2903                mk_install_tactic_cpp(cnames, c.src_dir)
2904
2905def mk_mem_initializer_cpp(cnames, path):
2906    component_src_dirs = []
2907    for cname in cnames:
2908        c = get_component(cname)
2909        component_src_dirs.append(c.src_dir)
2910    h_files_full_path = get_header_files_for_components(component_src_dirs)
2911    generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path)
2912    if VERBOSE:
2913        print("Generated '{}'".format(generated_file))
2914
2915def mk_all_mem_initializer_cpps():
2916    if not ONLY_MAKEFILES:
2917        for c in get_components():
2918            if c.require_mem_initializer():
2919                cnames = []
2920                cnames.extend(c.deps)
2921                cnames.append(c.name)
2922                mk_mem_initializer_cpp(cnames, c.src_dir)
2923
2924def mk_gparams_register_modules(cnames, path):
2925    component_src_dirs = []
2926    for cname in cnames:
2927        c = get_component(cname)
2928        component_src_dirs.append(c.src_dir)
2929    h_files_full_path = get_header_files_for_components(component_src_dirs)
2930    generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path)
2931    if VERBOSE:
2932        print("Generated '{}'".format(generated_file))
2933
2934def mk_all_gparams_register_modules():
2935    if not ONLY_MAKEFILES:
2936        for c in get_components():
2937            if c.require_mem_initializer():
2938                cnames = []
2939                cnames.extend(c.deps)
2940                cnames.append(c.name)
2941                mk_gparams_register_modules(cnames, c.src_dir)
2942
2943# Generate a .def based on the files at c.export_files slot.
2944def mk_def_file(c):
2945    defname = '%s.def' % os.path.join(c.src_dir, c.name)
2946    dll_name = c.dll_name
2947    export_header_files = []
2948    for dot_h in c.export_files:
2949        dot_h_c = c.find_file(dot_h, c.name)
2950        api = os.path.join(dot_h_c.src_dir, dot_h)
2951        export_header_files.append(api)
2952    mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files)
2953    if VERBOSE:
2954        print("Generated '%s'" % defname)
2955
2956def mk_def_files():
2957    if not ONLY_MAKEFILES:
2958        for c in get_components():
2959            if c.require_def_file():
2960                mk_def_file(c)
2961
2962def cp_z3py_to_build():
2963    mk_dir(BUILD_DIR)
2964    mk_dir(os.path.join(BUILD_DIR, 'python'))
2965    z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3')
2966    z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3')
2967
2968    # Erase existing .pyc files
2969    for root, dirs, files in os.walk(Z3PY_SRC_DIR):
2970        for f in files:
2971            if f.endswith('.pyc'):
2972                rmf(os.path.join(root, f))
2973    # Compile Z3Py files
2974    if compileall.compile_dir(z3py_src, force=1) != 1:
2975        raise MKException("failed to compile Z3Py sources")
2976    if is_verbose:
2977        print("Generated python bytecode")
2978    # Copy sources to build
2979    mk_dir(z3py_dest)
2980    for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)):
2981        shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py))
2982        if is_verbose():
2983            print("Copied '%s'" % py)
2984    # Python 2.x support
2985    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)):
2986        shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc))
2987        if is_verbose():
2988            print("Copied '%s'" % pyc)
2989    # Python 3.x support
2990    src_pycache = os.path.join(z3py_src, '__pycache__')
2991    target_pycache = os.path.join(z3py_dest, '__pycache__')
2992    if os.path.exists(src_pycache):
2993        for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)):
2994            mk_dir(target_pycache)
2995            shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
2996            if is_verbose():
2997                print("Copied '%s'" % pyc)
2998    # Copy z3test.py
2999    shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py'))
3000
3001def mk_bindings(api_files):
3002    if not ONLY_MAKEFILES:
3003        mk_z3consts_py(api_files)
3004        new_api_files = []
3005        api = get_component(API_COMPONENT)
3006        for api_file in api_files:
3007            api_file_path = api.find_file(api_file, api.name)
3008            new_api_files.append(os.path.join(api_file_path.src_dir, api_file))
3009        g = globals()
3010        g["API_FILES"] = new_api_files
3011        if is_java_enabled():
3012            check_java()
3013            mk_z3consts_java(api_files)
3014        # Generate some of the bindings and "api" module files
3015        import update_api
3016        dotnet_output_dir = None
3017        if is_dotnet_core_enabled():
3018          dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet')
3019          mk_dir(dotnet_output_dir)
3020        java_output_dir = None
3021        java_package_name = None
3022        if is_java_enabled():
3023          java_output_dir = get_component('java').src_dir
3024          java_package_name = get_component('java').package_name
3025        ml_output_dir = None
3026        if is_ml_enabled():
3027          ml_output_dir = get_component('ml').src_dir
3028        if is_js_enabled():
3029          set_z3js_dir("api/js")
3030          js_output_dir = get_component('js').src_dir
3031        # Get the update_api module to do the work for us
3032        update_api.generate_files(api_files=new_api_files,
3033          api_output_dir=get_component('api').src_dir,
3034          z3py_output_dir=get_z3py_dir(),
3035          dotnet_output_dir=dotnet_output_dir,
3036          java_output_dir=java_output_dir,
3037          java_package_name=java_package_name,
3038          js_output_dir=get_z3js_dir(),
3039          ml_output_dir=ml_output_dir,
3040          ml_src_dir=ml_output_dir
3041        )
3042        cp_z3py_to_build()
3043        if is_ml_enabled():
3044            check_ml()
3045            mk_z3consts_ml(api_files)
3046        if  is_dotnet_core_enabled():
3047            check_dotnet_core()
3048            mk_z3consts_dotnet(api_files, dotnet_output_dir)
3049
3050# Extract enumeration types from API files, and add python definitions.
3051def mk_z3consts_py(api_files):
3052    if Z3PY_SRC_DIR is None:
3053        raise MKException("You must invoke set_z3py_dir(path):")
3054    full_path_api_files = []
3055    api_dll = get_component(Z3_DLL_COMPONENT)
3056    for api_file in api_files:
3057        api_file_c = api_dll.find_file(api_file, api_dll.name)
3058        api_file   = os.path.join(api_file_c.src_dir, api_file)
3059        full_path_api_files.append(api_file)
3060    generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
3061    if VERBOSE:
3062        print("Generated '{}".format(generated_file))
3063
3064# Extract enumeration types from z3_api.h, and add .Net definitions
3065def mk_z3consts_dotnet(api_files, output_dir):
3066    dotnet = get_component(DOTNET_COMPONENT)
3067    if not dotnet:
3068       dotnet = get_component(DOTNET_CORE_COMPONENT)
3069    full_path_api_files = []
3070    for api_file in api_files:
3071        api_file_c = dotnet.find_file(api_file, dotnet.name)
3072        api_file   = os.path.join(api_file_c.src_dir, api_file)
3073        full_path_api_files.append(api_file)
3074    generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir)
3075    if VERBOSE:
3076        print("Generated '{}".format(generated_file))
3077
3078# Extract enumeration types from z3_api.h, and add Java definitions
3079def mk_z3consts_java(api_files):
3080    java = get_component(JAVA_COMPONENT)
3081    full_path_api_files = []
3082    for api_file in api_files:
3083        api_file_c = java.find_file(api_file, java.name)
3084        api_file   = os.path.join(api_file_c.src_dir, api_file)
3085        full_path_api_files.append(api_file)
3086    generated_files = mk_genfile_common.mk_z3consts_java_internal(
3087        full_path_api_files,
3088        java.package_name,
3089        java.src_dir)
3090    if VERBOSE:
3091        for generated_file in generated_files:
3092            print("Generated '{}'".format(generated_file))
3093
3094# Extract enumeration types from z3_api.h, and add ML definitions
3095def mk_z3consts_ml(api_files):
3096    ml = get_component(ML_COMPONENT)
3097    full_path_api_files = []
3098    for api_file in api_files:
3099        api_file_c = ml.find_file(api_file, ml.name)
3100        api_file   = os.path.join(api_file_c.src_dir, api_file)
3101        full_path_api_files.append(api_file)
3102    generated_file = mk_genfile_common.mk_z3consts_ml_internal(
3103        full_path_api_files,
3104        ml.src_dir)
3105    if VERBOSE:
3106        print ('Generated "%s"' % generated_file)
3107
3108def mk_gui_str(id):
3109    return '4D2F40D8-E5F9-473B-B548-%012d' % id
3110
3111def get_platform_toolset_str():
3112    default = 'v110';
3113    vstr = check_output(['msbuild', '/ver'])
3114    lines = vstr.split('\n')
3115    lline = lines[-1]
3116    tokens = lline.split('.')
3117    if len(tokens) < 2:
3118        return default
3119    else:
3120        if tokens[0] == "15":
3121            # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
3122            return "v141"
3123        else:
3124            return 'v' + tokens[0] + tokens[1]
3125
3126def mk_vs_proj_property_groups(f, name, target_ext, type):
3127    f.write('  <ItemGroup Label="ProjectConfigurations">\n')
3128    f.write('    <ProjectConfiguration Include="Debug|Win32">\n')
3129    f.write('      <Configuration>Debug</Configuration>\n')
3130    f.write('      <Platform>Win32</Platform>\n')
3131    f.write('    </ProjectConfiguration>\n')
3132    f.write('    <ProjectConfiguration Include="Release|Win32">\n')
3133    f.write('      <Configuration>Release</Configuration>\n')
3134    f.write('      <Platform>Win32</Platform>\n')
3135    f.write('    </ProjectConfiguration>\n')
3136    f.write('  </ItemGroup>\n')
3137    f.write('  <PropertyGroup Label="Globals">\n')
3138    f.write('    <ProjectGuid>{%s}</ProjectGuid>\n' % mk_gui_str(0))
3139    f.write('    <ProjectName>%s</ProjectName>\n' % name)
3140    f.write('    <Keyword>Win32Proj</Keyword>\n')
3141    f.write('    <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
3142    f.write('  </PropertyGroup>\n')
3143    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
3144    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
3145    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
3146    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
3147    f.write('    <UseOfMfc>false</UseOfMfc>\n')
3148    f.write('  </PropertyGroup>\n')
3149    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n')
3150    f.write('    <ConfigurationType>%s</ConfigurationType>\n' % type)
3151    f.write('    <CharacterSet>Unicode</CharacterSet>\n')
3152    f.write('    <UseOfMfc>false</UseOfMfc>\n')
3153    f.write('  </PropertyGroup>\n')
3154    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
3155    f.write('  <ImportGroup Label="ExtensionSettings" />\n')
3156    f.write('   <ImportGroup Label="PropertySheets">\n')
3157    f.write('    <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
3158    f.write('  <PropertyGroup Label="UserMacros" />\n')
3159    f.write('  <PropertyGroup>\n')
3160    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
3161    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
3162    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
3163    f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
3164    f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
3165    f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
3166    f.write('  </PropertyGroup>\n')
3167    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3168    f.write('        <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
3169    f.write('  </PropertyGroup>\n')
3170    f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3171    f.write('    <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
3172    f.write('  </PropertyGroup>\n')
3173
3174
3175def mk_vs_proj_cl_compile(f, name, components, debug):
3176    f.write('    <ClCompile>\n')
3177    f.write('      <Optimization>Disabled</Optimization>\n')
3178    if debug:
3179        f.write('      <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
3180    else:
3181        f.write('      <PreprocessorDefinitions>WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
3182    if VS_PAR:
3183        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
3184        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
3185    else:
3186        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
3187    f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
3188    f.write('      <WarningLevel>Level3</WarningLevel>\n')
3189    if debug:
3190        f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
3191    else:
3192        f.write('      <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')
3193    f.write('      <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
3194    f.write('      <AdditionalIncludeDirectories>')
3195    deps = find_all_deps(name, components)
3196    first = True
3197    for dep in deps:
3198        if first:
3199            first = False
3200        else:
3201            f.write(';')
3202        f.write(get_component(dep).to_src_dir)
3203    f.write(';%s\n' % os.path.join(REV_BUILD_DIR, SRC_DIR))
3204    f.write('</AdditionalIncludeDirectories>\n')
3205    f.write('    </ClCompile>\n')
3206
3207def mk_vs_proj_dep_groups(f, name, components):
3208    f.write('  <ItemGroup>\n')
3209    deps = find_all_deps(name, components)
3210    for dep in deps:
3211        dep = get_component(dep)
3212        for cpp in filter(lambda f: f.endswith('.cpp'), os.listdir(dep.src_dir)):
3213            f.write('    <ClCompile Include="%s" />\n' % os.path.join(dep.to_src_dir, cpp))
3214    f.write('  </ItemGroup>\n')
3215
3216def mk_vs_proj_link_exe(f, name, debug):
3217    f.write('    <Link>\n')
3218    f.write('      <OutputFile>$(OutDir)%s.exe</OutputFile>\n' % name)
3219    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
3220    f.write('      <SubSystem>Console</SubSystem>\n')
3221    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
3222    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
3223    f.write('      <DataExecutionPrevention/>\n')
3224    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
3225    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
3226    f.write('      <AdditionalDependencies>psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)</AdditionalDependencies>\n')
3227    f.write('    </Link>\n')
3228
3229def mk_vs_proj(name, components):
3230    if not VS_PROJ:
3231        return
3232    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
3233    modes=['Debug', 'Release']
3234    PLATFORMS=['Win32']
3235    f = open(proj_name, 'w')
3236    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
3237    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
3238    mk_vs_proj_property_groups(f, name, 'exe', 'Application')
3239    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3240    mk_vs_proj_cl_compile(f, name, components, debug=True)
3241    mk_vs_proj_link_exe(f, name, debug=True)
3242    f.write('  </ItemDefinitionGroup>\n')
3243    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3244    mk_vs_proj_cl_compile(f, name, components, debug=False)
3245    mk_vs_proj_link_exe(f, name, debug=False)
3246    f.write('  </ItemDefinitionGroup>\n')
3247    mk_vs_proj_dep_groups(f, name, components)
3248    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
3249    f.write('  <ImportGroup Label="ExtensionTargets">\n')
3250    f.write('  </ImportGroup>\n')
3251    f.write('</Project>\n')
3252    f.close()
3253    if is_verbose():
3254        print("Generated '%s'" % proj_name)
3255
3256def mk_vs_proj_link_dll(f, name, debug):
3257    f.write('    <Link>\n')
3258    f.write('      <OutputFile>$(OutDir)%s.dll</OutputFile>\n' % name)
3259    f.write('      <GenerateDebugInformation>true</GenerateDebugInformation>\n')
3260    f.write('      <SubSystem>Console</SubSystem>\n')
3261    f.write('      <StackReserveSize>8388608</StackReserveSize>\n')
3262    f.write('      <RandomizedBaseAddress>false</RandomizedBaseAddress>\n')
3263    f.write('      <DataExecutionPrevention/>\n')
3264    f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
3265    f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
3266    f.write('      <AdditionalDependencies>psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)</AdditionalDependencies>\n')
3267    f.write('      <ModuleDefinitionFile>%s</ModuleDefinitionFile>' % os.path.join(get_component('api_dll').to_src_dir, 'api_dll.def'))
3268    f.write('    </Link>\n')
3269
3270def mk_vs_proj_dll(name, components):
3271    if not VS_PROJ:
3272        return
3273    proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name)
3274    modes=['Debug', 'Release']
3275    PLATFORMS=['Win32']
3276    f = open(proj_name, 'w')
3277    f.write('<?xml version="1.0" encoding="utf-8"?>\n')
3278    f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
3279    mk_vs_proj_property_groups(f, name, 'dll', 'DynamicLibrary')
3280    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
3281    mk_vs_proj_cl_compile(f, name, components, debug=True)
3282    mk_vs_proj_link_dll(f, name, debug=True)
3283    f.write('  </ItemDefinitionGroup>\n')
3284    f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
3285    mk_vs_proj_cl_compile(f, name, components, debug=False)
3286    mk_vs_proj_link_dll(f, name, debug=False)
3287    f.write('  </ItemDefinitionGroup>\n')
3288    mk_vs_proj_dep_groups(f, name, components)
3289    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
3290    f.write('  <ImportGroup Label="ExtensionTargets">\n')
3291    f.write('  </ImportGroup>\n')
3292    f.write('</Project>\n')
3293    f.close()
3294    if is_verbose():
3295        print("Generated '%s'" % proj_name)
3296
3297def mk_win_dist(build_path, dist_path):
3298    for c in get_components():
3299        c.mk_win_dist(build_path, dist_path)
3300
3301def mk_unix_dist(build_path, dist_path):
3302    for c in get_components():
3303        c.mk_unix_dist(build_path, dist_path)
3304    # Add Z3Py to bin directory
3305    for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
3306        shutil.copy(os.path.join(build_path, pyc),
3307                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
3308
3309class MakeRuleCmd(object):
3310    """
3311        These class methods provide a convenient way to emit frequently
3312        needed commands used in Makefile rules
3313        Note that several of the method are meant for use during ``make
3314        install`` and ``make uninstall``.  These methods correctly use
3315        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable
3316        to writing commands manually which can be error prone.
3317    """
3318    @classmethod
3319    def install_root(cls):
3320        """
3321            Returns a string that will expand to the
3322            install location when used in a makefile rule.
3323        """
3324        # Note: DESTDIR is to support staged installs
3325        return "$(DESTDIR)$(PREFIX)/"
3326
3327    @classmethod
3328    def _is_str(cls, obj):
3329        if sys.version_info.major > 2:
3330            # Python 3 or newer. Strings are always unicode and of type str
3331            return isinstance(obj, str)
3332        else:
3333            # Python 2. Has byte-string and unicode representation, allow both
3334            return isinstance(obj, str) or isinstance(obj, unicode)
3335
3336    @classmethod
3337    def _install_root(cls, path, in_prefix, out, is_install=True):
3338        if not in_prefix:
3339            # The Python bindings on OSX are sometimes not installed inside the prefix.
3340            install_root = "$(DESTDIR)"
3341            action_string = 'install' if is_install else 'uninstall'
3342            cls.write_cmd(out, 'echo "WARNING: {}ing files/directories ({}) that are not in the install prefix ($(PREFIX))."'.format(
3343                    action_string, path))
3344            #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
3345            #        action_string, 'to' if is_install else 'from', path, PREFIX))
3346        else:
3347            # assert not os.path.isabs(path)
3348            install_root = cls.install_root()
3349        return install_root
3350
3351    @classmethod
3352    def install_files(cls, out, src_pattern, dest, in_prefix=True):
3353        assert len(dest) > 0
3354        assert cls._is_str(src_pattern)
3355        assert not ' ' in src_pattern
3356        assert cls._is_str(dest)
3357        assert not ' ' in dest
3358        assert not os.path.isabs(src_pattern)
3359        install_root = cls._install_root(dest, in_prefix, out)
3360
3361        cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
3362            src_pattern=src_pattern,
3363            install_root=install_root,
3364            dest=dest))
3365
3366    @classmethod
3367    def remove_installed_files(cls, out, pattern, in_prefix=True):
3368        assert len(pattern) > 0
3369        assert cls._is_str(pattern)
3370        assert not ' ' in pattern
3371        install_root = cls._install_root(pattern, in_prefix, out, is_install=False)
3372
3373        cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
3374            install_root=install_root,
3375            pattern=pattern))
3376
3377    @classmethod
3378    def make_install_directory(cls, out, dir, in_prefix=True):
3379        assert len(dir) > 0
3380        assert cls._is_str(dir)
3381        assert not ' ' in dir
3382        install_root = cls._install_root(dir, in_prefix, out)
3383
3384        if is_windows():
3385            cls.write_cmd(out, "IF NOT EXIST {dir} (mkdir {dir})".format(
3386                install_root=install_root,
3387                dir=dir))
3388        else:
3389            cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
3390                install_root=install_root,
3391                dir=dir))
3392
3393    @classmethod
3394    def _is_path_prefix_of(cls, temp_path, target_as_abs):
3395        """
3396            Returns True iff ``temp_path`` is a path prefix
3397            of ``target_as_abs``
3398        """
3399        assert cls._is_str(temp_path)
3400        assert cls._is_str(target_as_abs)
3401        assert len(temp_path) > 0
3402        assert len(target_as_abs) > 0
3403        assert os.path.isabs(temp_path)
3404        assert os.path.isabs(target_as_abs)
3405
3406        # Need to stick extra slash in front otherwise we might think that
3407        # ``/lib`` is a prefix of ``/lib64``.  Of course if ``temp_path ==
3408        # '/'`` then we shouldn't else we would check if ``//`` (rather than
3409        # ``/``) is a prefix of ``/lib64``, which would fail.
3410        if len(temp_path) > 1:
3411            temp_path += os.sep
3412        return target_as_abs.startswith(temp_path)
3413
3414    @classmethod
3415    def create_relative_symbolic_link(cls, out, target, link_name):
3416        assert cls._is_str(target)
3417        assert cls._is_str(link_name)
3418        assert len(target) > 0
3419        assert len(link_name) > 0
3420        assert not os.path.isabs(target)
3421        assert not os.path.isabs(link_name)
3422
3423        # We can't test to see if link_name is a file or directory
3424        # because it may not exist yet. Instead follow the convention
3425        # that if there is a leading slash target is a directory otherwise
3426        # it's a file
3427        if link_name[-1] != '/':
3428            # link_name is a file
3429            temp_path = os.path.dirname(link_name)
3430        else:
3431            # link_name is a directory
3432            temp_path = link_name[:-1]
3433        temp_path = '/' + temp_path
3434        relative_path = ""
3435        targetAsAbs = '/' + target
3436        assert os.path.isabs(targetAsAbs)
3437        assert os.path.isabs(temp_path)
3438        # Keep walking up the directory tree until temp_path
3439        # is a prefix of targetAsAbs
3440        while not cls._is_path_prefix_of(temp_path, targetAsAbs):
3441            assert temp_path != '/'
3442            temp_path = os.path.dirname(temp_path)
3443            relative_path += '../'
3444
3445        # Now get the path from the common prefix directory to the target
3446        target_from_prefix = targetAsAbs[len(temp_path):]
3447        relative_path += target_from_prefix
3448        # Remove any double slashes
3449        relative_path = relative_path.replace('//','/')
3450        cls.create_symbolic_link(out, relative_path, link_name)
3451
3452    @classmethod
3453    def create_symbolic_link(cls, out, target, link_name):
3454        assert cls._is_str(target)
3455        assert cls._is_str(link_name)
3456        assert not os.path.isabs(target)
3457
3458        cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
3459            target=target,
3460            install_root=cls.install_root(),
3461            link_name=link_name))
3462
3463    # TODO: Refactor all of the build system to emit commands using this
3464    # helper to simplify code. This will also let us replace ``@`` with
3465    # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
3466    # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
3467    # would be very helpful for debugging.
3468    @classmethod
3469    def write_cmd(cls, out, line):
3470        out.write("\t@{}\n".format(line))
3471
3472def strip_path_prefix(path, prefix):
3473    if path.startswith(prefix):
3474        stripped_path = path[len(prefix):]
3475        stripped_path.replace('//','/')
3476        if stripped_path[0] == '/':
3477            stripped_path = stripped_path[1:]
3478        assert not os.path.isabs(stripped_path)
3479        return stripped_path
3480    else:
3481        return path
3482
3483def configure_file(template_file_path, output_file_path, substitutions):
3484    """
3485        Read a template file ``template_file_path``, perform substitutions
3486        found in the ``substitutions`` dictionary and write the result to
3487        the output file ``output_file_path``.
3488        The template file should contain zero or more template strings of the
3489        form ``@NAME@``.
3490        The substitutions dictionary maps old strings (without the ``@``
3491        symbols) to their replacements.
3492    """
3493    assert isinstance(template_file_path, str)
3494    assert isinstance(output_file_path, str)
3495    assert isinstance(substitutions, dict)
3496    assert len(template_file_path) > 0
3497    assert len(output_file_path) > 0
3498    print("Generating {} from {}".format(output_file_path, template_file_path))
3499
3500    if not os.path.exists(template_file_path):
3501        raise MKException('Could not find template file "{}"'.format(template_file_path))
3502
3503    # Read whole template file into string
3504    template_string = None
3505    with open(template_file_path, 'r') as f:
3506        template_string = f.read()
3507
3508    # Do replacements
3509    for (old_string, replacement) in substitutions.items():
3510        template_string = template_string.replace('@{}@'.format(old_string), replacement)
3511
3512    # Write the string to the file
3513    with open(output_file_path, 'w') as f:
3514        f.write(template_string)
3515
3516if __name__ == '__main__':
3517    import doctest
3518    doctest.testmod()
3519