Skip to content

Commit 6d657a0

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1779 from diffblue/smt2-integers
SMT2 support for unbounded integers
2 parents 0fc9c5e + 897e29e commit 6d657a0

File tree

9 files changed

+147
-62
lines changed

9 files changed

+147
-62
lines changed

‎regression/CMakeLists.txt

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
33
macro(add_test_pl_profile name cmdline flag profile)
44
add_test(
55
NAME "${name}-${profile}"
6-
COMMAND ${test_pl_path} -p -c ${cmdline} ${flag}
6+
COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
77
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
88
)
99
set_tests_properties("${name}-${profile}" PROPERTIES
@@ -14,10 +14,10 @@ endmacro(add_test_pl_profile)
1414
macro(add_test_pl_tests cmdline)
1515
get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
1616
message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
17-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE)
18-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH)
19-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE)
20-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG)
17+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
18+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
19+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
20+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
2121
endmacro(add_test_pl_tests)
2222

2323
add_subdirectory(ansi-c)

‎regression/cbmc/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
2+
"$<TARGET_FILE:cbmc>" -X smt-backend
33
)

‎regression/cbmc/Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
88

99
show:
1010
@for dir in *; do \

‎regression/cbmc/integer-assignments1/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
__CPROVER_integer a, b;
4+
a=0;
5+
b=a;
6+
b++;
7+
b*=100;
8+
__CPROVER_assert(0, "");
9+
}

‎regression/cbmc/integer-assignments1/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE smt-backend
2+
main.c
3+
--trace --smt2
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^ b=100
7+
--

‎src/ansi-c/c_typecheck_base.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,9 @@ class c_typecheck_baset:
265265
src.id()==ID_c_bool ||
266266
src.id()==ID_bool ||
267267
src.id()==ID_c_enum_tag ||
268-
src.id()==ID_c_bit_field;
268+
src.id()==ID_c_bit_field ||
269+
src.id()==ID_integer ||
270+
src.id()==ID_real;
269271
}
270272

271273
typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> asm_label_mapt;

