Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bitvector arithmetics MBP #34

Open
wants to merge 33 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
8322953
catch2 unit testing framework
Almazis Aug 9, 2022
39c0e71
example of expr unit test
Almazis Aug 9, 2022
8f9438d
Some bv code
Almazis Aug 10, 2022
eb9403c
added some bv rules
Almazis Aug 10, 2022
e18b778
rewrite getLiterals
Almazis Aug 19, 2022
89508b2
some new bv code
Almazis Aug 22, 2022
53b7d6a
typeof bv operations
Almazis Aug 22, 2022
94b9b0e
get literals for bv
Almazis Aug 24, 2022
02623be
vscode and test files added
Almazis Aug 24, 2022
5197bd7
[fix] add header
Almazis Aug 24, 2022
6c019d9
the core of bv normalization
Almazis Aug 30, 2022
15499c4
some bv utils
Almazis Sep 2, 2022
63de6c9
mbputils changes for bv
Almazis Sep 6, 2022
05d7b11
overflow basic check
Almazis Sep 9, 2022
58b3413
simple version of bvQE
Almazis Sep 12, 2022
8471eb9
some bugfixes
Almazis Sep 12, 2022
90d619a
changed overflow check
Almazis Sep 14, 2022
1020d81
added new normalization rules
Almazis Sep 14, 2022
4ee6390
normalizator runs
Almazis Sep 16, 2022
cdff825
Refactoring and bugfix
Almazis Sep 19, 2022
2ce4c97
added bounds merging for bv
Almazis Sep 20, 2022
9861922
minor bugfix
Almazis Sep 21, 2022
9866ff1
minor bugfix
Almazis Sep 23, 2022
9eba623
Format of ZExprConverter
Almazis Sep 27, 2022
054349b
added div rules
Almazis Sep 30, 2022
87f9c82
rewrite burem
Almazis Sep 30, 2022
57b2f91
Lazy MBP
Almazis Oct 1, 2022
5b6fede
Merge branch 'master' into bv_utils
Almazis Oct 3, 2022
0592fe6
codestyle fixes
Almazis Oct 3, 2022
fe6d6b6
disable unit tests by default
Almazis Oct 3, 2022
300f5b1
clean up vscode files
Almazis Oct 3, 2022
bff92fe
bench files removed
Almazis Oct 3, 2022
4c040c3
pr cleanup
Almazis Oct 3, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
cmake_minimum_required(VERSION 2.8.11)
cmake_minimum_required(VERSION 3.5)

project (AeVal)
set (AeVal_VERSION_MAJOR 1)
set (AeVal_VERSION_MINOR 0)
set (CatchTestsEnabled FALSE) # set to TRUE to build catch unit tests

