Skip to content

Commit 07a18f3

Browse files
committed
Add conversion of address_of(symbol) to SMT terms
1 parent 5c56df4 commit 07a18f3

File tree

5 files changed

+191
-10
lines changed

5 files changed

+191
-10
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 52 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
#include <util/bitvector_expr.h>
55
#include <util/byte_operators.h>
66
#include <util/c_types.h>
7+
#include <util/config.h>
78
#include <util/expr.h>
89
#include <util/expr_cast.h>
910
#include <util/expr_util.h>
@@ -722,10 +723,53 @@ static smt_termt convert_expr_to_smt(
722723
}
723724
}
724725

726+
#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
727+
static mp_integer power2(unsigned exponent)
728+
{
729+
mp_integer result;
730+
result.setPower2(exponent);
731+
return result;
732+
}
733+
#endif
734+
735+
/// \details
736+
/// This conversion constructs a bit vector representation of the memory
737+
/// address. This address is composed of 2 concatenated bit vector components.
738+
/// The first part is the base object's unique identifier. The second is the
739+
/// offset into that object. For address of symbols the offset will be 0. The
740+
/// offset may be non-zero for cases such as the address of a member field of a
741+
/// struct or a the address of a non-zero index into an array.
725742
static smt_termt convert_expr_to_smt(
726743
const address_of_exprt &address_of,
727-
const sub_expression_mapt &converted)
744+
const sub_expression_mapt &converted,
745+
const smt_object_mapt &object_map)
728746
{
747+
const auto type = type_try_dynamic_cast<pointer_typet>(address_of.type());
748+
INVARIANT(
749+
type, "Result of the address_of operator should have pointer type.");
750+
const auto base = find_object_base_expression(address_of);
751+
const auto object = object_map.find(base);
752+
INVARIANT(
753+
object != object_map.end(),
754+
"Objects should be tracked before converting their address to SMT terms");
755+
const std::size_t object_id = object->second.unique_id;
756+
INVARIANT(
757+
object_id < power2(config.bv_encoding.object_bits),
758+
"There should be sufficient bits to encode unique object identifier.");
759+
const smt_termt object_bit_vector =
760+
smt_bit_vector_constant_termt{object_id, config.bv_encoding.object_bits};
761+
INVARIANT(
762+
type->get_width() > config.bv_encoding.object_bits,
763+
"Pointer should be wider than object_bits in order to allow for offset "
764+
"encoding.");
765+
const size_t offset_bits = type->get_width() - config.bv_encoding.object_bits;
766+
if(
767+
const auto symbol =
768+
expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
769+
{
770+
const smt_bit_vector_constant_termt offset{0, offset_bits};
771+
return smt_bit_vector_theoryt::concat(object_bit_vector, offset);
772+
}
729773
UNIMPLEMENTED_FEATURE(
730774
"Generation of SMT formula for address of expression: " +
731775
address_of.pretty());
@@ -1183,7 +1227,8 @@ static smt_termt convert_expr_to_smt(
11831227

11841228
static smt_termt dispatch_expr_to_smt_conversion(
11851229
const exprt &expr,
1186-
const sub_expression_mapt &converted)
1230+
const sub_expression_mapt &converted,
1231+
const smt_object_mapt &object_map)
11871232
{
11881233
if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
11891234
{
@@ -1337,7 +1382,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
13371382
#endif
13381383
if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
13391384
{
1340-
return convert_expr_to_smt(*address_of, converted);
1385+
return convert_expr_to_smt(*address_of, converted, object_map);
13411386
}
13421387
if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
13431388
{
@@ -1537,7 +1582,8 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
15371582
}
15381583
#endif
15391584

1540-
smt_termt convert_expr_to_smt(const exprt &expr)
1585+
smt_termt
1586+
convert_expr_to_smt(const exprt &expr, const smt_object_mapt &object_map)
15411587
{
15421588
#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
15431589
static bool in_conversion = false;
@@ -1554,7 +1600,8 @@ smt_termt convert_expr_to_smt(const exprt &expr)
15541600
const auto find_result = sub_expression_map.find(expr);
15551601
if(find_result != sub_expression_map.cend())
15561602
return;
1557-
smt_termt term = dispatch_expr_to_smt_conversion(expr, sub_expression_map);
1603+
smt_termt term =
1604+
dispatch_expr_to_smt_conversion(expr, sub_expression_map, object_map);
15581605
sub_expression_map.emplace_hint(find_result, expr, std::move(term));
15591606
});
15601607
return std::move(sub_expression_map.at(expr));

src/solvers/smt2_incremental/convert_expr_to_smt.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
44
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
55

6+
#include <solvers/smt2_incremental/object_tracking.h>
67
#include <solvers/smt2_incremental/smt_sorts.h>
78
#include <solvers/smt2_incremental/smt_terms.h>
89

@@ -15,6 +16,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
1516

1617
/// \brief Converts the \p expression to an smt encoding of the same expression
1718
/// stored as term ast (abstract syntax tree).
18-
smt_termt convert_expr_to_smt(const exprt &expression);
19+
smt_termt
20+
convert_expr_to_smt(const exprt &expression, const smt_object_mapt &object_map);
1921

2022
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,8 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
132132
: ns{_ns},
133133
number_of_solver_calls{0},
134134
solver_process(std::move(_solver_process)),
135-
log{message_handler}
135+
log{message_handler},
136+
object_map{initial_smt_object_map()}
136137
{
137138
solver_process->send(
138139
smt_set_option_commandt{smt_option_produce_modelst{true}});
@@ -157,6 +158,13 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
157158
solver_process->send(function);
158159
}
159160

161+
smt_termt
162+
smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
163+
{
164+
track_expression_objects(expr, ns, object_map);
165+
return ::convert_expr_to_smt(expr, object_map);
166+
}
167+
160168
exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
161169
{
162170
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
@@ -193,7 +201,11 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
193201
{
194202
if(gather_dependent_expressions(expr).empty())
195203
{
196-
descriptor = convert_expr_to_smt(expr);
204+
INVARIANT(
205+
objects_are_already_tracked(expr, object_map),
206+
"Objects in expressions being read should already be tracked from "
207+
"point of being set/handled.");
208+
descriptor = ::convert_expr_to_smt(expr, object_map);
197209
}
198210
else
199211
{

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,13 @@
66
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
77
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
88

9-
#include <solvers/smt2_incremental/smt_terms.h>
10-
#include <solvers/stack_decision_procedure.h>
119
#include <util/message.h>
1210
#include <util/std_expr.h>
1311

12+
#include <solvers/smt2_incremental/object_tracking.h>
13+
#include <solvers/smt2_incremental/smt_terms.h>
14+
#include <solvers/stack_decision_procedure.h>
15+
1416
#include <memory>
1517
#include <unordered_map>
1618
#include <unordered_set>
@@ -55,6 +57,9 @@ class smt2_incremental_decision_proceduret final
5557
/// been defined, along with their dependencies in turn.
5658
void define_dependent_functions(const exprt &expr);
5759
void ensure_handle_for_expr_defined(const exprt &expr);
60+
/// \brief Add objects in \p expr to object_map if needed and convert to smt.
61+
/// \note This function is non-const because it mutates the object_map.
62+
smt_termt convert_expr_to_smt(const exprt &expr);
5863

5964
const namespacet &ns;
6065

@@ -78,6 +83,7 @@ class smt2_incremental_decision_proceduret final
7883
expression_handle_identifiers;
7984
std::unordered_map<exprt, smt_identifier_termt, irep_hash>
8085
expression_identifiers;
86+
smt_object_mapt object_map;
8187
};
8288

8389
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,17 @@
77
#include <util/config.h>
88
#include <util/constructor_of.h>
99
#include <util/format.h>
10+
#include <util/namespace.h>
1011
#include <util/std_expr.h>
12+
#include <util/symbol_table.h>
1113

1214
#include <solvers/smt2_incremental/convert_expr_to_smt.h>
15+
#include <solvers/smt2_incremental/object_tracking.h>
1316
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
1417
#include <solvers/smt2_incremental/smt_core_theory.h>
1518
#include <solvers/smt2_incremental/smt_terms.h>
1619
#include <solvers/smt2_incremental/smt_to_smt2_string.h>
20+
#include <testing-utils/invariant.h>
1721
#include <testing-utils/use_catch.h>
1822

1923
TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
@@ -38,6 +42,11 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
3842
}
3943
}
4044

45+
smt_termt convert_expr_to_smt(const exprt &expression)
46+
{
47+
return convert_expr_to_smt(expression, initial_smt_object_map());
48+
}
49+
4150
TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
4251
{
4352
CHECK(
@@ -1058,3 +1067,108 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
10581067
}
10591068
}
10601069
}
1070+
1071+
TEST_CASE(
1072+
"expr to smt conversion for address of operator",
1073+
"[core][smt2_incremental]")
1074+
{
1075+
// The config lines are necessary to ensure that pointer width in configured.
1076+
config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
1077+
config.ansi_c.set_arch_spec_x86_64();
1078+
const symbol_tablet symbol_table;
1079+
const namespacet ns{symbol_table};
1080+
smt_object_mapt object_map = initial_smt_object_map();
1081+
const symbol_exprt foo{"foo", unsignedbv_typet{32}};
1082+
const symbol_exprt bar{"bar", unsignedbv_typet{32}};
1083+
SECTION("Address of symbol")
1084+
{
1085+
const address_of_exprt address_of_foo{foo};
1086+
track_expression_objects(address_of_foo, ns, object_map);
1087+
INFO("Expression " + address_of_foo.pretty(1, 0));
1088+
SECTION("8 object bits")
1089+
{
1090+
config.bv_encoding.object_bits = 8;
1091+
const auto converted = convert_expr_to_smt(address_of_foo, object_map);
1092+
CHECK(object_map.at(foo).unique_id == 1);
1093+
CHECK(
1094+
converted == smt_bit_vector_theoryt::concat(
1095+
smt_bit_vector_constant_termt{1, 8},
1096+
smt_bit_vector_constant_termt{0, 56}));
1097+
}
1098+
SECTION("16 object bits")
1099+
{
1100+
config.bv_encoding.object_bits = 16;
1101+
const auto converted = convert_expr_to_smt(address_of_foo, object_map);
1102+
CHECK(object_map.at(foo).unique_id == 1);
1103+
CHECK(
1104+
converted == smt_bit_vector_theoryt::concat(
1105+
smt_bit_vector_constant_termt{1, 16},
1106+
smt_bit_vector_constant_termt{0, 48}));
1107+
}
1108+
}
1109+
SECTION("Invariant checks")
1110+
{
1111+
const cbmc_invariants_should_throwt invariants_throw;
1112+
SECTION("Address of should result in a pointer")
1113+
{
1114+
exprt address_of = address_of_exprt{foo};
1115+
address_of.type() = bool_typet{};
1116+
REQUIRE_THROWS_MATCHES(
1117+
convert_expr_to_smt(address_of, object_map),
1118+
invariant_failedt,
1119+
invariant_failure_containing(
1120+
"Result of the address_of operator should have pointer type."));
1121+
}
1122+
SECTION("Objects should already be tracked")
1123+
{
1124+
REQUIRE_THROWS_MATCHES(
1125+
convert_expr_to_smt(address_of_exprt{foo}, object_map),
1126+
invariant_failedt,
1127+
invariant_failure_containing("Objects should be tracked before "
1128+
"converting their address to SMT terms"));
1129+
}
1130+
SECTION("There should be enough bits for object id")
1131+
{
1132+
config.bv_encoding.object_bits = 8;
1133+
const address_of_exprt address_of_foo{foo};
1134+
track_expression_objects(address_of_foo, ns, object_map);
1135+
object_map.at(foo).unique_id = 256;
1136+
REQUIRE_THROWS_MATCHES(
1137+
convert_expr_to_smt(address_of_exprt{foo}, object_map),
1138+
invariant_failedt,
1139+
invariant_failure_containing("There should be sufficient bits to "
1140+
"encode unique object identifier."));
1141+
}
1142+
SECTION("Pointer should be wide enough to encode offset")
1143+
{
1144+
config.bv_encoding.object_bits = 64;
1145+
const address_of_exprt address_of_foo{foo};
1146+
track_expression_objects(address_of_foo, ns, object_map);
1147+
object_map.at(foo).unique_id = 256;
1148+
REQUIRE_THROWS_MATCHES(
1149+
convert_expr_to_smt(address_of_exprt{foo}, object_map),
1150+
invariant_failedt,
1151+
invariant_failure_containing("Pointer should be wider than object_bits "
1152+
"in order to allow for offset encoding."));
1153+
}
1154+
}
1155+
SECTION("Comparison of address of operations.")
1156+
{
1157+
config.bv_encoding.object_bits = 8;
1158+
const exprt comparison =
1159+
notequal_exprt{address_of_exprt{foo}, address_of_exprt{bar}};
1160+
track_expression_objects(comparison, ns, object_map);
1161+
INFO("Expression " + comparison.pretty(1, 0));
1162+
const auto converted = convert_expr_to_smt(comparison, object_map);
1163+
CHECK(object_map.at(foo).unique_id == 2);
1164+
CHECK(object_map.at(bar).unique_id == 1);
1165+
CHECK(
1166+
converted == smt_core_theoryt::distinct(
1167+
smt_bit_vector_theoryt::concat(
1168+
smt_bit_vector_constant_termt{2, 8},
1169+
smt_bit_vector_constant_termt{0, 56}),
1170+
smt_bit_vector_theoryt::concat(
1171+
smt_bit_vector_constant_termt{1, 8},
1172+
smt_bit_vector_constant_termt{0, 56})));
1173+
}
1174+
}

0 commit comments

Comments
 (0)