From a374f7b577b48908d623cf7b64594f1c98cfb8b7 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sat, 20 Mar 2021 05:23:44 -0500 Subject: [PATCH] Generate cvc/Kind.java for the java API (#6143) PR changes: Refactor python/genkinds.py by separating parsing from file generation. Add java/genkinds.py to generate file Kind.java. Enable java API in ./configure.sh with "under development" warning. --- CMakeLists.txt | 4 +- cmake/CVC4Config.cmake.in | 10 +- configure.sh | 4 +- examples/CMakeLists.txt | 4 +- src/api/java/CMakeLists.txt | 28 ++++++ src/api/java/genkinds.py | 113 ++++++++++++++++++++++ src/api/parsekinds.py | 158 ++++++++++++++++++++++++++++++ src/api/python/genkinds.py | 187 +++++++----------------------------- 8 files changed, 345 insertions(+), 163 deletions(-) create mode 100644 src/api/java/CMakeLists.txt create mode 100644 src/api/java/genkinds.py create mode 100644 src/api/parsekinds.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 843fc16c1..1bbe6d288 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -565,8 +565,8 @@ if(BUILD_BINDINGS_PYTHON) endif() if(BUILD_BINDINGS_JAVA) - message(FATAL_ERROR - "Java bindings for the new API are not implemented yet.") + add_subdirectory(src/api/java) + message(WARNING "Java API is currently under development.") endif() #-----------------------------------------------------------------------------# diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in index 38cd4ba8d..ac6bccb20 100644 --- a/cmake/CVC4Config.cmake.in +++ b/cmake/CVC4Config.cmake.in @@ -18,7 +18,9 @@ if(NOT TARGET CVC4::cvc4) include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake) endif() -if(CVC4_BINDINGS_JAVA AND NOT TARGET CVC4::cvc4jar) - set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@") - include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake) -endif() +# TODO(project wishue #83): enable these lines +# if(CVC4_BINDINGS_JAVA AND NOT TARGET CVC4::cvc4jar) +# set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@") +# include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake) +# endif() + diff --git a/configure.sh b/configure.sh index ed84a7270..d57bcd5d5 100755 --- a/configure.sh +++ b/configure.sh @@ -295,7 +295,9 @@ do --java-bindings) java_bindings=ON;; --no-java-bindings) java_bindings=OFF;; - --all-bindings) python_bindings=ON;; + --all-bindings) + python_bindings=ON + java_bindings=ON;; --valgrind) valgrind=ON;; --no-valgrind) valgrind=OFF;; diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 7022aa674..4f7f1332f 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -96,8 +96,8 @@ if(TARGET CVC4::cvc4jar) # -Djava.library.path=${CVC4_JNI_PATH} # SimpleVC # ) - - add_subdirectory(api/java) + # TODO(project wishue #83): enable java examples + # add_subdirectory(api/java) endif() if(CVC4_BINDINGS_PYTHON) diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt new file mode 100644 index 000000000..9c25e7393 --- /dev/null +++ b/src/api/java/CMakeLists.txt @@ -0,0 +1,28 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Mudathir Mohamed +## This file is part of the CVC4 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. +## + +# create a directory for the cvc package +file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc") + +# Generate cvc/Kind.java +add_custom_target( + gen-java-kinds + ALL + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" + --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc/Kind" + DEPENDS + genkinds.py + COMMENT + "Generate Kind.java" +) diff --git a/src/api/java/genkinds.py b/src/api/java/genkinds.py new file mode 100644 index 000000000..955e47bae --- /dev/null +++ b/src/api/java/genkinds.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python +# +# genkinds.py +# Top contributors (to current version): +# Mudathir Mohamed +# This file is part of the CVC4 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. +# + +""" +This script reads CVC4/src/api/cvc4cppkind.h and generates +cvc/Kind.java file which declare all the CVC4 kinds. +""" + +import argparse +import os +import sys + +# the following command in CVC4/build/src/api/java/CMakeFiles/gen-java-kinds.dir/build.make +# cd CVC4/build/src/api/java && /usr/bin/python3 CVC4/src/api/java/genkinds.py ... +# indicates we are in directory CVC4/build/src/api/java +# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py +sys.path.insert(0, os.path.abspath('../../../../src/api')) + +from parsekinds import * + +# Default Filenames +DEFAULT_PREFIX = 'Kind' + +# Code Blocks + +KINDS_JAVA_TOP = \ + r"""package cvc; + +import java.util.HashMap; +import java.util.Map; + +public enum Kind +{ +""" + +KINDS_JAVA_BOTTOM = \ + r"""; + + /* the int value of the kind */ + private int value; + private static Map kindMap = new HashMap<>(); + private Kind(int value) + { + this.value = value; + } + + static + { + for (Kind kind : Kind.values()) + { + kindMap.put(kind.getValue(), kind); + } + } + + public static Kind fromInt(int value) throws CVCApiException + { + if (value < INTERNAL_KIND.value || value > LAST_KIND.value) + { + throw new CVCApiException("Kind value " + value + " is outside the valid range [" + + INTERNAL_KIND.value + "," + LAST_KIND.value + "]"); + } + return kindMap.get(value); + } + + public int getValue() + { + return value; + } +} +""" + + +# Files generation + +def gen_java(parser: KindsParser, filename): + f = open(filename, "w") + code = KINDS_JAVA_TOP + enum_value = -2 # initial enum value + for kind, name in parser.kinds.items(): + code += " {name}({enum_value}),\n".format(name=kind, enum_value=enum_value) + enum_value = enum_value + 1 + code += KINDS_JAVA_BOTTOM + f.write(code) + f.close() + + +if __name__ == "__main__": + parser = argparse.ArgumentParser('Read a kinds header file and generate a ' + 'corresponding java file') + parser.add_argument('--kinds-header', metavar='', + help='The header file to read kinds from', + default=DEFAULT_HEADER) + parser.add_argument('--kinds-file-prefix', metavar='', + help='The prefix for the generated .java file', + default=DEFAULT_PREFIX) + + args = parser.parse_args() + kinds_header = args.kinds_header + kinds_file_prefix = args.kinds_file_prefix + + kp = KindsParser() + kp.parse(kinds_header) + + gen_java(kp, kinds_file_prefix + ".java") diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py new file mode 100644 index 000000000..0b86d8cec --- /dev/null +++ b/src/api/parsekinds.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python +##################### +## genkinds.py +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 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. +## + +""" +This script implements KindsParser which +parses the header file CVC4/src/api/cvc4cppkind.h + +The script is aware of the '#if 0' pattern and will ignore +kinds declared between '#if 0' and '#endif'. It can also +handle nested '#if 0' pairs. +""" + +from collections import OrderedDict + +#################### Default Filenames ################ +DEFAULT_HEADER = 'cvc4cppkind.h' + +##################### Useful Constants ################ +OCB = '{' +CCB = '}' +SC = ';' +EQ = '=' +C = ',' +US = '_' +NL = '\n' + +# Enum Declarations +ENUM_START = 'enum CVC4_EXPORT Kind' +ENUM_END = CCB + SC + +# Comments and Macro Tokens +COMMENT = '//' +BLOCK_COMMENT_BEGIN = '/*' +BLOCK_COMMENT_END = '*/' +MACRO_BLOCK_BEGIN = '#if 0' +MACRO_BLOCK_END = '#endif' + +# Format Kind Names +# special cases for format_name +_IS = '_IS' +# replacements after some preprocessing +replacements = { + 'Bitvector': 'BV', + 'Floatingpoint': 'FP' +} + + +class KindsParser: + tokenmap = { + BLOCK_COMMENT_BEGIN: BLOCK_COMMENT_END, + MACRO_BLOCK_BEGIN: MACRO_BLOCK_END + } + + def __init__(self): + self.kinds = OrderedDict() + self.endtoken = None + self.endtoken_stack = [] + self.in_kinds = False + + def format_name(self, name): + ''' + In the Python API, each Kind name is reformatted for easier use + + The naming scheme is: + 1. capitalize the first letter of each word (delimited by underscores) + 2. make the rest of the letters lowercase + 3. replace Floatingpoint with FP + 4. replace Bitvector with BV + + There is one exception: + FLOATINGPOINT_ISNAN --> FPIsNan + + For every "_IS" in the name, there's an underscore added before step 1, + so that the word after "Is" is capitalized + + Examples: + BITVECTOR_PLUS --> BVPlus + APPLY_SELECTOR --> ApplySelector + FLOATINGPOINT_ISNAN --> FPIsNan + SETMINUS --> Setminus + + See the generated .pxi file for an explicit mapping + ''' + name = name.replace(_IS, _IS + US) + words = [w.capitalize() for w in name.lower().split(US)] + name = "".join(words) + + for og, new in replacements.items(): + name = name.replace(og, new) + + return name + + def ignore_block(self, line): + ''' + Returns a boolean telling self.parse whether to ignore a line or not. + It also updates all the necessary state to track comments and macro + blocks + ''' + + # check if entering block comment or macro block + for token in self.tokenmap: + if token in line: + if self.tokenmap[token] not in line: + if self.endtoken is not None: + self.endtoken_stack.append(self.endtoken) + self.endtoken = self.tokenmap[token] + return True + + # check if currently in block comment or macro block + if self.endtoken is not None: + # check if reached the end of block comment or macro block + if self.endtoken in line: + if self.endtoken_stack: + self.endtoken = self.endtoken_stack.pop() + else: + self.endtoken = None + return True + + return False + + def parse(self, filename): + f = open(filename, "r") + + for line in f.read().split(NL): + line = line.strip() + if COMMENT in line: + line = line[:line.find(COMMENT)] + if not line: + continue + + if self.ignore_block(line): + continue + + if ENUM_END in line: + self.in_kinds = False + break + elif self.in_kinds: + if line == OCB: + continue + if EQ in line: + line = line[:line.find(EQ)].strip() + elif C in line: + line = line[:line.find(C)].strip() + self.kinds[line] = self.format_name(line) + elif ENUM_START in line: + self.in_kinds = True + continue + f.close() + diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py index c19364559..30ee18708 100644 --- a/src/api/python/genkinds.py +++ b/src/api/python/genkinds.py @@ -22,41 +22,22 @@ handle nested '#if 0' pairs. """ import argparse -from collections import OrderedDict +import os +import sys -#################### Default Filenames ################ -DEFAULT_HEADER = 'cvc4cppkind.h' -DEFAULT_PREFIX = 'kinds' +# the following command in CVC4/build/src/api/python/CMakeFiles/gen-pycvc4-kinds.dir/build.make +# cd CVC4/build/src/api/python && /usr/bin/python3 CVC4/src/api/python/genkinds.py ... +# indicates we are in directory CVC4/build/src/api/python +# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py +sys.path.insert(0, os.path.abspath('../../../../src/api')) -##################### Useful Constants ################ -OCB = '{' -CCB = '}' -SC = ';' -EQ = '=' -C = ',' -US = '_' -NL = '\n' +from parsekinds import * -#################### Enum Declarations ################ -ENUM_START = 'enum CVC4_EXPORT Kind' -ENUM_END = CCB+SC +#################### Default Filenames ################ +DEFAULT_PREFIX = 'kinds' ################ Comments and Macro Tokens ############ PYCOMMENT = '#' -COMMENT = '//' -BLOCK_COMMENT_BEGIN = '/*' -BLOCK_COMMENT_END = '*/' -MACRO_BLOCK_BEGIN = '#if 0' -MACRO_BLOCK_END = '#endif' - -#################### Format Kind Names ################ -# special cases for format_name -_IS = '_IS' -# replacements after some preprocessing -replacements = { - 'Bitvector' : 'BV', - 'Floatingpoint': 'FP' -} ####################### Code Blocks ################### CDEF_KIND = " cdef Kind " @@ -126,130 +107,28 @@ cdef kind {name} = kind( {kind}) setattr(kinds, "{name}", {name}) """ -class KindsParser: - tokenmap = { - BLOCK_COMMENT_BEGIN : BLOCK_COMMENT_END, - MACRO_BLOCK_BEGIN : MACRO_BLOCK_END - } - - def __init__(self): - self.kinds = OrderedDict() - self.endtoken = None - self.endtoken_stack = [] - self.in_kinds = False - - def format_name(self, name): - ''' - In the Python API, each Kind name is reformatted for easier use - - The naming scheme is: - 1. capitalize the first letter of each word (delimited by underscores) - 2. make the rest of the letters lowercase - 3. replace Floatingpoint with FP - 4. replace Bitvector with BV - - There is one exception: - FLOATINGPOINT_ISNAN --> FPIsNan - - For every "_IS" in the name, there's an underscore added before step 1, - so that the word after "Is" is capitalized - - Examples: - BITVECTOR_PLUS --> BVPlus - APPLY_SELECTOR --> ApplySelector - FLOATINGPOINT_ISNAN --> FPIsNan - SETMINUS --> Setminus - - See the generated .pxi file for an explicit mapping - ''' - name = name.replace(_IS, _IS+US) - words = [w.capitalize() for w in name.lower().split(US)] - name = "".join(words) - - for og, new in replacements.items(): - name = name.replace(og, new) - - return name - - def ignore_block(self, line): - ''' - Returns a boolean telling self.parse whether to ignore a line or not. - It also updates all the necessary state to track comments and macro - blocks - ''' - - # check if entering block comment or macro block - for token in self.tokenmap: - if token in line: - if self.tokenmap[token] not in line: - if self.endtoken is not None: - self.endtoken_stack.append(self.endtoken) - self.endtoken = self.tokenmap[token] - return True - - # check if currently in block comment or macro block - if self.endtoken is not None: - # check if reached the end of block comment or macro block - if self.endtoken in line: - if self.endtoken_stack: - self.endtoken = self.endtoken_stack.pop() - else: - self.endtoken =None - return True - - return False - - def parse(self, filename): - f = open(filename, "r") - - for line in f.read().split(NL): - line = line.strip() - if COMMENT in line: - line = line[:line.find(COMMENT)] - if not line: - continue - - if self.ignore_block(line): - continue - - if ENUM_END in line: - self.in_kinds = False - break - elif self.in_kinds: - if line == OCB: - continue - if EQ in line: - line = line[:line.find(EQ)].strip() - elif C in line: - line = line[:line.find(C)].strip() - self.kinds[line] = self.format_name(line) - elif ENUM_START in line: - self.in_kinds = True - continue - - f.close() - - def gen_pxd(self, filename): - f = open(filename, "w") - f.write(KINDS_PXD_TOP) - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in self.format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) - for kind in self.kinds: - f.write(CDEF_KIND + kind + NL) - f.close() - def gen_pxi(self, filename): - f = open(filename, "w") - pxi = KINDS_PXI_TOP - for kind, name in self.kinds.items(): - pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) - f.write(pxi) - f.close() +def gen_pxd(parser: KindsParser, filename): + f = open(filename, "w") + f.write(KINDS_PXD_TOP) + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in parser.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + for kind in parser.kinds: + f.write(CDEF_KIND + kind + NL) + f.close() + +def gen_pxi(parser : KindsParser, filename): + f = open(filename, "w") + pxi = KINDS_PXI_TOP + for kind, name in parser.kinds.items(): + pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) + f.write(pxi) + f.close() if __name__ == "__main__": @@ -270,5 +149,5 @@ if __name__ == "__main__": kp = KindsParser() kp.parse(kinds_header) - kp.gen_pxd(kinds_file_prefix + ".pxd") - kp.gen_pxi(kinds_file_prefix + ".pxi") + gen_pxd(kp, kinds_file_prefix + ".pxd") + gen_pxi(kp, kinds_file_prefix + ".pxi") -- 2.30.2