if (NOT PACKAGE_VERSION)
set(PACKAGE_VERSION
Expand Down Expand Up @@ -169,3 +170,6 @@ include_directories(BEFORE ${CMAKE_CURRENT_BINARY_DIR}/src)

add_subdirectory(src)
add_subdirectory(tools)
if (${CatchTestsEnabled})
add_subdirectory(tests)
endif()
206 changes: 206 additions & 0 deletions cmake/Catch.cmake
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
# Distributed under the OSI-approved BSD 3-Clause License. See accompanying
# file Copyright.txt or https://cmake.org/licensing for details.

#[=======================================================================[.rst:
Catch
-----

This module defines a function to help use the Catch test framework.

The :command:`catch_discover_tests` discovers tests by asking the compiled test
executable to enumerate its tests. This does not require CMake to be re-run
when tests change. However, it may not work in a cross-compiling environment,
and setting test properties is less convenient.

This command is intended to replace use of :command:`add_test` to register
tests, and will create a separate CTest test for each Catch test case. Note
that this is in some cases less efficient, as common set-up and tear-down logic
cannot be shared by multiple test cases executing in the same instance.
However, it provides more fine-grained pass/fail information to CTest, which is
usually considered as more beneficial. By default, the CTest test name is the
same as the Catch name; see also ``TEST_PREFIX`` and ``TEST_SUFFIX``.

.. command:: catch_discover_tests

Automatically add tests with CTest by querying the compiled test executable
for available tests::

catch_discover_tests(target
[TEST_SPEC arg1...]
[EXTRA_ARGS arg1...]
[WORKING_DIRECTORY dir]
[TEST_PREFIX prefix]
[TEST_SUFFIX suffix]
[PROPERTIES name1 value1...]
[TEST_LIST var]
[REPORTER reporter]
[OUTPUT_DIR dir]
[OUTPUT_PREFIX prefix}
[OUTPUT_SUFFIX suffix]
)

``catch_discover_tests`` sets up a post-build command on the test executable
that generates the list of tests by parsing the output from running the test
with the ``--list-test-names-only`` argument. This ensures that the full
list of tests is obtained. Since test discovery occurs at build time, it is
not necessary to re-run CMake when the list of tests changes.
However, it requires that :prop_tgt:`CROSSCOMPILING_EMULATOR` is properly set
in order to function in a cross-compiling environment.

Additionally, setting properties on tests is somewhat less convenient, since
the tests are not available at CMake time. Additional test properties may be
assigned to the set of tests as a whole using the ``PROPERTIES`` option. If
more fine-grained test control is needed, custom content may be provided
through an external CTest script using the :prop_dir:`TEST_INCLUDE_FILES`
directory property. The set of discovered tests is made accessible to such a
script via the ``<target>_TESTS`` variable.

The options are:

``target``
Specifies the Catch executable, which must be a known CMake executable
target. CMake will substitute the location of the built executable when
running the test.

``TEST_SPEC arg1...``
Specifies test cases, wildcarded test cases, tags and tag expressions to
pass to the Catch executable with the ``--list-test-names-only`` argument.

``EXTRA_ARGS arg1...``
Any extra arguments to pass on the command line to each test case.

``WORKING_DIRECTORY dir``
Specifies the directory in which to run the discovered test cases. If this
option is not provided, the current binary directory is used.

``TEST_PREFIX prefix``
Specifies a ``prefix`` to be prepended to the name of each discovered test
case. This can be useful when the same test executable is being used in
multiple calls to ``catch_discover_tests()`` but with different
``TEST_SPEC`` or ``EXTRA_ARGS``.

``TEST_SUFFIX suffix``
Similar to ``TEST_PREFIX`` except the ``suffix`` is appended to the name of
every discovered test case. Both ``TEST_PREFIX`` and ``TEST_SUFFIX`` may
be specified.

``PROPERTIES name1 value1...``
Specifies additional properties to be set on all tests discovered by this
invocation of ``catch_discover_tests``.

``TEST_LIST var``
Make the list of tests available in the variable ``var``, rather than the
default ``<target>_TESTS``. This can be useful when the same test
executable is being used in multiple calls to ``catch_discover_tests()``.
Note that this variable is only available in CTest.

``REPORTER reporter``
Use the specified reporter when running the test case. The reporter will
be passed to the Catch executable as ``--reporter reporter``.

``OUTPUT_DIR dir``
If specified, the parameter is passed along as
``--out dir/<test_name>`` to Catch executable. The actual file name is the
same as the test name. This should be used instead of
``EXTRA_ARGS --out foo`` to avoid race conditions writing the result output
when using parallel test execution.

``OUTPUT_PREFIX prefix``
May be used in conjunction with ``OUTPUT_DIR``.
If specified, ``prefix`` is added to each output file name, like so
``--out dir/prefix<test_name>``.

``OUTPUT_SUFFIX suffix``
May be used in conjunction with ``OUTPUT_DIR``.
If specified, ``suffix`` is added to each output file name, like so
``--out dir/<test_name>suffix``. This can be used to add a file extension to
the output e.g. ".xml".

#]=======================================================================]

#------------------------------------------------------------------------------
function(catch_discover_tests TARGET)
cmake_parse_arguments(
""
""
"TEST_PREFIX;TEST_SUFFIX;WORKING_DIRECTORY;TEST_LIST;REPORTER;OUTPUT_DIR;OUTPUT_PREFIX;OUTPUT_SUFFIX"
"TEST_SPEC;EXTRA_ARGS;PROPERTIES"
${ARGN}
)

if(NOT _WORKING_DIRECTORY)
set(_WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}")
endif()
if(NOT _TEST_LIST)
set(_TEST_LIST ${TARGET}_TESTS)
endif()

## Generate a unique name based on the extra arguments
string(SHA1 args_hash "${_TEST_SPEC} ${_EXTRA_ARGS} ${_REPORTER} ${_OUTPUT_DIR} ${_OUTPUT_PREFIX} ${_OUTPUT_SUFFIX}")
string(SUBSTRING ${args_hash} 0 7 args_hash)

# Define rule to generate test list for aforementioned test executable
set(ctest_include_file "${CMAKE_CURRENT_BINARY_DIR}/${TARGET}_include-${args_hash}.cmake")
set(ctest_tests_file "${CMAKE_CURRENT_BINARY_DIR}/${TARGET}_tests-${args_hash}.cmake")
get_property(crosscompiling_emulator
TARGET ${TARGET}
PROPERTY CROSSCOMPILING_EMULATOR
)
add_custom_command(
TARGET ${TARGET} POST_BUILD
BYPRODUCTS "${ctest_tests_file}"
COMMAND "${CMAKE_COMMAND}"
-D "TEST_TARGET=${TARGET}"
-D "TEST_EXECUTABLE=$<TARGET_FILE:${TARGET}>"
-D "TEST_EXECUTOR=${crosscompiling_emulator}"
-D "TEST_WORKING_DIR=${_WORKING_DIRECTORY}"
-D "TEST_SPEC=${_TEST_SPEC}"
-D "TEST_EXTRA_ARGS=${_EXTRA_ARGS}"
-D "TEST_PROPERTIES=${_PROPERTIES}"
-D "TEST_PREFIX=${_TEST_PREFIX}"
-D "TEST_SUFFIX=${_TEST_SUFFIX}"
-D "TEST_LIST=${_TEST_LIST}"
-D "TEST_REPORTER=${_REPORTER}"
-D "TEST_OUTPUT_DIR=${_OUTPUT_DIR}"
-D "TEST_OUTPUT_PREFIX=${_OUTPUT_PREFIX}"
-D "TEST_OUTPUT_SUFFIX=${_OUTPUT_SUFFIX}"
-D "CTEST_FILE=${ctest_tests_file}"
-P "${_CATCH_DISCOVER_TESTS_SCRIPT}"
VERBATIM
)

file(WRITE "${ctest_include_file}"
"if(EXISTS \"${ctest_tests_file}\")\n"
" include(\"${ctest_tests_file}\")\n"
"else()\n"
" add_test(${TARGET}_NOT_BUILT-${args_hash} ${TARGET}_NOT_BUILT-${args_hash})\n"
"endif()\n"
)

if(NOT ${CMAKE_VERSION} VERSION_LESS "3.10.0")
# Add discovered tests to directory TEST_INCLUDE_FILES
set_property(DIRECTORY
APPEND PROPERTY TEST_INCLUDE_FILES "${ctest_include_file}"
)
else()
# Add discovered tests as directory TEST_INCLUDE_FILE if possible
get_property(test_include_file_set DIRECTORY PROPERTY TEST_INCLUDE_FILE SET)
if (NOT ${test_include_file_set})
set_property(DIRECTORY
PROPERTY TEST_INCLUDE_FILE "${ctest_include_file}"
)
else()
message(FATAL_ERROR
"Cannot set more than one TEST_INCLUDE_FILE"
)
endif()
endif()

endfunction()

###############################################################################

set(_CATCH_DISCOVER_TESTS_SCRIPT
${CMAKE_CURRENT_LIST_DIR}/CatchAddTests.cmake
CACHE INTERNAL "Catch2 full path to CatchAddTests.cmake helper file"
)
10 changes: 10 additions & 0 deletions cmake/Catch2Config.cmake
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
@PACKAGE_INIT@


# Avoid repeatedly including the targets
if(NOT TARGET Catch2::Catch2)
# Provide path for scripts
list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}")

