[TG-2922] Improve logging for byte flatten exceptions #2046

thk123 · 2018-04-12T11:27:20Z

Depends on: #2071 ✅

Submodule bump: https://github.com/diffblue/test-gen/pull/1739

A client has code that trips over this exception. However, we don't have access to the code so this change provides more information about the exception by re-throwing the exception back up the stack to record relevant information (like what kind of line is causing the problem).

TODO:

Adapt existing unit test for the string utils into a catch test
Fix commit history
Add the original goto instruction corresponding to the symex step exception.

Currently produces something like:

file TestClasses.java line 4 function java::Test1.f:(I)V: exception: Error converting guard for step
Souce GOTO statement: ((struct java::array[float] *)a1->data[j])->data[0] = 34.5f;
Step:
Thread 0 file TestClasses.java line 6 function java::Test1.f:(I)V bytecode-index 11
ASSIGNMENT (STATE)
dynamic_6_array#4 == (((struct java::array[float] { struct java.lang.Object { __CPROVER_string @class_identifier; _Bool @lock; } @java.lang.Object; signed int length; float *data; } *)byte_extract_little_endian(dynamic_2_array#5, POINTER_OFFSET(dynamic_object1#3.data), void *) == &dynamic_object5 ? dynamic_object5#5.data == dynamic_6_array : ((struct java::array[float] { struct java.lang.Object { __CPROVER_string @class_identifier; _Bool @lock; } @java.lang.Object; signed int length; float *data; } *)byte_extract_little_endian(dynamic_2_array#5, POINTER_OFFSET(dynamic_object1#3.data), void *) == &dynamic_object3 ? dynamic_object3#4.data == dynamic_6_array : invalid_object1#0.data == dynamic_6_array)) ? dynamic_6_array#3 WITH [0l:=34.5f] : dynamic_6_array#3)
Guard: (struct java::array[float] { struct java.lang.Object { __CPROVER_string @class_identifier; _Bool @lock; } @java.lang.Object; signed int length; float *data; } *)byte_extract_little_endian(dynamic_2_array#5, POINTER_OFFSET(dynamic_object1#3.data), void *) == &dynamic_object5 ? dynamic_object5#5.data == dynamic_6_array : ((struct java::array[float] { struct java.lang.Object { __CPROVER_string @class_identifier; _Bool @lock; } @java.lang.Object; signed int length; float *data; } *)byte_extract_little_endian(dynamic_2_array#5, POINTER_OFFSET(dynamic_object1#3.data), void *) == &dynamic_object3 ? dynamic_object3#4.data == dynamic_6_array : invalid_object1#0.data == dynamic_6_array)
 exception: Can't convert byte_extraction
  exception: cannot unpack array of non-const size
  array_type: array
    * size: symbol
        * type: signedbv
            * width: 32
            * #c_type: signed_int
        * identifier: java::Test1.f:(I)V::y!0@1#1
        * expression: symbol
            * type: signedbv
                * width: 32
                * #c_type: signed_int
            * identifier: java::Test1.f:(I)V::y
        * L0: 0
        * L1: 1
        * L2: 1
        * L1_object_identifier: java::Test1.f:(I)V::y!0@1
        * #SSA_symbol: 1
    * #dynamic: 1
    0: pointer
        * width: 64
        * #reference: 1
        0: struct
            * tag: java::array[float]
            * components: 
              0: 
                * type: struct
                    * incomplete_class: 1
                    * name: java::java.lang.Object
                    * tag: java.lang.Object
                    * base_name: java.lang.Object
                    * components: 
                      0: 
                        * type: string
                        * name: @class_identifier
                        * pretty_name: @class_identifier
                      1: 
                        * type: c_bool
                            * width: 8
                        * name: @lock
                        * pretty_name: @lock
                    * #class: 1
                * name: @java.lang.Object
                * base_name: @java.lang.Object
                * pretty_name: @java.lang.Object
              1: 
                * type: signedbv
                    * width: 32
                    * #c_type: signed_int
                * name: length
                * base_name: length
                * pretty_name: length
              2: 
                * type: pointer
                    * width: 64
                    * #reference: 1
                    0: floatbv
                        * width: 32
                        * f: 23
                * name: data
                * base_name: data
                * pretty_name: data
            * bases: 
              0: base
                  * type: symbol
                      * identifier: java::java.lang.Object
            * #class: 1
  max_bytes: +
    * type: unsignedbv
        * width: 64
        * #c_type: unsigned_long_int
    0: constant
        * type: unsignedbv
            * width: 64
            * #c_type: unsigned_long_int
        * value: 0000000000000000000000000000000000000000000000000000000000001000
    1: typecast
        * type: unsignedbv
            * width: 64
            * #c_type: unsigned_long_int
        0: pointer_offset
            * type: signedbv
                * width: 64
                * #c_type: signed_long_int
            0: member
                * type: pointer
                    * width: 64
                    * #reference: 1
                    0: pointer
                        * width: 64
                        0: empty
                * component_name: data
                0: symbol
                    * type: struct
                        * tag: java::array[reference]
                        * components: 
                          0: 
                            * type: struct
                                * incomplete_class: 1
                                * name: java::java.lang.Object
                                * tag: java.lang.Object
                                * base_name: java.lang.Object
                                * components: 
                                  0: 
                                    * type: string
                                    * name: @class_identifier
                                    * pretty_name: @class_identifier
                                  1: 
                                    * type: c_bool
                                        * width: 8
                                    * name: @lock
                                    * pretty_name: @lock
                                * #class: 1
                            * name: @java.lang.Object
                            * base_name: @java.lang.Object
                            * pretty_name: @java.lang.Object
                          1: 
                            * type: signedbv
                                * width: 32
                                * #c_type: signed_int
                            * name: length
                            * base_name: length
                            * pretty_name: length
                          2: 
                            * type: pointer
                                * width: 64
                                * #reference: 1
                                0: pointer
                                    * width: 64
                                    0: empty
                            * name: data
                            * base_name: data
                            * pretty_name: data
                        * bases: 
                          0: base
                              * type: symbol
                                  * identifier: java::java.lang.Object
                        * #class: 1
                    * identifier: symex_dynamic::dynamic_object1#3
                    * expression: symbol
                        * type: struct
                            * tag: java::array[reference]
                            * components: 
                              0: 
                                * type: struct
                                    * incomplete_class: 1
                                    * name: java::java.lang.Object
                                    * tag: java.lang.Object
                                    * base_name: java.lang.Object
                                    * components: 
                                      0: 
                                        * type: string
                                        * name: @class_identifier
                                        * pretty_name: @class_identifier
                                      1: 
                                        * type: c_bool
                                            * width: 8
                                        * name: @lock
                                        * pretty_name: @lock
                                    * #class: 1
                                * name: @java.lang.Object
                                * base_name: @java.lang.Object
                                * pretty_name: @java.lang.Object
                              1: 
                                * type: signedbv
                                    * width: 32
                                    * #c_type: signed_int
                                * name: length
                                * base_name: length
                                * pretty_name: length
                              2: 
                                * type: pointer
                                    * width: 64
                                    * #reference: 1
                                    0: pointer
                                        * width: 64
                                        0: empty
                                * name: data
                                * base_name: data
                                * pretty_name: data
                            * bases: 
                              0: base
                                  * type: symbol
                                      * identifier: java::java.lang.Object
                            * #class: 1
                        * identifier: symex_dynamic::dynamic_object1
                    * L2: 3
                    * L1_object_identifier: symex_dynamic::dynamic_object1
                    * #SSA_symbol: 1

Commit history still needs tidying up and I found some confusing behaviour in the string utils so want to finish off the unit tests for that.

tautschnig · 2018-04-12T11:39:57Z

I suppose that's to an extent the result of a discussion that @svorenova and I had: it is really surprising (wrong?) that Java code would generate byte_extract expressions. And actually I don't really see why this needs to be related to inaccessible client code for @svorenova has a very small example that produced this as well?!

tautschnig · 2018-04-12T11:53:23Z

More notes:

As said, the fact that Java code generates byte_extract seems broken to me. I may be wrong, but I think that's what should be fixed in the first instance.
This looks like pretty incredible machinery, and surely that's useful for debugging (notably C code will produce those kinds of byte_extract expressions).
Despite this, it's disaster recovery rather than preventing disaster. Check with @chrisr-diffblue and @danpoe on work to do the latter: such a byte_extract expression should never even hit the back-end. That's closely related to Goto program and SSA validation #1880.

majakusber · 2018-04-12T11:58:34Z

@tautschnig You are correct. Since the bug report came from a client, we are approaching this in two steps - first extending the logging for crashes of this type and second fixing the bug (by avoiding the byte extract instructions as we discussed). This is a PR for the first step, I will be preparing a PR for the second step. Extended logging should allow the client to provide us more information in the future if they encounter this crash (it took us considerable amount of time to dig out what was the actual problem).

tautschnig · 2018-04-12T12:05:55Z

(it took us considerable amount of time to dig out what was the actual problem)

You are not alone in this. @chrisr-diffblue will be able to tell you more.

Edit: that's why I insist that 3. from my above comment is important.

thk123 · 2018-04-12T12:52:02Z

@tautschnig That is mostly want I wanted to hear - that this is a reasonable approach for providing more info for these kind of errors, even when we fix the underlying problem. In this case we were able to match it up to an existing bug where we did have the source, but in general would have been hard to work out the problem without having a symmetric error in our own examples.

I suppose there will be other errors arising from the symex phase where knowing where in the symex has been got to would be useful. This machinery will make these easier to add in in the future.

Also thanks for the hint that @chrisr-diffblue is looking at something similar!

thk123 · 2018-04-12T16:06:09Z

I've updated this to also print out the original goto statement that the symex has failed to convert:

Source GOTO statement: ((struct java::array[float] *)a1->data[j])->data[0] = 34.5f;

This is probably the most important piece of information (in this case I believe clearly pointing towards writing to a multi-dimensional array.

To do this I had to thread a ns into it, only one level deeper but I think it is much clearer with this extra info right at the top.

tautschnig · 2018-04-13T17:24:56Z

I've updated this to also print out the original goto statement that the symex has failed to convert: [...]

Very useful indeed! And then I keep wondering why this introduces a byte_extract...

majakusber

Looks good and useful. The CI failures look like minor code issues. Please consider squashing the commits for introducing/moving/adjusting the unwrap code.

thk123 · 2018-04-16T11:13:08Z

So I split out the changes for the split_string (along with unit tests) into #2071 which this PR now depends on. Real diff for this commit (which remains changed from previous reviews): https://github.com/diffblue/cbmc/pull/2046/files/c00350b6d508ec40608a300db93d0288bd298304..705ee6592521f0682063273521a351c3244c0bf4

Need to add the new file to the Makefile and will squash the commits as suggested by @svorenova

thk123 · 2018-04-16T13:08:20Z

@svorenova Squashed as suggested. Also fixed the errors in Makefiles

thk123 · 2018-04-19T16:38:51Z

Created a version that should work on Windows: 9a68db3

Also added a test so we actually check the logging works (fix for the bug to come)

tautschnig · 2018-04-19T19:36:39Z

Since the "do not merge" label has been removed I've got to ask: my thinking was that this was an experimental feature. Please do state if that's not the case and there is an actual intent to get this merged.

thk123 · 2018-04-20T10:21:12Z

@tautschnig indeed the intention is to merge this. The goal here is to be able to provide more useful error messages for this kind of error in the future. That naturally requires the code to be in releases.

thk123 · 2018-04-20T10:35:27Z

Windows doesn't even appear to have the std::nested_exception so there is no way to unroll the exception. Log a warning saying you are not getting the full picture.

thk123 · 2018-04-23T12:53:48Z

src/goto-symex/symex_target_equation.cpp

+      {
+        util_throw_with_nested(
+          equation_conversion_exceptiont(
+            "Error converting guard for step", step, ns));


Copy paste error! isn't converting guard step

thk123 · 2018-04-23T12:54:24Z

@tautschnig I've added a (very) basic version for the other conversion steps. f7fd0a1

I don't have the bandwidth to expand it at the moment, but I think this is at least a mild improvement for all the cases.

I've messed up the ordering of includes in a couple of other commits, and copy pasted nonsense which I'll fix now - fixed ✅

Could you let me know if you're happy with:

Keeping the ns for the sake of printing the SSA_stept
The extra exception stuff for the other conversion steps (modulo the message being correct!)

thk123

Various include orders

thk123 · 2018-04-23T12:55:53Z

src/util/unwrap_nested_exception.cpp

+
+#include <util/invariant.h>
+#include <util/string_utils.h>
+#include <sstream>


Include in wrong place

thk123 · 2018-04-23T12:56:07Z

src/util/unwrap_nested_exception.h

+#define CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H
+
+#include <string>
+#include <exception>


Includes not correctly ordered

thk123 · 2018-04-23T13:09:58Z

src/solvers/flattening/flatten_byte_extract_exceptions.h

+
+#include <sstream>
+#include <iostream>
+#include <util/simplify_expr.h>


Not ordered correctly

thk123 · 2018-04-23T13:12:57Z

src/solvers/flattening/flatten_byte_operators.cpp

@@ -18,13 +18,17 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>

 #include "flatten_byte_operators.h"
+#include "flatten_byte_extract_exceptions.h"


Not ordered correctly

thk123 · 2018-04-23T13:13:14Z

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/endianness_map.h>

 #include "flatten_byte_operators.h"
+#include "flatten_byte_extract_exceptions.h"


Not ordered correctly

thk123 · 2018-04-23T13:13:39Z

src/goto-symex/symex_target_equation.cpp


 #include <langapi/language_util.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/literal_expr.h>
+#include <solvers/flattening/bv_conversion_exceptions.h>


Not ordered correctly

thk123 · 2018-04-23T13:13:51Z

src/goto-symex/symex_target_equation.cpp


 #include "goto_symex_state.h"
+#include "equation_conversion_exceptions.h"


Not ordered correctly

thk123 · 2018-04-23T15:08:24Z

@tautschnig Due to code owner permissions, once you're happy (As implied by the 👍), could you approve.

(@svorenova Might be worth a re-review of the final 5 commits as they are new since your review)

tautschnig · 2018-04-23T15:13:40Z

src/goto-symex/symex_target_equation.cpp

 #include <solvers/prop/literal_expr.h>
+#include <solvers/prop/prop.h>
+#include <solvers/prop/prop_conv.h>
+#include <util/format.h>


Place all util/ includes in one group.

You might add a comment with the language_util.h include that it can be removed once the now-deprecated function is gone.

tautschnig · 2018-04-23T15:17:34Z

src/goto-symex/symex_target_equation.h

@@ -32,7 +32,6 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
-  symex_target_equationt() = default;


I'm not currently reviewing this commit-by-commit so please excuse if my comment is wrong: this should go in a commit of its own. I agree that it can safely be removed, but this shouldn't be done as part of some random changes.

So this happened as I went from = default -> one that takes a namespace -> no constructor. Will update the last commit to go back to = default and while I'm in the area append an extra commit to remove it. I think this is the most logical commit history

Brilliant, thank you very much!

tautschnig · 2018-04-23T15:18:21Z

src/solvers/flattening/boolbv.cpp

+/// \return A vector of literals corresponding to the outputs of the Boolean
+///   circuit
+/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
+/// goes wrong. TODO: extend for other types of conversion exception).


Please create an issue for this "TODO" and include its id in the comment text.

tautschnig · 2018-04-23T15:21:09Z

src/goto-symex/equation_conversion_exceptions.h

+
+#include <ostream>
+
+#include <util/namespace.h>


Not needed/used.

tautschnig · 2018-04-23T15:21:22Z

src/goto-symex/equation_conversion_exceptions.h

+
+#include <util/namespace.h>
+
+#include <langapi/language_util.h>


Not needed/used.

tautschnig · 2018-04-23T15:24:10Z

src/solvers/flattening/flatten_byte_extract_exceptions.h

+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>


I think most of the above are unnecessary.

tautschnig · 2018-04-23T15:26:56Z

src/util/format.h

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_FORMAT_H

 #include <iosfwd>
+#include "format_expr.h"
+#include "format_type.h"


No, please don't. Why would this be necessary?

Need the declaration where used - I thought it made more sense to include them here so people can use format.h without further includes, but happy to devolve this to use sites.

Yes, code should use format_expr.h or format_type.h. If format.h were to be used directly then this should be done consistently across the code base.

tautschnig · 2018-04-23T15:28:28Z

src/util/unwrap_nested_exception.cpp

+
+#include <sstream>
+#include <util/invariant.h>
+#include <util/string_utils.h>


Use "..." within the folder instead of angle brackets.

tautschnig · 2018-04-23T15:29:21Z

src/util/unwrap_nested_exception.cpp

+  catch(const std::exception &e)
+  {
+    std::string nested_message = unwrap_exception(e, level + 1);
+    // Some exception messages already end in  a new line (e.g. as they have


Nit pick: two spaces between in and a.

tautschnig · 2018-04-23T15:29:45Z

src/util/unwrap_nested_exception.cpp

+#include "throw_with_nested.h"
+
+#include <exception>
+#include <string>


The header file already includes those two.

majakusber

Looks good, only one typo and please make sure to put the TODO ticket number in the code too.

majakusber · 2018-04-23T15:52:27Z

src/util/throw_with_nested.h

+
+#ifdef _MSC_VER
+#include <stdexcept>
+// TODO(tkiley): Nested exception logging not supported on windowsdue to bug


Typo: windowsdue to bug -> Windows due to a bug

Store error in string to avoid dangling pointers

Remove suprisous namespace from bv_conversion_exceptions

Throw the unwrapped exception as a string

This required the symex target_equation having the namespace to resolve names

Due to bug in the VS2013 C++ compiler, using std::rethrow_if_nested or std::nested_exception is not supported. This disables trying to unwrap the exception and just prints a warning saying the nested exceptionc couldn't be printed. Don't use noexcept directly, pull both part of the nested exception into a separate file to handle discrepancies.

thk123 · 2018-04-23T16:35:07Z

All comments addressed I believe and TG pointer bump passing.

tautschnig

Looks good modulo the remaining nit picks.

tautschnig · 2018-04-23T16:38:11Z

regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

+^EXIT=6$
+--
+--
+This is a bug - this validates the error output.


Nit pick: what does "This" refer to? The fact that this exception fires is some sort of bug, but the test case as set up now isn't. How about "The exception thrown in this test is the symptom of a bug; the purpose of this test is the validate the output of that exception."

tautschnig · 2018-04-23T16:38:26Z

src/goto-symex/equation_conversion_exceptions.h

+
+#include <ostream>
+
+#include <util/format.h>


format_expr.h

tautschnig · 2018-04-23T16:40:46Z

src/goto-symex/symex_target_equation.cpp

@@ -11,13 +11,21 @@ Author: Daniel Kroening, [email protected]

 #include "symex_target_equation.h"

+#include <util/format.h>


Unnecessary.

31c47c2 Merge pull request diffblue#2113 from diffblue/java_new_array_data fb3025d Merge pull request diffblue#2107 from thk123/feature/TG-3271/interpreter-tracking-mock-exceptions 32bf48e Merge pull request diffblue#2105 from tautschnig/determinise-test 7254a2a show java_new_array_data side effects 0f1482c Merge pull request diffblue#2094 from smowton/smowton/fix/tmp-object-factory-prefix 3cfec66 Merge pull request diffblue#2106 from diffblue/ptrmember_on_array bf4c39c Merge pull request diffblue#1966 from JohnDumbell/JohnDumbell/Update-Assertion-Validation 74a37c6 Merge pull request diffblue#1988 from tautschnig/cadical 74dc576 Merge pull request diffblue#2003 from tautschnig/bitfield-offset 8916906 Merge pull request diffblue#2008 from tautschnig/section-bug 0bd83ab Extension to interpreter class a0ca0ba fix array->f typechecking e1f4120 Make virtual function resolution independent of string table entry ordering 714ccff Merge pull request diffblue#2072 from danpoe/feature/small-shared-two-way-ptr 16b6c20 Merge pull request diffblue#2046 from thk123/gs_tg2922 04cb909 Merge pull request diffblue#2102 from thk123/formatting/sort-includes-clang-format 7070ba1 Sort includes using clang-format 9874a6b Reformatting touched output function f2a4054 Remove redundant default constructor 54fb9ab Use format rather than from_expr for output 781bf7c Introduce exceptions for all conversion steps. 21997b2 Add documentation to convert_bitvector 015b284 Test demonstrating logging with clause for dealing with Windows 9d41b0c Disable nested exception printing for Windows b866015 Provide the original goto statement in the error a97bc28 Introduce throwing a guard conversion exception 12f25c2 Introduce throwing bv_conversion expection 9bd5222 Convert flatten_byte_extract to use structured exceptions 3207291 Introduce nested exception printing 35c4be7 Small shared two way pointer 7d247da Merge pull request diffblue#2099 from mgudemann/bugfix/build/glucose_syrup 1776a9e Merge pull request diffblue#1950 from romainbrenguier/refactor/prop_conv_straightforward 4147243 Change set_variable_name API to consume irep_idt 2d8be06 Rename `it` to pair in boolbvt::print_assignment 4365c28 Simplify boolbvt::set_to b18109f Make make_(free_)bv_expr return exprt 5724a35 Simplify loop in prop_conv::get 4987f3a Remove useless comments 13e87a9 Simplify dec_solve a0500f6 Use standard algorithm for finding an element ba13c94 Use auto for iterator types 9179571 Remove useless includes a905a07 Replace throws by invariant or preconditions 7db44fc Remove virtual keyword where not needed 990f33e Initialize at declaration instead of construction c1a93b3 Renaming `it` to symbol 8eb20f6 Use ranged for dc799e0 Assert replaced by unreachable c34e073 Add support for CaDiCaL 1bd9efd Merge pull request diffblue#2097 from peterschrammel/java-cleanup-replace a079f46 Clang-format moved file 2eb3714 Move replace_java_nondet to java_bytecode 9a8c292 Remove unnecessary include c8cf100 Remove Java refs from ANSI-C docs 0090952 Merge pull request diffblue#2096 from diffblue/cleanout-java aa3caa3 Fix CMake build for Glucose Syrup 1156930 Merge pull request diffblue#1244 from tautschnig/goto-gcc-at-fix 706e391 Merge pull request diffblue#2093 from owen-jones-diffblue/owen-jones-diffblue/remove_unnecessary_irep_id_hash 290feb4 Merge pull request diffblue#2095 from diffblue/get_json_stream_precondition ac2df21 Merge pull request diffblue#2027 from tautschnig/linking-multiple-conflicts dd0d602 Merge pull request diffblue#2030 from tautschnig/goto-cc-linux-kernel 42e58d4 Merge pull request diffblue#2085 from tautschnig/from_expr-cleanup 692f92d remove dependency on java_bytecode 8c6165d precondition for get_json_stream() e28a662 Remove unused typedef 5626fb7 Merge pull request diffblue#2092 from smowton/smowton/cleanup/diffblue-spelling 4840154 Replace stack by deque and use range-based for loop 987edbe Use range-based for loops 92ac82c Remove redundant irep_id_hash for unordered maps dc2b436 Remove redundant irep_id_hash for sets 5aa2c2d Attribute main function arguments to __CPROVER_start b7ef5af Merge pull request diffblue#2053 from owen-jones-diffblue/owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions 252474f String tests: DiffBlue -> Diffblue de1915a Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-no-candidate-callees d73f6bc Make directed callgraph include nodes with no edges 2a45e61 Only the top-level section should be considered for renaming 9c66a66 fixup! Support __attribute__((section("x")) e133964 C front-end: Section/ASM renaming also needs to be applied to aliases 0cfc72f Test --call-graph and --reachable-call-graph 1c34d22 Test lazy-loading when there are no candidates 289a439 Deal with virtual function calls with no candidate targets 9347615 Remove incorrect comment 18b1962 Fix order of parameters in function header 82058da Store virtual function calls instead of virtual call-sites 3653550 Use unordered set of irep_ids in ci_lazy_methods c31d43f Remove code duplication 945f885 Rename two variables and make one more local b7d70e7 Replace do-while loop with equally valid while loop 58b990d Use from_{expr,type} matching the language of the expression/type 177c8c1 goto-cc: support thin ar archives, refactoring e80008e goto-cc: support GCC's print-sysroot* options 38e6fa5 Accept the --build-id option in goto-ld f3bbb12 Linking: report multiple conflicts 495f109 Fixing member offset computation in presence of bitfields 5109eab Add @<file> arguments to the original command line 97d556e Update desc file to add pass variables. eea76ec Add a regression test. c14e907 Increase AssertionError arguments allowed from 2 to 3 git-subtree-dir: cbmc git-subtree-split: 31c47c2

thk123 added the do not merge label Apr 12, 2018

thk123 requested review from kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners April 12, 2018 11:27

thk123 force-pushed the gs_tg2922 branch from bac6831 to ed76900 Compare April 12, 2018 14:54

thk123 requested a review from chrisr-diffblue as a code owner April 12, 2018 16:02

majakusber approved these changes Apr 16, 2018

View reviewed changes

thk123 force-pushed the gs_tg2922 branch from 6d2b7f9 to 705ee65 Compare April 16, 2018 11:10

thk123 force-pushed the gs_tg2922 branch from 705ee65 to a2482db Compare April 16, 2018 13:08

thk123 force-pushed the gs_tg2922 branch from a2482db to 5af6a77 Compare April 16, 2018 13:19

thk123 mentioned this pull request Apr 17, 2018

Enhance split_string to support splitting on white space [TG-2922] #2071

Merged

thk123 force-pushed the gs_tg2922 branch from 5af6a77 to 9b45302 Compare April 19, 2018 16:38

thk123 removed the do not merge label Apr 19, 2018

thk123 force-pushed the gs_tg2922 branch from 9b45302 to 467fe91 Compare April 20, 2018 10:35

thk123 force-pushed the gs_tg2922 branch from 467fe91 to 390aadd Compare April 20, 2018 10:40

thk123 force-pushed the gs_tg2922 branch from 2d6313d to 18018e9 Compare April 23, 2018 12:50

thk123 commented Apr 23, 2018

View reviewed changes

thk123 force-pushed the gs_tg2922 branch 2 times, most recently from f7fd0a1 to 069eeb1 Compare April 23, 2018 14:23

tautschnig reviewed Apr 23, 2018

View reviewed changes

majakusber approved these changes Apr 23, 2018

View reviewed changes

svorenova and others added 6 commits April 23, 2018 17:26

Introduce nested exception printing

3207291

Convert flatten_byte_extract to use structured exceptions

9bd5222

Store error in string to avoid dangling pointers

Introduce throwing bv_conversion expection

12f25c2

Remove suprisous namespace from bv_conversion_exceptions

Introduce throwing a guard conversion exception

a97bc28

Throw the unwrapped exception as a string

Provide the original goto statement in the error

b866015

This required the symex target_equation having the namespace to resolve names

thk123 force-pushed the gs_tg2922 branch from 069eeb1 to 0208aae Compare April 23, 2018 16:34

tautschnig approved these changes Apr 23, 2018

View reviewed changes

thk123 force-pushed the gs_tg2922 branch from 0208aae to 08237fc Compare April 23, 2018 16:44

thk123 added 6 commits April 23, 2018 17:46

Test demonstrating logging with clause for dealing with Windows

015b284

Add documentation to convert_bitvector

21997b2

Introduce exceptions for all conversion steps.

781bf7c

Use format rather than from_expr for output

54fb9ab

Remove redundant default constructor

f2a4054

Reformatting touched output function

9874a6b

thk123 force-pushed the gs_tg2922 branch from 08237fc to 9874a6b Compare April 23, 2018 16:46

thk123 merged commit 16b6c20 into diffblue:develop Apr 24, 2018

thk123 deleted the gs_tg2922 branch April 24, 2018 09:02

tautschnig mentioned this pull request May 17, 2018

Goto program and SSA validation #1880

Closed


		#include "goto_symex_state.h"
		#include "equation_conversion_exceptions.h"


		#include <util/namespace.h>

		#include <langapi/language_util.h>

		@@ -11,13 +11,21 @@ Author: Daniel Kroening, [email protected]

		#include "symex_target_equation.h"

		#include <util/format.h>

[TG-2922] Improve logging for byte flatten exceptions #2046

[TG-2922] Improve logging for byte flatten exceptions #2046

Conversation

thk123 commented Apr 12, 2018 • edited by danpoe Loading

tautschnig commented Apr 12, 2018

tautschnig commented Apr 12, 2018

majakusber commented Apr 12, 2018 • edited Loading

tautschnig commented Apr 12, 2018 • edited Loading

thk123 commented Apr 12, 2018

thk123 commented Apr 12, 2018

tautschnig commented Apr 13, 2018

majakusber left a comment • edited Loading

Choose a reason for hiding this comment

thk123 commented Apr 16, 2018

thk123 commented Apr 16, 2018

thk123 commented Apr 19, 2018

tautschnig commented Apr 19, 2018

thk123 commented Apr 20, 2018

thk123 commented Apr 20, 2018

Choose a reason for hiding this comment

thk123 commented Apr 23, 2018 • edited Loading

thk123 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

thk123 commented Apr 23, 2018

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

majakusber left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Apr 23, 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

thk123 commented Apr 12, 2018 •

edited by danpoe

Loading

majakusber commented Apr 12, 2018 •

edited

Loading

tautschnig commented Apr 12, 2018 •

edited

Loading

majakusber left a comment •

edited

Loading

thk123 commented Apr 23, 2018 •

edited

Loading