move setup_unwind to parse_unwindset_options to prevent duplication #2167

kroening · 2018-05-08T13:08:24Z

No description provided.

peterschrammel

There's another one that needs to be replaced here: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/unwind.cpp#L25

smowton · 2018-05-10T10:31:23Z

I think if the method is specific to configuring symex_bmct is should be defined on symex_bmct. Otherwise lgtm.

tautschnig · 2018-05-10T12:57:56Z

Echoing what @peterschrammel - my assumption had been that a key point of this PR was to re-use the existing implementation that @peterschrammel pointed out. With the work that @danpoe had done in implementing the static unwinder it's not actually specific to anything doing symbolic execution anymore. Indeed it might be adequate to move the bits from goto-instrument to goto-programs.

kroening · 2018-05-12T12:42:50Z

Now in a separate data structure, which enables use in goto-instrument as well

tautschnig

I think this is great work, making code a lot cleaner. My comments mostly suggest even more cleanup that would well fit this PR.

tautschnig · 2018-05-12T13:18:58Z

src/cbmc/symex_bmc.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]

 #include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/string_utils.h>
+#include <util/string2int.h>


Just wondering: are those still needed here?

tautschnig · 2018-05-12T13:20:14Z

src/cbmc/symex_bmc.cpp

-    }
-
-    abort_unwind_decision = tvt(unwind >= this_loop_limit);
+      abort_unwind_decision = tvt(unwind >= *limit);


Since the very same code exists twice: how about adding a tvt unwindsett::limit_reached(id, thread_nr, unwind)?

Not easy, "this_loop_limit" is used later, and those handlers want the function name, not the loop ID

(I want to get rid of the handlers, BTW, that is the whole point of overloading those methods in goto-symex)

I don't really understand. Lines 132...137 are, except for source.thread_nr vs thread_nr, exactly the same as lines 175..180.

