-
Notifications
You must be signed in to change notification settings - Fork 1.5k
/
mk_util.py
3469 lines (3068 loc) · 137 KB
/
mk_util.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
############################################
# Copyright (c) 2012 Microsoft Corporation
#
# Auxiliary scripts for generating Makefiles
# and Visual Studio project files.
#
# Author: Leonardo de Moura (leonardo)
############################################
import io
import sys
import os
import re
import getopt
import shutil
from mk_exception import *
import mk_genfile_common
from fnmatch import fnmatch
import distutils.sysconfig
import compileall
import subprocess
def getenv(name, default):
try:
return os.environ[name].strip(' "\'')
except:
return default
CXX=getenv("CXX", None)
CC=getenv("CC", None)
CPPFLAGS=getenv("CPPFLAGS", "")
CXXFLAGS=getenv("CXXFLAGS", "")
AR=getenv("AR", "ar")
EXAMP_DEBUG_FLAG=''
LDFLAGS=getenv("LDFLAGS", "")
JNI_HOME=getenv("JNI_HOME", None)
OCAMLC=getenv("OCAMLC", "ocamlc")
OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
OCAML_LIB=getenv("OCAML_LIB", None)
OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
DOTNET="dotnet"
# Standard install directories relative to PREFIX
INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig'))
CXX_COMPILERS=['g++', 'clang++']
C_COMPILERS=['gcc', 'clang']
JAVAC=None
JAR=None
PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
BUILD_DIR='build'
REV_BUILD_DIR='..'
SRC_DIR='src'
EXAMPLE_DIR='examples'
# Required Components
Z3_DLL_COMPONENT='api_dll'
PATTERN_COMPONENT='pattern'
UTIL_COMPONENT='util'
API_COMPONENT='api'
DOTNET_COMPONENT='dotnet'
DOTNET_CORE_COMPONENT='dotnet'
JAVA_COMPONENT='java'
ML_COMPONENT='ml'
CPP_COMPONENT='cpp'
PYTHON_COMPONENT='python'
#####################
IS_WINDOWS=False
IS_LINUX=False
IS_HURD=False
IS_OSX=False
IS_FREEBSD=False
IS_NETBSD=False
IS_OPENBSD=False
IS_SUNOS=False
IS_CYGWIN=False
IS_CYGWIN_MINGW=False
IS_MSYS2=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
VS_X64 = False
VS_ARM = False
LINUX_X64 = True
ONLY_MAKEFILES = False
Z3PY_SRC_DIR=None
Z3JS_SRC_DIR=None
VS_PROJ = False
TRACE = False
PYTHON_ENABLED=False
DOTNET_CORE_ENABLED=False
DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
JAVA_ENABLED=False
ML_ENABLED=False
JS_ENABLED=False
PYTHON_INSTALL_ENABLED=False
STATIC_LIB=False
STATIC_BIN=False
VER_MAJOR=None
VER_MINOR=None
VER_BUILD=None
VER_TWEAK=None
PREFIX=sys.prefix
GMP=False
VS_PAR=False
VS_PAR_NUM=8
GPROF=False
GIT_HASH=False
GIT_DESCRIBE=False
SLOW_OPTIMIZE=False
LOG_SYNC=False
SINGLE_THREADED=False
GUARD_CF=False
ALWAYS_DYNAMIC_BASE=False
FPMATH="Default"
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
def check_output(cmd):
out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
if out != None:
enc = sys.stdout.encoding
if enc != None: return out.decode(enc).rstrip('\r\n')
else: return out.rstrip('\r\n')
else:
return ""
def git_hash():
try:
branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
except:
raise MKException("Failed to retrieve git hash")
ls = r.split(' ')
if len(ls) != 2:
raise MKException("Unexpected git output " + r)
return ls[0]
def is_windows():
return IS_WINDOWS
def is_linux():
return IS_LINUX
def is_hurd():
return IS_HURD
def is_freebsd():
return IS_FREEBSD
def is_netbsd():
return IS_NETBSD
def is_openbsd():
return IS_OPENBSD
def is_sunos():
return IS_SUNOS
def is_osx():
return IS_OSX
def is_cygwin():
return IS_CYGWIN
def is_cygwin_mingw():
return IS_CYGWIN_MINGW
def is_msys2():
return IS_MSYS2
def norm_path(p):
return os.path.expanduser(os.path.normpath(p))
def which(program):
import os
def is_exe(fpath):
return os.path.isfile(fpath) and os.access(fpath, os.X_OK)
fpath, fname = os.path.split(program)
if fpath:
if is_exe(program):
return program
else:
for path in getenv("PATH", "").split(os.pathsep):
exe_file = os.path.join(path, program)
if is_exe(exe_file):
return exe_file
return None
class TempFile:
def __init__(self, name):
try:
self.name = name
self.fname = open(name, 'w')
except:
raise MKException("Failed to create temporary file '%s'" % self.name)
def add(self, s):
self.fname.write(s)
def commit(self):
self.fname.close()
def __del__(self):
self.fname.close()
try:
os.remove(self.name)
except:
pass
def exec_cmd(cmd):
if isinstance(cmd, str):
cmd = cmd.split(' ')
new_cmd = []
first = True
for e in cmd:
if first:
first = False
new_cmd.append(e)
else:
if e != "":
se = e.split(' ')
if len(se) > 1:
for e2 in se:
if e2 != "":
new_cmd.append(e2)
else:
new_cmd.append(e)
cmd = new_cmd
null = open(os.devnull, 'wb')
try:
return subprocess.call(cmd, stdout=null, stderr=null)
except:
# Failed to create process
return 1
finally:
null.close()
# rm -f fname
def rmf(fname):
if os.path.exists(fname):
os.remove(fname)
def exec_compiler_cmd(cmd):
r = exec_cmd(cmd)
if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
rmf('a.exe')
else:
rmf('a.out')
return r
def test_cxx_compiler(cc):
if is_verbose():
print("Testing %s..." % cc)
t = TempFile('tst.cpp')
t.add('#include<iostream>\nint main() { return 0; }\n')
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, CXXFLAGS, 'tst.cpp', LDFLAGS]) == 0
def test_c_compiler(cc):
if is_verbose():
print("Testing %s..." % cc)
t = TempFile('tst.c')
t.add('#include<stdio.h>\nint main() { return 0; }\n')
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, 'tst.c', LDFLAGS]) == 0
def test_gmp(cc):
if is_verbose():
print("Testing GMP...")
t = TempFile('tstgmp.cpp')
t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
def test_fpmath(cc):
global FPMATH_FLAGS
if is_verbose():
print("Testing floating point support...")
t = TempFile('tstsse.cpp')
t.add('int main() { return 42; }\n')
t.commit()
# -Werror is needed because some versions of clang warn about unrecognized
# -m flags.
if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
return "SSE2-GCC"
elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
FPMATH_FLAGS="-msse -msse2"
return "SSE2-CLANG"
elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
return "ARM-VFP"
else:
FPMATH_FLAGS=""
return "UNKNOWN"
def find_jni_h(path):
for root, dirs, files in os.walk(path):
for f in files:
if f == 'jni.h':
return root
return False
def check_java():
global JNI_HOME
global JAVAC
global JAR
JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.
if is_verbose():
print("Finding javac ...")
if JDK_HOME is not None:
if IS_WINDOWS:
JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe')
else:
JAVAC = os.path.join(JDK_HOME, 'bin', 'javac')
if not os.path.exists(JAVAC):
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))
else:
# Search for javac in the path.
ind = 'javac'
if IS_WINDOWS:
ind = ind + '.exe'
paths = os.getenv('PATH', None)
if paths:
spaths = paths.split(os.pathsep)
for i in range(0, len(spaths)):
cmb = os.path.join(spaths[i], ind)
if os.path.exists(cmb):
JAVAC = cmb
break
if JAVAC is None:
raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.')
if is_verbose():
print("Finding jar ...")
if IS_WINDOWS:
JAR = os.path.join(os.path.dirname(JAVAC), 'jar.exe')
else:
JAR = os.path.join(os.path.dirname(JAVAC), 'jar')
if not os.path.exists(JAR):
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))
if is_verbose():
print("Testing %s..." % JAVAC)
t = TempFile('Hello.java')
t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
t.commit()
oo = TempFile('output')
eo = TempFile('errout')
try:
subprocess.call([JAVAC, 'Hello.java', '-verbose', '-source', '1.8', '-target', '1.8' ], stdout=oo.fname, stderr=eo.fname)
oo.commit()
eo.commit()
except:
raise MKException('Found, but failed to run Java compiler at %s' % (JAVAC))
os.remove('Hello.class')
if is_verbose():
print("Finding jni.h...")
if JNI_HOME is not None:
if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
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))
else:
# Search for jni.h in the library directories...
t = open('errout', 'r')
open_pat = re.compile("\[search path for class files: (.*)\]")
cdirs = []
for line in t:
m = open_pat.match(line)
if m:
libdirs = m.group(1).split(',')
for libdir in libdirs:
q = os.path.dirname(libdir)
if cdirs.count(q) == 0 and len(q) > 0:
cdirs.append(q)
t.close()
# ... plus some heuristic ones.
extra_dirs = []
# For the libraries, even the JDK usually uses a JRE that comes with it. To find the
# headers we have to go a little bit higher up.
for dir in cdirs:
extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))
if IS_OSX: # Apparently Apple knows best where to put stuff...
extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')
cdirs[len(cdirs):] = extra_dirs
for dir in cdirs:
q = find_jni_h(dir)
if q is not False:
JNI_HOME = q
if JNI_HOME is None:
raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
def test_csc_compiler(c):
t = TempFile('hello.cs')
t.add('public class hello { public static void Main() {} }')
t.commit()
if is_verbose():
print ('Testing %s...' % c)
r = exec_cmd([c, 'hello.cs'])
try:
rmf('hello.cs')
rmf('hello.exe')
except:
pass
return r == 0
def check_dotnet_core():
if not IS_WINDOWS:
return
r = exec_cmd([DOTNET, '--help'])
if r != 0:
raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities')
def check_ml():
t = TempFile('hello.ml')
t.add('print_string "Hello world!\n";;')
t.commit()
if is_verbose():
print ('Testing %s...' % OCAMLC)
r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
if r != 0:
raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
if is_verbose():
print ('Testing %s...' % OCAMLOPT)
r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
if r != 0:
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.')
try:
rmf('hello.cmi')
rmf('hello.cmo')
rmf('hello.cmx')
rmf('a.out')
rmf('hello.o')
except:
pass
find_ml_lib()
find_ocaml_find()
def find_ocaml_find():
global OCAMLFIND
if is_verbose():
print ("Testing %s..." % OCAMLFIND)
r = exec_cmd([OCAMLFIND, 'printconf'])
if r != 0:
OCAMLFIND = ''
def find_ml_lib():
global OCAML_LIB
if is_verbose():
print ('Finding OCAML_LIB...')
t = TempFile('output')
null = open(os.devnull, 'wb')
try:
subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
t.commit()
except:
raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
finally:
null.close()
t = open('output', 'r')
for line in t:
OCAML_LIB = line[:-1]
if is_verbose():
print ('OCAML_LIB=%s' % OCAML_LIB)
t.close()
rmf('output')
return
def is64():
global LINUX_X64
if is_sunos() and sys.version_info.major < 3:
return LINUX_X64
else:
return LINUX_X64 and sys.maxsize >= 2**32
def check_ar():
if is_verbose():
print("Testing ar...")
if which(AR) is None:
raise MKException('%s (archive tool) was not found' % AR)
def find_cxx_compiler():
global CXX, CXX_COMPILERS
if CXX is not None:
if test_cxx_compiler(CXX):
return CXX
for cxx in CXX_COMPILERS:
if test_cxx_compiler(cxx):
CXX = cxx
return CXX
raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
def find_c_compiler():
global CC, C_COMPILERS
if CC is not None:
if test_c_compiler(CC):
return CC
for c in C_COMPILERS:
if test_c_compiler(c):
CC = c
return CC
raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
def set_version(major, minor, build, revision):
global VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK, GIT_DESCRIBE
VER_MAJOR = major
VER_MINOR = minor
VER_BUILD = build
VER_TWEAK = revision
if GIT_DESCRIBE:
branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
def get_version():
return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
def get_version_string(n):
if n == 3:
return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD)
return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_TWEAK)
def build_static_lib():
return STATIC_LIB
def build_static_bin():
return STATIC_BIN
def is_cr_lf(fname):
# Check whether text files use cr/lf
f = open(fname, 'r')
line = f.readline()
f.close()
sz = len(line)
return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n'
# dos2unix in python
# cr/lf --> lf
def dos2unix(fname):
if is_cr_lf(fname):
fin = open(fname, 'r')
fname_new = '%s.new' % fname
fout = open(fname_new, 'w')
for line in fin:
line = line.rstrip('\r\n')
fout.write(line)
fout.write('\n')
fin.close()
fout.close()
shutil.move(fname_new, fname)
if is_verbose():
print("dos2unix '%s'" % fname)
def dos2unix_tree():
for root, dirs, files in os.walk('src'):
for f in files:
dos2unix(os.path.join(root, f))
def check_eol():
if not IS_WINDOWS:
# Linux/OSX/BSD check if the end-of-line is cr/lf
if is_cr_lf('LICENSE.txt'):
if is_verbose():
print("Fixing end of line...")
dos2unix_tree()
if os.name == 'nt':
IS_WINDOWS=True
# Visual Studio already displays the files being compiled
SHOW_CPPS=False
elif os.name == 'posix':
if os.uname()[0] == 'Darwin':
IS_OSX=True
elif os.uname()[0] == 'Linux':
IS_LINUX=True
elif os.uname()[0] == 'GNU':
IS_HURD=True
elif os.uname()[0] == 'FreeBSD':
IS_FREEBSD=True
elif os.uname()[0] == 'NetBSD':
IS_NETBSD=True
elif os.uname()[0] == 'OpenBSD':
IS_OPENBSD=True
elif os.uname()[0] == 'SunOS':
IS_SUNOS=True
elif os.uname()[0][:6] == 'CYGWIN':
IS_CYGWIN=True
if (CC != None and "mingw" in CC):
IS_CYGWIN_MINGW=True
elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
IS_MSYS2=True
if os.uname()[4] == 'x86_64':
LINUX_X64=True
else:
LINUX_X64=False
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
print("This script generates the Makefile for the Z3 theorem prover.")
print("It must be executed from the Z3 root directory.")
print("\nOptions:")
print(" -h, --help display this message.")
print(" -s, --silent do not print verbose messages.")
if not IS_WINDOWS:
print(" -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX)
else:
print(" --parallel=num use cl option /MP with 'num' parallel processes")
print(" --pypkgdir=<dir> Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
print(" -b <subdir>, --build=<subdir> subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
print(" --githash=hash include the given hash in the binaries.")
print(" --git-describe include the output of 'git describe' in the version information.")
print(" -d, --debug compile Z3 in debug mode.")
print(" -t, --trace enable tracing in release mode.")
if IS_WINDOWS:
print(" --guardcf enable Control Flow Guard runtime checks.")
print(" -x, --x64 create 64 binary when using Visual Studio.")
else:
print(" --x86 force 32-bit x86 build on x64 systems.")
print(" -m, --makefiles generate only makefiles.")
if IS_WINDOWS:
print(" -v, --vsproj generate Visual Studio Project Files.")
print(" --optimize generate optimized code during linking.")
print(" --dotnet generate .NET platform bindings.")
print(" --dotnet-key=<file> sign the .NET assembly using the private key in <file>.")
print(" --java generate Java bindings.")
print(" --ml generate OCaml bindings.")
print(" --js generate JScript bindings.")
print(" --python generate Python bindings.")
print(" --staticlib build Z3 static library.")
print(" --staticbin build a statically linked Z3 binary.")
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
print(" --log-sync synchronize access to API log files to enable multi-thread API logging.")
print(" --single-threaded non-thread-safe build")
print("")
print("Some influential environment variables:")
if not IS_WINDOWS:
print(" CXX C++ compiler")
print(" CC C compiler")
print(" LDFLAGS Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
print(" CPPFLAGS Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
print(" CXXFLAGS C++ compiler flags")
print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)")
print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)")
print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)")
print(" OCAMLFIND Ocaml find tool (only relevant with --ml)")
print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)")
print(" OCAML_LIB Ocaml library directory (only relevant with --ml)")
print(" Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
print(" Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
print(" Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
print(" Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
exit(exit_code)
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
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
global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
global GUARD_CF, ALWAYS_DYNAMIC_BASE
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
except:
print("ERROR: Invalid command line option")
display_help(1)
for opt, arg in options:
print('opt = %s, arg = %s' % (opt, arg))
if opt in ('-b', '--build'):
if arg == 'src':
raise MKException('The src directory should not be used to host the Makefile')
set_build_dir(arg)
elif opt in ('-s', '--silent'):
VERBOSE = False
elif opt in ('-d', '--debug'):
DEBUG_MODE = True
elif opt in ('-x', '--x64'):
if not IS_WINDOWS:
raise MKException('x64 compilation mode can only be specified when using Visual Studio')
VS_X64 = True
elif opt in ('--x86'):
LINUX_X64=False
elif opt in ('-h', '--help'):
display_help(0)
elif opt in ('-m', '--makefiles'):
ONLY_MAKEFILES = True
elif opt in ('-c', '--showcpp'):
SHOW_CPPS = True
elif opt in ('-v', '--vsproj'):
VS_PROJ = True
elif opt in ('-t', '--trace'):
TRACE = True
elif opt in ('--dotnet',):
DOTNET_CORE_ENABLED = True
elif opt in ('--dotnet-key'):
DOTNET_KEY_FILE = arg
elif opt in ('--staticlib'):
STATIC_LIB = True
elif opt in ('--staticbin'):
STATIC_BIN = True
elif opt in ('--optimize'):
SLOW_OPTIMIZE = True
elif not IS_WINDOWS and opt in ('-p', '--prefix'):
PREFIX = arg
elif opt in ('--pypkgdir'):
PYTHON_PACKAGE_DIR = arg
elif IS_WINDOWS and opt == '--parallel':
VS_PAR = True
VS_PAR_NUM = int(arg)
elif opt in ('-g', '--gmp'):
GMP = True
elif opt in ('-j', '--java'):
JAVA_ENABLED = True
elif opt == '--gprof':
GPROF = True
elif opt == '--githash':
GIT_HASH=arg
elif opt == '--git-describe':
GIT_DESCRIBE = True
elif opt in ('', '--ml'):
ML_ENABLED = True
elif opt == "--js":
JS_ENABLED = True
elif opt in ('', '--log-sync'):
LOG_SYNC = True
elif opt == '--single-threaded':
SINGLE_THREADED = True
elif opt in ('--python'):
PYTHON_ENABLED = True
PYTHON_INSTALL_ENABLED = True
elif opt == '--guardcf':
GUARD_CF = True
ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE
else:
print("ERROR: Invalid command line option '%s'" % opt)
display_help(1)
# Return a list containing a file names included using '#include' in
# the given C/C++ file named fname.
def extract_c_includes(fname):
result = {}
# We look for well behaved #include directives
std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
# We should generate and error for any occurrence of #include that does not match the previous pattern.
non_std_inc_pat = re.compile(".*#include.*")
f = io.open(fname, encoding='utf-8', mode='r')
linenum = 1
for line in f:
m1 = std_inc_pat.match(line)
if m1:
root_file_name = m1.group(1)
slash_pos = root_file_name.rfind('/')
if slash_pos >= 0 and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src"
# print(root_file_name)
root_file_name = root_file_name[slash_pos+1:]
result[root_file_name] = m1.group(1)
elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
linenum = linenum + 1
f.close()
return result
# Given a path dir1/subdir2/subdir3 returns ../../..
def reverse_path(p):
# Filter out empty components (e.g. will have one if path ends in a slash)
l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
n = len(l)
r = '..'
for i in range(1, n):
r = os.path.join(r, '..')
return r
def mk_dir(d):
if not os.path.exists(d):
os.makedirs(d)
def set_build_dir(d):
global BUILD_DIR, REV_BUILD_DIR
BUILD_DIR = norm_path(d)
REV_BUILD_DIR = reverse_path(d)
def set_z3js_dir(p):
global SRC_DIR, Z3JS_SRC_DIR
p = norm_path(p)
full = os.path.join(SRC_DIR, p)
if not os.path.exists(full):
raise MKException("Python bindings directory '%s' does not exist" % full)
Z3JS_SRC_DIR = full
if VERBOSE:
print("Js bindings directory was detected.")
def set_z3py_dir(p):
global SRC_DIR, Z3PY_SRC_DIR
p = norm_path(p)
full = os.path.join(SRC_DIR, p)
if not os.path.exists(full):
raise MKException("Python bindings directory '%s' does not exist" % full)
Z3PY_SRC_DIR = full
if VERBOSE:
print("Python bindings directory was detected.")
_UNIQ_ID = 0
def mk_fresh_name(prefix):
global _UNIQ_ID
r = '%s_%s' % (prefix, _UNIQ_ID)
_UNIQ_ID = _UNIQ_ID + 1
return r
_Id = 0
_Components = []
_ComponentNames = set()
_Name2Component = {}
_Processed_Headers = set()
# Return the Component object named name
def get_component(name):
return _Name2Component[name]
def get_components():
return _Components
# Return the directory where the python bindings are located.
def get_z3py_dir():
return Z3PY_SRC_DIR
# Return directory where the js bindings are located
def get_z3js_dir():
return Z3JS_SRC_DIR
# Return true if in verbose mode
def is_verbose():
return VERBOSE
def is_java_enabled():
return JAVA_ENABLED
def is_ml_enabled():
return ML_ENABLED
def is_js_enabled():
return JS_ENABLED
def is_dotnet_core_enabled():
return DOTNET_CORE_ENABLED
def is_python_enabled():
return PYTHON_ENABLED
def is_python_install_enabled():
return PYTHON_INSTALL_ENABLED
def is_compiler(given, expected):
"""
Return True if the 'given' compiler is the expected one.
>>> is_compiler('g++', 'g++')
True
>>> is_compiler('/home/g++', 'g++')
True
>>> is_compiler(os.path.join('home', 'g++'), 'g++')
True
>>> is_compiler('clang++', 'g++')
False
>>> is_compiler(os.path.join('home', 'clang++'), 'clang++')
True
"""
if given == expected:
return True
if len(expected) < len(given):
return given[len(given) - len(expected) - 1] == os.sep and given[len(given) - len(expected):] == expected
return False
def is_CXX_gpp():
return is_compiler(CXX, 'g++')
def is_clang_in_gpp_form(cc):
str = check_output([cc, '--version'])
try:
version_string = str.encode('utf-8')
except:
version_string = str
clang = 'clang'.encode('utf-8')
return version_string.find(clang) != -1
def is_CXX_clangpp():
if is_compiler(CXX, 'g++'):
return is_clang_in_gpp_form(CXX)
return is_compiler(CXX, 'clang++')
def get_files_with_ext(path, ext):
return filter(lambda f: f.endswith(ext), os.listdir(path))
def get_cpp_files(path):
return get_files_with_ext(path,'.cpp')
def get_c_files(path):
return get_files_with_ext(path,'.c')
def get_cs_files(path):
return get_files_with_ext(path,'.cs')
def get_java_files(path):
return get_files_with_ext(path,'.java')
def get_ml_files(path):
return get_files_with_ext(path,'.ml')
def find_all_deps(name, deps):
new_deps = []
for dep in deps:
if dep in _ComponentNames:
if not (dep in new_deps):
new_deps.append(dep)
for dep_dep in get_component(dep).deps:
if not (dep_dep in new_deps):
new_deps.append(dep_dep)
else:
raise MKException("Unknown component '%s' at '%s'." % (dep, name))
return new_deps
class Component:
def __init__(self, name, path, deps):
global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
if name in _ComponentNames:
raise MKException("Component '%s' was already defined." % name)
if path is None:
path = name
self.name = name
path = norm_path(path)
self.path = path
self.deps = find_all_deps(name, deps)
self.build_dir = path
self.src_dir = os.path.join(SRC_DIR, path)
self.to_src_dir = os.path.join(REV_BUILD_DIR, self.src_dir)
def get_link_name(self):
return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)'
# Find fname in the include paths for the given component.
# ownerfile is only used for creating error messages.
# That is, we were looking for fname when processing ownerfile
def find_file(self, fname, ownerfile, orig_include=None):
full_fname = os.path.join(self.src_dir, fname)
# Store all our possible locations
possibilities = set()
# If the our file exists in the current directory, then we store it
if os.path.exists(full_fname):
# We cannot return here, as we might have files with the same
# basename, but different include paths
possibilities.add(self)
for dep in self.deps:
c_dep = get_component(dep)
full_fname = os.path.join(c_dep.src_dir, fname)
if os.path.exists(full_fname):
possibilities.add(c_dep)
if possibilities:
# We have ambiguity
if len(possibilities) > 1: