From 698ccdd1c2d100049410293de73e696892f046ec Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 29 Jan 2018 20:01:41 +0000 Subject: [PATCH 1/7] use a ranged for --- src/solvers/smt2/smt2_dec.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 41f17d66fc3..71deddfbc6d 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -216,14 +216,11 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) } } - for(identifier_mapt::iterator - it=identifier_map.begin(); - it!=identifier_map.end(); - it++) + for(auto &assignment : identifier_map) { - std::string conv_id=convert_identifier(it->first); + std::string conv_id=convert_identifier(assignment.first); const irept &value=values[conv_id]; - it->second.value=parse_rec(value, it->second.type); + assignment.second.value=parse_rec(value, assignment.second.type); } // Booleans From 12ae728634987e606028358ddcdc28297aa4d22e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 29 Jan 2018 20:19:44 +0000 Subject: [PATCH 2/7] fixes for integers in SMT2 This fixes output of formulas into SMT2 format that contain unbounded integers; conversely, values in satisfying assignments generated by SMT2 solvers that contain unbounded integers are now parsed. --- src/goto-programs/goto_trace.cpp | 6 ++++++ src/solvers/smt2/smt2_conv.cpp | 30 ++++++++++++++++++++++++------ src/solvers/smt2/smt2_dec.cpp | 2 ++ 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 651db1fef48..d93fc3f7055 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -143,6 +143,12 @@ std::string trace_value_binary( { return expr.is_true()?"1":"0"; } + else if(type.id()==ID_integer) + { + mp_integer i; + if(!to_integer(expr, i) && i>=0) + return integer2string(i, 2); + } } else if(expr.id()==ID_array) { diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 71b35530150..58039ede5b4 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -239,7 +239,15 @@ constant_exprt smt2_convt::parse_literal( value=string2integer(s.substr(2), 16); } else - PARSERERROR("smt2_convt::parse_literal can't parse \""+s+"\""); + { + // Numeral + value=string2integer(s); + } + } + else if(src.get_sub().size()==2 && + src.get_sub()[0].id()=="-") // (- 100) + { + value=-string2integer(src.get_sub()[1].id_string()); } else if(src.get_sub().size()==3 && src.get_sub()[0].id()=="_" && @@ -433,6 +441,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type) if(type.id()==ID_signedbv || type.id()==ID_unsignedbv || + type.id()==ID_integer || + type.id()==ID_rational || + type.id()==ID_real || type.id()==ID_bv || type.id()==ID_fixedbv || type.id()==ID_floatbv) @@ -970,7 +981,9 @@ void smt2_convt::convert_expr(const exprt &expr) { assert(expr.operands().size()==1); - if(expr.type().id()==ID_rational) + if(expr.type().id()==ID_rational || + expr.type().id()==ID_integer || + expr.type().id()==ID_real) { out << "(- "; convert_expr(expr.op0()); @@ -2898,9 +2911,11 @@ void smt2_convt::convert_plus(const plus_exprt &expr) out << ")"; } - else if(expr.type().id()==ID_rational) + else if(expr.type().id()==ID_rational || + expr.type().id()==ID_integer || + expr.type().id()==ID_real) { - out << "(+"; + out << "(+ "; convert_expr(expr.op0()); out << " "; convert_expr(expr.op1()); @@ -3285,7 +3300,9 @@ void smt2_convt::convert_mult(const mult_exprt &expr) out << "))"; // bvmul, extract } - else if(expr.type().id()==ID_rational) + else if(expr.type().id()==ID_rational || + expr.type().id()==ID_integer || + expr.type().id()==ID_real) { out << "(*"; @@ -4378,7 +4395,8 @@ void smt2_convt::convert_type(const typet &type) out << "(_ BitVec " << floatbv_type.get_width() << ")"; } - else if(type.id()==ID_rational) + else if(type.id()==ID_rational || + type.id()==ID_real) out << "Real"; else if(type.id()==ID_integer) out << "Int"; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 71deddfbc6d..f0473da4a6d 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -198,6 +198,8 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) // Examples: // ( (B0 true) ) // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) ) + // ( (|some_integer| 0) ) + // ( (|some_integer| (- 10)) ) values[s0.id()]=s1; } From 57ecf15ab03f7f854535bf84bcce2c4a1b4c35e8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 30 Jan 2018 13:14:25 +0000 Subject: [PATCH 3/7] + is multi-ary in SMT-LIB2 --- src/solvers/smt2/smt2_conv.cpp | 101 +++++++++++++++++++-------------- 1 file changed, 58 insertions(+), 43 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 58039ede5b4..a1ea20922a2 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2860,19 +2860,41 @@ void smt2_convt::convert_plus(const plus_exprt &expr) { convert_expr(expr.op0()); } - else if(expr.operands().size()==2) + else { - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv || - expr.type().id()==ID_fixedbv) + if(expr.type().id()==ID_rational || + expr.type().id()==ID_integer || + expr.type().id()==ID_real) + { + // these are multi-ary in SMT-LIB2 + out << "(+"; + + for(const auto &op : expr.operands()) + { + out << ' '; + convert_expr(op); + } + + out << ')'; + } + else if(expr.type().id()==ID_unsignedbv || + expr.type().id()==ID_signedbv || + expr.type().id()==ID_fixedbv) { // These could be chained, i.e., need not be binary, // but at least MathSat doesn't like that. - out << "(bvadd "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + if(expr.operands().size()==2) + { + out << "(bvadd "; + convert_expr(expr.op0()); + out << " "; + convert_expr(expr.op1()); + out << ")"; + } + else + { + convert_plus(to_plus_expr(make_binary(expr))); + } } else if(expr.type().id()==ID_floatbv) { @@ -2883,43 +2905,40 @@ void smt2_convt::convert_plus(const plus_exprt &expr) } else if(expr.type().id()==ID_pointer) { - exprt p=expr.op0(), i=expr.op1(); + if(expr.operands().size()==2) + { + exprt p=expr.op0(), i=expr.op1(); - if(p.type().id()!=ID_pointer) - p.swap(i); + if(p.type().id()!=ID_pointer) + p.swap(i); - if(p.type().id()!=ID_pointer) - INVALIDEXPR("unexpected mixture in pointer arithmetic"); + if(p.type().id()!=ID_pointer) + INVALIDEXPR("unexpected mixture in pointer arithmetic"); - mp_integer element_size= - pointer_offset_size(expr.type().subtype(), ns); - assert(element_size>0); + mp_integer element_size= + pointer_offset_size(expr.type().subtype(), ns); + assert(element_size>0); - out << "(bvadd "; - convert_expr(p); - out << " "; + out << "(bvadd "; + convert_expr(p); + out << " "; - if(element_size>=2) - { - out << "(bvmul "; - convert_expr(i); - out << " (_ bv" << element_size - << " " << boolbv_width(expr.type()) << "))"; + if(element_size>=2) + { + out << "(bvmul "; + convert_expr(i); + out << " (_ bv" << element_size + << " " << boolbv_width(expr.type()) << "))"; + } + else + convert_expr(i); + + out << ')'; } else - convert_expr(i); - - out << ")"; - } - else if(expr.type().id()==ID_rational || - expr.type().id()==ID_integer || - expr.type().id()==ID_real) - { - out << "(+ "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + { + convert_plus(to_plus_expr(make_binary(expr))); + } } else if(expr.type().id()==ID_vector) { @@ -2963,10 +2982,6 @@ void smt2_convt::convert_plus(const plus_exprt &expr) else UNEXPECTEDCASE("unsupported type for +: "+expr.type().id_string()); } - else - { - convert_plus(to_plus_expr(make_binary(expr))); - } } /// Converting a constant or symbolic rounding mode to SMT-LIB. Only called when From dea25928f895d014d73de34d464f5ef3d6ee0bf6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 12 Feb 2018 12:12:05 +0000 Subject: [PATCH 4/7] treat real and integer as 'numeric' in C front-end --- src/ansi-c/c_typecheck_base.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index ba6829bda05..cc2b68afa9b 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -265,7 +265,9 @@ class c_typecheck_baset: src.id()==ID_c_bool || src.id()==ID_bool || src.id()==ID_c_enum_tag || - src.id()==ID_c_bit_field; + src.id()==ID_c_bit_field || + src.id()==ID_integer || + src.id()==ID_real; } typedef std::unordered_map asm_label_mapt; From a827c77a161004496f11d0ae02413879a6c658ef Mon Sep 17 00:00:00 2001 From: polgreen Date: Tue, 30 Jan 2018 12:29:56 +0000 Subject: [PATCH 5/7] fix: add missing integer casts and operations adds: integer->bool cast bool -> integer cast integer minus operation --- regression/CMakeLists.txt | 8 +++--- regression/cbmc/CMakeLists.txt | 2 +- regression/cbmc/Makefile | 4 +-- regression/cbmc/integer-assignments1/main.c | 9 +++++++ .../cbmc/integer-assignments1/test.desc | 7 +++++ src/solvers/smt2/smt2_conv.cpp | 26 ++++++++++++++++--- 6 files changed, 46 insertions(+), 10 deletions(-) create mode 100644 regression/cbmc/integer-assignments1/main.c create mode 100644 regression/cbmc/integer-assignments1/test.desc diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index df6217d6fe0..dac3ae5514e 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -14,10 +14,10 @@ endmacro(add_test_pl_profile) macro(add_test_pl_tests cmdline) get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME) message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}") - add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE) - add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH) - add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE) - add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG) + add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -C CORE) + add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -T THOROUGH) + add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -F FUTURE) + add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -K KNOWNBUG) endmacro(add_test_pl_tests) add_subdirectory(ansi-c) diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 93d5ee716c2..7ae67e630f9 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + $ -X smt-backend ) diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile index 486a8c750f7..8096fc27cb3 100644 --- a/regression/cbmc/Makefile +++ b/regression/cbmc/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -p -c ../../../src/cbmc/cbmc + @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend tests.log: ../test.pl - @../test.pl -p -c ../../../src/cbmc/cbmc + @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend show: @for dir in *; do \ diff --git a/regression/cbmc/integer-assignments1/main.c b/regression/cbmc/integer-assignments1/main.c new file mode 100644 index 00000000000..c538edf7efc --- /dev/null +++ b/regression/cbmc/integer-assignments1/main.c @@ -0,0 +1,9 @@ +int main() +{ + __CPROVER_integer a, b; + a=0; + b=a; + b++; + b*=100; + __CPROVER_assert(0, ""); +} diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc new file mode 100644 index 00000000000..d8bae11e7af --- /dev/null +++ b/regression/cbmc/integer-assignments1/test.desc @@ -0,0 +1,7 @@ +CORE smt-backend +main.c +--trace --smt2 +^EXIT=10$ +^SIGNAL=0$ +^ b=100 +-- diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index a1ea20922a2..f43808749b8 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1829,7 +1829,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) src_type.id()==ID_unsignedbv || src_type.id()==ID_c_bool || src_type.id()==ID_fixedbv || - src_type.id()==ID_pointer) + src_type.id()==ID_pointer || + src_type.id()==ID_integer) { out << "(not (= "; convert_expr(src); @@ -2274,6 +2275,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float"); } + else if(dest_type.id()==ID_integer) + { + if(src_type.id()==ID_bool) + { + out << "(ite "; + convert_expr(src); + out <<" 1 0)"; + } + else + UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer"); + } else if(dest_type.id()==ID_c_bit_field) { std::size_t from_width=boolbv_width(src_type); @@ -2917,7 +2929,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr) mp_integer element_size= pointer_offset_size(expr.type().subtype(), ns); - assert(element_size>0); + CHECK_RETURN(element_size>0); out << "(bvadd "; convert_expr(p); @@ -3084,7 +3096,15 @@ void smt2_convt::convert_minus(const minus_exprt &expr) { assert(expr.operands().size()==2); - if(expr.type().id()==ID_unsignedbv || + if(expr.type().id()==ID_integer) + { + out << "(- "; + convert_expr(expr.op0()); + out << " "; + convert_expr(expr.op1()); + out << ")"; + } + else if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv || expr.type().id()==ID_fixedbv) { From 1ebec11850fb4a1fcaa8644014e4cbe372f3e160 Mon Sep 17 00:00:00 2001 From: polgreen Date: Mon, 29 Jan 2018 21:12:25 +0000 Subject: [PATCH 6/7] get values for nondet symbols --- src/solvers/smt2/smt2_conv.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f43808749b8..0fc06e7112e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -189,6 +189,15 @@ exprt smt2_convt::get(const exprt &expr) const if(it!=identifier_map.end()) return it->second.value; } + else if(expr.id()==ID_nondet_symbol) + { + const irep_idt &id=to_nondet_symbol_expr(expr).get_identifier(); + + identifier_mapt::const_iterator it=identifier_map.find(id); + + if(it!=identifier_map.end()) + return it->second.value; + } else if(expr.id()==ID_member) { const member_exprt &member_expr=to_member_expr(expr); From 897e29e874aace55bf171895866334ffe4cd7b28 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Mon, 19 Feb 2018 15:52:38 +0000 Subject: [PATCH 7/7] Fix CMakeLists to correctly pass test exclusion flags --- regression/CMakeLists.txt | 10 +++++----- regression/cbmc/CMakeLists.txt | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index dac3ae5514e..9b22e036e09 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl") macro(add_test_pl_profile name cmdline flag profile) add_test( NAME "${name}-${profile}" - COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} + COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN} WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" ) set_tests_properties("${name}-${profile}" PROPERTIES @@ -14,10 +14,10 @@ endmacro(add_test_pl_profile) macro(add_test_pl_tests cmdline) get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME) message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}") - add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -C CORE) - add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -T THOROUGH) - add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -F FUTURE) - add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -K KNOWNBUG) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN}) endmacro(add_test_pl_tests) add_subdirectory(ansi-c) diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 7ae67e630f9..1785e0f124b 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - $ -X smt-backend + "$" -X smt-backend )