From 2a5cea24a03d28e488de63dcc582ef1f437a500a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Jan 2018 15:27:20 +0000 Subject: [PATCH] This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett --- src/ansi-c/expr2c.cpp | 8 ++--- src/ansi-c/expr2c_class.h | 3 +- src/goto-symex/goto_symex.cpp | 4 +-- src/solvers/smt1/smt1_conv.cpp | 9 ++--- src/solvers/smt2/smt2_conv.cpp | 12 +++---- src/util/std_expr.h | 64 ++++++++++++++++++++++++++++++++++ 6 files changed, 83 insertions(+), 17 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5c732b2cf37..23ab4aa8310 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1644,11 +1644,11 @@ std::string expr2ct::convert_symbol( } std::string expr2ct::convert_nondet_symbol( - const exprt &src, + const nondet_symbol_exprt &src, unsigned &precedence) { - const std::string &id=src.get_string(ID_identifier); - return "nondet_symbol("+id+")"; + const irep_idt id=src.get_identifier(); + return "nondet_symbol("+id2string(id)+")"; } std::string expr2ct::convert_predicate_symbol( @@ -3790,7 +3790,7 @@ std::string expr2ct::convert_with_precedence( return convert_symbol(src, precedence); else if(src.id()==ID_nondet_symbol) - return convert_nondet_symbol(src, precedence); + return convert_nondet_symbol(to_nondet_symbol_expr(src), precedence); else if(src.id()==ID_predicate_symbol) return convert_predicate_symbol(src, precedence); diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 43371c0ef94..a94ffdd1281 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -227,7 +227,8 @@ class expr2ct std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence); // NOLINTNEXTLINE(whitespace/line_length) std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence); - std::string convert_nondet_symbol(const exprt &src, unsigned &precedence); + // NOLINTNEXTLINE(whitespace/line_length) + std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence); std::string convert_quantified_symbol(const exprt &src, unsigned &precedence); std::string convert_nondet_bool(const exprt &src, unsigned &precedence); std::string convert_object_descriptor(const exprt &src, unsigned &precedence); diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 7e50d9d9125..bfd37cee334 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -27,8 +27,8 @@ void goto_symext::replace_nondet(exprt &expr) if(expr.id()==ID_side_effect && expr.get(ID_statement)==ID_nondet) { - exprt new_expr(ID_nondet_symbol, expr.type()); - new_expr.set(ID_identifier, "symex::nondet"+std::to_string(nondet_count++)); + irep_idt identifier="symex::nondet"+std::to_string(nondet_count++); + nondet_symbol_exprt new_expr(identifier, expr.type()); new_expr.add_source_location()=expr.source_location(); expr.swap(new_expr); } diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index d1ab4e6fbfc..87d7858ef02 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -540,7 +540,7 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv) const typet &type=expr.type(); irep_idt id=to_symbol_expr(expr).get_identifier(); - assert(id!=""); + DATA_INVARIANT(!id.empty(), "symbol must have identifier"); // boolean symbols may have to be converted from_bool_begin(type, bool_as_bv); @@ -553,8 +553,8 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv) { const typet &type=expr.type(); - irep_idt id=expr.get(ID_identifier); - assert(id!=""); + 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); @@ -2822,7 +2822,8 @@ void smt1_convt::find_symbols(const exprt &expr) if(expr.id()==ID_symbol) identifier=to_symbol_expr(expr).get_identifier(); else - identifier="nondet_"+expr.get_string(ID_identifier); + 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. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 23e06f37c48..0e4c95f3609 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -853,20 +853,19 @@ void smt2_convt::convert_expr(const exprt &expr) if(expr.id()==ID_symbol) { irep_idt id=to_symbol_expr(expr).get_identifier(); - assert(id!=irep_idt()); - + DATA_INVARIANT(!id.empty(), "symbol must have identifier"); out << '|' << convert_identifier(id) << '|'; } else if(expr.id()==ID_nondet_symbol) { - irep_idt id=expr.get(ID_identifier); - assert(id!=""); + irep_idt id=to_nondet_symbol_expr(expr).get_identifier(); + DATA_INVARIANT(!id.empty(), "symbol must have identifier"); out << '|' << convert_identifier("nondet_"+id2string(id)) << '|'; } else if(expr.id()==ID_smt2_symbol) { irep_idt id=expr.get(ID_identifier); - assert(id!=irep_idt()); + DATA_INVARIANT(!id.empty(), "smt2_symbol must have identifier"); out << id; } else if(expr.id()==ID_typecast) @@ -4071,7 +4070,8 @@ void smt2_convt::find_symbols(const exprt &expr) if(expr.id()==ID_symbol) identifier=to_symbol_expr(expr).get_identifier(); else - identifier="nondet_"+id2string(expr.get(ID_identifier)); + identifier="nondet_"+ + id2string(to_nondet_symbol_expr(expr).get_identifier()); identifiert &id=identifier_map[identifier]; diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 71ee0f80687..f148723f3b5 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -238,6 +238,70 @@ inline void validate_expr(const symbol_exprt &value) } +/*! \brief Expression to hold a nondeterministic choice +*/ +class nondet_symbol_exprt:public exprt +{ +public: + /*! \brief Constructor + * \param identifier Name of symbol + * \param type Type of symbol + */ + nondet_symbol_exprt( + const irep_idt &identifier, + const typet &type):exprt(ID_nondet_symbol, type) + { + set_identifier(identifier); + } + + void set_identifier(const irep_idt &identifier) + { + set(ID_identifier, identifier); + } + + const irep_idt &get_identifier() const + { + return get(ID_identifier); + } +}; + +/*! \brief Cast a generic exprt to a \ref nondet_symbol_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * nondet_symbol_exprt. + * + * \param expr Source expression + * \return Object of type \ref nondet_symbol_exprt + * + * \ingroup gr_std_expr +*/ +inline const nondet_symbol_exprt &to_nondet_symbol_expr(const exprt &expr) +{ + PRECONDITION(expr.id()==ID_nondet_symbol); + DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); + return static_cast(expr); +} + +/*! \copydoc to_nondet_symbol_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr) +{ + PRECONDITION(expr.id()==ID_symbol); + DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); + return static_cast(expr); +} + +template<> inline bool can_cast_expr(const exprt &base) +{ + return base.id()==ID_nondet_symbol; +} +inline void validate_expr(const nondet_symbol_exprt &value) +{ + validate_operands(value, 0, "Symbols must not have operands"); +} + + /*! \brief Generic base class for unary expressions */ class unary_exprt:public exprt