Fix/bytecode args write from stack #951

mgudemann · 2017-05-22T22:35:06Z

alternative to #931 ; as suggested by @smowton instead of adding temporary variables for load operations, this adds temporary variables on store, and also filters for types of operations and variable names.

mgudemann · 2017-05-23T07:34:23Z

still needs a regression test for ?astore

smowton

Broadly looks good, a few specific suggestions, plus perhaps you could factor the stack backup routines into something like backup_stack_aliases (some_predicate) where the predicate differs by instruction type, looking for field or symbol or local variable references as appropriate?

smowton · 2017-05-23T09:26:51Z

regression/cbmc-java/LocalVarTable5/test.desc

@@ -4,7 +4,7 @@ test.class
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
-dead new_tmp0
+dead new_tmp[0123456789]+


You can use [0-9] for this

smowton · 2017-05-23T09:28:24Z

regression/cbmc-java/stack_var10/test.desc

+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+$


Remove this (it will match any line)

smowton · 2017-05-23T09:50:16Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      {
+        const exprt &stack_entry=stack[i];
+        exprt entry=stack_entry;
+        if(entry.id()==ID_typecast)


Probably while. I certainly try not to introduce double casts, but there are probably still places where they get introduced.

smowton · 2017-05-23T09:55:30Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        const exprt &stack_entry=stack[i];
+        if(stack_entry.id()!=ID_member)
+          continue;
+        const exprt tmp_var=tmp_variable("stack_field", stack_entry.type());


Might as well compare the member names like the symbol comparison above?

is done in the refactored code

tautschnig

Lots of mostly minor comments, but having repeated the very same comments 4-5 times makes me feel very uneasy about this. It seems a refactoring would be necessary.

tautschnig · 2017-05-23T17:10:42Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      block.add_source_location()=i_it->source_location;
+      // search dereferences on stack, replace all with values in temporary
+      // variables
+      for(size_t i=0; i<stack.size(); i++)


Is there any reason not to use a ranged for here?

I refactored the code, please have a look

tautschnig · 2017-05-24T06:52:16Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        {
+          const exprt tmp_var=
+            tmp_variable("stack_static_field", stack_entry.type());
+          code_assignt assign=code_assignt(tmp_var, stack_entry);


tautschnig · 2017-05-24T06:52:56Z

src/java_bytecode/java_bytecode_convert_method.cpp


      exprt toassign=op[0];
      if('a'==statement[0] && toassign.type()!=var.type())
        toassign=typecast_exprt(toassign, var.type());

-      c=code_assignt(var, toassign);
+      code_blockt block;
+      for(size_t i=0; i<stack.size(); i++)


Again: ranged for?

tautschnig · 2017-05-24T06:53:00Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        {
+          const exprt tmp_var=
+            tmp_variable("stack_store", stack_entry.type());
+          code_assignt assign=code_assignt(tmp_var, stack_entry);


As above: code_assignt assign(tmp_var, stack_entry);

tautschnig · 2017-05-24T06:53:02Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        }
+      }
+
+      code_assignt assign=code_assignt(var, toassign);


code_assignt assign(var, toassign);

tautschnig · 2017-05-24T06:53:08Z

src/java_bytecode/java_bytecode_convert_method.cpp

+          const exprt tmp_var=
+            tmp_variable("stack_iinc_lvar", java_int_type());
+          block.copy_to_operands(
+            code_assignt(tmp_var, locvar));


Make that code more similar to the above by introducing a temporary variable, which will then also have the source location assigned.

tautschnig · 2017-05-24T06:53:10Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+      // create temporary variables to save values of member exprts
+      for(size_t i=0; i<stack.size(); i++)


tautschnig · 2017-05-24T06:53:12Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        if(stack_entry.id()!=ID_member)
+          continue;
+        const exprt tmp_var=tmp_variable("stack_field", stack_entry.type());
+        code_assignt assign=code_assignt(tmp_var, stack_entry);


tautschnig · 2017-05-24T06:53:14Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+      // create temporary variables to save values of static fields
+      for(size_t i=0; i<stack.size(); i++)


tautschnig · 2017-05-24T06:53:29Z

src/java_bytecode/java_bytecode_convert_method.cpp

+          continue;
+        const exprt tmp_var=
+          tmp_variable("stack_astore", stack_entry.type());
+        code_assignt assign=code_assignt(tmp_var, stack_entry);


code assignt assign(tmp_var, stack_entry);

smowton

LGTM

tautschnig · 2017-05-25T13:02:05Z

src/java_bytecode/java_bytecode_convert_method.cpp

+            stack_entry.id()==ID_member)
+    {
+      const irep_idt &entry_id=
+        to_member_expr(stack_entry).get(ID_component_name);


Use .get_component_name()

tautschnig

Just one minor API-usage suggestion, but otherwise looks good. Thanks a lot for all the refactoring!

concerned bytecode instructions: - iinc - pustatic - putfield - ?store - ?astore

mgudemann · 2017-05-25T13:36:23Z

all fixed

mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from 84cc74b to b3e4296 Compare May 23, 2017 07:32

mgudemann requested review from smowton and tautschnig May 23, 2017 07:33

smowton approved these changes May 23, 2017

View reviewed changes

mgudemann mentioned this pull request May 23, 2017

Introduce temporary stack variables for getfield/-static and ?load #931

Closed

tautschnig requested changes May 24, 2017

View reviewed changes

mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from b3e4296 to ed0b3b1 Compare May 24, 2017 16:27

Matthias Güdemann added 7 commits May 24, 2017 18:40

Adapt existing regression tests

c93cb8c

Add regression tests for iload, dup, dup_x1, dup_x2

4c17377

Add regression tests for dup2, dup2_x1 and dup2_x2

21cd8a5

Add regression test for getfield, getstatic

953fb43

Add regression test for ?store

0b81ed6

Add regression test for ?astore

9368613

Add README to tests pointing to jasmin bytecode assembler

b5cbb7f

mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from ed0b3b1 to 8b4e2e9 Compare May 24, 2017 16:40

smowton approved these changes May 24, 2017

View reviewed changes

tautschnig reviewed May 25, 2017

View reviewed changes

tautschnig approved these changes May 25, 2017

View reviewed changes

Add temporary variables for values on stack for write operations

0ce085f

concerned bytecode instructions: - iinc - pustatic - putfield - ?store - ?astore

mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from 3e52f89 to 0ce085f Compare May 25, 2017 13:25

tautschnig assigned kroening May 25, 2017

tautschnig mentioned this pull request May 26, 2017

array index off by one #926

Closed

kroening merged commit a71dfb5 into diffblue:master Jun 18, 2017

mgudemann deleted the fix/bytecode_args_write_from_stack branch July 1, 2018 08:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix/bytecode args write from stack #951

Fix/bytecode args write from stack #951

mgudemann commented May 22, 2017

mgudemann commented May 23, 2017

smowton left a comment

smowton May 23, 2017

mgudemann May 24, 2017

smowton May 23, 2017

mgudemann May 24, 2017

smowton May 23, 2017

mgudemann May 24, 2017

smowton May 23, 2017

mgudemann May 24, 2017

tautschnig left a comment

tautschnig May 23, 2017

mgudemann May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

mgudemann May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

tautschnig May 24, 2017

mgudemann May 24, 2017

smowton left a comment

tautschnig May 25, 2017

tautschnig left a comment

mgudemann commented May 25, 2017

Fix/bytecode args write from stack #951

Fix/bytecode args write from stack #951

Conversation

mgudemann commented May 22, 2017

mgudemann commented May 23, 2017

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

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

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

tautschnig left a comment

Choose a reason for hiding this comment

mgudemann commented May 25, 2017