[fix] Constant arrays should not be marked as nondet. #1632

NlightNFotis · 2017-11-28T09:58:31Z

No description provided.

chrisr-diffblue · 2017-11-28T10:05:24Z

src/goto-instrument/nondet_static.cpp

-      if(sym.type().get_bool(ID_C_constant))
+      if(sym.type().get_bool(ID_C_constant)
+        // if it's an array, we need to check the subtype
+        || sym.type().subtype().get_bool(ID_C_constant))


Should you include a test for ID_array as part of the new condition? I'd feel happier if you explicitly tested for (pseudo code) sym is array && sym subtype is constant

Also this will require recursing to avoid the same problem for multi-dimensional arrays.

chrisr-diffblue · 2017-11-28T10:10:51Z

regression/goto-instrument/nondet_static/test.desc

+^VERIFICATION SUCCESSFUL$
+g_B = \{ 10, 20, 30 \}
+--
+!(g_B = NONDET\(const signed int \[3l\]\);)


Is this pattern correct - in particular the leading !? I've not written a negative test like this yet so I'm not totally sure of the syntax here. Also, I'd almost be tempted to wildcard match the contents of the NONDET in this pattern e.g. NONDET\(.*\); or whatever, since the key thing this patch fixes and we want to preserve is that we don't expect to NONDET the constant array. By making the pattern too specific, it could be possible that a bug might introduce a new way of NONDET'ing this that has slightly different values, which then wouldn't trigger this test to fail - by making the NONDET use a broader regex, this test will then catch any bug that causes a NONDET to appear.

Agreed that there's no place for the ! here.

chrisr-diffblue

Looks good in principal, but a couple of comments to look at if you could, please :-)

tautschnig · 2017-11-28T10:21:23Z

regression/goto-instrument/nondet_static/test.desc

+--
+!(g_B = NONDET\(const signed int \[3l\]\);)
+--
+This corresponds to [PB-10] - constant arrays being marked as nondet.


What is PB-10?

tautschnig · 2017-11-28T10:22:38Z

regression/goto-instrument/nondet_static/test.desc

+^VERIFICATION SUCCESSFUL$
+g_B = \{ 10, 20, 30 \}
+--
+!(g_B = NONDET\(const signed int \[3l\]\);)


Agreed that there's no place for the ! here.

tautschnig · 2017-11-28T10:24:48Z

src/goto-instrument/nondet_static.cpp

-      if(sym.type().get_bool(ID_C_constant))
+      if(sym.type().get_bool(ID_C_constant)
+        // if it's an array, we need to check the subtype
+        || sym.type().subtype().get_bool(ID_C_constant))


Also this will require recursing to avoid the same problem for multi-dimensional arrays.

chrisr-diffblue · 2017-11-28T14:53:26Z

regression/goto-instrument/nondet_static/main.c

@@ -0,0 +1,8 @@
+const int g_A = 100;


Minor nit, feel free to ignore, but now you have extended the tests, is it worth given them slightly better names? e.g. perhaps no_nondet_static_array and no_nondet_static_multi_array or something like that?

chrisr-diffblue · 2017-11-28T14:57:36Z

src/goto-instrument/nondet_static.cpp

@@ -21,6 +21,14 @@ Date: November 2011

 #include "nondet_static.h"

+static bool


