From bc15b1b1c62b6f8e52ffc6aaa7b3f2c2f1a5fe3e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 11:57:39 +0100 Subject: [PATCH 1/5] Move zero_initializer to util This is really just expression-generating code, it isn't specific to linking in any way. Get rid of the dependency on ansi-c/expr2c by using format(). --- .../java_bytecode_convert_class.cpp | 5 +-- .../java_bytecode_convert_method.cpp | 3 +- .../java_bytecode_typecheck_expr.cpp | 3 +- .../src/java_bytecode/java_object_factory.cpp | 3 +- .../java_bytecode/java_string_literals.cpp | 3 +- jbmc/src/java_bytecode/remove_java_new.cpp | 3 +- src/ansi-c/c_typecheck_code.cpp | 1 + src/ansi-c/c_typecheck_initializer.cpp | 3 +- src/cpp/cpp_typecheck.cpp | 2 +- src/cpp/cpp_typecheck_expr.cpp | 3 +- src/cpp/cpp_typecheck_initializer.cpp | 3 +- src/goto-cc/linker_script_merge.cpp | 2 +- src/goto-programs/builtin_functions.cpp | 3 +- src/goto-symex/symex_builtin_functions.cpp | 3 +- src/goto-symex/symex_start_thread.cpp | 2 +- src/linking/CMakeLists.txt | 2 +- src/linking/Makefile | 1 - src/linking/module_dependencies.txt | 1 - src/linking/static_lifetime_init.cpp | 12 +++--- src/util/Makefile | 1 + src/{linking => util}/zero_initializer.cpp | 43 +++++++------------ src/{linking => util}/zero_initializer.h | 12 +++--- 22 files changed, 44 insertions(+), 70 deletions(-) rename src/{linking => util}/zero_initializer.cpp (89%) rename src/{linking => util}/zero_initializer.h (69%) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 69758351b3f..0c281f54274 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -21,13 +21,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_language.h" #include "java_utils.h" -#include #include +#include #include #include - -#include #include +#include class java_bytecode_convert_classt:public messaget { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 6669e0e05a2..35f153261c2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -31,8 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include +#include #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 6fa16827fe9..9b39368216c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -13,8 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include - -#include +#include #include "java_pointer_casts.h" #include "java_types.h" diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index b8ed2371242..61968f243e2 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -11,12 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include -#include - #include "generic_parameter_specialization_map_keys.h" #include "java_root_class.h" diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index ca6832b4f2c..3292f9548f9 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -11,11 +11,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_types.h" #include "java_utils.h" -#include - #include #include #include +#include #include #include diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 1d88c7ddbcd..948bc2e3fc8 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -14,14 +14,13 @@ Author: Peter Schrammel #include #include -#include - #include #include #include #include #include #include +#include class remove_java_newt : public messaget { diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index c025aa1fb6b..77d867356ba 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" #include +#include #include "ansi_c_declaration.h" diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 6fea7bc9c77..ca4abef5ee3 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -19,8 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include +#include #include "anonymous_member.h" diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 549a5b6d77d..ef714518d90 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -16,8 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include -#include #include #include "expr2cpp.h" diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 75aebd7f4b4..adb89b60c1d 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -20,11 +20,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include -#include - #include "cpp_exception_id.h" #include "cpp_type2name.h" #include "expr2cpp.h" diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index c4c85637878..c858a8dd8f7 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -14,8 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include - -#include +#include /// Initialize an object with a value void cpp_typecheckt::convert_initializer(symbolt &symbol) diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index e530536a892..ac1b9c07bc0 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -17,11 +17,11 @@ Author: Kareem Khazem , 2017 #include #include #include +#include #include #include -#include #include diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 934b610e728..9297e93bb25 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -19,8 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include +#include #include diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 1fff82d17fa..06c71e1656a 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -17,8 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include +#include inline static typet c_sizeof_type_rec(const exprt &expr) { diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 4b672574aab..98d12d146ff 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include +#include void goto_symext::symex_start_thread(statet &state) { diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt index f33232fd156..4534ff02476 100644 --- a/src/linking/CMakeLists.txt +++ b/src/linking/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(linking ${sources}) generic_includes(linking) -target_link_libraries(linking util ansi-c) +target_link_libraries(linking util) diff --git a/src/linking/Makefile b/src/linking/Makefile index a2030500ec4..f1a52517dae 100644 --- a/src/linking/Makefile +++ b/src/linking/Makefile @@ -1,7 +1,6 @@ SRC = linking.cpp \ remove_internal_symbols.cpp \ static_lifetime_init.cpp \ - zero_initializer.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/linking/module_dependencies.txt b/src/linking/module_dependencies.txt index e5b9de47bd8..c686b60d2d7 100644 --- a/src/linking/module_dependencies.txt +++ b/src/linking/module_dependencies.txt @@ -1,4 +1,3 @@ -ansi-c # should go away goto-programs langapi # should go away linking diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 8178f839ea1..574549d3079 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -11,19 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include -#include +#include #include +#include #include - -#include +#include +#include +#include #include -#include "zero_initializer.h" - bool static_lifetime_init( symbol_tablet &symbol_table, const source_locationt &source_location, diff --git a/src/util/Makefile b/src/util/Makefile index 6afa460e650..784a6d26a84 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -98,6 +98,7 @@ SRC = arith_tools.cpp \ xml.cpp \ xml_expr.cpp \ xml_irep.cpp \ + zero_initializer.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/linking/zero_initializer.cpp b/src/util/zero_initializer.cpp similarity index 89% rename from src/linking/zero_initializer.cpp rename to src/util/zero_initializer.cpp index 675cdb7dd7f..ee41471d717 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/util/zero_initializer.cpp @@ -1,24 +1,24 @@ /*******************************************************************\ -Module: Linking: Zero Initialization +Module: Zero Initialization Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Linking: Zero Initialization +/// Zero Initialization #include "zero_initializer.h" -#include -#include -#include -#include -#include -#include - -#include +#include "arith_tools.h" +#include "c_types.h" +#include "format_expr.h" +#include "format_type.h" +#include "message.h" +#include "namespace.h" +#include "pointer_offset_size.h" +#include "std_expr.h" class zero_initializert:public messaget { @@ -41,16 +41,6 @@ class zero_initializert:public messaget protected: const namespacet &ns; - std::string to_string(const exprt &src) - { - return expr2c(src, ns); - } - - std::string to_string(const typet &src) - { - return type2c(src, ns); - } - exprt zero_initializer_rec( const typet &type, const source_locationt &source_location); @@ -137,15 +127,14 @@ exprt zero_initializert::zero_initializer_rec( { error().source_location=source_location; error() << "failed to zero-initialize array of non-fixed size `" - << to_string(array_type.size()) << "'" << eom; + << format(array_type.size()) << "'" << eom; throw 0; } if(array_size<0) { error().source_location=source_location; - error() << "failed to zero-initialize array of with negative size" - << eom; + error() << "failed to zero-initialize array with negative size" << eom; throw 0; } @@ -167,15 +156,14 @@ exprt zero_initializert::zero_initializer_rec( { error().source_location=source_location; error() << "failed to zero-initialize vector of non-fixed size `" - << to_string(vector_type.size()) << "'" << eom; + << format(vector_type.size()) << "'" << eom; throw 0; } if(vector_size<0) { error().source_location=source_location; - error() << "failed to zero-initialize vector of with negative size" - << eom; + error() << "failed to zero-initialize vector with negative size" << eom; throw 0; } @@ -299,8 +287,7 @@ exprt zero_initializert::zero_initializer_rec( else { error().source_location=source_location; - error() << "failed to zero-initialize `" << to_string(type) - << "'" << eom; + error() << "failed to zero-initialize `" << format(type) << "'" << eom; throw 0; } } diff --git a/src/linking/zero_initializer.h b/src/util/zero_initializer.h similarity index 69% rename from src/linking/zero_initializer.h rename to src/util/zero_initializer.h index 3bb440b8b74..0c11845add3 100644 --- a/src/linking/zero_initializer.h +++ b/src/util/zero_initializer.h @@ -1,18 +1,18 @@ /*******************************************************************\ -Module: Linking: Zero Initialization +Module: Zero Initialization Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Linking: Zero Initialization +/// Zero Initialization -#ifndef CPROVER_LINKING_ZERO_INITIALIZER_H -#define CPROVER_LINKING_ZERO_INITIALIZER_H +#ifndef CPROVER_UTIL_ZERO_INITIALIZER_H +#define CPROVER_UTIL_ZERO_INITIALIZER_H -#include +#include "expr.h" class message_handlert; class namespacet; @@ -30,4 +30,4 @@ exprt zero_initializer( const source_locationt &, const namespacet &); -#endif // CPROVER_LINKING_ZERO_INITIALIZER_H +#endif // CPROVER_UTIL_ZERO_INITIALIZER_H From 626fb98212ed4272eeaf18926fca9144baa9bd16 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 22 May 2018 15:08:41 +0100 Subject: [PATCH 2/5] Rename zero_initializer to expr_initializer in preparation of generalisation --- .../java_bytecode_convert_class.cpp | 2 +- .../java_bytecode_convert_method.cpp | 2 +- .../java_bytecode_typecheck_expr.cpp | 2 +- .../src/java_bytecode/java_object_factory.cpp | 2 +- .../java_bytecode/java_string_literals.cpp | 2 +- jbmc/src/java_bytecode/remove_java_new.cpp | 2 +- src/ansi-c/c_typecheck_code.cpp | 2 +- src/ansi-c/c_typecheck_initializer.cpp | 2 +- src/cpp/cpp_typecheck.cpp | 2 +- src/cpp/cpp_typecheck_expr.cpp | 2 +- src/cpp/cpp_typecheck_initializer.cpp | 2 +- src/goto-cc/linker_script_merge.cpp | 2 +- src/goto-programs/builtin_functions.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_start_thread.cpp | 2 +- src/linking/static_lifetime_init.cpp | 2 +- src/util/Makefile | 2 +- ...o_initializer.cpp => expr_initializer.cpp} | 39 ++++++++++--------- ...{zero_initializer.h => expr_initializer.h} | 10 ++--- 19 files changed, 42 insertions(+), 41 deletions(-) rename src/util/{zero_initializer.cpp => expr_initializer.cpp} (88%) rename src/util/{zero_initializer.h => expr_initializer.h} (74%) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 0c281f54274..52f79249fad 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -23,10 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include -#include class java_bytecode_convert_classt:public messaget { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 35f153261c2..a6f2996a215 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -31,7 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 9b39368216c..83dcaa6dd9b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -12,8 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_typecheck.h" #include +#include #include -#include #include "java_pointer_casts.h" #include "java_types.h" diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 61968f243e2..14329aaaba4 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_object_factory.h" +#include #include #include #include -#include #include #include diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index 3292f9548f9..b4de86b1cd4 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -12,9 +12,9 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_utils.h" #include +#include #include #include -#include #include #include diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 948bc2e3fc8..d6676d678dd 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -17,10 +17,10 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include -#include class remove_java_newt : public messaget { diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 77d867356ba..31eda7a4c33 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" #include -#include +#include #include "ansi_c_declaration.h" diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index ca4abef5ee3..977ad82f43f 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -14,12 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include #include #include -#include #include "anonymous_member.h" diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index ef714518d90..16d307e2324 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include -#include #include diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index adb89b60c1d..1476b0e2028 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -19,8 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include -#include #include diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index c858a8dd8f7..adc598e855c 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include -#include /// Initialize an object with a value void cpp_typecheckt::convert_initializer(symbolt &symbol) diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index ac1b9c07bc0..6a132bf88bb 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -14,10 +14,10 @@ Author: Kareem Khazem , 2017 #include #include +#include #include #include #include -#include #include diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 9297e93bb25..74bf5ede7a4 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -16,10 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include -#include #include diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 06c71e1656a..0d6455dc142 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include #include -#include inline static typet c_sizeof_type_rec(const exprt &expr) { diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 98d12d146ff..9986812598e 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include +#include void goto_symext::symex_start_thread(statet &state) { diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 574549d3079..3da62aec260 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -14,11 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include #include -#include #include diff --git a/src/util/Makefile b/src/util/Makefile index 784a6d26a84..10e7c6b3125 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -11,6 +11,7 @@ SRC = arith_tools.cpp \ dstring.cpp \ endianness_map.cpp \ expr.cpp \ + expr_initializer.cpp \ expr_util.cpp \ file_util.cpp \ find_macros.cpp \ @@ -98,7 +99,6 @@ SRC = arith_tools.cpp \ xml.cpp \ xml_expr.cpp \ xml_irep.cpp \ - zero_initializer.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/util/zero_initializer.cpp b/src/util/expr_initializer.cpp similarity index 88% rename from src/util/zero_initializer.cpp rename to src/util/expr_initializer.cpp index ee41471d717..52f3d7c9370 100644 --- a/src/util/zero_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -1,15 +1,15 @@ /*******************************************************************\ -Module: Zero Initialization +Module: Expression Initialization Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Zero Initialization +/// Expression Initialization -#include "zero_initializer.h" +#include "expr_initializer.h" #include "arith_tools.h" #include "c_types.h" @@ -20,10 +20,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" #include "std_expr.h" -class zero_initializert:public messaget +class expr_initializert : public messaget { public: - zero_initializert( + expr_initializert( const namespacet &_ns, message_handlert &_message_handler): messaget(_message_handler), @@ -35,18 +35,18 @@ class zero_initializert:public messaget const typet &type, const source_locationt &source_location) { - return zero_initializer_rec(type, source_location); + return expr_initializer_rec(type, source_location); } protected: const namespacet &ns; - exprt zero_initializer_rec( + exprt expr_initializer_rec( const typet &type, const source_locationt &source_location); }; -exprt zero_initializert::zero_initializer_rec( +exprt expr_initializert::expr_initializer_rec( const typet &type, const source_locationt &source_location) { @@ -86,7 +86,7 @@ exprt zero_initializert::zero_initializer_rec( } else if(type_id==ID_complex) { - exprt sub_zero=zero_initializer_rec(type.subtype(), source_location); + exprt sub_zero = expr_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; @@ -113,7 +113,8 @@ exprt zero_initializert::zero_initializer_rec( } else { - exprt tmpval=zero_initializer_rec(array_type.subtype(), source_location); + exprt tmpval = + expr_initializer_rec(array_type.subtype(), source_location); mp_integer array_size; @@ -148,7 +149,7 @@ exprt zero_initializert::zero_initializer_rec( { const vector_typet &vector_type=to_vector_type(type); - exprt tmpval=zero_initializer_rec(vector_type.subtype(), source_location); + exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location); mp_integer vector_size; @@ -195,7 +196,7 @@ exprt zero_initializert::zero_initializer_rec( } else value.copy_to_operands( - zero_initializer_rec(it->type(), source_location)); + expr_initializer_rec(it->type(), source_location)); } value.add_source_location()=source_location; @@ -245,14 +246,14 @@ exprt zero_initializert::zero_initializer_rec( { value.set_component_name(component.get_name()); value.op()= - zero_initializer_rec(component.type(), source_location); + expr_initializer_rec(component.type(), source_location); } return value; } else if(type_id==ID_symbol) { - exprt result=zero_initializer_rec(ns.follow(type), source_location); + exprt result = expr_initializer_rec(ns.follow(type), source_location); // we might have mangled the type for arrays, so keep that if(ns.follow(type).id()!=ID_array) result.type()=type; @@ -262,21 +263,21 @@ exprt zero_initializert::zero_initializer_rec( else if(type_id==ID_c_enum_tag) { return - zero_initializer_rec( + expr_initializer_rec( ns.follow_tag(to_c_enum_tag_type(type)), source_location); } else if(type_id==ID_struct_tag) { return - zero_initializer_rec( + expr_initializer_rec( ns.follow_tag(to_struct_tag_type(type)), source_location); } else if(type_id==ID_union_tag) { return - zero_initializer_rec( + expr_initializer_rec( ns.follow_tag(to_union_tag_type(type)), source_location); } @@ -298,7 +299,7 @@ exprt zero_initializer( const namespacet &ns, message_handlert &message_handler) { - zero_initializert z_i(ns, message_handler); + expr_initializert z_i(ns, message_handler); return z_i(type, source_location); } @@ -312,7 +313,7 @@ exprt zero_initializer( try { - zero_initializert z_i(ns, mh); + expr_initializert z_i(ns, mh); return z_i(type, source_location); } catch(int) diff --git a/src/util/zero_initializer.h b/src/util/expr_initializer.h similarity index 74% rename from src/util/zero_initializer.h rename to src/util/expr_initializer.h index 0c11845add3..24f55468d54 100644 --- a/src/util/zero_initializer.h +++ b/src/util/expr_initializer.h @@ -1,16 +1,16 @@ /*******************************************************************\ -Module: Zero Initialization +Module: Expression Initialization Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Zero Initialization +/// Expression Initialization -#ifndef CPROVER_UTIL_ZERO_INITIALIZER_H -#define CPROVER_UTIL_ZERO_INITIALIZER_H +#ifndef CPROVER_UTIL_EXPR_INITIALIZER_H +#define CPROVER_UTIL_EXPR_INITIALIZER_H #include "expr.h" @@ -30,4 +30,4 @@ exprt zero_initializer( const source_locationt &, const namespacet &); -#endif // CPROVER_UTIL_ZERO_INITIALIZER_H +#endif // CPROVER_UTIL_EXPR_INITIALIZER_H From cf41a88a621c1e4b74cca831086808a2e82d8095 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 14:35:47 +0100 Subject: [PATCH 3/5] nondet_initializer to build deep non-deterministic expressions Create a side_effect_expr_nondett for all PODs or types of unknown/unbounded size, and arrays/structs/vectors/unions of non-deterministic expressions. For example, struct { int; float; } will yield a struct{nondet(int), nondet(float)}. --- src/util/expr_initializer.cpp | 114 +++++++++++++++++++++++++++++----- src/util/expr_initializer.h | 11 ++++ 2 files changed, 110 insertions(+), 15 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 52f3d7c9370..d8ee8a7c0a0 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -18,8 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "message.h" #include "namespace.h" #include "pointer_offset_size.h" +#include "std_code.h" #include "std_expr.h" +template class expr_initializert : public messaget { public: @@ -46,7 +48,8 @@ class expr_initializert : public messaget const source_locationt &source_location); }; -exprt expr_initializert::expr_initializer_rec( +template +exprt expr_initializert::expr_initializer_rec( const typet &type, const source_locationt &source_location) { @@ -63,38 +66,62 @@ exprt expr_initializert::expr_initializer_rec( type_id==ID_floatbv || type_id==ID_fixedbv) { - exprt result=from_integer(0, type); + exprt result; + if(nondet) + result = side_effect_expr_nondett(type); + else + result = from_integer(0, type); + result.add_source_location()=source_location; return result; } else if(type_id==ID_rational || type_id==ID_real) { - constant_exprt result(ID_0, type); + exprt result; + if(nondet) + result = side_effect_expr_nondett(type); + else + result = constant_exprt(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'); + exprt result; + if(nondet) + result = side_effect_expr_nondett(type); + else + { + const std::size_t width = to_bitvector_type(type).get_width(); + std::string value(width, '0'); + + result = constant_exprt(value, type); + } - constant_exprt result(value, type); result.add_source_location()=source_location; return result; } else if(type_id==ID_complex) { - exprt sub_zero = expr_initializer_rec(type.subtype(), source_location); - complex_exprt result(sub_zero, sub_zero, to_complex_type(type)); + exprt result; + if(nondet) + result = side_effect_expr_nondett(type); + else + { + exprt sub_zero = expr_initializer_rec(type.subtype(), source_location); + result = complex_exprt(sub_zero, sub_zero, to_complex_type(type)); + } + result.add_source_location()=source_location; return result; } else if(type_id==ID_code) { error().source_location=source_location; - error() << "cannot zero-initialize code-type" << eom; + error() << "cannot initialize code-type" << eom; throw 0; } else if(type_id==ID_array) @@ -120,12 +147,26 @@ exprt expr_initializert::expr_initializer_rec( if(array_type.size().id()==ID_infinity) { + if(nondet) + { + side_effect_expr_nondett result(type); + result.add_source_location() = source_location; + return result; + } + array_of_exprt value(tmpval, array_type); value.add_source_location()=source_location; return value; } else if(to_integer(array_type.size(), array_size)) { + if(nondet) + { + side_effect_expr_nondett result(type); + result.add_source_location() = source_location; + return result; + } + error().source_location=source_location; error() << "failed to zero-initialize array of non-fixed size `" << format(array_type.size()) << "'" << eom; @@ -135,7 +176,7 @@ exprt expr_initializert::expr_initializer_rec( if(array_size<0) { error().source_location=source_location; - error() << "failed to zero-initialize array with negative size" << eom; + error() << "failed to initialize array with negative size" << eom; throw 0; } @@ -155,6 +196,13 @@ exprt expr_initializert::expr_initializer_rec( if(to_integer(vector_type.size(), vector_size)) { + if(nondet) + { + side_effect_expr_nondett result(type); + result.add_source_location() = source_location; + return result; + } + error().source_location=source_location; error() << "failed to zero-initialize vector of non-fixed size `" << format(vector_type.size()) << "'" << eom; @@ -164,7 +212,7 @@ exprt expr_initializert::expr_initializer_rec( if(vector_size<0) { error().source_location=source_location; - error() << "failed to zero-initialize vector with negative size" << eom; + error() << "failed to initialize vector with negative size" << eom; throw 0; } @@ -283,12 +331,19 @@ exprt expr_initializert::expr_initializer_rec( } else if(type_id==ID_string) { - return constant_exprt(irep_idt(), type); + exprt result; + if(nondet) + result = side_effect_expr_nondett(type); + else + result = constant_exprt(irep_idt(), type); + + result.add_source_location()=source_location; + return result; } else { error().source_location=source_location; - error() << "failed to zero-initialize `" << format(type) << "'" << eom; + error() << "failed to initialize `" << format(type) << "'" << eom; throw 0; } } @@ -299,7 +354,17 @@ exprt zero_initializer( const namespacet &ns, message_handlert &message_handler) { - expr_initializert z_i(ns, message_handler); + expr_initializert z_i(ns, message_handler); + return z_i(type, source_location); +} + +exprt nondet_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns, + message_handlert &message_handler) +{ + expr_initializert z_i(ns, message_handler); return z_i(type, source_location); } @@ -313,7 +378,26 @@ exprt zero_initializer( try { - expr_initializert z_i(ns, mh); + expr_initializert z_i(ns, mh); + return z_i(type, source_location); + } + catch(int) + { + throw oss.str(); + } +} + +exprt nondet_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns) +{ + std::ostringstream oss; + stream_message_handlert mh(oss); + + try + { + expr_initializert z_i(ns, mh); return z_i(type, source_location); } catch(int) diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h index 24f55468d54..696c0d9c3fe 100644 --- a/src/util/expr_initializer.h +++ b/src/util/expr_initializer.h @@ -24,10 +24,21 @@ exprt zero_initializer( const namespacet &, message_handlert &); +exprt nondet_initializer( + const typet &, + const source_locationt &, + const namespacet &, + message_handlert &); + // throws a char* in case of failure exprt zero_initializer( const typet &, const source_locationt &, const namespacet &); +exprt nondet_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns); + #endif // CPROVER_UTIL_EXPR_INITIALIZER_H From 4031eaca3a23e25c6aaba4f39ab0ee7d24cd0b95 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Jun 2018 09:31:12 +0000 Subject: [PATCH 4/5] Non-negative array/vector sizes are invariants --- src/util/expr_initializer.cpp | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index d8ee8a7c0a0..90510770fef 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_types.h" #include "format_expr.h" #include "format_type.h" +#include "invariant.h" #include "message.h" #include "namespace.h" #include "pointer_offset_size.h" @@ -173,12 +174,8 @@ exprt expr_initializert::expr_initializer_rec( throw 0; } - if(array_size<0) - { - error().source_location=source_location; - error() << "failed to initialize array with negative size" << eom; - throw 0; - } + DATA_INVARIANT( + array_size >= 0, "array should not have negative size"); array_exprt value(array_type); value.operands().resize(integer2unsigned(array_size), tmpval); @@ -209,12 +206,8 @@ exprt expr_initializert::expr_initializer_rec( throw 0; } - if(vector_size<0) - { - error().source_location=source_location; - error() << "failed to initialize vector with negative size" << eom; - throw 0; - } + DATA_INVARIANT( + vector_size >= 0, "vector should not have negative size"); vector_exprt value(vector_type); value.operands().resize(integer2unsigned(vector_size), tmpval); From 60ab7ecfb0e2ef1b3f6339c139311a6bb3f7fb07 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Jun 2018 09:31:17 +0000 Subject: [PATCH 5/5] Array/vector sizes can be size_t --- src/util/expr_initializer.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 90510770fef..e7504dd861d 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -178,7 +178,7 @@ exprt expr_initializert::expr_initializer_rec( array_size >= 0, "array should not have negative size"); array_exprt value(array_type); - value.operands().resize(integer2unsigned(array_size), tmpval); + value.operands().resize(integer2size_t(array_size), tmpval); value.add_source_location()=source_location; return value; } @@ -210,7 +210,7 @@ exprt expr_initializert::expr_initializer_rec( vector_size >= 0, "vector should not have negative size"); vector_exprt value(vector_type); - value.operands().resize(integer2unsigned(vector_size), tmpval); + value.operands().resize(integer2size_t(vector_size), tmpval); value.add_source_location()=source_location; return value;