Skip to content

Translation of array_of_exprt to SMT 2 backend #7079

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

Merged
merged 4 commits into from
Aug 23, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
15 changes: 12 additions & 3 deletions .github/workflows/pull-request-checks.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -698,13 +698,22 @@ jobs:
- name: Fetch dependencies
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
# remove libgcc-s1, which isn't normally available in Ubuntu 18.04
target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
# libgcc1 uses an epoch, thus the extra 1:
sudo apt-get install -y --allow-downgrades --reinstall gcc g++ libgcc-s1- libstdc++6=$target liblsan0=$target libtsan0=$target libcc1-0=$target libgcc1=1:$target gdb=8.1.1-0ubuntu1
- name: Confirm z3 solver is available and log the version installed
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ I'd prefer to leave this as a separate step, as it makes it easier to find the version number and keeps this job consistent with the others.

run: z3 --version
- name: Download z3 4.11.0 from the python wheel package, extract it and make sure it can be deployed
run: |
sudo apt-get install --no-install-recommends -y unzip
# download the z3 python wheel package
wget -O z3.4.11.0.whl https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3_solver-4.11.0.0-py2.py3-none-manylinux1_x86_64.whl
# unpack the bundle using python
unzip z3.4.11.0.whl
# make z3 executable and move it in /usr/local/bin
chmod u+x ./z3_solver-4.11.0.0.data/data/bin/z3
mv ./z3_solver-4.11.0.0.data/data/bin/z3 /usr/local/bin/
z3 --version
- name: Download cvc-5 from the releases page and make sure it can be deployed
run: |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
Expand Down
12 changes: 12 additions & 0 deletions regression/cbmc-incr-smt2/arrays/array_of.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
int main()
{
int example_array[10000];
unsigned int index;
__CPROVER_assume(index < 999);

__CPROVER_array_set(example_array, 43);
__CPROVER_assert(example_array[index] != 43, "False array condition");

__CPROVER_array_set(example_array, 42);
__CPROVER_assert(example_array[index] == 42, "Valid array condition");
}
13 changes: 13 additions & 0 deletions regression/cbmc-incr-smt2/arrays/array_of.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
CORE
array_of.c

Passing problem to incremental SMT2 solving
line \d+ False array condition: FAILURE
line \d+ Valid array condition: SUCCESS
^EXIT=10$
^SIGNAL=0$
--
--
Test using __CPROVER_array_set consisting in an `array_of` node which sets all values of a given
array to a given value.
This test uses a forall SMT statement.
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ control_flow.c
--verbosity 10
Passing problem to incremental SMT2 solving via
Sending command to SMT2 solver - \(set-option :produce-models true\)
Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
Sending command to SMT2 solver - \(set-logic ALL\)
Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ test.c
--verbosity 10
Passing problem to incremental SMT2 solving via
Sending command to SMT2 solver - \(set-option :produce-models true\)
Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
Sending command to SMT2 solver - \(set-logic ALL\)
Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
Expand Down
13 changes: 8 additions & 5 deletions src/solvers/smt2_incremental/convert_expr_to_smt.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -906,8 +906,10 @@ static smt_termt convert_expr_to_smt(
const array_of_exprt &array_of,
const sub_expression_mapt &converted)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for array of expression: " + array_of.pretty());
// This function is unreachable as the `array_of_exprt` nodes are already
// fully converted by the incremental decision procedure functions
// (smt2_incremental_decision_proceduret::define_array_function).
UNHANDLED_CASE;
}

static smt_termt convert_expr_to_smt(
Expand Down Expand Up @@ -1353,9 +1355,10 @@ static smt_termt convert_expr_to_smt(
const array_exprt &array_construction,
const sub_expression_mapt &converted)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for array construction expression: " +
array_construction.pretty());
// This function is unreachable as the `array_exprt` nodes are already fully
// converted by the incremental decision procedure functions
// (smt2_incremental_decision_proceduret::define_array_function).
UNHANDLED_CASE;
}

static smt_termt convert_expr_to_smt(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
if(
can_cast_expr<symbol_exprt>(expr_node) ||
can_cast_expr<array_exprt>(expr_node) ||
can_cast_expr<array_of_exprt>(expr_node) ||
can_cast_expr<nondet_symbol_exprt>(expr_node))
{
dependent_expressions.push_back(expr_node);
Expand All @@ -79,17 +80,10 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
return dependent_expressions;
}

void smt2_incremental_decision_proceduret::define_array_function(
const array_exprt &array)
void smt2_incremental_decision_proceduret::initialize_array_elements(
const array_exprt &array,
const smt_identifier_termt &array_identifier)
{
const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
INVARIANT(
array_sort.cast<smt_array_sortt>(),
"Converting array typed expression to SMT should result in a term of array "
"sort.");
const smt_identifier_termt array_identifier = smt_identifier_termt{
"array_" + std::to_string(array_sequence()), array_sort};
solver_process->send(smt_declare_function_commandt{array_identifier, {}});
const std::vector<exprt> &elements = array.operands();
const typet &index_type = array.type().index_type();
for(std::size_t i = 0; i < elements.size(); ++i)
Expand All @@ -100,6 +94,39 @@ void smt2_incremental_decision_proceduret::define_array_function(
convert_expr_to_smt(elements.at(i)))};
solver_process->send(element_definition);
}
}

