From 6cc1266de12af40c9c1b852e5272a3c2aa82e872 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 27 Feb 2017 10:40:20 +0000 Subject: [PATCH 1/5] Adding refined_string_type to util Makefile --- src/util/Makefile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/util/Makefile b/src/util/Makefile index e9dd739db8e..61cff93b9f0 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -23,7 +23,11 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ ssa_expr.cpp json_irep.cpp json_expr.cpp \ fresh_symbol.cpp \ - format_number_range.cpp string_utils.cpp nondet_ifthenelse.cpp + format_number_range.cpp \ + nondet_ifthenelse.cpp \ + string_utils.cpp \ + refined_string_type.cpp \ + #Empty last line INCLUDES= -I .. From 402f8e180f04ffbf1ce73aad1ea9e084a3cb4837 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 10 Jan 2017 13:42:48 +0000 Subject: [PATCH 2/5] Adding string preprocessing of goto-programs to Makefile --- src/goto-programs/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 1b303c759b9..1d8ac6e1752 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -24,7 +24,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_instanceof.cpp \ class_identifier.cpp \ system_library_symbols.cpp \ - + string_refine_preprocess.cpp \ + # Empty last line INCLUDES= -I .. From 05582912383fd88e01e74a6b1107d2f18d46ee76 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 10 Jan 2017 13:43:30 +0000 Subject: [PATCH 3/5] Adding string solver cpp files to Makefile --- src/solvers/Makefile | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 95ea7650274..136db5765c1 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -118,6 +118,17 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \ floatbv/float_utils.cpp floatbv/float_bv.cpp \ refinement/bv_refinement_loop.cpp refinement/refine_arithmetic.cpp \ refinement/refine_arrays.cpp \ + refinement/string_refinement.cpp \ + refinement/string_constraint_generator_code_points.cpp \ + refinement/string_constraint_generator_comparison.cpp \ + refinement/string_constraint_generator_concat.cpp \ + refinement/string_constraint_generator_constants.cpp \ + refinement/string_constraint_generator_indexof.cpp \ + refinement/string_constraint_generator_insert.cpp \ + refinement/string_constraint_generator_main.cpp \ + refinement/string_constraint_generator_testing.cpp \ + refinement/string_constraint_generator_transformation.cpp \ + refinement/string_constraint_generator_valueof.cpp \ miniBDD/miniBDD.cpp INCLUDES += -I .. \ From c7328e225f1e00e34aff9afe3067e4dfd02d30e9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 10 Jan 2017 13:36:33 +0000 Subject: [PATCH 4/5] Adding the string refinement option to the CBMC solvers We add the option `--string-refine` which can be used to activate the string solver, in order to deal precisely with string functions. --- src/cbmc/cbmc_parse_options.cpp | 15 +++++++++++++++ src/cbmc/cbmc_parse_options.h | 1 + src/cbmc/cbmc_solvers.cpp | 24 ++++++++++++++++++++++++ src/cbmc/cbmc_solvers.h | 13 ++++++++----- 4 files changed, 48 insertions(+), 5 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..b6a96d1e178 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -310,6 +311,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("refine-arithmetic", true); } + if(cmdline.isset("string-refine")) + { + options.set_option("string-refine", true); + } + if(cmdline.isset("max-node-refinement")) options.set_option( "max-node-refinement", @@ -904,6 +910,14 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); + + if(cmdline.isset("string-refine")) + { + status() << "Preprocessing for string refinement" << eom; + string_refine_preprocesst( + symbol_table, goto_functions, ui_message_handler); + } + // remove returns, gcc vectors, complex remove_returns(symbol_table, goto_functions); remove_vector(symbol_table, goto_functions); @@ -1191,6 +1205,7 @@ void cbmc_parse_optionst::help() " --yices use Yices\n" " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" + " --string-refine use string refinement (experimental)\n" " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a3fc5e7e7d3..c6ed41c1e6a 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -37,6 +37,7 @@ class optionst; "(no-sat-preprocessor)" \ "(no-pretty-names)(beautify)" \ "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ + "(string-refine)" \ "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index ccd660dc586..a72546a8d0c 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -213,6 +214,29 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement() /*******************************************************************\ +Function: cbmc_solverst::get_string_refinement + + Outputs: a solver for cbmc + + Purpose: the string refinement adds to the bit vector refinement + specifications for functions from the Java string library + +\*******************************************************************/ + +cbmc_solverst::solvert* cbmc_solverst::get_string_refinement() +{ + propt *prop; + prop=new satcheck_no_simplifiert(); + prop->set_message_handler(get_message_handler()); + + string_refinementt *string_refinement=new string_refinementt( + ns, *prop, MAX_NB_REFINEMENT); + string_refinement->set_ui(ui); + return new solvert(string_refinement, prop); +} + +/*******************************************************************\ + Function: cbmc_solverst::get_smt1 Inputs: diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 42d47fcaed3..be4a0e0ccde 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -111,15 +111,17 @@ class cbmc_solverst:public messaget solvert *solver; if(options.get_bool_option("dimacs")) - solver = get_dimacs(); + solver=get_dimacs(); else if(options.get_bool_option("refine")) - solver = get_bv_refinement(); + solver=get_bv_refinement(); + else if(options.get_bool_option("string-refine")) + solver=get_string_refinement(); else if(options.get_bool_option("smt1")) - solver = get_smt1(get_smt1_solver_type()); + solver=get_smt1(get_smt1_solver_type()); else if(options.get_bool_option("smt2")) - solver = get_smt2(get_smt2_solver_type()); + solver=get_smt2(get_smt2_solver_type()); else - solver = get_default(); + solver=get_default(); return std::unique_ptr(solver); } @@ -141,6 +143,7 @@ class cbmc_solverst:public messaget solvert *get_default(); solvert *get_dimacs(); solvert *get_bv_refinement(); + solvert *get_string_refinement(); solvert *get_smt1(smt1_dect::solvert solver); solvert *get_smt2(smt2_dect::solvert solver); From 9d2a1158dd4ff7f42083efcf47c80b8b1bc6b947 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 23 Mar 2017 18:18:14 +0000 Subject: [PATCH 5/5] Change option name to --refine-strings --- src/cbmc/cbmc_parse_options.cpp | 8 ++++---- src/cbmc/cbmc_parse_options.h | 2 +- src/cbmc/cbmc_solvers.h | 2 +- src/java_bytecode/java_bytecode_language.cpp | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b6a96d1e178..b90afbb307e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -311,9 +311,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("refine-arithmetic", true); } - if(cmdline.isset("string-refine")) + if(cmdline.isset("refine-strings")) { - options.set_option("string-refine", true); + options.set_option("refine-strings", true); } if(cmdline.isset("max-node-refinement")) @@ -911,7 +911,7 @@ bool cbmc_parse_optionst::process_goto_program( goto_partial_inline(goto_functions, ns, ui_message_handler); - if(cmdline.isset("string-refine")) + if(cmdline.isset("refine-strings")) { status() << "Preprocessing for string refinement" << eom; string_refine_preprocesst( @@ -1205,7 +1205,7 @@ void cbmc_parse_optionst::help() " --yices use Yices\n" " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" - " --string-refine use string refinement (experimental)\n" + " --refine-strings use string refinement (experimental)\n" " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index c6ed41c1e6a..266984c5c17 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -37,7 +37,7 @@ class optionst; "(no-sat-preprocessor)" \ "(no-pretty-names)(beautify)" \ "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ - "(string-refine)" \ + "(refine-strings)" \ "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index be4a0e0ccde..c837bd55806 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -114,7 +114,7 @@ class cbmc_solverst:public messaget solver=get_dimacs(); else if(options.get_bool_option("refine")) solver=get_bv_refinement(); - else if(options.get_bool_option("string-refine")) + else if(options.get_bool_option("refine-strings")) solver=get_string_refinement(); else if(options.get_bool_option("smt1")) solver=get_smt1(get_smt1_solver_type()); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 9faa16f676a..8ab88cf9dc6 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -44,7 +44,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { disable_runtime_checks=cmd.isset("disable-runtime-check"); assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); - string_refinement_enabled=cmd.isset("string-refine"); + string_refinement_enabled=cmd.isset("refine-strings"); if(cmd.isset("java-max-input-array-length")) max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length"));