Use zero_initializer instead of gen_zero

gen_zero/gen_one can now safely be removed.

Author: tautschnig

src/cegis/instrument/cegis_library.cpp

@@ -7,13 +7,13 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/expr_util.h>
-
 #include <goto-programs/goto_convert_functions.h>
 
 #include <ansi-c/c_types.h>
 #include <ansi-c/cprover_library.h>
 
+#include <linking/zero_initializer.h>
+
 #include <cegis/cegis-util/program_helper.h>
 #include <cegis/instrument/meta_variables.h>
 #include <cegis/instrument/instrument_var_ops.h>
@@ -78,7 +78,11 @@ goto_programt::targett init_array(const symbol_tablet &st, goto_programt &body,
   pos->source_location=default_cegis_source_location();
   const symbol_exprt array(st.lookup(name).symbol_expr());
   const array_typet &type=to_array_type(array.type());
-  pos->code=code_assignt(array, array_of_exprt(gen_zero(type.subtype()), type));
+  const namespacet ns(st);
+  pos->code=
+    code_assignt(
+      array,
+      zero_initializer(type, pos->source_location, ns));
   return pos;
 }
 

src/cpp/cpp_typecheck_expr.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_qualifiers.h>
 #include <ansi-c/c_sizeof.h>
 
+#include <linking/zero_initializer.h>
+
 #include "cpp_type2name.h"
 #include "cpp_typecheck.h"
 #include "cpp_convert_type.h"
