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_DRAGONFLY=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_dragonfly(): 150 return IS_DRAGONFLY 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] == 'DragonFly': 603 IS_DRAGONFLY=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.append(root_file_name) 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): 978 full_fname = os.path.join(self.src_dir, fname) 979 if os.path.exists(full_fname): 980 return self 981 for dep in self.deps: 982 c_dep = get_component(dep) 983 full_fname = os.path.join(c_dep.src_dir, fname) 984 if os.path.exists(full_fname): 985 return c_dep 986 raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name)) 987 988 # Display all dependencies of file basename located in the given component directory. 989 # The result is displayed at out 990 def add_cpp_h_deps(self, out, basename): 991 includes = extract_c_includes(os.path.join(self.src_dir, basename)) 992 out.write(os.path.join(self.to_src_dir, basename)) 993 for include in includes: 994 owner = self.find_file(include, basename) 995 out.write(' %s.node' % os.path.join(owner.build_dir, include)) 996 997 # Add a rule for each #include directive in the file basename located at the current component. 998 def add_rule_for_each_include(self, out, basename): 999 fullname = os.path.join(self.src_dir, basename) 1000 includes = extract_c_includes(fullname) 1001 for include in includes: 1002 owner = self.find_file(include, fullname) 1003 owner.add_h_rule(out, include) 1004 1005 # Display a Makefile rule for an include file located in the given component directory. 1006 # 'include' is something of the form: ast.h, polynomial.h 1007 # The rule displayed at out is of the form 1008 # ast/ast_pp.h.node : ../src/util/ast_pp.h util/util.h.node ast/ast.h.node 1009 # @echo "done" > ast/ast_pp.h.node 1010 def add_h_rule(self, out, include): 1011 include_src_path = os.path.join(self.to_src_dir, include) 1012 if include_src_path in _Processed_Headers: 1013 return 1014 _Processed_Headers.add(include_src_path) 1015 self.add_rule_for_each_include(out, include) 1016 include_node = '%s.node' % os.path.join(self.build_dir, include) 1017 out.write('%s: ' % include_node) 1018 self.add_cpp_h_deps(out, include) 1019 out.write('\n') 1020 out.write('\t@echo done > %s\n' % include_node) 1021 1022 def add_cpp_rules(self, out, include_defs, cppfile): 1023 self.add_rule_for_each_include(out, cppfile) 1024 objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]) 1025 srcfile = os.path.join(self.to_src_dir, cppfile) 1026 out.write('%s: ' % objfile) 1027 self.add_cpp_h_deps(out, cppfile) 1028 out.write('\n') 1029 if SHOW_CPPS: 1030 out.write('\t@echo %s\n' % os.path.join(self.src_dir, cppfile)) 1031 out.write('\t@$(CXX) $(CXXFLAGS) $(%s) $(CXX_OUT_FLAG)%s %s\n' % (include_defs, objfile, srcfile)) 1032 1033 def mk_makefile(self, out): 1034 include_defs = mk_fresh_name('includes') 1035 out.write('%s =' % include_defs) 1036 for dep in self.deps: 1037 out.write(' -I%s' % get_component(dep).to_src_dir) 1038 out.write(' -I%s' % os.path.join(REV_BUILD_DIR,"src")) 1039 out.write('\n') 1040 mk_dir(os.path.join(BUILD_DIR, self.build_dir)) 1041 if VS_PAR and IS_WINDOWS: 1042 cppfiles = list(get_cpp_files(self.src_dir)) 1043 dependencies = set() 1044 for cppfile in cppfiles: 1045 dependencies.add(os.path.join(self.to_src_dir, cppfile)) 1046 self.add_rule_for_each_include(out, cppfile) 1047 includes = extract_c_includes(os.path.join(self.src_dir, cppfile)) 1048 for include in includes: 1049 owner = self.find_file(include, cppfile) 1050 dependencies.add('%s.node' % os.path.join(owner.build_dir, include)) 1051 for cppfile in cppfiles: 1052 out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0])) 1053 out.write(': ') 1054 for dep in dependencies: 1055 out.write(dep) 1056 out.write(' ') 1057 out.write('\n') 1058 out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs)) 1059 for cppfile in cppfiles: 1060 out.write(' ') 1061 out.write(os.path.join(self.to_src_dir, cppfile)) 1062 out.write('\n') 1063 out.write('\tmove *.obj %s\n' % self.build_dir) 1064 else: 1065 for cppfile in get_cpp_files(self.src_dir): 1066 self.add_cpp_rules(out, include_defs, cppfile) 1067 1068 # Return true if the component should be included in the all: rule 1069 def main_component(self): 1070 return False 1071 1072 # Return true if the component contains an AssemblyInfo.cs file that needs to be updated. 1073 def has_assembly_info(self): 1074 return False 1075 1076 # Return true if the component needs builder to generate an install_tactics.cpp file 1077 def require_install_tactics(self): 1078 return False 1079 1080 # Return true if the component needs a def file 1081 def require_def_file(self): 1082 return False 1083 1084 # Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions. 1085 def require_mem_initializer(self): 1086 return False 1087 1088 def mk_install_deps(self, out): 1089 return 1090 1091 def mk_install(self, out): 1092 return 1093 1094 def mk_uninstall(self, out): 1095 return 1096 1097 def is_example(self): 1098 return False 1099 1100 # Invoked when creating a (windows) distribution package using components at build_path, and 1101 # storing them at dist_path 1102 def mk_win_dist(self, build_path, dist_path): 1103 return 1104 1105 def mk_unix_dist(self, build_path, dist_path): 1106 return 1107 1108 # Used to print warnings or errors after mk_make.py is done, so that they 1109 # are not quite as easy to miss. 1110 def final_info(self): 1111 pass 1112 1113class LibComponent(Component): 1114 def __init__(self, name, path, deps, includes2install): 1115 Component.__init__(self, name, path, deps) 1116 self.includes2install = includes2install 1117 1118 def mk_makefile(self, out): 1119 Component.mk_makefile(self, out) 1120 # generate rule for lib 1121 objs = [] 1122 for cppfile in get_cpp_files(self.src_dir): 1123 objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]) 1124 objs.append(objfile) 1125 1126 libfile = '%s$(LIB_EXT)' % os.path.join(self.build_dir, self.name) 1127 out.write('%s:' % libfile) 1128 for obj in objs: 1129 out.write(' ') 1130 out.write(obj) 1131 out.write('\n') 1132 out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile) 1133 for obj in objs: 1134 out.write(' ') 1135 out.write(obj) 1136 out.write('\n') 1137 out.write('%s: %s\n\n' % (self.name, libfile)) 1138 1139 def mk_install_deps(self, out): 1140 return 1141 1142 def mk_install(self, out): 1143 for include in self.includes2install: 1144 MakeRuleCmd.install_files( 1145 out, 1146 os.path.join(self.to_src_dir, include), 1147 os.path.join(INSTALL_INCLUDE_DIR, include) 1148 ) 1149 1150 def mk_uninstall(self, out): 1151 for include in self.includes2install: 1152 MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include)) 1153 1154 def mk_win_dist(self, build_path, dist_path): 1155 mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR)) 1156 for include in self.includes2install: 1157 shutil.copy(os.path.join(self.src_dir, include), 1158 os.path.join(dist_path, INSTALL_INCLUDE_DIR, include)) 1159 1160 def mk_unix_dist(self, build_path, dist_path): 1161 self.mk_win_dist(build_path, dist_path) 1162 1163# "Library" containing only .h files. This is just a placeholder for includes files to be installed. 1164class HLibComponent(LibComponent): 1165 def __init__(self, name, path, includes2install): 1166 LibComponent.__init__(self, name, path, [], includes2install) 1167 1168 def mk_makefile(self, out): 1169 return 1170 1171# Auxiliary function for sort_components 1172def comp_components(c1, c2): 1173 id1 = get_component(c1).id 1174 id2 = get_component(c2).id 1175 return id2 - id1 1176 1177# Sort components based on (reverse) definition time 1178def sort_components(cnames): 1179 return sorted(cnames, key=lambda c: get_component(c).id, reverse=True) 1180 1181class ExeComponent(Component): 1182 def __init__(self, name, exe_name, path, deps, install): 1183 Component.__init__(self, name, path, deps) 1184 if exe_name is None: 1185 exe_name = name 1186 self.exe_name = exe_name 1187 self.install = install 1188 1189 def mk_makefile(self, out): 1190 Component.mk_makefile(self, out) 1191 # generate rule for exe 1192 1193 exefile = '%s$(EXE_EXT)' % self.exe_name 1194 out.write('%s:' % exefile) 1195 deps = sort_components(self.deps) 1196 objs = [] 1197 for cppfile in get_cpp_files(self.src_dir): 1198 objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]) 1199 objs.append(objfile) 1200 for obj in objs: 1201 out.write(' ') 1202 out.write(obj) 1203 for dep in deps: 1204 c_dep = get_component(dep) 1205 out.write(' ' + c_dep.get_link_name()) 1206 out.write('\n') 1207 extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else '' 1208 out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile)) 1209 for obj in objs: 1210 out.write(' ') 1211 out.write(obj) 1212 for dep in deps: 1213 c_dep = get_component(dep) 1214 out.write(' ' + c_dep.get_link_name()) 1215 out.write(' $(LINK_EXTRA_FLAGS)\n') 1216 out.write('%s: %s\n\n' % (self.name, exefile)) 1217 1218 def require_install_tactics(self): 1219 return ('tactic' in self.deps) and ('cmd_context' in self.deps) 1220 1221 def require_mem_initializer(self): 1222 return True 1223 1224 # All executables (to be installed) are included in the all: rule 1225 def main_component(self): 1226 return self.install 1227 1228 def mk_install_deps(self, out): 1229 if self.install: 1230 exefile = '%s$(EXE_EXT)' % self.exe_name 1231 out.write('%s' % exefile) 1232 1233 def mk_install(self, out): 1234 if self.install: 1235 exefile = '%s$(EXE_EXT)' % self.exe_name 1236 MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile)) 1237 1238 def mk_uninstall(self, out): 1239 if self.install: 1240 exefile = '%s$(EXE_EXT)' % self.exe_name 1241 MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile)) 1242 1243 def mk_win_dist(self, build_path, dist_path): 1244 if self.install: 1245 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1246 shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name), 1247 '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name)) 1248 1249 def mk_unix_dist(self, build_path, dist_path): 1250 if self.install: 1251 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1252 shutil.copy(os.path.join(build_path, self.exe_name), 1253 os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name)) 1254 1255 1256class ExtraExeComponent(ExeComponent): 1257 def __init__(self, name, exe_name, path, deps, install): 1258 ExeComponent.__init__(self, name, exe_name, path, deps, install) 1259 1260 def main_component(self): 1261 return False 1262 1263 def require_mem_initializer(self): 1264 return False 1265 1266def get_so_ext(): 1267 sysname = os.uname()[0] 1268 if sysname == 'Darwin': 1269 return 'dylib' 1270 elif sysname == 'Linux' or sysname == 'GNU' or sysname == 'DragonFly' or sysname == 'NetBSD' or sysname == 'OpenBSD': 1271 return 'so' 1272 elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): 1273 return 'dll' 1274 else: 1275 assert(False) 1276 return 'dll' 1277 1278class DLLComponent(Component): 1279 def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None): 1280 Component.__init__(self, name, path, deps) 1281 if dll_name is None: 1282 dll_name = name 1283 self.dll_name = dll_name 1284 self.export_files = export_files 1285 self.reexports = reexports 1286 self.install = install 1287 self.static = static 1288 self.staging_link = staging_link # link a copy of the shared object into this directory on build 1289 1290 def get_link_name(self): 1291 if self.static: 1292 return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)' 1293 else: 1294 return self.name + '$(SO_EXT)' 1295 1296 def dll_file(self): 1297 """ 1298 Return file name of component suitable for use in a Makefile 1299 """ 1300 return '%s$(SO_EXT)' % self.dll_name 1301 1302 def install_path(self): 1303 """ 1304 Return install location of component (relative to prefix) 1305 suitable for use in a Makefile 1306 """ 1307 return os.path.join(INSTALL_LIB_DIR, self.dll_file()) 1308 1309 def mk_makefile(self, out): 1310 Component.mk_makefile(self, out) 1311 # generate rule for (SO_EXT) 1312 out.write('%s:' % self.dll_file()) 1313 deps = sort_components(self.deps) 1314 objs = [] 1315 for cppfile in get_cpp_files(self.src_dir): 1316 objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]) 1317 objs.append(objfile) 1318 # Explicitly include obj files of reexport. This fixes problems with exported symbols on Linux and OSX. 1319 for reexport in self.reexports: 1320 reexport = get_component(reexport) 1321 for cppfile in get_cpp_files(reexport.src_dir): 1322 objfile = '%s$(OBJ_EXT)' % os.path.join(reexport.build_dir, os.path.splitext(cppfile)[0]) 1323 objs.append(objfile) 1324 for obj in objs: 1325 out.write(' ') 1326 out.write(obj) 1327 for dep in deps: 1328 if dep not in self.reexports: 1329 c_dep = get_component(dep) 1330 out.write(' ' + c_dep.get_link_name()) 1331 out.write('\n') 1332 out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file()) 1333 for obj in objs: 1334 out.write(' ') 1335 out.write(obj) 1336 for dep in deps: 1337 if dep not in self.reexports: 1338 c_dep = get_component(dep) 1339 out.write(' ' + c_dep.get_link_name()) 1340 out.write(' $(SLINK_EXTRA_FLAGS)') 1341 if IS_WINDOWS: 1342 out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) 1343 if self.staging_link: 1344 if IS_WINDOWS: 1345 out.write('\n\tcopy %s %s' % (self.dll_file(), self.staging_link)) 1346 elif IS_OSX: 1347 out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link)) 1348 else: 1349 out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link)) 1350 out.write('\n') 1351 if self.static: 1352 if IS_WINDOWS: 1353 libfile = '%s-static$(LIB_EXT)' % self.dll_name 1354 else: 1355 libfile = '%s$(LIB_EXT)' % self.dll_name 1356 self.mk_static(out, libfile) 1357 out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile)) 1358 else: 1359 out.write('%s: %s\n\n' % (self.name, self.dll_file())) 1360 1361 def mk_static(self, out, libfile): 1362 # generate rule for lib 1363 objs = [] 1364 for cppfile in get_cpp_files(self.src_dir): 1365 objfile = '%s$(OBJ_EXT)' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]) 1366 objs.append(objfile) 1367 # we have to "reexport" all object files 1368 for dep in self.deps: 1369 dep = get_component(dep) 1370 for cppfile in get_cpp_files(dep.src_dir): 1371 objfile = '%s$(OBJ_EXT)' % os.path.join(dep.build_dir, os.path.splitext(cppfile)[0]) 1372 objs.append(objfile) 1373 out.write('%s:' % libfile) 1374 for obj in objs: 1375 out.write(' ') 1376 out.write(obj) 1377 out.write('\n') 1378 out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile) 1379 for obj in objs: 1380 out.write(' ') 1381 out.write(obj) 1382 out.write('\n') 1383 1384 def main_component(self): 1385 return self.install 1386 1387 def require_install_tactics(self): 1388 return ('tactic' in self.deps) and ('cmd_context' in self.deps) 1389 1390 def require_mem_initializer(self): 1391 return True 1392 1393 def require_def_file(self): 1394 return IS_WINDOWS and self.export_files 1395 1396 def mk_install_deps(self, out): 1397 out.write('%s$(SO_EXT)' % self.dll_name) 1398 if self.static: 1399 out.write(' %s$(LIB_EXT)' % self.dll_name) 1400 1401 def mk_install(self, out): 1402 if self.install: 1403 MakeRuleCmd.install_files(out, self.dll_file(), self.install_path()) 1404 if self.static: 1405 libfile = '%s$(LIB_EXT)' % self.dll_name 1406 MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile)) 1407 1408 def mk_uninstall(self, out): 1409 MakeRuleCmd.remove_installed_files(out, self.install_path()) 1410 libfile = '%s$(LIB_EXT)' % self.dll_name 1411 MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile)) 1412 1413 def mk_win_dist(self, build_path, dist_path): 1414 if self.install: 1415 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1416 shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), 1417 '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1418 shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), 1419 '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1420 shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name), 1421 '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1422 1423 def mk_unix_dist(self, build_path, dist_path): 1424 if self.install: 1425 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1426 so = get_so_ext() 1427 shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so), 1428 '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so)) 1429 shutil.copy('%s.a' % os.path.join(build_path, self.dll_name), 1430 '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1431 1432class JsComponent(Component): 1433 def __init__(self): 1434 Component.__init__(self, "js", None, []) 1435 1436 def main_component(self): 1437 return False 1438 1439 def mk_win_dist(self, build_path, dist_path): 1440 return 1441 1442 def mk_unix_dist(self, build_path, dist_path): 1443 return 1444 1445 def mk_makefile(self, out): 1446 return 1447 1448class PythonComponent(Component): 1449 def __init__(self, name, libz3Component): 1450 assert isinstance(libz3Component, DLLComponent) 1451 global PYTHON_ENABLED 1452 Component.__init__(self, name, None, []) 1453 self.libz3Component = libz3Component 1454 1455 def main_component(self): 1456 return False 1457 1458 def mk_win_dist(self, build_path, dist_path): 1459 if not is_python_enabled(): 1460 return 1461 1462 src = os.path.join(build_path, 'python', 'z3') 1463 dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3') 1464 if os.path.exists(dst): 1465 shutil.rmtree(dst) 1466 shutil.copytree(src, dst) 1467 1468 def mk_unix_dist(self, build_path, dist_path): 1469 self.mk_win_dist(build_path, dist_path) 1470 1471 def mk_makefile(self, out): 1472 return 1473 1474class PythonInstallComponent(Component): 1475 def __init__(self, name, libz3Component): 1476 assert isinstance(libz3Component, DLLComponent) 1477 global PYTHON_INSTALL_ENABLED 1478 Component.__init__(self, name, None, []) 1479 self.pythonPkgDir = None 1480 self.in_prefix_install = True 1481 self.libz3Component = libz3Component 1482 1483 if not PYTHON_INSTALL_ENABLED: 1484 return 1485 1486 if IS_WINDOWS: 1487 # Installing under Windows doesn't make sense as the install prefix is used 1488 # but that doesn't make sense under Windows 1489 # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix, 1490 # i.e., something along the lines of C:\Python\... At the moment we are not 1491 # sure whether we would want to install libz3.dll into that directory though. 1492 PYTHON_INSTALL_ENABLED = False 1493 return 1494 else: 1495 PYTHON_INSTALL_ENABLED = True 1496 1497 if IS_WINDOWS or IS_OSX: 1498 # Use full path that is possibly outside of install prefix 1499 self.in_prefix_install = PYTHON_PACKAGE_DIR.startswith(PREFIX) 1500 self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) 1501 else: 1502 # Use path inside the prefix (should be the normal case on Linux) 1503 # CMW: Also normal on *BSD? 1504 if not PYTHON_PACKAGE_DIR.startswith(PREFIX): 1505 raise MKException(('The python package directory ({}) must live ' + 1506 'under the install prefix ({}) to install the python bindings.' + 1507 'Use --pypkgdir and --prefix to set the python package directory ' + 1508 'and install prefix respectively. Note that the python package ' + 1509 'directory does not need to exist and will be created if ' + 1510 'necessary during install.').format( 1511 PYTHON_PACKAGE_DIR, 1512 PREFIX)) 1513 self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) 1514 self.in_prefix_install = True 1515 1516 if self.in_prefix_install: 1517 assert not os.path.isabs(self.pythonPkgDir) 1518 1519 def final_info(self): 1520 if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED: 1521 print("Warning: The detected Python package directory (%s) is not " 1522 "in the installation prefix (%s). This can lead to a broken " 1523 "Python API installation. Use --pypkgdir= to change the " 1524 "Python package directory." % (PYTHON_PACKAGE_DIR, PREFIX)) 1525 1526 def main_component(self): 1527 return False 1528 1529 def mk_install(self, out): 1530 if not is_python_install_enabled(): 1531 return 1532 MakeRuleCmd.make_install_directory(out, 1533 os.path.join(self.pythonPkgDir, 'z3'), 1534 in_prefix=self.in_prefix_install) 1535 MakeRuleCmd.make_install_directory(out, 1536 os.path.join(self.pythonPkgDir, 'z3', 'lib'), 1537 in_prefix=self.in_prefix_install) 1538 1539 # Sym-link or copy libz3 into python package directory 1540 if IS_WINDOWS or IS_OSX: 1541 MakeRuleCmd.install_files(out, 1542 self.libz3Component.dll_file(), 1543 os.path.join(self.pythonPkgDir, 'z3', 'lib', 1544 self.libz3Component.dll_file()), 1545 in_prefix=self.in_prefix_install 1546 ) 1547 else: 1548 # Create symbolic link to save space. 1549 # It's important that this symbolic link be relative (rather 1550 # than absolute) so that the install is relocatable (needed for 1551 # staged installs that use DESTDIR). 1552 MakeRuleCmd.create_relative_symbolic_link(out, 1553 self.libz3Component.install_path(), 1554 os.path.join(self.pythonPkgDir, 'z3', 'lib', 1555 self.libz3Component.dll_file() 1556 ), 1557 ) 1558 1559 MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'), 1560 os.path.join(self.pythonPkgDir, 'z3'), 1561 in_prefix=self.in_prefix_install) 1562 if sys.version >= "3": 1563 pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__') 1564 MakeRuleCmd.make_install_directory(out, 1565 pythonPycacheDir, 1566 in_prefix=self.in_prefix_install) 1567 MakeRuleCmd.install_files(out, 1568 os.path.join('python', 'z3', '__pycache__', '*.pyc'), 1569 pythonPycacheDir, 1570 in_prefix=self.in_prefix_install) 1571 else: 1572 MakeRuleCmd.install_files(out, 1573 os.path.join('python', 'z3', '*.pyc'), 1574 os.path.join(self.pythonPkgDir,'z3'), 1575 in_prefix=self.in_prefix_install) 1576 1577 if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): 1578 out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) 1579 1580 def mk_uninstall(self, out): 1581 if not is_python_install_enabled(): 1582 return 1583 MakeRuleCmd.remove_installed_files(out, 1584 os.path.join(self.pythonPkgDir, 1585 self.libz3Component.dll_file()), 1586 in_prefix=self.in_prefix_install 1587 ) 1588 MakeRuleCmd.remove_installed_files(out, 1589 os.path.join(self.pythonPkgDir, 'z3', '*.py'), 1590 in_prefix=self.in_prefix_install) 1591 MakeRuleCmd.remove_installed_files(out, 1592 os.path.join(self.pythonPkgDir, 'z3', '*.pyc'), 1593 in_prefix=self.in_prefix_install) 1594 MakeRuleCmd.remove_installed_files(out, 1595 os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'), 1596 in_prefix=self.in_prefix_install 1597 ) 1598 MakeRuleCmd.remove_installed_files(out, 1599 os.path.join(self.pythonPkgDir, 'z3', 'lib', 1600 self.libz3Component.dll_file())) 1601 1602 def mk_makefile(self, out): 1603 return 1604 1605def set_key_file(self): 1606 global DOTNET_KEY_FILE 1607 # We need to give the assembly a strong name so that it 1608 # can be installed into the GAC with ``make install`` 1609 if not DOTNET_KEY_FILE is None: 1610 self.key_file = DOTNET_KEY_FILE 1611 1612 if not self.key_file is None: 1613 if os.path.isfile(self.key_file): 1614 self.key_file = os.path.abspath(self.key_file) 1615 elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): 1616 self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) 1617 else: 1618 print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) 1619 self.key_file = None 1620 1621 1622# build for dotnet core 1623class DotNetDLLComponent(Component): 1624 def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): 1625 Component.__init__(self, name, path, deps) 1626 if dll_name is None: 1627 dll_name = name 1628 if assembly_info_dir is None: 1629 assembly_info_dir = "." 1630 self.dll_name = dll_name 1631 self.assembly_info_dir = assembly_info_dir 1632 self.key_file = default_key_file 1633 1634 1635 def mk_makefile(self, out): 1636 if not is_dotnet_core_enabled(): 1637 return 1638 cs_fp_files = [] 1639 for cs_file in get_cs_files(self.src_dir): 1640 cs_fp_files.append(os.path.join(self.to_src_dir, cs_file)) 1641 if self.assembly_info_dir != '.': 1642 for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)): 1643 cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file)) 1644 dllfile = '%s.dll' % self.dll_name 1645 out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name)) 1646 for cs_file in cs_fp_files: 1647 out.write(' ') 1648 out.write(cs_file) 1649 out.write('\n') 1650 1651 set_key_file(self) 1652 key = "" 1653 if not self.key_file is None: 1654 key = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file 1655 key += "\n<SignAssembly>true</SignAssembly>" 1656 1657 version = get_version_string(3) 1658 1659 core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk"> 1660 1661 <PropertyGroup> 1662 <TargetFramework>netstandard1.4</TargetFramework> 1663 <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants> 1664 <DebugType>portable</DebugType> 1665 <AssemblyName>Microsoft.Z3</AssemblyName> 1666 <OutputType>Library</OutputType> 1667 <PackageId>Microsoft.Z3</PackageId> 1668 <GenerateDocumentationFile>true</GenerateDocumentationFile> 1669 <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion> 1670 <Version>%s</Version> 1671 <GeneratePackageOnBuild>true</GeneratePackageOnBuild> 1672 <Authors>Microsoft</Authors> 1673 <Company>Microsoft</Company> 1674 <EnableDefaultCompileItems>false</EnableDefaultCompileItems> 1675 <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description> 1676 <Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright> 1677 <PackageTags>smt constraint solver theorem prover</PackageTags> 1678 %s 1679 </PropertyGroup> 1680 1681 <ItemGroup> 1682 <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" /> 1683 </ItemGroup> 1684 1685</Project>""" % (version, key, self.to_src_dir) 1686 1687 mk_dir(os.path.join(BUILD_DIR, 'dotnet')) 1688 csproj = os.path.join('dotnet', 'z3.csproj') 1689 with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: 1690 ous.write(core_csproj_str) 1691 1692 dotnetCmdLine = [DOTNET, "build", csproj] 1693 1694 dotnetCmdLine.extend(['-c']) 1695 if DEBUG_MODE: 1696 dotnetCmdLine.extend(['Debug']) 1697 else: 1698 dotnetCmdLine.extend(['Release']) 1699 1700 path = os.path.join(os.path.abspath(BUILD_DIR), ".") 1701 dotnetCmdLine.extend(['-o', path]) 1702 1703 MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) 1704 out.write('\n') 1705 out.write('%s: %s\n\n' % (self.name, dllfile)) 1706 1707 def main_component(self): 1708 return is_dotnet_core_enabled() 1709 1710 def has_assembly_info(self): 1711 # TBD: is this required for dotnet core given that version numbers are in z3.csproj file? 1712 return False 1713 1714 1715 def mk_win_dist(self, build_path, dist_path): 1716 if is_dotnet_core_enabled(): 1717 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1718 shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), 1719 '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1720 shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), 1721 '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1722 shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), 1723 '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1724 shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), 1725 '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1726 if DEBUG_MODE: 1727 shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), 1728 '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1729 1730 def mk_unix_dist(self, build_path, dist_path): 1731 if is_dotnet_core_enabled(): 1732 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1733 shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), 1734 '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1735 shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), 1736 '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1737 shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), 1738 '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) 1739 1740 def mk_install_deps(self, out): 1741 pass 1742 1743 def mk_install(self, out): 1744 pass 1745 1746 def mk_uninstall(self, out): 1747 pass 1748 1749class JavaDLLComponent(Component): 1750 def __init__(self, name, dll_name, package_name, manifest_file, path, deps): 1751 Component.__init__(self, name, path, deps) 1752 if dll_name is None: 1753 dll_name = name 1754 self.dll_name = dll_name 1755 self.package_name = package_name 1756 self.manifest_file = manifest_file 1757 self.install = not is_windows() 1758 1759 def mk_makefile(self, out): 1760 global JAVAC 1761 global JAR 1762 1763 if is_java_enabled(): 1764 mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes')) 1765 dllfile = '%s$(SO_EXT)' % self.dll_name 1766 out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp')) 1767 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) 1768 if IS_OSX: 1769 t = t.replace('PLATFORM', 'darwin') 1770 elif is_linux(): 1771 t = t.replace('PLATFORM', 'linux') 1772 elif is_hurd(): 1773 t = t.replace('PLATFORM', 'hurd') 1774 elif IS_DRAGONFLY: 1775 t = t.replace('PLATFORM', 'dragonfly') 1776 elif IS_NETBSD: 1777 t = t.replace('PLATFORM', 'netbsd') 1778 elif IS_OPENBSD: 1779 t = t.replace('PLATFORM', 'openbsd') 1780 elif IS_SUNOS: 1781 t = t.replace('PLATFORM', 'SunOS') 1782 elif IS_CYGWIN: 1783 t = t.replace('PLATFORM', 'cygwin') 1784 elif IS_MSYS2: 1785 t = t.replace('PLATFORM', 'win32') 1786 else: 1787 t = t.replace('PLATFORM', 'win32') 1788 out.write(t) 1789 if IS_WINDOWS: # On Windows, CL creates a .lib file to link against. 1790 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % 1791 os.path.join('api', 'java', 'Native')) 1792 else: 1793 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % 1794 os.path.join('api', 'java', 'Native')) 1795 out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name) 1796 deps = '' 1797 for jfile in get_java_files(self.src_dir): 1798 deps += ('%s ' % os.path.join(self.to_src_dir, jfile)) 1799 for jfile in get_java_files(os.path.join(self.src_dir, "enumerations")): 1800 deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile) 1801 out.write(deps) 1802 out.write('\n') 1803 #if IS_WINDOWS: 1804 JAVAC = '"%s"' % JAVAC 1805 JAR = '"%s"' % JAR 1806 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'))) 1807 out.write(t) 1808 t = ('\t%s -source 1.8 -target 1.8 -cp %s %s.java -d %s\n' % (JAVAC, 1809 os.path.join('api', 'java', 'classes'), 1810 os.path.join(self.to_src_dir, '*'), 1811 os.path.join('api', 'java', 'classes'))) 1812 out.write(t) 1813 out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name, 1814 os.path.join(self.to_src_dir, 'manifest'), 1815 os.path.join('api', 'java', 'classes'))) 1816 out.write('java: %s.jar\n\n' % self.package_name) 1817 1818 def main_component(self): 1819 return is_java_enabled() 1820 1821 def mk_win_dist(self, build_path, dist_path): 1822 if JAVA_ENABLED: 1823 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1824 shutil.copy('%s.jar' % os.path.join(build_path, self.package_name), 1825 '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name)) 1826 shutil.copy(os.path.join(build_path, 'libz3java.dll'), 1827 os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll')) 1828 shutil.copy(os.path.join(build_path, 'libz3java.lib'), 1829 os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib')) 1830 1831 def mk_unix_dist(self, build_path, dist_path): 1832 if JAVA_ENABLED: 1833 mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) 1834 shutil.copy('%s.jar' % os.path.join(build_path, self.package_name), 1835 '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name)) 1836 so = get_so_ext() 1837 shutil.copy(os.path.join(build_path, 'libz3java.%s' % so), 1838 os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so)) 1839 1840 def mk_install(self, out): 1841 if is_java_enabled() and self.install: 1842 dllfile = '%s$(SO_EXT)' % self.dll_name 1843 MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile)) 1844 jarfile = '{}.jar'.format(self.package_name) 1845 MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile)) 1846 1847 def mk_uninstall(self, out): 1848 if is_java_enabled() and self.install: 1849 dllfile = '%s$(SO_EXT)' % self.dll_name 1850 MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile)) 1851 jarfile = '{}.jar'.format(self.package_name) 1852 MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile)) 1853 1854class MLComponent(Component): 1855 1856 def __init__(self, name, lib_name, path, deps): 1857 Component.__init__(self, name, path, deps) 1858 if lib_name is None: 1859 lib_name = name 1860 self.lib_name = lib_name 1861 self.modules = ["z3enums", "z3native", "z3"] # dependencies in this order! 1862 self.stubs = "z3native_stubs" 1863 self.sub_dir = os.path.join('api', 'ml') 1864 1865 self.destdir = "" 1866 self.ldconf = "" 1867 # Calling _init_ocamlfind_paths() is postponed to later because 1868 # OCAMLFIND hasn't been checked yet. 1869 1870 def _install_bindings(self): 1871 # FIXME: Depending on global state is gross. We can't pre-compute this 1872 # in the constructor because we haven't tested for ocamlfind yet 1873 return OCAMLFIND != '' 1874 1875 def _init_ocamlfind_paths(self): 1876 """ 1877 Initialises self.destdir and self.ldconf 1878 Do not call this from the MLComponent constructor because OCAMLFIND 1879 has not been checked at that point 1880 """ 1881 if self.destdir != "" and self.ldconf != "": 1882 # Initialisation already done 1883 return 1884 # Use Ocamlfind to get the default destdir and ldconf path 1885 self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir']) 1886 if self.destdir == "": 1887 raise MKException('Failed to get OCaml destdir') 1888 1889 if not os.path.isdir(self.destdir): 1890 raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir)) 1891 1892 self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf']) 1893 if self.ldconf == "": 1894 raise MKException('Failed to get OCaml ldconf path') 1895 1896 def final_info(self): 1897 if not self._install_bindings(): 1898 print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed") 1899 1900 def mk_makefile(self, out): 1901 if is_ml_enabled(): 1902 CP_CMD = 'cp' 1903 if IS_WINDOWS: 1904 CP_CMD='copy' 1905 1906 OCAML_FLAGS = '' 1907 if DEBUG_MODE: 1908 OCAML_FLAGS += '-g' 1909 1910 if OCAMLFIND: 1911 OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package zarith' + ' ' + OCAML_FLAGS 1912 OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package zarith' + ' ' + OCAML_FLAGS 1913 else: 1914 OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS 1915 OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS 1916 1917 src_dir = self.to_src_dir 1918 mk_dir(os.path.join(BUILD_DIR, self.sub_dir)) 1919 api_src = get_component(API_COMPONENT).to_src_dir 1920 # remove /GL and -std=c++11; the ocaml tools don't like them. 1921 if IS_WINDOWS: 1922 out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') 1923 else: 1924 out.write('CXXFLAGS_OCAML=$(subst -std=c++11,,$(CXXFLAGS))\n') 1925 1926 substitutions = { 'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) } 1927 1928 configure_file(os.path.join(self.src_dir, 'META.in'), 1929 os.path.join(BUILD_DIR, self.sub_dir, 'META'), 1930 substitutions) 1931 1932 stubsc = os.path.join(src_dir, self.stubs + '.c') 1933 stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)' 1934 base_dll_name = get_component(Z3_DLL_COMPONENT).dll_name 1935 if STATIC_LIB: 1936 z3link = 'z3-static' 1937 z3linkdep = base_dll_name + '-static$(LIB_EXT)' 1938 out.write('%s: %s\n' % (z3linkdep, base_dll_name + '$(LIB_EXT)')) 1939 out.write('\tcp $< $@\n') 1940 else: 1941 z3link = 'z3' 1942 z3linkdep = base_dll_name + '$(SO_EXT)' 1943 out.write('%s: %s %s\n' % (stubso, stubsc, z3linkdep)) 1944 out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' % 1945 (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc)) 1946 1947 cmos = '' 1948 for m in self.modules: 1949 ml = os.path.join(src_dir, m + '.ml') 1950 cmo = os.path.join(self.sub_dir, m + '.cmo') 1951 existing_mli = os.path.join(src_dir, m + '.mli') 1952 mli = os.path.join(self.sub_dir, m + '.mli') 1953 cmi = os.path.join(self.sub_dir, m + '.cmi') 1954 out.write('%s: %s %s\n' % (cmo, ml, cmos)) 1955 if (os.path.exists(existing_mli[3:])): 1956 out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli)) 1957 else: 1958 out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli)) 1959 out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli)) 1960 out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml)) 1961 cmos = cmos + cmo + ' ' 1962 1963 cmxs = '' 1964 for m in self.modules: 1965 ff = os.path.join(src_dir, m + '.ml') 1966 ft = os.path.join(self.sub_dir, m + '.cmx') 1967 out.write('%s: %s %s %s\n' % (ft, ff, cmos, cmxs)) 1968 out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff)) 1969 cmxs = cmxs + ' ' + ft 1970 1971 1972 OCAMLMKLIB = 'ocamlmklib' 1973 1974 LIBZ3 = '-l' + z3link + ' -lstdc++' 1975 if is_cygwin() and not(is_cygwin_mingw()): 1976 LIBZ3 = z3linkdep 1977 1978 LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split())) 1979 1980 if DEBUG_MODE and not(is_cygwin()): 1981 # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well. 1982 OCAMLMKLIB += ' -g' 1983 1984 z3mls = os.path.join(self.sub_dir, 'z3ml') 1985 1986 out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep)) 1987 out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3)) 1988 out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls)) 1989 out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3)) 1990 out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls)) 1991 out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) 1992 1993 out.write('\n') 1994 out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) 1995 out.write('\n') 1996 1997 if IS_WINDOWS: 1998 out.write('ocamlfind_install: ') 1999 self.mk_install_deps(out) 2000 out.write('\n') 2001 self.mk_install(out) 2002 out.write('\n') 2003 out.write('ocamlfind_uninstall:\n') 2004 self.mk_uninstall(out) 2005 out.write('\n') 2006 2007 def mk_install_deps(self, out): 2008 if is_ml_enabled() and self._install_bindings(): 2009 out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') 2010 out.write(os.path.join(self.sub_dir, 'META ')) 2011 out.write(os.path.join(self.sub_dir, 'z3ml.cma ')) 2012 out.write(os.path.join(self.sub_dir, 'z3ml.cmxa ')) 2013 out.write(os.path.join(self.sub_dir, 'z3ml.cmxs ')) 2014 2015 def mk_install(self, out): 2016 if is_ml_enabled() and self._install_bindings(): 2017 self._init_ocamlfind_paths() 2018 in_prefix = self.destdir.startswith(PREFIX) 2019 maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX) 2020 # Note that when doing a staged install with DESTDIR that modifying 2021 # OCaml's ``ld.conf`` may fail. Therefore packagers will need to 2022 # make their packages modify it manually at package install time 2023 # as opposed to ``make install`` time. 2024 MakeRuleCmd.make_install_directory(out, 2025 maybe_stripped_destdir, 2026 in_prefix=in_prefix) 2027 out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format( 2028 ldconf=self.ldconf, 2029 ocamlfind=OCAMLFIND, 2030 ocaml_destdir=self.destdir, 2031 metafile=os.path.join(self.sub_dir, 'META'))) 2032 2033 for m in self.modules: 2034 mli = os.path.join(self.src_dir, m) + '.mli' 2035 if os.path.exists(mli): 2036 out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli') 2037 else: 2038 out.write(' ' + os.path.join(self.sub_dir, m) + '.mli') 2039 out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi') 2040 out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx') 2041 out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)')))) 2042 out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)')))) 2043 out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma')))) 2044 out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa')))) 2045 out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs')))) 2046 out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml')))) 2047 if is_windows() or is_cygwin_mingw(): 2048 out.write('.dll') 2049 else: 2050 out.write('.so') # .so also on OSX! 2051 out.write('\n') 2052 2053 def mk_uninstall(self, out): 2054 if is_ml_enabled() and self._install_bindings(): 2055 self._init_ocamlfind_paths() 2056 out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format( 2057 ldconf=self.ldconf, 2058 ocamlfind=OCAMLFIND, 2059 ocaml_destdir=self.destdir)) 2060 2061 def main_component(self): 2062 return is_ml_enabled() 2063 2064class ExampleComponent(Component): 2065 def __init__(self, name, path): 2066 Component.__init__(self, name, path, []) 2067 self.ex_dir = os.path.join(EXAMPLE_DIR, self.path) 2068 self.to_ex_dir = os.path.join(REV_BUILD_DIR, self.ex_dir) 2069 2070 def is_example(self): 2071 return True 2072 2073class CppExampleComponent(ExampleComponent): 2074 def __init__(self, name, path): 2075 ExampleComponent.__init__(self, name, path) 2076 2077 def compiler(self): 2078 return "$(CXX)" 2079 2080 def src_files(self): 2081 return get_cpp_files(self.ex_dir) 2082 2083 def mk_makefile(self, out): 2084 dll_name = get_component(Z3_DLL_COMPONENT).dll_name 2085 dll = '%s$(SO_EXT)' % dll_name 2086 2087 objfiles = '' 2088 for cppfile in self.src_files(): 2089 objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')]) 2090 objfiles = objfiles + ('%s ' % objfile) 2091 out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile))); 2092 out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile)) 2093 # Add include dir components 2094 out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) 2095 out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir) 2096 out.write(' %s' % os.path.join(self.to_ex_dir, cppfile)) 2097 out.write('\n') 2098 2099 exefile = '%s$(EXE_EXT)' % self.name 2100 out.write('%s: %s %s\n' % (exefile, dll, objfiles)) 2101 out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles)) 2102 if IS_WINDOWS: 2103 out.write('%s.lib' % dll_name) 2104 else: 2105 out.write(dll) 2106 out.write(' $(LINK_EXTRA_FLAGS)\n') 2107 out.write('_ex_%s: %s\n\n' % (self.name, exefile)) 2108 2109class CExampleComponent(CppExampleComponent): 2110 def __init__(self, name, path): 2111 CppExampleComponent.__init__(self, name, path) 2112 2113 def compiler(self): 2114 return "$(CC)" 2115 2116 def src_files(self): 2117 return get_c_files(self.ex_dir) 2118 2119 def mk_makefile(self, out): 2120 dll_name = get_component(Z3_DLL_COMPONENT).dll_name 2121 dll = '%s$(SO_EXT)' % dll_name 2122 2123 objfiles = '' 2124 for cfile in self.src_files(): 2125 objfile = '%s$(OBJ_EXT)' % (cfile[:cfile.rfind('.')]) 2126 objfiles = objfiles + ('%s ' % objfile) 2127 out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cfile))); 2128 out.write('\t%s $(CFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(C_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile)) 2129 out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) 2130 out.write(' %s' % os.path.join(self.to_ex_dir, cfile)) 2131 out.write('\n') 2132 2133 exefile = '%s$(EXE_EXT)' % self.name 2134 out.write('%s: %s %s\n' % (exefile, dll, objfiles)) 2135 out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles)) 2136 if IS_WINDOWS: 2137 out.write('%s.lib' % dll_name) 2138 else: 2139 out.write(dll) 2140 out.write(' $(LINK_EXTRA_FLAGS)\n') 2141 out.write('_ex_%s: %s\n\n' % (self.name, exefile)) 2142 2143class DotNetExampleComponent(ExampleComponent): 2144 def __init__(self, name, path): 2145 ExampleComponent.__init__(self, name, path) 2146 2147 def is_example(self): 2148 return is_dotnet_core_enabled() 2149 2150 def mk_makefile(self, out): 2151 if is_dotnet_core_enabled(): 2152 proj_name = 'dotnet_example.csproj' 2153 out.write('_ex_%s:' % self.name) 2154 for csfile in get_cs_files(self.ex_dir): 2155 out.write(' ') 2156 out.write(os.path.join(self.to_ex_dir, csfile)) 2157 2158 mk_dir(os.path.join(BUILD_DIR, 'dotnet_example')) 2159 csproj = os.path.join('dotnet_example', proj_name) 2160 if VS_X64: 2161 platform = 'x64' 2162 elif VS_ARM: 2163 platform = 'ARM' 2164 else: 2165 platform = 'x86' 2166 2167 dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk"> 2168 <PropertyGroup> 2169 <OutputType>Exe</OutputType> 2170 <TargetFramework>netcoreapp2.0</TargetFramework> 2171 <PlatformTarget>%s</PlatformTarget> 2172 </PropertyGroup> 2173 <ItemGroup> 2174 <Compile Include="..\%s/*.cs" /> 2175 <Reference Include="Microsoft.Z3"> 2176 <HintPath>..\Microsoft.Z3.dll</HintPath> 2177 </Reference> 2178 </ItemGroup> 2179</Project>""" % (platform, self.to_ex_dir) 2180 2181 with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: 2182 ous.write(dotnet_proj_str) 2183 2184 out.write('\n') 2185 dotnetCmdLine = [DOTNET, "build", csproj] 2186 dotnetCmdLine.extend(['-c']) 2187 if DEBUG_MODE: 2188 dotnetCmdLine.extend(['Debug']) 2189 else: 2190 dotnetCmdLine.extend(['Release']) 2191 MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) 2192 out.write('\n') 2193 2194class JavaExampleComponent(ExampleComponent): 2195 def __init__(self, name, path): 2196 ExampleComponent.__init__(self, name, path) 2197 2198 def is_example(self): 2199 return JAVA_ENABLED 2200 2201 def mk_makefile(self, out): 2202 if JAVA_ENABLED: 2203 pkg = get_component(JAVA_COMPONENT).package_name + '.jar' 2204 out.write('JavaExample.class: %s' % (pkg)) 2205 deps = '' 2206 for jfile in get_java_files(self.ex_dir): 2207 out.write(' %s' % os.path.join(self.to_ex_dir, jfile)) 2208 if IS_WINDOWS: 2209 deps = deps.replace('/', '\\') 2210 out.write('%s\n' % deps) 2211 out.write('\t%s -cp %s ' % (JAVAC, pkg)) 2212 win_ex_dir = self.to_ex_dir 2213 for javafile in get_java_files(self.ex_dir): 2214 out.write(' ') 2215 out.write(os.path.join(win_ex_dir, javafile)) 2216 out.write(' -d .\n') 2217 out.write('_ex_%s: JavaExample.class\n\n' % (self.name)) 2218 2219class MLExampleComponent(ExampleComponent): 2220 def __init__(self, name, path): 2221 ExampleComponent.__init__(self, name, path) 2222 2223 def is_example(self): 2224 return ML_ENABLED 2225 2226 def mk_makefile(self, out): 2227 if ML_ENABLED: 2228 out.write('ml_example.byte: api/ml/z3ml.cma') 2229 for mlfile in get_ml_files(self.ex_dir): 2230 out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) 2231 out.write('\n') 2232 out.write('\tocamlfind %s ' % OCAMLC) 2233 if DEBUG_MODE: 2234 out.write('-g ') 2235 out.write('-custom -o ml_example.byte -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cma') 2236 for mlfile in get_ml_files(self.ex_dir): 2237 out.write(' %s/%s' % (self.to_ex_dir, mlfile)) 2238 out.write('\n') 2239 out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa') 2240 for mlfile in get_ml_files(self.ex_dir): 2241 out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) 2242 out.write('\n') 2243 out.write('\tocamlfind %s ' % OCAMLOPT) 2244 if DEBUG_MODE: 2245 out.write('-g ') 2246 out.write('-o ml_example$(EXE_EXT) -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cmxa') 2247 for mlfile in get_ml_files(self.ex_dir): 2248 out.write(' %s/%s' % (self.to_ex_dir, mlfile)) 2249 out.write('\n') 2250 out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name) 2251 2252class PythonExampleComponent(ExampleComponent): 2253 def __init__(self, name, path): 2254 ExampleComponent.__init__(self, name, path) 2255 2256 # Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked. 2257 # We don't need to include them in the :examples rule 2258 def mk_makefile(self, out): 2259 full = os.path.join(EXAMPLE_DIR, self.path) 2260 for py in filter(lambda f: f.endswith('.py'), os.listdir(full)): 2261 shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py)) 2262 if is_verbose(): 2263 print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python'))) 2264 out.write('_ex_%s: \n\n' % self.name) 2265 2266 def mk_win_dist(self, build_path, dist_path): 2267 full = os.path.join(EXAMPLE_DIR, self.path) 2268 py = 'example.py' 2269 shutil.copyfile(os.path.join(full, py), 2270 os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py)) 2271 2272 def mk_unix_dist(self, build_path, dist_path): 2273 self.mk_win_dist(build_path, dist_path) 2274 2275 2276def reg_component(name, c): 2277 global _Id, _Components, _ComponentNames, _Name2Component 2278 c.id = _Id 2279 _Id = _Id + 1 2280 _Components.append(c) 2281 _ComponentNames.add(name) 2282 _Name2Component[name] = c 2283 if VERBOSE: 2284 print("New component: '%s'" % name) 2285 2286def add_lib(name, deps=[], path=None, includes2install=[]): 2287 c = LibComponent(name, path, deps, includes2install) 2288 reg_component(name, c) 2289 2290def add_clib(name, deps=[], path=None, includes2install=[]): 2291 c = CLibComponent(name, path, deps, includes2install) 2292 reg_component(name, c) 2293 2294def add_hlib(name, path=None, includes2install=[]): 2295 c = HLibComponent(name, path, includes2install) 2296 reg_component(name, c) 2297 2298def add_exe(name, deps=[], path=None, exe_name=None, install=True): 2299 c = ExeComponent(name, exe_name, path, deps, install) 2300 reg_component(name, c) 2301 2302def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True): 2303 c = ExtraExeComponent(name, exe_name, path, deps, install) 2304 reg_component(name, c) 2305 2306def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None): 2307 c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link) 2308 reg_component(name, c) 2309 return c 2310 2311def add_dot_net_core_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None): 2312 c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file) 2313 reg_component(name, c) 2314 2315def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None): 2316 c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps) 2317 reg_component(name, c) 2318 2319def add_python(libz3Component): 2320 name = 'python' 2321 reg_component(name, PythonComponent(name, libz3Component)) 2322 2323def add_js(): 2324 reg_component('js', JsComponent()) 2325 2326def add_python_install(libz3Component): 2327 name = 'python_install' 2328 reg_component(name, PythonInstallComponent(name, libz3Component)) 2329 2330def add_ml_lib(name, deps=[], path=None, lib_name=None): 2331 c = MLComponent(name, lib_name, path, deps) 2332 reg_component(name, c) 2333 2334def add_cpp_example(name, path=None): 2335 c = CppExampleComponent(name, path) 2336 reg_component(name, c) 2337 2338def add_c_example(name, path=None): 2339 c = CExampleComponent(name, path) 2340 reg_component(name, c) 2341 2342def add_dotnet_example(name, path=None): 2343 c = DotNetExampleComponent(name, path) 2344 reg_component(name, c) 2345 2346def add_java_example(name, path=None): 2347 c = JavaExampleComponent(name, path) 2348 reg_component(name, c) 2349 2350def add_ml_example(name, path=None): 2351 c = MLExampleComponent(name, path) 2352 reg_component(name, c) 2353 2354def add_z3py_example(name, path=None): 2355 c = PythonExampleComponent(name, path) 2356 reg_component(name, c) 2357 2358def mk_config(): 2359 if ONLY_MAKEFILES: 2360 return 2361 config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') 2362 global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED 2363 if IS_WINDOWS: 2364 config.write( 2365 'CC=cl\n' 2366 'CXX=cl\n' 2367 'CXX_OUT_FLAG=/Fo\n' 2368 'C_OUT_FLAG=/Fo\n' 2369 'OBJ_EXT=.obj\n' 2370 'LIB_EXT=.lib\n' 2371 'AR=lib\n' 2372 'AR_OUTFLAG=/OUT:\n' 2373 'EXE_EXT=.exe\n' 2374 'LINK=cl\n' 2375 'LINK_OUT_FLAG=/Fe\n' 2376 'SO_EXT=.dll\n' 2377 'SLINK=cl\n' 2378 'SLINK_OUT_FLAG=/Fe\n' 2379 'OS_DEFINES=/D _WINDOWS\n') 2380 extra_opt = '' 2381 link_extra_opt = '' 2382 if LOG_SYNC: 2383 extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt 2384 if SINGLE_THREADED: 2385 extra_opt = '%s /DSINGLE_THREAD' % extra_opt 2386 if GIT_HASH: 2387 extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) 2388 if GUARD_CF: 2389 extra_opt = ' %s /guard:cf' % extra_opt 2390 link_extra_opt = ' %s /GUARD:CF' % link_extra_opt 2391 if STATIC_BIN: 2392 static_opt = '/MT' 2393 else: 2394 static_opt = '/MD' 2395 maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO' 2396 if DEBUG_MODE: 2397 static_opt = static_opt + 'd' 2398 config.write( 2399 'AR_FLAGS=/nologo\n' 2400 'LINK_FLAGS=/nologo %s\n' 2401 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) 2402 if VS_X64: 2403 config.write( 2404 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd %s %s\n' % (extra_opt, static_opt)) 2405 config.write( 2406 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' 2407 '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)) 2408 elif VS_ARM: 2409 print("ARM on VS is unsupported") 2410 exit(1) 2411 else: 2412 config.write( 2413 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd /arch:SSE2 %s %s\n' % (extra_opt, static_opt)) 2414 config.write( 2415 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' 2416 '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)) 2417 else: 2418 # Windows Release mode 2419 LTCG=' /LTCG' if SLOW_OPTIMIZE else '' 2420 GL = ' /GL' if SLOW_OPTIMIZE else '' 2421 config.write( 2422 'AR_FLAGS=/nologo %s\n' 2423 'LINK_FLAGS=/nologo %s\n' 2424 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt)) 2425 if TRACE: 2426 extra_opt = '%s /D _TRACE ' % extra_opt 2427 if VS_X64: 2428 config.write( 2429 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /Gd /GF /Gy /TP %s %s\n' % (GL, extra_opt, static_opt)) 2430 config.write( 2431 'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n' 2432 'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) 2433 elif VS_ARM: 2434 print("ARM on VS is unsupported") 2435 exit(1) 2436 else: 2437 config.write( 2438 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /Gd /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt)) 2439 config.write( 2440 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' 2441 '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)) 2442 2443 config.write('CFLAGS=$(CXXFLAGS)\n') 2444 2445 # End of Windows VS config.mk 2446 if is_verbose(): 2447 print('64-bit: %s' % is64()) 2448 if is_java_enabled(): 2449 print('JNI Bindings: %s' % JNI_HOME) 2450 print('Java Compiler: %s' % JAVAC) 2451 if is_ml_enabled(): 2452 print('OCaml Compiler: %s' % OCAMLC) 2453 print('OCaml Find tool: %s' % OCAMLFIND) 2454 print('OCaml Native: %s' % OCAMLOPT) 2455 print('OCaml Library: %s' % OCAML_LIB) 2456 else: 2457 OS_DEFINES = "" 2458 ARITH = "internal" 2459 check_ar() 2460 CXX = find_cxx_compiler() 2461 CC = find_c_compiler() 2462 SLIBEXTRAFLAGS = '' 2463# SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS 2464 EXE_EXT = '' 2465 LIB_EXT = '.a' 2466 if GPROF: 2467 CXXFLAGS = '%s -pg' % CXXFLAGS 2468 LDFLAGS = '%s -pg' % LDFLAGS 2469 if GMP: 2470 test_gmp(CXX) 2471 ARITH = "gmp" 2472 CPPFLAGS = '%s -D_MP_GMP' % CPPFLAGS 2473 LDFLAGS = '%s -lgmp' % LDFLAGS 2474 SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS 2475 else: 2476 CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS 2477 if GIT_HASH: 2478 CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) 2479 CXXFLAGS = '%s -std=c++11' % CXXFLAGS 2480 CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS 2481 FPMATH = test_fpmath(CXX) 2482 CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) 2483 if LOG_SYNC: 2484 CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS 2485 if SINGLE_THREADED: 2486 CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS 2487 if DEBUG_MODE: 2488 CXXFLAGS = '%s -g -Wall' % CXXFLAGS 2489 EXAMP_DEBUG_FLAG = '-g' 2490 CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS 2491 else: 2492 CXXFLAGS = '%s -O3' % CXXFLAGS 2493 if GPROF: 2494 CXXFLAGS += '-fomit-frame-pointer' 2495 CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS 2496 if is_CXX_clangpp(): 2497 CXXFLAGS = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS 2498 sysname, _, _, _, machine = os.uname() 2499 if sysname == 'Darwin': 2500 SO_EXT = '.dylib' 2501 SLIBFLAGS = '-dynamiclib' 2502 elif sysname == 'Linux': 2503 CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS 2504 OS_DEFINES = '-D_LINUX_' 2505 SO_EXT = '.so' 2506 SLIBFLAGS = '-shared' 2507 SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS 2508 elif sysname == 'GNU': 2509 CXXFLAGS = '%s -D_HURD_' % CXXFLAGS 2510 OS_DEFINES = '-D_HURD_' 2511 SO_EXT = '.so' 2512 SLIBFLAGS = '-shared' 2513 elif sysname == 'DragonFly': 2514 CXXFLAGS = '%s -D_DRAGONFLY_' % CXXFLAGS 2515 OS_DEFINES = '-D_DRAGONFLY_' 2516 SO_EXT = '.so' 2517 SLIBFLAGS = '-shared' 2518 elif sysname == 'NetBSD': 2519 CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS 2520 OS_DEFINES = '-D_NETBSD_' 2521 SO_EXT = '.so' 2522 SLIBFLAGS = '-shared' 2523 elif sysname == 'OpenBSD': 2524 CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS 2525 OS_DEFINES = '-D_OPENBSD_' 2526 SO_EXT = '.so' 2527 SLIBFLAGS = '-shared' 2528 elif sysname == 'SunOS': 2529 CXXFLAGS = '%s -D_SUNOS_' % CXXFLAGS 2530 OS_DEFINES = '-D_SUNOS_' 2531 SO_EXT = '.so' 2532 SLIBFLAGS = '-shared' 2533 SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS 2534 elif sysname.startswith('CYGWIN'): 2535 CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS 2536 OS_DEFINES = '-D_CYGWIN' 2537 SO_EXT = '.dll' 2538 SLIBFLAGS = '-shared' 2539 elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): 2540 CXXFLAGS = '%s -D_MINGW' % CXXFLAGS 2541 OS_DEFINES = '-D_MINGW' 2542 SO_EXT = '.dll' 2543 SLIBFLAGS = '-shared' 2544 EXE_EXT = '.exe' 2545 LIB_EXT = '.lib' 2546 else: 2547 raise MKException('Unsupported platform: %s' % sysname) 2548 if is64(): 2549 if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): 2550 CXXFLAGS = '%s -fPIC' % CXXFLAGS 2551 if sysname == 'Linux': 2552 CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS 2553 elif not LINUX_X64: 2554 CXXFLAGS = '%s -m32' % CXXFLAGS 2555 LDFLAGS = '%s -m32' % LDFLAGS 2556 SLIBFLAGS = '%s -m32' % SLIBFLAGS 2557 if TRACE or DEBUG_MODE: 2558 CPPFLAGS = '%s -D_TRACE' % CPPFLAGS 2559 if is_cygwin_mingw(): 2560 # when cross-compiling with MinGW, we need to statically link its standard libraries 2561 # and to make it create an import library. 2562 SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS 2563 LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS 2564 if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'): 2565 CXXFLAGS = '%s -fpic' % CXXFLAGS 2566 2567 config.write('PREFIX=%s\n' % PREFIX) 2568 config.write('CC=%s\n' % CC) 2569 config.write('CXX=%s\n' % CXX) 2570 config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS)) 2571 config.write('CFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS.replace('-std=c++11', ''))) 2572 config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG) 2573 config.write('CXX_OUT_FLAG=-o \n') 2574 config.write('C_OUT_FLAG=-o \n') 2575 config.write('OBJ_EXT=.o\n') 2576 config.write('LIB_EXT=%s\n' % LIB_EXT) 2577 config.write('AR=%s\n' % AR) 2578 config.write('AR_FLAGS=rcs\n') 2579 config.write('AR_OUTFLAG=\n') 2580 config.write('EXE_EXT=%s\n' % EXE_EXT) 2581 config.write('LINK=%s\n' % CXX) 2582 config.write('LINK_FLAGS=\n') 2583 config.write('LINK_OUT_FLAG=-o \n') 2584 if is_linux() and (build_static_lib() or build_static_bin()): 2585 config.write('LINK_EXTRA_FLAGS=-Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive %s\n' % LDFLAGS) 2586 else: 2587 config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) 2588 config.write('SO_EXT=%s\n' % SO_EXT) 2589 config.write('SLINK=%s\n' % CXX) 2590 config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS) 2591 config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS) 2592 config.write('SLINK_OUT_FLAG=-o \n') 2593 config.write('OS_DEFINES=%s\n' % OS_DEFINES) 2594 if is_verbose(): 2595 print('Host platform: %s' % sysname) 2596 print('C++ Compiler: %s' % CXX) 2597 print('C Compiler : %s' % CC) 2598 if is_cygwin_mingw(): 2599 print('MinGW32 cross: %s' % (is_cygwin_mingw())) 2600 print('Archive Tool: %s' % AR) 2601 print('Arithmetic: %s' % ARITH) 2602 print('Prefix: %s' % PREFIX) 2603 print('64-bit: %s' % is64()) 2604 print('FP math: %s' % FPMATH) 2605 print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR) 2606 if GPROF: 2607 print('gprof: enabled') 2608 print('Python version: %s' % distutils.sysconfig.get_python_version()) 2609 if is_java_enabled(): 2610 print('JNI Bindings: %s' % JNI_HOME) 2611 print('Java Compiler: %s' % JAVAC) 2612 if is_ml_enabled(): 2613 print('OCaml Compiler: %s' % OCAMLC) 2614 print('OCaml Find tool: %s' % OCAMLFIND) 2615 print('OCaml Native: %s' % OCAMLOPT) 2616 print('OCaml Library: %s' % OCAML_LIB) 2617 if is_dotnet_core_enabled(): 2618 print('C# Compiler: %s' % DOTNET) 2619 2620 config.close() 2621 2622def mk_install(out): 2623 out.write('install: ') 2624 for c in get_components(): 2625 c.mk_install_deps(out) 2626 out.write(' ') 2627 out.write('\n') 2628 MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR) 2629 MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR) 2630 MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR) 2631 for c in get_components(): 2632 c.mk_install(out) 2633 out.write('\t@echo Z3 was successfully installed.\n') 2634 out.write('\n') 2635 2636def mk_uninstall(out): 2637 out.write('uninstall:\n') 2638 for c in get_components(): 2639 c.mk_uninstall(out) 2640 out.write('\t@echo Z3 was successfully uninstalled.\n') 2641 out.write('\n') 2642 2643# Generate the Z3 makefile 2644def mk_makefile(): 2645 mk_dir(BUILD_DIR) 2646 mk_config() 2647 if VERBOSE: 2648 print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile')) 2649 out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w') 2650 out.write('# Automatically generated file.\n') 2651 out.write('include config.mk\n') 2652 # Generate :all rule 2653 out.write('all:') 2654 for c in get_components(): 2655 if c.main_component(): 2656 out.write(' %s' % c.name) 2657 out.write('\n\t@echo Z3 was successfully built.\n') 2658 out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python')) 2659 pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH" 2660 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)) 2661 if not IS_WINDOWS: 2662 out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n") 2663 out.write('\t@echo " sudo make install"\n\n') 2664 # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n") 2665 # out.write('\t@echo " make DESTDIR=/some/temp/directory install"\n') 2666 # Generate :examples rule 2667 out.write('examples:') 2668 for c in get_components(): 2669 if c.is_example(): 2670 out.write(' _ex_%s' % c.name) 2671 out.write('\n\t@echo Z3 examples were successfully built.\n') 2672 # Generate components 2673 for c in get_components(): 2674 c.mk_makefile(out) 2675 # Generate install/uninstall rules if not WINDOWS 2676 if not IS_WINDOWS: 2677 mk_install(out) 2678 mk_uninstall(out) 2679 for c in get_components(): 2680 c.final_info() 2681 out.close() 2682 # Finalize 2683 if VERBOSE: 2684 print("Makefile was successfully generated.") 2685 if DEBUG_MODE: 2686 print(" compilation mode: Debug") 2687 else: 2688 print(" compilation mode: Release") 2689 if IS_WINDOWS: 2690 if VS_X64: 2691 print(" platform: x64\n") 2692 print("To build Z3, open a [Visual Studio x64 Command Prompt], then") 2693 elif VS_ARM: 2694 print(" platform: ARM\n") 2695 print("To build Z3, open a [Visual Studio ARM Command Prompt], then") 2696 else: 2697 print(" platform: x86") 2698 print("To build Z3, open a [Visual Studio Command Prompt], then") 2699 print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR)) 2700 print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"') 2701 else: 2702 print("Type 'cd %s; make' to build Z3" % BUILD_DIR) 2703 2704# Generate automatically generated source code 2705def mk_auto_src(): 2706 if not ONLY_MAKEFILES: 2707 exec_pyg_scripts() 2708 mk_pat_db() 2709 mk_all_install_tactic_cpps() 2710 mk_all_mem_initializer_cpps() 2711 mk_all_gparams_register_modules() 2712 2713 2714def _execfile(file, globals=globals(), locals=locals()): 2715 if sys.version < "2.7": 2716 execfile(file, globals, locals) 2717 else: 2718 with open(file, "r") as fh: 2719 exec(fh.read()+"\n", globals, locals) 2720 2721# Execute python auxiliary scripts that generate extra code for Z3. 2722def exec_pyg_scripts(): 2723 for root, dirs, files in os.walk('src'): 2724 for f in files: 2725 if f.endswith('.pyg'): 2726 script = os.path.join(root, f) 2727 generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root) 2728 if is_verbose(): 2729 print("Generated '{}'".format(generated_file)) 2730 2731# TODO: delete after src/ast/pattern/expr_pattern_match 2732# database.smt ==> database.h 2733def mk_pat_db(): 2734 c = get_component(PATTERN_COMPONENT) 2735 fin = os.path.join(c.src_dir, 'database.smt2') 2736 fout = os.path.join(c.src_dir, 'database.h') 2737 mk_genfile_common.mk_pat_db_internal(fin, fout) 2738 if VERBOSE: 2739 print("Generated '{}'".format(fout)) 2740 2741# Update version numbers 2742def update_version(): 2743 major = VER_MAJOR 2744 minor = VER_MINOR 2745 build = VER_BUILD 2746 revision = VER_TWEAK 2747 if major is None or minor is None or build is None or revision is None: 2748 raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()") 2749 if not ONLY_MAKEFILES: 2750 mk_version_dot_h(major, minor, build, revision) 2751 mk_all_assembly_infos(major, minor, build, revision) 2752 mk_def_files() 2753 2754def get_full_version_string(major, minor, build, revision): 2755 global GIT_HASH, GIT_DESCRIBE 2756 res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision) 2757 if GIT_HASH: 2758 res += " " + GIT_HASH 2759 if GIT_DESCRIBE: 2760 branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD']) 2761 res += " " + branch + " " + check_output(['git', 'describe']) 2762 return '"' + res + '"' 2763 2764# Update files with the version number 2765def mk_version_dot_h(major, minor, build, revision): 2766 c = get_component(UTIL_COMPONENT) 2767 version_template = os.path.join(c.src_dir, 'z3_version.h.in') 2768 version_header_output = os.path.join(c.src_dir, 'z3_version.h') 2769 # Note the substitution names are what is used by the CMake 2770 # builds system. If you change these you should change them 2771 # in the CMake build too 2772 configure_file(version_template, version_header_output, 2773 { 'Z3_VERSION_MAJOR': str(major), 2774 'Z3_VERSION_MINOR': str(minor), 2775 'Z3_VERSION_PATCH': str(build), 2776 'Z3_VERSION_TWEAK': str(revision), 2777 'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision) 2778 } 2779 ) 2780 if VERBOSE: 2781 print("Generated '%s'" % version_header_output) 2782 2783# Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template 2784def mk_all_assembly_infos(major, minor, build, revision): 2785 for c in get_components(): 2786 if c.has_assembly_info(): 2787 c.make_assembly_info(major, minor, build, revision) 2788 2789def get_header_files_for_components(component_src_dirs): 2790 assert isinstance(component_src_dirs, list) 2791 h_files_full_path = [] 2792 for component_src_dir in sorted(component_src_dirs): 2793 h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) 2794 h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) 2795 h_files_full_path.extend(h_files) 2796 return h_files_full_path 2797 2798def mk_install_tactic_cpp(cnames, path): 2799 component_src_dirs = [] 2800 for cname in cnames: 2801 print("Component %s" % cname) 2802 c = get_component(cname) 2803 component_src_dirs.append(c.src_dir) 2804 h_files_full_path = get_header_files_for_components(component_src_dirs) 2805 generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(h_files_full_path, path) 2806 if VERBOSE: 2807 print("Generated '{}'".format(generated_file)) 2808 2809def mk_all_install_tactic_cpps(): 2810 if not ONLY_MAKEFILES: 2811 for c in get_components(): 2812 if c.require_install_tactics(): 2813 cnames = [] 2814 cnames.extend(c.deps) 2815 cnames.append(c.name) 2816 mk_install_tactic_cpp(cnames, c.src_dir) 2817 2818def mk_mem_initializer_cpp(cnames, path): 2819 component_src_dirs = [] 2820 for cname in cnames: 2821 c = get_component(cname) 2822 component_src_dirs.append(c.src_dir) 2823 h_files_full_path = get_header_files_for_components(component_src_dirs) 2824 generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path) 2825 if VERBOSE: 2826 print("Generated '{}'".format(generated_file)) 2827 2828def mk_all_mem_initializer_cpps(): 2829 if not ONLY_MAKEFILES: 2830 for c in get_components(): 2831 if c.require_mem_initializer(): 2832 cnames = [] 2833 cnames.extend(c.deps) 2834 cnames.append(c.name) 2835 mk_mem_initializer_cpp(cnames, c.src_dir) 2836 2837def mk_gparams_register_modules(cnames, path): 2838 component_src_dirs = [] 2839 for cname in cnames: 2840 c = get_component(cname) 2841 component_src_dirs.append(c.src_dir) 2842 h_files_full_path = get_header_files_for_components(component_src_dirs) 2843 generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path) 2844 if VERBOSE: 2845 print("Generated '{}'".format(generated_file)) 2846 2847def mk_all_gparams_register_modules(): 2848 if not ONLY_MAKEFILES: 2849 for c in get_components(): 2850 if c.require_mem_initializer(): 2851 cnames = [] 2852 cnames.extend(c.deps) 2853 cnames.append(c.name) 2854 mk_gparams_register_modules(cnames, c.src_dir) 2855 2856# Generate a .def based on the files at c.export_files slot. 2857def mk_def_file(c): 2858 defname = '%s.def' % os.path.join(c.src_dir, c.name) 2859 dll_name = c.dll_name 2860 export_header_files = [] 2861 for dot_h in c.export_files: 2862 dot_h_c = c.find_file(dot_h, c.name) 2863 api = os.path.join(dot_h_c.src_dir, dot_h) 2864 export_header_files.append(api) 2865 mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files) 2866 if VERBOSE: 2867 print("Generated '%s'" % defname) 2868 2869def mk_def_files(): 2870 if not ONLY_MAKEFILES: 2871 for c in get_components(): 2872 if c.require_def_file(): 2873 mk_def_file(c) 2874 2875def cp_z3py_to_build(): 2876 mk_dir(BUILD_DIR) 2877 mk_dir(os.path.join(BUILD_DIR, 'python')) 2878 z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3') 2879 z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3') 2880 2881 # Erase existing .pyc files 2882 for root, dirs, files in os.walk(Z3PY_SRC_DIR): 2883 for f in files: 2884 if f.endswith('.pyc'): 2885 rmf(os.path.join(root, f)) 2886 # Compile Z3Py files 2887 if compileall.compile_dir(z3py_src, force=1) != 1: 2888 raise MKException("failed to compile Z3Py sources") 2889 if is_verbose: 2890 print("Generated python bytecode") 2891 # Copy sources to build 2892 mk_dir(z3py_dest) 2893 for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)): 2894 shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py)) 2895 if is_verbose(): 2896 print("Copied '%s'" % py) 2897 # Python 2.x support 2898 for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)): 2899 shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc)) 2900 if is_verbose(): 2901 print("Copied '%s'" % pyc) 2902 # Python 3.x support 2903 src_pycache = os.path.join(z3py_src, '__pycache__') 2904 target_pycache = os.path.join(z3py_dest, '__pycache__') 2905 if os.path.exists(src_pycache): 2906 for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)): 2907 mk_dir(target_pycache) 2908 shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc)) 2909 if is_verbose(): 2910 print("Copied '%s'" % pyc) 2911 # Copy z3test.py 2912 shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py')) 2913 2914def mk_bindings(api_files): 2915 if not ONLY_MAKEFILES: 2916 mk_z3consts_py(api_files) 2917 new_api_files = [] 2918 api = get_component(API_COMPONENT) 2919 for api_file in api_files: 2920 api_file_path = api.find_file(api_file, api.name) 2921 new_api_files.append(os.path.join(api_file_path.src_dir, api_file)) 2922 g = globals() 2923 g["API_FILES"] = new_api_files 2924 if is_java_enabled(): 2925 check_java() 2926 mk_z3consts_java(api_files) 2927 # Generate some of the bindings and "api" module files 2928 import update_api 2929 dotnet_output_dir = None 2930 if is_dotnet_core_enabled(): 2931 dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet') 2932 mk_dir(dotnet_output_dir) 2933 java_output_dir = None 2934 java_package_name = None 2935 if is_java_enabled(): 2936 java_output_dir = get_component('java').src_dir 2937 java_package_name = get_component('java').package_name 2938 ml_output_dir = None 2939 if is_ml_enabled(): 2940 ml_output_dir = get_component('ml').src_dir 2941 if is_js_enabled(): 2942 set_z3js_dir("api/js") 2943 js_output_dir = get_component('js').src_dir 2944 # Get the update_api module to do the work for us 2945 update_api.generate_files(api_files=new_api_files, 2946 api_output_dir=get_component('api').src_dir, 2947 z3py_output_dir=get_z3py_dir(), 2948 dotnet_output_dir=dotnet_output_dir, 2949 java_output_dir=java_output_dir, 2950 java_package_name=java_package_name, 2951 js_output_dir=get_z3js_dir(), 2952 ml_output_dir=ml_output_dir, 2953 ml_src_dir=ml_output_dir 2954 ) 2955 cp_z3py_to_build() 2956 if is_ml_enabled(): 2957 check_ml() 2958 mk_z3consts_ml(api_files) 2959 if is_dotnet_core_enabled(): 2960 check_dotnet_core() 2961 mk_z3consts_dotnet(api_files, dotnet_output_dir) 2962 2963# Extract enumeration types from API files, and add python definitions. 2964def mk_z3consts_py(api_files): 2965 if Z3PY_SRC_DIR is None: 2966 raise MKException("You must invoke set_z3py_dir(path):") 2967 full_path_api_files = [] 2968 api_dll = get_component(Z3_DLL_COMPONENT) 2969 for api_file in api_files: 2970 api_file_c = api_dll.find_file(api_file, api_dll.name) 2971 api_file = os.path.join(api_file_c.src_dir, api_file) 2972 full_path_api_files.append(api_file) 2973 generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) 2974 if VERBOSE: 2975 print("Generated '{}".format(generated_file)) 2976 2977# Extract enumeration types from z3_api.h, and add .Net definitions 2978def mk_z3consts_dotnet(api_files, output_dir): 2979 dotnet = get_component(DOTNET_COMPONENT) 2980 if not dotnet: 2981 dotnet = get_component(DOTNET_CORE_COMPONENT) 2982 full_path_api_files = [] 2983 for api_file in api_files: 2984 api_file_c = dotnet.find_file(api_file, dotnet.name) 2985 api_file = os.path.join(api_file_c.src_dir, api_file) 2986 full_path_api_files.append(api_file) 2987 generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir) 2988 if VERBOSE: 2989 print("Generated '{}".format(generated_file)) 2990 2991# Extract enumeration types from z3_api.h, and add Java definitions 2992def mk_z3consts_java(api_files): 2993 java = get_component(JAVA_COMPONENT) 2994 full_path_api_files = [] 2995 for api_file in api_files: 2996 api_file_c = java.find_file(api_file, java.name) 2997 api_file = os.path.join(api_file_c.src_dir, api_file) 2998 full_path_api_files.append(api_file) 2999 generated_files = mk_genfile_common.mk_z3consts_java_internal( 3000 full_path_api_files, 3001 java.package_name, 3002 java.src_dir) 3003 if VERBOSE: 3004 for generated_file in generated_files: 3005 print("Generated '{}'".format(generated_file)) 3006 3007# Extract enumeration types from z3_api.h, and add ML definitions 3008def mk_z3consts_ml(api_files): 3009 ml = get_component(ML_COMPONENT) 3010 full_path_api_files = [] 3011 for api_file in api_files: 3012 api_file_c = ml.find_file(api_file, ml.name) 3013 api_file = os.path.join(api_file_c.src_dir, api_file) 3014 full_path_api_files.append(api_file) 3015 generated_file = mk_genfile_common.mk_z3consts_ml_internal( 3016 full_path_api_files, 3017 ml.src_dir) 3018 if VERBOSE: 3019 print ('Generated "%s"' % generated_file) 3020 3021def mk_gui_str(id): 3022 return '4D2F40D8-E5F9-473B-B548-%012d' % id 3023 3024def get_platform_toolset_str(): 3025 default = 'v110'; 3026 vstr = check_output(['msbuild', '/ver']) 3027 lines = vstr.split('\n') 3028 lline = lines[-1] 3029 tokens = lline.split('.') 3030 if len(tokens) < 2: 3031 return default 3032 else: 3033 if tokens[0] == "15": 3034 # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141 3035 return "v141" 3036 else: 3037 return 'v' + tokens[0] + tokens[1] 3038 3039def mk_vs_proj_property_groups(f, name, target_ext, type): 3040 f.write(' <ItemGroup Label="ProjectConfigurations">\n') 3041 f.write(' <ProjectConfiguration Include="Debug|Win32">\n') 3042 f.write(' <Configuration>Debug</Configuration>\n') 3043 f.write(' <Platform>Win32</Platform>\n') 3044 f.write(' </ProjectConfiguration>\n') 3045 f.write(' <ProjectConfiguration Include="Release|Win32">\n') 3046 f.write(' <Configuration>Release</Configuration>\n') 3047 f.write(' <Platform>Win32</Platform>\n') 3048 f.write(' </ProjectConfiguration>\n') 3049 f.write(' </ItemGroup>\n') 3050 f.write(' <PropertyGroup Label="Globals">\n') 3051 f.write(' <ProjectGuid>{%s}</ProjectGuid>\n' % mk_gui_str(0)) 3052 f.write(' <ProjectName>%s</ProjectName>\n' % name) 3053 f.write(' <Keyword>Win32Proj</Keyword>\n') 3054 f.write(' <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str()) 3055 f.write(' </PropertyGroup>\n') 3056 f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n') 3057 f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n') 3058 f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type) 3059 f.write(' <CharacterSet>Unicode</CharacterSet>\n') 3060 f.write(' <UseOfMfc>false</UseOfMfc>\n') 3061 f.write(' </PropertyGroup>\n') 3062 f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n') 3063 f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type) 3064 f.write(' <CharacterSet>Unicode</CharacterSet>\n') 3065 f.write(' <UseOfMfc>false</UseOfMfc>\n') 3066 f.write(' </PropertyGroup>\n') 3067 f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n') 3068 f.write(' <ImportGroup Label="ExtensionSettings" />\n') 3069 f.write(' <ImportGroup Label="PropertySheets">\n') 3070 f.write(' <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n') 3071 f.write(' <PropertyGroup Label="UserMacros" />\n') 3072 f.write(' <PropertyGroup>\n') 3073 f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n') 3074 f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name) 3075 f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext) 3076 f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n') 3077 f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name) 3078 f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext) 3079 f.write(' </PropertyGroup>\n') 3080 f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n') 3081 f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n') 3082 f.write(' </PropertyGroup>\n') 3083 f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n') 3084 f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n') 3085 f.write(' </PropertyGroup>\n') 3086 3087 3088def mk_vs_proj_cl_compile(f, name, components, debug): 3089 f.write(' <ClCompile>\n') 3090 f.write(' <Optimization>Disabled</Optimization>\n') 3091 if debug: 3092 f.write(' <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n') 3093 else: 3094 f.write(' <PreprocessorDefinitions>WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n') 3095 if VS_PAR: 3096 f.write(' <MinimalRebuild>false</MinimalRebuild>\n') 3097 f.write(' <MultiProcessorCompilation>true</MultiProcessorCompilation>\n') 3098 else: 3099 f.write(' <MinimalRebuild>true</MinimalRebuild>\n') 3100 f.write(' <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n') 3101 f.write(' <WarningLevel>Level3</WarningLevel>\n') 3102 if debug: 3103 f.write(' <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n') 3104 else: 3105 f.write(' <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n') 3106 f.write(' <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n') 3107 f.write(' <AdditionalIncludeDirectories>') 3108 deps = find_all_deps(name, components) 3109 first = True 3110 for dep in deps: 3111 if first: 3112 first = False 3113 else: 3114 f.write(';') 3115 f.write(get_component(dep).to_src_dir) 3116 f.write(';%s\n' % os.path.join(REV_BUILD_DIR, SRC_DIR)) 3117 f.write('</AdditionalIncludeDirectories>\n') 3118 f.write(' </ClCompile>\n') 3119 3120def mk_vs_proj_dep_groups(f, name, components): 3121 f.write(' <ItemGroup>\n') 3122 deps = find_all_deps(name, components) 3123 for dep in deps: 3124 dep = get_component(dep) 3125 for cpp in filter(lambda f: f.endswith('.cpp'), os.listdir(dep.src_dir)): 3126 f.write(' <ClCompile Include="%s" />\n' % os.path.join(dep.to_src_dir, cpp)) 3127 f.write(' </ItemGroup>\n') 3128 3129def mk_vs_proj_link_exe(f, name, debug): 3130 f.write(' <Link>\n') 3131 f.write(' <OutputFile>$(OutDir)%s.exe</OutputFile>\n' % name) 3132 f.write(' <GenerateDebugInformation>true</GenerateDebugInformation>\n') 3133 f.write(' <SubSystem>Console</SubSystem>\n') 3134 f.write(' <StackReserveSize>8388608</StackReserveSize>\n') 3135 f.write(' <RandomizedBaseAddress>false</RandomizedBaseAddress>\n') 3136 f.write(' <DataExecutionPrevention/>\n') 3137 f.write(' <TargetMachine>MachineX86</TargetMachine>\n') 3138 f.write(' <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n') 3139 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') 3140 f.write(' </Link>\n') 3141 3142def mk_vs_proj(name, components): 3143 if not VS_PROJ: 3144 return 3145 proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name) 3146 modes=['Debug', 'Release'] 3147 PLATFORMS=['Win32'] 3148 f = open(proj_name, 'w') 3149 f.write('<?xml version="1.0" encoding="utf-8"?>\n') 3150 f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n') 3151 mk_vs_proj_property_groups(f, name, 'exe', 'Application') 3152 f.write(' <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n') 3153 mk_vs_proj_cl_compile(f, name, components, debug=True) 3154 mk_vs_proj_link_exe(f, name, debug=True) 3155 f.write(' </ItemDefinitionGroup>\n') 3156 f.write(' <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n') 3157 mk_vs_proj_cl_compile(f, name, components, debug=False) 3158 mk_vs_proj_link_exe(f, name, debug=False) 3159 f.write(' </ItemDefinitionGroup>\n') 3160 mk_vs_proj_dep_groups(f, name, components) 3161 f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n') 3162 f.write(' <ImportGroup Label="ExtensionTargets">\n') 3163 f.write(' </ImportGroup>\n') 3164 f.write('</Project>\n') 3165 f.close() 3166 if is_verbose(): 3167 print("Generated '%s'" % proj_name) 3168 3169def mk_vs_proj_link_dll(f, name, debug): 3170 f.write(' <Link>\n') 3171 f.write(' <OutputFile>$(OutDir)%s.dll</OutputFile>\n' % name) 3172 f.write(' <GenerateDebugInformation>true</GenerateDebugInformation>\n') 3173 f.write(' <SubSystem>Console</SubSystem>\n') 3174 f.write(' <StackReserveSize>8388608</StackReserveSize>\n') 3175 f.write(' <RandomizedBaseAddress>false</RandomizedBaseAddress>\n') 3176 f.write(' <DataExecutionPrevention/>\n') 3177 f.write(' <TargetMachine>MachineX86</TargetMachine>\n') 3178 f.write(' <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n') 3179 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') 3180 f.write(' <ModuleDefinitionFile>%s</ModuleDefinitionFile>' % os.path.join(get_component('api_dll').to_src_dir, 'api_dll.def')) 3181 f.write(' </Link>\n') 3182 3183def mk_vs_proj_dll(name, components): 3184 if not VS_PROJ: 3185 return 3186 proj_name = '%s.vcxproj' % os.path.join(BUILD_DIR, name) 3187 modes=['Debug', 'Release'] 3188 PLATFORMS=['Win32'] 3189 f = open(proj_name, 'w') 3190 f.write('<?xml version="1.0" encoding="utf-8"?>\n') 3191 f.write('<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n') 3192 mk_vs_proj_property_groups(f, name, 'dll', 'DynamicLibrary') 3193 f.write(' <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n') 3194 mk_vs_proj_cl_compile(f, name, components, debug=True) 3195 mk_vs_proj_link_dll(f, name, debug=True) 3196 f.write(' </ItemDefinitionGroup>\n') 3197 f.write(' <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n') 3198 mk_vs_proj_cl_compile(f, name, components, debug=False) 3199 mk_vs_proj_link_dll(f, name, debug=False) 3200 f.write(' </ItemDefinitionGroup>\n') 3201 mk_vs_proj_dep_groups(f, name, components) 3202 f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n') 3203 f.write(' <ImportGroup Label="ExtensionTargets">\n') 3204 f.write(' </ImportGroup>\n') 3205 f.write('</Project>\n') 3206 f.close() 3207 if is_verbose(): 3208 print("Generated '%s'" % proj_name) 3209 3210def mk_win_dist(build_path, dist_path): 3211 for c in get_components(): 3212 c.mk_win_dist(build_path, dist_path) 3213 3214def mk_unix_dist(build_path, dist_path): 3215 for c in get_components(): 3216 c.mk_unix_dist(build_path, dist_path) 3217 # Add Z3Py to bin directory 3218 for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)): 3219 shutil.copy(os.path.join(build_path, pyc), 3220 os.path.join(dist_path, INSTALL_BIN_DIR, pyc)) 3221 3222class MakeRuleCmd(object): 3223 """ 3224 These class methods provide a convenient way to emit frequently 3225 needed commands used in Makefile rules 3226 Note that several of the method are meant for use during ``make 3227 install`` and ``make uninstall``. These methods correctly use 3228 ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable 3229 to writing commands manually which can be error prone. 3230 """ 3231 @classmethod 3232 def install_root(cls): 3233 """ 3234 Returns a string that will expand to the 3235 install location when used in a makefile rule. 3236 """ 3237 # Note: DESTDIR is to support staged installs 3238 return "$(DESTDIR)$(PREFIX)/" 3239 3240 @classmethod 3241 def _is_str(cls, obj): 3242 if sys.version_info.major > 2: 3243 # Python 3 or newer. Strings are always unicode and of type str 3244 return isinstance(obj, str) 3245 else: 3246 # Python 2. Has byte-string and unicode representation, allow both 3247 return isinstance(obj, str) or isinstance(obj, unicode) 3248 3249 @classmethod 3250 def _install_root(cls, path, in_prefix, out, is_install=True): 3251 if not in_prefix: 3252 # The Python bindings on OSX are sometimes not installed inside the prefix. 3253 install_root = "$(DESTDIR)" 3254 action_string = 'install' if is_install else 'uninstall' 3255 cls.write_cmd(out, 'echo "WARNING: {}ing files/directories ({}) that are not in the install prefix ($(PREFIX))."'.format( 3256 action_string, path)) 3257 #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format( 3258 # action_string, 'to' if is_install else 'from', path, PREFIX)) 3259 else: 3260 # assert not os.path.isabs(path) 3261 install_root = cls.install_root() 3262 return install_root 3263 3264 @classmethod 3265 def install_files(cls, out, src_pattern, dest, in_prefix=True): 3266 assert len(dest) > 0 3267 assert cls._is_str(src_pattern) 3268 assert not ' ' in src_pattern 3269 assert cls._is_str(dest) 3270 assert not ' ' in dest 3271 assert not os.path.isabs(src_pattern) 3272 install_root = cls._install_root(dest, in_prefix, out) 3273 3274 cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format( 3275 src_pattern=src_pattern, 3276 install_root=install_root, 3277 dest=dest)) 3278 3279 @classmethod 3280 def remove_installed_files(cls, out, pattern, in_prefix=True): 3281 assert len(pattern) > 0 3282 assert cls._is_str(pattern) 3283 assert not ' ' in pattern 3284 install_root = cls._install_root(pattern, in_prefix, out, is_install=False) 3285 3286 cls.write_cmd(out, "rm -f {install_root}{pattern}".format( 3287 install_root=install_root, 3288 pattern=pattern)) 3289 3290 @classmethod 3291 def make_install_directory(cls, out, dir, in_prefix=True): 3292 assert len(dir) > 0 3293 assert cls._is_str(dir) 3294 assert not ' ' in dir 3295 install_root = cls._install_root(dir, in_prefix, out) 3296 3297 if is_windows(): 3298 cls.write_cmd(out, "IF NOT EXIST {dir} (mkdir {dir})".format( 3299 install_root=install_root, 3300 dir=dir)) 3301 else: 3302 cls.write_cmd(out, "mkdir -p {install_root}{dir}".format( 3303 install_root=install_root, 3304 dir=dir)) 3305 3306 @classmethod 3307 def _is_path_prefix_of(cls, temp_path, target_as_abs): 3308 """ 3309 Returns True iff ``temp_path`` is a path prefix 3310 of ``target_as_abs`` 3311 """ 3312 assert cls._is_str(temp_path) 3313 assert cls._is_str(target_as_abs) 3314 assert len(temp_path) > 0 3315 assert len(target_as_abs) > 0 3316 assert os.path.isabs(temp_path) 3317 assert os.path.isabs(target_as_abs) 3318 3319 # Need to stick extra slash in front otherwise we might think that 3320 # ``/lib`` is a prefix of ``/lib64``. Of course if ``temp_path == 3321 # '/'`` then we shouldn't else we would check if ``//`` (rather than 3322 # ``/``) is a prefix of ``/lib64``, which would fail. 3323 if len(temp_path) > 1: 3324 temp_path += os.sep 3325 return target_as_abs.startswith(temp_path) 3326 3327 @classmethod 3328 def create_relative_symbolic_link(cls, out, target, link_name): 3329 assert cls._is_str(target) 3330 assert cls._is_str(link_name) 3331 assert len(target) > 0 3332 assert len(link_name) > 0 3333 assert not os.path.isabs(target) 3334 assert not os.path.isabs(link_name) 3335 3336 # We can't test to see if link_name is a file or directory 3337 # because it may not exist yet. Instead follow the convention 3338 # that if there is a leading slash target is a directory otherwise 3339 # it's a file 3340 if link_name[-1] != '/': 3341 # link_name is a file 3342 temp_path = os.path.dirname(link_name) 3343 else: 3344 # link_name is a directory 3345 temp_path = link_name[:-1] 3346 temp_path = '/' + temp_path 3347 relative_path = "" 3348 targetAsAbs = '/' + target 3349 assert os.path.isabs(targetAsAbs) 3350 assert os.path.isabs(temp_path) 3351 # Keep walking up the directory tree until temp_path 3352 # is a prefix of targetAsAbs 3353 while not cls._is_path_prefix_of(temp_path, targetAsAbs): 3354 assert temp_path != '/' 3355 temp_path = os.path.dirname(temp_path) 3356 relative_path += '../' 3357 3358 # Now get the path from the common prefix directory to the target 3359 target_from_prefix = targetAsAbs[len(temp_path):] 3360 relative_path += target_from_prefix 3361 # Remove any double slashes 3362 relative_path = relative_path.replace('//','/') 3363 cls.create_symbolic_link(out, relative_path, link_name) 3364 3365 @classmethod 3366 def create_symbolic_link(cls, out, target, link_name): 3367 assert cls._is_str(target) 3368 assert cls._is_str(link_name) 3369 assert not os.path.isabs(target) 3370 3371 cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format( 3372 target=target, 3373 install_root=cls.install_root(), 3374 link_name=link_name)) 3375 3376 # TODO: Refactor all of the build system to emit commands using this 3377 # helper to simplify code. This will also let us replace ``@`` with 3378 # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on 3379 # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This 3380 # would be very helpful for debugging. 3381 @classmethod 3382 def write_cmd(cls, out, line): 3383 out.write("\t@{}\n".format(line)) 3384 3385def strip_path_prefix(path, prefix): 3386 if path.startswith(prefix): 3387 stripped_path = path[len(prefix):] 3388 stripped_path.replace('//','/') 3389 if stripped_path[0] == '/': 3390 stripped_path = stripped_path[1:] 3391 assert not os.path.isabs(stripped_path) 3392 return stripped_path 3393 else: 3394 return path 3395 3396def configure_file(template_file_path, output_file_path, substitutions): 3397 """ 3398 Read a template file ``template_file_path``, perform substitutions 3399 found in the ``substitutions`` dictionary and write the result to 3400 the output file ``output_file_path``. 3401 The template file should contain zero or more template strings of the 3402 form ``@NAME@``. 3403 The substitutions dictionary maps old strings (without the ``@`` 3404 symbols) to their replacements. 3405 """ 3406 assert isinstance(template_file_path, str) 3407 assert isinstance(output_file_path, str) 3408 assert isinstance(substitutions, dict) 3409 assert len(template_file_path) > 0 3410 assert len(output_file_path) > 0 3411 print("Generating {} from {}".format(output_file_path, template_file_path)) 3412 3413 if not os.path.exists(template_file_path): 3414 raise MKException('Could not find template file "{}"'.format(template_file_path)) 3415 3416 # Read whole template file into string 3417 template_string = None 3418 with open(template_file_path, 'r') as f: 3419 template_string = f.read() 3420 3421 # Do replacements 3422 for (old_string, replacement) in substitutions.items(): 3423 template_string = template_string.replace('@{}@'.format(old_string), replacement) 3424 3425 # Write the string to the file 3426 with open(output_file_path, 'w') as f: 3427 f.write(template_string) 3428 3429if __name__ == '__main__': 3430 import doctest 3431 doctest.testmod() 3432