Which, btw, changes the behaviour: in the previous code, one used >= in the comparison, while the other used >. (I'm not sure they actually should be different...)

tautschnig · 2018-05-12T13:24:36Z

src/goto-instrument/unwindset.cpp

+void unwindsett::parse_unwind(const std::string &unwind)
+{
+  if(!unwind.empty())
+    global_limit=unsafe_string2unsigned(unwind);


I would have gone for the safe variant, in particular as it is user-provided input.

tautschnig · 2018-05-12T13:28:10Z

src/goto-instrument/goto_instrument_parse_options.cpp

-        unwind_sett unwind_set;
-
-        if(unwindset_file)
+        if(unwindset_file_given)


Would it be possible to move all this code to unwindset.cpp as well? *parse_options tends to be way too big anyway...

that adds to the complexity of all users, say jbmc, cbmc; mildly reluctant

Just to be clear: I mainly wanted the code to move, not necessarily add that to the external user interface. Factoring out what belongs together would have seemed like a good idea?!

But also: It might actually be desirable to open up this additional option to all users?

smowton

Looks reasonable -- if you're killing the handlers in the future though, please do retain some way for the driver program to provide special unwind information, as its language-specific understanding can give us a concrete bound for a particular loop.

tautschnig · 2018-05-14T09:33:03Z

(This also needs a rebase, commits that have already been merged into develop have crept in.)

kroening · 2018-05-14T13:25:43Z

Rebase done

tautschnig · 2018-05-16T17:14:10Z

src/cbmc/symex_bmc.cpp

-    }
-
-    abort_unwind_decision = tvt(unwind>this_loop_limit);
+      abort_unwind_decision = tvt(unwind >= *limit);


This change still bothers me: the previous code used > instead of >= here.

The counting seems to be different for recursion and loops. Restoring >.

tautschnig

(redundantly) approving under the assumption of the > vs. >= fix.

31ef182 Merge pull request diffblue#2208 from diffblue/cleanout-goto-programs 0e84d3e Merge pull request diffblue#2195 from smowton/smowton/feature/smarter-reachability-slicer c801126 Merge pull request diffblue#2209 from diffblue/travis-no-osx-g++ 3487bf7 Reachability slicer: mark reachable code more precisely 85e8451 Merge pull request diffblue#2066 from tautschnig/bv-endianness 5e5eafb Merge pull request diffblue#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 diffblue#2203 from diffblue/typed-lookup d77dea3 strongly type the lookup() methods in namespacet 2382f27 Merge pull request diffblue#2193 from martin-cs/feature/correct-instruction-documentation c314272 Merge pull request diffblue#2181 from diffblue/format-expr-constants 514a0a5 Merge pull request diffblue#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 diffblue#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 diffblue#2110 from tautschnig/type-mismatch-exception 18fb262 Merge pull request diffblue#2025 from tautschnig/stack-depth-fix 9191b6a Merge pull request diffblue#2199 from tautschnig/simplifier-typing f99e631 Merge pull request diffblue#2198 from tautschnig/fix-test-desc 1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty a7690ba Merge pull request diffblue#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 diffblue#1899 from danpoe/sharing-map-catch-unit-tests 9cc6aae Merge pull request diffblue#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 diffblue#2187 from diffblue/move-convert-nondet 6d8c3fa Merge pull request diffblue#2189 from thk123/bugfix/json-parser-restart 2ad157f Merge pull request diffblue#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 diffblue#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 diffblue#1858 from danpoe/dependence-graph-fix 10b8b09 Merge pull request diffblue#2011 from thomasspriggs/final_classes a154593 Merge pull request diffblue#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 diffblue#2180 from thomasspriggs/json_id2string 8941567 Merge pull request diffblue#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: 31ef182

kroening requested review from tautschnig and peterschrammel May 8, 2018 13:08

kroening requested a review from smowton as a code owner May 8, 2018 13:08

peterschrammel reviewed May 9, 2018

View reviewed changes

kroening force-pushed the parse_unwindset_options branch from c5c75ad to 17e3f60 Compare May 12, 2018 12:42

kroening requested review from cesaro, chrisr-diffblue, martin-cs and mgudemann as code owners May 12, 2018 12:42

kroening assigned peterschrammel May 12, 2018

kroening force-pushed the parse_unwindset_options branch 2 times, most recently from 90924e6 to 1270225 Compare May 12, 2018 13:27

tautschnig reviewed May 12, 2018

View reviewed changes

kroening force-pushed the parse_unwindset_options branch 4 times, most recently from e98e447 to 6ad505e Compare May 12, 2018 17:41

smowton approved these changes May 14, 2018

View reviewed changes

kroening force-pushed the parse_unwindset_options branch 2 times, most recently from 8ded6e5 to 5846362 Compare May 14, 2018 09:09

kroening force-pushed the parse_unwindset_options branch from 5846362 to 8fd52ca Compare May 14, 2018 13:25

kroening force-pushed the parse_unwindset_options branch 2 times, most recently from 27a6fed to de9c170 Compare May 14, 2018 14:34

peterschrammel approved these changes May 16, 2018

View reviewed changes

tautschnig reviewed May 16, 2018

View reviewed changes

Daniel Kroening added 2 commits May 18, 2018 12:28

introduce unwindsett for unwinding limits

dcc907a

use unwindsett in goto-instrument

f1b6174

kroening force-pushed the parse_unwindset_options branch from de9c170 to f1b6174 Compare May 18, 2018 11:29

tautschnig approved these changes May 18, 2018

View reviewed changes

kroening merged commit 514a0a5 into develop May 18, 2018

kroening deleted the parse_unwindset_options branch May 18, 2018 14:59

tautschnig mentioned this pull request Jan 16, 2021

Unwindset parser duplicated #1684

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

move setup_unwind to parse_unwindset_options to prevent duplication #2167

move setup_unwind to parse_unwindset_options to prevent duplication #2167

kroening commented May 8, 2018

peterschrammel left a comment

smowton commented May 10, 2018

tautschnig commented May 10, 2018

kroening commented May 12, 2018

tautschnig left a comment

tautschnig May 12, 2018

kroening May 12, 2018

tautschnig May 12, 2018

kroening May 12, 2018

kroening May 12, 2018

tautschnig May 14, 2018

tautschnig May 14, 2018

tautschnig May 12, 2018

tautschnig May 12, 2018

kroening May 12, 2018

tautschnig May 14, 2018

kroening May 14, 2018

smowton left a comment

tautschnig commented May 14, 2018

kroening commented May 14, 2018

tautschnig May 16, 2018

kroening May 18, 2018

kroening May 18, 2018

tautschnig left a comment

move setup_unwind to parse_unwindset_options to prevent duplication #2167

move setup_unwind to parse_unwindset_options to prevent duplication #2167

Conversation

kroening commented May 8, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

smowton commented May 10, 2018

tautschnig commented May 10, 2018

kroening commented May 12, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

tautschnig commented May 14, 2018

kroening commented May 14, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment