This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett

Author: Daniel Kroening

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);

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);

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);
   }

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.

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];
 

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<const nondet_symbol_exprt &>(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<nondet_symbol_exprt &>(expr);
+}
+
+template<> inline bool can_cast_expr<nondet_symbol_exprt>(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