include(${CMAKE_CURRENT_LIST_DIR}/Catch2Targets.cmake)
endif()
135 changes: 135 additions & 0 deletions cmake/CatchAddTests.cmake
Original file line number Diff line number Diff line change
@@ -0,0 +1,135 @@
# Distributed under the OSI-approved BSD 3-Clause License. See accompanying
# file Copyright.txt or https://cmake.org/licensing for details.

set(prefix "${TEST_PREFIX}")
set(suffix "${TEST_SUFFIX}")
set(spec ${TEST_SPEC})
set(extra_args ${TEST_EXTRA_ARGS})
set(properties ${TEST_PROPERTIES})
set(reporter ${TEST_REPORTER})
set(output_dir ${TEST_OUTPUT_DIR})
set(output_prefix ${TEST_OUTPUT_PREFIX})
set(output_suffix ${TEST_OUTPUT_SUFFIX})
set(script)
set(suite)
set(tests)

function(add_command NAME)
set(_args "")
# use ARGV* instead of ARGN, because ARGN splits arrays into multiple arguments
math(EXPR _last_arg ${ARGC}-1)
foreach(_n RANGE 1 ${_last_arg})
set(_arg "${ARGV${_n}}")
if(_arg MATCHES "[^-./:a-zA-Z0-9_]")
set(_args "${_args} [==[${_arg}]==]") # form a bracket_argument
else()
set(_args "${_args} ${_arg}")
endif()
endforeach()
set(script "${script}${NAME}(${_args})\n" PARENT_SCOPE)
endfunction()

