From c781d274fbaf6f4b3e419140c5834511d6b7c7a0 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 18 May 2021 01:18:23 -0500 Subject: [PATCH] Add Solver.java to the Java API (#6196) PR changes: Add Solver.java and relation JNI c files Update FindJUnit to download JUnit5 Add Java unit tests --- cmake/FindJUnit.cmake | 62 +++++++---- src/api/java/CMakeLists.txt | 101 ++++++++++++++++-- src/api/java/cvc5/CVC5ApiException.java | 24 +++++ .../cvc5/CVC5ApiRecoverableException.java | 25 +++++ src/api/java/cvc5/IPointer.java | 21 ++++ src/api/java/cvc5/Solver.java | 61 +++++++++++ src/api/java/cvc5/Utils.java | 35 ++++++ src/api/java/genkinds.py.in | 1 + src/api/java/jni/cvc5JavaApi.h | 38 +++++++ src/api/java/jni/cvc5_Solver.cpp | 63 +++++++++++ test/unit/api/CMakeLists.txt | 3 + test/unit/api/java/CMakeLists.txt | 60 +++++++++++ test/unit/api/java/cvc5/SolverTest.java | 44 ++++++++ 13 files changed, 510 insertions(+), 28 deletions(-) create mode 100644 src/api/java/cvc5/CVC5ApiException.java create mode 100644 src/api/java/cvc5/CVC5ApiRecoverableException.java create mode 100644 src/api/java/cvc5/IPointer.java create mode 100644 src/api/java/cvc5/Solver.java create mode 100644 src/api/java/cvc5/Utils.java create mode 100644 src/api/java/jni/cvc5JavaApi.h create mode 100644 src/api/java/jni/cvc5_Solver.cpp create mode 100644 test/unit/api/java/CMakeLists.txt create mode 100644 test/unit/api/java/cvc5/SolverTest.java diff --git a/cmake/FindJUnit.cmake b/cmake/FindJUnit.cmake index caa2c3eb9..1532042a4 100644 --- a/cmake/FindJUnit.cmake +++ b/cmake/FindJUnit.cmake @@ -1,6 +1,6 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner +# Mathias Preiner, Mudathir Mohamed # # This file is part of the cvc5 project. # @@ -11,29 +11,53 @@ # ############################################################################# # # Find JUnit -# JUnit_FOUND - system has JUnit lib -# JUnit_JAR - JUnit jar file -# JUnit_JAR_DEPS - JUnit jar dependencies +# JUnit_FOUND - should be true for testing +# JUnit_JAR - absolute path to JUnit5 jar file ## -find_package(Java REQUIRED) -include(UseJava) -find_package(Hamcrest REQUIRED) +include(deps-helper) -find_jar(JUnit_JAR NAMES junit junit4) +find_jar(JUnit_JAR junit-platform-console-standalone + PATHS + ${DEPS_BASE}/share/java + $ENV{PATH} $ENV{HOME} $ENV{CLASSPATH} $ENV{JUNIT_HOME} +) +set(JUnit_FOUND_SYSTEM FALSE) if(JUnit_JAR) - set(JUnit_JAR_DEPS ${Hamcrest_JAR}) - # Determine version of JUnit - execute_process( - COMMAND ${Java_JAVA_EXECUTABLE} -cp ${JUnit_JAR} junit.runner.Version - OUTPUT_VARIABLE JUnit_VERSION - OUTPUT_STRIP_TRAILING_WHITESPACE) + set(JUnit_FOUND_SYSTEM TRUE) endif() -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(JUnit - REQUIRED_VARS JUnit_JAR JUnit_JAR_DEPS - VERSION_VAR JUnit_VERSION) +if(NOT JUnit_FOUND_SYSTEM) + check_auto_download("JUnit" "") + set(JUNIT_VERSION 1.7.1) + include(ExternalProject) -mark_as_advanced(JUnit_JAR JUnit_JAR_DEPS) + # Download junit generator jar + ExternalProject_Add( + JUnit-EP-jar + PREFIX ${DEPS_PREFIX} + URL https://repo1.maven.org/maven2/org/junit/platform/junit-platform-console-standalone/${JUNIT_VERSION}/junit-platform-console-standalone-${JUNIT_VERSION}.jar + URL_HASH SHA1=99245bde65d028a8b8ff604be26e929ab6ff2e58 + DOWNLOAD_NO_EXTRACT ON + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy + /../junit-platform-console-standalone-${JUNIT_VERSION}.jar + /share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar + BUILD_BYPRODUCTS /share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar + ) + + set(JUnit_JAR "${DEPS_BASE}/share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar") +endif() + +set(JUnit_FOUND TRUE) + +mark_as_advanced(JUnit_JAR) +mark_as_advanced(JUnit_FOUND) + +if(JUnit_FOUND_SYSTEM) + message(STATUS "Found JUnit: ${JUnit_JAR}") +else() + message(STATUS "Downloading JUnit: ${JUnit_JAR}") +endif() \ No newline at end of file diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 51d44c822..d56f594ce 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -13,21 +13,104 @@ # The build system configuration. ## -# create a directory for the cvc package -file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc") +# create directories +file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5") +set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/jni") +file(MAKE_DIRECTORY ${JNI_DIR}) -# Generate cvc/Kind.java +# Generate cvc5/Kind.java configure_file(genkinds.py.in genkinds.py) -add_custom_target( - gen-java-kinds - ALL + +set(JAVA_KIND_FILE + "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind.java" +) + +add_custom_command( + OUTPUT + ${JAVA_KIND_FILE} + BYPRODUCTS + ${JAVA_KIND_FILE} COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc/Kind" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - COMMENT - "Generate Kind.java" + "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" +) + +add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) + +# find java +find_package(Java COMPONENTS Development REQUIRED) +include(UseJava) + +# specify java source files +set(JAVA_FILES + ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiException.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiRecoverableException.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/IPointer.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Solver.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java + ${JAVA_KIND_FILE} +) + +# specify generated jni headers +set(JNI_HEADERS + ${JNI_DIR}/cvc5_Solver.h +) + +# generate jni headers +add_custom_command( + OUTPUT + ${JNI_HEADERS} + BYPRODUCTS + ${JNI_HEADERS} + COMMAND + # generate jni header files + ${Java_JAVAC_EXECUTABLE} -h ${JNI_DIR} ${JAVA_FILES} -d ${JNI_DIR} + DEPENDS + ${JAVA_FILES} + COMMENT "Generate jni headers" + VERBATIM ) + +add_custom_target(generate-jni-headers DEPENDS ${JNI_HEADERS}) +add_dependencies(generate-jni-headers generate-java-kinds) + +# find jni package +find_package(JNI REQUIRED) +message(STATUS "JAVA_AWT_LIBRARY : ${JAVA_AWT_LIBRARY}") +message(STATUS "JNI_INCLUDE_DIRS : ${JNI_INCLUDE_DIRS}") +message(STATUS "JNI_LIBRARIES : ${JNI_LIBRARIES} ") +message(STATUS "JNI_FOUND : ${JNI_FOUND}") +message(STATUS "JAVA_AWT_LIBRARY : ${JAVA_AWT_LIBRARY}") +message(STATUS "JAVA_JVM_LIBRARY : ${JAVA_JVM_LIBRARY}") +message(STATUS "JAVA_INCLUDE_PATH : ${JAVA_INCLUDE_PATH}") +message(STATUS "JAVA_INCLUDE_PATH2 : ${JAVA_INCLUDE_PATH2}") +message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}") + +add_library(cvc5jni SHARED jni/cvc5_Solver.cpp) +add_dependencies(cvc5jni generate-jni-headers) + +target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS}) +target_include_directories(cvc5jni PUBLIC ${PROJECT_SOURCE_DIR}/src) +target_include_directories(cvc5jni PUBLIC ${CMAKE_BINARY_DIR}/src/) +target_include_directories(cvc5jni PUBLIC ${JNI_DIR}) +target_link_libraries(cvc5jni PRIVATE ${JNI_LIBRARIES}) +target_link_libraries(cvc5jni PRIVATE cvc5) + +set(CVC5_JAR "cvc5-${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}.jar") + +# create cvc5.jar file +add_jar(cvc5jar + SOURCES + ${JAVA_FILES} + VERSION ${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE} + OUTPUT_NAME cvc5 +) + +add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5) + +get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE) \ No newline at end of file diff --git a/src/api/java/cvc5/CVC5ApiException.java b/src/api/java/cvc5/CVC5ApiException.java new file mode 100644 index 000000000..8b8b61198 --- /dev/null +++ b/src/api/java/cvc5/CVC5ApiException.java @@ -0,0 +1,24 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +public class CVC5ApiException extends Exception +{ + public CVC5ApiException(String message) + { + super(message); + } +} diff --git a/src/api/java/cvc5/CVC5ApiRecoverableException.java b/src/api/java/cvc5/CVC5ApiRecoverableException.java new file mode 100644 index 000000000..3f434d0ff --- /dev/null +++ b/src/api/java/cvc5/CVC5ApiRecoverableException.java @@ -0,0 +1,25 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + + +package cvc5; + +public class CVC5ApiRecoverableException extends CVC5ApiException +{ + public CVC5ApiRecoverableException(String message) + { + super(message); + } +} diff --git a/src/api/java/cvc5/IPointer.java b/src/api/java/cvc5/IPointer.java new file mode 100644 index 000000000..fc9c95338 --- /dev/null +++ b/src/api/java/cvc5/IPointer.java @@ -0,0 +1,21 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +interface IPointer +{ + long getPointer(); +} diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java new file mode 100644 index 000000000..6bb1b6b1e --- /dev/null +++ b/src/api/java/cvc5/Solver.java @@ -0,0 +1,61 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +import java.io.IOException; + +public class Solver implements IPointer +{ + private final long pointer; + + public long getPointer() + { + return pointer; + } + + public Solver() + { + this.pointer = newSolver(); + } + + private native long newSolver(); + + public void deletePointer() + { + deletePointer(pointer); + } + + private static native void deletePointer(long solverPointer); + + static + { + Utils.loadLibraries(); + } + + /** + * Set logic. + * SMT-LIB: ( set-logic ) + * + * @param logic + * @throws CVC5ApiException + */ + public void setLogic(String logic) throws CVC5ApiException + { + setLogic(pointer, logic); + } + + private native void setLogic(long solverPointer, String logic) throws CVC5ApiException; +} diff --git a/src/api/java/cvc5/Utils.java b/src/api/java/cvc5/Utils.java new file mode 100644 index 000000000..7f32932e4 --- /dev/null +++ b/src/api/java/cvc5/Utils.java @@ -0,0 +1,35 @@ + +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +import java.io.IOException; + +class Utils +{ + static + { + loadLibraries(); + } + + /** + * load cvc5 jni library + */ + public static void loadLibraries() + { + System.loadLibrary("cvc5jni"); + } +} diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in index 89cf6e3de..15de21805 100644 --- a/src/api/java/genkinds.py.in +++ b/src/api/java/genkinds.py.in @@ -23,6 +23,7 @@ import sys import re + # get access to cvc5/src/api/parsekinds.py sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api')) diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h new file mode 100644 index 000000000..2aa860f40 --- /dev/null +++ b/src/api/java/jni/cvc5JavaApi.h @@ -0,0 +1,38 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#ifndef CVC5__JAVA_API_H +#define CVC5__JAVA_API_H + +#define CVC5_JAVA_API_TRY_CATCH_BEGIN \ + try \ + { +#define CVC5_JAVA_API_TRY_CATCH_END(env) \ + } \ + catch (const CVC5ApiRecoverableException& e) \ + { \ + jclass exceptionClass = \ + env->FindClass("cvc5/CVC5ApiRecoverableException"); \ + env->ThrowNew(exceptionClass, e.what()); \ + } \ + catch (const CVC5ApiException& e) \ + { \ + jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \ + env->ThrowNew(exceptionClass, e.what()); \ + } +#define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \ + CVC5_JAVA_API_TRY_CATCH_END(env) \ + return returnValue; +#endif // CVC5__JAVA_API_H diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp new file mode 100644 index 000000000..9d7690e59 --- /dev/null +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -0,0 +1,63 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#include "cvc5_Solver.h" + +#include "api/cpp/cvc5.h" +#include "cvc5JavaApi.h" + +using namespace cvc5::api; + +/* + * Class: cvc5_Solver + * Method: newSolver + * Signature: ()J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_newSolver(JNIEnv*, jobject) +{ + Solver* solver = new Solver(); + return ((jlong)solver); +} + +/* + * Class: cvc5_Solver + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_deletePointer(JNIEnv*, + jclass, + jlong pointer) +{ + delete ((Solver*)pointer); +} + +/* + * Class: cvc5_Solver + * Method: setLogic + * Signature: (Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_setLogic(JNIEnv* env, + jobject, + jlong solverPointer, + jstring jLogic) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = (Solver*)solverPointer; + const char* cLogic = env->GetStringUTFChars(jLogic, nullptr); + solver->setLogic(std::string(cLogic)); + + CVC5_JAVA_API_TRY_CATCH_END(env); +} diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index c01b1cfe0..ae6db51ef 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -24,3 +24,6 @@ cvc5_add_unit_test_white(solver_white api) cvc5_add_unit_test_black(sort_black api) cvc5_add_unit_test_black(term_black api) cvc5_add_unit_test_white(term_white api) +if (BUILD_BINDINGS_JAVA) + add_subdirectory(java) +endif() diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt new file mode 100644 index 000000000..0ef649b87 --- /dev/null +++ b/test/unit/api/java/CMakeLists.txt @@ -0,0 +1,60 @@ +############################################################################### +# Top contributors (to current version): +# Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. +## + +find_package(Java REQUIRED) +include(UseJava) +find_package(JUnit REQUIRED) + +# specify source files for junit tests +set(java_test_src_files + ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SolverTest.java +) + +# build junit tests +add_custom_target( + build-junit-tests + ALL + COMMAND + ${Java_JAVAC_EXECUTABLE} ${java_test_src_files} + -cp ${JUnit_JAR}:${CVC5_JAR_PATH} # add JUnit and cvc5 jar files to the class path + -d . # specify the output directory for the generated .class files + COMMENT "Build junit tests" + VERBATIM +) + +# make sure junit jar file is present +add_dependencies(build-junit-tests JUnit-EP-jar) +# make sure cvc.jar file is built first +add_dependencies(build-junit-tests cvc5jar) + +get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY) + +# run junit tests +add_custom_target( + run-junit-tests + ALL + COMMAND + # run junit tests + ${Java_JAVA_EXECUTABLE} + -Djava.library.path=${CVC5_JNI_PATH} + -jar ${JUnit_JAR} + -cp ${JUnit_JAR}:${CVC5_JAR_PATH}:. + -select-package cvc5 + COMMENT "Run junit tests" + VERBATIM +) + +add_dependencies(run-junit-tests build-junit-tests) +add_dependencies(units run-junit-tests) \ No newline at end of file diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java new file mode 100644 index 000000000..57758ff88 --- /dev/null +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -0,0 +1,44 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of the Solver class of the Java API. + */ + + +package cvc5; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class SolverTest +{ + private Solver d_solver; + + @BeforeEach void setUp() + { + d_solver = new Solver(); + } + + @AfterEach void tearDown() + { + d_solver.deletePointer(); + } + + @Test void setLogic() + { + assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA")); + assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV")); + } +} -- 2.30.2