Don't phi-merge uninitialised objects #2168

JohnDumbell · 2018-05-08T15:19:13Z

This is the work mentioned in the last comment on #2121, making it so that a generation 0 of a symex variable means it's never been initialised in both Java and C. The approach is on an allocate to assign a nondet to it if it isn't zero-init'd to begin with, and then if we see a gen zero then to not consider it during conditionals on phi merges.

Along with these is a small change to test.pl's multi-line match option to enable traditional regex multi-line matching. The m flag causes ^ and $ to actually match correctly on new line/carriage returns, where before the match was actually on the entire file so ^ was just beginning of file $ was the end. This also fixes a few tests' failure condition where this subtle difference wasn't noticed and '^warning: ignoring' is used.

tautschnig

I'm struggling to understand why this proposal is the adequate solution for the problem. From #2121 it seems the problem is one of the points-to analysis not being sufficiently smart. I'll comment more over there. (Edit: That was me being dense.)

With this PR the commit message doesn't have information that would enable a future reader of this commit to understand what's going on. Please make a habit of writing good commit messages.

Edit 2: We also need tests outside Java.

tautschnig · 2018-05-08T18:42:56Z

regression/test.pl

@@ -174,7 +174,7 @@ ($$$$$$$$$)
            binmode $fh;
            my $whole_file = <$fh>;
            $whole_file =~ s/\r\n/\n/g;
-            my $is_match = $whole_file =~ /$result/;
+            my $is_match = $whole_file =~ /$result/m;


This is great, but could it please be put in a separate commit? The explanation in the PR is absolutely necessary to understand this, but will never make it to the commit history at this stage.

Thanks for factoring it out into a separate commit. Could you please also add the text from the PR to body of the commit message? It's really informative, and should be preserved!

Ah, sorry, fixed. Still getting fully used to git.

smowton

Looks good, some small changes

Additional tests that would be good (in each case for both C and Java): check that locals, static locals (namespaced globals), normal globals and dynamic allocations all behave as expected.

smowton · 2018-05-09T13:08:02Z

regression/cbmc-java/PhiMergeConstantPropogation/Main.java

