From bac97dc4744135a7eda69276a1b1308a012dbb4f Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Mon, 21 May 2018 14:42:34 +0100 Subject: [PATCH] Squashed 'cbmc/' changes from da61186..31ef182 31ef182 Merge pull request #2208 from diffblue/cleanout-goto-programs 0e84d3e Merge pull request #2195 from smowton/smowton/feature/smarter-reachability-slicer c801126 Merge pull request #2209 from diffblue/travis-no-osx-g++ 3487bf7 Reachability slicer: mark reachable code more precisely 85e8451 Merge pull request #2066 from tautschnig/bv-endianness 5e5eafb Merge pull request #2191 from smowton/smowton/feature/java-fatal-assertions 8a68ab8 remove g++ build on OS X; this is identical to the clang++ build 48e5b25 Amend faulty long-string test 3f718ba Java: make null-pointer and similar checks fatal 821eb1d remove basic_blocks and goto_program_irep d87c2db Merge pull request #2203 from diffblue/typed-lookup d77dea3 strongly type the lookup() methods in namespacet 2382f27 Merge pull request #2193 from martin-cs/feature/correct-instruction-documentation c314272 Merge pull request #2181 from diffblue/format-expr-constants 514a0a5 Merge pull request #2167 from diffblue/parse_unwindset_options 0102452 move escape(s) to string_utils f1b6174 use unwindsett in goto-instrument dcc907a introduce unwindsett for unwinding limits 10aeae8 format_expr now does index, c_bool constants, string constants 92b92d6 Correct the documentation of ASSERT : it does not alter control flow. a11add8 Expand the documentation of the goto-program instructions. a06503b Merge pull request #2197 from tautschnig/fix-help 05e4bc3 Remove stray whitespace previously demanded by clang-format 3261f4d Fix help output of --generate-function-body-options 7c67b23 Merge pull request #2110 from tautschnig/type-mismatch-exception 18fb262 Merge pull request #2025 from tautschnig/stack-depth-fix 9191b6a Merge pull request #2199 from tautschnig/simplifier-typing f99e631 Merge pull request #2198 from tautschnig/fix-test-desc 1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty a7690ba Merge pull request #2185 from smowton/smowton/fix/tolerate-ts18661-types fc02e8f Restore returns before writing the simplified binary 49333eb Make restore_returns handle simplified programs 46f7987 Fix perl regular expressioons in regression test descriptions 9fe432b Merge pull request #1899 from danpoe/sharing-map-catch-unit-tests 9cc6aae Merge pull request #2081 from hannes-steffenhagen-diffblue/floating_point_simplificiation da19abe Tolerate TS 18661 (_Float32 et al) types a055454 Try all rounding modes when domain is unknown 5f7bc15 Add float support to constant propagator domain 3dc2244 Move adjust_float_expressions to goto-programs 06d8bea Merge pull request #2187 from diffblue/move-convert-nondet 6d8c3fa Merge pull request #2189 from thk123/bugfix/json-parser-restart 2ad157f Merge pull request #2186 from smowton/smowton/fix/call-graph-uninit-field cd54ad7 Corrected state persistence in the json parser 4447be0 Fix uninitialised collect_callsites field in call_grapht ead0aa3 Merge pull request #2188 from smowton/smowton/fix/init-string-types-without-refine-strings 57988fc Fix String type initialisation when --refine-strings is not active 6a76aff Move convert_nondet to java_bytecode ac6eb21 Merge pull request #1858 from danpoe/dependence-graph-fix 10b8b09 Merge pull request #2011 from thomasspriggs/final_classes a154593 Merge pull request #2087 from danpoe/feature/small-map 7002909 More dependence graph tests 66263ea Make dependence graph merge() return true when abstract state changes 3aa6dca Control dependency computation fix a408423 Simplified state merging in the dependence graph 0315816 Merge pull request #2180 from thomasspriggs/json_id2string 8941567 Merge pull request #2124 from smowton/smowton/feature/fallback-function-provider cd04e70 JBMC: use simple method stubbing pass a6b2cda Add Java simple method stubbing pass ec1127c Lazy goto model: hook for driver program to replace or stub functions b6a4382 Remove `id2string` from inside calls to the `json_stringt` constructor. b673ebb Add storage of final modifier status of java classes in `java_class_typet`. a2ad909 Small map 808dade Provide suitable diagnostics for equality-without-matching-types 89cf6fe Throw appropriate exceptions when converting constraints 2ae66c2 Produce a proper error message when catching a std::runtime_error at top level e7b3ade Workaround for Visual Studio loss of CV qualifier bug 1f661f5 Move sharing map and sharing node unit tests to util 47463a3 Use std::size_t instead of unsigned in the sharing map 3e22217 Sharing map documentation e54f740 Fix sharing map compiler warnings bcc489c Move sharing map unit tests to catch 34114b8 Use a specialised endianness map for flattening git-subtree-dir: cbmc git-subtree-split: 31ef182d87d68f4b1645aa9b660f5902ff6a3a58 --- .travis.yml | 11 - .../NondetCharSequence.class | Bin 0 -> 768 bytes .../NondetCharSequence.java | 10 + .../cbmc-java/NondetCharSequence/test.desc | 8 + .../cbmc-java/NondetString/NondetString.class | Bin 0 -> 738 bytes .../cbmc-java/NondetString/NondetString.java | 10 + regression/cbmc-java/NondetString/test.desc | 8 + .../NondetStringBuffer.class | Bin 0 -> 768 bytes .../NondetStringBuffer.java | 10 + .../cbmc-java/NondetStringBuffer/test.desc | 8 + .../NondetStringBuilder.class | Bin 0 -> 773 bytes .../NondetStringBuilder.java | 10 + .../cbmc-java/NondetStringBuilder/test.desc | 8 + regression/cbmc-java/NullPointer3/test.desc | 2 +- regression/cbmc-java/repeated_guards/A.class | Bin 0 -> 251 bytes regression/cbmc-java/repeated_guards/B.class | Bin 0 -> 216 bytes .../cbmc-java/repeated_guards/Test.class | Bin 0 -> 1391 bytes .../cbmc-java/repeated_guards/Test.java | 45 ++ .../repeated_guards/test_arraybounds.desc | 12 + .../repeated_guards/test_arraycreation.desc | 10 + .../repeated_guards/test_assertion.desc | 10 + .../repeated_guards/test_classcast.desc | 10 + .../repeated_guards/test_divbyzero.desc | 10 + .../repeated_guards/test_nullderef.desc | 10 + .../cbmc/reachability-slice-interproc/test.c | 76 +++ .../reachability-slice-interproc/test.desc | 13 + regression/cbmc/ts18661_typedefs/main.c | 9 + regression/cbmc/ts18661_typedefs/test.desc | 8 + .../test.desc | 12 +- .../test.desc | 12 +- .../test.desc | 12 +- .../test.desc | 12 +- .../test.desc | 12 +- .../test.desc | 12 +- .../constant_propagation_05/test.desc | 2 +- .../constant_propagation_10/test.desc | 2 +- .../constant_propagation_11/test.desc | 4 +- .../constant_propagation_13/test.desc | 2 +- .../constant_propagation_14/test.desc | 4 +- .../constant_propagation_15/test.desc | 2 +- .../main.c | 9 + .../test.desc | 8 + .../main.c | 27 + .../test.desc | 13 + .../constant_propagation_rounding_mode/main.c | 12 + .../test.desc | 9 + .../goto-analyzer/dependence-graph10/main.c | 15 + .../dependence-graph10/test.desc | 39 ++ .../goto-analyzer/dependence-graph11/main.c | 15 + .../dependence-graph11/test.desc | 23 + .../goto-analyzer/dependence-graph12/main.c | 21 + .../dependence-graph12/test.desc | 38 ++ .../goto-analyzer/dependence-graph4/main.c | 16 + .../goto-analyzer/dependence-graph4/test.desc | 22 + .../goto-analyzer/dependence-graph7/main.c | 10 + .../goto-analyzer/dependence-graph7/test.desc | 50 ++ .../goto-analyzer/dependence-graph8/main.c | 13 + .../goto-analyzer/dependence-graph8/test.desc | 54 ++ .../goto-analyzer/dependence-graph9/main.c | 16 + .../goto-analyzer/dependence-graph9/test.desc | 38 ++ .../goto-analyzer/intervals_02/test.desc | 4 +- .../goto-analyzer/intervals_03/test.desc | 2 +- .../goto-analyzer/intervals_04/test.desc | 4 +- .../goto-analyzer/intervals_05/test.desc | 2 +- .../goto-analyzer/intervals_06/test.desc | 2 +- .../goto-analyzer/intervals_07/test.desc | 2 +- .../goto-analyzer/intervals_08/test.desc | 2 +- .../goto-analyzer/intervals_09/test.desc | 4 +- .../goto-analyzer/intervals_10/test.desc | 4 +- .../goto-analyzer/intervals_11/test.desc | 4 +- .../unwind-unwindset3/test.desc | 2 +- .../jbmc-strings/long_string/Test.class | Bin 985 -> 1185 bytes regression/jbmc-strings/long_string/Test.java | 7 +- regression/strings/test_index_of/test.desc | 2 +- regression/strings/test_int/test.desc | 2 +- src/analyses/call_graph.cpp | 3 +- src/analyses/constant_propagator.cpp | 108 +++- src/analyses/constant_propagator.h | 8 + src/analyses/dependence_graph.cpp | 127 ++-- src/analyses/dependence_graph.h | 53 +- src/ansi-c/ansi_c_convert_type.cpp | 19 +- src/ansi-c/c_typecheck_expr.cpp | 2 +- src/cbmc/Makefile | 7 +- src/cbmc/all_properties.cpp | 4 +- src/cbmc/bmc.cpp | 56 +- src/cbmc/bmc.h | 2 - src/cbmc/bmc_cover.cpp | 6 +- src/cbmc/cbmc_parse_options.cpp | 3 +- src/cbmc/symex_bmc.cpp | 44 +- src/cbmc/symex_bmc.h | 45 +- src/clobber/Makefile | 1 - src/cpp/cpp_constructor.cpp | 3 +- src/cpp/cpp_destructor.cpp | 3 +- src/cpp/cpp_instantiate_template.cpp | 2 +- src/cpp/cpp_typecheck_bases.cpp | 4 +- src/cpp/cpp_typecheck_expr.cpp | 6 +- src/cpp/cpp_typecheck_resolve.cpp | 7 +- .../goto_analyzer_parse_options.cpp | 2 + src/goto-analyzer/static_analyzer.cpp | 5 +- src/goto-analyzer/static_simplifier.cpp | 5 + src/goto-analyzer/taint_analysis.cpp | 7 +- .../unreachable_instructions.cpp | 4 +- src/goto-diff/Makefile | 1 - src/goto-diff/goto_diff_base.cpp | 2 +- src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-instrument/Makefile | 1 + src/goto-instrument/cover.cpp | 12 +- .../goto_instrument_parse_options.cpp | 43 +- src/goto-instrument/reachability_slicer.cpp | 119 +++- .../reachability_slicer_class.h | 23 + src/goto-instrument/stack_depth.cpp | 4 +- src/goto-instrument/unwind.cpp | 79 +-- src/goto-instrument/unwind.h | 40 +- src/goto-instrument/unwindset.cpp | 99 +++ src/goto-instrument/unwindset.h | 56 ++ src/goto-instrument/wmm/fence.cpp | 38 +- src/goto-programs/Makefile | 4 +- .../adjust_float_expressions.cpp | 2 +- .../adjust_float_expressions.h | 6 +- src/goto-programs/basic_blocks.cpp | 94 --- src/goto-programs/basic_blocks.h | 20 - src/goto-programs/generate_function_bodies.h | 22 +- src/goto-programs/goto_program.h | 25 +- src/goto-programs/goto_program_irep.cpp | 144 ----- src/goto-programs/goto_program_irep.h | 25 - src/goto-programs/json_goto_trace.cpp | 18 +- src/goto-programs/lazy_goto_functions_map.h | 55 +- src/goto-programs/lazy_goto_model.cpp | 18 +- src/goto-programs/lazy_goto_model.h | 21 + src/goto-programs/remove_returns.cpp | 33 +- .../show_goto_functions_json.cpp | 2 +- src/goto-programs/show_properties.cpp | 11 +- src/goto-symex/Makefile | 3 +- src/goto-symex/symex_assign.cpp | 4 +- src/goto-symex/symex_target_equation.cpp | 17 +- src/java_bytecode/Makefile | 2 + .../convert_java_nondet.cpp} | 13 +- .../convert_java_nondet.h} | 6 +- .../java_bytecode_convert_class.cpp | 1 + .../java_bytecode_instrument.cpp | 67 +- .../java_bytecode_parse_tree.cpp | 1 + src/java_bytecode/java_bytecode_parse_tree.h | 1 + src/java_bytecode/java_bytecode_parser.cpp | 1 + src/java_bytecode/java_object_factory.cpp | 31 +- src/java_bytecode/java_types.h | 10 + src/java_bytecode/simple_method_stubbing.cpp | 280 +++++++++ src/java_bytecode/simple_method_stubbing.h | 34 + src/jbmc/Makefile | 7 +- src/jbmc/jbmc_parse_options.cpp | 87 ++- src/jbmc/jbmc_parse_options.h | 10 + src/json/json_parser.h | 2 + .../goto_program_dereference.cpp | 2 +- src/solvers/Makefile | 1 + .../flattening/boolbv_byte_extract.cpp | 8 +- src/solvers/flattening/boolbv_byte_update.cpp | 11 +- src/solvers/flattening/boolbv_equality.cpp | 12 +- src/solvers/flattening/boolbv_union.cpp | 7 +- src/solvers/flattening/boolbv_with.cpp | 7 +- src/solvers/flattening/bv_endianness_map.cpp | 36 ++ src/solvers/flattening/bv_endianness_map.h | 40 ++ src/util/array_name.cpp | 2 +- src/util/container_utils.h | 57 ++ src/util/endianness_map.h | 8 +- src/util/format_expr.cpp | 110 ++-- src/util/format_expr.h | 2 +- src/util/format_type.cpp | 6 +- src/util/ieee_float.h | 4 + src/util/irep_ids.def | 5 +- src/util/json_expr.cpp | 34 +- src/util/lispexpr.cpp | 17 +- src/util/lispexpr.h | 2 - src/util/namespace.cpp | 47 +- src/util/namespace.h | 25 +- src/util/sharing_map.h | 299 +++++++-- src/util/sharing_node.h | 8 +- src/util/simplify_expr_int.cpp | 4 +- src/util/small_map.h | 590 ++++++++++++++++++ src/util/std_code.cpp | 12 + src/util/std_code.h | 22 +- src/util/string_utils.cpp | 15 + src/util/string_utils.h | 4 + src/util/type_eq.cpp | 10 +- unit/Makefile | 4 +- unit/analyses/call_graph.cpp | 22 + unit/json/invalid.json | 1 + unit/json/json_parser.cpp | 69 ++ unit/json/valid.json | 3 + unit/sharing_map.cpp | 336 ---------- unit/testing-utils/load_java_class.cpp | 2 + unit/util/sharing_map.cpp | 347 ++++++++++ unit/{ => util}/sharing_node.cpp | 77 ++- unit/util/small_map.cpp | 216 +++++++ 192 files changed, 3969 insertions(+), 1524 deletions(-) create mode 100644 regression/cbmc-java/NondetCharSequence/NondetCharSequence.class create mode 100644 regression/cbmc-java/NondetCharSequence/NondetCharSequence.java create mode 100644 regression/cbmc-java/NondetCharSequence/test.desc create mode 100644 regression/cbmc-java/NondetString/NondetString.class create mode 100644 regression/cbmc-java/NondetString/NondetString.java create mode 100644 regression/cbmc-java/NondetString/test.desc create mode 100644 regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class create mode 100644 regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java create mode 100644 regression/cbmc-java/NondetStringBuffer/test.desc create mode 100644 regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class create mode 100644 regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java create mode 100644 regression/cbmc-java/NondetStringBuilder/test.desc create mode 100644 regression/cbmc-java/repeated_guards/A.class create mode 100644 regression/cbmc-java/repeated_guards/B.class create mode 100644 regression/cbmc-java/repeated_guards/Test.class create mode 100644 regression/cbmc-java/repeated_guards/Test.java create mode 100644 regression/cbmc-java/repeated_guards/test_arraybounds.desc create mode 100644 regression/cbmc-java/repeated_guards/test_arraycreation.desc create mode 100644 regression/cbmc-java/repeated_guards/test_assertion.desc create mode 100644 regression/cbmc-java/repeated_guards/test_classcast.desc create mode 100644 regression/cbmc-java/repeated_guards/test_divbyzero.desc create mode 100644 regression/cbmc-java/repeated_guards/test_nullderef.desc create mode 100644 regression/cbmc/reachability-slice-interproc/test.c create mode 100644 regression/cbmc/reachability-slice-interproc/test.desc create mode 100644 regression/cbmc/ts18661_typedefs/main.c create mode 100644 regression/cbmc/ts18661_typedefs/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_floating_point_div/main.c create mode 100644 regression/goto-analyzer/constant_propagation_floating_point_div/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c create mode 100644 regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_rounding_mode/main.c create mode 100644 regression/goto-analyzer/constant_propagation_rounding_mode/test.desc create mode 100644 regression/goto-analyzer/dependence-graph10/main.c create mode 100644 regression/goto-analyzer/dependence-graph10/test.desc create mode 100644 regression/goto-analyzer/dependence-graph11/main.c create mode 100644 regression/goto-analyzer/dependence-graph11/test.desc create mode 100644 regression/goto-analyzer/dependence-graph12/main.c create mode 100644 regression/goto-analyzer/dependence-graph12/test.desc create mode 100644 regression/goto-analyzer/dependence-graph4/main.c create mode 100644 regression/goto-analyzer/dependence-graph4/test.desc create mode 100644 regression/goto-analyzer/dependence-graph7/main.c create mode 100644 regression/goto-analyzer/dependence-graph7/test.desc create mode 100644 regression/goto-analyzer/dependence-graph8/main.c create mode 100644 regression/goto-analyzer/dependence-graph8/test.desc create mode 100644 regression/goto-analyzer/dependence-graph9/main.c create mode 100644 regression/goto-analyzer/dependence-graph9/test.desc create mode 100644 src/goto-instrument/unwindset.cpp create mode 100644 src/goto-instrument/unwindset.h rename src/{goto-symex => goto-programs}/adjust_float_expressions.cpp (99%) rename src/{goto-symex => goto-programs}/adjust_float_expressions.h (79%) delete mode 100644 src/goto-programs/basic_blocks.cpp delete mode 100644 src/goto-programs/basic_blocks.h delete mode 100644 src/goto-programs/goto_program_irep.cpp delete mode 100644 src/goto-programs/goto_program_irep.h rename src/{goto-programs/convert_nondet.cpp => java_bytecode/convert_java_nondet.cpp} (96%) rename src/{goto-programs/convert_nondet.h => java_bytecode/convert_java_nondet.h} (91%) create mode 100644 src/java_bytecode/simple_method_stubbing.cpp create mode 100644 src/java_bytecode/simple_method_stubbing.h create mode 100644 src/solvers/flattening/bv_endianness_map.cpp create mode 100644 src/solvers/flattening/bv_endianness_map.h create mode 100644 src/util/container_utils.h create mode 100644 src/util/small_map.h create mode 100644 unit/json/invalid.json create mode 100644 unit/json/json_parser.cpp create mode 100644 unit/json/valid.json delete mode 100644 unit/sharing_map.cpp create mode 100644 unit/util/sharing_map.cpp rename unit/{ => util}/sharing_node.cpp (50%) create mode 100644 unit/util/small_map.cpp diff --git a/.travis.yml b/.travis.yml index 7225e86db563..cc9aaca6bd63 100644 --- a/.travis.yml +++ b/.travis.yml @@ -90,17 +90,6 @@ jobs: - COMPILER="ccache /usr/bin/g++-5" - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG" - # OS X using g++ - - stage: Test different OS/CXX/Flags - os: osx - sudo: false - compiler: gcc - cache: ccache - before_install: - - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel - - export PATH=$PATH:/usr/local/opt/ccache/libexec - env: COMPILER="ccache g++" - # OS X using clang++ - stage: Test different OS/CXX/Flags os: osx diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class new file mode 100644 index 0000000000000000000000000000000000000000..b4af31db09374bd8184688f6e08e34cc2f3de4e9 GIT binary patch literal 768 zcmZuuO>fgc5Pcgv*~E35G;Pz+@{!UOk|5QW-lz~Lz=aTyQWeqL#$GjBT)V98ir^;8^ZoYVzFamV#9U0MAw(XM=~QV+}1GFvIH4I8r@n>KFYHbd?IS~e`q zkd?{ngFiEQq;;sN$7z0!ri~Wb43$aUv%#TsW14EH4;=SchbK}yo#)xfFc)OQc%kB9 zFY$dEPqXz``xnJDp7MmS);Vc0!RsA9W7W zq{yL@(V1_bgPl>3Lz(`C?9xDmV*3Jsc~mJYVqsh?2%Q$MeL(Ijj3;klj!IF<=jAIoiLV!(WrzejNd ZZl1z4-oc#qos#5{v+t+fU7;k0mEU*Npd|nR literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java new file mode 100644 index 000000000000..eb8200154c64 --- /dev/null +++ b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetCharSequence +{ + static void main() + { + CharSequence x = CProver.nondetWithNull(); + assert x == null || x instanceof CharSequence; + } +} diff --git a/regression/cbmc-java/NondetCharSequence/test.desc b/regression/cbmc-java/NondetCharSequence/test.desc new file mode 100644 index 000000000000..baaa60614e55 --- /dev/null +++ b/regression/cbmc-java/NondetCharSequence/test.desc @@ -0,0 +1,8 @@ +CORE +NondetCharSequence.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetString/NondetString.class b/regression/cbmc-java/NondetString/NondetString.class new file mode 100644 index 0000000000000000000000000000000000000000..1e93b74e30fa7e1aa96648f6533e8d0cc879e7e8 GIT binary patch literal 738 zcmZWmOK;Oa5dJoHvWe?9kCqTx9w`(^f`l)as?b$INA=1SmRiC za23}$HW-#SM3P9IsyIp>s6>oI88EP2hSHXbRC<@e>U4J)?0y_bhU!2?ayUI0OTBHH z85)Dw7vYZ3%A8M&cDkn$hNZzUjslsEQmvxN9YQ$}DkA(>W^P{`2`?1U#LMp&N2%~% zJ`sl*4k>3SZ~5V=5@!@owJ#qj!&{$+zHP8vxLD-4?&1b+GSvRXci~`xp>KU9{=_D)g?b)-oO_v*;tYAWq6Wii~2hcMSH1 zk^-vqFJ(mwHOk$S2Gr4@QyI(ou%K=;y#4`&udp7!g*`*F_Z^MiH&`<)d_wWXF-l(y zu$2KXW&E5}l}TGAC*WAc3eHhqGb3R?(dIZ$U9FsMGb01)4gMbG8Myr#w)GD7|GEuG P5e4_2ad&|Z1+4xClS!1v literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetString/NondetString.java b/regression/cbmc-java/NondetString/NondetString.java new file mode 100644 index 000000000000..e2c14ae76f77 --- /dev/null +++ b/regression/cbmc-java/NondetString/NondetString.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetString +{ + static void main() + { + String x = CProver.nondetWithNull(); + assert x == null || x instanceof String; + } +} diff --git a/regression/cbmc-java/NondetString/test.desc b/regression/cbmc-java/NondetString/test.desc new file mode 100644 index 000000000000..6756c4a7630d --- /dev/null +++ b/regression/cbmc-java/NondetString/test.desc @@ -0,0 +1,8 @@ +CORE +NondetString.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class new file mode 100644 index 0000000000000000000000000000000000000000..4a2de67ab40cd612ec068bee8a31477f47cfb8ae GIT binary patch literal 768 zcmZuuO>fgc5Pcgv*~E35G%aap`ADJAB$et*Z&U~fa3KVwR7Lc*vA5|K*RIxf)!&jo zz!{Jz0*Q|c2YwSmjNOtT!ol8|-8b*OnfdYS<7WU{*sxH-iiIn<%5kj(j_Vu^3wf+? ztXjB%n;dHl3u_{Zq>fb>L=ROY2EOzd*d9Y+TLmh<%V0EHy9{P0^dv*Ms{+|ejs{Zi zq+o_>H*|%+E3``Ui%T;;P!Ypow-*MUjQg=x!SF${zc2M2;yMy4AeB>wdiPMA2*($} z(D?^7+mD6&>Zv%+IH?PU;_RouHJmm>t$EWp>aZg4{OKfgc5PcIn-Nbd9G;Pzg{YtOwX3yL@mul- zI0F(zAn|eGz;8l`v0D-Zrf}R2v(!HL$EuMuLz~C4pnb-Fi_@c z3MN##ktc&4X>^*OUfRi?jtR@%UKIK&=_f{q!@DCL_{!X5vID6@mU&57?e5DX*$!kl zZ2t|L>nGBC@kkzKtUL#yueL4MTWIXjir(M*}5W0~vyKpflaK*({TqCUfN6m$U zS*Dpj-}&v!ePbfSPMx73&~VX2i%^~xJ|65VFX4j74BOtJiH?+Mcb;S?VLr?pd8U)S z-Y5tNOO56q7Mv8bMWrcWC*U0ss=kV~QU0Vcb|)F}121S7bzX6iS5M_yItoV?e>^)_ zlcP4D#Am*B40_E$4kiB2WS17o9J?m~ETF_9r<2`a;U_E>TdyH!98!D}@ zu*R7Ei2UsOBj?^ur(5MDhqYfKC8Es$ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java new file mode 100644 index 000000000000..feec3c3ac6b1 --- /dev/null +++ b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetStringBuilder +{ + static void main() + { + StringBuilder x = CProver.nondetWithNull(); + assert x == null || x instanceof StringBuilder; + } +} diff --git a/regression/cbmc-java/NondetStringBuilder/test.desc b/regression/cbmc-java/NondetStringBuilder/test.desc new file mode 100644 index 000000000000..6aa68c42d41d --- /dev/null +++ b/regression/cbmc-java/NondetStringBuilder/test.desc @@ -0,0 +1,8 @@ +CORE +NondetStringBuilder.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc index 5dd14d8dfb94..3cf4998f5aa7 100644 --- a/regression/cbmc-java/NullPointer3/test.desc +++ b/regression/cbmc-java/NullPointer3/test.desc @@ -3,7 +3,7 @@ NullPointer3.class --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^.*Throw null: FAILURE$ +^.*Null pointer check: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/A.class b/regression/cbmc-java/repeated_guards/A.class new file mode 100644 index 0000000000000000000000000000000000000000..6f4617a522e71e12ef98af492c2e224e7817bc21 GIT binary patch literal 251 zcmXYr%}T>i5QV=<^J8PRwNKzuOEDXFickbW2)eLzf0JI@TVeuf>U+5oT=)P!lsGrI zIh>z4GxPKN^$lDzO&Kswm?WGD(W|r7T98K}zICq`riz@t=nrgU)%`kOLJ&T`{4ZeaB275)y}+|5iyD0S_l)bv&z() z?77(4vg4dU9|O$^iF$@Fs6JAa^$A3?Pvk?5fT3cnHq1#CM?H@?R^}I-C-5{1(9 z-?XZeD)}_nEC}8qzZQwyDIIr1Syt1txCtK?8U)%f))>Ix@4AS=8)lo;j9EL4@dI>c XVZh;T*X9IG*8VR57amW9R-N*{5Ah;C literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/repeated_guards/Test.class b/regression/cbmc-java/repeated_guards/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..057d0b980f2f8f3fe796647dcfb395c321161944 GIT binary patch literal 1391 zcmZWo+inwA6kTU7napGoC#JZm10)6l#z4|bdX2fnxu8e}9zaNhhidFO2?N7SHMUdo zDa{Y?Oj{MHsoK6(>PJ;wdpy{bj&v@2pS{=GYo9ZJ|MTnb0M^j*;A72&htC~+;lae3 zgD*YUvVP^kkwY6_JNU-KI+_k{D4e<&^m;n$M`_aAih4mO)}eyhQ?T5P8Usss!bKQ8$M6~*z zfV$l@2_qqA$b){+eSSCiu7D`zDOnaAwbDTn3R?Zi?yjWSfw&cnC%ZJFB-AfiGxz2} z+Aqj9V+z|0dbFKE@;phuCx`PQIO^zcJB(~^uq;2+`=V0EM?+_8oh>U6?hWF2OJ{mt zm>HfIoCC;75wsN@wvP66mWrmlI5Uh673N0OZ)Q3u6b_U10qsL}&ZG>5$!0e$I_*73 z2U%C|MABDRTDS5nI1GH0FzaI)GYa$KSdD|^V0F~a?JP?Pq&7HOK5k->#Ynb;TRv`s z{@HQb{mwJpWmoL|NXNYE()cLvnL;Jhy(rV+h=4cKAMgVB682Ez1M~Ud)a<;J#N8x_ zf?3XUv{tz)u6E-M)N5`GlsQl2PChv9{b2w;z-d}8D)^8dNe&n-$;&^&I7X>@jHwft zkKe%hTDM1l3|+Yg1U6#CO_CDY10DrED?EJK@I0~g%xVQK=q0-6IjNjq5=oT z%#MT0tfG!9h44FE4T4TJeumr3C*d1j)v%jqsN*bqdM@Xx48zeN1Mij$qEXad#kB%- zn=u0FTGhBI<9)~)g`DSex$q98OV1*cEP`GyAXnaj9M|fpi*sTBn literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/repeated_guards/Test.java b/regression/cbmc-java/repeated_guards/Test.java new file mode 100644 index 000000000000..5f177b7e7e9b --- /dev/null +++ b/regression/cbmc-java/repeated_guards/Test.java @@ -0,0 +1,45 @@ +public class Test { + + // In each of these cases a guard is repeated -- either an explicit assertion, + // or a guard implied by Java's semantics, e.g. that an array index is in bounds. + // It should be possible to violate the condition the first time, but not the second, + // as the program would have aborted (without --java-throw-runtime-exceptions) or a + // runtime exception thrown (with --java-throw-runtime-exceptions). + + public static void testAssertion(boolean condition) { + assert(condition); + assert(condition); + } + + public static void testArrayBounds(int[] array, int index) { + if(array == null) + return; + int got = array[index]; + got = array[index]; + } + + public static void testClassCast(boolean unknown) { + A maybe_b = unknown ? new A() : new B(); + B definitely_b = (B)maybe_b; + definitely_b = (B)maybe_b; + } + + public static void testNullDeref(A maybeNull) { + int got = maybeNull.field; + got = maybeNull.field; + } + + public static void testDivByZero(int unknown) { + int div = 1 / unknown; + div = 1 / unknown; + } + + public static void testArrayCreation(int maybeNegative) { + int[] arr = new int[maybeNegative]; + arr = new int[maybeNegative]; + } + +} + +class A { public int field; } +class B extends A {} diff --git a/regression/cbmc-java/repeated_guards/test_arraybounds.desc b/regression/cbmc-java/repeated_guards/test_arraybounds.desc new file mode 100644 index 000000000000..fd0383545a45 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_arraybounds.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.testArrayBounds +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +array-index-out-of-bounds-low\.1.*: FAILURE$ +array-index-out-of-bounds-low\.2.*: SUCCESS$ +array-index-out-of-bounds-high\.1.*: FAILURE$ +array-index-out-of-bounds-high\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_arraycreation.desc b/regression/cbmc-java/repeated_guards/test_arraycreation.desc new file mode 100644 index 000000000000..f737239e0cd9 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_arraycreation.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testArrayCreation +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +array-create-negative-size\.1.*: FAILURE$ +array-create-negative-size\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_assertion.desc b/regression/cbmc-java/repeated_guards/test_assertion.desc new file mode 100644 index 000000000000..182191d772f0 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_assertion.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testAssertion +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Test\.java line 10.*: FAILURE$ +assertion at file Test\.java line 11.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_classcast.desc b/regression/cbmc-java/repeated_guards/test_classcast.desc new file mode 100644 index 000000000000..c06857eb9249 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_classcast.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testClassCast +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +bad-dynamic-cast\.1.*: FAILURE$ +bad-dynamic-cast\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_divbyzero.desc b/regression/cbmc-java/repeated_guards/test_divbyzero.desc new file mode 100644 index 000000000000..4d9f15cd63d1 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_divbyzero.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testDivByZero +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +integer-divide-by-zero\.1.*: FAILURE$ +integer-divide-by-zero\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_nullderef.desc b/regression/cbmc-java/repeated_guards/test_nullderef.desc new file mode 100644 index 000000000000..082ef0af6a89 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_nullderef.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testNullDeref +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +testNullDeref:\(LA;\)V\.null-pointer-exception\.1.*: FAILURE$ +testNullDeref:\(LA;\)V\.null-pointer-exception\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc/reachability-slice-interproc/test.c b/regression/cbmc/reachability-slice-interproc/test.c new file mode 100644 index 000000000000..f149e6f09769 --- /dev/null +++ b/regression/cbmc/reachability-slice-interproc/test.c @@ -0,0 +1,76 @@ +#include + +// After a reachability slice based on the assertion in `target`, we should +// retain both its possible callers (...may_call_target_1, ...may_call_target_2) +// and their callees, but should be more precise concerning before_target and +// after_target, which even though they are also called by +// `unreachable_calls_before_target` and `unreachable_calls_after_target`, those +// functions are not reachable. + +void before_target() +{ + const char *local = "before_target_kept"; +} + +void after_target() +{ + const char *local = "after_target_kept"; +} + +void target() +{ + const char *local = "target_kept"; + + before_target(); + assert(0); + after_target(); +} + +void unreachable_calls_before_target() +{ + const char *local = "unreachable_calls_before_target_kept"; + before_target(); +} + +void unreachable_calls_after_target() +{ + const char *local = "unreachable_calls_after_target_kept"; + after_target(); +} + +void reachable_before_target_caller_1() +{ + const char *local = "reachable_before_target_caller_1_kept"; +} + +void reachable_after_target_caller_1() +{ + const char *local = "reachable_after_target_caller_1_kept"; +} + +void reachable_may_call_target_1() +{ + const char *local = "reachable_may_call_target_1_kept"; + reachable_before_target_caller_1(); + target(); + reachable_after_target_caller_1(); +} + +void reachable_before_target_caller_2() +{ + const char *local = "reachable_before_target_caller_2_kept"; +} + +void reachable_after_target_caller_2() +{ + const char *local = "reachable_after_target_caller_2_kept"; +} + +void reachable_may_call_target_2() +{ + const char *local = "reachable_may_call_target_2_kept"; + reachable_before_target_caller_2(); + target(); + reachable_after_target_caller_2(); +} + diff --git a/regression/cbmc/reachability-slice-interproc/test.desc b/regression/cbmc/reachability-slice-interproc/test.desc new file mode 100644 index 000000000000..d4d422fa6ba5 --- /dev/null +++ b/regression/cbmc/reachability-slice-interproc/test.desc @@ -0,0 +1,13 @@ +CORE +test.c +--reachability-slice-fb --show-goto-functions +target_kept +reachable_before_target_caller_1_kept +reachable_after_target_caller_1_kept +reachable_may_call_target_1_kept +reachable_before_target_caller_2_kept +reachable_after_target_caller_2_kept +reachable_may_call_target_2_kept +-- +unreachable_calls_before_target_kept +unreachable_calls_after_target_kept diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c new file mode 100644 index 000000000000..06ef87fbc729 --- /dev/null +++ b/regression/cbmc/ts18661_typedefs/main.c @@ -0,0 +1,9 @@ +typedef float _Float32; +typedef double _Float32x; +typedef double _Float64; +typedef long double _Float64x; +typedef long double _Float128; +typedef long double _Float128x; + +int main(int argc, char** argv) { +} diff --git a/regression/cbmc/ts18661_typedefs/test.desc b/regression/cbmc/ts18661_typedefs/test.desc new file mode 100644 index 000000000000..9efefbc7362d --- /dev/null +++ b/regression/cbmc/ts18661_typedefs/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index 1e35e023c982..cd46dae86ce8 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index 1ff684bf0a6a..0c12978ae7c0 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -10,10 +10,10 @@ replacing function pointer by 3 possible targets ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index 1e35e023c982..cd46dae86ce8 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 1e35e023c982..cd46dae86ce8 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index 1e35e023c982..cd46dae86ce8 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index c4ac12fc4cdb..18950ead3885 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index e84fdb08b4fb..7db491e7874a 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 527325b84bbc..25fbc2808767 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 4e9c87154295..c3eb2ca93e9b 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0$ +^Simplified: assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 2d2e078a4246..44ebe6f09e6a 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index fc3be9106704..cf993822161b 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -3,7 +3,7 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$ -^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: Success$ +^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index aba11ba0c06b..d3c619d08efc 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/main.c b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c new file mode 100644 index 000000000000..f80f5f042d48 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c @@ -0,0 +1,9 @@ +#include + +#define ROUND_F(x) ((int)((x) + 0.5f)) +int eight = ROUND_F(100.0f / 12.0f); + +int main() +{ + assert(eight == 8); +} diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc new file mode 100644 index 000000000000..2fc631c19334 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c new file mode 100644 index 000000000000..6b1e90e3427a --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c @@ -0,0 +1,27 @@ +#include +#include +#include + +int nondet_rounding_mode(void); + +int main(void) +{ + // slightly bigger than 0.1 + float f = 1.0f / 10.0f; + + // now we don't know what rounding mode we're in + __CPROVER_rounding_mode = nondet_rounding_mode(); + // depending on rounding mode 1.0f/10.0f could + // be greater or smaller than 0.1 + + // definitely not smaller than -0.1 + assert((1.0f / 10.0f) - f < -0.1f); + // might be smaller than 0 + assert((1.0f / 10.0f) - f < 0.0f); + // definitely smaller or equal to 0 + assert((1.0f / 10.0f) - f <= 0.0f); + // might be greater or equal to 0 + assert((1.0f / 10.0f) - f >= 0.0f); + // definitely not greater than 0 + assert((1.0f / 10.0f) - f > 0.0f); +} diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc new file mode 100644 index 000000000000..12b4b6443a25 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: Failure \(if reachable\) +\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: Unknown +\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: Success +\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: Unknown +\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: Failure \(if reachable\) + +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_rounding_mode/main.c new file mode 100644 index 000000000000..ace3fe60eb5e --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_rounding_mode/main.c @@ -0,0 +1,12 @@ +#include + +int main(void) +{ + __CPROVER_rounding_mode = 0; + float rounded_up = 1.0f / 10.0f; + __CPROVER_rounding_mode = 1; + float rounded_down = 1.0f / 10.0f; + assert(rounded_up - 0.1f >= 0); + assert(rounded_down - 0.1f < 0); + return 0; +} diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc new file mode 100644 index 000000000000..c7c1e94639c2 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success +^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success +-- +^warning: ignoring diff --git a/regression/goto-analyzer/dependence-graph10/main.c b/regression/goto-analyzer/dependence-graph10/main.c new file mode 100644 index 000000000000..8cdfb5e41584 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph10/main.c @@ -0,0 +1,15 @@ +int a; + +void main(void) +{ + int i = 0; + + if(i < 10) + { + a = 1; + } + else + { + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph10/test.desc b/regression/goto-analyzer/dependence-graph10/test.desc new file mode 100644 index 000000000000..e0d118d2ac3d --- /dev/null +++ b/regression/goto-analyzer/dependence-graph10/test.desc @@ -0,0 +1,39 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// First assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// Second assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 + +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + a = 1; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the assignment has a +control dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 +... +**** 5 file main.c line 13 function main +Control dependencies: + + // 5 file main.c line 13 function main + 1: a = 2; + diff --git a/regression/goto-analyzer/dependence-graph11/main.c b/regression/goto-analyzer/dependence-graph11/main.c new file mode 100644 index 000000000000..c3ab582f6763 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph11/main.c @@ -0,0 +1,15 @@ +int a; + +void func() +{ +} + +void main(void) +{ + func(); + + if(a < 10) + { + a = 1; + } +} diff --git a/regression/goto-analyzer/dependence-graph11/test.desc b/regression/goto-analyzer/dependence-graph11/test.desc new file mode 100644 index 000000000000..d8112318ed44 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph11/test.desc @@ -0,0 +1,23 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +-- +^warning: ignoring +-- +The regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 +... +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + a = 1; diff --git a/regression/goto-analyzer/dependence-graph12/main.c b/regression/goto-analyzer/dependence-graph12/main.c new file mode 100644 index 000000000000..0257cb1f1c53 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph12/main.c @@ -0,0 +1,21 @@ +int a; + +void func() +{ +} + +void main(void) +{ + if(a < 7) + { + goto L; + } + + if(a < 10) + { + func(); + L: + a = 1; + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph12/test.desc b/regression/goto-analyzer/dependence-graph12/test.desc new file mode 100644 index 000000000000..b14ba9f7ba66 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph12/test.desc @@ -0,0 +1,38 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the first if +\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +// Assignment has a control dependency on the second if +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 9 function main + IF a < 7 THEN GOTO 1 +... +**** 6 file main.c line 19 function main +Control dependencies: (,...)|(...,) + + // 6 file main.c line 19 function main + a = 2; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the assignment has a +control dependency on the goto statement. + + // file main.c line 14 function main + IF !(a < 10) THEN GOTO 2 +... +**** 6 file main.c line 19 function main +Control dependencies: (,...)|(...,) + + // 6 file main.c line 19 function main + a = 2; diff --git a/regression/goto-analyzer/dependence-graph4/main.c b/regression/goto-analyzer/dependence-graph4/main.c new file mode 100644 index 000000000000..cad28241847b --- /dev/null +++ b/regression/goto-analyzer/dependence-graph4/main.c @@ -0,0 +1,16 @@ +int g_in1, g_in2; +int g_out; + +void main(void) +{ + int t; + if(g_in1) + { + if(g_in2) + t = 0; + else + t = 1; + + g_out = 1; // depends on "if(g_in1) + } +} diff --git a/regression/goto-analyzer/dependence-graph4/test.desc b/regression/goto-analyzer/dependence-graph4/test.desc new file mode 100644 index 000000000000..ba3ca2eb1f5a --- /dev/null +++ b/regression/goto-analyzer/dependence-graph4/test.desc @@ -0,0 +1,22 @@ +CORE +main.c +--show --dependence-graph --text - +activate-multi-line-match +EXIT=0 +SIGNAL=0 +\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1 +-- +^warning: ignoring +-- +The regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(g_in1 != 0) THEN GOTO 3 +... +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + g_out = 1; diff --git a/regression/goto-analyzer/dependence-graph7/main.c b/regression/goto-analyzer/dependence-graph7/main.c new file mode 100644 index 000000000000..e0ab2d5b1a4c --- /dev/null +++ b/regression/goto-analyzer/dependence-graph7/main.c @@ -0,0 +1,10 @@ +int a; + +void main(void) +{ + int i = 0; + while(i < 10) + { + a = 1; + } +} diff --git a/regression/goto-analyzer/dependence-graph7/test.desc b/regression/goto-analyzer/dependence-graph7/test.desc new file mode 100644 index 000000000000..62067ef188a6 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph7/test.desc @@ -0,0 +1,50 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// Backedge has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}\s*GOTO [0-9]+ +// Loop head has a control dependency on itself +Control dependencies: ([0-9]+)\n(.*\n)?\n.*\/\/ \1.*\n.*IF.*i < 10.*THEN +-- +^warning: ignoring +-- +The first regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 +... +**** 3 file main.c line 8 function main +Control dependencies: + + // 3 file main.c line 8 function main + a = 1; + +The second regex above match output portions like shown below (with being a +location number). The intention is to check whether the backwards goto has a +control dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 +... +**** 4 file main.c line 6 function main +Control dependencies: + + // 4 file main.c line 6 function main + GOTO 1 + +The third regex above match output portions like shown below (with being a +location number). The intention is to check whether the loop head has a control +dependency on itself. + +Control dependencies: +Data dependencies: 1 + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 diff --git a/regression/goto-analyzer/dependence-graph8/main.c b/regression/goto-analyzer/dependence-graph8/main.c new file mode 100644 index 000000000000..ca7bf52632fc --- /dev/null +++ b/regression/goto-analyzer/dependence-graph8/main.c @@ -0,0 +1,13 @@ +int a; + +void main(void) +{ + int i = 0; + while(i < 10) + { + if(i < 7) + { + a = 1; + } + } +} diff --git a/regression/goto-analyzer/dependence-graph8/test.desc b/regression/goto-analyzer/dependence-graph8/test.desc new file mode 100644 index 000000000000..50549bb686f3 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph8/test.desc @@ -0,0 +1,54 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// If has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*i < 7 +-- +^warning: ignoring +// Assignment does not have a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the if. + + // file main.c line 6 function main + 1: IF !(i < 7) THEN GOTO 2 +... +**** 3 file main.c line 8 function main +Control dependencies: + + // 3 file main.c line 8 function main + a = 1; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the if has a control +dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 3 + +**** 3 file main.c line 8 function main +Control dependencies: +Data dependencies: 1 + + // 3 file main.c line 8 function main + IF !(i < 7) THEN GOTO 2 + +The third regex above matches output portions like shown below (with being a +location number). The intention is to check that the assignment does not have a +control dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 3 +... +**** 4 file main.c line 10 function main +Control dependencies: + + // 4 file main.c line 10 function main + a = 1; diff --git a/regression/goto-analyzer/dependence-graph9/main.c b/regression/goto-analyzer/dependence-graph9/main.c new file mode 100644 index 000000000000..d968c9f55e1c --- /dev/null +++ b/regression/goto-analyzer/dependence-graph9/main.c @@ -0,0 +1,16 @@ +int a; + +void main(void) +{ + int i = 0; + + if(i < 10) + { + if(i < 7) + { + a = 1; + } + + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph9/test.desc b/regression/goto-analyzer/dependence-graph9/test.desc new file mode 100644 index 000000000000..2bcae4642df5 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph9/test.desc @@ -0,0 +1,38 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Second assignment has a control dependency on the outer if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +// Second assignment does not have a control dependency on the inner if +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the outer if. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 2 +... +**** 6 file main.c line 14 function main +Control dependencies: + + // 6 file main.c line 14 function main + a = 2; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check that the assignment does not have +a control dependency on the inner if. + + // file main.c line 9 function main + IF !(i < 7) THEN GOTO 1 +... +**** 6 file main.c line 14 function main +Control dependencies: + + // 6 file main.c line 14 function main + a = 2; diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc index fa4f926287fb..b81b93bd2a03 100644 --- a/regression/goto-analyzer/intervals_02/test.desc +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: Success$ +^\[main.assertion.1\] file main.c line 5 function main, assertion x > -10 \&\& x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc index 79042c334dea..d9e5e2907233 100644 --- a/regression/goto-analyzer/intervals_03/test.desc +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: Success$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x > -10 \|\| x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc index 5bb03255f373..e28af3a18924 100644 --- a/regression/goto-analyzer/intervals_04/test.desc +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 && i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc index 5c9af29a2b17..d059546aab8b 100644 --- a/regression/goto-analyzer/intervals_05/test.desc +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \|\| i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc index 2dc8d29a3b66..d5836b3fde90 100644 --- a/regression/goto-analyzer/intervals_06/test.desc +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \|\| x > 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc index aa3962f39de7..d5fbbb70b93b 100644 --- a/regression/goto-analyzer/intervals_07/test.desc +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 && x > 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \&\& x > 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc index 7b83ecd0f21f..c8fff24bba7f 100644 --- a/regression/goto-analyzer/intervals_08/test.desc +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 && x < 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 \&\& x < 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc index 83776b8ae348..31f685aa72f9 100644 --- a/regression/goto-analyzer/intervals_09/test.desc +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \&\& i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc index 468ce13a5501..a359da82f4fe 100644 --- a/regression/goto-analyzer/intervals_10/test.desc +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$ ^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$ -^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure (if reachable)$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure \(if reachable\)$ ^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure (if reachable)$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc index 799ad36f64ff..05d8d74bd0d2 100644 --- a/regression/goto-analyzer/intervals_11/test.desc +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -3,7 +3,7 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ -^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$ +^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-instrument/unwind-unwindset3/test.desc b/regression/goto-instrument/unwind-unwindset3/test.desc index 01df8603ae6d..58a253c1062b 100644 --- a/regression/goto-instrument/unwind-unwindset3/test.desc +++ b/regression/goto-instrument/unwind-unwindset3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 10 --unwindset main.0:-1 +--unwind 10 --unwindset main.0: ^Unwinding loop ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/jbmc-strings/long_string/Test.class b/regression/jbmc-strings/long_string/Test.class index 9442a3c1cf466c5158a588f53da0901a688f5f87..aa76e7deca38c6e0ff8b9a66c641fa186584a088 100644 GIT binary patch delta 556 zcmZXR&rcIk5XV1nU)$H+ZfRJn7DOnt2;JHiv=o0NhJdF62P^Tu5E6+*jnp$9JbG#N zZbIZA=mjDN!wC{SdGs&wVhFQ~>4nS8cjnD}=R5QMm;<~0^Wx+O(Bg^15M_r6rXzDt zQ#(7=n1iCj46~Z?&!22uDhA)drmPdvXQ(>dr)H@4+Rsbg+Pke__f_y=C)nKG-iVAM z(S5zMr%0`BZ0~iS_P#WeNxT^j>Yas0+Bk3Qb`T{KSVpDNab5pQ;RlqH7OJq}EL^3x7e-GbU zt4fC_*1~>NSwxFnVw5}LBQz#Rkz<~_f-J@*n2#Cu+;?+ny;2I^O?t1pQ9yr@qLt@r;NP4VGZJ(G{NOk%l9(QT(B Huqa&uIPFR2 delta 359 zcmX|+PfG$(6vcltqdpyHl1kGwP4iDVYJYTU89}WKSG8#s7OiU0qII-r9mx9x(kGC> zphX0MLEoSc(Yj4UR~Pc&ymRk8=N@i9@}=6Je=o0qk8d+W)+WdD81fd4(VKVg(%4DJ@8D5$ zsMAoaJ8ZD2PmOA5%b`h2KNvstEQUM?de0aGAqH{5(4=WeW`YIb^U~A$-8?i*9kaG~ zlTy2c!u%3bq@qz*q>EGOEhd&od~bxReGnLUwIODwKE#@fKI(6?uy0O+D&m7QVKTyU q#3+)YB)iIj6~QVkxndmX5S#|O;z;Y0fFB=Ef|$hbgCQJW$F)t$k diff --git a/regression/jbmc-strings/long_string/Test.java b/regression/jbmc-strings/long_string/Test.java index 5decee619317..370dea0e1833 100644 --- a/regression/jbmc-strings/long_string/Test.java +++ b/regression/jbmc-strings/long_string/Test.java @@ -32,7 +32,12 @@ public static void checkAbort(String s, String t) { // Filter out // 67_108_864 corresponds to the maximum length for which the solver // will concretize the string. - if(u.length() <= 67_108_864) + if(s.length() <= 67_108_864 && t.length() <= 67_108_864) + return; + // Check at least one of them is short-ish, so we don't end up trying + // to concretise a very long but *just* allowable string and memout the + // test infrastructure: + if(s.length() > 1024 && t.length() > 1024) return; if(CProverString.charAt(u, 2_000_000) != 'b') return; diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc index dcb245dbf5e5..9da2a9e9eb21 100644 --- a/regression/strings/test_index_of/test.desc +++ b/regression/strings/test_index_of/test.desc @@ -5,5 +5,5 @@ test.c ^SIGNAL=0$ ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$ ^\[main.assertion.2\] assertion lastSlash == 7: SUCCESS$ -^\[main.assertion.3\] assertion firstSlash != 3 || lastSlash != 7: FAILURE$ +^\[main.assertion.3\] assertion firstSlash != 3 \|\| lastSlash != 7: FAILURE$ -- diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc index 0638394661ce..f89a9bf19072 100644 --- a/regression/strings/test_int/test.desc +++ b/regression/strings/test_int/test.desc @@ -6,5 +6,5 @@ test.c ^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$ ^\[main.assertion.2\] assertion __CPROVER_char_at\(s,1\) == .2.: SUCCESS$ ^\[main.assertion.3\] assertion j == 234: SUCCESS$ -^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at\(s,2\) == .4.: FAILURE$ +^\[main.assertion.4\] assertion j < 233 \|\| __CPROVER_char_at\(s,2\) == .4.: FAILURE$ -- diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 84b5b91d2cb3..881348279f2d 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -74,7 +74,8 @@ static void forall_callsites( call_grapht::call_grapht( const goto_functionst &goto_functions, const irep_idt &root, - bool collect_callsites) + bool collect_callsites): + collect_callsites(collect_callsites) { std::stack> pending_stack; pending_stack.push(root); diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index bbf20546b681..452e8355a931 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -16,6 +16,7 @@ Author: Peter Schrammel #include #endif +#include #include #include #include @@ -23,6 +24,9 @@ Author: Peter Schrammel #include +#include +#include + void constant_propagator_domaint::assign_rec( valuest &values, const exprt &lhs, @@ -35,8 +39,7 @@ void constant_propagator_domaint::assign_rec( const symbol_exprt &s=to_symbol_expr(lhs); exprt tmp=rhs; - values.replace_const(tmp); - simplify(tmp, ns); + partial_evaluate(tmp, ns); if(tmp.is_constant()) values.set_to(s, tmp); @@ -99,10 +102,10 @@ void constant_propagator_domaint::transform( // Comparing iterators is safe as the target must be within the same list // of instructions because this is a GOTO. if(from->get_target()==to) - g=simplify_expr(from->guard, ns); + g = from->guard; else - g=simplify_expr(not_exprt(from->guard), ns); - + g = not_exprt(from->guard); + partial_evaluate(g, ns); if(g.is_false()) values.set_to_bottom(); else @@ -269,10 +272,7 @@ bool constant_propagator_domaint::ai_simplify( exprt &condition, const namespacet &ns) const { - bool b=values.replace_const.replace(condition); - b&=simplify(condition, ns); - - return b; + return partial_evaluate(condition, ns); } @@ -504,6 +504,74 @@ bool constant_propagator_domaint::merge( return values.merge(other.values); } +/// Attempt to evaluate expression using domain knowledge +/// This function changes the expression that is passed into it. +/// \param expr The expression to evaluate +/// \param ns The namespace for symbols in the expression +/// \return True if the expression is unchanged, false otherwise +bool constant_propagator_domaint::partial_evaluate( + exprt &expr, + const namespacet &ns) const +{ + // if the current rounding mode is top we can + // still get a non-top result by trying all rounding + // modes and checking if the results are all the same + if(!values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str))) + { + return partial_evaluate_with_all_rounding_modes(expr, ns); + } + return replace_constants_and_simplify(expr, ns); +} + +/// Attempt to evaluate an expression in all rounding modes. +/// +/// If the result is the same for all rounding modes, change +/// expr to that result and return false. Otherwise, return true. +bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( + exprt &expr, + const namespacet &ns) const +{ // NOLINTNEXTLINE (whitespace/braces) + auto rounding_modes = std::array{ + // NOLINTNEXTLINE (whitespace/braces) + {ieee_floatt::ROUND_TO_EVEN, + ieee_floatt::ROUND_TO_ZERO, + ieee_floatt::ROUND_TO_MINUS_INF, + // NOLINTNEXTLINE (whitespace/braces) + ieee_floatt::ROUND_TO_PLUS_INF}}; + exprt first_result; + for(std::size_t i = 0; i < rounding_modes.size(); ++i) + { + constant_propagator_domaint child(*this); + child.values.set_to( + ID_cprover_rounding_mode_str, + from_integer(rounding_modes[i], integer_typet())); + exprt result = expr; + if(child.replace_constants_and_simplify(result, ns)) + { + return true; + } + else if(i == 0) + { + first_result = result; + } + else if(result != first_result) + { + return true; + } + } + expr = first_result; + return false; +} + +bool constant_propagator_domaint::replace_constants_and_simplify( + exprt &expr, + const namespacet &ns) const +{ + bool did_not_change_anything = values.replace_const.replace(expr); + did_not_change_anything &= simplify(expr, ns); + return did_not_change_anything; +} + void constant_propagator_ait::replace( goto_functionst &goto_functions, const namespacet &ns) @@ -529,38 +597,34 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - s_it->second.values.replace_const(it->guard); - simplify(it->guard, ns); + s_it->second.partial_evaluate(it->guard, ns); } else if(it->is_assign()) { exprt &rhs=to_code_assign(it->code).rhs(); - s_it->second.values.replace_const(rhs); - simplify(rhs, ns); + s_it->second.partial_evaluate(rhs, ns); if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { - s_it->second.values.replace_const( - to_code_function_call(it->code).function()); - - simplify(to_code_function_call(it->code).function(), ns); + exprt &function = to_code_function_call(it->code).function(); + s_it->second.partial_evaluate(function, ns); exprt::operandst &args= to_code_function_call(it->code).arguments(); - for(exprt::operandst::iterator o_it=args.begin(); - o_it!=args.end(); ++o_it) + for(auto &arg : args) { - s_it->second.values.replace_const(*o_it); - simplify(*o_it, ns); + s_it->second.partial_evaluate(arg, ns); } } else if(it->is_other()) { if(it->code.get_statement()==ID_expression) - s_it->second.values.replace_const(it->code); + { + s_it->second.partial_evaluate(it->code, ns); + } } } } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0fc4796e8b7c..e32a14bc0f24 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -138,6 +138,8 @@ class constant_propagator_domaint:public ai_domain_baset valuest values; + bool partial_evaluate(exprt &expr, const namespacet &ns) const; + protected: void assign_rec( valuest &values, @@ -147,6 +149,12 @@ class constant_propagator_domaint:public ai_domain_baset bool two_way_propagate_rec( const exprt &expr, const namespacet &ns); + + bool partial_evaluate_with_all_rounding_modes( + exprt &expr, + const namespacet &ns) const; + + bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const; }; class constant_propagator_ait:public ait diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index dd9a770d8372..95ae2de10aef 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -16,6 +16,7 @@ Date: August 2013 #include +#include #include #include @@ -26,36 +27,27 @@ bool dep_graph_domaint::merge( goto_programt::const_targett from, goto_programt::const_targett to) { - bool changed=has_values.is_false(); - has_values=tvt::unknown(); - - depst::iterator it=control_deps.begin(); - for(const auto &c_dep : src.control_deps) + // An abstract state at location `to` may be non-bottom even if + // `merge(..., `to`) has not been called so far. This is due to the special + // handling of function entry edges (see transform()). + bool changed = is_bottom() || has_changed; + + // For computing the data dependencies, we would not need a fixpoint + // computation. The data dependencies at a location are computed from the + // result of the reaching definitions analysis at that location + // (in data_dependencies()). Thus, we only need to set the data dependencies + // part of an abstract state at a certain location once. + if(changed && data_deps.empty()) { - while(it!=control_deps.end() && *itis_goto() || - from->is_assume()) - control_deps.insert(from); + // When computing the control dependencies of a node N (i.e., "to" + // being N), candidates for M are all control statements (gotos or + // assumes) from which there is a path in the CFG to N. + + // Add new candidates + + if(from->is_goto() || from->is_assume()) + control_dep_candidates.insert(from); + else if(from->is_end_function()) + { + control_dep_candidates.clear(); + return; + } + + if(control_dep_candidates.empty()) + return; + + // Get postdominators const irep_idt id=from->function; const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id); - // check all candidates for M - for(depst::iterator - it=control_deps.begin(); - it!=control_deps.end(); - ) // no ++it - { - depst::iterator next=it; - ++next; + // Check all candidates - // check all CFG successors + for(const auto &control_dep_candidate : control_dep_candidates) + { + // check all CFG successors of M // special case: assumptions also introduce a control dependency - bool post_dom_all=!(*it)->is_assume(); + bool post_dom_all = !control_dep_candidate->is_assume(); bool post_dom_one=false; // we could hard-code assume and goto handling here to improve // performance - cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e= - pd.cfg.entry_map.find(*it); + cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e = + pd.cfg.entry_map.find(control_dep_candidate); - assert(e!=pd.cfg.entry_map.end()); + INVARIANT( + e != pd.cfg.entry_map.end(), "cfg must have an entry for every location"); const cfg_post_dominatorst::cfgt::nodet &m= pd.cfg[e->second]; + // successors of M for(const auto &edge : m.out) { const cfg_post_dominatorst::cfgt::nodet &m_s= @@ -114,11 +118,14 @@ void dep_graph_domaint::control_dependencies( post_dom_all=false; } - if(post_dom_all || - !post_dom_one) - control_deps.erase(it); - - it=next; + if(post_dom_all || !post_dom_one) + { + control_deps.erase(control_dep_candidate); + } + else + { + control_deps.insert(control_dep_candidate); + } } } @@ -208,18 +215,18 @@ void dep_graph_domaint::transform( dynamic_cast(&(dep_graph->get_state(next))); assert(s!=nullptr); - depst::iterator it=s->control_deps.begin(); - for(const auto &c_dep : control_deps) + if(s->is_bottom()) { - while(it!=s->control_deps.end() && *itcontrol_deps.end() || c_dep<*it) - s->control_deps.insert(it, c_dep); - else if(it!=s->control_deps.end()) - ++it; + s->has_values = tvt::unknown(); + s->has_changed = true; } + s->has_changed |= util_inplace_set_union(s->control_deps, control_deps); + s->has_changed |= util_inplace_set_union( + s->control_dep_candidates, control_dep_candidates); + control_deps.clear(); + control_dep_candidates.clear(); } } else diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 30b971087766..de7ee8c5a208 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -68,9 +68,10 @@ class dep_graph_domaint:public ai_domain_baset public: typedef grapht::node_indext node_indext; - dep_graph_domaint(): - has_values(false), - node_id(std::numeric_limits::max()) + dep_graph_domaint() + : has_values(false), + node_id(std::numeric_limits::max()), + has_changed(false) { } @@ -101,6 +102,7 @@ class dep_graph_domaint:public ai_domain_baset has_values=tvt(true); control_deps.clear(); + control_dep_candidates.clear(); data_deps.clear(); } @@ -111,12 +113,24 @@ class dep_graph_domaint:public ai_domain_baset has_values=tvt(false); control_deps.clear(); + control_dep_candidates.clear(); data_deps.clear(); + + has_changed = false; } void make_entry() final override { - make_top(); + DATA_INVARIANT( + node_id != std::numeric_limits::max(), + "node_id must not be valid"); + + has_values = tvt::unknown(); + control_deps.clear(); + control_dep_candidates.clear(); + data_deps.clear(); + + has_changed = false; } bool is_top() const final override @@ -124,9 +138,11 @@ class dep_graph_domaint:public ai_domain_baset DATA_INVARIANT(node_id!=std::numeric_limits::max(), "node_id must be valid"); - DATA_INVARIANT(!has_values.is_true() || - (control_deps.empty() && data_deps.empty()), - "If the domain is top, it must have no dependencies"); + DATA_INVARIANT( + !has_values.is_true() || + (control_deps.empty() && control_dep_candidates.empty() && + data_deps.empty()), + "If the domain is top, it must have no dependencies"); return has_values.is_true(); } @@ -136,9 +152,11 @@ class dep_graph_domaint:public ai_domain_baset DATA_INVARIANT(node_id!=std::numeric_limits::max(), "node_id must be valid"); - DATA_INVARIANT(!has_values.is_false() || - (control_deps.empty() && data_deps.empty()), - "If the domain is bottom, it must have no dependencies"); + DATA_INVARIANT( + !has_values.is_false() || + (control_deps.empty() && control_dep_candidates.empty() && + data_deps.empty()), + "If the domain is bottom, it must have no dependencies"); return has_values.is_false(); } @@ -160,9 +178,22 @@ class dep_graph_domaint:public ai_domain_baset private: tvt has_values; node_indext node_id; + bool has_changed; typedef std::set depst; - depst control_deps, data_deps; + + // Set of locations with control instructions on which the instruction at this + // location has a control dependency on + depst control_deps; + + // Set of locations with control instructions from which there is a path in + // the CFG to the current location (with the locations being in the same + // function). The set control_deps is a subset of this set. + depst control_dep_candidates; + + // Set of locations with instructions on which the instruction at this + // location has a data dependency on + depst data_deps; friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &); diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 0ac703eebeef..aa541a9d6e88 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -344,9 +344,22 @@ void ansi_c_convert_typet::write(typet &type) gcc_float64_cnt+gcc_float64x_cnt+ gcc_float128_cnt+gcc_float128x_cnt>=2) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; - throw 0; + // Temporary workaround for our glibc versions that try to define TS 18661 + // types (for example, typedef float _Float32). This can be removed once + // upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us + // to provide these types natively), or disable parsing them ourselves + // when our preprocessor stage claims support <7.0. + if(c_storage_spec.is_typedef) + { + warning().source_location = source_location; + warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom; + } + else + { + error().source_location=source_location; + error() << "conflicting type modifiers" << eom; + throw 0; + } } // _not_ the same as float, double, long double diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b3d7389f9955..7c3e914ddfa9 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1469,7 +1469,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr) exprt &op0=expr.op0(); typet type=op0.type(); - follow_symbol(type); + type = follow(type); if(type.id()==ID_incomplete_struct) { diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 9da2d96efc2e..e1045b7bc9c6 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -30,9 +30,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ ../goto-instrument/cover_basic_blocks$(OBJEXT) \ ../goto-instrument/cover_filter$(OBJEXT) \ @@ -43,6 +40,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../goto-instrument/cover_instrument_other$(OBJEXT) \ ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-instrument/reachability_slicer$(OBJEXT) \ + ../goto-instrument/nondet_static$(OBJEXT) \ + ../goto-instrument/full_slicer$(OBJEXT) \ + ../goto-instrument/unwindset$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 421b8111edc8..d23889242fd7 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -214,8 +214,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) for(const auto &g : goal_map) { json_stream_objectt &result = result_array.push_back_stream_object(); - result["property"]=json_stringt(id2string(g.first)); - result["description"]=json_stringt(id2string(g.second.description)); + result["property"] = json_stringt(g.first); + result["description"] = json_stringt(g.second.description); result["status"]=json_stringt(g.second.status_string()); if(g.second.status==goalt::statust::FAILURE) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ea7b3e17f308..3fb3e9dcc430 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include @@ -74,10 +72,10 @@ void bmct::error_trace() json_stream_objectt &json_result = status().json_stream().push_back_stream_object(); const goto_trace_stept &step=goto_trace.steps.back(); - json_result["property"]= - json_stringt(id2string(step.pc->source_location.get_property_id())); - json_result["description"]= - json_stringt(id2string(step.pc->source_location.get_comment())); + json_result["property"] = + json_stringt(step.pc->source_location.get_property_id()); + json_result["description"] = + json_stringt(step.pc->source_location.get_comment()); json_result["status"]=json_stringt("failed"); json_stream_arrayt &json_trace = json_result.push_back_stream_array("trace"); @@ -319,7 +317,8 @@ void bmct::setup() symex.last_source_location.make_nil(); - setup_unwind(); + symex.unwindset.parse_unwind(options.get_option("unwind")); + symex.unwindset.parse_unwindset(options.get_option("unwindset")); } safety_checkert::resultt bmct::execute( @@ -549,43 +548,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv) } } -void bmct::setup_unwind() -{ - const std::string &set=options.get_option("unwindset"); - std::vector unwindset_loops; - split_string(set, ',', unwindset_loops, true, true); - - for(auto &val : unwindset_loops) - { - unsigned thread_nr=0; - bool thread_nr_set=false; - - if(!val.empty() && - isdigit(val[0]) && - val.find(":")!=std::string::npos) - { - std::string nr=val.substr(0, val.find(":")); - thread_nr=unsafe_string2unsigned(nr); - thread_nr_set=true; - val.erase(0, nr.size()+1); - } - - if(val.rfind(":")!=std::string::npos) - { - std::string id=val.substr(0, val.rfind(":")); - long uw=unsafe_string2int(val.substr(val.rfind(":")+1)); - - if(thread_nr_set) - symex.set_unwind_thread_loop_limit(thread_nr, id, uw); - else - symex.set_unwind_loop_limit(id, uw); - } - } - - if(options.get_option("unwind")!="") - symex.set_unwind_limit(options.get_unsigned_int_option("unwind")); -} - /// Perform core BMC, using an abstract model to supply GOTO function bodies /// (perhaps created on demand). /// \param opts: command-line options affecting BMC @@ -693,10 +655,10 @@ int bmct::do_language_agnostic_bmc( message.error() << error_msg << message.eom; return CPROVER_EXIT_EXCEPTION; } - catch(...) + catch(std::runtime_error &e) { - message.error() << "unable to get solver" << message.eom; - throw std::current_exception(); + message.error() << e.what() << message.eom; + return CPROVER_EXIT_EXCEPTION; } switch(final_result) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0e7efe46da99..a61ba9e3e6c4 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -183,8 +183,6 @@ class bmct:public safety_checkert const goto_functionst &, prop_convt &); - // unwinding - virtual void setup_unwind(); void do_conversion(); virtual void freeze_program_variables(); diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 72d64a184a50..2382c7d8bfa0 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -355,7 +355,7 @@ bool bmc_covert::operator()() json_result["status"] = json_stringt(goal.satisfied ? "satisfied" : "failed"); - json_result["goal"] = json_stringt(id2string(goal_pair.first)); + json_result["goal"] = json_stringt(goal_pair.first); json_result["description"] = json_stringt(goal.description); if(goal.source_location.is_not_nil()) @@ -382,7 +382,7 @@ bool bmc_covert::operator()() if(step.is_input()) { json_objectt json_input; - json_input["id"]=json_stringt(id2string(step.io_id)); + json_input["id"] = json_stringt(step.io_id); if(step.io_args.size()==1) json_input["value"]= json(step.io_args.front(), bmc.ns, ID_unknown); @@ -393,7 +393,7 @@ bool bmc_covert::operator()() json_arrayt &goal_refs=result["coveredGoals"].make_array(); for(const auto &goal_id : test.covered_goals) { - goal_refs.push_back(json_stringt(id2string(goal_id))); + goal_refs.push_back(json_stringt(goal_id)); } } diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 295efe9c38f3..35069fc96651 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include #include @@ -50,7 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 986e368ea451..abdda442a5b5 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -25,8 +25,6 @@ symex_bmct::symex_bmct( path_storaget &path_storage) : goto_symext(mh, outer_symbol_table, _target, path_storage), record_coverage(false), - max_unwind(0), - max_unwind_is_set(false), symex_coverage(ns) { } @@ -131,25 +129,12 @@ bool symex_bmct::get_unwind( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - // We use the most specific limit we have, - // and 'infinity' when we have none. + auto limit=unwindset.get_limit(id, source.thread_nr); - loop_limitst &this_thread_limits= - thread_loop_limits[source.thread_nr]; - - loop_limitst::const_iterator l_it=this_thread_limits.find(id); - if(l_it!=this_thread_limits.end()) - this_loop_limit=l_it->second; + if(!limit.has_value()) + abort_unwind_decision = tvt(false); else - { - l_it=loop_limits.find(id); - if(l_it!=loop_limits.end()) - this_loop_limit=l_it->second; - else if(max_unwind_is_set) - this_loop_limit=max_unwind; - } - - abort_unwind_decision = tvt(unwind >= this_loop_limit); + abort_unwind_decision = tvt(unwind >= *limit); } INVARIANT( @@ -187,25 +172,12 @@ bool symex_bmct::get_unwind_recursion( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - // We use the most specific limit we have, - // and 'infinity' when we have none. - - loop_limitst &this_thread_limits= - thread_loop_limits[thread_nr]; + auto limit=unwindset.get_limit(id, thread_nr); - loop_limitst::const_iterator l_it=this_thread_limits.find(id); - if(l_it!=this_thread_limits.end()) - this_loop_limit=l_it->second; + if(!limit.has_value()) + abort_unwind_decision = tvt(false); else - { - l_it=loop_limits.find(id); - if(l_it!=loop_limits.end()) - this_loop_limit=l_it->second; - else if(max_unwind_is_set) - this_loop_limit=max_unwind; - } - - abort_unwind_decision = tvt(unwind>this_loop_limit); + abort_unwind_decision = tvt(unwind > *limit); } INVARIANT( diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index bc43242037bf..0808604118c9 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "symex_coverage.h" class symex_bmct: public goto_symext @@ -32,29 +34,6 @@ class symex_bmct: public goto_symext // To show progress source_locationt last_source_location; - // Control unwinding. - - void set_unwind_limit(unsigned limit) - { - max_unwind=limit; - max_unwind_is_set=true; - } - - void set_unwind_thread_loop_limit( - unsigned thread_nr, - const irep_idt &id, - unsigned limit) - { - thread_loop_limits[thread_nr][id]=limit; - } - - void set_unwind_loop_limit( - const irep_idt &id, - unsigned limit) - { - loop_limits[id]=limit; - } - /// Loop unwind handlers take the function ID and loop number, the unwind /// count so far, and an out-parameter specifying an advisory maximum, which /// they may set. If set the advisory maximum is set it is *only* used to @@ -101,26 +80,12 @@ class symex_bmct: public goto_symext bool record_coverage; -protected: - // We have - // 1) a global limit (max_unwind) - // 2) a limit per loop, all threads - // 3) a limit for a particular thread. - // 4) zero or more handler functions that can special-case particular - // functions or loops - // We use the most specific of the above. - - unsigned max_unwind; - bool max_unwind_is_set; - - typedef std::unordered_map loop_limitst; - loop_limitst loop_limits; - - typedef std::map thread_loop_limitst; - thread_loop_limitst thread_loop_limits; + unwindsett unwindset; +protected: /// Callbacks that may provide an unwind/do-not-unwind decision for a loop std::vector loop_unwind_handlers; + /// Callbacks that may provide an unwind/do-not-unwind decision for a /// recursive call std::vector recursion_unwind_handlers; diff --git a/src/clobber/Makefile b/src/clobber/Makefile index aa195f87233c..4f9562e354b7 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -13,7 +13,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/dump_c$(OBJEXT) \ diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 4639103e47e0..252a9cb935e9 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -33,8 +33,7 @@ codet cpp_typecheckt::cpp_constructor( elaborate_class_template(object_tc.type()); - typet tmp_type(object_tc.type()); - follow_symbol(tmp_type); + typet tmp_type(follow(object_tc.type())); assert(!is_reference(tmp_type)); diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 273c59fbde42..82d796b18aa0 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -26,8 +26,7 @@ codet cpp_typecheckt::cpp_destructor( elaborate_class_template(object.type()); - typet tmp_type(object.type()); - follow_symbol(tmp_type); + typet tmp_type(follow(object.type())); assert(!is_reference(tmp_type)); diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 50da8557d3b5..44790ed2a42a 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -189,7 +189,7 @@ void cpp_typecheckt::elaborate_class_template( if(type.id()!=ID_symbol) return; - const symbolt &symbol=lookup(type); + const symbolt &symbol = lookup(to_symbol_type(type)); // Make a copy, as instantiate will destroy the symbol type! const typet t_type=symbol.type; diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp index 26d2efb210e7..a9cabf3c1120 100644 --- a/src/cpp/cpp_typecheck_bases.cpp +++ b/src/cpp/cpp_typecheck_bases.cpp @@ -51,8 +51,8 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) throw 0; } - const symbolt &base_symbol= - lookup(base_symbol_expr.type()); + const symbolt &base_symbol = + lookup(to_symbol_type(base_symbol_expr.type())); if(base_symbol.type.id()==ID_incomplete_struct) { diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 45d7c8727596..3a5ac9cd9c05 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -100,8 +100,8 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr) typecheck_type(base); typecheck_type(deriv); - follow_symbol(base); - follow_symbol(deriv); + base = follow(base); + deriv = follow(deriv); if(base.id()!=ID_struct || deriv.id()!=ID_struct) expr=false_exprt(); @@ -1991,7 +1991,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( // look at type of function - follow_symbol(expr.function().type()); + expr.function().type() = follow(expr.function().type()); if(expr.function().type().id()==ID_pointer) { diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 647e1e14e467..3eca6b3bc122 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -352,8 +352,8 @@ exprt cpp_typecheck_resolvet::convert_identifier( while(followed_type.id()==ID_symbol) { - typet tmp=cpp_typecheck.lookup(followed_type).type; - followed_type=tmp; + followed_type = + cpp_typecheck.follow(to_symbol_type(followed_type)); constant |= followed_type.get_bool(ID_C_constant); } @@ -1899,8 +1899,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( const exprt &expr, const cpp_typecheck_fargst &fargs) { - typet tmp=expr.type(); - cpp_typecheck.follow_symbol(tmp); + typet tmp = cpp_typecheck.follow(expr.type()); if(!tmp.get_bool(ID_is_template)) return nil_exprt(); // not a template diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 04cd02412d13..296d3965782b 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -56,6 +56,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "taint_analysis.h" #include "unreachable_instructions.h" @@ -477,6 +478,7 @@ int goto_analyzer_parse_optionst::doit() /// Depending on the command line mode, run one of the analysis tasks int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) { + adjust_float_expressions(goto_model); if(options.get_bool_option("taint")) { std::string taint_file=cmdline.get_value("taint"); diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index df85702500d0..2e763978dcb3 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -153,10 +153,9 @@ void static_analyzert::json_report(const std::string &file_name) else j["status"]=json_stringt("UNKNOWN"); - j["file"]=json_stringt(id2string(i_it->source_location.get_file())); + j["file"] = json_stringt(i_it->source_location.get_file()); j["line"]=json_numbert(id2string(i_it->source_location.get_line())); - j["description"]=json_stringt(id2string( - i_it->source_location.get_comment())); + j["description"] = json_stringt(i_it->source_location.get_comment()); } } diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 08e29037c703..ebda62896dd3 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -12,6 +12,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include #include #include #include @@ -169,6 +170,10 @@ bool static_simplifier( goto_model.goto_functions.update(); } + // restore return types before writing the binary + restore_returns(goto_model); + goto_model.goto_functions.update(); + m.status() << "Writing goto binary" << messaget::eom; return write_goto_binary(out, ns.get_symbol_table(), diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index f2722c98e911..675393872276 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -351,10 +351,9 @@ bool taint_analysist::operator()( if(use_json) { json_objectt json; - json["bugClass"]= - json_stringt(id2string(i_it->source_location.get_property_class())); - json["file"]= - json_stringt(id2string(i_it->source_location.get_file())); + json["bugClass"] = + json_stringt(i_it->source_location.get_property_class()); + json["file"] = json_stringt(i_it->source_location.get_file()); json["line"]= json_numbert(id2string(i_it->source_location.get_line())); json_result.array.push_back(json); diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index c691142aeadc..bae1266ee89d 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -127,7 +127,7 @@ static void add_to_json( DATA_INVARIANT(end_function->is_end_function(), "The last instruction in a goto-program must be END_FUNCTION"); - entry["function"]=json_stringt(id2string(end_function->function)); + entry["function"] = json_stringt(end_function->function); entry["fileName"]= json_stringt(concat_dir_file( id2string(end_function->source_location.get_working_directory()), @@ -261,7 +261,7 @@ static void json_output_function( { json_objectt &entry=dest.push_back().make_object(); - entry["function"]=json_stringt(id2string(function)); + entry["function"] = json_stringt(function); entry["file name"]= json_stringt(concat_dir_file( id2string(first_location.get_working_directory()), diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 9325b323c64c..648aa90b9a24 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -25,7 +25,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../goto-instrument/cover_instrument_other$(OBJEXT) \ ../goto-instrument/cover_util$(OBJEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index a06b13edf2b7..16a8f5239793 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -136,7 +136,7 @@ void goto_difft::convert_function_json( namespacet ns(goto_model.symbol_table); const symbolt &symbol = ns.lookup(function_name); - result["name"] = json_stringt(id2string(function_name)); + result["name"] = json_stringt(function_name); result["sourceLocation"] = json(symbol.location); if(options.get_bool_option("show-properties")) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 889fee4c0ede..e32b36ae50b1 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -24,6 +24,7 @@ Author: Peter Schrammel #include +#include #include #include #include @@ -45,7 +46,6 @@ Author: Peter Schrammel #include #include -#include #include diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index bb4ff425dafb..126151d9c037 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \ undefined_functions.cpp \ uninitialized.cpp \ unwind.cpp \ + unwindset.cpp \ wmm/abstract_event.cpp \ wmm/cycle_collection.cpp \ wmm/data_dp.cpp \ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 459fccd1ea48..6cebedc173de 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -261,8 +261,18 @@ static void instrument_cover_goals( { Forall_goto_program_instructions(i_it, function.body) { + // Simplify the common case where we have ASSERT(x); ASSUME(x): if(i_it->is_assert()) - i_it->type=goto_program_instruction_typet::ASSUME; + { + auto successor = std::next(i_it); + if(successor != function.body.instructions.end() && + successor->is_assume() && + successor->guard == i_it->guard) + { + successor->make_skip(); + } + i_it->type = goto_program_instruction_typet::ASSUME; + } } } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index cdfa46f45d9d..c8ddbf16a500 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -139,43 +139,26 @@ int goto_instrument_parse_optionst::doit() instrument_goto_program(); { - bool unwind=cmdline.isset("unwind"); - bool unwindset=cmdline.isset("unwindset"); - bool unwindset_file=cmdline.isset("unwindset-file"); + bool unwind_given=cmdline.isset("unwind"); + bool unwindset_given=cmdline.isset("unwindset"); + bool unwindset_file_given=cmdline.isset("unwindset-file"); - if(unwindset && unwindset_file) + if(unwindset_given && unwindset_file_given) throw "only one of --unwindset and --unwindset-file supported at a " "time"; - if(unwind || unwindset || unwindset_file) + if(unwind_given || unwindset_given || unwindset_file_given) { - int k=-1; + unwindsett unwindset; - if(unwind) - k=std::stoi(cmdline.get_value("unwind")); + if(unwind_given) + unwindset.parse_unwind(cmdline.get_value("unwind")); - unwind_sett unwind_set; + if(unwindset_file_given) + unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file")); - if(unwindset_file) - { - std::string us; - std::string fn=cmdline.get_value("unwindset-file"); - -#ifdef _MSC_VER - std::ifstream file(widen(fn)); -#else - std::ifstream file(fn); -#endif - if(!file) - throw "cannot open file "+fn; - - std::stringstream buffer; - buffer << file.rdbuf(); - us=buffer.str(); - parse_unwindset(us, unwind_set); - } - else if(unwindset) - parse_unwindset(cmdline.get_value("unwindset"), unwind_set); + if(unwindset_given) + unwindset.parse_unwindset(cmdline.get_value("unwindset")); bool unwinding_assertions=cmdline.isset("unwinding-assertions"); bool partial_loops=cmdline.isset("partial-loops"); @@ -202,7 +185,7 @@ int goto_instrument_parse_optionst::doit() } goto_unwindt goto_unwind; - goto_unwind(goto_model, unwind_set, k, unwind_strategy); + goto_unwind(goto_model, unwindset, unwind_strategy); goto_model.goto_functions.update(); goto_model.goto_functions.compute_loop_numbers(); diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 9658c218a837..2f65d0b48934 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -44,6 +44,15 @@ reachability_slicert::get_sources( return sources; } +static bool is_same_target( + goto_programt::const_targett it1, + goto_programt::const_targett it2) +{ + // Avoid comparing iterators belonging to different functions, and therefore + // different std::lists. + return it1->function == it2->function && it1 == it2; +} + /// Perform backwards depth-first search of the control-flow graph of the /// goto program, starting from the nodes corresponding to the criterion and /// the instructions that might be executed concurrently. Set reaches_assertion @@ -54,11 +63,50 @@ void reachability_slicert::fixedpoint_to_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion) { - std::vector src = get_sources(is_threaded, criterion); + std::vector stack; + std::vector sources = get_sources(is_threaded, criterion); + for(const auto source : sources) + stack.emplace_back(source, false); + + while(!stack.empty()) + { + auto &node = cfg[stack.back().node_index]; + const auto caller_is_known = stack.back().caller_is_known; + stack.pop_back(); - std::vector reachable = cfg.get_reachable(src, false); - for(const auto index : reachable) - cfg[index].reaches_assertion = true; + if(node.reaches_assertion) + continue; + node.reaches_assertion = true; + + for(const auto &edge : node.in) + { + const auto &pred_node = cfg[edge.first]; + + if(pred_node.PC->is_end_function()) + { + // This is an end-of-function -> successor-of-callsite edge. + // Queue both the caller and the end of the callee. + INVARIANT( + std::prev(node.PC)->is_function_call(), + "all function return edges should point to the successor of a " + "FUNCTION_CALL instruction"); + stack.emplace_back(edge.first, true); + stack.emplace_back( + cfg.entry_map[std::prev(node.PC)], caller_is_known); + } + else if(pred_node.PC->is_function_call()) + { + // Skip this predecessor, unless this is a bodyless function, or we + // don't know who our callee was: + if(!caller_is_known || is_same_target(std::next(pred_node.PC), node.PC)) + stack.emplace_back(edge.first, caller_is_known); + } + else + { + stack.emplace_back(edge.first, caller_is_known); + } + } + } } /// Perform forwards depth-first search of the control-flow graph of the @@ -71,11 +119,66 @@ void reachability_slicert::fixedpoint_from_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion) { - std::vector src = get_sources(is_threaded, criterion); + std::vector stack; + std::vector sources = get_sources(is_threaded, criterion); + for(const auto source : sources) + stack.emplace_back(source, false); - const std::vector reachable = cfg.get_reachable(src, true); - for(const auto index : reachable) - cfg[index].reachable_from_assertion = true; + while(!stack.empty()) + { + auto &node = cfg[stack.back().node_index]; + const auto caller_is_known = stack.back().caller_is_known; + stack.pop_back(); + + if(node.reachable_from_assertion) + continue; + node.reachable_from_assertion = true; + + if(node.PC->is_function_call()) + { + // Queue the instruction's natural successor (function head, or next + // instruction if the function is bodyless) + INVARIANT(node.out.size() == 1, "Call sites should have one successor"); + const auto successor_index = node.out.begin()->first; + + // If the function has a body, mark the function head, but note that we + // have already taken care of the return site. + const auto &callee_head_node = cfg[successor_index]; + auto callee_it = callee_head_node.PC; + if(!is_same_target(callee_it, std::next(node.PC))) + { + stack.emplace_back(successor_index, true); + + // Check if it can return, and if so mark the callsite's successor: + while(!callee_it->is_end_function()) + ++callee_it; + + if(!cfg[cfg.entry_map[callee_it]].out.empty()) + { + stack.emplace_back( + cfg.entry_map[std::next(node.PC)], caller_is_known); + } + } + else + { + // Bodyless function -- mark the successor instruction only. + stack.emplace_back(successor_index, caller_is_known); + } + } + else if(node.PC->is_end_function() && caller_is_known) + { + // Special case -- the callsite successor was already queued when entering + // this function, more precisely than we can see from the function return + // edges (which lead to all possible callers), so nothing to do here. + } + else + { + // General case, including end-of-function where we don't know our caller. + // Queue all successors. + for(const auto &edge : node.out) + stack.emplace_back(edge.first, caller_is_known); + } + } } /// This function removes all instructions that have the flag diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 5f52a6d17950..2bb241e785d2 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -51,6 +51,29 @@ class reachability_slicert typedef std::stack queuet; + /// A search stack entry, used in tracking nodes to mark reachable when + /// walking over the CFG in `fixedpoint_to_assertions` and + /// `fixedpoint_from_assertions`. + struct search_stack_entryt + { + /// CFG node to mark reachable + cfgt::node_indext node_index; + + /// If true, this function's caller is known and has already been queued to + /// mark reachable, so there is no need to queue anything when walking out + /// of the function, whether forwards (via END_FUNCTION) or backwards (via a + /// callsite). + /// If false, this function's caller is not known, so when walking forwards + /// from the end or backwards from the beginning we should queue all + /// possible callers. + bool caller_is_known; + + search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known) : + node_index(node_index), caller_is_known(caller_is_known) + { + } + }; + void fixedpoint_to_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion); diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 9784d648f392..581d5c1bb74e 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -107,8 +107,8 @@ void stack_depth( goto_programt::targett it=init.insert_before(first); it->make_assignment(); it->code=code_assignt(sym, from_integer(0, sym.type())); - it->source_location=first->source_location; - it->function=first->function; + // no suitable value for source location -- omitted + it->function = INITIALIZE_FUNCTION; // update counters etc. goto_model.goto_functions.update(); diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 01b0087c522a..00beb99ddcb2 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -22,40 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "loop_utils.h" -void parse_unwindset(const std::string &us, unwind_sett &unwind_set) -{ - assert(unwind_set.empty()); - - std::vector result; - split_string(us, ',', result, true, true); - assert(!result.empty()); - - if(result.front().empty()) // allow empty string as unwindset - return; - - for(std::vector::const_iterator it=result.begin(); - it!=result.end(); it++) - { - std::string loop; - std::string bound; - - split_string(*it, ':', loop, bound, true); - - std::string func; - std::string id; - - split_string(loop, '.', func, id, true); - - unsigned loop_id=std::stoi(id); - int loop_bound=std::stoi(bound); - - if(loop_bound<-1) - throw "given unwind bound < -1"; - - unwind_set[func][loop_id]=loop_bound; - } -} - void goto_unwindt::copy_segment( const goto_programt::const_targett start, const goto_programt::const_targett end, // exclusive @@ -290,37 +256,11 @@ void goto_unwindt::unwind( goto_program.destructive_insert(loop_exit, copies); } -int goto_unwindt::get_k( - const irep_idt func, - const unsigned loop_id, - const int global_k, - const unwind_sett &unwind_set) const -{ - assert(global_k>=-1); - - unwind_sett::const_iterator f_it=unwind_set.find(func); - if(f_it==unwind_set.end()) - return global_k; - - const std::map &m=f_it->second; - std::map::const_iterator l_it=m.find(loop_id); - if(l_it==m.end()) - return global_k; - - int k=l_it->second; - assert(k>=-1); - - return k; -} - void goto_unwindt::unwind( goto_programt &goto_program, - const unwind_sett &unwind_set, - const int k, + const unwindsett &unwindset, const unwind_strategyt unwind_strategy) { - assert(k>=-1); - for(goto_programt::const_targett i_it=goto_program.instructions.begin(); i_it!=goto_program.instructions.end();) { @@ -340,12 +280,14 @@ void goto_unwindt::unwind( const irep_idt func=i_it->function; assert(!func.empty()); - unsigned loop_number=i_it->loop_number; + const irep_idt loop_id= + id2string(func) + "." + std::to_string(i_it->loop_number); - int final_k=get_k(func, loop_number, k, unwind_set); + auto limit=unwindset.get_limit(loop_id, 0); - if(final_k==-1) + if(!limit.has_value()) { + // no unwinding given i_it++; continue; } @@ -355,7 +297,7 @@ void goto_unwindt::unwind( loop_exit++; assert(loop_exit!=goto_program.instructions.end()); - unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy); + unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy); // necessary as we change the goto program in the previous line i_it=loop_exit; @@ -364,12 +306,9 @@ void goto_unwindt::unwind( void goto_unwindt::operator()( goto_functionst &goto_functions, - const unwind_sett &unwind_set, - const int k, + const unwindsett &unwindset, const unwind_strategyt unwind_strategy) { - assert(k>=-1); - Forall_goto_functions(it, goto_functions) { goto_functionst::goto_functiont &goto_function=it->second; @@ -383,7 +322,7 @@ void goto_unwindt::operator()( goto_programt &goto_program=goto_function.body; - unwind(goto_program, unwind_set, k, unwind_strategy); + unwind(goto_program, unwindset, unwind_strategy); } } diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h index 072c6f542678..89b8ea40c086 100644 --- a/src/goto-instrument/unwind.h +++ b/src/goto-instrument/unwind.h @@ -13,17 +13,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H #define CPROVER_GOTO_INSTRUMENT_UNWIND_H +#include "unwindset.h" + #include #include #include class goto_modelt; -// -1: do not unwind loop -typedef std::map> unwind_sett; - -void parse_unwindset(const std::string &us, unwind_sett &unwind_set); - class goto_unwindt { public: @@ -50,44 +47,22 @@ class goto_unwindt void unwind( goto_programt &goto_program, - const unwind_sett &unwind_set, - const int k=-1, // -1: no global bound + const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL); // unwind all functions - - void operator()( - goto_functionst &goto_functions, - const unsigned k, // global bound - const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) - { - const unwind_sett unwind_set; - operator()(goto_functions, unwind_set, k, unwind_strategy); - } - void operator()( goto_functionst &, - const unwind_sett &unwind_set, - const int k=-1, // -1: no global bound + const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL); void operator()( goto_modelt &goto_model, - const unsigned k, // global bound - const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) - { - const unwind_sett unwind_set; - operator()(goto_model.goto_functions, unwind_set, k, unwind_strategy); - } - - void operator()( - goto_modelt &goto_model, - const unwind_sett &unwind_set, - const int k=-1, // -1: no global bound + const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) { operator()( - goto_model.goto_functions, unwind_set, k, unwind_strategy); + goto_model.goto_functions, unwindset, unwind_strategy); } // unwind log @@ -132,8 +107,7 @@ class goto_unwindt int get_k( const irep_idt func, const unsigned loop_id, - const int global_k, - const unwind_sett &unwind_set) const; + const unwindsett &unwindset) const; // copy goto program segment and redirect internal edges void copy_segment( diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp new file mode 100644 index 000000000000..5865494a6edc --- /dev/null +++ b/src/goto-instrument/unwindset.cpp @@ -0,0 +1,99 @@ +/*******************************************************************\ + +Module: Loop unwinding setup + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "unwindset.h" + +#include +#include +#include + +#include +#include + +void unwindsett::parse_unwind(const std::string &unwind) +{ + if(!unwind.empty()) + global_limit = unsafe_string2unsigned(unwind); +} + +void unwindsett::parse_unwindset(const std::string &unwindset) +{ + std::vector unwindset_loops; + split_string(unwindset, ',', unwindset_loops, true, true); + + for(auto &val : unwindset_loops) + { + unsigned thread_nr = 0; + bool thread_nr_set = false; + + if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos) + { + std::string nr = val.substr(0, val.find(":")); + thread_nr = unsafe_string2unsigned(nr); + thread_nr_set = true; + val.erase(0, nr.size() + 1); + } + + if(val.rfind(":") != std::string::npos) + { + std::string id = val.substr(0, val.rfind(":")); + std::string uw_string = val.substr(val.rfind(":") + 1); + + // the below initialisation makes g++-5 happy + optionalt uw(0); + + if(uw_string.empty()) + uw = { }; + else + uw = unsafe_string2unsigned(uw_string); + + if(thread_nr_set) + thread_loop_map[std::pair(id, thread_nr)] = uw; + else + loop_map[id] = uw; + } + } +} + +optionalt +unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const +{ + // We use the most specific limit we have + + // thread x loop + auto tl_it = + thread_loop_map.find(std::pair(loop_id, thread_nr)); + + if(tl_it != thread_loop_map.end()) + return tl_it->second; + + // loop + auto l_it = loop_map.find(loop_id); + + if(l_it != loop_map.end()) + return l_it->second; + + // global, if any + return global_limit; +} + +void unwindsett::parse_unwindset_file(const std::string &file_name) +{ + #ifdef _MSC_VER + std::ifstream file(widen(file_name)); + #else + std::ifstream file(file_name); + #endif + + if(!file) + throw "cannot open file "+file_name; + + std::stringstream buffer; + buffer << file.rdbuf(); + parse_unwindset(buffer.str()); +} diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h new file mode 100644 index 000000000000..3a20b2ac0289 --- /dev/null +++ b/src/goto-instrument/unwindset.h @@ -0,0 +1,56 @@ +/*******************************************************************\ + +Module: Loop unwinding setup + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Loop unwinding + +#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H +#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H + +#include +#include + +#include +#include + +class unwindsett +{ +public: + // We have + // 1) a global limit + // 2) a limit per loop, all threads + // 3) a limit for a particular thread. + // We use the most specific of the above. + + // global limit for all loops + void parse_unwind(const std::string &unwind); + + // limit for instances of a loop + void parse_unwindset(const std::string &unwindset); + + // queries + optionalt get_limit(const irep_idt &loop, unsigned thread_id) const; + + // read unwindset directives from a file + void parse_unwindset_file(const std::string &file_name); + +protected: + optionalt global_limit; + + // Limit for all instances of a loop. + // This may have 'no value'. + typedef std::map> loop_mapt; + loop_mapt loop_map; + + // separate limits per thread + using thread_loop_mapt = + std::map, optionalt>; + thread_loop_mapt thread_loop_map; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H diff --git a/src/goto-instrument/wmm/fence.cpp b/src/goto-instrument/wmm/fence.cpp index 82e9308278d8..0e0fe44f37cf 100644 --- a/src/goto-instrument/wmm/fence.cpp +++ b/src/goto-instrument/wmm/fence.cpp @@ -19,25 +19,33 @@ bool is_fence( const goto_programt::instructiont &instruction, const namespacet &ns) { - return (instruction.is_function_call() && ns.lookup( - to_code_function_call(instruction.code).function()).base_name == "fence") - /* if assembly-sensitive algorithms are not available */ - || (instruction.is_other() && instruction.code.get_statement()==ID_fence - && instruction.code.get_bool(ID_WWfence) - && instruction.code.get_bool(ID_WRfence) - && instruction.code.get_bool(ID_RWfence) - && instruction.code.get_bool(ID_RRfence)); + return (instruction.is_function_call() && + ns.lookup( + to_symbol_expr( + to_code_function_call(instruction.code).function())) + .base_name == "fence") + /* if assembly-sensitive algorithms are not available */ + || (instruction.is_other() && + instruction.code.get_statement() == ID_fence && + instruction.code.get_bool(ID_WWfence) && + instruction.code.get_bool(ID_WRfence) && + instruction.code.get_bool(ID_RWfence) && + instruction.code.get_bool(ID_RRfence)); } bool is_lwfence( const goto_programt::instructiont &instruction, const namespacet &ns) { - return (instruction.is_function_call() && ns.lookup( - to_code_function_call(instruction.code).function()).base_name == "lwfence") - /* if assembly-sensitive algorithms are not available */ - || (instruction.is_other() && instruction.code.get_statement()==ID_fence - && instruction.code.get_bool(ID_WWfence) - && instruction.code.get_bool(ID_RWfence) - && instruction.code.get_bool(ID_RRfence)); + return (instruction.is_function_call() && + ns.lookup( + to_symbol_expr( + to_code_function_call(instruction.code).function())) + .base_name == "lwfence") + /* if assembly-sensitive algorithms are not available */ + || (instruction.is_other() && + instruction.code.get_statement() == ID_fence && + instruction.code.get_bool(ID_WWfence) && + instruction.code.get_bool(ID_RWfence) && + instruction.code.get_bool(ID_RRfence)); } diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index cefd43949cef..19e5878ca412 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,9 +1,8 @@ -SRC = basic_blocks.cpp \ +SRC = adjust_float_expressions.cpp \ builtin_functions.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ compute_called_functions.cpp \ - convert_nondet.cpp \ destructor.cpp \ elf_reader.cpp \ format_strings.cpp \ @@ -20,7 +19,6 @@ SRC = basic_blocks.cpp \ goto_inline.cpp \ goto_inline_class.cpp \ goto_program.cpp \ - goto_program_irep.cpp \ goto_program_template.cpp \ goto_trace.cpp \ graphml_witness.cpp \ diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp similarity index 99% rename from src/goto-symex/adjust_float_expressions.cpp rename to src/goto-programs/adjust_float_expressions.cpp index 89abaf657577..c7163c8b19b6 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include "goto_model.h" static bool have_to_adjust_float_expressions( const exprt &expr, diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h similarity index 79% rename from src/goto-symex/adjust_float_expressions.h rename to src/goto-programs/adjust_float_expressions.h index bd011641d54b..eaa5417b75d4 100644 --- a/src/goto-symex/adjust_float_expressions.h +++ b/src/goto-programs/adjust_float_expressions.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution -#ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H -#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H +#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H +#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H #include @@ -31,4 +31,4 @@ void adjust_float_expressions( const namespacet &ns); void adjust_float_expressions(goto_modelt &goto_model); -#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H +#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H diff --git a/src/goto-programs/basic_blocks.cpp b/src/goto-programs/basic_blocks.cpp deleted file mode 100644 index 75b91b82bd68..000000000000 --- a/src/goto-programs/basic_blocks.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/*******************************************************************\ - -Module: Group Basic Blocks in Goto Program - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Group Basic Blocks in Goto Program - -#include "basic_blocks.h" - -/// convert basic blocks into single expressions of type "block" -void basic_blocks(goto_programt &goto_program, - unsigned max_block_size) -{ - // get the targets - typedef std::set targetst; - - targetst targets; - - for(goto_programt::instructionst::iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) - if(i_it->is_goto()) - for(const auto &target : i_it->targets) - targets.insert(target); - - // Scan program - for(goto_programt::instructionst::iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); - ) // intentionally no it++ - { - // gotos and empty code are left unchanged - if(it->is_goto() || it->is_dead() || - it->is_assert() || it->is_assume() || - it->is_atomic_begin() || it->is_atomic_end() || - it->is_end_thread() || it->is_start_thread() || - it->is_end_function() || it->is_location() || - it->is_skip() || it->is_function_call() || - it->is_decl()) - it++; - else if(it->is_other() || it->is_assign()) - { - if(it->code.is_nil()) - it++; - else - { - unsigned count=0; - - // this is the start of a new block - targetst::iterator t_it; // iterator for searching targets - - // find the end of the block - goto_programt::instructionst::iterator end_block = it; - do - { - end_block++; - count++; - if(end_block!=goto_program.instructions.end()) - t_it=targets.find(end_block); - - if(max_block_size!=0 && count>=max_block_size) - break; - } - while(end_block!=goto_program.instructions.end() && - (end_block->is_other() || end_block->is_assign()) && - t_it==targets.end()); - - // replace it with the code of the block - - { - code_blockt new_block; - - for(goto_programt::instructionst::iterator stmt = it; - stmt != end_block; - stmt++) - if(!stmt->code.is_nil()) - new_block.move_to_operands(stmt->code); - - it->code.swap(new_block); - it++; - if(it!=goto_program.instructions.end()) - it=goto_program.instructions.erase(it, end_block); - } - } - } - else - UNREACHABLE; - } -} diff --git a/src/goto-programs/basic_blocks.h b/src/goto-programs/basic_blocks.h deleted file mode 100644 index d667c4655d4b..000000000000 --- a/src/goto-programs/basic_blocks.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Group Basic Blocks in Goto Program - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Group Basic Blocks in Goto Program - -#ifndef CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H -#define CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H - -#include "goto_program.h" - -void basic_blocks(goto_programt &goto_program, - unsigned max_block_size=0); - -#endif // CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H diff --git a/src/goto-programs/generate_function_bodies.h b/src/goto-programs/generate_function_bodies.h index 4801b6cc5082..61e818a1b7a1 100644 --- a/src/goto-programs/generate_function_bodies.h +++ b/src/goto-programs/generate_function_bodies.h @@ -68,17 +68,21 @@ void generate_function_bodies( goto_modelt &model, message_handlert &message_handler); -#define OPT_REPLACE_FUNCTION_BODY \ - "(generate-function-body):" \ +// clang-format off +#define OPT_REPLACE_FUNCTION_BODY \ + "(generate-function-body):" \ "(generate-function-body-options):" -#define HELP_REPLACE_FUNCTION_BODY \ - " --generate-function-body \n" \ - " Generate bodies for functions matching regex" \ - " --generate-function-body-options