diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e7189f965d1..3eb08b6fd9a 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -312,100 +312,64 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("aig", true); // SMT Options - bool version_set=false; if(cmdline.isset("smt1")) { - options.set_option("smt1", true); - options.set_option("smt2", false); - version_set=true; + error() << "--smt1 is no longer supported" << eom; + exit(CPROVER_EXIT_USAGE_ERROR); } if(cmdline.isset("smt2")) - { - // If both are given, smt2 takes precedence - options.set_option("smt1", false); options.set_option("smt2", true); - version_set=true; - } if(cmdline.isset("fpa")) options.set_option("fpa", true); - bool solver_set=false; if(cmdline.isset("boolector")) { options.set_option("boolector", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("mathsat")) { options.set_option("mathsat", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; - } - - if(cmdline.isset("cvc3")) - { - options.set_option("cvc3", true), solver_set=true; - if(!version_set) - options.set_option("smt1", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("cvc4")) { options.set_option("cvc4", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("yices")) { options.set_option("yices", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; + options.set_option("smt2", true); } if(cmdline.isset("z3")) { options.set_option("z3", true), solver_set=true; - if(!version_set) - options.set_option("smt2", true), version_set=true; - } - - if(cmdline.isset("opensmt")) - { - options.set_option("opensmt", true), solver_set=true; - if(!version_set) - options.set_option("smt1", true), version_set=true; + options.set_option("smt2", true); } - if(version_set && !solver_set) + if(cmdline.isset("smt2") && !solver_set) { if(cmdline.isset("outfile")) { // outfile and no solver should give standard compliant SMT-LIB - options.set_option("generic", true), solver_set=true; + options.set_option("generic", true); } else { - if(options.get_bool_option("smt1")) - { - options.set_option("boolector", true), solver_set=true; - } - else - { - PRECONDITION(options.get_bool_option("smt2")); - options.set_option("z3", true), solver_set=true; - } + // the default smt2 solver + options.set_option("z3", true); } } - // Either have solver and standard version set, or neither. - PRECONDITION(version_set == solver_set); if(cmdline.isset("beautify")) options.set_option("beautify", true); diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index ed5787af6d3..e5a29ba7fe6 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -32,34 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "counterexample_beautification.h" #include "version.h" -/// Uses the options to pick an SMT 1.2 solver -/// \return An smt1_dect::solvert giving the solver to use. -smt1_dect::solvert cbmc_solverst::get_smt1_solver_type() const -{ - assert(options.get_bool_option("smt1")); - - smt1_dect::solvert s=smt1_dect::solvert::GENERIC; - - if(options.get_bool_option("boolector")) - s=smt1_dect::solvert::BOOLECTOR; - else if(options.get_bool_option("mathsat")) - s=smt1_dect::solvert::MATHSAT; - else if(options.get_bool_option("cvc3")) - s=smt1_dect::solvert::CVC3; - else if(options.get_bool_option("cvc4")) - s=smt1_dect::solvert::CVC4; - else if(options.get_bool_option("opensmt")) - s=smt1_dect::solvert::OPENSMT; - else if(options.get_bool_option("yices")) - s=smt1_dect::solvert::YICES; - else if(options.get_bool_option("z3")) - s=smt1_dect::solvert::Z3; - else if(options.get_bool_option("generic")) - s=smt1_dect::solvert::GENERIC; - - return s; -} - /// Uses the options to pick an SMT 2.0 solver /// \return An smt2_dect::solvert giving the solver to use. smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const @@ -76,8 +47,6 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const s=smt2_dect::solvert::CVC3; else if(options.get_bool_option("cvc4")) s=smt2_dect::solvert::CVC4; - else if(options.get_bool_option("opensmt")) - s=smt2_dect::solvert::OPENSMT; else if(options.get_bool_option("yices")) s=smt2_dect::solvert::YICES; else if(options.get_bool_option("z3")) @@ -189,76 +158,6 @@ std::unique_ptr cbmc_solverst::get_string_refinement() util_make_unique(info), std::move(prop)); } -std::unique_ptr cbmc_solverst::get_smt1( - smt1_dect::solvert solver) -{ - no_beautification(); - no_incremental_check(); - - const std::string &filename=options.get_option("outfile"); - - if(filename=="") - { - if(solver==smt1_dect::solvert::GENERIC) - { - error() << "please use --outfile" << eom; - throw 0; - } - - auto smt1_dec= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver); - - return util_make_unique(std::move(smt1_dec)); - } - else if(filename=="-") - { - auto smt1_conv= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver, - std::cout); - - smt1_conv->set_message_handler(get_message_handler()); - - return util_make_unique(std::move(smt1_conv)); - } - else - { - #ifdef _MSC_VER - auto out=util_make_unique(widen(filename)); - #else - auto out=util_make_unique(filename); - #endif - - if(!out) - { - error() << "failed to open " << filename << eom; - throw 0; - } - - auto smt1_conv= - util_make_unique( - ns, - "cbmc", - "Generated by CBMC " CBMC_VERSION, - "QF_AUFBV", - solver, - *out); - - smt1_conv->set_message_handler(get_message_handler()); - - return util_make_unique(std::move(smt1_conv), std::move(out)); - } -} - std::unique_ptr cbmc_solverst::get_smt2( smt2_dect::solvert solver) { diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 2245ff59b70..66df55eca87 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -112,8 +111,6 @@ class cbmc_solverst:public messaget return get_bv_refinement(); else if(options.get_bool_option("refine-strings")) return get_string_refinement(); - if(options.get_bool_option("smt1")) - return get_smt1(get_smt1_solver_type()); if(options.get_bool_option("smt2")) return get_smt2(get_smt2_solver_type()); return get_default(); @@ -137,10 +134,8 @@ class cbmc_solverst:public messaget std::unique_ptr get_dimacs(); std::unique_ptr get_bv_refinement(); std::unique_ptr get_string_refinement(); - std::unique_ptr get_smt1(smt1_dect::solvert solver); std::unique_ptr get_smt2(smt2_dect::solvert solver); - smt1_dect::solvert get_smt1_solver_type() const; smt2_dect::solvert get_smt2_solver_type() const; // consistency checks during solver creation diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 2256e0ee977..b33a2a149e1 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -189,8 +189,6 @@ SRC = $(BOOLEFORCE_SRC) \ sat/pbs_dimacs_cnf.cpp \ sat/resolution_proof.cpp \ sat/satcheck.cpp \ - smt1/smt1_conv.cpp \ - smt1/smt1_dec.cpp \ smt2/smt2_conv.cpp \ smt2/smt2_dec.cpp \ smt2/smt2_parser.cpp \ diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp deleted file mode 100644 index 39c2e3f2e20..00000000000 --- a/src/solvers/smt1/smt1_conv.cpp +++ /dev/null @@ -1,3215 +0,0 @@ -/*******************************************************************\ - -Module: SMT Version 1 Backend - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// SMT Version 1 Backend - -#include "smt1_conv.h" - -#include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include -#include -#include -#include - -void smt1_convt::print_assignment(std::ostream &out) const -{ - // Boolean stuff - - for(std::size_t v=0; vsecond.value; - } - else if(expr.id()==ID_member) - { - const member_exprt &member_expr=to_member_expr(expr); - exprt tmp=get(member_expr.struct_op()); - if(tmp.is_nil()) - return nil_exprt(); - return member_exprt(tmp, member_expr.get_component_name(), expr.type()); - } - else if(expr.id()==ID_index) - { - const index_exprt &index_expr=to_index_expr(expr); - exprt tmp_array=get(index_expr.array()); - exprt tmp_index=get(index_expr.index()); - if(tmp_array.is_nil() || tmp_index.is_nil()) - return nil_exprt(); - return index_exprt(tmp_array, tmp_index, expr.type()); - } - else if(expr.id()==ID_constant) - return expr; - else if(expr.id()==ID_typecast) - { - exprt tmp=get(to_typecast_expr(expr).op()); - if(tmp.is_nil()) - return nil_exprt(); - return typecast_exprt(tmp, expr.type()); - } - - return nil_exprt(); -} - -exprt smt1_convt::ce_value( - const typet &type, - const std::string &index, - const std::string &value, - bool in_struct) const -{ - if(type.id()==ID_symbol) - return ce_value(ns.follow(type), index, value, in_struct); - - if(type.id()==ID_signedbv || - type.id()==ID_unsignedbv || - type.id()==ID_bv || - type.id()==ID_fixedbv) - { - assert(value.size()==boolbv_width(type)); - constant_exprt c(type); - c.set_value(value); - return c; - } - else if(type.id()==ID_bool) - { - if(value=="1") - return true_exprt(); - else if(value=="0") - return false_exprt(); - } - else if(type.id()==ID_pointer) - { - assert(value.size()==boolbv_width(type)); - - constant_exprt result(type); - result.set_value(value); - - // add the elaborated expression as operand - - pointer_logict::pointert p; - p.object=integer2unsigned( - binary2integer( - value.substr(0, config.bv_encoding.object_bits), false)); - - p.offset= - binary2integer( - value.substr(config.bv_encoding.object_bits, std::string::npos), true); - - result.copy_to_operands( - pointer_logic.pointer_expr(p, to_pointer_type(type))); - - return result; - } - else if(type.id()==ID_struct) - { - return binary2struct(to_struct_type(type), value); - } - else if(type.id()==ID_union) - { - return binary2union(to_union_type(type), value); - } - else if(type.id()==ID_array) - { - const array_typet &array_type = to_array_type(type); - const typet &subtype=ns.follow(type.subtype()); - - // arrays in structs are flat, no index - if(in_struct) - { - // we can only do fixed-size arrays - mp_integer size; - - if(!to_integer(array_type.size(), size)) - { - std::size_t size_int=integer2unsigned(size); - std::size_t sub_width=value.size()/size_int; - array_exprt array_list(array_type); - array_list.reserve_operands(size_int); - - std::size_t offset=value.size(); - - for(std::size_t i=0; i!=size_int; i++) - { - offset-=sub_width; - std::string sub_value=value.substr(offset, sub_width); - array_list.copy_to_operands(ce_value(subtype, "", sub_value, true)); - } - - return array_list; - } - } - else if(subtype.id()==ID_array) - { - // a 2 dimensional array - second dimension is flattened - return ce_value(subtype, "", value, true); - } - else - { - exprt value_expr=ce_value(subtype, "", value, in_struct); - - if(index=="") - return nil_exprt(); - - // use index, recusive call - exprt index_expr= - ce_value(signedbv_typet(index.size()), "", index, false); - - if(index_expr.is_nil()) - return nil_exprt(); - - array_list_exprt array_list(array_type); - array_list.copy_to_operands(index_expr, value_expr); - - return array_list; - } - } - - return nil_exprt(); -} - -typet smt1_convt::array_index_type() const -{ - return signedbv_typet(array_index_bits); -} - -void smt1_convt::array_index(const exprt &expr) -{ - if(expr.type().id()==ID_integer) - return convert_expr(expr, true); - - typet t=array_index_type(); - if(t==expr.type()) - return convert_expr(expr, true); - const typecast_exprt tmp(expr, t); - convert_expr(tmp, true); -} - -void smt1_convt::convert_address_of_rec( - const exprt &expr, - const pointer_typet &result_type) -{ - if(expr.id()==ID_symbol || - expr.id()==ID_constant || - expr.id()==ID_string_constant || - expr.id()==ID_label) - { - out - << "(concat" - << " bv" << pointer_logic.add_object(expr) << "[" - << config.bv_encoding.object_bits << "]" - << " bv0[" - << boolbv_width(result_type)-config.bv_encoding.object_bits << "]" - << ")"; - } - else if(expr.id()==ID_index) - { - if(expr.operands().size()!=2) - throw "index takes two operands"; - - const exprt &array=to_index_expr(expr).array(); - const exprt &index=to_index_expr(expr).index(); - - if(index.is_zero()) - { - if(array.type().id()==ID_pointer) - convert_expr(array, true); - else if(array.type().id()==ID_array) - convert_address_of_rec(array, result_type); - else - assert(false); - } - else - { - // this is really pointer arithmetic - exprt new_index_expr=expr; - new_index_expr.op1()=from_integer(0, index.type()); - - address_of_exprt address_of_expr( - new_index_expr, - pointer_type(array.type().subtype())); - - plus_exprt plus_expr( - address_of_expr, - index, - address_of_expr.type()); - - convert_expr(plus_expr, true); - } - } - else if(expr.id()==ID_member) - { - if(expr.operands().size()!=1) - throw "member takes one operand"; - - const member_exprt &member_expr=to_member_expr(expr); - - const exprt &struct_op=member_expr.struct_op(); - const typet &struct_op_type=ns.follow(struct_op.type()); - - if(struct_op_type.id()==ID_struct) - { - const struct_typet &struct_type= - to_struct_type(struct_op_type); - - const irep_idt &component_name= - member_expr.get_component_name(); - - mp_integer offset=member_offset(struct_type, component_name, ns); - assert(offset>=0); - - const unsignedbv_typet index_type(boolbv_width(result_type)); - - out << "(bvadd "; - convert_address_of_rec(struct_op, result_type); - out << " "; - convert_expr(from_integer(offset, index_type), true); - out << ")"; - } - else if(struct_op_type.id()==ID_union) - { - // these all have offset 0 - convert_address_of_rec(struct_op, result_type); - } - else - throw "unexpected type of member operand"; - } - else if(expr.id()==ID_if) - { - assert(expr.operands().size()==3); - - out << "(ite "; - convert_expr(expr.op0(), false); - out << " "; - convert_address_of_rec(expr.op1(), result_type); - out << " "; - convert_address_of_rec(expr.op2(), result_type); - out << ")"; - } - else - throw "don't know how to take address of: "+expr.id_string(); -} - -void smt1_convt::convert_byte_extract( - const byte_extract_exprt &expr, - bool bool_as_bv) -{ - // we just run the flattener - exprt flattened_expr=flatten_byte_extract(expr, ns); - convert_expr(flattened_expr, bool_as_bv); -} - -void smt1_convt::convert_byte_update( - const exprt &expr, - bool bool_as_bv) -{ - assert(expr.operands().size()==3); - - // The situation: expr.op0 needs to be split in 3 parts - // |<--- L --->|<--- M --->|<--- R --->| - // where M is the expr.op1'th byte - // We need to output L expr.op2 R - - mp_integer i; - if(to_integer(expr.op1(), i)) - throw "byte_update takes constant as second operand"; - - std::size_t w=boolbv_width(expr.op0().type()); - - if(w==0) - throw "failed to get width of byte_update operand"; - - mp_integer upper, lower; // of the byte - mp_integer max=w-1; - std::size_t op_w = boolbv_width(expr.op2().type()); - - if(expr.id()==ID_byte_update_little_endian) - { - lower = i*8; - upper = lower+op_w-1; - } - else - { - upper = max-(i*8); - lower = max-(i*8+op_w-1); - } - - if(upper==max) - { - if(lower==0) // there was only one byte - convert_expr(expr.op2(), true); - else // uppermost byte selected, only R needed - { - out << "(concat "; - convert_expr(expr.op2(), true); - out << " (extract[" << lower-1 << ":0] "; - convert_expr(expr.op0(), true); - out << ")"; // extract - out << ")"; // concat - } - } - else - { - if(lower==0) // lowermost byte selected, only L needed - { - out << "(concat "; - out << "(extract[" << max << ":" << (upper+1) << "] "; - convert_expr(expr.op0(), true); - out << ") "; - convert_expr(expr.op2(), true); - out << ")"; - } - else // byte in the middle selected, L & R needed - { - out << "(concat (concat"; - out << " (extract[" << max << ":" << (upper+1) << "] "; - convert_expr(expr.op0(), true); - out << ")"; // extract - out << " "; - convert_expr(expr.op2(), true); - out << ")"; // concat - out<< " (extract[" << (lower-1) << ":0] "; - convert_expr(expr.op0(), true); - out << ")"; // extract - out << ")"; // concat - } - } -} - -literalt smt1_convt::convert(const exprt &expr) -{ - assert(expr.type().id()==ID_bool); - - // Trivial cases that don't need a new handle. - - if(expr.is_true()) - return const_literal(true); - else if(expr.is_false()) - return const_literal(false); - else if(expr.id()==ID_literal) - return to_literal_expr(expr).get_literal(); - - // Ok, need new handle - - out << "\n"; - - find_symbols(expr); - - literalt l(no_boolean_variables, false); - no_boolean_variables++; - - out << ":extrapreds(("; - convert_literal(l); - out << "))" << "\n"; - - out << ":assumption ; convert " << "\n" - << " (iff "; - convert_literal(l); - out << " "; - convert_expr(expr, false); - out << ")" << "\n"; - - return l; -} - -std::string smt1_convt::convert_identifier(const irep_idt &identifier) -{ - std::string s=id2string(identifier), dest; - dest.reserve(s.size()); - - // a sequence of letters, digits, dots (.), single quotes (’), and - // underscores (_), starting with a letter - - // MathSAT does not really seem to like the single quotes ' - // so we avoid these. - - for(std::string::const_iterator - it=s.begin(); - it!=s.end(); - ++it) - { - char ch=*it; - - if(isalnum(ch) || ch=='_') - dest+=ch; - else if(ch==':') - { - std::string::const_iterator next_it(it); - ++next_it; - if(next_it!=s.end() && *next_it==':') - { - dest.append(".S"); - it=next_it; - } - else - dest+=".C"; - } - else if(ch=='#') - dest+=".H"; - else if(ch=='$') - dest+=".D"; - else if(ch=='!') - dest+=".E"; - else if(ch=='.') - dest+=".."; - else if(ch=='%') - dest+=".P"; - else - { - dest+='.'; - dest.append(std::to_string(ch)); - dest+='.'; - } - } - - return dest; -} - -void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv) -{ - if(expr.id()==ID_symbol) - { - const typet &type=expr.type(); - - irep_idt id=to_symbol_expr(expr).get_identifier(); - DATA_INVARIANT(!id.empty(), "symbol must have identifier"); - - // boolean symbols may have to be converted - from_bool_begin(type, bool_as_bv); - - out << convert_identifier(id); - - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_nondet_symbol) - { - const typet &type=expr.type(); - - irep_idt id=to_nondet_symbol_expr(expr).get_identifier(); - DATA_INVARIANT(!id.empty(), "symbol must have identifier"); - - // boolean symbols may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "nondet_" << convert_identifier(id); - - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_literal) - { - convert_literal(to_literal_expr(expr).get_literal()); - } - else if(expr.id()==ID_typecast) - { - convert_typecast(to_typecast_expr(expr), bool_as_bv); - } - else if(expr.id()==ID_struct) - { - convert_struct(expr); - } - else if(expr.id()==ID_union) - { - convert_union(expr); - } - else if(expr.id()==ID_constant) - { - convert_constant(to_constant_expr(expr), bool_as_bv); - } - else if(expr.id()==ID_concatenation) - convert_nary(expr, "concat", true); - else if(expr.id()==ID_bitand) - convert_nary(expr, "bvand", true); - else if(expr.id()==ID_bitor) - convert_nary(expr, "bvor", true); - else if(expr.id()==ID_bitxor) - convert_nary(expr, "bvxor", true); - else if(expr.id()==ID_bitnand) - convert_nary(expr, "bvnand", true); - else if(expr.id()==ID_bitnor) - convert_nary(expr, "bvnor", true); - else if(expr.id()==ID_bitnot) - { - assert(expr.operands().size()==1); - out << "(bvnot "; - convert_expr(expr.op0(), true); - out << ")"; - } - else if(expr.id()==ID_unary_minus) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - - if(type.id()==ID_rational) - { - out << "(- "; - convert_expr(expr.op0(), true); - out << ")"; - } - else if(type.id()==ID_integer) - { - out << "(~ "; - convert_expr(expr.op0(), true); - out << ")"; - } - else - { - out << "(bvneg "; - convert_expr(expr.op0(), true); - out << ")"; - } - } - else if(expr.id()==ID_if) - { - assert(expr.operands().size()==3); - - // The SMTLIB standard requires a different operator in a boolean context - if(expr.op1().type().id()==ID_bool && !bool_as_bv) - out << "(if_then_else "; - else - out << "(ite "; - - convert_expr(expr.op0(), false); - out << " "; - convert_expr(expr.op1(), bool_as_bv); - out << " "; - convert_expr(expr.op2(), bool_as_bv); - out << ")"; - } - else if(expr.id()==ID_and || - expr.id()==ID_or || - expr.id()==ID_xor) - { - const typet &type=expr.type(); - const exprt::operandst &operands=expr.operands(); - - assert(type.id()==ID_bool); - assert(operands.size()>=2); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "(" << expr.id(); - forall_expr(it, operands) - { - out << " "; - convert_expr(*it, false); - } - out << ")"; - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_implies) - { - const typet &type=expr.type(); - - assert(type.id()==ID_bool); - assert(expr.operands().size()==2); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "(implies "; - convert_expr(expr.op0(), false); - out << " "; - convert_expr(expr.op1(), false); - out << ")"; - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_not) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "(not "; - convert_expr(expr.op0(), false); - out << ")"; - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_equal || - expr.id()==ID_notequal) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==2); - assert(base_type_eq(expr.op0().type(), expr.op1().type(), ns)); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - if(expr.op0().type().id()==ID_bool) - { - if(expr.id()==ID_notequal) - out << "(xor "; - else - out << "(iff "; - - convert_expr(expr.op0(), false); - out << " "; - convert_expr(expr.op1(), false); - out << ")"; - } - else - { - if(expr.id()==ID_notequal) - { - out << "(not (= "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << "))"; - } - else - { - out << "(= "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << ")"; - } - } - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_le || - expr.id()==ID_lt || - expr.id()==ID_ge || - expr.id()==ID_gt) - { - convert_relation(expr, bool_as_bv); - } - else if(expr.id()==ID_plus) - { - convert_plus(to_plus_expr(expr)); - } - else if(expr.id()==ID_floatbv_plus) - { - convert_floatbv_plus(expr); - } - else if(expr.id()==ID_minus) - { - convert_minus(to_minus_expr(expr)); - } - else if(expr.id()==ID_floatbv_minus) - { - convert_floatbv_minus(expr); - } - else if(expr.id()==ID_div) - { - convert_div(to_div_expr(expr)); - } - else if(expr.id()==ID_floatbv_div) - { - convert_floatbv_div(expr); - } - else if(expr.id()==ID_mod) - { - convert_mod(to_mod_expr(expr)); - } - else if(expr.id()==ID_mult) - { - convert_mult(to_mult_expr(expr)); - } - else if(expr.id()==ID_floatbv_mult) - { - convert_floatbv_mult(expr); - } - else if(expr.id()==ID_address_of) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - assert(type.id()==ID_pointer); - convert_address_of_rec(expr.op0(), to_pointer_type(type)); - } - else if(expr.id()=="implicit_address_of" || - expr.id()=="reference_to") - { - // old stuff - assert(false); - } - else if(expr.id()==ID_array_of) - { - assert(expr.type().id()==ID_array); - assert(expr.operands().size()==1); - - // const array_typet &array_type=to_array_type(expr.type()); - - // not really there in SMT, so we replace it - // this is an over-approximation - array_of_mapt::const_iterator it=array_of_map.find(expr); - assert(it!=array_of_map.end()); - - out << it->second; - } - else if(expr.id()==ID_index) - { - convert_index(to_index_expr(expr), bool_as_bv); - } - else if(expr.id()==ID_ashr || - expr.id()==ID_lshr || - expr.id()==ID_shl) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==2); - - if(type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_bv || - type.id()==ID_struct || - type.id()==ID_union) - { - if(expr.id()==ID_ashr) - out << "(bvashr "; - else if(expr.id()==ID_lshr) - out << "(bvlshr "; - else if(expr.id()==ID_shl) - out << "(bvshl "; - else - assert(false); - - convert_expr(expr.op0(), true); - out << " "; - - // SMT1 requires the shift distance to have the same width as - // the value that is shifted -- odd! - - std::size_t width_op0=boolbv_width(expr.op0().type()); - std::size_t width_op1=boolbv_width(expr.op1().type()); - - if(width_op0==width_op1) - convert_expr(expr.op1(), true); - else if(width_op0>width_op1) - { - out << "(zero_extend[" << width_op0-width_op1 << "] "; - convert_expr(expr.op1(), true); - out << ")"; // zero_extend - } - else // width_op00) - out << "(zero_extend[" << ext << "] "; - - out << "(extract[" - << (op_width-1) - << ":" - << op_width-1-config.bv_encoding.object_bits << "] "; - convert_expr(expr.op0(), true); - out << ")"; - - if(ext>0) - out << ")"; - } - else if(expr.id()=="is_dynamic_object") - { - convert_is_dynamic_object(expr, bool_as_bv); - } - else if(expr.id()==ID_invalid_pointer) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - assert(expr.op0().type().id()==ID_pointer); - std::size_t op_width=boolbv_width(expr.op0().type()); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "(= (extract[" - << (op_width-1) - << ":" << op_width-config.bv_encoding.object_bits << "] "; - convert_expr(expr.op0(), true); - out << ") bv" << pointer_logic.get_invalid_object() - << "[" << config.bv_encoding.object_bits << "])"; - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()=="pointer_object_has_type") - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - - // this may have to be converted - from_bool_begin(type, bool_as_bv); - - out << "false"; // TODO - - // this may have to be converted - from_bool_end(type, bool_as_bv); - } - else if(expr.id()==ID_string_constant) - { - exprt tmp; - string2array_mapt::const_iterator fit=string2array_map.find(expr); - assert(fit!=string2array_map.end()); - - convert_expr(fit->second, true); - } - else if(expr.id()==ID_extractbit) - { - assert(expr.operands().size()==2); - - if(expr.op0().type().id()==ID_unsignedbv || - expr.op0().type().id()==ID_signedbv) - { - const typet &type=expr.type(); - - // this may have to be converted - from_bv_begin(type, bool_as_bv); - - if(expr.op1().is_constant()) - { - mp_integer i; - if(to_integer(expr.op1(), i)) - throw "extractbit: to_integer failed"; - - out << "(extract[" << i << ":" << i << "] "; - convert_expr(expr.op0(), true); - out << ")"; - } - else - { - out << "(extract[0:0] "; - // the arguments of the shift need to have the same width - out << "(bvlshr "; - convert_expr(expr.op0(), true); - typecast_exprt tmp(expr.op0().type()); - tmp.op0()=expr.op1(); - convert_expr(tmp, true); - out << "))"; // bvlshr, extract - } - - // this may have to be converted - from_bv_end(type, bool_as_bv); - } - else - throw "unsupported type for "+expr.id_string()+ - ": "+expr.op0().type().id_string(); - } - else if(expr.id()==ID_replication) - { - assert(expr.operands().size()==2); - - mp_integer times; - if(to_integer(expr.op0(), times)) - throw "replication takes constant as first parameter"; - - out << "(repeat[" << times << "] "; - convert_expr(expr.op1(), true); // this ensures we have a vector - out << ")"; - } - else if(expr.id()==ID_byte_extract_little_endian || - expr.id()==ID_byte_extract_big_endian) - { - convert_byte_extract(to_byte_extract_expr(expr), bool_as_bv); - } - else if(expr.id()==ID_byte_update_little_endian || - expr.id()==ID_byte_update_big_endian) - { - convert_byte_update(expr, bool_as_bv); - } - else if(expr.id()==ID_width) - { - std::size_t result_width=boolbv_width(expr.type()); - - if(result_width==0) - throw "conversion failed"; - - if(expr.operands().size()!=1) - throw "width expects 1 operand"; - - std::size_t op_width=boolbv_width(expr.op0().type()); - - if(op_width==0) - throw "conversion failed"; - - out << "bv" << op_width/8 << "[" << result_width << "]"; - } - else if(expr.id()==ID_abs) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - const exprt &op0=expr.op0(); - - std::size_t result_width=boolbv_width(type); - - if(result_width==0) - throw "conversion failed"; - - if(type.id()==ID_signedbv || - type.id()==ID_fixedbv) - { - out << "(ite (bvslt "; - convert_expr(op0, true); - out << " bv0[" << result_width << "]) "; - out << "(bvneg "; - convert_expr(op0, true); - out << ") "; - convert_expr(op0, true); - out << ")"; - } - else if(type.id()==ID_floatbv) - { - out << "(bvand "; - convert_expr(op0, true); - out << " bv" - << (power(2, result_width-1)-1) - << "[" << result_width << "])"; - } - else - throw "abs with unsupported operand type"; - } - else if(expr.id()==ID_isnan) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==1); - - const typet &op_type=expr.op0().type(); - - if(op_type.id()==ID_fixedbv) - { - from_bool_begin(type, bool_as_bv); - out << "false"; - from_bool_end(type, bool_as_bv); - } - else - throw "isnan with unsupported operand type"; - } - else if(expr.id()==ID_isfinite) - { - const typet &type=expr.type(); - - if(expr.operands().size()!=1) - throw "isfinite expects one operand"; - - const typet &op_type=expr.op0().type(); - - if(op_type.id()==ID_fixedbv) - { - from_bool_begin(type, bool_as_bv); - out << "true"; - from_bool_end(type, bool_as_bv); - } - else - throw "isfinite with unsupported operand type"; - } - else if(expr.id()==ID_isinf) - { - const typet &type=expr.type(); - - if(expr.operands().size()!=1) - throw "isinf expects one operand"; - - const typet &op_type=expr.op0().type(); - - if(op_type.id()==ID_fixedbv) - { - from_bool_begin(type, bool_as_bv); - out << "false"; - from_bool_end(type, bool_as_bv); - } - else - throw "isinf with unsupported operand type"; - } - else if(expr.id()==ID_isnormal) - { - const typet &type=expr.type(); - - if(expr.operands().size()!=1) - throw "isnormal expects one operand"; - - const typet &op_type=expr.op0().type(); - - if(op_type.id()==ID_fixedbv) - { - from_bool_begin(type, bool_as_bv); - out << "true"; - from_bool_end(type, bool_as_bv); - } - else - throw "isnormal with unsupported operand type"; - } - else if(expr.id()==ID_overflow_plus || - expr.id()==ID_overflow_minus) - { - const typet &type=expr.type(); - - assert(expr.operands().size()==2); - bool subtract=expr.id()==ID_overflow_minus; - - const typet &op_type=expr.op0().type(); - - std::size_t width=boolbv_width(op_type); - - if(op_type.id()==ID_signedbv) - { - // an overflow occurs if the top two bits of the extended sum differ - - from_bool_begin(type, bool_as_bv); - out << "(let (?sum ("; - out << (subtract?"bvsub":"bvadd"); - out << " (sign_extend[1] "; - convert_expr(expr.op0(), true); - out << ")"; - out << " (sign_extend[1] "; - convert_expr(expr.op1(), true); - out << "))) "; // sign_extend, bvadd/sub let2 - out << "(not (= " - "(extract[" << width << ":" << width << "] ?sum) " - "(extract[" << (width-1) << ":" << (width-1) << "] ?sum)"; - out << ")))"; // =, not, let - from_bool_end(type, bool_as_bv); - } - else if(op_type.id()==ID_unsignedbv) - { - // overflow is simply carry-out - from_bv_begin(type, bool_as_bv); - out << "(extract[" << width << ":" << width << "] "; - out << "(" << (subtract?"bvsub":"bvadd"); - out << " (zero_extend[1] "; - convert_expr(expr.op0(), true); - out << ")"; - out << " (zero_extend[1] "; - convert_expr(expr.op1(), true); - out << ")))"; // zero_extend, bvsub/bvadd, extract - from_bv_end(type, bool_as_bv); - } - else - throw "overflow check on unknown type: "+op_type.id_string(); - } - else if(expr.id()==ID_overflow_mult) - { - assert(expr.operands().size()==2); - - // No better idea than to multiply with double the bits and then compare - // with max value. - - const typet &op_type=expr.op0().type(); - std::size_t width=boolbv_width(op_type); - - if(op_type.id()==ID_signedbv) - { - out << "(let (?prod (bvmul (sign_extend[" << width << "] "; - convert_expr(expr.op0(), true); - out << ") (sign_extend[" << width << "] "; - convert_expr(expr.op1(), true); - out << "))) "; // sign_extend, bvmul, ?prod - out << "(or (bvsge ?prod (bv" << power(2, width-1) - << "[" << width*2 << "]))"; - out << " (bvslt ?prod (bvneg (bv" << power(2, width-1) - << "[" << width*2 << "])))"; - out << "))"; // or, let - } - else if(op_type.id()==ID_unsignedbv) - { - out << "(bvuge (bvmul (zero_extend[" << width << "] "; - convert_expr(expr.op0(), true); - out << ") (zero_extend[" << width << "] "; - convert_expr(expr.op1(), true); - out << ")) bv" << power(2, width) << "[" << width*2 << "])"; - } - else - throw "overflow-* check on unknown type: "+op_type.id_string(); - } - else if(expr.id()==ID_forall || expr.id()==ID_exists) - { - from_bv_begin(expr.type(), bool_as_bv); - - assert(expr.operands().size()==2); - out << "(" << expr.id() << " ("; - exprt bound=expr.op0(); - convert_expr(bound, false); - out << " "; - - if(bound.type().id()==ID_bool) - out << "Bool"; - else - convert_type(bound.type()); - - out << ") "; - convert_expr(expr.op1(), false); - out << ")"; - - from_bv_end(expr.type(), bool_as_bv); - } - else if(expr.id()==ID_extractbits) - { - assert(expr.operands().size()==3); - - const typet &op_type=ns.follow(expr.op0().type()); - - if(op_type.id()==ID_unsignedbv || - op_type.id()==ID_signedbv || - op_type.id()==ID_bv || - op_type.id()==ID_fixedbv || - op_type.id()==ID_struct || - op_type.id()==ID_union || - op_type.id()==ID_vector) - { - if(expr.op1().is_constant() && - expr.op2().is_constant()) - { - mp_integer op1_i, op2_i; - - if(to_integer(expr.op1(), op1_i)) - throw "extractbits: to_integer failed"; - - if(to_integer(expr.op2(), op2_i)) - throw "extractbits: to_integer failed"; - - out << "(extract[" << op1_i << ":" << op2_i << "] "; - convert_expr(expr.op0(), true); - out << ")"; - } - else - { - #if 0 - out << "(extract["; - convert_expr(expr.op1(), bool_as_bv); - out << ":"; - convert_expr(expr.op2(), bool_as_bv); - out << "] "; - convert_expr(expr.op0(), bool_as_bv); - out << ")"; - #endif - throw "smt1 todo: extractbits with variable bits"; - } - } - else - throw "unsupported type for "+expr.id_string()+ - ": "+op_type.id_string(); - } - else if(expr.id()==ID_array) - { - const exprt::operandst &operands=expr.operands(); - - // array constructor - array_expr_mapt::const_iterator it=array_expr_map.find(expr); - assert(it!=array_expr_map.end()); - - assert(!operands.empty()); - - forall_expr(it, operands) - out << "(store "; - - out << it->second; - - std::size_t i=0; - forall_expr(it, operands) - { - exprt index=from_integer(i, unsignedbv_typet(array_index_bits)); - out << " "; - convert_expr(index, true); - out << " "; - convert_expr(*it, true); - out << ")"; - i++; - } - } - else if(expr.id()==ID_vector) - { - // Vector constructor. - // We flatten the vector by concatenating its elements. - convert_nary(expr, "concat", bool_as_bv); - } - else - throw "smt1_convt::convert_expr: `"+ - expr.id_string()+"' is unsupported"; -} - -void smt1_convt::convert_typecast( - const typecast_exprt &expr, - bool bool_as_bv) -{ - assert(expr.operands().size()==1); - const exprt &src=expr.op0(); - - typet dest_type=ns.follow(expr.type()); - if(dest_type.id()==ID_c_enum_tag) - dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type)); - - typet src_type=ns.follow(src.type()); - if(src_type.id()==ID_c_enum_tag) - src_type=ns.follow_tag(to_c_enum_tag_type(src_type)); - - if(dest_type.id()==ID_bool) - { - // boolean typecasts may have to be converted - from_bool_begin(dest_type, bool_as_bv); - - // this is comparison with zero - if(src_type.id()==ID_signedbv || - src_type.id()==ID_unsignedbv || - src_type.id()==ID_fixedbv || - src_type.id()==ID_c_bit_field || - src_type.id()==ID_pointer) - { - out << "(not (= "; - convert_expr(src, true); - out << " "; - convert_expr( - from_integer(0, src_type), - true); - out << "))"; - } - else - { - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast1 "+src_type.id_string()+" -> bool"; - } - - // boolean typecasts may have to be converted - from_bool_end(dest_type, bool_as_bv); - } - else if(dest_type.id()==ID_c_bool) - { - // this is comparison with zero - if(src_type.id()==ID_signedbv || - src_type.id()==ID_unsignedbv || - src_type.id()==ID_fixedbv || - src_type.id()==ID_c_bit_field || - src_type.id()==ID_pointer) - { - std::size_t to_width=boolbv_width(dest_type); - - out << "(ite "; - out << "(not (= "; - convert_expr(src, true); - out << " "; - convert_expr( - from_integer(0, src_type), - true); - out << ")) "; // not, = - out << " bv1[" << to_width << "]"; - out << " bv0[" << to_width << "]"; - out << ")"; // ite - } - else - { - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast1 "+src_type.id_string()+" -> bool"; - } - } - else if(dest_type.id()==ID_signedbv || - dest_type.id()==ID_unsignedbv || - dest_type.id()==ID_c_enum) - { - std::size_t to_width=boolbv_width(dest_type); - - if(src_type.id()==ID_signedbv || // from signedbv - src_type.id()==ID_unsignedbv || // from unsigedbv - src_type.id()==ID_c_bool || - src_type.id()==ID_c_enum) - { - std::size_t from_width=boolbv_width(src_type); - - if(from_width==to_width) - convert_expr(src, true); // ignore - else if(from_widthfrom_integer_bits) - { - out << "(sign_extend[" << (to_width-from_integer_bits) << "] "; - out << "(extract[" << (from_width-1) << ":" - << from_fraction_bits << "] "; - convert_expr(src, true); - out << "))"; - } - else - { - out << "(extract[" << (from_fraction_bits+to_width-1) - << ":" << from_fraction_bits << "] "; - convert_expr(src, true); - out << ")"; - } - } - else if(src_type.id()==ID_bool) // from boolean - { - out << "(ite "; - convert_expr(src, false); - - if(dest_type.id()==ID_fixedbv) - { - fixedbv_spect spec(to_fixedbv_type(expr.type())); - out << " (concat bv1[" << spec.integer_bits << "] " << - "bv0[" << spec.get_fraction_bits() << "]) " << - "bv0[" << spec.width << "]"; - } - else - { - out << " bv1[" << to_width << "]"; - out << " bv0[" << to_width << "]"; - } - - out << ")"; - } - else if(src_type.id()==ID_pointer) // from pointer to int - { - std::size_t from_width=boolbv_width(src_type); - - if(from_width "+dest_type.id_string(); - } - } - else if(dest_type.id()==ID_fixedbv) // to fixedbv - { - const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type); - std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits(); - std::size_t to_integer_bits=fixedbv_type.get_integer_bits(); - - if(src_type.id()==ID_unsignedbv || - src_type.id()==ID_signedbv || - src_type.id()==ID_c_enum) - { - // integer to fixedbv - std::size_t from_width=to_bitvector_type(src_type).get_width(); - - // we just concatenate a zero-valued fractional part - out << "(concat"; - - if(from_width==to_integer_bits) - convert_expr(src, true); - else if(from_width>to_integer_bits) - { - // too many integer bits, chop some off - out << " (extract[" << (to_integer_bits-1) << ":0] "; - convert_expr(src, true); - out << ")"; - } - else - { - // too few integer bits - assert(from_widthfrom_integer_bits); - out << "(sign_extend[" - << (to_integer_bits-from_integer_bits) - << "] (extract[" - << (from_width-1) << ":" - << from_fraction_bits - << "] "; - convert_expr(src, true); - out << "))"; - } - - out << " "; - - if(to_fraction_bits<=from_fraction_bits) - { - out << "(extract[" - << (from_fraction_bits-1) << ":" - << (from_fraction_bits-to_fraction_bits) - << "] "; - convert_expr(src, true); - out << ")"; - } - else - { - assert(to_fraction_bits>from_fraction_bits); - out << "(concat (extract[" - << (from_fraction_bits-1) << ":0] "; - convert_expr(src, true); - out << ")" - << " bv0[" << to_fraction_bits-from_fraction_bits - << "])"; - } - - out << ")"; // concat - } - else - throw "unexpected typecast to fixedbv"; - } - else if(dest_type.id()==ID_pointer) - { - std::size_t to_width=boolbv_width(dest_type); - - if(src_type.id()==ID_pointer) - { - // this just passes through - convert_expr(src, true); - } - else if(src_type.id()==ID_unsignedbv || - src_type.id()==ID_signedbv) - { - std::size_t from_width=boolbv_width(src_type); - - if(from_width==to_width) - convert_expr(src, true); // pass through - else if(from_widthto_width - { - out << "(extract[" - << to_width - << ":0] "; - convert_expr(src, true); - out << ")"; // extract - } - } - else - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast3 "+src_type.id_string()+" -> pointer"; - } - else if(dest_type.id()==ID_range) - { - // NOLINTNEXTLINE(readability/throw) - throw "TODO range typecast"; - } - else if(dest_type.id()==ID_c_bit_field) - { - std::size_t from_width=boolbv_width(src_type); - std::size_t to_width=boolbv_width(dest_type); - - if(from_width==to_width) - convert_expr(src, bool_as_bv); // ignore - else - { - typet t=c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns); - typecast_exprt tmp(typecast_exprt(src, t), dest_type); - convert_typecast(tmp, bool_as_bv); - } - } - else - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast4 ? -> "+dest_type.id_string(); -} - -void smt1_convt::convert_struct(const exprt &expr) -{ - const struct_typet &struct_type=to_struct_type(expr.type()); - - const struct_typet::componentst &components= - struct_type.components(); - - assert(components.size()==expr.operands().size()); - - assert(!components.empty()); - - if(components.size()==1) - { - const exprt &op=expr.op0(); - - if(op.type().id()==ID_array) - flatten_array(op); - else - convert_expr(op, true); - } - else - { - std::size_t nr_ops=0; - - for(std::size_t i=0; imember_width); - out << "(concat "; - out << "bv0[" << (total_width-member_width) << "] "; - convert_expr(op, true); - out << ")"; - } -} - -void smt1_convt::convert_constant( - const constant_exprt &expr, - bool bool_as_bv) -{ - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv || - expr.type().id()==ID_bv || - expr.type().id()==ID_c_enum || - expr.type().id()==ID_c_enum_tag || - expr.type().id()==ID_c_bool || - expr.type().id()==ID_c_bit_field) - { - mp_integer value; - - if(to_integer(expr, value)) - throw "failed to convert bitvector constant"; - - std::size_t width=boolbv_width(expr.type()); - - if(value<0) - value=power(2, width)+value; - - out << "bv" << value - << "[" << width << "]"; - } - else if(expr.type().id()==ID_fixedbv) - { - fixedbv_spect spec(to_fixedbv_type(expr.type())); - - std::string v_str=expr.get_string(ID_value); - mp_integer v=binary2integer(v_str, false); - - out << "bv" << v << "[" << spec.width << "]"; - } - else if(expr.type().id()==ID_floatbv) - { - ieee_float_spect spec(to_floatbv_type(expr.type())); - - std::string v_str=expr.get_string(ID_value); - mp_integer v=binary2integer(v_str, false); - - out << "bv" << v << "[" << spec.width() << "]"; - } - else if(expr.type().id()==ID_pointer) - { - const irep_idt &value=expr.get(ID_value); - - if(value==ID_NULL) - { - assert(boolbv_width(expr.type())!=0); - out << "(concat" - << " bv" << pointer_logic.get_null_object() - << "[" << config.bv_encoding.object_bits << "]" - << " bv0[" << boolbv_width(expr.type())-config.bv_encoding.object_bits - << "]" - << ")"; // concat - } - else - throw "unknown pointer constant: "+id2string(value); - } - else if(expr.type().id()==ID_bool) - { - if(expr.is_true()) - out << (bool_as_bv?"bit1":"true"); - else if(expr.is_false()) - out << (bool_as_bv?"bit0":"false"); - else - throw "unknown boolean constant"; - } - else if(expr.type().id()==ID_array) - { - // this should be the 'array' expression - assert(false); - } - else if(expr.type().id()==ID_rational) - { - std::string value=expr.get_string(ID_value); - size_t pos=value.find("/"); - - if(pos==std::string::npos) - out << value << ".0"; - else - { - out << "(/ " << value.substr(0, pos) << ".0 " - << value.substr(pos+1) << ".0)"; - } - } - else if(expr.type().id()==ID_integer || - expr.type().id()==ID_natural) - { - std::string value=expr.get_string(ID_value); - - if(value[0]=='-') - out << "(~ " << value.substr(1) << ")"; - else - out << value; - } - else - throw "unknown constant: "+expr.type().id_string(); -} - -void smt1_convt::convert_mod(const mod_exprt &expr) -{ - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - if(expr.type().id()==ID_unsignedbv) - out << "(bvurem "; - else - out << "(bvsrem "; - - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << ")"; - } - else - throw "unsupported type for mod: "+expr.type().id_string(); -} - -void smt1_convt::convert_is_dynamic_object( - const exprt &expr, - bool bool_as_bv) -{ - std::vector dynamic_objects; - pointer_logic.get_dynamic_objects(dynamic_objects); - - assert(expr.operands().size()==1); - assert(expr.op0().type().id()==ID_pointer); - std::size_t op_width=boolbv_width(expr.op0().type()); - - // this may have to be converted - from_bool_begin(expr.type(), bool_as_bv); - - if(dynamic_objects.empty()) - out << "false"; - else - { - // let is only allowed in formulas - - out << "(let (?obj (extract[" - << (op_width-1) - << ":" << op_width-config.bv_encoding.object_bits << "] "; - convert_expr(expr.op0(), true); - out << ")) "; - - if(dynamic_objects.size()==1) - { - out << "(= bv" << dynamic_objects.front() - << "[" << config.bv_encoding.object_bits << "] ?obj)"; - } - else - { - out << "(or"; - - for(const auto &obj : dynamic_objects) - out << " (= bv" << obj - << "[" << config.bv_encoding.object_bits << "] ?obj)"; - - out << ")"; // or - } - - out << ")"; // let - } - - // this may have to be converted - from_bool_end(expr.type(), bool_as_bv); -} - -void smt1_convt::convert_relation(const exprt &expr, bool bool_as_bv) -{ - assert(expr.operands().size()==2); - - // this may have to be converted - from_bool_begin(expr.type(), bool_as_bv); - - const typet &op_type=expr.op0().type(); - - out << "("; - - if(op_type.id()==ID_unsignedbv || - op_type.id()==ID_pointer) - { - if(expr.id()==ID_le) - out << "bvule"; - else if(expr.id()==ID_lt) - out << "bvult"; - else if(expr.id()==ID_ge) - out << "bvuge"; - else if(expr.id()==ID_gt) - out << "bvugt"; - - out << " "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - } - else if(op_type.id()==ID_signedbv || - op_type.id()==ID_fixedbv) - { - if(expr.id()==ID_le) - out << "bvsle"; - else if(expr.id()==ID_lt) - out << "bvslt"; - else if(expr.id()==ID_ge) - out << "bvsge"; - else if(expr.id()==ID_gt) - out << "bvsgt"; - - out << " "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - } - else if(op_type.id()==ID_rational || - op_type.id()==ID_integer) - { - out << expr.id(); - - out << " "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - } - else - throw "unsupported type for "+expr.id_string()+ - ": "+op_type.id_string(); - - out << ")"; - - // this may have to be converted - from_bool_end(expr.type(), bool_as_bv); -} - -void smt1_convt::convert_plus(const plus_exprt &expr) -{ - assert(expr.operands().size()>=2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv || - expr.type().id()==ID_fixedbv) - { - convert_nary(expr, "bvadd", true); - } - else if(expr.type().id()==ID_pointer) - { - if(expr.operands().size()<2) - throw "pointer arithmetic with less than two operands"; - - 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) - throw "unexpected mixture in pointer arithmetic"; - - mp_integer element_size= - pointer_offset_size(expr.type().subtype(), ns); - assert(element_size>0); - - // adjust width if needed - if(boolbv_width(i.type())!=boolbv_width(expr.type())) - i.make_typecast(signedbv_typet(boolbv_width(expr.type()))); - - out << "(bvadd "; - convert_expr(p, true); - out << " "; - - if(element_size>=2) - { - out << "(bvmul "; - convert_expr(i, true); - out << " bv" << element_size - << "[" << boolbv_width(expr.type()) << "])"; - } - else - convert_expr(i, true); - - out << ")"; - } - else - { - // more than two operands - exprt p; - typet integer_type=signedbv_typet(boolbv_width(expr.type())); - exprt integer_sum(ID_plus, integer_type); - - forall_operands(it, expr) - { - if(it->type().id()==ID_pointer) - p=*it; - else - integer_sum.copy_to_operands(*it); - } - - Forall_operands(it, integer_sum) - if(it->type()!=integer_type) - it->make_typecast(integer_type); - - plus_exprt pointer_arithmetic(p, integer_sum, expr.type()); - convert_plus(pointer_arithmetic); // recursive call - } - } - else if(expr.type().id()==ID_rational || - expr.type().id()==ID_integer) - { - convert_nary(expr, "+", true); - } - else - throw "unsupported type for +: "+expr.type().id_string(); -} - -void smt1_convt::convert_floatbv_plus(const exprt &expr) -{ - assert(expr.operands().size()==3); - assert(expr.type().id()==ID_floatbv); - - throw "todo: floatbv_plus"; -} - -void smt1_convt::convert_minus(const minus_exprt &expr) -{ - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv || - expr.type().id()==ID_fixedbv) - { - out << "(bvsub "; - - if(expr.op0().type().id()==ID_pointer) - out << "(extract[" << boolbv_width(expr.op0().type())-1 << ":0] "; - convert_expr(expr.op0(), true); - if(expr.op0().type().id()==ID_pointer) - out << ")"; - - out << " "; - - if(expr.op1().type().id()==ID_pointer) - out << "(extract[" << boolbv_width(expr.op1().type())-1 << ":0] "; - convert_expr(expr.op1(), true); - if(expr.op1().type().id()==ID_pointer) - out << ")"; - - out << ")"; - } - else if(expr.type().id()==ID_pointer) - { - convert_expr(binary_exprt( - expr.op0(), - "+", - unary_minus_exprt(expr.op1(), expr.op1().type()), - expr.type()), - true); - } - else - throw "unsupported type for -: "+expr.type().id_string(); -} - -void smt1_convt::convert_floatbv_minus(const exprt &expr) -{ - assert(expr.operands().size()==3); - assert(expr.type().id()==ID_floatbv); - - throw "todo: floatbv_minus"; -} - -void smt1_convt::convert_div(const div_exprt &expr) -{ - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - if(expr.type().id()==ID_unsignedbv) - out << "(bvudiv "; - else - out << "(bvsdiv "; - - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << ")"; - } - else if(expr.type().id()==ID_fixedbv) - { - fixedbv_spect spec(to_fixedbv_type(expr.type())); - std::size_t fraction_bits=spec.get_fraction_bits(); - - out << "(extract[" << spec.width-1 << ":0] "; - out << "(bvsdiv "; - - out << "(concat "; - convert_expr(expr.op0(), true); - out << " bv0[" << fraction_bits << "]) "; - - out << "(sign_extend[" << fraction_bits << "] "; - convert_expr(expr.op1(), true); - out << ")"; - - out << "))"; - } - else - throw "unsupported type for /: "+expr.type().id_string(); -} - -void smt1_convt::convert_floatbv_div(const exprt &expr) -{ - assert(expr.operands().size()==3); - assert(expr.type().id()==ID_floatbv); - - throw "todo: floatbv_div"; -} - -void smt1_convt::convert_mult(const mult_exprt &expr) -{ - assert(expr.operands().size()>=2); - - // re-write to binary if needed - if(expr.operands().size()>2) - { - // strip last operand - exprt tmp=expr; - tmp.operands().pop_back(); - - // recursive call - return convert_mult(mult_exprt(tmp, expr.operands().back())); - } - - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - // Note that bvmul is really unsigned, - // but this is irrelevant as we chop-off any extra result - // bits. - out << "(bvmul "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << ")"; - } - else if(expr.type().id()==ID_fixedbv) - { - fixedbv_spect spec(to_fixedbv_type(expr.type())); - std::size_t fraction_bits=spec.get_fraction_bits(); - - // strip away faction_bits off the result - out << "(extract[" << spec.width+fraction_bits-1 << ":" - << fraction_bits << "] "; - - out << "(bvmul "; - - out << "(sign_extend[" << fraction_bits << "] "; - convert_expr(expr.op0(), true); - out << ") "; - - out << "(sign_extend[" << fraction_bits << "] "; - convert_expr(expr.op1(), true); - out << ") "; - - out << ")"; // bvmul, fraction_bits+width wide - out << ")"; // extract, width bits wide - } - else if(expr.type().id()==ID_rational) - { - out << "(* "; - convert_expr(expr.op0(), true); - out << " "; - convert_expr(expr.op1(), true); - out << ")"; - } - else - throw "unsupported type for *: "+expr.type().id_string(); -} - -void smt1_convt::convert_floatbv_mult(const exprt &expr) -{ - assert(expr.operands().size()==3); - assert(expr.type().id()==ID_floatbv); - - throw "todo: floatbv_mult"; -} - -void smt1_convt::convert_with(const exprt &expr) -{ - // get rid of "with" that has more than three operands - - assert(expr.operands().size()>=3); - - if(expr.operands().size()>3) - { - std::size_t s=expr.operands().size(); - - // strip of the trailing two operands - exprt tmp=expr; - tmp.operands().resize(s-2); - - with_exprt new_with_expr; - assert(new_with_expr.operands().size()==3); - new_with_expr.type()=expr.type(); - new_with_expr.old()=tmp; - new_with_expr.where()=expr.operands()[s-2]; - new_with_expr.new_value()=expr.operands()[s-1]; - - // recursive call - return convert_with(new_with_expr); - } - - const typet &expr_type=ns.follow(expr.type()); - - if(expr_type.id()==ID_array) - { - const exprt &array=expr.op0(); - - if(array.id()==ID_member) - { - // arrays in structs and unions are flattened! - - const typet &array_type=to_array_type(expr.type()); - const typet &elem_type=array_type.subtype(); - - const member_exprt &member_expr=to_member_expr(array); - const exprt &struct_op=member_expr.struct_op(); - const irep_idt &name=member_expr.get_component_name(); - - const typet &struct_op_type=ns.follow(struct_op.type()); - - std::size_t total_width=boolbv_width(struct_op_type); - - if(total_width==0) - throw "failed to get struct width"; - - std::size_t offset; - - if(struct_op_type.id()==ID_struct) - offset=boolbv_width.get_member( - to_struct_type(struct_op_type), name).offset; - else if(struct_op_type.id()==ID_union) - offset=0; - else - throw "failed to get offset"; - - std::size_t width=boolbv_width(expr.type()); - - if(width==0) - throw "failed to get struct member width"; - - std::size_t elem_width=boolbv_width(elem_type); - - if(elem_width==0) - throw "failed to get struct width"; - - std::size_t array_bits=(offset+width) - offset; - - assert(expr.operands().size()==3); - const exprt &index=expr.operands()[1]; - const exprt &value=expr.operands()[2]; - typecast_exprt index_tc(index, array_index_type()); - - out << "(bvor "; - out << "(bvand "; - - // this gets us the array - out << "(extract[" << offset+width-1 << ":" << offset << "] "; - convert_expr(struct_op, true); - out << ")"; - - // the mask - out << " (bvnot (bvshl"; - - out << " (concat"; - out << " (repeat[" << array_bits-elem_width << "] bv0[1])"; - out << " (repeat[" << elem_width << "] bv1[1])"; - out << ")"; // concat - - // shift it to the index - if(width>=array_index_bits) - out << " (zero_extend[" << width-array_index_bits << "]"; - else - out << " (extract[" << width-1 << ":0]"; - out << " (bvmul "; - convert_expr(index_tc, true); - out << " bv" << elem_width << "[" << array_index_bits << "]"; - out << "))))"; // bvmul, zero_extend, bvshl, bvneg - - out << ")"; // bvand - - // the new value - out << " (bvshl (zero_extend[" << array_bits-elem_width << "] "; - convert_expr(value, true); - - // shift it to the index - out << ")"; - if(width>=array_index_bits) - out << " (zero_extend[" << width-array_index_bits << "]"; - else - out << " (extract[" << width-1 << ":0]"; - out << " (bvmul "; - convert_expr(index_tc, true); - out << " bv" << elem_width << "[" << array_index_bits << "]"; - out << ")))"; // bvmul, bvshl, ze - - out << ")"; // bvor - } - else if(array.id()==ID_index) - { - // arrays in structs are flattened! - - const typet &array_type=to_array_type(expr.type()); - const typet &elem_type=array_type.subtype(); - - const index_exprt &index_expr=to_index_expr(array); - - std::size_t width=boolbv_width(expr.type()); - - if(width==0) - throw "failed to get width of 2nd dimension array"; - - std::size_t elem_width=boolbv_width(elem_type); - - if(elem_width==0) - throw "failed to get array element width"; - - assert(expr.operands().size()==3); - const exprt &index_2nd=expr.operands()[1]; - const exprt &value=expr.operands()[2]; - typecast_exprt index_tc(index_2nd, array_index_type()); - - out << "(bvor "; - out << "(bvand "; - - // this gets us the array - convert_expr(index_expr, true); - - // the mask - out << " (bvnot (bvshl"; - - out << " (concat"; - out << " (repeat[" << width-elem_width << "] bv0[1])"; - out << " (repeat[" << elem_width << "] bv1[1])"; - out << ")"; // concat - - // shift it to the index - if(width>=array_index_bits) - out << " (zero_extend[" << width-array_index_bits << "]"; - else - out << " (extract[" << width-1 << ":0]"; - out << " (bvmul "; - convert_expr(index_tc, true); - out << " bv" << elem_width << "[" << array_index_bits << "]"; - out << "))))"; // bvmul, zero_extend, bvshl, bvneg - - out << ")"; // bvand - - // the new value - out << " (bvshl (zero_extend[" << width-elem_width << "] "; - convert_expr(value, true); - // shift it to the index - out << ")"; - if(width>=array_index_bits) - out << " (zero_extend[" << width-array_index_bits << "]"; - else - out << " (extract[" << width-1 << ":0]"; - out << " (bvmul "; - convert_expr(index_tc, true); - out << " bv" << elem_width << "[" << array_index_bits << "]"; - out << ")))"; // bvmul, bvshl, ze - - out << ")"; // bvor - } - else - { - out << "(store "; - - convert_expr(expr.op0(), true); - - out << " "; - array_index(expr.op1()); - out << " "; - - // Booleans are put as bv[1] into an array - convert_expr(expr.op2(), true); - - out << ")"; - } - } - else if(expr_type.id()==ID_struct) - { - const struct_typet &struct_type=to_struct_type(expr_type); - - const exprt &index=expr.op1(); - const exprt &value=expr.op2(); - - std::size_t total_width=boolbv_width(expr.type()); - - if(total_width==0) - throw "failed to get struct width for with"; - - std::size_t width=boolbv_width(value.type()); - - if(width==0) - throw "failed to get member width for with"; - - std::size_t offset=boolbv_width.get_member( - struct_type, index.get(ID_component_name)).offset; - - if(total_width==width) - convert_expr(value, true); - else - { - if(offset+width!=total_width) - { - out << "(concat"; - out << " (extract[" << (total_width-1) << ":" << (offset+width) << "] "; - convert_expr(expr.op0(), true); - out << ")"; - } - - if(offset!=0) - out << " (concat"; - - out << " "; - convert_expr(value, true); - - if(offset!=0) - { - out << " (extract[" << (offset-1) << ":0] "; - convert_expr(expr.op0(), true); - out << ")"; - out << ")"; // concat - } - - if(offset+width!=total_width) - out << ")"; // concat - } - } - else if(expr_type.id()==ID_union) - { - const union_typet &union_type=to_union_type(expr_type); - - const exprt &value=expr.op2(); - - std::size_t total_width=boolbv_width(union_type); - - if(total_width==0) - throw "failed to get union width for with"; - - std::size_t member_width=boolbv_width(value.type()); - - if(member_width==0) - throw "failed to get union member width for with"; - - if(total_width==member_width) - convert_expr(value, true); - else - { - assert(total_width>member_width); - out << "(concat "; - out << "(extract[" - << (total_width-1) - << ":" << member_width << "] "; - convert_expr(expr.op0(), true); - out << ") "; // extract - convert_expr(value, true); - out << ")"; // concat - } - } - else if(expr_type.id()==ID_bv || - expr_type.id()==ID_unsignedbv || - expr_type.id()==ID_signedbv) - { - // Update bits in a bit-vector. We will use masking and shifts. - - std::size_t total_width=boolbv_width(expr_type); - - if(total_width==0) - throw "failed to get total width"; - - assert(expr.operands().size()==3); - const exprt &index=expr.operands()[1]; - const exprt &value=expr.operands()[2]; - - std::size_t value_width=boolbv_width(value.type()); - - if(value_width==0) - throw "failed to get value width"; - - typecast_exprt index_tc(index, expr_type); - - out << "(bvor "; - out << "(band "; - - // the mask to get rid of the old bits - out << " (bvnot (bvshl"; - - out << " (concat"; - out << " (repeat[" << total_width-value_width << "] bv0[1])"; - out << " (repeat[" << value_width << "] bv1[1])"; - out << ")"; // concat - - // shift it to the index - convert_expr(index_tc, true); - out << "))"; // bvshl, bvot - - out << ")"; // bvand - - // the new value - out << " (bvshl "; - convert_expr(value, true); - - // shift it to the index - convert_expr(index_tc, true); - out << ")"; // bvshl - - out << ")"; // bvor - } - else - { - throw "with expects struct, union, or array type, " - "but got "+expr.type().id_string(); - } -} - -void smt1_convt::convert_update(const exprt &expr) -{ - assert(expr.operands().size()==3); - - // todo - throw "smt1_convt::convert_update to be implemented"; -} - -void smt1_convt::convert_index(const index_exprt &expr, bool bool_as_bv) -{ - assert(expr.operands().size()==2); - - if(expr.array().id()==ID_member || - expr.array().id()==ID_index) - { - // arrays inside structs and 2-dimensional arrays - // these were flattened - - const typet &array_type=to_array_type(expr.array().type()); - const typet &elem_type=array_type.subtype(); - - std::size_t width=boolbv_width(expr.array().type()); - if(width==0) - throw "failed to get array width"; - - std::size_t elem_width=boolbv_width(elem_type); - - if(elem_width==0) - throw "failed to get struct width"; - - out << "(extract[" << elem_width-1 << ":0] "; - out << "(bvlshr "; - convert_expr(expr.array(), true); - if(width>=array_index_bits) - out << " (zero_extend[" << width-array_index_bits << "]"; - else - out << " (extract[" << width-1 << ":0]"; - out << " (bvmul "; - typecast_exprt index_tc(expr.index(), array_index_type()); - convert_expr(index_tc, true); - out << " bv" << elem_width << "[" << array_index_bits << "]"; - out << "))))"; - } - else - { - // Booleans out of arrays may have to be converted - from_bv_begin(expr.type(), bool_as_bv); - - out << "(select "; - convert_expr(expr.array(), true); - out << " "; - array_index(expr.index()); - out << ")"; - - // Booleans out of arrays may have to be converted - from_bv_end(expr.type(), bool_as_bv); - } -} - -void smt1_convt::convert_member(const member_exprt &expr, bool bool_as_bv) -{ - assert(expr.operands().size()==1); - - const member_exprt &member_expr=to_member_expr(expr); - const exprt &struct_op=member_expr.struct_op(); - const typet &struct_op_type=ns.follow(struct_op.type()); - const irep_idt &name=member_expr.get_component_name(); - - // Booleans pulled out of structs may have to be converted - from_bv_begin(expr.type(), bool_as_bv); - - if(struct_op_type.id()==ID_struct) - { - std::size_t offset=boolbv_width.get_member( - to_struct_type(struct_op_type), name).offset; - - std::size_t width=boolbv_width(expr.type()); - - if(width==0) - throw "failed to get struct member width"; - - out << "(extract[" - << (offset+width-1) - << ":" - << offset - << "] "; - convert_expr(struct_op, true); - out << ")"; - } - else if(struct_op_type.id()==ID_union) - { - std::size_t width=boolbv_width(expr.type()); - - if(width==0) - throw "failed to get union member width"; - - out << "(extract[" - << (width-1) - << ":0] "; - convert_expr(struct_op, true); - out << ")"; - } - else - assert(false); - - // Booleans pulled out of structs may have to be converted - from_bv_end(expr.type(), bool_as_bv); -} - -void smt1_convt::convert_overflow(const exprt &expr) -{ -} - -void smt1_convt::set_to(const exprt &expr, bool value) -{ - if(expr.id()==ID_and && value) - { - forall_operands(it, expr) - set_to(*it, true); - return; - } - - if(expr.id()==ID_not) - { - assert(expr.operands().size()==1); - return set_to(expr.op0(), !value); - } - - out << "\n"; - - find_symbols(expr); - - #if 0 - out << "; CONV: " - << format(expr) << '\n'; - #endif - - out << ":assumption ; set_to " << (value ? "true" : "false") << '\n' << " "; - - assert(expr.type().id()==ID_bool); - - if(!value) - { - out << "(not "; - convert_expr(expr, false); - out << ")"; - } - else - convert_expr(expr, false); - - out << "\n"; -} - -void smt1_convt::find_symbols(const exprt &expr) -{ - const typet &type=expr.type(); - find_symbols(type); - - if(expr.id()==ID_forall || expr.id()==ID_exists) - { - assert(expr.operands().size()==2); - assert(expr.op0().id()==ID_symbol); - - const irep_idt &ident=expr.op0().get(ID_identifier); - quantified_symbols.insert(ident); - find_symbols(expr.op1()); - quantified_symbols.erase(ident); - } - else - forall_operands(it, expr) - find_symbols(*it); - - if(expr.id()==ID_symbol || - expr.id()==ID_nondet_symbol) - { - // we don't track function-typed symbols - if(type.id()==ID_code) - return; - - irep_idt identifier; - - if(expr.id()==ID_symbol) - identifier=to_symbol_expr(expr).get_identifier(); - else - identifier="nondet_"+ - id2string(to_nondet_symbol_expr(expr).get_identifier()); - - if(quantified_symbols.find(identifier)!=quantified_symbols.end()) - return; // Symbol is quantified, i.e., it doesn't require declaration. - - identifiert &id=identifier_map[identifier]; - - if(id.type.is_nil()) - { - id.type=type; - - if(id.type.id()==ID_bool) - { - out << ":extrapreds((" - << convert_identifier(identifier) - << "))" << "\n"; - } - else - { - out << ":extrafuns((" - << convert_identifier(identifier) - << " "; - convert_type(type); - out << "))" << "\n"; - } - } - } - else if(expr.id()==ID_array_of) - { - if(array_of_map.find(expr)==array_of_map.end()) - { - irep_idt id="array_of'"+std::to_string(array_of_map.size()); - out << "; the following is a poor substitute for lambda i. x" << "\n"; - out << ":extrafuns((" - << id - << " "; - convert_type(type); - out << "))" << "\n"; - - // we can initialize array_ofs if they have - // a constant size and a constant element - if(type.find(ID_size)!=get_nil_irep() && - expr.op0().id()==ID_constant) - { - const array_typet &array_type=to_array_type(type); - mp_integer size; - - if(!to_integer(array_type.size(), size)) - { - // since we can't use quantifiers, let's enumerate... - for(mp_integer i=0; i rec_stack; - find_symbols_rec(type, rec_stack); -} - -void smt1_convt::find_symbols_rec( - const typet &type, - std::set &recstack) -{ - if(type.id()==ID_array) - { - const array_typet &array_type=to_array_type(type); - find_symbols(array_type.size()); - find_symbols_rec(array_type.subtype(), recstack); - } - else if(type.id()==ID_struct || - type.id()==ID_union) - { - const struct_union_typet::componentst &components= - to_struct_union_type(type).components(); - - for(const auto &comp : components) - find_symbols_rec(comp.type(), recstack); - } - else if(type.id()==ID_code) - { - const code_typet::parameterst ¶meters= - to_code_type(type).parameters(); - - for(const auto ¶m : parameters) - find_symbols_rec(param.type(), recstack); - - find_symbols_rec(to_code_type(type).return_type(), recstack); - } - else if(type.id()==ID_pointer) - { - find_symbols_rec(type.subtype(), recstack); - } - else if(type.id()==ID_incomplete_array) - { - find_symbols_rec(type.subtype(), recstack); - } - else if(type.id()==ID_symbol) - { - const symbol_typet &st=to_symbol_type(type); - const irep_idt &id=st.get_identifier(); - - if(recstack.find(id)==recstack.end()) - { - recstack.insert(id); - find_symbols_rec(ns.follow(type), recstack); - } - } -} - -exprt smt1_convt::binary2struct( - const struct_typet &type, - const std::string &binary) const -{ - const struct_typet::componentst &components=type.components(); - - std::size_t total_width=boolbv_width(type); - - if(total_width==0) - throw "failed to get struct width"; - - struct_exprt e(type); - e.reserve_operands(components.size()); - - std::size_t index=binary.size(); - for(const auto &comp : components) - { - const typet &sub_type=ns.follow(comp.type()); - - std::size_t sub_size=boolbv_width(sub_type); - - if(sub_size==0) - throw "failed to get component width"; - - index-=sub_size; - std::string cval=binary.substr(index, sub_size); - - e.copy_to_operands(ce_value(sub_type, "", cval, true)); - } - - return e; -} - -exprt smt1_convt::binary2union( - const union_typet &type, - const std::string &binary) const -{ - std::size_t total_width=boolbv_width(type); - - if(total_width==0) - throw "failed to get union width"; - - const union_typet::componentst &components=type.components(); - - // Taking the first component should work. - // Maybe a better idea is to take a largest component - std::size_t component_nr=0; - - // construct a union expr - union_exprt e(type); - e.set_component_number(component_nr); - e.set_component_name(components[component_nr].get_name()); - - const typet &sub_type=ns.follow(components[component_nr].type()); - std::size_t comp_width=boolbv_width(sub_type); - assert(comp_width<=total_width); - - std::string cval=binary.substr(total_width-comp_width, comp_width); - e.op()=ce_value(sub_type, "", cval, true); - - return e; -} - -void smt1_convt::flatten_array(const exprt &op) -{ - const array_typet array_type=to_array_type(op.type()); - const typet &elem_type=array_type.subtype(); - const exprt &size=array_type.size(); - - if(size.id()!=ID_constant) - throw "non-constant size array cannot be flattened"; - - mp_integer sizei; - if(to_integer(size, sizei)) - throw "array with non-constant size"; - - std::size_t elem_width=boolbv_width(elem_type); - - if(elem_width==0) - throw "failed to get width of array subtype"; - - #if 0 - out << " (let (?fbv "; - convert_expr(op, true); - out << ")"; - #endif - - for(mp_integer i=1; i0); - - if(num_ops==1) - convert_expr(expr.op0(), bool_as_bv); - else - { - exprt::operandst::const_iterator it= - expr.operands().begin(); - - for(std::size_t i=0; i -#include - -#include - -#include -#include -#include - -class byte_extract_exprt; -class typecast_exprt; -class constant_exprt; -class index_exprt; -class member_exprt; - -class smt1_convt:public prop_convt -{ -public: - enum class solvert - { - GENERIC, - BOOLECTOR, - CVC3, - CVC4, - MATHSAT, - OPENSMT, - YICES, - Z3 - }; - - smt1_convt( - const namespacet &_ns, - const std::string &_benchmark, - const std::string &_source, - const std::string &_logic, - solvert _solver, - std::ostream &_out): - prop_convt(_ns), - benchmark(_benchmark), - source(_source), - logic(_logic), - solver(_solver), - out(_out), - boolbv_width(_ns), - pointer_logic(_ns), - array_index_bits(32), - no_boolean_variables(0) - { - write_header(); - } - - virtual ~smt1_convt() { } - virtual resultt dec_solve(); - - // overloading interfaces - virtual literalt convert(const exprt &expr); - virtual void set_to(const exprt &expr, bool value); - virtual exprt get(const exprt &expr) const; - virtual tvt l_get(literalt) const; - virtual std::string decision_procedure_text() const { return "SMT1"; } - virtual void print_assignment(std::ostream &out) const; - -protected: - std::string benchmark, source, logic; - solvert solver; - std::ostream &out; - boolbv_widtht boolbv_width; - - void write_header(); - void write_footer(); - - // new stuff - void convert_expr(const exprt &expr, bool bool_as_bv); - void convert_type(const typet &type); - - // specific expressions go here - void convert_byte_update(const exprt &expr, bool bool_as_bv); - void convert_byte_extract( - const byte_extract_exprt &expr, - bool bool_as_bv); - void convert_typecast(const typecast_exprt &expr, bool bool_as_bv); - void convert_struct(const exprt &expr); - void convert_union(const exprt &expr); - void convert_constant(const constant_exprt &expr, bool bool_as_bv); - void convert_relation(const exprt &expr, bool bool_as_bv); - void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv); - void convert_plus(const plus_exprt &expr); - void convert_minus(const minus_exprt &expr); - void convert_div(const div_exprt &expr); - void convert_mult(const mult_exprt &expr); - void convert_floatbv_plus(const exprt &expr); - void convert_floatbv_minus(const exprt &expr); - void convert_floatbv_div(const exprt &expr); - void convert_floatbv_mult(const exprt &expr); - void convert_mod(const mod_exprt &expr); - void convert_index(const index_exprt &expr, bool bool_as_bv); - void convert_member(const member_exprt &expr, bool bool_as_bv); - void convert_overflow(const exprt &expr); - void convert_with(const exprt &expr); - void convert_update(const exprt &expr); - - std::string convert_identifier(const irep_idt &identifier); - void convert_literal(const literalt l); - - // auxiliary methods - std::set quantified_symbols; - void find_symbols(const exprt &expr); - void find_symbols(const typet &type); - void find_symbols_rec(const typet &type, std::set &recstack); - void flatten_array(const exprt &op); - - // booleans vs. bit-vector[1] - void from_bv_begin(const typet &type, bool bool_as_bv); - void from_bv_end(const typet &type, bool bool_as_bv); - void from_bool_begin(const typet &type, bool bool_as_bv); - void from_bool_end(const typet &type, bool bool_as_bv); - - // arrays - typet array_index_type() const; - void array_index(const exprt &expr); - - // pointers - pointer_logict pointer_logic; - void convert_address_of_rec( - const exprt &expr, const pointer_typet &result_type); - - // keeps track of all symbols - struct identifiert - { - typet type; - exprt value; - - identifiert() - { - type.make_nil(); - value.make_nil(); - } - }; - - void set_value( - identifiert &identifier, - const std::string &index, - const std::string &value) - { - exprt tmp=ce_value(identifier.type, index, value, false); - if(tmp.id() == ID_array_list && identifier.value.id() == ID_array_list) - { - forall_operands(it, tmp) - identifier.value.copy_to_operands(*it); - } - else - identifier.value=tmp; - } - - typedef std::unordered_map identifier_mapt; - - identifier_mapt identifier_map; - - unsigned array_index_bits; - - // for replacing 'array_of' expressions - typedef std::map array_of_mapt; - array_of_mapt array_of_map; - - // for replacing 'array' expressions - typedef std::map array_expr_mapt; - array_expr_mapt array_expr_map; - - // for replacing string constants - typedef std::map string2array_mapt; - string2array_mapt string2array_map; - - exprt ce_value( - const typet &type, - const std::string &index, - const std::string &v, - bool in_struct) const; - - exprt binary2struct( - const struct_typet &type, - const std::string &binary) const; - - exprt binary2union( - const union_typet &type, - const std::string &binary) const; - - // flattens multi-operand expressions into binary - // expressions - void convert_nary(const exprt &expr, - const irep_idt op_string, - bool bool_as_bv); - - // Boolean part - unsigned no_boolean_variables; - std::vector boolean_assignment; -}; - -#endif // CPROVER_SOLVERS_SMT1_SMT1_CONV_H diff --git a/src/solvers/smt1/smt1_dec.cpp b/src/solvers/smt1/smt1_dec.cpp deleted file mode 100644 index 807fa527339..00000000000 --- a/src/solvers/smt1/smt1_dec.cpp +++ /dev/null @@ -1,667 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "smt1_dec.h" - -#include - -#if defined(__linux__) || \ - defined(__FreeBSD_kernel__) || \ - defined(__GNU__) || \ - defined(__unix__) || \ - defined(__CYGWIN__) || \ - defined(__MACH__) -#include -#endif - -#include -#include -#include -#include -#include -#include - -std::string smt1_dect::decision_procedure_text() const -{ - return "SMT1 "+logic+" using "+ - (solver==solvert::GENERIC?"Generic": - solver==solvert::BOOLECTOR?"Boolector": - solver==solvert::CVC3?"CVC3": - solver==solvert::CVC4?"CVC3": - solver==solvert::MATHSAT?"MathSAT": - solver==solvert::OPENSMT?"OpenSMT": - solver==solvert::YICES?"Yices": - solver==solvert::Z3?"Z3": - "(unknown)"); -} - -smt1_temp_filet::smt1_temp_filet() -{ - temp_out_filename=get_temporary_file("smt1_dec_out_", ""); - - temp_out.open( - temp_out_filename.c_str(), - std::ios_base::out | std::ios_base::trunc); -} - -smt1_temp_filet::~smt1_temp_filet() -{ - temp_out.close(); - - if(temp_out_filename!="") - unlink(temp_out_filename.c_str()); - - if(temp_result_filename!="") - unlink(temp_result_filename.c_str()); -} - -decision_proceduret::resultt smt1_dect::dec_solve() -{ - // SMT1 is really not incremental - assert(!dec_solve_was_called); - dec_solve_was_called=true; - - // this closes the SMT benchmark - write_footer(); - temp_out.close(); - - temp_result_filename= - get_temporary_file("smt1_dec_result_", ""); - - std::string command; - - switch(solver) - { - case solvert::BOOLECTOR: - // -rwl0 disables rewriting, which makes things slower, - // but in return values for arrays appear - // command = "boolector -rwl0 --smt " - // Removed as not necessarily needed on newer versions - command = "boolector --smt " - + temp_out_filename - + " --model --output " - + temp_result_filename; - break; - - case solvert::CVC3: - command = "cvc3 +model -lang smtlib -output-lang smtlib " - + temp_out_filename - + " > " - + temp_result_filename; - break; - - case solvert::CVC4: - command = "cvc4 -L smt1 " - + temp_out_filename - + " > " - + temp_result_filename; - break; - - case solvert::MATHSAT: - command = "mathsat -model -input=smt" - " < "+temp_out_filename - + " > "+temp_result_filename; - break; - - case solvert::OPENSMT: - command = "opensmt " - + temp_out_filename - + " > " - + temp_result_filename; - break; - - case solvert::YICES: - // command = "yices -smt -e " // Calling convention for older versions - command = "yices-smt --full-model " // Calling for 2.2.1 - + temp_out_filename - + " > " - + temp_result_filename; - break; - - case solvert::Z3: - command = "z3 -smt " - + temp_out_filename - + " > " - + temp_result_filename; - break; - - default: - assert(false); - } - - #if defined(__linux__) || defined(__APPLE__) - command+=" 2>&1"; - #endif - - int res=system(command.c_str()); - if(res<0) - { - error() << "error running SMT1 solver" << eom; - return decision_proceduret::resultt::D_ERROR; - } - - std::ifstream in(temp_result_filename.c_str()); - - switch(solver) - { - case solvert::BOOLECTOR: - return read_result_boolector(in); - - case solvert::CVC3: - return read_result_cvc3(in); - - case solvert::CVC4: - error() << "no support for CVC4 with SMT1, use SMT2 instead" << eom; - return decision_proceduret::resultt::D_ERROR; - - case solvert::MATHSAT: - return read_result_mathsat(in); - - case solvert::OPENSMT: - return read_result_opensmt(in); - - case solvert::YICES: - return read_result_yices(in); - - case solvert::Z3: - return read_result_z3(in); - - case solvert::GENERIC: - default: - error() << "Generic solver can't solve" << eom; - return decision_proceduret::resultt::D_ERROR; - } -} - -/// read model produced by Boolector -decision_proceduret::resultt smt1_dect::read_result_boolector(std::istream &in) -{ - std::string line; - - std::getline(in, line); - - if(line=="sat") - { - boolean_assignment.clear(); - boolean_assignment.resize(no_boolean_variables, false); - - typedef std::unordered_map valuest; - valuest values; - - while(std::getline(in, line)) - { - std::size_t pos=line.find(' '); - if(pos!=std::string::npos && pos!=0) - { - std::string id=std::string(line, 0, pos); - std::string value=std::string(line, pos+1, std::string::npos); - - // Boolector offers array values as follows: - // - // ID[INDEX] VALUE - // - // There may be more than one line per ID - - if(id!="" && id[id.size()-1]==']') // array? - { - std::size_t pos2=id.find('['); - - if(pos2!=std::string::npos) - { - std::string new_id=std::string(id, 0, pos2); - std::string index=std::string(id, pos2+1, id.size()-pos2-2); - values[new_id].index_value_map[index]=value; - } - } - else - values[id].value=value; - } - } - - // Theory variables - - for(identifier_mapt::iterator - it=identifier_map.begin(); - it!=identifier_map.end(); - it++) - { - it->second.value.make_nil(); - std::string conv_id=convert_identifier(it->first); - const valuet &v=values[conv_id]; - - for(valuet::index_value_mapt::const_iterator - i_it=v.index_value_map.begin(); i_it!=v.index_value_map.end(); i_it++) - set_value(it->second, i_it->first, i_it->second); - - if(v.value!="") - set_value(it->second, "", v.value); - } - - // Booleans - - for(unsigned v=0; v valuest; - valuest values; - - while(std::getline(in, line)) - { - if(line=="sat") - res=resultt::D_SATISFIABLE; - else if(line=="unsat") - res=resultt::D_UNSATISFIABLE; - else if(line.size()>=1 && line[0]=='(') - { - // (iff B0 true) - // (= c_h39__h39___CPROVER_malloc_size_h39_35_h39_1 bv0[64]) - // (= (select __h64_0 bv0[32]) bv5[8]) - std::size_t pos1=line.find(' '); - std::size_t pos2=line.rfind(' '); - if(pos1!=std::string::npos && - pos2!=std::string::npos && - pos1!=pos2) - { - std::string id=std::string(line, pos1+1, pos2-pos1-1); - std::string value=std::string(line, pos2+1, line.size()-pos2-2); - - if(has_prefix(id, "(select ")) - { - #if 0 - std::size_t pos3=id.rfind(' '); - std::string index=std::string(pos3+1, id.size()-pos3-1); - id=std::string(id, 8, pos3-8); - #endif - } - else - values[id].value=value; - } - } - } - - for(identifier_mapt::iterator - it=identifier_map.begin(); - it!=identifier_map.end(); - it++) - { - it->second.value.make_nil(); - std::string conv_id=convert_identifier(it->first); - std::string value=mathsat_value(values[conv_id].value); - - if(value!="") - set_value(it->second, "", value); - } - - // Booleans - for(unsigned v=0; v valuest; - valuest values; - - while(std::getline(in, line)) - { - if(line=="sat") - res = resultt::D_SATISFIABLE; - else if(line=="unsat") - res = resultt::D_UNSATISFIABLE; - else - { - std::size_t pos=line.find(" -> "); - if(pos!=std::string::npos) - values[std::string(line, 0, pos)]= - std::string(line, pos+4, std::string::npos); - } - } - - for(identifier_mapt::iterator - it=identifier_map.begin(); - it!=identifier_map.end(); - it++) - { - it->second.value.make_nil(); - std::string conv_id=convert_identifier(it->first); - std::string value=values[conv_id]; - if(value=="") - continue; - - exprt e; - if(string_to_expr_z3(it->second.type, value, e)) - it->second.value=e; - else - set_value(it->second, "", value); - } - - // Booleans - for(unsigned v=0; vsecond!=id) fit++; - - if(fit==array_of_map.end()) - return false; - - e = fit->first; - - return true; - } - else if(type.id()==ID_rational) - { - constant_exprt result; - result.type()=rational_typet(); - - if(value.substr(0, 4)=="val!") - result.set_value(value.substr(4)); - else - result.set_value(value); - - e = result; - return true; - } - - return false; -} - -decision_proceduret::resultt smt1_dect::read_result_cvc3(std::istream &in) -{ - std::string line; - decision_proceduret::resultt res = resultt::D_ERROR; - - boolean_assignment.clear(); - boolean_assignment.resize(no_boolean_variables, false); - - typedef std::unordered_map valuest; - valuest values; - - while(std::getline(in, line)) - { - if(line=="sat") - res = resultt::D_SATISFIABLE; - else if(line=="unsat") - res = resultt::D_UNSATISFIABLE; - else if(line.find("Current scope level")!=std::string::npos || - line.find("Variable Assignment")!=std::string::npos) - { - // ignore - } - else - { - assert(line.substr(0, 13)==" :assumption"); - std::size_t pos=line.find('('); - - if(pos!=std::string::npos) - { - std::string var; - std::string val; - - if(line[pos+1]=='=') - { - std::string ops = line.substr(pos+3, line.length()-pos-4); - std::size_t blank=ops.find(' '); - var = ops.substr(0, blank); - val = ops.substr(blank+1, ops.length()-blank); - - if((var.length()>=4 && var.substr(0, 4)=="cvc3") || - (val.length()>=4 && val.substr(0, 4)=="cvc3") || - var==val) - continue; - else if((var.substr(0, 9)=="array_of'") || - (var.substr(0, 2)=="bv" && val.substr(0, 2)!="bv")) - { - std::string t=var; var=val; val=t; - } - } - else if(line.substr(pos+1, 3)=="not") - { - var = line.substr(pos+5, line.length()-pos-6); - val = "false"; - } - else - { - var = line.substr(pos+1, line.length()-pos-2); - assert(var.find(' ')==std::string::npos); - val = "true"; - } - - values[var]=val; - } - } - } - - for(identifier_mapt::iterator - it=identifier_map.begin(); - it!=identifier_map.end(); - it++) - { - it->second.value.make_nil(); - std::string conv_id=convert_identifier(it->first); - std::string value=values[conv_id]; - if(value=="") - continue; - - if(value.substr(0, 2)=="bv") - { - std::string v=value.substr(2, value.find('[')-2); - size_t p = value.find('[')+1; - std::string w=value.substr(p, value.find(']')-p); - - std::string binary= - integer2binary( - string2integer(v, 10), - integer2unsigned(string2integer(w, 10))); - - set_value(it->second, "", binary); - } - else if(value=="false") - it->second.value=false_exprt(); - else if(value=="true") - it->second.value=true_exprt(); - else if(value.substr(0, 8)=="array_of") - { - // We assume that array_of has only concrete arguments... - irep_idt id(value); - array_of_mapt::const_iterator fit=array_of_map.begin(); - while(fit!=array_of_map.end() && fit->second!=id) fit++; - - if(fit!=array_of_map.end()) - it->second.value = fit->first; - } - else - set_value(it->second, "", value); - } - - // Booleans - for(unsigned v=0; v - -#include "smt1_conv.h" - -class smt1_temp_filet -{ -public: - smt1_temp_filet(); - ~smt1_temp_filet(); - -protected: - std::ofstream temp_out; - std::string temp_out_filename, temp_result_filename; -}; - -/*! \brief Decision procedure interface for various SMT 1.x solvers -*/ -class smt1_dect:protected smt1_temp_filet, public smt1_convt -{ -public: - smt1_dect( - const namespacet &_ns, - const std::string &_benchmark, - const std::string &_source, - const std::string &_logic, - solvert _solver): - smt1_temp_filet(), - smt1_convt(_ns, _benchmark, _source, _logic, _solver, temp_out), - logic(_logic), - dec_solve_was_called(false) - { - } - - virtual resultt dec_solve(); - virtual std::string decision_procedure_text() const; - -protected: - std::string logic; - bool dec_solve_was_called; - - resultt read_result_boolector(std::istream &in); - resultt read_result_cvc3(std::istream &in); - resultt read_result_opensmt(std::istream &in); - resultt read_result_mathsat(std::istream &in); - resultt read_result_yices(std::istream &in); - resultt read_result_z3(std::istream &in); - - bool string_to_expr_z3( - const typet &type, - const std::string &value, exprt &e) const; - - std::string mathsat_value(const std::string &src); - - struct valuet - { - // map from array index to value - typedef std::map index_value_mapt; - index_value_mapt index_value_map; - std::string value; - }; -}; - -#endif // CPROVER_SOLVERS_SMT1_SMT1_DEC_H diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 03bd1dc736f..9e46d45c67a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -78,7 +78,6 @@ void smt2_convt::write_header() case solvert::CVC3: out << "; Generated for CVC 3\n"; break; case solvert::CVC4: out << "; Generated for CVC 4\n"; break; case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break; - case solvert::OPENSMT: out << "; Generated for OPENSMT\n"; break; case solvert::YICES: out << "; Generated for Yices\n"; break; case solvert::Z3: out << "; Generated for Z3\n"; break; } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 665b747b58c..41d8564050b 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -35,7 +35,6 @@ class smt2_convt:public prop_convt CVC3, CVC4, MATHSAT, - OPENSMT, YICES, Z3 }; @@ -82,9 +81,6 @@ class smt2_convt:public prop_convt case solvert::MATHSAT: break; - case solvert::OPENSMT: - break; - case solvert::YICES: break; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 63bd0afaeca..e303701d26c 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -37,7 +37,6 @@ std::string smt2_dect::decision_procedure_text() const solver==solvert::CVC3?"CVC3": solver==solvert::CVC4?"CVC4": solver==solvert::MATHSAT?"MathSAT": - solver==solvert::OPENSMT?"OpenSMT": solver==solvert::YICES?"Yices": solver==solvert::Z3?"Z3": "(unknown)"); @@ -126,14 +125,6 @@ decision_proceduret::resultt smt2_dect::dec_solve() + " > "+smt2_temp_file.temp_result_filename; break; - case solvert::OPENSMT: - command = "opensmt " - + smt2_temp_file.temp_out_filename - + " > " - + smt2_temp_file.temp_result_filename; - break; - - case solvert::YICES: // command = "yices -smt -e " // Calling convention for older versions command = "yices-smt2 " // Calling for 2.2.1