Handle empty structs in the back-end (and a number of induced fixes) #2161

tautschnig · 2018-05-07T14:14:53Z

I will need to break this PR apart, but I'll publish it in full for visibility. My original intent was just to fix the problem didn't handle empty structs (regression test included), which causes unnecessary failures in SV-COMP.

While I will split it up to enable reasonable reviewing, it should actually be clean and be ready for an evaluation against test-gen.

tautschnig · 2018-05-07T14:34:34Z

I have created ~~#2162, #2163, #2164, #2165, #2166~~ to factor out the initial parts.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 51c11f8).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: 02a13a2).

smowton

Couple of things to check, otherwise lgtm

smowton · 2018-06-15T09:08:28Z

src/util/pointer_offset_size.cpp

-    if(cellidx < 0 || !cellidx.is_long())
+    const array_typet &array_type = to_array_type(source_type);
+
+    // no arrays of non-byte, zero-, or unknown-sized objects


non-byte-aligned?

smowton · 2018-06-15T09:11:50Z

regression/systemc/Array4/test.desc

 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+warning: ignoring byte_extract_little_endian


Do you mean this to be a comment?

Yeah... along with the previous line that does seem a little bizaar.

smowton · 2018-06-15T09:13:24Z

src/solvers/flattening/pointer_logic.cpp

-
-    return object_rec(rest, pointer_type, tmp);
+    return plus_exprt(
+      address_of_exprt(deep_object.op0(), pointer_type(char_type())),


Doesn't this need an explicit typecast?

tautschnig · 2018-10-15T19:00:46Z

Needs to be rebased once #3185 is merged.

martin-cs

A few minor comments. Shouldn't take much after the rebase.

martin-cs · 2018-10-16T10:29:45Z

regression/cbmc/Empty_struct2/main.c

+#pragma pack(1)
+struct S
+{
+  int x;


If I was a complete sadist I might suggest making this an int8_t because then we have to deal with the packing rules around an empty structure. If y was one as well you'd hope that sizeof(struct S) would be sizeof(int8_t) * 2 rather than 2 (or 3) times the minimum alignment unit.

martin-cs · 2018-10-16T10:30:32Z

regression/systemc/Array4/test.desc

 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+warning: ignoring byte_extract_little_endian


Yeah... along with the previous line that does seem a little bizaar.

regression/systemc/Array4/test.desc

martin-cs · 2018-10-16T10:32:22Z

src/solvers/flattening/pointer_logic.cpp

-    return src;
+    return plus_exprt(
+      address_of_exprt(deep_object.op0(), pointer_type(char_type())),
+      from_integer(pointer.offset / subtype_bytes, index_type()));


martin-cs · 2018-10-16T10:33:24Z

src/util/pointer_offset_size.cpp

+
+      if(
+        offset * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
+        offset * 8 + target_size <= m_offset_bits + m_size)


8? Are we really hard-coded to have 8-bit bytes?

Well, once #917 is merged (after me reworking some of it) that should no longer be the case.

OK; I'll leave this one for now.

We now support pointers into structs with zero-sized members, which is a GCC extension that we otherwise do support.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: d4296f1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89834675

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and smowton as code owners May 7, 2018 14:14

tautschnig self-assigned this May 7, 2018

tautschnig force-pushed the empty-struct branch from 38a3772 to a4cc466 Compare May 7, 2018 15:09

tautschnig force-pushed the empty-struct branch 3 times, most recently from bacc8c1 to 2b09684 Compare June 7, 2018 11:04

tautschnig added the bugfix label Jun 7, 2018

tautschnig assigned kroening and unassigned tautschnig Jun 7, 2018

tautschnig force-pushed the empty-struct branch 2 times, most recently from 51c11f8 to 02a13a2 Compare June 14, 2018 08:32

kroening approved these changes Jun 14, 2018

View reviewed changes

tautschnig assigned smowton, peterschrammel, martin-cs and chrisr-diffblue and unassigned kroening Jun 14, 2018

allredj reviewed Jun 14, 2018

View reviewed changes

smowton approved these changes Jun 15, 2018

View reviewed changes

tautschnig assigned tautschnig and unassigned smowton, peterschrammel, martin-cs and chrisr-diffblue Jul 6, 2018

tautschnig mentioned this pull request Oct 11, 2018

Include pointer offset in counterexample output #3135

Merged

4 tasks

martin-cs reviewed Oct 16, 2018

View reviewed changes

tautschnig force-pushed the empty-struct branch from 02a13a2 to 0d005d5 Compare October 31, 2018 14:58

tautschnig requested a review from pkesseli as a code owner October 31, 2018 14:58

tautschnig added 2 commits October 31, 2018 15:46

Use get_subexpression_at_offset in simplify_byte_extract

044b004

Use get_subexpression_at_offset in pointer_logict

d4296f1

We now support pointers into structs with zero-sized members, which is a GCC extension that we otherwise do support.

tautschnig force-pushed the empty-struct branch from 0d005d5 to d4296f1 Compare October 31, 2018 15:46

allredj reviewed Oct 31, 2018

View reviewed changes

tautschnig merged commit d3612cc into diffblue:develop Oct 31, 2018

tautschnig deleted the empty-struct branch October 31, 2018 16:53

Handle empty structs in the back-end (and a number of induced fixes) #2161

Handle empty structs in the back-end (and a number of induced fixes) #2161

Uh oh!

Conversation

tautschnig commented May 7, 2018

Uh oh!

tautschnig commented May 7, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Oct 15, 2018

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented May 7, 2018 •

edited

Loading