Skip to content

Commit

Permalink
Merge pull request #203 from VeriFIT/fix-tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@vhavlena
vhavlena authored Dec 23, 2024
2 parents e5ee303 + 03ec019 commit 771f0a5
Show file tree
Hide file tree
Showing 3 changed files with 109 additions and 12 deletions.
97 changes: 97 additions & 0 deletions .github/workflows/build.yml
View file
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
21 changes: 9 additions & 12 deletions src/test/noodler/parikh.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<ca::AtomicSymbol> used_symbols = tag_automaton.gather_used_symbols();

Expand Down Expand Up @@ -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<ca::AtomicSymbol> used_symbols = tag_automaton.gather_used_symbols();

Expand Down Expand Up @@ -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<ca::AtomicSymbol> used_symbols = tag_automaton.gather_used_symbols();

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -601,12 +601,12 @@ void add_all_possible_sampling_transitions(std::vector<TagSetTransition>& 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);
Expand Down Expand Up @@ -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');
Expand Down Expand Up @@ -872,7 +872,6 @@ void check_register_stores_for_level(int level, const TagAut& tag_automaton, con
std::map<RegisterValueImplicationVars, int> 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);
Expand All @@ -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);
}

Expand Down Expand Up @@ -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();

Expand Down

0 comments on commit 771f0a5

Please sign in to comment.