‎src/goto-programs/goto_trace.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,12 @@ std::string trace_value_binary(
143143
{
144144
return expr.is_true()?"1":"0";
145145
}
146+
else if(type.id()==ID_integer)
147+
{
148+
mp_integer i;
149+
if(!to_integer(expr, i) && i>=0)
150+
return integer2string(i, 2);
151+
}
146152
}
147153
else if(expr.id()==ID_array)
148154
{

‎src/solvers/smt2/smt2_conv.cpp

+109-47
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,15 @@ exprt smt2_convt::get(const exprt &expr) const
189189
if(it!=identifier_map.end())
190190
return it->second.value;
191191
}
192+
else if(expr.id()==ID_nondet_symbol)
193+
{
194+
const irep_idt &id=to_nondet_symbol_expr(expr).get_identifier();
195+
196+
identifier_mapt::const_iterator it=identifier_map.find(id);
197+
198+
if(it!=identifier_map.end())
199+
return it->second.value;
200+
}
192201
else if(expr.id()==ID_member)
193202
{
194203
const member_exprt &member_expr=to_member_expr(expr);
@@ -239,7 +248,15 @@ constant_exprt smt2_convt::parse_literal(
239248
value=string2integer(s.substr(2), 16);
240249
}
241250
else
242-
PARSERERROR("smt2_convt::parse_literal can't parse \""+s+"\"");
251+
{
252+
// Numeral
253+
value=string2integer(s);
254+
}
255+
}
256+
else if(src.get_sub().size()==2 &&
257+
src.get_sub()[0].id()=="-") // (- 100)
258+
{
259+
value=-string2integer(src.get_sub()[1].id_string());
243260
}
244261
else if(src.get_sub().size()==3 &&
245262
src.get_sub()[0].id()=="_" &&
@@ -433,6 +450,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
433450

434451
if(type.id()==ID_signedbv ||
435452
type.id()==ID_unsignedbv ||
453+
type.id()==ID_integer ||
454+
type.id()==ID_rational ||
455+
type.id()==ID_real ||
436456
type.id()==ID_bv ||
437457
type.id()==ID_fixedbv ||
438458
type.id()==ID_floatbv)
@@ -970,7 +990,9 @@ void smt2_convt::convert_expr(const exprt &expr)
970990
{
971991
assert(expr.operands().size()==1);
972992

973-
if(expr.type().id()==ID_rational)
993+
if(expr.type().id()==ID_rational ||
994+
expr.type().id()==ID_integer ||
995+
expr.type().id()==ID_real)
974996
{
975997
out << "(- ";
976998
convert_expr(expr.op0());
@@ -1816,7 +1838,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
18161838
src_type.id()==ID_unsignedbv ||
18171839
src_type.id()==ID_c_bool ||
18181840
src_type.id()==ID_fixedbv ||
1819-
src_type.id()==ID_pointer)
1841+
src_type.id()==ID_pointer ||
1842+
src_type.id()==ID_integer)
18201843
{
18211844
out << "(not (= ";
18221845
convert_expr(src);
@@ -2261,6 +2284,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
22612284
else
22622285
UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
22632286
}
2287+
else if(dest_type.id()==ID_integer)
2288+
{
2289+
if(src_type.id()==ID_bool)
2290+
{
2291+
out << "(ite ";
2292+
convert_expr(src);
2293+
out <<" 1 0)";
2294+
}
2295+
else
2296+
UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2297+
}
22642298
else if(dest_type.id()==ID_c_bit_field)
22652299
{
22662300
std::size_t from_width=boolbv_width(src_type);
@@ -2847,19 +2881,41 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
28472881
{
28482882
convert_expr(expr.op0());
28492883
}
2850-
else if(expr.operands().size()==2)
2884+
else
28512885
{
2852-
if(expr.type().id()==ID_unsignedbv ||
2853-
expr.type().id()==ID_signedbv ||
2854-
expr.type().id()==ID_fixedbv)
2886+
if(expr.type().id()==ID_rational ||
2887+
expr.type().id()==ID_integer ||
2888+
expr.type().id()==ID_real)
2889+
{
2890+
// these are multi-ary in SMT-LIB2
2891+
out << "(+";
2892+
2893+
for(const auto &op : expr.operands())
2894+
{
2895+
out << ' ';
2896+
convert_expr(op);
2897+
}
2898+
2899+
out << ')';
2900+
}
2901+
else if(expr.type().id()==ID_unsignedbv ||
2902+
expr.type().id()==ID_signedbv ||
2903+
expr.type().id()==ID_fixedbv)
28552904
{
28562905
// These could be chained, i.e., need not be binary,
28572906
// but at least MathSat doesn't like that.
2858-
out << "(bvadd ";
2859-
convert_expr(expr.op0());
2860-
out << " ";
2861-
convert_expr(expr.op1());
2862-
out << ")";
2907+
if(expr.operands().size()==2)
2908+
{
2909+
out << "(bvadd ";
2910+
convert_expr(expr.op0());
2911+
out << " ";
2912+
convert_expr(expr.op1());
2913+
out << ")";
2914+
}
2915+
else
2916+
{
2917+
convert_plus(to_plus_expr(make_binary(expr)));
2918+
}
28632919
}
28642920
else if(expr.type().id()==ID_floatbv)
28652921
{
@@ -2870,41 +2926,40 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
28702926
}
28712927
else if(expr.type().id()==ID_pointer)
28722928
{
2873-
exprt p=expr.op0(), i=expr.op1();
2929+
if(expr.operands().size()==2)
2930+
{
2931+
exprt p=expr.op0(), i=expr.op1();
28742932

2875-
if(p.type().id()!=ID_pointer)
2876-
p.swap(i);
2933+
if(p.type().id()!=ID_pointer)
2934+
p.swap(i);
28772935

2878-
if(p.type().id()!=ID_pointer)
2879-
INVALIDEXPR("unexpected mixture in pointer arithmetic");
2936+
if(p.type().id()!=ID_pointer)
2937+
INVALIDEXPR("unexpected mixture in pointer arithmetic");
28802938

2881-
mp_integer element_size=
2882-
pointer_offset_size(expr.type().subtype(), ns);
2883-
assert(element_size>0);
2939+
mp_integer element_size=
2940+
pointer_offset_size(expr.type().subtype(), ns);
2941+
CHECK_RETURN(element_size>0);
28842942

2885-
out << "(bvadd ";
2886-
convert_expr(p);
2887-
out << " ";
2943+
out << "(bvadd ";
2944+
convert_expr(p);
2945+
out << " ";
28882946

2889-
if(element_size>=2)
2890-
{
2891-
out << "(bvmul ";
2892-
convert_expr(i);
2893-
out << " (_ bv" << element_size
2894-
<< " " << boolbv_width(expr.type()) << "))";
2947+
if(element_size>=2)
2948+
{
2949+
out << "(bvmul ";
2950+
convert_expr(i);
2951+
out << " (_ bv" << element_size
2952+
<< " " << boolbv_width(expr.type()) << "))";
2953+
}
2954+
else
2955+
convert_expr(i);
2956+
2957+
out << ')';
28952958
}
28962959
else
2897-
convert_expr(i);
2898-
2899-
out << ")";
2900-
}
2901-
else if(expr.type().id()==ID_rational)
2902-
{
2903-
out << "(+";
2904-
convert_expr(expr.op0());
2905-
out << " ";
2906-
convert_expr(expr.op1());
2907-
out << ")";
2960+
{
2961+
convert_plus(to_plus_expr(make_binary(expr)));
2962+
}
29082963
}
29092964
else if(expr.type().id()==ID_vector)
29102965
{
@@ -2948,10 +3003,6 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
29483003
else
29493004
UNEXPECTEDCASE("unsupported type for +: "+expr.type().id_string());
29503005
}
2951-
else
2952-
{
2953-
convert_plus(to_plus_expr(make_binary(expr)));
2954-
}
29553006
}
29563007

29573008
/// Converting a constant or symbolic rounding mode to SMT-LIB. Only called when
@@ -3054,7 +3105,15 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
30543105
{
30553106
assert(expr.operands().size()==2);
30563107

3057-
if(expr.type().id()==ID_unsignedbv ||
3108+
if(expr.type().id()==ID_integer)
3109+
{
3110+
out << "(- ";
3111+
convert_expr(expr.op0());
3112+
out << " ";
3113+
convert_expr(expr.op1());
3114+
out << ")";
3115+
}
3116+
else if(expr.type().id()==ID_unsignedbv ||
30583117
expr.type().id()==ID_signedbv ||
30593118
expr.type().id()==ID_fixedbv)
30603119
{
@@ -3285,7 +3344,9 @@ void smt2_convt::convert_mult(const mult_exprt &expr)
32853344

32863345
out << "))"; // bvmul, extract
32873346
}
3288-
else if(expr.type().id()==ID_rational)
3347+
else if(expr.type().id()==ID_rational ||
3348+
expr.type().id()==ID_integer ||
3349+
expr.type().id()==ID_real)
32893350
{
32903351
out << "(*";
32913352

@@ -4378,7 +4439,8 @@ void smt2_convt::convert_type(const typet &type)
43784439
out << "(_ BitVec "
43794440
<< floatbv_type.get_width() << ")";
43804441
}
4381-
else if(type.id()==ID_rational)
4442+
else if(type.id()==ID_rational ||
4443+
type.id()==ID_real)
43824444
out << "Real";
43834445
else if(type.id()==ID_integer)
43844446
out << "Int";

‎src/solvers/smt2/smt2_dec.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -198,6 +198,8 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
198198
// Examples:
199199
// ( (B0 true) )
200200
// ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
201+
// ( (|some_integer| 0) )
202+
// ( (|some_integer| (- 10)) )
201203

202204
values[s0.id()]=s1;
203205
}
@@ -216,14 +218,11 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
216218
}
217219
}
218220

219-
for(identifier_mapt::iterator
220-
it=identifier_map.begin();
221-
it!=identifier_map.end();
222-
it++)
221+
for(auto &assignment : identifier_map)
223222
{
224-
std::string conv_id=convert_identifier(it->first);
223+
std::string conv_id=convert_identifier(assignment.first);
225224
const irept &value=values[conv_id];
226-
it->second.value=parse_rec(value, it->second.type);
225+
assignment.second.value=parse_rec(value, assignment.second.type);
227226
}
228227

229228
// Booleans

0 commit comments

Comments
 (0)