diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 00000000000..726454ae000 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,97 @@ +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: + 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 + export CPLUS_INCLUDE_PATH="${CPLUS_INCLUDE_PATH:+${CPLUS_INCLUDE_PATH}:}/usr/local/include/" + cmake -DCMAKE_BUILD_TYPE="Release" ../ + make -j4 + + - 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 + + 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: Install dependencies + run: | + sudo apt-get update + sudo apt-get 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 + + \ No newline at end of file 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. 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();