void smt2_incremental_decision_proceduret::initialize_array_elements(
const array_of_exprt &array,
const smt_identifier_termt &array_identifier)
{
const smt_sortt index_type =
convert_type_to_smt_sort(array.type().index_type());
const smt_identifier_termt array_index_identifier{
id2string(array_identifier.identifier()) + "_index", index_type};
const smt_termt element_value = convert_expr_to_smt(array.what());

const smt_assert_commandt elements_definition{smt_forall_termt{
{array_index_identifier},
smt_core_theoryt::equal(
smt_array_theoryt::select(array_identifier, array_index_identifier),
element_value)}};
solver_process->send(elements_definition);
}

template <typename t_exprt>
void smt2_incremental_decision_proceduret::define_array_function(
const t_exprt &array)
{
const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
INVARIANT(
array_sort.cast<smt_array_sortt>(),
"Converting array typed expression to SMT should result in a term of array "
"sort.");
const smt_identifier_termt array_identifier{
"array_" + std::to_string(array_sequence()), array_sort};
solver_process->send(smt_declare_function_commandt{array_identifier, {}});
initialize_array_elements(array, array_identifier);
expression_identifiers.emplace(array, array_identifier);
}

Expand Down Expand Up @@ -168,9 +195,14 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
solver_process->send(function);
}
}
if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
define_array_function(*array_expr);
if(
else if(
const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
{
define_array_function(*array_of_expr);
}
else if(
const auto nondet_symbol =
expr_try_dynamic_cast<nondet_symbol_exprt>(current))
{
Expand Down Expand Up @@ -213,8 +245,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
{
solver_process->send(
smt_set_option_commandt{smt_option_produce_modelst{true}});
solver_process->send(smt_set_logic_commandt{
smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}});
solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
solver_process->send(object_size_function.declaration);
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,29 @@ class smt2_incremental_decision_proceduret final
protected:
// Implementation of protected decision_proceduret member function.
resultt dec_solve() override;
/// \brief Defines a function of array sort and asserts the element values.
/// \brief Defines a function of array sort and asserts the element values
/// from `array_exprt` or `array_of_exprt`.
/// \details
/// The new array function identifier is added to the
/// `expression_identifiers` map.
void define_array_function(const array_exprt &array);
/// \note Statically fails if the template type is not a `array_exprt` or
/// `array_of_exprt`.
template <typename t_exprt>
void define_array_function(const t_exprt &array);
/// \brief Generate and send to the SMT solver clauses asserting that each
/// array element is as specified by \p array.
void initialize_array_elements(
const array_exprt &array,
const smt_identifier_termt &array_identifier);
/// \brief Generate and send to the SMT solver clauses asserting that each
/// array element is as specified by \p array.
/// \note This function uses a forall SMT2 term. Using it in combination with
/// arrays, bit vectors and uninterpreted functions requires the `ALL` SMT
/// logic that is not in the SMT 2.6 standard, but that it has been tested
/// working on Z3 and CVC5.
void initialize_array_elements(
const array_of_exprt &array,
const smt_identifier_termt &array_identifier);
/// \brief Defines any functions which \p expr depends on, which have not yet
/// been defined, along with their dependencies in turn.
void define_dependent_functions(const exprt &expr);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -171,9 +171,7 @@ TEST_CASE(
test.sent_commands ==
std::vector<smt_commandt>{
smt_set_option_commandt{smt_option_produce_modelst{true}},
smt_set_logic_commandt{
// NOLINTNEXTLINE(whitespace/line_length)
smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}},
smt_set_logic_commandt{smt_logic_allt{}},
test.object_size_function.declaration});
test.sent_commands.clear();
SECTION("Set symbol to true.")
Expand Down Expand Up @@ -615,5 +613,36 @@ TEST_CASE(
smt_declare_function_commandt{index_term, {}},
smt_assert_commandt{smt_core_theoryt::equal(
foo_term, smt_array_theoryt::select(array_term, index_term))}};
REQUIRE(test.sent_commands == expected_commands);
}
SECTION("array_of_exprt - all elements set to a given value")
{
const array_of_exprt array_of_expr{
from_integer(42, value_type), array_type};
test.sent_commands.clear();
test.procedure.set_to(
equal_exprt{
foo.symbol_expr(), index_exprt{array_of_expr, index.symbol_expr()}},
true);
const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{8}};
const auto array_term = smt_identifier_termt{
"array_0",
smt_array_sortt{smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}}};
const auto index_term =
smt_identifier_termt{"index", smt_bit_vector_sortt{32}};
const auto forall_term =
smt_identifier_termt{"array_0_index", smt_bit_vector_sortt{32}};
const std::vector<smt_commandt> expected_commands{
smt_declare_function_commandt{foo_term, {}},
smt_declare_function_commandt{array_term, {}},
smt_assert_commandt{smt_forall_termt{
{forall_term},
smt_core_theoryt::equal(
smt_array_theoryt::select(array_term, forall_term),
smt_bit_vector_constant_termt{42, 8})}},
smt_declare_function_commandt{index_term, {}},
smt_assert_commandt{smt_core_theoryt::equal(
foo_term, smt_array_theoryt::select(array_term, index_term))}};
REQUIRE(test.sent_commands == expected_commands);
}
}