From 99ea8fe61f8c7b4d050ece19a7b50a7002ef29f2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 15 Jan 2018 14:27:36 +0000 Subject: [PATCH 1/4] JBMC: run replace-Java-nondet on function-by-function basis --- src/goto-programs/replace_java_nondet.cpp | 10 ++++++++++ src/goto-programs/replace_java_nondet.h | 6 ++++++ src/jbmc/jbmc_parse_options.cpp | 4 ++-- 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp index b030cbaa312..431acc0efb2 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/goto-programs/replace_java_nondet.cpp @@ -235,6 +235,16 @@ static void replace_java_nondet(goto_programt &goto_program) } } +void replace_java_nondet(goto_model_functiont &function) +{ + goto_programt &program = function.get_goto_function().body; + replace_java_nondet(program); + + function.compute_location_numbers(); + + remove_skip(program); +} + void replace_java_nondet(goto_functionst &goto_functions) { for(auto &goto_program : goto_functions.function_map) diff --git a/src/goto-programs/replace_java_nondet.h b/src/goto-programs/replace_java_nondet.h index ac8f8cfb005..3653908588d 100644 --- a/src/goto-programs/replace_java_nondet.h +++ b/src/goto-programs/replace_java_nondet.h @@ -14,6 +14,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com class goto_modelt; class goto_functionst; +class goto_model_functiont; /// Replace calls to nondet library functions with an internal nondet /// representation. @@ -22,4 +23,9 @@ void replace_java_nondet(goto_modelt &); void replace_java_nondet(goto_functionst &); +/// Replace calls to nondet library functions with an internal nondet +/// representation in a single function. +/// \param function: The goto program to modify. +void replace_java_nondet(goto_model_functiont &function); + #endif diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index d86c5dc9258..17890ee1279 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -664,6 +664,8 @@ void jbmc_parse_optionst::process_goto_function( }; remove_returns(function, function_is_stub); + + replace_java_nondet(function); } catch(const char *e) @@ -718,8 +720,6 @@ bool jbmc_parse_optionst::process_goto_functions( ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) : MAX_NONDET_TREE_DEPTH; - replace_java_nondet(goto_model); - convert_nondet( goto_model, get_message_handler(), From db3bc99c80aa64f23175813f9b0593cca3e3cde9 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 15 Jan 2018 14:34:48 +0000 Subject: [PATCH 2/4] JBMC: run convert-nondet on a per-function basis --- src/goto-programs/convert_nondet.cpp | 14 +++++++++ src/goto-programs/convert_nondet.h | 12 ++++++++ src/jbmc/jbmc_parse_options.cpp | 44 ++++++++++++++-------------- 3 files changed, 48 insertions(+), 22 deletions(-) diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index 27d1017aced..6e6950f95ce 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -130,6 +130,20 @@ void convert_nondet( } } +void convert_nondet( + goto_model_functiont &function, + message_handlert &message_handler, + const object_factory_parameterst &object_factory_parameters) +{ + convert_nondet( + function.get_goto_function().body, + function.get_symbol_table(), + message_handler, + object_factory_parameters); + + function.compute_location_numbers(); +} + void convert_nondet( goto_functionst &goto_functions, symbol_tablet &symbol_table, diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h index 95b48ae5dd7..14a2840eb68 100644 --- a/src/goto-programs/convert_nondet.h +++ b/src/goto-programs/convert_nondet.h @@ -17,6 +17,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com class goto_functionst; class symbol_tablet; class goto_modelt; +class goto_model_functiont; class message_handlert; struct object_factory_parameterst; @@ -38,4 +39,15 @@ void convert_nondet( message_handlert &, const object_factory_parameterst &object_factory_parameters); +/// Replace calls to nondet library functions with an internal nondet +/// representation. +/// \param function: goto program to modify +/// \param message_handler: For error logging. +/// \param object_factory_parameters: Parameters for the generation of nondet +/// objects. +void convert_nondet( + goto_model_functiont &function, + message_handlert &message_handler, + const object_factory_parameterst &object_factory_parameters); + #endif diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 17890ee1279..a3a6937cad7 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -666,6 +666,28 @@ void jbmc_parse_optionst::process_goto_function( remove_returns(function, function_is_stub); replace_java_nondet(function); + + // Similar removal of java nondet statements: + // TODO Should really get this from java_bytecode_language somehow, but we + // don't have an instance of that here. + object_factory_parameterst factory_params; + factory_params.max_nondet_array_length= + cmdline.isset("java-max-input-array-length") + ? std::stoul(cmdline.get_value("java-max-input-array-length")) + : MAX_NONDET_ARRAY_LENGTH_DEFAULT; + factory_params.max_nondet_string_length= + cmdline.isset("string-max-input-length") + ? std::stoul(cmdline.get_value("string-max-input-length")) + : MAX_NONDET_STRING_LENGTH; + factory_params.max_nondet_tree_depth= + cmdline.isset("java-max-input-tree-depth") + ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) + : MAX_NONDET_TREE_DEPTH; + + convert_nondet( + function, + get_message_handler(), + factory_params); } catch(const char *e) @@ -703,28 +725,6 @@ bool jbmc_parse_optionst::process_goto_functions( // instrument library preconditions instrument_preconditions(goto_model); - // Similar removal of java nondet statements: - // TODO Should really get this from java_bytecode_language somehow, but we - // don't have an instance of that here. - object_factory_parameterst factory_params; - factory_params.max_nondet_array_length= - cmdline.isset("java-max-input-array-length") - ? std::stoul(cmdline.get_value("java-max-input-array-length")) - : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - factory_params.max_nondet_string_length= - cmdline.isset("string-max-input-length") - ? std::stoul(cmdline.get_value("string-max-input-length")) - : MAX_NONDET_STRING_LENGTH; - factory_params.max_nondet_tree_depth= - cmdline.isset("java-max-input-tree-depth") - ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) - : MAX_NONDET_TREE_DEPTH; - - convert_nondet( - goto_model, - get_message_handler(), - factory_params); - // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(options, goto_model); From eed983a76318e0b73358ba5a475f4cf2842145cb Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 15 Jan 2018 15:01:04 +0000 Subject: [PATCH 3/4] JBMC: add property checks on a per-function basis --- src/analyses/goto_check.cpp | 3 ++- src/analyses/goto_check.h | 1 + src/goto-programs/lazy_goto_model.h | 5 +++-- src/jbmc/jbmc_parse_options.cpp | 11 ++++++----- src/jbmc/jbmc_parse_options.h | 3 ++- 5 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index c36c8b189dc..d88035159b9 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1753,10 +1753,11 @@ void goto_checkt::goto_check( void goto_check( const namespacet &ns, const optionst &options, + const irep_idt &mode, goto_functionst::goto_functiont &goto_function) { goto_checkt goto_check(ns, options); - goto_check.goto_check(goto_function, irep_idt()); + goto_check.goto_check(goto_function, mode); } void goto_check( diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 44d98069de9..7b3d94b7d16 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -26,6 +26,7 @@ void goto_check( void goto_check( const namespacet &ns, const optionst &options, + const irep_idt &mode, goto_functionst::goto_functiont &goto_function); void goto_check( diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index c9f6f612833..362df30c0fb 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -64,8 +64,9 @@ class lazy_goto_modelt : public can_produce_functiont message_handlert &message_handler) { return lazy_goto_modelt( - [&handler] (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*) - handler.process_goto_function(fun, cpf); + [&handler, &options] + (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*) + handler.process_goto_function(fun, cpf, options); }, [&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*) return handler.process_goto_functions(goto_model, options); diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index a3a6937cad7..925bf3561af 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -643,9 +643,11 @@ int jbmc_parse_optionst::get_goto_program( void jbmc_parse_optionst::process_goto_function( goto_model_functiont &function, - const can_produce_functiont &available_functions) + const can_produce_functiont &available_functions, + const optionst &options) { symbol_tablet &symbol_table = function.get_symbol_table(); + namespacet ns(symbol_table); goto_functionst::goto_functiont &goto_function = function.get_goto_function(); try { @@ -688,6 +690,9 @@ void jbmc_parse_optionst::process_goto_function( function, get_message_handler(), factory_params); + + // add generic checks + goto_check(ns, options, ID_java, function.get_goto_function()); } catch(const char *e) @@ -725,10 +730,6 @@ bool jbmc_parse_optionst::process_goto_functions( // instrument library preconditions instrument_preconditions(goto_model); - // add generic checks - status() << "Generic Property Instrumentation" << eom; - goto_check(options, goto_model); - // checks don't know about adjusted float expressions adjust_float_expressions(goto_model); diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index c98b4ca6f49..327e9aa7ca2 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -86,7 +86,8 @@ class jbmc_parse_optionst: void process_goto_function( goto_model_functiont &function, - const can_produce_functiont &); + const can_produce_functiont &, + const optionst &); bool process_goto_functions(goto_modelt &goto_model, const optionst &options); protected: From c91ff69d33fe5cce9711ad3979951f0d394c0619 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 15 Jan 2018 15:05:18 +0000 Subject: [PATCH 4/4] JBMC: adjust float expressions per function --- src/jbmc/jbmc_parse_options.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 925bf3561af..3bf13fc6951 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -693,6 +693,9 @@ void jbmc_parse_optionst::process_goto_function( // add generic checks goto_check(ns, options, ID_java, function.get_goto_function()); + + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_function, ns); } catch(const char *e) @@ -730,9 +733,6 @@ bool jbmc_parse_optionst::process_goto_functions( // instrument library preconditions instrument_preconditions(goto_model); - // checks don't know about adjusted float expressions - adjust_float_expressions(goto_model); - // ignore default/user-specified initialization // of variables with static lifetime if(cmdline.isset("nondet-static"))