Nice 👍 but perhaps rather than making this static and hiding it away in here, would it be better to treat this as a proper utility function and move into one of the util/* files? Perhaps util/types.cpp/.h might be a good location as there is already an is_number utility function in there. Happy if you think there is a better candidate file to move it to though.

tautschnig · 2017-11-28T15:29:08Z

regression/goto-instrument/nondet_static/test.desc

+g_B = NONDET\(.*\);
+--
+This regression covers an issue with constant arrays being marked as nondet.
+


Nit: no need for blank line

tautschnig · 2017-11-28T15:30:36Z

regression/goto-instrument/nondet_static/main.c

@@ -0,0 +1,8 @@
+const int g_A = 100;
+const int g_B[]={10, 20, 30};
+int g_var;


To what extent are g_A and g_var relevant to this test (or, rather, the fact that they are global)?

tautschnig · 2017-11-28T15:31:13Z

regression/goto-instrument/nondet_static/main.c

+
+void main(void)
+{
+  g_var = g_B[g_A];


This always is undefined behaviour, I don't think that's good practice here.

tautschnig · 2017-11-28T15:31:50Z

regression/goto-instrument/nondet_static2/main.c

+
+void main(void)
+{
+  g_var = g_B[g_A][g_A];


See above for g_var, g_A, and undefined behaviour.

tautschnig · 2017-11-28T15:32:25Z

regression/goto-instrument/nondet_static2/test.desc

+--
+g_B = NONDET\(.*\);
+--
+This corresponds to [PB-10] - constant arrays being marked as nondet.


As before: what is PB-10?

tautschnig · 2017-11-28T15:33:23Z

src/goto-instrument/nondet_static.cpp

        continue;

+


Nit: newly added blank line seems unnecessary.

tautschnig · 2017-11-28T15:39:09Z

Why is this to be merged into diffblue:goto-analyzer-develop? (I guess that's the cause of it failing to build on AppVeyor.)

chrisr-diffblue · 2017-11-28T15:50:05Z

I think @NlightNFotis is still addressing comments, but thanks for the extra reviews. This is being merged into diffblue:goto-analyzer-develop because the bug that has spawned this work was reported against that branch, but currently goto-analyzer-develop is quite some number of commits behind develop or master. We have a plan and a rough schedule (pending other work, time for PR reviews, etc) for incrementally bring goto-analyzer-develop closer to develop and then merging across - so this work is intended to land back in develop eventually.

tautschnig · 2017-11-28T15:58:10Z

I'll stick with my changes-requested for the moment as I don't want to be making the same comments when a merge into develop eventually happens. But then obviously you might choose to just hit "Merge" anyhow.

chrisr-diffblue · 2017-11-28T15:59:19Z

We'll address your comments in this PR, don't worry :-)

NlightNFotis · 2017-11-29T11:29:02Z

@chrisr-diffblue @tautschnig All your comments have been addressed. Please check to see if you would like to make further comments, as this is very close to what my final solution looks like.

tautschnig · 2017-11-29T11:35:46Z

regression/goto-instrument/no_nondet_static_array/main.c

+int main(void)
+{
+  const int constant_array[]={10, 20, 30};
+  int var = constant_array[2];


Those tests will always have succeeded as the array isn't static?!

tautschnig · 2017-11-29T11:37:35Z

src/util/type.cpp

+
+bool is_constant_variable_or_array(const typet &type)
+{
+    return type.get_bool(ID_C_constant) ||


Nit pick: looks like 4-character instead of 2-character indent.

tautschnig · 2017-11-29T11:52:25Z

src/util/type.h

@@ -203,4 +203,8 @@ pre-defined types:
 bool is_number(const typet &type);
 // rational, real, integer, complex, unsignedbv, signedbv, floatbv

+// If a given type is a constant variable (e.g const int) or a constant
+// array (e.g. const int [])


Please word carefully: what does it mean for a type to be a "constant variable"? And: In C, const int [] does not actually declare a constant array, but instead declares an array of constant int elements. (This, however, implies that the entire object is constant as the size is constant.)

martin-cs

I would suggest the logic should be "if any part of the type has a const qualifier then don't nondet it". Will send some examples.

martin-cs · 2017-11-29T12:50:59Z

regression/goto-instrument/no_nondet_static_array/main.c

+{
+  static const int constant_array[]={10, 20, 30};
+  int var = constant_array[2];
+}


If it would make your life easier (and your test cases more robust), you could make this a CBMC test and add assert(var == 30);. If the verification succeeds, all is well. If it fails then something has been non-det'd that shouldn't have been.

Now you've added the cbmc regression test, do you still need this goto-instrument regression test?

martin-cs · 2017-11-29T12:51:56Z

src/util/type.h

@@ -203,4 +203,7 @@ pre-defined types:
 bool is_number(const typet &type);
 // rational, real, integer, complex, unsignedbv, signedbv, floatbv

+// Is the passed in type const qualified?
+bool is_constant_variable_or_array(const typet &type);


Comment doesn't match the function behaviour or name :-(

martin-cs · 2017-11-29T13:04:27Z

src/goto-instrument/nondet_static.cpp

@@ -50,7 +51,7 @@ void nondet_static(
        continue;

      // constant?
-      if(sym.type().get_bool(ID_C_constant))
+      if(is_constant_variable_or_array(sym.type()))
        continue;


I don't think this is quite the right logic because there are a number of cases that it doesn't cover. What about structs? What about unions? What about the difference between const int * and int * const?

[ I always mix the last ones up so I use cdelc:

cdecl> explain const int *s declare s as pointer to const int cdecl> explain const int * const s declare s as const pointer to const int cdecl> explain int * const s declare s as const pointer to int

]

martin-cs · 2017-11-29T13:54:06Z

int x;
int y = 23;
const int z = 23;

struct s { int x; };
struct s s1;
struct s s2 = { 23 };
const struct s s3 = { 23 };

struct t { int x; const int y; };
struct t t1;
struct t t2 = { 23, 23 };
const struct t t3 = { 23, 23 };

struct u { const int x; };
struct u u1;
struct u u2 = { 23 };
const struct u u3 = { 23 };

struct contains_pointer {  int x; int *p; };
struct contains_constant_pointer {  int x; const int *p; };
struct contains_pointer_to_const {  int x; int const *p; };

struct contains_pointer a[3] = { {23, &x}, {23, &x}, {23, &x} };
struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
struct contains_pointer_to_const c[3] = { {23, &z}, {23, &z}, {23, &z} };

typedef int Int;
typedef const int Const_Int;

const Int p = 23;
Const_Int q = 23;


#include <assert.h>

int main (int argc, char **argv) {
  
  /* Pass normally but fail with nondet-static */
  assert(x == 0);
  assert(y == 23);
  assert(s1.x == 0);
  assert(s2.x == 23);
  assert(a[0].x == 23);
  assert(a[0].p == &x);
  assert(c[2].x == 23);
  assert(c[2].p == &x);
  
  /* Should still pass */
  assert(z == 23);
  assert(s3.x == 23);
  assert(t1.y == 0);
  assert(t2.y == 23);
  assert(t3.x == 23);
  assert(t3.y == 23);
  assert(u1.x == 0);
  assert(u2.x == 23);
  assert(u3.x == 23);
  assert(b[1].p == &x);
  assert(p == 23);
  assert(q == 23);
  

  /* Debateable (part of struct is const, part isn't) */
  assert(t1.x == 0);
  assert(t2.x == 23);
  assert(b[1].x == 23);

  
  return 0;
}