# Run test executable to get list of available tests
if(NOT EXISTS "${TEST_EXECUTABLE}")
message(FATAL_ERROR
"Specified test executable '${TEST_EXECUTABLE}' does not exist"
)
endif()
execute_process(
COMMAND ${TEST_EXECUTOR} "${TEST_EXECUTABLE}" ${spec} --list-test-names-only
OUTPUT_VARIABLE output
RESULT_VARIABLE result
WORKING_DIRECTORY "${TEST_WORKING_DIR}"
)
# Catch --list-test-names-only reports the number of tests, so 0 is... surprising
if(${result} EQUAL 0)
message(WARNING
"Test executable '${TEST_EXECUTABLE}' contains no tests!\n"
)
elseif(${result} LESS 0)
message(FATAL_ERROR
"Error running test executable '${TEST_EXECUTABLE}':\n"
" Result: ${result}\n"
" Output: ${output}\n"
)
endif()

string(REPLACE "\n" ";" output "${output}")

# Run test executable to get list of available reporters
execute_process(
COMMAND ${TEST_EXECUTOR} "${TEST_EXECUTABLE}" ${spec} --list-reporters
OUTPUT_VARIABLE reporters_output
RESULT_VARIABLE reporters_result
WORKING_DIRECTORY "${TEST_WORKING_DIR}"
)
if(${reporters_result} EQUAL 0)
message(WARNING
"Test executable '${TEST_EXECUTABLE}' contains no reporters!\n"
)
elseif(${reporters_result} LESS 0)
message(FATAL_ERROR
"Error running test executable '${TEST_EXECUTABLE}':\n"
" Result: ${reporters_result}\n"
" Output: ${reporters_output}\n"
)
endif()
string(FIND "${reporters_output}" "${reporter}" reporter_is_valid)
if(reporter AND ${reporter_is_valid} EQUAL -1)
message(FATAL_ERROR
"\"${reporter}\" is not a valid reporter!\n"
)
endif()

# Prepare reporter
if(reporter)
set(reporter_arg "--reporter ${reporter}")
endif()

# Prepare output dir
if(output_dir AND NOT IS_ABSOLUTE ${output_dir})
set(output_dir "${TEST_WORKING_DIR}/${output_dir}")
if(NOT EXISTS ${output_dir})
file(MAKE_DIRECTORY ${output_dir})
endif()
endif()

# Parse output
foreach(line ${output})
set(test ${line})
# Escape characters in test case names that would be parsed by Catch2
set(test_name ${test})
foreach(char , [ ])
string(REPLACE ${char} "\\${char}" test_name ${test_name})
endforeach(char)
# ...add output dir
if(output_dir)
string(REGEX REPLACE "[^A-Za-z0-9_]" "_" test_name_clean ${test_name})
set(output_dir_arg "--out ${output_dir}/${output_prefix}${test_name_clean}${output_suffix}")
endif()

# ...and add to script
add_command(add_test
"${prefix}${test}${suffix}"
${TEST_EXECUTOR}
"${TEST_EXECUTABLE}"
"${test_name}"
${extra_args}
"${reporter_arg}"
"${output_dir_arg}"
)
add_command(set_tests_properties
"${prefix}${test}${suffix}"
PROPERTIES
WORKING_DIRECTORY "${TEST_WORKING_DIR}"
${properties}
)
list(APPEND tests "${prefix}${test}${suffix}")
endforeach()

# Create a list of all discovered tests, which users may use to e.g. set
# properties on the tests
add_command(set ${TEST_LIST} ${tests})

# Write CTest script
file(WRITE "${CTEST_FILE}" "${script}")
Loading