@@ -1035,15 +1037,12 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr)
   {
     // Default value, e.g., int()
     typecheck_type(expr.type());
-    exprt new_expr=gen_zero(expr.type());
-
-    if(new_expr.is_nil())
-    {
-      error().source_location=expr.find_source_location();
-      error() << "no default value for `" << to_string(expr.type())
-              << "'" << eom;
-      throw 0;
-    }
+    exprt new_expr=
+      ::zero_initializer(
+        expr.type(),
+        expr.find_source_location(),
+        *this,
+        get_message_handler());
 
     new_expr.add_source_location()=expr.source_location();
     expr=new_expr;

src/goto-programs/builtin_functions.cpp

@@ -814,7 +814,12 @@ void goto_convertt::do_java_new_array(
   t_p->source_location=location;
 
   // zero-initialize the data
-  exprt zero_element=gen_zero(data.type().subtype());
+  exprt zero_element=
+    zero_initializer(
+      data.type().subtype(),
+      location,
+      ns,
+      get_message_handler());
   codet array_set(ID_array_set);
   array_set.copy_to_operands(data, zero_element);
   goto_programt::targett t_d=dest.add_instruction(OTHER);
@@ -1646,7 +1651,13 @@ void goto_convertt::do_function_call_symbol(
     {
       goto_programt::targett t=dest.add_instruction(ASSIGN);
       t->source_location=function.source_location();
-      t->code=code_assignt(dest_expr, gen_zero(dest_expr.type()));
+      exprt zero=
+        zero_initializer(
+          dest_expr.type(),
+          function.source_location(),
+          ns,
+          get_message_handler());
+      t->code=code_assignt(dest_expr, zero);
     }
   }
   else if(identifier=="__sync_fetch_and_add" ||

src/goto-symex/symex_builtin_functions.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_types.h>
 
+#include <linking/zero_initializer.h>
+
 #include "goto_symex.h"
 #include "goto_symex_state.h"
 
@@ -235,7 +237,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
-  exprt rhs=gen_zero(lhs.type());
+  exprt rhs=zero_initializer(lhs.type(), code.source_location(), ns);
 
   if(id!=irep_idt())
   {

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -15,8 +15,10 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
 
+#include <util/namespace.h>
 #include <util/std_expr.h>
-#include <util/expr_util.h>
+
+#include <linking/zero_initializer.h>
 
 class java_bytecode_convert_classt:public messaget
 {
@@ -215,7 +217,13 @@ void java_bytecode_convert_classt::convert(
       "."+id2string(f.name);
     new_symbol.mode=ID_java;
     new_symbol.is_type=false;
-    new_symbol.value=gen_zero(field_type);
+    const namespacet ns(symbol_table);
+    new_symbol.value=
+      zero_initializer(
+        field_type,
+        class_symbol.location,
+        ns,
+        get_message_handler());
 
     // Do we have the static field symbol already?
     const auto s_it=symbol_table.symbols.find(new_symbol.name);

src/linking/zero_initializer.cpp

@@ -74,25 +74,42 @@ exprt zero_initializert::zero_initializer_rec(
 {
   const irep_idt &type_id=type.id();
 
-  if(type_id==ID_bool)
+  if(type_id==ID_unsignedbv ||
+     type_id==ID_signedbv ||
+     type_id==ID_pointer ||
+     type_id==ID_c_enum ||
+     type_id==ID_incomplete_c_enum ||
+     type_id==ID_c_bit_field ||
+     type_id==ID_bool ||
+     type_id==ID_c_bool ||
+     type_id==ID_floatbv ||
+     type_id==ID_fixedbv)
   {
-    exprt result=false_exprt();
+    exprt result=from_integer(0, type);
     result.add_source_location()=source_location;
     return result;
   }
-  else if(type_id==ID_unsignedbv ||
-          type_id==ID_signedbv ||
-          type_id==ID_floatbv ||
-          type_id==ID_fixedbv ||
-          type_id==ID_pointer ||
-          type_id==ID_complex ||
-          type_id==ID_c_enum ||
-          type_id==ID_incomplete_c_enum ||
-          type_id==ID_c_enum_tag ||
-          type_id==ID_c_bit_field ||
-          type_id==ID_c_bool)
+  else if(type_id==ID_rational ||
+          type_id==ID_real)
   {
-    exprt result=gen_zero(type);
+    constant_exprt result(ID_0, type);
+    result.add_source_location()=source_location;
+    return result;
+  }
+  else if(type_id==ID_verilog_signedbv ||
+          type_id==ID_verilog_unsignedbv)
+  {
+    std::size_t width=to_bitvector_type(type).get_width();
+    std::string value(width, '0');
+
+    constant_exprt result(value, type);
+    result.add_source_location()=source_location;
+    return result;
+  }
+  else if(type_id==ID_complex)
+  {
+    exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
+    complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
     result.add_source_location()=source_location;
     return result;
   }
@@ -266,6 +283,27 @@ exprt zero_initializert::zero_initializer_rec(
 
     return result;
   }
+  else if(type_id==ID_c_enum_tag)
+  {
+    return
+      zero_initializer_rec(
+        ns.follow_tag(to_c_enum_tag_type(type)),
+        source_location);
+  }
+  else if(type_id==ID_struct_tag)
+  {
+    return
+      zero_initializer_rec(
+        ns.follow_tag(to_struct_tag_type(type)),
+        source_location);
+  }
+  else if(type_id==ID_union_tag)
+  {
+    return
+      zero_initializer_rec(
+        ns.follow_tag(to_union_tag_type(type)),
+        source_location);
+  }
   else if(type_id==ID_string)
   {
     return constant_exprt(irep_idt(), type);

src/memory-models/Makefile

@@ -2,6 +2,8 @@ SRC = mm_y.tab.cpp mm_lex.yy.cpp mmcc_main.cpp mm_parser.cpp \
       mmcc_parse_options.cpp mm2cpp.cpp
 
 OBJ += ../big-int/big-int$(LIBEXT) \
+      ../ansi-c/ansi-c$(LIBEXT) \
+      ../linking/linking$(LIBEXT) \
       ../util/util$(LIBEXT)
 
 INCLUDES= -I ..

src/path-symex/path_symex.cpp

@@ -11,11 +11,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/string2int.h>
 #include <util/byte_operators.h>
 #include <util/pointer_offset_size.h>
-#include <util/expr_util.h>
 #include <util/base_type.h>
 #include <util/prefix.h>
 #include <ansi-c/c_types.h>
 
+#include <linking/zero_initializer.h>
+
 #include <pointer-analysis/dereference.h>
 
 #include "path_symex_class.h"
@@ -352,7 +353,11 @@ void path_symext::symex_va_arg_next(
 
   // Get old symbol of va_arg and modify it to generate a new one.
   irep_idt id=get_old_va_symbol(state, tmp);
-  exprt rhs=gen_zero(lhs.type());
+  exprt rhs=
+    zero_initializer(
+      lhs.type(),
+      code.source_location(),
+      state.var_map.ns);
 
   if(!id.empty())
   {

src/solvers/smt1/smt1_conv.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
+#include <linking/zero_initializer.h>
+
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
 #include <solvers/flattening/flatten_byte_operators.h>
@@ -1540,7 +1542,9 @@ void smt1_convt::convert_typecast(
       out << "(not (= ";
       convert_expr(src, true);
       out << " ";
-      convert_expr(gen_zero(src_type), true);
+      convert_expr(
+        zero_initializer(src_type, expr.source_location(), ns),
+        true);
       out << "))";
     }
     else
@@ -1566,7 +1570,9 @@ void smt1_convt::convert_typecast(
       out << "(not (= ";
       convert_expr(src, true);
       out << " ";
-      convert_expr(gen_zero(src_type), true);
+      convert_expr(
+        zero_initializer(src_type, expr.source_location(), ns),
+        true);
       out << ")) "; // not, =
       out << " bv1[" << to_width << "]";
       out << " bv0[" << to_width << "]";

src/solvers/smt2/smt2_conv.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
+#include <linking/zero_initializer.h>
+
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
@@ -2062,7 +2064,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       out << "(not (= ";
       convert_expr(src);
       out << " ";
-      convert_expr(gen_zero(src_type));
+      convert_expr(
+        zero_initializer(src_type, expr.source_location(), ns));
       out << "))";
     }
     else if(src_type.id()==ID_floatbv)
@@ -2088,7 +2091,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     out << "(not (= ";
     convert_expr(src);
     out << " ";
-    convert_expr(gen_zero(src_type));
+    convert_expr(
+      zero_initializer(src_type, expr.source_location(), ns));
     out << ")) "; // not, =
     out << " (_ bv1 " << to_width << ")";
     out << " (_ bv0 " << to_width << ")";