chrisr-diffblue · 2017-12-01T16:05:11Z

regression/cbmc/no_nondet_static/main.c

+  /* Should still pass */
+  assert(z == 23);
+  assert(s3.x == 23);
+  assert(t1.y == 0); // wrong


In what way are these wrong ??? Are you sure these comments are not left over from your own debugging or something?

They are not. They are notes that I had taken while debugging. They are deleted now.

chrisr-diffblue · 2017-12-01T16:16:35Z

src/util/type.cpp

+              return component.type().get_bool(ID_C_constant);
+            if (component.type().get_bool(ID_C_constant))
+              return true;
+        }


This feels like a large amount of code duplication... and because of the code duplication it makes me wonder a little if the logic is fully right, but I'm not really sure. It looks to me like the first if block is identical to the if (subtype.id() == ID_symbol) {} block in the second block - so I'd start by factoring that into a helper function. You may then find that what you are left with in this function can be further restructured and simplified...

chrisr-diffblue

I think the goto-analyser regression tests could probably be dropped as the cbmc regression test is much more comprehensive (thanks for that @martin-cs and @NlightNFotis - its good!) - but I think theres some code duplication that needs cleaning up.

chrisr-diffblue · 2017-12-04T11:09:30Z

src/util/type.cpp

@@ -34,3 +36,54 @@ bool is_number(const typet &type)
         id==ID_floatbv ||
         id==ID_fixedbv;
 }
