Refactor gen_nondet_init to master #1027

thk123 · 2017-06-16T17:02:16Z

I split up get_nodet_init so this PR just does this to split up the changes (and so I can get this in sooner).

This PR is already targeted to test-gen-support (#990), but to ease merging, here is a version for master.

tautschnig

It seems the comments require some cleanup.

tautschnig · 2017-06-16T17:53:11Z

src/java_bytecode/java_object_factory.cpp

@@ -250,6 +266,151 @@ void java_object_factoryt::gen_pointer_target_init(
  }
 }

+/// Initialises a primitive or object tree rooted at `expr`, of type pointer. It
+/// allocates child objects as necessary and nondet-initialising their members,
+/// or if MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated


Where is "MUST_UPDATE_IN_PLACE" set?

Apologies - comment moved across from test-gen-support but is no longer valid.

tautschnig · 2017-06-16T17:57:59Z

src/java_bytecode/java_object_factory.cpp

+    // <label1>: <expr> = &tmp$<temporary_counter>;
+    //           <code from recursive call to gen_nondet_init() with
+    //             tmp$<temporary_counter>>
+    // And the next line is labelled label2


The above comment does not coincide with the code.

How so? Since I just moved it I'm not well versed in it, but my reading of what it does matches this?

The comment refers to some previous version that would genuinely introduce labels; now the code just builds an if(...) {...} else {...} code block.

I've updated the comment to read:

// if(NONDET(_Bool) // { // <expr> = <null pointer> // } // else // { // <code from recursive call to gen_nondet_init() with // tmp$<temporary_counter>> // }

tautschnig · 2017-06-16T17:58:46Z

src/java_bytecode/java_object_factory.cpp

+}
+
+/// Initialises an object tree rooted at `expr`, allocating child objects as
+/// necessary and nondet-initialising their members, or if MUST_UPDATE_IN_PLACE


"MUST_UPDATE_IN_PLACE"?

Apologies - comment moved across from test-gen-support but is no longer valid.

tautschnig · 2017-06-16T18:00:16Z

src/java_bytecode/java_object_factory.cpp

+    class_identifier=struct_tag;
+
+  recursion_set.insert(struct_tag);
+  assert(!recursion_set.empty());


Why is this a useful assertion? (It seems to check that the STL-provided code is sound.)

Yes I agree - I have removed it (it doesn't even check struct_tag was inserted).

tautschnig · 2017-06-16T18:01:37Z

src/java_bytecode/java_object_factory.cpp

+#if 0
+      irep_idt _class_identifier=
+        _is_sub?(class_identifier.empty()?struct_tag:class_identifier):"";
+#endif


What is this code possibly useful for?

Don't know - looks to have been originally written by @kroening and ifdef'd out by @mgudemann, do either of you have any comments?

@thk123 should be removed, is an artifact of changing API of gen_nondet_init and a larger refactoring for a Java front-end cleanup

Broke up the code handling initilising a pointer into a standalone function.

Split out the logic for initilising a struct into a standalone method

Removing an assertion that validates the STL lib being correct. Changed assert to invariant that all components on a struct have a name.

thk123 · 2017-06-28T15:08:37Z

@tautschnig Done all your requests I believe.

peterschrammel · 2017-06-29T20:37:17Z

src/java_bytecode/java_object_factory.cpp

@@ -250,6 +266,144 @@ void java_object_factoryt::gen_pointer_target_init(
  }
 }

+/// Initialises a primitive or object tree rooted at `expr`, of type pointer. It


-ize- (whole file)

thk123 mentioned this pull request Jun 16, 2017

Refactor gen_nondet_init #990

Merged

thk123 force-pushed the refactor/gen-nondet-init-master branch from ddfc227 to 9af409e Compare June 16, 2017 17:05

tautschnig requested changes Jun 16, 2017

View reviewed changes

thk123 force-pushed the refactor/gen-nondet-init-master branch 2 times, most recently from feee078 to bc8db6d Compare June 19, 2017 09:28

thk123 added 4 commits June 28, 2017 16:07

Split up gen_nondet_init function

5a88619

Broke up the code handling initilising a pointer into a standalone function.

Split up gen_nondet_init for structs

f4e8a9a

Split out the logic for initilising a struct into a standalone method

Added missing comment to class_hieracrchyt

0547fae

Correcting assertions

e873e00

Removing an assertion that validates the STL lib being correct. Changed assert to invariant that all components on a struct have a name.

thk123 force-pushed the refactor/gen-nondet-init-master branch from bc8db6d to e873e00 Compare June 28, 2017 15:08

tautschnig approved these changes Jun 28, 2017

View reviewed changes

peterschrammel reviewed Jun 29, 2017

View reviewed changes

peterschrammel approved these changes Jun 29, 2017

View reviewed changes

peterschrammel added enhancement Java Front End labels Jun 29, 2017

peterschrammel assigned kroening Jun 29, 2017

kroening merged commit 9d232d4 into diffblue:master Jun 30, 2017

thk123 deleted the refactor/gen-nondet-init-master branch June 30, 2017 11:45

Refactor gen_nondet_init to master #1027

Refactor gen_nondet_init to master #1027

Uh oh!

Conversation

thk123 commented Jun 16, 2017

Uh oh!

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

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!

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!

thk123 commented Jun 28, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!