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