From d8291819e4bba179b0b4ec23053b2a9537948e51 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 20 Dec 2024 20:20:11 +0100 Subject: [PATCH 01/12] test: fixing parikh --- src/test/noodler/parikh.cc | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/test/noodler/parikh.cc b/src/test/noodler/parikh.cc index 6f1921539ae..bd20bfdaa48 100644 --- a/src/test/noodler/parikh.cc +++ b/src/test/noodler/parikh.cc @@ -67,7 +67,7 @@ TEST_CASE("NotContains::mk_parikh_images_encode_same_word_formula simple", "[noo ca::TagAut tag_automaton = tag_automaton_generator.construct_tag_aut(); - REQUIRE(tag_automaton.nfa.num_of_states() == 6); // 4 states * 3 copies, but half are needless and removed during trimming + REQUIRE(tag_automaton.nfa.num_of_states() == 8); // 4 states * 3 copies, but half are needless and removed during trimming std::set used_symbols = tag_automaton.gather_used_symbols(); @@ -138,7 +138,7 @@ TEST_CASE("NotContains::mk_rhs_longer_than_lhs_formula simple", "[noodler]") { ca::TagAut tag_automaton = tag_automaton_generator.construct_tag_aut(); size_t states_in_row = 8; // "abc" is 4-state automaton, we concatenate two of these - REQUIRE(tag_automaton.nfa.num_of_states() == 18); + REQUIRE(tag_automaton.nfa.num_of_states() == 20); std::set used_symbols = tag_automaton.gather_used_symbols(); @@ -190,7 +190,7 @@ TEST_CASE("NotContains::ensure_symbol_unqueness_using_total_sum simple", "[noodl ca::TagAut tag_automaton = tag_automaton_generator.construct_tag_aut(); size_t states_in_row = 7; - REQUIRE(tag_automaton.nfa.num_of_states() == 15); + REQUIRE(tag_automaton.nfa.num_of_states() == 17); std::set used_symbols = tag_automaton.gather_used_symbols(); @@ -442,7 +442,7 @@ TEST_CASE("NotContains::copies should differ in transition symbols", "[noodler]" ca::TagAut tag_automaton = tag_automaton_generator.construct_tag_aut(); // size_t states_in_row = 7; - REQUIRE(tag_automaton.nfa.num_of_states() == 15); + REQUIRE(tag_automaton.nfa.num_of_states() == 17); BasicTerm var_x = get_var('x'); auto what_mismatch_labels_do_levels_contain = get_nonsampling_transitions_labeled_with_symbol(tag_automaton, var_x); @@ -565,7 +565,7 @@ TEST_CASE("Disequations :: tag automaton for a single disequation is correct", " ca::TagDiseqGen tag_automaton_generator(diseq1, aut_assignment); ca::TagAut tag_automaton = tag_automaton_generator.construct_tag_aut(); - REQUIRE(tag_automaton.nfa.num_of_states() == 10); + REQUIRE(tag_automaton.nfa.num_of_states() == 13); ca::AtomicSymbol len_x = ca::AtomicSymbol::create_l_symbol(var_x); ca::AtomicSymbol len_y = ca::AtomicSymbol::create_l_symbol(var_y); @@ -601,12 +601,12 @@ void add_all_possible_sampling_transitions(std::vector& transi ca::AtomicSymbol mismatch_pos = ca::AtomicSymbol::create_p_symbol(var, copy_idx); for (size_t predicate_idx = 0; predicate_idx < predicate_count; predicate_idx++) { - ca::AtomicSymbol register_store_left = ca::AtomicSymbol::create_r_symbol_with_predicate_info(predicate_idx, AtomicSymbol::PredicateSide::LEFT, copy_idx, transition.symbol); + ca::AtomicSymbol register_store_left = ca::AtomicSymbol::create_r_symbol_with_predicate_info(predicate_idx, var, AtomicSymbol::PredicateSide::LEFT, copy_idx, transition.symbol); TagSet left_tag_set = {var_len, mismatch_pos, register_store_left}; TagSetTransition transition_sampling_left = {.source = transition.source, .tag_set = left_tag_set, .target = transition.target}; transitions.push_back(transition_sampling_left); - ca::AtomicSymbol register_store_right = ca::AtomicSymbol::create_r_symbol_with_predicate_info(predicate_idx, AtomicSymbol::PredicateSide::RIGHT, copy_idx, transition.symbol); + ca::AtomicSymbol register_store_right = ca::AtomicSymbol::create_r_symbol_with_predicate_info(predicate_idx, var, AtomicSymbol::PredicateSide::RIGHT, copy_idx, transition.symbol); TagSet right_tag_set = {var_len, mismatch_pos, register_store_right}; TagSetTransition transition_sampling_right = {.source = transition.source, .tag_set = right_tag_set, .target = transition.target}; transitions.push_back(transition_sampling_right); @@ -700,7 +700,7 @@ TEST_CASE("Disequations :: automaton for more predicates is constructed correctl ca::AtomicSymbol mismatch_pos_y_2 = ca::AtomicSymbol::create_p_symbol(var_y, 2); ca::AtomicSymbol mismatch_pos_z_2 = ca::AtomicSymbol::create_p_symbol(var_z, 2); - ca::AtomicSymbol register_store_x_1 = ca::AtomicSymbol::create_r_symbol_with_predicate_info(0, AtomicSymbol::PredicateSide::LEFT, 1, 'a'); + ca::AtomicSymbol register_store_x_1 = ca::AtomicSymbol::create_r_symbol_with_predicate_info(0, var_x, AtomicSymbol::PredicateSide::LEFT, 1, 'a'); ca::AtomicSymbol register_store_y_1 = ca::AtomicSymbol::create_r_symbol(var_y, 1, 'b'); ca::AtomicSymbol register_store_y_2 = ca::AtomicSymbol::create_r_symbol(var_y, 2, 'b'); @@ -872,7 +872,6 @@ void check_register_stores_for_level(int level, const TagAut& tag_automaton, con std::map seen_register_implications; const BasicTerm& reg_ord = formula_generator.registers_in_sampling_order[level].atom_val; - std::cout << "Using ORD register: " << reg_ord << "\n"; for (const auto& [transition, var] : formula_generator.get_trans_vars()) { mata::nfa::State source_state = std::get<0>(transition); mata::Symbol symbol_handle = std::get<1>(transition); @@ -894,9 +893,7 @@ void check_register_stores_for_level(int level, const TagAut& tag_automaton, con } } - std::cout << "----\n"; for (const LenNode& implication : implications_conjunction.succ) { - std::cout << implication << "\n"; assert_register_store_implication_structure(implication, seen_register_implications); } @@ -926,7 +923,7 @@ TEST_CASE("Disequations :: check assert_register_values", "[noodler]") { size_t num_of_copies = 5; size_t num_of_states_in_row = 6; ParikhImageDiseqTag formula_generator (tag_automaton, available_tags, num_of_states_in_row); - formula_generator.predicate_count = 2; + formula_generator.predicates = {diseq1, diseq2}; formula_generator.compute_parikh_image(); From 444da480b28d54e312f3c9bd54c81df42e647283 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 21 Dec 2024 14:22:02 +0100 Subject: [PATCH 02/12] action: build on ubuntu --- .github/workflows/build.yml | 40 +++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 00000000000..cd803a873f1 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,40 @@ +name: Various platforms (build-&-test) + +on: + push: + branches: + - master + - devel + pull_request: + branches: + - master + - devel + # allows to run the action from GitHub UI + workflow_dispatch: + + +jobs: + ubuntu-build: + name: "Ubuntu (build-&-test)" + runs-on: ubuntu-latest + steps: + - name: Clone Mata + uses: GuillaumeFalourd/clone-github-repo-action@v2.3 + with: + owner: 'VeriFIT' + repository: 'mata' + branch: devel + depth: 1 + + - name: Instal Mata + run: | + cd mata + make release + sudo make install + + - name: Compile Z3-Noodler release + run: | + mkdir build + cd build + cmake -DCMAKE_BUILD_TYPE=Release .. + make -j4 From b63710a7cdee098ff1593127dba172b5d04db8d5 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 21 Dec 2024 14:28:45 +0100 Subject: [PATCH 03/12] build: compiling noodler --- .github/workflows/build.yml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index cd803a873f1..b87e3d35092 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -18,23 +18,23 @@ jobs: name: "Ubuntu (build-&-test)" runs-on: ubuntu-latest steps: - - name: Clone Mata - uses: GuillaumeFalourd/clone-github-repo-action@v2.3 - with: - owner: 'VeriFIT' - repository: 'mata' - branch: devel - depth: 1 + # - name: Clone Mata + # uses: GuillaumeFalourd/clone-github-repo-action@v2.3 + # with: + # owner: 'VeriFIT' + # repository: 'mata' + # branch: devel + # depth: 1 - - name: Instal Mata - run: | - cd mata - make release - sudo make install + # - name: Install Mata + # run: | + # cd mata + # make release + # sudo make install - name: Compile Z3-Noodler release run: | mkdir build cd build - cmake -DCMAKE_BUILD_TYPE=Release .. + cmake -DCMAKE_BUILD_TYPE=Release ".." make -j4 From 9a5555e599c437f5d3bdb824bdf20e2148167ddd Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 21 Dec 2024 14:32:36 +0100 Subject: [PATCH 04/12] build: update --- .github/workflows/build.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b87e3d35092..98a476b375b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -34,7 +34,8 @@ jobs: - name: Compile Z3-Noodler release run: | + ls mkdir build cd build - cmake -DCMAKE_BUILD_TYPE=Release ".." + cmake -DCMAKE_BUILD_TYPE="Release" ../ make -j4 From be644f17de7fe08794176d05ec58e785b8837402 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 21 Dec 2024 14:34:31 +0100 Subject: [PATCH 05/12] build: update 2 --- .github/workflows/build.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 98a476b375b..18560900a22 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -32,6 +32,9 @@ jobs: # make release # sudo make install + - name: Check out repository code + uses: actions/checkout@v3 + - name: Compile Z3-Noodler release run: | ls From a439155226edfbbf238174e24048b06c296512c8 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 21 Dec 2024 14:35:56 +0100 Subject: [PATCH 06/12] build: update with mata --- .github/workflows/build.yml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 18560900a22..955d752eb87 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -18,26 +18,25 @@ jobs: name: "Ubuntu (build-&-test)" runs-on: ubuntu-latest steps: - # - name: Clone Mata - # uses: GuillaumeFalourd/clone-github-repo-action@v2.3 - # with: - # owner: 'VeriFIT' - # repository: 'mata' - # branch: devel - # depth: 1 + - name: Clone Mata + uses: GuillaumeFalourd/clone-github-repo-action@v2.3 + with: + owner: 'VeriFIT' + repository: 'mata' + branch: devel + depth: 1 - # - name: Install Mata - # run: | - # cd mata - # make release - # sudo make install + - name: Install Mata + run: | + cd mata + make release + sudo make install - name: Check out repository code uses: actions/checkout@v3 - name: Compile Z3-Noodler release run: | - ls mkdir build cd build cmake -DCMAKE_BUILD_TYPE="Release" ../ From f1de7832c0ba7b764c4a89924b580a0f7dba21e4 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 16:10:09 +0100 Subject: [PATCH 07/12] build: add noodler test --- .github/workflows/build.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 955d752eb87..be9f8c9eaa0 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -41,3 +41,11 @@ jobs: cd build cmake -DCMAKE_BUILD_TYPE="Release" ../ make -j4 + + - name: Test Z3-Noodler + run: | + mkdir build + cd build + cmake -DCMAKE_BUILD_TYPE="Release" ../ + make -j4 test-noodler + ./test-noodler From be4fae575dc42597e1eb8b77800a712f84c84897 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 16:28:10 +0100 Subject: [PATCH 08/12] build: install dependencies --- .github/workflows/build.yml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index be9f8c9eaa0..2699cf3816e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -26,6 +26,11 @@ jobs: branch: devel depth: 1 + - name: Install dependencies + run: | + sudo apt-get update + sudo apt-get install catch2 + - name: Install Mata run: | cd mata @@ -44,8 +49,6 @@ jobs: - name: Test Z3-Noodler run: | - mkdir build cd build - cmake -DCMAKE_BUILD_TYPE="Release" ../ make -j4 test-noodler ./test-noodler From 758c5cef2cc17ec3271902c04cf9016397337bad Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 16:54:07 +0100 Subject: [PATCH 09/12] build: macos --- .github/workflows/build.yml | 41 +++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 2699cf3816e..1f79d73b1fc 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -14,6 +14,45 @@ on: jobs: + macos-build: + name: "MacOS (build-&-test)" + runs-on: macos-15 + steps: + - name: Clone Mata + uses: GuillaumeFalourd/clone-github-repo-action@v2.3 + with: + owner: 'VeriFIT' + repository: 'mata' + branch: devel + depth: 1 + + - name: Install dependencies + run: | + brew update + brew install catch2 + + - name: Install Mata + run: | + cd mata + make release + sudo make install + + - name: Check out repository code + uses: actions/checkout@v3 + + - name: Compile Z3-Noodler release + run: | + mkdir build + cd build + cmake -DCMAKE_BUILD_TYPE="Release" ../ + make -j4 + + - name: Test Z3-Noodler + run: | + cd build + make -j4 test-noodler + ./test-noodler + ubuntu-build: name: "Ubuntu (build-&-test)" runs-on: ubuntu-latest @@ -52,3 +91,5 @@ jobs: cd build make -j4 test-noodler ./test-noodler + + \ No newline at end of file From c1c4f68964700d8b7509710b6e6f909c42ddd4cf Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 17:04:09 +0100 Subject: [PATCH 10/12] build: macos add include path --- .github/workflows/build.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 1f79d73b1fc..41c1350d164 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -44,6 +44,7 @@ jobs: run: | mkdir build cd build + export CPLUS_INCLUDE_PATH="${CPLUS_INCLUDE_PATH:+${CPLUS_INCLUDE_PATH}:}/usr/local/include/" cmake -DCMAKE_BUILD_TYPE="Release" ../ make -j4 From 520e7569287f293e9a9a9f10cb0df1ce3b7db0e2 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 17:14:05 +0100 Subject: [PATCH 11/12] build: macos: add export path to test step --- .github/workflows/build.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 41c1350d164..726454ae000 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -51,6 +51,7 @@ jobs: - name: Test Z3-Noodler run: | cd build + export CPLUS_INCLUDE_PATH="${CPLUS_INCLUDE_PATH:+${CPLUS_INCLUDE_PATH}:}/usr/local/include/" make -j4 test-noodler ./test-noodler From 03ec019b619fa2711bf82224071a8857c148ab15 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 17:32:22 +0100 Subject: [PATCH 12/12] README: add badges --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index 08237bcff53..c2b2206e5fc 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,8 @@ # Z3-Noodler +[![GitHub tag](https://img.shields.io/github/tag/VeriFIT/z3-noodler.svg)](https://github.com/VeriFIT/z3-noodler) +![Build](https://github.com/VeriFIT/z3-noodler/actions/workflows/build.yml/badge.svg) + Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, reasoning about configuration files of cloud services and smart contracts, etc. Z3-Noodler is based on the SMT solver [Z3 v4.13.0](https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0), in which it replaces the solver for the theory of strings.