macOS-related notes #44
Vassiliy-Kudryashov
started this conversation in
Ideas
Replies: 2 comments 4 replies
-
I guess it’s quite ok. @nikitavlaev can take care. |
Beta Was this translation helpful? Give feedback.
0 replies
-
How to link libz3java.dylib to libz3.dylib statically using z3 sources:
CXX=clang++ CC=clang python scripts/mk_make.py
cd build; make
make libz3.dylib Output will look like this: clang++ -o libz3.dylib -dynamiclib api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_special_relations.o api/api_algebraic.o api/api_tactic.o api/api_ast.o api/api_context.o api/api_qe.o api/api_log.o api/api_pb.o api/api_polynomial.o api/api_goal.o api/api_rcf.o api/api_seq.o api/api_bv.o api/api_stats.o api/api_config_params.o api/api_solver.o api/api_quant.o api/api_params.o api/api_numeral.o api/api_parsers.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a solver/assertions/solver_assertions.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a smt/params/smt_params.a params/params.a ast/euf/euf.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread
cp libz3.dylib python
libtool -static -o libz3.a api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_special_relations.o api/api_algebraic.o api/api_tactic.o api/api_ast.o api/api_context.o api/api_qe.o api/api_log.o api/api_pb.o api/api_polynomial.o api/api_goal.o api/api_rcf.o api/api_seq.o api/api_bv.o api/api_stats.o api/api_config_params.o api/api_solver.o api/api_quant.o api/api_params.o api/api_numeral.o api/api_parsers.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a solver/assertions/solver_assertions.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a smt/params/smt_params.a params/params.a ast/euf/euf.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a
make libz3java.dylib Output will look like this: clang++ -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -std=c++17 -fvisibility=hidden -fvisibility-inlines-hidden -c -mfpmath=sse -msse -msse2 -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC -o api/java/Native.o -I"/Library/Java/JavaVirtualMachines/jdk-11.jdk/Contents/Home/include" -I"/Library/Java/JavaVirtualMachines/jdk-11.jdk/Contents/Home/include/darwin" -I../src/api ../src/api/java/Native.cpp
clang++ -o libz3java.dylib -dynamiclib api/java/Native.o libz3.dylib
clang++ -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -std=c++17 -fvisibility=hidden -fvisibility-inlines-hidden -c -mfpmath=sse -msse -msse2 -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC -o api/java/Native.o -I"/Library/Java/JavaVirtualMachines/jdk-11.jdk/Contents/Home/include" -I"/Library/Java/JavaVirtualMachines/jdk-11.jdk/Contents/Home/include/darwin" -I../src/api ../src/api/java/Native.cpp
clang++ -o libz3java.dylib libz3.a -dynamiclib api/java/Native.o
$ otool -L libz3java.dylib
libz3java.dylib:
libz3java.dylib (compatibility version 0.0.0, current version 0.0.0)
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 800.6.0)
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1281.0.0) |
Beta Was this translation helpful? Give feedback.
4 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
In utbot-analytycs/build.gradle
System.getProperty('os.name')
returns "mac" in case of macOS 12.3.1Actual name should be "macosx" to get some JARs from maven repository.
Suggested patch:
String classifier = System.getProperty('os.name').toLowerCase().split()[0] + "-x86_64"
should be replaced with
Runtime exception No1:
java.lang.ExceptionInInitializerError
at org.utbot.engine.pc.UtContextInitializer.(UtSolver.kt:279)
at org.utbot.engine.UtBotSymbolicEngine.(UtBotSymbolicEngine.kt:299)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator.generateAsync(UtBotTestCaseGenerator.kt:173)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3$1$1.invokeSuspend(UtBotTestCaseGenerator.kt:249)
at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33)
at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106)
at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:274)
at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:84)
at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59)
at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source)
at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38)
at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source)
at org.utbot.common.ConcurrencyKt.runBlockingWithCancellationPredicate(Concurrency.kt:38)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3.invoke(UtBotTestCaseGenerator.kt:241)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3.invoke(UtBotTestCaseGenerator.kt:55)
at org.utbot.common.ConcurrencyKt.runIgnoringCancellationException(Concurrency.kt:47)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator.generateForSeveralMethods(UtBotTestCaseGenerator.kt:240)
at org.utbot.intellij.plugin.generator.CodeGenerator.generateForSeveralMethods(CodeGenerator.kt:53)
at org.utbot.intellij.plugin.ui.UtTestsDialogProcessor$createTests$2$1.run(UtTestsDialogProcessor.kt:164)
at com.intellij.openapi.progress.impl.CoreProgressManager$TaskRunnable.run(CoreProgressManager.java:935)
at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcessWithProgressAsync$5(CoreProgressManager.java:442)
at com.intellij.openapi.progress.impl.ProgressRunner.lambda$submit$3(ProgressRunner.java:235)
at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcess$2(CoreProgressManager.java:170)
at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:629)
at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:581)
at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:60)
at com.intellij.openapi.progress.impl.CoreProgressManager.runProcess(CoreProgressManager.java:157)
at com.intellij.openapi.progress.impl.ProgressRunner.lambda$submit$4(ProgressRunner.java:235)
at java.base/java.util.concurrent.CompletableFuture$AsyncSupply.run(CompletableFuture.java:1700)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
at java.base/java.security.AccessController.doPrivileged(Native Method)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
at java.base/java.lang.Thread.run(Thread.java:834)
Caused by: java.lang.IllegalArgumentException: Not supported arch: x86_64
at org.utbot.engine.z3.Z3Initializer$Companion$initializeCallback$2.invoke(Z3initializer.kt:27)
at org.utbot.engine.z3.Z3Initializer$Companion$initializeCallback$2.invoke(Z3initializer.kt:20)
at kotlin.SynchronizedLazyImpl.getValue(LazyJVM.kt:74)
at org.utbot.engine.z3.Z3Initializer$Companion.getInitializeCallback(Z3initializer.kt)
at org.utbot.engine.z3.Z3Initializer$Companion.access$getInitializeCallback$p(Z3initializer.kt:20)
at org.utbot.engine.z3.Z3Initializer.(Z3initializer.kt:65)
... 36 more
Runtime exception No2:
java.lang.NoClassDefFoundError: Could not initialize class org.utbot.engine.pc.UtContextInitializer$1
at org.utbot.engine.pc.UtContextInitializer.(UtSolver.kt:279)
at org.utbot.engine.UtBotSymbolicEngine.(UtBotSymbolicEngine.kt:299)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator.generateAsync(UtBotTestCaseGenerator.kt:173)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3$1$1.invokeSuspend(UtBotTestCaseGenerator.kt:249)
at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33)
at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106)
at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:274)
at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:84)
at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59)
at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source)
at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38)
at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source)
at org.utbot.common.ConcurrencyKt.runBlockingWithCancellationPredicate(Concurrency.kt:38)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3.invoke(UtBotTestCaseGenerator.kt:241)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator$generateForSeveralMethods$3.invoke(UtBotTestCaseGenerator.kt:55)
at org.utbot.common.ConcurrencyKt.runIgnoringCancellationException(Concurrency.kt:47)
at org.utbot.framework.plugin.api.UtBotTestCaseGenerator.generateForSeveralMethods(UtBotTestCaseGenerator.kt:240)
at org.utbot.intellij.plugin.generator.CodeGenerator.generateForSeveralMethods(CodeGenerator.kt:53)
at org.utbot.intellij.plugin.ui.UtTestsDialogProcessor$createTests$2$1.run(UtTestsDialogProcessor.kt:164)
at com.intellij.openapi.progress.impl.CoreProgressManager$TaskRunnable.run(CoreProgressManager.java:935)
at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcessWithProgressAsync$5(CoreProgressManager.java:442)
at com.intellij.openapi.progress.impl.ProgressRunner.lambda$submit$3(ProgressRunner.java:235)
at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcess$2(CoreProgressManager.java:170)
at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:629)
at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:581)
at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:60)
at com.intellij.openapi.progress.impl.CoreProgressManager.runProcess(CoreProgressManager.java:157)
at com.intellij.openapi.progress.impl.ProgressRunner.lambda$submit$4(ProgressRunner.java:235)
at java.base/java.util.concurrent.CompletableFuture$AsyncSupply.run(CompletableFuture.java:1700)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
at java.base/java.security.AccessController.doPrivileged(Native Method)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
at java.base/java.lang.Thread.run(Thread.java:834)
Beta Was this translation helpful? Give feedback.
All reactions