@@ -0,0 +1,30 @@
+public class Main {
+
+    public int phiMerge(Boolean trigger) {


sp s/propogation/propagation (in filename and elsewhere)

smowton · 2018-05-09T13:09:31Z

regression/cbmc-java/PhiMergeConstantPropogation/test.desc

+Main.class
+--function Main.phiMerge --show-vcc
+activate-multi-line-match
+^.*dynamic_object2#2 == \{ \.@class_identifier="java::Main\$Temp",\s*\.@lock=false \}$


Should probably check for the other dynamic object too (the instance of Temp and the instance of Ephemeral)

Decided to change the logic to make it more robust, it now just makes sure there's no gen zero objects in guards, doesn't matter where they are.

smowton · 2018-05-09T13:11:23Z

src/goto-symex/symex_goto.cpp

@@ -429,6 +429,14 @@ void goto_symext::phi_function(
      rhs=goto_state_rhs;
    else if(goto_state.guard.is_false())
      rhs=dest_state_rhs;
+    else if(goto_state.level2_current_count(l1_identifier) == 0)


Add comments briefly explaining why these checks are here

Added a comment block at the top of the if.

smowton · 2018-05-09T13:13:48Z

src/goto-symex/symex_builtin_functions.cpp

@@ -184,6 +184,12 @@ void goto_symext::symex_allocate(
    else
      throw "failed to zero initialize dynamic object";
  }
+  else
+  {
+    exprt nondet = build_symex_nondet(object_type);


Point of interest: you've copied the case for x = NONDET(int) rather than the case from code_declt("x", java_int_type()) for example. Check how their behaviour differs if at all.

I can't see any major deviations - the code isn't identical but the intentions seem the same and most of the code in decl is run in assign at some point too. One thing to note is that assign propagates the nondet as a constant, while the decl code flat-out disables any propagation, would that be an issue?

It'll only disable it for the time being, but it's interesting. I'm not quite well informed enough to give an authoritative answer -- I suggest running this by @peterschrammel and post his answer here.

I'd argue that this is what #35 is about, and you're doing parts of that here, even though the full value only unfolds once you break down nondet symbols into their individual fields.

JohnDumbell · 2018-05-09T17:48:12Z

Added a new set of tests and made some minor revisions to the code and commits in regards to comments (sans talking to peter). I'm not well versed in C so if there's a potential condition I've missed just say.

tautschnig

As expressed in a few places by reviewers: more comments and documentation (commit messages) needed, but otherwise looks good to me.

tautschnig · 2018-05-09T18:09:38Z

regression/test.pl

@@ -174,7 +174,7 @@ ($$$$$$$$$)
            binmode $fh;
            my $whole_file = <$fh>;
            $whole_file =~ s/\r\n/\n/g;
-            my $is_match = $whole_file =~ /$result/;
+            my $is_match = $whole_file =~ /$result/m;


Thanks for factoring it out into a separate commit. Could you please also add the text from the PR to body of the commit message? It's really informative, and should be preserved!

tautschnig · 2018-05-09T18:13:23Z

src/goto-symex/symex_builtin_functions.cpp

@@ -184,6 +184,12 @@ void goto_symext::symex_allocate(
    else
      throw "failed to zero initialize dynamic object";
  }
+  else
+  {
+    exprt nondet = build_symex_nondet(object_type);


I'd argue that this is what #35 is about, and you're doing parts of that here, even though the full value only unfolds once you break down nondet symbols into their individual fields.

smowton · 2018-05-10T10:52:08Z

regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.java

+        return obj.val;
+    }
+
+    private Ephemeral local;


This isn't really a local -- in Java we can't really have a local object at all (but we can have a local reference or pointer). Really the one labelled dynamic is using a local variable to store the pointer, and this one is using a member field to store it.

smowton · 2018-05-10T10:52:19Z

regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.java

+        return local.val;
+    }
+
+    private static Ephemeral staticLocal;


Again, staticField would be more accurate

smowton · 2018-05-10T10:53:54Z

regression/cbmc-java/phi-merge_uninitialized_values/local.desc

+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0


In test.desc files a second -- delimits comments. You should add one and then comment on what these regexes are looking for.

Format example:

CORE Main.class --other --arguments Must find this Also must find this -- Musn't find this Nor this -- This is a comment This is another comment

smowton · 2018-05-10T10:56:29Z

regression/cbmc/phi-merge_uninitialized_values/test.c

+  assert(*obj == 20);
+}
+
+int *staticLocal;


In C we really can have local objects. For all the cases other than dynamic, don't use malloc, instead declare the object on the stack, for example int local;

Static locals are possible in C, and are effectively globals that are only accessible in that function. For example,

int f() { static int staticvar = 100; return staticvar++; } void main() { assert(f() == 100); // Passes assert(f() == 101); // Passes }

The final missing case for C is a "real" global. For example:

int global; int main() { global = 1234; ... }

peterschrammel · 2018-05-10T13:05:23Z

regression/cbmc/phi-merge_uninitialized_values/test.c

+  }
+  else
+  {
+    *obj = 20;


Maybe also add a test where one branch is missing and the merge must happen.

smowton · 2018-05-11T10:05:59Z

regression/cbmc/phi-merge_uninitialized_values/test.c

+void dynamicAllocationUninitialized(int trigger)
+{
+  int *obj;
+  obj = (int*)malloc(sizeof(int));


For symmetry with the Java case this should only be allocated on one branch (i.e. we should allocate within the if / else)

smowton · 2018-05-11T10:06:24Z

This is looking much improved, just commented with one more nitpick, let me know when this is ready for re-review

This change means that if a generation zero symex variable is seen it can be assumed to not have been allocated at any point and still have its default values. We use this knowledge to then not add a guard on a phi merge that has a gen zero on its lhs or rhs, instead just simply assigning the other side directly.

This is a change to the multi-line match option to enable traditional regex multi-line matching. The m flag causes ^ and $ to actually match correctly on new line/carriage returns, where before the match was actually on the entire file so ^ was just beginning of file $ was the end. This also fixes a few tests' failure condition where this subtle difference wasn't noticed and '^warning: ignoring' is used.

smowton · 2018-05-11T15:18:21Z

Looks great, merge once tests are passing I say

JohnDumbell · 2018-05-11T16:19:16Z

Made all requested changes, I'll fix any issues that the CI flags up but right now it looks like some weird timeout issues, so I'll just re-run it until it gives me something useful or passes.

tautschnig · 2018-05-11T18:58:39Z

https://www.traviscistatus.com/ says there are problems with macOS, so it might take a little longer... (all other jobs have passed here).

da61186 Merge pull request diffblue#2182 from diffblue/trace-debug 5acf313 Merge pull request diffblue#2176 from mgudemann/fix/glucose_build_g++ e82dca0 formatting of debug output of traces f891f37 Merge pull request diffblue#2168 from JohnDumbell/bugfix/phi_merge_uninitialized 6faf376 Enable 'm' flag on regex for multi-line tests 646cf29 Add nondet assignment to non-zero'd allocations in symex 213db5f Remove trailing `;` from namespace closing bracket git-subtree-dir: cbmc git-subtree-split: da61186

JohnDumbell requested review from kroening, peterschrammel and tautschnig as code owners May 8, 2018 15:19

tautschnig requested changes May 8, 2018

View reviewed changes

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch from 71c61fe to f73be05 Compare May 9, 2018 10:37

JohnDumbell changed the title ~~[SEC-370] Don't phi-merge uninitialised objects~~ Don't phi-merge uninitialised objects May 9, 2018

smowton reviewed May 9, 2018

View reviewed changes

smowton mentioned this pull request May 9, 2018

Symex: don't phi-merge Java dynamic objects with uninitialised data #2121

Closed

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch 2 times, most recently from 53f8d95 to 1cce880 Compare May 9, 2018 17:40

tautschnig approved these changes May 9, 2018

View reviewed changes

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch 4 times, most recently from d03e11f to 2ba33cf Compare May 10, 2018 10:16

smowton reviewed May 10, 2018

View reviewed changes

peterschrammel added the Needs rebase label May 10, 2018

peterschrammel reviewed May 10, 2018

View reviewed changes

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch 2 times, most recently from bcc5211 to c1a4f70 Compare May 10, 2018 15:02

smowton reviewed May 11, 2018

View reviewed changes

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch 2 times, most recently from 2df875b to 7ba294d Compare May 11, 2018 14:28

JohnDumbell added 2 commits May 11, 2018 16:11

JohnDumbell force-pushed the bugfix/phi_merge_uninitialized branch from 7ba294d to 6faf376 Compare May 11, 2018 15:11

smowton approved these changes May 11, 2018

View reviewed changes

tautschnig mentioned this pull request May 11, 2018

Explicit nondet initialisation #35

Closed

tautschnig merged commit f891f37 into diffblue:develop May 12, 2018

tautschnig mentioned this pull request May 23, 2018

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486] #2220

Merged

JohnDumbell deleted the bugfix/phi_merge_uninitialized branch October 23, 2018 16:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Don't phi-merge uninitialised objects #2168

Don't phi-merge uninitialised objects #2168

JohnDumbell commented May 8, 2018

tautschnig left a comment •

edited

Loading

tautschnig May 8, 2018

tautschnig May 9, 2018

JohnDumbell May 10, 2018

smowton left a comment

smowton May 9, 2018

smowton May 9, 2018

JohnDumbell May 9, 2018 •

edited

Loading

smowton May 9, 2018

JohnDumbell May 10, 2018

tautschnig May 10, 2018

smowton May 9, 2018

JohnDumbell May 9, 2018

smowton May 9, 2018

tautschnig May 9, 2018

JohnDumbell commented May 9, 2018

tautschnig left a comment

tautschnig May 9, 2018

tautschnig May 9, 2018

smowton May 10, 2018

smowton May 10, 2018

smowton May 10, 2018

smowton May 10, 2018

peterschrammel May 10, 2018

smowton May 11, 2018

smowton commented May 11, 2018

smowton commented May 11, 2018

JohnDumbell commented May 11, 2018

tautschnig commented May 11, 2018

		@@ -0,0 +1,30 @@
		public class Main {

		public int phiMerge(Boolean trigger) {

Don't phi-merge uninitialised objects #2168

Don't phi-merge uninitialised objects #2168

Conversation

JohnDumbell commented May 8, 2018

tautschnig left a comment • edited Loading

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JohnDumbell May 9, 2018 • edited Loading

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

JohnDumbell commented May 9, 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

smowton commented May 11, 2018

smowton commented May 11, 2018

JohnDumbell commented May 11, 2018

tautschnig commented May 11, 2018

tautschnig left a comment •

edited

Loading

JohnDumbell May 9, 2018 •

edited

Loading