+
+bool is_constant_or_has_constant_components(


Could you add some doxygen comment to this please?

chrisr-diffblue · 2017-12-04T11:11:27Z

src/util/type.cpp

+    return true;
+
+  // struct t { const int a; };
+  // struct t t1; <--


Can you expand this comment and explain the case a little better?

chrisr-diffblue

Thanks for all the cleanups and restructuring - looks good to me now.

tautschnig · 2017-12-04T14:23:33Z

src/util/type.cpp

+      for(const auto &component : struct_union_type.components())
+      {
+        if(component.type().id() == ID_pointer)
+          return component.type().get_bool(ID_C_constant);


Why do you return false early in this case? There could be a constant member?

Ah, good catch!

tautschnig · 2017-12-04T14:24:28Z

src/util/type.cpp

+    if(subtype.id() == ID_symbol)
+    {
+      const auto &new_subtype = ns.follow(to_symbol_type(subtype));
+      return has_constant_components(new_subtype);


This may cause indefinite recursion.

I would assume that this would only be indefinite recursion if the source program had a recursive data structure?

Yes. You’ll need to maintain a set of symbols that have been seen already.

I investigated this a little bit further with recursive data types, and you were right that it caused infinite recursion with the solution as it was. I have modified it to contain a termination clause by checking if its a pointer and if so, checking if it's a const without hunting it in that specific case.

tautschnig · 2017-12-04T14:24:53Z

src/util/type.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_TYPE_H

 #include <util/source_location.h>
+#include "namespace.h"


Please use a forward declaration here.

chrisr-diffblue · 2017-12-05T17:18:41Z

regression/cbmc/no_nondet_static/main.c

+struct list { const int datum; struct list * next; };
+
+// The point of this is that cbmc needs to correctly handle
+// the embedded datum int the nested struct which is const.


This comment isn't quite true. The issue is not with the datum field, its with the recursive reference to the containing structure - i.e. next.

chrisr-diffblue

Thanks for expanding the test case further and fixing up the comments. I'm slightly wondering about multi-dimensional arrays, but I think this is probably ok, and I'm happy for this to be merged into goto-analyzer-develop as it is.

martin-cs · 2017-12-05T17:36:18Z

I'm happy enough to add this to goto-analyzer-develop. I'm going to leave this here so we can get @tautschnig 's concluding thoughts; then it would be nice to get it merged to master as well.

tautschnig · 2017-12-05T17:38:00Z

Can this maybe just be re-targetted to develop? All I'd ask for is squashing commits.

martin-cs · 2017-12-05T17:41:50Z

@tautschnig Thanks for the super-prompt response. @NlightNFotis is just squashing, I will merge and then he will submit a PR to develop as well and let's merge that one too!

chrisr-diffblue

Looks good, and I'm happy for this to go in now.

martin-cs · 2017-12-07T20:18:28Z

Happy with the code but am still not sure why we are getting CI failures. Any ideas @NlightNFotis ?

chrisr-diffblue · 2017-12-07T23:03:46Z

My understanding is that the failures are only on a job that runs Alpine linux. This job doesn't run on newer branches, and I'm told that Alpine linux uses a different libc and is basically always going to fail. If you look at travis builds for other PR's on this branch you'll see a few other jobs failing, and I believe that @thk123 had suggested just disabling the Alpine linux job. Likewise, the lint failure looks more like just infrastructure cruft rather than a code issue.

chrisr-diffblue · 2017-12-07T23:12:24Z

As far as the AppVeyor failure goes, it's not one I've seen before but I wonder if its somehow related to any of the recent windows build work, or whether AppVeyor builds have just bit-rotted on this branch, given its relative age?

thk123 · 2017-12-08T10:29:25Z

The Apline build fails because it has a different definition of assert which somehow trips over or changes the result of regression tests. There is a more full discussion on #726. If this is rebased on the current develop, the alpine build is no longer run.

The windows build I don't think is related to recent changes (in part as this not based on a recent version of develop). But it is also failing on goto-analyzer-develop HEAD so isn't a result of this PR. It may be resolved by rebasing on develop or there may be a problem here. Read @chrisr-diffblue comment more carefully - I think this is just a case of bit rotting.

chrisr-diffblue reviewed Nov 28, 2017

View reviewed changes

chrisr-diffblue changed the title ~~Fix for the constant arrays marked as nondet issue.~~ [fix] Constant arrays should not be marked as nondet. Nov 28, 2017

chrisr-diffblue reviewed Nov 28, 2017

View reviewed changes

tautschnig requested changes Nov 28, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from 4d3ef5d to 81c2c22 Compare November 28, 2017 14:15

chrisr-diffblue reviewed Nov 28, 2017

View reviewed changes

tautschnig reviewed Nov 28, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from 81c2c22 to 6289a76 Compare November 29, 2017 11:27

NlightNFotis force-pushed the fotis_pb10 branch from 6289a76 to 3151b7c Compare November 29, 2017 11:30

tautschnig reviewed Nov 29, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch 2 times, most recently from ed18460 to f31809f Compare November 29, 2017 12:22

martin-cs requested changes Nov 29, 2017

View reviewed changes

tautschnig assigned NlightNFotis Nov 30, 2017

chrisr-diffblue reviewed Dec 1, 2017

View reviewed changes

chrisr-diffblue suggested changes Dec 1, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from 6d7fe0d to 3311e93 Compare December 4, 2017 10:59

chrisr-diffblue reviewed Dec 4, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from 6b1dadc to c2e5a7e Compare December 4, 2017 11:49

chrisr-diffblue approved these changes Dec 4, 2017

View reviewed changes

tautschnig reviewed Dec 4, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from eb6a1be to ccb8700 Compare December 5, 2017 17:16

chrisr-diffblue reviewed Dec 5, 2017

View reviewed changes

NlightNFotis force-pushed the fotis_pb10 branch from ccb8700 to e7e2d1c Compare December 5, 2017 17:21

chrisr-diffblue approved these changes Dec 5, 2017

View reviewed changes

tautschnig approved these changes Dec 5, 2017

View reviewed changes

martin-cs approved these changes Dec 5, 2017

View reviewed changes

Fix for the constant arrays marked as nondet issue.

1e307d4

NlightNFotis force-pushed the fotis_pb10 branch from e7e2d1c to 6bc0d15 Compare December 5, 2017 17:43

NlightNFotis mentioned this pull request Dec 5, 2017

Fix for the handling of constant arrays and members of structs being marked nondet. #1654

Merged

NlightNFotis force-pushed the fotis_pb10 branch 3 times, most recently from 27cbf2f to a2198cc Compare December 6, 2017 13:52

Fix the handling of recursive data types.

9b1a75e

NlightNFotis force-pushed the fotis_pb10 branch from a2198cc to 9b1a75e Compare December 7, 2017 09:18

chrisr-diffblue approved these changes Dec 7, 2017

View reviewed changes

chrisr-diffblue merged commit 8879771 into diffblue:goto-analyzer-develop Dec 8, 2017

NlightNFotis mentioned this pull request Dec 20, 2017

Add extra tests for the non-det issue with constants. #1678

Merged

NlightNFotis deleted the fotis_pb10 branch October 20, 2020 15:13

		@@ -21,6 +21,14 @@ Date: November 2011

		#include "nondet_static.h"

		static bool

[fix] Constant arrays should not be marked as nondet. #1632

[fix] Constant arrays should not be marked as nondet. #1632

Conversation

NlightNFotis commented Nov 28, 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

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

tautschnig commented Nov 28, 2017

chrisr-diffblue commented Nov 28, 2017

tautschnig commented Nov 28, 2017

chrisr-diffblue commented Nov 28, 2017 • edited Loading

NlightNFotis commented Nov 29, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

martin-cs commented Nov 29, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

chrisr-diffblue left a comment

Choose a reason for hiding this comment

martin-cs commented Dec 5, 2017

tautschnig commented Dec 5, 2017

martin-cs commented Dec 5, 2017

chrisr-diffblue left a comment

Choose a reason for hiding this comment

martin-cs commented Dec 7, 2017

chrisr-diffblue commented Dec 7, 2017

chrisr-diffblue commented Dec 7, 2017

thk123 commented Dec 8, 2017 • edited Loading

chrisr-diffblue commented Nov 28, 2017 •

edited

Loading

thk123 commented Dec 8, 2017 •

edited

Loading