SV-COMP 2018: Rebase of Tautschnig's branch/PR `sv-comp-2017` on `cbmc/develop` #1532

marek-trtik · 2017-10-27T09:56:13Z

@tautschnig , @peterschrammel @martin-cs : Please check the correctness of the rebase. Thank you.

!!! IMPORTANT: I ask other reviewers to postpone their reviews till the PR is fixed (NOTE: I had to create the PR in order to fix issues in Travis and mainly AppVeyor). Once the PR is ready for reviews I'll post an explicit message to this PR. Thank you for understanding. !!!

This is the rebased PR: #363

peterschrammel · 2017-10-27T14:14:30Z

@marek-trtik, unfortunately, the minisat download is hard-coded in .travis.yml: https://travis-ci.org/diffblue/cbmc/jobs/293594798#L729
You'll have to hack https://github.com/diffblue/cbmc/blob/develop/.travis.yml#L239 to make this build on CI.

marek-trtik · 2017-10-27T15:09:19Z

Fixed. Thank you Petr!

romainbrenguier · 2017-10-30T12:43:37Z

src/solvers/flattening/bv_pointers.cpp

+    bvt invalid_bv, null_bv;
+    encode(pointer_logic.get_invalid_object(), invalid_bv);
+    invalid_bv.erase(invalid_bv.begin(), invalid_bv.begin()+offset_bits);
+    encode(pointer_logic.get_null_object(),    null_bv);


weird spacing

romainbrenguier · 2017-10-30T12:44:08Z

src/solvers/flattening/bv_pointers.cpp

@@ -439,6 +425,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
  {
    return SUB::convert_byte_extract(to_byte_extract_expr(expr));
  }
+  else if(expr.id()==ID_byte_update_little_endian ||
+          expr.id()==ID_byte_update_big_endian)
+    throw "byte-wise updates of pointers are unsupported";


not sure we should use throw if there is no corresponding catch

Sure. However, there are already 656 such throw "... statements in our code base, e.g.:
https://github.com/diffblue/cbmc/blob/develop/src/analyses/ai.cpp#L466

romainbrenguier · 2017-10-30T12:48:23Z

src/util/guard.cpp

@@ -95,9 +95,9 @@ guardt &operator -= (guardt &g1, const guardt &g2)
  if(g1.id()!=ID_and || g2.id()!=ID_and)
    return g1;

-  sort_and_join(g1);
+  // sort_and_join(g1);


remove or use #if 0 and explain

romainbrenguier · 2017-10-30T12:48:37Z

src/util/guard.cpp

