diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index df6217d6fe0..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 93d5ee716c2..1785e0f124b 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/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; 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..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); @@ -239,7 +248,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 +450,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 +990,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()); @@ -1816,7 +1838,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); @@ -2261,6 +2284,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); @@ -2847,19 +2881,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) { @@ -2870,41 +2926,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); + CHECK_RETURN(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) - { - 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) { @@ -2948,10 +3003,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 @@ -3054,7 +3105,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) { @@ -3285,7 +3344,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 +4439,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 41f17d66fc3..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; } @@ -216,14 +218,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