@@ -108,10 +108,12 @@ guardt &operator -= (guardt &g1, const guardt &g2)
      it2!=op2.end();
      ++it2)
  {
-    while(it1!=op1.end() && *it1<*it2)
-      ++it1;
+    /*while(it1!=op1.end() && *it1<*it2)


romainbrenguier · 2017-10-30T12:49:03Z

src/util/guard.cpp

@@ -145,9 +147,9 @@ guardt &operator |= (guardt &g1, const guardt &g2)
  }

  // find common prefix
-  sort_and_join(g1);
+  // sort_and_join(g1);


remove or use #if 0

romainbrenguier · 2017-10-30T13:54:26Z

src/analyses/goto_check.cpp

+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs=
+            if_exprt(


if_exprt rhs

romainbrenguier · 2017-10-30T13:55:41Z

src/ansi-c/expr2c.cpp

@@ -699,6 +699,7 @@ std::string expr2ct::convert_struct_type(
  if(tag!="")
    dest+=" "+id2string(tag);

+#if 0


why is this commented out?

Reverted back.

romainbrenguier · 2017-10-30T13:56:23Z

src/ansi-c/expr2c.cpp

    return convert_norep(src, precedence);

  unsigned p0;
  std::string op0=convert_with_precedence(src.op0(), p0);

-  std::string dest="MALLOC";
+  unsigned p1;
+  std::string op1=convert_with_precedence(src.op0(), p1);


romainbrenguier · 2017-10-30T14:04:57Z

src/analyses/goto_check.cpp

    else if(i.is_end_function())
    {
-      if(i.function==goto_functionst::entry_point() &&
-         enable_memory_leak_check)
+      if(i.function==goto_functionst::entry_point() && enable_memory_leak_check)


this change is not in the right commit

Reverted back.

romainbrenguier · 2017-10-30T14:06:48Z

.travis.yml

  - make -C src/ansi-c library_check
-  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
-  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir


I don't think that's a good idea to remove these flags

Sure, it is gone.

thk123

I don't think this is ready for review - though I agree with
@romainbrenguier's comments. Could you comment when it needs another review.

thk123 · 2017-10-31T12:59:43Z

.travis.yml

@@ -211,7 +211,7 @@ jobs:
            name: "diffblue/cbmc"
            description: "Travis build of ${TRAVIS_COMMIT}"
          notification_email: "[email protected]"
-          build_command_prepend: "make -C src minisat2-download"
+          build_command_prepend: "make -C src glucose-download"


This seems like a surprising change - what are the implications/justifications for this swap?

Reverted back.

thk123 · 2017-10-31T13:04:30Z

src/config.inc

@@ -5,7 +5,7 @@ BUILD_ENV = AUTO
 ifeq ($(BUILD_ENV),MSVC)
  #CXXFLAGS += /Wall /WX
 else
-  CXXFLAGS += -Wall -pedantic -Werror
+  CXXFLAGS += -Wall -Wno-parentheses


This shouldn't change

Reverted back.

tautschnig · 2017-11-01T14:58:28Z

I'm wondering how to proceed with #982 and #731, which contain a collection of the patches in this PR. Pushing on them would mean we get duplicate work through this one.

marek-trtik · 2017-11-01T15:08:09Z

@thk123 : Yes, the PR is NOT ready for a review yet. I'll post here an explicit message, when the PR is ready.

marek-trtik · 2017-11-01T15:27:46Z

@tautschnig : According to your response to @lucasccordeiro 's email I believe that #982 and #731 are (some of) those PRs factored out from #363. I think that it is still true that #363 contains all patches for SV_COMP we currently have. Also, everybody I asked told me that I should work with #363.

The goal with #363 was to prepare two branches, both rebased on the latest develop. The first branch should contain changes which should go to develop right now, and the other consisting of only SV-COMP related features. The second branch is supposed to be rebased on top of the first one. The second branch will also go to develop, but not now (after SV-COMP deadline). We will introduce a macro SV_COMP and all that code will be compiled only when the macro is defined.

Both branches are already created and they are rebased on latest develop. The first branch is already PRed (this PR). There is only one remaining thing to be resolved - fixing regression tests on Windows (on Linux build all pass).

I did not consider #982 nor #731 in this process. I am not sure whether it make a sense to use them at this point.

marek-trtik · 2017-11-01T15:39:46Z

@tautschnig : I could merge current states of #982 and #731 into this PR.

What solution would you propose?

peterschrammel · 2017-11-01T16:06:14Z

@tautschnig, Marek is fixing a long-on-Windows-is-32bits bug in these assumptions: https://github.com/tautschnig/cbmc/blob/799446487a95302106bbe8d1a9de9a88d46eceee/src/ansi-c/library/new.c#L14
Is it worth fixing them or have they become obsolete in the meanwhile?

tautschnig · 2017-11-01T16:51:03Z

@marek-trtik

@tautschnig : I could merge current states of #982 and #731 into this PR.
What solution would you propose?

If you could replace all commits with the same subject with their versions from #982 and #731 this would indeed be nice!

@peterschrammel

@tautschnig, Marek is fixing a long-on-Windows-is-32bits bug in these assumptions:

I've digged into my various pull requests, but it seems I've dropped this everywhere. One problem certainly is that the object:offset encoding is now configurable, hence any such check is somewhat questionable. Hopefully #1086 is something I'll find time for very soon...

marek-trtik · 2017-11-01T17:18:08Z

@tautschnig : Yes, I'll try to take versions of the corresponding commits from #982 and #731 (however, I'll keep fixes (CPPLINT/clang-formater) I made). So, it means, that I'll perform merge of the related commits instead of replacement.

Regarding the long-on-Windows-is-32bits issue: If I understood correctly #1086 should solve (avoid) the issue (those assumptions won't be needed anymore). However, this PR cannot be merged without the issue is solved (one way of the other). The question is whether we want to wait with merge of this PR till #1086 is merged.

tautschnig · 2017-11-01T17:36:43Z

The question is whether we want to wait with merge of this PR till #1086 is merged.

Let's try to avoid dependencies wherever possible, so: don't wait. A hack-fix should do for the moment.

tautschnig · 2017-11-01T18:14:34Z

Note that I have rebased #982 to make picking a bit easier.

marek-trtik · 2017-11-01T18:16:59Z

I fixed the issue long-on-Windows-is-32bits.

marek-trtik · 2017-11-01T18:17:33Z

@tautschnig : Thanks for the rebase. It will certainly help. However, I see there are still CPPLINT/clang-formater issues. I'll fixed them during the merge of corresponding commits.

marek-trtik · 2017-11-02T17:52:44Z

This PR now comprises #982 and #731. Also the assumptions (those with the long-on-Windows-is-32bits issue) were moved into the SV-COMP specific branch:
https://github.com/marek-trtik/cbmc/tree/sv-comp-2017-specific
which is rebased on top of the branch of this PR. However, 2 regression tests fails on the sv-comp-2017-specific branch:

regression/cbmc-java/generics_symtab1/test.desc
regression/cbmc-java/json_trace2/test.desc

I'll investigate that (but this is irrelevant to this PR).

marek-trtik · 2017-11-03T11:32:59Z

!!! To all reviewers: This PR is ready for your reviews !!!

__CPROVER_allocate takes two arguments, where the second requests zero-initialization of the newly allocated object. Thus `calloc` can be implemented efficiently.

Just ignoring them would yield unsound results.

Also includes an incomplete implementation to introduce a new L1 name for each declaration. This works for all regression tests, but fails on some larger examples.

They are constructed in a consistent order anyway.

Check whether the object part of a pointer is greater or equal the total number of objects, or equals a dynamic object that has not actually been allocated on a given trace.

tautschnig · 2018-04-03T13:39:39Z

Breaking up into series of 19 pull requests starting from #1990 all the way up to #2008.

marek-trtik requested review from kroening, martin-cs, mgudemann, peterschrammel, romainbrenguier, smowton, tautschnig and thk123 as code owners October 27, 2017 09:56

peterschrammel added the do not merge label Oct 27, 2017

marek-trtik requested a review from forejtv as a code owner October 27, 2017 15:08

romainbrenguier suggested changes Oct 30, 2017

View reviewed changes

thk123 reviewed Oct 31, 2017

View reviewed changes

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch 3 times, most recently from 1df8b94 to 47636ce Compare November 1, 2017 14:45

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch from 634bed1 to fe90cb8 Compare November 1, 2017 17:32

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch from fe90cb8 to f3c6be2 Compare November 1, 2017 17:55

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch 3 times, most recently from 2c16e06 to b8314de Compare November 2, 2017 16:41

tautschnig mentioned this pull request Nov 2, 2017

Fixes and improvements to dynamic memory handling #982

Merged

marek-trtik mentioned this pull request Nov 2, 2017

Simplifier and symex rewriting fixes/extensions #731

Merged

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch from 3debb60 to 72ae60c Compare November 3, 2017 11:32

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch from 72ae60c to ca541fd Compare November 3, 2017 12:06

tautschnig and others added 10 commits November 9, 2017 11:17

Generalize ID_malloc to ID_allocate with optional zero-init

b3591db

__CPROVER_allocate takes two arguments, where the second requests zero-initialization of the newly allocated object. Thus `calloc` can be implemented efficiently.

Abort on byte_update(pointer)

bbc3ff2

Just ignoring them would yield unsound results.

Ensure that local declarations do not introduce spurious dead warnings

ef9e7ad

Also includes an incomplete implementation to introduce a new L1 name for each declaration. This works for all regression tests, but fails on some larger examples.

Do not unnecessarily sort guard conjuncts

c4bc2ee

They are constructed in a consistent order anyway.

invalid_object(pointer) is true for all non-existent objects

19fd85d

Check whether the object part of a pointer is greater or equal the total number of objects, or equals a dynamic object that has not actually been allocated on a given trace.

fixup! invalid_object(pointer) is true for all non-existent objects

9e97463

Fixing compile issues after rebase of PR 363.

5ebd8ba

Fixing regression test.

0624b69

Fixing CPPLINTer/cnang-formater issues.

16c8bc8

Updates requested in the peer review.

eecaee0

marek-trtik force-pushed the rebase_sv-comp-2017_on_develop branch from ca541fd to eecaee0 Compare November 9, 2017 13:12

tautschnig assigned tautschnig, lucasccordeiro, peterschrammel and marek-trtik Nov 30, 2017

tautschnig mentioned this pull request Apr 3, 2018

Collection of patches for SV-COMP'17 #363

Closed

tautschnig closed this Apr 3, 2018

SV-COMP 2018: Rebase of Tautschnig's branch/PR sv-comp-2017 on cbmc/develop #1532

SV-COMP 2018: Rebase of Tautschnig's branch/PR sv-comp-2017 on cbmc/develop #1532

Conversation

marek-trtik commented Oct 27, 2017 • edited Loading

peterschrammel commented Oct 27, 2017

marek-trtik commented Oct 27, 2017

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

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 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

tautschnig commented Nov 1, 2017

marek-trtik commented Nov 1, 2017

marek-trtik commented Nov 1, 2017 • edited Loading

marek-trtik commented Nov 1, 2017

peterschrammel commented Nov 1, 2017

tautschnig commented Nov 1, 2017

marek-trtik commented Nov 1, 2017

tautschnig commented Nov 1, 2017

tautschnig commented Nov 1, 2017

marek-trtik commented Nov 1, 2017

marek-trtik commented Nov 1, 2017 • edited Loading

marek-trtik commented Nov 2, 2017 • edited Loading

marek-trtik commented Nov 3, 2017

tautschnig commented Apr 3, 2018 • edited Loading

SV-COMP 2018: Rebase of Tautschnig's branch/PR `sv-comp-2017` on `cbmc/develop` #1532

SV-COMP 2018: Rebase of Tautschnig's branch/PR `sv-comp-2017` on `cbmc/develop` #1532

marek-trtik commented Oct 27, 2017 •

edited

Loading

marek-trtik commented Nov 1, 2017 •

edited

Loading

marek-trtik commented Nov 1, 2017 •

edited

Loading

marek-trtik commented Nov 2, 2017 •

edited

Loading

tautschnig commented Apr 3, 2018 •

edited

Loading